o1vm/interpreters/keccak/
constraints.rs

1//! This module contains the constraints for one Keccak step.
2use crate::{
3    interpreters::keccak::{
4        helpers::{ArithHelpers, BoolHelpers, LogupHelpers},
5        interpreter::{Interpreter, KeccakInterpreter},
6        Constraint, KeccakColumn,
7    },
8    lookups::Lookup,
9    E,
10};
11use ark_ff::{Field, One};
12use kimchi::{
13    circuits::{
14        expr::{ConstantTerm::Literal, Expr, ExprInner, Operations, Variable},
15        gate::CurrOrNext,
16    },
17    o1_utils::Two,
18};
19use kimchi_msm::columns::ColumnIndexer;
20
21/// This struct contains all that needs to be kept track of during the execution of the Keccak step interpreter
22#[derive(Clone, Debug)]
23pub struct Env<Fp> {
24    /// Constraints that are added to the circuit
25    pub constraints: Vec<E<Fp>>,
26    /// Variables that are looked up in the circuit
27    pub lookups: Vec<Lookup<E<Fp>>>,
28}
29
30impl<F: Field> Default for Env<F> {
31    fn default() -> Self {
32        Self {
33            constraints: Vec::new(),
34            lookups: Vec::new(),
35        }
36    }
37}
38
39impl<F: Field> ArithHelpers<F> for Env<F> {
40    fn two_pow(x: u64) -> Self::Variable {
41        Self::constant_field(F::two_pow(x))
42    }
43}
44
45impl<F: Field> BoolHelpers<F> for Env<F> {}
46
47impl<F: Field> LogupHelpers<F> for Env<F> {}
48
49impl<F: Field> Interpreter<F> for Env<F> {
50    type Variable = E<F>;
51
52    fn constant(x: u64) -> Self::Variable {
53        Self::constant_field(F::from(x))
54    }
55
56    fn constant_field(x: F) -> Self::Variable {
57        Self::Variable::constant(Operations::from(Literal(x)))
58    }
59
60    fn variable(&self, column: KeccakColumn) -> Self::Variable {
61        // Despite `KeccakWitness` containing both `curr` and `next` fields,
62        // the Keccak step spans across one row only.
63        Expr::Atom(ExprInner::Cell(Variable {
64            col: column.to_column(),
65            row: CurrOrNext::Curr,
66        }))
67    }
68
69    fn constrain(&mut self, _tag: Constraint, if_true: Self::Variable, x: Self::Variable) {
70        if if_true == Self::Variable::one() {
71            self.constraints.push(x);
72        }
73    }
74
75    fn add_lookup(&mut self, if_true: Self::Variable, lookup: Lookup<Self::Variable>) {
76        if if_true == Self::Variable::one() {
77            self.lookups.push(lookup);
78        }
79    }
80}
81
82impl<F: Field> KeccakInterpreter<F> for Env<F> {}
o1vm/interpreters/keccak/constraints.rs

o1vm/interpreters/keccak/
constraints.rs
