make easycrypt independent from alt-ergo

This makes stdlib and examples go through without alt-ergo, and removes
that prover from the expected set of provers for EC CI.

This makes EasyCrypt more cleanly usable in commercial and non-free
contexts. Our docker images still contain alt-ergo versions, which are
available for proofs in external CI and individual proofs, upon a user's
(hopefully informed) choice.

Anyone wanting to transition their proofs away from alt-ergo should
expect proofs that use SMT to solve goals that require either
instantiation of existentials or case analysis on inductively-typed
values to fail after removing alt-ergo.

Author: fdupress

easycrypt.project

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

examples/ChaChaPoly/chacha_poly.ec

@@ -807,10 +807,13 @@ proof.
   rewrite (hrec (size (drop block_size p))) 2://; 1: smt(size_drop gt0_block_size).
   rewrite -{4}(cat_take_drop block_size p); congr.
   rewrite -!take_xor_map2_xor; apply (eq_from_nth Byte.zero).
-  + smt (size_map2 Block.bytes_of_blockP size_cat size_take gt0_block_size size_ge0).
+  + rewrite size_take 1:#smt:(gt0_block_size).
+    rewrite size_map2 size_cat size_map2 bytes_of_blockP.
+    by rewrite /min; smt(size_ge0).
   move=> j hj.
   have [hj1 hj2] : j < block_size /\ j < size p.
-  + smt (size_map2 Block.bytes_of_blockP size_cat size_take gt0_block_size size_ge0).
+  + move: hj; rewrite size_map2 size_cat size_map2 bytes_of_blockP /min.
+    smt(size_ge0).
   rewrite
     (nth_map2 Byte.zero Byte.zero)
     ?(size_cat, size_map2, Block.bytes_of_blockP) 1:#smt:(size_ge0).
@@ -878,7 +881,9 @@ proof.
   move=> _; rewrite /dblock; apply eq_distr => b.
   rewrite !dmap1E.
   apply (eq_trans _ (mu1 (dpoly `*` dextra_block) ((topair b).`1, (topair b).`2))); last first.
-  + congr; apply fun_ext; smt (topairK).
+  + congr; apply: fun_ext=> x @/(\o) @/pred1.
+    rewrite -{3}topairK; case: (topair b)=> />.
+    by move: (can_inj _ _ ofpairK)=> /#.
   rewrite dprod1E (_:block_size = poly_size + extra_block_size) //.
   rewrite dlist_add 1:ge0_poly_size 1:ge0_extra_block_size dmapE.
   rewrite !dmap1E /(\o) -dprodE &(mu_eq_support) => -[l1 l2] /supp_dprod /= [h1 h2].
@@ -946,7 +951,9 @@ proof.
   move=> _; rewrite /dpoly; apply eq_distr => b.
   rewrite !dmap1E.
   apply (eq_trans _ (mu1 (dpoly_in `*` dpoly_out) ((topair b).`1, (topair b).`2))); last first.
-  + congr; apply fun_ext; smt (topairK).
+  + congr; apply: fun_ext=> x @/(\o) @/pred1.
+    rewrite -{3}(topairK b); case: (topair b)=> />.
+    by move: (can_inj _ _ ofpairK)=> /#.
   rewrite dprod1E (_:poly_size = poly_in_size + poly_out_size) //.
   rewrite dlist_add 1:ge0_poly_in_size 1:ge0_poly_out_size dmapE.
   rewrite !dmap1E /(\o) -dprodE &(mu_eq_support) => -[l1 l2] /supp_dprod /= [h1 h2].
@@ -1752,31 +1759,18 @@ section PROOFS.
               let r = oget ROin.m{1}.[(n, C.ofintd 0)] in 
               let s = oget ROout.m{1}.[(n, C.ofintd 0)] in 
               s = t - poly1305_eval r (topol a c))); last first.
-    + auto => /> ; smt (undup_uniq size_undup size_map).
-
-    (* + auto => /> *; have [#] * :=H H0. *)
-    (*   rewrite H3/=. *)
-    (*   move:H4=> [][]->>[#] 3->> [#]*.  *)
-    (*   move:H6=> [#] ->> * /=. *)
-    (*   rewrite undup_uniq //=; do ! split=> //=. *)
-    (*   - smt (undup_uniq size_undup size_map). *)
-    (*   - smt (undup_uniq size_undup size_map). *)
-    (*   - smt (undup_uniq size_undup size_map). *)
-    (*   - move=> *. *)
-    (*     pose n1:= nth witness _ _. *)
-    (*     have* :=H5 _ _ H19. *)
-    (*     have:=H16 _ H21; rewrite H20 /= => -> //=.  *)
-    (*     rewrite/n1/=. *)
-    (*     pose l1:= List.map _ _. *)
-    (*     pose l := undup _. *)
-    (*     have:=mem_nth witness l j; rewrite H17 H18 /= =>*. *)
-    (*     move:H22; rewrite mem_undup mapP => [][] /= [] n2 y1 y2 y3 /= [] *. *)
-    (*     have:=H15 n1 x1 x2 x3. *)
-    (*     have:=H11 n1 x1 x2 x3. *)
-    (*     have := H19; rewrite -H8 => *.  *)
-    (*     have :=H13 n1 x1 x2 x3; rewrite H20 /= -H18/= get_some //= => -> //=. *)
-    (*     smt (undup_uniq size_undup size_map). *)
-
+    + auto=> /> &1 &2 + not_bad; rewrite not_bad=> />.
+      move=> inv_count inv_domRO inv_domSRO1 eq_domSRO2 inv_domSRO2.
+      move=> size_lenc inv_ndec inv_log inv_sc inv0 inv1 inv2 inv3 inv4.
+      do !split; [1..5:smt(undup_uniq size_undup size_map)].
+      move=> j ge0_j gtj_size lc_j x1 x2 x3.
+      pose n0 := nth _ _ _; case _: (UFCMA.log.[n0]{2})=> [/#|/> log_nth].
+      split=> [/#|]; case _: (SplitC2.I2.RO.m{1}.[n0, C.ofintd 0])=> [/#|].
+      case _: (RO.m{2}.[n0, C.ofintd 0])=> [/#|/>].
+      move: (inv2 n0 _); 1:by rewrite domE log_nth.
+      rewrite log_nth=> /> _ _ x0 m2_n0 x4 i2_n0.
+      move: (inv4 n0 _); 1:exact: (inv_domSRO1 _ (C.ofintd 0)).
+      by rewrite log_nth i2_n0 m2_n0.
     inline{1} 2; rcondt{1} 3. 
     + by move=> *;auto => />;rewrite /test /= C.ofintdK; smt (C.gt0_max_counter).
     inline{1} 3; inline{1} 4; sp 0 1; wp.
@@ -2086,12 +2080,13 @@ section PROOFS.
     - have:=allP (fun (n0 : nonce) => (n0, C.ofintd 0) \notin ROout.m{2}) l2.
       have-> /= -> //=:=filter_all (fun (n0 : nonce) => (n0, C.ofintd 0) \notin SplitC2.I2.RO.m{2}) l.
       by rewrite mem_nth //=.
-  rewrite (drop_nth witness i{2} l2) //= drop0 //=; do ! split=> /> *.
+  rewrite (drop_nth witness i{2} l2) //= drop0 //=; do ! split=> />.
   + smt().
   + smt(mem_set).
-  + rewrite get_set_neqE /=; smt(mem_nth).
-  + smt(mem_set).
+  + move=> *; rewrite get_set_neqE /=; smt(mem_nth).
   + smt(mem_set).
+  + move=> n0; rewrite mem_set; case=> [/#|/>].
+    by right; exists i{2}=> /#.
   + smt(mem_set size_drop size_ge0 size_eq0).
   + smt(mem_set size_drop size_ge0 size_eq0).
   qed.
@@ -2479,8 +2474,8 @@ section PROOFS.
   call(: ={glob BNR, UFCMA.cbad1, UFCMA.cbad1, glob RO, Mem.log, Mem.lc} /\ 
     inv_lbad1 UFCMA_l.lbad1{2} BNR.lenc{2} UFCMA.log{2} Mem.log{2} Mem.lc{2} UFCMA.cbad1{2} BNR.ndec{2} /\
     (UFCMA.bad1{1} => exists (tt : tag * tag), (tt \in UFCMA_l.lbad1{2}) /\ tt.`1 = tt.`2)); first last.
-  + by proc; inline*; sp 1 1; if; auto; smt(in_cons make_lbad1_size_cons2 leq_make_lbad1). 
-  + by skip; smt( mem_empty ge0_qenc ge0_qdec). 
+  + proc; inline*; sp 1 1; if; auto => &1 &2 /> ?????????????; smt(in_cons make_lbad1_size_cons2 leq_make_lbad1).
+  + skip => &1 &2 />; rewrite ge0_qenc size_flatten /sumz /= ge0_qdec /=; smt(mem_empty).
   proc; sp; if; 1, 3: auto=> />.
   sp; wp=> /=.
   case: (UFCMA.cbad1{1} < qenc); last first.
@@ -2492,8 +2487,19 @@ section PROOFS.
     wp -7 -7=> />.
     move => />; smt (get_setE).
     conseq (: ={c1, t, RO.m, Mem.log}); [2:sim=> /> /#].
-    move => />.
-    smt(get_setE leq_make_lbad1 make_lbad1_size_cons3 size_ge0).
+    move => &1 &2 /> 9? X ?????? c1_R t_R.
+    do! split.
+    - smt().
+    - rewrite (make_lbad1_size_cons3) //; smt(leq_make_lbad1 size_ge0).
+    - smt(leq_make_lbad1).
+    - move => n D ad msg tag; rewrite get_setE.
+      case: D => />.
+      + by rewrite /dom get_setE.
+      smt(get_setE).
+    - move => n; rewrite /dom get_setE /#.
+    move => t t' tt'; case: (X _ _ tt') => /> n hn ht ad msg ht'.
+    case: (n = n{!2}); first smt().
+    move => _; exists n; rewrite get_setE /#.
   inline*; sp.
   rcondt{1} 5; 1: auto=> />.
   - conseq(:_==> true)=> />; 1: smt(size_map size_filter count_size).
@@ -2509,8 +2515,10 @@ section PROOFS.
   - smt().  
   - rewrite size_cat !size_map make_lbad1_size_cons3 //= /#.
   - smt(leq_make_lbad1).
-  - smt(get_setE).
-  - smt(get_setE).
+  - move => n D ad msg tag; rewrite get_setE; case: D => />; first by rewrite /dom get_setE.
+    smt(get_setE).
+  - move => n; case: (n = n{!2}) => />; first by rewrite /dom get_setE.
+    smt(get_setE).
   - move=> ? ? H15; have:=H15; rewrite mem_cat=> [#][] H16 *.
     + smt(get_setE).
     have:= H16; rewrite mapP /= => [#][] t2 [#] h <<- <<-; have:=h.
@@ -2643,7 +2651,12 @@ section PROOFS.
       inv_lbad1_i UFCMA_l.lbad1{1} BNR.lenc{1} UFCMA.log{1} Mem.log{1} Mem.lc{1} UFCMA.cbad1{1} BNR.ndec{1} /\
       (((nth (w1,w2) UFCMA_l.lbad1{1} nth0).`1 =
         (nth (w1,w2) UFCMA_l.lbad1{1} nth0).`2) => UFCMA_li.badi{2})); first last.
-  + proc; sp; if; auto; inline*; auto; smt(make_lbad1_size_cons2 size_ge0 leq_make_lbad1).
+  + proc; sp; if; auto; inline*; auto => &1 &2 /> *; do !split.
+    - case: (c{2} \in Mem.log{2}); first smt().
+      rewrite make_lbad1_size_cons2 // /#.
+    - smt(leq_make_lbad1).
+    - smt().
+    - smt().
   + by auto; smt(neq_w1_w2 size_ge0 ge0_qdec size_flatten ge0_qenc).
   + proc; inline*; sp; if; 1, 3: auto; sp.
     swap [5..6] 7.
@@ -2732,8 +2745,8 @@ section PROOFS.
   proof.
   apply (RealOrder.ler_trans _ _ _ (step4_bad1_lbad1 &m)).
   apply (RealOrder.ler_trans _ _ _ (step4_lbad1_sum &m)).
-  apply (RealOrder.ler_trans _ _ _ (StdBigop.Bigreal.ler_sum_seq _ _ (fun _ => pr1_poly_out) _ _)); 
-    last by rewrite sumr_const count_predT size_iota; smt(ge0_qdec).
+  apply (RealOrder.ler_trans _ _ _ (StdBigop.Bigreal.ler_sum_seq _ _ (fun _ => pr1_poly_out) _ _));
+    last by rewrite sumr_const count_predT size_iota ler_maxr // ge0_qdec.
   move=> nth0; rewrite mem_iota /predT /= => [#] *.
   apply (RealOrder.ler_trans _ _ _ (step4_badi &m nth0 _))=> //.
   exact (pr_step4_badi &m).

examples/MEE-CBC/RCPA_CMA.ec

@@ -336,7 +336,7 @@ theory EtM.
     type leaks           <- leaks,
     op   leak            <- leak,
     op   dC    (l:leaks) <- (dC l) `*` (MUnit.dunit witness<:tag>)
-  proof * by smt.
+  proof * by smt(dprod_ll dC_ll dunit_ll).
 
   (** The black-box construction is as follows **)
   module EtM(E:SKEa.Enc_Scheme, M:MACa.MAC_Scheme): Enc_Scheme = {

examples/PIR.ec

@@ -22,7 +22,13 @@ proof. by exists [] s. qed.
 
 lemma sxor2_cons (s s':int list) (i j:int):
   sxor2 s s' i => sxor2 (j::s) (j::s') i.
-proof. smt (). qed.
+proof.
+move=> [].
+  move=> [] s1 s2 [] -> ->.
+  by left; exists (j :: s1) s2.
++ move=> [] s1 s2 [] -> ->.
+  by right; exists (j :: s1) s2.
+qed.
 
 (* The database *)
 op a : int -> word.
@@ -72,7 +78,7 @@ proof.
     while (j <= N /\ if j <= i then PIR.s = PIR.s' else sxor2 PIR.s PIR.s' i).
     + wp;rnd;skip => /= &m [[_]] + HjN.
       have -> /= : j{m} + 1 <= N by smt ().
-      case: (j{m} <= i{m}) => Hji;2: by smt ().
+      case: (j{m} <= i{m})=> Hji; 2:smt(sxor2_cons).
       move=> -> b _;case: (j{m} = i{m}) => [->> | /#].
       by rewrite (_ : !(i{m}+1 <= i{m})) 1:/# /=; smt (sxor_cons).
     by auto => /#.

examples/ehoare/qselect/partition.eca

@@ -100,9 +100,13 @@ lemma index_count x l: sorted (<=) l => uniq l => x \in l => index x l = count (
 proof.
   elim: l => // y l hrec /> hp hnin hu.
   case: (x = y) => [<<- _ | hne /= hin] /=.
-  + by rewrite index_cons /= count_pred0_eq_in //=; smt (order_path_min allP le_trans lt_nle).
+  + rewrite index_cons /= count_pred0_eq_in //=; 2:smt(lt_nle).
+    move=> x0 x0_in_l; move: (order_path_min (<=) le_trans x l hp).
+    by rewrite allP=> /(_ _ x0_in_l); rewrite lt_nle.
   rewrite index_cons hne /= hrec //; 1: by apply: path_sorted hp.
-  smt (order_path_min allP le_trans).
+  suff -> : y < x by smt().
+  have /allP := order_path_min _ le_trans _ _ hp.
+  move => /(_ _ hin) /#.
 qed.
 
 lemma sindex_countP (t: elem array) (lo hi p : int) : 

examples/hashed_elgamal_std.ec

@@ -192,7 +192,7 @@ section Security.
             - Pr[ES1(ESAdv(A)).main() @ &m : res]|.
   proof.
   rewrite (cpa_ddh0 &m) (ddh1_es1 &m) (es0_Gb &m) (Gb_half &m).
-  smt(@Real).
+  smt(StdOrder.RealOrder.ler_dist_add).
   qed.
 end section Security.
 

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 :
@@ -53,17 +55,21 @@ lemma flubZ (f: 'a -> real) c : has_fub f =>
   c >= 0%r => flub (fun x => c * f x) = c * flub f.
 proof.
 move => fub_f c_ge0 @/flub; pose E := fun r => exists a, f a = r.
-have -> : (fun r => exists a, c * f a = r) = scale_rset E c by smt().
+have -> : (fun r => exists a, c * f a = r) = scale_rset E c.
++ apply: fun_ext=> x; rewrite eq_iff; split.
+  + by move=> [] a xP; exists (f a); rewrite xP=> //=; exists a.
+  + by move=> /> a; exists a.
 by rewrite lub_scale //; apply has_fub_lub.
 qed.
 
 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/RealFun.ec

@@ -35,7 +35,7 @@ proof. smt (). qed.
 
 lemma convexD f1 f2 a b:
   convex f1 a b => convex f2 a b => convex (fun x => f1 x + f2 x) a b.
-proof. smt (). qed.
+proof. by move=> + + x x_in01; smt(). qed.
 
 lemma convexZ c f a b: 0%r <= c =>
   convex f a b => convex (fun x => c * f x) a b.

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.
 
 (* -------------------------------------------------------------------- *)