start removing our blessing from alt-ergo

Author: fdupress

easycrypt.project

@@ -1,4 +1,3 @@
 [general]
-provers = Alt-Ergo@2.4
 provers = CVC5@1.0
 provers = Z3@4.12

theories/algebra/DynMatrix.eca

@@ -73,7 +73,8 @@ lemma offunvK pv: tofunv (offunv pv) = vclamp pv.
 proof. by rewrite /tofunv /offunv eqv_repr vclamp_idemp. qed.
 
 lemma vectorW (P : vector -> bool): 
-  (forall pv, P (offunv pv)) => forall v, P v by smt(tofunvK).
+  (forall pv, P (offunv pv)) => forall v, P v.
+proof. by move=> P_pv v; rewrite -tofunvK; apply: P_pv. qed.
 
 (* Dimension of the vector *)
 op size v = (tofunv v).`2.
@@ -593,8 +594,10 @@ qed.
 lemma dvector1E (d : R distr) (v : vector) : mu1 (dvector d (size v)) v =
   BRM.bigi predT (fun i => mu1 d v.[i]) 0 (size v).
 proof.
-rewrite -{2}[v]tolistK dmapE /(\o) /pred1. 
-rewrite (@mu_eq _ _ (pred1 (tolist v))); 1: smt(oflist_inj).
+rewrite -{2}[v]tolistK dmapE /(\o) /pred1.
+rewrite (@mu_eq _ _ (pred1 (tolist v))).
++ move=> x; rewrite eq_iff /pred1 /=; split=> />.
+  exact: oflist_inj.
 rewrite dlist1E 1:/# size_tolist max0size /=.
 by rewrite BRM.big_mapT /(\o) &BRM.eq_big.
 qed.
@@ -694,7 +697,8 @@ proof. by rewrite /tofunm /offunm eqv_repr. qed.
 hint simplify offunmK.
 
 lemma matrixW (P : matrix -> bool) : (forall pm, P (offunm pm)) =>
-  forall m, P m by smt(tofunmK).
+  forall m, P m.
+proof. by move=> P_pm m; rewrite -tofunmK; exact: P_pm. qed.
 
 (* Number of rows and columns of matrices *)
 op rows m = (tofunm m).`2.
@@ -1451,16 +1455,17 @@ qed.
 lemma catmrA (m1 m2 m3: matrix): ((m1 || m2) || m3) = (m1 || (m2 || m3)).
 proof. 
 rewrite eq_matrixP. 
-split => [| i j bound]; 1: smt(size_catmr).
+split => [| i j bound]; 1:smt(size_catmr rows_catmr cols_catmr).
 rewrite 4!get_catmr cols_catmr // addrA. 
-algebra.
+by algebra.
 qed.
 
 lemma catmrDr (m1 m2 m3: matrix): m1 * (m2 || m3) = ((m1 * m2) || (m1 * m3)).
 proof.
 rewrite eq_matrixP.
 rewrite rows_mulmx cols_mulmx cols_catmr.
-split => [| i j bound]; 1: smt(size_mulmx size_catmr).
+split => [| i j bound].
++ by rewrite !size_catmr !rows_mulmx !cols_mulmx /#.
 rewrite get_catmr 3!get_mulmx. 
 case (j < cols m2) => bound2.
 - rewrite [col m3 _]col0E 1:/# dotpv0 addr0 !dotpE 2!size_col rows_catmr.
@@ -1667,7 +1672,9 @@ case (j < n) => j_bound.
   + smt(size_catmr size_subm).
   by rewrite addr0.
 - rewrite getm0E; 1: smt(size_catmr size_subm).
-  rewrite add0r get_subm; smt(size_catmr size_subm).
+  rewrite add0r get_subm; [3:smt()].
+  + smt(rows_catmr rows_subm).
+  + smt(cols_catmr cols_subm).
 qed.
 
 lemma subm_colmx (m: matrix) l : 
@@ -1908,7 +1915,8 @@ move => r_ge0 c_ge0; split => [m_supp|]; last first.
 - case => -[r_m c_m] m_d; rewrite /support -r_m -c_m dmatrix1E.
   apply prodr_gt0_seq => i i_row _ /=.
   by apply prodr_gt0_seq => j j_col _ /=; apply m_d; smt(mem_iota).
-have [r_m c_m] : size m = (r,c) by smt(size_dmatrix). 
+have [r_m c_m] : size m = (r,c).
++ exact: (size_dmatrix d).
 split => [//|i j range_ij]; move: m_supp. 
 rewrite -r_m -c_m /support dmatrix1E => gt0_big.
 pose G i0 := (fun (j0 : int) => mu1 d m.[i0, j0]).

theories/analysis/RealFLub.ec

@@ -25,8 +25,10 @@ by smt().
 lemma flub_upper_bound (F : 'a -> real) x : 
     has_fub F => F x <= flub F.
 proof.
-move => H. apply lub_upper_bound; 2: by exists x.
-by split; [ by exists (F x) x | smt() ].
+move => H; apply lub_upper_bound; 2: by exists x.
+split.
++ by exists (F x) x.
+by case: H=> r is_fub_F_r; exists r=> /#.
 qed.
 
 lemma flub_le_ub (F : 'a -> real) r :
@@ -61,9 +63,10 @@ lemma flub_const c :
   flub (fun _ : 'a => c) = c.
 proof.
 apply eqr_le; split; first apply flub_le_ub => /#.
-move => _; apply (@flub_upper_bound (fun _ => c) witness) => /#.
+move=> _; apply (@flub_upper_bound (fun _=> c) witness).
+by exists c=> /#.
 qed.
 
 lemma has_fubZ (f: 'a -> real) c: has_fub f =>
   c >= 0%r => has_fub (fun x => c * f x).
-proof. move => [ym ub_ym] ge0_c; exists (c * ym) => /#. qed.
+proof. by move => [ym ub_ym] ge0_c; exists (c * ym) => /#. qed.

theories/analysis/RealLub.ec

@@ -81,8 +81,11 @@ qed.
 (* -------------------------------------------------------------------- *)
 lemma lub1 x : lub (pred1 x) = x.
 proof.
-apply eqr_le; split; [apply lub_le_ub => /#|move => _].
-apply lub_upper_bound; smt().
+have haslub_1x: (has_lub (pred1 x)).
++ by rewrite /has_lub; split; exists x=> /#.
+apply: eqr_le; split.
++ by apply: lub_le_ub=> //#.
+by move=> _; apply: lub_upper_bound.
 qed.
 
 (* -------------------------------------------------------------------- *)
@@ -102,7 +105,8 @@ qed.
 lemma has_lub_scale E c : 0%r <= c =>
   has_lub E => has_lub (scale_rset E c).
 proof.
-move => c_ge0 [[x Ex] ?]; split; 1: smt().
+move=> c_ge0 [[x Ex] ?]; split.
++ by exists (c * x) x.
 exists (c * lub E) => cx; smt(lub_upper_bound).
 qed.
 
@@ -115,7 +119,9 @@ apply eqr_le; split => [|_].
 - apply lub_le_ub; first by apply has_lub_scale.
   smt(lub_upper_bound).
 rewrite -ler_pdivl_mull //; apply lub_le_ub => // x Ex.
-by rewrite ler_pdivl_mull //; smt(lub_upper_bound has_lub_scale). 
+rewrite ler_pdivl_mull //; apply: lub_upper_bound.
++ exact: has_lub_scale.
+by exists x.
 qed.
 
 (* -------------------------------------------------------------------- *)

theories/analysis/RealSeries.ec

@@ -965,7 +965,8 @@ lemma summable_inj (h : 'a -> 'b) (s : 'b -> real) :
   injective h => summable s => summable (s \o h).
 proof.
 move => inj_h [M] sum_s; exists M => J uniq_J. 
-have R := sum_s (map h J) _; 1: rewrite map_inj_in_uniq /#.
+have R := sum_s (map h J) _.
++ by rewrite map_inj_in_uniq=> // x y _ _ /inj_h.
 apply (ler_trans _ _ R) => {R}; rewrite big_map /(\o)/= big_mkcond.
 exact Bigreal.ler_sum.
 qed.

theories/crypto/PROM.ec

@@ -287,12 +287,22 @@ fel 1 (fsize RO.m) (fun x => x%r * Pc) q (fcoll f RO.m)
 - inline*; auto; smt(fsize_empty mem_empty).
 - proc; inline*; (rcondt 2; first by auto); wp.
   rnd (fun r => exists u, u \in RO.m /\ f (oget RO.m.[u]) = f r).
-  skip => &hr; rewrite andaE => /> 3? I ?; split; 2: smt(get_setE).
-  apply mu_mem_le_fsize => u /I /(dmap_supp _ f) /fcollP /= /(_ x{hr}).
-  rewrite dmap1E. apply: StdOrder.RealOrder.ler_trans.
-  by apply mu_sub => /#.
+  auto=> /> &0 ge0_size_m ltq_size_m nocoll I x_notin_m; split=> [|_].
+  + apply mu_mem_le_fsize => u /I /(dmap_supp _ f) /fcollP /= /(_ x{0}).
+    rewrite dmap1E; apply: StdOrder.RealOrder.ler_trans.
+    by apply: mu_sub=> @/pred1 @/(\o) /> x ->.
+  move=> v _ i j; rewrite !mem_set.
+  move=> i_in_mVx j_in_mVx i_neq_j; rewrite !get_setE.
+  case: (i = x{0}); case: (j = x{0})=> />.
+  + by move=> _ coll_v; exists j=> /#.
+  + by move=> _ coll_v; exists i=> /#.
+  move=> j_neq_x i_neq_x eq_f.
+  move: nocoll=> /negb_exists /= /(_ i) /negb_exists /= /(_ j).
+  rewrite i_neq_j eq_f.
+  move: i_in_mVx; rewrite i_neq_x=> /= -> /=.
+  by move: j_in_mVx; rewrite j_neq_x=> /= -> /=.
 - move => c; proc; auto => />; smt(get_setE fsize_set).
-- move => b c. proc. by auto.
+- move => b c; proc; by auto.
 qed.
 
 end section Collision.

theories/crypto/PRP.eca

@@ -279,15 +279,15 @@ lemma collision_add (m:(D,D) fmap) x y:
   collision m.[x <- y] <=> collision m \/ rng m y.
 proof.
 move=> x_notin_m; split=> [[z z' [z'_neq_z]]|].
-+ rewrite mem_set=> -[z_in_m] [z'_in_m] mz_eq_mz'.
++ rewrite !mem_set !get_setE=> -[z_in_m] [z'_in_m] mz_eq_mz'.
   case (rng m y)=> //= y_notin_rngm.
-  by exists z z'; smt(@SmtMap).
+  by exists z z'; smt().
 move=> [[z z' [z'_neq_z] [z_in_m] [z'_in_m] mz_eq_mz']|].
 + exists z z'; rewrite z'_neq_z !mem_set !get_setE mz_eq_mz' z_in_m z'_in_m /=.
   move/contra: (congr1 (dom m) z x); rewrite x_notin_m z_in_m=> -> //=.
   by move/contra: (congr1 (dom m) z' x); rewrite x_notin_m z'_in_m=> -> //=.
 rewrite rngE=> - /= [x'] mx'_y.
-by exists x x'; smt(@SmtMap).
+by exists x x'; rewrite !get_setE !mem_set /#.
 qed.
 
 lemma collision_stable (m:(D,D) fmap) y y':
@@ -459,7 +459,8 @@ section Upto.
                 PRFi.m{2} = RP.m.[x <- r0]{1} /\
                 ((PRP_indirect_bad.bad \/ rng RP.m r0){1} <=> collision PRFi.m{2})).
     + auto => /> &1 &2 coll _ x_notin_m r _; split=> [|x0 x'].
-      + rewrite rngE /= /collision=> - [x'] mx'; exists x{2} x'; smt(domE get_setE).
+      + rewrite rngE /= /collision=> - [x'] mx'.
+        by exists x{2} x'; rewrite !mem_set !get_setE /#.
       smt (rngE get_setE).
     sp; if{1}.
     + conseq (_: _ ==> collision PRFi.m{2} /\ PRP_indirect_bad.bad{1})=> //.
@@ -472,7 +473,9 @@ section Upto.
          [auto|if=> //=; auto|hoare; auto]=> />;rewrite ?dD_ll //.
     by move=> &hr x_notin_m r_in_rng_m; apply excepted_lossless; exists x{hr}.
     move=> &1; conseq (_: collision PRFi.m ==> collision PRFi.m: =1%r)=> //=.
-    by proc; if; auto=> />; rewrite dD_ll //=; smt(domE get_setE).
+    proc; if; auto=> />; rewrite dD_ll //=.
+    move=> &0 x x' x'_neq_x x_in_m x'_in_m x_coll_x' x0_notin_m v _ _.
+    by exists x x'=> />; rewrite !mem_set x_in_m x'_in_m /= !get_set_neqE 1,2:/#.
   inline *; auto=> />; split=> [|_].
   + by rewrite no_collision=> x x'; rewrite mem_empty.
   move=> /> rL rR DL b mL DR mR [-> //| /#].
@@ -583,15 +586,24 @@ section CollisionProbability.
   proc; inline*; wp.
   call (_: ={PRFi.m} /\
            size Sample.l{1} = card (fdom PRFi.m){2} /\
-           (forall x, mem (frng PRFi.m) x <=> mem Sample.l x){1} /\
+           (forall x, rng PRFi.m x <=> mem Sample.l x){1} /\
            (collision PRFi.m{2} <=> !uniq Sample.l{1})).
   + proc; inline*.
     if => //=.
     auto => /> &1 &2 h1 h2 h3 h4 r _.
-    rewrite fdom_set fcardUI_indep 2:fcard1; 1: by rewrite fsetI1 mem_fdom h4.
-    split; 1:smt(). 
-    split; smt(get_setE mem_frng rngE collision_add).    
-  auto; smt (size_eq0 fdom0 fcards0 frng0 in_fset0 mem_empty).
+    rewrite fdom_set fcardUI_indep 2:fcard1; 1:by rewrite fsetI1 mem_fdom h4.
+    split; 1:smt().
+    split.
+    + move=> v; rewrite -h2 !rngE /=; split.
+      + move=> [] x0; rewrite get_setE; case: (x0 = x{2})=> /> _ m_x0.
+        by right; exists x0.
+      + case=> />.
+        + by exists x{2}; rewrite get_set_sameE.
+        + move=> x0 m_x0; exists x0; rewrite get_set_neqE //.
+          rewrite domE in h4; rewrite -negP=> <<-.
+          by move: h4; rewrite m_x0.
+    + smt(collision_add).
+  by auto; smt (size_eq0 fdom0 fcards0 frng0 in_fset0 mem_empty).
   qed.
 
   local hoare IND_bounded : IND(PRFi,D).main : true ==> card (fdom PRFi.m) <= q.

theories/crypto/SplitRO.ec

@@ -162,7 +162,12 @@ section PROOFS.
         by rewrite /pred1 /(\o) (can_eq _ _ ofpairK).
       move=> _ t; rewrite sample_spec supp_dmap => -[[t1 t2] []] + ->>.
       by rewrite topairK ofpairK => ->.
-    by auto => />; smt (get_setE map_set set_pair_map mem_map mem_pair_map mem_set mapE mergeE).
+    auto=> /> &2 eq_dom; move: (eq_dom x{2}); rewrite !eq_iff.
+    rewrite !mem_map !mem_pair_map !mapE !mergeE 1:/o_pair //.
+    case _: (x{2} \in I1.RO.m{2})=> />.
+    + by rewrite !domE; case: (I1.RO.m.[x]{2})=> />; case: (I2.RO.m.[x]{2}).
+    rewrite !get_set_sameE /= -(map_set (fun _=> ofpair)) set_pair_map /=.
+    by move=> + + x0; rewrite mem_map mem_pair_map !mem_set /#.
   qed.
 
   equiv RO_split: 

theories/crypto/prp_prf/Strong_RP_RF.eca

@@ -145,7 +145,9 @@ proc; seq  1: (exists x, support uD x /\ !X x)=> //=.
 if=> //=.
 + rnd (predT); skip.
   move=> /> &0; rewrite dexceptedE predTI mu_not.
-  smt(notin_supportIP).
+  move=> x x_in_uD x_notin_X r_in_X.
+  apply/mulrV/ltr0_neq0/subr_gt0/notin_supportIP.
+  by exists x.
 by hoare; rnd=> //=; skip=> &hr ->.
 qed.
 
@@ -473,7 +475,9 @@ section CollisionProbability.
         + by apply/fun_ext=> x; rewrite mem_frng.
         apply/mu_mem_le; move=> x _; have [] uD_suf [] _ uD_fu:= uD_uf_fu.
         apply/RealOrder.lerr_eq/uD_suf; 1,2:rewrite uD_fu //.
-        smt(RealOrder.ler_wpmul2r mu_bounded le_fromint ltrW leq_card_rng_dom).
+        apply: RealOrder.ler_wpmul2r.
+        + exact: ge0_mu.
+        + exact/le_fromint/(lez_trans _ _ _ (leq_card_rng_dom _)).
       - by move: H9; rewrite H1.
     * by hoare; auto; smt(RealOrder.mulr_ge0 mu_bounded ge0_q).
   + move=> c; proc; rcondt 2; 1:by auto.

theories/datatypes/List.ec

@@ -1611,7 +1611,15 @@ qed.
 
 lemma index_uniq z0 i (s : 'a list):
   0 <= i < size s => uniq s => index (nth z0 s i) s = i.
-proof. by elim: s i=> //=; smt(mem_nth). qed.
+proof.
+elim: s i=> //= [/#|x s ih i [] ge0_i].
+rewrite addzC=> /ltzS /lez_eqVlt le_i_sizeS.
+move=> [] x_notin_s uniq_s.
+case: (i = 0)=> /> i_neq_0.
+rewrite index_cons; case: (nth z0 s (i - 1) = x)=> [/>|_].
++ by move: x_notin_s; apply: contraLR=> _ /=; apply: mem_nth=> /#.
+by rewrite ih // /#.
+qed.
 
 lemma nth_uniq (s : 'a list) :
   (forall (i j : int), 0 <= i < size s => 0 <= j < size s => i <> j =>
@@ -1677,7 +1685,9 @@ qed.
 lemma uniq_le_perm_eq (s1 s2 : 'a list) :
   uniq s1 => mem s1 <= mem s2 => size s2 <= size s1 => perm_eq s1 s2.
 proof.
-  elim: s1 s2 => [| x l ih s2 /= [ninl uql] lemem le1sz]; 1: smt(size_ge0).
+  elim: s1 s2 => [| x l ih s2 /= [ninl uql] lemem le1sz].
+  + move=> s _ _ /= le0_size_s.
+    have -> //: s = [] by smt(size_ge0).
   move: (ih (rem x s2) uql _ _); 1,2: smt(mem_rem_neq size_rem).
   rewrite -(perm_cons x) => pxc; rewrite (perm_eq_trans _ _ _ pxc).
   by rewrite perm_eq_sym perm_to_rem /#.
@@ -2089,7 +2099,14 @@ proof. exact: nth_mapi_rec. qed.
 lemma mapi_recP x0 (f : int -> 'a -> 'b) (s : 'a list) y m :
     y \in mapi_rec f s m <=>
     exists n, (0 <= n && n < size s) /\ y = f (n+m) (nth x0 s n).
-proof. elim: s m; smt(size_ge0). qed.
+proof.
+elim: s m; 1:smt(size_ge0).
+move=> x xs ih m /=; case: (y = f m x)=> [/>|/= y_neq_fmx].
++ by exists 0; smt(size_ge0).
+rewrite ih; split.
++ by move=> [] n hn; exists (n + 1)=> /#.
++ by move=> [] n hn; exists (n - 1)=> /#.
+qed.
 
 lemma mapiP x0 (f : int -> 'a -> 'b) (s : 'a list) y :
     y \in mapi f s <=>
@@ -3778,13 +3795,23 @@ end section ListMax.
 lemma maxr_seq (f : 'a -> real) (s : 'a list) x0 :
   x0 \in s => exists x, x \in s /\ forall y, y \in s => f y <= f x.
 proof.
-by case: s => // x s _; elim: s x => {x0} [|y s IHs] x; smt().
+case: s => // x s _; elim: s x => {x0} [|y s IHs] x.
++ by exists x.
+case: (forall z, z = y \/ z \in s => f z <= f x).
++ by move=> z_is_min; exists x=> /#.
+move: (IHs y)=> - [] x1 /= hx1 x_not_max.
+by exists x1=> /#.
 qed.
 
 lemma maxz_seq (f : 'a -> int) (s : 'a list) x0 :
   x0 \in s => exists x, x \in s /\ forall y, y \in s => f y <= f x.
 proof.
-by case: s => // x s _; elim: s x => {x0} [|y s IHs] x; smt().
+case: s => // x s _; elim: s x => {x0} [|y s IHs] x.
++ by exists x.
+case: (forall z, z = y \/ z \in s => f z <= f x).
++ by move=> z_is_min; exists x=> /#.
+move: (IHs y)=> - [] x1 /= hx1 x_not_max.
+by exists x1=> /#.
 qed.
 
 (* -------------------------------------------------------------------- *)