feat(gpu): O2 — arm the register_budget contract, vacuous since 2026-04-06

[noahgift]

O2 of the 0.67 CUDA Rust spec (#3062). Developed and validated on gx10 (GB10 Blackwell sm_121), the only host where the interesting arch lives.

The defect

contracts/trueno/ptx-codegen-safety-v1.yaml equation register_budget declares a register/shared-memory budget with postcondition cuOccupancyMaxActiveBlocksPerMultiprocessor > 0. Nothing enforced it:

• the generated macro contract_register_budget! is invoked nowhere in the tree
• its postcondition names cuOccupancyMaxActiveBlocksPerMultiprocessor, an unbound identifier that would not compile if the macro ever were invoked
• FALSIFY-PTX-003's test: is prose — "Parse ptxas output for register count, assert <= 128" — and prose never runs
• it carries registry: true, the exemption class retired 2026-08-21

Meanwhile aprender-gpu launches hand-emitted PTX with hardcoded block sizes (128/256) and validates nothing about the kernel the JIT actually produced.

Two deliberate design splits

1. The policy is ungated. crate::launch_budget::validate_launch is pure and lives at the crate root, not under driver. The whole driver module is #[cfg(feature = "cuda")] (lib.rs:138), so anything placed there runs only with --features cuda and would never reach the required check.

Measured while building this: that is exactly why driver::ptx_patch's GH-480 tests are dark today — despite its module comment claiming "NOT feature-gated so that its tests run without CUDA hardware." Putting the policy there would have made O2 theater.

aprender-gpu --lib goes 444 → 457 tests, all in the CPU-only path #3063 un-darks.

2. Limits are queried, not tabulated. A per-SM table goes stale every GPU generation and this one did — the hand-written CU_TARGET_COMPUTE_* list stops at 90, and so did the contract's own domain. driver/budget_query.rs reads limits from cuDeviceGetAttribute, so sm_100/120/121 and whatever ships next need no edit here.

Mechanism engaged, on Blackwell

Not "it compiled" — the actual values read back on GB10 sm_121 under ptxas 13.3:

cc=(12,1)  kernel{max_thr=1024 regs=8 smem=0 local=0}
           device{max_thr=1024 smem=49152 regs=65536 warp=32}
           occupancy@256=6

19/19 with --features cuda on sm_121, and 13/13 pure on the default build. Also 19/19 on RTX 4090 sm_89.

Mutation proof — and the test that failed it

Deleting the block-size comparison in validate_launch turns 4 tests RED, restoring turns them GREEN:

launch_budget::tests::rejects_block_above_kernel_max
launch_budget::tests::kernel_max_is_reported_before_device_max
launch_budget::tests::violations_name_both_sides_of_the_comparison
driver::cuda_tests::launch_budget_hw::budget_goes_red_on_an_oversized_block

The hardware test's first version SURVIVED the mutation. It asserted only that an error occurred — but with the kernel-max check deleted the oversized launch falls through to the device-wide check and still errors, so the test witnessed nothing. It now asserts the specific violation. That was found by running the mutation, not by reading the test, and the contract's red_witness records it.

Contract repaired in the same commit

• registry: true dropped
• FALSIFY-PTX-003 prose replaced with two executable cargo test commands
• domain extended past sm_90 to 100/120/121
• two pre-monorepo paths fixed (trueno/src/…, realizar/src/… — neither exists since APR-MONO)
• enforced_by: names the two files that now implement it
• pv validate → 0 errors, 0 warnings

Verification

cargo fmt clean · clippy -D warnings clean on both default and --features cuda — the raw-pointer entry points are unsafe fn with # Safety docs rather than an #[allow] · 457/457 default · 19/19 cuda on sm_89 and sm_121.

Refs #3062

🤖 Generated with Claude Code

https://claude.ai/code/session_01J9cSQynVPYeUkQ2i7ccvrs

[github-actions]

§13.11 rung 1 — quorum shadow verdict

S13-SHADOW pr=3064 head=c69bb00741f21326fb5f15e6e9f8c514daedb028 verdict=REFUSE class=Q1 arm_rc=1

Shadow mode: this records a verdict and merges nothing. A refusal
to arm is not a block (§13 adds zero rows to §7) — the pull request is
exactly as green as it was.