Derive normalization rules from phino as checked data by yegor256 · Pull Request #72 · objectionary/proof

yegor256 · 2026-06-04T12:24:26Z

This adds scripts/gen-rule-data.py, a deriver that turns phino's resources/*.yaml into structured RuleSpec data 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 Step relation and the display strings in Rules.lean — linked only by difftest, which compares one strategy's normal forms on a curated corpus. docs/RULES-AS-DATA.md proposes the Lean layer that turns that into a kernel-checked pin: an interpreter RuleSpec.applies plus 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 in DESIGN.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 is xi-free, not xi, so the data/display split introduced here is the clean fix.

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.

Copilot

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.py to generate Lean RuleSpec data 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.md to 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>

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`.

yegor256 · 2026-06-04T15:32:02Z

@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

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.

maxonfjvipon · 2026-06-06T07:22:10Z

+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'
+      - name: Regenerate Rules.lean and RuleData.lean from pinned phino


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.

maxonfjvipon · 2026-06-06T07:22:10Z

+            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`.")


Points to PhiConfluence/RuleConform.lean, which doesn't exist in this PR.

maxonfjvipon · 2026-06-06T07:22:11Z

+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.


References the rule-data-in-sync CI job, dropped in 82fe64d — the build job does this now.

maxonfjvipon · 2026-06-06T07:22:11Z

+            return f"index({rterm(v)})"
+        if k == "length":
+            return f"|{rterm(v)}|"
+        if k == "domain":


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.

Favixx

The fidelity-lock idea is good — asserting phino's rendered pattern/result/condition against a locked interpretation, and failing loudly on drift, is a much stronger pin than free-text parsing, and the RuleEntry vocabulary in RuleSchema.lean reads well.

My concern is with what the pinning does to the drift detection that already existed, and it is the reason I'm requesting changes rather than just commenting:

rules-in-sync.yml is deleted, and its git diff --exit-code gate is not replaced. build.yml now regenerates Rules.lean and RuleData.lean and compiles the result, but never compares it against what is committed — so the two tracked files can drift from phino indefinitely while CI stays green, and a reader of the repo sees a rule table nothing checks.
The old job deliberately tracked phino latest, which is what made drift loud. After this PR everything — regen-*.sh, difftest, confluence-probe — is pinned to .phino-version, and nothing anywhere compares that pin against phino's actual latest. There is no renovate config in this repo either.

Concretely: .phino-version says 0.0.0.74, tagged 2026-06-03. phino is at 0.0.106 as of 2026-07-23 — 32 releases later. That gap opened up while this PR was in review, and no CI job in it would ever have said so. Since difftest is the behavioral pin of Step to the reference implementation, pinning it means the proof is now differentially tested against a phino from June.

I'm not arguing against the pin — determinism is a fair goal. But the pin needs something that fails when it goes stale (a scheduled job comparing .phino-version to phino's latest tag, or renovate), otherwise this trades a loud failure for a silent one.

Two smaller process notes: the description points the reviewer at docs/RULES-AS-DATA.md, which is not in this PR and not on master — I reviewed without it. And the caveat that the Lean layer "is not imported into PhiConfluence.lean" is contradicted by the diff (see inline). Rest is inline and minor.

Favixx · 2026-07-28T19:53:30Z

@@ -0,0 +1 @@
+0.0.0.74


0.0.0.74 was phino's tip when this PR was opened (tag 0.0.74, 2026-06-03), but phino ships fast: it is at 0.0.106 now (2026-07-23), 32 releases later. Nothing in this repo will ever tell you that — there is no renovate config, and after this PR every consumer of phino (regen-rules.sh, regen-rule-data.sh, difftest.sh, confluence-probe.sh) reads this file, so they all agree with each other and none of them agrees with reality.

Since difftest is what pins Step to phino behaviorally, a stale pin quietly narrows the theorem's meaning: it becomes confluence-versus-June-phino. Please add something that fails on staleness — a scheduled workflow diffing this file against gh api repos/objectionary/phino/tags, or a renovate rule — otherwise the loud failure this PR removes doesn't come back anywhere.

Favixx · 2026-07-28T19:53:30Z

-      - name: Regenerate rules from phino (latest) and detect drift
-        run: |
-          bash scripts/regen-rules.sh
-          if ! git diff --exit-code PhiConfluence/Rules.lean; then


This git diff --exit-code is the whole gate: it is what made "the displayed rules cannot drift from phino" a checkable claim rather than a convention. Deleting the workflow removes it, and build.yml does not replace it — it regenerates and compiles, but never compares.

After this PR, PhiConfluence/Rules.lean and PhiConfluence/RuleData.lean are tracked files that CI overwrites before every build, so what is committed is never verified against what is compiled. Someone hand-editing Rules.lean (the header says DO NOT EDIT, but still) would see a green build. Please keep the gate — see my comment on build.yml, it is three lines.

Favixx · 2026-07-28T19:53:30Z

+        run: |
+          pip install pyyaml
+          bash scripts/regen-rules.sh
+          bash scripts/regen-rule-data.sh


Regenerating into the working tree right before lake build means the build compiles files that may differ from the committed ones, and says nothing about the difference. Restoring the deleted gate here is cheap and keeps the new pinning:

bash scripts/regen-rules.sh bash scripts/regen-rule-data.sh git diff --exit-code PhiConfluence/Rules.lean PhiConfluence/RuleData.lean \ || { echo "::error::generated rules are out of sync — run the regen scripts and commit"; exit 1; }

That way the build still compiles phino-derived rules, and a stale committed file fails instead of being silently replaced.

Favixx · 2026-07-28T19:53:30Z

      - uses: ./.github/actions/setup-lean
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'


python-version: '3.x' plus an unpinned pip install pyyaml on line 25 sits oddly in a PR whose whole subject is making the toolchain deterministic. Both float, and either one can change the generated RuleData.lean (or break gen-rule-data.py) without a commit here. If phino is worth pinning to a four-part version, Python and PyYAML are worth pinning to at least a minor.

Favixx · 2026-07-28T19:53:30Z

        run: |
-          sudo curl -fsSL -o /usr/local/bin/phino http://phino.objectionary.com/releases/ubuntu-24.04/phino-latest
+          version="$(cat .phino-version)"
+          sudo curl -fsSL -o /usr/local/bin/phino "http://phino.objectionary.com/releases/ubuntu-24.04/phino-$version"


Since this line is being rewritten anyway: it fetches an executable over plain http://, chmod +xes it and installs it into /usr/local/bin, and the only integrity check is that phino --version runs. Anyone able to answer that request controls what the differential test measures — and this PR is specifically about trusting phino as the reference. https:// if the host serves it, and ideally a checksum next to .phino-version that the workflow verifies.

Favixx · 2026-07-28T19:53:31Z

+
+# --- condition/where rendering: identical to gen-rules.py (kept in sync on purpose) ---
+
+def rterm(x):


rterm, rcmp, rcond and rwhere are copied verbatim from gen-rules.py — around sixty lines, kept in step by a comment saying "keep in sync". The fidelity lock compares strings produced by these functions against LOCK, so a divergence between the two copies would make the lock assert against a rendering the display table no longer uses, silently.

Both scripts live in scripts/ and this PR already touches both (and adds ruff over them), so this is the natural moment for scripts/phino_render.py imported by each. That also shrinks the diff for whoever reviews the next rule change.

Favixx · 2026-07-28T19:53:31Z

+        name = str(d["name"])
+        if name in found:
+            raise SystemExit(f"duplicate rule name '{name}' in {res_dir}")
+        got = (str(d["pattern"]), str(d["result"]), rcond(d.get("when")), rwhere(d.get("where")))


d["name"] (line 169) and d["pattern"]/d["result"] here are unguarded. A phino YAML that drops or renames one of those keys — precisely the kind of drift this script exists to catch — produces a bare KeyError traceback instead of the carefully written FIDELITY-LOCK BREACH message. Wrap them, and name the offending file in the error: path is right there in the loop and is the single most useful thing to print.

Favixx · 2026-07-28T19:53:31Z

+PHINO_VERSION="$(cat .phino-version)"
+# phino's package/binary version is 4-part (0.0.0.74), but its git tags drop the
+# leading component (0.0.74).
+PHINO_TAG="${PHINO_VERSION#0.}"


PHINO_TAG="${PHINO_VERSION#0.}" encodes "drop the leading component" as "strip a literal 0. prefix". For 0.0.0.74 that gives 0.0.74, correct today. For a future 0.1.0.5 it would give 1.0.5 — a tag that may well exist and point somewhere completely unrelated, so the clone succeeds and the rules are derived from the wrong phino. ${PHINO_VERSION#*.} says what is meant.

This block — comment, PHINO_VERSION, PHINO_TAG, clone, echo — is also duplicated verbatim in regen-rules.sh; the two scripts now differ only in which generator they call. A single script taking the generator and output as arguments, or a small sourced helper, would keep the version logic in one place.

Favixx · 2026-07-28T19:53:31Z

@@ -0,0 +1,27 @@
+#!/usr/bin/env bash


This file is added with mode 100644, while its siblings (regen-rules.sh, difftest.sh, confluence-probe.sh) are 755. It works because build.yml invokes it as bash scripts/regen-rule-data.sh, but the shebang on this line implies it is meant to be executable, and the usage comment says bash scripts/... for a script that should just be runnable. git update-index --chmod=+x.

Favixx · 2026-07-28T19:53:31Z

 set -uo pipefail
 cd "$(dirname "$0")/.."
 export PATH="$HOME/.elan/bin:$PATH"
+PHINO_VERSION="$(cat .phino-version)"


This reads .phino-version before the command -v phino guard below, and the script runs under set -uo pipefail without -e. If the file is missing or renamed, cat writes to stderr, PHINO_VERSION becomes empty, and every invocation gets --pin= — so the failure surfaces as phino complaining about an empty version, once per corpus entry, rather than as one clear message here. A [ -f .phino-version ] || { echo "FATAL: .phino-version missing" >&2; exit 1; } in the same style as the phino guard would keep the fail-fast behaviour the header advertises.

Copilot AI review requested due to automatic review settings June 4, 2026 12:24

Copilot started reviewing on behalf of yegor256 June 4, 2026 12:24 View session

Copilot AI reviewed Jun 4, 2026

View reviewed changes

Comment thread scripts/gen-rule-data.py Outdated

Comment thread scripts/gen-rule-data.py

Comment thread scripts/gen-rule-data.py

Comment thread docs/RULES-AS-DATA.md Outdated

Comment thread docs/DESIGN.md Outdated

yegor256 and others added 12 commits June 4, 2026 15:36

ci: add ruff workflow to lint Python scripts

46ade3d

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.

Potential fix for pull request finding

74b06a1

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Potential fix for pull request finding

edb5aa1

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Potential fix for pull request finding

9fe9659

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Potential fix for pull request finding

9e775bd

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Potential fix for pull request finding

dd7688f

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

docs: remove the rules-as-data design note

76d9ac9

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.

yegor256 requested a review from maxonfjvipon June 4, 2026 15:32

maxonfjvipon reviewed Jun 6, 2026

View reviewed changes

Favixx suggested changes Jul 28, 2026

View reviewed changes


		# --- condition/where rendering: identical to gen-rules.py (kept in sync on purpose) ---

		def rterm(x):

		@@ -0,0 +1 @@
		0.0.0.74

Uh oh!

Conversation

yegor256 commented Jun 4, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

yegor256 commented Jun 4, 2026

Uh oh!

maxonfjvipon left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Favixx left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants