跳到主要内容

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 non-native environment such as a ZK proving system may lack a natural boolean type. In order for ECLAIR to express bit-wise operations or truth-valued 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:

/// 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 non-zero element represents the boolean 1. We would specify this choice by an implementation:

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:

/// 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:

/// 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

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:

/// 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 self-explanatory.