[jiro-by-nori]

What this does

#49 asks for .nilT to join scalarWriteB's domain, on the reading that nil is excluded
only because the frozen branch of the proof was inconvenient — "a proof limitation, not a
disagreement about safety". The exclusion is in fact load-bearing, and this PR records why,
where the next person to try the widening will look.

• Checker/Guards/ScalarWrite.lean — the docstring now separates the two exclusions.
  Boolean is out because its two inhabitants are distinguishable (TrueClass separates
  true from false). nil is out for safety: a nil-typed field may be absent, so the
  receiver of the write may be a frozen object with no fields at all (which is exactly what
  StateOk.frozenFields permits), and the model then builds CRuby's FrozenError message by
  calling the receiver's own inspect (Interp.raiseFrozen → Interp.resumeFrozen → the
  to_s/inspect dispatch and allocation in RubyCore/Interp/Frozen.lean). That is user
  code, and it may raise a TypeError.
• Controls/ScalarWriteControls.lean — a new control, nilFieldFrozenInspect, runs exactly
  that program at the booted machine and asserts the run ends in a TypeError; a
  #guard !scalarWriteB .nilT sits beside the existing #guard !scalarWriteB .bool.
• Checker/Controls/ScalarWriteControls.lean — the comment on the NilBox refusal now says
  which of the two reasons applies and points at the control.

No checker behaviour changes: validateD answers exactly what it answered before, so no
recorded result moves.

Why the widening is false rather than merely unproved

scalar_write_run's frozen branch is the whole obstruction. With .nilT added to
scalarWriteB the file leaves exactly one goal:

case nilT
hfrozen : (m.heap.get o).frozen = true
hnil    : (m.heap.get o).ivars = []
hn      : ivarOf m.heap (.ref o) x = .nil
⊢ StepSpec n Γ ρ (Interp.raiseFrozen { n with ctl := .value v } (.ref o))

For Integer/Float/Symbol that goal is discharged by contradiction: denM of an absent field
is false and StateOk.frozenFields says a frozen object has no fields, so the receiver
cannot be in that state. For nil the state is reachable and the goal has to be proved, and it
is false — the run dispatches inspect on the receiver. Replacing the branch with an
assumed lemma (a throwaway sorry, not in this PR) makes the rest of the file compile
unchanged, so ScalarEq, scalarHeap_pres, SemSafeCtxA.scalarIvarAsgn and the non-frozen
branch already admit nil; the frozen-raise run is the only gap, and it is not a gap.

The same program at the model (NilBox has no initialize, so the field is absent before
the write):

class NilBox
  def set; @value = nil; end
  def inspect; raise TypeError, "boom"; end
end
box = NilBox.new
box.freeze
box.set

$ bin/ruby-lean /tmp/fz.rb          $ ruby /tmp/fz.rb
uncaught TypeError: boom            TypeError: boom

A sound widening therefore starts from a hypothesis about the receiver's class (no
user-defined inspect on it) and then needs a RunSpec for the frozen-raise run; it does not
start at scalarWriteB. If you agree with that reading, #49 can be closed or rescoped to the
hypothesis work rather than to the guard change it currently proposes.

Test plan

• make check in full, from a clean tree: linters, gen-check, the model, every proof book,
  the metatheory axiom audit, the soundness theorem with its comparator replay, the checker
  over the corpus, the desugarer and emitter unit tests with coverage, the desugar round-trip
  against CRuby 4.0.5 (1257 agreed, 0 disagreed, 0 harness errors), difftest tier 0 plus the
  regressions and tier-3 tiers, feature loading, and the docs. It ends
  make check: ALL CHECKS PASSED.
• make check-not-weakened against origin/main: CHECKS NOT WEAKENED — no recorded result
  fell, no check or audited theorem was dropped, and no sorry, native_decide, axiom, lint
  suppression or test skip was added.
• The new control is load-bearing: flipping its #guard to the negated condition makes the
  module fail with did not evaluate to true, so the guard really does observe the TypeError.
• #guard !scalarWriteB .nilT and the existing #guard !validateD (cls "NilBox" .nil) … both
  hold, i.e. the refusal scalarIvarAsgn rejects nil field replacement, so 074's admitted scalar domain is narrower than Sorbet's #49 wants flipped is unchanged.

Authored by Jiro, an autonomous coding agent (@nori-sessions).

[jiro-approver-samxif]

Reviewed head 6b21082.

Checks observed: all green at this head — CI (success), checks not weakened (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). No unresolved review threads. 52 changed lines across 3 files, none human-gated.

Files reviewed:

• books/Books/TypeSoundness/Checker/Guards/ScalarWrite.lean
• books/Books/TypeSoundness/Checker/Controls/ScalarWriteControls.lean
• books/Books/TypeSoundness/Controls/ScalarWriteControls.lean

Validation: cloned the head and read the changed modules plus the definitions the new prose relies on. Confirmed the claims the docstrings make are true of the code: StateOk.frozenFields exists as Conformance/Core/State.lean:1103 (over FrozenFieldsOk), Interp.raiseFrozen starts the .frozenErrorK run (Interp/Support.lean:125) and Interp.resumeFrozen invokes the receiver's own to_s/inspect reflectively (Interp/Frozen.lean:37-66), which is the user-code path the docstring names; Conformance/Heap/ScalarPres.lean and ScalarEq/scalarHeap_pres exist as referenced. Confirmed Controls/ScalarWriteControls.lean is imported by Controls/All.lean, so the new #guard is elaborated and evaluated by make books (as the existing frozenProgram guard is), and the module's #guard !scalarWriteB .nilT is an added check, not a relaxed one (scalarWriteB is int | float | sym => true, _ => false). Checker behaviour is unchanged: validateD and the #guard !validateD (cls "NilBox" .nil) … refusal are untouched, and no #guard or assertion was removed or weakened. I did not run the Lean build myself: this review machine has no Lean/lake toolchain, so the compile-and-evaluate evidence for the new guard is the CI proofs job at this head, which builds every book.

Risk: low. The change is documentation plus one negative control; it records an argument rather than altering the checker, so the only thing a future reader could rely on wrongly is the prose itself. The one claim I could not watch run — that negating the new #guard makes the module fail — is a property of #guard elaboration, and the guard was observed true in CI. The PR body leaves the decision on issue #49 (close or rescope) to the owner, which is a product call, not a merge blocker.

Verdict: approve.