Make a declared capacity readable from comptime: Memory::X.capacity

The gap

A machine file's declared capacity cannot be named in an expression. capacity appears zero
times in src/parser/expr.rs and src/hir/expr.rs — it exists only as a field on a Memory
declaration. So this is unwritable:

// none of these parse today
let budget = Memory::HBM.capacity;
if comptime kv_bytes < Memory::SMEM.capacity { /* tile in shared memory */ }

The capacity half of the machine model is readable by the compiler and invisible to the program.

What already works, so nobody re-implements it

Admission checking is real, end-to-end, and user-writable today. It is just not expressed as a
user-written predicate — the constraint is derived from the placement rather than asserted:

let kv: Tensor<f16, [2 * LAYERS * BATCH * CTX / TP, KVHEADS * HDIM]> = Tensor<f16>([...]);
let _kv_cache = transfer(kv, Memory::HBM);

$ vxc --host default --machine fleet/a100-80.vx decode_admit.vx --action emit-mlir -o /dev/null
Error[E6009]: transferred tensor needs 128849018880 bytes but memory space 'HBM' has capacity 85899345920 bytes
Error[E6010]: the working set placed in memory space 'HBM' (3 tiles) sums to 219043332096 bytes, over its 85899345920 byte capacity; place fewer/smaller tiles or declare it `overcommit`

E6009 (per tile) and E6010 (cumulative working set) come from
check_capacity and the end-of-function budget at
transfer.rs:271. The whole matrix in utils/campaign/ is 90 real vxc invocations over
fleet/admit.vx driven by run_matrix.py through subprocess — no internal APIs.

For the common case, derived is better than asserted, and this issue does not propose replacing
it. A user who never states the constraint cannot state it wrong.

Also worth correcting: this path does not use z3

It is easy to assume admission is an SMT obligation. It is not. check_capacity is integer
arithmetic — static_tensor_bytes → granule_round → compare — and never touches the prover.

z3 is wired in for exactly two things (src/hir/solver.rs header): comptime obligations via
src/hir/prover.rs, and relaxed transfer-edge visibility via src/hir/seam.rs. Neither is
admission. Recording this because the assumption has now come up twice.

What the accessor buys that the derived check cannot

Not a second way to spell E6009. Three things the derived form structurally cannot express:

1. Comptime dispatch on capacity. Choose an algorithm by whether a tile fits, with the losing
   branch pruned before it type-checks:

   if comptime tile_bytes <= Memory::SMEM.capacity { /* shared-memory path */ }
   else { /* streamed path */ }
   

   This is the strongest motivation — it is selection, not checking, and there is no way to write
   it today.
2. Headroom budgets. "Fit in 80% of HBM", leaving room for fragmentation and workspace. The
   derived check compares against the full declared figure or nothing.
3. Constraints on quantities that are never placed — asserting a KV-cache bound directly,
   without materialising a tensor whose only purpose is to be measured.

Precedent: the transfer half is already exposed

Reachable<A, B> is a comptime boolean over the machine model, usable in if comptime
(src/parser/expr.rs:327, docs/lang/syntax.md 3.2). The graph half of the machine model is
already a comptime-visible fact. Capacity is the missing analogue, and it should follow the same
shape rather than invent a new one.

Sketch of the work

• Parser: member access on a memory space (Memory::X.capacity). Memory::X already parses as
  a memory_space; this is a field read on it.
• Checker: resolve against MemoryHierarchy::descriptor (src/hir/memory.rs:220), which is
  what check_capacity already uses. Undeclared space, or a space with no capacity:, is an
  error rather than a silent zero.
• Const evaluation: fold to an integer so if comptime prunes and the existing prover sees a
  literal. Integer arithmetic is already in scope for QF_LIA.

Estimate: one to two days for the read-only accessor plus comptime folding. That is a reading
of the code, not a measurement — the requires/ensures path with real z3 discharge would be more,
and the open questions below could move it.

Open questions

• Which fields? capacity alone, or also bandwidth, granule, scope, replicas? Each is
  declared, each is arguably comptime-visible, and each widens the surface a machine file must keep
  stable.
• Units. 80 GiB is a ByteSize. Does the accessor yield a bare i64 of bytes, or a typed
  quantity? Bare bytes are simplest and make < work immediately; typed resists unit confusion.
• Absent capacity. A host declares none deliberately (see the E6014 note — host memory is
  virtual). Memory::CPU_DRAM.capacity has no answer, and "error" is probably right, but it means
  the accessor is partial.
• Sub-space interaction. SMEM declares replicas: 108. Is .capacity per-SM or aggregate?
  The A100 measurement found a real trap here: the declared per-SM figure (167,936 B) exceeds what
  a block can opt into (166,912 B), a window exactly one granule wide where the model admits what
  the hardware refuses. Whichever the accessor returns, it should be the one a program can rely on.
• Does it belong in requires/ensures? Those already exist and are discharged by z3. A
  capacity term there would be the first machine-model fact in a proof obligation.

Scope

Design + small implementation. Filed off the back of an admission-checking demo where the surface
was found missing; the demo itself works without it.

Start with member-access handling in src/parser/expr.rs and the MemoryHierarchy::descriptor path in src/hir/memory.rs, then compare the existing checks in src/hir/check/transfer.rs. Done means Memory::X.capacity resolves for declared spaces, folds to an integer usable by if comptime, and reports an error for missing or undeclared capacity; the open questions need resolution first.