From fe3daacdee90e4e3e129e7caddde739afe093653 Mon Sep 17 00:00:00 2001
From: Jonathan Wang <31040440+jonathanpwang@users.noreply.github.com>
Date: Fri, 24 Nov 2023 18:22:52 -0500
Subject: [PATCH] feat: add `decompose_le` to `RangeInstructions`

---
 halo2-base/src/gates/range/mod.rs            | 40 +++++++++++++++++++-
 halo2-base/src/gates/tests/range.rs          |  8 ++++
 halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs |  1 -
 3 files changed, 46 insertions(+), 3 deletions(-)

diff --git a/halo2-base/src/gates/range/mod.rs b/halo2-base/src/gates/range/mod.rs
index 0222cde1..359acec4 100644
--- a/halo2-base/src/gates/range/mod.rs
+++ b/halo2-base/src/gates/range/mod.rs
@@ -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,
@@ -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.
diff --git a/halo2-base/src/gates/tests/range.rs b/halo2-base/src/gates/tests/range.rs
index d477d3f2..9a7229cb 100644
--- a/halo2-base/src/gates/tests/range.rs
+++ b/halo2-base/src/gates/tests/range.rs
@@ -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()
+    })
+}
diff --git a/halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs b/halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs
index 46bb6481..44873850 100644
--- a/halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs
+++ b/halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs
@@ -1,5 +1,4 @@
 #![allow(non_snake_case)]
-use crate::ff::Field as _;
 use crate::halo2_proofs::{
     arithmetic::CurveAffine,
     halo2curves::secp256k1::{Fq, Secp256k1Affine},