phl: reorganize the program logic into a recheckable four-layer structure#1041
Draft
strub wants to merge 4 commits into
Draft
phl: reorganize the program logic into a recheckable four-layer structure#1041strub wants to merge 4 commits into
strub wants to merge 4 commits into
Conversation
Begin the src/phl reorganization into a four-layer spine (dispatch / elaboration / TCB rule / checker) with re-checkable proof-nodes, applied one tactic at a time. Kernel (ecCoreGoal): - open `type rule = ..` and a new `VRule of rule * handle list` validation node (the recheckable sibling of the opaque `VExtern`); - `FApi.xrule[1][_hyps]` emitting `VRule`; - a checker registry (`register_rule_checker`) over the open rule type, `recheck_proofenv` driver, and `RecheckFailure`. The driver runs at qed (ecScope.save_r) gated by the EC_RECHECK env var; unmigrated `VExtern` nodes and rules without a registered checker are skipped, so migration is incremental. Pilot: hoare `seq` migrated to rules/hoare/ecHoareSeq.ml — pure subgoal-builder shared by the rule and its checker, `RHoareSeq` node recording the split position + intermediate assertion. EcPhlSeq routes its hoareS arm here and re-exports t_hoare_seq, so the public interface and external callers are unchanged. Docs: src/phl/README.md (spine + layout convention) and src/phl/REFACTORING.md (plan, rationale, per-tactic recipe). Validated: 91 stdlib theories + 23 seq-using tests compile under EC_RECHECK=1 with zero RecheckFailure.
Extract the destruct/rebuild/compare boilerplate common to every proof-node checker into its own module, src/phl/ecPhlRecheck.ml: - recheck_forms: arity check + per-subgoal is_conv under each subgoal's own hypotheses; - checker_of name destr build: assemble a rule_checker from a pf_as_* reader and a subgoal builder, wrapping any exception raised while reading/rebuilding into a RecheckFailure (so a checker never leaks a raw user-level exception). The shared subgoal-builder now takes the goal's hypotheses (the authoritative context; env is just LDecl.toenv of it, and the conversion check needs hyps anyway) instead of a pre-projected env, so the rule and its checker reason in the same context. hoare_seq_subgoals updated accordingly; the rule passes FApi.tc1_hyps. check_hoare_seq collapses to its checker_of registration. Docs (README, REFACTORING) updated: builder signature, the EcPhlRecheck factoring, the migration recipe, and a note that hyps-changing rules (xrule*_hyps, e.g. while) will need a hyps-aware recheck variant.
Make the seq tactic self-documenting via records, and clean up its
dispatcher.
- EcParsetree.seq_info becomes a record { seqi_side; seqi_at; seqi_mid;
seqi_bd } (built at the one grammar site) instead of a 4-tuple.
- The migrated rule in rules/hoare/ exposes a parameter record
hoare_seq_rule { hsr_at; hsr_mid }, carried by the RHoareSeq node and
consumed by the shared subgoal-builder. The canonical
EcHoareSeq.t_hoare_seq takes that record; the legacy EcPhlSeq.t_hoare_seq
keeps its positional .mli and is a thin adapter onto it, so external
callers are untouched.
- process_hoare_seq takes the seq_info record and owns the hoare
surface-syntax validation (no side, no bound, single position/assertion).
- process_seq dispatches by pattern-matching the goal's f_node (no is_*
predicates); the five `when is_X` guards collapse to four F...S _ arms
plus a shared bad_params fallback reproducing the original error
messages exactly.
Docs (REFACTORING 7b + recipe, README) updated for the two-record
convention, the rules/*-record / phl/*-positional-adapter split, and
f_node dispatch.
Build clean; pilot + 23 seq-using files pass under EC_RECHECK=1 with
zero RecheckFailure.
The checker is trusted re-validation, so it must not redo elaboration
work the rule already did. The hoare-seq checker was re-resolving the
symbolic code gap (via s_split), pulling all of code-position
normalization into its trust boundary.
Split the parameters into two records: the high-level rule arguments
(hoare_seq_rule, with a symbolic codegap1) that the canonical rule
takes, and the low-level node payload (hoare_seq_node, with the resolved
nm_codegap1 integer index) that is recorded and rechecked. The rule
resolves the gap once (new EcLowPhlGoal.s_split_index = normalize_cgap1
with the s_split error), records the resolved node, and builds subgoals
through a pure low-level core that splits at the integer
(split_at_nmcgap1, no env). The checker reruns only that core, so
normalize_cgap1 stays out of its TCB; faithfulness is by construction
since the rule builds its subgoals through the same core.
Docs: new REFACTORING 7c ("the checker is post-resolution; the node
records resolved data") + rule of thumb to record the lowest-level value
that still determines the subgoals; 7b lists both records; recipe and
README spine updated.
Build clean; pilot + 23 seq files pass under EC_RECHECK=1.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Goal
Replace today's "one file per tactic, all logics inside, typing entangled with goal-inspecting dispatch, opaque proof-nodes" structure with a uniform four-layer spine per tactic:
process_<tactic>— logic-agnostic, inspects the goal kind, routes;process_<logic>_<tac>— types the parse-tree args, builds params;t_<logic>_<tac>— computes subgoals via a pure shared builder and emits a node recording its params;check_<logic>_<tac>— reruns the builder from the recorded params andis_conv-compares against the stored subgoals.Today a proof-node (
VExtern tc \Tag [...]`) records that a rule fired but not with what — the tag carries no parameters and is never inspected — so proofs cannot be re-validated. This refactor makes every TCB step carry its parameters and registers a checker for it.Kernel (
ecCoreGoal)type rule = ..+VRule of rule * handle list(recheckable sibling ofVExtern);FApi.xrule[1][_hyps]emittingVRule;register_rule_checker) over the openruletype,recheck_proofenvdriver,RecheckFailure.The driver runs at
qed(ecScope.save_r), gated by theEC_RECHECKenv var. Unmigrated nodes and rules with no registered checker are skipped, so migration is incremental and normal runs pay nothing.Layout (by family, then logic)
(include_subdirs unqualified)flattenssrc/into one library, so subdirs need no dune changes (module names stay globally unique):rules/<logic>/— genuine logic rules (hoare/ehoare/bdhoare/equiv/eager)codetx/— logic-uniform program transforms (wp, sp, inline, swap, rcond, …)bridge/— probabilistic / cross-logic (deno, pr, byequiv, fel, upto, eager)multi/— multi-logic tactics with shared machinery (conseq, trans, sym)Progress
Phase 0 — scaffolding ✅ kernel
rule/VRule/xrule, checker registry +recheck_proofenv,EC_RECHECKhook, docs.Tactic migrations (each = a commit;
seq/hoare is the reference pilot):seq— hoareseq— ehoare / bdhoare / equiv (+ one-sided)skipwp/sp(codetx pilot)cond/matchrndwhile(+ async)callfunexistsrcond/rmatchinline,swap,kill/alias/cfold(codetx)fission/fusion/unroll/splitwhile(looptx)deno,pr,byequiv,fel,upto,eager(bridge)conseq/trans/sym(multi-logic, last)Validation (continuous)
Every increment keeps
dune buildclean, the test suite green (-no-eco), and a fullEC_RECHECK=1sweep over the stdlib at zeroRecheckFailure. Current: 91 theories + 23seq-using tests pass underEC_RECHECK=1.