Repository navigation
Conversation
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>
…rate 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>
…t 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>
… 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>
…eipt 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>
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>
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>
…ority 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>
|
Fixed rather than deferred, on the one item review 54403 flagged as residue. The review called the surviving
The mode is symbolic, and the module says why: One structural addition came with it: After this, Five witnesses green, including the new chmod row and the two websocat stages that reach it. — sent from eager-crane-282 |
|
Superseded by #8796, which carries this work unchanged along with the rest of the srv3 stack and the fleet-converge capability binding. Consolidated at the operator's request (too many open PRs). Verified before closing: every declaration, module and witness file this PR introduced is present on Nothing is dropped. Review history stays here; the diff to review is now #8796. |
The terminal cut of the srv3 anemic-execution dissolution. Stacked on #8769 → #8760 → #8750 → #8759.
What this closes
Any module could reach
srv3_transport_witness_bin_successandsrv3_elevated_witness_bin_successdirectly — "run this argv on this transport" and "run this argv as root on this transport". Both are nowadmit_callers-sealed to the functions that legitimately reach them.The point of the whole program stated as a wall: a caller outside this module 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, with the permitted set named:
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 §4b calls worse than sitting low, so both halves sit beside the seal with the next-rung trigger: admission checked per caller rather than per module.
A second reason that trigger matters
The admitted lists were derived by walking the module, not 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. Because in-module admission is unchecked, nothing would have caught either — a list the compiler does not verify is a list nothing verifies.
On the probes
Both 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 — the same reason
product/pcb/stackup.dagrecords its seal receipt in prose rather than in a test. This is a real gap in §4b(4)'s "evidence stays enrolled", and it is a property of the mechanism rather than a choice I made: what keeps the wall honest in the enrolled suite is that every route to these functions runs through an admitted caller.Scope
No behaviour change. The same functions run the same commands for the same callers; what changed is who else may name them.