Layouts and assumptions

Layouts

A spec talks about logical tensors: K[b, s, h, d]. A kernel reads physical memory: pages of a KV cache, a strided view, a packed weight. A layout mapping is the function from one to the other. Pass one per pointer parameter in layout=:

@tfe.implements(
    "Qwen/Qwen3.8-27B@1.0:layers[*].attn.core",
    grid=("B", "heads"),
    bind={"Q": "q", "K": "k", "V": "v", "SL": "seq_lens", "O": "o", "sm_scale": "scale",
          "stride_bt": "cdiv(S, 16)"},
    layout={
        "K": tfe.layout.paged_kv(block_table="BT", page=16),
        "V": tfe.layout.paged_kv(block_table="BT", page=16),
    },
    domain={"B": (1, 256), "S": (1, 262144)},
)
@triton.jit
def paged_decode_attention(Q, K, V, BT, SL, O, sm_scale, stride_bt,
                           D: tl.constexpr, G: tl.constexpr, PAGE: tl.constexpr):
    ...

Constructor	Logical → physical	Typical use	Engine support
(default)	Row-major; outer strides from the kernel’s stride parameters, in signature order	Ordinary tensors	yes
`tfe.layout.strided(*strides)`	`x[i, j] = mem[i·s0 + j·s1]`; each stride is an int or a parameter name	Explicit strides	yes
`tfe.layout.row_major(*dims)`	Contiguous, last dimension fastest	Packed tensors	yes
`tfe.layout.paged_kv(block_table, page)`	`K[b, s, h, d] = cache[bt[b, s // P], s % P, h, d]`	Paged KV cache	yes
`tfe.layout.col_major(*dims)`	Contiguous, first dimension fastest	Transposed weights	parsed
`tfe.layout.ragged(cu_seqlens)`	`x[b, s, :] = mem[cu[b] + s, :]`	Variable-length batches	parsed
`tfe.layout.recurrent_state(slot)`	`S[b]` = the spec’s recurrent state after sequence `b`’s prefix	Gated DeltaNet decode state	parsed
`tfe.layout.blockwise_scaled(block, scale)`	`W[i, j] = q[i, j] × scale[i // B, j // B]`	FP8 block-quantised weights	parsed
`tfe.layout.permuted(*order)`	Dimension permutation	Pre-packed weights	parsed
`tfe.layout.interleaved(dim, parts)`	`parts` logical tensors interleaved along `dim`	Interleaved gate/up, per-head q/gate	parsed
`tfe.layout.custom("module:function")`	A pure index function you write	Anything else	parsed

“Parsed” layouts are accepted in annotations and recorded in reports. Where the engine does not model a layout yet, verification of that kernel ends UNKNOWN rather than assuming a layout. blockwise_scaled does more than remap indices: it interprets quantised storage as real-valued weights. Weight-quantisation error is the model provider’s decision, not a kernel bug. Activation quantisation changes the computation itself, and is out of scope.

Assumptions

An assumption is a precondition the kernel relies on but the spec does not guarantee:

@tfe.implements("Qwen/Qwen3.8-27B@1.0:layers[*].attn_residual", grid=("cdiv(T * 5120, BLOCK)",),
                bind={"X": "x", "Hh": "h", "Y": "y", "n": "T * 5120"},
                assume=["contiguous(X)", "contiguous(Hh)", "contiguous(Y)"])
@triton.jit
def residual_add_kernel(X, Hh, Y, n, BLOCK: tl.constexpr):
    ...

Supported forms:

Integer conditions on shape symbols and integer parameters: T % 16 == 0, T <= 8192, S >= 1.
Tensor properties: contiguous(X).

Each assumption becomes a hypothesis of the proof, is listed under assumptions in the JSON report, and is written into the release certificate.

Vacuity

If the assumptions contradict each other or empty the shape domain (T % 16 == 0 with T ∈ [1, 8]), any kernel would be “proved”. The engine checks satisfiability first, and reports such a run as:

FAILED · VACUOUS: the assumptions contradict each other or the shape domain: the proof would be vacuous

Runtime guards

A proof is only valid when its assumptions hold at runtime. theformalera guards generates a module with one check per kernel:

theformalera guards --emit kernels/_theformalera_guards.py

✓ wrote kernels/_theformalera_guards.py: guards for 5 kernels (3 assumptions)

kernels/_theformalera_guards.py

def guard_rmsnorm_kernel(eps) -> None:
    """Preconditions of rmsnorm_kernel (kernels/norm.py:14) for Qwen/Qwen3.8-27B@1.0:layers[*].input_norm, Qwen/Qwen3.8-27B@1.0:layers[*].post_attn_norm."""
    if not ENABLED:
        return
    if not (abs(float(eps) - 1e-06) <= 1e-12 * max(1.0, abs(1e-06))):
        raise AssumptionViolated('eps == 1e-06 (model constant)')

Call the guard in the launcher, before the kernel:

from kernels._theformalera_guards import guard_rmsnorm_kernel

def rmsnorm(x, w, eps=1e-6):
    guard_rmsnorm_kernel(eps)
    y = torch.empty_like(x)
    rmsnorm_kernel[(x.shape[0],)](x, w, y, x.stride(0), y.stride(0), eps, H=x.shape[1], BLOCK=BLOCK)
    return y

Scalars bound to model constants get guards too, as eps == 1e-06 shows.
Guards only compare integers and metadata, so their cost is negligible.
Set THEFORMALERA_GUARDS=0 to disable them, for example in a benchmark.
A failed guard raises AssumptionViolated, a subclass of AssertionError.

Narrowing the domain

domain= narrows the shape domain of one kernel:

@tfe.implements("Qwen/Qwen3.8-27B@1.0:layers[*].mlp.act", grid=("T", "cdiv(17408, BLOCK)"),
                domain={"T": (1, 8192)})

The narrowed domain is what gets proved, so it should match how the system is really deployed: for example, a prefill kernel that only ever sees chunks of at most 8192 tokens. Widening the default domain is rejected.

[policy] domain_narrowing (allow | warn | fail) is accepted in theformalera.toml but not enforced by this release, and narrowed domains are not yet listed in the release certificate. If a narrowing matters for your deployment, also state it as an assume= entry: assumptions are listed in the certificate and get runtime guards.

Get started

Concepts

Guides

Model conformance

Case studies

Help

Layouts

Assumptions

Vacuity

Runtime guards

Narrowing the domain

​Layouts

​Assumptions

​Vacuity

​Runtime guards

​Narrowing the domain

Layouts

Assumptions

Vacuity

Runtime guards

Narrowing the domain