miden-processor 0.9.2

Miden VM processor
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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174

use super::{uninit_vector, Felt, FieldElement, NUM_RAND_ROWS};
use alloc::collections::BTreeMap;
use alloc::vec::Vec;
use miden_air::trace::main_trace::MainTrace;
use miden_air::trace::range::{M_COL_IDX, V_COL_IDX};

// AUXILIARY TRACE BUILDER
// ================================================================================================

/// Describes how to construct the execution trace of columns related to the range checker in the
/// auxiliary segment of the trace. These are used in multiset checks.
pub struct AuxTraceBuilder {
    /// A list of the unique values for which range checks are performed.
    lookup_values: Vec<u16>,
    /// Range check lookups performed by all user operations, grouped and sorted by the clock cycle
    /// at which they are requested.
    cycle_lookups: BTreeMap<u32, Vec<u16>>,
    // The index of the first row of Range Checker's trace when the padded rows end and values to
    // be range checked start.
    values_start: usize,
}

impl AuxTraceBuilder {
    // CONSTRUCTOR
    // --------------------------------------------------------------------------------------------
    pub fn new(
        lookup_values: Vec<u16>,
        cycle_lookups: BTreeMap<u32, Vec<u16>>,
        values_start: usize,
    ) -> Self {
        Self {
            lookup_values,
            cycle_lookups,
            values_start,
        }
    }

    // AUX COLUMN BUILDERS
    // --------------------------------------------------------------------------------------------

    /// Builds and returns range checker auxiliary trace columns. Currently this consists of one
    /// column:
    /// - `b_range`: ensures that the range checks performed by the Range Checker match those
    ///   requested by the Stack and Memory processors.
    pub fn build_aux_columns<E: FieldElement<BaseField = Felt>>(
        &self,
        main_trace: &MainTrace,
        rand_elements: &[E],
    ) -> Vec<Vec<E>> {
        let b_range = self.build_aux_col_b_range(main_trace, rand_elements);
        vec![b_range]
    }

    /// Builds the execution trace of the range check `b_range` column which ensure that the range
    /// check lookups performed by user operations match those executed by the Range Checker.
    fn build_aux_col_b_range<E: FieldElement<BaseField = Felt>>(
        &self,
        main_trace: &MainTrace,
        rand_elements: &[E],
    ) -> Vec<E> {
        // run batch inversion on the lookup values
        let divisors = get_divisors(&self.lookup_values, rand_elements[0]);

        // allocate memory for the running sum column and set the initial value to ONE
        let mut b_range = unsafe { uninit_vector(main_trace.num_rows()) };
        b_range[0] = E::ONE;

        // keep track of the last updated row in the `b_range` running sum column. `b_range` is
        // filled with result values that are added to the next row after the operation's execution.
        let mut b_range_idx = 0_usize;

        // the first half of the trace only includes values from the operations.
        for (clk, range_checks) in self.cycle_lookups.range(0..self.values_start as u32) {
            let clk = *clk as usize;

            // if we skipped some cycles since the last update was processed, values in the last
            // updated row should be copied over until the current cycle.
            if b_range_idx < clk {
                let last_value = b_range[b_range_idx];
                b_range[(b_range_idx + 1)..=clk].fill(last_value);
            }

            // move the column pointer to the next row.
            b_range_idx = clk + 1;

            b_range[b_range_idx] = b_range[clk];
            // include the operation lookups
            for lookup in range_checks.iter() {
                let value = divisors.get(lookup).expect("invalid lookup value {}");
                b_range[b_range_idx] -= *value;
            }
        }

        // if we skipped some cycles since the last update was processed, values in the last
        // updated row should by copied over until the current cycle.
        if b_range_idx < self.values_start {
            let last_value = b_range[b_range_idx];
            b_range[(b_range_idx + 1)..=self.values_start].fill(last_value);
        }

        // after the padded section of the range checker table, include the lookup value specified
        // by the range checker into the running sum at each step, and remove lookups from user ops
        // at any step where user ops were executed.
        for (row_idx, (multiplicity, lookup)) in main_trace
            .get_column(M_COL_IDX)
            .iter()
            .zip(main_trace.get_column(V_COL_IDX).iter())
            .enumerate()
            .take(main_trace.num_rows() - NUM_RAND_ROWS)
            .skip(self.values_start)
        {
            b_range_idx = row_idx + 1;

            if multiplicity.as_int() != 0 {
                // add the value in the range checker: multiplicity / (alpha - lookup)
                let value = divisors.get(&(lookup.as_int() as u16)).expect("invalid lookup value");
                b_range[b_range_idx] = b_range[row_idx] + value.mul_base(*multiplicity);
            } else {
                b_range[b_range_idx] = b_range[row_idx];
            }

            // subtract the range checks requested by operations
            if let Some(range_checks) = self.cycle_lookups.get(&(row_idx as u32)) {
                for lookup in range_checks.iter() {
                    let value = divisors.get(lookup).expect("invalid lookup value");
                    b_range[b_range_idx] -= *value;
                }
            }
        }

        // at this point, all range checks from user operations and the range checker should be
        // matched - so, the last value must be ONE;
        assert_eq!(b_range[b_range_idx], E::ONE);

        if b_range_idx < b_range.len() - 1 {
            b_range[(b_range_idx + 1)..].fill(E::ONE);
        }

        b_range
    }
}

/// Runs batch inversion on all range check lookup values and returns a map which maps each value
/// to the divisor used for including it in the LogUp lookup. In other words, the map contains
/// mappings of x to 1/(alpha - x).
fn get_divisors<E: FieldElement<BaseField = Felt>>(
    lookup_values: &[u16],
    alpha: E,
) -> BTreeMap<u16, E> {
    // run batch inversion on the lookup values
    let mut values = unsafe { uninit_vector(lookup_values.len()) };
    let mut inv_values = unsafe { uninit_vector(lookup_values.len()) };
    let mut log_values = BTreeMap::new();

    let mut acc = E::ONE;
    for (i, (value, inv_value)) in values.iter_mut().zip(inv_values.iter_mut()).enumerate() {
        *inv_value = acc;
        *value = alpha - E::from(lookup_values[i]);
        acc *= *value;
    }

    // invert the accumulated product
    acc = acc.inv();

    // multiply the accumulated product by the original values to compute the inverses, then
    // build a map of inverses for the lookup values
    for i in (0..lookup_values.len()).rev() {
        inv_values[i] *= acc;
        acc *= values[i];
        log_values.insert(lookup_values[i], inv_values[i]);
    }

    log_values
}