[chore] stabilise SMT and bump provers

Makefile

@@ -3,14 +3,12 @@
 # --------------------------------------------------------------------
 DUNE      ?= dune
 ECARGS    ?=
-ECTOUT    ?= 10
 ECJOBS    ?= 0
 ECEXTRA   ?= --report=report.log
 CHECKPY   ?=
 CHECK     := $(CHECKPY) scripts/testing/runtest
 CHECK     += --bin=./ec.native
 CHECK     += --jobs="$(ECJOBS)"
-CHECK     += --bin-args=-timeout --bin-args="$(ECTOUT)"
 CHECK     += $(foreach arg,$(ECARGS),--bin-args="$(arg)")
 CHECK     += $(ECEXTRA) config/tests.config
 NIX       ?= nix --extra-experimental-features "nix-command flakes"

easycrypt.project

@@ -1,3 +1,5 @@
 [general]
-provers = CVC5@1.0
-provers = Z3@4.12
+provers = CVC5@1.1
+provers = Z3@4.16
+
+timeout = 1

examples/cramer-shoup/cramer_shoup.ec

@@ -868,8 +868,10 @@ section Security_Aux.
     (forall (x : 'a), mu1 dt x <= r) => mu dt (mem l) <= n%r * r.
   proof.
     move=> Hsize Hmu1;apply (ler_trans ((size l)%r * r)).
-    + by apply mu_mem_le_mu1.
-    apply ler_wpmul2r; 1: smt (mu_bounded).
+    + by apply: mu_mem_le_mu1.
+    apply: ler_wpmul2r.
+    + apply: (ler_trans (mu1 dt witness)); 1:exact: ge0_mu.
+      exact: Hmu1.
     by apply le_fromint.
   qed.
 

examples/ehoare/adversary.ec

@@ -14,7 +14,11 @@ axiom dr_mu_test : 0%r < p.
 op eps : real.
 axiom dr_mu1 : forall (x:r), mu1 dr x <= eps.
 
-lemma eps_ge0: 0%r <= eps. by smt(dr_mu1 mu_bounded). qed.
+lemma eps_ge0: 0%r <= eps.
+apply: (ler_trans (mu1 dr witness)).
++ exact: ge0_mu.
+exact: dr_mu1.
+qed.
 
 module type Oracle = { 
   proc o () : unit 

theories/algebra/Bigalg.ec

@@ -324,7 +324,7 @@ elim: s => // x s IHs F_ge0; rewrite BMul.big_cons.
 have {IHs} IHs := IHs _; first by smt().
 case: (P x) => [Px F_big_gt0 a a_x_s Pa| nPx /IHs]; 2:smt().
 rewrite pmulr_gt0 in F_big_gt0; 1, 3:smt().
-apply: prodr_ge0_seq; smt().
+by apply: prodr_ge0_seq; smt().
 qed.
 
 lemma ler_prod_seq (P : 'a -> bool) (F1 F2 : 'a -> t) s:

theories/algebra/DynMatrix.eca

@@ -1939,7 +1939,11 @@ qed.
 lemma supp_dmatrix_full m d r c : 
   0 <= r => 0 <= c =>
   is_full d => m \in dmatrix d r c <=> size m = (r,c).
-proof. smt(supp_dmatrix). qed.
+proof.
+move=> ge0_r ge0_c d_fu.
+rewrite supp_dmatrix //; split=> //.
+by move=> -> /= i j _; rewrite d_fu.
+qed.
 
 lemma dvector_rnd_funi (d : R distr) (v1 v2 : vector) l :
   is_funiform d => size v1 = size v2 => 

theories/crypto/SplitRO.ec

@@ -185,9 +185,17 @@ section PROOFS.
       have hn := o_pair_none <: from, to1, to2>.
       by rewrite /pair_map merge_empty // map_empty /= => ?; rewrite !mem_empty. 
     + by conseq RO_get.
-    + by proc; inline *; auto => />;
-       smt (get_setE map_set set_pair_map mem_map mem_pair_map mem_set mapE mergeE topairK).
-    + by proc; inline *; auto; smt (map_rem rem_merge mem_map mem_pair_map mem_rem).
+    + proc; inline *; auto => |> &2 ih; split.
+      + apply: fmap_eqP=> z; rewrite mapE /= mergeE // !get_setE; case: (z = x{2}).
+        + by case _: (topair y{2})=> y1 y2 |> @/o_pair /= <-; rewrite topairK.
+        by rewrite mapE /= mergeE.
+      move=> z; rewrite !domE !get_setE; case: (z = x{2})=> // _.
+      by rewrite -!domE; exact: ih.
+    + proc; inline *; auto=> |> &2 ih; split.
+      + apply: fmap_eqP=> z; rewrite mapE /= mergeE // !remE; case: (z = x{2})=> //.
+        by move=> _; rewrite mapE /= mergeE.
+      move=> z; rewrite !domE !remE; case: (z = x{2})=> // _.
+      by rewrite -!domE; exact: ih.
     + proc *.
       inline {1} 1.
       outline {2} 1 by { RO_Pair(I1.RO, I2.RO).get(x); }.

theories/crypto/assumptions/DHIES.ec

@@ -985,8 +985,8 @@ last by wp; skip; rewrite /inv /= => />; smt (fdom0 emptyE).
     case _: (Adv2_Procs.kindex.[(pk, ctxt.`1)]{2}).
     + by move: H10; rewrite -mem_fdom H -H2 mem_fdom domE.
     smt ().
-   wp; skip; rewrite /inv /= /#.
-  wp; skip; rewrite /inv /#.
+   by auto=> |> &1 &2 @/inv |> _ + _ _ _ _ _ _ _ _ _ _ /#.
+  by auto=> |> &1 &2 @/inv |> _ _ + _ _ _ _ _ _ _ /#.
 + by auto => />.
 + by auto => />.
 qed.

theories/datatypes/List.ec

@@ -446,7 +446,15 @@ proof. by move/onth_some => [? <-]; apply/mem_nth. qed.
 
 lemma nthP (x0 : 'a) (s : 'a list) (x : 'a) :
   (x \in s) <=> (exists (i : int), 0 <= i < size s /\ nth x0 s i = x) .
-proof. by elim: s; smt(size_ge0). qed.
+proof.
+elim: s=> [/#|y ys] /= ih; case: (x = y)=> [<<-|x_neq_y] /=.
++ by exists 0=> |>; smt(size_ge0).
+rewrite ih; split=> - [] i [#].
++ by move=> ge0_i i_lt_szys ith_ys_is_x; exists (i + 1)=> /#.
+move=> /lez_eqVlt; rewrite (eq_sym 0 i).
+case: (i = 0)=> [|>|/=] i_neq_0 gt0_i i_lt_Sszys ith_ys_x.
+by exists (i - 1)=> /#.
+qed.
 
 lemma nthPn (x0 : 'a) (s : 'a list) (x : 'a) :
   ! (x \in s) <=> (forall (i : int), 0 <= i < size s => nth x0 s i <> x).
@@ -858,7 +866,10 @@ proof. by rewrite /= lezNgt; case: (0 < n). qed.
 
 lemma size_drop n (s : 'a list):
   0 <= n => size (drop n s) = max 0 (size s - n).
-proof. by elim: s n => //= /#. qed.
+proof.
+elim: s n => //= [/#|x xs ih n ge0_n].
+smt(size_ge0).
+qed.
 
 lemma drop_cat n (s1 s2 : 'a list):
   drop n (s1 ++ s2) =

theories/datatypes/Xreal.ec

@@ -195,7 +195,12 @@ lemma of_realM x y : 0.0 <= x => 0.0 <= y =>
 proof. smt (of_realdK to_realP). qed.
 
 lemma of_realI (x:real) : (inv x)%rp = inv x%rp.
-proof. smt (of_realdK to_realP  of_real_neg divr0). qed.
+proof.
+case: (0%r <= x)=> [ge0_x|/ltrNge lt0_x].
++ rewrite -{1}(of_realdK x) 1:#smt:(divr0).
+  by rewrite -to_realI to_realKd.
+by rewrite (of_real_neg x) // of_real_neg // invr_lt0.
+qed.
 hint simplify of_realI.
 
 op (%pos) (x:real) = if 0.0 <= x then x else 0.0.

theories/distributions/DInterval.ec

@@ -75,12 +75,15 @@ have uniq_s: uniq s; first apply: uniq_flatten_map.
 have mem_s: forall x, (x \in s) <=> (x \in range 0 p).
 - move=> x; rewrite mem_range; split.
   - case/flatten_mapP=> j [/= /mem_range rgj] /=.
-    case/mapP => [k [/mem_range rgk]] ->; split; [smt()|smt(@IntDiv)].
+    case/mapP => [k [/mem_range rgk]] ->; split=> [/#|].
+    by rewrite (divz_eq p q); smt(modz_ge0).
   - case=> ge0x lex; apply/flatten_mapP => /=.
     exists (x %/ q); rewrite mem_range.
-    rewrite divz_ge0 // ge0x /=; split; 1: smt(@IntDiv).
+    rewrite divz_ge0 // ge0x /=; split.
+    + rewrite -(ltr_pmul2r q gt0_q) (divzK q p dvd_qp).
+      by apply/(ler_lt_trans x _ _ _ lex)/lez_floor=> /#.
     apply/mapP; exists (x %% q); rewrite mem_range.
-    rewrite modz_ge0 1:gtr_eqF //= ltz_pmod //= &(divz_eq).
+    by rewrite modz_ge0 1:gtr_eqF //= ltz_pmod //= &(divz_eq).
 have eqs: perm_eq s (range 0 p).
 - by apply: uniq_perm_eq => //; apply/range_uniq.
 rewrite dmap1E duniformE /= undup_id ?range_uniq /pred1 /(\o).

theories/distributions/Distr.ec

@@ -650,7 +650,8 @@ qed.
 
 lemma distr_0Vmem (d : 'a distr) : d = dnull \/ exists x, x \in d.
 proof.
-have := pred_0Vmem (support d); smt(support_eq0 supportP).
+have:= pred_0Vmem (support d); case: (exists x, x \in d)=> //=.
+by rewrite negb_exists=> /support_eq0.
 qed.
 
 lemma pmax_dnull ['a] : p_max dnull<:'a> = 0%r.

theories/distributions/SDist.ec

@@ -119,7 +119,9 @@ have <- : `| Sp - Sn | = `|weight d1 - weight d2|.
   rewrite /Sp /Sn -sumB /=; try exact/summable_cond/summable_sdist.
   rewrite !weightE -sumB /= ?summable_mu1. 
   by congr; apply eq_sum => x /= /#.
-suff : flub F = Sp by rewrite /sdist -/F; smt(ler_def).
+suff : flub F = Sp.
++ rewrite /sdist -/F. print ler_def.
+  by move: ler_Sn_Sp=> /ler_def -> /#.
 apply ler_anti; split => [|_]; last first. 
 - apply (ler_trans (F pos)); last first.
   + by apply (flub_upper_bound); exists 1%r; rewrite /is_fub; smt(mu_bounded).

theories/encryption/Hybrid.ec

@@ -428,7 +428,8 @@ section.
     by rewrite range_uniq=> /= x; rewrite mem_range supp_dinter=> /#.
   have Huni : forall (x : int), x \in [0..max 0 (q - 1)] => mu1 [0..max 0 (q - 1)] x = 1%r / q%r.
   + move=> x hx; rewrite dinter1E /=.
-    by rewrite -supp_dinter hx /= /#.
+    rewrite -supp_dinter hx /= /max subz_gt0.
+    by case: (1 < q)=> |> /lezNgt /lez_eqVlt=> - [] /#.
   pose ev :=
     fun (_j:int) (g:glob HybGameFixed(L(Ob))) (r:outputA),
       let (ga,ge,l,l0) = g in p ga ge l r /\ l <= q.