zk/vm: Allow strict and loose checks for less_than.

bin/dao/daod/proof/dao-exec.zk

@@ -137,7 +137,7 @@ circuit "DaoExec" {
     # Check that dao_quorum is less than or equal to all_votes_value
     one = witness_base(1);
     all_votes_value_1 = base_add(all_votes_value, one);
-    less_than(dao_quorum, all_votes_value_1);
+    less_than_strict(dao_quorum, all_votes_value_1);
 
     # approval_ratio_quot / approval_ratio_base <= yes_votes / all_votes
     #
@@ -149,7 +149,7 @@ circuit "DaoExec" {
     lhs = base_mul(yes_votes_value, dao_approval_ratio_base);
 
     lhs_1 = base_add(lhs, one);
-    less_than(rhs, lhs_1);
+    less_than_strict(rhs, lhs_1);
     
     ####
 

bin/dao/daod/proof/dao-propose-main.zk

@@ -66,13 +66,13 @@ circuit "DaoProposeMain" {
 
     # Rangeproof check for proposal amount
     zero = witness_base(0);
-    less_than(zero, proposal_amount);
+    less_than_strict(zero, proposal_amount);
 
     # This is the main check
     # We check that dao_proposer_limit <= total_funds
     one = witness_base(1);
     total_funds_1 = base_add(total_funds, one);
-    less_than(dao_proposer_limit, total_funds_1);
+    less_than_strict(dao_proposer_limit, total_funds_1);
 
 	# Pedersen commitment for coin's value
 	vcv = ec_mul_short(total_funds, VALUE_COMMIT_VALUE);

contrib/zk.lua

@@ -41,9 +41,9 @@ local type = token(l.TYPE, word_match{
 local instruction = token('instruction', word_match{
   'ec_add', 'ec_mul', 'ec_mul_base', 'ec_mul_short',
   'ec_get_x', 'ec_get_y',
-  'base_add', 'base_mul', 'base_sub', 'greater_than',
+  'base_add', 'base_mul', 'base_sub',
   'poseidon_hash', 'merkle_root',
-  'range_check', 'less_than', 'bool_check',
+  'range_check', 'less_than_strict', 'less_than_loose', 'bool_check',
   'witness_base',
   'constrain_equal_base', 'constrain_equal_point',
   'constrain_instance',

contrib/zk.vim

@@ -23,7 +23,8 @@ syn keyword zkasInstruction
     \ ec_get_x ec_get_y
     \ base_add base_mul base_sub
     \ poseidon_hash merkle_root
-    \ range_check less_than bool_check witness_base
+    \ range_check less_than_strict less_than_loose  bool_check
+    \ witness_base
     \ constrain_equal_base constrain_equal_point
     \ constrain_instance
 

doc/src/zkas/bincode.md

@@ -165,7 +165,8 @@ TBD
 | `BaseSub`            | `Base` Subtraction.                                             |
 | `WitnessBase`        | Witness an unsigned integer into a `Base`.                      |
 | `RangeCheck`         | Perform a (either 64bit or 253bit) range check over some `Base` |
-| `LessThan`           | Compare if `Base` a is lesser than `Base` b                     |
+| `LessThanStrict`     | Strictly compare if `Base` a is lesser than `Base` b            |
+| `LessThanLoose`      | Loosely compare if `Base` a is lesser than `Base` b             |
 | `BoolCheck`          | Enforce that a `Base` fits in a boolean value (either 0 or 1)   |
 | `ConstrainEqualBase` | Constrain equality of two `Base` elements from the stack        |
 | `ConstrainEqualPoint`| Constrain equality of two `EcPoint` elements from the stack     |
@@ -188,7 +189,8 @@ TBD
 | `BaseSub`             | `base_sub(Base a, Base b)`                              | `(Base c)`    |
 | `WitnessBase`         | `witness_base(123)`                                     | `(Base a)`    |
 | `RangeCheck`          | `range_check(64, Base a)`                               | `()`          |
-| `LessThan`            | `less_than(Base a, Base b)`                             | `()`          |
+| `LessThanStrict`      | `less_than_strict(Base a, Base b)`                      | `()`          |
+| `LessThanLoose`       | `less_than_loose(Base a, Base b)`                       | `()`          |
 | `BoolCheck`           | `bool_check(Base a)`                                    | `()`          |
 | `ConstrainEqualBase`  | `constrain_equal_base(Base a, Base b)`                  | `()`          |
 | `ConstrainEqualPoint` | `constrain_equal_point(EcPoint a, EcPoint b)`           | `()`          |

example/dao/proof/dao-exec.zk

@@ -137,7 +137,7 @@ circuit "DaoExec" {
     # Check that dao_quorum is less than or equal to all_votes_value
     one = witness_base(1);
     all_votes_value_1 = base_add(all_votes_value, one);
-    less_than(dao_quorum, all_votes_value_1);
+    less_than_strict(dao_quorum, all_votes_value_1);
 
     # approval_ratio_quot / approval_ratio_base <= yes_votes / all_votes
     #
@@ -149,7 +149,7 @@ circuit "DaoExec" {
     lhs = base_mul(yes_votes_value, dao_approval_ratio_base);
 
     lhs_1 = base_add(lhs, one);
-    less_than(rhs, lhs_1);
+    less_than_strict(rhs, lhs_1);
     
     ####
 

example/dao/proof/dao-propose-main.zk

@@ -66,13 +66,13 @@ circuit "DaoProposeMain" {
 
     # Rangeproof check for proposal amount
     zero = witness_base(0);
-    less_than(zero, proposal_amount);
+    less_than_strict(zero, proposal_amount);
 
     # This is the main check
     # We check that dao_proposer_limit <= total_funds
     one = witness_base(1);
     total_funds_1 = base_add(total_funds, one);
-    less_than(dao_proposer_limit, total_funds_1);
+    less_than_loose(dao_proposer_limit, total_funds_1);
 
 	# Pedersen commitment for coin's value
 	vcv = ec_mul_short(total_funds, VALUE_COMMIT_VALUE);

proof/arithmetic.zk

@@ -14,10 +14,4 @@ circuit "Arith" {
 
     difference = base_sub(a, b);
     constrain_instance(difference);
-
-    #a_gt_b = greater_than(a, b);
-    #constrain_instance(a_gt_b);
-
-    #b_gt_a = greater_than(b, a);
-    #constrain_instance(b_gt_a);
 }

proof/lead.zk

@@ -88,5 +88,5 @@ circuit "Lead" {
         term2 = base_mul(term2_1, value);
         target = base_add(term1, term2);
         #lottery
-        less_than(y_hash, target);
+        less_than_loose(y_hash, target);
 }

proof/opcodes.zk

@@ -45,7 +45,8 @@ circuit "Opcodes" {
 
 	range_check(64, a);
 	range_check(253, b);
-	less_than(a, b);
+	less_than_strict(a, b);
+	less_than_loose(a, b);
 
 	root = merkle_root(leaf_pos, path, c);
 	constrain_instance(root);

src/zk/vm.rs

@@ -718,8 +718,24 @@ impl Circuit<pallas::Base> for ZkCircuit {
                     }
                 }
 
-                Opcode::LessThan => {
-                    debug!("Executing `LessThan{:?}` opcode", opcode.1);
+                Opcode::LessThanStrict => {
+                    debug!("Executing `LessThanStrict{:?}` opcode", opcode.1);
+                    let args = &opcode.1;
+
+                    let a = stack[args[0].1].clone().into();
+                    let b = stack[args[1].1].clone().into();
+
+                    lessthan_chip.copy_less_than(
+                        layouter.namespace(|| "copy a<b check"),
+                        a,
+                        b,
+                        0,
+                        true,
+                    )?;
+                }
+
+                Opcode::LessThanLoose => {
+                    debug!("Executing `LessThanLoose{:?}` opcode", opcode.1);
                     let args = &opcode.1;
 
                     let a = stack[args[0].1].clone().into();

src/zkas/opcode.rs

@@ -64,11 +64,16 @@ pub enum Opcode {
     /// Range check a Base field element, given bit-width (up to 253)
     RangeCheck = 0x50,
 
-    /// Compare two Base field elements and see if a is less than b
-    LessThan = 0x51,
+    /// Strictly compare two Base field elements and see if a is less than b
+    /// This enforces the sum of remaining bits to be zero.
+    LessThanStrict = 0x51,
+
+    /// Loosely two Base field elements and see if a is less than b
+    /// This does not enforce the sum of remaining bits to be zero.
+    LessThanLoose = 0x52,
 
     /// Check if a field element fits in a boolean (Either 0 or 1)
-    BoolCheck = 0x52,
+    BoolCheck = 0x53,
 
     /// Constrain equality of two Base field elements inside the circuit
     ConstrainEqualBase = 0xe0,
@@ -99,7 +104,8 @@ impl Opcode {
             "base_sub" => Some(Self::BaseSub),
             "witness_base" => Some(Self::WitnessBase),
             "range_check" => Some(Self::RangeCheck),
-            "less_than" => Some(Self::LessThan),
+            "less_than_strict" => Some(Self::LessThanStrict),
+            "less_than_loose" => Some(Self::LessThanLoose),
             "bool_check" => Some(Self::BoolCheck),
             "constrain_equal_base" => Some(Self::ConstrainEqualBase),
             "constrain_equal_point" => Some(Self::ConstrainEqualPoint),
@@ -124,8 +130,9 @@ impl Opcode {
             0x32 => Some(Self::BaseSub),
             0x40 => Some(Self::WitnessBase),
             0x50 => Some(Self::RangeCheck),
-            0x51 => Some(Self::LessThan),
-            0x52 => Some(Self::BoolCheck),
+            0x51 => Some(Self::LessThanStrict),
+            0x52 => Some(Self::LessThanLoose),
+            0x53 => Some(Self::BoolCheck),
             0xe0 => Some(Self::ConstrainEqualBase),
             0xe1 => Some(Self::ConstrainEqualPoint),
             0xf0 => Some(Self::ConstrainInstance),
@@ -172,7 +179,9 @@ impl Opcode {
 
             Opcode::RangeCheck => (vec![], vec![VarType::Uint64, VarType::Base]),
 
-            Opcode::LessThan => (vec![], vec![VarType::Base, VarType::Base]),
+            Opcode::LessThanStrict => (vec![], vec![VarType::Base, VarType::Base]),
+
+            Opcode::LessThanLoose => (vec![], vec![VarType::Base, VarType::Base]),
 
             Opcode::BoolCheck => (vec![], vec![VarType::Base]),