feat: add function to convert from hi-lo to single AssignedValue (#39)

halo2-wasm/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "halo2-wasm"
-version = "0.2.7"
+version = "0.2.8"
 edition = "2021"
 
 [lib]

halo2-wasm/package.json

@@ -1,7 +1,7 @@
 {
   "name": "@axiom-crypto/halo2-wasm",
   "description": "Halo2 wasm bindings",
-  "version": "0.2.7",
+  "version": "0.2.8",
   "main": "index.js",
   "types": "index.d.ts",
   "scripts": {

halo2-wasm/src/halo2lib.rs

@@ -1,5 +1,5 @@
-use std::{cell::RefCell, str::FromStr};
 use std::rc::Rc;
+use std::{cell::RefCell, str::FromStr};
 
 use halo2_base::{
     gates::{
@@ -331,6 +331,11 @@ impl Halo2LibWasm {
         self.to_js_assigned_values(out)
     }
 
+    /// Returns a 256-bit hi-lo pair from a single CircuitValue
+    /// 
+    /// See `check_hi_lo` for what is constrained.
+    /// 
+    /// * `a`: the CircuitValue to split into hi-lo
     pub fn to_hi_lo(&mut self, a: usize) -> Vec<u32> {
         let a = self.get_assigned_value(a);
         let a_val = a.value();
@@ -346,27 +351,60 @@ impl Halo2LibWasm {
         let a_lo = self.builder.borrow_mut().main(0).load_witness(a_lo);
         let a_hi = self.builder.borrow_mut().main(0).load_witness(a_hi);
 
-        let (a_hi_max, a_lo_max) = modulus::<Fr>().div_mod_floor(&(BigUint::one() << 128));
+        let a_reconstructed = self.check_hi_lo(a_hi, a_lo);
 
-        //check a_hi < r // 2**128
-        let check_1 = self.range.is_big_less_than_safe(
-            self.builder.borrow_mut().main(0),
-            a_hi,
-            a_hi_max.clone(),
-        );
+        self.builder
+            .borrow_mut()
+            .main(0)
+            .constrain_equal(&a, &a_reconstructed);
 
-        //check (a_hi == r // 2 ** 128 AND a_lo < r % 2**128)
-        let a_hi_max_fe = biguint_to_fe::<Fr>(&a_hi_max);
-        let a_lo_max_fe = biguint_to_fe::<Fr>(&a_lo_max);
-        let check_2_hi = self.gate.is_equal(
+        let out = vec![a_hi, a_lo];
+        self.to_js_assigned_values(out)
+    }
+
+    /// Returns a single CircuitValue from a hi-lo pair
+    /// 
+    /// NOTE: this can fail if the hi-lo pair is greater than the Fr modulus.
+    /// See `check_hi_lo` for what is constrained.
+    /// 
+    /// * `hi`: the high 128 bits of the CircuitValue
+    /// * `lo`: the low 128 bits of the CircuitValue
+    pub fn from_hi_lo(&mut self, hi: usize, lo: usize) -> usize {
+        let hi = self.get_assigned_value(hi);
+        let lo = self.get_assigned_value(lo);
+
+        let out = self.check_hi_lo(hi, lo);
+
+        self.to_js_assigned_value(out)
+    }
+
+    /// Constrains and returns a single CircuitValue from a hi-lo pair
+    /// 
+    /// Constrains (hi < r // 2^128) OR (hi == r // 2^128 AND lo < r % 2^128)
+    /// * `hi`: the high 128 bits of the CircuitValue
+    /// * `lo`: the low 128 bits of the CircuitValue
+    fn check_hi_lo(&mut self, hi: AssignedValue<Fr>, lo: AssignedValue<Fr>) -> AssignedValue<Fr> {
+        let (hi_max, lo_max) = modulus::<Fr>().div_mod_floor(&(BigUint::one() << 128));
+
+        //check hi < r // 2**128
+        let check_1 =
+            self.range
+                .is_big_less_than_safe(self.builder.borrow_mut().main(0), hi, hi_max.clone());
+
+        //check (hi == r // 2 ** 128 AND lo < r % 2**128)
+        let hi_max_fe = biguint_to_fe::<Fr>(&hi_max);
+        let lo_max_fe = biguint_to_fe::<Fr>(&lo_max);
+        let check_2_hi =
+            self.gate
+                .is_equal(self.builder.borrow_mut().main(0), hi, Constant(hi_max_fe));
+        self.range
+            .range_check(self.builder.borrow_mut().main(0), lo, 128);
+        let check_2_lo = self.range.is_less_than(
             self.builder.borrow_mut().main(0),
-            a_hi,
-            Constant(a_hi_max_fe),
+            lo,
+            Constant(lo_max_fe),
+            128,
         );
-        self.range.range_check(self.builder.borrow_mut().main(0), a_lo, 128);
-        let check_2_lo =
-            self.range
-                .is_less_than(self.builder.borrow_mut().main(0), a_lo, Constant(a_lo_max_fe), 128);
         let check_2 = self
             .gate
             .and(self.builder.borrow_mut().main(0), check_2_hi, check_2_lo);
@@ -375,21 +413,16 @@ impl Halo2LibWasm {
         let check = self
             .gate
             .add(self.builder.borrow_mut().main(0), check_1, check_2);
-        self.gate.assert_is_const(self.builder.borrow_mut().main(0), &check, &Fr::one());
+        self.gate
+            .assert_is_const(self.builder.borrow_mut().main(0), &check, &Fr::one());
 
-        let a_reconstructed = self.gate.mul_add(
+        let combined = self.gate.mul_add(
             self.builder.borrow_mut().main(0),
-            a_hi,
+            hi,
             Constant(self.gate.pow_of_two()[128]),
-            a_lo,
+            lo,
         );
-        self.builder
-            .borrow_mut()
-            .main(0)
-            .constrain_equal(&a, &a_reconstructed);
-
-        let out = vec![a_hi, a_lo];
-        self.to_js_assigned_values(out)
+        combined
     }
 
     pub fn div_mod_var(&mut self, a: usize, b: usize, a_size: &str, b_size: &str) -> Vec<u32> {