From 919510b577164bda907dabf6318a486f5e0d6b78 Mon Sep 17 00:00:00 2001 From: KimiWu Date: Wed, 10 Jul 2024 17:29:11 +0800 Subject: [PATCH] add next_memory_ts --- singer/src/instructions/riscv_add.rs | 52 +++++++++++++++++++++------- 1 file changed, 39 insertions(+), 13 deletions(-) diff --git a/singer/src/instructions/riscv_add.rs b/singer/src/instructions/riscv_add.rs index b59a6b128..45f923a53 100644 --- a/singer/src/instructions/riscv_add.rs +++ b/singer/src/instructions/riscv_add.rs @@ -37,6 +37,7 @@ register_witness!( rd => RegisterUInt::N_OPRAND_CELLS, next_pc => UIntAddSub::::N_NO_OVERFLOW_WITNESS_UNSAFE_CELLS, + next_memory_ts => UIntAddSub::::N_NO_OVERFLOW_WITNESS_CELLS, // instruction operation addend_0 => UInt64::N_OPRAND_CELLS, @@ -45,9 +46,9 @@ register_witness!( // register timestamps and comparison gadgets prev_rs1_ts => TSUInt::N_OPRAND_CELLS, - rs2_ts => TSUInt::N_OPRAND_CELLS, + prev_rs2_ts => TSUInt::N_OPRAND_CELLS, prev_rs1_ts_lt => UIntCmp::::N_WITNESS_CELLS, - rs2_ts_lt => UIntCmp::::N_WITNESS_CELLS + prev_rs2_ts_lt => UIntCmp::::N_WITNESS_CELLS } ); @@ -65,7 +66,6 @@ impl Instruction for RVAddInstruction { let clk = phase0[Self::phase0_clk().start]; let clk_expr = MixedCell::Cell(clk); let zero_cell_ids = [0]; - let stack_top_expr = MixedCell::Cell(0); // Bytecode check for (pc, add) rom_handler.bytecode_with_pc_opcode( @@ -90,19 +90,25 @@ impl Instruction for RVAddInstruction { 1, &phase0[Self::phase0_next_pc()], )?; + let next_memory_ts = rom_handler.add_ts_with_const( + &mut circuit_builder, + &memory_ts.try_into()?, + 1, + &phase0[Self::phase0_next_memory_ts()], + )?; ram_handler.state_out( &mut circuit_builder, next_pc.values(), &zero_cell_ids, - &memory_ts, - stack_top_expr, + &next_memory_ts.values(), + MixedCell::Cell(0), clk_expr.add(E::BaseField::ONE), ); // Register timestamp range check let prev_rs1_ts = (&phase0[Self::phase0_prev_rs1_ts()]).try_into()?; - let rs2_ts = (&phase0[Self::phase0_rs2_ts()]).try_into()?; + let prev_rs2_ts = (&phase0[Self::phase0_prev_rs2_ts()]).try_into()?; UIntCmp::::assert_lt( &mut circuit_builder, &mut rom_handler, @@ -113,9 +119,9 @@ impl Instruction for RVAddInstruction { UIntCmp::::assert_lt( &mut circuit_builder, &mut rom_handler, - &rs2_ts, + &prev_rs2_ts, &memory_ts.try_into()?, - &phase0[Self::phase0_rs2_ts_lt()], + &phase0[Self::phase0_prev_rs2_ts_lt()], )?; if cfg!(feature = "dbg-opcode") { println!( @@ -148,7 +154,7 @@ impl Instruction for RVAddInstruction { ram_handler.register_read( &mut circuit_builder, rs2, - rs2_ts.values(), + prev_rs2_ts.values(), &phase0[Self::phase0_addend_1()], ); ram_handler.register_store(&mut circuit_builder, rd, memory_ts, result.values()); @@ -209,17 +215,25 @@ mod test { map.insert("phase0_rd".to_string(), Self::phase0_rd()); map.insert("phase0_next_pc".to_string(), Self::phase0_next_pc()); + map.insert( + "phase0_next_memory_ts".to_string(), + Self::phase0_next_memory_ts(), + ); + map.insert("phase0_addend_0".to_string(), Self::phase0_addend_0()); map.insert("phase0_addend_1".to_string(), Self::phase0_addend_1()); map.insert("phase0_outcome".to_string(), Self::phase0_outcome()); map.insert("phase0_prev_rs1_ts".to_string(), Self::phase0_prev_rs1_ts()); - map.insert("phase0_rs2_ts".to_string(), Self::phase0_rs2_ts()); + map.insert("phase0_prev_rs2_ts".to_string(), Self::phase0_prev_rs2_ts()); map.insert( "phase0_prev_rs1_ts_lt".to_string(), Self::phase0_prev_rs1_ts_lt(), ); - map.insert("phase0_rs2_ts_lt".to_string(), Self::phase0_rs2_ts_lt()); + map.insert( + "phase0_prev_rs2_ts_lt".to_string(), + Self::phase0_prev_rs2_ts_lt(), + ); map } @@ -249,6 +263,15 @@ mod test { let mut phase0_values_map = BTreeMap::>::new(); phase0_values_map.insert("phase0_pc".to_string(), vec![Goldilocks::from(1u64)]); phase0_values_map.insert("phase0_memory_ts".to_string(), vec![Goldilocks::from(3u64)]); + phase0_values_map.insert( + "phase0_next_memory_ts".to_string(), + vec![ + Goldilocks::from(4u64), + Goldilocks::from(0u64), + Goldilocks::from(0u64), + Goldilocks::from(0u64), + ], + ); phase0_values_map.insert("phase0_clk".to_string(), vec![Goldilocks::from(1u64)]); phase0_values_map.insert( "phase0_next_pc".to_string(), @@ -287,11 +310,14 @@ mod test { Goldilocks::from(1u64), // borrow ], ); - phase0_values_map.insert("phase0_rs2_ts".to_string(), vec![Goldilocks::from(1u64)]); + phase0_values_map.insert( + "phase0_prev_rs2_ts".to_string(), + vec![Goldilocks::from(1u64)], + ); let m: u64 = (1 << get_uint_params::().1) - 2; let range_values = u2vec::<{ TSUInt::N_RANGE_CHECK_CELLS }, RANGE_CHIP_BIT_WIDTH>(m); phase0_values_map.insert( - "phase0_rs2_ts_lt".to_string(), + "phase0_prev_rs2_ts_lt".to_string(), vec![ Goldilocks::from(range_values[0]), Goldilocks::from(range_values[1]),