Allow substitutions of locals using the same memory as that used by a Pr

ensure `/>` does not fail to substitute depending on direction of equality

Author: oskgo

src/ecLowGoal.ml

@@ -2424,7 +2424,10 @@ let t_crush ?(delta = true) ?tsolve (tc : tcenv1) =
                 | _, `Local _ -> `RtoL
                 | _, _        -> `LtoR
             in
-            t_subst_x ~clear:SCnone ~kind:sk ~tside ~eqid:eqid ~except:st.cs_sbeq tc
+            try t_subst_x ~clear:SCnone ~kind:sk ~tside ~eqid:eqid ~except:st.cs_sbeq tc
+            with InvalidGoalShape -> 
+              let tside = if tside = `LtoR then `RtoL else `LtoR in
+              t_subst_x ~clear:SCnone ~kind:sk ~tside ~eqid:eqid ~except:st.cs_sbeq tc
         in
 
 (*      let _, _, side = gen in

src/ecPV.ml

@@ -171,6 +171,16 @@ module PVM = struct
 
   let has_mod b =
     List.exists (fun (_,gty) -> match gty with GTmodty _ -> true | _ -> false) b
+  
+  let has_globs m (s: subst) =
+    try
+      let mpv = Mid.find m s in
+      let has_abstract_globs = not (Mm.is_empty mpv.s_gl) in
+      let has_concrete_globs =
+        let check pv _ = is_glob pv in
+        Mnpv.exists check mpv.s_pv in
+      has_abstract_globs || has_concrete_globs
+    with Not_found -> false
 
   let rec subst env (s : subst) =
     Hf.memo_rec 107 (fun aux f ->
@@ -187,9 +197,14 @@ module PVM = struct
       | FhoareF {hf_m=m}
       | FhoareS {hs_m=(m,_)}
       | FbdHoareF {bhf_m=m}
-      | FbdHoareS {bhs_m=(m,_)}
-      | Fpr {pr_mem=m} ->
+      | FbdHoareS {bhs_m=(m,_)} ->
+        check_binding m s;
+        EcFol.f_map (fun ty -> ty) aux f
+      | Fpr {pr_mem; pr_event={m}}  ->
         check_binding m s;
+        (* Substituting globals using the memory of the pr may erase information *)
+        if has_globs pr_mem s then
+          raise MemoryClash;
         EcFol.f_map (fun ty -> ty) aux f
       | Fquant(q,b,f1) ->
         let f1 =

tests/subst-with-pr.ec

@@ -0,0 +1,12 @@
+require import Real.
+
+module M = {var x: bool proc p()={}}.
+
+lemma L (&m: {b:bool}): b{m}= true => Pr[M.p()@&m:true] = 1%r. 
+proof. move => ->>. abort.
+
+lemma L (&m: {b:bool}): M.x{m}= true => Pr[M.p()@&m:true] = 1%r. 
+proof. fail move => ->>. abort.
+
+lemma L: phoare[M.p{&m}: true ==> Pr[M.p()@&m:true] = 1%r] = 1%r.
+proof. proc. abort.

theories/crypto/KeyEncapsulationMechanisms.eca

@@ -3205,7 +3205,7 @@ seq 1 : (k = kt) pr_dec_skc pr_dec_skcp _ 0%r (#pre) => //.
   rewrite Pr[mu_not] (: Pr[S.decaps(sk{m'}, c{m'}) @ &m' : true] = 1%r); 1: by byphoare S_decaps_ll => //.
   by rewrite RField.subr_eq0 eq_sym; byphoare (S_decaps_sl (glob S){m}) => //. 
 + call (: glob S = (glob S){m} /\ arg = (skt, ct) ==> res = kt); 2: by skip.
-  rewrite /pr_dec_skc; bypr => /> &m' glS ->.
+  rewrite /pr_dec_skc; bypr => /> &m' glS.
   by byequiv => //; proc true. 
 + call (: glob S = (glob S){m} /\ arg = (skt', ct') ==> res = kt'); 2: by skip => />.
   rewrite /pr_dec_skcp; bypr=> &m' [glS ->] /=.
@@ -3237,7 +3237,7 @@ local equiv Eqv_DecapsOrder :
     ={glob S} /\ arg{1} = (arg.`2, arg.`1, arg.`4, arg.`3){2} ==> res{1} = (res.`2, res.`1){2}.
 proof.
 bypr (res.`1, res.`2){1} (res.`2, res.`1){2} => [/#|]. 
-move=> /> &1 &2 [kt kt'] eqglS -> /=. 
+move=> /> &1 &2 [kt kt'] eqglS /=. 
 rewrite (EqPr_DecapsOrder &1 _ _ _ _ kt kt'). 
 have->: Pr[Decaps_Order.main(sk{2}, sk'{2}, c{2},
                      c'{2}) @ &2 :

theories/distributions/Dexcepted.ec

@@ -582,8 +582,8 @@ proof. by bypr=> &m; exact/(@pr_sampleW &m i{m} P). qed.
 equiv sampleE_sampleI : SampleE.sample ~ SampleI.sample :
   ={i} /\ is_lossless (dt i{1}) ==> ={res}.
 proof.
-bypr (res{1}) (res{2})=> /> &m1 &m2 a <- dt_ll.
-by rewrite (@pr_sampleE &m1 i{m1} (pred1 a)) (@pr_sampleI &m2 i{m1} (pred1 a)).
+bypr (res{1}) (res{2}) => /> &m1 &m2 a dt_ll.
+by rewrite (@pr_sampleE &m1 i{m2} (pred1 a)) (@pr_sampleI &m2 i{m2} (pred1 a)).
 qed.
 
 lemma sampleE_sampleI_pr &m x P:
@@ -594,9 +594,9 @@ proof. by move=> dt_ll; byequiv sampleE_sampleI. qed.
 equiv sampleE_sampleWi : SampleE.sample ~ SampleWi.sample :
   ={i} /\ is_lossless (dt i{1}) /\ test i{2} r{2} ==> ={res}.
 proof.
-bypr (res{1}) (res{2})=> /> &m1 &m2 a <- dt_ll Htr.
-rewrite (@pr_sampleE &m1 i{m1} (pred1 a)).
-by rewrite (@pr_sampleWi &m2 i{m1} r{m2} (pred1 a)) // Htr.
+bypr (res{1}) (res{2})=> /> &m1 &m2 a dt_ll Htr.
+rewrite (@pr_sampleE &m1 i{m2} (pred1 a)).
+by rewrite (@pr_sampleWi &m2 i{m2} r{m2} (pred1 a)) // Htr.
 qed.
 
 lemma sampleE_sampleWi_pr &m x y P:
@@ -608,8 +608,8 @@ proof. by move=> dt_ll test_i_r; byequiv sampleE_sampleWi. qed.
 equiv sampleE_sampleW : SampleE.sample ~ SampleW.sample :
   ={i} /\ is_lossless (dt i{1}) ==> ={res}.
 proof.
-bypr (res{1}) (res{2})=> /> &m1 &m2 a <- dt_ll.
-by rewrite (@pr_sampleE &m1 i{m1} (pred1 a)) (@pr_sampleW &m2 i{m1} (pred1 a)).
+bypr (res{1}) (res{2})=> /> &m1 &m2 a dt_ll.
+by rewrite (@pr_sampleE &m1 i{m2} (pred1 a)) (@pr_sampleW &m2 i{m2} (pred1 a)).
 qed.
 
 lemma sampleE_sampleW_pr &m x P:

theories/encryption/Means.ec

@@ -35,7 +35,7 @@ seq 1: (v = x) (mu1 d v) pr 1%r 0%r ((glob A) = (glob A){m})=> //.
 + by rnd; auto=> />; rewrite pred1E.
 + call (: (glob A) = (glob A){m} /\ x = v
           ==> ev v (glob A) res)=> //.
-  rewrite /pr; bypr=> /> &0 eqGlob <<-.
+  rewrite /pr; bypr=> /> &0 eqGlob.
   by byequiv (: ={glob A, x} ==> ={res, glob A})=> //; proc true.
 by hoare => /=; call (: true); auto=> /#.
 qed.