Skip to content

Route the fold-lowering witnesses into the executing floor: their first execution ever was 1/15 green, and the decline was hiding rot, not parking evidence - #8818

Merged
briansrls merged 17 commits into
mainfrom
session/royal-tern-339
Aug 22, 2026
Merged

briansrls merged 17 commits into
mainfrom
session/royal-tern-339

Conversation

@briansrls

@briansrls briansrls commented Aug 21, 2026 •

Copy link
Copy Markdown
Contributor

1 of 15 of these claims passed the first time anyone ran them, and thirteen of the failures were older than the PR that added the last seven. That is the reason for this change. Routing them onto the executing floor is the mechanism; the number is the justification.

What was true before

#8801 split fold lowering's malformed arm from its not-applicable one and added seven witnesses as the split's evidence. They were authored into module v2.test.long.fold_lowering, which the required floor DECLINES by authored module name (v2.workflow.required_floor long_home_prefixes). Proven from both directions by one number: main run 32515441229 reported declined_long=551; the branch carrying them reported 558. Discovery reaches them. They do not run.

What the first execution said

Measured with claim_batch against the long entry as it stood on main: 1 of 15 PASS. Thirteen died with no field 'kind' on type 'NormalizedTree'; one returned false.

So these claims were not parked-but-fine. They were RED, and had been since #8256 (BL-1) sealed NormalizedTree behind an admission door — the alias they were written against became a record, every consumer that mattered was updated, and this file was not, because nothing runs it.

A declined home does not freeze a witness's verdict. It freezes the last time anyone knew it. The decline was not parking working evidence; it was hiding rot, and the rot was invisible precisely because the mechanism that would have shown it was the mechanism that was switched off.

Three defects, all in the witness, none in the subject

  1. ingest returned the sealed carrier where a Node was wanted. Projecting .root clears the runtime error.

  2. ingest ran normalize between parse and the locate. Measured both ways on the same snippet: WITH normalize the well-formed fold reaches fold_call_lowering as FoldCallNotAFold and ^fold is not among the tree's atom identities at all; WITHOUT it, FoldCallLowered. v2.compiler.fold_lowering's own contract says its input is the surface ^dag_surface_primary_expr capture, read via ^grammar_sequence_left_node_projection — normalize's output is past that seam. The witness was handing the desugaring an input from the wrong side of it, and the refusal it produced was correct. The ingest now stops where the subject's input lives.

  3. A binder destructured from a GENERIC coproduct is usable in ARGUMENT position but not as the receiver of a field projection. l.children off Present { value: l } of Optional<Node> fails with error type cascade at the projection, while four sibling claims pass using the same binder as an argument. This is a v2 inference deficit, not a fact about these claims. It is now filed as gunbc.generic_binder_field_projection_deficit — invalid state, harm, rung found at (mitigatable), ceiling (structurally impossible; the class is decidable and unbuilt), next-rung trigger, and the two located sites — and named in an annotation at each site whose shape it dictates. The projection is performed where the type is concrete (a Node parameter); both claims assert exactly what they asserted before, and the helpers dissolve when the deficit closes.

The home

The routed home already existed: src/v2/test/claim/fold_lowering_test.dag, module v2.test.claim.fold_lowering, one unit claim over the same subject. This merges into it rather than minting a third name for one concept (DESIGN.md §3).

An explicit import block in a witness entry REPLACES the ambient witness pool rather than adding to it. Measured: with that file's two import rows present, every end-to-end claim fails no such function: tokenize. The rows are removed, not relocated; the one claim that used them still passes without them. That is a statement about how import blocks behave in witness entries, not a note about this file.

Result

16 of 16 PASS, measured in one claim_batch process (the 15 plus the unit claim already in the routed home).

Per-claim cost 1231–2209ms CPU, median ~1340ms, against the floor's enforced required_floor_claim_cpu_safety_limit_ms=5000 and required_floor_claim_wall_safety_limit_ms=10000. One row (2209ms) sits over required_floor_claim_cost_line_ms=1552, which is diagnostic only and refuses nothing. Nothing here approaches an admission limit.

Separately worth a line, because it is the class DESIGN.md keeps correcting itself for: required_floor.dag's prose still narrates a 500ms hard / 100ms warn tier pair. Those are stale narrative, not the values the host reads — the host reads the three functions above. Not changed here, flagged as found.

The floor's declined_long should fall by 15 and its routed population rise by 15.

Secondary effect

The FrozenPathDeferral row naming the departed entry and its 8 pre-existing functions is deleted with it. That roster counts witnesses admitted with no executing consumer, and these now have one — so the frozen population goes DOWN by one entry rather than up, which is the direction a freeze carrier is supposed to move.

🤖 Generated with Claude Code

Brian Searls and others added 15 commits August 21, 2026 21:06
…r the three defects their first execution found

#8801 landed a correct-looking split of fold lowering's malformed arm from its
not-applicable one, with seven new witnesses as its evidence. Those witnesses
were authored into module v2.test.long.fold_lowering, which the required floor
DECLINES by authored module name (v2.workflow.required_floor
long_home_prefixes). Proven from both directions by one number: main run
32515441229 reported declined_long=551, the branch carrying them reported 558.
Discovery reaches them; they do not run. That is DESIGN.md §5's
specification-without-execution exactly -- a repair whose discriminating RED has
no consumer.

WHAT THE FIRST EXECUTION SAID, and it is the whole reason this is a repair and
not a move. Measured on BuildBuddy via claim_batch against the long entry as it
stood on main: 1 of 15 claims passed. Thirteen died with `no field 'kind' on
type 'NormalizedTree'` and one returned false. So these claims were not merely
unexecuted -- they were RED, and had been since #8256 (BL-1) sealed
NormalizedTree behind an admission door. The alias they were authored against
became a record, every consumer that mattered was updated, and this file was not,
because nothing runs it. The decline did not park working evidence; it hid rot.

Three defects, each measured, none of them in the subject:

1. `ingest` returned the sealed carrier where a Node was wanted. Projecting
   `.root` clears the runtime error.

2. `ingest` ran `normalize` between parse and the locate. With normalize in the
   chain the well-formed fold reaches fold_call_lowering as FoldCallNotAFold and
   ^fold is not among the tree's atom identities at all; with the chain stopped
   at parse it reaches FoldCallLowered. v2.compiler.fold_lowering's own contract
   says its input is the surface `^dag_surface_primary_expr` capture and that it
   reads the callee by `^grammar_sequence_left_node_projection` -- normalize's
   output is past that seam, so the witness was handing the desugaring an input
   from the wrong side of it and the refusal was correct. The ingest now stops
   where the subject's input lives.

3. Two claims project `.children` off a binder destructured from a GENERIC
   coproduct (`Present { value: l }` of `Optional<Node>`). That fails with `error
   type cascade` at the projection, while four sibling claims pass using the same
   binder in ARGUMENT position. This is a v2 inference deficit, not a fact about
   these claims: it is named in an annotation at the site whose shape it dictates,
   the projection is performed where the type is concrete (a `Node` parameter),
   and both claims assert exactly what they asserted before.

THE HOME. The routed home already existed -- src/v2/test/claim/fold_lowering_test.dag,
module v2.test.claim.fold_lowering, one unit claim over the same subject -- so
this merges into it rather than minting a third name for one concept (§3). Its
two import rows are REMOVED, not relocated: measured, an explicit import block
replaces the ambient witness pool rather than adding to it, and with those rows
present every end-to-end claim fails with `no such function: tokenize`. The one
claim that used them still passes without them.

RESULT: 16 of 16 PASS, measured in one claim_batch process. Per-claim cost
1231-2209ms CPU (median ~1340ms), against the floor's enforced
required_floor_claim_cpu_safety_limit_ms=5000 and
required_floor_claim_wall_safety_limit_ms=10000; one row (2209ms) sits over the
DIAGNOSTIC required_floor_claim_cost_line_ms=1552, which reports and does not
refuse. Nothing here approaches an admission limit. The floor's declined_long
should fall by 15 and its routed population rise by 15.

The FrozenPathDeferral row naming the departed entry and its 8 pre-existing
functions is deleted with it: that roster counts witnesses admitted with no
executing consumer, and these now have one.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title WITNESS EXECUTION COVERAGE (zesty-carp-454 archived mid-lane, three findings stranded). #8801 MERGED with 7 new witnesses in module v2.test.long.fold_lowering, a DECLINED home - proven from both directions by one number, declined_long 551->558, which shows discovery REACHES them and they DO NOT RUN. Route the fold-lowering witnesses into the executing floor: their first execution ever was 1/15 green, and the decline was hiding rot, not parking evidence Aug 21, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 21, 2026 22:53
@briansrls
briansrls merged commit aecb1fe into main Aug 22, 2026
1 check passed
@briansrls
briansrls deleted the session/royal-tern-339 branch August 22, 2026 00:37
briansrls pushed a commit that referenced this pull request Aug 22, 2026
…s, and says so: a declared rung drop the floor cut owed and did not file (#8832)

gunbc.witness_deferral_freeze states a forward rule verbatim: "a new or
relocated witness under any OfflineLocalRecipe path must carry an exact
admission naming an executing cadence". That sentence was true when written and
is not satisfiable today. This adds the DESIGN.md §4b(3) declared row for it and
leaves the rule standing above, because what changed is not the rule's intent
but the world underneath it.

WHY IT IS UNSATISFIABLE. explicit_witness_admission_cadence_executes admits five
cadences. Four no longer execute anything: FalsifierSelfHostWet,
FalsifierRehomedBinWet and FalsifierSubstrateLongLane died with falsifier.yml at
611fd02 (#8283, the floor cut) -- gunbc.ci_layer_roots records that
"falsifier batch 2 no longer executes anything" -- and BinWitnessWet died with
the per-PR wet job in ci.yml in the same cut, which excl_bin_wet_reason states
for the whole class. The fifth, QuarantineProbeExpectRed, executes on the floor
but answers a different question: it declares a witness RED, and cannot be
written truthfully about a green one. So the only compliant moves for a green
witness under an offline home are to declare it expected-red, which is a lie, or
not to author there.

WHY NOTHING REFUSED WHEN THE RULE WAS BROKEN. The refusal exists and is well
written: v1_compiler.cli_run refuse_unexecuted_deferred_witnesses produces
UnclassifiedPathDeferral and says in its own text that moving a file under a
long/ or offline path "executes it NOWHERE". It has ONE caller,
run_discovery_corpus_with_options_inner -- the discovery-corpus batch path.
claim_executor --required-ci runs three phases, parse / regen / floor, and the
floor does its own site projection instead. No workflow invokes a batch or plan
mode. The host that would have refused is unreachable from every required run.
That is why the breakage could rot invisibly, and it is the same shape as the
rot #8818 found one level down: the rule's verdict froze at the last time
anyone could satisfy it.

The row is LostAsPassenger, not DeletedWithoutReplacement: nothing deleted the
rule, the cut deleted the cadences it names and the mode that enforces it. Its
restoration trigger carries both halves for the same reason -- re-adding one
falsifier cadence restores one door and not the refusal.

EVIDENCE GRADE, carried in the annotation rather than only here because two of
the three claims are about absences: the cadence standing is read from the
corpus's own recorded corrections; the reach argument is a source read of the
caller set, the phase banners, and .github/workflows holding three files. NO
EXECUTION was attempted against the discovery-corpus path. The row does not
establish behaviour under a mode nobody ran; it establishes that no required run
enters it, and a fourth workflow can make that half false with nobody having
touched the row.

Nothing here relaxes the rule. Unsatisfiability is not permission any more than
detection failure is: the answer for a green witness under an offline home is to
route out, which is what #8818 does.

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 22, 2026
…loor failures

The floor red on 77c9121 was 16 FAILs, all in v2.test.claim.fold_lowering (12) and
v2.test.claim.body_lowering.statement_let_bind (4), every one 'non-exhaustive pattern
match on OccurrenceId'. None of it is reachable from this branch's subject -- the diff
touches the systemd unit-file grammar and the build-cache renderers.

Diagnosed rather than assumed: main was GREEN at the same head class, and the two
failing families map exactly to two commits this branch did not contain -- #8818, which
routed the fold-lowering witnesses out of long/ and into the executing floor, and #8828,
which is the statement-form let lowering. This branch carried the test files at their
pre-#8818 home while the merged main-side routing executed them, so it ran witnesses
against a compiler half a lane behind them.

The remedy is the merge, not an edit: no file of mine is implicated, and the merge is
clean (#8818 deletes src/v2/test/claim/long/fold_lowering_test.dag outright).

Re-verified after merging: build_cache_ensure witness green, my grammar and renderer
changes intact, no body-level annotation in the diff.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Aug 22, 2026
…on family (#8827)

* Build-cache vertical: the systemd unit becomes a modeled value, not INI text gunbc spells itself

gunbc.build_cache_unit hand-concatenated "[Unit]", "[Service]", "Environment=..."
and "WantedBy=..." as string literals, which made gunbc a SECOND AUTHORITY for
systemd's unit-file syntax beside extdeps.systemd.unit_file -- the §3 nicknaming
that module's own header says it exists to prevent. Its systemd_medium_as_string_note
declared the debt and named the wrong exit: the dissolve-on pointed at
extdeps.languages, while the grammar had already landed at extdeps.systemd.unit_file.
The trigger had effectively fired and nothing noticed.

extdeps.systemd.unit_file grows the directives this consumer needs, each cited:
Before=/Requires= in [Unit] (systemd.unit(5), already in scope) and Slice= plus a
[Slice] section with MemoryMax=/MemoryHigh= (systemd.resource-control(5), a scope
the module did not previously cite and now does). SliceUnitFile joins the unit-type
coproduct, so a [Service] in a slice stays unwritable.

Drop-ins get their own type rather than a unit file with empty sections: a fragment
has no unit type, so SystemdDropIn is a LIST of known sections -- absence is absence
from the list, and an empty [Service] stays distinct from no [Service] at all.

The line view and the bytes are now one assembly read at two grains
(systemd_unit_file_lines / serialize_systemd_unit_file), which is what let the
build-cache render drop its own List<String> renderer instead of keeping one to
serve consumers that want lines.

The admissions stop carrying rendered text. EnsureBuildCacheAdmitted carried
unit_lines: List<String> and EnsureCompilePoolAdmitted carried slice_lines --
a decision type holding a serialized artifact of one realization. Both now carry
the modeled unit value, so bytes are produced by the single serializer at the
moment of writing rather than frozen into the decision.

NO HOST BYTES CHANGE, measured rather than reasoned. An earlier draft declared a
one-byte behavioural change (a trailing newline); that was wrong -- the heredoc
already supplied it. build_cache_ensure_daemon_body was rendered on this tree and
on origin/main with one compiler, for the CI instance (absent capacity) and the
session instance (present capacity), byte-identical both times, with a control
confirming the two trees genuinely differ. The write site concatenates the heredoc
terminator rather than joining it, which is what keeps that true.

95 witnesses across the six affected claim modules pass. Six new witnesses cover
the added grammar, including exact bytes for a slice unit and the empty-vs-absent
drop-in section. Three mutations were executed against the new walls -- a wrong
MemoryHigh spelling, a line view that stops sharing the serializer's assembly, and
a drop-in that always emits [Unit] -- each producing targeted reds.

Does NOT wire realize_provision_build_cache onto the admission; that stays open and
is zesty-wolf-464's lane on #8825.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Move the heredoc rationale to module-item grain: a body-level // refuses at the floor

CI's floor phase refused this branch with four typed, located diagnostics --
"source annotation sits inside a declaration body. Only module-item grain is
modeled" -- against the four-line comment I put inside build_cache_ensure_daemon_body's
list literal. DESIGN section 4c says exactly this: the .dag realization admits only
standalone leading // blocks attached to module-scope declarations, and body,
trailing, unattached and block-comment forms refuse until separately modeled.

The rationale is unchanged in substance and now sits above the declaration it
describes, which is where section 4c puts it.

WHY IT WAS NOT CAUGHT LOCALLY, recorded because the next person will reach for the
same tool: `gunbc run` is eval-only and never applies the annotation-grain gate, so
all 95 witnesses passed over source the floor refuses. `gunbc compile` is the strict
path, but a whole-corpus compile does not finish inside a single local window
(reconcile alone is 8-10 minutes, and the attempt timed out mid-emit), so the
known-positive probe for the gate was INCONCLUSIVE rather than green -- stated that
way rather than as a local check that passed.

What was actually verified before pushing is narrower and is the decidable proxy for
this class: the diff carries no indented // anywhere, checked mechanically across all
seven changed files. That is a syntactic property, not a run of the gate, and CI
remains the authority.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Merge origin/main: pick up #8818/#8828, whose witnesses were the 16 floor failures

The floor red on 77c9121 was 16 FAILs, all in v2.test.claim.fold_lowering (12) and
v2.test.claim.body_lowering.statement_let_bind (4), every one 'non-exhaustive pattern
match on OccurrenceId'. None of it is reachable from this branch's subject -- the diff
touches the systemd unit-file grammar and the build-cache renderers.

Diagnosed rather than assumed: main was GREEN at the same head class, and the two
failing families map exactly to two commits this branch did not contain -- #8818, which
routed the fold-lowering witnesses out of long/ and into the executing floor, and #8828,
which is the statement-form let lowering. This branch carried the test files at their
pre-#8818 home while the merged main-side routing executed them, so it ran witnesses
against a compiler half a lane behind them.

The remedy is the merge, not an edit: no file of mine is implicated, and the merge is
clean (#8818 deletes src/v2/test/claim/long/fold_lowering_test.dag outright).

Re-verified after merging: build_cache_ensure witness green, my grammar and renderer
changes intact, no body-level annotation in the diff.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

* Delete two _text projections that never gained a consumer

runner_ordering_drop_in_text and compile_pool_slice_text were authored as the
natural peers of their _lines projections and nothing ever called them -- not
in this module, not in the tests, not in the realize path. Under DESIGN §6
that is "a new artifact with no final consumer", and the honest fix is a
deletion rather than a note explaining why the surface exists.

The _lines peers stay: render_compile_pool_slice reaches compile_pool_ensure's
admission and runner_ordering_dropin_lines reaches the tests. build_cache_unit_text
stays: host_effect_realize writes it into the heredoc. serialize_systemd_drop_in
stays in the grammar module -- its byte-exact witnesses consume it -- and only
this module's now-unused import of it is dropped.

Found by review 54749 on #8827.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant