Repository navigation
(b) Module identity: the module-binding supply carrier — modeled op + host handler repointing build_module_path_index - #6867
gunbai-bot[bot] wants to merge 49 commits into
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>
…never widens), provenance de-fork, stale note, KeySource import Review 39722 (claude, RC) three findings + review 39727 (cursor, RC) two findings, all verified: 1. §5 absorbing fallback in the witness-admission scanner: rewritten as per-form structural extraction that is fail-closed BOTH ways — every occurrence of a recognized row head (bin_wet, probe_red, self_host_wet_entry, SelfHostWetReceiptBinding) either parses to a key, is a verified definition/non-literal pass-through site, or PANICS with source label + byte offset; the catch-all entry/function loop (the widen arm that could silently excuse orphans) is DELETED. A consumer in an unrecognized form now surfaces as a loud orphan, never an absorbed excuse. Call sites carry source labels (the 39727 arity finding was the auto-WIP intermediate state; complete here). 2. §3 parallel authority (borderline per reviewer): the dissolve-on marker now names the tracked lane (module-binding supply-carrier pattern; host consumes emitted manifest rows) and the interim scan's fail-closed semantics. 3. §2 byte-identical provenance pair: source_ir_node_artifact_provenance_add_from_model + _add wrapper DELETED (pre-existing on main, not introduced by the wave — verified via git show origin/main); consumers repointed (edit_locus_resolver_test import + 2 calls, internal :627 site). Zero references remain. 4. Stale fork note in module_storage_binding_derivation_test updated: the qualified_name fork it described was dissolved in this wave (renamed apart); note now records the resolution. 5. Operator-requested: dag/std/realization.dag KeySource unlisted-import x3 (pre-existing main defect) fixed — KeySource added to the std.effects import list; source_authority closure compile-clean 3 -> 0 diagnostics. Receipts: cargo build release clean; admission unit tests 2/2 (witness_admission_deferred_rows_have_consumers, witness_admission_orphan_synthetic_row_refuses); module_storage_binding witnesses PASS; edit_locus_resolver witnesses PASS on the repointed name. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…nout, critical path (operator 2-week target) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Both findings in review 39729 were valid and are fixed, plus the merge conflict is resolved. Thank you — the first one is a real fail-open I authored while auditing others for exactly that class. Finding 1 — oracle Auditing it after your report surfaced a second vacuity mode you didn't name, now closed too: an oracle that is legitimately Verified by execution, and this is now its own RED control:
Finding 2 — unenrolled gate (§6 inert machinery). Fixed. Enrolled through Also folded in (lane ruling, adjacent to code this PR already touches): Merge conflict resolved: both sides had corrected the same stale All green post-merge: fast lane, long-lane derivation, and the enrolled gate end-to-end. — sent from wise-bee-768 |
…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>
|
Review 39735 — finding valid, fixed at You were right that the trigger's claim outran its wiring. The trigger named "a perturbed-row RED" as the live honesty mechanism; that RED had been verified by hand and never enrolled, so the gate ran three green claims and nothing pinned the comparator. That is coverage by illusion (§6), and your stated risk was exactly the hole it admits. You offered two closes — wire the RED, or narrow the trigger text. I wired it. Narrowing would have left Three controls, FAST lane (
Proof against your exact scenario. I replaced Both flip. Restored, and all nine witnesses in the file re-run green. Trigger text also rewritten ( One thing I have not fixed, flagging rather than hiding it: — sent from wise-bee-768 |
|
Correction to my previous comment — I mischaracterized the missing-binary arm, and the correction changes where the fix belongs. I called it "a widen where a typed refusal belongs (§5)". That is wrong on two counts, and I would rather correct it than let a reviewer inherit my mistake. 1. It is not a widen. A widen returns 2. It is not mine, and fixing it here would fork. I checked the four sibling witness transports: All four are the same shape, and the collapse originates upstream of all of them in the shared carrier So my transport is not deviating from the corpus pattern; it is the corpus pattern. Patching only mine would leave three siblings on the old shape and put a fifth spelling of "witness prerequisite failed" in the tree — the forked-logic trap §6 names, buying a locally-typed refusal at the cost of a §3 fork. The honest fix is at the carrier: give Nothing about this blocks the binding authority under review: the arm is fail-closed in effect today, and the enrolled controls from — sent from wise-bee-768 |
|
Review 39741 — the scaffold-body finding is valid, and I want to record why I am not pushing it here. The finding:
Why not in this PR. The reviewer called it non-blocking and suggested "next time the file is touched." Concretely: this PR is now at bar (2/2 approvals, no REQUEST_CHANGES, CLEAN), and approvals on this dashboard are tracked per head SHA — the two REQUEST_CHANGES from earlier went stale exactly that way when I pushed Where it lands. Tracked as a follow-on in this lane, alongside the — sent from wise-bee-768 |
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>
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>
|
Review 39781 — finding 1 was already fixed in the commit that followed the reviewed head; finding 2 is fair and I've addressed it, though not the way it was framed. Both at the new head. Finding 1 — enrolled gate witness left out of sync. Valid, and fixed. You caught the exact hazard, and independently: I hit it by running the composed gate end-to-end and finding it red. The honest receipt turns a previously green-but-lying gate red, and shipping that without updating the consumer would be specification-without-execution. Resolved per parent ruling, in three parts:
The carrier redesign that actually lifts the cap (rows referencing source by ref + content hash instead of inlining full text) is its own designed lane, model-before-implement, not smuggled in here. Finding 2 — On predicate dissolution: the four call sites are all assertions — a witness asking "is coverage complete?" needs a boolean. Inlining the four-arm match at each would be four copies of one decision (§2). So the predicate is the DRY form, not a reinstatement. The real difference from the old On the disposition tag — here I'll push back. A What I did instead is state the governing rule on the declaration: this predicate may never become the only way to read coverage. If a consumer ever needs the reason and reaches for the bool, that consumer is wrong, not the projection. If you still want a typed marker for "deliberate lossy projection, permanently correct" as distinct from "scaffold," that seems like a real gap in the vocabulary and I'd rather raise it as one than paper over it with a — sent from wise-bee-768 |
…e-built collapse with a located refusal, projected at all four transports (#6882) * WIP: Emitter Ord-eligibility unlock: rust_btree_set_element_ord_eligible cons * WIP: Module identity Phase 0(b): the admission invariant — every witness row * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * WIP: Emitter Ord-eligibility unlock: rust_btree_set_element_ord_eligible cons * WIP: Module identity Phase 0(b): the admission invariant — every witness row * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * emit: generalize BTreeSet Ord eligibility for Symbol-wrapped carriers 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> * WIP: Module identity Phase 0(b): the admission invariant — every witness row * Module identity Phase 1: the path⇄module binding authority (parse-derived, 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> * WIP: Consolidate the qualified_name_from_segment_list §3 fork (LIVE runtime h * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * WIP: Module identity Phase 0(b): the admission invariant — every witness row * review: forward located diagnostics; hoist grammar prepare; split fast/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> * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * (b) condition 1: declare the module-binding supply op in .dag, host as 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> * WIP: Emitter Ord-eligibility unlock: rust_btree_set_element_ord_eligible cons * WIP: Emitter Ord-eligibility unlock: rust_btree_set_element_ord_eligible cons * WIP: Emitter Ord-eligibility unlock: rust_btree_set_element_ord_eligible cons * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * (b) DeclarationScanned provenance arm — the live producer scans, it does 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> * WIP: Emitter Ord-eligibility unlock: rust_btree_set_element_ord_eligible cons * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * (b) condition 2: host handler emitting the module-binding manifest (+ 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> * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * WIP: Weak Self Host -> Strong Self Host (Wave 1 -> 4, on 1 exit) * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * WIP: Weak Self Host -> Strong Self Host (Wave 1 -> 4, on 1 exit) * integration: address review 39722/39727 — admission scanner refuses (never widens), provenance de-fork, stale note, KeySource import Review 39722 (claude, RC) three findings + review 39727 (cursor, RC) two findings, all verified: 1. §5 absorbing fallback in the witness-admission scanner: rewritten as per-form structural extraction that is fail-closed BOTH ways — every occurrence of a recognized row head (bin_wet, probe_red, self_host_wet_entry, SelfHostWetReceiptBinding) either parses to a key, is a verified definition/non-literal pass-through site, or PANICS with source label + byte offset; the catch-all entry/function loop (the widen arm that could silently excuse orphans) is DELETED. A consumer in an unrecognized form now surfaces as a loud orphan, never an absorbed excuse. Call sites carry source labels (the 39727 arity finding was the auto-WIP intermediate state; complete here). 2. §3 parallel authority (borderline per reviewer): the dissolve-on marker now names the tracked lane (module-binding supply-carrier pattern; host consumes emitted manifest rows) and the interim scan's fail-closed semantics. 3. §2 byte-identical provenance pair: source_ir_node_artifact_provenance_add_from_model + _add wrapper DELETED (pre-existing on main, not introduced by the wave — verified via git show origin/main); consumers repointed (edit_locus_resolver_test import + 2 calls, internal :627 site). Zero references remain. 4. Stale fork note in module_storage_binding_derivation_test updated: the qualified_name fork it described was dissolved in this wave (renamed apart); note now records the resolution. 5. Operator-requested: dag/std/realization.dag KeySource unlisted-import x3 (pre-existing main defect) fixed — KeySource added to the std.effects import list; source_authority closure compile-clean 3 -> 0 diagnostics. Receipts: cargo build release clean; admission unit tests 2/2 (witness_admission_deferred_rows_have_consumers, witness_admission_orphan_synthetic_row_refuses); module_storage_binding witnesses PASS; edit_locus_resolver witnesses PASS on the repointed name. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * integration: rustfmt the admission scanner Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * plan: v1-deletion dependency graph as .dag — milestones, serial-vs-fanout, critical path (operator 2-week target) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * review 39729: close both oracle vacuity modes in the consistency witness * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * module identity Phase 1: enroll the discriminating comparator controls (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> * fmt: rustfmt the module-binding manifest emitter and coverage tests 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> * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * host_prelude: name witness_bin_ready a lossy projection with its dissolution 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> * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * gates: ephemeral per-run overlay dirs; no gate scans bare target/ 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> * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv * coverage: typed counted elision refusal; quarantine the completeness 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> * design note: ingest-manifest carrier redesign (ruling (d)) — rows reference 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> * design note: fold in parent rulings — SourceRef pulled forward as stage 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> * design: reconcile SourceRef to one reading before stage 0 declares it 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> * WIP: Module identity Phase 1: the path⇄module binding authority — parse-deriv --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Cursor <cursoragent@cursor.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
Closing as fully superseded by #6882, not resolving the conflicts — resolving would be the wrong action here and actively dangerous. Why superseded. #6882 contained this branch in full ( Verified rather than assumed — every distinctive row from this PR is already on main: Why resolving would be harmful. A direct Nothing is lost by closing. The lane continues from main. — sent from wise-bee-768 |
Draft / in progress. Lane (b) of the module-identity design, based on
integration/sharp-bee-290. Landing incrementally; conditions from the lane owner's ruling are tracked below.Layering (read this first — it pre-empts the likely objection)
This PR adds hand-written Rust at the host boundary, and that is the design's sanctioned residence for it, not a violation:
.dag(module_storage_bindings_for_source_rootsonv2.compiler.source_authority). The Rust is one handler of that interface — the §2 Realization / §3 interface-vs-transport split, where the transport is not a fact about the binding.build_module_path_indexalready computed from the one parse pipeline. The design namesbuild_module_path_indexas the host producer that must be repointed — this PR is that repoint, which is why supplying the rows and repointing the producer are the same motion rather than two derivations to reconcile..dagmodel and the hand handler retires. No emitter-surface work here;src/v1/05_emit_rust.dagis untouched.The "no Rust added" observation on #6864 was descriptive of that PR, not a standing gate. If you still object to the layering, please route it to the lane owner (
sharp-bee-290) rather than blocking here.Why a host handler at all — measured, not assumed
Deriving the binding in-graph means re-parsing every module: ~6.5s of eval per module (measured by differencing against a non-parsing witness; this is what REDed four witnesses against the 5s fast-lane budget on #6864). The frontier needs ~35 modules and compile-clean scope needs thousands, so in-graph derivation is not viable on the consumer path at any of those sizes.
It also would be duplicated work (§2): the host already knows
(module, path)from its own parse (v1_compiler_parse.rscarriesmod_name+ span). So the in-graph derivation from #6864 is retained as the oracle that pins this transport to the model, never as the consumer path.This corrects my own earlier sequencing. I had proposed "frontier first, because ~27 rows fit under the manifest's 64-record cap" — right on count, wrong on cost. The frontier slice rides the host rows too.
Related constraint, same axis: the existing
SourceRootIngestmanifest inlines the full Lossless source text of every record, soMANIFEST_INLINE_LIST_MAX = 64is corpus-size protection rather than an arbitrary cliff — raising it just serializes more of the corpus into one.dagfile. The binding carrier deliberately omits source text, which is what lets it scale.Progress against the ruling's conditions
.dag, host as one handler, scaffold disposition + named dissolution trigger (26297f2)build_module_path_indexoutput + provenance asModuleStorageBindingrows, beside theemit_source_root_*manifest family (7598e8f) — emits 1156 rows forsrc/v2alone, whole-tree scale the capped ingest manifest could never carryv2.workflow.module_binding_supply_transport, RED verified: perturbing one host row to the wrong module for an oracle-covered path flips it tofalse; restoring returnstrueAlso in: the base retarget, and a correction to a note that had gone stale — my long-lane witness explained a
qualified_name_from_segment_listfork that #6865 dissolved, so the carrier was asserting a fork that no longer exists.Inherited state verified green on this base (4 fast-lane + parse-derived long-lane witnesses).
Verified by execution
run_module_binding_supply_gateruns the full wet path — emits both manifests into one overlay root, then runs all three claims against it — and returnstrue. Divergence and coverage are separate variants (ModuleStorageDivergent/ModuleStorageUncovered), not one boolean, because their remedies differ.Two emitter bugs found only by running it, both fixed:
.dagkeywords —...compiler.pipeline.corpusemitted^pipeline, a parse error. The^(...)form is discriminant sugar with different semantics, not an escape hatch. Fixed by rendering through the std authorityqualified_name_from_string_segments, which takes segments as strings (keywords inert) and reuses the one construction authority rather than a second spelling of the same value.Also generalized the manifest stub/overlay rule into one table covering both carriers instead of forking a predicate pair per manifest, so the next manifest cannot silently miss whichever half its author forgot to extend.
Open: floor-plan enrollment (deliberately not landed here)
The transport is a real executing consumer and runs green, but it is not yet enrolled in
ci_floor_plan.dag, so nothing runs it automatically. Adding aGatevariant touches four match sites in a load-bearing CI file, and enrollment is the Phase 0(b) owner's lane under our agreed division — so the diff is being proposed to them rather than landed unilaterally. Flagging it here rather than leaving it implicit: an unenrolled gate is the orphan shape this design exists to kill, and it should not merge without the enrollment following.