Skip to content

Commit

Permalink
feat: add decompose_le to RangeInstructions
Browse files Browse the repository at this point in the history
  • Loading branch information
jonathanpwang committed Nov 24, 2023
1 parent df81d82 commit fe3daac
Show file tree
Hide file tree
Showing 3 changed files with 46 additions and 3 deletions.
40 changes: 38 additions & 2 deletions halo2-base/src/gates/range/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@ use crate::{
poly::Rotation,
},
utils::{
biguint_to_fe, bit_length, decompose_fe_to_u64_limbs, fe_to_biguint, BigPrimeField,
ScalarField,
biguint_to_fe, bit_length, decompose, decompose_fe_to_u64_limbs, fe_to_biguint,
BigPrimeField, ScalarField,
},
virtual_region::lookups::LookupAnyManager,
AssignedValue, Context,
Expand Down Expand Up @@ -403,6 +403,42 @@ pub trait RangeInstructions<F: ScalarField> {
bit
}

/// Decomposes `num` into `num_limbs` limbs in **little** endian with each `limb` having `limb_bits` bits
/// and constrains the decomposition holds. Returns the limbs. More precisely, checks that:
/// ```ignore
/// num = sum_{i=0}^{num_limbs-1} limb[i] * 2^{i * limb_bits}
/// ```
///
/// ## Panics
/// Circuit constraints will fail if `num` cannot be decomposed into `num_limbs` limbs of `limb_bits` bits.
fn decompose_le(
&self,
ctx: &mut Context<F>,
num: AssignedValue<F>,
limb_bits: usize,
num_limbs: usize,
) -> Vec<AssignedValue<F>>
where
F: BigPrimeField,
{
// mostly copied from RangeChip::range_check
let pows = self
.gate()
.pow_of_two()
.iter()
.step_by(limb_bits)
.take(num_limbs)
.map(|x| Constant(*x));
let limb_vals = decompose(num.value(), num_limbs, limb_bits).into_iter().map(Witness);
let (acc, limbs_le) = self.gate().inner_product_left(ctx, limb_vals, pows);
ctx.constrain_equal(&acc, &num);

for limb in &limbs_le {
self.range_check(ctx, *limb, limb_bits);
}
limbs_le
}

/// Bitwise right rotate a by BIT bits. BIT and NUM_BITS must be determined at compile time.
///
/// Assumes 'a' is a NUM_BITS bit integer and 0 < NUM_BITS <= 128.
Expand Down
8 changes: 8 additions & 0 deletions halo2-base/src/gates/tests/range.rs
Original file line number Diff line number Diff line change
Expand Up @@ -106,3 +106,11 @@ pub fn test_div_mod_var(
(*a.0.value(), *a.1.value())
})
}

#[test_case(Fr::from(0x1234), 4, 4 => [0x4, 0x3, 0x2, 0x1].map(Fr::from).to_vec(); "decompose_le(0x1234, 4, 4)")]
pub fn test_decompose_le(num: Fr, limb_bits: usize, num_limbs: usize) -> Vec<Fr> {
base_test().run(|ctx, chip| {
let num = ctx.load_witness(num);
chip.decompose_le(ctx, num, limb_bits, num_limbs).iter().map(|x| *x.value()).collect()
})
}
1 change: 0 additions & 1 deletion halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
#![allow(non_snake_case)]
use crate::ff::Field as _;
use crate::halo2_proofs::{
arithmetic::CurveAffine,
halo2curves::secp256k1::{Fq, Secp256k1Affine},
Expand Down

0 comments on commit fe3daac

Please sign in to comment.