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/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..487d0c142 --- /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 000000000..71910a51b --- /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 0b14bf08e..ade2e0a0e 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 000000000..bb11e80c6 --- /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 000000000..c615e4dbf --- /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