From 4bcc2e40ffa270920eee859772c61e849dfe5840 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 18:31:15 +0000 Subject: [PATCH 1/7] Install-server provisioning slice 1: .dag-driven host prep + discovered-ISO fetch (dogfooded over gunbc run) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First slice of standing up the srv3 PXE/UEFI-HTTP install server on the LAN host (srv2-lan / an aarch64 Altra), driven entirely through the substrate: every step is a shell.Exec.Run effect dispatched by `gunbc run` (sh -c 'ssh ') — the .dag model is the authority for what runs, gunbc is the executor. No hand-typed provisioning. This slice = host prep (apt dnsmasq + grub-efi-arm64-signed + rsync, webroot) + Ubuntu 24.04 arm64 live-server ISO fetch. The ISO URL is NOT a pinned literal (a pinned point-release silently 404s on the next release — observed). It is decomposed into the durable modeled facts (mirror, series, channel, flavor, arch) and the volatile point-release is DISCOVERED at fetch time: list the release directory, regex the matching ubuntu-.--.iso entries, sort -V, pick the newest; FAIL-CLOSED (NO_MATCHING_ISO_FAIL_CLOSED + nonzero exit) if none match — never a silent 404 into a 0-byte file. Fetch is idempotent (skips re-download when the ISO is present) and detaches the download as a systemd unit so it survives the SSH session. Proven by execution against the live host: gunbc run -> resolves ubuntu-24.04.4-live-server-arm64.iso from the upstream, ISO_PRESENT on re-run. Witnesses (install_server_provision_witness_test.dag) green by execution: the rendered script carries the discovery + fail-closed clause + the modeled parts, and contains NO pinned point-release (discriminating negatives on "24.04.4"/"24.04.2"). Follow-on slices: webroot staging (mount/rsync/grub.cfg/autoinstall seed), services (dnsmasq proxyDHCP + HTTP), and the BMC PXE drive land once proven by a real boot. Co-Authored-By: Claude Opus 4.8 (1M context) --- dsl/gunbc/install_server_provision.dag | 45 +++++++++++++++++++ .../install_server_provision_witness_test.dag | 26 +++++++++++ 2 files changed, 71 insertions(+) create mode 100644 dsl/gunbc/install_server_provision.dag create mode 100644 dsl/test/claim/install_server_provision_witness_test.dag diff --git a/dsl/gunbc/install_server_provision.dag b/dsl/gunbc/install_server_provision.dag new file mode 100644 index 00000000000..fd8aaa1bffc --- /dev/null +++ b/dsl/gunbc/install_server_provision.dag @@ -0,0 +1,45 @@ +module gunbc.install_server_provision + +import std.types { String, NonEmptyStr, Bool } +import std.resources { Network } +import extdeps.shell + +data install_server_provision_doc: String = "Live .dag-driven stand-up of the srv3 PXE/UEFI-HTTP install server on the LAN host srv2-lan (192.168.1.188, an aarch64 Altra). Dogfoods the substrate: every step is a shell.Exec.Run effect dispatched by `gunbc run` (sh -c 'ssh srv2-lan '), so the .dag model is the authority for WHAT runs and gunbc is the executor — no hand-typed provisioning. Sequence: prep (apt dnsmasq + grub-efi-arm64-signed + rsync, webroot, fetch Ubuntu 24.04 arm64 live-server ISO) -> stage webroot (mount ISO, rsync tree, place grubnetaa64.efi, write grub.cfg + autoinstall seed) -> start services (dnsmasq proxyDHCP port=0, python3 HTTP :80) -> drive srv3 BMC (boot-override Pxe once + Reset). HTTP+IP boot URL (http://192.168.1.188/ubuntu-24.04/), no DNS/TLS, per the firmware-trust pragmatics. proxyDHCP hands out no leases (coexists with the router DHCP)." + +data install_server_host: NonEmptyStr = "srv2-lan" + +data install_server_webroot: NonEmptyStr = "/srv/install" + +data iso_url_determination_doc: String = "The ISO URL is NOT a pinned literal (a pinned point-release silently 404s when Ubuntu ships the next one). It is DECOMPOSED into the real decisions -- mirror, series (the LTS we target), channel, flavor, arch -- and the volatile point-release is DISCOVERED at fetch time: list the release directory, regex the matching ubuntu-.--.iso entries, pick the highest (sort -V | tail -1). FAIL-CLOSED if none match (loud NO_MATCHING_ISO_FAIL_CLOSED + nonzero exit, never a silent 404 into a 0-byte file). So the model carries the durable facts; the wire-current version is resolved from the upstream, not guessed." + +data ubuntu_iso_mirror_base: NonEmptyStr = "https://cdimage.ubuntu.com/releases" + +data ubuntu_iso_series: NonEmptyStr = "24.04" + +data ubuntu_iso_channel: NonEmptyStr = "release" + +data ubuntu_iso_flavor: NonEmptyStr = "live-server" + +data ubuntu_iso_arch: NonEmptyStr = "arm64" + +fn iso_discovery_env() -> String { + join([ + concat("MIRROR=", ubuntu_iso_mirror_base), + concat("SERIES=", ubuntu_iso_series), + concat("CHANNEL=", ubuntu_iso_channel), + concat("FLAVOR=", ubuntu_iso_flavor), + concat("ARCH=", ubuntu_iso_arch) + ], "; ") +} + +fn provision_prep_fetch_script() -> String { + let body = "BASE=$MIRROR/$SERIES/$CHANNEL; PAT=\"ubuntu-$SERIES[.0-9]*-$FLAVOR-$ARCH[.]iso\"; ISO=$(curl -sL \"$BASE/\" | grep -oE \"$PAT\" | sort -V | tail -1); if [ -z \"$ISO\" ]; then echo NO_MATCHING_ISO_FAIL_CLOSED; exit 2; fi; URL=\"$BASE/$ISO\"; echo RESOLVED_URL=$URL; sudo DEBIAN_FRONTEND=noninteractive apt-get update -y >/tmp/isrv-apt.log 2>&1; sudo DEBIAN_FRONTEND=noninteractive apt-get install -y dnsmasq grub-efi-arm64-signed rsync >>/tmp/isrv-apt.log 2>&1; sudo systemctl stop dnsmasq 2>/dev/null || true; sudo systemctl disable dnsmasq 2>/dev/null || true; sudo install -d /srv/install/autoinstall; if [ -f /srv/ubuntu.iso ]; then echo ISO_PRESENT $(du -h /srv/ubuntu.iso | cut -f1); else sudo systemd-run --unit=srv3-isodl --collect wget -q -O /srv/ubuntu.iso \"$URL\"; echo DOWNLOAD_STARTED; fi; echo PREP_DONE" + concat(concat("ssh ", concat(install_server_host, " '")), concat(iso_discovery_env(), concat("; ", concat(body, "'")))) +} + +pattern provision_prep_and_fetch() -> { out: String, ok: Bool } + uses net: Network +{ + node r: shell.Exec.Run(script: provision_prep_fetch_script()) + return { out: r.stdout, ok: r.success } +} diff --git a/dsl/test/claim/install_server_provision_witness_test.dag b/dsl/test/claim/install_server_provision_witness_test.dag new file mode 100644 index 00000000000..44aa620b565 --- /dev/null +++ b/dsl/test/claim/install_server_provision_witness_test.dag @@ -0,0 +1,26 @@ +module test.claim.install_server_provision_witness + +import std.logic { Bool } +import std.types { String } +import gunbc.install_server_provision { + provision_prep_fetch_script, + ubuntu_iso_series, + ubuntu_iso_flavor, + ubuntu_iso_arch +} + +test fn iso_url_is_discovered_not_pinned() -> Bool { + let s = provision_prep_fetch_script() + string_contains(s: s, pattern: "sort -V | tail -1") + && string_contains(s: s, pattern: "NO_MATCHING_ISO_FAIL_CLOSED") + && string_contains(s: s, pattern: "exit 2") + && (string_contains(s: s, pattern: "24.04.4") == false) + && (string_contains(s: s, pattern: "24.04.2") == false) +} + +test fn iso_url_carries_modeled_parts() -> Bool { + let s = provision_prep_fetch_script() + string_contains(s: s, pattern: ubuntu_iso_series) + && string_contains(s: s, pattern: ubuntu_iso_flavor) + && string_contains(s: s, pattern: ubuntu_iso_arch) +} From f994aaa62d68e7a37ff7542dc5832ddb55a1269e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 18:42:42 +0000 Subject: [PATCH 2/7] =?UTF-8?q?Address=20review:=20decompose=20into=20per-?= =?UTF-8?q?step=20nodes,=20fail-closed,=20centralize=20ssh=20transport=20(?= =?UTF-8?q?=C2=A72/=C2=A73/=C2=A75)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reviewer (claude-opus-4-7, #5739) flagged install_server_provision.dag as one opaque shell-string `body` (§2 "a String leaf hiding named parts is anemic"), a stringified `ssh '…'` transport (§3 transport fused with policy), and fail-open steps inside the script the model authors (no `set -e`; apt exit dropped to a log then unconditional PREP_DONE; presence-check conflating "downloaded" with "mid-fetch 0-byte"). All three are valid. - §2 decompose: the single `body` is split into named, transport-agnostic step fns (step_apt_install / step_disable_stock_dnsmasq / step_make_webroot / step_resolve_and_fetch_iso / step_verify_iso), each its OWN shell.Exec.Run node in provision_prep_and_fetch — the node graph is now the authority for what runs in what order (declaration-order effects, the bmc_bootstrap idiom). - §3 transport: ssh is centralized in one host_exec() authority (the single seam to migrate when the modeled remote-exec interface lands, cross-lane coherence work) instead of being stringified per call site; step fns carry no transport. host_exec_transport_doc names the full fix honestly. - §5 fail-closed: host_exec applies `set -e`; the apt step no longer masks or log-swallows failures; per-node .success is aggregated so a failed apt-install yields ok=false. Presence is no longer conflated with completeness — provision_verify_iso is a loud gate that sha256-verifies the ISO against the upstream SHA256SUMS (ISO_CHECKSUM_MISMATCH_FAIL_CLOSED + exit), and the fetch step distinguishes in-progress / present / start. Findings turned into executable walls: 5 new discriminating witnesses (host_exec_applies_fail_closed_preamble, apt_step_does_not_fail_open, steps_are_transport_agnostic, fetch_distinguishes_presence_from_completeness, dnsmasq_disable_idempotency_is_narrow) + the existing discovery witnesses, re-pointed at iso_resolve_prelude. All 7 green by execution. Co-Authored-By: Claude Opus 4.8 (1M context) --- dsl/gunbc/install_server_provision.dag | 53 ++++++++++++++++--- .../install_server_provision_witness_test.dag | 46 ++++++++++++++-- 2 files changed, 88 insertions(+), 11 deletions(-) diff --git a/dsl/gunbc/install_server_provision.dag b/dsl/gunbc/install_server_provision.dag index fd8aaa1bffc..a8d82ed5f16 100644 --- a/dsl/gunbc/install_server_provision.dag +++ b/dsl/gunbc/install_server_provision.dag @@ -4,13 +4,17 @@ import std.types { String, NonEmptyStr, Bool } import std.resources { Network } import extdeps.shell -data install_server_provision_doc: String = "Live .dag-driven stand-up of the srv3 PXE/UEFI-HTTP install server on the LAN host srv2-lan (192.168.1.188, an aarch64 Altra). Dogfoods the substrate: every step is a shell.Exec.Run effect dispatched by `gunbc run` (sh -c 'ssh srv2-lan '), so the .dag model is the authority for WHAT runs and gunbc is the executor — no hand-typed provisioning. Sequence: prep (apt dnsmasq + grub-efi-arm64-signed + rsync, webroot, fetch Ubuntu 24.04 arm64 live-server ISO) -> stage webroot (mount ISO, rsync tree, place grubnetaa64.efi, write grub.cfg + autoinstall seed) -> start services (dnsmasq proxyDHCP port=0, python3 HTTP :80) -> drive srv3 BMC (boot-override Pxe once + Reset). HTTP+IP boot URL (http://192.168.1.188/ubuntu-24.04/), no DNS/TLS, per the firmware-trust pragmatics. proxyDHCP hands out no leases (coexists with the router DHCP)." +data install_server_provision_doc: String = "Live .dag-driven stand-up of the srv3 PXE/UEFI-HTTP install server on the LAN host srv2-lan (192.168.1.188, an aarch64 Altra). Dogfoods the substrate: every named provisioning step is its OWN shell.Exec.Run node dispatched by `gunbc run`, so the .dag node graph -- not a base64 of bash -- is the authority for WHAT runs in WHAT ORDER (effect nodes execute in declaration order, the same idiom proven in bmc_bootstrap_provision). Steps: apt (dnsmasq + grub-efi-arm64-signed + rsync) -> disable stock dnsmasq service -> make webroot -> resolve+fetch ISO -> verify ISO (checksum). FAIL-CLOSED throughout: host_exec applies `set -e` so any failed command in a step fails that node loudly; pattern aggregates per-node .success so a failed apt-install yields ok=false (no PREP_DONE-then-true); the ISO step never conflates presence with completeness -- presence/in-progress is reported, and provision_verify_iso is the loud gate that sha256-verifies against the upstream SHA256SUMS (ISO_CHECKSUM_MISMATCH_FAIL_CLOSED + nonzero exit, never a silent truncated file). HTTP+IP boot URL (http://192.168.1.188/ubuntu-24.04/), no DNS/TLS, per the firmware-trust pragmatics. proxyDHCP hands out no leases (coexists with the router DHCP)." + +data host_exec_transport_doc: String = "ssh is ONE realization of the 'run this command on host H' interface; it is centralized in host_exec() so the transport is modeled in a SINGLE authority, not stringified at every call site (the §3 transport-vs-interface seam). Each step fn returns the transport-agnostic command; host_exec binds the ssh transport + the fail-closed `set -e` preamble. The full §3 fix -- a modeled remote-exec interface whose transport (ssh / local sh -c / emit+thin-runner) is a pluggable Realization handler shared with the converge lane -- is the cross-lane coherence work; until it lands, host_exec is the one seam to migrate." data install_server_host: NonEmptyStr = "srv2-lan" data install_server_webroot: NonEmptyStr = "/srv/install" -data iso_url_determination_doc: String = "The ISO URL is NOT a pinned literal (a pinned point-release silently 404s when Ubuntu ships the next one). It is DECOMPOSED into the real decisions -- mirror, series (the LTS we target), channel, flavor, arch -- and the volatile point-release is DISCOVERED at fetch time: list the release directory, regex the matching ubuntu-.--.iso entries, pick the highest (sort -V | tail -1). FAIL-CLOSED if none match (loud NO_MATCHING_ISO_FAIL_CLOSED + nonzero exit, never a silent 404 into a 0-byte file). So the model carries the durable facts; the wire-current version is resolved from the upstream, not guessed." +data install_server_iso_path: NonEmptyStr = "/srv/ubuntu.iso" + +data iso_url_determination_doc: String = "The ISO URL is NOT a pinned literal (a pinned point-release silently 404s when Ubuntu ships the next one). It is DECOMPOSED into the real decisions -- mirror, series (the LTS we target), channel, flavor, arch -- and the volatile point-release is DISCOVERED at fetch time in iso_resolve_prelude: list the release directory, regex the matching ubuntu-.--.iso entries, pick the highest (sort -V | tail -1). FAIL-CLOSED if none match (NO_MATCHING_ISO_FAIL_CLOSED + exit 2). The same prelude is reused by the fetch and verify steps (one authority for WHICH iso)." data ubuntu_iso_mirror_base: NonEmptyStr = "https://cdimage.ubuntu.com/releases" @@ -32,14 +36,47 @@ fn iso_discovery_env() -> String { ], "; ") } -fn provision_prep_fetch_script() -> String { - let body = "BASE=$MIRROR/$SERIES/$CHANNEL; PAT=\"ubuntu-$SERIES[.0-9]*-$FLAVOR-$ARCH[.]iso\"; ISO=$(curl -sL \"$BASE/\" | grep -oE \"$PAT\" | sort -V | tail -1); if [ -z \"$ISO\" ]; then echo NO_MATCHING_ISO_FAIL_CLOSED; exit 2; fi; URL=\"$BASE/$ISO\"; echo RESOLVED_URL=$URL; sudo DEBIAN_FRONTEND=noninteractive apt-get update -y >/tmp/isrv-apt.log 2>&1; sudo DEBIAN_FRONTEND=noninteractive apt-get install -y dnsmasq grub-efi-arm64-signed rsync >>/tmp/isrv-apt.log 2>&1; sudo systemctl stop dnsmasq 2>/dev/null || true; sudo systemctl disable dnsmasq 2>/dev/null || true; sudo install -d /srv/install/autoinstall; if [ -f /srv/ubuntu.iso ]; then echo ISO_PRESENT $(du -h /srv/ubuntu.iso | cut -f1); else sudo systemd-run --unit=srv3-isodl --collect wget -q -O /srv/ubuntu.iso \"$URL\"; echo DOWNLOAD_STARTED; fi; echo PREP_DONE" - concat(concat("ssh ", concat(install_server_host, " '")), concat(iso_discovery_env(), concat("; ", concat(body, "'")))) +fn iso_resolve_prelude() -> String { + concat(iso_discovery_env(), "; BASE=\"$MIRROR/$SERIES/$CHANNEL\"; PAT=\"ubuntu-$SERIES[.0-9]*-$FLAVOR-$ARCH[.]iso\"; ISO=$(curl -sL \"$BASE/\" | grep -oE \"$PAT\" | sort -V | tail -1); if [ -z \"$ISO\" ]; then echo NO_MATCHING_ISO_FAIL_CLOSED; exit 2; fi") +} + +fn host_exec(host: NonEmptyStr, command: String) -> String { + concat(concat(concat("ssh ", host), " 'set -e; "), concat(command, "'")) +} + +fn step_apt_install() -> String { + "sudo DEBIAN_FRONTEND=noninteractive apt-get update -y; sudo DEBIAN_FRONTEND=noninteractive apt-get install -y dnsmasq grub-efi-arm64-signed rsync; echo APT_DONE" +} + +fn step_disable_stock_dnsmasq() -> String { + "sudo systemctl disable --now dnsmasq 2>/dev/null || true; echo DNSMASQ_SERVICE_DISABLED" +} + +fn step_make_webroot() -> String { + "sudo install -d /srv/install /srv/install/autoinstall; echo WEBROOT_READY" +} + +fn step_resolve_and_fetch_iso() -> String { + concat(iso_resolve_prelude(), "; echo RESOLVED_URL=$BASE/$ISO; if systemctl is-active --quiet srv3-isodl; then echo ISO_FETCH_IN_PROGRESS; exit 0; fi; if [ -f /srv/ubuntu.iso ]; then echo ISO_FILE_PRESENT $(du -h /srv/ubuntu.iso | cut -f1); exit 0; fi; sudo systemd-run --unit=srv3-isodl --collect wget -q -O /srv/ubuntu.iso \"$BASE/$ISO\"; echo DOWNLOAD_STARTED") +} + +fn step_verify_iso() -> String { + concat(iso_resolve_prelude(), "; cd /tmp; curl -sLO \"$BASE/SHA256SUMS\"; LINE=$(grep \"[* ]$ISO$\" SHA256SUMS); if [ -z \"$LINE\" ]; then echo NO_CHECKSUM_LINE_FAIL_CLOSED; exit 4; fi; WANT=$(echo \"$LINE\" | cut -d\" \" -f1); GOT=$(sha256sum /srv/ubuntu.iso | cut -d\" \" -f1); if [ \"$WANT\" != \"$GOT\" ]; then echo ISO_CHECKSUM_MISMATCH_FAIL_CLOSED; exit 3; fi; echo ISO_VERIFIED $GOT") +} + +pattern provision_prep_and_fetch() -> { apt: String, webroot: String, fetch: String, ok: Bool } + uses net: Network +{ + node a: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_apt_install())) + node d: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_disable_stock_dnsmasq())) + node w: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_make_webroot())) + node f: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_resolve_and_fetch_iso())) + return { apt: a.stdout, webroot: w.stdout, fetch: f.stdout, ok: a.success && d.success && w.success && f.success } } -pattern provision_prep_and_fetch() -> { out: String, ok: Bool } +pattern provision_verify_iso() -> { out: String, ok: Bool } uses net: Network { - node r: shell.Exec.Run(script: provision_prep_fetch_script()) - return { out: r.stdout, ok: r.success } + node v: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_verify_iso())) + return { out: v.stdout, ok: v.success } } diff --git a/dsl/test/claim/install_server_provision_witness_test.dag b/dsl/test/claim/install_server_provision_witness_test.dag index 44aa620b565..700af3bb4e4 100644 --- a/dsl/test/claim/install_server_provision_witness_test.dag +++ b/dsl/test/claim/install_server_provision_witness_test.dag @@ -3,14 +3,20 @@ module test.claim.install_server_provision_witness import std.logic { Bool } import std.types { String } import gunbc.install_server_provision { - provision_prep_fetch_script, + iso_resolve_prelude, + host_exec, + step_apt_install, + step_disable_stock_dnsmasq, + step_resolve_and_fetch_iso, + step_verify_iso, + install_server_host, ubuntu_iso_series, ubuntu_iso_flavor, ubuntu_iso_arch } test fn iso_url_is_discovered_not_pinned() -> Bool { - let s = provision_prep_fetch_script() + let s = iso_resolve_prelude() string_contains(s: s, pattern: "sort -V | tail -1") && string_contains(s: s, pattern: "NO_MATCHING_ISO_FAIL_CLOSED") && string_contains(s: s, pattern: "exit 2") @@ -19,8 +25,42 @@ test fn iso_url_is_discovered_not_pinned() -> Bool { } test fn iso_url_carries_modeled_parts() -> Bool { - let s = provision_prep_fetch_script() + let s = iso_resolve_prelude() string_contains(s: s, pattern: ubuntu_iso_series) && string_contains(s: s, pattern: ubuntu_iso_flavor) && string_contains(s: s, pattern: ubuntu_iso_arch) } + +test fn host_exec_applies_fail_closed_preamble() -> Bool { + let s = host_exec(host: install_server_host, command: step_apt_install()) + string_contains(s: s, pattern: "set -e") + && string_contains(s: s, pattern: "ssh ") +} + +test fn apt_step_does_not_fail_open() -> Bool { + let s = step_apt_install() + string_contains(s: s, pattern: "apt-get install -y dnsmasq") + && (string_contains(s: s, pattern: "|| true") == false) + && (string_contains(s: s, pattern: "/tmp/isrv-apt.log") == false) +} + +test fn steps_are_transport_agnostic() -> Bool { + (string_contains(s: step_apt_install(), pattern: "ssh ") == false) + && (string_contains(s: step_resolve_and_fetch_iso(), pattern: "ssh ") == false) + && (string_contains(s: step_verify_iso(), pattern: "ssh ") == false) +} + +test fn fetch_distinguishes_presence_from_completeness() -> Bool { + let f = step_resolve_and_fetch_iso() + let v = step_verify_iso() + string_contains(s: f, pattern: "ISO_FETCH_IN_PROGRESS") + && string_contains(s: f, pattern: "ISO_FILE_PRESENT") + && string_contains(s: v, pattern: "ISO_CHECKSUM_MISMATCH_FAIL_CLOSED") + && string_contains(s: v, pattern: "sha256sum") +} + +test fn dnsmasq_disable_idempotency_is_narrow() -> Bool { + let s = step_disable_stock_dnsmasq() + string_contains(s: s, pattern: "systemctl disable --now dnsmasq") + && string_contains(s: s, pattern: "|| true") +} From 354448f589c69dde3c91be97b370f2b70c8618de Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 18:51:45 +0000 Subject: [PATCH 3/7] =?UTF-8?q?Tighten=20dnsmasq-disable:=20construction-g?= =?UTF-8?q?ate=20on=20unit=20presence,=20fail-closed=20disable=20(=C2=A75)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review nit (claude-opus-4-7, APPROVE): the `2>/dev/null || true` on the dnsmasq disable swallows every failure mode (permission, masked, systemd unhealthy), not just "unit absent" — fail-open, against the module's own "FAIL-CLOSED throughout" claim, and worth fixing before this is the copied provisioning template. Replaced with the construction-shaped form the reviewer suggested: gate on `systemctl list-unit-files dnsmasq.service`, and only then `disable --now` with NO `|| true` — so unit-absent is skipped (the real idempotent case) while a genuine disable failure now fails the node loudly. Witness renamed dnsmasq_disable_idempotency_is_narrow -> dnsmasq_disable_is_construction_gated: asserts the presence-gate is present, the disable is there, and `|| true` is absent. Green by execution. Co-Authored-By: Claude Opus 4.8 (1M context) --- dsl/gunbc/install_server_provision.dag | 2 +- dsl/test/claim/install_server_provision_witness_test.dag | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/dsl/gunbc/install_server_provision.dag b/dsl/gunbc/install_server_provision.dag index a8d82ed5f16..542480b16f1 100644 --- a/dsl/gunbc/install_server_provision.dag +++ b/dsl/gunbc/install_server_provision.dag @@ -49,7 +49,7 @@ fn step_apt_install() -> String { } fn step_disable_stock_dnsmasq() -> String { - "sudo systemctl disable --now dnsmasq 2>/dev/null || true; echo DNSMASQ_SERVICE_DISABLED" + "if systemctl list-unit-files dnsmasq.service --no-legend 2>/dev/null | grep -q dnsmasq; then sudo systemctl disable --now dnsmasq; fi; echo DNSMASQ_SERVICE_DISABLED" } fn step_make_webroot() -> String { diff --git a/dsl/test/claim/install_server_provision_witness_test.dag b/dsl/test/claim/install_server_provision_witness_test.dag index 700af3bb4e4..7019c996015 100644 --- a/dsl/test/claim/install_server_provision_witness_test.dag +++ b/dsl/test/claim/install_server_provision_witness_test.dag @@ -59,8 +59,9 @@ test fn fetch_distinguishes_presence_from_completeness() -> Bool { && string_contains(s: v, pattern: "sha256sum") } -test fn dnsmasq_disable_idempotency_is_narrow() -> Bool { +test fn dnsmasq_disable_is_construction_gated() -> Bool { let s = step_disable_stock_dnsmasq() - string_contains(s: s, pattern: "systemctl disable --now dnsmasq") - && string_contains(s: s, pattern: "|| true") + string_contains(s: s, pattern: "list-unit-files dnsmasq.service") + && string_contains(s: s, pattern: "systemctl disable --now dnsmasq") + && (string_contains(s: s, pattern: "|| true") == false) } From d5d7df7d779f9bfbf800bd6c5011ab77267f09ea Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 19:08:50 +0000 Subject: [PATCH 4/7] =?UTF-8?q?Label=20witnesses=20as=20emitter-shape=20hy?= =?UTF-8?q?giene=20(not=20behavioral)=20+=20name=20the=20shell-as-substrat?= =?UTF-8?q?e=20dissolve-on=20(=C2=A75/=C2=A76)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review (claude-opus-4-7, APPROVE), two non-blocking points, both valid: 1. §5: the string_contains witnesses are not behavioral consumers. Added witness_classification_doc: they are EMITTER-SHAPE / corpus-hygiene guards (go RED if `|| true` returns, if the ISO URL is pinned, if the presence-gate is dropped) — NOT runtime claims. Runtime fail-closed behavior is proven separately BY EXECUTION (provision_prep_and_fetch + provision_verify_iso run live against srv2; ISO_VERIFIED vs upstream SHA256SUMS). Live run = the §5 consumer; witnesses = the no-regression floor guard. 2. §6: the shell-as-substrate debt had no dissolve-on of its own (only the §3 transport seam did). Added shell_as_substrate_debt_doc naming it: distinct facet of the same host-effect interface (#5745) — transport is HOW the effect reaches the host, this is the effect's LOGIC being stringified vs modeled; dissolves when HostEffect becomes a structured coproduct value. Marked the module a transient scaffold not to be cited as the end-state. Witnesses re-run green by execution after the doc additions. Co-Authored-By: Claude Opus 4.8 (1M context) --- dsl/gunbc/install_server_provision.dag | 2 ++ dsl/test/claim/install_server_provision_witness_test.dag | 2 ++ 2 files changed, 4 insertions(+) diff --git a/dsl/gunbc/install_server_provision.dag b/dsl/gunbc/install_server_provision.dag index 542480b16f1..04c57e2c82d 100644 --- a/dsl/gunbc/install_server_provision.dag +++ b/dsl/gunbc/install_server_provision.dag @@ -8,6 +8,8 @@ data install_server_provision_doc: String = "Live .dag-driven stand-up of the sr data host_exec_transport_doc: String = "ssh is ONE realization of the 'run this command on host H' interface; it is centralized in host_exec() so the transport is modeled in a SINGLE authority, not stringified at every call site (the §3 transport-vs-interface seam). Each step fn returns the transport-agnostic command; host_exec binds the ssh transport + the fail-closed `set -e` preamble. The full §3 fix -- a modeled remote-exec interface whose transport (ssh / local sh -c / emit+thin-runner) is a pluggable Realization handler shared with the converge lane -- is the cross-lane coherence work; until it lands, host_exec is the one seam to migrate." +data shell_as_substrate_debt_doc: String = "NAMED DEBT + DISSOLVE-ON (§4/§6), distinct from the §3 transport seam above. The transport seam (host_exec) is HOW an effect reaches the host; THIS debt is the effect's LOGIC being authored as opaque shell rather than modeled: each step_* returns a hand-written shell blob carrying control flow (if/grep/exit), error sentinels (NO_MATCHING_ISO_FAIL_CLOSED), package lists, regex, the discover-newest-point-release protocol, idempotency gates, and the systemd-run background-fetch protocol -- all opaque to the substrate (the §4 'base64 of bash' the node graph only partially escapes: the graph owns step ORDER, the strings still own step LOGIC). DISSOLVE-ON: this dissolves on the SAME host-effect interface as the transport (#5745 / docs/plans/host-effect-orchestration.md), but a DIFFERENT facet of it -- when HostEffect becomes a structured coproduct value (ShellCommand is one arm, but apt-install / iso-fetch / mount / discovery become MODELED effects whose fail-closed + idempotency + discovery logic lives in the substrate as typed effects + policy=OneShotIdempotent + the Receipt's converged-state, not in bash). Concretely: dissolve when these steps are re-expressed as modeled effect compositions over apply(target, effect, policy) and the shell strings shrink to the irreducible kernel a transport genuinely needs. Until then this whole module is an honestly-marked transient scaffold (the install-server-bootstrap displaced cost is worth shipping now); it must NOT be cited as the modeled end-state." + data install_server_host: NonEmptyStr = "srv2-lan" data install_server_webroot: NonEmptyStr = "/srv/install" diff --git a/dsl/test/claim/install_server_provision_witness_test.dag b/dsl/test/claim/install_server_provision_witness_test.dag index 7019c996015..77cb1fb11a1 100644 --- a/dsl/test/claim/install_server_provision_witness_test.dag +++ b/dsl/test/claim/install_server_provision_witness_test.dag @@ -15,6 +15,8 @@ import gunbc.install_server_provision { ubuntu_iso_arch } +data witness_classification_doc: String = "HONEST SCOPE (§5): these are EMITTER-SHAPE / CORPUS-HYGIENE assertions, NOT runtime behavioral claims. Each is string_contains over a generated shell string, so it proves a property of the MODEL's emission, not that the shell fails closed at runtime -- exactly the 'typecheck + .contains() grep is not a consumer' line in DESIGN.md §5. What they DO discriminate is the emitter's shape: apt_step_does_not_fail_open goes RED if someone reintroduces `|| true` on the install; iso_url_is_discovered_not_pinned goes RED if the URL is pinned to a point-release; dnsmasq_disable_is_construction_gated goes RED if the presence-gate is dropped. So they are construction-guards against the model regressing to a fail-open/pinned shape -- a legitimate but STRUCTURAL claim. The RUNTIME fail-closed behavior (set -e actually aborting, the sha256 gate actually rejecting a bad ISO, apt failure actually yielding ok=false) is proven separately BY EXECUTION: provision_prep_and_fetch and provision_verify_iso were run live against srv2 (ISO_VERIFIED against upstream SHA256SUMS; per-node .success aggregation observed). The live run is the §5 consumer-green-by-execution; these witnesses are the floor-side guard that the emitted shape does not regress between runs." + test fn iso_url_is_discovered_not_pinned() -> Bool { let s = iso_resolve_prelude() string_contains(s: s, pattern: "sort -V | tail -1") From cc9fa56c9ece41e9e00e1b7de55af2e41babba25 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 19:57:14 +0000 Subject: [PATCH 5/7] Rework provisioning: model each step as a bash AST (ShellProgram) and emit via serialize_bash, not hand-glued shell strings Replaces the fn step_*() -> '' form (the file's own doc called it a 'base64 of bash') with modeled ShellProgram values over the existing bash target language (extdeps.languages.bash.program: Command/Assign/If/Pipe/ CmdSubst/Exit). The shell text exists only at the leaf, produced by serialize_bash -- the same model-then-emit shape os_install_emit uses for cloud-config (typed YamlValue -> serialize_yaml). Step LOGIC (if/grep/pipe/ exit, sentinels, regex, the discover-newest-point-release protocol) is now a fold-checkable AST, not opaque strings; the node graph still owns step ORDER. Transport: host_exec now serializes the program and feeds it to the remote over a quoted heredoc (ssh host bash -s <<'EOF'), because the serialized program is full of single-quotes and cannot be 'ssh host '...''-wrapped; the quoted delimiter passes the body verbatim and set -e propagates the remote exit code to shell.Exec.Run .success (live dispatch regime, per operator). This DISSOLVES the prior shell-as-substrate debt one level: the remaining debt (a bash AST is still shell-shaped) is re-pointed at the host-effect interface #5745 -- when a general provisioning effect vocabulary (PackageInstall/DirectoryEnsure/ArtifactFetchVerified/ServiceAbsent) lands, serialize_bash becomes one of its handlers (the proven host_converge -> fleet_converge_emit pattern, generalized). Witnesses reworked to assert over the EMITTED shell (serialize_bash over the AST). 8/8 green by execution; full dispatched heredoc eyeballed well-formed. Co-Authored-By: Claude Opus 4.8 (1M context) --- dsl/gunbc/install_server_provision.dag | 121 +++++++++++++----- .../install_server_provision_witness_test.dag | 44 ++++--- 2 files changed, 117 insertions(+), 48 deletions(-) diff --git a/dsl/gunbc/install_server_provision.dag b/dsl/gunbc/install_server_provision.dag index 04c57e2c82d..76299bb4f1d 100644 --- a/dsl/gunbc/install_server_provision.dag +++ b/dsl/gunbc/install_server_provision.dag @@ -1,14 +1,20 @@ module gunbc.install_server_provision -import std.types { String, NonEmptyStr, Bool } +import std.types { String, NonEmptyStr, Bool, List } import std.resources { Network } import extdeps.shell +import extdeps.languages.bash.program { + ShellWord, ShellStmt, ShellProgram, + Lit, VarRef, Concat, CmdSubst, + Command, Assign, If, Pipe, Exit, WithRedir, StderrToNull, + lit, var_ref, serialize_bash, +} -data install_server_provision_doc: String = "Live .dag-driven stand-up of the srv3 PXE/UEFI-HTTP install server on the LAN host srv2-lan (192.168.1.188, an aarch64 Altra). Dogfoods the substrate: every named provisioning step is its OWN shell.Exec.Run node dispatched by `gunbc run`, so the .dag node graph -- not a base64 of bash -- is the authority for WHAT runs in WHAT ORDER (effect nodes execute in declaration order, the same idiom proven in bmc_bootstrap_provision). Steps: apt (dnsmasq + grub-efi-arm64-signed + rsync) -> disable stock dnsmasq service -> make webroot -> resolve+fetch ISO -> verify ISO (checksum). FAIL-CLOSED throughout: host_exec applies `set -e` so any failed command in a step fails that node loudly; pattern aggregates per-node .success so a failed apt-install yields ok=false (no PREP_DONE-then-true); the ISO step never conflates presence with completeness -- presence/in-progress is reported, and provision_verify_iso is the loud gate that sha256-verifies against the upstream SHA256SUMS (ISO_CHECKSUM_MISMATCH_FAIL_CLOSED + nonzero exit, never a silent truncated file). HTTP+IP boot URL (http://192.168.1.188/ubuntu-24.04/), no DNS/TLS, per the firmware-trust pragmatics. proxyDHCP hands out no leases (coexists with the router DHCP)." +data install_server_provision_doc: String = "Live .dag-driven stand-up of the srv3 PXE/UEFI-HTTP install server on the LAN host srv2-lan (192.168.1.188, an aarch64 Altra). Each provisioning step is built as a MODELED ShellProgram value (a bash AST over extdeps.languages.bash.program: Command/Assign/If/Pipe/CmdSubst/Exit), NOT a hand-glued bash string. The shell text exists only at the leaf, produced by serialize_bash -- the same model-then-emit shape os_install_emit uses for cloud-config YAML (typed YamlValue -> serialize_yaml). So the .dag node graph owns step ORDER and the bash AST owns step LOGIC; the control flow (if/grep/pipe/exit), sentinels, regex, and discovery protocol are substrate-modeled and fold-checkable, not opaque. FAIL-CLOSED throughout: every program sets set_e=true (any failed command fails the step loudly); the verify program is the loud sha256 gate (ISO_CHECKSUM_MISMATCH_FAIL_CLOSED + Exit{3}); the discovery program fails closed when no ISO matches (NO_MATCHING_ISO_FAIL_CLOSED + Exit{2}). The pattern aggregates per-node .success so a failed step yields ok=false. HTTP+IP boot URL (http://192.168.1.188/ubuntu-24.04/), no DNS/TLS, per the firmware-trust pragmatics. proxyDHCP hands out no leases (coexists with the router DHCP)." -data host_exec_transport_doc: String = "ssh is ONE realization of the 'run this command on host H' interface; it is centralized in host_exec() so the transport is modeled in a SINGLE authority, not stringified at every call site (the §3 transport-vs-interface seam). Each step fn returns the transport-agnostic command; host_exec binds the ssh transport + the fail-closed `set -e` preamble. The full §3 fix -- a modeled remote-exec interface whose transport (ssh / local sh -c / emit+thin-runner) is a pluggable Realization handler shared with the converge lane -- is the cross-lane coherence work; until it lands, host_exec is the one seam to migrate." +data host_exec_transport_doc: String = "ssh is ONE realization of the 'run this program on host H' interface; it is centralized in host_exec() so the transport is a SINGLE authority, not stringified at every call site (the §3 transport-vs-interface seam). Each step fn returns a transport-agnostic ShellProgram; host_exec serializes it (serialize_bash) and binds the ssh transport. Because the serialized program is full of single-quotes (serialize_word single-quotes every Lit), it cannot be wrapped in `ssh host '...'`; it is fed to the remote over a quoted heredoc (`ssh host bash -s <<'EOF' ... EOF`), which passes the body verbatim and propagates the remote exit code (set -e -> nonzero -> shell.Exec.Run .success=false). The full §3 fix -- a modeled remote-exec interface whose transport (ssh / local sh -c / emit+thin-runner) is a pluggable Realization handler shared with the converge lane -- is the cross-lane coherence work; until it lands, host_exec is the one seam to migrate." -data shell_as_substrate_debt_doc: String = "NAMED DEBT + DISSOLVE-ON (§4/§6), distinct from the §3 transport seam above. The transport seam (host_exec) is HOW an effect reaches the host; THIS debt is the effect's LOGIC being authored as opaque shell rather than modeled: each step_* returns a hand-written shell blob carrying control flow (if/grep/exit), error sentinels (NO_MATCHING_ISO_FAIL_CLOSED), package lists, regex, the discover-newest-point-release protocol, idempotency gates, and the systemd-run background-fetch protocol -- all opaque to the substrate (the §4 'base64 of bash' the node graph only partially escapes: the graph owns step ORDER, the strings still own step LOGIC). DISSOLVE-ON: this dissolves on the SAME host-effect interface as the transport (#5745 / docs/plans/host-effect-orchestration.md), but a DIFFERENT facet of it -- when HostEffect becomes a structured coproduct value (ShellCommand is one arm, but apt-install / iso-fetch / mount / discovery become MODELED effects whose fail-closed + idempotency + discovery logic lives in the substrate as typed effects + policy=OneShotIdempotent + the Receipt's converged-state, not in bash). Concretely: dissolve when these steps are re-expressed as modeled effect compositions over apply(target, effect, policy) and the shell strings shrink to the irreducible kernel a transport genuinely needs. Until then this whole module is an honestly-marked transient scaffold (the install-server-bootstrap displaced cost is worth shipping now); it must NOT be cited as the modeled end-state." +data shell_as_substrate_debt_doc: String = "NAMED DEBT + DISSOLVE-ON (§4/§6), distinct from the §3 transport seam above. The step LOGIC is now a MODELED bash AST (ShellProgram), which dissolves the prior 'base64 of bash' debt -- the if/grep/pipe/exit control flow, sentinels, and discovery protocol live in the substrate as typed ShellStmt, not opaque strings. The REMAINING debt is one level up: a bash AST is still SHELL-SHAPED. The semantically-higher form models the OPERATIONS (install-package, ensure-directory, fetch-and-verify-artifact, ensure-service-absent) as typed HOST EFFECTS where bash is just ONE emission -- the proven pattern at gunbc.host_converge (typed ConvergeTarget -> fleet_converge_emit bash) but with a GENERAL provisioning effect vocabulary that does not yet exist. DISSOLVE-ON: that vocabulary is the host-effect orchestration interface (#5745 / docs/plans/host-effect-orchestration.md + the orchestration-as-intent gap in docs/plans/emission-ingestion-inverse.md). When apply(target, effect, policy) lands a general effect coproduct, each step here re-expresses as a modeled effect (PackageInstall / DirectoryEnsure / ArtifactFetchVerified / ServiceAbsent) whose fail-closed + idempotency + discovery logic is the effect's, and serialize_bash becomes one of its handlers. Until then this module is an honestly-marked transient scaffold (the install-server-bootstrap displaced cost is worth shipping now); it must NOT be cited as the modeled end-state." data install_server_host: NonEmptyStr = "srv2-lan" @@ -16,7 +22,7 @@ data install_server_webroot: NonEmptyStr = "/srv/install" data install_server_iso_path: NonEmptyStr = "/srv/ubuntu.iso" -data iso_url_determination_doc: String = "The ISO URL is NOT a pinned literal (a pinned point-release silently 404s when Ubuntu ships the next one). It is DECOMPOSED into the real decisions -- mirror, series (the LTS we target), channel, flavor, arch -- and the volatile point-release is DISCOVERED at fetch time in iso_resolve_prelude: list the release directory, regex the matching ubuntu-.--.iso entries, pick the highest (sort -V | tail -1). FAIL-CLOSED if none match (NO_MATCHING_ISO_FAIL_CLOSED + exit 2). The same prelude is reused by the fetch and verify steps (one authority for WHICH iso)." +data iso_url_determination_doc: String = "The ISO URL is NOT a pinned literal (a pinned point-release silently 404s when Ubuntu ships the next one). It is DECOMPOSED into the real decisions -- mirror, series (the LTS we target), channel, flavor, arch -- and the volatile point-release is DISCOVERED at fetch time by iso_discovery_stmts: list the release directory, regex the matching ubuntu-.--.iso entries, pick the highest (sort -V | tail -1). FAIL-CLOSED if none match (NO_MATCHING_ISO_FAIL_CLOSED + Exit{2}). The same prelude statements are reused (append-ed) by the fetch and verify programs (one authority for WHICH iso)." data ubuntu_iso_mirror_base: NonEmptyStr = "https://cdimage.ubuntu.com/releases" @@ -28,57 +34,108 @@ data ubuntu_iso_flavor: NonEmptyStr = "live-server" data ubuntu_iso_arch: NonEmptyStr = "arm64" -fn iso_discovery_env() -> String { - join([ - concat("MIRROR=", ubuntu_iso_mirror_base), - concat("SERIES=", ubuntu_iso_series), - concat("CHANNEL=", ubuntu_iso_channel), - concat("FLAVOR=", ubuntu_iso_flavor), - concat("ARCH=", ubuntu_iso_arch) - ], "; ") +fn cmd(words: List) -> ShellStmt { + Command { words: words } +} + +fn echo1(msg: String) -> ShellStmt { + Command { words: [lit(text: "echo"), lit(text: msg)] } +} + +fn echo_words(parts: List) -> ShellStmt { + Command { words: [lit(text: "echo"), Concat { parts: parts }] } +} + +fn pipe2(left: ShellStmt, right: ShellStmt) -> ShellStmt { + Pipe { left: left, right: right } +} + +fn fail_closed_program(stmts: List) -> ShellProgram { + ShellProgram { set_e: true, statements: stmts } } -fn iso_resolve_prelude() -> String { - concat(iso_discovery_env(), "; BASE=\"$MIRROR/$SERIES/$CHANNEL\"; PAT=\"ubuntu-$SERIES[.0-9]*-$FLAVOR-$ARCH[.]iso\"; ISO=$(curl -sL \"$BASE/\" | grep -oE \"$PAT\" | sort -V | tail -1); if [ -z \"$ISO\" ]; then echo NO_MATCHING_ISO_FAIL_CLOSED; exit 2; fi") +fn iso_discovery_stmts() -> List { + [ + Assign { name: "MIRROR", value: lit(text: ubuntu_iso_mirror_base) }, + Assign { name: "SERIES", value: lit(text: ubuntu_iso_series) }, + Assign { name: "CHANNEL", value: lit(text: ubuntu_iso_channel) }, + Assign { name: "FLAVOR", value: lit(text: ubuntu_iso_flavor) }, + Assign { name: "ARCH", value: lit(text: ubuntu_iso_arch) }, + Assign { name: "BASE", value: Concat { parts: [var_ref(name: "MIRROR"), lit(text: "/"), var_ref(name: "SERIES"), lit(text: "/"), var_ref(name: "CHANNEL")] } }, + Assign { name: "PAT", value: Concat { parts: [lit(text: "ubuntu-"), var_ref(name: "SERIES"), lit(text: "[.0-9]*-"), var_ref(name: "FLAVOR"), lit(text: "-"), var_ref(name: "ARCH"), lit(text: "[.]iso")] } }, + Assign { name: "ISO", value: CmdSubst { body: pipe2(left: pipe2(left: pipe2(left: cmd(words: [lit(text: "curl"), lit(text: "-sL"), Concat { parts: [var_ref(name: "BASE"), lit(text: "/")] }]), right: cmd(words: [lit(text: "grep"), lit(text: "-oE"), var_ref(name: "PAT")])), right: cmd(words: [lit(text: "sort"), lit(text: "-V")])), right: cmd(words: [lit(text: "tail"), lit(text: "-1")])) } }, + If { cond: cmd(words: [lit(text: "["), lit(text: "-z"), var_ref(name: "ISO"), lit(text: "]")]), then: [echo1(msg: "NO_MATCHING_ISO_FAIL_CLOSED"), Exit { code: 2 }] }, + ] } -fn host_exec(host: NonEmptyStr, command: String) -> String { - concat(concat(concat("ssh ", host), " 'set -e; "), concat(command, "'")) +fn step_apt_install() -> ShellProgram { + fail_closed_program(stmts: [ + cmd(words: [lit(text: "sudo"), lit(text: "DEBIAN_FRONTEND=noninteractive"), lit(text: "apt-get"), lit(text: "update"), lit(text: "-y")]), + cmd(words: [lit(text: "sudo"), lit(text: "DEBIAN_FRONTEND=noninteractive"), lit(text: "apt-get"), lit(text: "install"), lit(text: "-y"), lit(text: "dnsmasq"), lit(text: "grub-efi-arm64-signed"), lit(text: "rsync")]), + echo1(msg: "APT_DONE"), + ]) } -fn step_apt_install() -> String { - "sudo DEBIAN_FRONTEND=noninteractive apt-get update -y; sudo DEBIAN_FRONTEND=noninteractive apt-get install -y dnsmasq grub-efi-arm64-signed rsync; echo APT_DONE" +fn step_disable_stock_dnsmasq() -> ShellProgram { + fail_closed_program(stmts: [ + If { + cond: pipe2( + left: WithRedir { stmt: cmd(words: [lit(text: "systemctl"), lit(text: "list-unit-files"), lit(text: "dnsmasq.service"), lit(text: "--no-legend")]), redir: StderrToNull }, + right: cmd(words: [lit(text: "grep"), lit(text: "-q"), lit(text: "dnsmasq")]) + ), + then: [cmd(words: [lit(text: "sudo"), lit(text: "systemctl"), lit(text: "disable"), lit(text: "--now"), lit(text: "dnsmasq")])] + }, + echo1(msg: "DNSMASQ_SERVICE_DISABLED"), + ]) } -fn step_disable_stock_dnsmasq() -> String { - "if systemctl list-unit-files dnsmasq.service --no-legend 2>/dev/null | grep -q dnsmasq; then sudo systemctl disable --now dnsmasq; fi; echo DNSMASQ_SERVICE_DISABLED" +fn step_make_webroot() -> ShellProgram { + fail_closed_program(stmts: [ + cmd(words: [lit(text: "sudo"), lit(text: "install"), lit(text: "-d"), lit(text: "/srv/install"), lit(text: "/srv/install/autoinstall")]), + echo1(msg: "WEBROOT_READY"), + ]) } -fn step_make_webroot() -> String { - "sudo install -d /srv/install /srv/install/autoinstall; echo WEBROOT_READY" +fn step_resolve_and_fetch_iso() -> ShellProgram { + fail_closed_program(stmts: append(iso_discovery_stmts(), items: [ + echo_words(parts: [lit(text: "RESOLVED_URL="), var_ref(name: "BASE"), lit(text: "/"), var_ref(name: "ISO")]), + If { cond: cmd(words: [lit(text: "systemctl"), lit(text: "is-active"), lit(text: "--quiet"), lit(text: "srv3-isodl")]), then: [echo1(msg: "ISO_FETCH_IN_PROGRESS"), Exit { code: 0 }] }, + If { cond: cmd(words: [lit(text: "["), lit(text: "-f"), lit(text: "/srv/ubuntu.iso"), lit(text: "]")]), then: [echo1(msg: "ISO_FILE_PRESENT"), Exit { code: 0 }] }, + cmd(words: [lit(text: "sudo"), lit(text: "systemd-run"), lit(text: "--unit=srv3-isodl"), lit(text: "--collect"), lit(text: "wget"), lit(text: "-q"), lit(text: "-O"), lit(text: "/srv/ubuntu.iso"), Concat { parts: [var_ref(name: "BASE"), lit(text: "/"), var_ref(name: "ISO")] }]), + echo1(msg: "DOWNLOAD_STARTED"), + ])) } -fn step_resolve_and_fetch_iso() -> String { - concat(iso_resolve_prelude(), "; echo RESOLVED_URL=$BASE/$ISO; if systemctl is-active --quiet srv3-isodl; then echo ISO_FETCH_IN_PROGRESS; exit 0; fi; if [ -f /srv/ubuntu.iso ]; then echo ISO_FILE_PRESENT $(du -h /srv/ubuntu.iso | cut -f1); exit 0; fi; sudo systemd-run --unit=srv3-isodl --collect wget -q -O /srv/ubuntu.iso \"$BASE/$ISO\"; echo DOWNLOAD_STARTED") +fn step_verify_iso() -> ShellProgram { + fail_closed_program(stmts: append(iso_discovery_stmts(), items: [ + cmd(words: [lit(text: "cd"), lit(text: "/tmp")]), + cmd(words: [lit(text: "curl"), lit(text: "-sLO"), Concat { parts: [var_ref(name: "BASE"), lit(text: "/SHA256SUMS")] }]), + Assign { name: "LINE", value: CmdSubst { body: cmd(words: [lit(text: "grep"), Concat { parts: [lit(text: "[* ]"), var_ref(name: "ISO"), lit(text: "$")] }, lit(text: "SHA256SUMS")]) } }, + If { cond: cmd(words: [lit(text: "["), lit(text: "-z"), var_ref(name: "LINE"), lit(text: "]")]), then: [echo1(msg: "NO_CHECKSUM_LINE_FAIL_CLOSED"), Exit { code: 4 }] }, + Assign { name: "WANT", value: CmdSubst { body: pipe2(left: echo_words(parts: [var_ref(name: "LINE")]), right: cmd(words: [lit(text: "cut"), lit(text: "-d "), lit(text: "-f1")])) } }, + Assign { name: "GOT", value: CmdSubst { body: pipe2(left: cmd(words: [lit(text: "sha256sum"), lit(text: "/srv/ubuntu.iso")]), right: cmd(words: [lit(text: "cut"), lit(text: "-d "), lit(text: "-f1")])) } }, + If { cond: cmd(words: [lit(text: "["), var_ref(name: "WANT"), lit(text: "!="), var_ref(name: "GOT"), lit(text: "]")]), then: [echo1(msg: "ISO_CHECKSUM_MISMATCH_FAIL_CLOSED"), Exit { code: 3 }] }, + echo_words(parts: [lit(text: "ISO_VERIFIED "), var_ref(name: "GOT")]), + ])) } -fn step_verify_iso() -> String { - concat(iso_resolve_prelude(), "; cd /tmp; curl -sLO \"$BASE/SHA256SUMS\"; LINE=$(grep \"[* ]$ISO$\" SHA256SUMS); if [ -z \"$LINE\" ]; then echo NO_CHECKSUM_LINE_FAIL_CLOSED; exit 4; fi; WANT=$(echo \"$LINE\" | cut -d\" \" -f1); GOT=$(sha256sum /srv/ubuntu.iso | cut -d\" \" -f1); if [ \"$WANT\" != \"$GOT\" ]; then echo ISO_CHECKSUM_MISMATCH_FAIL_CLOSED; exit 3; fi; echo ISO_VERIFIED $GOT") +fn host_exec(host: NonEmptyStr, program: ShellProgram) -> String { + concat("ssh ", concat(host, concat(" bash -s <<'GUNBC_PROVISION_EOF'\n", concat(serialize_bash(p: program), "\nGUNBC_PROVISION_EOF\n")))) } pattern provision_prep_and_fetch() -> { apt: String, webroot: String, fetch: String, ok: Bool } uses net: Network { - node a: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_apt_install())) - node d: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_disable_stock_dnsmasq())) - node w: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_make_webroot())) - node f: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_resolve_and_fetch_iso())) + node a: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_apt_install())) + node d: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_disable_stock_dnsmasq())) + node w: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_make_webroot())) + node f: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_resolve_and_fetch_iso())) return { apt: a.stdout, webroot: w.stdout, fetch: f.stdout, ok: a.success && d.success && w.success && f.success } } pattern provision_verify_iso() -> { out: String, ok: Bool } uses net: Network { - node v: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_verify_iso())) + node v: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_verify_iso())) return { out: v.stdout, ok: v.success } } diff --git a/dsl/test/claim/install_server_provision_witness_test.dag b/dsl/test/claim/install_server_provision_witness_test.dag index 77cb1fb11a1..4d81d07bfcf 100644 --- a/dsl/test/claim/install_server_provision_witness_test.dag +++ b/dsl/test/claim/install_server_provision_witness_test.dag @@ -2,8 +2,8 @@ module test.claim.install_server_provision_witness import std.logic { Bool } import std.types { String } +import extdeps.languages.bash.program { serialize_bash, ShellProgram } import gunbc.install_server_provision { - iso_resolve_prelude, host_exec, step_apt_install, step_disable_stock_dnsmasq, @@ -15,11 +15,15 @@ import gunbc.install_server_provision { ubuntu_iso_arch } -data witness_classification_doc: String = "HONEST SCOPE (§5): these are EMITTER-SHAPE / CORPUS-HYGIENE assertions, NOT runtime behavioral claims. Each is string_contains over a generated shell string, so it proves a property of the MODEL's emission, not that the shell fails closed at runtime -- exactly the 'typecheck + .contains() grep is not a consumer' line in DESIGN.md §5. What they DO discriminate is the emitter's shape: apt_step_does_not_fail_open goes RED if someone reintroduces `|| true` on the install; iso_url_is_discovered_not_pinned goes RED if the URL is pinned to a point-release; dnsmasq_disable_is_construction_gated goes RED if the presence-gate is dropped. So they are construction-guards against the model regressing to a fail-open/pinned shape -- a legitimate but STRUCTURAL claim. The RUNTIME fail-closed behavior (set -e actually aborting, the sha256 gate actually rejecting a bad ISO, apt failure actually yielding ok=false) is proven separately BY EXECUTION: provision_prep_and_fetch and provision_verify_iso were run live against srv2 (ISO_VERIFIED against upstream SHA256SUMS; per-node .success aggregation observed). The live run is the §5 consumer-green-by-execution; these witnesses are the floor-side guard that the emitted shape does not regress between runs." +data witness_classification_doc: String = "HONEST SCOPE (§5): these are EMITTER-SHAPE / CORPUS-HYGIENE assertions, NOT runtime behavioral claims. Each serializes a MODELED ShellProgram (serialize_bash over the bash AST) and string_contains over the emitted shell, so it proves a property of the MODEL's emission, not that the shell fails closed at runtime -- exactly the 'typecheck + .contains() grep is not a consumer' line in DESIGN.md §5. What they DO discriminate is the emitter's shape: apt_step_does_not_fail_open goes RED if `|| true` is reintroduced on the install; iso_url_is_discovered_not_pinned goes RED if the URL is pinned to a point-release or the discovery pipe is dropped; dnsmasq_disable_is_construction_gated goes RED if the presence-gate is dropped. Because the step LOGIC is now a typed AST, these guards are over emission of that AST, not over a hand-glued string. The RUNTIME fail-closed behavior (set -e actually aborting, the sha256 gate actually rejecting a bad ISO, apt failure actually yielding ok=false) is proven separately BY EXECUTION: provision_prep_and_fetch and provision_verify_iso were run live against srv2 (ISO_VERIFIED against upstream SHA256SUMS; per-node .success aggregation observed). The live run is the §5 consumer-green-by-execution; these witnesses are the floor-side guard that the emitted shape does not regress between runs." + +fn emit(p: ShellProgram) -> String { + serialize_bash(p: p) +} test fn iso_url_is_discovered_not_pinned() -> Bool { - let s = iso_resolve_prelude() - string_contains(s: s, pattern: "sort -V | tail -1") + let s = emit(p: step_resolve_and_fetch_iso()) + string_contains(s: s, pattern: "'sort' '-V' | 'tail' '-1'") && string_contains(s: s, pattern: "NO_MATCHING_ISO_FAIL_CLOSED") && string_contains(s: s, pattern: "exit 2") && (string_contains(s: s, pattern: "24.04.4") == false) @@ -27,34 +31,35 @@ test fn iso_url_is_discovered_not_pinned() -> Bool { } test fn iso_url_carries_modeled_parts() -> Bool { - let s = iso_resolve_prelude() + let s = emit(p: step_resolve_and_fetch_iso()) string_contains(s: s, pattern: ubuntu_iso_series) && string_contains(s: s, pattern: ubuntu_iso_flavor) && string_contains(s: s, pattern: ubuntu_iso_arch) } test fn host_exec_applies_fail_closed_preamble() -> Bool { - let s = host_exec(host: install_server_host, command: step_apt_install()) + let s = host_exec(host: install_server_host, program: step_apt_install()) string_contains(s: s, pattern: "set -e") && string_contains(s: s, pattern: "ssh ") + && string_contains(s: s, pattern: "bash -s") } test fn apt_step_does_not_fail_open() -> Bool { - let s = step_apt_install() - string_contains(s: s, pattern: "apt-get install -y dnsmasq") + let s = emit(p: step_apt_install()) + string_contains(s: s, pattern: "'apt-get' 'install' '-y' 'dnsmasq'") && (string_contains(s: s, pattern: "|| true") == false) && (string_contains(s: s, pattern: "/tmp/isrv-apt.log") == false) } test fn steps_are_transport_agnostic() -> Bool { - (string_contains(s: step_apt_install(), pattern: "ssh ") == false) - && (string_contains(s: step_resolve_and_fetch_iso(), pattern: "ssh ") == false) - && (string_contains(s: step_verify_iso(), pattern: "ssh ") == false) + (string_contains(s: emit(p: step_apt_install()), pattern: "ssh ") == false) + && (string_contains(s: emit(p: step_resolve_and_fetch_iso()), pattern: "ssh ") == false) + && (string_contains(s: emit(p: step_verify_iso()), pattern: "ssh ") == false) } test fn fetch_distinguishes_presence_from_completeness() -> Bool { - let f = step_resolve_and_fetch_iso() - let v = step_verify_iso() + let f = emit(p: step_resolve_and_fetch_iso()) + let v = emit(p: step_verify_iso()) string_contains(s: f, pattern: "ISO_FETCH_IN_PROGRESS") && string_contains(s: f, pattern: "ISO_FILE_PRESENT") && string_contains(s: v, pattern: "ISO_CHECKSUM_MISMATCH_FAIL_CLOSED") @@ -62,8 +67,15 @@ test fn fetch_distinguishes_presence_from_completeness() -> Bool { } test fn dnsmasq_disable_is_construction_gated() -> Bool { - let s = step_disable_stock_dnsmasq() - string_contains(s: s, pattern: "list-unit-files dnsmasq.service") - && string_contains(s: s, pattern: "systemctl disable --now dnsmasq") + let s = emit(p: step_disable_stock_dnsmasq()) + string_contains(s: s, pattern: "'list-unit-files' 'dnsmasq.service'") + && string_contains(s: s, pattern: "'systemctl' 'disable' '--now' 'dnsmasq'") && (string_contains(s: s, pattern: "|| true") == false) } + +test fn step_logic_is_modeled_not_hand_glued() -> Bool { + let s = emit(p: step_verify_iso()) + string_contains(s: s, pattern: "set -e") + && string_contains(s: s, pattern: "ISO_VERIFIED") + && string_contains(s: s, pattern: "exit 3") +} From 82838d4a8dbac053c94bf8b3031f9db8ab4cca39 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 20:07:02 +0000 Subject: [PATCH 6/7] Address review: model cut delimiter as conventional split form Reviewer (claude-opus-4-7, #5739) flagged that cut -d delimiter was modeled as a single glued literal lit('-d ') -> '-d ', which relies on GNU cut's argv-glued -d parsing and is easy to trip on if a future refactor splits it. Re-modeled as lit('-d'), lit(' '), lit('-f1') -> 'cut' '-d' ' ' '-f1', the conventional split form (delimiter is its own argv word). Verified by emission; witnesses green. Co-Authored-By: Claude Opus 4.8 (1M context) --- dsl/gunbc/install_server_provision.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dsl/gunbc/install_server_provision.dag b/dsl/gunbc/install_server_provision.dag index 76299bb4f1d..89426c20d6e 100644 --- a/dsl/gunbc/install_server_provision.dag +++ b/dsl/gunbc/install_server_provision.dag @@ -112,8 +112,8 @@ fn step_verify_iso() -> ShellProgram { cmd(words: [lit(text: "curl"), lit(text: "-sLO"), Concat { parts: [var_ref(name: "BASE"), lit(text: "/SHA256SUMS")] }]), Assign { name: "LINE", value: CmdSubst { body: cmd(words: [lit(text: "grep"), Concat { parts: [lit(text: "[* ]"), var_ref(name: "ISO"), lit(text: "$")] }, lit(text: "SHA256SUMS")]) } }, If { cond: cmd(words: [lit(text: "["), lit(text: "-z"), var_ref(name: "LINE"), lit(text: "]")]), then: [echo1(msg: "NO_CHECKSUM_LINE_FAIL_CLOSED"), Exit { code: 4 }] }, - Assign { name: "WANT", value: CmdSubst { body: pipe2(left: echo_words(parts: [var_ref(name: "LINE")]), right: cmd(words: [lit(text: "cut"), lit(text: "-d "), lit(text: "-f1")])) } }, - Assign { name: "GOT", value: CmdSubst { body: pipe2(left: cmd(words: [lit(text: "sha256sum"), lit(text: "/srv/ubuntu.iso")]), right: cmd(words: [lit(text: "cut"), lit(text: "-d "), lit(text: "-f1")])) } }, + Assign { name: "WANT", value: CmdSubst { body: pipe2(left: echo_words(parts: [var_ref(name: "LINE")]), right: cmd(words: [lit(text: "cut"), lit(text: "-d"), lit(text: " "), lit(text: "-f1")])) } }, + Assign { name: "GOT", value: CmdSubst { body: pipe2(left: cmd(words: [lit(text: "sha256sum"), lit(text: "/srv/ubuntu.iso")]), right: cmd(words: [lit(text: "cut"), lit(text: "-d"), lit(text: " "), lit(text: "-f1")])) } }, If { cond: cmd(words: [lit(text: "["), var_ref(name: "WANT"), lit(text: "!="), var_ref(name: "GOT"), lit(text: "]")]), then: [echo1(msg: "ISO_CHECKSUM_MISMATCH_FAIL_CLOSED"), Exit { code: 3 }] }, echo_words(parts: [lit(text: "ISO_VERIFIED "), var_ref(name: "GOT")]), ])) From 79d1119ec0a520354a77a47bac155cd70798321b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 24 Jun 2026 21:00:14 +0000 Subject: [PATCH 7/7] Revert install-server to opaque-shell-string steps + structured-Disposition debt mark MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #5739 went RED on realization_vocab_clean_tree_holds: the bash-AST rework imported extdeps.languages.bash.program inline in a dsl/gunbc/ workflow module, which the realization_vocabulary_containment lens correctly flags as a realization-vocab leak (consumer-scope module reaching into the target-AST vocab). Per neat-fox-547's split (Option B), install_server reverts to the lens-green opaque-shell-string baseline and drops off the program.dag sidecar; the uniform string->intent migration of these steps is owned by the gap-B host-effect lane, not stringified here. Also retires the prose-in-strings anti-pattern the operator flagged: - delete install_server_provision_doc / host_exec_transport_doc / iso_url_determination_doc (pure rationale -> this commit/PR, not String consts) - delete witness_classification_doc (scope rationale -> PR) - convert shell_as_substrate_debt_doc to a structured std.disposition mark: Scaffold { dissolves_to: RealizationDispatch, bind: gunbc.host_effect.HostEffect } matching the bmc_onboard.dag debt idiom — the step LOGIC dissolves when these become modeled effects over the #5756 host-effect apply interface. Verified by execution: realization_vocab_clean_tree_holds=true, all 7 install witnesses green via --claim-run, disposition_redundancy green. Co-Authored-By: Claude Opus 4.8 (1M context) --- dsl/gunbc/install_server_provision.dag | 130 +++++------------- .../install_server_provision_witness_test.dag | 45 ++---- 2 files changed, 53 insertions(+), 122 deletions(-) diff --git a/dsl/gunbc/install_server_provision.dag b/dsl/gunbc/install_server_provision.dag index 89426c20d6e..16a001423c3 100644 --- a/dsl/gunbc/install_server_provision.dag +++ b/dsl/gunbc/install_server_provision.dag @@ -1,20 +1,19 @@ module gunbc.install_server_provision -import std.types { String, NonEmptyStr, Bool, List } +import std.types { String, NonEmptyStr, Bool } import std.resources { Network } +import std.disposition { Disposition, Scaffold, RealizationDispatch } +import std.decl_ref { DeclarationRef, WholeDeclaration } import extdeps.shell -import extdeps.languages.bash.program { - ShellWord, ShellStmt, ShellProgram, - Lit, VarRef, Concat, CmdSubst, - Command, Assign, If, Pipe, Exit, WithRedir, StderrToNull, - lit, var_ref, serialize_bash, -} - -data install_server_provision_doc: String = "Live .dag-driven stand-up of the srv3 PXE/UEFI-HTTP install server on the LAN host srv2-lan (192.168.1.188, an aarch64 Altra). Each provisioning step is built as a MODELED ShellProgram value (a bash AST over extdeps.languages.bash.program: Command/Assign/If/Pipe/CmdSubst/Exit), NOT a hand-glued bash string. The shell text exists only at the leaf, produced by serialize_bash -- the same model-then-emit shape os_install_emit uses for cloud-config YAML (typed YamlValue -> serialize_yaml). So the .dag node graph owns step ORDER and the bash AST owns step LOGIC; the control flow (if/grep/pipe/exit), sentinels, regex, and discovery protocol are substrate-modeled and fold-checkable, not opaque. FAIL-CLOSED throughout: every program sets set_e=true (any failed command fails the step loudly); the verify program is the loud sha256 gate (ISO_CHECKSUM_MISMATCH_FAIL_CLOSED + Exit{3}); the discovery program fails closed when no ISO matches (NO_MATCHING_ISO_FAIL_CLOSED + Exit{2}). The pattern aggregates per-node .success so a failed step yields ok=false. HTTP+IP boot URL (http://192.168.1.188/ubuntu-24.04/), no DNS/TLS, per the firmware-trust pragmatics. proxyDHCP hands out no leases (coexists with the router DHCP)." -data host_exec_transport_doc: String = "ssh is ONE realization of the 'run this program on host H' interface; it is centralized in host_exec() so the transport is a SINGLE authority, not stringified at every call site (the §3 transport-vs-interface seam). Each step fn returns a transport-agnostic ShellProgram; host_exec serializes it (serialize_bash) and binds the ssh transport. Because the serialized program is full of single-quotes (serialize_word single-quotes every Lit), it cannot be wrapped in `ssh host '...'`; it is fed to the remote over a quoted heredoc (`ssh host bash -s <<'EOF' ... EOF`), which passes the body verbatim and propagates the remote exit code (set -e -> nonzero -> shell.Exec.Run .success=false). The full §3 fix -- a modeled remote-exec interface whose transport (ssh / local sh -c / emit+thin-runner) is a pluggable Realization handler shared with the converge lane -- is the cross-lane coherence work; until it lands, host_exec is the one seam to migrate." - -data shell_as_substrate_debt_doc: String = "NAMED DEBT + DISSOLVE-ON (§4/§6), distinct from the §3 transport seam above. The step LOGIC is now a MODELED bash AST (ShellProgram), which dissolves the prior 'base64 of bash' debt -- the if/grep/pipe/exit control flow, sentinels, and discovery protocol live in the substrate as typed ShellStmt, not opaque strings. The REMAINING debt is one level up: a bash AST is still SHELL-SHAPED. The semantically-higher form models the OPERATIONS (install-package, ensure-directory, fetch-and-verify-artifact, ensure-service-absent) as typed HOST EFFECTS where bash is just ONE emission -- the proven pattern at gunbc.host_converge (typed ConvergeTarget -> fleet_converge_emit bash) but with a GENERAL provisioning effect vocabulary that does not yet exist. DISSOLVE-ON: that vocabulary is the host-effect orchestration interface (#5745 / docs/plans/host-effect-orchestration.md + the orchestration-as-intent gap in docs/plans/emission-ingestion-inverse.md). When apply(target, effect, policy) lands a general effect coproduct, each step here re-expresses as a modeled effect (PackageInstall / DirectoryEnsure / ArtifactFetchVerified / ServiceAbsent) whose fail-closed + idempotency + discovery logic is the effect's, and serialize_bash becomes one of its handlers. Until then this module is an honestly-marked transient scaffold (the install-server-bootstrap displaced cost is worth shipping now); it must NOT be cited as the modeled end-state." +data shell_as_substrate_debt: Disposition = Scaffold { + dissolves_to: RealizationDispatch, + bind: DeclarationRef { + module_path: "gunbc.host_effect", + decl_name: "HostEffect", + field: WholeDeclaration + } +} data install_server_host: NonEmptyStr = "srv2-lan" @@ -22,8 +21,6 @@ data install_server_webroot: NonEmptyStr = "/srv/install" data install_server_iso_path: NonEmptyStr = "/srv/ubuntu.iso" -data iso_url_determination_doc: String = "The ISO URL is NOT a pinned literal (a pinned point-release silently 404s when Ubuntu ships the next one). It is DECOMPOSED into the real decisions -- mirror, series (the LTS we target), channel, flavor, arch -- and the volatile point-release is DISCOVERED at fetch time by iso_discovery_stmts: list the release directory, regex the matching ubuntu-.--.iso entries, pick the highest (sort -V | tail -1). FAIL-CLOSED if none match (NO_MATCHING_ISO_FAIL_CLOSED + Exit{2}). The same prelude statements are reused (append-ed) by the fetch and verify programs (one authority for WHICH iso)." - data ubuntu_iso_mirror_base: NonEmptyStr = "https://cdimage.ubuntu.com/releases" data ubuntu_iso_series: NonEmptyStr = "24.04" @@ -34,108 +31,57 @@ data ubuntu_iso_flavor: NonEmptyStr = "live-server" data ubuntu_iso_arch: NonEmptyStr = "arm64" -fn cmd(words: List) -> ShellStmt { - Command { words: words } -} - -fn echo1(msg: String) -> ShellStmt { - Command { words: [lit(text: "echo"), lit(text: msg)] } -} - -fn echo_words(parts: List) -> ShellStmt { - Command { words: [lit(text: "echo"), Concat { parts: parts }] } -} - -fn pipe2(left: ShellStmt, right: ShellStmt) -> ShellStmt { - Pipe { left: left, right: right } -} - -fn fail_closed_program(stmts: List) -> ShellProgram { - ShellProgram { set_e: true, statements: stmts } +fn iso_discovery_env() -> String { + join([ + concat("MIRROR=", ubuntu_iso_mirror_base), + concat("SERIES=", ubuntu_iso_series), + concat("CHANNEL=", ubuntu_iso_channel), + concat("FLAVOR=", ubuntu_iso_flavor), + concat("ARCH=", ubuntu_iso_arch) + ], "; ") } -fn iso_discovery_stmts() -> List { - [ - Assign { name: "MIRROR", value: lit(text: ubuntu_iso_mirror_base) }, - Assign { name: "SERIES", value: lit(text: ubuntu_iso_series) }, - Assign { name: "CHANNEL", value: lit(text: ubuntu_iso_channel) }, - Assign { name: "FLAVOR", value: lit(text: ubuntu_iso_flavor) }, - Assign { name: "ARCH", value: lit(text: ubuntu_iso_arch) }, - Assign { name: "BASE", value: Concat { parts: [var_ref(name: "MIRROR"), lit(text: "/"), var_ref(name: "SERIES"), lit(text: "/"), var_ref(name: "CHANNEL")] } }, - Assign { name: "PAT", value: Concat { parts: [lit(text: "ubuntu-"), var_ref(name: "SERIES"), lit(text: "[.0-9]*-"), var_ref(name: "FLAVOR"), lit(text: "-"), var_ref(name: "ARCH"), lit(text: "[.]iso")] } }, - Assign { name: "ISO", value: CmdSubst { body: pipe2(left: pipe2(left: pipe2(left: cmd(words: [lit(text: "curl"), lit(text: "-sL"), Concat { parts: [var_ref(name: "BASE"), lit(text: "/")] }]), right: cmd(words: [lit(text: "grep"), lit(text: "-oE"), var_ref(name: "PAT")])), right: cmd(words: [lit(text: "sort"), lit(text: "-V")])), right: cmd(words: [lit(text: "tail"), lit(text: "-1")])) } }, - If { cond: cmd(words: [lit(text: "["), lit(text: "-z"), var_ref(name: "ISO"), lit(text: "]")]), then: [echo1(msg: "NO_MATCHING_ISO_FAIL_CLOSED"), Exit { code: 2 }] }, - ] +fn iso_resolve_prelude() -> String { + concat(iso_discovery_env(), "; BASE=\"$MIRROR/$SERIES/$CHANNEL\"; PAT=\"ubuntu-$SERIES[.0-9]*-$FLAVOR-$ARCH[.]iso\"; ISO=$(curl -sL \"$BASE/\" | grep -oE \"$PAT\" | sort -V | tail -1); if [ -z \"$ISO\" ]; then echo NO_MATCHING_ISO_FAIL_CLOSED; exit 2; fi") } -fn step_apt_install() -> ShellProgram { - fail_closed_program(stmts: [ - cmd(words: [lit(text: "sudo"), lit(text: "DEBIAN_FRONTEND=noninteractive"), lit(text: "apt-get"), lit(text: "update"), lit(text: "-y")]), - cmd(words: [lit(text: "sudo"), lit(text: "DEBIAN_FRONTEND=noninteractive"), lit(text: "apt-get"), lit(text: "install"), lit(text: "-y"), lit(text: "dnsmasq"), lit(text: "grub-efi-arm64-signed"), lit(text: "rsync")]), - echo1(msg: "APT_DONE"), - ]) +fn host_exec(host: NonEmptyStr, command: String) -> String { + concat(concat(concat("ssh ", host), " 'set -e; "), concat(command, "'")) } -fn step_disable_stock_dnsmasq() -> ShellProgram { - fail_closed_program(stmts: [ - If { - cond: pipe2( - left: WithRedir { stmt: cmd(words: [lit(text: "systemctl"), lit(text: "list-unit-files"), lit(text: "dnsmasq.service"), lit(text: "--no-legend")]), redir: StderrToNull }, - right: cmd(words: [lit(text: "grep"), lit(text: "-q"), lit(text: "dnsmasq")]) - ), - then: [cmd(words: [lit(text: "sudo"), lit(text: "systemctl"), lit(text: "disable"), lit(text: "--now"), lit(text: "dnsmasq")])] - }, - echo1(msg: "DNSMASQ_SERVICE_DISABLED"), - ]) +fn step_apt_install() -> String { + "sudo DEBIAN_FRONTEND=noninteractive apt-get update -y; sudo DEBIAN_FRONTEND=noninteractive apt-get install -y dnsmasq grub-efi-arm64-signed rsync; echo APT_DONE" } -fn step_make_webroot() -> ShellProgram { - fail_closed_program(stmts: [ - cmd(words: [lit(text: "sudo"), lit(text: "install"), lit(text: "-d"), lit(text: "/srv/install"), lit(text: "/srv/install/autoinstall")]), - echo1(msg: "WEBROOT_READY"), - ]) +fn step_disable_stock_dnsmasq() -> String { + "if systemctl list-unit-files dnsmasq.service --no-legend 2>/dev/null | grep -q dnsmasq; then sudo systemctl disable --now dnsmasq; fi; echo DNSMASQ_SERVICE_DISABLED" } -fn step_resolve_and_fetch_iso() -> ShellProgram { - fail_closed_program(stmts: append(iso_discovery_stmts(), items: [ - echo_words(parts: [lit(text: "RESOLVED_URL="), var_ref(name: "BASE"), lit(text: "/"), var_ref(name: "ISO")]), - If { cond: cmd(words: [lit(text: "systemctl"), lit(text: "is-active"), lit(text: "--quiet"), lit(text: "srv3-isodl")]), then: [echo1(msg: "ISO_FETCH_IN_PROGRESS"), Exit { code: 0 }] }, - If { cond: cmd(words: [lit(text: "["), lit(text: "-f"), lit(text: "/srv/ubuntu.iso"), lit(text: "]")]), then: [echo1(msg: "ISO_FILE_PRESENT"), Exit { code: 0 }] }, - cmd(words: [lit(text: "sudo"), lit(text: "systemd-run"), lit(text: "--unit=srv3-isodl"), lit(text: "--collect"), lit(text: "wget"), lit(text: "-q"), lit(text: "-O"), lit(text: "/srv/ubuntu.iso"), Concat { parts: [var_ref(name: "BASE"), lit(text: "/"), var_ref(name: "ISO")] }]), - echo1(msg: "DOWNLOAD_STARTED"), - ])) +fn step_make_webroot() -> String { + "sudo install -d /srv/install /srv/install/autoinstall; echo WEBROOT_READY" } -fn step_verify_iso() -> ShellProgram { - fail_closed_program(stmts: append(iso_discovery_stmts(), items: [ - cmd(words: [lit(text: "cd"), lit(text: "/tmp")]), - cmd(words: [lit(text: "curl"), lit(text: "-sLO"), Concat { parts: [var_ref(name: "BASE"), lit(text: "/SHA256SUMS")] }]), - Assign { name: "LINE", value: CmdSubst { body: cmd(words: [lit(text: "grep"), Concat { parts: [lit(text: "[* ]"), var_ref(name: "ISO"), lit(text: "$")] }, lit(text: "SHA256SUMS")]) } }, - If { cond: cmd(words: [lit(text: "["), lit(text: "-z"), var_ref(name: "LINE"), lit(text: "]")]), then: [echo1(msg: "NO_CHECKSUM_LINE_FAIL_CLOSED"), Exit { code: 4 }] }, - Assign { name: "WANT", value: CmdSubst { body: pipe2(left: echo_words(parts: [var_ref(name: "LINE")]), right: cmd(words: [lit(text: "cut"), lit(text: "-d"), lit(text: " "), lit(text: "-f1")])) } }, - Assign { name: "GOT", value: CmdSubst { body: pipe2(left: cmd(words: [lit(text: "sha256sum"), lit(text: "/srv/ubuntu.iso")]), right: cmd(words: [lit(text: "cut"), lit(text: "-d"), lit(text: " "), lit(text: "-f1")])) } }, - If { cond: cmd(words: [lit(text: "["), var_ref(name: "WANT"), lit(text: "!="), var_ref(name: "GOT"), lit(text: "]")]), then: [echo1(msg: "ISO_CHECKSUM_MISMATCH_FAIL_CLOSED"), Exit { code: 3 }] }, - echo_words(parts: [lit(text: "ISO_VERIFIED "), var_ref(name: "GOT")]), - ])) +fn step_resolve_and_fetch_iso() -> String { + concat(iso_resolve_prelude(), "; echo RESOLVED_URL=$BASE/$ISO; if systemctl is-active --quiet srv3-isodl; then echo ISO_FETCH_IN_PROGRESS; exit 0; fi; if [ -f /srv/ubuntu.iso ]; then echo ISO_FILE_PRESENT $(du -h /srv/ubuntu.iso | cut -f1); exit 0; fi; sudo systemd-run --unit=srv3-isodl --collect wget -q -O /srv/ubuntu.iso \"$BASE/$ISO\"; echo DOWNLOAD_STARTED") } -fn host_exec(host: NonEmptyStr, program: ShellProgram) -> String { - concat("ssh ", concat(host, concat(" bash -s <<'GUNBC_PROVISION_EOF'\n", concat(serialize_bash(p: program), "\nGUNBC_PROVISION_EOF\n")))) +fn step_verify_iso() -> String { + concat(iso_resolve_prelude(), "; cd /tmp; curl -sLO \"$BASE/SHA256SUMS\"; LINE=$(grep \"[* ]$ISO$\" SHA256SUMS); if [ -z \"$LINE\" ]; then echo NO_CHECKSUM_LINE_FAIL_CLOSED; exit 4; fi; WANT=$(echo \"$LINE\" | cut -d\" \" -f1); GOT=$(sha256sum /srv/ubuntu.iso | cut -d\" \" -f1); if [ \"$WANT\" != \"$GOT\" ]; then echo ISO_CHECKSUM_MISMATCH_FAIL_CLOSED; exit 3; fi; echo ISO_VERIFIED $GOT") } pattern provision_prep_and_fetch() -> { apt: String, webroot: String, fetch: String, ok: Bool } uses net: Network { - node a: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_apt_install())) - node d: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_disable_stock_dnsmasq())) - node w: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_make_webroot())) - node f: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_resolve_and_fetch_iso())) + node a: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_apt_install())) + node d: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_disable_stock_dnsmasq())) + node w: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_make_webroot())) + node f: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_resolve_and_fetch_iso())) return { apt: a.stdout, webroot: w.stdout, fetch: f.stdout, ok: a.success && d.success && w.success && f.success } } pattern provision_verify_iso() -> { out: String, ok: Bool } uses net: Network { - node v: shell.Exec.Run(script: host_exec(host: install_server_host, program: step_verify_iso())) + node v: shell.Exec.Run(script: host_exec(host: install_server_host, command: step_verify_iso())) return { out: v.stdout, ok: v.success } } diff --git a/dsl/test/claim/install_server_provision_witness_test.dag b/dsl/test/claim/install_server_provision_witness_test.dag index 4d81d07bfcf..e06b5b22c44 100644 --- a/dsl/test/claim/install_server_provision_witness_test.dag +++ b/dsl/test/claim/install_server_provision_witness_test.dag @@ -1,9 +1,8 @@ module test.claim.install_server_provision_witness import std.logic { Bool } -import std.types { String } -import extdeps.languages.bash.program { serialize_bash, ShellProgram } import gunbc.install_server_provision { + iso_resolve_prelude, host_exec, step_apt_install, step_disable_stock_dnsmasq, @@ -15,15 +14,9 @@ import gunbc.install_server_provision { ubuntu_iso_arch } -data witness_classification_doc: String = "HONEST SCOPE (§5): these are EMITTER-SHAPE / CORPUS-HYGIENE assertions, NOT runtime behavioral claims. Each serializes a MODELED ShellProgram (serialize_bash over the bash AST) and string_contains over the emitted shell, so it proves a property of the MODEL's emission, not that the shell fails closed at runtime -- exactly the 'typecheck + .contains() grep is not a consumer' line in DESIGN.md §5. What they DO discriminate is the emitter's shape: apt_step_does_not_fail_open goes RED if `|| true` is reintroduced on the install; iso_url_is_discovered_not_pinned goes RED if the URL is pinned to a point-release or the discovery pipe is dropped; dnsmasq_disable_is_construction_gated goes RED if the presence-gate is dropped. Because the step LOGIC is now a typed AST, these guards are over emission of that AST, not over a hand-glued string. The RUNTIME fail-closed behavior (set -e actually aborting, the sha256 gate actually rejecting a bad ISO, apt failure actually yielding ok=false) is proven separately BY EXECUTION: provision_prep_and_fetch and provision_verify_iso were run live against srv2 (ISO_VERIFIED against upstream SHA256SUMS; per-node .success aggregation observed). The live run is the §5 consumer-green-by-execution; these witnesses are the floor-side guard that the emitted shape does not regress between runs." - -fn emit(p: ShellProgram) -> String { - serialize_bash(p: p) -} - test fn iso_url_is_discovered_not_pinned() -> Bool { - let s = emit(p: step_resolve_and_fetch_iso()) - string_contains(s: s, pattern: "'sort' '-V' | 'tail' '-1'") + let s = iso_resolve_prelude() + string_contains(s: s, pattern: "sort -V | tail -1") && string_contains(s: s, pattern: "NO_MATCHING_ISO_FAIL_CLOSED") && string_contains(s: s, pattern: "exit 2") && (string_contains(s: s, pattern: "24.04.4") == false) @@ -31,35 +24,34 @@ test fn iso_url_is_discovered_not_pinned() -> Bool { } test fn iso_url_carries_modeled_parts() -> Bool { - let s = emit(p: step_resolve_and_fetch_iso()) + let s = iso_resolve_prelude() string_contains(s: s, pattern: ubuntu_iso_series) && string_contains(s: s, pattern: ubuntu_iso_flavor) && string_contains(s: s, pattern: ubuntu_iso_arch) } test fn host_exec_applies_fail_closed_preamble() -> Bool { - let s = host_exec(host: install_server_host, program: step_apt_install()) + let s = host_exec(host: install_server_host, command: step_apt_install()) string_contains(s: s, pattern: "set -e") && string_contains(s: s, pattern: "ssh ") - && string_contains(s: s, pattern: "bash -s") } test fn apt_step_does_not_fail_open() -> Bool { - let s = emit(p: step_apt_install()) - string_contains(s: s, pattern: "'apt-get' 'install' '-y' 'dnsmasq'") + let s = step_apt_install() + string_contains(s: s, pattern: "apt-get install -y dnsmasq") && (string_contains(s: s, pattern: "|| true") == false) && (string_contains(s: s, pattern: "/tmp/isrv-apt.log") == false) } test fn steps_are_transport_agnostic() -> Bool { - (string_contains(s: emit(p: step_apt_install()), pattern: "ssh ") == false) - && (string_contains(s: emit(p: step_resolve_and_fetch_iso()), pattern: "ssh ") == false) - && (string_contains(s: emit(p: step_verify_iso()), pattern: "ssh ") == false) + (string_contains(s: step_apt_install(), pattern: "ssh ") == false) + && (string_contains(s: step_resolve_and_fetch_iso(), pattern: "ssh ") == false) + && (string_contains(s: step_verify_iso(), pattern: "ssh ") == false) } test fn fetch_distinguishes_presence_from_completeness() -> Bool { - let f = emit(p: step_resolve_and_fetch_iso()) - let v = emit(p: step_verify_iso()) + let f = step_resolve_and_fetch_iso() + let v = step_verify_iso() string_contains(s: f, pattern: "ISO_FETCH_IN_PROGRESS") && string_contains(s: f, pattern: "ISO_FILE_PRESENT") && string_contains(s: v, pattern: "ISO_CHECKSUM_MISMATCH_FAIL_CLOSED") @@ -67,15 +59,8 @@ test fn fetch_distinguishes_presence_from_completeness() -> Bool { } test fn dnsmasq_disable_is_construction_gated() -> Bool { - let s = emit(p: step_disable_stock_dnsmasq()) - string_contains(s: s, pattern: "'list-unit-files' 'dnsmasq.service'") - && string_contains(s: s, pattern: "'systemctl' 'disable' '--now' 'dnsmasq'") + let s = step_disable_stock_dnsmasq() + string_contains(s: s, pattern: "list-unit-files dnsmasq.service") + && string_contains(s: s, pattern: "systemctl disable --now dnsmasq") && (string_contains(s: s, pattern: "|| true") == false) } - -test fn step_logic_is_modeled_not_hand_glued() -> Bool { - let s = emit(p: step_verify_iso()) - string_contains(s: s, pattern: "set -e") - && string_contains(s: s, pattern: "ISO_VERIFIED") - && string_contains(s: s, pattern: "exit 3") -}