Struct arrabbiata::witness::Env

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

    pub indexed_relation: IndexedRelation<Fp, Fq, E1, E2>,
    pub accumulated_committed_state_e1: Vec<PolyComm<E1>>,
    pub accumulated_committed_state_e2: Vec<PolyComm<E2>>,
    pub previous_committed_state_e1: Vec<PolyComm<E1>>,
    pub previous_committed_state_e2: Vec<PolyComm<E2>>,
    pub accumulated_program_state_e1: Vec<Vec<E1::ScalarField>>,
    pub accumulated_program_state_e2: Vec<Vec<E2::ScalarField>>,
    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: Challenges<BigInt>,
    pub accumulated_challenges_e1: Challenges<BigInt>,
    pub accumulated_challenges_e2: Challenges<BigInt>,
    pub previous_challenges_e1: Challenges<BigInt>,
    pub previous_challenges_e2: Challenges<BigInt>,
    pub current_instruction: Instruction,
    pub sponge_e1: [BigInt; 3],
    pub sponge_e2: [BigInt; 3],
    pub prover_sponge_state: [BigInt; 3],
    pub verifier_sponge_state: [BigInt; 3],
    pub current_iteration: u64,
    pub last_program_digest_before_execution: BigInt,
    pub last_program_digest_after_execution: BigInt,
    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,
}

An environment is used to contain the state of a long “running program”.

The running program is composed of two parts: one user application and one verifier application. The verifier application is used to encode the correctness of previous program states computations.

The term “app(lication) state” will be used to refer to the state of the user application, and the term “IVC state” will be used to refer to the state of the verifier application. The term program state will be used to refer to the state of the whole program.

The environment 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.

The environment is generic over two curves (called E1 and E2) that are supposed to form a cycle.

Fields

indexed_relation: IndexedRelation<Fp, Fq, E1, E2>

The relation this witness environment is related to.

accumulated_committed_state_e1: Vec<PolyComm<E1>>

accumulated_committed_state_e2: Vec<PolyComm<E2>>

previous_committed_state_e1: Vec<PolyComm<E1>>

Commitments to the previous program states.

previous_committed_state_e2: Vec<PolyComm<E2>>

accumulated_program_state_e1: Vec<Vec<E1::ScalarField>>

Accumulated witness for the program state over E1 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.

accumulated_program_state_e2: Vec<Vec<E2::ScalarField>>

Accumulated witness for the program state over E2 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.

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: Challenges<BigInt>

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

accumulated_challenges_e1: Challenges<BigInt>

List of the accumulated challenges over time, over the curve E1.

accumulated_challenges_e2: Challenges<BigInt>

List of the accumulated challenges over time, over the curve E2.

previous_challenges_e1: Challenges<BigInt>

Challenges coined over E1 during the last computation. This field is useful to keep track of the challenges that must be verified in circuit.

previous_challenges_e2: Challenges<BigInt>

Challenges coined over E2 during the last computation. This field is useful to keep track of the challenges that must be verified in circuit.

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]

prover_sponge_state: [BigInt; 3]

Sponge state used by the prover for the current iteration.

This sponge is used at the current iteration to absorb commitments of the program state and generate the challenges for the current iteration. The outputs of the sponge will be verified by the verifier of the next iteration.

verifier_sponge_state: [BigInt; 3]

Sponge state used by the verifier for the current iteration.

This sponge is used at the current iteration to build the verifier circuit. The state will need to match with the previous prover sopnge state.

current_iteration: u64

The current iteration of the IVC.

last_program_digest_before_execution: BigInt

The digest of the program state before executing the last iteration. The value will be used to initialize the execution trace of the verifier in the next iteration, in particular to verify that the challenges have been generated correctly.

The value is a 128bits value.

last_program_digest_after_execution: BigInt

The digest of the program state after executing the last iteration. The value will be used to initialize the sponge before committing to the next iteration.

The value is a 128bits value.

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

Implementations

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

pub fn new( z0: BigInt, sponge_e1: [BigInt; 3], sponge_e2: [BigInt; 3], indexed_relation: IndexedRelation<Fp, Fq, E1, E2> ) -> 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 accumulated in the IVC.

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

pub fn commit_state(&mut self)

Commit to the program state and updating the environment with the result.

This method is supposed to be called after a new iteration of the program has been executed.

pub fn absorb_state(&mut self)

Absorb the last committed program state in the correct sponge.

For a description of the messages to be given to the sponge, including the expected instantiation, refer to the section “Message Passing” in crate::interpreter.

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 verifier 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 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))

pub fn coin_challenge(&mut self, chal: ChallengeTerm)

Simulate an interaction with the verifier by requesting to coin a challenge from the current prover sponge state.

This method supposes that all the messages have been sent to the verifier previously, and the attribute [self.prover_sponge_state] has been updated accordingly by absorbing all the messages correctly.

The side-effect of this method will be to run a permutation on the sponge state after coining the challenge. There is an hypothesis on the sponge state that the inner permutation has been correctly executed if the absorbtion rate had been reached at the last absorbtion.

The challenge will be added to the [self.challenges] attribute at the position given by the challenge chal.

Internally, the method is implemented by simply loading the prover sponge state, and squeezing a challenge from it, relying on the implementation of the sponge. Usually, the challenge would be the first N bits of the first element, but it is left as an implementation detail of the sponge given by the curve.

pub fn accumulate_program_state(&mut self)

Accumulate the program state (or in other words, the witness), by adding the last computed program state into the program state accumulator.

This method is supposed to be called after the program state has been committed (by calling [self.commit_state]) and absorbed (by calling [self.absorb_state]). The “relation randomiser” must also have been coined and saved in the environment before, by calling [self.coin_challenge].

The program state is accumulated into a different accumulator, depending on the curve currently being used.

This is part of the work the prover of the accumulation/folding scheme.

This must translate the following equation:

acc_(p, n + 1) = acc_(p, n) * chal w
              OR
acc_(q, n + 1) = acc_(q, n) * chal w

where acc and w are vectors of the same size.

pub fn accumulate_committed_state(&mut self)

Accumulate the committed state by adding the last committed state into the committed state accumulator.

The commitments are accumulated into a different accumulator, depending on the curve currently being used.

This is part of the work the prover of the accumulation/folding scheme.

This must translate the following equation:

C_(p, n + 1) = C_(p, n) + chal * comm
              OR
C_(q, n + 1) = C_(q, n) + chal * comm

Note that the committed program state is encoded in crate::NUMBER_OF_COLUMNS values, therefore we must iterate over all the columns to accumulate the committed state.

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::BaseField: PrimeField, E2::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