Struct o1vm::mips::witness::Env

pub struct Env<Fp, PreImageOracle: PreImageOracleT> {

    pub instruction_counter: u64,
    pub memory: Vec<(u32, Vec<u8>)>,
    pub last_memory_accesses: [usize; 3],
    pub memory_write_index: Vec<(u32, Vec<u64>)>,
    pub last_memory_write_index_accesses: [usize; 3],
    pub registers: Registers<u32>,
    pub registers_write_index: Registers<u64>,
    pub scratch_state_idx: usize,
    pub scratch_state: [Fp; 98],
    pub halt: bool,
    pub syscall_env: SyscallEnv,
    pub preimage_oracle: PreImageOracle,
    pub preimage: Option<Vec<u8>>,
    pub preimage_bytes_read: u64,
    pub preimage_key: Option<[u8; 32]>,
    pub keccak_env: Option<KeccakEnv<Fp>>,
    pub hash_counter: u64,
}

This structure represents the environment the virtual machine state will use to transition. This environment will be used by the interpreter. The virtual machine has access to its internal state and some external memory. In addition to that, it has access to the environment of the Keccak interpreter that is used to verify the preimage requested during the execution.

Fields

instruction_counter: u64

memory: Vec<(u32, Vec<u8>)>

last_memory_accesses: [usize; 3]

memory_write_index: Vec<(u32, Vec<u64>)>

last_memory_write_index_accesses: [usize; 3]

registers: Registers<u32>

registers_write_index: Registers<u64>

scratch_state_idx: usize

scratch_state: [Fp; 98]

halt: bool

syscall_env: SyscallEnv

preimage_oracle: PreImageOracle

preimage: Option<Vec<u8>>

preimage_bytes_read: u64

preimage_key: Option<[u8; 32]>

keccak_env: Option<KeccakEnv<Fp>>

hash_counter: u64

Implementations

impl<Fp: Field, PreImageOracle: PreImageOracleT> Env<Fp, PreImageOracle>

pub fn create( page_size: usize, state: State, preimage_oracle: PreImageOracle ) -> Self

pub fn reset_scratch_state(&mut self)

pub fn write_column(&mut self, column: Column, value: u64)

pub fn write_field_column(&mut self, column: Column, value: Fp)

pub fn update_last_memory_access(&mut self, i: usize)

pub fn get_memory_page_index(&mut self, page: u32) -> usize

pub fn update_last_memory_write_index_access(&mut self, i: usize)

pub fn get_memory_access_page_index(&mut self, page: u32) -> usize

pub fn get_memory_direct(&mut self, addr: u32) -> u8

pub fn decode_instruction(&mut self) -> (Instruction, u32)

pub fn normalized_instruction_counter(&self) -> u64

The actual number of instructions executed results from dividing the instruction counter by MAX_ACC (floor).

NOTE: actually, in practice it will be less than that, as there is no single instruction that performs all of them.

pub fn next_instruction_counter(&self) -> u64

Computes what is the non-normalized next instruction counter, which accounts for the maximum number of register and memory accesses per instruction.

Because MAX_NB_REG_ACC = 7 and MAX_NB_MEM_ACC = 12, at most the same instruction will increase the instruction counter by MAX_ACC = 19.

Then, in order to update the instruction counter, we need to add 1 to the real instruction counter and multiply it by MAX_ACC to have a unique representation of each step (which is helpful for debugging).

pub fn step( &mut self, config: &VmConfiguration, metadata: &Meta, start: &Start ) -> Instruction

Execute a single step of the MIPS program. Returns the instruction that was executed.

Trait Implementations

impl<Fp: Field, PreImageOracle: PreImageOracleT> InterpreterEnv for Env<Fp, PreImageOracle>

type Position = ColumnAlias

A position can be seen as an indexed variable

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

type Variable = u64

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

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.

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, x: &Self::Variable, y: &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, x: &Self::Variable, y: &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 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.

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

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

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

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 is_zero(&mut self, x: &Self::Variable) -> 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.