fact: Definition F_randomFunc k_in f d := match arrayLookup_f _ f (F k_in d) with | Some r => ret (r, ((d, F k_in d), r) :: f) | None => r <-$ {0, 1}^c; ret (r, ((d, F k_in d), r) :: f) end.
imports: FCF PRF SplitVector cAU CompFold DetSem SemEquiv