Bus in different field -1

the goal is to understand the extra cost (witness column) brought by using different field, in the bus part.

start with lookup_via_challenges_range_constraint.asm

use std::convert::fe;
use std::protocols::lookup::lookup;
use std::math::fp2::from_base;
use std::prover::challenge;

machine Main with degree: 8 {

    // Prove a correct decomposition of x into 3-bit limbs
    col fixed x = [1, 6, 23, 55, 63, 4, 1, 0];
    col witness x_low, x_high;

    col fixed BIT3 = [0, 1, 2, 3, 4, 5, 6, 7];

    lookup([x_low] in [BIT3]);
    lookup([x_high] in [BIT3]);

    x = x_low + 8 * x_high;
}

BN254 field

run this command to spell out Logup constraint without field extension.

cargo run pil test_data/std/lookup_via_challenges_range_constraint.asm -o output -f --field bn254

the generated …_opt.pil file:

code and constraint explanation:

Logup constraint:

accumulator initiate:

main::is_first * main::acc = 0;

logup constraint:

(std::prelude::challenge(0, 2) - main::x_low) * (std::prelude::challenge(0, 2) - main::BIT3) * (main::acc' - main::acc) + main::multiplicities * (std::prelude::challenge(0, 2) - main::x_low) = std::prelude::challenge(0, 2) - main::BIT3;

to make it more clear, let “std::prelude::challenge(0, 2)” to be \(\alpha\)

then the equation essentially become:

\((\alpha-x_{low}) \cdot (\alpha – BIT_3)\cdot (acc’-acc)+mul\cdot (\alpha-x_{low})= \alpha – BIT_3\)

divided by \((\alpha-x_{low}) \cdot (\alpha – BIT_3)\) from both side, it becomes:

\(acc’-acc=\frac{1}{\alpha-x_{low}}-\frac{mul}{\alpha – BIT_3}\)

which is Logup constraint.

acc and acc_1 are two columns, for x_low and x_high

stage

pay attention that acc and acc_1 are both for stage 1, which can only be calculated after the challenge is drawn.

Goldilock field

it becomes verbose with many different namespace, let’s focus on the main machine now:

let’s see the logup constraint now:

((std::prelude::challenge(0, 3) - main::x_low) * (std::prelude::challenge(0, 3) - main::BIT3) + 11 * std::prelude::challenge(0, 4) * std::prelude::challenge(0, 4)) * (main::acc' - main::acc) + 11 * (std::prelude::challenge(0, 4) * (std::prelude::challenge(0, 3) - main::BIT3) + (std::prelude::challenge(0, 3) - main::x_low) * std::prelude::challenge(0, 4)) * (main::acc_1' - main::acc_1) + main::multiplicities * (std::prelude::challenge(0, 3) - main::x_low) = std::prelude::challenge(0, 3) - main::BIT3;
    (std::prelude::challenge(0, 4) * (std::prelude::challenge(0, 3) - main::BIT3) + (std::prelude::challenge(0, 3) - main::x_low) * std::prelude::challenge(0, 4)) * (main::acc' - main::acc) + ((std::prelude::challenge(0, 3) - main::x_low) * (std::prelude::challenge(0, 3) - main::BIT3) + 11 * std::prelude::challenge(0, 4) * std::prelude::challenge(0, 4)) * (main::acc_1' - main::acc_1) + main::multiplicities * std::prelude::challenge(0, 4) = std::prelude::challenge(0, 4);

it is related to extension field operations, for 2 degree extension field, check this file

The irreducible polynomial is \(x^2 -11\), so the multiplication would be:

BN254 and Goldilock comparison of lookup_via_challenges..asm:

	wit cols	fixed col	wit: 2	logup wit	fixed	pattern
BN254	6	3	\(x_{low}\), \(x_{high}\)	\(acc, acc_1, \) for \(x_{low}\) for \(x_{high}\) \(mul, mul_1\) total: 4	\(x\), \(BIT_3\), is_first total: 3	2+4 4 is the non-changeable \(x_{low}\), \(x_{high}\) \(mul, mul_1\)
Goldilock	12	3	\(x_{low}\), \(x_{high}\)	\(acc, acc_1, \) for \(x_{low}\) \(acc_2, acc_3, \) for \(x_{high}\) \(acc_{next},\) \(acc_{next_1}, \) \(acc_{next_2},\) \(acc_{next_3}, \) \(mul, mul_1\) total: 10	\(x\), \(BIT_3\), is_first total: 3	2*4 + 4
M31	20	3

BN254 and Goldilock comparison of keccak.asm:

	wit cols	fixed col	stage 1 witness	pattern
BN254 bus linker mod	270	125	\(acc, acc_1, \) total: 48
Goldilock bus linker mode	453	125	\(acc, acc_1, \) \(acc_2, acc_3, \) total: 230
M31 bus linker mode	596	97	total: 596
m31 native	172	81