Struct arrabbiata::witness::Env

pub struct Env<Fp: PrimeField, Fq: PrimeField, E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>, E2: ArrabbiataCurve<ScalarField = Fq, BaseField = Fp>> {

    pub domain_fp: EvaluationDomains<Fp>,
    pub domain_fq: EvaluationDomains<Fq>,
    pub srs_e1: SRS<E1>,
    pub srs_e2: SRS<E2>,
    pub ivc_accumulator_e1: Vec<PolyComm<E1>>,
    pub ivc_accumulator_e2: Vec<PolyComm<E2>>,
    pub previous_commitments_e1: Vec<PolyComm<E1>>,
    pub previous_commitments_e2: Vec<PolyComm<E2>>,
    pub idx_var: usize,
    pub idx_var_next_row: usize,
    pub idx_var_pi: usize,
    pub current_row: usize,
    pub state: [BigInt; 15],
    pub next_state: [BigInt; 15],
    pub public_state: [BigInt; 17],
    pub selectors: Vec<Vec<bool>>,
    pub challenges: Vec<BigInt>,
    pub current_instruction: Instruction,
    pub sponge_e1: [BigInt; 3],
    pub sponge_e2: [BigInt; 3],
    pub current_iteration: u64,
    pub previous_hash: [u128; 2],
    pub r: BigInt,
    pub temporary_accumulators: ((BigInt, BigInt), (BigInt, BigInt)),
    pub idx_values_to_absorb: usize,
    pub witness: Vec<Vec<BigInt>>,
    pub z0: BigInt,
    pub zi: BigInt,
    pub _marker: PhantomData<(Fp, Fq, E1, E2)>,
}

An environment that can be shared between IVC instances.

It contains all the accumulators that can be picked for a given fold instance k, including the sponges.

The environment is run over big integers to avoid performing reduction at all step. Instead the user implementing the interpreter can reduce in the corresponding field when they want.

Fields

domain_fp: EvaluationDomains<Fp>

Domain for Fp

domain_fq: EvaluationDomains<Fq>

Domain for Fq

srs_e1: SRS<E1>

SRS for the first curve

srs_e2: SRS<E2>

SRS for the second curve

ivc_accumulator_e1: Vec<PolyComm<E1>>

ivc_accumulator_e2: Vec<PolyComm<E2>>

previous_commitments_e1: Vec<PolyComm<E1>>

Commitments to the previous instances

previous_commitments_e2: Vec<PolyComm<E2>>

idx_var: usize

The index of the latest allocated variable in the circuit. It is used to allocate new variables without having to keep track of the position.

idx_var_next_row: usize

idx_var_pi: usize

The index of the latest allocated public inputs in the circuit. It is used to allocate new public inputs without having to keep track of the position.

current_row: usize

Current processing row. Used to build the witness.

state: [BigInt; 15]

State of the current row in the execution trace

next_state: [BigInt; 15]

Next row in the execution trace. It is useful when we deal with polynomials accessing “the next row”, i.e. witness columns where we do evaluate at ζ and ζω.

public_state: [BigInt; 17]

Contain the public state

selectors: Vec<Vec<bool>>

Selectors to activate the gadgets. The size of the outer vector must be equal to the number of gadgets in the circuit. The size of the inner vector must be equal to the number of rows in the circuit.

The layout columns/rows is used to avoid rebuilding the arrays per column when committing to the witness.

challenges: Vec<BigInt>

While folding, we must keep track of the challenges the verifier would have sent in the SNARK, and we must aggregate them.

current_instruction: Instruction

Keep the current executed instruction This can be used to identify which gadget the interpreter is currently building.

sponge_e1: [BigInt; 3]

The sponges will be used to simulate the verifier messages, and will also be used to verify the consistency of the computation by hashing the public IO.

sponge_e2: [BigInt; 3]

current_iteration: u64

The current iteration of the IVC

previous_hash: [u128; 2]

A previous hash, encoded in 2 chunks of 128 bits.

r: BigInt

The coin folding combiner will be used to generate the combinaison of folding instances

temporary_accumulators: ((BigInt, BigInt), (BigInt, BigInt))

Temporary registers for elliptic curve points in affine coordinates than can be used to save values between instructions.

These temporary registers can be loaded into the state by using the function load_temporary_accumulators.

The registers can, and must, be cleaned after the gadget is computed.

The values are considered as BigInt, even though we should add some type. As we want to apply the KISS method, we tend to avoid adding types. We leave this for future work.

Two registers are provided, represented by a tuple for the coordinates (x, y).

idx_values_to_absorb: usize

Index of the values to absorb in the sponge

witness: Vec<Vec<BigInt>>

The witness of the current instance of the circuit. The size of the outer vector must be equal to the number of columns in the circuit. The size of the inner vector must be equal to the number of rows in the circuit.

The layout columns/rows is used to avoid rebuilding the witness per column when committing to the witness.

z0: BigInt

Initial input

zi: BigInt

Current input

_marker: PhantomData<(Fp, Fq, E1, E2)>

Implementations

impl<Fp: PrimeField, Fq: PrimeField, E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>, E2: ArrabbiataCurve<ScalarField = Fq, BaseField = Fp>> Env<Fp, Fq, E1, E2>

pub fn new( srs_log2_size: usize, z0: BigInt, sponge_e1: [BigInt; 3], sponge_e2: [BigInt; 3] ) -> Self

pub fn reset_for_next_iteration(&mut self)

Reset the environment to build the next iteration

pub fn accumulate_commitment_blinder(&mut self)

The blinder used to commit, to avoid committing to the zero polynomial and accumulate it in the IVC.

It is part of the instance, and it is accumulated in the IVC.

pub fn compute_and_update_previous_commitments(&mut self)

Compute the commitments to the current witness, and update the previous instances.

pub fn compute_output(&mut self)

Compute the output of the application on the previous output

pub fn fetch_instruction(&self) -> Instruction

pub fn fetch_next_instruction(&mut self) -> Instruction

Describe the control-flow for the IVC circuit.

For a step i + 1, the IVC circuit receives as public input the following values:

• The commitments to the previous witnesses.
• The previous challenges (α_{i}, β_{i}, γ_{i}) - the challenges β and γ are used by the permutation argument where α is used by the quotient polynomial, generated after also absorbing the accumulator of the permutation argument.
• The previous accumulators (acc_1, …, acc_17).
• The previous output z_i.
• The initial input z_0.
• The natural i describing the previous step.

The control flow is as follow:

• We compute the hash of the previous commitments and verify the hash corresponds to the public input:

hash = H(i, acc_1, ..., acc_17, z_0, z_i)

• We also have to check that the previous challenges (α, β, γ) have been correctly generated. Therefore, we must compute the hashes of the witnesses and verify they correspond to the public input.

TODO

• We compute the output of the application (TODO)

z_(i + 1) = F(w_i, z_i)

• We decompose the scalar r, the random combiner, into bits to compute the MSM for the next step.

• We compute the MSM (verifier)

acc_(i + 1)_j = acc_i + r C_j

And also the cross-terms:

E = E1 - r T1 - r^2 T2 - ... - r^d T^d + r^(d+1) E2
  = E1 - r (T1 + r (T2 + ... + r T^(d - 1)) - r E2)

where (d + 1) is the degree of the highest gate.

• We compute the next hash we give to the next instance

hash' = H(i + 1, acc'_1, ..., acc'_17, z_0, z_(i + 1))

Trait Implementations

impl<Fp: PrimeField, Fq: PrimeField, E1: ArrabbiataCurve<ScalarField = Fp, BaseField = Fq>, E2: ArrabbiataCurve<ScalarField = Fq, BaseField = Fp>> InterpreterEnv for Env<Fp, Fq, E1, E2>where <E1::Params as CurveConfig>::BaseField: PrimeField, <E2::Params as CurveConfig>::BaseField: PrimeField,

type Variable = BigInt

For efficiency, and for having a single interpreter, we do not use one of the fields. We use a generic BigInt to represent the values. When building the witness, we will reduce into the corresponding field.

fn activate_gadget(&mut self, gadget: Gadget)

Activate the gadget for the current row

unsafe fn bitmask_be( &mut self, x: &Self::Variable, highest_bit: u32, lowest_bit: u32, pos: Self::Position ) -> Self::Variable

Flagged as unsafe as it does require an additional range check

fn reset(&mut self)

Reset the environment to build the next row

fn coin_folding_combiner(&mut self, pos: Self::Position) -> Self::Variable

FIXME: check if we need to pick the left or right sponge

unsafe fn inverse( &mut self, pos: Self::Position, x: Self::Variable ) -> Self::Variable

Inverse of a variable

Safety

Zero is not allowed as an input.

fn double_ec_point( &mut self, pos_x: Self::Position, pos_y: Self::Position, x1: Self::Variable, y1: Self::Variable ) -> (Self::Variable, Self::Variable)

Double the elliptic curve point given by the affine coordinates (x1, y1) and save the result in the registers pos_x and pos_y.

type Position = (Column, CurrOrNext)

fn allocate(&mut self) -> Self::Position

Allocate a new variable in the circuit for the current row

fn allocate_next_row(&mut self) -> Self::Position

Allocate a new variable in the circuit for the next row

fn read_position(&self, pos: Self::Position) -> Self::Variable

Return the corresponding variable at the given position

fn allocate_public_input(&mut self) -> Self::Position

fn write_column( &mut self, pos: Self::Position, v: Self::Variable ) -> Self::Variable

Set the value of the variable at the given position for the current row

fn write_public_input( &mut self, pos: Self::Position, v: BigInt ) -> Self::Variable

Write the corresponding public inputs.

fn constrain_boolean(&mut self, x: Self::Variable)

fn constant(&self, v: BigInt) -> Self::Variable

fn add_constraint(&mut self, _x: Self::Variable)

fn assert_zero(&mut self, var: Self::Variable)

Assert that the variable is zero

fn assert_equal(&mut self, x: Self::Variable, y: Self::Variable)

Assert that the two variables are equal

fn square(&mut self, pos: Self::Position, x: Self::Variable) -> Self::Variable

Compute the square a field element

fn fetch_input(&mut self, pos: Self::Position) -> Self::Variable

Fetch an input of the application

fn load_poseidon_state( &mut self, pos: Self::Position, i: usize ) -> Self::Variable

Load the state of the Poseidon hash function into the environment

fn get_poseidon_round_constant( &mut self, pos: Self::Position, round: usize, i: usize ) -> Self::Variable

fn get_poseidon_mds_matrix(&mut self, i: usize, j: usize) -> Self::Variable

Return the requested MDS matrix coefficient

unsafe fn save_poseidon_state(&mut self, x: Self::Variable, i: usize)

Save the state of poseidon into the environment

unsafe fn fetch_value_to_absorb( &mut self, pos: Self::Position, curr_round: usize ) -> Self::Variable

Load the public value to absorb at the current step. The position should be a public column.

unsafe fn load_temporary_accumulators( &mut self, pos_x: Self::Position, pos_y: Self::Position, side: Side ) -> (Self::Variable, Self::Variable)

Load the affine coordinates of the elliptic curve point currently saved in the temporary accumulators. Temporary accumulators could be seen as a CPU cache, an intermediate storage between the RAM (random access memory) and the CPU registers (memory cells that are constrained).

unsafe fn save_temporary_accumulators( &mut self, x: Self::Variable, y: Self::Variable, side: Side )

Save temporary accumulators into the environment

unsafe fn is_same_ec_point( &mut self, pos: Self::Position, x1: Self::Variable, y1: Self::Variable, x2: Self::Variable, y2: Self::Variable ) -> Self::Variable

Check if the points given by (x1, y1) and (x2, y2) are equals.

fn zero(&self) -> Self::Variable

Build the constant zero

fn one(&self) -> Self::Variable

Build the constant one

fn compute_lambda( &mut self, pos: Self::Position, is_same_point: Self::Variable, x1: Self::Variable, y1: Self::Variable, x2: Self::Variable, y2: Self::Variable ) -> Self::Variable

Compute the coefficient λ used in the elliptic curve addition. If the two points are the same, the λ is computed as follows:

fn compute_x5(&self, x: Self::Variable) -> Self::Variable

Compute the x^5 of the given variable