Skip to content

Commit fd2cc4d

Browse files
nyunyunyunyunyunyunyunyu
committed
Add macro define_verify_openvm_stark for stark verification
1 parent c1829fc commit fd2cc4d

File tree

12 files changed

+141
-43
lines changed

12 files changed

+141
-43
lines changed

‎Cargo.lock

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

‎Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,7 @@ openvm-native-circuit = { path = "extensions/native/circuit", default-features =
140140
openvm-native-compiler = { path = "extensions/native/compiler", default-features = false }
141141
openvm-native-compiler-derive = { path = "extensions/native/compiler/derive", default-features = false }
142142
openvm-native-recursion = { path = "extensions/native/recursion", default-features = false }
143+
openvm-native-transpiler = { path = "extensions/native/transpiler", default-features = false }
143144
openvm-keccak256-circuit = { path = "extensions/keccak256/circuit", default-features = false }
144145
openvm-keccak256-transpiler = { path = "extensions/keccak256/transpiler", default-features = false }
145146
openvm-keccak256-guest = { path = "extensions/keccak256/guest", default-features = false }

‎crates/sdk/Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ openvm-pairing-transpiler = { workspace = true }
2525
openvm-native-circuit = { workspace = true }
2626
openvm-native-compiler = { workspace = true }
2727
openvm-native-recursion = { workspace = true, features = ["static-verifier"] }
28+
openvm-native-transpiler = { workspace = true }
2829
openvm-rv32im-circuit = { workspace = true }
2930
openvm-rv32im-transpiler = { workspace = true }
3031
openvm-transpiler = { workspace = true }

‎crates/sdk/src/config/global.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ use openvm_native_circuit::{
2424
CastFExtension, CastFExtensionExecutor, CastFExtensionPeriphery, Native, NativeExecutor,
2525
NativePeriphery,
2626
};
27+
use openvm_native_transpiler::LongFormTranspilerExtension;
2728
use openvm_pairing_circuit::{
2829
PairingExtension, PairingExtensionExecutor, PairingExtensionPeriphery,
2930
};
@@ -138,6 +139,9 @@ impl SdkVmConfig {
138139
if self.sha256.is_some() {
139140
transpiler = transpiler.with_extension(Sha256TranspilerExtension);
140141
}
142+
if self.native.is_some() {
143+
transpiler = transpiler.with_extension(LongFormTranspilerExtension);
144+
}
141145
if self.rv32m.is_some() {
142146
transpiler = transpiler.with_extension(Rv32MTranspilerExtension);
143147
}

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -126,6 +126,16 @@ pub fn reveal_u32(x: u32, index: usize) {
126126
println!("reveal {} at byte location {}", x, index * 4);
127127
}
128128

129+
/// Store u32 `x` to the native address `native_addr` as 4 field element in byte.
130+
#[allow(unused_variables)]
131+
#[inline(always)]
132+
pub fn store_u32_to_native(native_addr: u32, x: u32) {
133+
#[cfg(target_os = "zkvm")]
134+
openvm_rv32im_guest::store_to_native!(native_addr, x);
135+
#[cfg(not(target_os = "zkvm"))]
136+
panic!("store_to_native_u32 cannot run on non-zkVM platforms");
137+
}
138+
129139
/// A no-alloc writer to print to stdout on host machine for debugging purposes.
130140
pub struct Writer;
131141

‎crates/toolchain/openvm/src/lib.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ pub mod utils;
2929

3030
#[cfg(not(target_os = "zkvm"))]
3131
pub mod host;
32+
#[cfg(target_os = "zkvm")]
33+
pub mod verify_stark;
3234

3335
#[cfg(target_os = "zkvm")]
3436
core::arch::global_asm!(include_str!("memset.s"));

‎crates/toolchain/openvm/src/verify_stark.rs

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
/// Define a function with the given name that verifies an OpenVM Stark proof.
2+
#[macro_export]
3+
macro_rules! define_verify_openvm_stark {
4+
($fn_name: ident, $asm_folder: literal, $asm_filename: literal) => {
5+
pub fn $fn_name(app_exe_commit: &[u32; 8], app_vm_commit: &[u32; 8], user_pvs: &[u32]) {
6+
// The memory location for the start of the heap.
7+
const HEAP_START_ADDRESS: u32 = 1 << 24;
8+
const FIELDS_PER_U32: u32 = 4;
9+
const FILENAME: &str = $asm_filename;
10+
// Construct the hint key
11+
let hint_key: alloc::vec::Vec<u8> = FILENAME
12+
.as_bytes()
13+
.iter()
14+
.cloned()
15+
.chain(app_exe_commit.iter().flat_map(|x| x.to_le_bytes()))
16+
.chain(app_vm_commit.iter().flat_map(|x| x.to_le_bytes()))
17+
.chain(user_pvs.iter().flat_map(|x| x.to_le_bytes()))
18+
.collect();
19+
openvm::io::hint_load_by_key(&hint_key);
20+
// Store the expected public values into the beginning of the native heap.
21+
let mut native_addr = HEAP_START_ADDRESS;
22+
for &x in app_exe_commit {
23+
openvm::io::store_u32_to_native(native_addr, x);
24+
native_addr += FIELDS_PER_U32;
25+
}
26+
for &x in app_vm_commit {
27+
openvm::io::store_u32_to_native(native_addr, x);
28+
native_addr += FIELDS_PER_U32;
29+
}
30+
for &x in user_pvs {
31+
openvm::io::store_u32_to_native(native_addr, x);
32+
native_addr += FIELDS_PER_U32;
33+
}
34+
// Assumption: the asm file should be generated by SDK. The code block should:
35+
// 1. Increase the heap pointer in order to avoid overwriting expected public values.
36+
// 2. Hint a stark proof from the input stream
37+
// 3. Verify the proof
38+
// 4. Compare the public values with the expected ones. Panic if not equal.
39+
unsafe { core::arch::asm!(include_str!(concat!($asm_folder, "/", $asm_filename)),) }
40+
}
41+
};
42+
}

‎docs/specs/RISCV.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,10 @@ the guest must take care to validate all data and account for behavior in cases
7272
| printstr | I | 0001011 | 011 | 0x1 | Tries to convert `[rd..rd + rs1]_2` to UTF-8 string and print to host stdout. Will print error message if conversion fails. |
7373
| hintrandom | I | 0001011 | 011 | 0x2 | Resets the hint stream to `4 * rd` random bytes from `rand::rngs::OsRng` on the host. |
7474

75+
| RISC-V Inst | FMT | opcode[6:0] | funct3 | funct7 | RISC-V description and notes |
76+
|--------------|-----|-------------|---------|---------|---------------------------------------------------------------------------------------------------------------------------------|
77+
| nativestorew | R | 0001011 | 111 | 2 | Stores the 4-byte word `rs1` at address `rd` in native address space. The address `rd` must be aligned to a 4-byte boundary. |
78+
7579
## Keccak Extension
7680

7781
| RISC-V Inst | FMT | opcode[6:0] | funct3 | funct7 | RISC-V description and notes |

‎docs/specs/isa-table.md

Lines changed: 40 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -31,47 +31,48 @@ In the tables below, we provide the mapping between the `LocalOpcode` and `Phant
3131

3232
#### Instructions
3333

34-
| VM Extension | `LocalOpcode` | ISA Instruction |
35-
| ------------- | ---------- | ------------- |
36-
| RV32IM | `BaseAluOpcode::ADD` | ADD_RV32 |
37-
| RV32IM | `BaseAluOpcode::SUB` | SUB_RV32 |
38-
| RV32IM | `BaseAluOpcode::XOR` | XOR_RV32 |
39-
| RV32IM | `BaseAluOpcode::OR` | OR_RV32 |
40-
| RV32IM | `BaseAluOpcode::AND` | AND_RV32 |
41-
| RV32IM | `ShiftOpcode::SLL` | SLL_RV32 |
42-
| RV32IM | `ShiftOpcode::SRL` | SRL_RV32 |
43-
| RV32IM | `ShiftOpcode::SRA` | SRA_RV32 |
44-
| RV32IM | `LessThanOpcode::SLT` | SLT_RV32 |
45-
| RV32IM | `LessThanOpcode::SLTU` | SLTU_RV32 |
46-
| RV32IM | `Rv32LoadStoreOpcode::LOADB` | LOADB_RV32 |
47-
| RV32IM | `Rv32LoadStoreOpcode::LOADH` | LOADH_RV32 |
48-
| RV32IM | `Rv32LoadStoreOpcode::LOADW` | LOADW_RV32 |
49-
| RV32IM | `Rv32LoadStoreOpcode::LOADBU` | LOADBU_RV32 |
50-
| RV32IM | `Rv32LoadStoreOpcode::LOADHU` | LOADHU_RV32 |
51-
| RV32IM | `Rv32LoadStoreOpcode::STOREB` | STOREB_RV32 |
52-
| RV32IM | `Rv32LoadStoreOpcode::STOREH` | STOREH_RV32 |
53-
| RV32IM | `Rv32LoadStoreOpcode::STOREW` | STOREW_RV32 |
54-
| RV32IM | `BranchEqualOpcode::BEQ` | BEQ_RV32 |
55-
| RV32IM | `BranchEqualOpcode::BNE` | BNE_RV32 |
56-
| RV32IM | `BranchLessThanOpcode::BLT` | BLT_RV32 |
57-
| RV32IM | `BranchLessThanOpcode::BGE` | BGE_RV32 |
58-
| RV32IM | `BranchLessThanOpcode::BLTU` | BLTU_RV32 |
59-
| RV32IM | `BranchLessThanOpcode::BGEU` | BGEU_RV32 |
60-
| RV32IM | `Rv32JalLuiOpcode::JAL` | JAL_RV32 |
61-
| RV32IM | `Rv32JalrOpcode::JALR` | JALR_RV32 |
62-
| RV32IM | `Rv32JalLuiOpcode::LUI` | LUI_RV32 |
63-
| RV32IM | `Rv32AuipcOpcode::AUIPC` | AUIPC_RV32 |
64-
| RV32IM | `MulOpcode::MUL` | MUL_RV32 |
65-
| RV32IM | `MulHOpcode::MULH` | MULH_RV32 |
66-
| RV32IM | `MulHOpcode::MULHSU` | MULHSU_RV32 |
67-
| RV32IM | `MulHOpcode::MULHU` | MULHU_RV32 |
68-
| RV32IM | `DivRemOpcode::DIV` | DIV_RV32 |
69-
| RV32IM | `DivRemOpcode::DIVU` | DIVU_RV32 |
70-
| RV32IM | `DivRemOpcode::REM` | REM_RV32 |
71-
| RV32IM | `DivRemOpcode::REMU` | REMU_RV32 |
34+
| VM Extension | `LocalOpcode` | ISA Instruction |
35+
| ------------- | ---------- |------------------|
36+
| RV32IM | `BaseAluOpcode::ADD` | ADD_RV32 |
37+
| RV32IM | `BaseAluOpcode::SUB` | SUB_RV32 |
38+
| RV32IM | `BaseAluOpcode::XOR` | XOR_RV32 |
39+
| RV32IM | `BaseAluOpcode::OR` | OR_RV32 |
40+
| RV32IM | `BaseAluOpcode::AND` | AND_RV32 |
41+
| RV32IM | `ShiftOpcode::SLL` | SLL_RV32 |
42+
| RV32IM | `ShiftOpcode::SRL` | SRL_RV32 |
43+
| RV32IM | `ShiftOpcode::SRA` | SRA_RV32 |
44+
| RV32IM | `LessThanOpcode::SLT` | SLT_RV32 |
45+
| RV32IM | `LessThanOpcode::SLTU` | SLTU_RV32 |
46+
| RV32IM | `Rv32LoadStoreOpcode::LOADB` | LOADB_RV32 |
47+
| RV32IM | `Rv32LoadStoreOpcode::LOADH` | LOADH_RV32 |
48+
| RV32IM | `Rv32LoadStoreOpcode::LOADW` | LOADW_RV32 |
49+
| RV32IM | `Rv32LoadStoreOpcode::LOADBU` | LOADBU_RV32 |
50+
| RV32IM | `Rv32LoadStoreOpcode::LOADHU` | LOADHU_RV32 |
51+
| RV32IM | `Rv32LoadStoreOpcode::STOREB` | STOREB_RV32 |
52+
| RV32IM | `Rv32LoadStoreOpcode::STOREH` | STOREH_RV32 |
53+
| RV32IM | `Rv32LoadStoreOpcode::STOREW` | STOREW_RV32 |
54+
| RV32IM | `BranchEqualOpcode::BEQ` | BEQ_RV32 |
55+
| RV32IM | `BranchEqualOpcode::BNE` | BNE_RV32 |
56+
| RV32IM | `BranchLessThanOpcode::BLT` | BLT_RV32 |
57+
| RV32IM | `BranchLessThanOpcode::BGE` | BGE_RV32 |
58+
| RV32IM | `BranchLessThanOpcode::BLTU` | BLTU_RV32 |
59+
| RV32IM | `BranchLessThanOpcode::BGEU` | BGEU_RV32 |
60+
| RV32IM | `Rv32JalLuiOpcode::JAL` | JAL_RV32 |
61+
| RV32IM | `Rv32JalrOpcode::JALR` | JALR_RV32 |
62+
| RV32IM | `Rv32JalLuiOpcode::LUI` | LUI_RV32 |
63+
| RV32IM | `Rv32AuipcOpcode::AUIPC` | AUIPC_RV32 |
64+
| RV32IM | `MulOpcode::MUL` | MUL_RV32 |
65+
| RV32IM | `MulHOpcode::MULH` | MULH_RV32 |
66+
| RV32IM | `MulHOpcode::MULHSU` | MULHSU_RV32 |
67+
| RV32IM | `MulHOpcode::MULHU` | MULHU_RV32 |
68+
| RV32IM | `DivRemOpcode::DIV` | DIV_RV32 |
69+
| RV32IM | `DivRemOpcode::DIVU` | DIVU_RV32 |
70+
| RV32IM | `DivRemOpcode::REM` | REM_RV32 |
71+
| RV32IM | `DivRemOpcode::REMU` | REMU_RV32 |
7272
| RV32IM | `Rv32HintStoreOpcode::HINT_STOREW` | HINT_STOREW_RV32 |
7373
| RV32IM | `Rv32HintStoreOpcode::HINT_BUFFER` | HINT_BUFFER_RV32 |
74-
| RV32IM | Pseudo-instruction for `STOREW_RV32` | REVEAL_RV32 |
74+
| RV32IM | Pseudo-instruction for `STOREW_RV32` | REVEAL_RV32 |
75+
| RV32IM | Pseudo-instruction for `STOREW_RV32` | NATIVE_STOREW | |
7576

7677
#### Phantom Sub-Instructions
7778

‎extensions/rv32im/guest/src/io.rs

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,21 @@ macro_rules! reveal {
8181
};
8282
}
8383

84+
/// Store rs1 to [[rd]]_4.
85+
#[macro_export]
86+
macro_rules! store_to_native {
87+
($rd:ident, $rs1:ident) => {
88+
openvm_custom_insn::custom_insn_r!(
89+
opcode = openvm_rv32im_guest::SYSTEM_OPCODE,
90+
funct3 = openvm_rv32im_guest::NATIVE_STOREW_FUNCT3,
91+
funct7 = openvm_rv32im_guest::NATIVE_STOREW_FUNCT7,
92+
rd = In $rd,
93+
rs1 = In $rs1,
94+
rs2 = In $rs1,
95+
)
96+
};
97+
}
98+
8499
/// Print UTF-8 string encoded as bytes to host stdout for debugging purposes.
85100
#[inline(always)]
86101
pub fn print_str_from_bytes(str_as_bytes: &[u8]) {

‎extensions/rv32im/guest/src/lib.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ pub const SYSTEM_OPCODE: u8 = 0x0b;
1414
pub const CSR_OPCODE: u8 = 0b1110011;
1515
pub const RV32_ALU_OPCODE: u8 = 0b0110011;
1616
pub const RV32M_FUNCT7: u8 = 0x01;
17+
pub const NATIVE_STOREW_FUNCT3: u8 = 0b111;
18+
pub const NATIVE_STOREW_FUNCT7: u32 = 2;
1719

1820
pub const TERMINATE_FUNCT3: u8 = 0b000;
1921
pub const HINT_FUNCT3: u8 = 0b001;

‎extensions/rv32im/transpiler/src/lib.rs

Lines changed: 19 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ use openvm_instructions::{
66
};
77
use openvm_rv32im_guest::{
88
PhantomImm, CSRRW_FUNCT3, CSR_OPCODE, HINT_BUFFER_IMM, HINT_FUNCT3, HINT_STOREW_IMM,
9-
PHANTOM_FUNCT3, REVEAL_FUNCT3, RV32M_FUNCT7, RV32_ALU_OPCODE, SYSTEM_OPCODE, TERMINATE_FUNCT3,
9+
NATIVE_STOREW_FUNCT3, NATIVE_STOREW_FUNCT7, PHANTOM_FUNCT3, REVEAL_FUNCT3, RV32M_FUNCT7,
10+
RV32_ALU_OPCODE, SYSTEM_OPCODE, TERMINATE_FUNCT3,
1011
};
1112
use openvm_stark_backend::p3_field::PrimeField32;
1213
use openvm_transpiler::{
@@ -155,9 +156,6 @@ impl<F: PrimeField32> TranspilerExtension<F> for Rv32IoTranspilerExtension {
155156
if opcode != SYSTEM_OPCODE {
156157
return None;
157158
}
158-
if funct3 != HINT_FUNCT3 && funct3 != REVEAL_FUNCT3 {
159-
return None;
160-
}
161159

162160
let instruction = match funct3 {
163161
HINT_FUNCT3 => {
@@ -198,6 +196,23 @@ impl<F: PrimeField32> TranspilerExtension<F> for Rv32IoTranspilerExtension {
198196
(dec_insn.imm < 0) as isize,
199197
))
200198
}
199+
NATIVE_STOREW_FUNCT3 => {
200+
// NATIVE_STOREW is a pseudo-instruction for STOREW_RV32 a,b,0,1,4
201+
let dec_insn = RType::new(instruction_u32);
202+
if dec_insn.funct7 != NATIVE_STOREW_FUNCT7 {
203+
return None;
204+
}
205+
Some(Instruction::large_from_isize(
206+
Rv32LoadStoreOpcode::STOREW.global_opcode(),
207+
(RV32_REGISTER_NUM_LIMBS * dec_insn.rs1) as isize,
208+
(RV32_REGISTER_NUM_LIMBS * dec_insn.rd) as isize,
209+
0,
210+
1,
211+
4,
212+
1,
213+
0,
214+
))
215+
}
201216
_ => return None,
202217
};
203218

0 commit comments

Comments
 (0)