Skip to content

Workflow capability closure: a job that consumes cargo without a provider cannot be emitted - #8702

Merged
briansrls merged 1 commit into
mainfrom
workflow-capability-closure
Aug 21, 2026
Merged

briansrls merged 1 commit into
mainfrom
workflow-capability-closure

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

A deleted workflow ran cargo build as step two with no toolchain provider anywhere in the file, and died on cargo: command not found 30 out of 30 runs without reaching its terminal step. Nothing in this repository could refuse it — by the time a job is List<Step>, a step that needs a toolchain and one that provides it are indistinguishable.

Receipt, verifiable independently:

git show a4677f33f4a8d5951de84a9e32383a8835797bab:.github/workflows/deploy.yml

Counted with positive controls on the same scan of the same input — cargo=1, uses:=1, name:=6 all nonzero — so setup-rust-toolchain=0 is a real zero and not a broken pattern. The single uses: in all 42 lines is the checkout.

What this adds

gunbc.workflow_capability_closure models a step's relationship to the capabilities its job needs — Provides / Consumes / Neutral over the existing ExecutionCapability vocabulary, not a second one — and folds steps in order, so a capability is available only once a preceding step provides it.

It sits above extdeps.github.actions and does not touch it. RunStep { run: String } is a faithful model of the GitHub wire format; the defect is product modules constructing that wire representation directly for operations whose semantics are known. Editing Step would re-coin the upstream spec (§3).

Structural, not textual — and the reason is measured. The same consumption is spelled cargo build in one workflow and "$CARGO_BIN" build in another. My own regex over the second form returned a confident zero on a file that invokes cargo twice, because a closing quote sits between the name and the space. A check that cannot see one of two live spellings is not weaker; its green means nothing for half the corpus.

The binding — what makes this a change rather than a demonstration

witness_floor_bound_steps is one list carrying both the Step and its role; witness_floor_steps and witness_floor_step_annotations are both projections of it, so they cannot drift. A hand-maintained roles list beside the steps list would be the §3 fork this closure exists to close, reintroduced as its own fix.

expected_witness_floor_yml now refuses: a job whose consumer has no preceding provider yields a refusal marker instead of yaml. A check only tests call is specification-without-execution — green forever while the emitter produces the broken workflow beside it.

Evidence

Every witness falsified by a different plausible wrong implementation:

witness base M1 vacuous M2 blanket-reject M3c order-insensitive
no-provider job refuses true false true true
provider-first job admitted true true false true
provider-after-consumer refuses true false true false

M3c is the one that proves ordering is the content of the claim: a check asking only "does this job contain a toolchain anywhere" passes a job broken exactly the way deploy.yml was.

Binding proven in both directions (M4 — toolchain retagged neutral):

refusal marker name: witnesses
mutated 1 0
restored 0 1

The refusal replaces the workflow rather than decorating it — the line stops.

Emission is byte-identical to the committed .github/workflows/witnesses.yml (1428 bytes both sides), so the step-construction refactor is behaviour-preserving and no regeneration is required.

Rung, honestly

Mechanically preventable for the one job that is bound. Every other workflow can still be assembled as bare Steps and bypass closure entirely — fleet-converge.yml is not bound by this cut. Next-rung trigger: binding the remaining emitters, at which point an unannotated job becomes the unwritable state rather than merely the unchecked one.

🤖 Generated with Claude Code

…ider cannot be emitted

deploy.yml ran `cargo build --release -p v1-compiler --bin gunbc` as step two
with no toolchain provider anywhere in the file -- the only `uses:` in all 42
lines was the checkout -- and died on `cargo: command not found` 30 out of 30
runs without ever reaching its terminal step. Nothing in this repository could
refuse it, because by the time a job is List<Step> a step that NEEDS a toolchain
and one that PROVIDES it are indistinguishable.

Receipt for that claim: git show a4677f3:.github/workflows/deploy.yml
(deleted in 5814d0d). Counted with positive
controls on the same scan of the same input -- cargo=1, uses:=1, name:=6 all
nonzero, so setup-rust-toolchain=0 is a real zero rather than a broken pattern.

WHAT THIS ADDS. gunbc.workflow_capability_closure models a step's relationship
to the capabilities its job needs -- Provides / Consumes / Neutral over the
EXISTING ExecutionCapability vocabulary (CargoCapability et al), not a second
one -- and folds the steps IN ORDER, so a capability counts as available only
once a preceding step has provided it.

It sits ABOVE extdeps.github.actions and does not touch it. RunStep { run: String }
is a faithful model of the GitHub wire format; the defect is product modules
constructing that wire representation directly for operations whose semantics are
known. Editing Step would re-coin the upstream spec (§3).

STRUCTURAL, NOT TEXTUAL, and the reason is measured: the same consumption is
spelled `cargo build` in one workflow and `"$CARGO_BIN" build` in another. My own
regex over the second form returned a confident ZERO on a file that invokes cargo
twice, because a closing quote sits between the name and the space.

THE BINDING, which is what makes this a change rather than a demonstration.
witness_floor_bound_steps is ONE list carrying both the Step and its role;
witness_floor_steps and witness_floor_step_annotations are both projections of
it, so they cannot drift. A hand-maintained roles list beside the steps list
would be the §3 fork this closure exists to close, reintroduced as its own fix.

expected_witness_floor_yml now REFUSES: a job whose consumer has no preceding
provider yields a refusal marker instead of yaml. A check only tests call is
specification-without-execution -- green forever while the emitter produces the
broken workflow beside it.

EVIDENCE, every witness falsified by a different plausible wrong implementation:

  witness                          base  M1     M2       M3c
                                         vacuous blanket  order-insensitive
  no-provider job refuses          true  false  true     true
  provider-first job admitted      true  true   false    true
  provider-after-consumer refuses  true  false  true     false

M3c is the one that proves ordering is the content of the claim: a check asking
only "does this job contain a toolchain anywhere" passes a job broken exactly the
way deploy.yml was.

Binding proven in both directions (M4, toolchain retagged neutral):
  mutated:  refusal_marker=1  yaml_name_line=0   <- refusal REPLACES, not decorates
  restored: refusal_marker=0  yaml_name_line=1

Emission is byte-identical to the committed .github/workflows/witnesses.yml
(1428 bytes both sides), so the step-construction refactor is behaviour-preserving
and no regeneration is required.

RUNG, HONESTLY. Mechanically preventable for the one job that is bound. Every
other workflow can still be assembled as bare Steps and bypass closure entirely
-- fleet-converge.yml is not bound by this cut. Next-rung trigger: binding the
remaining emitters, at which point an unannotated job becomes the unwritable
state rather than merely the unchecked one.

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

gunbai-bot Bot commented Aug 21, 2026

Copy link
Copy Markdown
Contributor Author

REVIEW — REQUEST CHANGES. Posted as a comment because GitHub refuses a formal request-changes review from the shared bot identity that authored the PR. Treat it as blocking.

The refusal is typed as a success, and the regenerator writes it into .github/workflows/witnesses.yml

I have no stake in this change and disclose none.

Nearly all of this holds up under reading, and I checked the two claims that carry it rather than taking the body's word:

  • witness_floor_bound_steps really is the single authority. witness_floor_steps is list_map(… f: fn(b) { b.step }) over it and witness_floor_step_annotations maps the same list. The two projections cannot drift. The anti-fork argument is not decoration.
  • The fold really is order-sensitive, and M3c is the right control for it — capability_label_present is consulted against acc.provided accumulated only from preceding steps, so a provider placed after its consumer refuses. That is the deploy.yml failure exactly, and a presence-anywhere check would pass it.
  • Structural-not-textual is argued from a measurement, not a preference, and the measurement is the good kind: your own regex returned a confident zero on a file invoking cargo twice.

Then the refusal leaves this module, and one line undoes the change's own thesis.

The defect

gunbc.witness_floor_workflow:

fn expected_witness_floor_yml() -> String {
  … witness_floor_capability_closure_refusal   // a String
}

gunbc.generated_artifact_emit:

WitnessFloorYamlArtifact => artifact_generated(content: expected_witness_floor_yml())

artifact_generated constructs ArtifactGenerated { content }. So a capability-closure refusal is typed as a successful generation whose content is the refusal prose.

dag/tools/generated_artifact_gate.dag main_wet then does exactly what its name says:

ArtifactGenerationRefused { reason } => exit_failure(reason: …)
ArtifactGenerated { content } => {
  let w = Filesystem.Write(path: artifact_path(a: a), content: content)
  if w.success { ExitSuccess } else { … }
}

On refusal, main_wet writes the refusal prose into .github/workflows/witnesses.yml and exits ExitSuccess. That file is one of the two surviving workflows and the only one that runs the required floor. main_wet is not hypothetical — it is the documented regeneration route, named as such in this very gate at the hand-edit banner ("regenerate via main_wet on dag/tools/generated_artifact_gate.dag") and driven by the real-roster transport.

So the arm that exists to stop the line instead destroys CI and reports success. That is the absorbing fallback's worse sibling: not a widen, a fabricated plausible output written to disk under a green exit.

The fix is one constructor, already used twice on adjacent lines

ArtifactGenerationOutcome already has the right shape, and artifact_generate already routes two artifacts through it:

GitattributesArtifact => match expected_gitattributes() {
  GitattributesGenerated { content } => artifact_generated(content: content)
  GitattributesGenerationRefused => ArtifactGenerationRefused { reason: … }
}
V1InterpreterDispatchGeneratedRsArtifact => match expected_v1_interpreter_dispatch_generated_rs() {
  V1InterpreterDispatchGenerated { content } => artifact_generated(content: content)
  V1InterpreterDispatchGenerationRefused { reason } => …
}

expected_witness_floor_yml should return that same two-arm shape — WitnessFloorYamlGenerated { content } | WitnessFloorYamlGenerationRefused { reason } — and artifact_generate should match it. Then main_wet reaches exit_failure with the closure's own reason, and no write happens.

This is not a style preference and I would not raise it as one. The PR's whole argument is that a step needing a toolchain and a step providing one must not be the same type. Returning String for both "the workflow" and "no workflow" is that identical conflation, one layer up, in the same change — and unlike the wire-format Step, here the richer carrier already exists in the module being edited.

What this costs the evidence table

The M4 binding matrix counts refusal marker = 1 / name: witnesses = 0 in the mutated tree. Both readings are of the returned string, so the table is true and cannot distinguish the current construction from the correct one — the refusal marker is present either way. It is not a bad table; it is measuring one layer below where the defect sits. With the typed outcome, the discriminating assertion becomes artifact_generate(WitnessFloorYamlArtifact) yielding ArtifactGenerationRefused, which the current code cannot satisfy and the fixed code cannot fail.

What I checked and what I did not

Read directly: the closure module in full, the fold's accumulator, the three projections, artifact_generate's arms, artifact_path's mapping of WitnessFloorYamlArtifact to .github/workflows/witnesses.yml, and main_wet's write.

Not executed: I did not run main_wet against a mutated tree to watch the workflow file be overwritten. The write is a direct read of the code path with no intervening branch, so I am reporting it as confirmed-by-construction rather than confirmed-by-execution, and saying which.

Also not checked: whether the byte-identical claim holds — I took it as stated, since the defect above is upstream of it.

Verdict

Requesting changes on the one construction. Everything else in this PR I would approve as written, including the rung statement, which is honest about fleet-converge.yml being unbound.

— sent from smart-ram-730

@briansrls
briansrls merged commit 1a1ebf8 into main Aug 21, 2026
2 checks passed
@briansrls
briansrls deleted the workflow-capability-closure branch August 21, 2026 03:51
gunbai-bot Bot added a commit that referenced this pull request Aug 21, 2026
…r_workflow (#8737)

#8702 (mine) deleted a 14-line annotation block and reverted a CI step name that
another session had authored in #8657. I did not write those deletions. My branch
predated #8657, squash-merge takes the branch's version of every touched file
wholesale, and the result presented as if I had authored the removal.

WHAT WAS LOST:

  - the annotation explaining why the behavioral receipt is NOT a step here --
    that #8647 collapsed the step ladder into one invocation, that re-adding
    steps would rebuild the ladder that PR removed, and that the per-PR phase
    now decides from what it can OBSERVE rather than from a trigger name. That
    last paragraph records a BEHAVIOURAL difference, not a relocation, and it is
    the kind of thing a future reader needs and cannot re-derive.

  - the step name "Required CI: parse, regen, regen determinism, behavioral
    receipt, witness floor", reverted to a form omitting the receipt phase.

WHY NOTHING CAUGHT IT. Three properties compounded:

  1. squash-merge of a stale branch presents a revert as an authored deletion;
  2. the generated-artifact drift gate is UNGUARDED -- DESIGN names it in the
     floor cut's declared rung drop -- so the module and .github/workflows/
     witnesses.yml disagreed on main with nothing to notice;
  3. the merge was clean, five reviews approved the diff, and CI passed.

I found it only by chasing a 20-byte mismatch while byte-comparing an emitted
artifact in an unrelated branch. That comparison is exactly the check CI is
currently missing.

THE REPAIR NEEDS NO REGENERATION, which matters under the fleet stop-the-line
rule: the committed artifact still carries the correct text, so restoring the
module makes the two agree again.

  witnesses.yml   emitted 1457 == committed 1457   (was 1437 vs 1457 on main)
  the_live_witness_floor_job_closes_its_capabilities -> true
  in-body annotations -> 0

THE GENERAL HAZARD, recorded because it is not specific to this file: a
long-lived branch plus squash-merge is a silent-revert machine. Every hour a
branch sits unmerged, its copy of each touched file becomes a stale snapshot that
will overwrite whatever landed meanwhile, and no conflict, review, or green CI
will say so while the drift gate is down.

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Aug 21, 2026
…hole in admit_callers (#8796)

* Bind fleet-converge's build job to capability closure; widen the role to a relation

WIP commit before merging main -- full message on the PR.

* Restore what my stale-branch squash silently reverted in witness_floor_workflow

#8702 (mine) deleted a 14-line annotation block and reverted a CI step name that
another session had authored in #8657. I did not write those deletions. My branch
predated #8657, squash-merge takes the branch's version of every touched file
wholesale, and the result presented as if I had authored the removal.

WHAT WAS LOST:

  - the annotation explaining why the behavioral receipt is NOT a step here --
    that #8647 collapsed the step ladder into one invocation, that re-adding
    steps would rebuild the ladder that PR removed, and that the per-PR phase
    now decides from what it can OBSERVE rather than from a trigger name. That
    last paragraph records a BEHAVIOURAL difference, not a relocation, and it is
    the kind of thing a future reader needs and cannot re-derive.

  - the step name "Required CI: parse, regen, regen determinism, behavioral
    receipt, witness floor", reverted to a form omitting the receipt phase.

WHY NOTHING CAUGHT IT. Three properties compounded:

  1. squash-merge of a stale branch presents a revert as an authored deletion;
  2. the generated-artifact drift gate is UNGUARDED -- DESIGN names it in the
     floor cut's declared rung drop -- so the module and .github/workflows/
     witnesses.yml disagreed on main with nothing to notice;
  3. the merge was clean, five reviews approved the diff, and CI passed.

I found it only by chasing a 20-byte mismatch while byte-comparing an emitted
artifact in an unrelated branch. That comparison is exactly the check CI is
currently missing.

THE REPAIR NEEDS NO REGENERATION, which matters under the fleet stop-the-line
rule: the committed artifact still carries the correct text, so restoring the
module makes the two agree again.

  witnesses.yml   emitted 1457 == committed 1457   (was 1437 vs 1457 on main)
  the_live_witness_floor_job_closes_its_capabilities -> true
  in-body annotations -> 0

THE GENERAL HAZARD, recorded because it is not specific to this file: a
long-lived branch plus squash-merge is a silent-revert machine. Every hour a
branch sits unmerged, its copy of each touched file becomes a stale snapshot that
will overwrite whatever landed meanwhile, and no conflict, review, or green CI
will say so while the drift gate is down.

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

* Bind the websocat driver to the stage the sequence authority names

The first cut's claim that websocat_after is the sole transition authority was true of
the stop-or-continue decision and NOT true of the stage edge. Every driver site matched
`WebsocatContinue { next: _ }` and then ran the stage it was written to expect, so the
order existed twice: once as data in websocat_after, once as a hardcoded call chain.

That permitted a divergence no witness could see. Rewrite an edge -- EnsureDirectory
continuing to Download instead of EnsureOwnership -- and the trace, which follows `next`,
would report the new order while production carried on chowning in the old one. The
never-stops mutation could not catch it: it mutates the stop decision, not the edge.
Raised in side-chat review of #8747, verified here before acting on it (six sites
discarded `next`).

The driver now consults the authority. Each site checks that the stage websocat_after
named is the stage that site implements, and a disagreement REFUSES with both stage
names rather than running the code it happens to have. Comparison goes through
websocat_stage_label because that fold is already the total projection of the stage type;
a second equality over the same coproduct would be the fork this removes.

srv3_websocat_install_from is now one function per stage rather than one function nesting
five matches. That is not tidying: at depth five the guard and the effect it guards were
no longer visible together, which is the condition under which this file's defects have
been introduced twice.

Evidence, by mutation: rewriting the EnsureDirectory edge to Download reddens exactly the
directory-edge witness and the full-chain trace, and leaves the other three edge witnesses
green -- located, not just red. The guard's own negative control (an edge deliberately
compared against a stage no site implements) proves it can answer false at all.

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

* Ground the srv3 POSIX principal and privilege lowering; refuse degenerate ids

The chown that srv3's websocat install performs took its owner as a String composed
as uid + ":" + gid from two raw stdout captures, and ran under a hardcoded
"/usr/bin/sudo" with a bare "-n" at the head of the args list. Both are the
String-as-anemic-modeling class: there was no state in which a bad `id` read could be
noticed, because concatenation always succeeds.

POSIX owns the ids, so extdeps.posix.identity mints PosixUserId, PosixGroupId and
PosixOwnerSpec, and owns the ":" form chown takes. It is not a second spelling of
extdeps.access.posix_effective_principal, which models the principal's NAME as
whoami reports it -- POSIX keeps those two facts apart and so does this.

sudo's calling convention was spelled at four call sites. extdeps.sudo.elevation now
owns it: sudo_elevate takes the argv a command would run unelevated and returns the
elevated invocation, so elevation is a transformation OF an invocation rather than a
second way to spell one. All four "/usr/bin/sudo" literals and all three hand-carried
"-n" prefixes are gone. extdeps.tools.chown and extdeps.tools.mkdir own their argv and
their absolute paths; extdeps.tools.id gains id_binary_path. The absolute paths are
load-bearing rather than pedantry -- a sudoers NOPASSWD rule matches on command path.

The LocalShell arm also stopped reading .stdout raw. It goes through the same trimmed
token shape the ssh arms use, which was a live cross-transport disagreement: `id`
emits a trailing newline, ssh trimmed it and local did not.

DECODING DID NOT BY ITSELF CLOSE THE HOLE, and a witness is what proved it.
integer_lexeme_to_int_optional answers Present { value: 0 } for "", and 0 is root, so
an `id` that printed nothing decoded to the most privileged principal on the host and
was chowned to. The witness asserting that empty text does not decode came back FALSE
on its first run. The decoder now answers its own degenerate cases: empty,
whitespace-only and negative are refused; "0" is admitted, because root is a real
principal. The law is not "zero is invalid" -- it is that only the explicit lexical
representation of zero may construct id zero.

WHAT THIS DOES NOT CLAIM. Ownership is not ensured. This grounds the operands and the
privilege lowering; it does not observe the current owner, does not skip a chown that
is unnecessary, and does not read ownership back afterwards. A successful chown process
is still the only evidence, which is why nothing here is named EnsurePathOwner.

15 witnesses, all measured green.

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

* Ensure srv3's bin directory ownership by readback, not by chown's exit status

The websocat install's EnsureOwnership stage ran an elevated chown and returned
Holds or Fails straight from the process result, so "the chown exited zero" and
"the directory is owned by us" were one claim. They are not. A chown that followed
a symlink changed something else; one that raced a replaced path changed the old
inode; one under a sudoers rule permitting the binary but not the target can exit
zero having converged nothing. Exit status as convergence is the fabricated
plausible output at the actuation boundary.

extdeps.posix.path_ownership models the ensure as observe, decide, mutate only if
needed, observe again independently, and let the SECOND observation decide. The
mutation's own result cannot reach the verdict: path_ownership_verdict takes the
readback and the desired owner and has nowhere to put a process result. A chown that
reported failure is read back exactly like one that reported success, because a
process result is not evidence about the filesystem in either direction. The only arm
that skips the readback is the one where no host was reached at all.

Skipping an unnecessary chown is a safety property rather than an optimization: on a
converge that has already run, the declined mutation is the ONLY privileged
invocation this stage would have made.

An unobserved owner is not an unowned path. `stat` refusing and `stat` reporting a
different owner demand opposite actuations, and reading the first as the second would
chown a host that was never asked -- the empty-observation narrow pointed at a
privileged mutation.

extdeps.tools.stat is cited to GNU coreutils rather than POSIX, deliberately: -c is a
GNU extension, POSIX does not specify stat(1) at all, and BSD spells the same request
-f with different conversion characters. A host shipping the BSD utility needs its own
authority, not a widened format string here. Two probes of one token each, rather than
one "uid:gid" probe, so the existing single-id decoder is reused instead of a second
place where the ":" grammar lives.

srv3_transport_token replaces the third hand-rolled four-arm transport match over the
same shape.

Evidence: 8 witnesses green. By mutation -- the verdict rewritten to ignore the readback
and report convergence, which is the pre-cut behaviour -- the two refusal witnesses flip
to false while the positive control and the four decision witnesses stay true.

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

* Repair the ownership cut: restore the deleted helpers, keep the chown as evidence, stop sequencing by argument position

Three defects, none of them found by me.

ONE, from CI's floor: this branch did not resolve at all. The commit replaced a block
of host_effect_realize by index range, and the range swallowed three helpers added
minutes earlier in the same session -- srv3_transport_token and its two locals. They
are restored.

TWO, from review 54354: the cut deleted srv3_chown_to_decoded_owner while the
principal/privilege witness file still imported it, so the three load-bearing REDs for
the fabricated-owner refusal could not execute. They are rewritten against
srv3_owner_from_texts, the surviving pure entry point that carries the decode refusal,
plus a positive control -- three refusal assertions are satisfied by a function that
refuses everything. The "refuses before chowning" claim is now structural rather than
positional: the ensure is parameterised on the observed owner, so an unobserved owner
cannot reach the chown.

Why neither surfaced locally: after the change I ran only the NEW witness file, whose
subjects all live in extdeps modules, so it went 8/8 green without ever resolving the
file I had just edited. Running the witnesses for what I added is not the same as
running the witnesses whose subject I changed.

THREE, from side-chat review: the verdict discarded the mutation entirely, fusing "not
authoritative for state" with "not evidence at all". The state still comes from the
readback and nothing else -- every arm dispatches on it, and `attempt` reaches the
outcome only as a field of the receipt -- but the attempt is now carried, and the
outcome is renamed PathOwnershipConvergedAfterAttempt because "Changed" asserted a
causal claim the evidence does not support: a chown that reported FAILURE followed by a
desired-owner readback establishes that the state exists, not that our mutation produced
it. The mismatch diagnostic also said "the chown reported no error" while both reported
success and reported failure routed into it -- false half the times it fired. It now
names what the actuator reported.

The attempt carrier does not yet hold exit code or stderr, and says so with its
next-rung trigger: the transport surface projects a process result to a three-valued
predicate before this module sees it.

Also from that review: the chown was sequenced by ARGUMENT POSITION, with a comment
defending it as deliberately load-bearing eagerness. That reinstates the exact footgun
this sequence of cuts exists to remove -- implicit evaluation order is not a sequencing
authority, and wanting eagerness this time does not make it one. It is a `let` inside
the arm now.

26 witnesses green across both files. The principal file imports host_effect_realize,
so its resolution is now part of the evidence rather than assumed.

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

* Make each srv3 tool's acquisition mechanism a row, and derive the receipt from it

How a tool is acquired was expressed only by which function the author happened to call:
three srv3_ensure_apt_tool calls and one srv3_ensure_websocat, hand-written side by side.
The receipt that reports them was a concat chain naming each tool TWICE -- once as a
string literal in the receipt, once as a variable in the call -- so the two could disagree
and nothing would notice. Adding a tool meant editing three places and remembering a
fourth.

Srv3ToolAcquisition names the mechanism, Srv3ToolRow pairs it with the tool, and
srv3_ensure_tool is the only place a mechanism is chosen -- a total match, so a new
mechanism is a variant the compiler refuses to leave unanswered. The ensure folds the
rows and the receipt is derived from the same observations, so a tool cannot be ensured
and omitted from the receipt, or renamed in one and not the other.

require_version_probe moved INSIDE the apt variant rather than sitting beside the
acquisition as a peer field. The release path has no version probe to require, so as a
peer it was a value one variant silently ignored -- a state the type admitted and the
code dropped.

Evidence: 4 witnesses green, and each is discriminating. Switching websocat's row from
the release mechanism to apt reddens the mechanism witness alone; stripping the tool name
out of the receipt entry reddens both receipt witnesses and leaves the mechanism one
green. The empty case is stated rather than left to be discovered.

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

* Seal srv3's execution surface so no other module can name it

A caller outside gunbc.host_effect_realize could reach srv3_transport_witness_bin_success
and srv3_elevated_witness_bin_success directly -- "run this argv on this transport" and
"run this argv as root on this transport". Both are now admit_callers-sealed to the
functions that legitimately reach them, so a foreign caller can name a semantic operation
(ensure this tool, ensure this owner) and cannot name the machinery that executes it.

THE SEAL'S REACH IS MEASURED, AND IT IS NARROWER THAN THE NAME SUGGESTS. Two probes on
one build:

  - a caller in ANOTHER module REFUSES at resolve, naming the permitted set:
    "constructor call admission refused: ... refuses call from
    'test.claim.srv3_seal_probe.a_foreign_module_may_not_run_a_privileged_argv' --
    permitted callers: [...]"

  - a caller in THIS module, absent from the admitted list, calling the elevated form with
    ["/bin/rm", "-rf", "/"], typechecked and resolved with NO DIAGNOSTIC AT ALL.

So the rung is mechanically preventable at the module boundary and nothing within it.
Reporting only the refusal would be the rung inflation DESIGN section 4b calls worse than
sitting low, so both halves are recorded beside the seal with the next-rung trigger:
admission checked per caller rather than per module.

The admitted lists were derived by walking the module rather than by reading the call
sites. My first hand-read attributed two calls to the wrong enclosing function and
invented a fifth caller that does not exist -- and because in-module admission is
unchecked, nothing would have caught either. A list the compiler does not verify is the
second reason that trigger matters.

Both probes were removed after measurement: an admission refusal is a resolve-time error,
so it cannot be enrolled as a passing witness without breaking the corpus it proves.

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

* Assemble elevated argv with one append instead of a snoc per element

Raised as a non-blocking observation on review 54393, and fixed rather than noted:
DESIGN section 6's bare-minimum-cost rule says a proven cost shape -- "a copied
accumulator, a quadratic fold" is the wording -- is always fixed regardless of the
realized n, because "n is small here" is not a time-stable fact.

sudo_elevate folded the command argv, appending to a growing accumulator once per
element. It is the single place every privileged invocation in the repository is
assembled, so its n is whatever a future caller's argv turns out to be, which is exactly
the case the rule is about. srv3_argv_with_bin carried the same shape and is fixed with
it rather than left as the next instance of a defect just removed.

The reviewer's second observation -- that websocat_edge_admits compares stages through
websocat_stage_label rather than a structural equality -- is deliberate and stays. A
second total projection over the same coproduct would be the fork that function exists
to remove.

Five witnesses over both argv builders and the acquisition rows re-measured green.

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

* Dissolve the last argv literal in the srv3 chain: chmod gets its authority

Review 54403 called the surviving "/bin/chmod" literal minor residue and outside this
cut's scope. It is the last one in the chain, and leaving one of six is what makes the
class get re-derived later -- the operator's standing instruction on this program is that
a string in this position is anemic modeling and that the debt is mine to own, so the
scope argument cuts the other way here.

extdeps.tools.chmod cites POSIX and carries the absolute path for the same reason
extdeps.tools.chown and extdeps.tools.mkdir do: a sudoers NOPASSWD rule names a command by
path, and chmod sits at /bin rather than /usr/bin on the hosts this actuator targets --
a fact about those hosts, recorded rather than assumed at a call site.

The mode is SYMBOLIC and the module says why: `+x` ADDS the execute bit to whatever
permissions the file carries, while an octal mode REPLACES the whole set. They are not
interchangeable spellings of "make it executable" -- one preserves the other bits and one
silently decides them -- and an ensure means the additive one.

srv3_transport_argv_success is the argv-shaped sibling of the witness-bin surface. Every
extdeps tool row returns a complete argv while that surface takes a binary and its tail
separately, so callers were either splitting the argv apart by hand or, more often, not
building one at all and passing a literal binary beside a literal args list. It is sealed
to its caller like the rest of the execution surface, and it refuses an empty argv rather
than running whatever a split of nothing produces.

Five witnesses green, including the new chmod row and the two websocat stages that reach
it.

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

* Close the same-module hole in admit_callers

constructor_call_admission_diags skipped the permitted-list comparison entirely when
caller and callee shared a module, so the semantics the compiler implemented were
'a permitted caller OR any declaration in the defining module' -- an implicit wildcard
that never appeared in the authored declaration and that no reader of a sealed fn could
see.

Measured before the repair: a probe added to gunbc.host_effect_realize, absent from the
admitted list, calling the elevated execution leaf with ["/bin/rm", "-rf", "/"],
typechecked and resolved with no diagnostic at all, while the same call from another
module refused. Measured after: same-module unlisted callers now refuse with the existing
ConstructorCallAdmissionRefused diagnostic naming the permitted set.

The repair deletes the branch and nothing else. The exact caller-coordinate comparison,
the diagnostic, and the caller-identity-unavailable arm were all already present and
already correct -- the compiler had every fact it needed and declined to use it.

The stage0 mirror is the regen candidate, produced by claim_executor --required-regen and
installed from it, not hand-carried. required-regen reported drift on exactly one file,
v1_compiler_infer.rs, which is the mirror of this change.

Operator-admitted (2026-08-21, direct chat: 'regarding the compiler defect, you may fix
it'). The permitted lists this surfaces across the corpus follow in the same change.

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

* Admit the sibling constructor route the closed hole exposed

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

* Ground the build-step chmod invocation on the cited chmod authority

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

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <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