Function binius_core::protocols::lasso::prove

pub fn prove<'a, FC, U, F, FW, L, Backend>(
    oracles: &mut MultilinearOracleSet<F>,
    witness_index: MultilinearExtensionIndex<'a, U, FW>,
    lasso_claim: &LassoClaim<F>,
    lasso_witness: LassoWitness<'a, PackedType<U, FW>, L>,
    lasso_batches: &LassoBatches,
    gamma: F,
    alpha: F,
    backend: Backend
) -> Result<LassoProveOutput<'a, U, FW, F>, Error>
where
    U: UnderlierType + PackScalar<FW> + PackScalar<FC>,
    FC: TowerField,
    PackedType<U, FC>: PackedFieldIndexable,
    PackedType<U, FW>: PackedFieldIndexable,
    F: TowerField + From<FW> + ExtensionField<FC>,
    FW: TowerField + ExtensionField<FC> + From<F>,
    L: AsRef<[usize]>,
    Backend: ComputationBackend + 'static,

Prove a Lasso instance reduction.

Given $\nu$-variate multilinear $T$ (the “lookup table”) and array of $U$ (the “looker columns”) and a array of mappings $U \mapsto T$ from hypercube vertices of $U$ to hypercube vertices of $T$, represented by an array u_to_t_mapping of vertex indices, we define multilinears $C$ (for “counts”) as identically-0 polynomial and $F$ (for “final counts”) as identically-1 polynomial and $g$ as the Multiplicative generator of subgroup, and perform the following algorithm:

 for i in len(U)
   for j in len(U[i])
	   m := u_to_t_mappings[j]
	   C[i][j] := F[m]
	   F[m] *= g

The order of multiplicative subgroup must be sufficient to represent $\sum len(U_{i})$ elements, and is specified via FC type parameter.

We then proceed by defining a virtual oracles $O$ as identically-1 polynomial and $P = g \times C$, and reduce tables to grand product claims:

$\prod_{v∈B}(\gamma + U_{0}(v) + \alpha * C_{0}(v)) = L_{0}$
$\dots$
$\prod_{v∈B}(\gamma + U_{n}(v) + \alpha * C_{n}(v)) = L_{n}$
$\prod_{v∈B}(\gamma + T(v) + \alpha * F(v)) = L_{n+1}$

$\prod_{v∈B}(\gamma + U_{0}(v) + \alpha * P_{0}(v)) = R_{0}$
$\dots$
$\prod_{v∈B}(\gamma + U_{n}(v) + \alpha * P_{n}(v)) = R_{n}$
$\prod_{v∈B}(\gamma + T(v)+\alpha * O(v)) = R_{n+1}$

$\prod_{v∈B} C_{0}(v) = Z_{0}$
$\dots$
$\prod_{v∈B} C_{n}(v) = Z_{n}$
$\prod_{v∈B} F(v) = Z_{n+1}$

And check that $\prod_{i=0}^{n+1} L_{i} = \prod_{i=0}^{n+1} R_{i}$ and $\prod_{i=0}^{n+1} Z_{i}$ ≠ $0$
See Section 4.4 of DP23 for the proofs.