Repository navigation
XL-1 deliverable 1: derived effect demand — and no host effect observed on the compiler's compile path (a lower bound, not a zero) - #9669
Merged
Conversation
…transport, and find that the compiler's compile path demands no host effect at all XL-1's own sequencing rule is derive, disposition, then implement. This is the derive-and-disposition half. It implements no transport, and the measurement is why: the population it was going to build them for is not what it looked like. WHAT THE FIRST MEASUREMENT SAID AND WHY IT WAS WRONG. Censusing the v1_rt bridge callees present in the emitted closure of the v2 compiler entry found seven host operations across nine call sites, and that number was read as the compile path's effect demand. It is not. Presence in the emitted tree is OCCUPANCY; the demand is call-reachability from the entry, and reading one as the other is the class this repository already names. The corrected instrument is a call-graph reachability walk over the same emitted tree, and it reaches NONE of the nine sites while spanning 2376 of 5159 emitted functions across 90 modules. The nine sites' only callers are lens, census and test consumers that sit in the tree by import occupancy -- the same class v2.compiler.00_compile door_roster_tree_grain_note records having de-enrolled a lens for. THE WALK OVER-APPROXIMATES ON PURPOSE, because the cheap version would have been unsound in exactly the mechanism under test: the compile door dispatches its lens gates as STORED FUNCTION VALUES, which emit as bare identifiers with no call parentheses, so an extractor keyed on call syntax would miss precisely the edge that could carry a lens into the compile path. Every bare identifier reference is an edge, including from file-scope initialisers, and the positive control is that the walk does reach all six enrolled lens gates through that edge. Two further controls: every target is reachable from its own owning module, so the extraction is not silently broken, and planting a target as a root does reach it. The first root set was EMPTY and returned a vacuous NONE -- the entry module emits as v2_compiler_compile.rs, not v2_compiler_00_compile.rs -- which is recorded rather than quietly fixed, because it had the shape of a pass and the content of nothing. WHAT LANDS. A demand census keyed on (entry module, operation identity, execution mode, producer origin). Mode is carried in the KEY rather than split across dispositions: the two native dispositions differ only along std.execution_mode, which already owns that axis and has a third arm a flat enum could not spell. The census refuses in three directions -- a reachable demand no row disposes, a row naming a demand nothing reaches, and a row claiming a native realization the realization population does not contain. The third is the load-bearing one: a disposition CANNOT be made true by editing it, only by a realization landing. Completeness is structural, never an empty list. PopulationUnmeasured and PopulationMeasuredComplete both carry zero rows today and answer the promotion gate oppositely, which is a distinction a bare List cannot make and a note beside it cannot enforce. PrimitiveExecutionSemantics is kept strictly apart from EffectOperationDisposition, because an operation can reach the host through its CURRENT realization while its answer does not require external state, and those have opposite remedies. Of the seven operations: filesystem_read is NativeHostObservation and earns a transport; the six fact producers are Unclassified, blocking, on whether lens execution binds a corpus snapshot. Both flattering arms were declined -- BoundCompilerInput would assert a bound input nobody has shown, and NativeHostObservation would commit XL-1 to six live-tree transports for operations whose compile-path demand is zero. The two instruments are JOINED rather than blurred: the modeled reachability walk is the semantic producer, the emitted-Rust census is the target-realization falsifier, and their disagreement directions are kept apart because they are not the same emergency. Realized-only means the emitted program reaches a boundary the model never predicted, so its grant and receipt were designed for a smaller program than the one that runs. A receipt binds source revision, entry, emitted member identities, roster digest, call-site identities, operation identities and WHICH producer. Its member count is derived from the carried identities, which is the direct repair for this change's own 174-versus-175 discrepancy: both figures were correct answers to different questions (174 counted only .rs, 175 counted every member including Cargo.toml) and neither said which question it had answered. MEASURED, all on 6447dd4: compile origin none; execute origin emit_host_run_transport and its cached variant, both at the single call site run_host_process_admitted; bootstrap origin none; all eight minimal entrypoints none, several with root sets of one to six functions and therefore weak evidence. emit_host_native_cache_evict is occupancy-only. The required-test origin is still being measured over a SOUND candidate superset -- 443 of 2051 test entries whose import closure reaches one of the 93 modules containing a host-op call site -- and is declared PopulationUnmeasured until it completes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…he corrected spelling unable to return silently src/v2/compiler/00_compile.dag declares `module v2.compiler.compile`. The numeric prefix is a filename ordering convention and is not part of the module name, so the authored v2.compiler.00_compile named nothing. THE ERROR SURVIVED BEING LOOKED AT, which is the part worth recording. A reachability walk seeded on the path-derived spelling has an EMPTY root set, so it answers NONE for every question -- the shape of a pass with the content of nothing. That vacuous answer was produced, noticed, and repaired IN THE WALK by reading the emitted filename v2_compiler_compile.rs, and the data row that carried the same wrong spelling was still not corrected, because nothing joined the two. The row was also DEAD DATA: no witness read it and nothing in its own module consumed it, so it could carry a false value indefinitely. It is now asserted by effect_demand_witness_compiler_entry_identity_is_the_declared_module, which pins the declared spelling and makes the path-derived one a red rather than a silence. The residual is stated rather than closed: this is still a COPIED name with nothing joining it to the declaration it quotes, so it rots if the module is renamed. The next rung is a derived binding; until then the discriminating check is that a walk seeded on this identity has a non-empty root set. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
Contributor
Author
Mutation receipt — completeExecuted on a linux/aarch64 host at branch head, over the landing bytes. 17 witnesses × 8 passes = 136 runs.
The receipt is per-arm rather than whole-file on purpose. A mutation that reds every probe proves only that the file was consulted. Each mutation here reds a distinct, predictable subset and leaves the rest green, so the split says which probe covers which mechanism:
Supplementary receipt — the module-identity controlSeparate pass over the same landing bytes, for the control added in Run separately rather than folded into the main receipt because the main one had already started; a receipt taken against different bytes than the ones that land is the failure mode the byte-restore control exists to catch, so it gets its own pass rather than an assumption that the arm was unaffected. Still outstandingThe required-test origin is measuring now — 443 sound candidates, and it is declared |
…authoring the fact it derives Two lanes reported different seam populations -- 14 and 36 -- and the disagreement was about SUBJECT, not about rule. XL-0's 36 unioned two predicates: 5 rows from the wall's own emitted refusals, which are authoritative, and 31 from a regex matching any emitted function whose body is a single runtime-bridge call, which never tested self-call at all. A superset check read as a detector. The tell was structural rather than numeric: tightening the predicate left 14 unchanged with no near-misses, and the next-looser one jumped to 698 ordinary recursions, so nothing in the neighbourhood produced 36. XL-0 retracted; both lanes now derive 14 with identical membership. SeamStanding carries that census at identity grain, and two distinctions it would have been easy to flatten. Standing is keyed on the PROJECTED PRIMITIVE, never the declaration name, and seam_realization_for takes no declaration argument so the wrong key has no spelling -- empty_map_primitive_delegate is realized only via the empty_map primitive whose bridge is rc_empty_map, and declaration-name keying reports it unrealized, which is the defect that made a wall refuse a realized seam for a day. And the 11 unrealized seams do not share one rung: 5 were refused by the wall inside the v2 compiler's emitted closure, which is executing evidence, while 6 are derived from the roster and registry but never exercised. Collapsing them would report the derived six at the executed five's rung. The roster first carried an authored realization column beside the derived one, so one fact was writable in two places and a row could claim a realization its projection did not resolve to. The mutation receipt found it: a fault that made the derivation resolve an unrostered projection left the roster-level law green, which is the tell that a check was validating authored data rather than testing a derivation. The column is deleted; SeamStanding carries the projection and the registry answers. SeamRuntimeBinding is a separate type from EffectRealizationKey deliberately -- the demand-side key carries an ExecutionMode, and no authority states whether a bridge binding is wet or hermetically replayed, so borrowing it would have forced every row to invent a mode. Evidence: 4 planted faults, 0 compile errors in every arm, byte restore exact. Mutation B now reddens both unrostered witnesses where it previously reddened one, which is the test the repair was staked on. Mutation D reddened nothing, exposing that the three authored bridge identities had no consuming witness -- green by construction, carrying no information -- so registry_binds_each_realized_seam_to_its_cited_bridge now asserts each cited bridge against the registry, grounded in the external census rather than read back from the tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…nct and carries its revision
Compiler-generation promotion is owned by one lane, and effect_demand_promotion_admitted
crossed that boundary by name and by scope: a reader could take its true for a generation
flip. It now decides only what it decides -- whether XL-1's effect-demand evidence is
admissible as one conjunct of a promotion that lane composes -- and says so in its type.
EffectDemandEvidenceAdmitted | EffectDemandEvidenceRefused { conjunct } replaces the Bool,
because eleven distinct deficits collapsed into one false told a consumer nothing about
which measurement to repair; the four refusal witnesses now assert the conjunct by name.
Both arms carry source_revision. The consumer is another lane's generation receipt, which
cross-checks the revision this evidence was measured over against the generation it is
deciding; an admitted arm without a revision is a bare token pairable with any generation.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…population, at claim identity grain, for XL-5's cutover disposition Scheduler standing (FloorPlanned / FloorDeclinedLongModule / FloorDeclinedCostDebt) is what the required floor decided; it is NOT a cutover disposition, which XL-5 owns. 8450 claims across 1145 candidate entries from the full-tree floor run 33242663070; 588 declined across 117 modules. Digest 8f7b9bb846bdac2c over the body rows. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
A committed TSV of a measurement is the output of an instrument standing where the instrument should be named (DESIGN 6), and a second representation of what required_floor_site_disposition already derives (DESIGN 3). The entry point that re-derives it lands in its place. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…reaching closure × the floor's own standing The committed TSV this replaces was the output of an instrument standing where the instrument should be named (DESIGN section 6), and a second representation of what required_floor_site_disposition already derives (DESIGN section 3). This module is the instrument. Three authorities, none re-coined: the discovery walk is v2.workflow.floor_discovery_producer's, the closure is v2.lens.module_graph's dependency_closure over the same import-and-reference edge family claim_scope_for walks, and the standing is v2.workflow.required_floor's required_floor_site_disposition, called with the dotted module.function identity the cost-debt roster keys on. Every way the population can be wrong is a refusal arm, not a skip: an entry no declaration fact names, two rows with one identity, an empty population. The one genuine skip -- an entry whose closure reaches no seam -- is named as such. The closure walk is memoized per entry rather than per claim, because the floor discovers several claims per entry and the closure is a fact about the entry. The digest covers identity and standing in producer order, so two derivations over one tree agree and a consumer joins by identity. The live shell states its own population basis: no substrate producer of OwnedDataDeclRecord exists, so Bool-valued owned-data witnesses are absent from the live population and the result says so in owned_data_records_supplied. The default entry binds the floor's own roots and gunbc.ci_layer_roots.witness_exclusion_substrings through an import, so the shell and the Rust floor cannot drift on exclusions without a refusal. Witnesses run over a controlled six-module fixture, never the live tree: transitive reach, exclusion-without-refusal, each standing arm from the real prefix rosters (and the cost-debt arm from a policy-rostered identity), the three refusals, count partition, and digest sensitivity. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…, and two emit-route shapes in the floor join Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…ed, so two lanes join on one key Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…eId as the join key; the gate refuses on tree mismatch, and two commits over one tree admit Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…eplace target had the arms reordered and matched nothing), and the deletion that followed removed the only definition Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…of Present; rename the binder Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 30, 2026
) as typed evidence on the candidate's GenerationReceipt GenerationReceipt { requirements, producer, subject, build, conformance_evidence: ConformanceAdmission, fallback }, joined on source_tree; the request carries it and the sole constructor records it. Seven causes name each way the evidence can fail to be about THIS candidate: refused, other tree, off the promoted route, omitted-arm failed open / unobserved / judged over another generation, and a candidate receipt whose requirements disagree with the parent binding. Fixtures derive every admission through admit_conformance + omitted_arm_triple, so the battery cannot author an admitted arm. effect_evidence stays absent by name until #9669's carrier is on main (the HOLD's reason). 34/34 green remote. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A37WtqPwoQ1vj55d8yQMty
…re and DeclinedDiscoveryExcluded get a name, a counter and a place in the partition, so the exhaustiveness checker admits the join again Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
… own name and counter in the floor-standing join rather than folding into planned Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
…endency_closure lifts its walk into dependency_closure_over_adjacency and calls it, and the floor-standing join threads one adjacency through its fold — the live digest was rebuilding a 48k-edge map ~1,100 times Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VYW8LjeQuf519vq8mkGYAz
briansrls
marked this pull request as ready for review
August 30, 2026 14:16
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3ca686b9ad
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+774
to
+775
| else if length(xs: agreement.modeled_only) != 0 { EffectDemandEvidenceRefused { source_revision: left.source_revision, source_tree: left.source_tree, conjunct: ^modeled_only_nonempty } } | ||
| else if length(xs: agreement.realized_only) != 0 { EffectDemandEvidenceRefused { source_revision: left.source_revision, source_tree: left.source_tree, conjunct: ^realized_only_nonempty } } |
There was a problem hiding this comment.
When the two receipts contain different operation_identities, a caller can still supply a DemandAgreement with both disagreement lists empty. This gate validates only the receipts' emitted-member lists and never establishes that agreement was derived from either receipt, so every conjunct can pass and return EffectDemandEvidenceAdmitted despite an unmodeled host boundary. Derive the agreement from receipt-bound demand identities or carry verifiable provenance tying it to these receipts.
Useful? React with 👍 / 👎.
Comment on lines
+187
to
+189
| (demand.operation.slug == realization.operation.slug) | ||
| && execution_mode_eq(left: demand.mode, right: realization.mode) | ||
| } |
There was a problem hiding this comment.
When multiple runtimes are present, a realization registered for any runtime satisfies this predicate because runtime_identity is ignored. Consequently a demand can be marked proven by a bridge that the program does not link, contradicting the runtime-qualified realization key and potentially admitting a nonexistent native implementation. Include the demand's selected runtime in this comparison.
Useful? React with 👍 / 👎.
| observed: List<EffectDemandKey>, | ||
| realized: List<EffectRealizationKey> | ||
| ) -> EffectDemandCensus { | ||
| let rostered_keys = effect_demand_roster_keys(roster: roster) |
There was a problem hiding this comment.
When the roster contains multiple rows for the same full key, the census treats them as one membership while evaluating their dispositions independently. For example, duplicate NativeV2 and RetiredWithConsumer rows pass all refusal lists when the key is observed and realized, so effect_demand_acceptance_holds can return true even though the promised one-row/one-disposition invariant is violated. Detect duplicate roster keys explicitly instead of flattening them into this membership list.
Useful? React with 👍 / 👎.
Comment on lines
+269
to
+271
| let path_to_module = floor_join_path_to_module(nodes: nodes) | ||
| let seam_paths = floor_join_seam_paths(nodes: nodes, seam_modules: seam_modules) | ||
| let adjacency = build_dependency_adjacency(edges: edges, nodes: nodes) |
There was a problem hiding this comment.
When nodes omits one of the requested seam_modules but still contains another reachable seam, floor_join_seam_paths silently drops the missing module and the function can return FloorStandingJoined. Every claim reachable only through that omitted seam then disappears from the census and digest. Verify that every distinct seam module resolves to a declaration path and return a typed refusal if any are absent.
Useful? React with 👍 / 👎.
…IGN 4c, review 57607): every data <name>_note: String in effect_demand, effect_demand_floor_join and their two test modules becomes the annotation attached to the declaration it explains; no String row whose sole purpose is commentary remains Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MyDy8UXuqZwahQfg2QXzRJ
Contributor
Author
|
Review 57607 (dashboard artifact Verified count: 38 Executed evidence on the annotated tree (BuildBuddy, Draft state: the PR was flipped out of draft by the dashboard at the review; it is back in draft per the XL-N hold (READY only after the binding rerun on the XL-0B freeze tree). |
briansrls
marked this pull request as ready for review
August 31, 2026 16:58
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 6d85a6ef77
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+305
to
+307
| if effect_demand_key_in(key: key, keys: rostered_keys) { | ||
| acc | ||
| } else { Cons { head: DemandWithoutRow { key: key }, tail: acc } } |
There was a problem hiding this comment.
When an observed key is matched by a RetiredWithConsumer row, this branch removes it from undispositioned; the stale-row check also accepts it because the key is present, and the native-realization check ignores it. Consequently effect_demand_acceptance_holds can return true with no Unrealized rows even though the supposedly retired host effect remains reachable. A retirement row must be refused whenever its key is still observed.
Useful? React with 👍 / 👎.
Comment on lines
+686
to
+690
| fn effect_demand_producers_are_distinct(left: DemandReceipt, right: DemandReceipt) -> Bool { | ||
| match left.producer { | ||
| ModeledCallReachability => match right.producer { | ||
| ModeledCallReachability => false | ||
| EmittedRealizationCensus => true |
There was a problem hiding this comment.
When the same instrument produces both receipts but the caller assigns the two different DemandProducer tags, this predicate returns true because it never compares the receipts' instrument_identity fields. The local gate can therefore admit one instrument agreeing with itself, defeating the required independent modeled-versus-emitted evidence; require distinct, verifiable instrument identities rather than only distinct enum labels.
Useful? React with 👍 / 👎.
Comment on lines
+659
to
+662
| fn effect_demand_membership_identities_agree(left: List<String>, right: List<String>) -> Bool { | ||
| effect_demand_strings_contained(left: left, right: right) | ||
| && effect_demand_strings_contained(left: right, right: left) | ||
| && (length(xs: left) == length(xs: right)) |
There was a problem hiding this comment.
When both receipts contain the same set but different duplicate multiplicities, such as ['a', 'a', 'b'] versus ['a', 'b', 'b'], both containment checks and the total-length check succeed. The gate consequently admits receipts whose enumerated memberships differ. Either reject duplicate member identities in each receipt or compare multiplicities directly before declaring agreement.
Useful? React with 👍 / 👎.
Contributor
Author
|
Review 57607 (dashboard artifact /api/reviews/57607/artifacts/stdout.log) — sole finding addressed in 6d85a6e: every |
gunbai-bot
Bot
changed the title
…er bound where the annotation said zero (review 57899) Finding 1: the compile-path annotation opened THE COMPILE PATH'S HOST-EFFECT DEMAND IS ZERO while the carrier under it recorded PopulationMeasuredLowerBound with a named missing basis -- DESIGN 4b rung inflation in the module written to prevent it. The block now leads with what the instrument established (none observed by this producer, a lower bound), names the excluded basis, and records the earlier overstatement rather than quietly deleting it. The PR title is corrected the same way. Finding 2: every standalone variant-to-Bool predicate cited (effect_demand.dag row_claims_native, row_is_retired, row_is_unrealized, population_subject_is_complete, disposition_blocks_implementation, operation_is_implementable, seam_is_realized, seam_is_unrealized, seam_is_unrostered, seam_has_executed_evidence, seam_binding_is_ambiguous, local_gate_holds) is deleted; each consumer now matches the coproduct directly -- the census folds match row.disposition, the partitions match EffectOperationDisposition, the local gate folds DemandPopulation straight into its typed refusal instead of re-lifting a Bool one line later, and the seam folds match SeamRealization. Witnesses that consumed the deleted predicates assert through the derived lists (blocked_operations, implementable_operations) or match the carrier inline. Kept, deliberately: effect_demand_subject_eq and effect_demand_producers_are_distinct are equality relations over two coproducts, not single-variant classifiers; effect_demand_receipt_roots_resolved's resolved arm computes a length check, so it is not a second spelling of the constructor. Evidence: 42 census + 12 floor-join witnesses PASS, and four mutation arms go red on the rewritten assertions -- lower-bound population admitted at the gate (local_gate_refuses_an_incomplete_subject), ambiguity collapsed to a realized bridge (2 witnesses), unrostered seam resolving a realization (4), the blocked partition dropping its unclassified arm (3). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QFQu6KnGhrfAfNBry1a2ev
Contributor
Author
|
Both findings from review 57899 (artifact /api/reviews/57899/artifacts/stdout.log) are addressed in 7041d54. 1. Headline overstated a lower bound — agreed, fixed. The annotation opened "THE COMPILE PATH'S HOST-EFFECT DEMAND IS ZERO" while 2. Undispositioned coproduct predicates — agreed, dissolved. All twelve are deleted, not just the four cited: Kept deliberately, and stated so it can be disputed: Evidence, not just a typecheck: 42 census + 12 floor-join witnesses PASS under |
…e phase refuses an annotation inside a declaration body The subject-completeness block landed inside effect_demand_local_gate's else arm, which DESIGN 4c does not model -- only standalone leading blocks attached to module-scope declarations are admitted -- and the floor refused it six times (parse phase, effect_demand.dag:992-997). It now leads the fn declaration it describes and says the same thing about the whole gate rather than about one arm. Worth recording because the two instruments disagreed: claim_batch accepted the in-body block and ran 54 green witnesses over it, so a passing witness run is not evidence that the annotation grain is legal. The floor's parse phase is the authority. 42 census + 12 floor-join witnesses PASS after the move. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QFQu6KnGhrfAfNBry1a2ev
Contributor
Author
|
All four findings from review 57940 verified against the code and fixed in 917f252. 1. Runtime-insensitive realization join — confirmed, and it was a real fail-closed defect. 2. 3. "was just measured at zero" in the classification rationale — confirmed, fixed. Same overstatement as the earlier headline, in the place that actually steers the lane: it now says this instrument observed none, a lower bound, and therefore not a reason to decline a transport either. 4. Transcribed walk counts — confirmed, removed. The reached-function / total-function / module counts are gone. The block names the producer instead (the modeled call-reachability walk, carried as Evidence: 45 census + 12 floor-join witnesses PASS; three mutation arms go red on exactly the witness that owns them (runtime axis dropped → the new foreign-runtime witness; left root arm admitting → the new left-root witness; modeled-twice admitted → the new producer witness); restore control byte-identical. |
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 31, 2026
…et route added to RequiredFloorDisposition Merge interaction: main's XL-1 floor join (#9669) matches the disposition coproduct exhaustively; this branch widened it with DeclinedRoutedToWetLane. The arm is modeled, not swallowed: FloorStandingCounts gains declined_routed_to_wet_lane, the name and add folds gain the arm, and the four test expectation matches carry it as false. All three join witnesses pass scoped; both files are outside the wet closure (BFS: out), so v10's subject is unmoved. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Q8YpbTjFt7ETNf1AvX4Uqy
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 1, 2026
…urable documents before claiming there are none Four repairs, each found by executing rather than by reading. RECORDS_EQUAL WAS COMPARING THE TARGET'S ARM. It was `left.children == right.children` -- the substrate's structural equality -- which was exactly right while a StoredEdge held a bare locator, and stopped being right the moment the target became a NodeTarget. `NodeTargetResolved(r)` and `NodeTargetUnresolved(l)` over the SAME locator are different values structurally and the same object by content, because content_hash_of_children consumes only the locator. So the store reported "different record" for two records its own identity rule cannot tell apart, and insert_admission turned that into a LocatorCollision: a FABRICATED refusal, raised at a store being asked to do something ordinary. merge reaches it directly -- it reassembles a root from resolved children and re-inserts over a record whose children were unresolved. It was caught by a CONTROL, not by review. The file arm of the merge role claim passed and its node control failed, which is the whole reason a claim is paired with one. The comparison is now over label and LOCATOR, through the same labeled_children_of_stored the identity fold consumes, so there is one definition of what makes two records the same rather than two that agree until one is edited. THE DURABLE POPULATION WAS ASSUMED EMPTY AND IS NOT. The tag-bump note said no document exists to be compatible with, because the only producer is a witness rebuilt every run. True of the closure format; FALSE of the repository envelope, which has checked-in fixtures under dag/test/fixture/scm_repository_load carrying the v1 tags -- six claims went red on them. They are versioned test inputs, updated with the schema they exercise, and the note now says the population was counted rather than assumed. AN ENCODE FIXTURE BUILT ITS SUBJECT THROUGH A ROUTE THAT IS NOW CLOSED. scm_env_absent_root_repository rewrote an encoded root to an uncontained digest and decoded it back; decode now resolves a commit root against the object table and refuses. The state is still reachable and the fixture now reaches it honestly: mint against a store that HOLDS the root, then rebuild the envelope around a store that does not -- which is exactly the residual a SemanticNodeObjectRef leaves open, since it says its object was a node in SOME store and never in THIS one. The document route became its own decode-refusal claim, with a control one fact apart. A DUPLICATE IMPORT, named by review 58166 and real: ObjectTableEdgeTargetIsAuthoredSource was bound twice in one block, which I introduced by inserting it in two separate edits. Deleted. The review's other half -- that ingest may refuse on it -- is not the case: this module resolved cleanly throughout, and three duplicate-import blocks already stand on main from #9763, #9850 and #9669. The DESIGN section 2 objection is the one that holds. Instrument: claim_batch over every dag/test/claim/scm/*_witness_test.dag with each file's own `test fn` roster. 299 pass, 0 fail, exit 0 -- including all eight claims this branch added or moved. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
briansrls
pushed a commit
that referenced
this pull request
Sep 1, 2026
…scharges the self-host behavioral witnesses from route_gap_held (49 required / 112 full) (#9878) * floor_wet_route: model the wet execution route, realize the floor join, the wet lane, and the workflow job Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * wet-receipts: artifact upload on every event, receipt commit only on main Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * wet route: amended transport — subject+executor digest envelope, 7-arm standing, publication wall, candidate-exact changed-witness admission Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * post-merge: PlannedAsChangedWitness census field + selector preserves wet route; 4-arg projection test Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * cssl_assemble: binary-entrypoint disallowed-macros allow (clippy -D warnings, all-targets) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * cli_run: export floor_discovery_path_excluded for claim_batch's test target (clippy --all-targets) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * fix the three .dag defects CI named: envelope literal field, selector-test exhaustiveness, axis on the ancestor fixture; add the preserved-wet-route selector control Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * witnesses.yml: regenerate from gunbc.witness_floor_workflow — the wet-receipts lane job renders now that argv_command admits claim_batch_command Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * floor_wet_route: typed dissolve-on row for the four flat-scalar time fields (review 57567), same construction as required_floor's sibling row Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * floor_wet_route: 🟡 marker on the flat-scalar time-field dissolution row, relocated beside the envelope type (review 57568) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Census positive control asserts the sibling's real home disposition, not a gate membership the fixture never had The witness expected Planned for an unrostered sibling of module dag.test.claim.lifecycle_survivor_corpus_census, but that spelling matches no required_gate_prefixes row, so its home disposition is DeclinedOutsideRequiredGate. On main the witness never executed (its match went non-exhaustive when PlannedAsChangedWitness landed -> compile refusal -> outcome=absent); this branch's exhaustiveness repair ran it for the first time and surfaced the wrong expectation. The control keeps its discriminating power: a module-grain cost-debt reading would answer DeclinedCostDebt and go red. Also drops a duplicated DeclinedOutsideRequiredGate arm in the rostered-identity witness beside it. Both executed PASS remotely at this tree. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Census control comment: main's rows are declined_outside_gate_closure/not_executed, not absent Correction relayed by parent: no population hole in #9684's projection — the module was lawfully declined outside the gate closure on main; this branch pulled it into the closure, which is why it compiled (then refused) first here. Comment-only (§4c annotation channel); held locally to ride the seed-envelope push so the running wet dispatch stays candidate-exact. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Wet-receipt time fields consume the std carriers instead of landing as declared debt Per review 57576 on #9725 and the parent ruling that followed: wall_ms is std.types.Milliseconds; executed_at_unix_secs, published_at_unix_secs and the standing fold's evaluated_tree_commit_unix_secs parameter are std.types.EpochSecs (the corpus's one POSIX Unix-instant authority — DFS std first found it, no new type minted); the cadence/grace/budget/skew rows are std.types.Seconds. The 🟡 flat_scalar_wet_receipt_time_fields_dissolve_on row is deleted — the debt never lands. All 12 floor_wet_route and 18 floor_changed_witness witnesses PASS by remote execution on this tree. required_floor's observed_cpu_ms/observed_wall_ms remain main's pre-existing instance of the class under its own dissolution row. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Per-identity wet verdicts join the admission authority at typed outcome grain (ruling c, confirmed with three walls) Wall 1 — outcome grain: WetLaneOutcome and the envelope wire carry the raw typed observation (pass, assertion-false, and ten no-subject-verdict arms incl. the lane's resolve-failed/closure-subject-failed), never a collapsed Bool; the reader refuses any wire outside the closed vocabulary as a contract mismatch. Wall 3 — no duplicate expected-red authority: the expected set derives from gunbc.explicit_witness_admission's ExecutionWitnessKind rows via wet_route_expected_assertion_false_identities; nothing is authored in floor_expected_red. Algebra: pass+unenrolled clean; pass+enrolled now-passing (blocks until the row deletes); assertion-false+enrolled held (counted, shrink-only); assertion-false+unenrolled unexpected red (blocks); any no-verdict outcome blocks regardless of enrollment. ReceiptFailed leaves WetLaneReceiptStanding (six envelope-level arms remain, never waivable). Wall 2 — the publication transaction waives exactly the per-identity red classes so a red attempt's receipt-confined refresh PR can publish evidence. Also per review 57583: age_secs is Seconds on both arms; the variant->Bool publication table is dissolved into the per-identity fold. Refined time scalars bridge to arithmetic through wet_time_scalar (parameter-position coercion, the roadmap_forecast precedent) since the interpreter has no cast for refined scalars in either direction. All 15 floor_wet_route + 18 floor_changed_witness witnesses PASS by remote execution; clippy(lib+bins) clean; 580 lib tests green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Mark wet_time_scalar as a declared workaround with its capability trigger Per parent requirement: the parameter-position identity bridging refined time scalars to Int arithmetic is a workaround for the interpreter's missing refined-scalar coercion, marked on the carrier with a 🟡 dissolution row whose trigger names the capability (an evaluating cast/widening from a where-refined scalar to its base Int, sufficient for EpochSecs-as-Int and Seconds-as-Int under gunbc run). The roadmap_forecast EpochMs-difference site is cited as the same debt, one class, dissolving on the same capability. One identity at every site so the census counts one row. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * wet_route_expected_assertion_false_identities builds a decodable chain The fold_list+list_append form produced a Cons whose tail was a runtime List, which floor_decode_list refuses mid-chain — the PR floor at 069f82d red with 'expected a FreeMonoid Empty/Cons chain, observed List(len=1)' before reaching the wet join. Rebuilt with the filter/map idiom floor_expected_red_roster already decodes through. Executed locally: returns exactly the six enrolled ExecutionWitnessKind identities. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Wet envelope attempt 1 joined per-identity; review 57656 remediation; one-shot bootstrap lease homed outside the wet closure Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * seed-growth trigger count de-literalized * cargo fmt * Envelope v2 lands (attempt_seq 2, head-exact reproduction of the 15/8 split); the unexercised bootstrap lease retires under its own dissolution; review 57685 items 2-3 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Merge main (through XL-R-4A 22ab698); outcome-wire doc de-staled (review 57701) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Merge main (through bfa440b); wet envelope attempt 3 (v4 run) committed Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Merge main (through XL-R-4B a6d6c68); regen Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LUsJiEMrVVJYjbAXXvKtc * Wet subject digest is tree-only: candidate-exactness was unsatisfiable by construction The wet-lane receipt's candidate-exactness test is `envelope.subject_digest == computed_subject_digest`. The envelope is written by claim_batch; the equality is checked by claim_executor. `wet_subject_digest` folded `closure_subject_for_entry` -> `subject_digest_for_closure`, which mixes `transform_content_digest()` -- the bytes of the RUNNING EXECUTABLE (/proc/self/exe) -- into the digest. Two different binaries hash to two different transform digests, so that equality could never hold, on any tree, in any event. The floor refused seven consecutive landing cycles for a staleness that did not exist. The receipt: a one-line edit to a .rs file touching zero .dag moved the "semantic subject" from 5cc866cd221e7b56 to 846ead7b689b7ead on one commit and one pristine checkout, while wet_executor_contract_digest moved too -- correctly, that one is ABOUT the seed bytes. The fix is wet-specific. `subject_digest_for_closure` is UNCHANGED for its two other callers, both resolve-cache keys, where the transform axis is correct and load-bearing: an artifact produced by one compiler must not be served to another. The exe hash is right in a cache key and wrong in a semantic subject. The executor axis is not lost -- it stays on wet_executor_contract_digest, its own declared axis over its own input roster with its own standing arm -- so this removes a double-count rather than a guarantee. Enrolled RED, permanent (4b dissolution-on-climb keeps the evidence when the wall lands): wet_subject_is_independent_of_the_running_binary varies the transform axis directly and requires the wet subject not to move, and the_wet_subject_moves_on_dag_content requires it to move on what it claims to measure. Both run on a real two-module closure -- an empty source list folds both digests to their seed constant and would be green by construction -- and each assertion carries the positive control that makes it discriminating. Verified by mutation: re-pointing wet_closure_subject at subject_digest_for_closure reds them. Instrument: wet_subject_entry_subjects is now the named producer every caller of the digest folds, rendering one `[wet-subject] entry=... closure_subject=...` line per entry. The aggregate sha could say only THAT a producer and a consumer disagreed, never WHERE, which is what let this survive seven cycles. Also: the v6 envelope lands as history (it was computed under the old geometry and is superseded by v7), and the hand-committed-envelope-on-a-PR-branch actuation is declared with a dissolution row whose trigger names the CAPABILITY -- the wet lane commits its own receipt pair onto the head it executed, on any branch a required floor gates -- not merely an artifact that would contribute to one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011JJTD1474gf3cditgsAN6J * SHAPE 1: land the bootstrap-lease MECHANISM so a later envelope can be exact against a tree that carries it A mechanism whose authoring moves the subject must be IN the executed tree before its envelope runs. The wet subject digest folds the closure subject of `v2.workflow.floor_wet_route` -- the route authority is one of its own 19 entries. The lease implementation (the receipt type, `wet_seed_bootstrap_admission`, the `WetFloorAdmittedUnderBootstrapLease` disposition arm) must live in that module; it cannot move out without splitting the authority. So authoring the lease moves the very digest a lease exists to admit, and an envelope executed before the mechanism landed can never be candidate-exact against a head carrying it. Self-defeating in the same shape as the transform-in-the-subject defect this route just repaired. Measured, one binary on one runner, `claim_batch --wet-route`: bare head 40f5e60 subject_digest 7ee4cb3e692843b4...81618 same head + lease mechanism subject_digest d176d6b9e9c7d8b3...74ae7 That 7ee4cb3e is also what the wet lane and BOTH required floors independently computed on that head -- producer and consumer agreeing for the first time, and the end-to-end confirmation of the tree-only subject repair. THIS PUSH IS THE MECHANISM ONLY: types, admission fn, disposition arm, leaseless projection, and an `Absent` row in `gunbc.wet_seed_bootstrap_lease` (homed outside the wet closure so flipping it moves no digest). NO lease is declared, NO drop row is added, NO envelope is claimed -- with the row Absent no drop is in force, and a drop row declaring one would be a false declaration in the authority. The wet lane is dispatched afterwards on the tree that carries this mechanism; that run's envelope is semantic-exact by construction, and if no executor drift occurs while it runs, no lease is needed at all. The floor will refuse on every head until that envelope lands. That is the construction, not a defect: the committed pair is stale by definition until the lane runs on this tree. Lease history, recorded because the prose was wrong: an earlier one-shot lease landed and retired unexercised, and the `gunbc.rung_drop` `BootstrapLivenessLease` row its carrier cited BY NAME was never authored in any commit. Verified on the merged tree (main through 9c34ed7, incl. the TargetModel coproduct dissolution): `cargo check --release -p v1-compiler --all-targets` clean, and `cargo test --lib wet_` 10 passed / 0 failed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011JJTD1474gf3cditgsAN6J * Review 57856 fixes: unconditional wet-gate wall in the runner, lease comment states the obligation (no false rung_drop citation), test imports the derived lease name Operator lifted the semantic-freeze requirement (merge admitted without a window); v9 dispatches on this head. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Q8YpbTjFt7ETNf1AvX4Uqy * floor_wet_route_test: fixture receipts carry the two widened non-join fields (lease_identity, observed_executor_contract_digest) The merged type gained the two readability fields; the corpus census shows these two fixture literals are the only literals of the type, and the module stays outside the wet closure (BFS: out), so v9's semantic subject is unmoved. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Q8YpbTjFt7ETNf1AvX4Uqy * wet-receipts timeout 180 -> 360: the first partial run priced the roster past the provisional cap Run 33420133863 was killed by the 180-min cap at witness 15 of 23 with 162 min of witness execution; the annotation names the lane's per-identity wall_ms receipt as the instrument that re-derives the bound. witnesses.yml regenerated via tools.generated_artifact_gate.main_wet_one, not hand-edited. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Q8YpbTjFt7ETNf1AvX4Uqy * effect_demand_floor_join: carry the DeclinedRoutedToWetLane arm the wet route added to RequiredFloorDisposition Merge interaction: main's XL-1 floor join (#9669) matches the disposition coproduct exhaustively; this branch widened it with DeclinedRoutedToWetLane. The arm is modeled, not swallowed: FloorStandingCounts gains declined_routed_to_wet_lane, the name and add folds gain the arm, and the four test expectation matches carry it as false. All three join witnesses pass scoped; both files are outside the wet closure (BFS: out), so v10's subject is unmoved. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Q8YpbTjFt7ETNf1AvX4Uqy * Land the v10 wet-lane receipt envelope: 23 rows, 15 enrolled-held / 8 pass / 0 no-verdict, subject 9e3bba04 Produced by wet-receipts run 33438118287 on 39e4a3b (attempt_seq 6, executed_at 1788209668); pair taken verbatim from the run's uploaded wet-lane-receipt artifact — the lane's own PR step was skipped because claim_batch exits nonzero on enrolled-red rows. The envelope's subject digest equals the digest the required floor computes for this tree, discharging wet_route_standing_blocking for the 23 routed identities. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Q8YpbTjFt7ETNf1AvX4Uqy * Merge main (4 stage0 files) + review 57955: envelope citations refuse instead of fabricating on CI One seed-shaped push before the v11 dispatch so the envelope's executor contract matches the landing tree: main's stage0 movement and the write_wet_receipt_envelope fix land together. On CI a missing GITHUB_RUN_ID/GITHUB_SHA now refuses rather than mislabeling the publication as local, and a pre-epoch clock refuses rather than publishing timestamp 0; 'local' remains only for genuinely local runs where it is truthful provenance. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Q8YpbTjFt7ETNf1AvX4Uqy * Review 57969: the two §5 defects on the lane paths refuse instead of widening gh pr create failure now proves the already-open state with gh pr view before saying so — any other cause is a typed ::error and exit 1, not an absorbed publication failure. claim_batch's executed_at refuses on a pre-epoch clock instead of stamping the envelope with epoch 0. The force-push finding is declined on the PR: latest-attempt overwrite of the lane-owned refresh branch is the modeled publication semantics (attempt_seq carries the ordering fact, not git history). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Q8YpbTjFt7ETNf1AvX4Uqy * Land the v13 wet-lane receipt envelope: attempt 7, 23 rows, 15 enrolled-held / 8 pass, subject 9e3bba04, executor a2b8cae6 (this head's own seed) Produced by wet-receipts run 33451133460 on e66a850; pair taken verbatim from the run's uploaded artifact. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Q8YpbTjFt7ETNf1AvX4Uqy * Revert "Take over FLOOR-ROUTE-GAP-SELF-HOST implementation" This reverts commit 56799fc, reversing changes made to 72cbda3. --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 2, 2026
…e to live (#9891) * Give the SCM object store two kinds of object, so a file has somewhere to live WHY: `gunbc scm add <file>` could not be built, and the blocker was the model rather than the wiring. `ObjectStore` held `List<ObjectRecord>` -- a NodeKind plus labelled children -- so a file's bytes had exactly one route in: intern them as an Atom's Symbol. That makes the symbol table a content store and gives one name two materially different meanings, which is DESIGN §3's meaning fork, and it is the same wrong model I already rejected for the srv2 mirror. WHAT: `ScmObject = SemanticNodeObject(ObjectRecord) | AuthoredSourceObject(AuthoredSourceRecord)`, under ONE content identity family, because a store holding two identity kinds would make `store_contains` ambiguous about what it contains. The authored identity is derived from the bytes by `content_hash_atom` under a family tag, so a caller supplies content and never an identity -- the same wall `store_node` and `insert_from_structure` already stand behind, reached by a third producer rather than a second identity authority. THE EMPTY FILE HAS ITS OWN CONSTRUCTOR. `content_hash_atom` takes a NonEmptyStr, and hashing "" through some other path would give the empty file an identity minted by a different rule than every other file. `AuthoredSourceContent = AuthoredSourceEmpty | AuthoredSourceText(NonEmptyStr)` makes the degenerate case unwritable rather than admitted and checked. REFUSALS ADDED, EACH BECAUSE A CONSUMER CAN NOW REACH A KIND IT CANNOT ACT ON. Every site that needs a node asks `find_node_record`, whose three arms separate "nothing is here" from "a file is here where a program was required" -- folding those into one absent arm would send an operator looking for bytes that are right there. - checkout: `ObjectIsAuthoredSource` - merge: `TargetRootIsAuthoredSource` - insert: `objects_equal` answers false ACROSS arms, so a file landing on a node's locator is a LocatorCollision rather than silently satisfying a checkout. THE CODEC IS A STRICT EXTENSION, NOT A FORMAT VERSION. A node entry keeps `{kind, children}` byte for byte, so every document the predecessor accepted still decodes identically; an authored entry is `{source}`. The two member sets are disjoint, which is what makes discriminating on shape a partition rather than a guess -- and an entry matching neither still refuses by member set. The decoder routes bytes through `store_authored_source`, so an image cannot assert an identity for a file any more than it can for a node. EXECUTED, five new claims enrolled in test.claim.scm.scm_object_store_collision_witness (bodies in the defining module, where sole_constructor lets the impostor fixture exist): identity follows the bytes AND differs for different bytes; storing one file twice stores it once; the empty file is an object and is not the same object as " "; a file under a node's locator refuses; and the control that the same file stores cleanly under its own derived identity. All five evaluate `true`, as does the migrated both_insertion_orders_produce_the_same_canonical_record and the checkout witness's lost-object arm. Not in this commit: the `add` and `commit` verbs. They now have somewhere to write, and they need the one modeled ScmWriteOutcome the plan names -- that is the next increment, not a wiring afterthought. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT * Apply the authored-source tagging rule to both arms, and make the invariant executable Review 58068's nit was right and is worth more than a reply. `AuthoredSourceEmpty` hashed its tag directly through `content_hash_atom` while `AuthoredSourceText` went through `content_hash_tagged_structural`, so the tagging invariant stated in the comment directly above held for one arm and not the other -- an untagged digest sitting inside a family whose whole claim is that its members are tagged. A stated invariant with one exception is worse than no invariant, and the exception was the arm a reader is least likely to check. Both arms now apply the same combinator under different tags. The empty arm's payload is its own tag, which is degenerate deliberately: what the payload must NOT be is some file's content, because then an empty file and a file holding that content would collide BY CONSTRUCTION rather than by accident. Distinct tags keep the arms apart; the shared combinator is what makes "tagged" true of the family rather than of most of it. The invariant is now executed rather than asserted in prose: `no_authored_identity_is_an_untagged_digest` checks that neither arm's identity equals the bare atom digest of its own tag. It is discriminating -- against the revision this commit replaces it goes red, which is what separates it from a restatement of the comment. Green, along with re-runs of the two identity claims the change could have disturbed. This changes the empty file's identity. Nothing writes authored-source objects yet -- the format landed one commit ago and has no producer outside the witnesses -- so there is no document population to migrate. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT * Execute the authored-source checkout refusal instead of arguing it from the call graph Side-chat review cautioned that my reachability answer might not hold: authored objects decode, but a CHECKOUT might never be able to LAND on one, because every edge the encoder emits was derived from a node record. That caution is right about the encoder and wrong about the decoder, and the difference is worth executing rather than reasoning about -- a call-graph argument is not evidence that two halves meet. The decoder resolves {"target": {"at": "<n>"}} through the position map, and that map now holds authored entries alongside node entries. So a document may name a file as a node's CHILD -- an input no encoder would ever emit, and exactly the kind this repository does not control. The witness builds that document by hand: position 0 is the file, position 1 is a node whose only child targets position 0, root is position 1. Children-before-parents is the order the decoder requires, so the document is well-formed by the format's own rules -- it is not malformed, it is legitimate and says something the model must refuse to reconstruct. The document LOADS (which is what makes this a checkout claim rather than another decoder claim) and the checkout then refuses naming the authored source. It is red against a checkout reporting MissingObject for a file that is present -- the two have opposite remedies -- and red against one that reconstructs the node with the child dropped. Paired with the control that makes the claim about the FILE rather than the document shape: the identical shape with a node at position 0 checks out. Without it, a decoder refusing this shape for any reason would satisfy the claim. One fixture bug found and fixed while writing this: the parent node initially targeted position 1 (itself) rather than position 0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT * Refuse for the right owner: split MemberFailed, and stop reporting a present file as missing Three defects the side-chat review located, each now carrying an executed discriminating claim plus a control: - `root_edge_for` mapped EVERY `CheckoutRefused` to `TargetChildMissing`, so a merge role naming a present authored-source object was reported as absent. `MergeRefusal` gains `TargetChildIsAuthoredSource { role, identity }` and the arm is selected by matching the checkout cause. - `decode_object_step` treated every `MemberFailed` as source-absent, so `{source: null}`, a duplicated `source`, and a non-object subject were all reported as a missing `kind` or an unexpected member. Only `MemberReadMissing` now selects the node arm; the other three refuse in their own right. - Two comment blocks claimed the empty payload and the arm tags carry a property they do not. `content_hash_tagged_structural` already domain-separates the arms by outer tag, and separating preimages is not separating 64-bit digests. The prose now states the weaker true claim. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT * Put every annotation above a subject, and ask the store for a NODE where a node is required Two things, both refusals the corpus already owns. PARSE. The floor refused this branch at the parse phase, not at a claim: gunbc.scm.commit_closure_json_v2 carried a nine-line rationale INSIDE decode_object_step's body, and test.claim.scm.scm_merge_witness_test ended with an eight-line block naming no subject at all. DESIGN 4c models annotations at module-item grain only, so both are unparseable rather than untidy -- and because parse refuses whole, the refusal took every SCM claim in the lane down with it, which is why nothing else in this slice was measured. The first block moves above decode_object_step. The second's subject is merge_refusal_tag: it explains why that function's TargetChildIsAuthoredSource arm has no claim in this file and where the claim that reaches it does live, so it sits above the enumeration it is about. THE ROOT ADMISSION. mint_repository_commit and gunbc.scm.log both asked store_contains, which is kind-agnostic by design -- it answers about the LOCATOR. So an authored-source object under a root locator minted a commit cleanly and then refused at checkout, and log reported it as `LoggedCommitRootHeld`: a row claiming a checkoutable root where checkout refuses. Both now ask find_node_record, whose three arms separate "nothing is here" from "a file is here"; the remedies differ (fetch the object vs. repair a wrong-kind reference), so they are separate arms rather than one Bool. LoggedCommitStanding grows LoggedCommitRootIsAuthoredSource and render says so in words. The claim pair is executed, not argued: a store holding exactly ONE object -- a file -- so RootMissing is unreachable and a kind-agnostic check mints; the refusal must carry the file's own identity back. Its control is one fact apart, a stored node in the same shape, and mints. Both PASS under claim_batch. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Brand a node reference so a file cannot inhabit a program position, and move the tag the schema outgrew TWO REVIEWS, ONE CUT. The designated SCM re-review's central finding was that ObjectId was ONE untyped locator standing in every position that requires a program -- StoredEdge.target, a commit's root -- so an authored-source identity inhabited those positions perfectly well and the model's answer was to notice afterwards: find_node_record at a mint, at a log row, at a checkout. That is validation standing exactly where construction was available (DESIGN 5). codex/gpt-5.6-sol, independently, refused the same PR for continuing to write the v2 closure format tag over a schema that grew a `source` member. Both are fixed here. THE REFERENCE TYPES. SemanticNodeObjectRef and AuthoredSourceObjectRef are sole_constructor over one ObjectId, so only the store mints one and no caller can brand a locator it merely holds; ScmObjectRef is the join for consumers that genuinely handle both. store_node hands back the node brand, store_authored_source the source brand -- two outcome types, because one shared outcome would force store_node's caller to match an arm store_node cannot produce. The admission rule is NOT duplicated: both route through insert_admission. A CHILD EDGE HAS TWO HONEST STATES, and one brand cannot carry both. A partial closure deliberately references objects it does not carry, so a decoder holds edges whose kind nothing has established. Branding those anyway would need a mint that records a CLAIM rather than evidence, and the only place to put it is an exported function -- the importable forge factory this module already recorded once. So NodeTarget names the state: NodeTargetResolved(SemanticNodeObjectRef), or NodeTargetUnresolved(ObjectId). Neither arm reads as the other. WHAT THE BRAND DOES NOT CLAIM: that the object is a node in THIS store. It does not carry which store, so checkout's two refusal arms remain as the honest boundary between stores. What it removes is the authoring mistake. CONSEQUENCES THE REVIEW DERIVED, each now structural rather than checked: closure completeness resolves a child edge instead of asking the kind-agnostic store_contains, so a file no longer counts as a contained child; mint_repository_commit takes a NodeTarget and stores the reference THE STORE handed back, so a RepositoryCommit's root cannot name a file; the decoder's position map carries ScmObjectRef, so a contained edge target or root resolving to an authored entry refuses at decode, owned by the layer reading the document, instead of building the store and failing at checkout. EVIDENCE MOVED WITH THE WALL rather than being deleted with it (DESIGN 4b(4)). The child-edge claim was a CHECKOUT claim; the same document now refuses at decode, so it asserts ObjectTableEdgeTargetIsAuthoredSource -- red against a decoder that resolves without discriminating, and equally red against one reporting the not-present cause for an entry that is right there. A root naming a file has its own claim and cause. merge's TargetChildIsAuthoredSource is still reachable, through an UNRESOLVED target, and its claim moves to the merge witness where insert_from_structure can build that store; its node control moves with it. THE TAGS. This module's own policy is that a schema growing a member grows a new format tag, so the closure document is v3 and the repository envelope v2 -- the latter for two reasons, the embedded table's new entry shape and root resolution at decode. The identity rule is a separate axis and it moved too: v1 named one derivation, and an authored source's identity comes from a different one. ONE tag each, not two: no durable v2 document exists, the only producer is a witness rebuilt every run, and a compatibility arm over an empty population is machinery with no consumer. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Compare records by what the identity is derived from, and count the durable documents before claiming there are none Four repairs, each found by executing rather than by reading. RECORDS_EQUAL WAS COMPARING THE TARGET'S ARM. It was `left.children == right.children` -- the substrate's structural equality -- which was exactly right while a StoredEdge held a bare locator, and stopped being right the moment the target became a NodeTarget. `NodeTargetResolved(r)` and `NodeTargetUnresolved(l)` over the SAME locator are different values structurally and the same object by content, because content_hash_of_children consumes only the locator. So the store reported "different record" for two records its own identity rule cannot tell apart, and insert_admission turned that into a LocatorCollision: a FABRICATED refusal, raised at a store being asked to do something ordinary. merge reaches it directly -- it reassembles a root from resolved children and re-inserts over a record whose children were unresolved. It was caught by a CONTROL, not by review. The file arm of the merge role claim passed and its node control failed, which is the whole reason a claim is paired with one. The comparison is now over label and LOCATOR, through the same labeled_children_of_stored the identity fold consumes, so there is one definition of what makes two records the same rather than two that agree until one is edited. THE DURABLE POPULATION WAS ASSUMED EMPTY AND IS NOT. The tag-bump note said no document exists to be compatible with, because the only producer is a witness rebuilt every run. True of the closure format; FALSE of the repository envelope, which has checked-in fixtures under dag/test/fixture/scm_repository_load carrying the v1 tags -- six claims went red on them. They are versioned test inputs, updated with the schema they exercise, and the note now says the population was counted rather than assumed. AN ENCODE FIXTURE BUILT ITS SUBJECT THROUGH A ROUTE THAT IS NOW CLOSED. scm_env_absent_root_repository rewrote an encoded root to an uncontained digest and decoded it back; decode now resolves a commit root against the object table and refuses. The state is still reachable and the fixture now reaches it honestly: mint against a store that HOLDS the root, then rebuild the envelope around a store that does not -- which is exactly the residual a SemanticNodeObjectRef leaves open, since it says its object was a node in SOME store and never in THIS one. The document route became its own decode-refusal claim, with a control one fact apart. A DUPLICATE IMPORT, named by review 58166 and real: ObjectTableEdgeTargetIsAuthoredSource was bound twice in one block, which I introduced by inserting it in two separate edits. Deleted. The review's other half -- that ingest may refuse on it -- is not the case: this module resolved cleanly throughout, and three duplicate-import blocks already stand on main from #9763, #9850 and #9669. The DESIGN section 2 objection is the one that holds. Instrument: claim_batch over every dag/test/claim/scm/*_witness_test.dag with each file's own `test fn` roster. 299 pass, 0 fail, exit 0 -- including all eight claims this branch added or moved. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Name the identity rule for its subject, and freeze a predecessor document to prove the version refuses as a protocol gap Two items from the designated SCM reviewer's bar that the tag bump left half-done. THE RULE'S NAME SAID `node` WHILE ITS TABLE HELD NON-NODE IDENTITIES. `repository_node_identity_rule_tag` is the one authority in the document whose whole job is to say WHICH derivation reconstructed these identities, and it asserted something false about its own subject the moment the object table grew an authored-source arm -- a meaning fork in the worst possible place. It is now `repository_object_identity_rule_tag`, and its value names the rule rather than one branch's hash function: `scm-object-identity-v1`, a total law over the object coproduct whose semantic-node branch delegates to v2.std.node content_hash. A manifest branch joins this tag when it lands rather than minting a third. THE OLD-WRITER EVIDENCE, RESHAPED BY THE VERSIONING RATHER THAN DROPPED. The re-review asked for a frozen predecessor document -- bytes not produced by the current encoder -- to prove old documents still read. Bumping the tag changed what that evidence has to show: a v2 document is now a version this build does not implement, so the required behaviour is a REFUSAL. Specifically the unsupported-protocol one and never malformed, because those have opposite remedies and malformed is the ONE standing that permits supersession (gunbc.scm.supersession standing_permission_refusal) -- a reader that filed a predecessor document as damaged could discard a generation it merely cannot read. So three claims, not one: the cause is the format's own, the STANDING is the protocol gap, and the identical document under this build's tag loads. The document is a hand-authored literal precisely so nothing in the file can quietly re-derive it from the encoder under test, which is what made the existing round trips unable to answer this question. Instrument: claim_batch over every dag/test/claim/scm/*_witness_test.dag with each file's own `test fn` roster. 302 pass, 0 fail, exit 0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * The module names the codec and the tag names the version: retire a suffix that had started to fork meaning `gunbc.scm.commit_closure_json_v2` announced v2 in its name while emitting `gunbc-scm-commit-closure-v3` in its bytes. A reader has no way to decide which of the two is the contract, and that is the meaning fork DESIGN section 3 forbids sitting in the one authority whose whole job is to say which schema this build writes. The suffix was not wrong when it was authored: it named the second CODEC GENERATION, distinguishing this module from the predecessor that encoded the root positionally. That predecessor is deleted, so the suffix had already stopped distinguishing anything, and bumping the format tag turned a harmless fossil into an active contradiction. The fix is the ordinary one -- one fact per authority: the module names the codec, the tag names the version, and the version lives in a value the encoder actually emits rather than in a spelling in a path. Renamed with it: the module, its file, the witness module and file, and every prose citation across the corpus. A citation naming a symbol that no longer exists is the positional-citation failure by another route -- it decays silently and nothing refuses. Found by the designated SCM reviewer while tracing whether retired version names still fork meaning after the tag bump. They did. Instrument: claim_batch over every dag/test/claim/scm/*_witness_test.dag with each file's own `test fn` roster. 302 pass, 0 fail, exit 0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Restore the rung-drop row an auto-merge deleted, and revert a module rename whose admission wave every other lane would have paid for Three CI findings, and the first is the one that matters. A DECLARED SAFETY REGRESSION DISAPPEARED IN A MERGE, WITH NO CONFLICT. `direct_call_arg_seam_v2_exemption` landed on main today: a §4b(3) row declaring that one of the two direct-call argument judgments is switched off for every `v2.*` module. Taking main into this branch deleted it -- the declaration and its roster entry -- and git reported a clean auto-merge. That is exactly the class main filed this morning as `merge_region_excludes_shared_tail`, whose own text names `gunbc.rung_drop` as the second carrier with the vulnerable shape: multi-line rows sharing a `}` tail, so the three-way merge factors the tail out of the conflict region and the region's natural resolution drops what lived in it. I resolved the file git DID conflict on and never looked at the one it resolved for me. The recognition rule that row states is about the shared suffix; the operational half I learned here is that the same carrier class also produces SILENT deletions on the files that never conflict at all. `gunbc.rung_drop` and `docs/design-ledgers.md` are restored to main's content, and the ledger is REGENERATED from the authorities rather than hand-restored, so what is committed is what the projection derives. THE MODULE RENAME IS REVERTED, AND THE REASON IS AN EXTERNALITY. `commit_closure_json_v2` -> `commit_closure_json` was right on its merits: after the tag bump the module announced v2 in its name and v3 in its bytes. It is reverted because of what it costs everyone else. A rename re-targets every binding naming it, which the required namespace-wave-admission phase classifies `TargetChanged` -- not auto-admitted, one roster row each, 41 here. That roster's own header records the receipt: `stale_admissions` is computed PER RUN, so rows sitting on main are inherited by every open pull request, and a change touching no namespace can never match them; the phase then refuses every unrelated lane until they are dissolved. Spending every other lane's CI to fix one module's name is the externalized cost DESIGN §5 names, and doing it inside a pull request about the object model compounds it. So the fork is REPORTED where a reader meets it: the module header now says which of the two versions is the contract (the emitted tag), that the suffix is a dead codec-generation fossil, what the rename costs, and a dissolve-on naming the shape that can pay it -- its own change, rows authored and deleted in one wave, at a moment the open-PR population can absorb. A comment does not make the name honest and this one does not claim to; it stops the two from looking equally authoritative. AND ONE REAL DEFECT THE FLOOR CAUGHT THAT LOCAL RUNS DID NOT. `NewUnresolvedness binding gunbc.scm.log::CommitLogRow ObjectId` -- the row still named `ObjectId` after that import was dropped, resolving locally through bare-reference closure while the namespace wall measured it against the base and saw a name that had lost its declarer. The field is now `SemanticNodeObjectRef`, which is what it actually holds: `RepositoryCommit.root` is branded, so the log row carries the reference rather than a bare address. Instrument: claim_batch over every dag/test/claim/scm/*_witness_test.dag with each file's own `test fn` roster. 302 pass, 0 fail, exit 0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Execute the authored-source wire round trip in both arms The branded-reference cut gave AuthoredSourceContent two arms and gave the codec two encode branches, but nothing executed the claim that the arms survive the wire and stay distinct. A codec branch with no discriminating consumer is specification-without-execution (DESIGN.md §5). Two claims now encode a closure holding an empty and a non-empty authored source, decode it, and read the content back off the rebuilt store: one asserts each arm round-trips, the other asserts the two do not collapse into each other. Proven discriminating rather than decorative by mutation: collapsing the text branch of encode_authored_source_content to json_string(s: "") takes both claims red (PASS 0 FAIL 2, exit 1); the codec was restored byte-clean afterwards. Full SCM sweep: 304 pass, 0 fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Make a node requirement a proposition, and let only the store answer it The branded-reference recut left StoredEdge.target a two-armed sum, Resolved beside Unresolved, on the reasoning that a partial closure must reference an object it does not carry. The premise was right and the carrier was wrong, and the designated SCM reviewer is what made the difference visible. A child edge states a PROPOSITION -- a semantic node is required at locator L. Whether a store satisfies it is an OBSERVATION, and observations do not belong inside an object whose identity is derived from its content. The four facts offered as evidence the resolved arm was harmless are the proof it never belonged: the hash ignores the arm, records_equal must ignore it, the wire has no spelling for it, and every consumer re-resolves it anyway. Carrying it there was not merely redundant. store_contains_node_target answered Bool, and "false" meant BOTH "nothing is here" and "a file is here" -- states whose remedies are incompatible, since no fetch repairs an occupied locator. Completeness put wrong-kind locators into the fetchable population, and the encoder's position index was over OBJECTS, so it found the file and emitted the CONTAINED spelling. An admitted partial closure produced bytes this same build refuses at decode. - SemanticNodeTarget { locator } is canonical requirement content, plain and publicly constructible, because stating a requirement forges nothing. The sum is deleted, not deprecated: keeping both would leave a second authoring route that bypasses the census. - resolve_node_target projects it into find_node_record, which ALREADY carries the three arms. No peer NodeTargetResolution type is minted; one concept keeps one authority. - The Bool is deleted rather than kept beside the fix. - ClosureCensus separates absent from source_occupied in one traversal and keeps them apart all the way up. unresolved_identities projects absent only; closure_is_complete requires both empty; admission grew ClosureRequiresNodeAtAuthoredSource naming the whole population, so a caller repairing one does not discover the rest one round at a time. - The encoder now carries TWO indexes. Targets resolve against a node-only map, so a contained reference to a file has no entry to find. This is the part that makes the class unwritable rather than checked: .dag has no module privacy, so guarding the two intended entry points would leave the bad publication representable through the importable raw encoder. Red first, and the claim FORBIDS the state rather than describing the emit-then-refuse contradiction, which would have been green on the defect. Three cells one fact apart: source-occupied FAILED while both controls passed; all three pass now. Mutation: routing NodeRecordIsAuthoredSource back into absent takes exactly one claim red. The two authored-source claims now run through serialize_json and parse_json_document, reading content only from the reparsed value. The reviewer proposed a newline payload; mutating the newline escape left both GREEN, because this parser tolerates a raw newline in a string -- the durable leg would have looked rigorous and discriminated nothing. With a quote-bearing payload, mutating the cp==34 escape takes both red. An unreadable parse answers Absent rather than a manufactured ClosureDocRefusal, which would report a decoder verdict for something the decoder never saw. SCM suite 307 pass, 0 fail. Still open on the reviewer's bar: records_equal compares labeled children in supplied order while content_hash_of_children canonicalizes, so the permutation collision is LIVE; parent-first/child-later graft ordering; repository-v1 names under the v2 tag; a frozen v1 document refusing as unsupported protocol. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Canonicalize on the other route too, and stop fabricating a collision object_store already records why the stored record must be the canonical one: content_hash_of_children SORTS named edges, so keying on the canonical identity while persisting the authored order stores an arbitrary first-observed representative of an equivalence class. store_node does that. insert_from_ structure, the other public way to make a record, did not -- it derived the locator from the canonicalized children and then persisted the children AS SUPPLIED. The consequence was a FABRICATED REFUSAL, which is why it survived: writing [alpha, beta] and then [beta, alpha] derives ONE locator, so the second write found the first record, records_equal compared labeled children in supplied order, they differed, and insert_admission answered LocatorCollision. Nothing had collided. The store refused a write it should have accepted, and every existing claim stayed green because none of them wrote one object two ways. Found by external review reading the identity rule against the persistence, then executed here rather than argued: re_writing_the_same_bindings_in_another_order_is_idempotent FAIL -> PASS swapping_which_target_each_label_names_is_a_different_object PASS throughout The control is the half that matters: without it the claim is satisfied by collapsing genuinely different label-to-target associations into one object, which would trade a fabricated refusal for a fabricated equality. The canonicalization reuses std's canonicalize_labeled_for_content_hash rather than sorting locally. The ordering rule belongs to the identity authority, and a second sort in this module would be that rule written twice, free to drift from the one the hash actually uses. SCM suite 309 pass, 0 fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Derive dependency order instead of trusting insertion order store_records_in_dependency_order returned store.objects, and the note beside it argued that insertion order IS dependency order because store_node recurses into a target before appending its parent. True for store_node, false for the graft route: copy_object appends one record without its children, so copying a parent and then its child leaves the parent EARLIER than the object it references. Completeness never noticed -- both objects are present. The encoder did. It assigns positions in this order, so it reached the parent before the child had one and spelled the target UNCONTAINED while the document carried that very object a few entries later. That contradicts the declared wire meaning of the arm and let a complete closure emit a partial spelling. A post-order walk emits every referenced record before its referent, for any insertion history. The store is acyclic by construction -- a locator is derived from content that already includes its children's locators, so a cycle would have to hash itself -- which is what makes the walk terminate without a separate descent argument. THE FIRST VERSION OF THE CLAIM WAS NOT DISCRIMINATING, and the comment says so because the failure mode is instructive. Encoding, round-tripping through text and requiring the reloaded closure to be complete PASSES ON THE DEFECT: decode re-stores every object in the table, so the child arrives whichever spelling its parent used. The defect is in the BYTES, and an assertion that reads only the rebuilt store cannot see it. The claim now compares IMAGES. The grafted-then-completed store and the naturally-built store are the same closure, so they must serialize to the same document; under the insertion-order encoder they did not. one_closure_has_one_image_however_its_store_was_assembled FAIL -> PASS a_genuinely_partial_store_does_not_encode_as_the_complete_one PASS throughout The control is load-bearing: without it the claim is satisfied by an encoder that never spells a target uncontained at all, which would delete the partial-closure format this branch exists to add. ON COST, since DESIGN section 6 refuses "n is small here": emitted_holds is a linear scan, so the walk is quadratic in object count. That is the same shape find_object already has -- the carrier is a List -- and is bounded by the same dissolve-on already recorded for that carrier. A keyed collection retires both at once; fixing it here alone would leave the store's own lookup quadratic while adding a second index to maintain. SCM suite 311 pass, 0 fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Delete the two node-presence predicates the census replaced Review 58294 found store_contains_node has no caller anywhere in the tree. That is correct and it is mine: this PR added it, it is absent from main, and the census split then removed the need for it without removing it. The same deletion catches a second one the finding did not name. store_holds_node_at's ONLY caller was store_contains_node, so with that gone it is dead too. Deleting just the reported symbol would have left a dead function whose sole consumer had been deleted in the same commit -- fixing the finding rather than the fact. Both are superseded by resolve_node_target, which answers the same question three ways instead of two. That is the whole point of the census: a Bool at a node position cannot separate "nothing is here" from "a file is here", so nothing should be asking for one. I do not accept the rule the finding cites. There is no corpus-wide prohibition on Boolean projections over a coproduct in DESIGN.md -- the same claim was made in review 58182 and answered there with a census of 2,523 such functions across 908 files. What makes these two deletable is that they are UNUSED, which is DESIGN section 2: unnecessary work is redundant work, and dead API surface on a sole_constructor carrier is surface a later caller can reach for. SCM suite 311 pass, 0 fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Name the repository codec for the tag it implements, and freeze a real v1 document TWO ITEMS FROM THE SCM REVIEWER'S BAR, and they are the same seam from opposite sides: what this build CALLS its repository format, and what it DOES with the format it replaced. repository_envelope_format_tag has read "gunbc-scm-repository-v2" since the protocol cut, while the dispatch arm was RepositoryFormatV1 and the codec functions were encode_repository_v1 and decode_repository_v1. That is the meaning fork DESIGN section 3 names: one spelling over two materially different contracts, with the wrong one standing where a reader looks first. Nothing about the schema changes here -- the names were lying about which schema they were. The frozen-predecessor claim needed a REAL document. The existing unknown-format claim uses "gunbc-scm-repository-v99", a version that never existed: it proves the dispatch refuses a tag it does not know, which is a different question from whether this build handles the format it actually superseded. This branch moved the tag from -v1 to -v2, so every repository written before it is a real artifact a real caller can hand to this build today. The fixture is main's v1 document verbatim, carrying both v1 axes -- the schema tag and the fnv1a64-structural-canonical-v1 identity rule this branch also replaced. THE ASSERTION IS THE STANDING, NOT THE REFUSAL. Refusing is easy and the wrong refusal is worse than none: "these bytes are damaged" sends a reader hunting corruption in a perfectly intact file, while "I do not speak this protocol" names a version gap with a real remedy. A refusal-only assertion cannot separate them, because both arms refuse. Mutation receipt -- mapping RepositoryFormatUnrecognized to LoadDocumentMalformed: scm_rl_a_frozen_v1_document_is_a_protocol_gap_not_damage FAIL scm_rl_a_damaged_document_is_not_a_protocol_gap PASS (control held) The control is what stops a classifier that answers UnsupportedProtocol for everything from satisfying the claim. SCM suite 313 pass, 0 fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Read both census populations everywhere, not just the absent one The SCM reviewer re-anchored at 837115a and found the previous fix had MOVED the leak rather than closed it. They are right on all three counts. Splitting the census into absent and source_occupied is only worth what its consumers read. Three of them read the absent half alone: - encode_repository_checked guarded on an_uncontained_target and NOTHING else, so a requirement whose locator is occupied by an authored source walked through and got PUBLISHED. It now refuses first, with its own cause: RepositoryEncodeTargetIsAuthoredSource. The two refusals stay separate because their remedies are -- one says fetch an object that is not here, the other says something IS here and is the wrong kind, which no fetch repairs. - loaded_closure_standing answered LoadPartial for every not-complete closure. LoadPartial promises "fetch the named identities and this completes", which is FALSE for an occupied locator. LoadStanding grows LoadRequiresNodeAtAuthoredSource, and standing_loaded answers false for it: the document read fine, but what it asserts is unsatisfiable. - The raw encoder spells a source-occupied target uncontained, which is indistinguishable from absent on the wire. Both callers now refuse before reaching it. THE THIRD FINDING IS THE ONE I MOST NEEDED. My byte-equality claim -- one_closure_has_one_image_however_its_store_was_assembled -- catches a DISAGREEMENT between assembly routes but not a wrong spelling both routes share. Proven, not conceded: under an encoder that spells EVERY target uncontained, one_closure_has_one_image_however_its_store_was_assembled PASS a_complete_closure_spells_its_child_contained FAIL a_partial_closure_spells_its_missing_child_uncontained PASS Agreement is consistency, not correctness. The new claims read the arm out of the document through decode_target_reference -- the module's own reader, not a second parser written to grade the first. Item 3 also lacked its positional control. Canonicalizing named children is satisfied by sorting every child list unconditionally, which is wrong under Cardinality and Instantiation where PositionalEdges makes position the meaning. The canonicalizer already dispatches correctly on kind_edge_discipline; nothing executed it, so the rule was true and unwitnessed -- and an unwitnessed rule is one a later local sort can quietly replace. SCM suite 317 pass, 0 fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Seal the raw closure encoder behind a carrier the bad state cannot inhabit The SCM reviewer's exact-head ruling on 837115a listed five required closures. 54cd2e4 had already landed three of them (the repository source-occupied refusal, LoadRequiresNodeAtAuthoredSource, and the contained-spelling witness with the mutation receipt they asked for). These are the remaining two, plus the part of the first that their reading was right about and mine was not. encode_complete_closure_document asked unresolved_identities, which projects the ABSENT population. For a requirement whose locator is occupied by an authored source that population is EMPTY -- so the FRONT DOOR returned bytes for the identical state partial admission refused at the side door. My previous claim that "both entry points are closed" was true of admission and false of this one. THE REPAIR IS A CARRIER, NOT A THIRD CHECK. Writing the judgment at each entry point is what produced this bug twice: `.dag` has no module privacy, so encode_closure_document stayed importable and the wrong-kind state stayed representable through it no matter how many front doors were guarded. It now takes a WellKindedClosure -- sole_constructor, mintable only through admit_well_kinded_closure, which runs the census. There is no argument a caller can build that carries the state, so the raw writer needs no claim of its own. An ABSENT population is fine in that carrier and is the partial-closure case the format exists for: it seals KIND, not completeness. encode_admitted_partial_closure_document re-seals rather than re-judges, because admit_partial_commit_closure already refused source_occupied before minting. Also: unresolved_commit_root_step asked position_of, which is the GENERIC object index, so a commit root pointing at a file found a position and passed. It asks node_position_of now. Repository roots are established against node positions, not object occupancy. The seal is not decorative -- it broke three fixture call sites that had been handing the raw encoder a store and a root, which is exactly the shape a production caller could have used. the_complete_writer_refuses_a_wrong_kind_closure_and_names_it the_complete_writer_still_encodes_a_complete_closure (control) SCM suite 319 pass, 0 fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Separate a wrong-kind commit root from an absent one, and execute the new standing Four blockers from the SCM reviewer's exact-head ruling on 9bdd976. 1. COMMIT ROOT. Asking node_position_of was the right first question, but every node-index miss became RepositoryCommitRootNotInStore -- reporting ABSENCE for an object that is present and wrong-kind, the same conflation one layer later. commit_root_standing now answers three ways and the encoder grew RepositoryEncodeCommitRootIsAuthoredSource. HONESTY NOTE ON ITS EVIDENCE, because the arm ships without a discriminating RED and that must not pass silently. I could not author one. RepositoryCommit.root is a SemanticNodeObjectRef, sole_constructor, obtainable only by storing a node; reaching this arm needs a store where that same LOCATOR holds a file, which is a 64-bit digest collision. No fixture can construct it without the forge factory this module refuses to export. Per DESIGN section 4b the arm is therefore mitigatable-with-unauthorable-RED, and its next-rung trigger is a fixture capability that can seed a store at a chosen locator. I am not claiming coverage for it. 2. THE NEW STANDING IS NOW EXECUTED. LoadRequiresNodeAtAuthoredSource had an implementation, exhaustive plumbing, and no evidence any external document reaches it rather than LoadPartial -- a typed carrier and a tag are not a consumer. The document is authored BY HAND because the encoders now refuse to produce it, which is exactly section 4b's case for authoring a RED as source handed to the decoder. scm_image_a_requirement_over_a_carried_file_is_not_partial scm_image_a_requirement_over_nothing_is_partial_and_loaded (control) Mutation, the one the reviewer named: routing source_occupied back through the absent branch takes the first red and leaves the control green. 3. THE MANIFEST TRANSITION RULE was wrong. It said a manifest branch "joins this same tag; it does not mint a third one". The first half is right, the second does not follow: joining one authority is the section 3 point, but adding an arm changes the authority's TOTAL LAW, and this tag names the law. The tag is not pre-bumped for a branch that does not exist; the rule is corrected so the next author does not read it as permission to grow the law under a fixed name. 4. TWO SOURCE COMMENTS ASSERTED THINGS THAT ARE FALSE. object_store said "every node-requiring position takes the node brand; a file in a child edge is then not refused, it is UNWRITABLE." That was true of a design this module no longer has. It is the worst kind of stale comment -- one asserting a SAFETY property, which a reader plans against -- and an external review restated it back as the module's guarantee, which is how a false comment becomes a false shared premise. The honest statement is rung 3, not rung 4: the state is writable and every consumer refuses it by name. Three real defects were found in this seam AFTER the brands landed; had it been unwritable, none could have existed. commit_closure_json_v2 still called the schema addition "a strict extension, not a format version". The module's own policy refutes it -- a schema that grows a member grows a new format tag -- and this codec emits v3 and refuses the frozen predecessor outright. SCM suite 321 pass, 0 fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Make the commit-root fold exhaustive instead of rostering its wildcard CI red on 103f2d5, reproduced locally rather than assumed flaky: nfr_roster_receipt: unrostered=1 stale=0 live=187 unrostered: ["gunbc.scm.repository_envelope::unresolved_commit_root_step"] The new fold carried `_ => found` over CommitRootStanding, a closed coproduct. The roster exists to make exactly that visible, and the lens caught it on the first commit that introduced one. There are two ways to satisfy it and only one is right. Rostering the wildcard would record a residue that does not need to exist; the arms are enumerable, so the fold is written out. That also restores what the coproduct is for: a fourth standing would now break this match rather than being silently absorbed by the wildcard into "keep whatever we had" -- which, for a fold whose whole job is to report the FIRST bad root, would have quietly kept reporting the wrong one. nfr_roster_receipt 1 passed SCM suite 321 pass, 0 fail Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Carry the standing to its destination, scope the image claim, sweep the stale text Three of the four items from the SCM reviewer's ruling on 103f2d5. The fourth is terminal exact-head CI, which follows this push. They accepted the unwitnessed commit-root arm's disposition: keep it, export no forge, claim no coverage. 1. THE NEW STANDING NOW REACHES AN ACTUATOR. The hand-authored document proved LoadRequiresNodeAtAuthoredSource is produced; nothing proved it CHANGED anything. A standing no actuator consumes is a value with a name and no consequence, and the exhaustive arm in supersession was plumbing, not execution. The claim now drives the standing THAT DOCUMENT ACTUALLY PRODUCES -- not a literal handed to the actuator -- through observe_generation into supersede_head_slot with every other condition admitting, so the only thing that can refuse is the standing, and requires exactly StandingDoesNotPermit { standing: LoadRequiresNodeAtAuthoredSource }. The third one-fact cell was also missing: a SEMANTIC NODE carried at that locator must resolve the SAME uncontained spelling to LoadComplete. Without it the pair is about presence rather than kind, and satisfiable by a decoder that treats every uncontained target as unresolved -- which would make LoadComplete unreachable through that spelling. 2. THE IMAGE CLAIM IS RENAMED to a_completed_parent_first_graft_has_the_naturally_ built_image. The old name claimed GLOBAL image invariance across every assembly history -- more than the fixture builds and more than the repository authority grants, since insertion history still decides tie order among INDEPENDENT components. A claim whose name promises more than its body executes is the same inflation as a rung reported above its evidence. 3. THE STALE AUTHORITY TEXT IS ONE SWEEP, not another round of single-paragraph repairs, because that is how the previous two got missed: - repository_envelope said emission order is INSERTION order. It is a derived post-order walk; what survives is the narrower true claim that insertion history decides TIE ORDER among independent components. - "THIS FABRICATES NO v2" sat above an encoder emitting v2. The number moved and the prose did not; it is the v3 statement now. - The repository encode header and its witness header both said "the three causes" / "one claim per cause". The coproduct is larger and one cause is deliberately unwitnessed, so both now say which one and why. - commit_closure_json_v2 credited the index split alone with closing the raw route. It never did -- the carrier does. Both facts are needed and the note now says which does what. - "A missing position is UNREACHABLE" was true only while every closure was complete. For an ADMITTED PARTIAL closure a missing node position IS the uncontained arm, and reading it as unreachable would invite an author to delete the format's reason for existing. - supersession's producer census said loaded_closure_standing answers "only LoadComplete or LoadPartial", and that repository_envelope classifies NOTHING into LoadStanding. Both premises are obsolete; a stale count is exactly what corrupts a census. The conclusion is unchanged and broader. SCM suite 323 pass, 0 fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * State the populations that exist, not the ones these notes were written against The reviewer's hold on 689a2b5 was text-only but authority-bearing: three source notes described populations their own subjects had outgrown, and one asserted a rule in the present tense directly above its retraction. The supersession census is recomputed from the live tree rather than patched. It said "PRODUCERS, TOTAL: two" beside "the producer count grew"; both cannot hold at the declared denominator. There are five, across three modules. Recounting surfaced a second, load-bearing falsehood the review did not name. The census also claimed closure_document_load_standing was the ONLY declaration able to return LoadDocumentMalformed, and concluded that the producer count grew while the permitting surface did not. LoadDocumentMalformed is the sole permitting standing, and repository_envelope_load_standing returns it for its member-read and target-reference modes while object_table_load_standing returns it for six of its seven causes. The permitting surface grew with the producer count. Recording the growth of one while denying the other is exactly the stale count this census exists to catch, so the conclusion is replaced rather than the number. What survives is stated narrowly: the success path stays outside the relation by construction, because none of loaded_closure_standing's three arms permits. RepositoryEncodeRefusal's note described "the single producible cause" and "the two sibling arms" above an eight-arm coproduct, and the checked encoder's note named three ways a repository can be unrepresentable above the same eight. Both now enumerate what exists, grouped by remedy, keeping the domain rule that was each paragraph's actual content. The witness header opened by asserting one claim per cause and retracted it two lines later. The heading now carries the exception it always had. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Exclude witness helpers from the census denominator, by name The recount stated its denominator as "declarations whose return type is LoadStanding". That is too wide: witness modules declare their own, and test.claim.scm_commit_closure_json_v2_witness scm_image_standing_of is one. A fixture helper is not a producer this destination can be reached from, so the denominator is now production classifiers under gunbc.scm.*, and the witness helper is excluded by name rather than by being overlooked. The withdrawn claim -- that the producer count grew while the permitting surface did not -- is removed rather than qualified. The account states positively what holds: LoadDocumentMalformed is the one permitting standing, three of the five producers can answer with it, and no declaration or module owns it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Regenerate the Rust source-type bindings from their authority main carries an updated `proof` row in gunbc.rust_source_type_bindings whose committed projection was never regenerated, so origin/main is itself in a drifted state and every branch that merges it inherits a failing regen phase. Measured here rather than assumed: both the .dag authority and the .rs projection on this branch are byte-identical to origin/main, and regen still reports first_generation_equal=false for this one file. The fix is the projection, not the authority: the generated file now carries what the row says. The build lane is green at this head -- regen first_generation_equal=true, generated-artifact 35/35 matched, 0 drifted. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 * Two claims quantified over a population they did not check The census repair left its neighbours stating the population as it stood when each sentence was written. Two of those neighbours are claims, and that is the part that matters: their names quantify universally while their bodies enumerated a subset, so the standing this branch introduces could have collapsed into the permitting arm with both green. every_non_permitting_standing_refuses_and_says_which checked four of the five non-permitting standings. malformed_is_the_only_standing_that_permits_replacement checked two of the three it owns (LoadComplete and LoadPartial belong to a_partial_load_is_never_supersedable, so the five are covered between the pair). Both now check the whole population. Executed rather than argued: routing LoadRequiresNodeAtAuthoredSource to the permitting arm takes BOTH claims red, and both are green with the arm restored. Before this change that mutation was invisible to both. The prose repairs are the same defect without the teeth. load_standing said "four refusals ... for four different reasons" and listed four of five, so the new standing had no stated reason; it has one now, and it is its own -- the document decoded and what it asserts is unsatisfiable, so no fetch repairs it and superseding would destroy a generation over a defect not in its bytes. object_table_json called collision "the five"; it is the seventh cause against the other six. The census said "one producer today" after counting five, and "a sixth standing" above a six-arm coproduct. The census partition is restated at the grain the review asked for: three declarations DECIDE LoadDocumentMalformed from a refusal cause, one RELAYS it without deciding, and one cannot return it -- a fourth return route is not a fourth decision authority. The surviving consequence is stated at arm grain (the ClosureDocLoaded branch) rather than as "no load that succeeded", because this module deliberately separates a document that decoded from one whose standing answers standing_loaded true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
XL-1 deliverable 1: derive the effect demand before building any transport.
Implementation is intentionally empty. No host transport is added. The brief fixes the sequence — derive reachable effects, disposition every effect, implement only retained demands — and this PR is the first step.
effect_demand_v2_realized_operationsis[], and the census refuses any row claiming a realization that does not exist.The seam denominator, settled by identity
Two lanes reported 14 and 36 whole-body self-call seams. XL-0 retracted 36: their census unioned two predicates — 5 rows from the wall's own emitted refusals (authoritative) and 31 from a regex matching any emitted function whose body is a single
v1_rtbridge call, which never tested self-call at all. Both lanes now derive 14 with identical membership.The tell was structural, not numeric: tightening the predicate left 14 unchanged with no near-misses; the next-looser one jumped to 698 ordinary recursions. A gap with nothing in it says different subject, not different rule.
What this PR carries
v2.compiler.effect_demand— demand carrier, seam carrier (SeamStandingwith a derived realization:seam_realization_forcollects registry matches andseam_realization_from_matchesmaps 0 →SeamUnrealized, 1 →SeamRealizedByBridge, ≥2 →SeamRuntimeBindingAmbiguous; the fourth arm is not a boolean), the 14-row roster, the runtime-binding registry, and the local evidence gateeffect_demand_local_gate→EffectDemandEvidenceStanding = EffectDemandEvidenceAdmitted { source_revision: CommitSha, source_tree: FloorDiscoveryTreeId } | EffectDemandEvidenceRefused { …, conjunct: Symbol }. It is a LOCAL admission naming its failed conjunct; promotion is owned by XL-4 and is not decided here. Two commits over one tree admit; one commit over two trees refuses on the tree — the join key isFloorDiscoveryTreeId, the commit is carried.v2.compiler.effect_demand_floor_join— the producer that replaced a committed TSV: discovered floor claims × seam-reaching dependency closure (v2.lens.module_graph.dependency_closure, the same edge familyclaim_scope_forwalks) × the floor's ownrequired_floor_site_disposition, keyed bystd.decl_ref.DeclarationRef(XL-5's join key) with the dotted identity derived.effect_demand_floor_join_live_default()binds the floor's own roots andwitness_exclusion_substrings(); the digest entry returns text a consumer can quote. Refusals:DiscoveryRefused,EntryPathUndeclared,DuplicateClaimIdentity,JoinPopulationEmpty.src/v2/test/claim/effect_demand/.What is established, and by what
1. Witness discrimination — established on this head (d6746cf).
Mutation receipts with byte-restore controls and per-arm compile-error counts (0 on every arm), run remotely in three dispatches after a 45-minute runner cap killed the combined one:
Planned; digest constant;DeclarationRef.decl_namediverging from the dotted identity) → each reddened exactly its named discriminator(s) (fault 1 reddens the four reach-dependent witnesses, fault 3 the two standing witnesses plus the partition), 12/12 pass after restore, bytes identical to pre-mutation, 0 compile errors on every arm.Two faults earned their keep by finding real defects: one exposed an authored
realizationcolumn beside the derived one (deleted; the registry answers), and rebindingrc_empty_map→not_the_bridgereddened nothing until a bridge-identity witness existed.1b. Live floor-standing digest — refuses, typed, on today's corpus.
effect_demand_floor_join_digest_livereturns the producer's refusal:discover_floor_corpus_rows_from_host_factsfindstest-marked declarations outside*_test.dagin five files (dag/gunbc/predicate_cause_aliasing_roster.dag,dag/test/claim/duplicate_definition_binding_probe.dag,dag/test/claim/filesystem_list_hermetic_witness.dag,dag/test/claim/sole_constructor_completeness_audit_probe.dag,src/v2/test/claim/parse/grammar_validation.dag). The required floor does not refuse them — the full-tree run 33242663070 plans all 39 of their witnesses — so the .dag discovery producer and the runner's enumeration over the prepared closure are two authorities for one question, and the producer note ineffect_demand_floor_joinclaiming "the same refusal the floor would raise" is wrong on today's tree. XL-N ruling: the join stays bound to the producer and the typed refusal IS this slice's deliverable (§5: the refusal is the census); a separate lane dissolves the fork into one authority with an equivalence witness over the LIVE corpus and decides the five files against the Jul-23 rule — when it merges, the digest lands with no diff change here. Nothing here weakens the rule or special-cases the shell. Related executing evidence on main:test.claim.discovery_census_witness.w_counts_partition_the_offered_populationis failing and held on the full-tree run 33242663070. The join's population is therefore established over fixtures only; its live digest is not claimed.2. Current-tree demand standing — NOT established.
Every population figure here is a lower bound or an upper bound, never a measurement of demand: the compile path reaches zero host effects by a call-graph walk over emitted Rust — one producer, realization-side only;
DemandPopulationisPopulationMeasuredLowerBound; seam scope closure is visibility, not call-reachability.3. Local gate — refuses today, by construction. One producer, so
^one_producer_twiceis the conjunct named; a witness asserts the live population is not admitted.4. Final receipt — deliberately unbound. Per XL-N ORDER: #9665 merges → the exhaustiveness repair (#9676) merges → the discovery-fork dissolution lane merges (this PR's denominator depends on it) → merge that main → rerun MUT D/E, seam, demand, floor attribution and the live digest on that tree → bind
source_treeto the post-repair tree digest → READY.Program finding: a 4-module corpus growth inflates unrelated floor claims by 11–18%, with a 30–45% tail
CI on this head is red on the required floor — on a claim this PR never touches. The finding is a program fact and is being handed to the floor-flakiness lane (which is deleting that claim as
RetiredWithDeletedSubject); the red is not this PR's to green, and no workaround is in this diff.build_artifact_verification_witness×2 (395 → ≥502 censored at the cap; 317 → 420/455),int_cross_target_coercion×2,python_grammar_claim.python_grammar_parse_accepts,bash_program_fold.…golden_holds, plusarrow_body_form_witnessandenglish_emit_addover p90 on both — grammar / translate / fold claims.[floor-scope-cost]max 746 modules identical, total built 0.22 → 0.18 GB); reference reachability (dependency_closurefrom the slow entries does not reach any of the four modules; the control from this PR's own test does); the f1f9dd8 lex commit (control predates it).PREFLIGHT RECEIPTS -- NON-BINDING
Cost regression on main, on record (runner VM ceiling).
gunbc compile --source-root dag --source-root src/v2 --entry <E>for E =src/v2/compiler/effect_demand_floor_join.dag(three attempts, BuildBuddy invocations dd9cad4a / bbf17a63 / a115e4c8) and E =src/v2/compiler/effect_demand.dag(battery part af, invocation for tree 7d402b8a) is killed by the runner VM health check at guest usage 7,630,221,312 of 7,864,320,000 B — and measured on srv2 (aarch64,/usr/bin/time -f %M) for tree 5a730642 / head 5c2430e: peak RSS 7,864,888 kB (effect_demand.dag, 133 s), 8,035,636 kB (effect_demand_floor_join.dag, 394 s), 7,861,192 kB (census test), 8,032,596 kB (floor_join test); all four0 blocking error(s)— on a tree whose main is 2a11b31 / 5029d7f. On 2026-08-29 the same two compiles completed on the same runner class over main b726547…f1f9dd8 (receipts final3/part_*:0 blocking error(s), 322 / 768 advisory). The instrument that re-derives it:ctrl-build --remote -- bash -lc 'cargo build --release -p v1-compiler --bin gunbc && ./target/release/gunbc compile --source-root dag --source-root src/v2 --entry src/v2/compiler/effect_demand_floor_join.dag --output-dir /tmp/rc', withGUNBC_MEMORY_BUDGET_BYTESexported. Not localised to a commit between f1f9dd8 and 2a11b31; that bisection is not this PR's.PREFLIGHT ON 5a730642177def24bf507b29ba61975d5c2eaf77
status: PREFLIGHT -- NON-BINDING
tested_commit: 5c2430e
tested_git_tree: 5a730642177def24bf507b29ba61975d5c2eaf77
FloorDiscoveryTreeId: not emitted by this battery (the live digest is the only part that reads a tree identity; see its conjunct) -- the Git tree object above is what every part printed (
TREE=line,git rev-parse HEAD^{tree}on the runner)candidate_head: 5c2430e (#9669 head; main 5029d7f merged)
producer_left / producer_right:
ModeledCallReachability/EmittedRealizationCensus— the two arms ofv2.compiler.effect_demand.DemandProducer, the modeled semantic producers whose receipts the local gate joins (one producer cannot count as two; the gate's^one_producer_twiceconjunct is exactly that refusal). Harness, not producer:claim_batchexecutes the 42 + 12 witnesses and every mutation arm;gunbc run --function effect_demand_floor_join_digest_liveexecutes the live digest. Renderer: this body. Substitution, stated: the per-arm compile CONTROL wasgunbc compilein every earlier receipt; on this main it exceeds the default 7.1 GiB runner VM (regression row above), so on this tree the control is the harness's own resolve-refusal lines in the same run (resolve_refusals=Non every arm header, all 0). That changes the harness of the control, not the producers; thegunbc compilecontrol was re-executed on srv2 for this same tree: all four entries0 blocking error(s)(322 / 767 advisory), peaks in the regression row.entry_identity, roots, mode: entries
src/v2/test/claim/effect_demand/effect_demand_census_test.dag(42 witnesses) and…/effect_demand_floor_join_test.dag(12); mutation subjectssrc/v2/compiler/effect_demand.dag,src/v2/compiler/effect_demand_floor_join.dag; rootsdag,src/v2; claim_batch default execution mode;GUNBC_MEMORY_BUDGET_BYTES=10737418240exported inside the dispatch.command + invocation/artifact references:
.xl1_closing_battery.sh(untracked in the XL-1 worktree; parts af hk ln prod p5 live) viactrl-build --remote -- bash -lc "$(cat .xl1_closing_battery.sh)" x <part>; BuildBuddy invocations 2026-08-30 09:2x–10:xx UTC, outputspf_<part>.outin the XL-1 session.conjunct result (each fault → the witnesses it reddened; baseline 42/42 and 12/12 with resolve_refusals=0; every restore byte-identical):
effect_demand_local_gateover the live population): refuses on^one_producer_twiceby construction — witnessed in the 42 (local_gate_* witnesses), not a green conjuncteffect_demand_floor_join_digest_live): NOT COMPLETED on this tree — on the 20 GB BuildBuddy runner (15 GiB budget, forwarded) it exceeded its 2400 s bound (invocation 391a212b); on srv2 (10 GiB budget exported) it exceeded its 3600 s bound too — wall 3600.8 s, peak RSS 7,985,004 kB, no digest. Cause found and fixed on the next tree:dependency_closurerebuilt the 48k-edge adjacency on every call, once per distinct entry (~1,100×). Conjunct on this tree: RED (no digest). result recorded here when its producer output exists (pre-Floor discovery: one authority — the required floor's roster is the .dag producer's per-file fold; five sidecar dispositions #9685 it refused on five files; Floor discovery: one authority — the required floor's roster is the .dag producer's per-file fold; five sidecar dispositions #9685 renamed four and dispositioned one)effect on readiness: NONE
standing: NOT READY; NOT BOUND; NOT XL-1 CLOSED
superseded_by: 473950ce1f910a06c629123ad0cfd90c79f2b169 (SUPERSEDED AS PREFLIGHT)
PREFLIGHT ON 473950ce1f910a06c629123ad0cfd90c79f2b169
status: PREFLIGHT -- NON-BINDING
tested_commit: 3ca686b
tested_git_tree: 473950ce1f910a06c629123ad0cfd90c79f2b169
FloorDiscoveryTreeId: the join's digest
ac9869cb14394dad(content hash overidentity\tdispositionrows in producer order) — the Git tree object above is what the runner printedcandidate_head: 3ca686b (adds the cost fix:
v2.lens.module_graph.dependency_closure_over_adjacencylifted out ofdependency_closure, which now calls it; the join builds one adjacency per fold)producer_left / producer_right:
ModeledCallReachability/EmittedRealizationCensus(unchanged); harnessclaim_batch(producer witnesses) andgunbc run(live digest); renderer this bodyentry_identity, roots, mode: as the row above; live digest executed on srv2 (aarch64) with
GUNBC_MEMORY_BUDGET_BYTES=10737418240command + invocation/artifact references:
/tmp/xl1_srv2b.shon srv2 (worktree~/wt-xl1bat 3ca686b; log/tmp/xl1_srv2b.log); producer fault arms re-dispatched on the default runner VM (pf2_prod.out,pf2_p5.out)conjunct result — ONLY what executed on THIS tree; nothing is inherited from 5a730642:
digest=ac9869cb14394dad, wall 1317.8 s, peak RSS 15,520,044 kB (srv2,/usr/bin/time); before the fix the same entry exceeded 2400 s on the 20 GB runner. The peak sits 1.3% under the 15 GiB runner budget. Governor scope note (not a defect): the digest process hadGUNBC_MEMORY_BUDGET_BYTES=10737418240exported — line 1 of/tmp/xl1_srv2b.shreadsexport PATH=$HOME/.cargo/bin:$PATH GUNBC_MEMORY_BUDGET_BYTES=10737418240, andgunbc runis a child of that shell; no cgroup memory limit is readable on srv2 (/sys/fs/cgroup/memory.maxabsent). The 15.5 GB peak exceeded the 10 GiB budget without a refusal because The budget arm refuses when it cannot read its bound: MemAvailable and the declared-slot cap are deleted as budget sources #9726's bound governs typed-module-cache capacity and whole-corpus compile admission, not process RSS. Where the excess lives, by subtraction on the same host: the fourgunbc compilecontrols peak at 7.86–8.04 GB (cache + compile), the digest at 15.52 GB, so ≥7.5 GB is the run's own evaluation state outside the cache — the ~13k discovered rows, the 48k-edge adjacency, the per-entry closure walks and the reach memo held by the join's fold. Filed as a scope fact for the memory-governance lane; the remaining cost is the join over the full discovered population, not the closureGUNBC_MEMORY_BUDGET_BYTESforwarded — dispatch line confirms)effect on readiness: NONE
standing: NOT READY; NOT BOUND; NOT XL-1 CLOSED
superseded_by: —
The first attempt (tree
7d402b8ad6a9c7066f994fad86eb4db2bafc246d, head 0afd3b5) — SUPERSEDED AS PREFLIGHT, no result: died at its baseline compile: the BuildBuddy runner VM is killed by its health check at ~7.6 GB duringgunbc compileof these entries (three attempts), and the srv2 host is unreachable from this session since the container recreate. Rows land here, one per tree, in the ruled format (status / tested_commit / tested_git_tree / FloorDiscoveryTreeId / candidate_head / producer_left+right / entry_identity+roots+mode / command+artifact refs / every conjunct by name with its producer output / effect on readiness: NONE / standing: NOT READY; NOT BOUND; NOT XL-1 CLOSED / superseded_by). Earlier rows stay as history marked SUPERSEDED AS PREFLIGHT; nothing is rewritten onto an earlier tree. This section is an index of execution evidence, never its producer.Review dispositions (preflight work; hold unchanged)
data <name>_note: Stringrows = DESIGN §4c prose-as-data): FIXED in 6d85a6e — 55 rows (the 45 counted + 10 in the two test modules) became leading//annotation blocks on their declarations; 42/42 + 12/12 PASS, resolve_refusals=0 on the annotated tree. Candidate head is now 6d85a6e; the PREFLIGHT rows above stay on their own trees.BINDING FREEZE-TREE RECEIPT
HELD -- no receipt exists until the XL-0B freeze tree. At freeze: merge #9669 onto the frozen main, execute both producers and the entire battery (mutation, seam, demand, floor-attribution, live-digest, agreement, completeness, census), derive standing from those outputs, fill this section, then READY . Preflight supplies no inherited green conjunct to a different tree.
Corrections banked in this PR
gunbc compileper entry, the known cost-shape defect inentry_resolve.rstest.manual.*)Not claimed
Not a demand receipt. The 588 declined claims within candidate modules are the floor's scheduler standing (
FloorDeclined*), published by identity through the producer; their cutover disposition is XL-5's (#9675), not this PR's.A false-green generator found on this PR: claim_batch and the floor disagree about annotation grain
Recorded here rather than only in a session thread, because the direction is the dangerous one.
A leading
//block placed inside a declaration body (here, insideeffect_demand_local_gate'selsearm) is accepted byclaim_batch, which resolved the module and ran 54 green witnesses over it — and is refused by the floor's parse phase, six times, withsource annotation sits inside a declaration body. Only module-item grain is modeled(run 33421730079,effect_demand.dag:992-997). The parse refusal also took outnamespace-wave-admission(no head index) and the floor phase, so one illegal comment reads as three failed phases.Two instruments disagree about what is legal, and the permissive one is the one a lane naturally runs before pushing. So a green witness batch is positive evidence for a program the required gate will reject: green here does not screen for annotation grain at all. DESIGN §4c is the authority — only standalone leading blocks attached to module-scope declarations are modeled — and the floor's parse phase is the instrument that enforces it. Before pushing
.dag, grep the diff for^\s+//; a greenclaim_batchrun is not evidence that the placement is legal.