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

Show 74 methods // Required methods fn alloc_scratch(&mut self) -> Self::Position; fn variable(&self, column: Self::Position) -> Self::Variable; fn add_constraint(&mut self, assert_equals_zero: Self::Variable); fn activate_selector(&mut self, selector: Instruction); fn check_is_zero(assert_equals_zero: &Self::Variable); fn check_equal(x: &Self::Variable, y: &Self::Variable); fn check_boolean(x: &Self::Variable); 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; unsafe fn push_register_if( &mut self, idx: &Self::Variable, value: Self::Variable, if_is_true: &Self::Variable ); unsafe fn fetch_register_access( &mut self, idx: &Self::Variable, output: Self::Position ) -> Self::Variable; unsafe fn push_register_access_if( &mut self, idx: &Self::Variable, value: Self::Variable, if_is_true: &Self::Variable ); unsafe fn fetch_memory( &mut self, addr: &Self::Variable, output: Self::Position ) -> Self::Variable; unsafe fn push_memory( &mut self, addr: &Self::Variable, value: Self::Variable ); unsafe fn fetch_memory_access( &mut self, addr: &Self::Variable, output: Self::Position ) -> Self::Variable; unsafe fn push_memory_access( &mut self, addr: &Self::Variable, value: Self::Variable ); 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; unsafe fn shift_left( &mut self, x: &Self::Variable, by: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn shift_right( &mut self, x: &Self::Variable, by: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn shift_right_arithmetic( &mut self, x: &Self::Variable, by: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn test_zero( &mut self, x: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn inverse_or_zero( &mut self, x: &Self::Variable, position: Self::Position ) -> Self::Variable; fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable; fn equal( &mut self, x: &Self::Variable, y: &Self::Variable ) -> Self::Variable; unsafe fn test_less_than( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn test_less_than_signed( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn and_witness( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn or_witness( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn nor_witness( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn xor_witness( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn add_witness( &mut self, y: &Self::Variable, x: &Self::Variable, out_position: Self::Position, overflow_position: Self::Position ) -> (Self::Variable, Self::Variable); unsafe fn sub_witness( &mut self, y: &Self::Variable, x: &Self::Variable, out_position: Self::Position, underflow_position: Self::Position ) -> (Self::Variable, Self::Variable); unsafe fn mul_signed_witness( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position ) -> Self::Variable; 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); 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); unsafe fn divmod_signed( &mut self, x: &Self::Variable, y: &Self::Variable, position_quotient: Self::Position, position_remainder: Self::Position ) -> (Self::Variable, Self::Variable); unsafe fn divmod( &mut self, x: &Self::Variable, y: &Self::Variable, position_quotient: Self::Position, position_remainder: Self::Position ) -> (Self::Variable, Self::Variable); unsafe fn count_leading_zeros( &mut self, x: &Self::Variable, position: Self::Position ) -> Self::Variable; unsafe fn count_leading_ones( &mut self, x: &Self::Variable, position: Self::Position ) -> Self::Variable; 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 request_preimage_write( &mut self, addr: &Self::Variable, len: &Self::Variable, pos: Self::Position ) -> Self::Variable; fn request_hint_write( &mut self, addr: &Self::Variable, len: &Self::Variable ); fn reset(&mut self); // Provided methods fn assert_is_zero(&mut self, assert_equals_zero: Self::Variable) { ... } fn assert_equal(&mut self, x: Self::Variable, y: Self::Variable) { ... } fn assert_boolean(&mut self, x: Self::Variable) { ... } unsafe fn push_register( &mut self, idx: &Self::Variable, value: Self::Variable ) { ... } unsafe fn push_register_access( &mut self, idx: &Self::Variable, value: Self::Variable ) { ... } unsafe fn access_register_if( &mut self, idx: &Self::Variable, old_value: &Self::Variable, new_value: &Self::Variable, if_is_true: &Self::Variable ) { ... } 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 ) { ... } 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 ) { ... } 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) { ... } fn range_check16(&mut self, value: &Self::Variable, bits: u32) { ... } fn lookup_8bits(&mut self, value: &Self::Variable) { ... } fn range_check8(&mut self, value: &Self::Variable, bits: u32) { ... } fn lookup_2bits(&mut self, value: &Self::Variable) { ... } fn range_check2(&mut self, value: &Self::Variable) { ... } 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 { ... } fn sign_extend( &mut self, x: &Self::Variable, bitlength: u32 ) -> Self::Variable { ... }
}

Required Associated Types§

source

type Position

A position can be seen as an indexed variable

source

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§

source

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::mips::witness::SCRATCH_SIZE - 46] elements can be allocated. If more temporary variables are required for an instruction, increase the value crate::interpreters::mips::witness::SCRATCH_SIZE

source

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

source

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

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

source

fn activate_selector(&mut self, selector: Instruction)

Activate the selector for the given instruction.

source

fn check_is_zero(assert_equals_zero: &Self::Variable)

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

source

fn check_equal(x: &Self::Variable, y: &Self::Variable)

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

source

fn check_boolean(x: &Self::Variable)

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

source

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

source

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

source

fn increase_instruction_counter(&mut self)

source

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.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this operation.

source

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.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this operation.

source

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.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this operation.

source

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.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this operation.

source

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.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this memory operation.

source

unsafe fn push_memory(&mut self, addr: &Self::Variable, value: Self::Variable)

Set the memory value at address addr to value.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this memory operation.

source

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.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this memory operation.

source

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.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this memory operation.

source

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

source

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.

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.

Do not call this function with highest_bit - lowest_bit >= 32.

source

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.

Safety

There are no constraints on the returned value; callers must assert the relationship with the source variable x and the shift amount by.

source

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.

Safety

There are no constraints on the returned value; callers must assert the relationship with the source variable x and the shift amount by.

source

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.

Safety

There are no constraints on the returned value; callers must assert the relationship with the source variable x and the shift amount by.

source

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.

Safety

There are no constraints on the returned value; callers must assert the relationship with x.

source

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.

Safety

There are no constraints on the returned value; callers must assert the relationship with x.

The value returned may be a placeholder; callers should be careful not to depend directly on the value stored in the variable.

source

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

source

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.

source

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.

Safety

There are no constraints on the returned value; callers must assert that the value correctly represents the relationship between x and y

source

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.

Safety

There are no constraints on the returned value; callers must assert that the value correctly represents the relationship between x and y

source

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.

Safety

There are no constraints on the returned value; callers must manually add constraints to ensure that it is correctly constructed.

source

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.

Safety

There are no constraints on the returned value; callers must manually add constraints to ensure that it is correctly constructed.

source

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.

Safety

There are no constraints on the returned value; callers must manually add constraints to ensure that it is correctly constructed.

source

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.

Safety

There are no constraints on the returned value; callers must manually add constraints to ensure that it is correctly constructed.

source

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.

Safety

There are no constraints on the returned values; callers must manually add constraints to ensure that they are correctly constructed.

source

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.

Safety

There are no constraints on the returned values; callers must manually add constraints to ensure that they are correctly constructed.

source

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.

Safety

There are no constraints on the returned value; callers must manually add constraints to ensure that it is correctly constructed.

source

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.

Safety

There are no constraints on the returned values; callers must manually add constraints to ensure that the pair of returned values correspond to the given values x and y, and that they fall within the desired range.

source

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.

Safety

There are no constraints on the returned values; callers must manually add constraints to ensure that the pair of returned values correspond to the given values x and y, and that they fall within the desired range.

source

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.

Safety

There are no constraints on the returned values; callers must manually add constraints to ensure that the pair of returned values correspond to the given values x and y, and that they fall within the desired range.

source

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.

Safety

There are no constraints on the returned values; callers must manually add constraints to ensure that the pair of returned values correspond to the given values x and y, and that they fall within the desired range.

source

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.

Safety

There are no constraints on the returned value; callers must manually add constraints to ensure that it is correctly constructed.

source

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.

Safety

There are no constraints on the returned value; callers must manually add constraints to ensure that it is correctly constructed.

source

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

source

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

source

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

source

fn request_preimage_write( &mut self, addr: &Self::Variable, len: &Self::Variable, pos: Self::Position ) -> Self::Variable

Request the preimage oracle for len bytes and store the bytes starting from addr, and it returns the number of bytes actually read. The number of bytes actually read will be set into pos. The first 8 bytes will be the length of the preimage, encoded as an unsigned 64bits, and the rest will be the preimage.

source

fn request_hint_write(&mut self, addr: &Self::Variable, len: &Self::Variable)

source

fn reset(&mut self)

Reset the environment to handle the next instruction

Provided Methods§

source

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.

source

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.

source

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

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

source

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

Set the general purpose register with index idx to value.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this operation.

source

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.

Safety

No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this operation.

source

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.

Safety

Callers of this function must manually update the registers if required, this function will only update the access counter.

source

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

source

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.

Safety

Callers of this function must manually update the registers if required, this function will only update the access counter.

source

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

source

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

source

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.

Safety

Callers of this function must manually update the memory if required, this function will only update the access counter.

source

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

source

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

source

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

Adds a lookup to the RangeCheck16Lookup table

source

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

source

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

Adds a lookup to the ByteLookup table

source

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

source

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

Adds a lookup to the AtMost4Lookup table

source

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

Range checks with 1 lookup to the AtMost4Lookup table 0 <= value < 4

source

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

source

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

source

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

source

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

source

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

source

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.

source

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.

Implementors§

source§

impl<Fp: Field> InterpreterEnv for o1vm::interpreters::mips::constraints::Env<Fp>

§

type Position = ColumnAlias

§

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

source§

impl<Fp: Field, PreImageOracle: PreImageOracleT> InterpreterEnv for o1vm::interpreters::mips::witness::Env<Fp, PreImageOracle>