`Counter<Logic>`

Header: circuits/logic/counter.h

Counter embeds small unsigned integers (about 16 bits’ worth) into an additive group, while keeping the type distinct from EltW to avoid confusion at call sites. Like BitAdder, it dispatches on the field characteristic:

Prime fields: the integer is injected as a field element; addition is field addition.
Binary fields (GF(2^k)): the integer is encoded in the multiplicative group generated by F.g(); addition is field multiplication.

Dispatch


template <class Logic, bool kCharacteristicTwo> class CounterAux;
 
template <class Logic>
using Counter = CounterAux<Logic, Logic::Field::kCharacteristicTwo>;

Common surface

Both specializations expose:


using Field = typename Logic::Field;
using EltW  = typename Logic::EltW;
using BitW  = typename Logic::BitW;
using CElt  = typename Field::CElt;
 
struct CEltW { EltW e; };               // wire-borne counter value
 
explicit Counter(const Logic& l);
 
const Logic& logic() const;
 
EltW znz_indicator(const CEltW& celt) const;   // zero iff celt is the additive id
 
CEltW mone() const;                             // "-1"
CEltW as_counter(uint64_t n) const;
CEltW as_counter(const CElt& x) const;
CEltW as_counter(const BitW& b) const;
 
template <size_t N>
CEltW as_counter(const typename Logic::template bitvec<N>& v) const;
 
CEltW add(const CEltW& a, const CEltW& b) const;
 
CEltW ite0(const BitW& a, const CEltW& b) const;                 // a ? b : 0
CEltW mux (const BitW& a, const CEltW& b, const CEltW& c) const; // a ? b : c
 
void assert0  (const CEltW& a) const;
void assert_eq(const CEltW& a, const CEltW& b) const;
 
CEltW input() const;

Semantics note

znz_indicator is the bridge between CEltW and the rest of the arithmetic-circuit world: it returns an EltW that is zero iff the counter represents the additive identity. In the prime-field specialization it is the counter itself; in the GF(2^k) specialization it is celt − 1 — reflecting that the identity of the multiplicative group encoding is 1, not 0.

assert0 is specialized in the same way: on GF(2^k) it asserts a == 1 in the underlying field.