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

//! Miden VM Constraints
//!
//! This module contains the constraint functions for the Miden VM processor.
//!
//! ## Organization
//!
//! - **Main trace constraints** are evaluated by [`enforce_main`] and cover system / range / stack
//!   / decoder / chiplets transitions.
//! - **LogUp lookup-argument constraints** are evaluated separately through the closure-based
//!   `LookupAir` impls on [`crate::CoreAir`] and [`crate::ChipletsAir`], wired in from each AIR's
//!   `eval` via [`crate::lookup::ConstraintLookupBuilder`].

use chiplets::selectors::ChipletSelectors;

use crate::{ChipletCols, CoreCols, MidenAirBuilder};

pub mod chiplets;
pub mod columns;
pub mod constants;
pub mod decoder;
pub mod ext_field;
pub mod lookup;
pub(crate) mod op_flags;
pub mod public_inputs;
pub mod range;
pub mod stack;
pub mod system;
pub mod utils;

// ENTRY POINTS
// ================================================================================================
//
// Main trace constraints are partitioned by AIR: `enforce_core` runs the Core half (system,
// range, stack, decoder) and `enforce_chiplets` runs the Chiplets half. The per-AIR
// `LiftedAir` impls (`CoreAir`, `ChipletsAir`) each call only their share.

/// Enforces the Core-trace main constraints: system, range, stack, decoder.
///
/// Public-input boundary constraints ([`public_inputs::enforce_main`]) are owned by Core too
/// but live on a separate entry point because they don't read `next` or `op_flags`.
pub fn enforce_core<AB>(
    builder: &mut AB,
    local: &CoreCols<AB::Var>,
    next: &CoreCols<AB::Var>,
    op_flags: &op_flags::OpFlags<AB::Expr>,
) where
    AB: MidenAirBuilder,
{
    system::enforce_main(builder, local, next, op_flags);
    range::enforce_main(builder, local, next);
    stack::enforce_main(builder, local, next, op_flags);
    decoder::enforce_main(builder, local, next, op_flags);
}

/// Enforces the Chiplets-trace main constraints (hasher permutation/controller, bitwise,
/// memory, ACE). Selector validity is enforced separately via
/// [`chiplets::selectors::build_chiplet_selectors`].
pub fn enforce_chiplets<AB>(
    builder: &mut AB,
    local: &ChipletCols<AB::Var>,
    next: &ChipletCols<AB::Var>,
    selectors: &ChipletSelectors<AB::Expr>,
) where
    AB: MidenAirBuilder,
{
    chiplets::enforce_main(builder, local, next, selectors);
}