darkfi/zk/gadget/
smt.rs

1/* This file is part of DarkFi (https://dark.fi)
2 *
3 * Copyright (C) 2020-2026 Dyne.org foundation
4 *
5 * This program is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU Affero General Public License as
7 * published by the Free Software Foundation, either version 3 of the
8 * License, or (at your option) any later version.
9 *
10 * This program is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
13 * GNU Affero General Public License for more details.
14 *
15 * You should have received a copy of the GNU Affero General Public License
16 * along with this program.  If not, see <https://www.gnu.org/licenses/>.
17 */
18
19use darkfi_sdk::crypto::smt::SMT_FP_DEPTH;
20use halo2_gadgets::poseidon::{
21    primitives as poseidon, Hash as PoseidonHash, Pow5Chip as PoseidonChip,
22    Pow5Config as PoseidonConfig,
23};
24use halo2_proofs::{
25    circuit::{AssignedCell, Layouter, Value},
26    pasta::{
27        group::ff::{Field, PrimeFieldBits},
28        Fp,
29    },
30    plonk::{self, Advice, Column, ConstraintSystem, Constraints, Selector},
31    poly::Rotation,
32};
33
34use super::{
35    cond_select::{ConditionalSelectChip, ConditionalSelectConfig, NUM_OF_UTILITY_ADVICE_COLUMNS},
36    is_equal::{AssertEqualChip, AssertEqualConfig},
37};
38
39#[derive(Clone, Debug)]
40pub struct PathConfig {
41    s_path: Selector,
42    advices: [Column<Advice>; 2],
43    poseidon_config: PoseidonConfig<Fp, 3, 2>,
44    conditional_select_config: ConditionalSelectConfig<Fp>,
45    assert_equal_config: AssertEqualConfig<Fp>,
46}
47
48impl PathConfig {
49    fn poseidon_chip(&self) -> PoseidonChip<Fp, 3, 2> {
50        PoseidonChip::construct(self.poseidon_config.clone())
51    }
52
53    fn conditional_select_chip(&self) -> ConditionalSelectChip<Fp> {
54        ConditionalSelectChip::construct(self.conditional_select_config.clone())
55    }
56
57    fn assert_eq_chip(&self) -> AssertEqualChip<Fp> {
58        AssertEqualChip::construct(self.assert_equal_config.clone())
59    }
60}
61
62#[derive(Clone, Debug)]
63pub struct PathChip {
64    config: PathConfig,
65}
66
67impl PathChip {
68    pub fn configure(
69        meta: &mut ConstraintSystem<Fp>,
70        advices: [Column<Advice>; 2],
71        utility_advices: [Column<Advice>; NUM_OF_UTILITY_ADVICE_COLUMNS],
72        poseidon_config: PoseidonConfig<Fp, 3, 2>,
73    ) -> PathConfig {
74        let s_path = meta.selector();
75
76        for advice in &advices {
77            meta.enable_equality(*advice);
78        }
79
80        for advice in &utility_advices {
81            meta.enable_equality(*advice);
82        }
83
84        meta.create_gate("Path builder", |meta| {
85            let s_path = meta.query_selector(s_path);
86            let current_path = meta.query_advice(advices[0], Rotation::cur());
87            let bit = meta.query_advice(advices[1], Rotation::cur());
88            let next_path = meta.query_advice(advices[0], Rotation::next());
89
90            Constraints::with_selector(s_path, Some(next_path - (current_path * Fp::from(2) + bit)))
91        });
92
93        PathConfig {
94            s_path,
95            advices,
96            poseidon_config,
97            conditional_select_config: ConditionalSelectChip::configure(meta, utility_advices),
98            assert_equal_config: AssertEqualChip::configure(
99                meta,
100                [utility_advices[0], utility_advices[1]],
101            ),
102        }
103    }
104
105    pub fn construct(config: PathConfig) -> Self {
106        Self { config }
107    }
108
109    fn decompose_value(value: &Fp) -> Vec<Fp> {
110        // Returns 256 bits, but the last bit is uneeded
111        let bits: Vec<bool> = value.to_le_bits().into_iter().collect();
112
113        let mut bits: Vec<Fp> = bits[..SMT_FP_DEPTH].iter().map(|x| Fp::from(*x)).collect();
114        bits.resize(SMT_FP_DEPTH, Fp::from(0));
115        bits
116    }
117
118    pub fn check_membership(
119        &self,
120        layouter: &mut impl Layouter<Fp>,
121        pos: AssignedCell<Fp, Fp>,
122        path: Value<[Fp; SMT_FP_DEPTH]>,
123        leaf: AssignedCell<Fp, Fp>,
124    ) -> Result<AssignedCell<Fp, Fp>, plonk::Error> {
125        let path = path.transpose_array();
126        // Witness values
127        let (bits, path, zero) = layouter.assign_region(
128            || "witness",
129            |mut region| {
130                let bits = pos.value().map(Self::decompose_value).transpose_vec(SMT_FP_DEPTH);
131                assert_eq!(bits.len(), SMT_FP_DEPTH);
132
133                let mut witness_bits = vec![];
134                let mut witness_path = vec![];
135                for (i, (bit, sibling)) in bits.into_iter().zip(path.into_iter()).enumerate() {
136                    let bit = region.assign_advice(
137                        || "witness pos bit",
138                        self.config.advices[0],
139                        i,
140                        || bit,
141                    )?;
142                    witness_bits.push(bit);
143
144                    let sibling = region.assign_advice(
145                        || "witness path sibling",
146                        self.config.advices[1],
147                        i,
148                        || sibling,
149                    )?;
150                    witness_path.push(sibling);
151                }
152
153                let zero = region.assign_advice(
154                    || "witness zero",
155                    self.config.advices[0],
156                    SMT_FP_DEPTH,
157                    || Value::known(Fp::ZERO),
158                )?;
159                region.constrain_constant(zero.cell(), Fp::ZERO)?;
160
161                Ok((witness_bits, witness_path, zero))
162            },
163        )?;
164        assert_eq!(bits.len(), path.len());
165        assert_eq!(bits.len(), SMT_FP_DEPTH);
166
167        let condselect_chip = self.config.conditional_select_chip();
168        let asserteq_chip = self.config.assert_eq_chip();
169
170        // Check path construction
171        let mut current_path = zero;
172        for bit in bits.iter().rev() {
173            current_path = layouter.assign_region(
174                || "pᵢ₊₁ = 2pᵢ + bᵢ",
175                |mut region| {
176                    self.config.s_path.enable(&mut region, 0)?;
177
178                    current_path.copy_advice(
179                        || "current path",
180                        &mut region,
181                        self.config.advices[0],
182                        0,
183                    )?;
184                    bit.copy_advice(|| "path bit", &mut region, self.config.advices[1], 0)?;
185
186                    let next_path =
187                        current_path.value().zip(bit.value()).map(|(p, b)| p * Fp::from(2) + b);
188                    region.assign_advice(|| "next path", self.config.advices[0], 1, || next_path)
189                },
190            )?;
191        }
192
193        // Check tree construction
194        let mut current_node = leaf.clone();
195        for (bit, sibling) in bits.into_iter().zip(path.into_iter().rev()) {
196            // Conditional select also constraints the bit ∈ {0, 1}
197            let left = condselect_chip.conditional_select(
198                layouter,
199                sibling.clone(),
200                current_node.clone(),
201                bit.clone(),
202            )?;
203            let right = condselect_chip.conditional_select(
204                layouter,
205                current_node.clone(),
206                sibling,
207                bit.clone(),
208            )?;
209            //println!("bit: {:?}", bit);
210            //println!("left: {:?}, right: {:?}", left, right);
211
212            let hasher = PoseidonHash::<
213                _,
214                _,
215                poseidon::P128Pow5T3,
216                poseidon::ConstantLength<2>,
217                3,
218                2,
219            >::init(
220                self.config.poseidon_chip(),
221                layouter.namespace(|| "SmtPoseidonHash init"),
222            )?;
223
224            current_node =
225                hasher.hash(layouter.namespace(|| "SmtPoseidonHash hash"), [left, right])?;
226        }
227
228        asserteq_chip.assert_equal(layouter, current_path, pos)?;
229
230        let root = current_node;
231        Ok(root)
232    }
233}
234
235#[cfg(test)]
236mod tests {
237    use super::*;
238    use darkfi_sdk::crypto::smt::{MemoryStorageFp, PoseidonFp, SmtMemoryFp, EMPTY_NODES_FP};
239    use halo2_proofs::{circuit::floor_planner, dev::MockProver, plonk::Circuit};
240    use rand::rngs::OsRng;
241
242    struct TestCircuit {
243        path: Value<[Fp; SMT_FP_DEPTH]>,
244        leaf: Value<Fp>,
245        root: Value<Fp>,
246    }
247
248    impl Circuit<Fp> for TestCircuit {
249        type Config = PathConfig;
250        type FloorPlanner = floor_planner::V1;
251        type Params = ();
252
253        fn without_witnesses(&self) -> Self {
254            Self { root: Value::unknown(), path: Value::unknown(), leaf: Value::unknown() }
255        }
256
257        fn configure(meta: &mut ConstraintSystem<Fp>) -> Self::Config {
258            // Advice wires required by PathChip
259            let advices = [(); 2].map(|_| meta.advice_column());
260            let utility_advices = [(); NUM_OF_UTILITY_ADVICE_COLUMNS].map(|_| meta.advice_column());
261
262            // Setup poseidon config
263            let poseidon_advices = [(); 4].map(|_| meta.advice_column());
264            for advice in &poseidon_advices {
265                meta.enable_equality(*advice);
266            }
267
268            // Needed for poseidon hash
269            let col_const = meta.fixed_column();
270            meta.enable_constant(col_const);
271
272            let rc_a = [(); 3].map(|_| meta.fixed_column());
273            let rc_b = [(); 3].map(|_| meta.fixed_column());
274
275            let poseidon_config = PoseidonChip::configure::<poseidon::P128Pow5T3>(
276                meta,
277                poseidon_advices[1..4].try_into().unwrap(),
278                poseidon_advices[0],
279                rc_a,
280                rc_b,
281            );
282
283            PathChip::configure(meta, advices, utility_advices, poseidon_config)
284        }
285
286        fn synthesize(
287            &self,
288            config: Self::Config,
289            mut layouter: impl Layouter<Fp>,
290        ) -> Result<(), plonk::Error> {
291            // Initialize the Path chip
292            let path_chip = PathChip::construct(config.clone());
293
294            // Initialize the AssertEqual chip
295            let assert_eq_chip = config.assert_eq_chip();
296
297            // Witness values
298            let (leaf, root) = layouter.assign_region(
299                || "witness",
300                |mut region| {
301                    let leaf = region.assign_advice(
302                        || "witness leaf",
303                        config.advices[0],
304                        0,
305                        || self.leaf,
306                    )?;
307                    let root = region.assign_advice(
308                        || "witness root",
309                        config.advices[1],
310                        0,
311                        || self.root,
312                    )?;
313                    Ok((leaf, root))
314                },
315            )?;
316
317            let calc_root =
318                path_chip.check_membership(&mut layouter, leaf.clone(), self.path, leaf.clone())?;
319            // Normally we just reveal it as a public input.
320            // But I'm too lazy to make a separate config for this unit test so
321            // do this instead.
322            assert_eq_chip.assert_equal(&mut layouter, calc_root, root)?;
323
324            Ok(())
325        }
326    }
327
328    #[test]
329    fn test_smt_circuit() {
330        let hasher = PoseidonFp::new();
331        let store = MemoryStorageFp::new();
332        let mut smt = SmtMemoryFp::new(store, hasher.clone(), &EMPTY_NODES_FP);
333
334        let leaves = vec![Fp::random(&mut OsRng), Fp::random(&mut OsRng), Fp::random(&mut OsRng)];
335        // Use the leaf value as its position in the SMT
336        // Therefore we need an additional constraint that leaf == pos
337        let leaves: Vec<_> = leaves.into_iter().map(|l| (l, l)).collect();
338        smt.insert_batch(leaves.clone()).unwrap();
339
340        let (pos, leaf) = leaves[2];
341        assert_eq!(pos, leaf);
342        assert_eq!(smt.get_leaf(&pos), leaf);
343
344        let root = smt.root();
345        let path = smt.prove_membership(&pos);
346        assert!(path.verify(&root, &leaf, &pos));
347
348        let circuit = TestCircuit {
349            path: Value::known(path.path),
350            leaf: Value::known(leaf),
351            root: Value::known(root),
352        };
353
354        const K: u32 = 14;
355        let prover = MockProver::run(K, &circuit, vec![]).unwrap();
356        prover.assert_satisfied();
357
358        //use halo2_proofs::dev::CircuitLayout;
359        //use plotters::prelude::*;
360        //let root = BitMapBackend::new("target/smt.png", (3840, 2160)).into_drawing_area();
361        //CircuitLayout::default().render(K, &circuit, &root).unwrap();
362    }
363}