diff --git a/bin/zkas/src/main.rs b/bin/zkas/src/main.rs index f356d691d..5268135a6 100644 --- a/bin/zkas/src/main.rs +++ b/bin/zkas/src/main.rs @@ -81,7 +81,7 @@ fn main() { // the initial AST, not caring much about the semantics, just enforcing // syntax and general structure. let parser = Parser::new(filename, source.chars(), tokens); - let (namespace, constants, witnesses, statements) = parser.parse(); + let (namespace, k, constants, witnesses, statements) = parser.parse(); // The analyzer goes through the initial AST provided by the parser and // converts return and variable types to their correct forms, and also @@ -105,6 +105,7 @@ fn main() { filename, source.chars(), namespace, + k, analyzer.constants, analyzer.witnesses, analyzer.statements, diff --git a/bin/zkrunner/opcodes.no-nipoint.zk b/bin/zkrunner/opcodes.no-nipoint.zk index f70ea137c..7579c6724 100644 --- a/bin/zkrunner/opcodes.no-nipoint.zk +++ b/bin/zkrunner/opcodes.no-nipoint.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Opcodes" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/bin/zkrunner/opcodes.zk b/bin/zkrunner/opcodes.zk index f43026661..e4ca1c85c 100644 --- a/bin/zkrunner/opcodes.zk +++ b/bin/zkrunner/opcodes.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Opcodes" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/contrib/zk.lang b/contrib/zk.lang index cb686e8a5..7faec4890 100644 --- a/contrib/zk.lang +++ b/contrib/zk.lang @@ -23,6 +23,7 @@ + k constant witness circuit diff --git a/contrib/zk.lua b/contrib/zk.lua index c89d71a21..472891982 100644 --- a/contrib/zk.lua +++ b/contrib/zk.lua @@ -20,7 +20,7 @@ local number = token(l.NUMBER, l.integer) -- Keywords. local keyword = token(l.KEYWORD, word_match{ - 'constant', 'witness', 'circuit', + 'k', 'constant', 'witness', 'circuit', }) -- Constants. diff --git a/contrib/zk.vim b/contrib/zk.vim index 9c910453a..40ffc00ef 100644 --- a/contrib/zk.vim +++ b/contrib/zk.vim @@ -8,6 +8,7 @@ if exists("b:current_syntax") endif syn keyword zkasKeyword + \ k \ constant \ witness \ circuit diff --git a/doc/src/zkas/bincode.md b/doc/src/zkas/bincode.md index fb0e2f1fb..86df0fe1d 100644 --- a/doc/src/zkas/bincode.md +++ b/doc/src/zkas/bincode.md @@ -18,6 +18,7 @@ The compiled binary blob has the following layout: ``` MAGIC_BYTES BINARY_VERSION +K NAMESPACE .constant CONSTANT_TYPE CONSTANT_NAME @@ -60,11 +61,16 @@ potential different formats in the future. > `0x02` +### `K` + +This is a 32bit unsigned integer that represents the `k` parameter +needed to know how many rows our circuit needs. + ### `NAMESPACE` -This sector after `MAGIC_BYTES` and `BINARY_VERSION` contains the -reference namespace of the code. This is the namespace used in the -source code, e.g.: +This sector after `MAGIC_BYTES`, `BINARY_VERSION`, and `K` contains +the reference namespace of the code. This is the namespace used in +the source code, e.g.: ``` constant "MyNamespace" { ... } @@ -168,6 +174,8 @@ TBD | `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) | +| `CondSelect` | Select either `a` or `b` based on if `cond` is 0 or 1 | +| `ZeroCondSelect` | Output `a` if `a` is zero, or `b` if a is not zero | | `ConstrainEqualBase` | Constrain equality of two `Base` elements from the heap | | `ConstrainEqualPoint`| Constrain equality of two `EcPoint` elements from the heap | | `ConstrainInstance` | Constrain a `Base` to a Circuit's Public Input. | @@ -176,23 +184,25 @@ TBD | Opcode | Function | Return | | --------------------- | ------------------------------------------------------- | ------------- | -| `EcAdd` | `ec_add(EcPoint a, EcPoint b)` | `(EcPoint c)` | -| `EcMul` | `ec_mul(EcPoint a, EcPoint c)` | `(EcPoint c)` | -| `EcMulBase` | `ec_mul_base(Base a, EcFixedPointBase b)` | `(EcPoint c)` | -| `EcMulShort` | `ec_mul_short(Base a, EcFixedPointShort b)` | `(EcPoint c)` | -| `EcMulVarBase` | `ec_mul_var_base(Base a, EcNiPoint)` | `(EcPoint c)` | -| `EcGetX` | `ec_get_x(EcPoint a)` | `(Base x)` | -| `EcGetY` | `ec_get_y(EcPoint a)` | `(Base y)` | -| `PoseidonHash` | `poseidon_hash(Base a, ..., Base n)` | `(Base h)` | -| `MerkleRoot` | `merkle_root(Uint32 i, MerklePath p, Base a)` | `(Base r)` | -| `BaseAdd` | `base_add(Base a, Base b)` | `(Base c)` | -| `BaseMul` | `base_mul(Base a, Base b)` | `(Base c)` | -| `BaseSub` | `base_sub(Base a, Base b)` | `(Base c)` | -| `WitnessBase` | `witness_base(123)` | `(Base a)` | +| `EcAdd` | `ec_add(EcPoint a, EcPoint b)` | `(EcPoint)` | +| `EcMul` | `ec_mul(EcPoint a, EcPoint c)` | `(EcPoint)` | +| `EcMulBase` | `ec_mul_base(Base a, EcFixedPointBase b)` | `(EcPoint)` | +| `EcMulShort` | `ec_mul_short(Base a, EcFixedPointShort b)` | `(EcPoint)` | +| `EcMulVarBase` | `ec_mul_var_base(Base a, EcNiPoint)` | `(EcPoint)` | +| `EcGetX` | `ec_get_x(EcPoint a)` | `(Base)` | +| `EcGetY` | `ec_get_y(EcPoint a)` | `(Base)` | +| `PoseidonHash` | `poseidon_hash(Base a, ..., Base n)` | `(Base)` | +| `MerkleRoot` | `merkle_root(Uint32 i, MerklePath p, Base a)` | `(Base)` | +| `BaseAdd` | `base_add(Base a, Base b)` | `(Base)` | +| `BaseMul` | `base_mul(Base a, Base b)` | `(Base)` | +| `BaseSub` | `base_sub(Base a, Base b)` | `(Base)` | +| `WitnessBase` | `witness_base(123)` | `(Base)` | | `RangeCheck` | `range_check(64, Base a)` | `()` | | `LessThanStrict` | `less_than_strict(Base a, Base b)` | `()` | | `LessThanLoose` | `less_than_loose(Base a, Base b)` | `()` | | `BoolCheck` | `bool_check(Base a)` | `()` | +| `CondSelect` | `cond_select(Base cond, Base a, Base b)` | `(Base)` | +| `ZeroCondSelect` | `zero_cond(Base a, Base b)` | `(Base)` | | `ConstrainEqualBase` | `constrain_equal_base(Base a, Base b)` | `()` | | `ConstrainEqualPoint` | `constrain_equal_point(EcPoint a, EcPoint b)` | `()` | | `ConstrainInstance` | `constrain_instance(Base a)` | `()` | diff --git a/example/simple.zk b/example/simple.zk index 6a3430735..6939147f5 100644 --- a/example/simple.zk +++ b/example/simple.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Simple" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/proof/arithmetic.zk b/proof/arithmetic.zk index cbb0039f4..962c8cc49 100644 --- a/proof/arithmetic.zk +++ b/proof/arithmetic.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Arith" {} witness "Arith" { diff --git a/proof/burn.zk b/proof/burn.zk index 8873de3d5..52edaf5fd 100644 --- a/proof/burn.zk +++ b/proof/burn.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Burn" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/proof/encrypt.zk b/proof/encrypt.zk index 99005fac2..aa47b76b1 100644 --- a/proof/encrypt.zk +++ b/proof/encrypt.zk @@ -5,6 +5,8 @@ # # This is basically the el gamal scheme in ZK +k = 13; + constant "Encrypt" {} witness "Encrypt" { diff --git a/proof/inclusion_proof.zk b/proof/inclusion_proof.zk index 62ac8728d..05df4bf29 100644 --- a/proof/inclusion_proof.zk +++ b/proof/inclusion_proof.zk @@ -1,3 +1,5 @@ +k = 13; + constant "InclusionProof" { } diff --git a/proof/lead.zk b/proof/lead.zk index d60d233e6..0fb992d1e 100644 --- a/proof/lead.zk +++ b/proof/lead.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Lead" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/proof/mint.zk b/proof/mint.zk index a04483353..deca1c7c0 100644 --- a/proof/mint.zk +++ b/proof/mint.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Mint" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/proof/opcodes.zk b/proof/opcodes.zk index cddb124d7..ad18c6ae2 100644 --- a/proof/opcodes.zk +++ b/proof/opcodes.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Opcodes" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/proof/tx.zk b/proof/tx.zk index ee6753852..30f524d68 100644 --- a/proof/tx.zk +++ b/proof/tx.zk @@ -1,3 +1,5 @@ +k = 13; + constant "tx" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/proof/voting.zk b/proof/voting.zk index f93002b02..a8d7eb971 100644 --- a/proof/voting.zk +++ b/proof/voting.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Vote" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/script/research/rln/signal.zk b/script/research/rln/signal.zk index 42b80590c..9e2f93659 100644 --- a/script/research/rln/signal.zk +++ b/script/research/rln/signal.zk @@ -1,3 +1,5 @@ +k = 13; + constant "RlnSignal" {} witness "RlnSignal" { diff --git a/script/research/rln/slash.zk b/script/research/rln/slash.zk index d7a1d249a..9ff8be96d 100644 --- a/script/research/rln/slash.zk +++ b/script/research/rln/slash.zk @@ -1,3 +1,5 @@ +k = 13; + constant "RlnSlash" {} witness "RlnSlash" { diff --git a/src/contract/consensus/proof/consensus_burn_v1.zk b/src/contract/consensus/proof/consensus_burn_v1.zk index 4c99679d8..c7652a704 100644 --- a/src/contract/consensus/proof/consensus_burn_v1.zk +++ b/src/contract/consensus/proof/consensus_burn_v1.zk @@ -1,3 +1,5 @@ +k = 13; + constant "ConsensusBurn_V1" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/contract/consensus/proof/consensus_mint_v1.zk b/src/contract/consensus/proof/consensus_mint_v1.zk index 67fbdbd0d..aef9fc689 100644 --- a/src/contract/consensus/proof/consensus_mint_v1.zk +++ b/src/contract/consensus/proof/consensus_mint_v1.zk @@ -1,3 +1,5 @@ +k = 13; + constant "ConsensusMint_V1" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/contract/consensus/proof/consensus_proposal_v1.zk b/src/contract/consensus/proof/consensus_proposal_v1.zk index eddb83425..96a3335ed 100644 --- a/src/contract/consensus/proof/consensus_proposal_v1.zk +++ b/src/contract/consensus/proof/consensus_proposal_v1.zk @@ -1,3 +1,5 @@ +k = 13; + constant "ConsensusProposal_V1" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/contract/dao/proof/dao-exec.zk b/src/contract/dao/proof/dao-exec.zk index 953f05c96..d188f515e 100644 --- a/src/contract/dao/proof/dao-exec.zk +++ b/src/contract/dao/proof/dao-exec.zk @@ -1,3 +1,5 @@ +k = 13; + constant "DaoExec" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/contract/dao/proof/dao-mint.zk b/src/contract/dao/proof/dao-mint.zk index 0f851cff1..2a1776a99 100644 --- a/src/contract/dao/proof/dao-mint.zk +++ b/src/contract/dao/proof/dao-mint.zk @@ -1,3 +1,5 @@ +k = 13; + constant "DaoMint" { EcFixedPoint VALUE_COMMIT_RANDOM, EcFixedPointBase NULLIFIER_K, diff --git a/src/contract/dao/proof/dao-propose-burn.zk b/src/contract/dao/proof/dao-propose-burn.zk index 21d8e8ede..135605996 100644 --- a/src/contract/dao/proof/dao-propose-burn.zk +++ b/src/contract/dao/proof/dao-propose-burn.zk @@ -1,3 +1,5 @@ +k = 13; + constant "DaoProposeInput" { EcFixedPointBase NULLIFIER_K, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/contract/dao/proof/dao-propose-main.zk b/src/contract/dao/proof/dao-propose-main.zk index 8d914c854..b85a54a2e 100644 --- a/src/contract/dao/proof/dao-propose-main.zk +++ b/src/contract/dao/proof/dao-propose-main.zk @@ -1,3 +1,5 @@ +k = 13; + constant "DaoProposeMain" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/contract/dao/proof/dao-vote-burn.zk b/src/contract/dao/proof/dao-vote-burn.zk index 6f86b1de9..42756c868 100644 --- a/src/contract/dao/proof/dao-vote-burn.zk +++ b/src/contract/dao/proof/dao-vote-burn.zk @@ -1,3 +1,5 @@ +k = 13; + constant "DaoVoteInput" { EcFixedPointBase NULLIFIER_K, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/contract/dao/proof/dao-vote-main.zk b/src/contract/dao/proof/dao-vote-main.zk index 33e0cf257..921663ff9 100644 --- a/src/contract/dao/proof/dao-vote-main.zk +++ b/src/contract/dao/proof/dao-vote-main.zk @@ -1,3 +1,5 @@ +k = 13; + constant "DaoVoteMain" { EcFixedPoint VALUE_COMMIT_RANDOM, EcFixedPointShort VALUE_COMMIT_VALUE, diff --git a/src/contract/deployooor/proof/derive_contract_id.zk b/src/contract/deployooor/proof/derive_contract_id.zk index f5807b268..da70ed965 100644 --- a/src/contract/deployooor/proof/derive_contract_id.zk +++ b/src/contract/deployooor/proof/derive_contract_id.zk @@ -1,3 +1,5 @@ +k = 13; + constant "DeriveContractID" { EcFixedPointBase NULLIFIER_K, } diff --git a/src/contract/money/proof/burn_v1.zk b/src/contract/money/proof/burn_v1.zk index 2c3f61e83..cef429501 100644 --- a/src/contract/money/proof/burn_v1.zk +++ b/src/contract/money/proof/burn_v1.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Burn_V1" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/contract/money/proof/mint_v1.zk b/src/contract/money/proof/mint_v1.zk index 38b089f95..651e6c663 100644 --- a/src/contract/money/proof/mint_v1.zk +++ b/src/contract/money/proof/mint_v1.zk @@ -1,3 +1,5 @@ +k = 13; + constant "Mint_V1" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/contract/money/proof/token_freeze_v1.zk b/src/contract/money/proof/token_freeze_v1.zk index e4c74aeaa..a4c1eb9eb 100644 --- a/src/contract/money/proof/token_freeze_v1.zk +++ b/src/contract/money/proof/token_freeze_v1.zk @@ -1,3 +1,5 @@ +k = 13; + constant "TokenFreeze_V1" { EcFixedPointBase NULLIFIER_K, } diff --git a/src/contract/money/proof/token_mint_v1.zk b/src/contract/money/proof/token_mint_v1.zk index 28745c549..e504c5fc1 100644 --- a/src/contract/money/proof/token_mint_v1.zk +++ b/src/contract/money/proof/token_mint_v1.zk @@ -1,4 +1,7 @@ # Circuit used to mint arbitrary coins given a mint authority secret. + +k = 13; + constant "TokenMint_V1" { EcFixedPointShort VALUE_COMMIT_VALUE, EcFixedPoint VALUE_COMMIT_RANDOM, diff --git a/src/zkas/compiler.rs b/src/zkas/compiler.rs index 069617045..8951ff8ec 100644 --- a/src/zkas/compiler.rs +++ b/src/zkas/compiler.rs @@ -33,6 +33,7 @@ pub const MAGIC_BYTES: [u8; 4] = [0x0b, 0x01, 0xb1, 0x35]; pub struct Compiler { namespace: String, + k: u32, constants: Vec, witnesses: Vec, statements: Vec, @@ -47,6 +48,7 @@ impl Compiler { filename: &str, source: Chars, namespace: String, + k: u32, constants: Vec, witnesses: Vec, statements: Vec, @@ -58,7 +60,7 @@ impl Compiler { let lines: Vec = source.as_str().lines().map(|x| x.to_string()).collect(); let error = ErrorEmitter::new("Compiler", filename, lines); - Self { namespace, constants, witnesses, statements, literals, debug_info, error } + Self { namespace, k, constants, witnesses, statements, literals, debug_info, error } } pub fn compile(&self) -> Vec { @@ -68,6 +70,9 @@ impl Compiler { bincode.extend_from_slice(&MAGIC_BYTES); bincode.push(BINARY_VERSION); + // Write the circuit's k param + bincode.extend_from_slice(&serialize(&self.k)); + // Write the circuit's namespace bincode.extend_from_slice(&serialize(&self.namespace)); diff --git a/src/zkas/decoder.rs b/src/zkas/decoder.rs index 443f7aec3..707dffb2d 100644 --- a/src/zkas/decoder.rs +++ b/src/zkas/decoder.rs @@ -26,6 +26,7 @@ use crate::{Error::ZkasDecoderError as ZkasErr, Result}; #[derive(Clone, Debug)] pub struct ZkBinary { pub namespace: String, + pub k: u32, pub constants: Vec<(VarType, String)>, pub literals: Vec<(LitType, String)>, pub witnesses: Vec, @@ -46,8 +47,11 @@ impl ZkBinary { let _binary_version = &bytes[4]; - // After the binary version, we're supposed to have the witness namespace - let (namespace, _): (String, _) = deserialize_partial(&bytes[5..])?; + // Deserialize the k param + let (k, _): (u32, _) = deserialize_partial(&bytes[5..9])?; + + // After the binary version and k, we're supposed to have the witness namespace + let (namespace, _): (String, _) = deserialize_partial(&bytes[9..])?; // Enforce a limit on the namespace string length if namespace.len() > 32 { @@ -107,7 +111,7 @@ impl ZkBinary { // TODO: Debug info - Ok(Self { namespace, constants, literals, witnesses, opcodes }) + Ok(Self { namespace, k, constants, literals, witnesses, opcodes }) } fn parse_constants(bytes: &[u8]) -> Result> { diff --git a/src/zkas/parser.rs b/src/zkas/parser.rs index 56345208e..490992ddd 100644 --- a/src/zkas/parser.rs +++ b/src/zkas/parser.rs @@ -29,7 +29,7 @@ use super::{ /// zkas language builtin keywords. /// These can not be used anywhere except where they are expected. -const KEYWORDS: [&str; 3] = ["constant", "witness", "circuit"]; +const KEYWORDS: [&str; 4] = ["k", "constant", "witness", "circuit"]; /// Forbidden namespaces const NOPE_NS: [&str; 4] = [".constant", ".literal", ".witness", ".circuit"]; @@ -101,7 +101,7 @@ impl Parser { Self { tokens, error } } - pub fn parse(&self) -> (String, Vec, Vec, Vec) { + pub fn parse(&self) -> (String, u32, Vec, Vec, Vec) { // We use these to keep state while parsing. let mut namespace = None; let (mut declaring_constant, mut declared_constant) = (false, false); @@ -130,6 +130,29 @@ impl Parser { } let mut iter = self.tokens.iter(); + + // The first thing that has to be declared in the source + // code is the constant "k" which defines 2^k rows that + // the circuit needs to successfully execute. + let Some((k, equal, number, semicolon)) = iter.next_tuple() else { + self.error.abort("Source file does not start with k=n;", 0, 0); + unreachable!(); + }; + + if k.token_type != TokenType::Symbol || + equal.token_type != TokenType::Assign || + number.token_type != TokenType::Number || + semicolon.token_type != TokenType::Semicolon + { + self.error.abort("Source file does not start with k=n;", 0, 0); + } + + if k.token != "k" { + self.error.abort("Source file does not start with k=n;", 0, 0); + } + + let declared_k = number.token.parse().unwrap(); + while let Some(t) = iter.next() { // Sections "constant", "witness", and "circuit" are // the sections we must be declaring in our source code. @@ -350,7 +373,7 @@ impl Parser { self.error.abort("Circuit section is empty.", 0, 0); } - (ns, constants, witnesses, statements) + (ns, declared_k, constants, witnesses, statements) } /// Routine checks on section structure