From b2ec4e803046914775a74e74c713a25edca3c42b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 10 Jun 2026 17:07:39 +0200 Subject: [PATCH 1/4] phl: recheckable proof-node scaffolding + hoare-seq pilot MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Begin the src/phl reorganization into a four-layer spine (dispatch / elaboration / TCB rule / checker) with re-checkable proof-nodes, applied one tactic at a time. Kernel (ecCoreGoal): - open `type rule = ..` and a new `VRule of rule * handle list` validation node (the recheckable sibling of the opaque `VExtern`); - `FApi.xrule[1][_hyps]` emitting `VRule`; - a checker registry (`register_rule_checker`) over the open rule type, `recheck_proofenv` driver, and `RecheckFailure`. The driver runs at qed (ecScope.save_r) gated by the EC_RECHECK env var; unmigrated `VExtern` nodes and rules without a registered checker are skipped, so migration is incremental. Pilot: hoare `seq` migrated to rules/hoare/ecHoareSeq.ml — pure subgoal-builder shared by the rule and its checker, `RHoareSeq` node recording the split position + intermediate assertion. EcPhlSeq routes its hoareS arm here and re-exports t_hoare_seq, so the public interface and external callers are unchanged. Docs: src/phl/README.md (spine + layout convention) and src/phl/REFACTORING.md (plan, rationale, per-tactic recipe). Validated: 91 stdlib theories + 23 seq-using tests compile under EC_RECHECK=1 with zero RecheckFailure. --- src/ecCoreGoal.ml | 76 ++++++++++++ src/ecCoreGoal.mli | 33 +++++ src/ecScope.ml | 4 +- src/phl/README.md | 77 ++++++++++++ src/phl/REFACTORING.md | 191 +++++++++++++++++++++++++++++ src/phl/ecPhlSeq.ml | 23 +--- src/phl/rules/hoare/ecHoareSeq.ml | 71 +++++++++++ src/phl/rules/hoare/ecHoareSeq.mli | 14 +++ 8 files changed, 471 insertions(+), 18 deletions(-) create mode 100644 src/phl/README.md create mode 100644 src/phl/REFACTORING.md create mode 100644 src/phl/rules/hoare/ecHoareSeq.ml create mode 100644 src/phl/rules/hoare/ecHoareSeq.mli diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 4b75e5b0c1..67b1008514 100644 --- a/src/ecCoreGoal.ml +++ b/src/ecCoreGoal.ml @@ -125,6 +125,14 @@ type rwproofterm = { rpt_lc : ident option; } +(* -------------------------------------------------------------------- *) +(* An open (extensible) type of recheckable proof-rule nodes. Each tactic + that produces a trusted (TCB) judgement extends [rule] with a constructor + carrying exactly the parameters needed to recompute its subgoals, and + registers a checker (see [register_rule_checker]). The kernel never needs + to know the payload types: dispatch is by a registry of partial handlers. *) +type rule = .. + (* -------------------------------------------------------------------- *) type proof = { pr_env : proofenv; @@ -161,6 +169,10 @@ and validation = (* external (hl/phl/prhl/...) proof-node *) | VExtern : 'a * handle list -> validation + (* recheckable external proof-node: the [rule] carries enough information + to recompute (and thus re-validate) the listed subgoals. *) +| VRule of rule * handle list + and tcenv1 = { tce_penv : proofenv; (* top-level proof environment *) tce_ctxt : tcenv_ctxt; (* context *) @@ -528,6 +540,30 @@ module FApi = struct let xmutate1_hyps (tc : tcenv1) (vx : 'a) subgoals = xmutate_hyps (tcenv_of_tcenv1 tc) vx subgoals + (* ------------------------------------------------------------------ *) + (* Same as [xmutate], but emit a recheckable [VRule] node. [r] must carry + the parameters its registered checker needs to recompute [fp]. *) + let xrule (tc : tcenv) (r : rule) (fp : form list) = + let (tc, hds) = List.map_fold (fun tc fp -> newgoal tc fp) tc fp in + close tc (VRule (r, hds)) + + (* ------------------------------------------------------------------ *) + let xrule1 (tc : tcenv1) (r : rule) (fp : form list) = + xrule (tcenv_of_tcenv1 tc) r fp + + (* ------------------------------------------------------------------ *) + let xrule_hyps (tc : tcenv) (r : rule) subgoals = + let (tc, hds) = + List.map_fold + (fun tc (hyps, fp) -> newgoal tc ~hyps fp) + tc subgoals + in + close tc (VRule (r, hds)) + + (* ------------------------------------------------------------------ *) + let xrule1_hyps (tc : tcenv1) (r : rule) subgoals = + xrule_hyps (tcenv_of_tcenv1 tc) r subgoals + (* ------------------------------------------------------------------ *) let newfact (pe : proofenv) vx hyps concl = snd_map (fun x -> x.g_uid) (pf_newgoal pe ~vx:vx hyps concl) @@ -984,6 +1020,46 @@ let proof_of_tcenv (tc : tcenv) = let proofenv_of_proof (pf : proof) = pf.pr_env +(* -------------------------------------------------------------------- *) +(* Rechecking of [VRule] proof-nodes. + + A checker is given the proof environment, the node's (closed) goal and the + pregoals of the subgoals the rule produced. It must re-derive what subgoals + the rule should yield for that goal and confirm they match what was + recorded, raising [RecheckFailure] otherwise. Checkers are registered as + partial handlers over the open [rule] type. *) +exception RecheckFailure of string + +type rule_checker = proofenv -> pregoal -> pregoal list -> unit + +let rule_checkers : (rule -> rule_checker option) list ref = ref [] + +let register_rule_checker (f : rule -> rule_checker option) = + rule_checkers := f :: !rule_checkers + +let find_rule_checker (r : rule) : rule_checker option = + let rec aux = function + | [] -> None + | f :: fs -> (match f r with Some _ as x -> x | None -> aux fs) + in aux !rule_checkers + +(* Recheck every [VRule] node of [pe]. Nodes whose rule has no registered + checker are left untouched (not yet migrated); all other validation kinds + are trusted by construction. *) +let recheck_proofenv (pe : proofenv) = + ID.Map.iter (fun _ (g : goal) -> + match g.g_validation with + | Some (VRule (r, hds)) -> begin + match find_rule_checker r with + | None -> () + | Some chk -> + let subs = + List.map + (fun hd -> (FApi.get_goal_by_id hd pe).g_goal) hds in + chk pe g.g_goal subs + end + | _ -> ()) pe.pr_goals + (* -------------------------------------------------------------------- *) let start (hyps : LDecl.hyps) (goal : form) = let uid = ID.gen () in diff --git a/src/ecCoreGoal.mli b/src/ecCoreGoal.mli index f574b49bf3..16342dadae 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -146,6 +146,11 @@ type pregoal = { g_concl : form; } +(* An open (extensible) type of recheckable proof-rule nodes. Each TCB tactic + extends [rule] with a constructor carrying the parameters needed to + recompute its subgoals, and registers a checker (see below). *) +type rule = .. + type validation = | VSmt (* SMT call *) | VAdmit (* admit *) @@ -159,6 +164,9 @@ type validation = (* external (hl/phl/prhl/...) proof-node *) | VExtern : 'a * handle list -> validation + (* recheckable external proof-node *) +| VRule of rule * handle list + (* -------------------------------------------------------------------- *) type location = { plc_parent : location option; @@ -186,6 +194,22 @@ val tcenv_of_proof : proof -> tcenv val proof_of_tcenv : tcenv -> proof val proofenv_of_proof : proof -> proofenv +(* -------------------------------------------------------------------- *) +(* Rechecking of [VRule] proof-nodes. A [rule_checker] receives the proof + * environment, the node's (closed) goal and the pregoals of the subgoals the + * rule produced; it must re-derive the expected subgoals and confirm they + * match, raising [RecheckFailure] otherwise. Checkers are registered as + * partial handlers over the open [rule] type. *) +exception RecheckFailure of string + +type rule_checker = proofenv -> pregoal -> pregoal list -> unit + +val register_rule_checker : (rule -> rule_checker option) -> unit + +(* Recheck every [VRule] node reachable in this proof environment. Unregistered + * rules and non-[VRule] validations are skipped. *) +val recheck_proofenv : proofenv -> unit + (* Start a new interactive proof in a given local context * [LDecl.hyps] for given [form]. Mainly, a [proof] records the set * of all goals (closed or not - i.e. a proof-environment) + the list @@ -289,6 +313,15 @@ module FApi : sig val xmutate_hyps : tcenv -> 'a -> (LDecl.hyps * form) list -> tcenv val xmutate1_hyps : tcenv1 -> 'a -> (LDecl.hyps * form) list -> tcenv + (* Same as [xmutate], but emit a recheckable [VRule] node. The [rule] must + * carry the parameters its registered checker needs to recompute the + * subgoals. *) + val xrule : tcenv -> rule -> form list -> tcenv + val xrule1 : tcenv1 -> rule -> form list -> tcenv + + val xrule_hyps : tcenv -> rule -> (LDecl.hyps * form) list -> tcenv + val xrule1_hyps : tcenv1 -> rule -> (LDecl.hyps * form) list -> tcenv + (* Apply a forward tactic to a backward environment, using the * proof-environment of the latter *) val bwd1_of_fwd : forward -> tcenv1 -> tcenv1 * handle diff --git a/src/ecScope.ml b/src/ecScope.ml index c6f1ff7fdb..5e9d7f0032 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1076,7 +1076,9 @@ module Ax = struct | PSCheck _ when mode <> `Save -> () | PSCheck pf -> begin if not (EcCoreGoal.closed pf) then - hierror "cannot save an incomplete proof" + hierror "cannot save an incomplete proof"; + if EcUtils.is_some (Sys.getenv_opt "EC_RECHECK") then + EcCoreGoal.recheck_proofenv (EcCoreGoal.proofenv_of_proof pf) end end; (pac, pct) in diff --git a/src/phl/README.md b/src/phl/README.md new file mode 100644 index 0000000000..487d0c1421 --- /dev/null +++ b/src/phl/README.md @@ -0,0 +1,77 @@ +# Program-logic tactics (`src/phl`) + +This directory is being reorganized around a uniform, recheckable structure. +This note records the target layout and the per-tactic spine. It is being +applied **one tactic at a time**; until a tactic is migrated it keeps its old +shape (one `ecPhl.ml` holding every logic). + +## The four-layer spine + +Every tactic is decomposed into the same layers, so that typing, dispatch and +the trusted core are separated and each TCB step is re-checkable: + +``` +DISPATCH process_ logic-agnostic. Inspects the goal kind and + │ routes. The ONLY place is_hoareS / f_node + │ matching belongs. No typing here. + ▼ +ELABORATION process__ the goal kind is known. Type the parse-tree + │ arguments in that logic's memory and build + │ the typed rule parameters, then call the rule. + ▼ +RULE (TCB) t__ compute the subgoals from the typed params + │ and emit a recheckable node carrying THOSE + │ params: FApi.xrule1 tc (R... params) subgoals. + ▼ +CHECKER check__ read the params back from the node, recompute + the subgoals via the SAME pure core, and + confirm they match (is_conv) what was stored. +``` + +Key rule: the rule and its checker share one **pure subgoal-builder** +(`__subgoals : env -> -> params -> form list`). The +checker is then "rerun the builder and compare", which is why recording the +params in the node is all that recheckability costs. + +Derived (non-TCB) tactics that only orchestrate other tactics emit **no** node +and need **no** checker — rechecking recurses into the rules they expand to. + +## Recheckable proof-nodes + +The kernel ([`ecCoreGoal`](../ecCoreGoal.mli)) provides: + +- `type rule = ..` — an open type. Each migrated tactic adds one constructor, + e.g. `type EcCoreGoal.rule += RHoareSeq of codegap1 * ss_inv`. +- `FApi.xrule1 tc r subgoals` — like `xmutate1` but emits a recheckable + `VRule (r, _)` node instead of an opaque `VExtern`. +- `register_rule_checker : (rule -> rule_checker option) -> unit` — register a + partial handler that, for your constructor, returns its checker. +- `recheck_proofenv` — walks a finished proof and runs every registered checker. + It is invoked at `qed` time when the `EC_RECHECK` environment variable is set + (see `ecScope.save_r`); unmigrated `VExtern` nodes are skipped. + +Run the test suite with `EC_RECHECK=1` to exercise every migrated checker. + +## Directory layout + +`(include_subdirs unqualified)` in `src/dune` slurps everything under `src/` +into one flat-namespace library, so subdirectories are purely organizational — +**module names must stay globally unique** (keep the `Ec` prefix; +directories are for humans). + +``` +src/phl/ + rules/ genuine logic rules (different subgoals per logic) + hoare/ ehoare/ bdhoare/ equiv/ eager/ + codetx/ logic-uniform program transforms (wp, sp, inline, swap, rcond, …) + bridge/ probabilistic / cross-logic bridges (deno, pr, byequiv, fel, upto) + multi/ multi-logic tactics with shared machinery (conseq, trans, sym) + ecPhl.ml legacy, thin dispatchers, not-yet-migrated tactics +``` + +## Migrated so far + +- **hoare `seq`** — [`rules/hoare/ecHoareSeq.ml`](rules/hoare/ecHoareSeq.ml). + The reference example of the full spine + checker. `EcPhlSeq.process_seq` + dispatches its `hoareS` arm here; `EcPhlSeq.t_hoare_seq` re-exports the rule + so existing callers and the public interface are unchanged. diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md new file mode 100644 index 0000000000..71910a51b5 --- /dev/null +++ b/src/phl/REFACTORING.md @@ -0,0 +1,191 @@ +# Program-logic (`src/phl`) refactoring — plan & rationale + +This is the design document for the long-running reorganization of EasyCrypt's +program logic. The companion [README.md](README.md) is the short, stable +"how a migrated tactic is structured" reference; this file records the *why*, +the full plan, and the per-tactic migration recipe. Work proceeds **one tactic +at a time**. + +--- + +## 1. Motivation — what was wrong + +The original `src/phl` is ~75 files, one `.ml`/`.mli` pair per *tactic* +(`ecPhlSeq`, `ecPhlWhile`, …), each holding **every logic** for that tactic. +Concretely: + +1. **Typing entangled with dispatch.** `process_` interleaves + "which logic is this goal?" (`is_hoareS`, `match concl.f_node`) with + "type this formula in that logic's memory". You cannot read one logic's rule + without reading all the others' arms. +2. **Inconsistent dispatch.** Some tactics match `concl.f_node`, some use `is_*` + predicates, some add an extra `ecPhlHi` file — no principled layer. +3. **Proof-nodes are not recheckable.** Low-level (TCB) tactics close goals with + `FApi.xmutate1 tc \`Tag [subgoals]`. The tag (`` `HlApp ``, `` `While ``, …) + carries **no parameters** and is **never destructed anywhere in the tree**. + The data justifying the step (split position, intermediate assertion, + bijection, invariant) is discarded, so a node cannot be re-validated. + `FApi.close` trusts every tactic unconditionally; there is no checker kernel. +4. **TCB vs derived is implicit** — only discoverable by grepping for `xmutate` + (30 of 37 `.ml` files are TCB; 7 are pure orchestration). +5. **A logic is scattered** — auditing "everything in the equiv logic" means + opening ~30 files. + +## 2. Findings about the current engine (so the plan is grounded) + +- **TCB boundary** is `FApi.xmutate / close` ([ecCoreGoal.ml](../ecCoreGoal.ml)). + A node is `VExtern : 'a * handle list` — a GADT existential, so a generic + traversal cannot even inspect the tag. +- **Dispatch wiring**: `process1_phl` in [ecHiTacticals.ml](../ecHiTacticals.ml) + maps each `EcParsetree` tactic constructor (`Pseq`, `Pwhile`, …) to a + `process_*` function. +- **Goal classification** lives in `ecCoreFol` (`is_hoareS`/`destr_hoareS`/…) and + `ecLowPhlGoal` (`tc1_as_hoareS`/`pf_as_hoareS`/…). +- **Three tactic families** (this drives the directory layout, §5): + - *logic rules* — genuinely different subgoals per logic: seq, while, call, + cond, rnd, conseq, fun, exists. + - *code transforms* — transform the program statement and re-wrap in the + **same** judgement; logic enters only as "grab the stmt+memory", so the core + is shared across logics: wp, sp, inline, swap, rcond, fission/fusion/unroll/ + splitwhile, kill/alias/cfold, outline, rwequiv. + - *bridges / multi-logic* — deno, pr, byequiv, fel, upto, eager; and the + special multi-logic tactics conseq/trans/sym that operate across judgements. + +## 3. Target architecture — the four-layer spine + +Every tactic is decomposed into the same four layers: + +``` +DISPATCH process_ logic-agnostic. Inspect goal kind, route. + │ Only place is_hoareS / f_node lives. No typing. + ▼ +ELABORATION process__ goal kind known; type parse-tree args in that + │ logic's memory, build typed params, call rule. + ▼ +RULE (TCB) t__ compute subgoals from typed params via a PURE + │ shared builder, emit a recheckable node that + │ records those params. + ▼ +CHECKER check__ read params from the node, rerun the SAME pure + builder, is_conv-compare to the stored subgoals. +``` + +The rule and its checker **share one pure subgoal-builder** +`__subgoals : env -> -> params -> form list`. The checker +is then just "rerun the builder and compare", so recording the params in the node +is the entire cost of recheckability. Derived (orchestration-only) tactics emit +**no** node and need **no** checker — rechecking recurses into the rules they +expand to. + +## 4. Recheckable proof-nodes (kernel) + +Implemented in [ecCoreGoal.mli](../ecCoreGoal.mli) / `.ml`: + +- `type rule = ..` — an **open** (extensible) variant. Each migrated tactic adds + one constructor carrying its params, e.g. + `type EcCoreGoal.rule += RHoareSeq of codegap1 * ss_inv`. +- `VRule of rule * handle list` — a new `validation` node, the recheckable + sibling of `VExtern`. +- `FApi.xrule1 tc r subgoals` — like `xmutate1` but emits `VRule (r, _)`. + (`xrule`, `xrule_hyps`, `xrule1_hyps` for the other arities.) +- `register_rule_checker : (rule -> rule_checker option) -> unit` — a registry of + partial handlers over the open type. Each tactic registers a handler that + matches its constructor (capturing the params) and returns `None` otherwise. + This is what lets the kernel dispatch to a phl-layer checker without knowing + the constructor — no GADT-opacity, no upward type dependency. +- `recheck_proofenv : proofenv -> unit` — the **driver**: iterates the flat goal + map `pr_goals`; for each `VRule (r, hds)` it finds the checker, resolves the + subgoal handles to their pregoals, and runs the checker. Non-`VRule` + validations are trusted; `VRule` nodes with no registered checker (unmigrated) + are skipped — this is what makes migration incremental. +- `exception RecheckFailure of string`. + +The driver runs at `qed` in [ecScope.save_r](../ecScope.ml), gated by the +**`EC_RECHECK`** environment variable, so normal runs pay nothing and +`EC_RECHECK=1` re-validates every migrated node of every proof. + +### Known limitation (current state) + +The driver re-validates each node *locally* (the recorded subgoals are the ones +the builder yields for that goal). It does **not** yet check graph connectivity +(that a node's subgoal handles are the goals other nodes discharge) nor re-run +the trusted non-`VRule` kernel rules. It is a per-node soundness net for TCB +tactics, not yet a standalone independent proof-checker — that comes once enough +rules carry their params. + +## 5. Directory layout — by family, then logic + +`(include_subdirs unqualified)` in [src/dune](../dune) slurps everything under +`src/` into one flat-namespace library, so subdirectories are **purely +organizational** — module names must stay globally unique (keep the +`Ec` prefix; directories are for humans, no dune changes needed). + +``` +src/phl/ + rules/ genuine logic rules (different subgoals per logic) + hoare/ ehoare/ bdhoare/ equiv/ eager/ + codetx/ logic-uniform program transforms (wp, sp, inline, swap, rcond, …) + bridge/ probabilistic / cross-logic bridges (deno, pr, byequiv, fel, upto) + multi/ multi-logic tactics with shared machinery (conseq, trans, sym) + ecPhl.ml legacy, thin dispatchers, not-yet-migrated tactics +``` + +Rationale: dir-per-logic is right for *logic rules* but would **scatter** the +logic-uniform code transforms and has no home for the multi-logic tactics — +hence the family split first. Within `rules/`, file-per-(logic,tactic) because +that is the unit that pairs 1:1 with a proof-node kind + checker, and +one-file-per-logic would yield 2–3k-line modules. + +## 6. Special / multi-logic tactics + +`conseq` is the hard case: `t_conseq` matches goal-form × invariant-token +(`Inv_ss`/`Inv_ts`) and routes to 11 variants; `process_conseq` is ~2.5k lines. +These (and `trans`, `sym`, the deno/pr bridges) get their own `multi/` area: keep +the dispatcher generic, but still split each *logic's* rule into its own +builder+checker so the node model stays uniform. Do not force them into +`rules//`. Migrate them **last**, once the pattern is proven on the +regular rules. + +## 7. Phased plan + +- **Phase 0 — scaffolding** (DONE): kernel `rule`/`VRule`/`xrule`, checker + registry, `recheck_proofenv`, `EC_RECHECK` hook, layout dirs, this doc + README. +- **Phase 1 — pilot on `seq`** (hoare arm DONE): proves the whole spine + end-to-end with a real rule + checker. +- **Phase 2…N — one tactic per PR**, roughly increasing difficulty: + finish seq (ehoare / bdhoare / equiv / onesided) → skip → wp/sp (codetx pilot) + → cond → rnd → while → call → fun → exists → … → conseq / trans / sym last. + +Each PR: move the file into the new layout, split the four layers, record params +in the node + add the checker, register it. **Proofs must not change.** + +### Invariants for every phase + +- No proof-script changes anywhere in `theories/` or `tests/`. +- `dune build` clean; test suite green; always run `ec.exe` with `-no-eco`. +- A full `EC_RECHECK=1` pass over the stdlib raises **zero** `RecheckFailure`. + +## 8. Per-tactic migration recipe + +1. Create `src/phl///ecPhl…` (or `Ec`) keeping a + globally-unique module name. +2. Extract the pure core `__subgoals` from the existing `t_*_r` + (everything up to the `xmutate1` call, returning the `form list`). +3. Add `type EcCoreGoal.rule += R of `. +4. Rewrite the rule to `FApi.xrule1 tc (R… params) (… _subgoals …)`. +5. Write `check__` = rerun `_subgoals` from the recorded params and + `is_conv`-compare to the stored subgoals; `register_rule_checker` it. +6. Write/move `process__` (the typing), and have the tactic's + `process_` dispatcher route the relevant logic arm to it. +7. Re-export the moved `t_*`/`process_*` from the old module if its `.mli` or + external callers still reference them (avoids touching unrelated files). +8. Build; run the tactic's tests with `EC_RECHECK=1`; add a negative test once + (temporarily break the checker) to confirm it actually fires. + +## 9. Status + +Landed (this branch): Phase 0 + hoare-`seq`. Reference module: +[rules/hoare/ecHoareSeq.ml](rules/hoare/ecHoareSeq.ml). Validated: 91 stdlib +theories + 23 seq-using test files compile under `EC_RECHECK=1` with zero +`RecheckFailure`; negative test confirmed the checker fires only under +`EC_RECHECK`, at `qed`. diff --git a/src/phl/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml index 0b14bf08e6..ade2e0a0e5 100644 --- a/src/phl/ecPhlSeq.ml +++ b/src/phl/ecPhlSeq.ml @@ -14,19 +14,11 @@ open EcLowPhlGoal module TTC = EcProofTyping (* -------------------------------------------------------------------- *) -(* [t_hoare_seq_r gap phi]: splits the statement at [gap]; the first - subgoal covers instructions before the gap, the second after. *) -let t_hoare_seq_r i phi tc = - let env = FApi.tc1_env tc in - let hs = tc1_as_hoareS tc in - let phi = ss_inv_rebind phi (fst hs.hs_m) in - let s1, s2 = s_split env i hs.hs_s in - let post = update_hs_ss phi (hs_po hs) in - let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) post in - let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in - FApi.xmutate1 tc `HlApp [a; b] - -let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r +(* The hoare [seq] rule (split + intermediate assertion) now lives in + [EcHoareSeq], which owns its pure subgoal-builder, the recheckable + proof-node and the matching checker. Re-exported here so existing callers + and the public interface are unchanged. *) +let t_hoare_seq = EcHoareSeq.t_hoare_seq (* -------------------------------------------------------------------- *) let t_ehoare_seq_r i phi tc = @@ -229,10 +221,7 @@ let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) = match k, bd_info with | Single i, PSeqNone when is_hoareS concl -> - check_side side; - let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in - t_hoare_seq i phi tc + EcHoareSeq.process_hoare_seq side i (get_single phi) tc | Single i, PSeqNone when is_eHoareS concl -> check_side side; diff --git a/src/phl/rules/hoare/ecHoareSeq.ml b/src/phl/rules/hoare/ecHoareSeq.ml new file mode 100644 index 0000000000..bb11e80c66 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSeq.ml @@ -0,0 +1,71 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* Recheckable proof-node for the hoare [seq] rule. It records the split + position and the intermediate assertion, which is exactly what the checker + needs to recompute the rule's subgoals. *) +type EcCoreGoal.rule += RHoareSeq of EcMatching.Position.codegap1 * ss_inv + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule (to build the subgoals) and its checker (to + recompute and re-validate them): splitting a [hoareS] statement at [i] with + intermediate assertion [phi] yields the pre/[phi] and [phi]/post goals. *) +let hoare_seq_subgoals env (hs : sHoareS) i (phi : ss_inv) : form list = + let phi = ss_inv_rebind phi (fst hs.hs_m) in + let s1, s2 = s_split env i hs.hs_s in + let post = update_hs_ss phi (hs_po hs) in + let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) post in + let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB): split at [i], emit a recheckable node recording its params. *) +let t_hoare_seq_r i phi tc = + let env = FApi.tc1_env tc in + let hs = tc1_as_hoareS tc in + FApi.xrule1 tc (RHoareSeq (i, phi)) (hoare_seq_subgoals env hs i phi) + +let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r + +(* -------------------------------------------------------------------- *) +(* Checker: recompute the subgoals from the recorded params and confirm they + match (up to conversion) what the node stored. *) +let check_hoare_seq i phi (pe : proofenv) (goal : pregoal) (subs : pregoal list) = + let hyps = goal.g_hyps in + let env = EcEnv.LDecl.toenv hyps in + let hs = pf_as_hoareS pe goal.g_concl in + let expected = hoare_seq_subgoals env hs i phi in + let actual = List.map (fun (g : pregoal) -> g.g_concl) subs in + if List.length expected <> List.length actual then + raise (RecheckFailure "hoare-seq: wrong number of subgoals"); + List.iter2 + (fun e a -> + if not (EcReduction.is_conv hyps e a) then + raise (RecheckFailure "hoare-seq: subgoal mismatch")) + expected actual + +let () = + register_rule_checker + (function + | RHoareSeq (i, phi) -> Some (check_hoare_seq i phi) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS]. Type the intermediate + assertion and the split position, then apply the rule. *) +let process_hoare_seq (side : oside) i (phi : pformula) tc = + if is_some side then + tc_error !!tc "seq: no side information expected"; + let _, phi = TTC.tc1_process_Xhl_formula tc phi in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in + t_hoare_seq i phi tc diff --git a/src/phl/rules/hoare/ecHoareSeq.mli b/src/phl/rules/hoare/ecHoareSeq.mli new file mode 100644 index 0000000000..c615e4dbfe --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSeq.mli @@ -0,0 +1,14 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position +open EcAst + +(* -------------------------------------------------------------------- *) +(* Hoare [seq] rule (TCB): split the statement at [i], with [phi] as the + intermediate assertion. Emits a recheckable proof-node. *) +val t_hoare_seq : codegap1 -> ss_inv -> backward + +(* Elaboration entry for a goal already known to be a [hoareS]: types the + intermediate assertion and split position, then applies [t_hoare_seq]. *) +val process_hoare_seq : oside -> pcodegap1 -> pformula -> backward From 3e90b2f9f32f8e33c564e330df7be15126e493a1 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 11 Jun 2026 14:59:46 +0200 Subject: [PATCH 2/4] phl: factor checker scaffolding into EcPhlRecheck; pass hyps not env Extract the destruct/rebuild/compare boilerplate common to every proof-node checker into its own module, src/phl/ecPhlRecheck.ml: - recheck_forms: arity check + per-subgoal is_conv under each subgoal's own hypotheses; - checker_of name destr build: assemble a rule_checker from a pf_as_* reader and a subgoal builder, wrapping any exception raised while reading/rebuilding into a RecheckFailure (so a checker never leaks a raw user-level exception). The shared subgoal-builder now takes the goal's hypotheses (the authoritative context; env is just LDecl.toenv of it, and the conversion check needs hyps anyway) instead of a pre-projected env, so the rule and its checker reason in the same context. hoare_seq_subgoals updated accordingly; the rule passes FApi.tc1_hyps. check_hoare_seq collapses to its checker_of registration. Docs (README, REFACTORING) updated: builder signature, the EcPhlRecheck factoring, the migration recipe, and a note that hyps-changing rules (xrule*_hyps, e.g. while) will need a hyps-aware recheck variant. --- src/phl/README.md | 21 ++++++++++++--- src/phl/REFACTORING.md | 34 ++++++++++++++++------- src/phl/ecPhlRecheck.ml | 45 +++++++++++++++++++++++++++++++ src/phl/ecPhlRecheck.mli | 22 +++++++++++++++ src/phl/rules/hoare/ecHoareSeq.ml | 37 ++++++++++--------------- 5 files changed, 123 insertions(+), 36 deletions(-) create mode 100644 src/phl/ecPhlRecheck.ml create mode 100644 src/phl/ecPhlRecheck.mli diff --git a/src/phl/README.md b/src/phl/README.md index 487d0c1421..bfcbe3e9e3 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -29,9 +29,24 @@ CHECKER check__ read the params back from the node, recomp ``` Key rule: the rule and its checker share one **pure subgoal-builder** -(`__subgoals : env -> -> params -> form list`). The -checker is then "rerun the builder and compare", which is why recording the -params in the node is all that recheckability costs. +(`__subgoals : LDecl.hyps -> -> params -> form list`). +The checker is then "rerun the builder and compare", which is why recording the +params in the node is all that recheckability costs. The builder is handed the +goal's `hyps` (the authoritative context; its environment is `LDecl.toenv` of +them), so the rule and checker reason in exactly the same context. + +The comparison boilerplate is shared in [`ecPhlRecheck.ml`](ecPhlRecheck.ml): +`EcPhlRecheck.checker_of name destr build` turns a judgement reader (`pf_as_*`) +and a builder into a `rule_checker`, and wraps any exception raised while +rebuilding into a `RecheckFailure`. A checker is then just its registration: + +```ocaml +let () = register_rule_checker (function + | R params -> + Some (EcPhlRecheck.checker_of "-" pf_as_ + (fun hyps j -> __subgoals hyps j params)) + | _ -> None) +``` Derived (non-TCB) tactics that only orchestrate other tactics emit **no** node and need **no** checker — rechecking recurses into the rules they expand to. diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index 71910a51b5..50b1cbacd2 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -71,11 +71,22 @@ CHECKER check__ read params from the node, rerun the SAME ``` The rule and its checker **share one pure subgoal-builder** -`__subgoals : env -> -> params -> form list`. The checker -is then just "rerun the builder and compare", so recording the params in the node -is the entire cost of recheckability. Derived (orchestration-only) tactics emit -**no** node and need **no** checker — rechecking recurses into the rules they -expand to. +`__subgoals : LDecl.hyps -> -> params -> form list`. The +checker is then just "rerun the builder and compare", so recording the params in +the node is the entire cost of recheckability. The builder takes the goal's +`hyps` (the authoritative context — `env` is just `LDecl.toenv` of it, and the +conversion check needs `hyps` anyway), so the rule and checker share one context. +Derived (orchestration-only) tactics emit **no** node and need **no** checker — +rechecking recurses into the rules they expand to. + +The destruct/rebuild/compare boilerplate common to every checker is factored into +its own module, [`ecPhlRecheck.ml`](ecPhlRecheck.ml): `recheck_forms` (arity + +per-subgoal `is_conv` under each subgoal's hyps) and `checker_of name destr +build` (assemble a `rule_checker` from a `pf_as_*` reader and a builder, wrapping +any rebuild exception into a `RecheckFailure`). A per-rule checker is then only +its registration. A hyps-changing rule (one emitted via `xrule*_hyps`, e.g. +`while`) will need a hyps-aware variant that also validates the recorded +hypotheses — to be added when the first such rule is migrated. ## 4. Recheckable proof-nodes (kernel) @@ -169,12 +180,15 @@ in the node + add the checker, register it. **Proofs must not change.** 1. Create `src/phl///ecPhl…` (or `Ec`) keeping a globally-unique module name. -2. Extract the pure core `__subgoals` from the existing `t_*_r` - (everything up to the `xmutate1` call, returning the `form list`). +2. Extract the pure core `__subgoals : LDecl.hyps -> … -> form list` + from the existing `t_*_r` (everything up to the `xmutate1` call, returning the + `form list`; take `hyps` and derive `env = LDecl.toenv hyps` inside). 3. Add `type EcCoreGoal.rule += R of `. -4. Rewrite the rule to `FApi.xrule1 tc (R… params) (… _subgoals …)`. -5. Write `check__` = rerun `_subgoals` from the recorded params and - `is_conv`-compare to the stored subgoals; `register_rule_checker` it. +4. Rewrite the rule to + `FApi.xrule1 tc (R… params) (… _subgoals (FApi.tc1_hyps tc) …)`. +5. Register the checker with `EcPhlRecheck.checker_of "-" pf_as_ + (fun hyps j -> __subgoals hyps j params)` — no per-rule comparison + code. 6. Write/move `process__` (the typing), and have the tactic's `process_` dispatcher route the relevant logic arm to it. 7. Re-export the moved `t_*`/`process_*` from the old module if its `.mli` or diff --git a/src/phl/ecPhlRecheck.ml b/src/phl/ecPhlRecheck.ml new file mode 100644 index 0000000000..f4866bff9b --- /dev/null +++ b/src/phl/ecPhlRecheck.ml @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcEnv +open EcCoreGoal + +(* -------------------------------------------------------------------- *) +(* Shared scaffolding for proof-node checkers (see [EcCoreGoal.rule]). + + A checker rebuilds the subgoals a rule should have produced and compares + them, up to conversion, against what the node recorded. Only the two + per-rule pieces differ — how to read the judgement out of the goal, and how + to recompute its subgoals from the recorded parameters — everything else + (deriving the context, the arity check, the per-subgoal comparison and the + error reporting) lives here. *) + +(* -------------------------------------------------------------------- *) +(* Compare the [expected] subgoal conclusions against the recorded [subs], up + to conversion under each subgoal's own hypotheses. *) +let recheck_forms (name : string) (expected : form list) (subs : pregoal list) = + let nexp = List.length expected and ngot = List.length subs in + if nexp <> ngot then + raise (RecheckFailure + (Printf.sprintf "%s: expected %d subgoal(s), got %d" name nexp ngot)); + List.iteri + (fun k (e, (g : pregoal)) -> + if not (EcReduction.is_conv g.g_hyps e g.g_concl) then + raise (RecheckFailure (Printf.sprintf "%s: subgoal %d mismatch" name (k+1)))) + (List.combine expected subs) + +(* -------------------------------------------------------------------- *) +(* Build a [rule_checker] from a judgement reader [destr] and a subgoal builder + [build]. [build] is handed the goal's hypotheses (the authoritative context; + its environment is [LDecl.toenv] of them) and recomputes the subgoals — the + recorded parameters are captured in [build] at registration time. Any + exception raised while reading or rebuilding is surfaced as a + [RecheckFailure], so a checker never leaks a raw user-level exception. *) +let checker_of + (name : string) + (destr : proofenv -> form -> 'a) + (build : LDecl.hyps -> 'a -> form list) + : rule_checker = + fun pe goal subs -> + try recheck_forms name (build goal.g_hyps (destr pe goal.g_concl)) subs with + | RecheckFailure _ as e -> raise e + | e -> raise (RecheckFailure (Printf.sprintf "%s: %s" name (Printexc.to_string e))) diff --git a/src/phl/ecPhlRecheck.mli b/src/phl/ecPhlRecheck.mli new file mode 100644 index 0000000000..6e1c08a217 --- /dev/null +++ b/src/phl/ecPhlRecheck.mli @@ -0,0 +1,22 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcEnv +open EcCoreGoal + +(* -------------------------------------------------------------------- *) +(* Shared scaffolding for proof-node checkers (see [EcCoreGoal.rule]). *) + +(* Compare [expected] subgoal conclusions against the recorded subgoals, up to + conversion under each subgoal's own hypotheses; raise [RecheckFailure] on an + arity or conversion mismatch. *) +val recheck_forms : string -> form list -> pregoal list -> unit + +(* [checker_of name destr build] is a [rule_checker]: it reads the judgement + from the goal with [destr], recomputes the subgoals with [build] (handed the + goal's hypotheses), and compares them with [recheck_forms]. Any exception + raised while reading or rebuilding is wrapped in [RecheckFailure]. *) +val checker_of : + string + -> (proofenv -> form -> 'a) + -> (LDecl.hyps -> 'a -> form list) + -> rule_checker diff --git a/src/phl/rules/hoare/ecHoareSeq.ml b/src/phl/rules/hoare/ecHoareSeq.ml index bb11e80c66..024552de33 100644 --- a/src/phl/rules/hoare/ecHoareSeq.ml +++ b/src/phl/rules/hoare/ecHoareSeq.ml @@ -19,8 +19,11 @@ type EcCoreGoal.rule += RHoareSeq of EcMatching.Position.codegap1 * ss_inv (* -------------------------------------------------------------------- *) (* Pure core shared by the rule (to build the subgoals) and its checker (to recompute and re-validate them): splitting a [hoareS] statement at [i] with - intermediate assertion [phi] yields the pre/[phi] and [phi]/post goals. *) -let hoare_seq_subgoals env (hs : sHoareS) i (phi : ss_inv) : form list = + intermediate assertion [phi] yields the pre/[phi] and [phi]/post goals. It + takes the goal's hypotheses (its environment is [LDecl.toenv] of them) so the + rule and checker share the same context. *) +let hoare_seq_subgoals hyps (hs : sHoareS) i (phi : ss_inv) : form list = + let env = EcEnv.LDecl.toenv hyps in let phi = ss_inv_rebind phi (fst hs.hs_m) in let s1, s2 = s_split env i hs.hs_s in let post = update_hs_ss phi (hs_po hs) in @@ -31,34 +34,22 @@ let hoare_seq_subgoals env (hs : sHoareS) i (phi : ss_inv) : form list = (* -------------------------------------------------------------------- *) (* Rule (TCB): split at [i], emit a recheckable node recording its params. *) let t_hoare_seq_r i phi tc = - let env = FApi.tc1_env tc in - let hs = tc1_as_hoareS tc in - FApi.xrule1 tc (RHoareSeq (i, phi)) (hoare_seq_subgoals env hs i phi) + let hs = tc1_as_hoareS tc in + FApi.xrule1 tc (RHoareSeq (i, phi)) + (hoare_seq_subgoals (FApi.tc1_hyps tc) hs i phi) let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r (* -------------------------------------------------------------------- *) -(* Checker: recompute the subgoals from the recorded params and confirm they - match (up to conversion) what the node stored. *) -let check_hoare_seq i phi (pe : proofenv) (goal : pregoal) (subs : pregoal list) = - let hyps = goal.g_hyps in - let env = EcEnv.LDecl.toenv hyps in - let hs = pf_as_hoareS pe goal.g_concl in - let expected = hoare_seq_subgoals env hs i phi in - let actual = List.map (fun (g : pregoal) -> g.g_concl) subs in - if List.length expected <> List.length actual then - raise (RecheckFailure "hoare-seq: wrong number of subgoals"); - List.iter2 - (fun e a -> - if not (EcReduction.is_conv hyps e a) then - raise (RecheckFailure "hoare-seq: subgoal mismatch")) - expected actual - +(* Checker: read the judgement, rerun the shared builder on the recorded params, + and compare against the stored subgoals (see [EcPhlRecheck]). *) let () = register_rule_checker (function - | RHoareSeq (i, phi) -> Some (check_hoare_seq i phi) - | _ -> None) + | RHoareSeq (i, phi) -> + Some (EcPhlRecheck.checker_of "hoare-seq" pf_as_hoareS + (fun hyps hs -> hoare_seq_subgoals hyps hs i phi)) + | _ -> None) (* -------------------------------------------------------------------- *) (* Elaboration: the goal is known to be a [hoareS]. Type the intermediate From c42f1db05b368ba794383bd0ba433f2b4b0be3e4 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 11 Jun 2026 15:39:15 +0200 Subject: [PATCH 3/4] phl: records for seq params/info; f_node dispatch in process_seq Make the seq tactic self-documenting via records, and clean up its dispatcher. - EcParsetree.seq_info becomes a record { seqi_side; seqi_at; seqi_mid; seqi_bd } (built at the one grammar site) instead of a 4-tuple. - The migrated rule in rules/hoare/ exposes a parameter record hoare_seq_rule { hsr_at; hsr_mid }, carried by the RHoareSeq node and consumed by the shared subgoal-builder. The canonical EcHoareSeq.t_hoare_seq takes that record; the legacy EcPhlSeq.t_hoare_seq keeps its positional .mli and is a thin adapter onto it, so external callers are untouched. - process_hoare_seq takes the seq_info record and owns the hoare surface-syntax validation (no side, no bound, single position/assertion). - process_seq dispatches by pattern-matching the goal's f_node (no is_* predicates); the five `when is_X` guards collapse to four F...S _ arms plus a shared bad_params fallback reproducing the original error messages exactly. Docs (REFACTORING 7b + recipe, README) updated for the two-record convention, the rules/*-record / phl/*-positional-adapter split, and f_node dispatch. Build clean; pilot + 23 seq-using files pass under EC_RECHECK=1 with zero RecheckFailure. --- src/ecParser.mly | 2 +- src/ecParsetree.ml | 8 +- src/phl/README.md | 5 +- src/phl/REFACTORING.md | 59 +++++++++++--- src/phl/ecPhlSeq.ml | 121 +++++++++++++++++------------ src/phl/rules/hoare/ecHoareSeq.ml | 65 ++++++++++------ src/phl/rules/hoare/ecHoareSeq.mli | 19 +++-- 7 files changed, 182 insertions(+), 97 deletions(-) diff --git a/src/ecParser.mly b/src/ecParser.mly index 95d9999e64..300839935f 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3036,7 +3036,7 @@ direction: { Pfun `Code } | SEQ s=side? pos=s_codegap1_0before COLON p=form_or_double_form f=app_bd_info - { Pseq (s, pos, p, f) } + { Pseq { seqi_side = s; seqi_at = pos; seqi_mid = p; seqi_bd = f; } } | WP n=s_codegap1_0before? { Pwp n } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index e9deac3f92..b2589c9093 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -671,8 +671,12 @@ type fun_info = [ ] (* -------------------------------------------------------------------- *) -type seq_info = - oside * pcodegap1 doption * pformula doption * p_seq_xt_info +type seq_info = { + seqi_side : oside; (* side (prhl only) *) + seqi_at : pcodegap1 doption; (* split position(s) *) + seqi_mid : pformula doption; (* intermediate assertion / (pre, post) *) + seqi_bd : p_seq_xt_info; (* bound information (bdhoare only) *) +} (* -------------------------------------------------------------------- *) type pcond_info = [ diff --git a/src/phl/README.md b/src/phl/README.md index bfcbe3e9e3..e1194c39b9 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -88,5 +88,6 @@ src/phl/ - **hoare `seq`** — [`rules/hoare/ecHoareSeq.ml`](rules/hoare/ecHoareSeq.ml). The reference example of the full spine + checker. `EcPhlSeq.process_seq` - dispatches its `hoareS` arm here; `EcPhlSeq.t_hoare_seq` re-exports the rule - so existing callers and the public interface are unchanged. + dispatches its `hoareS` arm here. The canonical rule `EcHoareSeq.t_hoare_seq` + takes a `hoare_seq_rule` record; the legacy `EcPhlSeq.t_hoare_seq` keeps its + positional `.mli` and adapts onto it, so existing callers are unchanged. diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index 50b1cbacd2..d8a3be9fdf 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -176,23 +176,58 @@ in the node + add the checker, register it. **Proofs must not change.** - `dune build` clean; test suite green; always run `ec.exe` with `-no-eco`. - A full `EC_RECHECK=1` pass over the stdlib raises **zero** `RecheckFailure`. +## 7b. Parameters travel as records, not tuples + +Two records make each tactic self-documenting (fields show up in the `.mli`): + +- **Parse input** — *lives in the parsetree*, not in `src/phl`. The tactic's + `EcParsetree` info type is a record with named, prefixed fields (e.g. + `seq_info = { seqi_side; seqi_at; seqi_mid; seqi_bd }`), built in the grammar. + We do **not** mirror it with a phl-side copy — the parse info *is* the + parsetree node. The dispatcher `process_` routes purely on the goal + kind and forwards the **whole record** to the per-logic + `process__`, which takes that same record and owns its + surface-syntax validation (single vs double, side allowed, bound allowed, …). + So `process_*` are never positional. +- **Typed rule parameters** — a record defined in the migrated `rules/*` module + (e.g. `hoare_seq_rule = { hsr_at; hsr_mid }`), carried by the proof-node + constructor (`RHoareSeq of hoare_seq_rule`) and consumed by the shared + subgoal-builder. The **canonical rule in `rules/*` takes this record** + (`EcHoareSeq.t_hoare_seq : hoare_seq_rule -> backward`). The **legacy positional + entry in `phl/*` keeps its `.mli` unchanged** and is a thin adapter onto it + (`let t_hoare_seq i phi = EcHoareSeq.(t_hoare_seq { hsr_at = i; hsr_mid = phi })`), + so not-yet-migrated callers are untouched. + +Field names use a short per-record **prefix** (`seqi_`, `hsr_`), matching the +existing EC record style (`hs_m`, `es_pr`, `bhs_bd`) and avoiding label clashes +within a module. + ## 8. Per-tactic migration recipe 1. Create `src/phl///ecPhl…` (or `Ec`) keeping a globally-unique module name. -2. Extract the pure core `__subgoals : LDecl.hyps -> … -> form list` - from the existing `t_*_r` (everything up to the `xmutate1` call, returning the - `form list`; take `hyps` and derive `env = LDecl.toenv hyps` inside). -3. Add `type EcCoreGoal.rule += R of `. -4. Rewrite the rule to - `FApi.xrule1 tc (R… params) (… _subgoals (FApi.tc1_hyps tc) …)`. +2. Define the typed parameter record `__rule = { _… }` (prefixed + fields, §7b) and extract the pure core + `__subgoals : LDecl.hyps -> -> __rule -> form list` + from the existing `t_*_r` (everything up to the `xmutate1` call; take `hyps` + and derive `env = LDecl.toenv hyps` inside). +3. Add `type EcCoreGoal.rule += R of __rule`. +4. Write the canonical rule in `rules/*` taking the record: + `t__ : __rule -> backward`, body + `FApi.xrule1 tc (R… r) (<…>_subgoals (FApi.tc1_hyps tc) j r)`. Turn the legacy + `phl/*` `t_*` (positional `.mli` unchanged) into a thin adapter that builds the + record and calls it. If the tactic's `EcParsetree` info is still a tuple, + convert it to a record (§7b) at the same time. 5. Register the checker with `EcPhlRecheck.checker_of "-" pf_as_ - (fun hyps j -> __subgoals hyps j params)` — no per-rule comparison - code. -6. Write/move `process__` (the typing), and have the tactic's - `process_` dispatcher route the relevant logic arm to it. -7. Re-export the moved `t_*`/`process_*` from the old module if its `.mli` or - external callers still reference them (avoids touching unrelated files). + (fun hyps j -> __subgoals hyps j r)` — no per-rule comparison code. +6. Write `process__ : _info -> backward` (taking the parsetree + record): validate the surface syntax for that logic, type the arguments, build + the rule record and call `t__`. In the `phl/*` dispatcher + `process_`, route by **pattern-matching the goal's `f_node`** — + `| FS _ -> EcPhl…process__ info tc` — and drop the + corresponding legacy arm. Do not use `is_*` predicates for dispatch. +7. Keep the legacy `phl/*` `t_*` (positional adapter) so external callers and the + module's `.mli` are untouched. 8. Build; run the tactic's tests with `EC_RECHECK=1`; add a negative test once (temporarily break the checker) to confirm it actually fires. diff --git a/src/phl/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml index ade2e0a0e5..b383a13ae7 100644 --- a/src/phl/ecPhlSeq.ml +++ b/src/phl/ecPhlSeq.ml @@ -15,10 +15,12 @@ module TTC = EcProofTyping (* -------------------------------------------------------------------- *) (* The hoare [seq] rule (split + intermediate assertion) now lives in - [EcHoareSeq], which owns its pure subgoal-builder, the recheckable - proof-node and the matching checker. Re-exported here so existing callers - and the public interface are unchanged. *) -let t_hoare_seq = EcHoareSeq.t_hoare_seq + [EcHoareSeq], which owns its parameter record, pure subgoal-builder, the + recheckable proof-node and the matching checker. The canonical rule there + takes a record; this legacy positional entry adapts onto it, so existing + callers and this module's interface are unchanged. *) +let t_hoare_seq i phi = + EcHoareSeq.(t_hoare_seq { hsr_at = i; hsr_mid = phi }) (* -------------------------------------------------------------------- *) let t_ehoare_seq_r i phi tc = @@ -207,9 +209,14 @@ let process_phl_bd_info bd_info tc = (phi, f1, f2, g1, g2) (* -------------------------------------------------------------------- *) -let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) = +let process_seq (info : seq_info) (tc : tcenv1) = let concl = FApi.tc1_goal tc in + let side = info.seqi_side in + let k = info.seqi_at in + let phi = info.seqi_mid in + let bd_info = info.seqi_bd in + let get_single phi = match phi with | Single phi -> phi @@ -219,48 +226,62 @@ let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) = if EcUtils.is_some side then tc_error !!tc "seq: no side information expected" in - match k, bd_info with - | Single i, PSeqNone when is_hoareS concl -> - EcHoareSeq.process_hoare_seq side i (get_single phi) tc - - | Single i, PSeqNone when is_eHoareS concl -> - check_side side; - let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in - t_ehoare_seq i phi tc - - | Single i, PSeqNone when is_equivS concl -> - let pre, post = - match phi with - | Single _ -> tc_error !!tc "seq onsided: a pre and a post is expected" - | Double (pre, post) -> - let _, pre = TTC.tc1_process_Xhl_formula ?side tc pre in - let _, post = TTC.tc1_process_Xhl_formula ?side tc post in - (pre, post) in - let side = - match side with - | None -> tc_error !!tc "seq onsided: side information expected" - | Some side -> side in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some side, i) in - t_equiv_seq_onesided side i pre post tc - - | Single i, _ when is_bdHoareS concl -> - check_side side; - let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in - let (ra, f1, f2, f3, f4) = process_phl_bd_info bd_info tc in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in - t_bdhoare_seq i (ra, pia, f1, f2, f3, f4) tc - - | Double (i, j), PSeqNone when is_equivS concl -> - check_side side; - let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, i) in - let j = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, j) in - t_equiv_seq (i, j) phi tc - - | Single _, PSeqNone - | Double _, PSeqNone -> - tc_error !!tc "invalid `position' parameter" - - | _, _ -> - tc_error !!tc "optional bound parameter not supported" + let bad_params () = + match bd_info with + | PSeqNone -> tc_error !!tc "invalid `position' parameter" + | _ -> tc_error !!tc "optional bound parameter not supported" in + + (* Dispatch on the goal kind only; each logic owns its surface-syntax + handling. Migrated logics take the whole [seq_info] record; the others are + still inlined here pending migration. *) + match concl.f_node with + | FhoareS _ -> + EcHoareSeq.process_hoare_seq info tc + + | FeHoareS _ -> begin + match k, bd_info with + | Single i, PSeqNone -> + check_side side; + let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in + t_ehoare_seq i phi tc + | _ -> bad_params () + end + + | FbdHoareS _ -> begin + match k with + | Single i -> + check_side side; + let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in + let (ra, f1, f2, f3, f4) = process_phl_bd_info bd_info tc in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in + t_bdhoare_seq i (ra, pia, f1, f2, f3, f4) tc + | Double _ -> bad_params () + end + + | FequivS _ -> begin + match k, bd_info with + | Single i, PSeqNone -> + let pre, post = + match phi with + | Single _ -> tc_error !!tc "seq onsided: a pre and a post is expected" + | Double (pre, post) -> + let _, pre = TTC.tc1_process_Xhl_formula ?side tc pre in + let _, post = TTC.tc1_process_Xhl_formula ?side tc post in + (pre, post) in + let side = + match side with + | None -> tc_error !!tc "seq onsided: side information expected" + | Some side -> side in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some side, i) in + t_equiv_seq_onesided side i pre post tc + | Double (i, j), PSeqNone -> + check_side side; + let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in + let i = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, i) in + let j = EcLowPhlGoal.tc1_process_codegap1 tc (Some `Left, j) in + t_equiv_seq (i, j) phi tc + | _ -> bad_params () + end + + | _ -> bad_params () diff --git a/src/phl/rules/hoare/ecHoareSeq.ml b/src/phl/rules/hoare/ecHoareSeq.ml index 024552de33..cabd1de66c 100644 --- a/src/phl/rules/hoare/ecHoareSeq.ml +++ b/src/phl/rules/hoare/ecHoareSeq.ml @@ -11,34 +11,39 @@ open EcLowPhlGoal module TTC = EcProofTyping (* -------------------------------------------------------------------- *) -(* Recheckable proof-node for the hoare [seq] rule. It records the split - position and the intermediate assertion, which is exactly what the checker - needs to recompute the rule's subgoals. *) -type EcCoreGoal.rule += RHoareSeq of EcMatching.Position.codegap1 * ss_inv +(* Parameters of the hoare [seq] rule. Recorded in the proof-node, so the + checker can recompute the rule's subgoals. *) +type hoare_seq_rule = { + hsr_at : EcMatching.Position.codegap1; (* split position *) + hsr_mid : ss_inv; (* intermediate assertion *) +} + +type EcCoreGoal.rule += RHoareSeq of hoare_seq_rule (* -------------------------------------------------------------------- *) (* Pure core shared by the rule (to build the subgoals) and its checker (to - recompute and re-validate them): splitting a [hoareS] statement at [i] with - intermediate assertion [phi] yields the pre/[phi] and [phi]/post goals. It - takes the goal's hypotheses (its environment is [LDecl.toenv] of them) so the - rule and checker share the same context. *) -let hoare_seq_subgoals hyps (hs : sHoareS) i (phi : ss_inv) : form list = + recompute and re-validate them): splitting a [hoareS] statement at [hsr_at] + with intermediate assertion [hsr_mid] yields the pre/mid and mid/post goals. + It takes the goal's hypotheses (its environment is [LDecl.toenv] of them) so + the rule and checker share the same context. *) +let hoare_seq_subgoals hyps (hs : sHoareS) (r : hoare_seq_rule) : form list = let env = EcEnv.LDecl.toenv hyps in - let phi = ss_inv_rebind phi (fst hs.hs_m) in - let s1, s2 = s_split env i hs.hs_s in + let phi = ss_inv_rebind r.hsr_mid (fst hs.hs_m) in + let s1, s2 = s_split env r.hsr_at hs.hs_s in let post = update_hs_ss phi (hs_po hs) in let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) post in let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in [a; b] (* -------------------------------------------------------------------- *) -(* Rule (TCB): split at [i], emit a recheckable node recording its params. *) -let t_hoare_seq_r i phi tc = +(* Rule (TCB): split according to [r], emit a recheckable node recording it. + This canonical rule takes the parameter record; the legacy positional + interface (EcPhlSeq.t_hoare_seq) adapts onto it. *) +let t_hoare_seq_r (r : hoare_seq_rule) tc = let hs = tc1_as_hoareS tc in - FApi.xrule1 tc (RHoareSeq (i, phi)) - (hoare_seq_subgoals (FApi.tc1_hyps tc) hs i phi) + FApi.xrule1 tc (RHoareSeq r) (hoare_seq_subgoals (FApi.tc1_hyps tc) hs r) -let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r +let t_hoare_seq = FApi.t_low1 "hoare-seq" t_hoare_seq_r (* -------------------------------------------------------------------- *) (* Checker: read the judgement, rerun the shared builder on the recorded params, @@ -46,17 +51,29 @@ let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r let () = register_rule_checker (function - | RHoareSeq (i, phi) -> + | RHoareSeq r -> Some (EcPhlRecheck.checker_of "hoare-seq" pf_as_hoareS - (fun hyps hs -> hoare_seq_subgoals hyps hs i phi)) + (fun hyps hs -> hoare_seq_subgoals hyps hs r)) | _ -> None) (* -------------------------------------------------------------------- *) -(* Elaboration: the goal is known to be a [hoareS]. Type the intermediate - assertion and the split position, then apply the rule. *) -let process_hoare_seq (side : oside) i (phi : pformula) tc = - if is_some side then +(* Elaboration: the goal is known to be a [hoareS]. Validate the seq surface + syntax for that logic (no side, no bound, single position and assertion), + type the assertion and the split position, then apply the rule. *) +let process_hoare_seq (info : seq_info) tc = + if is_some info.seqi_side then tc_error !!tc "seq: no side information expected"; + begin match info.seqi_bd with + | PSeqNone -> () + | _ -> tc_error !!tc "seq: no bound information expected" end; + let i = + match info.seqi_at with + | Single i -> i + | Double _ -> tc_error !!tc "seq: a single position is expected" in + let phi = + match info.seqi_mid with + | Single phi -> phi + | Double _ -> tc_error !!tc "seq: a single formula is expected" in let _, phi = TTC.tc1_process_Xhl_formula tc phi in - let i = EcLowPhlGoal.tc1_process_codegap1 tc (side, i) in - t_hoare_seq i phi tc + let i = EcLowPhlGoal.tc1_process_codegap1 tc (info.seqi_side, i) in + t_hoare_seq { hsr_at = i; hsr_mid = phi } tc diff --git a/src/phl/rules/hoare/ecHoareSeq.mli b/src/phl/rules/hoare/ecHoareSeq.mli index c615e4dbfe..7d59ba5b23 100644 --- a/src/phl/rules/hoare/ecHoareSeq.mli +++ b/src/phl/rules/hoare/ecHoareSeq.mli @@ -5,10 +5,17 @@ open EcMatching.Position open EcAst (* -------------------------------------------------------------------- *) -(* Hoare [seq] rule (TCB): split the statement at [i], with [phi] as the - intermediate assertion. Emits a recheckable proof-node. *) -val t_hoare_seq : codegap1 -> ss_inv -> backward +(* Parameters of the hoare [seq] rule (recorded in the proof-node). *) +type hoare_seq_rule = { + hsr_at : codegap1; (* split position *) + hsr_mid : ss_inv; (* intermediate assertion *) +} -(* Elaboration entry for a goal already known to be a [hoareS]: types the - intermediate assertion and split position, then applies [t_hoare_seq]. *) -val process_hoare_seq : oside -> pcodegap1 -> pformula -> backward +(* Hoare [seq] rule (TCB): split the statement per [r]. Emits a recheckable + proof-node. *) +val t_hoare_seq : hoare_seq_rule -> backward + +(* Elaboration entry for a goal already known to be a [hoareS]: validates the + seq surface syntax, types the assertion and split position, then applies + [t_hoare_seq]. Takes the parse-tree [seq_info] record directly. *) +val process_hoare_seq : seq_info -> backward From 13273e4e0758c947f05f73e91709c8cb0753086e Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 11 Jun 2026 16:23:55 +0200 Subject: [PATCH 4/4] phl: keep code resolution out of the seq checker's TCB The checker is trusted re-validation, so it must not redo elaboration work the rule already did. The hoare-seq checker was re-resolving the symbolic code gap (via s_split), pulling all of code-position normalization into its trust boundary. Split the parameters into two records: the high-level rule arguments (hoare_seq_rule, with a symbolic codegap1) that the canonical rule takes, and the low-level node payload (hoare_seq_node, with the resolved nm_codegap1 integer index) that is recorded and rechecked. The rule resolves the gap once (new EcLowPhlGoal.s_split_index = normalize_cgap1 with the s_split error), records the resolved node, and builds subgoals through a pure low-level core that splits at the integer (split_at_nmcgap1, no env). The checker reruns only that core, so normalize_cgap1 stays out of its TCB; faithfulness is by construction since the rule builds its subgoals through the same core. Docs: new REFACTORING 7c ("the checker is post-resolution; the node records resolved data") + rule of thumb to record the lowest-level value that still determines the subgoals; 7b lists both records; recipe and README spine updated. Build clean; pilot + 23 seq files pass under EC_RECHECK=1. --- src/ecLowPhlGoal.ml | 8 ++++ src/phl/README.md | 17 +++---- src/phl/REFACTORING.md | 74 ++++++++++++++++++++++--------- src/phl/rules/hoare/ecHoareSeq.ml | 52 +++++++++++++--------- 4 files changed, 101 insertions(+), 50 deletions(-) diff --git a/src/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 416bb15627..1e1de92830 100644 --- a/src/ecLowPhlGoal.ml +++ b/src/ecLowPhlGoal.ml @@ -394,6 +394,14 @@ let s_split env i s = try Pos.split_at_cgap1 env i s with Pos.InvalidCPos -> raise (InvalidSplit (`Gap i)) +(* Resolve a (symbolic) code gap to its normalized integer index. This is the + env-dependent "code resolution" step; splitting a statement at the resulting + index ([EcMatching.Position.split_at_nmcgap1]) needs no environment. *) +let s_split_index env i s = + let module Pos = EcMatching.Position in + try Pos.normalize_cgap1 env i s + with Pos.InvalidCPos -> raise (InvalidSplit (`Gap i)) + (* -------------------------------------------------------------------- *) let s_split_i env i s = let module Pos = EcMatching.Position in diff --git a/src/phl/README.md b/src/phl/README.md index e1194c39b9..5751b2fd0d 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -28,12 +28,13 @@ CHECKER check__ read the params back from the node, recomp confirm they match (is_conv) what was stored. ``` -Key rule: the rule and its checker share one **pure subgoal-builder** -(`__subgoals : LDecl.hyps -> -> params -> form list`). -The checker is then "rerun the builder and compare", which is why recording the -params in the node is all that recheckability costs. The builder is handed the -goal's `hyps` (the authoritative context; its environment is `LDecl.toenv` of -them), so the rule and checker reason in exactly the same context. +Key rule: the rule and its checker share one **pure low-level subgoal-builder** +(`__subgoals : -> -> form list`), operating on the +node's *resolved* parameters (e.g. an integer split index, not a symbolic code +gap). The checker is then "rerun the builder and compare", which is why recording +the resolved params in the node is all that recheckability costs. Resolution +(code positions, typing, …) happens once in the rule, **before** the core, so it +stays out of the checker's trust boundary — see REFACTORING §7c. The comparison boilerplate is shared in [`ecPhlRecheck.ml`](ecPhlRecheck.ml): `EcPhlRecheck.checker_of name destr build` turns a judgement reader (`pf_as_*`) @@ -42,9 +43,9 @@ rebuilding into a `RecheckFailure`. A checker is then just its registration: ```ocaml let () = register_rule_checker (function - | R params -> + | R node -> Some (EcPhlRecheck.checker_of "-" pf_as_ - (fun hyps j -> __subgoals hyps j params)) + (fun _hyps j -> __subgoals j node)) | _ -> None) ``` diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index d8a3be9fdf..4badad6827 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -189,37 +189,69 @@ Two records make each tactic self-documenting (fields show up in the `.mli`): `process__`, which takes that same record and owns its surface-syntax validation (single vs double, side allowed, bound allowed, …). So `process_*` are never positional. -- **Typed rule parameters** — a record defined in the migrated `rules/*` module - (e.g. `hoare_seq_rule = { hsr_at; hsr_mid }`), carried by the proof-node - constructor (`RHoareSeq of hoare_seq_rule`) and consumed by the shared - subgoal-builder. The **canonical rule in `rules/*` takes this record** +- **Rule arguments** — a record defined in the migrated `rules/*` module (e.g. + `hoare_seq_rule = { hsr_at; hsr_mid }`, high level: the position is still a + symbolic `codegap1`). The **canonical rule in `rules/*` takes this record** (`EcHoareSeq.t_hoare_seq : hoare_seq_rule -> backward`). The **legacy positional entry in `phl/*` keeps its `.mli` unchanged** and is a thin adapter onto it (`let t_hoare_seq i phi = EcHoareSeq.(t_hoare_seq { hsr_at = i; hsr_mid = phi })`), so not-yet-migrated callers are untouched. - -Field names use a short per-record **prefix** (`seqi_`, `hsr_`), matching the -existing EC record style (`hs_m`, `es_pr`, `bhs_bd`) and avoiding label clashes -within a module. +- **Node payload** — a *separate* record (e.g. `hoare_seq_node = { hsn_at; hsn_mid }`) + carried by the proof-node constructor (`RHoareSeq of hoare_seq_node`) and + consumed by the shared subgoal-builder. It holds the **resolved, low-level** + parameters (see §7c): `hsn_at` is the normalized integer split index, not the + symbolic gap. + +Field names use a short per-record **prefix** (`seqi_`, `hsr_`, `hsn_`), matching +the existing EC record style (`hs_m`, `es_pr`, `bhs_bd`) and avoiding label +clashes within a module. + +## 7c. The checker is post-resolution; the node records resolved data + +A checker is *trusted* re-validation, so its TCB must be minimal. It must **not** +redo elaboration/resolution work the rule already did — code-position +resolution, name lookup, unification, etc. Concretely, the rule splits at a +symbolic `codegap1`, which `normalize_cgap1 env` resolves to an integer index +(`nm_codegap1`). If the node stored the `codegap1` and the checker re-resolved +it, all of code-position normalization would sit inside the checker's TCB. + +Instead: the rule does the env-dependent resolution **once** +(`EcLowPhlGoal.s_split_index`), records the **resolved** value in the node, and +both the rule and the checker build subgoals through the same pure low-level +core (`hoare_seq_subgoals : sHoareS -> hoare_seq_node -> form list`), which splits +at the integer with `split_at_nmcgap1` (no env). The rule builds its subgoals via +that core too, so faithfulness is by construction: the checker reruns the exact +same function on the exact same recorded data. + +Rule of thumb when migrating: **record the lowest-level value that still +determines the subgoals** (a resolved index, a typed formula, an instantiated +witness) — never the surface syntax that produced it. The high-level +`*_rule` record is the rule's *input*; the `*_node` record is what survives into +the proof and the checker. ## 8. Per-tactic migration recipe 1. Create `src/phl///ecPhl…` (or `Ec`) keeping a globally-unique module name. -2. Define the typed parameter record `__rule = { _… }` (prefixed - fields, §7b) and extract the pure core - `__subgoals : LDecl.hyps -> -> __rule -> form list` - from the existing `t_*_r` (everything up to the `xmutate1` call; take `hyps` - and derive `env = LDecl.toenv hyps` inside). -3. Add `type EcCoreGoal.rule += R of __rule`. -4. Write the canonical rule in `rules/*` taking the record: - `t__ : __rule -> backward`, body - `FApi.xrule1 tc (R… r) (<…>_subgoals (FApi.tc1_hyps tc) j r)`. Turn the legacy - `phl/*` `t_*` (positional `.mli` unchanged) into a thin adapter that builds the - record and calls it. If the tactic's `EcParsetree` info is still a tuple, - convert it to a record (§7b) at the same time. +2. Define two records (prefixed fields, §7b/§7c): the high-level **rule + arguments** `__rule` (symbolic positions, untyped-derived data as + supplied by callers) and the low-level **node payload** `__node` + (resolved indices, typed data). Extract the pure low-level core + `__subgoals : -> __node -> form list` from + the existing `t_*_r` — everything from *after* resolution up to the `xmutate1` + call. It should need no env (resolution already happened); if it genuinely + needs more, pass it explicitly. +3. Add `type EcCoreGoal.rule += R of __node`. +4. Write the canonical rule in `rules/*` taking the rule-arguments record: + `t__ : __rule -> backward`. Body: do the env-dependent + resolution (e.g. `EcLowPhlGoal.s_split_index`), build the `<…>_node`, then + `FApi.xrule1 tc (R… n) (<…>_subgoals j n)`. Turn the legacy `phl/*` `t_*` + (positional `.mli` unchanged) into a thin adapter that builds the rule record + and calls it. If the tactic's `EcParsetree` info is still a tuple, convert it + to a record (§7b) at the same time. 5. Register the checker with `EcPhlRecheck.checker_of "-" pf_as_ - (fun hyps j -> __subgoals hyps j r)` — no per-rule comparison code. + (fun _hyps j -> __subgoals j n)` — runs only the post-resolution + core, no comparison code. 6. Write `process__ : _info -> backward` (taking the parsetree record): validate the surface syntax for that logic, type the arguments, build the rule record and call `t__`. In the `phl/*` dispatcher diff --git a/src/phl/rules/hoare/ecHoareSeq.ml b/src/phl/rules/hoare/ecHoareSeq.ml index cabd1de66c..7a2ed8ccb5 100644 --- a/src/phl/rules/hoare/ecHoareSeq.ml +++ b/src/phl/rules/hoare/ecHoareSeq.ml @@ -11,49 +11,59 @@ open EcLowPhlGoal module TTC = EcProofTyping (* -------------------------------------------------------------------- *) -(* Parameters of the hoare [seq] rule. Recorded in the proof-node, so the - checker can recompute the rule's subgoals. *) +(* Parameters of the hoare [seq] rule as supplied by the caller: high level, the + split position is still a symbolic code gap that must be resolved. *) type hoare_seq_rule = { hsr_at : EcMatching.Position.codegap1; (* split position *) hsr_mid : ss_inv; (* intermediate assertion *) } -type EcCoreGoal.rule += RHoareSeq of hoare_seq_rule +(* Low-level parameters recorded in the proof-node: the split position is the + RESOLVED integer index. The checker recomputes the subgoals from this, so it + never redoes code resolution. *) +type hoare_seq_node = { + hsn_at : EcMatching.Position.nm_codegap1; (* resolved split index *) + hsn_mid : ss_inv; (* intermediate assertion *) +} + +type EcCoreGoal.rule += RHoareSeq of hoare_seq_node (* -------------------------------------------------------------------- *) -(* Pure core shared by the rule (to build the subgoals) and its checker (to - recompute and re-validate them): splitting a [hoareS] statement at [hsr_at] - with intermediate assertion [hsr_mid] yields the pre/mid and mid/post goals. - It takes the goal's hypotheses (its environment is [LDecl.toenv] of them) so - the rule and checker share the same context. *) -let hoare_seq_subgoals hyps (hs : sHoareS) (r : hoare_seq_rule) : form list = - let env = EcEnv.LDecl.toenv hyps in - let phi = ss_inv_rebind r.hsr_mid (fst hs.hs_m) in - let s1, s2 = s_split env r.hsr_at hs.hs_s in +(* Pure low-level core shared by the rule and its checker: split the statement + at the already-resolved index and build the pre/mid and mid/post subgoals. + Needs no environment — code resolution happened upstream, in the rule. *) +let hoare_seq_subgoals (hs : sHoareS) (n : hoare_seq_node) : form list = + let phi = ss_inv_rebind n.hsn_mid (fst hs.hs_m) in + let s1, s2 = EcMatching.Position.split_at_nmcgap1 n.hsn_at hs.hs_s in let post = update_hs_ss phi (hs_po hs) in let a = f_hoareS (snd hs.hs_m) (hs_pr hs) (stmt s1) post in let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in [a; b] (* -------------------------------------------------------------------- *) -(* Rule (TCB): split according to [r], emit a recheckable node recording it. - This canonical rule takes the parameter record; the legacy positional - interface (EcPhlSeq.t_hoare_seq) adapts onto it. *) +(* Rule (TCB): resolve the code gap to an index (the env-dependent step), record + the resolved node, and build its subgoals through the shared core. The + canonical rule takes the high-level record; the legacy positional interface + (EcPhlSeq.t_hoare_seq) adapts onto it. *) let t_hoare_seq_r (r : hoare_seq_rule) tc = - let hs = tc1_as_hoareS tc in - FApi.xrule1 tc (RHoareSeq r) (hoare_seq_subgoals (FApi.tc1_hyps tc) hs r) + let env = FApi.tc1_env tc in + let hs = tc1_as_hoareS tc in + let n = { hsn_at = s_split_index env r.hsr_at hs.hs_s; + hsn_mid = r.hsr_mid; } in + FApi.xrule1 tc (RHoareSeq n) (hoare_seq_subgoals hs n) let t_hoare_seq = FApi.t_low1 "hoare-seq" t_hoare_seq_r (* -------------------------------------------------------------------- *) -(* Checker: read the judgement, rerun the shared builder on the recorded params, - and compare against the stored subgoals (see [EcPhlRecheck]). *) +(* Checker: rerun ONLY the low-level core on the recorded index (see + [EcPhlRecheck]). It never redoes code resolution, so [normalize_cgap1] stays + out of its trust boundary. *) let () = register_rule_checker (function - | RHoareSeq r -> + | RHoareSeq n -> Some (EcPhlRecheck.checker_of "hoare-seq" pf_as_hoareS - (fun hyps hs -> hoare_seq_subgoals hyps hs r)) + (fun _hyps hs -> hoare_seq_subgoals hs n)) | _ -> None) (* -------------------------------------------------------------------- *)