Isolation and the resource envelope become fabric guarantees an offer can fail — and the work identity stops dropping the axes the matcher compares

dag/gunbc/doc_graph_roots.dag

@@ -1003,7 +1003,7 @@ data hand_authored_doc_bind_incomings: List<HandAuthoredDocBind> = [
   HandAuthoredDocBind {
     home: PlanDoc,
     slug: "space-lens-minimal-project",
-    primary_work: DeclarationRef { module_path: "gunbc.fleet_container", decl_name: "ResourceEnvelope", field: WholeDeclaration },
+    primary_work: DeclarationRef { module_path: "product.fabric.envelope", decl_name: "ResourceEnvelope", field: WholeDeclaration },
     additional_works: [
       DeclarationRef { module_path: "std.realization_schedule", decl_name: "cost_account_predicted_zero", field: WholeDeclaration },
       DeclarationRef { module_path: "gunbc.ci_input_envelope", decl_name: "InputEnvelope", field: WholeDeclaration },

dag/gunbc/fabric_witness_run.dag

@@ -4,6 +4,8 @@ import std.types { NonEmptyStr }
 import std.currency { CurrencyCode, Usd }
 import std.nat { Nat }
 import std.measure { HardwareThreadCount, hardware_thread_count, MoneyAmountMicro, Second, second }
+import product.fabric.isolation { IsolationProfile }
+import product.fabric.envelope { unstated_envelope }
 import product.fabric.identity {
   FabricIdentity, WorkKey, ExecutionAttemptKey, OfferKey, GrantKey,
   fabric_identity_eq,
@@ -160,11 +162,40 @@ fn floor_work_contract(source: SourceManifestRef) -> WorkContract {
 // modeled, and minting the carrier early buys nothing except a row that lies
 // about being load-bearing.
 
+// WHAT A FLOOR RUN REQUIRES OF ITS EXECUTOR, AND WHY THAT IS HONESTLY NOTHING.
+//
+// A floor run is OUR OWN work on OUR OWN fleet, and it demonstrably runs today on slots that
+// provide none of the isolation guarantees -- a reused writable root by design, the host's process
+// namespace, and /home/ghrunner shared across every slot. Declaring a requirement the floor does
+// not actually have would be inventing a gap: the run would be modeled as ineligible for the
+// executor it has been green on for months, and the first person to trust the model would go
+// looking for a break that is not there.
+//
+// SO THE EMPTY PROFILE HERE IS A MEASUREMENT, NOT A PLACEHOLDER. It says the floor asks for no
+// tenancy guarantee, which is true and is exactly why the floor was safe to run this way. The gap
+// this model exists to express belongs to CUSTOMER work, where the tenant is not us -- see
+// product.fabric.isolation tenant_workload_isolation_requirement and the witness that measures
+// today's slots against it.
+//
+// CONSUMPTION STATUS, STATED PLAINLY BECAUSE THIS MODULE'S OWN HEADER INSISTS ON IT: the fold that
+// reads this (floor_offer_fungibility -> offer_fungibility_for) has NO production consumer, exactly
+// as its siblings ShapeNotCovered and CapabilitiesNotOffered do not. This is the modeled decision
+// the broker will consume, not a live wall, and calling it enforcement would be the rung inflation
+// the paragraph above already records for affordability. NEXT-RUNG TRIGGER is the same one: a
+// broker fold that selects an Offer for this Demand.
+fn floor_isolation_requirement() -> IsolationProfile {
+  IsolationProfile { guarantees: [] }
+}
+
 fn floor_execution_requirements() -> ExecutionRequirements {
   ExecutionRequirements {
-    shape: Shape { hard: HardRequirements { threads: hardware_thread_count(count: 8) } },
+    shape: Shape {
+      hard: HardRequirements { threads: hardware_thread_count(count: 8) },
+      envelope: unstated_envelope(),
+    },
     capabilities: "gunbc.capabilities.linux-rust-toolchain",
     trust_domain: "gunbc.trust.internal-fleet",
+    isolation: floor_isolation_requirement(),
   }
 }
 

dag/gunbc/fleet_container.dag

@@ -13,6 +13,10 @@ import gunbc.fleet_intent {
   Ubicloud,
   GcloudRun,
 }
+import product.fabric.envelope {
+  CpuRequirement, GpuRequirement, MemoryRequirement, StorageRequirement, NetworkRequirement,
+  ResourceEnvelope,
+}
 import extdeps.toolchain.types { Architecture }
 import extdeps.gpu.types { GpuRuntime }
 import extdeps.storage.types { PersistenceKind }
@@ -30,19 +34,11 @@ import std.measure {
 }
 import std.realization_width { bounded_host_spawn_width, memory_aware_spawn_width }
 
-type CpuRequirement { min_threads: HardwareThreadCount, architecture: Architecture? }
-type GpuRequirement { min_vram: ByteSize, runtimes: List<GpuRuntime> }
-type MemoryRequirement { min_bytes: ByteSize }
-type StorageRequirement { min_bytes: ByteSize, persistence: PersistenceKind }
-type NetworkRequirement { egress: NetworkEgressClass?, ambient_allowed: Bool }
-
-type ResourceEnvelope {
-  cpu: CpuRequirement?
-  gpu: GpuRequirement?
-  memory: MemoryRequirement?
-  storage: StorageRequirement?
-  network: NetworkRequirement?
-}
+// THE REQUIREMENT VOCABULARY MOVED TO product.fabric.envelope AND IS CONSUMED HERE.
+//
+// These are machine questions, not container questions -- a bare-metal host and a rented VM answer
+// them identically -- so owning them inside a model of our fleet's containers put a general fact in
+// a specific home. Consumed, not redeclared (DESIGN section 3).
 
 type ContainerBaseline
   = ContainerBaselineMeasured { idle: ResourceEnvelope }

dag/product/fabric/envelope.dag

@@ -0,0 +1,75 @@
+module product.fabric.envelope
+
+import std.types { List, Bool }
+import std.measure { ByteSize, HardwareThreadCount }
+import extdeps.toolchain.types { Architecture }
+import extdeps.gpu.types { GpuRuntime }
+import extdeps.storage.types { PersistenceKind }
+import product.network_topology { NetworkEgressClass }
+
+// WHAT A UNIT OF WORK NEEDS FROM A MACHINE, AS GENERAL VOCABULARY RATHER THAN CONTAINER VOCABULARY.
+//
+// These five requirement types and the envelope over them were authored inside
+// gunbc.fleet_container, which is a model of OUR fleet's containers. They are not container facts:
+// a bare-metal host, a rented cloud VM and a microVM all answer the same questions about threads,
+// memory, storage and egress, and a fabric that brokers any of those needs the vocabulary without
+// depending on our container model. DESIGN section 3's rule is that a fact's home is its LAYER, so
+// the move is the single-authority action -- gunbc.fleet_container now consumes these rather than
+// owning them, and no second envelope was minted beside the first.
+//
+// THE ROWS ARE MOVED VERBATIM, NOT RE-DERIVED. Every field, optionality and cited type is exactly
+// what fleet_container carried; this relocation changes the home and nothing else, so a reader
+// comparing against git history should find the definitions byte-identical.
+data fabric_envelope_note: String = "General resource-requirement vocabulary for brokered compute. Moved verbatim from gunbc.fleet_container, which now consumes it: the questions are machine questions, not container questions."
+
+type CpuRequirement { min_threads: HardwareThreadCount, architecture: Architecture? }
+
+type GpuRequirement { min_vram: ByteSize, runtimes: List<GpuRuntime> }
+
+type MemoryRequirement { min_bytes: ByteSize }
+
+type StorageRequirement { min_bytes: ByteSize, persistence: PersistenceKind }
+
+type NetworkRequirement { egress: NetworkEgressClass?, ambient_allowed: Bool }
+
+// EVERY AXIS IS OPTIONAL, AND THE OPTIONALITY MEANS UNSTATED RATHER THAN UNCONSTRAINED.
+//
+// An absent axis is a requirement nobody expressed, not a requirement satisfied by everything.
+// The distinction decides who may answer: a fold matching an offer against an envelope may skip an
+// unstated axis, but it must never report an unstated axis as CHECKED -- that is the conflation
+// where absence of observation becomes positive clearance, and it is the same error
+// gunbc.runner_slot_allocation records for an unmeasured disk width.
+type ResourceEnvelope {
+  cpu: CpuRequirement?
+  gpu: GpuRequirement?
+  memory: MemoryRequirement?
+  storage: StorageRequirement?
+  network: NetworkRequirement?
+}
+
+// THE ALL-UNSTATED ENVELOPE, NAMED SO CALLERS DO NOT HAND-WRITE FIVE ABSENCES.
+//
+// Named "unstated" rather than "empty" or "any", because those two words claim different things
+// and only one of them is true: this states NO requirement on any axis, which a matching fold must
+// treat as nothing-to-check, never as satisfied-by-everything. A constructor called any_envelope
+// would invite the second reading at every call site.
+fn unstated_envelope() -> ResourceEnvelope {
+  ResourceEnvelope { cpu: none, gpu: none, memory: none, storage: none, network: none }
+}
+
+// THE TWO AXES FUNGIBILITY ACTUALLY COMPARES, FOR CALLERS THAT STATE A REAL REQUIREMENT.
+fn cpu_memory_envelope(
+  min_threads: HardwareThreadCount,
+  architecture: Architecture?,
+  min_bytes: ByteSize,
+) -> ResourceEnvelope {
+  ResourceEnvelope {
+    cpu: Present {
+      value: CpuRequirement { min_threads: min_threads, architecture: architecture },
+    },
+    gpu: none,
+    memory: Present { value: MemoryRequirement { min_bytes: min_bytes } },
+    storage: none,
+    network: none,
+  }
+}

dag/product/fabric/isolation.dag

@@ -0,0 +1,166 @@
+module product.fabric.isolation
+
+import std.types { String, NonEmptyStr, Bool, List }
+
+// WHAT A TENANT IS PROMISED ABOUT WHO ELSE CAN SEE ITS RUN.
+//
+// This is the fabric CORE's half of isolation, and the split is the point: the core states the
+// guarantees a unit of work REQUIRES and an offer PROVIDES, while the mechanism that delivers them
+// -- an OCI container, systemd-nspawn, a microVM, a dedicated host -- is a realization handler.
+// Work and Grant never learn whether the executor used Podman or a VM, exactly as DESIGN section 3
+// puts transport outside the interface: a core that named containers could not admit a supplier
+// who satisfies the same guarantees another way, and the guarantee is what the tenant is owed.
+//
+// EXCLUSIVITY IS NOT IN THIS FILE, AND CONFLATING THE TWO IS THE EXPENSIVE MISTAKE. Isolation
+// answers "what can this run observe once it starts"; ALLOCATION EXCLUSIVITY answers "may two
+// grants reserve the same cell at all", and that is a property of the durable grant store, not of
+// a sandbox. A container provides no exclusivity whatsoever: two brokers can each start one on the
+// same cell. Treating the sandbox as the exclusion wall is how a fabric double-books hardware
+// while every individual run looks correctly isolated.
+data fabric_isolation_note: String = "Core isolation vocabulary: what work requires and an offer provides. The delivering mechanism (container, nspawn, microVM) is a realization handler and is deliberately unnamed here. Allocation exclusivity is a separate guarantee owned by the grant store, not by isolation."
+
+// THE GUARANTEES, AS A CLOSED SET OF NAMED AXES RATHER THAN A BAG OF BOOLEANS.
+//
+// Each is something a tenant can be told and an offer can be held to. They are separate members
+// rather than one "isolated: Bool" because they fail independently and are satisfied by different
+// mechanisms: a shared-kernel container gives fresh filesystem and private namespaces but cannot
+// give DedicatedKernel, and an offer that conflates them would answer yes to a question it cannot
+// keep.
+//
+// DedicatedKernel is the tenancy boundary and the reason this is a coproduct rather than a
+// severity scale. Containers isolate much and share the kernel; for arbitrary customer code that
+// distinction is the whole risk model, and it must be expressible as a REQUIREMENT that an
+// otherwise-capable offer fails to meet.
+type IsolationGuarantee
+  = FreshWritableRoot
+  | PrivateProcessNamespace
+  | PrivateNetworkNamespace
+  | PrivateUserNamespace
+  | AttemptScopedSecrets
+  | DefaultDenyEgress
+  | DedicatedKernel
+
+fn isolation_guarantee_label(g: IsolationGuarantee) -> String {
+  match g {
+    FreshWritableRoot => "fresh-writable-root"
+    PrivateProcessNamespace => "private-process-namespace"
+    PrivateNetworkNamespace => "private-network-namespace"
+    PrivateUserNamespace => "private-user-namespace"
+    AttemptScopedSecrets => "attempt-scoped-secrets"
+    DefaultDenyEgress => "default-deny-egress"
+    DedicatedKernel => "dedicated-kernel"
+  }
+}
+
+// ONE TYPE FOR BOTH SIDES, BECAUSE REQUIRED AND PROVIDED ARE THE SAME KIND OF FACT.
+//
+// A separate OfferIsolationCapability record would be a second spelling of one concept, and the
+// comparison below would then have to translate between them -- the nicknaming violation DESIGN
+// section 3 names, arriving as symmetry.
+type IsolationProfile {
+  guarantees: List<IsolationGuarantee>
+}
+
+fn isolation_profile_contains(profile: IsolationProfile, wanted: IsolationGuarantee) -> Bool {
+  any(profile.guarantees, g => g == wanted)
+}
+
+// THE MATCH RETURNS THE MISSING GUARANTEES, NOT A BOOLEAN.
+//
+// "This offer is not isolated enough" is unactionable; "this offer cannot provide DedicatedKernel"
+// tells a broker exactly which supplier class to look for and tells an operator exactly what to
+// provision. A Bool here would be the typed-cause-erased-at-the-consumer failure: both a
+// shared-kernel host and a host with no network namespacing would answer false, and their remedies
+// are unrelated.
+//
+// The empty list means satisfied, and that is safe HERE because the list is derived by filtering
+// the REQUIRED set -- an empty result means every required guarantee was found, never that the
+// question could not be asked. A caller that built the required set from an unreadable source
+// would owe its own refusal upstream; this fold cannot manufacture one it was not given.
+fn unsatisfied_isolation_guarantees(
+  required: IsolationProfile,
+  provided: IsolationProfile,
+) -> List<IsolationGuarantee> {
+  filter(required.guarantees, g => !isolation_profile_contains(profile: provided, wanted: g))
+}
+
+fn isolation_profile_satisfies(required: IsolationProfile, provided: IsolationProfile) -> Bool {
+  (unsatisfied_isolation_guarantees(required: required, provided: provided) |> count) == 0
+}
+
+fn unsatisfied_isolation_wire(missing: List<IsolationGuarantee>) -> String {
+  join(map(missing, g => isolation_guarantee_label(g: g)), ", ")
+}
+
+// THE PROFILE A SHARED-KERNEL SANDBOX CAN HONESTLY OFFER.
+//
+// Named for what it IS rather than for a mechanism, so a handler using nspawn rather than OCI can
+// claim the same profile without the name lying. DedicatedKernel is absent by construction, which
+// is the whole content of the row: it is the guarantee this class cannot make, and an offer that
+// listed it would be claiming a wall it does not have.
+fn shared_kernel_sandbox_profile() -> IsolationProfile {
+  IsolationProfile {
+    guarantees: [
+      FreshWritableRoot,
+      PrivateProcessNamespace,
+      PrivateNetworkNamespace,
+      PrivateUserNamespace,
+      AttemptScopedSecrets,
+      DefaultDenyEgress,
+    ],
+  }
+}
+
+fn dedicated_kernel_sandbox_profile() -> IsolationProfile {
+  IsolationProfile {
+    guarantees: [
+      FreshWritableRoot,
+      PrivateProcessNamespace,
+      PrivateNetworkNamespace,
+      PrivateUserNamespace,
+      AttemptScopedSecrets,
+      DefaultDenyEgress,
+      DedicatedKernel,
+    ],
+  }
+}
+
+// WHAT THE FLEET'S RUNNER SLOTS PROVIDE TODAY, WHICH IS MEASURABLY LESS THAN THE SANDBOX PROFILE.
+//
+// A slot is a systemd unit with cgroup ceilings, not a sandbox. It gets per-slot memory and CPU
+// entitlement, and it gets a per-slot _work checkout -- but the writable root is REUSED across
+// attempts by design (the persistent checkout that avoids re-cloning), the process namespace is
+// the host's, and /home/ghrunner is one directory shared by every slot on the machine.
+//
+// So this profile is EMPTY, and that is a measurement rather than a pessimistic default. The
+// shared home is not hypothetical: it has produced two independent mid-run file deletions
+// (rust-cache cleanup, then rustup-init rewriting shims under a running job), and the second
+// appeared after the first was fixed precisely because nothing in the model forbade a third.
+// Writing the empty profile is what lets an offer built on today's slots FAIL a requirement it
+// cannot meet, instead of silently passing one nobody stated.
+fn current_runner_slot_profile() -> IsolationProfile {
+  IsolationProfile { guarantees: [] }
+}
+
+// WHAT ARBITRARY CUSTOMER WORK REQUIRES, WHICH IS WHERE THE REAL GAP LIVES.
+//
+// Our own floor run requires nothing here and says so -- it has run for months on slots providing
+// none of these, and inventing a requirement it does not have would model it as ineligible for the
+// executor it is demonstrably green on. The requirement belongs to work whose TENANT IS NOT US:
+// once someone else's code runs on our hardware, a reused writable root and a shared home stop
+// being an efficiency choice and become a disclosure between tenants.
+//
+// DedicatedKernel is deliberately NOT required here. It is the guarantee for untrusted or
+// hostile-by-assumption code, and requiring it of every customer workload would refuse every
+// container-based supplier including our own fleet's future one. Keeping it a separate axis is
+// what lets a stricter tenancy class ask for it later without re-cutting this profile.
+fn tenant_workload_isolation_requirement() -> IsolationProfile {
+  IsolationProfile {
+    guarantees: [
+      FreshWritableRoot,
+      PrivateProcessNamespace,
+      PrivateUserNamespace,
+      AttemptScopedSecrets,
+    ],
+  }
+}