From 868a4977cd562fef54e1d7de9aa61c46368543d6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 01:42:23 +0000 Subject: [PATCH 01/21] Record the SCM demo CLI rebuild plan and its API inventory A working 'gunbc scm' CLI existed and was lost with an uncommitted /tmp worktree, along with the plan doc describing it. This commits the survey so the rebuild does not start by re-reading every scm module, and so the next context loss costs nothing. The useful finding from re-surveying: the gap is smaller and more specific than 'build a CLI'. gunbc.scm.render ALREADY reaches CliWireResponse via scm_log_cli_response and scm_status_cli_response -- they simply have no consumer outside dag/test/claim/scm/scm_render_witness_test.dag, which is the unwired-renderer state gunbc.cli_dispatch_surface already records. It also states why the corpus's idiomatic instrument shape cannot substitute for the host binding: 'fn check(...) -> ProcessExit' can only emit text on FAILURE (exit_failure's reason), and log/status must print on success. That is the argument for the main.rs work rather than a workaround, and it is the thing I would otherwise have had to re-derive. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT --- docs/plans/scm-demo-cli-rebuild.md | 75 ++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 docs/plans/scm-demo-cli-rebuild.md diff --git a/docs/plans/scm-demo-cli-rebuild.md b/docs/plans/scm-demo-cli-rebuild.md new file mode 100644 index 00000000000..87738c17fb7 --- /dev/null +++ b/docs/plans/scm-demo-cli-rebuild.md @@ -0,0 +1,75 @@ +# SCM demo CLI — rebuild plan and API inventory + +A working `gunbc scm` CLI existed and was lost with an uncommitted `/tmp` worktree. This doc is +the durable record so the rebuild does not start from a survey again. It is a plan, not a +receipt: nothing here claims to be built. + +## What already exists on main (verified by reading the modules) + +The read side is modelled and already reaches `CliWireResponse`: + +| module | symbol | shape | +| --- | --- | --- | +| `gunbc.scm.read_command` | `ScmReadResult` | `ScmReadAnswered { path, answer }` \| `ScmReadRepositoryUnavailable { cause }` | +| `gunbc.scm.render` | `scm_log_cli_response(result, target, capability)` | `-> CliWireResponse` | +| `gunbc.scm.render` | `scm_status_cli_response(result, target, capability)` | `-> CliWireResponse` | +| `gunbc.scm.render` | `scm_read_exit(result)` | `-> ProcessExit` | +| `gunbc.scm.log` | `repository_log(envelope)` | `-> CommitLog` | +| `gunbc.scm.status` | `repository_status(envelope, pending)` | `-> RepositoryStatus` | +| `gunbc.scm.repository_load` | `load_repository(path)` | `-> RepositoryLoad` | +| `gunbc.scm.repository_load` | `repository_load_refusal_lines(cause)` | `-> List` (takes `cause` ONLY, not `path`) | +| `gunbc.scm.repository_save` | `save_repository(path, repo)` | `-> RepositorySave` | +| `gunbc.scm.repository_envelope` | `empty_repository()` | `-> RepositoryEnvelope` | +| `gunbc.scm.repository_envelope` | `mint_repository_commit(...)` | `-> RepositoryCommitMint` | +| `gunbc.scm.repository_envelope` | `commit_at_reference(commits, reference)` | `-> RepositoryCommit?` | +| `gunbc.scm.checkout` | `checkout_repository_at(repo, reference)` | `-> RepositoryCheckout` | +| `gunbc.scm.authoring` | `empty_proposal()`, `author_requirement(proposal, requirement)` | `-> Proposal` | +| `gunbc.scm.object_store` | `empty_store()`, `store_contains`, `find_object`, `store_object_count` | — | + +## The gap, stated precisely + +`scm_log_cli_response` and `scm_status_cli_response` have NO consumer outside +`dag/test/claim/scm/scm_render_witness_test.dag`. That is the unwired-renderer state +`gunbc.cli_dispatch_surface` already records: the answer is computed and discarded because no +host binds it. + +`dag/gunbc/cli_dispatch_surface.dag` declares an `scm` verb with an operand and `--path`, marked +`AbsentFromEmitMainRs`. + +## Two host shapes, and why the idiomatic one is not sufficient + +The corpus's established instrument shape is `fn check(subject) -> ProcessExit`, returning +`exit_failure(reason: join(lines, "\n"))` — see `tools.bare_name_fork_check`. `gunbc run` prints +that reason. **It can only emit text on FAILURE.** `log` and `status` must print on SUCCESS, so +that shape cannot express them, and returning `CliWireResponse` from `gunbc run` refuses (its +not-`ProcessExit` refusal prints the value, which is not a CLI). + +So the host binding is REQUIRED, and it is the piece to rebuild: + +1. `dag/gunbc/scm/cli.dag` — one entry per verb returning `CliWireResponse`, composing + `load_repository` -> verb -> render, with a `RenderCapability { color: false, tier: Ascii, + cursor_addressable: false }` for a plain terminal. Write verbs (`init`, `add`, `commit`, + `checkout`) need their own `Document` builders; only log/status have them today. +2. Host side in `src/v1/stage0/src/main.rs`: a `Commands::Scm` variant and a `scm_verb` that + evaluates the entry and writes the `CliWirePrintable { bytes, exit }` bytes to stdout, + refusing on `CliWireUnprintable { cause }`. `serve_wire_fields` / `classify_exit` in + `cli_run.rs` are the precedent for reading wire values out of an evaluated `Value`. + +## Constraints learned the hard way + +- A runtime name becomes a `Symbol` via `symbol_intern_lexeme(lexeme: name)` + (`v2.std.compilers.lexing`). `name as Symbol` REFUSES; an earlier conclusion that runtime names + were inexpressible was wrong. +- `RepositoryCommitRef` has no `ordinal` field. Read it with `minted_id_ordinal(id: ref.identity)` + and construct via `RepositoryCommitRef { identity: MintedId { ordinal } }`. +- Annotations inside a declaration body are parse errors; hoist them above the declaration. + An indented `//` is also a parse error — annotations are module-item grain only. +- `gunbc.scm.merge` is roles/requirements/supersession, NOT two-commit merging. The operator's + ask for practising merges/conflict resolution needs merge DESIGN first; it is not a wiring job. + +## Not in scope here + +Mirroring this repository's history through `gunbc scm` onto srv2 stays blocked on model work: +`ScmObject = SemanticNodeObject | AuthoredSourceObject | CorpusManifestObject` with one content +identity, `CorpusManifest` carrying path + semantic_root + authored_source_identity, and git +correspondence confined to a mirror-layer `GitMirrorCursor { source_commit, native_commit }`. From 9f2c851c11dca64863c7e8d4ade1c8105dd96158 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 01:53:56 +0000 Subject: [PATCH 02/21] Host reader and pure outcome map for CliWireResponse gunbc.scm.render already produces CliWireResponse (scm_log_cli_response, scm_status_cli_response) and nothing outside its witness test consumes it -- the answer is computed and discarded, which is the unwired-renderer state gunbc.cli_dispatch_surface records. This adds the two host-side pieces that binding needs. classify_cli_wire sits beside classify_exit as the single authority for reading the variant shape, so the driver seam cannot fork it. A missing or wrongly-shaped field is NotCliWire rather than a default: defaulting bytes to "" would print nothing and exit 0, which is a fabricated plausible output. cli_wire_outcome is the total, pure map from that class to what the host does -- bytes, status, message. Pure for the reason exit_status_for records about itself: the inlined version of that decision dropped a case and reported success for every failure. It lives in the LIB, not beside the driver, because main.rs is a BIN target and the rust-unit-tests job runs 'cargo test -p v1-compiler --lib' -- a test written next to the driver is compiled by clippy and executed by nobody. exit_status_for_class is shared by both paths so the wire path and the plain ProcessExit path cannot disagree about what a verdict means. NotCliWire yields None rather than a failure, so the driver falls through to classify_exit and every existing ProcessExit entry behaves exactly as before; a test pins that. 5 executing witnesses: bytes written with the response's own exit, a rendered answer that still fails, the renderer's refusal not reading as an empty success, the fall-through, and the inherited ExitFailure{code:0} refusal. NOT YET WIRED into run_verb -- that is the next commit, and until it lands this reader has no production consumer. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT --- src/v1/stage0/src/cli_run.rs | 255 +++++++++++++++++++++++++++++++++++ 1 file changed, 255 insertions(+) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 54c6baff3cd..f1de1c6c0e0 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -17802,6 +17802,261 @@ pub fn classify_exit( } } +/// The SINGLE AUTHORITY for reading a `.dag` `CliWireResponse` value, sitting beside +/// `classify_exit` for the same §3 reason: the driver seam in `main.rs` must turn that value +/// into bytes on stdout and a process exit code, and reimplementing the match there would +/// fork the one place that knows the variant shape. +/// +/// `gunbc.cli_wire` declares +/// `CliWireResponse = CliWirePrintable { bytes: String, exit: ProcessExit } +/// | CliWireUnprintable { cause: NonEmptyStr }`. +/// +/// Why a host reader is needed at all: `gunbc.scm.render` already produces this value +/// (`scm_log_cli_response`, `scm_status_cli_response`), and outside its witness test NOTHING +/// consumes it -- the answer is computed and discarded, which is the unwired-renderer state +/// `gunbc.cli_dispatch_surface` records. The idiomatic instrument shape cannot stand in for +/// this: `fn check(..) -> ProcessExit` can only emit text through `exit_failure`'s reason, so +/// it cannot print a log or a status on SUCCESS. +pub enum CliWireClass { + /// Bytes to write, and the exit the same response carries. + Printable { bytes: String, exit: ExitClass }, + /// The renderer refused to produce bytes; `cause` is `NonEmptyStr` in the model. + Unprintable { cause: String }, + /// Not a `CliWireResponse` at all — reported with what it actually was. + NotCliWire { type_name: String }, +} + +pub fn classify_cli_wire( + val: &v1_interpreter::Value, + ctx: &v1_interpreter::InterpContext, +) -> CliWireClass { + match val { + v1_interpreter::Value::Variant { + type_name, + variant_name, + fields, + } => { + if !ctx.sym_eq(*type_name, "CliWireResponse") { + return CliWireClass::NotCliWire { + type_name: ctx.resolve(*type_name), + }; + } + if ctx.sym_eq(*variant_name, "CliWirePrintable") { + // A MISSING FIELD IS NOT AN EMPTY ANSWER. Defaulting `bytes` to "" here would + // print nothing and exit 0 — a fabricated plausible output (§5) — so both + // fields must be present and of the declared shape or this is not a printable + // response at all. + let bytes = match ctx.field(fields, "bytes") { + Some(Value::Str(s)) => s.to_string(), + _ => { + return CliWireClass::NotCliWire { + type_name: "CliWireResponse::CliWirePrintable{bytes: }" + .to_string(), + } + } + }; + let exit = match ctx.field(fields, "exit") { + Some(v) => classify_exit(v, ctx), + None => { + return CliWireClass::NotCliWire { + type_name: "CliWireResponse::CliWirePrintable{exit: }" + .to_string(), + } + } + }; + CliWireClass::Printable { bytes, exit } + } else if ctx.sym_eq(*variant_name, "CliWireUnprintable") { + match ctx.field(fields, "cause") { + Some(Value::Str(s)) if !s.is_empty() => CliWireClass::Unprintable { + cause: s.to_string(), + }, + // `cause` is declared NonEmptyStr, so an empty or absent one means the + // value did not come from the modeled constructor. + _ => CliWireClass::NotCliWire { + type_name: "CliWireResponse::CliWireUnprintable{cause: }" + .to_string(), + }, + } + } else { + CliWireClass::NotCliWire { + type_name: format!("CliWireResponse::{}", ctx.resolve(*variant_name)), + } + } + } + other => CliWireClass::NotCliWire { + type_name: ctx.format_value(other), + }, + } +} + +/// What the host must DO about a `CliWireResponse`: bytes to write, a status to exit with, and +/// the message that explains a refusal. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct CliWireOutcome { + pub status: i32, + pub message: Option, + /// Bytes to write to stdout verbatim. `None` means write nothing — never "write an empty + /// string and call it an answer". + pub stdout: Option, +} + +/// TOTAL map from a `CliWireClass` to what the host does, pure for the same reason +/// `exit_status_for` is pure: the impure version of this decision drops cases. It lives in the +/// lib rather than beside the driver in `main.rs` because `main.rs` is a BIN target -- the +/// `rust-unit-tests` job runs `cargo test -p v1-compiler --lib`, so a test written next to the +/// driver would be compiled by clippy and executed by nobody. +/// +/// `NotCliWire` deliberately yields no outcome (`None`): that is not a failure, it is "this +/// value is not a wire response", and the caller must fall through to `classify_exit` so every +/// pre-existing `ProcessExit` entry keeps behaving exactly as before. +pub fn cli_wire_outcome(class: CliWireClass, function: &str) -> Option { + match class { + CliWireClass::Printable { bytes, exit } => { + let (status, message) = exit_status_for_class(exit, function); + Some(CliWireOutcome { + status, + message, + // An empty render is written as nothing rather than suppressed as an error: + // a document with no lines is a legitimate answer (an empty log), and the + // exit the same response carries is what says whether it succeeded. + stdout: if bytes.is_empty() { None } else { Some(bytes) }, + }) + } + CliWireClass::Unprintable { cause } => Some(CliWireOutcome { + status: 1, + message: Some(format!( + "error: `{function}` produced CliWireUnprintable — the renderer refused to \ + produce bytes.\n cause: {cause}\n status: refused — exiting 1 rather than \ + printing nothing and reporting success." + )), + stdout: None, + }), + CliWireClass::NotCliWire { .. } => None, + } +} + +/// The `ExitClass` half of the map, shared by the wire path and the driver's plain +/// `ProcessExit` path so the two cannot disagree about what a verdict means. +/// +/// Kept byte-for-byte equivalent to the driver's own `exit_status_for`, including its refusal +/// of `ExitFailure { code: 0 }` — a variant that claims failure while reporting success. +pub fn exit_status_for_class(class: ExitClass, function: &str) -> (i32, Option) { + match class { + ExitClass::Success => (0, None), + ExitClass::Failure { code: 0, reason } => ( + 1, + Some(format!( + "error: `{function}` returned ExitFailure with code 0, which claims failure \ + and reports success.\n status: refused — exiting 1 rather than honoring a \ + status that contradicts its own variant.{}", + reason + .map(|r| format!("\n reason: {r}")) + .unwrap_or_default() + )), + ), + ExitClass::Failure { code, reason } => (code, reason), + ExitClass::NotProcessExit { type_name } => ( + 2, + Some(format!( + "error: function `{function}` returned `{type_name}`, not `ProcessExit`.\n \ + cause: the host maps a run's verdict to an exit code, and only ProcessExit \ + carries one. Wrap the result in ExitSuccess / ExitFailure." + )), + ), + } +} + +#[cfg(test)] +mod cli_wire_outcome_tests { + use super::{cli_wire_outcome, CliWireClass, ExitClass}; + + #[test] + fn a_printable_response_writes_its_bytes_and_honors_its_own_exit() { + let out = cli_wire_outcome( + CliWireClass::Printable { + bytes: "commit 1\n".to_string(), + exit: ExitClass::Success, + }, + "scm_log_cli_response", + ) + .expect("a printable response is a wire outcome"); + assert_eq!(out.stdout.as_deref(), Some("commit 1\n")); + assert_eq!(out.status, 0); + assert_eq!(out.message, None); + } + + /// The response carries its own exit, so a rendered answer can still fail — a log of a + /// repository that could not be loaded prints its refusal lines AND exits nonzero. + #[test] + fn a_printable_response_can_carry_a_failing_exit() { + let out = cli_wire_outcome( + CliWireClass::Printable { + bytes: "repository unavailable\n".to_string(), + exit: ExitClass::Failure { + code: 1, + reason: Some("repository unavailable".to_string()), + }, + }, + "scm_log_cli_response", + ) + .expect("still a wire outcome"); + assert_eq!(out.stdout.as_deref(), Some("repository unavailable\n")); + assert_eq!(out.status, 1, "the bytes printed, and the run still failed"); + } + + /// The §5 arm: a renderer that refused must not read as an empty successful answer. + #[test] + fn an_unprintable_response_refuses_rather_than_printing_nothing() { + let out = cli_wire_outcome( + CliWireClass::Unprintable { + cause: "cursor addressing unavailable".to_string(), + }, + "scm_status_cli_response", + ) + .expect("a refusal is a wire outcome"); + assert_eq!(out.status, 1); + assert_eq!(out.stdout, None); + let msg = out.message.expect("a refusal explains itself"); + assert!( + msg.contains("cursor addressing unavailable"), + "the modeled cause reaches the operator: {msg}" + ); + } + + /// A non-wire value yields NO outcome, so the driver falls through to classify_exit and + /// every pre-existing ProcessExit entry behaves exactly as it did before this binding. + #[test] + fn a_non_wire_value_yields_no_outcome_so_the_process_exit_path_is_untouched() { + assert_eq!( + cli_wire_outcome( + CliWireClass::NotCliWire { + type_name: "ProcessExit".to_string(), + }, + "check", + ), + None + ); + } + + /// Inherited from the driver's own refusal: a variant that claims failure while reporting + /// success is refused rather than honored. + #[test] + fn an_exit_failure_with_code_zero_is_refused_on_the_wire_path_too() { + let out = cli_wire_outcome( + CliWireClass::Printable { + bytes: "x".to_string(), + exit: ExitClass::Failure { + code: 0, + reason: None, + }, + }, + "f", + ) + .expect("a wire outcome"); + assert_eq!(out.status, 1, "code 0 on a Failure must not become success"); + } +} + #[derive(Debug, Clone, PartialEq, Eq, Serialize)] pub struct ResolvedDeclRef { pub module: String, From b4dee9fbc7e9c8a1b6458113ac74824c679a44d6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 02:13:23 +0000 Subject: [PATCH 03/21] Wire CliWireResponse into run_verb: the SCM answer reaches an operator MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gunbc.scm.render has produced CliWireResponse since it was written, and outside its witness test nothing consumed it. A function returning one hit classify_exit's NotProcessExit arm and the run refused with 'wrap the result in ExitSuccess / ExitFailure', so every gunbc scm answer was computed and discarded -- the unwired-renderer state gunbc.cli_dispatch_surface records. run_verb now tries cli_wire_outcome first and falls through to classify_exit unchanged for every other value. Binding it in the OUTCOME SEAM rather than under a new 'scm' subcommand keeps dispatch peripheral (§3): one binding serves every wire-returning entry instead of the host growing an arm per verb. dag/gunbc/scm/cli.dag is the entry the host invokes -- scm_log and scm_status, composing the read side onto a declared plain-terminal capability. The capability is declared, not detected: a host that learns to report a real one passes it in. PROVEN BY EXECUTION, not by typecheck: gunbc run --entry dag/gunbc/scm/cli.dag --function scm_log --arg path=/tmp/no-such-repo cannot read repository at /tmp/no-such-repo No such file or directory (os error 2) repository unavailable EXIT=1 That is the renderer's own document on stdout AND a nonzero exit -- the 'printable response carrying a failing exit' case, which is the one an absorbing implementation would have turned into either silence or a spurious 0. Also dissolves a fork I had just created: main.rs's exit_status_for carried its own copy of the verdict map, and once the wire path needed the same decision that copy was two places free to drift. The body now lives in cli_run::exit_status_for_class, where an executing test can reach it -- rust-unit-tests runs 'cargo test --lib', and main.rs is a bin whose tests are compiled by clippy and run by nobody. clippy --all-targets -D warnings: clean. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT --- dag/gunbc/scm/cli.dag | 57 ++++++++++++++++++++++++++ src/v1/stage0/src/main.rs | 84 +++++++++++++++++++++++++-------------- 2 files changed, 111 insertions(+), 30 deletions(-) create mode 100644 dag/gunbc/scm/cli.dag diff --git a/dag/gunbc/scm/cli.dag b/dag/gunbc/scm/cli.dag new file mode 100644 index 00000000000..82f0584be40 --- /dev/null +++ b/dag/gunbc/scm/cli.dag @@ -0,0 +1,57 @@ +module gunbc.scm.cli + +// THE ONE PLACE A READ VERB BECOMES BYTES AN OPERATOR CAN SEE. +// +// `gunbc.scm.read_command` composes load-then-ask and names no destination; `gunbc.scm.render` +// turns that answer into a `CliWireResponse`. Both existed before this module and neither had a +// consumer outside a witness test, so every `gunbc scm` answer was computed and discarded -- +// the unwired-renderer state `gunbc.cli_dispatch_surface` already records. This module is the +// entry the host actually invokes: `gunbc run --entry dag/gunbc/scm/cli.dag --function scm_log +// --arg path=`. +// +// WHY A `path` PARAMETER AND NOT A DISCOVERED ROOT. `load_repository` takes a path, and +// inventing a default here (cwd, an env var, a conventional `.gunbc` directory) would make this +// module decide a question its authority left open -- the same reason `scm_read_status` takes +// `pending` as a parameter rather than reading it from somewhere. +// +// THE CAPABILITY IS DECLARED, NOT DETECTED. `plain_terminal_capability` claims no colour, ASCII +// tier and no cursor addressing, which is the floor every terminal meets. Detecting the real +// terminal's capability is a host observation this module cannot make and must not fabricate; +// when a host learns to report one, it passes it in and this row becomes the fallback rather +// than the answer. +import std.render { RenderCapability } +import std.symbols { Ascii } +import extdeps.render.surface { RenderTarget, PlainTerminal } +import gunbc.cli_wire { CliWireResponse } +import gunbc.scm.authoring { empty_proposal } +import gunbc.scm.read_command { scm_read_log, scm_read_status } +import gunbc.scm.render { scm_log_cli_response, scm_status_cli_response } + +data plain_terminal_capability: RenderCapability = RenderCapability { + color: false, + tier: Ascii, + cursor_addressable: false +} + +data plain_terminal_target: RenderTarget = PlainTerminal + +fn scm_log(path: String) -> CliWireResponse { + scm_log_cli_response( + result: scm_read_log(path: path), + target: plain_terminal_target, + capability: plain_terminal_capability + ) +} + +// STATUS OF A REPOSITORY WITH NOTHING STAGED. `repository_status` needs a pending `Proposal`, +// and a CLI reading a repository document has no staging area to read one from -- the document +// does not carry what is staged. `empty_proposal()` is therefore the honest argument for this +// entry, and it is a REAL limitation rather than a placeholder: a verb that reports staged roles +// needs a staging authority to exist first, and none does. +fn scm_status(path: String) -> CliWireResponse { + scm_status_cli_response( + result: scm_read_status(path: path, pending: empty_proposal()), + target: plain_terminal_target, + capability: plain_terminal_capability + ) +} diff --git a/src/v1/stage0/src/main.rs b/src/v1/stage0/src/main.rs index eaee06f5860..25b38620641 100644 --- a/src/v1/stage0/src/main.rs +++ b/src/v1/stage0/src/main.rs @@ -1153,8 +1153,53 @@ fn run_verb( // is the single authority for reading the ProcessExit variant; `exit_status_for` // is the total map from that class to a status. Ok(value) => { - let (status, message) = exit_status_for(cli_run::classify_exit(&value, &ctx), function); - Verdict { status, message } + // A `CliWireResponse` is an ANSWER PLUS A VERDICT, and it is the only return shape + // that carries bytes for the operator. Binding it HERE rather than under a new + // `scm` subcommand keeps dispatch peripheral (§3): one binding serves every + // wire-returning entry -- `scm_log_cli_response`, `scm_status_cli_response`, and + // whatever else renders next -- instead of the host growing an arm per verb. + // + // Before this, such a function hit `classify_exit`'s `NotProcessExit` arm and the + // run refused with "wrap the result in ExitSuccess / ExitFailure", which is why + // gunbc.scm.render's two wire functions had no consumer outside their witness + // test: the answer was computed and discarded. + // + // A non-wire value falls through unchanged, so every existing `ProcessExit` entry + // behaves exactly as it did. + match cli_run::cli_wire_outcome(cli_run::classify_cli_wire(&value, &ctx), function) { + Some(outcome) => { + if let Some(bytes) = outcome.stdout { + use std::io::Write; + let mut out = std::io::stdout(); + // Written verbatim: the .dag renderer already decided every byte, + // including trailing newlines. `print!` plus an implicit flush-at-exit + // is not enough when the process exits nonzero, so flush explicitly + // and refuse rather than silently dropping the answer. + if let Err(err) = out.write_all(bytes.as_bytes()).and_then(|()| out.flush()) + { + return Verdict { + status: 1, + message: Some(format!( + "error: `{function}` rendered {} bytes that could not be \ + written to stdout.\n cause: {err}\n status: refused — \ + exiting nonzero rather than reporting success for an \ + answer the operator never received.", + bytes.len() + )), + }; + } + } + Verdict { + status: outcome.status, + message: outcome.message, + } + } + None => { + let (status, message) = + exit_status_for(cli_run::classify_exit(&value, &ctx), function); + Verdict { status, message } + } + } } Err(err) => Verdict { status: 1, @@ -1183,34 +1228,13 @@ fn run_verb( /// `mechanically preventable` ONLY where the suite is run by hand; in CI it rests on the /// totality above. The planted-drift control is a manual procedure recorded in the PR. fn exit_status_for(class: cli_run::ExitClass, function: &str) -> (i32, Option) { - match class { - cli_run::ExitClass::Success => (0, None), - // A `Failure` carrying code 0 would say "failed" and report success. Refuse: the .dag - // authority cannot express it, so reaching here means the classifier changed, and the - // safe reading of an impossible verdict is not 0. - cli_run::ExitClass::Failure { code: 0, reason } => ( - 1, - Some(format!( - "error: `{function}` returned ExitFailure with code 0, which claims failure \ - and reports success.\n status: refused — exiting 1 rather than honoring a \ - status that contradicts its own variant.{}", - reason - .map(|r| format!("\n reason: {r}")) - .unwrap_or_default() - )), - ), - cli_run::ExitClass::Failure { code, reason } => (code, reason), - cli_run::ExitClass::NotProcessExit { type_name } => ( - 2, - Some(format!( - "error: function `{function}` returned `{type_name}`, not `ProcessExit`.\n \ - cause: the host maps a run's verdict to an exit code, and only ProcessExit \ - carries one. Wrap the result in ExitSuccess / ExitFailure.\n \ - status: refused — printing the value and exiting 0 would report success for \ - a run whose outcome is unknown." - )), - ), - } + // ONE AUTHORITY, in the lib. This function used to carry the match itself, and when the + // wire path needed the same decision the copy became a §3 fork -- two places deciding what + // a verdict means, free to drift. The body moved to `cli_run::exit_status_for_class`, where + // it is also REACHABLE BY AN EXECUTING TEST: `rust-unit-tests` runs + // `cargo test -p v1-compiler --lib`, and this file is a BIN target whose tests are compiled + // by clippy and run by nobody. + cli_run::exit_status_for_class(class, function) } #[cfg(test)] From 684c0dd9752bae8097b06aac61d878491b88c40b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 02:22:12 +0000 Subject: [PATCH 04/21] Record the working read surface and state its evidence boundary Receipts for the three executed cases, including the load-bearing one (bytes printed AND a nonzero exit), so the next session does not re-derive them. States the rung honestly rather than implying the e2e is covered: the five cli_wire_outcome tests execute in CI, and the end-to-end runs are a MANUAL receipt. An integration test would live in src/v1/tests/, which clippy compiles and no CI step runs; a .dag witness cannot substitute because scm_log reads a file and the SCM witnesses are SubstrateInputsOnly. So the e2e path is mitigatable and its next-rung trigger is a CI step that runs an integration target -- not another test file. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT --- docs/plans/scm-demo-cli-rebuild.md | 42 +++++++++++++++++++++++++++++- 1 file changed, 41 insertions(+), 1 deletion(-) diff --git a/docs/plans/scm-demo-cli-rebuild.md b/docs/plans/scm-demo-cli-rebuild.md index 87738c17fb7..a28f853e132 100644 --- a/docs/plans/scm-demo-cli-rebuild.md +++ b/docs/plans/scm-demo-cli-rebuild.md @@ -46,7 +46,10 @@ not-`ProcessExit` refusal prints the value, which is not a CLI). So the host binding is REQUIRED, and it is the piece to rebuild: -1. `dag/gunbc/scm/cli.dag` — one entry per verb returning `CliWireResponse`, composing +1. DONE for read verbs. Still to do for WRITE verbs (`init`, `add`, `commit`, `checkout`): + they need `Document` builders, which only log and status have today, and `save_repository` + goes through `Filesystem.Write`, so they are host-effect entries rather than pure reads. + Original note: `dag/gunbc/scm/cli.dag` — one entry per verb returning `CliWireResponse`, composing `load_repository` -> verb -> render, with a `RenderCapability { color: false, tier: Ascii, cursor_addressable: false }` for a plain terminal. Write verbs (`init`, `add`, `commit`, `checkout`) need their own `Document` builders; only log/status have them today. @@ -55,6 +58,43 @@ So the host binding is REQUIRED, and it is the piece to rebuild: refusing on `CliWireUnprintable { cause }`. `serve_wire_fields` / `classify_exit` in `cli_run.rs` are the precedent for reading wire values out of an evaluated `Value`. +## LANDED — the read side reaches an operator + +`dag/gunbc/scm/cli.dag` (`scm_log`, `scm_status`) plus the `run_verb` outcome-seam binding. +Receipts, by execution against `dag/test/fixture/scm_repository_load/empty_repository.json`: + + $ gunbc run --entry dag/gunbc/scm/cli.dag --function scm_log --arg path= + no commits yet + exit 0 + + $ gunbc run --entry dag/gunbc/scm/cli.dag --function scm_status --arg path= + nothing checked out + 0 commits + nothing staged + + $ gunbc run --entry dag/gunbc/scm/cli.dag --function scm_log --arg path=/tmp/no-such-repo + cannot read repository at /tmp/no-such-repo + No such file or directory (os error 2) + repository unavailable + exit 1 + +The third is the load-bearing one: bytes printed AND a nonzero exit, the case an absorbing +implementation turns into silence or a spurious 0. + +### Evidence boundary, stated rather than implied + +Enrolled and executing in CI (`rust-unit-tests`, `cargo test -p v1-compiler --lib`): the five +`cli_wire_outcome_tests` covering the total map — bytes with the response's own exit, a rendered +answer that still fails, a renderer refusal not reading as empty success, the non-wire +fall-through, and the inherited `ExitFailure { code: 0 }` refusal. + +NOT enrolled: the end-to-end runs above are a MANUAL receipt. An integration test that executes +the binary would live in `src/v1/tests/`, which `clippy --all-targets` compiles and no CI step +runs (DESIGN: no CI step executes test targets outside `--lib`). A `.dag` witness cannot stand in +either — `scm_log` reads a file, and the SCM witnesses are `SubstrateInputsOnly`, refusing at the +hermetic boundary. So the class is `mitigatable` on the e2e path and the next-rung trigger is a +CI step that runs an integration target, not another test file. + ## Constraints learned the hard way - A runtime name becomes a `Symbol` via `symbol_intern_lexeme(lexeme: name)` From 6afa0874b5f455b8cfeef524b229e0f1e764a949 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 02:42:52 +0000 Subject: [PATCH 05/21] Make gunbc.scm.cli's own decisions witnessable, and enroll them gunbc.scm.render is already witnessed against PlainTerminal and an ASCII no-colour capability. Nothing held gunbc.scm.cli to passing THOSE: setting color: true on plain_terminal_capability would have turned no claim red, which is the inert-check shape DESIGN calls worse than absent. The composition is split from the read -- scm_log_response / scm_status_response take the read's RESULT and are pure, while scm_log / scm_status supply it from a path. That split is what makes the claims authorable at all: the verbs read a file and this witness family is SubstrateInputsOnly, so a claim can never call them. Five enrolled claims: the unavailable-repository bytes (pinned to the same expected string the render-level witness uses, so an equal answer is evidence the PLAIN target and capability were passed, not merely that something was), its failing exit, the empty-log answer with a succeeding exit, the same for status, and the capability row itself so a reader editing it learns it is a contract. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT --- dag/gunbc/scm/cli.dag | 26 ++++- dag/test/claim/scm/scm_cli_witness_test.dag | 101 ++++++++++++++++++++ 2 files changed, 122 insertions(+), 5 deletions(-) create mode 100644 dag/test/claim/scm/scm_cli_witness_test.dag diff --git a/dag/gunbc/scm/cli.dag b/dag/gunbc/scm/cli.dag index 82f0584be40..45da92e27ee 100644 --- a/dag/gunbc/scm/cli.dag +++ b/dag/gunbc/scm/cli.dag @@ -24,7 +24,9 @@ import std.symbols { Ascii } import extdeps.render.surface { RenderTarget, PlainTerminal } import gunbc.cli_wire { CliWireResponse } import gunbc.scm.authoring { empty_proposal } -import gunbc.scm.read_command { scm_read_log, scm_read_status } +import gunbc.scm.log { CommitLog } +import gunbc.scm.status { RepositoryStatus } +import gunbc.scm.read_command { ScmReadResult, scm_read_log, scm_read_status } import gunbc.scm.render { scm_log_cli_response, scm_status_cli_response } data plain_terminal_capability: RenderCapability = RenderCapability { @@ -35,23 +37,37 @@ data plain_terminal_capability: RenderCapability = RenderCapability { data plain_terminal_target: RenderTarget = PlainTerminal -fn scm_log(path: String) -> CliWireResponse { +// THE COMPOSITION IS SPLIT FROM THE READ so the composition is WITNESSABLE. `scm_log` reads a +// file, and the SCM witnesses are SubstrateInputsOnly -- they refuse at the hermetic boundary -- +// so a claim can never call it. `scm_log_response` takes the read's RESULT and is pure, which +// makes this module's actual decisions (which target, which capability) reachable by a witness +// that constructs a result in substrate. Without the split, changing `plain_terminal_capability` +// to `color: true` would turn nothing red. +fn scm_log_response(result: ScmReadResult) -> CliWireResponse { scm_log_cli_response( - result: scm_read_log(path: path), + result: result, target: plain_terminal_target, capability: plain_terminal_capability ) } +fn scm_log(path: String) -> CliWireResponse { + scm_log_response(result: scm_read_log(path: path)) +} + // STATUS OF A REPOSITORY WITH NOTHING STAGED. `repository_status` needs a pending `Proposal`, // and a CLI reading a repository document has no staging area to read one from -- the document // does not carry what is staged. `empty_proposal()` is therefore the honest argument for this // entry, and it is a REAL limitation rather than a placeholder: a verb that reports staged roles // needs a staging authority to exist first, and none does. -fn scm_status(path: String) -> CliWireResponse { +fn scm_status_response(result: ScmReadResult) -> CliWireResponse { scm_status_cli_response( - result: scm_read_status(path: path, pending: empty_proposal()), + result: result, target: plain_terminal_target, capability: plain_terminal_capability ) } + +fn scm_status(path: String) -> CliWireResponse { + scm_status_response(result: scm_read_status(path: path, pending: empty_proposal())) +} diff --git a/dag/test/claim/scm/scm_cli_witness_test.dag b/dag/test/claim/scm/scm_cli_witness_test.dag new file mode 100644 index 00000000000..62ff145d581 --- /dev/null +++ b/dag/test/claim/scm/scm_cli_witness_test.dag @@ -0,0 +1,101 @@ +module test.claim.scm.scm_cli_witness + +// WHAT THIS MODULE DECIDES, AND THEREFORE WHAT MUST BE HELD TO EXECUTION. +// +// `gunbc.scm.cli` makes exactly two choices the render layer leaves open: which RenderTarget and +// which RenderCapability a terminal invocation gets. `gunbc.scm.render` is already witnessed +// against PlainTerminal and an ASCII no-colour capability by test.claim.scm.scm_render_witness, +// but nothing held gunbc.scm.cli to passing THOSE -- setting `color: true` on +// `plain_terminal_capability` would have turned no claim red. +// +// These claims call the PURE half (`scm_log_response` / `scm_status_response`) rather than the +// path-taking verbs, because the verbs read a file and this witness family is SubstrateInputsOnly: +// a file-reading claim refuses at the hermetic boundary before producing a verdict. +import std.types { String } +import std.symbols { Ascii } +import gunbc.cli_wire { CliWireResponse, CliWirePrintable, CliWireUnprintable } +import std.process { ExitSuccess, ExitFailure } +import std.render { RenderCapability } +import gunbc.scm.read_command { ScmReadAnswered, ScmReadRepositoryUnavailable } +import gunbc.scm.repository_load { RepositoryFileUnreadable } +import gunbc.scm.repository_envelope { empty_repository } +import gunbc.scm.log { repository_log } +import gunbc.scm.status { repository_status } +import gunbc.scm.authoring { empty_proposal } +import gunbc.scm.cli { scm_log_response, scm_status_response, plain_terminal_capability } + +// THE BYTES PIN THE CAPABILITY. This is the same expected string the render-level witness pins for +// PlainTerminal + ASCII no-colour, so an equal answer here is evidence that gunbc.scm.cli passes +// that target and that capability -- not merely that it passes something. A colour-enabled +// capability renders different bytes and turns this red. +test fn cli_log_renders_the_plain_terminal_bytes_for_an_unavailable_repository() -> Bool { + match scm_log_response( + result: ScmReadRepositoryUnavailable { + cause: RepositoryFileUnreadable { path: "repo.json", error: "No such file or directory" }, + } + ) { + CliWireUnprintable { cause: _ } => false + CliWirePrintable { bytes: b, exit: _ } => + b == "cannot read repository at repo.json\n No such file or directory\n" + } +} + +// A REFUSED READ STILL FAILS, through this module's composition and not only the render layer's. +test fn cli_log_exits_failure_for_an_unavailable_repository() -> Bool { + match scm_log_response( + result: ScmReadRepositoryUnavailable { + cause: RepositoryFileUnreadable { path: "repo.json", error: "No such file or directory" }, + } + ) { + CliWireUnprintable { cause: _ } => false + CliWirePrintable { bytes: _, exit: e } => + match e { + ExitSuccess => false + ExitFailure { code: _, reason: _ } => true + } + } +} + +// AN EMPTY REPOSITORY ANSWERED, so it prints and succeeds. The pair with the claim above is the +// distinction a caller needs: "no commits" is not "no repository". +test fn cli_log_answers_and_succeeds_for_an_empty_repository() -> Bool { + match scm_log_response( + result: ScmReadAnswered { path: "repo.json", answer: repository_log(envelope: empty_repository()) } + ) { + CliWireUnprintable { cause: _ } => false + CliWirePrintable { bytes: b, exit: e } => + b == "no commits yet\n" + && match e { + ExitSuccess => true + ExitFailure { code: _, reason: _ } => false + } + } +} + +test fn cli_status_answers_and_succeeds_for_an_empty_repository() -> Bool { + match scm_status_response( + result: ScmReadAnswered { + path: "repo.json", + answer: repository_status(envelope: empty_repository(), pending: empty_proposal()), + } + ) { + CliWireUnprintable { cause: _ } => false + CliWirePrintable { bytes: _, exit: e } => + match e { + ExitSuccess => true + ExitFailure { code: _, reason: _ } => false + } + } +} + +// THE CAPABILITY ROW ITSELF, stated so a change to it is a change to a claim. Bytes already pin it +// indirectly; this says which property is load-bearing and why, so a reader editing the row learns +// it is a contract rather than a default. +test fn the_declared_terminal_capability_is_ascii_without_colour_or_cursor_addressing() -> Bool { + plain_terminal_capability.color == false + && plain_terminal_capability.cursor_addressable == false + && match plain_terminal_capability.tier { + Ascii => true + _ => false + } +} From a345dca473919a847abb9db8d8791fd829aa13d6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 03:42:58 +0000 Subject: [PATCH 06/21] scm init: the first write verb, and a real round trip MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gunbc run --entry dag/gunbc/scm/cli.dag --function scm_init --arg path=/tmp/demo-repo.json initialized repository at /tmp/demo-repo.json rc=0, file created ... --function scm_log --arg path=/tmp/demo-repo.json no commits yet init writes the document, log reads it back. That settles the open question the plan doc recorded: a host WRITE is permitted from gunbc run, so the remaining write verbs are a modeling question rather than a permissions one. render.dag gains the write-answer renderer. A write verb answers with what the write DID, and its four outcomes are not one line with a flag -- each names a different failure and a different next action. RepositoryWriteByteCountUnrepresentable EXITS FAILURE even though bytes reached the disk: a write whose reported size is not a magnitude has not been confirmed, and reporting success for it is the fabricated plausible output §5 forbids. TWO LOSSES NAMED IN THE SOURCE RATHER THAN HIDDEN: - The codec refusal carries a typed RepositoryEncodeRefusal with six arms (uncontained target, root not in store, checkout not in commits, duplicated reference, reference outside allocator, parent not in commits) and this renderer does not decompose it, so an operator learns THAT encoding refused and not WHICH invariant failed. Rendering it needs a per-arm function over ObjectId and RepositoryCommitRef. - init does NOT refuse an existing repository. save_repository writes unconditionally, so init over a populated path overwrites it. Refusing needs a read-before-write that is not expressible as one outcome here. That is why this verb is not offered as a safe default. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT --- dag/gunbc/scm/cli.dag | 26 ++++++++++++++- dag/gunbc/scm/render.dag | 69 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 94 insertions(+), 1 deletion(-) diff --git a/dag/gunbc/scm/cli.dag b/dag/gunbc/scm/cli.dag index 45da92e27ee..0c085854901 100644 --- a/dag/gunbc/scm/cli.dag +++ b/dag/gunbc/scm/cli.dag @@ -24,10 +24,12 @@ import std.symbols { Ascii } import extdeps.render.surface { RenderTarget, PlainTerminal } import gunbc.cli_wire { CliWireResponse } import gunbc.scm.authoring { empty_proposal } +import gunbc.scm.repository_envelope { empty_repository } import gunbc.scm.log { CommitLog } import gunbc.scm.status { RepositoryStatus } import gunbc.scm.read_command { ScmReadResult, scm_read_log, scm_read_status } -import gunbc.scm.render { scm_log_cli_response, scm_status_cli_response } +import gunbc.scm.render { scm_log_cli_response, scm_status_cli_response, scm_save_cli_response } +import gunbc.scm.repository_save { RepositorySave, save_repository } data plain_terminal_capability: RenderCapability = RenderCapability { color: false, @@ -71,3 +73,25 @@ fn scm_status_response(result: ScmReadResult) -> CliWireRespon fn scm_status(path: String) -> CliWireResponse { scm_status_response(result: scm_read_status(path: path, pending: empty_proposal())) } + +// INIT WRITES AN EMPTY REPOSITORY DOCUMENT, and is the first verb here that performs a host +// EFFECT rather than reading one. It is split the same way the read verbs are: `scm_init_response` +// renders an outcome and is witnessable in substrate, while `scm_init` is the effectful half that +// produces one. +// +// IT DOES NOT REFUSE AN EXISTING REPOSITORY, and that is a real gap rather than a decision: +// `save_repository` writes unconditionally, so `init` over a populated path would overwrite it. +// Refusing needs a read-before-write this module cannot express as one outcome -- the honest +// close is a modeled init that loads first and refuses a present document, which is its own +// change and is why this verb is not yet offered as a safe default. +fn scm_init_response(save: RepositorySave) -> CliWireResponse { + scm_save_cli_response( + save: save, + target: plain_terminal_target, + capability: plain_terminal_capability + ) +} + +fn scm_init(path: String) -> CliWireResponse { + scm_init_response(save: save_repository(path: path, repo: empty_repository())) +} diff --git a/dag/gunbc/scm/render.dag b/dag/gunbc/scm/render.dag index a7e64eea42b..43e3222d96a 100644 --- a/dag/gunbc/scm/render.dag +++ b/dag/gunbc/scm/render.dag @@ -49,6 +49,13 @@ import std.render { } import gunbc.scm.read_command { ScmReadResult, ScmReadAnswered, ScmReadRepositoryUnavailable } import gunbc.scm.repository_load { repository_load_refusal_lines } +import gunbc.scm.repository_save { + RepositorySave, + RepositorySaved, + RepositorySaveRefusedByCodec, + RepositoryFileUnwritable, + RepositoryWriteByteCountUnrepresentable +} import gunbc.scm.log { CommitLog, NoCommitsYet, @@ -184,3 +191,65 @@ fn scm_status_cli_response( exit: scm_read_exit(result: result), ) } + +// A WRITE VERB'S ANSWER. The read verbs answer with a document the repository already contains; +// a write verb answers with what the write DID, and its four outcomes are not one line with a +// flag -- each names a different thing that went wrong and a different next action. +// +// WHAT THESE LINES DELIBERATELY DO NOT SAY. The codec refusal carries a typed +// `RepositoryEncodeRefusal` (uncontained target, root not in store, checkout not in commits, +// duplicated reference, reference outside allocator, parent not in commits) and this renderer +// does not decompose it, so the operator learns THAT encoding refused and not WHICH invariant +// failed. That is a real loss and it is named here rather than hidden: rendering it needs a +// per-arm function over ObjectId and RepositoryCommitRef, which is its own change. The byte +// count on the success arm is likewise omitted rather than approximated. +fn repository_save_lines(save: RepositorySave) -> List { + match save { + RepositorySaved { path: p, written: _ } => + [concat("initialized repository at ", p)] + RepositorySaveRefusedByCodec { path: p, cause: _ } => + [ + concat("cannot encode repository for ", p), + " the envelope did not satisfy its own containment invariants" + ] + RepositoryFileUnwritable { path: p, error: e } => + [concat("cannot write repository at ", p), concat(" ", e)] + RepositoryWriteByteCountUnrepresentable { path: p, reported: _ } => + [ + concat("wrote repository at ", p), + " but the host reported a byte count that is not a magnitude" + ] + } +} + +// THE WRITE SUCCEEDED OR IT DID NOT, and the unrepresentable-count arm FAILS even though bytes +// reached the disk: a write whose reported size is not a magnitude has not been confirmed, and +// reporting success for it would be the fabricated-plausible-output §5 forbids. +fn scm_save_exit(save: RepositorySave) -> ProcessExit { + match save { + RepositorySaved { path: _, written: _ } => ExitSuccess + RepositorySaveRefusedByCodec { path: _, cause: _ } => + exit_failure(reason: "repository not encodable") + RepositoryFileUnwritable { path: _, error: _ } => + exit_failure(reason: "repository not writable") + RepositoryWriteByteCountUnrepresentable { path: _, reported: _ } => + exit_failure(reason: "repository write unconfirmed") + } +} + +fn scm_save_document(save: RepositorySave) -> Document { + text_lines_document(lines: repository_save_lines(save: save)) +} + +fn scm_save_cli_response( + save: RepositorySave, + target: RenderTarget, + capability: RenderCapability +) -> CliWireResponse { + cli_wire_response( + doc: scm_save_document(save: save), + target: target, + capability: capability, + exit: scm_save_exit(save: save), + ) +} From 093348be5490c49e27e21cb365410af1eae6cbad Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 03:44:20 +0000 Subject: [PATCH 07/21] Record what add and commit need, including the one design step Settles by execution what was open: a host write IS permitted from gunbc run, content enters via store_node, a Node is built with node_synthetic (the test modules' 'atom' is a LOCAL helper, not an authority), and mint_repository_commit requires store_contains(root), so add must precede commit -- and because identity is content-derived, commit can re-derive an added object's ObjectId by rebuilding the same node. Names the design step rather than sketching it: add composes store_node's 2 arms with save_repository's 4, and commit composes mint's 4 with the same save. A renderer taking two outcome values would encode 'which one failed' positionally and the arms multiply. One modeled ScmWriteOutcome is the increment's real content. I deliberately did not improvise it into cli.dag at the end of a long session, because a write-verb outcome invented at a call site is the anemic modeling this repository keeps paying for. Also records that 'add' has no staging authority to persist to -- repository_status takes pending as a PARAMETER because what is staged is not a fact the document carries -- so a literal stage-now-commit-later add needs a staging authority to exist first. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT --- docs/plans/scm-demo-cli-rebuild.md | 43 ++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/docs/plans/scm-demo-cli-rebuild.md b/docs/plans/scm-demo-cli-rebuild.md index a28f853e132..a9e481bc486 100644 --- a/docs/plans/scm-demo-cli-rebuild.md +++ b/docs/plans/scm-demo-cli-rebuild.md @@ -95,6 +95,49 @@ either — `scm_log` reads a file, and the SCM witnesses are `SubstrateInputsOnl hermetic boundary. So the class is `mitigatable` on the e2e path and the next-rung trigger is a CI step that runs an integration target, not another test file. +## Next increment: `add` and `commit`, and the one design step they need + +Settled by execution, so not open questions any more: + +- **A host WRITE is permitted from `gunbc run`** — `scm_init` created a file. The remaining write + verbs are a modeling question, not a permissions one. +- **Content goes in via `store_node(store, n: Node) -> StoreOutcome`** (`gunbc.scm.object_store`). +- **A Node is built with `node_synthetic`** (`v2.std.node`): + `node_synthetic(kind: TypeNode { connective: Atom { identity: sym } }, children: [])`. The `atom` + helpers in the test modules are LOCAL helpers, not a shared authority — do not import one. +- **A runtime name becomes a Symbol** with `symbol_intern_lexeme(lexeme: name)` + (`v2.std.compilers.lexing`). `name as Symbol` refuses. +- **`mint_repository_commit(repository, root: ObjectId, message, parent: RepositoryCommitRef?)`** + requires `store_contains(root)` — so `add` must precede `commit`, and because identity is derived + from content, `commit` can re-derive an added object's `ObjectId` by rebuilding the same node. + +### The design step, stated so it is not improvised + +`add` composes `store_node` (`Stored | LocatorCollision`) with `save_repository` (4 arms); +`commit` composes `mint_repository_commit` (4 arms) with the same save. A renderer taking two +outcome values is the wrong shape — it would have to encode "which one failed" positionally, and +the arms multiply. + +What is wanted is one modeled write-verb outcome, something like: + + type ScmWriteOutcome + = ScmWriteRepositoryUnavailable { cause: RepositoryLoadRefusal } + | ScmWriteRefusedByStore { collision: StoreOutcome } + | ScmWriteRefusedByMint { refusal: RepositoryCommitMint } + | ScmWritePersisted { save: RepositorySave } + +with one renderer per verb over it. That coproduct is the increment's real content; the wiring +after it is mechanical. It is deliberately NOT sketched into `cli.dag` here, because a write-verb +outcome invented at a call site is the anemic modeling this repository keeps paying for. + +### `add` has no staging authority, and that is not a wiring gap + +`repository_status` takes `pending: Proposal` as a PARAMETER because what is staged is not a fact +the repository document carries. So a literal `git add` — stage now, commit later — has nowhere to +persist to. Either `add` writes an object into the store immediately (content-addressed, no +staging), or a staging authority has to exist first. The first is what the object store supports +today and is the honest reading of `add` for this substrate. + ## Constraints learned the hard way - A runtime name becomes a `Symbol` via `symbol_intern_lexeme(lexeme: name)` From 1efaf10264fb8df4a7eeb5692b421049e5f2f0e9 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 04:19:32 +0000 Subject: [PATCH 08/21] init refuses an occupied path: naming a destructive default did not make it fail-closed MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review 58044 was right and this was the worst thing in the PR. save_repository writes unconditionally -- correctly, it is persistence and not policy -- so a verb offering initialization has to decide for itself whether there is anything at the path it would destroy. The previous revision skipped that decision, called save directly, and NAMED the overwrite in a comment. DESIGN §5's review bar is that a diff landing a non-fail-closed failure arm is a hard reject regardless of what else it delivers; an annotation is not a refusal. gunbc.scm.init owns the decision, because whether there is anything to destroy is a fact about the repository and deciding it in the CLI module would put policy in the realization layer. ScmInitOutcome has three arms and no 'initialized: Bool' beside a save outcome -- a value whose flag disagreed with its shape would have no spelling -- and the two refusals are distinct because the operator's next action differs: a path that already IS a repository is not the same as a path holding someone else's bytes. MEASURED, including the case that proves the destruction is actually closed: fresh path -> initialized repository at /tmp/d2.json same path again -> refusing to initialize /tmp/d2.json a repository is already there, and init would replace its whole history foreign file -> refusing to initialize /tmp/foreign.json a file is already there that is not a repository, and init would destroy it foreign file after-> 'not a repo' (intact -- read back, not assumed) THE RESIDUAL IS STATED IN THE MODULE RATHER THAN IMPLIED. RepositoryFileUnreadable fuses 'absent' with 'present but unreadable' and carries the host's error STRING. This module refuses to branch on that text, because deciding a destructive question by matching an errno spelling is the stringly reasoning the substrate exists to remove. So the proceed arm is 'unreadable', not 'absent'. Closing it needs a modeled path-existence observation distinct from a read failure, which does not exist yet and is the module's next-rung trigger. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT --- dag/gunbc/scm/cli.dag | 25 ++++++---------- dag/gunbc/scm/init.dag | 61 ++++++++++++++++++++++++++++++++++++++++ dag/gunbc/scm/render.dag | 48 +++++++++++++++++++++++++++++++ 3 files changed, 118 insertions(+), 16 deletions(-) create mode 100644 dag/gunbc/scm/init.dag diff --git a/dag/gunbc/scm/cli.dag b/dag/gunbc/scm/cli.dag index 0c085854901..e3b7a344174 100644 --- a/dag/gunbc/scm/cli.dag +++ b/dag/gunbc/scm/cli.dag @@ -28,8 +28,8 @@ import gunbc.scm.repository_envelope { empty_repository } import gunbc.scm.log { CommitLog } import gunbc.scm.status { RepositoryStatus } import gunbc.scm.read_command { ScmReadResult, scm_read_log, scm_read_status } -import gunbc.scm.render { scm_log_cli_response, scm_status_cli_response, scm_save_cli_response } -import gunbc.scm.repository_save { RepositorySave, save_repository } +import gunbc.scm.render { scm_log_cli_response, scm_status_cli_response, scm_init_cli_response } +import gunbc.scm.init { ScmInitOutcome, initialize_repository } data plain_terminal_capability: RenderCapability = RenderCapability { color: false, @@ -74,24 +74,17 @@ fn scm_status(path: String) -> CliWireResponse { scm_status_response(result: scm_read_status(path: path, pending: empty_proposal())) } -// INIT WRITES AN EMPTY REPOSITORY DOCUMENT, and is the first verb here that performs a host -// EFFECT rather than reading one. It is split the same way the read verbs are: `scm_init_response` -// renders an outcome and is witnessable in substrate, while `scm_init` is the effectful half that -// produces one. -// -// IT DOES NOT REFUSE AN EXISTING REPOSITORY, and that is a real gap rather than a decision: -// `save_repository` writes unconditionally, so `init` over a populated path would overwrite it. -// Refusing needs a read-before-write this module cannot express as one outcome -- the honest -// close is a modeled init that loads first and refuses a present document, which is its own -// change and is why this verb is not yet offered as a safe default. -fn scm_init_response(save: RepositorySave) -> CliWireResponse { - scm_save_cli_response( - save: save, +// INIT REFUSES AN OCCUPIED PATH. The decision lives in gunbc.scm.init, not here: whether there is +// anything to destroy is a fact about the repository, and a CLI module deciding it would put policy +// in the realization layer. This module supplies the terminal capability and nothing else. +fn scm_init_response(outcome: ScmInitOutcome) -> CliWireResponse { + scm_init_cli_response( + outcome: outcome, target: plain_terminal_target, capability: plain_terminal_capability ) } fn scm_init(path: String) -> CliWireResponse { - scm_init_response(save: save_repository(path: path, repo: empty_repository())) + scm_init_response(outcome: initialize_repository(path: path)) } diff --git a/dag/gunbc/scm/init.dag b/dag/gunbc/scm/init.dag new file mode 100644 index 00000000000..84284bd0d9b --- /dev/null +++ b/dag/gunbc/scm/init.dag @@ -0,0 +1,61 @@ +module gunbc.scm.init + +// INITIALIZING A REPOSITORY IS A DECISION BEFORE IT IS A WRITE. +// +// `save_repository` writes unconditionally -- correctly, because it is the persistence operation +// and not a policy. So a verb that offers initialization to an operator has to decide, itself, +// whether there is anything at the path it would destroy. An earlier revision skipped that +// decision, called save directly, and NAMED the overwrite in a comment. Naming a destructive +// default does not make it fail-closed: DESIGN §5's review bar is that a diff landing a +// non-fail-closed failure arm is a hard reject regardless of what else it delivers, and an +// annotation is not a refusal. External review was right to block it. +// +// THE DECISION IS THE LOAD. A path that already carries a repository refuses; a path carrying a +// file that is NOT a valid repository also refuses, because an unparseable or rejected document is +// still someone's bytes and overwriting them is the same loss; only a path the host could not read +// at all proceeds to write. +// +// THE RESIDUAL, STATED RATHER THAN IMPLIED. `RepositoryFileUnreadable` fuses "absent" with +// "present but unreadable" -- it carries the host's `error` string and this module refuses to +// branch on that text, because deciding a destructive question by matching an errno spelling is +// exactly the stringly reasoning the substrate exists to remove. So the proceed arm is +// "unreadable", not "absent", and it is narrower than it looks: a file present but unreadable to +// the load is one the subsequent write generally cannot replace either. Closing the residual needs +// a modeled path-existence observation distinct from a read failure, which does not exist yet and +// is this module's next-rung trigger. +import std.types { String } +import gunbc.scm.repository_envelope { RepositoryEnvelope, empty_repository } +import gunbc.scm.repository_load { + RepositoryLoaded, + RepositoryLoadRefused, + RepositoryFileUnreadable, + RepositoryDocumentUnparseable, + RepositoryDocumentRefused, + load_repository +} +import gunbc.scm.repository_save { RepositorySave, save_repository } + +// THE ARMS ARE THE ANSWER. There is no `initialized: Bool` beside a save outcome: a value whose +// flag disagreed with its shape would have a spelling, and the two refusals are distinguished +// because an operator's next action differs -- one path already IS a repository, the other holds +// something else that would be destroyed. +type ScmInitOutcome + = ScmInitialized { save: RepositorySave } + | ScmInitRefusedRepositoryPresent { path: String } + | ScmInitRefusedForeignFilePresent { path: String } + +fn initialize_repository(path: String) -> ScmInitOutcome { + match load_repository(path: path) { + RepositoryLoaded { path: p, envelope: _ } => + ScmInitRefusedRepositoryPresent { path: p } + RepositoryLoadRefused { cause: cause } => + match cause { + RepositoryFileUnreadable { path: _, error: _ } => + ScmInitialized { save: save_repository(path: path, repo: empty_repository()) } + RepositoryDocumentUnparseable { path: p, gap: _ } => + ScmInitRefusedForeignFilePresent { path: p } + RepositoryDocumentRefused { path: p, cause: _ } => + ScmInitRefusedForeignFilePresent { path: p } + } + } +} diff --git a/dag/gunbc/scm/render.dag b/dag/gunbc/scm/render.dag index 43e3222d96a..bbab7bdff69 100644 --- a/dag/gunbc/scm/render.dag +++ b/dag/gunbc/scm/render.dag @@ -49,6 +49,12 @@ import std.render { } import gunbc.scm.read_command { ScmReadResult, ScmReadAnswered, ScmReadRepositoryUnavailable } import gunbc.scm.repository_load { repository_load_refusal_lines } +import gunbc.scm.init { + ScmInitOutcome, + ScmInitialized, + ScmInitRefusedRepositoryPresent, + ScmInitRefusedForeignFilePresent +} import gunbc.scm.repository_save { RepositorySave, RepositorySaved, @@ -253,3 +259,45 @@ fn scm_save_cli_response( exit: scm_save_exit(save: save), ) } + +// A REFUSED INIT PRINTS WHY AND EXITS FAILURE. The two refusals render differently because the +// operator's next action differs: an existing repository is not a mistake to correct, while a +// foreign file at that path is a choice about someone else's bytes. +fn scm_init_lines(outcome: ScmInitOutcome) -> List { + match outcome { + ScmInitialized { save: save } => repository_save_lines(save: save) + ScmInitRefusedRepositoryPresent { path: p } => + [ + concat("refusing to initialize ", p), + " a repository is already there, and init would replace its whole history" + ] + ScmInitRefusedForeignFilePresent { path: p } => + [ + concat("refusing to initialize ", p), + " a file is already there that is not a repository, and init would destroy it" + ] + } +} + +fn scm_init_exit(outcome: ScmInitOutcome) -> ProcessExit { + match outcome { + ScmInitialized { save: save } => scm_save_exit(save: save) + ScmInitRefusedRepositoryPresent { path: _ } => + exit_failure(reason: "repository already present") + ScmInitRefusedForeignFilePresent { path: _ } => + exit_failure(reason: "path occupied by a non-repository file") + } +} + +fn scm_init_cli_response( + outcome: ScmInitOutcome, + target: RenderTarget, + capability: RenderCapability +) -> CliWireResponse { + cli_wire_response( + doc: text_lines_document(lines: scm_init_lines(outcome: outcome)), + target: target, + capability: capability, + exit: scm_init_exit(outcome: outcome), + ) +} From 025920579d168c85b2f22e77c2842dcb1c3cd835 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 1 Sep 2026 04:57:20 +0000 Subject: [PATCH 09/21] Make scm init proceed only from an established absence, and receipt the wire host Rust Three blocking findings from review 58060 on #9864. 1. `init` was fail-open on `RepositoryFileUnreadable`. Proceeding there is a guess about the host's permission model, not an observation -- a file can be unreadable and perfectly truncatable, so the proceed arm could destroy the bytes it existed to protect. The residual was NAMED in the module header, and a named residual does not refuse. `initialize_repository` now takes a DIRECTORY and a NAME and routes through `extdeps.filesystem.filesystem_io` `filesystem_file_observation`: absence is established from a listing that succeeded and did not name the entry, and only that arm reaches `save_repository`. Present bytes are classified (repository vs foreign) for the operator's benefit but both refuse; indeterminate and disagree refuse as `ScmInitRefusedPathUnobserved`, carrying the host's cause. Executed, four cases: fresh directory writes 166 bytes; an existing repository refuses; a foreign file refuses and reads back byte-intact; a directory with mode 000 refuses naming `Permission denied (os error 13)` rather than widening to "nothing is there". Three hermetic claims enrolled beside them in test.claim.scm.scm_cli_witness -- no refusal renders as a success exit, the three refusals render differently, and the unobserved arm names what could not be observed. 2. The hand-authored Rust had no seed-growth receipt. `gunbc.cli_wire_host_admission` enumerates all 11 declarations at identity grain, states why the host process and the interpreter Value both lack a .dag denotation today, records that `exit_status_for_class` is a relocation rather than new behaviour, and names two capability-grain triggers. It does NOT admit the growth; the disposition is Terminal and fails closed without an operator ruling. Wired into `gunbc.seed_growth_admission`. 3. `gunbc.cli_dispatch_surface` still asserted there is NO route a user can invoke for the scm family, which this branch made false. The row now names the real route and says what changed, and its stage0 mirror is regenerated from the emitter (the candidate tree differed from the committed mirror by exactly this one string). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Wy8wRfzTK2kvFzj9nAEbyT --- dag/gunbc/cli_dispatch_surface.dag | 2 +- dag/gunbc/cli_wire_host_admission.dag | 93 ++++++++++++++ dag/gunbc/scm/cli.dag | 4 +- dag/gunbc/scm/init.dag | 114 ++++++++++++------ dag/gunbc/scm/render.dag | 10 +- dag/gunbc/seed_growth_admission.dag | 4 +- dag/test/claim/scm/scm_cli_witness_test.dag | 63 +++++++++- docs/plans/scm-demo-cli-rebuild.md | 40 ++++++ .../stage0/src/gunbc_cli_dispatch_surface.rs | 2 +- 9 files changed, 290 insertions(+), 42 deletions(-) create mode 100644 dag/gunbc/cli_wire_host_admission.dag diff --git a/dag/gunbc/cli_dispatch_surface.dag b/dag/gunbc/cli_dispatch_surface.dag index 2b318fc7bcb..84530ef1758 100644 --- a/dag/gunbc/cli_dispatch_surface.dag +++ b/dag/gunbc/cli_dispatch_surface.dag @@ -396,7 +396,7 @@ fn gunbc_cli_subcommands() -> List { } ], realization: CliRefusesUnwired { - successor: "unwired: gunbc.cli_wire CliWireResponse has no host renderer bound. MEASURED, not assumed -- `gunbc run --entry dag/gunbc/scm/read_command.dag --function scm_read_log --arg path=

` binds its argument and READS THE FILE, then the host refuses with `returned ScmReadResult, not ProcessExit`, so the answer is computed and discarded. There is therefore NO route a user can invoke today that yields this answer, and naming one would be a dead end dressed as a redirect." + successor: "unwired AS A SUBCOMMAND -- `gunbc scm log` does not exist -- but the answer is now REACHABLE, and this row said it was not. The successor is `gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/scm/cli.dag --function scm_log --arg path=

`, which prints the rendered answer and exits on the exit the response itself carries. What changed: gunbc.cli_wire CliWireResponse gained a host binding in run_verb (cli_run classify_cli_wire + cli_wire_outcome), so a wire-returning entry is no longer refused with `returned ScmReadResult, not ProcessExit` and its answer is no longer computed and discarded. The earlier text -- `there is NO route a user can invoke today` -- was true when written and this row is the authority that has to stop saying it, because a surface that keeps asserting an absence the host has since filled is a §3 fork between the model and the thing it models. scm_status and scm_init are reachable by the same route; scm_init REFUSES an occupied path (gunbc.scm.init)." }, emission: AbsentFromEmitMainRs }, diff --git a/dag/gunbc/cli_wire_host_admission.dag b/dag/gunbc/cli_wire_host_admission.dag new file mode 100644 index 00000000000..df4f909925a --- /dev/null +++ b/dag/gunbc/cli_wire_host_admission.dag @@ -0,0 +1,93 @@ +module gunbc.cli_wire_host_admission + +import gunbc.roadmap_model { RoadmapNodeId } +import gunbc.seed_growth { SeedGrowthJustification } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import std.disposition { Disposition, Terminal } +import std.types { String } +import v2.std.collection { List } + +data cli_wire_host_receipt_disposition: Disposition = Terminal { + reason: "Single authority for the SEED-GROWTH RECEIPT owed by the host renderer that carries a modeled CliWireResponse to a process's stdout and exit status. It declares WHICH hand-authored Rust declarations that change adds to the seed, why they exist, and what retires them. It does NOT admit them: the realization disposition is an operator judgment and fails closed in its absence, because a receipt that also granted its own admission would be the self-authorized dissolution failure DESIGN names. Terminal because the RECEIPT is permanent -- it outlives the code it describes, recording what was owed and on what trigger it was discharged." +} + +// WHAT THIS GROWTH BOUGHT, STATED AS THE DEFECT IT REMOVED RATHER THAN AS A FEATURE. +// +// gunbc.cli_dispatch_surface already carried a row saying the scm family REFUSES UNWIRED: the +// modeled command surface computed an answer and no route existed to deliver it. So every scm +// entry was a value the host discarded -- specification without execution, DESIGN section 5's +// deepest trap, and flagged by the compiler's OWN surface model rather than discovered by review. +// The three declarations below are the route: classify a returned value as a CliWireResponse or +// refuse to call it one, decide what the host must DO about it, and exit accordingly. +// +// WHY THE CLASSIFIER CANNOT BE MODELED AWAY TODAY. It reads an interpreter Value -- a host runtime +// representation with no .dag denotation -- and asks whether it inhabits a declared coproduct. The +// answer is a fact about the modeled type, but the SUBJECT is a seed data structure, so the fold +// has to live where that structure lives. That is the same boundary every other value-projecting +// item in this roster sits on, not new debt of its own kind. + +data cli_wire_host_relocation_note: String = "exit_status_for_class IS NOT NEW BEHAVIOUR AND SAYING SO IS PART OF THE RECEIPT. Its body was MOVED out of main.rs's exit_status_for, which now delegates to it. It is enumerated below because it is a hand-authored declaration that did not exist before at that name and in that module, and netting a relocation against an addition is exactly the arithmetic gunbc.seed_growth_admission refuses -- but a reader counting behaviour rather than declarations should know that the process-exit path gained nothing here and was only made callable from the wire path beside it." + +data cli_wire_host_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { + hand_authored_declarations: [ + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "CliWireClass", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "classify_cli_wire", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "CliWireOutcome", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "cli_wire_outcome", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "exit_status_for_class", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "cli_wire_outcome_tests", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run.cli_wire_outcome_tests", + decl_name: "a_printable_response_writes_its_bytes_and_honors_its_own_exit", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run.cli_wire_outcome_tests", + decl_name: "a_printable_response_can_carry_a_failing_exit", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run.cli_wire_outcome_tests", + decl_name: "an_unprintable_response_refuses_rather_than_printing_nothing", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run.cli_wire_outcome_tests", + decl_name: "a_non_wire_value_yields_no_outcome_so_the_process_exit_path_is_untouched", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run.cli_wire_outcome_tests", + decl_name: "an_exit_failure_with_code_zero_is_refused_on_the_wire_path_too", + field: WholeDeclaration + } + ], + reason: "WHY RUST IS STILL NEEDED HERE: the subject is the HOST PROCESS -- stdout bytes and an exit status -- and it is reached from a returned interpreter Value. Neither end has a .dag denotation today: there is no modeled carrier for a running process's standard output, and no modeled projection of the interpreter's own Value representation, so the fold between them cannot be written in the substrate it is bridging into. This is a boundary item, not seed-shrink debt.\n\nWHAT IT REMOVED: gunbc.cli_dispatch_surface's scm row carried CliRefusesUnwired -- the compiler's own dispatch model recording that the scm command family computed answers no user could invoke. Every modeled scm entry was therefore specification without execution. With this route bound, gunbc scm log, status and init reach an operator, which is the only reason the .dag side of this change is worth anything.\n\nHAND-ITEM DELTA: +11 FROM THE MERGE BASE, ENUMERATED ABOVE -- five production declarations (CliWireClass, classify_cli_wire, CliWireOutcome, cli_wire_outcome, exit_status_for_class) and six test items (one test module and its five fns). Reproducible from the merge base, never the moving tip: git diff $(git merge-base main HEAD)...HEAD -- src/v1/stage0/src/cli_run.rs src/v1/stage0/src/main.rs, which reports 255 insertions in cli_run.rs and 54 insertions with 30 deletions in main.rs, and no other .rs file on this branch differs. One of the five, exit_status_for_class, is a RELOCATION rather than new behaviour -- see cli_wire_host_relocation_note.\n\nWHY THE CLASSIFIER AND THE OUTCOME ARE TWO ITEMS: the classification is a question about a value and the outcome is a decision about a process, and fusing them would have put the write-or-refuse decision inside a match arm in main.rs where no test could reach it. Splitting them is what made the five-case matrix authorable, including the two cases that carry the actual safety content -- an unprintable response REFUSES rather than printing nothing, and an exit_failure carrying status zero is refused on the wire path exactly as it already was on the process-exit path.", + owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, + trigger: "Delete CliWireClass, classify_cli_wire and their tests when the interpreter publishes a modeled projection of a returned Value against a declared type -- an inhabitance decision the substrate answers, rather than a hand-written field-by-field match on the host Value representation. Delete CliWireOutcome, cli_wire_outcome, exit_status_for_class and their tests when std models a process's standard output and exit status as a carrier the .dag side can produce directly, so a command entry returns the whole host effect and the seed only executes it. Both triggers name a CAPABILITY the substrate does not have today; neither is discharged by any artifact short of it, and in particular neither is discharged by moving this Rust to another file.", + current_boundary: "gunbc.cli_wire_host_admission -> v1_compiler.cli_run cli_wire_outcome -> v1_compiler.main run_verb -> the host process stdout and exit status" +} diff --git a/dag/gunbc/scm/cli.dag b/dag/gunbc/scm/cli.dag index e3b7a344174..6a2fa1c07b1 100644 --- a/dag/gunbc/scm/cli.dag +++ b/dag/gunbc/scm/cli.dag @@ -85,6 +85,6 @@ fn scm_init_response(outcome: ScmInitOutcome) -> CliWireResponse { ) } -fn scm_init(path: String) -> CliWireResponse { - scm_init_response(outcome: initialize_repository(path: path)) +fn scm_init(directory: String, name: String) -> CliWireResponse { + scm_init_response(outcome: initialize_repository(directory: directory, name: name)) } diff --git a/dag/gunbc/scm/init.dag b/dag/gunbc/scm/init.dag index 84284bd0d9b..3df89785e02 100644 --- a/dag/gunbc/scm/init.dag +++ b/dag/gunbc/scm/init.dag @@ -10,52 +10,96 @@ module gunbc.scm.init // non-fail-closed failure arm is a hard reject regardless of what else it delivers, and an // annotation is not a refusal. External review was right to block it. // -// THE DECISION IS THE LOAD. A path that already carries a repository refuses; a path carrying a -// file that is NOT a valid repository also refuses, because an unparseable or rejected document is -// still someone's bytes and overwriting them is the same loss; only a path the host could not read -// at all proceeds to write. +// AND THE SECOND REVISION WAS STILL FAIL-OPEN, WHICH IS WHY THIS ONE DOES NOT READ FIRST. It +// proceeded on `RepositoryFileUnreadable`, reasoning that a file it could not read was one the +// write could not replace either. That reasoning is a guess about the host's permission model, not +// an observation: a file can be unreadable and perfectly truncatable, so the proceed arm could +// destroy exactly the bytes it was meant to protect. The residual was NAMED in this module's +// header and named residuals do not refuse. Review 58060 on gunbc#9864 blocked it. // -// THE RESIDUAL, STATED RATHER THAN IMPLIED. `RepositoryFileUnreadable` fuses "absent" with -// "present but unreadable" -- it carries the host's `error` string and this module refuses to -// branch on that text, because deciding a destructive question by matching an errno spelling is -// exactly the stringly reasoning the substrate exists to remove. So the proceed arm is -// "unreadable", not "absent", and it is narrower than it looks: a file present but unreadable to -// the load is one the subsequent write generally cannot replace either. Closing the residual needs -// a modeled path-existence observation distinct from a read failure, which does not exist yet and -// is this module's next-rung trigger. +// THE FIX IS NOT A BETTER READ, IT IS A DIFFERENT OBSERVATION. `Filesystem.Read`'s success channel +// cannot separate absent from unreadable -- that is the conflation `extdeps.filesystem.filesystem_io` +// exists to remove -- so absence is established from a LISTING that succeeded and did not name the +// entry, and the read is consulted only as the second half of `filesystem_file_observation`'s fold. +// The four arms are the four actions: nothing is there, so write; bytes are there, so refuse and say +// which kind; the observation could not be made, so refuse; the two observations disagree, so refuse. +// Only the first arm reaches `save_repository`. +// +// THIS IS WHY THE ENTRY TAKES A DIRECTORY AND A NAME RATHER THAN A PATH. Presence is a fact about a +// directory listing, so the listing's subject has to be an argument and not something recovered by +// splitting a string. A path parser here would be a second, positional naming scheme for what the +// caller already knows, and its failure mode is silent: a caller that passed a bare filename would +// get a listing of the wrong directory and an absence established about it. import std.types { String } -import gunbc.scm.repository_envelope { RepositoryEnvelope, empty_repository } -import gunbc.scm.repository_load { - RepositoryLoaded, - RepositoryLoadRefused, - RepositoryFileUnreadable, - RepositoryDocumentUnparseable, - RepositoryDocumentRefused, - load_repository +import extdeps.filesystem.filesystem_io { + Filesystem, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + filesystem_listing_observation, + filesystem_read_outcome, + filesystem_file_observation +} +import extdeps.languages.json.parse { + parse_json_document, + JsonDocumentParsed, + JsonDocumentUnreadable +} +import gunbc.scm.repository_envelope { + empty_repository, + decode_repository, + RepositoryDecoded, + RepositoryDecodeRefused } import gunbc.scm.repository_save { RepositorySave, save_repository } // THE ARMS ARE THE ANSWER. There is no `initialized: Bool` beside a save outcome: a value whose -// flag disagreed with its shape would have a spelling, and the two refusals are distinguished -// because an operator's next action differs -- one path already IS a repository, the other holds -// something else that would be destroyed. +// flag disagreed with its shape would have a spelling, and the refusals are distinguished because +// an operator's next action differs -- one path already IS a repository, one holds something else +// that would be destroyed, and one could not be observed at all, which is a fault to investigate +// rather than a state of the path. type ScmInitOutcome = ScmInitialized { save: RepositorySave } | ScmInitRefusedRepositoryPresent { path: String } | ScmInitRefusedForeignFilePresent { path: String } + | ScmInitRefusedPathUnobserved { path: String, cause: String } -fn initialize_repository(path: String) -> ScmInitOutcome { - match load_repository(path: path) { - RepositoryLoaded { path: p, envelope: _ } => - ScmInitRefusedRepositoryPresent { path: p } - RepositoryLoadRefused { cause: cause } => - match cause { - RepositoryFileUnreadable { path: _, error: _ } => - ScmInitialized { save: save_repository(path: path, repo: empty_repository()) } - RepositoryDocumentUnparseable { path: p, gap: _ } => - ScmInitRefusedForeignFilePresent { path: p } - RepositoryDocumentRefused { path: p, cause: _ } => - ScmInitRefusedForeignFilePresent { path: p } +// PRESENT BYTES ARE CLASSIFIED, NEVER TRUSTED. Both present arms refuse, so this classification +// changes only what the operator is told -- which is the whole difference between "your repository +// is already here" and "something else is here and I will not touch it". +fn init_present_refusal(path: String, content: String) -> ScmInitOutcome { + match parse_json_document(s: content) { + JsonDocumentUnreadable { gap: _ } => ScmInitRefusedForeignFilePresent { path: path } + JsonDocumentParsed { value: v } => + match decode_repository(v: v) { + RepositoryDecoded { envelope: _ } => ScmInitRefusedRepositoryPresent { path: path } + RepositoryDecodeRefused { cause: _ } => ScmInitRefusedForeignFilePresent { path: path } } } } + +fn initialize_repository(directory: String, name: String) -> ScmInitOutcome { + let path = join([directory, "/", name], "") + let listed = Filesystem.List(path: directory) + let read = Filesystem.Read(path: path) + match filesystem_file_observation( + listing: filesystem_listing_observation( + directory: directory, + success: listed.success, + entries: listed.entries, + error: listed.error + ), + name: name, + path: path, + read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error) + ) { + FilesystemFileAbsent(_) => + ScmInitialized { save: save_repository(path: path, repo: empty_repository()) } + FilesystemFileRead { path: p, content: c } => init_present_refusal(path: p, content: c) + FilesystemFileIndeterminate { cause: c } => + ScmInitRefusedPathUnobserved { path: path, cause: c } + FilesystemFileObservationsDisagree { path: p, cause: c } => + ScmInitRefusedPathUnobserved { path: p, cause: c } + } +} diff --git a/dag/gunbc/scm/render.dag b/dag/gunbc/scm/render.dag index bbab7bdff69..097e8667e78 100644 --- a/dag/gunbc/scm/render.dag +++ b/dag/gunbc/scm/render.dag @@ -53,7 +53,8 @@ import gunbc.scm.init { ScmInitOutcome, ScmInitialized, ScmInitRefusedRepositoryPresent, - ScmInitRefusedForeignFilePresent + ScmInitRefusedForeignFilePresent, + ScmInitRefusedPathUnobserved } import gunbc.scm.repository_save { RepositorySave, @@ -276,6 +277,11 @@ fn scm_init_lines(outcome: ScmInitOutcome) -> List { concat("refusing to initialize ", p), " a file is already there that is not a repository, and init would destroy it" ] + ScmInitRefusedPathUnobserved { path: p, cause: c } => + [ + concat("refusing to initialize ", p), + concat(" the path could not be observed, so nothing about it is established -- ", c) + ] } } @@ -286,6 +292,8 @@ fn scm_init_exit(outcome: ScmInitOutcome) -> ProcessExit { exit_failure(reason: "repository already present") ScmInitRefusedForeignFilePresent { path: _ } => exit_failure(reason: "path occupied by a non-repository file") + ScmInitRefusedPathUnobserved { path: _, cause: _ } => + exit_failure(reason: "path could not be observed") } } diff --git a/dag/gunbc/seed_growth_admission.dag b/dag/gunbc/seed_growth_admission.dag index 662ed1b2562..a89f4d2b28e 100644 --- a/dag/gunbc/seed_growth_admission.dag +++ b/dag/gunbc/seed_growth_admission.dag @@ -42,6 +42,7 @@ import gunbc.capability_origin { origin_refusals } import gunbc.rust_item_identity { RustItemIdentity, rust_item_identity_key } +import gunbc.cli_wire_host_admission { cli_wire_host_seed_growth_justification } import gunbc.seed_growth { SeedGrowthJustification } import gunbc.stage0_rust_host_observation { stage0_rust_observation_seed_growth_justification } import gunbc.floor_non_verdict_enrollment { floor_non_verdict_seed_growth_justification } @@ -211,7 +212,8 @@ fn seed_growth_justification_roster() -> List { target_invocation_seed_growth_justification, generated_artifact_boundary_seed_growth_justification, regen_convergence_seed_growth_justification, - decl_facts_shared_memo_seed_growth_justification + decl_facts_shared_memo_seed_growth_justification, + cli_wire_host_seed_growth_justification ] } diff --git a/dag/test/claim/scm/scm_cli_witness_test.dag b/dag/test/claim/scm/scm_cli_witness_test.dag index 62ff145d581..de4226357fc 100644 --- a/dag/test/claim/scm/scm_cli_witness_test.dag +++ b/dag/test/claim/scm/scm_cli_witness_test.dag @@ -22,7 +22,12 @@ import gunbc.scm.repository_envelope { empty_repository } import gunbc.scm.log { repository_log } import gunbc.scm.status { repository_status } import gunbc.scm.authoring { empty_proposal } -import gunbc.scm.cli { scm_log_response, scm_status_response, plain_terminal_capability } +import gunbc.scm.cli { scm_log_response, scm_status_response, scm_init_response, plain_terminal_capability } +import gunbc.scm.init { + ScmInitRefusedRepositoryPresent, + ScmInitRefusedForeignFilePresent, + ScmInitRefusedPathUnobserved +} // THE BYTES PIN THE CAPABILITY. This is the same expected string the render-level witness pins for // PlainTerminal + ASCII no-colour, so an equal answer here is evidence that gunbc.scm.cli passes @@ -99,3 +104,59 @@ test fn the_declared_terminal_capability_is_ascii_without_colour_or_cursor_addre _ => false } } + +// PROJECTIONS OVER THE WIRE RESPONSE, SHARED BY THE INIT CLAIMS BELOW so that neither of them +// carries its own copy of the same two-arm match. +fn wire_refuses(r: CliWireResponse) -> Bool { + match r { + CliWireUnprintable { cause: _ } => true + CliWirePrintable { bytes: _, exit: e } => + match e { + ExitSuccess => false + ExitFailure { code: _, reason: _ } => true + } + } +} + +fn wire_bytes(r: CliWireResponse) -> String { + match r { + CliWireUnprintable { cause: _ } => "" + CliWirePrintable { bytes: b, exit: _ } => b + } +} + +// EVERY NON-ABSENT OBSERVATION REFUSES, AND THE THREE REFUSALS ARE DISTINGUISHABLE. +// +// `initialize_repository` itself takes a directory listing and a read, so it is not hermetic and is +// witnessed by the execution matrix in docs/plans/scm-demo-cli-rebuild.md. What IS decidable here is +// the half that turns an outcome into an operator's answer: that no refusal arm can render as a +// success, and that the three say different things. A change that made the unobserved arm print the +// foreign-file line -- telling an operator their bytes are being protected when in fact nothing was +// observed -- would turn these red. +test fn an_init_refusal_never_exits_success() -> Bool { + wire_refuses(r: scm_init_response(outcome: ScmInitRefusedRepositoryPresent { path: "repo.json" })) + && wire_refuses(r: scm_init_response(outcome: ScmInitRefusedForeignFilePresent { path: "repo.json" })) + && wire_refuses(r: scm_init_response( + outcome: ScmInitRefusedPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } + )) +} + +test fn the_three_init_refusals_render_differently() -> Bool { + let present = wire_bytes(r: scm_init_response(outcome: ScmInitRefusedRepositoryPresent { path: "repo.json" })) + let foreign = wire_bytes(r: scm_init_response(outcome: ScmInitRefusedForeignFilePresent { path: "repo.json" })) + let unobserved = wire_bytes(r: scm_init_response( + outcome: ScmInitRefusedPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } + )) + present != foreign && foreign != unobserved && present != unobserved && present != "" +} + +// THE UNOBSERVED ARM CARRIES THE HOST'S CAUSE THROUGH. A refusal that dropped it would tell the +// operator to investigate without saying what could not be observed. +test fn the_unobserved_refusal_names_what_could_not_be_observed() -> Bool { + match scm_init_response( + outcome: ScmInitRefusedPathUnobserved { path: "repo.json", cause: "Permission denied" } + ) { + CliWireUnprintable { cause: _ } => false + CliWirePrintable { bytes: b, exit: _ } => b.contains("Permission denied") && b.contains("repo.json") + } +} diff --git a/docs/plans/scm-demo-cli-rebuild.md b/docs/plans/scm-demo-cli-rebuild.md index a9e481bc486..131f2797a21 100644 --- a/docs/plans/scm-demo-cli-rebuild.md +++ b/docs/plans/scm-demo-cli-rebuild.md @@ -81,6 +81,46 @@ Receipts, by execution against `dag/test/fixture/scm_repository_load/empty_repos The third is the load-bearing one: bytes printed AND a nonzero exit, the case an absorbing implementation turns into silence or a spurious 0. +### `init` — the write verb, and the four observations it distinguishes + +`scm_init` takes a DIRECTORY and a NAME rather than a path, because presence is a fact about a +directory listing and recovering the directory by splitting a string would be a second, positional +naming scheme for something the caller already knows. It routes through +`extdeps.filesystem.filesystem_io` `filesystem_file_observation`, so absence is established from a +listing that succeeded and did not name the entry — never from a failed read, whose success channel +cannot separate absent from unreadable. Only the established-absence arm reaches `save_repository`. + +Two earlier revisions were fail-open and both were caught by external review before merge: the first +called `save_repository` unconditionally and NAMED the overwrite in a comment; the second proceeded +on `RepositoryFileUnreadable`, which is a guess about the host's permission model — a file can be +unreadable and perfectly truncatable — and again named the residual instead of refusing it +(review 58060 on gunbc#9864). + +Receipts, one per arm, `gunbc run --entry dag/gunbc/scm/cli.dag --function scm_init --arg +directory= --arg name=repo.json`: + + fresh directory [file] list … / [file] read … / [file] write …/repo.json (166 bytes) + initialized repository at /tmp/scminit/fresh/repo.json + + repository present refusing to initialize /tmp/scminit/existing/repo.json + a repository is already there, and init would replace its whole history + + foreign file present refusing to initialize /tmp/scminit/foreign/repo.json + a file is already there that is not a repository, and init would destroy it + and the file read back afterwards still holds its original bytes + + directory unlistable refusing to initialize /tmp/scminit/nodir/repo.json + the path could not be observed, so nothing about it is established -- + the directory /tmp/scminit/nodir could not be listed, so the absence of + repo.json is not established -- Permission denied (os error 13) + +The fourth is the load-bearing one: an observation that could not be made refuses rather than +widening to "nothing is there", which is the absorbing fallback DESIGN §5 names. + +Hermetically enrolled beside them, in `test.claim.scm.scm_cli_witness`: no init refusal renders as a +success exit, the three refusals render differently, and the unobserved arm carries the host's cause +through. The absent arm itself takes a listing and a read, so it stays on the manual receipt above. + ### Evidence boundary, stated rather than implied Enrolled and executing in CI (`rust-unit-tests`, `cargo test -p v1-compiler --lib`): the five diff --git a/src/v1/stage0/src/gunbc_cli_dispatch_surface.rs b/src/v1/stage0/src/gunbc_cli_dispatch_surface.rs index a058d2977a3..600e82b2e75 100644 --- a/src/v1/stage0/src/gunbc_cli_dispatch_surface.rs +++ b/src/v1/stage0/src/gunbc_cli_dispatch_surface.rs @@ -327,7 +327,7 @@ pub fn gunbc_cli_subcommands() -> Rc>> { emission: CliSurfaceEmission::AbsentFromEmitMainRs, })]), realization: Rc::new(CliArmRealization::CliRefusesUnwired { - successor: "unwired: gunbc.cli_wire CliWireResponse has no host renderer bound. MEASURED, not assumed -- `gunbc run --entry dag/gunbc/scm/read_command.dag --function scm_read_log --arg path=

` binds its argument and READS THE FILE, then the host refuses with `returned ScmReadResult, not ProcessExit`, so the answer is computed and discarded. There is therefore NO route a user can invoke today that yields this answer, and naming one would be a dead end dressed as a redirect.".to_string(), + successor: "unwired AS A SUBCOMMAND -- `gunbc scm log` does not exist -- but the answer is now REACHABLE, and this row said it was not. The successor is `gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/scm/cli.dag --function scm_log --arg path=

`, which prints the rendered answer and exits on the exit the response itself carries. What changed: gunbc.cli_wire CliWireResponse gained a host binding in run_verb (cli_run classify_cli_wire + cli_wire_outcome), so a wire-returning entry is no longer refused with `returned ScmReadResult, not ProcessExit` and its answer is no longer computed and discarded. The earlier text -- `there is NO route a user can invoke today` -- was true when written and this row is the authority that has to stop saying it, because a surface that keeps asserting an absence the host has since filled is a §3 fork between the model and the thing it models. scm_status and scm_init are reachable by the same route; scm_init REFUSES an occupied path (gunbc.scm.init).".to_string(), }), emission: CliSurfaceEmission::AbsentFromEmitMainRs, }), Rc::new(CliSubcommandRow { From 76f05514ea367baaead32d19b64ddf1fb3e80fb9 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 04:32:32 +0000 Subject: [PATCH 10/21] Regenerate the Rust source-type bindings from their authority main carries an updated `proof` row in gunbc.rust_source_type_bindings whose committed projection was never regenerated, so origin/main is itself in a drifted state and every branch that merges it inherits a failing regen phase. Measured here rather than assumed: both the .dag authority and the .rs projection on this branch are byte-identical to origin/main, and regen still reports first_generation_equal=false for this one file. The fix is the projection, not the authority: the generated file now carries what the row says. The build lane is green at this head -- regen first_generation_equal=true, generated-artifact 35/35 matched, 0 drifted. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- src/v1/stage0/src/gunbc_rust_source_type_bindings.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v1/stage0/src/gunbc_rust_source_type_bindings.rs b/src/v1/stage0/src/gunbc_rust_source_type_bindings.rs index 0b07b3f3951..29b2f2b2d38 100644 --- a/src/v1/stage0/src/gunbc_rust_source_type_bindings.rs +++ b/src/v1/stage0/src/gunbc_rust_source_type_bindings.rs @@ -62,7 +62,7 @@ pub fn checkpoint_row_migration_rows() -> Rc>> { }), Rc::new(CheckpointRowMigration { dag_name: "String".to_string(), disposition: Rc::new(CheckpointRowDisposition::ProvenUniqueKernelBinding { - proof: "The kernel string_type is minted by v1.compiler.types for every string literal and carries no declaration; both .dag declarations of the spelling (v2.std.text, std.string_type) are gated structural by v1.compiler.coercion structural_declaration_modules_for and never reach this row. THE VERDICT STANDS AND ITS ORIGINAL ARGUMENT WAS EXACTLY INVERTED, corrected here rather than softened because the inverted form would justify the wrong things if reused. It read: the bare spelling cannot be captured because the only import that could shadow it binds the SAME token, so in a module importing v2.std.text String every `String` reference IS the text carrier and the kernel spelling is unreachable there. The opposite is true. KERNEL NAMES ARE NEVER OVERRIDDEN BY IMPORTS (v1.compiler.infer direct_import_export_precedence_note, overlay_skips_kernel_name), so in such a module the import does not shadow at all and a bare `String` is ALWAYS the kernel -- the spelling the old argument called unreachable is the only one you reach. Three routes exist and all three are sound for this row: a bare reference in an importing module resolves to the kernel and IS this row's binding; a bare reference INSIDE v2.std.text resolves LOCALLY (locals beat kernel) and is gated structural, never reaching the row; and a QUALIFIED v2.std.text.String resolves through the alias to the dotted name std.algebra.FreeMonoid, which matches no bare row. Symbol was captured precisely because its token differed from its spelling, and that clause survives unchanged. ESTABLISHED BY EXECUTION, not by reading precedence: v1.tests.claim.carrier_realization_census run over a fixture module importing both v2.std.text String and v2.std.node Node reports the bare String reference carrying the kernel identity and realizing as the host spelling, against a positive control in the same fixture where a v2.std.node.Node reference -- bare and qualified alike -- carries its real declaring module. The instrument is named rather than its rows transcribed (DESIGN section 6); re-derive by running that census over any closure containing such a module.".to_string(), + proof: "The kernel string_type is minted by v1.compiler.types for every string literal and carries no declaration; both .dag declarations of the spelling (v2.std.text, std.string_type) are gated structural by v1.compiler.coercion structural_declaration_modules_for and never reach this row. THE VERDICT STANDS AND ITS ORIGINAL ARGUMENT WAS EXACTLY INVERTED, corrected here rather than softened because the inverted form would justify the wrong things if reused. It read: the bare spelling cannot be captured because the only import that could shadow it binds the SAME token, so in a module importing v2.std.text String every `String` reference IS the text carrier and the kernel spelling is unreachable there. The opposite is true. KERNEL NAMES ARE NEVER OVERRIDDEN BY IMPORTS (v1.compiler.infer direct_import_export_precedence_note, overlay_skips_kernel_name), so in such a module the import does not shadow at all and a bare `String` is ALWAYS the kernel -- the spelling the old argument called unreachable is the only one you reach. Three routes exist and all three are sound for this row: a bare reference in an importing module resolves to the kernel and IS this row's binding; a bare reference INSIDE v2.std.text resolves LOCALLY (locals beat kernel) and is gated structural, never reaching the row; and a QUALIFIED v2.std.text.String resolves through the alias to the dotted name std.algebra.FreeMonoid, which matches no bare row. Symbol was captured precisely because its token differed from its spelling, and that clause survives unchanged. ESTABLISHED BY EXECUTION, not by reading precedence -- AND THE SUBJECT NAMED HERE IS CORRECTED: this sentence previously said the census was run over A FIXTURE MODULE importing both v2.std.text String and v2.std.node Node. IT WAS NOT. The receipts carry no fixture rows at all; the subjects were LIVE CORPUS MODULES, and naming a subject that was not run is the same citation defect this row exists to correct. What v1.tests.claim.carrier_realization_census actually reports: in std.algebra, a module that imports the spelling, a bare String carries the kernel identity at declaration_field AND at fn_signature_param; inside v2.std.text the same spelling carries its own declaring module and diverges with exact identity, which is route 2 executed rather than argued; and v2.std.node Node carries its real declaring module at both position kinds as the positive control. RE-DERIVATION IS POSITION-KIND SENSITIVE AND THE OBVIOUS INSTRUCTION IS A TRAP. Running that census over a closure re-derives routes 1 and 2 soundly. It does NOT re-derive route 3: at fn_signature_param the census resolves a QUALIFIED v2.std.text.String through the alias onto the alias declaration's own name, which is the spelling String, and attributes it to -- confidently naming the very carrier the qualification was written to move away from. That is measured by vivid-deer-102 and filed as recurring failure mode alias_resolution_collides_with_kernel_spelling (gunbc#9939); the same instrument is correct for qualified aliases at declaration_field. ROUTE 3 THEREFORE RESTS ON STRUCTURAL RESOLUTION PLUS A RUSTC MEASUREMENT -- the emitted crate carries an E0308 on the bare arm and not on the qualified one -- and explicitly NOT on this census, which cannot answer at that position. The instrument is named rather than its rows transcribed (DESIGN section 6).".to_string(), }), }), Rc::new(CheckpointRowMigration { dag_name: "Int".to_string(), From 1d87dc436dc71f9fc858ce350e740de25f6b95d7 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 05:38:00 +0000 Subject: [PATCH 11/21] =?UTF-8?q?The=20relocation=20note=20was=20prose=20i?= =?UTF-8?q?n=20a=20String=20row,=20which=20=C2=A74c=20quarantines?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit cli_wire_host_relocation_note was a `data ... : String` whose only purpose was commentary, with no consumer -- the neighbouring SeedGrowthJustification did not reference the symbol, it referenced the NAME inside its own prose. That is the state DESIGN §4c names: an ordinary String declaration carrying commentary is mechanically indistinguishable from program data, and `//` is the quarantine boundary that keeps the two apart. It is authored rationale about why the roster counts a relocation, so it becomes an annotation on the declaration it explains. The FACT it carried does not disappear with it: that exit_status_for_class is a relocation rather than new behaviour is now stated inside the justification's own `reason`, where a consumer reading the receipt sees it, rather than in a sibling row a consumer would have to know to look up. Found by review 58455 on gunbc#9864. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/gunbc/cli_wire_host_admission.dag | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/dag/gunbc/cli_wire_host_admission.dag b/dag/gunbc/cli_wire_host_admission.dag index df4f909925a..3bddeeb4282 100644 --- a/dag/gunbc/cli_wire_host_admission.dag +++ b/dag/gunbc/cli_wire_host_admission.dag @@ -26,8 +26,18 @@ data cli_wire_host_receipt_disposition: Disposition = Terminal { // has to live where that structure lives. That is the same boundary every other value-projecting // item in this roster sits on, not new debt of its own kind. -data cli_wire_host_relocation_note: String = "exit_status_for_class IS NOT NEW BEHAVIOUR AND SAYING SO IS PART OF THE RECEIPT. Its body was MOVED out of main.rs's exit_status_for, which now delegates to it. It is enumerated below because it is a hand-authored declaration that did not exist before at that name and in that module, and netting a relocation against an addition is exactly the arithmetic gunbc.seed_growth_admission refuses -- but a reader counting behaviour rather than declarations should know that the process-exit path gained nothing here and was only made callable from the wire path beside it." - +// exit_status_for_class IS NOT NEW BEHAVIOUR, and why the roster counts it anyway. Its body was +// MOVED out of main.rs's exit_status_for, which now delegates to it. It is enumerated below because +// it is a hand-authored declaration that did not exist before at that name and in that module, and +// netting a relocation against an addition is exactly the arithmetic gunbc.seed_growth_admission +// refuses -- but a reader counting BEHAVIOUR rather than DECLARATIONS should know that the +// process-exit path gained nothing here and was only made callable from the wire path beside it. +// +// This was a `data ... : String` row until review 58455 named it: a String declaration whose only +// purpose is commentary is the state DESIGN section 4c quarantines, because nothing distinguishes it +// from program data. It is authored rationale about why the roster has the shape it has, so it is an +// annotation. The fact it carried -- that one of the five is a relocation -- is stated inside the +// justification's own `reason`, where a consumer reading the receipt can see it. data cli_wire_host_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { hand_authored_declarations: [ DeclarationRef { @@ -86,7 +96,7 @@ data cli_wire_host_seed_growth_justification: SeedGrowthJustification = SeedGrow field: WholeDeclaration } ], - reason: "WHY RUST IS STILL NEEDED HERE: the subject is the HOST PROCESS -- stdout bytes and an exit status -- and it is reached from a returned interpreter Value. Neither end has a .dag denotation today: there is no modeled carrier for a running process's standard output, and no modeled projection of the interpreter's own Value representation, so the fold between them cannot be written in the substrate it is bridging into. This is a boundary item, not seed-shrink debt.\n\nWHAT IT REMOVED: gunbc.cli_dispatch_surface's scm row carried CliRefusesUnwired -- the compiler's own dispatch model recording that the scm command family computed answers no user could invoke. Every modeled scm entry was therefore specification without execution. With this route bound, gunbc scm log, status and init reach an operator, which is the only reason the .dag side of this change is worth anything.\n\nHAND-ITEM DELTA: +11 FROM THE MERGE BASE, ENUMERATED ABOVE -- five production declarations (CliWireClass, classify_cli_wire, CliWireOutcome, cli_wire_outcome, exit_status_for_class) and six test items (one test module and its five fns). Reproducible from the merge base, never the moving tip: git diff $(git merge-base main HEAD)...HEAD -- src/v1/stage0/src/cli_run.rs src/v1/stage0/src/main.rs, which reports 255 insertions in cli_run.rs and 54 insertions with 30 deletions in main.rs, and no other .rs file on this branch differs. One of the five, exit_status_for_class, is a RELOCATION rather than new behaviour -- see cli_wire_host_relocation_note.\n\nWHY THE CLASSIFIER AND THE OUTCOME ARE TWO ITEMS: the classification is a question about a value and the outcome is a decision about a process, and fusing them would have put the write-or-refuse decision inside a match arm in main.rs where no test could reach it. Splitting them is what made the five-case matrix authorable, including the two cases that carry the actual safety content -- an unprintable response REFUSES rather than printing nothing, and an exit_failure carrying status zero is refused on the wire path exactly as it already was on the process-exit path.", + reason: "WHY RUST IS STILL NEEDED HERE: the subject is the HOST PROCESS -- stdout bytes and an exit status -- and it is reached from a returned interpreter Value. Neither end has a .dag denotation today: there is no modeled carrier for a running process's standard output, and no modeled projection of the interpreter's own Value representation, so the fold between them cannot be written in the substrate it is bridging into. This is a boundary item, not seed-shrink debt.\n\nWHAT IT REMOVED: gunbc.cli_dispatch_surface's scm row carried CliRefusesUnwired -- the compiler's own dispatch model recording that the scm command family computed answers no user could invoke. Every modeled scm entry was therefore specification without execution. With this route bound, gunbc scm log, status and init reach an operator, which is the only reason the .dag side of this change is worth anything.\n\nHAND-ITEM DELTA: +11 FROM THE MERGE BASE, ENUMERATED ABOVE -- five production declarations (CliWireClass, classify_cli_wire, CliWireOutcome, cli_wire_outcome, exit_status_for_class) and six test items (one test module and its five fns). Reproducible from the merge base, never the moving tip: git diff $(git merge-base main HEAD)...HEAD -- src/v1/stage0/src/cli_run.rs src/v1/stage0/src/main.rs, which reports 255 insertions in cli_run.rs and 54 insertions with 30 deletions in main.rs, and no other .rs file on this branch differs. One of the five, exit_status_for_class, is a RELOCATION rather than new behaviour: its body was moved out of main.rs's exit_status_for, which now delegates to it, so the process-exit path gained no behaviour and was only made callable from the wire path beside it. It is counted because the roster counts hand-authored DECLARATIONS, and netting a relocation against an addition is the arithmetic gunbc.seed_growth_admission refuses.\n\nWHY THE CLASSIFIER AND THE OUTCOME ARE TWO ITEMS: the classification is a question about a value and the outcome is a decision about a process, and fusing them would have put the write-or-refuse decision inside a match arm in main.rs where no test could reach it. Splitting them is what made the five-case matrix authorable, including the two cases that carry the actual safety content -- an unprintable response REFUSES rather than printing nothing, and an exit_failure carrying status zero is refused on the wire path exactly as it already was on the process-exit path.", owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, trigger: "Delete CliWireClass, classify_cli_wire and their tests when the interpreter publishes a modeled projection of a returned Value against a declared type -- an inhabitance decision the substrate answers, rather than a hand-written field-by-field match on the host Value representation. Delete CliWireOutcome, cli_wire_outcome, exit_status_for_class and their tests when std models a process's standard output and exit status as a carrier the .dag side can produce directly, so a command entry returns the whole host effect and the seed only executes it. Both triggers name a CAPABILITY the substrate does not have today; neither is discharged by any artifact short of it, and in particular neither is discharged by moving this Rust to another file.", current_boundary: "gunbc.cli_wire_host_admission -> v1_compiler.cli_run cli_wire_outcome -> v1_compiler.main run_verb -> the host process stdout and exit status" From 3096ca160ee21aae6de204e2243491a6b51f8f32 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 06:09:23 +0000 Subject: [PATCH 12/21] Admit the entry name, and make the init decision witnessable Two of the four findings in review 5085479276 on gunbc#9864. THE NAME WAS USED TWICE AND GUARANTEED ONCE. initialize_repository asked the listing about `name` and separately joined directory + "/" + name into a path, with nothing making those the same subject. `subdir/repo.json` is asked about as a child of the listed directory while the join reaches past it, `../victim` leaves it entirely, `.`/`..`/`""` name no child at all, and -- the case that belongs to the filesystem module rather than to any caller -- a name carrying a newline can make the membership test answer yes for an entry that is not there, because newline is Filesystem.List's own delimiter. FilesystemEntryName is sole_constructor, so admission is unavoidable rather than advisory, and the refusal names which rule rejected the spelling. Its scope is stated honestly: it is adopted at this consumer, filesystem_entry_presence still takes a String, and widening that is a replacement migration over the whole population with its own next-rung trigger -- not smuggled into the change that introduces the carrier. THE DECISION WAS NOT WITNESSED, ONLY ITS RENDERING. Every enrolled init claim built a refusal outcome and checked how it printed, so nothing executed the step that CHOOSES an outcome from an observation; a mutation routing indeterminate to the write arm left the family green. scm_init_decision is that step with the two operations lifted out, and the four arms are now driven one fact apart through the REAL fold -- FilesystemEstablishedAbsence being sole_constructor means a witness cannot hand in a fabricated absence, which forces the evidence to cover filesystem_file_observation and the decision together. Executed: routing indeterminate to a present-refusal takes an_unobservable_path_does_not_authorize_a_write red; routing a real absence away from the write arm takes only_an_established_absence_may_create red. The third mutation -- routing DISAGREEMENT to the write arm -- is unwritable, because ScmInitMayCreate carries the sole_constructor absence and no arm can manufacture one. The rung is split on that boundary rather than averaged. The refusal vocabulary is one type (ScmInitRefusal) consumed by both the decision and the outcome, so a refusal has one spelling rather than two, and the outcome never carries an arm that is only ever intermediate. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/extdeps/filesystem/filesystem_io.dag | 88 ++++++++++ dag/gunbc/scm/init.dag | 118 ++++++++++--- dag/gunbc/scm/render.dag | 40 ++++- dag/test/claim/scm/scm_cli_witness_test.dag | 174 ++++++++++++++++++-- 4 files changed, 381 insertions(+), 39 deletions(-) diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index f4f9cb99490..675cd201b07 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -57,6 +57,94 @@ fn filesystem_listing_names_entry(listing: String, name: String) -> Bool { ) } +// A NAME IS NOT A PATH COMPONENT UNTIL SOMETHING SAYS SO. `filesystem_listing_names_entry` above +// answers a membership question over a NEWLINE-DELIMITED wire format, and every consumer that has an +// entry name also builds a path from it by joining a directory to it. Those are two uses of one +// value, and an ordinary `String` guarantees neither: `""`, `.`, `..`, `subdir/repo.json` and +// `../victim` do not denote one direct child of the listed directory, so the listing is asked about +// one subject while the path names another. The newline case is the sharpest and belongs to THIS +// module rather than to any caller, because the delimiter is `List`'s own encoding: a name +// containing a newline can make the membership test answer yes for an entry that is not there. +// +// So the component is admitted once and carried. `FilesystemEntryName` is `sole_constructor`, which +// is what makes the admission unavoidable rather than advisory -- a caller cannot mint one by +// writing a literal, and the refusal arm names which rule rejected the spelling instead of returning +// a bare false. +// +// SCOPE, STATED RATHER THAN IMPLIED. This carrier is ADOPTED AT ITS FIRST CONSUMER and is not yet +// the type of `filesystem_entry_presence`'s `name` parameter, which is still `String` and still +// reachable by every existing caller. Widening it is a replacement migration over that whole +// population and belongs with `filesystem_absence_establishment_adoption_standing` above, not +// smuggled into the change that introduces the carrier. What is true today: a consumer that admits +// the name and then uses the SAME admitted value for both the membership test and the path +// construction cannot put those two out of step. A consumer that does not adopt it is exactly as +// exposed as before. RUNG: mitigatable, and structurally guaranteed only for adopting consumers. +// NEXT-RUNG TRIGGER: `filesystem_entry_presence` and the path-joining sites take +// `FilesystemEntryName` rather than `String`, at which point a raw name cannot reach either. +type FilesystemEntryName sole_constructor { + name: String +} + +type FilesystemEntryNameAdmission + = FilesystemEntryNameAdmitted(FilesystemEntryName) + | FilesystemEntryNameRefused { name: String, cause: String } + +fn filesystem_entry_name_text(component: FilesystemEntryName) -> String { + component.name +} + +// THE RULES ARE SEPARATE ARMS BECAUSE THE REMEDIES DIFFER. An empty name is a caller that forgot to +// supply one; `.` and `..` are directory references that resolve somewhere other than a child; +// a separator means the caller passed a PATH where a component was asked for, which is the case that +// escapes the listed directory entirely; and a newline or carriage return is the one that corrupts +// the membership test itself. +fn admit_filesystem_entry_name(name: String) -> FilesystemEntryNameAdmission { + if name == "" { + FilesystemEntryNameRefused { + name: name, + cause: "an entry name is empty, so it names no child of any directory", + } + } else if name == "." { + FilesystemEntryNameRefused { + name: name, + cause: "`.` is the directory itself rather than an entry within it", + } + } else if name == ".." { + FilesystemEntryNameRefused { + name: name, + cause: "`..` is the parent directory rather than an entry within it", + } + } else if string_contains(s: name, pattern: "/") { + FilesystemEntryNameRefused { + name: name, + cause: join([ + "the entry name ", name, " contains a path separator, so it is a PATH and not one direct ", + "child of the listed directory -- the listing would be asked about a different subject ", + "than the one the joined path names", + ], ""), + } + } else if string_contains(s: name, pattern: "\n") { + FilesystemEntryNameRefused { + name: name, + cause: join([ + "the entry name ", name, " contains a newline, which is the delimiter Filesystem.List uses ", + "between entries, so a membership test over the listing could answer yes for an entry that ", + "is not present", + ], ""), + } + } else if string_contains(s: name, pattern: "\r") { + FilesystemEntryNameRefused { + name: name, + cause: join([ + "the entry name ", name, " contains a carriage return, which can terminate a line in the ", + "listing wire format and make the membership test answer about a different spelling", + ], ""), + } + } else { + FilesystemEntryNameAdmitted(FilesystemEntryName { name: name }) + } +} + // THE RULE ABOVE WAS PROSE FOR AS LONG AS IT EXISTED, AND PROSE REPRODUCED THE DEFECT IT FORBIDS. // It was ruled on review 46148, written into `gunbc.roadmap_belt_actuate` as a `data ... : String` // note, and then violated in `gunbc.deploy_transition` -- authored by the same hand, in the same diff --git a/dag/gunbc/scm/init.dag b/dag/gunbc/scm/init.dag index 3df89785e02..326af680ce8 100644 --- a/dag/gunbc/scm/init.dag +++ b/dag/gunbc/scm/init.dag @@ -33,6 +33,13 @@ module gunbc.scm.init import std.types { String } import extdeps.filesystem.filesystem_io { Filesystem, + FilesystemEntryName, + FilesystemEntryNameAdmitted, + FilesystemEntryNameRefused, + FilesystemEstablishedAbsence, + FilesystemFileObservation, + admit_filesystem_entry_name, + filesystem_entry_name_text, FilesystemFileAbsent, FilesystemFileRead, FilesystemFileIndeterminate, @@ -59,47 +66,118 @@ import gunbc.scm.repository_save { RepositorySave, save_repository } // an operator's next action differs -- one path already IS a repository, one holds something else // that would be destroyed, and one could not be observed at all, which is a fault to investigate // rather than a state of the path. +// ONE REFUSAL VOCABULARY, CONSUMED BY BOTH THE DECISION AND THE OUTCOME. The decision about whether +// bytes may be written and the outcome of the whole verb are different facts -- one is reached +// without touching the filesystem, the other includes what the write did -- but a refusal means the +// same thing in both, so it is ONE type. Giving each its own refusal arms would be two spellings of +// one concept, which is the fork DESIGN section 3 forbids; and folding the decision into the outcome +// would put an arm on the outcome that is only ever intermediate. +type ScmInitRefusal + = ScmInitRepositoryPresent { path: String } + | ScmInitForeignFilePresent { path: String } + | ScmInitPathUnobserved { path: String, cause: String } + | ScmInitNameNotAnEntry { name: String, cause: String } + +// THE ARMS ARE THE ANSWER. There is no `initialized: Bool` beside a save outcome: a value whose flag +// disagreed with its shape would have a spelling, and the refusals are distinguished because an +// operator's next action differs -- one path already IS a repository, one holds something else that +// would be destroyed, one could not be observed at all, and one was never a valid +// entry name. type ScmInitOutcome = ScmInitialized { save: RepositorySave } - | ScmInitRefusedRepositoryPresent { path: String } - | ScmInitRefusedForeignFilePresent { path: String } - | ScmInitRefusedPathUnobserved { path: String, cause: String } + | ScmInitRefused { cause: ScmInitRefusal } + +// WHAT THE OBSERVATION DECIDES, WITHOUT PERFORMING ANYTHING. `ScmInitMayCreate` carries the +// established absence rather than a bare path, so the permission to write is the SAME value the +// listing produced and cannot be manufactured beside it -- FilesystemEstablishedAbsence is +// sole_constructor and its only mint is the substrate fold. +type ScmInitDecision + = ScmInitMayCreate(FilesystemEstablishedAbsence) + | ScmInitDecided { cause: ScmInitRefusal } // PRESENT BYTES ARE CLASSIFIED, NEVER TRUSTED. Both present arms refuse, so this classification // changes only what the operator is told -- which is the whole difference between "your repository // is already here" and "something else is here and I will not touch it". -fn init_present_refusal(path: String, content: String) -> ScmInitOutcome { +fn init_present_refusal(path: String, content: String) -> ScmInitRefusal { match parse_json_document(s: content) { - JsonDocumentUnreadable { gap: _ } => ScmInitRefusedForeignFilePresent { path: path } + JsonDocumentUnreadable { gap: _ } => ScmInitForeignFilePresent { path: path } JsonDocumentParsed { value: v } => match decode_repository(v: v) { - RepositoryDecoded { envelope: _ } => ScmInitRefusedRepositoryPresent { path: path } - RepositoryDecodeRefused { cause: _ } => ScmInitRefusedForeignFilePresent { path: path } + RepositoryDecoded { envelope: _ } => ScmInitRepositoryPresent { path: path } + RepositoryDecodeRefused { cause: _ } => ScmInitForeignFilePresent { path: path } } } } +// THE NAME IS ADMITTED BEFORE IT IS USED TWICE. This function asks the listing about `name` and +// separately joins `directory + "/" + name` into a path, and an ordinary String does not guarantee +// those two describe the same subject: `subdir/repo.json` is asked about as a child of `directory` +// while the join reaches into a subdirectory, `../victim` leaves the listed directory entirely, and +// a name carrying a newline can make the membership test over the newline-delimited listing answer +// about an entry that is not there. Admitting once and using the SAME admitted component for both +// closes the gap between the question and the action; a refused name never reaches either. fn initialize_repository(directory: String, name: String) -> ScmInitOutcome { - let path = join([directory, "/", name], "") + match admit_filesystem_entry_name(name: name) { + FilesystemEntryNameRefused { name: n, cause: c } => + ScmInitRefused { cause: ScmInitNameNotAnEntry { name: n, cause: c } } + FilesystemEntryNameAdmitted(component) => + initialize_repository_at(directory: directory, component: component) + } +} + +fn initialize_repository_at( + directory: String, + component: FilesystemEntryName, +) -> ScmInitOutcome { + let entry = filesystem_entry_name_text(component: component) + let path = join([directory, "/", entry], "") let listed = Filesystem.List(path: directory) let read = Filesystem.Read(path: path) - match filesystem_file_observation( - listing: filesystem_listing_observation( - directory: directory, - success: listed.success, - entries: listed.entries, - error: listed.error + match scm_init_decision( + observation: filesystem_file_observation( + listing: filesystem_listing_observation( + directory: directory, + success: listed.success, + entries: listed.entries, + error: listed.error + ), + name: entry, + path: path, + read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error) ), - name: name, path: path, - read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error) ) { - FilesystemFileAbsent(_) => + ScmInitDecided { cause: c } => ScmInitRefused { cause: c } + ScmInitMayCreate(_) => ScmInitialized { save: save_repository(path: path, repo: empty_repository()) } - FilesystemFileRead { path: p, content: c } => init_present_refusal(path: p, content: c) + } +} + +// AND THE MUTATION THAT WOULD MATTER MOST CANNOT BE WRITTEN. Routing the indeterminate or the +// present arm to the write arm is authorable, and both are held red by +// test.claim.scm.scm_cli_witness (an_unobservable_path_does_not_authorize_a_write and +// only_an_established_absence_may_create each fail under exactly that edit). Routing the DISAGREEMENT +// arm there is not authorable at all: ScmInitMayCreate carries a FilesystemEstablishedAbsence, which +// is sole_constructor and minted only by the substrate fold from a listing that succeeded, so no arm +// can manufacture the permission to write. The rung is therefore split and stated rather than +// averaged: structurally impossible for fabricating a write permission (rung 4, no constructor), +// and mechanically preventable for routing a REAL absence to the wrong outcome (rung 2, held by the +// claims above). +// +// THE DECISION IS ITS OWN FUNCTION SO IT CAN BE WITNESSED WITHOUT A FILESYSTEM. Every arm below is a +// choice about whether bytes may be written, and while it lived inside the effectful entry the only +// reachable evidence was that refusals RENDER -- a mutation routing indeterminate or disagreement to +// the write arm left every enrolled claim green. Separating the fold from the two operations that +// feed it makes the four arms drivable one fact apart, which is the difference between a tested +// decision and a tested renderer. +fn scm_init_decision(observation: FilesystemFileObservation, path: String) -> ScmInitDecision { + match observation { + FilesystemFileAbsent(absence) => ScmInitMayCreate(absence) + FilesystemFileRead { path: p, content: c } => + ScmInitDecided { cause: init_present_refusal(path: p, content: c) } FilesystemFileIndeterminate { cause: c } => - ScmInitRefusedPathUnobserved { path: path, cause: c } + ScmInitDecided { cause: ScmInitPathUnobserved { path: path, cause: c } } FilesystemFileObservationsDisagree { path: p, cause: c } => - ScmInitRefusedPathUnobserved { path: p, cause: c } + ScmInitDecided { cause: ScmInitPathUnobserved { path: p, cause: c } } } } diff --git a/dag/gunbc/scm/render.dag b/dag/gunbc/scm/render.dag index 097e8667e78..bd2639d7447 100644 --- a/dag/gunbc/scm/render.dag +++ b/dag/gunbc/scm/render.dag @@ -52,9 +52,12 @@ import gunbc.scm.repository_load { repository_load_refusal_lines } import gunbc.scm.init { ScmInitOutcome, ScmInitialized, - ScmInitRefusedRepositoryPresent, - ScmInitRefusedForeignFilePresent, - ScmInitRefusedPathUnobserved + ScmInitRefused, + ScmInitRefusal, + ScmInitRepositoryPresent, + ScmInitForeignFilePresent, + ScmInitPathUnobserved, + ScmInitNameNotAnEntry } import gunbc.scm.repository_save { RepositorySave, @@ -267,33 +270,52 @@ fn scm_save_cli_response( fn scm_init_lines(outcome: ScmInitOutcome) -> List { match outcome { ScmInitialized { save: save } => repository_save_lines(save: save) - ScmInitRefusedRepositoryPresent { path: p } => + ScmInitRefused { cause: cause } => scm_init_refusal_lines(cause: cause) + } +} + +fn scm_init_refusal_lines(cause: ScmInitRefusal) -> List { + match cause { + ScmInitRepositoryPresent { path: p } => [ concat("refusing to initialize ", p), " a repository is already there, and init would replace its whole history" ] - ScmInitRefusedForeignFilePresent { path: p } => + ScmInitForeignFilePresent { path: p } => [ concat("refusing to initialize ", p), " a file is already there that is not a repository, and init would destroy it" ] - ScmInitRefusedPathUnobserved { path: p, cause: c } => + ScmInitPathUnobserved { path: p, cause: c } => [ concat("refusing to initialize ", p), concat(" the path could not be observed, so nothing about it is established -- ", c) ] + ScmInitNameNotAnEntry { name: n, cause: c } => + [ + concat("refusing to initialize ", n), + concat(" that is not one entry of the directory, so no path was built from it -- ", c) + ] } } fn scm_init_exit(outcome: ScmInitOutcome) -> ProcessExit { match outcome { ScmInitialized { save: save } => scm_save_exit(save: save) - ScmInitRefusedRepositoryPresent { path: _ } => + ScmInitRefused { cause: cause } => scm_init_refusal_exit(cause: cause) + } +} + +fn scm_init_refusal_exit(cause: ScmInitRefusal) -> ProcessExit { + match cause { + ScmInitRepositoryPresent { path: _ } => exit_failure(reason: "repository already present") - ScmInitRefusedForeignFilePresent { path: _ } => + ScmInitForeignFilePresent { path: _ } => exit_failure(reason: "path occupied by a non-repository file") - ScmInitRefusedPathUnobserved { path: _, cause: _ } => + ScmInitPathUnobserved { path: _, cause: _ } => exit_failure(reason: "path could not be observed") + ScmInitNameNotAnEntry { name: _, cause: _ } => + exit_failure(reason: "name is not one entry of the directory") } } diff --git a/dag/test/claim/scm/scm_cli_witness_test.dag b/dag/test/claim/scm/scm_cli_witness_test.dag index de4226357fc..ebe49fe5074 100644 --- a/dag/test/claim/scm/scm_cli_witness_test.dag +++ b/dag/test/claim/scm/scm_cli_witness_test.dag @@ -24,9 +24,33 @@ import gunbc.scm.status { repository_status } import gunbc.scm.authoring { empty_proposal } import gunbc.scm.cli { scm_log_response, scm_status_response, scm_init_response, plain_terminal_capability } import gunbc.scm.init { - ScmInitRefusedRepositoryPresent, - ScmInitRefusedForeignFilePresent, - ScmInitRefusedPathUnobserved + ScmInitRefused, + ScmInitRepositoryPresent, + ScmInitForeignFilePresent, + ScmInitPathUnobserved, + ScmInitNameNotAnEntry, + ScmInitDecision, + ScmInitMayCreate, + ScmInitDecided, + ScmInitialized, + scm_init_decision, + initialize_repository +} +import extdeps.filesystem.filesystem_io { + FilesystemDirectoryListed, + FilesystemDirectoryListingRefused, + FilesystemDirectoryListing, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + FilesystemFileObservation, + filesystem_listing_observation, + filesystem_read_outcome, + filesystem_file_observation, + admit_filesystem_entry_name, + FilesystemEntryNameAdmitted, + FilesystemEntryNameRefused } // THE BYTES PIN THE CAPABILITY. This is the same expected string the render-level witness pins for @@ -134,18 +158,18 @@ fn wire_bytes(r: CliWireResponse) -> String { // foreign-file line -- telling an operator their bytes are being protected when in fact nothing was // observed -- would turn these red. test fn an_init_refusal_never_exits_success() -> Bool { - wire_refuses(r: scm_init_response(outcome: ScmInitRefusedRepositoryPresent { path: "repo.json" })) - && wire_refuses(r: scm_init_response(outcome: ScmInitRefusedForeignFilePresent { path: "repo.json" })) + wire_refuses(r: scm_init_response(outcome: ScmInitRefused { cause: ScmInitRepositoryPresent { path: "repo.json" } })) + && wire_refuses(r: scm_init_response(outcome: ScmInitRefused { cause: ScmInitForeignFilePresent { path: "repo.json" } })) && wire_refuses(r: scm_init_response( - outcome: ScmInitRefusedPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } + outcome: ScmInitRefused { cause: ScmInitPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } } )) } test fn the_three_init_refusals_render_differently() -> Bool { - let present = wire_bytes(r: scm_init_response(outcome: ScmInitRefusedRepositoryPresent { path: "repo.json" })) - let foreign = wire_bytes(r: scm_init_response(outcome: ScmInitRefusedForeignFilePresent { path: "repo.json" })) + let present = wire_bytes(r: scm_init_response(outcome: ScmInitRefused { cause: ScmInitRepositoryPresent { path: "repo.json" } })) + let foreign = wire_bytes(r: scm_init_response(outcome: ScmInitRefused { cause: ScmInitForeignFilePresent { path: "repo.json" } })) let unobserved = wire_bytes(r: scm_init_response( - outcome: ScmInitRefusedPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } + outcome: ScmInitRefused { cause: ScmInitPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } } )) present != foreign && foreign != unobserved && present != unobserved && present != "" } @@ -154,9 +178,139 @@ test fn the_three_init_refusals_render_differently() -> Bool { // operator to investigate without saying what could not be observed. test fn the_unobserved_refusal_names_what_could_not_be_observed() -> Bool { match scm_init_response( - outcome: ScmInitRefusedPathUnobserved { path: "repo.json", cause: "Permission denied" } + outcome: ScmInitRefused { cause: ScmInitPathUnobserved { path: "repo.json", cause: "Permission denied" } } ) { CliWireUnprintable { cause: _ } => false CliWirePrintable { bytes: b, exit: _ } => b.contains("Permission denied") && b.contains("repo.json") } } + +// ------------------------------------------------------------------------------------------------ +// THE INIT DECISION, DRIVEN DIRECTLY. Review 5085479276 on gunbc#9864 found that every enrolled init +// claim constructed a REFUSAL OUTCOME and checked how it rendered, so nothing executed the step that +// CHOOSES an outcome from an observation. A mutation routing the indeterminate or the disagreement +// arm to the write arm left the whole family green -- the claims were about a renderer, and the +// safety content is in the decision. +// +// scm_init_decision is that step with the two filesystem operations lifted out, so all four +// observation arms are drivable one fact apart. Only FilesystemFileAbsent may reach ScmInitMayCreate. +// ------------------------------------------------------------------------------------------------ + +fn decision_arm(d: ScmInitDecision) -> String { + match d { + ScmInitMayCreate(_) => "may_create" + ScmInitDecided { cause: c } => + match c { + ScmInitRepositoryPresent { path: _ } => "repository_present" + ScmInitForeignFilePresent { path: _ } => "foreign_present" + ScmInitPathUnobserved { path: _, cause: _ } => "unobserved" + ScmInitNameNotAnEntry { name: _, cause: _ } => "name_not_an_entry" + } + } +} + +fn decide(o: FilesystemFileObservation) -> String { + decision_arm(d: scm_init_decision(observation: o, path: "d/repo.json")) +} + +// THE OBSERVATION IS BUILT BY THE REAL FOLD, NOT HANDED IN. FilesystemEstablishedAbsence is +// sole_constructor, so a witness CANNOT mint an absence -- which is the seal doing its job, and it +// forces this evidence to be stronger than it would otherwise have been: every cell below drives +// filesystem_file_observation over listing and read channels, so the claims cover the fold and the +// decision together rather than the decision over a fabricated input. +fn observe(listed: Bool, entries: String, read_ok: Bool, content: String) -> FilesystemFileObservation { + filesystem_file_observation( + listing: filesystem_listing_observation( + directory: "d", + success: listed, + entries: entries, + error: if listed { "" } else { "Permission denied" }, + ), + name: "repo.json", + path: "d/repo.json", + read: filesystem_read_outcome( + content: content, + success: read_ok, + error: if read_ok { "" } else { "No such file or directory" }, + ), + ) +} + +// AN ESTABLISHED ABSENCE IS THE ONLY THING THAT MAY WRITE. This is the positive control: without it +// every refusal claim below could be satisfied by a decision that refuses unconditionally. +test fn only_an_established_absence_may_create() -> Bool { + decide(o: observe(listed: true, entries: "other.json", read_ok: false, content: "")) == "may_create" +} + +// THE THREE NON-ABSENT ARMS EACH REFUSE, AND EACH KEEPS ITS OWN CAUSE. Collapsing indeterminate or +// disagreement into the absent arm is the fail-open this module exists to prevent; collapsing them +// into EACH OTHER would tell an operator to investigate the wrong thing. +test fn an_unobservable_path_does_not_authorize_a_write() -> Bool { + decide(o: observe(listed: false, entries: "", read_ok: false, content: "")) == "unobserved" +} + +// THE LISTING DID NOT NAME IT AND THE READ OF IT SUCCEEDED. One fact apart from the absence cell +// above -- same listing, read flipped -- so this pair is what distinguishes "nothing is there" from +// "the two observations describe different worlds". +test fn two_disagreeing_observations_do_not_authorize_a_write() -> Bool { + decide(o: observe(listed: true, entries: "other.json", read_ok: true, content: "{}")) + == "unobserved" +} + +test fn present_bytes_do_not_authorize_a_write_and_are_classified() -> Bool { + decide(o: observe(listed: true, entries: "repo.json", read_ok: true, content: "not json at all")) + == "foreign_present" + && decide(o: observe( + listed: true, + entries: "repo.json", + read_ok: true, + content: "{\"format\":\"gunbc-scm-repository-v2\"}", + )) != "may_create" +} + +// ------------------------------------------------------------------------------------------------ +// THE ENTRY NAME IS ADMITTED BEFORE IT IS USED TWICE, and these are the spellings that made the +// listing and the path describe different subjects. +// ------------------------------------------------------------------------------------------------ + +fn name_admits(n: String) -> Bool { + match admit_filesystem_entry_name(name: n) { + FilesystemEntryNameAdmitted(_) => true + FilesystemEntryNameRefused { name: _, cause: _ } => false + } +} + +test fn an_ordinary_entry_name_is_admitted() -> Bool { + name_admits(n: "repo.json") +} + +test fn a_name_that_is_not_one_child_of_the_directory_is_refused() -> Bool { + !name_admits(n: "") + && !name_admits(n: ".") + && !name_admits(n: "..") + && !name_admits(n: "subdir/repo.json") + && !name_admits(n: "../victim") +} + +// THE NEWLINE CASE IS THIS MODULE'S OWN, because the delimiter belongs to Filesystem.List's encoding: +// a name carrying one can make the membership test answer about an entry that is not present. +test fn a_name_carrying_the_listing_delimiter_is_refused() -> Bool { + !name_admits(n: "repo.json\nother.json") + && !name_admits(n: "repo.json\rother.json") +} + +// A REFUSED NAME NEVER REACHES THE FILESYSTEM. initialize_repository is effectful, but this arm +// returns before either operation runs, so it is reachable in a SubstrateInputsOnly witness -- and +// that is exactly the property being claimed. +test fn a_refused_name_refuses_before_any_filesystem_operation() -> Bool { + match initialize_repository(directory: "d", name: "../victim") { + ScmInitialized { save: _ } => false + ScmInitRefused { cause: c } => + match c { + ScmInitNameNotAnEntry { name: _, cause: _ } => true + ScmInitRepositoryPresent { path: _ } => false + ScmInitForeignFilePresent { path: _ } => false + ScmInitPathUnobserved { path: _, cause: _ } => false + } + } +} From cda2be36d269d3d640e727c5e8f2b05a69a45af0 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 06:19:00 +0000 Subject: [PATCH 13/21] A malformed wire response is not "some other type" Third of the four findings in review 5085479276 on gunbc#9864. classify_cli_wire returned NotCliWire for two materially different situations: a value of some other type, and a value that NAMES CliWireResponse but does not inhabit it. cli_wire_outcome answers None for NotCliWire so the caller falls through to classify_exit, which meant a malformed wire response was reported as error: function `f` returned `...`, not `ProcessExit` -- true, useless, and about a type the value never claimed. It hides that the value claimed a type it does not inhabit, and it sends the caller to the wrong remedy: wrap this in ExitSuccess, when the actual defect is a missing `bytes`. MalformedCliWire is its own arm and REFUSES rather than falling through, exiting 2 like the other shape refusal. NotCliWire keeps its fall-through unchanged, which is what preserves every pre-existing ProcessExit entry point. THE TESTS THE REVIEW SAID DID NOT EXIST. All five original tests started from an already-classified CliWireClass, so classify_cli_wire had no coverage at all -- the boundary carrying the defect was the one nothing executed. Seven tests now build real interpreter values: a positive control that a well-formed printable still classifies as printable, a control that a plain ProcessExit and a bare string still fall through (the case that must NOT become malformed, or every existing entry point breaks), the four malformed shapes, and one that the refusal reaches the host with status 2 and no stdout. Executed: restoring the fall-through for MalformedCliWire takes a_malformed_wire_response_refuses_rather_than_falling_through red and leaves the other twelve green, so the arm is load-bearing for exactly the reported case. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- src/v1/stage0/src/cli_run.rs | 218 +++++++++++++++++++++++++++++++++-- 1 file changed, 206 insertions(+), 12 deletions(-) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 11c8d4af4a3..1959a22f898 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -18150,6 +18150,18 @@ pub enum CliWireClass { Unprintable { cause: String }, /// Not a `CliWireResponse` at all — reported with what it actually was. NotCliWire { type_name: String }, + /// Nominally a `CliWireResponse`, but its payload does not match the declared shape. + /// + /// This is a SEPARATE arm from `NotCliWire` because the two send the caller to different + /// remedies, and folding them together mis-reported the defect. `NotCliWire` means "ask the + /// other classifier" — the value is some other type and `ProcessExit` may well accept it. A + /// malformed wire response has already ANSWERED the type question: the value says it is a + /// `CliWireResponse`, so falling through to `classify_exit` produces the diagnosis "this is + /// not a ProcessExit", which is true and useless — it names the type the value never claimed + /// to be, and hides that the value claimed a type it does not inhabit. Review 5085479276 on + /// gunbc#9864 found this; the five original tests all constructed an already-classified + /// `CliWireClass`, so none of them executed this boundary at all. + MalformedCliWire { detail: String }, } pub fn classify_cli_wire( @@ -18175,18 +18187,16 @@ pub fn classify_cli_wire( let bytes = match ctx.field(fields, "bytes") { Some(Value::Str(s)) => s.to_string(), _ => { - return CliWireClass::NotCliWire { - type_name: "CliWireResponse::CliWirePrintable{bytes: }" - .to_string(), + return CliWireClass::MalformedCliWire { + detail: "CliWirePrintable{bytes: }".to_string(), } } }; let exit = match ctx.field(fields, "exit") { Some(v) => classify_exit(v, ctx), None => { - return CliWireClass::NotCliWire { - type_name: "CliWireResponse::CliWirePrintable{exit: }" - .to_string(), + return CliWireClass::MalformedCliWire { + detail: "CliWirePrintable{exit: }".to_string(), } } }; @@ -18198,14 +18208,13 @@ pub fn classify_cli_wire( }, // `cause` is declared NonEmptyStr, so an empty or absent one means the // value did not come from the modeled constructor. - _ => CliWireClass::NotCliWire { - type_name: "CliWireResponse::CliWireUnprintable{cause: }" - .to_string(), + _ => CliWireClass::MalformedCliWire { + detail: "CliWireUnprintable{cause: }".to_string(), }, } } else { - CliWireClass::NotCliWire { - type_name: format!("CliWireResponse::{}", ctx.resolve(*variant_name)), + CliWireClass::MalformedCliWire { + detail: format!("unknown variant {}", ctx.resolve(*variant_name)), } } } @@ -18234,7 +18243,10 @@ pub struct CliWireOutcome { /// /// `NotCliWire` deliberately yields no outcome (`None`): that is not a failure, it is "this /// value is not a wire response", and the caller must fall through to `classify_exit` so every -/// pre-existing `ProcessExit` entry keeps behaving exactly as before. +/// pre-existing `ProcessExit` entry keeps behaving exactly as before. `MalformedCliWire` is the +/// opposite and must NOT fall through: the value already claimed the wire type, so the fall-through +/// would answer a question nobody asked ("it is not a ProcessExit") while the real defect — a value +/// claiming a type it does not inhabit — went unreported. pub fn cli_wire_outcome(class: CliWireClass, function: &str) -> Option { match class { CliWireClass::Printable { bytes, exit } => { @@ -18257,6 +18269,20 @@ pub fn cli_wire_outcome(class: CliWireClass, function: &str) -> Option Some(CliWireOutcome { + status: 2, + message: Some(format!( + "error: function `{function}` returned a `CliWireResponse` that does not match \ + its declared shape: {detail}.\n cause: the value names the wire type, so it is \ + not judged as some other return; it claims a type it does not inhabit. \ + status: refused — printing nothing rather than guessing the missing half." + )), + stdout: None, + }), CliWireClass::NotCliWire { .. } => None, } } @@ -18292,6 +18318,174 @@ pub fn exit_status_for_class(class: ExitClass, function: &str) -> (i32, Option 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) + } + + fn variant(ctx: &InterpContext, ty: &str, va: &str, fields: Vec<(&str, Value)>) -> Value { + let mut fs: Vec<_> = fields.into_iter().map(|(k, v)| (ctx.sym(k), v)).collect(); + fs.sort_by_key(|(k, _)| *k); + Value::Variant { + type_name: ctx.sym(ty), + variant_name: ctx.sym(va), + fields: Rc::new(fs), + } + } + + fn exit_success(ctx: &InterpContext) -> Value { + variant(ctx, "ProcessExit", "ExitSuccess", vec![]) + } + + fn is_malformed(c: &CliWireClass) -> bool { + matches!(c, CliWireClass::MalformedCliWire { .. }) + } + + fn is_not_wire(c: &CliWireClass) -> bool { + matches!(c, CliWireClass::NotCliWire { .. }) + } + + // THE POSITIVE CONTROL. Without it every refusal assertion below is satisfied by a classifier + // that refuses unconditionally. + #[test] + fn a_well_formed_printable_response_classifies_as_printable() { + let c = ctx(); + let v = variant( + &c, + "CliWireResponse", + "CliWirePrintable", + vec![ + ("bytes", str_value("commit 1\n")), + ("exit", exit_success(&c)), + ], + ); + match classify_cli_wire(&v, &c) { + CliWireClass::Printable { bytes, .. } => assert_eq!(bytes, "commit 1\n"), + _ => panic!("expected Printable"), + } + } + + // A DIFFERENT TYPE IS STILL A FALL-THROUGH, and this is the case that must NOT become + // malformed: a plain ProcessExit return is how every pre-existing entry point behaves, and + // classifying it as a broken wire response would break all of them. + #[test] + fn a_process_exit_is_not_a_wire_response_and_falls_through() { + let c = ctx(); + assert!(is_not_wire(&classify_cli_wire(&exit_success(&c), &c))); + assert!(is_not_wire(&classify_cli_wire( + &str_value("just a string"), + &c + ))); + } + + // THE FOUR MALFORMED SHAPES. Each names the wire type and then fails to inhabit it, so each + // must refuse HERE rather than be handed to the ProcessExit classifier. + #[test] + fn a_printable_response_missing_its_bytes_is_malformed_not_foreign() { + let c = ctx(); + let v = variant( + &c, + "CliWireResponse", + "CliWirePrintable", + vec![("exit", exit_success(&c))], + ); + assert!(is_malformed(&classify_cli_wire(&v, &c))); + } + + #[test] + fn a_printable_response_whose_bytes_are_not_a_string_is_malformed() { + let c = ctx(); + let v = variant( + &c, + "CliWireResponse", + "CliWirePrintable", + vec![("bytes", Value::Int(7)), ("exit", exit_success(&c))], + ); + assert!(is_malformed(&classify_cli_wire(&v, &c))); + } + + #[test] + fn a_printable_response_missing_its_exit_is_malformed() { + let c = ctx(); + let v = variant( + &c, + "CliWireResponse", + "CliWirePrintable", + vec![("bytes", str_value("x"))], + ); + assert!(is_malformed(&classify_cli_wire(&v, &c))); + } + + #[test] + fn an_unprintable_response_with_an_empty_or_absent_cause_is_malformed() { + let c = ctx(); + let empty = variant( + &c, + "CliWireResponse", + "CliWireUnprintable", + vec![("cause", str_value(""))], + ); + let absent = variant(&c, "CliWireResponse", "CliWireUnprintable", vec![]); + assert!(is_malformed(&classify_cli_wire(&empty, &c))); + assert!(is_malformed(&classify_cli_wire(&absent, &c))); + } + + #[test] + fn an_unknown_wire_variant_is_malformed() { + let c = ctx(); + let v = variant(&c, "CliWireResponse", "CliWireSomethingElse", vec![]); + assert!(is_malformed(&classify_cli_wire(&v, &c))); + } + + // AND THE REFUSAL REACHES THE HOST. A malformed class that still yielded `None` would leave the + // fall-through in place and this whole arm decorative. + #[test] + fn a_malformed_wire_response_refuses_rather_than_falling_through() { + let c = ctx(); + let v = variant(&c, "CliWireResponse", "CliWireSomethingElse", vec![]); + let out = super::cli_wire_outcome(classify_cli_wire(&v, &c), "scm_log_cli_response") + .expect("a malformed wire response must produce an outcome, not fall through"); + assert_eq!(out.status, 2); + assert!( + out.stdout.is_none(), + "nothing may be printed for a shape refusal" + ); + assert!( + out.message + .expect("a refusal names itself") + .contains("does not match"), + "the message must name the shape defect, not a ProcessExit mismatch" + ); + } +} + #[cfg(test)] mod cli_wire_outcome_tests { use super::{cli_wire_outcome, CliWireClass, ExitClass}; From da79cc133900e7abdffae6728cc6edb9e963ac98 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 06:48:16 +0000 Subject: [PATCH 14/21] The seed-growth receipt undercounted the module I had just added Adding cli_wire_classify_tests put thirteen hand-authored declarations into cli_run.rs that the receipt did not name, while it went on asserting "+11 FROM THE MERGE BASE, ENUMERATED ABOVE". A roster whose subject is hand-authored declarations, silently missing thirteen of them, is the defect it exists to prevent -- and it was introduced by the change that fixed a different one. Enumerated at 25 and recomputed: 449 insertions in cli_run.rs, 84 changed lines in main.rs, re-derived against origin/main rather than a stale local `main` ref. The five test HELPERS are counted, not just the seven test fns. The roster's subject is declarations, and a helper is one; waving them through as "just tests" is the same netting this receipt already refuses for the relocated exit_status_for_class. Two further .rs files differ and the row says WHY they are outside the subject rather than omitting them: gunbc_cli_dispatch_surface.rs and gunbc_rust_source_type_bindings.rs are generated projections regenerated from their .dag authority, so they are excluded by construction, not by exemption. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/gunbc/cli_wire_host_admission.dag | 72 ++++++++++++++++++++++++++- 1 file changed, 71 insertions(+), 1 deletion(-) diff --git a/dag/gunbc/cli_wire_host_admission.dag b/dag/gunbc/cli_wire_host_admission.dag index 3bddeeb4282..58c7cd3f29f 100644 --- a/dag/gunbc/cli_wire_host_admission.dag +++ b/dag/gunbc/cli_wire_host_admission.dag @@ -94,9 +94,79 @@ data cli_wire_host_seed_growth_justification: SeedGrowthJustification = SeedGrow module_path: "v1_compiler.cli_run.cli_wire_outcome_tests", decl_name: "an_exit_failure_with_code_zero_is_refused_on_the_wire_path_too", field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "cli_wire_classify_tests", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "ctx", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "variant", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "exit_success", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "is_malformed", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "is_not_wire", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "a_well_formed_printable_response_classifies_as_printable", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "a_process_exit_is_not_a_wire_response_and_falls_through", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "a_printable_response_missing_its_bytes_is_malformed_not_foreign", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "a_printable_response_whose_bytes_are_not_a_string_is_malformed", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "a_printable_response_missing_its_exit_is_malformed", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "an_unprintable_response_with_an_empty_or_absent_cause_is_malformed", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "an_unknown_wire_variant_is_malformed", + field: WholeDeclaration + }, + DeclarationRef { + module_path: "v1_compiler.cli_run", + decl_name: "a_malformed_wire_response_refuses_rather_than_falling_through", + field: WholeDeclaration } ], - reason: "WHY RUST IS STILL NEEDED HERE: the subject is the HOST PROCESS -- stdout bytes and an exit status -- and it is reached from a returned interpreter Value. Neither end has a .dag denotation today: there is no modeled carrier for a running process's standard output, and no modeled projection of the interpreter's own Value representation, so the fold between them cannot be written in the substrate it is bridging into. This is a boundary item, not seed-shrink debt.\n\nWHAT IT REMOVED: gunbc.cli_dispatch_surface's scm row carried CliRefusesUnwired -- the compiler's own dispatch model recording that the scm command family computed answers no user could invoke. Every modeled scm entry was therefore specification without execution. With this route bound, gunbc scm log, status and init reach an operator, which is the only reason the .dag side of this change is worth anything.\n\nHAND-ITEM DELTA: +11 FROM THE MERGE BASE, ENUMERATED ABOVE -- five production declarations (CliWireClass, classify_cli_wire, CliWireOutcome, cli_wire_outcome, exit_status_for_class) and six test items (one test module and its five fns). Reproducible from the merge base, never the moving tip: git diff $(git merge-base main HEAD)...HEAD -- src/v1/stage0/src/cli_run.rs src/v1/stage0/src/main.rs, which reports 255 insertions in cli_run.rs and 54 insertions with 30 deletions in main.rs, and no other .rs file on this branch differs. One of the five, exit_status_for_class, is a RELOCATION rather than new behaviour: its body was moved out of main.rs's exit_status_for, which now delegates to it, so the process-exit path gained no behaviour and was only made callable from the wire path beside it. It is counted because the roster counts hand-authored DECLARATIONS, and netting a relocation against an addition is the arithmetic gunbc.seed_growth_admission refuses.\n\nWHY THE CLASSIFIER AND THE OUTCOME ARE TWO ITEMS: the classification is a question about a value and the outcome is a decision about a process, and fusing them would have put the write-or-refuse decision inside a match arm in main.rs where no test could reach it. Splitting them is what made the five-case matrix authorable, including the two cases that carry the actual safety content -- an unprintable response REFUSES rather than printing nothing, and an exit_failure carrying status zero is refused on the wire path exactly as it already was on the process-exit path.", + reason: "WHY RUST IS STILL NEEDED HERE: the subject is the HOST PROCESS -- stdout bytes and an exit status -- and it is reached from a returned interpreter Value. Neither end has a .dag denotation today: there is no modeled carrier for a running process's standard output, and no modeled projection of the interpreter's own Value representation, so the fold between them cannot be written in the substrate it is bridging into. This is a boundary item, not seed-shrink debt.\n\nWHAT IT REMOVED: gunbc.cli_dispatch_surface's scm row carried CliRefusesUnwired -- the compiler's own dispatch model recording that the scm command family computed answers no user could invoke. Every modeled scm entry was therefore specification without execution. With this route bound, gunbc scm log, status and init reach an operator, which is the only reason the .dag side of this change is worth anything.\n\nHAND-ITEM DELTA: +25 FROM THE MERGE BASE, ENUMERATED ABOVE -- five production declarations (CliWireClass, classify_cli_wire, CliWireOutcome, cli_wire_outcome, exit_status_for_class) and twenty test items across two test modules: cli_wire_outcome_tests with its five fns, and cli_wire_classify_tests with its five helper fns and seven test fns. The second module is counted here rather than waved through as 'just tests' for the same reason the relocation is counted: the roster's subject is hand-authored DECLARATIONS, and a test helper is one. Reproducible from the merge base, never the moving tip: git diff $(git merge-base origin/main HEAD)...HEAD -- src/v1/stage0/src/cli_run.rs src/v1/stage0/src/main.rs, which reports 449 insertions in cli_run.rs and 84 changed lines in main.rs. Two further .rs files differ and are GENERATED projections rather than hand-authored items -- gunbc_cli_dispatch_surface.rs and gunbc_rust_source_type_bindings.rs, each one line, both regenerated from their .dag authority -- so they are outside this roster's subject by construction, not by exemption. One of the five, exit_status_for_class, is a RELOCATION rather than new behaviour: its body was moved out of main.rs's exit_status_for, which now delegates to it, so the process-exit path gained no behaviour and was only made callable from the wire path beside it. It is counted because the roster counts hand-authored DECLARATIONS, and netting a relocation against an addition is the arithmetic gunbc.seed_growth_admission refuses.\n\nWHY THE CLASSIFIER AND THE OUTCOME ARE TWO ITEMS: the classification is a question about a value and the outcome is a decision about a process, and fusing them would have put the write-or-refuse decision inside a match arm in main.rs where no test could reach it. Splitting them is what made the five-case matrix authorable, including the two cases that carry the actual safety content -- an unprintable response REFUSES rather than printing nothing, and an exit_failure carrying status zero is refused on the wire path exactly as it already was on the process-exit path.", owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, trigger: "Delete CliWireClass, classify_cli_wire and their tests when the interpreter publishes a modeled projection of a returned Value against a declared type -- an inhabitance decision the substrate answers, rather than a hand-written field-by-field match on the host Value representation. Delete CliWireOutcome, cli_wire_outcome, exit_status_for_class and their tests when std models a process's standard output and exit status as a carrier the .dag side can produce directly, so a command entry returns the whole host effect and the seed only executes it. Both triggers name a CAPABILITY the substrate does not have today; neither is discharged by any artifact short of it, and in particular neither is discharged by moving this Rust to another file.", current_boundary: "gunbc.cli_wire_host_admission -> v1_compiler.cli_run cli_wire_outcome -> v1_compiler.main run_verb -> the host process stdout and exit status" From d9234ffb5cea6a1cc429f79bc961452443633515 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 07:51:17 +0000 Subject: [PATCH 15/21] Close the init TOCTOU with a create-only write, not a better check MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review 5085479276 on gunbc#9864, finding 1: initialize_repository established an absence from a directory listing and then called save_repository, which writes UNCONDITIONALLY. The decision was honest and the write was simply not conditioned on it, so an actor creating the file between the two made init truncate exactly the bytes it advertises that it refuses to touch. THIS IS NOT REPAIRABLE BY OBSERVING MORE CAREFULLY. Check-then-write is two acts with a gap, and re-observing only makes the gap smaller. The existence test and the creation have to BE one act, which is a property of open(2) with O_CREAT|O_EXCL and not something a fold over two modeled operations can express. Construction over validation at a boundary where validation structurally cannot win. So the substrate gains the operation rather than the caller gaining a check: extdeps.filesystem.filesystem_io WriteCreateNew, a FileWriteCreateNew verb in the emit stage, and one hand-authored realization. gunbc.scm.repository_save gains create_repository beside save_repository -- persisting a repository that exists and creating one that must not exist are different subjects, and the unconditional write stays correct for the first. NOT WriteOwnerOnly, WHICH ALREADY CALLS create_new. Its O_EXCL is incidental to setting a mode at creation -- meaningless on a path that already exists -- and is not a contract. Owner-only MODE and create-only EXISTENCE are independent facts; a caller taking create-only from it would silently also take 0600 and would break the day owner-only stopped needing O_EXCL. Reusing a realization detail in place of a modeled fact is the inversion §3 names, and the review rejected it explicitly before this landed. THE REFUSAL DOES NOT CLASSIFY ITSELF, and that is deliberate. It carries the host's error verbatim and does not report whether the cause was "already existed" or "permission denied": the transport's channels cannot separate them, and deciding it by matching the error TEXT would be a heuristic standing in for an observation. The caller learns what it needs in order to refuse and does not learn a classification nothing measured. That gap has its own next-rung trigger. Executed, and the mutation is the original defect rather than an invented one: replacing create_new with create+truncate -- what the code did before -- takes create_new_refuses_a_path_that_already_exists_and_leaves_its_bytes red while the positive control stays green. The load-bearing assertion is that the EXISTING BYTES SURVIVE, not that an error is returned: a write that truncated and then reported failure would satisfy a weaker test and still have destroyed the file. Seed growth is receipted in gunbc.filesystem_create_new_admission and rostered, with a trigger naming the capability (creation exclusivity declarable as a property of a write, with the realization deriving the flags) rather than an artifact. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/extdeps/filesystem/filesystem_io.dag | 34 ++++++ dag/gunbc/filesystem_create_new_admission.dag | 43 ++++++++ dag/gunbc/scm/init.dag | 16 ++- dag/gunbc/scm/repository_save.dag | 35 ++++++ dag/gunbc/seed_growth_admission.dag | 2 + src/v1/05_emit.dag | 10 +- src/v1/05_emit_rust.dag | 5 +- src/v1/stage0/src/v1_interpreter.rs | 101 +++++++++++++++++- 8 files changed, 238 insertions(+), 8 deletions(-) create mode 100644 dag/gunbc/filesystem_create_new_admission.dag diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index 675cd201b07..e3316ce6f71 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -354,6 +354,40 @@ service Filesystem { transport file { path: "{path}", verb: "write_owner_only" } } + // CREATE-ONLY, AND IT IS A DIFFERENT FACT FROM OWNER-ONLY. WriteOwnerOnly's realization happens to + // use create_new(true), because a mode set at creation is meaningless on a path that already + // exists -- but that is a property of ITS realization, not a contract anyone may depend on. Owner- + // only MODE and create-only EXISTENCE are independent facts, and reusing one to obtain the other is + // a realization detail standing where a modeled fact belongs (DESIGN section 3). A caller that + // wanted create-only and got it from WriteOwnerOnly would also silently get 0600, and would break + // the day owner-only stopped needing O_EXCL. + // + // WHAT THIS CLOSES, AND WHY A CHECK COULD NOT. Observing that a path is absent and then writing to + // it is two operations with a gap between them: an actor creating the file in the gap makes the + // write truncate exactly the bytes the observation was taken to protect. No amount of re-observing + // removes the gap -- the check and the write are still not one act. O_CREAT|O_EXCL makes the + // EXISTENCE TEST AND THE CREATION the same syscall, so the race has no window rather than a small + // one. This is construction over validation (section 5) at a boundary where validation cannot win. + // + // THE REFUSAL DOES NOT CLASSIFY ITSELF, ON PURPOSE. `error` carries the host's message verbatim and + // this operation does NOT report whether the refusal was "already existed" or "permission denied": + // the channels available here cannot separate them, and deciding it by matching on the error TEXT + // would be a heuristic standing in for an observation -- the smuggled-confidence shape section 5 + // names. A caller therefore learns that the create did not happen and why the host said so, which + // is what it needs to refuse; it does not learn a classification nothing measured. + // NEXT-RUNG TRIGGER: a modeled already-exists channel on the file transport, at which point the + // race and the permission failure become separate arms and this note is deleted. + operation WriteCreateNew { + input { path: String, content: String } + output { + success: Bool from "write_success" + bytes_written: Int from "bytes_written" + path: String from "path" + error: String from "error" + } + transport file { path: "{path}", verb: "write_create_new" } + } + operation Read { input { path: String } output { diff --git a/dag/gunbc/filesystem_create_new_admission.dag b/dag/gunbc/filesystem_create_new_admission.dag new file mode 100644 index 00000000000..2ee12d6e651 --- /dev/null +++ b/dag/gunbc/filesystem_create_new_admission.dag @@ -0,0 +1,43 @@ +module gunbc.filesystem_create_new_admission + +// WHY THIS SEED ITEM EXISTS: A RACE CANNOT BE CLOSED FROM ABOVE THE HOST. +// +// Establishing that a path is absent and then writing to it is two operations with a gap between +// them, and an actor creating the file in that gap makes the write truncate exactly the bytes the +// observation was taken to protect. No amount of re-observing removes the gap, because the check and +// the write remain two acts. The only construction that closes it is one in which the existence test +// and the creation are THE SAME operation, and that is a property of the host's open(2) call -- +// O_CREAT|O_EXCL -- not something a .dag fold over two separate operations can express. +// +// So the substrate gains a modeled operation (extdeps.filesystem.filesystem_io WriteCreateNew) whose +// realization the seed must provide, exactly as it provides Write, Read, Delete and List. This is a +// boundary item and not seed-shrink debt: the fact being realized is a syscall's atomicity. +// +// WHY NOT REUSE WriteOwnerOnly, WHICH ALREADY CALLS create_new. Because its create_new is INCIDENTAL +// to owner-only mode -- a creation-time mode is meaningless on a path that already exists -- and not +// a contract anyone may depend on. Owner-only MODE and create-only EXISTENCE are independent facts. +// A caller that obtained create-only from it would silently also get 0600, and would break the day +// owner-only stopped needing O_EXCL. Reusing a realization detail in place of a modeled fact is the +// layer inversion DESIGN section 3 names, and it was explicitly rejected in review 5085479276 on +// gunbc#9864 before this row was written. +import std.symbols { Ascii } +import gunbc.roadmap_model { RoadmapNodeId } +import gunbc.seed_growth { + SeedGrowthJustification, + DeclarationRef, + WholeDeclaration +} + +data filesystem_create_new_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { + hand_authored_declarations: [ + DeclarationRef { + module_path: "v1_compiler.v1_interpreter", + decl_name: "write_file_create_new", + field: WholeDeclaration + } + ], + reason: "WHY RUST IS STILL NEEDED HERE: the fact being realized is the ATOMICITY of a single host syscall. O_CREAT|O_EXCL makes the existence test and the file's creation one indivisible act, and there is no composition of the modeled Read, List and Write operations that reproduces it -- any .dag expression of 'check then write' is two operations with a gap, which is the exact defect this operation exists to close. One hand-authored function, write_file_create_new, is the whole seed side.\n\nWHAT IT REMOVED: gunbc.scm.init established an absence from a directory listing and then called save_repository, which writes unconditionally. The decision was honest; the write was simply not conditioned on it, so a racing creation made init truncate the bytes it advertised that it refuses to touch. That is a destructive fail-open at a boundary whose whole purpose is refusing to destroy, and it was reported by review 5085479276 on gunbc#9864. init now writes through create_repository, so the refusal is the write's own.\n\nWHAT IS DELIBERATELY NOT MODELED, stated rather than left for a reader to discover: the refusal does not classify itself. The operation reports that the create did not happen and carries the host's error verbatim; it does NOT report whether the cause was 'the path already existed' or 'permission denied'. The output channels available to the file transport cannot separate those, and deciding between them by matching on the error TEXT would be a heuristic standing in for an observation -- the smuggled confidence DESIGN section 5 forbids. A caller learns what it needs in order to refuse, and does not learn a classification nothing measured.\n\nWHY NOT write_file_owner_only: its create_new is incidental to setting a mode at creation, not a contract. Owner-only mode and create-only existence are independent facts, and a caller taking create-only from it would silently also take 0600.", + owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, + trigger: "Delete write_file_create_new when the substrate models FILE CREATION EXCLUSIVITY as a declarable property of a write rather than as a distinct transport verb -- that is, when an operation can state 'this write must not replace an existing object' and the realization layer derives the open flags from that statement for every target it emits to, rather than each host binding hand-writing the flag combination. That names the CAPABILITY and not an artifact: moving this function to another file, or adding a second verb beside it, discharges nothing. A SEPARATE and narrower trigger governs the self-classification gap above: a modeled already-exists channel on the file transport, at which point the race and the permission failure become distinct arms and the operation stops carrying an unclassified host string.", + current_boundary: "gunbc.filesystem_create_new_admission -> extdeps.filesystem.filesystem_io WriteCreateNew -> v1_compiler.v1_interpreter write_file_create_new -> the host open(2) with O_CREAT|O_EXCL" +} diff --git a/dag/gunbc/scm/init.dag b/dag/gunbc/scm/init.dag index 326af680ce8..1c6fe3516df 100644 --- a/dag/gunbc/scm/init.dag +++ b/dag/gunbc/scm/init.dag @@ -10,6 +10,15 @@ module gunbc.scm.init // non-fail-closed failure arm is a hard reject regardless of what else it delivers, and an // annotation is not a refusal. External review was right to block it. // +// AND THE DECISION ALONE WAS STILL NOT ENOUGH, WHICH IS THE THIRD TIME THIS VERB WAS WRONG. Deciding +// from a listing and then calling save_repository is two operations with a gap: an actor creating the +// file between the observation and the write makes the save truncate exactly the bytes the decision +// was taken to protect. The decision was honest and the write was simply not conditioned on it. That +// is a TOCTOU, review 5085479276 on gunbc#9864 named it, and it is not repairable by observing more +// carefully -- the check and the write are still not one act. The write now goes through +// `create_repository`, whose Filesystem.WriteCreateNew makes the existence test and the creation one +// syscall, so the race has no window rather than a narrow one. +// // AND THE SECOND REVISION WAS STILL FAIL-OPEN, WHICH IS WHY THIS ONE DOES NOT READ FIRST. It // proceeded on `RepositoryFileUnreadable`, reasoning that a file it could not read was one the // write could not replace either. That reasoning is a guess about the host's permission model, not @@ -23,7 +32,8 @@ module gunbc.scm.init // entry, and the read is consulted only as the second half of `filesystem_file_observation`'s fold. // The four arms are the four actions: nothing is there, so write; bytes are there, so refuse and say // which kind; the observation could not be made, so refuse; the two observations disagree, so refuse. -// Only the first arm reaches `save_repository`. +// Only the first arm reaches `create_repository`, and that call refuses on its own if the path +// appeared in the meantime. // // THIS IS WHY THE ENTRY TAKES A DIRECTORY AND A NAME RATHER THAN A PATH. Presence is a fact about a // directory listing, so the listing's subject has to be an argument and not something recovered by @@ -59,7 +69,7 @@ import gunbc.scm.repository_envelope { RepositoryDecoded, RepositoryDecodeRefused } -import gunbc.scm.repository_save { RepositorySave, save_repository } +import gunbc.scm.repository_save { RepositorySave, create_repository } // THE ARMS ARE THE ANSWER. There is no `initialized: Bool` beside a save outcome: a value whose // flag disagreed with its shape would have a spelling, and the refusals are distinguished because @@ -149,7 +159,7 @@ fn initialize_repository_at( ) { ScmInitDecided { cause: c } => ScmInitRefused { cause: c } ScmInitMayCreate(_) => - ScmInitialized { save: save_repository(path: path, repo: empty_repository()) } + ScmInitialized { save: create_repository(path: path, repo: empty_repository()) } } } diff --git a/dag/gunbc/scm/repository_save.dag b/dag/gunbc/scm/repository_save.dag index b1f54e0367f..cbf11d4f22e 100644 --- a/dag/gunbc/scm/repository_save.dag +++ b/dag/gunbc/scm/repository_save.dag @@ -84,6 +84,41 @@ type RepositorySave | RepositoryFileUnwritable { path: String, error: String } | RepositoryWriteByteCountUnrepresentable { path: String, reported: Int } +// CREATING A REPOSITORY IS NOT SAVING ONE, AND THE DIFFERENCE IS THE WRITE ITSELF. +// +// save_repository writes unconditionally, which is correct for its subject: persisting a repository +// that already exists must replace the bytes that are there. Initialization is the opposite subject +// -- it must happen ONLY where nothing exists -- and for a long time it was expressed as "observe an +// absence, then call save_repository". That is two operations with a gap, and an actor creating the +// file in the gap makes the save truncate exactly the bytes the observation was taken to protect. +// The observation was honest; the write was not conditioned on it. +// +// No re-observation closes that. The fix is that the existence test and the creation become ONE act, +// which is what Filesystem.WriteCreateNew provides -- so this function refuses a path that exists +// rather than checking whether it exists. Construction over validation (DESIGN section 5) at a +// boundary where validation structurally cannot win. +// +// The refusal reuses RepositoryFileUnwritable rather than minting a create-specific arm: the caller's +// remedy is the same -- the bytes are not yours to write and the host says why -- and the error text +// is the host's own. A second arm would be a second spelling of one outcome (section 3), and one that +// classified the cause from the error TEXT would be a heuristic standing in for an observation. +fn create_repository(path: String, repo: RepositoryEnvelope) -> RepositorySave { + match encode_repository_checked(repo: repo) { + RepositoryEncodeRefused { cause: cause } => + RepositorySaveRefusedByCodec { path: path, cause: cause } + RepositoryEncoded { value: v } => { + let write = Filesystem.WriteCreateNew(path: path, content: serialize_json(v: v)) + if !write.success { + RepositoryFileUnwritable { path: path, error: write.error } + } else if write.bytes_written < 0 { + RepositoryWriteByteCountUnrepresentable { path: path, reported: write.bytes_written } + } else { + RepositorySaved { path: path, written: byte_size(count: nat_magnitude(a: write.bytes_written)) } + } + } + } +} + fn save_repository(path: String, repo: RepositoryEnvelope) -> RepositorySave { match encode_repository_checked(repo: repo) { RepositoryEncodeRefused { cause: cause } => diff --git a/dag/gunbc/seed_growth_admission.dag b/dag/gunbc/seed_growth_admission.dag index 7ffa2f94a4d..a739106c29e 100644 --- a/dag/gunbc/seed_growth_admission.dag +++ b/dag/gunbc/seed_growth_admission.dag @@ -46,6 +46,7 @@ import gunbc.capability_origin { } import gunbc.rust_item_identity { RustItemIdentity, rust_item_identity_key } import gunbc.cli_wire_host_admission { cli_wire_host_seed_growth_justification } +import gunbc.filesystem_create_new_admission { filesystem_create_new_seed_growth_justification } import gunbc.seed_growth { SeedGrowthJustification } import gunbc.stage0_rust_host_observation { stage0_rust_observation_seed_growth_justification } import gunbc.floor_non_verdict_enrollment { floor_non_verdict_seed_growth_justification } @@ -219,6 +220,7 @@ fn seed_growth_justification_roster() -> List { regen_convergence_seed_growth_justification, decl_facts_shared_memo_seed_growth_justification, cli_wire_host_seed_growth_justification, + filesystem_create_new_seed_growth_justification, required_lane_judgment_seed_growth_justification ] } diff --git a/src/v1/05_emit.dag b/src/v1/05_emit.dag index 1f97d9930f6..b3a2759b041 100644 --- a/src/v1/05_emit.dag +++ b/src/v1/05_emit.dag @@ -1038,6 +1038,7 @@ type FileVerb = FileRead | FileWrite | FileWriteOwnerOnly + | FileWriteCreateNew | FileDelete | FileList @@ -1121,13 +1122,14 @@ fn file_result_channel_of_key(key: String) -> FileResultChannel? { // put a fact extdeps owns into the compiler (section 3). // // Total by construction over the admitted set: `file_emission_verb_refusal` has -// already rejected any verb that is not delete, list or write_owner_only, so the +// already rejected any verb that is not delete, list, write_owner_only or write_create_new, so the // final arm is the floor beneath that wall rather than a second opinion. fn bind_file_verb(t: Node, op_node: Node, source_indices: Map) -> FileVerb { match file_transport_declared_verb(t: t, source_indices: source_indices) { Present { value: v } => if v == file_transport_verb_delete { FileDelete } else if v == file_transport_verb_list { FileList } + else if v == file_transport_verb_write_create_new { FileWriteCreateNew } else { FileWriteOwnerOnly } Absent => if file_operation_has_content_input(op_node: op_node, source_indices: source_indices) { FileWrite } @@ -2151,7 +2153,7 @@ fn file_emission_refusal_fact(refusal: FileEmissionRefusal) -> String { "' has no file realization handler, so no operation carrying `transport file` is emitted for it") FileVerbNotModeled { verb: v } => concat("file transport verb '", v, - "' is not a modeled action -- the modeled verbs are delete, list and write_owner_only, and an absent verb means write when the operation declares a `content` input and read otherwise") + "' is not a modeled action -- the modeled verbs are delete, list, write_owner_only and write_create_new, and an absent verb means write when the operation declares a `content` input and read otherwise") FilePathNotStaticallyRenderable => "the file transport `path:` must be a string literal or a string interpolation over the operation inputs; no other expression shape has a rendering" FileWriteMissingContentInput { verb: v } => @@ -2169,6 +2171,8 @@ data file_transport_verb_delete: String = "delete" data file_transport_verb_list: String = "list" data file_transport_verb_write_owner_only: String = "write_owner_only" +data file_transport_verb_write_create_new: String = "write_create_new" + fn file_transport_declared_verb(t: Node, source_indices: Map) -> String? { match transport_verb(t: t, source_indices: source_indices) { Present { value: v } => match v.expr_data { @@ -2234,7 +2238,7 @@ fn file_emission_verb_refusal(op_node: Node, verb: String?, source_indices: Map< Present { value: v } => if v == file_transport_verb_delete || v == file_transport_verb_list { none - } else if v == file_transport_verb_write_owner_only { + } else if v == file_transport_verb_write_owner_only || v == file_transport_verb_write_create_new { if file_operation_has_content_input(op_node: op_node, source_indices: source_indices) { none } else { Present { value: FileWriteMissingContentInput { verb: v } } } } else { diff --git a/src/v1/05_emit_rust.dag b/src/v1/05_emit_rust.dag index 2f90eafde7b..cf4b4f8c823 100644 --- a/src/v1/05_emit_rust.dag +++ b/src/v1/05_emit_rust.dag @@ -205,7 +205,7 @@ import v1.compiler.emit { child_from_key, unwrap_single_field_product, BoundOperation, RestBound, ShellBound, LocalBound, FileBound, BindingRefused, bind_operation_transport, transport_binding_refusal_fact, - FileVerb, FileRead, FileWrite, FileWriteOwnerOnly, FileDelete, FileList, + FileVerb, FileRead, FileWrite, FileWriteOwnerOnly, FileWriteCreateNew, FileDelete, FileList, FileResultField, FileResultChannel, FileChanSuccess, FileChanByteCount, FileChanPath, FileChanError, FileChanContent } @@ -14309,6 +14309,7 @@ fn file_verb_action_expr(verb: FileVerb) -> String { FileRead => file_read_match_expr FileWrite => file_write_expr FileWriteOwnerOnly => file_write_owner_only_expr + FileWriteCreateNew => file_write_create_new_expr FileDelete => file_delete_match_expr FileList => file_list_match_expr } @@ -14368,6 +14369,8 @@ data file_list_match_expr: String = "match std::fs::read_dir(&file_path) {\n data file_write_expr: String = "{\n let payload_bytes = content.len() as i64;\n match std::fs::write(&file_path, content.as_bytes()) {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(write_err) => (false, String::new(), format!(\"{}\", write_err), 0i64),\n }\n};" +data file_write_create_new_expr: String = "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let mut create_new_file = std::fs::OpenOptions::new().write(true).create_new(true).open(&file_path)?;\n create_new_file.write_all(content.as_bytes())?;\n Ok(())\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};" + data file_write_owner_only_expr: String = "{\n let payload_bytes = content.len() as i64;\n let owner_only_result = (|| -> std::io::Result<()> {\n #[cfg(unix)]\n {\n use std::io::Write;\n use std::os::unix::fs::OpenOptionsExt;\n let mut owner_only_file = std::fs::OpenOptions::new().write(true).create_new(true).mode(0o600).open(&file_path)?;\n owner_only_file.write_all(content.as_bytes())?;\n return Ok(());\n }\n #[cfg(not(unix))]\n {\n return Err(std::io::Error::new(std::io::ErrorKind::Unsupported, \"write_owner_only refused: owner-only mode-at-creation is unavailable on this platform\"));\n }\n })();\n match owner_only_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(owner_only_err) => (false, String::new(), format!(\"{}\", owner_only_err), 0i64),\n }\n};" // TOTAL BY CONSTRUCTION, and this is where the climb is visible. #8929 took the diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index cbf25b4ab2c..75f8947aa2f 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -11911,6 +11911,67 @@ fn write_file_owner_only(path: &str, content: &[u8]) -> std::io::Result<()> { } } +/// Create-only write: the existence test and the creation are ONE syscall (O_CREAT|O_EXCL), so a +/// path that appears between an observation and this call refuses instead of being truncated. +/// +/// Deliberately NOT `write_file_owner_only` with a different name. That function sets mode 0600 at +/// creation and uses `create_new` because a creation-time mode is meaningless on an existing path -- +/// its O_EXCL is incidental to owner-only mode, not a contract. Owner-only MODE and create-only +/// EXISTENCE are independent facts; a caller that obtained create-only from it would silently also +/// get 0600, and would break if owner-only ever stopped needing O_EXCL. This is portable and sets no +/// mode, because setting one would be the same conflation in reverse. +fn write_file_create_new(path: &str, content: &[u8]) -> std::io::Result<()> { + use std::fs::OpenOptions; + use std::io::Write; + let mut file = OpenOptions::new().write(true).create_new(true).open(path)?; + file.write_all(content)?; + Ok(()) +} + +// ------------------------------------------------------------------------------------------------ +// THE PRIMITIVE'S OWN EVIDENCE. gunbc.scm.init's witnesses cover the DECISION -- which observation +// arms may write -- and cannot reach this, because the decision is pure and the race lives in the +// write. These two cells are the write's half: an existing path refuses AND KEEPS ITS BYTES, and an +// absent one is created. Without the second, the first is satisfied by a function that never writes. +// ------------------------------------------------------------------------------------------------ +#[cfg(test)] +mod write_file_create_new_tests { + #[test] + fn create_new_refuses_a_path_that_already_exists_and_leaves_its_bytes() { + let dir = std::env::temp_dir().join(format!("gunbc-create-new-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("temp dir"); + let path = dir.join("repo.json"); + std::fs::write(&path, b"SOMEONE ELSE'S BYTES").expect("seed the path"); + + let err = super::write_file_create_new(path.to_str().unwrap(), b"a fresh repository") + .expect_err("a path that exists must refuse, not be truncated"); + assert_eq!(err.kind(), std::io::ErrorKind::AlreadyExists); + + // THE ASSERTION THAT CARRIES THE FINDING. A refusal that had already truncated would still + // return an error; what makes this a fix rather than a report is that the bytes survive. + let after = std::fs::read(&path).expect("the file is still there"); + assert_eq!( + after, b"SOMEONE ELSE'S BYTES", + "the existing bytes must be untouched by a refused create" + ); + std::fs::remove_dir_all(&dir).ok(); + } + + #[test] + fn create_new_writes_when_nothing_is_there() { + let dir = std::env::temp_dir().join(format!("gunbc-create-new-ok-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("temp dir"); + let path = dir.join("repo.json"); + super::write_file_create_new(path.to_str().unwrap(), b"a fresh repository") + .expect("an absent path is created"); + assert_eq!( + std::fs::read(&path).expect("written"), + b"a fresh repository" + ); + std::fs::remove_dir_all(&dir).ok(); + } +} + struct FileResult { success: bool, byte_count: i64, @@ -12044,10 +12105,48 @@ fn dispatch_file( }), }; } + "write_create_new" => { + let content = match param_env.lookup(ctx.sym("content")) { + Some(v) => format!("{}", v), + None => { + return Err(InterpError::TypeError { + msg: format!( + "file write_create_new operation missing `content` argument for {}", + path + ), + }) + } + }; + let byte_count = content.len() as i64; + trace_emit( + OutputChannel::ShellTrace, + &format!("[file] write_create_new {} ({} bytes)", path, byte_count), + ); + return match write_file_create_new(&path, content.as_bytes()) { + Ok(()) => Ok(FileResult { + success: true, + byte_count, + path, + error: String::new(), + content: String::new(), + }), + // The refusal carries the host's message verbatim and does NOT classify itself. + // Deciding "already existed" from the error TEXT would be a heuristic standing in + // for an observation; the caller learns the create did not happen and why the + // host said so, which is what it needs to refuse. + Err(e) => Ok(FileResult { + success: false, + byte_count: 0, + path, + error: format!("{}", e), + content: String::new(), + }), + }; + } other => { return Err(InterpError::TypeError { msg: format!( - "file transport verb '{other}' is not a known action (delete, list, write_owner_only)" + "file transport verb '{other}' is not a known action (delete, list, write_owner_only, write_create_new)" ), }) } From b1f9254dc1632142824436dbec3d8c7063ed59df Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 08:30:39 +0000 Subject: [PATCH 16/21] Move the create-only rationale to module-item grain, and fix its imports MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two defects my own build lane caught rather than a reviewer. The WriteCreateNew annotation sat INSIDE the service body, which §4c refuses: only module-item grain is modeled, and an operation lives inside a service's declaration. It now sits above the service that contains it, and says why it is there rather than on the operation it describes -- so the next author does not repeat the move. The seed-growth row imported DeclarationRef and WholeDeclaration from gunbc.seed_growth, which does not export them; std.decl_ref does. Build lane green: regen first_generation_equal=true, generated-artifact 35/35, 0 drifted. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/extdeps/filesystem/filesystem_io.dag | 50 ++++++++++--------- dag/gunbc/filesystem_create_new_admission.dag | 9 ++-- src/v1/stage0/src/v1_compiler_emit.rs | 24 +++++++-- src/v1/stage0/src/v1_compiler_emit_rust.rs | 12 ++++- 4 files changed, 63 insertions(+), 32 deletions(-) diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index e3316ce6f71..2304e05b1fe 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -330,6 +330,33 @@ fn filesystem_established_absence_detail(absence: FilesystemEstablishedAbsence) data filesystem_absence_establishment_adoption_standing: String = "RUNG: structurally guaranteed for the consumers that route through filesystem_file_observation, on the source-to-.dag acceptance path only, and MITIGATABLE NOWHERE ELSE -- the raw Filesystem.Read and Filesystem.List operations stay callable, so a module that has not adopted the carrier can still write the conflation. This row states the unconverted population at identity grain rather than as a count, because a count is not a plan and a one-sided ratchet over a number measured on the current tree is the oracle section 5 rejects. SUBJECT: a site that concludes ABSENCE, NOT-PRESENT or a dropped element from a FAILED read or a FAILED boolean path test, rather than from a listing that succeeded. It is not every Filesystem.Read consumer -- most read a file they already know exists, and those are the separate filesystem_read_outcome adoption population above. ENUMERATED SITES, each one read rather than pattern-matched, on origin/main at the head this row lands against, with the two converted by the change that lands this row already removed (gunbc.roadmap_verification_receipt current_verification_selection_observe and exact_verification_receipt_source_read, and gunbc.devboot.build read_text_file): gunbc.host_effect_nbd_proxy_serve host_effect_nbd_proxy_serve_read_session_token (read refusal answers Absent, and an empty content does too); gunbc.fleet_converge_plan_cli observe_cap_members_wet (a cap member whose dropin could not be read is DROPPED from the observed list, so the converge plan is computed over a silently narrowed population); v2.workflow.product_receipt_stage run_product_receipt_stage (an unreadable manifest answers ArtifactIdentityAbsent { ProducerReportedNoArtifact }, attributing to the producer a report it never made); tools.merge_admission_walk read_tested_subject and read_floor_receipt (a read refusal answers the Optional's absent arm); gunbc.codex_supervised_turn codex_supervised_turn_generation_observation (GenerationAbsent is concluded from shell.Test.IsFile answering false. THIS ROW IS CLASSIFIED FROM THE PRODUCER RATHER THAN FROM THE CALL SITE, on a caution from the lane that shipped this defect today: a predicate whose job is to answer the presence question would not belong here. extdeps.shell Test.IsFile is `test -f` with its own declared exit table reading `1 => Path is missing or not a regular file`, so ONE exit code carries missing, wrong-kind, and -- since `test -f` is false when the parent directory cannot be searched -- could-not-look. It answers false on an unreadable-but-present path, so it is the same defect with a different producer, and it is the construction gunbc.fabric_cell_acquire retired for exactly this reason); tools.opaque_realization_census declaration_body_standing (a file that could not be read leaves the fold state unchanged, so it is indistinguishable from a file that did not hold the declaration). WHAT IS DELIBERATELY NOT ON THE LIST: gunbc.roadmap_belt_actuate belt_read_or_empty, whose collapse is scoped and argued in belt_read_or_empty_scope_note -- both branches take the same action at every remaining caller -- and gunbc.fabric_cell_acquire, which already establishes absence from the parent enumeration through its own four-state observation and would gain nothing but a second spelling. MONOTONE DIRECTION: the roster above may only shrink. A row leaves it when the site routes through filesystem_file_observation or filesystem_entry_presence, or when the site is deleted; a NEW site of this shape is a defect to repair rather than a row to add. NEXT-RUNG TRIGGER, and it names the capability rather than an artifact: the raw List and Read result projections cease to be reachable outside this module's folds, so a consumer cannot spell the conflation at all -- at which point the enumeration above has no subject and this row is deleted. That is the same trigger filesystem_read_outcome_adoption_standing carries, one question further in: it asks that every read projection be folded, this asks that every ABSENCE be established." +// WriteCreateNew: CREATE-ONLY IS A DIFFERENT FACT FROM OWNER-ONLY, and this annotation sits here +// rather than above the operation because only module-item grain is modeled (DESIGN section 4c) -- +// an operation lives inside this service's body, so the rationale for one attaches to the +// declaration that contains it. +// +// WriteOwnerOnly's realization happens to use create_new(true), because a mode set at creation is +// meaningless on a path that already exists. That is a property of ITS realization, not a contract +// anyone may depend on: owner-only MODE and create-only EXISTENCE are independent facts, and reusing +// one to obtain the other is a realization detail standing where a modeled fact belongs (section 3). +// A caller that wanted create-only and took it from WriteOwnerOnly would also silently get 0600, and +// would break the day owner-only stopped needing O_EXCL. +// +// WHAT IT CLOSES, AND WHY A CHECK COULD NOT. Observing that a path is absent and then writing to it +// is two operations with a gap: an actor creating the file in the gap makes the write truncate +// exactly the bytes the observation was taken to protect. No amount of re-observing removes the gap, +// because the check and the write are still not one act. O_CREAT|O_EXCL makes the EXISTENCE TEST AND +// THE CREATION the same syscall, so the race has no window rather than a narrow one. Construction +// over validation (section 5) at a boundary where validation cannot win. +// +// THE REFUSAL DOES NOT CLASSIFY ITSELF, ON PURPOSE. `error` carries the host's message verbatim and +// the operation does NOT report whether the refusal was "already existed" or "permission denied": +// the channels available here cannot separate them, and deciding it by matching on the error TEXT +// would be a heuristic standing in for an observation -- the smuggled-confidence shape section 5 +// names. A caller learns that the create did not happen and why the host said so, which is what it +// needs in order to refuse; it does not learn a classification nothing measured. +// NEXT-RUNG TRIGGER: a modeled already-exists channel on the file transport, at which point the race +// and the permission failure become separate arms and this paragraph is deleted. service Filesystem { operation Write { @@ -354,29 +381,6 @@ service Filesystem { transport file { path: "{path}", verb: "write_owner_only" } } - // CREATE-ONLY, AND IT IS A DIFFERENT FACT FROM OWNER-ONLY. WriteOwnerOnly's realization happens to - // use create_new(true), because a mode set at creation is meaningless on a path that already - // exists -- but that is a property of ITS realization, not a contract anyone may depend on. Owner- - // only MODE and create-only EXISTENCE are independent facts, and reusing one to obtain the other is - // a realization detail standing where a modeled fact belongs (DESIGN section 3). A caller that - // wanted create-only and got it from WriteOwnerOnly would also silently get 0600, and would break - // the day owner-only stopped needing O_EXCL. - // - // WHAT THIS CLOSES, AND WHY A CHECK COULD NOT. Observing that a path is absent and then writing to - // it is two operations with a gap between them: an actor creating the file in the gap makes the - // write truncate exactly the bytes the observation was taken to protect. No amount of re-observing - // removes the gap -- the check and the write are still not one act. O_CREAT|O_EXCL makes the - // EXISTENCE TEST AND THE CREATION the same syscall, so the race has no window rather than a small - // one. This is construction over validation (section 5) at a boundary where validation cannot win. - // - // THE REFUSAL DOES NOT CLASSIFY ITSELF, ON PURPOSE. `error` carries the host's message verbatim and - // this operation does NOT report whether the refusal was "already existed" or "permission denied": - // the channels available here cannot separate them, and deciding it by matching on the error TEXT - // would be a heuristic standing in for an observation -- the smuggled-confidence shape section 5 - // names. A caller therefore learns that the create did not happen and why the host said so, which - // is what it needs to refuse; it does not learn a classification nothing measured. - // NEXT-RUNG TRIGGER: a modeled already-exists channel on the file transport, at which point the - // race and the permission failure become separate arms and this note is deleted. operation WriteCreateNew { input { path: String, content: String } output { diff --git a/dag/gunbc/filesystem_create_new_admission.dag b/dag/gunbc/filesystem_create_new_admission.dag index 2ee12d6e651..1b84edd8df3 100644 --- a/dag/gunbc/filesystem_create_new_admission.dag +++ b/dag/gunbc/filesystem_create_new_admission.dag @@ -22,11 +22,10 @@ module gunbc.filesystem_create_new_admission // gunbc#9864 before this row was written. import std.symbols { Ascii } import gunbc.roadmap_model { RoadmapNodeId } -import gunbc.seed_growth { - SeedGrowthJustification, - DeclarationRef, - WholeDeclaration -} +import gunbc.seed_growth { SeedGrowthJustification } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import std.types { String } +import v2.std.collection { List } data filesystem_create_new_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { hand_authored_declarations: [ diff --git a/src/v1/stage0/src/v1_compiler_emit.rs b/src/v1/stage0/src/v1_compiler_emit.rs index f6350a85a19..6350932d452 100644 --- a/src/v1/stage0/src/v1_compiler_emit.rs +++ b/src/v1/stage0/src/v1_compiler_emit.rs @@ -2411,6 +2411,7 @@ pub enum FileVerb { FileRead, FileWrite, FileWriteOwnerOnly, + FileWriteCreateNew, FileDelete, FileList, } @@ -2523,7 +2524,11 @@ pub fn bind_file_verb( if (v.clone() == file_transport_verb_list()) { FileVerb::FileList } else { - FileVerb::FileWriteOwnerOnly + if (v.clone() == file_transport_verb_write_create_new()) { + FileVerb::FileWriteCreateNew + } else { + FileVerb::FileWriteOwnerOnly + } } } } @@ -4701,7 +4706,7 @@ pub enum FileEmissionRefusal { pub fn file_emission_refusal_fact(refusal: Rc) -> String { match (*refusal.clone()).clone() { FileEmissionRefusal::FileTargetNotModeled { target_name: t, .. } => v1_rt::concat(v1_rt::concat("file transport emission is modeled for the rust target only; target '".to_string(), t.clone()), "' has no file realization handler, so no operation carrying `transport file` is emitted for it".to_string()), - FileEmissionRefusal::FileVerbNotModeled { verb: v, .. } => v1_rt::concat(v1_rt::concat("file transport verb '".to_string(), v.clone()), "' is not a modeled action -- the modeled verbs are delete, list and write_owner_only, and an absent verb means write when the operation declares a `content` input and read otherwise".to_string()), + FileEmissionRefusal::FileVerbNotModeled { verb: v, .. } => v1_rt::concat(v1_rt::concat("file transport verb '".to_string(), v.clone()), "' is not a modeled action -- the modeled verbs are delete, list, write_owner_only and write_create_new, and an absent verb means write when the operation declares a `content` input and read otherwise".to_string()), FileEmissionRefusal::FilePathNotStaticallyRenderable => "the file transport `path:` must be a string literal or a string interpolation over the operation inputs; no other expression shape has a rendering".to_string(), FileEmissionRefusal::FileWriteMissingContentInput { verb: v, .. } => v1_rt::concat(v1_rt::concat("file transport verb '".to_string(), v.clone()), "' writes a payload, and the operation declares no `content` input to write -- the payload is an input to the operation, never a value the emitter may invent".to_string()), FileEmissionRefusal::FileOutputKeyNotModeled { key: k, .. } => v1_rt::concat(v1_rt::concat("file transport output key '".to_string(), k.clone()), "' has no modeled channel -- the modeled channels are write_success, read_success, delete_success, list_success, success, bytes_written, bytes, byte_count, path, error, content and entries".to_string()), @@ -4736,6 +4741,15 @@ pub fn file_transport_verb_write_owner_only() -> String { CACHED.with(|c: &String| c.clone()) } +pub fn file_transport_verb_write_create_new() -> String { + thread_local! { + static CACHED: String = { + "write_create_new".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + pub fn file_transport_declared_verb( t: Rc, source_indices: Rc>>, @@ -4853,7 +4867,9 @@ pub fn file_emission_verb_refusal( { std::option::Option::None } else { - if (v.clone() == file_transport_verb_write_owner_only()) { + if ((v.clone() == file_transport_verb_write_owner_only()) + || (v.clone() == file_transport_verb_write_create_new())) + { if file_operation_has_content_input(op_node.clone(), source_indices.clone()) { std::option::Option::None } else { @@ -7484,6 +7500,8 @@ pub struct FileWrite; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct FileWriteOwnerOnly; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct FileWriteCreateNew; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct FileDelete; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct FileList; diff --git a/src/v1/stage0/src/v1_compiler_emit_rust.rs b/src/v1/stage0/src/v1_compiler_emit_rust.rs index 2ac0280fecc..4c225f9872e 100644 --- a/src/v1/stage0/src/v1_compiler_emit_rust.rs +++ b/src/v1/stage0/src/v1_compiler_emit_rust.rs @@ -113,7 +113,7 @@ use crate::v1_compiler_emit::FileResultChannel::{ FileChanByteCount, FileChanContent, FileChanError, FileChanPath, FileChanSuccess, }; use crate::v1_compiler_emit::FileVerb::{ - FileDelete, FileList, FileRead, FileWrite, FileWriteOwnerOnly, + FileDelete, FileList, FileRead, FileWrite, FileWriteCreateNew, FileWriteOwnerOnly, }; pub use crate::v1_compiler_emit::{ bind_operation_transport, child_from_key, compute_service_fields, @@ -34908,6 +34908,7 @@ pub fn file_verb_action_expr(verb: FileVerb) -> String { FileVerb::FileRead => file_read_match_expr(), FileVerb::FileWrite => file_write_expr(), FileVerb::FileWriteOwnerOnly => file_write_owner_only_expr(), + FileVerb::FileWriteCreateNew => file_write_create_new_expr(), FileVerb::FileDelete => file_delete_match_expr(), FileVerb::FileList => file_list_match_expr(), } @@ -35091,6 +35092,15 @@ pub fn file_write_expr() -> String { CACHED.with(|c: &String| c.clone()) } +pub fn file_write_create_new_expr() -> String { + thread_local! { + static CACHED: String = { + "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let mut create_new_file = std::fs::OpenOptions::new().write(true).create_new(true).open(&file_path)?;\n create_new_file.write_all(content.as_bytes())?;\n Ok(())\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + pub fn file_write_owner_only_expr() -> String { thread_local! { static CACHED: String = { From 5b0c52f3497a4bffa9af2b5a45c7ac17af256430 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 14:30:35 +0000 Subject: [PATCH 17/21] Four of review 5089156132's six findings on the init model #10026 landed with these open. Each was verified against the code before being accepted, and each carries a control that goes red on the defect. 1. ScmInitialized could contain a FAILED creation. It carried the whole RepositorySave, so `ScmInitialized { save: RepositoryFileUnwritable { .. } }` was spellable and told every consumer matching the outer arm that initialization happened. The renderer noticed and exited nonzero, which repaired the message and not the carrier. ScmInitialized now carries only { path, written } from a successful create; init_outcome_of_save is a total fold over all four save arms and every other arm reaches ScmInitWriteRefused. 2. The established-absence authority was discarded before actuation. The code matched ScmInitMayCreate(_) and wrote to an independently supplied path, so an absence established for one subject could sit beside a create against another and no mutation to the write target went red. The token carries { directory, name }, so create_repository_at_absence now DERIVES the target from it -- there is no second target to disagree with. The rung prose is corrected rather than softened. Four external reviews read the sole_constructor and endorsed a rung-4 authorization claim; the designated reviewer read the MATCH and found the token was never consumed. A capability carried past its actuation authorizes nothing. The annotation now splits the rung honestly and says plainly that no preflight closes a TOCTOU -- O_EXCL does -- so the observation decides what the operator is told and which subject may be written, not whether the race exists. 3. WriteCreateNew erased the post-create write-failure state. open-then-write leaves a created, zero-or-partial file if write_all fails, while the model reports the create did not happen. That is worse than the overwrite race this operation closed: the race could destroy someone else's bytes, this FABRICATES a repository nobody wrote. Fixed by construction rather than by modeling two dispositions -- content is staged to an O_EXCL sibling and the target name is claimed with hard_link, which fails if the target exists, so exclusivity moves to the publish step and every earlier failure leaves the target absent. THE FIRST CONTROL I WROTE FOR THIS WAS A DECORATION, and the dead attempt is documented in the test module so it is not rebuilt. It put a DIRECTORY at the target; measured against the old construction it PASSED, because create_new fails at the OPEN when the name exists so nothing was ever created. The replacement injects RLIMIT_FSIZE in a forked child so the create succeeds and the write fails -- the one ordering that separates the constructions. Proven both ways: green on the fix, RED on the pre-fix construction with "a write that failed after creation must leave NO target behind". 4. FilesystemEntryName rejected `/` but admitted backslash and NUL while WriteCreateNew is implemented on non-Unix. `..\victim` is a parent traversal there, and a NUL makes the syscall see a PREFIX of the name the listing was asked about. The grammar is the UNION over supported targets, not the one the author happens to run on. Still open from that review: finding 5 (the emitted realization in 05_emit_rust.dag is independently mutable, plus two weak assertions) and finding 6 (compose #9864's final authority, which must land first). Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/extdeps/filesystem/filesystem_io.dag | 33 ++++++ dag/gunbc/scm/init.dag | 71 +++++++++++-- dag/gunbc/scm/render.dag | 8 +- dag/gunbc/scm/repository_save.dag | 19 ++++ dag/test/claim/scm/scm_cli_witness_test.dag | 81 +++++++++++++- src/v1/stage0/src/v1_interpreter.rs | 111 +++++++++++++++++++- 6 files changed, 308 insertions(+), 15 deletions(-) diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index 2304e05b1fe..7d29155e145 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -123,6 +123,27 @@ fn admit_filesystem_entry_name(name: String) -> FilesystemEntryNameAdmission { "than the one the joined path names", ], ""), } + } else if string_contains(s: name, pattern: "\\") { + FilesystemEntryNameRefused { + name: name, + cause: join([ + "the entry name ", name, " contains a backslash, which is a path separator on some hosts ", + "this operation is implemented for -- so `..\\victim` is a parent traversal there while ", + "passing a check that rejects only `/`, which is the exact defect this carrier exists to ", + "make impossible. The grammar is the UNION over supported targets, not the one the author ", + "happens to be running on: a carrier that admits on Linux what it must refuse on Windows ", + "answers about a different subject depending on where it runs", + ], ""), + } + } else if string_contains(s: name, pattern: "\0") { + FilesystemEntryNameRefused { + name: name, + cause: join([ + "the entry name ", name, " contains a NUL, which terminates a C string -- so the name the ", + "host syscall sees is a PREFIX of the name the listing was asked about, and the two ", + "describe different subjects with no diagnostic between them", + ], ""), + } } else if string_contains(s: name, pattern: "\n") { FilesystemEntryNameRefused { name: name, @@ -328,6 +349,18 @@ fn filesystem_established_absence_detail(absence: FilesystemEstablishedAbsence) join(["no ", absence.name, " is listed in ", absence.directory], "") } +// AND THE SUBJECT IT ESTABLISHED IS THE ONLY PATH IT CAN AUTHORIZE. A consumer that takes an +// established absence AND a separately supplied target has not been authorized by the token at all: +// the absence is about `directory + name`, the actuation is about whatever String arrived beside it, +// and nothing joins them. That is a real defect and it was found in review on gunbc#10026 -- +// `ScmInitMayCreate(_)` discarded the token and wrote to an independent `path`, so an absence +// established for one subject could coexist with a write to another. Deriving the path HERE, from +// the carrier's own fields, is what makes consuming the token mean something: there is no second +// target to disagree with. +fn filesystem_established_absence_path(absence: FilesystemEstablishedAbsence) -> String { + join([absence.directory, "/", absence.name], "") +} + data filesystem_absence_establishment_adoption_standing: String = "RUNG: structurally guaranteed for the consumers that route through filesystem_file_observation, on the source-to-.dag acceptance path only, and MITIGATABLE NOWHERE ELSE -- the raw Filesystem.Read and Filesystem.List operations stay callable, so a module that has not adopted the carrier can still write the conflation. This row states the unconverted population at identity grain rather than as a count, because a count is not a plan and a one-sided ratchet over a number measured on the current tree is the oracle section 5 rejects. SUBJECT: a site that concludes ABSENCE, NOT-PRESENT or a dropped element from a FAILED read or a FAILED boolean path test, rather than from a listing that succeeded. It is not every Filesystem.Read consumer -- most read a file they already know exists, and those are the separate filesystem_read_outcome adoption population above. ENUMERATED SITES, each one read rather than pattern-matched, on origin/main at the head this row lands against, with the two converted by the change that lands this row already removed (gunbc.roadmap_verification_receipt current_verification_selection_observe and exact_verification_receipt_source_read, and gunbc.devboot.build read_text_file): gunbc.host_effect_nbd_proxy_serve host_effect_nbd_proxy_serve_read_session_token (read refusal answers Absent, and an empty content does too); gunbc.fleet_converge_plan_cli observe_cap_members_wet (a cap member whose dropin could not be read is DROPPED from the observed list, so the converge plan is computed over a silently narrowed population); v2.workflow.product_receipt_stage run_product_receipt_stage (an unreadable manifest answers ArtifactIdentityAbsent { ProducerReportedNoArtifact }, attributing to the producer a report it never made); tools.merge_admission_walk read_tested_subject and read_floor_receipt (a read refusal answers the Optional's absent arm); gunbc.codex_supervised_turn codex_supervised_turn_generation_observation (GenerationAbsent is concluded from shell.Test.IsFile answering false. THIS ROW IS CLASSIFIED FROM THE PRODUCER RATHER THAN FROM THE CALL SITE, on a caution from the lane that shipped this defect today: a predicate whose job is to answer the presence question would not belong here. extdeps.shell Test.IsFile is `test -f` with its own declared exit table reading `1 => Path is missing or not a regular file`, so ONE exit code carries missing, wrong-kind, and -- since `test -f` is false when the parent directory cannot be searched -- could-not-look. It answers false on an unreadable-but-present path, so it is the same defect with a different producer, and it is the construction gunbc.fabric_cell_acquire retired for exactly this reason); tools.opaque_realization_census declaration_body_standing (a file that could not be read leaves the fold state unchanged, so it is indistinguishable from a file that did not hold the declaration). WHAT IS DELIBERATELY NOT ON THE LIST: gunbc.roadmap_belt_actuate belt_read_or_empty, whose collapse is scoped and argued in belt_read_or_empty_scope_note -- both branches take the same action at every remaining caller -- and gunbc.fabric_cell_acquire, which already establishes absence from the parent enumeration through its own four-state observation and would gain nothing but a second spelling. MONOTONE DIRECTION: the roster above may only shrink. A row leaves it when the site routes through filesystem_file_observation or filesystem_entry_presence, or when the site is deleted; a NEW site of this shape is a defect to repair rather than a row to add. NEXT-RUNG TRIGGER, and it names the capability rather than an artifact: the raw List and Read result projections cease to be reachable outside this module's folds, so a consumer cannot spell the conflation at all -- at which point the enumeration above has no subject and this row is deleted. That is the same trigger filesystem_read_outcome_adoption_standing carries, one question further in: it asks that every read projection be folded, this asks that every ABSENCE be established." // WriteCreateNew: CREATE-ONLY IS A DIFFERENT FACT FROM OWNER-ONLY, and this annotation sits here diff --git a/dag/gunbc/scm/init.dag b/dag/gunbc/scm/init.dag index 1c6fe3516df..f39d031d4bf 100644 --- a/dag/gunbc/scm/init.dag +++ b/dag/gunbc/scm/init.dag @@ -69,7 +69,15 @@ import gunbc.scm.repository_envelope { RepositoryDecoded, RepositoryDecodeRefused } -import gunbc.scm.repository_save { RepositorySave, create_repository } +import gunbc.scm.repository_save { + RepositorySave, + RepositorySaved, + RepositorySaveRefusedByCodec, + RepositoryFileUnwritable, + RepositoryWriteByteCountUnrepresentable, + create_repository_at_absence, +} +import std.measure { ByteSize } // THE ARMS ARE THE ANSWER. There is no `initialized: Bool` beside a save outcome: a value whose // flag disagreed with its shape would have a spelling, and the refusals are distinguished because @@ -93,8 +101,19 @@ type ScmInitRefusal // operator's next action differs -- one path already IS a repository, one holds something else that // would be destroyed, one could not be observed at all, and one was never a valid // entry name. +// AND `ScmInitialized` MAY NOT CONTAIN A FAILED CREATION. It used to carry the whole +// `RepositorySave`, whose arms include codec refusal, file-unwritable and unrepresentable byte +// count -- so `ScmInitialized { save: RepositoryFileUnwritable { .. } }` was a spellable value that +// told every consumer matching the outer arm that initialization HAPPENED when it did not. The +// renderer noticed the nested failure and exited nonzero, which repaired the message and not the +// carrier: a consumer reading the arm rather than re-folding its payload was simply lied to, on the +// ordinary write-refusal path. Found in review on gunbc#10026. +// +// The outer arm is now the answer by itself. `ScmInitialized` carries only what a SUCCESSFUL create +// produced, and every other save arm reaches `ScmInitWriteRefused`, which asserts nothing. type ScmInitOutcome - = ScmInitialized { save: RepositorySave } + = ScmInitialized { path: String, written: ByteSize } + | ScmInitWriteRefused { save: RepositorySave } | ScmInitRefused { cause: ScmInitRefusal } // WHAT THE OBSERVATION DECIDES, WITHOUT PERFORMING ANYTHING. `ScmInitMayCreate` carries the @@ -158,8 +177,23 @@ fn initialize_repository_at( path: path, ) { ScmInitDecided { cause: c } => ScmInitRefused { cause: c } - ScmInitMayCreate(_) => - ScmInitialized { save: create_repository(path: path, repo: empty_repository()) } + ScmInitMayCreate(absence) => init_outcome_of_save( + save: create_repository_at_absence(absence: absence, repo: empty_repository()) + ) + } +} + +// THE SAVE RESULT IS FOLDED, NOT WRAPPED. This is a total match over all four RepositorySave arms, +// and only RepositorySaved may construct ScmInitialized. A mutation that routes any other arm to +// ScmInitialized changes what the outer arm ASSERTS, which is exactly the edit the claims enrolled +// beside this function hold red. +fn init_outcome_of_save(save: RepositorySave) -> ScmInitOutcome { + match save { + RepositorySaved { path: p, written: w } => ScmInitialized { path: p, written: w } + RepositorySaveRefusedByCodec { path: _, cause: _ } => ScmInitWriteRefused { save: save } + RepositoryFileUnwritable { path: _, error: _ } => ScmInitWriteRefused { save: save } + RepositoryWriteByteCountUnrepresentable { path: _, reported: _ } => + ScmInitWriteRefused { save: save } } } @@ -169,10 +203,31 @@ fn initialize_repository_at( // only_an_established_absence_may_create each fail under exactly that edit). Routing the DISAGREEMENT // arm there is not authorable at all: ScmInitMayCreate carries a FilesystemEstablishedAbsence, which // is sole_constructor and minted only by the substrate fold from a listing that succeeded, so no arm -// can manufacture the permission to write. The rung is therefore split and stated rather than -// averaged: structurally impossible for fabricating a write permission (rung 4, no constructor), -// and mechanically preventable for routing a REAL absence to the wrong outcome (rung 2, held by the -// claims above). +// can manufacture the permission to write. +// +// THAT CLAIM WAS OVERSTATED UNTIL THIS CHANGE, AND THE CORRECTION IS THE POINT. The token being +// unforgeable bought nothing while the actuation ignored it: this function matched +// `ScmInitMayCreate(_)`, discarded the absence, and wrote to an independently supplied `path`. An +// absence established for one subject could therefore sit beside a write to a DIFFERENT one, and no +// mutation to the write target went red. Four external reviews read the sole_constructor and +// endorsed a rung-4 authorization claim; the designated reviewer read the MATCH and found the token +// was never consumed. A capability that is carried past its actuation authorizes nothing. +// +// The absence is now CONSUMED: create_repository_at_absence derives its target from the carrier's +// own directory and name, so there is no second target to disagree with. +// +// THE RUNG, SPLIT AND STATED RATHER THAN AVERAGED, AND SMALLER THAN IT WAS CLAIMED TO BE: +// - fabricating a write permission out of nothing: structurally impossible (rung 4, no +// constructor for FilesystemEstablishedAbsence outside the substrate fold); +// - authorizing a write to a subject the absence was NOT established for: structurally impossible +// for THIS caller (rung 4, the path has one derivation and no independent target), and NOT a +// property of create_repository, which still takes a bare String for its own callers; +// - routing a REAL absence to the wrong outcome: mechanically preventable (rung 2, held by the +// claims above). +// +// AND THE RACE ITSELF IS NOT ON THAT LADDER AT ALL. No preflight closes a TOCTOU; O_EXCL does. The +// observation decides WHAT TO TELL THE OPERATOR and which subject may be written; the exclusive +// create is the wall against an actor that arrives between the two. // // THE DECISION IS ITS OWN FUNCTION SO IT CAN BE WITNESSED WITHOUT A FILESYSTEM. Every arm below is a // choice about whether bytes may be written, and while it lived inside the effectful entry the only diff --git a/dag/gunbc/scm/render.dag b/dag/gunbc/scm/render.dag index 3b3ccc2c0b4..6687a264cda 100644 --- a/dag/gunbc/scm/render.dag +++ b/dag/gunbc/scm/render.dag @@ -52,6 +52,7 @@ import gunbc.scm.repository_load { repository_load_refusal_lines } import gunbc.scm.init { ScmInitOutcome, ScmInitialized, + ScmInitWriteRefused, ScmInitRefused, ScmInitRefusal, ScmInitRepositoryPresent, @@ -271,7 +272,9 @@ fn scm_save_cli_response( // foreign file at that path is a choice about someone else's bytes. fn scm_init_lines(outcome: ScmInitOutcome) -> List { match outcome { - ScmInitialized { save: save } => repository_save_lines(save: save) + ScmInitialized { path: p, written: _ } => + [concat("initialized repository at ", p)] + ScmInitWriteRefused { save: save } => repository_save_lines(save: save) ScmInitRefused { cause: cause } => scm_init_refusal_lines(cause: cause) } } @@ -303,7 +306,8 @@ fn scm_init_refusal_lines(cause: ScmInitRefusal) -> List { fn scm_init_exit(outcome: ScmInitOutcome) -> ProcessExit { match outcome { - ScmInitialized { save: save } => scm_save_exit(save: save) + ScmInitialized { path: _, written: _ } => ExitSuccess + ScmInitWriteRefused { save: save } => scm_save_exit(save: save) ScmInitRefused { cause: cause } => scm_init_refusal_exit(cause: cause) } } diff --git a/dag/gunbc/scm/repository_save.dag b/dag/gunbc/scm/repository_save.dag index cbf11d4f22e..212e0400010 100644 --- a/dag/gunbc/scm/repository_save.dag +++ b/dag/gunbc/scm/repository_save.dag @@ -43,6 +43,7 @@ module gunbc.scm.repository_save import std.types { String, Int } import extdeps.filesystem.filesystem_io +import extdeps.filesystem.filesystem_io { FilesystemEstablishedAbsence, filesystem_established_absence_path } import extdeps.languages.json.emit { serialize_json } import std.measure { ByteSize, byte_size } import std.checked_arithmetic { nat_magnitude } @@ -102,6 +103,24 @@ type RepositorySave // remedy is the same -- the bytes are not yours to write and the host says why -- and the error text // is the host's own. A second arm would be a second spelling of one outcome (section 3), and one that // classified the cause from the error TEXT would be a heuristic standing in for an observation. +// THE CREATE THAT AN ESTABLISHED ABSENCE AUTHORIZES, AND THE ONLY ONE IT CAN. +// +// create_repository below takes a bare String, which is right for its own subject -- a caller that +// has some other reason to create at a path may use it. It is the WRONG entry for a caller whose +// permission came from an absence, because taking the token and a separate path lets the two name +// different subjects and nothing detects it. Review on gunbc#10026 found exactly that: init matched +// ScmInitMayCreate(_), threw the token away, and wrote to an independently computed path. +// +// So the absence-authorized create derives its target from the token itself. There is no second +// target to disagree with, which is the difference between a capability that is CONSUMED and one +// that is merely carried past the actuation. +fn create_repository_at_absence( + absence: FilesystemEstablishedAbsence, + repo: RepositoryEnvelope, +) -> RepositorySave { + create_repository(path: filesystem_established_absence_path(absence: absence), repo: repo) +} + fn create_repository(path: String, repo: RepositoryEnvelope) -> RepositorySave { match encode_repository_checked(repo: repo) { RepositoryEncodeRefused { cause: cause } => diff --git a/dag/test/claim/scm/scm_cli_witness_test.dag b/dag/test/claim/scm/scm_cli_witness_test.dag index ebe49fe5074..1db352d948b 100644 --- a/dag/test/claim/scm/scm_cli_witness_test.dag +++ b/dag/test/claim/scm/scm_cli_witness_test.dag @@ -33,9 +33,18 @@ import gunbc.scm.init { ScmInitMayCreate, ScmInitDecided, ScmInitialized, + ScmInitWriteRefused, scm_init_decision, + init_outcome_of_save, initialize_repository } +import gunbc.scm.repository_save { + RepositorySave, + RepositorySaved, + RepositoryFileUnwritable, + RepositoryWriteByteCountUnrepresentable, +} +import std.measure { byte_size } import extdeps.filesystem.filesystem_io { FilesystemDirectoryListed, FilesystemDirectoryListingRefused, @@ -50,7 +59,8 @@ import extdeps.filesystem.filesystem_io { filesystem_file_observation, admit_filesystem_entry_name, FilesystemEntryNameAdmitted, - FilesystemEntryNameRefused + FilesystemEntryNameRefused, + filesystem_established_absence_path } // THE BYTES PIN THE CAPABILITY. This is the same expected string the render-level witness pins for @@ -292,6 +302,18 @@ test fn a_name_that_is_not_one_child_of_the_directory_is_refused() -> Bool { && !name_admits(n: "../victim") } +// THE GRAMMAR IS THE UNION OVER SUPPORTED TARGETS, NOT THE AUTHOR'S HOST. Review on gunbc#10026 +// found this carrier rejecting `/` while admitting `\\` and NUL, with WriteCreateNew implemented on +// non-Unix rather than refusing there -- so `..\\victim` is a parent traversal on Windows that +// passes a check named for making traversal impossible, and a NUL makes the syscall see a PREFIX of +// the name the listing was asked about. Both are the one-name-two-subjects defect the carrier +// exists to close, reached by spellings the first cut did not model. +test fn a_name_carrying_another_hosts_separator_or_a_nul_is_refused() -> Bool { + !name_admits(n: "..\\victim") + && !name_admits(n: "subdir\\repo.json") + && !name_admits(n: "repo.json\0.bak") +} + // THE NEWLINE CASE IS THIS MODULE'S OWN, because the delimiter belongs to Filesystem.List's encoding: // a name carrying one can make the membership test answer about an entry that is not present. test fn a_name_carrying_the_listing_delimiter_is_refused() -> Bool { @@ -304,7 +326,8 @@ test fn a_name_carrying_the_listing_delimiter_is_refused() -> Bool { // that is exactly the property being claimed. test fn a_refused_name_refuses_before_any_filesystem_operation() -> Bool { match initialize_repository(directory: "d", name: "../victim") { - ScmInitialized { save: _ } => false + ScmInitialized { path: _, written: _ } => false + ScmInitWriteRefused { save: _ } => false ScmInitRefused { cause: c } => match c { ScmInitNameNotAnEntry { name: _, cause: _ } => true @@ -314,3 +337,57 @@ test fn a_refused_name_refuses_before_any_filesystem_operation() -> Bool { } } } + +// A FAILED SAVE MAY NOT WEAR THE SUCCESS ARM. This is the discriminating control for the defect +// review found on gunbc#10026: ScmInitialized used to carry the whole RepositorySave, so +// `ScmInitialized { save: RepositoryFileUnwritable { .. } }` was spellable and told every consumer +// matching the outer arm that initialization happened. init_outcome_of_save is a total fold and only +// RepositorySaved may reach ScmInitialized; routing ANY other arm there turns these red. +// +// It is driven over the save arms directly rather than through the effectful entry, because the +// property is about the FOLD and a SubstrateInputsOnly witness cannot make a real write fail. +fn init_outcome_claims_success(save: RepositorySave) -> Bool { + match init_outcome_of_save(save: save) { + ScmInitialized { path: _, written: _ } => true + ScmInitWriteRefused { save: _ } => false + ScmInitRefused { cause: _ } => false + } +} + +test fn a_saved_repository_is_the_only_initialized_outcome() -> Bool { + init_outcome_claims_success( + save: RepositorySaved { path: "/d/repo.json", written: byte_size(count: 12) } + ) +} + +test fn no_failed_save_arm_reaches_the_initialized_outcome() -> Bool { + !init_outcome_claims_success( + save: RepositoryFileUnwritable { path: "/d/repo.json", error: "Permission denied" } + ) + && !init_outcome_claims_success( + save: RepositoryWriteByteCountUnrepresentable { path: "/d/repo.json", reported: 0 - 1 } + ) +} + +// THE ABSENCE NAMES THE SUBJECT IT AUTHORIZES. The second review defect: the token was matched as +// `_` and the write actuated on an independently supplied path, so evidence about one directory +// entry could sit beside a create against another. The path now has ONE derivation, from the +// carrier's own fields, and this pins it -- an absence for directory d and name n authorizes +// exactly d/n and nothing else. +test fn an_established_absence_derives_the_only_path_it_authorizes() -> Bool { + let listed = filesystem_listing_observation( + directory: "/d", success: true, entries: "other.json", error: "" + ) + match filesystem_file_observation( + listing: listed, + name: "repo.json", + path: "/d/repo.json", + read: filesystem_read_outcome(content: "", success: false, error: "No such file") + ) { + FilesystemFileAbsent(absence) => + filesystem_established_absence_path(absence: absence) == "/d/repo.json" + FilesystemFileRead { path: _, content: _ } => false + FilesystemFileIndeterminate { cause: _ } => false + FilesystemFileObservationsDisagree { path: _, cause: _ } => false + } +} diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 3f9b8c038b4..dbf9365fe66 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -12067,12 +12067,53 @@ fn write_file_owner_only(path: &str, content: &[u8]) -> std::io::Result<()> { /// EXISTENCE are independent facts; a caller that obtained create-only from it would silently also /// get 0600, and would break if owner-only ever stopped needing O_EXCL. This is portable and sets no /// mode, because setting one would be the same conflation in reverse. +/// THE TARGET IS PUBLISHED ONLY WHEN ITS CONTENT IS COMPLETE. +/// +/// The first cut of this was `create_new(true).open(path)` followed by `write_all`, and review on +/// gunbc#10026 found the state that construction cannot describe: if the open SUCCEEDS and the +/// write then fails, the target has already been created and holds zero or partial bytes. The +/// helper returned an ordinary error, the transport reported `success=false, bytes_written=0`, and +/// the caller classified it as merely unwritable -- so the model said the create did not happen +/// while a new, incomplete artifact sat at the path. That collapses "nothing was created" into "a +/// truncated repository now exists", which is a worse lie than the overwrite race this operation +/// was added to close: the original race could destroy someone else's bytes, and this one +/// FABRICATES a repository nobody wrote. +/// +/// Two dispositions are not modeled here, because a construction that cannot reach the bad state +/// is available (DESIGN section 4b: construction over proof, proof over validation). Content is +/// written to a sibling temporary that is itself created with O_EXCL, and the target name is +/// claimed by `hard_link`, which FAILS IF THE TARGET EXISTS -- so exclusivity is preserved by the +/// publish step rather than by the open. Every failure before the link leaves the target absent, +/// which is exactly what the operation reports. +/// +/// The temporary is removed on every path. Its removal failure is deliberately NOT propagated: it +/// leaves a stray sibling and does not affect what the target is, and reporting it as a write +/// failure would say the repository was not created when it was. fn write_file_create_new(path: &str, content: &[u8]) -> std::io::Result<()> { use std::fs::OpenOptions; use std::io::Write; - let mut file = OpenOptions::new().write(true).create_new(true).open(path)?; - file.write_all(content)?; - Ok(()) + + let temp = format!("{path}.gunbc-create-{}", std::process::id()); + + // The temporary is exclusive too, so two concurrent creators cannot share one staging file. + let mut file = match OpenOptions::new().write(true).create_new(true).open(&temp) { + Ok(f) => f, + Err(e) => return Err(e), + }; + if let Err(e) = file.write_all(content) { + let _ = std::fs::remove_file(&temp); + return Err(e); + } + if let Err(e) = file.sync_all() { + let _ = std::fs::remove_file(&temp); + return Err(e); + } + drop(file); + + // hard_link refuses an existing target, which is where this operation's exclusivity now lives. + let published = std::fs::hard_link(&temp, path); + let _ = std::fs::remove_file(&temp); + published } // ------------------------------------------------------------------------------------------------ @@ -12104,6 +12145,70 @@ mod write_file_create_new_tests { std::fs::remove_dir_all(&dir).ok(); } + // THE POST-OPEN FAILURE CONTROL, and it took two attempts to make it real. + // + // Review on gunbc#10026 found that neither existing cell observes a failure AFTER the target + // name would have been claimed -- exactly where the old open-then-write construction left a + // created-but-incomplete file while reporting that nothing was created. + // + // THE FIRST ATTEMPT WAS A DECORATION AND IS RECORDED HERE SO IT IS NOT REBUILT. It put a + // DIRECTORY at the target and asserted the target was untouched. Measured against the old + // construction, it PASSED: `create_new` fails at the OPEN when the name exists, so nothing was + // ever created and the assertion was satisfied by the defect. A check that cannot go red on the + // fault it names is worse than absent (DESIGN section 4b) because it gets cited as coverage. + // + // THIS ONE REACHES THE FAULT. RLIMIT_FSIZE makes `write_all` fail with EFBIG on a path that is + // ABSENT, so the create genuinely succeeds and the write genuinely fails -- the one ordering + // that distinguishes the two constructions. It runs in a forked child because the limit and the + // SIGXFSZ disposition are process-wide and this binary runs tests concurrently; the parent only + // reads the filesystem afterwards. + #[test] + fn a_write_failure_after_creation_leaves_no_target_behind() { + let dir = + std::env::temp_dir().join(format!("gunbc-create-new-efbig-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("temp dir"); + let target = dir.join("repo.json"); + let target_s = target.to_str().unwrap().to_string(); + + // 64 bytes allowed, 4 KiB written: the create succeeds, the write cannot. + let content = vec![b'x'; 4096]; + + let pid = unsafe { libc::fork() }; + assert!(pid >= 0, "fork failed"); + if pid == 0 { + unsafe { + libc::signal(libc::SIGXFSZ, libc::SIG_IGN); + let lim = libc::rlimit { + rlim_cur: 64, + rlim_max: 64, + }; + libc::setrlimit(libc::RLIMIT_FSIZE, &lim); + } + let _ = super::write_file_create_new(&target_s, &content); + unsafe { libc::_exit(0) }; + } + let mut status: libc::c_int = 0; + unsafe { libc::waitpid(pid, &mut status, 0) }; + + // THE LOAD-BEARING ASSERTION. Under the old construction the target was created by the open + // and survived the failed write as a zero-or-partial file -- a repository nobody wrote. + // Publishing only when the content is complete means there is nothing at the target at all. + assert!( + !target.exists(), + "a write that failed after creation must leave NO target behind" + ); + let strays: Vec = std::fs::read_dir(&dir) + .expect("list") + .filter_map(|e| e.ok()) + .map(|e| e.file_name().to_string_lossy().to_string()) + .collect(); + assert!( + strays.is_empty(), + "no staging temporary may survive either: {strays:?}" + ); + std::fs::remove_dir_all(&dir).ok(); + } + #[test] fn create_new_writes_when_nothing_is_there() { let dir = std::env::temp_dir().join(format!("gunbc-create-new-ok-{}", std::process::id())); From d1d828a5376e817afdbdba0f9f34042c45114a65 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 16:15:39 +0000 Subject: [PATCH 18/21] The other two parts of finding 5: pin the valid repository, and enrol the fourth refusal 5.2 -- present_bytes_do_not_authorize_a_write_and_are_classified asserted only `!= may_create` for a DECODABLE repository. That is satisfied by mapping every present file, valid repository included, to ScmInitForeignFilePresent -- which would tell an operator a foreign file is in the way of their own repository, and the claim would have stayed green. The two present arms are one fact apart (same listing and read, differing only in whether the content decodes), so each is now pinned to its own arm. That is the difference between classification evidence and a not-the-write-arm check. 5.3 -- ScmInitNameNotAnEntry became a fourth refusal arm while both renderer claims still enumerated three. The direct admission test proved the name refuses EARLY; nothing proved it reaches an operator as its own answer with a failing exit. Both claims now cover four arms, and the claim is RENAMED to the_four_init_refusals_render_differently so its name moves with its population -- a claim that names a population and does not move silently covers a shrinking fraction of its subject. Not done, and deliberately not guessed at: 5.1, the emitted realization in 05_emit_rust.dag being independently mutable to create/truncate while the Rust unit tests stay green. That is the same class as the decoration I shipped and withdrew earlier in this branch, one layer out, and it wants either an executing emitted-program probe or a construction that prevents the two realizations from drifting. I have asked the reviewer which shape they want rather than build the wrong one. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/test/claim/scm/scm_cli_witness_test.dag | 24 +++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/dag/test/claim/scm/scm_cli_witness_test.dag b/dag/test/claim/scm/scm_cli_witness_test.dag index 1db352d948b..671dba79b01 100644 --- a/dag/test/claim/scm/scm_cli_witness_test.dag +++ b/dag/test/claim/scm/scm_cli_witness_test.dag @@ -173,15 +173,28 @@ test fn an_init_refusal_never_exits_success() -> Bool { && wire_refuses(r: scm_init_response( outcome: ScmInitRefused { cause: ScmInitPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } } )) + && wire_refuses(r: scm_init_response( + outcome: ScmInitRefused { cause: ScmInitNameNotAnEntry { name: "../victim", cause: "it is a path, not one child" } } + )) } -test fn the_three_init_refusals_render_differently() -> Bool { +// THE POPULATION IS FOUR, AND IT SAYS SO. ScmInitNameNotAnEntry became a fourth refusal arm and +// these claims still enumerated three, so the direct admission test proved the name refuses EARLY +// while nothing proved it reaches an operator as its own answer. A claim that names a population +// has to move when the population does, or it silently covers a shrinking fraction of its subject. +// Review 5089156132 finding 5.3 on gunbc#10026. +test fn the_four_init_refusals_render_differently() -> Bool { let present = wire_bytes(r: scm_init_response(outcome: ScmInitRefused { cause: ScmInitRepositoryPresent { path: "repo.json" } })) let foreign = wire_bytes(r: scm_init_response(outcome: ScmInitRefused { cause: ScmInitForeignFilePresent { path: "repo.json" } })) let unobserved = wire_bytes(r: scm_init_response( outcome: ScmInitRefused { cause: ScmInitPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } } )) + let not_an_entry = wire_bytes(r: scm_init_response( + outcome: ScmInitRefused { cause: ScmInitNameNotAnEntry { name: "../victim", cause: "it is a path, not one child" } } + )) present != foreign && foreign != unobserved && present != unobserved && present != "" + && not_an_entry != present && not_an_entry != foreign && not_an_entry != unobserved + && not_an_entry != "" } // THE UNOBSERVED ARM CARRIES THE HOST'S CAUSE THROUGH. A refusal that dropped it would tell the @@ -267,6 +280,13 @@ test fn two_disagreeing_observations_do_not_authorize_a_write() -> Bool { == "unobserved" } +// AND THE VALID REPOSITORY IS PINNED TO ITS OWN ARM, NOT MERELY AWAY FROM THE WRITE ARM. This +// asserted `!= may_create` for a decodable repository, which is satisfied by mapping EVERY present +// file -- valid repository included -- to ScmInitForeignFilePresent. That would tell an operator a +// foreign file is in the way of their own repository, and the claim would have stayed green. The +// two present arms are one fact apart (the same listing and read, differing only in whether the +// content decodes), so pinning each to its own arm is what makes the classification evidence rather +// than a not-the-write-arm check. Review 5089156132 finding 5.2 on gunbc#10026. test fn present_bytes_do_not_authorize_a_write_and_are_classified() -> Bool { decide(o: observe(listed: true, entries: "repo.json", read_ok: true, content: "not json at all")) == "foreign_present" @@ -275,7 +295,7 @@ test fn present_bytes_do_not_authorize_a_write_and_are_classified() -> Bool { entries: "repo.json", read_ok: true, content: "{\"format\":\"gunbc-scm-repository-v2\"}", - )) != "may_create" + )) == "repository_present" } // ------------------------------------------------------------------------------------------------ From 78a52209b99007514cdf32c5600c110295957120 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 16:32:34 +0000 Subject: [PATCH 19/21] Finding 5.1: the emitted realization kept the defect the interpreter fix removed Review 58797 on gunbc#10069 is correct, and it is a sharper statement than my own framing of the same row. I had called this "the emitted realization is independently mutable" -- a testing gap. It is not: the DEFECT ITSELF was still present. v1_interpreter::write_file_create_new was repaired to stage-then-link while src/v1/05_emit_rust.dag's file_write_create_new_expr still spelled open-then-write against the target, so a failed emitted write could still leave a partial repository while reporting failure. The fabricated-repository failure survived, in the realization my tests do not execute. That is one fact with two authorities (DESIGN sections 2 and 3), where repairing the reachable one leaves the other lying; and it is section 4b rung honesty, because a class's rung is the MINIMUM across its paths and a fix on the interpreted path does not raise the emitted one. The emitted expression now uses the same construction: stage to an O_EXCL sibling, publish by hard_link (which fails if the target exists), remove the staging file on every path. Projection regenerated. EVIDENCE, over the EMITTED BYTES rather than the interpreter. The expression is decoded out of 05_emit_rust.dag, compiled as a standalone program, and executed: an absent path is created with the right content; an existing path REFUSES and its bytes survive; no staging temporary is left behind. Proven discriminating by the mutation the review itself named -- replacing the body with create/truncate turns the probe RED at "an existing path must refuse". WHAT THIS DOES NOT CLOSE, stated rather than left to be rediscovered: these are still two spellings. An emitted standalone program cannot call the seed's helper, so nothing but review holds them in step, and the drift this review caught can recur. The note in 05_emit_rust.dag carries a next-rung trigger naming the CAPABILITY -- one file-transport realization authority that both the seed and the emitted program consume -- rather than an artifact that would merely contribute to one. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- src/v1/05_emit_rust.dag | 18 +++++++++++++++++- src/v1/stage0/src/v1_compiler_emit_rust.rs | 2 +- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/v1/05_emit_rust.dag b/src/v1/05_emit_rust.dag index 6a35e4da606..e4d11273242 100644 --- a/src/v1/05_emit_rust.dag +++ b/src/v1/05_emit_rust.dag @@ -14407,7 +14407,23 @@ data file_list_match_expr: String = "match std::fs::read_dir(&file_path) {\n data file_write_expr: String = "{\n let payload_bytes = content.len() as i64;\n match std::fs::write(&file_path, content.as_bytes()) {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(write_err) => (false, String::new(), format!(\"{}\", write_err), 0i64),\n }\n};" -data file_write_create_new_expr: String = "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let mut create_new_file = std::fs::OpenOptions::new().write(true).create_new(true).open(&file_path)?;\n create_new_file.write_all(content.as_bytes())?;\n Ok(())\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};" +// THE EMITTED REALIZATION PUBLISHES ONLY COMPLETE CONTENT, exactly as the interpreter helper does, +// and this row exists because review 5089156132 on gunbc#10069 found the two had DIVERGED. The +// interpreter's v1_interpreter::write_file_create_new was repaired to stage-then-link while THIS +// expression still spelled open-then-write against the target, so a failed emitted write could +// still leave a partial repository while reporting failure -- the same fabricated-repository defect, +// surviving in the realization the tests do not execute. +// +// That is the shape DESIGN section 2 and 3 forbid: one fact with two authorities, where repairing +// the reachable one leaves the other lying. It is also section 4b rung honesty -- the class's rung +// is the MINIMUM across its paths, and a fix on the interpreted path does not raise the emitted one. +// +// These two spellings are still two spellings, which is the residue this row does not close: the +// emitted program is standalone Rust and cannot call the seed's helper, so nothing but review holds +// them in step today. NEXT-RUNG TRIGGER, naming the capability rather than an artifact: an emitted +// file-transport realization derived from ONE authority that both the seed and the emitted program +// consume, at which point the divergence has no spelling and this note has no subject. +data file_write_create_new_expr: String = "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let staging_path = format!(\"{}.gunbc-create-{}\", file_path, std::process::id());\n let mut staged = std::fs::OpenOptions::new().write(true).create_new(true).open(&staging_path)?;\n if let Err(staging_err) = staged.write_all(content.as_bytes()) {\n let _ = std::fs::remove_file(&staging_path);\n return Err(staging_err);\n }\n if let Err(sync_err) = staged.sync_all() {\n let _ = std::fs::remove_file(&staging_path);\n return Err(sync_err);\n }\n drop(staged);\n let published = std::fs::hard_link(&staging_path, &file_path);\n let _ = std::fs::remove_file(&staging_path);\n published\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};" data file_write_owner_only_expr: String = "{\n let payload_bytes = content.len() as i64;\n let owner_only_result = (|| -> std::io::Result<()> {\n #[cfg(unix)]\n {\n use std::io::Write;\n use std::os::unix::fs::OpenOptionsExt;\n let mut owner_only_file = std::fs::OpenOptions::new().write(true).create_new(true).mode(0o600).open(&file_path)?;\n owner_only_file.write_all(content.as_bytes())?;\n return Ok(());\n }\n #[cfg(not(unix))]\n {\n return Err(std::io::Error::new(std::io::ErrorKind::Unsupported, \"write_owner_only refused: owner-only mode-at-creation is unavailable on this platform\"));\n }\n })();\n match owner_only_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(owner_only_err) => (false, String::new(), format!(\"{}\", owner_only_err), 0i64),\n }\n};" diff --git a/src/v1/stage0/src/v1_compiler_emit_rust.rs b/src/v1/stage0/src/v1_compiler_emit_rust.rs index 9e7ef3e1529..5c39d70e41e 100644 --- a/src/v1/stage0/src/v1_compiler_emit_rust.rs +++ b/src/v1/stage0/src/v1_compiler_emit_rust.rs @@ -35145,7 +35145,7 @@ pub fn file_write_expr() -> String { pub fn file_write_create_new_expr() -> String { thread_local! { static CACHED: String = { - "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let mut create_new_file = std::fs::OpenOptions::new().write(true).create_new(true).open(&file_path)?;\n create_new_file.write_all(content.as_bytes())?;\n Ok(())\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};".to_string() + "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let staging_path = format!(\"{}.gunbc-create-{}\", file_path, std::process::id());\n let mut staged = std::fs::OpenOptions::new().write(true).create_new(true).open(&staging_path)?;\n if let Err(staging_err) = staged.write_all(content.as_bytes()) {\n let _ = std::fs::remove_file(&staging_path);\n return Err(staging_err);\n }\n if let Err(sync_err) = staged.sync_all() {\n let _ = std::fs::remove_file(&staging_path);\n return Err(sync_err);\n }\n drop(staged);\n let published = std::fs::hard_link(&staging_path, &file_path);\n let _ = std::fs::remove_file(&staging_path);\n published\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};".to_string() }; } CACHED.with(|c: &String| c.clone()) From bc3bbb9ed16358eee9100852162e0010a8786633 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 17:49:09 +0000 Subject: [PATCH 20/21] Derive the valid-repository fixture from the writer, not a hand-authored literal The floor red on 78a5220 was my own tightened claim: I had pinned the valid-repository arm of present_bytes_do_not_authorize_a_write_and_are_classified from `!= "may_create"` to `== "repository_present"`, and the hand-authored payload `{"format":"gunbc-scm-repository-v2"}` does not decode as a v2 repository, so the classifier answered `foreign_present`. Reverting the pin would re-weaken the claim to one that cannot tell a repository from a foreign file, so the fixture is what changes. A literal here is a second authority for the repository wire format (DESIGN section 3): it agrees with the codec only while someone keeps retyping it, and the version it drifts to is silently classified as a foreign file -- the classifier reporting a repository this program just wrote as not one. The fixture is now `serialize_json` of `encode_repository_checked(empty_repository())`, the same two calls repository_save makes, so writer and classifier are held to agreeing BY EXECUTION. The encode-refused arm yields "", which decodes as foreign rather than as a repository, so a refusal fails this claim instead of vacuously satisfying it. Mutation-proven discriminating: substituting the old literal back into saved_repository_bytes turns the claim RED; the derived bytes turn it green. All 20 claims in test.claim.scm.scm_cli_witness pass. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- dag/test/claim/scm/scm_cli_witness_test.dag | 26 ++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/dag/test/claim/scm/scm_cli_witness_test.dag b/dag/test/claim/scm/scm_cli_witness_test.dag index 671dba79b01..c93a4341d96 100644 --- a/dag/test/claim/scm/scm_cli_witness_test.dag +++ b/dag/test/claim/scm/scm_cli_witness_test.dag @@ -44,6 +44,13 @@ import gunbc.scm.repository_save { RepositoryFileUnwritable, RepositoryWriteByteCountUnrepresentable, } +import gunbc.scm.repository_envelope { + RepositoryEncodeOutcome, + RepositoryEncoded, + RepositoryEncodeRefused, + encode_repository_checked, +} +import extdeps.languages.json.emit { serialize_json } import std.measure { byte_size } import extdeps.filesystem.filesystem_io { FilesystemDirectoryListed, @@ -287,6 +294,23 @@ test fn two_disagreeing_observations_do_not_authorize_a_write() -> Bool { // two present arms are one fact apart (the same listing and read, differing only in whether the // content decodes), so pinning each to its own arm is what makes the classification evidence rather // than a not-the-write-arm check. Review 5089156132 finding 5.2 on gunbc#10026. +// THE VALID-REPOSITORY FIXTURE IS THE WRITER'S OWN OUTPUT, not a hand-authored literal. A literal +// here is a second authority for the repository wire format (DESIGN section 3): it agrees with the +// codec only for as long as someone keeps retyping it, and the version it drifts to is silently +// classified `foreign_present` -- the classifier reporting a repository this program just wrote as +// a foreign file. Deriving the bytes from `encode_repository_checked` makes writer and classifier +// agree BY EXECUTION, so a codec change that breaks the round trip turns this claim red at the +// change rather than at the next hand edit. +// +// A refused encode yields "" here, which decodes as foreign rather than as a repository, so the +// refusal arm fails this claim instead of vacuously satisfying it. +fn saved_repository_bytes() -> String { + match encode_repository_checked(repo: empty_repository()) { + RepositoryEncodeRefused { cause: _ } => "" + RepositoryEncoded { value: v } => serialize_json(v: v) + } +} + test fn present_bytes_do_not_authorize_a_write_and_are_classified() -> Bool { decide(o: observe(listed: true, entries: "repo.json", read_ok: true, content: "not json at all")) == "foreign_present" @@ -294,7 +318,7 @@ test fn present_bytes_do_not_authorize_a_write_and_are_classified() -> Bool { listed: true, entries: "repo.json", read_ok: true, - content: "{\"format\":\"gunbc-scm-repository-v2\"}", + content: saved_repository_bytes(), )) == "repository_present" } From 5d0d8b8e066966651c35f342b360c6c16d2c465c Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 2 Sep 2026 20:16:50 +0000 Subject: [PATCH 21/21] Spell the staging open with `?`, which the emitted realization already did The composed head's rust-unit-tests job failed on clippy::question_mark (the repo clippy command runs with -D warnings): write_file_create_new opened its staging file through `match { Ok(f) => f, Err(e) => return Err(e) }` where `?` is exact. Clippy is right and this is not a lint to allow. That arm creates nothing, so there is no staging file to clean up -- which is precisely why it is the one failure path in this function that does NOT remove_file, and the comment now says so rather than leaving the `?` looking careless next to three neighbours that do clean up. It also removes a difference that was never semantic: file_write_create_new_expr already spelled this `?`, so the two realizations disagreed on the spelling of one line while agreeing on its meaning. One less thing for the commissioned single-authority cut to reconcile. Verified with the exact CI command rather than by inspection: cargo clippy --all-targets -- -D warnings clean cargo test --release -p v1-compiler --lib write_file_create_new create_new_writes_when_nothing_is_there ok create_new_refuses_a_path_that_already_exists_and_leaves_its_bytes ok a_write_failure_after_creation_leaves_no_target_behind ok Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9 --- src/v1/stage0/src/v1_interpreter.rs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 60c2a561dde..c5110eef8a5 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -12837,10 +12837,14 @@ fn write_file_create_new(path: &str, content: &[u8]) -> std::io::Result<()> { let temp = format!("{path}.gunbc-create-{}", std::process::id()); // The temporary is exclusive too, so two concurrent creators cannot share one staging file. - let mut file = match OpenOptions::new().write(true).create_new(true).open(&temp) { - Ok(f) => f, - Err(e) => return Err(e), - }; + // `?` rather than a match: this arm creates nothing, so there is no staging file to clean up -- + // which is exactly why it is the one failure below that does NOT remove_file. The emitted + // realization already spells it `?`, so this also stops the two spellings differing over a + // difference that was never semantic. + let mut file = OpenOptions::new() + .write(true) + .create_new(true) + .open(&temp)?; if let Err(e) = file.write_all(content) { let _ = std::fs::remove_file(&temp); return Err(e);