From d4deed735c15126ebb4f4ed11071ca5d19b4f24d Mon Sep 17 00:00:00 2001 From: Ayush Shukla Date: Sat, 25 Nov 2023 23:53:56 +0100 Subject: [PATCH] feat: add limbs_to_num function --- halo2-base/src/gates/range/mod.rs | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/halo2-base/src/gates/range/mod.rs b/halo2-base/src/gates/range/mod.rs index 7f99c20e..2172af5f 100644 --- a/halo2-base/src/gates/range/mod.rs +++ b/halo2-base/src/gates/range/mod.rs @@ -450,6 +450,37 @@ pub trait RangeInstructions { limbs_le } + /// Reconstructs a field element from `limbs` in **little** endian with each `limb` having + /// `limb_bits` bits and constrains the reconstruction holds. Returns the number. + /// More precisely, checks that: + /// ```ignore + /// num = sum_{i=0}^{num_limbs-1} limbs[i] * 2^{i * limb_bits} + /// ``` + /// + /// Assumes 'limbs' contains valid limbs of at most limb_bits size. + /// NOTE: There might be multiple `limbs` that represent the same number. eg. x and x + p. + /// Better to range check `limbs` before calling this function. + fn limbs_to_num( + &self, + ctx: &mut Context, + limbs: &[AssignedValue], + limb_bits: usize, + ) -> AssignedValue + where + F: BigPrimeField, + { + self.gate().inner_product( + ctx, + limbs.iter().map(|x| *x), + self.gate() + .pow_of_two() + .iter() + .step_by(limb_bits) + .take(limbs.len()) + .map(|x| Constant(*x)), + ) + } + /// 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.