From 4a7df608dc1411eba71e734d3a100d653346939e Mon Sep 17 00:00:00 2001 From: querolita Date: Sat, 6 Jul 2024 20:01:25 +0200 Subject: [PATCH] rangecheck64 initial ideas --- o1vm/src/mips/column.rs | 14 ++++++------ o1vm/src/mips/constraints.rs | 4 ++++ o1vm/src/mips/interpreter.rs | 43 +++++++++++++++++++++++++++++++++--- o1vm/src/mips/witness.rs | 9 +++++--- 4 files changed, 57 insertions(+), 13 deletions(-) diff --git a/o1vm/src/mips/column.rs b/o1vm/src/mips/column.rs index 5d1af8f936..e8b3097142 100644 --- a/o1vm/src/mips/column.rs +++ b/o1vm/src/mips/column.rs @@ -12,22 +12,22 @@ use strum::EnumCount; use super::{ITypeInstruction, JTypeInstruction, RTypeInstruction}; /// The number of hashes performed so far in the block -pub(crate) const MIPS_HASH_COUNTER_OFF: usize = 80; +pub(crate) const MIPS_HASH_COUNTER_OFF: usize = 128; /// The number of bytes of the preimage that have been read so far in this hash -pub(crate) const MIPS_BYTE_COUNTER_OFF: usize = 81; +pub(crate) const MIPS_BYTE_COUNTER_OFF: usize = 129; /// A flag indicating whether the preimage has been read fully or not -pub(crate) const MIPS_END_OF_PREIMAGE_OFF: usize = 82; +pub(crate) const MIPS_END_OF_PREIMAGE_OFF: usize = 130; /// The number of preimage bytes processed in this step -pub(crate) const MIPS_NUM_BYTES_READ_OFF: usize = 83; +pub(crate) const MIPS_NUM_BYTES_READ_OFF: usize = 131; /// The at most 4-byte chunk of the preimage that has been read in this step. /// Contains a field element of at most 4 bytes. -pub(crate) const MIPS_PREIMAGE_CHUNK_OFF: usize = 84; +pub(crate) const MIPS_PREIMAGE_CHUNK_OFF: usize = 132; /// The at most 4-bytes of the preimage that are currently being processed /// Consists of 4 field elements of at most 1 byte each. -pub(crate) const MIPS_PREIMAGE_BYTES_OFF: usize = 85; +pub(crate) const MIPS_PREIMAGE_BYTES_OFF: usize = 133; /// Flags indicating whether at least N bytes have been processed in this step. /// Contains 4 field elements of boolean type each. -pub(crate) const MIPS_HAS_N_BYTES_OFF: usize = 89; +pub(crate) const MIPS_HAS_N_BYTES_OFF: usize = 137; /// The number of columns used for relation witness in the MIPS circuit pub const N_MIPS_REL_COLS: usize = SCRATCH_SIZE + 2; diff --git a/o1vm/src/mips/constraints.rs b/o1vm/src/mips/constraints.rs index bb0a161f18..c936f84e16 100644 --- a/o1vm/src/mips/constraints.rs +++ b/o1vm/src/mips/constraints.rs @@ -152,6 +152,10 @@ impl InterpreterEnv for Env { } fn constant(x: u32) -> Self::Variable { + Self::constant64(x as u64) + } + + fn constant64(x: u64) -> Self::Variable { Self::Variable::constant(Operations::from(Literal(Fp::from(x)))) } diff --git a/o1vm/src/mips/interpreter.rs b/o1vm/src/mips/interpreter.rs index e8e53896ec..1f679ff092 100644 --- a/o1vm/src/mips/interpreter.rs +++ b/o1vm/src/mips/interpreter.rs @@ -539,8 +539,44 @@ pub trait InterpreterEnv { self.lookup_8bits(&(value.clone() + Self::constant(1 << 8) - Self::constant(1 << bits))); } - fn range_check64(&mut self, _value: &Self::Variable) { - // TODO + /// Checks that a value is at most 64 bits in length. + /// For this, it decomposes the value into 4 chunks of at most 16 bits each + /// using bitmask, and range checks each chunk using the RangeCheck16Lookup + /// table. Finally, it adds one constraint to check the decomposition. + /// It allocates 4 scratch variables to store the chunks. + fn range_check64(&mut self, value: &Self::Variable) { + let [v0, v1, v2, v3] = [ + { + let pos = self.alloc_scratch(); + unsafe { self.bitmask(value, 64, 48, pos) } + }, + { + let pos = self.alloc_scratch(); + unsafe { self.bitmask(value, 48, 32, pos) } + }, + { + let pos = self.alloc_scratch(); + unsafe { self.bitmask(value, 32, 16, pos) } + }, + { + let pos = self.alloc_scratch(); + unsafe { self.bitmask(value, 16, 0, pos) } + }, + ]; + self.lookup_16bits(&v0); + self.lookup_16bits(&v1); + self.lookup_16bits(&v2); + self.lookup_16bits(&v3); + // FIXME: uncomment the constraint below when it works + /* + self.add_constraint( + value.clone() + - (v0 * Self::constant64(1 << 48) + + v1 * Self::constant64(1 << 32) + + v2 * Self::constant(1 << 16) + + v3), + ); + */ } fn set_instruction_pointer(&mut self, ip: Self::Variable) { @@ -601,6 +637,8 @@ pub trait InterpreterEnv { fn constant(x: u32) -> Self::Variable; + fn constant64(x: u64) -> Self::Variable; + /// Extract the bits from the variable `x` between `highest_bit` and `lowest_bit`, and store /// the result in `position`. /// `lowest_bit` becomes the least-significant bit of the resulting value. @@ -611,7 +649,6 @@ pub trait InterpreterEnv { /// the source variable `x` and that the returned value fits in `highest_bit - lowest_bit` /// bits. /// - /// Do not call this function with highest_bit - lowest_bit >= 32. // TODO: embed the range check in the function when highest_bit - lowest_bit <= 16? unsafe fn bitmask( &mut self, diff --git a/o1vm/src/mips/witness.rs b/o1vm/src/mips/witness.rs index d771bea2ac..9b867b525a 100644 --- a/o1vm/src/mips/witness.rs +++ b/o1vm/src/mips/witness.rs @@ -44,7 +44,8 @@ pub const NUM_INSTRUCTION_LOOKUP_TERMS: usize = 5; pub const NUM_LOOKUP_TERMS: usize = NUM_GLOBAL_LOOKUP_TERMS + NUM_DECODING_LOOKUP_TERMS + NUM_INSTRUCTION_LOOKUP_TERMS; // TODO: Delete and use a vector instead -pub const SCRATCH_SIZE: usize = 93; // MIPS + hash_counter + chunk_read + bytes_read + bytes_left + bytes + has_n_bytes +// MIPS (includes rangecheck64) + hash_counter + chunk_read + bytes_read + bytes_left + bytes + has_n_bytes +pub const SCRATCH_SIZE: usize = 93 + (MAX_NB_MEM_ACC as usize) * 4; #[derive(Clone, Default)] pub struct SyscallEnv { @@ -288,6 +289,10 @@ impl InterpreterEnv for Env Self::Variable { + x + } + unsafe fn bitmask( &mut self, x: &Self::Variable, @@ -295,9 +300,7 @@ impl InterpreterEnv for Env Self::Variable { - let x: u32 = (*x).try_into().unwrap(); let res = (x >> lowest_bit) & ((1 << (highest_bit - lowest_bit)) - 1); - let res = res as u64; self.write_column(position, res); res }