[afflom]

What it does

First part of PR 2 of the stage 4 plan on #91, stacked on PR 1 (#224). Not the core runtime yet (RustRuntime, SP-22, RB-16 are blocked on the proof-surface finding below).

• SP-23 RustSyntax.Machine gains nine constructors: checkedNatAdd, checkedNatMul, checkedIntAdd, checkedIntSub, checkedIntMul, checkedIntNeg, checkedIntQuot (each Some of the calculus primitive's value, or None where the primitive overflows) and natSub, natQuot (total, the primitive's value). RustSemantics gains machineOptional and runMachine reads it. Reason (corrects the plan on [v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91): Machine.checkedAdd u64 accepts only Value.u64, and the runtime's nat_*/int_* compute on Value.nat/Value.int; and a body cannot observe abort, so nat_add can only return Err(Overflow) if the machine hands it None.
• rust::ast::Machine mirrors them (print, arity, width) and the certificate-B term builder writes them; the RB-15 harness covers them (106 functions now).
• SPEC §17.17 states twenty-six machine primitives and records the decision to write width families out (no ItemDef.family).
• Register 429 on this draft (SP-23 is the +1; the maintainer assigns the final count).

Measured

• conformance_sp_13 (all 13 library modules, pinned Lean 4.32.1, over the regenerated modules including the changed body of runMachine): passes, 400 s. 0 library repairs.
• conformance_sp_23: 18 claims evaluated by Lean, 4 wrong statements refused; two plants caught (VERIFICATION.md). conformance_sp_21, conformance_sp_18, conformance_rb_15: pass.
• fmt, clippy -D warnings, validate-model, validate-spec-links (429), check-test-inventory (757), the bdd meta-gate: clean.

Not run / left for the wave

Records bound to the compiler-semantics ID (rust_renderer, locks, goldens, production export, compiler/expected), check-calculus, full just vv, other hosts, repro, honesty. As on #224.

---

Generated by Claude Code

[afflom]

Subtle hazard in close_forward_references (668c2e9) without _callees ballast

We checked 668c2e949 against Lean 4.32.1's Lean/Util/CollectAxioms.lean:

1. What close_forward_references does:

   • It computes the transitive closure of row.axioms, so R6.__fits_76._unsafe_rec (and __fits_106._unsafe_rec, __fits_147._unsafe_rec) all pin ["propext"].

2. Why close_forward_references alone will fail in the opposite direction (depends on [], its policy pins ["propext"]) whenever PHashMap visits __fits_106._unsafe_rec first (e.g. on main's hash C8a84cfe657fcf5f4681430ed44252172):

   • In bootstrap/expected/verify/preserve/audit.txt on main, Lean's #print axioms prints:

     'LexLeanPreserve.C8a84cfe657fcf5f4681430ed44252172.R6.__fits_76._unsafe_rec' does not depend on any axioms
     'LexLeanPreserve.C8a84cfe657fcf5f4681430ed44252172.R6.__fits_106._unsafe_rec' depends on axioms: [propext]
     'LexLeanPreserve.C8a84cfe657fcf5f4681430ed44252172.R6.__fits_147._unsafe_rec' depends on axioms: [propext]
     

   • Why does Lean print does not depend on any axioms for R6.__fits_76._unsafe_rec ~1/3 of the time?
     Because in Lean/Util/CollectAxioms.lean:133-141, exportedAxiomsExt computes the .olean's exported axiom table by iterating env.checked.get.constants.foldStage2 (a PHashMap Name ConstantInfo keyed by Name.hash) with a shared CollectAxioms.State:
     • Whenever Name.hash orders __fits_106._unsafe_rec before __fits_76._unsafe_rec in the PHashMap, collect starts at 106, sets the cycle sentinel seen[106] := #[] (CollectAxioms.lean:53), and recurses into 76.
     • 76's own body only mentions 106._unsafe_rec (none of 76's own constants carry propext). When 76 looks up 106, it hits the in-progress sentinel seen[106] = #[]!
     • So 76 finishes with result = #[] and caches seen[76] := #[] in the .olean!
     • Then when foldStage2 later visits 76, collectAndGet immediately returns the cached seen[76] = #[]!

3. How boundary.rs:990-1043 solved this for __valid_k._unsafe_rec:

   • Look at the doc comment and implementation in crates/lexlean/src/production/certificate/data_a/boundary.rs:990-1043:

     // The records call one another, and Lean computes the axioms of a
     // definition in a cycle with a cache that a call still in progress cuts
     // short: which record sees the axioms of a callee that only another
     // record names depends on the order the declarations are visited in. So
     // that every record's axioms are the same whatever that order is, each
     // names (in a `let` the code generator drops) every callee outside the
     // group that brings axioms, so each record sees them directly.

   • Because each member of the mutual _unsafe_rec group binds let _callees := ... referencing the external axiom-bearing constants of the group (or in structural.rs:283-297, binding a _callees let over the external axiom-bearing constants mentioned anywhere in direct_minors), Lean's CollectAxioms sees propext directly on 76._unsafe_rec without traversing through 106._unsafe_rec, AND push_row sees propext directly on 76._unsafe_rec! That makes both Lean's .olean export and Certificate A's policy 100% invariant to the certificate hash.

[afflom]

Maintainer: landed on release/v0.4 by #248 (merge commit 9796067, the #91 stage-4 stack regenerated on one compiler-semantics identity, full gate green on 677e88d). Closing by hand, since release-line merges do not auto-close.

---

Generated by Claude Code