BitAdder<Logic, N>

Header: circuits/logic/bit_adder.h

A cheap field-level encoding of an N-bit value. The encoding has two properties:

1. Summing two encoded values is a single field operation — add for prime fields, mul for GF(2^k).
2. Given an encoded value E claimed to equal the sum of k N-bit inputs, a low-depth circuit verifies E == A (mod 2^N).

This makes BitAdder the preferred tool when a circuit needs to check that a field sum of bit-vectors matches a wider accumulator — for example, in SHA message scheduling.

Dispatch

template <class Logic, size_t N, bool kCharacteristicTwo>
class BitAdderAux;
 
template <class Logic, size_t N>
using BitAdder = BitAdderAux<Logic, N, Logic::Field::kCharacteristicTwo>;

There are two specializations, selected by the characteristic of the field. Both expose the same surface.

Common surface

using Field = typename Logic::Field;
using BitW  = typename Logic::BitW;
using EltW  = typename Logic::EltW;
using BV    = typename Logic::template bitvec<N>;
 
explicit BitAdder(const Logic& l);
 
EltW as_field_element(const BV& v) const;
 
EltW add(const EltW& a, const EltW& b) const;
EltW add(const BV&   a, const BV&   b) const;
EltW add(std::initializer_list<typename Logic::template bitvec_view<N>> a) const;
 
void assert_eqmod(const BV& a, const EltW& b, size_t k) const;

as_field_element

Embeds a bitvec<N> into the field under the chosen encoding.

• Prime fields (large characteristic): Σ 2^i · v[i], using axpy.
• GF(2^k): Π_{i : v[i]=1} α^{2^i}, where α = F.x() is a root of unity of sufficient order — i.e. a multiplicative encoding.

add

Combines two encoded values. In a prime field this is ordinary addition; in GF(2^k) it is field multiplication, matching the encoding. The initializer_list overload reduces a variadic list.

assert_eqmod

void assert_eqmod(const BV& a, const EltW& b, size_t k) const;

Asserts that b == a + i · 2^N for some 0 ≤ i < k — equivalently, that b ≡ a (mod 2^N) with the overflow bounded by k.

• Prime fields: computes z = b − as_field_element(a) and asserts that Π_{i=0}^{k-1} (z − i · 2^N) == 0.
• GF(2^k): uses the multiplicative analog — asserts Π_{i=0}^{k-1} (b − α^{i · 2^N} · as_field_element(a)) == 0, where the coefficients α^{i · 2^N} are precomputed in the constructor.