proposition: Theorem PRF_A'_cost : oc_cost cost (comp_cost cost) PRF_A' (fun x => (A1_cost (x + (5 * eta))) + (A2_cost_2 (x + (5 * eta))) + x + 5 * A2_cost_1 + 6 + 7 * eta).
proof: Proof. pose proof @PRFE_Encrypt_OC_cost_2 as PRFE_Encrypt_OC_cost_2. pose proof @PRFE_Encrypt_OC_oc_cost as PRFE_Encrypt_OC_oc_cost. unfold PRF_A'. eapply oc_cost_le. costtac. eauto. eapply PRFE_Encrypt_OC_cost_1. eapply PRFE_Encrypt_OC_cost_2. eapply PRFE_Encrypt_OC_oc_cost. costtac. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_compose_binary; costtac. eapply (@cost_compose _ _ _ _ _ (fun a => (snd (fst (fst (fst a))))) (fun (a : Plaintext * Plaintext * State * unit * bool * Bvector eta * Vector.t bool eta) => (OC_Run unit_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta)) (Bvector_EqDec eta) (A2 (snd (fst (fst (fst (fst a))))) (snd (fst a), (if snd (fst (fst a)) then snd (fst (fst (fst (fst (fst a))))) else fst (fst (fst (fst (fst (fst a)))))) xor snd a)) PRFE_Encrypt_OC )) ); costtac. eapply (@cost_compose_unary _ _ _ _ _ (fun a : (Plaintext * Plaintext * State * unit * bool * Bvector eta * Vector.t bool eta) => (A2 (snd (fst (fst (fst (fst a))))) (snd (fst a), (if snd (fst (fst a)) then snd (fst (fst (fst (fst (fst a))))) else fst (fst (fst (fst (fst (fst a)))))) xor snd a))) (fun x => OC_Run unit_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta)) (Bvector_EqDec eta) x PRFE_Encrypt_OC) ). eapply cost_compose_binary; costtac. eapply cost_compose_binary; costtac. eapply cost_compose_binary; costtac. eapply cost_if_bool; costtac. eapply cost_uncurry_1. eapply cost_BVxor. eapply cost_uncurry_2. eapply cost_BVxor. eapply cost_uncurry_1. eauto. eapply cost_uncurry_2. eauto. eapply (@cost_compose _ _ _ _ _ (fun x => _) ( OC_Run unit_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta)) (Bvector_EqDec eta)) ); costtac. eapply cost_OC_Run_1. intuition. eapply cost_OC_Run_2. intuition. eapply cost_OC_Run_3. eapply cost_uncurry_1. eapply cost_compose_unary; costtac. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_eqb_bool. eapply cost_uncurry_2. eapply cost_eqb_bool. intuition. costtac. eapply cost_vec_head. intuition. costtac. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_compose_binary; costtac. simpl. eapply (@cost_compose _ _ _ _ _ (fun a => _) (fun a0 : bool * Bvector eta * Vector.t bool eta => OC_Run unit_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta)) (Bvector_EqDec eta) (A2 b0 (snd (fst a0), (if fst (fst a0) then b1 else a) xor snd a0)) PRFE_Encrypt_OC) ); costtac. eapply (@cost_compose _ _ _ _ _ (fun a => _) (fun a0 : bool * Bvector eta * Vector.t bool eta => OC_Run unit_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta)) (Bvector_EqDec eta) (A2 b0 (snd (fst a0), (if fst (fst a0) then b1 else a) xor snd a0))) ); costtac. eapply cost_compose_binary; costtac. eapply cost_compose_binary; costtac. eapply cost_if_bool; costtac. eapply cost_uncurry_1. eapply cost_BVxor. intuition. eapply cost_uncurry_2. eapply cost_BVxor. eapply cost_uncurry_2. eauto. eapply cost_OC_Run_1. intuition. eapply cost_OC_Run_2. intuition. eapply cost_OC_Run_3. eapply cost_uncurry_1. eapply cost_compose_unary; costtac. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_eqb_bool. intuition. eapply cost_uncurry_2. eapply cost_eqb_bool. intuition. costtac. eapply cost_compose_binary; costtac. eapply cost_uncurry_1. eapply cost_compose_binary; costtac. simpl. eapply (@cost_compose _ _ _ _ _ (fun a => _) (fun a0 : Bvector eta * Vector.t bool eta => OC_Run unit_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta)) (Bvector_EqDec eta) (A2 b0 (fst a0, (if y then b1 else a) xor snd a0)) PRFE_Encrypt_OC) ); costtac. eapply (@cost_compose _ _ _ _ _ (fun a => _) (fun a0 : Bvector eta * Vector.t bool eta => OC_Run unit_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta)) (Bvector_EqDec eta) (A2 b0 (fst a0, (if y then b1 else a) xor snd a0))) ); costtac. eapply cost_compose_binary; costtac. eapply cost_uncurry_2. eapply cost_BVxor. eapply cost_uncurry_2. eauto. eapply cost_OC_Run_1. intuition. eapply cost_OC_Run_2. intuition. eapply cost_OC_Run_3. intuition. costtac. eapply cost_compose_binary; costtac. simpl. eapply (@cost_compose _ _ _ _ _ (fun a => _) (fun a0 : Vector.t bool eta => OC_Run unit_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta)) (Bvector_EqDec eta) (A2 b0 (y0, (if y then b1 else a) xor a0)) PRFE_Encrypt_OC) ); costtac. eapply (@cost_compose _ _ _ _ _ (fun a => _) (fun a0 : Vector.t bool eta => OC_Run unit_EqDec (pair_EqDec (Bvector_EqDec eta) (Bvector_EqDec eta)) (Bvector_EqDec eta) (A2 b0 (y0, (if y then b1 else a) xor a0)) ) ); costtac. eapply cost_uncurry_2. eapply cost_BVxor. eapply cost_pair_2. eapply cost_uncurry_2. eauto. eapply cost_OC_Run_1. intuition. eapply cost_OC_Run_2. intuition. eapply cost_OC_Run_3. intuition. costtac. simpl. eauto. eapply PRFE_Encrypt_OC_cost_1. eapply PRFE_Encrypt_OC_cost_2. eapply PRFE_Encrypt_OC_oc_cost. eapply cost_uncurry_2. eapply cost_eqb_bool. intuition. costtac. intuition. simpl. repeat rewrite Nat.add_0_r. assert (A1_cost (eta + eta + (x + (eta + (eta + eta)))) = A1_cost (x + (eta + (eta + (eta + (eta + eta)))))). f_equal; lia. rewrite H0. clear H0. remember ( A1_cost (x + (eta + (eta + (eta + (eta + eta)))))) as t1. assert (A2_cost_2 (eta + eta + (x + (eta + (eta + eta)))) = A2_cost_2 (x + (eta + (eta + (eta + (eta + eta)))))). f_equal; lia. rewrite H0. clear H0. remember (A2_cost_2 (x + (eta + (eta + (eta + (eta + eta)))))) as t2. lia. Qed.
imports: FCF PRF Encryption RndInList OTP WC_PolyTime