Skip to content

Commit 00a2a74

Browse files
committed
feat: Add Rv32HintLoadByKey (#1606)
- Add `kv_store` into `Streams`. More details at `docs/specs/ISA.md`. - Add a new phantom instruction `Rv32HintLoadByKey` which can hint data based on a key at runtime. More details at `docs/specs/ISA.md`. - SDK support will be added in the future PRs. close INT-3893
1 parent 5595c8f commit 00a2a74

File tree

16 files changed

+225
-18
lines changed

16 files changed

+225
-18
lines changed

Cargo.lock

Lines changed: 2 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

crates/toolchain/openvm/src/io/mod.rs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,16 @@ fn hint_store_word(ptr: *mut u32) {
5656
}
5757
}
5858

59+
/// Load hints by key and append into the input stream.
60+
#[allow(unused_variables)]
61+
#[inline(always)]
62+
pub fn hint_load_by_key(key: &[u8]) {
63+
#[cfg(target_os = "zkvm")]
64+
openvm_rv32im_guest::hint_load_by_key(key.as_ptr(), key.len() as u32);
65+
#[cfg(not(target_os = "zkvm"))]
66+
panic!("hint_load_by_key cannot run on non-zkVM platforms");
67+
}
68+
5969
/// Read the next `len` bytes from the hint stream into a vector.
6070
pub(crate) fn read_vec_by_len(len: usize) -> Vec<u8> {
6171
let num_words = len.div_ceil(4);

crates/vm/src/arch/vm.rs

Lines changed: 29 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,10 @@
1-
use std::{borrow::Borrow, collections::VecDeque, marker::PhantomData, mem, sync::Arc};
1+
use std::{
2+
borrow::Borrow,
3+
collections::{HashMap, VecDeque},
4+
marker::PhantomData,
5+
mem,
6+
sync::Arc,
7+
};
28

39
use openvm_circuit::system::program::trace::compute_exe_commit;
410
use openvm_instructions::exe::VmExe;
@@ -49,11 +55,25 @@ pub enum GenerationError {
4955
/// VM memory state for continuations.
5056
pub type VmMemoryState<F> = MemoryImage<F>;
5157

52-
#[derive(Clone, Default, Debug)]
58+
/// A trait for key-value store for `Streams`.
59+
pub trait KvStore: Send + Sync {
60+
fn get(&self, key: &[u8]) -> Option<&[u8]>;
61+
}
62+
63+
impl KvStore for HashMap<Vec<u8>, Vec<u8>> {
64+
fn get(&self, key: &[u8]) -> Option<&[u8]> {
65+
self.get(key).map(|v| v.as_slice())
66+
}
67+
}
68+
69+
#[derive(Clone)]
5370
pub struct Streams<F> {
5471
pub input_stream: VecDeque<Vec<F>>,
5572
pub hint_stream: VecDeque<F>,
5673
pub hint_space: Vec<Vec<F>>,
74+
/// The key-value store for hints. Both key and value are byte arrays. Executors which
75+
/// read `kv_store` need to encode the key and decode the value.
76+
pub kv_store: Arc<dyn KvStore>,
5777
}
5878

5979
impl<F> Streams<F> {
@@ -62,10 +82,17 @@ impl<F> Streams<F> {
6282
input_stream: input_stream.into(),
6383
hint_stream: VecDeque::default(),
6484
hint_space: Vec::default(),
85+
kv_store: Arc::new(HashMap::new()),
6586
}
6687
}
6788
}
6889

90+
impl<F> Default for Streams<F> {
91+
fn default() -> Self {
92+
Self::new(VecDeque::default())
93+
}
94+
}
95+
6996
impl<F> From<VecDeque<Vec<F>>> for Streams<F> {
7097
fn from(value: VecDeque<Vec<F>>) -> Self {
7198
Streams::new(value)

docs/specs/ISA.md

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -171,6 +171,9 @@ 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`
175+
at runtime. `kv_store` is designed for general purposes so both key and value are byte arrays. Encoding of key/value
176+
are decided by each executor. Users need to use the corresponding encoding when adding data to `kv_store`.
174177

175178
These data structures are **not** part of the guest state, and their state depends on host behavior that cannot be determined by the guest.
176179

@@ -204,7 +207,7 @@ which must satisfy the following conditions:
204207
- The execution has full read/write access to the data memory, except address space `0` must be read-only.
205208
- User public outputs can be set at any index in `[0, num_public_values)`. If continuations are disabled, a public
206209
value cannot be overwritten with a different value once it is set.
207-
- Input stream can only be popped from the front as a queue. Appends are not allowed.
210+
- Input stream can only be popped from the front as a queue.
208211
- Full read/write access to the hint stream.
209212
- Hint spaces can be read from at any index. Hint spaces may be mutated only by append.
210213
- The program counter is set to a new `to_pc` at the end of the instruction execution.
@@ -426,12 +429,12 @@ with user input-output.
426429

427430
The RV32IM extension defines the following phantom sub-instructions.
428431

429-
| Name | Discriminant | Operands | Description |
430-
| -------------- | ------------ | -------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
431-
| Rv32HintInput | 0x20 | `_` | Pops a vector `hint` of field elements from the input stream and resets the hint stream to equal the vector `[(hint.len() as u32).to_le_bytes()), hint].concat()`. |
432-
| Rv32PrintStr | 0x21 | `a,b,_` | Peeks at `[r32{0}(a)..r32{0}(a) + r32{0}(b)]_2`, tries to convert to byte array and then UTF-8 string and prints to host stdout. Prints error message if conversion fails. Does not change any VM state. |
433-
| Rv32HintRandom | 0x22 | `a,_,_` | Resets the hint stream to `4 * r32{0}(a)` random bytes. The source of randomness is the host operating system (`rand::rngs::OsRng`). Its result is not constrained in any way. |
434-
432+
| Name | Discriminant | Operands | Description |
433+
|-------------------| ------------ | -------- |--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
434+
| Rv32HintInput | 0x20 | `_` | Pops a vector `hint` of field elements from the input stream and resets the hint stream to equal the vector `[(hint.len() as u32).to_le_bytes()), hint].concat()`. |
435+
| Rv32PrintStr | 0x21 | `a,b,_` | Peeks at `[r32{0}(a)..r32{0}(a) + r32{0}(b)]_2`, tries to convert to byte array and then UTF-8 string and prints to host stdout. Prints error message if conversion fails. Does not change any VM state. |
436+
| Rv32HintRandom | 0x22 | `a,_,_` | Resets the hint stream to `4 * r32{0}(a)` random bytes. The source of randomness is the host operating system (`rand::rngs::OsRng`). Its result is not constrained in any way. |
437+
| Rv32HintLoadByKey | 0x23 | `a,b,_` | Look up the value by key `[r32{0}{a}:r32{0}{b}]_2` and prepend the value into `input_stream`. Users should use `openvm-rv32im-guest::hint_load_by_key_encode` to encode the value when constructing inputs. |
435438
### Native Extension
436439

437440
The native extension operates over native field elements and has instructions tailored for STARK proof recursion. It

docs/specs/isa-table.md

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -75,11 +75,12 @@ In the tables below, we provide the mapping between the `LocalOpcode` and `Phant
7575

7676
#### Phantom Sub-Instructions
7777

78-
| VM Extension | `PhantomDiscriminant` | ISA Phantom Sub-Instruction |
79-
| ------------- | ---------- | ------------- |
80-
| RV32IM | `Rv32Phantom::HintInput` | Rv32HintInput |
81-
| RV32IM | `Rv32Phantom::PrintStr` | Rv32PrintStr |
82-
| RV32IM | `Rv32Phantom::HintRandom` | Rv32HintRandom |
78+
| VM Extension | `PhantomDiscriminant` | ISA Phantom Sub-Instruction |
79+
| ------------- |-------------------------------| ------------- |
80+
| RV32IM | `Rv32Phantom::HintInput` | Rv32HintInput |
81+
| RV32IM | `Rv32Phantom::PrintStr` | Rv32PrintStr |
82+
| RV32IM | `Rv32Phantom::HintRandom` | Rv32HintRandom |
83+
| RV32IM | `Rv32Phantom::HintLoadByKey` | Rv32HintLoadByKey |
8384

8485
## Native Extension
8586

extensions/native/circuit/src/loadstore/core.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,6 @@ where
113113
}
114114
}
115115

116-
#[derive(Debug)]
117116
pub struct NativeLoadStoreCoreChip<F: Field, const NUM_CELLS: usize> {
118117
pub air: NativeLoadStoreCoreAir<NUM_CELLS>,
119118
pub streams: OnceLock<Arc<Mutex<Streams<F>>>>,
@@ -127,7 +126,10 @@ impl<F: Field, const NUM_CELLS: usize> NativeLoadStoreCoreChip<F, NUM_CELLS> {
127126
}
128127
}
129128
pub fn set_streams(&mut self, streams: Arc<Mutex<Streams<F>>>) {
130-
self.streams.set(streams).unwrap();
129+
self.streams
130+
.set(streams)
131+
.map_err(|_| "streams have already been set.")
132+
.unwrap();
131133
}
132134
}
133135

extensions/rv32im/circuit/src/extension.rs

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -352,6 +352,10 @@ impl<F: PrimeField32> VmExtension<F> for Rv32I {
352352
phantom::Rv32PrintStrSubEx,
353353
PhantomDiscriminant(Rv32Phantom::PrintStr as u16),
354354
)?;
355+
builder.add_phantom_sub_executor(
356+
phantom::Rv32HintLoadByKeySubEx,
357+
PhantomDiscriminant(Rv32Phantom::HintLoadByKey as u16),
358+
)?;
355359

356360
Ok(inventory)
357361
}
@@ -504,6 +508,7 @@ mod phantom {
504508
}
505509
}
506510
pub struct Rv32PrintStrSubEx;
511+
pub struct Rv32HintLoadByKeySubEx;
507512

508513
impl<F: Field> PhantomSubExecutor<F> for Rv32HintInputSubEx {
509514
fn phantom_execute(
@@ -579,4 +584,59 @@ mod phantom {
579584
Ok(())
580585
}
581586
}
587+
588+
impl<F: PrimeField32> PhantomSubExecutor<F> for Rv32HintLoadByKeySubEx {
589+
fn phantom_execute(
590+
&mut self,
591+
memory: &MemoryController<F>,
592+
streams: &mut Streams<F>,
593+
_: PhantomDiscriminant,
594+
a: F,
595+
b: F,
596+
_: u16,
597+
) -> eyre::Result<()> {
598+
let ptr = unsafe_read_rv32_register(memory, a);
599+
let len = unsafe_read_rv32_register(memory, b);
600+
let key: Vec<u8> = (0..len)
601+
.map(|i| {
602+
memory
603+
.unsafe_read_cell(F::TWO, F::from_canonical_u32(ptr + i))
604+
.as_canonical_u32() as u8
605+
})
606+
.collect();
607+
if let Some(val) = streams.kv_store.get(&key) {
608+
let to_push = hint_load_by_key_decode::<F>(val);
609+
for input in to_push.into_iter().rev() {
610+
streams.input_stream.push_front(input);
611+
}
612+
} else {
613+
bail!("Rv32HintLoadByKey: key not found");
614+
}
615+
Ok(())
616+
}
617+
}
618+
619+
pub fn hint_load_by_key_decode<F: PrimeField32>(value: &[u8]) -> Vec<Vec<F>> {
620+
let mut offset = 0;
621+
let len = extract_u32(value, offset) as usize;
622+
offset += 4;
623+
let mut ret = Vec::with_capacity(len);
624+
for _ in 0..len {
625+
let v_len = extract_u32(value, offset) as usize;
626+
offset += 4;
627+
let v = (0..v_len)
628+
.map(|_| {
629+
let ret = F::from_canonical_u32(extract_u32(value, offset));
630+
offset += 4;
631+
ret
632+
})
633+
.collect();
634+
ret.push(v);
635+
}
636+
ret
637+
}
638+
639+
fn extract_u32(value: &[u8], offset: usize) -> u32 {
640+
u32::from_le_bytes(value[offset..offset + 4].try_into().unwrap())
641+
}
582642
}

extensions/rv32im/circuit/src/hintstore/mod.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -313,7 +313,10 @@ impl<F: PrimeField32> Rv32HintStoreChip<F> {
313313
}
314314
}
315315
pub fn set_streams(&mut self, streams: Arc<Mutex<Streams<F>>>) {
316-
self.streams.set(streams).unwrap();
316+
self.streams
317+
.set(streams)
318+
.map_err(|_| "streams have already been set.")
319+
.unwrap();
317320
}
318321
}
319322

extensions/rv32im/guest/Cargo.toml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,5 +11,8 @@ repository.workspace = true
1111
openvm-custom-insn = { workspace = true }
1212
strum_macros = { workspace = true }
1313

14+
[target.'cfg(not(target_os = "zkvm"))'.dependencies]
15+
p3-field = { workspace = true }
16+
1417
[features]
1518
default = []

extensions/rv32im/guest/src/io.rs

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,18 @@ pub fn hint_random(len: usize) {
5555
);
5656
}
5757

58+
/// Hint the VM to load values with key = [ptr: len] into input streams.
59+
#[inline(always)]
60+
pub fn hint_load_by_key(ptr: *const u8, len: u32) {
61+
openvm_custom_insn::custom_insn_i!(
62+
opcode = SYSTEM_OPCODE,
63+
funct3 = PHANTOM_FUNCT3,
64+
rd = In ptr,
65+
rs1 = In len,
66+
imm = Const PhantomImm::HintLoadByKey as u16,
67+
);
68+
}
69+
5870
/// Store rs1 to [[rd] + imm]_3.
5971
#[macro_export]
6072
macro_rules! reveal {

extensions/rv32im/guest/src/lib.rs

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
11
#![no_std]
2+
extern crate alloc;
23

34
/// Library functions for user input/output.
45
#[cfg(target_os = "zkvm")]
56
mod io;
7+
68
#[cfg(target_os = "zkvm")]
79
pub use io::*;
810
use strum_macros::FromRepr;
@@ -28,4 +30,19 @@ pub enum PhantomImm {
2830
HintInput = 0,
2931
PrintStr,
3032
HintRandom,
33+
HintLoadByKey,
34+
}
35+
36+
/// Encode a 2d-array of field elements into bytes for `hint_load_by_key`
37+
#[cfg(not(target_os = "zkvm"))]
38+
pub fn hint_load_by_key_encode<F: p3_field::PrimeField32>(
39+
value: &[alloc::vec::Vec<F>],
40+
) -> alloc::vec::Vec<u8> {
41+
let len = value.len();
42+
let mut ret = (len as u32).to_le_bytes().to_vec();
43+
for v in value {
44+
ret.extend((v.len() as u32).to_le_bytes());
45+
ret.extend(v.iter().flat_map(|x| x.as_canonical_u32().to_le_bytes()));
46+
}
47+
ret
3148
}

extensions/rv32im/tests/Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ openvm-stark-sdk.workspace = true
1313
openvm-circuit = { workspace = true, features = ["test-utils"] }
1414
openvm-transpiler.workspace = true
1515
openvm-rv32im-circuit.workspace = true
16+
openvm-rv32im-guest.workspace = true
1617
openvm-rv32im-transpiler.workspace = true
1718
openvm = { workspace = true }
1819
openvm-toolchain-tests = { path = "../../../crates/toolchain/tests" }
Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
#![cfg_attr(not(feature = "std"), no_main)]
2+
#![cfg_attr(not(feature = "std"), no_std)]
3+
use openvm::io::{hint_load_by_key, read_vec};
4+
5+
openvm::entry!(main);
6+
7+
pub fn main() {
8+
const KEY: &str = "key";
9+
hint_load_by_key(KEY.as_bytes());
10+
11+
let vec = read_vec();
12+
// assert_eq!(vec.len(), 4);
13+
if vec.len() != 4 {
14+
openvm::process::panic();
15+
}
16+
#[allow(clippy::needless_range_loop)]
17+
for i in 0..4 {
18+
if vec[i] != i as u8 {
19+
openvm::process::panic();
20+
}
21+
}
22+
let vec = read_vec();
23+
if vec.len() != 3 {
24+
openvm::process::panic();
25+
}
26+
#[allow(clippy::needless_range_loop)]
27+
for i in 0..3 {
28+
if vec[i] != i as u8 {
29+
openvm::process::panic();
30+
}
31+
}
32+
}

0 commit comments

Comments
 (0)