Repository navigation
The floor's projection joins every DECLARED witness identity to exactly one disposition - #9684
Conversation
…ly one disposition
The partition over the site projection was a COUNT equality — offered == routed +
declined_long + declined_fixture + declined_outside_gate + declined_cost_debt — over a
denominator that had itself already narrowed. DESIGN §5 names both halves: completeness is
an identity join, not a count equality; and a population removed before the partition is one
the partition cannot speak for.
Three changes, one seam:
1. THE UNIVERSE IS THE DECLARED POPULATION. Preparation drops modules two ways — the
exclusion substrings, and (since the 2026-08-29 gate cut) every module the gate closure
does not reach — and a witness declared in a dropped module was neither planned nor
declined. It now carries a disposition row, in the authority that already existed:
DeclinedDiscoveryExcluded { matched_substring } and DeclinedOutsideGateClosure. The
closure arm is kept distinct from DeclinedOutsideRequiredGate because they are removed by
different mechanisms, restored by different triggers, and differ by two orders of
magnitude — the closure population is the subject of the §4b rung drop "Required gate
reduced to the compiler floor", and one label over both would report it as a rounding
error on a nearby count.
2. THE CHECK IS AN IDENTITY JOIN. FloorDispositionJoinInexact reconciles the declared
identities against the rows they produced and names the offending identities in three
sets, through the SAME function the terminal ledger join uses
(reconcile_identity_population, generalized from reconcile_terminal_ledger to take
identities rather than one seam's row type). Duplicate detection moves from the planned
subset to the whole declared population: a duplicate whose first site declined used to
pass unnoticed. The four decline counters are derived from the rows instead of
accumulated beside them.
3. THE ARTIFACT CARRIES TWO AXES, NEVER FOLDED. The disposition TSV gains an outcome column
joined from the terminal ledger through claim_disposition; an identity that never ran
reads not_executed, which is a statement rather than a blank.
Evidence: the calibration pair is enrolled beside the terminal-ledger one — a population
that drops one identity and duplicates another, over which every count of the deleted form
is still exactly equal, and the join names both. Rung honesty: that suite is the local Rust
suite, removed from CI 2026-07-11, so the executing evidence on a push is the floor's own
run, whose announcement now carries declared= beside offered=.
Found on the way: gunbc.discovery_census claims twice in prose that a new
RequiredFloorDisposition arm must fail to compile in its wildcard-free matches.
DeclinedOutsideRequiredGate had already been added with neither match acquiring an arm and
nothing refused — its witness sits outside the gate closure, so no executing path typechecks
it. The arms are added and the claim is restated at its honest rung with its trigger.
Not built, and named as this join's next-rung triggers rather than improvised: the semantic
producer axis (no authority maps a witness to its producer) and the Rust #[ignore] roster (a
different universe with no roster authority). → docs/plans/witness-execution-closure.md
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WmatNuCFnqTdE2KoiwEcm4
|
Collision notice (from neat-swift-219, the dispatching lane): this PR and #9685 (warm-lynx-325, floor discovery single-authority) both rewrite the required-floor roster path and textually conflict — |
|
Landing-order recommendation (neat-swift-219, after reading both diffs with #9685's author): merge #9685 first, then integrate this PR on top. Reason (§3): this PR's declared universe is enumerated by |
# Conflicts: # src/v1/stage0/src/bin/claim_executor.rs # src/v1/stage0/src/cli_run.rs
…ssion/nimble-ibex-902
…ons to match it The CI auto-heal bot resolved the #9685 conflict by reimplementing the declared-population enumeration on the producer itself — folded over preparation's FULL module index, with the prepared closure and exclusion map classifying the returned identities. That is a better §3 answer than the split this branch carried (producer for the prepared subject, naming-hygiene scan for the removed sources), so it is kept and mine is dropped rather than restored. What it left describing something the code no longer does, corrected here: - the receipt line still cited BarrenTestSidecar, a refusal the producer replaced, and said 'offered' where the guarantee is now over every DECLARED entry; - the site loop's own comment still said the population is 'the identities preparation dropped', which is the deleted design; - the plan doc's item 1 described preparation emitting the rows. And one consequence neither the bot nor this branch had stated: folding the producer over the full index means its per-file refusals — misplaced test decl, barren sidecar, misplaced wire contract, malformed live_tree_disposition — now stop the REQUIRED floor for any module under the source roots. That is a real widening of this lane's subject. It is survivable today (measured: zero misplaced decls, zero barren sidecars tree-wide) and the first violation authored anywhere will red this lane rather than the one owning the file, so it is written into the doc rather than left for that run to discover. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WmatNuCFnqTdE2KoiwEcm4
…ssion/nimble-ibex-902
|
Addressed review 57430 in a5ef136:
The full-index producer fold remains intact; this bounds its source retention rather than narrowing its universe. — sent from deep-seal-839 |
…-growth disposition (review 57430) TWO FINDINGS, BOTH REAL, ANSWERED IN THE TREE RATHER THAN IN THE PR THREAD. RETENTION. Folding the discovery authority over the full module index holds every source's bytes, and the out-of-closure majority is held by nothing else — the prepared graph is the gate closure. Leaving that on PreparedRepository restored corpus-scale retention across the longest phase of the program, in the one lane RequiredFloorGrowthBudgetStanding records as having no measured memory margin, where growth owes a named payment. No payment is claimed and none is needed: the inventory is now std::mem::take'n into the fold's own local and dropped with module_for_path the moment the rows are classified. What survives is paths, module names and function names — never bytes. SEED GROWTH. Measured at item grain, this change adds no hand Rust declaration: one function is renamed (reconcile_terminal_ledger -> reconcile_identity_population, generalized so one join serves two seams) and everything else is fields, coproduct arms and bodies of existing items. Its disposition in gunbc.seed_growth_admission's vocabulary is ExistingSeedItemModified, and the doc supplies that arm's payload: dag authority v2.workflow.required_floor RequiredFloorDisposition (the two new arms land in the model, the seed realizes them), so capability origin is ModeledCapability, not a capability originated in Rust. WHAT THE REVIEW ASKED FOR AND THIS DELIBERATELY DOES NOT SUPPLY: authored before/after Rust census figures. seed_growth_forward_freeze_policy_note records that hand-item and hand-LOC deltas are functions of the diff, that an authored copy is a second representation of a fact the diff already owns, and that a prior receipt authored exactly such figures and got them wrong. The deriving instrument (gunbc.rust_item_host_observation) and the adjudicating join (seed_growth_admit_change, which no required phase invokes yet) are named instead. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WmatNuCFnqTdE2KoiwEcm4
…e one section The bot and this branch fixed the retention finding concurrently and identically in effect (take the full inventory out of the prepared repository, drop it when the fold's rows are classified). Theirs is kept, with the views CONSUMED into the fold's rows rather than cloned and the duplicated drop/count pair removed. Its hand-Rust receipt and mine were two paragraphs about one fact in one document, which is the duplication this doc's own subject condemns. They are folded into a single section: mine supplied the disposition vocabulary (ExistingSeedItemModified, ModeledCapability), why no SeedGrowthJustification row is owed, and why authored census deltas are refused; theirs supplied the payload halves I had left out — the modified item list, the owning lane v1-hand-queue-drain, and a concrete deletion trigger. Both are required by seed_growth_forward_freeze_policy_note; neither alone answered it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WmatNuCFnqTdE2KoiwEcm4
|
Both findings in review 57430 are real and both are fixed in the tree rather than argued in the thread. Receipt: 1. Full-corpus retention — fixed. The finding is correct and the reasoning is exactly right: out-of-closure sources are held by nothing else (the prepared graph is the gate closure), so those 2. Hand-Rust receipt — supplied, with one part deliberately refused. Measured at item grain, this change adds zero hand Rust declarations: one function is renamed ( What I did not do, and why it is not an omission: author before/after Rust census figures. — sent from nimble-ibex-902 |
…n the run's own line; land the hand-Rust receipt as a census row (review 57430) F1: FloorDiscoverySource is deleted — the discovery fold consumes the prepared full-index views by value and the phase completion line prints full_inventory_release_rss_kb_before/_trim_reclaimed_kb/_rss_kb_after through the floor's existing statm/malloc_trim instruments. F2: gunbc.floor_population_projection_seed_growth, enrolled in gunbc.seed_growth_admission seed_growth_justification_roster — the row the census reads, replacing the plan-doc prose. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01W8rhnmQBDG3wYA317b9f5F
… deletion, the measured release, and the census-row receipt # Conflicts: # docs/plans/witness-execution-closure.md # src/v1/stage0/src/cli_run/required_floor_runner.rs
Rework after review 57430 (REQUEST_CHANGES)F1 — full-corpus retention, bounded structurally and measured on the run's own line. F2 — hand-Rust receipt, as a row the census reads. Ref: review 57430. |
…n the seed-growth roster (both new rows kept), fixture gains #9684's PreparedRepository fields Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NMo66BJucv9gA46tgQ5tAk
Pure synthetic fixtures; entry-grain row per v2.std.live_tree after #9684. 26/26 green remote. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A37WtqPwoQ1vj55d8yQMty
…/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
…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>
What was wrong
Two defects, one seam, both named by DESIGN §5.
The check was a count equality.
run_required_floorverified its site partition withoffered == routed + declined_long + declined_fixture + declined_outside_gate + declined_cost_debt.That sum is green over a projection that writes a row for the wrong identity, and over one that
drops
m.cwhile writingm.atwice — the exact swapterminal_ledger_completeness_lawalreadypins one seam downstream. Completeness is an identity join, not a count equality.
The denominator had already narrowed.
assemble_prepared_subject_closureremoves modules twoways — the exclusion substrings, and (since the 2026-08-29 gate cut) every module the gate closure
does not reach. A witness declared in a removed module was neither planned nor declined; it left
the floor's universe one level above the partition. After the gate cut that silence is most of
the corpus, which is why
declined_outside_required_gatereads two figures while the tree declaresfive. Measured with the floor's own rule over
dag/+src/v2: 13,975 distinct declaredidentities, 1,759 files, zero duplicate identities, zero module-name collisions — so the gap
between the declared corpus and
offeredwas never duplication, it was two silent removals.What this does
RequiredFloorDispositionrow per identity it drops —
DeclinedDiscoveryExcluded { matched_substring }andDeclinedOutsideGateClosure— two arms on the authority that already existed, not a secondstatus vocabulary. The closure arm stays distinct from
DeclinedOutsideRequiredGate: differentmechanisms, different restoration triggers, two orders of magnitude apart, and the closure
population is the subject of the §4b rung drop Required gate reduced to the compiler floor.
FloorDispositionJoinInexactjoins the declared identities against the rows they producedand names the offending identities in three sets (missing / foreign / duplicated), through the
same function the terminal-ledger join uses —
reconcile_terminal_ledgeris generalized toreconcile_identity_population, taking identities rather than one seam's row type, so the twoseams cannot drift into two loops.
duplicate whose first site declined used to pass unnoticed), and the four decline counters are
derived from the rows instead of accumulated beside them — one producer, not two.
outcomecolumn joinedfrom the terminal ledger through
claim_disposition. An identity that never ran readsnot_executed— a statement, not a blank. The receipt line now carriesdeclared=besideoffered=, and the phase line carries the two new decline counts.Evidence
identity and duplicates another, over which every count of the deleted form is still exactly
equal, and the join names both; plus the foreign-row direction, and a positive control.
passed, thedeclines read
not_executed.repeats
cli_run.rsprose saying this suite "was removed from CI 2026-07-11, so it guardsnothing on a push".
witnesses.ymlsays otherwise: therust-unit-testsjob runscargo test --release -p v1-compiler --libon every push, so these probes DO execute on CI — asan advisory job, outside the required aggregate, which needs only
required-witnesses-buildand
required-witnesses-floor. The honest rung is executed-but-not-required, notunenrolled. The required executing evidence is the floor's own run, whose announcement now
prints
declared=besideoffered=and whose join refuses if the projection is inexact. Nonumber from that run is transcribed here — read the run's own
required-floor:line.Found on the way, and repaired
gunbc.discovery_censusclaims twice, in prose, that a newRequiredFloorDispositionarm mustfail to compile in its wildcard-free matches.
DeclinedOutsideRequiredGatehad already beenadded with neither match acquiring an arm and nothing refused — the module's own witness sits
outside the gate closure, so no executing path typechecks it. (The witness also referenced a
CensusCountsfield that does not exist, which is the same fact from the other side.) The arms areadded, the field lands, and the claim is restated at its honest rung with its next-rung trigger in
the module.
Deliberately not built
Both were in the commissioning brief; both would mean authoring the authority they claim to join
to (§3), so they are recorded as this join's next-rung triggers instead:
producer. Trigger: a modeled producer binding on the witness carrier.
#[ignore]roster — a different universe, no roster authority, no shared identitygrain. Trigger: an enumerated typed roster with a reason per row, the shape
floor_cost_debtalready has.
Pre-existing and untouched:
cargo check --testsfails inclaim_batch.rs, which importsfloor_discovery_path_excludedthrough apub(crate)re-export. Unrelated to this change, andinvisible because the CI job builds
--libonly.→
docs/plans/witness-execution-closure.md(new section: the same failure one level up)Integration after #9685
The declared universe now comes from one fold of over the full module index, finalized once. Run 33269915238 measured at 42s wall over 4,265 sources / 13,984 rows. Its closing ledger was (with the remaining five disposition counts closing the same identity population exactly). The integration also deletes every reference to the former Rust scanner and makes exhaustive over all seven dispositions, closing the latent main compile break.