o1vm/interpreters/keccak/
helpers.rs

1use crate::{
2    interpreters::keccak::interpreter::Interpreter,
3    lookups::{Lookup, LookupTableIDs::*},
4};
5use ark_ff::{One, Zero};
6use std::fmt::Debug;
7
8/// This trait contains helper functions for the lookups used in the Keccak circuit
9/// using the zkVM lookup tables
10pub trait LogupHelpers<F: One + Debug + Zero>
11where
12    Self: Interpreter<F>,
13{
14    /// Adds a lookup to the RangeCheck16 table
15    fn lookup_rc16(&mut self, flag: Self::Variable, value: Self::Variable) {
16        self.add_lookup(flag, Lookup::read_one(RangeCheck16Lookup, vec![value]));
17    }
18
19    /// Adds a lookup to the Reset table
20    fn lookup_reset(
21        &mut self,
22        flag: Self::Variable,
23        dense: Self::Variable,
24        sparse: Self::Variable,
25    ) {
26        self.add_lookup(flag, Lookup::read_one(ResetLookup, vec![dense, sparse]));
27    }
28
29    /// Adds a lookup to the Shift table
30    fn lookup_sparse(&mut self, flag: Self::Variable, value: Self::Variable) {
31        self.add_lookup(flag, Lookup::read_one(SparseLookup, vec![value]));
32    }
33
34    /// Adds a lookup to the Byte table
35    fn lookup_byte(&mut self, flag: Self::Variable, value: Self::Variable) {
36        self.add_lookup(flag, Lookup::read_one(ByteLookup, vec![value]));
37    }
38
39    /// Adds a lookup to the Pad table
40    fn lookup_pad(&mut self, flag: Self::Variable, value: Vec<Self::Variable>) {
41        self.add_lookup(flag, Lookup::read_one(PadLookup, value));
42    }
43
44    /// Adds a lookup to the RoundConstants table
45    fn lookup_round_constants(&mut self, flag: Self::Variable, value: Vec<Self::Variable>) {
46        self.add_lookup(flag, Lookup::read_one(RoundConstantsLookup, value));
47    }
48
49    fn read_syscall(&mut self, flag: Self::Variable, value: Vec<Self::Variable>) {
50        self.add_lookup(flag, Lookup::read_one(SyscallLookup, value));
51    }
52
53    fn write_syscall(&mut self, flag: Self::Variable, value: Vec<Self::Variable>) {
54        self.add_lookup(flag, Lookup::write_one(SyscallLookup, value));
55    }
56}
57
58/// This trait contains helper functions for boolean operations used in the Keccak circuit
59pub trait BoolHelpers<F: One + Debug + Zero>
60where
61    Self: Interpreter<F>,
62{
63    /// Degree-2 variable encoding whether the input is a boolean value (0 = yes)
64    fn is_boolean(x: Self::Variable) -> Self::Variable {
65        x.clone() * (x - Self::Variable::one())
66    }
67
68    /// Degree-1 variable encoding the negation of the input
69    /// Note: it only works as expected if the input is a boolean value
70    fn not(x: Self::Variable) -> Self::Variable {
71        Self::Variable::one() - x
72    }
73
74    /// Degree-1 variable encoding whether the input is the value one (0 = yes)
75    fn is_one(x: Self::Variable) -> Self::Variable {
76        Self::not(x)
77    }
78
79    /// Degree-2 variable encoding whether the first input is nonzero (0 = yes).
80    /// It requires the second input to be the multiplicative inverse of the first.
81    /// Note: if the first input is zero, there is no multiplicative inverse.
82    fn is_nonzero(x: Self::Variable, x_inv: Self::Variable) -> Self::Variable {
83        Self::is_one(x * x_inv)
84    }
85
86    // The following two degree-2 constraints define the is_zero function meaning (1 = yes):
87    // - if x = 0 then is_zero(x) = 1
88    // - if x ≠ 0 then is_zero(x) = 0
89    // It is obtained by combining these two equations:
90    // x * xinv = 1 - z
91    // x * z = 0
92    // When x = 0, xinv could be anything, like 1.
93    fn is_zero(
94        x: Self::Variable,
95        x_inv: Self::Variable,
96        z: Self::Variable,
97    ) -> (Self::Variable, Self::Variable) {
98        (
99            x.clone() * x_inv.clone() - z.clone() + Self::Variable::one(),
100            x * z,
101        )
102    }
103
104    /// Degree-2 variable encoding the XOR of two variables which should be boolean (1 = true)
105    fn xor(x: Self::Variable, y: Self::Variable) -> Self::Variable {
106        x.clone() + y.clone() - Self::constant(2) * x * y
107    }
108
109    /// Degree-2 variable encoding the OR of two variables, which should be boolean (1 = true)
110    fn or(x: Self::Variable, y: Self::Variable) -> Self::Variable {
111        x.clone() + y.clone() - x * y
112    }
113
114    /// Degree-2 variable encoding whether at least one of the two inputs is zero (0 = yes)
115    fn either_zero(x: Self::Variable, y: Self::Variable) -> Self::Variable {
116        x * y
117    }
118}
119
120/// This trait contains helper functions for arithmetic operations used in the Keccak circuit
121pub trait ArithHelpers<F: One + Debug + Zero>
122where
123    Self: Interpreter<F>,
124{
125    /// Returns a variable representing the value zero
126    fn zero() -> Self::Variable {
127        Self::constant(0)
128    }
129    /// Returns a variable representing the value one
130    fn one() -> Self::Variable {
131        Self::constant(1)
132    }
133    /// Returns a variable representing the value two
134    fn two() -> Self::Variable {
135        Self::constant(2)
136    }
137
138    /// Returns a variable representing the value 2^x
139    fn two_pow(x: u64) -> Self::Variable;
140}
o1vm/interpreters/keccak/helpers.rs

o1vm/interpreters/keccak/
helpers.rs
