From 4cadc73c3c33f2d77fde231faae6d6f45615836e Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Mon, 24 Mar 2025 18:49:33 +0000 Subject: [PATCH 01/26] add memory to `sHoareF` --- src/ecAst.ml | 1 + src/ecAst.mli | 1 + src/ecCallbyValue.ml | 2 +- src/ecCoreFol.ml | 2 +- 4 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ecAst.ml b/src/ecAst.ml index 2b30c35686..08391c37c6 100644 --- a/src/ecAst.ml +++ b/src/ecAst.ml @@ -231,6 +231,7 @@ and equivS = { es_po : form; } and sHoareF = { + hf_m : memory; hf_pr : form; hf_f : EcPath.xpath; hf_po : form; diff --git a/src/ecAst.mli b/src/ecAst.mli index 53c542bdc0..30c51f7179 100644 --- a/src/ecAst.mli +++ b/src/ecAst.mli @@ -226,6 +226,7 @@ and equivS = { es_po : form; } and sHoareF = { + hf_m : memory; hf_pr : form; hf_f : EcPath.xpath; hf_po : form; diff --git a/src/ecCallbyValue.ml b/src/ecCallbyValue.ml index aee423acb8..1422520914 100644 --- a/src/ecCallbyValue.ml +++ b/src/ecCallbyValue.ml @@ -483,7 +483,7 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form = let hf_pr = norm st s hf.hf_pr in let hf_po = norm st s hf.hf_po in let hf_f = norm_xfun st s hf.hf_f in - f_hoareF_r { hf_pr; hf_f; hf_po } + f_hoareF_r { hf_m= mhr; hf_pr; hf_f; hf_po } | FhoareS hs -> assert (Args.isempty args); diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml index 962125360b..49c3da4ad1 100644 --- a/src/ecCoreFol.ml +++ b/src/ecCoreFol.ml @@ -278,7 +278,7 @@ let f_hoareS hs_m hs_pr hs_s hs_po = f_hoareS_r { hs_m; hs_pr; hs_s; hs_po; } let f_hoareF hf_pr hf_f hf_po = - f_hoareF_r { hf_pr; hf_f; hf_po; } + f_hoareF_r { hf_m=mhr; hf_pr; hf_f; hf_po; } (* -------------------------------------------------------------------- *) let f_eHoareS_r hs = mk_form (FeHoareS hs) tbool From abb7ff39de06e8d4c809dfa16d4c7c3981bdd28e Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 25 Mar 2025 15:42:28 +0000 Subject: [PATCH 02/26] propagate mhr --- src/ecCallbyValue.ml | 6 ++++-- src/ecCoreFol.ml | 4 ++-- src/ecCoreFol.mli | 2 +- src/ecCoreSubst.ml | 2 +- src/ecLowPhlGoal.ml | 6 +++--- src/ecScope.ml | 2 +- src/ecSubst.ml | 2 +- src/ecTyping.ml | 2 +- src/phl/ecPhlCall.ml | 6 +++--- src/phl/ecPhlConseq.ml | 26 +++++++++++++------------- src/phl/ecPhlCoreView.ml | 2 +- src/phl/ecPhlFel.ml | 4 ++-- src/phl/ecPhlFun.ml | 2 +- 13 files changed, 34 insertions(+), 32 deletions(-) diff --git a/src/ecCallbyValue.ml b/src/ecCallbyValue.ml index 1422520914..9f795d914a 100644 --- a/src/ecCallbyValue.ml +++ b/src/ecCallbyValue.ml @@ -7,6 +7,7 @@ open EcEnv open EcFol open EcReduction open EcBaseLogic +open EcMemory module BI = EcBigInt (* -------------------------------------------------------------------- *) @@ -479,11 +480,12 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form = | FhoareF hf -> assert (Args.isempty args); - assert (not (Subst.has_mem s mhr)); + assert (not (Subst.has_mem s hf.hf_m)); let hf_pr = norm st s hf.hf_pr in let hf_po = norm st s hf.hf_po in let hf_f = norm_xfun st s hf.hf_f in - f_hoareF_r { hf_m= mhr; hf_pr; hf_f; hf_po } + let (hf_m,_) = norm_me s (abstract hf.hf_m) in + f_hoareF_r { hf_m; hf_pr; hf_f; hf_po } | FhoareS hs -> assert (Args.isempty args); diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml index 49c3da4ad1..b61cce719a 100644 --- a/src/ecCoreFol.ml +++ b/src/ecCoreFol.ml @@ -277,8 +277,8 @@ let f_hoareF_r hf = mk_form (FhoareF hf) tbool let f_hoareS hs_m hs_pr hs_s hs_po = f_hoareS_r { hs_m; hs_pr; hs_s; hs_po; } -let f_hoareF hf_pr hf_f hf_po = - f_hoareF_r { hf_m=mhr; hf_pr; hf_f; hf_po; } +let f_hoareF hf_m hf_pr hf_f hf_po = + f_hoareF_r { hf_m; hf_pr; hf_f; hf_po; } (* -------------------------------------------------------------------- *) let f_eHoareS_r hs = mk_form (FeHoareS hs) tbool diff --git a/src/ecCoreFol.mli b/src/ecCoreFol.mli index 07f61851d1..9beb9c2213 100644 --- a/src/ecCoreFol.mli +++ b/src/ecCoreFol.mli @@ -117,7 +117,7 @@ val f_forall_mems : (EcIdent.t * memtype) list -> form -> form val f_hoareF_r : sHoareF -> form val f_hoareS_r : sHoareS -> form -val f_hoareF : form -> xpath -> form -> form +val f_hoareF : memory -> form -> xpath -> form -> form val f_hoareS : memenv -> form -> stmt -> form -> form (* soft-constructors - expected hoare *) diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml index 7e0253c63c..cfe8ac141d 100644 --- a/src/ecCoreSubst.ml +++ b/src/ecCoreSubst.ml @@ -455,7 +455,7 @@ module Fsubst = struct let s = f_rem_mem s mhr in let hf_pr = f_subst ~tx s hf.hf_pr in let hf_po = f_subst ~tx s hf.hf_po in - f_hoareF hf_pr hf_f hf_po + f_hoareF mhr hf_pr hf_f hf_po | FhoareS hs -> let hs_s = s_subst s hs.hs_s in diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 79244af03e..f24a775368 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -254,13 +254,13 @@ let tc1_get_post tc = (* -------------------------------------------------------------------- *) let set_pre ~pre f = match f.f_node with - | FhoareF hf -> f_hoareF pre hf.hf_f hf.hf_po + | FhoareF hf -> f_hoareF_r { hf with hf_pr = pre } | FhoareS hs -> f_hoareS_r { hs with hs_pr = pre } | FeHoareF hf -> f_eHoareF_r { hf with ehf_pr = pre } | FeHoareS hs -> f_eHoareS_r { hs with ehs_pr = pre } - | FbdHoareF hf -> f_bdHoareF pre hf.bhf_f hf.bhf_po hf.bhf_cmp hf.bhf_bd + | FbdHoareF hf -> f_bdHoareF_r { hf with bhf_pr = pre } | FbdHoareS hs -> f_bdHoareS_r { hs with bhs_pr = pre } - | FequivF ef -> f_equivF pre ef.ef_fl ef.ef_fr ef.ef_po + | FequivF ef -> f_equivF_r { ef with ef_pr = pre } | FequivS es -> f_equivS_r { es with es_pr = pre } | _ -> assert false diff --git a/src/ecScope.ml b/src/ecScope.ml index 17e1b1a4a4..1d3372987b 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1417,7 +1417,7 @@ module Op = struct f_forall (List.map (fun (x, ty) -> (x, GTty ty)) locs) - (f_hoareF + (f_hoareF mhr (f_eq args (f_tuple (List.map (fun (x, ty) -> f_local x ty) locs))) diff --git a/src/ecSubst.ml b/src/ecSubst.ml index d1b24f4f6f..6db712f800 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -536,7 +536,7 @@ let rec subst_form (s : subst) (f : form) = let hf_po = subst_form s hf_po in (hf_pr, hf_po) in let hf_f = subst_xpath s hf_f in - f_hoareF hf_pr hf_f hf_po + f_hoareF mhr hf_pr hf_f hf_po | FhoareS { hs_m; hs_pr; hs_s; hs_po } -> let hs_m, (hs_pr, hs_po) = diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 12676f0d63..06e1ff65e1 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3454,7 +3454,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let post' = transf qenv post in unify_or_fail penv ue pre.pl_loc ~expct:tbool pre' .f_ty; unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty; - f_hoareF pre' fpath post' + f_hoareF mhr pre' fpath post' | PFehoareF (pre, gp, post) -> if mode <> `Form then diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index f2f43747d2..5ca8ffbd2b 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -63,7 +63,7 @@ let t_hoare_call fpre fpost tc = let m = EcMemory.memory hs.hs_m in let fsig = (Fun.by_xpath f env).f_sig in (* The function satisfies the specification *) - let f_concl = f_hoareF fpre f fpost in + let f_concl = f_hoareF mhr fpre f fpost in (* The wp *) let pvres = pv_res in let vres = EcIdent.create "result" in @@ -391,7 +391,7 @@ let process_call side info tc = | FhoareS hs, None -> let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in let penv, qenv = LDecl.hoareF f hyps in - (penv, qenv, tbool, fun pre post -> f_hoareF pre f post) + (penv, qenv, tbool, fun pre post -> f_hoareF mhr pre f post) | FbdHoareS bhs, None -> let (_,f,_) = fst (tc1_last_call tc bhs.bhs_s) in @@ -431,7 +431,7 @@ let process_call side info tc = | FhoareS hs -> let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in let penv = LDecl.inv_memenv1 hyps in - (penv, tbool, fun inv -> f_hoareF inv f inv) + (penv, tbool, fun inv -> f_hoareF mhr inv f inv) | FeHoareS hs -> let (_,f,_) = fst (tc1_last_call tc hs.ehs_s) in diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index 5627676a70..4e72f48a70 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -55,7 +55,7 @@ let t_hoareF_conseq pre post tc = let cond1, cond2 = conseq_cond hf.hf_pr hf.hf_po pre post in let concl1 = f_forall_mems [mpr] cond1 in let concl2 = f_forall_mems [mpo] cond2 in - let concl3 = f_hoareF pre hf.hf_f post in + let concl3 = f_hoareF mhr pre hf.hf_f post in FApi.xmutate1 tc `Conseq [concl1; concl2; concl3] (* -------------------------------------------------------------------- *) @@ -610,8 +610,8 @@ let t_hoareF_conseq_conj pre post pre' post' tc = tc_error !!tc "invalid pre-condition"; if not (f_equal hf.hf_po (f_and post' post)) then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareF pre hf.hf_f post in - let concl2 = f_hoareF pre' hf.hf_f post' in + let concl1 = f_hoareF mhr pre hf.hf_f post in + let concl2 = f_hoareF mhr pre' hf.hf_f post' in FApi.xmutate1 tc `HlConseqBd [concl1; concl2] (* -------------------------------------------------------------------- *) @@ -632,7 +632,7 @@ let t_bdHoareF_conseq_conj ~add post post' tc = let posth = if add then post' else f_and post' post in if not (f_equal hs.bhf_po postc) then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareF hs.bhf_pr hs.bhf_f post in + let concl1 = f_hoareF mhr hs.bhf_pr hs.bhf_f post in let concl2 = f_bdHoareF_r { hs with bhf_po = posth } in FApi.xmutate1 tc `HlConseqBd [concl1; concl2] @@ -667,8 +667,8 @@ let t_equivF_conseq_conj pre1 post1 pre2 post2 pre' post' tc = tc_error !!tc "invalid pre-condition"; if not (f_equal ef.ef_po (f_ands [post';post1';post2'])) then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareF pre1 ef.ef_fl post1 in - let concl2 = f_hoareF pre2 ef.ef_fr post2 in + let concl1 = f_hoareF mhr pre1 ef.ef_fl post1 in + let concl2 = f_hoareF mhr pre2 ef.ef_fr post2 in let concl3 = f_equivF pre' ef.ef_fl ef.ef_fr post' in FApi.xmutate1 tc `HlConseqConj [concl1; concl2; concl3] @@ -724,7 +724,7 @@ let t_hoareF_conseq_equiv f2 p q p2 q2 tc = let env, hyps, _ = FApi.tc1_eflat tc in let hf1 = tc1_as_hoareF tc in let ef = f_equivF p hf1.hf_f f2 q in - let hf2 = f_hoareF p2 f2 q2 in + let hf2 = f_hoareF mhr p2 f2 q2 in let (prml, _prmr), (poml, pomr) = Fun.equivF_memenv hf1.hf_f f2 env in let (cond1, cond2) = transitivity_side_cond hyps prml poml pomr p q p2 q2 hf1.hf_pr hf1.hf_po in @@ -1184,13 +1184,13 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (* ------------------------------------------------------------------ *) (* equivF / ? / ? / ⊥ *) | FequivF ef, Some _, Some _, None -> - let f3 = f_hoareF f_true ef.ef_fr f_true in + let f3 = f_hoareF mhr f_true ef.ef_fr f_true in t_hi_conseq notmod f1 f2 (Some (None, f3)) tc (* ------------------------------------------------------------------ *) (* equivF / ? / ⊥ / ? *) | FequivF ef, Some _, None, Some _ -> - let f2 = f_hoareF f_true ef.ef_fl f_true in + let f2 = f_hoareF mhr f_true ef.ef_fl f_true in t_hi_conseq notmod f1 (Some (None, f2)) f3 tc | _ -> @@ -1248,7 +1248,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) let fmake pre post c_or_bd = match c_or_bd with | None -> - f_hoareF pre hf.hf_f post + f_hoareF mhr pre hf.hf_f post | Some (PCI_bd (cmp, bd)) -> f_bdHoareF pre hf.hf_f post (oget cmp) bd @@ -1344,7 +1344,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) in let penv, qenv = LDecl.hoareF f hyps in let fmake pre post c_or_bd = - ensure_none c_or_bd; f_hoareF pre f post in + ensure_none c_or_bd; f_hoareF mhr pre f post in (penv, qenv, pr, po, tbool, fmake) | FeHoareF hf -> @@ -1377,7 +1377,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) in let penv, qenv = LDecl.hoareF f hyps in let fmake pre post c_or_bd = - ensure_none c_or_bd; f_hoareF pre f post in + ensure_none c_or_bd; f_hoareF mhr pre f post in (penv, qenv, pr, po, tbool, fmake) | FequivF ef -> @@ -1385,7 +1385,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) let penv, qenv = LDecl.hoareF f hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; - f_hoareF pre f post in + f_hoareF mhr pre f post in (penv, qenv, f_true, f_true, tbool, fmake) | FequivS es -> diff --git a/src/phl/ecPhlCoreView.ml b/src/phl/ecPhlCoreView.ml index ef34c91b1d..39515872d3 100644 --- a/src/phl/ecPhlCoreView.ml +++ b/src/phl/ecPhlCoreView.ml @@ -17,7 +17,7 @@ let t_hoare_of_bdhoareF_r tc = let bhf = tc1_as_bdhoareF tc in if not (bhf.bhf_cmp = FHeq && f_equal bhf.bhf_bd f_r0) then tc_error !!tc "%s" "bound must be equal to 0%r"; - let concl = f_hoareF bhf.bhf_pr bhf.bhf_f (f_not bhf.bhf_po) in + let concl = f_hoareF mhr bhf.bhf_pr bhf.bhf_f (f_not bhf.bhf_po) in FApi.xmutate1 tc `ViewBdHoare [concl] (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml index 0bfdfbb7a6..2bb9344ff0 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -215,7 +215,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = let pre = f_and_simpl pre inv in let post = f_int_lt old_cntr cntr in let post = f_and_simpl post inv in - f_forall_simpl [old_cntr_id,GTty tint] (f_hoareF pre o post) + f_forall_simpl [old_cntr_id,GTty tint] (f_hoareF mhr pre o post) in let cntr_stable_goal = let pre = f_ands [f_not some_p;f_eq f_event old_b;f_eq cntr old_cntr] in @@ -224,7 +224,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = let post = f_and_simpl post inv in f_forall_simpl [old_b_id,GTty tbool; old_cntr_id,GTty tint] - (f_hoareF pre o post) + (f_hoareF mhr pre o post) in [not_F_to_F_goal;cntr_decr_goal;cntr_stable_goal] in diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index 98120db7ce..4612b44b96 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -160,7 +160,7 @@ module FunAbsLow = struct let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in let fv = PV.fv env mhr inv in PV.check_depend env fv top; - let ospec o = f_hoareF inv o inv in + let ospec o = f_hoareF mhr inv o inv in let sg = List.map ospec (OI.allowed oi) in (inv, inv, sg) From eecd60907ac3d0a82aa461caf73d6f82866a3a5c Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Thu, 27 Mar 2025 13:46:51 +0000 Subject: [PATCH 03/26] pv --- src/ecPV.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ecPV.ml b/src/ecPV.ml index 69125e29a6..0b78ca6611 100644 --- a/src/ecPV.ml +++ b/src/ecPV.ml @@ -187,7 +187,10 @@ module PVM = struct check_binding (fst es.es_ml) s; check_binding (fst es.es_mr) s; EcFol.f_map (fun ty -> ty) aux f - | FhoareF _ | FbdHoareF _ -> + | FhoareF hf -> + check_binding hf.hf_m s; + EcFol.f_map (fun ty -> ty) aux f + | FbdHoareF _ -> check_binding EcFol.mhr s; EcFol.f_map (fun ty -> ty) aux f | FhoareS hs -> From 02e2ca477fbc1d01040d620afc6eca78c7ad823a Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Mon, 31 Mar 2025 14:32:18 +0100 Subject: [PATCH 04/26] simple tactic fixes --- src/phl/ecPhlConseq.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index 4e72f48a70..c7f5f1dd82 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -55,7 +55,7 @@ let t_hoareF_conseq pre post tc = let cond1, cond2 = conseq_cond hf.hf_pr hf.hf_po pre post in let concl1 = f_forall_mems [mpr] cond1 in let concl2 = f_forall_mems [mpo] cond2 in - let concl3 = f_hoareF mhr pre hf.hf_f post in + let concl3 = f_hoareF_r { hf with hf_pr = pre; hf_po = post } in FApi.xmutate1 tc `Conseq [concl1; concl2; concl3] (* -------------------------------------------------------------------- *) @@ -610,8 +610,8 @@ let t_hoareF_conseq_conj pre post pre' post' tc = tc_error !!tc "invalid pre-condition"; if not (f_equal hf.hf_po (f_and post' post)) then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareF mhr pre hf.hf_f post in - let concl2 = f_hoareF mhr pre' hf.hf_f post' in + let concl1 = f_hoareF_r { hf with hf_pr=pre; hf_po=post } in + let concl2 = f_hoareF_r { hf with hf_pr=pre'; hf_po=post' } in FApi.xmutate1 tc `HlConseqBd [concl1; concl2] (* -------------------------------------------------------------------- *) @@ -1248,7 +1248,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) let fmake pre post c_or_bd = match c_or_bd with | None -> - f_hoareF mhr pre hf.hf_f post + f_hoareF_r { hf with hf_pr=pre; hf_po=post; } | Some (PCI_bd (cmp, bd)) -> f_bdHoareF pre hf.hf_f post (oget cmp) bd From e4b79d268cc512efda6ba4c31da3da724e7664d8 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Mon, 31 Mar 2025 17:22:52 +0100 Subject: [PATCH 05/26] give memenv constructor for hoare a memory parameter --- src/ecEnv.ml | 15 ++++++------ src/ecEnv.mli | 6 ++--- src/ecPrinting.ml | 12 ++++----- src/ecTyping.ml | 7 +++--- src/phl/ecPhlCall.ml | 10 ++++---- src/phl/ecPhlConseq.ml | 51 ++++++++++++++++++++------------------- src/phl/ecPhlDeno.ml | 8 +++--- src/phl/ecPhlExists.ml | 7 +++--- src/phl/ecPhlFel.ml | 2 +- src/phl/ecPhlHiBdHoare.ml | 2 +- src/phl/ecPhlPr.ml | 4 +-- src/phl/ecPhlTrans.ml | 4 +-- 12 files changed, 66 insertions(+), 62 deletions(-) diff --git a/src/ecEnv.ml b/src/ecEnv.ml index a83045d38d..61a3a8286a 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -1694,15 +1694,15 @@ module Fun = struct let post = prF_memenv EcCoreFol.mhr path env in Memory.push_active post env - let hoareF_memenv path env = + let hoareF_memenv mem path env = let (ip, _) = oget (ipath_of_xpath path) in let fun_ = snd (oget (by_ipath ip env)) in - let pre = actmem_pre EcCoreFol.mhr fun_ in - let post = actmem_post EcCoreFol.mhr fun_ in + let pre = actmem_pre mem fun_ in + let post = actmem_post mem fun_ in pre, post - let hoareF path env = - let pre, post = hoareF_memenv path env in + let hoareF mem path env = + let pre, post = hoareF_memenv mem path env in Memory.push_active pre env, Memory.push_active post env let hoareS path env = @@ -3566,8 +3566,9 @@ module LDecl = struct let push_all l lenv = { lenv with le_env = Memory.push_all l lenv.le_env } - let hoareF xp lenv = - let env1, env2 = Fun.hoareF xp lenv.le_env in +(* Note: Not confident about this change. I don't understand what this function does *) + let hoareF mem xp lenv = + let env1, env2 = Fun.hoareF mem xp lenv.le_env in { lenv with le_env = env1}, {lenv with le_env = env2 } let equivF xp1 xp2 lenv = diff --git a/src/ecEnv.mli b/src/ecEnv.mli index 0ed659eb22..a41100e444 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -97,9 +97,9 @@ module Fun : sig val prF : xpath -> env -> env - val hoareF_memenv : xpath -> env -> memenv * memenv + val hoareF_memenv : memory -> xpath -> env -> memenv * memenv - val hoareF : xpath -> env -> env * env + val hoareF : memory -> xpath -> env -> env * env val hoareS : xpath -> env -> memenv * (funsig * function_def) * env @@ -502,7 +502,7 @@ module LDecl : sig val push_all : memenv list -> hyps -> hyps val push_active : memenv -> hyps -> hyps - val hoareF : xpath -> hyps -> hyps * hyps + val hoareF : memory -> xpath -> hyps -> hyps * hyps val equivF : xpath -> xpath -> hyps -> hyps * hyps val inv_memenv : hyps -> hyps diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index a3529945b0..a21efd285a 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -1886,7 +1886,7 @@ and pp_form_core_r end | FhoareF hf -> - let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_f ppe.PPEnv.ppe_env in + let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f ppe.PPEnv.ppe_env in let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in Format.fprintf fmt "hoare[@[@ %a :@ @[%a ==>@ %a@]@]]" @@ -1902,7 +1902,7 @@ and pp_form_core_r (pp_form ppe) hs.hs_po | FeHoareF hf -> - let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.ehf_f ppe.PPEnv.ppe_env in + let mepr, mepo = EcEnv.Fun.hoareF_memenv mhr hf.ehf_f ppe.PPEnv.ppe_env in let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in Format.fprintf fmt @@ -1954,7 +1954,7 @@ and pp_form_core_r (pp_form ppepo) eg.eg_po | FbdHoareF hf -> - let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.bhf_f ppe.PPEnv.ppe_env in + let mepr, mepo = EcEnv.Fun.hoareF_memenv mhr hf.bhf_f ppe.PPEnv.ppe_env in let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in Format.fprintf fmt "phoare[@[@ %a :@ @[%a ==>@ %a@]@]] %s %a" @@ -2903,7 +2903,7 @@ let pp_post (ppe : PPEnv.t) ?prpo fmt post = (* -------------------------------------------------------------------- *) let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf = - let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_f ppe.PPEnv.ppe_env in + let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f ppe.PPEnv.ppe_env in let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in @@ -2928,7 +2928,7 @@ let pp_hoareS (ppe : PPEnv.t) ?prpo fmt hs = (* -------------------------------------------------------------------- *) let pp_eHoareF (ppe : PPEnv.t) ?prpo fmt hf = - let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.ehf_f ppe.PPEnv.ppe_env in + let mepr, mepo = EcEnv.Fun.hoareF_memenv mhr hf.ehf_f ppe.PPEnv.ppe_env in let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in @@ -2960,7 +2960,7 @@ let string_of_hrcmp = function (* -------------------------------------------------------------------- *) let pp_bdhoareF (ppe : PPEnv.t) ?prpo fmt hf = - let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.bhf_f ppe.PPEnv.ppe_env in + let mepr, mepo = EcEnv.Fun.hoareF_memenv mhr hf.bhf_f ppe.PPEnv.ppe_env in let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 06e1ff65e1..2b2a4aca66 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3449,7 +3449,8 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = tyerror f.pl_loc env (NotAnExpression `Logic); let fpath = trans_gamepath env gp in - let penv, qenv = EcEnv.Fun.hoareF fpath env in + (* TODO: Make mhr a fresh memory instead *) + let penv, qenv = EcEnv.Fun.hoareF mhr fpath env in let pre' = transf penv pre in let post' = transf qenv post in unify_or_fail penv ue pre.pl_loc ~expct:tbool pre' .f_ty; @@ -3461,7 +3462,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = tyerror f.pl_loc env (NotAnExpression `Logic); let fpath = trans_gamepath env gp in - let penv, qenv = EcEnv.Fun.hoareF fpath env in + let penv, qenv = EcEnv.Fun.hoareF mhr fpath env in let pre' = transf penv pre in let post' = transf qenv post in unify_or_fail penv ue pre.pl_loc ~expct:txreal pre'.f_ty; @@ -3473,7 +3474,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = tyerror f.pl_loc env (NotAnExpression `Logic); let fpath = trans_gamepath env gp in - let penv, qenv = EcEnv.Fun.hoareF fpath env in + let penv, qenv = EcEnv.Fun.hoareF mhr fpath env in let pre' = transf penv pre in let post' = transf qenv post in let bd' = transf penv bd in diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 5ca8ffbd2b..07c49ce23a 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -390,18 +390,18 @@ let process_call side info tc = match concl.f_node, side with | FhoareS hs, None -> let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in (penv, qenv, tbool, fun pre post -> f_hoareF mhr pre f post) | FbdHoareS bhs, None -> let (_,f,_) = fst (tc1_last_call tc bhs.bhs_s) in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in (penv, qenv, tbool, fun pre post -> bdhoare_call_spec !!tc pre post f bhs.bhs_cmp bhs.bhs_bd None) | FeHoareS hs, None -> let (_,f,_) = fst (tc1_last_call tc hs.ehs_s) in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in (penv, qenv, txreal, fun pre post -> f_eHoareF pre f post) | FbdHoareS _, Some _ @@ -417,7 +417,7 @@ let process_call side info tc = | FequivS es, Some side -> let fstmt = sideif side es.es_sl es.es_sr in let (_,f,_) = fst (tc1_last_call tc fstmt) in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in (penv, qenv, tbool, fun pre post -> f_bdHoareF pre f post FHeq f_r1) | _ -> tc_error !!tc "the conclusion is not a hoare or an equiv" in @@ -542,7 +542,7 @@ let process_call_concave (fc, info) tc = match concl.f_node with | FeHoareS hs -> let (_,f,_) = fst (tc1_last_call tc hs.ehs_s) in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in (penv, qenv, txreal, fun pre post -> f_eHoareF pre f post) | _ -> tc_error !!tc "the conclusion is not a ehoare" in diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index c7f5f1dd82..f8f2d03172 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -51,7 +51,7 @@ let bd_goal tc fcmp fbd cmp bd = let t_hoareF_conseq pre post tc = let env = FApi.tc1_env tc in let hf = tc1_as_hoareF tc in - let mpr,mpo = EcEnv.Fun.hoareF_memenv hf.hf_f env in + let mpr,mpo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f env in let cond1, cond2 = conseq_cond hf.hf_pr hf.hf_po pre post in let concl1 = f_forall_mems [mpr] cond1 in let concl2 = f_forall_mems [mpo] cond2 in @@ -71,7 +71,7 @@ let t_hoareS_conseq pre post tc = let t_ehoareF_conseq pre post tc = let env = FApi.tc1_env tc in let hf = tc1_as_ehoareF tc in - let mpr,mpo = EcEnv.Fun.hoareF_memenv hf.ehf_f env in + let mpr,mpo = EcEnv.Fun.hoareF_memenv mhr hf.ehf_f env in let cond1, cond2 = conseq_econd hf.ehf_pr hf.ehf_po pre post in let concl1 = f_forall_mems [mpr] cond1 in @@ -102,7 +102,7 @@ let bdHoare_conseq_conds cmp pr po new_pr new_po = let t_bdHoareF_conseq pre post tc = let env = FApi.tc1_env tc in let bhf = tc1_as_bdhoareF tc in - let mpr,mpo = EcEnv.Fun.hoareF_memenv bhf.bhf_f env in + let mpr,mpo = EcEnv.Fun.hoareF_memenv mhr bhf.bhf_f env in let cond1, cond2 = bdHoare_conseq_conds bhf.bhf_cmp bhf.bhf_pr bhf.bhf_po pre post in let concl1 = f_forall_mems [mpr] cond1 in @@ -124,7 +124,7 @@ let t_bdHoareS_conseq pre post tc = let t_bdHoareF_conseq_bd cmp bd tc = let env = FApi.tc1_env tc in let bhf = tc1_as_bdhoareF tc in - let mpr,_ = EcEnv.Fun.hoareF_memenv bhf.bhf_f env in + let mpr,_ = EcEnv.Fun.hoareF_memenv mhr bhf.bhf_f env in let bd_goal = bd_goal tc bhf.bhf_cmp bhf.bhf_bd cmp bd in let concl = f_bdHoareF bhf.bhf_pr bhf.bhf_f bhf.bhf_po cmp bd in let bd_goal = f_forall_mems [mpr] (f_imp bhf.bhf_pr bd_goal) in @@ -260,16 +260,15 @@ let t_equivS_notmod post tc = let cond_hoareF_notmod ?(mk_other=false) tc cond = let (env, hyps, _) = FApi.tc1_eflat tc in let hf = tc1_as_hoareF tc in - let f = hf.hf_f in - let mpr,mpo = Fun.hoareF_memenv f env in - let fsig = (Fun.by_xpath f env).f_sig in + let mpr,mpo = Fun.hoareF_memenv hf.hf_m hf.hf_f env in + let fsig = (Fun.by_xpath hf.hf_f env).f_sig in let pvres = pv_res in let vres = LDecl.fresh_id hyps "result" in let fres = f_local vres fsig.fs_ret in let m = fst mpo in let s = PVM.add env pvres m fres PVM.empty in let cond = PVM.subst env s cond in - let modi = f_write env f in + let modi = f_write env hf.hf_f in let cond,bdg,bde = generalize_mod_ env m modi cond in let cond = f_forall_simpl [(vres, GTty fsig.fs_ret)] cond in assert (fst mpr = m); @@ -315,7 +314,7 @@ let cond_bdHoareF_notmod ?(mk_other=false) tc cond = let (env, hyps, _) = FApi.tc1_eflat tc in let hf = tc1_as_bdhoareF tc in let f = hf.bhf_f in - let mpr,mpo = Fun.hoareF_memenv f env in + let mpr,mpo = Fun.hoareF_memenv mhr f env in let fsig = (Fun.by_xpath f env).f_sig in let pvres = pv_res in let vres = LDecl.fresh_id hyps "result" in @@ -398,7 +397,7 @@ let t_ehoareF_concave fc pre post tc = let env = FApi.tc1_env tc in let hf = tc1_as_ehoareF tc in let f = hf.ehf_f in - let mpr,mpo = Fun.hoareF_memenv f env in + let mpr,mpo = Fun.hoareF_memenv mhr f env in let fsig = (Fun.by_xpath f env).f_sig in let m = fst mpo in assert (fst mpr = m && fst mpo = m); @@ -475,7 +474,7 @@ let t_ehoareF_conseq_nm pre post tc = let (env, hyps, _) = FApi.tc1_eflat tc in let hf = tc1_as_ehoareF tc in let f = hf.ehf_f in - let _mpr,mpo = Fun.hoareF_memenv f env in + let _mpr,mpo = Fun.hoareF_memenv mhr f env in let fsig = (Fun.by_xpath f env).f_sig in let _cond1, cond2 = conseq_econd hf.ehf_pr hf.ehf_po pre post in @@ -525,7 +524,7 @@ let process_concave ((info, fc) : pformula option tuple2 gppterm * pformula) tc TTC.pf_process_form !!tc env (tfun txreal txreal) fc | FeHoareF hf -> - let _, env = LDecl.hoareF hf.ehf_f hyps in + let _, env = LDecl.hoareF mhr hf.ehf_f hyps in TTC.pf_process_form !!tc env (tfun txreal txreal) fc | _ -> tc_error !!tc "conseq concave: not a ehoare judgement" @@ -540,7 +539,7 @@ let process_concave ((info, fc) : pformula option tuple2 gppterm * pformula) tc (env, env, hs.ehs_pr, hs.ehs_po, fmake) | FeHoareF hf -> - let penv, qenv = LDecl.hoareF hf.ehf_f hyps in + let penv, qenv = LDecl.hoareF mhr hf.ehf_f hyps in let fmake pre post = f_eHoareF_r { hf with ehf_pr = pre; ehf_po = post } in (penv, qenv, hf.ehf_pr, hf.ehf_po, fmake) @@ -1001,7 +1000,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = let post1 = hs0.bhf_po in let post = hs.bhf_po in let posta = f_and post hs2.hf_po in - let mpr,_ = EcEnv.Fun.hoareF_memenv hs0.bhf_f (FApi.tc1_env tc) in + let mpr,_ = EcEnv.Fun.hoareF_memenv mhr hs0.bhf_f (FApi.tc1_env tc) in let concl1 = f_forall_mems [mpr] (f_imp hs0.bhf_pr pre) in let tc = ( t_cut concl1 @+ @@ -1243,7 +1242,8 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) in (env, env, hs.hs_pr, hs.hs_po, tbool, fmake) | FhoareF hf -> - let penv, qenv = LDecl.hoareF hf.hf_f hyps in + (* not confident about this change by transitivity *) + let penv, qenv = LDecl.hoareF hf.hf_m hf.hf_f hyps in let fmake pre post c_or_bd = match c_or_bd with @@ -1262,7 +1262,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) (env, env, hs.ehs_pr, hs.ehs_po, txreal, fmake) | FeHoareF hf -> - let penv, qenv = LDecl.hoareF hf.ehf_f hyps in + let penv, qenv = LDecl.hoareF mhr hf.ehf_f hyps in let fmake pre post bd = ensure_none bd; f_eHoareF_r { hf with ehf_pr = pre; ehf_po = post } in @@ -1287,7 +1287,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) (env, env, bhs.bhs_pr, bhs.bhs_po, tbool, fmake) | FbdHoareF hf -> - let penv, qenv = LDecl.hoareF hf.bhf_f hyps in + let penv, qenv = LDecl.hoareF mhr hf.bhf_f hyps in let fmake pre post c_or_bd = match c_or_bd with @@ -1336,13 +1336,14 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) in (env, env, hs.hs_pr, hs.hs_po, tbool, fmake) | FhoareF hf -> - let f, pr, po = match f1 with - | None -> hf.hf_f, hf.hf_pr, hf.hf_po + (* Not confident about this change by transitivity *) + let m, f, pr, po = match f1 with + | None -> hf.hf_m, hf.hf_f, hf.hf_pr, hf.hf_po | Some f1 -> match (snd f1).f_node with - | FequivF ef when side = `Left -> ef.ef_fr, f_true, f_true - | _ -> hf.hf_f, hf.hf_pr, hf.hf_po + | FequivF ef when side = `Left -> mhr, ef.ef_fr, f_true, f_true + | _ -> hf.hf_m, hf.hf_f, hf.hf_pr, hf.hf_po in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF m f hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; f_hoareF mhr pre f post in (penv, qenv, pr, po, tbool, fmake) @@ -1356,7 +1357,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) ef.ef_fr, f_xreal_1, f_xreal_1 | _ -> hf.ehf_f, hf.ehf_pr, hf.ehf_po in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; f_eHoareF pre f post in (penv, qenv, pr, po, txreal, fmake) @@ -1375,14 +1376,14 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) | FequivF ef when side = `Left -> ef.ef_fr, f_true, f_true | _ -> bhf.bhf_f, bhf.bhf_pr, bhf.bhf_po in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; f_hoareF mhr pre f post in (penv, qenv, pr, po, tbool, fmake) | FequivF ef -> let f = sideif side ef.ef_fl ef.ef_fr in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; f_hoareF mhr pre f post in diff --git a/src/phl/ecPhlDeno.ml b/src/phl/ecPhlDeno.ml index ff11151d6c..910d811ae8 100644 --- a/src/phl/ecPhlDeno.ml +++ b/src/phl/ecPhlDeno.ml @@ -98,7 +98,7 @@ let t_ehoare_deno_r pre post tc = let pr = destr_pr f in let concl_e = f_eHoareF pre pr.pr_fun post in - let mpr, mpo = EcEnv.Fun.hoareF_memenv pr.pr_fun env in + let mpr, mpo = EcEnv.Fun.hoareF_memenv mhr pr.pr_fun env in (* pre <= bd *) (* building the substitution for the pre *) let sargs = PVM.add env pv_arg (fst mpr) pr.pr_args PVM.empty in @@ -202,7 +202,7 @@ let process_phoare_deno info tc = in let { pr_fun = f; pr_event = event; } = destr_pr f in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in let pre = pre |> omap_dfl (fun p -> TTC.pf_process_formula !!tc penv p) f_true in let post = post |> omap_dfl (fun p -> TTC.pf_process_formula !!tc qenv p) event in @@ -236,7 +236,7 @@ let process_ehoare_deno info tc = in let { pr_fun = f; pr_mem = m; pr_event = event; } = destr_pr f in - let penv, qenv = LDecl.hoareF f hyps in + let penv, qenv = LDecl.hoareF mhr f hyps in let smem = Fsubst.f_bind_mem Fsubst.f_subst_id m mhr in let dpre = f_r2xr (Fsubst.f_subst smem bd) in @@ -542,7 +542,7 @@ let process_equiv_deno_bad2 info eq bad1 tc = let { pr_fun = fr; pr_event = evr } as prr = destr_pr fpr2 in let bad1 = - let _, qenv = LDecl.hoareF fl hyps in + let _, qenv = LDecl.hoareF mhr fl hyps in TTC.pf_process_formula !!tc qenv bad1 in let process_cut (pre, post) = diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml index c0b4bab2b8..44d8db9a2f 100644 --- a/src/phl/ecPhlExists.ml +++ b/src/phl/ecPhlExists.ml @@ -99,11 +99,12 @@ let process_exists_intro ~(elim : bool) fs tc = let (hyps, concl) = FApi.tc1_flat tc in let penv = match concl.f_node with - | FhoareF hf -> fst (LDecl.hoareF hf.hf_f hyps) + (* Not sure about this either *) + | FhoareF hf -> fst (LDecl.hoareF hf.hf_m hf.hf_f hyps) | FhoareS hs -> LDecl.push_active hs.hs_m hyps - | FeHoareF hf -> fst (LDecl.hoareF hf.ehf_f hyps) + | FeHoareF hf -> fst (LDecl.hoareF mhr hf.ehf_f hyps) | FeHoareS hs -> LDecl.push_active hs.ehs_m hyps - | FbdHoareF bhf -> fst (LDecl.hoareF bhf.bhf_f hyps) + | FbdHoareF bhf -> fst (LDecl.hoareF mhr bhf.bhf_f hyps) | FbdHoareS bhs -> LDecl.push_active bhs.bhs_m hyps | FequivF ef -> fst (LDecl.equivF ef.ef_fl ef.ef_fr hyps) | FequivS es -> LDecl.push_all [es.es_ml; es.es_mr] hyps diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml index 2bb9344ff0..63758476a2 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -272,7 +272,7 @@ let process_fel at_pos (infos : fel_info) tc = let process_pred (f,pre) = let env = LDecl.toenv hyps in let f = EcTyping.trans_gamepath env f in - let penv = fst (LDecl.hoareF f hyps) in + let penv = fst (LDecl.hoareF mhr f hyps) in (f, TTC.pf_process_form !!tc penv tbool pre) in diff --git a/src/phl/ecPhlHiBdHoare.ml b/src/phl/ecPhlHiBdHoare.ml index c0f4387631..b4d230a9b9 100644 --- a/src/phl/ecPhlHiBdHoare.ml +++ b/src/phl/ecPhlHiBdHoare.ml @@ -20,7 +20,7 @@ let process_bdhoare_split info tc = ((hyps, hyps), bhs.bhs_pr, bhs.bhs_po) | FbdHoareF bhf -> - (LDecl.hoareF bhf.bhf_f hyps, bhf.bhf_pr, bhf.bhf_po) + (LDecl.hoareF mhr bhf.bhf_f hyps, bhf.bhf_pr, bhf.bhf_po) | _ -> tc_error !!tc "the conclusion must be a bdhoare judgment" in diff --git a/src/phl/ecPhlPr.ml b/src/phl/ecPhlPr.ml index 25f1f3b31b..8fc075e5b9 100644 --- a/src/phl/ecPhlPr.ml +++ b/src/phl/ecPhlPr.ml @@ -22,7 +22,7 @@ let t_bdhoare_ppr_r tc = let bhf = tc1_as_bdhoareF tc in let f_xpath = bhf.bhf_f in let fun_ = EcEnv.Fun.by_xpath f_xpath env in - let penv,_qenv = EcEnv.Fun.hoareF_memenv f_xpath env in + let penv,_qenv = EcEnv.Fun.hoareF_memenv mhr f_xpath env in let m = EcIdent.create "&m" in let args = to_args fun_ (f_pvarg fun_.f_sig.fs_arg m) in (* Warning: currently no substitution on pre,post since penv is always mhr *) @@ -99,7 +99,7 @@ let t_prbounded_r conseq tc = let (m, pr, po, cmp, bd) = match concl.f_node with | FbdHoareF hf -> - let m = fst (Fun.hoareF_memenv hf.bhf_f env) in + let m = fst (Fun.hoareF_memenv mhr hf.bhf_f env) in (m, hf.bhf_pr, hf.bhf_po, hf.bhf_cmp, hf.bhf_bd) | FbdHoareS hf -> diff --git a/src/phl/ecPhlTrans.ml b/src/phl/ecPhlTrans.ml index 6bf9d99102..70d13c8790 100644 --- a/src/phl/ecPhlTrans.ml +++ b/src/phl/ecPhlTrans.ml @@ -66,7 +66,7 @@ module Low = struct let env, hyps, _ = FApi.tc1_eflat tc in let ef = tc1_as_equivF tc in let (prml, prmr), (poml, pomr) = Fun.equivF_memenv ef.ef_fl ef.ef_fr env in - let (_, pomt) = snd (Fun.hoareF_memenv f env) in + let (_, pomt) = snd (Fun.hoareF_memenv mhr f env) in let cond1, cond2 = transitivity_side_cond hyps prml prmr poml pomr @@ -199,7 +199,7 @@ let process_trans_fun f p1 q1 p2 q2 tc = let env, hyps, _ = FApi.tc1_eflat tc in let ef = tc1_as_equivF tc in let f = EcTyping.trans_gamepath env f in - let (_, prmt), (_, pomt) = Fun.hoareF_memenv f env in + let (_, prmt), (_, pomt) = Fun.hoareF_memenv mhr f env in let (prml, prmr), (poml, pomr) = Fun.equivF_memenv ef.ef_fl ef.ef_fr env in let process ml mr fo = TTC.pf_process_form !!tc (LDecl.push_all [ml; mr] hyps) tbool fo in From d3e1e32aae1e6a48dfc3b339cc1f2689e7bb911f Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Mon, 31 Mar 2025 17:54:10 +0100 Subject: [PATCH 06/26] add memory parameter to `hoareS` env constructor --- src/ecEnv.ml | 4 ++-- src/ecEnv.mli | 2 +- src/phl/ecPhlFel.ml | 2 +- src/phl/ecPhlFun.ml | 6 +++--- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 61a3a8286a..c4d952350c 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -1705,9 +1705,9 @@ module Fun = struct let pre, post = hoareF_memenv mem path env in Memory.push_active pre env, Memory.push_active post env - let hoareS path env = + let hoareS mem path env = let fun_ = by_xpath path env in - let fd, memenv = actmem_body EcCoreFol.mhr fun_ in + let fd, memenv = actmem_body mem fun_ in memenv, fd, Memory.push_active memenv env let equivF_memenv path1 path2 env = diff --git a/src/ecEnv.mli b/src/ecEnv.mli index a41100e444..de04b9f578 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -101,7 +101,7 @@ module Fun : sig val hoareF : memory -> xpath -> env -> env * env - val hoareS : xpath -> env -> memenv * (funsig * function_def) * env + val hoareS : memory -> xpath -> env -> memenv * (funsig * function_def) * env val actmem_body : memory -> function_ -> (funsig * function_def) * memenv val actmem_post : memory -> function_ -> memenv diff --git a/src/phl/ecPhlFel.ml b/src/phl/ecPhlFel.ml index 63758476a2..6e32de4a15 100644 --- a/src/phl/ecPhlFel.ml +++ b/src/phl/ecPhlFel.ml @@ -129,7 +129,7 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc = let ev = pr.pr_event in let memenv, (fsig, fdef), _ = - try Fun.hoareS f env + try Fun.hoareS mhr f env with _ -> tc_error !!tc "not applicable to abstract functions" in diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index 4612b44b96..5f74a71c4a 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -75,7 +75,7 @@ let t_hoareF_fun_def_r tc = let hf = tc1_as_hoareF tc in let f = NormMp.norm_xfun env hf.hf_f in check_concrete !!tc env f; - let (memenv, (fsig, fdef), env) = Fun.hoareS f env in + let (memenv, (fsig, fdef), env) = Fun.hoareS hf.hf_m f env in let m = EcMemory.memory memenv in let fres = odfl f_tt (omap (form_of_expr m) fdef.f_ret) in let post = PVM.subst1 env pv_res m fres hf.hf_po in @@ -89,7 +89,7 @@ let t_ehoareF_fun_def_r tc = let hf = tc1_as_ehoareF tc in let f = NormMp.norm_xfun env hf.ehf_f in check_concrete !!tc env f; - let (memenv, (fsig, fdef), env) = Fun.hoareS f env in + let (memenv, (fsig, fdef), env) = Fun.hoareS mhr f env in let m = EcMemory.memory memenv in let fres = odfl f_tt (omap (form_of_expr m) fdef.f_ret) in let post = PVM.subst1 env pv_res m fres hf.ehf_po in @@ -103,7 +103,7 @@ let t_bdhoareF_fun_def_r tc = let bhf = tc1_as_bdhoareF tc in let f = NormMp.norm_xfun env bhf.bhf_f in check_concrete !!tc env f; - let (memenv, (fsig, fdef), env) = Fun.hoareS f env in + let (memenv, (fsig, fdef), env) = Fun.hoareS mhr f env in let m = EcMemory.memory memenv in let fres = odfl f_tt (omap (form_of_expr m) fdef.f_ret) in let post = PVM.subst1 env pv_res m fres bhf.bhf_po in From 6d9c23c56cd7b73bb74cce5f55e0ef9e9061aa69 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Mon, 31 Mar 2025 18:13:22 +0100 Subject: [PATCH 07/26] Breaking everything, and I don't know why --- src/ecTyping.ml | 1 + src/phl/ecPhlFun.ml | 1 + 2 files changed, 2 insertions(+) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 2b2a4aca66..6fb441b76f 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3450,6 +3450,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let fpath = trans_gamepath env gp in (* TODO: Make mhr a fresh memory instead *) + let mhr = EcIdent.create "&foo" in let penv, qenv = EcEnv.Fun.hoareF mhr fpath env in let pre' = transf penv pre in let post' = transf qenv post in diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index 5f74a71c4a..5e1c717cf1 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -73,6 +73,7 @@ let subst_pre env fs (m : memory) s = let t_hoareF_fun_def_r tc = let env = FApi.tc1_env tc in let hf = tc1_as_hoareF tc in + assert (hf.hf_m <> mhr); let f = NormMp.norm_xfun env hf.hf_f in check_concrete !!tc env f; let (memenv, (fsig, fdef), env) = Fun.hoareS hf.hf_m f env in From aa0daf6a0b46244d3ba5fb50f9bae93b9538d8bd Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 4 Apr 2025 13:19:13 +0100 Subject: [PATCH 08/26] attempt at fix --- src/ecSubst.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/ecSubst.ml b/src/ecSubst.ml index 6db712f800..921a407c6e 100644 --- a/src/ecSubst.ml +++ b/src/ecSubst.ml @@ -529,14 +529,13 @@ let rec subst_form (s : subst) (f : form) = let ty = subst_ty s f.f_ty in f_op p tys ty - | FhoareF { hf_pr; hf_f; hf_po } -> + | FhoareF { hf_m; hf_pr; hf_f; hf_po } -> let hf_pr, hf_po = - let s = add_memory s mhr mhr in let hf_pr = subst_form s hf_pr in let hf_po = subst_form s hf_po in (hf_pr, hf_po) in let hf_f = subst_xpath s hf_f in - f_hoareF mhr hf_pr hf_f hf_po + f_hoareF hf_m hf_pr hf_f hf_po | FhoareS { hs_m; hs_pr; hs_s; hs_po } -> let hs_m, (hs_pr, hs_po) = From 533ae8882bef51a065aa62a82235d0532ace052f Mon Sep 17 00:00:00 2001 From: Cameron Low Date: Fri, 4 Apr 2025 15:17:54 +0100 Subject: [PATCH 09/26] fix subst? --- src/ecCoreSubst.ml | 3 +-- src/ecTyping.ml | 2 +- src/phl/ecPhlFun.ml | 2 +- 3 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml index cfe8ac141d..adc2027f7a 100644 --- a/src/ecCoreSubst.ml +++ b/src/ecCoreSubst.ml @@ -452,10 +452,9 @@ module Fsubst = struct | FhoareF hf -> let hf_f = x_subst s hf.hf_f in - let s = f_rem_mem s mhr in let hf_pr = f_subst ~tx s hf.hf_pr in let hf_po = f_subst ~tx s hf.hf_po in - f_hoareF mhr hf_pr hf_f hf_po + f_hoareF hf.hf_m hf_pr hf_f hf_po | FhoareS hs -> let hs_s = s_subst s hs.hs_s in diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 6fb441b76f..bdd900fc5d 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3450,7 +3450,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let fpath = trans_gamepath env gp in (* TODO: Make mhr a fresh memory instead *) - let mhr = EcIdent.create "&foo" in + (* let mhr = EcIdent.create "&" in *) let penv, qenv = EcEnv.Fun.hoareF mhr fpath env in let pre' = transf penv pre in let post' = transf qenv post in diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index 5e1c717cf1..a5810525a8 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -73,7 +73,7 @@ let subst_pre env fs (m : memory) s = let t_hoareF_fun_def_r tc = let env = FApi.tc1_env tc in let hf = tc1_as_hoareF tc in - assert (hf.hf_m <> mhr); + (* assert (hf.hf_m <> mhr); *) let f = NormMp.norm_xfun env hf.hf_f in check_concrete !!tc env f; let (memenv, (fsig, fdef), env) = Fun.hoareS hf.hf_m f env in From d9923e79b11b45f5d9cae72142f0a4a63de34fb9 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 11 Apr 2025 12:42:34 +0100 Subject: [PATCH 10/26] fix unroll for --- src/ecTyping.ml | 2 +- src/phl/ecPhlLoopTx.ml | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index bdd900fc5d..6fb441b76f 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3450,7 +3450,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let fpath = trans_gamepath env gp in (* TODO: Make mhr a fresh memory instead *) - (* let mhr = EcIdent.create "&" in *) + let mhr = EcIdent.create "&foo" in let penv, qenv = EcEnv.Fun.hoareF mhr fpath env in let pre' = transf penv pre in let post' = transf qenv post in diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 973fe8a140..81e82eca28 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -223,7 +223,7 @@ let process_splitwhile (b, side, cpos) tc = let process_unroll_for side cpos tc = let env = FApi.tc1_env tc in let hyps = FApi.tc1_hyps tc in - let _, c = EcLowPhlGoal.tc1_get_stmt side tc in + let (goal_m, _), c = EcLowPhlGoal.tc1_get_stmt side tc in if not (List.is_empty (fst cpos)) then tc_error !!tc "cannot use deep code position"; @@ -260,18 +260,18 @@ let process_unroll_for side cpos tc = (* Apply loop increment *) let incrz = - let fincr = form_of_expr mhr eincr in + let fincr = form_of_expr goal_m eincr in fun z0 -> - let f = PVM.subst1 env x mhr (f_int z0) fincr in + let f = PVM.subst1 env x goal_m (f_int z0) fincr in match (simplify full_red hyps f).f_node with | Fint z0 -> z0 | _ -> tc_error !!tc "loop increment does not reduce to a constant" in (* Evaluate loop guard *) let test_cond = - let ftest = form_of_expr mhr t in + let ftest = form_of_expr goal_m t in fun z0 -> - let cond = PVM.subst1 env x mhr (f_int z0) ftest in + let cond = PVM.subst1 env x goal_m (f_int z0) ftest in match sform_of_form (simplify full_red hyps cond) with | SFtrue -> true | SFfalse -> false @@ -284,7 +284,7 @@ let process_unroll_for side cpos tc = let zs = eval_cond z0 in let hds = Array.make (List.length zs) None in let m = LDecl.fresh_id hyps "&m" in - let x = f_pvar x tint mhr in + let x = f_pvar x tint goal_m in let t_set i pos z tc = hds.(i) <- Some (FApi.tc1_handle tc, pos, z); t_id tc in From 001abf105ca8217a2c85d306732b9a81786cc767 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 6 May 2025 11:17:12 +0100 Subject: [PATCH 11/26] fix subst in conseq --- src/ecTyping.ml | 2 +- src/phl/ecPhlConseq.ml | 8 ++++++-- src/phl/ecPhlFun.ml | 2 +- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 6fb441b76f..b3d079549d 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3450,7 +3450,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let fpath = trans_gamepath env gp in (* TODO: Make mhr a fresh memory instead *) - let mhr = EcIdent.create "&foo" in + (*let mhr = EcIdent.create "&foo" in*) let penv, qenv = EcEnv.Fun.hoareF mhr fpath env in let pre' = transf penv pre in let post' = transf qenv post in diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index f8f2d03172..bad715b0c7 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -1164,10 +1164,10 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = Some ((_, f2) as nf2), Some ((_, f3) as nf3) -> - let subst1 = Fsubst.f_subst_mem mhr mleft in - let subst2 = Fsubst.f_subst_mem mhr mright in let hs2 = pf_as_hoareF !!tc f2 in let hs3 = pf_as_hoareF !!tc f3 in + let subst1 = Fsubst.f_subst_mem hs2.hf_m mleft in + let subst2 = Fsubst.f_subst_mem hs3.hf_m mright in let pre = f_ands [ef.ef_pr; subst1 hs2.hf_pr; subst2 hs3.hf_pr] in let post = f_ands [ef.ef_po; subst1 hs2.hf_po; subst2 hs3.hf_po] in let tac = if notmod then t_equivF_conseq_nm else t_equivF_conseq in @@ -1183,12 +1183,14 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (* ------------------------------------------------------------------ *) (* equivF / ? / ? / ⊥ *) | FequivF ef, Some _, Some _, None -> + (*let mhr = EcIdent.create "&foo" in*) let f3 = f_hoareF mhr f_true ef.ef_fr f_true in t_hi_conseq notmod f1 f2 (Some (None, f3)) tc (* ------------------------------------------------------------------ *) (* equivF / ? / ⊥ / ? *) | FequivF ef, Some _, None, Some _ -> + (*let mhr = EcIdent.create "&foo" in*) let f2 = f_hoareF mhr f_true ef.ef_fl f_true in t_hi_conseq notmod f1 (Some (None, f2)) f3 tc @@ -1383,6 +1385,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) | FequivF ef -> let f = sideif side ef.ef_fl ef.ef_fr in + (*let mhr = EcIdent.create "&foo" in*) (*Doing this makes conseq fail to eliminate first goal*) let penv, qenv = LDecl.hoareF mhr f hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; @@ -1392,6 +1395,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) | FequivS es -> let f = sideif side es.es_sl es.es_sr in let m = sideif side es.es_ml es.es_mr in + (*let mhr = EcIdent.create "&foo" in*) let m = (mhr, snd m) in let env = LDecl.push_active m hyps in let fmake pre post c_or_bd = diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index a5810525a8..c71cff9a04 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -73,7 +73,7 @@ let subst_pre env fs (m : memory) s = let t_hoareF_fun_def_r tc = let env = FApi.tc1_env tc in let hf = tc1_as_hoareF tc in - (* assert (hf.hf_m <> mhr); *) + (*assert (hf.hf_m <> mhr);*) let f = NormMp.norm_xfun env hf.hf_f in check_concrete !!tc env f; let (memenv, (fsig, fdef), env) = Fun.hoareS hf.hf_m f env in From 36d9900bac2c8f38d4de4e72f55d58f36d9ffb36 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Wed, 7 May 2025 14:14:14 +0100 Subject: [PATCH 12/26] maybe subst later? --- src/phl/ecPhlConseq.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index bad715b0c7..55c52cd8dd 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -926,6 +926,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = as_seq4 (LDecl.fresh_ids (FApi.tc1_hyps tc) ["&m";"_";"_";"_"]) in let pre = f_and hs.bhs_pr hs2.hs_pr in let mpre = Fsubst.f_subst_mem mhr m pre in + (*let mpre = Fsubst.f_subst_mem (fst hs2.hs_m) m mpre in*) let post1 = hs0.bhs_po in let post = hs.bhs_po in let posta = f_and post hs2.hs_po in @@ -1183,14 +1184,14 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (* ------------------------------------------------------------------ *) (* equivF / ? / ? / ⊥ *) | FequivF ef, Some _, Some _, None -> - (*let mhr = EcIdent.create "&foo" in*) + let mhr = EcIdent.create "&foo" in let f3 = f_hoareF mhr f_true ef.ef_fr f_true in t_hi_conseq notmod f1 f2 (Some (None, f3)) tc (* ------------------------------------------------------------------ *) (* equivF / ? / ⊥ / ? *) | FequivF ef, Some _, None, Some _ -> - (*let mhr = EcIdent.create "&foo" in*) + let mhr = EcIdent.create "&foo" in let f2 = f_hoareF mhr f_true ef.ef_fl f_true in t_hi_conseq notmod f1 (Some (None, f2)) f3 tc @@ -1378,6 +1379,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) | FequivF ef when side = `Left -> ef.ef_fr, f_true, f_true | _ -> bhf.bhf_f, bhf.bhf_pr, bhf.bhf_po in + (*let mhr = EcIdent.create "&foo" in*) let penv, qenv = LDecl.hoareF mhr f hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; f_hoareF mhr pre f post in @@ -1385,7 +1387,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) | FequivF ef -> let f = sideif side ef.ef_fl ef.ef_fr in - (*let mhr = EcIdent.create "&foo" in*) (*Doing this makes conseq fail to eliminate first goal*) + let mhr = EcIdent.create "&foo" in let penv, qenv = LDecl.hoareF mhr f hyps in let fmake pre post c_or_bd = ensure_none c_or_bd; @@ -1395,7 +1397,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) | FequivS es -> let f = sideif side es.es_sl es.es_sr in let m = sideif side es.es_ml es.es_mr in - (*let mhr = EcIdent.create "&foo" in*) + let mhr = EcIdent.create "&foo" in let m = (mhr, snd m) in let env = LDecl.push_active m hyps in let fmake pre post c_or_bd = From 7cf7de42ce3bcb45a4d4a53eb75f5a3d24036b52 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Wed, 21 May 2025 14:39:25 +0100 Subject: [PATCH 13/26] fix conseq --- src/phl/ecPhlConseq.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index 55c52cd8dd..02fbefe757 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -654,10 +654,10 @@ let t_equivS_conseq_conj pre1 post1 pre2 post2 pre' post' tc = FApi.xmutate1 tc `HlConseqConj [concl1; concl2; concl3] (* -------------------------------------------------------------------- *) -let t_equivF_conseq_conj pre1 post1 pre2 post2 pre' post' tc = +let t_equivF_conseq_conj ml mr pre1 post1 pre2 post2 pre' post' tc = let ef = tc1_as_equivF tc in - let subst1 = Fsubst.f_subst_mem mhr mleft in - let subst2 = Fsubst.f_subst_mem mhr mright in + let subst1 = Fsubst.f_subst_mem ml mleft in + let subst2 = Fsubst.f_subst_mem mr mright in let pre1' = subst1 pre1 in let post1' = subst1 post1 in let pre2' = subst2 pre2 in @@ -666,8 +666,8 @@ let t_equivF_conseq_conj pre1 post1 pre2 post2 pre' post' tc = tc_error !!tc "invalid pre-condition"; if not (f_equal ef.ef_po (f_ands [post';post1';post2'])) then tc_error !!tc "invalid post-condition"; - let concl1 = f_hoareF mhr pre1 ef.ef_fl post1 in - let concl2 = f_hoareF mhr pre2 ef.ef_fr post2 in + let concl1 = f_hoareF ml pre1 ef.ef_fl post1 in + let concl2 = f_hoareF mr pre2 ef.ef_fr post2 in let concl3 = f_equivF pre' ef.ef_fl ef.ef_fr post' in FApi.xmutate1 tc `HlConseqConj [concl1; concl2; concl3] @@ -1177,7 +1177,7 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = (tac pre post) (FApi.t_seqsub (t_equivF_conseq_conj - hs2.hf_pr hs2.hf_po hs3.hf_pr hs3.hf_po ef.ef_pr ef.ef_po) + hs2.hf_m hs3.hf_m hs2.hf_pr hs2.hf_po hs3.hf_pr hs3.hf_po ef.ef_pr ef.ef_po) [t_apply_r nf2; t_apply_r nf3; t_apply_r nf1]) tc From 384818021f657f85e0d92aba7aebfb32f4ca6a06 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 23 May 2025 09:41:25 +0100 Subject: [PATCH 14/26] add internal debug tactical --- src/ecLowGoal.ml | 10 +++++----- src/ecLowGoal.mli | 7 +++++++ 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 6643c8e3cd..4a88bc5a2e 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -2290,6 +2290,11 @@ type cstate = { cs_sbeq : Sid.t; } +let t_debug ?(tag="") t tc = + Format.eprintf "%s" tag; + pp_tc (FApi.tcenv_of_tcenv1 tc); + t tc + let t_crush ?(delta = true) ?tsolve (tc : tcenv1) = let dtsolve = @@ -2299,11 +2304,6 @@ let t_crush ?(delta = true) ?tsolve (tc : tcenv1) = let tt = FApi.t_try (t_assumption `Alpha) in -(* let t_print s t tc = - Format.eprintf "%s@." s; - pp_tc (FApi.tcenv_of_tcenv1 tc); - t tc in *) - (* Entry of progress: simplify goal, and chain with progress *) let rec entry (st : cstate) = t_simplify ~delta:`No @! aux0 st diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index 2f03d513e6..358cdcc245 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -351,3 +351,10 @@ val t_solve : -> ?mode:EcMatching.fmoptions -> ?depth:int -> FApi.backward + +(* -------------------------------------------------------------------- *) +val t_debug : + ?tag:string (* for distinguishing prints *) + -> FApi.backward + -> FApi.backward +[@@ocaml.alert debug "Debug function, remove uses before merging"] From 78b9c7ca121be88d9641e69ada3db21af6cd4eab Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 23 May 2025 14:01:34 +0100 Subject: [PATCH 15/26] better debug --- src/ecLowGoal.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 4a88bc5a2e..0fcdb465cf 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -2291,9 +2291,12 @@ type cstate = { } let t_debug ?(tag="") t tc = - Format.eprintf "%s" tag; + Format.eprintf "Before (tag: %s):" tag; pp_tc (FApi.tcenv_of_tcenv1 tc); - t tc + let r = t tc in + Format.eprintf "After (tag: %s):" tag; + pp_tc r; + r let t_crush ?(delta = true) ?tsolve (tc : tcenv1) = From 699816b03353c4fe98570a977723e8f5df5de271 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 23 May 2025 14:01:59 +0100 Subject: [PATCH 16/26] hoare call --- src/phl/ecPhlCall.ml | 15 +++++++++------ src/phl/ecPhlCall.mli | 3 ++- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 07c49ce23a..ac5005a261 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -56,14 +56,17 @@ let wp2_call f_anda_simpl (PVM.subst env spre fpre) post (* -------------------------------------------------------------------- *) -let t_hoare_call fpre fpost tc = +let t_hoare_call fm fpre fpost tc = let env = FApi.tc1_env tc in let hs = tc1_as_hoareS tc in let (lp,f,args),s = tc1_last_call tc hs.hs_s in let m = EcMemory.memory hs.hs_m in let fsig = (Fun.by_xpath f env).f_sig in (* The function satisfies the specification *) - let f_concl = f_hoareF mhr fpre f fpost in + let f_concl = f_hoareF fm fpre f fpost in + (* substitute memories *) + let fpre = Fsubst.f_subst_mem fm m fpre in + let fpost = Fsubst.f_subst_mem fm m fpost in (* The wp *) let pvres = pv_res in let vres = EcIdent.create "result" in @@ -308,7 +311,7 @@ let t_call side ax tc = let (_, f, _), _ = tc1_last_call tc hs.hs_s in if not (EcEnv.NormMp.x_equal env hf.hf_f f) then call_error env tc hf.hf_f f; - t_hoare_call hf.hf_pr hf.hf_po tc + t_hoare_call hf.hf_m hf.hf_pr hf.hf_po tc | FeHoareF hf, FeHoareS hs -> let (_, f, _), _ = tc1_last_call tc hs.ehs_s in @@ -390,8 +393,8 @@ let process_call side info tc = match concl.f_node, side with | FhoareS hs, None -> let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in - let penv, qenv = LDecl.hoareF mhr f hyps in - (penv, qenv, tbool, fun pre post -> f_hoareF mhr pre f post) + let penv, qenv = LDecl.hoareF (fst hs.hs_m) f hyps in + (penv, qenv, tbool, fun pre post -> f_hoareF (fst hs.hs_m) pre f post) | FbdHoareS bhs, None -> let (_,f,_) = fst (tc1_last_call tc bhs.bhs_s) in @@ -431,7 +434,7 @@ let process_call side info tc = | FhoareS hs -> let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in let penv = LDecl.inv_memenv1 hyps in - (penv, tbool, fun inv -> f_hoareF mhr inv f inv) + (penv, tbool, fun inv -> f_hoareF (fst hs.hs_m) inv f inv) | FeHoareS hs -> let (_,f,_) = fst (tc1_last_call tc hs.ehs_s) in diff --git a/src/phl/ecPhlCall.mli b/src/phl/ecPhlCall.mli index 1242522d1c..de4113558f 100644 --- a/src/phl/ecPhlCall.mli +++ b/src/phl/ecPhlCall.mli @@ -2,6 +2,7 @@ open EcParsetree open EcFol open EcCoreGoal.FApi +open EcMemory (* -------------------------------------------------------------------- *) val wp2_call : @@ -13,7 +14,7 @@ val wp2_call : -> EcMemory.memory -> EcMemory.memory -> form -> EcEnv.LDecl.hyps -> form -val t_hoare_call : form -> form -> backward +val t_hoare_call : memory -> form -> form -> backward val t_bdhoare_call : form -> form -> form option -> backward val t_equiv_call : form -> form -> backward val t_equiv_call1 : side -> form -> form -> backward From 8131c841efe67e96373dc893971c55d72ce842d4 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 23 May 2025 14:35:27 +0100 Subject: [PATCH 17/26] proc * --- src/phl/ecPhlFun.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index c71cff9a04..46e3b0dc6b 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -419,9 +419,9 @@ let t_fun_to_code_hoare_r tc = let env = FApi.tc1_env tc in let hf = tc1_as_hoareF tc in let f = hf.hf_f in - let m, st, r, a = ToCodeLow.to_code env f mhr in - let spr = ToCodeLow.add_var_tuple env pv_arg mhr a m PVM.empty in - let spo = ToCodeLow.add_var env pv_res mhr r m PVM.empty in + let m, st, r, a = ToCodeLow.to_code env f hf.hf_m in + let spr = ToCodeLow.add_var_tuple env pv_arg hf.hf_m a m PVM.empty in + let spo = ToCodeLow.add_var env pv_res hf.hf_m r m PVM.empty in let pre = PVM.subst env spr hf.hf_pr in let post = PVM.subst env spo hf.hf_po in let concl = f_hoareS m pre st post in From e8d4ca6d5f27ab22598aa33814a969eeb642a675 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Sun, 25 May 2025 17:32:37 +0100 Subject: [PATCH 18/26] fix conseq more --- src/phl/ecPhlConseq.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index 02fbefe757..f41cf10696 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -851,7 +851,6 @@ let rec t_hi_conseq notmod f1 f2 f3 tc = -> let hs2 = pf_as_hoareF !!tc f2 in let tac = if notmod then t_hoareF_conseq_nm else t_hoareF_conseq in - t_on1seq 2 (tac (f_and hs.hf_pr hs2.hf_pr) (f_and hs.hf_po hs2.hf_po)) (FApi.t_seqsub @@ -1348,7 +1347,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3) in let penv, qenv = LDecl.hoareF m f hyps in let fmake pre post c_or_bd = - ensure_none c_or_bd; f_hoareF mhr pre f post in + ensure_none c_or_bd; f_hoareF hf.hf_m pre f post in (penv, qenv, pr, po, tbool, fmake) | FeHoareF hf -> From 517dd3c310544af81090e04ae6922cfcf9f96ebb Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Mon, 26 May 2025 13:16:46 +0100 Subject: [PATCH 19/26] fresh memory in trans --- src/ecTyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index b3d079549d..deaf38d2aa 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3450,7 +3450,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let fpath = trans_gamepath env gp in (* TODO: Make mhr a fresh memory instead *) - (*let mhr = EcIdent.create "&foo" in*) + let mhr = EcIdent.create "&frmtrans" in let penv, qenv = EcEnv.Fun.hoareF mhr fpath env in let pre' = transf penv pre in let post' = transf qenv post in From c28855e0d0a9911311b9657a671c222ccba1f6b6 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 27 May 2025 09:12:17 +0200 Subject: [PATCH 20/26] WIP --- src/ecSmt.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ecSmt.ml b/src/ecSmt.ml index 6d81016c62..0afea1b793 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -693,11 +693,11 @@ and trans_form ((genv, lenv) as env : tenv * lenv) (fp : form) = | Fglob (m,mem) -> trans_glob env m mem - | Fpr pr -> trans_pr env pr + | Fpr pr -> trans_pr env pr | FeagerF _ | FhoareF _ | FhoareS _ - | FeHoareF _ | FeHoareS _ + | FeHoareF _ | FeHoareS _ | FbdHoareF _ | FbdHoareS _ | FequivF _ | FequivS _ -> trans_gen env fp From 21ddbb8e05222c310758849c5bcd900523d8b717 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 27 May 2025 10:36:42 +0200 Subject: [PATCH 21/26] WIP --- src/ecEnv.ml | 27 ++--- src/ecEnv.mli | 6 +- src/ecPrinting.ml | 14 ++- src/phl/ecPhlCall.ml | 12 +- src/phl/ecPhlFun.ml | 4 +- theories/crypto/#Birthday.eca# | 198 +++++++++++++++++++++++++++++++++ theories/crypto/.#Birthday.eca | 1 + theories/crypto/Birthday.eca | 19 +++- 8 files changed, 249 insertions(+), 32 deletions(-) create mode 100644 theories/crypto/#Birthday.eca# create mode 120000 theories/crypto/.#Birthday.eca diff --git a/src/ecEnv.ml b/src/ecEnv.ml index c4d952350c..6c1152890b 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -1675,15 +1675,16 @@ module Fun = struct let locals = List.map ovar_of_var fd.f_locals in (fun_.f_sig,fd), adds_in_memenv mem locals - let inv_memory side = - let id = if side = `Left then EcCoreFol.mleft else EcCoreFol.mright in - EcMemory.abstract id + let inv_memory (side : [`Left | `Right]) = + match side with + | `Left -> EcMemory.abstract EcCoreFol.mleft + | `Right -> EcMemory.abstract EcCoreFol.mright - let inv_memenv env = - Memory.push_all [inv_memory `Left; inv_memory `Rigth] env + let inv_memenv ?(mem = [mleft; mright]) env = + Memory.push_all (List.map EcMemory.abstract mem) env - let inv_memenv1 env = - let mem = EcMemory.abstract EcCoreFol.mhr in + let inv_memenv1 ?(mem = EcCoreFol.mhr) env = + let mem = EcMemory.abstract mem in Memory.push_active mem env let prF_memenv m path env = @@ -3569,17 +3570,17 @@ module LDecl = struct (* Note: Not confident about this change. I don't understand what this function does *) let hoareF mem xp lenv = let env1, env2 = Fun.hoareF mem xp lenv.le_env in - { lenv with le_env = env1}, {lenv with le_env = env2 } + { lenv with le_env = env1 }, { lenv with le_env = env2 } let equivF xp1 xp2 lenv = let env1, env2 = Fun.equivF xp1 xp2 lenv.le_env in - { lenv with le_env = env1}, {lenv with le_env = env2 } + { lenv with le_env = env1 }, { lenv with le_env = env2 } - let inv_memenv lenv = - { lenv with le_env = Fun.inv_memenv lenv.le_env } + let inv_memenv ?mem lenv = + { lenv with le_env = Fun.inv_memenv ?mem lenv.le_env } - let inv_memenv1 lenv = - { lenv with le_env = Fun.inv_memenv1 lenv.le_env } + let inv_memenv1 ?mem lenv = + { lenv with le_env = Fun.inv_memenv1 ?mem lenv.le_env } end diff --git a/src/ecEnv.mli b/src/ecEnv.mli index de04b9f578..a77567cf0a 100644 --- a/src/ecEnv.mli +++ b/src/ecEnv.mli @@ -108,7 +108,7 @@ module Fun : sig val inv_memory : [`Left|`Right] -> memenv - val inv_memenv : env -> env + val inv_memenv : ?mem:(memory list) -> env -> env val equivF_memenv : xpath -> xpath -> env -> (memenv * memenv) * (memenv * memenv) @@ -505,8 +505,8 @@ module LDecl : sig val hoareF : memory -> xpath -> hyps -> hyps * hyps val equivF : xpath -> xpath -> hyps -> hyps * hyps - val inv_memenv : hyps -> hyps - val inv_memenv1 : hyps -> hyps + val inv_memenv : ?mem:(memory list) -> hyps -> hyps + val inv_memenv1 : ?mem:memory -> hyps -> hyps end val pp_debug_form : (env -> Format.formatter -> form -> unit) ref diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index a21efd285a..4cb81d72aa 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -787,14 +787,14 @@ let pp_stype (ppe : PPEnv.t) (fmt : Format.formatter) (ty : ty) = pp_type_r ppe ((1 + fst t_prio_tpl, `NonAssoc), `NonAssoc) fmt ty (* -------------------------------------------------------------------- *) -let pp_mem (ppe : PPEnv.t) (fmt : Format.formatter) (x : memory) = +let pp_mem (ppe : PPEnv.t) (fmt : Format.formatter) (x as id : memory) = let x = Format.sprintf "%s" (PPEnv.local_symb ppe x) in let x = if x <> "" && x.[0] = '&' then String.sub x 1 (String.length x - 1) else x in - Format.fprintf fmt "%s" x + Format.fprintf fmt "%s<%s>" x (EcIdent.tostring id) let pp_memtype (ppe : PPEnv.t) (fmt : Format.formatter) (mt : memtype) = match EcMemory.for_printing mt with @@ -1811,7 +1811,7 @@ and pp_form_core_r Format.fprintf fmt "%a{%s%a}" (pp_pv ppe) x (if force then "!" else "") (pp_mem ppe) i in - let force = + let force = true || match x with | PVloc x -> Ssym.mem x ppe.ppe_inuse | PVglob _ -> false in @@ -1889,15 +1889,17 @@ and pp_form_core_r let mepr, mepo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f ppe.PPEnv.ppe_env in let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in - Format.fprintf fmt "hoare[@[@ %a :@ @[%a ==>@ %a@]@]]" + Format.fprintf fmt "hoare[@[@ %a {%a} :@ @[%a ==>@ %a@]@]]" (pp_funname ppe) hf.hf_f + (pp_mem ppe) hf.hf_m (pp_form ppepr) hf.hf_pr (pp_form ppepo) hf.hf_po | FhoareS hs -> let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in - Format.fprintf fmt "hoare[@[@ %a :@ @[%a ==>@ %a@]@]]" + Format.fprintf fmt "hoare[@[@ %a {%a} :@ @[%a ==>@ %a@]@]]" (pp_stmt_for_form ppe) hs.hs_s + (pp_mem ppe) (fst hs.hs_m) (pp_form ppe) hs.hs_pr (pp_form ppe) hs.hs_po @@ -2908,7 +2910,7 @@ let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf = let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) hf.hf_pr; - Format.fprintf fmt " %a@\n%!" (pp_funname ppe) hf.hf_f; + Format.fprintf fmt " %a {%a}@\n%!" (pp_funname ppe) hf.hf_f (pp_mem ppe) hf.hf_m; Format.fprintf fmt "@\n%a%!" (pp_post ppepo ?prpo) hf.hf_po (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index ac5005a261..66dadbaf26 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -387,7 +387,7 @@ let mk_inv_spec (_pf : proofenv) env inv fl fr = let post = f_and eq_res inv in f_equivF pre fl fr post -let process_call side info tc = +let process_call (side : side option) (info : call_info gppterm) (tc : tcenv1) = let process_spec tc side = let (hyps, concl) = FApi.tc1_flat tc in match concl.f_node, side with @@ -433,7 +433,7 @@ let process_call side info tc = match concl.f_node with | FhoareS hs -> let (_,f,_) = fst (tc1_last_call tc hs.hs_s) in - let penv = LDecl.inv_memenv1 hyps in + let penv = LDecl.inv_memenv1 ~mem:(fst hs.hs_m) hyps in (penv, tbool, fun inv -> f_hoareF (fst hs.hs_m) inv f inv) | FeHoareS hs -> @@ -521,11 +521,15 @@ let process_call side info tc = tc_error !!tc "cannot infer all placeholders"; PT.concretize pt in + let ppe = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in + + Format.eprintf "@.@.[W]%a@." (EcPrinting.pp_form ppe) ax; + FApi.t_seqsub (t_call side ax) [FApi.t_seqs - [EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt; - !subtactic; t_trivial]; + [EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt] +(* !subtactic; t_trivial]; *); t_id] tc diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index 46e3b0dc6b..6bb227593a 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -523,12 +523,12 @@ let t_fun_to_code_r tc = let t_fun_to_code = FApi.t_low0 "fun-to-code" t_fun_to_code_r (* -------------------------------------------------------------------- *) -let t_fun_r inv tc = +let t_fun_r ?mem inv tc = let th tc = let env = FApi.tc1_env tc in let h = destr_hoareF (FApi.tc1_goal tc) in if NormMp.is_abstract_fun h.hf_f env - then t_hoareF_abs inv tc + then t_hoareF_abs ?mem inv tc else t_hoareF_fun_def tc and teh tc = diff --git a/theories/crypto/#Birthday.eca# b/theories/crypto/#Birthday.eca# new file mode 100644 index 0000000000..94e24bd873 --- /dev/null +++ b/theories/crypto/#Birthday.eca# @@ -0,0 +1,198 @@ +(* -------------------------------------------------------------------- *) +require import AllCore List Distr Ring. +require import StdRing StdOrder StdBigop FelTactic. +require (*--*) Mu_mem. +(*---*) import RField IntOrder RealOrder. + +(* Clone Parameters *) +(** A type T equipped with a distribution **) +type T. + +op uT: T distr. + +(* -------------------------------------------------------------------- *) + +(** A non-negative integer q **) +op q : { int | 0 <= q } as ge0_q. + +op maxu : T = mode uT. + +lemma maxuP x: mu1 uT x <= mu1 uT maxu by apply mode_ge. + +(** A module that samples in uT on queries to s **) +module Sample = { + var l:T list + + proc init(): unit = { + l <- []; + } + + proc s(): T = { + var r; + + r <$ uT; + l <- r::l; + return r; + } +}. + +module type Sampler = { + proc init(): unit + proc s(): T +}. + +(** Adversaries that may query an s oracle **) +module type ASampler = { + proc s(): T +}. + +module type Adv(S:ASampler) = { + proc a(): unit +}. + +(** And an experiment that initializes the sampler and runs the adversary **) +module Exp(S:Sampler,A:Adv) = { + module A = A(S) + + proc main(): unit = { + S.init(); + A.a(); + } +}. + +(** Forall adversary A that makes at most q queries to its s oracle, + the probability that the same output is sampled twice is bounded + by q^2/|T| **) +section. + declare module A <: Adv {-Sample}. + declare axiom A_ll (S <: ASampler {-A}): islossless S.s => islossless A(S).a. + + lemma pr_Sample_le &m: + Pr[Exp(Sample,A).main() @ &m : size Sample.l <= q /\ !uniq Sample.l] + <= (q*(q-1))%r/2%r * mu1 uT maxu. + proof. + fel 1 (size Sample.l) (fun x, x%r * mu1 uT maxu) q (!uniq Sample.l) []=> //. + + by rewrite -Bigreal.BRA.mulr_suml Bigreal.sumidE 1:ge0_q. + + by inline*; auto. + + proc;wp; rnd (mem Sample.l); skip=> // /> &hr ???. + apply (Mu_mem.mu_mem_le_size (Sample.l{hr}) uT (mu1 uT maxu)). + by move=> x _;rewrite maxuP. + by move=> c; proc; auto=> /#. + qed. + + lemma pr_Sample_le_q2 &m: + Pr[Exp(Sample,A).main() @ &m: size Sample.l <= q /\ !uniq Sample.l] + <= (q^2)%r * mu1 uT maxu. + proof. + apply (ler_trans _ _ _ (pr_Sample_le &m)). + apply ler_wpmul2r; 1: by apply ge0_mu. + have -> : q^2 = q*q by ring. + smt(ge0_q). + qed. + + declare axiom A_bounded: hoare [A(Sample).a : size Sample.l = 0 ==> size Sample.l <= q]. + + local lemma aux &m : + Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] = + Pr[Exp(Sample,A).main() @ &m: size Sample.l <= q /\ !uniq Sample.l]. + proof. + byequiv (_: ={glob A} ==> ={Sample.l} /\ size Sample.l{2} <= q)=> //=. + conseq (_: _ ==> ={Sample.l}) _ (_: _ ==> size Sample.l <= q)=> //=;2:by sim. + (*by proc;call A_bounded;inline *;auto.*) admit. + qed. + + lemma pr_collision &m: + Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] + <= (q*(q-1))%r/2%r* mu1 uT maxu. + proof. rewrite (aux &m); apply (pr_Sample_le &m). qed. + + lemma pr_collision_q2 &m: + Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] + <= (q^2)%r * mu1 uT maxu. + proof. rewrite (aux &m); apply (pr_Sample_le_q2 &m). qed. + +end section. + +(*** The same result using a bounding module ***) +module Bounder(S:Sampler) = { + var c:int + + proc init(): unit = { + S.init(); + c <- 0; + } + + proc s(): T = { + var r <- witness; + + if (c < q) { + r <@ S.s(); + c <- c + 1; + } + return r; + } +}. + +module ABounder(S:ASampler) = { + proc s(): T = { + var r <- witness; + + if (Bounder.c < q) { + r <@ S.s(); + Bounder.c <- Bounder.c + 1; + } + return r; + } +}. + +module Bounded(A:Adv,S:ASampler) = { + proc a(): unit = { + Bounder.c <- 0; + A(ABounder(S)).a(); + } +}. + +equiv PushBound (S <: Sampler {-Bounder}) (A <: Adv {-S,-Bounder}): + Exp(Bounder(S),A).main ~ Exp(S,Bounded(A)).main: + ={glob A,glob S} ==> + ={glob A,glob S}. +proof. by proc; inline*; sim. qed. + +(** Forall adversary A with access to the bounded s oracle, the + probability that the same output is sampled twice is bounded by + q^2/|T| **) +section. + declare module A <: Adv {-Sample,-Bounder}. + + declare axiom A_ll (S <: ASampler {-A}): islossless S.s => islossless A(S).a. + + lemma pr_collision_bounded_oracles &m: + Pr[Exp(Bounder(Sample),A).main() @ &m: !uniq Sample.l] + <= (q^2)%r * mu1 uT maxu. + proof. + have ->: Pr[Exp(Bounder(Sample),A).main() @ &m: !uniq Sample.l] = + Pr[Exp(Sample,Bounded(A)).main() @ &m: !uniq Sample.l]. + + byequiv (PushBound Sample A) => //. + apply (pr_collision_q2 (Bounded(A)) _ _ &m). + + move=> S HS;proc;call (A_ll (ABounder(S)) _);2:by auto. + by proc;sp;if;auto;call HS. + proc. +call (_: size Sample.l <= Bounder.c <= q). + + +admit. + +admit. + + proc; sp; if =>//. inline *. + wp. rnd. admit. + + + wp. + + auto. + + smt(ge0_q). + qed. + +end section. + diff --git a/theories/crypto/.#Birthday.eca b/theories/crypto/.#Birthday.eca new file mode 120000 index 0000000000..167b57bd79 --- /dev/null +++ b/theories/crypto/.#Birthday.eca @@ -0,0 +1 @@ +strub@CrapuMac.local.44707:1747731257 \ No newline at end of file diff --git a/theories/crypto/Birthday.eca b/theories/crypto/Birthday.eca index df2cfb3410..65d5579bb7 100644 --- a/theories/crypto/Birthday.eca +++ b/theories/crypto/Birthday.eca @@ -98,7 +98,7 @@ section. proof. byequiv (_: ={glob A} ==> ={Sample.l} /\ size Sample.l{2} <= q)=> //=. conseq (_: _ ==> ={Sample.l}) _ (_: _ ==> size Sample.l <= q)=> //=;2:by sim. - by proc;call A_bounded;inline *;auto. + (*by proc;call A_bounded;inline *;auto.*) admit. qed. lemma pr_collision &m: @@ -176,9 +176,20 @@ section. apply (pr_collision_q2 (Bounded(A)) _ _ &m). + move=> S HS;proc;call (A_ll (ABounder(S)) _);2:by auto. by proc;sp;if;auto;call HS. - proc; call (_: size Sample.l <= Bounder.c <= q). - + proc;sp;if=>//;inline *;auto=> /#. - auto; smt(ge0_q). + proc. +call (_: size Sample.l <= Bounder.c <= q). +admit. + +admit. + + proc; sp; if =>//. inline *. + wp. rnd. admit. + + + wp. + + auto. + + smt(ge0_q). qed. end section. From 1a959e1c622bc6989827badfdba3867b936ebf3d Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 27 May 2025 09:49:13 +0100 Subject: [PATCH 22/26] reset birthday --- theories/crypto/#Birthday.eca# | 198 --------------------------------- theories/crypto/.#Birthday.eca | 1 - theories/crypto/Birthday.eca | 19 +--- 3 files changed, 4 insertions(+), 214 deletions(-) delete mode 100644 theories/crypto/#Birthday.eca# delete mode 120000 theories/crypto/.#Birthday.eca diff --git a/theories/crypto/#Birthday.eca# b/theories/crypto/#Birthday.eca# deleted file mode 100644 index 94e24bd873..0000000000 --- a/theories/crypto/#Birthday.eca# +++ /dev/null @@ -1,198 +0,0 @@ -(* -------------------------------------------------------------------- *) -require import AllCore List Distr Ring. -require import StdRing StdOrder StdBigop FelTactic. -require (*--*) Mu_mem. -(*---*) import RField IntOrder RealOrder. - -(* Clone Parameters *) -(** A type T equipped with a distribution **) -type T. - -op uT: T distr. - -(* -------------------------------------------------------------------- *) - -(** A non-negative integer q **) -op q : { int | 0 <= q } as ge0_q. - -op maxu : T = mode uT. - -lemma maxuP x: mu1 uT x <= mu1 uT maxu by apply mode_ge. - -(** A module that samples in uT on queries to s **) -module Sample = { - var l:T list - - proc init(): unit = { - l <- []; - } - - proc s(): T = { - var r; - - r <$ uT; - l <- r::l; - return r; - } -}. - -module type Sampler = { - proc init(): unit - proc s(): T -}. - -(** Adversaries that may query an s oracle **) -module type ASampler = { - proc s(): T -}. - -module type Adv(S:ASampler) = { - proc a(): unit -}. - -(** And an experiment that initializes the sampler and runs the adversary **) -module Exp(S:Sampler,A:Adv) = { - module A = A(S) - - proc main(): unit = { - S.init(); - A.a(); - } -}. - -(** Forall adversary A that makes at most q queries to its s oracle, - the probability that the same output is sampled twice is bounded - by q^2/|T| **) -section. - declare module A <: Adv {-Sample}. - declare axiom A_ll (S <: ASampler {-A}): islossless S.s => islossless A(S).a. - - lemma pr_Sample_le &m: - Pr[Exp(Sample,A).main() @ &m : size Sample.l <= q /\ !uniq Sample.l] - <= (q*(q-1))%r/2%r * mu1 uT maxu. - proof. - fel 1 (size Sample.l) (fun x, x%r * mu1 uT maxu) q (!uniq Sample.l) []=> //. - + by rewrite -Bigreal.BRA.mulr_suml Bigreal.sumidE 1:ge0_q. - + by inline*; auto. - + proc;wp; rnd (mem Sample.l); skip=> // /> &hr ???. - apply (Mu_mem.mu_mem_le_size (Sample.l{hr}) uT (mu1 uT maxu)). - by move=> x _;rewrite maxuP. - by move=> c; proc; auto=> /#. - qed. - - lemma pr_Sample_le_q2 &m: - Pr[Exp(Sample,A).main() @ &m: size Sample.l <= q /\ !uniq Sample.l] - <= (q^2)%r * mu1 uT maxu. - proof. - apply (ler_trans _ _ _ (pr_Sample_le &m)). - apply ler_wpmul2r; 1: by apply ge0_mu. - have -> : q^2 = q*q by ring. - smt(ge0_q). - qed. - - declare axiom A_bounded: hoare [A(Sample).a : size Sample.l = 0 ==> size Sample.l <= q]. - - local lemma aux &m : - Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] = - Pr[Exp(Sample,A).main() @ &m: size Sample.l <= q /\ !uniq Sample.l]. - proof. - byequiv (_: ={glob A} ==> ={Sample.l} /\ size Sample.l{2} <= q)=> //=. - conseq (_: _ ==> ={Sample.l}) _ (_: _ ==> size Sample.l <= q)=> //=;2:by sim. - (*by proc;call A_bounded;inline *;auto.*) admit. - qed. - - lemma pr_collision &m: - Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] - <= (q*(q-1))%r/2%r* mu1 uT maxu. - proof. rewrite (aux &m); apply (pr_Sample_le &m). qed. - - lemma pr_collision_q2 &m: - Pr[Exp(Sample,A).main() @ &m: !uniq Sample.l] - <= (q^2)%r * mu1 uT maxu. - proof. rewrite (aux &m); apply (pr_Sample_le_q2 &m). qed. - -end section. - -(*** The same result using a bounding module ***) -module Bounder(S:Sampler) = { - var c:int - - proc init(): unit = { - S.init(); - c <- 0; - } - - proc s(): T = { - var r <- witness; - - if (c < q) { - r <@ S.s(); - c <- c + 1; - } - return r; - } -}. - -module ABounder(S:ASampler) = { - proc s(): T = { - var r <- witness; - - if (Bounder.c < q) { - r <@ S.s(); - Bounder.c <- Bounder.c + 1; - } - return r; - } -}. - -module Bounded(A:Adv,S:ASampler) = { - proc a(): unit = { - Bounder.c <- 0; - A(ABounder(S)).a(); - } -}. - -equiv PushBound (S <: Sampler {-Bounder}) (A <: Adv {-S,-Bounder}): - Exp(Bounder(S),A).main ~ Exp(S,Bounded(A)).main: - ={glob A,glob S} ==> - ={glob A,glob S}. -proof. by proc; inline*; sim. qed. - -(** Forall adversary A with access to the bounded s oracle, the - probability that the same output is sampled twice is bounded by - q^2/|T| **) -section. - declare module A <: Adv {-Sample,-Bounder}. - - declare axiom A_ll (S <: ASampler {-A}): islossless S.s => islossless A(S).a. - - lemma pr_collision_bounded_oracles &m: - Pr[Exp(Bounder(Sample),A).main() @ &m: !uniq Sample.l] - <= (q^2)%r * mu1 uT maxu. - proof. - have ->: Pr[Exp(Bounder(Sample),A).main() @ &m: !uniq Sample.l] = - Pr[Exp(Sample,Bounded(A)).main() @ &m: !uniq Sample.l]. - + byequiv (PushBound Sample A) => //. - apply (pr_collision_q2 (Bounded(A)) _ _ &m). - + move=> S HS;proc;call (A_ll (ABounder(S)) _);2:by auto. - by proc;sp;if;auto;call HS. - proc. -call (_: size Sample.l <= Bounder.c <= q). - - -admit. - -admit. - + proc; sp; if =>//. inline *. - wp. rnd. admit. - - - wp. - - auto. - - smt(ge0_q). - qed. - -end section. - diff --git a/theories/crypto/.#Birthday.eca b/theories/crypto/.#Birthday.eca deleted file mode 120000 index 167b57bd79..0000000000 --- a/theories/crypto/.#Birthday.eca +++ /dev/null @@ -1 +0,0 @@ -strub@CrapuMac.local.44707:1747731257 \ No newline at end of file diff --git a/theories/crypto/Birthday.eca b/theories/crypto/Birthday.eca index 65d5579bb7..e7fd1ff216 100644 --- a/theories/crypto/Birthday.eca +++ b/theories/crypto/Birthday.eca @@ -175,21 +175,10 @@ section. + byequiv (PushBound Sample A) => //. apply (pr_collision_q2 (Bounded(A)) _ _ &m). + move=> S HS;proc;call (A_ll (ABounder(S)) _);2:by auto. - by proc;sp;if;auto;call HS. - proc. -call (_: size Sample.l <= Bounder.c <= q). -admit. - -admit. - + proc; sp; if =>//. inline *. - wp. rnd. admit. - - - wp. - - auto. - - smt(ge0_q). + by proc;sp;if;auto;call HS. + proc; call (_: size Sample.l <= Bounder.c <= q). + + proc;sp;if=>//;inline *;auto=> /#. + auto; smt(ge0_q). qed. end section. From 3a877bce816d4be6ac5fa5fca27aab302947410d Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 27 May 2025 11:03:29 +0100 Subject: [PATCH 23/26] fix hoareF_abs_spec --- src/phl/ecPhlFun.ml | 12 ++++++------ src/phl/ecPhlFun.mli | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index 6bb227593a..f317c52bc4 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -157,11 +157,11 @@ let t_fun_def = FApi.t_low0 "fun-def" t_fun_def_r (* -------------------------------------------------------------------- *) module FunAbsLow = struct (* ------------------------------------------------------------------ *) - let hoareF_abs_spec _pf env f inv = + let hoareF_abs_spec _pf env mem f inv = let (top, _, oi, _) = EcLowPhlGoal.abstract_info env f in - let fv = PV.fv env mhr inv in + let fv = PV.fv env mem inv in PV.check_depend env fv top; - let ospec o = f_hoareF mhr inv o inv in + let ospec o = f_hoareF mem inv o inv in let sg = List.map ospec (OI.allowed oi) in (inv, inv, sg) @@ -246,7 +246,7 @@ end let t_hoareF_abs_r inv tc = let env = FApi.tc1_env tc in let hf = tc1_as_hoareF tc in - let pre, post, sg = FunAbsLow.hoareF_abs_spec !!tc env hf.hf_f inv in + let pre, post, sg = FunAbsLow.hoareF_abs_spec !!tc env hf.hf_m hf.hf_f inv in let tactic tc = FApi.xmutate1 tc `FunAbs sg in FApi.t_last tactic (EcPhlConseq.t_hoareF_conseq pre post tc) @@ -523,12 +523,12 @@ let t_fun_to_code_r tc = let t_fun_to_code = FApi.t_low0 "fun-to-code" t_fun_to_code_r (* -------------------------------------------------------------------- *) -let t_fun_r ?mem inv tc = +let t_fun_r inv tc = let th tc = let env = FApi.tc1_env tc in let h = destr_hoareF (FApi.tc1_goal tc) in if NormMp.is_abstract_fun h.hf_f env - then t_hoareF_abs ?mem inv tc + then t_hoareF_abs inv tc else t_hoareF_fun_def tc and teh tc = diff --git a/src/phl/ecPhlFun.mli b/src/phl/ecPhlFun.mli index b33b22f665..70c1a30c5f 100644 --- a/src/phl/ecPhlFun.mli +++ b/src/phl/ecPhlFun.mli @@ -28,7 +28,7 @@ val process_fun_to_code : FApi.backward (* -------------------------------------------------------------------- *) module FunAbsLow : sig val hoareF_abs_spec : - proofenv -> EcEnv.env -> xpath -> form + proofenv -> EcEnv.env -> memory -> xpath -> form -> form * form * form list val bdhoareF_abs_spec : From 375e0326d76c4d6d219cd7545911fcf0fb4f0559 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 27 May 2025 12:43:13 +0100 Subject: [PATCH 24/26] reset phl_call --- src/phl/ecPhlCall.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 66dadbaf26..c1d1f0d51c 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -528,8 +528,8 @@ let process_call (side : side option) (info : call_info gppterm) (tc : tcenv1) = FApi.t_seqsub (t_call side ax) [FApi.t_seqs - [EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt] -(* !subtactic; t_trivial]; *); + [EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt; + !subtactic; t_trivial]; t_id] tc From 9c0537428bdbcf2cca073310c74dd23dca5a5102 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Tue, 27 May 2025 13:51:56 +0100 Subject: [PATCH 25/26] fix matching --- src/ecMatching.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 8de810498d..4cde24e7ac 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -677,7 +677,7 @@ let f_match_core opts hyps (ue, ev) f1 f2 = | FhoareF hf1, FhoareF hf2 -> begin if not (EcReduction.EqTest.for_xp env hf1.hf_f hf2.hf_f) then failure (); - let mxs = Mid.add EcFol.mhr EcFol.mhr mxs in + let mxs = Mid.add hf1.hf_m hf2.hf_m mxs in List.iter2 (doit env (subst, mxs)) [hf1.hf_pr; hf1.hf_po] [hf2.hf_pr; hf2.hf_po] end From 56a3cb837b0d08d65d7a2beadefb136700d77f31 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Wed, 28 May 2025 10:02:03 +0100 Subject: [PATCH 26/26] fixed matching - broken reduction --- src/ecHiGoal.ml | 2 +- src/ecLowGoal.ml | 3 +++ src/ecLowGoal.mli | 6 ++++++ src/ecMatching.ml | 5 +++++ src/ecReduction.ml | 5 ++++- 5 files changed, 19 insertions(+), 2 deletions(-) diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index dc1a6b8e16..5ceed5e483 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -453,8 +453,8 @@ let process_done tc = (* -------------------------------------------------------------------- *) let process_apply_bwd ~implicits mode (ff : ppterm) (tc : tcenv1) = - let pt = PT.tc1_process_full_pterm ~implicits tc ff in + let pt = PT.tc1_process_full_pterm ~implicits tc ff in try match mode with | `Alpha -> diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 0fcdb465cf..5103465ad7 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -2290,6 +2290,9 @@ type cstate = { cs_sbeq : Sid.t; } +let pp_tc1 tc = + pp_tc (FApi.tcenv_of_tcenv1 tc) + let t_debug ?(tag="") t tc = Format.eprintf "Before (tag: %s):" tag; pp_tc (FApi.tcenv_of_tcenv1 tc); diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index 358cdcc245..28b57c777f 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -358,3 +358,9 @@ val t_debug : -> FApi.backward -> FApi.backward [@@ocaml.alert debug "Debug function, remove uses before merging"] + +val pp_tc :tcenv -> unit +[@@ocaml.alert debug "Debug function, remove uses before merging"] + +val pp_tc1 :tcenv1 -> unit +[@@ocaml.alert debug "Debug function, remove uses before merging"] diff --git a/src/ecMatching.ml b/src/ecMatching.ml index 4cde24e7ac..8b63351922 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -677,6 +677,11 @@ let f_match_core opts hyps (ue, ev) f1 f2 = | FhoareF hf1, FhoareF hf2 -> begin if not (EcReduction.EqTest.for_xp env hf1.hf_f hf2.hf_f) then failure (); + let subst = + if id_equal hf1.hf_m hf2.hf_m + then subst + else Fsubst.f_bind_mem subst hf1.hf_m hf2.hf_m in + assert (not (Mid.mem hf1.hf_m mxs) && not (Mid.mem hf2.hf_m mxs)); let mxs = Mid.add hf1.hf_m hf2.hf_m mxs in List.iter2 (doit env (subst, mxs)) [hf1.hf_pr; hf1.hf_po] [hf2.hf_pr; hf2.hf_po] diff --git a/src/ecReduction.ml b/src/ecReduction.ml index 355d420dc4..e0743d7585 100644 --- a/src/ecReduction.ml +++ b/src/ecReduction.ml @@ -1453,7 +1453,10 @@ let rec conv ri env f1 f2 stk = conv_next ri env f1 stk | FhoareF hf1, FhoareF hf2 when EqTest_i.for_xp env hf1.hf_f hf2.hf_f -> - conv ri env hf1.hf_pr hf2.hf_pr (zhl f1 [hf1.hf_po] [hf2.hf_po] stk) + let subst = if id_equal hf1.hf_m hf2.hf_m then Fsubst.f_subst_id + else Fsubst.f_bind_mem Fsubst.f_subst_id hf1.hf_m hf2.hf_m in + let subst = Fsubst.f_subst subst in + conv ri env hf1.hf_pr (subst hf2.hf_pr) (zhl f1 [hf1.hf_po] [subst hf2.hf_po] stk) | FhoareS hs1, FhoareS hs2 when EqTest_i.for_stmt env hs1.hs_s hs2.hs_s ->