diff --git a/dag/gunbc/doc_graph_roots.dag b/dag/gunbc/doc_graph_roots.dag index b958e8022ce..a794febef1e 100644 --- a/dag/gunbc/doc_graph_roots.dag +++ b/dag/gunbc/doc_graph_roots.dag @@ -1003,7 +1003,7 @@ data hand_authored_doc_bind_incomings: List = [ 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 }, diff --git a/dag/gunbc/fabric_witness_run.dag b/dag/gunbc/fabric_witness_run.dag index 1bd203f31e3..dd319ff697d 100644 --- a/dag/gunbc/fabric_witness_run.dag +++ b/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(), } } diff --git a/dag/gunbc/fleet_container.dag b/dag/gunbc/fleet_container.dag index ff688b940d8..168a7e55817 100644 --- a/dag/gunbc/fleet_container.dag +++ b/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 } -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 } diff --git a/dag/product/fabric/envelope.dag b/dag/product/fabric/envelope.dag new file mode 100644 index 00000000000..1ce4a775456 --- /dev/null +++ b/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 } + +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, + } +} diff --git a/dag/product/fabric/isolation.dag b/dag/product/fabric/isolation.dag new file mode 100644 index 00000000000..7bcc878750e --- /dev/null +++ b/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 +} + +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 { + 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) -> 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, + ], + } +} diff --git a/dag/product/fabric/supply.dag b/dag/product/fabric/supply.dag index 52271a802e7..9521f7287c3 100644 --- a/dag/product/fabric/supply.dag +++ b/dag/product/fabric/supply.dag @@ -1,7 +1,9 @@ module product.fabric.supply -import std.types { Timestamp, Int } +import std.types { Timestamp, Int, List } import std.measure { + ByteSize, + byte_size_count, MoneyAmountMicro, MoneyPerSecond, MoneyPerHour, MoneyOnce, HardwareThreadCount, hardware_thread_count_value, money_amount_micro_count, Second, second_count, minutes_per_hour, seconds_per_minute, measure_scale_fraction_ceil, @@ -10,6 +12,12 @@ import std.currency { CurrencyCode } import product.fabric.identity { FabricIdentity, OfferKey } import product.fabric.demand { ObservationReceiptRef } import product.fabric.work { Shape, CapabilityManifestRef, TrustDomainRef, ExecutionRequirements } +import extdeps.toolchain.types { Architecture, architecture_diagnostic_name } +import product.fabric.envelope { ResourceEnvelope } +import product.fabric.isolation { + IsolationProfile, IsolationGuarantee, + unsatisfied_isolation_guarantees, unsatisfied_isolation_wire, +} // An Offer is a supplier's statement of capacity it is willing to sell. Owned // capacity and rented capacity are ONE type: what differs is the evidence behind @@ -92,6 +100,7 @@ type Offer

{ shape: Shape capabilities: CapabilityManifestRef trust_domain: TrustDomainRef + isolation: IsolationProfile quantity_bound: Int ready_at: Timestamp quote: OfferQuote @@ -166,9 +175,19 @@ type SelectionPolicy = type OfferFungibility = Fungible - | ShapeNotCovered { required_threads: HardwareThreadCount, offered_threads: HardwareThreadCount } | TrustDomainMismatch { required: TrustDomainRef, offered: TrustDomainRef } | CapabilitiesNotOffered { required: CapabilityManifestRef, offered: CapabilityManifestRef } + | IsolationNotProvided { missing: List } + | ShapeAxesNotCovered { unmet: List } + +// ShapeNotCovered IS DELETED RATHER THAN KEPT BESIDE ITS REPLACEMENT. +// +// It carried exactly one axis -- required and offered thread counts -- which ShapeAxesNotCovered +// now carries as ThreadsNotCovered alongside the axes it could not express. Nothing constructs it +// any more, so keeping it would leave a variant every consumer must match and no producer can +// ever emit: a permanently-unreachable arm that reads as coverage. DESIGN section 4b(4) is +// explicit that a climb deletes the redundant lower-rung machinery it obsoletes rather than +// accumulating it beside the replacement. // GRANT DURATION -- the fact a RATE quote needs before its per-unit price can // be compared to a per-grant ceiling AT ALL. "I cannot compare a $/hr rate to @@ -206,7 +225,106 @@ type DemandOfferAffordability | QuoteCurrencyMismatch { quoted: CurrencyCode, budgeted: CurrencyCode } fn offer_covers_shape(offered: Shape, needed: Shape) -> Bool { - hardware_thread_count_value(t: offered.hard.threads) >= hardware_thread_count_value(t: needed.hard.threads) + (unmet_shape_axes(offered: offered, needed: needed) |> count) == 0 +} + +// THREADS WERE THE ONLY AXIS COMPARED, SO FUNGIBILITY RETURNED WRONG ANSWERS. +// +// An 8 GiB x64 workload was declared fungible with a 6 GiB arm offer whenever thread counts and the +// textual capability ref matched. The broker would route work to a machine that cannot run it, and +// nothing downstream refuses because fungibility already said yes. +// +// EACH UNMET AXIS IS NAMED, FOR THE REASON THE ISOLATION MATCH GIVES: "does not fit" is +// unactionable, while "needs 8589934592 bytes, offered 6442450944" tells a broker which supplier +// class to look for. An axis the WORK does not state is skipped and is not reported as checked -- +// unstated is not satisfied-by-everything, and rendering it as covered would turn absence of a +// requirement into a positive clearance. +// +// ARCHITECTURE IS EQUALITY, NOT ORDER. There is no sense in which x86_64 "covers" aarch64: a +// binary built for one does not run on the other, so the comparison is a match and a mismatch is +// total. Threads and memory are genuine at-least comparisons. +type UnmetShapeAxis + = ThreadsNotCovered { required: HardwareThreadCount, offered: HardwareThreadCount } + | MemoryNotCovered { required: ByteSize, offered: ByteSize } + | MemoryNotOffered { required: ByteSize } + | ArchitectureMismatch { required: Architecture, offered: Architecture } + | ArchitectureNotOffered { required: Architecture } + +fn unmet_shape_axis_wire(axis: UnmetShapeAxis) -> String { + match axis { + ThreadsNotCovered { required: r, offered: o } => + join(["threads: needs ", to_string(hardware_thread_count_value(t: r)), + ", offered ", to_string(hardware_thread_count_value(t: o))], "") + MemoryNotCovered { required: r, offered: o } => + join(["memory: needs ", to_string(byte_size_count(b: r)), + " bytes, offered ", to_string(byte_size_count(b: o))], "") + MemoryNotOffered { required: r } => + join(["memory: needs ", to_string(byte_size_count(b: r)), + " bytes, offer states none"], "") + ArchitectureMismatch { required: r, offered: o } => + join(["architecture: needs ", architecture_diagnostic_name(arch: r) as String, + ", offered ", architecture_diagnostic_name(arch: o) as String], "") + ArchitectureNotOffered { required: r } => + join(["architecture: needs ", architecture_diagnostic_name(arch: r) as String, + ", offer states none"], "") + } +} + +fn unmet_thread_axis(offered: Shape, needed: Shape) -> List { + if hardware_thread_count_value(t: offered.hard.threads) + >= hardware_thread_count_value(t: needed.hard.threads) { + [] + } else { + [ThreadsNotCovered { required: needed.hard.threads, offered: offered.hard.threads }] + } +} + +fn unmet_memory_axis(offered: Shape, needed: Shape) -> List { + match needed.envelope.memory { + Absent => [] + Present { value: want } => + match offered.envelope.memory { + Absent => [MemoryNotOffered { required: want.min_bytes }] + Present { value: have } => + if byte_size_count(b: have.min_bytes) >= byte_size_count(b: want.min_bytes) { + [] + } else { + [MemoryNotCovered { required: want.min_bytes, offered: have.min_bytes }] + } + } + } +} + +fn unmet_architecture_axis(offered: Shape, needed: Shape) -> List { + match needed.envelope.cpu { + Absent => [] + Present { value: want_cpu } => + match want_cpu.architecture { + Absent => [] + Present { value: want } => + match offered.envelope.cpu { + Absent => [ArchitectureNotOffered { required: want }] + Present { value: have_cpu } => + match have_cpu.architecture { + Absent => [ArchitectureNotOffered { required: want }] + Present { value: have } => + if have == want { [] } else { + [ArchitectureMismatch { required: want, offered: have }] + } + } + } + } + } +} + +fn unmet_shape_axes(offered: Shape, needed: Shape) -> List { + concat( + unmet_thread_axis(offered: offered, needed: needed), + concat( + unmet_memory_axis(offered: offered, needed: needed), + unmet_architecture_axis(offered: offered, needed: needed), + ), + ) } // THIS FOLD SCREENS FUNGIBILITY. IT DOES NOT SELECT, AND IT TAKES NO MONEY. @@ -217,15 +335,19 @@ fn offer_covers_shape(offered: Shape, needed: Shape) -> Bool { // never here. fn offer_fungibility_for

(requirements: ExecutionRequirements, offer: Offer

) -> OfferFungibility { + let missing_isolation = unsatisfied_isolation_guarantees( + required: requirements.isolation, + provided: offer.isolation, + ) + let unmet_axes = unmet_shape_axes(offered: offer.shape, needed: requirements.shape) if requirements.trust_domain != offer.trust_domain { TrustDomainMismatch { required: requirements.trust_domain, offered: offer.trust_domain } } else if requirements.capabilities != offer.capabilities { CapabilitiesNotOffered { required: requirements.capabilities, offered: offer.capabilities } - } else if !offer_covers_shape(offered: offer.shape, needed: requirements.shape) { - ShapeNotCovered { - required_threads: requirements.shape.hard.threads, - offered_threads: offer.shape.hard.threads, - } + } else if (missing_isolation |> count) > 0 { + IsolationNotProvided { missing: missing_isolation } + } else if (unmet_axes |> count) > 0 { + ShapeAxesNotCovered { unmet: unmet_axes } } else { Fungible } diff --git a/dag/product/fabric/work.dag b/dag/product/fabric/work.dag index 160aafc087a..2b643283b6a 100644 --- a/dag/product/fabric/work.dag +++ b/dag/product/fabric/work.dag @@ -1,8 +1,14 @@ module product.fabric.work +import product.fabric.isolation { IsolationProfile, isolation_guarantee_label } +import extdeps.toolchain.types { architecture_diagnostic_name } +import product.fabric.envelope { + ResourceEnvelope, CpuRequirement, MemoryRequirement, +} + import std.types { NonEmptyStr, List } import std.content_hash { ContentHash, content_hash_of_value, serialize_content_hash } -import std.measure { HardwareThreadCount, hardware_thread_count_value } +import std.measure { HardwareThreadCount, hardware_thread_count_value, byte_size_count } import product.fabric.identity { FabricIdentity, WorkKey } // Work is WHAT is computed, and it is provider-neutral by construction: no field @@ -108,12 +114,28 @@ type TrustDomainRef = NonEmptyStr where brand("TrustDomainRef") type HardRequirements { threads: HardwareThreadCount } -type Shape { hard: HardRequirements } +// A SHAPE CARRIED ONLY A THREAD COUNT, AND THAT MADE FUNGIBILITY GIVE WRONG ANSWERS. +// +// Until this field existed, offer_covers_shape compared threads and nothing else, so an 8 GiB x64 +// workload was declared FUNGIBLE with a 6 GiB arm offer whenever the thread counts and the textual +// capability ref happened to match. That is a wrong answer, not a missing annotation: the broker +// would route the work to a machine that cannot run it, and no downstream refusal would fire +// because fungibility had already said yes. Reported from the first production supplier binding +// (neat-heron-312, product.supplier.ubicloud), where memory and disk surfaced as +// UnexpressedSupplyFact -- honest diagnosis that could not repair the decision, because a sidecar +// saying "memory was dropped" cannot route work. +// +// THE ENVELOPE IS CONSUMED, NOT RESTATED. product.fabric.envelope owns the requirement vocabulary +// (moved there from gunbc.fleet_container, which now consumes it too), so threads keep their own +// cited home in HardRequirements while every other axis arrives through the one envelope authority +// rather than growing this record an axis at a time. +type Shape { hard: HardRequirements, envelope: ResourceEnvelope } type ExecutionRequirements { shape: Shape capabilities: CapabilityManifestRef trust_domain: TrustDomainRef + isolation: IsolationProfile } type Work

{ @@ -149,10 +171,31 @@ fn work_identity_material(contract: WorkContract, requirements: ExecutionRequire contract.output_contract, "\u{1f}", requirements.capabilities, "\u{1f}", requirements.trust_domain, "\u{1f}", + isolation_material(profile: requirements.isolation), "\u{1f}", shape_material(shape: requirements.shape) ) } +// ISOLATION IS A SEMANTIC INPUT, AND OMITTING IT WAS THE SAME DIVERGENCE THE SHAPE NOTE BELOW +// DESCRIBES -- COMMITTED BY ME, ONE FIELD LATER. +// +// The isolation profile landed on ExecutionRequirements without landing here, so two works +// differing ONLY in what they require of their executor -- one needing a fresh writable root and +// attempt-scoped secrets, one needing nothing -- derived the SAME key and deduplicated onto each +// other. Fungibility in product.fabric.supply compares isolation, so identity and matching would +// have disagreed about whether two things were the same work: exactly the failure the shape note +// records, reproduced by the next author to add a field. +// +// The guarantees are rendered in the order the profile carries them rather than sorted, which is a +// LIMITATION and not a design: two profiles listing the same guarantees in different orders derive +// different keys. That is safe in the conservative direction -- it over-distinguishes rather than +// collapsing two different requirements onto one identity -- and the constructors in +// product.fabric.isolation all emit a fixed order, so no production caller can currently reach it. +// Sorting wants a total order on the coproduct, which is a separate carrier. +fn isolation_material(profile: IsolationProfile) -> NonEmptyStr { + concat("isolation:", join(map(profile.guarantees, g => isolation_guarantee_label(g: g)), ",")) +} + // The shape feeds the digest, and leaving it out was a real divergence rather // than an omission of a decorative field. Two works needing different thread // counts would have derived the SAME key while carrying different shapes -- @@ -168,7 +211,67 @@ fn work_identity_material(contract: WorkContract, requirements: ExecutionRequire fn shape_material(shape: Shape) -> NonEmptyStr { concat( "threads:", - to_string(hardware_thread_count_value(t: shape.hard.threads)) + to_string(hardware_thread_count_value(t: shape.hard.threads)), + "\u{1f}", + envelope_material(envelope: shape.envelope) + ) +} + +// THE ARCHITECTURE TOKEN USES architecture_diagnostic_name, AND THAT NEEDS A WORD BECAUSE THAT +// FUNCTION'S OWN ANNOTATION SAYS IT IS DELIBERATELY NOT A WIRE LABEL. +// +// Its objection is to publishing that name OUTWARD -- every upstream spells architectures +// differently, and each of those projections refuses the arches its upstream does not publish, so +// reusing one internal name as a wire label would re-coin those authorities and defeat their +// fail-closed arms. A work-key material is not published to any upstream: it is an internal +// discriminator hashed into an identity, and what it needs is totality and injectivity, both of +// which that function has. No upstream projection is bypassed because no upstream ever sees it. +// +// THE ENVELOPE AXES FEED THE DIGEST, EACH RENDERED AS PRESENT-WITH-VALUE OR EXPLICITLY ABSENT. +// +// An unstated axis renders as a distinct token rather than as an empty string, because "no memory +// requirement" and "a memory requirement of zero" are different works and an empty rendering would +// collapse them. Only the axes fungibility actually compares are rendered; adding an axis to the +// comparison without adding it here would re-open the identity/matching divergence, which is the +// obligation the note above records and which no mechanism currently enforces. +fn envelope_axis_material(label: NonEmptyStr, value: NonEmptyStr?) -> NonEmptyStr { + match value { + Present { value: v } => concat(label, ":", v) + Absent => concat(label, ":unstated") + } +} + +fn envelope_material(envelope: ResourceEnvelope) -> NonEmptyStr { + concat( + envelope_axis_material( + label: "min-threads", + value: match envelope.cpu { + Present { value: c } => + Present { value: to_string(hardware_thread_count_value(t: c.min_threads)) as NonEmptyStr } + Absent => none + }, + ), + "\u{1f}", + envelope_axis_material( + label: "architecture", + value: match envelope.cpu { + Present { value: c } => + match c.architecture { + Present { value: a } => Present { value: architecture_diagnostic_name(arch: a) } + Absent => none + } + Absent => none + }, + ), + "\u{1f}", + envelope_axis_material( + label: "min-memory", + value: match envelope.memory { + Present { value: m } => + Present { value: to_string(byte_size_count(b: m.min_bytes)) as NonEmptyStr } + Absent => none + }, + ) ) } diff --git a/dag/test/claim/fabric_envelope_witness_test.dag b/dag/test/claim/fabric_envelope_witness_test.dag new file mode 100644 index 00000000000..2204d7c5003 --- /dev/null +++ b/dag/test/claim/fabric_envelope_witness_test.dag @@ -0,0 +1,129 @@ +module test.claim.fabric_envelope_witness_test + +import std.types { Bool, String, List, NonEmptyStr, Int } +import extdeps.toolchain.types { Architecture } +import std.measure { byte_size, hardware_thread_count } +import extdeps.toolchain.types { X86_64, Aarch64 } +import product.fabric.envelope { unstated_envelope, cpu_memory_envelope } +import product.fabric.work { + Shape, HardRequirements, ExecutionRequirements, shape_material, +} +import product.fabric.supply { + unmet_shape_axes, unmet_shape_axis_wire, offer_covers_shape, + MemoryNotCovered, ArchitectureMismatch, ThreadsNotCovered, + MemoryNotOffered, ArchitectureNotOffered, +} + +fn shape_of(threads: Int, arch: Architecture?, bytes: Int) -> Shape { + Shape { + hard: HardRequirements { threads: hardware_thread_count(count: threads) }, + envelope: cpu_memory_envelope( + min_threads: hardware_thread_count(count: threads), + architecture: arch, + min_bytes: byte_size(bytes), + ), + } +} + +fn eight_gib() -> Int { 8589934592 } +fn six_gib() -> Int { 6442450944 } + +// THE REPORTED WRONG ANSWER, EXECUTED. +// +// An 8 GiB x64 workload was declared FUNGIBLE with a 6 GiB arm offer whenever thread counts and +// the textual capability ref matched, because offer_covers_shape compared threads and nothing +// else. That is a routing decision, not a missing annotation: the broker sends work to a machine +// that cannot run it and nothing downstream refuses, because fungibility already said yes. +// +// The assertion names BOTH failing axes rather than merely that it refuses -- a fold that caught +// only memory would pass a "does it refuse" check while still routing arm work to an x64 request. +test fn an_eight_gib_x64_need_is_not_covered_by_a_six_gib_arm_offer() -> Bool { + let needed = shape_of(threads: 2, arch: Present { value: X86_64 }, bytes: eight_gib()) + let offered = shape_of(threads: 2, arch: Present { value: Aarch64 }, bytes: six_gib()) + let unmet = unmet_shape_axes(offered: offered, needed: needed) + !offer_covers_shape(offered: offered, needed: needed) + && (unmet |> count) == 2 + && any(unmet, a => match a { + MemoryNotCovered { required: _, offered: _ } => true + ThreadsNotCovered { required: _, offered: _ } => false + ArchitectureMismatch { required: _, offered: _ } => false + MemoryNotOffered { required: _ } => false + ArchitectureNotOffered { required: _ } => false + }) + && any(unmet, a => match a { + ArchitectureMismatch { required: _, offered: _ } => true + ThreadsNotCovered { required: _, offered: _ } => false + MemoryNotCovered { required: _, offered: _ } => false + MemoryNotOffered { required: _ } => false + ArchitectureNotOffered { required: _ } => false + }) +} + +// THE POSITIVE CONTROL: A BIGGER, MATCHING-ARCH OFFER STILL COVERS. +// Without it the witness above would pass against a fold that refuses everything. +test fn a_larger_same_arch_offer_still_covers() -> Bool { + let needed = shape_of(threads: 2, arch: Present { value: X86_64 }, bytes: six_gib()) + let offered = shape_of(threads: 8, arch: Present { value: X86_64 }, bytes: eight_gib()) + offer_covers_shape(offered: offered, needed: needed) + && (unmet_shape_axes(offered: offered, needed: needed) |> count) == 0 +} + +// ARCHITECTURE IS EQUALITY, NOT ORDER, AND THE ASYMMETRY PROVES IT. +// +// A bigger arm machine does not "cover" an x64 need in the way more memory covers less memory: a +// binary built for one does not run on the other. If architecture were folded into an at-least +// comparison this witness goes green in one direction and the model silently starts routing across +// ABIs. +test fn a_larger_arm_offer_does_not_cover_an_x64_need() -> Bool { + let needed = shape_of(threads: 2, arch: Present { value: X86_64 }, bytes: six_gib()) + let offered = shape_of(threads: 64, arch: Present { value: Aarch64 }, bytes: eight_gib()) + !offer_covers_shape(offered: offered, needed: needed) +} + +// AN UNSTATED AXIS IS SKIPPED, NOT REPORTED AS CHECKED. +// +// Work that states no memory requirement must not be refused by an offer that states none either, +// and must not be recorded as having had memory verified. Unstated is nothing-to-check; treating +// it as satisfied-by-everything is the same conflation, one step further along. +test fn an_unstated_requirement_neither_refuses_nor_claims_a_check() -> Bool { + let needed = Shape { + hard: HardRequirements { threads: hardware_thread_count(count: 2) }, + envelope: unstated_envelope(), + } + let offered = Shape { + hard: HardRequirements { threads: hardware_thread_count(count: 2) }, + envelope: unstated_envelope(), + } + offer_covers_shape(offered: offered, needed: needed) + && (unmet_shape_axes(offered: offered, needed: needed) |> count) == 0 +} + +// THE ENVELOPE REACHES THE WORK IDENTITY, WHICH IS THE HALF A FUNGIBILITY FIX ALONE WOULD MISS. +// +// shape_material hand-renders fields, so a new axis is included only if someone remembers. Two +// works differing ONLY in memory must not derive the same key: fungibility compares the envelope, +// so if identity ignored it, deduplication and matching would disagree about whether two things +// are the same work -- exactly the divergence that module's own note records for threads. +test fn two_shapes_differing_only_in_memory_do_not_share_material() -> Bool { + let small = shape_of(threads: 2, arch: Present { value: X86_64 }, bytes: six_gib()) + let large = shape_of(threads: 2, arch: Present { value: X86_64 }, bytes: eight_gib()) + shape_material(shape: small) != shape_material(shape: large) +} + +test fn two_shapes_differing_only_in_architecture_do_not_share_material() -> Bool { + let x64 = shape_of(threads: 2, arch: Present { value: X86_64 }, bytes: six_gib()) + let arm = shape_of(threads: 2, arch: Present { value: Aarch64 }, bytes: six_gib()) + shape_material(shape: x64) != shape_material(shape: arm) +} + +// AN UNSTATED AXIS AND A STATED-ZERO AXIS ARE DIFFERENT WORKS. +// The material renders absence as its own token rather than as an empty string, so the two cannot +// collapse onto one identity. +test fn unstated_and_stated_do_not_collapse_in_the_material() -> Bool { + let unstated = Shape { + hard: HardRequirements { threads: hardware_thread_count(count: 2) }, + envelope: unstated_envelope(), + } + let stated = shape_of(threads: 2, arch: none, bytes: 0) + shape_material(shape: unstated) != shape_material(shape: stated) +} diff --git a/dag/test/claim/fabric_isolation_witness_test.dag b/dag/test/claim/fabric_isolation_witness_test.dag new file mode 100644 index 00000000000..9a413c31b61 --- /dev/null +++ b/dag/test/claim/fabric_isolation_witness_test.dag @@ -0,0 +1,106 @@ +module test.claim.fabric_isolation_witness_test + +import std.types { Bool, String, List } +import product.fabric.isolation { + IsolationProfile, IsolationGuarantee, + FreshWritableRoot, PrivateProcessNamespace, PrivateNetworkNamespace, + PrivateUserNamespace, AttemptScopedSecrets, DefaultDenyEgress, DedicatedKernel, + isolation_guarantee_label, isolation_profile_satisfies, + unsatisfied_isolation_guarantees, unsatisfied_isolation_wire, + shared_kernel_sandbox_profile, dedicated_kernel_sandbox_profile, + current_runner_slot_profile, tenant_workload_isolation_requirement, +} +import gunbc.fabric_witness_run { floor_isolation_requirement } + +// A SHARED-KERNEL SANDBOX CANNOT SATISFY A DEDICATED-KERNEL REQUIREMENT, AND THE REFUSAL NAMES +// EXACTLY THAT ONE GUARANTEE. +// +// This is the discriminating control for the whole model. A Bool-returning match would answer +// "no" here and "no" for a host with no network namespacing at all, and those have unrelated +// remedies -- find a microVM supplier, versus fix this host. The assertion is that the missing +// list is exactly [DedicatedKernel], not merely non-empty. +test fn a_shared_kernel_offer_fails_only_the_dedicated_kernel_guarantee() -> Bool { + let missing = unsatisfied_isolation_guarantees( + required: dedicated_kernel_sandbox_profile(), + provided: shared_kernel_sandbox_profile(), + ) + (missing |> count) == 1 + && unsatisfied_isolation_wire(missing: missing) == "dedicated-kernel" +} + +// THE SAME OFFER SATISFIES EVERYTHING A SHARED-KERNEL TENANT ASKS FOR. +// The positive control: without it the witness above would pass against a match that refuses +// everything. +test fn a_shared_kernel_offer_satisfies_a_shared_kernel_requirement() -> Bool { + isolation_profile_satisfies( + required: shared_kernel_sandbox_profile(), + provided: shared_kernel_sandbox_profile(), + ) + && !isolation_profile_satisfies( + required: dedicated_kernel_sandbox_profile(), + provided: shared_kernel_sandbox_profile(), + ) +} + +// TODAY'S RUNNER SLOTS COULD NOT HOST A TENANT, AND THIS COUNTS THE GAP RATHER THAN ASSERTING IT. +// +// A slot reuses its writable root by design -- the persistent checkout that avoids re-cloning ~10G +// -- runs in the host's process namespace, and shares /home/ghrunner with every other slot on the +// machine, which has already produced two independent mid-run file deletions under running jobs. +// So all four tenant guarantees are missing, and the witness asserts the COUNT so that providing +// one of them turns it red: the correct trigger to revisit the profile, rather than a green that +// survives partial progress. +// +// THE FLOOR IS DELIBERATELY NOT THE SUBJECT HERE. Our own work requires none of these and runs +// green today; measuring the fleet against the floor's requirement would report a gap that does +// not exist. The tenant requirement is the one the fleet genuinely cannot meet. +test fn todays_slots_could_not_host_a_tenant_workload() -> Bool { + let missing = unsatisfied_isolation_guarantees( + required: tenant_workload_isolation_requirement(), + provided: current_runner_slot_profile(), + ) + (missing |> count) == 4 + && !isolation_profile_satisfies( + required: tenant_workload_isolation_requirement(), + provided: current_runner_slot_profile(), + ) +} + +// AND THE FLEET IS STILL ELIGIBLE FOR OUR OWN FLOOR, WHICH IS THE CONTROL THAT KEEPS THE ABOVE +// FROM BEING A UNIVERSAL "NOTHING IS ELIGIBLE". Without it, a match that refused every pairing +// would satisfy the gap witness and look like a working model. +test fn todays_slots_still_satisfy_our_own_floor() -> Bool { + isolation_profile_satisfies( + required: floor_isolation_requirement(), + provided: current_runner_slot_profile(), + ) +} + +// EVERY GUARANTEE HAS ITS OWN WIRE WORD. +// +// The discriminating half: a label function that collapsed two members would still render a +// plausible refusal, and the collapse would only surface as an operator provisioning the wrong +// thing. Asserted as distinctness across the whole closed set rather than by spot-checking one. +test fn the_seven_guarantees_do_not_share_a_wire_word() -> Bool { + let all = [ + FreshWritableRoot, PrivateProcessNamespace, PrivateNetworkNamespace, + PrivateUserNamespace, AttemptScopedSecrets, DefaultDenyEgress, DedicatedKernel, + ] + let labels = map(all, g => isolation_guarantee_label(g: g)) + (all |> count) == 7 + && (labels |> count) == 7 + && !any(labels, a => (filter(labels, b => b == a) |> count) > 1) +} + +// AN EMPTY REQUIREMENT IS SATISFIED BY AN EMPTY OFFER, WHICH IS NOT VACUOUS BUT LOAD-BEARING. +// +// It states that the empty missing-list means SATISFIED and never "could not ask". The fold +// derives its answer by filtering the REQUIRED set, so an empty result can only mean every +// required guarantee was found -- if it could also mean the question failed, every unsatisfiable +// offer in the fleet would read as fungible. +test fn requiring_nothing_is_satisfied_rather_than_unanswerable() -> Bool { + isolation_profile_satisfies( + required: IsolationProfile { guarantees: [] }, + provided: current_runner_slot_profile(), + ) +} diff --git a/dag/test/claim/fabric_terminal_contract_witness_test.dag b/dag/test/claim/fabric_terminal_contract_witness_test.dag index fc68b21e365..542d32e5f58 100644 --- a/dag/test/claim/fabric_terminal_contract_witness_test.dag +++ b/dag/test/claim/fabric_terminal_contract_witness_test.dag @@ -24,12 +24,16 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // assertion is that the Work identity they produce is IDENTICAL while the // demands remain distinct. If a provider fact ever leaks into Work, this // witness reds without anyone needing to notice the leak. -data fixture_shape: Shape = Shape { hard: HardRequirements { threads: hardware_thread_count(8) } } +data fixture_shape: Shape = Shape { + hard: HardRequirements { threads: hardware_thread_count(8) }, + envelope: unstated_envelope(), +} data fixture_requirements: ExecutionRequirements = ExecutionRequirements { shape: fixture_shape, capabilities: "linux-arm64", trust_domain: "fleet-owned", + isolation: shared_kernel_sandbox_profile(), } data fixture_contract: WorkContract = WorkContract { @@ -76,15 +80,20 @@ data other_source_contract: WorkContract = WorkContract { // matching constraints disagreed about whether two things were the same work. data bigger_shape_requirements: ExecutionRequirements = ExecutionRequirements { - shape: Shape { hard: HardRequirements { threads: hardware_thread_count(64) } }, + shape: Shape { + hard: HardRequirements { threads: hardware_thread_count(64) }, + envelope: unstated_envelope(), + }, capabilities: "linux-arm64", trust_domain: "fleet-owned", + isolation: shared_kernel_sandbox_profile(), } data other_runtime_requirements: ExecutionRequirements = ExecutionRequirements { shape: fixture_shape, capabilities: "linux-amd64", trust_domain: "fleet-owned", + isolation: shared_kernel_sandbox_profile(), } fn buy_terms(reservation: Int, ceiling: Int) -> BuyTerms { @@ -218,6 +227,7 @@ data owned_offer: Offer = Offer { shape: fixture_shape, capabilities: "linux-arm64", trust_domain: "fleet-owned", + isolation: shared_kernel_sandbox_profile(), quantity_bound: 1, ready_at: "2026-08-18T00:00:00Z", quote: QuotedPerSecond(MoneyRate { amount: money_amount_micro(0), currency: Usd }), @@ -230,6 +240,7 @@ data rented_offer: Offer = Offer { shape: fixture_shape, capabilities: "linux-arm64", trust_domain: "rented", + isolation: shared_kernel_sandbox_profile(), quantity_bound: 64, ready_at: "2026-08-18T00:04:00Z", quote: QuotedPerSecond(MoneyRate { amount: money_amount_micro(900), currency: Usd }), diff --git a/dag/test/claim/fabric_witness_run_test.dag b/dag/test/claim/fabric_witness_run_test.dag index 73be4d4e3d1..f6f2622d5d4 100644 --- a/dag/test/claim/fabric_witness_run_test.dag +++ b/dag/test/claim/fabric_witness_run_test.dag @@ -26,9 +26,10 @@ fn t_offer( Offer { id: FabricIdentity { principal: "gunbc", key: "offer-srv1" }, executor: "gunbc", - shape: Shape { hard: HardRequirements { threads: threads } }, + shape: Shape { hard: HardRequirements { threads: threads }, envelope: unstated_envelope() }, capabilities: caps, trust_domain: trust, + isolation: current_runner_slot_profile(), quantity_bound: 1, ready_at: "2026-08-19T00:00:00Z", quote: quote, @@ -71,9 +72,10 @@ fn t_fleet_offer() -> Offer { fn fungible(e: OfferFungibility) -> Bool { match e { Fungible => true - ShapeNotCovered { required_threads: _, offered_threads: _ } => false TrustDomainMismatch { required: _, offered: _ } => false CapabilitiesNotOffered { required: _, offered: _ } => false + IsolationNotProvided { missing: _ } => false + ShapeAxesNotCovered { unmet: _ } => false } } @@ -134,7 +136,8 @@ test fn foreign_trust_domain_refuses_despite_ample_capacity() -> Bool { )) { TrustDomainMismatch { required: _, offered: _ } => true Fungible => false - ShapeNotCovered { required_threads: _, offered_threads: _ } => false + ShapeAxesNotCovered { unmet: _ } => false + IsolationNotProvided { missing: _ } => false CapabilitiesNotOffered { required: _, offered: _ } => false } }