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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140

use crate::{
    interpreters::keccak::interpreter::Interpreter,
    lookups::{Lookup, LookupTableIDs::*},
};
use ark_ff::{One, Zero};
use std::fmt::Debug;

/// This trait contains helper functions for the lookups used in the Keccak circuit
/// using the zkVM lookup tables
pub trait LogupHelpers<F: One + Debug + Zero>
where
    Self: Interpreter<F>,
{
    /// Adds a lookup to the RangeCheck16 table
    fn lookup_rc16(&mut self, flag: Self::Variable, value: Self::Variable) {
        self.add_lookup(flag, Lookup::read_one(RangeCheck16Lookup, vec![value]));
    }

    /// Adds a lookup to the Reset table
    fn lookup_reset(
        &mut self,
        flag: Self::Variable,
        dense: Self::Variable,
        sparse: Self::Variable,
    ) {
        self.add_lookup(flag, Lookup::read_one(ResetLookup, vec![dense, sparse]));
    }

    /// Adds a lookup to the Shift table
    fn lookup_sparse(&mut self, flag: Self::Variable, value: Self::Variable) {
        self.add_lookup(flag, Lookup::read_one(SparseLookup, vec![value]));
    }

    /// Adds a lookup to the Byte table
    fn lookup_byte(&mut self, flag: Self::Variable, value: Self::Variable) {
        self.add_lookup(flag, Lookup::read_one(ByteLookup, vec![value]));
    }

    /// Adds a lookup to the Pad table
    fn lookup_pad(&mut self, flag: Self::Variable, value: Vec<Self::Variable>) {
        self.add_lookup(flag, Lookup::read_one(PadLookup, value));
    }

    /// Adds a lookup to the RoundConstants table
    fn lookup_round_constants(&mut self, flag: Self::Variable, value: Vec<Self::Variable>) {
        self.add_lookup(flag, Lookup::read_one(RoundConstantsLookup, value));
    }

    fn read_syscall(&mut self, flag: Self::Variable, value: Vec<Self::Variable>) {
        self.add_lookup(flag, Lookup::read_one(SyscallLookup, value));
    }

    fn write_syscall(&mut self, flag: Self::Variable, value: Vec<Self::Variable>) {
        self.add_lookup(flag, Lookup::write_one(SyscallLookup, value));
    }
}

/// This trait contains helper functions for boolean operations used in the Keccak circuit
pub trait BoolHelpers<F: One + Debug + Zero>
where
    Self: Interpreter<F>,
{
    /// Degree-2 variable encoding whether the input is a boolean value (0 = yes)
    fn is_boolean(x: Self::Variable) -> Self::Variable {
        x.clone() * (x - Self::Variable::one())
    }

    /// Degree-1 variable encoding the negation of the input
    /// Note: it only works as expected if the input is a boolean value
    fn not(x: Self::Variable) -> Self::Variable {
        Self::Variable::one() - x
    }

    /// Degree-1 variable encoding whether the input is the value one (0 = yes)
    fn is_one(x: Self::Variable) -> Self::Variable {
        Self::not(x)
    }

    /// Degree-2 variable encoding whether the first input is nonzero (0 = yes).
    /// It requires the second input to be the multiplicative inverse of the first.
    /// Note: if the first input is zero, there is no multiplicative inverse.
    fn is_nonzero(x: Self::Variable, x_inv: Self::Variable) -> Self::Variable {
        Self::is_one(x * x_inv)
    }

    // The following two degree-2 constraints define the is_zero function meaning (1 = yes):
    // - if x = 0 then is_zero(x) = 1
    // - if x ≠ 0 then is_zero(x) = 0
    // It is obtained by combining these two equations:
    // x * xinv = 1 - z
    // x * z = 0
    // When x = 0, xinv could be anything, like 1.
    fn is_zero(
        x: Self::Variable,
        x_inv: Self::Variable,
        z: Self::Variable,
    ) -> (Self::Variable, Self::Variable) {
        (
            x.clone() * x_inv.clone() - z.clone() + Self::Variable::one(),
            x * z,
        )
    }

    /// Degree-2 variable encoding the XOR of two variables which should be boolean (1 = true)
    fn xor(x: Self::Variable, y: Self::Variable) -> Self::Variable {
        x.clone() + y.clone() - Self::constant(2) * x * y
    }

    /// Degree-2 variable encoding the OR of two variables, which should be boolean (1 = true)
    fn or(x: Self::Variable, y: Self::Variable) -> Self::Variable {
        x.clone() + y.clone() - x * y
    }

    /// Degree-2 variable encoding whether at least one of the two inputs is zero (0 = yes)
    fn either_zero(x: Self::Variable, y: Self::Variable) -> Self::Variable {
        x * y
    }
}

/// This trait contains helper functions for arithmetic operations used in the Keccak circuit
pub trait ArithHelpers<F: One + Debug + Zero>
where
    Self: Interpreter<F>,
{
    /// Returns a variable representing the value zero
    fn zero() -> Self::Variable {
        Self::constant(0)
    }
    /// Returns a variable representing the value one
    fn one() -> Self::Variable {
        Self::constant(1)
    }
    /// Returns a variable representing the value two
    fn two() -> Self::Variable {
        Self::constant(2)
    }

    /// Returns a variable representing the value 2^x
    fn two_pow(x: u64) -> Self::Variable;
}