triton_air/
lib.rs

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
use constraint_circuit::ConstraintCircuitBuilder;
use constraint_circuit::ConstraintCircuitMonad;
use constraint_circuit::DualRowIndicator;
use constraint_circuit::SingleRowIndicator;
use strum::EnumCount;

use crate::table_column::MasterAuxColumn;
use crate::table_column::MasterMainColumn;

pub mod challenge_id;
pub mod cross_table_argument;
pub mod table;
pub mod table_column;

mod private {
    pub trait Seal {}
}

/// The degree of the AIR after the degree lowering step.
///
/// Using substitution and the introduction of new variables, the degree of the AIR as specified
/// in the respective tables
/// (e.g., in [`table::processor::ProcessorTable::transition_constraints`])
/// is lowered to this value.
/// For example, with a target degree of 2 and a (fictional) constraint of the form
/// `a = b²·c²·d`,
/// the degree lowering step could (as one among multiple possibilities)
/// - introduce new variables `e`, `f`, and `g`,
/// - introduce new constraints `e = b²`, `f = c²`, and `g = e·f`,
/// - replace the original constraint with `a = g·d`.
///
/// The degree lowering happens in Triton VM's build script, `build.rs`.
pub const TARGET_DEGREE: isize = 4;

/// The main trait for the [tables]' Arithmetic Intermediate Representation.
///
/// This is a _sealed_ trait. It is not intended (or possible) to implement this
/// trait outside the crate defining it.
///
/// [tables]: table::TableId
///
/// ### Object safety
///
/// This trait is _not_ object safe.
pub trait AIR: private::Seal {
    type MainColumn: MasterMainColumn + EnumCount;
    type AuxColumn: MasterAuxColumn + EnumCount;

    fn initial_constraints(
        circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>>;

    fn consistency_constraints(
        circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>>;

    fn transition_constraints(
        circuit_builder: &ConstraintCircuitBuilder<DualRowIndicator>,
    ) -> Vec<ConstraintCircuitMonad<DualRowIndicator>>;

    fn terminal_constraints(
        circuit_builder: &ConstraintCircuitBuilder<SingleRowIndicator>,
    ) -> Vec<ConstraintCircuitMonad<SingleRowIndicator>>;
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn public_types_implement_usual_auto_traits() {
        fn implements_auto_traits<T: Sized + Send + Sync + Unpin>() {}

        implements_auto_traits::<challenge_id::ChallengeId>();
        implements_auto_traits::<cross_table_argument::PermArg>();
        implements_auto_traits::<cross_table_argument::EvalArg>();
        implements_auto_traits::<cross_table_argument::LookupArg>();
        implements_auto_traits::<cross_table_argument::GrandCrossTableArg>();
        implements_auto_traits::<table_column::ProgramMainColumn>();
        implements_auto_traits::<table_column::ProgramAuxColumn>();
        implements_auto_traits::<table_column::ProcessorMainColumn>();
        implements_auto_traits::<table_column::ProcessorAuxColumn>();
        implements_auto_traits::<table_column::OpStackMainColumn>();
        implements_auto_traits::<table_column::OpStackAuxColumn>();
        implements_auto_traits::<table_column::RamMainColumn>();
        implements_auto_traits::<table_column::RamAuxColumn>();
        implements_auto_traits::<table_column::JumpStackMainColumn>();
        implements_auto_traits::<table_column::JumpStackAuxColumn>();
        implements_auto_traits::<table_column::HashMainColumn>();
        implements_auto_traits::<table_column::HashAuxColumn>();
        implements_auto_traits::<table_column::CascadeMainColumn>();
        implements_auto_traits::<table_column::CascadeAuxColumn>();
        implements_auto_traits::<table_column::LookupMainColumn>();
        implements_auto_traits::<table_column::LookupAuxColumn>();
        implements_auto_traits::<table_column::U32MainColumn>();
        implements_auto_traits::<table_column::U32AuxColumn>();

        implements_auto_traits::<table::TableId>();
        implements_auto_traits::<table::cascade::CascadeTable>();
        implements_auto_traits::<table::hash::HashTable>();
        implements_auto_traits::<table::hash::HashTableMode>();
        implements_auto_traits::<table::hash::PermutationTrace>();
        implements_auto_traits::<table::jump_stack::JumpStackTable>();
        implements_auto_traits::<table::lookup::LookupTable>();
        implements_auto_traits::<table::op_stack::OpStackTable>();
        implements_auto_traits::<table::processor::ProcessorTable>();
        implements_auto_traits::<table::program::ProgramTable>();
        implements_auto_traits::<table::ram::RamTable>();
        implements_auto_traits::<table::u32::U32Table>();
    }
}