start removing our blessing from alt-ergo

Author: fdupress

easycrypt.project

@@ -1,4 +1,3 @@
 [general]
-provers = [email protected]
 provers = [email protected]
 provers = [email protected]

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,7 +100,9 @@ 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).
 qed.

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

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.