From cd8a83fe4c7d31e1a59d62de40ebb6c4f3fc4ae5 Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 15:04:11 +0300 Subject: [PATCH 01/13] feat(rules): derive structured rule data from phino (fidelity lock) 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. --- docs/DESIGN.md | 13 ++ docs/RULES-AS-DATA.md | 324 +++++++++++++++++++++++++++++++++++++++ scripts/gen-rule-data.py | 211 +++++++++++++++++++++++++ 3 files changed, 548 insertions(+) create mode 100644 docs/RULES-AS-DATA.md create mode 100644 scripts/gen-rule-data.py diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 9ac385c9..3cf89366 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -311,3 +311,16 @@ Mechanically generating the Lean `Step` *relation* (not just the display table) YAML, so the proof object and the paper's figure share a single source. Today `Step` is hand-written and pinned to phino behaviorally by `difftest`; this would make the pin structural. Optional — it does not affect the proof's validity. + +**M5 — rules as checked data (proposed; `docs/RULES-AS-DATA.md`).** A concrete, partial +realization of the above. `scripts/gen-rule-data.py` (implemented, tested) emits the eleven +root rules as **structured** `RuleSpec` data — typed redex shape, side-conditions, and +contractum — under a *fidelity lock* that aborts if phino's YAML drifts from the locked +interpretation. A hand-written interpreter `RuleSpec.applies` gives that data a semantics, and +`conformance : RootStep e e' ↔ ∃ r ∈ normalizationRuleData, r.applies e e'` makes the pin +**kernel-checked** for the root fragment (`RootStep` = `Step` minus the four congruence +constructors). This shrinks the trusted, hand-written surface from "eleven `Step` +constructors" to "one interpreter + the semantic helpers `contextualize`/`nf`/`fill`/ +`voidAtOrdinal`" — which is the floor, since phino defines those in Haskell, not in the YAML. +Fully data-driving `Step` itself (defining it *as* the interpreter over the list, and redoing +the confluence proof against that) remains the larger, unforced step. diff --git a/docs/RULES-AS-DATA.md b/docs/RULES-AS-DATA.md new file mode 100644 index 00000000..a472ba1d --- /dev/null +++ b/docs/RULES-AS-DATA.md @@ -0,0 +1,324 @@ + + +# Rules as checked data — pinning `Step` to phino (M5, proposed) + +**Status.** The deriver (`scripts/gen-rule-data.py`) is implemented and tested. +The Lean layer below is a **reviewed draft**: it was written without a local Lean +toolchain, so the *definitions and the theorem statement* are the contract, and the +*proofs* are mechanical case-bashes that still need to be compiled and nudged into +shape. Nothing here is imported into `PhiConfluence.lean` yet, so the green build and +the `[propext, Quot.sound]` axiom gate are untouched until this is compiled and wired +in (see "Wiring", below). + +## Why this exists, and what it does (and does not) buy + +Today the eleven rules live in the repo **twice**: once as the hand-written `Step` +relation (the object the confluence theorem is about) and once as +`normalizationRules : List RuleSpec` in `Rules.lean` — display strings generated from +phino, with **no kernel-checked link** to `Step`. So "our `Step` matches phino" rests +on a human reading both plus `difftest` (which compares only one strategy's normal +forms on a curated corpus). That is the faithfulness gap. + +This milestone closes the gap *mechanically* for the **root rules**: + +``` +phino YAML ──gen-rule-data.py (fidelity lock)──▶ normalizationRuleData : List RuleSpec + │ + RuleSpec.applies │ (hand-written interpreter) + ▼ + RootStep ◀───── conformance : RootStep e e' ↔ ∃ r ∈ normalizationRuleData, r.applies e e' + │ (kernel-checked) + │ rootStep_to_step + ▼ + Step = RootStep + the four congruence constructors (the compatible closure; + phino has no congruence rules — "rules apply anywhere") +``` + +If phino changes a rule, one of two things breaks the build: + +* the change alters the rendered pattern/result/condition → the deriver's **fidelity + lock aborts** (`scripts/gen-rule-data.py` raises; CI red); or +* the change is absorbed into the regenerated `normalizationRuleData` tags but no + longer matches `RootStep` → **`conformance` fails to type-check**. + +**What it does not buy.** phino's rule *semantics* live in its Haskell — `contextualize`, +`isNF`/`nf`, the domain ordinal `voidAtOrdinal`, `fill` — and are only *named* in the +YAML (e.g. `dot`'s `where: 𝑒2 := contextualize(𝑒1, …)`). Those functions are still +hand-written in Lean (`Context.lean`, `Nf.lean`, `Attributes.lean`) and **trusted** to +match phino regardless of any codegen. So this does not make `Step` "derived from +phino" in the strong sense; it makes the *rule structure* (which redex shape, which +side-conditions, which contractum, per rule) generated data that is **kernel-checked +against `Step`**, while the semantic vocabulary remains a small, explicit trusted +surface. That is the honest ceiling of mechanization while phino is the reference and +its semantics are not themselves formalized. + +## ξ-free: data vs display (a bug this surfaced) + +`gen-rules.py` claims to strip `copy`'s `ξ`-free guard "so `copy` shows `nf(𝑒1)` only", +but the committed `Rules.lean` still reads `cond := "xi-free(𝑒) and nf(𝑒)"`: the strip +`if k == "xi"` never fires because phino's key is `xi-free`. The clean resolution is the +data/display split this milestone introduces: + +* **Data** (`gen-rule-data.py`, this layer) **keeps** `ξ`-free — because `Step.copy` + carries `xiFree e₁`, so the conformance theorem *needs* it. +* **Display** (`gen-rules.py`) may strip `ξ` for paper-figure parity — a rendering + choice, not a semantic one. + +So `gen-rules.py`'s `if k == "xi"` should be `if k == "xi-free"` (display intent), and +`gen-rule-data.py` deliberately does **not** strip it (proof intent). Filed as a +separate small fix; tracked here so the two generators do not silently disagree. + +## The Lean layer (draft — compile before relying on) + +### `PhiConfluence/RuleSchema.lean` (hand-written: schema + interpreter) + +```lean +-- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com +-- SPDX-License-Identifier: MIT + +import PhiConfluence.Step + +/-! +# Structured rule schema + interpreter + +`RuleSpec` is one normalization rule as interpretable tags (redex shape, side-conditions, +contractum). `RuleSpec.applies r e e'` is its semantics over `Term`, built from the same +primitives `Step` uses (`lookup`, `nf`, `xiFree`, `voidAtOrdinal`, `contextualize`, `fill`). +The generated `normalizationRuleData` (RuleData.lean) is a `List RuleSpec`; `RuleConform` +proves that list equal to the root fragment of `Step`. +-/ + +namespace PhiConfluence + +/-- Which redex a rule fires on: `⊥.a`, `⊥(a↦arg)`, `⟦bs⟧.a`, or `⟦bs⟧(a↦arg)`. -/ +inductive RedexShape where + | dispatchBot | appBot | dispatchForm | appForm + deriving Repr, DecidableEq + +/-- A side condition, read against the redex's `(bs, a, arg)`. -/ +inductive Cond where + | slotVoid | slotAttached | slotAbsent + | attrNeRho | attrIsRho | attrNotAlpha + | phiAbsent | phiPresent | noLambda + | valNf | argXiFree | argNf | alphaVoidOrdinal + deriving Repr, DecidableEq + +/-- The contractum, built from the redex's `(bs, a, arg)`. -/ +inductive Contractum where + | bot | formSame | phiExpand | dotFeedback | copyFill | alphaRename + deriving Repr, DecidableEq + +/-- One rule as data. -/ +structure RuleSpec where + name : String + shape : RedexShape + conds : List Cond + rhs : Contractum + +/-- A side condition as a `Prop` over the redex's formation `bs`, attribute `a`, argument `arg`. -/ +def Cond.holds (bs : List Binding) (a : Attr) (arg : Term) : Cond → Prop + | .slotVoid => lookup bs a = .void + | .slotAttached => ∃ v, lookup bs a = .attached v + | .slotAbsent => lookup bs a = .absent + | .attrNeRho => a ≠ .rho + | .attrIsRho => a = .rho + | .attrNotAlpha => a.isAlpha = false + | .phiAbsent => lookup bs .phi = .absent + | .phiPresent => lookup bs .phi ≠ .absent + | .noLambda => hasLambda bs = false + | .valNf => ∃ v, lookup bs a = .attached v ∧ nf v = true + | .argXiFree => xiFree arg = true + | .argNf => nf arg = true + | .alphaVoidOrdinal => ∃ i τ, a = .alpha i ∧ voidAtOrdinal bs i = some τ + +/-- The contractum as a (partial) `Term`, from the redex's `(bs, a, arg)`. -/ +def Contractum.build (bs : List Binding) (a : Attr) (arg : Term) : Contractum → Option Term + | .bot => some .bot + | .formSame => some (.form bs) + | .phiExpand => some (.dispatch (.dispatch (.form bs) .phi) a) + | .copyFill => some (.form (fill bs a arg)) + | .dotFeedback => + match lookup bs a with + | .attached v => some (.app (contextualize v (.form bs)) .rho (.form bs)) + | _ => none + | .alphaRename => + match a with + | .alpha i => match voidAtOrdinal bs i with + | some τ => some (.app (.form bs) τ arg) + | none => none + | _ => none + +/-- The semantics of a rule: does `e ↝ e'` by rule `r`? -/ +def RuleSpec.applies (r : RuleSpec) (e e' : Term) : Prop := + match r.shape, e with + | .dispatchBot, .dispatch .bot _ => r.conds = [] ∧ r.rhs = .bot ∧ e' = .bot + | .appBot, .app .bot _ _ => r.conds = [] ∧ r.rhs = .bot ∧ e' = .bot + | .dispatchForm, .dispatch (.form bs) a => (∀ c ∈ r.conds, c.holds bs a .bot) ∧ r.rhs.build bs a .bot = some e' + | .appForm, .app (.form bs) a arg => (∀ c ∈ r.conds, c.holds bs a arg) ∧ r.rhs.build bs a arg = some e' + | _, _ => False + +end PhiConfluence +``` + +### `PhiConfluence/RuleData.lean` (GENERATED by `gen-rule-data.py`) + +This is exactly what the (tested) deriver emits today; commit it via +`python3 scripts/gen-rule-data.py /resources PhiConfluence/RuleData.lean`: + +```lean +-- AUTO-GENERATED by scripts/gen-rule-data.py from objectionary/phino resources/*.yaml. +import PhiConfluence.RuleSchema +namespace PhiConfluence + +/-- The φ-calculus normalization rules as structured, interpretable data. -/ +def normalizationRuleData : List RuleSpec := + [ { name := "alpha", shape := .appForm, conds := [.alphaVoidOrdinal], rhs := .alphaRename } + , { name := "copy", shape := .appForm, conds := [.slotVoid, .argXiFree, .argNf], rhs := .copyFill } + , { name := "dc", shape := .appBot, conds := [], rhs := .bot } + , { name := "dd", shape := .dispatchBot, conds := [], rhs := .bot } + , { name := "dot", shape := .dispatchForm, conds := [.slotAttached, .valNf], rhs := .dotFeedback } + , { name := "miss", shape := .appForm, conds := [.slotAbsent, .attrNotAlpha], rhs := .bot } + , { name := "null", shape := .dispatchForm, conds := [.slotVoid], rhs := .bot } + , { name := "over", shape := .appForm, conds := [.slotAttached, .attrNeRho], rhs := .bot } + , { name := "phi", shape := .dispatchForm, conds := [.phiPresent, .slotAbsent], rhs := .phiExpand } + , { name := "stay", shape := .appForm, conds := [.attrIsRho, .slotAttached], rhs := .formSame } + , { name := "stop", shape := .dispatchForm, conds := [.slotAbsent, .phiAbsent, .noLambda], rhs := .bot } ] + +end PhiConfluence +``` + +### `PhiConfluence/RuleConform.lean` (hand-written: the pin) + +```lean +-- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com +-- SPDX-License-Identifier: MIT + +import PhiConfluence.RuleData + +/-! +# Conformance: the generated rule data is exactly `Step`'s root fragment + +`RootStep` is `Step` minus the four congruence constructors (phino has no congruence +rules; the closure is the project's own). `conformance` pins the phino-derived +`normalizationRuleData` to `RootStep`, and `rootStep_to_step` ties `RootStep` back into +the relation the confluence theorem governs. +-/ + +namespace PhiConfluence + +/-- The eleven root rules of `Step`, without the congruence closure. -/ +inductive RootStep : Term → Term → Prop where + | dd (a : Attr) : RootStep (.dispatch .bot a) .bot + | dc (a : Attr) (e : Term) : RootStep (.app .bot a e) .bot + | null {bs a} : lookup bs a = .void → RootStep (.dispatch (.form bs) a) .bot + | over {bs a e₁ e₂} : lookup bs a = .attached e₁ → a ≠ .rho → RootStep (.app (.form bs) a e₂) .bot + | stop {bs a} : lookup bs a = .absent → lookup bs .phi = .absent → hasLambda bs = false → + RootStep (.dispatch (.form bs) a) .bot + | miss {bs a e} : lookup bs a = .absent → a.isAlpha = false → RootStep (.app (.form bs) a e) .bot + | stay {bs e₁ e₂} : lookup bs .rho = .attached e₁ → RootStep (.app (.form bs) .rho e₂) (.form bs) + | phi {bs a} : lookup bs .phi ≠ .absent → lookup bs a = .absent → + RootStep (.dispatch (.form bs) a) (.dispatch (.dispatch (.form bs) .phi) a) + | alpha {bs i τ₁ e} : voidAtOrdinal bs i = some τ₁ → + RootStep (.app (.form bs) (.alpha i) e) (.app (.form bs) τ₁ e) + | dot {bs a e₁} : lookup bs a = .attached e₁ → nf e₁ = true → + RootStep (.dispatch (.form bs) a) (.app (contextualize e₁ (.form bs)) .rho (.form bs)) + | copy {bs a e₁} : lookup bs a = .void → xiFree e₁ = true → nf e₁ = true → + RootStep (.app (.form bs) a e₁) (.form (fill bs a e₁)) + +/-- Every root step is a `Step` (each constructor maps to the same-named `Step` rule). -/ +theorem rootStep_to_step {e e' : Term} (h : RootStep e e') : Step e e' := by + cases h with + | dd a => exact .dd a + | dc a e => exact .dc a e + | null h => exact .null h + | over h1 h2 => exact .over h1 h2 + | stop h1 h2 h3 => exact .stop h1 h2 h3 + | miss h1 h2 => exact .miss h1 h2 + | stay h => exact .stay h + | phi h1 h2 => exact .phi h1 h2 + | alpha h => exact .alpha h + | dot h1 h2 => exact .dot h1 h2 + | copy h1 h2 h3 => exact .copy h1 h2 h3 + +/-- **The pin.** The phino-derived rule data denotes exactly `RootStep`. A phino change +that survives the deriver but alters a rule's meaning breaks this theorem. -/ +theorem conformance {e e' : Term} : + RootStep e e' ↔ ∃ r ∈ normalizationRuleData, r.applies e e' := by + constructor + · intro h + -- forward: each RootStep constructor exhibits its generated entry as the witness. + cases h with + | dd a => exact ⟨_, by simp [normalizationRuleData], by simp [RuleSpec.applies]⟩ + | dc a e => exact ⟨_, by simp [normalizationRuleData], by simp [RuleSpec.applies]⟩ + | null h => + exact ⟨_, by simp [normalizationRuleData], + by simp [RuleSpec.applies, Cond.holds, Contractum.build, h]⟩ + | over h1 h2 => + exact ⟨_, by simp [normalizationRuleData], + by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2]⟩ + | stop h1 h2 h3 => + exact ⟨_, by simp [normalizationRuleData], + by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2, h3]⟩ + | miss h1 h2 => + exact ⟨_, by simp [normalizationRuleData], + by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2]⟩ + | stay h => + exact ⟨_, by simp [normalizationRuleData], + by simp [RuleSpec.applies, Cond.holds, Contractum.build, h]⟩ + | phi h1 h2 => + exact ⟨_, by simp [normalizationRuleData], + by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2]⟩ + | alpha h => + exact ⟨_, by simp [normalizationRuleData], + by simp [RuleSpec.applies, Cond.holds, Contractum.build, h]⟩ + | dot h1 h2 => + exact ⟨_, by simp [normalizationRuleData], + by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2]⟩ + | copy h1 h2 h3 => + exact ⟨_, by simp [normalizationRuleData], + by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2, h3]⟩ + · rintro ⟨r, hr, ha⟩ + -- backward: enumerate the 11 entries; each `applies` reconstructs its RootStep rule. + -- `fin_cases hr` splits the list; `RuleSpec.applies` then forces the redex shape and, + -- via `Cond.holds`/`Contractum.build`, the side-conditions and contractum. + fin_cases hr <;> + first + | (obtain ⟨hc, hb⟩ := ha; · skip) -- PUZZLE: per-entry, destructure conds/build then + -- `cases e` to expose the redex and apply the + -- matching `RootStep` constructor. See notes below. + | skip + +end PhiConfluence +``` + +The backward direction is the one genuine puzzle: after `fin_cases hr` each goal has a +concrete `r` and `ha : r.applies e e'`; `simp [RuleSpec.applies] at ha` forces `e` into +the rule's redex shape (`dispatch (form bs) a` etc.), `Cond.holds` turns the condition +list into the rule's hypotheses, `Contractum.build … = some e'` pins `e'`, and the +matching `RootStep.` closes it. It is mechanical but verbose; left as a +**Puzzle** to complete against the compiler rather than guess blind here. + +## Wiring (once compiled green) + +1. Add `RuleSchema.lean`; `python3 scripts/gen-rule-data.py /resources + PhiConfluence/RuleData.lean`; add `RuleConform.lean`. Compile and finish the one + backward-direction puzzle. +2. Add the three modules to `PhiConfluence.lean`'s import list. +3. Add a CI job mirroring `rules-in-sync` for the data file + (`gen-rule-data.py` → `git diff --exit-code PhiConfluence/RuleData.lean`); the + deriver's fidelity lock means a phino change fails the regen step itself. +4. Add `PhiConfluence.conformance` and `PhiConfluence.rootStep_to_step` to the + `#print axioms` gate in `build.yml` (expect `[propext, Quot.sound]` or cleaner). +5. Fix the display generator's `ξ` strip (`gen-rules.py`: `"xi"` → `"xi-free"`). + +## Puzzles left + +* **§M5-a** Complete the backward direction of `conformance` (see above). +* **§M5-b** Optional: extend the pin from `RootStep` to a statement about `Step` + directly — e.g. prove `Step` is the compatible closure of `RootStep`, so the + congruence constructors are visibly *not* phino-derived but the standard closure. +* **§M5-c** `λ`/`Δ` assets: the deriver has no rule for them by design (phino has + none); if asset reduction is ever modelled, both the lock and the schema extend. diff --git a/scripts/gen-rule-data.py b/scripts/gen-rule-data.py new file mode 100644 index 00000000..f6833a1b --- /dev/null +++ b/scripts/gen-rule-data.py @@ -0,0 +1,211 @@ +#!/usr/bin/env python3 +# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com +# SPDX-License-Identifier: MIT +""" +Generate PhiConfluence/RuleData.lean from phino's resources/*.yaml. + +Unlike `gen-rules.py` (which emits *display strings* for the demo), this emits the +**structured** rule data the proof is pinned against: each rule becomes a `RuleSpec` +of typed tags (redex shape, side-conditions, contractum) that the hand-written +interpreter `applies` (PhiConfluence/RuleSchema.lean) gives a semantics to, and that +`conformance` (PhiConfluence/RuleConform.lean) proves equal to the `Step` relation. +So if phino changes a rule, the regenerated data changes and the Lean conformance +theorem stops type-checking — drift between phino and the proof becomes a build error. + +DESIGN — a *fidelity lock*, not a general translator. + phino's rule semantics live in its Haskell (`contextualize`, `isNF`, ordinals …), + not in the YAML, so the YAML cannot be mechanically translated into a Lean relation + (see docs/RULES-AS-DATA.md). Instead this script carries one *locked interpretation* + per rule (the structured tags below) and ASSERTS that phino's current YAML still + renders to the pattern/result/condition this interpretation assumes — failing loudly + on any mismatch. The locked tags are emitted; the proof checks them against `Step`. + Net: phino-drift trips the assertion here (CI red); a tags-vs-`Step` mismatch trips + the Lean conformance theorem. Both ends are pinned. + +This re-uses `gen-rules.py`'s exact `when`/`where` rendering so the asserted condition +strings are identical to the display table's — one rendering, two consumers. + +Usage: + gen-rule-data.py +""" +import sys, os, glob, re +import yaml + + +# --- condition/where rendering: identical to gen-rules.py (kept in sync on purpose) --- + +def rterm(x): + return str(x) + + +def rcmp(x): + if isinstance(x, dict): + k = next(iter(x)); v = x[k] + if k == "index": + return f"index({rterm(v)})" + if k == "length": + return f"|{rterm(v)}|" + if k == "domain": + return f"domain({rterm(v)})" + return f"{k}({rterm(v)})" + return rterm(x) + + +def rcond(w): + if w is None: + return "" + if not isinstance(w, dict): + return rterm(w) + k = next(iter(w)); v = w[k] + if k == "and": + return " and ".join(p for p in (rcond(x) for x in v) if p) + if k == "or": + return " or ".join(p for p in (rcond(x) for x in v) if p) + if k == "not": + return "¬(" + rcond(v) + ")" + if k == "in": + return f"{rterm(v[0])} ∈ {rterm(v[1])}" + if k == "nf": + return f"nf({rterm(v)})" + if k == "alpha": + return f"α-attr({rterm(v)})" + if k == "eq": + return f"{rcmp(v[0])} = {rcmp(v[1])}" + return f"{k}({rterm(v)})" + + +def rwhere(ws): + parts = [] + for w in ws or []: + meta = w.get("meta"); fn = w.get("function"); args = w.get("args", []) + parts.append(f"{meta} := {fn}({', '.join(rterm(a) for a in args)})") + return " and ".join(parts) + + +def norm(s): + """Whitespace-insensitive comparison key (phino's pattern strings have stray spaces).""" + return re.sub(r"\s+", " ", s or "").strip() + + +# --- the locked interpretation: one entry per phino rule ------------------------------- +# +# Each entry asserts phino's rendered (pattern, result, cond, where) and, on a match, +# contributes the structured Lean tags. `shape`/`conds`/`rhs` are Lean `RuleSpec` field +# expressions; they MUST stay in step with PhiConfluence/RuleSchema.lean's inductives. +# `expect` strings are phino's current YAML as rendered above (== the gen-rules.py table). +# +# If phino's YAML drifts from `expect`, this script aborts (see `check`) — that is the +# point. If the *interpretation* (tags) is what changed, the Lean `conformance` theorem +# is what fails. Adding/removing a phino rule trips the name-set assertion in `main`. + +LOCK = { + "dd": dict( + expect=("⊥.𝜏", "⊥", "", ""), + shape=".dispatchBot", conds="[]", rhs=".bot"), + "dc": dict( + expect=("⊥(𝜏 ↦ 𝑒)", "⊥", "", ""), + shape=".appBot", conds="[]", rhs=".bot"), + "null": dict( + expect=("⟦𝐵1, 𝜏 ↦ ∅, 𝐵2⟧.𝜏", "⊥", "", ""), + shape=".dispatchForm", conds="[.slotVoid]", rhs=".bot"), + "over": dict( + expect=("⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧(𝜏 ↦ 𝑒2)", "⊥", "¬(𝜏 = ρ)", ""), + shape=".appForm", conds="[.slotAttached, .attrNeRho]", rhs=".bot"), + "stop": dict( + expect=("⟦𝐵⟧.𝜏", "⊥", "¬(𝜏 ∈ 𝐵) and ¬(φ ∈ 𝐵) and ¬(λ ∈ 𝐵)", ""), + shape=".dispatchForm", conds="[.slotAbsent, .phiAbsent, .noLambda]", rhs=".bot"), + "miss": dict( + expect=("⟦𝐵⟧(𝜏 ↦ 𝑒)", "⊥", "¬(𝜏 ∈ 𝐵) and ¬(α-attr(𝜏))", ""), + shape=".appForm", conds="[.slotAbsent, .attrNotAlpha]", rhs=".bot"), + "stay": dict( + expect=("⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧(ρ ↦ 𝑒2)", "⟦𝐵1, ρ ↦ 𝑒1, 𝐵2⟧", "", ""), + shape=".appForm", conds="[.attrIsRho, .slotAttached]", rhs=".formSame"), + "phi": dict( + expect=("⟦𝐵⟧.𝜏", "⟦𝐵⟧.φ.𝜏", "φ ∈ 𝐵 and ¬(𝜏 ∈ 𝐵)", ""), + shape=".dispatchForm", conds="[.phiPresent, .slotAbsent]", rhs=".phiExpand"), + "alpha": dict( + expect=("⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏2 ↦ 𝑒)", "⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒)", + "index(𝜏2) = domain(𝐵1)", ""), + shape=".appForm", conds="[.alphaVoidOrdinal]", rhs=".alphaRename"), + "dot": dict( + expect=("⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧.𝜏", "𝑒2(ρ ↦ ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧)", "nf(𝑒1)", + "𝑒2 := contextualize(𝑒1, ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧)"), + shape=".dispatchForm", conds="[.slotAttached, .valNf]", rhs=".dotFeedback"), + # NOTE — copy keeps phino's `xi-free` guard in the DATA (Step.copy carries `xiFree`); + # only the DISPLAY table (gen-rules.py) strips ξ for paper-figure parity. See + # docs/RULES-AS-DATA.md "ξ-free: data vs display". + "copy": dict( + expect=("⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒)", "⟦ 𝐵1, 𝜏 ↦ 𝑒, 𝐵2 ⟧", + "xi-free(𝑒) and nf(𝑒)", ""), + shape=".appForm", conds="[.slotVoid, .argXiFree, .argNf]", rhs=".copyFill"), +} + + +def check(name, got, want): + g = tuple(norm(x) for x in got) + w = tuple(norm(x) for x in want) + if g != w: + raise SystemExit( + 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`.") + + +def main(): + res_dir, out = sys.argv[1], sys.argv[2] + found = {} + for path in sorted(glob.glob(os.path.join(res_dir, "*.yaml"))): + with open(path, encoding="utf-8") as f: + d = yaml.safe_load(f) + name = str(d["name"]) + got = (str(d["pattern"]), str(d["result"]), rcond(d.get("when")), rwhere(d.get("where"))) + if name not in LOCK: + raise SystemExit(f"phino has an UNLOCKED rule '{name}' — add it to LOCK and to Step/conformance") + check(name, got, LOCK[name]["expect"]) + found[name] = LOCK[name] + missing = set(LOCK) - set(found) + if missing: + raise SystemExit(f"locked rules absent from phino's resources: {sorted(missing)}") + lines = [ + # REUSE-IgnoreStart + "-- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com", + "-- SPDX-License-Identifier: MIT", + # REUSE-IgnoreEnd + "", + "-- AUTO-GENERATED by scripts/gen-rule-data.py from objectionary/phino resources/*.yaml.", + "-- DO NOT EDIT BY HAND. Regenerate after phino's rules change.", + "", + "import PhiConfluence.RuleSchema", + "", + "/-!", + "# Normalization rules as structured data, generated from phino", + "", + "The eleven rules as `RuleSpec` tags, emitted by the fidelity-lock deriver", + "`scripts/gen-rule-data.py`. `PhiConfluence.RuleConform.conformance` proves this list", + "equal to the `Step` relation, so a phino change that survives the deriver's assertions", + "but alters a rule's meaning makes that theorem fail to compile.", + "-/", + "", + "namespace PhiConfluence", + "", + "/-- The φ-calculus normalization rules as structured, interpretable data. -/", + "def normalizationRuleData : List RuleSpec :=", + ] + entries = [] + for name in sorted(found): + e = found[name] + entries.append( + ' { name := "%s", shape := %s, conds := %s, rhs := %s }' + % (name, e["shape"], e["conds"], e["rhs"])) + lines.append(" [ " + "\n , ".join(x.strip() for x in entries) + " ]") + lines.append("") + lines.append("end PhiConfluence") + lines.append("") + with open(out, "w", encoding="utf-8") as f: + f.write("\n".join(lines)) + print(f"wrote {out} with {len(found)} rules (fidelity lock held)") + + +if __name__ == "__main__": + main() From 46ade3db76ad9c7a217e3ddbe5ba1825d8ff76c9 Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 15:36:14 +0300 Subject: [PATCH 02/13] ci: add ruff workflow to lint Python scripts 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. --- .github/workflows/ruff.yml | 18 ++++++++++++++++++ scripts/gen-rule-data.py | 16 ++++++++++++---- scripts/gen-rules.py | 15 +++++++++++---- 3 files changed, 41 insertions(+), 8 deletions(-) create mode 100644 .github/workflows/ruff.yml diff --git a/.github/workflows/ruff.yml b/.github/workflows/ruff.yml new file mode 100644 index 00000000..60b99290 --- /dev/null +++ b/.github/workflows/ruff.yml @@ -0,0 +1,18 @@ +# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com +# SPDX-License-Identifier: MIT +--- +name: ruff +'on': + push: + branches: + - master + pull_request: + branches: + - master +jobs: + ruff: + timeout-minutes: 15 + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@v4 + - uses: astral-sh/ruff-action@v3 diff --git a/scripts/gen-rule-data.py b/scripts/gen-rule-data.py index f6833a1b..b15b3c1f 100644 --- a/scripts/gen-rule-data.py +++ b/scripts/gen-rule-data.py @@ -28,7 +28,11 @@ Usage: gen-rule-data.py """ -import sys, os, glob, re +import glob +import os +import re +import sys + import yaml @@ -40,7 +44,8 @@ def rterm(x): def rcmp(x): if isinstance(x, dict): - k = next(iter(x)); v = x[k] + k = next(iter(x)) + v = x[k] if k == "index": return f"index({rterm(v)})" if k == "length": @@ -56,7 +61,8 @@ def rcond(w): return "" if not isinstance(w, dict): return rterm(w) - k = next(iter(w)); v = w[k] + k = next(iter(w)) + v = w[k] if k == "and": return " and ".join(p for p in (rcond(x) for x in v) if p) if k == "or": @@ -77,7 +83,9 @@ def rcond(w): def rwhere(ws): parts = [] for w in ws or []: - meta = w.get("meta"); fn = w.get("function"); args = w.get("args", []) + meta = w.get("meta") + fn = w.get("function") + args = w.get("args", []) parts.append(f"{meta} := {fn}({', '.join(rterm(a) for a in args)})") return " and ".join(parts) diff --git a/scripts/gen-rules.py b/scripts/gen-rules.py index ddae3fc9..73358e73 100644 --- a/scripts/gen-rules.py +++ b/scripts/gen-rules.py @@ -18,7 +18,10 @@ Usage: gen-rules.py """ -import sys, os, glob +import glob +import os +import sys + import yaml @@ -28,7 +31,8 @@ def rterm(x): def rcmp(x): if isinstance(x, dict): - k = next(iter(x)); v = x[k] + k = next(iter(x)) + v = x[k] if k == "index": return f"index({rterm(v)})" if k == "length": @@ -42,7 +46,8 @@ def rcond(w): return "" if not isinstance(w, dict): return rterm(w) - k = next(iter(w)); v = w[k] + k = next(iter(w)) + v = w[k] if k == "and": return " and ".join(p for p in (rcond(x) for x in v) if p) if k == "or": @@ -65,7 +70,9 @@ def rcond(w): def rwhere(ws): parts = [] for w in ws or []: - meta = w.get("meta"); fn = w.get("function"); args = w.get("args", []) + meta = w.get("meta") + fn = w.get("function") + args = w.get("args", []) parts.append(f"{meta} := {fn}({', '.join(rterm(a) for a in args)})") return " and ".join(parts) From 74b06a1910efebd995c0e49872a04a70ca869aaa Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 15:51:47 +0300 Subject: [PATCH 03/13] Potential fix for pull request finding Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- scripts/gen-rule-data.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/gen-rule-data.py b/scripts/gen-rule-data.py index b15b3c1f..a6708feb 100644 --- a/scripts/gen-rule-data.py +++ b/scripts/gen-rule-data.py @@ -22,8 +22,8 @@ Net: phino-drift trips the assertion here (CI red); a tags-vs-`Step` mismatch trips the Lean conformance theorem. Both ends are pinned. -This re-uses `gen-rules.py`'s exact `when`/`where` rendering so the asserted condition -strings are identical to the display table's — one rendering, two consumers. +This intentionally duplicates `gen-rules.py`'s `when`/`where` rendering (keep in sync) so +the asserted condition strings match the display table's — one rendering, two consumers. Usage: gen-rule-data.py From edb5aa11cbefa69c0988e2aa97609f866b79f062 Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 15:51:59 +0300 Subject: [PATCH 04/13] Potential fix for pull request finding Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- scripts/gen-rule-data.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/gen-rule-data.py b/scripts/gen-rule-data.py index a6708feb..e258117a 100644 --- a/scripts/gen-rule-data.py +++ b/scripts/gen-rule-data.py @@ -161,6 +161,8 @@ def check(name, got, want): def main(): + if len(sys.argv) != 3: + raise SystemExit("Usage: gen-rule-data.py ") res_dir, out = sys.argv[1], sys.argv[2] found = {} for path in sorted(glob.glob(os.path.join(res_dir, "*.yaml"))): From 9fe9659df32ee2036a2ee3cdf5f8c3d907ba3fb4 Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 15:52:09 +0300 Subject: [PATCH 05/13] Potential fix for pull request finding Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- scripts/gen-rule-data.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/scripts/gen-rule-data.py b/scripts/gen-rule-data.py index e258117a..fde7e0fa 100644 --- a/scripts/gen-rule-data.py +++ b/scripts/gen-rule-data.py @@ -169,6 +169,8 @@ def main(): with open(path, encoding="utf-8") as f: d = yaml.safe_load(f) 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"))) if name not in LOCK: raise SystemExit(f"phino has an UNLOCKED rule '{name}' — add it to LOCK and to Step/conformance") From 9e775bd5dcdcda347143d9e9ed4c1ac5975f912b Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 15:52:16 +0300 Subject: [PATCH 06/13] Potential fix for pull request finding Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- docs/RULES-AS-DATA.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/RULES-AS-DATA.md b/docs/RULES-AS-DATA.md index a472ba1d..aadd2108 100644 --- a/docs/RULES-AS-DATA.md +++ b/docs/RULES-AS-DATA.md @@ -5,7 +5,7 @@ SPDX-License-Identifier: MIT # Rules as checked data — pinning `Step` to phino (M5, proposed) -**Status.** The deriver (`scripts/gen-rule-data.py`) is implemented and tested. +**Status.** The deriver (`scripts/gen-rule-data.py`) is implemented; wiring it into CI is described below. The Lean layer below is a **reviewed draft**: it was written without a local Lean toolchain, so the *definitions and the theorem statement* are the contract, and the *proofs* are mechanical case-bashes that still need to be compiled and nudged into From dd7688fa82768a4532df0abaf7e76949ec8e49ed Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 15:52:24 +0300 Subject: [PATCH 07/13] Potential fix for pull request finding Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- docs/DESIGN.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 3cf89366..2816c013 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -313,7 +313,7 @@ hand-written and pinned to phino behaviorally by `difftest`; this would make the structural. Optional — it does not affect the proof's validity. **M5 — rules as checked data (proposed; `docs/RULES-AS-DATA.md`).** A concrete, partial -realization of the above. `scripts/gen-rule-data.py` (implemented, tested) emits the eleven +realization of the above. `scripts/gen-rule-data.py` (implemented) emits the eleven root rules as **structured** `RuleSpec` data — typed redex shape, side-conditions, and contractum — under a *fidelity lock* that aborts if phino's YAML drifts from the locked interpretation. A hand-written interpreter `RuleSpec.applies` gives that data a semantics, and From ea8c98fffd1c06c8856d798f47b9f7a8b2f51508 Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 16:59:43 +0300 Subject: [PATCH 08/13] build(phino): pin to 0.0.0.74 via .phino-version MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- .github/workflows/difftest.yml | 5 +++-- .phino-version | 1 + REUSE.toml | 1 + scripts/confluence-probe.sh | 9 +++++---- scripts/difftest.sh | 6 ++++-- scripts/regen-rules.sh | 14 ++++++++------ 6 files changed, 22 insertions(+), 14 deletions(-) create mode 100644 .phino-version diff --git a/.github/workflows/difftest.yml b/.github/workflows/difftest.yml index defc60c1..cfb47762 100644 --- a/.github/workflows/difftest.yml +++ b/.github/workflows/difftest.yml @@ -16,9 +16,10 @@ jobs: runs-on: ubuntu-24.04 steps: - uses: actions/checkout@v4 - - name: Install phino (latest) + - name: Install phino (pinned via .phino-version) 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" sudo chmod +x /usr/local/bin/phino phino --version - uses: ./.github/actions/setup-lean diff --git a/.phino-version b/.phino-version new file mode 100644 index 00000000..4b9517ee --- /dev/null +++ b/.phino-version @@ -0,0 +1 @@ +0.0.0.74 diff --git a/REUSE.toml b/REUSE.toml index 0355a763..54ef9512 100644 --- a/REUSE.toml +++ b/REUSE.toml @@ -5,6 +5,7 @@ version = 1 [[annotations]] path = [ ".gitignore", + ".phino-version", ".yamllint", "**.json", "**.md", diff --git a/scripts/confluence-probe.sh b/scripts/confluence-probe.sh index a5fc6903..7c792404 100755 --- a/scripts/confluence-probe.sh +++ b/scripts/confluence-probe.sh @@ -31,6 +31,7 @@ cd "$(dirname "$0")/.." ITERS="${ITERS:-24}" command -v phino >/dev/null 2>&1 || { echo "phino not on PATH; skipping" >&2; exit 0; } +PHINO_VERSION="$(cat .phino-version)" RESOURCES="${PHINO_RESOURCES:-}" if [ -z "$RESOURCES" ]; then @@ -50,7 +51,7 @@ total=0 # Normal form of a file, or the sentinel / for an unfinished/failed run. norm() { local out ec - out=$($TO phino rewrite --normalize --depth-sensitive --flat "$1" 2>&1); ec=$? + out=$($TO phino rewrite --pin="$PHINO_VERSION" --normalize --depth-sensitive --flat "$1" 2>&1); ec=$? if [ "$ec" = 124 ]; then echo "" elif [ "$ec" = 0 ]; then echo "$out" elif printf '%s' "$out" | grep -q 'depth-sensitive'; then echo "" @@ -71,16 +72,16 @@ probe() { local i s ec for ((i = 1; i <= ITERS; i++)); do - s=$($TO phino rewrite --normalize --shuffle --depth-sensitive --flat "$file" 2>&1); ec=$? + s=$($TO phino rewrite --pin="$PHINO_VERSION" --normalize --shuffle --depth-sensitive --flat "$file" 2>&1); ec=$? [ "$ec" = 0 ] && [ -n "$s" ] && samples+=("shuffle $s") done - local canon; canon=$($TO phino rewrite --flat "$file" 2>&1) + local canon; canon=$($TO phino rewrite --pin="$PHINO_VERSION" --flat "$file" 2>&1) local rule forced nfr tmp tmp="$(mktemp)" for rule in $RULES; do [ -f "$RESOURCES/$rule.yaml" ] || continue - forced=$($TO phino rewrite --rule "$RESOURCES/$rule.yaml" --max-depth 1 --max-cycles 1 --flat "$file" 2>&1) + forced=$($TO phino rewrite --pin="$PHINO_VERSION" --rule "$RESOURCES/$rule.yaml" --max-depth 1 --max-cycles 1 --flat "$file" 2>&1) { [ -z "$forced" ] || [ "$forced" = "$canon" ]; } && continue printf '%s\n' "$forced" > "$tmp" nfr=$(norm "$tmp") diff --git a/scripts/difftest.sh b/scripts/difftest.sh index 7cc00a16..c9411144 100755 --- a/scripts/difftest.sh +++ b/scripts/difftest.sh @@ -4,11 +4,13 @@ # # Differential test: for each example program, check that phino's normal form # (`phino rewrite --normalize`) equals our reducer's normal form. The behavioral -# pin between this prover's Step relation and phino. Requires `phino` on PATH. +# pin between this prover's Step relation and phino. Requires `phino` on PATH, +# pinned via `--pin` to the version in .phino-version (phino aborts on a mismatch). set -uo pipefail cd "$(dirname "$0")/.." export PATH="$HOME/.elan/bin:$PATH" +PHINO_VERSION="$(cat .phino-version)" if ! command -v phino >/dev/null 2>&1; then echo "FATAL: phino not found on PATH; the differential test requires it (fail-fast, not skip)" >&2 @@ -22,7 +24,7 @@ count=0 while IFS=$'\t' read -r input expected; do [ -z "${input:-}" ] && continue count=$((count + 1)) - out=$(printf '%s\n' "$input" | phino rewrite --normalize --flat 2>/dev/null) + out=$(printf '%s\n' "$input" | phino rewrite --normalize --pin="$PHINO_VERSION" --flat 2>/dev/null) pn=$(printf '%s' "$out" | tr -d '[:space:]'); pn=${pn#Φ↦} ours=$(printf '%s' "$expected" | tr -d '[:space:]') if [ "$pn" = "$ours" ]; then diff --git a/scripts/regen-rules.sh b/scripts/regen-rules.sh index 4200faf4..682291d5 100755 --- a/scripts/regen-rules.sh +++ b/scripts/regen-rules.sh @@ -2,9 +2,10 @@ # SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com # SPDX-License-Identifier: MIT # -# Regenerate PhiConfluence/Rules.lean from the LATEST phino rules on GitHub -# (objectionary/phino master). The rule source is phino's repo — the same source the -# paper's Fig. 4 is generated from — not any local checkout. +# Regenerate PhiConfluence/Rules.lean from the PINNED phino rules on GitHub +# (objectionary/phino at the tag in .phino-version). The rule source is phino's repo — +# the same source the paper's Fig. 4 is generated from — not any local checkout. Pinning +# keeps regeneration deterministic: tracking master let phino drift break this in CI. # # Usage: bash scripts/regen-rules.sh @@ -12,11 +13,12 @@ set -euo pipefail cd "$(dirname "$0")/.." PHINO_REPO="${PHINO_REPO:-https://github.com/objectionary/phino}" +PHINO_VERSION="$(cat .phino-version)" tmp="$(mktemp -d)" trap 'rm -rf "$tmp"' EXIT -echo "cloning $PHINO_REPO (master = latest) ..." -git clone --depth 1 "$PHINO_REPO" "$tmp/phino" >/dev/null 2>&1 +echo "cloning $PHINO_REPO at $PHINO_VERSION (pinned via .phino-version) ..." +git clone --depth 1 --branch "$PHINO_VERSION" "$PHINO_REPO" "$tmp/phino" >/dev/null 2>&1 python3 scripts/gen-rules.py "$tmp/phino/resources" PhiConfluence/Rules.lean -echo "done — PhiConfluence/Rules.lean regenerated from phino master" +echo "done — PhiConfluence/Rules.lean regenerated from phino $PHINO_VERSION" From d1b19391a37bb6e6483f4a89d5294d55a6056470 Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 17:12:25 +0300 Subject: [PATCH 09/13] fix(phino): clone 3-part git tag, pass --pin before subcommand MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- scripts/confluence-probe.sh | 8 ++++---- scripts/difftest.sh | 2 +- scripts/regen-rules.sh | 7 +++++-- 3 files changed, 10 insertions(+), 7 deletions(-) diff --git a/scripts/confluence-probe.sh b/scripts/confluence-probe.sh index 7c792404..9746f223 100755 --- a/scripts/confluence-probe.sh +++ b/scripts/confluence-probe.sh @@ -51,7 +51,7 @@ total=0 # Normal form of a file, or the sentinel / for an unfinished/failed run. norm() { local out ec - out=$($TO phino rewrite --pin="$PHINO_VERSION" --normalize --depth-sensitive --flat "$1" 2>&1); ec=$? + out=$($TO phino --pin="$PHINO_VERSION" rewrite --normalize --depth-sensitive --flat "$1" 2>&1); ec=$? if [ "$ec" = 124 ]; then echo "" elif [ "$ec" = 0 ]; then echo "$out" elif printf '%s' "$out" | grep -q 'depth-sensitive'; then echo "" @@ -72,16 +72,16 @@ probe() { local i s ec for ((i = 1; i <= ITERS; i++)); do - s=$($TO phino rewrite --pin="$PHINO_VERSION" --normalize --shuffle --depth-sensitive --flat "$file" 2>&1); ec=$? + s=$($TO phino --pin="$PHINO_VERSION" rewrite --normalize --shuffle --depth-sensitive --flat "$file" 2>&1); ec=$? [ "$ec" = 0 ] && [ -n "$s" ] && samples+=("shuffle $s") done - local canon; canon=$($TO phino rewrite --pin="$PHINO_VERSION" --flat "$file" 2>&1) + local canon; canon=$($TO phino --pin="$PHINO_VERSION" rewrite --flat "$file" 2>&1) local rule forced nfr tmp tmp="$(mktemp)" for rule in $RULES; do [ -f "$RESOURCES/$rule.yaml" ] || continue - forced=$($TO phino rewrite --pin="$PHINO_VERSION" --rule "$RESOURCES/$rule.yaml" --max-depth 1 --max-cycles 1 --flat "$file" 2>&1) + forced=$($TO phino --pin="$PHINO_VERSION" rewrite --rule "$RESOURCES/$rule.yaml" --max-depth 1 --max-cycles 1 --flat "$file" 2>&1) { [ -z "$forced" ] || [ "$forced" = "$canon" ]; } && continue printf '%s\n' "$forced" > "$tmp" nfr=$(norm "$tmp") diff --git a/scripts/difftest.sh b/scripts/difftest.sh index c9411144..a7818d36 100755 --- a/scripts/difftest.sh +++ b/scripts/difftest.sh @@ -24,7 +24,7 @@ count=0 while IFS=$'\t' read -r input expected; do [ -z "${input:-}" ] && continue count=$((count + 1)) - out=$(printf '%s\n' "$input" | phino rewrite --normalize --pin="$PHINO_VERSION" --flat 2>/dev/null) + out=$(printf '%s\n' "$input" | phino --pin="$PHINO_VERSION" rewrite --normalize --flat 2>/dev/null) pn=$(printf '%s' "$out" | tr -d '[:space:]'); pn=${pn#Φ↦} ours=$(printf '%s' "$expected" | tr -d '[:space:]') if [ "$pn" = "$ours" ]; then diff --git a/scripts/regen-rules.sh b/scripts/regen-rules.sh index 682291d5..eac72e89 100755 --- a/scripts/regen-rules.sh +++ b/scripts/regen-rules.sh @@ -14,11 +14,14 @@ cd "$(dirname "$0")/.." PHINO_REPO="${PHINO_REPO:-https://github.com/objectionary/phino}" PHINO_VERSION="$(cat .phino-version)" +# phino's package/binary version is 4-part (0.0.0.74 — what --pin and the release +# artifacts use), but its git tags drop the leading component (0.0.74). +PHINO_TAG="${PHINO_VERSION#0.}" tmp="$(mktemp -d)" trap 'rm -rf "$tmp"' EXIT -echo "cloning $PHINO_REPO at $PHINO_VERSION (pinned via .phino-version) ..." -git clone --depth 1 --branch "$PHINO_VERSION" "$PHINO_REPO" "$tmp/phino" >/dev/null 2>&1 +echo "cloning $PHINO_REPO at tag $PHINO_TAG (phino $PHINO_VERSION, pinned via .phino-version) ..." +git clone --depth 1 --branch "$PHINO_TAG" "$PHINO_REPO" "$tmp/phino" >/dev/null 2>&1 python3 scripts/gen-rules.py "$tmp/phino/resources" PhiConfluence/Rules.lean echo "done — PhiConfluence/Rules.lean regenerated from phino $PHINO_VERSION" From 76d9ac96be8b7ff2421941fb26a5271fc3918913 Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 17:24:55 +0300 Subject: [PATCH 10/13] docs: remove the rules-as-data design note 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. --- docs/DESIGN.md | 13 -- docs/RULES-AS-DATA.md | 324 --------------------------------------- scripts/gen-rule-data.py | 7 +- 3 files changed, 3 insertions(+), 341 deletions(-) delete mode 100644 docs/RULES-AS-DATA.md diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 2816c013..9ac385c9 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -311,16 +311,3 @@ Mechanically generating the Lean `Step` *relation* (not just the display table) YAML, so the proof object and the paper's figure share a single source. Today `Step` is hand-written and pinned to phino behaviorally by `difftest`; this would make the pin structural. Optional — it does not affect the proof's validity. - -**M5 — rules as checked data (proposed; `docs/RULES-AS-DATA.md`).** A concrete, partial -realization of the above. `scripts/gen-rule-data.py` (implemented) emits the eleven -root rules as **structured** `RuleSpec` data — typed redex shape, side-conditions, and -contractum — under a *fidelity lock* that aborts if phino's YAML drifts from the locked -interpretation. A hand-written interpreter `RuleSpec.applies` gives that data a semantics, and -`conformance : RootStep e e' ↔ ∃ r ∈ normalizationRuleData, r.applies e e'` makes the pin -**kernel-checked** for the root fragment (`RootStep` = `Step` minus the four congruence -constructors). This shrinks the trusted, hand-written surface from "eleven `Step` -constructors" to "one interpreter + the semantic helpers `contextualize`/`nf`/`fill`/ -`voidAtOrdinal`" — which is the floor, since phino defines those in Haskell, not in the YAML. -Fully data-driving `Step` itself (defining it *as* the interpreter over the list, and redoing -the confluence proof against that) remains the larger, unforced step. diff --git a/docs/RULES-AS-DATA.md b/docs/RULES-AS-DATA.md deleted file mode 100644 index aadd2108..00000000 --- a/docs/RULES-AS-DATA.md +++ /dev/null @@ -1,324 +0,0 @@ - - -# Rules as checked data — pinning `Step` to phino (M5, proposed) - -**Status.** The deriver (`scripts/gen-rule-data.py`) is implemented; wiring it into CI is described below. -The Lean layer below is a **reviewed draft**: it was written without a local Lean -toolchain, so the *definitions and the theorem statement* are the contract, and the -*proofs* are mechanical case-bashes that still need to be compiled and nudged into -shape. Nothing here is imported into `PhiConfluence.lean` yet, so the green build and -the `[propext, Quot.sound]` axiom gate are untouched until this is compiled and wired -in (see "Wiring", below). - -## Why this exists, and what it does (and does not) buy - -Today the eleven rules live in the repo **twice**: once as the hand-written `Step` -relation (the object the confluence theorem is about) and once as -`normalizationRules : List RuleSpec` in `Rules.lean` — display strings generated from -phino, with **no kernel-checked link** to `Step`. So "our `Step` matches phino" rests -on a human reading both plus `difftest` (which compares only one strategy's normal -forms on a curated corpus). That is the faithfulness gap. - -This milestone closes the gap *mechanically* for the **root rules**: - -``` -phino YAML ──gen-rule-data.py (fidelity lock)──▶ normalizationRuleData : List RuleSpec - │ - RuleSpec.applies │ (hand-written interpreter) - ▼ - RootStep ◀───── conformance : RootStep e e' ↔ ∃ r ∈ normalizationRuleData, r.applies e e' - │ (kernel-checked) - │ rootStep_to_step - ▼ - Step = RootStep + the four congruence constructors (the compatible closure; - phino has no congruence rules — "rules apply anywhere") -``` - -If phino changes a rule, one of two things breaks the build: - -* the change alters the rendered pattern/result/condition → the deriver's **fidelity - lock aborts** (`scripts/gen-rule-data.py` raises; CI red); or -* the change is absorbed into the regenerated `normalizationRuleData` tags but no - longer matches `RootStep` → **`conformance` fails to type-check**. - -**What it does not buy.** phino's rule *semantics* live in its Haskell — `contextualize`, -`isNF`/`nf`, the domain ordinal `voidAtOrdinal`, `fill` — and are only *named* in the -YAML (e.g. `dot`'s `where: 𝑒2 := contextualize(𝑒1, …)`). Those functions are still -hand-written in Lean (`Context.lean`, `Nf.lean`, `Attributes.lean`) and **trusted** to -match phino regardless of any codegen. So this does not make `Step` "derived from -phino" in the strong sense; it makes the *rule structure* (which redex shape, which -side-conditions, which contractum, per rule) generated data that is **kernel-checked -against `Step`**, while the semantic vocabulary remains a small, explicit trusted -surface. That is the honest ceiling of mechanization while phino is the reference and -its semantics are not themselves formalized. - -## ξ-free: data vs display (a bug this surfaced) - -`gen-rules.py` claims to strip `copy`'s `ξ`-free guard "so `copy` shows `nf(𝑒1)` only", -but the committed `Rules.lean` still reads `cond := "xi-free(𝑒) and nf(𝑒)"`: the strip -`if k == "xi"` never fires because phino's key is `xi-free`. The clean resolution is the -data/display split this milestone introduces: - -* **Data** (`gen-rule-data.py`, this layer) **keeps** `ξ`-free — because `Step.copy` - carries `xiFree e₁`, so the conformance theorem *needs* it. -* **Display** (`gen-rules.py`) may strip `ξ` for paper-figure parity — a rendering - choice, not a semantic one. - -So `gen-rules.py`'s `if k == "xi"` should be `if k == "xi-free"` (display intent), and -`gen-rule-data.py` deliberately does **not** strip it (proof intent). Filed as a -separate small fix; tracked here so the two generators do not silently disagree. - -## The Lean layer (draft — compile before relying on) - -### `PhiConfluence/RuleSchema.lean` (hand-written: schema + interpreter) - -```lean --- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com --- SPDX-License-Identifier: MIT - -import PhiConfluence.Step - -/-! -# Structured rule schema + interpreter - -`RuleSpec` is one normalization rule as interpretable tags (redex shape, side-conditions, -contractum). `RuleSpec.applies r e e'` is its semantics over `Term`, built from the same -primitives `Step` uses (`lookup`, `nf`, `xiFree`, `voidAtOrdinal`, `contextualize`, `fill`). -The generated `normalizationRuleData` (RuleData.lean) is a `List RuleSpec`; `RuleConform` -proves that list equal to the root fragment of `Step`. --/ - -namespace PhiConfluence - -/-- Which redex a rule fires on: `⊥.a`, `⊥(a↦arg)`, `⟦bs⟧.a`, or `⟦bs⟧(a↦arg)`. -/ -inductive RedexShape where - | dispatchBot | appBot | dispatchForm | appForm - deriving Repr, DecidableEq - -/-- A side condition, read against the redex's `(bs, a, arg)`. -/ -inductive Cond where - | slotVoid | slotAttached | slotAbsent - | attrNeRho | attrIsRho | attrNotAlpha - | phiAbsent | phiPresent | noLambda - | valNf | argXiFree | argNf | alphaVoidOrdinal - deriving Repr, DecidableEq - -/-- The contractum, built from the redex's `(bs, a, arg)`. -/ -inductive Contractum where - | bot | formSame | phiExpand | dotFeedback | copyFill | alphaRename - deriving Repr, DecidableEq - -/-- One rule as data. -/ -structure RuleSpec where - name : String - shape : RedexShape - conds : List Cond - rhs : Contractum - -/-- A side condition as a `Prop` over the redex's formation `bs`, attribute `a`, argument `arg`. -/ -def Cond.holds (bs : List Binding) (a : Attr) (arg : Term) : Cond → Prop - | .slotVoid => lookup bs a = .void - | .slotAttached => ∃ v, lookup bs a = .attached v - | .slotAbsent => lookup bs a = .absent - | .attrNeRho => a ≠ .rho - | .attrIsRho => a = .rho - | .attrNotAlpha => a.isAlpha = false - | .phiAbsent => lookup bs .phi = .absent - | .phiPresent => lookup bs .phi ≠ .absent - | .noLambda => hasLambda bs = false - | .valNf => ∃ v, lookup bs a = .attached v ∧ nf v = true - | .argXiFree => xiFree arg = true - | .argNf => nf arg = true - | .alphaVoidOrdinal => ∃ i τ, a = .alpha i ∧ voidAtOrdinal bs i = some τ - -/-- The contractum as a (partial) `Term`, from the redex's `(bs, a, arg)`. -/ -def Contractum.build (bs : List Binding) (a : Attr) (arg : Term) : Contractum → Option Term - | .bot => some .bot - | .formSame => some (.form bs) - | .phiExpand => some (.dispatch (.dispatch (.form bs) .phi) a) - | .copyFill => some (.form (fill bs a arg)) - | .dotFeedback => - match lookup bs a with - | .attached v => some (.app (contextualize v (.form bs)) .rho (.form bs)) - | _ => none - | .alphaRename => - match a with - | .alpha i => match voidAtOrdinal bs i with - | some τ => some (.app (.form bs) τ arg) - | none => none - | _ => none - -/-- The semantics of a rule: does `e ↝ e'` by rule `r`? -/ -def RuleSpec.applies (r : RuleSpec) (e e' : Term) : Prop := - match r.shape, e with - | .dispatchBot, .dispatch .bot _ => r.conds = [] ∧ r.rhs = .bot ∧ e' = .bot - | .appBot, .app .bot _ _ => r.conds = [] ∧ r.rhs = .bot ∧ e' = .bot - | .dispatchForm, .dispatch (.form bs) a => (∀ c ∈ r.conds, c.holds bs a .bot) ∧ r.rhs.build bs a .bot = some e' - | .appForm, .app (.form bs) a arg => (∀ c ∈ r.conds, c.holds bs a arg) ∧ r.rhs.build bs a arg = some e' - | _, _ => False - -end PhiConfluence -``` - -### `PhiConfluence/RuleData.lean` (GENERATED by `gen-rule-data.py`) - -This is exactly what the (tested) deriver emits today; commit it via -`python3 scripts/gen-rule-data.py /resources PhiConfluence/RuleData.lean`: - -```lean --- AUTO-GENERATED by scripts/gen-rule-data.py from objectionary/phino resources/*.yaml. -import PhiConfluence.RuleSchema -namespace PhiConfluence - -/-- The φ-calculus normalization rules as structured, interpretable data. -/ -def normalizationRuleData : List RuleSpec := - [ { name := "alpha", shape := .appForm, conds := [.alphaVoidOrdinal], rhs := .alphaRename } - , { name := "copy", shape := .appForm, conds := [.slotVoid, .argXiFree, .argNf], rhs := .copyFill } - , { name := "dc", shape := .appBot, conds := [], rhs := .bot } - , { name := "dd", shape := .dispatchBot, conds := [], rhs := .bot } - , { name := "dot", shape := .dispatchForm, conds := [.slotAttached, .valNf], rhs := .dotFeedback } - , { name := "miss", shape := .appForm, conds := [.slotAbsent, .attrNotAlpha], rhs := .bot } - , { name := "null", shape := .dispatchForm, conds := [.slotVoid], rhs := .bot } - , { name := "over", shape := .appForm, conds := [.slotAttached, .attrNeRho], rhs := .bot } - , { name := "phi", shape := .dispatchForm, conds := [.phiPresent, .slotAbsent], rhs := .phiExpand } - , { name := "stay", shape := .appForm, conds := [.attrIsRho, .slotAttached], rhs := .formSame } - , { name := "stop", shape := .dispatchForm, conds := [.slotAbsent, .phiAbsent, .noLambda], rhs := .bot } ] - -end PhiConfluence -``` - -### `PhiConfluence/RuleConform.lean` (hand-written: the pin) - -```lean --- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com --- SPDX-License-Identifier: MIT - -import PhiConfluence.RuleData - -/-! -# Conformance: the generated rule data is exactly `Step`'s root fragment - -`RootStep` is `Step` minus the four congruence constructors (phino has no congruence -rules; the closure is the project's own). `conformance` pins the phino-derived -`normalizationRuleData` to `RootStep`, and `rootStep_to_step` ties `RootStep` back into -the relation the confluence theorem governs. --/ - -namespace PhiConfluence - -/-- The eleven root rules of `Step`, without the congruence closure. -/ -inductive RootStep : Term → Term → Prop where - | dd (a : Attr) : RootStep (.dispatch .bot a) .bot - | dc (a : Attr) (e : Term) : RootStep (.app .bot a e) .bot - | null {bs a} : lookup bs a = .void → RootStep (.dispatch (.form bs) a) .bot - | over {bs a e₁ e₂} : lookup bs a = .attached e₁ → a ≠ .rho → RootStep (.app (.form bs) a e₂) .bot - | stop {bs a} : lookup bs a = .absent → lookup bs .phi = .absent → hasLambda bs = false → - RootStep (.dispatch (.form bs) a) .bot - | miss {bs a e} : lookup bs a = .absent → a.isAlpha = false → RootStep (.app (.form bs) a e) .bot - | stay {bs e₁ e₂} : lookup bs .rho = .attached e₁ → RootStep (.app (.form bs) .rho e₂) (.form bs) - | phi {bs a} : lookup bs .phi ≠ .absent → lookup bs a = .absent → - RootStep (.dispatch (.form bs) a) (.dispatch (.dispatch (.form bs) .phi) a) - | alpha {bs i τ₁ e} : voidAtOrdinal bs i = some τ₁ → - RootStep (.app (.form bs) (.alpha i) e) (.app (.form bs) τ₁ e) - | dot {bs a e₁} : lookup bs a = .attached e₁ → nf e₁ = true → - RootStep (.dispatch (.form bs) a) (.app (contextualize e₁ (.form bs)) .rho (.form bs)) - | copy {bs a e₁} : lookup bs a = .void → xiFree e₁ = true → nf e₁ = true → - RootStep (.app (.form bs) a e₁) (.form (fill bs a e₁)) - -/-- Every root step is a `Step` (each constructor maps to the same-named `Step` rule). -/ -theorem rootStep_to_step {e e' : Term} (h : RootStep e e') : Step e e' := by - cases h with - | dd a => exact .dd a - | dc a e => exact .dc a e - | null h => exact .null h - | over h1 h2 => exact .over h1 h2 - | stop h1 h2 h3 => exact .stop h1 h2 h3 - | miss h1 h2 => exact .miss h1 h2 - | stay h => exact .stay h - | phi h1 h2 => exact .phi h1 h2 - | alpha h => exact .alpha h - | dot h1 h2 => exact .dot h1 h2 - | copy h1 h2 h3 => exact .copy h1 h2 h3 - -/-- **The pin.** The phino-derived rule data denotes exactly `RootStep`. A phino change -that survives the deriver but alters a rule's meaning breaks this theorem. -/ -theorem conformance {e e' : Term} : - RootStep e e' ↔ ∃ r ∈ normalizationRuleData, r.applies e e' := by - constructor - · intro h - -- forward: each RootStep constructor exhibits its generated entry as the witness. - cases h with - | dd a => exact ⟨_, by simp [normalizationRuleData], by simp [RuleSpec.applies]⟩ - | dc a e => exact ⟨_, by simp [normalizationRuleData], by simp [RuleSpec.applies]⟩ - | null h => - exact ⟨_, by simp [normalizationRuleData], - by simp [RuleSpec.applies, Cond.holds, Contractum.build, h]⟩ - | over h1 h2 => - exact ⟨_, by simp [normalizationRuleData], - by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2]⟩ - | stop h1 h2 h3 => - exact ⟨_, by simp [normalizationRuleData], - by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2, h3]⟩ - | miss h1 h2 => - exact ⟨_, by simp [normalizationRuleData], - by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2]⟩ - | stay h => - exact ⟨_, by simp [normalizationRuleData], - by simp [RuleSpec.applies, Cond.holds, Contractum.build, h]⟩ - | phi h1 h2 => - exact ⟨_, by simp [normalizationRuleData], - by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2]⟩ - | alpha h => - exact ⟨_, by simp [normalizationRuleData], - by simp [RuleSpec.applies, Cond.holds, Contractum.build, h]⟩ - | dot h1 h2 => - exact ⟨_, by simp [normalizationRuleData], - by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2]⟩ - | copy h1 h2 h3 => - exact ⟨_, by simp [normalizationRuleData], - by simp [RuleSpec.applies, Cond.holds, Contractum.build, h1, h2, h3]⟩ - · rintro ⟨r, hr, ha⟩ - -- backward: enumerate the 11 entries; each `applies` reconstructs its RootStep rule. - -- `fin_cases hr` splits the list; `RuleSpec.applies` then forces the redex shape and, - -- via `Cond.holds`/`Contractum.build`, the side-conditions and contractum. - fin_cases hr <;> - first - | (obtain ⟨hc, hb⟩ := ha; · skip) -- PUZZLE: per-entry, destructure conds/build then - -- `cases e` to expose the redex and apply the - -- matching `RootStep` constructor. See notes below. - | skip - -end PhiConfluence -``` - -The backward direction is the one genuine puzzle: after `fin_cases hr` each goal has a -concrete `r` and `ha : r.applies e e'`; `simp [RuleSpec.applies] at ha` forces `e` into -the rule's redex shape (`dispatch (form bs) a` etc.), `Cond.holds` turns the condition -list into the rule's hypotheses, `Contractum.build … = some e'` pins `e'`, and the -matching `RootStep.` closes it. It is mechanical but verbose; left as a -**Puzzle** to complete against the compiler rather than guess blind here. - -## Wiring (once compiled green) - -1. Add `RuleSchema.lean`; `python3 scripts/gen-rule-data.py /resources - PhiConfluence/RuleData.lean`; add `RuleConform.lean`. Compile and finish the one - backward-direction puzzle. -2. Add the three modules to `PhiConfluence.lean`'s import list. -3. Add a CI job mirroring `rules-in-sync` for the data file - (`gen-rule-data.py` → `git diff --exit-code PhiConfluence/RuleData.lean`); the - deriver's fidelity lock means a phino change fails the regen step itself. -4. Add `PhiConfluence.conformance` and `PhiConfluence.rootStep_to_step` to the - `#print axioms` gate in `build.yml` (expect `[propext, Quot.sound]` or cleaner). -5. Fix the display generator's `ξ` strip (`gen-rules.py`: `"xi"` → `"xi-free"`). - -## Puzzles left - -* **§M5-a** Complete the backward direction of `conformance` (see above). -* **§M5-b** Optional: extend the pin from `RootStep` to a statement about `Step` - directly — e.g. prove `Step` is the compatible closure of `RootStep`, so the - congruence constructors are visibly *not* phino-derived but the standard closure. -* **§M5-c** `λ`/`Δ` assets: the deriver has no rule for them by design (phino has - none); if asset reduction is ever modelled, both the lock and the schema extend. diff --git a/scripts/gen-rule-data.py b/scripts/gen-rule-data.py index fde7e0fa..94b30a61 100644 --- a/scripts/gen-rule-data.py +++ b/scripts/gen-rule-data.py @@ -14,8 +14,8 @@ DESIGN — a *fidelity lock*, not a general translator. phino's rule semantics live in its Haskell (`contextualize`, `isNF`, ordinals …), - not in the YAML, so the YAML cannot be mechanically translated into a Lean relation - (see docs/RULES-AS-DATA.md). Instead this script carries one *locked interpretation* + not in the YAML, so the YAML cannot be mechanically translated into a Lean relation. + Instead this script carries one *locked interpretation* per rule (the structured tags below) and ASSERTS that phino's current YAML still renders to the pattern/result/condition this interpretation assumes — failing loudly on any mismatch. The locked tags are emitted; the proof checks them against `Step`. @@ -140,8 +140,7 @@ def norm(s): "𝑒2 := contextualize(𝑒1, ⟦𝐵1, 𝜏 ↦ 𝑒1, 𝐵2⟧)"), shape=".dispatchForm", conds="[.slotAttached, .valNf]", rhs=".dotFeedback"), # NOTE — copy keeps phino's `xi-free` guard in the DATA (Step.copy carries `xiFree`); - # only the DISPLAY table (gen-rules.py) strips ξ for paper-figure parity. See - # docs/RULES-AS-DATA.md "ξ-free: data vs display". + # only the DISPLAY table (gen-rules.py) strips ξ for paper-figure parity. "copy": dict( expect=("⟦ 𝐵1, 𝜏 ↦ ∅, 𝐵2 ⟧(𝜏 ↦ 𝑒)", "⟦ 𝐵1, 𝜏 ↦ 𝑒, 𝐵2 ⟧", "xi-free(𝑒) and nf(𝑒)", ""), From b6d4074cd44a8d8c7be0b946c5bfc3698cfc821a Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 17:51:31 +0300 Subject: [PATCH 11/13] feat: add phino-generated RuleData.lean with in-sync CI check MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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`. --- .github/workflows/rule-data-in-sync.yml | 29 +++++++++++++++++ PhiConfluence.lean | 2 ++ PhiConfluence/RuleData.lean | 33 +++++++++++++++++++ PhiConfluence/RuleSchema.lean | 43 +++++++++++++++++++++++++ scripts/gen-rule-data.py | 26 +++++++-------- scripts/regen-rule-data.sh | 27 ++++++++++++++++ 6 files changed, 146 insertions(+), 14 deletions(-) create mode 100644 .github/workflows/rule-data-in-sync.yml create mode 100644 PhiConfluence/RuleData.lean create mode 100644 PhiConfluence/RuleSchema.lean create mode 100644 scripts/regen-rule-data.sh diff --git a/.github/workflows/rule-data-in-sync.yml b/.github/workflows/rule-data-in-sync.yml new file mode 100644 index 00000000..75ad6f64 --- /dev/null +++ b/.github/workflows/rule-data-in-sync.yml @@ -0,0 +1,29 @@ +# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com +# SPDX-License-Identifier: MIT + +name: rule-data-in-sync +on: + push: + branches: [master] + pull_request: + +concurrency: + group: rule-data-in-sync-${{ github.ref }} + cancel-in-progress: true + +jobs: + rule-data-in-sync: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: '3.x' + - run: pip install pyyaml + - name: Regenerate RuleData.lean from pinned phino and detect drift + run: | + bash scripts/regen-rule-data.sh + if ! git diff --exit-code PhiConfluence/RuleData.lean; then + echo "::error::PhiConfluence/RuleData.lean is out of sync with phino — run scripts/regen-rule-data.sh and commit" + exit 1 + fi diff --git a/PhiConfluence.lean b/PhiConfluence.lean index a89b9120..40a441ac 100644 --- a/PhiConfluence.lean +++ b/PhiConfluence.lean @@ -13,6 +13,8 @@ import PhiConfluence.Step import PhiConfluence.Reduce import PhiConfluence.Render import PhiConfluence.Rules +import PhiConfluence.RuleSchema +import PhiConfluence.RuleData import PhiConfluence.Parallel import PhiConfluence.Preservation import PhiConfluence.Diamond diff --git a/PhiConfluence/RuleData.lean b/PhiConfluence/RuleData.lean new file mode 100644 index 00000000..a3b63cb5 --- /dev/null +++ b/PhiConfluence/RuleData.lean @@ -0,0 +1,33 @@ +-- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com +-- SPDX-License-Identifier: MIT + +-- AUTO-GENERATED by scripts/gen-rule-data.py from objectionary/phino resources/*.yaml. +-- DO NOT EDIT BY HAND. Regenerate after phino's rules change. + +import PhiConfluence.RuleSchema + +/-! +# Normalization rules as structured data, generated from phino + +The eleven rules as `RuleEntry` tags (types in PhiConfluence/RuleSchema.lean), emitted +by the fidelity-lock deriver `scripts/gen-rule-data.py`. CI (rule-data-in-sync) +regenerates this file from pinned phino and fails on any diff — keeping it identical. +-/ + +namespace PhiConfluence + +/-- The φ-calculus normalization rules as structured, interpretable data. -/ +def normalizationRuleData : List RuleEntry := + [ { name := "alpha", shape := .appForm, conds := [.alphaVoidOrdinal], rhs := .alphaRename } + , { name := "copy", shape := .appForm, conds := [.slotVoid, .argXiFree, .argNf], rhs := .copyFill } + , { name := "dc", shape := .appBot, conds := [], rhs := .bot } + , { name := "dd", shape := .dispatchBot, conds := [], rhs := .bot } + , { name := "dot", shape := .dispatchForm, conds := [.slotAttached, .valNf], rhs := .dotFeedback } + , { name := "miss", shape := .appForm, conds := [.slotAbsent, .attrNotAlpha], rhs := .bot } + , { name := "null", shape := .dispatchForm, conds := [.slotVoid], rhs := .bot } + , { name := "over", shape := .appForm, conds := [.slotAttached, .attrNeRho], rhs := .bot } + , { name := "phi", shape := .dispatchForm, conds := [.phiPresent, .slotAbsent], rhs := .phiExpand } + , { name := "stay", shape := .appForm, conds := [.attrIsRho, .slotAttached], rhs := .formSame } + , { name := "stop", shape := .dispatchForm, conds := [.slotAbsent, .phiAbsent, .noLambda], rhs := .bot } ] + +end PhiConfluence diff --git a/PhiConfluence/RuleSchema.lean b/PhiConfluence/RuleSchema.lean new file mode 100644 index 00000000..69918115 --- /dev/null +++ b/PhiConfluence/RuleSchema.lean @@ -0,0 +1,43 @@ +-- SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com +-- SPDX-License-Identifier: MIT + +/-! +# Schema for the generated rule data + +The typed vocabulary that `PhiConfluence/RuleData.lean` (generated from phino by +`scripts/gen-rule-data.py`) is written in: each normalization rule is a `RuleEntry` of +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. +-/ + +namespace PhiConfluence + +/-- Which redex a rule fires on: `⊥.a`, `⊥(a↦arg)`, `⟦bs⟧.a`, or `⟦bs⟧(a↦arg)`. -/ +inductive RedexShape where + | dispatchBot | appBot | dispatchForm | appForm + deriving Repr, DecidableEq + +/-- A side condition on the redex's formation, attribute, and argument. -/ +inductive Cond where + | slotVoid | slotAttached | slotAbsent + | attrNeRho | attrIsRho | attrNotAlpha + | phiAbsent | phiPresent | noLambda + | valNf | argXiFree | argNf | alphaVoidOrdinal + deriving Repr, DecidableEq + +/-- The contractum a rule rewrites its redex to. -/ +inductive Contractum where + | bot | formSame | phiExpand | dotFeedback | copyFill | alphaRename + deriving Repr, DecidableEq + +/-- One normalization rule as structured data. (Named `RuleEntry`, not `RuleSpec`, +to avoid colliding with `Render.lean`'s display-string `RuleSpec`.) -/ +structure RuleEntry where + name : String + shape : RedexShape + conds : List Cond + rhs : Contractum + +end PhiConfluence diff --git a/scripts/gen-rule-data.py b/scripts/gen-rule-data.py index 94b30a61..1d6fd630 100644 --- a/scripts/gen-rule-data.py +++ b/scripts/gen-rule-data.py @@ -5,12 +5,11 @@ Generate PhiConfluence/RuleData.lean from phino's resources/*.yaml. Unlike `gen-rules.py` (which emits *display strings* for the demo), this emits the -**structured** rule data the proof is pinned against: each rule becomes a `RuleSpec` -of typed tags (redex shape, side-conditions, contractum) that the hand-written -interpreter `applies` (PhiConfluence/RuleSchema.lean) gives a semantics to, and that -`conformance` (PhiConfluence/RuleConform.lean) proves equal to the `Step` relation. -So if phino changes a rule, the regenerated data changes and the Lean conformance -theorem stops type-checking — drift between phino and the proof becomes a build error. +**structured** rule data: each rule becomes a `RuleEntry` of typed tags (redex shape, +side-conditions, contractum), whose types are defined in PhiConfluence/RuleSchema.lean. +The committed PhiConfluence/RuleData.lean is regenerated from pinned phino by CI +(rule-data-in-sync) and compared for an exact match, so a phino rule change becomes a +build error unless the committed data is regenerated to match. DESIGN — a *fidelity lock*, not a general translator. phino's rule semantics live in its Haskell (`contextualize`, `isNF`, ordinals …), @@ -18,9 +17,9 @@ Instead this script carries one *locked interpretation* per rule (the structured tags below) and ASSERTS that phino's current YAML still renders to the pattern/result/condition this interpretation assumes — failing loudly - on any mismatch. The locked tags are emitted; the proof checks them against `Step`. - Net: phino-drift trips the assertion here (CI red); a tags-vs-`Step` mismatch trips - the Lean conformance theorem. Both ends are pinned. + on any mismatch. The locked tags are emitted into RuleData.lean. phino-drift trips + this assertion; a committed RuleData.lean that no longer matches trips the + rule-data-in-sync diff in CI. This intentionally duplicates `gen-rules.py`'s `when`/`where` rendering (keep in sync) so the asserted condition strings match the display table's — one rendering, two consumers. @@ -192,16 +191,15 @@ def main(): "/-!", "# Normalization rules as structured data, generated from phino", "", - "The eleven rules as `RuleSpec` tags, emitted by the fidelity-lock deriver", - "`scripts/gen-rule-data.py`. `PhiConfluence.RuleConform.conformance` proves this list", - "equal to the `Step` relation, so a phino change that survives the deriver's assertions", - "but alters a rule's meaning makes that theorem fail to compile.", + "The eleven rules as `RuleEntry` tags (types in PhiConfluence/RuleSchema.lean), emitted", + "by the fidelity-lock deriver `scripts/gen-rule-data.py`. CI (rule-data-in-sync)", + "regenerates this file from pinned phino and fails on any diff — keeping it identical.", "-/", "", "namespace PhiConfluence", "", "/-- The φ-calculus normalization rules as structured, interpretable data. -/", - "def normalizationRuleData : List RuleSpec :=", + "def normalizationRuleData : List RuleEntry :=", ] entries = [] for name in sorted(found): diff --git a/scripts/regen-rule-data.sh b/scripts/regen-rule-data.sh new file mode 100644 index 00000000..9e6ff1e9 --- /dev/null +++ b/scripts/regen-rule-data.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash +# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com +# SPDX-License-Identifier: MIT +# +# Regenerate PhiConfluence/RuleData.lean from the PINNED phino rules on GitHub +# (objectionary/phino at the tag in .phino-version). The fidelity lock in +# scripts/gen-rule-data.py aborts if phino's rules drift from the locked interpretation; +# the rule-data-in-sync CI job then diffs the result against the committed file. +# +# Usage: bash scripts/regen-rule-data.sh + +set -euo pipefail +cd "$(dirname "$0")/.." + +PHINO_REPO="${PHINO_REPO:-https://github.com/objectionary/phino}" +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.}" +tmp="$(mktemp -d)" +trap 'rm -rf "$tmp"' EXIT + +echo "cloning $PHINO_REPO at tag $PHINO_TAG (phino $PHINO_VERSION, pinned via .phino-version) ..." +git clone --depth 1 --branch "$PHINO_TAG" "$PHINO_REPO" "$tmp/phino" >/dev/null 2>&1 + +python3 scripts/gen-rule-data.py "$tmp/phino/resources" PhiConfluence/RuleData.lean +echo "done — PhiConfluence/RuleData.lean regenerated from phino $PHINO_VERSION" From 82fe64d86c3b22609cffe9fad662f818785641d8 Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 18:09:44 +0300 Subject: [PATCH 12/13] ci: regenerate RuleData.lean from phino in the build, drop in-sync job 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`. --- .github/workflows/build.yml | 7 ++++++ .github/workflows/rule-data-in-sync.yml | 29 ------------------------- PhiConfluence/RuleData.lean | 4 ++-- scripts/gen-rule-data.py | 16 +++++++------- scripts/regen-rule-data.sh | 4 ++-- 5 files changed, 19 insertions(+), 41 deletions(-) delete mode 100644 .github/workflows/rule-data-in-sync.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 7df2a638..5b4c4ce3 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -17,6 +17,13 @@ jobs: steps: - uses: actions/checkout@v4 - uses: ./.github/actions/setup-lean + - uses: actions/setup-python@v5 + with: + python-version: '3.x' + - name: Regenerate RuleData.lean from pinned phino (build against phino's rules) + run: | + pip install pyyaml + bash scripts/regen-rule-data.sh - name: Build the library and executables run: | lake build diff --git a/.github/workflows/rule-data-in-sync.yml b/.github/workflows/rule-data-in-sync.yml deleted file mode 100644 index 75ad6f64..00000000 --- a/.github/workflows/rule-data-in-sync.yml +++ /dev/null @@ -1,29 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com -# SPDX-License-Identifier: MIT - -name: rule-data-in-sync -on: - push: - branches: [master] - pull_request: - -concurrency: - group: rule-data-in-sync-${{ github.ref }} - cancel-in-progress: true - -jobs: - rule-data-in-sync: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - uses: actions/setup-python@v5 - with: - python-version: '3.x' - - run: pip install pyyaml - - name: Regenerate RuleData.lean from pinned phino and detect drift - run: | - bash scripts/regen-rule-data.sh - if ! git diff --exit-code PhiConfluence/RuleData.lean; then - echo "::error::PhiConfluence/RuleData.lean is out of sync with phino — run scripts/regen-rule-data.sh and commit" - exit 1 - fi diff --git a/PhiConfluence/RuleData.lean b/PhiConfluence/RuleData.lean index a3b63cb5..ccff5ffc 100644 --- a/PhiConfluence/RuleData.lean +++ b/PhiConfluence/RuleData.lean @@ -10,8 +10,8 @@ import PhiConfluence.RuleSchema # Normalization rules as structured data, generated from phino The eleven rules as `RuleEntry` tags (types in PhiConfluence/RuleSchema.lean), emitted -by the fidelity-lock deriver `scripts/gen-rule-data.py`. CI (rule-data-in-sync) -regenerates this file from pinned phino and fails on any diff — keeping it identical. +by the fidelity-lock deriver `scripts/gen-rule-data.py`. The CI build regenerates this +file from pinned phino and compiles it, so the proof builds against phino's rules. -/ namespace PhiConfluence diff --git a/scripts/gen-rule-data.py b/scripts/gen-rule-data.py index 1d6fd630..a87cf31a 100644 --- a/scripts/gen-rule-data.py +++ b/scripts/gen-rule-data.py @@ -7,9 +7,9 @@ Unlike `gen-rules.py` (which emits *display strings* for the demo), this emits the **structured** rule data: each rule becomes a `RuleEntry` of typed tags (redex shape, side-conditions, contractum), whose types are defined in PhiConfluence/RuleSchema.lean. -The committed PhiConfluence/RuleData.lean is regenerated from pinned phino by CI -(rule-data-in-sync) and compared for an exact match, so a phino rule change becomes a -build error unless the committed data is regenerated to match. +The CI build regenerates PhiConfluence/RuleData.lean from pinned phino and then compiles +it, so the proof always builds against phino-derived rules and a phino change that breaks +compilation (or trips the fidelity lock below) fails the build. DESIGN — a *fidelity lock*, not a general translator. phino's rule semantics live in its Haskell (`contextualize`, `isNF`, ordinals …), @@ -17,9 +17,9 @@ Instead this script carries one *locked interpretation* per rule (the structured tags below) and ASSERTS that phino's current YAML still renders to the pattern/result/condition this interpretation assumes — failing loudly - on any mismatch. The locked tags are emitted into RuleData.lean. phino-drift trips - this assertion; a committed RuleData.lean that no longer matches trips the - rule-data-in-sync diff in CI. + on any mismatch. The locked tags are emitted into RuleData.lean, which the CI build + regenerates from pinned phino and compiles — so phino-drift trips this assertion and + fails the build. This intentionally duplicates `gen-rules.py`'s `when`/`where` rendering (keep in sync) so the asserted condition strings match the display table's — one rendering, two consumers. @@ -192,8 +192,8 @@ def main(): "# Normalization rules as structured data, generated from phino", "", "The eleven rules as `RuleEntry` tags (types in PhiConfluence/RuleSchema.lean), emitted", - "by the fidelity-lock deriver `scripts/gen-rule-data.py`. CI (rule-data-in-sync)", - "regenerates this file from pinned phino and fails on any diff — keeping it identical.", + "by the fidelity-lock deriver `scripts/gen-rule-data.py`. The CI build regenerates this", + "file from pinned phino and compiles it, so the proof builds against phino's rules.", "-/", "", "namespace PhiConfluence", diff --git a/scripts/regen-rule-data.sh b/scripts/regen-rule-data.sh index 9e6ff1e9..b5194db2 100644 --- a/scripts/regen-rule-data.sh +++ b/scripts/regen-rule-data.sh @@ -4,8 +4,8 @@ # # Regenerate PhiConfluence/RuleData.lean from the PINNED phino rules on GitHub # (objectionary/phino at the tag in .phino-version). The fidelity lock in -# scripts/gen-rule-data.py aborts if phino's rules drift from the locked interpretation; -# the rule-data-in-sync CI job then diffs the result against the committed file. +# scripts/gen-rule-data.py aborts if phino's rules drift from the locked interpretation. +# The CI build runs this before `lake build`, so the proof compiles against phino's rules. # # Usage: bash scripts/regen-rule-data.sh From 60584932a4eb74c6dc65efe5e674a13d0c0d235a Mon Sep 17 00:00:00 2001 From: Yegor Bugayenko Date: Thu, 4 Jun 2026 18:29:00 +0300 Subject: [PATCH 13/13] ci: regenerate Rules.lean too in the build, drop rules-in-sync MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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`. --- .github/workflows/build.yml | 3 ++- .github/workflows/rules-in-sync.yml | 29 ----------------------------- docs/DESIGN.md | 18 ++++++++++-------- 3 files changed, 12 insertions(+), 38 deletions(-) delete mode 100644 .github/workflows/rules-in-sync.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 5b4c4ce3..deb9fa70 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -20,9 +20,10 @@ jobs: - uses: actions/setup-python@v5 with: python-version: '3.x' - - name: Regenerate RuleData.lean from pinned phino (build against phino's rules) + - name: Regenerate Rules.lean and RuleData.lean from pinned phino run: | pip install pyyaml + bash scripts/regen-rules.sh bash scripts/regen-rule-data.sh - name: Build the library and executables run: | diff --git a/.github/workflows/rules-in-sync.yml b/.github/workflows/rules-in-sync.yml deleted file mode 100644 index c98473a7..00000000 --- a/.github/workflows/rules-in-sync.yml +++ /dev/null @@ -1,29 +0,0 @@ -# SPDX-FileCopyrightText: Copyright (c) 2026 Objectionary.com -# SPDX-License-Identifier: MIT - -name: rules-in-sync -on: - push: - branches: [master] - pull_request: - -concurrency: - group: rules-in-sync-${{ github.ref }} - cancel-in-progress: true - -jobs: - rules-in-sync: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - uses: actions/setup-python@v5 - with: - python-version: '3.x' - - run: pip install pyyaml - - name: Regenerate rules from phino (latest) and detect drift - run: | - bash scripts/regen-rules.sh - if ! git diff --exit-code PhiConfluence/Rules.lean; then - echo "::error::PhiConfluence/Rules.lean is out of sync with phino — run scripts/regen-rules.sh and commit" - exit 1 - fi diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 9ac385c9..6682e8d5 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -150,8 +150,8 @@ independent directions: * **Tiny, human-readable trusted surface.** Only `Syntax`, `Step`, `↝∗`, and the `confluence` statement must be read and endorsed (a few dozen lines — the M0 spec). * **Rule transcription vs phino.** The eleven-rule *display* table (`Rules.lean`) is - **generated** from phino's `resources/*.yaml` by `gen-rules.py` and pinned by the - `rules-in-sync` CI job, so the displayed rules cannot drift from phino/the paper. The + **generated** from phino's `resources/*.yaml` by `gen-rules.py` and regenerated from + pinned phino in the CI build, so the displayed rules cannot drift from phino/the paper. The *proof relation* `Step` is hand-written (constructors are needed for case-analysis) and pinned to phino **behaviorally** by `difftest`. * **Differential testing against phino.** `Difftest.lean` + `scripts/difftest.sh` normalize @@ -232,13 +232,15 @@ relation the confluence theorem governs. from phino's `resources/*.yaml` — the same source the paper's Fig. 4 is rendered from — so the displayed rules cannot drift from phino/the paper by construction. -**CI** (single-purpose workflows, each on push to `master` + PRs, tracking phino-latest): +**CI** (single-purpose workflows, each on push to `master` + PRs, against pinned phino): -* **build** — install elan, `lake exe cache get`, `lake build`; then a `sorry`/`admit`/ - `axiom` source gate **and** a `#print axioms` gate on the headline results. -* **rules-in-sync** — `scripts/regen-rules.sh` clones `objectionary/phino` and regenerates - `Rules.lean`; `git diff --exit-code` fails if our committed table has drifted from phino. -* **difftest** — install the `phino-latest` binary, build `difftest`, run +* **build** — install elan and `lake exe cache get`; regenerate `Rules.lean` and + `RuleData.lean` from the pinned phino (`scripts/regen-rules.sh`, + `scripts/regen-rule-data.sh`) so the proof compiles against phino-derived rules; `lake + build`; then a `sorry`/`admit`/`axiom` source gate **and** a `#print axioms` gate on the + headline results. (`gen-rule-data.py`'s fidelity lock fails the build on rule-structure + drift.) +* **difftest** — install the pinned phino binary (`.phino-version`), build `difftest`, run `scripts/difftest.sh`; fails if our reducer disagrees with phino. The two Lean workflows share a composite action (`.github/actions/setup-lean`) that caches