jf_relation/gadgets/ultraplonk/
lookup_table.rs

1// Copyright (c) 2022 Espresso Systems (espressosys.com)
2// This file is part of the Jellyfish library.
3
4// You should have received a copy of the MIT License
5// along with the Jellyfish library. If not, see <https://mit-license.org/>.
6
7//! Lookup gates over variable tables.
8
9use crate::{gates::LookupGate, Circuit, CircuitError, PlonkCircuit, Variable};
10use ark_ff::PrimeField;
11use ark_std::{boxed::Box, cmp::max};
12
13impl<F: PrimeField> PlonkCircuit<F> {
14    /// Create a table with keys/values
15    ///     [0, ..., n - 1] and
16    ///     [table_vars\[0\], ..., table_vars\[n - 1\]];
17    /// and create a list of variable tuples to be looked up:
18    ///     [lookup_vars\[0\], ..., lookup_vars\[m - 1\]];
19    ///
20    /// w.l.o.g we assume n = m as we can pad with dummy tuples when n != m
21    pub fn create_table_and_lookup_variables(
22        &mut self,
23        lookup_vars: &[(Variable, Variable, Variable)],
24        table_vars: &[(Variable, Variable)],
25    ) -> Result<(), CircuitError> {
26        for lookup_var in lookup_vars.iter() {
27            self.check_var_bound(lookup_var.0)?;
28            self.check_var_bound(lookup_var.1)?;
29            self.check_var_bound(lookup_var.2)?;
30        }
31        for table_var in table_vars.iter() {
32            self.check_var_bound(table_var.0)?;
33            self.check_var_bound(table_var.1)?;
34        }
35        let n = max(lookup_vars.len(), table_vars.len());
36        let n_gate = self.num_gates();
37        (*self.table_gate_ids_mut()).push((n_gate, n));
38        let table_ctr = F::from(self.table_gate_ids_mut().len() as u64);
39        for i in 0..n {
40            let (q_dom_sep, key, val0, val1) = match i < lookup_vars.len() {
41                true => (
42                    table_ctr,
43                    lookup_vars[i].0,
44                    lookup_vars[i].1,
45                    lookup_vars[i].2,
46                ),
47                false => (F::zero(), self.zero(), self.zero(), self.zero()),
48            };
49            let (table_dom_sep, table_key, table_val0, table_val1) = match i < table_vars.len() {
50                true => (
51                    table_ctr,
52                    F::from(i as u64),
53                    table_vars[i].0,
54                    table_vars[i].1,
55                ),
56                false => (F::zero(), F::zero(), self.zero(), self.zero()),
57            };
58            let wire_vars = [key, val0, val1, table_val0, table_val1];
59
60            self.insert_gate(
61                &wire_vars,
62                Box::new(LookupGate {
63                    q_dom_sep,
64                    table_dom_sep,
65                    table_key,
66                }),
67            )?;
68        }
69        *self.num_table_elems_mut() += n;
70        Ok(())
71    }
72}
73
74#[cfg(test)]
75mod test {
76    use super::*;
77    use ark_bls12_377::Fq as Fq377;
78    use ark_ed_on_bls12_377::Fq as FqEd377;
79    use ark_ed_on_bls12_381::Fq as FqEd381;
80    use ark_ed_on_bn254::Fq as FqEd254;
81    use ark_std::vec;
82    use jf_utils::test_rng;
83
84    #[test]
85    fn test_lookup_table() -> Result<(), CircuitError> {
86        test_lookup_table_helper::<FqEd254>()?;
87        test_lookup_table_helper::<FqEd377>()?;
88        test_lookup_table_helper::<FqEd381>()?;
89        test_lookup_table_helper::<Fq377>()
90    }
91    fn test_lookup_table_helper<F: PrimeField>() -> Result<(), CircuitError> {
92        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(4);
93        let mut rng = test_rng();
94
95        // create table variables
96        let mut table_vars = vec![];
97        let n = 10;
98        for _ in 0..n {
99            let val0 = circuit.create_variable(F::rand(&mut rng))?;
100            let val1 = circuit.create_variable(F::rand(&mut rng))?;
101            table_vars.push((val0, val1));
102        }
103        // create lookup variables
104        let mut lookup_vars = vec![];
105        table_vars
106            .iter()
107            .enumerate()
108            .try_for_each(|(i, (idx0, idx1))| {
109                let val0 = circuit.witness(*idx0)?;
110                let val1 = circuit.witness(*idx1)?;
111                let key_var = circuit.create_variable(F::from(i as u32))?;
112                let val0_var = circuit.create_variable(val0)?;
113                let val1_var = circuit.create_variable(val1)?;
114                lookup_vars.push((key_var, val0_var, val1_var));
115                Ok(())
116            })?;
117        // add lookup variables and tables
118        circuit.create_table_and_lookup_variables(&lookup_vars, &table_vars)?;
119        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
120
121        // the number of added lookup vars is less than the added table size
122        circuit.create_table_and_lookup_variables(&lookup_vars[..n - 1], &table_vars)?;
123        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
124
125        // the number of added lookup vars is larger than the added table size
126        for i in 0..n {
127            // add a new lookup var
128            lookup_vars.push(lookup_vars[i]);
129        }
130        circuit.create_table_and_lookup_variables(&lookup_vars, &table_vars)?;
131        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
132
133        // Error paths
134        // lookup variable outside the table.
135        lookup_vars[0].1 = circuit.zero();
136        circuit.create_table_and_lookup_variables(&lookup_vars[..1], &table_vars)?;
137        assert!(circuit.check_circuit_satisfiability(&[]).is_err());
138
139        // out-of-bound variables
140        let bad_lookup_vars = vec![(circuit.num_vars(), circuit.zero(), circuit.zero())];
141        let bad_table_vars = vec![(circuit.num_vars(), circuit.zero())];
142        assert!(circuit
143            .create_table_and_lookup_variables(&bad_lookup_vars, &table_vars)
144            .is_err());
145        assert!(circuit
146            .create_table_and_lookup_variables(&lookup_vars, &bad_table_vars)
147            .is_err());
148
149        // A lookup over a separate table should not satisfy the circuit.
150        let mut circuit: PlonkCircuit<F> = PlonkCircuit::new_ultra_plonk(4);
151        let mut rng = test_rng();
152
153        let val0 = circuit.create_variable(F::rand(&mut rng))?;
154        let val1 = circuit.create_variable(F::rand(&mut rng))?;
155        let table_vars_1 = vec![(val0, val1)];
156        let val2 = circuit.create_variable(F::rand(&mut rng))?;
157        let val3 = circuit.create_variable(F::rand(&mut rng))?;
158        let table_vars_2 = vec![(val2, val3)];
159        let val2 = circuit.witness(table_vars_2[0].0)?;
160        let val3 = circuit.witness(table_vars_2[0].1)?;
161        let val2_var = circuit.create_variable(val2)?;
162        let val3_var = circuit.create_variable(val3)?;
163        let lookup_vars_1 = vec![(circuit.zero(), val2_var, val3_var)];
164
165        circuit.create_table_and_lookup_variables(&lookup_vars_1, &table_vars_2)?;
166        assert!(circuit.check_circuit_satisfiability(&[]).is_ok());
167        circuit.create_table_and_lookup_variables(&lookup_vars_1, &table_vars_1)?;
168        assert!(circuit.check_circuit_satisfiability(&[]).is_err());
169
170        Ok(())
171    }
172}
jf_relation/gadgets/ultraplonk/lookup_table.rs

jf_relation/gadgets/ultraplonk/
lookup_table.rs
