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/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,7 +1759,30 @@ 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).
+    (** TODO DUPRESSOIR: CLEAN THIS UP **)
+    + auto=> /> &1 &2 + not_bad; rewrite not_bad=> />.
+      move=> inv_count inv_domRO inv_domSRO1 eq_domSRO2 inv_domSRO2 size_lenc inv_ndec inv_log inv_sc inv0 inv1 inv2 inv3 inv4.
+      split; 1:smt(undup_uniq).
+      split=> [/#|].
+      split; 1:smt(size_undup size_map).
+      split=> [/#|].
+      split=> [/#|].
+      move=> j ge0_j gtj_size lc_j x1 x2 x3.
+      pose n0 := nth witness (undup (map (fun (p : ciphertext)=> p.`1) Mem.lc{2})) j.
+      case _: (UFCMA.log.[n0]{2}).
+      + smt().
+      move=> /> log_nth.
+      split=> [/#|].
+      case _: (SplitC2.I2.RO.m{1}.[n0, C.ofintd 0]).
+      + smt().
+      case _: (RO.m{2}.[n0, C.ofintd 0]).
+      + smt().
+      move=> />.
+      move: (inv2 n0 _); 1:smt().
+      rewrite log_nth=> /> _ _ x0 m2_n0 x4 i2_n0.
+      move: (inv4 n0 _).
+      + exact: (inv_domSRO1 _ (C.ofintd 0)).
+      by rewrite log_nth i2_n0 m2_n0.
 
     (* + auto => /> *; have [#] * :=H H0. *)
     (*   rewrite H3/=. *)
@@ -2086,12 +2116,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.

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.