Struct arrabbiata::witness::Env
source · 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,{Show 24 fields
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,
}
Expand description
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§
source§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,
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
sourcepub fn reset_for_next_iteration(&mut self)
pub fn reset_for_next_iteration(&mut self)
Reset the environment to build the next iteration
sourcepub fn accumulate_commitment_blinder(&mut self)
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.
sourcepub fn commit_state(&mut self)
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.
sourcepub fn absorb_state(&mut self)
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.
sourcepub fn compute_output(&mut self)
pub fn compute_output(&mut self)
Compute the output of the application on the previous output
pub fn fetch_instruction(&self) -> Instruction
sourcepub fn coin_challenge(&mut self, chal: ChallengeTerm)
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.
sourcepub fn accumulate_program_state(&mut self)
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.
sourcepub fn accumulate_committed_state(&mut self)
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§
source§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,
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
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.
source§unsafe fn bitmask_be(
&mut self,
x: &Self::Variable,
highest_bit: u32,
lowest_bit: u32,
pos: Self::Position
) -> Self::Variable
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
source§fn coin_folding_combiner(&mut self, pos: Self::Position) -> Self::Variable
fn coin_folding_combiner(&mut self, pos: Self::Position) -> Self::Variable
FIXME: check if we need to pick the left or right sponge
source§fn double_ec_point(
&mut self,
pos_x: Self::Position,
pos_y: Self::Position,
x1: Self::Variable,
y1: Self::Variable
) -> (Self::Variable, Self::Variable)
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)
source§fn allocate(&mut self) -> Self::Position
fn allocate(&mut self) -> Self::Position
source§fn allocate_next_row(&mut self) -> Self::Position
fn allocate_next_row(&mut self) -> Self::Position
source§fn read_position(&self, pos: Self::Position) -> Self::Variable
fn read_position(&self, pos: Self::Position) -> Self::Variable
source§fn write_column(
&mut self,
pos: Self::Position,
v: Self::Variable
) -> Self::Variable
fn write_column( &mut self, pos: Self::Position, v: Self::Variable ) -> Self::Variable
fn constrain_boolean(&mut self, x: Self::Variable)
fn constant(&self, v: BigInt) -> Self::Variable
fn add_constraint(&mut self, _x: Self::Variable)
source§fn assert_zero(&mut self, var: Self::Variable)
fn assert_zero(&mut self, var: Self::Variable)
source§fn assert_equal(&mut self, x: Self::Variable, y: Self::Variable)
fn assert_equal(&mut self, x: Self::Variable, y: Self::Variable)
source§fn square(&mut self, pos: Self::Position, x: Self::Variable) -> Self::Variable
fn square(&mut self, pos: Self::Position, x: Self::Variable) -> Self::Variable
source§fn fetch_input(&mut self, pos: Self::Position) -> Self::Variable
fn fetch_input(&mut self, pos: Self::Position) -> Self::Variable
source§fn load_poseidon_state(
&mut self,
pos: Self::Position,
i: usize
) -> Self::Variable
fn load_poseidon_state( &mut self, pos: Self::Position, i: usize ) -> Self::Variable
source§fn get_poseidon_round_constant(&self, round: usize, i: usize) -> Self::Variable
fn get_poseidon_round_constant(&self, round: usize, i: usize) -> Self::Variable
source§fn get_poseidon_mds_matrix(&mut self, i: usize, j: usize) -> Self::Variable
fn get_poseidon_mds_matrix(&mut self, i: usize, j: usize) -> Self::Variable
source§unsafe fn save_poseidon_state(&mut self, x: Self::Variable, i: usize)
unsafe fn save_poseidon_state(&mut self, x: Self::Variable, i: usize)
source§unsafe fn fetch_value_to_absorb(
&mut self,
pos: Self::Position
) -> Self::Variable
unsafe fn fetch_value_to_absorb( &mut self, pos: Self::Position ) -> Self::Variable
pos
. Read more