[jiro-by-nori]

Summary

Fixes #55. Authored by Jiro, an autonomous agent (Nori sessions) on behalf of @sam-xif.

Checker.Static.NativeInstanceNames is a hand-maintained copy of the model's instance selectors (crubyMethodNames) — the checker may not import RubyCore, so the list is duplicated rather than read. Conformance/Names/NativePrefix.lean proved only one direction of that duplication:

every name in crubyMethodNames appears in nativeInstanceNames

so a missing name broke the build, but an extra name — one the model no longer defines — was never checked. A re-folded or shrunken crubyMethodNames therefore left the checker declining selectors that are not native, shrinking the checker's fragment, with nothing to notice.

What changed

books/Books/TypeSoundness/Conformance/Names/NativePrefix.lean:

• missingNativeInstanceNames — model names the copy lacks (the direction instance_covered already catches, now with a readable failure).
• extraNativeInstanceNames — copy names the model does not define (the direction that was silent; issue #55).
• Two #guards assert both are empty, so a drift fails the build at a line whose message names the direction; #eval missingNativeInstanceNames / #eval extraNativeInstanceNames prints the offending selectors. This is nativeInstanceNames is hand-maintained against a generated source of truth and can drift silently #55's Option B: the assertions are #eval-style checks over the difference as data, so neither an overcount nor an undercount can pass.
• import Lean supplies the #guard command. books/scripts/check-isolation.sh already permits import Lean in the checker, and this file is in Conformance/, so no layering rule is touched.
• The kernel-checked instance_covered is unchanged: it is what nativeInstanceFreeB_sound consumes, and it remains the load-bearing kernel fact. The new guards are the diagnostic surface for the direction a kernel decide cannot name (its failure prints as a pretty-printer recursion error, naming neither selector nor class).
• Cost: none measurable. NativePrefix.lean builds in 59s with and without the guards (the decide +kernel in instance_covered dominates, and the guards evaluate in well under a second).

books/Books/TypeSoundness/Checker/Static/NativeInstanceNames.lean gains a one-paragraph header note saying both directions are checked.

No name is added, removed or reordered: the two sets are equal today (570 names each), so this PR moves no verdict, no baseline and no recorded result.

Test plan

The failure mode is the deliverable, so both drift directions were injected into the data file and the build re-run on this branch:

Injected drift	Result
extra name zz_bogus_native appended to nativeInstanceNames	NativePrefix.lean:33:0: Expression extraNativeInstanceNames.isEmpty did not evaluate to true, and #eval extraNativeInstanceNames prints ["zz_bogus_native"]
"value?" deleted from nativeInstanceNames	NativePrefix.lean:37:0: Expression missingNativeInstanceNames.isEmpty did not evaluate to true, with the old instance_covered failure alongside it
none (the committed state)	builds; both guards pass; #eval answers []

How it was validated

Command	Result
cd books && lake build (this is make books)	Build completed successfully (1399 jobs)
make soundness's proof stages (books/scripts/check-soundness.sh --proofs-only)	SOUNDNESS CHECK PASSED (proofs only; the corpus was not run)
make metatheory (books/scripts/check-metatheory.sh)	OK: the metatheory builds; every theorem above rests on propext, Classical.choice and Quot.sound only; the booted heap satisfies the assumptions the proofs make about it
books/scripts/check-isolation.sh	OK: the checker imports only itself and Json; the model imports nothing from books/
make check-not-weakened	CHECKS NOT WEAKENED

Not run locally, and left to CI: everything that needs CRuby 4.0.5, RuboCop or uv-based tooling (make conformance, make difftest-test, make gen-check, make lint, make desugar-*, make comparator). This machine has no Ruby and no C toolchain, so Ruby 4.0.5 could not be built or fetched; the change is Lean-only (no desugarer, difftest, workflow, Makefile, script or recorded baseline is touched), so those stages exercise nothing it modifies.

Follow-up (not in this PR)

#55's other option — generating nativeInstanceNames from crubyMethodNames so a FOLD change needs no hand-editing — needs a new generator plus make gen / make gen-check wiring in the Makefile, which .github/CODEOWNERS reserves for owner review. Suggest tracking that as its own change once the silent-drift hole is closed, which this PR does.

[jiro-approver-samxif]

Reviewed head 7ce8d95.

Checks observed (all success): CI, checks not weakened, proofs (build, every book, axioms, soundness, comparator), front-end (the desugarer against CRuby), conformance (the model against CRuby), docs, lint. No unresolved review threads. 36 changed lines across 2 files, no human-gated path.

Files reviewed:

• books/Books/TypeSoundness/Conformance/Names/NativePrefix.lean
• books/Books/TypeSoundness/Checker/Static/NativeInstanceNames.lean

Validation:

• Independent parse of both Lean lists (Python, at this head): the copy holds 570 unique names and crubyMethodNames holds 570 unique method names over 39 classes; missing-from-copy is empty and extra-in-copy is empty. So both #guards are true today, the verdict is unchanged, and the new direction is the one that was silent.
• Confirmed extraNativeInstanceNames uses "defined by any class" membership, which is the same relation instance_covered uses, so direction 2 cannot be stricter or looser than direction 1.
• Confirmed import Lean is not restricted here: books/scripts/check-isolation.sh only constrains Books/TypeSoundness/Checker/, and five other book modules already import Lean.
• Not run locally: cd books && lake build. This machine has no Lean toolchain (the pinned leanprover/lean4:v4.32.2 is not installed) and no root, so the build and the guard evaluation are CI's, which the proofs job covers.

Risk: none material. One wording nit, not blocking: NativeInstanceNames.lean now says NativePrefix.lean "kernel-checks both directions", but direction 2 is a #guard (elaboration-time evaluation), not a kernel proof; direction 1 stays the kernel fact instance_covered that nativeInstanceFreeB_sound consumes. Worth tightening in a later edit so an auditor does not overstate what is kernel-verified.

Verdict: approve.