Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: fix memory as to 2 for rv32 loadstore #1310

Closed
wants to merge 1 commit into from
Closed

feat: fix memory as to 2 for rv32 loadstore #1310

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 9 additions & 11 deletions docs/specs/ISA.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down
12 changes: 4 additions & 8 deletions extensions/rv32im/circuit/src/adapters/loadstore.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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, *};
Expand Down Expand Up @@ -130,7 +130,6 @@ pub struct Rv32LoadStoreReadRecord<F: Field> {
pub imm: F,
pub imm_sign: bool,
pub mem_ptr_limbs: [u32; 2],
pub mem_as: F,
pub shift_amount: u32,
}

Expand Down Expand Up @@ -158,7 +157,6 @@ pub struct Rv32LoadStoreAdapterCols<T> {
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<T>,
}
Expand Down Expand Up @@ -255,7 +253,7 @@ impl<AB: InteractionBuilder> VmAdapterAir<AB> for Rv32LoadStoreAdapterAir {
// read_as is 2 for loads and 1 for stores
let read_as = select::<AB::Expr>(
is_load.clone(),
local_cols.mem_as,
AB::F::from_canonical_u32(RV32_MEMORY_AS),
AB::F::from_canonical_u32(RV32_REGISTER_AS),
);

Expand All @@ -281,7 +279,7 @@ impl<AB: InteractionBuilder> VmAdapterAir<AB> for Rv32LoadStoreAdapterAir {
let write_as = select::<AB::Expr>(
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
Expand All @@ -308,7 +306,7 @@ impl<AB: InteractionBuilder> VmAdapterAir<AB> 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 {
Expand Down Expand Up @@ -403,7 +401,6 @@ impl<F: PrimeField32> VmAdapterChip<F> for Rv32LoadStoreAdapterChip<F> {
imm_sign: imm_sign == 1,
shift_amount,
mem_ptr_limbs,
mem_as: e,
},
))
}
Expand Down Expand Up @@ -477,7 +474,6 @@ impl<F: PrimeField32> VmAdapterChip<F> for Rv32LoadStoreAdapterChip<F> {
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 {
Expand Down
Loading