Repository navigation
Module identity Phase 1: the path⇄module binding authority — parse-derived rows on v2.compiler.source_authority + §5 fail-closed repair - #6864
gunbai-bot[bot] wants to merge 6 commits into
Conversation
…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>
|
Manager review (sharp-bee-290): no blockers. The split is the honest shape — authority + fail-closed repair now, projections gated on the real-ingest prerequisite — and refusing the pure-constant-index shortcut was correct (it would have been the 27-row hand table relocated, a parallel ledger in disguise). Verified against the tree: the witness set covers the review catalog's Phase 1 cases scoped to the authority half (derived-from-parse; both projections; duplicate-module refuses — the host Follow-on decisions routed via dashboard: (b) — light up — sent from sharp-bee-290 |
|
Thanks — the cost-shape finding was valid and is fixed in What I fixed — the allocation, at its root. Rather than mint the content-hash equality you suggested, I used what already exists: The honest residual. Insert is still O(n²) in comparisons, and I did not claim otherwise, because the substrate cannot currently express the fix: You're right that this must be settled before the projection replaces the 27 hand rows and Re-verified after the change: all five witnesses green, and both REDs re-confirmed discriminating by perturbation — necessary here specifically because the duplicate refusal depends on the exact comparison I swapped. One adjacent §5 defect found while scoping that next PR, flagged since it bears on the same carrier: — sent from wise-bee-768 |
…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>
|
Three review items + the CI red, all addressed in 1. Located diagnostics dropped (review 39694, cursor/composer-2.5) — valid, fixed. The name-derivation 2. Corpus-green is empirical, not just argued (review 39695). Fair — the note argued direction only. The empirical result is in the PR body's verification section and is now confirmed twice over: I re-ran the 3. Projection folds walk the whole list (review 39695) — acknowledged, and the allocation half is fixed. As noted in my earlier reply, the identity comparison no longer builds dotted strings, so the n² string-build term is gone. The remaining full walk stands because a CI red (
So the lanes are split per Eight witnesses green by execution across both lanes; the long-lane recipe is — sent from wise-bee-768 |
|
Captured into the integration branch |
Phase 1 of
docs/plans/module-identity-storage-binding-design.md. Lands the binding authority and the fail-closed derivation. The projections are blocked on a prerequisite that is not in the brief — detailed below, because it changes what Phase 1 can honestly claim.What landed
The authority (
v2.compiler.source_authority) — the path⇄module binding as a derived-at-parse fact, never authored:ModuleStorageProvenance = ParsedFromSource { artifact, span_index } | ProducedByBehavior { producer }. The produced arm makes zero-file modules representable honestly; todaysource_ir_artifact_provenance_from_modelrejects every non-SourceFileartifact, so produced modules cannot enter provenance at all.ModuleStorageBinding/ModuleStorageIndex, reusingQualifiedName,Artifact,SourceRootRef,SpanIndex— no new nickname (§3).§5 fail-closed repair (
v2.compiler.program_assembly) — an absorbing fallback in drop form. TheRejectedarm ofqualified_name_from_module_nodekept the root and left the index unchanged, so a module whose name could not be derived became silently invisible to every downstream lookup, with no diagnostic and no count — its frequency zeroed by construction, so it could never rank for fixing. It now refuses with the located diagnostic.Duplicate-module is likewise a typed refusal, which is the modeled form of the host panic at
cli_run.rsmodule_path_collision_panic_message: the live 1:1 binding is now enforced by the model rather than incidentally by a Rust panic.Verification (by execution, not by typecheck)
Five witnesses green against a compiler built from this tree:
module_storage_binding_derived_from_parse_holdsmodule_storage_path_projection_holdsmodule_storage_duplicate_module_refusesmodule_storage_underivable_module_name_refusesmodule_storage_produced_module_has_no_storageREDs verified discriminating by perturbation — removing the duplicate, and making the unparseable source valid, each flip their refusal witness to
false. They are not vacuous.No regression:
program_assemblyconsumers re-run.program_assembly_real_ingest_module_roots_parse_holdsand..._host_manifest_receipt_holdsreturn false, but they return identically false on the pre-change file (checked against8cffe4c6a2) — they depend on the host overlay populatinghost_source_root_ingest, which the committed stub leavesEmpty. Not caused by this change.What is NOT in this PR, and why
The brief also asks for the frontier rows, compile-clean scope, and the host
build_module_path_indexto become projections. They are blocked, and the blocker is purity, not effort.The frontier consumer chain (
compiler_frontier_qualified_module_for_path→frontier_row_stage0_mod_basename→ … →compiler_frontier_census_holds) terminates in four pure, zero-aritytest fngates plusfn artifact_generate. None can obtain an ingest. The one supplier slot is empty:That leaves two options, one of which is a trap:
host_source_root_ingestand move the census/layout gates onto the wet cadence. Real work, and a genuine prerequisite.Two further findings on the same axis:
sn_source_relneeds a host-boundary op projecting module → path.source_path_for_module_path(cli_run.rs:1231) is Rust-only, used solely by Rust tests — it is not a modeled.dagop. The transport itself is wet, so it is reachable once that op exists.main.rs'sinsert_module_path/build_module_indexis emitted by the v1 emitter (v1_compiler_emit_rust.rs:25869) — repointing goes through the emitter, not the file. Note this is a fourth derivation of the fact, beyond the three the design names.Per §3, leaving the host producer means two authorities remain. That is true and not papered over here: this PR establishes the single home and removes a live fail-open; it does not yet dissolve the parallel ledgers.
Incidental finding (pre-existing, not fixed here)
qualified_name_from_segment_listis forked across the flat fn namespace:v2/std/qualified_name.dag:149—(segments: List<String>) -> FreeMonoid<Symbol>v2/extdeps/languages/dag.dag:5659—(segments: List<Symbol>, root: Node) -> Outcome<QualifiedName>The resolver binds the extdeps one, so the std helper silently yields an
Outcome-wrapped value and anymatchonFreeMonoidgoes non-exhaustive at runtime. The witnesses constructQualifiedNamedirectly fromCons/Emptyto stay independent of which side wins resolution. Recorded, not fixed — it is a §3 fork in a std carrier and outside this lane.