内存检查在zkVM中，用于使证明者能够向验证者证明读/写内存的操作是正确的。在内存系统中，值 $v$ 可以被写入地址 $a$，随后程序可以通过地址 $a$ 检索值 $v$。该技术允许验证者高效地确认证明者遵守了内存的规则（即，任何读取操作返回的值确实是写入该内存地址的最新值）。

术语“离线内存检查”指的是在 zkVM 证明中，在所有读取操作返回的值被提交后，一次性检查所有读取操作的正确性的技术。离线检查技术不会在每次读取发生时立即确定其是否正确，而是在所有读取操作完成后，进行一次性检查，确认所有读取是否正确。这与“在线内存检查”技术，如 Merkle 哈希，形成对比。后者通过要求每次读取都包含认证路径来立即确认内存读取的正确性。Merkle 哈希在每次读取的基础上进行证明对证明者来说成本更高，而离线内存检查更适合 zkVM 的场景。

1. 构建读集合 $RS$ 和写集合 $WS$

我们构建两个集合，读集合 $RS$ 和写集合 $WS$，它们的元素都是元组 $(a, v, c)$，其中 $a$、$v$、$c$ 分别表示地址、值和指令计数。按如下方式进行构造。

初始化：

• $RS = WS = \emptyset$；
• 如需向内存 $a_i$ 初始存入值 $v_i$，则将初始元组添加到写集合，即 $WS = WS \bigcup {(a_i, v_i, 0)}$。

内存读取和写入操作：

• 从地址 $a$ 读取值时，找到写集合 $WS$ 中最后一个(即对应最大的指令计数 $c$ )该地址的元组 $(a,v,c)$。更新 $RS = RS \bigcup {(a, v, c)}$ 和 $WS = WS \bigcup {(a, v, c{now})}$，其中 $c{now}$ 为当前指令计数；
• 将值 $v'$ 写入地址 $a$ 时，找到写集合 $WS$ 中最后一个地址为 $a$ 的元组 $(a,v,c)$。更新 $RS = RS \bigcup {(a, v, c)}$ 和 $WS = WS \bigcup {(a, v', c_{now})}$。

后处理：

• 对于所有内存地址 $a_i$，找到写集合 $WS$ 中该地址的最后一个元组 $(a_i, v_i, c_i)$，更新读集合 $RS = RS \bigcup {(a_i, v_i, c_i)}$.

2. 核心论点

如果做如下限制，则证明者遵守了内存的规则，即从内存中读取了正确的值。

1) 读集合和写集合...