Trait arrabiata::interpreter::InterpreterEnv

pub trait InterpreterEnv {
    type Position: Clone + Copy;
    type Variable: Clone + Add<Self::Variable, Output = Self::Variable> + Sub<Self::Variable, Output = Self::Variable> + Mul<Self::Variable, Output = Self::Variable> + Debug + Zero + One;

    // Required methods
    fn allocate(&mut self) -> Self::Position;
    fn allocate_next_row(&mut self) -> Self::Position;
    fn read_position(&self, pos: Self::Position) -> Self::Variable;
    fn allocate_public_input(&mut self) -> Self::Position;
    fn write_column(
        &mut self,
        col: Self::Position,
        v: Self::Variable
    ) -> Self::Variable;
    fn write_public_input(
        &mut self,
        x: Self::Position,
        v: BigInt
    ) -> Self::Variable;
    fn activate_gadget(&mut self, gadget: Gadget);
    fn zero(&self) -> Self::Variable;
    fn one(&self) -> Self::Variable;
    fn constant(&self, v: BigInt) -> Self::Variable;
    fn assert_zero(&mut self, x: Self::Variable);
    fn assert_equal(&mut self, x: Self::Variable, y: Self::Variable);
    fn add_constraint(&mut self, x: Self::Variable);
    fn constrain_boolean(&mut self, x: Self::Variable);
    fn square(
        &mut self,
        res: Self::Position,
        x: Self::Variable
    ) -> Self::Variable;
    unsafe fn bitmask_be(
        &mut self,
        x: &Self::Variable,
        highest_bit: u32,
        lowest_bit: u32,
        position: Self::Position
    ) -> Self::Variable;
    fn fetch_input(&mut self, res: Self::Position) -> Self::Variable;
    fn reset(&mut self);
    fn coin_folding_combiner(&mut self, pos: Self::Position) -> Self::Variable;
    fn load_poseidon_state(
        &mut self,
        pos: Self::Position,
        i: usize
    ) -> Self::Variable;
    unsafe fn save_poseidon_state(&mut self, v: Self::Variable, i: usize);
    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;
    unsafe fn fetch_value_to_absorb(
        &mut self,
        pos: Self::Position,
        curr_round: usize
    ) -> Self::Variable;
    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;
    unsafe fn inverse(
        &mut self,
        pos: Self::Position,
        x: Self::Variable
    ) -> Self::Variable;
    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;
    fn double_ec_point(
        &mut self,
        pos_x: Self::Position,
        pos_y: Self::Position,
        x1: Self::Variable,
        y1: Self::Variable
    ) -> (Self::Variable, Self::Variable);
    unsafe fn load_temporary_accumulators(
        &mut self,
        pos_x: Self::Position,
        pos_y: Self::Position,
        side: Side
    ) -> (Self::Variable, Self::Variable);
    unsafe fn save_temporary_accumulators(
        &mut self,
        _v1: Self::Variable,
        _v2: Self::Variable,
        _side: Side
    );

    // Provided method
    fn compute_x5(&self, x: Self::Variable) -> Self::Variable { ... }
}

An abstract interpreter that provides some functionality on the circuit. The interpreter should be seen as a state machine with some built-in functionality whose state is a matrix, and whose transitions are described by polynomial functions.

Required Associated Types

type Position: Clone + Copy

type Variable: Clone + Add<Self::Variable, Output = Self::Variable> + Sub<Self::Variable, Output = Self::Variable> + Mul<Self::Variable, Output = Self::Variable> + Debug + Zero + One

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.

Required Methods

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, col: 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, x: Self::Position, v: BigInt) -> Self::Variable

Write the corresponding public inputs.

fn activate_gadget(&mut self, gadget: Gadget)

Activate the gadget for the row.

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

Build the constant zero

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

Build the constant one

fn constant(&self, v: BigInt) -> 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

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

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

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

Compute the square a field element

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

Flagged as unsafe as it does require an additional range check

Safety

There are no constraints on the returned value; callers must assert the relationship with the source variable x and that the returned value fits in highest_bit - lowest_bit bits.

fn fetch_input(&mut self, res: 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, v: Self::Variable, i: usize)

Save the state of poseidon into the environment

Safety

It does not have any effect on the constraints

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.

IMPROVEME: we could have in the environment an heterogeneous typed list, and we pop values call after call. However, we try to keep the interpreter simple.

Safety

No constraint is added. It should be used with caution.

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.

Safety

No constraint is added. It should be used with caution.

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. Witness only

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:

• λ = (3 X1^2 + a) / (2Y1) Otherwise, the λ is computed as follows:
• λ = (Y1 - Y2) / (X1 - X2)

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. The last argument, row, is used to decide if the result should be written in the current or the next row of the variable position pos_x and pos_y.

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

For now, it can only be used to load affine coordinates of elliptic curve points given in the short Weierstrass form.

Temporary accumulators could also be seen as return values of a function.

Safety

No constraints are enforced. It is not also enforced that the accumulators have been cleaned between two different gadgets.

unsafe fn save_temporary_accumulators( &mut self, _v1: Self::Variable, _v2: Self::Variable, _side: Side )

Save temporary accumulators into the environment

Safety

It does not have any effect on the constraints.

Provided Methods

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

Compute the x^5 of the given variable

Implementors

impl<Fp: PrimeField> InterpreterEnv for arrabiata::constraints::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.

type Position = (Column, CurrOrNext)

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

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

type Position = (Column, CurrOrNext)

type Variable = BigInt