diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2c7d219c6a5..ba46b455393 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -39,6 +39,9 @@ jobs: if sccache --show-stats >/dev/null 2>&1; then echo "RUSTC_WRAPPER=sccache" >> "$GITHUB_ENV" echo "CARGO_INCREMENTAL=0" >> "$GITHUB_ENV" + printf '%s\n' "CiSccacheProviderReceipt: provider=bound catalog=sccache_local" + else + printf '%s\n' "CiSccacheProviderReceipt: provider=SKIPPED catalog=sccache_local host=$(hostname) cause=daemon-unavailable; the release build runs UNCACHED β€” a counted degradation, not a supported mode (host_build_cache_provision P1b should have converged this host)" fi - name: Setup Rust uses: actions-rust-lang/setup-rust-toolchain@v1.16.0 diff --git a/.github/workflows/falsifier.yml b/.github/workflows/falsifier.yml index 2d304fdf62b..493ae081729 100644 --- a/.github/workflows/falsifier.yml +++ b/.github/workflows/falsifier.yml @@ -33,6 +33,9 @@ jobs: if sccache --show-stats >/dev/null 2>&1; then echo "RUSTC_WRAPPER=sccache" >> "$GITHUB_ENV" echo "CARGO_INCREMENTAL=0" >> "$GITHUB_ENV" + printf '%s\n' "CiSccacheProviderReceipt: provider=bound catalog=sccache_local" + else + printf '%s\n' "CiSccacheProviderReceipt: provider=SKIPPED catalog=sccache_local host=$(hostname) cause=daemon-unavailable; the release build runs UNCACHED β€” a counted degradation, not a supported mode (host_build_cache_provision P1b should have converged this host)" fi - name: Setup Rust uses: actions-rust-lang/setup-rust-toolchain@v1.16.0 diff --git a/dag/extdeps/cache/sccache.dag b/dag/extdeps/cache/sccache.dag index 8b4c7445151..abca5a5c62c 100644 --- a/dag/extdeps/cache/sccache.dag +++ b/dag/extdeps/cache/sccache.dag @@ -30,7 +30,23 @@ import std.cache_interface { import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } import std.types { NonEmptyStr, String, List } -import extdeps.toolchain.types { ToolchainCapability, SharedHomeAcrossJobs, CtrlBuild } +import extdeps.toolchain.types { + ToolchainCapability, + SharedHomeAcrossJobs, + CtrlBuild, + Architecture, + Aarch64, + X86_64, + X86, + Arm, + Armv7, + Mips, + Mipsel, + Mips64, + Mips64el, + Riscv64, + Wasm32, +} data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { uri: Uri { @@ -67,6 +83,10 @@ data sccache_toolchain_capability: ToolchainCapability = ToolchainCapability { data sccache_install_dissolution_trigger: String = "🟑 dissolve-on: sccache_install_script β€” the sccache binary install (curl release tarball + sha256sum -c verify + tar + mv to /usr/local/bin, cited to github.com/mozilla/sccache/releases with pinned v0.15.0 and per-arch sha256) is rendered as a POSIX shell provisioning sequence (medium-as-string); the SccacheBinaryRelease row is the typed authority for version and digests. DISSOLVES WHEN host_effect_apply binds a verified-download-plus-install effect (FetchAndVerify then InstallBinary) without the shell leaf." +data sccache_installed_binary_path_note: String = "Single authority for WHERE the cited release lands on a host. sccache_install_script writes it and every downstream consumer (the host-standup P1b systemd unit ExecStart, the PATH-shadow read-back check) reads it β€” so 'which sccache is the modeled one' has exactly one answer. Before this row the P1b provisioning path hand-rolled `apt-get install -y sccache` and a unit with ExecStart=/usr/bin/sccache while this module installed the pinned v0.15.0 tarball to /usr/local/bin: a Β§3 fork of one concept across two authorities, disagreeing on source, version, digest verification AND path, both firing on the same host (P1:runner-deploy-slot then P1b:build-cache-provision)." + +data sccache_installed_binary_path: String = "/usr/local/bin/sccache" + fn sccache_install_script(rel: SccacheBinaryRelease, arch: NonEmptyStr, digest: Digest) -> String { let dir = join(["sccache-", rel.version as String, "-", arch as String, "-unknown-linux-musl"], "") let url = join(["https://github.com/mozilla/sccache/releases/download/", rel.version as String, "/", dir, ".tar.gz"], "") @@ -75,19 +95,61 @@ fn sccache_install_script(rel: SccacheBinaryRelease, arch: NonEmptyStr, digest: join(["curl -fsSL '", url, "' -o /tmp/sccache.tar.gz"], ""), digest_shell_verify_line(digest: digest, file_path: "/tmp/sccache.tar.gz"), "tar -xzf /tmp/sccache.tar.gz -C /tmp", - join(["sudo mv '/tmp/", dir, "/sccache' /usr/local/bin/sccache"], ""), - "sudo chmod +x /usr/local/bin/sccache", + join(["sudo mv '/tmp/", dir, "/sccache' ", sccache_installed_binary_path], ""), + join(["sudo chmod +x ", sccache_installed_binary_path], ""), join(["rm -rf /tmp/sccache.tar.gz '/tmp/", dir, "'"], ""), "", ], "\n") } +data sccache_release_arch_selection_note: String = "The release row carries per-arch digests as two named fields, so selecting one by hand is how a caller pins an arch (runner_host_sccache_provision_aarch64). These two selectors make the choice a total function of the modeled Architecture coproduct instead: every arch the cited release does NOT publish a musl tarball for returns Absent, so an unsupported host REFUSES rather than silently receiving an aarch64 binary. Fail-closed by construction (Β§5) β€” there is no default arm." + +fn sccache_release_arch_token(arch: Architecture) -> NonEmptyStr? { + match arch { + Aarch64 => Present { value: "aarch64" as NonEmptyStr } + X86_64 => Present { value: "x86_64" as NonEmptyStr } + X86 => none + Arm => none + Armv7 => none + Mips => none + Mipsel => none + Mips64 => none + Mips64el => none + Riscv64 => none + Wasm32 => none + } +} + +fn sccache_release_digest(rel: SccacheBinaryRelease, arch: Architecture) -> Digest? { + match arch { + Aarch64 => Present { value: rel.digest_aarch64 } + X86_64 => Present { value: rel.digest_x86_64 } + X86 => none + Arm => none + Armv7 => none + Mips => none + Mipsel => none + Mips64 => none + Mips64el => none + Riscv64 => none + Wasm32 => none + } +} + data sccache_fatal_error_log_fragment: String = "sccache: encountered fatal error" data sccache_rustc_wrapper_exit_254_log_fragment: String = "(exit status: 254)" data sccache_failed_to_execute_compile_log_fragment: String = "sccache: error: failed to execute compile" +data sccache_misconfigured_log_fragments_note: String = "The cited roster of stdout/stderr fragments that mean 'the daemon answered, but it is misconfigured' β€” as a LIST, so a consumer classifying an observation folds over it. The three rows above were previously read one-by-one by a hand-unrolled if/elif chain in the host-standup provisioning emitter, which meant citing a fourth fragment here required an edit there too (the emitter naming a concept it does not own). Consumers iterate this roster; adding a row costs zero emitter edits." + +data sccache_misconfigured_log_fragments: List = [ + sccache_fatal_error_log_fragment, + sccache_rustc_wrapper_exit_254_log_fragment, + sccache_failed_to_execute_compile_log_fragment, +] + data sccache_local_facts: CacheInterfaceCatalogFacts = { identity: sccache_local_id backing_surface: "sccache-local-disk" diff --git a/dag/extdeps/dhcp/v4.dag b/dag/extdeps/dhcp/v4.dag index b9ea57d4b5f..8ee2e09ae32 100644 --- a/dag/extdeps/dhcp/v4.dag +++ b/dag/extdeps/dhcp/v4.dag @@ -18,15 +18,11 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { type MacAddress = NonEmptyStr where brand("MacAddress") -type Ipv4Address = NonEmptyStr where brand("Ipv4Address") - data dissolve_on_mac_address_anemic_brand: List = [ "closure:decompose_mac_address_octets|MacAddress is a branded NonEmptyStr hiding six grounded octets; deep-decompose to structured MAC carrier (e.g. MacAddress { octets: [UInt8; 6] }) at parse boundary|trigger:extdeps/network/mac.dag lands with parse_mac_address witness" ] -data dissolve_on_ipv4_address_anemic_brand: List = [ - "closure:decompose_ipv4_address_octets|Ipv4Address is a branded NonEmptyStr hiding four grounded octets; deep-decompose to structured IPv4 carrier at parse boundary|trigger:extdeps/network/ipv4.dag lands with parse_ipv4_address witness" -] +data ipv4_address_brand_dissolved_note: String = "The Ipv4Address anemic brand (NonEmptyStr where brand) was dissolved 2026-07-24: it is now the structured four-octet carrier in extdeps.network.ipv4 (dissolve_on_ipv4_address_anemic_brand fired β€” its named trigger, extdeps/network/ipv4.dag + parse_ipv4_address witness, landed). Consumers import Ipv4Address from extdeps.network.ipv4 directly (ipv4 is a network concept, not a DHCP one β€” the prior re-home through this module was a layering artifact). The MacAddress brand above remains anemic; its dissolution (extdeps/network/mac.dag, hex-octet parse) is the fast-follow β€” same consumer files, deferred to keep the IPv4 reach-lane change focused." type DhcpClientHostNameOption12 = HostName diff --git a/dag/extdeps/network/address.dag b/dag/extdeps/network/address.dag new file mode 100644 index 00000000000..5c385f6796a --- /dev/null +++ b/dag/extdeps/network/address.dag @@ -0,0 +1,49 @@ +module extdeps.network.address + +import std.types { String, Bool, NonEmptyStr } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import extdeps.network.ipv4 { Ipv4Address, render_ipv4_address } +import extdeps.network.ipv6 { Ipv6Address, ipv6_is_loopback } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https, + locator: "www.iana.org/assignments/address-family-numbers/address-family-numbers.xhtml", + } +} + +data ip_address_note: String = "An IP address is v4 OR v6 (RFC 791 / RFC 4291) β€” the honestly CLOSED coproduct over the two grounded address leaves, not a string. The v4 arm is fully grounded with a wire codec (extdeps.network.ipv4); the v6 arm's type is grounded but its string codec is staged (extdeps.network.ipv6, zero fleet consumers). render_ip_address is fail-closed on the v6 arm β€” it returns Absent rather than fabricating a v6 string until that codec lands (Β§5), so no consumer can accidentally emit a wrong v6 literal. Constructors ip_v4 / ip_v6 are the tagged injections." + +type IpAddress = + IpV4 { v4: Ipv4Address } + | IpV6 { v6: Ipv6Address } + +fn ip_v4(addr: Ipv4Address) -> IpAddress { + IpV4 { v4: addr } +} + +fn ip_v6(addr: Ipv6Address) -> IpAddress { + IpV6 { v6: addr } +} + +fn render_ip_address(addr: IpAddress) -> NonEmptyStr? { + match addr { + IpV4 { v4: a } => Present { value: render_ipv4_address(addr: a) } + IpV6 { v6: _ } => none + } +} + +fn ip_address_is_v4(addr: IpAddress) -> Bool { + match addr { + IpV4 { v4: _ } => true + IpV6 { v6: _ } => false + } +} + +fn ip_address_is_loopback(addr: IpAddress) -> Bool { + match addr { + IpV4 { v4: a } => a.octet1 == 127 + IpV6 { v6: a } => ipv6_is_loopback(addr: a) + } +} diff --git a/dag/extdeps/network/endpoint.dag b/dag/extdeps/network/endpoint.dag new file mode 100644 index 00000000000..4bf82bb14e4 --- /dev/null +++ b/dag/extdeps/network/endpoint.dag @@ -0,0 +1,47 @@ +module extdeps.network.endpoint + +import std.types { String, Bool, NonEmptyStr, Port } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import extdeps.dns.domain_name { HostName, DomainName, domain_name_wire } +import extdeps.network.address { IpAddress, render_ip_address, ip_v4 } +import extdeps.network.ipv4 { Ipv4Address } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https, + locator: "www.rfc-editor.org/rfc/rfc3986#section-3.2.2", + } +} + +data network_host_note: String = "A reachable host reference is a NAME or a literal ADDRESS β€” the two ways ssh/connect targets are actually written (an ssh_host is exactly this, today a bare NonEmptyStr). Reuses the already-grounded authorities: extdeps.dns.domain_name.HostName (RFC 1123, with its real label constraints) for the name arm, extdeps.network.address.IpAddress for the address arm β€” no fresh nickname. This is the leaf the transport model's `ssh_host: NonEmptyStr` grounds onto, and the payload of a network Reach (extdeps.network.reach)." + +type NetworkHost = + HostByName { name: HostName } + | HostByAddress { address: IpAddress } + +fn host_by_name(name: HostName) -> NetworkHost { + HostByName { name: name } +} + +fn host_by_ipv4(addr: Ipv4Address) -> NetworkHost { + HostByAddress { address: ip_v4(addr: addr) } +} + +fn render_network_host(host: NetworkHost) -> NonEmptyStr? { + match host { + HostByName { name: n } => Present { value: domain_name_wire(name: n.name) as NonEmptyStr } + HostByAddress { address: a } => render_ip_address(addr: a) + } +} + +data socket_address_note: String = "A transport endpoint: a host reference paired with a port. Reuses std.types.Port (the Int-where-range(1,65535) authority) verbatim β€” the port bound is not re-declared here. A SocketAddress is what a connect() targets; a bare NetworkHost (no port) is the ssh-config-style reference where the port is defaulted by the protocol." + +type SocketAddress { + host: NetworkHost + port: Port +} + +fn socket_address(host: NetworkHost, port: Port) -> SocketAddress { + SocketAddress { host: host, port: port } +} diff --git a/dag/extdeps/network/ipv4.dag b/dag/extdeps/network/ipv4.dag new file mode 100644 index 00000000000..3c0f06cab73 --- /dev/null +++ b/dag/extdeps/network/ipv4.dag @@ -0,0 +1,100 @@ +module extdeps.network.ipv4 + +import std.types { Int, String, Bool, NonEmptyStr, List } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https, + locator: "www.rfc-editor.org/rfc/rfc791", + } +} + +data ipv4_dotted_decimal_authority: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https, + locator: "www.rfc-editor.org/rfc/rfc790", + } +} + +data ipv4_grounding_note: String = "Structured IPv4 address β€” the dissolution of extdeps.dhcp.v4.Ipv4Address's anemic 'NonEmptyStr where brand(Ipv4Address)' (its dissolve_on_ipv4_address_anemic_brand named THIS module and a parse_ipv4_address witness). An IPv4 address is four octets (RFC 791 Β§3.1 β€” a 32-bit address), written in dotted-decimal (RFC 790 conventions); the octet is the grounded unit, a 0..255 bound modeled with the same `Int where range` refinement std.types.Port already uses for network numerics (NOT a fresh nickname β€” reuses the established bound idiom). Two entry points, per the model/realization split: ipv4_address(...) constructs from four octets for AUTHORED literals (byte-known at author time), parse_ipv4_address(String) recovers structure from WIRE text (DHCP tables, ip output) and REFUSES malformed input with a typed, located Ipv4ParseError rather than fabricating an address (Β§5 fail-closed). Round-trip (parse ∘ render == id on valid; render ∘ parse == id) is the witness." + +type Octet = Int where range(min: 0, max: 255) + +type Ipv4Address { + octet1: Octet + octet2: Octet + octet3: Octet + octet4: Octet +} + +type Ipv4ParseError = + Ipv4WrongOctetCount { observed_count: Int } + | Ipv4OctetNotNumeric { position: Int, raw: String } + | Ipv4OctetOutOfRange { position: Int, value: Int } + +type Ipv4ParseResult = + Ipv4Parsed { address: Ipv4Address } + | Ipv4ParseFailed { error: Ipv4ParseError } + +fn ipv4_address(octet1: Octet, octet2: Octet, octet3: Octet, octet4: Octet) -> Ipv4Address { + Ipv4Address { + octet1: octet1, + octet2: octet2, + octet3: octet3, + octet4: octet4, + } +} + +fn render_ipv4_address(addr: Ipv4Address) -> NonEmptyStr { + join([ + to_string(addr.octet1), + to_string(addr.octet2), + to_string(addr.octet3), + to_string(addr.octet4), + ], ".") as NonEmptyStr +} + +type OctetResult = + OctetOk { value: Octet } + | OctetErr { error: Ipv4ParseError } + +fn parse_octet_at(parts: List, position: Int) -> OctetResult { + match parts |> get(position) { + Absent => OctetErr { error: Ipv4WrongOctetCount { observed_count: list_length(items: parts) } } + Present { value: raw } => + match parse_int(s: raw) { + Absent => OctetErr { error: Ipv4OctetNotNumeric { position: position, raw: raw } } + Present { value: n } => + if n < 0 || n > 255 { + OctetErr { error: Ipv4OctetOutOfRange { position: position, value: n } } + } else { + OctetOk { value: n } + } + } + } +} + +fn parse_ipv4_address(text: String) -> Ipv4ParseResult { + let parts = split(s: text, delimiter: ".") + if list_length(items: parts) != 4 { + Ipv4ParseFailed { error: Ipv4WrongOctetCount { observed_count: list_length(items: parts) } } + } else { + match parse_octet_at(parts: parts, position: 0) { + OctetErr { error: e0 } => Ipv4ParseFailed { error: e0 } + OctetOk { value: o1 } => match parse_octet_at(parts: parts, position: 1) { + OctetErr { error: e1 } => Ipv4ParseFailed { error: e1 } + OctetOk { value: o2 } => match parse_octet_at(parts: parts, position: 2) { + OctetErr { error: e2 } => Ipv4ParseFailed { error: e2 } + OctetOk { value: o3 } => match parse_octet_at(parts: parts, position: 3) { + OctetErr { error: e3 } => Ipv4ParseFailed { error: e3 } + OctetOk { value: o4 } => Ipv4Parsed { + address: Ipv4Address { octet1: o1, octet2: o2, octet3: o3, octet4: o4 } + } + } + } + } + } + } +} diff --git a/dag/extdeps/network/ipv6.dag b/dag/extdeps/network/ipv6.dag new file mode 100644 index 00000000000..2dd2ab49b7d --- /dev/null +++ b/dag/extdeps/network/ipv6.dag @@ -0,0 +1,53 @@ +module extdeps.network.ipv6 + +import std.types { Int, String, Bool, NonEmptyStr, List } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https, + locator: "www.rfc-editor.org/rfc/rfc4291", + } +} + +data ipv6_text_representation_authority: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https, + locator: "www.rfc-editor.org/rfc/rfc5952", + } +} + +data ipv6_grounding_note: String = "Structured IPv6 address (RFC 4291 Β§2.5): eight 16-bit groups. The group is the grounded unit β€” a 0..65535 bound modeled with the same `Int where range` refinement std.types.Port uses (reuses the bound idiom, not a fresh nickname), parallel to extdeps.network.ipv4's octet. STAGED CODEC (deliberate, Β§6): the TYPE and constructor are grounded, but the string codec (canonical text form, RFC 5952 β€” lowercase hex groups with :: run-length compression) is NOT built here. It is a decode/encode over extdeps.numeric.base16 (the cited hex authority β€” render via its int-to-hex, parse via a reverse-fold over base16_digit_rows), and there are ZERO IPv6 addresses in the fleet today, so building a wire parser now would be building for a host that does not diverge. The codec lands when a real v6 address needs (de)serializing β€” dissolution trigger below. This keeps IpAddress an HONESTLY CLOSED coproduct (an IP is v4 or v6) with a grounded v6 arm, without an anemic string or a speculative parser." + +data dissolve_on_ipv6_text_codec_staged: List = [ + "closure:ipv6_text_codec|Ipv6Address has no RFC 5952 string parse/render yet; it reuses extdeps.numeric.base16 (render) and a reverse-fold over base16_digit_rows (parse), with :: compression|trigger:the first fleet IPv6 address needs ingesting or emitting (parse_ipv6_address / render_ipv6_address land with a round-trip witness)" +] + +type Hextet = Int where range(min: 0, max: 65535) + +type Ipv6Address { + group1: Hextet + group2: Hextet + group3: Hextet + group4: Hextet + group5: Hextet + group6: Hextet + group7: Hextet + group8: Hextet +} + +fn ipv6_address( + group1: Hextet, group2: Hextet, group3: Hextet, group4: Hextet, + group5: Hextet, group6: Hextet, group7: Hextet, group8: Hextet, +) -> Ipv6Address { + Ipv6Address { + group1: group1, group2: group2, group3: group3, group4: group4, + group5: group5, group6: group6, group7: group7, group8: group8, + } +} + +fn ipv6_is_loopback(addr: Ipv6Address) -> Bool { + addr.group1 == 0 && addr.group2 == 0 && addr.group3 == 0 && addr.group4 == 0 + && addr.group5 == 0 && addr.group6 == 0 && addr.group7 == 0 && addr.group8 == 1 +} diff --git a/dag/extdeps/network/reach.dag b/dag/extdeps/network/reach.dag new file mode 100644 index 00000000000..15d246b2771 --- /dev/null +++ b/dag/extdeps/network/reach.dag @@ -0,0 +1,75 @@ +module extdeps.network.reach + +import std.types { String, Bool, List, NonEmptyStr, Int } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import extdeps.network.endpoint { NetworkHost } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https, + locator: "man.openbsd.org/ssh_config#ProxyJump", + } +} + +data reach_proxycommand_authority: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https, + locator: "man.openbsd.org/ssh_config#ProxyCommand", + } +} + +data reach_note: String = "How packets get to a host β€” a network-reach fact, DELIBERATELY INDEPENDENT of the shell/execution transport (operator rule 2026-07-24: 'the network transport should be independent of the shell transport'). This module names NO shell mechanism; a Reach says only how the host is reachable, and the same Reach can carry any interpreter. Three grounded arms, cited to OpenSSH ssh_config: DirectLan (the host is directly on the segment); ProxyJump (reach the target THROUGH one or more jump hosts β€” the real, documented `-J` / ProxyJump feature, ProxyCommand being its general form); FabricTunnel (the intended long-term reach over the network fabric). FabricTunnel does not work yet (operator: 'none of that actually works'), so it is modeled but REFUSES realization β€” reach_realizability returns ReachRefused{FabricTunnelNotOperational}, a typed/located/counted refusal, never a silent fall-through (Β§5). The operator-sanctioned interim for a fabric-only target (e.g. srv3) is a ProxyJump through something actually reachable (srv2) that stands in for the fabric β€” a NAMED interim with a dissolution trigger, not a hidden hack: the ProxyJump reach dissolves to FabricTunnel when tunneling is operational. The srv-specific reach ROWS live in the gunbc layer (a fleet host is not an extdeps concept); this module owns only the cited Reach model + its realizability gate." + +type Reach = + DirectLan { host: NetworkHost } + | ProxyJump { jumps: List, target: NetworkHost } + | FabricTunnel { target: NetworkHost } + +type ReachRefusalCause = + FabricTunnelNotOperational + | ProxyJumpChainEmpty + +type ReachRealizability = + ReachRealizable + | ReachRefused { cause: ReachRefusalCause } + +fn direct_lan(host: NetworkHost) -> Reach { + DirectLan { host: host } +} + +fn proxy_jump(jumps: List, target: NetworkHost) -> Reach { + ProxyJump { jumps: jumps, target: target } +} + +fn fabric_tunnel(target: NetworkHost) -> Reach { + FabricTunnel { target: target } +} + +fn reach_target(reach: Reach) -> NetworkHost { + match reach { + DirectLan { host: h } => h + ProxyJump { jumps: _, target: t } => t + FabricTunnel { target: t } => t + } +} + +fn reach_realizability(reach: Reach) -> ReachRealizability { + match reach { + DirectLan { host: _ } => ReachRealizable + ProxyJump { jumps: js, target: _ } => + if list_length(items: js) == 0 { + ReachRefused { cause: ProxyJumpChainEmpty } + } else { + ReachRealizable + } + FabricTunnel { target: _ } => ReachRefused { cause: FabricTunnelNotOperational } + } +} + +fn reach_is_realizable(reach: Reach) -> Bool { + match reach_realizability(reach: reach) { + ReachRealizable => true + ReachRefused { cause: _ } => false + } +} diff --git a/dag/extdeps/router/verizon_cr1000a.dag b/dag/extdeps/router/verizon_cr1000a.dag index 86e298a4dac..c673ec1562d 100644 --- a/dag/extdeps/router/verizon_cr1000a.dag +++ b/dag/extdeps/router/verizon_cr1000a.dag @@ -6,7 +6,6 @@ import extdeps.dhcp.v4 { DhcpLeaseAssignment, DhcpLeaseStatus, MacAddress, - Ipv4Address, DynamicLease, StaticReservation, DynamicDhcpLease, @@ -14,6 +13,7 @@ import extdeps.dhcp.v4 { Active, Inactive, } +import extdeps.network.ipv4 { Ipv4Address } import extdeps.vendor.verizon { verizon } import extdeps.vendor { Vendor } import extdeps.hardware { Hardware } diff --git a/dag/extdeps/toolchain/types.dag b/dag/extdeps/toolchain/types.dag index 7e99e58bc0d..a66e8180933 100644 --- a/dag/extdeps/toolchain/types.dag +++ b/dag/extdeps/toolchain/types.dag @@ -15,6 +15,24 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { type Architecture = X86_64 | X86 | Aarch64 | Arm | Armv7 | Mips | Mipsel | Mips64 | Mips64el | Riscv64 | Wasm32 +data architecture_diagnostic_name_note: String = "A total variant name for Architecture, for DIAGNOSTICS ONLY β€” a refusal that cannot say which architecture it refused is typed but not located (Β§5). Deliberately NOT a wire label: every upstream that names architectures does so differently (debian arm64, Go GOARCH, sccache's musl tarball token, grub EFI filenames), and each of those already lives with its own upstream as a partial projection that REFUSES the arches that upstream does not publish. Reusing this name as a wire label would re-coin those authorities and defeat their fail-closed arms, so it is named for its purpose." + +fn architecture_diagnostic_name(arch: Architecture) -> NonEmptyStr { + match arch { + X86_64 => "X86_64" as NonEmptyStr + X86 => "X86" as NonEmptyStr + Aarch64 => "Aarch64" as NonEmptyStr + Arm => "Arm" as NonEmptyStr + Armv7 => "Armv7" as NonEmptyStr + Mips => "Mips" as NonEmptyStr + Mipsel => "Mipsel" as NonEmptyStr + Mips64 => "Mips64" as NonEmptyStr + Mips64el => "Mips64el" as NonEmptyStr + Riscv64 => "Riscv64" as NonEmptyStr + Wasm32 => "Wasm32" as NonEmptyStr + } +} + type TripleVendor = UnknownVendor | Pc | Apple | W64 type Os = Linux | Macos | Windows | Freebsd | Android | Ios | Wasi type AbiEnv = NoneAbi | Gnu | GnuEabi | GnuEabihf | Musl | Msvc | AndroidAbi | Eabi | Eabihf diff --git a/dag/gunbc/ci_materialization.dag b/dag/gunbc/ci_materialization.dag index e973d263135..d4bdf598b28 100644 --- a/dag/gunbc/ci_materialization.dag +++ b/dag/gunbc/ci_materialization.dag @@ -272,15 +272,16 @@ fn ci_floor_resolve_receipt_gate_script() -> String { ) } +data ci_sccache_provider_skip_is_counted_note: String = "The skip arm is LOUD and COUNTED, not silent (Β§5: a degradation must be a typed, located, countable diagnostic so its frequency is observable and prioritizable). This guard was a bare `if` with no else until 2026-07-24 β€” when the daemon was down the release build simply ran uncached, and the deficit's frequency was zero by construction, so it never ranked for fixing (shellβ†’dag census Β§4.I lists it as an absorbing fallback). It is NOT yet a refusal: STEP 2 of the srvN build-cache design flips this to fail-closed, and that flip is operator-sequenced AFTER a live T4 read-back proves P1b provisioning converges on srv1/srv2/srv4 β€” refusing before then would red the whole fleet, which is why the interim is loudness rather than a wall. The receipt line names the host, so a single misconfigured runner is attributable rather than fleet-wide noise." + fn ci_sccache_provider_shell_injection() -> String { - concat( - "if sccache --show-stats >/dev/null 2>&1; then\n", - concat( - " echo \"RUSTC_WRAPPER=sccache\" >> \"$GITHUB_ENV\"\n", - concat( - " echo \"CARGO_INCREMENTAL=0\" >> \"$GITHUB_ENV\"\n", - "fi" - ) - ) - ) + join([ + "if sccache --show-stats >/dev/null 2>&1; then", + " echo \"RUSTC_WRAPPER=sccache\" >> \"$GITHUB_ENV\"", + " echo \"CARGO_INCREMENTAL=0\" >> \"$GITHUB_ENV\"", + " printf '%s\\n' \"CiSccacheProviderReceipt: provider=bound catalog=sccache_local\"", + "else", + " printf '%s\\n' \"CiSccacheProviderReceipt: provider=SKIPPED catalog=sccache_local host=$(hostname) cause=daemon-unavailable; the release build runs UNCACHED β€” a counted degradation, not a supported mode (host_build_cache_provision P1b should have converged this host)\"", + "fi", + ], "\n") } diff --git a/dag/gunbc/fleet_intent_network.dag b/dag/gunbc/fleet_intent_network.dag index c42ea824a16..7a4ec3d5008 100644 --- a/dag/gunbc/fleet_intent_network.dag +++ b/dag/gunbc/fleet_intent_network.dag @@ -22,6 +22,8 @@ data operator_host_srv2: HostIdentity = "srv2" data operator_host_srv3: HostIdentity = "srv3" data operator_host_srv4: HostIdentity = "srv4" +data network_endpoint_address_grounding_residual_note: String = "🟑 dissolve-on: the NetworkEndpoint.address / NetworkSegment.cidr / gateway literals in this file are still bare `\"192.168.1.x\"` / CIDR strings even though this same lane grounded the address leaves (extdeps.network.ipv4 Ipv4Address = 4 bounded Octets, extdeps.network.address IpAddress = IpV4|IpV6, and the DHCP lease rows migrated to the ipv4_address constructor). The octet decomposition is half-consumed here: product.network_topology.NetworkEndpoint.address is typed String, so grounding these sites means re-typing that field to extdeps.network.address.IpAddress (and cidr/gateway to their grounded carriers) and migrating every NetworkEndpoint/NetworkSegment consumer β€” a product-layer field change, not a gunbc-local edit, so it is deliberately deferred rather than half-done. DISSOLVES WHEN NetworkEndpoint.address re-grounds onto IpAddress; until then these literals are the Β§3 residual the reach lane closes, tracked here so the loop is visible rather than silently forked. The grounded rows the reach lane already built β€” gunbc.fleet_reach.srv2_lan_ipv4 / srv3_lan_ipv4 (extdeps.network.ipv4.Ipv4Address, consumed by srv3_reach) β€” are the CONVERGENCE TARGET these bare strings dissolve onto, not an independent second grounding: srv2/srv3's address becomes those rows when the field re-types, so the transitional dual representation is marked debt heading toward one authority, not a permanent fork." + data operator_lan_segment: NetworkSegment = NetworkSegment { cidr: "192.168.1.0/24", gateway: Present { value: "192.168.1.1" }, @@ -96,6 +98,16 @@ data srv4_host_lan_endpoint: NetworkEndpoint = NetworkEndpoint { locality: Lan, } +data srv3_host_lan_endpoint_note: String = "srv3's HOST OS endpoint, absent from this topology until 2026-07-24 β€” only srv3_bmc_endpoint (192.168.1.192) was modeled, so the model could name srv3's out-of-band controller but not the machine itself. Observed live from the operator's DHCP table (192.168.1.221, MAC 48:21:0B:81:C7:1D) and confirmed addressable by probe (sshd answers on :22). REACHABLE via the srv2 hop (corrected 2026-07-25): ubuntu@srv3 runs commands today authenticated by srv2's local node-orch key (proven live β€” hostname=srv3, aarch64, 128 cores). What is NOT yet present is the FLEET identity: the fleet-automation-ssh-key is authorized for no user on srv3 (born Jul 13 with ssh.authorized-keys EMPTY, hand-keyed post-install with node-orch@srv2 / briansrls@srv1 / macbook only), the B2 runner-user + A1 secret-materialization gap in gunbc.plans.fleet_subsumption_manual_gaps β€” a one-time host_authorized_keys_reconcile upsert over the working node-orch hop, not a networking fact and not an unreachable host. LEASE STATUS: as of 2026-07-24 the operator converted this to a STATIC reservation (192.168.1.221 ↔ MAC 48:21:0B:81:C7:1D), so the literal is now a fact rather than a lease-lifetime observation β€” matching the srv1/srv2 hosts and the srv1/srv2/srv3 BMCs. STILL DYNAMIC and therefore provisional: srv4's host (192.168.1.196) and srv4's BMC (192.168.1.195); those two literals remain only as stable as their leases until the operator reserves them. The DHCP-reservation act itself is an unmodeled manual step β€” a static-lease intent (MAC ↔ address binding on the operator's router) has no carrier here yet; see gunbc.plans.fleet_subsumption_manual_gaps for where that gap is tracked." + +data srv3_host_lan_endpoint: NetworkEndpoint = NetworkEndpoint { + label: "srv3-host-lan", + host: Present { value: operator_host_srv3 }, + address: "192.168.1.221", + role: HostOperatingSystem, + locality: Lan, +} + data srv1_tailscale_endpoint: NetworkEndpoint = NetworkEndpoint { label: "srv1-tailscale", host: Present { value: operator_host_srv1 }, @@ -131,6 +143,7 @@ data fleet_intent_network: NetworkTopology = NetworkTopology { operator_lan_gateway_endpoint, srv1_host_lan_endpoint, srv2_host_lan_endpoint, + srv3_host_lan_endpoint, srv4_host_lan_endpoint, srv1_bmc_endpoint, srv2_bmc_endpoint, diff --git a/dag/gunbc/fleet_reach.dag b/dag/gunbc/fleet_reach.dag new file mode 100644 index 00000000000..fe18268329e --- /dev/null +++ b/dag/gunbc/fleet_reach.dag @@ -0,0 +1,36 @@ +module gunbc.fleet_reach + +import std.types { String, Bool } +import extdeps.network.ipv4 { Ipv4Address, ipv4_address } +import extdeps.network.endpoint { NetworkHost, host_by_ipv4 } +import extdeps.network.reach { + Reach, + proxy_jump, + fabric_tunnel, + reach_is_realizable, + reach_target, +} + +data fleet_reach_grounded_address_note: String = "The grounded fleet host addresses β€” the SINGLE authority the gunbc.fleet_intent_network endpoint literals (still bare `\"192.168.1.x\"` strings, tracked by network_endpoint_address_grounding_residual_note) will consume when NetworkEndpoint.address re-grounds onto extdeps.network.address.IpAddress. Declaring them here as extdeps.network.ipv4.Ipv4Address (four bounded Octets) rather than re-parsing the bare strings is what keeps this a CONVERGENCE target and not a Β§3 fork: there is one grounded row per address, and the reach rows below consume it. srv2 = 192.168.1.188 (the reachable jump host), srv3 = 192.168.1.221 (the fabric-only target, static-leased 2026-07-24)." + +data srv2_lan_ipv4: Ipv4Address = ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 188) +data srv3_lan_ipv4: Ipv4Address = ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 221) + +data srv2_lan_reach_host: NetworkHost = host_by_ipv4(addr: srv2_lan_ipv4) +data srv3_lan_reach_host: NetworkHost = host_by_ipv4(addr: srv3_lan_ipv4) + +data srv3_reach_note: String = "How packets reach srv3's host OS β€” a network-reach fact, DELIBERATELY INDEPENDENT of the shell/auth transport that runs on srv3 once reached (operator rule 2026-07-24: 'the network transport should be independent of the shell transport'). srv3 is a fabric-only target: the intended long-term reach is FabricTunnel, which does not work yet ('none of that actually works'), so the operator-sanctioned interim is a ProxyJump through srv2 β€” something actually reachable that stands in for the fabric ('proxy to something actually reachable to the target (i.e. srv2) and pretend you are reaching it from a fabric β€” that is okay for now'). GROUNDED LIVE 2026-07-25: from srv2, `ssh -i ~/.node-orch/id_ed25519 ubuntu@192.168.1.221` runs a real command on srv3 (hostname=srv3, aarch64, 128 cores) β€” so the network reach via srv2 is realizable AND a shell path works, using srv2's local node-orch key which ubuntu@srv3's authorized_keys trusts. REALIZATION DETAIL: the reach realizes as NESTED EXEC (ssh srv2 'ssh srv3'), NOT a -J TCP tunnel β€” srv2 sets AllowTcpForwarding no, so a -J / -W attempt returns 'administratively prohibited'; the ProxyJump reach therefore realizes through the ProxyCommand-family nested-exec handler (also cited in reach.dag), which the reach abstraction is agnostic to (one reach, the realization srv2's policy permits). The reach-vs-shell split this model makes explicit still holds and is still worth keeping separate: reach_is_realizable(srv3_reach) is a NETWORK fact (packets flow via srv2), independent of WHICH identity authenticates once reached. The bootstrap identity (node-orch@srv2) works, and the FLEET identity (fleet-automation) was ADDED to ubuntu@srv3 on 2026-07-25 β€” the host_authorized_keys_reconcile srv3 upsert executed live over this hop (fleet-automation appended, the 3 pre-existing keys untouched per R5, backup taken), so srv3 now trusts the fleet identity too. srv3 was autoinstalled Jul 13 with empty ssh.authorized-keys and hand-keyed post-install; that A1/B2 drift is what the reconcile closed. NOT an unreachable host. DISSOLUTION TRIGGER: srv3_reach becomes FabricTunnel { target: srv3_lan_reach_host } when tunneling over the network fabric is operational; the ProxyJump-through-srv2 arm is a named interim, not a hidden hack, and it retires then." + +data srv3_reach: Reach = proxy_jump(jumps: [srv2_lan_reach_host], target: srv3_lan_reach_host) + +data srv3_reach_fabric_intended_note: String = "The intended long-term reach srv3_reach dissolves TO when the fabric works β€” modeled so the dissolution target is a real value, not just prose. It REFUSES realization today (reach_realizability -> ReachRefused { FabricTunnelNotOperational }), which is why srv3_reach uses the ProxyJump interim instead. This row is the dissolution trigger made concrete, not a second live reach." + +data srv3_reach_fabric_intended: Reach = fabric_tunnel(target: srv3_lan_reach_host) + +fn srv3_reach_is_realizable() -> Bool { + reach_is_realizable(reach: srv3_reach) +} + +fn srv3_reach_target() -> NetworkHost { + reach_target(reach: srv3_reach) +} diff --git a/dag/gunbc/host_authorized_keys_reconcile.dag b/dag/gunbc/host_authorized_keys_reconcile.dag new file mode 100644 index 00000000000..b2877fb6992 --- /dev/null +++ b/dag/gunbc/host_authorized_keys_reconcile.dag @@ -0,0 +1,88 @@ +module gunbc.host_authorized_keys_reconcile + +import std.types { String, List, Bool, NonEmptyStr } +import extdeps.access.ssh { SshPublicKey, SshKeyAlgorithm, ssh_key_algorithm_token } +import gunbc.fleet_ssh_access { + fleet_authorized_keys, + operator_macbook_ssh_key, + fleet_automation_ssh_key, +} +import gunbc.ownership { Ownership, Owned } +import gunbc.membership_reconcile { + MembershipPlan, + membership_reconcile, +} + +data host_authorized_keys_reconcile_authority_note: String = "Instantiates the grain-agnostic gunbc.membership_reconcile spine for one host's ~/.ssh/authorized_keys, keyed by SSH key IDENTITY. This is the durable fix for the srv3 first-contact gap (fleet_subsumption_manual_gaps A1/B2) AND for every future key rotation, both instances of the same silent drift: authorized_keys is materialized once at install and never re-converged against fleet_ssh_access.fleet_authorized_keys, so a key added to the model after a host was installed never reaches that host. srv3 is the live proof: installed via the pre-#7027 lane before fleet_automation_ssh_key existed, so its ubuntu authorized_keys carries the operator macbook key (operator reach) but NOT fleet-automation (workflow reach) β€” observed 2026-07-24. This module does NOT fork the spine: member = SshPublicKey, and the (key_of, key_eq, value_eq, ownership_of) bundle below is passed to the ONE membership_reconcile fn (a Realization β€” one fn, N bundles; a forked reconcile would mean the genericity bought nothing). key_of returns the key MATERIAL (the cryptographic identity), never the whole line, so a comment-only drift is Modified (re-upsert the line), not Remove+Add (which would delete then re-add the key)." + +fn authorized_key_identity(k: SshPublicKey) -> NonEmptyStr { + k.material +} + +fn authorized_key_identity_eq(a: NonEmptyStr, b: NonEmptyStr) -> Bool { + a == b +} + +fn ssh_algorithm_eq(a: SshKeyAlgorithm, b: SshKeyAlgorithm) -> Bool { + ssh_key_algorithm_token(a: a) == ssh_key_algorithm_token(a: b) +} + +fn authorized_key_value_eq(a: SshPublicKey, b: SshPublicKey) -> Bool { + ssh_algorithm_eq(a: a.algorithm, b: b.algorithm) + && (a.material == b.material) + && (a.comment == b.comment) +} + +data fleet_owned_key_materials_note: String = "The registry of key materials the FLEET manages β€” the ownership authority the R5 teardown-owned-only wall reads for a Removed key. DERIVED from fleet_authorized_keys (single authority, never a hand-copied material list), so today it is exactly the two declared fleet keys. A key NOT in this registry (an out-of-band key like node-orch@srv2 or briansrls@srv1 hand-added in the node-orch bootstrap era) has NO ownership record -> ownership_of returns Absent -> OwnershipUnknown -> the spine REFUSES to tear it down (fail-closed; we never delete a key we did not place). ROTATION EXTENSION (dissolution trigger, not built here): when a fleet key rotates, its retired material must be appended to a retired-owned list so the Removed old key resolves Owned -> teardown-eligible; until that lands, a rotated-out fleet key drops out of this derived registry and is REFUSED rather than removed β€” a safe leak, not a silent delete. That extension is what makes the Owned teardown arm non-degenerate; today every teardown-refusal is OwnershipUnknown by construction, which is honest for the srv3 case (zero teardowns needed)." + +fn fleet_owned_key_materials() -> List { + map(fleet_authorized_keys, k => k.material) +} + +fn authorized_key_ownership(k: SshPublicKey) -> Ownership? { + if any(fleet_owned_key_materials(), m => m == k.material) { + Present { value: Owned } + } else { + none + } +} + +data host_authorized_keys_reconcile_note: String = "desired = fleet_authorized_keys (the model's declared key set); observed = a live read of the host's authorized_keys (an OBSERVATION effect, staged β€” the fixtures below are point-in-time reads, not the live provider). The apply-grain POLICY is deliberately NOT resolved in this module: authorized_keys is an EVERYTHING-ON-HOST observed scope (foreign keys are normal, not anomalies), which is exactly the scope where membership_reconcile's wholesale-refuse policy (membership_effects) would be wrong β€” a foreign key's refusal would block our owned upsert. That is the conscious wholesale-vs-siblings-continue call the spine reserves to a human (membership_effects_wholesale_refuse_policy_note); this module produces the PLAN grain only and leaves the apply projection to that decision." + +fn host_authorized_keys_reconcile(observed: List) -> MembershipPlan { + membership_reconcile( + desired: fleet_authorized_keys, + observed: observed, + key_of: authorized_key_identity, + key_eq: authorized_key_identity_eq, + value_eq: authorized_key_value_eq, + ownership_of: authorized_key_ownership, + ) +} + +data srv3_observed_authorized_keys_note: String = "OBSERVED, not intended: a point-in-time read of ubuntu@192.168.1.221 ~/.ssh/authorized_keys, run by the operator from the macbook 2026-07-24 (the macbook key is the one credential that reaches srv3 today). node-orch@srv2 and briansrls@srv1 are out-of-band keys the fleet does not own; macbook-m4 is reused from fleet_ssh_access (single authority) since it is byte-identical to the declared operator key. This is a fixture standing in for the staged live observation provider, marked so it is never mistaken for a desired/intent row." + +data srv3_observed_node_orch_srv2_key: SshPublicKey = SshPublicKey { + algorithm: Ed25519, + material: "AAAAC3NzaC1lZDI1NTE5AAAAIIQp4ylHo8mQNGwvSg7ftW1LSXNFEPuwVjsDKvdqJnkj", + comment: "node-orch@srv2", +} + +data srv3_observed_briansrls_srv1_key: SshPublicKey = SshPublicKey { + algorithm: Ed25519, + material: "AAAAC3NzaC1lZDI1NTE5AAAAIL28hOj+Q0ddJuX7OUslZpJOuHMZGDxoXCR8MA6iWpdQ", + comment: "briansrls@srv1", +} + +data srv3_observed_authorized_keys: List = [ + srv3_observed_node_orch_srv2_key, + srv3_observed_briansrls_srv1_key, + operator_macbook_ssh_key, +] + +data srv4_observed_authorized_keys_note: String = "OBSERVED read of ubuntu@192.168.1.196 ~/.ssh/authorized_keys (operator, macbook, 2026-07-24). srv4 was installed via #7027 with fleet_authorized_keys in the seed, so it carries EXACTLY the two declared fleet keys and nothing foreign β€” the CONVERGED control: reconciling it against desired yields an empty plan (0 upsert / 0 teardown / 0 refusal). Both keys reused from fleet_ssh_access (single authority)." + +data srv4_observed_authorized_keys: List = [ + operator_macbook_ssh_key, + fleet_automation_ssh_key, +] diff --git a/dag/gunbc/host_build_cache_provision.dag b/dag/gunbc/host_build_cache_provision.dag index cccfe9d00d2..aace34c4402 100644 --- a/dag/gunbc/host_build_cache_provision.dag +++ b/dag/gunbc/host_build_cache_provision.dag @@ -37,11 +37,14 @@ data ci_sccache_opportunistic_detect_scaffold: Disposition = Scaffold { field: WholeDeclaration, } } +data build_cache_path_authority_observation_note: String = "CI and ctrl-build sessions consume the cache as bare `sccache` on PATH (RUSTC_WRAPPER=sccache), so provisioning the modeled binary is NOT sufficient β€” the PATH-visible sccache must BE the modeled one. A second sccache earlier in PATH (a distro package, a stale copy) is precisely the two-authority state this lane exists to remove, and it is invisible to a read-back that probes the absolute path: that read-back greens on the binary we provisioned while the compiler calls a different one. DaemonPathShadowed carries BOTH paths so the refusal is located (which binary won, which one was expected) rather than merely typed. This judgement is modeled HERE, in the verdict fold (proven by design_witness_path_shadow_refuses_fail_closed against a synthetic DaemonPathShadowed observation), not decided by the provisioning shell. Its LIVE observation is STAGED, not emitted: per the shellβ†’dag census this module's script side is an A5 `decompose` row that must not grow its emitted shell surface, so the `command -v sccache` resolve waits for the typed-argv dissolve-on (#5828) rather than landing as hand-shell now (review 42343). The model carries the state and its refusal today; only the live producer is deferred." + type BuildCacheDaemonObservation = DaemonStatsOk { stats_line: String } | DaemonAbsent | DaemonUnresponsive { detail: NonEmptyStr } | DaemonMisconfigured { matched_fragment: String, detail: NonEmptyStr } + | DaemonPathShadowed { resolved: String, expected: String } type BuildCacheProvisionRefusal = RefusalDaemonAbsent @@ -49,6 +52,7 @@ type BuildCacheProvisionRefusal | RefusalDaemonMisconfigured | RefusalPrivilegeDenied | RefusalCatalogUnknown + | RefusalPathShadowed type BuildCacheProvisionVerdict = ProvisionConverged { catalog_id: CacheInterfaceId, stats_line: String } @@ -73,6 +77,11 @@ fn provision_build_cache_absorbing_fallback_widen_sketch( cause: RefusalDaemonMisconfigured, reason: concat(concat(concat("host_build_cache_provision: ", frag), ": "), d) as NonEmptyStr, } + DaemonPathShadowed { resolved: r, expected: e } => + ProvisionConverged { + catalog_id: catalog_id, + stats_line: concat("path-shadow-widen-sketch: ", concat(r, concat(" vs ", e))), + } } } @@ -103,6 +112,12 @@ fn build_cache_provision_gate_accepts( ProvisionConverged { catalog_id: _, stats_line: _ } => false ProvisionRefused { cause: _, reason: _ } => false } + DaemonPathShadowed { resolved: _, expected: _ } => + match verdict { + ProvisionRefused { cause: RefusalPathShadowed, reason: _ } => true + ProvisionConverged { catalog_id: _, stats_line: _ } => false + ProvisionRefused { cause: _, reason: _ } => false + } } } @@ -132,6 +147,17 @@ fn provision_build_cache_verdict( cause: RefusalDaemonMisconfigured, reason: concat(concat(concat("host_build_cache_provision: ", frag), ": "), d) as NonEmptyStr, } + DaemonPathShadowed { resolved: r, expected: e } => + ProvisionRefused { + cause: RefusalPathShadowed, + reason: concat( + concat("host_build_cache_provision: PATH resolves sccache to ", r), + concat( + concat(" but the modeled install authority is ", e), + "; the compiler would call a binary this lane never provisioned. Fail-closed, no local-build fallback.", + ), + ) as NonEmptyStr, + } } } } diff --git a/dag/gunbc/host_build_cache_provision_script.dag b/dag/gunbc/host_build_cache_provision_script.dag index 16fb1d543ba..79730a6be79 100644 --- a/dag/gunbc/host_build_cache_provision_script.dag +++ b/dag/gunbc/host_build_cache_provision_script.dag @@ -1,17 +1,21 @@ module gunbc.host_build_cache_provision_script -import std.types { String, Bool } +import std.types { String, NonEmptyStr, Bool, List } import std.disposition { Disposition, Scaffold, SingleAuthority } import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.crypto.hash { Digest } import gunbc.shell_bash_runner { shell_exec_via_bash } import extdeps.cache.sccache { - sccache_fatal_error_log_fragment, - sccache_rustc_wrapper_exit_254_log_fragment, - sccache_failed_to_execute_compile_log_fragment, + sccache_misconfigured_log_fragments, + sccache_installed_binary_path, + sccache_install_script, + sccache_release_0_15_0, } data host_build_cache_provision_script_dissolution_trigger: String = "🟑 dissolve-on: host_build_cache_provision_script β€” concat-built systemd/sccache ensure shell; DISSOLVES WHEN bash-emit (#5828) realizes ProvisionBuildCache observe/ensure/read-back as typed host-effect argv and realize_provision_build_cache retires shell_exec_via_bash transport." +data host_build_cache_provision_script_census_row_note: String = "CENSUS STANDING: docs/plans/shell-to-dag-residual-census-and-arc-completion.md Β§4.A keys this file as the builder for host_effect_realize.ProvisionBuildCache, action DECOMPOSE, sub-class A5 (srv* cluster, deferred by operator 2026-07-22 β€” real debt, NOT done; un-defer trigger is the operator). This site is RUNTIME-PRESENT (it realizes through host_effect_apply_gated on LocalShell/SshShell), so per that doc's routing decision its end state is a typed effect-plan with NO bash emitted β€” the six *_body builders below are the debt, not the design. Standing constraint while the row is deferred, stated precisely (review 42401 sharpened this): NEW emitted shell must be either a DEDUCTION or a cited-de-fork SWAP β€” never an unbounded, uncited addition. Two exact deltas this PR made, both accounted: (1) the sccache DE-FORK swap β€” `apt-get install sccache` + an `ExecStart=/usr/bin/sccache` unit went OUT, and the cited-tarball install invocation (sccache_install_script, one authority row) came IN; that is the Β§3 fork removal this PR exists to make, a swap that de-duplicates rather than grows. (2) `sudo -n loginctl enable-linger \"$USER\"` is genuinely NEW shell, not a swap β€” acknowledged here as growth rather than hidden: it is the one primitive that makes the already-selected user-scope systemd handler viable at all (a `--user` manager is torn down with the login otherwise), justified in build_cache_user_service_linger_note, and it is bounded (a single fixed leaf, not a corpus-denominated fold). What must NOT grow is the PATH-shadow OBSERVATION: the judgement went to gunbc.host_build_cache_provision (DaemonPathShadowed / RefusalPathShadowed + verdict fold, witnessed against a synthetic observation), and its live shell observation is STAGED, NOT emitted here β€” an earlier attempt folded `command -v sccache` lines into the two existing bodies, which kept the builder count at six but still grew the shell surface (review 42343 rejected that as a census regression). The observation lands when ProvisionBuildCache realizes as typed argv (dissolve-on #5828). Adding a *_body, or an uncited emitted-shell leaf that is neither a deduction nor a de-fork swap, is a census regression even when the behaviour it adds is correct." + data host_build_cache_provision_script_scaffold: Disposition = Scaffold { dissolves_to: SingleAuthority, bind: DeclarationRef { @@ -21,172 +25,169 @@ data host_build_cache_provision_script_scaffold: Disposition = Scaffold { } } -data build_cache_systemd_user_unit_path: String = ".config/systemd/user/sccache.service" +data build_cache_install_authority_note: String = "The ensure arm installs sccache by calling the cited authority extdeps.cache.sccache.sccache_install_script (pinned release, per-arch sha256 verified, landing at sccache_installed_binary_path) β€” it does NOT hand-roll a package-manager install. Until 2026-07-24 this module ran `sudo -n apt-get install -y sccache` and wrote a unit with ExecStart=/usr/bin/sccache, a Β§3 fork of the same concept: P1:runner-deploy-slot installs the pinned tarball to /usr/local/bin and then P1b:build-cache-provision pointed its unit at a path that install never creates, so the daemon could not start and the read-back refused. Both the install and the unit now read ONE path row, so the two phases cannot disagree." + +data build_cache_systemd_user_unit_path: String = "$HOME/.config/systemd/user/sccache.service" + +fn build_cache_systemd_user_unit_body() -> String { + join([ + "[Unit]", + "Description=sccache compiler cache (gunbc host standup)", + "After=network.target", + "", + "[Service]", + "Type=simple", + join(["ExecStart=", sccache_installed_binary_path, " --start-server"], ""), + "Restart=on-failure", + "", + "[Install]", + "WantedBy=default.target", + "", + ], "\n") +} -data build_cache_systemd_user_unit_body: String = "[Unit]\nDescription=sccache compiler cache (gunbc host standup)\nAfter=network.target\n\n[Service]\nType=simple\nExecStart=/usr/bin/sccache --start-server\nRestart=on-failure\n\n[Install]\nWantedBy=default.target\n" +data build_cache_path_authority_note: String = "The PATH-shadow JUDGEMENT lives in the model β€” gunbc.host_build_cache_provision.DaemonPathShadowed / RefusalPathShadowed and the verdict fold that refuses it, proven by design_witness_path_shadow_refuses_fail_closed against a synthetic DaemonPathShadowed observation. Its LIVE OBSERVATION is STAGED, deliberately NOT emitted as hand-shell here: this file is an A5 `decompose` scaffold that the census pledges may SHRINK but must not GROW (dissolve-on #5828), and a `command -v sccache` observation folded into the bodies still GROWS the emitted shell surface β€” a census regression even though the model verdict it feeds is correct (review 42343 caught this; the earlier 'folded in, count six' defense counted *_body builders, not the shell surface). The observation lands when ProvisionBuildCache realizes as typed host-effect argv (this module's own dissolve-on): the resolve becomes a typed op (shell.Which.Check) and the comparison a typed predicate over captured values (the deploy-preflight `whoami` precedent: a negated StrEq, never a minted StrNeq). Until then the model carries the state and its refusal; only the live producer is deferred." fn build_cache_observe_stats_body() -> String { - concat( - "stats_rc=0\n", - concat( - "stats_out=\"$(sccache --show-stats 2>&1)\" || stats_rc=$?\n", - concat( - "if [ \"$stats_rc\" -eq 0 ]; then\n", - concat( - " printf '%s\\n' \"BuildCacheProvisionReceipt: observe=ok\"\n", - concat( - " printf '%s\\n' \"$stats_out\"\n", - " exit 0\n", - ) - ) - ) - ) + join([ + "stats_out=\"\"", + "stats_rc=0", + join(["if [ -x '", sccache_installed_binary_path, "' ]; then"], ""), + join([" stats_out=\"$('", sccache_installed_binary_path, "' --show-stats 2>&1)\" || stats_rc=$?"], ""), + "else", + " printf '%s\\n' \"BuildCacheProvisionReceipt: observe=absent\"", + " stats_rc=127", + "fi", + "if [ \"$stats_rc\" -eq 0 ]; then", + " printf '%s\\n' \"BuildCacheProvisionReceipt: observe=ok\"", + " printf '%s\\n' \"$stats_out\"", + " exit 0", + "fi", + "", + ], "\n") +} + +fn build_cache_fragment_word(fragment: String) -> String { + join(["'", fragment, "'"], "") +} + +fn build_cache_fragment_words() -> String { + join( + map(sccache_misconfigured_log_fragments, f => build_cache_fragment_word(fragment: f)), + " ", ) } +data build_cache_classify_fold_note: String = "The misconfigured-fragment classifier is a FOLD over the cited roster extdeps.cache.sccache.sccache_misconfigured_log_fragments, not one emitted branch per fragment. It was a hand-unrolled 3-way if/elif chain until 2026-07-24, which meant the emitter named each cited fragment individually and a fourth citation could not take effect without an edit here. The roster is now data the loop iterates: adding a fragment upstream changes the emitted word list and nothing else. Fragments are single-quoted as shell words, which is total only while no fragment contains a single quote β€” build_cache_fragment_words_are_shell_safe() is the construction check that keeps it so." + fn build_cache_classify_failure_body() -> String { - concat( - concat( - concat( - "if printf '%s' \"$stats_out\" | grep -Fq ", - concat("\"", sccache_fatal_error_log_fragment), - ), - "\"; then\n", - ), - concat( - concat( - concat( - " printf '%s\\n' \"BuildCacheProvisionReceipt: observe=misconfigured fragment=", - sccache_fatal_error_log_fragment, - ), - "\"\n", - ), - concat( - concat( - concat( - "elif printf '%s' \"$stats_out\" | grep -Fq ", - concat("\"", sccache_rustc_wrapper_exit_254_log_fragment), - ), - "\"; then\n", - ), - concat( - concat( - concat( - " printf '%s\\n' \"BuildCacheProvisionReceipt: observe=misconfigured fragment=", - sccache_rustc_wrapper_exit_254_log_fragment, - ), - "\"\n", - ), - concat( - concat( - concat( - "elif printf '%s' \"$stats_out\" | grep -Fq ", - concat("\"", sccache_failed_to_execute_compile_log_fragment), - ), - "\"; then\n", - ), - concat( - concat( - concat( - " printf '%s\\n' \"BuildCacheProvisionReceipt: observe=misconfigured fragment=", - sccache_failed_to_execute_compile_log_fragment, - ), - "\"\n", - ), - "else\n printf '%s\\n' \"BuildCacheProvisionReceipt: observe=unresponsive\"\nfi\n" - ) - ) - ) - ) - ) - ) + join([ + "observe_class=unresponsive", + "observe_fragment=\"\"", + join(["for frag in ", build_cache_fragment_words(), "; do"], ""), + " if printf '%s' \"$stats_out\" | grep -Fq \"$frag\"; then", + " observe_class=misconfigured", + " observe_fragment=\"$frag\"", + " break", + " fi", + "done", + "if [ \"$observe_class\" = misconfigured ]; then", + " printf '%s\\n' \"BuildCacheProvisionReceipt: observe=misconfigured fragment=$observe_fragment\"", + "else", + " printf '%s\\n' \"BuildCacheProvisionReceipt: observe=unresponsive\"", + "fi", + "", + ], "\n") } -fn build_cache_ensure_daemon_body() -> String { - concat( - "if ! command -v sccache >/dev/null 2>&1; then\n", - concat( - " sudo -n apt-get update -qq && sudo -n apt-get install -y sccache\n", - concat( - "fi\n", - concat( - concat("mkdir -p \"$(dirname ", build_cache_systemd_user_unit_path, ")\""), - concat( - "\n", - concat( - concat("cat > ", build_cache_systemd_user_unit_path, " <<'__GUNBC_SCCACHE_UNIT__'\n"), - concat( - build_cache_systemd_user_unit_body, - concat( - "__GUNBC_SCCACHE_UNIT__\n", - "systemctl --user daemon-reload\nsystemctl --user enable --now sccache.service\n", - ) - ) - ) - ) - ) - ) - ) - ) +fn build_cache_ensure_daemon_body(arch_token: NonEmptyStr, digest: Digest) -> String { + join([ + join(["if [ ! -x '", sccache_installed_binary_path, "' ]; then"], ""), + sccache_install_script(rel: sccache_release_0_15_0, arch: arch_token, digest: digest), + "fi", + join(["mkdir -p \"$(dirname \"", build_cache_systemd_user_unit_path, "\")\""], ""), + join(["cat > \"", build_cache_systemd_user_unit_path, "\" <<'__GUNBC_SCCACHE_UNIT__'"], ""), + build_cache_systemd_user_unit_body(), + "__GUNBC_SCCACHE_UNIT__", + "sudo -n loginctl enable-linger \"$USER\"", + "systemctl --user daemon-reload", + "systemctl --user enable --now sccache.service", + "", + ], "\n") +} + +data build_cache_user_service_linger_note: String = "A `systemd --user` manager is torn down when the user's last session ends, so on a headless runner host an enabled user unit stops the moment the provisioning ssh connection closes β€” the daemon would be observed healthy by the read-back in the same connection and be gone before the first CI job. enable-linger keeps the manager running without a login, which is what makes the user-scope handler viable at all. It does NOT settle open question 1 of the srvN build-cache design (user service vs system service for the shared daemon) β€” that handler choice is still operator-open; this only makes the handler already selected in tree behave as modeled." + +fn build_cache_read_back_body(binary: String) -> String { + join([ + join(["if stats_out=\"$('", binary, "' --show-stats 2>&1)\"; then"], ""), + " printf '%s\\n' \"BuildCacheProvisionReceipt: read_back=ok\"", + " printf '%s\\n' \"$stats_out\"", + " exit 0", + "else", + " printf '%s\\n' \"BuildCacheProvisionReceipt: read_back=FAILED sccache unhealthy after ensure\"", + " printf '%s\\n' \"$stats_out\"", + " exit 1", + "fi", + "", + ], "\n") +} + +fn build_cache_provision_script_body(arch_token: NonEmptyStr, digest: Digest) -> String { + join([ + "set -euo pipefail", + build_cache_observe_stats_body(), + build_cache_classify_failure_body(), + "printf '%s\\n' \"BuildCacheProvisionReceipt: ensure=starting\"", + build_cache_ensure_daemon_body(arch_token: arch_token, digest: digest), + build_cache_read_back_body(binary: sccache_installed_binary_path), + ], "\n") +} + +fn build_cache_provision_read_back_fails_closed() -> Bool { + let body = build_cache_read_back_body(binary: sccache_installed_binary_path) + string_contains(s: body, pattern: "read_back=FAILED") + && string_contains(s: body, pattern: "exit 1") + && !string_contains(s: body, pattern: "stats_rc") } -fn build_cache_read_back_body() -> String { - concat( - "if stats_out=\"$(sccache --show-stats 2>&1)\"; then\n", - concat( - " printf '%s\\n' \"BuildCacheProvisionReceipt: read_back=ok\"\n", - concat( - " printf '%s\\n' \"$stats_out\"\n", - concat( - " exit 0\n", - concat( - "else\n", - concat( - " printf '%s\\n' \"BuildCacheProvisionReceipt: read_back=FAILED sccache unhealthy after ensure\"\n", - concat( - " printf '%s\\n' \"$stats_out\"\n", - " exit 1\n", - ) - ) - ) - ) - ) - ) +fn build_cache_fragment_words_are_shell_safe() -> Bool { + fold( + sccache_misconfigured_log_fragments, + init: true, + f: (acc, frag) => acc && !string_contains(s: frag, pattern: "'"), ) } -fn build_cache_provision_script_body() -> String { - concat( - "set -euo pipefail\n", - concat( - build_cache_observe_stats_body(), - concat( - build_cache_classify_failure_body(), - concat( - "printf '%s\\n' \"BuildCacheProvisionReceipt: ensure=starting\"\n", - concat( - build_cache_ensure_daemon_body(), - build_cache_read_back_body(), - ) - ) - ) - ) +fn build_cache_install_is_cited_not_package_manager() -> Bool { + let body = build_cache_provision_script_body( + arch_token: "aarch64" as NonEmptyStr, + digest: sccache_release_0_15_0.digest_aarch64, ) + string_contains(s: body, pattern: "github.com/mozilla/sccache/releases/download/") + && string_contains(s: body, pattern: sccache_release_0_15_0.version as String) + && !string_contains(s: body, pattern: "apt-get install") + && !string_contains(s: body, pattern: "/usr/bin/sccache") } -fn build_cache_provision_read_back_fails_closed() -> Bool { +fn build_cache_unit_execstart_matches_install_path() -> Bool { string_contains( - s: build_cache_read_back_body(), - pattern: "read_back=FAILED", - ) && string_contains( - s: build_cache_read_back_body(), - pattern: "exit 1", - ) && !string_contains( - s: build_cache_read_back_body(), - pattern: "stats_rc", + s: build_cache_systemd_user_unit_body(), + pattern: join(["ExecStart=", sccache_installed_binary_path], ""), + ) +} + +fn build_cache_classifier_covers_every_cited_fragment() -> Bool { + fold( + sccache_misconfigured_log_fragments, + init: true, + f: (acc, frag) => + acc && string_contains(s: build_cache_classify_failure_body(), pattern: frag), ) } -fn build_cache_provision_shell_script() -> String { - shell_exec_via_bash(body: build_cache_provision_script_body()) +fn build_cache_provision_shell_script(arch_token: NonEmptyStr, digest: Digest) -> String { + shell_exec_via_bash( + body: build_cache_provision_script_body(arch_token: arch_token, digest: digest), + ) } diff --git a/dag/gunbc/host_effect_realize.dag b/dag/gunbc/host_effect_realize.dag index 07ae399e2eb..48513ef9499 100644 --- a/dag/gunbc/host_effect_realize.dag +++ b/dag/gunbc/host_effect_realize.dag @@ -54,7 +54,8 @@ import gunbc.typed_argv_exec { TypedArgvExecRefused, } import extdeps.bmc.types { RedfishSystemAction } -import gunbc.fleet_intent { ComputeHost, srv1_host } +import gunbc.fleet_intent { ComputeHost, srv1_host, compute_host_primary_cpu } +import extdeps.toolchain.types { Architecture, architecture_diagnostic_name } import gunbc.host_converge { HostConverge, FreshStandup, ExistingHostQuiescentReload, gunbc_apply_mode_for_host } import gunbc.host_converge_realize { interpret_host_converge, @@ -108,7 +109,12 @@ import gunbc.host_build_cache_catalog_gate { ProvisionBuildCacheCatalogRealizable, ProvisionBuildCacheCatalogRefused, } -import extdeps.cache.sccache { sccache_local_id } +import extdeps.cache.sccache { + sccache_local_id, + sccache_release_0_15_0, + sccache_release_arch_token, + sccache_release_digest, +} import gunbc.srv3_os_install_reconcile_types { srv3_boot_once_approval_grant_path, srv3_boot_once_apply_read_back_sleep, @@ -707,9 +713,12 @@ fn realize_bmcweb_token_extract_on_host( } } -fn srv3_toolchain_ensure_reconcile( +data toolchain_ensure_reconcile_located_note: String = "The refusal names the effect that produced it. This fold was written for OsInstallActuatorToolchainEnsure and hardcoded that effect in its failure header; when ProvisionBuildCache started reusing it (P1b:build-cache-provision), every build-cache refusal reported itself as an OS-install-actuator failure β€” a located diagnostic pointing at the wrong location, which is the Β§5 'typed, located' bar failing at the second half. The header is now a parameter supplied by each realize arm." + +fn toolchain_ensure_reconcile( observed: ShellExecObserved, intent: HostEffectIntent, + effect_label: String, ) -> Reconciliation { let grounding = if observed.success { Grounds { evidence: ShellEffectApplied { exit_code: observed.exit_code, stdout: observed.stdout } } @@ -717,7 +726,14 @@ fn srv3_toolchain_ensure_reconcile( DoesNotGround { reason: shell_exec_failure_reason_headered( observed: observed, - header: "host_effect_apply: OsInstallActuatorToolchainEnsure synthesized receipt from typed per-tool ensure results; fail-closed", + header: join( + [ + "host_effect_apply: ", + effect_label, + " synthesized receipt from typed per-tool ensure results; fail-closed", + ], + "", + ), ), } } @@ -728,6 +744,28 @@ fn srv3_toolchain_ensure_reconcile( ) } +fn srv3_toolchain_ensure_reconcile( + observed: ShellExecObserved, + intent: HostEffectIntent, +) -> Reconciliation { + toolchain_ensure_reconcile( + observed: observed, + intent: intent, + effect_label: "OsInstallActuatorToolchainEnsure", + ) +} + +fn provision_build_cache_reconcile( + observed: ShellExecObserved, + intent: HostEffectIntent, +) -> Reconciliation { + toolchain_ensure_reconcile( + observed: observed, + intent: intent, + effect_label: "ProvisionBuildCache", + ) +} + fn realize_srv3_install_diagnostic_observe( bmc: String, port: String, @@ -1063,15 +1101,72 @@ fn realize_os_install_actuator_toolchain_ensure( } } +data provision_build_cache_arch_derivation_note: String = "The provisioning script is a function of the TARGET HOST's architecture, not a constant: the cited release publishes one musl tarball plus one sha256 per arch, so emitting a script at all requires knowing which. Arch comes from the effect target's own ComputeHost (compute_host_primary_cpu -> CpuFacts.architecture) and the token/digest selectors in extdeps.cache.sccache are partial over the Architecture coproduct β€” a host whose CPU is unreadable, or whose arch the release does not publish, yields NO script and a typed NotConverged. There is no default arch: shipping an aarch64 binary to an unlisted host is precisely the fabricated-plausible-output Β§5 forbids." + +fn provision_build_cache_host_arch(effect_intent: HostEffectIntent) -> Architecture? { + match effect_intent.target { + HostOs { node: host } => + match compute_host_primary_cpu(host: host) { + Present { value: cpu } => Present { value: cpu.catalog.architecture } + Absent => none + } + BmcController { node: _ } => none + } +} + fn realize_provision_build_cache_body( transport: HostEffectTransport, effect_intent: HostEffectIntent, ) -> Reconciliation { - let observed = run_shell_transport( - script: retained_srvn(body: build_cache_provision_shell_script(), reason: "srvN build-cache provisioning (sccache daemon ensure)"), - transport: transport, - ) - srv3_toolchain_ensure_reconcile(observed: observed, intent: effect_intent) + match provision_build_cache_host_arch(effect_intent: effect_intent) { + Absent => + NotConverged { + reason: "host_effect_apply: ProvisionBuildCache cannot derive a target architecture from the effect target (no primary CPU on the ComputeHost, or the target is not HostOs); fail-closed, no default arch.", + applied: effect_intent, + } + Present { value: arch } => + match sccache_release_arch_token(arch: arch) { + Absent => + NotConverged { + reason: join( + [ + "host_effect_apply: ProvisionBuildCache refused β€” the cited sccache release ", + sccache_release_0_15_0.version as String, + " publishes no musl tarball for architecture ", + architecture_diagnostic_name(arch: arch) as String, + "; fail-closed, no default arch.", + ], + "", + ), + applied: effect_intent, + } + Present { value: token } => + match sccache_release_digest(rel: sccache_release_0_15_0, arch: arch) { + Absent => + NotConverged { + reason: join( + [ + "host_effect_apply: ProvisionBuildCache refused β€” no pinned sha256 in the cited release row for architecture ", + architecture_diagnostic_name(arch: arch) as String, + "; fail-closed, never install unverified.", + ], + "", + ), + applied: effect_intent, + } + Present { value: digest } => { + let observed = run_shell_transport( + script: retained_srvn( + body: build_cache_provision_shell_script(arch_token: token, digest: digest), + reason: "srvN build-cache provisioning (sccache daemon ensure)", + ), + transport: transport, + ) + provision_build_cache_reconcile(observed: observed, intent: effect_intent) + } + } + } + } } fn realize_provision_build_cache( @@ -1119,10 +1214,33 @@ fn provision_build_cache_witness_intent() -> HostEffectIntent { } } +data provision_build_cache_arch_unknown_fixture_note: String = "A host the fleet knows by identity but whose processor inventory is empty β€” the shape a freshly-racked srvN has before its BMC read lands (srv4 carried exactly this deferral for memory). Realization must REFUSE it, because 'which binary do I install' has no answer. The fixture deliberately does NOT fabricate a CPU catalog row for an arch the cited release omits: minting a machine that does not exist to test a refusal would be its own Β§3 violation, so the not-published arm is witnessed at the selector (sccache_release_arch_token over Riscv64/Wasm32) instead." + +fn provision_build_cache_arch_unknown_host_fixture() -> ComputeHost { + ComputeHost { + identity: srv1_host.identity, + baseboard: none, + processors: [], + memory: [], + storage: [], + network_interfaces: [], + } +} + +fn provision_build_cache_arch_unknown_intent_fixture() -> HostEffectIntent { + HostEffectIntent { + target: HostOs { node: provision_build_cache_arch_unknown_host_fixture() }, + effect: ProvisionBuildCache { catalog_id: sccache_local_id }, + evidence: host_effect_identity_evidence, + transport: LocalShell, + privilege_denial: none, + } +} + fn provision_build_cache_reconcile_shell_observed( observed: ShellExecObserved, ) -> Reconciliation { - srv3_toolchain_ensure_reconcile( + provision_build_cache_reconcile( observed: observed, intent: provision_build_cache_witness_intent(), ) diff --git a/dag/gunbc/host_identity_access.dag b/dag/gunbc/host_identity_access.dag index a9cb7d19f6e..5daa27542a7 100644 --- a/dag/gunbc/host_identity_access.dag +++ b/dag/gunbc/host_identity_access.dag @@ -28,6 +28,13 @@ data host_identity_srv4_access: DeployAccess = host_identity_ssh_access( ssh_host: operator_host_srv4 as NonEmptyStr, ) +data host_identity_srv3_access_note: String = "srv3 gains the same direct-SSH access shape as srv4 (operator, 2026-07-24: 'same access pattern as srv4'), now that its host OS is a modeled endpoint (gunbc.fleet_intent_network.srv3_host_lan_endpoint, 192.168.1.221) rather than BMC-only. This row is how you reach srv3 ITSELF, and it is NOT interchangeable with ci_deploy_srv1_operator_access: the latter reaches the host an OsInstallActuator run drives srv3's BMC FROM, which is a different machine. Consumed through gunbc.host_toolchain_ensure.host_toolchain_direct_access, which the reach pairing derives from the resolved TARGET host β€” so the kind-aware split (BuildCache targets srv3, OsInstallActuator targets the selected actuator host) falls out of target resolution instead of being a second parallel lookup that could disagree with it. NETWORK REACH is NOT direct despite the shape mirroring srv4: srv3 is a fabric-only target reached through srv2, modeled as gunbc.fleet_reach.srv3_reach (ProxyJump interim, dissolving to FabricTunnel when the fabric works). This transport's SshShell ssh_host realizes OVER that reach β€” the network path (how packets get to srv3) is deliberately INDEPENDENT of the shell/auth transport (how a command runs once reached), per the operator rule 2026-07-24; encoding the jump INTO the transport (so SshShell carries a Reach rather than a bare host alias) is the reach-independent-of-shell decomposition (step b, coordinated with the shellβ†’dag transport-wall lane). LIVENESS grounded 2026-07-25 (corrected from an earlier over-broad claim): srv3 IS reachable and a command DOES run today β€” session -> srv2 (briansrls) -> ubuntu@srv3 authenticated by srv2's local node-orch key (~/.node-orch/id_ed25519 = node-orch@srv2, which ubuntu@srv3's authorized_keys trusts); proven by execution (hostname=srv3, aarch64, 128 cores, Ubuntu 24.04.3). So both the network reach AND a working shell path exist via that bootstrap credential. The NARROWER real gap: the FLEET identity (fleet-automation-ssh-key) is not yet on srv3 β€” srv3 was autoinstalled Jul 13 with ssh.authorized-keys EMPTY and hand-keyed post-install with node-orch@srv2 / briansrls@srv1 / macbook only, so the modeled DeployAccess principal (FleetAccountOperator) does not yet have a key srv3 trusts. That is a one-time host_authorized_keys_reconcile upsert over the working node-orch hop (fleet_subsumption_manual_gaps A1/B2), NOT an unreachable host. Reach realizable; a bootstrap shell path works; the fleet-identity shell path is pending key distribution β€” three facts held separate." + +data host_identity_srv3_access: DeployAccess = host_identity_ssh_access( + host: srv3_host, + ssh_host: operator_host_srv3 as NonEmptyStr, +) + fn host_identity_operator_principal_name() -> NonEmptyStr { grounded_posix_principal_name( p: fleet_posix_principal(key: FleetAccountOperator) diff --git a/dag/gunbc/host_runner_memory_provision.dag b/dag/gunbc/host_runner_memory_provision.dag index 046f217e725..26115c5fc7f 100644 --- a/dag/gunbc/host_runner_memory_provision.dag +++ b/dag/gunbc/host_runner_memory_provision.dag @@ -14,7 +14,7 @@ import gunbc.host_converge { NoMembershipProbe, } import gunbc.host_converge_slice1 { host_converge_from_policy } -import gunbc.host_toolchain_ensure { host_toolchain_ensure_access } +import gunbc.host_toolchain_ensure { host_toolchain_direct_access } import gunbc.fleet_converge_apply { fleet_compute_host_for_identity } import gunbc.host_effect { HostEffect, @@ -126,7 +126,7 @@ fn runner_memory_converge_effect(host: HostIdentity) -> HostEffect? { func provision_runner_memory_caps(host: HostIdentity) -> ProcessExit uses net: Network { - match host_toolchain_ensure_access(host: host) { + match host_toolchain_direct_access(host: host) { Present { value: access } => match fleet_compute_host_for_identity(identity: host) { Present { value: compute_host } => diff --git a/dag/gunbc/host_toolchain_ensure.dag b/dag/gunbc/host_toolchain_ensure.dag index e315af0191f..84b187418bb 100644 --- a/dag/gunbc/host_toolchain_ensure.dag +++ b/dag/gunbc/host_toolchain_ensure.dag @@ -7,7 +7,12 @@ import std.process { ProcessExit, ExitSuccess, exit_failure } import std.resources { Network } import product.placement_supply { HostIdentity } import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv2, operator_host_srv3, operator_host_srv4 } -import gunbc.host_identity_access { host_identity_srv1_access, host_identity_srv2_access, host_identity_srv4_access } +import gunbc.host_identity_access { + host_identity_srv1_access, + host_identity_srv2_access, + host_identity_srv3_access, + host_identity_srv4_access, +} import gunbc.ci_deploy_access { DeployAccess, ci_deploy_srv1_operator_access } import gunbc.fleet_intent { ComputeHost } import gunbc.host_effect { @@ -38,18 +43,45 @@ data host_toolchain_ensure_apply_dispatch_scaffold: Disposition = Scaffold { } } -fn host_toolchain_ensure_access(host: HostIdentity) -> DeployAccess? { +data host_toolchain_reach_pairing_note: String = "Access is DERIVED FROM THE TARGET HOST, never looked up independently from the requested host. Before 2026-07-24 these were two parallel decisions: host_toolchain_ensure_target_host was kind-aware (srv3 + OsInstallActuator resolves to the SELECTED actuator host) while the access lookup keyed on the requested host alone and pinned srv3 to ci_deploy_srv1_operator_access. Two defects followed, both silent. (1) A BuildCache request for srv3 targeted srv3 but authenticated to srv1, so the provisioning effect would have landed on the WRONG MACHINE and reported success β€” a Β§5 fail-open, and the exact kind this lane adds. (2) The srv1 pin is only correct in the actuator selector's UNSATISFIABLE FALLBACK arm; whenever ActuatorSelected names a different host the access still pointed at srv1. Pairing target and access in one return value makes the disagreement unwritable (Β§5 construction over validation) rather than a check that could flag it afterwards. Consequence: this module no longer consumes ci_deploy_srv1_operator_access, which is construction-identical to host_identity_srv1_access (same principal, host, transport, privileged commands β€” witnessed by host_toolchain_srv1_access_rows_are_one_concept); that Β§3 nickname still has consumers elsewhere and its corpus-wide dissolution is a separate lane, not smuggled in here." + +type HostToolchainReach = HostToolchainReach { + target: ComputeHost, + access: DeployAccess, +} + +fn host_toolchain_direct_access(host: HostIdentity) -> DeployAccess? { if host == operator_host_srv1 { Present { value: host_identity_srv1_access } } else { if host == operator_host_srv2 { Present { value: host_identity_srv2_access } } else { if host == operator_host_srv3 { - Present { value: ci_deploy_srv1_operator_access } + Present { value: host_identity_srv3_access } } else { if host == operator_host_srv4 { Present { value: host_identity_srv4_access } } else { none } } } } } +type HostToolchainReachOutcome + = ReachResolved { reach: HostToolchainReach } + | ReachTargetAbsent + | ReachAccessAbsent { target_identity: HostIdentity } + +fn host_toolchain_ensure_reach( + kind: HostToolchainKind, + host: HostIdentity, +) -> HostToolchainReachOutcome { + match host_toolchain_ensure_target_host(kind: kind, host: host) { + Present { value: target } => + match host_toolchain_direct_access(host: target.identity) { + Present { value: access } => + ReachResolved { reach: HostToolchainReach { target: target, access: access } } + Absent => ReachAccessAbsent { target_identity: target.identity } + } + Absent => ReachTargetAbsent {} + } +} + fn host_toolchain_ensure_effect(kind: HostToolchainKind) -> HostEffect { match kind { BuildCache => ProvisionBuildCache { catalog_id: sccache_local_id } @@ -72,29 +104,29 @@ fn host_toolchain_ensure_target_host(kind: HostToolchainKind, host: HostIdentity func host_toolchain_ensure(host: HostIdentity, kind: HostToolchainKind) -> ProcessExit uses net: Network { - match host_toolchain_ensure_access(host: host) { - Present { value: access } => - match host_toolchain_ensure_target_host(kind: kind, host: host) { - Present { value: compute_host } => - match host_effect_apply_gated( - access: access, - target: HostOs { node: compute_host }, - effect: host_toolchain_ensure_effect(kind: kind), - evidence: host_effect_identity_evidence, - transport: access.transport, - fixture_actor: none, - ) { - Converged { evidence: _, applied: _ } => ExitSuccess - NotConverged { reason: why, applied: _ } => exit_failure(reason: why) - } - Absent => - exit_failure( - reason: concat("host_toolchain_ensure: host absent from compute inventory ", host as String) - ) + match host_toolchain_ensure_reach(kind: kind, host: host) { + ReachResolved { reach: reach } => + match host_effect_apply_gated( + access: reach.access, + target: HostOs { node: reach.target }, + effect: host_toolchain_ensure_effect(kind: kind), + evidence: host_effect_identity_evidence, + transport: reach.access.transport, + fixture_actor: none, + ) { + Converged { evidence: _, applied: _ } => ExitSuccess + NotConverged { reason: why, applied: _ } => exit_failure(reason: why) } - Absent => + ReachTargetAbsent => + exit_failure( + reason: concat("host_toolchain_ensure: host absent from compute inventory ", host as String) + ) + ReachAccessAbsent { target_identity: target_identity } => exit_failure( - reason: concat("host_toolchain_ensure: no deploy access for host ", host as String) + reason: concat( + concat("host_toolchain_ensure: no deploy access for target host ", target_identity as String), + concat(" (requested host ", concat(host as String, ")")) + ) ) } } diff --git a/dag/gunbc/network_identity_subsumption.dag b/dag/gunbc/network_identity_subsumption.dag index 99b88e1743c..57f7897bfa6 100644 --- a/dag/gunbc/network_identity_subsumption.dag +++ b/dag/gunbc/network_identity_subsumption.dag @@ -12,9 +12,9 @@ import extdeps.dhcp.v4 { Inactive, Expired, MacAddress, - Ipv4Address, dhcp_lease_remaining_from_cited_minutes, } +import extdeps.network.ipv4 { Ipv4Address, ipv4_address } import extdeps.dns.domain_name { HostName, DomainName, @@ -86,7 +86,7 @@ fn lease_table_has_os_up_subsumption( data srv3_bmc_static_lease_row: Cr1000aDhcpLeaseRow = Cr1000aDhcpLeaseRow { mac_address: "48:21:0B:81:C5:14" as MacAddress, - ipv4_address: "192.168.1.192" as Ipv4Address, + ipv4_address: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 192), lease: StaticDhcpReservation { reservation_label: "bmc-altrad8ud-1l2t-3" as NonEmptyStr, status: Active, @@ -95,7 +95,7 @@ data srv3_bmc_static_lease_row: Cr1000aDhcpLeaseRow = Cr1000aDhcpLeaseRow { data srv3_os_up_dynamic_lease_row: Cr1000aDhcpLeaseRow = Cr1000aDhcpLeaseRow { mac_address: "00:00:00:00:00:00" as MacAddress, - ipv4_address: "192.168.1.193" as Ipv4Address, + ipv4_address: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 193), lease: DynamicDhcpLease { client_hostname: Present { value: srv3_fleet_slot_host_name }, lease_time_remaining: dhcp_lease_remaining_from_cited_minutes(minutes: 120), diff --git a/dag/test/claim/cr1000a_dhcp_lease_naming_witness_test.dag b/dag/test/claim/cr1000a_dhcp_lease_naming_witness_test.dag index 94668a26b2c..840ec04a9a7 100644 --- a/dag/test/claim/cr1000a_dhcp_lease_naming_witness_test.dag +++ b/dag/test/claim/cr1000a_dhcp_lease_naming_witness_test.dag @@ -10,7 +10,7 @@ data srv1_option12_host_name: HostName = HostName { data sample_dynamic_srv1_lease: Cr1000aDhcpLeaseRow = Cr1000aDhcpLeaseRow { mac_address: "48:21:0B:81:C6:EA" as MacAddress, - ipv4_address: "192.168.1.185" as Ipv4Address, + ipv4_address: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 185), lease: DynamicDhcpLease { client_hostname: Present { value: srv1_option12_host_name }, lease_time_remaining: dhcp_lease_remaining_from_cited_minutes(minutes: 120), @@ -20,7 +20,7 @@ data sample_dynamic_srv1_lease: Cr1000aDhcpLeaseRow = Cr1000aDhcpLeaseRow { data sample_static_srv3_reservation: Cr1000aDhcpLeaseRow = Cr1000aDhcpLeaseRow { mac_address: "48:21:0B:81:C5:14" as MacAddress, - ipv4_address: "192.168.1.192" as Ipv4Address, + ipv4_address: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 192), lease: StaticDhcpReservation { reservation_label: "bmc-altrad8ud-1l2t-3" as NonEmptyStr, status: extdeps.dhcp.v4.Active, diff --git a/dag/test/claim/fleet_intent_network_witness_test.dag b/dag/test/claim/fleet_intent_network_witness_test.dag index 6d296f7f7cf..ee4b3ac4a17 100644 --- a/dag/test/claim/fleet_intent_network_witness_test.dag +++ b/dag/test/claim/fleet_intent_network_witness_test.dag @@ -12,10 +12,19 @@ test fn fleet_intent_network_container_to_host_lan_denied() -> Bool { } test fn fleet_intent_network_topology_endpoint_count_holds() -> Bool { - list_length(items: fleet_intent_network.endpoints) == 10 + list_length(items: fleet_intent_network.endpoints) == 11 } test fn fleet_intent_network_srv1_addresses_holds() -> Bool { srv1_host_lan_endpoint.address == "192.168.1.185" && srv1_bmc_endpoint.address == "192.168.1.183" } + +data fleet_intent_network_srv3_host_witness_note: String = "The count row above is a tripwire, not a fact about srv3 β€” it reds on ANY topology edit and says nothing about WHICH endpoint appeared. This row is the discriminating half for the 2026-07-24 srv3 host addition, mirroring fleet_intent_network_srv1_addresses_holds: srv3 must be modeled with BOTH of its interfaces distinguished by role (its BMC at .192 was modeled since the srv3 onboarding lane; its host OS at .221 was not, so a model that named srv3 could still not name the machine). Asserting both addresses AND the role split is what makes a regression that collapses host onto BMC β€” the exact confusion this row was added to end β€” go red rather than merely shifting a count." + +test fn fleet_intent_network_srv3_addresses_holds() -> Bool { + srv3_host_lan_endpoint.address == "192.168.1.221" + && srv3_host_lan_endpoint.role == HostOperatingSystem + && srv3_bmc_endpoint.address == "192.168.1.192" + && srv3_bmc_endpoint.role == BmcOutOfBand +} diff --git a/dag/test/claim/host_build_cache_provision_design_witness_test.dag b/dag/test/claim/host_build_cache_provision_design_witness_test.dag index 11cdc05c1c5..609663314d8 100644 --- a/dag/test/claim/host_build_cache_provision_design_witness_test.dag +++ b/dag/test/claim/host_build_cache_provision_design_witness_test.dag @@ -103,8 +103,151 @@ fn witness_red_control_widen_on_absent_rejected_by_gate() -> Bool { && design_witness_authority_gate_accepts_absent_refusal() } +fn path_shadow_observation_fixture() -> BuildCacheDaemonObservation { + DaemonPathShadowed { resolved: "/usr/bin/sccache", expected: "/usr/local/bin/sccache" } +} + +fn design_witness_path_shadow_refuses_fail_closed() -> Bool { + match provision_build_cache_verdict( + catalog_id: sccache_local_id, + observed: path_shadow_observation_fixture(), + ) { + ProvisionRefused { cause: RefusalPathShadowed, reason: reason } => + string_contains(s: reason as String, pattern: "/usr/bin/sccache") + && string_contains(s: reason as String, pattern: "/usr/local/bin/sccache") + && string_contains(s: reason as String, pattern: "Fail-closed") + ProvisionRefused { cause: _, reason: _ } => false + ProvisionConverged { catalog_id: _, stats_line: _ } => false + } +} + +fn design_witness_red_control_widen_on_path_shadow_rejected_by_gate() -> Bool { + match provision_build_cache_absorbing_fallback_widen_sketch( + catalog_id: sccache_local_id, + observed: path_shadow_observation_fixture(), + ) { + ProvisionConverged { catalog_id: _, stats_line: _ } => true + ProvisionRefused { cause: _, reason: _ } => false + } && !build_cache_provision_gate_accepts( + verdict: provision_build_cache_absorbing_fallback_widen_sketch( + catalog_id: sccache_local_id, + observed: path_shadow_observation_fixture(), + ), + observed: path_shadow_observation_fixture(), + ) + && build_cache_provision_gate_accepts( + verdict: provision_build_cache_verdict( + catalog_id: sccache_local_id, + observed: path_shadow_observation_fixture(), + ), + observed: path_shadow_observation_fixture(), + ) +} + +fn design_witness_path_authority_observation_not_emitted_as_shell() -> Bool { + !string_contains( + s: build_cache_observe_stats_body(), + pattern: "path_authority=SHADOWED", + ) && !string_contains( + s: build_cache_read_back_body(binary: sccache_installed_binary_path), + pattern: "path_authority=SHADOWED", + ) && !string_contains( + s: build_cache_provision_script_body( + arch_token: "aarch64" as NonEmptyStr, + digest: sccache_release_0_15_0.digest_aarch64, + ), + pattern: "command -v sccache", + ) +} + +fn design_witness_install_is_cited_not_package_manager() -> Bool { + build_cache_install_is_cited_not_package_manager() +} + +fn design_witness_unit_execstart_matches_install_path() -> Bool { + build_cache_unit_execstart_matches_install_path() +} + +fn design_witness_classifier_covers_every_cited_fragment() -> Bool { + build_cache_classifier_covers_every_cited_fragment() +} + +fn design_witness_classifier_is_a_fold_not_an_unrolled_chain() -> Bool { + !string_contains(s: build_cache_classify_failure_body(), pattern: "elif") + && string_contains(s: build_cache_classify_failure_body(), pattern: "for frag in ") +} + +fn design_witness_fragment_words_are_shell_safe() -> Bool { + build_cache_fragment_words_are_shell_safe() +} + +fn design_witness_release_arch_token_is_fail_closed() -> Bool { + match sccache_release_arch_token(arch: Aarch64) { + Present { value: token } => token as String == "aarch64" + Absent => false + } && match sccache_release_arch_token(arch: X86_64) { + Present { value: token } => token as String == "x86_64" + Absent => false + } && match sccache_release_arch_token(arch: Riscv64) { + Absent => true + Present { value: _ } => false + } && match sccache_release_arch_token(arch: Wasm32) { + Absent => true + Present { value: _ } => false + } +} + +fn design_witness_release_digest_is_fail_closed() -> Bool { + match sccache_release_digest(rel: sccache_release_0_15_0, arch: Aarch64) { + Present { value: d } => d == sccache_release_0_15_0.digest_aarch64 + Absent => false + } && match sccache_release_digest(rel: sccache_release_0_15_0, arch: X86_64) { + Present { value: d } => d == sccache_release_0_15_0.digest_x86_64 + Absent => false + } && match sccache_release_digest(rel: sccache_release_0_15_0, arch: Riscv64) { + Absent => true + Present { value: _ } => false + } +} + +fn design_witness_arch_unknown_host_refuses_realization() -> Bool { + match realize_provision_build_cache( + effect_intent: provision_build_cache_arch_unknown_intent_fixture(), + ) { + NotConverged { reason: why, applied: _ } => + string_contains(s: why, pattern: "cannot derive a target architecture") + && string_contains(s: why, pattern: "no default arch") + Converged { evidence: _, applied: _ } => false + } +} + +fn design_witness_known_arch_host_does_not_refuse_for_arch() -> Bool { + match provision_build_cache_host_arch( + effect_intent: provision_build_cache_witness_intent(), + ) { + Present { value: arch } => + match sccache_release_arch_token(arch: arch) { + Present { value: token } => token as String == "aarch64" + Absent => false + } + Absent => false + } +} + test fn host_build_cache_provision_design_witnesses() -> Bool { design_witness_read_back_fails_closed_in_shell() + && design_witness_path_shadow_refuses_fail_closed() + && design_witness_red_control_widen_on_path_shadow_rejected_by_gate() + && design_witness_path_authority_observation_not_emitted_as_shell() + && design_witness_install_is_cited_not_package_manager() + && design_witness_unit_execstart_matches_install_path() + && design_witness_classifier_covers_every_cited_fragment() + && design_witness_classifier_is_a_fold_not_an_unrolled_chain() + && design_witness_fragment_words_are_shell_safe() + && design_witness_release_arch_token_is_fail_closed() + && design_witness_release_digest_is_fail_closed() + && design_witness_arch_unknown_host_refuses_realization() + && design_witness_known_arch_host_does_not_refuse_for_arch() && design_witness_unknown_catalog_refuses_at_gate() && design_witness_known_non_sccache_catalog_refuses_at_gate() && design_witness_known_non_sccache_catalog_refuses_at_verdict() diff --git a/dag/test/claim/host_build_cache_provision_real_execution_witness_test.dag b/dag/test/claim/host_build_cache_provision_real_execution_witness_test.dag index 4ba98821b4e..2d7603a2ed0 100644 --- a/dag/test/claim/host_build_cache_provision_real_execution_witness_test.dag +++ b/dag/test/claim/host_build_cache_provision_real_execution_witness_test.dag @@ -5,7 +5,9 @@ import extdeps.shell import gunbc.retained_shell_script { retained_runtime } import extdeps.filesystem.filesystem_io import gunbc.shell_bash_runner { shell_exec_via_bash } -import gunbc.host_build_cache_provision_script { build_cache_read_back_body } +import gunbc.host_build_cache_provision_script { + build_cache_read_back_body, +} import gunbc.host_effect_realize { provision_build_cache_reconcile_shell_observed, ShellExecObserved, @@ -15,38 +17,60 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -data real_execution_home_doc: String = "Wet execution witness for ProvisionBuildCache read-back fail-closed: runs build_cache_read_back_body under set -euo pipefail with a PATH-prepended fake sccache that always exits 1, then asserts provision_build_cache_reconcile_shell_observed returns NotConverged (not Converged/ExitSuccess). Excluded from hermetic discovery and enrolled in bin_witness_wet_entries β€” shell.Mktemp.Dir / Filesystem.Write / shell.Exec.Run have no mock_response. RED control: a regressing script that implicit-exit-0 on failed read-back would reconcile Converged and fail this witness." +data real_execution_home_doc: String = "Wet execution witness for ProvisionBuildCache fail-closed behaviour: it runs a real bash body against a real fake-sccache on disk. read-back β€” the modeled binary answers non-zero, so the reconcile must be NotConverged, never Converged/ExitSuccess; the fake lives at an explicit OFF-PATH path passed as the read-back body's `binary` argument, so this witness exercises the read-back arm on the binary this lane provisioned. The earlier PATH-shadow shell witnesses were withdrawn 2026-07-24 (review 42343): the PATH-shadow judgement is proven at the MODEL grain (host_build_cache_provision_design_witness_test.design_witness_path_shadow_refuses_fail_closed) and its live observation is staged on the typed-argv dissolve-on (#5828), not emitted as hand-shell. Excluded from hermetic discovery and enrolled in bin_witness_wet_entries β€” shell.Mktemp.Dir / Filesystem.Write / shell.Exec.Run have no mock_response. Transport scripts mint through the counted retained_runtime bridge (shell-to-dag section 5.E construction wall, #7184), never the deleted free-minter." -test fn provision_read_back_failure_not_converged_by_real_execution() -> Bool { - let dir = shell.Mktemp.Dir() - let fake_sccache_path = concat(dir.path as String, "/sccache") - let wrote = Filesystem.Write(path: fake_sccache_path, content: "#!/bin/sh\nexit 1\n") - let chmod = shell.Exec.Run(script: retained_runtime(body: concat("chmod +x ", fake_sccache_path), reason: "build-cache provision witness chmod +x fake sccache stub")) - let body = concat( - "set -euo pipefail\n", - concat( - concat("export PATH=\"", dir.path as String), - concat(":$PATH\"\n", build_cache_read_back_body()), +fn write_fake_sccache(dir_path: String, exit_code: String) -> Bool { + let path = concat(dir_path, "/sccache") + let wrote = Filesystem.Write( + path: path, + content: concat("#!/bin/sh\nexit ", concat(exit_code, "\n")), + ) + let chmod = shell.Exec.Run( + script: retained_runtime( + body: concat("chmod +x ", path), + reason: "build-cache provision witness chmod +x fake sccache stub" as NonEmptyStr, + ), + ) + wrote.success && chmod.success +} + +fn run_body(prelude: String, body: String) -> ShellExecObserved { + let full = concat("set -euo pipefail\n", concat(prelude, body)) + let result = shell.Exec.Run( + script: retained_runtime( + body: shell_exec_via_bash(body: full), + reason: "build-cache provision witness body under fake failing sccache" as NonEmptyStr, ), ) - let script = shell_exec_via_bash(body: body) - let result = shell.Exec.Run(script: retained_runtime(body: script, reason: "build-cache provision witness read-back body under fake failing sccache")) - let observed = ShellExecObserved { + ShellExecObserved { exit_code: result.exit_code, success: result.success, stdout: result.stdout, stderr: result.stderr, } +} + +test fn provision_read_back_failure_not_converged_by_real_execution() -> Bool { + let dir = shell.Mktemp.Dir() + let fake_sccache_path = concat(dir.path as String, "/sccache") + let seeded = write_fake_sccache(dir_path: dir.path as String, exit_code: "1") + let observed = run_body( + prelude: "", + body: build_cache_read_back_body(binary: fake_sccache_path), + ) let reconciled = provision_build_cache_reconcile_shell_observed(observed: observed) let cleaned = shell.Remove.RecursiveForce(path: dir.path) dir.success - && wrote.success - && chmod.success - && !result.success + && seeded + && !observed.success + && string_contains(s: observed.stdout, pattern: "read_back=FAILED") && cleaned.success && match reconciled { NotConverged { reason: why, applied: _ } => string_contains(s: why, pattern: "fail-closed") + && string_contains(s: why, pattern: "ProvisionBuildCache") Converged { evidence: _, applied: _ } => false } } + +data path_authority_observation_staged_note: String = "The two live PATH-shadow shell witnesses that lived here (refuses-healthy-shadowing / passes-when-no-sccache) were removed 2026-07-24 (review 42343): the shell observation they exercised grew the A5 census scaffold's emitted surface, so it was withdrawn and the PATH-shadow judgement is now proven at the MODEL grain only (host_build_cache_provision_design_witness_test.design_witness_path_shadow_refuses_fail_closed, a synthetic DaemonPathShadowed -> RefusalPathShadowed fold). The live observation is staged on the typed-argv dissolve-on (#5828); its real-execution witness returns when the observation is a typed op (shell.Which.Check), not hand-shell." diff --git a/dag/test/claim/network_grounding_witness_test.dag b/dag/test/claim/network_grounding_witness_test.dag new file mode 100644 index 00000000000..092b52667c4 --- /dev/null +++ b/dag/test/claim/network_grounding_witness_test.dag @@ -0,0 +1,175 @@ +module test.claim.network_grounding + + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data network_grounding_witness_home_note: String = "Consolidated green-by-execution proofs for the extdeps.network grounding leaves β€” the structured IPv4 address, the IpAddress/NetworkHost/SocketAddress surfaces, and the reach model. These were three witness files (ipv4_address / network_address_host / network_reach) until 2026-07-25; each was its own floor entry resolve, so consolidating them into one entry is a Β§6 cost-shape fix (fewer whole-tree closure resolves, zero coverage lost) β€” all three prove the same extdeps.network module family. The three original witness notes are preserved verbatim below." + +data ipv4_address_witness_note: String = "Green-by-execution proof for the structured IPv4 leaf (extdeps.network.ipv4), the witness the dissolution trigger dissolve_on_ipv4_address_anemic_brand requires. Proves parse recovers the four octets from wire text, render is its inverse (round-trip both ways), and β€” the fail-closed half β€” malformed input REFUSES with a typed, located Ipv4ParseError (wrong octet count, out-of-range, non-numeric), never a fabricated address. The discriminating controls are the three distinct refusal shapes: a parser that fabricated on bad input would return Ipv4Parsed and red these." + +fn ipv4_or_none(text: String) -> Ipv4Address? { + match parse_ipv4_address(text: text) { + Ipv4Parsed { address: a } => Present { value: a } + Ipv4ParseFailed { error: _ } => none + } +} + +test fn ipv4_parse_recovers_octets() -> Bool { + match parse_ipv4_address(text: "192.168.1.221") { + Ipv4Parsed { address: a } => + a.octet1 == 192 && a.octet2 == 168 && a.octet3 == 1 && a.octet4 == 221 + Ipv4ParseFailed { error: _ } => false + } +} + +test fn ipv4_render_is_parse_inverse() -> Bool { + match parse_ipv4_address(text: "10.0.42.7") { + Ipv4Parsed { address: a } => render_ipv4_address(addr: a) as String == "10.0.42.7" + Ipv4ParseFailed { error: _ } => false + } +} + +test fn ipv4_constructor_renders_dotted_decimal() -> Bool { + let rendered = render_ipv4_address(addr: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 192)) + rendered as String == "192.168.1.192" +} + +test fn ipv4_wrong_octet_count_refuses() -> Bool { + match parse_ipv4_address(text: "192.168.1") { + Ipv4Parsed { address: _ } => false + Ipv4ParseFailed { error: Ipv4WrongOctetCount { observed_count: c } } => c == 3 + Ipv4ParseFailed { error: _ } => false + } +} + +test fn ipv4_out_of_range_refuses_located() -> Bool { + match parse_ipv4_address(text: "192.168.1.999") { + Ipv4Parsed { address: _ } => false + Ipv4ParseFailed { error: Ipv4OctetOutOfRange { position: p, value: v } } => p == 3 && v == 999 + Ipv4ParseFailed { error: _ } => false + } +} + +test fn ipv4_non_numeric_refuses_located() -> Bool { + match parse_ipv4_address(text: "192.168.one.4") { + Ipv4Parsed { address: _ } => false + Ipv4ParseFailed { error: Ipv4OctetNotNumeric { position: p, raw: r } } => p == 2 && r == "one" + Ipv4ParseFailed { error: _ } => false + } +} + +test fn ipv4_valid_and_invalid_discriminate() -> Bool { + match ipv4_or_none(text: "192.168.1.221") { + Present { value: _ } => + match ipv4_or_none(text: "999.999.999.999") { + Present { value: _ } => false + Absent => true + } + Absent => false + } +} + +data network_address_host_witness_note: String = "Green-by-execution proof for the address+host leaves of extdeps/network: the IpAddress = V4 | V6 coproduct, NetworkHost = ByName | ByAddress (reusing the grounded HostName + IpAddress), and SocketAddress (reusing std.types.Port). The load-bearing control is ip_v6_render_refuses_not_fabricates: the v6 string codec is staged, so render_ip_address on a v6 value must return Absent β€” a parser/renderer that fabricated a v6 string would red this. Loopback is checked on both arms (127.0.0.1 and ::1) so the coproduct's two arms are both exercised." + +fn srv2_hostname() -> HostName { + HostName { + name: DomainName { labels: ["srv2" as DnsLabel] }, + qualification: PartiallyQualified, + } +} + +test fn ipv4_ipaddress_renders_dotted_decimal() -> Bool { + let a = ip_v4(addr: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 221)) + match render_ip_address(addr: a) { + Present { value: s } => s as String == "192.168.1.221" + Absent => false + } +} + +test fn ip_v6_render_refuses_not_fabricates() -> Bool { + let a = ip_v6(addr: ipv6_address( + group1: 65152, group2: 0, group3: 0, group4: 0, + group5: 0, group6: 0, group7: 0, group8: 1, + )) + match render_ip_address(addr: a) { + Present { value: _ } => false + Absent => true + } +} + +test fn ipv4_loopback_is_the_whole_slash8() -> Bool { + ip_address_is_loopback(addr: ip_v4(addr: ipv4_address(octet1: 127, octet2: 0, octet3: 0, octet4: 1))) + && ip_address_is_loopback(addr: ip_v4(addr: ipv4_address(octet1: 127, octet2: 5, octet3: 9, octet4: 2))) + && ip_address_is_loopback(addr: ip_v4(addr: ipv4_address(octet1: 126, octet2: 0, octet3: 0, octet4: 1))) == false + && ip_address_is_loopback(addr: ip_v4(addr: ipv4_address(octet1: 128, octet2: 0, octet3: 0, octet4: 1))) == false +} + +test fn ipv6_loopback_detected() -> Bool { + let lo = ip_v6(addr: ipv6_address(group1: 0, group2: 0, group3: 0, group4: 0, group5: 0, group6: 0, group7: 0, group8: 1)) + let not_lo = ip_v6(addr: ipv6_address(group1: 65152, group2: 0, group3: 0, group4: 0, group5: 0, group6: 0, group7: 0, group8: 1)) + ip_address_is_loopback(addr: lo) && ip_address_is_loopback(addr: not_lo) == false +} + +test fn network_host_by_address_renders() -> Bool { + let h = host_by_ipv4(addr: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 188)) + match render_network_host(host: h) { + Present { value: s } => s as String == "192.168.1.188" + Absent => false + } +} + +test fn network_host_by_name_renders_wire() -> Bool { + match render_network_host(host: host_by_name(name: srv2_hostname())) { + Present { value: s } => s as String == "srv2" + Absent => false + } +} + +test fn socket_address_pairs_host_and_port() -> Bool { + let sa = socket_address(host: host_by_ipv4(addr: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 188)), port: 22) + sa.port == 22 && ip_address_is_v4(addr: match sa.host { HostByAddress { address: a } => a HostByName { name: _ } => ip_v4(addr: ipv4_address(octet1: 0, octet2: 0, octet3: 0, octet4: 0)) }) +} + +data network_reach_witness_note: String = "Green-by-execution proof for extdeps.network.reach β€” the network-reach model independent of shell transport. The load-bearing Β§5 control is fabric_tunnel_refuses_realization: FabricTunnel is the intended long-term reach that does NOT work yet, so its realizability MUST be ReachRefused{FabricTunnelNotOperational}; a model that let it fall through as realizable would red this. DirectLan and a non-empty ProxyJump are realizable; an empty-chain ProxyJump refuses by construction (a jump with no hops is a modeling error, not a direct reach). reach_target extracts the ultimate target across all three arms. Together these prove the interim srv3-via-srv2 ProxyJump is a realizable, cited config while the fabric it stands in for stays honestly refused." + +fn reach_srv2() -> NetworkHost { + host_by_ipv4(addr: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 188)) +} + +fn reach_srv3() -> NetworkHost { + host_by_ipv4(addr: ipv4_address(octet1: 192, octet2: 168, octet3: 1, octet4: 221)) +} + +test fn direct_lan_is_realizable() -> Bool { + reach_is_realizable(reach: direct_lan(host: reach_srv2())) +} + +test fn proxy_jump_via_srv2_to_srv3_is_realizable() -> Bool { + reach_is_realizable(reach: proxy_jump(jumps: [reach_srv2()], target: reach_srv3())) +} + +test fn fabric_tunnel_refuses_realization() -> Bool { + match reach_realizability(reach: fabric_tunnel(target: reach_srv3())) { + ReachRealizable => false + ReachRefused { cause: FabricTunnelNotOperational } => true + ReachRefused { cause: ProxyJumpChainEmpty } => false + } +} + +test fn empty_proxy_jump_chain_refuses_by_construction() -> Bool { + match reach_realizability(reach: proxy_jump(jumps: [], target: reach_srv3())) { + ReachRealizable => false + ReachRefused { cause: ProxyJumpChainEmpty } => true + ReachRefused { cause: FabricTunnelNotOperational } => false + } +} + +test fn reach_target_extracts_ultimate_target_across_arms() -> Bool { + let via = proxy_jump(jumps: [reach_srv2()], target: reach_srv3()) + let direct = direct_lan(host: reach_srv3()) + let fabric = fabric_tunnel(target: reach_srv3()) + let via_t = render_network_host(host: reach_target(reach: via)) + let direct_t = render_network_host(host: reach_target(reach: direct)) + let fabric_t = render_network_host(host: reach_target(reach: fabric)) + via_t == direct_t && fabric_t == direct_t +} diff --git a/dag/test/claim/srv3_subsumption_witness_test.dag b/dag/test/claim/srv3_subsumption_witness_test.dag new file mode 100644 index 00000000000..5a9fab335a7 --- /dev/null +++ b/dag/test/claim/srv3_subsumption_witness_test.dag @@ -0,0 +1,208 @@ +module test.claim.srv3_subsumption + + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data srv3_subsumption_witness_home_note: String = "Consolidated green-by-execution proofs for the gunbc-layer srv3 subsumption facts β€” the reach row, the authorized-keys reconcile, and the toolchain target/access pairing. These three were separate witness files (fleet_reach / host_authorized_keys_reconcile / host_toolchain_reach_pairing) until 2026-07-25; each paid a full whole-tree closure resolve in the floor as its own entry, and three gunbc-closure resolves pushed batch 3 over its wall budget. They share one closure, so they are one floor entry here β€” a Β§6 cost-shape fix (fewer entry resolves, zero coverage lost), not a merge of unrelated concerns: all three are the srv3 subsumption lane. The three original witness notes are preserved verbatim below." + +data fleet_reach_witness_note: String = "Green-by-execution proof for the CONCRETE gunbc srv3 reach row (gunbc.fleet_reach.srv3_reach), distinct from the extdeps model mechanics that test.claim.network_grounding already proves. These pin the FLEET fact: srv3_reach is the ProxyJump-through-srv2 interim (exactly one hop), its network reach is realizable (grounded live 2026-07-25 β€” a Permission-denied handshake from srv2 proves packets reach srv3), and its target renders to srv3's grounded address 192.168.1.221 (consuming extdeps.network.ipv4, one of the sites the fleet_intent_network bare-string residual dissolves onto). The load-bearing Β§5 control is srv3_fabric_intended_refuses: the dissolution TARGET (srv3_reach_fabric_intended, the FabricTunnel srv3_reach retires to when the fabric works) is a real value that HONESTLY refuses realization today, so the dissolution trigger is not just prose β€” a model that let the intended fabric reach fall through as realizable would red this." + +test fn srv3_reach_is_single_hop_proxy_jump() -> Bool { + match srv3_reach { + ProxyJump { jumps: js, target: _ } => list_length(items: js) == 1 + DirectLan { host: _ } => false + FabricTunnel { target: _ } => false + } +} + +test fn srv3_reach_network_is_realizable() -> Bool { + srv3_reach_is_realizable() +} + +test fn srv3_reach_target_is_srv3_address() -> Bool { + let got = render_network_host(host: srv3_reach_target()) + let want = render_network_host(host: srv3_lan_reach_host) + got == want +} + +test fn srv3_reach_jump_is_srv2() -> Bool { + match srv3_reach { + ProxyJump { jumps: js, target: _ } => + fold( + js, + init: true, + f: (acc, h) => + acc && (render_network_host(host: h) == render_network_host(host: srv2_lan_reach_host)), + ) + DirectLan { host: _ } => false + FabricTunnel { target: _ } => false + } +} + +test fn srv3_fabric_intended_refuses_realization() -> Bool { + match reach_realizability(reach: srv3_reach_fabric_intended) { + ReachRealizable => false + ReachRefused { cause: FabricTunnelNotOperational } => true + ReachRefused { cause: ProxyJumpChainEmpty } => false + } +} + +data host_authorized_keys_reconcile_witness_note: String = "Green-by-execution proof of the SSH-authorized-keys reconcile on REAL observed data (operator macbook reads of srv3/srv4, 2026-07-24). The load-bearing discriminations: srv3 (installed pre-#7027, missing the fleet key) yields exactly ONE upsert β€” the fleet-automation key, named specifically, not just a count β€” and TWO refusals, both the out-of-band keys the fleet does not own, REFUSED (not torn down). srv4 (installed with the fleet key in the seed) yields the empty converged plan β€” the negative control that proves the reconcile does not fabricate work. The R5-wall RED control (reconcile_would_teardown_only_if_ownership_claimed_it) reconstructs the wall's hinge: feed a ownership fn that lies 'Owned' about the foreign keys and the SAME spine WOULD emit teardowns β€” so the refusal is caused by ownership_of returning Absent, not by the spine being unable to teardown. That makes the wall discriminating rather than asserted." + +fn srv3_plan() -> MembershipPlan { + host_authorized_keys_reconcile(observed: srv3_observed_authorized_keys) +} + +fn srv4_plan() -> MembershipPlan { + host_authorized_keys_reconcile(observed: srv4_observed_authorized_keys) +} + +test fn srv3_reconcile_adds_exactly_the_missing_fleet_key() -> Bool { + let plan = srv3_plan() + let upsert_materials = flat_map(plan.actions, a => + match a { + MemberUpsert { member: m } => [m.material as String] + MemberTeardown { member: _ } => [] + MemberTeardownRefused { member: _, cause: _ } => [] + } + ) + count(upsert_materials) == 1 + && any(upsert_materials, m => m == fleet_automation_ssh_key.material as String) +} + +test fn srv3_reconcile_refuses_both_unowned_keys_never_teardown() -> Bool { + let plan = srv3_plan() + let tally = membership_tally(plan: plan) + let refused_materials = flat_map(plan.actions, a => + match a { + MemberTeardownRefused { member: m, cause: OwnershipUnknown } => [m.material as String] + MemberTeardownRefused { member: _, cause: MemberNotOwned } => [] + MemberUpsert { member: _ } => [] + MemberTeardown { member: _ } => [] + } + ) + tally.upserts == 1 + && tally.teardowns == 0 + && tally.refusals == 2 + && any(refused_materials, m => m == srv3_observed_node_orch_srv2_key.material as String) + && any(refused_materials, m => m == srv3_observed_briansrls_srv1_key.material as String) +} + +test fn srv4_reconcile_is_converged_empty_plan() -> Bool { + let tally = membership_tally(plan: srv4_plan()) + tally.upserts == 0 && tally.teardowns == 0 && tally.refusals == 0 +} + +test fn srv3_and_srv4_disagree_on_convergence() -> Bool { + let srv3 = membership_tally(plan: srv3_plan()) + let srv4 = membership_tally(plan: srv4_plan()) + (srv3.upserts + srv3.refusals) > 0 + && (srv4.upserts + srv4.teardowns + srv4.refusals) == 0 +} + +fn ownership_lies_owned(k: SshPublicKey) -> Ownership? { + authorized_key_ownership(k: operator_macbook_ssh_key) +} + +test fn reconcile_would_teardown_only_if_ownership_claimed_it() -> Bool { + let honest = membership_tally(plan: srv3_plan()) + let lying = membership_tally(plan: membership_reconcile( + desired: fleet_authorized_keys, + observed: srv3_observed_authorized_keys, + key_of: authorized_key_identity, + key_eq: authorized_key_identity_eq, + value_eq: authorized_key_value_eq, + ownership_of: ownership_lies_owned, + )) + honest.refusals == 2 + && honest.teardowns == 0 + && lying.refusals == 0 + && lying.teardowns == 2 +} + +test fn comment_only_drift_is_reupsert_not_remove_add() -> Bool { + let renamed_macbook = SshPublicKey { + algorithm: operator_macbook_ssh_key.algorithm, + material: operator_macbook_ssh_key.material, + comment: "macbook-m4-renamed", + } + let observed = [renamed_macbook, fleet_automation_ssh_key] + let tally = membership_tally(plan: host_authorized_keys_reconcile(observed: observed)) + tally.upserts == 1 && tally.teardowns == 0 && tally.refusals == 0 +} + +data host_toolchain_reach_pairing_witness_note: String = "Discriminating witnesses for the 2026-07-24 target/access pairing in gunbc.host_toolchain_ensure. The defect being walled: access used to be looked up from the REQUESTED host while the target was resolved kind-aware, so a BuildCache request for srv3 targeted srv3 and authenticated to srv1 β€” the effect lands on the wrong machine and reports success. A test that merely asserts the reach resolves would pass under the old code too, so the load-bearing row here is reach_access_host_is_the_target_host, which compares the two sides of the pair and is red exactly when they disagree. Its negative control is reach_wrong_machine_pairing_is_unwritable: the old behaviour is reconstructed by hand and shown to violate the same predicate, so the predicate is proven to discriminate rather than assumed to." + +fn reach_or_absent(kind: HostToolchainKind, host: HostIdentity) -> HostToolchainReach? { + match host_toolchain_ensure_reach(kind: kind, host: host) { + ReachResolved { reach: reach } => Present { value: reach } + ReachTargetAbsent => none + ReachAccessAbsent { target_identity: _ } => none + } +} + +fn reach_pair_agrees(kind: HostToolchainKind, host: HostIdentity) -> Bool { + match reach_or_absent(kind: kind, host: host) { + Present { value: reach } => reach.access.host.identity == reach.target.identity + Absent => false + } +} + +test fn reach_access_host_is_the_target_host() -> Bool { + reach_pair_agrees(kind: BuildCache, host: operator_host_srv1) + && reach_pair_agrees(kind: BuildCache, host: operator_host_srv2) + && reach_pair_agrees(kind: BuildCache, host: operator_host_srv3) + && reach_pair_agrees(kind: BuildCache, host: operator_host_srv4) + && reach_pair_agrees(kind: OsInstallActuator, host: operator_host_srv3) +} + +test fn reach_build_cache_on_srv3_targets_srv3_not_the_actuator() -> Bool { + match reach_or_absent(kind: BuildCache, host: operator_host_srv3) { + Present { value: reach } => + reach.target.identity == operator_host_srv3 + && reach.access.host.identity == operator_host_srv3 + Absent => false + } +} + +test fn reach_os_install_actuator_on_srv3_runs_from_the_actuator_host() -> Bool { + match reach_or_absent(kind: OsInstallActuator, host: operator_host_srv3) { + Present { value: reach } => + reach.target.identity == srv3_os_install_actuator_host.identity + && reach.access.host.identity == srv3_os_install_actuator_host.identity + Absent => false + } +} + +fn reach_pair_agrees_for(reach: HostToolchainReach) -> Bool { + reach.access.host.identity == reach.target.identity +} + +test fn reach_wrong_machine_pairing_is_unwritable() -> Bool { + let old_shape = HostToolchainReach { + target: srv3_host, + access: host_identity_srv1_access, + } + let old_disagrees = reach_pair_agrees_for(reach: old_shape) == false + let honest_agrees = match reach_or_absent(kind: BuildCache, host: operator_host_srv3) { + Present { value: reach } => reach_pair_agrees_for(reach: reach) + Absent => false + } + old_disagrees && honest_agrees +} + +test fn host_toolchain_srv1_access_rows_are_one_concept() -> Bool { + let a = host_identity_srv1_access + let b = ci_deploy_srv1_operator_access + a.host.identity == b.host.identity + && a.transport == b.transport + && a.principal == b.principal + && a.privileged_commands == b.privileged_commands +} + +test fn direct_access_covers_every_modeled_fleet_host() -> Bool { + match host_toolchain_direct_access(host: operator_host_srv3) { + Present { value: a } => a.host.identity == operator_host_srv3 + Absent => false + } +}