proposition: Theorem RF_EncryptOracle_spec : forall a x2, comp_spec (fun (y1 : Ciphertext * list (Bvector eta * Bvector eta)) (y2 : Ciphertext * (unit * list (Bvector eta * Bvector eta))) => fst y1 = fst y2 /\ snd y1 = snd (snd y2)) (RF_Encrypt (snd x2) a) (p <-$ (PRFE_Encrypt_OC (fst x2) a) (list (Bvector eta * Bvector eta)) (list_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta))) PRFE_RandomFunc (snd x2); ret (fst (fst p), (snd (fst p), snd p))).
proof: Proof. intuition. unfold RF_Encrypt, PRFE_RandomFunc, randomFunc. simpl. do 2 prog_inline_r. comp_skip. prog_simp. prog_inline_r. comp_skip. prog_inline_r. prog_simp. eapply comp_spec_ret. simpl. intuition. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime