Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 18 additions & 1 deletion dag/product/fabric/execution.dag
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,20 @@ import product.fabric.supply { OfferQuote }
// 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
// the termination reason. CapabilityEscalation is that same shape for a
// DIFFERENT cause: the prior attempt reached a terminal result its resolved
// model could not carry, and a more capable model takes the next try. It is a
// sibling of InfrastructureRetry rather than an arm of one generic Retry
// because the two differ in exactly the ways lineage exists to record --
// authorization, accounting, and what the edge licenses you to conclude. An
// infrastructure loss says nothing about the work; an escalation says the work
// exceeded the capability that was tried, which is the single observation the
// resident-model thesis is measured on, and collapsing the two would erase it.
// Like InfrastructureRetry it names the prior attempt AND the receipt that
// established the prior result, so an attempt can never claim escalation
// without evidence of what it escalated from: merely resolving a more
// expensive model after a cheaper one is a selection fact, not an escalation.
// 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.
Expand All @@ -27,6 +40,10 @@ type ExecutionAttemptLineage<P>
prior_attempt: FabricIdentity<P, ExecutionAttemptKey>,
cause_receipt: ObservationReceiptRef,
}
| CapabilityEscalation {
prior_attempt: FabricIdentity<P, ExecutionAttemptKey>,
cause_receipt: ObservationReceiptRef,
}
| RequestedReexecution { initiating_demand: FabricIdentity<P, DemandKey> }

type Attempt<P> {
Expand Down
56 changes: 55 additions & 1 deletion dag/test/claim/fabric_terminal_contract_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ import product.fabric.identity { FabricIdentity, fabric_identity_key, DemandKey,
import product.fabric.work { Shape, HardRequirements, 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 { SupplierOffer, 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 product.fabric.execution { Attempt, InitialAttempt, InfrastructureRetry, CapabilityEscalation, LeaseIdentity, Receipt, ExecutionReceipt, ExecutionGrant, FabricGrantObject, FabricGrantContext, FabricGrantEvidence, ReceiptAdmissible, ReceiptFromDifferentLease, ReceiptFromDifferentAttempt, ReceiptFingerprintIncomparable, ReceiptGenerationStale, admit_receipt_for_grant }

import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

Expand Down Expand Up @@ -307,10 +307,64 @@ test fn retry_is_a_new_attempt_naming_its_cause() -> Bool {
InfrastructureRetry { prior_attempt: prior, cause_receipt: _ } =>
(prior.key as String) == (first_attempt.id.key as String)
InitialAttempt { initiating_demand: _ } => false
CapabilityEscalation { prior_attempt: _, cause_receipt: _ } => false
RequestedReexecution { initiating_demand: _ } => false
}
}

// AN ESCALATION IS A NEW ATTEMPT AT THE SAME WORK, AND IT IS NOT A RETRY.
// The two arms are deliberately the same SHAPE -- prior attempt plus the
// receipt that established the prior result -- so the only thing separating
// them is the arm itself. That is exactly why the discriminating control below
// matches on the arm rather than on its payload: a witness that only checked
// the prior-attempt key would pass identically against a lineage that had
// collapsed escalation into InfrastructureRetry, which is the collapse the
// authority's note argues against and therefore the one its evidence must be
// able to see.

data escalated_attempt: Attempt<NonEmptyStr> = Attempt {
id: FabricIdentity { principal: "operator", key: "attempt-3" },
work: FabricIdentity { principal: "operator", key: fixture_work_key },
lineage: CapabilityEscalation {
prior_attempt: FabricIdentity { principal: "operator", key: "attempt-1" },
cause_receipt: "obs-local-model-terminal-1",
},
created_at: "2026-08-18T00:20:00Z",
}

test fn escalation_is_a_new_attempt_at_the_same_work() -> Bool {
(escalated_attempt.id.key as String) != (first_attempt.id.key as String)
&& (escalated_attempt.work.key as String) == (first_attempt.work.key as String)
}

test fn escalation_names_the_attempt_it_escalated_from() -> Bool {
match escalated_attempt.lineage {
CapabilityEscalation { prior_attempt: prior, cause_receipt: _ } =>
(prior.key as String) == (first_attempt.id.key as String)
InitialAttempt { initiating_demand: _ } => false
InfrastructureRetry { prior_attempt: _, cause_receipt: _ } => false
RequestedReexecution { initiating_demand: _ } => false
}
}

// THE DISCRIMINATING CONTROL. An escalation must not read as an infrastructure
// loss and an infrastructure loss must not read as an escalation, because the
// two license opposite conclusions about the work: a lost worker says nothing
// about whether the model could carry the task, while an escalation says
// precisely that it could not. If these ever collapse into one arm, the two
// assertions below cannot both hold.
test fn escalation_and_infrastructure_retry_do_not_read_as_each_other() -> Bool {
let escalation_is_not_a_retry = match escalated_attempt.lineage {
InfrastructureRetry { prior_attempt: _, cause_receipt: _ } => false
_ => true
}
let retry_is_not_an_escalation = match retry_attempt.lineage {
CapabilityEscalation { prior_attempt: _, cause_receipt: _ } => false
_ => true
}
escalation_is_not_a_retry && retry_is_not_an_escalation
}

// A receipt carries the generation it was produced under, so a stale producer is
// distinguishable from a current one.

Expand Down
Loading