EXL3 Flash Next: host-resident K/V on the tier (6/8)

docs/kernel-contract.md

@@ -285,10 +285,59 @@ CUDA also checks the affine-3 experts' split decode pair, bit-equal to the pair
 one dropping a last round of K groups short of the warps, one chaining the groups in reverse).
 CUDA also checks Flash Next's NVFP4 experts on prompt tiles with the decode form's sums (SwiGLU gate-up and fp32
 down, each bit-equal to the decode instance it replaces; the scaled-code prompt tile is the planted control).
+CUDA also checks Flash Next EXL3's canonical expert reduction (`flashnext_batch.cu`): `fn_exl3_leaf_tree` over leaves
+0-31, 32-63 and all 64 (rows 1, 2, 5 and 16 at width 2560) and `fn_exl3_leaf_finish` over the pieces of 2, 3, 5 and 8
+ranks, each output byte-equal to the host reference `exl3_canon.zig` (NaN payloads aside), its class equal to float64's
+and its value within float64's bound. Six controls, each one planted fault: the tree as one flat fma chain, NaN products
+dropped, a write into the input, bf16 tree adds, and the finish as one flat chain and with bf16 merges.
+Its order is TP-independent: 64 leaves of 8 expert ids (the shared expert in the last), an fp32 fma chain a leaf in
+slot order from +0, then a fixed balanced fp32 tree, so every TP degree 1 to 8 gives the same bits. Against exact integer
+sums of the products (`exl3_canon_fp64_test.zig`) the host tests check each output at |err| <= n u / (1 - n u) times the
+sum of |y w| with n = 11 and u = 2^-24, not the contract's depth 17: a term meets at most c roundings in its leaf's chain
+of c and one per tree level whose sibling holds terms, at most 11 - c, so n <= 11, as for the old one chain over the 11
+slots (the bound is the chain's, not a lower one). On router-like and wide-range rows the tree's worst output is no
+worse than the old chain's or a rank-split sum's and its mean within a quarter of the best of them.
+CUDA also checks Flash Next's EXL3 deep prefill: its rotate and gate-up pass (`tf_exl3pf_rotate`, `tf_exl3pf_gu`) and
+its down pass (`tf_exl3pf_down`), on rows of ten routed picks and the shared expert at 1 to 1,408 rows, each bit-equal
+to the grouped decode form of `exl3_experts` it replaces (the planted control runs the gate-up pass against a decode
+form with the other SwiGLU roundings); gate 4 runs zero trellis words, whose one dyadic weight makes every dot an exact
+FP32 integer. Its dense prompt tile (`exl3_candidate.cu`'s `tf_exl3_promptd_0`, `_1` and `_2`, one a codebook) is
+bit-equal to `linear_body` at 1 to 2,048 rows (the 64-row block's and the 256-row chunk's edges included) at every
+width of 1 to 8 bits, on each form `plan()` gives (a K split or none, 4 or 8 warps) and on a family's fixed plans (one
+split of 4 warps, two of 8); gate 4 runs all-ones states, one weight at every width, where an fp16 sum overflows. Four
+controls: the tile at another K split, one a codebook, and one that zeroes x's NaN and infinities (red at gate 1).
+CUDA also checks the deep prefill's rotate and its expert-parallel reduction on their own (`flashnext_exl3_prefill.cu`,
+`tf-cuda-test exl3-tppf-contract` runs them alone): `tf_exl3pf_rotate` (the tables of 16 experts, 1 to 1,408 rows of ten
+picks and the shared expert at width 2,560) against a host fp32 Hadamard in the kernel's butterfly order, bit for bit
+(NaN payloads aside), and `tf_exl3pf_tp_combine` (every rank's partial blocks into the all-gather layout at degrees 1
+to 8, one region or 256-row sub-blocks, to 2,048 rows, picks masked, foreign or past the table), `tf_exl3pf_tp_finish`
+(the gathered partials at degrees 2, 3, 5 and 8, to 4,096 rows) and `tf_exl3pf_tp_place` (y[r, 0] and the weights, the
+other slots untouched, to 1,024 rows), each byte-equal to the host `exl3_canon.zig` order, with float64's class and its
+bound on every output. Gate 4 runs a transform whose two big outputs leave the rest cancelling (rotate), mirrored
+integer products (combine) and shuffled pairs of 2^19 to 2^20 (finish); place has no sums (N/A). Fourteen controls: the
+rotate with NaN zeroed, its input written, the up table's signs from the gate table, and bf16 butterfly adds; the
+combine as one chain, with NaN products dropped, its input written, and bf16 tree adds; the finish as one chain, with
+bf16 merges and its input written; the place with NaN zeroed, its input written, and every weight 1. The host test
+`test-flashnext-tppf-contract-host` runs the same oracles through the gates and the gathered ranks equal to one rank.
 CUDA also checks Nemotron's pocket (`nemotron_ops.cu`, the learned neurons the living-weights learner adds beside the
 shared expert): relu^2 up into act rows and down added into the shared expert's slot, a block row a row and tiled, the
 down to fp32 and bf16, against float64, the neurons past the count NaN so a read of one shows (two controls: the up's
 relu by `fmaxf`, and the down launched one neuron short).
+CUDA also checks Flash Next's EXL3 host tier (`flashnext_exl3_kvtier.cu`: a layer's K/V in lent frames, a block cache
+over the host store). `kvt_fetch` is compared with a host model byte for byte over every lent frame (the NaN and
+infinities planted in the host rows arrive as stored, nothing else is written, entries of the list past the count are
+never read) and `kvt_remap` with its model over the key lists, counts and overflow flag, which it rewrites in place
+(a missing block, a flag already set and rows without a selection included). `kvt_plan` places each miss in whichever
+victim an atomic reaches first, so the harness reads an image of what does not depend on that: the counters, the blocks
+needed and missed, the marks and the multiset of stamps, which the host's LRU model gives exactly, then checks the
+placement is one an LRU may make (victims are the least recently used slots the call does not use, equally old ones in
+any order; evicted blocks are unmapped, hit slots are stamped, nothing else moves). Its calls start from a steady
+cache, every block a hit, a fresh one, heavy stamp ties, a wrapped clock, no selecting rows, and a flag left set, and at
+the smallest slot count the lists overflow. Gate 4 does not apply (integers only), and gate 1 plants garbage and the bit
+patterns of NaN and the infinities where the kernels never read. Three controls, red at gate 3: the table read one
+entry late, slot rows one block late, the window one block early. What it does not check: which miss takes which of
+several equally old slots, as that is the atomics' order, so a run of many calls is not compared byte for byte (the
+device test, `exl3-kvtier`, holds its misses within 5% of the model over 60 drifting calls).
 
 Metal also checks DeepSeek V4.1's CSA2 attention (`csa2_attn.metal`): decode rows (ring or linear windows) and prompt rows
 (16-key tiles at absolute positions), fp32 and bf16 out, against float64's softmax over the window, the selected rows and
@@ -329,6 +378,16 @@ shared memory, the device's limits and the planted controls are checked the same
 A restored 13.0 receipt can arrive after the later compiler sets. Such records mark `later_pending` so 13.0 and
 13.1 use their base usage, while 13.2 and later keep their independently measured or pending selection.
 A missing later receipt remains pending; a 13.0 measurement never substitutes for it.
+Flash Next's 16 EXL3 launches (`flashnext_exl3_pending.zig`) carry only an nvcc 13.4 receipt: they stay pending under
+13.0 to 13.3 and take their 13.4 usage from `cuda_134`, which `pending_132.lookup` serves for that release.
+The first, `fn_exl3_split_f16`, also runs gates 1 to 4 on the CUDA runner (`contract_flashnext_exl3.zig`): an fp16
+row splits into bf16 hi = bf16(x) and lo = bf16(x - hi), every output's bits must equal float64's (NaN stays NaN; an
+infinity gives hi = Inf and lo = NaN), and the device's hi + lo must equal x for every finite pattern. Its shapes
+hold all 65,536 fp16 patterns and partial last blocks (n = 1,000 and 65,537). Three controls go red: one flushing NaN
+and Inf to zero (gate 1), one launching whole blocks only (gate 3, at every tail) and one writing hi over its input
+(gate 2). Gate 4 is N/A: it has no sums.
+The other 12 launches of the set also run gates 1 to 4 on the CUDA runner (see the coverage above): the canonical tree
+and finish, the pick mask, the prefill's rotate, gate-up, down, combine, finish and place, and the prompt tiles.
 
 Gemma 4 CUDA tower QKV norms and nine-term pooling register FP32 sums and BF16 outputs.
 Their contract keeps the exact FP32 mirror and adds independent FP64 ranges at the BF16 nodes.

docs/multi-rank-receipts.md

@@ -13,7 +13,8 @@ Each path places its ranks its own way:
 | Native ROCm build | `--tp`, `--rank`, `--master` | [Native ROCm placement](../zig/src/native/hip.zig) |
 | The `fabric/tp` transport's harness | `TF_TP_WORLD`, `TF_TP_RANK`, `TF_TP_MASTER` | [The transport's README](../zig/src/fabric/tp/README.md) |
 
-The native CUDA build serves neither `--tp` nor `--rank`: a family's own variables place its ranks. `tf-tp-test` is
+The native CUDA build serves neither `--tp` nor `--rank` for a checkpoint other than a Flash Next EXL3 pack, which they
+place across two GPUs (`--tp 2 --rank N --master HOST`): a family's own variables place its ranks. `tf-tp-test` is
 the transport's harness rather than a server. `tensorfold benchmark` accepts no group placement flags and records 1
 for a managed run. Its child inherits the parent's rank environment, so start managed runs from a single-rank
 configuration. Measure a group as an attached server: start the group, then point the client at the rank that serves.

docs/recipes/exl3.md

@@ -7,8 +7,9 @@ GLM-5.3-Flash.
 ## Where it stands
 
 - The native engine has the format and a reference decoder in core (`zig/src/core/exl3_format.zig`, @akol1, #496),
-  and Metal has a standalone EXL3 projection (`zig/src/core/exl3_projection.zig`, @akol1, #681). No model serves an
-  EXL3 checkpoint in this release.
+  and Metal has a standalone EXL3 projection (`zig/src/core/exl3_projection.zig`, @akol1, #681). Flash Next serves an
+  EXL3 pack on CUDA (sm_120, one rank or two; see [its recipe](flash-next-cuda.md#exl3-checkpoints)); no other model
+  does.
 - CUDA projections and routed experts on this format are in review (#740, #741, #806). A model needs them and a loader
   for its EXL3 tensors before it can serve a checkpoint; the 27B on CUDA is the first planned.
 - The Python engine served EXL3 on CUDA from 0.3.6 to 0.6.6 through the module @vcruz305 wrote (#42): every codebook,

docs/recipes/flash-next-cuda.md

@@ -110,6 +110,42 @@ tensorfold-native serve /path/to/checkpoint --temperature 0
   `_chunks,_merge`) runs those entry points on our kernels and the rest on the set's, to put a difference down to one
   kernel.
 
+## EXL3 checkpoints
+
+An EXL3 pack (see [EXL3 weights](exl3.md)) serves on one sm_120 rank, or on two with expert parallel (`--tp 2`), with
+its routed experts in pinned host memory and a pool of expert lines a layer on the device. `tools/exl3_serve_tp2.sh`
+starts a rank. These switches tune it:
+
+| Name | Default | Effect |
+| --- | --- | --- |
+| `TF_FLASHNEXT_EXPERT_LINES` | from free memory | Expert lines a layer keeps on the device. |
+| `TF_FLASHNEXT_EXPERT_RESERVE_MB` | the server's reserve (`TENSORFOLD_MEMORY_RESERVE_GIB`) | MiB left free after the pools. |
+| `TF_FLASHNEXT_EXL3_STREAMS` | 1 | Streams whose caches the pool leaves room for, when `--parallel` does not say. |
+| `TF_FLASHNEXT_EXL3_LINE_DELTAS` | unset | `POOL:+N,POOL:-N` lines added to or removed from single pools of the uniform count. |
+| `TF_FLASHNEXT_EXL3_PROFILE_DIR` | unset | Directory where expert-use profiles persist between runs. |
+| `TF_FLASHNEXT_EXL3_PROFILE_SIZING` | `0` | `1` sizes the pools from the stored profile; ignored with `TF_FLASHNEXT_EXPERT_LINES`. |
+| `TF_FLASHNEXT_EXL3_ROUTED` | host | `device` keeps every routed expert on the device. |
+| `TF_FLASHNEXT_EXL3_ARCH` | unset | `unqualified` serves on a device that is not sm_120, without a claim. |
+| `TF_FLASHNEXT_EXL3_MTP_RESIDENT` | `0` | `1` keeps the MTP layer's experts on the device instead of a pool (one rank). |
+| `TF_FLASHNEXT_EXL3_PREFILL` | on | `0` turns the deep-chunk prefill path off. |
+| `TF_FLASHNEXT_EXL3_PREFILL_ROWS` | 8,192 | Rows of a deep chunk; also what the server reserves at load. |
+| `TF_FLASHNEXT_EXL3_PREFILL_RING` | on | `0` stops streaming the coming layers' experts into one ring of the pools' lines. |
+| `TF_FLASHNEXT_EXL3_PREFILL_RING_AHEAD` | 1 | Layers ahead the ring prefetches. |
+| `TF_FLASHNEXT_EXL3_PREFILL_OVERLAP` | on | `0` (two ranks) stops overlapping the all-reduce with a chunk's compute. |
+| `TF_FLASHNEXT_EXL3_PREFILL_REDUCED_BRANCH` | `0` | Experimental: `1` (two ranks) reduces the weighted branch in fp32, written back with unit weights. |
+| `TF_FLASHNEXT_EXL3_PREFILL_TWO_CHUNK` | `0` | Experimental: `1` (two ranks, ring) runs a second deep chunk beside the first when memory admits it. |
+| `TF_FLASHNEXT_EXL3_PREFILL_SNAP_GRID` | on | Diagnostics only: `0` keeps prompt-cache states at any row instead of on the serving step's starts, to test that a resumed prompt equals a fresh one. |
+| `TF_FLASHNEXT_PROFILE` | `0` | Diagnostics only: `1` times the ranks' combine, all-reduce and place of a deep chunk, with a wait each. |
+| `TF_FLASHNEXT_KV_PAGES` | unset | `n`: streams beside the first take their attention caches from one pool of `n`-position pages. |
+| `TF_FLASHNEXT_KV_HOST` | unset | With `TF_FLASHNEXT_KV_PAGES`: MiB of pinned host RAM holding the K/V plane of every page; `0` is no host tier. |
+| `TF_FLASHNEXT_KV_FRAMES` | the pages the plan gave | With the host tier: at most this many device frames of the K/V plane. |
+| `TF_FLASHNEXT_KV_SLOTS` | 128 | With the host tier: frames lent to a stream, 64 four-row slots a frame for each attention layer. |
+| `TF_FLASHNEXT_PLE_READ` | `map` | `pread` reads the n-gram embedding rows by positional read. |
+| `TF_FLASHNEXT_SNAP_HOST` | `1` above 32,768 tokens of context, else `0` | Whether kept prompt-cache states live in pinned host memory. |
+| `TF_FLASHNEXT_CACHE_TELEMETRY` | `0` | Diagnostics only: `1` logs `EXL3-CACHE` expert-cache counters per phase, with a sync at each boundary. |
+| `TF_FLASHNEXT_EXL3_LAYER_TELEMETRY` | `0` | Diagnostics only: `1`, with the switch above, adds per-layer counters. |
+| `TENSORFOLD_BIN`, `TF_SRC` | built binary, the checkout | Diagnostics only: the binary `tools/exl3_*.sh` run and the checkout `tools/exl3_*.py` read their corpus from. |
+
 ## What the core runs and what the family runs
 
 The family plugs into the core's pieces and adds no scheduler:

tools/exl3_len_abba.py

@@ -0,0 +1,97 @@
+"""Concurrent two-request HTTP bench (repeated-ID prompts) for EXL3 ABBA runs: PORT IDS.json OUT.json LENGTH DRAFT."""
+import concurrent.futures
+import json
+import statistics
+import sys
+import time
+import urllib.request
+
+
+def one(port, prompt, tokens=128, draft=False):
+    body = {
+        "prompt": prompt,
+        "max_tokens": tokens,
+        "temperature": 0,
+        "ignore_eos": True,
+        "stream": True,
+        "stream_options": {"include_usage": True},
+        "draft": draft,
+    }
+    request = urllib.request.Request(
+        f"http://127.0.0.1:{port}/v1/completions",
+        json.dumps(body).encode(),
+        {"Content-Type": "application/json"},
+    )
+    started = time.perf_counter()
+    first = last = None
+    usage = {}
+    runtime = {}
+    text_events = 0
+    complete = False
+    with urllib.request.urlopen(request, timeout=1800) as response:
+        for raw in response:
+            line = raw.decode().strip()
+            if line == "data: [DONE]":
+                complete = True
+                break
+            if not line.startswith("data:"):
+                continue
+            event = json.loads(line[5:])
+            usage = event.get("usage") or usage
+            runtime = event.get("tensorfold") or runtime
+            for choice in event.get("choices", []):
+                piece = choice.get("text") or (choice.get("delta") or {}).get("content") or ""
+                if piece:
+                    now = time.perf_counter()
+                    first = first or now
+                    last = now
+                    text_events += 1
+    generated = int(usage.get("completion_tokens", 0))
+    span = (last - first) if first is not None and last is not None else 0.0
+    return {
+        "complete": complete,
+        "prompt_tokens": usage.get("prompt_tokens"),
+        "tokens": generated,
+        "ttft_s": (first - started) if first is not None else None,
+        "first_token_at": first,
+        "last_token_at": last,
+        "prefill_s": runtime.get("prefill_seconds"),
+        "decode_tps_server": runtime.get("tokens_per_second"),
+        "decode_tps_client": ((generated - 1) / span) if generated > 1 and span > 0 else None,
+        "itl_ms_client": (1000 * span / (generated - 1)) if generated > 1 and span > 0 else None,
+        "token_sha256": runtime.get("token_sha256"),
+        "text_events": text_events,
+    }
+
+
+def batch(port, prompt, tokens, draft=False):
+    start = time.perf_counter()
+    with concurrent.futures.ThreadPoolExecutor(max_workers=2) as pool:
+        results = list(pool.map(lambda _: one(port, prompt, tokens, draft), range(2)))
+    end = time.perf_counter()
+    total = sum(row["tokens"] for row in results)
+    first_times = [row["first_token_at"] for row in results if row["first_token_at"] is not None]
+    last_times = [row["last_token_at"] for row in results if row["last_token_at"] is not None]
+    decode_span = max(last_times) - min(first_times) if first_times and last_times else 0.0
+    return {
+        "requests": results,
+        "batch_wall_s": end - start,
+        "aggregate_decode_tps": total / decode_span if decode_span > 0 else None,
+        "end_to_end_aggregate_tps": total / (end - start) if end > start else None,
+        "mean_prefill_s": statistics.mean(row["prefill_s"] for row in results if row["prefill_s"] is not None),
+    }
+
+
+if __name__ == "__main__":
+    port = int(sys.argv[1])
+    with open(sys.argv[2], encoding="utf-8") as source:
+        base = json.load(source)
+    length = int(sys.argv[4]); draft = sys.argv[5] == "1"
+    ids = (base * (length // len(base) + 1))[:length]
+    report = {"prompt_tokens": len(ids), "tokens": 128, "drafts": draft, "batches": []}
+    for phase in ("warmup-1", "measure-1", "measure-2"):
+        result = batch(port, ids, int(__import__("os").environ.get("TOK", "128")), draft)
+        report["batches"].append({"phase": phase, **result})
+        print(json.dumps(report["batches"][-1]), flush=True)
+    with open(sys.argv[3], "w", encoding="utf-8") as target:
+        json.dump(report, target, indent=2)