From e274fcd630cb9aba9a607ef55886ee0fa02ef10b Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Tue, 26 Mar 2024 21:20:27 +0100
Subject: [PATCH] bigint assert less than or equal

---
 src/lib/provable/gadgets/foreign-field.ts | 28 +++++++++++++++++++++--
 src/lib/provable/gadgets/gadgets.ts       |  9 ++++++++
 2 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/src/lib/provable/gadgets/foreign-field.ts b/src/lib/provable/gadgets/foreign-field.ts
index 3109c0a61b..33840f30f4 100644
--- a/src/lib/provable/gadgets/foreign-field.ts
+++ b/src/lib/provable/gadgets/foreign-field.ts
@@ -61,6 +61,7 @@ const ForeignField = {
   assertAlmostReduced,
 
   assertLessThan,
+  assertLessThanOrEqual,
 
   equals,
 };
@@ -712,8 +713,10 @@ class Sum {
 // Field3 comparison
 
 function assertLessThan(x: Field3, y: bigint | Field3) {
-  if (typeof y === 'bigint')
-    assert(y > 0n, 'assertLessThan: upper bound must be positive');
+  assert(
+    typeof y !== 'bigint' || y > 0n,
+    'assertLessThan: upper bound must be positive'
+  );
   let y_ = Field3.from(y);
 
   // constant case
@@ -747,3 +750,24 @@ function assertLessThan(x: Field3, y: bigint | Field3) {
   // z = y - x - 1 - 0*(o1 + o2) for some overflows o1, o2
   sum([y_, x, Field3.from(1n)], [-1n, -1n], 0n);
 }
+
+function assertLessThanOrEqual(x: Field3, y: bigint | Field3) {
+  assert(
+    typeof y !== 'bigint' || y >= 0n,
+    'assertLessThanOrEqual: upper bound must be positive'
+  );
+  let y_ = Field3.from(y);
+
+  // constant case
+  if (Field3.isConstant(x) && Field3.isConstant(y_)) {
+    assert(
+      Field3.toBigint(x) <= Field3.toBigint(y_),
+      'assertLessThan: got x > y'
+    );
+    return;
+  }
+
+  // provable case
+  // we compute z = y - x and check that z \in [0, 2^3l), which implies x <= y
+  sum([y_, x], [-1n], 0n);
+}
diff --git a/src/lib/provable/gadgets/gadgets.ts b/src/lib/provable/gadgets/gadgets.ts
index 15c492f11b..6a67973693 100644
--- a/src/lib/provable/gadgets/gadgets.ts
+++ b/src/lib/provable/gadgets/gadgets.ts
@@ -764,6 +764,15 @@ const Gadgets = {
     assertLessThan(x: Field3, f: bigint | Field3) {
       ForeignField.assertLessThan(x, f);
     },
+
+    /**
+     * Prove that x <= f for any constant f < 2^264, or for another `Field3` f.
+     *
+     * See {@link ForeignField.assertLessThan} for details and usage examples.
+     */
+    assertLessThanOrEqual(x: Field3, f: bigint | Field3) {
+      ForeignField.assertLessThanOrEqual(x, f);
+    },
   },
 
   /**