diff --git a/dag/gunbc/ci_gate.dag b/dag/gunbc/ci_gate.dag index b34bb6d163c..0cb38a65185 100644 --- a/dag/gunbc/ci_gate.dag +++ b/dag/gunbc/ci_gate.dag @@ -1,5 +1,8 @@ module gunbc.ci_gate +import std.types { NonEmptyStr, String } +import std.process { ProcessExit, ExitSuccess, exit_failure } + type Gate = EmitHostGate | CheapClaimPoolGate @@ -9,3 +12,54 @@ type Gate | ExtdepsScopePlacementGate | ProseRowIntroductionGate | SourceRootIngestGate + +data gate_receipt_state_split_note: String = "WHY A GATE ANSWERS A RECEIPT AND NOT A Bool. The two host gate consumers behind DagCompileCleanGate and GeneratedArtifactDriftGate used to answer through a process-global read collapsed to Bool, with a second String builtin beside it carrying the located detail. consume_floor_compile_clean_gate_verdict folded FIVE distinct states into false -- receipt lock poisoned, receipt install failed, no in-run receipt at all, the receipt's own typed Refused arm, and a genuine Compiled ok:false -- and folded the scope disposition's Skipped into true. So a gate that never ran in this process was indistinguishable from a compile that found hard diagnostics, and a scope disposition selecting nothing was indistinguishable from a clean tree. That is DESIGN's execution-provenance-loss row (a masked run and a clean run rendered identically) sitting underneath not-applicable-rendered-as-malformed, in one Bool. The detail companion did not repair it: it was a SECOND builtin over the SAME global, so a caller had to correlate two reads to recover one fact, and the generated-artifact one FABRICATED prose ('gate body did not run in this process') for the very state the Bool had already erased. THE THREE ARMS ARE THE THREE OWNERS, which is why this is a construction and not a wider enum. GateObserved means the gate reached its subject and decided; its GateOutcome carries the located detail on the failing side, so the detail can no longer be read without the verdict that produced it. GateNotApplicable means the gate's own scope disposition selected nothing to check, an answer whose owner is the disposition and whose remedy is never 'fix the tree'. GateNotRun means could-not-measure: the instrument did not arrive at its subject, whose owner is the instrument and whose remedy is never 'fix the tree' either. The line still stops on GateNotRun (gate_receipt_exit refuses it), so this is not a relaxation: what changes is that the stop is typed and located, and analysis can precede restart. MODELLED ON gunbc.compile_diagnostic_census, deliberately and not coincidentally: that carrier splits CensusObserved from CensusNotRunnable for exactly this reason, and its census_projection_note records that exporting a reader which answers empty on the not-runnable arm was the fail-open it existed to prevent. The same rule holds here, and it is why no accessor hands back a Bool from a GateReceipt: the only way to a verdict is to match the coproduct." + +type GateOutcome + = GateClean + | GateFailed { detail: NonEmptyStr } + +type GateReceipt + = GateObserved { outcome: GateOutcome } + | GateNotApplicable { reason: NonEmptyStr } + | GateNotRun { cause: NonEmptyStr } + +data gate_receipt_exit_note: String = "The one place a receipt becomes a line-stop, so the three arms cannot drift apart across gates. GateNotRun exits FAILURE and says so in its OWN vocabulary rather than borrowing the subject's: a reader of the exit reason can tell 'the gate did not run' from 'the gate ran and refused the tree', which is the whole distinction the Bool destroyed. GateNotApplicable exits SUCCESS and that is not a widen: the scope disposition is the authority for what this gate covers, so a disposition selecting nothing is an answer, not an absence of one, and its reason travels in the receipt for any consumer that wants to count it." + +fn gate_outcome_exit(outcome: GateOutcome) -> ProcessExit { + match outcome { + GateClean => ExitSuccess + GateFailed { detail: detail } => exit_failure(reason: (detail as String)) + } +} + +fn gate_receipt_exit(r: GateReceipt) -> ProcessExit { + match r { + GateObserved { outcome: outcome } => gate_outcome_exit(outcome: outcome) + GateNotApplicable { reason: _ } => ExitSuccess + GateNotRun { cause: cause } => exit_failure( + reason: concat("gate did not run over its subject: ", (cause as String)) + ) + } +} + +data gate_receipt_failure_detail_note: String = "THE COMPANION PROJECTION, and it is a String only because its consumer is. claim_executor derives a _failure_receipt companion from a Bool witness's own name and evaluates it to explain a red (tools.floor_effect_gate_witness floor_gate_failure_receipt_note is that mechanism's authority), so the two CI gates must still be able to hand back a located line. What changes is where the line comes from: it is now PROJECTED from the same receipt that produced the verdict, instead of read out of a second builtin over the same process global. That is the §3 half of this retype -- one authority, two projections -- and it is why no arm here answers a detail the verdict did not produce. Each arm keeps its OWN vocabulary: a gate that did not run says so, and never borrows the subject's ('compile-clean failed'), which is precisely what the two-builtin form could not avoid, because the detail read had no idea which state the verdict read had been in." + +fn gate_outcome_failure_detail(outcome: GateOutcome) -> String { + match outcome { + GateClean => "" + GateFailed { detail: detail } => (detail as String) + } +} + +fn gate_receipt_failure_detail(r: GateReceipt) -> String { + match r { + GateObserved { outcome: outcome } => gate_outcome_failure_detail(outcome: outcome) + GateNotApplicable { reason: reason } => concat( + "gate not applicable over its subject: ", (reason as String) + ) + GateNotRun { cause: cause } => concat( + "gate did not run over its subject: ", (cause as String) + ) + } +} diff --git a/dag/gunbc/ci_spec.dag b/dag/gunbc/ci_spec.dag index 466bec0c5f4..2fe4ee6af08 100644 --- a/dag/gunbc/ci_spec.dag +++ b/dag/gunbc/ci_spec.dag @@ -243,7 +243,7 @@ data gunbc_ci_floor_batch_clamp_params: List = [ gunbc_ci_floor_positional_clamp(overhead_seconds: 125, per_unit_ms: 0), ] -data gunbc_ci_compile_clean_clamp_note: String = "COMPILE-CLEAN LEG CLAMP (prelude coverage, first slice): discharges the compile-clean portion of gunbc_ci_floor_batch_clamp_note FOLLOW-UP ROW (a) — the eager compile-clean install ran OUTSIDE every batch budget and could only red at the step cap, which is how a 15m32s green gate grew past 49 minutes across #7398/#7438 with nothing naming the growth (typecheck-perf investigation, PR #7490). Same shape as the batch clamps: clamp_ms = overhead_seconds*1000 + closure_units * per_unit_ms, where closure_units is the compiled closure's MODULE COUNT — a runtime fact of the scope disposition (whole-tree ~2725 today, affected-set proportional to the diff), so the clamp re-denominates with scope exactly as batch clamps re-denominate with the affected set. Over-clamp is FLOOR-COMPILE-CLEAN-OVER-BUDGET: a typed, located walk refusal (admission grain — the compile receipt's ok is untouched, per the signed admission/verdict split in gunbc_ci_floor_batch_wall_budget_note); never a rerun, never a widen. RED-control hook GUNBC_FLOOR_COMPILE_CLEAN_BUDGET_TIGHTEN_MS lowers the computed clamp (min), never raises. GROWTH DETECTION at row grain is NOT this clamp's job (the family margin ruling, 2026-07-25): per-row 2x drift against dated basis rows rides gunbc.witness_row_cost's comparator over dag/gunbc/compile_clean_cost_basis.tsv — the pass + module_typecheck rows of target/floor-compile-clean-cost-receipt.tsv, basis rows citing arm64 fleet run ids only, BasisAbsent counted until seeded from a cited run's own receipt FILE (the #7475 seeding pattern; an empty basis must count loudly, never read as no-drift). SEEDING SOURCE CORRECTED: this clause used to name the [compile-clean-cost] log lines, because the receipt file had no way off the runner and every row was mirrored into the step log to compensate — ~1,690 lines per floor run, and the same shape cost 8,614 more on the disclosure receipt. THAT REPLACEMENT ROUTE IS NOW GONE TOO, which is the correction this clause carries: it used to say the ci job uploads the receipts as the floor-receipts artifact via gunbc.ci_workflow ci_floor_receipts_upload_step, so seeding downloads the TSV instead of scraping a log. No live workflow carries that step -- it died with ci.yml in the floor cut. TRANSPORT IS NOW PARTIAL RATHER THAN ABSENT, and this clause is written at that grain because the coarser claim went stale within a day: gunbc#8875 (2026-08-22) added an upload to witnesses.yml, so DISPOSITION receipts DO leave the runner today. gunbc#8877 then replaced that single bundled artifact with one artifact per file -- required-floor-disposition, expected-red-roster-join and long-home-storage-agreement -- because the bundled form evaluates if-no-files-found once over the combined list and so cannot report a single missing file. A reader looking for the name required-floor-receipts will not find it; the population is unchanged and none of the cost receipts this note names are in any of the three. So the gap is no longer the absence of any transport; it is that the transport which exists carries a different population, and a reader who sees an artifact on a green run must not infer that these receipts are in it. So this note deliberately retired the log route in favour of an artifact route that was then deleted underneath it, and both of its named routes are inoperative. THE PRODUCER IS UNREACHABLE ON THE NAMED INVOCATION AS WELL, so restoring transport alone would not seed anything: install_floor_compile_clean_receipt's claim_executor caller sits below the required_floor_mode early return, and the only path that could reach it under required CI is the consume_floor_compile_clean_gate_verdict builtin, whose live .dag caller sits in dag/tools/dag_compile_clean_transport -- reached by compile-clean witnesses that are themselves ROUTE-GAPPED and never arrive at their subject. Measured on the certified main run: zero compile-clean-cost markers. NO BASIS MAY BE INFERRED FROM THE AGGREGATE LOG OR FABRICATED FROM AN ABSENT RECEIPT -- an empty basis must count loudly, exactly as this note already requires of BasisAbsent, and that requirement is what forbids papering over the gap while it stands, and the writers no longer mirror their bodies. The log lines are GONE, not merely deprecated: a seeding attempt that greps a run log for them will find nothing, which is why this clause is corrected rather than left to rot. BASIS OF THE CONSTANTS (worker-sized, 2026-07-31, from run 30602520347 @ 0ecb898, host srv1-01 arm64, post-#7490 fixes): whole-tree pass 258s over the ~1648-unit whole-tree entry closure (units = the leg's compiled closure module count, receipted by the first [compile-clean-cost] execution — NOT the ~2725-file module index, which overcounts by pool files outside every entry closure) = ~157ms/unit observed; per_unit_ms 320 is ~2x that rate, funding a full 2x fleet-spread host on top of the observed wall (the family margin ruling: a breach means content grew, never which host answered; pre-fix completing runs spread ~1.8x across hosts) — the batch family's 1000ms coefficient carries 1.4-1.7x the same way; overhead 60s covers the closure-size-independent tail (census fill parse ~13s fleet + governor arm). Whole-tree clamp = 60s + 1648*320ms = ~587s (~2.3x the observed 258s fleet wall). MECHANISM RECEIPTS (local x86, logic-not-cost host): green e2e via gunbc_ci_plan_artifact_plan — pass 310127ms/1648 units, WithinBudget, 1204 module rows, drift basis_absent=1205 counted, exit 0 (run at the pre-resize 200ms sizing; the arm proof is arithmetic-independent and the formula is witness-pinned at the final constants); RED control via GUNBC_FLOOR_COMPILE_CLEAN_BUDGET_TIGHTEN_MS=1 receipted beside it. DISPATCH: operator direction this session ('can we add the budget gating ... i suggest we share that model' — briansrls, 2026-07-31). OPERATOR SIGNATURE (briansrls, 2026-07-31): the worker-sized constants are affirmed as proposed — overhead_seconds 60, per_unit_ms 320 ('the clamp constants you chose are fine, please proceed') — so the refusal arm is signed-live per the family raise discipline; TIGHTENING may still land by ordinary receipt note, and the first fleet observations should tighten per_unit_ms toward the measured rate." +data gunbc_ci_compile_clean_clamp_note: String = "COMPILE-CLEAN LEG CLAMP (prelude coverage, first slice): discharges the compile-clean portion of gunbc_ci_floor_batch_clamp_note FOLLOW-UP ROW (a) — the eager compile-clean install ran OUTSIDE every batch budget and could only red at the step cap, which is how a 15m32s green gate grew past 49 minutes across #7398/#7438 with nothing naming the growth (typecheck-perf investigation, PR #7490). Same shape as the batch clamps: clamp_ms = overhead_seconds*1000 + closure_units * per_unit_ms, where closure_units is the compiled closure's MODULE COUNT — a runtime fact of the scope disposition (whole-tree ~2725 today, affected-set proportional to the diff), so the clamp re-denominates with scope exactly as batch clamps re-denominate with the affected set. Over-clamp is FLOOR-COMPILE-CLEAN-OVER-BUDGET: a typed, located walk refusal (admission grain — the compile receipt's ok is untouched, per the signed admission/verdict split in gunbc_ci_floor_batch_wall_budget_note); never a rerun, never a widen. RED-control hook GUNBC_FLOOR_COMPILE_CLEAN_BUDGET_TIGHTEN_MS lowers the computed clamp (min), never raises. GROWTH DETECTION at row grain is NOT this clamp's job (the family margin ruling, 2026-07-25): per-row 2x drift against dated basis rows rides gunbc.witness_row_cost's comparator over dag/gunbc/compile_clean_cost_basis.tsv — the pass + module_typecheck rows of target/floor-compile-clean-cost-receipt.tsv, basis rows citing arm64 fleet run ids only, BasisAbsent counted until seeded from a cited run's own receipt FILE (the #7475 seeding pattern; an empty basis must count loudly, never read as no-drift). SEEDING SOURCE CORRECTED: this clause used to name the [compile-clean-cost] log lines, because the receipt file had no way off the runner and every row was mirrored into the step log to compensate — ~1,690 lines per floor run, and the same shape cost 8,614 more on the disclosure receipt. THAT REPLACEMENT ROUTE IS NOW GONE TOO, which is the correction this clause carries: it used to say the ci job uploads the receipts as the floor-receipts artifact via gunbc.ci_workflow ci_floor_receipts_upload_step, so seeding downloads the TSV instead of scraping a log. No live workflow carries that step -- it died with ci.yml in the floor cut. TRANSPORT IS NOW PARTIAL RATHER THAN ABSENT, and this clause is written at that grain because the coarser claim went stale within a day: gunbc#8875 (2026-08-22) added an upload to witnesses.yml, so DISPOSITION receipts DO leave the runner today. gunbc#8877 then replaced that single bundled artifact with one artifact per file -- required-floor-disposition, expected-red-roster-join and long-home-storage-agreement -- because the bundled form evaluates if-no-files-found once over the combined list and so cannot report a single missing file. A reader looking for the name required-floor-receipts will not find it; the population is unchanged and none of the cost receipts this note names are in any of the three. So the gap is no longer the absence of any transport; it is that the transport which exists carries a different population, and a reader who sees an artifact on a green run must not infer that these receipts are in it. So this note deliberately retired the log route in favour of an artifact route that was then deleted underneath it, and both of its named routes are inoperative. THE PRODUCER IS UNREACHABLE ON THE NAMED INVOCATION AS WELL, so restoring transport alone would not seed anything: install_floor_compile_clean_receipt's claim_executor caller sits below the required_floor_mode early return, and the only path that could reach it under required CI is the install_or_consume_floor_compile_clean_gate_receipt builtin, whose live .dag caller sits in dag/tools/dag_compile_clean_transport -- reached by compile-clean witnesses that are themselves ROUTE-GAPPED and never arrive at their subject. Measured on the certified main run: zero compile-clean-cost markers. NO BASIS MAY BE INFERRED FROM THE AGGREGATE LOG OR FABRICATED FROM AN ABSENT RECEIPT -- an empty basis must count loudly, exactly as this note already requires of BasisAbsent, and that requirement is what forbids papering over the gap while it stands, and the writers no longer mirror their bodies. The log lines are GONE, not merely deprecated: a seeding attempt that greps a run log for them will find nothing, which is why this clause is corrected rather than left to rot. BASIS OF THE CONSTANTS (worker-sized, 2026-07-31, from run 30602520347 @ 0ecb898, host srv1-01 arm64, post-#7490 fixes): whole-tree pass 258s over the ~1648-unit whole-tree entry closure (units = the leg's compiled closure module count, receipted by the first [compile-clean-cost] execution — NOT the ~2725-file module index, which overcounts by pool files outside every entry closure) = ~157ms/unit observed; per_unit_ms 320 is ~2x that rate, funding a full 2x fleet-spread host on top of the observed wall (the family margin ruling: a breach means content grew, never which host answered; pre-fix completing runs spread ~1.8x across hosts) — the batch family's 1000ms coefficient carries 1.4-1.7x the same way; overhead 60s covers the closure-size-independent tail (census fill parse ~13s fleet + governor arm). Whole-tree clamp = 60s + 1648*320ms = ~587s (~2.3x the observed 258s fleet wall). MECHANISM RECEIPTS (local x86, logic-not-cost host): green e2e via gunbc_ci_plan_artifact_plan — pass 310127ms/1648 units, WithinBudget, 1204 module rows, drift basis_absent=1205 counted, exit 0 (run at the pre-resize 200ms sizing; the arm proof is arithmetic-independent and the formula is witness-pinned at the final constants); RED control via GUNBC_FLOOR_COMPILE_CLEAN_BUDGET_TIGHTEN_MS=1 receipted beside it. DISPATCH: operator direction this session ('can we add the budget gating ... i suggest we share that model' — briansrls, 2026-07-31). OPERATOR SIGNATURE (briansrls, 2026-07-31): the worker-sized constants are affirmed as proposed — overhead_seconds 60, per_unit_ms 320 ('the clamp constants you chose are fine, please proceed') — so the refusal arm is signed-live per the family raise discipline; TIGHTENING may still land by ordinary receipt note, and the first fleet observations should tighten per_unit_ms toward the measured rate." data gunbc_ci_compile_clean_clamp: RunnableBatchClamp = RunnableBatchClamp { overhead: second(count: 60), diff --git a/dag/gunbc/cli_run_hand_rust_area_ledger.dag b/dag/gunbc/cli_run_hand_rust_area_ledger.dag index aa484259166..3bfdea86b8c 100644 --- a/dag/gunbc/cli_run_hand_rust_area_ledger.dag +++ b/dag/gunbc/cli_run_hand_rust_area_ledger.dag @@ -1,32 +1,43 @@ module gunbc.cli_run_hand_rust_area_ledger import gunbc.plans.cli_run_hollowing_plan { cli_run_hollowing_plan } -import std.types { Int, List, String } +import std.types { Int, List, NonEmptyStr, String } -data cli_run_hand_rust_area_ledger_note: String = "LIVE ITEM-GRAIN ledger for cli_run.rs hand Rust (Lane swift-lynx-164). Supersedes cli_run_hollowing_plan §0 stale prose (26,773 LOC / 976 fns dated 2026-07-23). Live scale is measured at execution by scripts/rust_item_census.py — this note does NOT pin numeric literals (DESIGN §3 stale-citation class). Area grain follows the 16 functional areas in gunbc.plans.cli_run_hollowing_plan §2.1–2.16. NOT a per-function ledger (#7074 closed). NOT a deletion plan — instrument only." +data cli_run_hand_rust_area_ledger_note: String = "LIVE ITEM-GRAIN ledger for cli_run.rs hand Rust. Supersedes cli_run_hollowing_plan section 0 stale prose. Area grain follows the 16 functional areas in gunbc.plans.cli_run_hollowing_plan sections 2.1 to 2.16. NOT a per-function ledger. NOT a deletion plan -- instrument only. This note does NOT pin numeric literals, per DESIGN section 3's stale-citation class." -data cli_run_area_2_2_anchor_retirement_receipt: String = "Area 2.2 lost ONE anchor symbol, not the row. handle_run_with_options was the argv-dispatch DRIVER; the cli-run cut (PR 8286) deleted it and rebuilt that seam in main.rs, so its occurrence count in cli_run.rs went 3 to 0 and the symbol no longer names anything. It is removed from anchor_symbols. The ROW SURVIVES because its other two anchors do: claim_batch and claim_executor are both live in the retained engine (19 and 21 occurrences at the time of writing, deliberately not pinned here per the module note's stale-citation rule). The disposition stays RetainedKernel and is unchanged by this edit. +data cli_run_ledger_measurement_route_missing: String = "THE LEDGER HAS NO EXECUTABLE MEASUREMENT ROUTE, AND THIS ROW SAYS SO INSTEAD OF PRETENDING OTHERWISE. Until 2026-08-24 the module note above named scripts/rust_item_census.py as the instrument that re-derived this ledger's live scale at execution -- item identity primary, LOC secondary. THAT FILE IS DELETED. It went with the measurement bankruptcy (gunbc#9132), which removed docs/probes/ whole and left no .sh or .py anywhere in the repository outside .githooks, under the ruling that an ad-hoc script is DESIGN section 6 unmodeled realization: if a measurement is worth re-deriving it is worth a .dag entry point, and if it is not worth an entry point it is not an instrument. So the ledger has been citing a dead instrument since that cut, which is the rot mode DESIGN section 3 predicts of a citation nothing checks. WHAT IS MISSING, precisely, because 'no instrument' is too coarse to act on. Two different measurements have no route, and they fail for different reasons. (1) LIVE SCALE -- how much hand Rust cli_run.rs still carries, at item grain. Nothing in the tree re-derives it. (2) ANCHOR LIVENESS -- whether a symbol named in anchor_symbols still names a declared Rust item, and where. No host builtin answers 'does this Rust symbol exist and in which file'; the module-fact builtins reach .dag modules, not .rs items, so this is not a matter of wiring an existing feed up. RESTORATION TRIGGER: a .dag entry point that walks the seed's Rust sources and returns item identities with their declaring file, cited by name from this module -- at which point both measurements become derivable and anchor_home below stops being an authored field. WHAT THIS ROW DOES NOT CLAIM: that the ledger is unusable meanwhile. The disposition carrier below is now a construction rather than a transcription, which is a real climb and is independent of this gap; what stays unmeasured is the SCALE the ledger reports on, not the READINESS it asserts." -WHY THE GRAIN IS THE ANCHOR SYMBOL AND NOT THE ROW: this ledger was DELETED WHOLE by that same cut and then restored, because deleting it unmarked 22 live areas to retire one symbol. Restoring it unedited would have been the mirror error — an anchor pointing at a symbol that no longer exists is an obligation nobody can discharge, which never retires and reads as live debt forever. Neither whole-file answer was available; both halves are answerable per symbol. That is the same grain rule the cut itself was corrected by, applied one level down." +data cli_run_area_anchor_retirement_receipt: String = "FOUR ANCHOR SYMBOLS ARE RETIRED IN THIS EDIT, AND TWO MORE ARE RE-HOMED. The grain is the anchor symbol, not the row, and the reason is recorded rather than assumed: this ledger was once DELETED WHOLE by a cut and then restored, because deleting it unmarked 22 live areas in order to retire one symbol. Restoring it unedited would have been the mirror error -- an anchor pointing at a symbol that no longer exists is an obligation nobody can discharge, so it never retires and reads as live debt forever. Neither whole-file answer was available; both halves are answerable per symbol.\n\nRETIRED, each because the symbol names nothing in the seed: load_both_closure and run_witness_batch resolve nowhere in src/v1/stage0/src at all; merge_envs survives only inside a prose string in a generated file, its subject having been DELETED by operator ruling on 2026-07-06 (v1.compiler.infer_env visible_bindings_invariant records that deletion, and DESIGN section 6 carries the receipt for why the example that cited it was kept without it); regen_stage0 survives only in generated file headers, its binary having been deleted at the root by the regen cut. Their rows SURVIVE -- 2.4, 2.5, 2.10 and 2.12 each keep their other anchors and their dispositions -- because retiring a symbol is not retiring an area.\n\nRE-HOMED rather than retired: eval_builtin and floor_materialization are both LIVE and neither is in cli_run.rs. eval_builtin is a real function in v1_interpreter.rs, which is correct for area 2.13 (the interpreter seam) and merely not in this ledger's nominal subject file; floor_materialization is a .dag module read from claim_executor.rs. ONE ANCHOR IS ALSO RESPELLED, and it is a different defect from either of the two above: area 2.11 carried the anchor \"compile_clean\", which is a PREFIX rather than a symbol -- it matches compile_clean_scope_plan_for_ci, compile_clean_source_roots, compile_clean_diagnostic_is_hard and a dozen more, so it names no declaration and any liveness check over it answers yes forever regardless of what is actually there. It is replaced by compile_clean_scope_plan_for_ci, a real function in the subject and the symbol DESIGN's CI section already names when it reports that this area's selection capability has no caller. A prefix anchor is the positional-citation failure wearing a name: it looks symbolic and resolves to nothing in particular. That mix is what the anchor_home field below exists to make visible: the previous shape was a bare List, so a reader could not tell an anchor in the subject from an anchor somewhere else in the seed from an anchor naming nothing at all, and all three read identically." -data cli_run_live_scale_receipt: String = "cli_run.rs LIVE SCALE is measured at execution by scripts/rust_item_census.py (item identity primary, LOC secondary). cli_run_hollowing_plan §0 prose (26,773 LOC dated 2026-07-23) is stale. seed-shrink-census Chunk F (~4,165 LOC) remains the dissolution sign-off unit for CI orchestration only." +data cli_run_disposition_is_derived_not_transcribed: String = "THE CARRIER NOW REFUSES AN UNEARNED READINESS, WHICH IS THE POINT OF THIS EDIT. GenerateNow means 'the v2 replacement exists, generate it'. As a BARE VARIANT it was a transcription -- a claim about readiness that only a human's memory could check, and one that had gone false underneath eight rows without any of them changing. The 2026-08-15 floor cut DELETED the machinery two of those rows named as their replacement (gunbc.ci_floor_plan and src/v2/workflow/ci_floor_plan.dag are both absent from the tree) rather than replacing it, and for the other six nothing in the repository establishes that the named v2 authority carries the area -- the module existing is necessary and nowhere near sufficient. A row asserting a readiness with no referent is rung inflation in DESIGN section 4b's sense, and its cost is exactly the one that clause names: an inflated row never ranks for climbing, because it already reports the state it is supposed to reach.\n\nTHE FIX IS CONSTRUCTION, NOT A CORRECTED TRANSCRIPTION. GenerateNow now CARRIES the entry point that emits the area, so the claim cannot be written without naming the thing that would discharge it -- 'name the instrument, never transcribe its output', applied to a disposition. No such entry point can be named for any of the sixteen areas today, so no row is GenerateNow, and that is a fact about the tree rather than a judgement about it. Correspondingly UnclassifiedStopLine carries its cause, so a stop-line row says WHICH of the two situations it is in -- replacement deleted, or replacement never established -- which are different problems with different owners and were previously the same variant.\n\nWHAT THIS DOES NOT CLAIM: that the eight retyped areas are un-generatable, or that the six whose named authority still stands are as far from generation as the two whose authority was deleted. It claims only that nothing in the tree currently establishes readiness, which is what the row is now shaped to record. A row climbs back to GenerateNow the moment someone can name its emitting entry, and that is a one-field edit rather than an argument." type CliRunHandRustAreaDisposition = DeleteNow - | GenerateNow + | GenerateNow { emitting_entry: NonEmptyStr } | ThinHostBoundary | DeleteWithV1 | RetainedKernel - | UnclassifiedStopLine + | UnclassifiedStopLine { cause: NonEmptyStr } + +type CliRunAreaAnchor { + symbol: NonEmptyStr + anchor_home: NonEmptyStr +} type CliRunHandRustAreaRow { area_id: String area_title: String disposition: CliRunHandRustAreaDisposition hollowing_plan_disposition: String - anchor_symbols: List + anchors: List } +data subject: NonEmptyStr = "src/v1/stage0/src/cli_run.rs" as NonEmptyStr + +data replacement_deleted_by_floor_cut: NonEmptyStr = "the named v2 replacement is ABSENT from the tree: gunbc.ci_floor_plan and src/v2/workflow/ci_floor_plan.dag were deleted by the 2026-08-15 floor cut, which removed the machinery rather than replacing it (DESIGN CI section, the declared rung drop)" as NonEmptyStr + +data replacement_not_established: NonEmptyStr = "the named v2 authority is present in the tree but nothing establishes that it carries this area, and no entry point emits it -- necessary is not sufficient, and the module's existence was the whole of the evidence behind the previous GenerateNow" as NonEmptyStr + fn cli_run_hand_rust_area_rows() -> List { [ CliRunHandRustAreaRow { @@ -34,112 +45,161 @@ fn cli_run_hand_rust_area_rows() -> List { area_title: "Workspace & repo paths", disposition: ThinHostBoundary, hollowing_plan_disposition: "emit-when", - anchor_symbols: ["workspace_root", "repo_relative_path"] + anchors: [ + CliRunAreaAnchor { symbol: "workspace_root" as NonEmptyStr, anchor_home: subject }, + CliRunAreaAnchor { symbol: "repo_relative_path" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.2", area_title: "CLI argv & bin dispatch", disposition: RetainedKernel, hollowing_plan_disposition: "seed-kernel-retained", - anchor_symbols: ["claim_batch", "claim_executor"] + anchors: [ + CliRunAreaAnchor { symbol: "claim_batch" as NonEmptyStr, anchor_home: subject }, + CliRunAreaAnchor { symbol: "claim_executor" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.3", area_title: "Corpus discovery & file walk", - disposition: GenerateNow, + disposition: UnclassifiedStopLine { cause: replacement_deleted_by_floor_cut }, hollowing_plan_disposition: "emit-when", - anchor_symbols: ["collect_dag_files", "run_discovery_corpus"] + anchors: [ + CliRunAreaAnchor { symbol: "collect_dag_files" as NonEmptyStr, anchor_home: subject }, + CliRunAreaAnchor { symbol: "run_discovery_corpus" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.4", area_title: "Resolve / typecheck entry orchestration", - disposition: GenerateNow, + disposition: UnclassifiedStopLine { cause: replacement_not_established }, hollowing_plan_disposition: "emit-when", - anchor_symbols: ["resolve_entry_graph", "load_both_closure"] + anchors: [ + CliRunAreaAnchor { symbol: "resolve_entry_graph" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.5", area_title: "Reconcile & env merge", - disposition: GenerateNow, + disposition: UnclassifiedStopLine { cause: replacement_not_established }, hollowing_plan_disposition: "already-subsumed", - anchor_symbols: ["reconcile", "merge_envs"] + anchors: [ + CliRunAreaAnchor { symbol: "reconcile" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.6", area_title: "Typed module cache / memo", - disposition: GenerateNow, + disposition: UnclassifiedStopLine { cause: replacement_not_established }, hollowing_plan_disposition: "emit-when", - anchor_symbols: ["typed_module_cache", "resolved_graph_cache"] + anchors: [ + CliRunAreaAnchor { symbol: "typed_module_cache" as NonEmptyStr, anchor_home: subject }, + CliRunAreaAnchor { symbol: "resolved_graph_cache" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.7", area_title: "Import & module-graph host facts", disposition: ThinHostBoundary, hollowing_plan_disposition: "emit-when", - anchor_symbols: ["import_resolution_facts", "module_declaration_facts"] + anchors: [ + CliRunAreaAnchor { symbol: "import_resolution_facts" as NonEmptyStr, anchor_home: subject }, + CliRunAreaAnchor { symbol: "module_declaration_facts" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.8", area_title: "Reference / cross-tree edges", - disposition: GenerateNow, + disposition: UnclassifiedStopLine { cause: replacement_not_established }, hollowing_plan_disposition: "emit-when", - anchor_symbols: ["reference_resolution_facts", "reference_edges_as_import_facts"] + anchors: [ + CliRunAreaAnchor { symbol: "reference_resolution_facts" as NonEmptyStr, anchor_home: subject }, + CliRunAreaAnchor { symbol: "reference_edges_as_import_facts" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.9", area_title: "Affected-set & diff provenance", - disposition: GenerateNow, + disposition: UnclassifiedStopLine { cause: replacement_not_established }, hollowing_plan_disposition: "emit-when", - anchor_symbols: ["floor_diff_observe", "affected_set"] + anchors: [ + CliRunAreaAnchor { symbol: "floor_diff_observe" as NonEmptyStr, anchor_home: subject }, + CliRunAreaAnchor { symbol: "affected_set" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.10", area_title: "Floor / witness execution", - disposition: GenerateNow, + disposition: UnclassifiedStopLine { cause: replacement_deleted_by_floor_cut }, hollowing_plan_disposition: "emit-when", - anchor_symbols: ["run_discovery_corpus", "run_witness_batch"] + anchors: [ + CliRunAreaAnchor { symbol: "run_discovery_corpus" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.11", area_title: "Compile-clean shard scope", disposition: ThinHostBoundary, hollowing_plan_disposition: "partial", - anchor_symbols: ["dag_compile_clean_scope", "compile_clean"] + anchors: [ + CliRunAreaAnchor { symbol: "dag_compile_clean_scope" as NonEmptyStr, anchor_home: subject }, + CliRunAreaAnchor { symbol: "compile_clean_scope_plan_for_ci" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.12", area_title: "Regen oracle & self-host scope", disposition: DeleteWithV1, hollowing_plan_disposition: "delete-with-v1", - anchor_symbols: ["regen_input_sources", "regen_stage0"] + anchors: [ + CliRunAreaAnchor { symbol: "regen_input_sources" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.13", area_title: "Host builtin bridge", disposition: RetainedKernel, hollowing_plan_disposition: "seed-kernel-retained", - anchor_symbols: ["eval_builtin", "filesystem_read"] + anchors: [ + CliRunAreaAnchor { + symbol: "eval_builtin" as NonEmptyStr, + anchor_home: "src/v1/stage0/src/v1_interpreter.rs" as NonEmptyStr + }, + CliRunAreaAnchor { symbol: "filesystem_read" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.14", area_title: "Lens census / hygiene host feeds", - disposition: GenerateNow, + disposition: UnclassifiedStopLine { cause: replacement_not_established }, hollowing_plan_disposition: "emit-when", - anchor_symbols: ["non_fold_residue", "fact_cardinality"] + anchors: [ + CliRunAreaAnchor { symbol: "non_fold_residue" as NonEmptyStr, anchor_home: subject }, + CliRunAreaAnchor { symbol: "fact_cardinality" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.15", area_title: "Floor observability & adaptive width", disposition: ThinHostBoundary, hollowing_plan_disposition: "partial", - anchor_symbols: ["floor_materialization", "memory_governor"] + anchors: [ + CliRunAreaAnchor { + symbol: "floor_materialization" as NonEmptyStr, + anchor_home: "dag/gunbc/floor_materialization.dag" as NonEmptyStr + }, + CliRunAreaAnchor { symbol: "memory_governor" as NonEmptyStr, anchor_home: subject } + ] }, CliRunHandRustAreaRow { area_id: "2.16", area_title: "Test-migration debt builtins", disposition: DeleteWithV1, hollowing_plan_disposition: "delete-with-v1", - anchor_symbols: ["test_migration_debt"] + anchors: [ + CliRunAreaAnchor { symbol: "test_migration_debt" as NonEmptyStr, anchor_home: subject } + ] } ] } @@ -151,3 +211,27 @@ fn cli_run_hand_rust_area_row_count() -> Int { fn cli_run_hand_rust_area_ledger_covers_sixteen_areas() -> Bool { cli_run_hand_rust_area_row_count() == 16 } + +data generate_now_row_count_note: String = "The readiness reader, and it counts ROWS rather than answering a Bool so that a caller can tell 'none are ready' from 'the ledger is empty'. Its RED is authorable in a fixture -- a test module constructs a row carrying GenerateNow with an emitting entry -- which is what keeps the live-tree assertion in dag/test/claim/cli_run_area_ledger_witness_test.dag a check rather than a decoration." + +fn cli_run_area_generate_now_row_count(rows: List) -> Int { + fold(rows, init: 0, f: (acc, r) => match r.disposition { + GenerateNow { emitting_entry: _ } => acc + 1 + DeleteNow => acc + ThinHostBoundary => acc + DeleteWithV1 => acc + RetainedKernel => acc + UnclassifiedStopLine { cause: _ } => acc + }) +} + +fn cli_run_area_stop_line_row_count(rows: List) -> Int { + fold(rows, init: 0, f: (acc, r) => match r.disposition { + UnclassifiedStopLine { cause: _ } => acc + 1 + GenerateNow { emitting_entry: _ } => acc + DeleteNow => acc + ThinHostBoundary => acc + DeleteWithV1 => acc + RetainedKernel => acc + }) +} diff --git a/dag/gunbc/compile_clean_diagnostic_policy.dag b/dag/gunbc/compile_clean_diagnostic_policy.dag index 81e2749c33f..9594324011d 100644 --- a/dag/gunbc/compile_clean_diagnostic_policy.dag +++ b/dag/gunbc/compile_clean_diagnostic_policy.dag @@ -9,7 +9,7 @@ type UnlistedImportUseEnforcement = FloorNotYet | Enforced -data unlisted_import_use_enforcement_note: String = "Single policy authority for whether UnlistedImportUse blocks compile-clean (issue 11 / ci-floor-child-spawn-attribution section 7). FloorNotYet = advisory (current namespace-lane staging: the resolver emits UnlistedImportUse but compile-clean does not red). Enforced = blocking (terminal promotion when namespace-only resolution deletes the import grammar — DISSOLVES WHEN UnlistedImportUse promoted to an error per namespace_import_closure_behavioral_transport.dag:15). BOTH the floor receipt path (consume_floor_compile_clean_gate_verdict via floor_compile_clean_emit_ok_via_index) and the standalone CLI transport (gunbc compile --target dag) read this row — never restate the predicate in either consumer (DESIGN section 3)." +data unlisted_import_use_enforcement_note: String = "Single policy authority for whether UnlistedImportUse blocks compile-clean (issue 11 / ci-floor-child-spawn-attribution section 7). FloorNotYet = advisory (current namespace-lane staging: the resolver emits UnlistedImportUse but compile-clean does not red). Enforced = blocking (terminal promotion when namespace-only resolution deletes the import grammar — DISSOLVES WHEN UnlistedImportUse promoted to an error per namespace_import_closure_behavioral_transport.dag:15). BOTH the floor receipt path (install_or_consume_floor_compile_clean_gate_receipt via floor_compile_clean_emit_ok_via_index) and the standalone CLI transport (gunbc compile --target dag) read this row — never restate the predicate in either consumer (DESIGN section 3)." data compile_clean_unlisted_import_use_enforcement: UnlistedImportUseEnforcement = FloorNotYet diff --git a/dag/gunbc/seed_growth_admission.dag b/dag/gunbc/seed_growth_admission.dag index 42781770f14..58de070c0cd 100644 --- a/dag/gunbc/seed_growth_admission.dag +++ b/dag/gunbc/seed_growth_admission.dag @@ -20,7 +20,7 @@ import std.roster_frontier { import std.types { Bool, Int, List, String } import v2.std.algebra { any, filter, fold_list, length, list_append } -data seed_growth_admission_note: String = "ITEM-GRAIN admission authority for hand-authored Rust growth (Lane swift-lynx-164). TARGET: compare every newly authored or modified hand Rust item in a change against SeedGrowthJustification.hand_authored_declarations and refuse on the difference (gunbc.seed_growth.seed_growth_note completeness join). PATH-GRAIN census (sibling proud-owl-773 PR #7894) answers which files lack disposition; THIS MODULE answers which ITEMS within files lack justification. NOT IN SCOPE: deleting existing Rust. NOT IN SCOPE: netting deletions against additions. G0 HOST: GONE. scripts/rust_item_census.py was SCAFFOLD-MARKED (seed_growth_g0_census_host_scaffold) and was DELETED from the tree by gunbc#9132, which bankrupted the measurement corpus and left no .sh or .py anywhere outside .githooks. This row cited it in the present tense until 2026-08-24; a reader planning against that sentence would have looked for a producer that does not exist, which is the positional-citation decay DESIGN 3 names, arriving here as a path rather than a line. TWO FURTHER ROWS IN THIS SAME FILE asserted the script was the current host -- seed_growth_g0_census_host_scaffold_note and seed_growth_admission_g0_population_note -- and they ARE repaired in this change, because a module that answers two ways about one fact is the DESIGN §3 violation this correction exists to remove, and leaving them would have made this file its own counter-example (caught by review 55623; an earlier revision of this sentence listed only the sibling modules and omitted the local pair, which is how the contradiction survived the first pass). Five SIBLING modules still carry the same dead citation (gunbc.bare_reference_scanner_admission, gunbc.cli_run_hand_rust_area_ledger, gunbc.rust_item_identity and two witness tests); those are NOT repaired here, and that is the residue gunbc#9132 declared it was leaving rather than a gap this change opened. Item extraction has no host at all until rust_item_host_observation lands, so the G0 interim path is not merely scaffolded now -- it is absent. ENROLLED TODAY: seed_growth_roster_well_formed_gate_holds — roster well-formedness only (non-empty closed roster, well-formed rows, no duplicate DeclarationRef keys). NOT ENROLLED: seed_growth_join_declarations as admission — diff candidates absent until rust_item_host_observation; seed_growth_admission_join_scaffold marks that boundary." +data seed_growth_admission_note: String = "ITEM-GRAIN admission authority for hand-authored Rust growth (Lane swift-lynx-164). TARGET: compare every newly authored or modified hand Rust item in a change against SeedGrowthJustification.hand_authored_declarations and refuse on the difference (gunbc.seed_growth.seed_growth_note completeness join). PATH-GRAIN census (sibling proud-owl-773 PR #7894) answers which files lack disposition; THIS MODULE answers which ITEMS within files lack justification. NOT IN SCOPE: deleting existing Rust. NOT IN SCOPE: netting deletions against additions. G0 HOST: GONE. scripts/rust_item_census.py was SCAFFOLD-MARKED (seed_growth_g0_census_host_scaffold) and was DELETED from the tree by gunbc#9132, which bankrupted the measurement corpus and left no .sh or .py anywhere outside .githooks. This row cited it in the present tense until 2026-08-24; a reader planning against that sentence would have looked for a producer that does not exist, which is the positional-citation decay DESIGN 3 names, arriving here as a path rather than a line. TWO FURTHER ROWS IN THIS SAME FILE asserted the script was the current host -- seed_growth_g0_census_host_scaffold_note and seed_growth_admission_g0_population_note -- and they ARE repaired in this change, because a module that answers two ways about one fact is the DESIGN §3 violation this correction exists to remove, and leaving them would have made this file its own counter-example (caught by review 55623; an earlier revision of this sentence listed only the sibling modules and omitted the local pair, which is how the contradiction survived the first pass). THREE SIBLING modules still carry the same dead citation as if it were live (gunbc.bare_reference_scanner_admission, gunbc.rust_item_identity, and dag/test/claim/rust_item_identity_witness_test); they are NOT repaired here, and that is the residue gunbc#9132 declared it was leaving rather than a gap this change opened. IT WAS FIVE UNTIL 2026-08-25, and the two that left are recorded here rather than silently subtracted, because a count that moves without saying why is the transcription this repository keeps paying for: gunbc.cli_run_hand_rust_area_ledger and its witness were repaired together, the ledger replacing the citation with a declared missing-measurement-route row and the witness dropping an assertion that the dead path STILL APPEARED in that prose -- which is why the pair had to move together, the witness having been the thing holding the ledger's dead citation green. Item extraction has no host at all until rust_item_host_observation lands, so the G0 interim path is not merely scaffolded now -- it is absent. ENROLLED TODAY: seed_growth_roster_well_formed_gate_holds — roster well-formedness only (non-empty closed roster, well-formed rows, no duplicate DeclarationRef keys). NOT ENROLLED: seed_growth_join_declarations as admission — diff candidates absent until rust_item_host_observation; seed_growth_admission_join_scaffold marks that boundary." type SeedGrowthAdmissionVerdict = SeedGrowthAdmissionComplete { diff --git a/dag/gunbc/v1_interpreter_primitive_surface.dag b/dag/gunbc/v1_interpreter_primitive_surface.dag index 62d6064fddb..dc2374c01f8 100644 --- a/dag/gunbc/v1_interpreter_primitive_surface.dag +++ b/dag/gunbc/v1_interpreter_primitive_surface.dag @@ -1085,36 +1085,36 @@ fn v1_interpreter_authored_roster_arms() -> List List { "compile_dag_rust_emit_check", "witness_layer_roots_compile_clean_check", "witness_layer_roots_compile_clean_emit_check", - "consume_floor_compile_clean_gate_verdict", - "consume_floor_compile_clean_gate_failure_detail", + "install_or_consume_floor_compile_clean_gate_receipt", "record_generated_artifact_drift_gate_failure_detail", - "consume_generated_artifact_drift_gate_failure_detail", + "record_generated_artifact_drift_gate_clean", + "consume_generated_artifact_drift_gate_receipt", "witness_compile_clean_cli_floor_verdicts_agree", "test_migration_debt_module_names", "test_migration_legacy_behavior_ids", diff --git a/dag/test/claim/cli_run_hand_rust_area_ledger_witness_test.dag b/dag/test/claim/cli_run_hand_rust_area_ledger_witness_test.dag index e906c1a5dd8..83bdf030497 100644 --- a/dag/test/claim/cli_run_hand_rust_area_ledger_witness_test.dag +++ b/dag/test/claim/cli_run_hand_rust_area_ledger_witness_test.dag @@ -1,21 +1,92 @@ module test.claim.cli_run_hand_rust_area_ledger_witness import gunbc.cli_run_hand_rust_area_ledger { + CliRunAreaAnchor, + CliRunHandRustAreaDisposition, + CliRunHandRustAreaRow, + GenerateNow, + RetainedKernel, + UnclassifiedStopLine, + cli_run_area_generate_now_row_count, + cli_run_area_stop_line_row_count, cli_run_hand_rust_area_ledger_covers_sixteen_areas, cli_run_hand_rust_area_ledger_note, - cli_run_live_scale_receipt + cli_run_hand_rust_area_rows } +import std.types { Int, List, NonEmptyStr } import v2.std.text { String } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } -test fn cli_run_area_ledger_covers_sixteen_areas() -> Bool { - cli_run_hand_rust_area_ledger_covers_sixteen_areas() +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data ledger_witness_scope_note: String = "WHAT REPLACED THE PREVIOUS SHAPE, AND WHY IT IS NOT AN EQUIVALENT CHECK. This file used to assert that a prose row CONTAINED the substring 'scripts/rust_item_census.py'. That is the prose-self-match antipattern in its purest form -- the assertion's only content was that someone had written a path into a string -- and it was worse than empty, because the path it pinned had been DELETED from the tree by gunbc#9132 and this witness was the thing keeping the dead citation green. A check whose sole failure mode is 'the sentence was edited' cannot tell a repair from a regression, and here it actively defended the regression.\n\nWHAT IS ASSERTED NOW IS STRUCTURE OVER THE ROWS. The load-bearing one is that the LIVE ledger carries no GenerateNow row, because GenerateNow now carries the entry point that emits the area and no such entry point can be named for any of the sixteen. Its RED IS AUTHORABLE and is authored below rather than argued for: the fixture arm constructs a GenerateNow row and requires the counter to see it. Without that arm the live assertion would be a decoration -- permanently green because the counter could be broken in a way that returns zero for every input, which is exactly the shape DESIGN section 4b calls worse than absent. The two arms together are the check: one says the counter can count, the other says the tree has nothing to count." + +data fixture_generate_now_row: CliRunHandRustAreaRow = CliRunHandRustAreaRow { + area_id: "fixture", + area_title: "fixture row asserting the counter can return non-zero", + disposition: GenerateNow { + emitting_entry: "dag/test/fixture/not-a-real-entry.dag" as NonEmptyStr + }, + hollowing_plan_disposition: "fixture", + anchors: [ + CliRunAreaAnchor { + symbol: "fixture_symbol" as NonEmptyStr, + anchor_home: "src/v1/stage0/src/cli_run.rs" as NonEmptyStr + } + ] } -test fn cli_run_live_scale_receipt_updates_stale_prose() -> Bool { - string_contains(s: cli_run_live_scale_receipt, pattern: "scripts/rust_item_census.py") - && string_contains(s: cli_run_live_scale_receipt, pattern: "cli_run_hollowing_plan") +data fixture_retained_row: CliRunHandRustAreaRow = CliRunHandRustAreaRow { + area_id: "fixture", + area_title: "fixture row that must NOT be counted as ready", + disposition: RetainedKernel, + hollowing_plan_disposition: "fixture", + anchors: [] +} + +test fn cli_run_area_ledger_covers_sixteen_areas() -> Bool { + cli_run_hand_rust_area_ledger_covers_sixteen_areas() } test fn cli_run_area_ledger_is_instrument_not_deletion() -> Bool { string_contains(s: cli_run_hand_rust_area_ledger_note, pattern: "NOT a deletion plan") } + +// The positive control, and it is stated FIRST because the live assertion below is +// uninterpretable without it: a counter that answered zero for every input would pass that +// assertion while establishing nothing. +test fn generate_now_counter_sees_a_generate_now_row() -> Bool { + cli_run_area_generate_now_row_count(rows: [fixture_generate_now_row]) == 1 + && cli_run_area_generate_now_row_count(rows: [fixture_retained_row]) == 0 + && cli_run_area_generate_now_row_count( + rows: [fixture_generate_now_row, fixture_retained_row] + ) == 1 +} + +// The load-bearing assertion. GenerateNow means the v2 replacement exists and the area can be +// generated NOW; the variant carries the entry point that would do it, so the claim cannot be +// written without naming the thing that discharges it. Nothing in the tree can be named today. +// This goes RED the moment someone re-classifies a row as ready, which is the point: a return +// to GenerateNow should require naming an emitting entry, not just editing a variant. +test fn live_ledger_asserts_no_unearned_readiness() -> Bool { + cli_run_area_generate_now_row_count(rows: cli_run_hand_rust_area_rows()) == 0 +} + +// Stop-line rows must actually be present: the previous shape had eight rows asserting a +// readiness with no referent, and a retype that quietly emptied the ledger of stop lines would +// be indistinguishable from one that resolved them. +test fn live_ledger_records_its_stop_lines() -> Bool { + cli_run_area_stop_line_row_count(rows: cli_run_hand_rust_area_rows()) > 0 + && cli_run_area_stop_line_row_count(rows: [fixture_retained_row]) == 0 +} + +// Every anchor names where it lives. The previous shape was a bare List, under which an +// anchor in cli_run.rs, an anchor elsewhere in the seed, and an anchor naming nothing at all +// were the same value. +test fn every_anchor_carries_its_home() -> Bool { + fold(cli_run_hand_rust_area_rows(), init: true, f: (acc, r) => + acc && fold(r.anchors, init: true, f: (inner, a) => + inner && (a.anchor_home as String) != "" && (a.symbol as String) != "" + ) + ) +} diff --git a/dag/test/claim/gate_receipt_witness_test.dag b/dag/test/claim/gate_receipt_witness_test.dag new file mode 100644 index 00000000000..70a5d4b36eb --- /dev/null +++ b/dag/test/claim/gate_receipt_witness_test.dag @@ -0,0 +1,96 @@ +module test.claim.gate_receipt_witness + +import gunbc.ci_gate { + GateReceipt, GateOutcome, + GateObserved, GateNotApplicable, GateNotRun, + GateClean, GateFailed, + gate_receipt_exit, gate_receipt_failure_detail +} +import std.process { ProcessExit, ExitSuccess, ExitFailure } +import std.types { String, NonEmptyStr, Bool } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data gate_receipt_witness_scope_note: String = "SubstrateInputsOnly, and that is the honest declaration rather than a convenience: every subject here is a hand-constructed GateReceipt, and the projections under test are pure folds over it. Nothing calls the host builtins that PRODUCE a receipt. WHAT THESE PROVE: that the three arms reach three DIFFERENT places, in both the exit projection and the detail projection. WHAT THEY DO NOT PROVE: that the host maps its own states onto the right arms -- that half is asserted by the cargo tests beside the globals in cli_run.rs (floor_compile_clean_gate_separates_not_applicable_from_clean and generated_artifact_drift_gate_separates_unrecorded_from_clean), because only there can a receipt fixture be installed into the process global the builtin reads. The two halves are complementary and neither is the other's substitute: a host that mapped every state to GateNotRun would pass every witness in this file." + +data gate_receipt_discrimination_note: String = "THE ASSERTIONS ARE WRITTEN AS DISCRIMINATIONS, not as arm-by-arm value checks, because an arm-by-arm check greens on a projection that collapses two arms as long as each row is read separately. The predecessor of this carrier answered Bool, where NotApplicable and Clean were BOTH true and NotRun and Failed were BOTH false; the pairs asserted below are exactly those two collapses, so each one goes red against the shape this retype replaced. That is the discriminating RED this evidence is enrolled for, and it stays enrolled after the climb rather than retiring with it (DESIGN 4b meta-obligation 4: a climb dissolves the redundant production machinery, never the evidence that the higher rung is still real)." + +data clean_receipt: GateReceipt = GateObserved { outcome: GateClean } +data failed_receipt: GateReceipt = GateObserved { + outcome: GateFailed { detail: "dag compile-clean: unresolved import at dag/x.dag" as NonEmptyStr } +} +data not_applicable_receipt: GateReceipt = GateNotApplicable { + reason: "compile-clean scope: no shard intersection" as NonEmptyStr +} +data not_run_receipt: GateReceipt = GateNotRun { + cause: "compile-clean gate: no in-run compile receipt" as NonEmptyStr +} + +fn exit_is_success(e: ProcessExit) -> Bool { + match e { + ExitSuccess => true + ExitFailure { code: _, reason: _ } => false + } +} + +fn exit_reason(e: ProcessExit) -> String { + match e { + ExitSuccess => "" + ExitFailure { code: _, reason: reason } => reason + } +} + +test fn clean_and_failed_exit_differently() -> Bool { + exit_is_success(e: gate_receipt_exit(r: clean_receipt)) + && !exit_is_success(e: gate_receipt_exit(r: failed_receipt)) +} + +// The first of the two Bool collapses: a scope disposition that selected nothing and a gate +// that never reached its subject were the SAME false under the predecessor. They must exit +// differently, because only one of them is a statement about the tree. +test fn not_applicable_and_not_run_exit_differently() -> Bool { + exit_is_success(e: gate_receipt_exit(r: not_applicable_receipt)) + && !exit_is_success(e: gate_receipt_exit(r: not_run_receipt)) +} + +// The second collapse: NotRun and Failed both stopped the line before, and both still do -- +// so an exit-status assertion alone cannot separate them. The REASON is what carries the +// distinction, and a reader of a red must be able to tell "the gate did not run" from "the +// gate ran and refused the tree". +test fn not_run_stops_the_line_in_its_own_vocabulary() -> Bool { + let not_run_reason = exit_reason(e: gate_receipt_exit(r: not_run_receipt)) + let failed_reason = exit_reason(e: gate_receipt_exit(r: failed_receipt)) + !exit_is_success(e: gate_receipt_exit(r: not_run_receipt)) + && not_run_reason != failed_reason + && not_run_reason != "" +} + +test fn failure_detail_is_empty_only_when_the_gate_ran_clean() -> Bool { + gate_receipt_failure_detail(r: clean_receipt) == "" + && gate_receipt_failure_detail(r: failed_receipt) != "" + && gate_receipt_failure_detail(r: not_applicable_receipt) != "" + && gate_receipt_failure_detail(r: not_run_receipt) != "" +} + +// The detail projection must not answer a state's text out of a DIFFERENT state's vocabulary: +// four distinct receipts, four distinct lines. This is what makes the companion a projection +// of the receipt rather than a second read that has to guess which state produced it. +test fn every_arm_projects_its_own_detail() -> Bool { + let clean = gate_receipt_failure_detail(r: clean_receipt) + let failed = gate_receipt_failure_detail(r: failed_receipt) + let not_applicable = gate_receipt_failure_detail(r: not_applicable_receipt) + let not_run = gate_receipt_failure_detail(r: not_run_receipt) + clean != failed + && failed != not_applicable + && not_applicable != not_run + && not_run != failed +} + +// The failing side carries the LOCATED text the gate produced, not a fixed gate-level string. +// Before this retype the gate body invented its own constant reason on the false side while +// the located diagnostic lived in a separate builtin, so the two could not both be true. +test fn failed_detail_is_the_receipts_own_located_text() -> Bool { + gate_receipt_failure_detail(r: failed_receipt) + == "dag compile-clean: unresolved import at dag/x.dag" +} diff --git a/dag/tools/dag_compile_clean_gate.dag b/dag/tools/dag_compile_clean_gate.dag index 04717f3dcc6..2d2c3ae4d9e 100644 --- a/dag/tools/dag_compile_clean_gate.dag +++ b/dag/tools/dag_compile_clean_gate.dag @@ -1,9 +1,10 @@ module tools.dag_compile_clean_gate import std.process { ProcessExit, ExitSuccess, exit_failure } +import gunbc.ci_gate { gate_receipt_exit, gate_receipt_failure_detail } import tools.dag_compile_clean_transport { run_clean_tree_compile } -data dag_compile_clean_failure_receipt_note: String = "The loudness half: the floor witness collapses this gate's ProcessExit to Bool via tools.ci_gates.exit_ok, so compile-clean reds reported only returned Bool(false). The gate consumes the executor's one in-run compile receipt; the failure-receipt companion projects the same receipt's located diagnostic without a second compile." +data dag_compile_clean_failure_receipt_note: String = "The loudness half: the floor witness collapses this gate's ProcessExit to Bool via tools.ci_gates.exit_ok, so compile-clean reds reported only returned Bool(false). The gate consumes the executor's one in-run compile receipt; the failure-receipt companion projects the same receipt's located diagnostic without a second compile. BOTH HALVES NOW READ ONE RECEIPT. Until this retype the body branched on a Bool and, on the false side, INVENTED its own reason -- the fixed string 'dag compile-clean gate failed: clean-tree compile over witness layer roots' -- while the companion read the located detail from a SECOND builtin over the same process global. So the exit reason a reader saw was a constant that could not distinguish a failed compile from a gate that never ran, and the only text that could was somewhere else. Now the receipt carries its verdict and its detail together and gunbc.ci_gate projects both." fn dag_compile_clean_failure_reason(exit: ProcessExit) -> String { match exit { @@ -13,13 +14,7 @@ fn dag_compile_clean_failure_reason(exit: ProcessExit) -> String { } func run_dag_compile_clean_gate_body() -> ProcessExit { - if run_clean_tree_compile() { - ExitSuccess - } else { - exit_failure( - reason: "dag compile-clean gate failed: clean-tree compile over witness layer roots" - ) - } + gate_receipt_exit(r: run_clean_tree_compile()) } func run_dag_compile_clean_gate() -> ProcessExit { @@ -27,7 +22,7 @@ func run_dag_compile_clean_gate() -> ProcessExit { } func dag_compile_clean_failure_receipt() -> String { - consume_floor_compile_clean_gate_failure_detail() + gate_receipt_failure_detail(r: run_clean_tree_compile()) } func main() -> ProcessExit { diff --git a/dag/tools/dag_compile_clean_transport.dag b/dag/tools/dag_compile_clean_transport.dag index 4f12caa96bb..be203ffcc5f 100644 --- a/dag/tools/dag_compile_clean_transport.dag +++ b/dag/tools/dag_compile_clean_transport.dag @@ -5,6 +5,7 @@ import extdeps.filesystem.filesystem_io import extdeps.git import extdeps.git.inspect import extdeps.gunbc +import gunbc.ci_gate { GateReceipt } import gunbc.ci_layer_roots { compile_clean_source_roots } import gunbc.output_policy { ExpectFailure, ExpectSuccess } import std.logic { Bool } @@ -78,8 +79,10 @@ fn run_clean_tree_compile_typed() -> Bool { } } -fn run_clean_tree_compile() -> Bool { - consume_floor_compile_clean_gate_verdict() +data run_clean_tree_compile_receipt_note: String = "The name is unchanged and the return type is not: this used to answer Bool via consume_floor_compile_clean_gate_verdict, which folded five host states into false and the scope disposition's skip into true. The builtin behind it is now spelled install_or_consume_floor_compile_clean_gate_receipt, and that spelling carries a fact the old one hid -- under the executor's lazy-install arm the FIRST call here RUNS THE WHOLE-TREE COMPILE. The predecessor was spelled consume_ and documented as reading the receipt only, so nothing at this call site said that a boolean read could cost a whole-tree compile." + +fn run_clean_tree_compile() -> GateReceipt { + install_or_consume_floor_compile_clean_gate_receipt() } data perturb_module_source: String = "module test.perturb_compile_clean_red\nfn probe() -> String? {\n match Present { value: \"x\" } {\n Some { value: s } => Some { value: s }\n None => none\n }\n}" diff --git a/dag/tools/generated_artifact_gate.dag b/dag/tools/generated_artifact_gate.dag index 2debf80f6b8..6dbaab9fcc0 100644 --- a/dag/tools/generated_artifact_gate.dag +++ b/dag/tools/generated_artifact_gate.dag @@ -3,6 +3,7 @@ module tools.generated_artifact_gate import std.process { ProcessExit, ExitSuccess, exit_failure } import extdeps.filesystem.filesystem_io { Filesystem } +import gunbc.ci_gate { gate_receipt_failure_detail } import gunbc.generated_artifact { GeneratedArtifact, committed_generated_artifacts, @@ -38,7 +39,9 @@ func run_generated_artifact_drift_gate_body() -> ProcessExit { " — it is a GENERATED projection of its .dag authority; do not hand-edit, regenerate via main_wet on dag/tools/generated_artifact_gate.dag" ) } - if !all_ok { + if all_ok { + record_generated_artifact_drift_gate_clean() + } else { record_generated_artifact_drift_gate_failure_detail(detail: reason) } return if all_ok { @@ -56,7 +59,7 @@ func run_generated_artifact_drift_gate() -> ProcessExit { run_generated_artifact_drift_gate_body() } -data generated_artifact_drift_failure_receipt_note: String = "The loudness half: the floor witness collapses this gate's ProcessExit to Bool via tools.ci_gates.exit_ok, so a generated-artifact drift red reported only returned Bool(false) without the located path. The gate body records the reason from its single observe_generated_artifact_population pass; the failure-receipt companion consumes that retained detail instead of re-observing." +data generated_artifact_drift_failure_receipt_note: String = "The loudness half: the floor witness collapses this gate's ProcessExit to Bool via tools.ci_gates.exit_ok, so a generated-artifact drift red reported only returned Bool(false) without the located path. The gate body records the reason from its single observe_generated_artifact_population pass; the failure-receipt companion consumes that retained detail instead of re-observing. THE BODY NOW RECORDS THE CLEAN SIDE TOO, and that is the whole point of the change rather than a tidy-up. Before it, only the FAILING side wrote, so the global's unset state carried two facts at once -- the body ran and found no drift, and the body never ran in this process -- and the companion papered the second over with the fabricated prose 'gate body did not run in this process' handed back as if it were a drift detail. Nothing downstream could tell an unguarded run from a clean one, which is DESIGN's execution-provenance rule exactly: a stage that can prevent an observation from executing must participate in the observation carrier, so refused-before-observing cannot inhabit the same state as observed-nothing. Recording the clean side is what makes GateNotRun mean only the thing it says." fn generated_artifact_drift_failure_reason(exit: ProcessExit) -> String { match exit { @@ -66,7 +69,7 @@ fn generated_artifact_drift_failure_reason(exit: ProcessExit) -> String { } func generated_artifact_drift_failure_receipt() -> String { - consume_generated_artifact_drift_gate_failure_detail() + gate_receipt_failure_detail(r: consume_generated_artifact_drift_gate_receipt()) } func main_wet() -> ProcessExit { diff --git a/docs/plans/ci-floor-child-spawn-attribution.md b/docs/plans/ci-floor-child-spawn-attribution.md index 88eb587c774..fe1daaf6cef 100644 --- a/docs/plans/ci-floor-child-spawn-attribution.md +++ b/docs/plans/ci-floor-child-spawn-attribution.md @@ -126,7 +126,7 @@ Standalone `gunbc compile --target dag` over the three witness-layer roots (`dag `src/v1` — the exact `compile_clean_source_roots()` set) exits **rc=1 with 2652 `UnlistedImportUse` errors** on the tree CI greens (identical count at 2 and 3 roots). CI's compile-clean gate does **not** exercise this path: it consumes `claim_executor`'s internal shared-index compile receipt -(`run_clean_tree_compile` → `consume_floor_compile_clean_gate_verdict`), and the CLI transport +(`run_clean_tree_compile` → `install_or_consume_floor_compile_clean_gate_receipt`), and the CLI transport (`run_clean_tree_compile_typed` / `run_dag_compile_clean_gate_shell`) has no in-tree caller. `UnlistedImportUse` is precisely the resolver class the namespace-resolution lane is mid-promotion on (`namespace_import_closure_behavioral_transport.dag:15`: "DISSOLVES WHEN … UnlistedImportUse diff --git a/src/v1/04_method.dag b/src/v1/04_method.dag index f38113e6c70..670101926ea 100644 --- a/src/v1/04_method.dag +++ b/src/v1/04_method.dag @@ -56,6 +56,8 @@ fn builtin_kernel_seed_diagnostics() -> List { data compile_dag_diagnostic_census_row_note: String = "WHY THIS ROW EXISTS, and why it is additive rather than contested (ladder-probe-corpus, operator-amended scope 2026-08-01). Its sibling compile_dag_rust_emit_check compiles a synthetic source and collapses the whole result to a Bool - it counts diagnostics passing compile_clean_diagnostic_is_hard and answers false when that count is nonzero. That discards three facts the guarantee probe corpus must observe: WHICH judgment fired (a probe refusing for any hard reason, a typo included, otherwise reads as the wall firing), whether it BLOCKS (the filter IS the severity predicate, so demoting a landed wall from blocking to advisory turns its RED silently green), and every advisory (so a positive control cannot state zero-diagnostics-of-ANY-severity, the assertion codex review 45357 added after an advisory MethodExistenceUndecided passed unnoticed as a green control). The Stage-0 receipt vocabulary gunbc.guarantee_measurement makes the gap structural rather than stylistic: RefusedTyped and AcceptedCounted both carry a diagnostic class and a count, and neither is inhabitable from a Bool, so without this row that schema is uninhabitable on every v1 path. MEASUREMENT ONLY - the host arm reports what the compile decided and filters nothing; callers filter. Registered as a type variable rather than a kernel record because the result is a COPRODUCT (observed census vs typed not-runnable, the top-as-answer/top-as-ignorance split), following shell_materialize_operation_argv's argv_materialization_result precedent; filesystem_read_result_type's make_kernel_record_type idiom is the right one only for a product. DISSOLUTION, answering the compile_clean_forcecheck objection in place: this registry is itself a flat global map that plan argues is a section-3 fork awaiting the PrimitiveDefinition identity join, and this row inherits that trigger EXACTLY as its sibling does - when the join dissolves the registry, the two migrate together. One additive row is linear cost against that dissolution; the alternative was a schema no v1 probe could inhabit." +data gate_receipt_rows_note: String = "THE TWO CI-GATE ROWS ANSWER A COPRODUCT, and the reason is the same one compile_dag_diagnostic_census_row_note gives one row up. Their predecessors were three rows -- consume_floor_compile_clean_gate_verdict as bool_type, consume_floor_compile_clean_gate_failure_detail as string_type, consume_generated_artifact_drift_gate_failure_detail as string_type -- and the Bool folded FIVE host states into false (lock poisoned, install failed, no in-run receipt, the receipt's typed Refused arm, and a real failed compile) while folding the scope disposition's Skipped into true. The String companions were second builtins over the SAME process global, so a caller reconstructed one fact from two correlated reads, and the generated-artifact one fabricated prose for the state the Bool had already erased. gunbc.ci_gate GateReceipt is the single carrier: GateObserved holds the verdict WITH its located detail, GateNotApplicable is the scope disposition answering, GateNotRun is could-not-measure. Registered as a type variable rather than a kernel record for the reason its two siblings are -- the result is a coproduct, so make_kernel_record_type is the wrong idiom. THE NAME CARRIES A FACT THE OLD ONE HID: install_or_consume MAY RUN A WHOLE-TREE COMPILE. Under the executor's lazy-install arm the first consume installs the receipt, which is that compile; the predecessor was spelled consume_ and documented as reading the receipt only, so a .dag reader had no way to see the cost. DISSOLUTION: inherits compile_dag_diagnostic_census_row_note's PrimitiveDefinition identity-join trigger exactly -- do not mint a fresh trigger." + data observe_declared_import_closure_symbol_binding_row_note: String = "CLASS B binding-source observation for declared-import-closure-only compiles (#6985). Production classify_unlisted_import_binding_source already exists in cli_run.rs; this row exposes it through the same builtin-registry pattern as compile_dag_diagnostic_census: coproduct result (observed binding vs not-runnable), registered as type_variable_node(id: declared_import_closure_binding_result) rather than a kernel record. MEASUREMENT ONLY — callers judge ListedImport vs PoolCoincidence vs refusal. DISSOLUTION: inherits compile_dag_diagnostic_census_row_note's PrimitiveDefinition identity-join trigger exactly — one additive row is linear cost against that dissolution; do not mint a fresh trigger." // `emit_map_has` WAS A ROW OF THE REGISTRY BELOW AND HAD NO RUNTIME AT ANY TIER @@ -170,10 +172,10 @@ fn builtin_function_registry() -> Map { let m = map_insert(m, "class_b_import_closure_gate_not_affected_skip", bool_type) let m = map_insert(m, "witness_layer_roots_compile_clean_check", bool_type) let m = map_insert(m, "witness_layer_roots_compile_clean_emit_check", bool_type) - let m = map_insert(m, "consume_floor_compile_clean_gate_verdict", bool_type) - let m = map_insert(m, "consume_floor_compile_clean_gate_failure_detail", string_type) + let m = map_insert(m, "install_or_consume_floor_compile_clean_gate_receipt", type_variable_node(id: "gate_receipt_result")) let m = map_insert(m, "record_generated_artifact_drift_gate_failure_detail", unit_type) - let m = map_insert(m, "consume_generated_artifact_drift_gate_failure_detail", string_type) + let m = map_insert(m, "record_generated_artifact_drift_gate_clean", unit_type) + let m = map_insert(m, "consume_generated_artifact_drift_gate_receipt", type_variable_node(id: "gate_receipt_result")) let m = map_insert(m, "witness_compile_clean_cli_floor_verdicts_agree", bool_type) let m = map_insert(m, "test_migration_debt_module_names", list_of_type_variable(id: "test_migration_debt_module_name_elem")) let m = map_insert(m, "test_migration_legacy_behavior_ids", list_of_type_variable(id: "test_migration_legacy_behavior_id_elem")) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index dd66d6db985..49d3f2ce3ef 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -4377,7 +4377,7 @@ fn witness_layer_roots_compile_clean_sources_for_plan( } /// Test-only inject: append an unresolved-import module to the compile-clean closure so -/// `install_floor_compile_clean_receipt` + `consume_floor_compile_clean_gate_verdict` can be +/// `install_floor_compile_clean_receipt` + `install_or_consume_floor_compile_clean_gate_receipt` can be /// proven end-to-end (§5 discriminating RED) without mutating the workspace tree. fn append_test_floor_compile_clean_inject(sources: &mut Vec>) { if std::env::var("GUNBC_TEST_FLOOR_COMPILE_CLEAN_INJECT_UNRESOLVED") @@ -4401,6 +4401,25 @@ enum FloorCompileCleanReceipt { Compiled { ok: bool, failure_detail: String }, } +/// Host mirror of `gunbc.ci_gate` `GateReceipt` — what a CI gate answers to the substrate. +/// +/// The three arms are three OWNERS, not three severities. `Clean`/`Failed` are the gate +/// having reached its subject and decided (`GateObserved`); `NotApplicable` is the gate's +/// own scope disposition selecting nothing to check; `NotRun` is could-not-measure — the +/// instrument never arrived at its subject. The predecessors of this type collapsed all +/// four into a `bool` plus a second `String` builtin over the same global, so "the gate +/// did not run in this process" and "the compile found hard diagnostics" rendered +/// identically at the `.dag` call site (DESIGN §5, execution-provenance loss). `NotRun` +/// still stops the line — `gate_receipt_exit` refuses it — it simply stops it in its own +/// vocabulary instead of the subject's. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum GateReceipt { + Clean, + Failed { detail: String }, + NotApplicable { reason: String }, + NotRun { cause: String }, +} + static FLOOR_COMPILE_CLEAN_RECEIPT: Mutex> = Mutex::new(None); static GENERATED_ARTIFACT_DRIFT_GATE_FAILURE_DETAIL: Mutex> = Mutex::new(None); @@ -4411,15 +4430,46 @@ pub fn record_generated_artifact_drift_gate_failure_detail(detail: String) { } } -pub fn consume_generated_artifact_drift_gate_failure_detail() -> String { +#[cfg(test)] +fn reset_generated_artifact_drift_gate_detail_for_test() { + if let Ok(mut guard) = GENERATED_ARTIFACT_DRIFT_GATE_FAILURE_DETAIL.lock() { + *guard = None; + } +} + +/// The clean-side counterpart of the recorder above. It exists so that "ran, no drift" is +/// WRITTEN rather than inferred from the absence of a failure detail: without it the +/// global's `None` carries both "clean" and "never ran", which is the conflation this +/// retype exists to close, one layer down from the builtin. +pub fn record_generated_artifact_drift_gate_clean() { + if let Ok(mut guard) = GENERATED_ARTIFACT_DRIFT_GATE_FAILURE_DETAIL.lock() { + *guard = Some(String::new()); + } +} + +/// Gate consumer: the drift gate body records a located reason on the failing side and +/// records NOTHING on the clean side, so the global's `None` is genuinely two states — +/// "the body ran and found no drift" is indistinguishable from "the body never ran" at +/// this seam. The predecessor answered a `String` and papered the second one over with +/// the prose "gate body did not run in this process", which is a fabricated plausible +/// output standing exactly where the distinction was lost. It is not reconstructible from +/// the global alone, so the honest arm is `NotRun`: the gate body is the only thing that +/// can establish it ran, and it establishes that by recording — the clean side is recorded +/// by `record_generated_artifact_drift_gate_clean`. +pub fn consume_generated_artifact_drift_gate_receipt() -> GateReceipt { match GENERATED_ARTIFACT_DRIFT_GATE_FAILURE_DETAIL.lock() { - Ok(guard) => guard.clone().unwrap_or_else(|| { - "generated-artifact drift failure detail unavailable (gate body did not run in this process)" - .to_string() - }), - Err(e) => format!( - "generated-artifact drift failure detail refused: gate detail lock poisoned ({e})" - ), + Ok(guard) => match guard.as_ref() { + Some(detail) if detail.is_empty() => GateReceipt::Clean, + Some(detail) => GateReceipt::Failed { + detail: detail.clone(), + }, + None => GateReceipt::NotRun { + cause: "generated-artifact drift gate: no in-run observation recorded (the gate body did not run in this process)".to_string(), + }, + }, + Err(e) => GateReceipt::NotRun { + cause: format!("generated-artifact drift gate: detail lock poisoned ({e})"), + }, } } @@ -4754,16 +4804,31 @@ pub fn floor_compile_clean_receipt_installed() -> bool { .unwrap_or(false) } -/// Gate consumer: reads the receipt from `install_floor_compile_clean_receipt` only. -/// Refuses when no receipt exists — never runs a second compile. -pub fn consume_floor_compile_clean_gate_verdict() -> bool { +/// Gate consumer for the floor's ONE whole-tree `--target dag` compile. +/// +/// IT MAY RUN THAT COMPILE. When `claim_executor` armed `FLOOR_COMPILE_CLEAN_LAZY_INSTALL` +/// this call installs the receipt on first consume, which is a whole-tree compile — the name +/// says `install_or_consume` for that reason. The two functions this replaces were named +/// `consume_*` and documented as "reads the receipt only ... never runs a second compile", +/// which was false of the first of them and invisible at the `.dag` call site; a reader had +/// no way to see that a `Bool` read could cost a whole-tree compile. +/// +/// The other half of the replacement is the return type. `consume_floor_compile_clean_gate_verdict` +/// answered `bool`, folding FIVE states into `false` — lock poisoned, install failed, no +/// receipt at all, the receipt's typed `Refused`, and a real `Compiled { ok: false }` — and +/// folding `Skipped` into `true`; its located detail arrived through a SECOND builtin over +/// the same global, so recovering one fact took two correlated reads. Here the detail rides +/// the arm that produced it and cannot be read without it, and the three states with +/// different owners are three arms. +pub fn install_or_consume_floor_compile_clean_gate_receipt() -> GateReceipt { if FLOOR_COMPILE_CLEAN_LAZY_INSTALL.load(Ordering::SeqCst) && !floor_compile_clean_receipt_installed() { if let Err(msg) = install_floor_compile_clean_receipt() { if !floor_compile_clean_receipt_installed() { - eprintln!("compile-clean gate: refused — receipt install failed ({msg})"); - return false; + return GateReceipt::NotRun { + cause: format!("compile-clean gate: receipt install failed ({msg})"), + }; } // Serial `run_walk` today; if a future scheduler fans out batch-1, a concurrent // lazy install may win first — consume the installed receipt, do not refuse. @@ -4772,51 +4837,35 @@ pub fn consume_floor_compile_clean_gate_verdict() -> bool { let guard = match FLOOR_COMPILE_CLEAN_RECEIPT.lock() { Ok(g) => g, Err(e) => { - eprintln!("compile-clean gate: refused — receipt lock poisoned ({e})"); - return false; - } - }; - match guard.as_ref() { - None => { - eprintln!( - "compile-clean gate: refused — no in-run compile receipt (gate must consume the executor's one whole-tree --target dag compile)" - ); - false - } - Some(FloorCompileCleanReceipt::Skipped { reason }) => { - eprintln!("compile-clean gate: skipped ({reason})"); - true - } - Some(FloorCompileCleanReceipt::Refused { reason }) => { - eprintln!("compile-clean gate: refused ({reason})"); - false - } - Some(FloorCompileCleanReceipt::Compiled { ok, .. }) => *ok, - } -} - -/// Failure-receipt companion for the compile-clean gate: reads the in-run receipt only. -pub fn consume_floor_compile_clean_gate_failure_detail() -> String { - let guard = match FLOOR_COMPILE_CLEAN_RECEIPT.lock() { - Ok(g) => g, - Err(e) => { - return format!("compile-clean failure detail refused: receipt lock poisoned ({e})"); + return GateReceipt::NotRun { + cause: format!("compile-clean gate: receipt lock poisoned ({e})"), + }; } }; match guard.as_ref() { - None => "compile-clean failure detail unavailable: no in-run compile receipt".to_string(), - Some(FloorCompileCleanReceipt::Skipped { reason }) => { - format!("compile-clean gate skipped: {reason}") - } - Some(FloorCompileCleanReceipt::Refused { reason }) => reason.clone(), + None => GateReceipt::NotRun { + cause: "compile-clean gate: no in-run compile receipt (the gate consumes the executor's one whole-tree --target dag compile, and it was never installed in this process)".to_string(), + }, + Some(FloorCompileCleanReceipt::Skipped { reason }) => GateReceipt::NotApplicable { + reason: reason.clone(), + }, + Some(FloorCompileCleanReceipt::Refused { reason }) => GateReceipt::NotRun { + cause: reason.clone(), + }, Some(FloorCompileCleanReceipt::Compiled { ok: true, failure_detail: _, - }) => String::new(), + }) => GateReceipt::Clean, Some(FloorCompileCleanReceipt::Compiled { ok: false, failure_detail, - }) => failure_detail.clone(), + }) => GateReceipt::Failed { + detail: if failure_detail.is_empty() { + "dag compile-clean gate failed: compile receipt records failure with no located diagnostic".to_string() + } else { + failure_detail.clone() + }, + }, } } @@ -5265,7 +5314,7 @@ pub fn witness_layer_roots_compile_clean_check() -> bool { /// Emit leg: `--target dag` compile over witness layer roots without shell or disk write. /// Direct-run oracle for non-floor contexts (cargo tests, enrolled witnesses). The CI -/// floor gate consumes `consume_floor_compile_clean_gate_verdict` instead (Lever A). +/// floor gate consumes `install_or_consume_floor_compile_clean_gate_receipt` instead (Lever A). pub fn witness_layer_roots_compile_clean_emit_check() -> bool { match witness_layer_roots_compile_clean_sources_for_plan(&compile_clean_scope_plan_for_ci()) { Ok(None) => true, @@ -37343,9 +37392,15 @@ mod witness_layer_roots_compile_clean_tests { fn floor_compile_clean_gate_refuses_without_receipt() { with_env_test_lock(|| { reset_floor_compile_clean_receipt_for_test(); + // Sharper than the `!verdict` this replaces: it pins the arm, so a future + // change that makes the gate refuse for a DIFFERENT reason (a real failed + // compile, say) fails here instead of passing as "still false". assert!( - !consume_floor_compile_clean_gate_verdict(), - "gate must refuse when no in-run compile receipt exists" + matches!( + install_or_consume_floor_compile_clean_gate_receipt(), + GateReceipt::NotRun { .. } + ), + "gate must answer NotRun when no in-run compile receipt exists" ); assert!(!floor_compile_clean_receipt_installed()); }); @@ -37360,15 +37415,105 @@ mod witness_layer_roots_compile_clean_tests { ok: false, failure_detail: "compile-clean: synthetic hard diagnostic".to_string(), }); + // The discriminating half against the test above: a recorded compile failure + // must reach `Failed` carrying its located detail, NOT `NotRun`. Under the + // predecessor `bool` these two tests asserted the same value. + assert_eq!( + install_or_consume_floor_compile_clean_gate_receipt(), + GateReceipt::Failed { + detail: "compile-clean: synthetic hard diagnostic".to_string() + }, + "gate must report the receipt's located failure detail, not a bare refusal" + ); + }); + } + + /// The distinction the predecessor `bool` could not express, asserted in both + /// directions in one test: a scope disposition that selected nothing (`Skipped`) and a + /// clean compile both used to answer `true`, so no test could tell them apart. They are + /// different owners — the first is the disposition's answer, the second is the tree's — + /// and only the second is evidence about the tree. + #[test] + fn floor_compile_clean_gate_separates_not_applicable_from_clean() { + with_env_test_lock(|| { + reset_floor_compile_clean_receipt_for_test(); + install_floor_compile_clean_receipt_fixture(FloorCompileCleanReceipt::Skipped { + reason: "compile-clean scope: no shard intersection".to_string(), + }); + assert_eq!( + install_or_consume_floor_compile_clean_gate_receipt(), + GateReceipt::NotApplicable { + reason: "compile-clean scope: no shard intersection".to_string() + }, + "a scope disposition selecting nothing is NotApplicable, never Clean" + ); + + reset_floor_compile_clean_receipt_for_test(); + install_floor_compile_clean_receipt_fixture(FloorCompileCleanReceipt::Compiled { + ok: true, + failure_detail: String::new(), + }); + assert_eq!( + install_or_consume_floor_compile_clean_gate_receipt(), + GateReceipt::Clean, + "a compiled-ok receipt is Clean" + ); + + // The receipt's own typed Refused arm is ignorance, not a verdict on the tree. + reset_floor_compile_clean_receipt_for_test(); + install_floor_compile_clean_receipt_fixture(FloorCompileCleanReceipt::Refused { + reason: "compile-clean: index roots never armed".to_string(), + }); + assert!( + matches!( + install_or_consume_floor_compile_clean_gate_receipt(), + GateReceipt::NotRun { .. } + ), + "a Refused receipt is NotRun, never Failed — nothing was measured about the tree" + ); + reset_floor_compile_clean_receipt_for_test(); + }); + } + + /// Same split on the generated-artifact drift gate, whose predecessor answered a + /// `String` and FABRICATED the prose "gate body did not run in this process" for the + /// state it had lost. Unrecorded is now `NotRun`; the clean side is recorded, so it is + /// no longer inferred from the absence of a failure detail. + #[test] + fn generated_artifact_drift_gate_separates_unrecorded_from_clean() { + with_env_test_lock(|| { + reset_generated_artifact_drift_gate_detail_for_test(); assert!( - !consume_floor_compile_clean_gate_verdict(), - "gate must refuse when the installed receipt records compile failure" + matches!( + consume_generated_artifact_drift_gate_receipt(), + GateReceipt::NotRun { .. } + ), + "no recorded observation must read as NotRun, never as clean" + ); + + record_generated_artifact_drift_gate_clean(); + assert_eq!( + consume_generated_artifact_drift_gate_receipt(), + GateReceipt::Clean, + "a recorded clean observation is Clean" + ); + + record_generated_artifact_drift_gate_failure_detail( + "generated-artifact drift: docs/plans/x.md".to_string(), + ); + assert_eq!( + consume_generated_artifact_drift_gate_receipt(), + GateReceipt::Failed { + detail: "generated-artifact drift: docs/plans/x.md".to_string() + }, + "a recorded failure carries its located path" ); + reset_generated_artifact_drift_gate_detail_for_test(); }); } /// §5 discriminating RED (end-to-end): real whole-tree compile with an injected broken module - /// must refuse through install_floor_compile_clean_receipt → consume_floor_compile_clean_gate_verdict. + /// must refuse through install_floor_compile_clean_receipt → install_or_consume_floor_compile_clean_gate_receipt. /// Ignored in CI: ~minutes cold whole-tree compile; recorded execution receipt in PR #6361 body. #[test] #[ignore = "manual ~minutes whole-tree compile; recorded execution receipt in PR #6361 body (clever-koi demand 1)"] @@ -37387,8 +37532,11 @@ mod witness_layer_roots_compile_clean_tests { install_floor_compile_clean_receipt() .expect("real whole-tree compile with injected unresolved import"); assert!( - !consume_floor_compile_clean_gate_verdict(), - "gate must refuse when the one real compile hits hard errors" + matches!( + install_or_consume_floor_compile_clean_gate_receipt(), + GateReceipt::Failed { .. } + ), + "gate must report Failed when the one real compile hits hard errors" ); }); }); @@ -41208,6 +41356,12 @@ mod peel_alias_fixpoint_termination { bindings: crate::v1_rt::rc_empty_map(), str_bindings: crate::v1_rt::rc_empty_map(), ancestry_str_bindings: crate::v1_rt::rc_empty_map(), + // Pre-existing on main and unrelated to this change: the field landed on the + // GENERATED `TypeEnv` and this hand-written `#[cfg(test)]` constructor was never + // updated, so the whole lib-test target failed to compile. No gate could see it + // — CI builds the binary, and the Rust suite left CI on 2026-07-11 — which is + // why it stood. Repaired here because this PR's evidence cannot execute otherwise. + authored_import_names: crate::v1_rt::rc_empty_map(), parents: std::rc::Rc::new(im::vector![]), recursive_types: std::rc::Rc::new(im::vector![]), recursive_type_set: crate::v1_rt::rc_empty_map(), diff --git a/src/v1/stage0/src/v1_compiler_infer_method.rs b/src/v1/stage0/src/v1_compiler_infer_method.rs index 70b29212781..83f51a50ce6 100644 --- a/src/v1/stage0/src/v1_compiler_infer_method.rs +++ b/src/v1/stage0/src/v1_compiler_infer_method.rs @@ -8,15 +8,16 @@ pub use crate::v1_compiler_infer_types::{ use crate::v1_rt; use crate::v1_rt::{VecCompat, VecJoin}; use crate::v1_std_core::Cardinality::Required; -pub use crate::v1_std_core::CompilerDiagnostic; use crate::v1_std_core::CompilerDiagnostic::*; use crate::v1_std_core::Connective::NoConnective; use crate::v1_std_core::ExprData::NoExprData; use crate::v1_std_core::InferredNode::{Resolved, TypeVariable}; +use crate::v1_std_core::UnaryOpKind::*; pub use crate::v1_std_core::{ bool_type, hash_type, int_type, no_span, string_type, unit_type, with_optional_cardinality, }; pub use crate::v1_std_core::{Cardinality, Connective, ErrorNode, ExprData, InferredNode, Node}; +pub use crate::v1_std_core::{CompilerDiagnostic, UnaryOpKind}; use crate::NonEmptyBTreeSet; use crate::NonEmptyVec; use im::{vector as vec, HashMap, OrdSet as BTreeSet, Vector as Vec}; @@ -127,6 +128,15 @@ pub fn compile_dag_diagnostic_census_row_note() -> String { CACHED.with(|c: &String| c.clone()) } +pub fn gate_receipt_rows_note() -> String { + thread_local! { + static CACHED: String = { + "THE TWO CI-GATE ROWS ANSWER A COPRODUCT, and the reason is the same one compile_dag_diagnostic_census_row_note gives one row up. Their predecessors were three rows -- consume_floor_compile_clean_gate_verdict as bool_type, consume_floor_compile_clean_gate_failure_detail as string_type, consume_generated_artifact_drift_gate_failure_detail as string_type -- and the Bool folded FIVE host states into false (lock poisoned, install failed, no in-run receipt, the receipt's typed Refused arm, and a real failed compile) while folding the scope disposition's Skipped into true. The String companions were second builtins over the SAME process global, so a caller reconstructed one fact from two correlated reads, and the generated-artifact one fabricated prose for the state the Bool had already erased. gunbc.ci_gate GateReceipt is the single carrier: GateObserved holds the verdict WITH its located detail, GateNotApplicable is the scope disposition answering, GateNotRun is could-not-measure. Registered as a type variable rather than a kernel record for the reason its two siblings are -- the result is a coproduct, so make_kernel_record_type is the wrong idiom. THE NAME CARRIES A FACT THE OLD ONE HID: install_or_consume MAY RUN A WHOLE-TREE COMPILE. Under the executor's lazy-install arm the first consume installs the receipt, which is that compile; the predecessor was spelled consume_ and documented as reading the receipt only, so a .dag reader had no way to see the cost. DISSOLUTION: inherits compile_dag_diagnostic_census_row_note's PrimitiveDefinition identity-join trigger exactly -- do not mint a fresh trigger.".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + pub fn observe_declared_import_closure_symbol_binding_row_note() -> String { thread_local! { static CACHED: String = { @@ -387,23 +397,23 @@ pub fn builtin_function_registry() -> Rc>> { ); let m = v1_rt::rc_map_insert( m.clone(), - "consume_floor_compile_clean_gate_verdict".to_string(), - bool_type(), + "install_or_consume_floor_compile_clean_gate_receipt".to_string(), + type_variable_node("gate_receipt_result".to_string()), ); let m = v1_rt::rc_map_insert( m.clone(), - "consume_floor_compile_clean_gate_failure_detail".to_string(), - string_type(), + "record_generated_artifact_drift_gate_failure_detail".to_string(), + unit_type(), ); let m = v1_rt::rc_map_insert( m.clone(), - "record_generated_artifact_drift_gate_failure_detail".to_string(), + "record_generated_artifact_drift_gate_clean".to_string(), unit_type(), ); let m = v1_rt::rc_map_insert( m.clone(), - "consume_generated_artifact_drift_gate_failure_detail".to_string(), - string_type(), + "consume_generated_artifact_drift_gate_receipt".to_string(), + type_variable_node("gate_receipt_result".to_string()), ); let m = v1_rt::rc_map_insert( m.clone(), diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 4c02be96084..ce1055ff099 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -8801,6 +8801,41 @@ fn compile_diagnostic_census_value( } } +/// Projects a host gate receipt into the `gunbc.ci_gate` `GateReceipt` coproduct. +/// The arms stay distinct all the way to the substrate for the same reason +/// `compile_diagnostic_census_value`'s do: `GateNotRun` must never arrive as a clean +/// verdict, because could-not-measure and the subject passing are different facts with +/// different owners, and a `Bool` at this seam made them the same value. +fn gate_receipt_value(receipt: crate::cli_run::GateReceipt, ctx: &InterpContext) -> Value { + let observed = |outcome: Value| Value::Variant { + type_name: ctx.sym("GateReceipt"), + variant_name: ctx.sym("GateObserved"), + fields: Rc::new(sorted_fields(vec![(ctx.sym("outcome"), outcome)])), + }; + match receipt { + crate::cli_run::GateReceipt::Clean => observed(Value::Variant { + type_name: ctx.sym("GateOutcome"), + variant_name: ctx.sym("GateClean"), + fields: Rc::new(vec![]), + }), + crate::cli_run::GateReceipt::Failed { detail } => observed(Value::Variant { + type_name: ctx.sym("GateOutcome"), + variant_name: ctx.sym("GateFailed"), + fields: Rc::new(sorted_fields(vec![(ctx.sym("detail"), str_value(detail))])), + }), + crate::cli_run::GateReceipt::NotApplicable { reason } => Value::Variant { + type_name: ctx.sym("GateReceipt"), + variant_name: ctx.sym("GateNotApplicable"), + fields: Rc::new(sorted_fields(vec![(ctx.sym("reason"), str_value(reason))])), + }, + crate::cli_run::GateReceipt::NotRun { cause } => Value::Variant { + type_name: ctx.sym("GateReceipt"), + variant_name: ctx.sym("GateNotRun"), + fields: Rc::new(sorted_fields(vec![(ctx.sym("cause"), str_value(cause))])), + }, + } +} + fn unlisted_import_binding_source_value( source: crate::cli_run::UnlistedImportBindingSource, ctx: &InterpContext, @@ -13861,12 +13896,9 @@ macro_rules! v1_builtin_arms { arm "free_call.witness_layer_roots_compile_clean_emit_check" { "witness_layer_roots_compile_clean_emit_check" } => Ok(Some(Value::Bool( crate::cli_run::witness_layer_roots_compile_clean_emit_check(), ))), - arm "free_call.consume_floor_compile_clean_gate_verdict" { "consume_floor_compile_clean_gate_verdict" } => Ok(Some(Value::Bool( - crate::cli_run::consume_floor_compile_clean_gate_verdict(), - ))), - - arm "free_call.consume_floor_compile_clean_gate_failure_detail" { "consume_floor_compile_clean_gate_failure_detail" } => Ok(Some(str_value( - crate::cli_run::consume_floor_compile_clean_gate_failure_detail(), + arm "free_call.install_or_consume_floor_compile_clean_gate_receipt" { "install_or_consume_floor_compile_clean_gate_receipt" } => Ok(Some(gate_receipt_value( + crate::cli_run::install_or_consume_floor_compile_clean_gate_receipt(), + $ctx, ))), arm "free_call.record_generated_artifact_drift_gate_failure_detail" { "record_generated_artifact_drift_gate_failure_detail" } => { @@ -13876,8 +13908,14 @@ macro_rules! v1_builtin_arms { Ok(Some(Value::Unit)) }, - arm "free_call.consume_generated_artifact_drift_gate_failure_detail" { "consume_generated_artifact_drift_gate_failure_detail" } => Ok(Some(str_value( - crate::cli_run::consume_generated_artifact_drift_gate_failure_detail(), + arm "free_call.record_generated_artifact_drift_gate_clean" { "record_generated_artifact_drift_gate_clean" } => { + crate::cli_run::record_generated_artifact_drift_gate_clean(); + Ok(Some(Value::Unit)) + }, + + arm "free_call.consume_generated_artifact_drift_gate_receipt" { "consume_generated_artifact_drift_gate_receipt" } => Ok(Some(gate_receipt_value( + crate::cli_run::consume_generated_artifact_drift_gate_receipt(), + $ctx, ))), arm "free_call.witness_compile_clean_cli_floor_verdicts_agree" { "witness_compile_clean_cli_floor_verdicts_agree" } => Ok(Some(Value::Bool( diff --git a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs index 28ee9cb01ca..0c8badc61ce 100644 --- a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs +++ b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs @@ -97,10 +97,10 @@ pub enum EvalBuiltinArm { FreeCallClassBImportClosureGateNotAffectedSkip, FreeCallWitnessLayerRootsCompileCleanCheck, FreeCallWitnessLayerRootsCompileCleanEmitCheck, - FreeCallConsumeFloorCompileCleanGateVerdict, - FreeCallConsumeFloorCompileCleanGateFailureDetail, + FreeCallInstallOrConsumeFloorCompileCleanGateReceipt, FreeCallRecordGeneratedArtifactDriftGateFailureDetail, - FreeCallConsumeGeneratedArtifactDriftGateFailureDetail, + FreeCallRecordGeneratedArtifactDriftGateClean, + FreeCallConsumeGeneratedArtifactDriftGateReceipt, FreeCallWitnessCompileCleanCliFloorVerdictsAgree, FreeCallTestMigrationDebtModuleNames, FreeCallTestMigrationLegacyBehaviorIds, @@ -227,10 +227,10 @@ pub fn lookup_eval_builtin_inner(spelling: &str) -> Option { "class_b_import_closure_gate_not_affected_skip" => Some(EvalBuiltinArm::FreeCallClassBImportClosureGateNotAffectedSkip), "witness_layer_roots_compile_clean_check" => Some(EvalBuiltinArm::FreeCallWitnessLayerRootsCompileCleanCheck), "witness_layer_roots_compile_clean_emit_check" => Some(EvalBuiltinArm::FreeCallWitnessLayerRootsCompileCleanEmitCheck), - "consume_floor_compile_clean_gate_verdict" => Some(EvalBuiltinArm::FreeCallConsumeFloorCompileCleanGateVerdict), - "consume_floor_compile_clean_gate_failure_detail" => Some(EvalBuiltinArm::FreeCallConsumeFloorCompileCleanGateFailureDetail), + "install_or_consume_floor_compile_clean_gate_receipt" => Some(EvalBuiltinArm::FreeCallInstallOrConsumeFloorCompileCleanGateReceipt), "record_generated_artifact_drift_gate_failure_detail" => Some(EvalBuiltinArm::FreeCallRecordGeneratedArtifactDriftGateFailureDetail), - "consume_generated_artifact_drift_gate_failure_detail" => Some(EvalBuiltinArm::FreeCallConsumeGeneratedArtifactDriftGateFailureDetail), + "record_generated_artifact_drift_gate_clean" => Some(EvalBuiltinArm::FreeCallRecordGeneratedArtifactDriftGateClean), + "consume_generated_artifact_drift_gate_receipt" => Some(EvalBuiltinArm::FreeCallConsumeGeneratedArtifactDriftGateReceipt), "witness_compile_clean_cli_floor_verdicts_agree" => Some(EvalBuiltinArm::FreeCallWitnessCompileCleanCliFloorVerdictsAgree), "test_migration_debt_module_names" => Some(EvalBuiltinArm::FreeCallTestMigrationDebtModuleNames), "test_migration_legacy_behavior_ids" => Some(EvalBuiltinArm::FreeCallTestMigrationLegacyBehaviorIds), @@ -355,10 +355,10 @@ macro_rules! eval_builtin_inner_arm { ("free_call.class_b_import_closure_gate_not_affected_skip") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallClassBImportClosureGateNotAffectedSkip }; ("free_call.witness_layer_roots_compile_clean_check") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallWitnessLayerRootsCompileCleanCheck }; ("free_call.witness_layer_roots_compile_clean_emit_check") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallWitnessLayerRootsCompileCleanEmitCheck }; - ("free_call.consume_floor_compile_clean_gate_verdict") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallConsumeFloorCompileCleanGateVerdict }; - ("free_call.consume_floor_compile_clean_gate_failure_detail") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallConsumeFloorCompileCleanGateFailureDetail }; + ("free_call.install_or_consume_floor_compile_clean_gate_receipt") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallInstallOrConsumeFloorCompileCleanGateReceipt }; ("free_call.record_generated_artifact_drift_gate_failure_detail") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallRecordGeneratedArtifactDriftGateFailureDetail }; - ("free_call.consume_generated_artifact_drift_gate_failure_detail") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallConsumeGeneratedArtifactDriftGateFailureDetail }; + ("free_call.record_generated_artifact_drift_gate_clean") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallRecordGeneratedArtifactDriftGateClean }; + ("free_call.consume_generated_artifact_drift_gate_receipt") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallConsumeGeneratedArtifactDriftGateReceipt }; ("free_call.witness_compile_clean_cli_floor_verdicts_agree") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallWitnessCompileCleanCliFloorVerdictsAgree }; ("free_call.test_migration_debt_module_names") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallTestMigrationDebtModuleNames }; ("free_call.test_migration_legacy_behavior_ids") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallTestMigrationLegacyBehaviorIds };