Struct Witness 

pub struct Witness<'a, 'alloc, A: Allocator, P: PackedField> {

    pub a_exponents: &'a [Word],
    pub a_prodcheck: ProdcheckProver<'alloc, A, P>,
    pub a_root: FieldVec<P, A>,
    pub b_exponents: &'a [Word],
    pub b_leaves: FieldVec<P, A>,
    pub b_prodcheck: ProdcheckProver<'alloc, A, P>,
    pub b_root: FieldVec<P, A>,
    pub c_lo_exponents: &'a [Word],
    pub c_lo_prodcheck: ProdcheckProver<'alloc, A, P>,
    pub c_lo_root: FieldVec<P, A>,
    pub c_hi_exponents: &'a [Word],
    pub c_hi_prodcheck: ProdcheckProver<'alloc, A, P>,
    pub c_hi_root: FieldVec<P, A>,
    pub tables: Vec<FieldVec<P, A>>,
}

An integer multiplication protocol witness. Created from integer slices, consumed during proving.

The statement being proven is a * b = c, where c is represented as a pair (c_lo, c_hi): Word::BITS-wide multiplicands with a double-wide product.

For each of a, c_lo, c_hi the exponent words split into N_LIMBS limbs, and the constant-base exponentiation factors as a product of N_LIMBS limb columns — column l reads the row limb_l(e) of the power table of the base $G^{2^{wl}}$ (where $w$ is the limb bit width). The columns are concatenated into one (n_vars + LOG_N_LIMBS)-variate buffer with the limb index in the high bits, and a ProdcheckProver is constructed over each:

1. a and c_lo exponentiate the multiplicative group generator $G$
2. c_hi exponentiates $G^{2^{2^m}}$
3. b selects a variable base (the root of the a tree) per bit, over Word::BITS per-bit leaves as before

The shared power table $T\colon i \mapsto G^i$ over $2^w$ rows is retained for the Phase 5 logup* lookup.

Protocol proves that ${(G^a)}^b = G^{c\_lo} \times (G^{2^{2^m}})^{c\_hi}$, which is equivalent to $a \times b = c$ modulo $2^{2^{m+1}} - 1$. The special case of 0 * 0 = 1 is handled separately.

Fields

a_exponents: &'a [Word]

The exponents for a (needed for the phase 5 lookup indices and parity zerocheck on a_0).

a_prodcheck: ProdcheckProver<'alloc, A, P>

Prodcheck prover for the a exponentiation tree (leaf layer retained).

a_root: FieldVec<P, A>

The root of the a tree (product of all leaves element-wise); the b variable base.

b_exponents: &'a [Word]

The exponents for b (needed for phase 5).

b_leaves: FieldVec<P, A>

Concatenated b leaves for prodcheck: [L_0, L_1, …, L_{2^k-1}]. Has log_len = n_vars + Word::LOG_BITS.

b_prodcheck: ProdcheckProver<'alloc, A, P>

The prover for the prodcheck reduction on b_leaves.

b_root: FieldVec<P, A>

The root of the b tree (product of all leaves element-wise).

c_lo_exponents: &'a [Word]

The exponents for c_lo (needed for the phase 5 lookup indices, parity zerocheck on c_lo_0, and the raw per-bit output evaluations).

c_lo_prodcheck: ProdcheckProver<'alloc, A, P>

Prodcheck prover for the c_lo exponentiation tree (leaf layer retained).

c_lo_root: FieldVec<P, A>

The root of the c_lo tree.

c_hi_exponents: &'a [Word]

The exponents for c_hi (needed for the phase 5 lookup indices and raw per-bit output evaluations).

c_hi_prodcheck: ProdcheckProver<'alloc, A, P>

Prodcheck prover for the c_hi exponentiation tree (leaf layer retained).

c_hi_root: FieldVec<P, A>

The root of the c_hi tree.

tables: Vec<FieldVec<P, A>>

The 2·N_LIMBS twisted power tables: tables[s][i] = (G^{2^{ws}})^i. Limb column (t, l) is a gather from table s(t, l); tables[0] is the shared table read by the Phase 5 logup* lookup.

Implementations

impl<'a, 'alloc, A: Allocator, P: PackedField> Witness<'a, 'alloc, A, P>

pub fn a_prodcheck(&self) -> &ProdcheckProver<'alloc, A, P>

Prodcheck prover for the a exponentiation tree (leaf layer retained).

pub fn a_root(&self) -> &FieldVec<P, A>

The root of the a tree (product of all leaves element-wise); the b variable base.

pub fn b_leaves(&self) -> &FieldVec<P, A>

Concatenated b leaves for prodcheck: [L_0, L_1, …, L_{2^k-1}]. Has log_len = n_vars + Word::LOG_BITS.

pub fn b_prodcheck(&self) -> &ProdcheckProver<'alloc, A, P>

The prover for the prodcheck reduction on b_leaves.

pub fn b_root(&self) -> &FieldVec<P, A>

The root of the b tree (product of all leaves element-wise).

pub fn c_lo_prodcheck(&self) -> &ProdcheckProver<'alloc, A, P>

Prodcheck prover for the c_lo exponentiation tree (leaf layer retained).

pub fn c_lo_root(&self) -> &FieldVec<P, A>

The root of the c_lo tree.

pub fn c_hi_prodcheck(&self) -> &ProdcheckProver<'alloc, A, P>

Prodcheck prover for the c_hi exponentiation tree (leaf layer retained).

pub fn c_hi_root(&self) -> &FieldVec<P, A>

The root of the c_hi tree.

pub fn tables(&self) -> &Vec<FieldVec<P, A>>

The 2·N_LIMBS twisted power tables: tables[s][i] = (G^{2^{ws}})^i. Limb column (t, l) is a gather from table s(t, l); tables[0] is the shared table read by the Phase 5 logup* lookup.

impl<'a, 'alloc, A, F, P> Witness<'a, 'alloc, A, P>

where A: Allocator, F: BinaryField, P: PackedField<Scalar = F>,

pub fn new( alloc: &'alloc A, a: &'a [Word], b: &'a [Word], c_lo: &'a [Word], c_hi: &'a [Word], ) -> Result<Self, Error>

Constructs a new integer multiplication witness from the statement.

The GKR prodcheck provers draw their layer buffers from alloc.

The four columns must have equal length, but need not have a power-of-two one: the reduction runs over the constraint axis of 2^ceil(log2(n)) rows, and the rows past the columns’ end read as Word::ZERO. Every buffer built here still spans that whole axis, and each derives its own value for a padding row rather than being handed one. In the product-check trees that value is the multiplicative identity, not zero: a zero exponent word indexes row 0 of a power table, which holds base^0 = 1. So no tree’s product moves.

Trait Implementations

impl<A: Allocator, P: PackedField> Clone for Witness<'_, '_, A, P>

where A::Vec<P>: Clone,

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.