Add uint128 by aritkulova · Pull Request #21 · BlockstreamResearch/simplicityhl-std

aritkulova · 2026-07-07T21:47:34Z

No description provided.

added assert_eq_128

LesterEvSe · 2026-07-08T09:48:27Z

Okay, I see the problem with running the tests, they take a lot of time. I have been playing around with the code, and the main problem is that with match if_test_this_function(...) we run a lot of similar operations, and in fact, to reach, for example, assert_bool(is_zero_128(a), expected_bool);, we need to go through 10 checks beforehand.

For example, when I run code like this, simplex tests finishes in under 3s, compared to the current 45s:

fn main() {
    let fn_idx: u8 = witness::FUNCTION_INDEX;

    let a: u128 = witness::FIRST_ARG;
    let b: u128 = witness::SECOND_ARG;
    let expected: Option<u128> = witness::EXPECTED;

    let expected_bool: bool = witness::EXPECTED_BOOL;
    let second_expected: u128 = witness::SECOND_EXPECTED; // for cases where the result is a 256 bit value
    let third_expected: u128 = witness::THIRD_EXPECTED; // for cases where the result is 256 bit + 128 bit values

    match if_test_this_function(197, fn_idx) { true => { assert_bool(is_zero_128(a), expected_bool); }, false => (), };
}

Note: The same optimization is true for other operations as well. I checked this for fn_idx == 195.

I have two possible solutions:

We could split u128_test.simf into several smaller files. I think this would partially fix the problem of tests taking too long to run.
Another solution is to wait for feat: add enum declarations and multi-arm enum match expressions SimplicityHL#336 to be merged. Then we would have a multi-arm match block with an enum, and we could probably solve this problem that way too.

removed temporary helper

LesterEvSe

Please add tests for this optimization. Suggested cases: a_low == b_low, a_low - b_low == u64::MAX, and if possible a property test asserting q * b + r == a on randomized inputs

LesterEvSe · 2026-07-10T08:42:11Z

+
+    /// Bit logic
+
+    match if_test_this_function(192, fn_idx) { true => { assert!(eq_128(and_128(a, b), unwrap(expected))); }, false => (), };


Same problem with index here

LesterEvSe · 2026-07-10T08:43:47Z

+
+    /// Arithmetic
+
+    match if_test_this_function(192, fn_idx) { true => { assert_bool(is_zero_128(a), expected_bool); }, false => (), };


Let's start from 0 because a shift of 192 is redundant here. We need this within the scope of a single file, where we have the default operations from the uint_tests! macro, along with other custom functionality

LesterEvSe · 2026-07-10T11:14:55Z

+pub fn add_128_64(a: u128, b: u64) -> (bool, u128) {
+    let (a_high, a_low): (u64, u64) = <u128>::into(a);
+
+    let (carry, res_low): (bool, u64) = jet::add_64(a_low, b);
+
+    match carry {
+        true => {
+            let (carry, res_high): (bool, u64) = jet::add_64(a_high, 1);
+            let res: u128 = <(u64, u64)>::into((res_high, res_low));
+
+            (carry, res)
+        }, false => {
+            (carry,  <(u64, u64)>::into((a_high, res_low)))
+        }
+    }
+}


Suggested change

pub fn add_128_64(a: u128, b: u64) -> (bool, u128) {

let (a_high, a_low): (u64, u64) = <u128>::into(a);

let (carry, res_low): (bool, u64) = jet::add_64(a_low, b);

match carry {

true => {

let (carry, res_high): (bool, u64) = jet::add_64(a_high, 1);

let res: u128 = <(u64, u64)>::into((res_high, res_low));

(carry, res)

}, false => {

(carry, <(u64, u64)>::into((a_high, res_low)))

}

}

}

pub fn add_128_64(a: u128, b: u64) -> (bool, u128) {

let (a_high, a_low): (u64, u64) = <u128>::into(a);

let (carry_low, res_low): (bool, u64) = jet::add_64(a_low, b);

let (carry_high, res_high): (bool, u64) = jet::full_add_64(carry_low, a_high, 0);

(carry_high, <(u64, u64)>::into((res_high, res_low)))

}

LesterEvSe · 2026-07-10T11:15:33Z

+pub fn sub_128(a: u128, b: u128) -> (bool, u128) {
+    let (a_high, a_low): (u64, u64) = <u128>::into(a);
+    let (b_high, b_low): (u64, u64) = <u128>::into(b);
+
+    let (borrow_high, diff_high): (bool, u64) = jet::subtract_64(a_high, b_high);
+    let (borrow_low, diff_low): (bool, u64) = jet::subtract_64(a_low, b_low);
+
+    match borrow_low {
+        true => {
+            let (borrow, diff_high): (bool, u64) = jet::subtract_64(diff_high, 1);
+            let res: u128 = <(u64, u64)>::into((diff_high, diff_low));
+
+            let final_borrow: bool = or(borrow, borrow_high);
+
+            (final_borrow, res)
+        },
+        false => {
+            let res: u128 = <(u64, u64)>::into((diff_high, diff_low));
+
+            (borrow_high, res)
+        },
+    }
+}


Suggested change

pub fn sub_128(a: u128, b: u128) -> (bool, u128) {

let (a_high, a_low): (u64, u64) = <u128>::into(a);

let (b_high, b_low): (u64, u64) = <u128>::into(b);

let (borrow_high, diff_high): (bool, u64) = jet::subtract_64(a_high, b_high);

let (borrow_low, diff_low): (bool, u64) = jet::subtract_64(a_low, b_low);

match borrow_low {

true => {

let (borrow, diff_high): (bool, u64) = jet::subtract_64(diff_high, 1);

let res: u128 = <(u64, u64)>::into((diff_high, diff_low));

let final_borrow: bool = or(borrow, borrow_high);

(final_borrow, res)

},

false => {

let res: u128 = <(u64, u64)>::into((diff_high, diff_low));

(borrow_high, res)

},

}

}

pub fn sub_128(a: u128, b: u128) -> (bool, u128) {

let (a_high, a_low): (u64, u64) = <u128>::into(a);

let (b_high, b_low): (u64, u64) = <u128>::into(b);

let (borrow_low, diff_low): (bool, u64) = jet::subtract_64(a_low, b_low);

let (borrow_high, diff_high): (bool, u64) = jet::full_subtract_64(borrow_low, a_high, b_high);

let res: u128 = <(u64, u64)>::into((diff_high, diff_low));

(borrow_high, res)

}

LesterEvSe · 2026-07-10T11:17:03Z

+pub fn checked_sub_128(a: u128, b: u128) -> Option<u128> {
+    let (borrow, diff): (bool, u128) = sub_128(a, b);
+    match borrow {
+        true => None,
+        false => Some(diff),
+    }
+}


I am following your style as defined by the checked_add_128 function

Suggested change

pub fn checked_sub_128(a: u128, b: u128) -> Option<u128> {

let (borrow, diff): (bool, u128) = sub_128(a, b);

match borrow {

true => None,

false => Some(diff),

}

}

pub fn checked_sub_128(a: u128, b: u128) -> Option<u128> {

let (borrow, diff): (bool, u128) = sub_128(a, b);

match borrow {

true => None,

false => Some(diff),

}

}

LesterEvSe · 2026-07-10T11:49:03Z

+    // a' = remainder * 2^64 + a_low
+    let a_prime: u128 = <(u64, u64)>::into((remainder, a_low));
+
+    // we need to normalize here, because jet::div_mod_128_64 only acceps b >= 2^63


Suggested change

// we need to normalize here, because jet::div_mod_128_64 only acceps b >= 2^63

// we need to normalize here, because jet::div_mod_128_64 only accepts b >= 2^63

LesterEvSe · 2026-07-10T11:49:46Z

+        false => {
+            match and(jet::is_zero_64(a_high), jet::is_zero_64(b_high)) { 
+                true => { 
+                    // if both a_high and b_high is equal to zero, this narrows down to 64-bit division


Suggested change

// if both a_high and b_high is equal to zero, this narrows down to 64-bit division

// if both a_high and b_high are zero, this narrows down to 64-bit division

LesterEvSe · 2026-07-10T11:56:28Z

+                },
+                false => {
+                    match jet::eq_64(a_high, b_high) {
+                        true => (1, <(u64, u64)>::into((0, safe_sub_64(a_low, b_low)))),


Suggested change

true => (1, <(u64, u64)>::into((0, safe_sub_64(a_low, b_low)))),

true => {

// Safe: !lt_128(a, b) and a_high == b_high implies a_low >= b_low,

// so the subtraction cannot underflow.

let (_, diff): (bool, u64) = jet::subtract_64(a_low, b_low);

(1, <(u64, u64)>::into((0, diff)))

},

LesterEvSe · 2026-07-10T12:00:40Z

+    (a_high, a_low)
+}
+
+mod u128_tests {


Splitting by module makes it easier to run a focused subset. u128_tests currently has 55 tests, which is a lot to run together.

Suggested change

mod u128_tests {

mod u128_tests_arithmetic {

LesterEvSe · 2026-07-10T12:03:22Z

+    }
+}
+
+mod u128_tests {


Suggested change

mod u128_tests {

mod u128_tests_bits {

aritkulova added 4 commits July 8, 2026 00:43

added functions for u128;

00241df

added assert_eq_128

added test for assert_eq_128

5d6f371

updated simplex version

a12c20e

fixed typo

4917be8

aritkulova requested a review from Hrom131 July 7, 2026 21:47

aritkulova self-assigned this Jul 7, 2026

fixed typo

18fd9e0

Hrom131 reviewed Jul 9, 2026

View reviewed changes

Comment thread simf/lib/u128.simf

Hrom131 reviewed Jul 9, 2026

View reviewed changes

Comment thread simf/lib/u128.simf

aritkulova added 3 commits July 9, 2026 14:59

optimized mul_128;

cae272f

removed temporary helper

divided tests for uint128 to speed up github ci

1fa9938

trying to optimize ci by running simplex tests on multiple threads

dd3611c

LesterEvSe requested changes Jul 10, 2026

View reviewed changes


		/// Bit logic

		match if_test_this_function(192, fn_idx) { true => { assert!(eq_128(and_128(a, b), unwrap(expected))); }, false => (), };


		/// Arithmetic

		match if_test_this_function(192, fn_idx) { true => { assert_bool(is_zero_128(a), expected_bool); }, false => (), };

	// we need to normalize here, because jet::div_mod_128_64 only acceps b >= 2^63
	// we need to normalize here, because jet::div_mod_128_64 only accepts b >= 2^63

	// if both a_high and b_high is equal to zero, this narrows down to 64-bit division
	// if both a_high and b_high are zero, this narrows down to 64-bit division

-                        true => (1, <(u64, u64)>::into((0, safe_sub_64(a_low, b_low)))),
+                        true => {
+                            // Safe: !lt_128(a, b) and a_high == b_high implies a_low >= b_low,
+                            // so the subtraction cannot underflow.
+                            let (_, diff): (bool, u64) = jet::subtract_64(a_low, b_low);
+                            (1, <(u64, u64)>::into((0, diff)))
+                        },

Uh oh!

Conversation

aritkulova commented Jul 7, 2026

Uh oh!

LesterEvSe commented Jul 8, 2026

Uh oh!

Uh oh!

Uh oh!

LesterEvSe left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants