diff --git a/dag/extdeps/realization/eval_memo.dag b/dag/extdeps/realization/eval_memo.dag deleted file mode 100644 index d4c151ae335..00000000000 --- a/dag/extdeps/realization/eval_memo.dag +++ /dev/null @@ -1,127 +0,0 @@ -module extdeps.realization.eval_memo - -import extdeps.external_authority { ExternalAuthority } -import extdeps.uri { Uri, Https } -import v2.std.optional { Absent } - -import extdeps.cache.types { CacheInterfaceCatalogFacts, ContentAddressed, CatalogCasContentEncoding } -import std.cache_identity { CacheInterfaceId } -import std.cache_interface { - ContentAddressLookup, - OverwriteAllowed, - MissThenCreate, - StructuredArtifact, - InProcess, - PerFile, - None, - InProcessNs, - Strong, - OperatorObserved, - ManualPurge, - Repo, - CapacityBounded, - EntryCountCapacity, - ExactLimit, - RefuseNewStore, - ReleasedAtProviderScopeExit, -} -import std.disposition { Disposition, Scaffold, RealizationDispatch } -import std.decl_ref { DeclarationRef, WholeDeclaration } - -// The eval-frame memo: the ladder's single-site discharge provider, realized in the seed -// interpreter (v1_interpreter.rs eval_pure_named_call / EvalCallMemo). Serves every repeated pure -// named-fn demand from its first evaluation within one InterpContext. SOUNDNESS IS CONSTRUCTION, -// NOT PROBABILITY: buckets by the demand-ledger key (fn identity x argument content identity) but -// serves ONLY after the stored call's argument names AND values verify equal (Value equality, the -// one equality authority) — a hash collision degrades to recompute, never to a wrong value. A memo -// hit still records the DEMAND in the ledger: plurality is the fact the receipt counts; the -// provider changes its cost, never its count (so the multi-site rewire worklist survives discharge -// intact). Release is ReleasedAtProviderScopeExit and the provider scope is the WITNESS FRAME -// (corrected 2026-07-10, same-day regression owned at confession grade: the first landing evicted -// at ctx lifetime while batch surfaces share one ctx across an entry's witnesses, so retained -// argument+result values were byte-unbounded by construction — measured single-witness plateau -// ~3.4GiB vs six-witness climb past ~20GiB to SIGKILL on a quiet host, eager-ram-612's A/B; batch -// surfaces now call eval_call_memo_frame_exit after each claim fn, counters cumulative). -// Cross-witness serving is an outer-frame promotion that must arrive as a conscious provider row -// with byte-bounded admission, never a default; the count cap (1M entries) is admission at the -// wrong unit and is slated to become a DECLARED byte cap consuming the single value-size authority -// (one fn beside Value; merry-owl-649's space-lens predictor binds to the same authority). -// Admission stops at the cap with the refusal COUNTED (memo_overflow), never silent. COUNTER -// INVARIANT (review-pinned 2026-07-10): a miss means the call was NOT served, so it evaluated — a -// cap-refused store attempt is still a miss; overflow is a subset of misses, and hits + misses -// equals the keyed Ok-resulting calls through the memo path, including under overflow (misses is -// NOT entries-stored). Default ON in every binary; GUNBC_EVAL_MEMO=0 is a diagnostic realization -// switch (recompute instead of serve, semantics identical) and the receipt discloses -// memo_hits/memo_misses so a disabled or ineffective memo is visible, never assumed working. The -// switch is PER-CTX (read at InterpContext construction; set_eval_call_memo_enabled), because a -// covering provider at an outer frame legitimately quiets an inner provider's hit counters: an -// inner door's by-execution receipt suite (the parse-table MemoTier amortization tests) pins this -// provider off on its own ctxs so pass-2 demands re-execute and the door's counters keep -// discriminating — provider-attribution receipts select their realization explicitly, never racing -// a process latch. MEASURED (2026-07-10, artifact-regen workload): single-site duplicated keys 7285 -// -> 505 (93.1 percent discharged), wasted_ms 586 -> 57, misses == distinct keys (every distinct -// computation evaluated exactly once), regenerated artifacts byte-identical with the memo on and -// off — the purity oracle by execution. - -data eval_memo_seed_handler_dissolution_trigger: Disposition = Scaffold { - dissolves_to: RealizationDispatch, - bind: DeclarationRef { - module_path: "std.materialization_ladder", - decl_name: "materialization_ladder", - field: WholeDeclaration - } -} - -data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { - uri: Uri { - scheme: Https - locator: "github.com/gunb-ai/gunbc/tree/main/dag/extdeps/realization" - } -} - -data eval_memo_id: CacheInterfaceId = "eval_call_memo_cache" - -data eval_memo_facts: CacheInterfaceCatalogFacts = { - identity: eval_memo_id - backing_surface: "gunbc-eval-call-in-process" - transport_encoding: CatalogCasContentEncoding - key_derivation: { - - key_inputs: ContentAddressed - overwritable: true - prefix_fallback_allowed: false - content_verified_on_read: true - visibility_scope: Repo - invalidation_triggers: [ManualPurge] - } - io: { - lookup_semantics: ContentAddressLookup - write_semantics: OverwriteAllowed - miss_semantics: MissThenCreate - } - placement: { - value_shape: StructuredArtifact - locality: InProcess - retention: { release_policy: ReleasedAtProviderScopeExit, capacity: CapacityBounded { limit: EntryCountCapacity { limit: ExactLimit { value: 1000000 } }, at_capacity: RefuseNewStore } } - atomicity: PerFile - auth: None - read_latency: InProcessNs - consistency: Strong - } - evidence: [ - { - field: "locality" - evidence: OperatorObserved { - note: "scoped to InterpContext for the resolve-side share, but EVICTED at the witness frame (eval_call_memo_frame_exit after each claim fn on batch surfaces — ctx-lifetime retention across witnesses was the 2026-07-10 20GiB-class regression); entry-cap refusals counted as memo_overflow in the floor materialization receipt" - observed_at: Absent - } - }, - { - field: "key_derivation" - evidence: OperatorObserved { - note: "EvalRecomputeKey = fn identity x per-argument identity (scalars exact; composites recursive content hash, allocation-memoized with Weak liveness); content_verified_on_read is TRUE structurally: a hit serves only after stored argument names and values verify equal via Value equality, so a collision recomputes rather than lies" - observed_at: Absent - } - }, - ] -} diff --git a/dag/gunbc/ci/ci_materialization.dag b/dag/gunbc/ci/ci_materialization.dag index 0345100ca61..e91263a9f83 100644 --- a/dag/gunbc/ci/ci_materialization.dag +++ b/dag/gunbc/ci/ci_materialization.dag @@ -505,7 +505,7 @@ data ci_sccache_provider_shell_injection_dissolution_trigger: Disposition = Scaf } } -data ci_floor_materialization_receipt_note: String = "Increment 1 of INFERRED materialization (operator ruling 2026-07-10: code is forcefully framed under materialization — running IS enrolling; and: plural pure demand means a provider or a hard error, no wall-clock term in any verdict, exemptions only as declared human-signed rows). The interpreter ledgers every keyed pure call (fn identity x argument content identity); every InterpContext absorbs its ledger totals into a process-wide accumulator on Drop — BY CONSTRUCTION, so no eval path (threaded, memoized, or future) can escape the receipt by forgetting a harvest call. claim_executor writes target/floor-materialization-receipt.txt at walk end. WHAT GATES NOW: the receipt must exist and parse, and keyed_calls must be nonzero (a floor that evaluated nothing is a lie — an explicit GUNBC_RECOMPUTE_TRACE=0 zeroes the receipt and reds this gate, so disabling is loud, never an escape hatch). PIN RETRACTION (2026-07-10 — the resolve gate's declare-measure-refuse-retract loop applied to this gate's own promise): the first counted CI receipt landed (run 29123412337: keyed=2313593 unkeyed=2516564 duplicated=50766) and the promised exact count pins were REFUSED twice over. By measurement: keyed/distinct/duplicated sum PER-CTX numbers and witness-to-ctx grouping is a thread-pool accident — back-to-back identical full floors differed by a few counts (duplicated 50713 vs 50711 locally; CI +54 vs local) — an exact pin would flap on schedule, and a flapping wall is a fail-open generator. By architecture: the affected-set enrollment flip (ci_spec_discovery_flip_note, merged 2026-07-10) makes this job's evaluated witness set diff-dependent BY DESIGN, so ANY count pin at this job's grain reds on nearly every PR for the wrong reason. What survives is what is diff-independent: unkeyed_calls is corpus-deterministic (measured identical five times across schedules, machines, debug/release, truncated and full floors — 2516564) but diff-scoped under the flip, so its terminal form is the RELATION unkeyed == 0, not a count. Count-shaped pins at full-corpus grain belong to a full-corpus surface, and AS OF 2026-08-15 NO SUCH SURFACE EXISTS: this sentence named the nightly affected-set falsifier as the place they would go, falsifier.yml was deleted at 611fd02770 (#8283), and the repository carries three workflows none of which runs the corpus cold. The deferral was therefore made to a consumer that no longer exists, which is a different standing from a deferral still waiting on its owner -- it is censused as PremiseInvalidated in gunbc.deleted_cadence_reference_census with its restoration trigger, rather than left reading as a plan; duplicated accounting pins only when the frame grain is structural (deterministic witness-to-ctx assignment, or content-keyed cross-ctx identity — the outer-frame store direction). Until a wall lands, this gate is a DISCLOSURE gate: receipt existence, parseability of every field, keyed nonzero. unkeyed_calls is known NONZERO on the floor (measured 2026-07-10: the corpus is fold-heavy and every fold-family call carries a predicate closure, and a closure argument has no computed identity — the ONE disclosed unkeyed class, per the interpreter ledger's own disclosure); the wall's dissolve-on is captured-env content identity for closure arguments, at which point unkeyed == 0 lands as the identity-computability wall (underspecified identity = error, operator ruling) — a relation, diff-independent under affected-set enrollment. duplicated_keys burns down via the eval-frame provider (single_site class, discharged wholesale) and the multi_site rewire worklist, then flips to hard error per frame-class at zero. PROVIDER LANDED (2026-07-10, extdeps.realization.eval_memo): the eval-frame memo serves repeated pure demands from the first evaluation — verified-hit serve (argument names AND values must equal; collision recomputes, never lies), demands still counted on hits so this receipt keeps observing plurality, hits/misses/overflow disclosed in the receipt. Measured on the artifact-regen workload: single-site duplicated keys 7285 -> 505 (93.1 percent), wasted_ms 586 -> 57, regenerated artifacts byte-identical memo-on vs memo-off. wasted_ms lines are observational timing and MUST never gate. Consciously NO new witness entry file: this gate is a derived ci.yml step, so ci_floor_declared_resolve_count stays untouched by this increment." +data ci_floor_materialization_receipt_note: String = "Increment 1 of INFERRED materialization (operator ruling 2026-07-10: code is forcefully framed under materialization — running IS enrolling; and: plural pure demand means a provider or a hard error, no wall-clock term in any verdict, exemptions only as declared human-signed rows). The interpreter ledgers every keyed pure call (fn identity x argument content identity); every InterpContext absorbs its ledger totals into a process-wide accumulator on Drop — BY CONSTRUCTION, so no eval path (threaded, memoized, or future) can escape the receipt by forgetting a harvest call. claim_executor writes target/floor-materialization-receipt.txt at walk end. WHAT GATES NOW: the receipt must exist and parse, and keyed_calls must be nonzero (a floor that evaluated nothing is a lie — an explicit GUNBC_RECOMPUTE_TRACE=0 zeroes the receipt and reds this gate, so disabling is loud, never an escape hatch). PIN RETRACTION (2026-07-10 — the resolve gate's declare-measure-refuse-retract loop applied to this gate's own promise): the first counted CI receipt landed (run 29123412337: keyed=2313593 unkeyed=2516564 duplicated=50766) and the promised exact count pins were REFUSED twice over. By measurement: keyed/distinct/duplicated sum PER-CTX numbers and witness-to-ctx grouping is a thread-pool accident — back-to-back identical full floors differed by a few counts (duplicated 50713 vs 50711 locally; CI +54 vs local) — an exact pin would flap on schedule, and a flapping wall is a fail-open generator. By architecture: the affected-set enrollment flip (ci_spec_discovery_flip_note, merged 2026-07-10) makes this job's evaluated witness set diff-dependent BY DESIGN, so ANY count pin at this job's grain reds on nearly every PR for the wrong reason. What survives is what is diff-independent: unkeyed_calls is corpus-deterministic (measured identical five times across schedules, machines, debug/release, truncated and full floors — 2516564) but diff-scoped under the flip, so its terminal form is the RELATION unkeyed == 0, not a count. Count-shaped pins at full-corpus grain belong to a full-corpus surface, and AS OF 2026-08-15 NO SUCH SURFACE EXISTS: this sentence named the nightly affected-set falsifier as the place they would go, falsifier.yml was deleted at 611fd02770 (#8283), and the repository carries three workflows none of which runs the corpus cold. The deferral was therefore made to a consumer that no longer exists, which is a different standing from a deferral still waiting on its owner -- it is censused as PremiseInvalidated in gunbc.deleted_cadence_reference_census with its restoration trigger, rather than left reading as a plan; duplicated accounting pins only when the frame grain is structural (deterministic witness-to-ctx assignment, or content-keyed cross-ctx identity — the outer-frame store direction). Until a wall lands, this gate is a DISCLOSURE gate: receipt existence, parseability of every field, keyed nonzero. unkeyed_calls is known NONZERO on the floor (measured 2026-07-10: the corpus is fold-heavy and every fold-family call carries a predicate closure, and a closure argument has no computed identity — the ONE disclosed unkeyed class, per the interpreter ledger's own disclosure); the wall's dissolve-on is captured-env content identity for closure arguments, at which point unkeyed == 0 lands as the identity-computability wall (underspecified identity = error, operator ruling) — a relation, diff-independent under affected-set enrollment. duplicated_keys burns down via the eval-frame provider (single_site class, discharged wholesale) and the multi_site rewire worklist, then flips to hard error per frame-class at zero. PROVIDER LANDED (2026-07-10, extdeps.realization.eval_memo): the eval-frame memo serves repeated pure demands from the first evaluation — verified-hit serve (argument names AND values must equal; collision recomputes, never lies), demands still counted on hits so this receipt keeps observing plurality, hits/misses/overflow disclosed in the receipt. Measured on the artifact-regen workload: single-site duplicated keys 7285 -> 505 (93.1 percent), wasted_ms 586 -> 57, regenerated artifacts byte-identical memo-on vs memo-off. wasted_ms lines are observational timing and MUST never gate. Consciously NO new witness entry file: this gate is a derived ci.yml step, so ci_floor_declared_resolve_count stays untouched by this increment. PROVIDER RETIRED (2026-09-19, gunbc.recurring_failure_mode.memo_key_rehashes_a_growing_persistent_value second instance): the eval-frame memo derived an identity for every pure call before any admission was asked, and std.materialization_ladder never discharges a demand into a provider scoped to one shared-state frame (rule 5: single undeclared demand recomputes; rule 1: a within-frame repeat is Share, never Memoize), so its admitted population was empty and the per-call key was pure cost -- quadratic on a fold threading a document through recursion. The memo, GUNBC_EVAL_MEMO and the memo_hits/memo_misses/memo_overflow receipt fields are deleted; the ledger still counts every demand under GUNBC_RECOMPUTE_TRACE=1 and now also discloses argument_identities_derived, its own keying work. The duplicated_keys burn-down named above proceeds by the multi_site rewire worklist and by declared providers (the roster-admitted cross-claim tier), which is what the ladder prescribed for it all along. ALSO RECORDED HONESTLY: no consumer of take_process_eval_recompute_totals exists in the tree today, so the receipt file this note names is not written by any current surface; that gap predates this change and is a separate finding." data ci_floor_materialization_receipt_path: String = "target/floor-materialization-receipt.txt" diff --git a/dag/gunbc/instruments/cause_assertion_census.dag b/dag/gunbc/instruments/cause_assertion_census.dag index 8b5d7029171..2a447d6fc7b 100644 --- a/dag/gunbc/instruments/cause_assertion_census.dag +++ b/dag/gunbc/instruments/cause_assertion_census.dag @@ -629,8 +629,11 @@ fn cause_complete_report(acquisition: CauseCorpusAcquisition, declarations: List } // On-demand only. Whole-corpus acquisition must not enter ordinary witness discovery. -// GUNBC_EVAL_MEMO=0 gunbc run --source-root dag --source-root src/v2 \ +// gunbc run --source-root dag --source-root src/v2 \ // --entry dag/gunbc/instruments/cause_assertion_census.dag --function census --arg report=/tmp/causes.tsv +// (The GUNBC_EVAL_MEMO=0 prefix this invocation once carried selected the seed's recompute +// realization over its eval-frame result memo; that memo is retired -- an undeclared single +// demand derives no identity -- so recompute is the only realization and the prefix is gone.) fn census(report: String) -> ProcessExit { let roots = ["dag", "src/v2"] match floor_discovery_source_inventory_live(pool_roots: roots) { @@ -642,7 +645,7 @@ fn census(report: String) -> ProcessExit { let acquisition = cause_corpus_acquire(subjects: subjects, modules: module_declaration_facts_live(pool_roots: roots)) let complete = count(acquisition.refusals) == 0 let content = if complete { - join([join(["rederive with selected realization: GUNBC_EVAL_MEMO=0 gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/instruments/cause_assertion_census.dag --function census --arg report=", report], ""), + join([join(["rederive with: gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/instruments/cause_assertion_census.dag --function census --arg report=", report], ""), cause_complete_report(acquisition: acquisition, declarations: data_decl_type_facts(pool_roots: roots))], "\n") } else { join(["ACQUISITION_REFUSED: no negative coverage conclusions are available", diff --git a/dag/gunbc/instruments/json_parse_cost_probe.dag b/dag/gunbc/instruments/json_parse_cost_probe.dag new file mode 100644 index 00000000000..f6c664f37e1 --- /dev/null +++ b/dag/gunbc/instruments/json_parse_cost_probe.dag @@ -0,0 +1,57 @@ +module tools.json_parse_cost_probe +import std.types { Bool, Int, List, String } +import std.process { ProcessExit, ExitSuccess, exit_failure } +import extdeps.filesystem.filesystem_io { Filesystem } +import extdeps.languages.json.parse { parse_json_document, JsonDocumentParsed, JsonDocumentUnreadable, json_document_gap_text } +import extdeps.languages.json.emit { serialize_json } +import v2.std.algebra { list_snoc_item } + +// THE INSTRUMENT for gunbc.recurring_failure_mode.memo_key_rehashes_a_growing_persistent_value's +// second instance: a document threaded whole through every recursive parse call, at a series of +// sizes, so the cost curve of the seed's pure-call path is re-derived by running this rather than +// transcribed. One document per member count is synthesized (Redfish-event-shaped members, each +// distinct by Id), parsed with parse_json_document, and its result -- the serialized value on a +// parse, the gap text on a refusal -- is written beside a BEGIN marker; the pair's modification +// times bracket the parse and the .out files are the semantic receipt, byte-comparable across +// binaries (memo-on seed versus admission-first seed). Three refusal subjects ride the same +// route so refusal equality is part of the same comparison: malformed, truncated, and trailing. +// +// gunbc run --source-root dag --source-root src/v2 \ +// --entry dag/gunbc/instruments/json_parse_cost_probe.dag --function probe --arg report=/tmp/json-parse-cost +// Peak retained memory is read by the shell around that invocation (/usr/bin/time -v), not here. +fn event_member(n: Int) -> String { + join(["{\"@odata.id\":\"/redfish/v1/Managers/bmc/LogServices/EventLog/Entries/", to_string(n), + "\",\"Id\":\"", to_string(n), + "\",\"Severity\":\"OK\",\"EntryType\":\"Event\",\"Created\":\"2026-09-19T00:00:00+00:00\",\"Message\":\"Sensor threshold crossed and returned to normal\",\"MessageArgs\":[\"Temp_", to_string(n), + "\",\"42.5\"],\"Resolved\":false}"], "") +} +fn members_loop(n: Int, acc: List) -> List { + if n == 0 { acc } else { members_loop(n: n - 1, acc: list_snoc_item(xs: acc, item: event_member(n: n))) } +} +fn event_log(members: Int) -> String { + join(["{\"Members\":[", join(members_loop(n: members, acc: []), ","), "],\"Members@odata.count\":", to_string(members), "}"], "") +} +fn parse_receipt(s: String) -> String { + match parse_json_document(s: s) { + JsonDocumentParsed { value: v } => join(["PARSED ", serialize_json(v: v)], "") + JsonDocumentUnreadable { gap: g } => join(["REFUSED ", json_document_gap_text(gap: g)], "") + } +} +fn measure(label: String, doc: String, report: String) -> Bool { + let begin = Filesystem.Write(path: join([report, label, "begin"], "."), content: to_string(doc.length())) + let out = Filesystem.Write(path: join([report, label, "out"], "."), content: parse_receipt(s: doc)) + begin.success && out.success +} +fn probe(report: String) -> ProcessExit { + let truncated_source = event_log(members: 50) + if measure(label: "malformed", doc: "{\"Members\":[1, 2,, 3]}", report: report) + && measure(label: "truncated", doc: substring(truncated_source, 0, truncated_source.length() - 40), report: report) + && measure(label: "trailing", doc: join([event_log(members: 3), " ]"], ""), report: report) + && measure(label: "m0250", doc: event_log(members: 250), report: report) + && measure(label: "m0500", doc: event_log(members: 500), report: report) + && measure(label: "m1000", doc: event_log(members: 1000), report: report) + && measure(label: "m2000", doc: event_log(members: 2000), report: report) + && measure(label: "m4000", doc: event_log(members: 4000), report: report) { + ExitSuccess + } else { exit_failure(reason: "json parse cost probe output refused") } +} diff --git a/dag/gunbc/legacy_extdeps_scope_frontier.tsv b/dag/gunbc/legacy_extdeps_scope_frontier.tsv index e701215923e..ffdde2a339a 100644 --- a/dag/gunbc/legacy_extdeps_scope_frontier.tsv +++ b/dag/gunbc/legacy_extdeps_scope_frontier.tsv @@ -263,7 +263,6 @@ dag/extdeps/realization/artifact_store_fs.dag dag/extdeps/realization/cache_purity.dag dag/extdeps/realization/compile_stage_memo.dag dag/extdeps/realization/emit_on_demand_host.dag -dag/extdeps/realization/eval_memo.dag dag/extdeps/realization/frame_boundary_simulated.dag dag/extdeps/realization/hermetic_fixture.dag dag/extdeps/realization/native_artifact_cache.dag diff --git a/dag/gunbc/materialization_provider_targets.dag b/dag/gunbc/materialization_provider_targets.dag index 069dad219b7..c5d55ce5566 100644 --- a/dag/gunbc/materialization_provider_targets.dag +++ b/dag/gunbc/materialization_provider_targets.dag @@ -7,7 +7,6 @@ import extdeps.realization.reconcile_in_process { parse_cache_id, typed_module_c import extdeps.realization.resolved_graph { resolved_graph_cache_id } import extdeps.realization.compile_stage_memo { compile_stage_memo_id } import extdeps.realization.parse_table_memo { parse_table_memo_id } -import extdeps.realization.eval_memo { eval_memo_id } import extdeps.realization.native_artifact_cache { native_artifact_cache_id } import std.dissolution { DissolutionCondition, unbound_dissolution } @@ -89,13 +88,6 @@ data materialization_provider_targets: List = [ reason: "the v2 ParseTable memo is the standing DESIGN section 2 hand-rolled-cache debt; its lookup answers are untyped hits/misses on an in-process map", dissolution: unbound_dissolution(description: "ParseTable grounds on the Realization carrier and its lookups adopt the contract's typed outcomes") }, - ProviderContractTarget { - cache: eval_memo_id, - cache_row: target_decl(module_path: "extdeps.realization.eval_memo", decl_name: "eval_memo_facts"), - consumer_seam: target_decl(module_path: "gunbc.plans.cli_run_hollowing_plan", decl_name: "cli_run_hollowing_plan"), - reason: "the interpreter eval-frame memo serves verified hits with its own ad-hoc verify-on-serve arm — the contract's wrong-content refusal, hand-rolled; the host seam is the interpreter builtin bridge (hollowing-plan area 2.13)", - dissolution: unbound_dissolution(description: "eval-memo serves through provider_serve so the verify-on-serve arm is the shared ProviderRefusedWrongContent, not a private one") - }, ProviderContractTarget { cache: native_artifact_cache_id, cache_row: target_decl(module_path: "extdeps.realization.native_artifact_cache", decl_name: "native_artifact_cache_facts"), diff --git a/dag/gunbc/pure_demand_admission_seed_growth.dag b/dag/gunbc/pure_demand_admission_seed_growth.dag new file mode 100644 index 00000000000..601b462a9cc --- /dev/null +++ b/dag/gunbc/pure_demand_admission_seed_growth.dag @@ -0,0 +1,52 @@ +module gunbc.pure_demand_admission_seed_growth + +import gunbc.roadmap_model { RoadmapNodeId } +import gunbc.seed_growth { SeedGrowthJustification } +import std.decl_ref { DeclarationRef, WholeDeclaration } + +// FORWARD-FREEZE RECEIPT for the change that makes admission precede identity on the seed's +// pure-call path (gunbc.recurring_failure_mode.memo_key_rehashes_a_growing_persistent_value, +// second instance). The change is a NET DELETION of the seed: the eval-frame result memo +// (EvalCallMemo, its entry cap, its GUNBC_EVAL_MEMO realization switch, its frame-exit eviction, +// its get/put/counters, and value_fast_eq) and its provider row extdeps.realization.eval_memo are +// gone, because std.materialization_ladder never discharges a demand into a provider scoped to one +// shared-state frame -- the memo's admitted population was empty by construction and the identity +// it derived per call was pure cost. Deletions offset nothing under gunbc.seed_growth_admission, +// so the two items the change ADDS are enumerated here on their own. +// +// WHAT IS ADDED, AND WHY IT IS AN ODOMETER AND NOT A DECISION. `argument_identities_derived` +// reads a per-frame count of argument positions that reached `eval_recompute_arg_key`; +// `note_argument_identity_derived` is its single writer, called from the three keying sites +// (`eval_recompute_key`, `eval_recompute_partial_key`, `cross_claim_args_hash`) and nowhere else. +// Neither adds an arm, a decision or an evaluation order. They exist so the fact this change +// establishes -- an undeclared single pure demand derives NO identity -- is executable evidence +// rather than an assertion: v1_compiler tests/pure_demand_recompute_admission reads the odometer +// back at zero on the production route and goes red when unconditional keying is restored, with the +// recompute-trace ledger (which legitimately keys) as its positive control. The count is also +// printed on the [recompute-trace] totals line so the ledger discloses its own keying work. +// +// WHY RUST IS STILL NEEDED: the keying sites are inside the seed evaluator's call path, which is +// the boundary this change repairs; no .dag fold observes an individual identity derivation, and a +// .dag-side counter would be a second representation of a count the evaluator alone can produce. +// +// WHY IT IS ADMITTED AGAINST THE v1 FREEZE: gunbc.v1_maintenance_standing v1_seed_standing admits +// by PURPOSE. The seed interpreter is what executes every v2 source today -- the self-host compile +// (v2.compiler.compile), the required floor's witnesses and every instrument -- and each of those +// paid an identity derivation per pure call that no admission had asked for, quadratic wherever a +// fold threads a growing value through recursion. Removing a cost the ladder already prescribes +// away, and leaving the seed smaller, is BehaviorPreservingRedundancyRemoval in the shape the +// standing already records; the semantics are unchanged (recompute was always one of the two +// realizations, declared identical) and the refused classes are untouched: no new language +// behavior, no compatibility obligation (GUNBC_EVAL_MEMO is retired, not kept as a no-op arm), no +// escape hatch, no seed capability, and the exported surface grows by exactly the one reader +// enumerated below. +data pure_demand_admission_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { + hand_authored_declarations: [ + DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "argument_identities_derived", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "note_argument_identity_derived", field: WholeDeclaration } + ], + reason: "A per-frame ODOMETER of argument identities derived, with one reader and one writer, added so that 'an undeclared single pure demand derives no identity' is executable evidence with an enrolled RED (tests/pure_demand_recompute_admission) rather than a sentence. No arm, decision or evaluation order is added; the change it accompanies deletes the eval-frame result memo, its realization switch and its provider row, because std.materialization_ladder rule 5 prescribes Recompute for an undeclared single pure demand and rule 1 prescribes Share for a within-frame repeat, so a within-frame result memo had no admitted population. Admitted against the v1 freeze by purpose: every interpreted v2 route, including the self-host compile and the required floor, paid the deleted per-call identity derivation.", + owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, + trigger: "Delete both items and this row when demand identity is derived by the demand engine (docs/plans/demand-engine-program.md M1: demand identity and the dependency read set as modeled carriers), at which point which demands derive an identity is a fact of the derived demand population and the seed's keying sites -- the recompute-trace ledger and the cross-claim tier -- retire with the interpreter under the failure-mode row's program remedy. NOT retired by the odometer reading zero everywhere: zero is the property the control guards, and deleting the guard because it holds is deleting the evidence that it holds.", + current_boundary: "One Cell on InterpContext, incremented at the three keying sites and read by the enrolled control and by the [recompute-trace] totals line. It changes no verdict and no value; cost on the production route is zero increments (no keying site runs there), and under the trace ledger one Cell add per argument position beside a content hash that already dominates it." +} diff --git a/dag/gunbc/recurring_failure_mode/memo_key_rehashes_a_growing_persistent_value.dag b/dag/gunbc/recurring_failure_mode/memo_key_rehashes_a_growing_persistent_value.dag index af14a25ed8f..a2e2878d5fe 100644 --- a/dag/gunbc/recurring_failure_mode/memo_key_rehashes_a_growing_persistent_value.dag +++ b/dag/gunbc/recurring_failure_mode/memo_key_rehashes_a_growing_persistent_value.dag @@ -1,6 +1,7 @@ module gunbc.recurring_failure_mode.memo_key_rehashes_a_growing_persistent_value import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } import gunbc.recurring_failure_mode { RecurringFailureMode } data memo_key_rehashes_a_growing_persistent_value: RecurringFailureMode = RecurringFailureMode { @@ -8,10 +9,17 @@ data memo_key_rehashes_a_growing_persistent_value: RecurringFailureMode = Recurr receipts: [ "INVALID STATE: a memoized pure fold carries a growing persistent Map, but the memo demand key recursively hashes the contents of each fresh root. Sharing inside the value does not share its content hash across roots. A constant-cost map update is surrounded by a growing key-construction cost, and successive keys retain successive argument values. HARM: an otherwise incremental census becomes quadratic in identifier count before it can report its first corpus result.", "INSTANCE: v1_interpreter.eval_pure_named_call constructs eval_recompute_key before lookup or admission. Composite argument identity is content-hashed with allocation-local hash reuse; a new persistent Map root is a new allocation. tools.cause_assertion_census.cause_identifier_counts exposes this cost while consuming the parser's already-acquired Token stream. INSTRUMENT: tools.cause_identifier_cost_probe.probe, invoked with gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/instruments/cause_identifier_cost_probe.dag --function probe --arg report=/tmp/cause-identifier-cost. Each begin/end output pair brackets identifier counting after fixture construction; its file modification times expose the cost curve and its payload verifies the resulting key cardinality. Timings are derived from this instrument, not transcribed here.", - "REALIZATION SELECTION: extdeps.realization.eval_memo declares GUNBC_EVAL_MEMO=0 a diagnostic recompute realization with identical semantics. The census invocation discloses that selection. tools.cause_assertion_census.bounded_census supplies the bounded module-identity control: run the same production and witness subjects under both realizations and compare complete rows by declaration identity, including all fields and identity refusals. Agreement of counts alone is not semantic agreement.", - "RUNG FOUND AT: mitigatable by diagnosis and realization selection. The found condition is repeated whole-value memo-key construction over fresh roots sharing unchanged persistent structure; no structural guard stops that work or the retention of successive argument roots. CURRENT MITIGATION: the disclosed census invocation selects extdeps.realization.eval_memo's existing recompute realization, avoiding memo-key construction on that invocation only. The bounded memo-on/off identity comparison is a semantic experiment, not containment of other memoized demands. The defect remains on retained memo-enabled paths.", + "REALIZATION SELECTION (as found, 2026-09-18; RETIRED 2026-09-19 -- the provider row extdeps.realization.eval_memo and its GUNBC_EVAL_MEMO switch were deleted by the REPAIR receipt below, so there is no longer a second realization to select and the census invocation carries no prefix): at the time of the first instance extdeps.realization.eval_memo declared GUNBC_EVAL_MEMO=0 a diagnostic recompute realization with identical semantics, the census invocation disclosed that selection, and tools.cause_assertion_census.bounded_census supplied the bounded module-identity control -- the same production and witness subjects under both realizations, complete rows compared by declaration identity including all fields and identity refusals; agreement of counts alone is not semantic agreement. That control remains the shape of the semantic receipt (tools.json_parse_cost_probe re-derives it across binaries for the second instance), but the realization it selected between is gone.", + "RUNG FOUND AT (2026-09-18): mitigatable by diagnosis and realization selection. The found condition is repeated whole-value memo-key construction over fresh roots sharing unchanged persistent structure; no structural guard stops that work or the retention of successive argument roots. THE MITIGATION AS FOUND, SINCE SUPERSEDED: the disclosed census invocation selected the eval-frame memo's recompute realization, avoiding memo-key construction on that invocation only, while the defect remained on every retained memo-enabled path; that selection is no longer available or needed, because the REPAIR receipt below removes the keying from every undeclared demand rather than from one invocation.", "ATTAINABLE CEILING: structurally guaranteed for the declared population of memoized pure-call demands over persistent composite arguments. Unchanged shared structure must carry reusable key evidence, so a persistent update constructs key evidence only for changed structure; key retention must follow an explicit bounded demand lifetime rather than retain every successive argument root. This requires a producer and consumer contract for persistent-structure key evidence and retention ownership, missing at v1_interpreter.eval_recompute_key and eval_pure_named_call. An allocation-local hash cache on each fresh root does not provide that capability. NEXT-RUNG TRIGGER: every retained demand in that population consumes such evidence without re-traversing unchanged structure, and expired demand keys release their retained roots under the declared lifetime contract.", "PROGRAM REMEDY: retire the seed implementation rather than author a new seed cache or evaluator patch. RETIREMENT TRIGGER: v1_interpreter.eval_pure_named_call and eval_recompute_key are absent from EVERY retained demand path in the declared population, including tools.cause_assertion_census.census and other interpreted pure folds; moving the census alone to the native route does not establish retirement of this class. Interpreter retirement is the program remedy, not the property's attainable ceiling. This row admits no new cache, evaluator patch, or census-specific bypass.", + "SECOND INSTANCE (2026-09-19, swift-newt-222, gunbc built at 488aa317 on srv1 arm64): the same key construction over a growing STRING rather than a persistent Map. extdeps.languages.json.parse threads the whole document through every recursive *_at(s, i) call and Value::Str is hashed in full per call (no allocation-local reuse exists for strings), so parsing is quadratic in document size on the memo-enabled realization; perf attributed 79 percent of parse-phase samples to the SipHash write under eval_pure_named_call, and the recompute trace on a 112 KB document reported keyed_calls=156685 distinct_keys=134565 duplicated_keys=545 wasted_ms=44 -- seconds of key building to avoid tens of milliseconds. Re-derive with tools.json_parse_cost_probe.probe, never from these figures.", + "EARLIEST UNJUSTIFIED BOUNDARY (DESIGN 6b), read from the ladder downward: std.materialization_ladder rule 5 prescribes Recompute for a single undeclared pure demand and rule 1 prescribes Share, never Memoize, for a repeat whose least common ancestor is a shared-state frame. The eval-frame result memo (extdeps.realization.eval_memo, since deleted) was a provider whose scope was ONE such frame, so no demand it could see was ever discharged into it by the ladder -- its admitted population was empty by construction -- yet it derived an identity for every pure call before any admission question was asked. Both instances of this row are that one boundary: the identity was built where no judgment had asked for it. The symptom-link patches this row refused (an allocation-local hash reuse for strings, a name allowlist, an adaptive cache) all keep the boundary and cheapen the work done past it.", + "REPAIR (the seed change this row admits because it DELETES a seed cache rather than authoring one): v1_interpreter.eval_pure_named_call now consumes the admission BEFORE identity. The two provider tiers that remain -- the cross-claim tier admitted by the resolved-declaration roster of v2.workflow.floor_pure_producer_share, and the parse-table memo admitted by the Memoize verdict carried on the table -- each decide admission first and derive their key only for an admitted demand; an undeclared single demand derives no identity, looks nothing up and retains nothing. The eval-frame result memo, its per-ctx realization switch GUNBC_EVAL_MEMO, its frame-exit eviction and its hit/miss counters are deleted with their provider row. The recompute-trace ledger (GUNBC_RECOMPUTE_TRACE=1) still derives identities, as the rule-4 measurement instrument it always was, and serves nothing.", + "RUNG AFTER REPAIR, at the declared grain and stated no higher than its executed evidence (DESIGN 4b(1)). For the population of UNDECLARED pure demands in the seed interpreter the class is MECHANICALLY PREVENTABLE, not structural: the invalid state stays writable -- one call to eval_recompute_key above the admission branch of eval_pure_named_call restores it -- and what refuses it is a control, v1_compiler tests/pure_demand_recompute_admission an_undeclared_single_pure_demand_derives_no_identity_and_is_never_served, which reads the frame's argument-identity odometer back at zero and goes red when unconditional keying is restored, with the trace ledger as its positive control. That control is off the merge path with the rest of the seed unit suite (gunbc.rung_drop rust_unit_tests_off_the_merge_path), so even rung 2's executing condition holds only under local diligence and the required floor's cost ceilings, which fire on the same regression one consumer later; the ceiling of this population is structural -- an evaluator whose keying sites are reachable only from an admitted provider has no constructor for the state -- and its next-rung trigger is the demand engine deriving demand identity (docs/plans/demand-engine-program.md M1), which retires the seed's keying sites with the interpreter. For the DECLARED population -- a roster-admitted cross-claim producer whose argument is a growing persistent value -- the found condition still stands and this row's ceiling, next-rung trigger and program remedy are unchanged: the roster is bounded and reviewed, and a row whose argument grows is the admission criterion's serve-below-recompute test failing, not this class dissolving.", + ], + evidence: [ + DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_pure_named_call", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "argument_identities_derived", field: WholeDeclaration }, ], - evidence: [], } diff --git a/dag/gunbc/rung_drop/determinism_transitive_reachability.dag b/dag/gunbc/rung_drop/determinism_transitive_reachability.dag index f07a6456a36..14a6851239d 100644 --- a/dag/gunbc/rung_drop/determinism_transitive_reachability.dag +++ b/dag/gunbc/rung_drop/determinism_transitive_reachability.dag @@ -121,6 +121,6 @@ data determinism_transitive_reachability: RungDrop = RungDrop { "v2.lens.affected_set.corpus_dependency_view (fn-arrow composition, deleted)", "v2.lens.affected_set.entry_selection (fn-arrow declarations, deleted)", ], - restoration_trigger: "THE TRIGGER, STATED ONCE AND AT CAPABILITY GRAIN: the reachability walk's cost becomes proportional to WHAT IT REACHES rather than to the POOL IT IS HANDED, sufficient for determinism_transitive_holds to reach a verdict within the per-claim line at directory grain WITHOUT NARROWING THE SUBJECT. Nothing else retires this row. Everything after this sentence is the evidence for that trigger and the record of what was tried; none of it is a second trigger, and where a later paragraph names an obligation belonging to another subject it says so explicitly and that obligation is carried by its own row. THE TRIGGER WAS REPLACED RATHER THAN WEAKENED, 2026-09-07. It previously prescribed a specific implementation -- that the callee lookup answer BY INDEX rather than by scanning the candidate pool -- and that prescription is refuted by execution below. A trigger naming a REPAIR that does not work is worse than one naming none, because it is satisfiable while the capability stays dead. This one names the COST SHAPE the capability requires, which is what was actually measured, and is satisfiable only by achieving it. The previously declared capability (the callee lookup answering BY INDEX rather than by scanning the candidate pool) is withdrawn because the mechanism it was derived from is refuted by execution. THE REFUTATION, BY REASONING: v2.std.fn_index.decls_in_modules is a plain-valued call with hashable arguments, and the v1 interpreter's eval-frame call memo is on by default (GUNBC_EVAL_MEMO), keyed by fn identity x argument identity -- so the loop-invariant that trigger asked a lane to hoist had already been hoisted by the interpreter, and the per-lookup rescan named as the cost was not being paid. THE REFUTATION, BY MEASUREMENT: gunbc#10753 built exactly the prescribed index and measured it against the unindexed lookup at directory grain under a verdict rule pre-registered before the numbers existed; that PR carries the method, the pre-registration and the figures, and is the citation for them rather than a copy here. Its verdict is that the index is HARMFUL -- it adds cost and removes none -- and that both arms remain far above the per-claim line, so the prescription was not merely insufficient but wrong. WHAT SURVIVES: the O(reached x pool) FIT, unchanged and still good evidence. WHAT DOES NOT: the causal sentence behind it. ATTRIBUTION SO FAR, AND THE INSTRUMENT IS NOT IN THE TREE -- THAT IS STATED FIRST BECAUSE IT IS THE FACT A READER MUST HAVE BEFORE ANY FINDING BELOW. The six-arm probe that produced these findings was written, run, and DELIBERATELY NOT LANDED, and three placements were tried and refused before that conclusion was reached (gunbc#10757). Under scratch-probe/, outside every source root, the floor refused every arm as declined_changed_witness_outside_discovery: a planned witness it cannot reach is a typed refusal, not a skip. Moved into the long home it was refused again by floor DISCOVERY, which requires a test-marked declaration to live in a *_test.dag file. Renamed to satisfy that, the arms RAN and blocked the lane sixteen ways -- interrupted before verdict, completed over the per-claim cost requirement, and changed-witness-planned-without-terminal-verdict. THE RULE THAT MAKES THIS GENERAL RATHER THAN A BAD CHOICE OF DIRECTORY: the changed-witness selector REPLACES the ordinary disposition, so a long-home decline, a fixture decline and a declared cost-debt withhold are all overridden for any claim whose FILE THE CHANGE TOUCHES. There is therefore NO location in this repository where a multi-second claim can be added, or later edited, without running on the floor of the change that touches it. An instrument of this cost cannot be a claim here at all. HOW TO RE-DERIVE THE FINDINGS: rebuild the arms locally and run them under claim_batch, which charges each arm separately -- one arm per invocation when peak RSS matters, because claim_batch reports VmHWM for the process at exit. The arms are acquisition alone; the closure list alone; the reachability walk alone; the walk plus the determinism fold; and two arms holding the entry and the CLOSURE fixed while enlarging only the candidate POOL so the reached set is unchanged. Frame structure is itself a variable, so name it whenever a ratio is quoted. THIS IS A WEAKER CITATION THAN A LANDED INSTRUMENT AND IS RECORDED AS ONE: nothing in the tree re-derives these findings, so a lane taking up the trigger rebuilds the arms before quoting anything here. That is the honest cost of the constraint above, not a preference. What it establishes: the determinism fold is NOT the cost -- adding determinism_findings over every reached declaration's whole subtree does not rise above run-to-run noise, so a lane optimising it or its concat accumulator will move nothing; and the reachability WALK is pool-sensitive at a fixed reached set, which corroborates the pool term and locates it inside the walk. WHAT REMAINS UNATTRIBUTED, AND IS NOT A SECOND TRIGGER BUT AN OPEN QUESTION UNDER THE ONE ABOVE: WHICH construct inside that walk is pool-proportional, given that the per-lookup rescan is refuted. Naming it would make the repair easier to find; it is not required to retire this row, because the trigger is stated as the shape the cost must reach and a lane that reaches it has retired this drop whether or not it can say which construct was responsible. ONE CANDIDATE WAS PROPOSED HERE AND IS NOW REFUTED BY EXECUTION, RECORDED SO THE NEXT LANE DOES NOT SPEND ITS DISPATCH RE-KILLING IT. The candidate was the eval-frame memo's own keying -- that a probe must derive a key from the pool-sized argument on every call, so removing a pool-sized scan reintroduces a pool-sized cost in the key. Its death condition was written before the arm ran: if the pool sensitivity SURVIVES with GUNBC_EVAL_MEMO=0, keying is not the cost. Run the probe's a/c/e/f arms with the memo off and the sensitivity survives essentially unchanged, so the walk is pool-proportional INTRINSICALLY -- with the memo and without it -- and no repair to keying removes that term. The same arm establishes the opposite of what the candidate assumed: the memo is not a cost here but very nearly the whole performance of this walk, so any later repair in this area must PROTECT it rather than trim it. TWO MECHANISM SENTENCES HAVE NOW DIED ON THIS SUBJECT -- the candidate-pool rescan of gunbc#10744, and this one -- and the fit has survived both, which is why this row states a fit and refuses to state a cause. A third sentence does not go here until an arm supports it. WHAT IS ESTABLISHED IS NOT A MECHANISM BUT A SHAPE, AND THE SHAPE IS THE FINDING: THE WALK'S COST IS PROPORTIONAL TO THE POOL IT IS HANDED RATHER THAN TO WHAT IT REACHES. Three independent measurements, all re-derivable from the named instrument: the reached-set size is pinned EQUAL across a small pool and a pool several times larger, so reach is held constant while cost moves; the walk's cost ratio between those two pools is the same with the eval-frame memo ON as with it OFF. That third one is what makes this a shape rather than an implementation detail -- a cost that tracks the pool identically with a caching tier present and absent is not a property of that tier, of any key, or of any index, but of the WALK, and it is INVARIANT UNDER EVERY MECHANISM PROPOSED AND REFUTED HERE. That invariance is why this row states it as established while stating no cause. A measured cost-shape defect with no carrier is how a defect becomes ownerless, and DESIGN 2's bare-minimum-cost rule prices a PROVEN cost-shape defect as always worth fixing regardless of realized n, without waiting for the cause to be named. Reach-proportional is what this walk should be; pool-proportional is what it measures as. A CONSTRAINT ON ANY FUTURE REPAIR, MEASURED AND RECORDED HERE BECAUSE THE NEXT LANE WILL NOT EXPECT IT: with GUNBC_EVAL_MEMO=0 the same arms run roughly TWO ORDERS OF MAGNITUDE slower. The eval-frame memo is not a cost on this path, it is very nearly the whole performance of it. A later simplification that bypasses or replaces the memo -- which will look clean, because the memo is invisible in the .dag source -- makes this walk about a hundred times slower. Protect it; do not route around it. WHAT THIS ROW DOES NOT CLAIM, having measured it and found otherwise: that the floor claim's own excess over the per-claim line is explained by anything above. Reproduced term by term at the floor's own grain the claim runs at well under half the line, and running it beside deliberately pool-diverse company on one machine does not move it. So the shape defect above is REAL AND IS NOT THE BLOCKER'S EXCESS, and a lane that fixes the shape should expect the intermittency to survive it. AND THE DISPOSITION THAT FOLLOWS IS NOT THE ONE A READER WILL REACH FOR. Learning that the claim's own cost is well under half the line makes a bigger line look reasonable, and it is not: a budget cannot distinguish a claim whose true cost is half the line from one measured AT the line when the environment is separately recorded as swinging by more than a factor of two on BYTE-IDENTICAL evaluator steps. That is a MEASUREMENT TRUSTWORTHINESS defect and not a THRESHOLD defect, and the repair for it is never a bigger number: a number raised to accommodate an unattributed cost stops the refusal firing without stopping the wrongness and destroys the signal that the measurement cannot be trusted, which is the escape hatch DESIGN 5 forbids. A READING, LABELLED AS ONE BECAUSE IT EXPLAINS EVERY ARM AT ONCE AND THAT IS EXACTLY WHEN TO BE CAREFUL: the eval-frame memo is evicted PER WITNESS FRAME, so diversity BETWEEN claims is cleaned up while diversity WITHIN one frame is not. That predicts all three observations without residue -- the floor claim is unmoved when run beside deliberately pool-diverse company, two walks over two pools in ONE frame cost an order of magnitude more than the same two walks in separate frames, and the floor claim is the one-frame one-pool case that never blows up. THE CONSEQUENCE A LATER LANE MUST NOT MISS: that within-frame blowup DOES NOT BEAR ON THIS BLOCKER. Whoever re-derives it will have found something real and will be tempted to call it the cause. Its payer is not retention, refuted by two independent instruments -- an arm holding the walk count fixed while varying the pools retained, and the peak-RSS column, which moves a few percent while the time moves an order of magnitude. Before those two, every arm inferred memory from time, so a timing result and a memory story could not disagree; these can, and do not. A re-deriver must also pin whether each arm re-pays its acquisition or is served from a cross-witness share, which the probe does not settle. AND A RE-DERIVER MUST NOT CARRY ANY FIGURE HERE ONTO THE MACHINE THAT BLOCKS. Every measurement behind this row was taken on remote build executors; the per-claim line is enforced on the required-lane CI runner, which is a different machine population. A distribution measured on the first says nothing about the second, and treating it as though it did is the same error as comparing an isolated figure to a CI figure -- true measurement, wrong subject. THE BLOCKER IS ACCOUNTED FOR, POSITIVELY, ON THE POPULATION WHERE THE LINE IS ENFORCED, AND IT IS NOT THIS SUBJECT. Harvest the retained required-floor claim-cost artifacts from the successful main runs, take this claim's rows, and GROUP THEM BY eval_steps so that work is held constant -- the whole point of the existing pairing authority. AND READ THE ENFORCING POPULATION FROM THE ARTIFACT RATHER THAN FROM A CLOCK: required-floor-claim-cost is published by every completed witnesses run, so this claim's cost on the population that actually enforces it is readable with no push, no lane and no window -- an earlier reading of this row treated a merge freeze as preventing measurement, which confuses producing a new head with reading a receipt from a run that already finished. PARTITION THOSE ROWS BY eval_steps AND BY NOTHING ELSE. eval_steps is deterministic work rather than a clock, so it is immune to runner variance and pool contention, it states the effect of a work-removing repair directly instead of inferring it from a noisy distribution, and it is what makes the partition AUDITABLE: a run classified as pre-repair by its id and date was found to be a post-repair sample only because its eval_steps disagreed with its neighbours. Partitioning by run id, by date or by branch silently mixes the arms and yields a smaller, believable, wrong delta. AND READ THE PRE-REPAIR ARM AS A DISTRIBUTION THAT WORSENS AS IT GROWS, which is the strongest form of the original complaint rather than a restatement of it: as the pre-repair sample grew the top of the range rose and the margin under the 500ms limit fell, with a growing minority of runs landing within 50ms of the line. A shrinking margin under a GROWING sample is not noise -- noise widens a range symmetrically around a stable centre, while this arm's maximum climbs, which is what an intermittent blocker looks like before it becomes a constant one. That is why this class was worth repairing at a realized n that looked survivable. The large majority of recent runs share one step count, and across that group -- at BYTE-IDENTICAL evaluator work, with no change to this claim and none to the tree -- the observed CPU spans a wide factor whose top reaches essentially the whole per-claim ceiling. THE FIGURES ARE NOT WRITTEN HERE ON PURPOSE, and this sentence is the instrument rather than the reading: harvest required-floor-claim-cost from the completed main runs, take this claim's COMPLETED rows, group them by eval_steps, and read the spread and the maximum of the largest group against the limit. A number copied here would be a run-local figure that nothing re-derives, which is the defect this same field names two paragraphs down. A claim whose cost distribution at fixed work already touches its own line does not need a cost defect, a drift, an accounting hole, or any mechanism to refuse intermittently. It needs only to be sampled again. THAT IS THE INTERMITTENCY, and it is why this refuses on changes that touch nothing near it. AND THE ARM IT REFUSES THROUGH IS NOT AN OVERRUN, WHICH MATTERS BECAUSE THE TWO HAVE DIFFERENT DISPOSITIONS AND ONLY ONE OF THEM BLOCKS. Harvest the RED main runs as well as the green ones and this claim's blocking row reads verdict_reached=FALSE with a right-censored cost and a LOWER eval_steps count than any completed run -- fewer steps precisely because it never finished. On red runs where it did finish it came in under budget and those runs were red for other reasons. So the failure mode is INTERRUPTED-BEFORE-VERDICT and not COMPLETED-OVER-BUDGET: the deadline preempts the witness, whether it would have passed is UNKNOWN, and the reported cost is a bound with no upper limit. That is the stronger reason such a row is inadmissible in the distribution above -- not merely that a bound cannot be divided as a cost, but that it is not a sample from that distribution AT ALL, being the cost of a computation that did not happen. AND eval_steps ON A RIGHT-CENSORED ROW IS A TRUNCATION ARTIFACT, NOT A WORKLOAD FIGURE -- one sentence here to save the next harvester an afternoon. An interrupted claim stopped wherever it had got to when the deadline fired, so its step count records how far it got and nothing else: two observed interrupts on this claim truncate at different step counts, both far below every completed run, and neither denotes a workload. The harvest above groups by eval_steps to hold work constant, which is correct ONLY over completed rows. Group the censored ones the same way and they form a third apparent level out of nothing but where the deadline landed -- a bogus population that will look exactly like the drift finding this row already withdrew once. The two arms are the same underlying fact reached differently: a claim whose completed cost distribution touches its ceiling will, on a bad draw, hit the deadline BEFORE finishing, and then it does not report a larger number, it reports no verdict. THE CONSEQUENCE FOR THE REPAIR IS THAT MARGIN IS WORTH MORE THAN IT LOOKS: an overrun is a cost debt on a claim that PASSED, while an interrupt leaves the subject UNDECIDED and is the arm that refuses. Headroom is bought against the second. AND THE REFUSAL BEHAVIOUR OF THAT ARM IS A SEPARATE FILED CLASS, cited here rather than re-derived and deliberately NOT absorbed into this row: gunbc.recurring_failure_mode.non_verdict_disposition_surfaces_as_refusal records that the floor computes the difference between THIS SUBJECT IS WRONG and I DID NOT FINISH LOOKING AT THIS SUBJECT and then discards it at the aggregate boundary, so the red check and the merge gate receive one bit whose only affordance is to run it again. Its specimen is a run refused by interrupted rows in which ZERO claims failed. That is a different defect from this one, it is what makes an interrupt here block an unrelated change, and it is that row's to repair. TWO READINGS WERE PROPOSED AND WITHDRAWN ON THE WAY TO THAT, RECORDED BECAUSE BOTH ARE TEMPTING. A drift -- the claim walking toward the line across a level change -- dissolved once the smaller step-count group was compared against the larger group's actual range rather than against its own mean: the apparent second level sits inside the first population's spread. And a small-sample variance figure understated that spread, which is what made the two groups look separated at all. One error, twice: a sample too small to see its own width. THE REFUSAL IS CORRECT AS A MEASUREMENT AND WRONG AS AN ATTRIBUTION, and the distinction decides the repair. The CPU really was consumed, so the gate is not lying; but that cost is not a property of this claim's code, so charging it to this claim attributes it wrongly. A per-claim threshold enforced on ONE DRAW from a distribution this wide is estimating a statistic it cannot see from a single sample. Raising the ceiling would silence the wrong half and destroy the evidence, which is why no number moves here. THE REPAIR IS MARGIN, AND IT IS THE POOL-PROPORTIONAL SHAPE ALREADY ESTABLISHED ABOVE -- which needs no separate justification, being a DESIGN 2 bare-minimum-cost defect that is fixed regardless of realized n. It was never the blocker and it is still the fix. AND THE ACCEPTANCE TARGET IS DERIVED FROM THE MEASUREMENT RATHER THAN GUESSED: holding the line against a spread of that width requires the MEDIAN to sit below the ceiling divided by the spread, which gives the required reduction directly -- re-derive both the median and the spread from the harvest named above and take the ratio, rather than reading a percentage here. AND THE ACCEPTANCE EVIDENCE IS A DISTRIBUTION, NEVER A GREEN RUN. A claim this near its ceiling under this spread goes green sometimes with nothing repaired, so the first green after any change carries almost no information and is exactly what will be offered as proof. What establishes a repair is a distribution at EQUAL WORK, before and after, on the enforcing population. The before is the harvest described above and it exists today. IF MARGIN CANNOT BE OBTAINED, the remaining honest arm is a further bounded drop naming the shape fix as its trigger at capability grain. Never a bigger ceiling. A RECEIPT FOR THE COST COPRODUCT, RECORDED BECAUSE IT IS A RUNG CLAIM WITH AN EXECUTION BEHIND IT RATHER THAN A DESIGN INTENTION. The observation that opened this investigation was a budget-refused reading -- a lower bound on a cost that never completed, not a cost. It was the most persuasive number available and it was on the correct population, and it is INADMISSIBLE in any ratio. gunbc.floor_cost_distribution refuses it STRUCTURALLY, because its cost reading is a coproduct and a bound has no constructor a cost fits into; no reviewer's judgement had to catch it. That class was filed after a rendered figure just over this same ceiling was read as a completed cost, and it then prevented the identical error in a later lane that knew the story and still reached for the number. AN INSTRUMENT GAP IS DECLARED HERE RATHER THAN PAPERED OVER. The ANALYSIS for the environment-variance question already exists and is not to be re-minted: gunbc.floor_cost_distribution models the cost reading as a coproduct so a censored bound cannot be divided as a cost, and identity_inflation_permille_at_equal_work pairs rows across two runs by identity AND by equal evaluator steps, which is precisely CPU divergence at byte-identical work. What does not exist is an ACTUATOR that runs one claim N times in N processes over one tree and hands the pairs to it, and the actuator that does exist runs only inside CI. So the variance figures recorded elsewhere in the seed were transcribed not because the concept lacked a home but because nothing could RE-RUN it on demand. A NEIGHBOURING CLASS THIS INVESTIGATION SURFACED, FILED IN ITS OWN ROW AND CITED HERE RATHER THAN STORED HERE: gunbc.recurring_failure_mode.inflation_fold_cannot_name_the_environment_it_measures. It is not a trigger of this drop and cannot retire it -- its subject is whether a per-claim cost MEASUREMENT can be trusted, which is a different invalid state with a different harm. It is named here for one reason only: a lane meeting THIS row's trigger must show the cost shape changed, and the evidence for that is a distribution over repeated runs, which is exactly the analysis that class governs. Read it before quoting any such distribution. A repair must be derived from measurement rather than from a plausible mechanism -- that is what the refutations below establish -- but it is the cost SHAPE that must change, not a named construct that must be found first. SUFFICIENT FOR (unchanged, and still the thing being restored): determinism_transitive_holds with pool_roots=['src/v2/lens'] and pool_files=[] reaching a verdict within the per-claim line at directory grain, WITHOUT NARROWING THE SUBJECT -- scoping pool_roots to the modules the walk happens to reach remains the trap and not the repair, because it lowers the number by shrinking the population, leaves the cost shape intact, and re-breaks the moment the subject widens, which is the widening this drop exists to restore. COST SHAPES IN THIS WALK ARE REAL AND ARE EXPLICITLY NOT THE COST, recorded so a later reader does not fix them and believe the defect is gone. THREE OF THEM ARE NOW REPAIRED and are named in the past tense because their symbols no longer resolve: call_reachable_decls_go scanned `reached` linearly per seed through a decl_in_list helper that is deleted, and now answers membership by keyed lookup over a seen map; it appended to `reached` with a copied accumulator and now conses and reverses once at the end; and list_append(rest, callee_decls) copied the worklist every step and is now guarded so an empty callee list does not copy it. REPAIRING THEM DID NOT RETIRE THIS DROP AND WAS NEVER EXPECTED TO: the pool scan in decls_matching_callee is untouched, and this row is retired by the trigger stated at the head of this field -- the cost shape -- and by nothing else. ONE SHAPE IN callees_from_node IS AN ADMITTED, UNRESOLVED OBLIGATION rather than a repair: its duplicate suppression is a linear scan of the accumulated list per callee, which is quadratic in the callees of one declaration and is subject to the same bare-minimum-cost rule. A map-keyed arm was written and measured SLOWER than the list scan at the realized callee counts and was reverted on that measurement; big-O did not grant permission to ship the slower realization, and equally the slower first attempt did not retire the defect it was aimed at. The obligation dissolves when the walk is asked at a grain whose per-declaration callee counts are large enough for the keyed arm to win, and it is recorded here rather than in the source so that it is folded with the rest of this row. THE REMAINING UNREPAIRED SHAPES: determinism_transitive_findings folds with concat(acc, determinism_findings(...)), a copied accumulator that is FREE while the corpus is clean and degrades quadratically exactly when findings appear, so it is invisible in every green run and expensive only when something is already wrong. determinism_live_closure_modules folds list_snoc_item over module_declaration_facts_live(pool_roots: []), a copied accumulator over a list that is empty today. Until the trigger stated at the head of this field is met, determinism over the fn-arrow call graph is unverified. The way out is that trigger and nothing else.", + restoration_trigger: "THE TRIGGER, STATED ONCE AND AT CAPABILITY GRAIN: the reachability walk's cost becomes proportional to WHAT IT REACHES rather than to the POOL IT IS HANDED, sufficient for determinism_transitive_holds to reach a verdict within the per-claim line at directory grain WITHOUT NARROWING THE SUBJECT. Nothing else retires this row. Everything after this sentence is the evidence for that trigger and the record of what was tried; none of it is a second trigger, and where a later paragraph names an obligation belonging to another subject it says so explicitly and that obligation is carried by its own row. THE TRIGGER WAS REPLACED RATHER THAN WEAKENED, 2026-09-07. It previously prescribed a specific implementation -- that the callee lookup answer BY INDEX rather than by scanning the candidate pool -- and that prescription is refuted by execution below. A trigger naming a REPAIR that does not work is worse than one naming none, because it is satisfiable while the capability stays dead. This one names the COST SHAPE the capability requires, which is what was actually measured, and is satisfiable only by achieving it. The previously declared capability (the callee lookup answering BY INDEX rather than by scanning the candidate pool) is withdrawn because the mechanism it was derived from is refuted by execution. THE REFUTATION, BY REASONING: v2.std.fn_index.decls_in_modules is a plain-valued call with hashable arguments, and at the time of that refutation (2026-09-07) the v1 interpreter's eval-frame call memo was on by default (its GUNBC_EVAL_MEMO switch; the memo and the switch were RETIRED on 2026-09-19 by gunbc#11741 -- see RECONCILED below), keyed by fn identity x argument identity -- so the loop-invariant that trigger asked a lane to hoist was being served by the interpreter, and the per-lookup rescan named as the cost was not being paid on that head. The refutation-by-measurement (gunbc#10753) stands on its own: the index was harmful with the memo serving, and the memo's retirement does not revive the index prescription, because what the memo was serving is the authored loop-invariant the ladder prescribes SHARE for, not an index. THE REFUTATION, BY MEASUREMENT: gunbc#10753 built exactly the prescribed index and measured it against the unindexed lookup at directory grain under a verdict rule pre-registered before the numbers existed; that PR carries the method, the pre-registration and the figures, and is the citation for them rather than a copy here. Its verdict is that the index is HARMFUL -- it adds cost and removes none -- and that both arms remain far above the per-claim line, so the prescription was not merely insufficient but wrong. WHAT SURVIVES: the O(reached x pool) FIT, unchanged and still good evidence. WHAT DOES NOT: the causal sentence behind it. ATTRIBUTION SO FAR, AND THE INSTRUMENT IS NOT IN THE TREE -- THAT IS STATED FIRST BECAUSE IT IS THE FACT A READER MUST HAVE BEFORE ANY FINDING BELOW. The six-arm probe that produced these findings was written, run, and DELIBERATELY NOT LANDED, and three placements were tried and refused before that conclusion was reached (gunbc#10757). Under scratch-probe/, outside every source root, the floor refused every arm as declined_changed_witness_outside_discovery: a planned witness it cannot reach is a typed refusal, not a skip. Moved into the long home it was refused again by floor DISCOVERY, which requires a test-marked declaration to live in a *_test.dag file. Renamed to satisfy that, the arms RAN and blocked the lane sixteen ways -- interrupted before verdict, completed over the per-claim cost requirement, and changed-witness-planned-without-terminal-verdict. THE RULE THAT MAKES THIS GENERAL RATHER THAN A BAD CHOICE OF DIRECTORY: the changed-witness selector REPLACES the ordinary disposition, so a long-home decline, a fixture decline and a declared cost-debt withhold are all overridden for any claim whose FILE THE CHANGE TOUCHES. There is therefore NO location in this repository where a multi-second claim can be added, or later edited, without running on the floor of the change that touches it. An instrument of this cost cannot be a claim here at all. HOW TO RE-DERIVE THE FINDINGS: rebuild the arms locally and run them under claim_batch, which charges each arm separately -- one arm per invocation when peak RSS matters, because claim_batch reports VmHWM for the process at exit. The arms are acquisition alone; the closure list alone; the reachability walk alone; the walk plus the determinism fold; and two arms holding the entry and the CLOSURE fixed while enlarging only the candidate POOL so the reached set is unchanged. Frame structure is itself a variable, so name it whenever a ratio is quoted. THIS IS A WEAKER CITATION THAN A LANDED INSTRUMENT AND IS RECORDED AS ONE: nothing in the tree re-derives these findings, so a lane taking up the trigger rebuilds the arms before quoting anything here. That is the honest cost of the constraint above, not a preference. What it establishes: the determinism fold is NOT the cost -- adding determinism_findings over every reached declaration's whole subtree does not rise above run-to-run noise, so a lane optimising it or its concat accumulator will move nothing; and the reachability WALK is pool-sensitive at a fixed reached set, which corroborates the pool term and locates it inside the walk. WHAT REMAINS UNATTRIBUTED, AND IS NOT A SECOND TRIGGER BUT AN OPEN QUESTION UNDER THE ONE ABOVE: WHICH construct inside that walk is pool-proportional, given that the per-lookup rescan is refuted. Naming it would make the repair easier to find; it is not required to retire this row, because the trigger is stated as the shape the cost must reach and a lane that reaches it has retired this drop whether or not it can say which construct was responsible. ONE CANDIDATE WAS PROPOSED HERE AND IS NOW REFUTED BY EXECUTION, RECORDED SO THE NEXT LANE DOES NOT SPEND ITS DISPATCH RE-KILLING IT. The candidate was the eval-frame memo's own keying -- that a probe must derive a key from the pool-sized argument on every call, so removing a pool-sized scan reintroduces a pool-sized cost in the key. Its death condition was written before the arm ran: if the pool sensitivity SURVIVES with the memo off (then GUNBC_EVAL_MEMO=0; that switch is retired, and the memo-off realization is now the only one), keying is not the cost. Run the probe's a/c/e/f arms with the memo off and the sensitivity survives essentially unchanged, so the walk is pool-proportional INTRINSICALLY -- with the memo and without it -- and no repair to keying removes that term. The same arm establishes the opposite of what the candidate assumed: the memo is not a cost here but very nearly the whole performance of this walk, so any later repair in this area must PROTECT it rather than trim it. TWO MECHANISM SENTENCES HAVE NOW DIED ON THIS SUBJECT -- the candidate-pool rescan of gunbc#10744, and this one -- and the fit has survived both, which is why this row states a fit and refuses to state a cause. A third sentence does not go here until an arm supports it. WHAT IS ESTABLISHED IS NOT A MECHANISM BUT A SHAPE, AND THE SHAPE IS THE FINDING: THE WALK'S COST IS PROPORTIONAL TO THE POOL IT IS HANDED RATHER THAN TO WHAT IT REACHES. Three independent measurements, all re-derivable from the named instrument: the reached-set size is pinned EQUAL across a small pool and a pool several times larger, so reach is held constant while cost moves; the walk's cost ratio between those two pools is the same with the eval-frame memo ON as with it OFF. That third one is what makes this a shape rather than an implementation detail -- a cost that tracks the pool identically with a caching tier present and absent is not a property of that tierA CONSTRAINT THAT WAS RECORDED HERE ON 2026-09-07 AND IS WITHDRAWN, WITH THE MEASUREMENT THAT WITHDRAWS IT: the six-arm probe found that with the memo off (GUNBC_EVAL_MEMO=0 at the time) the same directory-grain arms ran roughly TWO ORDERS OF MAGNITUDE slower, and this row then instructed later lanes to PROTECT the eval-frame memo. RECONCILED 2026-09-19 (gunbc#11741, DESIGN section 6b: a contradicting result from an admitted instrument falsifies the claim, and neither arm is kept to protect the preferred explanation). That arm compared memo-on-WITH-keying against memo-off-WITH-keying: the seed's GUNBC_EVAL_MEMO=0 realization still derived a content identity for every pure call, so the arm measured the memo's SERVING minus nothing, not the memo's whole cost. What it established is that the walk carries a large authored within-frame recurrence -- decls_in_modules and its siblings demanded per lookup with equal arguments -- which the memo made cheap. std.materialization_ladder rule 1 names that recurrence AuthoredDuplication whose prescription is Share (hoist or carry the value), never Memoize, and gunbc#11741 retired the memo on that ground: a provider scoped to one shared-state frame has no admitted population. The 'protect the memo' instruction is therefore withdrawn as a violation of the ladder this repository already carries, and the recurrence it was protecting is RESTATED AS PART OF THIS ROW'S TRIGGER OBLIGATION: the walk's cost becoming proportional to what it reaches requires, among other things, that the per-lookup loop-invariant be carried rather than re-demanded, which is the same shape the withdrawn 2026-09-07 index prescription was groping for and the ladder states exactly. THE READING AT THE RETIRING HEAD, on the one surviving executing consumer (the directory-grain arms are deleted and the probe never landed): v2.test.claim.enforcement.determinism_transitive_witness determinism_live_intra_holds, eval_steps 165094 with the memo serving (base 56375ec) versus 327130 with it retired, CPU roughly 312ms versus 582ms on the session host, re-derived with claim_batch --claim-run on that function under both binaries; its grandfathered ceiling is 500ms of work at the pinned 723 steps per millisecond, 361500 steps, so the claim holds at the ceiling with the memo retired and the required floor is the standing check that it keeps doing so. That is a factor of two on the live walk, not the hundred the deleted arms showed, and the remainder of the difference is the keying the retired memo was paying on every call. A later lane that hoists the loop-invariant removes the factor of two and moves this row toward its trigger; a lane that reintroduces a within-frame memo to recover it is refused by the ladder and by gunbc.recurring_failure_mode.memo_key_rehashes_a_growing_persistent_value.oportional is what it measures as. A CONSTRAINT THAT STOOD HERE FROM 2026-09-07 AND IS WITHDRAWN (the memo-off arms at directory grain ran roughly two orders of magnitude slower, and this row told later lanes to protect the eval-frame memo); the withdrawal, its reason and the reading at the retiring head are in the RECONCILED paragraph above, stated once. WHAT THIS ROW DOES NOT CLAIM, having measured it and found otherwise: that the floor claim's own excess over the per-claim line is explained by anything above. Reproduced term by term at the floor's own grain the claim runs at well under half the line, and running it beside deliberately pool-diverse company on one machine does not move it. So the shape defect above is REAL AND IS NOT THE BLOCKER'S EXCESS, and a lane that fixes the shape should expect the intermittency to survive it. AND THE DISPOSITION THAT FOLLOWS IS NOT THE ONE A READER WILL REACH FOR. Learning that the claim's own cost is well under half the line makes a bigger line look reasonable, and it is not: a budget cannot distinguish a claim whose true cost is half the line from one measured AT the line when the environment is separately recorded as swinging by more than a factor of two on BYTE-IDENTICAL evaluator steps. That is a MEASUREMENT TRUSTWORTHINESS defect and not a THRESHOLD defect, and the repair for it is never a bigger number: a number raised to accommodate an unattributed cost stops the refusal firing without stopping the wrongness and destroys the signal that the measurement cannot be trusted, which is the escape hatch DESIGN 5 forbids. A READING, LABELLED AS ONE BECAUSE IT EXPLAINS EVERY ARM AT ONCE AND THAT IS EXACTLY WHEN TO BE CAREFUL: the eval-frame memo is evicted PER WITNESS FRAME, so diversity BETWEEN claims is cleaned up while diversity WITHIN one frame is not. That predicts all three observations without residue -- the floor claim is unmoved when run beside deliberately pool-diverse company, two walks over two pools in ONE frame cost an order of magnitude more than the same two walks in separate frames, and the floor claim is the one-frame one-pool case that never blows up. THE CONSEQUENCE A LATER LANE MUST NOT MISS: that within-frame blowup DOES NOT BEAR ON THIS BLOCKER. Whoever re-derives it will have found something real and will be tempted to call it the cause. Its payer is not retention, refuted by two independent instruments -- an arm holding the walk count fixed while varying the pools retained, and the peak-RSS column, which moves a few percent while the time moves an order of magnitude. Before those two, every arm inferred memory from time, so a timing result and a memory story could not disagree; these can, and do not. A re-deriver must also pin whether each arm re-pays its acquisition or is served from a cross-witness share, which the probe does not settle. AND A RE-DERIVER MUST NOT CARRY ANY FIGURE HERE ONTO THE MACHINE THAT BLOCKS. Every measurement behind this row was taken on remote build executors; the per-claim line is enforced on the required-lane CI runner, which is a different machine population. A distribution measured on the first says nothing about the second, and treating it as though it did is the same error as comparing an isolated figure to a CI figure -- true measurement, wrong subject. THE BLOCKER IS ACCOUNTED FOR, POSITIVELY, ON THE POPULATION WHERE THE LINE IS ENFORCED, AND IT IS NOT THIS SUBJECT. Harvest the retained required-floor claim-cost artifacts from the successful main runs, take this claim's rows, and GROUP THEM BY eval_steps so that work is held constant -- the whole point of the existing pairing authority. AND READ THE ENFORCING POPULATION FROM THE ARTIFACT RATHER THAN FROM A CLOCK: required-floor-claim-cost is published by every completed witnesses run, so this claim's cost on the population that actually enforces it is readable with no push, no lane and no window -- an earlier reading of this row treated a merge freeze as preventing measurement, which confuses producing a new head with reading a receipt from a run that already finished. PARTITION THOSE ROWS BY eval_steps AND BY NOTHING ELSE. eval_steps is deterministic work rather than a clock, so it is immune to runner variance and pool contention, it states the effect of a work-removing repair directly instead of inferring it from a noisy distribution, and it is what makes the partition AUDITABLE: a run classified as pre-repair by its id and date was found to be a post-repair sample only because its eval_steps disagreed with its neighbours. Partitioning by run id, by date or by branch silently mixes the arms and yields a smaller, believable, wrong delta. AND READ THE PRE-REPAIR ARM AS A DISTRIBUTION THAT WORSENS AS IT GROWS, which is the strongest form of the original complaint rather than a restatement of it: as the pre-repair sample grew the top of the range rose and the margin under the 500ms limit fell, with a growing minority of runs landing within 50ms of the line. A shrinking margin under a GROWING sample is not noise -- noise widens a range symmetrically around a stable centre, while this arm's maximum climbs, which is what an intermittent blocker looks like before it becomes a constant one. That is why this class was worth repairing at a realized n that looked survivable. The large majority of recent runs share one step count, and across that group -- at BYTE-IDENTICAL evaluator work, with no change to this claim and none to the tree -- the observed CPU spans a wide factor whose top reaches essentially the whole per-claim ceiling. THE FIGURES ARE NOT WRITTEN HERE ON PURPOSE, and this sentence is the instrument rather than the reading: harvest required-floor-claim-cost from the completed main runs, take this claim's COMPLETED rows, group them by eval_steps, and read the spread and the maximum of the largest group against the limit. A number copied here would be a run-local figure that nothing re-derives, which is the defect this same field names two paragraphs down. A claim whose cost distribution at fixed work already touches its own line does not need a cost defect, a drift, an accounting hole, or any mechanism to refuse intermittently. It needs only to be sampled again. THAT IS THE INTERMITTENCY, and it is why this refuses on changes that touch nothing near it. AND THE ARM IT REFUSES THROUGH IS NOT AN OVERRUN, WHICH MATTERS BECAUSE THE TWO HAVE DIFFERENT DISPOSITIONS AND ONLY ONE OF THEM BLOCKS. Harvest the RED main runs as well as the green ones and this claim's blocking row reads verdict_reached=FALSE with a right-censored cost and a LOWER eval_steps count than any completed run -- fewer steps precisely because it never finished. On red runs where it did finish it came in under budget and those runs were red for other reasons. So the failure mode is INTERRUPTED-BEFORE-VERDICT and not COMPLETED-OVER-BUDGET: the deadline preempts the witness, whether it would have passed is UNKNOWN, and the reported cost is a bound with no upper limit. That is the stronger reason such a row is inadmissible in the distribution above -- not merely that a bound cannot be divided as a cost, but that it is not a sample from that distribution AT ALL, being the cost of a computation that did not happen. AND eval_steps ON A RIGHT-CENSORED ROW IS A TRUNCATION ARTIFACT, NOT A WORKLOAD FIGURE -- one sentence here to save the next harvester an afternoon. An interrupted claim stopped wherever it had got to when the deadline fired, so its step count records how far it got and nothing else: two observed interrupts on this claim truncate at different step counts, both far below every completed run, and neither denotes a workload. The harvest above groups by eval_steps to hold work constant, which is correct ONLY over completed rows. Group the censored ones the same way and they form a third apparent level out of nothing but where the deadline landed -- a bogus population that will look exactly like the drift finding this row already withdrew once. The two arms are the same underlying fact reached differently: a claim whose completed cost distribution touches its ceiling will, on a bad draw, hit the deadline BEFORE finishing, and then it does not report a larger number, it reports no verdict. THE CONSEQUENCE FOR THE REPAIR IS THAT MARGIN IS WORTH MORE THAN IT LOOKS: an overrun is a cost debt on a claim that PASSED, while an interrupt leaves the subject UNDECIDED and is the arm that refuses. Headroom is bought against the second. AND THE REFUSAL BEHAVIOUR OF THAT ARM IS A SEPARATE FILED CLASS, cited here rather than re-derived and deliberately NOT absorbed into this row: gunbc.recurring_failure_mode.non_verdict_disposition_surfaces_as_refusal records that the floor computes the difference between THIS SUBJECT IS WRONG and I DID NOT FINISH LOOKING AT THIS SUBJECT and then discards it at the aggregate boundary, so the red check and the merge gate receive one bit whose only affordance is to run it again. Its specimen is a run refused by interrupted rows in which ZERO claims failed. That is a different defect from this one, it is what makes an interrupt here block an unrelated change, and it is that row's to repair. TWO READINGS WERE PROPOSED AND WITHDRAWN ON THE WAY TO THAT, RECORDED BECAUSE BOTH ARE TEMPTING. A drift -- the claim walking toward the line across a level change -- dissolved once the smaller step-count group was compared against the larger group's actual range rather than against its own mean: the apparent second level sits inside the first population's spread. And a small-sample variance figure understated that spread, which is what made the two groups look separated at all. One error, twice: a sample too small to see its own width. THE REFUSAL IS CORRECT AS A MEASUREMENT AND WRONG AS AN ATTRIBUTION, and the distinction decides the repair. The CPU really was consumed, so the gate is not lying; but that cost is not a property of this claim's code, so charging it to this claim attributes it wrongly. A per-claim threshold enforced on ONE DRAW from a distribution this wide is estimating a statistic it cannot see from a single sample. Raising the ceiling would silence the wrong half and destroy the evidence, which is why no number moves here. THE REPAIR IS MARGIN, AND IT IS THE POOL-PROPORTIONAL SHAPE ALREADY ESTABLISHED ABOVE -- which needs no separate justification, being a DESIGN 2 bare-minimum-cost defect that is fixed regardless of realized n. It was never the blocker and it is still the fix. AND THE ACCEPTANCE TARGET IS DERIVED FROM THE MEASUREMENT RATHER THAN GUESSED: holding the line against a spread of that width requires the MEDIAN to sit below the ceiling divided by the spread, which gives the required reduction directly -- re-derive both the median and the spread from the harvest named above and take the ratio, rather than reading a percentage here. AND THE ACCEPTANCE EVIDENCE IS A DISTRIBUTION, NEVER A GREEN RUN. A claim this near its ceiling under this spread goes green sometimes with nothing repaired, so the first green after any change carries almost no information and is exactly what will be offered as proof. What establishes a repair is a distribution at EQUAL WORK, before and after, on the enforcing population. The before is the harvest described above and it exists today. IF MARGIN CANNOT BE OBTAINED, the remaining honest arm is a further bounded drop naming the shape fix as its trigger at capability grain. Never a bigger ceiling. A RECEIPT FOR THE COST COPRODUCT, RECORDED BECAUSE IT IS A RUNG CLAIM WITH AN EXECUTION BEHIND IT RATHER THAN A DESIGN INTENTION. The observation that opened this investigation was a budget-refused reading -- a lower bound on a cost that never completed, not a cost. It was the most persuasive number available and it was on the correct population, and it is INADMISSIBLE in any ratio. gunbc.floor_cost_distribution refuses it STRUCTURALLY, because its cost reading is a coproduct and a bound has no constructor a cost fits into; no reviewer's judgement had to catch it. That class was filed after a rendered figure just over this same ceiling was read as a completed cost, and it then prevented the identical error in a later lane that knew the story and still reached for the number. AN INSTRUMENT GAP IS DECLARED HERE RATHER THAN PAPERED OVER. The ANALYSIS for the environment-variance question already exists and is not to be re-minted: gunbc.floor_cost_distribution models the cost reading as a coproduct so a censored bound cannot be divided as a cost, and identity_inflation_permille_at_equal_work pairs rows across two runs by identity AND by equal evaluator steps, which is precisely CPU divergence at byte-identical work. What does not exist is an ACTUATOR that runs one claim N times in N processes over one tree and hands the pairs to it, and the actuator that does exist runs only inside CI. So the variance figures recorded elsewhere in the seed were transcribed not because the concept lacked a home but because nothing could RE-RUN it on demand. A NEIGHBOURING CLASS THIS INVESTIGATION SURFACED, FILED IN ITS OWN ROW AND CITED HERE RATHER THAN STORED HERE: gunbc.recurring_failure_mode.inflation_fold_cannot_name_the_environment_it_measures. It is not a trigger of this drop and cannot retire it -- its subject is whether a per-claim cost MEASUREMENT can be trusted, which is a different invalid state with a different harm. It is named here for one reason only: a lane meeting THIS row's trigger must show the cost shape changed, and the evidence for that is a distribution over repeated runs, which is exactly the analysis that class governs. Read it before quoting any such distribution. A repair must be derived from measurement rather than from a plausible mechanism -- that is what the refutations below establish -- but it is the cost SHAPE that must change, not a named construct that must be found first. SUFFICIENT FOR (unchanged, and still the thing being restored): determinism_transitive_holds with pool_roots=['src/v2/lens'] and pool_files=[] reaching a verdict within the per-claim line at directory grain, WITHOUT NARROWING THE SUBJECT -- scoping pool_roots to the modules the walk happens to reach remains the trap and not the repair, because it lowers the number by shrinking the population, leaves the cost shape intact, and re-breaks the moment the subject widens, which is the widening this drop exists to restore. COST SHAPES IN THIS WALK ARE REAL AND ARE EXPLICITLY NOT THE COST, recorded so a later reader does not fix them and believe the defect is gone. THREE OF THEM ARE NOW REPAIRED and are named in the past tense because their symbols no longer resolve: call_reachable_decls_go scanned `reached` linearly per seed through a decl_in_list helper that is deleted, and now answers membership by keyed lookup over a seen map; it appended to `reached` with a copied accumulator and now conses and reverses once at the end; and list_append(rest, callee_decls) copied the worklist every step and is now guarded so an empty callee list does not copy it. REPAIRING THEM DID NOT RETIRE THIS DROP AND WAS NEVER EXPECTED TO: the pool scan in decls_matching_callee is untouched, and this row is retired by the trigger stated at the head of this field -- the cost shape -- and by nothing else. ONE SHAPE IN callees_from_node IS AN ADMITTED, UNRESOLVED OBLIGATION rather than a repair: its duplicate suppression is a linear scan of the accumulated list per callee, which is quadratic in the callees of one declaration and is subject to the same bare-minimum-cost rule. A map-keyed arm was written and measured SLOWER than the list scan at the realized callee counts and was reverted on that measurement; big-O did not grant permission to ship the slower realization, and equally the slower first attempt did not retire the defect it was aimed at. The obligation dissolves when the walk is asked at a grain whose per-declaration callee counts are large enough for the keyed arm to win, and it is recorded here rather than in the source so that it is folded with the rest of this row. THE REMAINING UNREPAIRED SHAPES: determinism_transitive_findings folds with concat(acc, determinism_findings(...)), a copied accumulator that is FREE while the corpus is clean and degrades quadratically exactly when findings appear, so it is invisible in every green run and expensive only when something is already wrong. determinism_live_closure_modules folds list_snoc_item over module_declaration_facts_live(pool_roots: []), a copied accumulator over a list that is empty today. Until the trigger stated at the head of this field is met, determinism over the fn-arrow call graph is unverified. The way out is that trigger and nothing else.", } } diff --git a/dag/gunbc/seed_growth_admission.dag b/dag/gunbc/seed_growth_admission.dag index afbf0aff384..36017452edd 100644 --- a/dag/gunbc/seed_growth_admission.dag +++ b/dag/gunbc/seed_growth_admission.dag @@ -9,6 +9,7 @@ import gunbc.persisted_resolved_graph_consumer_test_seed_growth { import gunbc.claim_scope_fixture_seed_growth { claim_scope_fixture_seed_growth_justification } import gunbc.scope_rank_view_seed_growth { scope_rank_view_seed_growth_justification } import gunbc.floor_teardown_attribution_seed_growth { floor_teardown_attribution_seed_growth_justification } +import gunbc.pure_demand_admission_seed_growth { pure_demand_admission_seed_growth_justification } import gunbc.anonymous_record_resolution_seed_growth { anonymous_record_resolution_seed_growth_justification } import gunbc.closure_edge_demand_seed_growth { closure_edge_demand_seed_growth_justification } import gunbc.reference_closure_binder_seed_growth { reference_closure_binder_seed_growth_justification } @@ -293,7 +294,8 @@ fn seed_growth_justification_roster() -> List { floor_arm_set_consumer_seed_growth_justification, scope_rank_view_seed_growth_justification, floor_teardown_attribution_seed_growth_justification, - primitive_egress_census_seed_growth_justification + primitive_egress_census_seed_growth_justification, + pure_demand_admission_seed_growth_justification ] } diff --git a/dag/test/claim/materialization_provider_witness_test.dag b/dag/test/claim/materialization_provider_witness_test.dag index a2fe0f8ed4f..be123031fb8 100644 --- a/dag/test/claim/materialization_provider_witness_test.dag +++ b/dag/test/claim/materialization_provider_witness_test.dag @@ -710,8 +710,8 @@ test fn completeness_holds_when_all_required_outputs_are_carried() -> Bool { )) } -test fn consumer_target_frontier_names_seven_caches_with_typed_binds() -> Bool { - (materialization_provider_target_count() == 7) +test fn consumer_target_frontier_names_six_caches_with_typed_binds() -> Bool { + (materialization_provider_target_count() == 6) && materialization_provider_targets_contain(id: resolved_graph_cache_id) && materialization_provider_targets_all_bound() } diff --git a/docs/design-rung-drops.md b/docs/design-rung-drops.md index 14aab04d9c6..7b56cb280d7 100644 --- a/docs/design-rung-drops.md +++ b/docs/design-rung-drops.md @@ -208,7 +208,7 @@ two passing produced-declaration emission witnesses whose charged CPU straddles ### Transitive determinism reachability over the fn-arrow call graph — declared 2026-09-05 -Transitive determinism reachability over the fn-arrow call graph: RUNG DROP, mechanically preventable -> mitigatable (deleted without replacement). Population: v2.lens.affected_set.corpus_dependency_view (fn-arrow composition, deleted), v2.lens.affected_set.entry_selection (fn-arrow declarations, deleted). Restored when: THE TRIGGER, STATED ONCE AND AT CAPABILITY GRAIN: the reachability walk's cost becomes proportional to WHAT IT REACHES rather than to the POOL IT IS HANDED, sufficient for determinism_transitive_holds to reach a verdict within the per-claim line at directory grain WITHOUT NARROWING THE SUBJECT. Nothing else retires this row. Everything after this sentence is the evidence for that trigger and the record of what was tried; none of it is a second trigger, and where a later paragraph names an obligation belonging to another subject it says so explicitly and that obligation is carried by its own row. THE TRIGGER WAS REPLACED RATHER THAN WEAKENED, 2026-09-07. It previously prescribed a specific implementation -- that the callee lookup answer BY INDEX rather than by scanning the candidate pool -- and that prescription is refuted by execution below. A trigger naming a REPAIR that does not work is worse than one naming none, because it is satisfiable while the capability stays dead. This one names the COST SHAPE the capability requires, which is what was actually measured, and is satisfiable only by achieving it. The previously declared capability (the callee lookup answering BY INDEX rather than by scanning the candidate pool) is withdrawn because the mechanism it was derived from is refuted by execution. THE REFUTATION, BY REASONING: v2.std.fn_index.decls_in_modules is a plain-valued call with hashable arguments, and the v1 interpreter's eval-frame call memo is on by default (GUNBC_EVAL_MEMO), keyed by fn identity x argument identity -- so the loop-invariant that trigger asked a lane to hoist had already been hoisted by the interpreter, and the per-lookup rescan named as the cost was not being paid. THE REFUTATION, BY MEASUREMENT: gunbc#10753 built exactly the prescribed index and measured it against the unindexed lookup at directory grain under a verdict rule pre-registered before the numbers existed; that PR carries the method, the pre-registration and the figures, and is the citation for them rather than a copy here. Its verdict is that the index is HARMFUL -- it adds cost and removes none -- and that both arms remain far above the per-claim line, so the prescription was not merely insufficient but wrong. WHAT SURVIVES: the O(reached x pool) FIT, unchanged and still good evidence. WHAT DOES NOT: the causal sentence behind it. ATTRIBUTION SO FAR, AND THE INSTRUMENT IS NOT IN THE TREE -- THAT IS STATED FIRST BECAUSE IT IS THE FACT A READER MUST HAVE BEFORE ANY FINDING BELOW. The six-arm probe that produced these findings was written, run, and DELIBERATELY NOT LANDED, and three placements were tried and refused before that conclusion was reached (gunbc#10757). Under scratch-probe/, outside every source root, the floor refused every arm as declined_changed_witness_outside_discovery: a planned witness it cannot reach is a typed refusal, not a skip. Moved into the long home it was refused again by floor DISCOVERY, which requires a test-marked declaration to live in a *_test.dag file. Renamed to satisfy that, the arms RAN and blocked the lane sixteen ways -- interrupted before verdict, completed over the per-claim cost requirement, and changed-witness-planned-without-terminal-verdict. THE RULE THAT MAKES THIS GENERAL RATHER THAN A BAD CHOICE OF DIRECTORY: the changed-witness selector REPLACES the ordinary disposition, so a long-home decline, a fixture decline and a declared cost-debt withhold are all overridden for any claim whose FILE THE CHANGE TOUCHES. There is therefore NO location in this repository where a multi-second claim can be added, or later edited, without running on the floor of the change that touches it. An instrument of this cost cannot be a claim here at all. HOW TO RE-DERIVE THE FINDINGS: rebuild the arms locally and run them under claim_batch, which charges each arm separately -- one arm per invocation when peak RSS matters, because claim_batch reports VmHWM for the process at exit. The arms are acquisition alone; the closure list alone; the reachability walk alone; the walk plus the determinism fold; and two arms holding the entry and the CLOSURE fixed while enlarging only the candidate POOL so the reached set is unchanged. Frame structure is itself a variable, so name it whenever a ratio is quoted. THIS IS A WEAKER CITATION THAN A LANDED INSTRUMENT AND IS RECORDED AS ONE: nothing in the tree re-derives these findings, so a lane taking up the trigger rebuilds the arms before quoting anything here. That is the honest cost of the constraint above, not a preference. What it establishes: the determinism fold is NOT the cost -- adding determinism_findings over every reached declaration's whole subtree does not rise above run-to-run noise, so a lane optimising it or its concat accumulator will move nothing; and the reachability WALK is pool-sensitive at a fixed reached set, which corroborates the pool term and locates it inside the walk. WHAT REMAINS UNATTRIBUTED, AND IS NOT A SECOND TRIGGER BUT AN OPEN QUESTION UNDER THE ONE ABOVE: WHICH construct inside that walk is pool-proportional, given that the per-lookup rescan is refuted. Naming it would make the repair easier to find; it is not required to retire this row, because the trigger is stated as the shape the cost must reach and a lane that reaches it has retired this drop whether or not it can say which construct was responsible. ONE CANDIDATE WAS PROPOSED HERE AND IS NOW REFUTED BY EXECUTION, RECORDED SO THE NEXT LANE DOES NOT SPEND ITS DISPATCH RE-KILLING IT. The candidate was the eval-frame memo's own keying -- that a probe must derive a key from the pool-sized argument on every call, so removing a pool-sized scan reintroduces a pool-sized cost in the key. Its death condition was written before the arm ran: if the pool sensitivity SURVIVES with GUNBC_EVAL_MEMO=0, keying is not the cost. Run the probe's a/c/e/f arms with the memo off and the sensitivity survives essentially unchanged, so the walk is pool-proportional INTRINSICALLY -- with the memo and without it -- and no repair to keying removes that term. The same arm establishes the opposite of what the candidate assumed: the memo is not a cost here but very nearly the whole performance of this walk, so any later repair in this area must PROTECT it rather than trim it. TWO MECHANISM SENTENCES HAVE NOW DIED ON THIS SUBJECT -- the candidate-pool rescan of gunbc#10744, and this one -- and the fit has survived both, which is why this row states a fit and refuses to state a cause. A third sentence does not go here until an arm supports it. WHAT IS ESTABLISHED IS NOT A MECHANISM BUT A SHAPE, AND THE SHAPE IS THE FINDING: THE WALK'S COST IS PROPORTIONAL TO THE POOL IT IS HANDED RATHER THAN TO WHAT IT REACHES. Three independent measurements, all re-derivable from the named instrument: the reached-set size is pinned EQUAL across a small pool and a pool several times larger, so reach is held constant while cost moves; the walk's cost ratio between those two pools is the same with the eval-frame memo ON as with it OFF. That third one is what makes this a shape rather than an implementation detail -- a cost that tracks the pool identically with a caching tier present and absent is not a property of that tier, of any key, or of any index, but of the WALK, and it is INVARIANT UNDER EVERY MECHANISM PROPOSED AND REFUTED HERE. That invariance is why this row states it as established while stating no cause. A measured cost-shape defect with no carrier is how a defect becomes ownerless, and DESIGN 2's bare-minimum-cost rule prices a PROVEN cost-shape defect as always worth fixing regardless of realized n, without waiting for the cause to be named. Reach-proportional is what this walk should be; pool-proportional is what it measures as. A CONSTRAINT ON ANY FUTURE REPAIR, MEASURED AND RECORDED HERE BECAUSE THE NEXT LANE WILL NOT EXPECT IT: with GUNBC_EVAL_MEMO=0 the same arms run roughly TWO ORDERS OF MAGNITUDE slower. The eval-frame memo is not a cost on this path, it is very nearly the whole performance of it. A later simplification that bypasses or replaces the memo -- which will look clean, because the memo is invisible in the .dag source -- makes this walk about a hundred times slower. Protect it; do not route around it. WHAT THIS ROW DOES NOT CLAIM, having measured it and found otherwise: that the floor claim's own excess over the per-claim line is explained by anything above. Reproduced term by term at the floor's own grain the claim runs at well under half the line, and running it beside deliberately pool-diverse company on one machine does not move it. So the shape defect above is REAL AND IS NOT THE BLOCKER'S EXCESS, and a lane that fixes the shape should expect the intermittency to survive it. AND THE DISPOSITION THAT FOLLOWS IS NOT THE ONE A READER WILL REACH FOR. Learning that the claim's own cost is well under half the line makes a bigger line look reasonable, and it is not: a budget cannot distinguish a claim whose true cost is half the line from one measured AT the line when the environment is separately recorded as swinging by more than a factor of two on BYTE-IDENTICAL evaluator steps. That is a MEASUREMENT TRUSTWORTHINESS defect and not a THRESHOLD defect, and the repair for it is never a bigger number: a number raised to accommodate an unattributed cost stops the refusal firing without stopping the wrongness and destroys the signal that the measurement cannot be trusted, which is the escape hatch DESIGN 5 forbids. A READING, LABELLED AS ONE BECAUSE IT EXPLAINS EVERY ARM AT ONCE AND THAT IS EXACTLY WHEN TO BE CAREFUL: the eval-frame memo is evicted PER WITNESS FRAME, so diversity BETWEEN claims is cleaned up while diversity WITHIN one frame is not. That predicts all three observations without residue -- the floor claim is unmoved when run beside deliberately pool-diverse company, two walks over two pools in ONE frame cost an order of magnitude more than the same two walks in separate frames, and the floor claim is the one-frame one-pool case that never blows up. THE CONSEQUENCE A LATER LANE MUST NOT MISS: that within-frame blowup DOES NOT BEAR ON THIS BLOCKER. Whoever re-derives it will have found something real and will be tempted to call it the cause. Its payer is not retention, refuted by two independent instruments -- an arm holding the walk count fixed while varying the pools retained, and the peak-RSS column, which moves a few percent while the time moves an order of magnitude. Before those two, every arm inferred memory from time, so a timing result and a memory story could not disagree; these can, and do not. A re-deriver must also pin whether each arm re-pays its acquisition or is served from a cross-witness share, which the probe does not settle. AND A RE-DERIVER MUST NOT CARRY ANY FIGURE HERE ONTO THE MACHINE THAT BLOCKS. Every measurement behind this row was taken on remote build executors; the per-claim line is enforced on the required-lane CI runner, which is a different machine population. A distribution measured on the first says nothing about the second, and treating it as though it did is the same error as comparing an isolated figure to a CI figure -- true measurement, wrong subject. THE BLOCKER IS ACCOUNTED FOR, POSITIVELY, ON THE POPULATION WHERE THE LINE IS ENFORCED, AND IT IS NOT THIS SUBJECT. Harvest the retained required-floor claim-cost artifacts from the successful main runs, take this claim's rows, and GROUP THEM BY eval_steps so that work is held constant -- the whole point of the existing pairing authority. AND READ THE ENFORCING POPULATION FROM THE ARTIFACT RATHER THAN FROM A CLOCK: required-floor-claim-cost is published by every completed witnesses run, so this claim's cost on the population that actually enforces it is readable with no push, no lane and no window -- an earlier reading of this row treated a merge freeze as preventing measurement, which confuses producing a new head with reading a receipt from a run that already finished. PARTITION THOSE ROWS BY eval_steps AND BY NOTHING ELSE. eval_steps is deterministic work rather than a clock, so it is immune to runner variance and pool contention, it states the effect of a work-removing repair directly instead of inferring it from a noisy distribution, and it is what makes the partition AUDITABLE: a run classified as pre-repair by its id and date was found to be a post-repair sample only because its eval_steps disagreed with its neighbours. Partitioning by run id, by date or by branch silently mixes the arms and yields a smaller, believable, wrong delta. AND READ THE PRE-REPAIR ARM AS A DISTRIBUTION THAT WORSENS AS IT GROWS, which is the strongest form of the original complaint rather than a restatement of it: as the pre-repair sample grew the top of the range rose and the margin under the 500ms limit fell, with a growing minority of runs landing within 50ms of the line. A shrinking margin under a GROWING sample is not noise -- noise widens a range symmetrically around a stable centre, while this arm's maximum climbs, which is what an intermittent blocker looks like before it becomes a constant one. That is why this class was worth repairing at a realized n that looked survivable. The large majority of recent runs share one step count, and across that group -- at BYTE-IDENTICAL evaluator work, with no change to this claim and none to the tree -- the observed CPU spans a wide factor whose top reaches essentially the whole per-claim ceiling. THE FIGURES ARE NOT WRITTEN HERE ON PURPOSE, and this sentence is the instrument rather than the reading: harvest required-floor-claim-cost from the completed main runs, take this claim's COMPLETED rows, group them by eval_steps, and read the spread and the maximum of the largest group against the limit. A number copied here would be a run-local figure that nothing re-derives, which is the defect this same field names two paragraphs down. A claim whose cost distribution at fixed work already touches its own line does not need a cost defect, a drift, an accounting hole, or any mechanism to refuse intermittently. It needs only to be sampled again. THAT IS THE INTERMITTENCY, and it is why this refuses on changes that touch nothing near it. AND THE ARM IT REFUSES THROUGH IS NOT AN OVERRUN, WHICH MATTERS BECAUSE THE TWO HAVE DIFFERENT DISPOSITIONS AND ONLY ONE OF THEM BLOCKS. Harvest the RED main runs as well as the green ones and this claim's blocking row reads verdict_reached=FALSE with a right-censored cost and a LOWER eval_steps count than any completed run -- fewer steps precisely because it never finished. On red runs where it did finish it came in under budget and those runs were red for other reasons. So the failure mode is INTERRUPTED-BEFORE-VERDICT and not COMPLETED-OVER-BUDGET: the deadline preempts the witness, whether it would have passed is UNKNOWN, and the reported cost is a bound with no upper limit. That is the stronger reason such a row is inadmissible in the distribution above -- not merely that a bound cannot be divided as a cost, but that it is not a sample from that distribution AT ALL, being the cost of a computation that did not happen. AND eval_steps ON A RIGHT-CENSORED ROW IS A TRUNCATION ARTIFACT, NOT A WORKLOAD FIGURE -- one sentence here to save the next harvester an afternoon. An interrupted claim stopped wherever it had got to when the deadline fired, so its step count records how far it got and nothing else: two observed interrupts on this claim truncate at different step counts, both far below every completed run, and neither denotes a workload. The harvest above groups by eval_steps to hold work constant, which is correct ONLY over completed rows. Group the censored ones the same way and they form a third apparent level out of nothing but where the deadline landed -- a bogus population that will look exactly like the drift finding this row already withdrew once. The two arms are the same underlying fact reached differently: a claim whose completed cost distribution touches its ceiling will, on a bad draw, hit the deadline BEFORE finishing, and then it does not report a larger number, it reports no verdict. THE CONSEQUENCE FOR THE REPAIR IS THAT MARGIN IS WORTH MORE THAN IT LOOKS: an overrun is a cost debt on a claim that PASSED, while an interrupt leaves the subject UNDECIDED and is the arm that refuses. Headroom is bought against the second. AND THE REFUSAL BEHAVIOUR OF THAT ARM IS A SEPARATE FILED CLASS, cited here rather than re-derived and deliberately NOT absorbed into this row: gunbc.recurring_failure_mode.non_verdict_disposition_surfaces_as_refusal records that the floor computes the difference between THIS SUBJECT IS WRONG and I DID NOT FINISH LOOKING AT THIS SUBJECT and then discards it at the aggregate boundary, so the red check and the merge gate receive one bit whose only affordance is to run it again. Its specimen is a run refused by interrupted rows in which ZERO claims failed. That is a different defect from this one, it is what makes an interrupt here block an unrelated change, and it is that row's to repair. TWO READINGS WERE PROPOSED AND WITHDRAWN ON THE WAY TO THAT, RECORDED BECAUSE BOTH ARE TEMPTING. A drift -- the claim walking toward the line across a level change -- dissolved once the smaller step-count group was compared against the larger group's actual range rather than against its own mean: the apparent second level sits inside the first population's spread. And a small-sample variance figure understated that spread, which is what made the two groups look separated at all. One error, twice: a sample too small to see its own width. THE REFUSAL IS CORRECT AS A MEASUREMENT AND WRONG AS AN ATTRIBUTION, and the distinction decides the repair. The CPU really was consumed, so the gate is not lying; but that cost is not a property of this claim's code, so charging it to this claim attributes it wrongly. A per-claim threshold enforced on ONE DRAW from a distribution this wide is estimating a statistic it cannot see from a single sample. Raising the ceiling would silence the wrong half and destroy the evidence, which is why no number moves here. THE REPAIR IS MARGIN, AND IT IS THE POOL-PROPORTIONAL SHAPE ALREADY ESTABLISHED ABOVE -- which needs no separate justification, being a DESIGN 2 bare-minimum-cost defect that is fixed regardless of realized n. It was never the blocker and it is still the fix. AND THE ACCEPTANCE TARGET IS DERIVED FROM THE MEASUREMENT RATHER THAN GUESSED: holding the line against a spread of that width requires the MEDIAN to sit below the ceiling divided by the spread, which gives the required reduction directly -- re-derive both the median and the spread from the harvest named above and take the ratio, rather than reading a percentage here. AND THE ACCEPTANCE EVIDENCE IS A DISTRIBUTION, NEVER A GREEN RUN. A claim this near its ceiling under this spread goes green sometimes with nothing repaired, so the first green after any change carries almost no information and is exactly what will be offered as proof. What establishes a repair is a distribution at EQUAL WORK, before and after, on the enforcing population. The before is the harvest described above and it exists today. IF MARGIN CANNOT BE OBTAINED, the remaining honest arm is a further bounded drop naming the shape fix as its trigger at capability grain. Never a bigger ceiling. A RECEIPT FOR THE COST COPRODUCT, RECORDED BECAUSE IT IS A RUNG CLAIM WITH AN EXECUTION BEHIND IT RATHER THAN A DESIGN INTENTION. The observation that opened this investigation was a budget-refused reading -- a lower bound on a cost that never completed, not a cost. It was the most persuasive number available and it was on the correct population, and it is INADMISSIBLE in any ratio. gunbc.floor_cost_distribution refuses it STRUCTURALLY, because its cost reading is a coproduct and a bound has no constructor a cost fits into; no reviewer's judgement had to catch it. That class was filed after a rendered figure just over this same ceiling was read as a completed cost, and it then prevented the identical error in a later lane that knew the story and still reached for the number. AN INSTRUMENT GAP IS DECLARED HERE RATHER THAN PAPERED OVER. The ANALYSIS for the environment-variance question already exists and is not to be re-minted: gunbc.floor_cost_distribution models the cost reading as a coproduct so a censored bound cannot be divided as a cost, and identity_inflation_permille_at_equal_work pairs rows across two runs by identity AND by equal evaluator steps, which is precisely CPU divergence at byte-identical work. What does not exist is an ACTUATOR that runs one claim N times in N processes over one tree and hands the pairs to it, and the actuator that does exist runs only inside CI. So the variance figures recorded elsewhere in the seed were transcribed not because the concept lacked a home but because nothing could RE-RUN it on demand. A NEIGHBOURING CLASS THIS INVESTIGATION SURFACED, FILED IN ITS OWN ROW AND CITED HERE RATHER THAN STORED HERE: gunbc.recurring_failure_mode.inflation_fold_cannot_name_the_environment_it_measures. It is not a trigger of this drop and cannot retire it -- its subject is whether a per-claim cost MEASUREMENT can be trusted, which is a different invalid state with a different harm. It is named here for one reason only: a lane meeting THIS row's trigger must show the cost shape changed, and the evidence for that is a distribution over repeated runs, which is exactly the analysis that class governs. Read it before quoting any such distribution. A repair must be derived from measurement rather than from a plausible mechanism -- that is what the refutations below establish -- but it is the cost SHAPE that must change, not a named construct that must be found first. SUFFICIENT FOR (unchanged, and still the thing being restored): determinism_transitive_holds with pool_roots=['src/v2/lens'] and pool_files=[] reaching a verdict within the per-claim line at directory grain, WITHOUT NARROWING THE SUBJECT -- scoping pool_roots to the modules the walk happens to reach remains the trap and not the repair, because it lowers the number by shrinking the population, leaves the cost shape intact, and re-breaks the moment the subject widens, which is the widening this drop exists to restore. COST SHAPES IN THIS WALK ARE REAL AND ARE EXPLICITLY NOT THE COST, recorded so a later reader does not fix them and believe the defect is gone. THREE OF THEM ARE NOW REPAIRED and are named in the past tense because their symbols no longer resolve: call_reachable_decls_go scanned `reached` linearly per seed through a decl_in_list helper that is deleted, and now answers membership by keyed lookup over a seen map; it appended to `reached` with a copied accumulator and now conses and reverses once at the end; and list_append(rest, callee_decls) copied the worklist every step and is now guarded so an empty callee list does not copy it. REPAIRING THEM DID NOT RETIRE THIS DROP AND WAS NEVER EXPECTED TO: the pool scan in decls_matching_callee is untouched, and this row is retired by the trigger stated at the head of this field -- the cost shape -- and by nothing else. ONE SHAPE IN callees_from_node IS AN ADMITTED, UNRESOLVED OBLIGATION rather than a repair: its duplicate suppression is a linear scan of the accumulated list per callee, which is quadratic in the callees of one declaration and is subject to the same bare-minimum-cost rule. A map-keyed arm was written and measured SLOWER than the list scan at the realized callee counts and was reverted on that measurement; big-O did not grant permission to ship the slower realization, and equally the slower first attempt did not retire the defect it was aimed at. The obligation dissolves when the walk is asked at a grain whose per-declaration callee counts are large enough for the keyed arm to win, and it is recorded here rather than in the source so that it is folded with the rest of this row. THE REMAINING UNREPAIRED SHAPES: determinism_transitive_findings folds with concat(acc, determinism_findings(...)), a copied accumulator that is FREE while the corpus is clean and degrades quadratically exactly when findings appear, so it is invisible in every green run and expensive only when something is already wrong. determinism_live_closure_modules folds list_snoc_item over module_declaration_facts_live(pool_roots: []), a copied accumulator over a list that is empty today. Until the trigger stated at the head of this field is met, determinism over the fn-arrow call graph is unverified. The way out is that trigger and nothing else. +Transitive determinism reachability over the fn-arrow call graph: RUNG DROP, mechanically preventable -> mitigatable (deleted without replacement). Population: v2.lens.affected_set.corpus_dependency_view (fn-arrow composition, deleted), v2.lens.affected_set.entry_selection (fn-arrow declarations, deleted). Restored when: THE TRIGGER, STATED ONCE AND AT CAPABILITY GRAIN: the reachability walk's cost becomes proportional to WHAT IT REACHES rather than to the POOL IT IS HANDED, sufficient for determinism_transitive_holds to reach a verdict within the per-claim line at directory grain WITHOUT NARROWING THE SUBJECT. Nothing else retires this row. Everything after this sentence is the evidence for that trigger and the record of what was tried; none of it is a second trigger, and where a later paragraph names an obligation belonging to another subject it says so explicitly and that obligation is carried by its own row. THE TRIGGER WAS REPLACED RATHER THAN WEAKENED, 2026-09-07. It previously prescribed a specific implementation -- that the callee lookup answer BY INDEX rather than by scanning the candidate pool -- and that prescription is refuted by execution below. A trigger naming a REPAIR that does not work is worse than one naming none, because it is satisfiable while the capability stays dead. This one names the COST SHAPE the capability requires, which is what was actually measured, and is satisfiable only by achieving it. The previously declared capability (the callee lookup answering BY INDEX rather than by scanning the candidate pool) is withdrawn because the mechanism it was derived from is refuted by execution. THE REFUTATION, BY REASONING: v2.std.fn_index.decls_in_modules is a plain-valued call with hashable arguments, and at the time of that refutation (2026-09-07) the v1 interpreter's eval-frame call memo was on by default (its GUNBC_EVAL_MEMO switch; the memo and the switch were RETIRED on 2026-09-19 by gunbc#11741 -- see RECONCILED below), keyed by fn identity x argument identity -- so the loop-invariant that trigger asked a lane to hoist was being served by the interpreter, and the per-lookup rescan named as the cost was not being paid on that head. The refutation-by-measurement (gunbc#10753) stands on its own: the index was harmful with the memo serving, and the memo's retirement does not revive the index prescription, because what the memo was serving is the authored loop-invariant the ladder prescribes SHARE for, not an index. THE REFUTATION, BY MEASUREMENT: gunbc#10753 built exactly the prescribed index and measured it against the unindexed lookup at directory grain under a verdict rule pre-registered before the numbers existed; that PR carries the method, the pre-registration and the figures, and is the citation for them rather than a copy here. Its verdict is that the index is HARMFUL -- it adds cost and removes none -- and that both arms remain far above the per-claim line, so the prescription was not merely insufficient but wrong. WHAT SURVIVES: the O(reached x pool) FIT, unchanged and still good evidence. WHAT DOES NOT: the causal sentence behind it. ATTRIBUTION SO FAR, AND THE INSTRUMENT IS NOT IN THE TREE -- THAT IS STATED FIRST BECAUSE IT IS THE FACT A READER MUST HAVE BEFORE ANY FINDING BELOW. The six-arm probe that produced these findings was written, run, and DELIBERATELY NOT LANDED, and three placements were tried and refused before that conclusion was reached (gunbc#10757). Under scratch-probe/, outside every source root, the floor refused every arm as declined_changed_witness_outside_discovery: a planned witness it cannot reach is a typed refusal, not a skip. Moved into the long home it was refused again by floor DISCOVERY, which requires a test-marked declaration to live in a *_test.dag file. Renamed to satisfy that, the arms RAN and blocked the lane sixteen ways -- interrupted before verdict, completed over the per-claim cost requirement, and changed-witness-planned-without-terminal-verdict. THE RULE THAT MAKES THIS GENERAL RATHER THAN A BAD CHOICE OF DIRECTORY: the changed-witness selector REPLACES the ordinary disposition, so a long-home decline, a fixture decline and a declared cost-debt withhold are all overridden for any claim whose FILE THE CHANGE TOUCHES. There is therefore NO location in this repository where a multi-second claim can be added, or later edited, without running on the floor of the change that touches it. An instrument of this cost cannot be a claim here at all. HOW TO RE-DERIVE THE FINDINGS: rebuild the arms locally and run them under claim_batch, which charges each arm separately -- one arm per invocation when peak RSS matters, because claim_batch reports VmHWM for the process at exit. The arms are acquisition alone; the closure list alone; the reachability walk alone; the walk plus the determinism fold; and two arms holding the entry and the CLOSURE fixed while enlarging only the candidate POOL so the reached set is unchanged. Frame structure is itself a variable, so name it whenever a ratio is quoted. THIS IS A WEAKER CITATION THAN A LANDED INSTRUMENT AND IS RECORDED AS ONE: nothing in the tree re-derives these findings, so a lane taking up the trigger rebuilds the arms before quoting anything here. That is the honest cost of the constraint above, not a preference. What it establishes: the determinism fold is NOT the cost -- adding determinism_findings over every reached declaration's whole subtree does not rise above run-to-run noise, so a lane optimising it or its concat accumulator will move nothing; and the reachability WALK is pool-sensitive at a fixed reached set, which corroborates the pool term and locates it inside the walk. WHAT REMAINS UNATTRIBUTED, AND IS NOT A SECOND TRIGGER BUT AN OPEN QUESTION UNDER THE ONE ABOVE: WHICH construct inside that walk is pool-proportional, given that the per-lookup rescan is refuted. Naming it would make the repair easier to find; it is not required to retire this row, because the trigger is stated as the shape the cost must reach and a lane that reaches it has retired this drop whether or not it can say which construct was responsible. ONE CANDIDATE WAS PROPOSED HERE AND IS NOW REFUTED BY EXECUTION, RECORDED SO THE NEXT LANE DOES NOT SPEND ITS DISPATCH RE-KILLING IT. The candidate was the eval-frame memo's own keying -- that a probe must derive a key from the pool-sized argument on every call, so removing a pool-sized scan reintroduces a pool-sized cost in the key. Its death condition was written before the arm ran: if the pool sensitivity SURVIVES with the memo off (then GUNBC_EVAL_MEMO=0; that switch is retired, and the memo-off realization is now the only one), keying is not the cost. Run the probe's a/c/e/f arms with the memo off and the sensitivity survives essentially unchanged, so the walk is pool-proportional INTRINSICALLY -- with the memo and without it -- and no repair to keying removes that term. The same arm establishes the opposite of what the candidate assumed: the memo is not a cost here but very nearly the whole performance of this walk, so any later repair in this area must PROTECT it rather than trim it. TWO MECHANISM SENTENCES HAVE NOW DIED ON THIS SUBJECT -- the candidate-pool rescan of gunbc#10744, and this one -- and the fit has survived both, which is why this row states a fit and refuses to state a cause. A third sentence does not go here until an arm supports it. WHAT IS ESTABLISHED IS NOT A MECHANISM BUT A SHAPE, AND THE SHAPE IS THE FINDING: THE WALK'S COST IS PROPORTIONAL TO THE POOL IT IS HANDED RATHER THAN TO WHAT IT REACHES. Three independent measurements, all re-derivable from the named instrument: the reached-set size is pinned EQUAL across a small pool and a pool several times larger, so reach is held constant while cost moves; the walk's cost ratio between those two pools is the same with the eval-frame memo ON as with it OFF. That third one is what makes this a shape rather than an implementation detail -- a cost that tracks the pool identically with a caching tier present and absent is not a property of that tierA CONSTRAINT THAT WAS RECORDED HERE ON 2026-09-07 AND IS WITHDRAWN, WITH THE MEASUREMENT THAT WITHDRAWS IT: the six-arm probe found that with the memo off (GUNBC_EVAL_MEMO=0 at the time) the same directory-grain arms ran roughly TWO ORDERS OF MAGNITUDE slower, and this row then instructed later lanes to PROTECT the eval-frame memo. RECONCILED 2026-09-19 (gunbc#11741, DESIGN section 6b: a contradicting result from an admitted instrument falsifies the claim, and neither arm is kept to protect the preferred explanation). That arm compared memo-on-WITH-keying against memo-off-WITH-keying: the seed's GUNBC_EVAL_MEMO=0 realization still derived a content identity for every pure call, so the arm measured the memo's SERVING minus nothing, not the memo's whole cost. What it established is that the walk carries a large authored within-frame recurrence -- decls_in_modules and its siblings demanded per lookup with equal arguments -- which the memo made cheap. std.materialization_ladder rule 1 names that recurrence AuthoredDuplication whose prescription is Share (hoist or carry the value), never Memoize, and gunbc#11741 retired the memo on that ground: a provider scoped to one shared-state frame has no admitted population. The 'protect the memo' instruction is therefore withdrawn as a violation of the ladder this repository already carries, and the recurrence it was protecting is RESTATED AS PART OF THIS ROW'S TRIGGER OBLIGATION: the walk's cost becoming proportional to what it reaches requires, among other things, that the per-lookup loop-invariant be carried rather than re-demanded, which is the same shape the withdrawn 2026-09-07 index prescription was groping for and the ladder states exactly. THE READING AT THE RETIRING HEAD, on the one surviving executing consumer (the directory-grain arms are deleted and the probe never landed): v2.test.claim.enforcement.determinism_transitive_witness determinism_live_intra_holds, eval_steps 165094 with the memo serving (base 56375ec) versus 327130 with it retired, CPU roughly 312ms versus 582ms on the session host, re-derived with claim_batch --claim-run on that function under both binaries; its grandfathered ceiling is 500ms of work at the pinned 723 steps per millisecond, 361500 steps, so the claim holds at the ceiling with the memo retired and the required floor is the standing check that it keeps doing so. That is a factor of two on the live walk, not the hundred the deleted arms showed, and the remainder of the difference is the keying the retired memo was paying on every call. A later lane that hoists the loop-invariant removes the factor of two and moves this row toward its trigger; a lane that reintroduces a within-frame memo to recover it is refused by the ladder and by gunbc.recurring_failure_mode.memo_key_rehashes_a_growing_persistent_value.oportional is what it measures as. A CONSTRAINT THAT STOOD HERE FROM 2026-09-07 AND IS WITHDRAWN (the memo-off arms at directory grain ran roughly two orders of magnitude slower, and this row told later lanes to protect the eval-frame memo); the withdrawal, its reason and the reading at the retiring head are in the RECONCILED paragraph above, stated once. WHAT THIS ROW DOES NOT CLAIM, having measured it and found otherwise: that the floor claim's own excess over the per-claim line is explained by anything above. Reproduced term by term at the floor's own grain the claim runs at well under half the line, and running it beside deliberately pool-diverse company on one machine does not move it. So the shape defect above is REAL AND IS NOT THE BLOCKER'S EXCESS, and a lane that fixes the shape should expect the intermittency to survive it. AND THE DISPOSITION THAT FOLLOWS IS NOT THE ONE A READER WILL REACH FOR. Learning that the claim's own cost is well under half the line makes a bigger line look reasonable, and it is not: a budget cannot distinguish a claim whose true cost is half the line from one measured AT the line when the environment is separately recorded as swinging by more than a factor of two on BYTE-IDENTICAL evaluator steps. That is a MEASUREMENT TRUSTWORTHINESS defect and not a THRESHOLD defect, and the repair for it is never a bigger number: a number raised to accommodate an unattributed cost stops the refusal firing without stopping the wrongness and destroys the signal that the measurement cannot be trusted, which is the escape hatch DESIGN 5 forbids. A READING, LABELLED AS ONE BECAUSE IT EXPLAINS EVERY ARM AT ONCE AND THAT IS EXACTLY WHEN TO BE CAREFUL: the eval-frame memo is evicted PER WITNESS FRAME, so diversity BETWEEN claims is cleaned up while diversity WITHIN one frame is not. That predicts all three observations without residue -- the floor claim is unmoved when run beside deliberately pool-diverse company, two walks over two pools in ONE frame cost an order of magnitude more than the same two walks in separate frames, and the floor claim is the one-frame one-pool case that never blows up. THE CONSEQUENCE A LATER LANE MUST NOT MISS: that within-frame blowup DOES NOT BEAR ON THIS BLOCKER. Whoever re-derives it will have found something real and will be tempted to call it the cause. Its payer is not retention, refuted by two independent instruments -- an arm holding the walk count fixed while varying the pools retained, and the peak-RSS column, which moves a few percent while the time moves an order of magnitude. Before those two, every arm inferred memory from time, so a timing result and a memory story could not disagree; these can, and do not. A re-deriver must also pin whether each arm re-pays its acquisition or is served from a cross-witness share, which the probe does not settle. AND A RE-DERIVER MUST NOT CARRY ANY FIGURE HERE ONTO THE MACHINE THAT BLOCKS. Every measurement behind this row was taken on remote build executors; the per-claim line is enforced on the required-lane CI runner, which is a different machine population. A distribution measured on the first says nothing about the second, and treating it as though it did is the same error as comparing an isolated figure to a CI figure -- true measurement, wrong subject. THE BLOCKER IS ACCOUNTED FOR, POSITIVELY, ON THE POPULATION WHERE THE LINE IS ENFORCED, AND IT IS NOT THIS SUBJECT. Harvest the retained required-floor claim-cost artifacts from the successful main runs, take this claim's rows, and GROUP THEM BY eval_steps so that work is held constant -- the whole point of the existing pairing authority. AND READ THE ENFORCING POPULATION FROM THE ARTIFACT RATHER THAN FROM A CLOCK: required-floor-claim-cost is published by every completed witnesses run, so this claim's cost on the population that actually enforces it is readable with no push, no lane and no window -- an earlier reading of this row treated a merge freeze as preventing measurement, which confuses producing a new head with reading a receipt from a run that already finished. PARTITION THOSE ROWS BY eval_steps AND BY NOTHING ELSE. eval_steps is deterministic work rather than a clock, so it is immune to runner variance and pool contention, it states the effect of a work-removing repair directly instead of inferring it from a noisy distribution, and it is what makes the partition AUDITABLE: a run classified as pre-repair by its id and date was found to be a post-repair sample only because its eval_steps disagreed with its neighbours. Partitioning by run id, by date or by branch silently mixes the arms and yields a smaller, believable, wrong delta. AND READ THE PRE-REPAIR ARM AS A DISTRIBUTION THAT WORSENS AS IT GROWS, which is the strongest form of the original complaint rather than a restatement of it: as the pre-repair sample grew the top of the range rose and the margin under the 500ms limit fell, with a growing minority of runs landing within 50ms of the line. A shrinking margin under a GROWING sample is not noise -- noise widens a range symmetrically around a stable centre, while this arm's maximum climbs, which is what an intermittent blocker looks like before it becomes a constant one. That is why this class was worth repairing at a realized n that looked survivable. The large majority of recent runs share one step count, and across that group -- at BYTE-IDENTICAL evaluator work, with no change to this claim and none to the tree -- the observed CPU spans a wide factor whose top reaches essentially the whole per-claim ceiling. THE FIGURES ARE NOT WRITTEN HERE ON PURPOSE, and this sentence is the instrument rather than the reading: harvest required-floor-claim-cost from the completed main runs, take this claim's COMPLETED rows, group them by eval_steps, and read the spread and the maximum of the largest group against the limit. A number copied here would be a run-local figure that nothing re-derives, which is the defect this same field names two paragraphs down. A claim whose cost distribution at fixed work already touches its own line does not need a cost defect, a drift, an accounting hole, or any mechanism to refuse intermittently. It needs only to be sampled again. THAT IS THE INTERMITTENCY, and it is why this refuses on changes that touch nothing near it. AND THE ARM IT REFUSES THROUGH IS NOT AN OVERRUN, WHICH MATTERS BECAUSE THE TWO HAVE DIFFERENT DISPOSITIONS AND ONLY ONE OF THEM BLOCKS. Harvest the RED main runs as well as the green ones and this claim's blocking row reads verdict_reached=FALSE with a right-censored cost and a LOWER eval_steps count than any completed run -- fewer steps precisely because it never finished. On red runs where it did finish it came in under budget and those runs were red for other reasons. So the failure mode is INTERRUPTED-BEFORE-VERDICT and not COMPLETED-OVER-BUDGET: the deadline preempts the witness, whether it would have passed is UNKNOWN, and the reported cost is a bound with no upper limit. That is the stronger reason such a row is inadmissible in the distribution above -- not merely that a bound cannot be divided as a cost, but that it is not a sample from that distribution AT ALL, being the cost of a computation that did not happen. AND eval_steps ON A RIGHT-CENSORED ROW IS A TRUNCATION ARTIFACT, NOT A WORKLOAD FIGURE -- one sentence here to save the next harvester an afternoon. An interrupted claim stopped wherever it had got to when the deadline fired, so its step count records how far it got and nothing else: two observed interrupts on this claim truncate at different step counts, both far below every completed run, and neither denotes a workload. The harvest above groups by eval_steps to hold work constant, which is correct ONLY over completed rows. Group the censored ones the same way and they form a third apparent level out of nothing but where the deadline landed -- a bogus population that will look exactly like the drift finding this row already withdrew once. The two arms are the same underlying fact reached differently: a claim whose completed cost distribution touches its ceiling will, on a bad draw, hit the deadline BEFORE finishing, and then it does not report a larger number, it reports no verdict. THE CONSEQUENCE FOR THE REPAIR IS THAT MARGIN IS WORTH MORE THAN IT LOOKS: an overrun is a cost debt on a claim that PASSED, while an interrupt leaves the subject UNDECIDED and is the arm that refuses. Headroom is bought against the second. AND THE REFUSAL BEHAVIOUR OF THAT ARM IS A SEPARATE FILED CLASS, cited here rather than re-derived and deliberately NOT absorbed into this row: gunbc.recurring_failure_mode.non_verdict_disposition_surfaces_as_refusal records that the floor computes the difference between THIS SUBJECT IS WRONG and I DID NOT FINISH LOOKING AT THIS SUBJECT and then discards it at the aggregate boundary, so the red check and the merge gate receive one bit whose only affordance is to run it again. Its specimen is a run refused by interrupted rows in which ZERO claims failed. That is a different defect from this one, it is what makes an interrupt here block an unrelated change, and it is that row's to repair. TWO READINGS WERE PROPOSED AND WITHDRAWN ON THE WAY TO THAT, RECORDED BECAUSE BOTH ARE TEMPTING. A drift -- the claim walking toward the line across a level change -- dissolved once the smaller step-count group was compared against the larger group's actual range rather than against its own mean: the apparent second level sits inside the first population's spread. And a small-sample variance figure understated that spread, which is what made the two groups look separated at all. One error, twice: a sample too small to see its own width. THE REFUSAL IS CORRECT AS A MEASUREMENT AND WRONG AS AN ATTRIBUTION, and the distinction decides the repair. The CPU really was consumed, so the gate is not lying; but that cost is not a property of this claim's code, so charging it to this claim attributes it wrongly. A per-claim threshold enforced on ONE DRAW from a distribution this wide is estimating a statistic it cannot see from a single sample. Raising the ceiling would silence the wrong half and destroy the evidence, which is why no number moves here. THE REPAIR IS MARGIN, AND IT IS THE POOL-PROPORTIONAL SHAPE ALREADY ESTABLISHED ABOVE -- which needs no separate justification, being a DESIGN 2 bare-minimum-cost defect that is fixed regardless of realized n. It was never the blocker and it is still the fix. AND THE ACCEPTANCE TARGET IS DERIVED FROM THE MEASUREMENT RATHER THAN GUESSED: holding the line against a spread of that width requires the MEDIAN to sit below the ceiling divided by the spread, which gives the required reduction directly -- re-derive both the median and the spread from the harvest named above and take the ratio, rather than reading a percentage here. AND THE ACCEPTANCE EVIDENCE IS A DISTRIBUTION, NEVER A GREEN RUN. A claim this near its ceiling under this spread goes green sometimes with nothing repaired, so the first green after any change carries almost no information and is exactly what will be offered as proof. What establishes a repair is a distribution at EQUAL WORK, before and after, on the enforcing population. The before is the harvest described above and it exists today. IF MARGIN CANNOT BE OBTAINED, the remaining honest arm is a further bounded drop naming the shape fix as its trigger at capability grain. Never a bigger ceiling. A RECEIPT FOR THE COST COPRODUCT, RECORDED BECAUSE IT IS A RUNG CLAIM WITH AN EXECUTION BEHIND IT RATHER THAN A DESIGN INTENTION. The observation that opened this investigation was a budget-refused reading -- a lower bound on a cost that never completed, not a cost. It was the most persuasive number available and it was on the correct population, and it is INADMISSIBLE in any ratio. gunbc.floor_cost_distribution refuses it STRUCTURALLY, because its cost reading is a coproduct and a bound has no constructor a cost fits into; no reviewer's judgement had to catch it. That class was filed after a rendered figure just over this same ceiling was read as a completed cost, and it then prevented the identical error in a later lane that knew the story and still reached for the number. AN INSTRUMENT GAP IS DECLARED HERE RATHER THAN PAPERED OVER. The ANALYSIS for the environment-variance question already exists and is not to be re-minted: gunbc.floor_cost_distribution models the cost reading as a coproduct so a censored bound cannot be divided as a cost, and identity_inflation_permille_at_equal_work pairs rows across two runs by identity AND by equal evaluator steps, which is precisely CPU divergence at byte-identical work. What does not exist is an ACTUATOR that runs one claim N times in N processes over one tree and hands the pairs to it, and the actuator that does exist runs only inside CI. So the variance figures recorded elsewhere in the seed were transcribed not because the concept lacked a home but because nothing could RE-RUN it on demand. A NEIGHBOURING CLASS THIS INVESTIGATION SURFACED, FILED IN ITS OWN ROW AND CITED HERE RATHER THAN STORED HERE: gunbc.recurring_failure_mode.inflation_fold_cannot_name_the_environment_it_measures. It is not a trigger of this drop and cannot retire it -- its subject is whether a per-claim cost MEASUREMENT can be trusted, which is a different invalid state with a different harm. It is named here for one reason only: a lane meeting THIS row's trigger must show the cost shape changed, and the evidence for that is a distribution over repeated runs, which is exactly the analysis that class governs. Read it before quoting any such distribution. A repair must be derived from measurement rather than from a plausible mechanism -- that is what the refutations below establish -- but it is the cost SHAPE that must change, not a named construct that must be found first. SUFFICIENT FOR (unchanged, and still the thing being restored): determinism_transitive_holds with pool_roots=['src/v2/lens'] and pool_files=[] reaching a verdict within the per-claim line at directory grain, WITHOUT NARROWING THE SUBJECT -- scoping pool_roots to the modules the walk happens to reach remains the trap and not the repair, because it lowers the number by shrinking the population, leaves the cost shape intact, and re-breaks the moment the subject widens, which is the widening this drop exists to restore. COST SHAPES IN THIS WALK ARE REAL AND ARE EXPLICITLY NOT THE COST, recorded so a later reader does not fix them and believe the defect is gone. THREE OF THEM ARE NOW REPAIRED and are named in the past tense because their symbols no longer resolve: call_reachable_decls_go scanned `reached` linearly per seed through a decl_in_list helper that is deleted, and now answers membership by keyed lookup over a seen map; it appended to `reached` with a copied accumulator and now conses and reverses once at the end; and list_append(rest, callee_decls) copied the worklist every step and is now guarded so an empty callee list does not copy it. REPAIRING THEM DID NOT RETIRE THIS DROP AND WAS NEVER EXPECTED TO: the pool scan in decls_matching_callee is untouched, and this row is retired by the trigger stated at the head of this field -- the cost shape -- and by nothing else. ONE SHAPE IN callees_from_node IS AN ADMITTED, UNRESOLVED OBLIGATION rather than a repair: its duplicate suppression is a linear scan of the accumulated list per callee, which is quadratic in the callees of one declaration and is subject to the same bare-minimum-cost rule. A map-keyed arm was written and measured SLOWER than the list scan at the realized callee counts and was reverted on that measurement; big-O did not grant permission to ship the slower realization, and equally the slower first attempt did not retire the defect it was aimed at. The obligation dissolves when the walk is asked at a grain whose per-declaration callee counts are large enough for the keyed arm to win, and it is recorded here rather than in the source so that it is folded with the rest of this row. THE REMAINING UNREPAIRED SHAPES: determinism_transitive_findings folds with concat(acc, determinism_findings(...)), a copied accumulator that is FREE while the corpus is clean and degrades quadratically exactly when findings appear, so it is invisible in every green run and expensive only when something is already wrong. determinism_live_closure_modules folds list_snoc_item over module_declaration_facts_live(pool_roots: []), a copied accumulator over a list that is empty today. Until the trigger stated at the head of this field is met, determinism over the fn-arrow call graph is unverified. The way out is that trigger and nothing else. ### admission rows on falsifier-family cadences with no scheduled route, awaiting transition to a cadence that executes — declared 2026-09-08 diff --git a/src/v1/stage0/src/bin/claim_batch.rs b/src/v1/stage0/src/bin/claim_batch.rs index f796d43125d..9af26e51dcb 100644 --- a/src/v1/stage0/src/bin/claim_batch.rs +++ b/src/v1/stage0/src/bin/claim_batch.rs @@ -619,11 +619,7 @@ fn run_witnesses( ctx.set_witness_eval_budget(eval_budget_ms); for function in &group.functions { run_claim_timed(&ctx, &closure_subject, function, timings); - // The eval-call memo's eviction scope is the witness frame, not this - // shared per-entry ctx — ctx-lifetime retention of argument+result - // values across witnesses is byte-unbounded (20GiB-class kills). v1_compiler::v1_interpreter::print_eval_recompute_trace(&ctx); - v1_compiler::v1_interpreter::eval_call_memo_frame_exit(&ctx); } Ok(()) } @@ -913,11 +909,7 @@ fn run() -> Result { ctx.set_witness_eval_budget(eval_budget_ms); for function in &group.functions { run_claim_timed(&ctx, &closure_subject, function, &mut timings); - // Witness frame exit on the single-entry fast path too — this is - // the exact path the 6-witness 20GiB-kill recipe runs (the memo - // must not retain values across witnesses sharing this ctx). v1_compiler::v1_interpreter::print_eval_recompute_trace(&ctx); - v1_compiler::v1_interpreter::eval_call_memo_frame_exit(&ctx); } if stats_requested { print_interp_stats(&ctx, flatten_baseline); diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 3fde45cfc2d..69d9255336e 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -18591,9 +18591,6 @@ pub fn run_claims_in_process( let closure_subject = format!("in-process-claim:{entry}"); for function in functions { let (outcome, _receipt) = run_claim_measured(&ctx, &closure_subject, function); - // Frame exit: the eval memo must not retain values across claims sharing - // this ctx (byte-unbounded, the 20GiB-class kills — same as the gate path). - v1_interpreter::eval_call_memo_frame_exit(&ctx); if outcome == ClaimOutcome::Pass { println!("PASS {function}"); } else { diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index d2ac5dba487..fabc4da4410 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -2116,6 +2116,7 @@ fn cross_claim_args_hash(ctx: &InterpContext, args: &[(Option, Value)]) let mut hasher = std::collections::hash_map::DefaultHasher::new(); args.len().hash(&mut hasher); for (name, value) in args { + note_argument_identity_derived(ctx); name.hash(&mut hasher); eval_recompute_arg_key(&mut hash_memo, &interner, value)?.hash(&mut hasher); } @@ -4242,72 +4243,18 @@ pub fn refresh_eval_recompute_trace_enabled_cache_for_tests() { eval_recompute_trace_refresh_cache(); } -// The eval-frame memo: the ladder's single-site discharge provider, realized in the seed. -// Buckets by the ledger key (fn identity x argument identity), serves only after the stored -// call's argument names AND values verify equal — a collision degrades to recompute, never a -// wrong value. Eviction is ScopeExit at the WITNESS frame: batch surfaces share one ctx across -// an entry's witnesses and call eval_call_memo_frame_exit after each claim fn (ctx-lifetime -// retention of argument+result values is byte-unbounded — the 2026-07-10 20GiB-class -// regression). Admission stops at the entry cap with the refusal COUNTED (overflow). Default -// ON everywhere; GUNBC_EVAL_MEMO=0 is a diagnostic realization switch (recompute instead of -// serve, semantics identical), and the receipt discloses hits/misses so a disabled memo shows -// as memo_hits=0, never assumed working. -struct EvalCallMemo { - // Per-ctx realization switch (GUNBC_EVAL_MEMO read at ctx construction, not a - // process-wide latch): provider-attribution tests pin the outer eval-frame provider off on - // their own ctx so an inner provider's hit counters stay discriminating; semantics are - // identical either way. - enabled: bool, - map: std::collections::HashMap, Value)>, Value)>>, - // fn-node Rcs kept alive so fn_ptr keys stay valid for the ctx lifetime - // (same discipline as EvalRecomputeTrace.keepalive_fns). - keepalive_fns: Vec>, - hits: u64, - misses: u64, - overflow: u64, +/// How many argument identities this frame has derived so far (see the field). Zero on the +/// production route: no keying site runs for an undeclared single demand. +pub fn argument_identities_derived(ctx: &InterpContext) -> u64 { + ctx.argument_identities_derived.get() } -impl Default for EvalCallMemo { - fn default() -> Self { - EvalCallMemo { - enabled: eval_call_memo_env_default(), - map: std::collections::HashMap::new(), - keepalive_fns: Vec::new(), - hits: 0, - misses: 0, - overflow: 0, - } - } -} - -const EVAL_CALL_MEMO_ENTRY_CAP: usize = 1_000_000; - -fn eval_call_memo_env_default() -> bool { - std::env::var("GUNBC_EVAL_MEMO") - .map(|v| v != "0") - .unwrap_or(true) -} - -/// Realization switch, per ctx: an inner provider's by-execution receipt suite (e.g. the -/// parse-table MemoTier's amortization tests) pins the eval-frame provider off so pass-2 -/// demands re-execute and the inner door's hit counters keep discriminating. Values are -/// identical either way. -pub fn set_eval_call_memo_enabled(ctx: &InterpContext, enabled: bool) { - ctx.eval_call_memo.borrow_mut().enabled = enabled; -} - -/// Frame exit for the eval-call memo: eviction scope is the WITNESS frame, not the ctx. Batch -/// surfaces (claim_batch, claim_executor) share one ctx across an entry's witnesses for the -/// resolve-side ReferenceTier share, but the memo stores full argument+result VALUES, so -/// ctx-lifetime retention across N witnesses is byte-unbounded (measured 2026-07-10: one -/// witness plateaus ~3.4GiB, six in one ctx pass ~20GiB to SIGKILL). Called after each claim -/// function; map and keepalives drain, counters stay CUMULATIVE so receipts remain honest. -/// Cross-witness serving is an outer-frame promotion that must arrive as a conscious provider -/// row with byte-bounded admission — never a default. -pub fn eval_call_memo_frame_exit(ctx: &InterpContext) { - let mut m = ctx.eval_call_memo.borrow_mut(); - m.map.clear(); - m.keepalive_fns.clear(); +/// One argument position reached `eval_recompute_arg_key`. Called from the three keying sites +/// (`eval_recompute_key`, `eval_recompute_partial_key`, `cross_claim_args_hash`) and nowhere +/// else, so the odometer's unit is stated by those call sites rather than by convention. +fn note_argument_identity_derived(ctx: &InterpContext) { + ctx.argument_identities_derived + .set(ctx.argument_identities_derived.get().wrapping_add(1)); } #[derive(Default, Clone)] @@ -5023,8 +4970,7 @@ pub struct InterpContext { // per call (authored_name_at). Memoized per fn_node pointer. The pointer alone is unsound: // the ctx does not own fn_nodes (borrowed `Rc`s droppable while the ctx lives), so a // freed address can be reused and collide. keepalive_fns retains the `Rc` behind each - // key for the ctx's lifetime (as PureCallMemo.keepalive_fns / EvalRecomputeTrace.keepalive_fns - // / EvalCallMemo.keepalive_fns), and the cache dies with the ctx (as data_cache). + // key for the ctx's lifetime (as PureCallMemo.keepalive_fns / EvalRecomputeTrace.keepalive_fns), and the cache dies with the ctx (as data_cache). // Value = (filtered named-param list, all-param list), matching call_function's two uses. param_name_cache: std::cell::RefCell, Vec)>>>, param_name_cache_keepalive: std::cell::RefCell>>, @@ -5051,14 +4997,19 @@ pub struct InterpContext { pure_call_memo: std::cell::RefCell, parse_table_memo: std::cell::RefCell, eval_recompute_trace: std::cell::RefCell, - eval_call_memo: std::cell::RefCell, - // Effect-dispatch odometer, incremented per service-operation dispatch. The eval-call memo - // compares it across a named call and refuses to memoize any call during which it advanced - // — a WorldRead/effect is never served stale (the uses-empty purity gate is vacuous - // corpus-wide: no corpus func declares `uses`, so every effectful wrapper was memo-eligible; + // Effect-dispatch odometer, incremented per service-operation dispatch. The cross-claim + // tier compares it across a named call and refuses to store any call during which it + // advanced — a WorldRead/effect is never served stale (the uses-empty purity gate is vacuous + // corpus-wide: no corpus func declares `uses`, so every effectful wrapper was store-eligible; // found via the artifact-store List-after-Delete staleness). effect_dispatch_count: std::cell::Cell, eval_recompute_hash_memo: std::cell::RefCell, + // Odometer of ARGUMENT IDENTITIES DERIVED in this frame -- one per argument position that + // reached `eval_recompute_arg_key`, whichever keying site asked (the recompute-trace ledger + // or the cross-claim tier). It exists so the fact that an undeclared single demand derives + // NO identity is executable rather than asserted: the enrolled control reads it back at zero + // on the production route and would go red if unconditional keying were restored. + argument_identities_derived: std::cell::Cell, mutation_counters: std::cell::RefCell, symbols: RefCell, published_mock_keys: RefCell>>>, @@ -5478,9 +5429,9 @@ impl InterpContext { pure_call_memo: std::cell::RefCell::new(PureCallMemo::default()), parse_table_memo: std::cell::RefCell::new(ParseTableMemo::default()), eval_recompute_trace: std::cell::RefCell::new(EvalRecomputeTrace::default()), - eval_call_memo: std::cell::RefCell::new(EvalCallMemo::default()), effect_dispatch_count: std::cell::Cell::new(0), eval_recompute_hash_memo: std::cell::RefCell::new(EvalRecomputeHashMemo::default()), + argument_identities_derived: std::cell::Cell::new(0), mutation_counters: std::cell::RefCell::new(MutationCounters::default()), symbols: RefCell::new({ let mut interner = SymbolInterner::default(); @@ -8432,13 +8383,28 @@ fn eval_call(node: &Rc, env: &Rc, ctx: &InterpContext) -> InterpResul call_function(ctx, &fn_node, &args, env) } -/// Pure named-fn calls flow through here: the demand ledger records every keyed call, and the -/// eval-frame memo (the ladder's single-site discharge provider) serves repeats from the first -/// evaluation. A hit still records the DEMAND — the receipt counts plurality; the provider -/// changes cost, never count. Soundness: hash-bucketed on the ledger key but served only after -/// argument names AND values verify equal (Value::eq, the one equality authority) — a collision -/// degrades to recompute, never a wrong value. Unkeyed calls (closure args) stay unmemoized -/// and are counted. +/// Pure named-fn calls flow through here, and ADMISSION PRECEDES IDENTITY. A demand is judged +/// before any key is built for it, and the judgment is the one `std.materialization_ladder` +/// already states: a pure demand with no declared plural obligation is AcceptedSingleRecompute, +/// whose prescription is Recompute -- so it constructs, looks up and retains NO result-memo key +/// merely because its callee is pure. Two provider tiers still serve, and both are admitted by a +/// declared judgment consumed BEFORE their key is derived: the cross-claim tier (a roster of +/// producers whose demands are plural across the floor's isolated claim frames -- +/// `try_cross_claim_pure_memo`, admission by resolved declaration identity, then the content +/// hash) and the parse-table memo (`try_parse_table_memo_dispatch`, admission by the Memoize +/// verdict carried on the table). The eval-frame result memo that used to stand here keyed EVERY +/// pure call in case a second, undeclared demand arrived: a provider whose scope was one +/// shared-state frame, which the ladder never discharges into (a within-frame repeat is +/// AuthoredDuplication, prescribed Share, never Memoize), so its admitted population was empty by +/// construction and the key it built per call was pure cost -- O(|argument|) per call, which on +/// a fold threading a document through every recursive call is O(n^2) +/// (gunbc.recurring_failure_mode.memo_key_rehashes_a_growing_persistent_value). It is deleted, +/// not gated: a gate over an empty admitted set is dead weight of the same kind. +/// +/// The only remaining keying on this path is the recompute-trace LEDGER, and it is not a +/// provider: it is the DESIGN section 5 stopped-line audit that measures demand plurality so an +/// unexpected recurrence can be declared for the next run (ladder rule 4). It keys only under +/// GUNBC_RECOMPUTE_TRACE=1, which the floor sets for itself, and it serves nothing. fn eval_pure_named_call( ctx: &InterpContext, call_node: &Rc, @@ -8458,9 +8424,8 @@ fn eval_pure_named_call( } else { None }; - let trace_on = eval_recompute_trace_enabled(); - let memo_on = ctx.eval_call_memo.borrow().enabled; - if !trace_on && !memo_on { + if !eval_recompute_trace_enabled() { + // The production route: no identity is derived for an undeclared single demand. let effects_before = ctx.effect_dispatch_count.get(); let result = call_function(ctx, fn_node, args, env); if let Ok(v) = &result { @@ -8484,9 +8449,6 @@ fn eval_pure_named_call( let key = match eval_recompute_key(ctx, fn_node, args) { Some(key) => key, None => { - if !trace_on { - return call_function(ctx, fn_node, args, env); - } // TIMED, not merely counted: the composite-argument bucket feeds the cross-claim // census, which ranks by duration. Recording after the call is what makes the two // buckets comparable; the earlier count-only form could name a producer it could @@ -8503,21 +8465,6 @@ fn eval_pure_named_call( return result; } }; - if memo_on { - if let Some(v) = eval_call_memo_get(ctx, &key, args) { - if trace_on { - eval_recompute_record( - ctx, - call_node, - fn_node, - func_name, - key, - started.elapsed().as_nanos(), - ); - } - return Ok(v); - } - } let effects_before = ctx.effect_dispatch_count.get(); let result = call_function(ctx, fn_node, args, env); if let Ok(v) = &result { @@ -8526,21 +8473,14 @@ fn eval_pure_named_call( store_cross_claim_pure_memo(ctx, fn_node, func_name, args, v, fill_guard.as_ref()); } } - if memo_on && ctx.effect_dispatch_count.get() == effects_before { - if let Ok(v) = &result { - eval_call_memo_put(ctx, fn_node, key.clone(), args, v.clone()); - } - } - if trace_on { - eval_recompute_record( - ctx, - call_node, - fn_node, - func_name, - key, - started.elapsed().as_nanos(), - ); - } + eval_recompute_record( + ctx, + call_node, + fn_node, + func_name, + key, + started.elapsed().as_nanos(), + ); result } @@ -9115,6 +9055,7 @@ fn eval_recompute_key( let interner = ctx.symbols.borrow(); let mut keys = Vec::with_capacity(args.len()); for (_, v) in args { + note_argument_identity_derived(ctx); keys.push(eval_recompute_arg_key(&mut memo, &interner, v)?); } Some(EvalRecomputeKey { @@ -9143,6 +9084,7 @@ fn eval_recompute_partial_key( let mut keys = Vec::with_capacity(args.len()); let mut unkeyable = 0usize; for (_, v) in args { + note_argument_identity_derived(ctx); match eval_recompute_arg_key(&mut memo, &interner, v) { Some(k) => keys.push(k), None => { @@ -9293,13 +9235,14 @@ pub fn print_eval_recompute_trace(ctx: &InterpContext) { .collect(); duplicated.sort_by(|a, b| b.1.cmp(&a.1)); eprintln!( - "[recompute-trace] keyed_calls={} unkeyed_calls={} overflow_calls={} distinct_keys={} duplicated_keys={} wasted_ms={} (durations inclusive of callees)", + "[recompute-trace] keyed_calls={} unkeyed_calls={} overflow_calls={} distinct_keys={} duplicated_keys={} wasted_ms={} argument_identities_derived={} (durations inclusive of callees)", totals.keyed_calls, totals.unkeyed_calls, totals.overflow_calls, totals.distinct_keys, totals.duplicated_keys, - totals.wasted_ns_total / 1_000_000 + totals.wasted_ns_total / 1_000_000, + argument_identities_derived(ctx) ); eprintln!( "[recompute-trace] gap: single_site_keys={} wasted_ms={} (same call expression re-hit — value-coincident/loop-borne, memoize/Share territory) | multi_site_keys={} wasted_ms={} (cross-site duplicate demand — static rewire candidates)", @@ -9344,11 +9287,6 @@ pub fn print_eval_recompute_trace(ctx: &InterpContext) { site ); } - let (hits, misses, overflow) = eval_call_memo_counters(ctx); - eprintln!( - "[recompute-trace] eval-memo: hits={} misses={} overflow={} (verified-hit serve; a hit still counts as a demand above)", - hits, misses, overflow - ); } // Everything a re-evaluated key cost beyond one evaluation's amortized share. @@ -9661,8 +9599,8 @@ fn cross_claim_demand_absorb_one( /// no-op unless `GUNBC_RECOMPUTE_TRACE=1`, which the floor sets for itself. /// /// THE CALLER MUST OWN A FRESH FRAME PER CLAIM, and that is a real precondition rather than a -/// style note. The ledger accumulates for the lifetime of its `InterpContext` and is NOT -/// cleared by `eval_call_memo_frame_exit`, so a surface that shares one context across several +/// style note. The ledger accumulates for the lifetime of its `InterpContext`, so a surface +/// that shares one context across several /// claims — `claim_batch` shares one per ENTRY — would fold each claim's ledger again on the /// next call, inflating both `evals` and `total_ns` and, worse, reporting cross-claim demand /// where there is only one frame's. The required floor builds a frame per claim @@ -9834,9 +9772,6 @@ pub struct EvalRecomputeTotals { pub wasted_ns_total: u128, pub wasted_ns_single_site: u128, pub wasted_ns_multi_site: u128, - pub memo_hits: u64, - pub memo_misses: u64, - pub memo_overflow: u64, } impl EvalRecomputeTotals { @@ -9851,9 +9786,6 @@ impl EvalRecomputeTotals { self.wasted_ns_total += o.wasted_ns_total; self.wasted_ns_single_site += o.wasted_ns_single_site; self.wasted_ns_multi_site += o.wasted_ns_multi_site; - self.memo_hits += o.memo_hits; - self.memo_misses += o.memo_misses; - self.memo_overflow += o.memo_overflow; } } @@ -9884,12 +9816,7 @@ fn trace_totals(t: &EvalRecomputeTrace) -> EvalRecomputeTotals { } pub fn eval_recompute_totals(ctx: &InterpContext) -> EvalRecomputeTotals { - let mut out = trace_totals(&ctx.eval_recompute_trace.borrow()); - let m = ctx.eval_call_memo.borrow(); - out.memo_hits = m.hits; - out.memo_misses = m.misses; - out.memo_overflow = m.overflow; - out + trace_totals(&ctx.eval_recompute_trace.borrow()) } // Process-wide accumulator fed by InterpContext::drop, so EVERY eval path lands in the receipt @@ -9941,76 +9868,6 @@ fn value_rc_identity(v: &Value) -> Option { } } -// Same-allocation composites are equal without a walk; everything else takes -// the full structural equality (Value::eq, the one equality authority). -fn value_fast_eq(a: &Value, b: &Value) -> bool { - if let (Some(x), Some(y)) = (value_rc_identity(a), value_rc_identity(b)) { - if x == y { - return true; - } - } - a == b -} - -// A stored call matches only when argument NAMES and values both agree — -// names participate in parameter binding, so value-equal args under different -// labels are a different call, never served. -fn eval_call_memo_args_match( - stored: &[(Option, Value)], - args: &[(Option, Value)], -) -> bool { - stored.len() == args.len() - && stored - .iter() - .zip(args.iter()) - .all(|((sn, sv), (an, av))| sn == an && value_fast_eq(sv, av)) -} - -fn eval_call_memo_get( - ctx: &InterpContext, - key: &EvalRecomputeKey, - args: &[(Option, Value)], -) -> Option { - let mut m = ctx.eval_call_memo.borrow_mut(); - let mm = &mut *m; - if let Some(bucket) = mm.map.get(key) { - for (stored_args, value) in bucket { - if eval_call_memo_args_match(stored_args, args) { - mm.hits += 1; - return Some(value.clone()); - } - } - } - None -} - -fn eval_call_memo_put( - ctx: &InterpContext, - fn_node: &Rc, - key: EvalRecomputeKey, - args: &[(Option, Value)], - value: Value, -) { - let mut m = ctx.eval_call_memo.borrow_mut(); - // Counter invariant: a miss means the call was NOT served (it evaluated), so a cap-refused - // store is still a miss — overflow ⊆ misses, and hits + misses == keyed Ok-resulting calls - // through the memo path, including under overflow. `misses` is NOT "entries stored". - m.misses += 1; - if m.map.len() >= EVAL_CALL_MEMO_ENTRY_CAP && !m.map.contains_key(&key) { - m.overflow += 1; - return; - } - m.keepalive_fns.push(fn_node.clone()); - let stored_args: Vec<(Option, Value)> = args.to_vec(); - m.map.entry(key).or_default().push((stored_args, value)); -} - -/// Per-ctx memo counters (hits, misses, overflow) — for witnesses and -/// diagnostics; the process receipt aggregates these via ctx Drop. -pub fn eval_call_memo_counters(ctx: &InterpContext) -> (u64, u64, u64) { - let m = ctx.eval_call_memo.borrow(); - (m.hits, m.misses, m.overflow) -} fn pure_call_memo_key( fn_node: &Rc, func_name: &str, diff --git a/src/v1/stage0/tests/pure_demand_recompute_admission.rs b/src/v1/stage0/tests/pure_demand_recompute_admission.rs new file mode 100644 index 00000000000..ab732533b0f --- /dev/null +++ b/src/v1/stage0/tests/pure_demand_recompute_admission.rs @@ -0,0 +1,91 @@ +//! A pure demand with no declared plural obligation derives no identity: the seed consumes the +//! ladder's AcceptedSingleRecompute judgment BEFORE any key is built (DESIGN section 2; +//! `std.materialization_ladder` rule 5), so an undeclared single demand constructs, looks up and +//! retains no result-memo key merely because its callee is pure. +//! +//! Execute: cargo test -p v1-compiler --test pure_demand_recompute_admission. +//! Required clippy --all-targets compiles this target; no CI step executes it. +//! The declared drop is gunbc.rung_drop.rust_unit_tests_off_the_merge_path. +//! +//! ITS OWN BINARY, DELIBERATELY: the recompute-trace switch is a process-wide latch, and the +//! interpreter's in-crate tests turn it ON and never off. The RED here needs it OFF, so the two +//! arms run sequentially in one test in a process nothing else shares. + +use std::rc::Rc; +use v1_compiler::v1_compiler_compile::{compile_to_resolved, SourceFile}; +use v1_compiler::v1_interpreter::{self, ExecutionMode, InterpContext, Value}; + +const FIXTURE: &str = "module fixture.recompute_admission\n\ + fn measure(s: String) -> Int { string_length(s) }\n\ + fn demand() -> Int { measure(s: \"a pure demand, undeclared, single\") }\n"; + +fn fresh_ctx(result: &v1_compiler::v1_compiler_compile::ResolvedPipelineResult) -> InterpContext { + let graph = result.graph.as_ref().expect("fixture graph"); + InterpContext::new( + graph, + result.source_indices.clone(), + ExecutionMode::Hermetic, + ) +} + +/// Evaluate `demand()` once and return (value, evaluator steps it took). +fn one_demand(ctx: &InterpContext) -> (Value, u64) { + let before = v1_interpreter::evaluator_steps(); + let v = v1_interpreter::run_in_context(ctx, "fixture.recompute_admission.demand", false) + .expect("demand evaluates"); + (v, v1_interpreter::evaluator_steps() - before) +} + +/// THE RED: on the production route (trace off) two equal pure demands derive ZERO argument +/// identities and both EVALUATE -- the second is not served from the first. Restoring +/// unconditional keying (a key built before admission) turns the first assertion red; restoring +/// a result memo that serves the repeat turns the second red (a served call takes no callee +/// steps). THE POSITIVE CONTROL is the same pair under the recompute-trace ledger, the one +/// keying site that is admitted on this path: it derives exactly one identity per demand (one +/// String argument each) and STILL evaluates both, because the ledger is an instrument and not +/// a provider. Without that control the RED could pass because keying was unreachable for an +/// unrelated reason. +#[test] +fn an_undeclared_single_pure_demand_derives_no_identity_and_is_never_served() { + let result = compile_to_resolved(Rc::new(im::vector![Rc::new(SourceFile { + path: "workspace/src/recompute_admission.dag".to_string(), + content: FIXTURE.to_string(), + })])); + + // Arm 1: production route. + std::env::remove_var("GUNBC_RECOMPUTE_TRACE"); + v1_interpreter::refresh_eval_recompute_trace_enabled_cache_for_tests(); + assert!(!v1_interpreter::eval_recompute_trace_enabled()); + let ctx = fresh_ctx(&result); + let (first, first_steps) = one_demand(&ctx); + let (second, second_steps) = one_demand(&ctx); + assert!(matches!(first, Value::Int(33)), "{first:?}"); + assert_eq!(first, second); + assert_eq!( + v1_interpreter::argument_identities_derived(&ctx), + 0, + "an undeclared single demand must reach no keying site" + ); + assert!(first_steps > 0); + assert_eq!( + first_steps, second_steps, + "the repeat must evaluate in full: a served repeat takes no callee steps" + ); + + // Arm 2: the recompute-trace ledger, the admitted keying site, keys and still evaluates. + std::env::set_var("GUNBC_RECOMPUTE_TRACE", "1"); + v1_interpreter::refresh_eval_recompute_trace_enabled_cache_for_tests(); + assert!(v1_interpreter::eval_recompute_trace_enabled()); + let traced = fresh_ctx(&result); + let (_, traced_first_steps) = one_demand(&traced); + let (_, traced_second_steps) = one_demand(&traced); + assert_eq!( + v1_interpreter::argument_identities_derived(&traced), + 2, + "the ledger derives one identity per demand: one String argument, two demands" + ); + assert_eq!(traced_first_steps, first_steps); + assert_eq!(traced_second_steps, first_steps); + std::env::remove_var("GUNBC_RECOMPUTE_TRACE"); + v1_interpreter::refresh_eval_recompute_trace_enabled_cache_for_tests(); +} diff --git a/src/v2/lens/complexity_accumulator_copy/roster_gate.dag b/src/v2/lens/complexity_accumulator_copy/roster_gate.dag index 2bb6d3016ac..8526df87cc1 100644 --- a/src/v2/lens/complexity_accumulator_copy/roster_gate.dag +++ b/src/v2/lens/complexity_accumulator_copy/roster_gate.dag @@ -23,8 +23,7 @@ import std.types { List } // Operator-ruled OFFLINE (NOT CI discovery-enrolled; witness_exclusion_substrings row // claim/complexity/accumulator_copy_roster_gate in gunbc.ci_layer_roots — owned by #6452, not -// duplicated on #6440). Serial wet claim_batch only — do not codify GUNBC_EVAL_MEMO=0 in CI; -// diagnostic local runs may set it. Std tranche (PR #6440): claim_batch --source-root dag +// duplicated on #6440). Serial wet claim_batch only. Std tranche (PR #6440): claim_batch --source-root dag // --source-root src/v2 --entry // src/v2/test/claim/complexity/accumulator_copy_roster_gate_std_test.dag --function // roster_std_change_dag_zero_suspects_within_ratchet --claim-run --wet. Prior roster carriers: diff --git a/src/v2/workflow/realization_runner.dag b/src/v2/workflow/realization_runner.dag index 8c097c1ea57..9a6dba3fb62 100644 --- a/src/v2/workflow/realization_runner.dag +++ b/src/v2/workflow/realization_runner.dag @@ -76,8 +76,9 @@ fn node_keyed_store_node_count(store: NodeKeyedStore) -> Int { // ROW-LOCAL FACTS ONLY (encoded body length): a stored transitive size would be a dual // representation of the child_refs topology, so transitive footprint is DERIVED, never stored. The // reachable-set fold node_keyed_graph_transitive_bytes IS the single value-size authority — the -// eval-memo byte-cap admission (extdeps.realization.eval_memo) and the space-lens predictor both -// bind to it, and no parallel size walk may exist anywhere. Content hashes ground on the fnv1a64 +// space-lens predictor binds to it (the eval-frame memo whose byte cap was to bind here is +// retired: an undeclared single demand derives no identity), and no parallel size walk may exist +// anywhere. Content hashes ground on the fnv1a64 // authority surfaced by std.content_hash / the v1 intrinsics (DESIGN section 3 convergence thread) // — this schema must not mint a third hash surface; ContentHash here is the std.types carrier. // Failure arms REFUSE, never widen: a child ref with no row refuses with the missing hash, never a