halo2_ecc/bigint/
sub.rs

Help
1use super::{CRTInteger, OverflowInteger, ProperCrtUint, ProperUint};
2use halo2_base::{
3    gates::{GateInstructions, RangeInstructions},
4    utils::ScalarField,
5    AssignedValue, Context,
6    QuantumCell::{Constant, Existing, Witness},
7};
8use itertools::Itertools;
9
10/// # Assumptions
11/// * Should only be called on integers a, b in proper representation with all limbs having at most `limb_bits` number of bits
12/// * `a, b` have same nonzero number of limbs
13pub fn assign<F: ScalarField>(
14    range: &impl RangeInstructions<F>,
15    ctx: &mut Context<F>,
16    a: impl Into<ProperUint<F>>,
17    b: impl Into<ProperUint<F>>,
18    limb_bits: usize,
19    limb_base: F,
20) -> (OverflowInteger<F>, AssignedValue<F>) {
21    let a = a.into();
22    let b = b.into();
23    let k = a.0.len();
24    let mut out_limbs = Vec::with_capacity(k);
25
26    let mut borrow: Option<AssignedValue<F>> = None;
27    for (a_limb, b_limb) in a.0.into_iter().zip_eq(b.0) {
28        let (bottom, lt) = match borrow {
29            None => {
30                let lt = range.is_less_than(ctx, a_limb, b_limb, limb_bits);
31                (b_limb, lt)
32            }
33            Some(borrow) => {
34                let b_plus_borrow = range.gate().add(ctx, b_limb, borrow);
35                let lt = range.is_less_than(ctx, a_limb, b_plus_borrow, limb_bits + 1);
36                (b_plus_borrow, lt)
37            }
38        };
39        let out_limb = {
40            // | a | lt | 2^n | a + lt * 2^n | -1 | bottom | a + lt * 2^n - bottom
41            let a_with_borrow_val = limb_base * lt.value() + a_limb.value();
42            let out_val = a_with_borrow_val - bottom.value();
43            ctx.assign_region_last(
44                [
45                    Existing(a_limb),
46                    Existing(lt),
47                    Constant(limb_base),
48                    Witness(a_with_borrow_val),
49                    Constant(-F::ONE),
50                    Existing(bottom),
51                    Witness(out_val),
52                ],
53                [0, 3],
54            )
55        };
56        out_limbs.push(out_limb);
57        borrow = Some(lt);
58    }
59    (OverflowInteger::new(out_limbs, limb_bits), borrow.unwrap())
60}
61
62// returns (a-b, underflow), where underflow is nonzero iff a < b
63/// # Assumptions
64/// * `a, b` are proper CRT representations of integers with the same number of limbs
65pub fn crt<F: ScalarField>(
66    range: &impl RangeInstructions<F>,
67    ctx: &mut Context<F>,
68    a: ProperCrtUint<F>,
69    b: ProperCrtUint<F>,
70    limb_bits: usize,
71    limb_base: F,
72) -> (CRTInteger<F>, AssignedValue<F>) {
73    let out_native = range.gate().sub(ctx, a.0.native, b.0.native);
74    let a_limbs = ProperUint(a.0.truncation.limbs);
75    let b_limbs = ProperUint(b.0.truncation.limbs);
76    let (out_trunc, underflow) = assign(range, ctx, a_limbs, b_limbs, limb_bits, limb_base);
77    let out_val = a.0.value - b.0.value;
78    (CRTInteger::new(out_trunc, out_native, out_val), underflow)
79}
halo2_ecc/bigint/sub.rs

halo2_ecc/bigint/
sub.rs
