Derive normalization rules from phino as checked data

.github/workflows/build.yml

@@ -17,6 +17,14 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/actions/setup-lean
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.x'
+      - 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: |
           lake build

.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

.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

.phino-version

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

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

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`. The CI build regenerates this
+file from pinned phino and compiles it, so the proof builds against phino's rules.
+-/
+
+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

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

REUSE.toml

@@ -5,6 +5,7 @@ version = 1
 [[annotations]]
 path = [
     ".gitignore",
+    ".phino-version",
     ".yamllint",
     "**.json",
     "**.md",

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

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 <diverge>/<error> for an unfinished/failed run.
 norm() {
   local out ec
-  out=$($TO phino rewrite --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 "<diverge>"
   elif [ "$ec" = 0 ]; then echo "$out"
   elif printf '%s' "$out" | grep -q 'depth-sensitive'; then echo "<diverge>"
@@ -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 --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 --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 --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")

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