Module launch_budget 

Error types for trueno-gpu operations Launch budget validation — the executable form of contracts/trueno/ptx-codegen-safety-v1.yaml register_budget. Deliberately NOT under driver (which is #[cfg(feature = "cuda")] in its entirety): the policy is pure, so its case table runs in the required check. Launch budget validation — the enforcement ptx-codegen-safety-v1 has always declared.

contracts/trueno/ptx-codegen-safety-v1.yaml equation register_budget states

forall kernel K:
  reg_count(K)  <= max_regs_per_thread(sm)
  shared_mem(K) <= max_shared_per_block(sm)
postcondition: cuOccupancyMaxActiveBlocksPerMultiprocessor > 0

and nothing enforced it: the generated contract_register_budget! macro is invoked nowhere in the tree, and its postcondition names an unbound identifier that would not compile if it ever were. This module is that missing enforcement.

Arch-agnostic by construction. The contract’s own domain stops at sm_90, and so does the hand-written arch table in driver/sys/mod.rs (CU_TARGET_COMPUTE_90 is the last constant). A per-SM limit table is a thing that goes stale every GPU generation — this one has, twice. So the limits here are queried from the device (cuDeviceGetAttribute) rather than looked up, and adding a new architecture requires no change to this file.

The policy — [validate_launch] — is pure and needs no GPU, so its case table runs in the required check. Only [DeviceLimits::query] and [KernelAttributes::query] need CUDA.

Structs

DeviceLimits

Device-side limits, queried rather than tabulated.

KernelAttributes

Per-kernel resource usage, as reported by the JIT for a compiled kernel.

Enums

LaunchBudgetViolation

A way a launch violates the kernel’s or the device’s budget.

Functions

spills_to_local

Whether a kernel spilled registers to local memory.

validate_launch

Validate one launch configuration against a compiled kernel and its device.