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

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

This PR makes phino the only source of the normalization rules. PhiConfluence/Rules.lean (the display table) and PhiConfluence/RuleData.lean (the rules as structured tags) are no longer kept in Git. .github/regen-rules.sh generates both from phino's resources/*.yaml before every build, locally and in CI.

The phino used is pinned in .phino-version, which names the release. .phino-sha256 verifies the binary that difftest downloads, since the release host serves plain HTTP only. A weekly phino-latest workflow fails when the pin falls behind phino's newest release, so a stale pin is reported, not silent.

.github/gen-rule-data.py is a fidelity lock, not a translator: it holds one hand-written interpretation per rule and aborts when phino's pattern, result or condition no longer matches it, or when a rule is added or removed. Both generators share one renderer, .github/phino_render.py. Unit tests in .github/test_*.py cover drift, malformed rule files and empty rule directories, and the build runs them. Python, PyYAML and ruff versions are pinned, and ruff's rules are set in ruff.toml.

The whole project now builds and checks with one command, make (GNU Make 4.3 or newer). It runs the generator tests, generates the rule files (only when .phino-version or a generator changes), runs lake build, and runs the sorry/axiom source check and the #print axioms check, which moved from build.yml into .github/axioms.lean. CI runs the same targets (make and make difftest), so a green local make means a green build job. Python dependencies are pinned in .github/requirements.txt. The scripts CI runs live directly in .github/, and scripts/confluence-probe.sh is removed: it probed for counterexamples before the Lean diamond existed, and no job ran it.

What this PR does not do: nothing checks the tags in RuleData.lean against Step yet, because there is no conformance theorem so far. The pin stays at phino 0.0.0.74 on purpose: phino 0.0.137 changed the rules in substance, which needs new proof work, tracked in #73. The ξ condition that .github/gen-rules.py claims to hide but never did is tracked in #74.

🤖 Generated with Claude Code

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

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

Fixed: the message no longer points at RuleConform.lean. It now says to update LOCK and its tags and to check Step by hand, since no conformance theorem exists yet.

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.

Fixed: the docstring no longer names a nonexistent job. It now says RuleData.lean is not tracked by Git and .github/regen-rules.sh generates it from pinned phino before every build.

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.

Fixed: the duplicated renderer is gone. Both generators now import .github/phino_render.py, and unit tests cover both.

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

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

The generated files are no longer committed at all (00fbe5c): .github/regen-rules.sh creates Rules.lean and RuleData.lean from pinned phino before every build, locally and in CI, so there is no committed copy that can differ from what is compiled. So the diff gate has nothing left to compare; phino is the only source of the rules.

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.

The host does not serve HTTPS (the TLS connection is reset), so the workflow now checks the download against .phino-sha256 with sha256sum --check --strict before installing it.

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.

Fixed: the duplicated renderer is gone. Both generators now import .github/phino_render.py, and unit tests cover both.

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.

Fixed: a rule file without name, pattern or result now fails with a one-line message naming the file, and the tests cover it.

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.

Fixed: it is now ${PHINO_VERSION#*.}. The two regen scripts are merged into one .github/regen-rules.sh, which also checks that the tag still points to the commit in .phino-commit.

Update: we later dropped .phino-commit (c100156). .phino-version alone pins phino now, since release tags are not moved in practice.

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.

This file is gone: it was merged into .github/regen-rules.sh, which is executable.

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.

Fixed: difftest.sh now fails with a clear message when .phino-version is missing.

The build regenerated Rules.lean and RuleData.lean without comparing them to the committed files, so they could drift silently. It now fails on any difference, runs unit tests for both generators, and verifies the phino binary against a pinned checksum. A weekly job reports when the phino pin falls behind the newest release. Both generators now share one renderer, fail with a clear message on malformed or missing rule files, and the stale references to jobs and files that do not exist are gone.

Rules.lean and RuleData.lean are now generated from the pinned phino before every build instead of being committed, so phino stays the only source of the rules and nothing needs a drift gate. Since a git tag can be moved, the regeneration also checks that the phino tag still points to the commit recorded in .phino-commit. Local builds must run scripts/regen-rules.sh before lake build.

Scripts that CI runs now sit next to the workflows that call them, so scripts/ keeps only confluence-probe.sh, a manual tool no job runs.

yegor256 · 2026-09-23T17:24:43Z

@Favixx @maxonfjvipon I have answered every inline comment, and the description now matches the diff. The main change since your reviews: Rules.lean and RuleData.lean are no longer kept in Git, and are generated from pinned phino before every build, so phino is the only source of the rules. On splitting the PR: we keep RuleData.lean here on purpose. The description now says plainly that nothing checks its tags against Step yet. Could you take another look?

The commit pin guarded only against someone moving a phino release tag, which does not happen in practice, and it added one more file to bump on every upgrade.

A local build took four ordered commands, and the axiom gate existed only inside build.yml. Now `make` runs the generator tests, generates the rule files from pinned phino when the pin or a generator changes, builds, and runs both gates, and CI calls the same targets, so a green local `make` means a green build job. confluence-probe.sh is removed: it probed for counterexamples before the Lean diamond existed, and no job ran it.

yegor256 · 2026-09-23T17:51:25Z

@Favixx @maxonfjvipon Since my last note, the PR also adds a Makefile: make now runs the generator tests, generates the rule files, builds, and runs both axiom checks, and CI calls the same targets. The CI scripts moved into .github/, .phino-commit was dropped in favor of .phino-version alone, and scripts/confluence-probe.sh is removed. The description is updated to match.

#72 moved rendering into .github/phino_render.py, shared by the display table and the fidelity lock, and stopped tracking Rules.lean. The lock keeps copy's xi-free guard (Step.copy carries xiFree), so the #74 fix becomes a strip_xi flag that only gen-rules.py turns on, with a test. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XWY8yTGgWJ1HXoFjmLt3AZ

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 .github/gen-rule-data.py

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

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

yegor256 added 2 commits September 23, 2026 19:12

Merge branch 'master' into rules-as-checked-data

5eade22

This was referenced Sep 23, 2026

Step in PhiConfluence/Step.lean follows phino 0.0.74 rules, phino 0.0.137 changed them #73

Open

gen-rules.py never strips the xi-free condition of copy it claims to strip #74

Closed

yegor256 added 2 commits September 23, 2026 19:39

refactor(ci): #72 move the scripts ci runs into .github

cadf727

Scripts that CI runs now sit next to the workflows that call them, so scripts/ keeps only confluence-probe.sh, a manual tool no job runs.

yegor256 requested review from Favixx and maxonfjvipon September 23, 2026 17:24

build(phino): #72 pin phino by version only

c100156

The commit pin guarded only against someone moving a phino release tag, which does not happen in practice, and it added one more file to bump on every upgrade.

yegor256 merged commit 97df5aa into master Sep 23, 2026
12 checks passed

yegor256 mentioned this pull request Sep 23, 2026

fix(#74): strip phino's xi-free condition in gen-rules.py #75

Merged


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

		def rterm(x):

Conversation

yegor256 commented Jun 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

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!

Favixx left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

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!

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!

yegor256 commented Sep 23, 2026

Uh oh!

yegor256 commented Sep 23, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

yegor256 commented Jun 4, 2026 •

edited

Loading