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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
//! Instantiation of the lookups for the VM project.

use self::LookupTableIDs::*;
use crate::{keccak::pad_blocks, ramlookup::RAMLookup};
use ark_ff::{Field, PrimeField};
use kimchi::{
    circuits::polynomials::keccak::{
        constants::{RATE_IN_BYTES, ROUNDS},
        Keccak, RC,
    },
    o1_utils::{FieldHelpers, Two},
};
use kimchi_msm::{LogupTable, LogupWitness, LookupTableID};

/// The lookups struct based on RAMLookups for the VM table IDs
pub(crate) type Lookup<F> = RAMLookup<F, LookupTableIDs>;

#[allow(dead_code)]
/// Represents a witness of one instance of the lookup argument of the zkVM project
pub(crate) type LookupWitness<F> = LogupWitness<F, LookupTableIDs>;

/// The lookup table struct based on LogupTable for the VM table IDs
pub(crate) type LookupTable<F> = LogupTable<F, LookupTableIDs>;

/// All of the possible lookup table IDs used in the zkVM
#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)]
pub enum LookupTableIDs {
    // PadLookup ID is 0 because this is the only fixed table whose first entry is not 0.
    // This way, it is guaranteed that the 0 value is not always in the tables after the
    // randomization with the joint combiner is applied.
    /// All [1..136] values of possible padding lengths, the value 2^len, and the 5 corresponding pad suffixes with the 10*1 rule
    PadLookup = 0,
    /// 24-row table with all possible values for round and their round constant in expanded form (in big endian) [0..=23]
    RoundConstantsLookup = 1,
    /// Values from 0 to 4 to check the number of bytes read from syscalls
    AtMost4Lookup = 2,
    /// All values that can be stored in a byte (amortized table, better than model as RangeCheck16 (x and scaled x)
    ByteLookup = 3,
    // Read tables come first to allow indexing with the table ID for the multiplicities
    /// Single-column table of all values in the range [0, 2^16)
    RangeCheck16Lookup = 4,
    /// Single-column table of 2^16 entries with the sparse representation of all values
    SparseLookup = 5,
    /// Dual-column table of all values in the range [0, 2^16) and their sparse representation
    ResetLookup = 6,

    // RAM Tables
    MemoryLookup = 7,
    RegisterLookup = 8,
    /// Syscalls communication channel
    SyscallLookup = 9,
    /// Input/Output of Keccak steps
    KeccakStepLookup = 10,
}

impl LookupTableID for LookupTableIDs {
    fn to_u32(&self) -> u32 {
        *self as u32
    }

    fn from_u32(value: u32) -> Self {
        match value {
            0 => PadLookup,
            1 => RoundConstantsLookup,
            2 => ByteLookup,
            3 => RangeCheck16Lookup,
            4 => SparseLookup,
            5 => ResetLookup,
            6 => MemoryLookup,
            7 => RegisterLookup,
            8 => SyscallLookup,
            9 => KeccakStepLookup,
            _ => panic!("Invalid table ID"),
        }
    }

    fn length(&self) -> usize {
        match self {
            PadLookup => RATE_IN_BYTES,
            RoundConstantsLookup => ROUNDS,
            AtMost4Lookup => 5,
            ByteLookup => 1 << 8,
            RangeCheck16Lookup | SparseLookup | ResetLookup => 1 << 16,
            MemoryLookup | RegisterLookup | SyscallLookup | KeccakStepLookup => {
                panic!("RAM Tables do not have a fixed length")
            }
        }
    }

    fn is_fixed(&self) -> bool {
        match self {
            PadLookup | RoundConstantsLookup | AtMost4Lookup | ByteLookup | RangeCheck16Lookup
            | SparseLookup | ResetLookup => true,
            MemoryLookup | RegisterLookup | SyscallLookup | KeccakStepLookup => false,
        }
    }

    fn runtime_create_column(&self) -> bool {
        panic!("No runtime tables specified");
    }

    fn ix_by_value<F: PrimeField>(&self, _value: &[F]) -> Option<usize> {
        todo!()
    }

    fn all_variants() -> Vec<Self> {
        vec![
            Self::PadLookup,
            Self::RoundConstantsLookup,
            Self::AtMost4Lookup,
            Self::ByteLookup,
            Self::RangeCheck16Lookup,
            Self::SparseLookup,
            Self::ResetLookup,
            Self::MemoryLookup,
            Self::RegisterLookup,
            Self::SyscallLookup,
            Self::KeccakStepLookup,
        ]
    }
}

/// Trait that creates all the fixed lookup tables used in the VM
pub(crate) trait FixedLookupTables<F> {
    /// Checks whether a value is in a table and returns the position if it is or None otherwise.
    fn is_in_table(table: &LookupTable<F>, value: Vec<F>) -> Option<usize>;
    /// Returns the pad table
    fn table_pad() -> LookupTable<F>;
    /// Returns the round constants table
    fn table_round_constants() -> LookupTable<F>;
    /// Returns the at most 4 table
    fn table_at_most_4() -> LookupTable<F>;
    /// Returns the byte table
    fn table_byte() -> LookupTable<F>;
    /// Returns the range check 16 table
    fn table_range_check_16() -> LookupTable<F>;
    /// Returns the sparse table
    fn table_sparse() -> LookupTable<F>;
    /// Returns the reset table
    fn table_reset() -> LookupTable<F>;
}

impl<F: Field> FixedLookupTables<F> for LookupTable<F> {
    fn is_in_table(table: &LookupTable<F>, value: Vec<F>) -> Option<usize> {
        let id = table.table_id;
        // In these tables, the first value of the vector is related to the index within the table.
        let idx = value[0]
            .to_bytes()
            .iter()
            .rev()
            .fold(0u64, |acc, &x| acc * 256 + x as u64) as usize;

        match id {
            RoundConstantsLookup | AtMost4Lookup | ByteLookup | RangeCheck16Lookup
            | ResetLookup => {
                if idx < id.length() && table.entries[idx] == value {
                    Some(idx)
                } else {
                    None
                }
            }
            PadLookup => {
                // Because this table starts with entry 1
                if idx - 1 < id.length() && table.entries[idx - 1] == value {
                    Some(idx - 1)
                } else {
                    None
                }
            }
            SparseLookup => {
                let res = u64::from_str_radix(&format!("{:x}", idx), 2);
                let dense = if let Ok(ok) = res {
                    ok as usize
                } else {
                    id.length() // So that it returns None
                };
                if dense < id.length() && table.entries[dense] == value {
                    Some(dense)
                } else {
                    None
                }
            }
            MemoryLookup | RegisterLookup | SyscallLookup | KeccakStepLookup => None,
        }
    }

    fn table_pad() -> Self {
        Self {
            table_id: PadLookup,
            entries: (1..=PadLookup.length())
                .map(|i| {
                    let suffix = pad_blocks(i);
                    vec![
                        F::from(i as u64),
                        F::two_pow(i as u64),
                        suffix[0],
                        suffix[1],
                        suffix[2],
                        suffix[3],
                        suffix[4],
                    ]
                })
                .collect(),
        }
    }

    fn table_round_constants() -> Self {
        Self {
            table_id: RoundConstantsLookup,
            entries: (0..RoundConstantsLookup.length())
                .map(|i| {
                    vec![
                        F::from(i as u32),
                        F::from(Keccak::sparse(RC[i])[3]),
                        F::from(Keccak::sparse(RC[i])[2]),
                        F::from(Keccak::sparse(RC[i])[1]),
                        F::from(Keccak::sparse(RC[i])[0]),
                    ]
                })
                .collect(),
        }
    }

    fn table_at_most_4() -> LookupTable<F> {
        Self {
            table_id: AtMost4Lookup,
            entries: (0..AtMost4Lookup.length())
                .map(|i| vec![F::from(i as u32)])
                .collect(),
        }
    }

    fn table_byte() -> Self {
        Self {
            table_id: ByteLookup,
            entries: (0..ByteLookup.length())
                .map(|i| vec![F::from(i as u32)])
                .collect(),
        }
    }

    fn table_range_check_16() -> Self {
        Self {
            table_id: RangeCheck16Lookup,
            entries: (0..RangeCheck16Lookup.length())
                .map(|i| vec![F::from(i as u32)])
                .collect(),
        }
    }

    fn table_sparse() -> Self {
        Self {
            table_id: SparseLookup,
            entries: (0..SparseLookup.length())
                .map(|i| {
                    vec![F::from(
                        u64::from_str_radix(&format!("{:b}", i), 16).unwrap(),
                    )]
                })
                .collect(),
        }
    }

    fn table_reset() -> Self {
        Self {
            table_id: ResetLookup,
            entries: (0..ResetLookup.length())
                .map(|i| {
                    vec![
                        F::from(i as u32),
                        F::from(u64::from_str_radix(&format!("{:b}", i), 16).unwrap()),
                    ]
                })
                .collect(),
        }
    }
}