Repository navigation
Dissolve the srv3 shell execution surface, and close the same-module hole in admit_callers - #8796
Merged
Merged
Conversation
… to a relation WIP commit before merging main -- full message on the PR.
…r_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>
…rop the restored block
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>
Both sides changed expected_fleet_converge_yml: main added a typed FleetConvergeYamlGenerationOutcome with a timeout-ceiling refusal, this branch made it a String with a capability-closure refusal. They are peers rather than alternatives, so the resolution keeps main's typed outcome and gives the closure its own refusal arm instead of picking a side. The closure is checked first -- it is a fact about the steps, while the timeout is a fact about the job containing them. witness_floor_workflow takes main's side wholesale: the behavioral receipt was cut from required mode by an operator ruling on 2026-08-21, after this branch was cut, so main's step name and its account of where the receipt lives are the current ones.
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>
This was referenced Aug 21, 2026
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 5, 2026
§4.I — ci_native_cache_root_toolchain_segment_command DELETED #7436 (003d960). CASE 1 dissolution — toolchain segment computation reordered after setup-rust-toolchain; fallback table entry struck through as RESOLVED. §4.J.A — ci_floor_stamp_merge_admission_script All three raw leaves (ci_floor_stamp_ambient_exit_command, ci_floor_stamp_root_command, merge_admission_stamp_command) DELETED #7522 (87a4af3). CASE 1 dissolution. 'PARTIAL #7293' status stale. §4.J.B — ci_floor_materialization_receipt_gate_script, ci_floor_resolve_receipt_gate_script DELETED #7470 (b01cdf4). CASE 1 dissolution — WalkPlan success stages finalization dissolved both receipt gates. §4.J.C (ci_spec.dag table): - gunbc_ci_floor_only_script DELETED #9252 — CASE 1 - ci_regen_floor_skip_shortcut_script DELETED #8406 — CASE 1 - gunbc_ci_regen_floor_only_script DELETED #8406 — CASE 1 - scheduler_invoke/scheduler_invoke_with DELETED #9252 — CASE 1 - git_fetch_script RENAMED #6833 — CASE 3 (successor: git_fetch_no_tags_shell / git_fetch_prune_shell) §4.J.D (ownership table): - Merge-admission row: all three raw leaves struck #7522 (CLOSED) - CI materialization row: both receipt gates struck #7470 (CLOSED) - CI-spec row: stale symbols struck through individually - Already-routed row: ci_selection_control_script #8283, gunbc_ci_run_script #9252, ci_regen_ensure_rustfmt_path_script #8406 (and 11 rustfmt raw leaves) struck through - Runtime terminal row: host_effect_plan_placeholder_effect DELETED #10509 - Deferred srv3 row: srv3_chown_directory_to_current_user struck #8796 (ref §4.D), all 4 host_hygiene_reap_*_body + liveness body struck #8583 (ref §4.A) All deletion commits verified as ancestors of origin/main ✅. Part of #10537's per-row adjudication program.
briansrls
added a commit
that referenced
this pull request
Sep 5, 2026
….E, §4.I, §4.J (#10576) * Correct §4.A hygiene-reaper row: CASE 2 — four host_hygiene_reap_*_body symbols deleted by #8583 The §4.A row at L379 described host_hygiene_reaper_script.dag's 4 body symbols as A5-deferred. The file was deleted by ffa16a5 (#8583, Migrate host-hygiene reaper and liveness onto typed observation) and the construction was migrated to typed host_hygiene_reaper_observe.dag / host_hygiene_reaper_remediate.dag / host_hygiene_liveness_observe.dag. No direct successor body names exist — CASE 2 (file deletion upstream) with hybrid CASE 1 (body names dissolved). Verification: - ffa16a5 is ancestor of origin/main ✅ - host_hygiene_reaper_script.dag: D in #8583's diff - zero files define host_hygiene_reap_install_units_body et al. - observe/remediate files present at dag/gunbc/host/ Part of #10537's per-row adjudication program. * Correct §4.D srv3_chown_directory_to_current_user: CASE 4 — renamed AND climbed The row at §4.D L436 listed srv3_chown_directory_to_current_user as A5-deferred (srv3). It was actually renamed AND climbed by 20ad5b3 (#8796): successor is gunbc.host_effect_realize.srv3_ensure_directory_owned_by_current_user. New name has a stronger guarantee (readback-based, not chown exit-status based). This is CASE 4 (rename plus climb) — distinct from CASE 1 (dissolution) because the construction did not disappear; it acquired a better name and a stronger guarantee. Verification: - 20ad5b3 is ancestor of origin/main ✅ - srv3_chown_directory_to_current_user: 0 declaration files - srv3_ensure_directory_owned_by_current_user: 2 declaration files Part of #10537's per-row adjudication program. * Correct §4.E: 4 stale foreign-executor rows Four symbols claimed as 'already on emit' are no longer present in the corpus. Each is struck through with its deletion commit: 1. ci_selection_control_script — DELETED by 611fd02 (#8283, CI floor cut). CASE 1/2: the ci.yml file was deleted and its selection-control script dissolved with it. Successor workflow is witnesses.yml via gunbc.witness_floor_workflow. 2. gunbc_ci_run_script — DELETED by 489346f (#9252, plan/walk CLI delete). CASE 1: the gunbc ci verb was deleted, taking its run script. 3. ci_regen_ensure_rustfmt_path_script — DELETED by 3b431f3 (#8406, REGEN ROOT CUT). CASE 1: regen_stage0 root deleted; rustfmt path script was zero-consumer machinery. 4. expected_live_deploy_retract_script — DELETED by d409b75 (#7909, Phase A release identity refactor). CASE 1: recategorized to runtime-present, then dissolved. All four deletion commits are ancestors of origin/main ✅. Part of #10537's per-row adjudication program. * Correct §4.I, §4.J, §4.D ownership table: 18+ stale symbols §4.I — ci_native_cache_root_toolchain_segment_command DELETED #7436 (003d960). CASE 1 dissolution — toolchain segment computation reordered after setup-rust-toolchain; fallback table entry struck through as RESOLVED. §4.J.A — ci_floor_stamp_merge_admission_script All three raw leaves (ci_floor_stamp_ambient_exit_command, ci_floor_stamp_root_command, merge_admission_stamp_command) DELETED #7522 (87a4af3). CASE 1 dissolution. 'PARTIAL #7293' status stale. §4.J.B — ci_floor_materialization_receipt_gate_script, ci_floor_resolve_receipt_gate_script DELETED #7470 (b01cdf4). CASE 1 dissolution — WalkPlan success stages finalization dissolved both receipt gates. §4.J.C (ci_spec.dag table): - gunbc_ci_floor_only_script DELETED #9252 — CASE 1 - ci_regen_floor_skip_shortcut_script DELETED #8406 — CASE 1 - gunbc_ci_regen_floor_only_script DELETED #8406 — CASE 1 - scheduler_invoke/scheduler_invoke_with DELETED #9252 — CASE 1 - git_fetch_script RENAMED #6833 — CASE 3 (successor: git_fetch_no_tags_shell / git_fetch_prune_shell) §4.J.D (ownership table): - Merge-admission row: all three raw leaves struck #7522 (CLOSED) - CI materialization row: both receipt gates struck #7470 (CLOSED) - CI-spec row: stale symbols struck through individually - Already-routed row: ci_selection_control_script #8283, gunbc_ci_run_script #9252, ci_regen_ensure_rustfmt_path_script #8406 (and 11 rustfmt raw leaves) struck through - Runtime terminal row: host_effect_plan_placeholder_effect DELETED #10509 - Deferred srv3 row: srv3_chown_directory_to_current_user struck #8796 (ref §4.D), all 4 host_hygiene_reap_*_body + liveness body struck #8583 (ref §4.A) All deletion commits verified as ancestors of origin/main ✅. Part of #10537's per-row adjudication program. --------- Co-authored-by: Brian Searls <briansearls1@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Consolidates the srv3 execution-surface work into one PR (six redundant PRs closed), and closes a compiler admission hole the work exposed.
Anemic execution-surface dissolution (srv3). The srv3 realizer's shell surface — argv vectors, process-success booleans and stringly principals — is replaced by semantic requests and typed observations:
extdeps/posix/identity.dag—PosixUserId/PosixGroupId/PosixOwnerSpec, with a total text→id decode that refuses empty, non-numeric and negative lexemes rather than defaulting.extdeps/posix/path_ownership.dag—PathOwnershipObservation/PathOwnershipDecision/ChownAttemptObservation/PathOwnershipEnsureOutcome. Every verdict arm dispatches on the read-back; the chown attempt reaches the outcome only as a receipt field, so a mutation that reported success is never authoritative for state and is never discarded either.extdeps/sudo/elevation.dag—ElevatedInvocationbuilt withlist_append, not a per-element snoc fold (§6 bare-minimum-cost).extdeps/tools/{chown,mkdir,chmod,stat}.dag— one cited upstream each;chmodrecords why additive+xand a replacing octal mode are not interchangeable,statrecords the BSD-fdivergence.gunbc/host_effect_realize.dag— websocat staged per-step with admits/disagreement observations, tool acquisition asSrv3ToolRowreceipts, andadmit_callersseals on the two execution leaves.Compiler defect (operator-admitted).
src/v1/04_infer.dagconstructor_call_admission_diagsunconditionally admitted any caller in the defining module, soadmit_callersconfined cross-module callers only and every permitted list silently under-described its callers. The same-module arm is removed; admission is now exact for every caller. The stage0 mirror was installed from the sanctioned regen producer's candidate tree, not hand-written.The corpus census that the repair forces surfaced one under-declared caller, now admitted explicitly:
fleet_ssh_execution_context_ofonfleet_openssh_trust_policy_seal.Test plan
claim_executor --required-ci --source-root dag --source-root src/v2(the required floor) — the authoritative census for the admission change; run in CI on this branch.srv3_websocat_sequence_witness_test.dag(12),srv3_principal_privilege_witness_test.dag(16),srv3_path_ownership_witness_test.dag(10),srv3_tool_acquisition_witness_test.dag(4),workflow_capability_closure_witness_test.dag. The read-back witness was shown RED under a mutation that reports success while the read-back disagrees.