> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Layouts and assumptions

> Tell the engine how physical storage maps to the spec's logical tensors, and which preconditions a kernel relies on.

## 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=`:

```python theme={"system"}
@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:

```python theme={"system"}
@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:

```text theme={"system"}
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:

```bash theme={"system"}
theformalera guards --emit kernels/_theformalera_guards.py
```

```text theme={"system"}
✓ wrote kernels/_theformalera_guards.py: guards for 5 kernels (3 assumptions)
```

```python kernels/_theformalera_guards.py theme={"system"}
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:

```python theme={"system"}
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:

```python theme={"system"}
@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.

> [!NOTE]
>
> `[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.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.