halo2_ecc/bigint/
big_is_zero.rs

1use super::{OverflowInteger, ProperCrtUint, ProperUint};
2use halo2_base::{gates::GateInstructions, utils::ScalarField, AssignedValue, Context};
3
4/// # Assumptions
5/// * `a` has nonzero number of limbs
6/// * The limbs of `a` are all in [0, 2<sup>a.max_limb_bits</sup>)
7/// * a.limbs.len() * 2<sup>a.max_limb_bits</sup> ` is less than modulus of `F`
8pub fn positive<F: ScalarField>(
9    gate: &impl GateInstructions<F>,
10    ctx: &mut Context<F>,
11    a: OverflowInteger<F>,
12) -> AssignedValue<F> {
13    let k = a.limbs.len();
14    assert_ne!(k, 0);
15    assert!(a.max_limb_bits as u32 + k.ilog2() < F::CAPACITY);
16
17    let sum = gate.sum(ctx, a.limbs);
18    gate.is_zero(ctx, sum)
19}
20
21/// Given `ProperUint<F>` `a`, returns 1 iff every limb of `a` is zero. Returns 0 otherwise.
22///
23/// It is almost always more efficient to use [`positive`] instead.
24///
25/// # Assumptions
26/// * `a` has nonzero number of limbs
27pub fn assign<F: ScalarField>(
28    gate: &impl GateInstructions<F>,
29    ctx: &mut Context<F>,
30    a: ProperUint<F>,
31) -> AssignedValue<F> {
32    assert!(!a.0.is_empty());
33
34    let mut a_limbs = a.0.into_iter();
35    let mut partial = gate.is_zero(ctx, a_limbs.next().unwrap());
36    for a_limb in a_limbs {
37        let limb_is_zero = gate.is_zero(ctx, a_limb);
38        partial = gate.and(ctx, limb_is_zero, partial);
39    }
40    partial
41}
42
43/// Returns 0 or 1. Returns 1 iff the limbs of `a` are identically zero.
44/// This just calls [`assign`] on the limbs.
45///
46/// It is almost always more efficient to use [`positive`] instead.
47pub fn crt<F: ScalarField>(
48    gate: &impl GateInstructions<F>,
49    ctx: &mut Context<F>,
50    a: ProperCrtUint<F>,
51) -> AssignedValue<F> {
52    assign(gate, ctx, ProperUint(a.0.truncation.limbs))
53}