start removing our blessing from alt-ergo

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.

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: