From dcc5bcfe2176d45ccc121b512cf91090575818c1 Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Fri, 26 Jan 2024 23:59:19 +0800 Subject: [PATCH] fix soundness arguement on challenges --- src/gadgets/lookup.rs | 120 ++++++++++++++++++++++++++++++------------ src/lib.rs | 4 +- 2 files changed, 87 insertions(+), 37 deletions(-) diff --git a/src/gadgets/lookup.rs b/src/gadgets/lookup.rs index c84358617..5e176698c 100644 --- a/src/gadgets/lookup.rs +++ b/src/gadgets/lookup.rs @@ -43,9 +43,9 @@ pub fn alloc_const>(mut cs: CS, val: F) - #[derive(Clone, Debug)] pub enum RWTrace { /// read - Read(T, T, T), // addr, read_value, read_ts + Read(T, T, T, T), // addr, read_value, read_ts, write_ts /// write - Write(T, T, T, T), // addr, read_value, write_value, read_ts + Write(T, T, T, T, T), // addr, read_value, write_value, read_ts, write_ts } /// Lookup in R1CS @@ -83,7 +83,7 @@ impl LookupTrace { self.cursor, self.expected_rw_trace.len() ); - let RWTrace::Read(expected_addr, expected_read_value, expected_read_ts) = + let RWTrace::Read(expected_addr, expected_read_value, expected_read_ts, expected_write_ts) = self.expected_rw_trace[self.cursor] else { Err(SynthesisError::AssignmentMissing)? @@ -100,12 +100,14 @@ impl LookupTrace { let read_value = AllocatedNum::alloc(cs.namespace(|| "read_value"), || Ok(expected_read_value))?; let read_ts = AllocatedNum::alloc(cs.namespace(|| "read_ts"), || Ok(expected_read_ts))?; + let write_ts = AllocatedNum::alloc(cs.namespace(|| "write_ts"), || Ok(expected_write_ts))?; self .rw_trace_allocated_num .push(RWTrace::Read::>( addr.clone(), read_value.clone(), read_ts, + write_ts, )); // append read trace self.cursor += 1; @@ -128,8 +130,13 @@ impl LookupTrace { self.cursor, self.expected_rw_trace.len() ); - let RWTrace::Write(expected_addr, expected_read_value, expected_write_value, expected_read_ts) = - self.expected_rw_trace[self.cursor] + let RWTrace::Write( + expected_addr, + expected_read_value, + expected_write_value, + expected_read_ts, + expected_write_ts, + ) = self.expected_rw_trace[self.cursor] else { Err(SynthesisError::AssignmentMissing)? }; @@ -153,11 +160,14 @@ impl LookupTrace { AllocatedNum::alloc(cs.namespace(|| "read_value"), || Ok(expected_read_value))?; let expected_read_ts = AllocatedNum::alloc(cs.namespace(|| "read_ts"), || Ok(expected_read_ts))?; + let expected_write_ts = + AllocatedNum::alloc(cs.namespace(|| "write_ts"), || Ok(expected_write_ts))?; self.rw_trace_allocated_num.push(RWTrace::Write( addr.clone(), expected_read_value, value.clone(), expected_read_ts, + expected_write_ts, )); // append write trace self.cursor += 1; Ok(()) @@ -188,14 +198,14 @@ impl LookupTrace { { let mut ro = E2::ROCircuit::new( ro_const, - 1 + 3 * self.expected_rw_trace.len(), // prev_challenge + [(address, value, ts)] + 1 + 5 * self.expected_rw_trace.len(), // prev_challenge + [(address, read_value, read_ts, write_value, write_ts)] ); ro.absorb(prev_intermediate_gamma); let rw_trace_allocated_num = &self.rw_trace_allocated_num; let (next_RW_acc, next_global_ts) = rw_trace_allocated_num.iter().enumerate().try_fold( (prev_RW_acc.clone(), prev_global_ts.clone()), |(prev_RW_acc, prev_global_ts), (i, rwtrace)| match rwtrace { - RWTrace::Read(addr, read_value, expected_read_ts) => { + RWTrace::Read(addr, read_value, expected_read_ts, _) => { let (next_RW_acc, next_global_ts) = self.rw_operation_circuit( cs.namespace(|| format!("{}th read ", i)), addr, @@ -209,12 +219,14 @@ impl LookupTrace { ro.absorb(addr); ro.absorb(read_value); ro.absorb(expected_read_ts); + ro.absorb(read_value); + ro.absorb(&next_global_ts); Ok::<(AllocatedNum, AllocatedNum), SynthesisError>(( next_RW_acc, next_global_ts, )) } - RWTrace::Write(addr, read_value, write_value, read_ts) => { + RWTrace::Write(addr, read_value, write_value, read_ts, _) => { let (next_RW_acc, next_global_ts) = self.rw_operation_circuit( cs.namespace(|| format!("{}th write ", i)), addr, @@ -228,6 +240,8 @@ impl LookupTrace { ro.absorb(addr); ro.absorb(read_value); ro.absorb(read_ts); + ro.absorb(write_value); + ro.absorb(&next_global_ts); Ok::<(AllocatedNum, AllocatedNum), SynthesisError>(( next_RW_acc, next_global_ts, @@ -395,9 +409,12 @@ impl<'a, E: Engine> LookupTraceBuilder<'a, E> { .cloned() .unwrap_or((E::Scalar::ZERO, E::Scalar::ZERO)) }); - self - .rw_trace - .push(RWTrace::Read(addr, *value, E::Scalar::ZERO)); + self.rw_trace.push(RWTrace::Read( + addr, + *value, + E::Scalar::ZERO, + E::Scalar::ZERO, + )); *value } /// write value to lookup table @@ -417,6 +434,7 @@ impl<'a, E: Engine> LookupTraceBuilder<'a, E> { E::Scalar::ZERO, value, E::Scalar::ZERO, + E::Scalar::ZERO, )); // append read trace } @@ -432,41 +450,48 @@ impl<'a, E: Engine> LookupTraceBuilder<'a, E> { E2: Engine::Scalar>, { let mut hasher: ::RO = - ::RO::new(ro_consts, 1 + self.rw_trace.len() * 3); + ::RO::new(ro_consts, 1 + self.rw_trace.len() * 5); hasher.absorb(prev_intermediate_gamma); let rw_processed = self .rw_trace .drain(..) .map(|rwtrace| { - let (rw_trace_with_ts, addr, read_value, read_ts) = match rwtrace { - RWTrace::Read(addr, expected_read_value, _) => { - let (read_value, read_ts) = self.lookup.rw_operation(addr, None); + let (rw_trace_with_ts, addr, read_value, read_ts, write_value, write_ts) = match rwtrace { + RWTrace::Read(addr, expected_read_value, _, _) => { + let (read_value, read_ts, _, write_ts) = self.lookup.rw_operation(addr, None); assert_eq!( read_value, expected_read_value, "expected_read_value {:?} != read_value {:?}", expected_read_value, read_value ); ( - RWTrace::Read(addr, expected_read_value, read_ts), + RWTrace::Read(addr, expected_read_value, read_ts, write_ts), addr, expected_read_value, read_ts, + expected_read_value, + write_ts, ) } - RWTrace::Write(addr, _, write_value, _) => { - let (read_value, read_ts) = self.lookup.rw_operation(addr, Some(write_value)); + RWTrace::Write(addr, _, write_value, _, _) => { + let (read_value, read_ts, write_value, write_ts) = + self.lookup.rw_operation(addr, Some(write_value)); ( - RWTrace::Write(addr, read_value, write_value, read_ts), + RWTrace::Write(addr, read_value, write_value, read_ts, write_ts), addr, read_value, read_ts, + write_value, + write_ts, ) } }; hasher.absorb(addr); hasher.absorb(read_value); hasher.absorb(read_ts); + hasher.absorb(write_value); + hasher.absorb(write_ts); rw_trace_with_ts }) @@ -579,7 +604,7 @@ impl Lookup { self.map_aux.values() } - fn rw_operation(&mut self, addr: F, external_value: Option) -> (F, F) + fn rw_operation(&mut self, addr: F, external_value: Option) -> (F, F, F, F) where F: Ord, { @@ -603,7 +628,7 @@ impl Lookup { ); self.map_aux.insert(addr, (write_value, write_ts)); self.global_ts = write_ts; - (read_value, read_ts) + (read_value, read_ts, write_value, write_ts) } } @@ -728,20 +753,32 @@ mod test { let (next_intermediate_gamma, _) = lookup_trace_builder.snapshot::(ro_consts.clone(), prev_intermediate_gamma); - let mut hasher = ::RO::new(ro_consts, 1 + 3 * 4); + let mut hasher = ::RO::new(ro_consts, 1 + 5 * 4); hasher.absorb(prev_intermediate_gamma); + + hasher.absorb(::Scalar::ZERO); // addr 0 + hasher.absorb(::Scalar::ZERO); // read_value + hasher.absorb(::Scalar::ZERO); // read_ts + hasher.absorb(::Scalar::ZERO); // write_value + hasher.absorb(::Scalar::ONE); // write_ts + + hasher.absorb(::Scalar::ONE); // addr 1 + hasher.absorb(::Scalar::ONE); // read_value + hasher.absorb(::Scalar::ZERO); // read_ts + hasher.absorb(::Scalar::ONE); // write_value + hasher.absorb(::Scalar::from(2)); // write_ts + + hasher.absorb(::Scalar::ZERO); // addr 0 + hasher.absorb(::Scalar::ZERO); // read_value + hasher.absorb(::Scalar::ONE); // read_ts + hasher.absorb(::Scalar::from(111)); // write_value + hasher.absorb(::Scalar::from(3)); // write_ts + hasher.absorb(::Scalar::ZERO); // addr - hasher.absorb(::Scalar::ZERO); // value - hasher.absorb(::Scalar::ZERO); // ts - hasher.absorb(::Scalar::ONE); // addr - hasher.absorb(::Scalar::ONE); // value - hasher.absorb(::Scalar::ZERO); // ts - hasher.absorb(::Scalar::ZERO); // addr - hasher.absorb(::Scalar::ZERO); // value - hasher.absorb(::Scalar::ONE); // ts - hasher.absorb(::Scalar::ZERO); // addr - hasher.absorb(::Scalar::from(111)); // value - hasher.absorb(::Scalar::from(3)); // ts + hasher.absorb(::Scalar::from(111)); // read_value + hasher.absorb(::Scalar::from(3)); // read_ts + hasher.absorb(::Scalar::from(111)); // write_value + hasher.absorb(::Scalar::from(4)); // write_ts let res = hasher.squeeze(NUM_CHALLENGE_BITS); assert_eq!(scalar_as_base::(res), next_intermediate_gamma); } @@ -843,14 +880,20 @@ mod test { .unwrap() .neg()) ); - let mut hasher = ::RO::new(ro_consts, 7); + let mut hasher = ::RO::new(ro_consts, 1 + 5 * 2); hasher.absorb(prev_intermediate_gamma.get_value().unwrap()); + hasher.absorb(addr.get_value().unwrap()); hasher.absorb(read_value.get_value().unwrap()); hasher.absorb(::Scalar::ZERO); + hasher.absorb(read_value.get_value().unwrap()); + hasher.absorb(::Scalar::ONE); + hasher.absorb(addr.get_value().unwrap()); hasher.absorb(read_value.get_value().unwrap()); hasher.absorb(::Scalar::ONE); + hasher.absorb(read_value.get_value().unwrap()); + hasher.absorb(::Scalar::from(2)); let res = hasher.squeeze(NUM_CHALLENGE_BITS); assert_eq!( scalar_as_base::(res), @@ -956,14 +999,21 @@ mod test { .neg()) ); - let mut hasher = ::RO::new(ro_consts, 7); + let mut hasher = ::RO::new(ro_consts, 1 + 5 * 2); hasher.absorb(prev_intermediate_gamma.get_value().unwrap()); + hasher.absorb(addr.get_value().unwrap()); hasher.absorb(::Scalar::ZERO); hasher.absorb(::Scalar::ZERO); + hasher.absorb(write_value_1.get_value().unwrap()); + hasher.absorb(::Scalar::ONE); + hasher.absorb(addr.get_value().unwrap()); hasher.absorb(read_value.get_value().unwrap()); hasher.absorb(::Scalar::ONE); + hasher.absorb(read_value.get_value().unwrap()); + hasher.absorb(::Scalar::from(2)); + let res = hasher.squeeze(NUM_CHALLENGE_BITS); assert_eq!( scalar_as_base::(res), diff --git a/src/lib.rs b/src/lib.rs index 34e45c10e..724439493 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -2400,8 +2400,8 @@ mod tests { zn_primary[4] ); // global ts = number_of_iterated_nodes * (3r + 4w) operations - assert_eq!(pp.circuit_shape_primary.r1cs_shape.num_cons, 12608); - assert_eq!(pp.circuit_shape_primary.r1cs_shape.num_vars, 12612); + assert_eq!(pp.circuit_shape_primary.r1cs_shape.num_cons, 13385); + assert_eq!(pp.circuit_shape_primary.r1cs_shape.num_vars, 13396); assert_eq!(pp.circuit_shape_secondary.r1cs_shape.num_cons, 10357); assert_eq!(pp.circuit_shape_secondary.r1cs_shape.num_vars, 10337);