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,
    <<E1 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,
    <<E2 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField,{

    pub indexed_relation: IndexedRelation<Fp, Fq, E1, E2>,
    pub program_e1: Program<Fp, Fq, E1>,
    pub program_e2: Program<Fq, Fp, 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 challenges: 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.

program_e1: Program<Fp, Fq, E1>

Program state for curve E1

program_e2: Program<Fq, Fp, E2>

Program state for curve 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 ζω.

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.

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, 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 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, <<E1 as CommitmentCurve>::Params as CurveConfig>::BaseField: PrimeField, <<E2 as CommitmentCurve>::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.

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 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 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(&self, round: usize, i: usize) -> Self::Variable

Return the Poseidon round constants as a constant.

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 ) -> Self::Variable

Load the value to absorb at the current step at the position given by pos.

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