From 68a210267c1c5a370971d876cde230648867eb67 Mon Sep 17 00:00:00 2001 From: Yi Sun Date: Fri, 10 Jan 2025 04:36:58 -0500 Subject: [PATCH] chore: rename SHINTW -> HINT_STOREW --- crates/vm/tests/integration_test.rs | 4 ++-- docs/specs/ISA.md | 15 +++++++------- docs/specs/RISCV.md | 2 +- .../src/adapters/loadstore_native_adapter.rs | 20 +++++++++---------- extensions/native/circuit/src/extension.rs | 4 ++-- .../native/circuit/src/loadstore/core.rs | 19 +++++++++--------- .../native/circuit/src/loadstore/tests.rs | 4 ++-- .../native/compiler/src/conversion/mod.rs | 4 ++-- extensions/native/compiler/src/lib.rs | 5 +++-- 9 files changed, 40 insertions(+), 37 deletions(-) diff --git a/crates/vm/tests/integration_test.rs b/crates/vm/tests/integration_test.rs index 7e5e018a1..04f53e93b 100644 --- a/crates/vm/tests/integration_test.rs +++ b/crates/vm/tests/integration_test.rs @@ -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), @@ -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)), diff --git a/docs/specs/ISA.md b/docs/specs/ISA.md index c73ba7d31..6bb73419e 100644 --- a/docs/specs/ISA.md +++ b/docs/specs/ISA.md @@ -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 @@ -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 @@ -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\ | `a,b,c,d,e` | Set `[a:W]_d = [[c]_d + b:W]_e`. Both `d, e` must be non-zero. | -| STORE\ | `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\ | `a,b,c,d,e` | If `[a:W]_d == [b:W]_e`, then set `pc = pc + c`. | | BNE\ | `a,b,c,d,e` | If `[a:W]_d != [b:W]_e`, then set `pc = pc + c`. | -| HINTSTORE\ | `_,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. | diff --git a/docs/specs/RISCV.md b/docs/specs/RISCV.md index d0273436d..0d6988267 100644 --- a/docs/specs/RISCV.md +++ b/docs/specs/RISCV.md @@ -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` | diff --git a/extensions/native/circuit/src/adapters/loadstore_native_adapter.rs b/extensions/native/circuit/src/adapters/loadstore_native_adapter.rs index dbf0a78a9..fc6b2940c 100644 --- a/extensions/native/circuit/src/adapters/loadstore_native_adapter.rs +++ b/extensions/native/circuit/src/adapters/loadstore_native_adapter.rs @@ -33,7 +33,7 @@ pub struct NativeLoadStoreInstruction { pub opcode: T, pub is_loadw: T, pub is_storew: T, - pub is_shintw: T, + pub is_hint_storew: T, } pub struct NativeLoadStoreAdapterInterface(PhantomData); @@ -144,7 +144,7 @@ impl VmAdapterAir 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 @@ -162,14 +162,14 @@ impl VmAdapterAir // 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::(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 @@ -179,8 +179,8 @@ impl VmAdapterAir 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( @@ -191,7 +191,7 @@ impl VmAdapterAir 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( @@ -254,18 +254,18 @@ impl VmAdapterChip 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::(data_read_as, data_read_ptr)) } diff --git a/extensions/native/circuit/src/extension.rs b/extensions/native/circuit/src/extension.rs index 1e54d1469..147199eec 100644 --- a/extensions/native/circuit/src/extension.rs +++ b/extensions/native/circuit/src/extension.rs @@ -119,7 +119,7 @@ impl VmExtension for Native { [ NativeLoadStoreOpcode::LOADW, NativeLoadStoreOpcode::STOREW, - NativeLoadStoreOpcode::SHINTW, + NativeLoadStoreOpcode::HINT_STOREW, ] .iter() .map(|&opcode| VmOpcode::with_default_offset(opcode)), @@ -144,7 +144,7 @@ impl VmExtension for Native { [ NativeLoadStoreOpcode::LOADW4, NativeLoadStoreOpcode::STOREW4, - NativeLoadStoreOpcode::SHINTW4, + NativeLoadStoreOpcode::HINT_STOREW4, ] .iter() .map(|&opcode| VmOpcode::with_default_offset(opcode)), diff --git a/extensions/native/circuit/src/loadstore/core.rs b/extensions/native/circuit/src/loadstore/core.rs index 677ffc090..96fa2d375 100644 --- a/extensions/native/circuit/src/loadstore/core.rs +++ b/extensions/native/circuit/src/loadstore/core.rs @@ -27,7 +27,7 @@ use super::super::adapters::loadstore_native_adapter::NativeLoadStoreInstruction pub struct NativeLoadStoreCoreCols { 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], @@ -76,7 +76,7 @@ where _from_pc: AB::Var, ) -> AdapterAirContext { 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() @@ -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); @@ -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(), } @@ -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 { @@ -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); } diff --git a/extensions/native/circuit/src/loadstore/tests.rs b/extensions/native/circuit/src/loadstore/tests.rs index 6c76247b1..47c798fd2 100644 --- a/extensions/native/circuit/src/loadstore/tests.rs +++ b/extensions/native/circuit/src/loadstore/tests.rs @@ -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), } } @@ -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(); diff --git a/extensions/native/compiler/src/conversion/mod.rs b/extensions/native/compiler/src/conversion/mod.rs index 2f64eadd6..a93566d94 100644 --- a/extensions/native/compiler/src/conversion/mod.rs +++ b/extensions/native/compiler/src/conversion/mod.rs @@ -511,7 +511,7 @@ fn convert_instruction>( 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), @@ -519,7 +519,7 @@ fn convert_instruction>( 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), diff --git a/extensions/native/compiler/src/lib.rs b/extensions/native/compiler/src/lib.rs index c4da7e5f4..f8d2f63af 100644 --- a/extensions/native/compiler/src/lib.rs +++ b/extensions/native/compiler/src/lib.rs @@ -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)]