Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
37 commits
Select commit Hold shift + click to select a range
de8bcea
WIP: srvN subsumption
Jul 24, 2026
03899e2
WIP: srvN subsumption
Jul 24, 2026
e08f1d8
WIP: srvN subsumption
Jul 24, 2026
fe4bd8f
srvN build-cache: de-fork the sccache install authority on the P1b pr…
Jul 24, 2026
701ef2b
WIP: srvN subsumption
Jul 24, 2026
5630240
Relocate the PATH-shadow judgement into the model; shrink the script …
Jul 24, 2026
50492db
Merge remote-tracking branch 'origin/main' into session/vivid-wolf-453
Jul 24, 2026
13850c5
WIP: srvN subsumption
Jul 24, 2026
d433b43
WIP: srvN subsumption
Jul 24, 2026
c911f1b
WIP: srvN subsumption
Jul 24, 2026
9cf16df
WIP: srvN subsumption
Jul 24, 2026
4ea67ff
WIP: srvN subsumption
Jul 24, 2026
ab1ae8f
WIP: srvN subsumption
Jul 24, 2026
c288127
Merge remote-tracking branch 'origin/main' into session/vivid-wolf-453
Jul 24, 2026
9fd9daf
Fix compile-clean whole-tree failure: bare `Owned` variant is ambiguous
Jul 24, 2026
82833f9
WIP: srvN subsumption
Jul 24, 2026
0f3a878
WIP: srvN subsumption
Jul 24, 2026
d43d1b9
WIP: srvN subsumption
Jul 24, 2026
52b1e1a
Ground the IP address + network-host leaves (step a, reach lane)
Jul 24, 2026
6ae18c0
WIP: srvN subsumption
Jul 24, 2026
e6dc27c
WIP: srvN subsumption
Jul 24, 2026
2c24bd5
WIP: srvN subsumption
Jul 25, 2026
5f064a5
WIP: srvN subsumption
Jul 25, 2026
c24e096
WIP: srvN subsumption
Jul 25, 2026
fb590ab
Merge remote-tracking branch 'origin/main' into session/vivid-wolf-453
Jul 25, 2026
dca226c
WIP: srvN subsumption
Jul 25, 2026
6e44056
WIP: srvN subsumption
Jul 25, 2026
027121d
WIP: srvN subsumption
Jul 25, 2026
1241f9b
WIP: srvN subsumption
Jul 25, 2026
0438bb9
WIP: srvN subsumption
Jul 25, 2026
c2b9599
WIP: srvN subsumption
Jul 25, 2026
c44ea4e
srv3 network reach: model the srv2 ProxyJump interim, grounded live; …
Jul 25, 2026
b78f0dc
WIP: srvN subsumption
Jul 25, 2026
bcc9a76
Merge remote-tracking branch 'origin/main' into session/vivid-wolf-453
Jul 25, 2026
d1b7fab
WIP: srvN subsumption
Jul 25, 2026
a581f06
WIP: srvN subsumption
Jul 25, 2026
5d91083
Consolidate 6 new witness files → 2 to fix floor batch-3 over-budget
Jul 25, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions .github/workflows/falsifier.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
68 changes: 65 additions & 3 deletions dag/extdeps/cache/sccache.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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"], "")
Expand All @@ -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<String> = [
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"
Expand Down
6 changes: 1 addition & 5 deletions dag/extdeps/dhcp/v4.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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<String> = [
"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<String> = [
"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

Expand Down
49 changes: 49 additions & 0 deletions dag/extdeps/network/address.dag
Original file line number Diff line number Diff line change
@@ -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)
}
}
47 changes: 47 additions & 0 deletions dag/extdeps/network/endpoint.dag
Original file line number Diff line number Diff line change
@@ -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 }
}
100 changes: 100 additions & 0 deletions dag/extdeps/network/ipv4.dag
Original file line number Diff line number Diff line change
@@ -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<String>, 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 }
}
}
}
}
}
}
}
53 changes: 53 additions & 0 deletions dag/extdeps/network/ipv6.dag
Original file line number Diff line number Diff line change
@@ -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<String> = [
"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
}
Loading
Loading