miden-air 0.25.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

//! Generic traits and adapters for LogUp lookup arguments.
//!
//! This module contains the generic lookup contract ([`LookupAir`]), the builder API,
//! message encoding, challenge precomputation, constraint and prover adapters, and
//! aux-trace accumulation helpers.

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: 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.
    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 once-per-proof boundary interactions 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.
    ///
    /// 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>,
    {
    }
}