Repository navigation
PRINT-9: seal inventory provenance behind the admitted ledger, and assess filament supply without minting a capability - #10218
Conversation
…e grain corrections it forced THREE PIECES, and the first two are repairs to what PRINT-8 merged. physical_asset_identity_eq MOVES TO THE MODULE THAT OWNS THE TYPE. The manifest defined a private copy. product.placement_supply owns PhysicalAssetIdentity and already carries host_identity_eq for the sibling branded type, whose annotation states the rule outright: a comparison for a type belongs with the type rather than being re-derived by each consumer. The private copy was tolerable only while one module consumed it, and stopped being tolerable the moment product.inventory needed the same question -- inventory is a generic authority, and importing a specific product's helper to get an equality would invert the layering. THE CITATION CLAIM IS NARROWED TO THE GRAIN ITS RED ESTABLISHED. CITED-MODULE-ABSENT proves the cited module_path resolves. It does NOT establish that decl_name resolves, that field exists, or that the target is a catalog row -- no mutation tested any of those. The annotation had called the whole DeclarationRef a gated citation, which promotes evidence past what it measured, and PrinterCatalogMismatch is renamed PrinterCatalogModuleMismatch because the arm only ever carried expected_module/found_module. The admission asserts the catalog module identifies the A1 mini product AUTHORITY, not an exact catalog row; the trigger for the stronger sentence is authoring that catalog declaration. AssetSourceLotStanding ANSWERS ABOUT ONE ASSET, NOT ABOUT THE WHOLE EVENT. It lives in product.inventory because that module owns what an installation event says; a consumer re-reading assets, origin and stock semantics for itself would be a second interpretation that drifts. The distinction it preserves was nearly lost. QuantityInstalled deliberately permits fewer named assets than units installed -- it refuses only when there are MORE -- so quantity 2 with one named asset records two installed units of which one is individuated, a state this ledger means to represent. The rule I was about to write made identified-count == quantity a precondition for resolving ANY asset's lot, which refuses a named spool's provenance because its SIBLING is anonymous: evidence unrelated to the requested subject. An over-strict refusal is a defect in the same way a permissive one is. Whether the whole population is individuated is a separate question and a caller that needs it must ask it separately. REPEATED EVIDENCE REFUSES RATHER THAN CORROBORATING. Two events naming one asset, even under one lot, are not a stronger fact but an unadjudicated one: these events carry no asset-grained removal or reinstallation history, so a legitimate reinstall and a double installation are indistinguishable here. Calling that corroboration would be answering confidently where the model cannot discriminate. The trigger is an asset-grained stock lifecycle. Seven witnesses over the discriminating population. The first two are the reason the file exists: quantity 2 naming only the requested asset MUST resolve, paired with the same question where the population is fully individuated. An implementation that fused the two properties passes every obvious test and fails row 1. The day-one singleton is the positive control and deliberately not the design target -- it is the shape where exact attribution and full individuation coincide, and building to it alone is how the distinction gets erased. Compile: 35 blocking, all in pre-existing files, none in any file touched here. Witnesses: 15/15 green by direct execution, subject digests verified unchanged across the run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
required-witnesses-floor failed on #10218 with FAILED PHASE namespace-wave-admission (1 unadjudicated delta). The floor itself was clean -- verdict=FloorClean, claims_failed=0 -- so this is not a defect but a governance step the change owed and did not pay. THE DELTA IS EXACTLY THE RE-HOME THAT PR MADE: TargetChanged binding product.printed_chassis.manufacturing_manifest::scan_printer_assets `physical_asset_identity_eq` -- base {product.printed_chassis.manufacturing_manifest} -> head {product.placement_supply} The spelling is authored on both sides and only its TARGET moved, which is what TargetChanged names. The roster's own rule states the remedy and forbids the shortcut: "empty is not permissive -- a run with a real delta still refuses it as UNADJUDICATED, closed by authoring a row and never by a silent admission." So a row is authored, naming the module the name went to, which is the fact that later separates a consumed row from an author-error row. THE RELOCATION IS THE ONE §3 REQUIRES. product.placement_supply owns PhysicalAssetIdentity and already carries host_identity_eq for the sibling branded type, whose annotation states the rule outright. The private copy in the manifest was tolerable while one module consumed it and stopped being tolerable when product.inventory needed the same comparison: inventory is a generic authority, so importing a specific product's helper to obtain an equality would invert the layering. THE DOC COMMENT ABOVE THE ROSTER SAID "THE RESTING STATE IS RESTORED: empty", WHICH THIS MAKES FALSE. Rewritten rather than left standing: it now states what the single row admits, why the layering demanded it, and that its consumption is decidable -- once this merges the base itself binds the spelling to product.placement_supply, the delta stops being produced, and the row matches nothing and is reported as a stale admission. It is therefore due for deletion on the next roster-touching change, by the same rule the previous 57 rows were retired under. Verified: cargo check -p v1-compiler --lib on the remote, "Finished dev profile in 1m 02s", zero errors -- and confirmed the remote had this edit by grepping the shipped tree, since uncommitted tracked changes do ship but the first two checks printed no cargo output at all (ANSI codes defeated the grep, not an absent compile). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
# Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
briansrls
left a comment
There was a problem hiding this comment.
Review on exact remote head b0f68a3: no approval issued. This SHA still exposes asset_source_lot_standing(events: List<InventoryEvent>, ...) and its witness fixtures derive provenance from lone QuantityInstalled rows without the acquire/receive/qualify history, so the fail-open identified by review 59291 is still present on the tree GitHub would merge. The AdmittedInventoryLedger repair described in the side channel has not been pushed to this branch.
Design read for the incoming repair: a sealed admitted ledger may expose the event sequence it admitted; unlike decoded CAD geometry, those events are the judged history itself rather than an untrusted projection of a separate canonical authority. The wall is sufficient only if (1) the carrier remains bound to the exact ProcurementLot against which the sequence settled, (2) every provenance-producing entry point takes the admitted carrier rather than raw events, (3) the later AdmittedFilamentSupply mint derives provenance internally rather than accepting a caller-authored AssetSourceLotStanding, and (4) the new record seal has red/green/differential compile evidence. No trusted raw-event path may remain.
Please push the repaired exact head and replace the placeholder PR title/body before re-review.
…d evidence
Review 59291 (REQUEST_CHANGES) found that asset_source_lot_standing read a raw
List<InventoryEvent>, so provenance could be resolved out of populations
fold_inventory_ledger refuses. The repair is by construction, not validation:
- AdmittedInventoryLedger sole_constructor { lot: ProcurementLot, events }
minted only on the LedgerSettled arm of admit_inventory_ledger.
- asset_source_lot_standing now takes List<AdmittedInventoryLedger>; the raw
entry point is gone. scan_asset_lot_hits survives only BELOW that route.
- The carrier retains the whole ProcurementLot, not its identity: the fold
judges a product, and available stock originates from quantity_acquired, so
an identity-only carrier leaves events-admitted-under-A readable-under-B.
Evidence (all green by execution, digests verified against the run):
- 15 runtime witnesses in test.claim.inventory_asset_source_lot_witness_test,
including the full refused population the ruling named -- unacquired,
zero-quantity, insufficient-stock, more-assets-than-units, event-lot
mismatch -- each asserting its CAUSE label, plus the prefix-leakage row: a
lawful installation followed by a later refusal yields no admitted ledger
AND no provenance.
- 3 constructor-seal witnesses in the new
test.claim.inventory_admitted_ledger_seal_livetree_witness_test: forged
record literal refuses, lawful pass-through is unsealed, differential >= 1.
Non-gating and ReadsLiveTree for the same reason as its manifest sibling.
Also: asset_hits_in_event collapses map-over-filter into one fold, removing a
literal `_ =>` the non-fold-residue detector reads as a wildcard arm.
Compile gate: 34 blocking errors, all pre-existing on main, none in any file
this change touches (attributed by file, not by count).
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
# Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
briansrls
left a comment
There was a problem hiding this comment.
Re-review on exact remote head 8e66d57d7006bf7483709b60b1e66f7de2172541: no approval yet.
The central 59291 repair is present and directionally correct: AdmittedInventoryLedger retains the exact ProcurementLot and event population, admit_inventory_ledger mints it only after fold_inventory_ledger returns LedgerSettled, the externally meaningful asset_source_lot_standing now accepts admitted ledgers, the raw-event version of that function is gone, and the new seal battery targets the sealed record rather than the public coproduct arm.
Four source/evidence defects remain:
-
The raw-event provenance bypass still exists one helper lower.
asset_hits_in_event(event: InventoryEvent, ...) -> List<AssetLotHit>andscan_asset_lot_hits(events: List<InventoryEvent>, ...) -> AssetLotScanremain top-level callable mints. An importer can hand either a lone/refusedQuantityInstalled, receive sealed hit values, and read theirlot/ordinalwithout possessingAdmittedInventoryLedger. With no module privacy, “below the admitted route” is call-graph placement, not a wall. Inline the raw event fold inside a function whose input isAdmittedInventoryLedger, or replace these with an admitted-ledger-only hit producer; no production function accepting raw events should return provenance-bearing hits/scans. -
One witness still absorbs admission refusal into the verdict it expects. Helper
admitted(...)mapsLedgerAdmissionRefusedto[].w_an_unnamed_asset_is_unobserved_not_resolvedthen expectsAssetSourceLotUnobserved; if its fixture starts refusing, the empty fallback produces exactly that arm and the witness stays green. Matchadmit_inventory_ledgerin that witness (or return a typed fixture outcome) and make every admission refusal false before asking whether the admitted ledger contains the requested asset. -
Both live-tree seal files carry a stale, now-false gating account. They say
ReadsLiveTreecausesRequiredFloorDisposition DeclinedLiveTreeand therefore the batteries are non-gating. On this exact head,v2.workflow.required_floorsaysDeclinedLiveTreewas deleted from both the model and host;ReadsLiveTreeremains for affected-set selection, not floor exclusion. Keep the truthful disposition declaration, but replace the obsolete account with the actual exact-head disposition shown by CI. Do not call these non-gating unless the current receipt supplies another real exclusion. -
The printer manifest still contains the serial/asset conflation that its later paragraph retracts. Immediately above
admit_printer_assetit says “Until a printer is registered with its serial, no coupon can be attributed”; the roster annotation later correctly says receipt plus durable individuation is enough and serial merely corroborates. Replace the first sentence so one module does not state both policies.
Additionally, the PR title/body are still the auto-open (3D) PRINT-N template, and exact-head CI on 8e66d57d... is pending. Those must be terminal and synchronized before an exact-head approval.
Next-slice condition, not a present production blocker: AssetSourceLotResolved currently discards the full ProcurementLot retained by the admitted ledger. The filament mint must derive the hit-bearing exact lot directly from the authoritative admitted-ledger population; it must not rejoin a returned lot identity to a caller-supplied lot value or accept a caller-selected/incomplete ledger subset.
… and pay the consumed-row obligation Review 5103871417 (side chat, no approval) found four things. All four are repaired. 1. THE RAW-EVENT ROUTE SURVIVED ONE HELPER LOWER. Deleting the raw form of asset_source_lot_standing was not enough: asset_hits_in_event and scan_asset_lot_hits still took raw events and MINTED a provenance-bearing AssetLotScan. sole_constructor stops a foreign record literal; it does not stop a foreign CALL to an authorized mint, and this language has no module-private functions -- so "below the admitted route" was a statement about the call graph, not a wall. Both collapse into one scan_one_admitted_ledger(ledger: AdmittedInventoryLedger, ...) with the per-event match inside it. There is now no way to obtain an AssetLotScan without first holding a ledger the fold settled. 2. ONE WITNESS CONVERTED ADMISSION REFUSAL INTO ITS EXPECTED VERDICT. The `admitted` helper yields [] on refusal, and an empty ledger population produces exactly Unobserved -- so w_an_unnamed_asset_is_unobserved_not_resolved would have stayed green under fixture-construction failure. It now matches admit_inventory_ledger directly with an explicit false on the refusal arm. The helper's annotation states which three standings it is safe for and why it is unsafe for the fourth. 3. TWO ANNOTATIONS WERE INVALIDATED BY COMPOSITION WITH MAIN. Both live-tree seal files explained their non-gating status by RequiredFloorDisposition DeclinedLiveTree, which main deleted at the root. live_tree_disposition = ReadsLiveTree stays because it is truthful; the obsolete consequence is removed rather than re-asserted. Run 33772917866 settled the question: all six seal witnesses were planned_as_changed_witness and PASSED, so they gate. 4. THE PRINTER AUTHORITY STATED TWO SERIAL POLICIES. "Until a printer is registered with its serial" is replaced with durable individuation, which is what the rest of the module already said. NEW: product.printed_chassis.filament_supply. AdmittedFilamentSupply is the only value a manufacturing attempt may spend as this physical feedstock supply. admit_filament_supply takes RAW lot-and-event evidence, admits every ledger itself, and derives the source-lot standing inside the same call that mints the capability -- it never accepts an AssetSourceLotStanding, which is a verdict vocabulary whose arms any module may author. The exact ProcurementLot comes from the admitted ledgers, never from the caller's unjudged list. FilamentConditionStanding is deliberately outside identity admission. ROSTER: the 47 gunbc#10106 rows that arrived here by merging main are CONSUMED -- run 33772917866 reported every one of them as already satisfied at the base -- and this merge is the toucher their trigger named. Deleted, with their shared label constant. One row stands: gunbc#10218. Evidence: 45/45 witnesses returned true across five files with pre/post md5 digests verified. Compile gate: 34 blocking errors, all pre-existing on main, none in any file this change touches. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
# Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
briansrls
left a comment
There was a problem hiding this comment.
Re-review on exact head 3f2612087d9510911bdb51af3a274291a72941ef: the six items from review 5103871417 are closed. The raw-event hit/scan route is gone, the Unobserved fixture no longer absorbs admission refusal, the live-tree account is updated, the serial contradiction is removed, metadata is real, and the current CI run is attached to this SHA.
No approval yet, because the new filament slice reopens the capability problem at its own boundary.
-
AdmittedFilamentSupplycan be minted through several public bypasses. The module saysadmit_filament_supplyis “THE ENTRY POINT, AND THE ONLY ONE,” butadmit_identified_supplydirectly constructsAdmittedFilamentSupplyfrom an arbitraryPhysicalAsset, arbitraryProcurementLot, and any nonempty identifier list.admit_supply_under_product,admit_supply_against_lot,admit_supply_for_lot_identity, andadmit_supply_for_standingalso returnFilamentSupplyAdmission; the last one accepts caller-authoredAssetSourceLotStanding, exactly the detached verdict the module says no caller may supply. With no module privacy, these are production mints, not internal helpers. Make helpers return non-capability analysis values; only the full judgment may construct the sealed carrier, unless a helper takes an independently sealed predecessor sufficient for the claim. -
The full judgment is not bound to an authoritative, complete population.
admit_filament_supplyaccepts caller-selectedasset_inventoryandInventoryLotEvidence. A caller can fabricate a roster or omit the admitted ledger that carries a conflict and still obtain the final capability. A parametric judge is useful for fixtures, but it should return an unsealed assessment. The capability-bearing producer must close over the owned authority rosters or accept a sealed complete inventory/evidence snapshot. The same bounded weakness exists in the current printer mint and should be repaired beforeManufacturingAttempttreats either carrier as physical authority. -
Identifier evidence neither names the asset nor respects identifier namespaces.
ManufacturerRfidObserved { tag }andOperatorLabelObserved { label }carry no requested asset, reader/observer, or observation receipt. Any nonempty label can therefore admit any requested spool. Flattening the two strings and requiring equality is also the wrong corroboration law: an RFID UID and a human label normally have different values. They corroborate by both being observed as bindings to the samePhysicalAssetIdentity, not by raw-string equality. Carry the subject and provenance on each observation; compare bindings, and keep scheme-specific values distinct. -
The exact lot value can still be silently switched.
lot_record_forreturns every admittedProcurementLotwith a matching identity, andadmit_supply_for_lot_identityfolds them withfn(_, l), so the last record wins. Two valid admitted ledgers may carry the same lot identity with different lot values; if only one names the spool,AssetSourceLotStandingresolves the identity while the final carrier may take the other record. Carry the hit-bearingProcurementLotthrough the provenance projection, or refuse duplicate/conflicting lot records before minting. Add the same-identity/different-record discriminator. -
The new final carrier has no constructor-seal battery. The PR adds
AdmittedFilamentSupply sole_constructor, but the evidence section names only the printer and inventory-ledger seal batteries, and no census fixture targetsAdmittedFilamentSupply. Add forged-literal, lawful pass-through, and scoped differential evidence. This is necessary but not sufficient: it will not detect the callable bypasses in item 1. -
Two authority claims are flattened or over-broad.
FilamentSupplyLedgerEvidenceUnavailableconvertsLedgerRefusalCauseintocause_label: NonEmptyStr, discarding the typed fields already available; carry the typed cause and derive a label only for presentation. Separately,FilamentProductBound/FilamentSupplyProductMismatchcurrently mean only catalog-module agreement, while the positive fixture deliberately points atextdeps.printing.fdm::FilamentMaterial, which the module itself says is not a product authority. Either split product standing from physical-supply admission, or name this as catalog-module agreement until a real filament product authority exists.
Your omission of AssetSourceLotEvidenceUnavailable from AssetSourceLotStanding is correct: that projection accepts only admitted ledgers and therefore cannot observe a ledger refusal. The unavailable arm belongs in the outer filament judgment, where it already sits.
Exact-head CI is still in progress, so a final source disposition also waits on that terminal receipt.
…s the last time Run 33786062832: required-floor verdict=FloorClean (the prior run's completed_over_cost_requirement=1 at cost=500ms EXACT against a 500ms budget did not recur, so it was a boundary observation and not a defect this change caused). The only surviving phase failure is namespace-wave-admission, which reported all 17 `call-reachability grounding gunbc#10156` rows as CONSUMED: #10156 merged, so the base binds every one of those spellings to v2.std.fn_index and no run after it can produce those deltas. Deleted, with their shared label constant. THIS IS THE SECOND SET IN TWO RUNS AND THE REPETITION IS THE FINDING. 47 gunbc#10106 rows went the same way one run earlier. Both were unioned in from main under the rule "keep the rows whose transitions are still open"; both were already closed. The rule was right and its INPUT was guessed. A branch that merges main is downstream of main's own sweep, so main's rows have almost always been consumed by the time they arrive -- and consumption is not readable from the diff, only from the gate. The doc block now states the operational form: keep the rows THIS branch authored and whose transitions are open, take none of the incoming ones on faith, and let the required run name any that are genuinely still open. The discriminator is the receipt, never which branch authored the row. The one row that stands (gunbc#10218) is the positive control: the same run reported the physical_asset_identity_eq delta as ADMITTED-BY it, so the roster is not merely emptier -- it is still adjudicating the one delta this branch makes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
|
Heads-up: your PR touches #10028 merged as The signature is the part worth knowing in advance: a lane goes red with no failing claim. Nothing points at a defect in your change, because there isn't one — the rows are stale and refuse. They are not greppable. The label consts that made previous cohorts enumerable were deleted in that PR. Find them in the namespace-wave-admission phase output, which prints one The remedy is the established pattern, not a workaround: delete the consumed rows in your PR. #10028 itself removed 47 of #10106's consumed rows on the same principle — the obligation is armed by whoever touches the roster next. This was disclosed by cool-ferret-679 in #10028's body and hand-off; the operator ruled it should land now with the next toucher notified, and notifying you is my half of that. Nothing is wrong with your change, and you shouldn't need to debug it from scratch when the lane reds. — sent from tidy-lynx-804 |
…ord on the hit
Review 5105127492 found that the filament module reproduced, one layer down, the
defect this PR had just repaired one layer up -- and wider. Its ruling, followed
here, is that the repair is not a better-guarded mint but no mint at all in this
cut.
1. NO CAPABILITY IS MINTED FROM A CALLER-SELECTED POPULATION. Five public
functions could return a positive arm carrying a sealed AdmittedFilamentSupply,
and the most direct -- admit_identified_supply -- built it from an arbitrary
asset and an arbitrary lot with no provenance derivation at all. Another took
an AssetSourceLotStanding, whose arms any module may author. An honest NAME
would not have repaired this: a parametric judge is a bypass whenever its
positive arm contains the spendable carrier. So AdmittedFilamentSupply is
removed from this cut entirely, along with its seal battery, and returns with
its authority-bound producer in the cut that carries the first real inventory
rows and ManufacturingAttempt -- the cut where it first has a consumer.
assess_filament_supply now yields FilamentSupplyCandidate, an ordinary record
that no actuator accepts.
2. THE EXACT ProcurementLot TRAVELS ON THE HIT. AssetLotHit carries the whole
record rather than the identity, so AssetSourceLotResolved carries the record
the admitted installation event produced. Two admitted ledgers may share an
InventoryLotIdentity while holding different lot VALUES, and the previous
lookup-then-fold resolved that by last-match-wins -- which could return the
record whose event history never named the asset. The lookup is deleted, so
there is nothing left to choose among.
3. IDENTIFIER EVIDENCE NAMES ITS SUBJECT, AND THE TWO ROUTES ARE SEPARATE
NAMESPACES. Observations carry the asset they identify, and a bundle naming
another spool REFUSES rather than being filtered -- filtering is the absorbing
fallback. An earlier cut flattened RFID tags and operator labels into one list
of strings, so a tag and a label that happened to spell the same thing read as
corroboration; consistency is now asked within each route and never across.
4. THE TYPED CAUSE SURVIVES THE BOUNDARY. FilamentSupplyLedgerEvidenceUnavailable
carries LedgerRefusalCause and event_label, not a rendered label, so the
witness asserts InsufficientStock { requested: 11, held: 10 } rather than a
string.
5. AN UNREAD CATALOG NO LONGER REFUSES. Admission asks which physical spool this
is and where it came from; an unread package SKU makes neither unknown, and
refusing there was the serial conflation again. FilamentProductStanding reports
it instead, and the remaining refusal is renamed
FilamentSupplyCatalogModuleMismatch because module agreement is a
contradiction check that cannot establish either side names a filament product.
6. The premature FilamentConditionStanding carrier is removed; a freeform note is
not a condition observation and it had no consumer.
Evidence: 46/46 witnesses returned true across five files with pre/post md5
digests verified. Compile gate: 25 blocking errors, all pre-existing on main,
none in a file this change touches.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
# Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
…remnants of the abandoned shape Review 59427 (dashboard, APPROVE with a nit) found a defect I had noticed and wrongly dismissed as latent. scan_admitted_ledgers summed each ledger's event count while scan_one_admitted_ledger numbered its own events from zero, so two ledgers both reported a hit at ordinal 3 and the number identified no event. It was survivable only because the Resolved arm implies one hit -- a property of today's callers rather than of the value, which is the kind of correctness that stops holding the moment a later reader asks a question the current one does not. The base ordinal now passes DOWN. w_the_event_ordinal_counts_across_ledgers_not_within_one is the discriminator: two admitted ledgers of four events each, the asset named only in the SECOND, and it asserts the cross-ledger ordinal 7 rather than the within-ledger 3. Asserting the resolved lot alone would have passed under either shape. Review 5105127492 (side chat) found two remnants of the shape this PR abandoned: - The opening annotation still said assess_filament_supply "derives the standing inside the same call that mints the capability", contradicting the same file's later and correct statement that there is no sealed carrier here. An authority that states two things about itself is the fork this lane keeps closing. - owned_filament_supply_inventory stood at the bottom of an assessment-only module with no authority-bound producer to consume it. An empty roster with no reader is speculative authority residue; it moves to the cut that carries the final carrier and its first consumer. Evidence: 47/47 witnesses returned true across five files with pre/post md5 digests verified. Compile gate: 25 blocking errors, all pre-existing on main, none in a file this change touches. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4
# Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
briansrls
left a comment
There was a problem hiding this comment.
SOURCE APPROVAL for exact head cc1554de2052608d59f5d08da546ef01fce2d175.
GitHub will not accept a native APPROVE from the connected identity because it is also the PR author; this comment records the source disposition instead.
All source findings from reviews 5103871417 and 5105127492 are closed. The admitted-ledger wall, whole-lot propagation, population-global event ordinal, assessment-only filament boundary, identifier-namespace split, typed refusal, and removal of the premature capability and empty roster are accepted.
This is not a waiver of required CI. The remaining non-green state is the floor's cost verdict: no semantic witness failure is reported, but the revision still lacks a terminal FloorClean receipt. Rotating near-500 ms victims support a floor-headroom/contention problem rather than a regression in those identities. The branch's 42 added identities may still be a trigger for the system-level load, so the exact causal mechanism remains unestablished and belongs with the floor owner. Do not remove the six constructor-seal witnesses or raise another lane's budget in this PR merely to obtain green.
briansrls
left a comment
There was a problem hiding this comment.
FINAL APPROVAL for exact head cc1554de2052608d59f5d08da546ef01fce2d175.
GitHub will not accept a native APPROVE from this connected identity because it is also the PR author; this review records the final disposition.
I re-read the two late changes. The ordinal base is threaded correctly: scan_admitted_ledgers passes the accumulated next_ordinal into each admitted ledger, scan_one_admitted_ledger advances it once per event, and the cross-ledger discriminator requires the second ledger's local index 3 to surface as population index 7. The value remains bounded to the supplied ordered scan and is not a durable event identity.
owned_filament_supply_inventory has been removed without a surviving reader. It was branch-only, is absent from the exact-head change, and the exact-head build completes cleanly. The filament boundary remains a parametric assessment and mints no authority-bound capability.
Run 33818908502, attempt 2, is terminal success on this SHA. The required floor executed 3,637/3,637, with no interruption, over-cost completion, incomplete verdict, or unexpected failure, and returned FloorClean. Its changed-witness receipt records every changed identity as passed. GitHub reports the PR mergeable and clean.
No source or evidence findings remain. The earlier cost-only refusals remain a separate, non-blocking floor-headroom investigation; the clean rerun establishes nondeterminism, not closure.
The operator may merge this exact head. Any source movement invalidates this approval and requires exact-head revalidation.
…e rather than by union main's #10218 sweep and this branch both edited NAMESPACE_TRANSITION_ADMISSIONS. The roster's own note states the rule for exactly this conflict: keep the rows this branch authored whose transitions are open, and for every incoming row READ THE BASE before carrying it. So the two #10324 rows stay, and the incoming #10218 row is deleted — checked against the tree, not guessed: #10218 merged as 95cf395, main declares physical_asset_identity_eq in product.placement_supply and manufacturing_manifest imports it from there, so the base already binds the spelling to the target and the delta is no longer producible. main also deleted the same six consumed rows this branch had deleted, so that claim is dropped from the new entry rather than restated over work already done. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015EdHQ244XXdBKRKGX6jrV4
… and retire the one row the base consumed ONE CONFLICT, in `src/v1/stage0/src/namespace_wave_admission.rs`, and main's incoming side is the authority on how to resolve it: the TWENTY-THIRD DISSOLUTION that landed there writes the rule down operationally -- keep the rows THIS branch authored whose transitions are open, and for every incoming row READ THE BASE before carrying it, because consumption is decidable from the tree and guessing it has cost a required run four times. KEPT: this branch's ten `gunbc#10328 guarantee_stall split` rows. Their transition is open -- the split has not merged, so the base still binds those ten spellings to `gunbc.guarantee_stall` and every one of the deltas is producible. DROPPED, MINE: my own TWENTY-FIRST DISSOLUTION entry. Main removed the same four `gunbc#10028` and two `gunbc#10206` rows independently and recorded it as the TWENTY-THIRD. One event, one record -- a second narration of the same deletion is the double-record this ledger already refuses once, so my entry goes and main's stands. DELETED, AS THE TWENTY-FOURTH DISSOLUTION: the one incoming `gunbc#10218 identity-equality re-home` row. Read from the base rather than waited on, which is what the rule above asks: main declares `physical_asset_identity_eq` in `product.placement_supply` and `product.printed_chassis.manufacturing_manifest` imports it from there by name, so the base already binds that spelling to that target and the delta is not producible. Main's own paragraph says this row is owed deletion by the next roster-touching change once #10218 merges; #10218 has merged and this is that change. `cargo fmt --all --check` clean and `cargo check --release -p v1-compiler --lib` clean under `-D warnings` on the merge result. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017XohvmvDmFP4SVY5t9Sux2
…s consumed row The only conflicted path was `src/v1/stage0/src/namespace_wave_admission.rs`. Resolved three ways, each decided from the tree rather than from a label: - Doc block: kept main's, which carries the new "read the base before carrying an incoming row" rule. My own tail said less and said it later. - Kept the 16 `RUNG_DROP_PER_ROW_SPLIT_LABEL` rows -- the admissions this PR exists to declare. - Deleted main's single #10218 row as CONSUMED, verified against the merged tree: `product.printed_chassis.manufacturing_manifest` imports `physical_asset_identity_eq` from `product.placement_supply`, and `product.placement_supply` declares it. Base and head therefore agree, the delta is not producible, and a surviving row can only be stale. Recorded as the TWENTY-THIRD DISSOLUTION, retired by #10218's own stated trigger and by nothing else. Receipts on this tree: zero conflict markers; 17 `TransitionAdmission {` matches (the struct plus 16 rows); `generated_artifact_gate --function main_wet` errors=0; `claim_executor --required-regen` first_generation_equal=true (156/156 adjudicated); `cargo fmt --all --check` clean. The relocation stays pure: `git diff --numstat` against the merge base over `docs/` and `DESIGN.md` leaves `docs/design-rung-drops.md` at 0/0. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VpnmpcnG82KZBgAaRB7cWD
The previous commit deleted main's `gunbc#10218` admission row on a correct reading of the base, but left the present-tense doc block above the array saying `ONE ROW STANDS (gunbc#10218)` and authored no dissolution entry for it. The TWENTY-THIRD DISSOLUTION directly above covers the six earlier consumed rows and not this one. That is the defect the TWENTY-FIRST DISSOLUTION names -- a doc block describing rows a reader cannot find -- at one row instead of seventeen but in the same shape, and DESIGN section 4c forbids prose asserting what the data does not carry. Found by warm-seal-35 reading the pushed head rather than my report. The block is replaced by a TWENTY-FOURTH DISSOLUTION that keeps what the row admitted (the `physical_asset_identity_eq` relocation, ADMITTED-BY in run 33792437834) in the past tense and states why it no longer stands: #10218 merged as 95cf395, and at merge base d6fb9d6 product.placement_supply declares the symbol while manufacturing_manifest imports it from there, so the delta is not producible. Prose only -- no row, type, or arm changes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VpnmpcnG82KZBgAaRB7cWD
…o logically disjoint edits to one row are a guaranteed textual conflict — three lanes hit it in one night (#10197) * WIP prototype: one rung_drop row per file (do not push; awaiting #10106) * WIP: blank-separated fields (measured), projections regenerated * WIP: rung honesty + projection-side obligation stated in the carrier note * WIP: route-gap precedent closes the probe question; trigger names the required-lane capability * WIP: repoint the one typed DeclarationRef the split's census refused * Restore the sentence my receipt append had deleted from merge_region_excludes_shared_tail * Record the #10218 row's deletion as the TWENTY-FOURTH DISSOLUTION The previous commit deleted main's `gunbc#10218` admission row on a correct reading of the base, but left the present-tense doc block above the array saying `ONE ROW STANDS (gunbc#10218)` and authored no dissolution entry for it. The TWENTY-THIRD DISSOLUTION directly above covers the six earlier consumed rows and not this one. That is the defect the TWENTY-FIRST DISSOLUTION names -- a doc block describing rows a reader cannot find -- at one row instead of seventeen but in the same shape, and DESIGN section 4c forbids prose asserting what the data does not carry. Found by warm-seal-35 reading the pushed head rather than my report. The block is replaced by a TWENTY-FOURTH DISSOLUTION that keeps what the row admitted (the `physical_asset_identity_eq` relocation, ADMITTED-BY in run 33792437834) in the past tense and states why it no longer stands: #10218 merged as 95cf395, and at merge base d6fb9d6 product.placement_supply declares the symbol while manufacturing_manifest imports it from there, so the delta is not producible. Prose only -- no row, type, or arm changes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VpnmpcnG82KZBgAaRB7cWD * Port main's widening of floor_cut_regen_second_generation_agreement into its per-row module Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VpnmpcnG82KZBgAaRB7cWD --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…y this branch's two rows The roster conflicted for the fifth time. Resolved by PROVENANCE rather than by union, because a union here would have resurrected a deliberate deletion. WHAT MAIN DELETED ON PURPOSE: gunbc#10254's spark OOBE rows and their entry. #10254 declared "TRIGGER: these rows go when #10254 merges", it merged at the base, and main's 61274d0 paid that trigger by deleting them. This branch still carried them from an older merge, so unioning the two sides would have re-added rows main retired for cause -- the deletion is invisible in my own diff because I never edited those lines. BOTH SIDES ALSO NARRATED THE SAME gunbc#10218 DELETION independently. Taking the union would have double-recorded one event, which is the failure this roster's own text already refuses once. Main's narration is kept and mine is dropped: one event, one record. So the file is main's wholesale plus exactly two TransitionAdmission rows and one entry. Verified in BOTH directions rather than only mine -- main's 20 rows all present (21 fleet_asset_identity references, 5 cooling_qualification, the TWENTY-THIRD DISSOLUTION), my 2 present, 22 total, zero spark labels, and the #10218 mention count equal to main's own so nothing is narrated twice. The ordinal's justification is rewritten rather than carried: it said TWENTIETH had been minted twice, which described the base it was authored against and not the tree it now lands in, where main has already deleted one of the two. An ordinal tracks the tree it lands in. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015EdHQ244XXdBKRKGX6jrV4
… and mine is dropped #10358 landed 255 admission rows and, in the same change, paid the roster-touching obligation this branch had just paid: main's own TWENTY-FOURTH DISSOLUTION deletes the same nineteen gunbc#10344 asset-identity rows, by the same trigger, with a 15+4 partition matching the nineteen measured here. ONE EVENT, ONE RECORD -- so THIS BRANCH'S TWENTY-FOURTH DISSOLUTION IS DELETED, not reconciled. Both entries carried the same ordinal for the same deletion; keeping both would be the double-narration this roster refuses in its own prose and which it has already resolved this way twice (the #10011 rows yielded to #10106, the #10218 row yielded to main). Main's record is kept because it is main's, and because it is the better entry: it states the partition rather than generalising from one specimen. The deletion itself is unaffected -- the rows are gone either way, and the adjudicator independently confirmed nineteen on run 33862141548 before either record existed. RESOLVED AS MAIN WHOLESALE PLUS THIS BRANCH'S TRANSITION. The file is not generated: .gitattributes line 65 excludes it from merge=generated-artifact and git check-attr reports "merge: unspecified", so ordinary markers and hand resolution are correct here and the regeneration recipe would have been the wrong ceremony. VERIFIED AGAINST THE NEW DENOMINATOR, because main changed the population the arithmetic was measured on: 255 main rows all present, 2 mine, 257 total, identity 255+2 holds, zero surviving fleet_asset_identity rows, exactly one TWENTY-FOURTH DISSOLUTION, and the TWENTY-FIRST TRANSITION intact. Main's highest transition ordinal is still TWENTIETH, so the ordinal needs no renumber. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015EdHQ244XXdBKRKGX6jrV4
Summary
PRINT-9 — the provenance wall between physical inventory and the printed-chassis lane.
A printed coupon is attributable only if the program can say which spool, from which procurement
lot, was mounted on which printer. This change makes the first link of that chain unforgeable,
and classifies the second without yet minting a capability for it.
The defect it repairs (review 59291, REQUEST_CHANGES)
asset_source_lot_standingtook a rawList<InventoryEvent>and scanned it directly, so provenancecould be resolved out of event populations
fold_inventory_ledgerrefuses — an installationbefore acquisition, a zero-quantity event, an install exceeding qualified stock, more named assets
than units. Two live interpretations of whether an event happened is the §3 fork, and it let a
rejected inventory transition produce trusted manufacturing provenance.
The repair is by construction, not validation (§5):
AdmittedInventoryLedger sole_constructor { lot: ProcurementLot, events }, minted only on theLedgerSettledarm ofadmit_inventory_ledger.asset_source_lot_standingtakesList<AdmittedInventoryLedger>. The raw entry point isdeleted, not deprecated.
asset_hits_in_event,scan_asset_lot_hits—were also public mints of a provenance-bearing carrier over raw events.
sole_constructorstopsa foreign record literal; it does not stop a foreign call to an authorised mint, and this
language has no module-private functions. Both collapse into one
scan_one_admitted_ledger(ledger: AdmittedInventoryLedger, …).ProcurementLot, and so does eachAssetLotHit: two admittedledgers may share an
InventoryLotIdentitywhile holding different lot values, so resolving theidentity and looking the record up afterwards was last-match-wins over that set. The lookup is
deleted; the record travels with the hit that produced it.
product.printed_chassis.filament_supply— an assessment, deliberately not a capabilityassess_filament_supplytakes raw lot-and-event evidence, admits every ledger itself, andderives the source-lot standing inside the same call. It never accepts an
AssetSourceLotStanding,which is a verdict vocabulary whose arms any module may author.
Its positive arm carries
FilamentSupplyCandidate, an ordinary record. An earlier cut minted asealed
AdmittedFilamentSupplyhere, and an honest name would not have repaired that: a parametricjudge is a bypass whenever its positive arm holds the spendable carrier, because the caller chooses
the populations — it can omit the ledger carrying a conflicting source-lot claim and still get a
truthful answer about what it supplied. The invariant that matters is not "the parametric judge is
not the only door" but "no caller-selected population can ever produce the value
ManufacturingAttemptwill trust". The sealed carrier, its authority-bound producer closing over thelive rosters, and its constructor-seal battery land in the cut that carries the first real inventory
rows and that consumer.
Other properties this module holds:
than being filtered — filtering is the absorbing fallback.
asked within each route.
LedgerRefusalCause, not a rendered label.came from; an unread package SKU makes neither unknown.
FilamentProductStandingreports it.The remaining refusal is
FilamentSupplyCatalogModuleMismatch— module agreement is acontradiction check and cannot establish that either side names a filament product at all.
Evidence
All green by execution, with pre/post md5 digests over every source so no result comes from a
stale tree. Per witness:
./target/release/gunbc run --source-root dag --source-root src/v2 --entry <file> --function <fn>, over everytest fnin the five files below, withmd5sum -cbefore andafter so no result can come from a tree that moved under the run.
The count is deliberately not transcribed here. A number copied into prose is unreachable from
the thing that owns it, so it rots without anyone touching either end (§6 — name the instrument,
never transcribe its output); this body already carried a stale
46/46after one more witnesslanded. The instrument is the command above and the terminal receipt is the exact-head
required-witnesses-floorrun, which prints one[changed-witness] … outcome=line per identity.test.claim.inventory_asset_source_lot_witness_test— the discriminator population, the fullrefused population each asserting its cause label, and prefix leakage: a lawful installation
followed by a later refusal yields no admitted ledger and no provenance.
test.claim.filament_supply_assessment_witness_test— the nine specified controls, including arefused ledger refusing by cause rather than reporting "unobserved", and the same spool in two
separately valid ledgers conflicting rather than resolving by first match.
test.claim.inventory_admitted_ledger_seal_livetree_witness_test(new) and its printer sibling —forged foreign record literal refuses with
SoleConstructorViolationscoped to the type, lawfulpass-through counts zero, differential ≥ 1, and
CensusNotRunnableyields −1 so a harness thatnever ran satisfies nothing. Run 33772917866 executed all six as
planned_as_changed_witnessand passed them: these gate.test.claim.printed_chassis_manufacturing_manifest_witness_test— unchanged admission battery.Compile gate:
gunbc compile --source-root dag --source-root src/v2 --source-root test --dependency-pool-index primary-precedence. Blocking errors are attributed by file, not bycount; none is in any file this change touches.
Single authority
physical_asset_identity_eqmoves from a private copy inmanufacturing_manifesttoplacement_supply, which ownsPhysicalAssetIdentityand already carrieshost_identity_eq. TheNAMESPACE_TRANSITION_ADMISSIONSrow records it asTargetChangedwith a decidable retirementtrigger.
That roster produced four merge conflicts here, and three of them carried rows from main that were
already consumed by their own subject's merge — 47 for
#10106, 17 for#10156, 4 for#10028.The first two cost a required run each to discover. The doc block now states the operational rule:
keep what this branch authored and whose transition is open, and verify consumption of every
incoming row against the base before carrying it, because consumption is decidable from the tree.
Annotations invalidated by composition, not by this diff
Main deleted
RequiredFloorDisposition::DeclinedLiveTreeat the root. Both live-tree seal filesstill explained their non-gating status by that arm.
live_tree_disposition = ReadsLiveTreestays —it is truthful — but the obsolete consequence is replaced by the executed result.
🤖 Generated with Claude Code
https://claude.ai/code/session_01TuCmz2HjuYzP6GWLgw11E4