1
1
use std:: array;
2
2
3
3
use openvm_circuit:: arch:: instructions:: program:: Program ;
4
- use openvm_native_compiler:: { conversion:: CompilerOptions , prelude:: * } ;
4
+ use openvm_native_compiler:: { asm :: HEAP_START_ADDRESS , conversion:: CompilerOptions , prelude:: * } ;
5
5
use openvm_native_recursion:: {
6
6
fri:: TwoAdicFriPcsVariable , hints:: Hintable , types:: new_from_inner_multi_vk,
7
7
utils:: const_fri_config,
8
8
} ;
9
+ use openvm_stark_backend:: proof:: Proof ;
9
10
use openvm_stark_sdk:: {
10
11
config:: FriParameters ,
11
12
openvm_stark_backend:: { keygen:: types:: MultiStarkVerifyingKey , p3_field:: FieldAlgebra } ,
@@ -30,7 +31,7 @@ mod vars;
30
31
pub struct RootVmVerifierConfig {
31
32
pub leaf_fri_params : FriParameters ,
32
33
pub internal_fri_params : FriParameters ,
33
- pub num_public_values : usize ,
34
+ pub num_user_public_values : usize ,
34
35
pub internal_vm_verifier_commit : [ F ; DIGEST_SIZE ] ,
35
36
pub compiler_options : CompilerOptions ,
36
37
}
@@ -40,73 +41,163 @@ impl RootVmVerifierConfig {
40
41
leaf_vm_vk : & MultiStarkVerifyingKey < SC > ,
41
42
internal_vm_vk : & MultiStarkVerifyingKey < SC > ,
42
43
) -> Program < F > {
43
- let leaf_advice = new_from_inner_multi_vk ( leaf_vm_vk) ;
44
- let internal_advice = new_from_inner_multi_vk ( internal_vm_vk) ;
45
44
let mut builder = Builder :: < C > :: default ( ) ;
46
45
47
- {
48
- builder. cycle_tracker_start ( "ReadProofsFromInput" ) ;
49
- let RootVmVerifierInputVariable {
46
+ builder. cycle_tracker_start ( "ReadProofsFromInput" ) ;
47
+ let root_verifier_input = RootVmVerifierInput :: < SC > :: read ( & mut builder) ;
48
+ builder. cycle_tracker_end ( "ReadProofsFromInput" ) ;
49
+ let pvs = self . verifier_impl (
50
+ & mut builder,
51
+ leaf_vm_vk,
52
+ internal_vm_vk,
53
+ root_verifier_input,
54
+ ) ;
55
+ pvs. flatten ( )
56
+ . into_iter ( )
57
+ . for_each ( |v| builder. commit_public_value ( v) ) ;
58
+ builder. halt ( ) ;
59
+ builder. compile_isa_with_options ( self . compiler_options )
60
+ }
61
+
62
+ /// Build instructions which can be called as a kernel function in RISC-V guest programs.
63
+ /// Inputs for generated instructions:
64
+ /// - expected `app_exe_commit`, `app_vm_commit` and user public values should be stored from
65
+ /// `HEAP_START_ADDRESS` in the native address space .
66
+ ///
67
+ /// These instructions take a proof from the input stream and verify the proof. Then these
68
+ /// instructions check if the public values are consistent with the expected public values
69
+ /// from RISC-V guest programs.
70
+ pub fn build_kernel_asm (
71
+ & self ,
72
+ leaf_vm_vk : & MultiStarkVerifyingKey < SC > ,
73
+ internal_vm_vk : & MultiStarkVerifyingKey < SC > ,
74
+ ) -> Program < F > {
75
+ let mut builder = Builder :: < C > :: default ( ) ;
76
+
77
+ const BYTE_PER_WORD : usize = 4 ;
78
+ let num_public_values = self . num_user_public_values + DIGEST_SIZE * 2 ;
79
+ let num_bytes = num_public_values * BYTE_PER_WORD ;
80
+ // Move heap pointer in order to keep input arguments from address space 2.
81
+ let heap_addr: Var < F > = builder. eval ( F :: from_canonical_u32 (
82
+ HEAP_START_ADDRESS as u32 + num_bytes as u32 ,
83
+ ) ) ;
84
+ builder. store_heap_ptr ( Ptr { address : heap_addr } ) ;
85
+ let expected_pvs: Vec < Felt < _ > > = ( 0 ..num_public_values)
86
+ . map ( |i| {
87
+ let fs: [ Felt < _ > ; BYTE_PER_WORD ] = array:: from_fn ( |j| {
88
+ let ptr = Ptr {
89
+ address : builder. eval ( F :: from_canonical_u32 (
90
+ HEAP_START_ADDRESS as u32 + ( i * 4 ) as u32 ,
91
+ ) ) ,
92
+ } ;
93
+ let idx = MemIndex {
94
+ index : RVar :: from ( j) ,
95
+ offset : 0 ,
96
+ size : 1 ,
97
+ } ;
98
+ let f = Felt :: uninit ( & mut builder) ;
99
+ f. load ( ptr, idx, & mut builder) ;
100
+ f
101
+ } ) ;
102
+ builder. eval (
103
+ fs[ 0 ]
104
+ + fs[ 1 ] * F :: from_canonical_u32 ( 1 << 8 )
105
+ + fs[ 2 ] * F :: from_canonical_u32 ( 1 << 16 )
106
+ + fs[ 3 ] * F :: from_canonical_u32 ( 1 << 24 ) ,
107
+ )
108
+ } )
109
+ . collect ( ) ;
110
+ let expected_pvs = RootVmVerifierPvs :: < Felt < F > > :: from_flatten ( expected_pvs) ;
111
+ let user_pvs = builder. array ( self . num_user_public_values ) ;
112
+ for ( i, & pv) in expected_pvs. public_values . iter ( ) . enumerate ( ) {
113
+ builder. set ( & user_pvs, i, pv) ;
114
+ }
115
+
116
+ builder. cycle_tracker_start ( "ReadFromStdin" ) ;
117
+ let proof = Proof :: < SC > :: read ( & mut builder) ;
118
+ builder. cycle_tracker_end ( "ReadFromStdin" ) ;
119
+ let proofs = builder. array ( 1 ) ;
120
+ builder. set ( & proofs, 0 , proof) ;
121
+ let pvs = self . verifier_impl (
122
+ & mut builder,
123
+ leaf_vm_vk,
124
+ internal_vm_vk,
125
+ RootVmVerifierInputVariable {
50
126
proofs,
51
- public_values,
52
- } = RootVmVerifierInput :: < SC > :: read ( & mut builder) ;
53
- builder. cycle_tracker_end ( "ReadProofsFromInput" ) ;
54
- builder. cycle_tracker_start ( "InitializePcsConst" ) ;
55
- let leaf_pcs = TwoAdicFriPcsVariable {
56
- config : const_fri_config ( & mut builder, & self . leaf_fri_params ) ,
57
- } ;
58
- let internal_pcs = TwoAdicFriPcsVariable {
59
- config : const_fri_config ( & mut builder, & self . internal_fri_params ) ,
60
- } ;
61
- builder. cycle_tracker_end ( "InitializePcsConst" ) ;
62
- builder. cycle_tracker_start ( "VerifyProofs" ) ;
63
- let internal_program_commit =
64
- array:: from_fn ( |i| builder. eval ( self . internal_vm_verifier_commit [ i] ) ) ;
65
- let non_leaf_verifier = NonLeafVerifierVariables {
66
- internal_program_commit,
67
- leaf_pcs,
68
- leaf_advice,
69
- internal_pcs,
70
- internal_advice,
71
- } ;
72
- let ( merged_pvs, expected_leaf_commit) =
73
- non_leaf_verifier. verify_internal_or_leaf_verifier_proofs ( & mut builder, & proofs) ;
74
- builder. cycle_tracker_end ( "VerifyProofs" ) ;
127
+ public_values : user_pvs,
128
+ } ,
129
+ ) ;
130
+ builder. assert_eq :: < [ Felt < _ > ; DIGEST_SIZE ] > ( pvs. exe_commit , expected_pvs. exe_commit ) ;
131
+ builder. assert_eq :: < [ Felt < _ > ; DIGEST_SIZE ] > (
132
+ pvs. leaf_verifier_commit ,
133
+ expected_pvs. leaf_verifier_commit ,
134
+ ) ;
135
+
136
+ builder. compile_isa_with_options ( self . compiler_options )
137
+ }
138
+
139
+ fn verifier_impl (
140
+ & self ,
141
+ builder : & mut Builder < C > ,
142
+ leaf_vm_vk : & MultiStarkVerifyingKey < SC > ,
143
+ internal_vm_vk : & MultiStarkVerifyingKey < SC > ,
144
+ root_verifier_input : RootVmVerifierInputVariable < C > ,
145
+ ) -> RootVmVerifierPvs < Felt < F > > {
146
+ let leaf_advice = new_from_inner_multi_vk ( leaf_vm_vk) ;
147
+ let internal_advice = new_from_inner_multi_vk ( internal_vm_vk) ;
148
+ let RootVmVerifierInputVariable {
149
+ proofs,
150
+ public_values,
151
+ } = root_verifier_input;
75
152
76
- // App Program should terminate
77
- builder. assert_felt_eq ( merged_pvs. connector . is_terminate , F :: ONE ) ;
78
- // App Program should exit successfully
79
- builder. assert_felt_eq ( merged_pvs. connector . exit_code , F :: ZERO ) ;
153
+ builder. cycle_tracker_start ( "InitializePcsConst" ) ;
154
+ let leaf_pcs = TwoAdicFriPcsVariable {
155
+ config : const_fri_config ( builder, & self . leaf_fri_params ) ,
156
+ } ;
157
+ let internal_pcs = TwoAdicFriPcsVariable {
158
+ config : const_fri_config ( builder, & self . internal_fri_params ) ,
159
+ } ;
160
+ builder. cycle_tracker_end ( "InitializePcsConst" ) ;
161
+ builder. cycle_tracker_start ( "VerifyProofs" ) ;
162
+ let internal_program_commit =
163
+ array:: from_fn ( |i| builder. eval ( self . internal_vm_verifier_commit [ i] ) ) ;
164
+ let non_leaf_verifier = NonLeafVerifierVariables {
165
+ internal_program_commit,
166
+ leaf_pcs,
167
+ leaf_advice,
168
+ internal_pcs,
169
+ internal_advice,
170
+ } ;
171
+ let ( merged_pvs, expected_leaf_commit) =
172
+ non_leaf_verifier. verify_internal_or_leaf_verifier_proofs ( builder, & proofs) ;
173
+ builder. cycle_tracker_end ( "VerifyProofs" ) ;
80
174
81
- builder. cycle_tracker_start ( "ExtractPublicValues" ) ;
82
- builder. assert_usize_eq ( public_values. len ( ) , RVar :: from ( self . num_public_values ) ) ;
83
- let public_values_vec: Vec < Felt < F > > = ( 0 ..self . num_public_values )
84
- . map ( |i| builder. get ( & public_values, i) )
85
- . collect ( ) ;
86
- let hasher = VariableP2Hasher :: new ( & mut builder) ;
87
- let pv_commit = hasher. merkle_root ( & mut builder, & public_values_vec) ;
88
- builder. assert_eq :: < [ _ ; DIGEST_SIZE ] > ( merged_pvs. public_values_commit , pv_commit) ;
89
- builder. cycle_tracker_end ( "ExtractPublicValues" ) ;
175
+ // App Program should terminate
176
+ builder. assert_felt_eq ( merged_pvs. connector . is_terminate , F :: ONE ) ;
177
+ // App Program should exit successfully
178
+ builder. assert_felt_eq ( merged_pvs. connector . exit_code , F :: ZERO ) ;
90
179
91
- let pvs = RootVmVerifierPvs {
92
- exe_commit : compute_exe_commit (
93
- & mut builder,
94
- & hasher,
95
- merged_pvs. app_commit ,
96
- merged_pvs. memory . initial_root ,
97
- merged_pvs. connector . initial_pc ,
98
- ) ,
99
- leaf_verifier_commit : expected_leaf_commit,
100
- public_values : public_values_vec,
101
- } ;
102
- pvs. flatten ( )
103
- . into_iter ( )
104
- . for_each ( |v| builder. commit_public_value ( v) ) ;
180
+ builder. cycle_tracker_start ( "ExtractPublicValues" ) ;
181
+ builder. assert_usize_eq ( public_values. len ( ) , RVar :: from ( self . num_user_public_values ) ) ;
182
+ let public_values_vec: Vec < Felt < F > > = ( 0 ..self . num_user_public_values )
183
+ . map ( |i| builder. get ( & public_values, i) )
184
+ . collect ( ) ;
185
+ let hasher = VariableP2Hasher :: new ( builder) ;
186
+ let pv_commit = hasher. merkle_root ( builder, & public_values_vec) ;
187
+ builder. assert_eq :: < [ _ ; DIGEST_SIZE ] > ( merged_pvs. public_values_commit , pv_commit) ;
188
+ builder. cycle_tracker_end ( "ExtractPublicValues" ) ;
105
189
106
- builder. halt ( ) ;
190
+ RootVmVerifierPvs {
191
+ exe_commit : compute_exe_commit (
192
+ builder,
193
+ & hasher,
194
+ merged_pvs. app_commit ,
195
+ merged_pvs. memory . initial_root ,
196
+ merged_pvs. connector . initial_pc ,
197
+ ) ,
198
+ leaf_verifier_commit : expected_leaf_commit,
199
+ public_values : public_values_vec,
107
200
}
108
-
109
- builder. compile_isa_with_options ( self . compiler_options )
110
201
}
111
202
}
112
203
0 commit comments