diff --git a/docs/specs/ISA.md b/docs/specs/ISA.md index a744543ce..e31a19689 100644 --- a/docs/specs/ISA.md +++ b/docs/specs/ISA.md @@ -174,9 +174,7 @@ unsigned integer, and convert to field element. In the instructions below, `[c:4 #### Load/Store -For all load/store instructions, we assume the operand `c` is in `[0, 2^16)`, and we fix address spaces `d = 1`. -The address space `e` can be any [valid address space](#addressing). -We will use shorthand `r32{c}(b) := i32([b:4]_1) + sign_extend(decompose(c)[0:2])` as `i32`. This means we interpret `c` +For all load/store instructions, we assume the operand `c` is in `[0, 2^16)`, and we fix address spaces `d = 1` and `e = 2`. We will use the shorthand `r32{c}(b) := i32([b:4]_1) + sign_extend(decompose(c)[0:2])` as `i32`. This means we interpret `c` as the 2's complement encoding of a 16-bit integer, sign extend it to 32-bits, and then perform signed 32-bit addition with the value of the register `[b:4]_1`. Memory access to `ptr: i32` is only valid if `0 <= ptr < 2^addr_max_bits`, in which case it is an access to @@ -186,14 +184,14 @@ All load/store instructions always do block accesses of block size `4`, even for | Name | Operands | Description | | ----------- | ----------- | ------------------------------------------------------------------------------------------------------------------------------ | -| LOADB_RV32 | `a,b,c,1,e` | `[a:4]_1 = sign_extend([r32{c}(b):1]_e)` Must sign-extend the byte read from memory, which is represented in 2’s complement. | -| LOADH_RV32 | `a,b,c,1,e` | `[a:4]_1 = sign_extend([r32{c}(b):2]_e)` Must sign-extend the number read from memory, which is represented in 2’s complement. | -| LOADW_RV32 | `a,b,c,1,e` | `[a:4]_1 = [r32{c}(b):4]_e` | -| LOADBU_RV32 | `a,b,c,1,e` | `[a:4]_1 = zero_extend([r32{c}(b):1]_e)` Must zero-extend the number read from memory. | -| LOADHU_RV32 | `a,b,c,1,e` | `[a:4]_1 = zero_extend([r32{c}(b):2]_e)` Must zero-extend the number read from memory. | -| STOREB_RV32 | `a,b,c,1,e` | `[r32{c}(b):1]_e <- [a:1]_1` | -| STOREH_RV32 | `a,b,c,1,e` | `[r32{c}(b):2]_e <- [a:2]_1` | -| STOREW_RV32 | `a,b,c,1,e` | `[r32{c}(b):4]_e <- [a:4]_1` | +| LOADB_RV32 | `a,b,c,1,2` | `[a:4]_1 = sign_extend([r32{c}(b):1]_2)` Must sign-extend the byte read from memory, which is represented in 2’s complement. | +| LOADH_RV32 | `a,b,c,1,2` | `[a:4]_1 = sign_extend([r32{c}(b):2]_2)` Must sign-extend the number read from memory, which is represented in 2’s complement. | +| LOADW_RV32 | `a,b,c,1,2` | `[a:4]_1 = [r32{c}(b):4]_2` | +| LOADBU_RV32 | `a,b,c,1,2` | `[a:4]_1 = zero_extend([r32{c}(b):1]_2)` Must zero-extend the number read from memory. | +| LOADHU_RV32 | `a,b,c,1,2` | `[a:4]_1 = zero_extend([r32{c}(b):2]_2)` Must zero-extend the number read from memory. | +| STOREB_RV32 | `a,b,c,1,2` | `[r32{c}(b):1]_2 <- [a:1]_1` | +| STOREH_RV32 | `a,b,c,1,2` | `[r32{c}(b):2]_2 <- [a:2]_1` | +| STOREW_RV32 | `a,b,c,1,2` | `[r32{c}(b):4]_2 <- [a:4]_1` | #### Branch/Jump/Upper Immediate diff --git a/extensions/rv32im/circuit/src/adapters/loadstore.rs b/extensions/rv32im/circuit/src/adapters/loadstore.rs index be0253799..cfa2ee9a7 100644 --- a/extensions/rv32im/circuit/src/adapters/loadstore.rs +++ b/extensions/rv32im/circuit/src/adapters/loadstore.rs @@ -27,7 +27,7 @@ use openvm_circuit_primitives_derive::AlignedBorrow; use openvm_instructions::{ instruction::Instruction, program::DEFAULT_PC_STEP, - riscv::{RV32_IMM_AS, RV32_REGISTER_AS}, + riscv::{RV32_IMM_AS, RV32_MEMORY_AS, RV32_REGISTER_AS}, LocalOpcode, }; use openvm_rv32im_transpiler::Rv32LoadStoreOpcode::{self, *}; @@ -130,7 +130,6 @@ pub struct Rv32LoadStoreReadRecord { pub imm: F, pub imm_sign: bool, pub mem_ptr_limbs: [u32; 2], - pub mem_as: F, pub shift_amount: u32, } @@ -158,7 +157,6 @@ pub struct Rv32LoadStoreAdapterCols { pub imm_sign: T, /// mem_ptr is the intermediate memory pointer limbs, needed to check the correct addition pub mem_ptr_limbs: [T; 2], - pub mem_as: T, /// prev_data will be provided by the core chip to make a complete MemoryWriteAuxCols pub write_base_aux: MemoryBaseAuxCols, } @@ -255,7 +253,7 @@ impl VmAdapterAir for Rv32LoadStoreAdapterAir { // read_as is 2 for loads and 1 for stores let read_as = select::( is_load.clone(), - local_cols.mem_as, + AB::F::from_canonical_u32(RV32_MEMORY_AS), AB::F::from_canonical_u32(RV32_REGISTER_AS), ); @@ -281,7 +279,7 @@ impl VmAdapterAir for Rv32LoadStoreAdapterAir { let write_as = select::( is_load.clone(), AB::F::from_canonical_u32(RV32_REGISTER_AS), - local_cols.mem_as, + AB::F::from_canonical_u32(RV32_MEMORY_AS), ); // write_ptr is rd_rs2_ptr for loads and mem_ptr for stores @@ -308,7 +306,7 @@ impl VmAdapterAir for Rv32LoadStoreAdapterAir { local_cols.rs1_ptr.into(), local_cols.imm.into(), AB::Expr::from_canonical_u32(RV32_REGISTER_AS), - local_cols.mem_as.into(), + AB::Expr::from_canonical_u32(RV32_MEMORY_AS), ], local_cols.from_state, ExecutionState { @@ -403,7 +401,6 @@ impl VmAdapterChip for Rv32LoadStoreAdapterChip { imm_sign: imm_sign == 1, shift_amount, mem_ptr_limbs, - mem_as: e, }, )) } @@ -477,7 +474,6 @@ impl VmAdapterChip for Rv32LoadStoreAdapterChip { adapter_cols.mem_ptr_limbs = read_record.mem_ptr_limbs.map(F::from_canonical_u32); let write = memory.record_by_id(write_record.write_id); aux_cols_factory.generate_base_aux(write, &mut adapter_cols.write_base_aux); - adapter_cols.mem_as = read_record.mem_as; } fn air(&self) -> &Self::Air {