Skip to content

Commit

Permalink
chore: rename SHINTW -> HINT_STOREW
Browse files Browse the repository at this point in the history
  • Loading branch information
yi-sun committed Jan 10, 2025
1 parent 26bf32e commit 68a2102
Show file tree
Hide file tree
Showing 9 changed files with 40 additions and 37 deletions.
4 changes: 2 additions & 2 deletions crates/vm/tests/integration_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -756,7 +756,7 @@ fn test_vm_hint() {
0,
0,
),
Instruction::from_isize(VmOpcode::with_default_offset(SHINTW), 32, 0, 0, 1, 2),
Instruction::from_isize(VmOpcode::with_default_offset(HINT_STOREW), 32, 0, 0, 1, 2),
Instruction::from_isize(VmOpcode::with_default_offset(LOADW), 38, 0, 32, 1, 2),
Instruction::large_from_isize(VmOpcode::with_default_offset(ADD), 44, 20, 0, 1, 1, 0, 0),
Instruction::from_isize(VmOpcode::with_default_offset(MUL), 24, 38, 1, 1, 0),
Expand All @@ -772,7 +772,7 @@ fn test_vm_hint() {
),
Instruction::from_isize(VmOpcode::with_default_offset(MUL), 0, 50, 1, 1, 0),
Instruction::large_from_isize(VmOpcode::with_default_offset(ADD), 0, 44, 0, 1, 1, 1, 0),
Instruction::from_isize(VmOpcode::with_default_offset(SHINTW), 0, 0, 0, 1, 2),
Instruction::from_isize(VmOpcode::with_default_offset(HINT_STOREW), 0, 0, 0, 1, 2),
Instruction::large_from_isize(VmOpcode::with_default_offset(ADD), 50, 50, 1, 1, 1, 0, 0),
Instruction::from_isize(
VmOpcode::with_default_offset(NativeBranchEqualOpcode(BNE)),
Expand Down
15 changes: 8 additions & 7 deletions docs/specs/ISA.md
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ addressable cells. Registers are represented using the [LIMB] format with `LIMB_
## Hints

The `input_stream` is a private non-interactive queue of vectors of field elements which is provided at the start of
runtime execution. The `hint_stream` is a queue of values that can be written to memory by calling the `HINTSTOREW_RV32` and `HINTSTORE` instructions. The `hint_stream` is populated via [phantom sub-instructions](#phantom-sub-instructions) such
runtime execution. The `hint_stream` is a queue of values that can be written to memory by calling the `HINT_STOREW_RV32` and `HINT_STORE_RV32` instructions. The `hint_stream` is populated via [phantom sub-instructions](#phantom-sub-instructions) such
as `HINT_INPUT` and `HINT_BITS`.

## Public Outputs
Expand Down Expand Up @@ -266,7 +266,7 @@ We use the same notation for `r32{c}(b) := i32([b:4]_1) + sign_extend(decompose(

| Name | Operands | Description |
| --------------- | ----------- | ----------------------------------------------------------------------------------------------------------------------------------- |
| HINTSTOREW_RV32 | `_,b,c,1,2` | `[r32{c}(b):4]_2 = next 4 bytes from hint stream`. Only valid if next 4 values in hint stream are bytes. |
| HINT_STOREW_RV32 | `_,b,c,1,2` | `[r32{c}(b):4]_2 = next 4 bytes from hint stream`. Only valid if next 4 values in hint stream are bytes. |
| REVEAL_RV32 | `a,b,c,1,3` | Pseudo-instruction for `STOREW_RV32 a,b,c,1,3` writing to the user IO address space `3`. Only valid when continuations are enabled. |

### Hashes
Expand Down Expand Up @@ -425,16 +425,17 @@ instruction format suggested by Max Gillet to enable easier compatibility with o

In the instructions below, `d,e` may be any valid address space unless otherwise specified. In particular, the immediate address space `0` is allowed for non-vectorized reads but not allowed for writes. When using immediates, we interpret `[a]_0` as the immediate value `a`. Base kernel instructions enable memory movement between address spaces.

In some instructions below, `W` is a generic parameter for the block size.

| Name | Operands | Description |
| -------------- | --------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
| LOAD\<W\> | `a,b,c,d,e` | Set `[a:W]_d = [[c]_d + b:W]_e`. Both `d, e` must be non-zero. |
| STORE\<W\> | `a,b,c,d,e` | Set `[[c]_d + b:W]_e = [a:W]_d`. Both `d, e` must be non-zero. |
| LOADW | `a,b,c,d,e` | Set `[a]_d = [[c]_d + b]_e`. Both `d, e` must be non-zero. |
| STOREW | `a,b,c,d,e` | Set `[[c]_d + b]_e = [a]_d`. Both `d, e` must be non-zero. |
| LOADW4 | `a,b,c,d,e` | Set `[a:4]_d = [[c]_d + b:4]_e`. Both `d, e` must be non-zero. |
| STOREW4 | `a,b,c,d,e` | Set `[[c]_d + b:4]_e = [a:4]_d`. Both `d, e` must be non-zero. |
| JAL | `a,b,c,d` | Jump to address and link: set `[a]_d = (pc + DEFAULT_PC_STEP)` and `pc = pc + b`. Here `d` must be non-zero. |
| BEQ\<W\> | `a,b,c,d,e` | If `[a:W]_d == [b:W]_e`, then set `pc = pc + c`. |
| BNE\<W\> | `a,b,c,d,e` | If `[a:W]_d != [b:W]_e`, then set `pc = pc + c`. |
| HINTSTORE\<W\> | `_,b,c,d,e` | Set `[[c]_d + b:W]_e = next W elements from hint stream`. Both `d, e` must be non-zero. |
| HINT_STOREW | `_,b,c,d,e` | Set `[[c]_d + b]_e = next element from hint stream`. Both `d, e` must be non-zero. |
| HINT_STOREW4 | `_,b,c,d,e` | Set `[[c]_d + b:4]_e = next 4 elements from hint stream`. Both `d, e` must be non-zero. |
| PUBLISH | `a,b,_,d,e` | Set the user public output at index `[a]_d` to equal `[b]_e`. Invalid if `[a]_d` is greater than or equal to the configured length of user public outputs. Only valid when continuations are disabled. |
| CASTF | `a,b,_,d,e` | Cast a field element represented as `u32` into four bytes in little-endian: Set `[a:4]_d` to the unique array such that `sum_{i=0}^3 [a + i]_d * 2^{8i} = [b]_e` where `[a + i]_d < 2^8` for `i = 0..2` and `[a + 3]_d < 2^6`. This opcode constrains that `[b]_e` must be at most 30-bits. Both `d, e` must be non-zero. |

Expand Down
2 changes: 1 addition & 1 deletion docs/specs/RISCV.md
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,7 @@ The transpilation will only be valid for programs where:
| RISC-V Inst | OpenVM Instruction |
| -------------- | ---------------------------------------------------------------- |
| terminate | TERMINATE `_, _, utof(imm)` |
| hintstorew | HINTSTOREW_RV32 `0, ind(rd), utof(sign_extend_16(imm)), 1, 2` |
| hintstorew | HINT_STOREW_RV32 `0, ind(rd), utof(sign_extend_16(imm)), 1, 2` |
| reveal | REVEAL_RV32 `0, ind(rd), utof(sign_extend_16(imm)), 1, 3` |
| hintinput | PHANTOM `_, _, HintInputRv32 as u16` |
| printstr | PHANTOM `ind(rd), ind(rs1), PrintStrRv32 as u16` |
Expand Down
20 changes: 10 additions & 10 deletions extensions/native/circuit/src/adapters/loadstore_native_adapter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ pub struct NativeLoadStoreInstruction<T> {
pub opcode: T,
pub is_loadw: T,
pub is_storew: T,
pub is_shintw: T,
pub is_hint_storew: T,
}

pub struct NativeLoadStoreAdapterInterface<T, const NUM_CELLS: usize>(PhantomData<T>);
Expand Down Expand Up @@ -144,7 +144,7 @@ impl<AB: InteractionBuilder, const NUM_CELLS: usize> VmAdapterAir<AB>
let is_valid = ctx.instruction.is_valid;
let is_loadw = ctx.instruction.is_loadw;
let is_storew = ctx.instruction.is_storew;
let is_shintw = ctx.instruction.is_shintw;
let is_hint_storew = ctx.instruction.is_hint_storew;

// first pointer read is always [c]_d
self.memory_bridge
Expand All @@ -162,14 +162,14 @@ impl<AB: InteractionBuilder, const NUM_CELLS: usize> VmAdapterAir<AB>
// read data, disabled if SHINTW
// data pointer = [c]_d + b, degree 2
builder
.when(is_valid.clone() - is_shintw.clone())
.when(is_valid.clone() - is_hint_storew.clone())
.assert_eq(
cols.data_read_as,
utils::select::<AB::Expr>(is_loadw.clone(), cols.e, cols.d),
);
// TODO[yi]: Do we need to check for overflow?
builder.assert_eq(
(is_valid.clone() - is_shintw.clone()) * cols.data_read_pointer,
(is_valid.clone() - is_hint_storew.clone()) * cols.data_read_pointer,
is_storew.clone() * cols.a + is_loadw.clone() * (ctx.reads.0.clone() + cols.b),
);
self.memory_bridge
Expand All @@ -179,8 +179,8 @@ impl<AB: InteractionBuilder, const NUM_CELLS: usize> VmAdapterAir<AB>
timestamp + timestamp_delta.clone(),
&cols.data_read_aux_cols,
)
.eval(builder, is_valid.clone() - is_shintw.clone());
timestamp_delta += is_valid.clone() - is_shintw.clone();
.eval(builder, is_valid.clone() - is_hint_storew.clone());
timestamp_delta += is_valid.clone() - is_hint_storew.clone();

// data write
builder.when(is_valid.clone()).assert_eq(
Expand All @@ -191,7 +191,7 @@ impl<AB: InteractionBuilder, const NUM_CELLS: usize> VmAdapterAir<AB>
builder.assert_eq(
is_valid.clone() * cols.data_write_pointer,
is_loadw.clone() * cols.a
+ (is_storew.clone() + is_shintw.clone()) * (ctx.reads.0.clone() + cols.b),
+ (is_storew.clone() + is_hint_storew.clone()) * (ctx.reads.0.clone() + cols.b),
);
self.memory_bridge
.write(
Expand Down Expand Up @@ -254,18 +254,18 @@ impl<F: PrimeField32, const NUM_CELLS: usize> VmAdapterChip<F>
let (data_read_as, data_write_as) = {
match local_opcode {
LOADW | LOADW4 => (e, d),
STOREW | STOREW4 | SHINTW | SHINTW4 => (d, e),
STOREW | STOREW4 | HINT_STOREW | HINT_STOREW4 => (d, e),
}
};
let (data_read_ptr, data_write_ptr) = {
match local_opcode {
LOADW | LOADW4 => (read_cell.1 + b, a),
STOREW | STOREW4 | SHINTW | SHINTW4 => (a, read_cell.1 + b),
STOREW | STOREW4 | HINT_STOREW | HINT_STOREW4 => (a, read_cell.1 + b),
}
};

let data_read = match local_opcode {
SHINTW | SHINTW4 => None,
HINT_STOREW | HINT_STOREW4 => None,
LOADW | LOADW4 | STOREW | STOREW4 => {
Some(memory.read::<NUM_CELLS>(data_read_as, data_read_ptr))
}
Expand Down
4 changes: 2 additions & 2 deletions extensions/native/circuit/src/extension.rs
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ impl<F: PrimeField32> VmExtension<F> for Native {
[
NativeLoadStoreOpcode::LOADW,
NativeLoadStoreOpcode::STOREW,
NativeLoadStoreOpcode::SHINTW,
NativeLoadStoreOpcode::HINT_STOREW,
]
.iter()
.map(|&opcode| VmOpcode::with_default_offset(opcode)),
Expand All @@ -144,7 +144,7 @@ impl<F: PrimeField32> VmExtension<F> for Native {
[
NativeLoadStoreOpcode::LOADW4,
NativeLoadStoreOpcode::STOREW4,
NativeLoadStoreOpcode::SHINTW4,
NativeLoadStoreOpcode::HINT_STOREW4,
]
.iter()
.map(|&opcode| VmOpcode::with_default_offset(opcode)),
Expand Down
19 changes: 10 additions & 9 deletions extensions/native/circuit/src/loadstore/core.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ use super::super::adapters::loadstore_native_adapter::NativeLoadStoreInstruction
pub struct NativeLoadStoreCoreCols<T, const NUM_CELLS: usize> {
pub is_loadw: T,
pub is_storew: T,
pub is_shintw: T,
pub is_hint_storew: T,

pub pointer_read: T,
pub data_read: [T; NUM_CELLS],
Expand Down Expand Up @@ -76,7 +76,7 @@ where
_from_pc: AB::Var,
) -> AdapterAirContext<AB::Expr, I> {
let cols: &NativeLoadStoreCoreCols<_, NUM_CELLS> = (*local_core).borrow();
let flags = [cols.is_loadw, cols.is_storew, cols.is_shintw];
let flags = [cols.is_loadw, cols.is_storew, cols.is_hint_storew];
let is_valid = flags.iter().fold(AB::Expr::ZERO, |acc, &flag| {
builder.assert_bool(flag);
acc + flag.into()
Expand All @@ -89,13 +89,13 @@ where
[
NativeLoadStoreOpcode::LOADW,
NativeLoadStoreOpcode::STOREW,
NativeLoadStoreOpcode::SHINTW,
NativeLoadStoreOpcode::HINT_STOREW,
]
} else if NUM_CELLS == 4 {
[
NativeLoadStoreOpcode::LOADW4,
NativeLoadStoreOpcode::STOREW4,
NativeLoadStoreOpcode::SHINTW4,
NativeLoadStoreOpcode::HINT_STOREW4,
]
} else {
panic!("Unsupported number of cells: {}", NUM_CELLS);
Expand All @@ -114,7 +114,7 @@ where
opcode: expected_opcode,
is_loadw: cols.is_loadw.into(),
is_storew: cols.is_storew.into(),
is_shintw: cols.is_shintw.into(),
is_hint_storew: cols.is_hint_storew.into(),
}
.into(),
}
Expand Down Expand Up @@ -159,8 +159,8 @@ where
NativeLoadStoreOpcode::from_usize(opcode.local_opcode_idx(self.air.offset));
let (pointer_read, data_read) = reads.into();

let data_write = if (NUM_CELLS == 1 && local_opcode == NativeLoadStoreOpcode::SHINTW)
|| (NUM_CELLS == 4 && local_opcode == NativeLoadStoreOpcode::SHINTW4)
let data_write = if (NUM_CELLS == 1 && local_opcode == NativeLoadStoreOpcode::HINT_STOREW)
|| (NUM_CELLS == 4 && local_opcode == NativeLoadStoreOpcode::HINT_STOREW4)
{
let mut streams = self.streams.get().unwrap().lock().unwrap();
if streams.hint_stream.len() < NUM_CELLS {
Expand Down Expand Up @@ -193,11 +193,12 @@ where
if NUM_CELLS == 1 {
cols.is_loadw = F::from_bool(record.opcode == NativeLoadStoreOpcode::LOADW);
cols.is_storew = F::from_bool(record.opcode == NativeLoadStoreOpcode::STOREW);
cols.is_shintw = F::from_bool(record.opcode == NativeLoadStoreOpcode::SHINTW);
cols.is_hint_storew = F::from_bool(record.opcode == NativeLoadStoreOpcode::HINT_STOREW);
} else if NUM_CELLS == 4 {
cols.is_loadw = F::from_bool(record.opcode == NativeLoadStoreOpcode::LOADW4);
cols.is_storew = F::from_bool(record.opcode == NativeLoadStoreOpcode::STOREW4);
cols.is_shintw = F::from_bool(record.opcode == NativeLoadStoreOpcode::SHINTW4);
cols.is_hint_storew =
F::from_bool(record.opcode == NativeLoadStoreOpcode::HINT_STOREW4);
} else {
panic!("Unsupported number of cells: {}", NUM_CELLS);
}
Expand Down
4 changes: 2 additions & 2 deletions extensions/native/circuit/src/loadstore/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ fn gen_test_data(rng: &mut StdRng, is_immediate: bool, opcode: NativeLoadStoreOp
cd_val: F::from_canonical_u32(222),
data_val: F::from_canonical_u32(444),
is_load,
is_hint: matches!(opcode, NativeLoadStoreOpcode::SHINTW),
is_hint: matches!(opcode, NativeLoadStoreOpcode::HINT_STOREW),
}
}

Expand Down Expand Up @@ -171,7 +171,7 @@ fn rand_native_loadstore_test() {
let (mut rng, mut tester, mut chip) = setup();
for _ in 0..20 {
set_and_execute(&mut tester, &mut chip, &mut rng, false, STOREW);
set_and_execute(&mut tester, &mut chip, &mut rng, false, SHINTW);
set_and_execute(&mut tester, &mut chip, &mut rng, false, HINT_STOREW);
set_and_execute(&mut tester, &mut chip, &mut rng, false, LOADW);
}
let tester = tester.build().load(chip).finalize();
Expand Down
4 changes: 2 additions & 2 deletions extensions/native/compiler/src/conversion/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -511,15 +511,15 @@ fn convert_instruction<F: PrimeField32, EF: ExtensionField<F>>(
Instruction::phantom(PhantomDiscriminant(NativePhantom::HintBits as u16), i32_f(src), F::from_canonical_u32(len), AS::Native as u16)
],
AsmInstruction::StoreHintWordI(val, offset) => vec![inst(
options.opcode_with_offset(NativeLoadStoreOpcode::SHINTW),
options.opcode_with_offset(NativeLoadStoreOpcode::HINT_STOREW),
F::ZERO,
offset,
i32_f(val),
AS::Native,
AS::Native,
)],
AsmInstruction::StoreHintExtI(val, offset) => vec![inst(
options.opcode_with_offset(NativeLoadStoreOpcode::SHINTW4),
options.opcode_with_offset(NativeLoadStoreOpcode::HINT_STOREW4),
F::ZERO,
offset,
i32_f(val),
Expand Down
5 changes: 3 additions & 2 deletions extensions/native/compiler/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -42,14 +42,15 @@ pub mod prelude {
)]
#[opcode_offset = 0x100]
#[repr(usize)]
#[allow(non_camel_case_types)]
pub enum NativeLoadStoreOpcode {
LOADW,
STOREW,
/// Instruction to write the next hint word into memory.
SHINTW,
HINT_STOREW,
LOADW4,
STOREW4,
SHINTW4,
HINT_STOREW4,
}

#[derive(Copy, Clone, Debug, UsizeOpcode)]
Expand Down

0 comments on commit 68a2102

Please sign in to comment.