Skip to main content

midnight_circuits/instructions/
zero.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//! Zero instructions interface.
15//!
16//! It provides an interface for comparing assigned values with zero.
17//!
18//! Implementors of this trait need to implement [AssertionInstructions]
19//! and [EqualityInstructions]. The trait is parametrized by `assigned`
20//! values that implement `InnerConstants`, which gives access to zero.
21
22use midnight_proofs::{circuit::Layouter, plonk::Error};
23
24use crate::{
25    instructions::{AssertionInstructions, EqualityInstructions},
26    types::{AssignedBit, InnerConstants},
27    CircuitField,
28};
29
30/// The set of circuit instructions for zero equality and assertions.
31pub trait ZeroInstructions<F, Assigned>:
32    AssertionInstructions<F, Assigned> + EqualityInstructions<F, Assigned>
33where
34    F: CircuitField,
35    Assigned: InnerConstants,
36{
37    /// Enforces that the given assigned element is zero.
38    ///
39    /// ```
40    /// # midnight_circuits::run_test_native_gadget!(chip, layouter, {
41    /// let x: AssignedNative<F> = chip.assign(&mut layouter, Value::known(F::ZERO))?;
42    ///
43    /// // we can now assert that the value is zero (this, obviously, discloses the value)
44    /// chip.assert_zero(&mut layouter, &x)?;
45    /// # });
46    /// ```
47    fn assert_zero(&self, layouter: &mut impl Layouter<F>, x: &Assigned) -> Result<(), Error> {
48        self.assert_equal_to_fixed(layouter, x, Assigned::inner_zero())
49    }
50
51    /// Asserts that the given element is non-zero.
52    fn assert_non_zero(&self, layouter: &mut impl Layouter<F>, x: &Assigned) -> Result<(), Error> {
53        self.assert_not_equal_to_fixed(layouter, x, Assigned::inner_zero())
54    }
55
56    /// Returns `1` iff the given element equals zero (the additive identity).
57    ///
58    /// ```
59    /// # midnight_circuits::run_test_native_gadget!(chip, layouter, {
60    /// let x: AssignedNative<F> = chip.assign(&mut layouter, Value::known(F::ZERO))?;
61    ///
62    /// // the following value should be constrained further
63    /// let cond: AssignedBit<F> = chip.is_zero(&mut layouter, &x)?;
64    /// # });
65    /// ```
66    fn is_zero(
67        &self,
68        layouter: &mut impl Layouter<F>,
69        x: &Assigned,
70    ) -> Result<AssignedBit<F>, Error> {
71        self.is_equal_to_fixed(layouter, x, Assigned::inner_zero())
72    }
73}
74
75#[cfg(test)]
76pub(crate) mod tests {
77    use std::marker::PhantomData;
78
79    use ff::FromUniformBytes;
80    use midnight_proofs::{
81        circuit::{Layouter, SimpleFloorPlanner},
82        dev::MockProver,
83        plonk::{Circuit, ConstraintSystem},
84    };
85    use rand::SeedableRng;
86    use rand_chacha::ChaCha8Rng;
87
88    use super::*;
89    use crate::{
90        instructions::AssignmentInstructions,
91        testing_utils::{FromScratch, Sampleable},
92        types::{AssignedNative, InnerValue},
93        utils::circuit_modeling::{circuit_to_json, cost_measure_end, cost_measure_start},
94    };
95
96    #[derive(Clone, Debug)]
97    enum Operation {
98        Assert,
99        AssertNon,
100        IsZero,
101    }
102
103    #[derive(Clone, Debug)]
104    struct TestCircuit<F, Assigned, ZeroChip>
105    where
106        Assigned: InnerValue,
107    {
108        x: Assigned::Element,
109        expected: Option<bool>,
110        operation: Operation,
111        _marker: PhantomData<(F, Assigned, ZeroChip)>,
112    }
113
114    impl<F, Assigned, ZeroChip> Circuit<F> for TestCircuit<F, Assigned, ZeroChip>
115    where
116        F: CircuitField,
117        Assigned: InnerConstants,
118        ZeroChip:
119            ZeroInstructions<F, Assigned> + AssignmentInstructions<F, Assigned> + FromScratch<F>,
120    {
121        type Config = <ZeroChip as FromScratch<F>>::Config;
122        type FloorPlanner = SimpleFloorPlanner;
123        type Params = ();
124
125        fn without_witnesses(&self) -> Self {
126            unreachable!()
127        }
128
129        fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
130            let committed_instance_column = meta.instance_column();
131            let instance_column = meta.instance_column();
132            let constants_column = meta.fixed_column();
133            meta.enable_constant(constants_column);
134            ZeroChip::configure_from_scratch(
135                meta,
136                &mut vec![],
137                &mut vec![],
138                &[committed_instance_column, instance_column],
139            )
140        }
141
142        fn synthesize(
143            &self,
144            config: Self::Config,
145            mut layouter: impl Layouter<F>,
146        ) -> Result<(), Error> {
147            let chip = ZeroChip::new_from_scratch(&config);
148
149            let x = chip.assign_fixed(&mut layouter, self.x.clone())?;
150            cost_measure_start(&mut layouter);
151            match self.operation {
152                Operation::Assert => chip.assert_zero(&mut layouter, &x),
153                Operation::AssertNon => chip.assert_non_zero(&mut layouter, &x),
154                Operation::IsZero => {
155                    let res = chip.is_zero(&mut layouter, &x)?;
156                    let res_as_value: AssignedNative<F> = res.into();
157                    layouter.assign_region(
158                        || "assert contains fixed",
159                        |mut region| {
160                            region.constrain_constant(
161                                res_as_value.cell(),
162                                if self.expected.unwrap() {
163                                    F::ONE
164                                } else {
165                                    F::ZERO
166                                },
167                            )
168                        },
169                    )
170                }
171            }?;
172            cost_measure_end(&mut layouter);
173
174            chip.load_from_scratch(&mut layouter)
175        }
176    }
177
178    fn run<F, Assigned, ZeroChip>(
179        x: &Assigned::Element,
180        expected: Option<bool>,
181        operation: Operation,
182        must_pass: bool,
183        cost_model: bool,
184        chip_name: &str,
185        op_name: &str,
186    ) where
187        F: CircuitField + FromUniformBytes<64> + Ord,
188        Assigned: InnerConstants,
189        ZeroChip:
190            ZeroInstructions<F, Assigned> + AssignmentInstructions<F, Assigned> + FromScratch<F>,
191    {
192        let circuit = TestCircuit::<F, Assigned, ZeroChip> {
193            x: x.clone(),
194            expected,
195            operation,
196            _marker: PhantomData,
197        };
198
199        let public_inputs = vec![vec![], vec![]];
200        match MockProver::run(&circuit, public_inputs) {
201            Ok(prover) => match prover.verify() {
202                Ok(()) => assert!(must_pass),
203                Err(e) => assert!(!must_pass, "Failed verifier with error {e:?}"),
204            },
205            Err(e) => assert!(!must_pass, "Failed prover with error {e:?}"),
206        }
207
208        if cost_model {
209            circuit_to_json(chip_name, op_name, circuit);
210        }
211    }
212
213    pub fn test_zero_assertions<F, Assigned, ZeroChip>(name: &str)
214    where
215        F: CircuitField + FromUniformBytes<64> + Ord,
216        Assigned: InnerConstants + Sampleable,
217        ZeroChip:
218            ZeroInstructions<F, Assigned> + AssignmentInstructions<F, Assigned> + FromScratch<F>,
219    {
220        let mut rng = ChaCha8Rng::seed_from_u64(0xc0ffee);
221        let mut cost_model = true;
222        [
223            (Assigned::sample_inner(&mut rng), false),
224            (Assigned::inner_zero(), true),
225            (Assigned::inner_one(), false),
226        ]
227        .into_iter()
228        .for_each(|(x, is_zero)| {
229            run::<F, Assigned, ZeroChip>(
230                &x,
231                None,
232                Operation::Assert,
233                is_zero,
234                cost_model,
235                name,
236                "assert_zero",
237            );
238            run::<F, Assigned, ZeroChip>(
239                &x,
240                None,
241                Operation::AssertNon,
242                !is_zero,
243                cost_model,
244                name,
245                "assert_non_zero",
246            );
247            cost_model = false;
248        });
249    }
250
251    pub fn test_is_zero<F, Assigned, ZeroChip>(name: &str)
252    where
253        F: CircuitField + FromUniformBytes<64> + Ord,
254        Assigned: InnerConstants + Sampleable,
255        ZeroChip:
256            ZeroInstructions<F, Assigned> + AssignmentInstructions<F, Assigned> + FromScratch<F>,
257    {
258        let mut rng = ChaCha8Rng::seed_from_u64(0xc0ffee);
259        let mut cost_model = true;
260        [
261            (Assigned::sample_inner(&mut rng), false),
262            (Assigned::inner_zero(), true),
263            (Assigned::inner_one(), false),
264        ]
265        .into_iter()
266        .for_each(|(x, expected)| {
267            run::<F, Assigned, ZeroChip>(
268                &x,
269                Some(expected),
270                Operation::IsZero,
271                true,
272                cost_model,
273                name,
274                "is_zero",
275            );
276            run::<F, Assigned, ZeroChip>(
277                &x,
278                Some(!expected),
279                Operation::IsZero,
280                false,
281                false,
282                "",
283                "",
284            );
285            cost_model = false;
286        });
287    }
288}