sneaky bugs

Author: oskgo

src/ecPrinting.ml

@@ -388,7 +388,7 @@ module PPEnv = struct
     oget (Mint.find_opt i (fst !(ppe.ppe_univar)))
 end
 
-let debug_mode = false
+let debug_mode = true
 
 (* -------------------------------------------------------------------- *)
 let shorten_path

src/phl/ecPhlPr.ml

@@ -53,12 +53,15 @@ let t_equiv_ppr_r ty phi_l phi_r tc =
   let funl = EcEnv.Fun.by_xpath fl env in
   let funr = EcEnv.Fun.by_xpath fr env in
   let (penvl,penvr), (qenvl,qenvr) = EcEnv.Fun.equivF_memenv ef.ef_ml ef.ef_mr fl fr env in
+  let m = EcIdent.create "&hr" in
   let argsl = map_ss_inv1 (to_args funl) (f_pvarg funl.f_sig.fs_arg (fst penvl)) in
   let argsr = map_ss_inv1 (to_args funr) (f_pvarg funr.f_sig.fs_arg (fst penvr)) in
   let a_id = EcIdent.create "a" in
   let a_f = f_local a_id ty in
-  let pr1 = f_pr (fst penvl) fl argsl.inv (map_ss_inv1 (fun p -> f_eq p a_f) phi_l) in
-  let pr2 = f_pr (fst penvr) fr argsr.inv (map_ss_inv1 (fun p -> f_eq p a_f) phi_r) in
+  let pr1_ev = EcSubst.ss_inv_rebind (map_ss_inv1 (fun p -> f_eq p a_f) phi_l) m in
+  let pr1 = f_pr (fst penvl) fl argsl.inv pr1_ev in
+  let pr2_ev = EcSubst.ss_inv_rebind (map_ss_inv1 (fun p -> f_eq p a_f) phi_r) m in
+  let pr2 = f_pr (fst penvr) fr argsr.inv pr2_ev in
   let concl_pr =
     f_forall_mems_ts_inv penvl penvr
       (map_ts_inv1 (f_forall_simpl [a_id,GTty ty])

theories/crypto/AdvAbsVal.ec

@@ -38,6 +38,6 @@ lemma abs_val (P:real -> bool):
 proof.
 move=> HP &m A Hl.
 case (Pr[A.main() @ &m : res] <= 1%r / 2%r)=> Hle.
-+ move: (HP &m (Neg_main(A))); rewrite (Neg_A_Pr_minus A &m); 1:auto; smt().
++ by move: (HP &m (Neg_main(A))); rewrite (Neg_A_Pr_minus A &m) //#.
 by move: (HP &m A)=> /#.
 qed.

theories/modules/EventPartitioning.ec

@@ -128,7 +128,10 @@ theory ResultPartitioning.
     = big predT (fun a=> Pr[M.f(i) @ &m: E i (glob M) res /\ res = a]) (undup (X i))
       + Pr[M.f(i) @ &m: E i (glob M) res /\ !mem (X i) res].
   proof.
-  rewrite -mem_undup.
+print mem_undup.
+  have->:Pr[M.f(i) @ &m : E i (glob M){hr} res{hr} /\ ! (res{hr} \in X i)]=
+         Pr[M.f(i) @ &m : E i (glob M){hr} res{hr} /\ ! (res{hr} \in undup (X i))].
+  - smt(mem_undup).
   exact/(@list_partitioning M i E (fun _ _ x=> x) (undup (X i)) &m)/undup_uniq.
   qed.
   end section.
@@ -255,7 +258,7 @@ abstract theory SubuniformReference.
   move=> a_in_X. rewrite (@is_subuniform arg{1} X a &1 support_M a_in_X).
   byphoare (_: (i,xs) = (i,xs){2} ==> _)=> //=; proc; rnd (pred1 a); auto=> />.
   rewrite dscalar1E 1:ltrW 1:gt0_k.
-  + by rewrite duniform_ll 1:xs_def 1:Xi_neq0 //= le1_k.
+  +rewrite duniform_ll 1:xs_def 1:Xi_neq0 //= le1_k.
   by rewrite duniform1E i_def xs_def a_in_X.
   qed.
   end section.