From 3447c87dd8ead90eefc1abacf16a0227cc8ca8da Mon Sep 17 00:00:00 2001 From: parazyd Date: Thu, 24 Mar 2022 19:02:13 +0100 Subject: [PATCH] zkas, vm: Implement greater_than opcode for scalar comparison. --- contrib/zk.lua | 2 +- contrib/zk.vim | 2 +- proof/arithmetic.zk | 22 +++++++++----- src/zk/vm.rs | 62 +++++++++++++++++++++++++++++++++------ src/zkas/opcode.rs | 5 ++++ tests/arithmetic_proof.rs | 8 +++-- 6 files changed, 79 insertions(+), 22 deletions(-) diff --git a/contrib/zk.lua b/contrib/zk.lua index 6ee506c85..58820aa7e 100644 --- a/contrib/zk.lua +++ b/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', }) diff --git a/contrib/zk.vim b/contrib/zk.vim index 7e7bd18bd..e9feec63b 100644 --- a/contrib/zk.vim +++ b/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 diff --git a/proof/arithmetic.zk b/proof/arithmetic.zk index 29e5a0d69..cc4434191 100644 --- a/proof/arithmetic.zk +++ b/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); } diff --git a/src/zk/vm.rs b/src/zk/vm.rs index 5b13c39df..1b298bf4a 100644 --- a/src/zk/vm.rs +++ b/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, poseidon_config: PoseidonConfig, 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 { + EvenBitsChip::construct(self.evenbits_config.clone()) + } + + fn greaterthan_chip(&self) -> GreaterThanChip { + GreaterThanChip::construct(self.greaterthan_config.clone()) + } } #[derive(Clone, Default)] @@ -186,6 +200,12 @@ impl Circuit for ZkCircuit { // Configuration for the Arithmetic chip let arith_config = ArithmeticChip::configure(meta); + // Configuration for the EvenBits chip + let evenbits_config = EvenBitsChip::::configure(meta); + + // Configuration for the GreaterThan chip + let greaterthan_config = GreaterThanChip::::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 for ZkCircuit { _sinsemilla_cfg2, poseidon_config, arith_config, + evenbits_config, + greaterthan_config, } } @@ -251,6 +273,13 @@ impl Circuit 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 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 for ZkCircuit { poseidon_message.try_into().unwrap(), )?; - //let $cell: AssignedCell = $output.inner().into(); let $cell: AssignedCell = $output.into(); debug!("Pushing hash to stack index {}", stack.len()); @@ -545,6 +567,28 @@ impl Circuit for ZkCircuit { stack.push(StackVar::Base(difference)); } + Opcode::GreaterThan => { + debug!("Executing `GreaterThan{:?}` opcode", opcode.1); + let args = &opcode.1; + + let lhs: AssignedCell = stack[args[0]].clone().into(); + let rhs: AssignedCell = 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 for ZkCircuit { public_inputs_offset += 1; } - _ => unimplemented!(), + _ => todo!("Handle gracefully"), } } diff --git a/src/zkas/opcode.rs b/src/zkas/opcode.rs index 891df363f..938708dfc 100644 --- a/src/zkas/opcode.rs +++ b/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!(), } diff --git a/tests/arithmetic_proof.rs b/tests/arithmetic_proof.rs index 64bd1bc5c..aa80d7b36 100644 --- a/tests/arithmetic_proof.rs +++ b/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 */