From 93bd9b879db68f1cd59a522d8549839ad22dc60f Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 27 Aug 2026 02:05:41 +0000 Subject: [PATCH 1/5] wip: OCI join + ContainerRuntime dissolution --- dag/extdeps/container/docker_engine.dag | 39 ++ dag/extdeps/container/engine.dag | 99 ++++ dag/extdeps/container/oci/image_config.dag | 22 + dag/extdeps/container/oci/reference.dag | 266 ++++++++++ dag/extdeps/software.dag | 19 + dag/extdeps/vendor/docker_inc.dag | 29 ++ dag/gunbc/ci_fleet.dag | 2 +- dag/gunbc/fleet_container.dag | 61 ++- dag/gunbc/fleet_intent.dag | 49 +- dag/product/fabric/customer_image.dag | 218 ++++++++ .../customer_image_admission_witness_test.dag | 471 ++++++++++++++++++ 11 files changed, 1258 insertions(+), 17 deletions(-) create mode 100644 dag/extdeps/container/docker_engine.dag create mode 100644 dag/extdeps/container/engine.dag create mode 100644 dag/extdeps/container/oci/reference.dag create mode 100644 dag/extdeps/software.dag create mode 100644 dag/extdeps/vendor/docker_inc.dag create mode 100644 dag/product/fabric/customer_image.dag create mode 100644 dag/test/claim/customer_image_admission_witness_test.dag diff --git a/dag/extdeps/container/docker_engine.dag b/dag/extdeps/container/docker_engine.dag new file mode 100644 index 00000000000..c18ec504897 --- /dev/null +++ b/dag/extdeps/container/docker_engine.dag @@ -0,0 +1,39 @@ +module extdeps.container.docker_engine + +import extdeps.container.engine { ContainerEngine, RootfulDaemon, RootlessDaemon } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } +import extdeps.vendor.docker_inc { docker_inc } +import std.decl_ref { DeclarationRef, WholeDeclaration } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "docs.docker.com/engine/security/rootless/" + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.container.docker_engine", + decl_name: "docker_engine", + field: WholeDeclaration + } + }, + first_citation: extdeps.container.docker_engine.extdeps_external_authority_anchor, + further_citations: [] +} + +// Docker Engine as a PRODUCT. Its Ubuntu apt distribution is a separate fact and keeps its own +// module (extdeps.container.docker_ce): how you install it is not what it is. +// +// Both privilege modes are cited: the rootless mode is documented at the anchor above as a +// supported way to run the daemon and the CLI as a non-root user, and the default installation is +// the rootful daemon that same page contrasts it with. The fleet runs the rootless mode, and that +// is recorded where the fleet is described, not here. +data docker_engine: ContainerEngine = ContainerEngine { + vendor: docker_inc, + product_name: "Docker Engine", + privilege_modes: [RootfulDaemon, RootlessDaemon], +} diff --git a/dag/extdeps/container/engine.dag b/dag/extdeps/container/engine.dag new file mode 100644 index 00000000000..c474af2fe0a --- /dev/null +++ b/dag/extdeps/container/engine.dag @@ -0,0 +1,99 @@ +module extdeps.container.engine + +import extdeps.external_authority { ExternalAuthority } +import extdeps.software { Software } +import extdeps.uri { Uri, Https } +import extdeps.vendor { Vendor } +import std.types { Bool, List, NonEmptyStr, String } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "github.com/opencontainers/runtime-spec/blob/main/spec.md" + } +} + +// THE AGNOSTIC SHAPE OF A THING THAT RUNS AN OCI IMAGE, WITH NO PRODUCT ENUMERATED IN IT. +// +// This hub defines what a container engine IS. It does not name Docker, Podman or anything else, +// and it deliberately carries no `match` over products: enumerating them here is precisely the case +// DESIGN's external-upstream-decomposition section rules out with "adding Opera must not widen a +// generic browser-product enum". Each engine is an independently versioned upstream product with +// its own module authority and its own cited row; adding one is a new file, never an edit here. +// +// WHAT THIS REPLACES. `gunbc.fleet_intent` carried +// type ContainerRuntime = Docker | Podman | Gvisor | Ubicloud | GcloudRun +// which fused three unrelated concepts into five members of one enum: container engines (Docker, +// Podman), a sandboxing runtime whose whole point is the isolation guarantee it adds (gVisor), and +// two companies that rent you a machine (Ubicloud, Google Cloud Run). Widening it was the only way +// to add either an engine or a supplier, so the two questions could never be asked separately. + +type EnginePrivilegeMode + = RootfulDaemon + | RootlessDaemon + +fn engine_privilege_mode_label(mode: EnginePrivilegeMode) -> String { + match mode { + RootfulDaemon => "rootful" + RootlessDaemon => "rootless" + } +} + +// A PRODUCT CAPABILITY ROW, NOT A DEPLOYMENT. +// +// `privilege_modes` is what the PRODUCT supports, cited to its own docs. Which mode a particular +// host actually runs is a fact about that host and lives on the deployment below -- the +// interface / realization / policy split of DESIGN section 3. Fusing them is how "we run Docker" +// came to mean nothing about whether the daemon is root, which is the one property that decides +// whether a compromised job owns the machine. +type ContainerEngine { + vendor: Vendor + product_name: NonEmptyStr + privilege_modes: List +} + +fn container_engine_supports_privilege_mode(engine: ContainerEngine, mode: EnginePrivilegeMode) -> Bool { + any(engine.privilege_modes, m => m == mode) +} + +type EngineDeploymentRefusal + = PrivilegeModeUnsupported { product_name: NonEmptyStr, mode: EnginePrivilegeMode } + +// WHAT IS ACTUALLY INSTALLED SOMEWHERE, WHICH IS THE ENGINE PLUS ONE CHOICE ABOUT IT. +type ContainerEngineDeployment { + engine: ContainerEngine + privilege_mode: EnginePrivilegeMode +} + +type ContainerEngineDeploymentOutcome + = ContainerEngineDeployed { deployment: ContainerEngineDeployment } + | ContainerEngineDeploymentRefused { refusal: EngineDeploymentRefusal } + +// Claiming a mode the product does not offer is a declaration that cannot be true, so it refuses +// here rather than being carried as a surface fact nothing ever checks. +fn container_engine_deployment( + engine: ContainerEngine, + privilege_mode: EnginePrivilegeMode, +) -> ContainerEngineDeploymentOutcome { + if container_engine_supports_privilege_mode(engine: engine, mode: privilege_mode) { + ContainerEngineDeployed { + deployment: ContainerEngineDeployment { engine: engine, privilege_mode: privilege_mode }, + } + } else { + ContainerEngineDeploymentRefused { + refusal: PrivilegeModeUnsupported { + product_name: engine.product_name, + mode: privilege_mode, + }, + } + } +} + +fn container_engine_deployment_label(deployment: ContainerEngineDeployment) -> String { + concat( + deployment.engine.product_name as String, + " (", + engine_privilege_mode_label(mode: deployment.privilege_mode), + ")", + ) +} diff --git a/dag/extdeps/container/oci/image_config.dag b/dag/extdeps/container/oci/image_config.dag index a552c922baa..ad46ced7091 100644 --- a/dag/extdeps/container/oci/image_config.dag +++ b/dag/extdeps/container/oci/image_config.dag @@ -68,6 +68,28 @@ fn image_config_entrypoint(c: ImageConfiguration) -> List { } } +fn image_config_cmd(c: ImageConfiguration) -> List { + match c.config { + null => [] + cfg => + match cfg.Cmd { + null => [] + cmd => cmd + } + } +} + +// THE COMMAND A RUNTIME WOULD ACTUALLY EXECUTE, WHICH NEITHER FIELD ANSWERS ALONE. +// +// config.md defines the executed command as Entrypoint with Cmd appended as its arguments, so an +// image with only Cmd starts and an image with only Entrypoint starts, while an image with neither +// has nothing to run. A consumer reading either field on its own would refuse a startable image or +// admit an unstartable one; the concatenation is the fact, and it is modelled once here rather +// than re-derived by every consumer. +fn image_config_start_command(c: ImageConfiguration) -> List { + append(image_config_entrypoint(c: c), items: image_config_cmd(c: c)) +} + fn image_config_first_exposed_port(c: ImageConfiguration) -> ContainerExposedPort? { match c.config { null => null diff --git a/dag/extdeps/container/oci/reference.dag b/dag/extdeps/container/oci/reference.dag new file mode 100644 index 00000000000..70b1cea5fc6 --- /dev/null +++ b/dag/extdeps/container/oci/reference.dag @@ -0,0 +1,266 @@ +module extdeps.container.oci.reference + +import extdeps.container.oci.digest { OciContentDigest, render_oci_content_digest_wire } +import extdeps.dns.domain_name { HostName, domain_name_wire } +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.uri { Uri, Https } +import std.error_primitives { Result, Ok, Err } +import std.types { Bool, Int, List, Port, String } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "github.com/opencontainers/distribution-spec/blob/main/spec.md" + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.container.oci.reference", + decl_name: "OciImageReference", + field: WholeDeclaration + } + }, + first_citation: extdeps.container.oci.reference.extdeps_external_authority_anchor, + further_citations: [] +} + +// HOW AN IMAGE IS NAMED, WHICH THE OCI MODEL IN THIS DIRECTORY DID NOT CARRY. +// +// manifest.dag and image_config.dag model what an image IS once you hold its bytes. Nothing +// modelled how a party REFERS to one, so the only way to say "run this image" was a String -- the +// anemic leaf DESIGN section 2 names, hiding a registry host, a repository path and a mutable-or- +// immutable identifier behind one opaque scalar. +// +// BOTH IDENTIFIER ARMS ARE MODELLED, INCLUDING THE MUTABLE ONE, AND THAT IS DELIBERATE. A tag is a +// real thing the distribution spec defines; refusing to admit a tag is POLICY, and policy in an +// extdeps module is the layer inversion DESIGN section 3 rules out. The spec says what may be +// written; the consumer says what it will accept. + +fn oci_code_point_at(text: String, index: Int) -> Int { + code_point(substring(s: text, start: index, end: index + 1)) +} + +fn oci_lower_alnum_code_point(cp: Int) -> Bool { + (cp >= 48 && cp <= 57) || (cp >= 97 && cp <= 122) +} + +fn oci_separator_code_point(cp: Int) -> Bool { + cp == 46 || cp == 95 || cp == 45 +} + +// path-component := alpha-numeric [separator alpha-numeric]* +// separator := "." | "_" | "__" | "-"+ +// +// The separator alternatives are enumerated rather than collapsed to "one or more of ._-" because +// the spec admits a DOUBLE underscore and a single dot, and nothing else doubled: "a..b" and "a___b" +// are not repository names. A permissive reading here would be a fail-open at the naming boundary. +fn oci_hyphen_run(text: String, index: Int) -> Bool { + if index >= text.length() { + text.length() > 0 + } else if oci_code_point_at(text: text, index: index) == 45 { + oci_hyphen_run(text: text, index: index + 1) + } else { + false + } +} + +fn oci_separator_run_valid(run: String) -> Bool { + run == "." || run == "_" || run == "__" || oci_hyphen_run(text: run, index: 0) +} + +fn oci_separator_run_end(text: String, index: Int) -> Int { + if index >= text.length() { + index + } else if oci_separator_code_point(cp: oci_code_point_at(text: text, index: index)) { + oci_separator_run_end(text: text, index: index + 1) + } else { + index + } +} + +// Returns the index after a non-empty alpha-numeric run, or -1 when none starts at `index`. +fn oci_alnum_run_end(text: String, index: Int, consumed: Int) -> Int { + if index >= text.length() { + if consumed > 0 { index } else { -1 } + } else if oci_lower_alnum_code_point(cp: oci_code_point_at(text: text, index: index)) { + oci_alnum_run_end(text: text, index: index + 1, consumed: consumed + 1) + } else if consumed > 0 { + index + } else { + -1 + } +} + +fn oci_path_component_from(text: String, index: Int) -> Bool { + let after_alnum = oci_alnum_run_end(text: text, index: index, consumed: 0) + if after_alnum < 0 { + false + } else if after_alnum >= text.length() { + true + } else { + let separator_end = oci_separator_run_end(text: text, index: after_alnum) + if separator_end == after_alnum { + false + } else if !(oci_separator_run_valid(run: substring(s: text, start: after_alnum, end: separator_end))) { + false + } else { + oci_path_component_from(text: text, index: separator_end) + } + } +} + +fn oci_path_component_syntax(value: String) -> Bool { + value.length() > 0 && oci_path_component_from(text: value, index: 0) +} + +type OciPathComponent = String where oci_path_component_syntax + +// tag := [a-zA-Z0-9_][a-zA-Z0-9._-]{0,127} +fn oci_tag_leading_code_point(cp: Int) -> Bool { + oci_lower_alnum_code_point(cp: cp) || (cp >= 65 && cp <= 90) || cp == 95 +} + +fn oci_tag_trailing_code_point(cp: Int) -> Bool { + oci_tag_leading_code_point(cp: cp) || cp == 46 || cp == 45 +} + +fn oci_tag_tail_valid(text: String, index: Int) -> Bool { + if index >= text.length() { + true + } else if oci_tag_trailing_code_point(cp: oci_code_point_at(text: text, index: index)) { + oci_tag_tail_valid(text: text, index: index + 1) + } else { + false + } +} + +fn oci_tag_syntax(value: String) -> Bool { + value.length() > 0 + && value.length() <= 128 + && oci_tag_leading_code_point(cp: oci_code_point_at(text: value, index: 0)) + && oci_tag_tail_valid(text: value, index: 1) +} + +type OciTag = String where oci_tag_syntax + +type OciRegistry { + host: HostName + port: Port? +} + +type OciRepositoryName { + components: List +} + +// THE ONE AXIS THAT DECIDES WHETHER A REFERENCE NAMES FIXED BYTES. +// +// A digest reference resolves to exactly one set of bytes forever; a tag resolves to whatever the +// registry currently points it at, so two pulls of one tag are two different programs. That is a +// difference in KIND, not a nullable field, which is why this is a coproduct: a record with both +// slots optional admits "neither" and "both", neither of which a reference can be. +type OciReferenceIdentifier + = ReferenceByDigest(OciContentDigest) + | ReferenceByTag(OciTag) + +// registry is optional because the spec's grammar makes the host optional; what a bare name +// resolves to is a CLIENT default (Docker Hub for one client, a mirror for another), so filling it +// in here would author a policy fact as an upstream one. +type OciImageReference { + registry: OciRegistry? + repository: OciRepositoryName + identifier: OciReferenceIdentifier +} + +type OciReferenceRejectReason + = EmptyRepositoryName + | BadPathComponent { raw: String } + | BadTag { raw: String } + +fn oci_path_component(raw: String) -> Result { + if oci_path_component_syntax(value: raw) { + Ok { value: raw as OciPathComponent } + } else { + Err { value: BadPathComponent { raw: raw } } + } +} + +fn oci_tag(raw: String) -> Result { + if oci_tag_syntax(value: raw) { + Ok { value: raw as OciTag } + } else { + Err { value: BadTag { raw: raw } } + } +} + +fn oci_repository_path_components( + segments: List, + index: Int, + acc: List, +) -> Result, OciReferenceRejectReason> { + if index >= count(segments) { + Ok { value: acc } + } else { + match segments |> get(index) { + Absent => Err { value: EmptyRepositoryName } + Present { value: segment } => + match oci_path_component(raw: segment) { + Err { value: e } => Err { value: e } + Ok { value: component } => + oci_repository_path_components( + segments: segments, + index: index + 1, + acc: append(acc, items: [component]), + ) + } + } + } +} + +fn oci_repository_name(raw: String) -> Result { + let segments = split(s: raw, delimiter: "/") + if count(segments) == 0 { + Err { value: EmptyRepositoryName } + } else { + match oci_repository_path_components(segments: segments, index: 0, acc: []) { + Err { value: e } => Err { value: e } + Ok { value: components } => Ok { value: OciRepositoryName { components: components } } + } + } +} + +fn oci_repository_name_wire(name: OciRepositoryName) -> String { + join(map(name.components, c => c as String), "/") +} + +fn oci_registry_wire(registry: OciRegistry) -> String { + match registry.port { + Absent => domain_name_wire(name: registry.host.name) + Present { value: port } => + concat(domain_name_wire(name: registry.host.name), ":", to_string(port)) + } +} + +// Emission is the structural inverse of the grammar above, not a second spelling of it: the +// separator between repository and identifier is "@" for a digest and ":" for a tag, which is +// exactly the distinction OciReferenceIdentifier carries. +fn render_oci_image_reference(reference: OciImageReference) -> String { + let named = match reference.registry { + Absent => oci_repository_name_wire(name: reference.repository) + Present { value: registry } => + concat(oci_registry_wire(registry: registry), "/", oci_repository_name_wire(name: reference.repository)) + } + match reference.identifier { + ReferenceByDigest(digest) => concat(named, "@", render_oci_content_digest_wire(d: digest)) + ReferenceByTag(tag) => concat(named, ":", tag as String) + } +} + +fn oci_reference_is_digest_pinned(reference: OciImageReference) -> Bool { + match reference.identifier { + ReferenceByDigest(_) => true + ReferenceByTag(_) => false + } +} diff --git a/dag/extdeps/software.dag b/dag/extdeps/software.dag new file mode 100644 index 00000000000..8b31cec0a79 --- /dev/null +++ b/dag/extdeps/software.dag @@ -0,0 +1,19 @@ +module extdeps.software + +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "en.wikipedia.org/wiki/Software" + } +} + +// The domain tag for Vendor, peer to extdeps.hardware Hardware. +// +// A software vendor is not a securities issuer and not a hardware manufacturer, and the two +// domains already in the tree cover neither: Docker, Inc. and Red Hat are companies whose +// governed product is a program. Vendor is the single authority (DESIGN section 3); this +// file adds the missing domain rather than a second vendor concept for software. +type Software diff --git a/dag/extdeps/vendor/docker_inc.dag b/dag/extdeps/vendor/docker_inc.dag new file mode 100644 index 00000000000..deb5c686fd4 --- /dev/null +++ b/dag/extdeps/vendor/docker_inc.dag @@ -0,0 +1,29 @@ +module extdeps.vendor.docker_inc + +import std.decl_ref { DeclarationRef, WholeDeclaration } +import extdeps.vendor { Vendor } +import extdeps.software { Software } + +import extdeps.external_authority { ExternalAuthority, ExternalModelScope, ExternalSubjectRef } +import extdeps.uri { Uri, Https } + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "en.wikipedia.org/wiki/Docker,_Inc." + } +} + +data extdeps_model_scope: ExternalModelScope = ExternalModelScope { + subject: ExternalSubjectRef { + declaration: DeclarationRef { + module_path: "extdeps.vendor.docker_inc", + decl_name: "docker_inc", + field: WholeDeclaration + } + }, + first_citation: extdeps.vendor.docker_inc.extdeps_external_authority_anchor, + further_citations: [] +} + +data docker_inc: Vendor = Vendor { legal_name: "Docker, Inc." } diff --git a/dag/gunbc/ci_fleet.dag b/dag/gunbc/ci_fleet.dag index 6e232c20bcf..c7e0aea6b7d 100644 --- a/dag/gunbc/ci_fleet.dag +++ b/dag/gunbc/ci_fleet.dag @@ -157,7 +157,7 @@ data gunbc_ci_fleet_offer: ComputeOffer = ComputeOffer { execution: ExecutionSurface { os: gunbc_ci_linux_surface, isolation: PerJobFilesystem, - container_runtime: none, + container_engine: none, toolchains: [], mounted_storage: [], network: [], diff --git a/dag/gunbc/fleet_container.dag b/dag/gunbc/fleet_container.dag index 168a7e55817..20e4bf562f2 100644 --- a/dag/gunbc/fleet_container.dag +++ b/dag/gunbc/fleet_container.dag @@ -1,18 +1,15 @@ module gunbc.fleet_container import gunbc.fleet_intent { - IsolationBoundary, - SharedHostHome, - PerJobFilesystem, - ContainerHermetic, - Vm, - ContainerRuntime, - Docker, - Podman, - Gvisor, - Ubicloud, - GcloudRun, -} + ComputeHost, + ExecutionSurface, + compute_host_primary_cpu, + fleet_intent_execution_surface, + srv1_host, +} +import product.fabric.customer_image { ExecutionTarget } +import extdeps.toolchain.types { Os } +import std.os.types { KernelFamily, Linux, Darwin, WindowsNt, LinuxGuestOnWindows } import product.fabric.envelope { CpuRequirement, GpuRequirement, MemoryRequirement, StorageRequirement, NetworkRequirement, ResourceEnvelope, @@ -198,3 +195,43 @@ fn witness_unreadable_budget_uses_conservative_demand() -> Bool { ) demand_envelope_thread_count(envelope: envelope) == 4 } + + +// WHAT AN IMAGE HAS TO MATCH TO RUN HERE, PROJECTED FROM THE FLEET RATHER THAN RESTATED. +// +// product.fabric.customer_image asks its questions against an ExecutionTarget and never imports +// this fleet, so the agnostic core stays usable by a supplier who is not us. This is the projection +// in the other direction: our hardware and our surface, read, not asserted. +// +// THE ARCHITECTURE IS DERIVED FROM THE HOST'S CPU AND THE FUNCTION REFUSES WITHOUT ONE. Writing +// `Aarch64` here would be a second place the fleet's architecture is stated, and the two would +// diverge the first time a machine with a different CPU joined -- at which point every customer +// image would be checked against an architecture no host has. A host declaring no processor cannot +// answer the question, so it returns no target and every image is refused, rather than being +// checked against a guess. +fn execution_target_os(kernel: KernelFamily) -> Os { + match kernel { + Linux => extdeps.toolchain.types.Linux + LinuxGuestOnWindows => extdeps.toolchain.types.Linux + Darwin => extdeps.toolchain.types.Macos + WindowsNt => extdeps.toolchain.types.Windows + } +} + +fn fleet_execution_target(host: ComputeHost, surface: ExecutionSurface) -> ExecutionTarget? { + match compute_host_primary_cpu(host: host) { + Absent => none + Present { value: cpu } => + Present { + value: ExecutionTarget { + architecture: cpu.catalog.architecture, + os: execution_target_os(kernel: surface.os.kernel), + engine: surface.container_engine, + } + } + } +} + +fn fleet_container_execution_target() -> ExecutionTarget? { + fleet_execution_target(host: srv1_host, surface: fleet_intent_execution_surface()) +} diff --git a/dag/gunbc/fleet_intent.dag b/dag/gunbc/fleet_intent.dag index 13bdad44704..b2339fe1b84 100644 --- a/dag/gunbc/fleet_intent.dag +++ b/dag/gunbc/fleet_intent.dag @@ -11,6 +11,14 @@ import extdeps.storage.types { StorageMedium, } import extdeps.cpu.ampere { altra_max_m12830_catalog } +import extdeps.container.engine { + ContainerEngineDeployed, + ContainerEngineDeployment, + ContainerEngineDeploymentRefused, + RootlessDaemon, + container_engine_deployment, +} +import extdeps.container.docker_engine { docker_engine } import extdeps.cpu.types { CpuFacts, CpuDeploymentFacts } import extdeps.cpu { cpu_facts_threads, cpu_facts_sustained_per_thread_hz } import extdeps.boards.asrock_rack { asrock_altrad8ud_1l2t_catalog } @@ -38,7 +46,23 @@ import std.nat { Nat } import std.float { Float } type IsolationBoundary = SharedHostHome | PerJobFilesystem | ContainerHermetic | Vm -type ContainerRuntime = Docker | Podman | Gvisor | Ubicloud | GcloudRun + +// ContainerRuntime IS GONE. It read +// type ContainerRuntime = Docker | Podman | Gvisor | Ubicloud | GcloudRun +// and it was three concepts in one enum. Docker and Podman are container ENGINES -- independently +// versioned upstream products. gVisor is a SANDBOX whose whole value is the isolation guarantee it +// adds, and what a tenant is promised about isolation is product.fabric.isolation's IsolationProfile, +// which deliberately names no mechanism. Ubicloud and Google Cloud Run are SUPPLIERS: companies that +// rent a machine, whose homes are extdeps.cloud.ubicloud and product.supplier. So adding an engine +// and adding a supplier both widened one enum -- the case DESIGN's external-decomposition section +// rules out -- and no member of it could be added without an edit here. +// +// The engine half is replaced by extdeps.container.engine's ContainerEngineDeployment: a cited +// product row plus the privilege mode this host actually runs it in. FOUR MEMBERS GET NO REPLACEMENT +// ROW AND THAT IS DELETE-FIRST WORKING, NOT A LOSS: Podman, gVisor, Ubicloud and GcloudRun had zero +// constructors anywhere in the corpus, so nothing refused when they went. Podman becomes one new +// file in extdeps whenever a host runs it; gVisor is a guarantee question, not an engine name; the +// two suppliers already have their own authorities and never belonged in a runtime enum. type WorkUnitId = NonEmptyStr where brand("WorkUnitId") @@ -64,7 +88,7 @@ type ProcessorKind type ExecutionSurface { os: OperatingSystemSurface isolation: IsolationBoundary - container_runtime: ContainerRuntime? + container_engine: ContainerEngineDeployment? toolchains: List mounted_storage: List network: List @@ -141,7 +165,7 @@ data host_v1_interpreter_execution_surface: ExecutionSurface = ExecutionSurface process_semantics: PosixProcess, }, isolation: SharedHostHome, - container_runtime: none, + container_engine: none, toolchains: [], mounted_storage: [], network: [], @@ -309,11 +333,28 @@ data srv4_host: ComputeHost = ComputeHost { data fleet_intent_known_hosts: List = [srv1_host, srv2_host, srv3_host, srv4_host] +// WHAT THE FLEET ACTUALLY RUNS, WHICH CARRIES ONE FACT MORE THAN "Docker" DID. +// +// The old surface said `Docker` and stopped. Whether that daemon runs as root is the property that +// decides whether a job that escapes its container owns the machine, and the enum could not say it, +// so the surface was silent on the only security-relevant thing about the engine. srv1 runs the +// rootless daemon. +// +// A mode the product does not support yields no deployment at all rather than a surface asserting +// one, and a target with no engine refuses every image (product.fabric.customer_image's +// TargetHasNoContainerEngine) instead of admitting one it cannot run. +fn fleet_container_engine_deployment() -> ContainerEngineDeployment? { + match container_engine_deployment(engine: docker_engine, privilege_mode: RootlessDaemon) { + ContainerEngineDeployed { deployment: deployment } => Present { value: deployment } + ContainerEngineDeploymentRefused { refusal: _ } => none + } +} + fn fleet_intent_execution_surface() -> ExecutionSurface { ExecutionSurface { os: fleet_intent_os_surface, isolation: PerJobFilesystem, - container_runtime: Present { value: Docker }, + container_engine: fleet_container_engine_deployment(), toolchains: [sccache_toolchain_capability], mounted_storage: [], network: [], diff --git a/dag/product/fabric/customer_image.dag b/dag/product/fabric/customer_image.dag new file mode 100644 index 00000000000..0c2e02ef249 --- /dev/null +++ b/dag/product/fabric/customer_image.dag @@ -0,0 +1,218 @@ +module product.fabric.customer_image + +import extdeps.container.engine { + ContainerEngineDeployment, + container_engine_deployment_label, +} +import extdeps.container.oci.image_config { + ImageConfigAccepted, + ImageConfigRejectReason, + ImageConfigRejected, + ImageConfiguration, + accept_image_configuration, + image_config_layer_count, + image_config_start_command, +} +import extdeps.container.oci.manifest { + ImageManifest, + ManifestAccepted, + ManifestRejectReason, + ManifestRejected, + accept_image_manifest, +} +import extdeps.container.oci.reference { + OciImageReference, + oci_reference_is_digest_pinned, + render_oci_image_reference, +} +import extdeps.toolchain.types { Architecture, Os, architecture_diagnostic_name } +import std.types { Bool, Int, List, String } + +// A CUSTOMER-SUPPLIED CONTAINER IMAGE, AND WHAT IT TAKES TO ADMIT ONE. +// +// The image is the one container-shaped thing a tenant genuinely names: it is the program, and it +// arrives from outside. That makes it a workload INPUT, and the OCI modules in extdeps already say +// what such an input is -- a reference, a manifest and a configuration, each with its own typed +// accept/refuse. Until this module they said it to nobody: every one of them had zero product +// consumers, which is the declared-and-unrouted state that reads as covered and is not. +// +// THE ISOLATION MECHANISM IS NOT IN THIS FILE, AND ITS ABSENCE IS THE POINT. +// +// CustomerSuppliedImage has no field naming a runtime, a sandbox or an isolation boundary, and it +// has no constructor that could carry one. That is structural rather than a convention: a tenant +// cannot select the mechanism because there is nowhere to put the selection. What a tenant IS +// promised is the guarantee set in product.fabric.isolation -- what holds, not what enforces it -- +// and the engine that enforces it is chosen by us and supplied here as part of the TARGET, on the +// other side of the admission function. +// +// TARGET FACTS ARE PASSED IN RATHER THAN IMPORTED FROM THE FLEET. This module must stay usable by +// any supplier: importing gunbc.fleet_intent to read an architecture would make the agnostic core +// depend on one operator's hardware. The fleet projects its own surface into ExecutionTarget. +type ExecutionTarget { + architecture: Architecture + os: Os + engine: ContainerEngineDeployment? +} + +type CustomerSuppliedImage { + reference: OciImageReference + manifest: ImageManifest + configuration: ImageConfiguration +} + +// EVERY REFUSAL NAMES ITS OWN CAUSE, BECAUSE THE REMEDIES ARE UNRELATED. +// +// "Image rejected" is unactionable. An architecture mismatch is fixed by the tenant pushing a +// multi-arch build; a tag reference is fixed by pinning a digest; a layer disagreement means the +// bytes are corrupt or forged and no tenant action helps. Collapsing them to a Bool -- or to one +// String -- would erase the distinction at exactly the boundary that has to explain itself to +// someone outside this repository. +type CustomerImageRefusal + = TargetHasNoContainerEngine + | ReferenceNotDigestPinned { reference_wire: String } + | ManifestRefused { reason: ManifestRejectReason } + | ConfigurationRefused { reason: ImageConfigRejectReason } + | LayerCountDisagreement { manifest_layers: Int, config_diff_ids: Int } + | ArchitectureUnsupported { image: Architecture, target: Architecture } + | OperatingSystemUnsupported { image: Os, target: Os } + | NoStartCommand + +type CustomerImageAdmission + = CustomerImageAdmitted { image: CustomerSuppliedImage, engine: ContainerEngineDeployment } + | CustomerImageRefused { refusal: CustomerImageRefusal } + +// THE CROSS-MODULE INVARIANT NEITHER OCI MODULE CAN CHECK ALONE, AND THE REASON THIS FILE EXISTS. +// +// image-spec requires rootfs.diff_ids to correspond one-for-one with the manifest's layers: the +// manifest lists the compressed blobs to fetch, the configuration lists the uncompressed layer +// identities those blobs unpack to. accept_image_manifest sees only the first list and +// accept_image_configuration only the second, so each accepts a pair that disagrees. A disagreeing +// pair is not a cosmetic defect -- it is a manifest whose layer set does not match the identity the +// config commits to, which is what a substituted layer looks like. +fn customer_image_layers_agree(image: CustomerSuppliedImage) -> Bool { + count(image.manifest.layers) == image_config_layer_count(c: image.configuration) +} + +fn admit_customer_image_platform( + image: CustomerSuppliedImage, + target: ExecutionTarget, + engine: ContainerEngineDeployment, +) -> CustomerImageAdmission { + if image.configuration.architecture != target.architecture { + CustomerImageRefused { + refusal: ArchitectureUnsupported { + image: image.configuration.architecture, + target: target.architecture, + }, + } + } else if image.configuration.os != target.os { + CustomerImageRefused { + refusal: OperatingSystemUnsupported { image: image.configuration.os, target: target.os }, + } + } else if count(image_config_start_command(c: image.configuration)) == 0 { + CustomerImageRefused { refusal: NoStartCommand } + } else { + CustomerImageAdmitted { image: image, engine: engine } + } +} + +fn admit_customer_image_contents( + image: CustomerSuppliedImage, + target: ExecutionTarget, + engine: ContainerEngineDeployment, +) -> CustomerImageAdmission { + match accept_image_manifest(image.manifest) { + ManifestRejected { reason: reason } => + CustomerImageRefused { refusal: ManifestRefused { reason: reason } } + ManifestAccepted { value: _ } => + match accept_image_configuration(image.configuration) { + ImageConfigRejected { reason: reason } => + CustomerImageRefused { refusal: ConfigurationRefused { reason: reason } } + ImageConfigAccepted { value: _ } => + if !(customer_image_layers_agree(image: image)) { + CustomerImageRefused { + refusal: LayerCountDisagreement { + manifest_layers: count(image.manifest.layers), + config_diff_ids: image_config_layer_count(c: image.configuration), + }, + } + } else { + admit_customer_image_platform(image: image, target: target, engine: engine) + } + } + } +} + +// A TAG IS REFUSED HERE AND MODELLED IN EXTDEPS, WHICH IS NOT A CONTRADICTION. +// +// The distribution spec admits tags, so the extdeps reference model carries them: an upstream +// module that could not represent a tag would be modelling our policy instead of the spec. Whether +// we will RUN one is ours to decide, and the answer is no -- a tag resolves to different bytes on +// different days, so admitting one means the thing we audited and the thing we executed are not +// established to be the same program. That is the same posture the fleet already takes on Docker's +// apt signing key and on pinned sccache release digests. +fn admit_customer_image(image: CustomerSuppliedImage, target: ExecutionTarget) -> CustomerImageAdmission { + match target.engine { + Absent => CustomerImageRefused { refusal: TargetHasNoContainerEngine } + Present { value: engine } => + if !(oci_reference_is_digest_pinned(reference: image.reference)) { + CustomerImageRefused { + refusal: ReferenceNotDigestPinned { + reference_wire: render_oci_image_reference(reference: image.reference), + }, + } + } else { + admit_customer_image_contents(image: image, target: target, engine: engine) + } + } +} + +fn customer_image_refusal_wire(refusal: CustomerImageRefusal) -> String { + match refusal { + TargetHasNoContainerEngine => + "target declares no container engine deployment: it cannot run any image" + ReferenceNotDigestPinned { reference_wire: wire } => + concat("image reference is not digest-pinned: ", wire) + ManifestRefused { reason: _ } => "image manifest refused by the OCI manifest authority" + ConfigurationRefused { reason: _ } => + "image configuration refused by the OCI image-config authority" + LayerCountDisagreement { manifest_layers: layers, config_diff_ids: diff_ids } => + concat( + "manifest layer count ", + to_string(layers), + " disagrees with config rootfs.diff_ids count ", + to_string(diff_ids), + ) + ArchitectureUnsupported { image: image_arch, target: target_arch } => + concat( + "image architecture ", + architecture_diagnostic_name(arch: image_arch), + " is not the target architecture ", + architecture_diagnostic_name(arch: target_arch), + ) + OperatingSystemUnsupported { image: _, target: _ } => + "image operating system is not the target operating system" + NoStartCommand => "image configuration carries neither Entrypoint nor Cmd: nothing to run" + } +} + +fn customer_image_admitted(admission: CustomerImageAdmission) -> Bool { + match admission { + CustomerImageAdmitted { image: _, engine: _ } => true + CustomerImageRefused { refusal: _ } => false + } +} + +fn customer_image_admission_wire(admission: CustomerImageAdmission) -> String { + match admission { + CustomerImageAdmitted { image: image, engine: engine } => + concat( + "admitted ", + render_oci_image_reference(reference: image.reference), + " on ", + container_engine_deployment_label(deployment: engine), + ) + CustomerImageRefused { refusal: refusal } => + concat("refused: ", customer_image_refusal_wire(refusal: refusal)) + } +} diff --git a/dag/test/claim/customer_image_admission_witness_test.dag b/dag/test/claim/customer_image_admission_witness_test.dag new file mode 100644 index 00000000000..2d0fbdf5236 --- /dev/null +++ b/dag/test/claim/customer_image_admission_witness_test.dag @@ -0,0 +1,471 @@ +module test.claim.customer_image_admission_witness + +import extdeps.container.engine { + ContainerEngine, + ContainerEngineDeployed, + ContainerEngineDeploymentRefused, + RootfulDaemon, + RootlessDaemon, + container_engine_deployment, +} +import extdeps.container.docker_engine { docker_engine } +import extdeps.vendor.docker_inc { docker_inc } +import extdeps.container.oci.descriptor { OciDescriptor } +import extdeps.container.oci.digest { OciContentDigest, oci_sha256_content_digest } +import extdeps.container.oci.image_config { + ContainerImageConfig, + ImageConfiguration, + ImageRootfs, + RootfsLayers, +} +import extdeps.container.oci.manifest { ImageManifest } +import extdeps.container.oci.media_types { + media_type_oci_image_config_v1, + media_type_oci_image_layer_v1_tar_gzip, + media_type_oci_image_manifest_v1, + oci_image_schema_version, +} +import extdeps.container.oci.reference { + OciImageReference, + OciReferenceIdentifier, + OciRepositoryName, + ReferenceByDigest, + ReferenceByTag, + oci_repository_name, + oci_tag, + render_oci_image_reference, +} +import extdeps.toolchain.types { Aarch64, Architecture, Linux, X86_64 } +import gunbc.fleet_container { fleet_container_execution_target } +import product.fabric.customer_image { + ArchitectureUnsupported, + ConfigurationRefused, + CustomerImageAdmission, + CustomerImageAdmitted, + CustomerImageRefused, + CustomerSuppliedImage, + ExecutionTarget, + LayerCountDisagreement, + ManifestRefused, + NoStartCommand, + ReferenceNotDigestPinned, + TargetHasNoContainerEngine, + admit_customer_image, + customer_image_admitted, +} +import std.error_primitives { Ok, Err } +import std.types { Bool, Int, List, String } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE FIRST EXECUTING CONSUMER OF THE OCI MODEL. +// +// Nine OCI modules typechecked for months with zero product consumers: accept_image_manifest and +// accept_image_configuration were never called by anything that ships. That is the +// specification-without-execution state DESIGN section 5 names, and a join that only typechecked +// would have reproduced it one layer up. Each case below drives the real admission fold and the +// refusal cases are DISCRIMINATING: each one differs from the admitted case in exactly the fact its +// refusal names, so an admission fold that stopped checking would go red here rather than quietly +// widen. + +data fixture_config_hex: String = "1111111111111111111111111111111111111111111111111111111111111111" +data fixture_layer_a_hex: String = "2222222222222222222222222222222222222222222222222222222222222222" +data fixture_layer_b_hex: String = "3333333333333333333333333333333333333333333333333333333333333333" + +type FixtureCase + = WellFormedArm64Image + | TagReferencedImage + | ForeignArchitectureImage + | LayerCountDisagreementImage + | EmptyDiffIdsImage + | EmptyLayersImage + | NoStartCommandImage + +// A DELIBERATELY NARROWER ENGINE THAN ANY REAL PRODUCT ROW, so the refusing arm of +// container_engine_deployment has a reachable red. It is a fixture and is not a claim about any +// vendor's product: the vendor field is filled because ContainerEngine requires one. +fn rootful_only_engine_fixture() -> ContainerEngine { + ContainerEngine { + vendor: docker_inc, + product_name: "rootful-only-fixture-engine", + privilege_modes: [RootfulDaemon], + } +} + +fn fixture_descriptor(digest: OciContentDigest, config: Bool) -> OciDescriptor { + OciDescriptor { + mediaType: if config { media_type_oci_image_config_v1 } else { media_type_oci_image_layer_v1_tar_gzip }, + digest: digest, + size: 1024, + } +} + +fn fixture_manifest(config_digest: OciContentDigest, layers: List) -> ImageManifest { + ImageManifest { + schemaVersion: oci_image_schema_version, + mediaType: media_type_oci_image_manifest_v1, + config: fixture_descriptor(digest: config_digest, config: true), + layers: map(layers, d => fixture_descriptor(digest: d, config: false)), + } +} + +fn fixture_configuration( + architecture: Architecture, + diff_ids: List, + cmd: List, +) -> ImageConfiguration { + ImageConfiguration { + architecture: architecture, + os: Linux, + config: Present { + value: ContainerImageConfig { + User: none, + Env: none, + Entrypoint: none, + Cmd: Present { value: cmd }, + WorkingDir: none, + ExposedPorts: none, + } + }, + rootfs: RootfsLayers { diff_ids: diff_ids }, + } +} + +fn fixture_repository() -> OciRepositoryName? { + match oci_repository_name(raw: "acme/build-image") { + Err { value: _ } => none + Ok { value: name } => Present { value: name } + } +} + +fn fixture_identifier(case: FixtureCase, digest: OciContentDigest) -> OciReferenceIdentifier? { + match case { + TagReferencedImage => + match oci_tag(raw: "latest") { + Err { value: _ } => none + Ok { value: tag } => Present { value: ReferenceByTag(tag) } + } + _ => Present { value: ReferenceByDigest(digest) } + } +} + +fn fixture_architecture(case: FixtureCase) -> Architecture { + match case { + ForeignArchitectureImage => X86_64 + _ => Aarch64 + } +} + +fn fixture_layer_digests(case: FixtureCase, a: OciContentDigest, b: OciContentDigest) -> List { + match case { + EmptyLayersImage => [] + LayerCountDisagreementImage => [a, b] + _ => [a] + } +} + +fn fixture_diff_ids(case: FixtureCase, a: OciContentDigest, b: OciContentDigest) -> List { + match case { + EmptyDiffIdsImage => [] + _ => [a] + } +} + +fn fixture_cmd(case: FixtureCase) -> List { + match case { + NoStartCommandImage => [] + _ => ["/usr/bin/build"] + } +} + +fn fixture_image_from_parts( + case: FixtureCase, + repository: OciRepositoryName, + identifier: OciReferenceIdentifier, + config_digest: OciContentDigest, + a: OciContentDigest, + b: OciContentDigest, +) -> CustomerSuppliedImage { + CustomerSuppliedImage { + reference: OciImageReference { + registry: none, + repository: repository, + identifier: identifier, + }, + manifest: fixture_manifest( + config_digest: config_digest, + layers: fixture_layer_digests(case: case, a: a, b: b), + ), + configuration: fixture_configuration( + architecture: fixture_architecture(case: case), + diff_ids: fixture_diff_ids(case: case, a: a, b: b), + cmd: fixture_cmd(case: case), + ), + } +} + +// Absent means the FIXTURE could not be built, never that admission said nothing. Every witness +// below fails on Absent rather than treating it as a pass, so a broken fixture is a red. +fn fixture_image(case: FixtureCase) -> CustomerSuppliedImage? { + match fixture_repository() { + Absent => none + Present { value: repository } => + match oci_sha256_content_digest(hex: fixture_config_hex) { + Absent => none + Present { value: config_digest } => + match oci_sha256_content_digest(hex: fixture_layer_a_hex) { + Absent => none + Present { value: a } => + match oci_sha256_content_digest(hex: fixture_layer_b_hex) { + Absent => none + Present { value: b } => + match fixture_identifier(case: case, digest: a) { + Absent => none + Present { value: identifier } => + Present { + value: fixture_image_from_parts( + case: case, + repository: repository, + identifier: identifier, + config_digest: config_digest, + a: a, + b: b, + ) + } + } + } + } + } + } +} + +// THE TARGET IS THE REAL FLEET, NOT A FIXTURE TARGET. +// +// srv1's architecture is read from its declared Ampere CPU and its engine from the surface, so the +// foreign-architecture refusal below is a claim about what this fleet would actually do with an +// amd64 image, not about a target authored to make the test pass. +fn fixture_admission(case: FixtureCase) -> CustomerImageAdmission? { + match fleet_container_execution_target() { + Absent => none + Present { value: target } => + match fixture_image(case: case) { + Absent => none + Present { value: image } => + Present { value: admit_customer_image(image: image, target: target) } + } + } +} + +fn admission_is_refused_with(case: FixtureCase, expected: Bool) -> Bool { + match fixture_admission(case: case) { + Absent => false + Present { value: admission } => customer_image_admitted(admission: admission) == expected + } +} + +test fn w_fleet_declares_a_container_execution_target() -> Bool { + match fleet_container_execution_target() { + Absent => false + Present { value: target } => + target.architecture == Aarch64 + && target.os == Linux + && match target.engine { + Absent => false + Present { value: engine } => engine.privilege_mode == RootlessDaemon + } + } +} + +test fn w_well_formed_digest_pinned_arm64_image_is_admitted() -> Bool { + admission_is_refused_with(case: WellFormedArm64Image, expected: true) +} + +test fn w_tag_reference_is_refused_unpinned() -> Bool { + match fixture_admission(case: TagReferencedImage) { + Absent => false + Present { value: admission } => + match admission { + CustomerImageAdmitted { image: _, engine: _ } => false + CustomerImageRefused { refusal: refusal } => + match refusal { + ReferenceNotDigestPinned { reference_wire: wire } => wire == "acme/build-image:latest" + _ => false + } + } + } +} + +test fn w_foreign_architecture_image_is_refused_naming_both_sides() -> Bool { + match fixture_admission(case: ForeignArchitectureImage) { + Absent => false + Present { value: admission } => + match admission { + CustomerImageAdmitted { image: _, engine: _ } => false + CustomerImageRefused { refusal: refusal } => + match refusal { + ArchitectureUnsupported { image: image_arch, target: target_arch } => + image_arch == X86_64 && target_arch == Aarch64 + _ => false + } + } + } +} + +// THE CROSS-MODULE INVARIANT, AND THE ONLY WITNESS HERE THAT NEITHER OCI MODULE COULD CARRY. +// +// Both halves accept in isolation: two layers is a valid manifest and one diff_id is a valid +// rootfs. Only the join sees that they describe different images. +test fn w_layer_count_disagreement_is_refused_with_both_counts() -> Bool { + match fixture_admission(case: LayerCountDisagreementImage) { + Absent => false + Present { value: admission } => + match admission { + CustomerImageAdmitted { image: _, engine: _ } => false + CustomerImageRefused { refusal: refusal } => + match refusal { + LayerCountDisagreement { manifest_layers: layers, config_diff_ids: diff_ids } => + layers == 2 && diff_ids == 1 + _ => false + } + } + } +} + +test fn w_empty_layers_manifest_is_refused_by_the_manifest_authority() -> Bool { + match fixture_admission(case: EmptyLayersImage) { + Absent => false + Present { value: admission } => + match admission { + CustomerImageAdmitted { image: _, engine: _ } => false + CustomerImageRefused { refusal: refusal } => + match refusal { + ManifestRefused { reason: _ } => true + _ => false + } + } + } +} + +test fn w_empty_diff_ids_is_refused_by_the_image_config_authority() -> Bool { + match fixture_admission(case: EmptyDiffIdsImage) { + Absent => false + Present { value: admission } => + match admission { + CustomerImageAdmitted { image: _, engine: _ } => false + CustomerImageRefused { refusal: refusal } => + match refusal { + ConfigurationRefused { reason: _ } => true + _ => false + } + } + } +} + +test fn w_image_with_no_entrypoint_and_no_cmd_is_refused() -> Bool { + match fixture_admission(case: NoStartCommandImage) { + Absent => false + Present { value: admission } => + match admission { + CustomerImageAdmitted { image: _, engine: _ } => false + CustomerImageRefused { refusal: refusal } => + match refusal { + NoStartCommand => true + _ => false + } + } + } +} + +// A TARGET WITH NO ENGINE RUNS NOTHING, AND SAYS SO RATHER THAN ADMITTING. +// +// This is the fail-closed arm of the dissolution: the old surface could carry `Docker` and be +// believed; a deployment that cannot be constructed produces no engine at all, and the admission +// refuses instead of proceeding against a runtime nobody established exists. +test fn w_target_without_an_engine_refuses_every_image() -> Bool { + match fixture_image(case: WellFormedArm64Image) { + Absent => false + Present { value: image } => + match admit_customer_image( + image: image, + target: ExecutionTarget { architecture: Aarch64, os: Linux, engine: none }, + ) { + CustomerImageAdmitted { image: _, engine: _ } => false + CustomerImageRefused { refusal: refusal } => + match refusal { + TargetHasNoContainerEngine => true + _ => false + } + } + } +} + +// THE ENGINE HUB REFUSES A MODE THE PRODUCT DOES NOT DECLARE, WHICH IS WHAT MAKES THE SURFACE'S +// `none` MEAN SOMETHING. Docker Engine declares both modes, so both deploy; the refusing arm is +// exercised against an engine row that declares only one. +test fn w_engine_deployment_refuses_an_undeclared_privilege_mode() -> Bool { + match container_engine_deployment(engine: docker_engine, privilege_mode: RootlessDaemon) { + ContainerEngineDeploymentRefused { refusal: _ } => false + ContainerEngineDeployed { deployment: deployment } => + deployment.privilege_mode == RootlessDaemon + && match container_engine_deployment( + engine: rootful_only_engine_fixture(), + privilege_mode: RootlessDaemon, + ) { + ContainerEngineDeployed { deployment: _ } => false + ContainerEngineDeploymentRefused { refusal: _ } => true + } + } +} + +test fn w_reference_wire_renders_digest_form() -> Bool { + match fixture_image(case: WellFormedArm64Image) { + Absent => false + Present { value: image } => + render_oci_image_reference(reference: image.reference) + == concat("acme/build-image@sha256:", fixture_layer_a_hex) + } +} + + +// THE REFERENCE GRAMMAR REFUSES WHAT THE DISTRIBUTION SPEC DOES NOT ADMIT. +// +// The separator alternatives are the discriminating part: "a__b" and "a-b" and "a.b" are names and +// "a..b", "a___b" and a leading or trailing separator are not, so a predicate that merely allowed +// the character class would go red on the second half of this witness. +test fn w_repository_path_component_grammar_discriminates() -> Bool { + fixture_repository_accepts(raw: "acme/build-image") + && fixture_repository_accepts(raw: "a__b") + && fixture_repository_accepts(raw: "a.b") + && fixture_repository_accepts(raw: "a---b/c") + && !fixture_repository_accepts(raw: "a..b") + && !fixture_repository_accepts(raw: "a___b") + && !fixture_repository_accepts(raw: "-abc") + && !fixture_repository_accepts(raw: "abc-") + && !fixture_repository_accepts(raw: "Abc") + && !fixture_repository_accepts(raw: "") +} + +fn fixture_repository_accepts(raw: String) -> Bool { + match oci_repository_name(raw: raw) { + Err { value: _ } => false + Ok { value: _ } => true + } +} + +fn fixture_tag_accepts(raw: String) -> Bool { + match oci_tag(raw: raw) { + Err { value: _ } => false + Ok { value: _ } => true + } +} + +test fn w_tag_grammar_discriminates_leading_character_and_length() -> Bool { + fixture_tag_accepts(raw: "latest") + && fixture_tag_accepts(raw: "v1.2.3-rc1") + && fixture_tag_accepts(raw: "_underscore") + && !fixture_tag_accepts(raw: ".leading-dot") + && !fixture_tag_accepts(raw: "-leading-hyphen") + && !fixture_tag_accepts(raw: "has/slash") + && !fixture_tag_accepts(raw: "") +} From 0a8b8a4a4cfd0be07fbbd127f5b79bface2464c9 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 27 Aug 2026 02:07:40 +0000 Subject: [PATCH 2/5] wip: join(...) instead of variadic concat; prose citations --- dag/extdeps/container/engine.dag | 13 +++--- dag/extdeps/container/oci/reference.dag | 8 ++-- .../plans/realization_measurement_loop.dag | 2 +- dag/gunbc/runner_host_deploy.dag | 2 +- dag/product/fabric/customer_image.dag | 43 +++++++++++-------- .../customer_image_admission_witness_test.dag | 2 +- 6 files changed, 41 insertions(+), 29 deletions(-) diff --git a/dag/extdeps/container/engine.dag b/dag/extdeps/container/engine.dag index c474af2fe0a..066bc3c7b18 100644 --- a/dag/extdeps/container/engine.dag +++ b/dag/extdeps/container/engine.dag @@ -90,10 +90,13 @@ fn container_engine_deployment( } fn container_engine_deployment_label(deployment: ContainerEngineDeployment) -> String { - concat( - deployment.engine.product_name as String, - " (", - engine_privilege_mode_label(mode: deployment.privilege_mode), - ")", + join( + [ + deployment.engine.product_name as String, + " (", + engine_privilege_mode_label(mode: deployment.privilege_mode), + ")", + ], + "", ) } diff --git a/dag/extdeps/container/oci/reference.dag b/dag/extdeps/container/oci/reference.dag index 70b1cea5fc6..dea960f1ebb 100644 --- a/dag/extdeps/container/oci/reference.dag +++ b/dag/extdeps/container/oci/reference.dag @@ -239,7 +239,7 @@ fn oci_registry_wire(registry: OciRegistry) -> String { match registry.port { Absent => domain_name_wire(name: registry.host.name) Present { value: port } => - concat(domain_name_wire(name: registry.host.name), ":", to_string(port)) + join([domain_name_wire(name: registry.host.name), ":", to_string(port)], "") } } @@ -250,11 +250,11 @@ fn render_oci_image_reference(reference: OciImageReference) -> String { let named = match reference.registry { Absent => oci_repository_name_wire(name: reference.repository) Present { value: registry } => - concat(oci_registry_wire(registry: registry), "/", oci_repository_name_wire(name: reference.repository)) + join([oci_registry_wire(registry: registry), "/", oci_repository_name_wire(name: reference.repository)], "") } match reference.identifier { - ReferenceByDigest(digest) => concat(named, "@", render_oci_content_digest_wire(d: digest)) - ReferenceByTag(tag) => concat(named, ":", tag as String) + ReferenceByDigest(digest) => join([named, "@", render_oci_content_digest_wire(d: digest)], "") + ReferenceByTag(tag) => join([named, ":", tag as String], "") } } diff --git a/dag/gunbc/plans/realization_measurement_loop.dag b/dag/gunbc/plans/realization_measurement_loop.dag index 08674aa3e13..8c15684ef54 100644 --- a/dag/gunbc/plans/realization_measurement_loop.dag +++ b/dag/gunbc/plans/realization_measurement_loop.dag @@ -116,7 +116,7 @@ fn realization_measurement_loop_body() -> List { ]), hr(), h2(text: "Phase 3 — Infra / deployment onto `.dag` (srv1 / srv2) · the second ask"), - p(text: "**Goal:** model the actual infra/deployment — runner config, access, host config — as **data**, dissolving bespoke `ci.yml` shell + manual runner setup. **\"Get CI onto `.dag`\" = instantiate the fabric for srv1/srv2:** `gunbc.ci_fleet` `ComputeOffer` models self-hosted offers; `gunbc.fleet_intent` `ContainerRuntime` enumerates cloud realizations. This meets note 1 at the placement carrier — the offer the runner *declares* is the budget Phase 1's scheduler *consumes*."), + p(text: "**Goal:** model the actual infra/deployment — runner config, access, host config — as **data**, dissolving bespoke `ci.yml` shell + manual runner setup. **\"Get CI onto `.dag`\" = instantiate the fabric for srv1/srv2:** `gunbc.ci_fleet` `ComputeOffer` models self-hosted offers; `extdeps.container.engine` models the container engine a surface deploys, and cloud suppliers are their own authorities (`extdeps.cloud.ubicloud`, `product.supplier`). This meets note 1 at the placement carrier — the offer the runner *declares* is the budget Phase 1's scheduler *consumes*."), p(text: "**§3 boundary — THREE tiers, not two (refined after the #5177 review).** The operator's rule: keep the *generic* \"CI runner\" cleanly apart from *our* CI runner; CI does not need to know our fleet. So:"), ul(items: [ li(text: "**3a-generic — \"CI runner\" in the abstract (any project).** What we expect *any* CI runner to do, project-agnostic: **a workflow triggered by an event** (`trigger → workflow`), realized per platform. The GHA realization already exists — `extdeps.github.actions` `Workflow`, `WorkflowTrigger`, and `RunnerSpec`. The **generic `offer → RunnerSpec` projection** (`gunbc.runner_spec_from_offer` `runner_spec_from_offer`, kernel/arch → labels) belongs HERE, next to `RunnerSpec` in the generalized layer — it works for *any* fleet offer. **This tier MUST NOT import a concrete SKU (`extdeps.cpu.ampere`) or name srv1/srv2.** (GitLab/Buildkite/etc. would be sibling platform handlers — one generic interface, N realizations, §2/§4.)"), diff --git a/dag/gunbc/runner_host_deploy.dag b/dag/gunbc/runner_host_deploy.dag index 5116d676bd2..8e6cb4dfdb8 100644 --- a/dag/gunbc/runner_host_deploy.dag +++ b/dag/gunbc/runner_host_deploy.dag @@ -125,7 +125,7 @@ data fleet_runner_host_deploys: List = [ // runner_host_installer_command_argv — install-actions-runner.sh has no slot-count parameter // (per-host handler only). Width realization lives in gunbc.runner_slot_provision. -data runner_host_prereq_note: String = "Execution-surface prereqs the runner host must satisfy (gunbc.fleet_intent.fleet_intent_execution_surface now declares container_runtime: Docker + toolchains: [sccache], so the surface no longer lies). These two scripts provision that surface on a fresh host BEFORE install-actions-runner.sh: docker_ce (the rootless-docker apt prereq the ctrl installer assumes) then sccache (the pinned binary install-ctrl-sccache.sh assumes on PATH). Each cites its upstream; the shell leaves carry dissolution triggers in their extdeps modules." +data runner_host_prereq_note: String = "Execution-surface prereqs the runner host must satisfy (gunbc.fleet_intent fleet_intent_execution_surface declares container_engine: the cited Docker Engine row deployed rootless (extdeps.container.docker_engine, extdeps.container.engine) + toolchains: [sccache], so the surface no longer lies). These two scripts provision that surface on a fresh host BEFORE install-actions-runner.sh: docker_ce (the rootless-docker apt prereq the ctrl installer assumes) then sccache (the pinned binary install-ctrl-sccache.sh assumes on PATH). Each cites its upstream; the shell leaves carry dissolution triggers in their extdeps modules." fn runner_host_docker_provision_script() -> String { docker_ce_repo_install_script(repo: docker_ce_apt_repo_noble_arm64, packages: docker_ce_packages) diff --git a/dag/product/fabric/customer_image.dag b/dag/product/fabric/customer_image.dag index 0c2e02ef249..6ab385d2e59 100644 --- a/dag/product/fabric/customer_image.dag +++ b/dag/product/fabric/customer_image.dag @@ -172,23 +172,29 @@ fn customer_image_refusal_wire(refusal: CustomerImageRefusal) -> String { TargetHasNoContainerEngine => "target declares no container engine deployment: it cannot run any image" ReferenceNotDigestPinned { reference_wire: wire } => - concat("image reference is not digest-pinned: ", wire) + join(["image reference is not digest-pinned: ", wire], "") ManifestRefused { reason: _ } => "image manifest refused by the OCI manifest authority" ConfigurationRefused { reason: _ } => "image configuration refused by the OCI image-config authority" LayerCountDisagreement { manifest_layers: layers, config_diff_ids: diff_ids } => - concat( - "manifest layer count ", - to_string(layers), - " disagrees with config rootfs.diff_ids count ", - to_string(diff_ids), + join( + [ + "manifest layer count ", + to_string(layers), + " disagrees with config rootfs.diff_ids count ", + to_string(diff_ids), + ], + "", ) ArchitectureUnsupported { image: image_arch, target: target_arch } => - concat( - "image architecture ", - architecture_diagnostic_name(arch: image_arch), - " is not the target architecture ", - architecture_diagnostic_name(arch: target_arch), + join( + [ + "image architecture ", + architecture_diagnostic_name(arch: image_arch) as String, + " is not the target architecture ", + architecture_diagnostic_name(arch: target_arch) as String, + ], + "", ) OperatingSystemUnsupported { image: _, target: _ } => "image operating system is not the target operating system" @@ -206,13 +212,16 @@ fn customer_image_admitted(admission: CustomerImageAdmission) -> Bool { fn customer_image_admission_wire(admission: CustomerImageAdmission) -> String { match admission { CustomerImageAdmitted { image: image, engine: engine } => - concat( - "admitted ", - render_oci_image_reference(reference: image.reference), - " on ", - container_engine_deployment_label(deployment: engine), + join( + [ + "admitted ", + render_oci_image_reference(reference: image.reference), + " on ", + container_engine_deployment_label(deployment: engine), + ], + "", ) CustomerImageRefused { refusal: refusal } => - concat("refused: ", customer_image_refusal_wire(refusal: refusal)) + join(["refused: ", customer_image_refusal_wire(refusal: refusal)], "") } } diff --git a/dag/test/claim/customer_image_admission_witness_test.dag b/dag/test/claim/customer_image_admission_witness_test.dag index 2d0fbdf5236..90df54db715 100644 --- a/dag/test/claim/customer_image_admission_witness_test.dag +++ b/dag/test/claim/customer_image_admission_witness_test.dag @@ -423,7 +423,7 @@ test fn w_reference_wire_renders_digest_form() -> Bool { Absent => false Present { value: image } => render_oci_image_reference(reference: image.reference) - == concat("acme/build-image@sha256:", fixture_layer_a_hex) + == join(["acme/build-image@sha256:", fixture_layer_a_hex], "") } } From 7e28ffb58d02bbb59dc8bb28c3595e7f209e3b07 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 27 Aug 2026 02:33:11 +0000 Subject: [PATCH 3/5] wip: remove unauthorable KernelFamily/Os bridge; OS is a stated parameter --- dag/gunbc/fleet_container.dag | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/dag/gunbc/fleet_container.dag b/dag/gunbc/fleet_container.dag index 20e4bf562f2..ad2f7f733ae 100644 --- a/dag/gunbc/fleet_container.dag +++ b/dag/gunbc/fleet_container.dag @@ -8,13 +8,11 @@ import gunbc.fleet_intent { srv1_host, } import product.fabric.customer_image { ExecutionTarget } -import extdeps.toolchain.types { Os } -import std.os.types { KernelFamily, Linux, Darwin, WindowsNt, LinuxGuestOnWindows } import product.fabric.envelope { CpuRequirement, GpuRequirement, MemoryRequirement, StorageRequirement, NetworkRequirement, ResourceEnvelope, } -import extdeps.toolchain.types { Architecture } +import extdeps.toolchain.types { Architecture, Linux, Os } import extdeps.gpu.types { GpuRuntime } import extdeps.storage.types { PersistenceKind } import product.network_topology { NetworkEgressClass } @@ -201,7 +199,7 @@ fn witness_unreadable_budget_uses_conservative_demand() -> Bool { // // product.fabric.customer_image asks its questions against an ExecutionTarget and never imports // this fleet, so the agnostic core stays usable by a supplier who is not us. This is the projection -// in the other direction: our hardware and our surface, read, not asserted. +// in the other direction: our hardware, read rather than asserted. // // THE ARCHITECTURE IS DERIVED FROM THE HOST'S CPU AND THE FUNCTION REFUSES WITHOUT ONE. Writing // `Aarch64` here would be a second place the fleet's architecture is stated, and the two would @@ -209,23 +207,23 @@ fn witness_unreadable_budget_uses_conservative_demand() -> Bool { // image would be checked against an architecture no host has. A host declaring no processor cannot // answer the question, so it returns no target and every image is refused, rather than being // checked against a guess. -fn execution_target_os(kernel: KernelFamily) -> Os { - match kernel { - Linux => extdeps.toolchain.types.Linux - LinuxGuestOnWindows => extdeps.toolchain.types.Linux - Darwin => extdeps.toolchain.types.Macos - WindowsNt => extdeps.toolchain.types.Windows - } -} - -fn fleet_execution_target(host: ComputeHost, surface: ExecutionSurface) -> ExecutionTarget? { +// +// THE OPERATING SYSTEM IS A PARAMETER AND NOT DERIVED, AND THE REASON IS A MEASURED COMPILER +// REFUSAL RATHER THAN A PREFERENCE. An image configuration's `os` is extdeps.toolchain.types `Os`; +// a ComputeHost's surface carries std.os.types `KernelFamily`. Those are two authorities for one +// concept -- the section 3 fork -- and the substrate says so: a module importing both is refused +// with `variant 'Linux' appears in both 'Os' and 'KernelFamily'`, so the bridging match cannot be +// written anywhere. Dissolving that fork is a real change and it is NOT this one; what is done here +// is to refuse to hide it. The caller states the target OS in the vocabulary the image speaks, the +// mismatch still refuses loudly, and no silent widening is introduced by the gap. +fn fleet_execution_target(host: ComputeHost, surface: ExecutionSurface, os: Os) -> ExecutionTarget? { match compute_host_primary_cpu(host: host) { Absent => none Present { value: cpu } => Present { value: ExecutionTarget { architecture: cpu.catalog.architecture, - os: execution_target_os(kernel: surface.os.kernel), + os: os, engine: surface.container_engine, } } @@ -233,5 +231,9 @@ fn fleet_execution_target(host: ComputeHost, surface: ExecutionSurface) -> Execu } fn fleet_container_execution_target() -> ExecutionTarget? { - fleet_execution_target(host: srv1_host, surface: fleet_intent_execution_surface()) + fleet_execution_target( + host: srv1_host, + surface: fleet_intent_execution_surface(), + os: Linux, + ) } From 7274bd1a5a89afa86f470cb568fcb979a29e6f7c Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 27 Aug 2026 02:55:20 +0000 Subject: [PATCH 4/5] fix: image_config optional arms bound the Optional, not its payload --- dag/extdeps/container/oci/image_config.dag | 46 +++++++++++++--------- 1 file changed, 27 insertions(+), 19 deletions(-) diff --git a/dag/extdeps/container/oci/image_config.dag b/dag/extdeps/container/oci/image_config.dag index ad46ced7091..0b70d0e1379 100644 --- a/dag/extdeps/container/oci/image_config.dag +++ b/dag/extdeps/container/oci/image_config.dag @@ -57,24 +57,32 @@ fn image_config_layer_count(c: ImageConfiguration) -> Int { } } +// THE BARE-BINDING ARM DID NOT UNWRAP, AND NOTHING NOTICED BECAUSE NOTHING RAN. +// +// This read `match c.config { null => [] ; cfg => match cfg.Entrypoint { ... } }`. The bare arm +// binds the OPTIONAL, not its payload, so the inner field read refused at runtime with +// `NoSuchField { type_name: "Optional", field: "Entrypoint" }`. It typechecked and had witnesses, +// and the defect surfaced the first time a consumer actually called it -- which is precisely the +// specification-without-execution failure DESIGN section 5 names, found the way that section says +// it is found. Present/Absent binds the payload. fn image_config_entrypoint(c: ImageConfiguration) -> List { match c.config { - null => [] - cfg => + Absent => [] + Present { value: cfg } => match cfg.Entrypoint { - null => [] - ep => ep + Absent => [] + Present { value: entrypoint } => entrypoint } } } fn image_config_cmd(c: ImageConfiguration) -> List { match c.config { - null => [] - cfg => + Absent => [] + Present { value: cfg } => match cfg.Cmd { - null => [] - cmd => cmd + Absent => [] + Present { value: cmd } => cmd } } } @@ -90,17 +98,16 @@ fn image_config_start_command(c: ImageConfiguration) -> List { append(image_config_entrypoint(c: c), items: image_config_cmd(c: c)) } +// Same defect as image_config_entrypoint above, repaired together rather than left for the next +// consumer to rediscover: it is one class in one file, and fixing only the arm this change happens +// to call would leave a known-broken sibling behind. fn image_config_first_exposed_port(c: ImageConfiguration) -> ContainerExposedPort? { match c.config { - null => null - cfg => + Absent => none + Present { value: cfg } => match cfg.ExposedPorts { - null => null - ports => - match ports |> get(0) { - null => null - port => port - } + Absent => none + Present { value: ports } => ports |> get(0) } } } @@ -114,8 +121,9 @@ fn image_config_has_exposed_port( expected_port: Int, protocol: ContainerPortProtocol, ) -> Bool { - match image_config_first_exposed_port(c) { - null => false - port => container_exposed_port_is(port: port, expected_port: expected_port, protocol: protocol) + match image_config_first_exposed_port(c: c) { + Absent => false + Present { value: port } => + container_exposed_port_is(port: port, expected_port: expected_port, protocol: protocol) } } From 2a77a19f2ac084203e8d8caaf4807a5af45bdee2 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 27 Aug 2026 03:19:23 +0000 Subject: [PATCH 5/5] record the discriminating-red procedure in the witness module --- .../customer_image_admission_witness_test.dag | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/dag/test/claim/customer_image_admission_witness_test.dag b/dag/test/claim/customer_image_admission_witness_test.dag index 90df54db715..0fa6cd48779 100644 --- a/dag/test/claim/customer_image_admission_witness_test.dag +++ b/dag/test/claim/customer_image_admission_witness_test.dag @@ -59,6 +59,24 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly +// HOW TO CHECK THAT THESE ROWS DISCRIMINATE, STATED AS A PROCEDURE RATHER THAN AS A TRANSCRIBED +// RESULT, so a later reader re-derives it instead of trusting a number that has since rotted. +// +// Run this module through `claim_batch --claim-run`, then delete ONE check in +// product.fabric.customer_image and run it again. Each of these three deletions must turn exactly +// ONE row red and leave every other row green: +// +// customer_image_layers_agree returning true unconditionally +// -> only w_layer_count_disagreement_is_refused_with_both_counts +// admit_customer_image skipping the digest-pin test +// -> only w_tag_reference_is_refused_unpinned +// admit_customer_image_platform skipping the architecture comparison +// -> only w_foreign_architecture_image_is_refused_naming_both_sides +// +// A deletion that turns NOTHING red means the row is agreeing with the fold's shape rather than +// testing its decision; a deletion that turns SEVERAL red means the rows are not independent and +// one defect would be reported three times. Both are failures of this file, not of the fold. + // THE FIRST EXECUTING CONSUMER OF THE OCI MODEL. // // Nine OCI modules typechecked for months with zero product consumers: accept_image_manifest and