From dd6e20d29d2e57b0fd7fe2636b90f3e5e9a3997c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 27 Jun 2026 02:24:10 +0000 Subject: [PATCH 1/8] WIP: Model two-tier compute allocation in compute_fabric: unified heavy_compu --- dsl/product/compute_fabric.dag | 120 ++++++++++++++++++++++++++++++++- 1 file changed, 119 insertions(+), 1 deletion(-) diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index 80a4809a6b1..1b0f784321c 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -33,6 +33,7 @@ import std.measure { hardware_thread_count, hardware_thread_count_value, measure_scale_fraction_ceil, + measure_scale_fraction_floor, hertz, watt, Bandwidth, @@ -312,7 +313,7 @@ type ComputeSupplyFacts { type ProviderConstraint = HostJobserverFifo { fifo_path: NonEmptyStr, config_ref: CtrlJobserverConfig } | SharedHomeRoot { path: NonEmptyStr } - | MaxConcurrentRunners { cap: Int } + | MaxConcurrentHeavyComputeLanes { cap: Int } | OomBehavior { signal: OomSignalClass } type AvailabilityWindow { open: LogicalTime, close: LogicalTime? } @@ -799,6 +800,123 @@ fn satisfies(offer: ComputeOffer, demand: WorkDemand) -> ComputeLeaseEligibility } } +type DemandClass + = SessionClass + | HeavyComputeClass + +type ClassedWorkDemand { + demand_class: DemandClass + demand: WorkDemand +} + +type HeavyComputeLaneSource + = GithubCiRunner + | OnDemandSessionLease + +type HeavyWorkRoutability + = RoutableRemote + | NonRoutableLocal + +type HeavyWorkPlacement + = OffHostRemote + | LeasedLane { source: HeavyComputeLaneSource } + +fn heavy_work_placement(routability: HeavyWorkRoutability) -> HeavyWorkPlacement { + match routability { + RoutableRemote => OffHostRemote + NonRoutableLocal => LeasedLane { source: OnDemandSessionLease } + } +} + +type HeavyComputeLeaseId = NonEmptyStr where brand("HeavyComputeLeaseId") + +type LeaseReleaseTrigger + = LeaseExit + | LeaseTimeout + | SessionArchive + +type HeavyComputeLease { + lease_id: HeavyComputeLeaseId + source: HeavyComputeLaneSource + demand: WorkDemand + acquired_at: LogicalTime + max_hold: Duration +} + +type LeaseLedger { + held: List +} + +data empty_lease_ledger: LeaseLedger = LeaseLedger { held: [] } + +type HeavyComputePool { + lane_envelope: ResourceEnvelope + lane_count: Nat +} + +fn heavy_compute_lane_memory(pool: HeavyComputePool) -> ByteSize { + demand_envelope_memory(envelope: pool.lane_envelope) +} + +fn heavy_compute_pool_bytes(pool: HeavyComputePool) -> ByteSize { + measure_scale_fraction_floor(m: heavy_compute_lane_memory(pool: pool), num: pool.lane_count, den: 1) +} + +fn ledger_held_count(ledger: LeaseLedger) -> Nat { + fold(ledger.held, init: 0, f: (acc, _l) => acc + 1) +} + +fn ledger_has_free_lane(pool: HeavyComputePool, ledger: LeaseLedger) -> Bool { + ledger_held_count(ledger: ledger) < pool.lane_count +} + +fn ledger_conserves(pool: HeavyComputePool, ledger: LeaseLedger) -> Bool { + !(pool.lane_count < ledger_held_count(ledger: ledger)) +} + +type LeaseGrantOutcome + = LeaseGranted { ledger: LeaseLedger, granted: HeavyComputeLease } + | LeaseRejectedIneligible { reason: MissingDemandFact } + | LeaseRejectedPoolExhausted { lane_count: Nat, held: Nat } + +fn lease_grant( + pool: HeavyComputePool, + ledger: LeaseLedger, + offer: ComputeOffer, + lease_id: HeavyComputeLeaseId, + source: HeavyComputeLaneSource, + demand: WorkDemand, + acquired_at: LogicalTime, + max_hold: Duration +) -> LeaseGrantOutcome { + match satisfies(offer: offer, demand: demand) { + Rejected { reason: r } => LeaseRejectedIneligible { reason: r } + Eligible { witness: _w } => + if ledger_has_free_lane(pool: pool, ledger: ledger) { + let lease = HeavyComputeLease { + lease_id: lease_id, + source: source, + demand: demand, + acquired_at: acquired_at, + max_hold: max_hold, + } + LeaseGranted { + ledger: LeaseLedger { held: concat(ledger.held, [lease]) }, + granted: lease, + } + } else { + LeaseRejectedPoolExhausted { + lane_count: pool.lane_count, + held: ledger_held_count(ledger: ledger), + } + } + } +} + +fn lease_release(ledger: LeaseLedger, lease_id: HeavyComputeLeaseId) -> LeaseLedger { + LeaseLedger { held: filter(ledger.held, l => l.lease_id != lease_id) } +} + type WorkUnitId = NonEmptyStr where brand("WorkUnitId") type WorkUnit { From 8f5ef80dc7e2b1ce613a2e8885077a81007de0cc Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 27 Jun 2026 02:34:42 +0000 Subject: [PATCH 2/8] WIP: Model two-tier compute allocation in compute_fabric: unified heavy_compu --- dsl/product/compute_fabric.dag | 387 +++++++++++++++++- .../compute_fabric_resource_witness_test.dag | 24 ++ 2 files changed, 391 insertions(+), 20 deletions(-) diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index 1b0f784321c..88d9885d439 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -800,34 +800,52 @@ fn satisfies(offer: ComputeOffer, demand: WorkDemand) -> ComputeLeaseEligibility } } -type DemandClass - = SessionClass - | HeavyComputeClass +type ControlPlaneAgent + = ClaudeCode + | Codex + | Cursor -type ClassedWorkDemand { - demand_class: DemandClass - demand: WorkDemand +type SessionSubject { + agent: ControlPlaneAgent } -type HeavyComputeLaneSource - = GithubCiRunner - | OnDemandSessionLease +type ComputeLocality + = FulfillableRemotely + | MustRunLocal -type HeavyWorkRoutability - = RoutableRemote - | NonRoutableLocal +type ComputeRequest { + requester: SessionSubject + workload: WorkUnitId + needs: ResourceEnvelope + locality: ComputeLocality +} -type HeavyWorkPlacement - = OffHostRemote - | LeasedLane { source: HeavyComputeLaneSource } +type ExecutorTarget + = BuildBuddyRemote { endpoint: NonEmptyStr } + | LeasedComputeLane { lease_id: HeavyComputeLeaseId, host: HostIdentity } -fn heavy_work_placement(routability: HeavyWorkRoutability) -> HeavyWorkPlacement { - match routability { - RoutableRemote => OffHostRemote - NonRoutableLocal => LeasedLane { source: OnDemandSessionLease } - } +type RemoteExecutorHandle { + provider: ProviderIdentity + target: ExecutorTarget } +type FulfillmentRejection + = LocalCapacityExhausted { lane_count: Nat, held: Nat } + | NeedsUnsatisfiable { reason: MissingDemandFact } + +type Fulfillment + = Fulfilled { executor: RemoteExecutorHandle } + | FulfillmentRejected { reason: FulfillmentRejection } + +type FulfillmentOutcome { + fulfillment: Fulfillment + ledger: LeaseLedger +} + +type HeavyComputeLaneSource + = GithubCiRunner + | OnDemandSessionLease + type HeavyComputeLeaseId = NonEmptyStr where brand("HeavyComputeLeaseId") type LeaseReleaseTrigger @@ -917,6 +935,79 @@ fn lease_release(ledger: LeaseLedger, lease_id: HeavyComputeLeaseId) -> LeaseLed LeaseLedger { held: filter(ledger.held, l => l.lease_id != lease_id) } } +type ComputeFabric { + pool: HeavyComputePool + remote_executor: RemoteExecutorHandle + local_offer: ComputeOffer +} + +fn request_to_work_demand(request: ComputeRequest) -> WorkDemand { + WorkDemand { + resources: request.needs, + os: none, + isolation: IsolationRequirement { boundary: SharedHostHome }, + toolchains: [], + parallelism: SingleWorkItem, + data_locality: [], + effects: [], + input_envelope: EnvelopeUnknown, + } +} + +fn fulfill( + fabric: ComputeFabric, + ledger: LeaseLedger, + request: ComputeRequest, + lease_id: HeavyComputeLeaseId, + acquired_at: LogicalTime, + max_hold: Duration +) -> FulfillmentOutcome { + match request.locality { + FulfillableRemotely => + FulfillmentOutcome { + fulfillment: Fulfilled { executor: fabric.remote_executor }, + ledger: ledger, + } + MustRunLocal => + match lease_grant( + pool: fabric.pool, + ledger: ledger, + offer: fabric.local_offer, + lease_id: lease_id, + source: OnDemandSessionLease, + demand: request_to_work_demand(request: request), + acquired_at: acquired_at, + max_hold: max_hold + ) { + LeaseGranted { ledger: granted_ledger, granted: g } => + FulfillmentOutcome { + fulfillment: Fulfilled { + executor: RemoteExecutorHandle { + provider: fabric.local_offer.provider, + target: LeasedComputeLane { + lease_id: g.lease_id, + host: fabric.local_offer.supply.physical.identity, + }, + }, + }, + ledger: granted_ledger, + } + LeaseRejectedPoolExhausted { lane_count: lc, held: h } => + FulfillmentOutcome { + fulfillment: FulfillmentRejected { + reason: LocalCapacityExhausted { lane_count: lc, held: h }, + }, + ledger: ledger, + } + LeaseRejectedIneligible { reason: r } => + FulfillmentOutcome { + fulfillment: FulfillmentRejected { reason: NeedsUnsatisfiable { reason: r } }, + ledger: ledger, + } + } + } +} + type WorkUnitId = NonEmptyStr where brand("WorkUnitId") type WorkUnit { @@ -1475,3 +1566,259 @@ data gunbc_ci_corpus_envelope_ceiling_scaffold: Disposition = Scaffold { field: WholeDeclaration } } + +data heavy_compute_lane_work_demand: WorkDemand = WorkDemand { + resources: ResourceEnvelope { + cpu: Present { + value: CpuRequirement { min_threads: hardware_thread_count(16), architecture: none }, + }, + gpu: none, + memory: Present { value: MemoryRequirement { min_bytes: byte_size(34359738368) } }, + storage: none, + network: none, + }, + os: none, + isolation: IsolationRequirement { boundary: SharedHostHome }, + toolchains: [], + parallelism: SingleWorkItem, + data_locality: [], + effects: [], + input_envelope: EnvelopeUnknown, +} + +data example_heavy_compute_pool: HeavyComputePool = HeavyComputePool { + lane_envelope: heavy_compute_lane_work_demand.resources, + lane_count: 2, +} + +data example_lease_max_hold: Duration = Measure { count: 7200 } + +data example_session_subject: SessionSubject = SessionSubject { agent: ClaudeCode } + +data example_remote_executor: RemoteExecutorHandle = RemoteExecutorHandle { + provider: "buildbuddy-remote", + target: BuildBuddyRemote { endpoint: "grpcs://remote.buildbuddy.io" }, +} + +data example_compute_fabric: ComputeFabric = ComputeFabric { + pool: example_heavy_compute_pool, + remote_executor: example_remote_executor, + local_offer: example_resource_offer, +} + +data example_remote_request: ComputeRequest = ComputeRequest { + requester: example_session_subject, + workload: "cargo-build-workspace", + needs: heavy_compute_lane_work_demand.resources, + locality: FulfillableRemotely, +} + +data example_local_request: ComputeRequest = ComputeRequest { + requester: example_session_subject, + workload: "profile-typed-ast-byte-breakdown", + needs: heavy_compute_lane_work_demand.resources, + locality: MustRunLocal, +} + +data example_oversized_local_request: ComputeRequest = ComputeRequest { + requester: example_session_subject, + workload: "oversized-local", + needs: example_thread_work_demand.resources, + locality: MustRunLocal, +} + +fn witness_session_subject_is_control_plane_agent() -> Bool { + match example_session_subject.agent { + ClaudeCode => true + Codex => true + Cursor => true + } +} + +fn witness_remote_request_fulfilled_off_session() -> Bool { + let outcome = fulfill( + fabric: example_compute_fabric, + ledger: empty_lease_ledger, + request: example_remote_request, + lease_id: "unused-remote", + acquired_at: "t0", + max_hold: example_lease_max_hold + ) + match outcome.fulfillment { + Fulfilled { executor: e } => + match e.target { + BuildBuddyRemote { endpoint: _ } => ledger_held_count(ledger: outcome.ledger) == 0 + LeasedComputeLane { lease_id: _, host: _ } => false + } + FulfillmentRejected { reason: _ } => false + } +} + +fn witness_local_request_leases_a_lane() -> Bool { + let outcome = fulfill( + fabric: example_compute_fabric, + ledger: empty_lease_ledger, + request: example_local_request, + lease_id: "lease-local-1", + acquired_at: "t0", + max_hold: example_lease_max_hold + ) + match outcome.fulfillment { + Fulfilled { executor: e } => + match e.target { + LeasedComputeLane { lease_id: lid, host: _ } => + lid == "lease-local-1" && ledger_held_count(ledger: outcome.ledger) == 1 + BuildBuddyRemote { endpoint: _ } => false + } + FulfillmentRejected { reason: _ } => false + } +} + +fn witness_local_request_rejected_when_pool_exhausted() -> Bool { + let o1 = fulfill( + fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_local_request, + lease_id: "l1", acquired_at: "t0", max_hold: example_lease_max_hold + ) + let o2 = fulfill( + fabric: example_compute_fabric, ledger: o1.ledger, request: example_local_request, + lease_id: "l2", acquired_at: "t1", max_hold: example_lease_max_hold + ) + let o3 = fulfill( + fabric: example_compute_fabric, ledger: o2.ledger, request: example_local_request, + lease_id: "l3", acquired_at: "t2", max_hold: example_lease_max_hold + ) + match o3.fulfillment { + FulfillmentRejected { reason: r } => + match r { + LocalCapacityExhausted { lane_count: _, held: h } => + h == 2 && ledger_held_count(ledger: o3.ledger) == 2 + NeedsUnsatisfiable { reason: _ } => false + } + Fulfilled { executor: _ } => false + } +} + +fn witness_unsatisfiable_local_needs_rejected() -> Bool { + let outcome = fulfill( + fabric: example_compute_fabric, + ledger: empty_lease_ledger, + request: example_oversized_local_request, + lease_id: "oversized", + acquired_at: "t0", + max_hold: example_lease_max_hold + ) + match outcome.fulfillment { + FulfillmentRejected { reason: r } => + match r { + NeedsUnsatisfiable { reason: m } => m.dimension == DemandCpu + LocalCapacityExhausted { lane_count: _, held: _ } => false + } + Fulfilled { executor: _ } => false + } +} + +fn witness_heavy_pool_bytes_is_lanes_times_envelope() -> Bool { + byte_size_count(heavy_compute_pool_bytes(pool: example_heavy_compute_pool)) == 68719476736 +} + +fn witness_pool_unifies_ci_and_ondemand_then_rejects() -> Bool { + match lease_grant( + pool: example_heavy_compute_pool, + ledger: empty_lease_ledger, + offer: example_resource_offer, + lease_id: "ci-1", + source: GithubCiRunner, + demand: heavy_compute_lane_work_demand, + acquired_at: "t0", + max_hold: example_lease_max_hold + ) { + LeaseRejectedIneligible { reason: _ } => false + LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseGranted { ledger: l1, granted: _ } => + match lease_grant( + pool: example_heavy_compute_pool, + ledger: l1, + offer: example_resource_offer, + lease_id: "od-1", + source: OnDemandSessionLease, + demand: heavy_compute_lane_work_demand, + acquired_at: "t1", + max_hold: example_lease_max_hold + ) { + LeaseRejectedIneligible { reason: _ } => false + LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseGranted { ledger: l2, granted: _ } => + match lease_grant( + pool: example_heavy_compute_pool, + ledger: l2, + offer: example_resource_offer, + lease_id: "od-2", + source: OnDemandSessionLease, + demand: heavy_compute_lane_work_demand, + acquired_at: "t2", + max_hold: example_lease_max_hold + ) { + LeaseGranted { ledger: _, granted: _ } => false + LeaseRejectedIneligible { reason: _ } => false + LeaseRejectedPoolExhausted { lane_count: _, held: h } => + ledger_held_count(ledger: l2) == 2 && h == 2 + } + } + } +} + +fn witness_lease_release_frees_lane() -> Bool { + match lease_grant( + pool: example_heavy_compute_pool, + ledger: empty_lease_ledger, + offer: example_resource_offer, + lease_id: "rel-1", + source: GithubCiRunner, + demand: heavy_compute_lane_work_demand, + acquired_at: "t0", + max_hold: example_lease_max_hold + ) { + LeaseRejectedIneligible { reason: _ } => false + LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseGranted { ledger: l1, granted: _ } => { + let l2 = lease_release(ledger: l1, lease_id: "rel-1") + ledger_held_count(ledger: l1) == 1 + && ledger_held_count(ledger: l2) == 0 + && ledger_has_free_lane(pool: example_heavy_compute_pool, ledger: l2) + } + } +} + +fn witness_full_ledger_conserves_with_no_free_lane() -> Bool { + match lease_grant( + pool: example_heavy_compute_pool, + ledger: empty_lease_ledger, + offer: example_resource_offer, + lease_id: "ci-1", + source: GithubCiRunner, + demand: heavy_compute_lane_work_demand, + acquired_at: "t0", + max_hold: example_lease_max_hold + ) { + LeaseRejectedIneligible { reason: _ } => false + LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseGranted { ledger: l1, granted: _ } => + match lease_grant( + pool: example_heavy_compute_pool, + ledger: l1, + offer: example_resource_offer, + lease_id: "od-1", + source: OnDemandSessionLease, + demand: heavy_compute_lane_work_demand, + acquired_at: "t1", + max_hold: example_lease_max_hold + ) { + LeaseRejectedIneligible { reason: _ } => false + LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseGranted { ledger: l2, granted: _ } => + ledger_conserves(pool: example_heavy_compute_pool, ledger: l2) + && !ledger_has_free_lane(pool: example_heavy_compute_pool, ledger: l2) + && ledger_held_count(ledger: l2) == 2 + } + } +} diff --git a/dsl/test/claim/compute_fabric_resource_witness_test.dag b/dsl/test/claim/compute_fabric_resource_witness_test.dag index ca14963d86e..705e597cf59 100644 --- a/dsl/test/claim/compute_fabric_resource_witness_test.dag +++ b/dsl/test/claim/compute_fabric_resource_witness_test.dag @@ -8,6 +8,15 @@ import product.compute_fabric { witness_high_demand_shrinks_envelope_and_fits, witness_fail_open_memory_blind_demand_exceeds_budget, witness_unreadable_budget_uses_conservative_demand, + witness_session_subject_is_control_plane_agent, + witness_remote_request_fulfilled_off_session, + witness_local_request_leases_a_lane, + witness_local_request_rejected_when_pool_exhausted, + witness_unsatisfiable_local_needs_rejected, + witness_heavy_pool_bytes_is_lanes_times_envelope, + witness_pool_unifies_ci_and_ondemand_then_rejects, + witness_lease_release_frees_lane, + witness_full_ledger_conserves_with_no_free_lane, } test fn compute_fabric_resource_feasibility_holds() -> Bool { @@ -22,3 +31,18 @@ test fn ci_floor_run_demand_envelope_model_holds() -> Bool { && witness_fail_open_memory_blind_demand_exceeds_budget() && witness_unreadable_budget_uses_conservative_demand() } + +test fn compute_request_fulfillment_interface_holds() -> Bool { + witness_session_subject_is_control_plane_agent() + && witness_remote_request_fulfilled_off_session() + && witness_local_request_leases_a_lane() + && witness_local_request_rejected_when_pool_exhausted() + && witness_unsatisfiable_local_needs_rejected() +} + +test fn fulfillment_internals_conserve_the_pool() -> Bool { + witness_heavy_pool_bytes_is_lanes_times_envelope() + && witness_pool_unifies_ci_and_ondemand_then_rejects() + && witness_lease_release_frees_lane() + && witness_full_ledger_conserves_with_no_free_lane() +} From e8b408ad0c7da319368a1802df452da007c2f3f4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 27 Jun 2026 02:45:14 +0000 Subject: [PATCH 3/8] WIP: Model two-tier compute allocation in compute_fabric: unified heavy_compu --- dsl/product/compute_fabric.dag | 111 ++++++++++++++++-- .../compute_fabric_resource_witness_test.dag | 9 ++ 2 files changed, 110 insertions(+), 10 deletions(-) diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index 88d9885d439..7842a44bdde 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -813,9 +813,13 @@ type ComputeLocality = FulfillableRemotely | MustRunLocal +type ComputeWorkload + = ExecCommand { command: NonEmptyStr } + | GhaRunner { repo: NonEmptyStr, labels: List } + type ComputeRequest { requester: SessionSubject - workload: WorkUnitId + workload: ComputeWorkload needs: ResourceEnvelope locality: ComputeLocality } @@ -835,6 +839,7 @@ type FulfillmentRejection type Fulfillment = Fulfilled { executor: RemoteExecutorHandle } + | FulfillmentQueued { lane_count: Nat, held: Nat } | FulfillmentRejected { reason: FulfillmentRejection } type FulfillmentOutcome { @@ -941,6 +946,13 @@ type ComputeFabric { local_offer: ComputeOffer } +fn workload_lease_source(workload: ComputeWorkload) -> HeavyComputeLaneSource { + match workload { + ExecCommand { command: _ } => OnDemandSessionLease + GhaRunner { repo: _, labels: _ } => GithubCiRunner + } +} + fn request_to_work_demand(request: ComputeRequest) -> WorkDemand { WorkDemand { resources: request.needs, @@ -974,7 +986,7 @@ fn fulfill( ledger: ledger, offer: fabric.local_offer, lease_id: lease_id, - source: OnDemandSessionLease, + source: workload_lease_source(workload: request.workload), demand: request_to_work_demand(request: request), acquired_at: acquired_at, max_hold: max_hold @@ -993,11 +1005,19 @@ fn fulfill( ledger: granted_ledger, } LeaseRejectedPoolExhausted { lane_count: lc, held: h } => - FulfillmentOutcome { - fulfillment: FulfillmentRejected { - reason: LocalCapacityExhausted { lane_count: lc, held: h }, - }, - ledger: ledger, + match request.workload { + GhaRunner { repo: _, labels: _ } => + FulfillmentOutcome { + fulfillment: FulfillmentQueued { lane_count: lc, held: h }, + ledger: ledger, + } + ExecCommand { command: _ } => + FulfillmentOutcome { + fulfillment: FulfillmentRejected { + reason: LocalCapacityExhausted { lane_count: lc, held: h }, + }, + ledger: ledger, + } } LeaseRejectedIneligible { reason: r } => FulfillmentOutcome { @@ -1608,25 +1628,32 @@ data example_compute_fabric: ComputeFabric = ComputeFabric { data example_remote_request: ComputeRequest = ComputeRequest { requester: example_session_subject, - workload: "cargo-build-workspace", + workload: ExecCommand { command: "cargo build --workspace" }, needs: heavy_compute_lane_work_demand.resources, locality: FulfillableRemotely, } data example_local_request: ComputeRequest = ComputeRequest { requester: example_session_subject, - workload: "profile-typed-ast-byte-breakdown", + workload: ExecCommand { command: "profile_typed_ast_byte_breakdown" }, needs: heavy_compute_lane_work_demand.resources, locality: MustRunLocal, } data example_oversized_local_request: ComputeRequest = ComputeRequest { requester: example_session_subject, - workload: "oversized-local", + workload: ExecCommand { command: "oversized-local" }, needs: example_thread_work_demand.resources, locality: MustRunLocal, } +data example_gha_runner_request: ComputeRequest = ComputeRequest { + requester: example_session_subject, + workload: GhaRunner { repo: "gunb-ai/gunbc", labels: ["self-hosted", "srv1"] }, + needs: heavy_compute_lane_work_demand.resources, + locality: MustRunLocal, +} + fn witness_session_subject_is_control_plane_agent() -> Bool { match example_session_subject.agent { ClaudeCode => true @@ -1650,6 +1677,7 @@ fn witness_remote_request_fulfilled_off_session() -> Bool { BuildBuddyRemote { endpoint: _ } => ledger_held_count(ledger: outcome.ledger) == 0 LeasedComputeLane { lease_id: _, host: _ } => false } + FulfillmentQueued { lane_count: _, held: _ } => false FulfillmentRejected { reason: _ } => false } } @@ -1670,6 +1698,7 @@ fn witness_local_request_leases_a_lane() -> Bool { lid == "lease-local-1" && ledger_held_count(ledger: outcome.ledger) == 1 BuildBuddyRemote { endpoint: _ } => false } + FulfillmentQueued { lane_count: _, held: _ } => false FulfillmentRejected { reason: _ } => false } } @@ -1695,6 +1724,7 @@ fn witness_local_request_rejected_when_pool_exhausted() -> Bool { NeedsUnsatisfiable { reason: _ } => false } Fulfilled { executor: _ } => false + FulfillmentQueued { lane_count: _, held: _ } => false } } @@ -1714,6 +1744,67 @@ fn witness_unsatisfiable_local_needs_rejected() -> Bool { LocalCapacityExhausted { lane_count: _, held: _ } => false } Fulfilled { executor: _ } => false + FulfillmentQueued { lane_count: _, held: _ } => false + } +} + +fn witness_gha_runner_request_leases_same_lane_as_exec() -> Bool { + let exec_outcome = fulfill( + fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_local_request, + lease_id: "exec-1", acquired_at: "t0", max_hold: example_lease_max_hold + ) + let runner_outcome = fulfill( + fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_gha_runner_request, + lease_id: "runner-1", acquired_at: "t0", max_hold: example_lease_max_hold + ) + let same_envelope = + work_demand_content_digest(demand: request_to_work_demand(request: example_local_request)) + == work_demand_content_digest(demand: request_to_work_demand(request: example_gha_runner_request)) + match exec_outcome.fulfillment { + Fulfilled { executor: ee } => + match runner_outcome.fulfillment { + Fulfilled { executor: re } => + match ee.target { + LeasedComputeLane { lease_id: _, host: eh } => + match re.target { + LeasedComputeLane { lease_id: _, host: rh } => eh == rh && same_envelope + BuildBuddyRemote { endpoint: _ } => false + } + BuildBuddyRemote { endpoint: _ } => false + } + FulfillmentQueued { lane_count: _, held: _ } => false + FulfillmentRejected { reason: _ } => false + } + FulfillmentQueued { lane_count: _, held: _ } => false + FulfillmentRejected { reason: _ } => false + } +} + +fn witness_gha_runner_queues_when_pool_exhausted_not_rejects() -> Bool { + let o1 = fulfill( + fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_local_request, + lease_id: "l1", acquired_at: "t0", max_hold: example_lease_max_hold + ) + let o2 = fulfill( + fabric: example_compute_fabric, ledger: o1.ledger, request: example_local_request, + lease_id: "l2", acquired_at: "t1", max_hold: example_lease_max_hold + ) + let o3 = fulfill( + fabric: example_compute_fabric, ledger: o2.ledger, request: example_gha_runner_request, + lease_id: "runner-overflow", acquired_at: "t2", max_hold: example_lease_max_hold + ) + match o3.fulfillment { + FulfillmentQueued { lane_count: _, held: h } => + h == 2 && ledger_held_count(ledger: o3.ledger) == 2 + Fulfilled { executor: _ } => false + FulfillmentRejected { reason: _ } => false + } +} + +fn witness_gha_runner_uses_ci_lane_source() -> Bool { + match workload_lease_source(workload: GhaRunner { repo: "gunb-ai/gunbc", labels: [] }) { + GithubCiRunner => true + OnDemandSessionLease => false } } diff --git a/dsl/test/claim/compute_fabric_resource_witness_test.dag b/dsl/test/claim/compute_fabric_resource_witness_test.dag index 705e597cf59..2620357e360 100644 --- a/dsl/test/claim/compute_fabric_resource_witness_test.dag +++ b/dsl/test/claim/compute_fabric_resource_witness_test.dag @@ -13,6 +13,9 @@ import product.compute_fabric { witness_local_request_leases_a_lane, witness_local_request_rejected_when_pool_exhausted, witness_unsatisfiable_local_needs_rejected, + witness_gha_runner_request_leases_same_lane_as_exec, + witness_gha_runner_queues_when_pool_exhausted_not_rejects, + witness_gha_runner_uses_ci_lane_source, witness_heavy_pool_bytes_is_lanes_times_envelope, witness_pool_unifies_ci_and_ondemand_then_rejects, witness_lease_release_frees_lane, @@ -40,6 +43,12 @@ test fn compute_request_fulfillment_interface_holds() -> Bool { && witness_unsatisfiable_local_needs_rejected() } +test fn gha_runner_is_same_request_on_one_ledger() -> Bool { + witness_gha_runner_request_leases_same_lane_as_exec() + && witness_gha_runner_queues_when_pool_exhausted_not_rejects() + && witness_gha_runner_uses_ci_lane_source() +} + test fn fulfillment_internals_conserve_the_pool() -> Bool { witness_heavy_pool_bytes_is_lanes_times_envelope() && witness_pool_unifies_ci_and_ondemand_then_rejects() From 77f0116f9724a07497d6f181dfa56acca9fe2b8d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 27 Jun 2026 02:57:18 +0000 Subject: [PATCH 4/8] WIP: Model two-tier compute allocation in compute_fabric: unified heavy_compu --- dsl/product/compute_fabric.dag | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index 7842a44bdde..e9801651323 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -1757,9 +1757,7 @@ fn witness_gha_runner_request_leases_same_lane_as_exec() -> Bool { fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_gha_runner_request, lease_id: "runner-1", acquired_at: "t0", max_hold: example_lease_max_hold ) - let same_envelope = - work_demand_content_digest(demand: request_to_work_demand(request: example_local_request)) - == work_demand_content_digest(demand: request_to_work_demand(request: example_gha_runner_request)) + let same_envelope = work_demand_content_digest(demand: request_to_work_demand(request: example_local_request)) == work_demand_content_digest(demand: request_to_work_demand(request: example_gha_runner_request)) match exec_outcome.fulfillment { Fulfilled { executor: ee } => match runner_outcome.fulfillment { From 95fc0a7304b3e394d5a4e642257810288bf3f956 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 27 Jun 2026 03:07:47 +0000 Subject: [PATCH 5/8] WIP: Model two-tier compute allocation in compute_fabric: unified heavy_compu --- dsl/product/compute_fabric.dag | 119 ++++++++++++++++++--------------- 1 file changed, 64 insertions(+), 55 deletions(-) diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index e9801651323..c7b1461736c 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -853,17 +853,10 @@ type HeavyComputeLaneSource type HeavyComputeLeaseId = NonEmptyStr where brand("HeavyComputeLeaseId") -type LeaseReleaseTrigger - = LeaseExit - | LeaseTimeout - | SessionArchive - type HeavyComputeLease { lease_id: HeavyComputeLeaseId source: HeavyComputeLaneSource demand: WorkDemand - acquired_at: LogicalTime - max_hold: Duration } type LeaseLedger { @@ -889,6 +882,29 @@ fn ledger_held_count(ledger: LeaseLedger) -> Nat { fold(ledger.held, init: 0, f: (acc, _l) => acc + 1) } +fn ledger_holds_source(ledger: LeaseLedger, source: HeavyComputeLaneSource) -> Bool { + fold( + ledger.held, + init: false, + f: (acc, l) => acc || lease_source_eq(a: l.source, b: source) + ) +} + +fn lease_source_eq(a: HeavyComputeLaneSource, b: HeavyComputeLaneSource) -> Bool { + match a { + GithubCiRunner => + match b { + GithubCiRunner => true + OnDemandSessionLease => false + } + OnDemandSessionLease => + match b { + OnDemandSessionLease => true + GithubCiRunner => false + } + } +} + fn ledger_has_free_lane(pool: HeavyComputePool, ledger: LeaseLedger) -> Bool { ledger_held_count(ledger: ledger) < pool.lane_count } @@ -908,9 +924,7 @@ fn lease_grant( offer: ComputeOffer, lease_id: HeavyComputeLeaseId, source: HeavyComputeLaneSource, - demand: WorkDemand, - acquired_at: LogicalTime, - max_hold: Duration + demand: WorkDemand ) -> LeaseGrantOutcome { match satisfies(offer: offer, demand: demand) { Rejected { reason: r } => LeaseRejectedIneligible { reason: r } @@ -920,8 +934,6 @@ fn lease_grant( lease_id: lease_id, source: source, demand: demand, - acquired_at: acquired_at, - max_hold: max_hold, } LeaseGranted { ledger: LeaseLedger { held: concat(ledger.held, [lease]) }, @@ -970,9 +982,7 @@ fn fulfill( fabric: ComputeFabric, ledger: LeaseLedger, request: ComputeRequest, - lease_id: HeavyComputeLeaseId, - acquired_at: LogicalTime, - max_hold: Duration + lease_id: HeavyComputeLeaseId ) -> FulfillmentOutcome { match request.locality { FulfillableRemotely => @@ -987,9 +997,7 @@ fn fulfill( offer: fabric.local_offer, lease_id: lease_id, source: workload_lease_source(workload: request.workload), - demand: request_to_work_demand(request: request), - acquired_at: acquired_at, - max_hold: max_hold + demand: request_to_work_demand(request: request) ) { LeaseGranted { ledger: granted_ledger, granted: g } => FulfillmentOutcome { @@ -1611,7 +1619,23 @@ data example_heavy_compute_pool: HeavyComputePool = HeavyComputePool { lane_count: 2, } -data example_lease_max_hold: Duration = Measure { count: 7200 } +data control_plane_agent_vendor_scaffold: Disposition = Scaffold { + dissolves_to: SingleAuthority, + bind: DeclarationRef { + module_path: "extdeps.vendor", + decl_name: "Vendor", + field: WholeDeclaration + } +} + +data heavy_compute_pool_lane_count_projection_scaffold: Disposition = Scaffold { + dissolves_to: SingleAuthority, + bind: DeclarationRef { + module_path: "gunbc.fleet_host_budget", + decl_name: "fleet_host_plan_for_offer", + field: WholeDeclaration + } +} data example_session_subject: SessionSubject = SessionSubject { agent: ClaudeCode } @@ -1667,9 +1691,7 @@ fn witness_remote_request_fulfilled_off_session() -> Bool { fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_remote_request, - lease_id: "unused-remote", - acquired_at: "t0", - max_hold: example_lease_max_hold + lease_id: "unused-remote" ) match outcome.fulfillment { Fulfilled { executor: e } => @@ -1687,9 +1709,7 @@ fn witness_local_request_leases_a_lane() -> Bool { fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_local_request, - lease_id: "lease-local-1", - acquired_at: "t0", - max_hold: example_lease_max_hold + lease_id: "lease-local-1" ) match outcome.fulfillment { Fulfilled { executor: e } => @@ -1706,15 +1726,15 @@ fn witness_local_request_leases_a_lane() -> Bool { fn witness_local_request_rejected_when_pool_exhausted() -> Bool { let o1 = fulfill( fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_local_request, - lease_id: "l1", acquired_at: "t0", max_hold: example_lease_max_hold + lease_id: "l1" ) let o2 = fulfill( fabric: example_compute_fabric, ledger: o1.ledger, request: example_local_request, - lease_id: "l2", acquired_at: "t1", max_hold: example_lease_max_hold + lease_id: "l2" ) let o3 = fulfill( fabric: example_compute_fabric, ledger: o2.ledger, request: example_local_request, - lease_id: "l3", acquired_at: "t2", max_hold: example_lease_max_hold + lease_id: "l3" ) match o3.fulfillment { FulfillmentRejected { reason: r } => @@ -1733,9 +1753,7 @@ fn witness_unsatisfiable_local_needs_rejected() -> Bool { fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_oversized_local_request, - lease_id: "oversized", - acquired_at: "t0", - max_hold: example_lease_max_hold + lease_id: "oversized" ) match outcome.fulfillment { FulfillmentRejected { reason: r } => @@ -1751,11 +1769,11 @@ fn witness_unsatisfiable_local_needs_rejected() -> Bool { fn witness_gha_runner_request_leases_same_lane_as_exec() -> Bool { let exec_outcome = fulfill( fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_local_request, - lease_id: "exec-1", acquired_at: "t0", max_hold: example_lease_max_hold + lease_id: "exec-1" ) let runner_outcome = fulfill( fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_gha_runner_request, - lease_id: "runner-1", acquired_at: "t0", max_hold: example_lease_max_hold + lease_id: "runner-1" ) let same_envelope = work_demand_content_digest(demand: request_to_work_demand(request: example_local_request)) == work_demand_content_digest(demand: request_to_work_demand(request: example_gha_runner_request)) match exec_outcome.fulfillment { @@ -1781,15 +1799,15 @@ fn witness_gha_runner_request_leases_same_lane_as_exec() -> Bool { fn witness_gha_runner_queues_when_pool_exhausted_not_rejects() -> Bool { let o1 = fulfill( fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_local_request, - lease_id: "l1", acquired_at: "t0", max_hold: example_lease_max_hold + lease_id: "l1" ) let o2 = fulfill( fabric: example_compute_fabric, ledger: o1.ledger, request: example_local_request, - lease_id: "l2", acquired_at: "t1", max_hold: example_lease_max_hold + lease_id: "l2" ) let o3 = fulfill( fabric: example_compute_fabric, ledger: o2.ledger, request: example_gha_runner_request, - lease_id: "runner-overflow", acquired_at: "t2", max_hold: example_lease_max_hold + lease_id: "runner-overflow" ) match o3.fulfillment { FulfillmentQueued { lane_count: _, held: h } => @@ -1817,9 +1835,7 @@ fn witness_pool_unifies_ci_and_ondemand_then_rejects() -> Bool { offer: example_resource_offer, lease_id: "ci-1", source: GithubCiRunner, - demand: heavy_compute_lane_work_demand, - acquired_at: "t0", - max_hold: example_lease_max_hold + demand: heavy_compute_lane_work_demand ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false @@ -1830,9 +1846,7 @@ fn witness_pool_unifies_ci_and_ondemand_then_rejects() -> Bool { offer: example_resource_offer, lease_id: "od-1", source: OnDemandSessionLease, - demand: heavy_compute_lane_work_demand, - acquired_at: "t1", - max_hold: example_lease_max_hold + demand: heavy_compute_lane_work_demand ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false @@ -1843,14 +1857,15 @@ fn witness_pool_unifies_ci_and_ondemand_then_rejects() -> Bool { offer: example_resource_offer, lease_id: "od-2", source: OnDemandSessionLease, - demand: heavy_compute_lane_work_demand, - acquired_at: "t2", - max_hold: example_lease_max_hold + demand: heavy_compute_lane_work_demand ) { LeaseGranted { ledger: _, granted: _ } => false LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: h } => - ledger_held_count(ledger: l2) == 2 && h == 2 + ledger_held_count(ledger: l2) == 2 + && h == 2 + && ledger_holds_source(ledger: l2, source: GithubCiRunner) + && ledger_holds_source(ledger: l2, source: OnDemandSessionLease) } } } @@ -1863,9 +1878,7 @@ fn witness_lease_release_frees_lane() -> Bool { offer: example_resource_offer, lease_id: "rel-1", source: GithubCiRunner, - demand: heavy_compute_lane_work_demand, - acquired_at: "t0", - max_hold: example_lease_max_hold + demand: heavy_compute_lane_work_demand ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false @@ -1885,9 +1898,7 @@ fn witness_full_ledger_conserves_with_no_free_lane() -> Bool { offer: example_resource_offer, lease_id: "ci-1", source: GithubCiRunner, - demand: heavy_compute_lane_work_demand, - acquired_at: "t0", - max_hold: example_lease_max_hold + demand: heavy_compute_lane_work_demand ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false @@ -1898,9 +1909,7 @@ fn witness_full_ledger_conserves_with_no_free_lane() -> Bool { offer: example_resource_offer, lease_id: "od-1", source: OnDemandSessionLease, - demand: heavy_compute_lane_work_demand, - acquired_at: "t1", - max_hold: example_lease_max_hold + demand: heavy_compute_lane_work_demand ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false From 83ec75821f9138e6e776681cd618d52e487f74da Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 27 Jun 2026 03:20:04 +0000 Subject: [PATCH 6/8] Review polish: fold lease_source_eq into substrate == (coproduct equality lifts) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit claude-opus-4-7 #5866: == lifts over the HeavyComputeLaneSource coproduct (verified by execution), so the hand-rolled 2-variant equality predicate is the DESIGN §5 predicate-dissolution shape — replaced with l.source == source. Witnesses re-run green. Co-Authored-By: Claude Opus 4.8 --- dsl/product/compute_fabric.dag | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index c7b1461736c..aa2e37e6e23 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -886,25 +886,10 @@ fn ledger_holds_source(ledger: LeaseLedger, source: HeavyComputeLaneSource) -> B fold( ledger.held, init: false, - f: (acc, l) => acc || lease_source_eq(a: l.source, b: source) + f: (acc, l) => acc || l.source == source ) } -fn lease_source_eq(a: HeavyComputeLaneSource, b: HeavyComputeLaneSource) -> Bool { - match a { - GithubCiRunner => - match b { - GithubCiRunner => true - OnDemandSessionLease => false - } - OnDemandSessionLease => - match b { - OnDemandSessionLease => true - GithubCiRunner => false - } - } -} - fn ledger_has_free_lane(pool: HeavyComputePool, ledger: LeaseLedger) -> Bool { ledger_held_count(ledger: ledger) < pool.lane_count } From 60c23d4f8303b72aae5e70ae21c6656c223350e0 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 27 Jun 2026 03:30:15 +0000 Subject: [PATCH 7/8] WIP: Model two-tier compute allocation in compute_fabric: unified heavy_compu --- dsl/product/compute_fabric.dag | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index aa2e37e6e23..10288d1553f 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -836,6 +836,7 @@ type RemoteExecutorHandle { type FulfillmentRejection = LocalCapacityExhausted { lane_count: Nat, held: Nat } | NeedsUnsatisfiable { reason: MissingDemandFact } + | DuplicateLeaseId { lease_id: HeavyComputeLeaseId } type Fulfillment = Fulfilled { executor: RemoteExecutorHandle } @@ -894,6 +895,10 @@ fn ledger_has_free_lane(pool: HeavyComputePool, ledger: LeaseLedger) -> Bool { ledger_held_count(ledger: ledger) < pool.lane_count } +fn ledger_has_lease_id(ledger: LeaseLedger, lease_id: HeavyComputeLeaseId) -> Bool { + fold(ledger.held, init: false, f: (acc, l) => acc || l.lease_id == lease_id) +} + fn ledger_conserves(pool: HeavyComputePool, ledger: LeaseLedger) -> Bool { !(pool.lane_count < ledger_held_count(ledger: ledger)) } @@ -902,6 +907,7 @@ type LeaseGrantOutcome = LeaseGranted { ledger: LeaseLedger, granted: HeavyComputeLease } | LeaseRejectedIneligible { reason: MissingDemandFact } | LeaseRejectedPoolExhausted { lane_count: Nat, held: Nat } + | LeaseRejectedDuplicateId { lease_id: HeavyComputeLeaseId } fn lease_grant( pool: HeavyComputePool, @@ -914,7 +920,9 @@ fn lease_grant( match satisfies(offer: offer, demand: demand) { Rejected { reason: r } => LeaseRejectedIneligible { reason: r } Eligible { witness: _w } => - if ledger_has_free_lane(pool: pool, ledger: ledger) { + if ledger_has_lease_id(ledger: ledger, lease_id: lease_id) { + LeaseRejectedDuplicateId { lease_id: lease_id } + } else if ledger_has_free_lane(pool: pool, ledger: ledger) { let lease = HeavyComputeLease { lease_id: lease_id, source: source, From 2b2a5de236e46712b8f536f48a31dda6cc99852f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 27 Jun 2026 03:32:54 +0000 Subject: [PATCH 8/8] Address review (claude-opus-4-7 #2): fail-closed on duplicate lease_id + BuildBuddy vendor scaffold MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - lease_grant now rejects a duplicate lease_id (LeaseRejectedDuplicateId) instead of silently double-booking a lane (DESIGN §5 fail-open -> fail-closed); fulfill maps it to FulfillmentRejected{DuplicateLeaseId}. New discriminating witness witness_duplicate_lease_id_rejected_fail_closed (2nd grant of same id -> rejected, ledger still holds 1). - ExecutorTarget BuildBuddyRemote: add buildbuddy_remote_executor_vendor_scaffold (DESIGN §3, parallel to control_plane_agent_vendor_scaffold). - All LeaseGrantOutcome / FulfillmentRejection matches made exhaustive over the new variants. Witnesses re-run green by execution. Co-Authored-By: Claude Opus 4.8 --- dsl/product/compute_fabric.dag | 44 +++++++++++++++++++ .../compute_fabric_resource_witness_test.dag | 2 + 2 files changed, 46 insertions(+) diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index 10288d1553f..12bd9bfeb3c 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -1025,6 +1025,11 @@ fn fulfill( fulfillment: FulfillmentRejected { reason: NeedsUnsatisfiable { reason: r } }, ledger: ledger, } + LeaseRejectedDuplicateId { lease_id: dup } => + FulfillmentOutcome { + fulfillment: FulfillmentRejected { reason: DuplicateLeaseId { lease_id: dup } }, + ledger: ledger, + } } } } @@ -1630,6 +1635,15 @@ data heavy_compute_pool_lane_count_projection_scaffold: Disposition = Scaffold { } } +data buildbuddy_remote_executor_vendor_scaffold: Disposition = Scaffold { + dissolves_to: SingleAuthority, + bind: DeclarationRef { + module_path: "extdeps.vendor", + decl_name: "Vendor", + field: WholeDeclaration + } +} + data example_session_subject: SessionSubject = SessionSubject { agent: ClaudeCode } data example_remote_executor: RemoteExecutorHandle = RemoteExecutorHandle { @@ -1735,6 +1749,7 @@ fn witness_local_request_rejected_when_pool_exhausted() -> Bool { LocalCapacityExhausted { lane_count: _, held: h } => h == 2 && ledger_held_count(ledger: o3.ledger) == 2 NeedsUnsatisfiable { reason: _ } => false + DuplicateLeaseId { lease_id: _ } => false } Fulfilled { executor: _ } => false FulfillmentQueued { lane_count: _, held: _ } => false @@ -1753,6 +1768,7 @@ fn witness_unsatisfiable_local_needs_rejected() -> Bool { match r { NeedsUnsatisfiable { reason: m } => m.dimension == DemandCpu LocalCapacityExhausted { lane_count: _, held: _ } => false + DuplicateLeaseId { lease_id: _ } => false } Fulfilled { executor: _ } => false FulfillmentQueued { lane_count: _, held: _ } => false @@ -1832,6 +1848,7 @@ fn witness_pool_unifies_ci_and_ondemand_then_rejects() -> Bool { ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseRejectedDuplicateId { lease_id: _ } => false LeaseGranted { ledger: l1, granted: _ } => match lease_grant( pool: example_heavy_compute_pool, @@ -1843,6 +1860,7 @@ fn witness_pool_unifies_ci_and_ondemand_then_rejects() -> Bool { ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseRejectedDuplicateId { lease_id: _ } => false LeaseGranted { ledger: l2, granted: _ } => match lease_grant( pool: example_heavy_compute_pool, @@ -1854,6 +1872,7 @@ fn witness_pool_unifies_ci_and_ondemand_then_rejects() -> Bool { ) { LeaseGranted { ledger: _, granted: _ } => false LeaseRejectedIneligible { reason: _ } => false + LeaseRejectedDuplicateId { lease_id: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: h } => ledger_held_count(ledger: l2) == 2 && h == 2 @@ -1875,6 +1894,7 @@ fn witness_lease_release_frees_lane() -> Bool { ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseRejectedDuplicateId { lease_id: _ } => false LeaseGranted { ledger: l1, granted: _ } => { let l2 = lease_release(ledger: l1, lease_id: "rel-1") ledger_held_count(ledger: l1) == 1 @@ -1895,6 +1915,7 @@ fn witness_full_ledger_conserves_with_no_free_lane() -> Bool { ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseRejectedDuplicateId { lease_id: _ } => false LeaseGranted { ledger: l1, granted: _ } => match lease_grant( pool: example_heavy_compute_pool, @@ -1906,6 +1927,7 @@ fn witness_full_ledger_conserves_with_no_free_lane() -> Bool { ) { LeaseRejectedIneligible { reason: _ } => false LeaseRejectedPoolExhausted { lane_count: _, held: _ } => false + LeaseRejectedDuplicateId { lease_id: _ } => false LeaseGranted { ledger: l2, granted: _ } => ledger_conserves(pool: example_heavy_compute_pool, ledger: l2) && !ledger_has_free_lane(pool: example_heavy_compute_pool, ledger: l2) @@ -1913,3 +1935,25 @@ fn witness_full_ledger_conserves_with_no_free_lane() -> Bool { } } } + +fn witness_duplicate_lease_id_rejected_fail_closed() -> Bool { + let o1 = fulfill( + fabric: example_compute_fabric, ledger: empty_lease_ledger, request: example_local_request, + lease_id: "dup-1" + ) + let o2 = fulfill( + fabric: example_compute_fabric, ledger: o1.ledger, request: example_local_request, + lease_id: "dup-1" + ) + match o2.fulfillment { + FulfillmentRejected { reason: r } => + match r { + DuplicateLeaseId { lease_id: lid } => + lid == "dup-1" && ledger_held_count(ledger: o2.ledger) == 1 + LocalCapacityExhausted { lane_count: _, held: _ } => false + NeedsUnsatisfiable { reason: _ } => false + } + Fulfilled { executor: _ } => false + FulfillmentQueued { lane_count: _, held: _ } => false + } +} diff --git a/dsl/test/claim/compute_fabric_resource_witness_test.dag b/dsl/test/claim/compute_fabric_resource_witness_test.dag index 2620357e360..cee2fe6d04b 100644 --- a/dsl/test/claim/compute_fabric_resource_witness_test.dag +++ b/dsl/test/claim/compute_fabric_resource_witness_test.dag @@ -13,6 +13,7 @@ import product.compute_fabric { witness_local_request_leases_a_lane, witness_local_request_rejected_when_pool_exhausted, witness_unsatisfiable_local_needs_rejected, + witness_duplicate_lease_id_rejected_fail_closed, witness_gha_runner_request_leases_same_lane_as_exec, witness_gha_runner_queues_when_pool_exhausted_not_rejects, witness_gha_runner_uses_ci_lane_source, @@ -41,6 +42,7 @@ test fn compute_request_fulfillment_interface_holds() -> Bool { && witness_local_request_leases_a_lane() && witness_local_request_rejected_when_pool_exhausted() && witness_unsatisfiable_local_needs_rejected() + && witness_duplicate_lease_id_rejected_fail_closed() } test fn gha_runner_is_same_request_on_one_ledger() -> Bool {