zkas: Add opcodes for equality constraints of Base and EcPoint.

contrib/zk.lua

@@ -42,9 +42,11 @@ 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',
-  'poseidon_hash', 'merkle_root', 'constrain_instance',
+  'poseidon_hash', 'merkle_root',
   'range_check', 'less_than', 'bool_check',
   'witness_base',
+  'constrain_equal_base', 'constrain_equal_point',
+  'constrain_instance',
 })
 
 -- Identifiers.

contrib/zk.vim

@@ -22,8 +22,10 @@ syn keyword zkasInstruction
     \ ec_add ec_mul ec_mul_base ec_mul_short
     \ ec_get_x ec_get_y
     \ base_add base_mul base_sub
-    \ poseidon_hash merkle_root constrain_instance
+    \ poseidon_hash merkle_root
     \ range_check less_than bool_check witness_base
+    \ constrain_equal_base constrain_equal_point
+    \ constrain_instance
 
 syn region zkasString start='"' end='"' contained
 

doc/src/zkas/bincode.md

@@ -166,6 +166,9 @@ TBD
 | `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                     |
+| `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     |
 | `ConstrainInstance`  | Constrain a `Base` to a Circuit's Public Input.                 |
 
 ### Built-in Opcode Wrappers
@@ -186,6 +189,9 @@ TBD
 | `WitnessBase`         | `witness_base(123)`                                     | `(Base a)`    |
 | `RangeCheck`          | `range_check(64, Base a)`                               | `()`          |
 | `LessThan`            | `less_than(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)`           | `()`          |
 | `ConstrainInstance`   | `constrain_instance(Base a)`                            | `()`          |
 
 ## Decoding the bincode

proof/opcodes.zk

@@ -28,6 +28,11 @@ circuit "Opcodes" {
 	constrain_instance(ec_get_x(value_commit));
 	constrain_instance(ec_get_y(value_commit));
 
+	vcv2 = ec_mul_short(value, VALUE_COMMIT_VALUE);
+	vcr2 = ec_mul(value_blind, VALUE_COMMIT_RANDOM);
+	value_commit_2 = ec_add(vcv2, vcr2);
+	constrain_equal_point(value_commit, value_commit2);
+
 	one = witness_base(1);
 	c = poseidon_hash(one, blind);
 	constrain_instance(c);
@@ -35,6 +40,9 @@ circuit "Opcodes" {
 	d = poseidon_hash(one, blind, ec_get_x(value_commit), ec_get_y(value_commit));
 	constrain_instance(d);
 
+	d2 = poseidon_hash(one, blind, ec_get_x(value_commit2), ec_get_y(value_commit2));
+	constrain_equal_base(d, d2);
+
 	range_check(64, a);
 	range_check(253, b);
 	less_than(a, b);

src/zk/vm.rs

@@ -744,6 +744,35 @@ impl Circuit<pallas::Base> for ZkCircuit {
                         .small_range_check(layouter.namespace(|| "copy boolean check"), w)?;
                 }
 
+                Opcode::ConstrainEqualBase => {
+                    debug!("Executing `ConstrainEqualBase{:?}` opcode", opcode.1);
+                    let args = &opcode.1;
+
+                    let lhs: AssignedCell<Fp, Fp> = stack[args[0].1].clone().into();
+                    let rhs: AssignedCell<Fp, Fp> = stack[args[1].1].clone().into();
+
+                    layouter.assign_region(
+                        || "constrain witnessed base equality",
+                        |mut region| region.constrain_equal(lhs.cell(), rhs.cell()),
+                    )?;
+                }
+
+                Opcode::ConstrainEqualPoint => {
+                    debug!("Executing `ConstrainEqualPoint{:?}` opcode", opcode.1);
+                    let args = &opcode.1;
+
+                    let lhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
+                        stack[args[0].1].clone().into();
+
+                    let rhs: Point<pallas::Affine, EccChip<OrchardFixedBases>> =
+                        stack[args[1].1].clone().into();
+
+                    lhs.constrain_equal(
+                        layouter.namespace(|| "constrain ec point equality"),
+                        &rhs,
+                    )?;
+                }
+
                 Opcode::ConstrainInstance => {
                     debug!("Executing `ConstrainInstance{:?}` opcode", opcode.1);
                     let args = &opcode.1;

src/zkas/opcode.rs

@@ -70,6 +70,12 @@ pub enum Opcode {
     /// Check if a field element fits in a boolean (Either 0 or 1)
     BoolCheck = 0x52,
 
+    /// Constrain equality of two Base field elements inside the circuit
+    ConstrainEqualBase = 0xe0,
+
+    /// Constrain equality of two EcPoint elements inside the circuit
+    ConstrainEqualPoint = 0xe1,
+
     /// Constrain a Base field element to a circuit's public input
     ConstrainInstance = 0xf0,
 
@@ -95,6 +101,8 @@ impl Opcode {
             "range_check" => Some(Self::RangeCheck),
             "less_than" => Some(Self::LessThan),
             "bool_check" => Some(Self::BoolCheck),
+            "constrain_equal_base" => Some(Self::ConstrainEqualBase),
+            "constrain_equal_point" => Some(Self::ConstrainEqualPoint),
             "constrain_instance" => Some(Self::ConstrainInstance),
             "debug" => Some(Self::DebugPrint),
             _ => None,
@@ -118,6 +126,8 @@ impl Opcode {
             0x50 => Some(Self::RangeCheck),
             0x51 => Some(Self::LessThan),
             0x52 => Some(Self::BoolCheck),
+            0xe0 => Some(Self::ConstrainEqualBase),
+            0xe1 => Some(Self::ConstrainEqualPoint),
             0xf0 => Some(Self::ConstrainInstance),
             0xff => Some(Self::DebugPrint),
             _ => None,
@@ -166,6 +176,10 @@ impl Opcode {
 
             Opcode::BoolCheck => (vec![], vec![VarType::Base]),
 
+            Opcode::ConstrainEqualBase => (vec![], vec![VarType::Base, VarType::Base]),
+
+            Opcode::ConstrainEqualPoint => (vec![], vec![VarType::EcPoint, VarType::EcPoint]),
+
             Opcode::ConstrainInstance => (vec![], vec![VarType::Base]),
 
             Opcode::DebugPrint => (vec![], vec![]),