[jiro-by-nori]

What this fixes

An unsoundness witness was in the typed fragment, and therefore in theorem_scope (issue #44).

escape-hatches/002.rb is Sorbet-accepted, and it reaches an uncaught NoMethodError:

sig { params(x: Integer).returns(String) }
def f(x)
  x.to_s
end

define_method(:f) { |x| x.no_such_method }

Fragment.lean's criterion 3 (D10) admits a method redefinition because the pre-ratchet checker used to discharge the obligation that the replacement conforms to the declaration it displaces. That checker was removed in 5ee6b034, so the admission stayed while the proof behind it did not: rubycore --fragment said in_fragment: true, and nothing downstream ever checked the displaced sig.

The change

scan now tracks the sig-annotated names declared so far in the current body — from def, def self., a visibility-wrapped def (private def), and the names attr_* generates (attr_writer declares name=, attr_accessor both) — and refuses a literal define_method/define_singleton_method whose target is one of them, reporting a redefinition violation.

Everything D10 admitted for a reason it still has stays admitted:

• a computed name (define_method(name)) stays in the fragment — nothing syntactic can match it;
• alias/alias_method/prepend keep D10's conditional admission;
• the sig wrapper lives in prelude.rb, not in the scanned program, so an annotated method's own wrapper is not refused.

The check only ever excludes, so it cannot turn a rejected program into an accepted one.

Fragment.lean's header no longer cites infer as the handler for a displaced declaration, and now names the per-body scope as the third known gap in criterion 3 (a sig in one class C body and a define_method in a reopened class C body are still not matched).

Measurements on the corpus

run_check over difftest/corpus/sorbet, before → after:

	before	after
in fragment	13	12
theorem_scope	6	5
unsoundness witnesses	8	8
witnesses inside the fragment	1 (escape-hatches/002.rb)	0

Every other program's classification is unchanged; no cell of the static-oracle two-by-two moved.

Tests

make difftest-test — 202 passed (201 before), coverage held.

difftest/tests/test_sorbet_check.py:

• test_no_unsoundness_witness_is_in_the_fragment asserts the property outright — witnesses & in_fragment == ∅ — instead of pinning escape-hatches/002.rb as a named exception;
• test_fragment_checker_classifies_the_hatches gains the block, explicit-Proc (define_method(:f, proc { … }), whose installed name is the first argument, not a one-element argument list) and singleton forms, plus both attr_* shapes;
• new test_fragment_checker_admits_a_non_displacing_define_method pins the other side: a fresh name and a computed name stay in the fragment.

Validation

Run locally on the branch, from a cold toolchain (Lean v4.32.2, CRuby 4.0.5):

make check              -> make check: ALL CHECKS PASSED
make check-not-weakened -> CHECKS NOT WEAKENED

Highlights:

• make lean, make books (1405 jobs), make metatheory — every proof book builds; the audited axioms are still propext, Classical.choice, Quot.sound;
• make soundness, make comparator — OK: the comparator accepts — statements match, axioms are Lean's three, the kernel replays the closure;
• make conformance — CRuby 4.0.5 over the 1287-program bootstraptest corpus: ran 1287, agree 1087, sut_unsupported, disagree 0, exactly the recorded baseline, and the regressions tier and tier3 agree;
• make difftest-test — 202 passed, COVERAGE OK -- the baseline holds;
• make gen-check, make lint, make docs — generated sources fresh, no lint finding, docs build.

No recorded result fell, no check or theorem was dropped, no sorry/native_decide/axiom/lint suppression/test skip was added.

Provenance

Authored by Jiro, an autonomous agent, including this description.

Closes #44