o1vm/
lookups.rs

1//! Instantiation of the lookups for the VM project.
2
3use self::LookupTableIDs::*;
4use crate::{interpreters::keccak::pad_blocks, ramlookup::RAMLookup};
5use ark_ff::{Field, PrimeField};
6use kimchi::{
7    circuits::polynomials::keccak::{
8        constants::{RATE_IN_BYTES, ROUNDS},
9        Keccak, RC,
10    },
11    o1_utils::{FieldHelpers, Two},
12};
13use kimchi_msm::{LogupTable, LogupWitness, LookupTableID};
14
15/// The lookups struct based on RAMLookups for the VM table IDs
16pub(crate) type Lookup<F> = RAMLookup<F, LookupTableIDs>;
17
18#[allow(dead_code)]
19/// Represents a witness of one instance of the lookup argument of the zkVM project
20pub(crate) type LookupWitness<F> = LogupWitness<F, LookupTableIDs>;
21
22/// The lookup table struct based on LogupTable for the VM table IDs
23pub(crate) type LookupTable<F> = LogupTable<F, LookupTableIDs>;
24
25/// All of the possible lookup table IDs used in the zkVM
26#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)]
27pub enum LookupTableIDs {
28    // PadLookup ID is 0 because this is the only fixed table whose first entry
29    // is not 0. This way, it is guaranteed that the 0 value is not always in
30    // the tables after the randomization with the joint combiner is applied.
31    /// All [1..136] values of possible padding lengths, the value 2^len, and
32    /// the 5 corresponding pad suffixes with the 10*1 rule
33    PadLookup = 0,
34    /// 24-row table with all possible values for round and their round constant
35    /// in expanded form (in big endian) [0..=23]
36    RoundConstantsLookup = 1,
37    /// Values from 0 to 4 to check the number of bytes read from syscalls
38    AtMost4Lookup = 2,
39    /// All values that can be stored in a byte (amortized table, better than
40    /// model as RangeCheck16 (x and scaled x)
41    ByteLookup = 3,
42    // Read tables come first to allow indexing with the table ID for the
43    // multiplicities
44    /// Single-column table of all values in the range [0, 2^16)
45    RangeCheck16Lookup = 4,
46    /// Single-column table of 2^16 entries with the sparse representation of
47    /// all values
48    SparseLookup = 5,
49    /// Dual-column table of all values in the range [0, 2^16) and their sparse
50    /// representation
51    ResetLookup = 6,
52
53    // RAM Tables
54    MemoryLookup = 7,
55    RegisterLookup = 8,
56    /// Syscalls communication channel
57    SyscallLookup = 9,
58    /// Input/Output of Keccak steps
59    KeccakStepLookup = 10,
60}
61
62impl LookupTableID for LookupTableIDs {
63    fn to_u32(&self) -> u32 {
64        *self as u32
65    }
66
67    fn from_u32(value: u32) -> Self {
68        match value {
69            0 => PadLookup,
70            1 => RoundConstantsLookup,
71            2 => AtMost4Lookup,
72            3 => ByteLookup,
73            4 => RangeCheck16Lookup,
74            5 => SparseLookup,
75            6 => ResetLookup,
76            7 => MemoryLookup,
77            8 => RegisterLookup,
78            9 => SyscallLookup,
79            10 => KeccakStepLookup,
80            _ => panic!("Invalid table ID"),
81        }
82    }
83
84    fn length(&self) -> usize {
85        match self {
86            PadLookup => RATE_IN_BYTES,
87            RoundConstantsLookup => ROUNDS,
88            AtMost4Lookup => 5,
89            ByteLookup => 1 << 8,
90            RangeCheck16Lookup | SparseLookup | ResetLookup => 1 << 16,
91            MemoryLookup | RegisterLookup | SyscallLookup | KeccakStepLookup => {
92                panic!("RAM Tables do not have a fixed length")
93            }
94        }
95    }
96
97    fn is_fixed(&self) -> bool {
98        match self {
99            PadLookup | RoundConstantsLookup | AtMost4Lookup | ByteLookup | RangeCheck16Lookup
100            | SparseLookup | ResetLookup => true,
101            MemoryLookup | RegisterLookup | SyscallLookup | KeccakStepLookup => false,
102        }
103    }
104
105    fn runtime_create_column(&self) -> bool {
106        panic!("No runtime tables specified");
107    }
108
109    fn ix_by_value<F: PrimeField>(&self, value: &[F]) -> Option<usize> {
110        // Shamelessly copied from below, where it is likely also incorrect.
111        let idx = value[0]
112            .to_bytes()
113            .iter()
114            .rev()
115            .fold(0u64, |acc, &x| acc * 256 + x as u64) as usize;
116        match self {
117            // Fixed tables
118            Self::RoundConstantsLookup
119            | Self::AtMost4Lookup
120            | Self::ByteLookup
121            | Self::RangeCheck16Lookup
122            | Self::ResetLookup => Some(idx),
123            Self::PadLookup => Some(idx - 1),
124            Self::SparseLookup => {
125                // Big yikes. This is copied from below.
126                let res = u64::from_str_radix(&format!("{:x}", idx), 2);
127                if let Ok(ok) = res {
128                    Some(ok as usize)
129                } else {
130                    panic!("Help");
131                }
132            }
133            // Non-fixed tables
134            Self::MemoryLookup
135            | Self::RegisterLookup
136            | Self::SyscallLookup
137            | Self::KeccakStepLookup => None,
138        }
139    }
140
141    fn all_variants() -> Vec<Self> {
142        vec![
143            Self::PadLookup,
144            Self::RoundConstantsLookup,
145            Self::AtMost4Lookup,
146            Self::ByteLookup,
147            Self::RangeCheck16Lookup,
148            Self::SparseLookup,
149            Self::ResetLookup,
150            Self::MemoryLookup,
151            Self::RegisterLookup,
152            Self::SyscallLookup,
153            Self::KeccakStepLookup,
154        ]
155    }
156}
157
158/// Trait that creates all the fixed lookup tables used in the VM
159pub(crate) trait FixedLookupTables<F> {
160    /// Checks whether a value is in a table and returns the position if it is
161    /// or None otherwise.
162    fn is_in_table(table: &LookupTable<F>, value: Vec<F>) -> Option<usize>;
163    /// Returns the pad table
164    fn table_pad() -> LookupTable<F>;
165    /// Returns the round constants table
166    fn table_round_constants() -> LookupTable<F>;
167    /// Returns the at most 4 table
168    fn table_at_most_4() -> LookupTable<F>;
169    /// Returns the byte table
170    fn table_byte() -> LookupTable<F>;
171    /// Returns the range check 16 table
172    fn table_range_check_16() -> LookupTable<F>;
173    /// Returns the sparse table
174    fn table_sparse() -> LookupTable<F>;
175    /// Returns the reset table
176    fn table_reset() -> LookupTable<F>;
177    /// Returns a vector containing all fixed tables
178    fn get_all_tables() -> Vec<LookupTable<F>>;
179}
180
181impl<F: Field> FixedLookupTables<F> for LookupTable<F> {
182    fn get_all_tables() -> Vec<LookupTable<F>> {
183        vec![
184            Self::table_pad(),
185            Self::table_round_constants(),
186            Self::table_byte(),
187            Self::table_range_check_16(),
188            Self::table_sparse(),
189            Self::table_reset(),
190        ]
191    }
192
193    fn is_in_table(table: &LookupTable<F>, value: Vec<F>) -> Option<usize> {
194        let id = table.table_id;
195        // In these tables, the first value of the vector is related to the
196        // index within the table.
197        let idx = value[0]
198            .to_bytes()
199            .iter()
200            .rev()
201            .fold(0u64, |acc, &x| acc * 256 + x as u64) as usize;
202
203        match id {
204            RoundConstantsLookup | AtMost4Lookup | ByteLookup | RangeCheck16Lookup
205            | ResetLookup => {
206                if idx < id.length() && table.entries[idx] == value {
207                    Some(idx)
208                } else {
209                    None
210                }
211            }
212            PadLookup => {
213                // Because this table starts with entry 1
214                if idx - 1 < id.length() && table.entries[idx - 1] == value {
215                    Some(idx - 1)
216                } else {
217                    None
218                }
219            }
220            SparseLookup => {
221                let res = u64::from_str_radix(&format!("{:x}", idx), 2);
222                let dense = if let Ok(ok) = res {
223                    ok as usize
224                } else {
225                    id.length() // So that it returns None
226                };
227                if dense < id.length() && table.entries[dense] == value {
228                    Some(dense)
229                } else {
230                    None
231                }
232            }
233            MemoryLookup | RegisterLookup | SyscallLookup | KeccakStepLookup => None,
234        }
235    }
236
237    fn table_pad() -> Self {
238        Self {
239            table_id: PadLookup,
240            entries: (1..=PadLookup.length())
241                .map(|i| {
242                    let suffix = pad_blocks(i);
243                    vec![
244                        F::from(i as u64),
245                        F::two_pow(i as u64),
246                        suffix[0],
247                        suffix[1],
248                        suffix[2],
249                        suffix[3],
250                        suffix[4],
251                    ]
252                })
253                .collect(),
254        }
255    }
256
257    fn table_round_constants() -> Self {
258        Self {
259            table_id: RoundConstantsLookup,
260            entries: (0..RoundConstantsLookup.length())
261                .map(|i| {
262                    vec![
263                        F::from(i as u32),
264                        F::from(Keccak::sparse(RC[i])[3]),
265                        F::from(Keccak::sparse(RC[i])[2]),
266                        F::from(Keccak::sparse(RC[i])[1]),
267                        F::from(Keccak::sparse(RC[i])[0]),
268                    ]
269                })
270                .collect(),
271        }
272    }
273
274    fn table_at_most_4() -> LookupTable<F> {
275        Self {
276            table_id: AtMost4Lookup,
277            entries: (0..AtMost4Lookup.length())
278                .map(|i| vec![F::from(i as u32)])
279                .collect(),
280        }
281    }
282
283    fn table_byte() -> Self {
284        Self {
285            table_id: ByteLookup,
286            entries: (0..ByteLookup.length())
287                .map(|i| vec![F::from(i as u32)])
288                .collect(),
289        }
290    }
291
292    fn table_range_check_16() -> Self {
293        Self {
294            table_id: RangeCheck16Lookup,
295            entries: (0..RangeCheck16Lookup.length())
296                .map(|i| vec![F::from(i as u32)])
297                .collect(),
298        }
299    }
300
301    fn table_sparse() -> Self {
302        Self {
303            table_id: SparseLookup,
304            entries: (0..SparseLookup.length())
305                .map(|i| {
306                    vec![F::from(
307                        u64::from_str_radix(&format!("{:b}", i), 16).unwrap(),
308                    )]
309                })
310                .collect(),
311        }
312    }
313
314    fn table_reset() -> Self {
315        Self {
316            table_id: ResetLookup,
317            entries: (0..ResetLookup.length())
318                .map(|i| {
319                    vec![
320                        F::from(i as u32),
321                        F::from(u64::from_str_radix(&format!("{:b}", i), 16).unwrap()),
322                    ]
323                })
324                .collect(),
325        }
326    }
327}
o1vm/lookups.rs

o1vm/
lookups.rs
