|
| | 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, const bool &use_range_constraint=false) |
| | 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, the 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 | is_inverted () 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_witness_index () const |
| | Get the witness index of the current boolean element.
|
| |
| 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 | clear_round_provenance () const |
| |
| void | fix_witness () |
| |
template<typename
Builder>
class bb::stdlib::bool_t< Builder >
Implements boolean logic in-circuit.
Representing bools 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.
Detailed example of an operation (logical OR)
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).
Definition at line 59 of file bool.hpp.
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
- w_a.(i_b.(1 - 2.i_a)) -> q_1 coefficient
- w_b.(i_a.(1 - 2.i_b)) -> q_2 coefficient
- i_a.i_b -> q_c 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.
Definition at line 159 of file bool.cpp.
1.9.8