From 2b2cbaf974679be0708d14b5b2e5af616970d875 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 16:55:37 +0000 Subject: [PATCH 01/16] Correct two gates that describe per-PR enforcement in the present tense 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) --- dag/tools/extdeps_scope_placement_gate.dag | 9 +++++++++ dag/tools/prose_row_introduction_gate.dag | 18 ++++++++++++++++++ 2 files changed, 27 insertions(+) diff --git a/dag/tools/extdeps_scope_placement_gate.dag b/dag/tools/extdeps_scope_placement_gate.dag index 19a72e9e53b..06f92a285c9 100644 --- a/dag/tools/extdeps_scope_placement_gate.dag +++ b/dag/tools/extdeps_scope_placement_gate.dag @@ -20,6 +20,15 @@ import gunbc.extdeps_scope_frontier { DiffAddedObservation, AddedPathsObserved, DiffObserveFailed, DiffParseTruncated, } +// THIS GATE DOES NOT CURRENTLY RUN (measured 2026-08-19): no workflow in .github/workflows/ +// references it, and the only executing CI step is `claim_executor --required-floor`. The note +// below calls it a "server-side per-PR wall" that "refuses" — present tense, and not true today. +// DESIGN's "Building & checks" section already declares the floor cut's bounded rung drop and names +// the effect gates among what is unguarded; this comment carries that fact to the module a reader +// actually opens. Nothing is re-added, deleted, or re-rostered here — only the description is +// corrected. The durable rule this is an instance of is stated in full in +// tools.prose_row_introduction_gate: the .dag call graph is not the execution graph, and "runs in +// CI" is decided by .github/workflows/ and the fold it invokes, never by who calls whom in .dag. data extdeps_scope_placement_gate_note: String = "Server-side per-PR wall for the ExternalModelScope disk-to-roster direction (codex review 46281; modeled on the publication placement gate pattern, whose own gate was deleted by operator ruling in #7591 — this gate is independent and remains). It collects Added/Copied/Renamed paths with git.Core.DiffNameStatus at TWO bases, one per question (scope_placement_base_split_note), and refuses when (a) a dag/extdeps .dag file added by THIS CHANGE — the merge base origin/main...HEAD — is in neither scope_carrier_paths nor scope_machinery_exempt_paths (scope_placement_refused_paths — the frozen manifest is deliberately NOT an admission channel for a new file), (b) any frozen-manifest row names a file added after the freeze anchor, read over the whole post-freeze population at legacy_manifest_freeze_sha..HEAD (manifest_freeze_holds — the smuggling channel), or (c) the change itself ADDS a line to the manifest (manifest_line_observation folded to a verdict by manifest_remove_only_exit, over git.Core.DiffUnified0 against origin/main merge-base — the remove-only lifecycle made mechanical, codex review 46378; the sole admitted arm is the manifest file absent at the merge base, i.e. the PR that first introduces it, unforgeable once it exists on main). Diff failure and parse truncation are refusals, never skips. Merge-base grain on the membership arm is what makes the refusal attributable: only paths the change itself introduces are judged there, so this gate neither retroactively reds the frozen manifest population nor blocks a lane for a file some other lane landed. The wet live-cover witness (dag/test/claim/external_model_scope_live_cover_witness_test.dag) remains the whole-population re-verification. This gate dissolves with the whole storage-grain frontier into the v2.lens.mandatory_tag region promotion (compile-grain, module-name grain)." // ONE fold over a name-status diff, read at two different bases (DESIGN section 2 horizontal: one concept, every breadth). The base is the caller's parameter because WHICH base answers WHICH question is a workflow fact, not a property of the git operation (DESIGN section 3: business policy must not fuse into the extdeps interface). diff --git a/dag/tools/prose_row_introduction_gate.dag b/dag/tools/prose_row_introduction_gate.dag index 0f88394417a..40ba82539e2 100644 --- a/dag/tools/prose_row_introduction_gate.dag +++ b/dag/tools/prose_row_introduction_gate.dag @@ -12,6 +12,24 @@ import gunbc.prose_row_frontier { prose_rows_refused, prose_rows_out_of_scope, prose_rows_render, } +// THIS GATE DOES NOT CURRENTLY RUN, and every present-tense enforcement sentence below describes +// a wall that is not standing (measured 2026-08-19). DESIGN's "Building & checks" section already +// declares this as a bounded rung drop: the floor cut of 2026-08-15 deleted the workflows that +// invoked the effect gates, and names them among what is unguarded until the re-add queue closes. +// The paragraph below was written while the wall stood and was never updated with it, so a session +// reading this module has no reason to doubt a gate it describes in the present tense. Nothing is +// re-added or deleted here: this is the description being corrected to match the mechanism. +// +// THE DURABLE LESSON, recorded here because it is what made the gap invisible and it generalises far +// past this file: THE .dag CALL GRAPH IS NOT THE EXECUTION GRAPH. Post-floor-cut the difference +// between them is most of the repository. Any claim of the form "this runs in CI" is decided by +// .github/workflows/ and the fold those workflows invoke -- today one step, `claim_executor +// --required-floor` -- and 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 with each other was not a second observation, because both had read the same +// artifact. Check the workflow, not the callers. +// +// WHAT FOLLOWS DESCRIBES THE INTENDED WALL: // THE PER-PR WALL over newly introduced prose-only `data NAME_note: String` rows, at the merge base so // the refusal is attributable to the change that caused it. DESIGN 4c makes the class debt; the kernel // in gunbc.prose_row_frontier decides membership; this module is only the execution. From 199791f4c1f69748f1062f3cb1e367f2b4a6d578 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 17:19:42 +0000 Subject: [PATCH 02/16] Refuse the argv representation ambiguity instead of silently resolving 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 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 `. 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) --- src/v1/stage0/src/v1_interpreter.rs | 179 ++++++++++++++++++++++++++++ 1 file changed, 179 insertions(+) diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index cab08e2560e..d43cf2ecf2c 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -3873,6 +3873,131 @@ fn eval_unaryop(op: &UnaryOpKind, val: Value) -> InterpResult { } } +#[cfg(test)] +mod argv_representation_ambiguity_tests { + //! THE RED FOR THE ARGV AMBIGUITY REFUSAL. + //! + //! It is a unit-level construction rather than an executed process, and that is forced rather + //! than chosen: 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. There is + //! no execution to assert against, and a witness that waited for one would assert nothing. + //! + //! What discriminates: both cases below carry the SAME two strings and the SAME declared + //! meaning. Only the runtime representation differs. The native list expands to two argv words; + //! the monoid-encoded form used to collapse to the single word "mainHEAD" and now refuses. + //! Delete the refusal and `monoid_encoded_string_sequence_refuses` fails with one argv word. + use std::rc::Rc; + + use im::{vector as im_vec, HashMap}; + + use crate::v1_compiler_infer_emit_info::empty_emit_graph_info; + use crate::v1_compiler_infer_items::ResolvedGraph; + + use super::{ + list_value, push_shell_argv_tokens, with_active_ctx, ExecutionMode, InterpContext, + InterpError, Value, + }; + + fn fresh_ctx() -> InterpContext { + let graph = ResolvedGraph { + modules: Rc::new(im_vec![]), + item_registry: Rc::new(HashMap::new()), + diagnostics: Rc::new(im_vec![]), + emit_graph_info: empty_emit_graph_info(), + }; + InterpContext::new(&graph, Rc::new(HashMap::new()), ExecutionMode::Hermetic) + } + + /// `Cons { head, tail }` over `Empty` — the representation a fold produces. + fn monoid_of(ctx: &InterpContext, items: &[&str]) -> Value { + let mut cur = Value::Variant { + type_name: ctx.sym("FreeMonoid"), + variant_name: ctx.sym("Empty"), + fields: Rc::new(Vec::new()), + }; + for s in items.iter().rev() { + cur = Value::Variant { + type_name: ctx.sym("FreeMonoid"), + variant_name: ctx.sym("Cons"), + fields: Rc::new(vec![ + (ctx.sym("head"), Value::Str(Rc::from(*s))), + (ctx.sym("tail"), cur), + ]), + }; + } + cur + } + + #[test] + fn native_list_of_two_strings_expands_to_two_argv_words() { + let ctx = fresh_ctx(); + with_active_ctx(&ctx, || { + let mut argv = Vec::new(); + push_shell_argv_tokens( + &mut argv, + list_value(vec![ + Value::Str(Rc::from("main")), + Value::Str(Rc::from("HEAD")), + ]), + ) + .expect("a native list is unambiguous and must expand"); + assert_eq!(argv, vec!["main".to_string(), "HEAD".to_string()]); + }); + } + + #[test] + fn monoid_encoded_string_sequence_refuses() { + let ctx = fresh_ctx(); + with_active_ctx(&ctx, || { + let mut argv = Vec::new(); + let result = push_shell_argv_tokens(&mut argv, monoid_of(&ctx, &["main", "HEAD"])); + match result { + Err(InterpError::TypeError { msg }) => { + assert!( + msg.contains("ambiguous"), + "the refusal must name the ambiguity, got: {msg}" + ); + } + // The pre-refusal behaviour: one concatenated word. Named explicitly so the + // regression is legible rather than appearing as a bare count mismatch. + Ok(()) => panic!( + "expected a refusal; the ambiguity was resolved silently into argv {argv:?} \ + (pre-fix this was the single word \"mainHEAD\")" + ), + Err(other) => panic!("expected a TypeError naming the ambiguity, got {other:?}"), + } + }); + } + + #[test] + fn codepoint_monoid_still_decodes_to_one_word() { + let ctx = fresh_ctx(); + with_active_ctx(&ctx, || { + // An Int-element monoid is a code-point sequence: unambiguous under one reading only, + // so it must keep decoding. This is the control that keeps the refusal from widening + // into every modeled string. + let mut cur = Value::Variant { + type_name: ctx.sym("FreeMonoid"), + variant_name: ctx.sym("Empty"), + fields: Rc::new(Vec::new()), + }; + for c in "hi".chars().rev() { + cur = Value::Variant { + type_name: ctx.sym("FreeMonoid"), + variant_name: ctx.sym("Cons"), + fields: Rc::new(vec![ + (ctx.sym("head"), Value::Int(c as i64)), + (ctx.sym("tail"), cur), + ]), + }; + } + let mut argv = Vec::new(); + push_shell_argv_tokens(&mut argv, cur).expect("a codepoint monoid is a host string"); + assert_eq!(argv, vec!["hi".to_string()]); + }); + } +} + #[cfg(test)] mod eval_int_binop_overflow_tests { use super::{eval_int_binop, InterpError, Value}; @@ -7762,7 +7887,61 @@ fn push_shell_argv_tokens(argv: &mut Vec, val: Value) -> InterpResult<() } Ok(()) } + // THE AMBIGUITY IS REFUSED HERE, NOT RESOLVED — and the two readings really are both + // well-formed, which is why no ordering of the old arms could have been correct. + // + // A free monoid whose elements are `Str` satisfies BOTH readings at once: + // `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, so the previous code silently took the first — meaning + // one declared `List` 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. + // + // The measured specimen: `extdeps.git.git` `git_diff_range_argv` returns `[base, head]` on + // its TwoDot arm, spliced into `git diff -U0 `. Monoid-encoded, that reaches the + // process as `mainHEAD` — and 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 (DESIGN §5). + // + // So this is a state-space conflation, not a missing wall: "one argument whose text is the + // concatenation" and "N arguments" are different states with different remedies, and a + // position that cannot tell them apart must refuse rather than pick. + // + // WHAT DELIBERATELY DOES NOT CHANGE: + // * Int-element monoids stay char-decoded into one word. A code-point sequence is a + // genuine host string under one reading only, so nothing is ambiguous there. + // * A native `Value::List` keeps its N-word expansion (arm above) — it states the list + // reading structurally. + // * `ProcessArgvExpansion` stays authoritative (arm at the top) — it states the role. + // * `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 precisely the forked + // -logic trap this lane exists to remove. The discrimination belongs to the argv + // position, so it lives here. + // + // An EMPTY monoid is treated as the empty string, preserving existing behaviour. Stated + // rather than left implicit: it is the one input where the two readings differ in arity + // (one empty word vs no words) and this arm still picks. It is called out as a deliberate + // narrow choice with no observed consumer, not an oversight. Value::Variant { .. } => { + if let Some(items) = free_monoid_to_vec(&val) { + let has_str_element = items.iter().any(|i| matches!(i, Value::Str(_))); + if has_str_element { + return Err(InterpError::TypeError { + msg: format!( + "argv position {}: a modeled sequence of {} string element(s) is \ + ambiguous here — it reads BOTH as one argument whose text is their \ + concatenation AND as {} separate arguments, and the value records no \ + choice. Refusing rather than picking. Say which is meant: wrap the \ + surface in ProcessArgvExpansion for the argument-list reading, or \ + join the parts explicitly for the single-word reading", + argv.len(), + items.len(), + items.len() + ), + }); + } + } if let Some(s) = value_as_host_string(&val) { argv.push(s); Ok(()) From a8de84f33ed14480ac6ae4ac5531421508dd8565 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 19:03:47 +0000 Subject: [PATCH 03/16] Open the vocabulary axis of realization_vocabulary_containment; falsify 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) --- docs/plans/cli-invocation-emission-design.md | 65 +++++++ .../realization_vocabulary_containment.dag | 162 +++++++++++++++++- .../rest_path_reaches_no_cli_test.dag | 91 ++++++++++ 3 files changed, 310 insertions(+), 8 deletions(-) create mode 100644 src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag diff --git a/docs/plans/cli-invocation-emission-design.md b/docs/plans/cli-invocation-emission-design.md index 48d8c8b5284..11167bb8a0b 100644 --- a/docs/plans/cli-invocation-emission-design.md +++ b/docs/plans/cli-invocation-emission-design.md @@ -1278,3 +1278,68 @@ lane's actual position: single run of all 43 exceeded the 45-minute remote timeout, because every `gunbc run` pays a whole-corpus typecheck. That is a cost-shape observation about the harness, not evidence about the code, and it is recorded rather than left as an unexplained split. + +## 16. The negative falsifier: the REST/CLI boundary becomes a row that reds + +Every prior section of this document asserts, in prose, that the REST path constructs no +process invocation. Prose cannot be contradicted by the tree. This section records the +mechanism that can. + +**The question already had an authority, so no second mechanism was minted.** +`v2.lens.realization_vocabulary_containment` answers "does module X reach construction +vocabulary from set V" and has answered it since the TypeScript-only ratchet. The obstacle +was not that the question was unmodeled but that `V` was a literal: `scan_facts_for_leaks_under` +threads the *importer-path* axis as a parameter while `module_is_target_ast_vocab` was welded +into the predicate. Building a second lens for a second `V` would have been precisely the §3 +duplication this lens exists to detect, so the vocabulary axis was opened instead — the §2 +horizontal move, one axis rather than N copies. + +What that cost, exactly: + +- `RealizationVocabularySet` (name, modules, module_prefixes) and `module_is_in_vocab`. +- `target_ast_vocabulary()` derives from the existing `target_ast_vocab_modules` / + `target_ast_vocab_module_prefixes` rows rather than replacing them — those rows are consumed + directly by `gunbc.realization_vocab_confinement_census`, which has live claims against them. +- `is_vocab_leak_in` / `scan_facts_for_leaks_in` / `vocab_leak_count_in` / `vocab_leak_count_live_in`, + taking vocabulary and exempt-edge population as arguments. Every pre-existing entry point + delegates to these with the target-AST set, so no behavior moved. +- The exempt population is a **parameter**, not a global roster read, so "this vocabulary has + zero admitted exceptions" is a stated fact rather than an accident of the target-AST roster + happening to name no CLI module. + +**Two sites were left target-AST-only, deliberately.** +`realization_vocab_leak_candidate_paths_from_facts` and +`realization_vocab_live_leak_edges_from_facts` feed the grandfathered-roster staleness check, +and every row in that roster is target-AST debt by construction — `RealizationVocabDebtClass` +has no other inhabitant. A second vocabulary reaches the lens with an empty exempt population, +so it has no roster for those projections to be stale against, and parameterizing them now +would produce a staleness answer about a population that does not exist. The trigger is +recorded in-file: the first non-empty exempt roster for a second vocabulary. + +**The subject is not an empty universe** — the usual way a negative claim turns vacuous. The +scanned population (`dag/extdeps/bmc`, `dag/extdeps/transports`) *contains* a module that +legitimately reaches CLI vocabulary: `extdeps.bmc.openbmc_fan_control`, the module this very +lane routes through jq, sitting in the same directory as `extdeps.bmc.redfish`, 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 the positive result is indistinguishable from a scan that read nothing, +which is the empty-observation narrow DESIGN names — ⊥-as-answer conflated with ⊥-as-ignorance. + +The admitted edge is named at exact `(importer_path, vocab_module)` grain rather than by +category or path prefix, so a *second* jq-reaching module anywhere in the scanned roots reds +instead of being absorbed by a pattern broad enough to cover it. + +**What executes, and what does not.** The witness is floor-discovered — it is neither +`long/`-homed nor in `floor_prepared_subject_exclusions` — and its scan is a live read of the +two named directories, so this is corpus data rather than a fixture. It is **not** whole-corpus +coverage: a module outside those roots reaching CLI vocabulary is not seen, and no green here +may be read as saying otherwise. The whole-corpus half of this lens is enrolled on a cadence +that does not currently run, which is a fact about that cadence, not about this witness. Both +halves are stated because a scoped green presented as a general one is the rung inflation §4b +calls worse than sitting low. + +**Where this goes, not scoped here.** The boundary in #8535 is a paragraph today. If this +generalization holds, the natural successor is that the paragraph becomes a row that reds — +which changes what the lens is *for*: not one witness for one lane, but the mechanism by which +a named architectural boundary is enforceable at all. That is a separate change and is +deliberately not attempted in this one. diff --git a/src/v2/lens/realization_vocabulary_containment.dag b/src/v2/lens/realization_vocabulary_containment.dag index 9755917a6d5..e82ebedea1e 100644 --- a/src/v2/lens/realization_vocabulary_containment.dag +++ b/src/v2/lens/realization_vocabulary_containment.dag @@ -143,6 +143,21 @@ fn realization_vocab_edge_from_fact(fact: LayerImportFact) -> RealizationVocabIm } } +// Membership of an edge in an exempt population, with the population supplied. The +// grandfathered-roster reader below is one caller of it, not its definition. +fn realization_vocab_edge_in( + edges: List, + edge: RealizationVocabImportEdge +) -> Bool { + fold_list( + xs: edges, + empty: false, + cons: fn(acc, candidate) { + acc || realization_vocab_import_edge_eq(a: candidate, b: edge) + } + ) +} + fn realization_vocab_edge_grandfathered(edge: RealizationVocabImportEdge) -> Bool { fold_list( xs: realization_vocab_grandfathered_edge_roster, @@ -230,24 +245,80 @@ fn path_has_any_prefix(prefixes: List, path: String) -> Bool { ) } +// THE VOCABULARY AXIS IS AN ARGUMENT, NOT A LITERAL. This lens answers one +// question -- does module X reach construction vocabulary from set V -- and V was +// welded to the target-AST set at every use site. Opening it is the DESIGN section 2 +// horizontal move (one axis, not N copies): a second question about a second +// vocabulary is a row, never a second lens, because a forked lens would be exactly +// the section 3 duplication this mechanism exists to detect. +// +// WHERE THE SETS LIVE, AND WHEN THEY MOVE. A vocabulary set is a fact about the +// vocabulary, not about this lens, so with a third set these rows belong with their +// owning modules. With two they do not: the lens is where a reader currently looks, +// and relocating now would be speculative generality. TRIGGER, not a plan: a third +// set is authored. +type RealizationVocabularySet { + name: String + modules: List + module_prefixes: List +} + +fn module_is_in_vocab(module: String, vocab: RealizationVocabularySet) -> Bool { + list_contains_str(xs: vocab.modules, target: module) + || path_has_any_prefix(prefixes: vocab.module_prefixes, path: module) +} + +fn target_ast_vocabulary() -> RealizationVocabularySet { + RealizationVocabularySet { + name: "target-ast", + modules: target_ast_vocab_modules, + module_prefixes: target_ast_vocab_module_prefixes + } +} + +// THE CLI/PROCESS CONSTRUCTION VOCABULARY. A module reaching these is building a +// process invocation: a jq program plan, a CLI surface, or the argv expansion +// carrier. It is deliberately NOT the bash language vocabulary above -- that set is +// about emitting a target language, this one is about constructing an argument +// vector -- and the two are separate sets rather than one widened set precisely +// because a module may legitimately reach one and not the other. +data cli_process_vocab_modules: List = [ + "extdeps.tools.jq", + "v2.std.compilers.cli_surface", + "extdeps.shell.exec" +] + +data cli_process_vocab_module_prefixes: List = [] + +fn cli_process_vocabulary() -> RealizationVocabularySet { + RealizationVocabularySet { + name: "cli-process", + modules: cli_process_vocab_modules, + module_prefixes: cli_process_vocab_module_prefixes + } +} + fn module_is_target_ast_vocab(module: String) -> Bool { - list_contains_str(xs: target_ast_vocab_modules, target: module) - || path_has_any_prefix(prefixes: target_ast_vocab_module_prefixes, path: module) + module_is_in_vocab(module: module, vocab: target_ast_vocabulary()) } fn path_is_realization_edge(path: String) -> Bool { path_has_any_prefix(prefixes: realization_edge_path_prefixes, path: path) } +// The target-AST binding of the general predicate. It DELEGATES rather than +// restating the fold: leaving a second copy here would be one predicate with two +// implementations, which is the fork this lens exists to detect, one level down. fn is_realization_vocab_leak_under( fact: LayerImportFact, edge_prefixes: List ) -> Bool { - module_is_target_ast_vocab(module: fact.import_module) - && (path_has_any_prefix(prefixes: edge_prefixes, path: fact.path) == false) - && (realization_vocab_edge_grandfathered( - edge: realization_vocab_edge_from_fact(fact: fact) - ) == false) + is_vocab_leak_in( + fact: fact, + vocab: target_ast_vocabulary(), + edge_prefixes: edge_prefixes, + exempt_edges: realization_vocab_grandfathered_edges() + ) } fn is_realization_vocab_leak(fact: LayerImportFact) -> Bool { @@ -274,12 +345,50 @@ fn realization_edge_path_prefixes_without(excluded: String) -> List { fn scan_facts_for_leaks_under( facts: List, edge_prefixes: List +) -> List { + scan_facts_for_leaks_in( + facts: facts, + vocab: target_ast_vocabulary(), + edge_prefixes: edge_prefixes, + exempt_edges: realization_vocab_grandfathered_edges() + ) +} + +// THE GENERALIZED SCAN. Same predicate, same fold, with the vocabulary and the +// exempt-edge population supplied by the caller instead of read from a literal. The +// exemptions are a PARAMETER rather than a global roster read because "this +// vocabulary has zero admitted exceptions" must be a stated fact rather than an +// accident of the target-AST roster happening not to name any CLI module. +fn is_vocab_leak_in( + fact: LayerImportFact, + vocab: RealizationVocabularySet, + edge_prefixes: List, + exempt_edges: List +) -> Bool { + module_is_in_vocab(module: fact.import_module, vocab: vocab) + && (path_has_any_prefix(prefixes: edge_prefixes, path: fact.path) == false) + && (realization_vocab_edge_in( + edges: exempt_edges, + edge: realization_vocab_edge_from_fact(fact: fact) + ) == false) +} + +fn scan_facts_for_leaks_in( + facts: List, + vocab: RealizationVocabularySet, + edge_prefixes: List, + exempt_edges: List ) -> List { fold_list( xs: facts, empty: empty_realization_vocab_leaks, cons: fn(acc, fact) { - if is_realization_vocab_leak_under(fact: fact, edge_prefixes: edge_prefixes) { + if is_vocab_leak_in( + fact: fact, + vocab: vocab, + edge_prefixes: edge_prefixes, + exempt_edges: exempt_edges + ) { list_snoc_item( xs: acc, item: RealizationVocabularyLeak { @@ -294,6 +403,34 @@ fn scan_facts_for_leaks_under( ) } +fn vocab_leak_count_in( + facts: List, + vocab: RealizationVocabularySet, + edge_prefixes: List, + exempt_edges: List +) -> Int { + length(xs: scan_facts_for_leaks_in( + facts: facts, + vocab: vocab, + edge_prefixes: edge_prefixes, + exempt_edges: exempt_edges + )) +} + +fn vocab_leak_count_live_in( + scan_roots: List, + vocab: RealizationVocabularySet, + edge_prefixes: List, + exempt_edges: List +) -> Int { + vocab_leak_count_in( + facts: layer_import_facts_live(std_roots: scan_roots, extdeps_roots: []), + vocab: vocab, + edge_prefixes: edge_prefixes, + exempt_edges: exempt_edges + ) +} + fn realization_vocab_leak_count(facts: List) -> Int { length(xs: scan_facts_for_leaks_under(facts: facts, edge_prefixes: realization_edge_path_prefixes)) } @@ -329,6 +466,15 @@ fn realization_vocab_containment_clean_live(scan_roots: List) -> Bool { ) } +// DELIBERATELY TARGET-AST-ONLY, decided rather than left welded. These two +// projections exist to feed the grandfathered-roster staleness check, and every row +// in that roster is target-AST debt by construction -- RealizationVocabDebtClass has +// no other inhabitant. A second vocabulary reaches this lens with an EMPTY exempt +// population supplied at the call site, so it has no roster for these to be stale +// against, and parameterizing them now would produce a staleness answer about a +// population that does not exist. TRIGGER: the first non-empty exempt roster for a +// second vocabulary is authored, at which point these take the same argument the +// scan already takes. fn realization_vocab_leak_candidate_paths_from_facts(facts: List) -> List { fold_list( xs: facts, diff --git a/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag new file mode 100644 index 00000000000..7a50e5c77ef --- /dev/null +++ b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag @@ -0,0 +1,91 @@ +module v2.test.realization_vocabulary_containment.cli_vocabulary.rest_path_reaches_no_cli + +// THE NEGATIVE FALSIFIER FOR THE REST/CLI BOUNDARY. +// +// The claim under test is the one the argv lane keeps asserting in prose: a +// Redfish/REST path constructs no process invocation -- no jq program, no CLI +// surface, no argv expansion carrier. Prose cannot be contradicted by the tree. +// This can. +// +// WHY THIS IS A FALSIFIER AND NOT A DECORATION. A witness asserting that the REST +// path constructs a REST carrier restates a type signature: it cannot fail for the +// reason anyone cares about. The failure this watches for is a CLI carrier +// APPEARING where none should, so the assertion is over the vocabulary a module +// reaches, and it reds when a new module in the scanned population reaches CLI +// construction vocabulary. +// +// THE SUBJECT IS NOT AN EMPTY UNIVERSE, which is the usual way a negative claim +// turns vacuous. The scanned population CONTAINS a module that legitimately reaches +// this vocabulary -- extdeps.bmc.openbmc_fan_control, which the argv lane routes +// through jq deliberately -- sitting in the same directory as extdeps.bmc.redfish, +// which does not. So the scan discriminates WITHIN the population rather than over +// a population where nothing could have been found, and the RED control below is +// real corpus data rather than a planted fixture. +// +// WHAT EXECUTES AND WHAT DOES NOT. This witness is discovered by the floor and its +// scan is a live read of the two named directories. It is NOT whole-corpus +// coverage: a module outside these roots reaching CLI vocabulary is not seen here, +// and no green from this file may be read as saying otherwise. The whole-corpus +// half of this lens is enrolled on a cadence that does not currently run, which is +// a fact about that cadence and not about this witness. + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// The REST/BMC transport population. Both directories, because the boundary claim +// is about the transport layer as a whole rather than one file. +data rest_path_scan_roots: List = [ + "dag/extdeps/bmc", + "dag/extdeps/transports" +] + +// THE ONE ADMITTED EDGE, named at exact identity grain. This is not a category or a +// path prefix: it is one importer reaching one vocabulary module, so a SECOND +// jq-reaching module anywhere in the scanned roots reds rather than being absorbed +// by a pattern broad enough to cover it. The admission exists because the fan +// control path's transport genuinely is a CLI process today; it is the subject of +// the argv lane, not an exception to the boundary. +data fan_control_admitted_cli_edges: List = [ + RealizationVocabImportEdge { + importer_path: "dag/extdeps/bmc/openbmc_fan_control.dag", + vocab_module: "extdeps.tools.jq" + } +] + +data no_admitted_cli_edges: List = [] + +// POSITIVE: everything in the REST/BMC transport population except the one admitted +// edge reaches no CLI construction vocabulary. +test fn rest_path_reaches_no_cli_construction_vocabulary() -> Bool { + vocab_leak_count_live_in( + scan_roots: rest_path_scan_roots, + vocab: cli_process_vocabulary(), + edge_prefixes: [], + exempt_edges: fan_control_admitted_cli_edges + ) == 0 +} + +// RED CONTROL, from live corpus data rather than a fixture: withdraw the admission +// and the scan must FIND the fan control edge. Without this the positive above is +// indistinguishable from a scan that reads nothing -- an empty result and a clean +// result are different states, and only this assertion separates them. +test fn withdrawing_the_admission_surfaces_the_known_cli_edge() -> Bool { + vocab_leak_count_live_in( + scan_roots: rest_path_scan_roots, + vocab: cli_process_vocabulary(), + edge_prefixes: [], + exempt_edges: no_admitted_cli_edges + ) == 1 +} + +// SECOND RED, on the other axis: the scan must not be blind to the vocabulary set +// itself. The same roots scanned for TARGET-AST vocabulary also report zero, so the +// two sets are genuinely separate questions over one mechanism rather than one +// question answered twice. +test fn rest_path_reaches_no_target_ast_vocabulary() -> Bool { + vocab_leak_count_live_in( + scan_roots: rest_path_scan_roots, + vocab: target_ast_vocabulary(), + edge_prefixes: [], + exempt_edges: no_admitted_cli_edges + ) == 0 +} From 81fe0c55f57ed465c501582ceaaa41dae0676ae2 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 19:48:14 +0000 Subject: [PATCH 04/16] Widen the CLI-vocabulary falsifier root by root; every clean root carries 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) --- .../realization_vocabulary_containment.dag | 9 ++ .../rest_path_reaches_no_cli_test.dag | 94 +++++++++++++++++++ 2 files changed, 103 insertions(+) diff --git a/src/v2/lens/realization_vocabulary_containment.dag b/src/v2/lens/realization_vocabulary_containment.dag index e82ebedea1e..d28bb1b122c 100644 --- a/src/v2/lens/realization_vocabulary_containment.dag +++ b/src/v2/lens/realization_vocabulary_containment.dag @@ -417,6 +417,15 @@ fn vocab_leak_count_in( )) } +// NON-VACUITY PRIMITIVE. A clean root and a root the scan never read both report +// zero leaks, and those are different states -- bottom-as-answer against +// bottom-as-ignorance, the empty-observation narrow. Counting the facts the scan +// actually acquired is what separates them, so a widened root set can prove it read +// something rather than assert it. +fn vocab_scan_fact_count_live(scan_roots: List) -> Int { + length(xs: layer_import_facts_live(std_roots: scan_roots, extdeps_roots: [])) +} + fn vocab_leak_count_live_in( scan_roots: List, vocab: RealizationVocabularySet, diff --git a/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag index 7a50e5c77ef..90500f293bf 100644 --- a/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag +++ b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag @@ -89,3 +89,97 @@ test fn rest_path_reaches_no_target_ast_vocabulary() -> Bool { exempt_edges: no_admitted_cli_edges ) == 0 } + +// --------------------------------------------------------------------------- +// WIDENING, ROOT BY ROOT. The boundary above is enforced in two directories and +// prose everywhere else, which is the whole of its limitation. Each root below is a +// SEPARATE assertion rather than one widened list, so a failure names the root that +// broke instead of reporting that something, somewhere, reaches CLI vocabulary. +// --------------------------------------------------------------------------- + +// The paths permitted to reach CLI construction vocabulary because constructing a +// CLI surface is what they are FOR. This is the lens's existing realization-edge +// mechanism used as designed: jq's own extdeps module defines the jq CLI surface, +// so its edge to cli_surface is internal to the vocabulary rather than a leak out of +// anywhere. Note this is a PATH prefix and the fan control admission is an exact +// edge -- the difference is deliberate: a definition site is a location whose whole +// purpose is this vocabulary, while an admission is one consumer that happens to +// need it and must not silently become two. +data cli_vocab_definition_edges: List = [ + "dag/extdeps/tools/jq.dag", + "src/v2/std/compilers/cli_surface.dag" +] + +// ROOT: all of dag/extdeps. Widens past bmc/ and transports/ to every cited +// upstream module. Lands with exactly one admitted edge -- the fan control jq +// edge already named above -- and the jq definition site on the edge roster. +data extdeps_scan_roots: List = [ + "dag/extdeps" +] + +test fn extdeps_reaches_no_cli_construction_vocabulary() -> Bool { + vocab_leak_count_live_in( + scan_roots: extdeps_scan_roots, + vocab: cli_process_vocabulary(), + edge_prefixes: cli_vocab_definition_edges, + exempt_edges: fan_control_admitted_cli_edges + ) == 0 +} + +// ROOT: the compiler substrate. This is the strongest claim in the file and the one +// with no admissions at all: std, the compiler stages, the lenses and the workflow +// layer construct no process invocation whatsoever. If any of these ever needs a +// CLI surface, that is an architectural event and it should red here first. +data substrate_scan_roots: List = [ + "src/v2/std", + "src/v2/compiler", + "src/v2/lens", + "src/v2/workflow" +] + +test fn compiler_substrate_reaches_no_cli_construction_vocabulary() -> Bool { + vocab_leak_count_live_in( + scan_roots: substrate_scan_roots, + vocab: cli_process_vocabulary(), + edge_prefixes: cli_vocab_definition_edges, + exempt_edges: no_admitted_cli_edges + ) == 0 +} + +// NON-VACUITY, and it is why the two clean results above mean anything. A root the +// scan never read reports zero leaks exactly as a clean root does. These assert the +// scans acquired real facts, so a zero is a finding rather than a silence -- the +// same distinction the withdraw-the-admission control makes for the REST roots, +// made here for roots that have no known edge to withdraw. +test fn widened_scans_actually_read_the_tree() -> Bool { + (vocab_scan_fact_count_live(scan_roots: extdeps_scan_roots) > 0) + && (vocab_scan_fact_count_live(scan_roots: substrate_scan_roots) > 0) + && (vocab_scan_fact_count_live(scan_roots: rest_path_scan_roots) > 0) +} + +// DISCRIMINATION FOR THE WIDENED ROOT, not just the narrow one. A nonzero fact +// count proves the extdeps scan read SOMETHING; it does not prove it descended into +// bmc/ where the only known edge lives. Withdrawing the admission over the WIDE root +// must surface that edge exactly as it does over the narrow one -- otherwise +// "dag/extdeps is clean" could be clean because the subtree containing the one dirty +// module was never reached. +test fn withdrawing_the_admission_surfaces_the_edge_under_the_wide_root() -> Bool { + vocab_leak_count_live_in( + scan_roots: extdeps_scan_roots, + vocab: cli_process_vocabulary(), + edge_prefixes: cli_vocab_definition_edges, + exempt_edges: no_admitted_cli_edges + ) == 1 +} + +// AND THE EDGE ROSTER ITSELF MUST BE LOAD-BEARING. Drop the jq definition site from +// the permitted paths and the count must RISE, which is what proves that roster is +// admitting a real edge rather than naming a path the scan never had a fact for. +test fn dropping_the_definition_edge_roster_surfaces_more() -> Bool { + vocab_leak_count_live_in( + scan_roots: extdeps_scan_roots, + vocab: cli_process_vocabulary(), + edge_prefixes: [], + exempt_edges: fan_control_admitted_cli_edges + ) > 0 +} From 85e761d2d34231c903258a59ce950b71b6adb7e6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 20:08:57 +0000 Subject: [PATCH 05/16] Close the last roots: the #8535 boundary now reds, stated as infrastructure-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) --- .../rest_path_reaches_no_cli_test.dag | 125 ++++++++++++++++++ 1 file changed, 125 insertions(+) diff --git a/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag index 90500f293bf..658097103fc 100644 --- a/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag +++ b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag @@ -183,3 +183,128 @@ test fn dropping_the_definition_edge_roster_surfaces_more() -> Bool { exempt_edges: fan_control_admitted_cli_edges ) > 0 } + +// --------------------------------------------------------------------------- +// ROOT: dag/gunbc, and the rule the whole boundary reduces to. +// +// REALIZATION INFRASTRUCTURE MAY REACH TRANSPORT VOCABULARY; CONSUMERS MAY NOT, +// EXCEPT BY EXACT NAMED ADMISSION. That is the #8535 boundary in a form that reds. +// The prose version says CLI-backed handlers are one realization cell; this says +// which modules ARE that cell and refuses the rest by name. +// +// The six modules here reaching extdeps.shell.exec are two different things, and +// the split is by what the module IS rather than by what it imports. +// --------------------------------------------------------------------------- + +// Realization infrastructure. Reaching transport vocabulary is what these locations +// are FOR, which is the same reason the jq definition site is path-rostered above -- +// same rule, same shape. retained_shell_script defines the counted bridges and calls +// transport_script_seal; bash_materialized_transport is the only other +// admit_callers-sealed caller of that seal; host_effect_realize is the realization +// core and reaches the vocabulary through retained_srvn. +data transport_realization_edges: List = [ + "dag/gunbc/retained_shell_script.dag", + "dag/gunbc/bash_materialized_transport.dag", + "dag/gunbc/host_effect_realize.dag" +] + +// CONSUMERS HOLDING A TRANSPORT, admitted as exact pairs so that a SEVENTH consumer +// reds instead of being absorbed by a prefix broad enough to cover it. +// +// The reason on each is the finding, not a justification: all three reach the +// vocabulary 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. So the admission records a bucket that is probably +// wrong rather than laundering it, and when someone fixes the bucket the admission +// comes OFF instead of being re-justified. +// +// This population was reached twice independently: by a retained_foreign call census +// (#8535) 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. +data transport_consumer_admitted_edges: List = [ + RealizationVocabImportEdge { + importer_path: "dag/gunbc/package_delivery.dag", + vocab_module: "extdeps.shell.exec" + }, + RealizationVocabImportEdge { + importer_path: "dag/gunbc/codex_app_server_press.dag", + vocab_module: "extdeps.shell.exec" + }, + RealizationVocabImportEdge { + importer_path: "dag/gunbc/provider_wire_evidence.dag", + vocab_module: "extdeps.shell.exec" + } +] + +data gunbc_scan_roots: List = [ + "dag/gunbc" +] + +test fn gunbc_consumers_reach_transport_vocabulary_only_by_named_admission() -> Bool { + vocab_leak_count_live_in( + scan_roots: gunbc_scan_roots, + vocab: cli_process_vocabulary(), + edge_prefixes: transport_realization_edges, + exempt_edges: transport_consumer_admitted_edges + ) == 0 +} + +// DISCRIMINATION AT THIS SCOPE, established here rather than inherited. See the +// general rule below -- this is the control the rule exists to make mandatory. +test fn withdrawing_the_consumer_admissions_surfaces_exactly_three() -> Bool { + vocab_leak_count_live_in( + scan_roots: gunbc_scan_roots, + vocab: cli_process_vocabulary(), + edge_prefixes: transport_realization_edges, + exempt_edges: no_admitted_cli_edges + ) == 3 +} + +// The realization-edge roster must be load-bearing too: drop it and the count rises +// past the three consumers, proving those paths carry facts the scan really saw. +test fn dropping_the_transport_realization_roster_surfaces_more() -> Bool { + vocab_leak_count_live_in( + scan_roots: gunbc_scan_roots, + vocab: cli_process_vocabulary(), + edge_prefixes: [], + exempt_edges: transport_consumer_admitted_edges + ) > 0 +} + +// ROOT: dag/test. Path-rostered, and the reason is plain -- these are the witnesses +// that exercise this vocabulary deliberately, including the ones proving the argv +// refusal and the jq lowering. A test that could not import the thing it tests would +// be a test of nothing. Stated as a roster rather than left as an unscanned gap, so +// the exclusion is visible instead of implied by absence. +data witness_exercise_edges: List = [ + "dag/test/" +] + +test fn test_corpus_reaches_cli_vocabulary_only_as_declared_exercise() -> Bool { + vocab_leak_count_live_in( + scan_roots: ["dag/test"], + vocab: cli_process_vocabulary(), + edge_prefixes: witness_exercise_edges, + exempt_edges: no_admitted_cli_edges + ) == 0 +} + +// --------------------------------------------------------------------------- +// THE GENERAL RULE FOR WIDENING, written down because the next person to add 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 control proves the scan discriminates over THAT root. Widen the +// root 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. This was +// caught here under a green -- dag/extdeps reported clean and would have reported +// clean had bmc/ never been reached at all. +// +// So every root added carries, at its own scope: a withdrawal control with an exact +// expected count, and a roster-drop control asserting the count RISES. The second is +// the same question aimed at the roster instead of the scan, and it matters because +// an edge roster that no fact matches is indistinguishable from a correct one. +// --------------------------------------------------------------------------- From d3543f9cb2e0373b3401fb5c05f6af23f9ef7e0f Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 20:38:58 +0000 Subject: [PATCH 06/16] Model the local process-argv seam; fix the trailing-annotation refusal 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) --- dag/extdeps/shell/exec.dag | 130 +++++++++++++++++- .../rest_path_reaches_no_cli_test.dag | 46 ++++--- 2 files changed, 156 insertions(+), 20 deletions(-) diff --git a/dag/extdeps/shell/exec.dag b/dag/extdeps/shell/exec.dag index c2d31827f0d..06c24ab03f9 100644 --- a/dag/extdeps/shell/exec.dag +++ b/dag/extdeps/shell/exec.dag @@ -1,6 +1,7 @@ module extdeps.shell.exec -import std.types { String } +import std.types { String, Int, Bool, NonEmptyStr } +import v2.std.compilers.cli_surface { ProcessArgvExpansion } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } import extdeps.exec.exec_arg_limit { host_exec_arg_max_strlen } @@ -76,6 +77,58 @@ service shell.Exec { } } + // --------------------------------------------------------------------------------------------- + // THE LOCAL PROCESS-ARGV SEAM. Run above is argv ["bash", "-s"] with the script on stdin -- the + // heredoc path -- so every local ArgvCommand in the corpus currently renders its argv to quoted + // TEXT and hands that text to a shell, which parses it back into an argument vector. The seed + // does Command::new(&argv[0]).args(&argv[1..]) at the far end regardless, so the round trip + // through shell quoting buys nothing and costs the one thing argv-as-serialization exists to + // stop: a re-parse where the boundary between arguments is inferred from text instead of carried. + // + // THE PROGRAM IS NOT AN ARGUMENT, which is why it is a separate input rather than the first + // element of the expansion. Two reasons, and the second is the load-bearing one. execve takes + // the executable and the argument vector as distinct parameters; conflating them is the same + // state-space collapse this lane keeps removing. And with the program separate, an EMPTY argv is + // unconstructible -- a NonEmptyStr program means there is always an argv[0], so the unspawnable + // empty vector has no representation here rather than being refused after the fact. + operation RunArgv { + input { program: NonEmptyStr, arguments: ProcessArgvExpansion } + + // NO success: Bool FIELD, DELIBERATELY, and this is the output-shape decision stated where it + // is made. `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 forces every caller to re-derive that judgement from a field that already threw the + // information away, and lets a refusal read as empty output, which is precisely the confusion + // run_shell_command_capture's callers live with today. + // + // So the wire carries the honest triple -- a wire returns scalars, it cannot return a + // coproduct -- and the typed outcome is decoded immediately above it by + // classify_process_observation, against a policy the caller declares. That is not a new + // pattern: it is the one already landed for jq (jq_classify_observation / JqExitPolicy / + // JqOutcome), reused rather than re-coined. + output { + exit_code: Int from "exit_code" + stdout: String from "stdout" + stderr: String from "stderr" + } + + // The argv IS the expansion, spliced one word per CliArgument, with no shell between the + // carrier and the process. Nothing here is quoted, joined, or re-parsed. + transport shell { + argv: [program, arguments] + } + + // A nonzero exit is DATA, not an error. Refusing here would hard-code one exit policy into the + // seam and make every legitimate nonzero convention unreachable. + exit { + 0 => Unit + nonzero => Unit + } + mock_response { + 0 => { exit_code: 0, stdout: "", stderr: "" } "hermetic shell.Exec.RunArgv success" + } + } + operation Check { input { command: TransportScript } output { exists: Bool from "exit_success" } @@ -91,3 +144,78 @@ service shell.Exec { } } } + +// ------------------------------------------------------------------------------------------- +// DECODING THE OBSERVATION, immediately above the wire. +// +// The seam returns three scalars because that is what a process gives back. Correlating them is +// a decision, and it belongs in one place rather than at each of the twenty-five call sites that +// currently do it by hand. +// ------------------------------------------------------------------------------------------- + +type ProcessObservation { + exit_code: Int + stdout: String + stderr: String +} + +fn process_observation(exit_code: Int, stdout: String, stderr: String) -> ProcessObservation { + ProcessObservation { exit_code: exit_code, stdout: stdout, stderr: stderr } +} + +// CONVERGENCE OWED, declared rather than left for someone to notice. extdeps.tools.jq carries +// JqOutcome / JqExitPolicy / jq_classify_observation, which are this same pair specialized to one +// tool -- JqOutputPresent, JqOutputAbsent, JqExecutionRefused against the general variants above. +// Two names for one concept is the nicknaming DESIGN section 3 forbids, and the correct end state +// is that jq's policy becomes a ProcessExitPolicy row (its 4-means-absent rule is a third variant +// this type does not yet carry) and JqOutcome dissolves into ProcessOutcome. +// +// It is NOT done in this change, and the reason is scope rather than difficulty: jq's classifier +// is landed, reviewed and consumed by witnesses, so folding it in belongs with the consumer +// migration that motivates it rather than inside the operation that models the seam. +// DISSOLVE-ON: the first consumer migrated onto RunArgv, at which point both classifiers have a +// live caller and the merge is a refactor with execution behind it rather than a speculative one. + +// WHAT THE CALLER WANTS FROM THE PROCESS, which is the thing a bare Bool cannot say. Callers of +// the current run_shell_command_capture split into two populations that a success flag renders +// identically: those for whom stdout IS the product (ssh-keyscan, ssh-keygen -lf) and those for +// whom the exit status is the product. For the first, "refused" and "produced nothing" are +// different answers with different remedies, and a refusal that reads as empty output is the +// fabricated plausible output DESIGN forbids -- an empty string is a legitimate value, so nothing +// downstream can tell it apart from a failure. +type ProcessOutcome + = ProcessOutputPresent { text: String } + | ProcessOutputAbsent + | ProcessRefused { exit_code: Int, stderr: String } + +// The policy is DECLARED by the caller because there is no universal one -- that is the whole +// reason `success` is not a field on the operation. ExitZeroSucceeds is the ordinary convention; +// ExitZeroOrOneSucceeds covers the diff/grep family where 1 means "no match" rather than failure. +type ProcessExitPolicy + = ExitZeroSucceeds + | ExitZeroOrOneSucceeds + +fn process_exit_is_admitted(policy: ProcessExitPolicy, exit_code: Int) -> Bool { + match policy { + ExitZeroSucceeds => exit_code == 0 + ExitZeroOrOneSucceeds => (exit_code == 0) || (exit_code == 1) + } +} + +// An admitted exit with empty stdout is ABSENT, not present-and-empty. That distinction is the +// point of the coproduct: a caller matching on ProcessOutputPresent cannot silently receive the +// empty string where a refusal occurred, because a refusal is not that variant. +fn classify_process_observation( + policy: ProcessExitPolicy, + observation: ProcessObservation +) -> ProcessOutcome { + if process_exit_is_admitted(policy: policy, exit_code: observation.exit_code) { + if observation.stdout == "" { + ProcessOutputAbsent + } else { + ProcessOutputPresent { text: observation.stdout } + } + } else { + ProcessRefused { exit_code: observation.exit_code, stderr: observation.stderr } + } +} diff --git a/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag index 658097103fc..3a90a5313b4 100644 --- a/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag +++ b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag @@ -107,9 +107,35 @@ test fn rest_path_reaches_no_target_ast_vocabulary() -> Bool { // need it and must not silently become two. data cli_vocab_definition_edges: List = [ "dag/extdeps/tools/jq.dag", - "src/v2/std/compilers/cli_surface.dag" + "src/v2/std/compilers/cli_surface.dag", + // Added when shell.Exec.RunArgv landed, and worth recording HOW rather than just + // that it was: this witness redded on the change that introduced the edge. The + // module is itself a member of cli_process_vocab_modules, so its reach into + // cli_surface is internal to the vocabulary rather than a leak out of anywhere -- + // the same footing as jq's module, which also defines a CLI surface for the tool + // it wraps. A roster entry added because a real scan refused is a different thing + // from one added in anticipation, and only the first kind has been tested. + "dag/extdeps/shell/exec.dag" ] +// --------------------------------------------------------------------------- +// THE GENERAL RULE FOR WIDENING, written down because the next person to add 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 control proves the scan discriminates over THAT root. Widen the +// root 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. This was +// caught here under a green -- dag/extdeps reported clean and would have reported +// clean had bmc/ never been reached at all. +// +// So every root added carries, at its own scope: a withdrawal control with an exact +// expected count, and a roster-drop control asserting the count RISES. The second is +// the same question aimed at the roster instead of the scan, and it matters because +// an edge roster that no fact matches is indistinguishable from a correct one. +// --------------------------------------------------------------------------- + // ROOT: all of dag/extdeps. Widens past bmc/ and transports/ to every cited // upstream module. Lands with exactly one admitted edge -- the fan control jq // edge already named above -- and the jq definition site on the edge roster. @@ -290,21 +316,3 @@ test fn test_corpus_reaches_cli_vocabulary_only_as_declared_exercise() -> Bool { exempt_edges: no_admitted_cli_edges ) == 0 } - -// --------------------------------------------------------------------------- -// THE GENERAL RULE FOR WIDENING, written down because the next person to add 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 control proves the scan discriminates over THAT root. Widen the -// root 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. This was -// caught here under a green -- dag/extdeps reported clean and would have reported -// clean had bmc/ never been reached at all. -// -// So every root added carries, at its own scope: a withdrawal control with an exact -// expected count, and a roster-drop control asserting the count RISES. The second is -// the same question aimed at the roster instead of the scan, and it matters because -// an edge roster that no fact matches is indistinguishable from a correct one. -// --------------------------------------------------------------------------- From 66a7e3a131858da13ccdf68597c82c3e8a952234 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 20:51:42 +0000 Subject: [PATCH 07/16] Move seam rationale to module-item grain; annotations are not admitted 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) --- dag/extdeps/shell/exec.dag | 59 +++++++++---------- .../rest_path_reaches_no_cli_test.dag | 15 ++--- 2 files changed, 37 insertions(+), 37 deletions(-) diff --git a/dag/extdeps/shell/exec.dag b/dag/extdeps/shell/exec.dag index 06c24ab03f9..e4b5b48b770 100644 --- a/dag/extdeps/shell/exec.dag +++ b/dag/extdeps/shell/exec.dag @@ -53,6 +53,35 @@ data shell_exec_check_argv_embed_note: String = "shell.Exec.Check transport: arg data shell_exec_transport_ceiling_authority: ByteSize = host_exec_arg_max_strlen +// THE LOCAL PROCESS-ARGV SEAM (shell.Exec.RunArgv, declared in the service below). +// +// Run is argv ["bash", "-s"] with the script on stdin -- the heredoc path -- so every local +// ArgvCommand in the corpus renders its argv to quoted TEXT and hands that text to a shell, which +// parses it back into an argument vector. The seed does Command::new(&argv[0]).args(&argv[1..]) at +// the far end regardless, so the round trip through shell quoting buys nothing and costs the one +// thing argv-as-serialization exists to stop: a re-parse where the boundary between arguments is +// inferred from text instead of carried. +// +// THE PROGRAM IS NOT AN ARGUMENT, which is why RunArgv takes it as a separate input rather than as +// the first element of the expansion. execve takes the executable and the argument vector as +// distinct parameters; conflating them is the same state-space collapse this lane keeps removing. +// And with the program separate and NonEmptyStr, an EMPTY argv is unconstructible -- there is +// always an argv[0], so the unspawnable empty vector has no representation here rather than being +// refused after the fact. +// +// NO success: Bool FIELD, DELIBERATELY. `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 forces every caller to re-derive that judgement from a field that +// already threw the information away, and lets a refusal read as empty output. So the wire carries +// the honest triple -- a wire returns scalars, it cannot return a coproduct -- and the typed +// outcome is decoded immediately above it by classify_process_observation against a policy the +// caller declares. That is the pattern already landed for jq (jq_classify_observation / +// JqExitPolicy / JqOutcome), reused rather than re-coined. +// +// The argv IS the expansion, spliced one word per CliArgument, with no shell between the carrier +// and the process: nothing is quoted, joined, or re-parsed. A nonzero exit is DATA, not an error -- +// refusing there would hard-code one exit policy into the seam and make every legitimate nonzero +// convention unreachable. service shell.Exec { operation Run { input { script: TransportScript } @@ -77,49 +106,19 @@ service shell.Exec { } } - // --------------------------------------------------------------------------------------------- - // THE LOCAL PROCESS-ARGV SEAM. Run above is argv ["bash", "-s"] with the script on stdin -- the - // heredoc path -- so every local ArgvCommand in the corpus currently renders its argv to quoted - // TEXT and hands that text to a shell, which parses it back into an argument vector. The seed - // does Command::new(&argv[0]).args(&argv[1..]) at the far end regardless, so the round trip - // through shell quoting buys nothing and costs the one thing argv-as-serialization exists to - // stop: a re-parse where the boundary between arguments is inferred from text instead of carried. - // - // THE PROGRAM IS NOT AN ARGUMENT, which is why it is a separate input rather than the first - // element of the expansion. Two reasons, and the second is the load-bearing one. execve takes - // the executable and the argument vector as distinct parameters; conflating them is the same - // state-space collapse this lane keeps removing. And with the program separate, an EMPTY argv is - // unconstructible -- a NonEmptyStr program means there is always an argv[0], so the unspawnable - // empty vector has no representation here rather than being refused after the fact. operation RunArgv { input { program: NonEmptyStr, arguments: ProcessArgvExpansion } - // NO success: Bool FIELD, DELIBERATELY, and this is the output-shape decision stated where it - // is made. `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 forces every caller to re-derive that judgement from a field that already threw the - // information away, and lets a refusal read as empty output, which is precisely the confusion - // run_shell_command_capture's callers live with today. - // - // So the wire carries the honest triple -- a wire returns scalars, it cannot return a - // coproduct -- and the typed outcome is decoded immediately above it by - // classify_process_observation, against a policy the caller declares. That is not a new - // pattern: it is the one already landed for jq (jq_classify_observation / JqExitPolicy / - // JqOutcome), reused rather than re-coined. output { exit_code: Int from "exit_code" stdout: String from "stdout" stderr: String from "stderr" } - // The argv IS the expansion, spliced one word per CliArgument, with no shell between the - // carrier and the process. Nothing here is quoted, joined, or re-parsed. transport shell { argv: [program, arguments] } - // A nonzero exit is DATA, not an error. Refusing here would hard-code one exit policy into the - // seam and make every legitimate nonzero convention unreachable. exit { 0 => Unit nonzero => Unit diff --git a/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag index 3a90a5313b4..c6b7937ff41 100644 --- a/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag +++ b/src/v2/test/claim/realization_vocabulary_containment/cli_vocabulary/rest_path_reaches_no_cli_test.dag @@ -105,16 +105,17 @@ test fn rest_path_reaches_no_target_ast_vocabulary() -> Bool { // edge -- the difference is deliberate: a definition site is a location whose whole // purpose is this vocabulary, while an admission is one consumer that happens to // need it and must not silently become two. +// The third entry was added when shell.Exec.RunArgv landed, and it is worth +// recording HOW rather than just that it happened: this witness REDDED on the +// change that introduced the edge. exec.dag is itself a member of +// cli_process_vocab_modules, so its reach into cli_surface is internal to the +// vocabulary rather than a leak out of anywhere -- the same footing as jq's +// module, which also defines a CLI surface for the tool it wraps. A roster entry +// added because a real scan refused is a different thing from one added in +// anticipation, and only the first kind has been tested. data cli_vocab_definition_edges: List = [ "dag/extdeps/tools/jq.dag", "src/v2/std/compilers/cli_surface.dag", - // Added when shell.Exec.RunArgv landed, and worth recording HOW rather than just - // that it was: this witness redded on the change that introduced the edge. The - // module is itself a member of cli_process_vocab_modules, so its reach into - // cli_surface is internal to the vocabulary rather than a leak out of anywhere -- - // the same footing as jq's module, which also defines a CLI surface for the tool - // it wraps. A roster entry added because a real scan refused is a different thing - // from one added in anticipation, and only the first kind has been tested. "dag/extdeps/shell/exec.dag" ] From 4bd7afe29a6d0e2fb93001356c8038b9c55a7e7e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 22:40:07 +0000 Subject: [PATCH 08/16] File the finding: admit_callers on a service operation is accepted and 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) --- ...ation_admit_callers_inert_witness_test.dag | 88 +++++++++++++++++++ src/v2/workflow/floor_expected_red.dag | 2 +- 2 files changed, 89 insertions(+), 1 deletion(-) create mode 100644 dag/test/claim/operation_admit_callers_inert_witness_test.dag diff --git a/dag/test/claim/operation_admit_callers_inert_witness_test.dag b/dag/test/claim/operation_admit_callers_inert_witness_test.dag new file mode 100644 index 00000000000..94281161fbe --- /dev/null +++ b/dag/test/claim/operation_admit_callers_inert_witness_test.dag @@ -0,0 +1,88 @@ +module test.claim.operation_admit_callers_inert_witness + +import std.types { String, Bool, Int } +import v2.std.optional { Present, Absent } +import gunbc.compile_diagnostic_census { CompileDiagnosticCensus } +import gunbc.guarantee_probe_corpus { census_blocking_count_for_class } + +// ADMIT_CALLERS ON A SERVICE OPERATION IS ACCEPTED AND 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 -- every caller is admitted, and nothing warns. +// +// WHY THAT IS WORSE THAN THE WALL SIMPLY BEING ABSENT, which is the reason this file exists at +// all. An absent wall is visible: you go looking, 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: the session that found this was one +// step from reporting "the wall is available" after seeing the declaration parse, and the reviewing +// session would have believed it. +// +// BLAST RADIUS TODAY: ZERO. No operation in the corpus currently carries admit_callers -- checked +// across every .dag in dag/ and src/v2/, where all 21 occurrences attach to a fn or a sealed type. +// So this is a LATENT TRAP, not a live hole, and the distinction is deliberate: the first author +// to reach for it is the one who gets hurt, and they will have no reason to doubt it. +// +// TWO INDEPENDENT ROUTES ESTABLISH IT, because two readings of one artifact is not two +// observations. 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. By SOURCE: enforcement lives at +// exactly one site in the seed, gated on an exact-constructor-declaration lookup and 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. +// +// THE RUNG, stated honestly. Not mitigatable -- BELOW it, because no mitigation occurs: nothing +// refuses, nothing counts, nothing is logged. Attainable ceiling: structurally guaranteed, once +// the check reaches operation calls; the class is decidable and fully modeled, so nothing but +// implementation stands between here and there. NEXT-RUNG TRIGGER: an operation-grain construction +// refusal exists, verified by a correctly-imported unadmitted caller. That trigger is stated in +// its verified form because its first two attempted verifications were inconclusive for reasons +// that had nothing to do with the seal -- a missing import, then a fixture whose service did not +// resolve at all. A trigger that has already been mis-measured twice should carry how to measure it. +// +// ON THIS FILE'S SHAPE: the offending sources are compiled as DATA through the guarantee probe +// corpus rather than being written as modules, which is what lets the positive control and the +// finding live in one file and run through one invocation. Split apart they would be two +// observations; together they are a discrimination, and the discrimination is the finding. A +// refusal here is a resolve error, so an unadmitted call written directly into this module would +// take the whole file down with it. + +data admit_fn_form_source: String = "module probe_admit_fn_form\nimport extdeps.shell.exec { TransportScript, transport_script_seal }\nfn unadmitted_caller() -> TransportScript {\n transport_script_seal(body: \"x\")\n}\n" + +data admit_op_form_source: String = "module probe_admit_op_form\nimport std.types { String, Int }\nservice probe.Svc {\n operation Sealed {\n input { arg: String }\n output { exit_code: Int from \"exit_code\" }\n readonly\n admit_callers: [\n decl_ref(module_path: \"probe_admit_op_form\", decl_name: \"admitted_caller\"),\n ]\n transport shell { argv: [\"true\", arg] }\n exit { 0 => Unit nonzero => Unit }\n mock_response { 0 => { exit_code: 0 } \"hermetic\" }\n }\n}\nfn unadmitted_caller() -> Int {\n probe.Svc.Sealed(arg: \"x\").exit_code\n}\n" + +fn admit_census_of(source: String) -> CompileDiagnosticCensus { + compile_dag_diagnostic_census(source) +} + +// POSITIVE CONTROL, GREEN TODAY. The fn form refuses an unadmitted caller. This is what makes the +// expected-red below a finding rather than a broken harness: without it, a red could mean the +// mechanism is inert OR that this file cannot compile a probe at all, and those are different +// states with different remedies. +test fn fn_form_admission_refuses_unadmitted_caller() -> Bool { + match census_blocking_count_for_class( + census: admit_census_of(source: admit_fn_form_source), + wanted: "ConstructorCallAdmissionRefused" + ) { + Present { value: n } => n >= 1 + Absent => false + } +} + +// THE FINDING, EXPECTED-RED. Identical question at operation grain: a sealed operation whose +// admit_callers list does not name the caller. This asserts the refusal that OUGHT to occur, so it +// fails today and is enrolled as known-red rather than left to take the floor down as unexplained +// breakage. 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. +test fn operation_form_admission_refuses_unadmitted_caller() -> Bool { + match census_blocking_count_for_class( + census: admit_census_of(source: admit_op_form_source), + wanted: "ConstructorCallAdmissionRefused" + ) { + Present { value: n } => n >= 1 + Absent => false + } +} diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index f8af4bee6bc..7d811e9c8ac 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -317,7 +317,7 @@ fn floor_expected_red_chunk_03() -> List { } fn floor_expected_red_chunk_04() -> List { - Cons { head: "test.claim.materialized_secret.witness_destroyed_version_refuses_even_when_probe_says_live", tail: Cons { head: "test.claim.materialized_secret.witness_enabled_but_revoked_refuses", tail: Cons { head: "test.claim.materialized_secret.witness_enabled_but_unprobed_refuses", tail: Cons { head: "test.claim.materialized_secret.witness_live_secret_materializes_and_runs_the_use", tail: Cons { head: "test.claim.materialized_secret.witness_red_control_existence_only_rejected_by_gate", tail: Cons { head: "test.claim.materialized_secret.witness_self_repairing_probe_is_refused_by_classification", tail: Cons { head: "test.claim.materialized_ssh_key_file_real_execution_witness.witness_ssh_key_bracket_write_owner_only_shreds_and_not_under_target", tail: Cons { head: "test.claim.materialized_ssh_key_file_real_execution_witness.witness_write_owner_only_refuses_when_path_already_exists", tail: Cons { head: "test.claim.namespace_import_closure_witness.namespace_import_closure_receipt_holds", tail: Cons { head: "test.claim.namespace_reference_derived_closure_acceptance.witness_namespace_reference_derived_closure_closing_contract_holds", tail: Cons { head: "test.claim.non_fold_residue_witness.non_fold_residue_clean_holds", tail: Cons { head: "test.claim.observation_raw_print_retirement_acceptance_test.observation_emit_frontier_is_zero", tail: Cons { head: "test.claim.parse_test.parse_witness_floor_holds", tail: Cons { head: "test.claim.parse_test.parse_witness_perf_holds", tail: Cons { head: "test.claim.proc_self_cgroup_real_execution_witness.bash_assign_from_source_observed_shell_holds", tail: Cons { head: "test.claim.proc_self_cgroup_real_execution_witness.bash_assign_from_source_refuses_ambiguous_shell_holds", tail: Cons { head: "test.claim.proc_self_cgroup_real_execution_witness.bash_assign_from_source_refuses_malformed_shell_holds", tail: Cons { head: "test.claim.proc_self_cgroup_real_execution_witness.bash_assign_from_source_refuses_missing_shell_holds", tail: Cons { head: "test.claim.random_bytes_csprng_witness.random_bytes_base64url_mint_16_length_holds", tail: Cons { head: "test.claim.random_bytes_csprng_witness.random_bytes_base64url_mint_20_length_holds", tail: Cons { head: "test.claim.random_bytes_csprng_witness.random_bytes_count_holds", tail: Cons { head: "test.claim.random_bytes_csprng_witness.random_bytes_zero_holds", tail: Cons { head: "test.claim.realization_reconcile_witness.witness_different_keysource_does_not_collapse", tail: Cons { head: "test.claim.realization_reconcile_witness.witness_post_always_never_collapses", tail: Cons { head: "test.claim.realization_reconcile_witness.witness_same_keysource_collapses_to_share", tail: Cons { head: "test.claim.repo_local_git_config_real_execution.repo_local_git_config_actuator_sets_local_bindings_by_real_execution", tail: Empty {} } } } } } } } } } } } } } } } } } } } } } } } } } } + Cons { head: "test.claim.materialized_secret.witness_destroyed_version_refuses_even_when_probe_says_live", tail: Cons { head: "test.claim.materialized_secret.witness_enabled_but_revoked_refuses", tail: Cons { head: "test.claim.materialized_secret.witness_enabled_but_unprobed_refuses", tail: Cons { head: "test.claim.materialized_secret.witness_live_secret_materializes_and_runs_the_use", tail: Cons { head: "test.claim.materialized_secret.witness_red_control_existence_only_rejected_by_gate", tail: Cons { head: "test.claim.materialized_secret.witness_self_repairing_probe_is_refused_by_classification", tail: Cons { head: "test.claim.materialized_ssh_key_file_real_execution_witness.witness_ssh_key_bracket_write_owner_only_shreds_and_not_under_target", tail: Cons { head: "test.claim.materialized_ssh_key_file_real_execution_witness.witness_write_owner_only_refuses_when_path_already_exists", tail: Cons { head: "test.claim.namespace_import_closure_witness.namespace_import_closure_receipt_holds", tail: Cons { head: "test.claim.namespace_reference_derived_closure_acceptance.witness_namespace_reference_derived_closure_closing_contract_holds", tail: Cons { head: "test.claim.non_fold_residue_witness.non_fold_residue_clean_holds", tail: Cons { head: "test.claim.observation_raw_print_retirement_acceptance_test.observation_emit_frontier_is_zero", tail: Cons { head: "test.claim.operation_admit_callers_inert_witness.operation_form_admission_refuses_unadmitted_caller", tail: Cons { head: "test.claim.parse_test.parse_witness_floor_holds", tail: Cons { head: "test.claim.parse_test.parse_witness_perf_holds", tail: Cons { head: "test.claim.proc_self_cgroup_real_execution_witness.bash_assign_from_source_observed_shell_holds", tail: Cons { head: "test.claim.proc_self_cgroup_real_execution_witness.bash_assign_from_source_refuses_ambiguous_shell_holds", tail: Cons { head: "test.claim.proc_self_cgroup_real_execution_witness.bash_assign_from_source_refuses_malformed_shell_holds", tail: Cons { head: "test.claim.proc_self_cgroup_real_execution_witness.bash_assign_from_source_refuses_missing_shell_holds", tail: Cons { head: "test.claim.random_bytes_csprng_witness.random_bytes_base64url_mint_16_length_holds", tail: Cons { head: "test.claim.random_bytes_csprng_witness.random_bytes_base64url_mint_20_length_holds", tail: Cons { head: "test.claim.random_bytes_csprng_witness.random_bytes_count_holds", tail: Cons { head: "test.claim.random_bytes_csprng_witness.random_bytes_zero_holds", tail: Cons { head: "test.claim.realization_reconcile_witness.witness_different_keysource_does_not_collapse", tail: Cons { head: "test.claim.realization_reconcile_witness.witness_post_always_never_collapses", tail: Cons { head: "test.claim.realization_reconcile_witness.witness_same_keysource_collapses_to_share", tail: Cons { head: "test.claim.repo_local_git_config_real_execution.repo_local_git_config_actuator_sets_local_bindings_by_real_execution", tail: Empty {} } } } } } } } } } } } } } } } } } } } } } } } } } } } } fn floor_expected_red_chunk_05() -> List { From 2e194dba838395863243d0dd37a462b692051d55 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 23:34:38 +0000 Subject: [PATCH 09/16] Retarget the admission control onto the sealed fixture: 54.9s over a 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) --- .../operation_admit_callers_inert_witness_test.dag | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/dag/test/claim/operation_admit_callers_inert_witness_test.dag b/dag/test/claim/operation_admit_callers_inert_witness_test.dag index 94281161fbe..b90799569e7 100644 --- a/dag/test/claim/operation_admit_callers_inert_witness_test.dag +++ b/dag/test/claim/operation_admit_callers_inert_witness_test.dag @@ -49,7 +49,15 @@ import gunbc.guarantee_probe_corpus { census_blocking_count_for_class } // refusal here is a resolve error, so an unadmitted call written directly into this module would // take the whole file down with it. -data admit_fn_form_source: String = "module probe_admit_fn_form\nimport extdeps.shell.exec { TransportScript, transport_script_seal }\nfn unadmitted_caller() -> TransportScript {\n transport_script_seal(body: \"x\")\n}\n" +// THE CONTROL'S SUBJECT IS THE PURPOSE-BUILT FIXTURE, not a production sealed fn, and that is a +// COST decision with a measured cause rather than a preference. The first cut of this control +// forged a caller of extdeps.shell.exec.transport_script_seal; it established the same fact but +// took 54.9 SECONDS against the floor's 10s per-witness ceiling and grew RSS by about a gigabyte, +// because compiling that source drags the whole shell/extdeps closure through the census. The +// fixture's closure is a few declarations, and the operation-form probe beside it costs 516ms for +// the same reason -- it imports only std.types. Same mechanism, same refusal, two orders of +// magnitude less work. +data admit_fn_form_source: String = "module probe_admit_fn_form\nimport test.fixture.sole_constructor_sealed.definer { LocalValidated, mint_sealed_local }\nfn unadmitted_caller() -> LocalValidated {\n mint_sealed_local(n: 65)\n}\n" data admit_op_form_source: String = "module probe_admit_op_form\nimport std.types { String, Int }\nservice probe.Svc {\n operation Sealed {\n input { arg: String }\n output { exit_code: Int from \"exit_code\" }\n readonly\n admit_callers: [\n decl_ref(module_path: \"probe_admit_op_form\", decl_name: \"admitted_caller\"),\n ]\n transport shell { argv: [\"true\", arg] }\n exit { 0 => Unit nonzero => Unit }\n mock_response { 0 => { exit_code: 0 } \"hermetic\" }\n }\n}\nfn unadmitted_caller() -> Int {\n probe.Svc.Sealed(arg: \"x\").exit_code\n}\n" From 88d538fc89ca4cde575122abccbe74cc4624a924 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 23:34:38 +0000 Subject: [PATCH 10/16] Cut command_runner's local path onto shell.Exec.RunArgv: argv stops round-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; 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 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) --- dag/gunbc/command_runner.dag | 139 +++++++++++++++--- ...command_runner_local_argv_receipt_test.dag | 53 +++++++ src/v1/stage0/src/cli_run.rs | 6 + src/v2/std/compilers/cli_surface.dag | 28 ++++ 4 files changed, 207 insertions(+), 19 deletions(-) create mode 100644 dag/test/manual/command_runner_local_argv_receipt_test.dag diff --git a/dag/gunbc/command_runner.dag b/dag/gunbc/command_runner.dag index 009087138c0..ee4f144d64c 100644 --- a/dag/gunbc/command_runner.dag +++ b/dag/gunbc/command_runner.dag @@ -15,6 +15,10 @@ import extdeps.exec.command { import extdeps.shell import gunbc.shell_bash_runner { shell_exec_via_bash } import gunbc.retained_shell_script { retained_runtime } +import v2.std.algebra { list_head, list_tail, HeadFound, HeadAbsent, TailFound, TailAbsent } +import std.algebra { Empty } +import v2.std.compilers.cli_surface { cli_surface_of_literal_words, process_argv_expansion } +import extdeps.shell.exec { ExitZeroSucceeds, process_exit_is_admitted } import std.disposition { Disposition, Scaffold, RealizationDispatch } import std.decl_ref { DeclarationRef, WholeDeclaration } @@ -29,20 +33,72 @@ data command_runner_scaffold: Disposition = Scaffold { data command_runner_dissolution_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: run_shell_command — generic ArgvCommand runner routes the typed extdeps.exec.command shape through shell.Exec.Run via the shell_bash_runner heredoc transport; DISSOLVES WHEN host_effect_apply binds ArgvCommand execution as a typed transport handler and dag/gunbc/command_runner.dag retires its shell_exec_via_bash glue") +// THE LOCAL ARM NO LONGER ROUND-TRIPS ARGV THROUGH A STRING. +// +// What it used to do, and why none of it was necessary: render the argv to quoted text, wrap the +// text in a bash heredoc, hand that to a shell, and 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 in that chain existed only to undo the step before it. On LocalExec command_over_transport +// is the IDENTITY, so the render had nothing to transform either. +// +// The words now reach the process as words. Nothing is quoted, joined, split, or re-parsed, which +// is the whole point: an argv is a serialization, and a serialization that is immediately +// deserialized by a different grammar is where argument boundaries get lost. +// +// EMPTY ARGV REFUSES rather than defaulting. A command with no argv has no program, and there is +// no plausible process to run -- inventing one is exactly the fabricated output DESIGN forbids. +// +// THE SSH ARM IS UNTOUCHED, deliberately and not by oversight. Its prefix-append shape is wrong in +// kind -- RFC 4254 carries one string, so the inner command is a nested serialization target +// rather than a concatenation -- and that target is being built in another lane. Two sessions +// editing one contested branch is worse than either fix. Measured before leaving it: every one of +// the 22 live call sites of this module's entry points passes LocalExec, so this arm currently +// carries no traffic through here at all. func run_shell_command(command: ArgvCommand, transport: CommandTransport) -> ProcessExit uses net: Network { - let rendered = shell_command_render(command: command_over_transport(command: command, transport: transport)) - let run = shell.Exec.Run( - script: retained_runtime( - body: shell_exec_via_bash(body: rendered), - reason: "generic ArgvCommand runner heredoc transport, pending the typed host_effect_apply argv handler" as NonEmptyStr, - ) - ) - if run.success { - ExitSuccess - } else { - exit_failure(reason: concat("command failed: ", run.stderr)) + match transport { + LocalExec => + match list_head(xs: command.argv) { + HeadAbsent => + exit_failure(reason: "empty argv: a command with no words names no program to execute") + HeadFound { value: program } => { + let run = shell.Exec.RunArgv( + program: program as NonEmptyStr, + arguments: process_argv_expansion( + surface: cli_surface_of_literal_words(words: argv_operands(command: command)) + ), + ) + if process_exit_is_admitted(policy: ExitZeroSucceeds, exit_code: run.exit_code) { + ExitSuccess + } else { + exit_failure(reason: concat("command failed: ", run.stderr)) + } + } + } + SshExec { ssh_target: _ } => { + let rendered = shell_command_render(command: command_over_transport(command: command, transport: transport)) + let run = shell.Exec.Run( + script: retained_runtime( + body: shell_exec_via_bash(body: rendered), + reason: "SSH arm only: nested command-string target is owned by another lane; the local arm no longer routes here" as NonEmptyStr, + ) + ) + if run.success { + ExitSuccess + } else { + exit_failure(reason: concat("command failed: ", run.stderr)) + } + } + } +} + +// The operands are everything after the program. A missing tail is the one-word command, whose +// operand list is empty -- not an error, and not the same state as an empty argv. +fn argv_operands(command: ArgvCommand) -> List { + match list_tail(xs: command.argv) { + TailAbsent => Empty + TailFound { tail: rest } => rest } } @@ -56,17 +112,62 @@ type ShellCaptureResult { stderr: String } +// THE success FIELD IS DERIVED THROUGH A NAMED POLICY, not a bare exit_code == 0, and the +// difference is not cosmetic. RunArgv deliberately carries no success field because success is a +// POLICY judgement about an observation rather than part of it -- jq exits 4 to mean "no output" +// and 1 to mean "false result", neither of which is failure. Routing through +// process_exit_is_admitted(ExitZeroSucceeds) states which convention this runner applies, so a +// caller needing a different one has something to change rather than a literal to discover. +// +// WHAT THIS SHAPE STILL COLLAPSES, named rather than fixed here. "the program ran and exited +// nonzero" and "the program 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 the process ran and exited when it never existed. Going direct removes the +// shell that fabricated that code, so the distinction is now AVAILABLE at the transport even +// though this record cannot express it. +// +// It is not fixed in this change because it is not free: 17 of the 22 live call sites read +// ShellCaptureResult, and the correct destination is the ProcessOutcome coproduct that already +// exists one module away -- ProcessOutputPresent / ProcessOutputAbsent / ProcessRefused -- so the +// repair is a caller migration and belongs with the sites it changes. Recorded here so the +// collapse is a known state with a destination rather than an unremarked property of the record. func run_shell_command_capture(command: ArgvCommand, transport: CommandTransport) -> ShellCaptureResult uses net: Network { - let rendered = shell_command_render(command: command_over_transport(command: command, transport: transport)) - let run = shell.Exec.Run( - script: retained_runtime( - body: shell_exec_via_bash(body: rendered), - reason: "generic ArgvCommand capture runner heredoc transport, pending the typed host_effect_apply argv handler" as NonEmptyStr, - ) - ) - ShellCaptureResult { success: run.success, stdout: run.stdout, stderr: run.stderr } + match transport { + LocalExec => + match list_head(xs: command.argv) { + HeadAbsent => + ShellCaptureResult { + success: false, + stdout: "", + stderr: "empty argv: a command with no words names no program to execute", + } + HeadFound { value: program } => { + let run = shell.Exec.RunArgv( + program: program as NonEmptyStr, + arguments: process_argv_expansion( + surface: cli_surface_of_literal_words(words: argv_operands(command: command)) + ), + ) + ShellCaptureResult { + success: process_exit_is_admitted(policy: ExitZeroSucceeds, exit_code: run.exit_code), + stdout: run.stdout, + stderr: run.stderr, + } + } + } + SshExec { ssh_target: _ } => { + let rendered = shell_command_render(command: command_over_transport(command: command, transport: transport)) + let run = shell.Exec.Run( + script: retained_runtime( + body: shell_exec_via_bash(body: rendered), + reason: "SSH arm only: nested command-string target is owned by another lane; the local arm no longer routes here" as NonEmptyStr, + ) + ) + ShellCaptureResult { success: run.success, stdout: run.stdout, stderr: run.stderr } + } + } } // Receipt owner probe — admitted under command_runner_scaffold until diff --git a/dag/test/manual/command_runner_local_argv_receipt_test.dag b/dag/test/manual/command_runner_local_argv_receipt_test.dag new file mode 100644 index 00000000000..2dd563be894 --- /dev/null +++ b/dag/test/manual/command_runner_local_argv_receipt_test.dag @@ -0,0 +1,53 @@ +module test.manual.command_runner_local_argv_receipt + +import std.types { Bool, String } +import extdeps.exec.command { ArgvCommand, LocalExec } +import gunbc.command_runner { run_shell_command_capture } + +// THE DISCRIMINATING RECEIPT FOR THE LOCAL ARGV CUT. +// +// WHAT IT DISCRIMINATES, which is the only thing that makes it worth running. The local path used +// to render argv to text and hand it to bash, which split it back apart on whitespace. It now goes +// word-for-word to the process. A test that merely runs a command green proves nothing about that +// change -- it would be equally green with the bash hop restored. So the subject is an argument +// that the two paths DISAGREE about: one containing a space. +// +// argv: ["printf", "%s|", "a b"] +// direct exec: one operand "a b" -> stdout "a b|" +// via a shell: two operands "a" and "b" -> stdout "a|b|" +// +// If this ever reads "a|b|", the local path has reached a shell again and the cut has silently +// regressed. That is the failure this file exists to make loud. +// +// WHY IT IS WET AND NOT ENROLLED. Hermetic evaluation replays an operation's declared +// mock_response off the declaration and never constructs an argv at all, so the property under +// test -- how the words reach the process -- is not observable hermetically by construction. A +// hermetic version of this file could only assert the mock, which is the specification-without- +// execution trap. It therefore runs wet, by hand, and is excluded from the floor exactly as +// test/manual/process_argv_expansion_receipt_test.dag is, for the same reason. + +test fn spaced_operand_survives_as_one_argument() -> Bool { + run_shell_command_capture( + command: ArgvCommand { argv: ["printf", "%s|", "a b"] }, + transport: LocalExec, + ).stdout == "a b|" +} + +// The RED half of the same observation, stated as its own assertion rather than left implicit in +// the equality above: the shell-split rendering must NOT be what comes back. Written separately so +// a future edit that weakens the positive into something like a nonempty check still trips here. +test fn shell_split_rendering_is_not_what_comes_back() -> Bool { + run_shell_command_capture( + command: ArgvCommand { argv: ["printf", "%s|", "a b"] }, + transport: LocalExec, + ).stdout != "a|b|" +} + +// Control that the runner works at all on the ordinary case, so a failure above is read as a +// splitting regression rather than as the whole path being broken. +test fn plain_operand_round_trips() -> Bool { + run_shell_command_capture( + command: ArgvCommand { argv: ["printf", "%s|", "plain"] }, + transport: LocalExec, + ).stdout == "plain|" +} diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 6b1e476c032..0f33ea0da78 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -38648,6 +38648,12 @@ pub fn floor_prepared_subject_exclusions() -> Vec { // re-enrolls when a wet lane exists again — which required_floor.dag deliberately defers // until it can be "asked against a live consumer". "test/manual/process_argv_expansion_receipt_test.dag".to_string(), + // Wet receipt for the command_runner local-argv cut. Excluded for the same reason as the + // line above and not a new class: hermetic evaluation replays an operation's declared + // mock_response and never constructs an argv, so "the words reached the process unsplit" + // is not observable hermetically. Enrolling it would assert the mock rather than the + // behaviour -- specification without execution. + "test/manual/command_runner_local_argv_receipt_test.dag".to_string(), ] } diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index f06fa062dd7..66d22fe0822 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -104,6 +104,34 @@ type CliArgument sole_constructor { text: String } type CliSurface sole_constructor { arguments: List } +// LITERAL WORDS INTO A SURFACE, and this is the ONE route for arguments whose spelling is a +// runtime value rather than a declared token. +// +// WHY IT IS NOT THE AMBIGUITY THIS CARRIER EXISTS TO CLOSE. The refused state is a List +// 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 readings of the same value and the +// realization has to guess. This constructor IS the declaration: its name says each element is +// exactly one argv word, so the caller has chosen the reading rather than leaving it to be +// inferred. It is the same resolution the interpreter's refusal diagnostic tells authors to +// reach for. +// +// WHAT IT DOES NOT LICENSE. It is not a general escape from structural modeling. An argument +// whose spelling is known when the program is written belongs in CliArgumentSyntax fragments, +// which carry token classes and bindings and can be checked; this route carries none of that and +// can check none of it. It exists because argv words like a filesystem path or a hostname are +// genuinely runtime strings, and no fragment vocabulary can express a value that does not exist +// until the program runs. Reaching for it when fragments would have served is modeling debt, not +// a shortcut. +fn cli_surface_of_literal_words(words: List) -> CliSurface { + CliSurface { + arguments: fold_list( + xs: words, + empty: Empty, + cons: fn(acc, word) { list_snoc_item(xs: acc, item: CliArgument { text: word }) } + ) + } +} + fn cli_surface_arguments(surface: CliSurface) -> List { surface.arguments } From 1526e00874db4827ac106f90a1584ffe2b5d517e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 19 Aug 2026 23:58:22 +0000 Subject: [PATCH 11/16] Restrict the literal-words mint to its two callers; state what CI does not guard; correct the trigger MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- dag/gunbc/command_runner.dag | 21 ++++++++++++++++++++- src/v2/std/compilers/cli_surface.dag | 23 ++++++++++++++++++++--- 2 files changed, 40 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/command_runner.dag b/dag/gunbc/command_runner.dag index ee4f144d64c..1eea6b541d4 100644 --- a/dag/gunbc/command_runner.dag +++ b/dag/gunbc/command_runner.dag @@ -31,7 +31,26 @@ data command_runner_scaffold: Disposition = Scaffold { } } -data command_runner_dissolution_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: run_shell_command — generic ArgvCommand runner routes the typed extdeps.exec.command shape through shell.Exec.Run via the shell_bash_runner heredoc transport; DISSOLVES WHEN host_effect_apply binds ArgvCommand execution as a typed transport handler and dag/gunbc/command_runner.dag retires its shell_exec_via_bash glue") +data command_runner_dissolution_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: the SSH arm of run_shell_command / run_shell_command_capture. THE LOCAL ARM IS DONE -- it routes straight at shell.Exec.RunArgv, constructs no TransportScript, and reaches no shell. WORDING CORRECTED, and the correction is the point: this row previously named host_effect_apply binding ArgvCommand as a typed transport handler. No such production module exists -- host_effect_apply appears only as a witness test, and host_effect_realize never mentions ArgvCommand -- so the trigger named a binding that was never built, and satisfying it literally would have meant building a second route to answer a question command_runner already answers. Measured before rewriting: 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, which is a different destination rather than a second local-exec path. DISSOLVES WHEN the SSH arm stops rendering argv to a string -- which needs the nested command-string target RFC 4254 actually requires, owned by another lane -- at which point shell_exec_via_bash and retained_runtime leave this module entirely.") + +// WHAT GUARDS THIS, AND WHAT DOES NOT -- read before assuming the property below is enforced. +// +// The property "the local path reaches no shell" is established by execution, wet, against a real +// process: test/manual/command_runner_local_argv_receipt_test.dag runs printf against an operand +// containing a space and asserts the one-argument reading arrives while the shell-split reading +// does not. It passes. It is also EXCLUDED FROM THE FLOOR, so CI does not run it, and after this +// lands someone reintroducing a render-and-bash hop on this arm gets NO SIGNAL from CI. +// +// The exclusion is structural rather than convenient: hermetic evaluation replays an operation's +// declared mock_response and never constructs an argv, so how the words reach the process is not +// observable hermetically at all. A hermetic version of that receipt could only assert the mock, +// which is specification-without-execution -- it would look like coverage while proving nothing. +// +// RUNG: mitigatable. The invalid state (argv re-split by a shell) is writable, and the mechanism +// that detects it does not execute in CI. NEXT-RUNG TRIGGER: a wet lane that executes +// floor-excluded receipts, at which point this row's evidence enrolls and the class climbs to +// mechanically preventable. Stated here rather than left to be inferred from a passing receipt, +// because a green test that nothing runs is exactly the inert evidence DESIGN calls a lie. // THE LOCAL ARM NO LONGER ROUND-TRIPS ARGV THROUGH A STRING. // diff --git a/src/v2/std/compilers/cli_surface.dag b/src/v2/std/compilers/cli_surface.dag index 66d22fe0822..3408151d6c3 100644 --- a/src/v2/std/compilers/cli_surface.dag +++ b/src/v2/std/compilers/cli_surface.dag @@ -122,15 +122,32 @@ type CliSurface sole_constructor { arguments: List } // genuinely runtime strings, and no fragment vocabulary can express a value that does not exist // until the program runs. Reaching for it when fragments would have served is modeling debt, not // a shortcut. -fn cli_surface_of_literal_words(words: List) -> CliSurface { - CliSurface { +// RESTRICTED, because an unbounded declaration is a nominal wall rather than a structural one. +// sole_constructor stops other modules writing CliSurface directly, so adding a mint here breaks +// no seal -- but it widens THIS module's mint surface, and an unrestricted mint would let any +// module turn an arbitrary List into a surface. The interpreter's argv refusal would then +// be one import away from being routed around: not defeated, but satisfied by declaring an intent +// nobody checked was true. +// +// The admitted population is the two runner entry points that genuinely hold runtime words -- a +// filesystem path, a hostname -- and it is enumerable at TWO today, which is what makes the +// restriction honest rather than aspirational. Adding a third is an edit to this list in the +// declaring module: a conspicuous, counted review event rather than an import written elsewhere. +// This mechanism is verified to enforce at fn grain (a refused call names the caller and lists the +// roster); it is NOT verified at operation grain, which is a separate filed defect and does not +// affect this row. +fn cli_surface_of_literal_words(words: List) -> CliSurface + admit_callers: [ + decl_ref(module_path: "gunbc.command_runner", decl_name: "run_shell_command"), + decl_ref(module_path: "gunbc.command_runner", decl_name: "run_shell_command_capture"), + ] + = CliSurface { arguments: fold_list( xs: words, empty: Empty, cons: fn(acc, word) { list_snoc_item(xs: acc, item: CliArgument { text: word }) } ) } -} fn cli_surface_arguments(surface: CliSurface) -> List { surface.arguments From 71cfb853ab1389aaabb4efd4ee53eb07a967b652 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 20 Aug 2026 00:06:02 +0000 Subject: [PATCH 12/16] Correct a false premise in the trigger I just rewrote: host_effect_apply 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) --- dag/gunbc/command_runner.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/gunbc/command_runner.dag b/dag/gunbc/command_runner.dag index 1eea6b541d4..fb94e5f6943 100644 --- a/dag/gunbc/command_runner.dag +++ b/dag/gunbc/command_runner.dag @@ -31,7 +31,7 @@ data command_runner_scaffold: Disposition = Scaffold { } } -data command_runner_dissolution_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: the SSH arm of run_shell_command / run_shell_command_capture. THE LOCAL ARM IS DONE -- it routes straight at shell.Exec.RunArgv, constructs no TransportScript, and reaches no shell. WORDING CORRECTED, and the correction is the point: this row previously named host_effect_apply binding ArgvCommand as a typed transport handler. No such production module exists -- host_effect_apply appears only as a witness test, and host_effect_realize never mentions ArgvCommand -- so the trigger named a binding that was never built, and satisfying it literally would have meant building a second route to answer a question command_runner already answers. Measured before rewriting: 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, which is a different destination rather than a second local-exec path. DISSOLVES WHEN the SSH arm stops rendering argv to a string -- which needs the nested command-string target RFC 4254 actually requires, owned by another lane -- at which point shell_exec_via_bash and retained_runtime leave this module entirely.") +data command_runner_dissolution_trigger: DissolutionCondition = unbound_dissolution(description: "🟡 dissolve-on: the SSH arm of run_shell_command / run_shell_command_capture. THE LOCAL ARM IS DONE -- it routes straight at shell.Exec.RunArgv, constructs no TransportScript, and reaches no shell. WORDING CORRECTED, and the correction is the point: this row previously named host_effect_apply binding ArgvCommand as a typed transport handler. host_effect_apply DOES exist -- gunbc.host_effect_realize declares host_effect_apply and host_effect_apply_gated, and they are production, not test scaffolding. What it does not do is reach an ArgvCommand: that module contains ZERO occurrences of the type and does not appear among its consumers at all. So the binding this trigger named was never built in the sense that matters -- host_effect_apply dispatches effects but is not, and has never been, a route from an ArgvCommand to a process. An earlier revision of this row said host_effect_apply did not exist, which is false and checkable in one grep; the correction is recorded rather than quietly overwritten because a replacement trigger carrying a false premise makes the next author re-derive the whole question, which is exactly the cost the original trigger imposed. Measured before rewriting: 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, which is a different destination rather than a second local-exec path. DISSOLVES WHEN the SSH arm stops rendering argv to a string -- which needs the nested command-string target RFC 4254 actually requires, owned by another lane -- at which point shell_exec_via_bash and retained_runtime leave this module entirely.") // WHAT GUARDS THIS, AND WHAT DOES NOT -- read before assuming the property below is enforced. // From 090dfdc1aa9c2296fc5944ad5cba55dfe4bd6732 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 20 Aug 2026 01:25:02 +0000 Subject: [PATCH 13/16] Replace ShellCaptureResult with ProcessOutcome across every capture site 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) --- dag/gunbc/command_runner.dag | 113 ++++++++++++------ dag/gunbc/fleet_converge_cli.dag | 30 +++-- dag/gunbc/fleet_converge_plan_cli.dag | 44 +++++-- dag/gunbc/fleet_host_key_enrollment.dag | 112 +++++++++++------ dag/gunbc/fleet_probe_identity_observe.dag | 41 ++++--- dag/gunbc/fleet_ssh_credential_verify.dag | 68 +++++++---- ...command_runner_local_argv_receipt_test.dag | 82 +++++++++++-- 7 files changed, 349 insertions(+), 141 deletions(-) diff --git a/dag/gunbc/command_runner.dag b/dag/gunbc/command_runner.dag index fb94e5f6943..a5f70e7b701 100644 --- a/dag/gunbc/command_runner.dag +++ b/dag/gunbc/command_runner.dag @@ -2,7 +2,7 @@ module gunbc.command_runner import std.dissolution { DissolutionCondition, dissolution_description, unbound_dissolution } -import std.types { List, String, NonEmptyStr } +import std.types { List, String, NonEmptyStr, Bool } import std.process { ProcessExit, ExitSuccess, exit_failure } import std.resources { Network } import extdeps.exec.command { @@ -18,7 +18,11 @@ import gunbc.retained_shell_script { retained_runtime } import v2.std.algebra { list_head, list_tail, HeadFound, HeadAbsent, TailFound, TailAbsent } import std.algebra { Empty } import v2.std.compilers.cli_surface { cli_surface_of_literal_words, process_argv_expansion } -import extdeps.shell.exec { ExitZeroSucceeds, process_exit_is_admitted } +import extdeps.shell.exec { + ExitZeroSucceeds, process_exit_is_admitted, + ProcessOutcome, ProcessOutputPresent, ProcessOutputAbsent, ProcessRefused, + process_observation, classify_process_observation, +} import std.disposition { Disposition, Scaffold, RealizationDispatch } import std.decl_ref { DeclarationRef, WholeDeclaration } @@ -125,41 +129,45 @@ fn argv_operands(command: ArgvCommand) -> List { // but the caller receives the process observation instead of a collapsed ProcessExit — // for wet observations whose PRODUCT is the stdout (ssh-keyscan, ssh-keygen -lf). // Success/stdout/stderr travel together so a refusal cannot be read as empty output. -type ShellCaptureResult { - success: Bool - stdout: String - stderr: String -} -// THE success FIELD IS DERIVED THROUGH A NAMED POLICY, not a bare exit_code == 0, and the -// difference is not cosmetic. RunArgv deliberately carries no success field because success is a -// POLICY judgement about an observation rather than part of it -- jq exits 4 to mean "no output" -// and 1 to mean "false result", neither of which is failure. Routing through -// process_exit_is_admitted(ExitZeroSucceeds) states which convention this runner applies, so a -// caller needing a different one has something to change rather than a literal to discover. +// SPAWN FAILURE IS ALREADY FAIL-CLOSED, and this is the transport fact that decides what the +// capture surface can and cannot say. Measured wet against the real local path: a command whose +// program does not exist does NOT come back as a failed result. It REFUSES the evaluation with a +// typed diagnostic naming the program and the OS error -- +// failed to execute 'no_such_binary': No such file or directory (os error 2) +// -- so no result record is produced at all. +// +// TWO CONSEQUENCES, and the second is the useful one. +// +// There is no unspawnable-versus-ran distinction for this surface to model. A fourth "not spawned" +// variant would be an uninhabited arm that every consumer must handle and none can ever reach, so +// it is deliberately absent. // -// WHAT THIS SHAPE STILL COLLAPSES, named rather than fixed here. "the program ran and exited -// nonzero" and "the program 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 the process ran and exited when it never existed. Going direct removes the -// shell that fabricated that code, so the distinction is now AVAILABLE at the transport even -// though this record cannot express it. +// AND A CALLER CANNOT PROBE FOR A BINARY'S EXISTENCE BY TRYING TO RUN IT. The attempt does not +// return an answer; it stops the line. Presence must be asked of something that exists -- spawn a +// shell and let `command -v` report -- rather than spawning the candidate and interpreting the +// wreckage. That is why a separate presence probe has to exist, and it is a boundary fact about +// the transport rather than a limitation of this module. // -// It is not fixed in this change because it is not free: 17 of the 22 live call sites read -// ShellCaptureResult, and the correct destination is the ProcessOutcome coproduct that already -// exists one module away -- ProcessOutputPresent / ProcessOutputAbsent / ProcessRefused -- so the -// repair is a caller migration and belongs with the sites it changes. Recorded here so the -// collapse is a known state with a destination rather than an unremarked property of the record. -func run_shell_command_capture(command: ArgvCommand, transport: CommandTransport) -> ShellCaptureResult +// WHAT THE CAPTURE SURFACE RETURNS, and why it is a coproduct rather than a record. +// ShellCaptureResult carried success: Bool beside stdout: String, which made two states that a +// caller cannot tell apart: a program that RAN AND FAILED printing nothing, and one that RAN AND +// SUCCEEDED printing nothing. Both are stdout == "". Correlating them was the caller's duty, and +// measured across the live sites, EIGHT of them did not perform it -- they read stdout and acted +// on the empty string as though it were an answer. That is the empty-observation narrow: not a +// widen, its mirror, and it was live in production at eight sites. +// +// The coproduct makes the failure unignorable: output is reachable ONLY through the variant that +// carries it, so a caller cannot read text without having confronted the arm where there is none. +func run_shell_command_capture(command: ArgvCommand, transport: CommandTransport) -> ProcessOutcome uses net: Network { match transport { LocalExec => match list_head(xs: command.argv) { HeadAbsent => - ShellCaptureResult { - success: false, - stdout: "", + ProcessRefused { + exit_code: 0 - 1, stderr: "empty argv: a command with no words names no program to execute", } HeadFound { value: program } => { @@ -169,11 +177,14 @@ func run_shell_command_capture(command: ArgvCommand, transport: CommandTransport surface: cli_surface_of_literal_words(words: argv_operands(command: command)) ), ) - ShellCaptureResult { - success: process_exit_is_admitted(policy: ExitZeroSucceeds, exit_code: run.exit_code), - stdout: run.stdout, - stderr: run.stderr, - } + classify_process_observation( + policy: ExitZeroSucceeds, + observation: process_observation( + exit_code: run.exit_code, + stdout: run.stdout, + stderr: run.stderr, + ), + ) } } SshExec { ssh_target: _ } => { @@ -184,14 +195,46 @@ func run_shell_command_capture(command: ArgvCommand, transport: CommandTransport reason: "SSH arm only: nested command-string target is owned by another lane; the local arm no longer routes here" as NonEmptyStr, ) ) - ShellCaptureResult { success: run.success, stdout: run.stdout, stderr: run.stderr } + classify_process_observation( + policy: ExitZeroSucceeds, + observation: process_observation( + exit_code: run.exit_code, + stdout: run.stdout, + stderr: run.stderr, + ), + ) } } } +// Did the process do its job? Callers whose product is the EXIT STATUS rather than the output ask +// this instead of matching all three arms -- `test -f` has no stdout anyone wants, and forcing it +// through an output-bearing variant would add a field it cannot answer. This is not a flattening +// helper for output-consuming callers: it deliberately cannot reach the text. +fn process_outcome_admitted(outcome: ProcessOutcome) -> Bool { + match outcome { + ProcessOutputPresent { text: _ } => true + ProcessOutputAbsent => true + ProcessRefused { exit_code: _, stderr: _ } => false + } +} + +// A receipt line's text, and it is NOT a flattening back to the conflated shape. The three arms +// render to three DISTINGUISHABLE strings: a refusal can never be mistaken for empty output, which +// is the exact property the old record lacked. Use it only where the value is being written into +// human-readable text; a caller that uses the value AS DATA -- a path, a hostname -- must match the +// arms itself, because "(refused: ...)" is a fine thing to print and a catastrophic thing to open. +fn process_outcome_receipt_text(outcome: ProcessOutcome) -> String { + match outcome { + ProcessOutputPresent { text: t } => trim(s: t) + ProcessOutputAbsent => "(no output)" + ProcessRefused { exit_code: _, stderr: e } => join(["(refused: ", trim(s: e), ")"], "") + } +} + // Receipt owner probe — admitted under command_runner_scaffold until // extdeps.filesystem.filesystem_io carries typed owner observation. -fn stat_owner_name_capture(path: String) -> ShellCaptureResult { +fn stat_owner_name_capture(path: String) -> ProcessOutcome { run_shell_command_capture( command: ArgvCommand { argv: ["stat", "-c", "%U", path] }, transport: LocalExec, diff --git a/dag/gunbc/fleet_converge_cli.dag b/dag/gunbc/fleet_converge_cli.dag index f2a7667dde5..a627234788d 100644 --- a/dag/gunbc/fleet_converge_cli.dag +++ b/dag/gunbc/fleet_converge_cli.dag @@ -4,6 +4,7 @@ import extdeps.filesystem.filesystem_io { Filesystem } import extdeps.shell import std.algebra { trim } import gunbc.command_runner { stat_owner_name_capture } +import extdeps.shell.exec { ProcessOutputPresent, ProcessOutputAbsent, ProcessRefused } import gunbc.fleet_posix_accounts { fleet_posix_operator_user } import gunbc.hostname_read { @@ -583,19 +584,22 @@ fn converge_cli_expected_receipt_owner_name() -> String { fn converge_cli_receipt_owner_readback(host: String) -> String? { let path = fleet_converge_receipt_path(host: host) let expected = converge_cli_expected_receipt_owner_name() - let r = stat_owner_name_capture(path: path) - if !r.success { - Present { value: concat("gunbc converge: receipt owner read-back refused (stat): ", trim(s: r.stderr)) } - } else { - let owner = trim(s: r.stdout) - if owner == expected { - none - } else { - Present { - value: concat( - concat("gunbc converge: receipt owner read-back mismatch — expected ", expected), - concat(" observed ", owner), - ), + match stat_owner_name_capture(path: path) { + ProcessRefused { exit_code: _, stderr: e } => + Present { value: concat("gunbc converge: receipt owner read-back refused (stat): ", trim(s: e)) } + ProcessOutputAbsent => + Present { value: "gunbc converge: receipt owner read-back refused (stat): admitted exit but no owner name on stdout" } + ProcessOutputPresent { text: t } => { + let owner = trim(s: t) + if owner == expected { + none + } else { + Present { + value: concat( + concat("gunbc converge: receipt owner read-back mismatch — expected ", expected), + concat(" observed ", owner), + ), + } } } } diff --git a/dag/gunbc/fleet_converge_plan_cli.dag b/dag/gunbc/fleet_converge_plan_cli.dag index fa006da1452..2d07c17b070 100644 --- a/dag/gunbc/fleet_converge_plan_cli.dag +++ b/dag/gunbc/fleet_converge_plan_cli.dag @@ -42,12 +42,30 @@ data fleet_converge_plan_cli_note: String = "Wet CLI for on-demand fleet converg func observe_host_short_wet() -> String uses net: Network { - trim( - s: run_shell_command_capture( - command: ArgvCommand { argv: ["hostname", "-s"] }, - transport: LocalExec, - ).stdout, - ) + // STATED, NOT SILENTLY DEFAULTED. This value KEYS THE CONVERGE PLAN's subject identity, so a + // hostname that could not be read must not become "" and flow into a plan named for the wrong + // host. The old code took .stdout straight off the call expression -- no binding, so there was + // not even a variable a later author could think to check. + // + // WHAT THIS DOES AND DOES NOT FIX, stated because the residue is real. A `-> String` function + // has no way to refuse: the substrate offers no abort from this position, so the only honest + // options are to change the return type or to return a value. This returns a value that CANNOT + // BE MISTAKEN FOR A HOSTNAME -- deliberately implausible rather than plausibly empty -- so a + // plan keyed on it is visibly wrong at a glance instead of silently wrong forever. That is + // strictly better than "" and is still not a refusal. + // + // RUNG: mitigatable, not fixed. The conflation is surfaced, not closed. NEXT-RUNG TRIGGER: this + // function returns an optional (or a typed outcome) and its two callers handle the absent case; + // that cascades into plan subject identity, which is a different change from this migration and + // deliberately not attempted inside it. + match run_shell_command_capture( + command: ArgvCommand { argv: ["hostname", "-s"] }, + transport: LocalExec, + ) { + ProcessOutputPresent { text: t } => trim(s: t) + ProcessOutputAbsent => "(hostname-unreadable: admitted but printed nothing)" + ProcessRefused { exit_code: _, stderr: _ } => "(hostname-unreadable: probe refused)" + } } func observe_generation_store_wet() -> Int? @@ -62,10 +80,16 @@ func observe_timer_members_wet() -> List { let legacy = timer_retirement_observed_legacy_srv1() filter(legacy, m => - run_shell_command_capture( - command: ArgvCommand { argv: ["test", "-f", concat("/etc/systemd/system/", m.unit_name as String)] }, - transport: LocalExec, - ).success + // EXIT STATUS IS THE PRODUCT HERE and there is no stdout anyone wants, so this asks the + // two-state question directly instead of matching three arms, two of which would be + // indistinguishable to it. Forcing `test -f` through an output-bearing variant would add a + // field it cannot answer -- cosmetic richness in the opposite direction. + process_outcome_admitted( + outcome: run_shell_command_capture( + command: ArgvCommand { argv: ["test", "-f", concat("/etc/systemd/system/", m.unit_name as String)] }, + transport: LocalExec, + ) + ) ) } diff --git a/dag/gunbc/fleet_host_key_enrollment.dag b/dag/gunbc/fleet_host_key_enrollment.dag index f64c03e62e1..ad757468214 100644 --- a/dag/gunbc/fleet_host_key_enrollment.dag +++ b/dag/gunbc/fleet_host_key_enrollment.dag @@ -9,7 +9,8 @@ import std.decl_ref { DeclarationRef, WholeDeclaration } import extdeps.filesystem.filesystem_io { Filesystem } import extdeps.exec.command { ArgvCommand, LocalExec } import extdeps.ssh { ssh_public_key_line } -import gunbc.command_runner { run_shell_commands, run_shell_command_capture, ShellCaptureResult } +import gunbc.command_runner { run_shell_commands, run_shell_command_capture, process_outcome_admitted, process_outcome_receipt_text } +import extdeps.shell.exec { ProcessOutcome, ProcessOutputPresent, ProcessOutputAbsent, ProcessRefused } import product.placement_supply { HostIdentity } import gunbc.fleet_reach_endpoint { fleet_probe_endpoint_for, fleet_reach_probe_targets } import gunbc.fleet_ssh_access { fleet_automation_ssh_key, fleet_automation_privkey_version_segment, fleet_automation_ssh_privkey_secret } @@ -169,32 +170,65 @@ data fleet_host_key_scan_receipt_path: String = "target/fleet-host-key-scan-rece // bold-eagle measurements and OpenSSH defaults lead with), then fingerprint the scanned // line. Both captures ride the receipt VERBATIM with a per-host outcome label; a // refusing scan is a typed absent line, never an empty fabrication. +// Post-apply verification. Hoisted out of the apply arms so both admitted arms share one route, +// and matched rather than read: the old code did concat("outcome=", trim(verify.stdout)), so a +// verify that REFUSED emitted the literal receipt line "outcome=" -- a fabricated plausible output +// standing where the answer was unknown, written into a receipt someone would later read as fact. +func verify_enrollment_outcome() -> String + uses net: Network +{ + match run_shell_command_capture( + command: ArgvCommand { argv: ["sh", "-c", "H=$(getent passwd \"$(whoami)\" | cut -d: -f6); grep -qxF \"$(cat target/fleet-authorized-key-line | head -1)\" \"$H/.ssh/authorized_keys\" && echo enrolled || echo ABSENT-after-apply"] }, + transport: LocalExec, + ) { + ProcessOutputPresent { text: t } => concat("outcome=", trim(s: t)) + ProcessOutputAbsent => "outcome=UNKNOWN cause=verify admitted but printed nothing" + ProcessRefused { exit_code: _, stderr: e } => join(["outcome=UNKNOWN cause=verify refused: ", trim(s: e)], "") + } +} + fn scan_host_key_lines(host: String) -> String { let endpoint = fleet_probe_endpoint_for(host: host) - let scan = run_shell_command_capture( + // ProcessOutputPresent already means admitted-and-non-empty, so the old + // `scan.success && trim(scan.stdout) != ""` correlation is the variant itself rather than a + // condition the caller must remember to write. ProcessOutputAbsent is now a NAMED outcome -- + // ssh-keyscan exiting 0 with no key is a different fact from ssh-keyscan failing, and the old + // shape reported both as "refused" with an empty cause. + match run_shell_command_capture( command: ArgvCommand { argv: ["ssh-keyscan", "-T", "5", "-t", "ed25519", endpoint] }, transport: LocalExec, - ) - if scan.success && trim(s: scan.stdout) != "" { - let key_file = join(["target/fleet-host-key-scan-", host, ".pub"], "") - let w = Filesystem.Write(path: key_file, content: scan.stdout) - let fp = if w.success { - run_shell_command_capture( - command: ArgvCommand { argv: ["ssh-keygen", "-l", "-f", key_file] }, - transport: LocalExec, - ) - } else { - ShellCaptureResult { success: false, stdout: "", stderr: w.error } + ) { + ProcessOutputPresent { text: key_text } => { + let key_file = join(["target/fleet-host-key-scan-", host, ".pub"], "") + let w = Filesystem.Write(path: key_file, content: key_text) + // The old code fabricated a ShellCaptureResult here to stand in for a FILESYSTEM failure -- + // a process result for something that was never a process, with an invented success: false. + // The coproduct makes that unwritable, which is the point: a write failure is not a process + // outcome and now has to be said in its own words. + let fingerprint_text = if w.success { + process_outcome_receipt_text( + outcome: run_shell_command_capture( + command: ArgvCommand { argv: ["ssh-keygen", "-l", "-f", key_file] }, + transport: LocalExec, + ) + ) + } else { + join(["(not computed: staging write refused: ", w.error, ")"], "") + } + join([ + "scan host=", host, " endpoint=", endpoint, " outcome=observed\n", + "key ", trim(s: key_text), "\n", + "fingerprint ", fingerprint_text, "\n", + ], "") } - join([ - "scan host=", host, " endpoint=", endpoint, " outcome=observed\n", - "key ", trim(s: scan.stdout), "\n", - "fingerprint ", trim(s: fp.stdout), "\n", - ], "") - } else { - join([ - "scan host=", host, " endpoint=", endpoint, " outcome=refused cause=", trim(s: scan.stderr), "\n", - ], "") + ProcessOutputAbsent => + join([ + "scan host=", host, " endpoint=", endpoint, " outcome=no-key-offered cause=scan admitted but returned no key\n", + ], "") + ProcessRefused { exit_code: _, stderr: e } => + join([ + "scan host=", host, " endpoint=", endpoint, " outcome=refused cause=", trim(s: e), "\n", + ], "") } } @@ -278,7 +312,7 @@ func fleet_host_key_enroll_apply() -> String join([ "enroll host=", k.host as String, " endpoint=", k.endpoint, " provenance=", host_key_provenance_label(p: k.provenance), - if f.success { " readback=found-in-pinned-fragment" } else { " readback=ABSENT" }, "\n", + if process_outcome_admitted(outcome: f) { " readback=found-in-pinned-fragment" } else { " readback=ABSENT" }, "\n", ], "") }), "") } @@ -334,29 +368,39 @@ func fleet_authorized_key_self_enroll_wet() -> ProcessExit command: ArgvCommand { argv: ["sh", "-c", "H=$(getent passwd \"$(whoami)\" | cut -d: -f6); grep -qxF \"$(cat target/fleet-authorized-key-line | head -1)\" \"$H/.ssh/authorized_keys\" 2>/dev/null && echo present || echo absent"] }, transport: LocalExec, ) - if trim(s: check.stdout) == "present" { + // THE DEFECT THIS MIGRATION EXISTS FOR. The old test was `trim(check.stdout) == "present"` + // with no consultation of success, so a probe that FAILED produced "" -- not "present" -- and + // fell through to the else branch, which APPLIES. A refusal to read the file was therefore + // indistinguishable from the key being absent, and the remedy for the two states is opposite: + // absent means write it, unreadable means stop and say so. Matching the arms makes the third + // state impossible to fall through: a refusal now refuses instead of mutating the file. + match check { + ProcessRefused { exit_code: _, stderr: ce } => + join(["outcome=refused cause=presence-probe refused, not applying: ", trim(s: ce)], "") + ProcessOutputAbsent => + "outcome=refused cause=presence-probe admitted but printed nothing, not applying" + ProcessOutputPresent { text: ct } => + if trim(s: ct) == "present" { "outcome=already-present" } else { let apply = run_shell_command_capture( command: ArgvCommand { argv: ["sh", "-c", "H=$(getent passwd \"$(whoami)\" | cut -d: -f6); mkdir -p \"$H/.ssh\" && chmod 700 \"$H/.ssh\" && touch \"$H/.ssh/authorized_keys\" && chmod 600 \"$H/.ssh/authorized_keys\" && cat target/fleet-authorized-key-line >> \"$H/.ssh/authorized_keys\""] }, transport: LocalExec, ) - if apply.success { - let verify = run_shell_command_capture( - command: ArgvCommand { argv: ["sh", "-c", "H=$(getent passwd \"$(whoami)\" | cut -d: -f6); grep -qxF \"$(cat target/fleet-authorized-key-line | head -1)\" \"$H/.ssh/authorized_keys\" && echo enrolled || echo ABSENT-after-apply"] }, - transport: LocalExec, - ) - concat("outcome=", trim(s: verify.stdout)) - } else { - join(["outcome=refused cause=", trim(s: apply.stderr)], "") + match apply { + ProcessRefused { exit_code: _, stderr: ae } => + join(["outcome=refused cause=", trim(s: ae)], "") + ProcessOutputPresent { text: _ } => verify_enrollment_outcome() + ProcessOutputAbsent => verify_enrollment_outcome() } } + } } else { join(["outcome=refused cause=staging: ", w.error], "") } let body = join([ - "authorized-key-self-enroll host=", trim(s: hostname.stdout), - " user=", trim(s: user.stdout), " ", outcome, "\n", + "authorized-key-self-enroll host=", process_outcome_receipt_text(outcome: hostname), + " user=", process_outcome_receipt_text(outcome: user), " ", outcome, "\n", ], "") let wr = Filesystem.Write(path: fleet_authorized_key_enroll_receipt_path, content: body) if wr.success { diff --git a/dag/gunbc/fleet_probe_identity_observe.dag b/dag/gunbc/fleet_probe_identity_observe.dag index 82d72760f3c..514dfab939a 100644 --- a/dag/gunbc/fleet_probe_identity_observe.dag +++ b/dag/gunbc/fleet_probe_identity_observe.dag @@ -6,7 +6,8 @@ import std.process { ProcessExit, ExitSuccess, exit_failure } import std.resources { Network } import extdeps.filesystem.filesystem_io { Filesystem } import extdeps.exec.command { ArgvCommand, LocalExec } -import gunbc.command_runner { run_shell_command_capture } +import gunbc.command_runner { run_shell_command_capture, process_outcome_receipt_text } +import extdeps.shell.exec { ProcessOutcome, ProcessOutputPresent, ProcessOutputAbsent, ProcessRefused } import gunbc.fleet_ssh_access { fleet_automation_ssh_key } // Observe-first for the probe-identity decision (parent msg_156e62bd): READ-ONLY @@ -20,25 +21,29 @@ import gunbc.fleet_ssh_access { fleet_automation_ssh_key } data fleet_probe_identity_receipt_path: String = "target/fleet-probe-identity-observe-receipt.txt" fn observe_capture_line(label: String, argv: List) -> String { - let r = run_shell_command_capture(command: ArgvCommand { argv: argv }, transport: LocalExec) - if r.success { - join([label, " outcome=observed value=", trim(s: r.stdout), "\n"], "") - } else { - join([label, " outcome=refused cause=", trim(s: r.stderr), "\n"], "") + match run_shell_command_capture(command: ArgvCommand { argv: argv }, transport: LocalExec) { + ProcessOutputPresent { text: t } => + join([label, " outcome=observed value=", trim(s: t), "\n"], "") + ProcessOutputAbsent => + join([label, " outcome=observed-empty value=\n"], "") + ProcessRefused { exit_code: _, stderr: e } => + join([label, " outcome=refused cause=", trim(s: e), "\n"], "") } } fn observe_authorized_keys_line(home: String) -> String { let path = concat(home, "/.ssh/authorized_keys") - let read = run_shell_command_capture(command: ArgvCommand { argv: ["cat", path] }, transport: LocalExec) - if read.success { - if string_contains(s: read.stdout, pattern: fleet_automation_ssh_key.material) { + match run_shell_command_capture(command: ArgvCommand { argv: ["cat", path] }, transport: LocalExec) { + ProcessOutputPresent { text: read_text } => + if string_contains(s: read_text, pattern: fleet_automation_ssh_key.material) { join(["authorized-keys home=", home, " outcome=fleet-key-present\n"], "") } else { join(["authorized-keys home=", home, " outcome=fleet-key-absent (file readable, key material not found)\n"], "") } - } else { - join(["authorized-keys home=", home, " outcome=unreadable cause=", trim(s: read.stderr), "\n"], "") + ProcessOutputAbsent => + join(["authorized-keys home=", home, " outcome=fleet-key-absent (file readable and empty)\n"], "") + ProcessRefused { exit_code: _, stderr: e } => + join(["authorized-keys home=", home, " outcome=unreadable cause=", trim(s: e), "\n"], "") } } @@ -54,13 +59,17 @@ func fleet_probe_identity_observe_wet() -> ProcessExit command: ArgvCommand { argv: ["sh", "-c", "echo \"$HOME\"" ] }, transport: LocalExec, ) - let ph = trim(s: passwd_home.stdout) - let jh = trim(s: job_home.stdout) + // ph and jh are USED AS PATHS below, not merely printed, so they match the arms rather than + // routing through the receipt-text projection: "(refused: ...)" is fine to print and wrong to + // open. An unreadable home yields "" here and the guarded call below skips the probe entirely + // rather than reading /.ssh/authorized_keys off a fabricated root. + let ph = match passwd_home { ProcessOutputPresent { text: t } => trim(s: t) ProcessOutputAbsent => "" ProcessRefused { exit_code: _, stderr: _ } => "" } + let jh = match job_home { ProcessOutputPresent { text: t } => trim(s: t) ProcessOutputAbsent => "" ProcessRefused { exit_code: _, stderr: _ } => "" } let body = join([ - join(["observer user=", trim(s: user.stdout), " passwd-home=", ph, " job-home=", jh, "\n"], ""), + join(["observer user=", process_outcome_receipt_text(outcome: user), " passwd-home=", process_outcome_receipt_text(outcome: passwd_home), " job-home=", process_outcome_receipt_text(outcome: job_home), "\n"], ""), "local-host-note only the host this runner occupies is locally observable pre-auth; srv2-srv4 authorized_keys standing is PENDING-FIRST-AUTH (recorded, not assumed)\n", - observe_authorized_keys_line(home: ph), - if jh != ph { observe_authorized_keys_line(home: jh) } else { "" }, + if ph != "" { observe_authorized_keys_line(home: ph) } else { "authorized-keys home=(passwd home unreadable) outcome=not-probed\n" }, + if jh != ph && jh != "" { observe_authorized_keys_line(home: jh) } else { "" }, observe_capture_line(label: "gcloud-binary", argv: ["sh", "-c", "command -v gcloud || echo absent"]), observe_capture_line(label: "gcloud-auth-list", argv: ["sh", "-c", "command -v gcloud >/dev/null && gcloud auth list --format=value(account) 2>&1 || echo gcloud-absent"]), observe_capture_line(label: "adc-env", argv: ["sh", "-c", "echo \"$\{GOOGLE_APPLICATION_CREDENTIALS:-absent}\""]), diff --git a/dag/gunbc/fleet_ssh_credential_verify.dag b/dag/gunbc/fleet_ssh_credential_verify.dag index 4a71322f61e..3d5df424454 100644 --- a/dag/gunbc/fleet_ssh_credential_verify.dag +++ b/dag/gunbc/fleet_ssh_credential_verify.dag @@ -15,7 +15,8 @@ import std.content_hash { ContentHashDifferent, ContentHashCrossFamilyIncomparable, } -import gunbc.command_runner { ShellCaptureResult, run_shell_command_capture } +import gunbc.command_runner { run_shell_command_capture } +import extdeps.shell.exec { ProcessOutcome, ProcessOutputPresent, ProcessOutputAbsent, ProcessRefused } import gunbc.fleet_known_hosts_anchor { FleetSshAttemptIdentity, FleetSshCredentialBinding, @@ -97,7 +98,7 @@ fn classify_derived_public_key_line( // The observation, carrying no judgment. `LocalExec` because the identity file is on the machine // running the workflow; this must never reach a remote host, since the whole point is to decide // whether to contact one at all. -func derive_identity_file_public_key_line(identity_file: NonEmptyStr) -> ShellCaptureResult +func derive_identity_file_public_key_line(identity_file: NonEmptyStr) -> ProcessOutcome uses net: Network { run_shell_command_capture( @@ -114,14 +115,29 @@ func verify_fleet_ssh_credential( ) -> FleetSshCredentialVerification uses net: Network { - let observation = derive_identity_file_public_key_line(identity_file: identity_file) - classify_derived_public_key_line( - identity_file: identity_file, - expected_key: expected_key, - derivation_succeeded: observation.success, - derivation_stdout: observation.stdout, - derivation_stderr: observation.stderr, - ) + // DECOMPOSED AT THE CLASSIFIER BOUNDARY, and this is not the conflation surviving one layer + // out. classify_derived_public_key_line consumes all three values TOGETHER and its own arms + // distinguish them, so the correlation is performed rather than skipped. What the match adds is + // that the decomposition is now exhaustive over the outcome instead of reading two fields and + // hoping they agree -- and ProcessOutputAbsent, previously indistinguishable from a failure with + // empty stdout, is stated. + match derive_identity_file_public_key_line(identity_file: identity_file) { + ProcessOutputPresent { text: t } => + classify_derived_public_key_line( + identity_file: identity_file, expected_key: expected_key, + derivation_succeeded: true, derivation_stdout: t, derivation_stderr: "", + ) + ProcessOutputAbsent => + classify_derived_public_key_line( + identity_file: identity_file, expected_key: expected_key, + derivation_succeeded: true, derivation_stdout: "", derivation_stderr: "", + ) + ProcessRefused { exit_code: _, stderr: e } => + classify_derived_public_key_line( + identity_file: identity_file, expected_key: expected_key, + derivation_succeeded: false, derivation_stdout: "", derivation_stderr: e, + ) + } } // ── The agent selector file ───────────────────────────────────────────────────────────────────── @@ -275,7 +291,7 @@ fn classify_agent_key_listing( // The observation. `SSH_AUTH_SOCK` is passed explicitly rather than inherited, so the agent that // answered is the agent the binding names. -func list_agent_identities(agent_socket: NonEmptyStr) -> ShellCaptureResult +func list_agent_identities(agent_socket: NonEmptyStr) -> ProcessOutcome uses net: Network { run_shell_command_capture( @@ -294,16 +310,26 @@ func verify_fleet_ssh_agent_credential( ) -> FleetSshCredentialVerification uses net: Network { - let observation = list_agent_identities(agent_socket: agent_socket) - classify_agent_key_listing( - agent_socket: agent_socket, - selector: selector, - expected_key: expected_key, - expected_fingerprint: expected_fingerprint, - listing_succeeded: observation.success, - listing_stdout: observation.stdout, - listing_stderr: observation.stderr, - ) + match list_agent_identities(agent_socket: agent_socket) { + ProcessOutputPresent { text: t } => + classify_agent_key_listing( + agent_socket: agent_socket, selector: selector, expected_key: expected_key, + expected_fingerprint: expected_fingerprint, + listing_succeeded: true, listing_stdout: t, listing_stderr: "", + ) + ProcessOutputAbsent => + classify_agent_key_listing( + agent_socket: agent_socket, selector: selector, expected_key: expected_key, + expected_fingerprint: expected_fingerprint, + listing_succeeded: true, listing_stdout: "", listing_stderr: "", + ) + ProcessRefused { exit_code: _, stderr: e } => + classify_agent_key_listing( + agent_socket: agent_socket, selector: selector, expected_key: expected_key, + expected_fingerprint: expected_fingerprint, + listing_succeeded: false, listing_stdout: "", listing_stderr: e, + ) + } } // The refusal reason a consumer reports when it declines to proceed. Kept beside the coproduct so a diff --git a/dag/test/manual/command_runner_local_argv_receipt_test.dag b/dag/test/manual/command_runner_local_argv_receipt_test.dag index 2dd563be894..f9da00ba81f 100644 --- a/dag/test/manual/command_runner_local_argv_receipt_test.dag +++ b/dag/test/manual/command_runner_local_argv_receipt_test.dag @@ -2,7 +2,8 @@ module test.manual.command_runner_local_argv_receipt import std.types { Bool, String } import extdeps.exec.command { ArgvCommand, LocalExec } -import gunbc.command_runner { run_shell_command_capture } +import gunbc.command_runner { run_shell_command_capture, process_outcome_receipt_text } +import extdeps.shell.exec { ProcessOutputPresent, ProcessOutputAbsent, ProcessRefused } // THE DISCRIMINATING RECEIPT FOR THE LOCAL ARGV CUT. // @@ -27,27 +28,84 @@ import gunbc.command_runner { run_shell_command_capture } // test/manual/process_argv_expansion_receipt_test.dag is, for the same reason. test fn spaced_operand_survives_as_one_argument() -> Bool { - run_shell_command_capture( - command: ArgvCommand { argv: ["printf", "%s|", "a b"] }, - transport: LocalExec, - ).stdout == "a b|" + process_outcome_receipt_text( + outcome: run_shell_command_capture( + command: ArgvCommand { argv: ["printf", "%s|", "a b"] }, + transport: LocalExec, + ) + ) == "a b|" } // The RED half of the same observation, stated as its own assertion rather than left implicit in // the equality above: the shell-split rendering must NOT be what comes back. Written separately so // a future edit that weakens the positive into something like a nonempty check still trips here. test fn shell_split_rendering_is_not_what_comes_back() -> Bool { - run_shell_command_capture( - command: ArgvCommand { argv: ["printf", "%s|", "a b"] }, - transport: LocalExec, - ).stdout != "a|b|" + process_outcome_receipt_text( + outcome: run_shell_command_capture( + command: ArgvCommand { argv: ["printf", "%s|", "a b"] }, + transport: LocalExec, + ) + ) != "a|b|" } // Control that the runner works at all on the ordinary case, so a failure above is read as a // splitting regression rather than as the whole path being broken. test fn plain_operand_round_trips() -> Bool { - run_shell_command_capture( - command: ArgvCommand { argv: ["printf", "%s|", "plain"] }, + process_outcome_receipt_text( + outcome: run_shell_command_capture( + command: ArgvCommand { argv: ["printf", "%s|", "plain"] }, + transport: LocalExec, + ) + ) == "plain|" +} + +// THE DISCRIMINATING RED FOR THE COPRODUCT MIGRATION. +// +// The two states the old ShellCaptureResult could not tell apart: +// a program that RAN AND FAILED printing nothing -> success=false, stdout="" +// a program that RAN AND SUCCEEDED printing nothing -> success=true, stdout="" +// Both are stdout == "". Eight live sites read stdout without consulting success, so at every one +// of them a failure and an empty result were the same value. +// +// NOTE WHAT IS *NOT* BEING TESTED, because it was the first RED proposed and it proves nothing: a +// program that does not EXIST is already distinguishable, because the transport refuses the whole +// evaluation with a typed diagnostic naming the program and the OS error. That property holds with +// or without this migration, so a test of it would pass against the old record too. +// +// These two go red if ShellCaptureResult is restored, because then both arms are stdout == "" and +// nothing in the value distinguishes them. + +test fn nonzero_exit_printing_nothing_is_refused_not_absent() -> Bool { + match run_shell_command_capture( + command: ArgvCommand { argv: ["sh", "-c", "exit 3"] }, + transport: LocalExec, + ) { + ProcessRefused { exit_code: _, stderr: _ } => true + ProcessOutputAbsent => false + ProcessOutputPresent { text: _ } => false + } +} + +test fn zero_exit_printing_nothing_is_absent_not_refused() -> Bool { + match run_shell_command_capture( + command: ArgvCommand { argv: ["true"] }, + transport: LocalExec, + ) { + ProcessOutputAbsent => true + ProcessRefused { exit_code: _, stderr: _ } => false + ProcessOutputPresent { text: _ } => false + } +} + +// The positive arm, so a failure above reads as a lost distinction rather than as everything +// collapsing into one variant. +test fn zero_exit_with_output_is_present() -> Bool { + match run_shell_command_capture( + command: ArgvCommand { argv: ["printf", "%s", "value"] }, transport: LocalExec, - ).stdout == "plain|" + ) { + ProcessOutputPresent { text: t } => t == "value" + ProcessOutputAbsent => false + ProcessRefused { exit_code: _, stderr: _ } => false + } } From 00b562e7582752c2e504a019b0837094f848a61e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 20 Aug 2026 01:35:04 +0000 Subject: [PATCH 14/16] =?UTF-8?q?Site=208:=20the=20poison=20IS=20persisted?= =?UTF-8?q?,=20and=20it=20defeats=20the=20guard=20=E2=80=94=20second=20row?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- dag/gunbc/fleet_converge_plan_cli.dag | 53 +++++++++++++++++++-------- 1 file changed, 37 insertions(+), 16 deletions(-) diff --git a/dag/gunbc/fleet_converge_plan_cli.dag b/dag/gunbc/fleet_converge_plan_cli.dag index 2d07c17b070..f3776fc32e4 100644 --- a/dag/gunbc/fleet_converge_plan_cli.dag +++ b/dag/gunbc/fleet_converge_plan_cli.dag @@ -39,25 +39,46 @@ data fleet_converge_plan_spark_typed_actions_wire_path: String = "/tmp/fleet-con data fleet_converge_plan_cli_note: String = "Wet CLI for on-demand fleet converge plan/apply (sleek-heron-218). Plan observes the host, runs membership_reconcile once, names the subject (host + member-set fingerprint), mints a std.temporal_effect LeaseEpoch generation in the artifact, and writes the human-readable plan plus apply.sh. plan_content.hex is the Fnv1a64Structural bundle digest of plan.txt + apply.sh + spark_serving_typed_actions.wire (empty wire on non-Spark hosts); on success plan_wet prints plan.txt then that digest for workflow_dispatch plan_artifact_hash. Apply re-observes subject identity and observed-baseline fingerprint in .dag, refuses unless on-disk plan.txt + apply.sh + spark wire match plan_content.hex, then runs fleet_converge_locked_apply_script under flock. Generation store reads refuse corrupt or negative values; a missing store file is generation 0." +// STATED, NOT SILENTLY DEFAULTED. This value KEYS THE CONVERGE PLAN's subject identity, so a +// hostname that could not be read must not become "" and flow into a plan named for the wrong +// host. The old code took .stdout straight off the call expression -- no binding, so there was +// not even a variable a later author could think to check. +// +// WHAT THIS DOES AND DOES NOT FIX, stated because the residue is real. A `-> String` function +// has no way to refuse: the substrate offers no abort from this position, so the only honest +// options are to change the return type or to return a value. This returns a value that CANNOT +// BE MISTAKEN FOR A HOSTNAME -- deliberately implausible rather than plausibly empty -- so a +// plan keyed on it is visibly wrong at a glance instead of silently wrong forever. That is +// strictly better than "" and is still not a refusal. +// +// RUNG: mitigatable, not fixed. The conflation is surfaced, not closed. NEXT-RUNG TRIGGER: this +// function returns an optional (or a typed outcome) and its two callers handle the absent case; +// that cascades into plan subject identity, which is a different change from this migration and +// deliberately not attempted inside it. +// +// SECOND ROW, SEPARATE FROM THE ONE ABOVE BECAUSE ITS REACHABILITY IS DIFFERENT AND WORSE. The +// row above says the value is visibly wrong rather than plausibly empty. It does NOT say the +// value dies before it is recorded, and it does not: 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. So an +// unobserved hostname IS PERSISTED as a receipt that later reads as fact. +// +// AND IT DEFEATS THE GUARD THAT EXISTS TO CATCH EXACTLY THIS. 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 whole +// purpose is to stop a plan being applied on the wrong host is satisfied by two non-observations +// agreeing with each other. That is the empty-observation narrow at the guard: bottom == bottom +// read as "same host". Making the marker unique per call would NOT fix it -- it would convert a +// false match into a false mismatch, which is a different wrong answer, not an observation. +// +// NOT INTRODUCED HERE, AND SAYING SO PRECISELY: the prior code persisted "" and compared "" == "", +// which passed identically. The defect predates this migration and this migration does not repair +// it -- it makes the persisted evidence legible instead of blank. Rung: mitigatable. NEXT-RUNG +// TRIGGER: the subject-host comparison consumes an outcome rather than a String, so that +// unobserved-vs-unobserved is a REFUSAL to compare and not an equality. func observe_host_short_wet() -> String uses net: Network { - // STATED, NOT SILENTLY DEFAULTED. This value KEYS THE CONVERGE PLAN's subject identity, so a - // hostname that could not be read must not become "" and flow into a plan named for the wrong - // host. The old code took .stdout straight off the call expression -- no binding, so there was - // not even a variable a later author could think to check. - // - // WHAT THIS DOES AND DOES NOT FIX, stated because the residue is real. A `-> String` function - // has no way to refuse: the substrate offers no abort from this position, so the only honest - // options are to change the return type or to return a value. This returns a value that CANNOT - // BE MISTAKEN FOR A HOSTNAME -- deliberately implausible rather than plausibly empty -- so a - // plan keyed on it is visibly wrong at a glance instead of silently wrong forever. That is - // strictly better than "" and is still not a refusal. - // - // RUNG: mitigatable, not fixed. The conflation is surfaced, not closed. NEXT-RUNG TRIGGER: this - // function returns an optional (or a typed outcome) and its two callers handle the absent case; - // that cascades into plan subject identity, which is a different change from this migration and - // deliberately not attempted inside it. match run_shell_command_capture( command: ArgvCommand { argv: ["hostname", "-s"] }, transport: LocalExec, From b87367fe80b14f57c474c2a673a0124f4da6de12 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 20 Aug 2026 02:02:32 +0000 Subject: [PATCH 15/16] =?UTF-8?q?Hoist=2029=20body=20annotations=20to=20mo?= =?UTF-8?q?dule-item=20grain=20(=C2=A74c),=20and=20integrate=20main's=20co?= =?UTF-8?q?mmand=5Fover=5Ftransport=20refusal=20coproduct?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) From a750b6761da5aa6c0f8948288c5f78404b67447d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 20 Aug 2026 02:25:11 +0000 Subject: [PATCH 16/16] Take main's optional-hostname repair and re-express it on ProcessOutcome; 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)