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=;
  • All memory cells ai are initialized with some value vi at op count c=0. Add the initial tuples to the write set WS=WS{(ai,vi,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{(a,v,c)} and WS=WS{(a,v,cnow)}, with cnow 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{(a,v,c)} and WS=WS{(a,v,cnow)}.

Post-processing:

  • For all memory cells ai, add the last tuple (ai,vi,ci) in write set WS to RS: RS=RS{(ai,vi,ci)}.

Core Observation

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

  1. The read and write sets are correctly initialized;
  2. For each address ai, the instruction count added to WS strictly increases over time;
  3. ​For read operations: Tuples added to RS and WS must have the same value.
  4. ​For write operations: The operation counter of the tuple in RS must be less than that in WS.
  5. 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,vv,c) and added it to read set RS. Note that all tuples in WS are distinct. After adding (a,v,cnow) to WS, the tuples (a,v,c) and (a,v,cnow) 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 y2=x3+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: FP, with P=231224+1.
  • Septic extension field: Defined under irreducible polynomial u7+2u8.
  • Elliptic curve: Defined with A=3u,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=231224+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 264232+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: x7+2x8. This sparse form minimizes arithmetic complexity while ensuring irreducibility.
  • Step 2: Candidate Curve Filtering

    • ​Curve Form​​: y2=x3+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=(P7+1n)24P7, where n is the full order of the original curve. Where 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​​.