Sidesteps the obligation entirely. There is no RAM, so there is nothing to check.

To realize KV-caching, the prover has to emulate read/write RAM operations within the SNARK circuit. This complicates the prover's logic and leads to large concrete overheads even when using state-of-the-art protocols for emulating RAM (e.g., via lookup arguments) as they require the prover to commit to additional auxiliary data that scales linearly to the number of reads/writes.

DeepProve · §1.1

• Proving proceeds layer-by-layer, backwards, GKR-style. Each operator converts a claim about its output into a claim about its input. No addresses, no cycles, no mutable buffers.
• This is exactly why the certification trick matters: emulating a KV cache would introduce RAM into a model that otherwise has none, "requiring the prover to commit to additional auxiliary data that scales linearly to the number of reads/writes."
• Embedding — the one genuinely data-dependent read — is reformulated as a sparse one-hot matmul the verifier checks locally, so it needs no memory argument.

Inherited from Jolt's Twist and Shout, adapted from CPU RAM to ONNX tensor buffers. It is Stages 4 and 5 of the proof.

Although ONNX computation removes general-purpose registers and arbitrary RAM access, we still need a notion of consistency of reads and writes over tensor buffers; the lesson from Twist and Shout is that domain-specific access patterns admit much cheaper consistency proofs than prior offline memory checking arguments.

Jolt Atlas · §1.1

• ONNX removes general-purpose registers and arbitrary RAM, but reads and writes over tensor buffers still need consistency. The lesson taken from Twist and Shout is that domain-specific access patterns admit much cheaper consistency proofs than generic offline memory checking.
• Stage 4 batches RASumCheck (virtualising $D=8$ per-chunk one-hot address polynomials into groups) with MemoryDag (read-write consistency).
• Stage 5 evaluates the memory-value polynomial: $\mathrm{Inc}$ is the committed increment, $\mathrm{Wa}$ the write-allocation indicator, and $\mathrm{Lt}$ the less-than MLE selecting only writes before the queried cycle.
• Supporting checks: BooleanitySumcheck forces $ra_i(k)^2 = ra_i(k)$, and HammingWeightSumcheck forces $\sum_k ra_i(k) = 1$ — together, each address polynomial is genuinely one-hot.
• This is the substrate under everything. The same Shout read-checking + RAF sumcheck (with the booleanity / hamming-weight / ra-virtualization trio) proves every table lookup in the system — exp, SatClamp, UnsignedLessThan, ReLU, the activation tables. Large tables never materialize: their MLE is prefix-suffix decomposed.

// val (public table MLE) and int (identity / read-back index) are
// recomputed by the verifier; only ra_claim is prover-supplied and
// is constrained by the booleanity + hamming-weight + ra-virtual sumchecks.
let expected = rv_claim + gamma * raf_claim;