diff --git a/src/ecCoreGoal.ml b/src/ecCoreGoal.ml index 4b75e5b0c..67b100851 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 f574b49bf..16342dada 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/ecLowPhlGoal.ml b/src/ecLowPhlGoal.ml index 416bb1562..1e1de9283 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/ecParser.mly b/src/ecParser.mly index 95d9999e6..300839935 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 e9deac3f9..b2589c909 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/ecScope.ml b/src/ecScope.ml index c6f1ff7fd..5e9d7f003 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 000000000..5751b2fd0 --- /dev/null +++ b/src/phl/README.md @@ -0,0 +1,94 @@ +# 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 [`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 node -> + Some (EcPhlRecheck.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. + +## 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. 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 new file mode 100644 index 000000000..4badad682 --- /dev/null +++ b/src/phl/REFACTORING.md @@ -0,0 +1,272 @@ +# 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 : 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) + +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`. + +## 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. +- **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. + +## 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. +5. Register the checker with `EcPhlRecheck.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. 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/ecPhlRecheck.ml b/src/phl/ecPhlRecheck.ml new file mode 100644 index 000000000..f4866bff9 --- /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 000000000..6e1c08a21 --- /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/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml index 0b14bf08e..b383a13ae 100644 --- a/src/phl/ecPhlSeq.ml +++ b/src/phl/ecPhlSeq.ml @@ -14,19 +14,13 @@ 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 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 = @@ -215,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 @@ -227,51 +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 -> - 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 - - | 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 new file mode 100644 index 000000000..7a2ed8ccb --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSeq.ml @@ -0,0 +1,89 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcParsetree +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +module TTC = EcProofTyping + +(* -------------------------------------------------------------------- *) +(* 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 *) +} + +(* 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 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): 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 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: 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 n -> + Some (EcPhlRecheck.checker_of "hoare-seq" pf_as_hoareS + (fun _hyps hs -> hoare_seq_subgoals hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* 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 (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 new file mode 100644 index 000000000..7d59ba5b2 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareSeq.mli @@ -0,0 +1,21 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position +open EcAst + +(* -------------------------------------------------------------------- *) +(* 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 *) +} + +(* 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