Struct arrabiata::constraints::Env

pub struct Env<Fp: Field> {
    pub poseidon_mds: Vec<Vec<Fp>>,
    pub a: BigInt,
    pub idx_var: usize,
    pub idx_var_next_row: usize,
    pub idx_var_pi: usize,
    pub constraints: Vec<E<Fp>>,
    pub activated_gadget: Option<Gadget>,
}

Fields

poseidon_mds: Vec<Vec<Fp>>

a: BigInt

The parameter a is the coefficients of the elliptic curve in affine coordinates.

idx_var: usize

idx_var_next_row: usize

idx_var_pi: usize

constraints: Vec<E<Fp>>

activated_gadget: Option<Gadget>

Implementations

impl<Fp: PrimeField> Env<Fp>

pub fn new(poseidon_mds: Vec<Vec<Fp>>, a: BigInt) -> Self

impl<F: PrimeField> Env<F>

pub fn get_all_constraints_for_ivc(&self) -> Vec<E<F>>

Get all the constraints for the IVC circuit, only.

The following gadgets are used in the IVC circuit:

• Instruction::Poseidon to verify the challenges and the public IO
• Instruction::EllipticCurveScaling and Instruction::EllipticCurveAddition to accumulate the commitments

pub fn get_all_constraints(&self) -> Vec<E<F>>

Get all the constraints for the IVC circuit and the application.

Trait Implementations

impl<Fp: Clone + Field> Clone for Env<Fp>

fn clone(&self) -> Env<Fp>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<Fp: Debug + Field> Debug for Env<Fp>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<Fp: PrimeField> InterpreterEnv for Env<Fp>

An environment to build constraints. The constraint environment is mostly useful when we want to perform a Nova proof. The constraint environment must be instantiated only once, at the last step of the computation.

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

Return the corresponding expression regarding the selected public input

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

Return the corresponding expression regarding the selected column

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)

type Variable = Operations<ExprInner<Operations<ConstantExprInner<Fp, ChallengeTerm>>, Column>>

The variable should be seen as a certain object that can be built by multiplying and adding, i.e. the variable can be seen as a solution to a polynomial. When instantiating as expressions - “constraints” - it defines multivariate polynomials.

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 constant(&self, value: BigInt) -> Self::Variable

fn activate_gadget(&mut self, gadget: Gadget)

Activate the gadget for the row.

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

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

fn assert_zero(&mut self, x: 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

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 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 reset(&mut self)

Reset the environment to build the next row

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

Return the folding combiner

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

Load the state of the Poseidon hash function into the environment

unsafe fn save_poseidon_state(&mut self, _x: Self::Variable, _i: usize)

Save the state of poseidon 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 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