miden-stdlib 0.19.1

Miden VM standard library
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

use.std::crypto::hashes::rpo

use.std::sys::vm::deep_queries
use.std::sys::vm::constraints_eval
use.std::sys::vm::ood_frames
use.std::sys::vm::public_inputs

use.std::crypto::stark::verifier

# Indicates the existence of auxiliary trace segment.
const.IS_AUX_TRACE=1

# Main segment width is 80 (0x50) and there are 1 (0x01) auxiliary segments
# of width 8 (0x08) using 16 (0x10) random extension field elements
const.TRACE_INFO=0x50010810

#! Verifies a STARK proof attesting to the correct execution of a program in the Miden VM.
#!
#! - The public inputs are composed of the input and output stacks, of fixed size equal to 16, as
#!   well as the program and the kernel procedures digests.
#! - There are two trace segments, main and auxiliary. It is assumed that the main trace segment
#!   is 73 columns wide while the auxiliary trace segment is 8 columns wide. Note that we pad the main
#!   trace to the next multiple of 8.
#! - The OOD evaluation frame is composed of two concatenated rows, current and next, each composed
#!   of 73 elements representing the main trace portion and 8 elements for the auxiliary trace one.
#!   Note that, due to the padding of the main trace columns, the number of OOD evaluations per row
#!   is 80 for the main trace.
#!
#! Inputs:  [log(trace_length), num_queries, grinding]
#! Outputs: []
#!
#! Cycles:
#!  1- Remainder polynomial size 64:
#!   2515 + num_queries * (512 + num_fri_layers * 83) + 108 * num_fri_layers + 10 * log(trace_length)
#!  2- Remainder polynomial size 128:
#!   2540 + num_queries * (541 + num_fri_layers * 83) + 108 * num_fri_layers + 10 * log(trace_length)
#!
#!  where num_fri_layers is computed as:
#!
#!  1- If log(trace_length) is even, then num_fri_layers = (log(trace_length) - 6) / 2, where 6 = log2(64),
#!  2- If log(trace_length) is odd, then num_fri_layers = (log(trace_length) - 7) / 2, where 7 = log2(128).
export.verify_proof
    # --- Get constants -------------------------------------------------------

    # Flag indicating the existence of auxiliary trace
    push.IS_AUX_TRACE movdn.3
    # => [log(trace_length), num_queries, grinding, is_aux_trace]

    # Number of fixed length public inputs
    exec.public_inputs::get_num_fixed_len_public_inputs movdn.3
    # => [log(trace_length), num_queries, grinding, num_fixed_len_pi, is_aux_trace]

    # Trace info as one field element
    push.TRACE_INFO movdn.3
    # => [log(trace_length), num_queries, grinding, trace_info, num_fixed_len_pi, is_aux_trace]

    # Number of constraints
    exec.constraints_eval::get_num_constraints movdn.3
    # => [log(trace_length), num_queries, grinding, num_constraints, trace_info, num_fixed_len_pi, is_aux_trace]

    # --- Load the digests of all dynamically invoked procedures --------------

    procref.deep_queries::compute_deep_composition_polynomial_queries
    procref.constraints_eval::execute_constraint_evaluation_check
    procref.ood_frames::process_row_ood_evaluations
    procref.public_inputs::process_public_inputs
    # =>[D3, D2, D1, D0, log(trace_length), num_queries, grinding, num_constraints, trace_info, num_fixed_len_pi, is_aux_trace]

    # --- Call the core verification procedure from `stdlib` ------------------

    exec.verifier::verify
    # => [...]
end