review comments

Author: jonathanpwang

docs/specs/ISA.md

@@ -418,7 +418,7 @@ with user input-output.
 
 | Name             | Operands        | Description                                                                                                                                                                       |
 | ---------------- | --------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
-| HINT_STOREW_RV32 | `_,b,_,1,2`     | `[r32{0}(b):4]_2 = next 4 bytes from hint stream`. Only valid if next 4 values in hint stream are bytes.                                                                          |
+| HINT_STOREW_RV32 | `_,b,_,1,2`     | `[r32{0}(b):4]_2 = next 4 bytes from hint stream`. Only valid if next 4 values in hint stream are bytes.  The pointer address `r32{0}(b)` must be divisible by 4. |
 | HINT_BUFFER_RV32 | `a,b,_,1,2`     | `[r32{0}(b):4 * l]_2 = next 4 * l bytes from hint stream` where `l = r32{0}(a)`. Only valid if next `4 * l` values in hint stream are bytes. Very important: `l` should not be 0. The pointer address `r32{0}(b)` must be divisible by 4. |
 | REVEAL_RV32      | `a,b,c,1,3,_,g` | Pseudo-instruction for `STOREW_RV32 a,b,c,1,3,_,g` writing to the user IO address space `3`. Only valid when continuations are enabled.                                           |
 

docs/specs/RISCV.md

@@ -62,7 +62,7 @@ as part of its state:
 
 | RISC-V Inst | FMT | opcode[6:0] | funct3 | imm[0:11] | RISC-V description and notes                                                                                                                                               |
 | ----------- | --- | ----------- | ------ | --------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
-| hintstorew  | I   | 0001011     | 001    | 0x0       | Stores next 4-byte word from hint stream in user memory at `[rd]_2`. Only valid if next 4 values in hint stream are bytes.                                                 |
+| hintstorew  | I   | 0001011     | 001    | 0x0       | Stores next 4-byte word from hint stream in user memory at `[rd]_2`. Only valid if next 4 values in hint stream are bytes. The address `rd` must be aligned to a 4-byte boundary. |
 | hintbuffer  | I   | 0001011     | 001    | 0x1       | Stores next `4 * rs1` bytes from hint stream in user memory at `[rd..rd + 4 * rs1]_2`. Only valid if next `4 * rs1` values in hint stream are bytes and `rs1` is non-zero. The address `rd` must be aligned to a 4-byte boundary. |
 | reveal      | I   | 0001011     | 010    |           | Stores the 4-byte word `rs1` at address `rd + imm` in user IO space. The address `rd + imm` must be aligned to a 4-byte boundary. |
 | hintinput   | I   | 0001011     | 011    | 0x0       | Pop next vector from input stream and reset hint stream to the vector.                                                                                                     |

extensions/rv32im/circuit/src/hintstore/mod.rs

@@ -36,6 +36,7 @@ use openvm_stark_backend::{
     p3_air::{Air, AirBuilder, BaseAir},
     p3_field::{Field, FieldAlgebra, PrimeField32},
     p3_matrix::{dense::RowMajorMatrix, Matrix},
+    p3_util::log2_strict_usize,
     prover::types::AirProofInput,
     rap::{AnyRap, BaseAirWithPublicValues, PartitionedBaseAir},
     Chip, ChipUsageGetter,
@@ -232,10 +233,12 @@ impl<AB: InteractionBuilder> Air<AB> for Rv32HintStoreAir {
         self.memory_bridge
             .range_bus()
             .range_check::<AB::Expr>(
-                local_cols.mem_ptr_limbs[0] * AB::F::from_canonical_u32(4).inverse(),
-                RV32_CELL_BITS - 2,
+                local_cols.mem_ptr_limbs[0]
+                    * AB::F::from_canonical_usize(RV32_REGISTER_NUM_LIMBS).inverse(),
+                RV32_CELL_BITS - log2_strict_usize(RV32_REGISTER_NUM_LIMBS),
             )
             .eval(builder, is_start.clone());
+        // We only check this on `is_start` since it is implied on non-start rows by the next_mem_ptr = mem_ptr + 4 constraint below
 
         // Checking that hint is bytes
         for i in 0..RV32_REGISTER_NUM_LIMBS / 2 {
@@ -366,7 +369,7 @@ impl<F: PrimeField32> InstructionExecutor<F> for Rv32HintStoreChip<F> {
 
         debug_assert!(mem_ptr <= (1 << self.air.pointer_max_bits));
         assert!(
-            mem_ptr % 4 == 0,
+            (mem_ptr as usize) % RV32_REGISTER_NUM_LIMBS == 0,
             "Memory pointer {mem_ptr} is not 4-byte aligned"
         );
 
@@ -478,9 +481,10 @@ impl<F: PrimeField32> Rv32HintStoreChip<F> {
             mem_ptr_msl << (RV32_REGISTER_NUM_LIMBS * RV32_CELL_BITS - pointer_max_bits),
             rem_words_msl << (RV32_REGISTER_NUM_LIMBS * RV32_CELL_BITS - pointer_max_bits),
         );
-        memory
-            .range_checker()
-            .add_count((mem_ptr & 0xff) >> 2, RV32_CELL_BITS - 2);
+        memory.range_checker().add_count(
+            (mem_ptr & ((1 << RV32_CELL_BITS) - 1)) >> 2,
+            RV32_CELL_BITS - 2,
+        );
         for (i, &(data, write)) in record.hints.iter().enumerate() {
             for half in 0..(RV32_REGISTER_NUM_LIMBS / 2) {
                 bitwise_lookup_chip.request_range(