Skip to main content

midnight_circuits/map/
map_gadget.rs

1// This file is part of MIDNIGHT-ZK.
2// Copyright (C) Midnight Foundation
3// SPDX-License-Identifier: Apache-2.0
4// Licensed under the Apache License, Version 2.0 (the "License");
5// You may not use this file except in compliance with the License.
6// You may obtain a copy of the License at
7// http://www.apache.org/licenses/LICENSE-2.0
8// Unless required by applicable law or agreed to in writing, software
9// distributed under the License is distributed on an "AS IS" BASIS,
10// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11// See the License for the specific language governing permissions and
12// limitations under the License.
13
14//! In-circuit implementation of Succinct Key-Value Map Representation Using
15//! Merkle Trees
16use midnight_proofs::{
17    circuit::{Layouter, Value},
18    plonk::Error,
19};
20#[cfg(any(test, feature = "testing"))]
21use {
22    crate::testing_utils::FromScratch,
23    midnight_proofs::plonk::{Advice, Column, ConstraintSystem, Fixed, Instance},
24};
25
26use crate::{
27    instructions::{
28        map::{MapCPU, MapInstructions},
29        HashInstructions, NativeInstructions,
30    },
31    map::cpu::{MapMt, TREE_HEIGHT},
32    types::AssignedNative,
33    CircuitField,
34};
35
36#[derive(Clone, Debug)]
37/// State of [MapGadget], containing the assigned succinct representation and
38/// the unassigned map.
39struct State<F, H>
40where
41    F: CircuitField,
42    H: HashInstructions<F, AssignedNative<F>, AssignedNative<F>>,
43{
44    succinct_repr: AssignedNative<F>,
45    map: Box<MapMt<F, H>>,
46}
47
48#[derive(Clone, Debug)]
49/// Gadget for proving `insert` and `get` instructions in a map.
50pub struct MapGadget<F, N, H>
51where
52    F: CircuitField,
53    N: NativeInstructions<F>,
54    H: HashInstructions<F, AssignedNative<F>, AssignedNative<F>>,
55{
56    native_gadget: N,
57    hash_chip: H,
58    state: Option<State<F, H>>,
59}
60
61impl<F, N, H> MapInstructions<F, AssignedNative<F>, AssignedNative<F>> for MapGadget<F, N, H>
62where
63    F: CircuitField,
64    N: NativeInstructions<F>,
65    H: HashInstructions<F, AssignedNative<F>, AssignedNative<F>>,
66{
67    type MapCPU = MapMt<F, H>;
68
69    fn init(
70        &mut self,
71        layouter: &mut impl Layouter<F>,
72        map: Value<MapMt<F, H>>,
73    ) -> Result<(), Error> {
74        let mut init_map = MapMt::new(&F::ZERO);
75        let succinct_repr_value = map.map(|v| {
76            let repr = v.succinct_repr();
77            init_map = v;
78            repr
79        });
80
81        self.state = Some(State {
82            succinct_repr: self.native_gadget.assign(layouter, succinct_repr_value)?,
83            map: Box::new(init_map),
84        });
85
86        Ok(())
87    }
88
89    fn succinct_repr(&self) -> AssignedNative<F> {
90        self.state().succinct_repr.clone()
91    }
92
93    fn insert(
94        &mut self,
95        layouter: &mut impl Layouter<F>,
96        key: &AssignedNative<F>,
97        value: &AssignedNative<F>,
98    ) -> Result<(), Error> {
99        // First we get the path for the current value of `key`, and prove its
100        // correctness.
101        let current_value = key.value().map(|key| self.state().map.get(key));
102        let assigned_current_value = self.native_gadget.assign(layouter, current_value)?;
103
104        let path = self.get_path(layouter, key)?;
105        self.verify_path(layouter, key, &assigned_current_value, &path)?;
106
107        // Next, we update the state (succinct_repr and map), and verify that the same
108        // path is valid with the inserted value.
109        self.update_state(layouter, key, value)?;
110        self.verify_path(layouter, key, value, &path)?;
111
112        Ok(())
113    }
114
115    fn get(
116        &self,
117        layouter: &mut impl Layouter<F>,
118        key: &AssignedNative<F>,
119    ) -> Result<AssignedNative<F>, Error> {
120        let value = key.value().map(|key| self.state().map.get(key));
121        let assigned_value = self.native_gadget.assign(layouter, value)?;
122
123        let path = self.get_path(layouter, key)?;
124        self.verify_path(layouter, key, &assigned_value, &path)?;
125
126        Ok(assigned_value)
127    }
128}
129
130impl<F, N, H> MapGadget<F, N, H>
131where
132    F: CircuitField,
133    N: NativeInstructions<F>,
134    H: HashInstructions<F, AssignedNative<F>, AssignedNative<F>>,
135{
136    /// Create a map gadget
137    pub fn new(native_gadget: &N, hash_chip: &H) -> Self {
138        Self {
139            native_gadget: native_gadget.clone(),
140            hash_chip: hash_chip.clone(),
141            state: None::<State<F, H>>,
142        }
143    }
144
145    /// Returns a reference to the state.
146    ///
147    /// # Panics
148    ///
149    /// If the [MapGadget] has not been initialised.
150    fn state(&self) -> &State<F, H> {
151        self.state.as_ref().expect("Map gadget must be initialised before usage.")
152    }
153
154    /// Update the state by inserting a new value `(value, key)` pair into the
155    /// map and update the assigned succinct_repr accordingly.
156    ///
157    /// # Panics
158    ///
159    /// If the [MapGadget] has not been initialised.
160    fn update_state(
161        &mut self,
162        layouter: &mut impl Layouter<F>,
163        key: &AssignedNative<F>,
164        value: &AssignedNative<F>,
165    ) -> Result<(), Error> {
166        let state = self.state.as_mut().expect("Map gadget must be initialised before usage.");
167
168        let new_root = key.value().zip(value.value()).map(|(key, value)| {
169            state.map.insert(key, value);
170            state.map.succinct_repr()
171        });
172
173        let assigned_new_root: AssignedNative<F> = self.native_gadget.assign(layouter, new_root)?;
174        state.succinct_repr = assigned_new_root.clone();
175
176        self.state = Some(state.clone());
177
178        Ok(())
179    }
180
181    /// Returns the assigned path for the given `key` pair.
182    ///
183    /// # Warning
184    /// This function does not prove that the path is correct. To guarantee its
185    /// correctness, one should call [Self::verify_path].
186    fn get_path(
187        &self,
188        layouter: &mut impl Layouter<F>,
189        key: &AssignedNative<F>,
190    ) -> Result<[AssignedNative<F>; TREE_HEIGHT as usize], Error> {
191        // First we assign the MT path.
192        let path = key.value().map(|key| self.state().map.get_path(key)).transpose_array();
193        Ok(self.native_gadget.assign_many(layouter, &path)?.try_into().unwrap())
194    }
195
196    /// Verify a `proof` is correct w.r.t. the `(key, value)` pair.
197    fn verify_path(
198        &self,
199        layouter: &mut impl Layouter<F>,
200        key: &AssignedNative<F>,
201        value: &AssignedNative<F>,
202        proof: &[AssignedNative<F>; TREE_HEIGHT as usize],
203    ) -> Result<(), Error> {
204        let zero = self.native_gadget.assign_fixed(layouter, F::ZERO)?;
205        let path = self.hash_chip.hash(layouter, &[key.clone(), zero])?;
206        let path_as_bits = self.native_gadget.assigned_to_le_bits(layouter, &path, None, true)?;
207
208        let mut node: AssignedNative<F> = value.clone();
209
210        for (is_right, sibling) in path_as_bits[..TREE_HEIGHT as usize].iter().zip(proof.iter()) {
211            let (left_sibling, right_sibling) =
212                self.native_gadget.cond_swap(layouter, is_right, &node, sibling)?;
213
214            node = self.hash_chip.hash(layouter, &[left_sibling, right_sibling])?;
215        }
216
217        self.native_gadget.assert_equal(layouter, &node, &self.state().succinct_repr)?;
218
219        Ok(())
220    }
221}
222
223#[cfg(any(test, feature = "testing"))]
224impl<F, N, H> FromScratch<F> for MapGadget<F, N, H>
225where
226    F: CircuitField,
227    N: NativeInstructions<F> + FromScratch<F>,
228    H: HashInstructions<F, AssignedNative<F>, AssignedNative<F>> + FromScratch<F>,
229{
230    type Config = (<N as FromScratch<F>>::Config, <H as FromScratch<F>>::Config);
231
232    fn new_from_scratch(config: &Self::Config) -> Self {
233        Self {
234            native_gadget: N::new_from_scratch(&config.0),
235            hash_chip: H::new_from_scratch(&config.1),
236            state: None::<State<F, H>>,
237        }
238    }
239
240    fn configure_from_scratch(
241        meta: &mut ConstraintSystem<F>,
242        advice_columns: &mut Vec<Column<Advice>>,
243        fixed_columns: &mut Vec<Column<Fixed>>,
244        instance_columns: &[Column<Instance>; 2],
245    ) -> Self::Config {
246        (
247            N::configure_from_scratch(meta, advice_columns, fixed_columns, instance_columns),
248            H::configure_from_scratch(meta, advice_columns, fixed_columns, instance_columns),
249        )
250    }
251
252    fn load_from_scratch(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
253        self.native_gadget.load_from_scratch(layouter)?;
254        self.hash_chip.load_from_scratch(layouter)
255    }
256}
257
258#[cfg(test)]
259mod test {
260    use std::marker::PhantomData;
261
262    use ff::FromUniformBytes;
263    use midnight_proofs::{
264        circuit::{SimpleFloorPlanner, Value},
265        dev::MockProver,
266        plonk::Circuit,
267    };
268    use rand::SeedableRng;
269    use rand_chacha::ChaCha8Rng;
270
271    use super::*;
272    use crate::{
273        field::{decomposition::chip::P2RDecompositionChip, NativeChip, NativeGadget},
274        hash::poseidon::{constants::PoseidonField, PoseidonChip},
275        map::cpu::MapMt,
276        utils::circuit_modeling::{circuit_to_json, cost_measure_end, cost_measure_start},
277    };
278
279    #[derive(Clone, Debug)]
280    enum MapTests {
281        Get,
282        Insert,
283    }
284
285    struct TestCircuit<F, N, H>
286    where
287        F: CircuitField,
288        N: NativeInstructions<F>,
289        H: HashInstructions<F, AssignedNative<F>, AssignedNative<F>> + FromScratch<F>,
290    {
291        map: Value<MapMt<F, H>>,
292        key: Value<F>,
293        value: Value<F>,
294        mode: MapTests,
295        _marker: PhantomData<N>,
296    }
297
298    impl<F, N, H> Circuit<F> for TestCircuit<F, N, H>
299    where
300        F: CircuitField,
301        N: NativeInstructions<F> + FromScratch<F>,
302        H: HashInstructions<F, AssignedNative<F>, AssignedNative<F>> + FromScratch<F>,
303    {
304        type Config = <MapGadget<F, N, H> as FromScratch<F>>::Config;
305        type FloorPlanner = SimpleFloorPlanner;
306        type Params = ();
307
308        fn without_witnesses(&self) -> Self {
309            Self {
310                key: Value::unknown(),
311                value: Value::unknown(),
312                map: Value::unknown(),
313                mode: MapTests::Get,
314                _marker: PhantomData,
315            }
316        }
317
318        fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
319            let committed_instance_column = meta.instance_column();
320            let instance_column = meta.instance_column();
321            MapGadget::<F, N, H>::configure_from_scratch(
322                meta,
323                &mut vec![],
324                &mut vec![],
325                &[committed_instance_column, instance_column],
326            )
327        }
328
329        fn synthesize(
330            &self,
331            config: Self::Config,
332            mut layouter: impl Layouter<F>,
333        ) -> Result<(), Error> {
334            let native_gadget = N::new_from_scratch(&config.0);
335            let poseidon_gadget = H::new_from_scratch(&config.1);
336            let mut map_gadget = MapGadget::<F, N, H>::new(&native_gadget, &poseidon_gadget);
337
338            map_gadget.init(&mut layouter, self.map.clone())?;
339
340            let assigned_key: AssignedNative<F> = native_gadget.assign(&mut layouter, self.key)?;
341            let assigned_value: AssignedNative<F> =
342                native_gadget.assign(&mut layouter, self.value)?;
343
344            native_gadget.constrain_as_public_input(&mut layouter, &map_gadget.succinct_repr())?;
345
346            cost_measure_start(&mut layouter);
347            match self.mode {
348                MapTests::Get => {
349                    let value = map_gadget.get(&mut layouter, &assigned_key)?;
350                    map_gadget.native_gadget.assert_equal(
351                        &mut layouter,
352                        &value,
353                        &assigned_value,
354                    )?;
355                }
356                MapTests::Insert => {
357                    map_gadget.insert(&mut layouter, &assigned_key, &assigned_value)?;
358
359                    native_gadget
360                        .constrain_as_public_input(&mut layouter, &map_gadget.succinct_repr())?;
361                }
362            }
363            cost_measure_end(&mut layouter);
364
365            map_gadget.load_from_scratch(&mut layouter)
366        }
367    }
368
369    fn test_map<F, N, H>(cost_model: bool)
370    where
371        F: CircuitField + FromUniformBytes<64> + Ord,
372        N: NativeInstructions<F> + FromScratch<F>,
373        H: HashInstructions<F, AssignedNative<F>, AssignedNative<F>> + FromScratch<F>,
374    {
375        let mut rng = ChaCha8Rng::seed_from_u64(0xc0ffee);
376
377        let mut mt = MapMt::<F, H>::new(&F::ZERO);
378
379        // Let's add 100 random elements
380        for _ in 0..100 {
381            mt.insert(&F::random(&mut rng), &F::random(&mut rng));
382        }
383
384        mt.insert(&F::ONE, &F::ONE);
385
386        [
387            (F::ZERO, F::ZERO, true, MapTests::Get, cost_model),
388            (F::ZERO, F::ONE, false, MapTests::Get, false),
389            (F::ONE, F::ONE, true, MapTests::Get, false),
390            (F::random(&mut rng), F::ZERO, true, MapTests::Get, false),
391            (F::ONE, F::ZERO, false, MapTests::Get, false),
392            (
393                F::ONE,
394                F::random(&mut rng),
395                true,
396                MapTests::Insert,
397                cost_model,
398            ),
399            (
400                F::ONE,
401                F::random(&mut rng),
402                false,
403                MapTests::Insert,
404                cost_model,
405            ),
406        ]
407        .into_iter()
408        .for_each(|(key, value, test_passes, mode, cost_model)| {
409            let updated_map = if test_passes {
410                let mut map = mt.clone();
411                map.insert(&key, &value);
412                map
413            } else {
414                mt.clone()
415            };
416
417            let mut pi = vec![mt.root];
418            pi.push(updated_map.root);
419
420            let circuit = TestCircuit {
421                map: Value::known(mt.clone()),
422                key: Value::known(key),
423                value: Value::known(value),
424                mode: mode.clone(),
425                _marker: PhantomData::<N>,
426            };
427
428            let prover = MockProver::run(&circuit, vec![vec![], pi.clone()]).unwrap();
429            if test_passes {
430                assert!(prover.verify().is_ok());
431            } else {
432                assert!(prover.verify().is_err());
433            }
434
435            if cost_model {
436                circuit_to_json::<F>("Map gadget", &format!("{:?}", mode), circuit);
437            }
438        });
439    }
440
441    fn run_poseidon_test<F: PoseidonField + ff::FromUniformBytes<64> + Ord>(cost_model: bool) {
442        test_map::<F, NativeGadget<F, P2RDecompositionChip<F>, NativeChip<F>>, PoseidonChip<F>>(
443            cost_model,
444        )
445    }
446
447    #[test]
448    fn test_map_poseidon() {
449        run_poseidon_test::<midnight_curves::Fq>(true);
450    }
451}