From 4beaa8f81e1a31eed34df1f005e40552653c97ff Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 6 Oct 2026 17:36:49 +0200 Subject: [PATCH] feat(pl): recheckable proof-nodes for program-logic rules First PR of a stack that reorganizes the program-logic tactics (src/phl) into a uniform four-layer structure per tactic (dispatch, elaboration, rule, checker), one tactic class per PR. The design and the per-tactic recipe are in src/phl/REFACTORING.md; src/phl/README.md is the short reference. This supersedes the draft #1041. The design also fixes two conventions every migrated rule follows: a trusted rule is stated on exactly the statement it governs, with no implicit seq-ing or framing (splitting is the seq rule's job, framing that of a single frame rule per logic; surface tactics acting on larger programs are derived compositions), and each rule is documented in its .mli as an inference rule, separately from the derived tactics. Today a low-level tactic closes its goal with an opaque VExtern node: the tag records that a rule fired, not with which parameters, so a proof step cannot be re-validated. This PR adds the kernel support for recheckable nodes, without migrating any rule yet: - ecCoreGoal: an open `rule` type and a `VRule of rule * handle list` validation node, emitted by FApi.xrule / xrule1 / xrule_hyps / xrule1_hyps; a registry of rule checkers (register_rule_checker) and a driver, recheck_proofenv, that reruns the checker of every VRule node of a proof (raising RecheckFailure on mismatch). Nodes without a registered checker, and VExtern nodes, are skipped. - ecScope: the driver runs at `qed` when EC_RECHECK is set, so normal runs pay nothing. - EcPlRecheck: shared checker scaffolding. A checker rebuilds the subgoals from the recorded parameters and compares them, up to conversion, with the stored ones. No behaviour change: with no rule migrated, the stdlib and the unit tests pass unchanged, with and without EC_RECHECK=1. --- src/ecCoreGoal.ml | 76 +++++++++ src/ecCoreGoal.mli | 33 ++++ src/ecScope.ml | 4 +- src/phl/README.md | 98 ++++++++++++ src/phl/REFACTORING.md | 335 ++++++++++++++++++++++++++++++++++++++++ src/phl/ecPlRecheck.ml | 45 ++++++ src/phl/ecPlRecheck.mli | 22 +++ 7 files changed, 612 insertions(+), 1 deletion(-) create mode 100644 src/phl/README.md create mode 100644 src/phl/REFACTORING.md create mode 100644 src/phl/ecPlRecheck.ml create mode 100644 src/phl/ecPlRecheck.mli diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 728824b4d..e7b85837d 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; @@ -163,6 +171,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 *) @@ -543,6 +555,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) @@ -999,6 +1035,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 2f1b51740..7af9ba8ab 100644 --- a/src/ecCoreGoal.mli +++ b/src/ecCoreGoal.mli @@ -147,6 +147,11 @@ type pregoal = { g_simpl : EcEnv.simplify_context; } +(* 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 *) @@ -161,6 +166,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; @@ -188,6 +196,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 @@ -292,6 +316,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 50af5d56e..718657540 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -1071,7 +1071,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 000000000..4b7784de3 --- /dev/null +++ b/src/phl/README.md @@ -0,0 +1,98 @@ +# 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 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 [`ecPlRecheck.ml`](ecPlRecheck.ml): +`EcPlRecheck.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 node -> + Some (EcPlRecheck.checker_of "-" pf_as_ + (fun _hyps j -> __subgoals j node)) + | _ -> 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. + +## Trusted rules + +- A TCB rule is stated on exactly the statement it governs: **no implicit + seq-ing** (splitting is the `seq` rule's job) and **no implicit framing** + (generalizing over modified variables is the frame rule's job). Surface + tactics acting on a larger program are derived compositions of these. +- Each rule module's `.mli` documents its TCB rules as inference rules (with + their node and checker), then its derived tactics (with what they expand to), + then its elaboration entry points. + +See `REFACTORING.md` §7d–§7e. + +## 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 hoare_seq_node`. +- `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 +``` diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md new file mode 100644 index 000000000..ed6668e03 --- /dev/null +++ b/src/phl/REFACTORING.md @@ -0,0 +1,335 @@ +# 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. +6. **Rules do implicit seq-ing and framing.** Many TCB rules act on a larger + program than the statement they are about: `rnd` and `call` take + `c; i` and keep the prefix `c` (an implicit `seq`), and `call`, `while`, + `rcond`, … generalize their conditions over the modified variables (an + implicit frame, `generalize_mod`). Each rule thus re-implements, slightly + differently, the side conditions of `seq` and of the frame rule; this has + been a recurring source of soundness bugs. + +## 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 : 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, [`ecPlRecheck.ml`](ecPlRecheck.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) + +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 hoare_seq_node`. +- `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 program-logic 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 + +- **Basis** — kernel `rule`/`VRule`/`xrule`, checker registry, + `recheck_proofenv`, `EC_RECHECK` hook, `EcPlRecheck`, layout, this doc + + README. No rule uses it yet. +- **Then one PR per tactic class**, all of its logics at once, roughly by + increasing difficulty: seq (the reference, proving the whole spine + end-to-end with real rules + checkers) → frame (the frame rule of §7d, + which every other rule relies on) → skip → wp/sp (codetx pilot) → cond + → rnd → while → call → fun → exists → … → the rest of conseq / trans / sym + last. + +Each PR: move the code 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 change to any existing proof script in `theories/`, `tests/` or + `examples/` (new tests exercising a migrated rule are welcome). +- `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 copy on the program-logic side — 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. +- **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. +- **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. + +## 7d. No implicit seq-ing, no implicit framing + +A TCB rule is stated on **exactly the statement it governs**: + +- **No implicit seq-ing.** The `rnd` rule is about `x <$ d`, the `call` rule + about `x <- f(a)`, the `if` rule about `if b then c1 else c2` — never about + `c; x <$ d`. Splitting a program is done by the `seq` rule, and only by it. +- **No implicit framing.** A rule does not generalize its conditions over the + variables written by the program. Framing is done by a single *frame* rule + per logic — a framed weakening of the postcondition — and only by it: + + ``` + forall &m, P => forall (mod c), Q' => Q hoare [c : P ==> Q'] + ------------------------------------------------------------------- + hoare [c : P ==> Q] + ``` + + The framed consequence (also strengthening the precondition) is derived: + the frame rule followed by the consequence rule. + +Surface tactics that act on a larger program (`rnd` on the last instruction, +`call`, `while`, …) are **derived**: they compose `seq` (at the position they +act on, with the intermediate assertion they compute today), the frame rule (or +the framed consequence), and the single-statement rule, and close the premises +they always closed. The user-visible subgoals are therefore unchanged, while +the TCB shrinks to small single-statement rules plus `seq` and the frame rules, +each with its own checker. + +## 7e. Each rule is documented, in the `.mli`, as an inference rule + +The `.mli` of a rule module has three sections, in this order: + +- **Rules (trusted).** Each TCB rule as an inference rule — premises above the + line, conclusion below, side conditions next to it — followed by the node it + records and the name of its checker. For instance: + + ``` + (* [t_hoare_seq { hsr_at = k; hsr_mid = R }] + + hoare [c1 : P ==> R] hoare [c2 : R ==> Q] + ------------------------------------------------ c = c1; c2 + hoare [c : P ==> Q] (c1 = c[0..k)) + + Node: RHoareSeq { hsn_at = k (resolved); hsn_mid = R }. + Checker: "hoare-seq". *) + ``` + +- **Derived tactics.** Each derived tactic, with the rules it expands to and + the premises it closes itself. +- **Elaboration.** The `process_*` entry points, described as surface syntax. + +So what is trusted, which rule is applied, and what is derived is readable +from the interface alone. + +## 8. Per-tactic migration recipe + +1. Create `src/phl///ecPhl…` (or `Ec`) keeping a + globally-unique module name. +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. Do not wrap the rule in + `FApi.t_low0..4`: they ignore their name argument and are the identity, so + drop them from each tactic as it is ported. +5. Register the checker with `EcPlRecheck.checker_of "-" pf_as_ + (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 + `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. Remove implicit seq-ing and framing (§7d): restate the rule on the single + statement it governs, and make the surface tactic a derived composition of + `seq`, the frame rule (or the framed consequence) and that rule, producing + the same subgoals as before. +9. Document the module's `.mli` as in §7e. +10. 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/ecPlRecheck.ml b/src/phl/ecPlRecheck.ml new file mode 100644 index 000000000..f4866bff9 --- /dev/null +++ b/src/phl/ecPlRecheck.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/ecPlRecheck.mli b/src/phl/ecPlRecheck.mli new file mode 100644 index 000000000..6e1c08a21 --- /dev/null +++ b/src/phl/ecPlRecheck.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