midnight_circuits/instructions/
division.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//! Integer division and moduli instructions interface.
15//!
16//! It provides instructions for computing quotient and remidners between
17//! bounded integers that fit in the native field.
18
19use midnight_proofs::{circuit::Layouter, plonk::Error};
20use num_bigint::BigUint;
21use num_integer::Integer;
22use num_traits::{One, Zero};
23
24use crate::{
25    instructions::{ArithInstructions, RangeCheckInstructions},
26    types::InnerValue,
27    utils::util::big_to_fe,
28    CircuitField,
29};
30
31/// Set of circuit instructions for integer division.
32pub trait DivisionInstructions<F, Assigned>:
33    ArithInstructions<F, Assigned> + RangeCheckInstructions<F, Assigned>
34where
35    F: CircuitField,
36    Assigned: InnerValue,
37    Assigned::Element: CircuitField,
38{
39    /// Integer division by a constant.
40    ///
41    /// This trait is implemented with respect to an Assigned type whose inner
42    /// value has an integer structure (enforced by requiring `CircuitField`).
43    ///
44    /// Given a `dividend` as an assigned element (interpreted as an integer),
45    /// and a constant `divisor`, returns the quotient and remainder of
46    /// dividing the former by the latter, as integers.
47    ///
48    /// An optional (inclusive) upper bound can be provided on the value of
49    /// the `dividend`. It is the responsibility of the caller that, if
50    /// provided, the bound on the dividend be valid.
51    ///
52    /// # Panics
53    ///  - If `divisor = 0`.
54    ///  - If `divisor > dividend_bound` when the bound is provided or if
55    ///    `divisor` is greater than or equal to the maximum value that an
56    ///    `Assigned::Element` can take.
57    ///
58    /// ```
59    /// # midnight_circuits::run_test_native_gadget!(chip, layouter, {
60    /// let x = chip.assign(&mut layouter, Value::known(F::from(17)))?;
61    ///
62    /// let (q, r) = chip.div_rem(&mut layouter, &x, 5u64.into(), None)?;
63    /// chip.assert_equal_to_fixed(&mut layouter, &q, F::from(3))?;
64    /// chip.assert_equal_to_fixed(&mut layouter, &r, F::from(2))?;
65    /// # });
66    /// ```
67    fn div_rem(
68        &self,
69        layouter: &mut impl Layouter<F>,
70        dividend: &Assigned,
71        divisor: BigUint,
72        dividend_bound: Option<BigUint>,
73    ) -> Result<(Assigned, Assigned), Error> {
74        if divisor == BigUint::one() {
75            return Ok((
76                dividend.clone(),
77                self.assign_fixed(layouter, Assigned::Element::from(0))?,
78            ));
79        }
80
81        let dividend_bound = dividend_bound.unwrap_or((-Assigned::Element::from(1)).to_biguint());
82        assert!(divisor > BigUint::zero());
83        assert!(divisor <= dividend_bound);
84
85        let (q, r) = dividend
86            .value()
87            .map(|v| {
88                let (q, r) = v.to_biguint().div_rem(&divisor);
89                (big_to_fe(q), big_to_fe(r))
90            })
91            .unzip();
92
93        let q_strict_bound = (dividend_bound / &divisor) + BigUint::one();
94
95        let r = self.assign_lower_than_fixed(layouter, r, &divisor)?;
96        let q = self.assign_lower_than_fixed(layouter, q, &q_strict_bound)?;
97
98        let sum = self.linear_combination(
99            layouter,
100            &[
101                (big_to_fe(divisor), q.clone()),
102                (Assigned::Element::from(1), r.clone()),
103            ],
104            Assigned::Element::from(0),
105        )?;
106        self.assert_equal(layouter, dividend, &sum)?;
107
108        Ok((q, r))
109    }
110
111    /// Integer modulo operation.
112    ///
113    /// This trait is implemented with respect to an Assigned type whose inner
114    /// value has an integer structure (enforced by requiring `CircuitField`).
115    ///
116    /// Given an `input` as an assigned element (interpreted as an integer
117    /// bounded by `bound`), and a constant `modulus`, returns the remainder of
118    /// dividing the former by the latter, as integers.
119    ///
120    /// An optional (inclusive) upper bound can be provided on the value of
121    /// the `input`. It is the responsibility of the caller that, if
122    /// provided, the bound on the input be valid.
123    ///
124    /// # Panics
125    ///  - If `modulus = 0`.
126    ///  - If `modulus > input_bound` when the bound is provided or if `modulus`
127    ///    is greater than or equal to the maximum value that an
128    ///    `Assigned::Element` can take.
129    ///
130    /// ```
131    /// # midnight_circuits::run_test_native_gadget!(chip, layouter, {
132    /// let x = chip.assign(&mut layouter, Value::known(F::from(17)))?;
133    ///
134    /// let r = chip.rem(&mut layouter, &x, 5u64.into(), None)?;
135    /// chip.assert_equal_to_fixed(&mut layouter, &r, F::from(2))?;
136    /// # });
137    /// ```
138    fn rem(
139        &self,
140        layouter: &mut impl Layouter<F>,
141        input: &Assigned,
142        modulus: BigUint,
143        input_bound: Option<BigUint>,
144    ) -> Result<Assigned, Error> {
145        self.div_rem(layouter, input, modulus, input_bound).map(|(_, r)| r)
146    }
147}
148
149#[cfg(test)]
150pub(crate) mod tests {
151    use std::marker::PhantomData;
152
153    use ff::FromUniformBytes;
154    use midnight_proofs::{
155        circuit::{SimpleFloorPlanner, Value},
156        dev::MockProver,
157        plonk::{Circuit, ConstraintSystem},
158    };
159
160    use super::*;
161    use crate::{
162        testing_utils::FromScratch,
163        types::InnerValue,
164        utils::circuit_modeling::{circuit_to_json, cost_measure_end, cost_measure_start},
165    };
166
167    struct TestCircuit<F, Assigned, DivChip>
168    where
169        Assigned: InnerValue,
170    {
171        dividend: Value<Assigned::Element>,
172        divisor: BigUint,
173        expected: (Assigned::Element, Assigned::Element),
174        _marker: PhantomData<(F, DivChip)>,
175    }
176
177    impl<F, Assigned, DivChip> Circuit<F> for TestCircuit<F, Assigned, DivChip>
178    where
179        F: CircuitField,
180        Assigned: InnerValue,
181        Assigned::Element: CircuitField,
182        DivChip: DivisionInstructions<F, Assigned> + FromScratch<F>,
183    {
184        type Config = <DivChip as FromScratch<F>>::Config;
185
186        type FloorPlanner = SimpleFloorPlanner;
187
188        type Params = ();
189
190        fn without_witnesses(&self) -> Self {
191            unreachable!();
192        }
193
194        fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
195            let committed_instance_column = meta.instance_column();
196            let instance_column = meta.instance_column();
197            DivChip::configure_from_scratch(
198                meta,
199                &mut vec![],
200                &mut vec![],
201                &[committed_instance_column, instance_column],
202            )
203        }
204
205        fn synthesize(
206            &self,
207            config: Self::Config,
208            mut layouter: impl Layouter<F>,
209        ) -> Result<(), Error> {
210            let chip = DivChip::new_from_scratch(&config);
211
212            let x = chip.assign(&mut layouter, self.dividend)?;
213            cost_measure_start(&mut layouter);
214            let (q, r) = chip.div_rem(&mut layouter, &x, self.divisor.clone(), None)?;
215            cost_measure_end(&mut layouter);
216
217            chip.assert_equal_to_fixed(&mut layouter, &q, self.expected.0)?;
218            chip.assert_equal_to_fixed(&mut layouter, &r, self.expected.1)?;
219
220            chip.load_from_scratch(&mut layouter)
221        }
222    }
223
224    fn run<F, Assigned, DivChip>(
225        dividend: Assigned::Element,
226        divisor: BigUint,
227        expected: (Assigned::Element, Assigned::Element),
228        must_pass: bool,
229        cost_model: bool,
230        chip_name: &str,
231    ) where
232        F: CircuitField + FromUniformBytes<64> + Ord,
233        Assigned: InnerValue,
234        Assigned::Element: CircuitField,
235        DivChip: DivisionInstructions<F, Assigned> + FromScratch<F>,
236    {
237        let circuit = TestCircuit::<F, Assigned, DivChip> {
238            dividend: Value::known(dividend),
239            divisor,
240            expected,
241            _marker: PhantomData,
242        };
243
244        let public_inputs = vec![vec![], vec![]];
245        match MockProver::run(&circuit, public_inputs) {
246            Ok(prover) => match prover.verify() {
247                Ok(()) => assert!(must_pass),
248                Err(e) => assert!(!must_pass, "Failed verifier with error {e:?}"),
249            },
250            Err(e) => assert!(!must_pass, "Failed prover with error {e:?}"),
251        }
252
253        if cost_model {
254            circuit_to_json(chip_name, "div_rem", circuit);
255        }
256    }
257
258    pub fn test_div_rem<F, Assigned, DivChip>(chip_name: &str)
259    where
260        F: CircuitField + FromUniformBytes<64> + Ord,
261        Assigned: InnerValue,
262        Assigned::Element: CircuitField,
263        DivChip: DivisionInstructions<F, Assigned> + FromScratch<F>,
264    {
265        [
266            (17, 5, (3, 2), true),
267            (0, 1, (0, 0), true),
268            (1, 1, (1, 0), true),
269            (100, 5, (20, 0), true),
270            (100, 7, (14, 2), true),
271            (1 << 13, 1, (1 << 13, 0), true),
272        ]
273        .into_iter()
274        .enumerate()
275        .for_each(|(i, (dividend, divisor, (q, r), must_pass))| {
276            run::<F, Assigned, DivChip>(
277                Assigned::Element::from(dividend),
278                BigUint::from(divisor as u64),
279                (Assigned::Element::from(q), Assigned::Element::from(r)),
280                must_pass,
281                i == 0,
282                chip_name,
283            )
284        });
285
286        let zero = BigUint::from(0u64);
287        let one = BigUint::from(1u64);
288        let two = BigUint::from(2u64);
289        let max = (-Assigned::Element::from(1)).to_biguint();
290
291        [
292            (&max, &(&max - &one), (&one, &one), true),
293            (&(&max + &one), &(&max - &one), (&one, &two), false),
294            (&(&max + &one), &(&max - &one), (&zero, &zero), true),
295        ]
296        .into_iter()
297        .for_each(|(dividend, divisor, (q, r), must_pass)| {
298            run::<F, Assigned, DivChip>(
299                big_to_fe(dividend.clone()),
300                divisor.clone(),
301                (big_to_fe(q.clone()), big_to_fe(r.clone())),
302                must_pass,
303                false,
304                chip_name,
305            )
306        });
307    }
308}
midnight_circuits/instructions/division.rs

midnight_circuits/instructions/
division.rs
