Memory Consistency Checking

Offline memory checking is a method that enables a prover to demonstrate to a verifier that a read/write memory was used correctly. In such a memory system, a value $v$ can be written to an addresses $a$ and subsequently retrieved. This technique allows the verifier to efficiently confirm that the prover adhered to the memory's rules (i.e., that the value returned by any read operation is indeed the most recent value that was written to that memory address).

This is in contrast to "online memory checking" techniques like Merkle hashing which immediately verify that a memory read was done correctly by insisting that each read includes an authentication path. Merkle hashing is computationally expensive on a per-read basis for ZK provers, and offline memory checking suffices for zkVM design.

zkMIPS replaces ZKM’s online memory checking with multiset-hashing-based offline memory checking for improved efficiency. zkMIPS's verifies the consistency of read/write operations by constructing a read set $RS$ and a write set $WS$ and proving their equivalence. This mechanism leverages multiset hashing on an elliptic curve over KoalaBear Prime's 7th extension field to ensure memory integrity efficiently. Below is a detailed breakdown of its key components.

Construction of Read Set and Write Set

Definition: The read set $RS$ and write set $WS$ are sets of tuples $a, v, c$ , where:

$a$ : Memory address
$v$ : Value stored at address $a$
$c$ : Operation counter

Three-Stage Construction

Initialization:

$RS = WS = \emptyset$ ;
All memory cells $a_i$ are initialized with some value $v_i$ at op count $c=0$ . Add the initial tuples to the write set $WS = WS \bigcup \{(a_i, v_i, 0)\}$ for all $i$ .

Read and write operations:

Read Operation, for reading a value from address a:
- Find the last tuple $(a, v, c)$ added to write set $WS$ with the address $a$ .
- $RS = RS \bigcup \{(a, v, c)\}$ and $WS = WS \bigcup \{(a, v, c_{now})\}$ , with $c_{now}$ the current op count.
Write Operation, for writing a value v′ to address a:
- Find the last tuple $(a, v, c)$ added to write set $WR$ with the address $a$ .
- $RS = RS \bigcup \{(a, v, c)\}$ and $WS = WS \bigcup \{(a, v', c_{now})\}$ .

Post-processing：

For all memory cells $a_i$ , add the last tuple $(a_i, v_i, c_i)$ in write set $WS$ to $RS$ : $RS = RS \bigcup \{(a_i, v_i, c_i)\}$ .

Core Observation

The prover adheres to the memory rules if the following conditions hold:

The read and write sets are correctly initialized;
For each address $a_i$ , the instruction count added to $WS$ strictly increases over time;
For read operations: Tuples added to $RS$ and $WS$ must have the same value.
For write operations: The operation counter of the tuple in $RS$ must be less than that in $WS$ .
After post-processing, $RS = WS$ .

Brief Proof: Consider the first erroneous read memory operation. Assume that a read operation was expected to return the tuple $(a,v,c)$ , but it actually returned an incorrect tuple $(a, v' \neq v, c')$ and added it to read set $RS$ . Note that all tuples in $WS$ are distinct. After adding $(a,v',c_{now})$ to $WS$ , the tuples $(a,v,c)$ and $(a,v',c_{now})$ are not in the read set $RS$ . According to restriction 3, after each read-write operation, there are always at least two tuples in $WS$ that are not in $RS$ , making it impossible to adjust to $RS = WS$ through post-processing.

Multiset Hashing

Multiset hashing maps a (multi-)set to a short string, making it computationally infeasible to find two distinct sets with the same hash. The hash is computed incrementally, with order-independence as a key property.

Implementation on Elliptic Curve

Consider the group $G$ as the set of points $(x,y)$ on the elliptic curve $y^2 = x^3 +Ax+B$ (including the point at infinity). We can implement a hash-to-group approach. To hash a set element into a point on the elliptic curve, we first map the set element to the $x$ -coordinate of the point. Since this may not be a valid $x$ -coordinate on the elliptic curve, we add an 8-bit tweak $t$ . Additionally, we constrain the sign of the $y$ -coordinate to prevent flipping, either by ensuring $y$ is a quadratic residue or by adding range checks.

In zkMIPS, the following parameters are used.

KoalaBear Prime field: $\mathbb{F}_P$ , with $P = 2^{31} - 2^{24} +1$ .
Septic extension field: Defined under irreducible polynomial $u^7 + 2u -8$ .
Elliptic curve: Defined with $A = 3*u , B= -3$ (provides ≥102-bit security).
Hash algorithm: Poseidon2 is used as the hash algorithm.

Elliptic Curve Selection over KoalaBear Prime Extension Field

Objective

Construct an elliptic curve over the 7th-degree extension field of KoalaBear Prime $P = 2^{31} - 2^{24} +1$ , achieving >100-bit security against known attacks while maintaining computational efficiency.

Code Location

Implementation available here. It is a fork from Cheetah that finds secure curve over a sextic extension of Goldilock Prime $2^{64} - 2^{32} + 1$ .

Construction Workflow

Step 1: Sparse Irreducible Polynomial Selection
- Requirements:
  - Minimal non-zero coefficients in polynomial
  - Small absolute values of non-zero coefficients
  - Irreducibility over base field
- Implementation (septic_search.sage):
  - poly = find_sparse_irreducible_poly(Fpx, extension_degree, use_root=True)
  - The selected polynomial: $x^7 + 2x - 8$ . This sparse form minimizes arithmetic complexity while ensuring irreducibility.
Step 2: Candidate Curve Filtering
- Curve Form: $y^2 = x^3 + ax + b$ , with small |a| and |b| to optimize arithmetic operations.
- Parameter Search in septic_search.sage:
```
for i in range(wid, 1000000000, processes):
    coeff_a = 3 * a  # Fixed coefficient scaling
    coeff_b = i - 3
    E = EllipticCurve(extension, [coeff_a, coeff_b])
```
- Final parameters chosen: $a = 3u, b = -3$ (with $u$ as extension field generator).
Step 3: Security Validation
- Pollard-Rho Resistance
  
  Verify prime subgroup order > 210 bits:
```
prime_order = list(ecm.factor(n))[-1]
assert prime_order.nbits() > 210
```
- Embedding Degree Check:
```
embedding_degree = calculate_embedding_degree(E)
assert embedding_degree.nbits() > EMBEDDING_DEGREE_SECURITY
```
- Twist Security:
  - Pollard-Rho Resistance
  - Embedding Degree Check
Step 4: Complex Discriminant Verification

Check discriminant condition for secure parameterization: $D=(P^7 + 1 − n)^ 2 - 4P^7$ , where $n$ is the full order of the original curve. Where $\text{D}$ must satisfies:
- Large negative integer (absolute value > 100 bits)
- Square-free part > 100 bits
Validation command: sage verify.sage

The selected curve achieves >100-bit security. This construction follows NIST-recommended practices while optimizing for zkSNARK arithmetic circuits through sparse polynomial selection and small curve coefficients.