@@ -5,22 +5,85 @@ use eyre::Result;
5
5
use num_bigint:: BigUint ;
6
6
use openvm_algebra_circuit:: { Fp2Extension , ModularExtension } ;
7
7
use openvm_benchmarks_prove:: util:: BenchmarkCli ;
8
- use openvm_circuit:: arch:: { instructions:: exe:: VmExe , SystemConfig } ;
8
+ use openvm_circuit:: arch:: { instructions:: exe:: VmExe , SingleSegmentVmExecutor , SystemConfig } ;
9
+ use openvm_continuations:: verifier:: leaf:: types:: LeafVmVerifierInput ;
9
10
use openvm_ecc_circuit:: { WeierstrassExtension , P256_CONFIG , SECP256K1_CONFIG } ;
11
+ use openvm_native_circuit:: { NativeConfig , NATIVE_MAX_TRACE_HEIGHTS } ;
10
12
use openvm_native_recursion:: halo2:: utils:: { CacheHalo2ParamsReader , DEFAULT_PARAMS_DIR } ;
11
13
use openvm_pairing_circuit:: { PairingCurve , PairingExtension } ;
12
14
use openvm_pairing_guest:: {
13
15
bls12_381:: BLS12_381_COMPLEX_STRUCT_NAME , bn254:: BN254_COMPLEX_STRUCT_NAME ,
14
16
} ;
15
17
use openvm_sdk:: {
16
- commit:: commit_app_exe, config:: SdkVmConfig , prover:: EvmHalo2Prover ,
17
- DefaultStaticVerifierPvHandler , Sdk , StdIn ,
18
+ commit:: commit_app_exe,
19
+ config:: SdkVmConfig ,
20
+ keygen:: AppProvingKey ,
21
+ prover:: { vm:: types:: VmProvingKey , EvmHalo2Prover } ,
22
+ DefaultStaticVerifierPvHandler , NonRootCommittedExe , Sdk , StdIn , SC ,
18
23
} ;
19
24
use openvm_stark_sdk:: {
20
25
bench:: run_with_metric_collection, config:: baby_bear_poseidon2:: BabyBearPoseidon2Engine ,
21
26
} ;
22
27
use openvm_transpiler:: FromElf ;
23
28
29
+ fn verify_native_max_trace_heights (
30
+ sdk : & Sdk ,
31
+ app_pk : Arc < AppProvingKey < SdkVmConfig > > ,
32
+ app_committed_exe : Arc < NonRootCommittedExe > ,
33
+ leaf_vm_pk : Arc < VmProvingKey < SC , NativeConfig > > ,
34
+ num_children_leaf : usize ,
35
+ ) -> Result < ( ) > {
36
+ let app_proof =
37
+ sdk. generate_app_proof ( app_pk. clone ( ) , app_committed_exe. clone ( ) , StdIn :: default ( ) ) ?;
38
+ let leaf_inputs =
39
+ LeafVmVerifierInput :: chunk_continuation_vm_proof ( & app_proof, num_children_leaf) ;
40
+ let vm_vk = leaf_vm_pk. vm_pk . get_vk ( ) ;
41
+
42
+ leaf_inputs. iter ( ) . for_each ( |leaf_input| {
43
+ let executor = {
44
+ let mut executor = SingleSegmentVmExecutor :: new ( leaf_vm_pk. vm_config . clone ( ) ) ;
45
+ executor
46
+ . set_trace_height_constraints ( leaf_vm_pk. vm_pk . trace_height_constraints . clone ( ) ) ;
47
+ executor
48
+ } ;
49
+ let max_trace_heights = executor
50
+ . execute_metered (
51
+ app_pk. leaf_committed_exe . exe . clone ( ) ,
52
+ leaf_input. write_to_stream ( ) ,
53
+ & vm_vk. total_widths ( ) ,
54
+ & vm_vk. num_interactions ( ) ,
55
+ )
56
+ . expect ( "execute_metered failed" ) ;
57
+ println ! ( "max_trace_heights: {:?}" , max_trace_heights) ;
58
+
59
+ let actual_trace_heights = executor
60
+ . execute_and_generate (
61
+ app_pk. leaf_committed_exe . clone ( ) ,
62
+ leaf_input. write_to_stream ( ) ,
63
+ & max_trace_heights,
64
+ )
65
+ . expect ( "execute_and_generate failed" )
66
+ . per_air
67
+ . iter ( )
68
+ . map ( |( _, air) | air. raw . height ( ) )
69
+ . collect :: < Vec < usize > > ( ) ;
70
+ println ! ( "actual_trace_heights: {:?}" , actual_trace_heights) ;
71
+
72
+ actual_trace_heights
73
+ . iter ( )
74
+ . zip ( NATIVE_MAX_TRACE_HEIGHTS )
75
+ . for_each ( |( & actual, & expected) | {
76
+ assert ! (
77
+ actual <= ( expected as usize ) ,
78
+ "Actual trace height {} exceeds expected height {}" ,
79
+ actual,
80
+ expected
81
+ ) ;
82
+ } ) ;
83
+ } ) ;
84
+ Ok ( ( ) )
85
+ }
86
+
24
87
fn main ( ) -> Result < ( ) > {
25
88
let args = BenchmarkCli :: parse ( ) ;
26
89
@@ -88,6 +151,15 @@ fn main() -> Result<()> {
88
151
& DefaultStaticVerifierPvHandler ,
89
152
) ?;
90
153
154
+ // Verify that NATIVE_MAX_TRACE_HEIGHTS remains valid
155
+ verify_native_max_trace_heights (
156
+ & sdk,
157
+ app_pk. clone ( ) ,
158
+ app_committed_exe. clone ( ) ,
159
+ full_agg_pk. agg_stark_pk . leaf_vm_pk . clone ( ) ,
160
+ args. agg_tree_config . num_children_leaf ,
161
+ ) ?;
162
+
91
163
run_with_metric_collection ( "OUTPUT_PATH" , || -> Result < ( ) > {
92
164
let mut prover = EvmHalo2Prover :: < _ , BabyBearPoseidon2Engine > :: new (
93
165
& halo2_params_reader,
0 commit comments