Skip to content

Commit 8638194

Browse files
authored
fix(new-execution): disable loads from address space 1 (#1802)
- update isa spec to specify that loads are only allowed from address space 2 - update isa spec to specify that the maximum valid pointer value in address space 1 is 127 - add a `debug_assert` that load address space is not 1 in loadstore instructions Towards INT-4237
1 parent 25ecd07 commit 8638194

File tree

3 files changed

+6
-7
lines changed

3 files changed

+6
-7
lines changed

docs/specs/ISA.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ address spaces and the size of each address space are configurable constants.
117117
- Valid pointers are field elements that lie in `[0, 2^pointer_max_bits)`, for
118118
configuration constant `pointer_max_bits`. When accessing an address out of `[0, 2^pointer_max_bits)`, the VM should
119119
panic.
120-
120+
- For the register address space (address space `1`), valid pointers lie in `[0, 128)`, corresponding to 32 registers with 4 byte limbs each.
121121
These configuration constants must satisfy `addr_space_height, pointer_max_bits <= F::bits() - 2`. We use the following notation
122122
to denote cells in memory:
123123

@@ -171,7 +171,7 @@ structures during runtime execution:
171171
- `hint_space`: a vector of vectors of field elements used to store hints during runtime execution
172172
via [phantom sub-instructions](#phantom-sub-instructions) such as `NativeHintLoad`. The outer `hint_space` vector is append-only, but
173173
each internal `hint_space[hint_id]` vector may be mutated, including deletions, by the host.
174-
- `kv_store`: a read-only key-value store for hints. Executors(e.g. `Rv32HintLoadByKey`) can read data from `kv_store`
174+
- `kv_store`: a read-only key-value store for hints. Executors(e.g. `Rv32HintLoadByKey`) can read data from `kv_store`
175175
at runtime. `kv_store` is designed for general purposes so both key and value are byte arrays. Encoding of key/value
176176
are decided by each executor. Users need to use the corresponding encoding when adding data to `kv_store`.
177177

@@ -327,7 +327,7 @@ unsigned integer, and convert to field element. In the instructions below, `[c:4
327327
#### Load/Store
328328

329329
For all load/store instructions, we assume the operand `c` is in `[0, 2^16)`, and we fix address spaces `d = 1`.
330-
The address space `e` can be `0`, `1`, or `2` for load instructions, and `2`, `3`, or `4` for store instructions.
330+
The address space `e` is `2` for load instructions, and can be `2`, `3`, or `4` for store instructions.
331331
The operand `g` must be a boolean. We let `sign_extend(decompose(c)[0:2], g)` denote the `i32` defined by first taking
332332
the unsigned integer encoding of `c` as 16 bits, then sign extending it to 32 bits using the sign bit `g`, and considering
333333
the 32 bits as the 2's complement of an `i32`.

extensions/rv32im/circuit/src/adapters/loadstore.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -368,6 +368,7 @@ where
368368

369369
debug_assert_eq!(d.as_canonical_u32(), RV32_REGISTER_AS);
370370
debug_assert!(e.as_canonical_u32() != RV32_IMM_AS);
371+
debug_assert!(e.as_canonical_u32() != RV32_REGISTER_AS);
371372

372373
let local_opcode = Rv32LoadStoreOpcode::from_usize(
373374
opcode.local_opcode_idx(Rv32LoadStoreOpcode::CLASS_OFFSET),
@@ -449,6 +450,7 @@ where
449450

450451
debug_assert_eq!(d.as_canonical_u32(), RV32_REGISTER_AS);
451452
debug_assert!(e.as_canonical_u32() != RV32_IMM_AS);
453+
debug_assert!(e.as_canonical_u32() != RV32_REGISTER_AS);
452454

453455
let local_opcode = Rv32LoadStoreOpcode::from_usize(
454456
opcode.local_opcode_idx(Rv32LoadStoreOpcode::CLASS_OFFSET),

extensions/rv32im/circuit/src/loadstore/tests.rs

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ fn set_and_execute(
9191

9292
let is_load = [LOADW, LOADHU, LOADBU].contains(&opcode);
9393
let mem_as = mem_as.unwrap_or(if is_load {
94-
*[1, 2].choose(rng).unwrap()
94+
2
9595
} else {
9696
*[2, 3, 4].choose(rng).unwrap()
9797
});
@@ -109,9 +109,6 @@ fn set_and_execute(
109109
some_prev_data = [F::ZERO; RV32_REGISTER_NUM_LIMBS];
110110
}
111111
tester.write(1, a, some_prev_data);
112-
if mem_as == 1 && ptr_val - shift_amount == 0 {
113-
read_data = [F::ZERO; RV32_REGISTER_NUM_LIMBS];
114-
}
115112
tester.write(mem_as, (ptr_val - shift_amount) as usize, read_data);
116113
} else {
117114
if mem_as == 4 {

0 commit comments

Comments
 (0)