zkas: Enforce k declaration on top of the source file.

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,

bin/zkrunner/opcodes.no-nipoint.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Opcodes" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

bin/zkrunner/opcodes.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Opcodes" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

contrib/zk.lang

@@ -23,6 +23,7 @@
 
   <definitions>
     <context id="keywords" style-ref="keyword">
+      <keyword>k</keyword>
       <keyword>constant</keyword>
       <keyword>witness</keyword>
       <keyword>circuit</keyword>

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.

contrib/zk.vim

@@ -8,6 +8,7 @@ if exists("b:current_syntax")
 endif
 
 syn keyword zkasKeyword 
+    \ k
     \ constant
     \ witness
     \ circuit

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)`                            | `()`          |

example/simple.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Simple" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

proof/arithmetic.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Arith" {}
 
 witness "Arith" {

proof/burn.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Burn" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

proof/encrypt.zk

@@ -5,6 +5,8 @@
 #
 # This is basically the el gamal scheme in ZK
 
+k = 13;
+
 constant "Encrypt" {}
 
 witness "Encrypt" {

proof/inclusion_proof.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "InclusionProof" {
 }
 

proof/lead.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Lead" {
          EcFixedPointShort VALUE_COMMIT_VALUE,
          EcFixedPoint VALUE_COMMIT_RANDOM,

proof/mint.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Mint" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

proof/opcodes.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Opcodes" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

proof/tx.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "tx" {
          EcFixedPointShort VALUE_COMMIT_VALUE,
          EcFixedPoint VALUE_COMMIT_RANDOM,

proof/voting.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Vote" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

script/research/rln/signal.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "RlnSignal" {}
 
 witness "RlnSignal" {

script/research/rln/slash.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "RlnSlash" {}
 
 witness "RlnSlash" {

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,

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,

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,

src/contract/dao/proof/dao-exec.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "DaoExec" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

src/contract/dao/proof/dao-mint.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "DaoMint" {
 	EcFixedPoint VALUE_COMMIT_RANDOM,
 	EcFixedPointBase NULLIFIER_K,

src/contract/dao/proof/dao-propose-burn.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "DaoProposeInput" {
 	EcFixedPointBase NULLIFIER_K,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

src/contract/dao/proof/dao-propose-main.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "DaoProposeMain" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

src/contract/dao/proof/dao-vote-burn.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "DaoVoteInput" {
 	EcFixedPointBase NULLIFIER_K,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

src/contract/dao/proof/dao-vote-main.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "DaoVoteMain" {
 	EcFixedPoint VALUE_COMMIT_RANDOM,
 	EcFixedPointShort VALUE_COMMIT_VALUE,

src/contract/deployooor/proof/derive_contract_id.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "DeriveContractID" {
 	EcFixedPointBase NULLIFIER_K,
 }

src/contract/money/proof/burn_v1.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Burn_V1" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

src/contract/money/proof/mint_v1.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "Mint_V1" {
 	EcFixedPointShort VALUE_COMMIT_VALUE,
 	EcFixedPoint VALUE_COMMIT_RANDOM,

src/contract/money/proof/token_freeze_v1.zk

@@ -1,3 +1,5 @@
+k = 13;
+
 constant "TokenFreeze_V1" {
 	EcFixedPointBase NULLIFIER_K,
 }

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,

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<Constant>,
     witnesses: Vec<Witness>,
     statements: Vec<Statement>,
@@ -47,6 +48,7 @@ impl Compiler {
         filename: &str,
         source: Chars,
         namespace: String,
+        k: u32,
         constants: Vec<Constant>,
         witnesses: Vec<Witness>,
         statements: Vec<Statement>,
@@ -58,7 +60,7 @@ impl Compiler {
         let lines: Vec<String> = 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<u8> {
@@ -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));
 

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<VarType>,
@@ -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<Vec<(VarType, String)>> {

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<Constant>, Vec<Witness>, Vec<Statement>) {
+    pub fn parse(&self) -> (String, u32, Vec<Constant>, Vec<Witness>, Vec<Statement>) {
         // 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