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

//! Chiplets constraints module.
//!
//! Currently we implement:
//! - chiplet selector constraints (including hasher internal selectors)
//! - permutation sub-chiplet main-trace constraints
//! - controller sub-chiplet main-trace constraints
//! - bitwise chiplet main-trace constraints
//! - memory chiplet main-trace constraints
//! - ACE chiplet main-trace constraints
//!
//! Chiplet LogUp lookup-argument constraints are emitted by
//! [`crate::constraints::lookup::chiplet_air::emit_chiplet_lookup_columns`] and wired
//! through [`crate::ChipletsAir`]'s `LookupAir` impl from `ChipletsAir::eval`.

pub mod ace;
pub mod bitwise;
pub mod columns;
pub mod hasher_control;
pub mod memory;
pub mod permutation;
pub mod selectors;

use miden_core::field::PrimeCharacteristicRing;
use miden_crypto::stark::air::AirBuilder;
use selectors::ChipletSelectors;

use crate::{ChipletCols, MidenAirBuilder};

// ENTRY POINTS
// ================================================================================================

/// Enforces chiplets main-trace constraints.
pub fn enforce_main<AB>(
    builder: &mut AB,
    local: &ChipletCols<AB::Var>,
    next: &ChipletCols<AB::Var>,
    selectors: &ChipletSelectors<AB::Expr>,
) where
    AB: MidenAirBuilder,
{
    // Selector constraints (including hasher internal selectors) are enforced in
    // build_chiplet_selectors (called from lib.rs).

    // Chiplet-trace row counter `chip_clk`: starts at 1 and increments by 1 each row.
    builder.when_first_row().assert_eq(local.chip_clk, AB::Expr::ONE);
    builder
        .when_transition()
        .assert_eq(next.chip_clk.into(), local.chip_clk.into() + AB::Expr::ONE);

    // Hasher sub-chiplets: permutation + controller.
    permutation::enforce_permutation_constraints(builder, local, next, &selectors.permutation);
    hasher_control::enforce_controller_constraints(builder, local, next, &selectors.controller);

    bitwise::enforce_bitwise_constraints(builder, local, next, &selectors.bitwise);
    memory::enforce_memory_constraints(builder, local, next, &selectors.memory);
    ace::enforce_ace_constraints_all_rows(builder, local, next, &selectors.ace);
}