[chore] remove more raw smt calls

EasyCrypt · Jun 26, 2023 · 78d5954 · 78d5954
1 parent 3693e61
commit 78d5954
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 10 deletions.
diff --git a/theories/algebra/Bigop.eca b/theories/algebra/Bigop.eca
@@ -258,8 +258,9 @@ lemma nosmt eq_big_perm (P : 'a -> bool) (F : 'a -> t) s1 s2:
 proof.
   move=> /perm_eqP; rewrite !(@big_mkcond P).
   elim s1 s2 => [|i s1 ih1] s2 eq_s12.
-    by case s2 eq_s12 => // i s2 h; have := h (pred1 i); smt.
-  have r2i: mem s2 i by rewrite -has_pred1 has_count -eq_s12 #smt.
+  + case: s2 eq_s12=> // i s2 h.
+    by have := h (pred1 i)=> //=; smt(count_ge0).
+  have r2i: mem s2 i by rewrite -has_pred1 has_count -eq_s12 #smt:(count_ge0).
   have/splitPr [s3 s4] ->> := r2i.
   rewrite big_cat !big_cons /(predT i) /=.
   rewrite addmCA; congr; rewrite -big_cat; apply/ih1=> a.
@@ -483,7 +484,7 @@ qed.
 (* -------------------------------------------------------------------- *)
 lemma nosmt big_int_cond m n P F:
   bigi P F m n = bigi (fun i => m <= i < n /\ P i) F m n.
-proof. by rewrite big_seq_cond; apply/eq_bigl=> i /=; smt. qed.
+proof. by rewrite big_seq_cond; apply/eq_bigl=> i /=; rewrite mem_range. qed.
 
 (* -------------------------------------------------------------------- *)
 lemma nosmt big_int m n F:
@@ -498,7 +499,7 @@ lemma nosmt congr_big_int (m1 n1 m2 n2 : int) P1 P2 F1 F2:
     => bigi P1 F1 m1 n1 = bigi P2 F2 m2 n2.
 proof.
   move=> <- <- eqP12 eqF12; rewrite big_seq_cond (@big_seq_cond P2).
-  by apply/eq_big=> i /=; rewrite mem_range #smt.
+  by apply/eq_big=> i /=; rewrite mem_range #smt:().
 qed.
 
 (* -------------------------------------------------------------------- *)

diff --git a/theories/crypto/assumptions/DHIES.ec b/theories/crypto/assumptions/DHIES.ec
@@ -701,9 +701,13 @@ wp; call (_: inv (glob MRPKE_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} Adv1
       rewrite (L1 (fun k v => (g^ephL, hash(k^ephL))) pks{2} keys00) //.
        by apply/(supp_dlist_size _ _ _ _ H11)/size_ge0.
       move=> /= ? ?; move: H17; rewrite mem_cat mem_join; move=> [?|?]; first left; smt().
-      right; rewrite mem_ofassoc -!map_comp /(\o) /=; apply/mapP; exists pk; split; first smt.
+      right; rewrite mem_ofassoc -!map_comp /(\o) /=; apply/mapP; exists pk; split.
+      + move: H17; rewrite /fold_encs; elim: (elems pks{2})=> // pk0 pks ih.
+        by case: (pk = pk0)=> />.
       have T: pk \in map fst (map (fun x => (x, (g^ephL, hash(x^ephL)))) (elems pks{2})).
-       rewrite -map_comp /(\o) map_id; smt.
+      + rewrite -map_comp /(\o) map_id.
+        move: H17; rewrite /fold_encs; elim: (elems pks{2})=> // pk0 pks ih.
+        by case: (pk = pk0)=> />.
       rewrite (ephmem_foldenc _ _ _ _ _ _ _ _ T H16 H17) /=.
       have ? : 0 <= index pk (elems pks{2}) < size (elems pks{2}).
       + smt(index_ge0 index_mem map_comp mapP).
@@ -883,10 +887,12 @@ wp; call (_: inv (glob MRPKErnd_lor){1} (glob MRPKE_lor){2} (glob ODH_Orcl){2} A
     move=> /pkmem_foldenc; smt (memE mem_fdom).
   + move: H10; rewrite mem_cat mem_join; move=> [?|?]; first smt().
     right; rewrite mem_ofassoc -!map_comp /(\o) /=.
-    have T: pk \in map fst hs{2} by smt.
+    have T: pk \in map fst hs{2}.
+    + rewrite H7; move: H10=> @/fold_encs.
+      by elim: (elems pks{2})=> /> pk0 pks ih; case: (pk = pk0).
     rewrite (ephmem_foldenc _ _ _ _ _ _ _ _ T H9 H10) /=.
-    have ?: (pk \in map fst hs{2})%List by smt.
-    have ?: uniq (map fst hs{2}) by smt.
+    have ?: uniq (map fst hs{2}).
+    + by rewrite H7 uniq_elems.
     apply/mapP => /=.
     exists (pk,oget (assoc hs{2} pk)) => //=.
     by apply assoc_get_mem.

diff --git a/theories/crypto/prp_prf/Strong_RP_RF.eca b/theories/crypto/prp_prf/Strong_RP_RF.eca
@@ -144,7 +144,8 @@ proc; seq  1: (exists x, support uD x /\ !X x)=> //=.
 + by rnd (predT); skip; smt(uD_uf_fu).
 if=> //=.
 + rnd (predT); skip.
-  progress [-split]; split=> //=; smt.
+  move=> /> &0; rewrite dexceptedE predTI mu_not.
+  smt(notin_supportIP).
 by hoare; rnd=> //=; skip=> &hr ->.
 qed.