From 2e65ee8c26e380d27f68ed3ff5931af5a6c82acf Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 6 Oct 2026 18:52:01 +0200 Subject: [PATCH] refactor(pl): explicit, recheckable frame rule per logic MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Third PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). Framing — generalizing a condition over the variables a program writes — becomes explicit: it is done by one trusted frame rule per logic, and by nothing else. - rules/ecPlFrame.ml: the framing conditions (statement / procedure, one- / two-sided), i.e. the only place computing the written variables (s_write / f_write) and generalizing over them. Shared by the frame rules and by `conseq auto`. - rules/hoare/ecHoareFrame.ml, rules/bdhoare/ecBdHoareFrame.ml, rules/equiv/ecEquivFrame.ml: the frame rules — framed weakening of the postcondition — for statements and procedures, each emitting a node recording the new postcondition and with a registered checker. The checker recomputes the written variables from the goal's own context, so this soundness-critical step is re-validated. - EcPhlConseq: the former notmod rules and their condition builders are now adapters onto these modules; the framed consequence (t_*_conseq_nm) remains a derived composition of the frame rule and the (not yet migrated) consequence rule, and so do the seq derived forms that use it. Behaviour is unchanged (ehoare framing, done through concave, is left to the conseq migration). The stdlib and the unit tests pass under EC_RECHECK=1 with no RecheckFailure; each of the six checkers, when deliberately broken, is caught on the stdlib (hoareS 14 files, hoareF 3, bdhoareS 6, bdhoareF 8, equivS 13, equivF 17) and only under EC_RECHECK. --- src/phl/ecPhlConseq.ml | 247 +++-------------------- src/phl/rules/bdhoare/ecBdHoareFrame.ml | 83 ++++++++ src/phl/rules/bdhoare/ecBdHoareFrame.mli | 36 ++++ src/phl/rules/bdhoare/ecBdHoareSeq.ml | 3 +- src/phl/rules/bdhoare/ecBdHoareSeq.mli | 5 +- src/phl/rules/ecPlFrame.ml | 144 +++++++++++++ src/phl/rules/ecPlFrame.mli | 37 ++++ src/phl/rules/equiv/ecEquivFrame.ml | 67 ++++++ src/phl/rules/equiv/ecEquivFrame.mli | 38 ++++ src/phl/rules/equiv/ecEquivSeq.ml | 3 +- src/phl/rules/equiv/ecEquivSeq.mli | 3 +- src/phl/rules/hoare/ecHoareFrame.ml | 82 ++++++++ src/phl/rules/hoare/ecHoareFrame.mli | 37 ++++ 13 files changed, 560 insertions(+), 225 deletions(-) create mode 100644 src/phl/rules/bdhoare/ecBdHoareFrame.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareFrame.mli create mode 100644 src/phl/rules/ecPlFrame.ml create mode 100644 src/phl/rules/ecPlFrame.mli create mode 100644 src/phl/rules/equiv/ecEquivFrame.ml create mode 100644 src/phl/rules/equiv/ecEquivFrame.mli create mode 100644 src/phl/rules/hoare/ecHoareFrame.ml create mode 100644 src/phl/rules/hoare/ecHoareFrame.mli diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml index f820393dc..cff256371 100644 --- a/src/phl/ecPhlConseq.ml +++ b/src/phl/ecPhlConseq.ml @@ -404,245 +404,52 @@ let t_conseq (pre : inv) (post : inv) (tc : tcenv1) = (* -------------------------------------------------------------------- *) -(* Build the non-modification side-condition for equivF: - * universally quantify the pre-memories, substitute the result variables, - * then generalize over program variables modified by each procedure. - * Returns (cond, bound_mems, other_bindings). *) +(* The notmod rules are the frame rules of [EcHoareFrame], [EcBdHoareFrame] + and [EcEquivFrame]; their conditions are built by [EcPlFrame]. The + functions below are adapters keeping this module's legacy entry points. *) + let cond_equivF_notmod ?(mk_other=false) (tc : tcenv1) (cond : ts_inv) = let (env, hyps, _) = FApi.tc1_eflat tc in - let ef = tc1_as_equivF tc in - let fl, fr = ef.ef_fl, ef.ef_fr in - let (mprl,mprr),(mpol,mpor) = Fun.equivF_memenv ef.ef_ml ef.ef_mr fl fr env in - let fsigl = (Fun.by_xpath fl env).f_sig in - let fsigr = (Fun.by_xpath fr env).f_sig in - let pvresl = pv_res and pvresr = pv_res in - let vresl = LDecl.fresh_id hyps "result_L" in - let vresr = LDecl.fresh_id hyps "result_R" in - let fresl = f_local vresl fsigl.fs_ret in - let fresr = f_local vresr fsigr.fs_ret in - let ml, mr = fst mpol, fst mpor in - assert (ml = cond.ml && mr = cond.mr); - let s = PVM.add env pvresl ml fresl (PVM.add env pvresr mr fresr PVM.empty) in - let cond = map_ts_inv1 (PVM.subst env s) cond in - let modil, modir = f_write env fl, f_write env fr in - let cond, bdgr, bder = generalize_mod_right_ env modir cond in - let cond, bdgl, bdel = generalize_mod_left_ env modil cond in - let cond = - map_ts_inv1 (f_forall_simpl - [(vresl, GTty fsigl.fs_ret); - (vresr, GTty fsigr.fs_ret)]) - cond in - assert (fst mprl = ml && fst mprr = mr); - let cond = f_forall_mems_ts_inv mprl mprr (map_ts_inv2 f_imp (ef_pr ef) cond) in - let bmem = [ml;mr] in - let bother = - if mk_other then - mk_bind_pvar ml vresl (pvresl, fsigl.fs_ret) :: - mk_bind_pvar mr vresr (pvresr, fsigr.fs_ret) :: - List.flatten [mk_bind_globs env ml bdgl; mk_bind_pvars ml bdel; - mk_bind_globs env mr bdgr; mk_bind_pvars mr bder] - else [] in - cond, bmem, bother - -(* equivF notmod rule: - * - * ∀ml mr, P ml mr ⇒ - * ∀(res_L : ret_L) (res_R : ret_R) (x1 ... xn : modified vars), - * Q' ml mr ⇒ Q ml mr - * equiv[f1 ~ f2] P ==> Q' - * —————————————————————————————————————————————————————————————————— - * equiv[f1 ~ f2] P ==> Q - * - * The first premise universally quantifies over the return values and - * all program variables modified by f1/f2, then checks that Q' ⇒ Q - * holds under those bindings. *) -let t_equivF_notmod (post : ts_inv) (tc : tcenv1) = - let ef = tc1_as_equivF tc in - let post = ts_inv_rebind post ef.ef_ml ef.ef_mr in - let cond1, _, _ = cond_equivF_notmod tc (map_ts_inv2 f_imp post (ef_po ef)) in - let cond2 = f_equivF (ef_pr ef) ef.ef_fl ef.ef_fr post in - FApi.xmutate1 tc `HlNotmod [cond1; cond2] + EcPlFrame.ts_frame_cond_F ~mk_other env hyps (tc1_as_equivF tc) cond -(* -------------------------------------------------------------------- *) let cond_equivS_notmod ?(mk_other=false) (tc : tcenv1) (cond : ts_inv) = - let env = FApi.tc1_env tc in - let es = tc1_as_equivS tc in - let sl, sr = es.es_sl, es.es_sr in - let ml, mr = fst es.es_ml, fst es.es_mr in - assert (ml = cond.ml && mr = cond.mr); - let modil, modir = s_write env sl, s_write env sr in - let cond, bdgr, bder = generalize_mod_right_ env modir cond in - let cond, bdgl, bdel = generalize_mod_left_ env modil cond in - let cond = f_forall_mems_ts_inv es.es_ml es.es_mr (map_ts_inv2 f_imp (es_pr es) cond) in - let bmem = [ml;mr] in - let bother = - if mk_other then - List.flatten [mk_bind_globs env ml bdgl; mk_bind_pvars ml bdel; - mk_bind_globs env mr bdgr; mk_bind_pvars mr bder] - else [] in - cond, bmem, bother - -(* equivS notmod rule: same as equivF_notmod but for statements - * (no result variable generalization needed). *) -let t_equivS_notmod (post : ts_inv) (tc : tcenv1) = - let es = tc1_as_equivS tc in - let post = ts_inv_rebind post (fst es.es_ml) (fst es.es_mr) in - let cond1,_,_ = cond_equivS_notmod tc (map_ts_inv2 f_imp post (es_po es)) in - let cond2 = f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) es.es_sl es.es_sr post in - FApi.xmutate1 tc `HlNotmod [cond1; cond2] - -(* -------------------------------------------------------------------- *) -(* Shared core for F-level notmod: substitutes the result variable, *) -(* generalizes over modified variables, quantifies over the result, *) -(* and builds the implication with the precondition. *) -(* *) -(* Returns (cond, bmem, bother) where: *) -(* cond : the fully quantified side-condition formula *) -(* bmem : memories bound in the quantification ([m]) *) -(* bother : when ~mk_other, bindings for result + modified vars; *) -(* otherwise [] *) - -let cond_F_notmod_core - ~(mk_other : bool) - (env : env) - (hyps : LDecl.hyps) - (f : EcPath.xpath) - (m : memory) - (pre : ss_inv) - (cond : ss_inv) -= - let mpr,mpo = Fun.hoareF_memenv m 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 - 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 = map_ss_inv1 (PVM.subst env s) cond in - let modi = f_write env f in - let cond, bdg, bde = generalize_mod_ env modi cond in - let cond = map_ss_inv1 (f_forall_simpl [(vres, GTty fsig.fs_ret)]) cond in - assert (fst mpr = m); - let cond = f_forall_mems_ss_inv mpr (map_ss_inv2 f_imp pre cond) in - let bmem = [m] in - let bother = - if mk_other then - mk_bind_pvar m vres (pvres, fsig.fs_ret) :: - List.flatten [mk_bind_globs env m bdg; mk_bind_pvars m bde] - else [] in - cond, bmem, bother + EcPlFrame.ts_frame_cond_S ~mk_other (FApi.tc1_env tc) (tc1_as_equivS tc) cond let cond_hoareF_notmod ?(mk_other=false) (tc : tcenv1) (cond : ss_inv) = let (env, hyps, _) = FApi.tc1_eflat tc in let hf = tc1_as_hoareF tc in - cond_F_notmod_core ~mk_other env hyps hf.hf_f hf.hf_m (hf_pr hf) cond - -(* hoareF notmod rule: - * - * ∀m, P m ⇒ - * ∀(res : ret) (x1 ... xn : modified vars), - * Q' m ⇒ Q m [∧ Qe_i' ⇒ Qe_i for each exception] - * hoare[f] P ==> Q' / Qe' - * ——————————————————————————————————————————————————————— - * hoare[f] P ==> Q / Qe - * - * Q / Qe denotes the normal postcondition Q together with the - * per-exception postconditions Qe_i (if any). *) -let t_hoareF_notmod (post : hs_inv) (tc : tcenv1) = - let hf = tc1_as_hoareF tc in - let p = hs_inv_rebind post hf.hf_m in - let post, epost = POE.destruct p.hsi_inv in - let fpost, fepost = POE.destruct (hf_po hf).hsi_inv in - let cond = f_imp post fpost in - let econd1 = TTC.merge2_poe_list fepost epost in - let cond1 = List.fold f_and cond econd1 in - let cond1, _, _ = cond_hoareF_notmod tc {m=hf.hf_m;inv=cond1} in - let cond2 = f_hoareF (hf_pr hf) hf.hf_f p in - FApi.xmutate1 tc `HlNotmod [cond1; cond2] - -(* -------------------------------------------------------------------- *) -(* Shared core for S-level notmod: generalizes over modified variables *) -(* and builds the implication with the precondition. *) - -let cond_S_notmod_core - ~(mk_other : bool) - (env : env) - (stmt : stmt) - (memenv : memenv) - (pre : ss_inv) - (cond : ss_inv) -= - let m = fst memenv in - let modi = s_write env stmt in - let cond, bdg, bde = generalize_mod_ env modi cond in - let cond = f_forall_mems_ss_inv memenv (map_ss_inv2 f_imp pre cond) in - let bmem = [m] in - let bother = - if mk_other then - List.flatten [mk_bind_globs env m bdg; mk_bind_pvars m bde] - else [] in - cond, bmem, bother + EcPlFrame.ss_frame_cond_F ~mk_other env hyps hf.hf_f hf.hf_m (hf_pr hf) cond let cond_hoareS_notmod ?(mk_other=false) (tc : tcenv1) (cond : ss_inv) = - let env = FApi.tc1_env tc in - let hs = tc1_as_hoareS tc in - cond_S_notmod_core ~mk_other env hs.hs_s hs.hs_m (hs_pr hs) cond - -(* hoareS notmod rule: same as hoareF_notmod but for statements. *) -let t_hoareS_notmod (post : hs_inv) (tc : tcenv1) = let hs = tc1_as_hoareS tc in - let p = hs_inv_rebind post (fst hs.hs_m) in - let post, epost = POE.destruct p.hsi_inv in - let fpost, fepost = POE.destruct (hs_po hs).hsi_inv in - let cond = f_imp post fpost in - let econd1 = TTC.merge2_poe_list fepost epost in - let cond1 = List.fold f_and cond econd1 in - let cond1, _, _ = cond_hoareS_notmod tc {m=fst hs.hs_m;inv=cond1} in - let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s p in - FApi.xmutate1 tc `HlNotmod [cond1; cond2] + EcPlFrame.ss_frame_cond_S ~mk_other (FApi.tc1_env tc) hs.hs_s hs.hs_m (hs_pr hs) cond -(* -------------------------------------------------------------------- *) let cond_bdHoareF_notmod ?(mk_other=false) (tc : tcenv1) (cond : ss_inv) = let (env, hyps, _) = FApi.tc1_eflat tc in let hf = tc1_as_bdhoareF tc in - cond_F_notmod_core ~mk_other env hyps hf.bhf_f hf.bhf_m (bhf_pr hf) cond - + EcPlFrame.ss_frame_cond_F ~mk_other env hyps hf.bhf_f hf.bhf_m (bhf_pr hf) cond -(* bdHoareF notmod rule: - * - * ∀m, P m ⇒ - * ∀(res : ret) (x1 ... xn : modified vars), - * Q' m ⇒/⇔/⇐ Q m - * phoare[f] P ==> Q' cmp bd - * —————————————————————————————————————————————— - * phoare[f] P ==> Q cmp bd - * - * The direction of the postcondition implication depends on cmp: - * FHle (≤): Q' ⇒ Q FHeq (=): Q' ⇔ Q FHge (≥): Q ⇒ Q' *) -let t_bdHoareF_notmod (post : ss_inv) (tc : tcenv1) = - let hf = tc1_as_bdhoareF tc in - let post = ss_inv_rebind post hf.bhf_m in - let _, cond = - bdHoare_conseq_conds hf.bhf_cmp (bhf_pr hf) (bhf_po hf) (bhf_pr hf) post in - let cond1, _, _ = cond_bdHoareF_notmod tc cond in - let cond2 = f_bdHoareF (bhf_pr hf) hf.bhf_f post hf.bhf_cmp (bhf_bd hf) in - FApi.xmutate1 tc `HlNotmod [cond1; cond2] - -(* -------------------------------------------------------------------- *) let cond_bdHoareS_notmod ?(mk_other=false) (tc : tcenv1) (cond : ss_inv) = - let env = FApi.tc1_env tc in let hs = tc1_as_bdhoareS tc in - cond_S_notmod_core ~mk_other env hs.bhs_s hs.bhs_m (bhs_pr hs) cond + EcPlFrame.ss_frame_cond_S ~mk_other (FApi.tc1_env tc) hs.bhs_s hs.bhs_m (bhs_pr hs) cond -(* bdHoareS notmod rule: same as bdHoareF_notmod but for statements. *) -let t_bdHoareS_notmod (post : ss_inv) (tc : tcenv1) = - let hs = tc1_as_bdhoareS tc in - let post = ss_inv_rebind post (fst hs.bhs_m) in - let _, cond = - bdHoare_conseq_conds hs.bhs_cmp (bhs_pr hs) (bhs_po hs) (bhs_pr hs) post in - let cond1, _, _ = cond_bdHoareS_notmod tc cond in - let cond2 = f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s post hs.bhs_cmp (bhs_bd hs) in - FApi.xmutate1 tc `HlNotmod [cond1; cond2] +let t_equivF_notmod (post : ts_inv) = + EcEquivFrame.t_equivF_frame { efr_post = post } + +let t_equivS_notmod (post : ts_inv) = + EcEquivFrame.t_equivS_frame { efr_post = post } + +let t_hoareF_notmod (post : hs_inv) = + EcHoareFrame.t_hoareF_frame { hfr_post = post } + +let t_hoareS_notmod (post : hs_inv) = + EcHoareFrame.t_hoareS_frame { hfr_post = post } + +let t_bdHoareF_notmod (post : ss_inv) = + EcBdHoareFrame.t_bdhoareF_frame { bfr_post = post } + +let t_bdHoareS_notmod (post : ss_inv) = + EcBdHoareFrame.t_bdhoareS_frame { bfr_post = post } (* -------------------------------------------------------------------- *) let gen_conseq_nm diff --git a/src/phl/rules/bdhoare/ecBdHoareFrame.ml b/src/phl/rules/bdhoare/ecBdHoareFrame.ml new file mode 100644 index 000000000..9924771e5 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareFrame.ml @@ -0,0 +1,83 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare frame rules: the new postcondition [Q']. Already + typed, nothing to resolve: the same record is the rule argument and the + node payload. *) +type bdhoare_frame = { + bfr_post : ss_inv; +} + +type EcCoreGoal.rule += + | RBdHoareSFrame of bdhoare_frame + | RBdHoareFFrame of bdhoare_frame + +(* -------------------------------------------------------------------- *) +(* The postcondition condition, before framing. Its direction follows the + comparison: an upper bound needs [Q] to imply [Q'], a lower bound the + converse, an equality both. *) +let bdhoare_frame_post_cond (cmp : hoarecmp) (q : ss_inv) (q' : ss_inv) = + match cmp with + | FHle -> map_ss_inv2 f_imp q q' + | FHeq -> map_ss_inv2 f_iff q q' + | FHge -> map_ss_inv2 f_imp q' q + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. *) +let bdhoareS_frame_subgoals + (hyps : LDecl.hyps) (hs : bdHoareS) (n : bdhoare_frame) += + let env = LDecl.toenv hyps in + let post = ss_inv_rebind n.bfr_post (fst hs.bhs_m) in + let cond = bdhoare_frame_post_cond hs.bhs_cmp (bhs_po hs) post in + let cond1, _, _ = + EcPlFrame.ss_frame_cond_S ~mk_other:false + env hs.bhs_s hs.bhs_m (bhs_pr hs) cond in + let cond2 = + f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) hs.bhs_s post hs.bhs_cmp (bhs_bd hs) in + [cond1; cond2] + +let bdhoareF_frame_subgoals + (hyps : LDecl.hyps) (hf : bdHoareF) (n : bdhoare_frame) += + let env = LDecl.toenv hyps in + let post = ss_inv_rebind n.bfr_post hf.bhf_m in + let cond = bdhoare_frame_post_cond hf.bhf_cmp (bhf_po hf) post in + let cond1, _, _ = + EcPlFrame.ss_frame_cond_F ~mk_other:false + env hyps hf.bhf_f hf.bhf_m (bhf_pr hf) cond in + let cond2 = f_bdHoareF (bhf_pr hf) hf.bhf_f post hf.bhf_cmp (bhf_bd hf) in + [cond1; cond2] + +(* -------------------------------------------------------------------- *) +(* Rules (TCB). *) +let t_bdhoareS_frame (r : bdhoare_frame) (tc : tcenv1) = + let hs = tc1_as_bdhoareS tc in + FApi.xrule1 tc (RBdHoareSFrame r) + (bdhoareS_frame_subgoals (FApi.tc1_hyps tc) hs r) + +let t_bdhoareF_frame (r : bdhoare_frame) (tc : tcenv1) = + let hf = tc1_as_bdhoareF tc in + FApi.xrule1 tc (RBdHoareFFrame r) + (bdhoareF_frame_subgoals (FApi.tc1_hyps tc) hf r) + +(* -------------------------------------------------------------------- *) +(* Checkers: rerun the core, which recomputes the variables written by the + program from the goal's own context. *) +let () = + register_rule_checker + (function + | RBdHoareSFrame n -> + Some (EcPlRecheck.checker_of "bdhoareS-frame" pf_as_bdhoareS + (fun hyps hs -> bdhoareS_frame_subgoals hyps hs n)) + | RBdHoareFFrame n -> + Some (EcPlRecheck.checker_of "bdhoareF-frame" pf_as_bdhoareF + (fun hyps hf -> bdhoareF_frame_subgoals hyps hf n)) + | _ -> None) diff --git a/src/phl/rules/bdhoare/ecBdHoareFrame.mli b/src/phl/rules/bdhoare/ecBdHoareFrame.mli new file mode 100644 index 000000000..f66cb3ef8 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareFrame.mli @@ -0,0 +1,36 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_frame = { + bfr_post : ss_inv; (* new postcondition Q' *) +} + +(* [t_bdhoareS_frame { bfr_post = Q' }] — framed change of the + postcondition, with [~] the goal's comparison: + + forall &m, P => forall (mod c), Q [~>] Q' + phoare [c : P ==> Q'] ~ d + ----------------------------------------- + phoare [c : P ==> Q] ~ d + + where [mod c] are the program variables and globals written by [c], and + [Q [~>] Q'] is [Q => Q'] for [<=], [Q <=> Q'] for [=], [Q' => Q] for [>=]. + + Node: [RBdHoareSFrame { bfr_post = Q' }]. Checker: "bdhoareS-frame"; it + recomputes [mod c] from the goal's context. *) +val t_bdhoareS_frame : bdhoare_frame -> backward + +(* [t_bdhoareF_frame { bfr_post = Q' }] — same for a procedure [f], also + quantifying over its result: + + forall &m, P => forall (res : ret) (mod f), (Q [~>] Q')[res/result] + phoare [f : P ==> Q'] ~ d + ------------------------------------------------------------------- + phoare [f : P ==> Q] ~ d + + Node: [RBdHoareFFrame { bfr_post = Q' }]. Checker: "bdhoareF-frame". *) +val t_bdhoareF_frame : bdhoare_frame -> backward diff --git a/src/phl/rules/bdhoare/ecBdHoareSeq.ml b/src/phl/rules/bdhoare/ecBdHoareSeq.ml index f9bb7e886..8b30becc5 100644 --- a/src/phl/rules/bdhoare/ecBdHoareSeq.ml +++ b/src/phl/rules/bdhoare/ecBdHoareSeq.ml @@ -139,7 +139,8 @@ let () = write the bounds [f2] / [g2]. This is what the surface [seq] tactic and the legacy positional entry (EcPhlSeq.t_bdhoare_seq) use. - TEMPORARY: depends on the not-yet-migrated [EcPhlConseq]. *) + TEMPORARY: the consequence rule still comes from the not-yet-migrated + [EcPhlConseq]. *) let t_bdhoare_seq_full (r : bdhoare_seq_rule) tc = let tactic tc = let hs = tc1_as_hoareS tc in diff --git a/src/phl/rules/bdhoare/ecBdHoareSeq.mli b/src/phl/rules/bdhoare/ecBdHoareSeq.mli index 787228ed0..fc5496c22 100644 --- a/src/phl/rules/bdhoare/ecBdHoareSeq.mli +++ b/src/phl/rules/bdhoare/ecBdHoareSeq.mli @@ -46,8 +46,9 @@ val t_bdhoare_seq : bdhoare_seq_rule -> backward (* Derived tactics *) (* [t_bdhoare_seq_full r] — [t_bdhoare_seq r], then a best-effort discharge - of (N): introduce [r1 r2], apply the framed consequence (currently - [EcPhlConseq.t_hoareS_conseq_nm]) down to [hoare [c1 : _ ==> true]], and + of (N): introduce [r1 r2], apply the framed consequence + [EcPhlConseq.t_hoareS_conseq_nm] (the frame rule + [EcHoareFrame.t_hoareS_frame], then the consequence rule) down to [hoare [c1 : _ ==> true]], and close everything with [EcPhlAuto.t_pl_trivial] — which succeeds when [c1] does not write the variables of [f2] / [g2]. Otherwise (N) is left open unchanged. Emits no node of its own. *) diff --git a/src/phl/rules/ecPlFrame.ml b/src/phl/rules/ecPlFrame.ml new file mode 100644 index 000000000..b95bc16eb --- /dev/null +++ b/src/phl/rules/ecPlFrame.ml @@ -0,0 +1,144 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcTypes +open EcFol +open EcEnv +open EcPV +open EcSubst +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Framing conditions, shared by the frame rules of every logic (and by + [conseq auto]). Framing — generalizing a condition over the variables a + program writes — is done here and nowhere else. + + Each builder returns [(cond, bmem, bother)]: the closed side condition, + the memories it quantifies over, and (only when [~mk_other]) bindings for + the other quantified variables (result, modified globals and variables), + used by [conseq auto] to introduce them. *) + +type frame_cond = form * memory list * (EcIdent.t * ss_inv) list + +(* -------------------------------------------------------------------- *) +(* One-sided, statement: forall &m, pre => forall (mod s), cond. *) +let ss_frame_cond_S + ~(mk_other : bool) + (env : env) + (s : stmt) + (memenv : memenv) + (pre : ss_inv) + (cond : ss_inv) += + let m = fst memenv in + let modi = s_write env s in + let cond, bdg, bde = generalize_mod_ env modi cond in + let cond = f_forall_mems_ss_inv memenv (map_ss_inv2 f_imp pre cond) in + let bmem = [m] in + let bother = + if mk_other then + List.flatten [mk_bind_globs env m bdg; mk_bind_pvars m bde] + else [] in + cond, bmem, bother + +(* -------------------------------------------------------------------- *) +(* One-sided, procedure: + forall &m, pre => forall (res : ret) (mod f), cond[res/result]. *) +let ss_frame_cond_F + ~(mk_other : bool) + (env : env) + (hyps : LDecl.hyps) + (f : EcPath.xpath) + (m : memory) + (pre : ss_inv) + (cond : ss_inv) += + let mpr,mpo = Fun.hoareF_memenv m 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 + 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 = map_ss_inv1 (PVM.subst env s) cond in + let modi = f_write env f in + let cond, bdg, bde = generalize_mod_ env modi cond in + let cond = map_ss_inv1 (f_forall_simpl [(vres, GTty fsig.fs_ret)]) cond in + assert (fst mpr = m); + let cond = f_forall_mems_ss_inv mpr (map_ss_inv2 f_imp pre cond) in + let bmem = [m] in + let bother = + if mk_other then + mk_bind_pvar m vres (pvres, fsig.fs_ret) :: + List.flatten [mk_bind_globs env m bdg; mk_bind_pvars m bde] + else [] in + cond, bmem, bother + +(* -------------------------------------------------------------------- *) +(* Two-sided, statements: + forall &1 &2, pre => forall (mod sl)<1> (mod sr)<2>, cond. *) +let ts_frame_cond_S + ~(mk_other : bool) + (env : env) + (es : equivS) + (cond : ts_inv) += + let sl, sr = es.es_sl, es.es_sr in + let ml, mr = fst es.es_ml, fst es.es_mr in + assert (ml = cond.ml && mr = cond.mr); + let modil, modir = s_write env sl, s_write env sr in + let cond, bdgr, bder = generalize_mod_right_ env modir cond in + let cond, bdgl, bdel = generalize_mod_left_ env modil cond in + let cond = f_forall_mems_ts_inv es.es_ml es.es_mr (map_ts_inv2 f_imp (es_pr es) cond) in + let bmem = [ml;mr] in + let bother = + if mk_other then + List.flatten [mk_bind_globs env ml bdgl; mk_bind_pvars ml bdel; + mk_bind_globs env mr bdgr; mk_bind_pvars mr bder] + else [] in + cond, bmem, bother + +(* -------------------------------------------------------------------- *) +(* Two-sided, procedures: + forall &1 &2, pre => + forall (res_L : retl) (res_R : retr) (mod fl)<1> (mod fr)<2>, + cond[res_L/result<1>, res_R/result<2>]. *) +let ts_frame_cond_F + ~(mk_other : bool) + (env : env) + (hyps : LDecl.hyps) + (ef : equivF) + (cond : ts_inv) += + let fl, fr = ef.ef_fl, ef.ef_fr in + let (mprl,mprr),(mpol,mpor) = Fun.equivF_memenv ef.ef_ml ef.ef_mr fl fr env in + let fsigl = (Fun.by_xpath fl env).f_sig in + let fsigr = (Fun.by_xpath fr env).f_sig in + let pvresl = pv_res and pvresr = pv_res in + let vresl = LDecl.fresh_id hyps "result_L" in + let vresr = LDecl.fresh_id hyps "result_R" in + let fresl = f_local vresl fsigl.fs_ret in + let fresr = f_local vresr fsigr.fs_ret in + let ml, mr = fst mpol, fst mpor in + assert (ml = cond.ml && mr = cond.mr); + let s = PVM.add env pvresl ml fresl (PVM.add env pvresr mr fresr PVM.empty) in + let cond = map_ts_inv1 (PVM.subst env s) cond in + let modil, modir = f_write env fl, f_write env fr in + let cond, bdgr, bder = generalize_mod_right_ env modir cond in + let cond, bdgl, bdel = generalize_mod_left_ env modil cond in + let cond = + map_ts_inv1 (f_forall_simpl + [(vresl, GTty fsigl.fs_ret); + (vresr, GTty fsigr.fs_ret)]) + cond in + assert (fst mprl = ml && fst mprr = mr); + let cond = f_forall_mems_ts_inv mprl mprr (map_ts_inv2 f_imp (ef_pr ef) cond) in + let bmem = [ml;mr] in + let bother = + if mk_other then + mk_bind_pvar ml vresl (pvresl, fsigl.fs_ret) :: + mk_bind_pvar mr vresr (pvresr, fsigr.fs_ret) :: + List.flatten [mk_bind_globs env ml bdgl; mk_bind_pvars ml bdel; + mk_bind_globs env mr bdgr; mk_bind_pvars mr bder] + else [] in + cond, bmem, bother diff --git a/src/phl/rules/ecPlFrame.mli b/src/phl/rules/ecPlFrame.mli new file mode 100644 index 000000000..ec29364a0 --- /dev/null +++ b/src/phl/rules/ecPlFrame.mli @@ -0,0 +1,37 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcEnv + +(* -------------------------------------------------------------------- *) +(* Framing conditions, shared by the frame rules of every logic (and by + [conseq auto]). Framing — generalizing a condition over the variables a + program writes — is done here and nowhere else. + + Each builder returns [(cond, bmem, bother)]: the closed side condition, + the memories it quantifies over, and — only when [~mk_other] — bindings + for the other quantified variables (result, modified globals and program + variables), used by [conseq auto] to introduce them. *) + +type frame_cond = form * memory list * (EcIdent.t * ss_inv) list + +(* Statement [s] in memory [memenv]: + forall &m, pre => forall (mod s), cond *) +val ss_frame_cond_S : + mk_other:bool -> env -> stmt -> memenv -> ss_inv -> ss_inv -> frame_cond + +(* Procedure [f], postcondition memory [m]: + forall &m, pre => forall (res : ret) (mod f), cond[res / result] *) +val ss_frame_cond_F : + mk_other:bool -> env -> LDecl.hyps -> EcPath.xpath -> memory + -> ss_inv -> ss_inv -> frame_cond + +(* Two-sided, statements of [es], under its precondition: + forall &1 &2, pre => forall (mod sl)<1> (mod sr)<2>, cond *) +val ts_frame_cond_S : mk_other:bool -> env -> equivS -> ts_inv -> frame_cond + +(* Two-sided, procedures of [ef], under its precondition: + forall &1 &2, pre => + forall (res_L : retl) (res_R : retr) (mod fl)<1> (mod fr)<2>, + cond[res_L / result<1>, res_R / result<2>] *) +val ts_frame_cond_F : + mk_other:bool -> env -> LDecl.hyps -> equivF -> ts_inv -> frame_cond diff --git a/src/phl/rules/equiv/ecEquivFrame.ml b/src/phl/rules/equiv/ecEquivFrame.ml new file mode 100644 index 000000000..02ebfb375 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFrame.ml @@ -0,0 +1,67 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the equiv frame rules: the new postcondition [Q']. Already + typed, nothing to resolve: the same record is the rule argument and the + node payload. *) +type equiv_frame = { + efr_post : ts_inv; +} + +type EcCoreGoal.rule += + | REquivSFrame of equiv_frame + | REquivFFrame of equiv_frame + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. *) +let equivS_frame_subgoals (hyps : LDecl.hyps) (es : equivS) (n : equiv_frame) = + let env = LDecl.toenv hyps in + let post = ts_inv_rebind n.efr_post (fst es.es_ml) (fst es.es_mr) in + let cond1, _, _ = + EcPlFrame.ts_frame_cond_S ~mk_other:false + env es (map_ts_inv2 f_imp post (es_po es)) in + let cond2 = + f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) es.es_sl es.es_sr post in + [cond1; cond2] + +let equivF_frame_subgoals (hyps : LDecl.hyps) (ef : equivF) (n : equiv_frame) = + let env = LDecl.toenv hyps in + let post = ts_inv_rebind n.efr_post ef.ef_ml ef.ef_mr in + let cond1, _, _ = + EcPlFrame.ts_frame_cond_F ~mk_other:false + env hyps ef (map_ts_inv2 f_imp post (ef_po ef)) in + let cond2 = f_equivF (ef_pr ef) ef.ef_fl ef.ef_fr post in + [cond1; cond2] + +(* -------------------------------------------------------------------- *) +(* Rules (TCB). *) +let t_equivS_frame (r : equiv_frame) (tc : tcenv1) = + let es = tc1_as_equivS tc in + FApi.xrule1 tc (REquivSFrame r) + (equivS_frame_subgoals (FApi.tc1_hyps tc) es r) + +let t_equivF_frame (r : equiv_frame) (tc : tcenv1) = + let ef = tc1_as_equivF tc in + FApi.xrule1 tc (REquivFFrame r) + (equivF_frame_subgoals (FApi.tc1_hyps tc) ef r) + +(* -------------------------------------------------------------------- *) +(* Checkers: rerun the core, which recomputes the variables written by both + programs from the goal's own context. *) +let () = + register_rule_checker + (function + | REquivSFrame n -> + Some (EcPlRecheck.checker_of "equivS-frame" pf_as_equivS + (fun hyps es -> equivS_frame_subgoals hyps es n)) + | REquivFFrame n -> + Some (EcPlRecheck.checker_of "equivF-frame" pf_as_equivF + (fun hyps ef -> equivF_frame_subgoals hyps ef n)) + | _ -> None) diff --git a/src/phl/rules/equiv/ecEquivFrame.mli b/src/phl/rules/equiv/ecEquivFrame.mli new file mode 100644 index 000000000..a65b475b1 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivFrame.mli @@ -0,0 +1,38 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_frame = { + efr_post : ts_inv; (* new postcondition Q' *) +} + +(* [t_equivS_frame { efr_post = Q' }] — framed weakening of the + postcondition: + + forall &1 &2, P => forall (mod c)<1> (mod c')<2>, Q' => Q + equiv [c ~ c' : P ==> Q'] + --------------------------------------------------------- + equiv [c ~ c' : P ==> Q] + + where [mod c] / [mod c'] are the program variables and globals written by + each side. + + Node: [REquivSFrame { efr_post = Q' }]. Checker: "equivS-frame"; it + recomputes [mod c], [mod c'] from the goal's context. *) +val t_equivS_frame : equiv_frame -> backward + +(* [t_equivF_frame { efr_post = Q' }] — same for procedures [f ~ f'], also + quantifying over their results: + + forall &1 &2, P => + forall (res_L : ret) (res_R : ret') (mod f)<1> (mod f')<2>, + (Q' => Q)[res_L/result<1>, res_R/result<2>] + equiv [f ~ f' : P ==> Q'] + --------------------------------------------------------------- + equiv [f ~ f' : P ==> Q] + + Node: [REquivFFrame { efr_post = Q' }]. Checker: "equivF-frame". *) +val t_equivF_frame : equiv_frame -> backward diff --git a/src/phl/rules/equiv/ecEquivSeq.ml b/src/phl/rules/equiv/ecEquivSeq.ml index fda89a500..76926fb25 100644 --- a/src/phl/rules/equiv/ecEquivSeq.ml +++ b/src/phl/rules/equiv/ecEquivSeq.ml @@ -71,7 +71,8 @@ let () = two-sided rule (the other side split at its end) followed by [conseq] steps that discharge the one-sided part. - TEMPORARY: depends on the not-yet-migrated [EcPhlConseq]. *) + TEMPORARY: the consequence rule still comes from the not-yet-migrated + [EcPhlConseq]. *) let t_equiv_seq_onesided side i pre post tc = let env = FApi.tc1_env tc in let es = tc1_as_equivS tc in diff --git a/src/phl/rules/equiv/ecEquivSeq.mli b/src/phl/rules/equiv/ecEquivSeq.mli index acbe7d0bd..ce38a14e0 100644 --- a/src/phl/rules/equiv/ecEquivSeq.mli +++ b/src/phl/rules/equiv/ecEquivSeq.mli @@ -34,7 +34,8 @@ val t_equiv_seq : equiv_seq_rule -> backward R := pre<1> /\ forall (mod c2)<1>, post<1> => Q giving (a) equiv [c1 ~ c' : P ==> R] — left open, (b) equiv [c2 ~ skip : R ==> Q]; - 2. on (b), the framed consequence (currently [EcPhlConseq.t_equivS_conseq_nm]) + 2. on (b), the framed consequence [EcPhlConseq.t_equivS_conseq_nm] (the + frame rule [EcEquivFrame.t_equivS_frame], then the consequence rule) to [equiv [c2 ~ skip : pre<1> ==> post<1>]]; its side conditions [R => pre<1>] and [R => forall (mod c2)<1>, post<1> => Q] are closed by [t_trivial]; diff --git a/src/phl/rules/hoare/ecHoareFrame.ml b/src/phl/rules/hoare/ecHoareFrame.ml new file mode 100644 index 000000000..a0441b16e --- /dev/null +++ b/src/phl/rules/hoare/ecHoareFrame.ml @@ -0,0 +1,82 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcFol +open EcAst +open EcEnv +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Parameters of the hoare frame rules: the new postcondition [Q'] (normal + and exceptional parts). Already typed, nothing to resolve: the same record + is the rule argument and the node payload. *) +type hoare_frame = { + hfr_post : hs_inv; +} + +type EcCoreGoal.rule += + | RHoareSFrame of hoare_frame + | RHoareFFrame of hoare_frame + +(* -------------------------------------------------------------------- *) +(* The postcondition condition, before framing: + (Q' => Q) /\ (for each exception e, Q'_e => Q_e) *) +let hoare_frame_post_cond (post : exnpost) (fpost : exnpost) : form = + let post , epost = POE.destruct post in + let fpost, fepost = POE.destruct fpost in + let cond = f_imp post fpost in + let econd1 = TTC.merge2_poe_list fepost epost in + List.fold f_and cond econd1 + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. *) +let hoareS_frame_subgoals (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_frame) = + let env = LDecl.toenv hyps in + let p = hs_inv_rebind n.hfr_post (fst hs.hs_m) in + let cond = hoare_frame_post_cond p.hsi_inv (hs_po hs).hsi_inv in + let cond1, _, _ = + EcPlFrame.ss_frame_cond_S ~mk_other:false + env hs.hs_s hs.hs_m (hs_pr hs) { m = fst hs.hs_m; inv = cond } in + let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s p in + [cond1; cond2] + +let hoareF_frame_subgoals (hyps : LDecl.hyps) (hf : sHoareF) (n : hoare_frame) = + let env = LDecl.toenv hyps in + let p = hs_inv_rebind n.hfr_post hf.hf_m in + let cond = hoare_frame_post_cond p.hsi_inv (hf_po hf).hsi_inv in + let cond1, _, _ = + EcPlFrame.ss_frame_cond_F ~mk_other:false + env hyps hf.hf_f hf.hf_m (hf_pr hf) { m = hf.hf_m; inv = cond } in + let cond2 = f_hoareF (hf_pr hf) hf.hf_f p in + [cond1; cond2] + +(* -------------------------------------------------------------------- *) +(* Rules (TCB). *) +let t_hoareS_frame (r : hoare_frame) (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + FApi.xrule1 tc (RHoareSFrame r) + (hoareS_frame_subgoals (FApi.tc1_hyps tc) hs r) + +let t_hoareF_frame (r : hoare_frame) (tc : tcenv1) = + let hf = tc1_as_hoareF tc in + FApi.xrule1 tc (RHoareFFrame r) + (hoareF_frame_subgoals (FApi.tc1_hyps tc) hf r) + +(* -------------------------------------------------------------------- *) +(* Checkers: rerun the core, which recomputes the variables written by the + program — the soundness-critical part of framing — from the goal's own + context. *) +let () = + register_rule_checker + (function + | RHoareSFrame n -> + Some (EcPlRecheck.checker_of "hoareS-frame" pf_as_hoareS + (fun hyps hs -> hoareS_frame_subgoals hyps hs n)) + | RHoareFFrame n -> + Some (EcPlRecheck.checker_of "hoareF-frame" pf_as_hoareF + (fun hyps hf -> hoareF_frame_subgoals hyps hf n)) + | _ -> None) diff --git a/src/phl/rules/hoare/ecHoareFrame.mli b/src/phl/rules/hoare/ecHoareFrame.mli new file mode 100644 index 000000000..2f9ff6095 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareFrame.mli @@ -0,0 +1,37 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi +open EcAst + +(* ==================================================================== *) +(* Rules (trusted) *) + +type hoare_frame = { + hfr_post : hs_inv; (* new postcondition Q' (normal and exceptional) *) +} + +(* [t_hoareS_frame { hfr_post = Q' }] — framed weakening of the + postcondition: + + forall &m, P => forall (mod c), (Q' => Q) /\ (forall e, Q'_e => Q_e) + hoare [c : P ==> Q' | Q'_e] + --------------------------------------------------------------------- + hoare [c : P ==> Q | Q_e] + + where [mod c] are the program variables and globals written by [c], and + [Q_e] / [Q'_e] the exceptional postconditions. + + Node: [RHoareSFrame { hfr_post = Q' }]. Checker: "hoareS-frame"; it + recomputes [mod c] from the goal's context. *) +val t_hoareS_frame : hoare_frame -> backward + +(* [t_hoareF_frame { hfr_post = Q' }] — same for a procedure [f], also + quantifying over its result: + + forall &m, P => + forall (res : ret) (mod f), ((Q' => Q) /\ (forall e, Q'_e => Q_e))[res/result] + hoare [f : P ==> Q' | Q'_e] + --------------------------------------------------------------------- + hoare [f : P ==> Q | Q_e] + + Node: [RHoareFFrame { hfr_post = Q' }]. Checker: "hoareF-frame". *) +val t_hoareF_frame : hoare_frame -> backward