get rid of unbounded smt calls outside examples

theories/algebra/Ring.ec

@@ -822,11 +822,16 @@ clone include IDomain with
   op   [ - ] <- Int.([-]),
   op   ( * ) <- Int.( * ),
   op   invr  <- (fun (z : int) => z)
-  proof * by smt
+  proof unitP
+  proof * by smt()
   remove abbrev (-)
   remove abbrev (/)
   rename "ofint" as "ofint_id".
 
+realize unitP.
+  move => ? y ?; have /# : 1 <= `|y| by smt().
+qed.
+
 abbrev (^) = exp.
 
 lemma intmulz z c : intmul z c = z * c.

theories/crypto/Birthday.ec

@@ -173,7 +173,7 @@ section.
       by proc;sp;if;auto;call HS.     
     proc; call (_: size Sample.l <= Bounder.c <= q).
     + proc;sp;if=>//;inline *;auto=> /#.
-    auto;smt w=ge0_q.
+    auto; smt(ge0_q).
   qed.
 
 end section.

theories/crypto/PRP.eca

@@ -187,7 +187,7 @@ rewrite fcardD fcardUI_indep.
 rewrite fcard1 fsetIUl fcardUI_indep.
 + by apply/fsetP=> x'; rewrite !inE mem_fdom /#.
 have ->: card (fset1 x `&` frng m) = if x \in (frng m) then 1 else 0.
-+ smt (@FSet).
++ smt(fset1I fcard1 fcards0).
 by move: x_notin_m; rewrite -mem_fdom; smt (leq_card_rng_dom @FSet).
 qed.
 

theories/crypto/assumptions/DHIES.ec

@@ -638,7 +638,7 @@ wp; call (_: inv (glob MRPKE_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} Adv1
     by wp; skip; rewrite /inv /=; clear inv => />; smt (fdom_set get_setE mem_fdom).
   by skip.
 + proc.
-  sp; if; 1: (by rewrite /inv; progress; smt); 2: (by wp;skip;progress;smt).
+  sp; if; 1: (by rewrite /inv; progress; smt()); 2: (by wp;skip;progress;smt()).
   if => //=.
   + by move=> /> /#.
   wp; transitivity{1} { r <@ MEnc.mencrypt(pks, tag, MRPKE_lor.b ? m1 : m0); }
@@ -835,7 +835,7 @@ wp; call (_: inv (glob MRPKErnd_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} A
    by wp; skip; rewrite /inv => />; smt (fdom_set mem_fdom in_fsetU).
   by skip; rewrite /inv.
 + proc.
-  sp; if; 1: (by rewrite /inv; progress; smt); 2: (by wp;skip;progress;smt).
+  sp; if; 1: (by rewrite /inv; progress; smt()); 2: (by wp;skip;progress;smt()).
   if => //=; 1: by smt ().
   inline *.
   rcondt {2} 9; 1: by move => *;wp;rnd;rnd;wp;rewrite /inv /=; clear inv;wp;skip => />; smt().

theories/crypto/prp_prf/Strong_RP_RF.eca

@@ -133,7 +133,7 @@ lemma excepted_lossless (m:(D,D) fmap):
   mu (uD \ (rng m)) predT = 1%r.
 proof. 
 move=> /endo_dom_rng [x h]; rewrite dexcepted_ll //.
-+ smt w=uD_uf_fu.
++ smt(uD_uf_fu).
 have [?[<- @/is_full Hsupp]]:= uD_uf_fu.
 apply/notin_supportIP;exists x => />;apply Hsupp.
 qed.

theories/datatypes/Real.ec

@@ -172,21 +172,21 @@ instance ring with real
   op expr  = RField.exp
   op ofint = CoreReal.from_int
 
-  proof oner_neq0 by smt ml=0
-  proof addr0     by smt ml=0
-  proof addrA     by smt ml=0
-  proof addrC     by smt ml=0
-  proof addrN     by smt ml=0
-  proof mulr1     by smt ml=0
-  proof mulrA     by smt ml=0
-  proof mulrC     by smt ml=0
-  proof mulrDl    by smt ml=0
-  proof expr0     by smt w=(expr0 exprS exprN)
-  proof exprS     by smt w=(expr0 exprS exprN)
-  proof ofint0    by smt ml=0
-  proof ofint1    by smt ml=0
-  proof ofintS    by smt ml=0
-  proof ofintN    by smt ml=0.
+  proof oner_neq0 by smt()
+  proof addr0     by smt()
+  proof addrA     by smt()
+  proof addrC     by smt()
+  proof addrN     by smt()
+  proof mulr1     by smt()
+  proof mulrA     by smt()
+  proof mulrC     by smt()
+  proof mulrDl    by smt()
+  proof expr0     by smt(expr0 exprS exprN)
+  proof exprS     by smt(expr0 exprS exprN)
+  proof ofint0    by smt()
+  proof ofint1    by smt()
+  proof ofintS    by smt()
+  proof ofintN    by smt().
 
 instance field with real
   op rzero = CoreReal.zero
@@ -198,23 +198,23 @@ instance field with real
   op ofint = CoreReal.from_int
   op inv   = CoreReal.inv
 
-  proof oner_neq0 by smt ml=0
-  proof addr0     by smt ml=0
-  proof addrA     by smt ml=0
-  proof addrC     by smt ml=0
-  proof addrN     by smt ml=0
-  proof mulr1     by smt ml=0
-  proof mulrA     by smt ml=0
-  proof mulrC     by smt ml=0
-  proof mulrDl    by smt ml=0
-  proof mulrV     by smt ml=0
-  proof expr0     by smt w=(expr0 exprS exprN)
-  proof exprS     by smt w=(expr0 exprS exprN)
-  proof exprN     by smt w=(expr0 exprS exprN)
-  proof ofint0    by smt ml=0
-  proof ofint1    by smt ml=0
-  proof ofintS    by smt ml=0
-  proof ofintN    by smt ml=0.
+  proof oner_neq0 by smt()
+  proof addr0     by smt()
+  proof addrA     by smt()
+  proof addrC     by smt()
+  proof addrN     by smt()
+  proof mulr1     by smt()
+  proof mulrA     by smt()
+  proof mulrC     by smt()
+  proof mulrDl    by smt()
+  proof mulrV     by smt()
+  proof expr0     by smt(expr0 exprS exprN)
+  proof exprS     by smt(expr0 exprS exprN)
+  proof exprN     by smt(expr0 exprS exprN)
+  proof ofint0    by smt()
+  proof ofint1    by smt()
+  proof ofintS    by smt()
+  proof ofintN    by smt().
 
 (* -------------------------------------------------------------------- *)
 op floor : real -> int.

theories/distributions/Distr.ec

@@ -689,7 +689,7 @@ qed.
 lemma supp_drat (s : 'a list) x : x \in (drat s) <=> x \in s.
 proof.
 rewrite /support dratE -has_pred1 has_count.
-case: (count (pred1 x) s <= 0); [smt w=count_ge0|].
+case: (count (pred1 x) s <= 0); [smt(count_ge0)|].
 move=> /IntOrder.ltrNge ^ + -> /=; rewrite -lt_fromint; case: s=> //=.
 move=> ? s /(@mulr_gt0 _ (inv (1 + size s)%r)) -> //.
 by rewrite invr_gt0 lt_fromint #smt:(size_ge0).

theories/query_counting/Counter.eca

@@ -67,7 +67,7 @@ section.
   move=> S_ll.
   exists* Counter.c; elim*=> c0.
   bypr=> &m0 /= /eq_sym /(D_bounded S c0 &m0 S_ll) pr_E1.
-  apply/ler_anti; split=> [|_]; first by smt w=mu_bounded.
+  apply/ler_anti; split=> [|_]; first by smt(mu_bounded).
   by rewrite -pr_E1 Pr [mu_sub].
   qed.
 

theories/query_counting/OracleBounds.ec

@@ -143,29 +143,29 @@ theory EnfPen.
     lemma enf_implies_pen &m:
       Pr[IND(Count(O),A).main() @ &m: res /\ Counter.c <= bound] <= Pr[IND(Enforce(Count(O)),A).main() @ &m: res].
     proof strict.
-    byequiv (_: ={glob A, glob O} ==> Counter.c{1} <= bound => res{1} = res{2})=> //; last smt.
+    byequiv (_: ={glob A, glob O} ==> Counter.c{1} <= bound => res{1} = res{2})=> //; last smt().
     symmetry; proc.
     call (_: !Counter.c <= bound, ={glob Counter, glob O}, Counter.c{1} <= bound).
       (* A lossless *)
       by apply A_distinguishL.
       (* Enforce(Count(O)).f ~ Count(O) *)
       proc*; inline Enforce(Count(O)).f; case (Counter.c{2} = bound).
-        rcondf{1} 3; first by progress; wp; skip; smt.
+        rcondf{1} 3; first by progress; wp; skip; smt().
         exists* Counter.c{1}; elim* => c; call{2} (CountO_fC O c _); first by apply O_fL.
-        by wp; skip; smt.
-        rcondt{1} 3; first by progress; wp; skip; smt.
+        by wp; skip; smt().
+        rcondt{1} 3; first by progress; wp; skip; smt().
         wp; exists* Counter.c{2}; elim* => c; call (CountO_fC_E O c).
-        by wp; skip; smt.
+        by wp; skip; smt().
       (* Enforce(Count(O)).f lossless *)
       by progress; proc; sp; if=> //;
-         inline Count(O).f Counter.incr; wp; call O_fL; wp; skip; smt.
+         inline Count(O).f Counter.incr; wp; call O_fL; wp; skip; smt().
       (* Count(O).f preserves bad *)
       move=> &m1 //=; bypr; move=> &m0 bad.
-        apply/ler_anti; rewrite andaE; split; first by smt w=mu_bounded.
+        apply/ler_anti; rewrite andaE; split; first by smt(mu_bounded).
         have lbnd: phoare[Count(O).f: Counter.c = Counter.c{m0} ==> Counter.c = Counter.c{m0} + 1] >= 1%r;
           first by conseq [-frame] (CountO_fC O Counter.c{m0} _); apply O_fL.
-        by byphoare lbnd=> //; smt.
-    by inline Counter.init; wp; skip; smt.
+        by byphoare lbnd=> //; smt().
+    inline Counter.init; wp; skip; smt(leq0_bound).
     qed.
   end section.
 end EnfPen.
@@ -231,28 +231,28 @@ theory BndPen.
     lemma enforcedAdv_bounded:
       phoare[EnforcedAdv(A,Count(O)).distinguish: Counter.c = 0 ==> Counter.c <= bound] = 1%r.
     proof strict.
-      proc (Counter.c <= bound)=> //; first by smt.
+      proc (Counter.c <= bound)=> //; first by smt(leq0_bound).
         by apply A_distinguishL.
       by proc; sp; if;
            [exists* Counter.c; elim* => c; call (CountO_fC O c _); first apply O_fL |];
-         skip; smt.
+         skip; smt().
     qed.
 
     equiv enforcedAdv_bounded_E:
       EnforcedAdv(A,Count(O)).distinguish ~ EnforcedAdv(A,Count(O)).distinguish:
         ={glob A, glob O, Counter.c} /\ Counter.c{1} = 0 ==>
         ={glob A, glob O, res, Counter.c} /\ Counter.c{1} <= bound.
     proof strict.
-    proc (={glob O, Counter.c} /\ Counter.c{1} <= bound)=> //; first smt.
-    proc; sp; if=> //; inline Count(O).f Counter.incr; wp; call (_: true); wp; skip; smt.
+    proc (={glob O, Counter.c} /\ Counter.c{1} <= bound)=> //; first smt(leq0_bound).
+    proc; sp; if=> //; inline Count(O).f Counter.incr; wp; call (_: true); wp; skip; smt().
     qed.
 
     (* Security against the bounded adversary implies penalty-style security  *)
     lemma bnd_implied_pen &m:
       Pr[IND(Count(O),A).main() @ &m: res /\ Counter.c <= bound] <=
        Pr[IND(Count(O),EnforcedAdv(A)).main() @ &m: res].
     proof strict.
-    byequiv (_: ={glob A, glob O} ==> Counter.c{1} <= bound => ={res, glob Count})=> //; last smt.
+    byequiv (_: ={glob A, glob O} ==> Counter.c{1} <= bound => ={res, glob Count})=> //; last smt().
     symmetry; proc.
     call (_: bound < Counter.c, ={glob Counter, glob Enforce, glob O}).
       (* A lossless *)
@@ -262,20 +262,21 @@ theory BndPen.
         rcondf{1} 3; first by progress; wp.
         exists* Counter.c{2}; elim* => c; call{2} (CountO_fC O c _);
           first apply O_fL.
-        by wp; skip; smt.
-        rcondt{1} 3; first by progress; wp; skip; smt.
+        by wp; skip; smt().
+        rcondt{1} 3; first by progress; wp; skip; smt().
         wp; exists* Counter.c{2}; elim* => c; call (CountO_fC_E O c).
         by wp.
       (* Wrap(O).f lossless *)
       by progress; proc; sp; if; [call (CountO_fL O _); first apply O_fL |].
       (* O.f preserves bad *)
       progress; bypr; move=> &m0 bad.
-      have: 1%r <= Pr[Count(O).f(x{m0}) @ &m0: bound < Counter.c]; last smt.
+      have: 1%r <= Pr[Count(O).f(x{m0}) @ &m0: bound < Counter.c]; last first.
+        have /#: Pr[Count(O).f(x{m0}) @ &m0: bound < Counter.c] <= 1%r by byphoare => /> //.
       have lbnd: phoare[Count(O).f: Counter.c = Counter.c{m0} ==> Counter.c = Counter.c{m0} + 1] >= 1%r;
         first by conseq [-frame] (CountO_fC O Counter.c{m0} _); first apply O_fL.
-      by byphoare lbnd; last smt.
+      by byphoare lbnd; last smt().
     inline Counter.init; wp.
-    by skip; smt.
+    by skip; smt().
     qed.
   end section.
 end BndPen.