# 内存与查找

> 两个论证承载一切跨行的内容。覆盖整个执行过程、只核对一次的单一读/写多重集，使每次读取都返回最近一次写入，并为每一行排序；LogUp 通道使每个值都是一个字节、一个字或一个表行。

电路族的门每次只约束一行。一切跨越行、分片或电路族的内容，例如寄存器存放的值、加载返回的值、一行执行的是哪条指令、一个值是否放得进 32 位，都由两个论证承载，而这两个论证就位于同样的 GKR 电路之中。

## 内存论证

每次内存访问都变成一个域元素，即一个**元组**：

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

它作用于地址空间、地址、时间戳和值，其中的四个挑战每个陈述只抽取一次。一个查询把它的读元组贡献给一侧，把写元组贡献给另一侧。每个分片的电路输出两个数：其读元组之积与写元组之积。然后验证者在整个陈述上检查一个等式：

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

`W_b` 和 `R_b` 是 32 个寄存器和 pc 的初始元组与最终元组，它们没有自己的行：验证者根据陈述携带的 64 个边界标量把它们乘进去。RAM 的初始值和最终值来自窗口电路族的分片，每行存放一个字：窗口 0 中是程序映像，这次运行触及的其他每个窗口中是零，公开输入窗口中是陈述的输入，证明者提示（advice）中是证明者的字节。

如果等式成立，那么两个多重集以压倒性的概率相等。多重集相等意味着**每次读取都返回在它之前的最近一次写入**：每次读取恰好与一次写入匹配，读取必须严格晚于它所消费的写入，并且每个地址恰好有一次初始写入。

### 免费得到的顺序

pc 和其他内存单元一样，也是一个内存单元，位于它自己空间的地址 0。每一行都读取 pc 并写入下一个 pc，其电路要求这次写入至少比读取晚四个时间戳。所以 pc 的历史是一条穿过每个电路族每个有效行的路径，从入口点一直到退出行。这一条路径带来：

- **程序顺序**，因为各行按其 pc 写入排序；
- **跨分片、跨电路族的连续性**，因为每一行的 pc 读取都消费了某一行的 pc 写入；
- **没有周期被证明两次**，因为任何写入都不能被消费两次。

没有哪个分片与相邻分片衔接，也不需要衔接。分片所声称的时间窗口不绑定任何东西，只检查其形状。

### 什么必须先确定

内存挑战每个陈述只抽取一次，位于全局 transcript 的末尾，在元组可能读取的一切都已固定之后：每个分片的内存承诺、程序身份（它固定了入口 pc 和映像）、仪式摘要、分片数和窗口列表、公开输入与公开输出（journal）的摘要，最后是 64 个边界标量。在挑战之后才选定的值，可以被反解出来；正是 transcript 的顺序禁止了这一点。出于同样的原因，内存元组只能读取内存列、设置列和虚拟列，绝不能读取见证列，因为见证列是在挑战之后、于分片自己的 transcript 中承诺的。电路构造器会拒绝任何违反这一点的制品。

## 查找

**查找**（lookup）是说：一行中若干值构成的元组，是某张表中的一行。远地虚拟机用 **LogUp** 证明一个分片的每个查找：每张表（即每个**通道**）一个恒等式，

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

该恒等式由电路族自身 GKR 电路中的分式树求和，并在树根处检查：分子为零，分母非零。重数列完全不需要约束：一个不在任何表行中的元组会留下一个重数无法抵消的极点。

| 通道 | 表 | 用途 |
| --- | --- | --- |
| `TIMESTAMP` | `[0, 2^19)`，虚拟 | 每个查询的时间戳差，拆为两个 19 位块 |
| `RANGE16` | `[0, 2^16)`，虚拟 | 把 32 位值拆为两个半字；进位；帧的边界 |
| `XOR8` | 所有字节对及其 XOR，虚拟 | 逐字节计算 Keccak 和 SHA-256 |
| `GENERIC` | 一张已承诺的表，含 AND 行、符号行和移位幂行 | 按位运算、符号位、移位量 |
| `DECODER` | 电路族的解码表，由程序身份承诺 | 把每个被执行的行绑定到程序 |

其中三张表是虚拟的：它们是行索引的闭式表达式，由验证者自己求值，不花费任何承诺。通用表用仪式的幂次承诺一次，并由 SRS 摘要覆盖。

### 解码器查找

每个执行电路族都为每个有效行在自己的解码表中做一次查找，以该行从内存中读到的 pc 为键。这一次查找就把这个周期绑定到程序：该行的操作数、立即数和指令类别都是程序在该 pc 处的；它的类别位是 one-hot 的，因为表的每个有效行都存放一个 one-hot 掩码，而每个填充行存放 `−1`，任何类别位之和都达不到这个值。如果程序在某个 pc 处没有指令，位于该 pc 的行根本找不到任何表行。

### 键必须有界

通道证明的是属于某张表，仅此而已。几张子表以互不相交的键范围共用通用表，所以一个无界的键可能落进错误的子表，从而证明一个错误的 AND。因此，每个电路族都用同一选择子下的范围查找，为它查找的每个键设定界；电路构造器还会检查：通过缩放因子写出的界，同时也带有直接界。规范针对每个电路族说明了这一规则所防范的攻击。

## 如何组合起来

这两个论证与每个电路族的门一起，赋予陈述其含义：每一行都遵循其指令，该指令就是程序的指令，每次读取都看到最近一次写入，各行构成一条从入口到出口的路径，每个值都是它所声称的那个整数，公开窗口存放的是陈述中的字节。[可靠性地图](https://apogee.gweb3networks.com/docs/auditors/soundness-map)把每项断言对应到证明它的章节。

规范见[内存论证](https://apogee.gweb3networks.com/docs/auditors/spec/memory)、[查找](https://apogee.gweb3networks.com/docs/auditors/spec/lookup)。