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

[yegor256]

Closes #74.

The display table (PhiConfluence/Rules.lean, generated by .github/gen-rules.py) says it strips phino's ξ-free side-conditions, so that copy shows only nf(𝑒), as in the paper. It never did. The renderer looked for the key xi, but phino's copy.yaml uses xi-free, so copy was rendered as xi-free(𝑒) and nf(𝑒).

Since #72, the rendering lives in .github/phino_render.py, which is shared by the display table and the fidelity lock in gen-rule-data.py. The lock deliberately keeps the ξ-free guard, because Step.copy carries xiFree and LOCK["copy"] expects "xi-free(𝑒) and nf(𝑒)". So the strip has to apply to the display table only.

Changes:

• phino_render.rcond and phino_render.rules take a strip_xi=False flag. When it is set, xi-free conditions are dropped. The module docstring now explains who sets it and why.
• gen-rules.py calls rendered(res_dir, strip_xi=True). Its docstring now names the right key, and the generated header now says copy shows nf(𝑒), not nf(𝑒1), since copy's metavariable is 𝑒.
• New test test_strips_the_xi_free_condition_of_copy in .github/test_gen_rules.py. It fails without the fix and passes with it.

Checked locally:

• python3 -m pytest .github: 13 passed.
• ruff check .github: clean.
• bash .github/regen-rules.sh against the pinned phino 0.0.0.74: the fidelity lock still holds, and Rules.lean now has cond := "nf(𝑒)" for copy.

🤖 Generated with Claude Code

https://claude.ai/code/session_01XWY8yTGgWJ1HXoFjmLt3AZ

[yegor256]

rules-in-sync fails here, but this PR didn't cause it. The check has also failed on master since June: see run 27506805660 on 58aa773 and run 27184788483.

The log shows the cause. scripts/regen-rules.sh clones phino master and reads resources/*.yaml, but phino has moved its rules to resources/normalize/*.yaml. The script finds 0 rules and writes normalizationRules := [ ], so any committed Rules.lean counts as out of sync. The failure is deterministic, so re-running it won't help.

I don't know of an existing fix. The script needs to read resources/normalize/, but phino's rule set has also changed in substance: there are now 15 rules, including amiss, dca, dl, dotg and overa, and the patterns are different. Bringing those in is a separate decision, so it isn't part of this PR. This PR's Rules.lean was regenerated from phino 1f2fada, the commit the file on master was generated from.

---

Generated by Claude Code

[yegor256]

difftest also fails here, and this PR didn't cause it either. The diff only changes the display string RuleSpec.cond for copy and the generator script. It doesn't touch Step, the reducer or Difftest.lean. The last green run on master was on June 14 (run 27506805691). What has changed since then is phino-latest, which is now 0.0.137.

I reproduced it locally with that binary. It has two layers:

1. Input syntax. phino 0.0.137 no longer accepts the { e } program wrapper that lake exe difftest emits: Couldn't parse given phi expression … unexpected "{ ". scripts/difftest.sh sends phino's stderr to /dev/null, so each case just shows phino=[]. The fix is to strip the wrapper before piping, e.g. in scripts/difftest.sh:

   e=${input#\{ }; e=${e% \}}
   out=$(printf '%s\n' "$e" | phino rewrite --normalize --flat 2>/dev/null)

2. Semantic drift. With the wrapper stripped, 17 of the 20 cases pass. Three still differ because phino's rule set has changed (see the previous comment):
   • ⟦φ ↦ ∅⟧.y: phino gives ⟦ φ ↦ ∅, ρ ↦ ∅ ⟧.y, ours gives ⊥. phino no longer has the phi rule.
   • ⟦x ↦ ∅⟧(α1 ↦ Φ): phino gives ⊥, ours gives ⟦x ↦ ∅, ρ ↦ Φ⟧. phino's new amiss rule is the cause.
   • ⟦λ ⤍ Fn, x ↦ ∅⟧(α1 ↦ Φ): same as the previous case.

Layer 2 comes down to whether the proof's Step should follow phino's new rules, which is beyond what this PR is for. I haven't re-run the check, because the failure is deterministic against the current phino-latest.

---

Generated by Claude Code

[yegor256]

Update: my two comments above no longer apply. After merging master (#72: phino pinned to 0.0.0.74, rules-in-sync removed), every check is green on d8e4fb4, difftest included. The fix now lives in .github/phino_render.py. The PR description has the details.

---

Generated by Claude Code

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.