midnight_circuits/instructions/
bitwise.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//! Bitwise instructions interface.
15//!
16//! It provides functions for performing bit-wise Boolean operations between
17//! assigned values in the circuit.
18//!
19//! This trait is parametrized by a generic `Assigned` (required to implement
20//! [InnerValue](crate::types::InnerValue)) and whose inner `Element` type is
21//! required to implement [CircuitField]). `Assigned` defined the type over
22//! which the bitwise operations take place.
23
24use ff::Field;
25use midnight_proofs::{circuit::Layouter, plonk::Error};
26use num_bigint::BigUint;
27use num_traits::One;
28
29use super::{BinaryInstructions, DecompositionInstructions, RangeCheckInstructions};
30use crate::{
31    types::{InnerConstants, Instantiable},
32    CircuitField,
33};
34
35/// The set of circuit instructions for binary bit-wise operations.
36pub trait BitwiseInstructions<F, Assigned>:
37    BinaryInstructions<F> + DecompositionInstructions<F, Assigned> + RangeCheckInstructions<F, Assigned>
38where
39    F: CircuitField,
40    Assigned: Instantiable<F> + InnerConstants + Clone,
41    Assigned::Element: CircuitField,
42{
43    /// Bitwise conjunction of the given assigned elements, interpreted as
44    /// binary bit-strings of length `n`.
45    ///
46    /// # Unsatisfiable Circuit
47    ///
48    /// If any of the given assigned elements cannot be decomposed in `n` bits.
49    ///
50    /// ```
51    /// # midnight_circuits::run_test_native_gadget!(chip, layouter, {
52    /// let x = chip.assign(&mut layouter, Value::known(F::from(13)))?;
53    /// let y = chip.assign(&mut layouter, Value::known(F::from(7)))?;
54    ///
55    /// // 0b1101 & 0b0111 = 0b0101
56    /// let res = chip.band(&mut layouter, &x, &y, 4)?;
57    /// chip.assert_equal_to_fixed(&mut layouter, &res, F::from(5))?;
58    /// # });
59    /// ```
60    ///
61    /// ```should_panic
62    /// # midnight_circuits::run_test_native_gadget!(chip, layouter, {
63    /// let x = chip.assign(&mut layouter, Value::known(F::from(16)))?;
64    /// let y = chip.assign(&mut layouter, Value::known(F::from(7)))?;
65    ///
66    /// // x is not in the range [0, 2^4), the following should be unsatisfiable
67    /// let res = chip.band(&mut layouter, &x, &y, 4)?;
68    /// # });
69    /// ```
70    fn band(
71        &self,
72        layouter: &mut impl Layouter<F>,
73        x: &Assigned,
74        y: &Assigned,
75        n: usize,
76    ) -> Result<Assigned, Error> {
77        let x_bits = self.assigned_to_le_bits(layouter, x, Some(n), true)?;
78        let y_bits = self.assigned_to_le_bits(layouter, y, Some(n), true)?;
79        let res_bits = x_bits
80            .into_iter()
81            .zip(y_bits.into_iter())
82            .map(|(bx, by)| self.and(layouter, &[bx, by]))
83            .collect::<Result<Vec<_>, Error>>()?;
84        self.assigned_from_le_bits(layouter, &res_bits)
85    }
86
87    /// Bitwise disjunction of the given assigned elements, interpreted as
88    /// binary bit-strings of length `n`.
89    ///
90    /// # Unsatisfiable Circuit
91    ///
92    /// If any of the given assigned elements cannot be decomposed in `n` bits.
93    ///
94    /// ```
95    /// # midnight_circuits::run_test_native_gadget!(chip, layouter, {
96    /// let x = chip.assign(&mut layouter, Value::known(F::from(13)))?;
97    /// let y = chip.assign(&mut layouter, Value::known(F::from(7)))?;
98    ///
99    /// // 0b1101 | 0b0111 = 0b1111
100    /// let res = chip.bor(&mut layouter, &x, &y, 4)?;
101    /// chip.assert_equal_to_fixed(&mut layouter, &res, F::from(15))?;
102    /// # });
103    /// ```
104    fn bor(
105        &self,
106        layouter: &mut impl Layouter<F>,
107        x: &Assigned,
108        y: &Assigned,
109        n: usize,
110    ) -> Result<Assigned, Error> {
111        let x_bits = self.assigned_to_le_bits(layouter, x, Some(n), true)?;
112        let y_bits = self.assigned_to_le_bits(layouter, y, Some(n), true)?;
113        let res_bits = x_bits
114            .into_iter()
115            .zip(y_bits.into_iter())
116            .map(|(bx, by)| self.or(layouter, &[bx, by]))
117            .collect::<Result<Vec<_>, Error>>()?;
118        self.assigned_from_le_bits(layouter, &res_bits)
119    }
120
121    /// Bitwise exclusive-or of the given assigned elements, interpreted as
122    /// binary bit-strings of length `n`.
123    ///
124    /// # Unsatisfiable Circuit
125    ///
126    /// If any of the given assigned elements cannot be decomposed in `n` bits.
127    ///
128    /// ```
129    /// # midnight_circuits::run_test_native_gadget!(chip, layouter, {
130    /// let x = chip.assign(&mut layouter, Value::known(F::from(13)))?;
131    /// let y = chip.assign(&mut layouter, Value::known(F::from(7)))?;
132    ///
133    /// // 0b1101 ^ 0b0111 = 0b1010
134    /// let res = chip.bxor(&mut layouter, &x, &y, 4)?;
135    /// chip.assert_equal_to_fixed(&mut layouter, &res, F::from(10))?;
136    /// # });
137    /// ```
138    fn bxor(
139        &self,
140        layouter: &mut impl Layouter<F>,
141        x: &Assigned,
142        y: &Assigned,
143        n: usize,
144    ) -> Result<Assigned, Error> {
145        let x_bits = self.assigned_to_le_bits(layouter, x, Some(n), true)?;
146        let y_bits = self.assigned_to_le_bits(layouter, y, Some(n), true)?;
147        let res_bits = x_bits
148            .into_iter()
149            .zip(y_bits.into_iter())
150            .map(|(bx, by)| self.xor(layouter, &[bx, by]))
151            .collect::<Result<Vec<_>, Error>>()?;
152        self.assigned_from_le_bits(layouter, &res_bits)
153    }
154
155    /// Bitwise negation of the given assigned element, interpreted as a
156    /// binary bit-string of length `n`.
157    ///
158    /// # Unsatisfiable Circuit
159    ///
160    /// If the given assigned element cannot be decomposed in `n` bits.
161    ///
162    /// ```
163    /// # midnight_circuits::run_test_native_gadget!(chip, layouter, {
164    /// let x = chip.assign(&mut layouter, Value::known(F::from(6)))?;
165    ///
166    /// // !0b0110 = 0b1001
167    /// let res = chip.bnot(&mut layouter, &x, 4)?;
168    /// chip.assert_equal_to_fixed(&mut layouter, &res, F::from(9))?;
169    /// # });
170    /// ```
171    fn bnot(
172        &self,
173        layouter: &mut impl Layouter<F>,
174        x: &Assigned,
175        n: usize,
176    ) -> Result<Assigned, Error> {
177        // Simply return `2^n - 1 - x` after having verified that `x in [0, 2^n)`.
178        self.assert_lower_than_fixed(layouter, x, &(BigUint::one() << n))?;
179        self.linear_combination(
180            layouter,
181            &[(-Assigned::inner_one(), x.clone())],
182            Assigned::Element::from(2).pow([n as u64]) - Assigned::inner_one(),
183        )
184    }
185}
186
187#[cfg(test)]
188pub(crate) mod tests {
189    use std::{cmp::min, marker::PhantomData};
190
191    use ff::FromUniformBytes;
192    use midnight_proofs::{
193        circuit::{Layouter, SimpleFloorPlanner, Value},
194        dev::MockProver,
195        plonk::{Circuit, ConstraintSystem},
196    };
197    use rand::{RngCore, SeedableRng};
198    use rand_chacha::ChaCha8Rng;
199
200    use super::*;
201    use crate::{
202        testing_utils::FromScratch,
203        utils::circuit_modeling::{circuit_to_json, cost_measure_end, cost_measure_start},
204    };
205
206    #[derive(Clone, Copy, Debug)]
207    enum Operation {
208        Band,
209        Bor,
210        Bxor,
211        Bnot,
212    }
213
214    #[derive(Clone, Debug)]
215    struct TestCircuit<F, Assigned, BitwiseChip>
216    where
217        Assigned: InnerConstants,
218    {
219        inputs: Vec<Assigned::Element>,
220        expected: Assigned::Element,
221        n: usize,
222        operation: Operation,
223        _marker: PhantomData<(F, Assigned, BitwiseChip)>,
224    }
225
226    impl<F, Assigned, BitwiseChip> Circuit<F> for TestCircuit<F, Assigned, BitwiseChip>
227    where
228        F: CircuitField,
229        Assigned: Instantiable<F> + InnerConstants + Clone,
230        Assigned::Element: CircuitField,
231        BitwiseChip: BitwiseInstructions<F, Assigned> + FromScratch<F>,
232    {
233        type Config = <BitwiseChip as FromScratch<F>>::Config;
234        type FloorPlanner = SimpleFloorPlanner;
235        type Params = ();
236
237        fn without_witnesses(&self) -> Self {
238            unreachable!()
239        }
240
241        fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
242            let committed_instance_column = meta.instance_column();
243            let instance_column = meta.instance_column();
244            BitwiseChip::configure_from_scratch(
245                meta,
246                &mut vec![],
247                &mut vec![],
248                &[committed_instance_column, instance_column],
249            )
250        }
251
252        fn synthesize(
253            &self,
254            config: Self::Config,
255            mut layouter: impl Layouter<F>,
256        ) -> Result<(), Error> {
257            let chip = BitwiseChip::new_from_scratch(&config);
258
259            // y does not apply in tests of arity-1 functions.
260            let y_idx = min(self.inputs.len() - 1, 1);
261            let x = chip.assign(&mut layouter, Value::known(self.inputs[0]))?;
262            let y = chip.assign(&mut layouter, Value::known(self.inputs[y_idx]))?;
263
264            cost_measure_start(&mut layouter);
265            let res = match self.operation {
266                Operation::Band => chip.band(&mut layouter, &x, &y, self.n),
267                Operation::Bor => chip.bor(&mut layouter, &x, &y, self.n),
268                Operation::Bxor => chip.bxor(&mut layouter, &x, &y, self.n),
269                Operation::Bnot => chip.bnot(&mut layouter, &x, self.n),
270            }?;
271            cost_measure_end(&mut layouter);
272
273            chip.assert_equal_to_fixed(&mut layouter, &res, self.expected)?;
274
275            chip.load_from_scratch(&mut layouter)
276        }
277    }
278
279    #[allow(clippy::too_many_arguments)]
280    fn run<F, Assigned, BitwiseChip>(
281        inputs: &[Assigned::Element],
282        expected: &Assigned::Element,
283        n: usize,
284        operation: Operation,
285        must_pass: bool,
286        cost_model: bool,
287        circuit_name: &str,
288        op_name: &str,
289    ) where
290        F: CircuitField + FromUniformBytes<64> + Ord,
291        Assigned: Instantiable<F> + InnerConstants + Clone,
292        Assigned::Element: CircuitField,
293        BitwiseChip: BitwiseInstructions<F, Assigned> + FromScratch<F>,
294    {
295        let circuit = TestCircuit::<F, Assigned, BitwiseChip> {
296            inputs: inputs.to_vec(),
297            expected: *expected,
298            n,
299            operation,
300            _marker: PhantomData,
301        };
302        let public_inputs = vec![vec![], vec![]];
303        match MockProver::run(&circuit, public_inputs) {
304            Ok(prover) => match prover.verify() {
305                Ok(()) => assert!(must_pass),
306                Err(e) => assert!(!must_pass, "Failed verifier with error {e:?}"),
307            },
308            Err(e) => assert!(!must_pass, "Failed prover with error {e:?}"),
309        }
310
311        if cost_model {
312            circuit_to_json(circuit_name, op_name, circuit);
313        }
314    }
315
316    pub fn test_band<F, Assigned, BitwiseChip>(name: &str)
317    where
318        F: CircuitField + FromUniformBytes<64> + Ord,
319        Assigned: Instantiable<F> + InnerConstants + Clone,
320        Assigned::Element: CircuitField + From<u64>,
321        BitwiseChip: BitwiseInstructions<F, Assigned> + FromScratch<F>,
322    {
323        let mut rng = ChaCha8Rng::seed_from_u64(0xc0ffee);
324        let r = rng.next_u64();
325        let s = rng.next_u64();
326        let mut cost_model = true;
327        [
328            (r, r, r, true),
329            (r, r, 0, false),
330            (r, s, r & s, true),
331            (0, 0, 0, true),
332            (1, 1, 1, true),
333            (5, 7, 5, true),
334            (5, 2, 0, true),
335            (0, 0, 1, false),
336        ]
337        .iter()
338        .for_each(|(x, y, z, must_pass)| {
339            let inputs = [Assigned::Element::from(*x), Assigned::Element::from(*y)];
340            let expected = Assigned::Element::from(*z);
341            run::<F, Assigned, BitwiseChip>(
342                &inputs,
343                &expected,
344                64,
345                Operation::Band,
346                *must_pass,
347                cost_model,
348                name,
349                "band",
350            );
351            cost_model = false;
352        });
353        let ten = Assigned::Element::from(10);
354        run::<F, Assigned, BitwiseChip>(
355            &[ten, ten],
356            &ten,
357            3,
358            Operation::Band,
359            false,
360            cost_model,
361            "",
362            "",
363        );
364    }
365
366    pub fn test_bor<F, Assigned, BitwiseChip>(name: &str)
367    where
368        F: CircuitField + FromUniformBytes<64> + Ord,
369        Assigned: Instantiable<F> + InnerConstants + Clone,
370        Assigned::Element: CircuitField + From<u64>,
371        BitwiseChip: BitwiseInstructions<F, Assigned> + FromScratch<F>,
372    {
373        let mut rng = ChaCha8Rng::seed_from_u64(0xc0ffee);
374        let r = rng.next_u64();
375        let s = rng.next_u64();
376        let mut cost_model = true;
377        [
378            (r, r, r, true),
379            (r, r, 0, false),
380            (r, s, r | s, true),
381            (0, 0, 0, true),
382            (1, 1, 1, true),
383            (5, 7, 7, true),
384            (5, 2, 7, true),
385            (0, 0, 1, false),
386        ]
387        .iter()
388        .for_each(|(x, y, z, must_pass)| {
389            let inputs = [Assigned::Element::from(*x), Assigned::Element::from(*y)];
390            let expected = Assigned::Element::from(*z);
391            run::<F, Assigned, BitwiseChip>(
392                &inputs,
393                &expected,
394                64,
395                Operation::Bor,
396                *must_pass,
397                cost_model,
398                name,
399                "bor",
400            );
401            cost_model = false;
402        });
403        let ten = Assigned::Element::from(10);
404        run::<F, Assigned, BitwiseChip>(&[ten, ten], &ten, 3, Operation::Bor, false, false, "", "");
405    }
406
407    pub fn test_bxor<F, Assigned, BitwiseChip>(name: &str)
408    where
409        F: CircuitField + FromUniformBytes<64> + Ord,
410        Assigned: Instantiable<F> + InnerConstants + Clone,
411        Assigned::Element: CircuitField + From<u64>,
412        BitwiseChip: BitwiseInstructions<F, Assigned> + FromScratch<F>,
413    {
414        let mut rng = ChaCha8Rng::seed_from_u64(0xc0ffee);
415        let r = rng.next_u64();
416        let s = rng.next_u64();
417        let mut cost_model = true;
418        [
419            (r, r, r, false),
420            (r, r, 0, true),
421            (r, s, r ^ s, true),
422            (0, 0, 0, true),
423            (1, 1, 0, true),
424            (5, 7, 2, true),
425            (5, 2, 7, true),
426            (0, 0, 1, false),
427        ]
428        .iter()
429        .for_each(|(x, y, z, must_pass)| {
430            let inputs = [Assigned::Element::from(*x), Assigned::Element::from(*y)];
431            let expected = Assigned::Element::from(*z);
432            run::<F, Assigned, BitwiseChip>(
433                &inputs,
434                &expected,
435                64,
436                Operation::Bxor,
437                *must_pass,
438                cost_model,
439                name,
440                "bxor",
441            );
442            cost_model = false;
443        });
444        let zero = Assigned::Element::from(0);
445        let ten = Assigned::Element::from(10);
446        run::<F, Assigned, BitwiseChip>(
447            &[ten, ten],
448            &zero,
449            3,
450            Operation::Bxor,
451            false,
452            false,
453            "",
454            "",
455        );
456    }
457
458    pub fn test_bnot<F, Assigned, BitwiseChip>(name: &str)
459    where
460        F: CircuitField + FromUniformBytes<64> + Ord,
461        Assigned: Instantiable<F> + InnerConstants + Clone,
462        Assigned::Element: CircuitField + From<u64>,
463        BitwiseChip: BitwiseInstructions<F, Assigned> + FromScratch<F>,
464    {
465        let mut rng = ChaCha8Rng::seed_from_u64(0xc0ffee);
466        let r = rng.next_u64();
467        let mut cost_model = true;
468        [
469            (r, !r, true, 64),
470            (r, !r + 1, false, 64),
471            (0, 7, true, 3),
472            (1, 6, true, 3),
473            (2, 5, true, 3),
474            (5, 2, true, 3),
475            (0, 1, false, 3),
476        ]
477        .iter()
478        .for_each(|(x, z, must_pass, n)| {
479            let inputs = [Assigned::Element::from(*x)];
480            let expected = Assigned::Element::from(*z);
481            run::<F, Assigned, BitwiseChip>(
482                &inputs,
483                &expected,
484                *n,
485                Operation::Bnot,
486                *must_pass,
487                cost_model,
488                name,
489                "bnot",
490            );
491            cost_model = false;
492        });
493        let mone = -Assigned::Element::from(1);
494        let eight = Assigned::Element::from(8);
495        run::<F, Assigned, BitwiseChip>(&[eight], &mone, 3, Operation::Bnot, false, false, "", "");
496    }
497}
midnight_circuits/instructions/bitwise.rs

midnight_circuits/instructions/
bitwise.rs
