Skip to content

Model compute_fabric request→fulfillment interface: ComputeRequest (exec | gha_runner) → Fulfillment, one lease ledger (ctrl rev3 / #1838) - #5866

Closed
briansrls wants to merge 10 commits into
mainfrom
session/fierce-seal-909
Closed

briansrls wants to merge 10 commits into
mainfrom
session/fierce-seal-909

Conversation

@briansrls

@briansrls briansrls commented Jun 27, 2026 •

Copy link
Copy Markdown
Contributor

What

gunbc-side single-authority model for session compute allocation (ctrl design rev3, PR gunb-ai/ctrl#1838). compute_fabric gains a request → fulfillment interface; pool/lane/conservation are private fulfillment internals.

Interface (public):

  • SessionSubject { agent: ControlPlaneAgent = ClaudeCode | Codex | Cursor } — the light always-on session.
  • ComputeRequest { requester, workload: ComputeWorkload, needs: ResourceEnvelope, locality } where locality = FulfillableRemotely | MustRunLocal. No heavy/pool/lane vocabulary at the interface.
  • ComputeWorkload = ExecCommand { command } | GhaRunner { repo, labels } — a queued CI job is a ComputeRequest of the same shape (one concept, every breadth — DESIGN §2).
  • fulfill(...) -> Fulfillment = Fulfilled { executor: RemoteExecutorHandle } | FulfillmentQueued { lane_count, held } | FulfillmentRejected { reason }.

Below the interface (private bookkeeping): HeavyComputePool, LeaseLedger, lease_grant/lease_release, ledger_conserves (held ≤ lanes, construction-not-validation, DESIGN §5). Lane source is derived from the workload (GhaRunner → GithubCiRunner, ExecCommand → OnDemandSessionLease) so CI and on-demand exec draw from one ledger — the separate runner_pool dissolves. Routable work → BuildBuddy executor; MustRunLocal → a leased pooled lane.

Semantics (12 witnesses, green by execution via gunbc run --claim-run)

  • gha_runner leases the same lane envelope/host as exec (equal work_demand digest) — operator's "the same sessions".
  • CI backpressure = FulfillmentQueued (GitHub's own queue), not Reject; in-session exec exhaustion = fail-closed FulfillmentRejected.
  • unsatisfiable needs → NeedsUnsatisfiable; pool conserves at capacity; release frees a lane.

Scope / authority

  • Count-based ledger conservation + lease eligibility live here (gunbc single authority).
  • Byte-level host conservation (heavy_compute_pool + session_pool + overhead + headroom ≤ host) remains in fleet_host_budget/node_conserves (calm-carp lane).
  • ctrl is a dumb applier; field names converge with ctrl#1838 §2.

HELD for operator review — do not merge.

🤖 Generated with Claude Code

@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 27, 2026 03:01
@gunbai-bot gunbai-bot Bot changed the title Model two-tier compute allocation in compute_fabric: unified heavy_compute_pool lease + conservation (ctrl design rev3 / PR gunb-ai/ctrl#1838) Model compute_fabric request→fulfillment interface: ComputeRequest (exec | gha_runner) → Fulfillment, one lease ledger (ctrl rev3 / #1838) Jun 27, 2026
@gunbai-bot

gunbai-bot Bot commented Jun 27, 2026

Copy link
Copy Markdown
Contributor

Addressed all three findings in 95fc0a7 (fix commit):

  1. LeaseReleaseTrigger (unused) — removed. The eviction/timeout lane will land with its reader; no scaffold needed since nothing references it now.
  2. acquired_at / max_hold (written, never read) — removed from HeavyComputeLease and from the lease_grant/fulfill signatures (+ example_lease_max_hold). They land with their reader when the eviction lane arrives.
  3. ControlPlaneAgent re-mints vendor identity (§3) — added a Disposition scaffold (control_plane_agent_vendor_scaffold) dissolving to extdeps.vendor Vendor<Domain>, per your suggestion.

Also, while in here: HeavyComputeLease.source was likewise write-only — gave it a real reader (ledger_holds_source + lease_source_eq) and strengthened witness_pool_unifies_ci_and_ondemand_then_rejects to assert the single ledger holds both GithubCiRunner and OnDemandSessionLease (was count-only). And added heavy_compute_pool_lane_count_projection_scaffold marking that lane_count must project from fleet_host_budget (single authority for the number; byte-pool conservation stays layered there per keen-dove-772).

All witnesses re-run green by execution (gunbc run --claim-run). — sent from fierce-seal-909

…lity lifts)

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 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 27, 2026

Copy link
Copy Markdown
Contributor

Thanks for the approve. Both findings:

  1. lease_source_eq → == — fixed in 83ec758. Verified by execution that substrate == lifts over the HeavyComputeLaneSource coproduct (GithubCiRunner == GithubCiRunner true, vs OnDemandSessionLease false), so the hand-rolled predicate was exactly the §5 dissolution shape. Replaced with l.source == source; witnesses re-run green.

  2. ControlPlaneAgent bind target — agreed it should point at a concrete Vendor<Software> (or Vendor<ControlPlaneAgent>) row under extdeps/vendor/, not the abstract Vendor decl. Leaving as tracked debt for the next pass per your note — minting the cited vendor rows (Anthropic/OpenAI/Cursor agent products) is its own extdeps modeling step and out of scope for this interface PR. The scaffold marker keeps it from going silent. — sent from fierce-seal-909

Brian Searls and others added 2 commits June 27, 2026 03:30
…d + BuildBuddy vendor scaffold

- 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 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 27, 2026

Copy link
Copy Markdown
Contributor

CI note: rust_tests is green. The ci job's 2 failing discovery witnesses (medium_structure_clean_tree_holds, realization_vocab_clean_tree_holds) are a pre-existing main breakage, not from this PR:

  • Reverting both files in this PR to their origin/main versions and re-running both gates locally still returns false — they fail with zero of my changes present.
  • origin/main's own CI is currently failing (latest 3 runs all failure).
  • These lenses scan dsl/{std,extdeps,compiler,tools,gunbc} + src/v2/*; dsl/product (where compute_fabric.dag lives) is not scanned. My only scanned file (the witness test) has no medium-syntax / realization-vocab literals.

The breakage is in a recent main merge's domain (#5841 String-grounding / #5822 roadmap_spawn_request). This PR's CI will go green once main is fixed and re-merged. — sent from fierce-seal-909

@briansrls briansrls closed this Jun 27, 2026
briansrls added a commit that referenced this pull request Jun 28, 2026
…shape DERIVED from the .dag program, no heavy/workload/locality (replaces discarded #5866) (#5889)

* WIP: Re-model compute_fabric as a namespace need<->opportunity connector; sha

* Ground threads in HardwareThreadCount (std.measure), drop bare Int

Addresses unit-modeling finding from review: HardRequirements.threads
was a bare Int where HardwareThreadCount (Measure<Count,One,Nat>) is
the single authority. shape_covers now uses measure_le; witnesses use
hardware_thread_count/hardware_thread_count_value at construction/read
sites.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* Remove ProgramPreference: connector spec excludes preference/locality

ProgramPreference was decorative (connect never read it) with no
scaffold dissolution trigger — DESIGN §6 violation. The connector
spec is 'no heavy/workload/locality'; preferences are locality.
Removed ProgramPreference type, prefers field, example_pref_* data.
Simplified witness_hard_requirement_unmet_is_unmet to only test the
hard requirement path (threads=64 vs capacity=8 → Unmet).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansrls@gunb.ai>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
briansrls pushed a commit that referenced this pull request Jun 28, 2026
…nector; shape DERIVED from the .dag program, no heavy/workload/locality (replaces discarded #5866) (#5889)" (#5901)

This reverts commit 989ba32.

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant