Heterogeneous targets · P1-1: bounded dynamic shapes (where n <= N, Tensor<[<=N,..]>)

P1-1 — Bounded dynamic shapes

Vx's guarantee needs byte bounds, not exact shapes. Proving a KV tile fits in VMEM requires seq_len <= 4096, never that seq_len is 1723. Bounded dynamism is ~90% of real serving need and is entirely tractable; it is also the strongest positioning vs torch.compile(dynamic=True) (guards vs proofs). Shares the solver with P0-2.

Today

Shapes are literal, const-generic (§4.5), or unverified (a runtime dim silently skips the capacity check — now at least warned via P0-4/W1029).

Proposed — two surfaces, the second sugar for the first

(a) bound on a value, via the existing where clause:

fn stage(n : i32) -> i32 where n <= 512 {
  let a = Tensor<f32>([n, 128]);        // bounded: 512 * 128 * 4 = 256 KB
  let va = transfer(a, Memory::VMEM);   // E6009 checked against the bound
  return 0;
}
fn main() -> i32 {
  stage(384);                            // ok: 384 <= 512 discharged statically
  stage(600);                            // E60xx
  return 0;
}

(b) bound in the type, for tensors crossing an API boundary:

fn attend(q : Tensor<f32, [<=4096, 128]>,
          k : Tensor<f32, [<=4096, 128]>) -> Tensor<f32, [<=4096, 128]>
  on Topology::TensorCore { ... }

Semantics

• static_tensor_bytes becomes tensor_bytes(elem, dims, bounds) -> { exact: Option<u64>, upper: Option<u64> }.
• E6009 (per-tile) and E6010 (working set) check upper; the granule allocator reserves slots from upper (worst-case, which is what a real allocator does).
• Codegen unchanged: memref<?x128xf32> + masking already works.

Diagnostics

E60xx: cannot prove the bound 'n <= 512' at this call (argument is the literal 600)
E6009: transferred tensor needs up to 2097152 bytes (bound: n <= 4096) but 'VMEM' has capacity 67108864

Discharge

Reuse hir::seam::Solver — bound propagation is QF_LIA, cheaper than the QF_BV obligations already running. Syntactic fast path first (literal ≤ literal, param with a declared bound), z3 fallback.

Where it lands

src/parser/decl.rs (extend the where arm beyond Transfer<A,B>), src/parser/types.rs (<=N in a dim), src/syntax/types.rs (Dim::{Exact,Bounded}), src/hir/memory.rs (tensor_bytes), src/hir/expr.rs (bound env + call-site discharge).

From the Heterogeneous Target Gap Analysis (§9). Status tracked there and in the P0 decision log. Sibling to the landed P0 work (P0-1 fa056b4e, P0-3 33ce0b64, P0-4 5e10637a, P1-4a-core 34b31902).

Read §9 of docs/discussions/heterogeneous_target_gap_analysis.md and the P0 decision log first, then trace the existing Transfer where-clause handling in src/parser/decl.rs and tensor sizing in src/hir/memory.rs. Review the related type and expression paths in src/parser/types.rs, src/syntax/types.rs, and src/hir/expr.rs; done means bounded dimensions and values propagate through the existing solver, capacity checks use upper bounds, and the specified diagnostics are emitted.