Derive normalization rules from phino as checked data#72
Conversation
The eleven normalization rules currently live twice: as the hand-written Step relation and as display strings in Rules.lean, linked only by difftest. This adds scripts/gen-rule-data.py, which emits the root rules as structured RuleSpec tags under a fidelity lock that aborts when phino's YAML drifts from the locked interpretation (tested against result-change, condition-change, and added/removed-rule drift). docs/RULES-AS-DATA.md proposes the Lean layer that makes the pin kernel-checked: an interpreter RuleSpec.applies and a conformance theorem RootStep e e' iff the generated data denotes it. That layer is a reviewed draft only; it is not imported into PhiConfluence.lean, so the build and the [propext, Quot.sound] axiom gate are unchanged. docs/DESIGN.md points to it as milestone M5.
There was a problem hiding this comment.
Pull request overview
This PR introduces a new Python “fidelity lock” generator (scripts/gen-rule-data.py) intended to derive structured RuleSpec-style rule data from phino’s resources/*.yaml and abort on drift, and it adds design documentation describing how that generated data could later be kernel-checked against the Lean Step relation.
Changes:
- Add
scripts/gen-rule-data.pyto generate LeanRuleSpecdata with strict drift assertions against phino YAML rendering. - Add a detailed proposal doc (
docs/RULES-AS-DATA.md) describing the intended Lean schema/interpreter + conformance theorem wiring. - Update
docs/DESIGN.mdto reference the new “rules as checked data” milestone (M5).
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 5 comments.
| File | Description |
|---|---|
| scripts/gen-rule-data.py | New generator script that “locks” each of the 11 root rules to expected phino-rendered (pattern/result/conditions) and emits structured Lean-facing tags. |
| docs/RULES-AS-DATA.md | New design note proposing the Lean-side schema + conformance theorem plan and the rationale for a data/display split. |
| docs/DESIGN.md | Adds an M5 milestone entry summarizing the “rules as checked data” approach and its intended impact. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
ruff.yml runs `ruff check` on push and pull requests. To pass the default ruleset, split the combined imports (E401) and the multi-statement semicolon lines (E702) in both generator scripts; pyflakes found no bugs.
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
rules-in-sync regenerated Rules.lean from phino master, so a phino release drifting past the version this repo targets (0.0.0.74) turned the job red with no change here. Pin phino in one place — .phino-version — and read it everywhere: regen-rules.sh clones that tag, difftest.yml downloads that binary, and difftest.sh/confluence-probe.sh pass --pin so phino aborts on a version mismatch.
The pin commit cloned --branch 0.0.0.74, but phino's git tags drop the leading component (0.0.74), so the clone failed and rules-in-sync stayed red; derive the tag from .phino-version. It also passed --pin after the `rewrite` subcommand, but --pin is a global option that must precede it (`phino --pin=… rewrite …`), so every call errored to empty output and difftest failed. Verified: regen now reproduces the committed Rules.lean.
Drop docs/RULES-AS-DATA.md (the rules-as-data proposal, including the uncompiled Lean conformance-layer draft) and the now-dangling references to it: the M5 paragraph in DESIGN.md and two comments in gen-rule-data.py.
scripts/gen-rule-data.py emits the eleven root rules as structured RuleEntry tags (types in RuleSchema.lean) from pinned phino. The committed RuleData.lean is compiled as part of the library, and rule-data-in-sync.yml regenerates it from pinned phino and fails on any diff — mirroring rules-in-sync for the display table. Verified with a full local `lake build`.
Replace the separate rule-data-in-sync diff check with regeneration in the main build job: build.yml runs scripts/regen-rule-data.sh (clone pinned phino, run the generator) before `lake build`, so the proof is compiled against rules freshly generated from phino. A phino change that breaks compilation, or trips the generator's fidelity lock, fails the build. Verified locally with regen + full `lake build`.
build.yml now regenerates both generated files — Rules.lean and RuleData.lean — from pinned phino before `lake build`, so the proof and demo always compile against phino-derived rules. The separate rules-in-sync diff job is redundant now that the build regenerates Rules.lean itself, mirroring the earlier rule-data-in-sync removal. Verified with a local regen-both + full `lake build`.
|
@maxonfjvipon take a look, this is cleaner: on every CI build we take phino YAML files and generate .lean files from them, replacing the files we have in the code base |
maxonfjvipon
left a comment
maxonfjvipon
left a comment
There was a problem hiding this comment.
The pin (.phino-version + --pin + tag clone) is a clear win and could merge alone. The data layer is less than the title says: the tags are hand-written in LOCK, the script only checksums phino's YAML, and RuleData.lean is consumed by nothing — without applies and the conformance theorem, the lock catches exactly the drift rules-in-sync already caught.
The PR body is also stale: it references docs/RULES-AS-DATA.md (deleted in 76d9ac9), milestone M5, and RuleSpec.applies — none are in the diff — and says the Lean layer "is not imported into PhiConfluence.lean" while the diff imports it. It says the drift detection "is tested", but no tests ship here.
Suggest splitting: merge the pin now, hold the data layer until the conformance proof lands — or at least sync the body with the diff.
| - uses: actions/setup-python@v5 | ||
| with: | ||
| python-version: '3.x' | ||
| - name: Regenerate Rules.lean and RuleData.lean from pinned phino |
There was a problem hiding this comment.
rules-in-sync had git diff --exit-code; this regen-and-overwrite never compares against the committed files. Committed Rules.lean/RuleData.lean can now drift silently from what CI builds, and a local lake build uses different sources than CI. Add a diff check after regen, or stop committing the generated files.
| f"FIDELITY-LOCK BREACH for rule '{name}': phino's YAML no longer matches the " | ||
| f"locked interpretation in gen-rule-data.py.\n phino : {g}\n locked: {w}\n" | ||
| f"Re-read the phino rule, update LOCK['{name}'] AND the matching tags, and " | ||
| f"re-verify PhiConfluence/RuleConform.lean's `conformance` against `Step`.") |
There was a problem hiding this comment.
Points to PhiConfluence/RuleConform.lean, which doesn't exist in this PR.
| tags — the redex it fires on, its side-conditions, and its contractum. These are *data* | ||
| describing the eleven `phino` rules; the proof relation `Step` (`Step.lean`) is the | ||
| authoritative hand-written object, and `RuleData.lean` is kept identical to phino by the | ||
| `rule-data-in-sync` CI job. |
There was a problem hiding this comment.
References the rule-data-in-sync CI job, dropped in 82fe64d — the build job does this now.
| return f"index({rterm(v)})" | ||
| if k == "length": | ||
| return f"|{rterm(v)}|" | ||
| if k == "domain": |
There was a problem hiding this comment.
The "identical, kept in sync on purpose" copy is already out of sync — gen-rules.py has no domain branch (same output via its fallback today, but that's the drift trap in action). Extract a shared module instead of duplicating.
This adds
scripts/gen-rule-data.py, a deriver that turns phino'sresources/*.yamlinto structuredRuleSpecdata for the eleven root rules. It works as a fidelity lock: rather than free-text parsing, it carries one locked interpretation per rule and aborts if phino's rendered pattern, result, or condition drifts from it. The drift detection is tested against result changes, condition changes, and added/removed rules.Today the rules effectively exist twice — the hand-written
Steprelation and the display strings inRules.lean— linked only bydifftest, which compares one strategy's normal forms on a curated corpus.docs/RULES-AS-DATA.mdproposes the Lean layer that turns that into a kernel-checked pin: an interpreterRuleSpec.appliesplus a conformance theorem (RootStep e e'iff the generated data denotes it). With both in place, a phino change either trips the deriver or breaks the theorem.One caveat for the reviewer: the Lean layer ships here as a reviewed draft only — it is not imported into
PhiConfluence.lean, so the build and the[propext, Quot.sound]axiom gate are unchanged until it's compiled (I didn't have a Lean toolchain on hand). The remaining work — finishing the backward direction of the conformance proof and wiring the CI — is written up as milestone M5 inDESIGN.md. That note also flags a small pre-existing bug it resolves:gen-rules.py'sξ-strip is a no-op because phino's key isxi-free, notxi, so the data/display split introduced here is the clean fix.