diff --git a/bin/dao/daod/proof/dao-exec.zk b/bin/dao/daod/proof/dao-exec.zk index 9fa9c199e..7c695f2a3 100644 --- a/bin/dao/daod/proof/dao-exec.zk +++ b/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); #### diff --git a/bin/dao/daod/proof/dao-propose-main.zk b/bin/dao/daod/proof/dao-propose-main.zk index 2d7db4d02..7a4660e9b 100644 --- a/bin/dao/daod/proof/dao-propose-main.zk +++ b/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); diff --git a/contrib/zk.lua b/contrib/zk.lua index 1d22acaec..e56672f77 100644 --- a/contrib/zk.lua +++ b/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', diff --git a/contrib/zk.vim b/contrib/zk.vim index 223fcac57..2c105d3ed 100644 --- a/contrib/zk.vim +++ b/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 diff --git a/doc/src/zkas/bincode.md b/doc/src/zkas/bincode.md index 170b03e84..0fadf5c07 100644 --- a/doc/src/zkas/bincode.md +++ b/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)` | `()` | diff --git a/example/dao/proof/dao-exec.zk b/example/dao/proof/dao-exec.zk index 9fa9c199e..7c695f2a3 100644 --- a/example/dao/proof/dao-exec.zk +++ 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); #### diff --git a/example/dao/proof/dao-propose-main.zk b/example/dao/proof/dao-propose-main.zk index 2d7db4d02..9419074a6 100644 --- a/example/dao/proof/dao-propose-main.zk +++ b/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); diff --git a/proof/arithmetic.zk b/proof/arithmetic.zk index a2ae69ced..e6e1cbccc 100644 --- a/proof/arithmetic.zk +++ b/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); } diff --git a/proof/lead.zk b/proof/lead.zk index 4c222a967..a49ad9470 100644 --- a/proof/lead.zk +++ b/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); } diff --git a/proof/opcodes.zk b/proof/opcodes.zk index 34d6bcb2b..21518a279 100644 --- a/proof/opcodes.zk +++ b/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); diff --git a/src/zk/vm.rs b/src/zk/vm.rs index e3d05f2b5..90a3ecd78 100644 --- a/src/zk/vm.rs +++ b/src/zk/vm.rs @@ -718,8 +718,24 @@ impl Circuit 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 { + debug!("Executing `LessThanLoose{:?}` opcode", opcode.1); let args = &opcode.1; let a = stack[args[0].1].clone().into(); diff --git a/src/zkas/opcode.rs b/src/zkas/opcode.rs index 85411cd5f..58e21f085 100644 --- a/src/zkas/opcode.rs +++ b/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]),