[ColoCarletti]

…fs and a differential check against the prover

[MauroToscano]

/review-ai

[MauroToscano]

/ai-review

[claude]

Low (readability): label.len() gives the same seed for "LT" and "EQ" (both are length 2), so salting by label length does nothing here. It's harmless because the tables differ, but a fixed seed (or one passed in per table) would be clearer.

[claude]

Low (CI): Because the key ends in github.sha, every push saves a new .lake cache entry. That cache includes the Clean and CompPoly builds, so entries will pile up and push older caches (including the Rust ones) out of the repo's 10 GB cache quota. Consider keying only on toolchain + manifest, plus a hash of formal/**/*.lean if incremental builds matter.

[claude]

Review summary

No critical, high or medium issues. The Rust changes are test-only, apart from making Multiplicity::evaluate_with public. The differential harness in lean_diff.rs is sound:

• eval_program_base asserts that a constraint reads only the current row, so a constraint that also reads the next row fails loudly rather than being skipped.
• Unknown export nodes or channels panic.
• Column counts are asserted to match.
• Honest traces include a padding row.
• The expected LT differences (μ·(1−μ) vs. ARE_BYTES[μ,0]) are pinned exactly, so any further drift fails the test.

Minor notes (two are posted inline):

• Low: formal.yml cache key ends in github.sha, which saves a new cache entry on every run and adds pressure on the repo's cache quota.
• Low: the seed 0xC1EA_0000 ^ label.len() is the same for LT and EQ, so the label salt has no effect.
• Low: git diff --exit-code -- export does not catch untracked new export files. If a chip is added to Export.lean without committing its JSON, the check still passes. git status --porcelain -- export with an empty-output check would cover that.
• Low: Multiplicity::evaluate_with became pub only for this test. That's fine, but #[doc(hidden)] or a short note would make the intent clear.
• Note: BITWISE is modeled in Lean but is not exported or diff-checked like LT, EQ and SHIFT. Worth saying so in the README so readers don't assume it's covered.

🤖 Generated with Claude Code