Introduction
Welcome to OpenZL, the "missing ZKP library."
OpenZL is an opensource library for development of secure, highperformance, zeroknowledge applications. OpenZL aims to bridge the gap between highlevel languages that miss valuable opportunities for optimization and lowlevel libraries that require extensive cryptographic expertise. We believe that bridging this gap can improve both the speed and security of ZK app development.
OpenZL takes a threetiered approach to the problem:
Gadget Layer
The highlevel layer provides cryptographic "gadgets" such as accumulators, hash functions, commitment schemes, etc. These readytogo gadgets are intended for dropin use in ZK applications. They are composable, allowing complex logic to be built from cryptographic primitives. The gadget library serves developers who want to access ZK without getting in the weeds.
Plugin Layer
Importantly, OpenZL gadgets make no assumptions about the ZK proving system they target. Instead, developers choose an appropriate proof system plugin to use whatever proving system works best for their application. These plugins form the lowlevel layer of OpenZL; this is where nittygritty, proofsystemspecific optimization occurs.
Middle Layer: ECLAIR
Between the gadget layer and the proof system layer sits ECLAIR: the Embedded Circuit Language And Intermediate Representation. ECLAIR is a proofsystemagnostic language for circuit descriptions. Gadgets written in ECLAIR can target any of the ZK proving systems provided by lowlevel plugins. OpenZL thus achieves modularity at both the high and low level.
We will have much more to say on ECLAIR in the following chapters. For now, let us just emphasize our goals. We believe that ZK app development should be:

Fast: both in the sense that developers should be able to quickly start using and composing gadgets and in the sense that those gadgets should be optimized for speed.

Flexible: as new ZK proving systems appear, developers should be able to quickly adopt the latest technology. We should also deduplicate the effort required for projects to switch over.

Secure: you shouldn't have to be an expert cryptographer to build secure applications. We should instead pool our expertise and package it in the form of safe cryptographic libraries.

Opensource: "NO" to walled gardens! "YES" to collaboration! OpenZL is and will remain opensource.
Please read on to learn more. For now these docs focus on ECLAIR, but we will soon update them with more explanation of the gadget and plugin layers.
Native vs NonNative Computation
ECLAIR aims to unify and simplify the development of ZK applications by providing a circuit language that can target a myriad of zero knowledge proof systems. In doing so ECLAIR treats each ZK proof system as its own computational environment. Much as Rust source code can be compiled to executables for Linux, MacOS, or Windows, a circuit written in ECLAIR can target implementations of Groth16, Plonklike proving systems, or any other proving backend for which an appropriate plugin exists.
In this framework it is useful to distinguish between "native" and "nonnative" computational environments. "Native computation" is the everyday sort of computation that simply concerns itself with executing instructions on computer hardware; it produces no ZKP to attest to the computation's correctness. This is what computers do natively.
In ECLAIR, native computation is treated on an equal footing with other computational environments that do produce ZKPs of a computation's correctness. These are collectively referred to as "nonnative computation." A proving system such as Groth16 is a nonnative computational environment which provides a proof of correctness for any computation that can be represented as an arithmetic circuit. Likewise there are a variety of "Plonklike" proving systems that achieve the same goal of performing a computation and providing a succinct argument of its correctness.
Given the variety of nonnative computational environments and the current rate of innovation in ZK proving systems, it is desirable to describe circuits in a proving system agnostic representation like ECLAIR. The main advantages of doing so are:
 Agility: A circuit described in ECLAIR can target any proving system via plugins. Thus a developer can quickly switch the proving system used in their ZK app according to their needs. When the next hot new ZK proving system is discovered, a new plugin allows existing ECLAIR circuits to target that proving system.
 Correctness: Computation described in ECLAIR is performed the same way in all computational environments, native or nonnative. This gives developers confidence that computations performed within a ZK proving system match their native version.
The COM
Abstraction
As explained above, a computation described in ECLAIR can be carried out in various native or nonnative computational environments. The computational environment is specified by choosing a type COM
, short for "compiler."
We think of COM
as a compiler that takes instructions written in ECLAIR and translates them to instructions for the target computational environment. In the case of native computation, COM
would compile ECLAIR circuits to machine code for manipulating computer hardware. In the case of nonnative computation, COM
would compile ECLAIR circuits to a constraint representation such as R1CS for ZK proof generation.
For example, consider a trait Add
that consists of a single function fn add
for adding like types. Ordinarily, the signature of this function would be
#![allow(unused)] fn main() { fn add(lhs: Self, rhs: Self) > Self }
But in ECLAIR, we include a generic type COM
to define a trait Add<COM>
for addition in an arbitrary computational environment. The signature of fn add
becomes
#![allow(unused)] fn main() { fn add(lhs: Self, rhs: Self, compiler: &mut COM) > Self }
In an ECLAIR circuit we may see a line like
#![allow(unused)] fn main() { output = add(lhs, rhs, &mut compiler); }
In the case of nonnative computation, this results in a constraint being added to enforce output = lhs + rhs
in whatever constraint system is appropriate to that computational environment. A circuit described using the Add<COM>
trait can be compiled to any proving system that has a type implementing Add<COM>
.
The Native Compiler Default COM = ()
In native computation there is no correctness proof and therefore no constraints for the compiler to generate. In this case ECLAIR hands off compilation to the Rust compiler to produce machine code. The native equivalent of an unsatisfied circuit is a computation that produces a runtime error. ECLAIR uses the unit type COM = ()
to represent the native compiler.
ECLAIR traits generally use the native compiler by default, such as Add<COM = ()>
. This means that unless a ZK proving system is chosen by specifying some other type for COM
, the computation will be carried out natively. When implementing ECLAIR traits for the native compiler, we still need to include the compiler
argument in function signatures. For nativeonly computation this looks like
#![allow(unused)] fn main() { output = add(lhs, rhs, &mut ()); }
ECLAIR Standard Library
We explained in the previous section that ECLAIR achieves compatibility with various proof systems through its COM
abstraction, which regards each ZK proving system as its own computational environment. ECLAIR makes minimal assumptions on the inner workings of each computational environment in an attempt to stay general enough to target a wide variety of ZK proving systems.
ECLAIR does, however, include a standard library of traits and types that will be relevant to nearly all COM
types. We model this ECLAIR Standard Library on the Rust Standard Library. Whenever possible, ECLAIR uses the same API as Rust, with minimal changes to accommodate the COM
abstraction.
Like the Rust standard library, ECLAIR's standard library is not strictly required; ECLAIR can handle compiler types that for whatever reason do not include implementations of the standard library traits. However, common compiler types will have implementations of most standard library traits, if not all of them.
We recommend reading through this chapter as a way to familiarize oneself with common patterns in ECLAIR. Most readers will be familiar with the Rust standard library and can ease their way into the COM
abstraction by comparing ECLAIR's standard library traits to their counterparts in the Rust standard library. (The Bool and Num sections are not so Rustlike, but the Cmp and Ops sections are.)
Bool
Any reasonable computational environment has a notion of boolean type, but not all environments represent this concept in the same way. Native computation operates directly on bits and therefore has a natural notion of boolean type: a single bit. However a nonnative environment such as a ZK proving system may lack a natural boolean type. In order for ECLAIR to express bitwise operations or truthvalued comparisons in these environments, we need to specify how each COM
type executes boolean operations.
Has<bool>
First we must specify a given compiler's boolean type. We do so through the eclair::Has
trait:
#![allow(unused)] fn main() { /// Compiler Type Introspection pub trait Has<T> { /// Compiler Type /// /// This type represents the allocation of `T` into `Self` as a compiler. /// Whenever we need to define abstractions that require the compiler to /// have access to some type internally, we can use this `trait` as a /// requirement of that abstraction. type Type; } }
The Has<T>
trait is implemented for a compiler type COM
to specify how the type T
is represented within COM
's computational environment. The native compiler COM = ()
always represents T
as T
, so it implements Has<T>
for any type T
.
To see the usefulness of Has<T>
, suppose COM
corresponds to a ZK proving system such as Groth16 that represents computation as a R1CS over some finite field F
. We can call this compiler type R1CS<F>
.
In this setting there are no "bits," only finite field elements. Thus we need to choose how to represent bits. A reasonable choice would be to use the field F
itself, perhaps with the convention that the zero element represents the boolean 0
and any nonzero element represents the boolean 1
. We would specify this choice by an implementation:
#![allow(unused)] fn main() { impl Has<bool> for R1CS<F> { type Type = FVar; } }
Here FVar
is a type that represents variables in the R1CS that can have values in F
. With this implementation we specify that the R1CS<F>
compiler represents booleans as variables with values in F
.
Has<bool>
is a necessary trait for a compiler type to make sense of many natural operations such as comparison, conditional switching, assertion, etc. For example, an ==
comparison between two variables in COM
produces a boolean truth value; this truth value must itself be represented somehow within COM
, hence the requirement COM: Has<bool>
in order for equality comparisons to be possible in COM
. See Cmp for more on comparisons in ECLAIR.
Assert
An example of an ECLAIR
trait that requires Has<bool>
is Assert
:
#![allow(unused)] fn main() { /// Assertion pub trait Assert: Has<bool> { /// Asserts that `bit` reduces to `true`. fn assert(&mut self, bit: &Bool<Self>); /// Asserts that all the items in the `iter` reduce to `true`. #[inline] fn assert_all<'b, I>(&mut self, iter: I) where Self: Assert, Bool<Self>: 'b, I: IntoIterator<Item = &'b Bool<Self>>, { iter.into_iter().for_each(move b self.assert(b)); } } }
If compiler
is of a type COM
that implements Assert
then compiler.assert(bit)
should generate a constraint that is satisfied if and only if bit
represents true
according to COM
's implementation of Has<bool>
. In the native compiler COM = ()
the computation produces a runtime error if bit = false
.
The requirement COM: Assert
is a prerequisite for the trait PartialEq<Rhs, COM>
. More on that in Cmp.
Conditional Selection and Swap
Another common operation involving booleans is selection, expressed in ECLAIR through the ConditionalSelect<COM>
trait:
#![allow(unused)] fn main() { /// Conditional Selection pub trait ConditionalSelect<COM = ()> where COM: Has<bool>, { /// Selects `true_value` when `bit == true` and `false_value` when `bit == false`. fn select( bit: &Bool<COM>, true_value: &Self, false_value: &Self, compiler: &mut COM ) > Self; } }
If an ECLAIR circuit contains the line
#![allow(unused)] fn main() { output = select(bit, true_value, false_value, &mut compiler); }
then this generates a constraint in compiler
that enforces output == true_value
if bit
represents true
and output == false_value
otherwise. Of course this only makes sense if compiler
knows how to interpret bit
as a boolean value, hence the requirement COM: Has<bool>
.
A similar operation is conditionally swapping values based on a boolean. For this we have the ConditionalSwap<COM>
trait:
#![allow(unused)] fn main() { /// Conditional Swap pub trait ConditionalSwap<COM = ()> where COM: Has<bool>, { /// Swaps `lhs` and `rhs` whenever `bit == true` and keeps /// them in the same order when `bit == false`. fn swap( bit: &Bool<COM>, lhs: &Self, rhs: &Self, compiler: &mut COM ) > (Self, Self); } }
This trait is selfexplanatory.
Cmp
Comparison is expressed in Rust through the traits PartialEq
and Eq
. ECLAIR has analogues of these that explicitly mention the compiler COM
to specify the computational environment where comparison occurs. As in Rust, Eq
is simply a subtrait of PartialEq
used to indicate that a partial equivalence relation is actually a true equivalence relation.
The ECLAIR equivalent of PartialEq
is
#![allow(unused)] fn main() { /// Partial Equivalence Relations pub trait PartialEq<Rhs, COM = ()> where COM: Has<bool>, { /// Returns `true` if `self` and `rhs` are equal. fn eq(&self, rhs: &Rhs, compiler: &mut COM) > Bool<COM>; /// Returns `true` if `self` and `rhs` are not equal. fn ne(&self, other: &Rhs, compiler: &mut COM) > Bool<COM> where Bool<COM>: Not<COM, Output = Bool<COM>>, { self.eq(other, compiler).not(compiler) } /// Asserts that `self` and `rhs` are equal. /// /// # Implementation Note /// /// This method is an optimization path for the case when /// comparing for equality and then asserting is more expensive /// than a custom assertion. fn assert_equal(&self, rhs: &Rhs, compiler: &mut COM) where COM: Assert, { let are_equal = self.eq(rhs, compiler); compiler.assert(&are_equal); } } }
As with most traits in the ECLAIR Standard Library, PartialEq
differs from its pure Rust equivalent mainly by the addition of the COM
type and an argument compiler: &mut COM
in the function signatures. This allows ECLAIR to generate appropriate constraints whenever COM
specifies a ZK proving system.
For example, when an ECLAIR circuit contains the line
#![allow(unused)] fn main() { output = lhs.eq(rhs, &mut compiler); }
this means that compiler
will allocate a variable output
of COM
's boolean type and constraint output
to carry the truth value of lhs == rhs
.
Besides the compiler
argument, the main difference from Rust's PartialEq
trait is the added method fn assert_equal
. The reason for including this method is that in some ZK proving systems it may be possible to assert equality using fewer constraints than separate calls to PartialEq::eq
and Assert::assert
. In such situations, the implementation of PartialEq<COM>
should replace the blanket implementation here with the more optimized version. This is an example of the sort lowlevel, COM
specific optimizations that ECLAIR allows.
Num
This module provides some useful traits and types for numerical operations. Currently it provides the traits Zero
, One
, and AssertWithinBitRange
as well as an UnsignedInteger
type for ECLAIR.
Zero
, One
These traits can be implemented for a type T
relative to a compiler COM
in order to indicate that COM
understands a notion of zero/one value for T
. Moreover, the trait specifies how COM
determines whether a given instance of T
is equal to that zero/one value:
#![allow(unused)] fn main() { /// Additive Identity pub trait Zero<COM = ()> { /// Verification Type type Verification; /// Returns the additive identity for `Self`. fn zero(compiler: &mut COM) > Self; /// Returns a truthy value if `self` is equal to the additive identity. fn is_zero(&self, compiler: &mut COM) > Self::Verification; } }
Note the Verification
type, which allows fn is_zero
to output "truthy values" in whatever sense is appropriate for COM
. For the native compiler COM = ()
we would choose Verification = bool
. For a compiler such that COM: Has<bool>
, we would likely choose Verification = Bool<COM>
to be this compiler's boolean type. (Note, however, that we do not require that COM: Has<bool>
for this trait.)
The trait One
is similar to Zero
:
#![allow(unused)] fn main() { /// Multiplicative Identity pub trait One<COM = ()> { /// Verification Type type Verification; /// Returns the multiplicative identity for `Self`. fn one(compiler: &mut COM) > Self; /// Returns a truthy value if `self` is equal to the multiplicative identity. fn is_one(&self, compiler: &mut COM) > Self::Verification; } }
Bit Range Assertion
Range checks arise frequently in ZK circuits. One reason is that the primitive data type in a ZK proving system is often a finite field element. When we use one of these finite field elements to represent a quantity such as a 20byte ETH address we need to ensure that the field element really is within the correct range.
In the native computation setting this is a straightforward comparison between the finite field element (represented as a positive integer) and the maximum size of a 20byte integer. However a nonnative compiler needs to generate constraints that are satisfied only if the finite field element lies in the correct range.
ECLAIR's interface for range checks is the trait AssertWithinBitRange
:
#![allow(unused)] fn main() { /// WithinBitRange Assertion /// /// # Restrictions /// /// This `trait` assumes that `BITS > 0` and does not currently support `BITS = 0`. /// In this case we would have an assertion that `x < 2^0 = 1` which is just that /// `x = 0` in most systems. For this usecase, the [`Zero`] `trait` should be /// considered instead. pub trait AssertWithinBitRange<T, const BITS: usize> { /// Asserts that `value` is smaller than `2^BITS`. fn assert_within_range(&mut self, value: &T); } }
This trait is implemented by a compiler type COM
to specify how COM
constrains values of type T
to lie in the range specified by BITS
. The line
#![allow(unused)] fn main() { compiler.assert_within_range::<BITS>(value); }
causes the compiler to generate constraints that are satisfied only if value
lies within the range specified by BITS
.
Unsigned Integers
The AssertWithinBitRange
trait allows ECLAIR to handle unsigned integers within proof systems as finite field elements with a checked size. We define unsigned integers as a thin wrapper around a type T
:
#![allow(unused)] fn main() { /// Unsigned Integer pub struct UnsignedInteger<T, const BITS: usize>(T); }
One should think of this construction as analogous to representing a boolean value with a u8
. The u8
type is acting as a container for the boolean value. But this container is "too large" in the sense that many u8
values do not correspond to a boolean value. Before interpreting a u8
as a boolean it is necessary to check that its value lies in the range [0,1]
.
Similarly, when we work within a proving system over a finite field, we may need to use field elements as a container for unsigned integer types. In this case a range check is required to make sure that the value in this container really does have an interpretation as an unsigned integer of the given size.
The compiler type COM
does not appear as part of the UnsignedInteger
type, but it must be mentioned whenever we construct or mutate an UnsignedInteger
:
#![allow(unused)] fn main() { impl<T, const BITS: usize> UnsignedInteger<T, BITS> { /// Builds a new [`UnsignedInteger`] over `value` asserting that it does not /// exceed `BITS`many bits. pub fn new<COM>(value: T, compiler: &mut COM) > Self where COM: AssertWithinBitRange<T, BITS>, { compiler.assert_within_range(&value); Self::new_unchecked(value) } /// Mutates the underlying value of `self` with `f`, asserting that after /// mutation the value is still within the `BITS` range. pub fn mutate<F, U, COM>(&mut self, f: F, compiler: &mut COM) > U where COM: AssertWithinBitRange<T, BITS>, F: FnOnce(&mut T, &mut COM) > U, { let output = f(&mut self.0, compiler); compiler.assert_within_range(&self.0); output } } }
Observe that both functions require the trait bound COM: AssertWithinBitRange<T, BITS>
, meaning that the compiler must know how to constrain values of type T
to the range specified by BITS
. Before constructing an UnsignedInteger
with fn new
, compiler
generates constraints that guarantee that T
lies in the range specified by BITS
. Similarly, fn mutate
transforms an UnsignedInteger
's value in some way and generates constraints to ensure that the result of the transformation still lies within range before returning a value.
When COM = ()
is the native compiler, fn new
and fn mutate
would panic if the inner value of type T
exceeds the bitrange. In nonnative computation, compiler
would generate constraints that the inner value does not satisfy, resulting in an unsatisfied constraint system.
These functions can be seen at work in the implementation of Add
and AddAssign
for UnsignedInteger
:
#![allow(unused)] fn main() { impl<T, COM, const BITS: usize> Add<Self, COM> for UnsignedInteger<T, BITS> where T: Add<T, COM>, COM: AssertWithinBitRange<T::Output, BITS>, { type Output = UnsignedInteger<T::Output, BITS>; fn add(self, rhs: Self, compiler: &mut COM) > Self::Output { Self::Output::new(self.0.add(rhs.0, compiler), compiler) } } impl<T, COM, const BITS: usize> AddAssign<Self, COM> for UnsignedInteger<T, BITS> where COM: AssertWithinBitRange<T, BITS>, T: AddAssign<T, COM>, { fn add_assign(&mut self, rhs: Self, compiler: &mut COM) { self.mutate(lhs, compiler lhs.add_assign(rhs.0, compiler), compiler); } } }
As a thin wrapper around T
, UnsignedInteger<T, BITS>
inherits many implementations from T
. But not all operations that can be performed on T
result in a valid UnsignedInteger
. For example, fn add
uses the UnsignedInteger::new
function to construct its return value, telling compiler
to constrain that return value to the bitrange. Similarly fn add_assign
calls fn mutate
to mutate the value, again generating constraints that enforce a range check on the mutated value.
Checked vs Unchecked
Looking at the body of the UnsignedInteger::new
method we see that after a range check it uses fn new_unchecked
to construct its return value. ECLAIR exposes fn new_unchecked
as a public function because it allows for optimizations in instances where range checks are unnecessary.
For example, if T
implements Zero<COM>
or One<COM>
then we know that T
's zero/one value will pass any range check (we require BITS >= 1
for range checks, see AssertWithinBitRange
above). Thus the implementation is:
#![allow(unused)] fn main() { impl<T, const BITS: usize, COM> Zero<COM> for UnsignedInteger<T, BITS> where T: Zero<COM>, { type Verification = T::Verification; fn zero(compiler: &mut COM) > Self { Self::new_unchecked(T::zero(compiler)) } fn is_zero(&self, compiler: &mut COM) > Self::Verification { self.0.is_zero(compiler) } } }
In this instance it would be wasteful to add a range check to the value T::zero(compiler)
because the contract of the Zero
trait guarantees that this is within range. The same holds for T::one(compiler)
in the implementation of One<COM>
.
Another example where the unchecked construction should be used is the ConditionalSelect<COM>
trait (see Bool):
#![allow(unused)] fn main() { impl<T, const BITS: usize, COM> ConditionalSelect<COM> for UnsignedInteger<T, BITS> where COM: Has<bool>, T: ConditionalSelect<COM>, { fn select(bit: &Bool<COM>, true_value: &Self, false_value: &Self, compiler: &mut COM) > Self { Self::new_unchecked(T::select(bit, &true_value.0, &false_value.0, compiler)) } } }
Again it is appropriate to use unchecked construction because both true_value
and false_value
are of type UnsignedInteger
and so it would be wasteful to perform another range check on their inner values.
Ops
ECLAIR has analogues of many of Rust's overloadable operators. These are the traits like Neg
, Add
, Mul
, etc that overload the behavior of the 
, +
, *
operators.
By now you can probably guess how ECLAIR defines analogues of these traits: function signatures pick up a mutable reference compiler: &mut COM
to a compiler type and use this to generate constraints, when appropriate. For the native compiler COM = ()
, each trait is identical to its pure Rust analogue.
For example, the pure Rust trait Add<Rhs>
:
#![allow(unused)] fn main() { pub trait Add<Rhs = Self> { type Output; fn add(self, rhs: Rhs) > Self::Output; } }
is replaced with the ECLAIR trait Add<Rhs, COM>
:
#![allow(unused)] fn main() { pub trait Add<Rhs = Self, COM = ()> { type Output; fn add(self, rhs: Rhs, compiler: &mut COM) > Self::Output; } }
Now a line like
#![allow(unused)] fn main() { output = lhs.add(rhs, &mut compiler); }
causes compiler
to allocate a variable output
and constrain the value of output
to be the sum lhs + rhs
.
This straightforward transformation of traits is carried out for the following traits: Neg
, Not
, Add
, BitAnd
, BitOr
, BitXor
, Div
, Mul
, Rem
, Shl
, Shr
, Sub
, AddAssign
, BitAndAssign
, BitOrAssign
, BitXorAssign
, DivAssign
, MulAssign
, RemAssign
, ShlAssign
, ShrAssign
, SubAssign
. See the Rust documentation of these traits for more information.
Compiler Reflection
When some type T
implements Add<COM>
, this means that the compiler type COM
knows how to generate constraints that enforce correct addition of values of type T
. It can be useful to express this as a property of COM
rather than a property of T
, which ECLAIR does through "compiler reflection."
When T: Add<COM>
, compiler reflection means that COM: HasAdd<T>
. Explicitly, the HasAdd<T>
trait is
#![allow(unused)] fn main() { pub trait HasAdd<L, R = L> { /// Output Type /// The resulting type after applying the `+` operator. type Output; /// Performs the `lhs + rhs` operation over the /// `self` compiler. fn add(&mut self, lhs: L, rhs: R) > Self::Output; } }
So the line
#![allow(unused)] fn main() { output = lhs.add(rhs, &mut compiler); }
is equivalent to
#![allow(unused)] fn main() { output = compiler.add(lhs, rhs); }
For each of the traits listed above we include an implementation of the corresponding reflection trait:
#![allow(unused)] fn main() { impl<COM, L, R> HasAdd<L, R> for COM where L: Add<R, COM> { fn add(&mut self, lhs: L, rhs: R) > Self::Output { lhs.add(rhs, self) } } }
With this HasAdd
trait we can now use a trait bound COM: HasAdd<T>
to express the requirement that certain other ECLAIR traits or circuits make sense only for compilers that can add values of type T
.
Allocation
The alloc
module defines ECLAIR's interface for allocating values in a compiler. We use the term "allocation" here to refer to the process of declaring a variable in a ZK proof system and (maybe) assigning it a value. Note that we are not referring to memoryrelated abstractions like heap allocation.
Variables in a ZK proof system can be private witnesses, public inputs, constants, or some mixture of these. For example, in a merkle tree membership proof we would have variables representing the values stored:
 in some leaf of the tree
 along the path from that leaf to the root
 in the root of the tree.
In the simplest case, all those values have the same type  perhaps a finite field element. But in a ZKP, all those values should be private except the root, which would be public. So the description of this circuit must distinguish between public and private variables.
ECLAIR calls this distinction the "allocation mode." There are four allocation modes:

Constant: values that are proper to the circuit description and never change. These are public quantities known at compilation time.

Public: values that are public but may change in each instance of the circuit. For example, the root hash of a merkle tree. These values need to be exposed to the verifier in a ZKP.

Secret: values that are private. These values are known only to the prover in a ZKP and are never revealed.

Derived: values that are a composite of some public and secret values. For example, if the above merkle tree proof were considered as a single object then its allocation mode would be derived because it consists of both private and public values.
The constant allocation mode is substantially different from the other three in that constants are known at compilation time, whereas a variable's value will not be known until execution time when an instance of the circuit is constructed. For this reason, ECLAIR uses different interfaces for allocation of constants and variables.
Constants
The interface for allocating constants in ECLAIR is the Constant
trait:
#![allow(unused)] fn main() { pub trait Constant<COM = ()> { /// Underlying Type type Type; /// Allocates a new constant from `this` into the `compiler`. fn new_constant(this: &Self::Type, compiler: &mut COM) > Self; } }
So a type T
that implements Constant<COM>
has some "underlying type" Type
that it represents. Given values of that underlying type, we introduce them into our circuit description using fn new_constant
, which takes the underlying value this
, allocates it in the compiler
, and returns COM
's representation of the allocated value. We then use this output in our circuit description.
Note that ECLAIR assumes almost nothing about what it means to be a "constant"; it is up to the compiler COM
to define how constants should be represented and manipulated. The one assumption ECLAIR does make is that constant values are known at compilation time, i.e. they are a fixed part of the circuit description.
Variables
All other quantities whose values are not known at compilation time are considered to be "variables." ECLAIR allocates these using the Variable
trait:
#![allow(unused)] fn main() { pub trait Variable<M, COM = ()> { /// Underlying Type type Type; /// Allocates a new unknown value into the `compiler`. The terminology "unknown" /// refers to the fact that we need to allocate a slot for this variable during /// compilation time, but do not yet know its underlying value. fn new_unknown(compiler: &mut COM) > Self; /// Allocates a new known value from `this` into the `compiler`. The terminology /// "known" refers to the fact that we have access to the underyling value during /// execution time where we are able to use its concrete value for execution. fn new_known(this: &Self::Type, compiler: &mut COM) > Self; } }
As with constants, variables have an underlying Type
that they represent within COM
. This means that some type T
implementing Variable<M, COM>
is a Type
valued variable. The generic type M
specifies the allocation Mode, which can be Public
, Private
, or Derived
.
As with the Constant
allocation mode, ECLAIR makes no assumptions about what it means to be Public
, Private
or Derived
in a given COM
context. ECLAIR assumes only that a variable's value is not yet known at compilation time.
Known vs Unknown Allocation
Unlike constants, there are two ways of allocating variables: as known and unknown. Allocation using fn new_known
requires the variable's concrete value this
. Allocation using fn new_unknown
merely tells the compiler
that when execution occurs, a value of this Type
will go here.
Of course execution cannot actually occur until all variables have been provided a value. Allocating variables before their values are known using fn new_unknown
allows us to perform certain useful operations from the circuit description before execution time, akin to performing algebraic manipulations on physical formulae before substituting in concrete values for the variables.
For example, some proving systems require precomputed prover and verifier keys. When these are circuitspecific, they must be extracted from a circuit description. Since this occurs before execution time, we need a circuit description that accounts for all of the variables without assigning them a concrete value. Therefore a description of the circuit using fn new_unknown
to allocate variables is appropriate for computing the prover and verifier keys. At execution time, when the circuit is used to generate proofs, it is appropriate to allocate the same variables using fn new_known
.
This suggests an important principle of circuitwriting in ECLAIR: it is generally useful to separate variable allocation from variable manipulation. That is, one should identify the variables whose values are provided as inputs, either public or private, by the prover. Then, taking those as inputs, one writes a function to describe how they are manipulated according to the circuit logic.
Example: Merkle Tree Membership
To illustrate this we return to the merkle tree membership example we started with above. The relevant input values are:
 a leaf value:
leaf: L
 the values of all sibling nodes on a path from that leaf to the root:
path: P
 a root value:
root: R
The first two kinds of values are private, so we require that L: Variable<Secret, COM>
and P: Variable<Secret, COM>
. The root value is public, so we require R: Variable<Public, COM>
. The function that describes a merkle tree membership check would look something like this:
#![allow(unused)] fn main() { fn membership_check<L, P, R, COM>(leaf: L, path: P, root: R, compiler: &mut COM) where L: Variable<Secret, COM>, P: Variable<Secret, COM>, R: Variable<Public, COM> { // hash `leaf` with its sibling // hash the result with the next sibling in `path` // ... // assert that final result equals `root` } }
The body of this function will perform computations on the input variables, allocating new intermediate variables in the process and generating constraints within compiler
. Because we've specified that leaf
and path
allocate as Secret
and root
allocates as Public
, the constraint generation will occur in whatever way is appropriate for dealing with public and private variables in the context of COM
.
To extract a circuit description while leaving the variable values unknown, we might do something like this:
#![allow(unused)] fn main() { // Construct an instance of the compiler let mut compiler = CompilerType::new(); // Allocate variables with unknown values let leaf = Leaf::new_unknown(&mut compiler); let path = Path::new_unknown(&mut compiler); let root = Root::new_unknown(&mut compiler); // Generate membership check constraints membership_check(leaf, path, root, &mut compiler); }
Now compiler
has allocated all the intermediate variables for a membership check and generated the necessary constraints among them. We could then extract proving and verifying keys from it, or any other information that can be extracted from the circuit description without concrete values. Note that we cannot compute a ZKP from compiler
, since this would require concrete values for the variables.
In order to compute a ZKP in an instance where we have concrete values, we would do something like this:
#![allow(unused)] fn main() { // Construct an instance of the compiler let mut compiler = CompilerType::new(); // Allocate variables with known values let leaf = Leaf::new_known(leaf_value, &mut compiler); let path = Path::new_known(path_value, &mut compiler); let root = Root::new_known(root_value, &mut compiler); // Generate membership check constraints membership_check(leaf, path, root, &mut compiler); // Compute proof let proof = compiler.prove(); }
This time the compiler was able to compute a ZKP because the variables were allocated with known values.
As mentioned above, it was useful in this example to separate allocation and manipulation. All manipulation occurs within fn membership_check
, which takes arguments that are assumed to be already allocated in the compiler
. This ensured that the same manipulations would be performed on the symbolic and concrete forms of these variables.
(Of course many new variables are allocated as fn membership_check
performs its computation, but their values are not provided directly by the prover. Perhaps it is more correct to say that one should separate variable input from variable manipulation.)
Tutorial: Poseidon Permutation
The Poseidon permutation, defined in GKRRS '19 operates on vectors of field elements. For a fixed width, the permutation transforms a vector of width
many field elements in repeated rounds. Each round consists of the following operations:
 Add Round Keys: Add a constant to each component of the vector.
 SBox: Raise each component of the resulting vector to a power (in a full round), or raise just one component of the vector to a power (in a partial round).
 MDS Matrix: Multiply the resulting vector by a constant matrix.
This tutorial will walk through building the Poseidon permutation in ECLAIR. All OpenZL tutorials are accompanied by code examples, see here. Note that this code differs somewhat from our optimized Poseidon implementation.
trait Specification
The Poseidon permutation requires a choice of finite field. We will keep this example generic by using a Rust trait Specification
to specify our assumptions on the field and defining the Poseidon permutation relative to any type that implements Specification
.
#![allow(unused)] fn main() { /// Poseidon Specification /// /// This trait defines basic arithmetic operations we use to define the Poseidon permutation. pub trait Specification<COM = ()>: Constants { /// Field Type used for Permutation State type Field; /// Field Type used for Permutation Parameters type ParameterField; /// Returns the zero element of the field. fn zero(compiler: &mut COM) > Self::Field; /// Adds two field elements together. fn add(lhs: &Self::Field, rhs: &Self::Field, compiler: &mut COM) > Self::Field; /// Adds a field element `lhs` with a constant `rhs` fn add_const(lhs: &Self::Field, rhs: &Self::ParameterField, compiler: &mut COM) > Self::Field; /// Multiplies two field elements together. fn mul(lhs: &Self::Field, rhs: &Self::Field, compiler: &mut COM) > Self::Field; /// Multiplies a field element `lhs` with a constant `rhs` fn mul_const(lhs: &Self::Field, rhs: &Self::ParameterField, compiler: &mut COM) > Self::Field; /// Adds the `rhs` field element to `lhs` field element, updating the value in `lhs` fn add_assign(lhs: &mut Self::Field, rhs: &Self::Field, compiler: &mut COM); /// Adds the `rhs` constant to `lhs` field element, updating the value in `lhs` fn add_const_assign(lhs: &mut Self::Field, rhs: &Self::ParameterField, compiler: &mut COM); /// Applies the SBOX to `point`. fn apply_sbox(point: &mut Self::Field, compiler: &mut COM); /// Converts a constant parameter `point` for permutation state. fn from_parameter(point: Self::ParameterField) > Self::Field; } }
The trait requires two types, Field
and ParameterField
. The permutation acts on vectors of elements of type Field
. The constant parameters that define the permutation are of type ParameterField
. At first it may seem strange to distinguish between these two types, since they coincide for native computation of the Poseidon permutation. But remember that one of the reasons to use ECLAIR is to specify computation in a language that applies to both native and nonnative computation.
In practice we may need to compute Poseidon incircuit as part of a ZKproof. In this case the type Field
would be some representation of private witnesses to the circuit, whereas ParameterField
would be public input constants. These are quite different types indeed! Therefore it is appropriate to treat them as distinct for now and let the compiler
deal with them in whatever way is appropriate for the mode of computation specified by the type COM
.
Keeping in mind that the Field
type may represent incircuit variables, it is easy to see that we need two distinct notions of add
(and mul
). When adding two incircuit variables we use
#![allow(unused)] fn main() { fn add(lhs: &Self::Field, rhs: &Self::Field, compiler: &mut COM) > Self::Field; }
but when adding a constant to a variable it is appropriate to use
#![allow(unused)] fn main() { fn add_const(lhs: &Self::Field, rhs: &Self::ParameterField, compiler: &mut COM) > Self::Field; }
Although these two methods coincide for the native compiler type COM = ()
, in general they are distinct. This illustrates an important principle of circuit writing in ECLAIR: We describe circuits in a general language that applies to all modes of computation; this ensures that different instances of computation (native/incircuit) agree. Often it is useful to keep the more "exotic" case of incircuit computation in mind.
Note that we specify the default compiler type to be COM = ()
, meaning that by default we use the native compiler.
trait Constants
You may notice that the previous trait Specification
extends a trait Constants
. Constants
is a trait specifying three constant parameters that belong to the definition of a Poseidon permutation:
#![allow(unused)] fn main() { pub trait Constants { /// Width of the Permutation /// /// This number is the total number `t` of field elements in the state which is `F^t`. const WIDTH: usize; /// Number of Full Rounds /// /// The total number of full rounds in the Poseidon permutation, including the first set of full /// rounds and then the second set after the partial rounds. const FULL_ROUNDS: usize; /// Number of Partial Rounds const PARTIAL_ROUNDS: usize; /// Half Number of Full Rounds /// /// Poseidon Hash first has [`HALF_FULL_ROUNDS`]many full rounds in the beginning, /// followed by [`PARTIAL_ROUNDS`]many partial rounds in the middle, and finally /// [`HALF_FULL_ROUNDS`]many full rounds at the end. /// /// [`HALF_FULL_ROUNDS`]: Self::HALF_FULL_ROUNDS /// [`PARTIAL_ROUNDS`]: Constants::PARTIAL_ROUNDS const HALF_FULL_ROUNDS: usize = Self::FULL_ROUNDS / 2; /// Total Number of Rounds const ROUNDS: usize = Self::FULL_ROUNDS + Self::PARTIAL_ROUNDS; /// Number of Entries in the MDS Matrix const MDS_MATRIX_SIZE: usize = Self::WIDTH * Self::WIDTH; /// Total Number of Additive Rounds Keys const ADDITIVE_ROUND_KEYS_COUNT: usize = Self::ROUNDS * Self::WIDTH; } }
Here WIDTH
is the length of the vector of field elements that the permutation acts on via addition and matrix multiplication. FULL_ROUNDS
and PARTIAL_ROUNDS
specify the number of full and partial rounds of iteration that are performed on the state vector to achieve the desired security level. The remaining constants are computed in terms of the first three; they specify the number of "Additive Round Keys" and the size of the "MDS Matrix."
struct State
Given some type S
that implements the above Specification
trait we next define a state for the permutation to act on. This state is a vector of length WIDTH
. We'll use a struct State
to represent it:
#![allow(unused)] fn main() { /// The state vector that a Poseidon permutation acts on. pub struct State<S, COM = ()>(Box<[S::Field]>) where S: Specification<COM>; impl<S, COM> State<S, COM> where S: Specification<COM>, { /// Builds a new [`State`] from `state`. pub fn new(state: Box<[S::Field]>) > Self { assert_eq!(state.len(), S::WIDTH); Self(state) } /// Returns a slice iterator over the state. pub fn iter(&self) > slice::Iter<S::Field> { self.0.iter() } /// Returns a mutable slice iterator over the state. pub fn iter_mut(&mut self) > slice::IterMut<S::Field> { self.0.iter_mut() } } }
Observe that although the compiler type COM
plays no direct role in the definition of the State
vector, it must be mentioned because it provides the context to understand the trait Specification<COM>
. When COM
specifies some ZK proof system to compute the permutation in, the elements of State
will represent witness variables and the operations performed on State
will generate constraints in whatever representation COM
specifies. Again we have the default COM = ()
, meaning that when no compiler type is specified State
consists of native field elements and the operations performed on it are computed natively.
For Rustrelated reasons we choose not to specify the width as part of State
's type. Observe however that the constructor fn new
enforces that State
must have the size specified by S
via the Constants
trait.
struct Permutation
The final ingredient is the parameters, a collection of constants that define a particular instance of the Poseidon permutation. In each round the permutation adds some constants, the additive_round_keys
, to the State
and multiplies the State
by a constant matrix, the mds_matrix
. These precomputed constants are considered to be part of the definition of a Poseidon permutation. For information on generating secure constants, please refer to GKRRS '19.
Since these parameters define a specific instance of the Poseidon implementation, we call this struct Permutation
. We define the Permutation
to be generic over a type S
that implements Specification
:
#![allow(unused)] fn main() { /// The constant parameters defining a particular instance /// of the Poseidon permutation. pub struct Permutation<S, COM = ()> where S: Specification<COM>, { /// Additive Round Keys additive_round_keys: Box<[S::ParameterField]>, /// MDS Matrix mds_matrix: Box<[S::ParameterField]>, /// Type Parameter Marker __: PhantomData<COM>, } }
The additive_round_keys
can be thought of as a list of constants from F::ParameterField
, whereas the mds_matrix
should be thought of as a matrix; this struct carries the flattening of that matrix. The sizes of these arrays are determined by the same WIDTH
parameter that determines the length of State
. Again, we enforce these size constraints with the constructor rather than the type system:
#![allow(unused)] fn main() { impl<S, COM> Permutation<S, COM> where S: Specification<COM>, { /// Builds a new [`Permutation`] from `additive_round_keys` and `mds_matrix`. /// /// # Panics /// /// This method panics if the input vectors are not the correct size for the specified /// [`Specification`]. pub fn new( additive_round_keys: Box<[S::ParameterField]>, mds_matrix: Box<[S::ParameterField]>, ) > Self { assert_eq!( additive_round_keys.len(), S::ADDITIVE_ROUND_KEYS_COUNT, "Additive Rounds Keys are not the correct size." ); assert_eq!( mds_matrix.len(), S::MDS_MATRIX_SIZE, "MDS Matrix is not the correct size." ); Self { additive_round_keys, mds_matrix, __: PhantomData, } } } }
fn full_round
, fn partial_round
A full round of permutation begins by adding the next WIDTH
many additive round keys to the State
vector, then applying the "Sbox" to each entry of the vector. Observe that the Sbox operation is part of the Specification
trait, fn apply_sbox
. This operation on field elements is typically exponentiation to the power 3, 5, or 1.
A partial round of permutation also adds the next WIDTH
many additive round keys to the State
vector, but then applies the Sbox only to first element of this vector. The reason for mixing full and partial rounds is explained in GKRRS '19.
Both rounds finish by applying the MDS Matrix to the State
vector. Let's add these methods to the Permutation
:
#![allow(unused)] fn main() { impl<S, COM> Permutation<S, COM> where S: Specification<COM>, { /// Returns the additive keys for the given `round`. #[inline] pub fn additive_keys(&self, round: usize) > &[S::ParameterField] { let start = round * S::WIDTH; &self.additive_round_keys[start..start + S::WIDTH] } /// Computes the MDS matrix multiplication against the `state`. pub fn mds_matrix_multiply(&self, state: &mut State<S, COM>, compiler: &mut COM) { let mut next = Vec::with_capacity(S::WIDTH); for i in 0..S::WIDTH { let linear_combination = state .iter() .enumerate() .map((j, elem) S::mul_const(elem, &self.mds_matrix[S::WIDTH * i + j], compiler)) .collect::<Vec<_>>(); next.push( linear_combination .into_iter() .reduce(acc, next S::add(&acc, &next, compiler)) .unwrap(), ); } mem::swap(&mut next.into_boxed_slice(), &mut state.0); } /// Computes a full round at the given `round` index on the internal permutation `state`. pub fn full_round(&self, round: usize, state: &mut State<S, COM>, compiler: &mut COM) { let keys = self.additive_keys(round); for (i, elem) in state.iter_mut().enumerate() { S::add_const_assign(elem, &keys[i], compiler); S::apply_sbox(elem, compiler); } self.mds_matrix_multiply(state, compiler); } /// Computes a partial round at the given `round` index on the internal permutation `state`. pub fn partial_round(&self, round: usize, state: &mut State<S, COM>, compiler: &mut COM) { let keys = self.additive_keys(round); for (i, elem) in state.iter_mut().enumerate() { S::add_const_assign(elem, &keys[i], compiler); } S::apply_sbox(&mut state.0[0], compiler); self.mds_matrix_multiply(state, compiler); } } }
Note that fn full_round
and fn partial_round
take the round number as an input; this is so that they will take correct constants for the given round. Note that they also take the compiler
as an input. As we explained above, this enables these functions to generate constraints within the ZK proof system specified by the type COM
. For example, when adding round constants the add_const_assign
method will add a constraint to compiler
that enforces the addition of a public constant to the secret witness. Similarly, fn mds_matrix_multiply
generates constraints within compiler
to enforce that state
was multiplied by the MDS Matrix.
Again, when no COM
type is specified the default COM = ()
simply performs native computation without any constraint generation. The advantage of ECLAIR's COM
abstraction is the certainty that add_const_assign
or mds_matrix_multiply
always conform to the same definition whether they are being used in native or nonnative computation.
Putting it all Together: fn permute
Finally we combine the pieces to define the full permutation:
#![allow(unused)] fn main() { impl<S, COM> Permutation<S, COM> where S: Specification<COM>, { /// Computes the full permutation without the first round. fn permute(&self, state: &mut State<S, COM>, compiler: &mut COM) { for round in 0..S::HALF_FULL_ROUNDS { self.full_round(round, state, compiler); } for round in S::HALF_FULL_ROUNDS..(S::HALF_FULL_ROUNDS + S::PARTIAL_ROUNDS) { self.partial_round(round, state, compiler); } for round in (S::HALF_FULL_ROUNDS + S::PARTIAL_ROUNDS)..(S::FULL_ROUNDS + S::PARTIAL_ROUNDS) { self.full_round(round, state, compiler); } } } }
This function simply performs as many partial and full rounds as specified in the Constants
trait.
Proof System Plugins
One of the goals of OpenZL is to provide great flexibility with respect to ZK proof systems. Developers should focus on the business logic of their application without committing to a particular ZK proof system. ECLAIR makes this possible.
ECLAIR code describes computation in general terms that make minimal assumptions about the environment where that code will be executed. This is ideal in the early stage of production when we need a circuit description that conforms to our spec. But at some point we do have to turn words into actions and use ECLAIR code to create ZKPs. This is where plugins come in.
A proof system plugin provides the lowlevel instructions for variable allocation and constraint generation in a specific ZK proof system. The plugin defines how ECLAIR code is compiled to constraints and, ultimately, used to generate ZKPs.
As a technical note, it is not quite correct to say that a plugin targets a specific ZK proof system, but rather a specific implementation of a ZK proof system. For example, there is no such thing as a "Groth16 plugin"; rather, there is a plugin for the Arkworks implementation ArkGroth16.