Merge pull request #503 from o1-labs/fix/uint-lt-gt

Fix Uint comparisons and division

src/examples/simple_zkapp.ts

@@ -65,10 +65,7 @@ class SimpleZkapp extends SmartContract {
     // pay out half of the zkapp balance to the caller
     let balance = this.account.balance.get();
     this.account.balance.assertEquals(balance);
-    // FIXME UInt64.div() doesn't work on variables
-    let halfBalance = Circuit.witness(UInt64, () =>
-      balance.toConstant().div(2)
-    );
+    let halfBalance = balance.div(2);
     this.send({ to: callerAccountUpdate, amount: halfBalance });
 
     // emit some events

src/examples/zkapps/dex/dex.ts

@@ -71,10 +71,8 @@ function createDex({
       // // assert dy == [dx * y/x], or x == 0
       let isXZero = dexXBalance.equals(UInt64.zero);
       let xSafe = Circuit.if(isXZero, UInt64.one, dexXBalance);
-
-      // FIXME
-      // Error: Constraint unsatisfied (unreduced): Equal 0 1
-      dy.equals(dx.mul(dexYBalance).div(xSafe)).or(isXZero).assertTrue();
+      let isDyCorrect = dy.equals(dx.mul(dexYBalance).div(xSafe));
+      isDyCorrect.or(isXZero).assertTrue();
 
       tokenX.transfer(user, this.address, dx);
       tokenY.transfer(user, this.address, dy);

src/examples/zkapps/simple_and_counter_zkapp.ts

@@ -133,10 +133,7 @@ class SimpleZkapp extends SmartContract {
     // pay out half of the zkapp balance to the caller
     let balance = this.account.balance.get();
     this.account.balance.assertEquals(balance);
-    // FIXME UInt64.div() doesn't work on variables
-    let halfBalance = Circuit.witness(UInt64, () =>
-      balance.toConstant().div(2)
-    );
+    let halfBalance = balance.div(2);
     this.balance.subInPlace(halfBalance);
     callerAccountUpdate.balance.addInPlace(halfBalance);
 

src/lib/int.ts

@@ -155,12 +155,13 @@ class UInt64 extends CircuitValue {
       return Bool(this.value.toBigInt() <= y.value.toBigInt());
     } else {
       let xMinusY = this.value.sub(y.value).seal();
+      let yMinusX = xMinusY.neg();
       let xMinusYFits = xMinusY
         .rangeCheckHelper(UInt64.NUM_BITS)
         .equals(xMinusY);
-      let yMinusXFits = xMinusY
+      let yMinusXFits = yMinusX
         .rangeCheckHelper(UInt64.NUM_BITS)
-        .equals(xMinusY.neg());
+        .equals(yMinusX);
       xMinusYFits.or(yMinusXFits).assertEquals(true);
       // x <= y if y - x fits in 64 bits
       return yMinusXFits;
@@ -329,12 +330,13 @@ class UInt32 extends CircuitValue {
       return Bool(this.value.toBigInt() <= y.value.toBigInt());
     } else {
       let xMinusY = this.value.sub(y.value).seal();
+      let yMinusX = xMinusY.neg();
       let xMinusYFits = xMinusY
         .rangeCheckHelper(UInt32.NUM_BITS)
         .equals(xMinusY);
-      let yMinusXFits = xMinusY
+      let yMinusXFits = yMinusX
         .rangeCheckHelper(UInt32.NUM_BITS)
-        .equals(xMinusY.neg());
+        .equals(yMinusX);
       xMinusYFits.or(yMinusXFits).assertEquals(true);
       // x <= y if y - x fits in 64 bits
       return yMinusXFits;

src/lib/primitives.unit-test.ts

@@ -0,0 +1,23 @@
+import { Circuit, circuitMain } from './circuit_value.js';
+import { isReady } from '../snarky.js';
+import { UInt64, UInt32 } from './int.js';
+import { expect } from 'expect';
+
+class Primitives extends Circuit {
+  @circuitMain
+  static main() {
+    // division
+    let x64 = Circuit.witness(UInt64, () => UInt64.from(10));
+    x64.div(2).assertEquals(UInt64.from(5));
+    let x32 = Circuit.witness(UInt32, () => UInt32.from(15));
+    x32.div(4).assertEquals(UInt32.from(3));
+  }
+}
+
+await isReady;
+let keypair = Primitives.generateKeypair();
+let proof = Primitives.prove([], [], keypair);
+let ok = Primitives.verify([], keypair.verificationKey(), proof);
+expect(ok).toEqual(true);
+
+console.log('primitive operations in the circuit are working! 🎉');