Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions .github/workflows/witnesses.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ env:
GUNBC_REQUIRED_FLOOR_DISPOSITION: required_floor_disposition.tsv
GUNBC_LONG_HOME_STORAGE_AGREEMENT: long_home_storage_agreement.tsv
GUNBC_REQUIRED_FLOOR_CLAIM_COST: required_floor_claim_cost.tsv
GUNBC_REQUIRED_FLOOR_CROSS_CLAIM_DEMAND: required_floor_cross_claim_demand.tsv
GUNBC_REQUIRED_CI_CONTRACT_EPOCH: 2026-09-01.1
jobs:
required-witnesses-build:
Expand Down Expand Up @@ -173,6 +174,14 @@ jobs:
if-no-files-found: error
retention-days: 14
if: "!cancelled() && steps.build_witness_fold.outcome == 'success'"
- name: Upload the floor's cross-claim demand census
uses: actions/upload-artifact@v4
with:
name: required-floor-cross-claim-demand
path: required_floor_cross_claim_demand.tsv
if-no-files-found: error
retention-days: 14
if: "!cancelled() && steps.build_witness_fold.outcome == 'success'"
- name: Record runner filesystem at job end
run: |
# dissolve-on: toolchain_filesystem_probe -- delete the start/end runner-filesystem instrument after its joined readings identify and the fleet fixes the toolchain deleter, OR after per-job runner microVMs make the shared filesystem eviction class impossible
Expand Down
1 change: 1 addition & 0 deletions DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -240,6 +240,7 @@ One row per class, each carrying its recognition rule and its receipts, in [docs
- `ambient_process_state_read_by_a_concurrent_reader`
- `predicate_vacuously_true_on_an_empty_domain`
- `check_subject_narrower_than_its_declared_claim`
- `recurrence_ledger_scoped_below_the_recurrence`

## Building & checks

Expand Down
43 changes: 43 additions & 0 deletions dag/gunbc/floor/cross_claim_demand_census_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
module gunbc.cross_claim_demand_census_seed_growth

import gunbc.roadmap_model { RoadmapNodeId }
import gunbc.seed_growth { SeedGrowthJustification }
import std.decl_ref { DeclarationRef, WholeDeclaration }

// FORWARD-FREEZE RECEIPT for the cross-claim demand census: the required floor reporting, as a run
// product, which pure producer identities it re-derived across claim frames.
//
// WHAT THE ARTIFACT IS FOR, stated first because a justification that only says what the code does
// cannot be checked. `v2.workflow.floor_pure_producer_share` is the mechanism that stops the floor
// re-deriving a pure producer once per claim, and its roster is HAND-AUTHORED. Nothing in the
// repository produced its candidates, because the interpreter's recompute ledger is scoped to ONE
// evaluation frame and reports only keys re-hit inside it: a producer evaluated exactly once per
// claim, across thousands of claims, carries count=1 in every frame's ledger and appears in none of
// them. The instrument that exists to rank redundant recompute was structurally blind to the whole
// population its own repair roster is enrolled from, so candidates were discovered when a per-claim
// budget refusal landed on an unrelated lane's pull request. This artifact names the next candidate
// instead.
data cross_claim_demand_census_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CrossClaimDemandRow", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CrossClaimDemandKey", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CrossClaimDemandCell", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CrossClaimDemandCensus", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CROSS_CLAIM_DEMAND", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CROSS_CLAIM_DEMAND_RETENTION_FLOOR_NS", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CROSS_CLAIM_DEMAND_KEY_CAP", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "CROSS_CLAIM_DEMAND_MODULE_SAMPLE_CAP", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "cross_claim_demand_args_hash", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "cross_claim_demand_absorb_one", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "absorb_claim_recompute_demand", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "cross_claim_demand_rows", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "cross_claim_demand_disclosure", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "clear_cross_claim_demand_census", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_recompute_decl_site", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "write_required_floor_cross_claim_demand_tsv", field: WholeDeclaration }
],
reason: "WHY RUST IS STILL NEEDED, and it is the same boundary cross_claim_pure_share_seed_growth names rather than a second one: the floor builds a FRESH EVALUATION FRAME PER CLAIM, deliberately, so one witness cannot contaminate the next -- and the substrate carries no modeled claim-frame boundary, so nothing authored in .dag can observe across it. The recompute ledger this census folds is already interpreter state; the census stands exactly where the frames are built and does nothing else there.\n\nWHAT IS NOT GROWN: no policy, no threshold anyone refuses on, no roster membership, no escape hatch, and no second producer. The census READS the ledger the interpreter already keeps under GUNBC_RECOMPUTE_TRACE and adds one aggregation across the frame boundary; enrolment stays entirely with v2.workflow.floor_pure_producer_share, which decides membership on a criterion this artifact deliberately cannot supply. A row here is a CANDIDATE whose SERVE cost is unmeasured -- that roster's own header records the case where the serve lost to the recompute and two enrolled rows were REMOVED -- so reading a top row as an enrolment instruction would trade a measured red for an unmeasured regression, and the artifact's header says so.\n\nEVERY TRUNCATION IS DISCLOSED, which is the one place this instrument could have failed the way its subject did. Sub-millisecond first sightings are not retained at identity grain and the omitted key count and their summed cost are printed and written; the distinct-key cap counts its refusals; the per-row module sample is bounded while the module COUNT is exact; and single-claim rows are RETAINED rather than filtered, so the shared population has a control beside it. An artifact that truncated silently would be read as a population, which is gunbc.recurring_failure_mode instrument_output_read_as_subject_content -- the class this census would otherwise commit while reporting on its own cause.\n\nWHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits work serving the v2 self-host program, and the required floor is the instrument that program gates on. Measured on main run 33615659836 (required_floor_claim_cost.tsv, 3477 executed rows, cost_basis=cpu): p50 is 2ms and 3379 rows sit under 280ms, while a tail family sits against the 500ms per-claim ceiling -- and inside that family a witness and its DISCRIMINATING RED, which do materially different work, cost within 2ms of each other. A cost that does not move when the assertion changes is not the assertion's cost. One 34-row module spans 0ms to the ceiling in three bands that track which shared producer a row forces rather than what it asserts. That is the per-claim re-derivation, and while it is invisible to every instrument this repository runs, the budget refusal it causes lands on whichever unrelated lane is pushing.\n\nTHE COST COLUMN IS NOT ADDITIVE, AND THE ONE-NUMBER DISPLACED-COST SENTENCE IS THEREFORE UNDERIVABLE RATHER THAN MERELY UNSTATED. Durations are inclusive of callees, so nested producers overlap: on the first run that produced the artifact, summing cross-claim over the shared rows gave 1,850,686ms against the same run's ENTIRE claim-side CPU of 130,335ms -- fourteen times the whole quantity it is supposed to be a part of, and bind_outcome alone reads 424 seconds inclusive, three times the run total by itself. The summary line therefore carries claim_cpu_total_ms as the ceiling any true total must sit under and says cost_columns=inclusive_of_callees_do_not_sum, so the artifact refuses the reading rather than leaving it to a reviewer. NEXT-RUNG TRIGGER, A CAPABILITY: SELF TIME -- inclusive minus the callees the same pass already counted -- after which the column is additive and the sentence is derivable. IT IS A TRACKED STALL RATHER THAN A WISH, because the mechanism already exists one tier over: v1_compiler.v1_interpreter CrossClaimFillGuard's Drop computes exactly that netting against the CROSS_CLAIM_FILL_FRAMES child stack for the shared-fill ledger; what is missing is a child stack over the recompute ledger's frames.\n\nWHAT IT DOES NOT ANSWER, declared rather than left for a reader to discover: it explains the LEVEL and not the VARIANCE. A per-closure constant is by construction identical on two runs of one tree, and a run-to-run delta is measured (32 rows, byte-identical eval_steps, cpu up 1.31-1.80x over a byte-identical payload module -- gentle-wolf-793), so the two compose rather than compete: the constant puts a family AT the line and something run-to-run decides which of its rows cross it, and the second half has two receipts, neither a cross-run comparison: two rows of one module measured 502ms and EXACTLY 500ms against the 500ms budget, and one row was observed crossing the two populations on ONE tree -- run 33620893203 attempt 1 records an_empty_receipt_series_leaves_the_live_tree_unmeasured_rather_than_held as INTERRUPTED-BEFORE-VERDICT with cost=UNMEASURED while ATTEMPT 2 of the same run records it as COMPLETED-OVER-COST-REQUIREMENT at cpu_ms=500 -- a BOUND beside a VALUE rather than two measurements of one quantity, which is why no cost is written for attempt 1: an interrupted row's reported figure names where the poll observed the ceiling and is a property of the budget. At that margin which population a row lands in is decided by whether the poll fired before or after the work finished, which is a fact about the poll rather than about the row. CITE THE ATTEMPT, NOT THE RUN: a bare run id and a bare job id both resolve to the latest attempt, so a rerun silently changes what a citation serves with no error and nothing visible from the citing end -- the readings above are pinned to /actions/runs/<id>/attempts/<n>/logs, and the other figures in this row come from runs 33615659836 and 33622954427 at run_attempt=1. Through the retraction and the restoration of that evidence, this census reported the same thing throughout, because it keys PRODUCERS and never which rows tipped. The tipping variable is separately open and is not this instrument's subject. Second boundary: the ledger keys PURE NAMED FN evaluations, so a native builtin called directly from a claim body is not a row here -- the same boundary std.evaluation_budget evaluation_budget_opaque_host_call_note draws for the deadline, where no poll stride falls inside an opaque host call and such a claim surfaces as completed-over-cost rather than interrupted. A producer missing from this ranking is therefore not evidence that nothing is re-derived under it.\n\nTHE REDS ARE ENROLLED AND THE FIRST ONE IS THE BLINDNESS ITSELF: a_producer_demanded_once_per_claim_is_invisible_per_frame_and_visible_across_claims asserts duplicated_keys=0 in EACH frame's own ledger beside the census's two-claim row, so re-scoping the census back to one frame reds it. Its controls are a_single_claim_producer_ranks_at_zero_cross_claim_waste (a single-claim cost is the claim's own work and must not score), same_named_producers_at_distinct_declaration_sites_do_not_merge (name-only keying would manufacture cross-claim sharing out of two unrelated single-claim costs) and the_retention_floor_omits_loudly_rather_than_silently.\n\nHAND-ITEM DELTA: the enumerated items are the new module-scope declarations in this diff (v1_interpreter's census types, constants, thread-local and functions, plus the declaration-site helper the unkeyed bucket needed; cli_run's writer). The remaining diff is ExistingSeedItemModified -- EvalRecomputeTrace's unkeyed bucket gains a duration and a declaration site so a composite-argument producer can be RANKED rather than only named, its two call sites follow, and required_floor_runner gains the absorb call, the report block and one env read -- plus enrolled test scope (the four census tests above).",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete the seed declarations when the claim-frame boundary is a MODELED fact -- the evaluator and its frame lifecycle migrated into the self-emitted substrate -- at which point cross-frame demand is a fold over modeled receipts and this host aggregation has nothing left to stand on. NOT retired by the generic cross-claim pure memo landing: a tier that shares every safely servable pure call removes the RECOMPUTE, and this artifact is the DEMAND measurement that says which values a tier must reach and what its coverage gaps cost -- the two are different facts, and a trigger satisfied by the repair would delete the instrument that measures whether the repair covered anything.",
current_boundary: "v1_compiler.cli_run.required_floor_runner claim loop -> v1_compiler.v1_interpreter absorb_claim_recompute_demand -> cross_claim_demand_rows / cross_claim_demand_disclosure -> [cross-claim-demand] log lines and v1_compiler.cli_run write_required_floor_cross_claim_demand_tsv -> gunbc.witness_floor_workflow required_floor_cross_claim_demand_path artifact"
}
Loading
Loading