Skip to content

Commit 56e4f86

Browse files
876polshuklaayush
authored andcommitted
feat: rv64 more cleanup (#2752)
1 parent 507dc96 commit 56e4f86

19 files changed

Lines changed: 85 additions & 133 deletions

File tree

extensions/deferral/circuit/src/call/execution.rs

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ use crate::{
2222
poseidon2::deferral_poseidon2_chip,
2323
utils::{
2424
byte_commit_to_f, combine_output, join_memory_ops, memory_op_chunk, COMMIT_MEMORY_OPS,
25-
COMMIT_NUM_BYTES, DIGEST_MEMORY_OPS, OUTPUT_TOTAL_MEMORY_OPS,
25+
COMMIT_NUM_BYTES, DIGEST_MEMORY_OPS, OUTPUT_LEN_NUM_BYTES, OUTPUT_TOTAL_MEMORY_OPS,
2626
},
2727
DeferralFn, CALL_AIR_REL_IDX, POSEIDON2_AIR_REL_IDX,
2828
};
@@ -204,8 +204,13 @@ unsafe fn execute_e12_impl<F: VmField, CTX: ExecutionCtxTrait>(
204204
let output_f_commit =
205205
byte_commit_to_f(&output_commit.iter().map(|v| F::from_u8(*v)).collect_vec());
206206

207-
// (output_commit, output_len) pair, corresponds to guest struct OutputKey
208-
let output_key = combine_output(output_commit, output_len.to_le_bytes());
207+
let output_len_u32 =
208+
u32::try_from(output_len).expect("deferral output length should fit in a u32");
209+
let mut output_len_full = [0u8; OUTPUT_LEN_NUM_BYTES];
210+
output_len_full[..4].copy_from_slice(&output_len_u32.to_le_bytes());
211+
212+
// (output_commit, output_len) pair, corresponds to guest struct OutputKey.
213+
let output_key = combine_output(output_commit, output_len_full);
209214

210215
let new_input_acc = poseidon2_chip.perm(&old_input_acc, &input_commit, true);
211216
let new_output_acc = poseidon2_chip.perm(&old_output_acc, &output_f_commit, true);

extensions/deferral/circuit/src/output/execution.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -163,7 +163,7 @@ unsafe fn execute_e12_impl<F: PrimeField32, CTX: ExecutionCtxTrait>(
163163
let output_key: [u8; OUTPUT_TOTAL_BYTES] = join_memory_ops(output_key_chunks);
164164
let (output_commit, output_len) = split_output(output_key);
165165

166-
let output_len_val = u64::from_le_bytes(output_len) as usize;
166+
let output_len_val = rv64_bytes_to_u32(output_len) as usize;
167167

168168
// Bytes are sponge-hashed and constrained against output_commit. The
169169
// sponge rate is DIGEST_SIZE.

extensions/deferral/circuit/src/output/trace.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -189,7 +189,7 @@ where
189189
let output_key: [u8; OUTPUT_TOTAL_BYTES] = join_memory_ops(output_key_chunks);
190190
let (output_commit, output_len) = split_output(output_key);
191191

192-
let output_len_val = u64::from_le_bytes(output_len) as usize;
192+
let output_len_val = rv64_bytes_to_u32(output_len) as usize;
193193
let num_rows = output_len_val / DIGEST_SIZE + 1;
194194
debug_assert!(output_len_val.is_multiple_of(DIGEST_SIZE));
195195

extensions/riscv-adapters/src/eq_mod.rs

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -29,17 +29,15 @@ use openvm_instructions::{
2929
riscv::{RV64_MEMORY_AS, RV64_REGISTER_AS, RV64_WORD_NUM_LIMBS},
3030
};
3131
use openvm_riscv_circuit::adapters::{
32-
abstract_compose, expand_to_rv64_register, tracing_read, tracing_write, RV64_CELL_BITS,
33-
RV64_REGISTER_NUM_LIMBS,
32+
abstract_compose, expand_to_rv64_register, tracing_read, tracing_read_reg_ptr, tracing_write,
33+
RV64_CELL_BITS, RV64_REGISTER_NUM_LIMBS,
3434
};
3535
use openvm_stark_backend::{
3636
interaction::InteractionBuilder,
3737
p3_air::BaseAir,
3838
p3_field::{Field, PrimeCharacteristicRing, PrimeField32},
3939
};
4040

41-
use crate::helpers::tracing_read_reg_ptr;
42-
4341
/// This adapter reads from NUM_READS <= 2 pointers and writes to a register.
4442
/// * The data is read from the heap (address space 2), and the pointers are read from registers
4543
/// (address space 1).
@@ -329,6 +327,7 @@ where
329327
memory,
330328
record.rs_ptr[i],
331329
&mut record.rs_read_aux[i].prev_timestamp,
330+
self.pointer_max_bits,
332331
)
333332
});
334333

extensions/riscv-adapters/src/helpers.rs

Lines changed: 0 additions & 17 deletions
This file was deleted.

extensions/riscv-adapters/src/lib.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
mod eq_mod;
2-
mod helpers;
32
mod vec_heap;
43
mod vec_heap_branch;
54
mod vec_to_flat;

extensions/riscv-adapters/src/vec_heap.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,16 +30,15 @@ use openvm_instructions::{
3030
riscv::{RV64_MEMORY_AS, RV64_REGISTER_AS, RV64_WORD_NUM_LIMBS},
3131
};
3232
use openvm_riscv_circuit::adapters::{
33-
abstract_compose, expand_to_rv64_register, tracing_read, tracing_write, RV64_CELL_BITS,
33+
abstract_compose, expand_to_rv64_register, tracing_read, tracing_read_reg_ptr, tracing_write,
34+
RV64_CELL_BITS,
3435
};
3536
use openvm_stark_backend::{
3637
interaction::InteractionBuilder,
3738
p3_air::BaseAir,
3839
p3_field::{Field, PrimeCharacteristicRing, PrimeField32},
3940
};
4041

41-
use crate::helpers::tracing_read_reg_ptr;
42-
4342
/// This adapter reads from R (R <= 2) pointers and writes to 1 pointer.
4443
/// * The data is read from the heap (address space 2), and the pointers are read from registers
4544
/// (address space 1).
@@ -376,6 +375,7 @@ impl<
376375
memory,
377376
record.rs_ptrs[i],
378377
&mut record.rs_read_aux[i].prev_timestamp,
378+
self.pointer_max_bits,
379379
)
380380
});
381381

@@ -384,6 +384,7 @@ impl<
384384
memory,
385385
record.rd_ptr,
386386
&mut record.rd_read_aux.prev_timestamp,
387+
self.pointer_max_bits,
387388
);
388389

389390
// Read memory values

extensions/riscv-adapters/src/vec_heap_branch.rs

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -27,16 +27,14 @@ use openvm_instructions::{
2727
riscv::{RV64_MEMORY_AS, RV64_REGISTER_AS, RV64_WORD_NUM_LIMBS},
2828
};
2929
use openvm_riscv_circuit::adapters::{
30-
abstract_compose, expand_to_rv64_register, tracing_read, RV64_CELL_BITS,
30+
abstract_compose, expand_to_rv64_register, tracing_read, tracing_read_reg_ptr, RV64_CELL_BITS,
3131
};
3232
use openvm_stark_backend::{
3333
interaction::InteractionBuilder,
3434
p3_air::BaseAir,
3535
p3_field::{Field, PrimeCharacteristicRing, PrimeField32},
3636
};
3737

38-
use crate::helpers::tracing_read_reg_ptr;
39-
4038
/// This adapter reads from NUM_READS <= 2 pointers (for branch operations).
4139
/// * The data is read from the heap (address space 2), and the pointers are read from registers
4240
/// (address space 1).
@@ -273,6 +271,7 @@ impl<
273271
memory,
274272
record.rs_ptrs[i],
275273
&mut record.rs_read_aux[i].prev_timestamp,
274+
self.pointer_max_bits,
276275
)
277276
});
278277

extensions/riscv/circuit/src/adapters/loadstore.rs

Lines changed: 4 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -39,8 +39,8 @@ use openvm_stark_backend::{
3939

4040
use super::{RV64_REGISTER_NUM_LIMBS, RV64_WORD_NUM_LIMBS};
4141
use crate::adapters::{
42-
expand_to_rv64_register, memory_read, memory_read_deferral, timed_write, timed_write_deferral,
43-
tracing_read, RV64_CELL_BITS,
42+
expand_to_rv64_register, memory_read, memory_read_deferral, rv64_bytes_to_u32, timed_write,
43+
timed_write_deferral, tracing_read, RV64_CELL_BITS,
4444
};
4545

4646
/// LoadStore Adapter handles all memory and register operations, so it must be aware
@@ -371,18 +371,12 @@ where
371371
);
372372

373373
record.rs1_ptr = b.as_canonical_u32();
374-
let rs1_u64 = u64::from_le_bytes(tracing_read(
374+
record.rs1_val = rv64_bytes_to_u32(tracing_read(
375375
memory,
376376
RV64_REGISTER_AS,
377377
record.rs1_ptr,
378378
&mut record.rs1_aux_record.prev_timestamp,
379379
));
380-
assert_eq!(
381-
rs1_u64 >> 32,
382-
0,
383-
"rs1 upper 4 bytes must be zero for load/store adapter"
384-
);
385-
record.rs1_val = rs1_u64 as u32;
386380
let rs1_val = record.rs1_val;
387381

388382
record.imm = c.as_canonical_u32() as u16;
@@ -393,12 +387,7 @@ where
393387
let shift_amount = ptr_val & (RV64_REGISTER_NUM_LIMBS as u32 - 1);
394388
let ptr_val = ptr_val - shift_amount;
395389

396-
assert!(
397-
ptr_val < (1 << self.pointer_max_bits),
398-
"ptr_val: {ptr_val} = rs1_val: {} + imm_extended: {imm_extended} >= 2 ** {}",
399-
rs1_val,
400-
self.pointer_max_bits
401-
);
390+
debug_assert!((ptr_val as u64) < (1u64 << self.pointer_max_bits));
402391

403392
// prev_data: We need to keep values of some cells to keep them unchanged when writing to
404393
// those cells

extensions/riscv/circuit/src/adapters/mod.rs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -218,6 +218,22 @@ pub fn tracing_read<const N: usize>(
218218
data
219219
}
220220

221+
/// Reads an RV64 register, records the memory access, and returns the low 32 bits. Debug-asserts
222+
/// the returned value fits in `pointer_max_bits` (which, for `pointer_max_bits <= 32`, also
223+
/// implies the upper 32 bits are zero).
224+
#[inline(always)]
225+
pub fn tracing_read_reg_ptr(
226+
memory: &mut TracingMemory,
227+
ptr: u32,
228+
prev_timestamp: &mut u32,
229+
pointer_max_bits: usize,
230+
) -> u32 {
231+
let bytes = tracing_read(memory, RV64_REGISTER_AS, ptr, prev_timestamp);
232+
let val = rv64_bytes_to_u32(bytes);
233+
debug_assert!((val as u64) < (1u64 << pointer_max_bits));
234+
val
235+
}
236+
221237
#[inline(always)]
222238
pub fn tracing_read_imm(
223239
memory: &mut TracingMemory,

0 commit comments

Comments
 (0)