Merge branch 'develop' of github.com:Zokrates/ZoKrates into annotate-ir-conditions

2025-09-24 04:40:05 +00:00 · 2021-07-06 15:29:32 +02:00 · 2021-07-06 15:29:32 +02:00 · a492075be5
commit a492075be5
parent ccb70a8e96 e6d0752328
98 changed files with 3580 additions and 714 deletions
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@ -106,7 +106,7 @@ jobs:
            - v4-cargo-cache-{{ arch }}-{{ checksum "Cargo.lock" }}
      - run:
          name: Run integration tests
-          command: WITH_LIBSNARK=1 RUSTFLAGS="-D warnings" ./full_test.sh
+          command: WITH_LIBSNARK=1 RUSTFLAGS="-D warnings" ./integration_test.sh
  deploy:
    docker:
      - image: circleci/python:latest-node
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@ -4,6 +4,25 @@ All notable changes to this project will be documented in this file.
 ## [Unreleased]
 https://github.com/Zokrates/ZoKrates/compare/latest...develop

+## [0.7.4] - 2021-06-17
+
+### Release
+- https://github.com/Zokrates/ZoKrates/releases/tag/0.7.4 <!-- markdown-link-check-disable-line -->
+
+### Changes
+- Add `FIELD_SIZE_IN_BITS`, `FIELD_MIN` and `FIELD_MAX` constants to `field` stdlib module (#917, @dark64)
+- Fix crash on import of functions containing constants (#913, @schaeff)
+- Change endianness in keccak, sha3 and blake2s hash algorithms to big endian (#906, @dark64)
+- Documentation improvements, move examples to a separate section, remove deprecated `--light` flag used in a rng tutorial, add a simple file system resolver example to zokrates.js docs (#914, @dark64)
+- Fixed deserialization logic in the zokrates.js that caused issues on cli-compiled binaries (#912, @dark64)
+- Reduce the cost of conditionals (#907, @schaeff)
+- Improve propagation on if-else expressions when consequence and alternative are equal (#905, @schaeff)
+- Fix access to constant in local function call (#910, @schaeff)
+- Fix parsing of the left hand side of definitions (#896, @schaeff)
+- Fix variable write remover when isolating branches (#904, @schaeff)
+- Introduce a limit of 2**20 for for-loop sizes (#902, @schaeff)
+- Run compilation test on RNG tutorial and fix bugs (#881, @axic)
+
 ## [0.7.3] - 2021-05-19

 ### Release
--- a/Cargo.lock
+++ b/Cargo.lock
@ -2269,7 +2269,7 @@ dependencies = [

 [[package]]
 name = "zokrates_cli"
-version = "0.7.3"
+version = "0.7.4"
 dependencies = [
 "assert_cli",
 "bincode",
@ -2294,7 +2294,7 @@ version = "0.1.0"

 [[package]]
 name = "zokrates_core"
-version = "0.6.3"
+version = "0.6.4"
 dependencies = [
 "ark-bls12-377",
 "ark-bn254",
@ -2343,7 +2343,7 @@ dependencies = [

 [[package]]
 name = "zokrates_embed"
-version = "0.1.2"
+version = "0.1.3"
 dependencies = [
 "bellman_ce",
 "sapling-crypto_ce",
@ -2402,7 +2402,7 @@ dependencies = [

 [[package]]
 name = "zokrates_stdlib"
-version = "0.2.2"
+version = "0.2.3"
 dependencies = [
 "fs_extra",
 "zokrates_test",
--- a/README.md
+++ b/README.md
@ -21,7 +21,7 @@ curl -LSfs get.zokrat.es | sh
 ```

 Have a look at the [documentation](https://zokrates.github.io/) for more information about using ZoKrates.
-[Get started](https://zokrates.github.io/gettingstarted.html), then try a [tutorial](https://zokrates.github.io/rng_tutorial.html)!
+[Get started](https://zokrates.github.io/gettingstarted.html), then try a [tutorial](https://zokrates.github.io/examples/rng_tutorial.html)!

 ## Getting Help

--- a/build.sh
+++ b/build.sh
@ -6,5 +6,5 @@ set -e
 if [ -n "$WITH_LIBSNARK" ]; then
 	cargo build --package zokrates_cli --features="libsnark"
 else
-	cargo build
+	cargo build --package zokrates_cli
 fi
--- a/build_release.sh
+++ b/build_release.sh
@ -6,5 +6,5 @@ set -e
 if [ -n "$WITH_LIBSNARK" ]; then
 	cargo build --release --package zokrates_cli --features="libsnark"
 else
-	cargo build --release
+	cargo build --release --package zokrates_cli
 fi
--- a/changelogs/unreleased/881-axic
+++ b/changelogs/unreleased/881-axic
@ -1 +0,0 @@
-Run compilation test on RNG tutorial and fix bugs
--- a/changelogs/unreleased/896-schaeff
+++ b/changelogs/unreleased/896-schaeff
@ -1 +0,0 @@
-Fix parsing of the left hand side of definitions
--- a/changelogs/unreleased/902-schaeff
+++ b/changelogs/unreleased/902-schaeff
@ -1 +0,0 @@
-Introduce a limit of 2**20 for for-loop sizes
--- a/changelogs/unreleased/904-schaeff
+++ b/changelogs/unreleased/904-schaeff
@ -1 +0,0 @@
-Fix variable write remover when isolating branches
--- a/changelogs/unreleased/905-schaeff
+++ b/changelogs/unreleased/905-schaeff
@ -1 +0,0 @@
-Improve propagation on if-else expressions when consequence and alternative are equal
--- a/changelogs/unreleased/907-schaeff
+++ b/changelogs/unreleased/907-schaeff
@ -1 +0,0 @@
-Reduce the cost of conditionals
--- a/changelogs/unreleased/910-schaeff
+++ b/changelogs/unreleased/910-schaeff
@ -1 +0,0 @@
-Fix access to constant in local function call
--- a/changelogs/unreleased/912-dark64
+++ b/changelogs/unreleased/912-dark64
@ -1 +0,0 @@
-Fixed deserialization logic in the zokrates.js that caused issues on cli-compiled binaries
--- a/changelogs/unreleased/914-dark64
+++ b/changelogs/unreleased/914-dark64
@ -1 +0,0 @@
-Documentation improvements, move examples to a separate section, remove deprecated `--light` flag used in a rng tutorial, add a simple file system resolver example to zokrates.js docs
--- a/changelogs/unreleased/919-leonardoalt
+++ b/changelogs/unreleased/919-leonardoalt
@ -0,0 +1 @@
+Add a CLI option `generate-smtlib2` to output the compiled IR as an SMT formula.
--- a/changelogs/unreleased/924-schaeff
+++ b/changelogs/unreleased/924-schaeff
@ -0,0 +1 @@
+Add details to for-loop documentation
--- a/changelogs/unreleased/930-schaeff
+++ b/changelogs/unreleased/930-schaeff
@ -0,0 +1 @@
+Reduce cost of variable memory access
--- a/integration_test.sh
+++ b/integration_test.sh
@ -6,5 +6,5 @@ set -e
 if [ -n "$WITH_LIBSNARK" ]; then
 	cargo test --release --package zokrates_cli --features="libsnark" -- --ignored
 else
-	cargo test --release -- --ignored
+	cargo test --release --package zokrates_cli                       -- --ignored
 fi
--- a/scripts/changelog.sh
+++ b/scripts/changelog.sh
@ -30,7 +30,7 @@ cat << EOT
 ## [${tag}] - $(qdate '+%Y-%m-%d')

 ### Release
- https://github.com/Zokrates/ZoKrates/releases/tag/${tag}
+- https://github.com/Zokrates/ZoKrates/releases/tag/${tag} <!-- markdown-link-check-disable-line -->

 ### Changes
 EOT
--- a/test.sh
+++ b/test.sh
@ -4,7 +4,9 @@
 set -e

 if [ -n "$WITH_LIBSNARK" ]; then
-	cargo test --release --package zokrates_cli --features="libsnark"
-else
-	cargo test --release
+	# run specifically the libsnark tests inside zokrates_core
+	cargo test --release --package zokrates_core --features="libsnark" libsnark -- --test-threads=1
 fi
+
+# run all tests without libsnark on
+cargo test --release
--- a/zokrates_book/src/examples/rng_tutorial.md
+++ b/zokrates_book/src/examples/rng_tutorial.md
@ -26,7 +26,7 @@ There are many ways to calculate a hash, but here we use Zokrates.

 1. Create this file under the name `get_hash.zok`:
 ```zokrates
-{{#include ../../zokrates_cli/examples/book/rng_tutorial/get_hash.zok}}
+{{#include ../../../zokrates_cli/examples/book/rng_tutorial/get_hash.zok}}
 ```
 2. Compile the program to a form that is usable for zero knowledge proofs. This command writes 
 the binary to `get_hash`. You can see a textual representation, somewhat analogous to assembler 
@ -99,7 +99,7 @@ The next step is to reveal a single bit.

 1. Use this program, `reveal_bit.zok`:
 ```zokrates
-{{#include ../../zokrates_cli/examples/book/rng_tutorial/reveal_bit.zok}}
+{{#include ../../../zokrates_cli/examples/book/rng_tutorial/reveal_bit.zok}}
 ```

 2. Compile and run as you did the previous program:
--- a/zokrates_book/src/examples/sha256example.md
+++ b/zokrates_book/src/examples/sha256example.md
@ -16,7 +16,7 @@ We will start this tutorial by using ZoKrates to compute the hash for an arbitra
 First, we create a new file named `hashexample.zok` with the following content:

 ```zokrates
-{{#include ../../zokrates_cli/examples/book/hashexample.zok}}
+{{#include ../../../zokrates_cli/examples/book/hashexample.zok}}
 ```

 The first line imports the `sha256packed` function from the ZoKrates standard library.
@ -70,7 +70,7 @@ To make it work, the two parties have to follow their roles in the protocol:
 First, Victor has to specify what hash he is interested in. Therefore, we have to adjust the zkSNARK circuit, compiled by ZoKrates, such that in addition to computing the digest, it also validates it against the digest of interest, provided by Victor. This leads to the following update for `hashexample.zok`:

 ```zokrates
-{{#include ../../zokrates_cli/examples/book/hashexample_updated.zok}}
+{{#include ../../../zokrates_cli/examples/book/hashexample_updated.zok}}
 ```

 Note that we now compare the result of `sha256packed` with the hard-coded correct solution defined by Victor. The lines which we added are treated as assertions: the verifier will not accept a proof where these constraints were not satisfied. Clearly, this program only returns 1 if all of the computed bits are equal.
--- a/zokrates_book/src/language/control_flow.md
+++ b/zokrates_book/src/language/control_flow.md
@ -53,6 +53,8 @@ For loops are available with the following syntax:

 The bounds have to be constant at compile-time, therefore they cannot depend on execution inputs. They can depend on generic parameters.

+> For loops are only syntactic sugar for repeating a block of statements many times. No condition of the type `index < max` is being checked at run-time after each iteration. Instead, at compile-time, the index is incremented and the block is executed again. Therefore, assigning to the loop index does not have any influence on the number of iterations performed and is considered bad practice.
+
 ### Assertions

 Any boolean can be asserted to be true using the `assert` function.
--- a/zokrates_cli/Cargo.toml
+++ b/zokrates_cli/Cargo.toml
@ -1,6 +1,6 @@
 [package]
 name = "zokrates_cli"
-version = "0.7.3"
+version = "0.7.4"
 authors = ["Jacob Eberhardt <jacob.eberhardt@tu-berlin.de>", "Dennis Kuhnert <mail@kyroy.com>", "Thibaut Schaeffer <thibaut@schaeff.fr>"]
 repository = "https://github.com/JacobEberhardt/ZoKrates.git"
 edition = "2018"
--- a/zokrates_cli/src/bin.rs
+++ b/zokrates_cli/src/bin.rs
@ -48,6 +48,7 @@ fn cli() -> Result<(), String> {
            export_verifier::subcommand(),
            #[cfg(any(feature = "bellman", feature = "ark", feature = "libsnark"))]
            generate_proof::subcommand(),
+            generate_smtlib2::subcommand(),
            print_proof::subcommand(),
            #[cfg(any(feature = "bellman", feature = "ark", feature = "libsnark"))]
            verify::subcommand()])
@ -62,6 +63,7 @@ fn cli() -> Result<(), String> {
        ("export-verifier", Some(sub_matches)) => export_verifier::exec(sub_matches),
        #[cfg(any(feature = "bellman", feature = "ark", feature = "libsnark"))]
        ("generate-proof", Some(sub_matches)) => generate_proof::exec(sub_matches),
+        ("generate-smtlib2", Some(sub_matches)) => generate_smtlib2::exec(sub_matches),
        ("print-proof", Some(sub_matches)) => print_proof::exec(sub_matches),
        #[cfg(any(feature = "bellman", feature = "ark", feature = "libsnark"))]
        ("verify", Some(sub_matches)) => verify::exec(sub_matches),
--- a/zokrates_cli/src/constants.rs
+++ b/zokrates_cli/src/constants.rs
@ -5,6 +5,7 @@ pub const PROVING_KEY_DEFAULT_PATH: &str = "proving.key";
 pub const VERIFICATION_CONTRACT_DEFAULT_PATH: &str = "verifier.sol";
 pub const WITNESS_DEFAULT_PATH: &str = "witness";
 pub const JSON_PROOF_PATH: &str = "proof.json";
+pub const SMTLIB2_DEFAULT_PATH: &str = "out.smt2";

 pub const BELLMAN: &str = "bellman";
 pub const LIBSNARK: &str = "libsnark";
--- a/zokrates_cli/src/ops/generate_smtlib2.rs
+++ b/zokrates_cli/src/ops/generate_smtlib2.rs
@ -0,0 +1,64 @@
+use crate::constants::{FLATTENED_CODE_DEFAULT_PATH, SMTLIB2_DEFAULT_PATH};
+use clap::{App, Arg, ArgMatches, SubCommand};
+use std::fs::File;
+use std::io::{BufReader, Write};
+use std::path::Path;
+use zokrates_core::ir;
+use zokrates_core::ir::smtlib2::SMTLib2Display;
+use zokrates_core::ir::ProgEnum;
+use zokrates_field::Field;
+
+pub fn subcommand() -> App<'static, 'static> {
+    SubCommand::with_name("generate-smtlib2")
+        .about("Outputs the constraint system in the SMTLib2 format")
+        .arg(
+            Arg::with_name("input")
+                .short("i")
+                .long("input")
+                .help("Path of the binary")
+                .value_name("FILE")
+                .takes_value(true)
+                .required(false)
+                .default_value(FLATTENED_CODE_DEFAULT_PATH),
+        )
+        .arg(
+            Arg::with_name("output")
+                .short("o")
+                .long("output")
+                .help("Path of the output file")
+                .value_name("FILE")
+                .takes_value(true)
+                .required(false)
+                .default_value(SMTLIB2_DEFAULT_PATH),
+        )
+}
+
+pub fn exec(sub_matches: &ArgMatches) -> Result<(), String> {
+    // read compiled program
+    let path = Path::new(sub_matches.value_of("input").unwrap());
+    let file =
+        File::open(&path).map_err(|why| format!("Could not open {}: {}", path.display(), why))?;
+
+    let mut reader = BufReader::new(file);
+
+    match ProgEnum::deserialize(&mut reader)? {
+        ProgEnum::Bn128Program(p) => cli_smtlib2(p, sub_matches),
+        ProgEnum::Bls12_377Program(p) => cli_smtlib2(p, sub_matches),
+        ProgEnum::Bls12_381Program(p) => cli_smtlib2(p, sub_matches),
+        ProgEnum::Bw6_761Program(p) => cli_smtlib2(p, sub_matches),
+    }
+}
+
+fn cli_smtlib2<T: Field>(ir_prog: ir::Prog<T>, sub_matches: &ArgMatches) -> Result<(), String> {
+    println!("Generating SMTLib2...");
+
+    let output_path = Path::new(sub_matches.value_of("output").unwrap());
+    let mut output_file = File::create(output_path).unwrap();
+
+    output_file
+        .write(format!("{}", SMTLib2Display(&ir_prog)).as_bytes())
+        .map_err(|why| format!("Could not save smtlib2: {:?}", why))?;
+
+    println!("SMTLib2 file written to '{}'", output_path.display());
+    Ok(())
+}
--- a/zokrates_cli/src/ops/mod.rs
+++ b/zokrates_cli/src/ops/mod.rs
@ -4,6 +4,7 @@ pub mod compute_witness;
 pub mod export_verifier;
 #[cfg(any(feature = "bellman", feature = "ark", feature = "libsnark"))]
 pub mod generate_proof;
+pub mod generate_smtlib2;
 pub mod print_proof;
 #[cfg(any(feature = "bellman", feature = "ark", feature = "libsnark"))]
 pub mod setup;
--- a/zokrates_cli/tests/code/arithmetics.smt2
+++ b/zokrates_cli/tests/code/arithmetics.smt2
@ -0,0 +1,15 @@
+; Auto generated by ZoKrates
+; Number of circuit variables: 5
+; Number of equalities: 2
+(declare-const |~prime| Int)
+(declare-const |~out_0| Int)
+(declare-const |~one| Int)
+(declare-const |_0| Int)
+(declare-const |_1| Int)
+(declare-const |_2| Int)
+(assert (and
+(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
+(= |~one| 1)
+(= (mod (* (+ (* |_0| 1) (* |_1| 1)) (+ (* |_0| 1) (* |_1| 1))) |~prime|) (mod (* |_2| 1) |~prime|))
+(= (mod (* (* |~one| 1) (+ (* |_0| 3) (* |_2| 1))) |~prime|) (mod (* |~out_0| 1) |~prime|))
+))
--- a/zokrates_cli/tests/code/if_else_false.smt2
+++ b/zokrates_cli/tests/code/if_else_false.smt2
@ -0,0 +1,17 @@
+; Auto generated by ZoKrates
+; Number of circuit variables: 5
+; Number of equalities: 4
+(declare-const |~prime| Int)
+(declare-const |~out_0| Int)
+(declare-const |~one| Int)
+(declare-const |_0| Int)
+(declare-const |_2| Int)
+(declare-const |_3| Int)
+(assert (and
+(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
+(= |~one| 1)
+
+(= (mod (* (+ (* |~one| 21888242871839275222246405745257275088548364400416034343698204186575808495616) (* |_0| 1)) (* |_3| 1)) |~prime|) (mod (* |_2| 1) |~prime|))
+(= (mod (* (+ (* |~one| 1) (* |_2| 21888242871839275222246405745257275088548364400416034343698204186575808495616)) (+ (* |~one| 21888242871839275222246405745257275088548364400416034343698204186575808495616) (* |_0| 1))) |~prime|) (mod 0 |~prime|))
+(= (mod (* (* |~one| 1) (+ (* |~one| 1) (* |_2| 21888242871839275222246405745257275088548364400416034343698204186575808495616))) |~prime|) (mod (* |~out_0| 1) |~prime|))
+))
--- a/zokrates_cli/tests/code/if_else_true.smt2
+++ b/zokrates_cli/tests/code/if_else_true.smt2
@ -0,0 +1,17 @@
+; Auto generated by ZoKrates
+; Number of circuit variables: 5
+; Number of equalities: 4
+(declare-const |~prime| Int)
+(declare-const |~out_0| Int)
+(declare-const |~one| Int)
+(declare-const |_0| Int)
+(declare-const |_2| Int)
+(declare-const |_3| Int)
+(assert (and
+(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
+(= |~one| 1)
+
+(= (mod (* (+ (* |~one| 21888242871839275222246405745257275088548364400416034343698204186575808495616) (* |_0| 1)) (* |_3| 1)) |~prime|) (mod (* |_2| 1) |~prime|))
+(= (mod (* (+ (* |~one| 1) (* |_2| 21888242871839275222246405745257275088548364400416034343698204186575808495616)) (+ (* |~one| 21888242871839275222246405745257275088548364400416034343698204186575808495616) (* |_0| 1))) |~prime|) (mod 0 |~prime|))
+(= (mod (* (* |~one| 1) (+ (* |~one| 1) (* |_2| 21888242871839275222246405745257275088548364400416034343698204186575808495616))) |~prime|) (mod (* |~out_0| 1) |~prime|))
+))
--- a/zokrates_cli/tests/code/multidim_update.smt2
+++ b/zokrates_cli/tests/code/multidim_update.smt2
@ -0,0 +1,21 @@
+; Auto generated by ZoKrates
+; Number of circuit variables: 9
+; Number of equalities: 4
+(declare-const |~prime| Int)
+(declare-const |~out_3| Int)
+(declare-const |~out_2| Int)
+(declare-const |~out_1| Int)
+(declare-const |~out_0| Int)
+(declare-const |~one| Int)
+(declare-const |_0| Int)
+(declare-const |_1| Int)
+(declare-const |_2| Int)
+(declare-const |_3| Int)
+(assert (and
+(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
+(= |~one| 1)
+(= (mod (* (* |~one| 1) (* |_0| 1)) |~prime|) (mod (* |~out_0| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |_1| 1)) |~prime|) (mod (* |~out_1| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |_2| 1)) |~prime|) (mod (* |~out_2| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |~one| 42)) |~prime|) (mod (* |~out_3| 1) |~prime|))
+))
--- a/zokrates_cli/tests/code/no_return.smt2
+++ b/zokrates_cli/tests/code/no_return.smt2
@ -0,0 +1,12 @@
+; Auto generated by ZoKrates
+; Number of circuit variables: 3
+; Number of equalities: 1
+(declare-const |~prime| Int)
+(declare-const |~one| Int)
+(declare-const |_0| Int)
+(declare-const |_1| Int)
+(assert (and
+(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
+(= |~one| 1)
+(= (mod (* (* |~one| 1) (* |_0| 1)) |~prime|) (mod (* |_1| 1) |~prime|))
+))
--- a/zokrates_cli/tests/code/return_array.smt2
+++ b/zokrates_cli/tests/code/return_array.smt2
@ -0,0 +1,33 @@
+; Auto generated by ZoKrates
+; Number of circuit variables: 17
+; Number of equalities: 8
+(declare-const |~prime| Int)
+(declare-const |~out_7| Int)
+(declare-const |~out_6| Int)
+(declare-const |~out_5| Int)
+(declare-const |~out_4| Int)
+(declare-const |~out_3| Int)
+(declare-const |~out_2| Int)
+(declare-const |~out_1| Int)
+(declare-const |~out_0| Int)
+(declare-const |~one| Int)
+(declare-const |_0| Int)
+(declare-const |_1| Int)
+(declare-const |_2| Int)
+(declare-const |_3| Int)
+(declare-const |_4| Int)
+(declare-const |_5| Int)
+(declare-const |_6| Int)
+(declare-const |_7| Int)
+(assert (and
+(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
+(= |~one| 1)
+(= (mod (* (* |~one| 1) (* |_3| 1)) |~prime|) (mod (* |~out_0| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |_0| 1)) |~prime|) (mod (* |~out_1| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |_1| 1)) |~prime|) (mod (* |~out_2| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |_2| 1)) |~prime|) (mod (* |~out_3| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |_4| 1)) |~prime|) (mod (* |~out_4| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |_5| 1)) |~prime|) (mod (* |~out_5| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |_6| 1)) |~prime|) (mod (* |~out_6| 1) |~prime|))
+(= (mod (* (* |~one| 1) (* |_7| 1)) |~prime|) (mod (* |~out_7| 1) |~prime|))
+))
--- a/zokrates_cli/tests/code/simple_add.smt2
+++ b/zokrates_cli/tests/code/simple_add.smt2
@ -0,0 +1,13 @@
+; Auto generated by ZoKrates
+; Number of circuit variables: 4
+; Number of equalities: 1
+(declare-const |~prime| Int)
+(declare-const |~out_0| Int)
+(declare-const |~one| Int)
+(declare-const |_0| Int)
+(declare-const |_1| Int)
+(assert (and
+(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
+(= |~one| 1)
+(= (mod (* (* |~one| 1) (+ (* |_0| 1) (* |_1| 1))) |~prime|) (mod (* |~out_0| 1) |~prime|))
+))
--- a/zokrates_cli/tests/code/simple_mul.smt2
+++ b/zokrates_cli/tests/code/simple_mul.smt2
@ -0,0 +1,16 @@
+; Auto generated by ZoKrates
+; Number of circuit variables: 6
+; Number of equalities: 2
+(declare-const |~prime| Int)
+(declare-const |~out_0| Int)
+(declare-const |~one| Int)
+(declare-const |_0| Int)
+(declare-const |_1| Int)
+(declare-const |_2| Int)
+(declare-const |_3| Int)
+(assert (and
+(= |~prime| 21888242871839275222246405745257275088548364400416034343698204186575808495617)
+(= |~one| 1)
+(= (mod (* (* |_0| 1) (* |_1| 1)) |~prime|) (mod (* |_3| 1) |~prime|))
+(= (mod (* (* |_3| 1) (* |_2| 1)) |~prime|) (mod (* |~out_0| 1) |~prime|))
+))
--- a/zokrates_cli/tests/code/taxation.smt2
+++ b/zokrates_cli/tests/code/taxation.smt2
--- a/zokrates_cli/tests/integration.rs
+++ b/zokrates_cli/tests/integration.rs
@ -314,4 +314,78 @@ mod integration {
            }
        }
    }
+
+    fn test_compile_and_smtlib2(
+        program_name: &str,
+        program_path: &Path,
+        expected_smtlib2_path: &Path,
+    ) {
+        let tmp_dir = TempDir::new(".tmp").unwrap();
+        let tmp_base = tmp_dir.path();
+        let test_case_path = tmp_base.join(program_name);
+        let flattened_path = tmp_base.join(program_name).join("out");
+        let smtlib2_path = tmp_base.join(program_name).join("out.smt2");
+
+        // create a tmp folder to store artifacts
+        fs::create_dir(test_case_path).unwrap();
+
+        let stdlib = std::fs::canonicalize("../zokrates_stdlib/stdlib").unwrap();
+
+        // prepare compile arguments
+        let compile = vec![
+            "../target/release/zokrates",
+            "compile",
+            "-i",
+            program_path.to_str().unwrap(),
+            "--stdlib-path",
+            stdlib.to_str().unwrap(),
+            "-o",
+            flattened_path.to_str().unwrap(),
+        ];
+
+        // compile
+        assert_cli::Assert::command(&compile).succeeds().unwrap();
+
+        // prepare generate-smtlib2 arguments
+        let gen = vec![
+            "../target/release/zokrates",
+            "generate-smtlib2",
+            "-i",
+            flattened_path.to_str().unwrap(),
+            "-o",
+            smtlib2_path.to_str().unwrap(),
+        ];
+
+        // generate-smtlib2
+        assert_cli::Assert::command(&gen).succeeds().unwrap();
+
+        // load the expected smtlib2
+        let mut expected_smtlib2_file = File::open(&expected_smtlib2_path).unwrap();
+        let mut expected_smtlib2 = String::new();
+        expected_smtlib2_file
+            .read_to_string(&mut expected_smtlib2)
+            .unwrap();
+
+        // load the actual smtlib2
+        let mut smtlib2_file = File::open(&smtlib2_path).unwrap();
+        let mut smtlib2 = String::new();
+        smtlib2_file.read_to_string(&mut smtlib2).unwrap();
+
+        assert_eq!(expected_smtlib2, smtlib2);
+    }
+
+    #[test]
+    fn test_compile_and_smtlib2_dir() {
+        let dir = Path::new("./tests/code");
+        assert!(dir.is_dir());
+        for entry in fs::read_dir(dir).unwrap() {
+            let entry = entry.unwrap();
+            let path = entry.path();
+            if path.extension().unwrap() == "smt2" {
+                let program_name = Path::new(path.file_stem().unwrap());
+                let prog = dir.join(program_name).with_extension("zok");
+                test_compile_and_smtlib2(program_name.to_str().unwrap(), &prog, &path);
+            }
+        }
+    }
 }
--- a/zokrates_core/Cargo.toml
+++ b/zokrates_core/Cargo.toml
@ -1,6 +1,6 @@
 [package]
 name = "zokrates_core"
-version = "0.6.3"
+version = "0.6.4"
 edition = "2018"
 authors = ["Jacob Eberhardt <jacob.eberhardt@tu-berlin.de>", "Dennis Kuhnert <mail@kyroy.com>"]
 repository = "https://github.com/JacobEberhardt/ZoKrates"
--- a/zokrates_core/lib/ffi.cpp
+++ b/zokrates_core/lib/ffi.cpp
@ -1,6 +1,6 @@
 #include "ffi.hpp"

-void __free(uint8_t* ptr)
+void c_free(uint8_t* ptr)
 {
    free(ptr);
 }
--- a/zokrates_core/lib/ffi.hpp
+++ b/zokrates_core/lib/ffi.hpp
@ -30,7 +30,7 @@ struct proof_result_t {
    }
 };

-void __free(uint8_t* ptr);
+void c_free(uint8_t* ptr);

 #ifdef __cplusplus
 } // extern "C"
--- a/zokrates_core/src/embed.rs
+++ b/zokrates_core/src/embed.rs
@ -4,7 +4,8 @@ use crate::flat_absy::{
 };
 use crate::solvers::Solver;
 use crate::typed_absy::types::{
-    ConcreteGenericsAssignment, Constant, DeclarationSignature, DeclarationType, GenericIdentifier,
+    ConcreteGenericsAssignment, DeclarationConstant, DeclarationSignature, DeclarationType,
+    GenericIdentifier,
 };
 use std::collections::HashMap;
 use zokrates_field::{Bn128Field, Field};
@ -43,10 +44,12 @@ impl FlatEmbed {
                .inputs(vec![DeclarationType::uint(32)])
                .outputs(vec![DeclarationType::FieldElement]),
            FlatEmbed::Unpack => DeclarationSignature::new()
-                .generics(vec![Some(Constant::Generic(GenericIdentifier {
-                    name: "N",
-                    index: 0,
-                }))])
+                .generics(vec![Some(DeclarationConstant::Generic(
+                    GenericIdentifier {
+                        name: "N",
+                        index: 0,
+                    },
+                ))])
                .inputs(vec![DeclarationType::FieldElement])
                .outputs(vec![DeclarationType::array((
                    DeclarationType::Boolean,
@ -122,7 +125,7 @@ impl FlatEmbed {
            .generics
            .into_iter()
            .map(|c| match c.unwrap() {
-                Constant::Generic(g) => g,
+                DeclarationConstant::Generic(g) => g,
                _ => unreachable!(),
            });

--- a/zokrates_core/src/flatten/mod.rs
+++ b/zokrates_core/src/flatten/mod.rs
@ -659,6 +659,9 @@ impl<'ast, T: Field> Flattener<'ast, T> {
            BooleanExpression::Identifier(x) => {
                FlatExpression::Identifier(*self.layout.get(&x).unwrap())
            }
+            BooleanExpression::Select(a, box index) => self
+                .flatten_select_expression(statements_flattened, a, index)
+                .get_field_unchecked(),
            BooleanExpression::FieldLt(box lhs, box rhs) => {
                // Get the bit width to know the size of the binary decompositions for this Field
                let bit_width = T::get_required_bits();
@ -1459,6 +1462,9 @@ impl<'ast, T: Field> Flattener<'ast, T> {
                });
                FlatUExpression::with_field(field).bits(bits)
            }
+            UExpressionInner::Select(a, box index) => {
+                self.flatten_select_expression(statements_flattened, a, index)
+            }
            UExpressionInner::Not(box e) => {
                let e = self.flatten_uint_expression(statements_flattened, e);

@ -1996,6 +2002,61 @@ impl<'ast, T: Field> Flattener<'ast, T> {
        })
    }

+    fn flatten_select_expression<U: Flatten<'ast, T>>(
+        &mut self,
+        statements_flattened: &mut FlatStatements<T>,
+        a: Vec<U>,
+        index: UExpression<'ast, T>,
+    ) -> FlatUExpression<T> {
+        let (range_check, result) = a
+            .into_iter()
+            .enumerate()
+            .map(|(i, e)| {
+                let condition = self.flatten_boolean_expression(
+                    statements_flattened,
+                    BooleanExpression::UintEq(
+                        box UExpressionInner::Value(i as u128)
+                            .annotate(UBitwidth::B32)
+                            .metadata(UMetadata {
+                                should_reduce: ShouldReduce::True,
+                                max: T::from(i),
+                            }),
+                        box index.clone(),
+                    ),
+                );
+
+                let element = e.flatten(self, statements_flattened);
+
+                (condition, element)
+            })
+            .collect::<Vec<_>>()
+            .into_iter()
+            .fold(
+                (
+                    FlatExpression::Number(T::zero()),
+                    FlatExpression::Number(T::zero()),
+                ),
+                |(mut range_check, mut result), (condition, element)| {
+                    range_check = FlatExpression::Add(box range_check, box condition.clone());
+
+                    let conditional_element_id = self.use_sym();
+                    statements_flattened.push(FlatStatement::Definition(
+                        conditional_element_id,
+                        FlatExpression::Mult(box condition, box element.flat()),
+                    ));
+
+                    result = FlatExpression::Add(box result, box conditional_element_id.into());
+                    (range_check, result)
+                },
+            );
+
+        statements_flattened.push(FlatStatement::Condition(
+            range_check,
+            FlatExpression::Number(T::one()),
+        ));
+        FlatUExpression::with_field(result)
+    }
+
    /// Flattens a field expression
    ///
    /// # Arguments
@ -2012,6 +2073,9 @@ impl<'ast, T: Field> Flattener<'ast, T> {
            FieldElementExpression::Identifier(x) => {
                FlatExpression::Identifier(*self.layout.get(&x).unwrap_or_else(|| panic!("{}", x)))
            }
+            FieldElementExpression::Select(a, box index) => self
+                .flatten_select_expression(statements_flattened, a, index)
+                .get_field_unchecked(),
            FieldElementExpression::Add(box left, box right) => {
                let left_flattened = self.flatten_field_expression(statements_flattened, left);
                let right_flattened = self.flatten_field_expression(statements_flattened, right);
--- a/zokrates_core/src/imports.rs
+++ b/zokrates_core/src/imports.rs
@ -14,6 +14,7 @@ use std::fmt;
 use std::io;
 use std::path::{Path, PathBuf};

+use crate::absy::types::UnresolvedType;
 use typed_arena::Arena;
 use zokrates_common::Resolver;
 use zokrates_field::{Bn128Field, Field};
@ -156,6 +157,17 @@ impl Importer {
                    id: symbol.get_alias(),
                    symbol: Symbol::Flat(FlatEmbed::U8FromBits),
                },
+                "FIELD_SIZE_IN_BITS" => SymbolDeclaration {
+                    id: symbol.get_alias(),
+                    symbol: Symbol::Here(SymbolDefinition::Constant(
+                        ConstantDefinition {
+                            ty: UnresolvedType::Uint(32).into(),
+                            expression: Expression::U32Constant(T::get_required_bits() as u32)
+                                .into(),
+                        }
+                        .start_end(pos.0, pos.1),
+                    )),
+                },
                s => {
                    return Err(CompileErrorInner::ImportError(
                        Error::new(format!("Embed {} not found", s)).with_pos(Some(pos)),
--- a/zokrates_core/src/ir/mod.rs
+++ b/zokrates_core/src/ir/mod.rs
@ -11,6 +11,8 @@ pub mod folder;
 mod from_flat;
 mod interpreter;
 mod serialize;
+pub mod smtlib2;
+pub mod visitor;
 mod witness;

 pub use self::expression::QuadComb;
--- a/zokrates_core/src/ir/smtlib2.rs
+++ b/zokrates_core/src/ir/smtlib2.rs
@ -0,0 +1,141 @@
+use num_bigint::BigUint;
+use std::collections::BTreeSet;
+
+use super::*;
+use zokrates_field::Field;
+
+use super::expression::LinComb;
+use super::expression::QuadComb;
+use super::visitor::*;
+
+pub trait SMTLib2 {
+    fn to_smtlib2(&self, f: &mut fmt::Formatter) -> fmt::Result;
+}
+
+impl<T: Field> SMTLib2 for Prog<T> {
+    fn to_smtlib2(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        self.main.to_smtlib2(f)
+    }
+}
+
+pub struct SMTLib2Display<'a, T>(pub &'a Prog<T>);
+
+impl<T: Field> fmt::Display for SMTLib2Display<'_, T> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        self.0.to_smtlib2(f)
+    }
+}
+
+struct FlatVariableCollector {
+    variables: BTreeSet<FlatVariable>,
+}
+
+impl<T: Field> Visitor<T> for FlatVariableCollector {
+    fn visit_variable(&mut self, v: &FlatVariable) {
+        self.variables.insert(*v);
+    }
+}
+
+impl<T: Field> SMTLib2 for Function<T> {
+    fn to_smtlib2(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        let mut collector = FlatVariableCollector {
+            variables: BTreeSet::<FlatVariable>::new(),
+        };
+        collector.visit_function(self);
+        collector.variables.insert(FlatVariable::one());
+
+        writeln!(f, "; Auto generated by ZoKrates")?;
+        writeln!(
+            f,
+            "; Number of circuit variables: {}",
+            collector.variables.len()
+        )?;
+        writeln!(f, "; Number of equalities: {}", self.statements.len())?;
+
+        writeln!(f, "(declare-const |~prime| Int)")?;
+        for v in collector.variables.iter() {
+            writeln!(f, "(declare-const |{}| Int)", v)?;
+        }
+
+        writeln!(f, "(assert (and")?;
+        writeln!(f, "(= |~prime| {})", T::max_value().to_biguint() + 1usize)?;
+        writeln!(f, "(= |~one| 1)")?;
+        for s in &self.statements {
+            s.to_smtlib2(f)?;
+            writeln!(f)?;
+        }
+        write!(f, "))")
+    }
+}
+
+fn format_prefix_op_smtlib2<T: SMTLib2, Ts: SMTLib2>(
+    f: &mut fmt::Formatter,
+    op: &str,
+    a: &T,
+    b: &Ts,
+) -> fmt::Result {
+    write!(f, "({} ", op)?;
+    a.to_smtlib2(f)?;
+    write!(f, " ")?;
+    b.to_smtlib2(f)?;
+    write!(f, ")")
+}
+
+impl<T: Field> SMTLib2 for Statement<T> {
+    fn to_smtlib2(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match *self {
+            Statement::Constraint(ref quad, ref lin) => {
+                write!(f, "(= (mod ")?;
+                quad.to_smtlib2(f)?;
+                write!(f, " |~prime|) (mod ")?;
+                lin.to_smtlib2(f)?;
+                write!(f, " |~prime|))")
+            }
+            Statement::Directive(ref s) => s.to_smtlib2(f),
+        }
+    }
+}
+
+impl<T: Field> SMTLib2 for Directive<T> {
+    fn to_smtlib2(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "")
+    }
+}
+
+impl<T: Field> SMTLib2 for QuadComb<T> {
+    fn to_smtlib2(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        format_prefix_op_smtlib2(f, "*", &self.left, &self.right)
+    }
+}
+
+impl<T: Field> SMTLib2 for LinComb<T> {
+    fn to_smtlib2(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match self.is_zero() {
+            true => write!(f, "0"),
+            false => {
+                if self.0.len() > 1 {
+                    write!(f, "(+")?;
+                    for expr in self.0.iter() {
+                        write!(f, " ")?;
+                        format_prefix_op_smtlib2(f, "*", &expr.0, &expr.1.to_biguint())?;
+                    }
+                    write!(f, ")")
+                } else {
+                    format_prefix_op_smtlib2(f, "*", &self.0[0].0, &self.0[0].1.to_biguint())
+                }
+            }
+        }
+    }
+}
+
+impl SMTLib2 for FlatVariable {
+    fn to_smtlib2(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "|{}|", self)
+    }
+}
+
+impl SMTLib2 for BigUint {
+    fn to_smtlib2(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "{}", self)
+    }
+}
--- a/zokrates_core/src/ir/visitor.rs
+++ b/zokrates_core/src/ir/visitor.rs
@ -0,0 +1,98 @@
+// Generic walk through an IR AST. Not mutating in place
+
+use crate::flat_absy::flat_variable::FlatVariable;
+use crate::ir::*;
+use zokrates_field::Field;
+
+pub trait Visitor<T: Field>: Sized {
+    fn visit_module(&mut self, p: &Prog<T>) {
+        visit_module(self, p)
+    }
+
+    fn visit_function(&mut self, f: &Function<T>) {
+        visit_function(self, f)
+    }
+
+    fn visit_argument(&mut self, p: &FlatVariable) {
+        visit_argument(self, p)
+    }
+
+    fn visit_variable(&mut self, v: &FlatVariable) {
+        visit_variable(self, v)
+    }
+
+    fn visit_value(&mut self, v: &T) {
+        visit_value(self, v)
+    }
+
+    fn visit_statement(&mut self, s: &Statement<T>) {
+        visit_statement(self, s)
+    }
+
+    fn visit_linear_combination(&mut self, e: &LinComb<T>) {
+        visit_linear_combination(self, e)
+    }
+
+    fn visit_quadratic_combination(&mut self, es: &QuadComb<T>) {
+        visit_quadratic_combination(self, es)
+    }
+
+    fn visit_directive(&mut self, d: &Directive<T>) {
+        visit_directive(self, d)
+    }
+}
+
+pub fn visit_module<T: Field, F: Visitor<T>>(f: &mut F, p: &Prog<T>) {
+    f.visit_function(&p.main)
+}
+
+pub fn visit_statement<T: Field, F: Visitor<T>>(f: &mut F, s: &Statement<T>) {
+    match s {
+        Statement::Constraint(quad, lin) => {
+            f.visit_quadratic_combination(quad);
+            f.visit_linear_combination(lin);
+        }
+        Statement::Directive(dir) => f.visit_directive(dir),
+    }
+}
+
+pub fn visit_linear_combination<T: Field, F: Visitor<T>>(f: &mut F, e: &LinComb<T>) {
+    for expr in e.0.iter() {
+        f.visit_variable(&expr.0);
+        f.visit_value(&expr.1);
+    }
+}
+
+pub fn visit_quadratic_combination<T: Field, F: Visitor<T>>(f: &mut F, e: &QuadComb<T>) {
+    f.visit_linear_combination(&e.left);
+    f.visit_linear_combination(&e.right);
+}
+
+pub fn visit_directive<T: Field, F: Visitor<T>>(f: &mut F, ds: &Directive<T>) {
+    for expr in ds.inputs.iter() {
+        f.visit_quadratic_combination(expr);
+    }
+    for expr in ds.outputs.iter() {
+        f.visit_variable(expr);
+    }
+}
+
+pub fn visit_function<T: Field, F: Visitor<T>>(f: &mut F, fun: &Function<T>) {
+    for expr in fun.arguments.iter() {
+        f.visit_argument(expr);
+    }
+    for expr in fun.statements.iter() {
+        f.visit_statement(expr);
+    }
+    for expr in fun.returns.iter() {
+        f.visit_variable(expr);
+    }
+}
+
+pub fn visit_argument<T: Field, F: Visitor<T>>(f: &mut F, a: &FlatVariable) {
+    f.visit_variable(a)
+}
+
+pub fn visit_variable<T: Field, F: Visitor<T>>(_f: &mut F, _v: &FlatVariable) {}
+
+pub fn visit_value<T: Field, F: Visitor<T>>(_f: &mut F, _v: &T) {}
--- a/zokrates_core/src/proof_system/libsnark/ffi.rs
+++ b/zokrates_core/src/proof_system/libsnark/ffi.rs
@ -1,6 +1,6 @@
 #[repr(C)]
 pub struct Buffer {
-    pub data: *mut u8,
+    pub data: *const u8,
    pub length: i32,
 }

@ -16,33 +16,17 @@ pub struct ProofResult {
 }

 extern "C" {
-    fn __free(ptr: *mut u8);
+    pub fn c_free(ptr: *const u8);
 }

 impl Buffer {
    pub fn from_vec(v: &Vec<u8>) -> Buffer {
-        let mut buf = vec![0; v.len()].into_boxed_slice();
-        buf.copy_from_slice(v.as_slice());
-
-        let data = buf.as_mut_ptr();
-        let len = buf.len();
-
-        std::mem::forget(buf);
+        let data = v.as_ptr();
+        let len = v.len();

        Buffer {
            data,
            length: len as i32,
        }
    }
-
-    pub unsafe fn drop(&self) {
-        let s = std::slice::from_raw_parts_mut(self.data, self.length as usize);
-        let s = s.as_mut_ptr();
-        Box::from_raw(s);
-    }
-
-    /// The purpose of this function is to free memory allocated by C. Do not use otherwise.
-    pub fn free(self) {
-        unsafe { __free(self.data) };
-    }
 }
--- a/zokrates_core/src/proof_system/libsnark/gm17.rs
+++ b/zokrates_core/src/proof_system/libsnark/gm17.rs
@ -1,6 +1,6 @@
 use crate::ir::{Prog, Witness};
 use crate::proof_system::gm17::{ProofPoints, VerificationKey, GM17};
-use crate::proof_system::libsnark::ffi::{Buffer, ProofResult, SetupResult};
+use crate::proof_system::libsnark::ffi::{c_free, Buffer, ProofResult, SetupResult};
 use crate::proof_system::libsnark::{
    prepare_generate_proof, prepare_public_inputs, prepare_setup, serialization::*, Libsnark,
 };
@ -64,8 +64,8 @@ impl Backend<Bn128Field, GM17> for Libsnark {
                std::slice::from_raw_parts(result.pk.data, result.pk.length as usize).to_vec();

            // free c allocated buffers
-            result.vk.free();
-            result.pk.free();
+            c_free(result.vk.data);
+            c_free(result.pk.data);

            (vk, pk)
        };
@ -104,9 +104,9 @@ impl Backend<Bn128Field, GM17> for Libsnark {
        let (public_inputs_arr, public_inputs_length, private_inputs_arr, private_inputs_length) =
            prepare_generate_proof(program.clone(), witness.clone());

-        let proof = unsafe {
-            let mut pk_buffer = Buffer::from_vec(&proving_key);
+        let mut pk_buffer = Buffer::from_vec(&proving_key);

+        let proof = unsafe {
            let result = gm17_bn128_generate_proof(
                &mut pk_buffer as *mut _,
                public_inputs_arr[0].as_ptr(),
@ -115,14 +115,11 @@ impl Backend<Bn128Field, GM17> for Libsnark {
                private_inputs_length as i32,
            );

-            pk_buffer.drop(); // drop the buffer manually
-
-            let proof: Vec<u8> =
-                std::slice::from_raw_parts(result.proof.data, result.proof.length as usize)
-                    .to_vec();
+            let proof = std::slice::from_raw_parts(result.proof.data, result.proof.length as usize)
+                .to_vec();

            // free c allocated buffer
-            result.proof.free();
+            c_free(result.proof.data);

            proof
        };
@ -175,21 +172,16 @@ impl Backend<Bn128Field, GM17> for Libsnark {

        let (public_inputs_arr, public_inputs_length) = prepare_public_inputs(public_inputs);

-        unsafe {
-            let mut vk_buffer = Buffer::from_vec(vk_writer.get_ref());
-            let mut proof_buffer = Buffer::from_vec(proof_writer.get_ref());
+        let mut vk_buffer = Buffer::from_vec(vk_writer.get_ref());
+        let mut proof_buffer = Buffer::from_vec(proof_writer.get_ref());

-            let ans = gm17_bn128_verify(
+        unsafe {
+            gm17_bn128_verify(
                &mut vk_buffer as *mut _,
                &mut proof_buffer as *mut _,
                public_inputs_arr[0].as_ptr(),
                public_inputs_length as i32,
-            );
-
-            vk_buffer.drop();
-            proof_buffer.drop();
-
-            ans
+            )
        }
    }
 }
--- a/zokrates_core/src/proof_system/libsnark/pghr13.rs
+++ b/zokrates_core/src/proof_system/libsnark/pghr13.rs
@ -1,4 +1,4 @@
-use crate::proof_system::libsnark::ffi::{Buffer, ProofResult, SetupResult};
+use crate::proof_system::libsnark::ffi::{c_free, Buffer, ProofResult, SetupResult};
 use crate::proof_system::libsnark::{
    prepare_generate_proof, prepare_public_inputs, prepare_setup, Libsnark,
 };
@ -67,8 +67,8 @@ impl Backend<Bn128Field, PGHR13> for Libsnark {
                std::slice::from_raw_parts(result.pk.data, result.pk.length as usize).to_vec();

            // free c allocated buffers
-            result.vk.free();
-            result.pk.free();
+            c_free(result.vk.data);
+            c_free(result.pk.data);

            (vk, pk)
        };
@ -111,9 +111,9 @@ impl Backend<Bn128Field, PGHR13> for Libsnark {
        let (public_inputs_arr, public_inputs_length, private_inputs_arr, private_inputs_length) =
            prepare_generate_proof(program.clone(), witness.clone());

-        let proof = unsafe {
-            let mut pk_buffer = Buffer::from_vec(&proving_key);
+        let mut pk_buffer = Buffer::from_vec(&proving_key);

+        let proof = unsafe {
            let result = pghr13_bn128_generate_proof(
                &mut pk_buffer as *mut _,
                public_inputs_arr[0].as_ptr(),
@ -122,14 +122,11 @@ impl Backend<Bn128Field, PGHR13> for Libsnark {
                private_inputs_length as i32,
            );

-            pk_buffer.drop(); // drop the buffer manually
-
-            let proof: Vec<u8> =
-                std::slice::from_raw_parts(result.proof.data, result.proof.length as usize)
-                    .to_vec();
+            let proof = std::slice::from_raw_parts(result.proof.data, result.proof.length as usize)
+                .to_vec();

            // free c allocated buffer
-            result.proof.free();
+            c_free(result.proof.data);

            proof
        };
@ -205,21 +202,16 @@ impl Backend<Bn128Field, PGHR13> for Libsnark {

        let (public_inputs_arr, public_inputs_length) = prepare_public_inputs(public_inputs);

-        unsafe {
-            let mut vk_buffer = Buffer::from_vec(vk_writer.get_ref());
-            let mut proof_buffer = Buffer::from_vec(proof_writer.get_ref());
+        let mut vk_buffer = Buffer::from_vec(vk_writer.get_ref());
+        let mut proof_buffer = Buffer::from_vec(proof_writer.get_ref());

-            let ans = pghr13_bn128_verify(
+        unsafe {
+            pghr13_bn128_verify(
                &mut vk_buffer as *mut _,
                &mut proof_buffer as *mut _,
                public_inputs_arr[0].as_ptr(),
                public_inputs_length as i32,
-            );
-
-            vk_buffer.drop();
-            proof_buffer.drop();
-
-            ans
+            )
        }
    }
 }
--- a/zokrates_core/src/semantics.rs
+++ b/zokrates_core/src/semantics.rs
@ -19,9 +19,9 @@ use crate::parser::Position;
 use crate::absy::types::{UnresolvedSignature, UnresolvedType, UserTypeId};

 use crate::typed_absy::types::{
-    ArrayType, Constant, DeclarationArrayType, DeclarationFunctionKey, DeclarationSignature,
-    DeclarationStructMember, DeclarationStructType, DeclarationType, GenericIdentifier,
-    StructLocation,
+    ArrayType, DeclarationArrayType, DeclarationConstant, DeclarationFunctionKey,
+    DeclarationSignature, DeclarationStructMember, DeclarationStructType, DeclarationType,
+    GenericIdentifier, StructLocation,
 };
 use std::hash::{Hash, Hasher};

@ -350,7 +350,7 @@ impl<'ast, T: Field> Checker<'ast, T> {

    fn check_constant_definition(
        &mut self,
-        id: &'ast str,
+        id: ConstantIdentifier<'ast>,
        c: ConstantDefinitionNode<'ast>,
        module_id: &ModuleId,
        state: &State<'ast, T>,
@ -445,8 +445,8 @@ impl<'ast, T: Field> Checker<'ast, T> {
        declaration: SymbolDeclarationNode<'ast>,
        module_id: &ModuleId,
        state: &mut State<'ast, T>,
-        functions: &mut HashMap<DeclarationFunctionKey<'ast>, TypedFunctionSymbol<'ast, T>>,
-        constants: &mut HashMap<ConstantIdentifier<'ast>, TypedConstantSymbol<'ast, T>>,
+        functions: &mut TypedFunctionSymbols<'ast, T>,
+        constants: &mut TypedConstantSymbols<'ast, T>,
        symbol_unifier: &mut SymbolUnifier<'ast>,
    ) -> Result<(), Vec<Error>> {
        let mut errors: Vec<Error> = vec![];
@ -506,8 +506,13 @@ impl<'ast, T: Field> Checker<'ast, T> {
                                .in_file(module_id),
                            ),
                            true => {
-                                constants
-                                    .insert(declaration.id, TypedConstantSymbol::Here(c.clone()));
+                                constants.push((
+                                    CanonicalConstantIdentifier::new(
+                                        declaration.id,
+                                        module_id.into(),
+                                    ),
+                                    TypedConstantSymbol::Here(c.clone()),
+                                ));
                                self.insert_into_scope(Variable::with_id_and_type(
                                    declaration.id,
                                    c.get_type(),
@ -600,7 +605,9 @@ impl<'ast, T: Field> Checker<'ast, T> {
                            .constants
                            .entry(import.module_id.to_path_buf())
                            .or_default()
-                            .get(import.symbol_id)
+                            .iter()
+                            .find(|(i, _)| *i == &import.symbol_id)
+                            .map(|(_, c)| c)
                            .cloned();

                        match (function_candidates.len(), type_candidate, const_candidate) {
@ -653,7 +660,10 @@ impl<'ast, T: Field> Checker<'ast, T> {
                                            }});
                                    }
                                    true => {
-                                        constants.insert(declaration.id, TypedConstantSymbol::There(import.module_id.to_path_buf(), import.symbol_id));
+                                        let imported_id = CanonicalConstantIdentifier::new(import.symbol_id, import.module_id);
+                                        let id = CanonicalConstantIdentifier::new(declaration.id, module_id.into());
+
+                                        constants.push((id.clone(), TypedConstantSymbol::There(imported_id)));
                                        self.insert_into_scope(Variable::with_id_and_type(declaration.id, ty.clone()));

                                        state
@ -750,8 +760,8 @@ impl<'ast, T: Field> Checker<'ast, T> {
        module_id: &ModuleId,
        state: &mut State<'ast, T>,
    ) -> Result<(), Vec<Error>> {
-        let mut checked_functions = HashMap::new();
-        let mut checked_constants = HashMap::new();
+        let mut checked_functions = TypedFunctionSymbols::new();
+        let mut checked_constants = TypedConstantSymbols::new();

        // check if the module was already removed from the untyped ones
        let to_insert = match state.modules.remove(module_id) {
@ -856,7 +866,7 @@ impl<'ast, T: Field> Checker<'ast, T> {

                    let v = Variable::with_id_and_type(
                        match generic {
-                            Constant::Generic(g) => g.name,
+                            DeclarationConstant::Generic(g) => g.name,
                            _ => unreachable!(),
                        },
                        Type::Uint(UBitwidth::B32),
@ -996,7 +1006,7 @@ impl<'ast, T: Field> Checker<'ast, T> {
            } else {
                match generics_map.insert(g.value, index).is_none() {
                    true => {
-                        generics.push(Some(Constant::Generic(GenericIdentifier {
+                        generics.push(Some(DeclarationConstant::Generic(GenericIdentifier {
                            name: g.value,
                            index,
                        })));
@ -1112,16 +1122,17 @@ impl<'ast, T: Field> Checker<'ast, T> {
    fn check_generic_expression(
        &mut self,
        expr: ExpressionNode<'ast>,
+        module_id: &ModuleId,
        constants_map: &HashMap<ConstantIdentifier<'ast>, Type<'ast, T>>,
        generics_map: &HashMap<Identifier<'ast>, usize>,
-    ) -> Result<Constant<'ast>, ErrorInner> {
+    ) -> Result<DeclarationConstant<'ast>, ErrorInner> {
        let pos = expr.pos();

        match expr.value {
-            Expression::U32Constant(c) => Ok(Constant::Concrete(c)),
+            Expression::U32Constant(c) => Ok(DeclarationConstant::Concrete(c)),
            Expression::IntConstant(c) => {
                if c <= BigUint::from(2u128.pow(32) - 1) {
-                    Ok(Constant::Concrete(
+                    Ok(DeclarationConstant::Concrete(
                        u32::from_str_radix(&c.to_str_radix(16), 16).unwrap(),
                    ))
                } else {
@ -1138,7 +1149,7 @@ impl<'ast, T: Field> Checker<'ast, T> {
                match (constants_map.get(name), generics_map.get(&name)) {
                    (Some(ty), None) => {
                        match ty {
-                            Type::Uint(UBitwidth::B32) => Ok(Constant::Identifier(name, 32usize)),
+                            Type::Uint(UBitwidth::B32) => Ok(DeclarationConstant::Constant(CanonicalConstantIdentifier::new(name, module_id.into()))),
                            _ => Err(ErrorInner {
                                pos: Some(pos),
                                message: format!(
@ -1148,7 +1159,7 @@ impl<'ast, T: Field> Checker<'ast, T> {
                            })
                        }
                    }
-                    (None, Some(index)) => Ok(Constant::Generic(GenericIdentifier { name, index: *index })),
+                    (None, Some(index)) => Ok(DeclarationConstant::Generic(GenericIdentifier { name, index: *index })),
                    _ => Err(ErrorInner {
                        pos: Some(pos),
                        message: format!("Undeclared symbol `{}` in function definition", name)
@ -1182,6 +1193,7 @@ impl<'ast, T: Field> Checker<'ast, T> {
            UnresolvedType::Array(t, size) => {
                let checked_size = self.check_generic_expression(
                    size.clone(),
+                    module_id,
                    state.constants.get(module_id).unwrap_or(&HashMap::new()),
                    generics_map,
                )?;
--- a/zokrates_core/src/static_analysis/bounds_checker.rs
+++ b/zokrates_core/src/static_analysis/bounds_checker.rs
@ -1,85 +0,0 @@
-use crate::typed_absy::result_folder::*;
-use crate::typed_absy::*;
-use zokrates_field::Field;
-
-pub struct BoundsChecker;
-
-pub type Error = String;
-
-impl BoundsChecker {
-    pub fn check<T: Field>(p: TypedProgram<T>) -> Result<TypedProgram<T>, Error> {
-        BoundsChecker.fold_program(p)
-    }
-}
-
-impl<'ast, T: Field> ResultFolder<'ast, T> for BoundsChecker {
-    type Error = Error;
-
-    fn fold_array_expression_inner(
-        &mut self,
-        ty: &ArrayType<'ast, T>,
-        e: ArrayExpressionInner<'ast, T>,
-    ) -> Result<ArrayExpressionInner<'ast, T>, Self::Error> {
-        match e {
-            ArrayExpressionInner::Slice(box array, box from, box to) => {
-                let array = self.fold_array_expression(array)?;
-                let from = self.fold_uint_expression(from)?;
-                let to = self.fold_uint_expression(to)?;
-
-                match (array.ty().size.as_inner(), from.as_inner(), to.as_inner()) {
-                    (
-                        UExpressionInner::Value(size),
-                        UExpressionInner::Value(from),
-                        UExpressionInner::Value(to),
-                    ) => {
-                        if from > to {
-                            return Err(format!(
-                                "Slice is created from an invalid range {}..{}",
-                                from, to
-                            ));
-                        }
-
-                        if from > size {
-                            return Err(format!("Lower bound {} of slice {}[{}..{}] is out of bounds for array of size {}", from, array, from, to, size));
-                        }
-
-                        if to > size {
-                            return Err(format!("Upper bound {} of slice {}[{}..{}] is out of bounds for array of size {}", to, array, from, to, size));
-                        }
-                    }
-                    _ => unreachable!(),
-                };
-
-                Ok(ArrayExpressionInner::Slice(box array, box from, box to))
-            }
-            e => fold_array_expression_inner(self, ty, e),
-        }
-    }
-
-    fn fold_select_expression<
-        E: Expr<'ast, T> + Select<'ast, T> + From<TypedExpression<'ast, T>>,
-    >(
-        &mut self,
-        _: &E::Ty,
-        select: SelectExpression<'ast, T, E>,
-    ) -> Result<SelectOrExpression<'ast, T, E>, Self::Error> {
-        let array = self.fold_array_expression(*select.array)?;
-        let index = self.fold_uint_expression(*select.index)?;
-
-        match (array.ty().size.as_inner(), index.as_inner()) {
-            (UExpressionInner::Value(size), UExpressionInner::Value(index)) => {
-                if index >= size {
-                    return Err(format!(
-                        "Out of bounds access: {}[{}] but {} is of size {}",
-                        array, index, array, size
-                    ));
-                }
-            }
-            _ => unreachable!(),
-        };
-
-        Ok(SelectOrExpression::Select(SelectExpression::new(
-            array, index,
-        )))
-    }
-}
--- a/zokrates_core/src/static_analysis/constant_inliner.rs
+++ b/zokrates_core/src/static_analysis/constant_inliner.rs
@ -1,161 +1,153 @@
-use crate::static_analysis::propagation::Propagator;
+use crate::static_analysis::Propagator;
 use crate::typed_absy::folder::*;
 use crate::typed_absy::result_folder::ResultFolder;
-use crate::typed_absy::types::{Constant, DeclarationStructType, GStructMember};
+use crate::typed_absy::types::DeclarationConstant;
 use crate::typed_absy::*;
 use std::collections::HashMap;
 use std::convert::TryInto;
 use zokrates_field::Field;

-pub struct ConstantInliner<'ast, 'a, T: Field> {
+type ProgramConstants<'ast, T> =
+    HashMap<OwnedTypedModuleId, HashMap<Identifier<'ast>, TypedExpression<'ast, T>>>;
+
+pub struct ConstantInliner<'ast, T> {
    modules: TypedModules<'ast, T>,
    location: OwnedTypedModuleId,
-    propagator: Propagator<'ast, 'a, T>,
+    constants: ProgramConstants<'ast, T>,
 }

-impl<'ast, 'a, T: Field> ConstantInliner<'ast, 'a, T> {
+impl<'ast, 'a, T: Field> ConstantInliner<'ast, T> {
    pub fn new(
        modules: TypedModules<'ast, T>,
        location: OwnedTypedModuleId,
-        propagator: Propagator<'ast, 'a, T>,
+        constants: ProgramConstants<'ast, T>,
    ) -> Self {
        ConstantInliner {
            modules,
            location,
-            propagator,
+            constants,
        }
    }
    pub fn inline(p: TypedProgram<'ast, T>) -> TypedProgram<'ast, T> {
-        let mut constants = HashMap::new();
-        let mut inliner = ConstantInliner::new(
-            p.modules.clone(),
-            p.main.clone(),
-            Propagator::with_constants(&mut constants),
-        );
+        let constants = ProgramConstants::new();
+        let mut inliner = ConstantInliner::new(p.modules.clone(), p.main.clone(), constants);
        inliner.fold_program(p)
    }

-    fn module(&self) -> &TypedModule<'ast, T> {
-        self.modules.get(&self.location).unwrap()
-    }
-
    fn change_location(&mut self, location: OwnedTypedModuleId) -> OwnedTypedModuleId {
        let prev = self.location.clone();
        self.location = location;
+        self.constants.entry(self.location.clone()).or_default();
        prev
    }

-    fn get_constant(&mut self, id: &Identifier) -> Option<TypedConstant<'ast, T>> {
-        self.modules
-            .get(&self.location)
-            .unwrap()
-            .constants
-            .get(id.clone().try_into().unwrap())
-            .cloned()
-            .map(|symbol| self.get_canonical_constant(symbol))
+    fn treated(&self, id: &TypedModuleId) -> bool {
+        self.constants.contains_key(id)
    }

-    fn get_canonical_constant(
-        &mut self,
-        symbol: TypedConstantSymbol<'ast, T>,
-    ) -> TypedConstant<'ast, T> {
-        match symbol {
-            TypedConstantSymbol::There(module_id, id) => {
-                let location = self.change_location(module_id);
-                let symbol = self.module().constants.get(id).cloned().unwrap();
+    fn get_constant(
+        &self,
+        id: &CanonicalConstantIdentifier<'ast>,
+    ) -> Option<TypedExpression<'ast, T>> {
+        self.constants
+            .get(&id.module)
+            .and_then(|constants| constants.get(&id.id.into()))
+            .cloned()
+    }

-                let symbol = self.get_canonical_constant(symbol);
-                let _ = self.change_location(location);
-                symbol
-            }
-            TypedConstantSymbol::Here(tc) => {
-                let tc: TypedConstant<T> = self.fold_constant(tc);
-                TypedConstant {
-                    expression: self.propagator.fold_expression(tc.expression).unwrap(),
-                    ..tc
-                }
-            }
-        }
+    fn get_constant_for_identifier(
+        &self,
+        id: &Identifier<'ast>,
+    ) -> Option<TypedExpression<'ast, T>> {
+        self.constants
+            .get(&self.location)
+            .and_then(|constants| constants.get(&id))
+            .cloned()
    }
 }

-impl<'ast, 'a, T: Field> Folder<'ast, T> for ConstantInliner<'ast, 'a, T> {
-    fn fold_program(&mut self, p: TypedProgram<'ast, T>) -> TypedProgram<'ast, T> {
-        TypedProgram {
-            modules: p
-                .modules
+impl<'ast, T: Field> Folder<'ast, T> for ConstantInliner<'ast, T> {
+    fn fold_module_id(&mut self, id: OwnedTypedModuleId) -> OwnedTypedModuleId {
+        // anytime we encounter a module id, visit the corresponding module if it hasn't been done yet
+        if !self.treated(&id) {
+            let current_m_id = self.change_location(id.clone());
+            let m = self.modules.remove(&id).unwrap();
+            let m = self.fold_module(m);
+            self.modules.insert(id.clone(), m);
+            self.change_location(current_m_id);
+        }
+        id
+    }
+
+    fn fold_module(&mut self, m: TypedModule<'ast, T>) -> TypedModule<'ast, T> {
+        TypedModule {
+            constants: m
+                .constants
                .into_iter()
-                .map(|(module_id, module)| {
-                    self.change_location(module_id.clone());
-                    (module_id, self.fold_module(module))
+                .map(|(id, tc)| {
+                    let constant = match tc {
+                        TypedConstantSymbol::There(imported_id) => {
+                            // visit the imported symbol. This triggers visiting the corresponding module if needed
+                            let imported_id = self.fold_canonical_constant_identifier(imported_id);
+                            // after that, the constant must have been defined defined in the global map. It is already reduced
+                            // to a literal, so running propagation isn't required
+                            self.get_constant(&imported_id).unwrap()
+                        }
+                        TypedConstantSymbol::Here(c) => {
+                            let non_propagated_constant = fold_constant(self, c).expression;
+                            // folding the constant above only reduces it to an expression containing only literals, not to a single literal.
+                            // propagating with an empty map of constants reduces it to a single literal
+                            Propagator::with_constants(&mut HashMap::default())
+                                .fold_expression(non_propagated_constant)
+                                .unwrap()
+                        }
+                    };
+
+                    // add to the constant map. The value added is always a single litteral
+                    self.constants
+                        .get_mut(&self.location)
+                        .unwrap()
+                        .insert(id.id.into(), constant.clone());
+
+                    (
+                        id,
+                        TypedConstantSymbol::Here(TypedConstant {
+                            ty: constant.get_type().clone(),
+                            expression: constant,
+                        }),
+                    )
+                })
+                .collect(),
+            functions: m
+                .functions
+                .into_iter()
+                .map(|(key, fun)| {
+                    (
+                        self.fold_declaration_function_key(key),
+                        self.fold_function_symbol(fun),
+                    )
                })
                .collect(),
-            main: p.main,
        }
    }

-    fn fold_declaration_type(&mut self, t: DeclarationType<'ast>) -> DeclarationType<'ast> {
-        match t {
-            DeclarationType::Array(ref array_ty) => match array_ty.size {
-                Constant::Identifier(name, _) => {
-                    let tc = self.get_constant(&name.into()).unwrap();
-                    let expression: UExpression<'ast, T> = tc.expression.try_into().unwrap();
-                    match expression.inner {
-                        UExpressionInner::Value(v) => DeclarationType::array((
-                            self.fold_declaration_type(*array_ty.ty.clone()),
-                            Constant::Concrete(v as u32),
-                        )),
-                        _ => unreachable!("expected u32 value"),
-                    }
-                }
-                _ => t,
-            },
-            DeclarationType::Struct(struct_ty) => DeclarationType::struc(DeclarationStructType {
-                members: struct_ty
-                    .members
-                    .into_iter()
-                    .map(|m| GStructMember::new(m.id, self.fold_declaration_type(*m.ty)))
-                    .collect(),
-                ..struct_ty
-            }),
-            _ => t,
-        }
-    }
-
-    fn fold_type(&mut self, t: Type<'ast, T>) -> Type<'ast, T> {
-        use self::GType::*;
-        match t {
-            Array(ref array_type) => match &array_type.size.inner {
-                UExpressionInner::Identifier(v) => match self.get_constant(v) {
-                    Some(tc) => {
-                        let expression: UExpression<'ast, T> = tc.expression.try_into().unwrap();
-                        Type::array(GArrayType::new(
-                            self.fold_type(*array_type.ty.clone()),
-                            expression,
-                        ))
-                    }
-                    None => t,
-                },
-                _ => t,
-            },
-            Struct(struct_type) => Type::struc(GStructType {
-                members: struct_type
-                    .members
-                    .into_iter()
-                    .map(|m| GStructMember::new(m.id, self.fold_type(*m.ty)))
-                    .collect(),
-                ..struct_type
-            }),
-            _ => t,
-        }
-    }
-
-    fn fold_constant_symbol(
+    fn fold_declaration_constant(
        &mut self,
-        s: TypedConstantSymbol<'ast, T>,
-    ) -> TypedConstantSymbol<'ast, T> {
-        let tc = self.get_canonical_constant(s);
-        TypedConstantSymbol::Here(tc)
+        c: DeclarationConstant<'ast>,
+    ) -> DeclarationConstant<'ast> {
+        match c {
+            // replace constants by their concrete value in declaration types
+            DeclarationConstant::Constant(id) => {
+                DeclarationConstant::Concrete(match self.get_constant(&id).unwrap() {
+                    TypedExpression::Uint(UExpression {
+                        inner: UExpressionInner::Value(v),
+                        ..
+                    }) => v as u32,
+                    _ => unreachable!("all constants found in declaration types should be reduceable to u32 literals"),
+                })
+            }
+            c => c,
+        }
    }

    fn fold_field_expression(
@ -163,10 +155,12 @@ impl<'ast, 'a, T: Field> Folder<'ast, T> for ConstantInliner<'ast, 'a, T> {
        e: FieldElementExpression<'ast, T>,
    ) -> FieldElementExpression<'ast, T> {
        match e {
-            FieldElementExpression::Identifier(ref id) => match self.get_constant(id) {
-                Some(c) => self.fold_constant(c).try_into().unwrap(),
-                None => fold_field_expression(self, e),
-            },
+            FieldElementExpression::Identifier(ref id) => {
+                match self.get_constant_for_identifier(id) {
+                    Some(c) => c.try_into().unwrap(),
+                    None => fold_field_expression(self, e),
+                }
+            }
            e => fold_field_expression(self, e),
        }
    }
@ -176,8 +170,8 @@ impl<'ast, 'a, T: Field> Folder<'ast, T> for ConstantInliner<'ast, 'a, T> {
        e: BooleanExpression<'ast, T>,
    ) -> BooleanExpression<'ast, T> {
        match e {
-            BooleanExpression::Identifier(ref id) => match self.get_constant(id) {
-                Some(c) => self.fold_constant(c).try_into().unwrap(),
+            BooleanExpression::Identifier(ref id) => match self.get_constant_for_identifier(id) {
+                Some(c) => c.try_into().unwrap(),
                None => fold_boolean_expression(self, e),
            },
            e => fold_boolean_expression(self, e),
@ -190,9 +184,9 @@ impl<'ast, 'a, T: Field> Folder<'ast, T> for ConstantInliner<'ast, 'a, T> {
        e: UExpressionInner<'ast, T>,
    ) -> UExpressionInner<'ast, T> {
        match e {
-            UExpressionInner::Identifier(ref id) => match self.get_constant(id) {
+            UExpressionInner::Identifier(ref id) => match self.get_constant_for_identifier(id) {
                Some(c) => {
-                    let e: UExpression<'ast, T> = self.fold_constant(c).try_into().unwrap();
+                    let e: UExpression<'ast, T> = c.try_into().unwrap();
                    e.into_inner()
                }
                None => fold_uint_expression_inner(self, size, e),
@ -207,13 +201,15 @@ impl<'ast, 'a, T: Field> Folder<'ast, T> for ConstantInliner<'ast, 'a, T> {
        e: ArrayExpressionInner<'ast, T>,
    ) -> ArrayExpressionInner<'ast, T> {
        match e {
-            ArrayExpressionInner::Identifier(ref id) => match self.get_constant(id) {
-                Some(c) => {
-                    let e: ArrayExpression<'ast, T> = self.fold_constant(c).try_into().unwrap();
-                    e.into_inner()
+            ArrayExpressionInner::Identifier(ref id) => {
+                match self.get_constant_for_identifier(id) {
+                    Some(c) => {
+                        let e: ArrayExpression<'ast, T> = c.try_into().unwrap();
+                        e.into_inner()
+                    }
+                    None => fold_array_expression_inner(self, ty, e),
                }
-                None => fold_array_expression_inner(self, ty, e),
-            },
+            }
            e => fold_array_expression_inner(self, ty, e),
        }
    }
@ -224,9 +220,10 @@ impl<'ast, 'a, T: Field> Folder<'ast, T> for ConstantInliner<'ast, 'a, T> {
        e: StructExpressionInner<'ast, T>,
    ) -> StructExpressionInner<'ast, T> {
        match e {
-            StructExpressionInner::Identifier(ref id) => match self.get_constant(id) {
+            StructExpressionInner::Identifier(ref id) => match self.get_constant_for_identifier(id)
+            {
                Some(c) => {
-                    let e: StructExpression<'ast, T> = self.fold_constant(c).try_into().unwrap();
+                    let e: StructExpression<'ast, T> = c.try_into().unwrap();
                    e.into_inner()
                }
                None => fold_struct_expression_inner(self, ty, e),
@ -265,7 +262,7 @@ mod tests {
        };

        let constants: TypedConstantSymbols<_> = vec![(
-            const_id,
+            CanonicalConstantIdentifier::new(const_id, "main".into()),
            TypedConstantSymbol::Here(TypedConstant::new(
                GType::FieldElement,
                TypedExpression::FieldElement(FieldElementExpression::Number(Bn128Field::from(1))),
@ -353,7 +350,7 @@ mod tests {
        };

        let constants: TypedConstantSymbols<_> = vec![(
-            const_id,
+            CanonicalConstantIdentifier::new(const_id, "main".into()),
            TypedConstantSymbol::Here(TypedConstant::new(
                GType::Boolean,
                TypedExpression::Boolean(BooleanExpression::Value(true)),
@ -442,7 +439,7 @@ mod tests {
        };

        let constants: TypedConstantSymbols<_> = vec![(
-            const_id,
+            CanonicalConstantIdentifier::new(const_id, "main".into()),
            TypedConstantSymbol::Here(TypedConstant::new(
                GType::Uint(UBitwidth::B32),
                UExpressionInner::Value(1u128)
@ -543,9 +540,9 @@ mod tests {
        };

        let constants: TypedConstantSymbols<_> = vec![(
-            const_id,
+            CanonicalConstantIdentifier::new(const_id, "main".into()),
            TypedConstantSymbol::Here(TypedConstant::new(
-                GType::FieldElement,
+                GType::array(GArrayType::new(GType::FieldElement, 2usize)),
                TypedExpression::Array(
                    ArrayExpressionInner::Value(
                        vec![
@ -682,7 +679,7 @@ mod tests {
                    .collect(),
                    constants: vec![
                        (
-                            const_a_id,
+                            CanonicalConstantIdentifier::new(const_a_id, "main".into()),
                            TypedConstantSymbol::Here(TypedConstant::new(
                                GType::FieldElement,
                                TypedExpression::FieldElement(FieldElementExpression::Number(
@ -691,7 +688,7 @@ mod tests {
                            )),
                        ),
                        (
-                            const_b_id,
+                            CanonicalConstantIdentifier::new(const_b_id, "main".into()),
                            TypedConstantSymbol::Here(TypedConstant::new(
                                GType::FieldElement,
                                TypedExpression::FieldElement(FieldElementExpression::Add(
@ -740,7 +737,7 @@ mod tests {
                    .collect(),
                    constants: vec![
                        (
-                            const_a_id,
+                            CanonicalConstantIdentifier::new(const_a_id, "main".into()),
                            TypedConstantSymbol::Here(TypedConstant::new(
                                GType::FieldElement,
                                TypedExpression::FieldElement(FieldElementExpression::Number(
@ -749,7 +746,7 @@ mod tests {
                            )),
                        ),
                        (
-                            const_b_id,
+                            CanonicalConstantIdentifier::new(const_b_id, "main".into()),
                            TypedConstantSymbol::Here(TypedConstant::new(
                                GType::FieldElement,
                                TypedExpression::FieldElement(FieldElementExpression::Number(
@ -801,7 +798,7 @@ mod tests {
            .into_iter()
            .collect(),
            constants: vec![(
-                foo_const_id,
+                CanonicalConstantIdentifier::new(foo_const_id, "foo".into()),
                TypedConstantSymbol::Here(TypedConstant::new(
                    GType::FieldElement,
                    TypedExpression::FieldElement(FieldElementExpression::Number(
@ -833,8 +830,11 @@ mod tests {
            .into_iter()
            .collect(),
            constants: vec![(
-                foo_const_id,
-                TypedConstantSymbol::There(OwnedTypedModuleId::from("foo"), foo_const_id),
+                CanonicalConstantIdentifier::new(foo_const_id, "main".into()),
+                TypedConstantSymbol::There(CanonicalConstantIdentifier::new(
+                    foo_const_id,
+                    "foo".into(),
+                )),
            )]
            .into_iter()
            .collect(),
@ -871,7 +871,7 @@ mod tests {
            .into_iter()
            .collect(),
            constants: vec![(
-                foo_const_id,
+                CanonicalConstantIdentifier::new(foo_const_id, "main".into()),
                TypedConstantSymbol::Here(TypedConstant::new(
                    GType::FieldElement,
                    TypedExpression::FieldElement(FieldElementExpression::Number(
--- a/zokrates_core/src/static_analysis/flatten_complex_types.rs
+++ b/zokrates_core/src/static_analysis/flatten_complex_types.rs
@ -577,13 +577,66 @@ fn fold_select_expression<'ast, T: Field, E>(
    let array = f.fold_array_expression(statements_buffer, *select.array);
    let index = f.fold_uint_expression(statements_buffer, *select.index);

-    match index.into_inner() {
-        zir::UExpressionInner::Value(i) => {
-            let start = i as usize * size;
-            let end = start + size;
-            array[start..end].to_vec()
+    match index.as_inner() {
+        zir::UExpressionInner::Value(v) => {
+            let v = *v as usize;
+
+            array[v * size..(v + 1) * size].to_vec()
        }
-        _ => unreachable!(),
+        _ => array
+            .chunks(size)
+            .fold(vec![vec![]; size], |mut acc, e| {
+                acc = acc
+                    .into_iter()
+                    .zip(e)
+                    .map(|(mut a, e)| {
+                        a.push(e);
+                        a
+                    })
+                    .collect();
+                acc
+            })
+            .into_iter()
+            .map(|a| {
+                use crate::zir::Typed;
+
+                let ty = a[0].get_type();
+
+                match ty {
+                    zir::Type::Boolean => zir::BooleanExpression::Select(
+                        a.into_iter()
+                            .map(|e| match e {
+                                zir::ZirExpression::Boolean(e) => e.clone(),
+                                _ => unreachable!(),
+                            })
+                            .collect(),
+                        box index.clone(),
+                    )
+                    .into(),
+                    zir::Type::FieldElement => zir::FieldElementExpression::Select(
+                        a.into_iter()
+                            .map(|e| match e {
+                                zir::ZirExpression::FieldElement(e) => e.clone(),
+                                _ => unreachable!(),
+                            })
+                            .collect(),
+                        box index.clone(),
+                    )
+                    .into(),
+                    zir::Type::Uint(bitwidth) => zir::UExpressionInner::Select(
+                        a.into_iter()
+                            .map(|e| match e {
+                                zir::ZirExpression::Uint(e) => e.clone(),
+                                _ => unreachable!(),
+                            })
+                            .collect(),
+                        box index.clone(),
+                    )
+                    .annotate(bitwidth)
+                    .into(),
+                }
+            })
+            .collect(),
    }
 }

--- a/zokrates_core/src/static_analysis/mod.rs
+++ b/zokrates_core/src/static_analysis/mod.rs
@ -4,7 +4,6 @@
 //! @author Thibaut Schaeffer <thibaut@schaeff.fr>
 //! @date 2018

-mod bounds_checker;
 mod branch_isolator;
 mod constant_inliner;
 mod flat_propagation;
@ -14,10 +13,8 @@ mod reducer;
 mod shift_checker;
 mod uint_optimizer;
 mod unconstrained_vars;
-mod variable_read_remover;
 mod variable_write_remover;

-use self::bounds_checker::BoundsChecker;
 use self::branch_isolator::Isolator;
 use self::flatten_complex_types::Flattener;
 use self::propagation::Propagator;
@ -25,7 +22,6 @@ use self::reducer::reduce_program;
 use self::shift_checker::ShiftChecker;
 use self::uint_optimizer::UintOptimizer;
 use self::unconstrained_vars::UnconstrainedVariableDetector;
-use self::variable_read_remover::VariableReadRemover;
 use self::variable_write_remover::VariableWriteRemover;
 use crate::compile::CompileConfig;
 use crate::flat_absy::FlatProg;
@ -42,25 +38,25 @@ pub trait Analyse {
 #[derive(Debug)]
 pub enum Error {
    Reducer(self::reducer::Error),
-    OutOfBounds(self::bounds_checker::Error),
    Propagation(self::propagation::Error),
+    NonConstantShift(self::shift_checker::Error),
 }

-impl From<self::reducer::Error> for Error {
+impl From<reducer::Error> for Error {
    fn from(e: self::reducer::Error) -> Self {
        Error::Reducer(e)
    }
 }

-impl From<self::bounds_checker::Error> for Error {
-    fn from(e: bounds_checker::Error) -> Self {
-        Error::OutOfBounds(e)
+impl From<propagation::Error> for Error {
+    fn from(e: propagation::Error) -> Self {
+        Error::Propagation(e)
    }
 }

-impl From<self::propagation::Error> for Error {
-    fn from(e: propagation::Error) -> Self {
-        Error::Propagation(e)
+impl From<shift_checker::Error> for Error {
+    fn from(e: shift_checker::Error) -> Self {
+        Error::NonConstantShift(e)
    }
 }

@ -68,8 +64,8 @@ impl fmt::Display for Error {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match self {
            Error::Reducer(e) => write!(f, "{}", e),
-            Error::OutOfBounds(e) => write!(f, "{}", e),
            Error::Propagation(e) => write!(f, "{}", e),
+            Error::NonConstantShift(e) => write!(f, "{}", e),
        }
    }
 }
@ -84,6 +80,7 @@ impl<'ast, T: Field> TypedProgram<'ast, T> {
        } else {
            r
        };
+
        // reduce the program to a single function
        let r = reduce_program(r).map_err(Error::from)?;
        // generate abi
@ -93,10 +90,6 @@ impl<'ast, T: Field> TypedProgram<'ast, T> {
        let r = Propagator::propagate(r).map_err(Error::from)?;
        // remove assignment to variable index
        let r = VariableWriteRemover::apply(r);
-        // remove variable access to complex types
-        let r = VariableReadRemover::apply(r);
-        // check array accesses are in bounds
-        let r = BoundsChecker::check(r).map_err(Error::from)?;
        // detect non constant shifts
        let r = ShiftChecker::check(r).map_err(Error::from)?;
        // convert to zir, removing complex types
--- a/zokrates_core/src/static_analysis/reducer/mod.rs
+++ b/zokrates_core/src/static_analysis/reducer/mod.rs
@ -614,7 +614,7 @@ fn compute_hash<T: Field>(f: &TypedFunction<T>) -> u64 {
 #[cfg(test)]
 mod tests {
    use super::*;
-    use crate::typed_absy::types::Constant;
+    use crate::typed_absy::types::DeclarationConstant;
    use crate::typed_absy::types::DeclarationSignature;
    use crate::typed_absy::{
        ArrayExpression, ArrayExpressionInner, DeclarationFunctionKey, DeclarationType,
@ -834,11 +834,11 @@ mod tests {
            )])
            .inputs(vec![DeclarationType::array((
                DeclarationType::FieldElement,
-                Constant::Generic(GenericIdentifier::with_name("K").index(0)),
+                DeclarationConstant::Generic(GenericIdentifier::with_name("K").index(0)),
            ))])
            .outputs(vec![DeclarationType::array((
                DeclarationType::FieldElement,
-                Constant::Generic(GenericIdentifier::with_name("K").index(0)),
+                DeclarationConstant::Generic(GenericIdentifier::with_name("K").index(0)),
            ))]);

        let foo: TypedFunction<Bn128Field> = TypedFunction {
@ -1053,11 +1053,11 @@ mod tests {
            )])
            .inputs(vec![DeclarationType::array((
                DeclarationType::FieldElement,
-                Constant::Generic(GenericIdentifier::with_name("K").index(0)),
+                DeclarationConstant::Generic(GenericIdentifier::with_name("K").index(0)),
            ))])
            .outputs(vec![DeclarationType::array((
                DeclarationType::FieldElement,
-                Constant::Generic(GenericIdentifier::with_name("K").index(0)),
+                DeclarationConstant::Generic(GenericIdentifier::with_name("K").index(0)),
            ))]);

        let foo: TypedFunction<Bn128Field> = TypedFunction {
@ -1285,11 +1285,11 @@ mod tests {
        let foo_signature = DeclarationSignature::new()
            .inputs(vec![DeclarationType::array((
                DeclarationType::FieldElement,
-                Constant::Generic(GenericIdentifier::with_name("K").index(0)),
+                DeclarationConstant::Generic(GenericIdentifier::with_name("K").index(0)),
            ))])
            .outputs(vec![DeclarationType::array((
                DeclarationType::FieldElement,
-                Constant::Generic(GenericIdentifier::with_name("K").index(0)),
+                DeclarationConstant::Generic(GenericIdentifier::with_name("K").index(0)),
            ))])
            .generics(vec![Some(
                GenericIdentifier::with_name("K").index(0).into(),
@ -1299,7 +1299,7 @@ mod tests {
            arguments: vec![DeclarationVariable::array(
                "a",
                DeclarationType::FieldElement,
-                Constant::Generic(GenericIdentifier::with_name("K").index(0)),
+                DeclarationConstant::Generic(GenericIdentifier::with_name("K").index(0)),
            )
            .into()],
            statements: vec![
@ -1363,7 +1363,7 @@ mod tests {
            arguments: vec![DeclarationVariable::array(
                "a",
                DeclarationType::FieldElement,
-                Constant::Generic(GenericIdentifier::with_name("K").index(0)),
+                DeclarationConstant::Generic(GenericIdentifier::with_name("K").index(0)),
            )
            .into()],
            statements: vec![TypedStatement::Return(vec![
--- a/zokrates_core/src/static_analysis/uint_optimizer.rs
+++ b/zokrates_core/src/static_analysis/uint_optimizer.rs
@ -54,11 +54,38 @@ fn force_no_reduce<T: Field>(e: UExpression<T>) -> UExpression<T> {
 }

 impl<'ast, T: Field> Folder<'ast, T> for UintOptimizer<'ast, T> {
+    fn fold_field_expression(
+        &mut self,
+        e: FieldElementExpression<'ast, T>,
+    ) -> FieldElementExpression<'ast, T> {
+        match e {
+            FieldElementExpression::Select(a, box i) => {
+                let a = a
+                    .into_iter()
+                    .map(|e| self.fold_field_expression(e))
+                    .collect();
+                let i = self.fold_uint_expression(i);
+
+                FieldElementExpression::Select(a, box force_reduce(i))
+            }
+            _ => fold_field_expression(self, e),
+        }
+    }
+
    fn fold_boolean_expression(
        &mut self,
        e: BooleanExpression<'ast, T>,
    ) -> BooleanExpression<'ast, T> {
        match e {
+            BooleanExpression::Select(a, box i) => {
+                let a = a
+                    .into_iter()
+                    .map(|e| self.fold_boolean_expression(e))
+                    .collect();
+                let i = self.fold_uint_expression(i);
+
+                BooleanExpression::Select(a, box force_reduce(i))
+            }
            BooleanExpression::UintEq(box left, box right) => {
                let left = self.fold_uint_expression(left);
                let right = self.fold_uint_expression(right);
@ -133,6 +160,27 @@ impl<'ast, T: Field> Folder<'ast, T> for UintOptimizer<'ast, T> {
                    .cloned()
                    .unwrap_or_else(|| panic!("identifier should have been defined: {}", id)),
            ),
+            Select(values, box index) => {
+                let index = self.fold_uint_expression(index);
+
+                let index = force_reduce(index);
+
+                let values: Vec<_> = values
+                    .into_iter()
+                    .map(|v| force_no_reduce(self.fold_uint_expression(v)))
+                    .collect();
+
+                let max_value = T::try_from(
+                    values
+                        .iter()
+                        .map(|v| v.metadata.as_ref().unwrap().max.to_biguint())
+                        .max()
+                        .unwrap(),
+                )
+                .unwrap();
+
+                UExpression::select(values, index).with_max(max_value)
+            }
            Add(box left, box right) => {
                // reduce the two terms
                let left = self.fold_uint_expression(left);
--- a/zokrates_core/src/static_analysis/variable_read_remover.rs
+++ b/zokrates_core/src/static_analysis/variable_read_remover.rs
@ -1,167 +0,0 @@
-//! Module containing removal of variable access to complex types
-//!
-//! For example:
-//! ```zokrates
-//! a[index]
-//! ```
-//!
-//! Would become
-//! ```zokrates
-//! if(index == 0, a[0], if(index == 1, a[1], ...))
-//! ```
-
-use crate::typed_absy::{folder::*, *};
-use zokrates_field::Field;
-
-pub struct VariableReadRemover<'ast, T: Field> {
-    statements: Vec<TypedStatement<'ast, T>>,
-}
-
-impl<'ast, T: Field> VariableReadRemover<'ast, T> {
-    fn new() -> Self {
-        Self { statements: vec![] }
-    }
-
-    pub fn apply(p: TypedProgram<'ast, T>) -> TypedProgram<'ast, T> {
-        Self::new().fold_program(p)
-    }
-
-    fn select<E: Expr<'ast, T> + Select<'ast, T> + IfElse<'ast, T>>(
-        &mut self,
-        e: SelectExpression<'ast, T, E>,
-    ) -> E::Inner {
-        let a = *e.array;
-        let i = *e.index;
-
-        match i.into_inner() {
-            UExpressionInner::Value(i) => {
-                E::select(a, UExpressionInner::Value(i).annotate(UBitwidth::B32)).into_inner()
-            }
-            i => {
-                let size = match a.get_type().clone() {
-                    Type::Array(array_ty) => match array_ty.size.into_inner() {
-                        UExpressionInner::Value(size) => size as u32,
-                        _ => unreachable!(),
-                    },
-                    _ => unreachable!(),
-                };
-
-                self.statements.push(TypedStatement::Assertion(
-                    (0..size)
-                        .map(|index| {
-                            BooleanExpression::UintEq(
-                                box i.clone().annotate(UBitwidth::B32),
-                                box index.into(),
-                            )
-                        })
-                        .fold(None, |acc, e| match acc {
-                            Some(acc) => Some(BooleanExpression::Or(box acc, box e)),
-                            None => Some(e),
-                        })
-                        .unwrap(),
-                ));
-
-                (0..size)
-                    .map(|i| {
-                        E::select(
-                            a.clone(),
-                            UExpressionInner::Value(i.into()).annotate(UBitwidth::B32),
-                        )
-                    })
-                    .enumerate()
-                    .rev()
-                    .fold(None, |acc, (index, res)| match acc {
-                        Some(acc) => Some(E::if_else(
-                            BooleanExpression::UintEq(
-                                box i.clone().annotate(UBitwidth::B32),
-                                box (index as u32).into(),
-                            ),
-                            res,
-                            acc,
-                        )),
-                        None => Some(res),
-                    })
-                    .unwrap()
-                    .into_inner()
-            }
-        }
-    }
-}
-
-impl<'ast, T: Field> Folder<'ast, T> for VariableReadRemover<'ast, T> {
-    fn fold_select_expression<
-        E: Expr<'ast, T> + Select<'ast, T> + IfElse<'ast, T> + From<TypedExpression<'ast, T>>,
-    >(
-        &mut self,
-        _: &E::Ty,
-        e: SelectExpression<'ast, T, E>,
-    ) -> SelectOrExpression<'ast, T, E> {
-        SelectOrExpression::Expression(self.select(e))
-    }
-
-    fn fold_statement(&mut self, s: TypedStatement<'ast, T>) -> Vec<TypedStatement<'ast, T>> {
-        let s = fold_statement(self, s);
-        self.statements.drain(..).chain(s).collect()
-    }
-}
-
-#[cfg(test)]
-mod tests {
-    use super::*;
-    use zokrates_field::Bn128Field;
-
-    #[test]
-    fn select() {
-        // b = a[i]
-
-        // ->
-
-        // i <= 1 == true
-        // b = if i == 0 then a[0] else if i == 1 then a[1] else 0
-
-        let access: TypedStatement<Bn128Field> = TypedStatement::Definition(
-            TypedAssignee::Identifier(Variable::field_element("b")),
-            FieldElementExpression::select(
-                ArrayExpressionInner::Identifier("a".into()).annotate(Type::FieldElement, 2u32),
-                UExpressionInner::Identifier("i".into()).annotate(UBitwidth::B32),
-            )
-            .into(),
-        );
-
-        assert_eq!(
-            VariableReadRemover::new().fold_statement(access),
-            vec![
-                TypedStatement::Assertion(BooleanExpression::Or(
-                    box BooleanExpression::UintEq(
-                        box UExpressionInner::Identifier("i".into()).annotate(UBitwidth::B32),
-                        box UExpressionInner::Value(0).annotate(UBitwidth::B32)
-                    ),
-                    box BooleanExpression::UintEq(
-                        box UExpressionInner::Identifier("i".into()).annotate(UBitwidth::B32),
-                        box UExpressionInner::Value(1).annotate(UBitwidth::B32)
-                    )
-                )),
-                TypedStatement::Definition(
-                    TypedAssignee::Identifier(Variable::field_element("b")),
-                    FieldElementExpression::if_else(
-                        BooleanExpression::UintEq(
-                            box UExpressionInner::Identifier("i".into()).annotate(UBitwidth::B32),
-                            box UExpressionInner::Value(0).annotate(UBitwidth::B32)
-                        ),
-                        FieldElementExpression::select(
-                            ArrayExpressionInner::Identifier("a".into())
-                                .annotate(Type::FieldElement, 2u32),
-                            0u32,
-                        ),
-                        FieldElementExpression::select(
-                            ArrayExpressionInner::Identifier("a".into())
-                                .annotate(Type::FieldElement, 2u32),
-                            1u32,
-                        )
-                    )
-                    .into()
-                )
-            ]
-        );
-    }
-}
--- a/zokrates_core/src/typed_absy/folder.rs
+++ b/zokrates_core/src/typed_absy/folder.rs
@ -1,6 +1,6 @@
 // Generic walk through a typed AST. Not mutating in place

-use crate::typed_absy::types::{ArrayType, StructMember, StructType};
+use crate::typed_absy::types::*;
 use crate::typed_absy::*;
 use zokrates_field::Field;

@ -80,6 +80,13 @@ pub trait Folder<'ast, T: Field>: Sized {
        fold_signature(self, s)
    }

+    fn fold_declaration_constant(
+        &mut self,
+        c: DeclarationConstant<'ast>,
+    ) -> DeclarationConstant<'ast> {
+        fold_declaration_constant(self, c)
+    }
+
    fn fold_parameter(&mut self, p: DeclarationParameter<'ast>) -> DeclarationParameter<'ast> {
        DeclarationParameter {
            id: self.fold_declaration_variable(p.id),
@ -144,7 +151,40 @@ pub trait Folder<'ast, T: Field>: Sized {
    }

    fn fold_declaration_type(&mut self, t: DeclarationType<'ast>) -> DeclarationType<'ast> {
-        t
+        use self::GType::*;
+
+        match t {
+            Array(array_type) => Array(self.fold_declaration_array_type(array_type)),
+            Struct(struct_type) => Struct(self.fold_declaration_struct_type(struct_type)),
+            t => t,
+        }
+    }
+
+    fn fold_declaration_array_type(
+        &mut self,
+        t: DeclarationArrayType<'ast>,
+    ) -> DeclarationArrayType<'ast> {
+        DeclarationArrayType {
+            ty: box self.fold_declaration_type(*t.ty),
+            size: self.fold_declaration_constant(t.size),
+        }
+    }
+
+    fn fold_declaration_struct_type(
+        &mut self,
+        t: DeclarationStructType<'ast>,
+    ) -> DeclarationStructType<'ast> {
+        DeclarationStructType {
+            members: t
+                .members
+                .into_iter()
+                .map(|m| DeclarationStructMember {
+                    ty: box self.fold_declaration_type(*m.ty),
+                    ..m
+                })
+                .collect(),
+            ..t
+        }
    }

    fn fold_assignee(&mut self, a: TypedAssignee<'ast, T>) -> TypedAssignee<'ast, T> {
@ -175,6 +215,20 @@ pub trait Folder<'ast, T: Field>: Sized {
        }
    }

+    fn fold_canonical_constant_identifier(
+        &mut self,
+        i: CanonicalConstantIdentifier<'ast>,
+    ) -> CanonicalConstantIdentifier<'ast> {
+        CanonicalConstantIdentifier {
+            module: self.fold_module_id(i.module),
+            id: i.id,
+        }
+    }
+
+    fn fold_module_id(&mut self, i: OwnedTypedModuleId) -> OwnedTypedModuleId {
+        i
+    }
+
    fn fold_expression(&mut self, e: TypedExpression<'ast, T>) -> TypedExpression<'ast, T> {
        match e {
            TypedExpression::FieldElement(e) => self.fold_field_expression(e).into(),
@ -316,7 +370,12 @@ pub fn fold_module<'ast, T: Field, F: Folder<'ast, T>>(
        constants: m
            .constants
            .into_iter()
-            .map(|(key, tc)| (key, f.fold_constant_symbol(tc)))
+            .map(|(id, tc)| {
+                (
+                    f.fold_canonical_constant_identifier(id),
+                    f.fold_constant_symbol(tc),
+                )
+            })
            .collect(),
        functions: m
            .functions
@ -901,6 +960,13 @@ fn fold_signature<'ast, T: Field, F: Folder<'ast, T>>(
    }
 }

+fn fold_declaration_constant<'ast, T: Field, F: Folder<'ast, T>>(
+    _: &mut F,
+    c: DeclarationConstant<'ast>,
+) -> DeclarationConstant<'ast> {
+    c
+}
+
 pub fn fold_array_expression<'ast, T: Field, F: Folder<'ast, T>>(
    f: &mut F,
    e: ArrayExpression<'ast, T>,
@ -988,7 +1054,9 @@ pub fn fold_constant_symbol<'ast, T: Field, F: Folder<'ast, T>>(
 ) -> TypedConstantSymbol<'ast, T> {
    match s {
        TypedConstantSymbol::Here(tc) => TypedConstantSymbol::Here(f.fold_constant(tc)),
-        there => there,
+        TypedConstantSymbol::There(id) => {
+            TypedConstantSymbol::There(f.fold_canonical_constant_identifier(id))
+        }
    }
 }

@ -998,7 +1066,10 @@ pub fn fold_function_symbol<'ast, T: Field, F: Folder<'ast, T>>(
 ) -> TypedFunctionSymbol<'ast, T> {
    match s {
        TypedFunctionSymbol::Here(fun) => TypedFunctionSymbol::Here(f.fold_function(fun)),
-        there => there, // by default, do not fold modules recursively
+        TypedFunctionSymbol::There(key) => {
+            TypedFunctionSymbol::There(f.fold_declaration_function_key(key))
+        }
+        s => s,
    }
 }

@ -1023,8 +1094,8 @@ pub fn fold_program<'ast, T: Field, F: Folder<'ast, T>>(
        modules: p
            .modules
            .into_iter()
-            .map(|(module_id, module)| (module_id, f.fold_module(module)))
+            .map(|(module_id, module)| (f.fold_module_id(module_id), f.fold_module(module)))
            .collect(),
-        main: p.main,
+        main: f.fold_module_id(p.main),
    }
 }
--- a/zokrates_core/src/typed_absy/mod.rs
+++ b/zokrates_core/src/typed_absy/mod.rs
@ -19,9 +19,10 @@ mod variable;
 pub use self::identifier::CoreIdentifier;
 pub use self::parameter::{DeclarationParameter, GParameter};
 pub use self::types::{
-    ConcreteFunctionKey, ConcreteSignature, ConcreteType, DeclarationFunctionKey,
-    DeclarationSignature, DeclarationType, GArrayType, GStructType, GType, GenericIdentifier,
-    IntoTypes, Signature, StructType, Type, Types, UBitwidth,
+    CanonicalConstantIdentifier, ConcreteFunctionKey, ConcreteSignature, ConcreteType,
+    ConstantIdentifier, DeclarationFunctionKey, DeclarationSignature, DeclarationType, GArrayType,
+    GStructType, GType, GenericIdentifier, IntoTypes, Signature, StructType, Type, Types,
+    UBitwidth,
 };
 use crate::typed_absy::types::ConcreteGenericsAssignment;

@ -62,17 +63,18 @@ pub type TypedModules<'ast, T> = HashMap<OwnedTypedModuleId, TypedModule<'ast, T
 pub type TypedFunctionSymbols<'ast, T> =
    HashMap<DeclarationFunctionKey<'ast>, TypedFunctionSymbol<'ast, T>>;

-pub type ConstantIdentifier<'ast> = &'ast str;
-
 #[derive(Clone, Debug, PartialEq)]
 pub enum TypedConstantSymbol<'ast, T> {
    Here(TypedConstant<'ast, T>),
-    There(OwnedTypedModuleId, ConstantIdentifier<'ast>),
+    There(CanonicalConstantIdentifier<'ast>),
 }

 /// A collection of `TypedConstantSymbol`s
-pub type TypedConstantSymbols<'ast, T> =
-    HashMap<ConstantIdentifier<'ast>, TypedConstantSymbol<'ast, T>>;
+/// It is still ordered, as we inline the constants in the order they are declared
+pub type TypedConstantSymbols<'ast, T> = Vec<(
+    CanonicalConstantIdentifier<'ast>,
+    TypedConstantSymbol<'ast, T>,
+)>;

 /// A typed program as a collection of modules, one of them being the main
 #[derive(PartialEq, Debug, Clone)]
@ -188,12 +190,17 @@ impl<'ast, T: fmt::Display> fmt::Display for TypedModule<'ast, T> {
        let res = self
            .constants
            .iter()
-            .map(|(key, symbol)| match symbol {
+            .map(|(id, symbol)| match symbol {
                TypedConstantSymbol::Here(ref tc) => {
-                    format!("const {} {} = {}", tc.ty, key, tc.expression)
+                    format!("const {} {} = {}", tc.ty, id.id, tc.expression)
                }
-                TypedConstantSymbol::There(ref module_id, ref id) => {
-                    format!("from \"{}\" import {} as {}", module_id.display(), id, key)
+                TypedConstantSymbol::There(ref imported_id) => {
+                    format!(
+                        "from \"{}\" import {} as {}",
+                        imported_id.module.display(),
+                        imported_id.id,
+                        id.id
+                    )
                }
            })
            .chain(self.functions.iter().map(|(key, symbol)| match symbol {
@ -291,6 +298,7 @@ impl<'ast, T: fmt::Display> fmt::Display for TypedFunction<'ast, T> {

 #[derive(Clone, PartialEq, Debug)]
 pub struct TypedConstant<'ast, T> {
+    // the type is already stored in the TypedExpression, but we want to avoid awkward trait bounds in `fmt::Display`
    pub ty: Type<'ast, T>,
    pub expression: TypedExpression<'ast, T>,
 }
@ -303,6 +311,7 @@ impl<'ast, T> TypedConstant<'ast, T> {

 impl<'ast, T: fmt::Display> fmt::Display for TypedConstant<'ast, T> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        // using `self.expression.get_type()` would be better here but ends up requiring stronger trait bounds
        write!(f, "const {}({})", self.ty, self.expression)
    }
 }
--- a/zokrates_core/src/typed_absy/parameter.rs
+++ b/zokrates_core/src/typed_absy/parameter.rs
@ -1,4 +1,4 @@
-use crate::typed_absy::types::Constant;
+use crate::typed_absy::types::DeclarationConstant;
 use crate::typed_absy::GVariable;
 use std::fmt;

@ -18,7 +18,7 @@ impl<'ast, S> From<GVariable<'ast, S>> for GParameter<'ast, S> {
    }
 }

-pub type DeclarationParameter<'ast> = GParameter<'ast, Constant<'ast>>;
+pub type DeclarationParameter<'ast> = GParameter<'ast, DeclarationConstant<'ast>>;

 impl<'ast, S: fmt::Display + Clone> fmt::Display for GParameter<'ast, S> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
--- a/zokrates_core/src/typed_absy/result_folder.rs
+++ b/zokrates_core/src/typed_absy/result_folder.rs
@ -1,6 +1,6 @@
 // Generic walk through a typed AST. Not mutating in place

-use crate::typed_absy::types::{ArrayType, StructMember, StructType};
+use crate::typed_absy::types::*;
 use crate::typed_absy::*;
 use zokrates_field::Field;

@ -97,6 +97,13 @@ pub trait ResultFolder<'ast, T: Field>: Sized {
        fold_signature(self, s)
    }

+    fn fold_declaration_constant(
+        &mut self,
+        c: DeclarationConstant<'ast>,
+    ) -> Result<DeclarationConstant<'ast>, Self::Error> {
+        fold_declaration_constant(self, c)
+    }
+
    fn fold_parameter(
        &mut self,
        p: DeclarationParameter<'ast>,
@ -107,6 +114,20 @@ pub trait ResultFolder<'ast, T: Field>: Sized {
        })
    }

+    fn fold_canonical_constant_identifier(
+        &mut self,
+        i: CanonicalConstantIdentifier<'ast>,
+    ) -> Result<CanonicalConstantIdentifier<'ast>, Self::Error> {
+        Ok(CanonicalConstantIdentifier {
+            module: self.fold_module_id(i.module)?,
+            id: i.id,
+        })
+    }
+
+    fn fold_module_id(&mut self, i: OwnedTypedModuleId) -> Result<OwnedTypedModuleId, Self::Error> {
+        Ok(i)
+    }
+
    fn fold_name(&mut self, n: Identifier<'ast>) -> Result<Identifier<'ast>, Self::Error> {
        Ok(n)
    }
@ -224,6 +245,34 @@ pub trait ResultFolder<'ast, T: Field>: Sized {
        Ok(t)
    }

+    fn fold_declaration_array_type(
+        &mut self,
+        t: DeclarationArrayType<'ast>,
+    ) -> Result<DeclarationArrayType<'ast>, Self::Error> {
+        Ok(DeclarationArrayType {
+            ty: box self.fold_declaration_type(*t.ty)?,
+            size: self.fold_declaration_constant(t.size)?,
+        })
+    }
+
+    fn fold_declaration_struct_type(
+        &mut self,
+        t: DeclarationStructType<'ast>,
+    ) -> Result<DeclarationStructType<'ast>, Self::Error> {
+        Ok(DeclarationStructType {
+            members: t
+                .members
+                .into_iter()
+                .map(|m| {
+                    let id = m.id;
+                    self.fold_declaration_type(*m.ty)
+                        .map(|ty| DeclarationStructMember { ty: box ty, id })
+                })
+                .collect::<Result<_, _>>()?,
+            ..t
+        })
+    }
+
    fn fold_assignee(
        &mut self,
        a: TypedAssignee<'ast, T>,
@ -909,6 +958,7 @@ pub fn fold_declaration_function_key<'ast, T: Field, F: ResultFolder<'ast, T>>(
    key: DeclarationFunctionKey<'ast>,
 ) -> Result<DeclarationFunctionKey<'ast>, F::Error> {
    Ok(DeclarationFunctionKey {
+        module: f.fold_module_id(key.module)?,
        signature: f.fold_signature(key.signature)?,
        ..key
    })
@ -955,6 +1005,13 @@ fn fold_signature<'ast, T: Field, F: ResultFolder<'ast, T>>(
    })
 }

+fn fold_declaration_constant<'ast, T: Field, F: ResultFolder<'ast, T>>(
+    _: &mut F,
+    c: DeclarationConstant<'ast>,
+) -> Result<DeclarationConstant<'ast>, F::Error> {
+    Ok(c)
+}
+
 pub fn fold_array_expression<'ast, T: Field, F: ResultFolder<'ast, T>>(
    f: &mut F,
    e: ArrayExpression<'ast, T>,
@ -1046,7 +1103,9 @@ pub fn fold_constant_symbol<'ast, T: Field, F: ResultFolder<'ast, T>>(
 ) -> Result<TypedConstantSymbol<'ast, T>, F::Error> {
    match s {
        TypedConstantSymbol::Here(tc) => Ok(TypedConstantSymbol::Here(f.fold_constant(tc)?)),
-        there => Ok(there),
+        TypedConstantSymbol::There(id) => Ok(TypedConstantSymbol::There(
+            f.fold_canonical_constant_identifier(id)?,
+        )),
    }
 }

@ -1056,7 +1115,10 @@ pub fn fold_function_symbol<'ast, T: Field, F: ResultFolder<'ast, T>>(
 ) -> Result<TypedFunctionSymbol<'ast, T>, F::Error> {
    match s {
        TypedFunctionSymbol::Here(fun) => Ok(TypedFunctionSymbol::Here(f.fold_function(fun)?)),
-        there => Ok(there), // by default, do not fold modules recursively
+        TypedFunctionSymbol::There(key) => Ok(TypedFunctionSymbol::There(
+            f.fold_declaration_function_key(key)?,
+        )),
+        s => Ok(s),
    }
 }

@ -1088,6 +1150,6 @@ pub fn fold_program<'ast, T: Field, F: ResultFolder<'ast, T>>(
            .into_iter()
            .map(|(module_id, module)| f.fold_module(module).map(|m| (module_id, m)))
            .collect::<Result<_, _>>()?,
-        main: p.main,
+        main: f.fold_module_id(p.main)?,
    })
 }
--- a/zokrates_core/src/typed_absy/types.rs
+++ b/zokrates_core/src/typed_absy/types.rs
@ -101,37 +101,51 @@ impl<'ast> fmt::Display for GenericIdentifier<'ast> {
 #[derive(Debug)]
 pub struct SpecializationError;

+pub type ConstantIdentifier<'ast> = &'ast str;
+
+#[derive(Clone, PartialEq, Eq, Debug, Hash, PartialOrd, Ord)]
+pub struct CanonicalConstantIdentifier<'ast> {
+    pub module: OwnedTypedModuleId,
+    pub id: ConstantIdentifier<'ast>,
+}
+
+impl<'ast> CanonicalConstantIdentifier<'ast> {
+    pub fn new(id: ConstantIdentifier<'ast>, module: OwnedTypedModuleId) -> Self {
+        CanonicalConstantIdentifier { module, id }
+    }
+}
+
 #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub enum Constant<'ast> {
+pub enum DeclarationConstant<'ast> {
    Generic(GenericIdentifier<'ast>),
    Concrete(u32),
-    Identifier(&'ast str, usize),
+    Constant(CanonicalConstantIdentifier<'ast>),
 }

-impl<'ast> From<u32> for Constant<'ast> {
+impl<'ast> From<u32> for DeclarationConstant<'ast> {
    fn from(e: u32) -> Self {
-        Constant::Concrete(e)
+        DeclarationConstant::Concrete(e)
    }
 }

-impl<'ast> From<usize> for Constant<'ast> {
+impl<'ast> From<usize> for DeclarationConstant<'ast> {
    fn from(e: usize) -> Self {
-        Constant::Concrete(e as u32)
+        DeclarationConstant::Concrete(e as u32)
    }
 }

-impl<'ast> From<GenericIdentifier<'ast>> for Constant<'ast> {
+impl<'ast> From<GenericIdentifier<'ast>> for DeclarationConstant<'ast> {
    fn from(e: GenericIdentifier<'ast>) -> Self {
-        Constant::Generic(e)
+        DeclarationConstant::Generic(e)
    }
 }

-impl<'ast> fmt::Display for Constant<'ast> {
+impl<'ast> fmt::Display for DeclarationConstant<'ast> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match self {
-            Constant::Generic(i) => write!(f, "{}", i),
-            Constant::Concrete(v) => write!(f, "{}", v),
-            Constant::Identifier(v, _) => write!(f, "{}", v),
+            DeclarationConstant::Generic(i) => write!(f, "{}", i),
+            DeclarationConstant::Concrete(v) => write!(f, "{}", v),
+            DeclarationConstant::Constant(v) => write!(f, "{}/{}", v.module.display(), v.id),
        }
    }
 }
@ -142,15 +156,17 @@ impl<'ast, T> From<usize> for UExpression<'ast, T> {
    }
 }

-impl<'ast, T> From<Constant<'ast>> for UExpression<'ast, T> {
-    fn from(c: Constant<'ast>) -> Self {
+impl<'ast, T> From<DeclarationConstant<'ast>> for UExpression<'ast, T> {
+    fn from(c: DeclarationConstant<'ast>) -> Self {
        match c {
-            Constant::Generic(i) => {
+            DeclarationConstant::Generic(i) => {
                UExpressionInner::Identifier(i.name.into()).annotate(UBitwidth::B32)
            }
-            Constant::Concrete(v) => UExpressionInner::Value(v as u128).annotate(UBitwidth::B32),
-            Constant::Identifier(v, size) => {
-                UExpressionInner::Identifier(Identifier::from(v)).annotate(UBitwidth::from(size))
+            DeclarationConstant::Concrete(v) => {
+                UExpressionInner::Value(v as u128).annotate(UBitwidth::B32)
+            }
+            DeclarationConstant::Constant(v) => {
+                UExpressionInner::Identifier(Identifier::from(v.id)).annotate(UBitwidth::B32)
            }
        }
    }
@ -169,12 +185,12 @@ impl<'ast, T> TryInto<usize> for UExpression<'ast, T> {
    }
 }

-impl<'ast> TryInto<usize> for Constant<'ast> {
+impl<'ast> TryInto<usize> for DeclarationConstant<'ast> {
    type Error = SpecializationError;

    fn try_into(self) -> Result<usize, Self::Error> {
        match self {
-            Constant::Concrete(v) => Ok(v as usize),
+            DeclarationConstant::Concrete(v) => Ok(v as usize),
            _ => Err(SpecializationError),
        }
    }
@ -190,7 +206,7 @@ pub struct GStructMember<S> {
    pub ty: Box<GType<S>>,
 }

-pub type DeclarationStructMember<'ast> = GStructMember<Constant<'ast>>;
+pub type DeclarationStructMember<'ast> = GStructMember<DeclarationConstant<'ast>>;
 pub type ConcreteStructMember = GStructMember<usize>;
 pub type StructMember<'ast, T> = GStructMember<UExpression<'ast, T>>;

@ -242,7 +258,7 @@ pub struct GArrayType<S> {
    pub ty: Box<GType<S>>,
 }

-pub type DeclarationArrayType<'ast> = GArrayType<Constant<'ast>>;
+pub type DeclarationArrayType<'ast> = GArrayType<DeclarationConstant<'ast>>;
 pub type ConcreteArrayType = GArrayType<usize>;
 pub type ArrayType<'ast, T> = GArrayType<UExpression<'ast, T>>;

@ -250,7 +266,7 @@ impl<'ast, T: PartialEq> PartialEq<DeclarationArrayType<'ast>> for ArrayType<'as
    fn eq(&self, other: &DeclarationArrayType<'ast>) -> bool {
        *self.ty == *other.ty
            && match (self.size.as_inner(), &other.size) {
-                (UExpressionInner::Value(l), Constant::Concrete(r)) => *l as u32 == *r,
+                (UExpressionInner::Value(l), DeclarationConstant::Concrete(r)) => *l as u32 == *r,
                _ => true,
            }
    }
@ -349,7 +365,7 @@ pub struct GStructType<S> {
    pub members: Vec<GStructMember<S>>,
 }

-pub type DeclarationStructType<'ast> = GStructType<Constant<'ast>>;
+pub type DeclarationStructType<'ast> = GStructType<DeclarationConstant<'ast>>;
 pub type ConcreteStructType = GStructType<usize>;
 pub type StructType<'ast, T> = GStructType<UExpression<'ast, T>>;

@ -588,7 +604,7 @@ impl<'de, S: Deserialize<'de>> Deserialize<'de> for GType<S> {
    }
 }

-pub type DeclarationType<'ast> = GType<Constant<'ast>>;
+pub type DeclarationType<'ast> = GType<DeclarationConstant<'ast>>;
 pub type ConcreteType = GType<usize>;
 pub type Type<'ast, T> = GType<UExpression<'ast, T>>;

@ -711,7 +727,7 @@ impl<'ast, T: fmt::Display + PartialEq + fmt::Debug> Type<'ast, T> {
                        // check the size if types match
                        match (&l.size.as_inner(), &r.size) {
                            // compare the sizes for concrete ones
-                            (UExpressionInner::Value(v), Constant::Concrete(c)) => {
+                            (UExpressionInner::Value(v), DeclarationConstant::Concrete(c)) => {
                                (*v as u32) == *c
                            }
                            _ => true,
@ -772,7 +788,7 @@ pub struct GFunctionKey<'ast, S> {
    pub signature: GSignature<S>,
 }

-pub type DeclarationFunctionKey<'ast> = GFunctionKey<'ast, Constant<'ast>>;
+pub type DeclarationFunctionKey<'ast> = GFunctionKey<'ast, DeclarationConstant<'ast>>;
 pub type ConcreteFunctionKey<'ast> = GFunctionKey<'ast, usize>;
 pub type FunctionKey<'ast, T> = GFunctionKey<'ast, UExpression<'ast, T>>;

@ -948,7 +964,7 @@ pub mod signature {
        }
    }

-    pub type DeclarationSignature<'ast> = GSignature<Constant<'ast>>;
+    pub type DeclarationSignature<'ast> = GSignature<DeclarationConstant<'ast>>;
    pub type ConcreteSignature = GSignature<usize>;
    pub type Signature<'ast, T> = GSignature<UExpression<'ast, T>>;

@ -968,15 +984,17 @@ pub mod signature {
                    && match &t0.size {
                        // if the declared size is an identifier, we insert into the map, or check if the concrete size
                        // matches if this identifier is already in the map
-                        Constant::Generic(id) => match constants.0.entry(id.clone()) {
+                        DeclarationConstant::Generic(id) => match constants.0.entry(id.clone()) {
                            Entry::Occupied(e) => *e.get() == s1,
                            Entry::Vacant(e) => {
                                e.insert(s1);
                                true
                            }
                        },
-                        Constant::Concrete(s0) => s1 == *s0 as usize,
-                        Constant::Identifier(_, s0) => s1 == *s0,
+                        DeclarationConstant::Concrete(s0) => s1 == *s0 as usize,
+                        // in the case of a constant, we do not know the value yet, so we optimistically assume it's correct
+                        // if it does not match, it will be caught during inlining
+                        DeclarationConstant::Constant(..) => true,
                    }
            }
            (DeclarationType::FieldElement, GType::FieldElement)
@ -1000,9 +1018,11 @@ pub mod signature {

                let ty = box specialize_type(*t0.ty, &constants)?;
                let size = match t0.size {
-                    Constant::Generic(s) => constants.0.get(&s).cloned().ok_or(s),
-                    Constant::Concrete(s) => Ok(s.into()),
-                    Constant::Identifier(_, s) => Ok((s as u32).into()),
+                    DeclarationConstant::Generic(s) => constants.0.get(&s).cloned().ok_or(s),
+                    DeclarationConstant::Concrete(s) => Ok(s.into()),
+                    DeclarationConstant::Constant(..) => {
+                        unreachable!("identifiers should have been removed in constant inlining")
+                    }
                }?;

                GType::Array(GArrayType { size, ty })
@ -1053,7 +1073,7 @@ pub mod signature {
            assert_eq!(self.generics.len(), values.len());

            let decl_generics = self.generics.iter().map(|g| match g.clone().unwrap() {
-                Constant::Generic(g) => g,
+                DeclarationConstant::Generic(g) => g,
                _ => unreachable!(),
            });

@ -1096,7 +1116,7 @@ pub mod signature {
                    v.map(|v| {
                        (
                            match g.clone().unwrap() {
-                                Constant::Generic(g) => g,
+                                DeclarationConstant::Generic(g) => g,
                                _ => unreachable!(),
                            },
                            v,
--- a/zokrates_core/src/typed_absy/variable.rs
+++ b/zokrates_core/src/typed_absy/variable.rs
@ -1,4 +1,4 @@
-use crate::typed_absy::types::{Constant, GStructType, UBitwidth};
+use crate::typed_absy::types::{DeclarationConstant, GStructType, UBitwidth};
 use crate::typed_absy::types::{GType, SpecializationError};
 use crate::typed_absy::Identifier;
 use crate::typed_absy::UExpression;
@ -11,7 +11,7 @@ pub struct GVariable<'ast, S> {
    pub _type: GType<S>,
 }

-pub type DeclarationVariable<'ast> = GVariable<'ast, Constant<'ast>>;
+pub type DeclarationVariable<'ast> = GVariable<'ast, DeclarationConstant<'ast>>;
 pub type ConcreteVariable<'ast> = GVariable<'ast, usize>;
 pub type Variable<'ast, T> = GVariable<'ast, UExpression<'ast, T>>;

--- a/zokrates_core/src/zir/folder.rs
+++ b/zokrates_core/src/zir/folder.rs
@ -133,6 +133,10 @@ pub fn fold_field_expression<'ast, T: Field, F: Folder<'ast, T>>(
        FieldElementExpression::Identifier(id) => {
            FieldElementExpression::Identifier(f.fold_name(id))
        }
+        FieldElementExpression::Select(a, box i) => FieldElementExpression::Select(
+            a.into_iter().map(|a| f.fold_field_expression(a)).collect(),
+            box f.fold_uint_expression(i),
+        ),
        FieldElementExpression::Add(box e1, box e2) => {
            let e1 = f.fold_field_expression(e1);
            let e2 = f.fold_field_expression(e2);
@ -174,6 +178,12 @@ pub fn fold_boolean_expression<'ast, T: Field, F: Folder<'ast, T>>(
    match e {
        BooleanExpression::Value(v) => BooleanExpression::Value(v),
        BooleanExpression::Identifier(id) => BooleanExpression::Identifier(f.fold_name(id)),
+        BooleanExpression::Select(a, box i) => BooleanExpression::Select(
+            a.into_iter()
+                .map(|a| f.fold_boolean_expression(a))
+                .collect(),
+            box f.fold_uint_expression(i),
+        ),
        BooleanExpression::FieldEq(box e1, box e2) => {
            let e1 = f.fold_field_expression(e1);
            let e2 = f.fold_field_expression(e2);
@ -270,6 +280,10 @@ pub fn fold_uint_expression_inner<'ast, T: Field, F: Folder<'ast, T>>(
    match e {
        UExpressionInner::Value(v) => UExpressionInner::Value(v),
        UExpressionInner::Identifier(id) => UExpressionInner::Identifier(f.fold_name(id)),
+        UExpressionInner::Select(a, box i) => UExpressionInner::Select(
+            a.into_iter().map(|a| f.fold_uint_expression(a)).collect(),
+            box f.fold_uint_expression(i),
+        ),
        UExpressionInner::Add(box left, box right) => {
            let left = f.fold_uint_expression(left);
            let right = f.fold_uint_expression(right);
--- a/zokrates_core/src/zir/mod.rs
+++ b/zokrates_core/src/zir/mod.rs
@ -259,10 +259,11 @@ pub enum ZirExpressionList<'ast, T> {
 }

 /// An expression of type `field`
-#[derive(Clone, PartialEq, Hash, Eq)]
+#[derive(Clone, PartialEq, Hash, Eq, Debug)]
 pub enum FieldElementExpression<'ast, T> {
    Number(T),
    Identifier(Identifier<'ast>),
+    Select(Vec<Self>, Box<UExpression<'ast, T>>),
    Add(
        Box<FieldElementExpression<'ast, T>>,
        Box<FieldElementExpression<'ast, T>>,
@ -291,10 +292,11 @@ pub enum FieldElementExpression<'ast, T> {
 }

 /// An expression of type `bool`
-#[derive(Clone, PartialEq, Hash, Eq)]
+#[derive(Clone, PartialEq, Hash, Eq, Debug)]
 pub enum BooleanExpression<'ast, T> {
    Identifier(Identifier<'ast>),
    Value(bool),
+    Select(Vec<Self>, Box<UExpression<'ast, T>>),
    FieldLt(
        Box<FieldElementExpression<'ast, T>>,
        Box<FieldElementExpression<'ast, T>>,
@ -411,6 +413,15 @@ impl<'ast, T: fmt::Display> fmt::Display for FieldElementExpression<'ast, T> {
        match *self {
            FieldElementExpression::Number(ref i) => write!(f, "{}", i),
            FieldElementExpression::Identifier(ref var) => write!(f, "{}", var),
+            FieldElementExpression::Select(ref a, ref i) => write!(
+                f,
+                "[{}][{}]",
+                a.iter()
+                    .map(|a| a.to_string())
+                    .collect::<Vec<_>>()
+                    .join(", "),
+                i
+            ),
            FieldElementExpression::Add(ref lhs, ref rhs) => write!(f, "({} + {})", lhs, rhs),
            FieldElementExpression::Sub(ref lhs, ref rhs) => write!(f, "({} - {})", lhs, rhs),
            FieldElementExpression::Mult(ref lhs, ref rhs) => write!(f, "({} * {})", lhs, rhs),
@ -432,6 +443,15 @@ impl<'ast, T: fmt::Display> fmt::Display for UExpression<'ast, T> {
        match self.inner {
            UExpressionInner::Value(ref v) => write!(f, "{}", v),
            UExpressionInner::Identifier(ref var) => write!(f, "{}", var),
+            UExpressionInner::Select(ref a, ref i) => write!(
+                f,
+                "[{}][{}]",
+                a.iter()
+                    .map(|a| a.to_string())
+                    .collect::<Vec<_>>()
+                    .join(", "),
+                i
+            ),
            UExpressionInner::Add(ref lhs, ref rhs) => write!(f, "({} + {})", lhs, rhs),
            UExpressionInner::Sub(ref lhs, ref rhs) => write!(f, "({} - {})", lhs, rhs),
            UExpressionInner::Mult(ref lhs, ref rhs) => write!(f, "({} * {})", lhs, rhs),
@ -457,6 +477,15 @@ impl<'ast, T: fmt::Display> fmt::Display for BooleanExpression<'ast, T> {
        match *self {
            BooleanExpression::Identifier(ref var) => write!(f, "{}", var),
            BooleanExpression::Value(b) => write!(f, "{}", b),
+            BooleanExpression::Select(ref a, ref i) => write!(
+                f,
+                "[{}][{}]",
+                a.iter()
+                    .map(|a| a.to_string())
+                    .collect::<Vec<_>>()
+                    .join(", "),
+                i
+            ),
            BooleanExpression::FieldLt(ref lhs, ref rhs) => write!(f, "{} < {}", lhs, rhs),
            BooleanExpression::FieldLe(ref lhs, ref rhs) => write!(f, "{} <= {}", lhs, rhs),
            BooleanExpression::FieldGe(ref lhs, ref rhs) => write!(f, "{} >= {}", lhs, rhs),
@ -480,79 +509,6 @@ impl<'ast, T: fmt::Display> fmt::Display for BooleanExpression<'ast, T> {
    }
 }

-impl<'ast, T: fmt::Debug> fmt::Debug for BooleanExpression<'ast, T> {
-    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        match *self {
-            BooleanExpression::Identifier(ref var) => write!(f, "Ide({:?})", var),
-            BooleanExpression::Value(b) => write!(f, "Value({})", b),
-            BooleanExpression::FieldLt(ref lhs, ref rhs) => {
-                write!(f, "FieldLt({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::FieldLe(ref lhs, ref rhs) => {
-                write!(f, "FieldLe({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::FieldGe(ref lhs, ref rhs) => {
-                write!(f, "FieldGe({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::FieldGt(ref lhs, ref rhs) => {
-                write!(f, "FieldGt({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::UintLt(ref lhs, ref rhs) => {
-                write!(f, "UintLt({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::UintLe(ref lhs, ref rhs) => {
-                write!(f, "UintLe({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::UintGe(ref lhs, ref rhs) => {
-                write!(f, "UintGe({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::UintGt(ref lhs, ref rhs) => {
-                write!(f, "UintGt({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::FieldEq(ref lhs, ref rhs) => {
-                write!(f, "FieldEq({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::BoolEq(ref lhs, ref rhs) => {
-                write!(f, "BoolEq({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::UintEq(ref lhs, ref rhs) => {
-                write!(f, "UintEq({:?}, {:?})", lhs, rhs)
-            }
-            BooleanExpression::Or(ref lhs, ref rhs) => write!(f, "Or({:?}, {:?})", lhs, rhs),
-            BooleanExpression::And(ref lhs, ref rhs) => write!(f, "And({:?}, {:?})", lhs, rhs),
-            BooleanExpression::Not(ref exp) => write!(f, "Not({:?})", exp),
-            BooleanExpression::IfElse(ref condition, ref consequent, ref alternative) => write!(
-                f,
-                "IfElse({:?}, {:?}, {:?})",
-                condition, consequent, alternative
-            ),
-        }
-    }
-}
-
-impl<'ast, T: fmt::Debug> fmt::Debug for FieldElementExpression<'ast, T> {
-    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        match *self {
-            FieldElementExpression::Number(ref i) => write!(f, "Num({:?})", i),
-            FieldElementExpression::Identifier(ref var) => write!(f, "Ide({:?})", var),
-            FieldElementExpression::Add(ref lhs, ref rhs) => write!(f, "Add({:?}, {:?})", lhs, rhs),
-            FieldElementExpression::Sub(ref lhs, ref rhs) => write!(f, "Sub({:?}, {:?})", lhs, rhs),
-            FieldElementExpression::Mult(ref lhs, ref rhs) => {
-                write!(f, "Mult({:?}, {:?})", lhs, rhs)
-            }
-            FieldElementExpression::Div(ref lhs, ref rhs) => write!(f, "Div({:?}, {:?})", lhs, rhs),
-            FieldElementExpression::Pow(ref lhs, ref rhs) => write!(f, "Pow({:?}, {:?})", lhs, rhs),
-            FieldElementExpression::IfElse(ref condition, ref consequent, ref alternative) => {
-                write!(
-                    f,
-                    "IfElse({:?}, {:?}, {:?})",
-                    condition, consequent, alternative
-                )
-            }
-        }
-    }
-}
-
 impl<'ast, T: fmt::Display> fmt::Display for ZirExpressionList<'ast, T> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match *self {
--- a/zokrates_core/src/zir/uint.rs
+++ b/zokrates_core/src/zir/uint.rs
@ -16,6 +16,11 @@ impl<'ast, T: Field> UExpression<'ast, T> {
        UExpressionInner::Sub(box self, box other).annotate(bitwidth)
    }

+    pub fn select(values: Vec<Self>, index: Self) -> UExpression<'ast, T> {
+        let bitwidth = values[0].bitwidth;
+        UExpressionInner::Select(values, box index).annotate(bitwidth)
+    }
+
    pub fn mult(self, other: Self) -> UExpression<'ast, T> {
        let bitwidth = self.bitwidth;
        assert_eq!(bitwidth, other.bitwidth);
@ -160,6 +165,7 @@ pub struct UExpression<'ast, T> {
 pub enum UExpressionInner<'ast, T> {
    Identifier(Identifier<'ast>),
    Value(u128),
+    Select(Vec<UExpression<'ast, T>>, Box<UExpression<'ast, T>>),
    Add(Box<UExpression<'ast, T>>, Box<UExpression<'ast, T>>),
    Sub(Box<UExpression<'ast, T>>, Box<UExpression<'ast, T>>),
    Mult(Box<UExpression<'ast, T>>, Box<UExpression<'ast, T>>),
--- a/zokrates_core_test/tests/tests/arrays/identity.json
+++ b/zokrates_core_test/tests/tests/arrays/identity.json
@ -1,5 +1,5 @@
 {
-	"entry_point": "./tests/tests/arrays/identity.code",
+	"entry_point": "./tests/tests/arrays/identity.zok",
 	"curves": ["Bn128", "Bls12_381", "Bls12_377", "Bw6_761"],
 	"tests": [
 		{
--- a/zokrates_core_test/tests/tests/arrays/identity.code
+++ b/zokrates_core_test/tests/tests/arrays/identity.code
--- a/zokrates_core_test/tests/tests/arrays/select.json
+++ b/zokrates_core_test/tests/tests/arrays/select.json
@ -0,0 +1,50 @@
+{
+	"entry_point": "./tests/tests/arrays/select.zok",
+    "max_constraint_count": 44,
+	"curves": ["Bn128", "Bls12_381", "Bls12_377", "Bw6_761"],
+	"tests": [
+		{
+			"input": {
+				"values": ["0", "11", "22", "0"]
+			},
+			"output": {
+				"Ok": {
+					"values": ["0"]
+				}
+			}
+		},
+		{
+			"input": {
+				"values": ["0", "11", "22", "1"]
+			},
+			"output": {
+				"Ok": {
+					"values": ["11"]
+				}
+			}
+		},
+        {
+			"input": {
+				"values": ["0", "11", "22", "2"]
+			},
+			"output": {
+				"Ok": {
+					"values": ["22"]
+				}
+			}
+		},
+		{
+			"input": {
+				"values": ["0", "11", "22", "3"]
+			},
+			"output": {
+				"Err": {
+					"UnsatisfiedConstraint": {
+						"left": "1",
+						"right": "0"
+					}
+				}
+			}
+		}
+	]
+}
--- a/zokrates_core_test/tests/tests/arrays/select.zok
+++ b/zokrates_core_test/tests/tests/arrays/select.zok
@ -0,0 +1,2 @@
+def main(field[3] array, u32 index) -> field:
+    return array[index]
--- a/zokrates_core_test/tests/tests/cached_condition.json
+++ b/zokrates_core_test/tests/tests/cached_condition.json
@ -1,4 +1,5 @@
 {
-	"entry_point": "./tests/tests/cached_condition.zok",
-    "max_constraint_count": 2015
+  "entry_point": "./tests/tests/cached_condition.zok",
+  "max_constraint_count": 2015,
+  "tests": []
 }
--- a/zokrates_core_test/tests/tests/constants/import/destination.json
+++ b/zokrates_core_test/tests/tests/constants/import/destination.json
@ -0,0 +1,4 @@
+{
+    "entry_point": "./tests/tests/constants/import/destination.zok",
+    "tests": []
+}
--- a/zokrates_core_test/tests/tests/constants/import/destination.zok
+++ b/zokrates_core_test/tests/tests/constants/import/destination.zok
@ -0,0 +1,4 @@
+from "./origin.zok" import foo
+def main():
+    assert(foo([1, 1]))
+    return
--- a/zokrates_core_test/tests/tests/constants/import/origin.zok
+++ b/zokrates_core_test/tests/tests/constants/import/origin.zok
@ -0,0 +1,3 @@
+const u32 N = 1 + 1
+def foo(field[N] a) -> bool:
+   return true
--- a/zokrates_embed/Cargo.toml
+++ b/zokrates_embed/Cargo.toml
@ -1,6 +1,6 @@
 [package]
 name = "zokrates_embed"
-version = "0.1.2"
+version = "0.1.3"
 authors = ["schaeff <thibaut@schaeff.fr>"]
 edition = "2018"

--- a/zokrates_js/Cargo.toml
+++ b/zokrates_js/Cargo.toml
@ -1,6 +1,6 @@
 [package]
 name = "zokrates_js"
-version = "1.0.32"
+version = "1.0.33"
 authors = ["Darko Macesic"]
 edition = "2018"

--- a/zokrates_js/package.json
+++ b/zokrates_js/package.json
@ -2,7 +2,7 @@
  "name": "zokrates-js",
  "main": "index.js",
  "author": "Darko Macesic <darem966@gmail.com>",
-  "version": "1.0.32",
+  "version": "1.0.33",
  "keywords": [
    "zokrates",
    "wasm-bindgen",
--- a/zokrates_parser/src/ace_mode/index.js
+++ b/zokrates_parser/src/ace_mode/index.js
@ -47,7 +47,7 @@ ace.define("ace/mode/zokrates_highlight_rules",["require","exports","module","ac
        var decimalInteger = "(?:(?:[1-9]\\d*)|(?:0))";
        var decimalSuffix = "(?:_?(?:f|u(?:8|16|32|64)))?";
        var hexInteger = "(?:0[xX][\\dA-Fa-f]+)";
-        var integer = "(?:" + decimalInteger + decimalSuffix "|" + hexInteger + ")\\b";
+        var integer = "(?:" + decimalInteger + decimalSuffix + "|" + hexInteger + ")\\b";

        this.$rules = {
            "start": [
@ -118,4 +118,4 @@ ace.define("ace/mode/zokrates",["require","exports","module","ace/lib/oop","ace/
    }).call(Mode.prototype);

    exports.Mode = Mode;
-});
+});
--- a/zokrates_parser/src/ace_mode/package.json
+++ b/zokrates_parser/src/ace_mode/package.json
@ -1,6 +1,6 @@
 {
  "name": "ace-mode-zokrates",
-  "version": "1.0.3",
+  "version": "1.0.4",
  "description": "Ace Mode for ZoKrates DSL",
  "main": "index.js",
  "scripts": {
--- a/zokrates_stdlib/Cargo.toml
+++ b/zokrates_stdlib/Cargo.toml
@ -1,6 +1,6 @@
 [package]
 name = "zokrates_stdlib"
-version = "0.2.2"
+version = "0.2.3"
 authors = ["Stefan Deml <stefandeml@gmail.com>", "schaeff <thibaut@schaeff.fr>"]
 edition = "2018"

--- a/zokrates_stdlib/stdlib/field.zok
+++ b/zokrates_stdlib/stdlib/field.zok
@ -0,0 +1,8 @@
+from "EMBED" import FIELD_SIZE_IN_BITS
+
+const field FIELD_MIN = 0
+const field FIELD_MAX = -1
+
+// A dummy `main` function, should NOT be used.
+def main():
+    return
--- a/zokrates_stdlib/stdlib/hashes/blake2/blake2s_p.zok
+++ b/zokrates_stdlib/stdlib/hashes/blake2/blake2s_p.zok
@ -3,9 +3,17 @@
 import "utils/casts/u32_to_bits"
 import "utils/casts/u32_from_bits"

+// right rotation
 def rotr32<N>(u32 x) -> u32:
    return (x >> N) | (x << (32 - N))

+// change endianness
+def swap_u32(u32 val) -> u32:
+    return (val << 24) | \
+          ((val <<  8) & 0x00ff0000) | \
+          ((val >>  8) & 0x0000ff00) | \
+          ((val >> 24) & 0x000000ff)
+
 def blake2s_iv() -> (u32[8]):
    return [
        0x6A09E667, 0xBB67AE85, 0x3C6EF372, 0xA54FF53A,
@ -73,8 +81,8 @@ def blake2s_init(u32[2] p) -> (u32[8]):
        iv[3],
        iv[4],
        iv[5],
-        iv[6] ^ p[0],
-        iv[7] ^ p[1]
+        iv[6] ^ swap_u32(p[0]),
+        iv[7] ^ swap_u32(p[1])
    ]
    return h

@ -84,6 +92,13 @@ def main<K>(u32[K][16] input, u32[2] p) -> (u32[8]):
    u32 t0 = 0
    u32 t1 = 0

+    // change endianness of inputs from big endian to little endian
+    for u32 i in 0..K do
+        for u32 j in 0..16 do
+            input[i][j] = swap_u32(input[i][j])
+        endfor
+    endfor
+
    for u32 i in 0..K-1 do
        t0 = (i + 1) * 64
        t1 = if t0 == 0 then t1 + 1 else t1 fi
@ -94,4 +109,10 @@ def main<K>(u32[K][16] input, u32[2] p) -> (u32[8]):
    t1 = if t0 == 0 then t1 + 1 else t1 fi

    h = blake2s_compression(h, input[K - 1], [t0, t1], true)
+
+    // change endianness of output from little endian to big endian
+    for u32 i in 0..8 do
+        h[i] = swap_u32(h[i])
+    endfor
+
    return h
--- a/zokrates_stdlib/stdlib/hashes/keccak/keccak.zok
+++ b/zokrates_stdlib/stdlib/hashes/keccak/keccak.zok
@ -28,6 +28,12 @@ def rc() -> u64[24]:
 def rotl64(u64 x, u32 n) -> u64:
    return ((x << n) | (x >> (64 - n)))

+// change endianness
+def swap_u64(u64 val) -> u64:
+    val = ((val << 8) & 0xFF00FF00FF00FF00) | ((val >> 8) & 0x00FF00FF00FF00FF)
+    val = ((val << 16) & 0xFFFF0000FFFF0000) | ((val >> 16) & 0x0000FFFF0000FFFF)
+    return (val << 32) | (val >> 32)
+
 // compression function
 def keccakf(u64[25] st) -> u64[25]:
    u32[24] rotc = rho()
@ -80,6 +86,11 @@ def main<N, W>(u64[N] input, u64 pad) -> u64[25]:
    u32 rate = (200 - (W / 4)) / 8
    u32 pt = 0

+    // change endianness of inputs from big endian to little endian
+    for u32 i in 0..N do
+        input[i] = swap_u64(input[i])
+    endfor
+
    // update
    for u32 i in 0..N do
        q[pt] = q[pt] ^ input[i]
@ -90,6 +101,11 @@ def main<N, W>(u64[N] input, u64 pad) -> u64[25]:
    // finalize
    q[pt] = q[pt] ^ pad
    q[rate - 1] = q[rate - 1] ^ 0x8000000000000000
-
    q = keccakf(q)
+
+    // change endianness of output from little endian to big endian
+    for u32 i in 0..W/64 do
+        q[i] = swap_u64(q[i])
+    endfor
+
    return q
--- a/zokrates_stdlib/tests/tests/field.json
+++ b/zokrates_stdlib/tests/tests/field.json
@ -0,0 +1,17 @@
+{
+    "entry_point": "./tests/tests/field.zok",
+    "max_constraint_count": 3,
+    "curves": ["Bn128"],
+    "tests": [
+        {
+            "input": {
+                "values": []
+            },
+            "output": {
+                "Ok": {
+                    "values": ["0", "21888242871839275222246405745257275088548364400416034343698204186575808495616", "254"]
+                }
+            }
+        }
+    ]
+}
--- a/zokrates_stdlib/tests/tests/field.zok
+++ b/zokrates_stdlib/tests/tests/field.zok
@ -0,0 +1,4 @@
+from "field" import FIELD_MIN, FIELD_MAX, FIELD_SIZE_IN_BITS
+
+def main() -> (field, field, u32):
+    return FIELD_MIN, FIELD_MAX, FIELD_SIZE_IN_BITS
--- a/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_1024bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_1024bit.zok
@ -1,6 +1,17 @@
 import "hashes/blake2/blake2s"

+// Python code:
+// >>> from hashlib import blake2s
+
+// >>> digest = blake2s()
+// >>> digest.update(b'\x12\x34\x56\x78' * 32)
+// >>> digest.hexdigest()
+// '4858b8174f8f5851ddac0507003b2490f42c33df8362770c5e79b770c84ffdb4'
+
 def main():
-    u32[8] h = blake2s::<2>([[0; 16]; 2])
-    assert(h == [0x2005424E, 0x7BCE81B9, 0x2CCEF4DB, 0x94DBBA4D, 0x7D9B0750, 0xB53797EB, 0xD3572923, 0xCB01F823])
+    u32[8] h = blake2s::<2>([[0x12345678; 16]; 2]) // 2 * 16 * 32 = 1024 bit input
+    assert(h == [
+        0x4858B817, 0x4F8F5851, 0xDDAC0507, 0x003B2490,
+        0xF42C33DF, 0x8362770C, 0x5E79B770, 0xC84FFDB4
+    ])
    return
--- a/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_1536bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_1536bit.zok
@ -1,6 +1,17 @@
 import "hashes/blake2/blake2s"

+// Python code:
+// >>> from hashlib import blake2s
+
+// >>> digest = blake2s()
+// >>> digest.update(b'\x12\x34\x56\x78' * 48)
+// >>> digest.hexdigest()
+// '879043503b04cab2f3c0d7a4bb01c1db74c238c49887da84e8a619893092b6e2'
+
 def main():
-    u32[8] h = blake2s::<3>([[0x42424242; 16]; 3])
-    assert(h == [0x804BD0E6, 0x90AD426E, 0x6BCF0BAD, 0xCB2D22C1, 0xF717B3C3, 0x4D9CB47F, 0xEB541A97, 0x061D9ED0])
+    u32[8] h = blake2s::<3>([[0x12345678; 16]; 3]) // 3 * 16 * 32 = 1536 bit input
+    assert(h == [
+        0x87904350, 0x3B04CAB2, 0xF3C0D7A4, 0xBB01C1DB,
+        0x74C238C4, 0x9887DA84, 0xE8A61989, 0x3092B6E2
+    ])
    return
--- a/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_512bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_512bit.zok
@ -1,6 +1,17 @@
 import "hashes/blake2/blake2s"

+// Python code:
+// >>> from hashlib import blake2s
+
+// >>> digest = blake2s()
+// >>> digest.update(b'\x12\x34\x56\x78' * 16)
+// >>> digest.hexdigest()
+// '52af1aec3e6663bcc759d55fc7557fbb2f710219f0de138b1b52c919f5c94415'
+
 def main():
-    u32[8] h = blake2s::<1>([[0; 16]])
-    assert(h == [0x7CDB09AE, 0xB4424FD5, 0xB609EF90, 0xF61A54BC, 0x9B95E488, 0x353FC5B8, 0xE3566F9A, 0xA354B48A])
+    u32[8] h = blake2s::<1>([[0x12345678; 16]; 1]) // 16 * 32 = 512 bit input
+    assert(h == [
+        0x52AF1AEC, 0x3E6663BC, 0xC759D55F, 0xC7557FBB,
+        0x2F710219, 0xF0DE138B, 0x1B52C919, 0xF5C94415
+    ])
    return
--- a/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_8192bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_8192bit.zok
@ -1,6 +1,17 @@
 import "hashes/blake2/blake2s"

+// Python code:
+// >>> from hashlib import blake2s
+
+// >>> digest = blake2s()
+// >>> digest.update(b'\x12\x34\x56\x78' * 256)
+// >>> digest.hexdigest()
+// 'b41c4704f49df139039bbc91c6e23a84198ffedc78d0b677e8b2a6a57f3460e8'
+
 def main():
-    u32[8] h = blake2s::<16>([[0; 16]; 16])
-    assert(h == [0x63665303, 0x046C502A, 0xC8514A5D, 0x67B7E833, 0xA9DAD591, 0xB421A8BC, 0x662A73A2, 0x2DA25AFB])
+    u32[8] h = blake2s::<16>([[0x12345678; 16]; 16]) // 16 * 16 * 32 = 8192 bit input
+    assert(h == [
+        0xB41C4704, 0xF49DF139, 0x039BBC91, 0xC6E23A84,
+        0x198FFEDC, 0x78D0B677, 0xE8B2A6A5, 0x7F3460E8
+    ])
    return
--- a/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_p.zok
+++ b/zokrates_stdlib/tests/tests/hashes/blake2/blake2s_p.zok
@ -1,6 +1,17 @@
 import "hashes/blake2/blake2s_p" as blake2s

+// Python code:
+// >>> from hashlib import blake2s
+
+// >>> digest = blake2s(person=b'\x12\x34\x56\x78\x00\x00\x00\x00')
+// >>> digest.update(b'\x12\x34\x56\x78' * 16)
+// >>> digest.hexdigest()
+// '780105bc9ca7633b1f289b3d1558dece65e04ac23f88e711dc29600fa3e0258a'
+
 def main():
-    u32[8] h = blake2s::<1>([[0; 16]], [0x12345678, 0])
-    assert(h == [0xC63C8C31, 0x5FCA3E69, 0x13850D46, 0x1DE48657, 0x208D2534, 0x9AA6E0EF, 0xAFEE7610, 0xFBDFAC13])
+    u32[8] h = blake2s::<1>([[0x12345678; 16]; 1], [0x12345678, 0])
+    assert(h == [
+        0x780105BC, 0x9CA7633B, 0x1F289B3D, 0x1558DECE,
+        0x65E04AC2, 0x3F88E711, 0xDC29600F, 0xA3E0258A
+    ])
    return
--- a/zokrates_stdlib/tests/tests/hashes/keccak/256bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/keccak/256bit.zok
@ -1,6 +1,14 @@
 import "hashes/keccak/256bit" as keccak256

+// Python code:
+// >>> from Crypto.Hash import keccak
+
+// >>> digest = keccak.new(digest_bits=256)
+// >>> digest.update(b'\x00\x00\x00\x00\x00\x00\x00\x2A' * 20)
+// >>> digest.hexdigest()
+// '33d0141407fee6e5d9caf6ae44e840bc67a37da55e3c845fbc2b4a6dce1f02f0'
+
 def main():
    u64[4] h = keccak256::<20>([42; 20])
-    assert(h == [0x09330DD35B609CA9, 0xDACFC1598C95602C, 0xACD911013FB018F3, 0x17233D68F05E0826])
+    assert(h == [0x33D0141407FEE6E5, 0xD9CAF6AE44E840BC, 0x67A37DA55E3C845F, 0xBC2B4A6DCE1F02F0])
    return
--- a/zokrates_stdlib/tests/tests/hashes/keccak/384bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/keccak/384bit.zok
@ -1,6 +1,17 @@
 import "hashes/keccak/384bit" as keccak384

+// Python code:
+// >>> from Crypto.Hash import keccak
+
+// >>> digest = keccak.new(digest_bits=384)
+// >>> digest.update(b'\x00\x00\x00\x00\x00\x00\x00\x2A' * 20)
+// >>> digest.hexdigest()
+// 'a944b9b859c1e69d66b52d4cf1f678b24ed8a9ccb0a32bbe882af8a3a1acbd3b68eed9c628307e5d3789f1a64a50e8e7'
+
 def main():
    u64[6] h = keccak384::<20>([42; 20])
-    assert(h == [0x2E9DCE590F0A1908, 0x0C4234AB952C5598, 0xFB2DF066B44780C2, 0x717039E101D4A8DA, 0xBAD1EFE140C4B2C4, 0xFAE08DAC3438416E])
+    assert(h == [
+        0xA944B9B859C1E69D, 0x66B52D4CF1F678B2, 0x4ED8A9CCB0A32BBE,
+        0x882AF8A3A1ACBD3B, 0x68EED9C628307E5D, 0x3789F1A64A50E8E7
+    ])
    return
--- a/zokrates_stdlib/tests/tests/hashes/keccak/512bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/keccak/512bit.zok
@ -1,9 +1,17 @@
 import "hashes/keccak/512bit" as keccak512

+// Python code:
+// >>> from Crypto.Hash import keccak
+
+// >>> digest = keccak.new(digest_bits=512)
+// >>> digest.update(b'\x00\x00\x00\x00\x00\x00\x00\x2A' * 20)
+// >>> digest.hexdigest()
+// '5451affca80019c7ac9a7ff647ca073b56e19d55857031df14e00bb1d36ed18a05bdac99bcc0417240dea0cf3fddd19144b8d1e9618fd3f6c8f1a79f7e489eb8'
+
 def main():
    u64[8] h = keccak512::<20>([42; 20])
    assert(h == [
-        0x2716192386255918, 0x68DFF390376BBF13, 0xBD695ADA4CD230E3, 0xF3B00388676A04D3,
-        0x484F3F1BB9F36A09, 0x9D0119067282F940, 0xDF27DE0F48072A66, 0xF5957972134160EB
+        0x5451AFFCA80019C7, 0xAC9A7FF647CA073B, 0x56E19D55857031DF, 0x14E00BB1D36ED18A,
+        0x05BDAC99BCC04172, 0x40DEA0CF3FDDD191, 0x44B8D1E9618FD3F6, 0xC8F1A79F7E489EB8
    ])
    return
--- a/zokrates_stdlib/tests/tests/hashes/sha3/256bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/sha3/256bit.zok
@ -1,6 +1,14 @@
 import "hashes/sha3/256bit" as sha3_256

+// Python code:
+// >>> from Crypto.Hash import SHA3_256
+
+// >>> digest = SHA3_256.new()
+// >>> digest.update(b'\x00\x00\x00\x00\x00\x00\x00\x2A' * 20)
+// >>> digest.hexdigest()
+// '18d00c9e97cd5516243b67b243ede9e2cf0d45d3a844d33340bfc4efc9165100'
+
 def main():
    u64[4] h = sha3_256::<20>([42; 20])
-    assert(h == [0x84350A3A90DED183, 0x70518606C7DC401A, 0x2D44F39C0FCEAC92, 0x3E9533A716130C5A])
+    assert(h == [0x18D00C9E97CD5516, 0x243B67B243EDE9E2, 0xCF0D45D3A844D333, 0x40BFC4EFC9165100])
    return
--- a/zokrates_stdlib/tests/tests/hashes/sha3/384bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/sha3/384bit.zok
@ -1,6 +1,17 @@
 import "hashes/sha3/384bit" as sha3_384

+// Python code:
+// >>> from Crypto.Hash import SHA3_384
+
+// >>> digest = SHA3_384.new()
+// >>> digest.update(b'\x00\x00\x00\x00\x00\x00\x00\x2A' * 20)
+// >>> digest.hexdigest()
+// 'fbb5abd69915e316836d438f0e833a3ebd0f2d8a11e17e248c96c77210b183aab0874eaaef37609d2c4a9a37a6e9740f'
+
 def main():
    u64[6] h = sha3_384::<20>([42; 20])
-    assert(h == [0x75A036FA8B615B37, 0x6C73086BB56F092C, 0x536E658916EC18AE, 0xB2F2EEE620CDF698, 0xB7E904DE62A70A31, 0x84FDAA0665836ADD])
+    assert(h == [
+        0xFBB5ABD69915E316, 0x836D438F0E833A3E, 0xBD0F2D8A11E17E24,
+        0x8C96C77210B183AA, 0xB0874EAAEF37609D, 0x2C4A9A37A6E9740F
+    ])
    return
--- a/zokrates_stdlib/tests/tests/hashes/sha3/512bit.zok
+++ b/zokrates_stdlib/tests/tests/hashes/sha3/512bit.zok
@ -1,9 +1,17 @@
 import "hashes/sha3/512bit" as sha3_512

+// Python code:
+// >>> from Crypto.Hash import SHA3_512
+
+// >>> digest = SHA3_512.new()
+// >>> digest.update(b'\x00\x00\x00\x00\x00\x00\x00\x2A' * 20)
+// >>> digest.hexdigest()
+// '73a0967b68de5ce1093cbd7482fd4de9ccc9c782e2edc71b583d26fe16fb19e3322a2a024b7f6e163fbb1a15161686dd3a39233f9cf8616e7c74e91fa1aa3b2b'
+
 def main():
    u64[8] h = sha3_512::<20>([42; 20])
    assert(h == [
-        0x22DFD92B47C60DAC, 0xDA47C8C247A84FA2, 0x7C5809F122D6950A, 0x8034D41097680656,
-        0xD6D06F820B046994, 0xF62743594A554B88, 0x4966E0821CB4D667, 0x974D4391624C5619
+        0x73A0967B68DE5CE1, 0x093CBD7482FD4DE9, 0xCCC9C782E2EDC71B, 0x583D26FE16FB19E3,
+        0x322A2A024B7F6E16, 0x3FBB1A15161686DD, 0x3A39233F9CF8616E, 0x7C74E91FA1AA3B2B
    ])
    return
				`@ -1 +0,0 @@`
				`Run compilation test on RNG tutorial and fix bugs`
				`@ -1 +0,0 @@`
				`Fix parsing of the left hand side of definitions`
				`@ -1 +0,0 @@`
				`Introduce a limit of 2**20 for for-loop sizes`
				`@ -1 +0,0 @@`
				`Fix variable write remover when isolating branches`
				`@ -1 +0,0 @@`
				`Improve propagation on if-else expressions when consequence and alternative are equal`
				`@ -1 +0,0 @@`
				`Fix access to constant in local function call`
				`@ -1 +0,0 @@`
				`Fixed deserialization logic in the zokrates.js that caused issues on cli-compiled binaries`
				`@ -1 +0,0 @@`
				Documentation improvements, move examples to a separate section, remove deprecated `--light` flag used in a rng tutorial, add a simple file system resolver example to zokrates.js docs
				`@ -0,0 +1 @@`
				Add a CLI option `generate-smtlib2` to output the compiled IR as an SMT formula.