Struct o1vm::interpreters::riscv32i::constraints::Env

pub struct Env<F: Field> {
    pub scratch_state_idx: usize,
    pub lookups: Vec<RAMLookup<E<F>, LookupTableIDs>>,
    pub constraints: Vec<E<F>>,
    pub selector: Option<E<F>>,
}

Fields

scratch_state_idx: usize

lookups: Vec<RAMLookup<E<F>, LookupTableIDs>>

constraints: Vec<E<F>>

selector: Option<E<F>>

Implementations

impl<Fp: Field> Env<Fp>

pub fn get_selector_constraints(&self) -> Vec<E<Fp>>

Return the constraints for the selector. Each selector must be a boolean.

pub fn get_selector(&self) -> E<Fp>

pub fn get_constraints(&self) -> Vec<E<Fp>>

Return the constraints for the current instruction, without the selector

pub fn get_lookups(&self) -> Vec<RAMLookup<E<Fp>, LookupTableIDs>>

Trait Implementations

impl<Fp: Field> Default for Env<Fp>

fn default() -> Self

Returns the “default value” for a type.

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

type Position = Column

In the concrete implementation for the constraints, the interpreter will work over columns. The position in this case can be seen as a new variable/input of our circuit.

fn alloc_scratch(&mut self) -> Self::Position

Allocate a new abstract variable for the current step. The variable can be used to store temporary values. The variables are “freed” after each step/instruction. The variable allocation can be seen as an allocation on a stack that is popped after each step execution. At the moment, crate::interpreters::riscv32i::SCRATCH_SIZE elements can be allocated. If more temporary variables are required for an instruction, increase the value crate::interpreters::riscv32i::SCRATCH_SIZE

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

fn variable(&self, column: Self::Position) -> Self::Variable

fn activate_selector(&mut self, selector: Instruction)

Activate the selector for the given instruction.

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

Add a constraint to the proof system, asserting that assert_equals_zero is 0.

fn check_is_zero(_assert_equals_zero: &Self::Variable)

Check that the witness value in assert_equals_zero is 0; otherwise abort.

fn check_equal(_x: &Self::Variable, _y: &Self::Variable)

Check that the witness values in x and y are equal; otherwise abort.

fn check_boolean(_x: &Self::Variable)

Check that the witness value x is a boolean (0 or 1); otherwise abort.

fn add_lookup(&mut self, lookup: RAMLookup<Self::Variable, LookupTableIDs>)

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

fn increase_instruction_counter(&mut self)

unsafe fn fetch_register( &mut self, _idx: &Self::Variable, output: Self::Position ) -> Self::Variable

Fetch the value of the general purpose register with index idx and store it in local position output.

unsafe fn push_register_if( &mut self, _idx: &Self::Variable, _value: Self::Variable, _if_is_true: &Self::Variable )

Set the general purpose register with index idx to value if if_is_true is true.

unsafe fn fetch_register_access( &mut self, _idx: &Self::Variable, output: Self::Position ) -> Self::Variable

Fetch the last ‘access index’ for the general purpose register with index idx, and store it in local position output.

unsafe fn push_register_access_if( &mut self, _idx: &Self::Variable, _value: Self::Variable, _if_is_true: &Self::Variable )

Set the last ‘access index’ for the general purpose register with index idx to value if if_is_true is true.

unsafe fn fetch_memory( &mut self, _addr: &Self::Variable, output: Self::Position ) -> Self::Variable

Fetch the memory value at address addr and store it in local position output.

unsafe fn push_memory(&mut self, _addr: &Self::Variable, _value: Self::Variable)

Set the memory value at address addr to value.

unsafe fn fetch_memory_access( &mut self, _addr: &Self::Variable, output: Self::Position ) -> Self::Variable

Fetch the last ‘access index’ that the memory at address addr was written at, and store it in local position output.

unsafe fn push_memory_access( &mut self, _addr: &Self::Variable, _value: Self::Variable )

Set the last ‘access index’ for the memory at address addr to value.

fn constant(x: u32) -> Self::Variable

unsafe fn bitmask( &mut self, _x: &Self::Variable, _highest_bit: u32, _lowest_bit: u32, position: Self::Position ) -> Self::Variable

Extract the bits from the variable x between highest_bit and lowest_bit, and store the result in position. lowest_bit becomes the least-significant bit of the resulting value.

unsafe fn shift_left( &mut self, _x: &Self::Variable, _by: &Self::Variable, position: Self::Position ) -> Self::Variable

Return the result of shifting x by by, storing the result in position.

unsafe fn shift_right( &mut self, _x: &Self::Variable, _by: &Self::Variable, position: Self::Position ) -> Self::Variable

Return the result of shifting x by by, storing the result in position.

unsafe fn shift_right_arithmetic( &mut self, _x: &Self::Variable, _by: &Self::Variable, position: Self::Position ) -> Self::Variable

Return the result of shifting x by by, storing the result in position.

unsafe fn test_zero( &mut self, _x: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns 1 if x is 0, or 0 otherwise, storing the result in position.

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

unsafe fn inverse_or_zero( &mut self, _x: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns x^(-1), or 0 if x is 0, storing the result in position.

fn equal(&mut self, x: &Self::Variable, y: &Self::Variable) -> Self::Variable

Returns 1 if x is equal to y, or 0 otherwise, storing the result in position.

unsafe fn test_less_than( &mut self, _x: &Self::Variable, _y: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns 1 if x < y as unsigned integers, or 0 otherwise, storing the result in position.

unsafe fn test_less_than_signed( &mut self, _x: &Self::Variable, _y: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns 1 if x < y as signed integers, or 0 otherwise, storing the result in position.

unsafe fn and_witness( &mut self, _x: &Self::Variable, _y: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns x or y, storing the result in position.

unsafe fn nor_witness( &mut self, _x: &Self::Variable, _y: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns x nor y, storing the result in position.

unsafe fn or_witness( &mut self, _x: &Self::Variable, _y: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns x or y, storing the result in position.

unsafe fn xor_witness( &mut self, _x: &Self::Variable, _y: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns x xor y, storing the result in position.

unsafe fn add_witness( &mut self, _y: &Self::Variable, _x: &Self::Variable, out_position: Self::Position, overflow_position: Self::Position ) -> (Self::Variable, Self::Variable)

Returns x + y and the overflow bit, storing the results in position_out and position_overflow respectively.

unsafe fn sub_witness( &mut self, _y: &Self::Variable, _x: &Self::Variable, out_position: Self::Position, underflow_position: Self::Position ) -> (Self::Variable, Self::Variable)

Returns x + y and the underflow bit, storing the results in position_out and position_underflow respectively.

unsafe fn mul_signed_witness( &mut self, _x: &Self::Variable, _y: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns x * y, where x and y are treated as integers, storing the result in position.

unsafe fn mul_hi_lo_signed( &mut self, _x: &Self::Variable, _y: &Self::Variable, position_hi: Self::Position, position_lo: Self::Position ) -> (Self::Variable, Self::Variable)

Returns ((x * y) >> 32, (x * y) & ((1 << 32) - 1)), storing the results in position_hi and position_lo respectively.

unsafe fn mul_hi_lo( &mut self, _x: &Self::Variable, _y: &Self::Variable, position_hi: Self::Position, position_lo: Self::Position ) -> (Self::Variable, Self::Variable)

Returns ((x * y) >> 32, (x * y) & ((1 << 32) - 1)), storing the results in position_hi and position_lo respectively.

unsafe fn divmod_signed( &mut self, _x: &Self::Variable, _y: &Self::Variable, position_quotient: Self::Position, position_remainder: Self::Position ) -> (Self::Variable, Self::Variable)

Returns (x / y, x % y), storing the results in position_quotient and position_remainder respectively.

unsafe fn divmod( &mut self, _x: &Self::Variable, _y: &Self::Variable, position_quotient: Self::Position, position_remainder: Self::Position ) -> (Self::Variable, Self::Variable)

Returns (x / y, x % y), storing the results in position_quotient and position_remainder respectively.

unsafe fn count_leading_zeros( &mut self, _x: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns the number of leading 0s in x, storing the result in position.

unsafe fn count_leading_ones( &mut self, _x: &Self::Variable, position: Self::Position ) -> Self::Variable

Returns the number of leading 1s in x, storing the result in position.

fn copy( &mut self, x: &Self::Variable, position: Self::Position ) -> Self::Variable

fn set_halted(&mut self, _flag: Self::Variable)

fn report_exit(&mut self, _exit_code: &Self::Variable)

fn reset(&mut self)

fn assert_is_zero(&mut self, assert_equals_zero: Self::Variable)

Assert that the value assert_equals_zero is 0, and add a constraint in the proof system.

fn assert_equal(&mut self, x: Self::Variable, y: Self::Variable)

Assert that the values x and y are equal, and add a constraint in the proof system.

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

Assert that the value x is boolean, and add a constraint in the proof system.

unsafe fn push_register(&mut self, idx: &Self::Variable, value: Self::Variable)

Set the general purpose register with index idx to value.

unsafe fn push_register_access( &mut self, idx: &Self::Variable, value: Self::Variable )

Set the last ‘access index’ for the general purpose register with index idx to value.

unsafe fn access_register_if( &mut self, idx: &Self::Variable, old_value: &Self::Variable, new_value: &Self::Variable, if_is_true: &Self::Variable )

Access the general purpose register with index idx, adding constraints asserting that the old value was old_value and that the new value will be new_value, if if_is_true is true.

fn read_register(&mut self, idx: &Self::Variable) -> Self::Variable

unsafe fn access_register( &mut self, idx: &Self::Variable, old_value: &Self::Variable, new_value: &Self::Variable )

Access the general purpose register with index idx, adding constraints asserting that the old value was old_value and that the new value will be new_value.

fn write_register_if( &mut self, idx: &Self::Variable, new_value: Self::Variable, if_is_true: &Self::Variable )

fn write_register(&mut self, idx: &Self::Variable, new_value: Self::Variable)

unsafe fn access_memory( &mut self, addr: &Self::Variable, old_value: &Self::Variable, new_value: &Self::Variable )

Access the memory address addr, adding constraints asserting that the old value was old_value and that the new value will be new_value.

fn read_memory(&mut self, addr: &Self::Variable) -> Self::Variable

fn write_memory(&mut self, addr: &Self::Variable, new_value: Self::Variable)

fn lookup_16bits(&mut self, value: &Self::Variable)

Adds a lookup to the RangeCheck16Lookup table

fn range_check16(&mut self, value: &Self::Variable, bits: u32)

Range checks with 2 lookups to the RangeCheck16Lookup table that a value is at most 2^bits-1 (bits <= 16).

fn lookup_8bits(&mut self, value: &Self::Variable)

Adds a lookup to the ByteLookup table

fn range_check8(&mut self, value: &Self::Variable, bits: u32)

Range checks with 2 lookups to the ByteLookup table that a value is at most 2^bits-1 (bits <= 8).

fn lookup_2bits(&mut self, value: &Self::Variable)

Adds a lookup to the AtMost4Lookup table

fn range_check64(&mut self, _value: &Self::Variable)

fn set_instruction_pointer(&mut self, ip: Self::Variable)

fn get_instruction_pointer(&mut self) -> Self::Variable

fn set_next_instruction_pointer(&mut self, ip: Self::Variable)

fn get_next_instruction_pointer(&mut self) -> Self::Variable

fn increase_heap_pointer( &mut self, by_amount: &Self::Variable, if_is_true: &Self::Variable ) -> Self::Variable

Increases the heap pointer by by_amount if if_is_true is 1, and returns the previous value of the heap pointer.

fn sign_extend(&mut self, x: &Self::Variable, bitlength: u32) -> Self::Variable

Given a variable x, this function extends it to a signed integer of bitlength bits.