Repository navigation
host_prelude: typed witness-binary readiness — replace the Bool ensure-built collapse with a located refusal, projected at all four transports - #6882
Conversation
FormalNonterminal and FormalTerminal ({ identity: Symbol }) now pass
rust_btree_set_element_ord_eligible and receive Ord derives, unblocking
04_infer and program_partition self-emit cargo probes.
Co-authored-by: Cursor <cursoragent@cursor.com>
…ived, fail-closed)
Homes the path⇄module binding on v2.compiler.source_authority as a
DERIVED-at-parse fact per docs/plans/module-identity-storage-binding-design.md §2.
- ModuleStorageProvenance = ParsedFromSource { artifact, span_index }
| ProducedByBehavior { producer } — zero-file produced modules are now
representable honestly instead of being excluded.
- ModuleStorageBinding / ModuleStorageIndex, reusing QualifiedName, Artifact,
SourceRootRef and SpanIndex (no new nickname, §3).
- Both projections: file -> module and module -> storage.
- Scope is the LIVE 1:1 binding; many-to-many is a named deferral (§6).
§5 fail-closed repair in v2.compiler.program_assembly: the Rejected arm of
qualified_name_from_module_node kept the root and left the index UNCHANGED,
so a module whose name could not be derived went silently invisible to every
downstream lookup — an absorbing fallback in drop form, its frequency zeroed
by construction. It now refuses with the located diagnostic.
Witnesses (green by execution, REDs verified discriminating by perturbation):
derivation from parse; path projection; duplicate-module refuses; underivable
name refuses; produced module has no storage.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…t/long witness lanes
Three fixes from review + CI.
1. Located refusal (cursor/composer-2.5). The name-derivation Rejected arm
discarded the derivation's diagnostics and substituted a port-level
source_authority_diagnostic — satisfying "typed" while destroying "located"
(§5 requires both), contradicting this PR's own notes, and diverging from the
sibling arm in program_assembly which forwards d. It now forwards d unchanged,
so one failure yields one diagnostic regardless of entry point.
2. Grammar prepare hoisted above the fold, mirroring
program_assembly_prepare_once_note. The derivation called parse_module per
read, re-validating the grammar K times over a K-module ingest; it now
prepares once and uses parse_module_prepared. Empty ingest is guarded so it
never pays the prepare for zero reads. Same cost-shape defect the assembly
fold already documents (§6 always-fix).
3. Witness lanes split per the operator 5-second rule (CI EvalBudgetExceeded:
4 witnesses at ~5002ms). Measured by differencing against the non-parsing
witness, parse-derived eval is ~13s — inherently over the fast-lane budget
even after fix 2. Per gunbc.ci_layer_roots long_lane_exclusion_note ("fast
receipts stay discovered, execution proofs live in long/"), the parse-derived
proofs move to src/v2/test/claim/long/, and the fast lane keeps NEW witnesses
that exercise the §5 construction wall over hand-built rows at zero parse
cost: duplicate-module refusal, its accept control, and the produced/zero-file
arm. Duplicate detection keys on module identity independently of provenance,
which is why the wall is provable without a parse.
All eight witnesses green by execution across both lanes.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…s one handler Model before implement, per the parent ruling: the SHAPE of the binding-supply operation is declared on v2.compiler.source_authority; the host is one handler of it at the effect boundary, not a rival authority. module_storage_bindings_for_source_roots(source_roots) -> Outcome<ModuleStorageIndex> Inputs: source roots. Output: ModuleStorageBinding rows (module, path, provenance) and deliberately NO source text — the binding never needed file contents, only module <-> path. That is what makes this a different carrier from SourceRootIngest, whose witnesses inline the full Lossless source of every file and are therefore capped at corpus-protection scale (MANIFEST_INLINE_LIST_MAX=64). Why a host handler rather than in-graph derivation, measured: the in-graph derivation re-parses every module at ~6.5s of eval per module. Fine at ORACLE scale, impossible at consumer scale (frontier ~35 modules, compile-clean thousands). The host already knows (module, path) from its own parse, so re-deriving in-graph is duplicated work as well as slow. The in-graph derivation is retained as the ORACLE that pins the transport to the model, never as the consumer path. Scaffold disposition + named dissolution trigger declared on the producer: when host-effect emission lands, the handler is emitted from this model and the hand handler retires. No emitter-surface work here; 05_emit_rust.dag untouched. Conditions 2-4 (Rust handler serializing build_module_path_index, the consistency witness with its perturbed-row RED, reviewer framing) follow. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…oes not parse
Per the lane ruling: option (a) approved, (b) is its dissolution trigger, (c)
rejected.
The live host producer build_module_path_index derives the mapping via
extract_module_path (cli_run.rs:120-133) — a SUBSTRING SCAN of the first
non-blank, non-comment line beginning with "module ". It has no spans and no
parse ever ran for those rows. Emitting them as ParsedFromSource with a
synthesized span_index would fabricate parse provenance (§5) and defeat the
coproduct's whole job. Widening span_index to Optional was rejected: it collapses
parsed-but-spanless and never-parsed into one shape — the named "Option meaning
>2 things" failure mode.
ModuleStorageProvenance
= ParsedFromSource { artifact, span_index }
| DeclarationScanned { artifact } <- new
| ProducedByBehavior { producer }
Because the scan and the parser are different code paths they can DISAGREE. The
arm makes that visible instead of assumed away, and it gives the coming
host-vs-oracle consistency witness a real question to answer.
Dissolution trigger declared on the arm: when the host producer routes through
the real parse path (v1_compiler_parse.rs, which already carries mod_name + its
span), rows upgrade to ParsedFromSource with real spans and DeclarationScanned is
DELETED, not kept as a second way to say the same thing. Not started here — that
is bootstrap-path surgery needing its own measured lane.
Also: two fast-lane witnesses for the arm (scanned rows HAVE storage where
produced rows do not), the path->module lookup one verified discriminating by
perturbation — it originally asserted on the input binding rather than the
returned value, which proved Present but not correctness.
docs/plans/module-identity-storage-binding-design.md §2 corrected on the same
point: "derived at parse" is the end state, not what the live producer does.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
… committed stub) The host transport for the .dag-modeled op module_storage_bindings_for_source_roots. Carries zero independent policy: it serializes what build_module_path_index already derived — the one host producer the design says must be repointed — so supplying the rows and repointing the producer are a single motion rather than two derivations to reconcile. - emit_module_storage_binding_manifest (cli_run.rs), beside the emit_source_root_* family. Calls build_module_path_index PER SOURCE ROOT so each row records its own SourceRootRef, reusing the existing derivation instead of adding a second walker (a new walker would be the very fork this repoint removes). - Rows are DeclarationScanned, never ParsedFromSource — the producer scans, it does not parse. - Deterministic by construction: build_module_path_index returns a HashMap, so rows are sorted before emission (byte-identical manifests across runs on unchanged inputs). - Imports exactly the SourceRootRef constructors the rows reference, mirroring emit_source_root_ref_import (an unreferenced import is an unlisted-import error; a referenced-but-unimported one fails to resolve). - --emit-module-binding-manifest on discover_source_root_ingest. - Committed stub at src/v2/test/claim/workflow/host_module_binding_manifest.dag so consumers always resolve, same posture as the ingest manifest stub. Proven by execution: emits 1156 rows for src/v2 alone. That is the point of the separate carrier — it holds module <-> path + provenance and NO source text, so it is not bounded by the ingest manifest's corpus-protection inline cap (64), which exists because that manifest inlines the full source of every file. Whole-tree supply is therefore reachable here and was not there. Remaining before #6867 can flip ready: overlay exclusion for the new stub (the generated manifest and the committed stub both declare the module, which the module index must resolve the same way it does for the ingest manifest), and condition 3 — the consistency witness comparing host rows against the in-graph oracle, with its perturbed-row RED. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…nout, critical path (operator 2-week target) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…s (review 39735)
Review 39735 (REQUEST_CHANGES) found that the scaffold dissolution trigger on
module_storage_bindings_for_source_roots claimed the live honesty mechanism was
"the consistency witness ... with a perturbed-row RED", but only three GREEN
claims were wired. The perturbed RED had been verified by hand and never
enrolled — coverage by illusion (DESIGN.md §6), and the reviewer named the exact
failure it admits: module_storage_host_agrees_with_oracle could regress to
answering ModuleStorageAgrees unconditionally and the live witness would still
go green.
The reviewer offered two closes: wire the RED, or narrow the trigger text. Wired
the RED — narrowing would have left the comparator unpinned.
Three controls land in the FAST lane (src/v2/test/claim/module_storage_binding_test.dag,
zero parse cost, per-PR discovery) over hand-built rows:
module_storage_agreement_holds_when_host_matches_oracle (positive)
module_storage_agreement_reports_divergent_on_wrong_module (host resolves a
covered path to a DIFFERENT module -> ModuleStorageDivergent, path asserted)
module_storage_agreement_reports_uncovered_on_missing_row (host lacks the
row entirely -> ModuleStorageUncovered, path asserted)
Divergent and Uncovered are asserted as DISTINCT variants, not merged into one
false, because their remedies differ (§5 state-space conflation).
Proven discriminating by execution against the reviewer's own scenario: with
module_storage_host_agrees_with_oracle's body temporarily replaced by a constant
ModuleStorageAgrees, both negative controls flip to false. Restored and
re-verified green.
Trigger text on source_authority.dag:551 rewritten to name what is actually
enrolled — the live half (module_binding_host_consistency, wet cadence) and the
discriminating half (these controls, per-PR) — so the scaffold's claim and its
wiring cannot drift apart again.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
cargo fmt --all --check fails on cli_run.rs at 7c50e7f — the module-binding manifest emitter and the coverage_complete tests added in this PR were never run through rustfmt. This did not surface on #6867 because its base (integration/sharp-bee-290) does not run CI, so the PR reported checks: none. It surfaced only when the stacked follow-on branch opened against a base that does run the build job. Left alone, the breakage would have reached main when the integration branch merged — later, and attributed to the merge rather than to this change. Pure reflow: line wrapping and one trailing comma. `git diff -w` shows no token changes; behavior is identical. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…olution trigger Parent requirement before ready: the Bool projection used by the seven dag/tools self-host harnesses must declare itself a scaffold with a named trigger rather than read as a design choice. The note states what the projection buys (one named greppable collapse over one typed carrier, removable in one place) and what it does not (the diagnostic is still lost at those seven sites), names the five sites that match the typed value instead, and records the dissolve-on: convert the seven to typed matches on next touch or as its own change, then delete the fn. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Fixes a CI-breaking module-path collision introduced by the module-binding supply gate, and closes the class behind it. THE BUG: run_module_binding_supply_gate wrote a FIXED, never-cleaned target/module-binding-supply/ containing host_module_binding_manifest.dag. The sibling run_real_ingest_gate scans --source-root target RECURSIVELY, so that manifest collided with the committed stub of the same module and panicked the indexer: module-path collision: module 'v2.test.workflow.host_module_binding_manifest' is declared by both 'src/v2/test/claim/workflow/host_module_binding_manifest.dag' and 'target/module-binding-supply/host_module_binding_manifest.dag' One run DELAYED, which is what made it dangerous: on a fresh workspace the composed gate runs real_ingest BEFORE the supply gate creates the directory, so run 1 is green; the runners are persistent and target/ is gitignored, so the directory survives and run 2 panics. Found by running the composed gate end-to-end — compile-clean and green individual witnesses had both missed it. The enrollment was the point of the PR that introduced it, and I never ran it. THE CLASS: bare target/ as a source root was not deliberate. source_root_ingest was the corpus's ONLY bare-target source root, and it admitted the entire build tree as source purely to read back one manifest it had emitted there. Any tool writing a .dag under target/ recreates the collision. So both gates now emit into a per-run mktemp directory that is scanned and then removed unconditionally, mirroring compiler_closure_ingest_transport, which already solved this correctly. No gate scans bare target/ any more, so gate ORDER stops being load-bearing for correctness. The emitted manifest FILENAME is preserved deliberately: the host-side stub-supersession table keys on the manifest basename (cli_run.rs MANIFEST_STUB_OVERLAYS), so relocating the file cannot silently break supersession. Verified run-twice (the discriminating input for this class is the SECOND run in the same workspace): both gates green on run 1 and run 2, zero .dag left under target/ after each. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
# Conflicts: # dag/gunbc/v1_deletion_plan.dag # src/v2/compiler/source_authority.dag # src/v2/test/claim/long/module_storage_binding_derivation_test.dag # src/v2/test/claim/module_storage_binding_test.dag
…claim; scaffold stub refuses
Parent ruling (e)+(a)+(3) on the vacuous-gate finding.
WHAT WAS WRONG: the compiler-closure ingest manifest carries ZERO rows (91
reads against MANIFEST_INLINE_LIST_MAX=64, so the row list elides to Empty),
and main's receipt emitted produced_row_count = read_count with
coverage_complete = true over that Empty carrier. The gate witness asserting
complete coverage read 91 == 91 && true and passed. It had been vacuously green.
(e) TYPED COUNTED REFUSAL: coverage_complete: Bool becomes SourceRootCoverage,
a coproduct whose arms each carry only numbers their own producer knows:
SourceRootCoverageComplete
SourceRootManifestElided { read_count, cap } host emitter: a cap rejected the rows
SourceRootRowsMissing { read_count, produced_row_count } in-graph: rows lost, no cap
SourceRootManifestAbsent committed stub: nothing supplied yet
Four arms because the causes and remedies genuinely differ; collapsing them
would have forced the in-graph derivation to name a cap it does not have.
Verified by execution: the 91-read closure now emits
SourceRootManifestElided { read_count: 91, cap: 64 }, an under-cap root emits
SourceRootCoverageComplete.
(a) HONEST RECEIPT SHIPS. Fabrication does not survive a repair window.
(3) QUARANTINE: compiler_closure_scoped_ingest_module_count_ok_holds is
admitted to known_red_probe_entries with the required per-row diagnosis, owner
and dissolve-on. Its gate did NOT go vacuous — compiler_closure_ingest_receipt_
describes_carrier_holds replaces it as the live claim: the receipt must describe
the carrier that landed, whatever its size. That is falsifiable at any corpus
size and reds if the receipt drifts again, rather than restating something
already true.
ALSO, since the seam was open (reviews 39741, 39773): the
module_storage_bindings_for_source_roots scaffold body now REFUSES with a
located diagnostic instead of self-recursing. The inert_lens siblings keep the
self-call correctly — they ARE registered in interpreter dispatch so their
bodies are unreachable; this one is not registered, so its body was genuinely
reachable and would have hung.
Two pre-existing unlisted-import defects fixed because they blocked compiling
the touched closures: Symbol in the closure test, KeySource in host_effect.dag.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
# Conflicts: # src/v2/workflow/module_binding_supply_transport.dag # src/v2/workflow/source_root_ingest_transport.dag
…erence source, not inline it Design note only; no code lands from it. Parent ruling (d), 2026-07-19, model-before-implement. Frames the measured defect (91-read compiler closure against a 64-row inline cap, carrier Empty), rejects the three obvious remedies with reasons (raise the cap, shrink the closure, emit a prefix — the last is worse than eliding, being a partial answer wearing the shape of a complete one), and proposes rows carrying SourceRef + ContentHash so row size stops tracking file size. Names the consequence rather than burying it: reading through a ref is a live read, so ingest consumers flip SubstrateInputsOnly -> ReadsLiveTree and lose affected-set selection eligibility. That is a real trade, not a free win — a correct answer that runs too often beats a fabricated one that runs cheaply — and the content hash is what can eventually restore selection, which is the argument for putting it on the row from the start. Five stages each with a trigger; stage 3's acceptance test is the already- quarantined completeness witness greening by itself, which is the counted un-quarantine event this lane registered. Four open questions for review, the sharpest being whether this SourceRef is the same one as the Phase-3 effect-boundary type (it must be, or it is a fork) and whether the ref names a path or a module. Linked from the module-identity design so it is not an orphan doc. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ge 0, ref names the storage realization Q1: same type as the Phase-3 effect boundary, and this lane owns that phase, so there was no external dependency to wait on. Type declaration pulled forward to a new stage 0 (declaration only, not enforcement), homed with the storage-binding authority, established as the single authority BEFORE it has two consumers. Q2: the ref names the storage realization (path + source root + ContentHash), not a module and not a coproduct. The manifest is a host-boundary artifact about files the host read, and only host boundaries project paths — so path-shaped is correct exactly there, with the module binding joined rather than fused. Raises a consequence that is NOT yet settled: the parent design's §3 describes the boundary SourceRef as 'module reference, or an explicit typed path', which admits a module-shaped ref and contradicts the uniform storage-shaped ruling. Two readings of one type name, and one must go before stage 0 declares it — otherwise the fork is minted at the moment of declaration, inside the very type introduced to prevent forks. Also: hermeticity flip confirmed separable (named in stage 3's trigger; these rows join an existing never-predict-skip class rather than minting one), and DecodeFidelity on ref+hash rows confirmed required. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The Q2 ruling makes SourceRef uniformly storage-shaped (path + source root + ContentHash, module identity joined not fused). The module-identity design §3 still described it as 'module reference, or an explicit typed path', which admits a module-shaped ref. Two readings of one type name would have minted a §3 fork at the moment of declaration, inside the type introduced to prevent forks. §3 now carries the uniform storage-shaped reading with the module-shaped reading explicitly withdrawn, and the carrier note records the reconciliation rather than leaving a dangling question. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
Scope note, flagged by me rather than left for a reviewer to trip over. This PR reached bar (2/2) at Why they rode along: this branch is the module-identity lane's working branch and the note is that lane's next deliverable, so it landed where I was standing. In hindsight it should have gone to its own branch, precisely so a PR at bar didn't get reset by work unrelated to it. Recording that as my error rather than quietly re-collecting approvals. I'm not moving them off now — reverting and re-landing would cost another reset and more churn than it saves, and the earlier reviews already read the bundled module-identity work in this PR as coherent. But the reviewable surface of this PR is still exactly what it was: the For anyone re-reviewing: the two doc files are — sent from wise-bee-768 |
Follow-on authorized by sharp-bee-290 after #6867 reached bar. Converts the shared witness-binary readiness carrier from a
Boolcollapse to a typed, located refusal.Why
witness_bin_ensure_built_typedreturnedBooldespite its name, and consumers collapsed every prerequisite failure toelse { false }. So "binary absent", "build failed", "build succeeded but produced nothing", and "artifact is a zero-byte stub" were indistinguishable at every call site.Precisely what this was not: a widen. The arm returned
falseand the gate failed, so the line stopped. What was missing was the location, not the stop. (I originally mischaracterized it as a widen on #6867 and corrected that there.) Gate outcome is unchanged on every path — every non-Ready state still fails the gate. This buys diagnosis, not permission.The displaced cost — the flake caught itself, mid-review
This is not a hypothetical. While verifying this PR, the new probe caught the sccache exit-0-no-binary flake live:
Four minutes, exit 0, no artifact. Rebuilt with
RUSTC_WRAPPERunset: same command, 19,672,328-byte binary. Diagnosis confirmed.The
test -fline is theIsFileprobe this PR adds — the old code only rantest -x. Under the old shape this entire sequence collapsed to onefalse, indistinguishable from "the corruption probe legitimately failed". I initially mistook it for exactly that, and only established otherwise by checking out the pre-change branch and re-running. Under the new carrier it isWitnessBinArtifactAbsent { path }— a build that claims success and delivers nothing, named as such at the path it was expected.That is the displaced cost: the diagnosis I paid a branch-switch for is now free at every call site.
The carrier
The three-way probe is honest about what the shell can actually observe:
IsFileseparates absent from present,IsExecutableseparates a present non-executable file from a runnable one,IsNonEmptyseparates the zero-byte stub. No arm claims a distinction the probes cannot make.Scope correction — 11 callers, not 4
The authorized scope named four transports. The real caller set is eleven; when a carrier changes shape the caller set is discovered by the compiler, not by the brief. Stopping at four would have left seven siblings on the old spelling and broken them.
build_step_transportmatchon the typed value — located refusal where diagnosis livesdag/toolsself-host harnesseswitness_bin_readyhelperThose seven still collapse to
Bool. That is a known lossy projection, approved as staged, and it now carries a note naming it a scaffold with its dissolution trigger (convert the seven to typed matches on next touch or as its own change, then delete the fn). What it buys: one named, greppable collapse over one typed carrier, removable in one place. What it does not: recover the diagnostic at those seven sites.Verification
witness_bin_artifact_readinessto a constantWitnessBinReadyflips all three refusal arms tofalse(the Ready arm correctly staystrue). Restored and re-verified green.claim_executoris present, and cannot be flaky from ordering —claim_executoris the floor executor that runs the batch, so it necessarily exists before any witness in it executes. The red I hit was sccache, not enrollment.BuildFailedis deliberately unprobed — staging it needs a failing cargo build costing minutes. Recorded in a note rather than silently omitted.CI caveat
Based on
integration/sharp-bee-290, which does not run CI — so this PR inherits thechecks: nonefail-open surfaced during #6867 (a PR there can reachready=truewithout a single gate running; accepted by the parent, infra fix routed to the operator). Compensating control run locally:cargo fmt --all --checkclean (touches no.rs) and compile-clean across all 11 closures.Stacking
Cut from
session/wise-bee-768-b(#6867) rather than bareintegration/sharp-bee-290, becausemodule_binding_supply_transport.dag— the fourth transport — exists only in un-captured #6867. Until #6867 is captured this diff shows the stack; read only the top commits.Coupling
stern-lark-430's chain B witness-realization kernel consumes this carrier so it does not mint a second spelling of ensure-built verification.
🤖 Generated with Claude Code