proposition: Theorem WCR_h_star_pad_impl_h_star : cAU.Adv_WCR _ _ h_star_pad ({ 0 , 1 }^c) Z <= cAU.Adv_WCR _ _ h_star ({ 0 , 1 }^c) Y.
proof: Proof. unfold cAU.Adv_WCR, cAU.Adv_WCR_G. comp_skip. unfold Y. eapply comp_spec_impl_le. simpl. inline_first. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => fst b = a)). trivial. intuition. subst. unfold cAU.WCR_Oracle. inline_first. comp_simp. inline_first. comp_simp. simpl. eapply comp_spec_ret. intuition. simpl in *. intuition. destruct b2. simpl in *. subst. comp_simp. simpl. comp_simp. inline_first. comp_simp. eapply comp_spec_ret. intuition. unfold h_star_pad in *. case_eq (eqb a b1); intuition; rewrite H3 in H2; simpl in *. discriminate. apply eqbBvector_sound in H2. unfold HMAC_spec.h_star_pad, HMAC_spec.app_fpad in *. eapply Vector_append_inj_first in H2. unfold h_star, NMAC_to_HMAC.h_star. rewrite H2. eapply eqbBvector_complete. Qed.
imports: FCF HMAC_spec PRF NMAC_to_HMAC hF GHMAC_PRF