winter_prover/trace/
mod.rs

1// Copyright (c) Facebook, Inc. and its affiliates.
2//
3// This source code is licensed under the MIT license found in the
4// LICENSE file in the root directory of this source tree.
5
6use air::{Air, AuxRandElements, EvaluationFrame, TraceInfo};
7use math::{polynom, FieldElement, StarkField};
8
9use super::ColMatrix;
10
11mod trace_lde;
12pub use trace_lde::{DefaultTraceLde, TraceLde};
13
14mod poly_table;
15pub use poly_table::TracePolyTable;
16
17mod trace_table;
18pub use trace_table::{TraceTable, TraceTableFragment};
19
20#[cfg(test)]
21mod tests;
22
23// AUX TRACE WITH METADATA
24// ================================================================================================
25
26/// Holds the auxiliary trace, the random elements used when generating the auxiliary trace.
27pub struct AuxTraceWithMetadata<E: FieldElement> {
28    pub aux_trace: ColMatrix<E>,
29    pub aux_rand_elements: AuxRandElements<E>,
30}
31
32// TRACE TRAIT
33// ================================================================================================
34/// Defines an execution trace of a computation.
35///
36/// Execution trace can be reduced to a two-dimensional matrix in which each row represents the
37/// state of a computation at a single point in time and each column corresponds to an algebraic
38/// column tracked over all steps of the computation.
39///
40/// Building a trace is required for STARK proof generation. An execution trace of a specific
41/// instance of a computation must be supplied to [Prover::prove()](super::Prover::prove) method
42/// to generate a STARK proof.
43///
44/// This crate exposes one concrete implementation of the [Trace] trait: [TraceTable]. This
45/// implementation supports concurrent trace generation and should be sufficient in most
46/// situations. However, if functionality provided by [TraceTable] is not sufficient, uses can
47/// provide custom implementations of the [Trace] trait which better suit their needs.
48pub trait Trace: Sized {
49    /// Base field for this execution trace.
50    ///
51    /// All cells of this execution trace contain values which are elements in this field.
52    type BaseField: StarkField;
53
54    // REQUIRED METHODS
55    // --------------------------------------------------------------------------------------------
56    /// Returns trace info for this trace.
57    fn info(&self) -> &TraceInfo;
58
59    /// Returns a reference to a [Matrix] describing the main segment of this trace.
60    fn main_segment(&self) -> &ColMatrix<Self::BaseField>;
61
62    /// Reads an evaluation frame from the main trace segment at the specified row.
63    fn read_main_frame(&self, row_idx: usize, frame: &mut EvaluationFrame<Self::BaseField>);
64
65    // PROVIDED METHODS
66    // --------------------------------------------------------------------------------------------
67
68    /// Returns the number of rows in this trace.
69    fn length(&self) -> usize {
70        self.info().length()
71    }
72
73    /// Returns the number of columns in the main segment of this trace.
74    fn main_trace_width(&self) -> usize {
75        self.info().main_trace_width()
76    }
77
78    /// Returns the number of columns in the auxiliary trace segment.
79    fn aux_trace_width(&self) -> usize {
80        self.info().aux_segment_width()
81    }
82
83    /// Checks if this trace is valid against the specified AIR, and panics if not.
84    ///
85    /// NOTE: this is a very expensive operation and is intended for use only in debug mode.
86    fn validate<A, E>(&self, air: &A, aux_trace_with_metadata: Option<&AuxTraceWithMetadata<E>>)
87    where
88        A: Air<BaseField = Self::BaseField>,
89        E: FieldElement<BaseField = Self::BaseField>,
90    {
91        // make sure the width align; if they don't something went terribly wrong
92        assert_eq!(
93            self.main_trace_width(),
94            air.trace_info().main_trace_width(),
95            "inconsistent trace width: expected {}, but was {}",
96            self.main_trace_width(),
97            air.trace_info().main_trace_width(),
98        );
99
100        // --- 1. make sure the assertions are valid ----------------------------------------------
101
102        // first, check assertions against the main segment of the execution trace
103        for assertion in air.get_assertions() {
104            assertion.apply(self.length(), |step, value| {
105                assert!(
106                    value == self.main_segment().get(assertion.column(), step),
107                    "trace does not satisfy assertion main_trace({}, {}) == {}",
108                    assertion.column(),
109                    step,
110                    value
111                );
112            });
113        }
114
115        // then, check assertions against the auxiliary trace segment
116        if let Some(aux_trace_with_metadata) = aux_trace_with_metadata {
117            let aux_trace = &aux_trace_with_metadata.aux_trace;
118            let aux_rand_elements = &aux_trace_with_metadata.aux_rand_elements;
119
120            for assertion in air.get_aux_assertions(aux_rand_elements) {
121                // get the matrix and verify the assertion against it
122                assertion.apply(self.length(), |step, value| {
123                    assert!(
124                        value == aux_trace.get(assertion.column(), step),
125                        "trace does not satisfy assertion aux_trace({}, {}) == {}",
126                        assertion.column(),
127                        step,
128                        value
129                    );
130                });
131            }
132        }
133
134        // --- 2. make sure this trace satisfies all transition constraints -----------------------
135
136        // collect the info needed to build periodic values for a specific step
137        let g = air.trace_domain_generator();
138        let periodic_values_polys = air.get_periodic_column_polys();
139        let mut periodic_values = vec![Self::BaseField::ZERO; periodic_values_polys.len()];
140
141        // initialize buffers to hold evaluation frames and results of constraint evaluations
142        let mut x = Self::BaseField::ONE;
143        let mut main_frame = EvaluationFrame::new(self.main_trace_width());
144        let mut aux_frame = if air.trace_info().is_multi_segment() {
145            Some(EvaluationFrame::<E>::new(self.aux_trace_width()))
146        } else {
147            None
148        };
149        let mut main_evaluations =
150            vec![Self::BaseField::ZERO; air.context().num_main_transition_constraints()];
151        let mut aux_evaluations = vec![E::ZERO; air.context().num_aux_transition_constraints()];
152
153        // we check transition constraints on all steps except the last k steps, where k is the
154        // number of steps exempt from transition constraints (guaranteed to be at least 1)
155        for step in 0..self.length() - air.context().num_transition_exemptions() {
156            // build periodic values
157            for (p, v) in periodic_values_polys.iter().zip(periodic_values.iter_mut()) {
158                let num_cycles = air.trace_length() / p.len();
159                let x = x.exp((num_cycles as u32).into());
160                *v = polynom::eval(p, x);
161            }
162
163            // evaluate transition constraints for the main trace segment and make sure they all
164            // evaluate to zeros
165            self.read_main_frame(step, &mut main_frame);
166            air.evaluate_transition(&main_frame, &periodic_values, &mut main_evaluations);
167            for (i, &evaluation) in main_evaluations.iter().enumerate() {
168                assert!(
169                    evaluation == Self::BaseField::ZERO,
170                    "main transition constraint {i} did not evaluate to ZERO at step {step}"
171                );
172            }
173
174            // evaluate transition constraints for the auxiliary trace segment (if any) and make
175            // sure they all evaluate to zeros
176            if let Some(ref mut aux_frame) = aux_frame {
177                let aux_trace_with_metadata =
178                    aux_trace_with_metadata.expect("expected aux trace to be present");
179                let aux_trace = &aux_trace_with_metadata.aux_trace;
180                let aux_rand_elements = &aux_trace_with_metadata.aux_rand_elements;
181
182                read_aux_frame(aux_trace, step, aux_frame);
183                air.evaluate_aux_transition(
184                    &main_frame,
185                    aux_frame,
186                    &periodic_values,
187                    aux_rand_elements,
188                    &mut aux_evaluations,
189                );
190                for (i, &evaluation) in aux_evaluations.iter().enumerate() {
191                    assert!(
192                        evaluation == E::ZERO,
193                        "auxiliary transition constraint {i} did not evaluate to ZERO at step {step}"
194                    );
195                }
196            }
197
198            // update x coordinate of the domain
199            x *= g;
200        }
201    }
202}
203
204// HELPER FUNCTIONS
205// ================================================================================================
206
207/// Reads an evaluation frame from the provided auxiliary segment.
208///
209/// This is probably not the most efficient implementation, but since we call this function only
210/// for trace validation purposes (which is done in debug mode only), we don't care all that much
211/// about its performance.
212fn read_aux_frame<E>(aux_segment: &ColMatrix<E>, row_idx: usize, frame: &mut EvaluationFrame<E>)
213where
214    E: FieldElement,
215{
216    for (current_frame_cell, aux_segment_col) in
217        frame.current_mut().iter_mut().zip(aux_segment.columns())
218    {
219        *current_frame_cell = aux_segment_col[row_idx];
220    }
221
222    let next_row_idx = (row_idx + 1) % aux_segment.num_rows();
223    for (next_frame_cell, aux_segment_col) in frame.next_mut().iter_mut().zip(aux_segment.columns())
224    {
225        *next_frame_cell = aux_segment_col[next_row_idx];
226    }
227}