# Memory and Lookups

> Two arguments carry everything that crosses a row. One read/write multiset over the whole execution, reconciled once, makes every read return the last write and orders every row; LogUp channels make every value a byte, a word or a table row.

A family's gates constrain one row at a time. Everything that crosses rows, shards or families, such as what a register holds, what a load returns, which instruction a row executes and whether a value fits in 32 bits, is carried by two arguments that live inside the same GKR circuits.

## The memory argument

Every memory access becomes a field element, a **tuple**:

```text
T(AS, ADDR, TS, VAL) = γ + AS + α_addr·ADDR + α_ts·TS + α_val·VAL
```

over the address space, the address, the timestamp and the value, with four challenges drawn once per statement. A query contributes its read tuple to one side and its write tuple to the other. Each shard's circuit outputs two numbers, the product of its read tuples and the product of its write tuples. The verifier then checks one equation over the whole statement:

```text
∏ read roots · R_b  =  ∏ write roots · W_b          over every shard of every family
```

`W_b` and `R_b` are the initial and final tuples of the 32 registers and the pc, which have no rows of their own: the verifier multiplies them in from 64 boundary scalars the statement carries. RAM gets its initial and final values from the window families' shards, which hold one word per row: the program's image in window 0, zeros in every other window the run touched, the statement's input in the public input window, the prover's bytes in advice.

If the equation holds, the multisets are equal with overwhelming probability. Equal multisets mean **every read returns the last write before it**: each read is matched to exactly one write, a read must strictly follow the write it consumes, and every address has exactly one initial write.

### Order for free

The pc is a memory cell like any other, at address 0 of its own space. Every row reads the pc and writes the next one, and its circuit holds the write at least four timestamps after the read. So the pc's history is one path through every live row of every family, from the entry point to the exit row. That single path gives:

- **program order**, since rows are ordered by their pc writes;
- **continuity across shards and families**, since every row's pc read consumes some row's pc write;
- **no cycle proved twice**, since no write can be consumed twice.

No shard chains to its neighbour, and none needs to. A shard's claimed time window binds nothing; it is checked only for shape.

### What must come first

The memory challenges are drawn once per statement, at the end of the global transcript, after everything a tuple can read is fixed: every shard's memory commitments, the program identity (which fixes the entry pc and the image), the ceremony digest, the shard counts and the window list, the digest of the public input and journal, and last the 64 boundary scalars. A value chosen after the challenges could be solved for; the order of the transcript is what forbids it. For the same reason a memory tuple may read only memory, setup and virtual columns, never a witness column, which is committed in the shard's own transcript after the challenges. The circuit constructors refuse any artifact that breaks this.

## Lookups

A **lookup** says that a tuple of a row's values is a row of some table. Apogee proves every lookup of a shard with **LogUp**: one identity per table, or **channel**,

```text
Σ_rows Σ_lookups 1/(E(y) + g)  −  Σ_rows mult(y)/(T(y) + g)  =  0
```

summed by a fraction tree inside the family's own GKR circuit and checked at its root: numerator zero, denominator nonzero. The multiplicity column needs no constraint at all: a tuple in no table row leaves a pole the multiplicities cannot cancel.

| Channel | Table | Used for |
| --- | --- | --- |
| `TIMESTAMP` | `[0, 2^19)`, virtual | each query's timestamp gap, as two 19-bit chunks |
| `RANGE16` | `[0, 2^16)`, virtual | 32-bit values as two halfwords; carries; frame bounds |
| `XOR8` | all byte pairs and their XOR, virtual | Keccak and SHA-256, byte by byte |
| `GENERIC` | a committed table of AND, sign and shift-power rows | bitwise operations, sign bits, shift amounts |
| `DECODER` | the family's decoded table, committed by the identity | binding each executed row to the program |

Three of the tables are virtual: closed forms of the row index that the verifier evaluates itself, which cost no commitment. The generic table is committed once by the ceremony's powers and covered by the SRS digest.

### The decoder lookup

Every execution family makes one lookup per live row into its own decoded table, keyed by the pc the row read from memory. That single lookup binds the cycle to the program: the row's operands, immediate and instruction kind are the program's at that pc, and its kind bits are one-hot because every live row of the table holds a one-hot mask and every padding row holds `−1`, which no sum of kind bits reaches. A row at a pc where the program has no instruction finds no table row at all.

### Keys must be bounded

A channel proves membership of a table and nothing more. Several sub-tables share the generic table under disjoint key ranges, so an unbounded key could land in the wrong sub-table and prove a false AND. Every family therefore bounds each key it looks up, with a range lookup under the same selector, and the circuit constructors check that a bound written through a scaling factor also carries a direct bound. The specification states the attack this prevents for every family.

## How it adds up

Together with each family's gates, these two arguments give the statement its meaning: each row obeys its instruction, the instruction is the program's, every read sees the last write, the rows form one path from the entry to the exit, every value is the integer it claims to be, and the public windows hold the statement's bytes. The [soundness map](https://apogee.gweb3networks.com/docs/auditors/soundness-map) carries each claim to the sections that prove it.

The specification: [The memory argument](https://apogee.gweb3networks.com/docs/auditors/spec/memory), [Lookups](https://apogee.gweb3networks.com/docs/auditors/spec/lookup).