Repository navigation
Seed-mirror constant lens over five hand-Rust budget constants — and the 11-day fleet arming drift it caught (13GiB -> 15GiB) - #8638
Merged
Conversation
…o their authority rows Two seed_mirror_notes each asked for "one lens reading the seed's constants against their cited rows" and neither was built. They also named DIFFERENT overlapping subsets, so the mechanism had two partial specifications and no implementation. This is the union. The lens never writes an expected value: each assertion renders its literal from the imported authority row, so editing the lens cannot satisfy it and editing the authority moves the expectation. An uncited or unparseable constant REFUSES rather than skipping -- "nothing to check, so green" is the empty-observation narrow, and of the five constants in scope the one that carried no citation is the one that drifted. Also canonicalizes the in-scope seed literals to plain decimal (3 * 1024 * 1024, 4_000, 12_884_901_888) and adds the missing authority citations. Values unchanged in this commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…iB -> 15GiB This is the value correction, isolated so it can be signed separately from the lens that found it. The seed constant is a MIRROR of gunbc.runner_slot_allocation gunbc_runner_slot_desired field memory_high. That row moved to 16106127360 (15.0 GiB) in 936f451 / #8388 on 2026-08-17 -- "Raise fleet per-slot row to 16GiB/15GiB from a re-measured floor peak" -- and the mirror did not follow, so the seed carried the superseded 13958643712 (13.0 GiB) for eleven days. This is convergence, not a fleet-axis decision: a committed mirror may only move toward its authority, and the judgement was made by #8388. DIRECTION, stated plainly. The constant has one use site, uncapped_host_budget_from_mem_available, which caps an uncapped host's MemAvailable sample at the declared throttle line. The governor was therefore capping 2 GiB BELOW the declared line; this RAISES arming to what placement and ci_budget_tree already size against. Source-level reading of the use site and its doc comment -- not executed, and not a claim about observed fleet behaviour. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… both notes' future tense Two inert-by-construction surfaces sat beside the drift, which is why eleven days passed without either catching it. The witness: test.claim.host_budget_source built BudgetSourceMemAvailableCappedAtDeclaredHigh with byte_size(13958643712) -- the mirror value under test, retyped into the expectation -- so it greened whichever way the mirror went. A measurement copied from the tree under test is not an oracle. It now reads gunbc_runner_slot_desired().memory_high. The notes: both seed_mirror_notes described the covering lens in the future tense while nothing executed. A dissolution trigger naming a mechanism that does not run reads as guarded to every later author. Both now describe what executes, and state what remains undissolved -- the lens proves the mirror AGREES, not that it is unnecessary, so the class sits at mechanically preventable rather than structurally impossible. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot
Bot
force-pushed
the
session/stern-heron-695-seedlens
branch
from
August 20, 2026 05:15
031aa9d to
f183226
Compare
…ch gap the enumeration hid neat-bee-14 refuted this PR's own claim by reading the diff: it said an uncited in-scope constant REFUSES rather than skips, but "in scope" was five hand-enumerated assertions plus five hardcoded symbol names. A new seed mirror constant was therefore neither checked NOR refused -- invisible, exactly like the drift this module exists to catch. Shipping that sentence would have reproduced the defect inside its own fix. The rows are now one folded roster. Forward: every row must find its declaration and authority symbol in the seed. Backward: marker occurrences per seed file must equal roster rows homed in that file. Rows are distinct and each must be present, so agreeing counts mean no marked constant exists that the roster does not carry -- set equality, not a count standing in for one. The backward count folds this module's own roster, so automating it does not collapse to measure() == measure(). Standardizes the marker across all five declarations, and states the residual plainly: a constant carrying NO marker is still invisible to both arms. This raises the bar from "remembered to edit a list in another file" to "marked the declaration where it was written", and names the next-rung trigger as a Rust-declaration-level census. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…lter(f:) The substrate refused filter(xs:, f:) -- it declares 'predicate', not 'f'. Mirrors the idiom from e0599_emitter_decision_census_witness_test rather than inventing one, and replaces the filter+length count with a fold. Note filesystem_path_grant absolute_path_segments calls filter(xs:, f:) and is the shape that misled me; that is a separate finding, not touched here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…hey used CI caught a regression I caused. Importing gunbc.runner_slot_allocation to derive the declared_high expectation pulled v2.std.algebra into this module's closure, and its contains(xs, item, eq) captured the bare name four unrelated lines were using for the string contains(haystack, needle). v1-seed fn names are not module-scoped, so an import added for one declaration re-resolved a name used by different declarations in the same file, with no local edit to those lines. The floor fold aborted during preparation, so the entire roster failed to run over a two-line edit elsewhere in the file. string_contains is unambiguous and is what this PR's own lens already uses. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The obligation to enroll #8635's DECLARED_WHOLE_CORPUS_COMPILE_MEASURED_DEMAND_BYTES lived only in messages between two sessions, either of which can archive. Anything that must outlive a session belongs in a carrier. Also records WHY that constant is unmarked rather than merely unrostered: the backward arm reds on a marked constant with no row, so a marker landing before its row would red main for the interval between merges. Marker and row land together, in whichever PR is second. Adding the marker alone is the one repair that must not happen. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…s mitigatable Measured, not inferred. Floor run 32337765205 at 4806220 reports claims=9782 declined_live=782; run 32333231183 at the same base reports claims=9782 declined_live=778. Adding this module moved declined_live by exactly +4 and claims by 0, so discovery finds it and the hermetic fold declines it. The declaration is correct: the lens reads .rs text, which is live host state, so ReadsLiveTree is true and SubstrateInputsOnly would be a lie -- and the falsifier that used to catch lying rows died in the floor cut. So the honest rung is MITIGATABLE. The lens discriminates by execution (three arms, 8573608) but nothing runs it automatically, which is exactly the tier DESIGN section 6 names: machinery exists, nothing gates on it. Both seed_mirror_notes are corrected to say so. Larger than this module: 778 live-tree witnesses were already declined at this PR's base. The whole class of seed-.rs-versus-.dag-row check is unexecutable by the current fold, so the covering mechanism both notes asked for cannot be enforced by CI as architected. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Aug 20, 2026
…#8667) DECLARED_WHOLE_CORPUS_COMPILE_MEASURED_DEMAND_BYTES (memory_governor, 7516192768) now carries its SEED MIRROR marker and its row in seed_mirror_constant_rows, joined to gunbc.whole_corpus_compile_admission whole_corpus_compile_measured_peak_demand. The two land in ONE commit because the lens's backward arm requires marker occurrences per seed file to equal roster rows homed in that file: a marker without its row reds main for the interval between the merges. That is why neat-bee-14 withheld the marker on #8635 and why the obligation was recorded in the module rather than left in session chat. #8635 and #8638 have both merged, so the coupling is satisfiable and this is the second PR the note named. The pending-sixth-row note is REPLACED rather than annotated -- every load-bearing sentence in it described an obligation that no longer exists, and a reader finding the old text beside a correction has to adjudicate which half is live. What survives, because it was never about this constant: the residual is that a seed constant with a real authority row and no marker is invisible to both arms, so coverage is bounded by who remembers to mark. This constant was the live specimen of that residual and is no longer one. The residual and its next-rung trigger (a census from the Rust declaration's own syntax rather than from a marker convention) are unchanged. Co-authored-by: Brian Searls <briansearls1@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Owned by session
stern-heron-695. Branchsession/stern-heron-695-seedlens(my session branchsession/stern-heron-695is held by #8619).Routed by
deep-ant-102after a sibling-mirror check on #8635 turned up a live defect. Scoping the lens found the thing the lens was for.The finding
Two
seed_mirror_noterows —gunbc.typed_module_cache_capacitytyped_module_cache_capacity_seed_mirror_noteandgunbc.host_budget_sourcehost_budget_source_seed_mirror_note— each asked for "one lens reading the seed's constants against their cited rows" as their covering dissolution. Neither was built. They also named different overlapping subsets, and neither was the union: two partial specifications of one mechanism, which is the §3 shape in its own right.Under that unbuilt trigger, one constant was drifted:
TYPED_MODULE_BYTES_PER_ENTRY_ESTIMATEtyped_module_bytes_per_entry_estimate3145728TYPED_MODULE_CACHE_MAX_ENTRIES_FLOORtyped_module_cache_entries_floor100TYPED_MODULE_CACHE_MAX_ENTRIES_CEILtyped_module_cache_entries_ceiling4000DECLARED_FLOOR_MINIMUM_VIABLE_ARMED_BUDGET_BYTESgunbc_floor_minimum_viable_armed_budget12884901888DECLARED_RUNNER_SLOT_MEMORY_HIGH_BYTESgunbc_runner_slot_desired.memory_high16106127360gunbc_runner_slot_desired.memory_highmoved to 15.0 GiB in936f451446(#8388, 2026-08-17, "Raise fleet per-slot row to 16GiB/15GiB from a re-measured floor peak"). The mirror last moved in47c602caa7(2026-08-06) and did not follow — eleven days at a value a dated operator ruling had superseded. Measured at36a1a42a2e, this PR's base.Two independent surfaces were structurally unable to catch it, which is why eleven days passed. The
typed_module_cache_capacitywitness has 8test fns and zero references to any.rspath, tostage0, or to the literal — it checks the model against itself. Andtest.claim.host_budget_source_witnessbuilt its expectation withbyte_size(13958643712)— the mirror value under test, retyped — so it greened whichever way the mirror went. A measurement copied from the tree under test is not an oracle (2026-08-01 ruling).What lands
1 — the lens (
test.claim.seed_mirror_constant_lens_witness_test). The union of what both notes asked for: five constants, two seed files, two authority modules, as one foldedSeedMirrorRowroster rather than hand-enumerated assertions.It never writes an expected value. Each assertion renders its literal from the imported authority row, so editing the lens cannot satisfy it and editing the authority moves the expectation automatically.
Reach is a two-way join, and this is the part an earlier revision of this PR got wrong. Forward: every roster row must find its declaration and its authority symbol in the seed. Backward: marker occurrences per seed file must equal roster rows homed in that file. Rows are distinct and each is required, so agreeing counts mean no marked constant exists that the roster does not carry — set equality, not a count standing in for one. The backward count folds this module's own roster, so automating it does not collapse to
measure() == measure()and it is not the tree-copied literal the 2026-08-01 oracle ruling forbids.What that does NOT reach, stated because the first version of this PR overclaimed it: a seed constant carrying no marker at all is invisible to both arms. The marker is the enrollment act. So this raises the bar from "someone remembered to edit a list in another file" to "someone marked the declaration where they wrote it" — a real climb, and not a census of every
constin the seed. Next-rung trigger: a Rust-declaration-level census enumerating candidates from the seed's own syntax, at which point the marker is redundant and the roster derives instead of being authored.Also canonicalizes the in-scope seed literals to plain decimal (
3 * 1024 * 1024,4_000,12_884_901_888) and adds the missing authority citations — a mirror's job is to equal its authority, and an equality no join can reach is not one. Values unchanged in that commit.2 — the value correction, in its own commit (
4905a9bb40) so it can be signed separately.13958643712→16106127360. This is convergence, not a fleet-axis decision: a committed mirror may only move toward its authority, and the judgement was made by #8388. Direction stated plainly: the constant's one use site,uncapped_host_budget_from_mem_available, caps an uncapped host's MemAvailable sample at the declared throttle line — so the governor was capping 2 GiB below the declared line, and this raises arming to what placement andci_budget_treealready size against. Source-level reading of the use site and its doc comment; not executed, and not a claim about observed fleet behaviour.3 — the second oracle, and both notes. The witness now derives from
gunbc_runner_slot_desired().memory_high. Both notes are rewritten out of the future tense: a dissolution trigger naming a mechanism that does not run reads as guarded to every later author, and this PR is the receipt for what that costs.Execution receipt
Built and run in one remote dispatch (BuildBuddy, amd64),
SHA=8573608,BUILD_EXIT=0. One binary, three arms. Each perturbation is reverted before the next.013958643712every_seed_mirror_row_matches_its_authority1no_marked_seed_constant_is_missing_from_the_roster1Each arm fails exactly one assertion, and a different one — so the forward and backward arms are independently discriminating and neither fires spuriously. Arm 2 is the real drift value, not a planted one. Arm 3 is the control for reach, which is a separate claim from firing: perturbing an enrolled row can never tell you anything about an unenrolled one, and conflating those two is exactly how the earlier revision of this PR came to claim a refusal it did not have.
The substrate refused this lens three times before it passed, and each refusal improved it.
no field 'success' on type 'FilesystemReadResult'— the primitive carries one field and panics on an unreadable file, so no guard is warranted (cited todag/tools/frontier_ingestion_probefrontier_read_refusal_disposition_note). Thenno parameter named 'f'callingfilter, twice-learned: I had copiedfilter(xs:, f:)fromdag/std/filesystem_path_grant.dagabsolute_path_segments, which contains that shape — a nearby file containing a call is not evidence the call compiles. Worth recording that the dispatch exited 0 on a run whose witness failed; only the in-script exit status made it visible.What changed after that receipt, stated so the SHA is not read as covering more than it does. The three arms ran at
8573608. Two commits followed:afb920a990(below) touches only the sibling witness, not the lens;4806220c04adds a prose row to the lens module and changes no assertion, roster entry, or expected value. The arms therefore still describe the lens's behaviour, but the authority for current HEAD is the floor run on this PR, not this receipt.CI caught a regression these arms structurally could not
Worth stating plainly rather than leaving in the commit log, because it is the same lesson as the reach defect one layer out. Deriving the sibling witness's expectation from its authority row required adding
import gunbc.runner_slot_allocationto it. v1-seed fn names are not module-scoped, so widening that closure pulled inv2.std.algebraand itscontains(xs, item, eq)captured the bare name four lines I never edited were using for the stringcontains(haystack, needle).The failure shape is worth knowing: the fold aborts during preparation, so a two-line edit to an expectation failed the entire ~9782-witness roster, and it presents as "nothing ran" — no
planned=line, no per-witness output — rather than "a test failed". Fixed inafb920a990by pinning those calls tostring_contains(s:, pattern:), the builtin this PR's own lens already uses and has a green receipt for, and verified by resolving that module on its own (both its tests pass atafb920a990).import_widening_shadowed_contains_noterecords it as a receipt so it is not reverted as a style preference.Why my own three arms missed it: all three ran one entry through
claim_batch --entry, resolving the lens and its closure. Nothing imports a test witness — they are leaves — so the edited sibling was never resolved at all. A per-entry green proves the entry compiles, not that the PR does. The rule: resolve the module you edited, which equals "resolve your entry" only when they are the same file; and a per-module resolve still cannot see a capture that manifests only when the fold prepares one subject over the whole roster, so the floor run is the only sufficient check.Rung, stated honestly — and it is lower than this PR first claimed
Mitigatable. NOT mechanically preventable. The floor run settled it, against me:
claimsdeclined_live36a1a42a2e(run32333231183)4806220c04(run32337765205)Adding this module moved
declined_liveby exactly +4 — its four witnesses — and movedclaimsby zero. The floor discovers this lens and declines it. It does not execute in CI.The declaration causing that is correct and stays: the lens reads
.rstext, which is host state outside its resolved substrate closure, soReadsLiveTreeis true. The required floor folds one hermetic prepared subject, so a live-tree reader cannot participate by construction.SubstrateInputsOnlywould make it eligible and would be a lie — and the enforcementlive_tree_disposition_notenames for a lying row, the nightly affected-set falsifier, died in the 2026-08-15 floor cut. That trade is not available honestly.So: the lens discriminates by execution (three arms above, each failing exactly one assertion and a different one), and nothing runs it automatically. Between manual runs it is precisely the tier DESIGN §6 names — machinery that exists while nothing gates on it. Claiming mechanically preventable would have been the inflation this PR was written against, inside the PR written against it.
This is larger than this module, and is not a gap it opened. 778 live-tree witnesses were already declined at this PR's base. The entire class of check that compares committed seed
.rstext to a.dagrow is unexecutable by the fold as architected — so the covering mechanism bothseed_mirror_notes asked for cannot be enforced by CI today, not because nobody built it but because the fold cannot run it.Next-rung trigger: an executing consumer for the declined-live population — a cadence, a dedicated non-hermetic lane, or relocating a seed-vs-row check into a phase that already reads the tree (regen or ingestion parse the seed anyway). Any of those makes this lens mechanically preventable with no change to it.
No planted control, deliberately. Four rows matched at authorship and one did not, so the discriminating RED and its positive control came from live data. A synthetic mismatch would prove only that the lens can fire; this proved the class is not hypothetical as well.
What is not claimed
That CI protects this class. It does not — see the rung section above; that question is now answered by measurement rather than left open. Enrolled, executed, and held are three axes: this module is discovered (proven, +4), not executed by the floor, and therefore not held.
How that was nearly reported wrong, since it bears on the evidence. My first check grepped the run log for the module name: zero hits. But the known-positive shows the log names no individual witness — not
host_budget_source, notv1_source_audit— only phase, heartbeat, and[floor-witness-slow](>100ms) lines, and these witnesses run in single-digit ms. That zero was an instrument that cannot express the answer, not evidence. The fact lives in thesite-projectionphase line.