From 2a48281620e8bd3d772874993b8ff15864471d2c Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 9 Oct 2026 09:47:28 +0200 Subject: [PATCH] refactor(pl): weakmem as recheckable per-logic rules PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the `weakmem` tactic class: - new trusted rule per logic, `t__weakmem` (`rules/{hoare,ehoare,bdhoare,equiv}/EcWeakMem`; equiv: one side at a time): weakening of the memory of a judgement on a statement by fresh local variables it does not mention. The node records the typed variables (and the side); the pure builder restricts the goal's memory and re-checks that the variables are the last declared ones, fresh in the rest of the memory and unused by the judgement (new shared computation EcPlWeakMem); checkers "hoare-weakmem", "ehoare-weakmem", "bdhoare-weakmem", "equiv-weakmem". - the tactic is derived in each logic (`t__weakmem_hyp`): it cuts the hypothesis weakened by the variables, and closes the cut judgement by the rule (on each weakened side) and the hypothesis; the visible goal is the implication the tactic always produced. - EcPhlCodeTx.process_weakmem keeps the lookup of the hypothesis and the typing of the variables, and dispatches on the logic of the hypothesis; its interface is unchanged. The opaque `` `WeakenMem `` node is gone. Behaviour is preserved: same visible goal, same error messages in the same order. Validation: new test tests/weakmem.ec (every logic, each side and both sides for equiv, the error paths; passes with the reference build and this one under EC_RECHECK=1, with identical goals and error messages); stdlib and unit pass under EC_RECHECK=1 with no RecheckFailure; each checker, when broken, is caught only under EC_RECHECK=1, on the new test and, for "bdhoare-weakmem", on the stdlib (1 failure: Dexcepted.ec, the only use of weakmem; the other three rules are not used by the stdlib). --- src/phl/README.md | 6 +- src/phl/REFACTORING.md | 9 +- src/phl/ecPhlCodeTx.ml | 57 ++++----- src/phl/rules/bdhoare/ecBdHoareWeakMem.ml | 61 ++++++++++ src/phl/rules/bdhoare/ecBdHoareWeakMem.mli | 41 +++++++ src/phl/rules/ecPlWeakMem.ml | 65 ++++++++++ src/phl/rules/ecPlWeakMem.mli | 25 ++++ src/phl/rules/ehoare/ecEHoareWeakMem.ml | 61 ++++++++++ src/phl/rules/ehoare/ecEHoareWeakMem.mli | 41 +++++++ src/phl/rules/equiv/ecEquivWeakMem.ml | 80 +++++++++++++ src/phl/rules/equiv/ecEquivWeakMem.mli | 49 ++++++++ src/phl/rules/hoare/ecHoareWeakMem.ml | 61 ++++++++++ src/phl/rules/hoare/ecHoareWeakMem.mli | 41 +++++++ tests/weakmem.ec | 131 +++++++++++++++++++++ 14 files changed, 694 insertions(+), 34 deletions(-) create mode 100644 src/phl/rules/bdhoare/ecBdHoareWeakMem.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareWeakMem.mli create mode 100644 src/phl/rules/ecPlWeakMem.ml create mode 100644 src/phl/rules/ecPlWeakMem.mli create mode 100644 src/phl/rules/ehoare/ecEHoareWeakMem.ml create mode 100644 src/phl/rules/ehoare/ecEHoareWeakMem.mli create mode 100644 src/phl/rules/equiv/ecEquivWeakMem.ml create mode 100644 src/phl/rules/equiv/ecEquivWeakMem.mli create mode 100644 src/phl/rules/hoare/ecHoareWeakMem.ml create mode 100644 src/phl/rules/hoare/ecHoareWeakMem.mli create mode 100644 tests/weakmem.ec diff --git a/src/phl/README.md b/src/phl/README.md index 562fd8486..28a35b665 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -143,7 +143,7 @@ src/phl/ transforms/ EcTr: catalogue entries of the program transformations ecPl*.ml computations shared by the rules of every logic: EcPlFrame, EcPlSp, EcPlWp, EcPlRndSem, EcPlRCond, EcPlTransform, - EcPlMatch, EcPlFun, EcPlCall + EcPlMatch, EcPlFun, EcPlCall, EcPlWeakMem ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -158,6 +158,10 @@ src/phl/ - The `call` rules (`EcCall`) are logic rules on the call alone; `call` is derived (`seq` + rule), except in bdhoare, whose rule keeps its composite statement on `c; x <@ f(a)`. +- The `weakmem` rules (`EcWeakMem`) weaken the memory of a statement + judgement by fresh locals it does not mention; the `weakmem` tactic is + derived (cut of the weakened hypothesis, closed by the rule and the + hypothesis). - A rule relating two logics (e.g. the `pr` bridges) lives with the logic of its conclusion. - A rule concluding a probability statement from a judgement (`byphoare`, diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index d644e6dfb..d4ab01682 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -157,7 +157,9 @@ src/phl/ fresh program variables), EcPlFun (unfolding a procedure, the oracle conditions of the abstract-procedure rules, the single-call statement of `proc*`), EcPlCall (the - result assignment and argument substitution of a call) + result assignment and argument substitution of a call), + EcPlWeakMem (restricting a memory weakened by fresh local + variables) ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -183,6 +185,11 @@ uniform across logics or relate several judgements: `call` is derived (`seq`, then the rule); the bdhoare rule keeps its statement on `c; lv <@ f(a)` (implicit seq and framing: the bdhoare `seq` rule has extra premises); +- the `weakmem` rules (`EcWeakMem`; equiv: one side at a time) + weaken the memory of a judgement on a statement by fresh local + variables it does not mention (the shared computation in + `EcPlWeakMem`); the `weakmem` tactic is derived: a cut of the weakened + hypothesis, closed by the rule and the hypothesis; - a rule relating judgements of two logics (the `pr` bridges, `hoare` from `phoare`, …) lives with the logic of its conclusion; - a rule concluding a statement on probabilities from a judgement diff --git a/src/phl/ecPhlCodeTx.ml b/src/phl/ecPhlCodeTx.ml index da84ea3ed..4d0a8d6da 100644 --- a/src/phl/ecPhlCodeTx.ml +++ b/src/phl/ecPhlCodeTx.ml @@ -31,7 +31,8 @@ module TTC = EcProofTyping logic-agnostic dispatcher [t_transform] below, and no per-logic module. [weakmem] is not a program transformation (it changes the memory type - of the goal and adds an implication): it is not migrated. *) + of a hypothesis and adds an implication): it has its own rule in each + logic ([EcWeakMem], see [process_weakmem] below). *) (* -------------------------------------------------------------------- *) (* The memory and statement transformed: the program of the goal (hoare, @@ -180,11 +181,17 @@ let process_set_match (side, cpos, id, pattern) tc = tc (* -------------------------------------------------------------------- *) +(* [weakmem h (xs : t)]: the hypothesis [h], a judgement on a statement, + weakened by the fresh local variables [xs] (in the memory of the given + side for equiv, both memories by default), is added as a premise of the + goal. Derived in each logic (cut, then the [weakmem] rule of the logic + of [h], [EcWeakMem]); the variables are typed first, the logic + being then the one of [h]. *) let process_weakmem (side, id, params) tc = let open EcLocation in let hyps = FApi.tc1_hyps tc in let env = FApi.tc1_env tc in - let _, f = + let h, f = try LDecl.hyp_by_name (unloc id) hyps with LDecl.LdeclError _ -> tc_lookup_error !!tc ~loc:id.pl_loc `Local ([], unloc id) @@ -198,42 +205,28 @@ let process_weakmem (side, id, params) tc = let decls = List.map process_decl params in - let bind me = - try EcMemory.bindall decls me - with EcMemory.DuplicatedMemoryBinding x -> - tc_error ~loc:id.pl_loc !!tc "variable %s already declared" x in - - let h = + let t = match f.f_node with - | FhoareS hs -> - let _, mt = bind hs.hs_m in - f_hoareS mt (hs_pr hs) hs.hs_s (hs_po hs) - - | FeHoareS hs -> - let _, mt = bind hs.ehs_m in - f_eHoareS mt (ehs_pr hs) hs.ehs_s (ehs_po hs) - - | FbdHoareS hs -> - let _, mt = bind hs.bhs_m in - f_bdHoareS mt (bhs_pr hs) hs.bhs_s (bhs_po hs) hs.bhs_cmp (bhs_bd hs) - - | FequivS es -> - let do_side side (ml, mr) = - let es_ml, es_mr = if side = `Left then bind ml, mr else ml, bind mr in - (es_ml, es_mr) - in - let ((_, mtl), (_, mtr)) = - match side with - | None -> do_side `Left (do_side `Right (es.es_ml, es.es_mr)) - | Some side -> do_side side (es.es_ml, es.es_mr) in - f_equivS mtl mtr (es_pr es) es.es_sl es.es_sr (es_po es) + | FhoareS _ -> + EcHoareWeakMem.t_hoare_weakmem_hyp h { hwm_vars = decls } + + | FeHoareS _ -> + EcEHoareWeakMem.t_ehoare_weakmem_hyp h { ehwm_vars = decls } + + | FbdHoareS _ -> + EcBdHoareWeakMem.t_bdhoare_weakmem_hyp h { bwm_vars = decls } + + | FequivS _ -> + EcEquivWeakMem.t_equiv_weakmem_hyp h side decls | _ -> tc_error ~loc:id.pl_loc !!tc "the hypothesis need to be a hoare/phoare/ehoare/equiv on statement" in - let concl = f_imp h (FApi.tc1_goal tc) in - FApi.xmutate1 tc `WeakenMem [concl] + + try t tc + with EcMemory.DuplicatedMemoryBinding x -> + tc_error ~loc:id.pl_loc !!tc "variable %s already declared" x (* -------------------------------------------------------------------- *) (* [case <- p]: split the tuple assignment at [p]. The checks done before diff --git a/src/phl/rules/bdhoare/ecBdHoareWeakMem.ml b/src/phl/rules/bdhoare/ecBdHoareWeakMem.ml new file mode 100644 index 000000000..4b9e6ca9b --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareWeakMem.ml @@ -0,0 +1,61 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcPlWeakMem + +(* -------------------------------------------------------------------- *) +(* Parameter of the bdhoare [weakmem] rule: the variables declared in the + goal's memory, typed. Nothing to resolve: the same record is the rule + argument and the node payload. *) +type bdhoare_weakmem = { + bwm_vars : ovariable list; +} + +type EcCoreGoal.rule += RBdHoareWeakMem of bdhoare_weakmem + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + variables are the last ones declared in the memory, fresh in the rest + of it, and not used by the judgement) are re-checked by + [EcPlWeakMem.restrict], so the checker re-validates them. *) +let bdhoare_weakmem_subgoals + (hyps : LDecl.hyps) (hs : bdHoareS) (n : bdhoare_weakmem) += + let env = LDecl.toenv hyps in + let used = + used env (fst hs.bhs_m) hs.bhs_s [hs.bhs_pr; hs.bhs_po; hs.bhs_bd] in + [f_bdHoareS_r { hs with bhs_m = restrict env n.bwm_vars hs.bhs_m used }] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_bdhoare_weakmem (r : bdhoare_weakmem) (tc : tcenv1) = + let hs = tc1_as_bdhoareS tc in + let sg = + try bdhoare_weakmem_subgoals (FApi.tc1_hyps tc) hs r + with InvalidWeakening msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (RBdHoareWeakMem r) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareWeakMem n -> + Some (EcPlRecheck.checker_of "bdhoare-weakmem" pf_as_bdhoareS + (fun hyps hs -> bdhoare_weakmem_subgoals hyps hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): cut the hypothesis [h] weakened by the + variables, close the cut judgement by the rule and [h]. Raises + [EcMemory.DuplicatedMemoryBinding] (before acting) when a variable is + already declared. *) +let t_bdhoare_weakmem_hyp (h : EcIdent.t) (r : bdhoare_weakmem) (tc : tcenv1) = + let hs = destr_bdHoareS (LDecl.hyp_by_id h (FApi.tc1_hyps tc)) in + let hs = { hs with bhs_m = EcMemory.bindall r.bwm_vars hs.bhs_m } in + FApi.t_first + (FApi.t_seq (t_bdhoare_weakmem r) (EcLowGoal.t_apply_hyp h ~args:[] ~sk:0)) + (EcLowGoal.t_cut (f_bdHoareS_r hs) tc) diff --git a/src/phl/rules/bdhoare/ecBdHoareWeakMem.mli b/src/phl/rules/bdhoare/ecBdHoareWeakMem.mli new file mode 100644 index 000000000..fc598b8f5 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareWeakMem.mli @@ -0,0 +1,41 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_weakmem = { + bwm_vars : ovariable list; (* the variables, typed *) +} + +(* [t_bdhoare_weakmem { bwm_vars = xs }] — weakening of the memory: + + phoare [c : P ==> Q] <> b (memory m) + ------------------------------------------ m' = m + xs + phoare [c : P ==> Q] <> b (memory m') + + ([<>] any of [<=], [=], [>=]), where [m + xs] is [m] in which the + local program variables [xs] are declared ([EcMemory.bindall]). Side + conditions (re-checked by [EcPlWeakMem.restrict], otherwise fails): + [xs] are the last variables declared in the memory [m'] of the goal, + each fresh in [m], and none of them is read or written by [c] nor + occurs in [P], [Q] or [b] (the premise is well-formed in [m]). + + Node: [RBdHoareWeakMem { bwm_vars = xs }]. Checker: "bdhoare-weakmem". *) +val t_bdhoare_weakmem : bdhoare_weakmem -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_bdhoare_weakmem_hyp h { bwm_vars = xs }] — on any goal [G], [h] being + the hypothesis [phoare [c : P ==> Q] <> b] (memory [m]), with + [H' := phoare [c : P ==> Q] <> b] (memory [m + xs]): + 1. [EcLowGoal.t_cut] [H'], giving + (a) H', + (b) H' => G — left open; + 2. [t_bdhoare_weakmem] reduces (a) to [h], closed by [h]. + Visible goal: (b). Raises [EcMemory.DuplicatedMemoryBinding] (before + acting) when a variable of [xs] is already declared in [m]. Emits no + node of its own. *) +val t_bdhoare_weakmem_hyp : EcIdent.t -> bdhoare_weakmem -> backward diff --git a/src/phl/rules/ecPlWeakMem.ml b/src/phl/rules/ecPlWeakMem.ml new file mode 100644 index 000000000..e84554983 --- /dev/null +++ b/src/phl/rules/ecPlWeakMem.ml @@ -0,0 +1,65 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcTypes +open EcEnv +open EcPV + +(* -------------------------------------------------------------------- *) +(* Weakening of a memory, shared by the [weakmem] rules of every logic: a + judgement on a statement that holds in a memory [me] holds in [me] + extended with fresh local program variables [xs], which the judgement + does not mention. *) + +exception InvalidWeakening of string + +let invalid fmt = Format.kasprintf (fun msg -> raise (InvalidWeakening msg)) fmt + +(* -------------------------------------------------------------------- *) +(* The memory [me] is rebuilt from the declarations of [me'] that precede + [xs] (a memory being built by successive [EcMemory.bindall]), then + checked: binding [xs] in it must give back [me'] (which re-checks the + freshness of [xs]). *) +let restrict + (env : env) (xs : ovariable list) ((m, mt') : memenv) (used : PV.t) += + let name, decls' = + match EcMemory.for_printing mt' with + | None -> invalid "the memory has no local variables" + | Some x -> x in + + let n = List.length decls' - List.length xs in + let decls = List.filteri (fun i _ -> i < n) decls' in + let suffix = List.filteri (fun i _ -> i >= n) decls' in + + if n < 0 || not (List.all2 ov_equal xs suffix) then + invalid "the variables are not the last declared ones"; + + let mt = EcMemory.empty_local_mt ~witharg:(is_some name) in + let mt = + try EcMemory.bindall_mt decls mt + with EcMemory.DuplicatedMemoryBinding x -> + invalid "variable %s declared twice" x in + + let mt'' = + try EcMemory.bindall_mt xs mt + with EcMemory.DuplicatedMemoryBinding x -> + invalid "variable %s already declared" x in + + if not (EcMemory.mt_equal mt'' mt') then + invalid "the memory is not an extension of a memory by the variables"; + + List.iter (fun (x : ovariable) -> + x.ov_name |> oiter (fun x -> + if PV.mem_pv env (pv_loc x) used then + invalid "variable %s is used by the judgement" x)) + xs; + + (m, mt) + +(* -------------------------------------------------------------------- *) +let used (env : env) (m : memory) (s : stmt) (fs : form list) = + List.fold_left + (fun pv f -> PV.union pv (PV.fv env m f)) + (PV.union (s_read env s) (s_write env s)) + fs diff --git a/src/phl/rules/ecPlWeakMem.mli b/src/phl/rules/ecPlWeakMem.mli new file mode 100644 index 000000000..b3b19eddd --- /dev/null +++ b/src/phl/rules/ecPlWeakMem.mli @@ -0,0 +1,25 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcEnv +open EcPV + +(* -------------------------------------------------------------------- *) +(* Weakening of a memory, shared by the [weakmem] rules of every logic: a + judgement on a statement that holds in a memory [me] holds in [me] + extended with fresh local program variables [xs], which the judgement + does not mention. *) + +exception InvalidWeakening of string + +(* [restrict env xs me' used] is the memory [me] such that + [me' = EcMemory.bindall xs me] (same memory identifier): [xs] are the + last variables declared in [me'], each fresh in [me]. The program + variables [used] by the judgement must not include [xs], so that the + judgement is well-formed in [me]. Raises [InvalidWeakening] + otherwise. *) +val restrict : env -> ovariable list -> memenv -> PV.t -> memenv + +(* [used env m s fs]: the program variables read or written by [s], + joined with the program variables of memory [m] in the formulas + [fs]. *) +val used : env -> memory -> stmt -> form list -> PV.t diff --git a/src/phl/rules/ehoare/ecEHoareWeakMem.ml b/src/phl/rules/ehoare/ecEHoareWeakMem.ml new file mode 100644 index 000000000..04f20f5dc --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareWeakMem.ml @@ -0,0 +1,61 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcPlWeakMem + +(* -------------------------------------------------------------------- *) +(* Parameter of the ehoare [weakmem] rule: the variables declared in the + goal's memory, typed. Nothing to resolve: the same record is the rule + argument and the node payload. *) +type ehoare_weakmem = { + ehwm_vars : ovariable list; +} + +type EcCoreGoal.rule += REHoareWeakMem of ehoare_weakmem + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + variables are the last ones declared in the memory, fresh in the rest + of it, and not used by the judgement) are re-checked by + [EcPlWeakMem.restrict], so the checker re-validates them. *) +let ehoare_weakmem_subgoals + (hyps : LDecl.hyps) (hs : eHoareS) (n : ehoare_weakmem) += + let env = LDecl.toenv hyps in + let used = + used env (fst hs.ehs_m) hs.ehs_s [hs.ehs_pr; hs.ehs_po] in + [f_eHoareS_r { hs with ehs_m = restrict env n.ehwm_vars hs.ehs_m used }] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_ehoare_weakmem (r : ehoare_weakmem) (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + let sg = + try ehoare_weakmem_subgoals (FApi.tc1_hyps tc) hs r + with InvalidWeakening msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REHoareWeakMem r) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareWeakMem n -> + Some (EcPlRecheck.checker_of "ehoare-weakmem" pf_as_ehoareS + (fun hyps hs -> ehoare_weakmem_subgoals hyps hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): cut the hypothesis [h] weakened by the + variables, close the cut judgement by the rule and [h]. Raises + [EcMemory.DuplicatedMemoryBinding] (before acting) when a variable is + already declared. *) +let t_ehoare_weakmem_hyp (h : EcIdent.t) (r : ehoare_weakmem) (tc : tcenv1) = + let hs = destr_eHoareS (LDecl.hyp_by_id h (FApi.tc1_hyps tc)) in + let hs = { hs with ehs_m = EcMemory.bindall r.ehwm_vars hs.ehs_m } in + FApi.t_first + (FApi.t_seq (t_ehoare_weakmem r) (EcLowGoal.t_apply_hyp h ~args:[] ~sk:0)) + (EcLowGoal.t_cut (f_eHoareS_r hs) tc) diff --git a/src/phl/rules/ehoare/ecEHoareWeakMem.mli b/src/phl/rules/ehoare/ecEHoareWeakMem.mli new file mode 100644 index 000000000..7a188df28 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareWeakMem.mli @@ -0,0 +1,41 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +type ehoare_weakmem = { + ehwm_vars : ovariable list; (* the variables, typed *) +} + +(* [t_ehoare_weakmem { ehwm_vars = xs }] — weakening of the memory: + + ehoare [c : P ==> Q] (memory m) + ------------------------------------------ m' = m + xs + ehoare [c : P ==> Q] (memory m') + + where [m + xs] is [m] in which the local program variables [xs] are + declared ([EcMemory.bindall]). Side conditions (re-checked by + [EcPlWeakMem.restrict], otherwise fails): [xs] are the last variables + declared in the memory [m'] of the goal, each fresh in [m], and none + of them is read or written by [c] nor occurs in [P] or [Q] (the + premise is well-formed in [m]). + + Node: [REHoareWeakMem { ehwm_vars = xs }]. Checker: "ehoare-weakmem". *) +val t_ehoare_weakmem : ehoare_weakmem -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_ehoare_weakmem_hyp h { ehwm_vars = xs }] — on any goal [G], [h] being + the hypothesis [ehoare [c : P ==> Q]] (memory [m]), with + [H' := ehoare [c : P ==> Q]] (memory [m + xs]): + 1. [EcLowGoal.t_cut] [H'], giving + (a) H', + (b) H' => G — left open; + 2. [t_ehoare_weakmem] reduces (a) to [h], closed by [h]. + Visible goal: (b). Raises [EcMemory.DuplicatedMemoryBinding] (before + acting) when a variable of [xs] is already declared in [m]. Emits no + node of its own. *) +val t_ehoare_weakmem_hyp : EcIdent.t -> ehoare_weakmem -> backward diff --git a/src/phl/rules/equiv/ecEquivWeakMem.ml b/src/phl/rules/equiv/ecEquivWeakMem.ml new file mode 100644 index 000000000..34266d406 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivWeakMem.ml @@ -0,0 +1,80 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcPlWeakMem + +(* -------------------------------------------------------------------- *) +(* Parameters of the equiv [weakmem] rule: the side whose memory is + weakened and the variables declared in it, typed. Nothing to resolve: + the same record is the rule argument and the node payload. *) +type equiv_weakmem = { + ewm_side : side; + ewm_vars : ovariable list; +} + +type EcCoreGoal.rule += REquivWeakMem of equiv_weakmem + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + variables are the last ones declared in the memory of the side, fresh + in the rest of it, and not used by the judgement on that side) are + re-checked by [EcPlWeakMem.restrict], so the checker re-validates + them. *) +let equiv_weakmem_subgoals + (hyps : LDecl.hyps) (es : equivS) (n : equiv_weakmem) += + let env = LDecl.toenv hyps in + let me, s = sideif n.ewm_side (es.es_ml, es.es_sl) (es.es_mr, es.es_sr) in + let me = restrict env n.ewm_vars me + (used env (fst me) s [es.es_pr; es.es_po]) in + let es = + match n.ewm_side with + | `Left -> { es with es_ml = me } + | `Right -> { es with es_mr = me } in + [f_equivS_r es] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_equiv_weakmem (r : equiv_weakmem) (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_weakmem_subgoals (FApi.tc1_hyps tc) es r + with InvalidWeakening msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REquivWeakMem r) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivWeakMem n -> + Some (EcPlRecheck.checker_of "equiv-weakmem" pf_as_equivS + (fun hyps es -> equiv_weakmem_subgoals hyps es n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): cut the hypothesis [h] weakened by the + variables on the given side(s) (both when [side] is [None]: the right + memory first, then the left one), reduce the cut judgement to [h] by + the rule on each weakened side and close it by [h]. Raises + [EcMemory.DuplicatedMemoryBinding] (before acting) when a variable is + already declared. *) +let t_equiv_weakmem_hyp + (h : EcIdent.t) (side : oside) (xs : ovariable list) (tc : tcenv1) += + let es = destr_equivS (LDecl.hyp_by_id h (FApi.tc1_hyps tc)) in + let sides = match side with None -> [`Right; `Left] | Some s -> [s] in + let weaken es = function + | `Left -> { es with es_ml = EcMemory.bindall xs es.es_ml } + | `Right -> { es with es_mr = EcMemory.bindall xs es.es_mr } in + let es = List.fold_left weaken es sides in + let t_rule s = t_equiv_weakmem { ewm_side = s; ewm_vars = xs } in + FApi.t_first + (FApi.t_seqs + (List.map t_rule sides @ [EcLowGoal.t_apply_hyp h ~args:[] ~sk:0])) + (EcLowGoal.t_cut (f_equivS_r es) tc) diff --git a/src/phl/rules/equiv/ecEquivWeakMem.mli b/src/phl/rules/equiv/ecEquivWeakMem.mli new file mode 100644 index 000000000..8768becd9 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivWeakMem.mli @@ -0,0 +1,49 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcAst +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_weakmem = { + ewm_side : side; (* weakened side *) + ewm_vars : ovariable list; (* the variables, typed *) +} + +(* [t_equiv_weakmem { ewm_side = `Left; ewm_vars = xs }] — weakening of + the memory of one side: + + equiv [c ~ d : P ==> Q] (memories m1, m2) + ----------------------------------------------- m1' = m1 + xs + equiv [c ~ d : P ==> Q] (memories m1', m2) + + (symmetrically for [`Right]; the other memory is unchanged), where + [m1 + xs] is [m1] in which the local program variables [xs] are + declared ([EcMemory.bindall]). Side conditions (re-checked by + [EcPlWeakMem.restrict], otherwise fails): [xs] are the last variables + declared in the memory [m1'] of the goal, each fresh in [m1], and none + of them is read or written by [c] nor occurs, on [&1], in [P] or [Q] + (the premise is well-formed in [m1]). + + Node: [REquivWeakMem { ewm_side; ewm_vars = xs }]. Checker: + "equiv-weakmem". *) +val t_equiv_weakmem : equiv_weakmem -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_equiv_weakmem_hyp h side xs] — on any goal [G], [h] being the + hypothesis [equiv [c ~ d : P ==> Q]] (memories [m1], [m2]), with [H'] + the same judgement with [xs] declared in the memory of [side] (in both + memories when [side] is [None]): + 1. [EcLowGoal.t_cut] [H'], giving + (a) H', + (b) H' => G — left open; + 2. [t_equiv_weakmem] on each weakened side reduces (a) to [h], closed + by [h]. + Visible goal: (b). Raises [EcMemory.DuplicatedMemoryBinding] (before + acting) when a variable of [xs] is already declared in a weakened + memory (the right one checked first). Emits no node of its own. *) +val t_equiv_weakmem_hyp : + EcIdent.t -> oside -> ovariable list -> backward diff --git a/src/phl/rules/hoare/ecHoareWeakMem.ml b/src/phl/rules/hoare/ecHoareWeakMem.ml new file mode 100644 index 000000000..5857c0cdd --- /dev/null +++ b/src/phl/rules/hoare/ecHoareWeakMem.ml @@ -0,0 +1,61 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcPlWeakMem + +(* -------------------------------------------------------------------- *) +(* Parameter of the hoare [weakmem] rule: the variables declared in the + goal's memory, typed. Nothing to resolve: the same record is the rule + argument and the node payload. *) +type hoare_weakmem = { + hwm_vars : ovariable list; +} + +type EcCoreGoal.rule += RHoareWeakMem of hoare_weakmem + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + variables are the last ones declared in the memory, fresh in the rest + of it, and not used by the judgement) are re-checked by + [EcPlWeakMem.restrict], so the checker re-validates them. *) +let hoare_weakmem_subgoals + (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_weakmem) += + let env = LDecl.toenv hyps in + let used = + used env (fst hs.hs_m) hs.hs_s (hs.hs_pr :: POE.to_list hs.hs_po) in + [f_hoareS_r { hs with hs_m = restrict env n.hwm_vars hs.hs_m used }] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). *) +let t_hoare_weakmem (r : hoare_weakmem) (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let sg = + try hoare_weakmem_subgoals (FApi.tc1_hyps tc) hs r + with InvalidWeakening msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (RHoareWeakMem r) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareWeakMem n -> + Some (EcPlRecheck.checker_of "hoare-weakmem" pf_as_hoareS + (fun hyps hs -> hoare_weakmem_subgoals hyps hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): cut the hypothesis [h] weakened by the + variables, close the cut judgement by the rule and [h]. Raises + [EcMemory.DuplicatedMemoryBinding] (before acting) when a variable is + already declared. *) +let t_hoare_weakmem_hyp (h : EcIdent.t) (r : hoare_weakmem) (tc : tcenv1) = + let hs = destr_hoareS (LDecl.hyp_by_id h (FApi.tc1_hyps tc)) in + let hs = { hs with hs_m = EcMemory.bindall r.hwm_vars hs.hs_m } in + FApi.t_first + (FApi.t_seq (t_hoare_weakmem r) (EcLowGoal.t_apply_hyp h ~args:[] ~sk:0)) + (EcLowGoal.t_cut (f_hoareS_r hs) tc) diff --git a/src/phl/rules/hoare/ecHoareWeakMem.mli b/src/phl/rules/hoare/ecHoareWeakMem.mli new file mode 100644 index 000000000..9bf5d4581 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareWeakMem.mli @@ -0,0 +1,41 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +type hoare_weakmem = { + hwm_vars : ovariable list; (* the variables, typed *) +} + +(* [t_hoare_weakmem { hwm_vars = xs }] — weakening of the memory: + + hoare [c : P ==> Q | E] (memory m) + ------------------------------------------ m' = m + xs + hoare [c : P ==> Q | E] (memory m') + + where [m + xs] is [m] in which the local program variables [xs] are + declared ([EcMemory.bindall]). Side conditions (re-checked by + [EcPlWeakMem.restrict], otherwise fails): [xs] are the last variables + declared in the memory [m'] of the goal, each fresh in [m], and none + of them is read or written by [c] nor occurs in [P], [Q] or [E] (the + premise is well-formed in [m]). + + Node: [RHoareWeakMem { hwm_vars = xs }]. Checker: "hoare-weakmem". *) +val t_hoare_weakmem : hoare_weakmem -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +(* [t_hoare_weakmem_hyp h { hwm_vars = xs }] — on any goal [G], [h] being + the hypothesis [hoare [c : P ==> Q | E]] (memory [m]), with + [H' := hoare [c : P ==> Q | E]] (memory [m + xs]): + 1. [EcLowGoal.t_cut] [H'], giving + (a) H', + (b) H' => G — left open; + 2. [t_hoare_weakmem] reduces (a) to [h], closed by [h]. + Visible goal: (b). Raises [EcMemory.DuplicatedMemoryBinding] (before + acting) when a variable of [xs] is already declared in [m]. Emits no + node of its own. *) +val t_hoare_weakmem_hyp : EcIdent.t -> hoare_weakmem -> backward diff --git a/tests/weakmem.ec b/tests/weakmem.ec new file mode 100644 index 000000000..f8149be9b --- /dev/null +++ b/tests/weakmem.ec @@ -0,0 +1,131 @@ +(* The `weakmem` tactic: a hypothesis, a judgement on a statement, is + weakened by fresh local variables declared in its memory (through the + weakmem rule of its logic: hoare, ehoare, phoare and equiv, on each + side and on both sides at once), and added as a premise of the goal; + and the error paths. Each tactic is a separate sentence, so that the + goals it leaves can be compared across builds. *) +require import AllCore Xreal. + +(* Turns the goal [G] into [G] and [G => G], so that a judgement on a + statement can be a hypothesis. *) +lemma dup (b : bool) : b => (b => b) => b. +proof. by []. qed. + +module M = { + var g : int + + proc f() : int = { + var x : int; + x <- 1; + return x; + } + + proc h() : unit = { + M.g <- 1; + } +}. + +(* -------------------------------------------------------------------- *) +(* hoare: the weakened hypothesis proves the judgement on the memory + extended by [alias]. *) +lemma L_hoare : hoare [M.f : true ==> res = 1]. +proof. +proc. +apply dup; first by auto. +move=> h. +alias 1 y = 0. +weakmem h (y : int). +move=> h'. +seq 1 : true. +- by auto. +exact h'. +qed. + +(* several variables, an anonymous one, and a side (ignored) *) +lemma L_hoare_multi : hoare [M.f : true ==> res = 1]. +proof. +proc. +apply dup; first by auto. +move=> h. +weakmem h (y : int, _ : bool, z : int * bool). +move=> _. +weakmem {2} h (y : int). +move=> _. +weakmem h (). +move=> _. +exact h. +qed. + +(* the errors *) +lemma L_hoare_err : hoare [M.f : true ==> res = 1]. +proof. +proc. +apply dup; first by auto. +move=> h. +have t : true by done. +fail weakmem nosuchhyp (y : int). +fail weakmem t (y : int). +fail weakmem h (x : int). +fail weakmem h (y : int, y : bool). +fail weakmem h (y). +fail weakmem h (y : nosuchtype). +exact h. +qed. + +(* -------------------------------------------------------------------- *) +(* ehoare *) +lemma L_ehoare : ehoare [M.h : (1%xr) ==> (1%xr)]. +proof. +proc. +apply dup; first by auto. +move=> h. +weakmem h (y : int). +move=> h'. +fail weakmem h (y y : int). +exact h. +qed. + +(* -------------------------------------------------------------------- *) +(* phoare *) +lemma L_phoare : phoare [M.f : true ==> res = 1] = 1%r. +proof. +proc. +apply dup; first by auto. +move=> h. +weakmem h (y : int, z : bool). +move=> h'. +fail weakmem h (x : int). +exact h. +qed. + +(* -------------------------------------------------------------------- *) +(* equiv: each side, and both sides *) +lemma L_equiv : equiv [M.f ~ M.f : true ==> ={res}]. +proof. +proc. +apply dup; first by auto. +move=> h. +weakmem {1} h (y : int). +move=> h1. +weakmem {2} h (y z : int). +move=> h2. +weakmem h (y : int). +move=> h3. +alias{1} 1 y = 0. +alias{2} 1 y = 0. +seq 1 1 : true. +- by auto. +exact h3. +qed. + +lemma L_equiv_err : equiv [M.f ~ M.f : true ==> ={res}]. +proof. +proc. +apply dup; first by auto. +move=> h. +fail weakmem h (x : int). +fail weakmem {1} h (x : int). +fail weakmem {2} h (x : int). +fail weakmem h (y y : int). +exact h. +qed.