[SamMausberg]

Summary

compiler/check/facts.py, proofs/Cairn/Facts.lean and the audit in verify/elision.py now read a product the same way: two constants multiply on all three sides, and a product atom times a constant names nothing on any. Every guard the facts propose to leave out over such a product is now one Lean proves and the audit accepts, where before the audit refused those proposals and kept the guard. The Lean differential generates both shapes, and asks a ninth decision that only the two sides' exact terms decide.

Motivation

Part of #2, following #171. The work behind #181, which timed #171 and #173 on the GH200, found that facts.py:times folds a constant times a constant (2 * 3 is 6) and names a product atom times a constant ((k * 4) * 2 as the atom k*4*2), while Facts.lean's exact returns nothing for either, and tools/checks/differential_facts.py never generated either shape, so the comparison that ties the proof to the Python could not see the gap.

No wrong guard reached emitted code: the audit's own exact agreed with Lean, so it refused every proposal resting on either shape and kept the guard. But each such proposal became a refusal that the receipt counted under refused_discharges (x[2 * 3] in a view of 8, let q = n / (2 * 4) above x[k * 8], and if k * 4 * 2 < n { return x[k * 4 * 2]; } each had one), and the Python rule was claimed to be what Lean proves when it was not.

I extended Lean for the first shape and narrowed Python for the second. Folding two constants is sound and used beyond guards (check/places.py compares part bounds made of constants through facts.exact), so dropping it from Python would change which parts leases see as equal. Naming (k * 4) * 2 as the one atom k*8 would also be sound, and I tried it first, but the same term feeds the lane rule's window, which would then place out[b * 4 * 2 + j] in lane b's block. It refuses that today (E-PARALLEL-RACE), so accepting it is a language change and belongs in a change of its own.

Changes

• compiler (compiler/check/facts.py): times gives no term for a product atom times a constant; two constants still multiply.
• verify (verify/elision.py): the audit's exact multiplies two constants, as facts.py and Facts.lean do; it already gave no term for a product atom times a constant.
• proofs (proofs/Cairn/Facts.lean): exact multiplies two constants, and exact_sound and exact_mul, hence mul_sound, cover the case. No theorem statement changes; the certificates are unaffected (export_lean_certificates.py --check: up to date).
• tools (tools/checks/differential_facts.py): products of two constants and products of a product atom among the generated expressions and as the sides of a *; the quotient's multiple x5 * C written four ways; a ninth decision, a product minus itself.
• tools (tools/checks/differential_guards.py): divisors (2 * 4) and (2 * 128), and a multiple below a quotient sometimes written j * 1 * C.
• tests: test_differential_facts.py plants the two old readings in times and requires the comparison to report each; test_elision.py requires the three programs above to have no refused discharge, and plants two slips in times that must reach no emitted program; test_established.py pins the guards x[2 * 3] and the nested product keep.
• docs (docs/verification.md): the guard-elision section says how a product is read, and cites the new differential run.
• evidence (evidence/v1_2/facts/): the Lean differential, the emission identity and the guard differential of this change, in a new section of the README.

Behaviour and compatibility

No program is accepted or refused differently, and no diagnostic changes. tools/checks/emission_identity.py --normalize guards over 2,289 programs, against the compiler of fd64dd2 on the same programs: none changed otherwise, none emits more guards, and 4 emit fewer (16,071 guards in all to 16,066). Three are the tests added here; the fourth, in tests/language/test_layouts.py, loses the guard on 16 * 18 - 2. No example, std module or docs block changed. A program that writes (k * 4) * 2 gets no fact from it, as before in effect, since the audit refused every proposal that rested on one.

Testing

make lint                                                     # clean
python -m pytest -q tests -n 4 -p no:cacheprovider            # 6 failed, 6222 passed, 58 skipped
cd proofs && lake build && lake env lean Cairn/Audit.lean     # built; the Facts theorems use propext and Quot.sound only
python tools/checks/export_lean_certificates.py --check       # up to date
python tools/checks/differential_facts.py --count 20000       # agreed on 20,000 inputs
python tools/checks/differential_guards.py --programs 2000 --batch 50 --workers 3 --gcc --sanitize-gcc
python tools/checks/emission_identity.py compare RECORD --normalize guards   # RECORD taken with fd64dd2's compiler

All on the GH200 host (aarch64, Ubuntu 22.04, clang++ 14, g++ 11.4, Lean 4.34.0), shared with other agents' suites. The six failures are the g++ ThreadSanitizer tests that fail on this machine at main (GCC 11's libtsan fails a CHECK on this kernel). The guard differential agreed on 1,869 functions and 179,424 cases per compiler, clang++ and g++ both under AddressSanitizer and UndefinedBehaviorSanitizer. After merging main (4d495bf), lint and the touched test files (335 tests) passed again. The new tests fail against main's compiler where they should: the three programs above each have a refused discharge there, and x[2 * 3] keeps its index guard. Nothing ran on the GPU.

Evidence and claims

• Lean-checked: exact_sound, exact_mul and mul_sound over the model with two constants multiplied. The model is still transliterated, not extracted, and the differential samples the agreement: 20,000 inputs agreed (facts_differential_products.json), and the two old readings are each reported within 300.
• finite-tested and sanitizer-clean: 1,869 generated functions, 179,424 cases per compiler, built with the 4,592 discharged guards left out and with every guard, under clang++ and g++ with AddressSanitizer and UndefinedBehaviorSanitizer, gave the same value, trap or status in every case (guards_differential_products.json).
• That the facts in scope are true where they are cited is still checked by the audit at each site, not proved.

Performance

Not measured. Five guards go from the four programs above: three over constants, which the C++ compiler folds anyway, and in a test the multiply and the index of x[k * 8] below let q = n / (2 * 4).

Checklist

• The title is one plain sentence saying what is now true; it becomes the squash commit's subject
• Every behaviour added has a test, and every new refusal a rejection test naming its code (no refusal is added)
• The documentation is updated in the file that owns the subject, and its examples compile
• Generated files are current (make editors, make docs): nothing they generate from changed
• A language change carries everything AGENTS.md lists: not a language change; accepted programs and their meaning are unchanged
• No emojis, no attribution trailers, nothing unrelated to the change

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-28T19:35:54.490326Z	ddec270	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ddec270dfc

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Preserve lane windows that use nested product atoms

When a lane is guarded by b * 4 <= (b * 4) * 2 && (b * 4) * 2 < b * 4 + 4 plus the normal extent check, the parent compiler uses the b*4*2 term and those facts to show that out[(b * 4) * 2] lies in lane b's stride-4 block. Filtering the term here leaves facts.window without that lower bound, so this previously accepted, race-free write is now refused with E-PARALLEL-RACE. This is an accepted-program change despite the compatibility claim; preserve a representation for lane-window reasoning or add the required language-change coverage and documentation.

AGENTS.md reference: AGENTS.md:L128-L136

Useful? React with 👍 / 👎.