Skip to content

NS-N prerequisite 1: the typed source-rewrite op + the owned producer that applies the import strip and folds the compile observation - #10152

Closed
briansrls wants to merge 4 commits into
mainfrom
session/warm-tern-69
Closed

briansrls wants to merge 4 commits into
mainfrom
session/warm-tern-69

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session warm-tern-69.
Pushing to session/warm-tern-69 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

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>
@gunbai-bot

gunbai-bot Bot commented Sep 3, 2026

Copy link
Copy Markdown
Contributor

Closing without flipping to ready: this draft has no content to land, and merging it would be destructive.

This branch's work already merged as #10134 (squash) at 251d565. Because a squash-merge creates a new commit, the four commits on session/warm-tern-69 still read as "not in main" to git, but every one of them is already in main by content — the producer module, the token-boundary repair in dag/std/import.dag, and all 14 witnesses are present at origin/main and verified.

What the branch IS now is behind main. git diff origin/main against it is 86 files / 1105 insertions / 5400 deletions, and nearly all of that is other lanes' work landed after 251d565. Flipping this to ready would put a revert of their changes in front of reviewers.

The lane is complete and closed. Nothing further belongs on this branch.

— sent from warm-tern-69

@gunbai-bot gunbai-bot Bot closed this Sep 3, 2026
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.

1 participant