From a531b16c810d544a8189e889ddf3122ba29003ea Mon Sep 17 00:00:00 2001 From: svv232 Date: Fri, 25 Oct 2024 22:47:51 -0400 Subject: [PATCH] Adding new range check32 table implementation to add constraints for arithmetic results --- o1vm/src/interpreters/mips/interpreter.rs | 18 ++++++++++++++++ o1vm/src/lookups.rs | 25 ++++++++++++++++++++++- 2 files changed, 42 insertions(+), 1 deletion(-) diff --git a/o1vm/src/interpreters/mips/interpreter.rs b/o1vm/src/interpreters/mips/interpreter.rs index cd158c04be..52c46ed555 100644 --- a/o1vm/src/interpreters/mips/interpreter.rs +++ b/o1vm/src/interpreters/mips/interpreter.rs @@ -554,6 +554,24 @@ pub trait InterpreterEnv { self.lookup_2bits(value); } + // Adds a lookup to the ByteLookup table for each byte of a 32-bit value + fn lookup_32bits(&mut self, value: &Self::Variable) { + self.add_lookup(Lookup::read_one( + LookupTableIDs::ByteLookup, + vec![ + value.clone(), + value.clone() + Self::constant(1 << 8), + value.clone() + Self::constant(1 << 16), + value.clone() + Self::constant(1 << 24), + ], + )); + } + + /// Range checks with 4 lookups to the ByteLookup table that a value + fn range_check32(&mut self, value: &Self::Variable) { + self.lookup_32bits(value); + } + fn range_check64(&mut self, _value: &Self::Variable) { // TODO } diff --git a/o1vm/src/lookups.rs b/o1vm/src/lookups.rs index eff69771f3..2b51aa377c 100644 --- a/o1vm/src/lookups.rs +++ b/o1vm/src/lookups.rs @@ -51,6 +51,8 @@ pub enum LookupTableIDs { SyscallLookup = 9, /// Input/Output of Keccak steps KeccakStepLookup = 10, + /// Single-column table of 2^32 entries with the sparse representation of all values + RangeCheck32Lookup = 11, } impl LookupTableID for LookupTableIDs { @@ -71,6 +73,7 @@ impl LookupTableID for LookupTableIDs { 8 => RegisterLookup, 9 => SyscallLookup, 10 => KeccakStepLookup, + 11 => RangeCheck32Lookup, _ => panic!("Invalid table ID"), } } @@ -82,6 +85,7 @@ impl LookupTableID for LookupTableIDs { AtMost4Lookup => 5, ByteLookup => 1 << 8, RangeCheck16Lookup | SparseLookup | ResetLookup => 1 << 16, + RangeCheck32Lookup => 1 << 32, MemoryLookup | RegisterLookup | SyscallLookup | KeccakStepLookup => { panic!("RAM Tables do not have a fixed length") } @@ -91,7 +95,7 @@ impl LookupTableID for LookupTableIDs { fn is_fixed(&self) -> bool { match self { PadLookup | RoundConstantsLookup | AtMost4Lookup | ByteLookup | RangeCheck16Lookup - | SparseLookup | ResetLookup => true, + | SparseLookup | ResetLookup | RangeCheck32Lookup => true, MemoryLookup | RegisterLookup | SyscallLookup | KeccakStepLookup => false, } } @@ -117,6 +121,7 @@ impl LookupTableID for LookupTableIDs { Self::RegisterLookup, Self::SyscallLookup, Self::KeccakStepLookup, + Self::RangeCheck32Lookup, ] } } @@ -139,6 +144,8 @@ pub(crate) trait FixedLookupTables { fn table_sparse() -> LookupTable; /// Returns the reset table fn table_reset() -> LookupTable; + /// Returns the range check 32 table + fn table_range_check_32() -> LookupTable; } impl FixedLookupTables for LookupTable { @@ -160,6 +167,13 @@ impl FixedLookupTables for LookupTable { None } } + RangeCheck32Lookup => { + if idx < id.length() && table.entries[idx] == value { + Some(idx) + } else { + None + } + } PadLookup => { // Because this table starts with entry 1 if idx - 1 < id.length() && table.entries[idx - 1] == value { @@ -275,4 +289,13 @@ impl FixedLookupTables for LookupTable { .collect(), } } + + fn table_range_check_32() -> Self { + Self { + table_id: RangeCheck32Lookup, + entries: (0..RangeCheck32Lookup.length()) + .map(|i| vec![F::from(i as u32)]) + .collect(), + } + } }