diff --git a/dag/extdeps/accounting/encumbrance.dag b/dag/extdeps/accounting/encumbrance.dag new file mode 100644 index 00000000000..1270dbb817f --- /dev/null +++ b/dag/extdeps/accounting/encumbrance.dag @@ -0,0 +1,275 @@ +module extdeps.accounting.encumbrance + +import std.measure { Measure, measure_add, measure_le } +import std.nat { Nat } +import std.types { NonEmptyStr, List, Timestamp } +import extdeps.accounting.budget { Appropriation } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// Encumbrance accounting, the upstream this module models. In fund and +// governmental accounting a commitment is recorded against an appropriation +// BEFORE the cash moves: an appropriation authorizes a ceiling, an encumbrance +// reserves part of it against an expected obligation, and an expenditure +// finally consumes some amount at or below what was encumbered. The residue +// is released back to the appropriation rather than silently retained. +// +// This is imported rather than coined because the reserve-then-settle +// lifecycle already has a name, a literature and a settled meaning. Minting a +// second vocabulary for it would be the nicknaming violation, and the borrowed +// names carry the discipline with them: an encumbrance is not spend, and an +// expenditure may not exceed the encumbrance that authorized it. +// +// The kernel is quantity-generic. It knows nothing about money, and nothing +// about compute; both are instantiations. That is deliberate rather than +// speculative genericity, since the reserve-settle-release shape is the same +// operation at both scales and forking it per subject would duplicate the +// conservation argument along with it. + +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "en.wikipedia.org/wiki/Encumbrance_(accounting)" + } +} + +// The lifecycle is a closed three-state coproduct rather than a record with +// nullable settlement fields. A reservation is held, or it settled at an exact +// amount, or it was released with a reason - and no fourth state exists to be +// represented by an absent field. The terminal arms carry their own timestamp +// because when a commitment ended is part of the commitment's record. + +type EncumbranceState = + | Held { maximum_liability: Measure } + | Expended { actual: Measure, settled_at: Timestamp } + | Released { reason: NonEmptyStr, released_at: Timestamp } + +// This carrier deliberately holds NO generation and no fencing vocabulary. +// An earlier version put a generation on every encumbrance and a stale- +// generation arm in the refusals, which is a layer inversion: temporal +// fencing is this repository's CI lease protocol, not a fact about +// encumbrance accounting, and an upstream authority that carried it would +// impose CI lease generations on every future consumer of appropriation +// conservation. The fence lives in product.fabric.budget, which checks it and +// then calls the transition here. + +type Encumbrance { + reference: NonEmptyStr + state: EncumbranceState +} + +type EncumbranceLedger { + appropriation: Appropriation + entries: List> +} + +// Committed funds are DERIVED from the entries, never stored. A stored balance +// can disagree with the entries that produced it, and then two authorities +// answer one question; recomputing cannot. Held liability and settled +// expenditure both count against the ceiling, because the whole point of +// encumbering is that an outstanding commitment is already spoken for. + +fn encumbrance_charge(e: Encumbrance) -> Measure { + match e.state { + Held { maximum_liability: m } => m + Expended { actual: a, settled_at: _ } => a + Released { reason: _, released_at: _ } => Measure { count: 0 } + } +} + +fn committed_total(ledger: EncumbranceLedger) -> Measure { + fold( + ledger.entries, + init: Measure { count: 0 }, + f: (acc, e) => measure_add(a: acc, b: encumbrance_charge(e: e)) + ) +} + +// Every refusal is typed and carries the two facts a reader needs to act on +// it. None of them carries a computed headroom: Nat subtraction is partial, +// and a difference that underflows would have to fabricate a value at exactly +// the moment the ledger is over its ceiling. The ceiling and the committed +// total are both present, so the reader can compare them without the kernel +// inventing arithmetic it cannot perform totally. + +type EncumbranceRefusal = + | ExceedsAppropriation { + requested: Measure, + committed: Measure, + ceiling: Measure, + } + | UnknownEncumbrance { reference: NonEmptyStr } + | DuplicateReference { reference: NonEmptyStr } + | ExpenditureExceedsEncumbrance { + reference: NonEmptyStr, + actual: Measure, + maximum_liability: Measure, + } + | AlreadyTerminal { reference: NonEmptyStr } + +type EncumbranceOutcome = + | LedgerAdvanced { ledger: EncumbranceLedger } + | EncumbranceRefused { refusal: EncumbranceRefusal } + +// Reserving refuses rather than admitting a commitment the appropriation +// cannot cover. It does not admit-and-flag, and it does not partially reserve: +// a caller that asked to hold an amount and received a smaller hold would +// proceed believing it was covered. + +fn reserve_encumbrance( + ledger: EncumbranceLedger, + reference: NonEmptyStr, + maximum_liability: Measure, +) -> EncumbranceOutcome { + match entry_matching(ledger: ledger, reference: reference) { + Cons { head: _, tail: _ } => + EncumbranceRefused { refusal: DuplicateReference { reference: reference } } + Empty {} => reserve_fresh_reference( + ledger: ledger, + reference: reference, + maximum_liability: maximum_liability, + ) + } +} + +// The reference is a KEY, and reserving refuses a second entry under one that +// is already present. Before this refusal existed it was not a key at all, and +// the consequence was not merely an untidy ledger. Settlement resolves a +// reference by taking the FIRST match while replacement rewrites EVERY match, +// so two holds under one reference meant a single settlement of some amount +// wrote that amount onto both entries - charging the appropriation twice for +// one commitment, at a total the caller never asked for - and no operation +// could ever address the second entry on its own to release it. +// +// So the wall is not defensive tidiness. It is what makes first-match +// resolution and rewrite-all-matches the same operation, which is the +// assumption the two functions below are written against. + +fn reserve_fresh_reference( + ledger: EncumbranceLedger, + reference: NonEmptyStr, + maximum_liability: Measure, +) -> EncumbranceOutcome { + let committed = committed_total(ledger: ledger) + let next = measure_add(a: committed, b: maximum_liability) + if measure_le(a: next, b: ledger.appropriation.ceiling) { + LedgerAdvanced { + ledger: EncumbranceLedger { + appropriation: ledger.appropriation, + entries: concat(ledger.entries, [ + Encumbrance { + reference: reference, + state: Held { maximum_liability: maximum_liability }, + } + ]), + } + } + } else { + EncumbranceRefused { + refusal: ExceedsAppropriation { + requested: maximum_liability, + committed: committed, + ceiling: ledger.appropriation.ceiling, + } + } + } +} + +fn entry_matching(ledger: EncumbranceLedger, reference: NonEmptyStr) -> List> { + ledger.entries |> filter(e => e.reference == reference) +} + +fn held_liability(e: Encumbrance) -> List> { + match e.state { + Held { maximum_liability: m } => [m] + Expended { actual: _, settled_at: _ } => [] + Released { reason: _, released_at: _ } => [] + } +} + +fn replace_entry( + ledger: EncumbranceLedger, + reference: NonEmptyStr, + next_state: EncumbranceState, +) -> EncumbranceLedger { + EncumbranceLedger { + appropriation: ledger.appropriation, + entries: ledger.entries |> map(e => + if e.reference == reference { + Encumbrance { reference: e.reference, state: next_state } + } else { + e + } + ), + } +} + +// Settlement checks what an accounting authority can check: that the +// reference is known, that it is still held, and that the expenditure does not +// exceed what was encumbered. An expenditure above the encumbrance refuses +// instead of expanding the hold, because expanding would cross the ceiling +// through the settle path rather than the reserve path -- the one place the +// conservation argument assumed it could not be crossed. + +fn settle_encumbrance( + ledger: EncumbranceLedger, + reference: NonEmptyStr, + actual: Measure, + settled_at: Timestamp, +) -> EncumbranceOutcome { + let matches = entry_matching(ledger: ledger, reference: reference) + match matches { + Empty {} => EncumbranceRefused { refusal: UnknownEncumbrance { reference: reference } } + Cons { head: e, tail: _ } => + match held_liability(e: e) { + Empty {} => EncumbranceRefused { refusal: AlreadyTerminal { reference: reference } } + Cons { head: liability, tail: _ } => + if measure_le(a: actual, b: liability) { + LedgerAdvanced { + ledger: replace_entry( + ledger: ledger, + reference: reference, + next_state: Expended { actual: actual, settled_at: settled_at }, + ) + } + } else { + EncumbranceRefused { + refusal: ExpenditureExceedsEncumbrance { + reference: reference, + actual: actual, + maximum_liability: liability, + } + } + } + } + } +} + +// Releasing an unused hold returns its full liability to the appropriation, +// which is what makes reserving the MAXIMUM safe rather than wasteful. Without +// it, a conservative liability estimate would permanently consume headroom it +// never used, and callers would be pushed toward under-reserving instead. + +fn release_encumbrance( + ledger: EncumbranceLedger, + reference: NonEmptyStr, + reason: NonEmptyStr, + released_at: Timestamp, +) -> EncumbranceOutcome { + let matches = entry_matching(ledger: ledger, reference: reference) + match matches { + Empty {} => EncumbranceRefused { refusal: UnknownEncumbrance { reference: reference } } + Cons { head: e, tail: _ } => + match held_liability(e: e) { + Empty {} => EncumbranceRefused { refusal: AlreadyTerminal { reference: reference } } + Cons { head: _, tail: _ } => + LedgerAdvanced { + ledger: replace_entry( + ledger: ledger, + reference: reference, + next_state: Released { reason: reason, released_at: released_at }, + ) + } + } + } +} diff --git a/dag/product/fabric/budget.dag b/dag/product/fabric/budget.dag new file mode 100644 index 00000000000..9273baef2a2 --- /dev/null +++ b/dag/product/fabric/budget.dag @@ -0,0 +1,253 @@ +module product.fabric.budget + +import std.types { NonEmptyStr, Int, Timestamp } +import std.measure { MoneyAmountMicro, Currency, Micro } +import std.currency { CurrencyCode } +import product.fabric.demand { BudgetAccountId } +import product.fabric.execution { ReservationRef } +import extdeps.accounting.encumbrance { + EncumbranceLedger, EncumbranceOutcome, EncumbranceRefusal, + LedgerAdvanced, EncumbranceRefused, + reserve_encumbrance, settle_encumbrance, release_encumbrance, committed_total, +} + +// The fabric's money binding over the generic encumbrance kernel. Everything +// about reserve-settle-release lives upstream; what is added here is the one +// fact the generic kernel cannot carry, and the reason it cannot. +// +// MoneyAmountMicro is Measure, and Currency there is a +// QUANTITY - the dimension - not a currency CODE. So two amounts in different +// currencies have the same type and add without complaint. A generic ledger +// instantiated at that quantity would therefore sum dollars and euros into a +// number with no meaning, and would do it silently, which is the worst +// available failure: the ceiling check would still pass or fail, just against +// a quantity that denominates nothing. +// +// The fix is not to teach the kernel about currency - a compute ledger has no +// use for that - but to bind the code ONCE to the account and refuse anything +// presented against it in another code. One account, one denomination, and a +// cross-currency line has nowhere to land. + +// The account identifier is product.fabric.demand's BudgetAccountId, imported +// rather than re-minted. A second identifier for one fact would be the +// nicknaming fork, and here it would also be actively load-bearing in the +// wrong direction: a demand's buy terms name the account they draw on, so +// joining terms to ledger is the whole point of the identifier, and two types +// for it make that join impossible to state. The one I had minted was also +// weaker -- a plain alias against a branded id -- so the fork was losing +// information as well as duplicating it. +// +// The import direction is worth noting as unfinished: the identity of an +// account arguably belongs with the account rather than with the demand that +// references it. Moving it would mean demand importing from this module, which +// cannot happen while this module is stacked above it. Left as the smaller of +// two wrongs, and cheap to correct once both land. +type MoneyAccount { + account: BudgetAccountId + currency: CurrencyCode + ledger: EncumbranceLedger + leases: List +} + +// A request names its own currency rather than inheriting the account's. That +// is the entire mechanism: if the request could not state a currency, a +// mismatch would be unrepresentable and therefore undetectable, and the check +// below would be checking nothing. The caller says what it means, and the +// account says whether that is what it holds. + +// The reference is product.fabric.execution's ReservationRef. An ExecutionGrant +// already carries money_reservation at that type and SettlementReceipt already +// names it, so these requests are the two operations that ACT on the thing the +// grant is holding -- taking an unbranded string here would mean the one type +// in the flow that cannot be confused with another key space is dropped +// precisely at the boundary where the grant hands over. +// +// The generic kernel below still takes NonEmptyStr, and that is correct rather +// than a leak: an encumbrance kernel that knew about fabric reservations would +// not be quantity-generic. The branding lives at the fabric API boundary and +// projects inward, which is the direction that keeps both true. +type MoneyReservationRequest { + reference: ReservationRef + generation: Int + maximum_liability: MoneyAmountMicro + currency: CurrencyCode +} + +type MoneySettlementRequest { + reference: ReservationRef + generation: Int + actual_spend: MoneyAmountMicro + currency: CurrencyCode + settled_at: Timestamp +} + +// The generation fence lives HERE, not in the accounting kernel. Temporal +// fencing is this fabric's lease protocol rather than a fact about +// encumbrance accounting, so an upstream carrier holding it would impose CI +// lease generations on every future consumer of appropriation conservation. +// The binding checks the fence and then calls the transition, which keeps the +// upstream authority about money and this module about leases. +// +// The held generation is recorded per reservation reference, because that is +// what a superseded holder's late settlement has to be compared against. + +type MoneyLease { + reference: ReservationRef + generation: Int +} + +fn lease_generation_for(a: MoneyAccount, reference: ReservationRef) -> List { + a.leases |> filter(l => l.reference == reference) |> map(l => l.generation) +} + +fn fence_admits(a: MoneyAccount, reference: ReservationRef, presented: Int) -> Bool { + match lease_generation_for(a: a, reference: reference) { + Empty {} => false + Cons { head: held, tail: _ } => held == presented + } +} + +type MoneyRefusal = + | CurrencyMismatch { + account: BudgetAccountId, + account_currency: CurrencyCode, + presented_currency: CurrencyCode, + } + | LedgerRefused { account: BudgetAccountId, refusal: EncumbranceRefusal } + | StaleLeaseGeneration { reference: ReservationRef, presented: Int } + +type MoneyOutcome = + | AccountAdvanced { account: MoneyAccount } + | MoneyRefused { refusal: MoneyRefusal } + +fn account_with_ledger(a: MoneyAccount, ledger: EncumbranceLedger) -> MoneyAccount { + MoneyAccount { account: a.account, currency: a.currency, ledger: ledger, leases: a.leases } +} + +fn account_with_lease(a: MoneyAccount, lease: MoneyLease) -> MoneyAccount { + MoneyAccount { + account: a.account, + currency: a.currency, + ledger: a.ledger, + leases: concat(a.leases, [lease]), + } +} + +fn project_outcome(a: MoneyAccount, outcome: EncumbranceOutcome) -> MoneyOutcome { + match outcome { + LedgerAdvanced { ledger: l } => AccountAdvanced { account: account_with_ledger(a: a, ledger: l) } + EncumbranceRefused { refusal: r } => + MoneyRefused { refusal: LedgerRefused { account: a.account, refusal: r } } + } +} + +// The currency wall is checked BEFORE the amount reaches the kernel, because +// once it is inside the kernel the code is gone and the mismatch is no longer +// observable. There is no arm that converts: a conversion needs a rate, a rate +// needs a source and a time, and inventing one at an admission boundary would +// fabricate the exact fact the refusal exists to demand. + +fn reserve_money(a: MoneyAccount, request: MoneyReservationRequest) -> MoneyOutcome { + if a.currency != request.currency { + MoneyRefused { + refusal: CurrencyMismatch { + account: a.account, + account_currency: a.currency, + presented_currency: request.currency, + } + } + } else { + record_lease( + o: project_outcome( + a: a, + outcome: reserve_encumbrance( + ledger: a.ledger, + reference: request.reference, + maximum_liability: request.maximum_liability, + ), + ), + reference: request.reference, + generation: request.generation, + ) + } +} + +fn settle_money(a: MoneyAccount, request: MoneySettlementRequest) -> MoneyOutcome { + if !fence_admits(a: a, reference: request.reference, presented: request.generation) { + MoneyRefused { + refusal: StaleLeaseGeneration { + reference: request.reference, + presented: request.generation, + } + } + } else if a.currency != request.currency { + MoneyRefused { + refusal: CurrencyMismatch { + account: a.account, + account_currency: a.currency, + presented_currency: request.currency, + } + } + } else { + project_outcome( + a: a, + outcome: settle_encumbrance( + ledger: a.ledger, + reference: request.reference, + actual: request.actual_spend, + settled_at: request.settled_at, + ), + ) + } +} + +// Release takes no amount, so it takes no currency and needs no wall. The +// released quantity is whatever was held, which the ledger already knows; a +// caller-supplied release amount would be a second authority for a number the +// entry carries, and could disagree with it. + +fn release_money( + a: MoneyAccount, + reference: ReservationRef, + generation: Int, + reason: NonEmptyStr, + released_at: Timestamp, +) -> MoneyOutcome { + if !fence_admits(a: a, reference: reference, presented: generation) { + MoneyRefused { + refusal: StaleLeaseGeneration { reference: reference, presented: generation } + } + } else { + project_outcome( + a: a, + outcome: release_encumbrance( + ledger: a.ledger, + reference: reference, + reason: reason, + released_at: released_at, + ), + ) + } +} + +// A successful reservation records the generation it was taken under, so a +// later settlement from a superseded holder has something exact to fail +// against. Recording only on success matters: a refused reservation that still +// wrote a lease would let the fence admit a hold that does not exist. + +fn record_lease(o: MoneyOutcome, reference: ReservationRef, generation: Int) -> MoneyOutcome { + match o { + AccountAdvanced { account: a } => + AccountAdvanced { + account: account_with_lease( + a: a, + lease: MoneyLease { reference: reference, generation: generation }, + ) + } + MoneyRefused { refusal: r } => MoneyRefused { refusal: r } + } +} + +fn account_committed(a: MoneyAccount) -> MoneyAmountMicro { + committed_total(ledger: a.ledger) +} diff --git a/dag/product/fabric/demand.dag b/dag/product/fabric/demand.dag new file mode 100644 index 00000000000..8fcafd93c42 --- /dev/null +++ b/dag/product/fabric/demand.dag @@ -0,0 +1,128 @@ +module product.fabric.demand + +import std.types { NonEmptyStr, Timestamp, Bool } +import std.measure { MoneyAmountMicro } +import std.currency { CurrencyCode } +import product.fabric.identity { FabricIdentity, DemandKey, WorkKey } + +// Demand is WHO currently wants a result and WHERE to report it. Provider facts +// live here and nowhere else, which is what keeps Work provider-neutral. + +// A Demand is immutable. There is deliberately no cancelled, superseded or +// rerun field on it, because those are TRANSITIONS over an identity rather +// than properties of one - and a mutable status field is the thing that later +// makes it impossible to answer what was true when a decision was taken. A +// binding interprets a provider observation into one of the normalized +// commands below and supplies authenticated evidence for that interpretation; +// the core decides the effect. +// Cancellation CANNOT live entirely in a provider binding, and the reason is a +// two-provider argument rather than a stylistic one. Suppose a GitHub demand +// and a GitLab demand attach to the same Work. If the GitHub binding cancels +// that Work directly when its pull request is superseded, it destroys work the +// GitLab demand still requires. Only the core knows the complete demand +// population, so the binding owns INTERPRETATION - this observation means +// withdraw, or supersede, or re-execute - and the core owns EFFECT: whether +// the transition is authorized, whether any other demand still requires the +// Work, whether a running Attempt should continue, whether capacity and budget +// should be released. +// Rerun is not one flag. It decomposes into three independent questions, and +// collapsing them is how re-run comes to mean delete every cache. (1) May an +// existing terminal receipt satisfy this demand? (2) Must a new Attempt exist? +// (3) May that Attempt reuse accepted step receipts and materializations? An +// ordinary duplicate demand answers yes, no, yes - it attaches to the existing +// execution. A provider rerun answers no, yes, yes - the prior verdict is not +// accepted but warm materializations remain valid. An operator clean recompute +// answers no, yes, no - prior step materializations are refused at the +// declared frame. Three separate fields, because a system that offers only +// rerun forces the third answer whenever the first is wanted. +type SatisfactionRequirement { + terminal_receipt_may_satisfy: Bool + new_attempt_required: Bool + step_reuse_permitted: Bool +} + +// Provenance is the binding's stable, idempotent reference to whatever the +// provider observed. The core treats it as opaque: it is carried so a result can +// be reported back, and it is never interpreted. + +type ObservationReceiptRef = NonEmptyStr where brand("ObservationReceiptRef") + +type BudgetAccountId = NonEmptyStr where brand("BudgetAccountId") + +// Buy terms are the BUYER half of the posted-offer market. A reservation price is +// the maximum this demand will pay; a delay valuation prices waiting, without +// which a fabric optimizing money alone waits minutes to save cents. + +// Three monetary facts stay separate throughout, and conflating them into one +// price field is the defect this note exists to prevent. MaximumLiability is +// the amount that must be RESERVED before a grant may issue. SelectionCost is +// the amount used to COMPARE candidates, and it includes valued availability +// delay so that a supplier who can start now is correctly preferred over a +// cheaper supplier who cannot. ActualSpend is the irreversible amount SETTLED +// after execution and release. For the first policy the maximum liability may +// equal the provider-charge portion of the selection cost; keeping the three +// named means a later expected-cost model can diverge without touching ExecutionGrant +// or settlement. maximum_buy_order is the ceiling on a single grant's +// liability - a refusal boundary, never a degradation: an ask above it refuses +// rather than selecting something cheaper and unsuitable. +// There is deliberately NO delay-valuation field yet. Selection is specified +// to compare a provider charge against a valued availability delay, which +// needs a money-per-second RATE, and this record has no honest carrier for +// one: MoneyAmountMicro would put the dimension in the field name, and the +// existing MoneyRate bundles a CurrencyCode that would let a rate disagree +// with the currency these terms already carry. +// +// Landing the field on the wrong type and describing the mismatch in a comment +// was the alternative, and it is the shape DESIGN refuses -- a dissolution note +// is a lifecycle fact, not permission to create the debt, and the author cannot +// grant himself that permission. Since nothing consumes the field yet, the +// cheaper and more honest option is simply not to ship it: the terms carry what +// they can state correctly, and the rate arrives with its carrier once the +// denomination authority -- these terms, or the referenced budget account -- is +// decided. An absent field forces that decision; a wrongly-typed one hides it. +type BuyTerms { + budget_account: BudgetAccountId + currency: CurrencyCode + reservation_price: MoneyAmountMicro + maximum_buy_order: MoneyAmountMicro +} + +type AdmissionTerms { + priority_class: NonEmptyStr + deadline: Timestamp? + buy: BuyTerms +} + +type Demand

{ + id: FabricIdentity + work: FabricIdentity + origin: ObservationReceiptRef + submitted_at: Timestamp + admission: AdmissionTerms + satisfaction: SatisfactionRequirement +} + +// The normalized command vocabulary a binding may produce. A provider event is +// interpreted into exactly one of these; the core never sees the provider's own +// event shape. + +type DemandCommand

+ = SubmitDemand { demand: Demand

} + | WithdrawDemand { demand: FabricIdentity, evidence: ObservationReceiptRef } + | SupersedeDemand { + superseded: FabricIdentity, + replacement: Demand

, + evidence: ObservationReceiptRef, + } + +fn demand_work

(d: Demand

) -> FabricIdentity { + d.work +} + +fn demand_reservation_price

(d: Demand

) -> MoneyAmountMicro { + d.admission.buy.reservation_price +} + +fn demand_maximum_buy_order

(d: Demand

) -> MoneyAmountMicro { + d.admission.buy.maximum_buy_order +} diff --git a/dag/product/fabric/execution.dag b/dag/product/fabric/execution.dag new file mode 100644 index 00000000000..150d29685a5 --- /dev/null +++ b/dag/product/fabric/execution.dag @@ -0,0 +1,217 @@ +module product.fabric.execution + +import std.types { NonEmptyStr, Timestamp, List, Int } +import std.measure { MoneyAmountMicro, Second } +import std.content_hash { ContentHash, compare_content_hash, ContentHashEqual, ContentHashDifferent, ContentHashCrossFamilyIncomparable } +import product.fabric.identity { fabric_identity_eq, FabricIdentity, ExecutionAttemptKey, DemandKey, WorkKey, GrantKey, OfferKey, ReceiptKey } +import product.fabric.demand { ObservationReceiptRef } +import product.fabric.supply { OfferQuote } + +// An Attempt is one concrete try at a Work. Retries create attempts; they never +// create new Work and never mutate a failed attempt back into a pending one. + +// Lineage is a typed reason rather than a counter, because the three reasons +// an attempt exists have different authorization, different accounting and +// different reuse rules, and a retry_count answers none of them. +// InitialAttempt is the first try for a demand. InfrastructureRetry names the +// prior attempt AND the receipt that classified the loss, so an attempt can +// never claim infrastructure loss without evidence of it - the failure mode +// that makes a real compile error retry forever is a classifier that discards +// the termination reason. RequestedReexecution is a demand-driven rerun, which +// is policy rather than infrastructure. An attempt carries no host and no +// mutable status: the host lives on the ExecutionGrant, and the position in the run is +// DERIVED from accepted receipts, never stored. +type ExecutionAttemptLineage

+ = InitialAttempt { initiating_demand: FabricIdentity } + | InfrastructureRetry { + prior_attempt: FabricIdentity, + cause_receipt: ObservationReceiptRef, + } + | RequestedReexecution { initiating_demand: FabricIdentity } + +type Attempt

{ + id: FabricIdentity + work: FabricIdentity + lineage: ExecutionAttemptLineage

+ created_at: Timestamp +} + +// A resource claim is a quantity reserved against a conserved appropriation. The +// money claim and the compute claims are the same shape at different magnitudes, +// which is why one parameterized ledger serves both. + +type ReservationRef = NonEmptyStr where brand("ReservationRef") + +type LeaseKey = NonEmptyStr where brand("LeaseKey") + +type LeaseIdentity { + lease_key: LeaseKey + resource_fingerprint: ContentHash + generation: Int +} + +// resource_fingerprint names the EXACT reserved claim, not the host. Naming +// the host is the defect that makes two admitted slices of one machine +// indistinguishable at the fence, so a stale holder of one slice can +// invalidate a live holder of another. Ownership and generation fencing come +// from std.temporal_effect HeldLease; what that carrier does NOT supply is +// time - it has no timestamp and no expiry, and its stale arm is a supplied +// observation rather than a verdict derived from a deadline. Lease liveness is +// therefore new modeling that lands with the reservation ledger, and it is +// stated here so no reader concludes from the presence of a generation that +// expiry is already solved. +// The ExecutionGrant is an authorization decision, not a bespoke fold. It projects into +// std.access, whose AccessDecision is the only allow/deny result in the system. + +// There is deliberately no FabricGrantDecision of Allowed and Denied. +// std.access is the one authorization kernel, its decision type is the only +// allow/deny result, and every denial already carries a typed cause at +// structured request coordinates. Minting a parallel decision sum here would +// be the second authority DESIGN forbids, and it would immediately diverge: +// one of the two would gain a refusal cause the other lacked. The positive +// ExecutionGrant carrier below records what an admitted request produced; it is not a +// second verdict. +type FabricGrantAction = + | ExecuteAttempt + +type FabricGrantObject

{ + offer: FabricIdentity + quote: OfferQuote +} + +type FabricGrantContext

{ + demand: FabricIdentity + work: FabricIdentity + attempt: FabricIdentity + executor: P + lease: LeaseIdentity + issued_at: Timestamp + maximum_liability: MoneyAmountMicro +} + +type FabricGrantEvidence { + fungibility_receipt: ObservationReceiptRef + offer_authority: ObservationReceiptRef + resource_conservation: ObservationReceiptRef + budget_conservation: ObservationReceiptRef + principal_authority: ObservationReceiptRef +} + +type ExecutionGrant

{ + id: FabricIdentity + object: FabricGrantObject

+ context: FabricGrantContext

+ evidence: FabricGrantEvidence + resource_reservations: List + money_reservation: ReservationRef +} + +// Every reservation a grant requires is applied tentatively and committed only +// if EVERY ledger admits. Resource admitted with money refused must commit no +// resource reservation, and money admitted with resource refused must commit +// no money reservation; both are one canonical state transition. A partial +// commit is the state that leaks capacity or budget with no grant to account +// for it, and it is unreachable only if the join is atomic rather than +// sequential. +// Receipts are what was materialized, executed and settled. Acceptance is gated +// on the lease generation still being canonical. + +type ReceiptPayload + = MaterializationReceipt { source: ContentHash, verified_at: Timestamp } + | ExecutionReceipt { + step_id: NonEmptyStr, + outputs: ContentHash, + billable: Second, + completed_at: Timestamp, + } + | SettlementReceipt { + reservation: ReservationRef, + actual_spend: MoneyAmountMicro, + settled_at: Timestamp, + } + +type Receipt

{ + id: FabricIdentity + attempt: FabricIdentity + lease: LeaseIdentity + payload: ReceiptPayload +} + +// Elapsed execution time is NOT by itself authoritative spend, which is why +// the execution receipt carries billable seconds as an OBSERVATION and the +// settlement receipt carries the settled amount as a separate fact. The +// supplier binding owns the billing rule - when billing starts, the quantum +// and rounding, minimum charge, fixed and setup charges, caps, and when +// billing stops - because those differ per supplier and are already visible in +// the cited rows: hourly rates alongside monthly caps and setup fees. +// Settlement therefore derives from quote plus billable-usage evidence plus +// release evidence, and MISSING RELEASE EVIDENCE HOLDS THE RESERVATION rather +// than assuming the supplier stopped charging. Assuming release is the arm +// that quietly under-reserves against a machine still billing. +fn receipt_lease_generation

(r: Receipt

) -> Int { + r.lease.generation +} + +fn grant_lease_generation

(g: ExecutionGrant

) -> Int { + g.context.lease.generation +} + +// Acceptance compares the WHOLE lease identity, not the generation alone. +// Comparing generations only was a real fencing hole: generation is a small +// integer that every lease starts at and increments independently, so two +// entirely different leases sit at the same number almost immediately, and a +// receipt produced under one would have been accepted against a grant holding +// the other. The comment above this block already said resource_fingerprint +// must name the exact reserved claim so a stale holder of one slice cannot +// invalidate a live holder of another -- and then the check ignored it, which +// made the prose describe a wall the code did not build. +// +// The attempt is compared for the same reason. A receipt names the attempt +// that produced it, and a grant names the attempt it authorized; a receipt +// from a different attempt is not stale, it is unrelated, and the two +// deserve different causes rather than one Bool that says only "no". +// +// It is compared as a full FabricIdentity, not by key. Comparing keys alone +// admitted a receipt from a DIFFERENT PRINCIPAL that happened to use the same +// attempt name -- a cross-tenant fail-open in the exact carrier whose whole +// design puts the principal inside the identity so it cannot be dropped by +// accident. It was dropped by accident anyway, one field access at a time, +// which is why the pair now has an equality function rather than leaving each +// caller to remember. +// +// A cross-family fingerprint comparison REFUSES rather than reporting +// difference. Two hashes from different families are not known-different, +// they are incomparable, and collapsing that into "different" would report +// a definite mismatch where the honest answer is that no comparison happened. + +type ReceiptAdmission = + | ReceiptAdmissible + | ReceiptFromDifferentLease + | ReceiptFromDifferentAttempt + | ReceiptFingerprintIncomparable + | ReceiptGenerationStale { presented: Int, current: Int } + +fn admit_receipt_for_grant

(r: Receipt

, g: ExecutionGrant

) -> ReceiptAdmission { + if !fabric_identity_eq(left: r.attempt, right: g.context.attempt) { + ReceiptFromDifferentAttempt + } else if r.lease.lease_key != g.context.lease.lease_key { + ReceiptFromDifferentLease + } else { + match compare_content_hash( + left: r.lease.resource_fingerprint, + right: g.context.lease.resource_fingerprint, + ) { + ContentHashCrossFamilyIncomparable => ReceiptFingerprintIncomparable + ContentHashDifferent => ReceiptFromDifferentLease + ContentHashEqual => + if receipt_lease_generation(r: r) == grant_lease_generation(g: g) { + ReceiptAdmissible + } else { + ReceiptGenerationStale { + presented: receipt_lease_generation(r: r), + current: grant_lease_generation(g: g), + } + } + } + } +} diff --git a/dag/product/fabric/identity.dag b/dag/product/fabric/identity.dag new file mode 100644 index 00000000000..bb41f84a71d --- /dev/null +++ b/dag/product/fabric/identity.dag @@ -0,0 +1,55 @@ +module product.fabric.identity + +import std.types { NonEmptyStr } + +// Identity shell for every fabric carrier. The principal is PART of the identity +// rather than metadata beside it, so that two principals asking for the same +// computation hold two distinct identities without a later migration widening +// every carrier. P stays a type parameter: the core imports no closed principal +// enum, and a provider binding supplies its own evidence-derived principal type. + +// The principal is a component of identity, not a field beside it. A fabric +// identity is the pair (principal, key), so cross-principal isolation holds by +// construction rather than by every consumer remembering to compare two +// things. P is open: the core never imports a closed GitHub/GitLab/OIDC/POSIX +// principal enum, because a fabric that names its principal sources cannot +// admit a supplier it did not anticipate. The role P plays differs per carrier +// and is documented on each: requester on Demand, accounting and security +// scope on Work, the account a try is authorized and charged under on Attempt, +// supplier on Offer, grantee on ExecutionGrant, attesting producer on Receipt. An ExecutionGrant +// is bilateral, so naming its grantee here does not erase the supplier role +// its Offer reference carries. +type DemandKey = NonEmptyStr where brand("DemandKey") + +type WorkKey = NonEmptyStr where brand("WorkKey") + +type ExecutionAttemptKey = NonEmptyStr where brand("ExecutionAttemptKey") + +type OfferKey = NonEmptyStr where brand("OfferKey") + +type GrantKey = NonEmptyStr where brand("GrantKey") + +type ReceiptKey = NonEmptyStr where brand("ReceiptKey") + +type FabricIdentity { + principal: P + key: K +} + +fn fabric_identity_key(id: FabricIdentity) -> K { + id.key +} + +// Equality is over the PAIR, because that is what identity means here. A +// comparison on the key alone silently merges two tenants who chose the same +// name for their work, which is not a naming collision but a cross-principal +// leak: the whole reason principal sits INSIDE identity rather than beside it +// is that dropping it must not be expressible as an ordinary field access. + +fn fabric_identity_eq(left: FabricIdentity, right: FabricIdentity) -> Bool { + left.principal == right.principal && left.key == right.key +} + +fn fabric_identity_principal(id: FabricIdentity) -> P { + id.principal +} diff --git a/dag/product/fabric/supply.dag b/dag/product/fabric/supply.dag new file mode 100644 index 00000000000..ab8f956a43a --- /dev/null +++ b/dag/product/fabric/supply.dag @@ -0,0 +1,135 @@ +module product.fabric.supply + +import std.types { Timestamp, Int } +import std.measure { MoneyAmountMicro, MoneyPerSecond, MoneyPerHour, MoneyOnce } +import std.currency { CurrencyCode } +import product.compute_fabric { Shape } +import product.fabric.identity { FabricIdentity, OfferKey } +import product.fabric.demand { ObservationReceiptRef } +import product.fabric.work { CapabilityManifestRef, TrustDomainRef } + +// 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 +// the statement, not the kind of thing being stated. + +// Observed and quoted supply differ in their evidence, not in their type, and +// minting two Offer types would fork the selection fold that must compare +// them. ObservedSupply is a measurement - this host has three free slots right +// now, and here is the receipt. QuotedSupply is a standing willingness to sell +// - this supplier will provide up to N of this shape at this rate until this +// time, and here is the quote. Bottomless cloud supply is a QuotedSupply with +// a large quantity bound, never an unbounded one: an offer without a bound +// cannot be conserved against, and infinite supply is a claim no supplier +// actually makes. The fields the decision consumes - quantity bound, +// readiness, validity, normalized quote - stay SURFACED on the offer rather +// than hidden inside the evidence; the evidence proves those values, it does +// not replace them. +// An owned offer carries an EXPLICIT ZERO quote and creates a zero-valued +// money reservation, rather than carrying no quote at all. Absence must never +// be interpreted as free. The predecessor model made cost_quote optional and +// every owned host used the absent arm, so a consumer reading it could not +// distinguish costs nothing from nobody priced this - and the safe reading of +// the second is not zero. Requiring the amount means a supplier whose price is +// genuinely unknown has to say so in a way the selection fold can refuse, +// instead of being silently treated as the cheapest offer available. +// A quote is std.measure's MoneyRate at the period the supplier bills in, +// never a second money-per-period record. MoneyRate already carries the amount +// and the currency and already makes the period a type argument, so a rate at +// one period is not assignable where another is expected -- which is exactly +// the property a price needs, and the reason an earlier version of this file +// minting its own carrier was a fork rather than a specialization. That +// version's stated defence was that folding the unit into the measure would +// make two rates addable; MoneyRate does not fold it into the measure, so the +// defence described a carrier that does not exist. +// +// The runtime coproduct is here for a reason the type parameter cannot serve: +// selection ranks offers billed on different bases against each other, so they +// must inhabit one roster, and Offer and Offer would +// be different types. Discriminating at the value level keeps the roster +// homogeneous while keeping the periods unaddable, since reaching either +// amount requires naming which period it is. +// +// Normalizing a supplier's published terms into one of these is the supplier +// binding's work, and so are billing quantum, rounding, minimum charge, fixed +// and setup charges, caps, and when billing starts and stops. The core +// compares normalized quotes; it does not model any supplier's tariff. + +type OfferQuote = + | QuotedPerSecond(MoneyPerSecond) + | QuotedPerHour(MoneyPerHour) + | QuotedFlatPerGrant(MoneyOnce) + +fn offer_quote_amount(q: OfferQuote) -> MoneyAmountMicro { + match q { + QuotedPerSecond(r) => r.amount + QuotedPerHour(r) => r.amount + QuotedFlatPerGrant(r) => r.amount + } +} + +fn offer_quote_currency(q: OfferQuote) -> CurrencyCode { + match q { + QuotedPerSecond(r) => r.currency + QuotedPerHour(r) => r.currency + QuotedFlatPerGrant(r) => r.currency + } +} + +type OfferEvidence + = ObservedSupply { observed_at: Timestamp, receipt: ObservationReceiptRef } + | QuotedSupply { + quoted_at: Timestamp, + valid_until: Timestamp, + receipt: ObservationReceiptRef, + } + +type Offer

{ + id: FabricIdentity + executor: P + shape: Shape + capabilities: CapabilityManifestRef + trust_domain: TrustDomainRef + quantity_bound: Int + ready_at: Timestamp + quote: OfferQuote + evidence: OfferEvidence +} + +// An Offer carries no remaining_capacity field. Remaining capacity is DERIVED +// as the allocatable bound minus the sum of active grant claims against that +// offer, and deriving it is precisely what makes atomic grant issuance +// conserve supply. A stored remainder is a second representation of the grant +// set: it can disagree with the grants that actually exist, and the +// disagreement is invisible until two grants have already been issued against +// capacity that existed only in a stale field. +// Selection is a named policy with one implementation. The interface is named so +// a second policy is a second instantiation rather than an edit to ExecutionGrant or to +// the clearing fold; if adding one later requires touching a core carrier, the +// axis was never real. + +// The policy is an axis with exactly one instantiation today: cheapest +// fungible with delay valuation. The ORDER of its filters is load-bearing and +// is not a performance detail. Fungibility is decided FIRST - which offers can +// satisfy this work's shape, capabilities and trust domain, with price not +// consulted - so that price can never rescue an offer that cannot run the +// work. Affordability is decided SECOND: within the demand's reservation price +// and maximum buy order, with budget remaining. Cheapest is decided LAST, over +// the survivors, comparing provider charge plus valued availability delay, +// with a stable deterministic tie-break. This is a posted-offer market and not +// an auction: suppliers publish asks, each demand carries a buyer reservation +// price, and the fabric takes the cheapest admissible ask. No clearing-price +// machinery exists because none is needed to make that decision. +// Rented supply being selected only after owned supply is exhausted is a +// CONSEQUENCE of cheapest-admissible-ask, never a fallback arm, and the +// distinction decides whether cost can run away. A fallback is a failure arm +// that widens when the preferred path is unavailable, and it hides the deficit +// that triggered it. Here nothing widens: owned capacity at an explicit zero +// quote is simply the cheapest admissible ask while any remains, and when none +// remains the same fold evaluates the same predicate over the remaining asks. +// If no ask is admissible - budget exhausted, every ask above the reservation +// price or the maximum buy order, no offer fungible - the outcome is a typed +// refusal or a demand that stays pending. It is never a degraded execution +// path, and there is no arm to reach for one. + +type SelectionPolicy = + | CheapestFungibleWithDelayValuation diff --git a/dag/product/fabric/work.dag b/dag/product/fabric/work.dag new file mode 100644 index 00000000000..00dff2d400c --- /dev/null +++ b/dag/product/fabric/work.dag @@ -0,0 +1,221 @@ +module product.fabric.work + +import std.types { NonEmptyStr, List } +import std.content_hash { ContentHash, content_hash_of_value, serialize_content_hash } +import product.compute_fabric { Shape } +import std.measure { hardware_thread_count_value } +import product.fabric.identity { FabricIdentity, WorkKey } + +// Work is WHAT is computed, and it is provider-neutral by construction: no field +// here can name a repository, a pull request, a branch or a commit, because those +// are facts about who asked and where to report, which live on Demand. + +// No field on Work or WorkContract may carry a provider identifier. This is +// not a naming preference: it is what makes a second SCM binding a new +// authority plus a new binding rather than an edit to the core. Two bindings +// that normalize to the same source manifest, program, runtime closure, effect +// contract and output contract produce the SAME Work, so one execution serves +// demands arriving from different providers. They produce DIFFERENT Work when +// the declared inputs genuinely differ - one testing a pull-request head and +// another a synthesized merge tree, history or merge base consumed as input, +// submodule or large-file materialization differing, available effects +// differing, or provenance itself declared as an input. The decision is made +// by the declared inputs, never by a global rule that repository always +// matters or that tree bytes are always sufficient. +// Source identity is a canonical MANIFEST, not a bare tree digest. It covers +// path, content digest, file mode where semantically relevant, symlink target, +// submodule object identity and large-file object identity wherever those are +// consumed by the contract. A Git tree object id is a valid BINDING-level +// source identity and may be sufficient for a first Git-based implementation; +// it is not the universal fabric source type, because a fabric that assumes +// Git tree semantics has assumed an SCM. The binding produces two separate +// facts - a source content manifest and a provenance receipt - and Work always +// consumes the manifest, consuming provenance only where provenance is a +// declared input. +type ProgramRef = NonEmptyStr where brand("ProgramRef") + +type ArtifactManifestRef = NonEmptyStr where brand("ArtifactManifestRef") + +type EffectContractRef = NonEmptyStr where brand("EffectContractRef") + +type OutputContractRef = NonEmptyStr where brand("OutputContractRef") + +type SourceManifestRef = NonEmptyStr where brand("SourceManifestRef") + +// Resumability is a property of what a step DECLARES, never of the fabric. A step +// whose effects are undeclared cannot be resumed by any mechanism, so the tier is +// carried on the contract and the fabric refuses to claim checkpointing it cannot +// honor. + +// Three tiers, ordered by what the step declares rather than by how it is +// implemented. ReceiptSatisfiable: inputs declared and outputs are content- +// addressed artifacts, so an accepted receipt whose outputs remain +// materializable lets the step be skipped entirely. IdempotentUnderKey: the +// step has external effects but re-running under the same idempotency key is +// safe, so it is never skippable by content yet is safely repeatable. +// OpaqueEffects: effects are undeclared, so the step is not resumable at all +// and its only sound treatment is rerun from a clean boundary. An arbitrary +// shell step in a foreign CI workflow is OpaqueEffects unless its contract +// says otherwise, and that is the honest degradation: the fabric runs it and +// declines to promise resume, rather than inventing a checkpoint where no +// state was captured. A long compiler invocation is ONE step at +// ReceiptSatisfiable grain - twenty minutes into it there is no accepted +// receipt, so interruption reruns it; a mutable build directory or a compiler +// cache is a materialization provider that may accelerate the rerun, never +// proof the step completed. +type ResumabilityTier + = ReceiptSatisfiable + | IdempotentUnderKey { idempotency_key: ContentHash } + | OpaqueEffects { reason: NonEmptyStr } + +type WorkStep { + step_id: NonEmptyStr + resumability: ResumabilityTier +} + +type WorkContract { + program: ProgramRef + steps: List + source: SourceManifestRef + inputs: ArtifactManifestRef + runtime_closure: ArtifactManifestRef + effect_contract: EffectContractRef + output_contract: OutputContractRef +} + +// Scheduling facts that do not change the promised answer live BESIDE the +// contract, never inside it, so that revising a resource estimate cannot mint a +// new semantic Work. + +// Capability and trust-domain references are declared HERE, on the +// requirement side, and imported by supply rather than redeclared there. +// Fungibility - selection's first and load-bearing step - compares a Work's +// requirements against an Offer's capabilities, so the two sides of that +// comparison are two readings of one fact. Typing them separately would make +// the comparison need a coercion, and a coercion between two spellings of one +// concept is where the divergence starts. + +type CapabilityManifestRef = NonEmptyStr where brand("CapabilityManifestRef") + +type TrustDomainRef = NonEmptyStr where brand("TrustDomainRef") + +type ExecutionRequirements { + shape: Shape + capabilities: CapabilityManifestRef + trust_domain: TrustDomainRef +} + +type Work

{ + id: FabricIdentity + contract: WorkContract + requirements: ExecutionRequirements +} + +// The key is DERIVED here rather than accepted from a caller, and that is the +// difference between a claim and a mechanism. Before this function existed the +// comment below already said the key derives from the semantic contract, but +// nothing computed it: a Work took an arbitrary branded key beside an arbitrary +// contract, so one contract could carry two keys, two contracts could carry one +// key, and a binding could let a provider fact influence the key with the core +// unable to notice. The witness that was supposed to prove neutrality authored +// one constant and placed it in both demands, so it would have passed against a +// key that ignored every input. +// +// Every field of the contract and of the requirements feeds the digest, and +// nothing else can: the function takes no other argument, so excluding +// scheduling facts is a property of its signature rather than of an author's +// discipline. Requirements are included because a Work that needs a different +// architecture or trust domain does not promise the same answer. + +fn work_identity_material(contract: WorkContract, requirements: ExecutionRequirements) -> NonEmptyStr { + concat( + contract.program, "\u{1f}", + work_steps_material(steps: contract.steps), "\u{1f}", + contract.source, "\u{1f}", + contract.inputs, "\u{1f}", + contract.runtime_closure, "\u{1f}", + contract.effect_contract, "\u{1f}", + contract.output_contract, "\u{1f}", + requirements.capabilities, "\u{1f}", + requirements.trust_domain, "\u{1f}", + shape_material(shape: requirements.shape) + ) +} + +// 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 -- +// and fungibility in product.fabric.supply compares shape, so deduplication +// identity and matching constraints would have disagreed about whether two +// things were the same work. A machine that cannot run one of them is not an +// interchangeable executor for both. +// +// It is rendered through the cited accessor rather than by reaching into the +// record, so a shape that grows an axis fails to compile here instead of +// silently dropping the new axis out of the identity. + +fn shape_material(shape: Shape) -> NonEmptyStr { + concat( + "threads:", + to_string(hardware_thread_count_value(t: shape.hard.threads)) + ) +} + +fn work_step_material(step: WorkStep) -> NonEmptyStr { + concat(step.step_id, "\u{1e}", resumability_material(tier: step.resumability)) +} + +fn resumability_material(tier: ResumabilityTier) -> NonEmptyStr { + match tier { + ReceiptSatisfiable => "receipt-satisfiable" + IdempotentUnderKey { idempotency_key: k } => + concat("idempotent-under-key:", serialize_content_hash(hash: k)) + OpaqueEffects { reason: _ } => "opaque-effects" + } +} + +fn work_steps_material(steps: List) -> NonEmptyStr { + fold( + steps, + init: "steps", + f: (acc, step) => concat(acc, "\u{1d}", work_step_material(step: step)) + ) +} + +fn derive_work_key(contract: WorkContract, requirements: ExecutionRequirements) -> WorkKey { + serialize_content_hash( + hash: content_hash_of_value( + value: work_identity_material(contract: contract, requirements: requirements) + ) + ) +} + +// The public constructor. A Work cannot be built with a key someone chose, +// because this is the only place a key comes from. + +fn work_for

(principal: P, contract: WorkContract, requirements: ExecutionRequirements) -> Work

{ + Work { + id: FabricIdentity { + principal: principal, + key: derive_work_key(contract: contract, requirements: requirements), + }, + contract: contract, + requirements: requirements, + } +} + +// The work key is derived from the semantic contract alone. Excluded, each for +// the same reason - it changes how work is scheduled or attempted, never what +// answer the work promises: priority, queue position, chosen host, cache +// presence, attempt number, resource prediction, monetary quote, budget +// account, reservation price. Including any of them forks one computation into +// many identities and destroys the deduplication the key exists to provide. +// Conversely a property that can change the ANSWER - toolchain, architecture, +// available effects - belongs in the runtime closure or effect contract and +// therefore DOES participate. The test is not whether a fact is important; it +// is whether two runs differing only in that fact could legitimately produce +// different output. +fn work_contract_source(contract: WorkContract) -> SourceManifestRef { + contract.source +} + diff --git a/dag/std/measure.dag b/dag/std/measure.dag index 661679a7058..ed88253c4cb 100644 --- a/dag/std/measure.dag +++ b/dag/std/measure.dag @@ -656,6 +656,8 @@ fn money_amount_micro_count(m: MoneyAmountMicro) -> Nat { data money_rate_billing_unit_note: String = "Billing unit is part of the fact: per-minute, per-hour, and per-month are distinct carriers — never folded into a bare amount with the unit in the field name. Cross-vendor normalization is a derived projection at read time, never a stored catalog field." +type PerSecond + type PerMinute type PerHour @@ -669,6 +671,8 @@ type MoneyRate

{ currency: CurrencyCode } +type MoneyPerSecond = MoneyRate + type MoneyPerMinute = MoneyRate type MoneyPerHour = MoneyRate diff --git a/dag/test/claim/fabric_budget_encumbrance_witness_test.dag b/dag/test/claim/fabric_budget_encumbrance_witness_test.dag new file mode 100644 index 00000000000..880b2e3e93b --- /dev/null +++ b/dag/test/claim/fabric_budget_encumbrance_witness_test.dag @@ -0,0 +1,330 @@ +module test.claim.fabric_budget_encumbrance_witness + +import std.types { NonEmptyStr, Bool, Int, List } +import std.measure { money_amount_micro, money_amount_micro_count } +import std.currency { Usd, Eur } +import std.nat { Nat } +import extdeps.accounting.budget { Appropriation } +import extdeps.accounting.encumbrance { EncumbranceLedger, ExceedsAppropriation, UnknownEncumbrance, ExpenditureExceedsEncumbrance, AlreadyTerminal, DuplicateReference } +import product.fabric.budget { MoneyAccount, MoneyReservationRequest, MoneySettlementRequest, MoneyOutcome, AccountAdvanced, MoneyRefused, CurrencyMismatch, LedgerRefused, StaleLeaseGeneration, reserve_money, settle_money, release_money, account_committed } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// Budget is modeled as a lease over money: something is held exclusively, +// the holder can be superseded while still believing it holds, and a late +// settlement from a superseded holder must not be honoured. These witnesses +// exercise that claim at the two boundaries where it is decidable - the +// ceiling and the generation fence - plus the currency wall the generic +// kernel deliberately cannot carry. + +data usd_account: MoneyAccount = MoneyAccount { + account: "fleet-ci", + currency: Usd, + ledger: EncumbranceLedger { + appropriation: Appropriation { ceiling: money_amount_micro(count: 1000000) }, + entries: [], + }, + leases: [], +} + +fn advanced_account(o: MoneyOutcome) -> List { + match o { + AccountAdvanced { account: a } => [a] + MoneyRefused { refusal: _ } => [] + } +} + +fn is_refused(o: MoneyOutcome) -> Bool { + match o { + AccountAdvanced { account: _ } => false + MoneyRefused { refusal: _ } => true + } +} + +// Every refusal below names the arm it expects, rather than asserting that +// something refused. The distinction is not pedantry: `is_refused` is true for +// a ceiling overrun, a stale generation and a duplicate reference alike, so a +// ceiling test written against it passes against an implementation that +// refuses for entirely the wrong reason - and would have passed against the +// duplicate-reference bug this file now covers. Naming the arm is what makes +// each test discriminate the wall it claims to be about. + +fn refusal_label(o: MoneyOutcome) -> NonEmptyStr { + match o { + AccountAdvanced { account: _ } => "advanced" + MoneyRefused { refusal: r } => + match r { + CurrencyMismatch { account: _, account_currency: _, presented_currency: _ } => "currency-mismatch" + StaleLeaseGeneration { reference: _, presented: _ } => "stale-generation" + LedgerRefused { account: _, refusal: lr } => + match lr { + ExceedsAppropriation { requested: _, committed: _, ceiling: _ } => "exceeds-appropriation" + UnknownEncumbrance { reference: _ } => "unknown-encumbrance" + DuplicateReference { reference: _ } => "duplicate-reference" + ExpenditureExceedsEncumbrance { reference: _, actual: _, maximum_liability: _ } => "expenditure-exceeds-encumbrance" + AlreadyTerminal { reference: _ } => "already-terminal" + } + } + } +} + +fn reserve_on(a: MoneyAccount, reference: NonEmptyStr, generation: Int, micros: Nat) -> MoneyOutcome { + reserve_money( + a: a, + request: MoneyReservationRequest { + reference: reference, + generation: generation, + maximum_liability: money_amount_micro(count: micros), + currency: Usd, + }, + ) +} + +fn settle_on(a: MoneyAccount, reference: NonEmptyStr, generation: Int, micros: Nat) -> MoneyOutcome { + settle_money( + a: a, + request: MoneySettlementRequest { + reference: reference, + generation: generation, + actual_spend: money_amount_micro(count: micros), + currency: Usd, + settled_at: "2026-08-18T02:00:00Z", + }, + ) +} + +// Reserving the maximum liability encumbers the full amount up front. This is +// the property that makes the ceiling meaningful: an outstanding commitment +// counts against the budget before any money moves, so a second reservation +// cannot be admitted against headroom the first one has already spoken for. + +test fn a_held_reservation_encumbers_its_full_liability() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 1, micros: 400000)) { + Empty {} => false + Cons { head: a, tail: _ } => + money_amount_micro_count(m: account_committed(a: a)) == 400000 + } +} + +// The ceiling refuses rather than admitting a partial hold. A caller that +// asked to hold 700000 against 600000 of headroom and received a smaller hold +// would proceed believing it was covered for the larger amount. + +test fn a_reservation_over_the_ceiling_refuses_rather_than_partially_holding() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 1, micros: 400000)) { + Empty {} => false + Cons { head: a, tail: _ } => { + let second = reserve_on(a: a, reference: "grant-2", generation: 1, micros: 700000) + refusal_label(o: second) == "exceeds-appropriation" + && money_amount_micro_count(m: account_committed(a: a)) == 400000 + } + } +} + +// Settling below the held liability is the ordinary case, and the released +// residue returns to the appropriation. Without that, reserving a +// conservative maximum would permanently consume headroom it never used, and +// callers would be pushed toward under-reserving instead. + +test fn settling_under_the_hold_returns_the_residue() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 1, micros: 400000)) { + Empty {} => false + Cons { head: held, tail: _ } => + match advanced_account(o: settle_on(a: held, reference: "grant-1", generation: 1, micros: 250000)) { + Empty {} => false + Cons { head: settled, tail: _ } => + money_amount_micro_count(m: account_committed(a: held)) == 400000 + && money_amount_micro_count(m: account_committed(a: settled)) == 250000 + } + } +} + +// Spending above what was encumbered refuses instead of expanding the hold. +// Expanding it would cross the ceiling through the settle path rather than the +// reserve path, which is the one place the conservation argument assumed it +// could not be crossed. + +test fn spending_above_the_hold_refuses_instead_of_expanding_it() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 1, micros: 400000)) { + Empty {} => false + Cons { head: held, tail: _ } => + refusal_label(o: settle_on(a: held, reference: "grant-1", generation: 1, micros: 400001)) + == "expenditure-exceeds-encumbrance" + } +} + +// The generation fence is the lease half. A superseded holder settling late +// must not be honoured, and the check is decidable at settlement rather than +// racing, because the reservation carries the generation it was made under. + +test fn a_superseded_holder_cannot_settle() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 7, micros: 400000)) { + Empty {} => false + Cons { head: held, tail: _ } => + refusal_label(o: settle_on(a: held, reference: "grant-1", generation: 6, micros: 100000)) + == "stale-generation" + && refusal_label(o: settle_on(a: held, reference: "grant-1", generation: 7, micros: 100000)) == "advanced" + } +} + +// A terminal entry cannot be settled twice. Double settlement would charge one +// commitment against the appropriation two times, and the second charge would +// be invisible in a ledger that only stored a running total. + +test fn a_settled_reservation_cannot_settle_again() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 1, micros: 400000)) { + Empty {} => false + Cons { head: held, tail: _ } => + match advanced_account(o: settle_on(a: held, reference: "grant-1", generation: 1, micros: 250000)) { + Empty {} => false + Cons { head: settled, tail: _ } => + refusal_label(o: settle_on(a: settled, reference: "grant-1", generation: 1, micros: 100000)) + == "already-terminal" + } + } +} + +// Releasing frees the whole hold, so the headroom it occupied becomes +// available to a later reservation that would otherwise have been refused. + +test fn releasing_a_hold_frees_its_headroom() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 1, micros: 900000)) { + Empty {} => false + Cons { head: held, tail: _ } => { + let blocked = reserve_on(a: held, reference: "grant-2", generation: 1, micros: 500000) + match advanced_account( + o: release_money( + a: held, + reference: "grant-1", + generation: 1, + reason: "attempt abandoned before execution", + released_at: "2026-08-18T02:00:00Z", + ) + ) { + Empty {} => false + Cons { head: freed, tail: _ } => + refusal_label(o: blocked) == "exceeds-appropriation" + && money_amount_micro_count(m: account_committed(a: freed)) == 0 + && refusal_label(o: reserve_on(a: freed, reference: "grant-2", generation: 1, micros: 500000)) == "advanced" + } + } + } +} + +// The currency wall. MoneyAmountMicro carries no currency code, so a generic +// ledger would add euros to dollars silently and check the ceiling against a +// quantity denominating nothing. The account binds the code once and refuses +// anything presented in another - and it never converts, because a conversion +// needs a rate, and a rate invented at an admission boundary fabricates the +// exact fact the refusal exists to demand. + +test fn a_foreign_currency_reservation_refuses_and_never_converts() -> Bool { + let foreign = reserve_money( + a: usd_account, + request: MoneyReservationRequest { + reference: "grant-eu", + generation: 1, + maximum_liability: money_amount_micro(count: 100000), + currency: Eur, + }, + ) + refusal_label(o: foreign) == "currency-mismatch" + && money_amount_micro_count(m: account_committed(a: usd_account)) == 0 +} + +// The refusal must be the CURRENCY one specifically. A euro amount inside the +// ceiling would be admitted by the kernel on the numbers alone, so if the wall +// were merely ordering the mismatch would surface as some other refusal, or as +// none - which is how a silent cross-currency sum gets in. + +test fn the_currency_refusal_is_distinct_from_a_ceiling_refusal() -> Bool { + let foreign = reserve_money( + a: usd_account, + request: MoneyReservationRequest { + reference: "grant-eu", + generation: 1, + maximum_liability: money_amount_micro(count: 100000), + currency: Eur, + }, + ) + match foreign { + AccountAdvanced { account: _ } => false + MoneyRefused { refusal: r } => + match r { + CurrencyMismatch { account: _, account_currency: ac, presented_currency: pc } => + ac == Usd && pc == Eur + LedgerRefused { account: _, refusal: _ } => false + StaleLeaseGeneration { reference: _, presented: _ } => false + } + } +} + +// Review 53147: the reference must be a KEY. A second hold under a live +// reference is refused, and the ledger is unchanged by the refusal - the +// second half matters because a refusal that still appended would leave the +// exact state the wall exists to prevent while reporting that it did not. + +test fn a_second_hold_under_one_reference_refuses() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 1, micros: 400000)) { + Empty {} => false + Cons { head: held, tail: _ } => { + let duplicate = reserve_on(a: held, reference: "grant-1", generation: 1, micros: 100000) + refusal_label(o: duplicate) == "duplicate-reference" + && money_amount_micro_count(m: account_committed(a: held)) == 400000 + } + } +} + +// The discriminating half, and the reason the wall is not tidiness. Settlement +// takes the FIRST match while replacement rewrites EVERY match, so before the +// refusal existed one settlement of 250000 against two holds wrote 250000 onto +// both - charging 500000 for one commitment. This asserts a settled reference +// charges its amount EXACTLY ONCE, which is the property the duplicate broke. + +test fn one_settlement_charges_the_appropriation_exactly_once() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 1, micros: 400000)) { + Empty {} => false + Cons { head: held, tail: _ } => + match advanced_account(o: settle_on(a: held, reference: "grant-1", generation: 1, micros: 250000)) { + Empty {} => false + Cons { head: settled, tail: _ } => + money_amount_micro_count(m: account_committed(a: settled)) == 250000 + } + } +} + +// Uniqueness spans EVERY entry, not just the live ones, so a released +// reference is not reusable. That is the deliberate choice rather than the +// convenient one: the entries are an append-only record of what was committed +// and what became of it, and admitting a second "grant-1" after the first was +// released would put two entries under one name in that record, with only +// their position to tell them apart. A reader asking what happened to +// "grant-1" would get an ambiguous answer, and the audit value of the ledger +// is exactly that the question has one. +// +// The cost is that a caller wanting to retry must mint a new reference. That +// is the correct obligation anyway - a retry is a new commitment, and the +// fabric already models it as a new attempt with its own identity. + +test fn a_released_reference_is_not_reusable() -> Bool { + match advanced_account(o: reserve_on(a: usd_account, reference: "grant-1", generation: 1, micros: 400000)) { + Empty {} => false + Cons { head: held, tail: _ } => + match advanced_account( + o: release_money( + a: held, + reference: "grant-1", + generation: 1, + reason: "attempt abandoned before execution", + released_at: "2026-08-18T02:00:00Z", + ) + ) { + Empty {} => false + Cons { head: freed, tail: _ } => + refusal_label(o: reserve_on(a: freed, reference: "grant-1", generation: 1, micros: 400000)) + == "duplicate-reference" + && money_amount_micro_count(m: account_committed(a: freed)) == 0 + && refusal_label(o: reserve_on(a: freed, reference: "grant-1-retry", generation: 1, micros: 400000)) == "advanced" + } + } +} diff --git a/dag/test/claim/fabric_terminal_contract_witness_test.dag b/dag/test/claim/fabric_terminal_contract_witness_test.dag new file mode 100644 index 00000000000..f17db0a94b5 --- /dev/null +++ b/dag/test/claim/fabric_terminal_contract_witness_test.dag @@ -0,0 +1,483 @@ +module test.claim.fabric_terminal_contract_witness + +import std.types { NonEmptyStr, String, Bool, Int } +import std.measure { money_amount_micro, money_amount_micro_count, hardware_thread_count, second, MoneyRate } +import std.content_hash { content_hash_of_value } +import std.currency { Usd } +import product.compute_fabric { Shape, HardRequirements } +import product.fabric.identity { FabricIdentity, fabric_identity_key, DemandKey, WorkKey } +import product.fabric.work { Work, WorkContract, ExecutionRequirements, WorkStep, derive_work_key, work_for, ReceiptSatisfiable, IdempotentUnderKey, OpaqueEffects } +import product.fabric.demand { Demand, AdmissionTerms, BuyTerms, SatisfactionRequirement, demand_work, demand_reservation_price, demand_maximum_buy_order } +import product.fabric.supply { Offer, QuotedPerSecond, offer_quote_amount, offer_quote_currency, ObservedSupply, QuotedSupply } +import product.fabric.execution { Attempt, InitialAttempt, InfrastructureRetry, LeaseIdentity, Receipt, ExecutionReceipt, ExecutionGrant, FabricGrantObject, FabricGrantContext, FabricGrantEvidence, ReceiptAdmissible, ReceiptFromDifferentLease, ReceiptFromDifferentAttempt, ReceiptFingerprintIncomparable, ReceiptGenerationStale, admit_receipt_for_grant } + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// The acceptance test for the terminal contract: two synthetic SCM bindings must +// project into the same core carriers without the core naming either of them. + +// These fixtures stand in for a GitHub binding and a GitLab binding. Nothing +// in this file imports a provider module, and nothing in product.fabric.* +// names one - that absence IS the claim under test. The two bindings differ +// only in the provenance they carry on their Demand, and the discriminating +// 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_requirements: ExecutionRequirements = ExecutionRequirements { + shape: fixture_shape, + capabilities: "linux-arm64", + trust_domain: "fleet-owned", +} + +data fixture_contract: WorkContract = WorkContract { + program: "gunbc-required-floor", + steps: [WorkStep { step_id: "floor", resumability: ReceiptSatisfiable }], + source: "sha256:tree-abc", + inputs: "manifest-inputs-1", + runtime_closure: "toolchain-rust-1.89", + effect_contract: "effects-read-only", + output_contract: "outputs-verdict", +} + +// The key is DERIVED, never authored. An earlier version of this file declared +// a constant and placed it into both synthetic demands, which made the headline +// neutrality test unfalsifiable: it would have passed against a key that +// ignored every contract input, while claiming to prove the opposite. + +data fixture_work_key: WorkKey = derive_work_key( + contract: fixture_contract, + requirements: fixture_requirements, +) + +fn work_for_principal(p: NonEmptyStr) -> Work { + work_for(principal: p, contract: fixture_contract, requirements: fixture_requirements) +} + +// A contract differing in ONE semantic input - the source tree - and one +// differing only in a scheduling-irrelevant way are the two controls the +// derivation has to separate. + +data other_source_contract: WorkContract = WorkContract { + program: "gunbc-required-floor", + steps: [WorkStep { step_id: "floor", resumability: ReceiptSatisfiable }], + source: "sha256:tree-DIFFERENT", + inputs: "manifest-inputs-1", + runtime_closure: "toolchain-rust-1.89", + effect_contract: "effects-read-only", + output_contract: "outputs-verdict", +} + +// Same contract, same capabilities and trust domain, DIFFERENT shape. Before +// the shape fed the digest these derived one key while carrying different +// machine requirements, and fungibility compares shape - so dedup identity and +// 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) } }, + capabilities: "linux-arm64", + trust_domain: "fleet-owned", +} + +data other_runtime_requirements: ExecutionRequirements = ExecutionRequirements { + shape: fixture_shape, + capabilities: "linux-amd64", + trust_domain: "fleet-owned", +} + +fn buy_terms(reservation: Int, ceiling: Int) -> BuyTerms { + BuyTerms { + budget_account: "acct-fleet", + currency: Usd, + reservation_price: money_amount_micro(reservation), + maximum_buy_order: money_amount_micro(ceiling), + } +} + +fn demand_from_binding( + key: DemandKey, + provenance: NonEmptyStr, + reservation: Int, + ceiling: Int, +) -> Demand { + Demand { + id: FabricIdentity { principal: "operator", key: key }, + work: FabricIdentity { principal: "operator", key: fixture_work_key }, + origin: provenance, + submitted_at: "2026-08-18T00:00:00Z", + admission: AdmissionTerms { + priority_class: "required-gate", + deadline: none, + buy: buy_terms(reservation: reservation, ceiling: ceiling), + }, + satisfaction: SatisfactionRequirement { + terminal_receipt_may_satisfy: true, + new_attempt_required: false, + step_reuse_permitted: true, + }, + } +} + +data github_binding_demand: Demand = demand_from_binding( + key: "demand-gh-1", + provenance: "github:pull/8387/head", + reservation: 500, + ceiling: 1000, +) + +data gitlab_binding_demand: Demand = demand_from_binding( + key: "demand-gl-1", + provenance: "gitlab:merge_request/42/head", + reservation: 250, + ceiling: 400, +) + +// The load-bearing claim: two providers, one Work. + +test fn two_bindings_project_into_one_work_identity() -> Bool { + fabric_identity_key(id: demand_work(d: github_binding_demand)) + == fabric_identity_key(id: demand_work(d: gitlab_binding_demand)) + && github_binding_demand.origin != gitlab_binding_demand.origin + && fabric_identity_key(id: github_binding_demand.id) + != fabric_identity_key(id: gitlab_binding_demand.id) +} + +// The derivation controls. Without these the test above is satisfied by a key +// that ignores its inputs entirely, which is what an authored constant was. + +test fn one_changed_semantic_input_changes_the_work_key() -> Bool { + derive_work_key(contract: fixture_contract, requirements: fixture_requirements) + != derive_work_key(contract: other_source_contract, requirements: fixture_requirements) +} + +// Requirements are part of the promise, not scheduling trivia: work that needs +// a different architecture does not promise the same answer, so it must not +// share a key with work that does. + +test fn changed_execution_requirements_change_the_work_key() -> Bool { + derive_work_key(contract: fixture_contract, requirements: fixture_requirements) + != derive_work_key(contract: fixture_contract, requirements: other_runtime_requirements) +} + +// And the direction that matters most for the fabric: identical semantics +// reached through two different providers derive the SAME key, so the +// deduplication the whole design rests on is a property of the function rather +// than of two fixtures happening to be given one constant. + +test fn identical_contracts_derive_one_key_regardless_of_who_asked() -> Bool { + derive_work_key(contract: fixture_contract, requirements: fixture_requirements) + == derive_work_key( + contract: WorkContract { + program: "gunbc-required-floor", + steps: [WorkStep { step_id: "floor", resumability: ReceiptSatisfiable }], + source: "sha256:tree-abc", + inputs: "manifest-inputs-1", + runtime_closure: "toolchain-rust-1.89", + effect_contract: "effects-read-only", + output_contract: "outputs-verdict", + }, + requirements: fixture_requirements, + ) +} + +// Cost differs between the two demands while the Work they attach to does not. +// This is the structural form of cost does not enter the work key. + +// A machine that cannot run one of them is not an interchangeable executor for +// both, so a differing shape must derive a differing key. + +test fn a_different_machine_shape_changes_the_work_key() -> Bool { + derive_work_key(contract: fixture_contract, requirements: fixture_requirements) + != derive_work_key(contract: fixture_contract, requirements: bigger_shape_requirements) +} + +test fn cost_terms_differ_without_forking_work() -> Bool { + money_amount_micro_count(m: demand_reservation_price(d: github_binding_demand)) == 500 + && money_amount_micro_count(m: demand_reservation_price(d: gitlab_binding_demand)) == 250 + && money_amount_micro_count(m: demand_maximum_buy_order(d: github_binding_demand)) == 1000 + && (demand_work(d: github_binding_demand).key as String) + == (demand_work(d: gitlab_binding_demand).key as String) +} + +// Different principals are different Work, even at an identical contract. + +test fn principals_do_not_share_work_identity() -> Bool { + let mine = work_for_principal(p: "operator") + let theirs = work_for_principal(p: "other-tenant") + (mine.id.key as String) == (theirs.id.key as String) + && (mine.id.principal as String) != (theirs.id.principal as String) +} + +// An owned offer states zero explicitly; absence is not free. + +data owned_offer: Offer = Offer { + id: FabricIdentity { principal: "operator", key: "offer-srv3-slot" }, + executor: "srv3", + shape: fixture_shape, + capabilities: "linux-arm64", + trust_domain: "fleet-owned", + quantity_bound: 1, + ready_at: "2026-08-18T00:00:00Z", + quote: QuotedPerSecond(MoneyRate { amount: money_amount_micro(0), currency: Usd }), + evidence: ObservedSupply { observed_at: "2026-08-18T00:00:00Z", receipt: "obs-srv3-1" }, +} + +data rented_offer: Offer = Offer { + id: FabricIdentity { principal: "operator", key: "offer-rented-1" }, + executor: "rented-pool", + shape: fixture_shape, + capabilities: "linux-arm64", + trust_domain: "rented", + quantity_bound: 64, + ready_at: "2026-08-18T00:04:00Z", + quote: QuotedPerSecond(MoneyRate { amount: money_amount_micro(900), currency: Usd }), + evidence: QuotedSupply { + quoted_at: "2026-08-18T00:00:00Z", + valid_until: "2026-08-18T01:00:00Z", + receipt: "quote-rented-1", + }, +} + +test fn owned_supply_states_zero_rather_than_absent() -> Bool { + money_amount_micro_count(m: offer_quote_amount(q: owned_offer.quote)) == 0 + && money_amount_micro_count(m: offer_quote_amount(q: rented_offer.quote)) == 900 + && offer_quote_currency(q: owned_offer.quote) == Usd + && owned_offer.quantity_bound == 1 + && rented_offer.quantity_bound == 64 +} + +// Observed and quoted supply are one type with two evidences. + +test fn observed_and_quoted_supply_share_one_offer_type() -> Bool { + match owned_offer.evidence { + ObservedSupply { observed_at: _, receipt: _ } => + match rented_offer.evidence { + QuotedSupply { quoted_at: _, valid_until: _, receipt: _ } => true + ObservedSupply { observed_at: _, receipt: _ } => false + } + QuotedSupply { quoted_at: _, valid_until: _, receipt: _ } => false + } +} + +// A retry is a new attempt naming its cause, never a mutated old one. + +data lease_gen_9: LeaseIdentity = LeaseIdentity { + lease_key: "lease-attempt-1", + resource_fingerprint: content_hash_of_value(value: "srv3-slot-2"), + generation: 9, +} + +data first_attempt: Attempt = Attempt { + id: FabricIdentity { principal: "operator", key: "attempt-1" }, + work: FabricIdentity { principal: "operator", key: fixture_work_key }, + lineage: InitialAttempt { + initiating_demand: FabricIdentity { principal: "operator", key: "demand-gh-1" }, + }, + created_at: "2026-08-18T00:00:00Z", +} + +data retry_attempt: Attempt = Attempt { + id: FabricIdentity { principal: "operator", key: "attempt-2" }, + work: FabricIdentity { principal: "operator", key: fixture_work_key }, + lineage: InfrastructureRetry { + prior_attempt: FabricIdentity { principal: "operator", key: "attempt-1" }, + cause_receipt: "obs-worker-lost-1", + }, + created_at: "2026-08-18T00:10:00Z", +} + +test fn retry_is_a_new_attempt_naming_its_cause() -> Bool { + (first_attempt.id.key as String) != (retry_attempt.id.key as String) + && (first_attempt.work.key as String) == (retry_attempt.work.key as String) + && match retry_attempt.lineage { + InfrastructureRetry { prior_attempt: prior, cause_receipt: _ } => + (prior.key as String) == (first_attempt.id.key as String) + InitialAttempt { initiating_demand: _ } => false + RequestedReexecution { initiating_demand: _ } => false + } +} + +// A receipt carries the generation it was produced under, so a stale producer is +// distinguishable from a current one. + +data stale_receipt: Receipt = Receipt { + id: FabricIdentity { principal: "operator", key: "receipt-1" }, + attempt: FabricIdentity { principal: "operator", key: "attempt-1" }, + lease: LeaseIdentity { + lease_key: "lease-attempt-1", + resource_fingerprint: content_hash_of_value(value: "srv3-slot-2"), + generation: 8, + }, + payload: ExecutionReceipt { + step_id: "floor", + outputs: content_hash_of_value(value: "outputs-1"), + billable: second(count: 3600), + completed_at: "2026-08-18T01:00:00Z", + }, +} + +data fixture_grant: ExecutionGrant = ExecutionGrant { + id: FabricIdentity { principal: "operator", key: "grant-1" }, + object: FabricGrantObject { offer: owned_offer.id, quote: owned_offer.quote }, + context: FabricGrantContext { + demand: github_binding_demand.id, + work: FabricIdentity { principal: "operator", key: fixture_work_key }, + attempt: first_attempt.id, + executor: "srv3", + lease: lease_gen_9, + issued_at: "2026-08-18T01:00:00Z", + maximum_liability: money_amount_micro(1000000), + }, + evidence: FabricGrantEvidence { + fungibility_receipt: "fungibility-1", + offer_authority: "offer-authority-1", + resource_conservation: "resource-conservation-1", + budget_conservation: "budget-conservation-1", + principal_authority: "principal-authority-1", + }, + resource_reservations: ["reservation-cpu-1"], + money_reservation: "reservation-money-1", +} + +// The receipt that makes the fence discriminating. It is at the SAME +// generation as the grant and names the same attempt, and differs only in +// which slice of the host it was produced against. A fence comparing +// generations alone accepts it, which is the defect this fixture exists to +// catch: generation is a small integer every lease starts at and increments +// independently, so two unrelated leases share a number almost immediately. + +data other_slice_receipt: Receipt = Receipt { + id: FabricIdentity { principal: "operator", key: "receipt-2" }, + attempt: FabricIdentity { principal: "operator", key: "attempt-1" }, + lease: LeaseIdentity { + lease_key: "lease-attempt-1", + resource_fingerprint: content_hash_of_value(value: "srv3-slot-7"), + generation: 9, + }, + payload: ExecutionReceipt { + step_id: "floor", + outputs: content_hash_of_value(value: "outputs-2"), + billable: second(count: 3600), + completed_at: "2026-08-18T01:00:00Z", + }, +} + +// Same attempt KEY, different principal. This is the cross-tenant case: two +// tenants naming their attempt identically must not share receipts, and a +// key-only comparison admits this one. + +data foreign_principal_receipt: Receipt = Receipt { + id: FabricIdentity { principal: "other-tenant", key: "receipt-4" }, + attempt: FabricIdentity { principal: "other-tenant", key: "attempt-1" }, + lease: lease_gen_9, + payload: ExecutionReceipt { + step_id: "floor", + outputs: content_hash_of_value(value: "outputs-4"), + billable: second(count: 3600), + completed_at: "2026-08-18T01:00:00Z", + }, +} + +data foreign_attempt_receipt: Receipt = Receipt { + id: FabricIdentity { principal: "operator", key: "receipt-3" }, + attempt: FabricIdentity { principal: "operator", key: "attempt-99" }, + lease: lease_gen_9, + payload: ExecutionReceipt { + step_id: "floor", + outputs: content_hash_of_value(value: "outputs-3"), + billable: second(count: 3600), + completed_at: "2026-08-18T01:00:00Z", + }, +} + +fn admission_label(r: Receipt) -> NonEmptyStr { + match admit_receipt_for_grant(r: r, g: fixture_grant) { + ReceiptAdmissible => "admissible" + ReceiptFromDifferentLease => "different-lease" + ReceiptFromDifferentAttempt => "different-attempt" + ReceiptFingerprintIncomparable => "fingerprint-incomparable" + ReceiptGenerationStale { presented: _, current: _ } => "generation-stale" + } +} + +// Acceptance must compare the WHOLE lease identity. The three refusals below +// are each reachable only if a different part of that identity is checked: +// generation alone cannot tell same-generation-different-slice from current, +// and cannot tell a foreign attempt from a stale one. + +test fn acceptance_compares_lease_identity_not_only_generation() -> Bool { + admission_label(r: stale_receipt) == "generation-stale" + && admission_label(r: other_slice_receipt) == "different-lease" + && admission_label(r: foreign_attempt_receipt) == "different-attempt" +} + +// The cross-tenant control. Identity is the pair, so an attempt key alone is +// not an attempt; a receipt carrying another principal's identically-named +// attempt is refused rather than admitted. + +test fn a_receipt_from_another_principal_is_not_the_same_attempt() -> Bool { + admission_label(r: foreign_principal_receipt) == "different-attempt" +} + +// The positive control. Without it every refusal above is satisfied by an +// admission function that refuses everything. + +test fn a_receipt_from_the_granted_lease_is_admissible() -> Bool { + match admit_receipt_for_grant( + r: Receipt { + id: FabricIdentity { principal: "operator", key: "receipt-ok" }, + attempt: first_attempt.id, + lease: lease_gen_9, + payload: ExecutionReceipt { + step_id: "floor", + outputs: content_hash_of_value(value: "outputs-ok"), + billable: second(count: 10), + completed_at: "2026-08-18T01:00:00Z", + }, + }, + g: fixture_grant, + ) { + ReceiptAdmissible => true + ReceiptFromDifferentLease => false + ReceiptFromDifferentAttempt => false + ReceiptFingerprintIncomparable => false + ReceiptGenerationStale { presented: _, current: _ } => false + } +} + +// Resumability is declared per step, so a step with opaque effects cannot be +// mistaken for a checkpointable one. The three tiers are discriminated +// SEPARATELY rather than folded to a Bool: "may this be replayed" has three +// answers, and idempotent-under-key differs from opaque-effects in what the +// fabric is permitted to do, so a projection that answered false for both +// would erase the distinction this type exists to carry. + +fn resumability_tier_of(step: WorkStep) -> NonEmptyStr { + match step.resumability { + ReceiptSatisfiable => "receipt-satisfiable" + IdempotentUnderKey { idempotency_key: _ } => "idempotent-under-key" + OpaqueEffects { reason: _ } => "opaque-effects" + } +} + +test fn resumability_is_declared_not_assumed() -> Bool { + let satisfiable = resumability_tier_of(step: WorkStep { + step_id: "build", + resumability: ReceiptSatisfiable, + }) + let idempotent_tier = resumability_tier_of(step: WorkStep { + step_id: "deploy", + resumability: IdempotentUnderKey { idempotency_key: content_hash_of_value(value: "deploy-1") }, + }) + let opaque = resumability_tier_of(step: WorkStep { + step_id: "arbitrary-shell", + resumability: OpaqueEffects { reason: "foreign workflow step declares no effects" }, + }) + satisfiable == "receipt-satisfiable" + && idempotent_tier == "idempotent-under-key" + && opaque == "opaque-effects" + && idempotent_tier != opaque +}