Skip to content

NS-N prerequisite 1: the typed source-rewrite op and the owned Step-0 producer - #10134

Merged
gunbai-bot[bot] merged 4 commits into
mainfrom
session/warm-tern-69
Sep 3, 2026
Merged

gunbai-bot[bot] merged 4 commits into
mainfrom
session/warm-tern-69

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 2, 2026 •

Copy link
Copy Markdown
Contributor

SCORING: THIS IS CAPABILITY WORK WITH ZERO PREREQUISITE CREDIT. THE CANARY DOES NOT MOVE.

Stated at the top so nobody later cites this PR as Step 0 movement. Scored by the lane manager
(wise-badger-902) on exactly that basis: a PR that moves nothing may not DELAY Step 0, and the
stop rule does not say such a PR may not land. It lands as the two capabilities, not as an advance.

The frozen command was run on this branch and the receipt is byte-for-byte the ZERO, not the
successor:

prefix=[CanaryContractFrozen,SourceTreePinned,CompilerExecutablePinned,InputSubjectManifestPinned]
blocker=ApplyTypedImportStrip
entry=Step0SubjectNotEntered
observation=NoStep0Observation

PASS current_main_step0_canary_receipt_is_admitted here means the zero still holds. Receipt zero
is untouched: the three literals in test.claim.namespace_step0_canary_witness are unchanged from
#10117 (commit 20caf4e, tree a6a6e0a531, digest a89dfc88a9), and the contract, the classifier
and the subject-entry rule are unedited. Run locally on aarch64; BuildBuddy cannot execute the
canary (HostBudgetUnreadable), and nothing here reads a remote result as a canary result.

WHY IT CANNOT MOVE YET, WHICH IS PREREQUISITE 2

The producer observes the (path, content) vector it is HANDED, and nothing collects that vector
from the pinned tree
: there is no directory walk, glob or corpus enumeration anywhere in the
builtin registry, filesystem_read takes one named path, and tools.multi_module_compile_fixture
is in-memory only. So the manifest subject -- every parsed import statement in dag, src/v2 and
src/v1 at tree a6a6e0a531 -- has no producer.

A receipt naming that manifest over a hand-supplied two-file vector would be a lie the classifier
could not catch
: admit_namespace_step0_canary_receipt checks the tree PIN, not that the vector
IS the tree. That receipt is writable today and would have scored. It is not written here.

THE MEASURED FINDING THAT CHANGES WHAT STEP 0 IS

With every import removed, a kernel-typed two-module subject STILL COMPILES -- Bool needs no
import and the cross-module callee is recovered by bare-name resolution across the supplied pool.
This is reproduced under an ISOLATED fixture with no corpus pool, which is stronger than the
v2.lens.module_graph observation from #7908 because it removes the ambient-pool explanation.

"Strip the imports and see whether the compile exits 0" is the canonical shape named in
gunbc.recurring_failure_mode proxy_observation_mistaken_for_action_semantics (landed at
5e9f65a). This fixture is that class's discriminating instance, produced independently.
So the honest expectation for corpus-scale Step 0 is not a containment-compile refusal at all,
and the census the lane has been treating as the subject may be measuring the checker's absorbing
arm.
That row's evidence list is still empty; this fixture is available to it if the lane wants
the receipt attached, which is a separate change to a ledger this PR does not touch.


gunbc.namespace_step0_canary reports the Step 0 strip-entry canary blocked at
ApplyTypedImportStrip for two named missing capabilities: "a typed parse-level source
rewrite that removes one complete import statement" and "an owned Step-0 producer that
applies the rewrite and folds the resulting compile observation". This lands both, green
by execution.

THE REWRITE (std.import). One authority: a fold that consumes an ascending set of
parser-delimited spans once and rebuilds the source from the gaps between them, because
removing several statements is not removing one several times -- every removal shifts the
offsets of the ones after it. The singular case is that fold on a one-element list, not a
second implementation. It accepts only spans a parse produced and refuses, typed and
located, when the source at a span is not an import statement of the module the parse
named, when a span belongs to another file, when spans descend, and when a span leaves the
source. The parse observation deliberately does NOT carry the statement text: if the span
and the text were slices of one another, agreeing would be a tautology.

THE EXTENTS (v1.compiler.parse). An import node's span is the import keyword and its
ident_span is the module path, so where a statement STOPS is known only while its tokens
are being consumed. parse_import_statement_extents reuses the seed's own parse_import and
decides only where that production started and stopped, from the token stream's own
position before and after it -- there is no second grammar, and a rule corrected in
parse_import is reflected with no edit here. The trailing newlines parse_import consumes
are excluded: removing a statement must not also remove the blank line after it. The
opening ParseContext is now built by one extracted parse_context_for_tokens so this reading
enters the grammar under the same context the full reading does.

THE PRODUCER (gunbc.namespace_step0_strip_producer). It strips a supplied subject, compiles
the rewritten sources through tools.multi_module_compile_fixture, and folds what came back.
Every stage refuses rather than widens, and the arm that matters most is the one that looks
like success: a stripped subject that COMPILES has no blocking transition, and the canary's
receipt has no spelling for one, so the producer reports Step0ContainmentCompileCompleted
instead of fabricating a blocker. That arm is not hypothetical -- the witness measures it on
a kernel-typed pair whose imports bare-name resolution recovers anyway.

The receipt constructor is sealed to this producer's fold and takes the executed rewrite and
the compile's own cause as arguments; it is declared in the canary module because the
receipt is sole_constructor, and ownership is expressed by the caller seal. The fixture
constructors and this one are reachable from disjoint doors.

WHAT THIS DOES NOT CLAIM. Step 0 has not moved. The frozen contract, the classifier, the
subject-entry rule and the controls in test.claim.namespace_step0_canary_witness are
untouched, and no receipt is minted over the repository tree. The producer observes the
sources it is HANDED; that the handed vector is the whole of the tree the receipt names is
the caller's obligation, bound only by the canary's commit and tree pins. The next-rung
trigger is a capability that COLLECTS the subject from the pinned tree, so the vector and
the tree have one producer instead of two. Rebinding the baseline to a corpus-scale run
lands separately, as the freeze note requires.

The dag-to-v1 crossing is declared seed growth (+1 hand item, the interpreter encoder) at
gunbc.parsed_import_statement_bridge_seed_growth, with the same reachability reason and
dissolution trigger shape as the structural-observation bridge beside it.


🤖 Generated with Claude Code

Brian Searls and others added 4 commits September 2, 2026 22:09
… producer

gunbc.namespace_step0_canary reports the Step 0 strip-entry canary blocked at
ApplyTypedImportStrip for two named missing capabilities: "a typed parse-level source
rewrite that removes one complete import statement" and "an owned Step-0 producer that
applies the rewrite and folds the resulting compile observation". This lands both, green
by execution.

THE REWRITE (std.import). One authority: a fold that consumes an ascending set of
parser-delimited spans once and rebuilds the source from the gaps between them, because
removing several statements is not removing one several times -- every removal shifts the
offsets of the ones after it. The singular case is that fold on a one-element list, not a
second implementation. It accepts only spans a parse produced and refuses, typed and
located, when the source at a span is not an import statement of the module the parse
named, when a span belongs to another file, when spans descend, and when a span leaves the
source. The parse observation deliberately does NOT carry the statement text: if the span
and the text were slices of one another, agreeing would be a tautology.

THE EXTENTS (v1.compiler.parse). An import node's span is the `import` keyword and its
ident_span is the module path, so where a statement STOPS is known only while its tokens
are being consumed. parse_import_statement_extents reuses the seed's own parse_import and
decides only where that production started and stopped, from the token stream's own
position before and after it -- there is no second grammar, and a rule corrected in
parse_import is reflected with no edit here. The trailing newlines parse_import consumes
are excluded: removing a statement must not also remove the blank line after it. The
opening ParseContext is now built by one extracted parse_context_for_tokens so this reading
enters the grammar under the same context the full reading does.

THE PRODUCER (gunbc.namespace_step0_strip_producer). It strips a supplied subject, compiles
the rewritten sources through tools.multi_module_compile_fixture, and folds what came back.
Every stage refuses rather than widens, and the arm that matters most is the one that looks
like success: a stripped subject that COMPILES has no blocking transition, and the canary's
receipt has no spelling for one, so the producer reports Step0ContainmentCompileCompleted
instead of fabricating a blocker. That arm is not hypothetical -- the witness measures it on
a kernel-typed pair whose imports bare-name resolution recovers anyway.

The receipt constructor is sealed to this producer's fold and takes the executed rewrite and
the compile's own cause as arguments; it is declared in the canary module because the
receipt is sole_constructor, and ownership is expressed by the caller seal. The fixture
constructors and this one are reachable from disjoint doors.

WHAT THIS DOES NOT CLAIM. Step 0 has not moved. The frozen contract, the classifier, the
subject-entry rule and the controls in test.claim.namespace_step0_canary_witness are
untouched, and no receipt is minted over the repository tree. The producer observes the
sources it is HANDED; that the handed vector is the whole of the tree the receipt names is
the caller's obligation, bound only by the canary's commit and tree pins. The next-rung
trigger is a capability that COLLECTS the subject from the pinned tree, so the vector and
the tree have one producer instead of two. Rebinding the baseline to a corpus-scale run
lands separately, as the freeze note requires.

The dag-to-v1 crossing is declared seed growth (+1 hand item, the interpreter encoder) at
gunbc.parsed_import_statement_bridge_seed_growth, with the same reachability reason and
dissolution trigger shape as the structural-observation bridge beside it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…efusal carries a NonEmptyStr

Both notes were advisory on an APPROVE and both are worth taking.

compiler_program is no longer a literal in the producer. Which program was run and which
bytes it had are two halves of ONE observation about ONE dispatch, and spelling the first
half here made this module a second authority on it while the caller owned the second --
they could disagree with nothing to notice. It now travels beside
compiler_executable_sha256 as an argument, so both halves arrive from the caller that
performed the dispatch. This is the DESIGN section 3 interface/realization/policy split
applied to a receipt field rather than to a dispatch: not a correctness break as it stood,
but a policy fact sitting in a producer.

std.import ImportStatementParseRefused.cause and the producer's Step0SourceImportsNotParsed
cause are NonEmptyStr. Every producer of that cause in the tree emits a non-empty literal,
so the String typing was carrying an "empty cause is a possible value" state the classifier
had to trust producers not to write -- validation standing where construction was
available, and out of step with the discipline the receipt fields already use.

Executed after the change: all 12 witnesses in
test.claim.namespace_step0_strip_producer_witness still pass, including the two that drive
the producer to a minted receipt and the one that drives it to
Step0ContainmentCompileCompleted. std_import.rs is re-emitted from the changed .dag rather
than hand-patched.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…arsed_import_statements.rs

CI refused at `required-ci: regen` with `generated surface drift` on both files.
My hand-written stage0 mirrors were the error: stage0 `.rs` under
src/v1/stage0/src are MACHINE-REGENERATED by the regen gate
(`claim_executor --required-regen`), which re-emits the whole surface from
the `.dag` authority and compares it to what is committed. A hand-written
mirror of an emitted file is a second authority for the same fact (DESIGN
§3), and the gate is exactly the check that says so.

So the fix is to take the emitter's bytes, not to argue with them. The
drift was import-list contents and ordering, `heads_only: heads_only.clone()`
where I wrote `heads_only`, and the emitter dropping the `///` doc comments
I had added by hand. Every other emitted file in this PR
(std_import.rs, v1_compiler_infer_method.rs, lib.rs,
v1_interpreter_dispatch_generated.rs, emitted_population.rs) already
matched the candidate; v1_interpreter.rs is hand-carried seed and is
covered by the declared SeedGrowthJustification row.

Verified after the copy: the seed builds (`cargo build --release -p
v1-compiler --bin gunbc`), and all 12 witnesses in
test.claim.namespace_step0_strip_producer_witness are green by execution.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…8968)

Review 58968 was right that `starts_with(text, "import")` and
`string_contains(text, imported_module)` are substring predicates standing
where a token-level check belongs. They are not fail-open -- the span comes
from the parser and a mismatch is a typed refusal either way -- but a check
softer than the property it guards is a check that would not go red on the
case it exists for, and the two false positives are concrete:

  - `import xy { .. }` satisfies `string_contains` for module `x`, so the
    statement would have been cut out under a module path that does not
    exist in it;
  - a declaration whose name merely BEGINS with the keyword satisfies
    `starts_with`.

So the two predicates now read the span's text POSITIONALLY. The keyword
must occupy its own token (a whitespace character follows it), the module
path must be the exact run of bytes after the whitespace run, and the
character after it must come from an ALLOWLIST of delimiters -- an
unanticipated following byte refuses rather than widening.

Both of those false positives are now enrolled as discriminating REDs in
test.claim.namespace_step0_strip_producer_witness; each one was green under
the old predicates. All 14 witnesses are green by execution, and
std_import.rs is the regen gate's own emission.

Not taken: the same review's note on `ImportSpanDoesNotNameItsModule
.source_text: String`. §4c quarantines PROSE from program data; the
offending bytes at a refused span are the diagnostic's located evidence,
which is exactly what a fail-closed refusal is obligated to carry.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants