Barretenberg
The ZK-SNARK library at the core of Aztec
|
Implements boolean logic in-circuit. More...
#include <bool.hpp>
Public Member Functions | |
bool_t (const bool value=false) | |
Construct a constant bool_t object from a bool value. | |
bool_t (Builder *parent_context) | |
Construct a constant bool_t object with a given Builder argument, its value is false . | |
bool_t (Builder *parent_context, const bool value) | |
Construct a constant bool_t object from a bool value with a given Builder argument. | |
bool_t (const witness_t< Builder > &value) | |
Construct a bool_t object from a witness, note that the value stored at witness_index is constrained to be 0 or 1. | |
bool_t (const bool_t &other) | |
bool_t (bool_t &&other) | |
bool_t & | operator= (const bool other) |
Assigns a native bool to bool_t object. | |
bool_t & | operator= (const witness_t< Builder > &other) |
Assigns a witness_t to a bool_t . As above, he value stored at witness_index is constrained to be 0 or 1. | |
bool_t & | operator= (const bool_t &other) |
Assigns a bool_t to a bool_t object. | |
bool_t & | operator= (bool_t &&other) |
Assigns a bool_t to a bool_t object. | |
bool_t | operator& (const bool_t &other) const |
Implements AND in circuit. | |
bool_t | operator| (const bool_t &other) const |
Implements OR in circuit. | |
bool_t | operator^ (const bool_t &other) const |
Implements XOR in circuit. | |
bool_t | operator! () const |
Implements negation in circuit. | |
bool_t | operator== (const bool_t &other) const |
Implements equality operator in circuit. | |
bool_t | operator!= (const bool_t &other) const |
Implements the not equal operator in circuit. | |
bool_t | operator~ () const |
bool_t | operator&& (const bool_t &other) const |
bool_t | operator|| (const bool_t &other) const |
bool_t | implies (const bool_t &other) const |
Implements implication operator in circuit. | |
bool_t | implies_both_ways (const bool_t &other) const |
Implements a "double-implication" (<=>), a.k.a "iff", a.k.a. "biconditional". | |
void | operator|= (const bool_t &other) |
void | operator&= (const bool_t &other) |
void | operator^= (const bool_t &other) |
void | assert_equal (const bool_t &rhs, std::string const &msg="bool_t::assert_equal") const |
Implements copy constraint for bool_t elements. | |
void | must_imply (const bool_t &other, std::string const &msg="bool_t::must_imply") const |
Constrains the (a => b) == true. | |
bool | get_value () const |
bool | is_constant () const |
bool_t | normalize () const |
A bool_t element is normalized if witness_inverted == false . For a given *this , output its normalized version. | |
uint32_t | get_normalized_witness_index () const |
Builder * | get_context () const |
void | set_origin_tag (const OriginTag &new_tag) const |
OriginTag | get_origin_tag () const |
void | set_free_witness_tag () |
void | unset_free_witness_tag () |
void | fix_witness () |
Static Public Member Functions | |
static bool_t | conditional_assign (const bool_t< Builder > &predicate, const bool_t &lhs, const bool_t &rhs) |
Implements the ternary operator - if predicate == true then return lhs, else return rhs. | |
Public Attributes | |
Builder * | context = nullptr |
bool | witness_bool = false |
bool | witness_inverted = false |
uint32_t | witness_index = IS_CONSTANT |
OriginTag | tag {} |
Implements boolean logic in-circuit.
To avoid constraining negation operations, we represent an in-circuit boolean \( a \) by a witness value \( w_a
\) and an witness_inverted
flag \( i_a \). The value of \( a \) is defined via the equation:
\begin{align} w_a \oplus i_a = w_a + i_a - 2 \cdot i_a \cdot w_a \end{align}
and can be read from the following table
w_a | i_a | a = w_a + i_a - 2 i_a w_a |
---|---|---|
0 | 0 | 0 |
0 | 1 | 1 |
1 | 0 | 1 |
1 | 1 | 0 |
When a new bool_t element \( a \) is created, its witness_inverted
flag is set to false
and its witness_value
is constrained to be \( 0 \) or \( 1\). More precisely, if \( a \) is a witness, then we add a boolean constraint ensuring \( w_a^2 = w_a \), if \( a \) is a constant bool_t element, then it's checked by an ASSERT.
To negate \( a \) we simply flip the flag. Other basic operations are deduced from their algebraic representations and the result is constrained to satisfy corresponding algebraic equation.
For example, to produce \( a || b \) in circuit, we compute
\begin{align} a + b - a \cdot b = ( w_a \cdot (1- 2 i_a) + i_a) + ( w_b \cdot (1 - 2 i_b) + i_b) - ( w_a \cdot (1-2 i_a) + i_a) ( w_b \cdot (1 - 2 i_b) + i_b) \end{align}
Thus we can use a poly
gate to constrain the result of a || b as follows:
\begin{align} q_m \cdot w_a \cdot w_b + q_l \cdot w_a + q_r \cdot w_b + q_o \cdot (a || b) + q_c = 0\end{align}
where
\begin{eqnarray*} q_m &=& -(1 - 2*i_a) * (1 - 2*i_b) \\ q_l &=& (1 - 2 * i_a) * (1 - i_b) \\ q_r &=& (1 - 2 * i_b) * (1 - i_a) \\ q_o &=& -1 \\ q_c &=& i_a + i_b - i_a * i_b \end{eqnarray*}
As \( w_a \) and \( w_b \) are constrained to be boolean, \( i_a \), \( i_b\) are boolean flags, we see that \( (a || b)^2 = (a || b)\) (as a field element).
bb::stdlib::bool_t< Builder >::bool_t | ( | const bool | value = false | ) |
bb::stdlib::bool_t< Builder >::bool_t | ( | Builder * | parent_context | ) |
bb::stdlib::bool_t< Builder >::bool_t | ( | Builder * | parent_context, |
const bool | value | ||
) |
bb::stdlib::bool_t< Builder >::bool_t | ( | const witness_t< Builder > & | value | ) |
bb::stdlib::bool_t< Builder >::bool_t | ( | const bool_t< Builder > & | other | ) |
bb::stdlib::bool_t< Builder >::bool_t | ( | bool_t< Builder > && | other | ) |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
bool_t< Builder > bb::stdlib::bool_t< Builder >::normalize | ( | ) | const |
bool_t< Builder > bb::stdlib::bool_t< Builder >::operator! | ( | ) | const |
bool_t< Builder > bb::stdlib::bool_t< Builder >::operator!= | ( | const bool_t< Builder > & | other | ) | const |
bool_t< Builder > bb::stdlib::bool_t< Builder >::operator& | ( | const bool_t< Builder > & | other | ) | const |
Implements AND in circuit.
A bool can be represented by a witness value w
and an 'inverted' flag i
A bool's value is defined via the equation: w + i - 2.i.w
w | i | w + i - 2.i.w |
---|---|---|
0 | 0 | 0 |
0 | 1 | 1 |
1 | 0 | 1 |
1 | 1 | 0 |
For two bools (w_a, i_a), (w_b, i_b), the & operation is expressed as:
(w_a + i_a - 2.i_a.w_a).(w_b + i_b - 2.i_b.w_b)
This can be rearranged to:
w_a.w_b.(1 - 2.i_b - 2.i_a + 4.i_a.i_b) -> q_m coefficient
Note that since the value of the product above is always boolean, we don't need to add an explicit range constraint for result
.
|
inline |
bool_t< Builder > & bb::stdlib::bool_t< Builder >::operator= | ( | const bool | other | ) |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
|
mutable |
|
mutable |
|
mutable |
|
mutable |
|
mutable |