zkas, vm: Implement greater_than opcode for scalar comparison.

contrib/zk.lua

@@ -32,7 +32,7 @@ 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',
+  'base_add', 'base_mul', 'base_sub', 'greater_than',
   'poseidon_hash', 'calculate_merkle_root',
   'constrain_instance',
 })

contrib/zk.vim

@@ -19,7 +19,7 @@ syn keyword zkasType
 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
+    \ base_add base_mul base_sub greater_than
     \ poseidon_hash calculate_merkle_root
     \ constrain_instance
 

proof/arithmetic.zk

@@ -1,17 +1,23 @@
 constant "Arith" {}
 
 contract "Arith" {
-	Base a,
-	Base b,
+    Base a,
+    Base b,
 }
 
 circuit "Arith" {
-	sum = base_add(a, b);
-	constrain_instance(sum);
+    sum = base_add(a, b);
+    constrain_instance(sum);
 
-	product = base_mul(a, b);
-	constrain_instance(product);
+    product = base_mul(a, b);
+    constrain_instance(product);
 
-	difference = base_sub(a, b);
-	constrain_instance(difference);
+    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);
 }

src/zk/vm.rs

@@ -22,7 +22,11 @@ use halo2_proofs::{
 use log::debug;
 use pasta_curves::{group::Curve, pallas, Fp};
 
-use super::arith_chip::{ArithmeticChip, ArithmeticChipConfig};
+use super::{
+    arith_chip::{ArithmeticChip, ArithmeticChipConfig},
+    even_bits::{EvenBitsChip, EvenBitsConfig, EvenBitsLookup},
+    greater_than::{GreaterThanChip, GreaterThanConfig, GreaterThanInstruction},
+};
 
 pub use super::vm_stack::{StackVar, Witness};
 use crate::{
@@ -45,6 +49,8 @@ pub struct VmConfig {
     _sinsemilla_cfg2: SinsemillaConfig<OrchardHashDomains, OrchardCommitDomains, OrchardFixedBases>,
     poseidon_config: PoseidonConfig<pallas::Base, 3, 2>,
     arith_config: ArithmeticChipConfig,
+    evenbits_config: EvenBitsConfig,
+    greaterthan_config: GreaterThanConfig,
 }
 
 impl VmConfig {
@@ -85,6 +91,14 @@ impl VmConfig {
     fn arithmetic_chip(&self) -> ArithmeticChip {
         ArithmeticChip::construct(self.arith_config.clone())
     }
+
+    fn evenbits_chip(&self) -> EvenBitsChip<pallas::Base, 24> {
+        EvenBitsChip::construct(self.evenbits_config.clone())
+    }
+
+    fn greaterthan_chip(&self) -> GreaterThanChip<pallas::Base, 24> {
+        GreaterThanChip::construct(self.greaterthan_config.clone())
+    }
 }
 
 #[derive(Clone, Default)]
@@ -186,6 +200,12 @@ impl Circuit<pallas::Base> for ZkCircuit {
         // Configuration for the Arithmetic chip
         let arith_config = ArithmeticChip::configure(meta);
 
+        // Configuration for the EvenBits chip
+        let evenbits_config = EvenBitsChip::<pallas::Base, 24>::configure(meta);
+
+        // Configuration for the GreaterThan chip
+        let greaterthan_config = GreaterThanChip::<pallas::Base, 24>::configure(meta);
+
         // Configuration for a Sinsemilla hash instantiation and a
         // Merkle hash instantiation using this Sinsemilla instance.
         // Since the Sinsemilla config uses only 5 advice columns,
@@ -226,6 +246,8 @@ impl Circuit<pallas::Base> for ZkCircuit {
             _sinsemilla_cfg2,
             poseidon_config,
             arith_config,
+            evenbits_config,
+            greaterthan_config,
         }
     }
 
@@ -251,6 +273,13 @@ impl Circuit<pallas::Base> for ZkCircuit {
         // Construct the Arithmetic chip.
         let arith_chip = config.arithmetic_chip();
 
+        // Construct the EvenBits chip.
+        let eb_chip = config.evenbits_chip();
+        eb_chip.alloc_table(&mut layouter.namespace(|| "alloc table"))?;
+
+        // Construct the GreaterThan chip.
+        let gt_chip = config.greaterthan_chip();
+
         // This constant one is used for short multiplication
         let one = self.load_private(
             layouter.namespace(|| "Load constant one"),
@@ -443,12 +472,6 @@ impl Circuit<pallas::Base> for ZkCircuit {
 
                     macro_rules! poseidon_hash {
                         ($len:expr, $hasher:ident, $output:ident, $cell:ident) => {
-                            // let $hasher = PoseidonHash::<_, _, P128Pow5T3, _, 3, 2>::init(
-                            // config.poseidon_chip(),
-                            // layouter.namespace(|| "PoseidonHash init"),
-                            // ConstantLength::<$len>,
-                            // )?;
-
                             let $hasher =
                                 PoseidonHash::<_, _, P128Pow5T3, ConstantLength<$len>, 3, 2>::init(
                                     config.poseidon_chip(),
@@ -460,7 +483,6 @@ impl Circuit<pallas::Base> for ZkCircuit {
                                 poseidon_message.try_into().unwrap(),
                             )?;
 
-                            //let $cell: AssignedCell<Fp, Fp> = $output.inner().into();
                             let $cell: AssignedCell<Fp, Fp> = $output.into();
 
                             debug!("Pushing hash to stack index {}", stack.len());
@@ -545,6 +567,28 @@ impl Circuit<pallas::Base> for ZkCircuit {
                     stack.push(StackVar::Base(difference));
                 }
 
+                Opcode::GreaterThan => {
+                    debug!("Executing `GreaterThan{:?}` opcode", opcode.1);
+                    let args = &opcode.1;
+
+                    let lhs: AssignedCell<Fp, Fp> = stack[args[0]].clone().into();
+                    let rhs: AssignedCell<Fp, Fp> = stack[args[1]].clone().into();
+
+                    eb_chip.decompose(layouter.namespace(|| "lhs range check"), lhs.clone())?;
+                    eb_chip.decompose(layouter.namespace(|| "rhs range check"), rhs.clone())?;
+
+                    let (helper, greater_than) = gt_chip.greater_than(
+                        layouter.namespace(|| "lhs > rhs"),
+                        lhs.into(),
+                        rhs.into(),
+                    )?;
+
+                    eb_chip.decompose(layouter.namespace(|| "helper range check"), helper.0)?;
+
+                    debug!("Pushing comparison result to stack index {}", stack.len());
+                    stack.push(StackVar::Base(greater_than.0));
+                }
+
                 Opcode::ConstrainInstance => {
                     debug!("Executing `ConstrainInstance{:?}` opcode", opcode.1);
                     let args = &opcode.1;
@@ -560,7 +604,7 @@ impl Circuit<pallas::Base> for ZkCircuit {
                     public_inputs_offset += 1;
                 }
 
-                _ => unimplemented!(),
+                _ => todo!("Handle gracefully"),
             }
         }
 

src/zkas/opcode.rs

@@ -37,6 +37,9 @@ pub enum Opcode {
     /// Base field element subtraction
     BaseSub = 0x32,
 
+    /// Base field greater than comparison
+    GreaterThan = 0x33,
+
     /// Constrain a Base field element to a circuit's public input
     ConstrainInstance = 0xf0,
 
@@ -63,6 +66,7 @@ impl Opcode {
             Opcode::BaseAdd => (vec![Type::Base], vec![Type::Base, Type::Base]),
             Opcode::BaseMul => (vec![Type::Base], vec![Type::Base, Type::Base]),
             Opcode::BaseSub => (vec![Type::Base], vec![Type::Base, Type::Base]),
+            Opcode::GreaterThan => (vec![Type::Base], vec![Type::Base, Type::Base]),
             Opcode::ConstrainInstance => (vec![], vec![Type::Base]),
             Opcode::Noop => (vec![], vec![]),
         }
@@ -81,6 +85,7 @@ impl Opcode {
             0x30 => Self::BaseAdd,
             0x31 => Self::BaseMul,
             0x32 => Self::BaseSub,
+            0x33 => Self::GreaterThan,
             0xf0 => Self::ConstrainInstance,
             _ => unimplemented!(),
         }

tests/arithmetic_proof.rs

@@ -26,6 +26,8 @@ fn arithmetic_proof() -> Result<()> {
     // Witness values
     let a = pallas::Base::from(42);
     let b = pallas::Base::from(69);
+    let y_0 = pallas::Base::from(0); // Here we will compare a > b, which is false (0)
+    let y_1 = pallas::Base::from(1); // Here we will compare b > a, which is true (1)
 
     let prover_witnesses = vec![Witness::Base(Some(a)), Witness::Base(Some(b))];
 
@@ -34,12 +36,12 @@ fn arithmetic_proof() -> Result<()> {
     let product = a * b;
     let difference = a - b;
 
-    let public_inputs = vec![sum, product, difference];
+    let public_inputs = vec![sum, product, difference, y_0, y_1];
 
     // Create the circuit
     let circuit = ZkCircuit::new(prover_witnesses, zkbin.clone());
 
-    let proving_key = ProvingKey::build(11, &circuit);
+    let proving_key = ProvingKey::build(13, &circuit);
     let proof = Proof::create(&proving_key, &[circuit], &public_inputs, &mut OsRng)?;
 
     // ========
@@ -52,7 +54,7 @@ fn arithmetic_proof() -> Result<()> {
     // Create the circuit
     let circuit = ZkCircuit::new(verifier_witnesses, zkbin);
 
-    let verifying_key = VerifyingKey::build(11, &circuit);
+    let verifying_key = VerifyingKey::build(13, &circuit);
     proof.verify(&verifying_key, &public_inputs)?;
     /* ANCHOR_END: main */