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

//! General stack transition constraints.
//!
//! This module contains the general constraints that enforce how stack items transition
//! based on the operation type (no shift, left shift, right shift).
//!
//! ## Stack Transition Model
//!
//! The stack has 16 visible positions (0-15). For each operation, stack items can:
//! - **Stay in place** (no shift): item stays at same position
//! - **Shift left**: item moves to position i from position i+1
//! - **Shift right**: item moves to position i from position i-1
//!
//! ## Constraints
//!
//! 1. **Position 0**: Can receive from position 0 (no shift) or position 1 (left shift). Right
//!    shift doesn't apply - position 0 gets a new value pushed.
//!
//! 2. **Positions 1-14**: Can receive from position i (no shift), i+1 (left shift), or i-1 (right
//!    shift).
//!
//! 3. **Position 15**: Can receive from position 15 (no shift) or position 14 (right shift). Left
//!    shift at position 15 is handled by overflow constraints (zeroing).
//!
//! 4. **Top binary**: Enforced by the specific op constraints that require it.

use miden_crypto::stark::air::AirBuilder;

use crate::{MainCols, MidenAirBuilder, constraints::op_flags::OpFlags};

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

/// Enforces all general stack transition constraints.
///
/// This includes:
/// - 16 constraints for stack item transitions at each position
pub fn enforce_main<AB>(
    builder: &mut AB,
    local: &MainCols<AB::Var>,
    next: &MainCols<AB::Var>,
    op_flags: &OpFlags<AB::Expr>,
) where
    AB: MidenAirBuilder,
{
    // For each position i, the constraint ensures that the next value is consistent
    // with the current value based on the shift flags:
    //
    // next[i] * flag_sum = no_shift[i] * current[i]
    //                    + left_shift[i+1] * current[i+1]
    //                    + right_shift[i-1] * current[i-1]
    //
    // where flag_sum is the sum of applicable flags for that position.

    // Position 0: no right shift (new value pushed instead)
    // next[0] * flag_sum = no_shift[0] * current[0] + left_shift[1] * current[1]
    {
        let flag_sum = op_flags.no_shift_at(0) + op_flags.left_shift_at(1);
        let expected = op_flags.no_shift_at(0) * local.stack.get(0).into()
            + op_flags.left_shift_at(1) * local.stack.get(1).into();
        let actual = next.stack.get(0);

        builder.when_transition().assert_zero(actual * flag_sum - expected);
    }

    // Positions 1-14: all three shift types possible.
    for i in 1..15 {
        let flag_sum = op_flags.no_shift_at(i)
            + op_flags.left_shift_at(i + 1)
            + op_flags.right_shift_at(i - 1);

        let expected = op_flags.no_shift_at(i) * local.stack.get(i).into()
            + op_flags.left_shift_at(i + 1) * local.stack.get(i + 1).into()
            + op_flags.right_shift_at(i - 1) * local.stack.get(i - 1).into();
        let actual = next.stack.get(i);

        builder.when_transition().assert_zero(actual * flag_sum - expected);
    }

    // Position 15: no left shift (handled by overflow constraints)
    // next[15] * flag_sum = no_shift[15] * current[15] + right_shift[14] * current[14]
    {
        let flag_sum = op_flags.no_shift_at(15) + op_flags.right_shift_at(14);
        let expected = op_flags.no_shift_at(15) * local.stack.get(15).into()
            + op_flags.right_shift_at(14) * local.stack.get(14).into();
        let actual = next.stack.get(15);

        builder.when_transition().assert_zero(actual * flag_sum - expected);
    }
}