miden_processor/trace/chiplets/aux_trace/
mod.rs

1use alloc::vec::Vec;
2
3use miden_air::trace::MainTrace;
4use miden_core::{field::ExtensionField, precompile::PrecompileTranscriptState, program::Kernel};
5use wiring_bus::WiringBusBuilder;
6
7use super::{Felt, ace::AceHints};
8use crate::trace::AuxColumnBuilder;
9
10mod bus;
11pub use bus::{
12    BusColumnBuilder, build_ace_memory_read_element_request, build_ace_memory_read_word_request,
13};
14
15mod virtual_table;
16pub use virtual_table::ChipletsVTableColBuilder;
17
18mod wiring_bus;
19
20/// Constructs the execution trace for chiplets-related auxiliary columns (used in multiset checks).
21#[derive(Debug, Clone)]
22pub struct AuxTraceBuilder {
23    kernel: Kernel,
24    ace_hints: AceHints,
25    /// Final precompile transcript state (sponge capacity) emitted by the VM.
26    final_transcript_state: PrecompileTranscriptState,
27}
28
29impl AuxTraceBuilder {
30    // CONSTRUCTORS
31    // --------------------------------------------------------------------------------------------
32
33    pub fn new(
34        kernel: Kernel,
35        ace_hints: AceHints,
36        final_transcript_state: PrecompileTranscriptState,
37    ) -> Self {
38        Self {
39            kernel,
40            ace_hints,
41            final_transcript_state,
42        }
43    }
44
45    // COLUMN TRACE CONSTRUCTOR
46    // --------------------------------------------------------------------------------------------
47
48    /// Builds and returns the Chiplets's auxiliary trace columns. This consists of:
49    ///
50    /// 1. A bus column `b_chip` describing requests made by the stack and decoder and responses
51    ///    received from the chiplets in the Chiplets module. It also responds to requests made by
52    ///    the verifier with kernel procedure hashes included in the public inputs of the program.
53    /// 2. A column acting as
54    ///    - a virtual table for the sibling table used by the hasher chiplet,
55    ///    - a bus between the memory chiplet and the ACE chiplet.
56    /// 3. A column used as a bus to wire the gates of the ACE chiplet.
57    pub fn build_aux_columns<E: ExtensionField<Felt>>(
58        &self,
59        main_trace: &MainTrace,
60        rand_elements: &[E],
61    ) -> [Vec<E>; 3] {
62        let v_table_col_builder = ChipletsVTableColBuilder::new(self.final_transcript_state);
63        let bus_col_builder = BusColumnBuilder::new(&self.kernel);
64        let wiring_bus_builder = WiringBusBuilder::new(&self.ace_hints);
65        let t_chip = v_table_col_builder.build_aux_column(main_trace, rand_elements);
66        let b_chip = bus_col_builder.build_aux_column(main_trace, rand_elements);
67        let wiring_bus = wiring_bus_builder.build_aux_column(main_trace, rand_elements);
68
69        // When debugging, check that all multi-set and logUp interactions are valid.
70        let v_table_final_value = t_chip.last().copied().unwrap_or(E::ONE);
71        let chiplets_bus_final_value = b_chip.last().copied().unwrap_or(E::ONE);
72        let log_up_final_value = wiring_bus.last().copied().unwrap_or(E::ZERO);
73
74        debug_assert_eq!(log_up_final_value, E::ZERO);
75        debug_assert_eq!(v_table_final_value * chiplets_bus_final_value, E::ONE);
76
77        [t_chip, b_chip, wiring_bus]
78    }
79}
80
81// HELPER FUNCTIONS
82// ================================================================================================
83
84/// Runs an inner product between the alphas and the elements.
85#[inline(always)]
86fn build_value<E, const N: usize>(alphas: &[E], elements: [Felt; N]) -> E
87where
88    E: ExtensionField<Felt>,
89{
90    debug_assert_eq!(alphas.len(), elements.len());
91    let mut value = alphas[0] * elements[0];
92    for i in 1..N {
93        value += alphas[i] * elements[i];
94    }
95    value
96}
miden_processor/trace/chiplets/aux_trace/mod.rs

miden_processor/trace/chiplets/aux_trace/
mod.rs
