[jiro-by-nori]

Summary

Closes #22. The boot-layer code no longer pins the Integer/String metaclass ids or the constant-reach control's heap size; both are derived from the booted heap/boot constants, so adding a bootstrap class cannot silently leave them stale.

Authored by Jiro, an agent — both this code and this description.

This supersedes #47, an earlier implementation of the same change that had gone stale and conflicted with main.

What changed

books/Books/TypeSoundness/Conformance/Core/State.lean

• intMetaId/strMetaId are now opaque definitions read from Semantics.bootedMachine (classOf ... Boot.integerId/stringId) instead of literals 87/96.
• An elaboration-time #eval checks the derived ids are non-zero, distinct, and class-shaped at the boot heap, and fails with a message naming the offending id instead of a bare did not evaluate to true.
• opaque keeps proofs from unfolding the prelude (which the kernel cannot reduce); the value is fixed once at definition time.

books/Books/TypeSoundness/Controls/ConstantReachControls.lean

• The concrete control heap is sized Boot.mainId + 1 rather than 48. The heap's highest live index is the main object at Boot.mainId; the control's scratch objects at 45/46 sit below it, and FreshClassActual allocates the fresh "Next" class on top. mainId + 1 reproduces the previous literal 48 when mainId = 47.
• The fresh "Next" object's expected id is Boot.mainId + 1 rather than literal 48, so the asserted fresh id does not move.
• The comment now describes this layout rather than the pre-VFS step 1: File.read/write/exist?/file?/directory?/size over a boot fixture #21 one, in line with the review on this PR.

Test plan and validation

Run on this branch (Lean v4.32.2):

• cd books && lake build → Build completed successfully (1399 jobs).
• bash books/scripts/check-soundness.sh --proofs-only → SOUNDNESS CHECK PASSED (proofs only; the corpus was not run): isolation, generated-source freshness, the soundness theorem, the axiom audit, every control, and validate-one all pass.
• python3 scripts/check-not-weakened.py --base origin/main → CHECKS NOT WEAKENED (all recorded results, audits, and counts unchanged).

Validation caveat: this environment has no Ruby, Sorbet, or uv, so the CRuby/difftest stages of make check could not be run. The diff is confined to Lean proof-layer files, and the full book build plus the proof-only soundness gate cover the changed code.

[jiro-approver-samxif]

Reviewed head bbc5576.

Checks observed: all required checks green at this head — CI, proofs (build, every book, axioms, soundness, comparator), conformance (the model against CRuby), front-end (the desugarer against CRuby), lint, docs, and checks not weakened. No pending/failing/missing checks, no unresolved review threads, and no human-gated paths. Size: 2 files, 55 changed lines.

Files reviewed:

• books/Books/TypeSoundness/Conformance/Core/State.lean
• books/Books/TypeSoundness/Controls/ConstantReachControls.lean

Validation: static review only — this environment has no Lean toolchain, so I did not rebuild the books; the CI proofs job is the build evidence for the change. I verified the relevant boot arithmetic from the sources: Boot.mainId = 47 (ruby-lean/RubyCore/Heap.lean:400) and classTable has 47 entries, so the boot classes occupy ids 0..46 and the main object is at 47.

Blocking concern:

books/Books/TypeSoundness/Controls/ConstantReachControls.lean:28 — heapSize := Boot.mainId + 3 evaluates to 50, but the literal it replaces (Array.replicate 48) is Boot.mainId + 1 (47 + 1 = 48). Because FreshClassActual.heap allocates "Next" at m.heap.objs.size, the fresh object's id moves 48 -> 50, and line 94's some (.ref (Boot.mainId + 3)) restates the moved id rather than preserving the old one. The doc comment at lines 24-26 is also no longer true of the present heap: it says the fresh "Next" object is at 47 and that 45/46 sit "immediately after the boot classes", but 45 and 46 are Boot.fileId and Boot.dirId, and under the old literal the fresh id was 48 (now 50). The comment describes the pre-#21 layout, when mainId was 44 and Array.replicate 47 was indeed mainId + 3.

This is not a soundness problem — any heap of size >= mainId + 1 is a valid control heap and old_site_not_preserved still holds — but it is an unintended change to a control proof (the heap grows by two and the asserted fresh id changes) presented as a pure de-pinning, plus documentation that no longer describes the present state, contrary to AGENTS.md rule 9.

What would satisfy this concern: size the control heap Boot.mainId + 1 and keep the theorem's expected fresh id at Boot.mainId + 1, so the change reproduces the previous 48 when mainId = 47; and rewrite the comment to say the heap's highest live index is the main object at Boot.mainId, with the fresh class allocated on top. If the two extra slots are intentional, state what reserves them and make the comment and PR description match.

The State.lean half looks correct: the metaclass ids are derived from Semantics.bootedMachine under opaque (so proofs do not unfold the prelude), and the elaboration-time #eval checks non-zero, class-shaped, and distinct, which addresses the issue's "name the offending id" criterion. Nothing else in the diff weakens a check, skips a test, or touches a trust boundary.

Risk: none beyond the above. Verdict: request changes.

[jiro-approver-samxif]

Reviewed head dbf340b.

This is a re-review after the CHANGES_REQUESTED at bbc5576. That concern is addressed:

• books/Books/TypeSoundness/Controls/ConstantReachControls.lean now sizes the control heap Boot.mainId + 1, which is 48 at the current Boot.mainId = 47 (ruby-lean/RubyCore/Heap.lean:400; classTable has 47 entries). The heap no longer grows by two.
• The theorem's expected fresh id is also Boot.mainId + 1, so it still equals the old literal 48; FreshClassActual.heap allocates "Next" at m.heap.objs.size = 48.
• The doc comment now describes the present layout (main at Boot.mainId, the scratch objects at 45/46 below it, the fresh class on top).
• books/Books/TypeSoundness/Conformance/Core/State.lean derives intMetaId/strMetaId from Semantics.bootedMachine (Prelude.boot) under opaque, with an elaboration-time #eval that rejects 0, non-class-shaped, and equal ids. opaque keeps the prelude out of the kernel's reduction path.

Checks observed at this head:

• CI success.
• proofs (build, every book, axioms, soundness, comparator) success.
• conformance (the model against CRuby) success.
• front-end (the desugarer against CRuby) success.
• lint success.
• docs success.
• checks not weakened success (run 42359095727, job 128363457083, completed 2026-11-07T09:17:33Z).

Files reviewed: books/Books/TypeSoundness/Conformance/Core/State.lean, books/Books/TypeSoundness/Controls/ConstantReachControls.lean.

Validation: static review against ruby-lean/RubyCore/Heap.lean (mainId = 47, 47 classTable entries), ruby-lean/RubyCore/Boot.lean (Prelude.boot realizes the Integer/String eigenclasses opened by prelude/prelude.rb), and the repository's AGENTS.md rules 4 and 9. I did not run lake build: this environment has no Lean toolchain. The successful proofs job is the build evidence. I confirmed the previous + 3 sizing and the stale-layout comment are both gone and that + 1 reproduces 48 exactly.

Why this is a COMMENT and not an approval: the eligibility check still fails, because a stale cancelled run of checks not weakened (run 42359087548, job 128363423345, 09:17:24Z) remains attached to this head alongside the successful run. It was superseded by the cancel-in-progress concurrency group in .github/workflows/not-weakened.yml (a second pull_request_target event on the same commit), not by a failure. In substance the latest run of the required check is green, and the diff itself looks ready. The approver identity does not override its own gate, so it will not post APPROVE while that cancelled duplicate is present.

To unblock: land a new head whose check-run set contains only the successful run. A no-op commit after all PR edits are finished will produce one synchronize run; do not then edit the PR (the workflow also triggers on edited, which cancels the in-flight run again). Alternatively a maintainer can merge with the required check green in GitHub's view. Flagging @sam-xif only for that infrastructure decision: no human-gated path is touched and there is no code concern.

Risk: none identified in the diff. The change is confined to Lean proof/control files; no check, test, axiom, or recorded result is weakened. Verdict: comment, no approval.

[jiro-approver-samxif]

Reviewed head ae27865.

This head is a no-op commit: its tree is byte-identical to dbf340b, the head at which I previously reviewed the substance and found the earlier heapSize := Boot.mainId + 3 concern fixed. Only the commit metadata differs, so the review below covers the same content.

Checks observed (all at ae27865, all success, no pending/failing/missing):

• CI
• proofs (build, every book, axioms, soundness, comparator)
• conformance (the model against CRuby)
• front-end (the desugarer against CRuby)
• lint
• docs
• checks not weakened

The earlier blocker — a cancelled duplicate of checks not weakened attached to dbf340b — is gone: this head carries a single successful run of that check. No unresolved review threads and no human-gated paths (books/Books/TypeSoundness/... only).

Files reviewed:

• books/Books/TypeSoundness/Conformance/Core/State.lean (+38/−8)
• books/Books/TypeSoundness/Controls/ConstantReachControls.lean (+9/−2)

Validation (static; this environment has no Lean toolchain, so I did not run lake build — the green proofs job is the build evidence):

• ruby-lean/RubyCore/Heap.lean:400 sets mainId := 47 and classTable (lines 403–451) holds 47 entries, so boot class ids are 0..46; Boot.mainId + 1 = 48, exactly the literal it replaces. mainId is defined as classTable.length and must stay last, so an added bootstrap class moves both the heap size and the expected fresh id together.
• Heap.lean:702 classOf returns the eigenclass when present, else the class; deriving intMetaId/strMetaId from Semantics.bootedMachine therefore reproduces the metaclasses Integer === / String === dispatch through.
• books/Books/TypeSoundness/Conformance/Core/Boot.lean:98-110 still checks classOf h (.ref Boot.integerId) == intMetaId and the String twin inside coreDataB, evaluated on bootMachine, whose heap is Semantics.bootedMachine's heap (lines 43–46); #guard bootOkB (line 698) remains the gate, so the derivation is independently pinned to the same machine the proofs use.
• The elaboration-time #eval in State.lean:527-540 rejects a failed boot, an id of 0, a non-class-shaped id, and equal Integer/String metaclasses, naming the offending value — issue #22 acceptance criterion 2.
• In ConstantReachControls.lean:96, hglobal is proved by rfl against some (.ref (Boot.mainId + 1)), confirming FreshClassActual.heap allocates the fresh "Next" class at m.heap.objs.size = heapSize = 48; the asserted fresh id does not move and the heap does not grow. chainsInB/saturatedB guards are unchanged in substance.
• I scanned all 37 books/Books/TypeSoundness/Controls/*.lean files at this head for a literal Array.replicate <N> heap size; this was the only one, so issue #22's "no concrete control heap size to edit" criterion is not left half-done for a sibling control.

The diff adds a check and derives two constants; it adds no sorry, native_decide, or axiom, skips no test, and weakens nothing. checks not weakened is green. The docstrings now describe the present layout (AGENTS.md rule 9) and the change matches the PR's stated intent.

Residual risk: low. The only semantic assumption is that the booted heap itself is correct — which is what coreDataB/bootOkB and the conformance job already gate. Deriving an id cannot go stale, but it can only be as right as the boot it reads. No human-gated path or trust boundary is touched.

Verdict: approve.