Boojum Gadgets
Gadgets in ZK programming are common arrangement of circuits abstracted for ease of use. Boojum gadgets are low-level implementations of tools for constraint systems. They consist of various types such as curves, hash functions, lookup tables, and different circuit types.
These gadgets are mostly a reference from franklin-crypto, with additional hash functions added. These gadgets have been changed to use the Goldilocks field (order 2^64 - 2^32 + 1), which is much smaller than bn256. This allows us to reduce the proof system.
Circuits types
We have next types with we use for circuits:
Num (Number):
pub struct Num<F: SmallField> {
pub(crate) variable: Variable,
pub(crate) _marker: std::marker::PhantomData<F>,
}
Boolean:
pub struct Boolean<F: SmallField> {
pub(crate) variable: Variable,
pub(crate) _marker: std::marker::PhantomData<F>,
}
U8:
pub struct UInt8<F: SmallField> {
pub(crate) variable: Variable,
pub(crate) _marker: std::marker::PhantomData<F>,
}
U16:
pub struct UInt16<F: SmallField> {
pub(crate) variable: Variable,
pub(crate) _marker: std::marker::PhantomData<F>,
}
U32:
pub struct UInt32<F: SmallField> {
pub(crate) variable: Variable,
pub(crate) _marker: std::marker::PhantomData<F>,
}
U160:
pub struct UInt160<F: SmallField> {
pub inner: [UInt32<F>; 5],
}
U256:
pub struct UInt256<F: SmallField> {
pub inner: [UInt32<F>; 8],
}
U512:
pub struct UInt512<F: SmallField> {
pub inner: [UInt32<F>; 16],
}
Every type consists of a Variable (the number inside Variable is just the index):
pub struct Variable(pub(crate) u64);
which is represented in the current Field. Variable is quite diverse. To have "good" alignment and size we manually do encoding management to be able to represent it as both a variable (that can be copied) or witness.
The implementation of this circuit type itself is similar. We can also divide them into classes as main and dependent: Such type like U8-U512 decoding inside functions to Num<F> for using them in logical operations. As mentioned above, the property of these types is to perform logical operations and allocate witnesses.
Let's demonstrate this in a Boolean example:
impl<F: SmallField> CSAllocatable<F> for Boolean<F> {
type Witness = bool;
fn placeholder_witness() -> Self::Witness {
false
}
#[inline(always)]
fn allocate_without_value<CS: ConstraintSystem<F>>(cs: &mut CS) -> Self {
let var = cs.alloc_variable_without_value();
Self::from_variable_checked(cs, var)
}
fn allocate<CS: ConstraintSystem<F>>(cs: &mut CS, witness: Self::Witness) -> Self {
let var = cs.alloc_single_variable_from_witness(F::from_u64_unchecked(witness as u64));
Self::from_variable_checked(cs, var)
}
}
As you see, you can allocate both with and without witnesses.
Hash function
In gadgets we have a lot of hast implementation:
- blake2s
- keccak256
- poseidon/poseidon2
- sha256
Each of them perform different functions in our proof system.
Queues
One of the most important gadgets in our system is queue. It helps us to send data between circuits. Here is the quick explanation how it works:
Struct CircuitQueue{
head: HashState,
tail: HashState,
length: UInt32,
witness: VecDeque<Witness>,
}
The structure consists of head
and tail
commitments that basically are rolling hashes. Also, it has a length
of
the queue. These three fields are allocated inside the constraint system. Also, there is a witness
, that keeps actual
values that are now stored in the queue.
And here is the main functions:
fn push(&mut self, value: Element) {
// increment length
// head - hash(head, value)
// witness.push_back(value.witness)
}
fn pop(&mut self) -> Element {
// check length > 0
// decrement length
// value = witness.pop_front()
// tail = hash(tail, value)
// return value
}
fn final_check(&self) -> Element {
// check that length == 0
// check that head == tail
}
So the key point, of how the queue proofs that popped elements are the same as pushed ones, is equality of rolling
hashes that stored in fields head
and tail
.
Also, we check that we can’t pop an element before it was pushed. This is done by checking that length >= 0
.
Very important is making the final_check
that basically checks the equality of two hashes. So if the queue is never
empty, and we haven’t checked the equality of head
and tail
in the end, we also haven’t proven that the elements we
popped are correct.
For now, we use poseidon2 hash. Here is the link to queue implementations:
The difference is that we actually compute and store a hash inside CircuitQueue during push
and pop
operations. But
in FullStateCircuitQueue our head
and tail
are just states of sponges. So instead of computing a full hash, we just
absorb a pushed (popped) element.