sp1_core_machine/air/
operation.rs

1use std::ops::{Add, Mul, MulAssign, Sub};
2
3use slop_air::AirBuilder;
4use slop_algebra::{AbstractField, ExtensionField, Field};
5use slop_uni_stark::SymbolicAirBuilder;
6use sp1_hypercube::{
7    air::SP1AirBuilder, ConstraintSumcheckFolder, DebugConstraintBuilder,
8    GenericVerifierConstraintFolder, InteractionBuilder,
9};
10
11use crate::{
12    adapter::{
13        register::{
14            alu_type::ALUTypeReader,
15            i_type::{ITypeReader, ITypeReaderImmutable},
16            j_type::JTypeReader,
17            r_type::{RTypeReader, RTypeReaderImmutable},
18        },
19        state::CPUState,
20    },
21    operations::{
22        AddOperation, AddrAddOperation, AddressOperation, AddwOperation, BitwiseOperation,
23        BitwiseU16Operation, IsEqualWordOperation, IsZeroOperation, IsZeroWordOperation,
24        LtOperationSigned, LtOperationUnsigned, MulOperation, SubOperation, SubwOperation,
25        U16CompareOperation, U16MSBOperation, U16toU8OperationSafe, U16toU8OperationUnsafe,
26    },
27};
28
29type F<AB> = <AB as AirBuilder>::F;
30
31pub trait SP1CoreOperationBuilder:
32    SP1AirBuilder
33    + SP1OperationBuilder<AddOperation<F<Self>>>
34    + SP1OperationBuilder<U16toU8OperationSafe>
35    + SP1OperationBuilder<U16toU8OperationUnsafe>
36    + SP1OperationBuilder<IsZeroOperation<F<Self>>>
37    + SP1OperationBuilder<IsZeroWordOperation<F<Self>>>
38    + SP1OperationBuilder<IsEqualWordOperation<F<Self>>>
39    + SP1OperationBuilder<BitwiseOperation<F<Self>>>
40    + SP1OperationBuilder<BitwiseU16Operation<F<Self>>>
41    + SP1OperationBuilder<RTypeReader<F<Self>>>
42    + SP1OperationBuilder<CPUState<F<Self>>>
43    + SP1OperationBuilder<RTypeReaderImmutable>
44    + SP1OperationBuilder<ALUTypeReader<F<Self>>>
45    + SP1OperationBuilder<CPUState<F<Self>>>
46    + SP1OperationBuilder<SubOperation<F<Self>>>
47    + SP1OperationBuilder<U16CompareOperation<F<Self>>>
48    + SP1OperationBuilder<U16MSBOperation<F<Self>>>
49    + SP1OperationBuilder<LtOperationUnsigned<F<Self>>>
50    + SP1OperationBuilder<LtOperationSigned<F<Self>>>
51    + SP1OperationBuilder<CPUState<F<Self>>>
52    + SP1OperationBuilder<MulOperation<F<Self>>>
53    + SP1OperationBuilder<ITypeReader<F<Self>>>
54    + SP1OperationBuilder<AddwOperation<F<Self>>>
55    + SP1OperationBuilder<SubwOperation<F<Self>>>
56    + SP1OperationBuilder<JTypeReader<F<Self>>>
57    + SP1OperationBuilder<ITypeReaderImmutable>
58    + SP1OperationBuilder<AddrAddOperation<F<Self>>>
59    + SP1OperationBuilder<AddressOperation<F<Self>>>
60{
61}
62
63impl<AB> SP1CoreOperationBuilder for AB where
64    AB: SP1AirBuilder
65        + SP1OperationBuilder<AddOperation<F<Self>>>
66        + SP1OperationBuilder<U16toU8OperationSafe>
67        + SP1OperationBuilder<U16toU8OperationUnsafe>
68        + SP1OperationBuilder<IsZeroOperation<F<Self>>>
69        + SP1OperationBuilder<IsZeroWordOperation<F<Self>>>
70        + SP1OperationBuilder<IsEqualWordOperation<F<Self>>>
71        + SP1OperationBuilder<BitwiseOperation<F<Self>>>
72        + SP1OperationBuilder<BitwiseU16Operation<F<Self>>>
73        + SP1OperationBuilder<RTypeReaderImmutable>
74        + SP1OperationBuilder<ALUTypeReader<F<Self>>>
75        + SP1OperationBuilder<RTypeReader<F<Self>>>
76        + SP1OperationBuilder<CPUState<F<Self>>>
77        + SP1OperationBuilder<SubOperation<F<Self>>>
78        + SP1OperationBuilder<U16CompareOperation<F<Self>>>
79        + SP1OperationBuilder<U16MSBOperation<F<Self>>>
80        + SP1OperationBuilder<LtOperationUnsigned<F<Self>>>
81        + SP1OperationBuilder<LtOperationSigned<F<Self>>>
82        + SP1OperationBuilder<MulOperation<F<Self>>>
83        + SP1OperationBuilder<ITypeReader<F<Self>>>
84        + SP1OperationBuilder<AddwOperation<F<Self>>>
85        + SP1OperationBuilder<SubwOperation<F<Self>>>
86        + SP1OperationBuilder<JTypeReader<F<Self>>>
87        + SP1OperationBuilder<ITypeReaderImmutable>
88        + SP1OperationBuilder<AddrAddOperation<F<Self>>>
89        + SP1OperationBuilder<AddressOperation<F<Self>>>
90{
91}
92
93/// A trait for operations that can be lowered to constraints in an AIR.
94pub trait SP1Operation<AB: SP1AirBuilder> {
95    /// The input arguments to the operation.
96    type Input;
97
98    /// The output of the operation.
99    type Output;
100
101    /// The underlying constraints corresponding to the operation.
102    fn lower(builder: &mut AB, input: Self::Input) -> Self::Output;
103
104    /// Evaluate the operation on the given inputs.
105    fn eval(builder: &mut AB, input: Self::Input) -> Self::Output
106    where
107        Self: Sized,
108        AB: SP1OperationBuilder<Self>,
109    {
110        builder.eval_operation(input)
111    }
112}
113
114/// A trait for handling an SP1 operation.
115///
116/// This trait enables an AIR builder to evaluate an operation in a specific way, such as emitting
117/// code or changing state while keeping the semantic meaning of the operation being separated from
118/// arbitrary constraints.
119pub trait SP1OperationBuilder<O: SP1Operation<Self>>: SP1AirBuilder {
120    fn eval_operation(&mut self, input: O::Input) -> O::Output;
121}
122
123/// A trait for demarking a builder that lowers every operation to it's underlying constraints.
124pub trait TrivialOperationBuilder: SP1AirBuilder {}
125
126impl<AB: TrivialOperationBuilder, O: SP1Operation<AB>> SP1OperationBuilder<O> for AB {
127    fn eval_operation(&mut self, input: O::Input) -> O::Output {
128        O::lower(self, input)
129    }
130}
131
132impl<F: Field> TrivialOperationBuilder for InteractionBuilder<F> {}
133
134impl<F: Field> TrivialOperationBuilder for SymbolicAirBuilder<F> {}
135
136impl<F: Field, EF: ExtensionField<F>> TrivialOperationBuilder
137    for DebugConstraintBuilder<'_, F, EF>
138{
139}
140
141impl<
142        'a,
143        F: Field,
144        K: Field + From<F> + Add<F, Output = K> + Sub<F, Output = K> + Mul<F, Output = K>,
145        EF: Field + Mul<K, Output = EF>,
146    > TrivialOperationBuilder for ConstraintSumcheckFolder<'a, F, K, EF>
147{
148}
149
150impl<'a, F, EF, PubVar, Var, Expr> TrivialOperationBuilder
151    for GenericVerifierConstraintFolder<'a, F, EF, PubVar, Var, Expr>
152where
153    F: Field,
154    EF: ExtensionField<F>,
155    Expr: AbstractField<F = EF>
156        + From<F>
157        + Add<Var, Output = Expr>
158        + Add<F, Output = Expr>
159        + Sub<Var, Output = Expr>
160        + Sub<F, Output = Expr>
161        + Mul<Var, Output = Expr>
162        + Mul<F, Output = Expr>
163        + MulAssign<EF>,
164    Var: Into<Expr>
165        + Copy
166        + Add<F, Output = Expr>
167        + Add<Var, Output = Expr>
168        + Add<Expr, Output = Expr>
169        + Sub<F, Output = Expr>
170        + Sub<Var, Output = Expr>
171        + Sub<Expr, Output = Expr>
172        + Mul<F, Output = Expr>
173        + Mul<Var, Output = Expr>
174        + Mul<Expr, Output = Expr>
175        + Send
176        + Sync,
177    PubVar: Into<Expr> + Copy,
178{
179}
sp1_core_machine/air/operation.rs

sp1_core_machine/air/
operation.rs
