From cb06194a26837cbce73f17bc459f9aeefc11cfb7 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Wed, 21 Jan 2026 18:05:59 +0100 Subject: [PATCH 1/4] Allow substitutions of locals using the same memory as that used by a `Pr` --- src/ecPV.ml | 19 +++++++++++++++++-- .../crypto/KeyEncapsulationMechanisms.eca | 4 ++-- theories/distributions/Dexcepted.ec | 14 +++++++------- theories/encryption/Means.ec | 2 +- 4 files changed, 27 insertions(+), 12 deletions(-) diff --git a/src/ecPV.ml b/src/ecPV.ml index 6d5c5bd5e1..f2fb14ad06 100644 --- a/src/ecPV.ml +++ b/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 = diff --git a/theories/crypto/KeyEncapsulationMechanisms.eca b/theories/crypto/KeyEncapsulationMechanisms.eca index 3a49fb1a91..57b847b08d 100644 --- a/theories/crypto/KeyEncapsulationMechanisms.eca +++ b/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 : diff --git a/theories/distributions/Dexcepted.ec b/theories/distributions/Dexcepted.ec index 96929b681c..4fe1391855 100644 --- a/theories/distributions/Dexcepted.ec +++ b/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: diff --git a/theories/encryption/Means.ec b/theories/encryption/Means.ec index 1600f38c80..7ba0edb18c 100644 --- a/theories/encryption/Means.ec +++ b/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. From b305f7a5b38b5499af6a1ba6e86ad3818fc39748 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 23 Jan 2026 13:25:27 +0100 Subject: [PATCH 2/4] add tests --- tests/subst-with-pr.ec | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/subst-with-pr.ec diff --git a/tests/subst-with-pr.ec b/tests/subst-with-pr.ec new file mode 100644 index 0000000000..72cd05e7f0 --- /dev/null +++ b/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. From 136f27883094b3c4ae20180b31cd5d3b484cf746 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 23 Jan 2026 13:59:51 +0100 Subject: [PATCH 3/4] ensure `/>` does not fail to substitute depending on direction of equality --- src/ecLowGoal.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 1e9306ac2d..129643d90d 100644 --- a/src/ecLowGoal.ml +++ b/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 _ -> + 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 From bec19f40b221f0f01eb4799fb689d5c947747ed7 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 23 Jan 2026 19:59:36 +0100 Subject: [PATCH 4/4] avoid using catchall --- src/ecLowGoal.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 129643d90d..b643224c7e 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -2425,7 +2425,7 @@ let t_crush ?(delta = true) ?tsolve (tc : tcenv1) = | _, _ -> `LtoR in try t_subst_x ~clear:SCnone ~kind:sk ~tside ~eqid:eqid ~except:st.cs_sbeq tc - with _ -> + 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