miden_processor/trace/chiplets/aux_trace/
mod.rs

1use alloc::vec::Vec;
2
3use miden_air::trace::{Challenges, MainTrace};
4use miden_core::field::ExtensionField;
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    ace_hints: AceHints,
24}
25
26impl AuxTraceBuilder {
27    // CONSTRUCTORS
28    // --------------------------------------------------------------------------------------------
29
30    pub fn new(ace_hints: AceHints) -> Self {
31        Self { ace_hints }
32    }
33
34    // COLUMN TRACE CONSTRUCTOR
35    // --------------------------------------------------------------------------------------------
36
37    /// Builds and returns the Chiplets's auxiliary trace columns. This consists of:
38    ///
39    /// 1. A bus column `b_chip` describing requests made by the stack and decoder and responses
40    ///    received from the chiplets in the Chiplets module. It also responds to requests made by
41    ///    the verifier with kernel procedure hashes included in the public inputs of the program.
42    /// 2. A column acting as
43    ///    - a virtual table for the sibling table used by the hasher chiplet,
44    ///    - a bus between the memory chiplet and the ACE chiplet.
45    /// 3. A column used as a bus to wire the gates of the ACE chiplet.
46    pub(crate) fn build_aux_columns<E: ExtensionField<Felt>>(
47        &self,
48        main_trace: &MainTrace,
49        challenges: &Challenges<E>,
50    ) -> [Vec<E>; 3] {
51        let v_table_col_builder = ChipletsVTableColBuilder;
52        let bus_col_builder = BusColumnBuilder;
53        let wiring_bus_builder = WiringBusBuilder::new(&self.ace_hints);
54        let t_chip = v_table_col_builder.build_aux_column(main_trace, challenges);
55        let b_chip = bus_col_builder.build_aux_column(main_trace, challenges);
56        let wiring_bus = wiring_bus_builder.build_aux_column(main_trace, challenges);
57
58        // When debugging, check that the LogUp wiring bus balances.
59        // The vtable and chiplets bus final values are non-trivial (they encode public-input-
60        // dependent boundary terms) and are checked by the verifier in reduced_aux_values.
61        let log_up_final_value = wiring_bus.last().copied().unwrap_or(E::ZERO);
62        debug_assert_eq!(log_up_final_value, E::ZERO);
63
64        [t_chip, b_chip, wiring_bus]
65    }
66}
miden_processor/trace/chiplets/aux_trace/mod.rs

miden_processor/trace/chiplets/aux_trace/
mod.rs
