miden-air 0.23.0

Algebraic intermediate representation of 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

//! Generic `LookupAir` / `LookupBuilder` lookup-argument module.
//!
//! Holds the field-polymorphic core of the closure-based LogUp machinery: the
//! [`LookupAir`] trait, the [`LookupBuilder`] / [`LookupColumn`] / [`LookupGroup`] /
//! [`LookupBatch`] surface, the [`Challenges`] struct, the [`LookupMessage`] encode trait,
//! the two-path adapters ([`ConstraintLookupBuilder`] for symbolic constraint
//! evaluation, [`ProverLookupBuilder`] for concrete-row fraction collection), the
//! [`LookupFractions`] accumulator, and the [`build_logup_aux_trace`] /
//! [`build_lookup_fractions`] drivers.
//!
//! This module is deliberately free of Miden-specific types so it can be extracted into
//! its own crate without further disentangling. The Miden-side wiring (aggregator AIR,
//! bus message structs, aux-trace builder, bus identifiers) is surfaced separately
//! through [`crate::logup`].

pub mod aux_builder;
pub mod builder;
pub mod challenges;
pub mod constraint;
#[cfg(feature = "std")]
pub mod debug;
pub mod message;
pub mod prover;

pub use aux_builder::{LookupFractions, accumulate, accumulate_slow, build_logup_aux_trace};
pub use builder::{BoundaryBuilder, Deg, LookupBatch, LookupBuilder, LookupColumn, LookupGroup};
pub use challenges::Challenges;
pub use constraint::ConstraintLookupBuilder;
pub use message::LookupMessage;
pub use prover::{ProverLookupBuilder, build_lookup_fractions};

// LOOKUP AIR
// ================================================================================================

/// A declarative LogUp lookup argument.
///
/// Shaped the same way as `p3_air::Air<AB>`: generic over the builder
/// the caller picks, and evaluated once per logical "row pair" (the
/// constraint path visits every row symbolically, the prover path visits
/// every concrete row).
///
/// The trait carries both the static *shape* (column count, payload
/// width bound, bus-id upper bound) and the `eval` method that actually
/// emits the interactions. Adapter constructors take a `&impl
/// LookupAir<Self>` and read the shape via the trait — the `LB` type
/// parameter is pinned to the adapter itself, so there is no
/// ambiguity when the blanket `impl<LB: LookupBuilder> LookupAir<LB>
/// for MyAir` implementations apply.
///
/// ## Contract
///
/// - [`num_columns()`](Self::num_columns) must match the number of `LookupBuilder::next_column`
///   calls issued from [`eval`](Self::eval) — the adapter advances its internal column index each
///   time the closure returns and will panic (or produce undefined constraints) on a mismatch.
/// - [`max_message_width()`](Self::max_message_width) must be ≥ the widest payload any message in
///   the AIR emits. It counts **only** contiguous payload slots — the bus identifier is handled
///   separately through the precomputed bus-prefix table.
/// - [`num_bus_ids()`](Self::num_bus_ids) must be ≥ the largest bus ID any message in the AIR
///   emits, plus one; the adapter precomputes exactly that many bus prefixes and indexes into the
///   table with `bus_id as usize`.
pub trait LookupAir<LB: LookupBuilder> {
    /// Number of permutation columns this argument occupies.
    fn num_columns(&self) -> usize;

    /// Per-column upper bound on the number of fractions a single row can push.
    ///
    /// Length must equal [`num_columns()`](Self::num_columns). Each entry is the
    /// **mutual-exclusion-aware** max — i.e. the largest active branch count taken across
    /// all mutually exclusive groups inside the column, not the sum of every structural
    /// `add` / `remove` / `insert` / `batch` push site.
    ///
    /// The prover-path adapter uses this to size the dense per-column fraction buffer
    /// (`Vec::with_capacity`) so the hot row loop never re-allocates.
    fn column_shape(&self) -> &[usize];

    /// Upper bound on the **payload** width of any message emitted by
    /// [`eval`](Self::eval), exclusive of the bus identifier slot.
    fn max_message_width(&self) -> usize;

    /// Upper bound on any bus ID this AIR emits through
    /// [`LookupMessage::encode`],
    /// plus one. The adapter pre-computes that many bus prefixes at
    /// construction time and indexes into the table with
    /// `bus_id as usize`.
    fn num_bus_ids(&self) -> usize;

    /// Evaluate the lookup argument, describing its interactions through
    /// the builder's closure API.
    fn eval(&self, builder: &mut LB);

    /// Emit boundary / "outer" interactions — once-per-proof contributions that don't
    /// come from any main-trace row.
    ///
    /// Typical sources are committed-final terminals and public-input-driven seed
    /// emissions (kernel ROM init, block hash seed, log-precompile terminals).
    /// These close out buses whose per-row [`eval`](Self::eval) contributions alone
    /// don't cancel.
    ///
    /// Consumed today only by the real-trace debug walker in
    /// [`crate::lookup::debug::trace`], which combines per-row and boundary emissions
    /// into a single balance check. The constraint and prover paths don't call this
    /// method yet — boundary terms still flow through `when_first_row` / `when_last_row`
    /// flag selectors inside [`eval`](Self::eval) until they are refactored to read
    /// from here too.
    ///
    /// Default is a no-op so AIRs with no boundary contributions don't need to
    /// override it.
    fn eval_boundary<B>(&self, _boundary: &mut B)
    where
        B: BoundaryBuilder<F = LB::F, EF = LB::EF>,
    {
    }
}