Skip to content

HealthzEffectiveRead becomes the coproduct it always was; the rung is measured, not claimed - #8655

Merged
briansrls merged 26 commits into
mainfrom
session/sharp-ant-396-argv2
Aug 20, 2026
Merged

briansrls merged 26 commits into
mainfrom
session/sharp-ant-396-argv2

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 20, 2026

Copy link
Copy Markdown
Contributor

HealthzEffectiveRead was { body: String, probe_error: String }. All 20 constructions set exactly one field — never both, because there is no such observation: a probe either landed and produced a body, or it refused and produced a reason. The empty string was doing the work of a tag, in a type that also admits the empty string as a legitimate body.

type HealthzEffectiveRead
  = HealthzBodyRead    { body: String }
  | HealthzProbeRefused { probe_error: String }

Every construction mapped mechanically to one variant — no site required interpreting what its author meant.

The rung, probed in both directions

I did not assert a rung. I wrote two probes and ran them.

Field access is structural. A probe reaching read.body off a refusal made the floor refuse during preparation:

required-floor: refused: subject=a6a0c917... modules_resolved=3729 modules_excluded=4
readiness_witness_test.dag:285:7: error: no field 'body' on type 'HealthzEffectiveRead'

Located, typed, before a single witness executed. Broader than the headline claim, too: the carrier has no fields at the type level, so every field-access route into it is gone.

The bare record literal is not. A literal naming the coproduct with no variant tag still resolves and still constructs; it is refused only at the match, at evaluation:

required-floor: FAIL ...probe_contradictory_healthz_read_is_constructible_today errored:
  non-exhaustive pattern match on: HealthzEffectiveRead { body: {"status":"ok"}, probe_error: curl: (7) ... }

Measured, not inferred: that probe passed pre-change (planned=9784 failed=0) and became a per-witness runtime FAIL post-change with the corpus fully executed — not a preparation refusal.

So the construction half sits at mechanically preventable, not structurally impossible, and the declaration says so. Next-rung trigger is a compiler capability, named on the carrier: a record literal naming a coproduct type with no variant tag should refuse at resolve, where field access already does. Claiming the state was unwritable would have been the §4b rung inflation that is worse than sitting low.

What did not climb

readiness_check_order_note documented five ordered stages. PROBE left it — not because it moved earlier, but because it is no longer ordered by anything. The other four (PARSE, IDENTITY, REVISION, SURFACE) remain ordering-by-discipline inside the new ground_service_ready_from_healthz_body, and the note now names the four that remain and says why it still has work to do.

Evidence

pre-change final
planned / executed 9784 9783
passed 9476 9475
known_red_held 304 304
failed 0 0

Delta is exactly the deleted probe. The 4 stale-quarantine rows are identical in both runs and inherited from main — v2.test.execution.emit_host_*, unrelated to this carrier — so they are reported, not fixed here.

One unexplained observation, stated rather than smoothed: over_cost_line_diagnostic read 6 pre-change and 22 in the final run. It is a wall-clock slow-witness warning, not a failure, and this change replaces a field access with a match — no plausible cost shape for a 3× move — so I read it as runner variance, but I have not proven that and am not claiming it.

Neither probe survives in the corpus: both are hard refusals, so neither can remain enrolled as an executing control. They are cited on the declaration by their measurement instead.

gunbc-ci-auto-heal and others added 23 commits August 19, 2026 16:55
…se while not running

Measured 2026-08-19: dag/tools carries 12 gate modules and ZERO are referenced by any
workflow. .github/workflows/ holds two files, and witnesses.yml's only executing step is
claim_executor --required-floor. tools.extdeps_scope_placement_gate calls itself a
"server-side per-PR wall" that "refuses any dag/extdeps .dag file added by THIS CHANGE";
tools.prose_row_introduction_gate opens with "THE PER-PR WALL". Neither is standing.

DESIGN is already honest about this -- its "Building & checks" section declares the
2026-08-15 floor cut as a bounded rung drop and names the effect gates among what is
unguarded until the re-add queue closes. What was never updated is the module-level
prose, and that is the copy a session actually opens. A wall described in the present
tense is a premise the next plan gets built on.

PROSE ONLY. No enforcement is re-added, no gate deleted, no roster touched. Only the
description is corrected to match the mechanism, citing DESIGN as the authority rather
than restating its contents.

tools.rust_stage0_gates was checked and needs no correction: it says per-PR execution is
"gated on #6239", which states the wall is blocked rather than asserting it stands.

RECORDED WITH IT, because it is what made the gap invisible and it generalises past these
files: THE .dag CALL GRAPH IS NOT THE EXECUTION GRAPH. Any claim of the form "this runs
in CI" is decided by .github/workflows/ and the fold those workflows invoke, never by who
calls whom in .dag. Two sessions independently traced the .dag callers of
git.Core.DiffUnified0, both concluded it was on a path CI walks every run, and both were
wrong -- agreeing was not a second observation, because both had read the same artifact.

The finding is stronger than "these two gates are dormant". In hermetic mode
eval_mock_response replays the operation RESULT off the declaration's mock_response and
never touches argv, so no argv is CONSTRUCTED in the mode CI runs. No argv defect of any
kind is observable there.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…g it

A free monoid whose elements are Strings satisfies BOTH readings at an argv position:
value_as_host_string folds it into one concatenated word (its `Value::Str(s) =>
out.push_str(&s)` arm), and free_monoid_to_vec splices it into N words. The value records
no choice between them, and push_shell_argv_tokens tried the concatenating reader first
-- so one declared List<String> produced ONE argv word when it arrived monoid-encoded and
N words when it arrived as a native list. Same type, same declaration, opposite arity,
decided by a representation the author never selected.

This is a state-space conflation, not a missing wall, which is why no branch ordering
could have been correct: "one argument whose text is the concatenation" and "N arguments"
are different states with different remedies. The position now raises a typed, located
diagnostic naming the argv index and both readings.

MEASURED SPECIMEN: extdeps.git.git git_diff_range_argv returns [base, head] on its TwoDot
arm, spliced into `git diff -U0 <range>`. Monoid-encoded that reaches the process as
`mainHEAD`. The failure is not that git errors -- on any pair whose concatenation names a
real object it produces a successful diff of the WRONG RANGE, which is fabricated
plausible output rather than a crash.

DELIBERATELY UNCHANGED: Int-element monoids stay char-decoded (unambiguous under one
reading only); native Value::List keeps its N-word expansion; ProcessArgvExpansion stays
authoritative; and value_as_host_string itself is untouched -- value_to_host_string wraps
it for general use, and narrowing a shared helper to fix one caller is the forked-logic
trap this lane exists to remove. The empty monoid keeps its current empty-string reading,
called out in-code as a deliberate narrow choice rather than left implicit.

EVIDENCE, and the RED is unit-level by necessity rather than convenience: in hermetic
mode eval_mock_response replays an operation's RESULT off its declaration and never
touches argv, so no argv is CONSTRUCTED in the mode CI runs and there is no execution to
assert against. Three assertions build the representations directly. Proven discriminating
by disabling the refusal and re-running:

  native list of two strings          -> 2 argv words   (holds both ways: control)
  monoid-encoded, refusal enabled     -> refuses
  monoid-encoded, refusal disabled    -> FAILED, argv ["mainHEAD"]
  codepoint monoid                    -> 1 word         (holds both ways: control)

NO FROZEN ROSTER, because the refusal IS the census: whatever breaks was relying on the
concatenation, and that is exactly the population worth enumerating. Each will be fixed
from first principles -- either a latent instance of this defect, or a site that genuinely
wants one word and should say so with an explicit join. No arm restoring the old behaviour
will be added for sites that complain.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…fy the REST/CLI boundary

The argv lane keeps asserting in prose that a Redfish/REST path constructs no
process invocation. Prose cannot be contradicted by the tree. This makes it a
row that reds.

NO SECOND LENS WAS MINTED. v2.lens.realization_vocabulary_containment already
answers "does module X reach construction vocabulary from set V". The obstacle
was that V was a literal: the importer-path axis was already threaded as a
parameter through scan_facts_for_leaks_under, while module_is_target_ast_vocab
was welded into the predicate. A second lens for a second V would have been the
section 3 duplication this lens exists to detect, so the vocabulary axis was
opened instead -- the section 2 horizontal move, one axis rather than N copies.

RealizationVocabularySet + module_is_in_vocab + is_vocab_leak_in /
scan_facts_for_leaks_in / vocab_leak_count_in / vocab_leak_count_live_in.
target_ast_vocabulary() DERIVES from the existing target_ast_vocab_modules and
target_ast_vocab_module_prefixes rows rather than replacing them, because
gunbc.realization_vocab_confinement_census consumes those rows directly and has
live claims against them.

THE OLD ENTRY POINTS DELEGATE, they do not keep a parallel copy. Leaving the
original fold beside the general one would have been one predicate with two
implementations -- the fork this lens detects, one level down.

The exempt population is a PARAMETER rather than a global roster read, so "this
vocabulary has zero admitted exceptions" is a stated fact instead of an accident
of the target-AST roster happening to name no CLI module.

TWO SITES LEFT TARGET-AST-ONLY, DELIBERATELY, with the reason in-file: the two
projections feeding the grandfathered-roster staleness check, whose roster rows
are target-AST debt by construction (RealizationVocabDebtClass has no other
inhabitant). A second vocabulary arrives with an empty exempt population and so
has no roster to be stale against; parameterizing them now would answer a
staleness question about a population that does not exist. Trigger recorded.

THE FALSIFIER'S SUBJECT IS NOT AN EMPTY UNIVERSE, which is how a negative claim
usually turns vacuous. dag/extdeps/bmc contains a module that legitimately
reaches this vocabulary -- openbmc_fan_control, the module this lane routes
through jq -- beside redfish.dag, which does not. So the scan discriminates
WITHIN the population, and the RED control is live corpus data rather than a
planted fixture: withdraw the one admitted edge and the count must become 1.
Without that assertion a clean result is indistinguishable from a scan that read
nothing, which is the empty-observation narrow.

The admitted edge is named at exact (importer_path, vocab_module) grain, so a
SECOND jq-reaching module anywhere in the scanned roots reds rather than being
absorbed by a pattern broad enough to cover it.

EXECUTED: all three witnesses return true, including the discrimination control
at exactly 1. The pre-existing lens witnesses (planted_leak, discriminators,
roster_soundness) return true unchanged.

SCOPE, STATED RATHER THAN IMPLIED: the witness is floor-discovered -- neither
long/-homed nor in floor_prepared_subject_exclusions -- and reads the live tree,
but only the two named directories. A module outside those roots reaching CLI
vocabulary is not seen here, and no green from this file may be read as
whole-corpus coverage. That lens's whole-corpus half is enrolled on a cadence
that does not currently run, which is a fact about the cadence rather than about
this witness.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ries its own control

The boundary was enforced in two directories and prose everywhere else. That was
the whole of its limitation, so this widens it -- one root per assertion rather
than one widened list, so a failure names the root that broke instead of
reporting that something, somewhere, reaches CLI vocabulary.

ROOTS ADDED, each landing in a stated state rather than behind one green:
  dag/extdeps entirely -- one admitted edge (the fan control jq edge, already
    named) plus the jq definition site on the edge roster. Clean otherwise.
  src/v2/{std,compiler,lens,workflow} -- ZERO admissions. The compiler substrate
    constructs no process invocation at all. If any of it ever needs a CLI
    surface, that is an architectural event and it reds here first.

A CLEAN ROOT AND AN UNREAD ROOT BOTH REPORT ZERO, and those are different states
-- bottom-as-answer against bottom-as-ignorance. Three controls separate them,
because the widened roots have no known edge to withdraw:

  vocab_scan_fact_count_live asserts each scan acquired real facts, so a zero is
  a finding rather than a silence.

  Withdrawing the admission under the WIDE root must still surface the fan
  control edge at exactly 1. A nonzero fact count proves the extdeps scan read
  something; it does NOT prove it descended into bmc/ where the only known edge
  lives, so without this "dag/extdeps is clean" could be clean because the one
  dirty subtree was never reached.

  Dropping the definition-edge roster must make the count RISE, which proves
  that roster admits a real edge rather than naming a path the scan never had a
  fact for.

THE TWO ROSTERS ARE DELIBERATELY DIFFERENT SHAPES. The jq definition site is a
PATH prefix because constructing a CLI surface is what that location is for; the
fan control admission is an EXACT (importer_path, vocab_module) pair because it
is one consumer that happens to need the vocabulary and must not silently become
two.

EXECUTED: 8 of 8 green, including all four controls.

STILL NOT COVERED, stated rather than implied: dag/gunbc carries six modules
reaching extdeps.shell.exec (the host-effect and transport layer) and dag/test
carries the witnesses that exercise this vocabulary deliberately. Neither is
added here. Whether dag/gunbc's shell reach is a realization edge or admitted
debt is a policy question about the boundary itself, not a mechanical widening,
and it is not this change's to decide.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ucture-vs-consumer

THE BOUNDARY, in the form that fails rather than the paragraph:

  Realization infrastructure may reach transport vocabulary; consumers may not,
  except by exact named admission.

#8535's prose says CLI-backed handlers are one realization cell. This says which
modules ARE that cell and refuses the rest by name.

dag/gunbc's six extdeps.shell.exec reaches are two different things, split by
what the module IS rather than by what it imports:

PATH-ROSTERED AS REALIZATION EDGES -- retained_shell_script (defines the counted
bridges, calls transport_script_seal), bash_materialized_transport (the only
other admit_callers-sealed caller of that seal), host_effect_realize (the
realization core, reaching through retained_srvn). Reaching transport vocabulary
is what these locations are FOR, which is the same reason jq's definition site is
path-rostered.

ADMITTED AS EXACT PAIRS -- package_delivery, codex_app_server_press,
provider_wire_evidence. Exact, so a SEVENTH consumer reds instead of being
absorbed by a prefix broad enough to cover it.

THE REASON ON THOSE THREE IS THE FINDING, NOT A JUSTIFICATION. All three reach
through retained_foreign, whose declared dissolves_to is the bash emitter -- the
destination for foreign executors and pre-runtime bootstrap -- while all three
appear to run inside a present gunbc runtime, which would make their real
destination typed effects. The roster records a bucket that is probably wrong
rather than laundering it, so fixing the bucket takes the admission OFF instead
of re-justifying it.

That population was reached TWICE INDEPENDENTLY: by a retained_foreign call
census and by this import-graph scan, which additionally separated out
provider_wire_evidence. Two routes landing on one set is why these are named
rather than guessed.

dag/test is path-rostered and said so: these are the witnesses that exercise this
vocabulary deliberately, including the ones proving the argv refusal itself. A
test that could not import the thing it tests would be a test of nothing. Stated
as a roster rather than left unscanned, so the exclusion is visible instead of
implied by absence.

THE GENERAL RULE, written into the file because the next person widening a root
will reach for the inherited control and it will pass while proving nothing:

  RE-ESTABLISH DISCRIMINATION AT THE NEW SCOPE. DO NOT INHERIT IT.

A narrow root's RED proves the scan discriminates over THAT root. Widen it and it
proves nothing about the new subtrees -- a nonzero fact count shows the scan read
something, not that it descended where the dirty modules live. Caught here under
a green: dag/extdeps reported clean and would have reported clean had bmc/ never
been reached at all. So every root carries, at its own scope, a withdrawal
control with an exact expected count and a roster-drop control asserting the
count RISES, the latter because an edge roster no fact matches is
indistinguishable from a correct one.

EXECUTED: 12 of 12 green, six of them controls. The gunbc withdrawal returns
exactly 3, which is what establishes the split is real rather than fitted to
produce a pass.

CONTEXT A READER NEEDS FIRST: only 13 files in the whole corpus reach CLI
construction vocabulary. The boundary was substantially intact before anyone
described it; this confirms and pins a property the tree mostly has rather than
negotiating one into existence.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…l my own edit introduced

TWO THINGS, and the second is a defect I caused and did not catch.

1. shell.Exec.RunArgv -- the local process-argv execution seam.

Run is argv ["bash", "-s"] with the script on stdin, so every local ArgvCommand
in the corpus renders its argv to quoted TEXT and hands it to a shell that parses
it back into an argument vector. The seed does Command::new(&argv[0]) at the far
end regardless, so the round trip buys nothing and costs exactly what
argv-as-serialization exists to stop: a re-parse where argument boundaries are
inferred from text instead of carried.

THE PROGRAM IS A SEPARATE INPUT, not the first element of the expansion. execve
takes the executable and the argument vector as distinct parameters, and with the
program separate as NonEmptyStr an EMPTY argv becomes unconstructible -- the
unspawnable empty vector has no representation rather than being refused after
the fact.

NO success: Bool FIELD. `success` is not an observation, it is a POLICY judgement
about one -- jq exits 4 to mean "no output" and 1 to mean "false result", neither
of which is failure. A Bool beside stdout makes every caller re-derive that from
a field that already discarded the information, and lets a refusal read as empty
output. So the wire carries the honest triple and the typed outcome is decoded
immediately above it against a caller-declared policy.

THAT DECODER IS NOT NEW VOCABULARY. It is the pattern already landed for jq
(jq_classify_observation / JqExitPolicy / JqOutcome), so ProcessOutcome and
ProcessExitPolicy generalize it and the module records what is owed: jq's types
are the specialization, its 4-means-absent rule is the missing third policy
variant, and they dissolve into these on the first migrated consumer. Named
rather than left to be discovered, and deliberately not done here -- jq's
classifier is landed and consumed, so folding it in belongs with the migration
that motivates it.

Local only, per the standing constraint: no SSH arm. command_over_transport's
SshExec prefix-append stays where it is.

2. THE REFUSAL I INTRODUCED. Adding the operation left two block comments
trailing at end-of-file with no declaration after them -- in the witness, and in
exec.dag, where deleting a `data ... : String` prose row (correctly, per section
4c) orphaned the annotation that had described it. Source annotations attach to a
FOLLOWING module item; a trailing block names no subject and the substrate
refuses it. Both moved above the declarations they govern, and every .dag this
branch touches swept for a trailing `//`.

WHY 12 OF 12 GREEN DID NOT CATCH IT, which is the part worth carrying: `gunbc run
--function` accepted the file the floor refused. The two paths do not agree on
annotation validation, so a per-function green is not evidence that the floor
will prepare the same file. My verification loop was reading the weaker path and
reporting it as though it were the stronger one.

The witness assertions themselves are unaffected and still green, including the
new definition-edge roster entry -- which exists because THIS change tripped the
falsifier: exec.dag reaching cli_surface is a CLI-vocabulary edge inside
dag/extdeps, a root the witness asserts is clean. The module is itself a member
of cli_process_vocab_modules, so the reach is vocabulary-internal, on the same
footing as jq's module. A roster entry added because a real scan refused is a
different thing from one added in anticipation, and the file says so.

CI is the verifying consumer for the annotation fix: the refusal reproduces on
the floor's preparation path, which is not reachable from any local invocation I
could find, so I am not claiming a local green I did not get.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…d inside declaration bodies

Second refusal from the same root cause, and the constraint is stated in DESIGN
section 4c rather than being discovered here: the .dag realization admits only
standalone leading // blocks attached to MODULE-SCOPE declarations. Trailing,
body, unattached and block-comment forms refuse until separately modeled.

I wrote the seam's rationale inside the operation body, which is body grain, so
every one of those lines refused. Moved to one consolidated module-scope block
above the service declaration -- which is also why the pre-existing operations in
this file carry their notes as module-scope rows rather than inline: the language
has never admitted the inline form, and I should have read that as the constraint
it is instead of as a stylistic accident.

Also fixed a comment inside a list literal in the witness. My first sweep counted
brace depth and missed it, because a list body is bracket-delimited; the sweep
now counts both and the branch is clean under it.

NOTHING SEMANTIC CHANGED IN THIS COMMIT. The operation, its inputs, its output
shape and the decoder are byte-identical in meaning to the previous commit; only
the position of prose moved. Recorded explicitly so the next reader does not have
to diff it to find out whether the seam was redesigned under cover of a
formatting fix.

WHAT THIS COST AND WHY IT RECURRED: I pushed the first annotation fix without
local verification, saying CI was the verifying consumer because the refusal is
raised on the floor's preparation path and gunbc run --function does not raise
it. That was honest but it was also one class at a time -- I fixed the trailing
form, pushed, and only then learned the body form refuses too, because CI reports
the first failing class and stops being informative about the rest. Reading
section 4c's own sentence would have given me both forms at once, and a sweep
derived from the RULE rather than from the error message is what I should have
run the first time.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…d inert

THE CLASS. admit_callers is the repository's construction wall -- a declaration
names who may call it, and anyone else is refused. On a fn it works. On a service
operation the same syntax PARSES, RESOLVES CLEAN, and DOES NOTHING.

WHY THAT IS WORSE THAN THE WALL BEING ABSENT. An absent wall is visible: you look,
find nothing, and know where you stand. This one is invisible while reading as
present -- an author seals an operation, a reviewer reads the roster as a
boundary, and it admits everyone. It is the inert-lens failure at CONSTRUCTION
grain, which is the worst place for it, because a construction refusal is the rung
people stop checking behind. Measured evidence that the illusion works: I was one
step from reporting "the wall is available" after watching the declaration parse,
and the reviewing session says it would have believed me.

TWO INDEPENDENT ROUTES, deliberately not two readings of one artifact. BY
EXECUTION: admit_callers added to the real shell.Exec.Run naming only
gunbc.command_runner, after which the unadmitted gunbc.package_delivery -- which
calls Run five times -- resolved byte-identically to the unsealed baseline
captured first. BY SOURCE (the other session, independently): enforcement lives at
exactly one seed site, gated on an exact-constructor-declaration lookup reading
the fn admission list; an operation invocation is not a constructor-declaration
lookup, so it never reaches that arm, and no operation-call analogue exists.

BLAST RADIUS TODAY: ZERO. No operation in the corpus carries admit_callers -- all
21 occurrences across dag/ and src/v2/ attach to a fn or a sealed type. So this is
a LATENT TRAP, not a live hole, and the distinction is stated because the first
author to reach for it is the one who gets hurt and will have no reason to doubt
it.

THE PAIR IS ONE ARTIFACT, which is the point rather than a convenience. The
positive control (fn form refuses, green today) and the finding (operation form
does not, red today) run through one invocation over sources compiled as DATA via
the guarantee probe corpus. Split into two files they would be two observations;
together they are a discrimination, and the discrimination is the finding. Without
the control, a red could equally mean the mechanism is inert or that this file
cannot compile a probe at all -- different states, different remedies. Compiling
the sources as data is also what makes the pair possible: a refusal here is a
resolve error, so an unadmitted call written directly into this module would take
the whole file down with it.

EXECUTED: fn form returns true, operation form returns false, same file, same run.

ENROLLED AS KNOWN-RED rather than left to fail. A bare red takes the floor down
and gets triaged as breakage by someone who does not know why it is there. Per
DESIGN 4b it does NOT get deleted when the resolver gains operation-grain
enforcement -- it flips to a permanent regression control, because deleting the
evidence on the climb recreates specification-without-execution one rung up. The
roster's own coherence witness passes with the identity added.

RUNG, HONESTLY: not mitigatable but BELOW it, because no mitigation occurs --
nothing refuses, nothing counts, nothing is logged. Attainable ceiling:
structurally guaranteed, since the class is decidable and fully modeled and only
implementation stands between here and there. NEXT-RUNG TRIGGER: an
operation-grain construction refusal exists, verified by a correctly-imported
unadmitted caller. The trigger is stated in its VERIFIED form because its first
two attempted verifications were inconclusive for reasons unrelated to the seal --
a missing import, then a fixture whose service did not resolve at all. A trigger
already mis-measured twice should carry how to measure it.

NOT FIXED HERE. The resolver change is substrate work with its own owner and its
own review bar; routing around the defect or following it into infer would both be
the wrong move from this lane.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…10s ceiling

CI caught a cost defect in my own control, and the floor's summary is what
identified it: failed=0, known_red_held=307 (my expected-red enrollment took,
306 -> 307), and completed_over_cost_requirement=1. Nothing was broken; one
witness was too expensive.

THE ROW: fn_form_admission_refuses_unadmitted_caller took 54940ms against the
floor's 10000ms per-witness ceiling and grew RSS by 0.99GB. Its forged source
imported extdeps.shell.exec to reach transport_script_seal, so compiling it
dragged the whole shell/extdeps closure through the diagnostic census. The
operation-form probe beside it cost 516ms for exactly the inverse reason: it
imports only std.types.

THE FIX is to change the control's SUBJECT, not to raise a ceiling or split the
file. test.fixture.sole_constructor_sealed.definer exists precisely to exercise
caller admission on a minimal closure -- it is the fixture the corpus already
uses for this mechanism -- so the control now forges an unadmitted caller of
mint_sealed_local. Same mechanism, same refusal class, two orders of magnitude
less work, and it moves the control off a production module it never needed to
depend on.

DISCRIMINATION RE-VERIFIED AFTER THE CHANGE, not assumed from it: fn form returns
true, operation form returns false. A cheaper control that stopped discriminating
would be worse than the expensive one.

WHAT I COULD NOT MEASURE LOCALLY, said rather than implied: every gunbc run pays
a whole-corpus typecheck, so both probes report ~58s wall from this session and
the witness-level cost the floor meters is invisible from here. The 54.9s and
516ms figures are the floor's own per-witness numbers, and CI is what will
confirm the retarget landed under the ceiling. I am not claiming a local
measurement I did not get.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ound-tripping through a shell

THE CHAIN THAT IS NOW GONE from the local arm: render the argv to quoted text,
wrap it in a bash heredoc, hand it to a shell, let the shell split it back into
an argument vector -- to reach a seed that ends in
Command::new(argv[0]).args(argv[1..]) regardless. Every step existed only to undo
the step before it. On LocalExec command_over_transport is the IDENTITY, so the
render had nothing to transform either. Deleted from that path rather than
routed around.

MEASURED FIRST, because the assignment's census was stale by construction: 22
live call sites across 5 modules (not 25 across 6), 17 of them
run_shell_command_capture. ALL 22 PASS LocalExec -- zero use SshExec -- so the
entire live population moves in this cut. The callers are untouched: the change
is internal to command_runner and both signatures are preserved.

THE ONE ENABLER, and it is the part worth reviewing hardest.
ArgvCommand.argv is a runtime List<String>; CliSurface is sole_constructor and
its only construction route is through CliArgumentSyntax fragments, which carry
declared token classes and bindings. Fragments structurally CANNOT express a word
that does not exist until the program runs -- a filesystem path, a hostname. So
cli_surface_of_literal_words was added to v2.std.compilers.cli_surface.

WHY THAT IS NOT THE AMBIGUITY THE CARRIER EXISTS TO CLOSE: the refused state is a
List<String> arriving at an argv position with NO declared role, where "one word
whose text is the concatenation" and "N separate words" are both well-formed and
the realization must guess. This constructor IS the declaration -- its name says
each element is exactly one argv word. It is the same resolution the interpreter
refusal I landed earlier tells authors to reach for. The file states what it does
not license: an argument whose spelling is known at authoring time belongs in
fragments, and reaching for this instead is modeling debt.

EMPTY ARGV REFUSES rather than defaulting -- a command with no words names no
program, and inventing one is fabricated output.

THE SSH ARM IS UNTOUCHED, deliberately. Its prefix-append shape is wrong in kind
(RFC 4254 carries one string, so the inner command is a nested serialization
target, not a concatenation) and that target belongs to another lane. Two sessions
editing one contested branch is worse than either fix. It also carries no traffic
through this module today, which is why leaving it cost nothing.

THE success FIELD is derived through a NAMED policy --
process_exit_is_admitted(ExitZeroSucceeds) -- rather than a bare exit_code == 0,
so the convention this runner applies is something a caller can change rather
than a literal to discover.

WHAT STILL COLLAPSES, named and not fixed here: "ran and exited nonzero" and
"could not be executed at all" both arrive as success: false. Under the old bash
hop those were genuinely indistinguishable -- a missing binary became the shell's
exit 127, which claims a process ran when it never existed. Going direct removes
the shell that fabricated that code, so the distinction is now AVAILABLE at the
transport even though ShellCaptureResult cannot express it. Not repaired in this
cut because it is not free: 17 call sites read that record and the destination is
the ProcessOutcome coproduct one module away, so the repair belongs with the
sites it changes.

THE DISCRIMINATING RECEIPT, executed wet against a real process:

  argv ["printf", "%s|", "a b"]
  direct exec -> one operand "a b" -> stdout "a b|"    OBSERVED
  via a shell -> two operands     -> stdout "a|b|"     asserted absent

All three assertions pass. A green that would still be green with the bash hop
restored would prove nothing about what changed, which is why the subject is an
argument the two paths DISAGREE about rather than a command that merely succeeds.

IT IS WET AND EXCLUDED, for a reason that is structural rather than convenient:
hermetic evaluation replays an operation's declared mock_response and never
constructs an argv at all, so "the words reached the process unsplit" is not
observable hermetically. A hermetic version could only assert the mock, which is
specification-without-execution. Excluded exactly as the prior argv receipt is,
and the file says so.

DIVERGENCE FROM THE RECORDED TRIGGER, stated rather than left for a reader to
notice: command_runner_dissolution_trigger names host_effect_apply binding
ArgvCommand execution as a typed transport handler. This cut routes command_runner
directly at shell.Exec.RunArgv instead. The trigger's second clause -- retire the
shell_exec_via_bash glue -- is satisfied for the local arm and NOT for the SSH
arm, so the trigger is not yet discharged and I have left it in place rather than
claiming it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…s not guard; correct the trigger

Three review items, all taken. The first is the one that mattered and my
semantic defence of it was insufficient.

1. THE MINT IS NOW admit_callers-RESTRICTED. My argument was that a constructor
whose name says "each element is one argv word" IS the declaration the refused
state lacks, and that stands -- but the declaration was UNBOUNDED. Anyone could
make it, about anything, which left the interpreter's argv refusal one import
away from being routed around: not defeated, just satisfied by an intent nobody
checked was true. Nominal wall, not structural.

The admitted population is TWO -- run_shell_command and run_shell_command_capture
-- which is what makes the restriction honest rather than aspirational. A third
caller is an edit to the list in the declaring module: a counted review event
rather than an import written elsewhere.

VERIFIED BY EXECUTION, with a discriminating RED rather than by reading the
declaration -- which matters more than usual here, because I spent this session
proving that this exact mechanism is ACCEPTED AND INERT at operation grain. An
unadmitted module calling it is refused:

  constructor call admission refused:
  'v2.std.compilers.cli_surface.cli_surface_of_literal_words' refuses call from
  'test.fixture.mint_admit_probe.intruder.unadmitted_mint' — permitted callers:
  [gunbc.command_runner.run_shell_command,
   gunbc.command_runner.run_shell_command_capture]

Located, names the caller, lists the roster. The admitted callers still work: the
wet receipt passes unchanged. This is a fn, which is the grain where the
mechanism is verified to fire.

The file's note that authoring-time spelling belongs in fragments carries no
enforcement, and now says so rather than reading as a wall.

2. WHAT GUARDS THIS CUT, AND WHAT DOES NOT, written where the next author stands.
The property "the local path reaches no shell" is established wet and the receipt
is FLOOR-EXCLUDED, so CI does not run it and someone reintroducing a
render-and-bash hop gets no signal. The exclusion is structural -- hermetic
evaluation replays mock_response and never constructs an argv, so a hermetic
version could only assert the mock -- but the consequence is a real gap and the
module now states it: rung mitigatable, next-rung trigger a wet lane that
executes floor-excluded receipts. A green test that nothing runs is exactly the
inert evidence DESIGN calls a lie, and the file should not read as enforced.

3. THE TRIGGER NAMED A MODULE THAT WAS NEVER BUILT. Asked whether I had created
PARALLEL AUTHORITY rather than whether I matched wording, I measured: there is no
host_effect_apply production module (it exists only as a witness test), and
host_effect_realize never mentions ArgvCommand. command_runner is the ONLY module
that turns an ArgvCommand into a local process. The other ArgvCommand consumers
reach shell_command_render, which serializes argv into TEXT for emission
(githooks) or for the SSH leg -- a different destination, not a second local-exec
route.

So this did not diverge from the trigger; it satisfied a better version of one
that named a binding nobody wrote, and satisfying it literally would have meant
building the second route DESIGN forbids. The row is rewritten to name the
condition that actually remains: the SSH arm, which needs the nested
command-string target another lane owns, and at which point shell_exec_via_bash
and retained_runtime leave this module entirely.

Also fixed in passing: my own trigger rewrite wrote a \\U escape into the .dag
string instead of the literal character, which made the module unparseable. Caught
by resolving the file rather than by reading the diff.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ply exists

The conclusion was right and one clause of its evidence was false, which is worse
than usual here because it sits in a REPLACEMENT trigger -- the row exists to stop
the next author re-deriving the question, and a false premise makes them do it
anyway.

WHAT I WROTE: no host_effect_apply production module exists, witness test only.
WHY I GOT IT WRONG: I searched for a FILE named host_effect_apply*.dag and found
only the witness test. It is a FUNCTION. gunbc.host_effect_realize declares
host_effect_apply and host_effect_apply_gated and both are production. That is the
third scope error of this session in one family -- a limited view read as the
population -- and the specific lesson is narrower than the earlier two: searching
for a filename does not answer a question about a symbol.

WHAT ACTUALLY CARRIES THE ARGUMENT, verified independently rather than taken from
the correction: host_effect_realize contains ZERO occurrences of ArgvCommand and
does not appear among that type's consumers. So host_effect_apply exists and
dispatches effects, but it never reaches an ArgvCommand and is therefore not a
second route from an ArgvCommand to a process. command_runner remains the sole
one, there is no parallel authority, and satisfying the original trigger literally
would still have meant BUILDING the second route rather than finding it.

The row now says that, and records the correction in place rather than quietly
overwriting it, so a reader who saw the earlier claim learns it was wrong instead
of wondering which revision to believe.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
THE CONFLATION, corrected from how we first described it. I claimed in the
previous commit that removing the shell's fabricated 127 made "could not be
executed at all" available beside "ran and exited nonzero". I TESTED THAT AND IT
IS FALSE: a missing program does not produce a result record at all, it REFUSES
the evaluation --
  failed to execute 'no_such_binary': No such file or directory (os error 2)
-- so spawn failure was already fail-closed one rung above the record, and the
RED first proposed for this work would have passed against the old record too.

The real conflation is one step over and it was live at EIGHT sites:
  ran and FAILED, printing nothing    -> success=false, stdout=""
  ran and SUCCEEDED, printing nothing -> success=true,  stdout=""
Both are stdout == "". Those eight read stdout without consulting success, so a
failed probe and an empty result were the same value.

THE EIGHT, AND WHAT EACH NOW DOES:

fleet_host_key_enrollment.check -- THE WORST ONE. Tested trim(stdout)=="present"
  with no success check, so a probe that FAILED produced "" != "present" and fell
  through to the branch that APPLIES. A refusal to read authorized_keys was
  indistinguishable from the key being absent, and the remedies are opposite.
  Now: refusal refuses and does not mutate the file.
fleet_host_key_enrollment.verify -- did concat("outcome=", trim(stdout)), so a
  refused verify wrote the literal receipt line "outcome=" into a file someone
  would later read as fact. Now: outcome=UNKNOWN with the cause.
fleet_host_key_enrollment.{user,hostname} -- display only. Routed through
  process_outcome_receipt_text, which renders the three arms to three DISTINCT
  strings; a refusal can no longer read as empty.
fleet_probe_identity_observe.user -- display only, same route.
fleet_probe_identity_observe.{passwd_home,job_home} -- USED AS PATHS, not just
  printed, so they match the arms directly: "(refused: ...)" is fine to print and
  catastrophic to open. An unreadable home now skips the probe with a stated
  not-probed line instead of reading .ssh/authorized_keys off a fabricated root.
fleet_converge_plan_cli hostname -s -- SURFACED, NOT CLOSED, and said so in file.
  A `-> String` function has no way to refuse; the honest repair changes the
  return type and cascades into converge plan subject identity. It now returns a
  value that CANNOT be mistaken for a hostname rather than a plausible "", so a
  plan keyed on it is visibly wrong instead of silently wrong. Rung: mitigatable,
  with the next-rung trigger named.

SITES THAT GENUINELY DO NOT NEED THE DISTINCTION, stated rather than left silent:
  fleet_converge_plan_cli test -f -- exit status IS the product, no stdout anyone
  wants. Asks process_outcome_admitted directly. Forcing it through an
  output-bearing variant would add a field it cannot answer.
  ssh-keygen -F readback -- same shape, same treatment.
  fleet_ssh_credential_verify x2 -- decompose into a classifier that consumes all
  three values TOGETHER, so the correlation was already performed. The match adds
  exhaustiveness and names ProcessOutputAbsent, previously indistinguishable from
  a failure with empty stdout.

DELETED, not kept beside: type ShellCaptureResult is gone. Its one fabricated
construction is gone too -- fleet_host_key_enrollment built a ShellCaptureResult
to stand in for a FILESYSTEM write failure, inventing success:false for something
that was never a process. The coproduct makes that unwritable.

scan_host_key_lines shows why the type fits: `scan.success && trim(stdout) != ""`
IS ProcessOutputPresent, so a hand-written correlation became a variant. And
ssh-keyscan exiting 0 with no key is now a named outcome rather than being
reported as a refusal with an empty cause.

DISCRIMINATING RED, executed wet, six of six green: nonzero-exit-printing-nothing
must be Refused and zero-exit-printing-nothing must be Absent. Both go red if
ShellCaptureResult is restored, because then both are stdout == "". The file also
records what is NOT tested and why -- the nonexistent-program case is already
distinguishable via transport refusal, so asserting it would prove nothing.

Recorded on the carrier: spawn failure is fail-closed at the transport, therefore
A CALLER CANNOT PROBE FOR A BINARY'S EXISTENCE BY TRYING TO RUN IT -- the attempt
stops the line instead of answering. Presence must be asked of something that
exists. That is why a separate presence probe has to exist, and it is why no
fourth "not spawned" variant was added: it would be an uninhabited arm every
consumer must handle and none can reach.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Checked rather than argued, and the answer is worse than "it might reach a
receipt". fleet_converge_plan_wet WRITES host_short verbatim to
fleet_converge_plan_subject_host_path, coerces it to NonEmptyStr as the plan's
subject host, and folds it into the member-set fingerprint and the plan content
hash. An unobserved hostname is persisted as a receipt that later reads as fact.

AND IT DEFEATS THE GUARD BUILT FOR THIS EXACT CASE. fleet_converge_apply_wet
re-observes the host and refuses on SubjectHostMismatch when observed != planned.
Two consecutive refusals produce the SAME string, so the comparison SUCCEEDS and
apply proceeds. The check whose entire purpose is to stop a plan being applied on
the wrong host is satisfied by two non-observations agreeing with each other --
the empty-observation narrow relocated to the guard: bottom == bottom read as
"same host". Making the marker unique per call would NOT repair it; it converts a
false match into a false mismatch, which is a different wrong answer, not an
observation.

NOT INTRODUCED HERE, stated precisely: the prior code persisted "" and compared
"" == "", which passed identically. This migration does not repair the defect --
it makes the persisted evidence legible instead of blank.

Filed as a SECOND row rather than folded into the first, because the first row's
claim (visibly wrong rather than plausibly empty) says nothing about reachability
and this row is entirely about reachability. Both mitigatable; different next-rung
triggers. This one's: the subject-host comparison consumes an outcome rather than
a String, so unobserved-vs-unobserved is a REFUSAL to compare, not an equality.

The block is hoisted to module scope as a leading annotation on the declaration
(§4c), not left inside the func body.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…-argv2

# Conflicts:
#	dag/gunbc/command_runner.dag
…ain's command_over_transport refusal coproduct

TWO SEPARATE THINGS, both landing here because CI surfaced them together.

(1) THE §4c REFUSAL, 29 sites across four files. I put per-site rationale
where the explanation belongs conceptually -- beside the line it explains --
which is exactly the position the language refuses. Hoisted every block to a
consolidated leading annotation on the declaration.

WHAT I ACTUALLY GOT WRONG, since I had already hit this twice: I fixed ONE
block earlier and reported it as fixed. I repaired the instance the error named
instead of the class the RULE names. The sweep this time is the whole branch
and then the whole corpus -- both now zero indented `//`.

The refusal is correct and I am not routing around it. It is fail-closed at the
source boundary, typed, located to the byte, and it stopped the line rather than
silently dropping the prose. The corpus already tried the alternative: `//` as an
outright parse error made comment SYNTAX unwritable without making commentary
unwritable, and prose migrated into `data ...: String` rows where intent is
mechanically indistinguishable from program data.

(2) THE MERGE, which was NOT a text conflict to pick a side on. main landed the
command_over_transport refusal coproduct (Built | Refused, #8596) while this
branch replaced the capture return type. Both arms of both functions had to be
rebuilt, not chosen:

  run_shell_command         SSH arm: Refused -> exit_failure with the rendered cause
  run_shell_command_capture SSH arm: Refused -> ProcessRefused, NOT the deleted
                            ShellCaptureResult main still constructed there

Taking either side whole would have been wrong in a way that still compiles on
one of them: ours drops main's new refusal handling, theirs resurrects a deleted
type. So I took ours and re-applied main's additions explicitly -- the imports,
command_over_transport_refusal_reason and its note, and both refusal arms.

Note the refusal now composes rather than collapsing: an SSH command that cannot
even be BUILT is a ProcessRefused with a stated cause, distinct from one that ran
and failed. That is the same distinction this branch exists to make, arriving
from main's side of the merge.

The LocalExec arm is untouched by the merge and still routes through RunArgv.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…-argv2

# Conflicts:
#	dag/gunbc/fleet_converge_plan_cli.dag
…ome; DELETE my two mitigatable rows because they are no longer true

MAIN FIXED THE DEFECT WHILE THIS BRANCH WAS OPEN, and it fixed it at the rung
this lane named as the trigger rather than at the one I settled for.

  mine: -> String, returning a marker that cannot be mistaken for a hostname.
        Legible, still not a refusal. Two rows at mitigatable.
  main: -> NonEmptyStr?, Absent when the probe did not succeed. Plan AND apply
        refuse outright on Absent, and the subject comparison routes through
        fleet_converge_apply_subject_host_matches over two NonEmptyStr values
        instead of a bare String equality.

That closes BOTH rows. Row 1 (the value is visibly wrong rather than plausibly
empty) is obsolete because there is no longer a value. Row 2 (the poison is
persisted, and two non-observations comparing equal DEFEAT the SubjectHostMismatch
guard) is obsolete because Absent never reaches the comparison at all.

SO I DELETED BOTH ANNOTATIONS RATHER THAN KEEPING THEM. A rung row that describes
a defect the tree no longer has is not harmless documentation -- it is a false
claim in the file that owns the fact, and the next reader plans against it. That
is the stale-citation class this repo already pays for, and the cost is worse for
a row asserting a LIVE SAFETY DEFECT than for a stale line number: someone would
have re-escalated a fixed bug.

WHAT I ACTUALLY CHANGED is only the probe's input shape. main derived Absent from
`!run.success || trimmed == ""`, reading the record this branch deletes. The same
judgment now reads the arms of ProcessOutcome, and the mapping is exact rather
than re-decided:

  ProcessRefused                      -> none   (did not observe)
  ProcessOutputAbsent                 -> none   (ran, said nothing)
  ProcessOutputPresent, trims empty   -> none   (wrote bytes that do not name a host)
  ProcessOutputPresent, trims nonempty-> Present

The third arm is the one worth stating: ProcessOutputPresent means the process
WROTE BYTES, not that those bytes name a host, so the empty-after-trim guard main
had is preserved rather than assumed away by the richer type.

Also migrated this file's `test -f` site off `.success` onto process_outcome_admitted
-- exit status IS the product there, which is why it takes the admitted projection
rather than matching arms.

CONVERGENCE WORTH NAMING: main's repair and this branch's migration are the same
argument from two directions. Main gave the RESULT somewhere to say "not observed";
this branch gave the OBSERVATION somewhere to say it. Neither is redundant with the
other, and the merged form is stronger than either -- which is why this resolution
takes main's shape rather than defending mine.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…-argv2

# Conflicts:
#	dag/gunbc/command_runner.dag
#	dag/test/manual/command_runner_local_argv_receipt_test.dag
#	src/v1/stage0/src/cli_run.rs
…g is measured rather than claimed

The carrier was { body: String, probe_error: String }, and all 20 of its
constructions set exactly one field -- never both, because there is no such
observation: a probe either landed and produced a body or refused and produced
a reason. The empty string was doing the work of a tag, in a type that also
admits the empty string as a legitimate body. It is now
HealthzBodyRead | HealthzProbeRefused.

ground_service_ready_from_healthz_with_bundle's probe check was the first
clause of an if-chain; it is now a match, and the four stages below it split
into ground_service_ready_from_healthz_body, which can only ever be reached
with a body in hand.

THE RUNG, PROBED IN BOTH DIRECTIONS, AND IT IS TWO RUNGS:

  FIELD ACCESS IS STRUCTURAL. A probe reaching read.body off a refusal made
  the floor refuse during strict-preparation -- 'no field body on type
  HealthzEffectiveRead', located, at modules_resolved=3729, before a single
  witness executed.

  THE BARE RECORD LITERAL IS NOT. A literal naming the coproduct with no
  variant tag still resolves and still constructs; it is refused only at the
  match, at evaluation. Measured: that probe PASSED pre-change (planned=9784,
  failed=0) and became a per-witness runtime FAIL post-change with the corpus
  fully executed, not a preparation refusal.

So the construction half sits at mechanically preventable, not structurally
impossible, and the carrier says so. Next-rung trigger is a compiler
capability, named on the declaration: a record literal naming a coproduct type
with no variant tag should refuse at resolve, where field access already does.

readiness_check_order_note shrank from five ordered stages to four. PROBE left
it because it is no longer ordered by anything; the other four remain
ordering-by-discipline and the note says which and why.

Floor: planned=9783 executed=9783 passed=9475 known_red_held=304 failed=0,
against a pre-change baseline of 9784/9476/304/0 -- the delta is exactly the
deleted probe. The 4 stale-quarantine rows are identical in both runs and are
inherited from main, not from this change.
@gunbai-bot

gunbai-bot Bot commented Aug 20, 2026

Copy link
Copy Markdown
Contributor Author

The next-rung trigger is not this module's debt

The declaration names its next-rung trigger as a compiler capability. On review that framing is too small, and the correction is worth more than the migration, so it is stated here rather than left implicit.

What I proved, by execution, for one carrier: a record literal naming HealthzEffectiveRead with no variant tag resolves, constructs, and is refused only when something matches on it — the same source passed pre-change and became a per-witness runtime FAIL post-change with the corpus fully executed.

Two static facts I then read, which are consistent with that being general and are not themselves executed evidence:

  • the refusal is InterpError::PatternMatchFailure in v1_interpreter.rs — the interpreter, at evaluation, and it is the only site that emits that text;
  • the literal path that admits it is infer_record_lit (v1.compiler.infer, reached from the generic record-literal arm), the general record-literal inference route. 04_infer.dag says as much where it notes that two forms reach it — the record literal and the cast.

So, at the reach of what is actually established: the hole I hit is not a property of this coproduct. As far as those two facts reach, any coproduct in the corpus can be constructed by naming its type with no variant tag, with nothing refusing until something matches the value — and if nothing ever matches it, nothing refuses at all. This carrier is where it surfaced, not where it lives.

That caps every coproduct in the tree at mechanically-preventable for construction, however strong its field access is. HealthzEffectiveRead's field access is now resolve-time and located; that is a real climb and it is unaffected. But the construction ceiling it reports is a general one.

This is filed, not fixed. v1 is frozen and I am not its admission owner. Recording it as a located general finding with a named mechanism, rather than as a note on one declaration, so it can be ranked as the compiler row it is.

Distinguishing the two grades of claim above is deliberate: one carrier is proven by execution in both directions; the generalisation is read from source and is stated as such. I have not run a second coproduct to confirm it, and this comment does not claim I have.

— sent from sharp-ant-396

…eclared grain, NOT admitted

push_shell_argv_tokens ends in two arms that push the format! Display
rendering of a value as a host argv word. Null becomes the word 'null', Map
and Set become brace-wrapped renderings, Record becomes its type name plus
fields -- fabricated plausible output in argv position rather than a crash.
For Int, Float and Bool the same arm is correct and wanted, so deleting the
fallback would break the good half.

REACHABILITY: no declared argv site in the tree can carry a structured value
there. All 258 shell-transport operations enumerated, every argv element
classified -- 889 string literals, idents typed List<String> /
ProcessArgvExpansion / String / NonEmptyStr / FilePath, and calls each
returning List<String> or String. Nothing else. Both production callers draw
from that population. cargo_build Build does declare env: Map of String to
String inside a shell-transport operation, but it is an env input, never an
argv element -- a probe matching on the operation rather than on the argv list
would have reported a fabricator that cannot execute.

The claim is unreachable-at-DECLARED-grain, not unreachable: declared types
are not construction-enforced (3939 WhereRefinementUnenforced, no refinement
predicate evaluated on any kernel).

NOT ADMITTED, failing the standing in both directions: it is not
DefectRepairDiagnosticsMayMove because that class needs a behavior the seed
exhibits today and an unreachable arm exhibits nothing; and it fails the
2026-08-20 purpose test because hardening a dead seed arm serves v1, not the
v2 self-host program. Refusal dominates, so it is recorded rather than fixed,
with the one thing that would make it admissible named: a reachable specimen.

Floor unchanged: planned=9783 executed=9783 passed=9475 known_red_held=304
failed=0, no errors, no refusals.
@gunbai-bot

gunbai-bot Bot commented Aug 20, 2026

Copy link
Copy Markdown
Contributor Author

The red check is inherited from main, not produced here

Step-level result on run 32356442753 — exactly one failing step:

success  Build the witness fold
success  src/v1 .dag sources parse
FAILURE  Regen fixed point: first generation matches committed candidate
skipped  Regen determinism  (skipped because the step above failed)
success  All witnesses (one prepared subject, one fold)

The witness fold — the thing this PR changes — is green.

The same step fails on main, on both of its last two runs (32343207326, 32343044158), with a byte-identical message:

required-regen: first_generation_equal=false planned=129 executed=129
required-regen: FAIL generated surface drift: v1_compiler_emit_rust.rs

4cec10f66 — the commit merged into this branch — is among main's failures. Not regenerating the stage0 mirror or landing a mirror repair from here; reported instead.

Correcting my own evidence in the body above

The pre-change and final receipts I quoted were --required-floor only. The regen fixed point is a different entry (--required-regen) that I never ran, so my green was green about the axis I measured and silent about the one that failed. Not a wrong number — a denominator that excluded the failing check.

Closing the open question I left

The body says over_cost_line_diagnostic went 6 → 22 and that I read it as variance without proving it. A third run over an essentially identical corpus reads 4. So 6, 22, 4 — it is noise, and the open question is closed rather than left standing.

Added since review

36df1b1f17d files a separate finding on gunbc.v1_maintenance_standing: push_shell_argv_tokens fabricates a shell word from Null/Map/Set/Record via their Display rendering, in a position no declared argv site can reach — 258 shell-transport operations enumerated, every argv element typed to a string, List<String>, or ProcessArgvExpansion. Recorded as not admitted under the v1 standing (an unreachable arm exhibits no behavior to repair, and hardening a dead seed arm serves v1 rather than v2 self-host), with the one thing that would flip it named: a reachable specimen. Floor after the row is unchanged — planned=9783 passed=9475 failed=0.

— sent from sharp-ant-396

gunbc-ci-auto-heal added 2 commits August 20, 2026 12:59
…usal does not

The trigger read 'a compiler capability', which implies infrastructure to be
built. That is not what is missing. v1.compiler.types is_coproduct_type
answers the question in one expression -- n.connective == Disj -- and
record-literal inference already resolves the literal's named type and already
reasons about coproduct membership on the neighbouring path
(lookup_variant_parent_enum, variant_owner_node,
record_lit_variant_from_expected, record_lit_expected_coproduct). What is
absent is the judgment, not the fact.

Stated at the reach measured: those symbols answer the VARIANT-named literal
(this name is an arm, whose parent is X); the failing case is the PARENT-named
literal, which is a different question, and the refusal is neither built nor
tested here. So the row moves from DESIGN 4b's second category (can climb
after one grounding) to its third (can climb now but unbuilt).

Also records the trap for whoever builds it: is_coproduct_type is sufficient
for the direct, exactly-resolved specimen; a generalization must apply it to
the RESOLVED STRUCTURAL declaration rather than assume every authored alias
node carries Disj, or it would silently admit the construction it exists to
refuse.

Floor: planned=9783 executed=9783 passed=9475 known_red_held=304 failed=0, no
errors, no refusals.
@briansrls
briansrls merged commit 0d586b0 into main Aug 20, 2026
1 check passed
@briansrls
briansrls deleted the session/sharp-ant-396-argv2 branch August 20, 2026 16:13
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