Feature/Implement memory consistency using Supernova

Cargo.toml

@@ -41,3 +41,5 @@ serde_json = "1.0.128"
 serde = "1.0.210"
 nova-snark = { git = "https://github.com/microsoft/Nova", default-features = false }
 bellpepper-core = { version="0.4.0", default-features = false }
+arecibo = { git = "https://github.com/argumentcomputer/arecibo" }
+

zkmemory/Cargo.toml

@@ -31,3 +31,4 @@ itertools = "0.13.0"
 nova-snark = { workspace = true }
 bellpepper-core = { workspace = true }
 poseidon = { path = "../poseidon" }
+arecibo = { workspace = true }

zkmemory/src/lib.rs

@@ -27,6 +27,8 @@ pub mod error;
 pub mod machine;
 /// Memory consistency circuit using Nova proof system
 pub mod nova;
+/// Memory consistency circuit using Supernova proof system
+pub mod supernova;
 #[cfg(test)]
 mod tests {
     extern crate alloc;

zkmemory/src/nova/memory_consistency_circuit.rs

@@ -12,6 +12,20 @@ use nova_snark::traits::{circuit::StepCircuit, Group};
 use poseidon::poseidon_hash::ConstantLength;
 use poseidon::poseidon_hash::Hash;
 use poseidon::poseidon_hash::Spec;
+// The memory consistency check is as follows:
+// Given an initial memory M and a trace record list (addr_i,instruction_i,value_i)_{i=1}^n
+// meaning that in step i, if instruction_i=0, then read value_i from M[addr_i]
+// else write value_i to M[addr_i]
+// Let M_j  denote the j-th state of the memory, then the constraints
+// are as follows:
+// 1) add_j<=|M|, 2) (instruction_j-1)*(M_j[addr_j]-val_j)=0
+// 3) instruction_j \in {0,1}
+// In the implementation, we let z_i to be the i-th memory state, and
+// the circuit has a witness input, the i-th trace record, consisting of
+// addr_i, instruction_i and value_i
+// We also introduce the commitment to the memory at the last cell of z_i
+// in application where one need to commit to the memory before proving.
+
 #[derive(Copy, Clone)]
 /// the trace record struct
 pub struct TraceRecord<G: Group> {
@@ -123,7 +137,9 @@ impl<
                 || "commitment to the memory must be valid",
                 |lc| lc + commitment.get_variable(),
                 |lc| lc + CS::one(),
-                |lc| lc + z_out[self.memory_len].get_variable(),
+                |lc: bellpepper_core::LinearCombination<_>| {
+                    lc + z_out[self.memory_len].get_variable()
+                },
             );
 
             // if instruction = 0 then memory[address]=value

zkmemory/src/nova/testcases.rs

@@ -44,8 +44,17 @@ mod test {
     }
 
     #[test]
-    // test correct memory consistency in one step
-    // for simplicity we experiment with a memory of size 4 only
+    // To check memory consistency, customize the inputs (z0_primary, address,
+    // instruction, value) as the example below, where:
+    // z0_primary consists of the initial memory (M[0]) and its commitment, and
+    // address=(addr_i)_{i=1}^n, instruction=(instruction_i)_{i=1}^n
+    // and value=(value_i)_{i=1}^n, which are the address, instruction
+    // and values representing the change of the memory from step 1 to n
+    // which we have mentioned in the file memory_consistency_circuit.rs
+    // So to use this for applications, change z_primary with your
+    // initial memory state, and address, instruction and value with
+    // your trace record.
+
     fn test_memory_consistency_in_one_step() {
         let address = [0_u64].to_vec();
         let instruction = [1_u64].to_vec();