In matching, forbid the capture of all variables

EasyCrypt · Feb 5, 2025 · 1112be6 · 1112be6
1 parent ee61190
commit 1112be6
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 8 deletions.
diff --git a/src/ecMatching.ml b/src/ecMatching.ml
@@ -946,8 +946,7 @@ module FPosition = struct
                doit pos (`WithCtxt (ctxt, b :: fs))
 
           | Fquant (_, b, f) ->
-              let xs   = List.pmap (function (x, GTty _) -> Some x | _ -> None) b in
-              let ctxt = List.fold_left ((^~) Sid.add) ctxt xs in
+              let ctxt = List.fold_left ((^~) Sid.add) ctxt (List.fst b) in
               doit pos (`WithCtxt (ctxt, [f]))
 
           | Flet (lp, f1, f2) ->

diff --git a/theories/crypto/PROM.ec b/theories/crypto/PROM.ec
@@ -233,16 +233,16 @@ section ConditionalLL.
 declare axiom dout_ll x: is_lossless (dout x).
 
 lemma RO_get_ll : islossless RO.get.
-proof. by proc; auto=> />; rewrite dout_ll. qed.
+proof. by proc; auto=> /> &0; rewrite dout_ll. qed.
 
 lemma FRO_get_ll : islossless FRO.get.
-proof. by proc; auto=> />; rewrite dout_ll. qed.
+proof. by proc; auto=> /> &0; rewrite dout_ll. qed.
 
 lemma RO_sample_ll : islossless RO.sample.
 proof. by proc; call RO_get_ll. qed.
 
 lemma FRO_sample_ll : islossless FRO.sample.
-proof. by proc; auto=> />; rewrite dout_ll. qed.
+proof. by proc; auto=> /> &0; rewrite dout_ll. qed.
 end section ConditionalLL.
 end section LL.
 

diff --git a/theories/crypto/ROM.eca b/theories/crypto/ROM.eca
@@ -61,7 +61,7 @@ lemma LRO_init_ll : islossless LRO.init.
 proof. by proc; auto. qed.
 
 lemma LRO_o_ll : (forall x, is_lossless (dout x)) => islossless LRO.o.
-proof. by move=> dout_ll; proc; auto; rewrite dout_ll. qed.
+proof. by move=> dout_ll; proc; auto=> &0; rewrite dout_ll. qed.
 
 hoare LRO_initE : LRO.init : true ==> LRO.m = empty.
 proof. by proc; auto. qed.

diff --git a/theories/distributions/DProd.ec b/theories/distributions/DProd.ec
@@ -103,8 +103,8 @@ have ->:   Pr[SampleDLet.sample(dt{m1}, du{m1}) @ &m1 : res = x]
 suff ->//:   Pr[SampleDLet.sample2(dt{m1}, du{m1}) @ &m2 : res.`2 = x]
            = mu1 (dlet dt{m1} du{m1}) x.
 byphoare(_ : dt{m1} = dt /\ du{m1} = du ==> _) => //=.
-proc; rnd; skip => /=; rewrite dlet1E dlet_muE_swap /=.
-move=> &hr [-> ->]; apply: eq_sum => y /=; rewrite (@sumD1 _ (y, x)) /=.
+proc; rnd; auto=> />; rewrite dlet1E dlet_muE_swap /=.
+apply: eq_sum => y /=; rewrite (@sumD1 _ (y, x)) /=.
 + by apply/summable_cond/summableZ/summable_mu1. 
 rewrite dprod1E dunit1E sum0_eq //=.
 case=> y' x' /=; case: (x' = x) => //= ->>.