[WIP] Functions for RangeCheck64 in MIPS

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;

o1vm/src/mips/constraints.rs

@@ -152,6 +152,10 @@ impl<Fp: Field> InterpreterEnv for Env<Fp> {
     }
 
     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))))
     }
 

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,

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,16 +289,18 @@ impl<Fp: Field, PreImageOracle: PreImageOracleT> InterpreterEnv for Env<Fp, PreI
         x as u64
     }
 
+    fn constant64(x: u64) -> Self::Variable {
+        x
+    }
+
     unsafe fn bitmask(
         &mut self,
         x: &Self::Variable,
         highest_bit: u32,
         lowest_bit: u32,
         position: Self::Position,
     ) -> 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
     }