Struct o1vm::mips::constraints::Env
source · pub struct Env<Fp> {
pub scratch_state_idx: usize,
pub constraints: Vec<Expr<ConstantExpr<Fp>, Column>>,
pub lookups: Vec<RAMLookup<Expr<ConstantExpr<Fp>, Column>, LookupTableIDs>>,
}
Expand description
The environment keeping the constraints between the different polynomials
Fields§
§scratch_state_idx: usize
§constraints: Vec<Expr<ConstantExpr<Fp>, Column>>
A list of constraints, which are multi-variate polynomials over a field,
represented using the expression framework of kimchi
.
lookups: Vec<RAMLookup<Expr<ConstantExpr<Fp>, Column>, LookupTableIDs>>
Trait Implementations§
source§impl DecomposableTracer<Env<<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField>> for DecomposedMIPSTrace
impl DecomposableTracer<Env<<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField>> for DecomposedMIPSTrace
source§fn new(
domain_size: usize,
env: &mut Env<<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField>
) -> Self
fn new( domain_size: usize, env: &mut Env<<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField> ) -> Self
Create a new decomposable trace with the given domain size, and environment.
source§fn pad_witnesses(&mut self)
fn pad_witnesses(&mut self)
Pads the rows of the witnesses until reaching the domain size using the first
row repeatedly. It does not add selector columns.
source§impl<Fp: Field> InterpreterEnv for Env<Fp>
impl<Fp: Field> InterpreterEnv for Env<Fp>
§type Position = ColumnAlias
type Position = ColumnAlias
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.
source§fn request_preimage_write(
&mut self,
_addr: &Self::Variable,
len: &Self::Variable,
pos: Self::Position
) -> Self::Variable
fn request_preimage_write( &mut self, _addr: &Self::Variable, len: &Self::Variable, pos: Self::Position ) -> Self::Variable
This function checks that the preimage is read correctly. It adds 13 constraints, and 5 lookups for the communication channel. In particular, at every step it writes the bytes of the preimage into the channel (excluding the length bytes) and it reads the hash digest from the channel when the preimage is fully read. The output is the actual number of bytes that have been read.
source§fn alloc_scratch(&mut self) -> Self::Position
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 = Operations<ExprInner<Operations<ConstantExprInner<Fp>>, Column>>
fn variable(&self, column: Self::Position) -> Self::Variable
source§fn add_constraint(&mut self, assert_equals_zero: 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.source§fn check_is_zero(_assert_equals_zero: &Self::Variable)
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)
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)
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)
source§unsafe fn fetch_register(
&mut self,
_idx: &Self::Variable,
output: Self::Position
) -> Self::Variable
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
. Read moresource§unsafe fn push_register_if(
&mut self,
_idx: &Self::Variable,
_value: Self::Variable,
_if_is_true: &Self::Variable
)
unsafe fn push_register_if( &mut self, _idx: &Self::Variable, _value: Self::Variable, _if_is_true: &Self::Variable )
source§unsafe fn fetch_register_access(
&mut self,
_idx: &Self::Variable,
output: Self::Position
) -> Self::Variable
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
. Read moresource§unsafe fn push_register_access_if(
&mut self,
_idx: &Self::Variable,
_value: Self::Variable,
_if_is_true: &Self::Variable
)
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. Read moresource§unsafe fn fetch_memory(
&mut self,
_addr: &Self::Variable,
output: Self::Position
) -> Self::Variable
unsafe fn fetch_memory( &mut self, _addr: &Self::Variable, output: Self::Position ) -> Self::Variable
source§unsafe fn push_memory(&mut self, _addr: &Self::Variable, _value: Self::Variable)
unsafe fn push_memory(&mut self, _addr: &Self::Variable, _value: Self::Variable)
source§unsafe fn fetch_memory_access(
&mut self,
_addr: &Self::Variable,
output: Self::Position
) -> Self::Variable
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
. Read moresource§unsafe fn push_memory_access(
&mut self,
_addr: &Self::Variable,
_value: Self::Variable
)
unsafe fn push_memory_access( &mut self, _addr: &Self::Variable, _value: Self::Variable )
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
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. Read moresource§unsafe fn shift_left(
&mut self,
_x: &Self::Variable,
_by: &Self::Variable,
position: Self::Position
) -> Self::Variable
unsafe fn shift_left( &mut self, _x: &Self::Variable, _by: &Self::Variable, position: Self::Position ) -> Self::Variable
source§unsafe fn shift_right(
&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
source§unsafe fn shift_right_arithmetic(
&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
source§unsafe fn test_zero(
&mut self,
_x: &Self::Variable,
position: Self::Position
) -> Self::Variable
unsafe fn test_zero( &mut self, _x: &Self::Variable, position: Self::Position ) -> Self::Variable
source§unsafe fn inverse_or_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
source§fn equal(&mut self, x: &Self::Variable, y: &Self::Variable) -> Self::Variable
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
unsafe fn test_less_than( &mut self, _x: &Self::Variable, _y: &Self::Variable, position: Self::Position ) -> Self::Variable
source§unsafe fn test_less_than_signed(
&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
source§unsafe fn and_witness(
&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
source§unsafe fn nor_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
source§unsafe fn or_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
source§unsafe fn xor_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
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)
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. Read moresource§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 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. Read moresource§unsafe fn mul_signed_witness(
&mut self,
_x: &Self::Variable,
_y: &Self::Variable,
position: Self::Position
) -> Self::Variable
unsafe fn mul_signed_witness( &mut self, _x: &Self::Variable, _y: &Self::Variable, position: Self::Position ) -> Self::Variable
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)
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. Read moresource§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 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. Read moresource§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_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. Read moresource§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 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. Read moresource§unsafe fn count_leading_zeros(
&mut self,
_x: &Self::Variable,
position: Self::Position
) -> Self::Variable
unsafe fn count_leading_zeros( &mut self, _x: &Self::Variable, position: Self::Position ) -> Self::Variable
source§unsafe fn count_leading_ones(
&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_hint_write(&mut self, _addr: &Self::Variable, _len: &Self::Variable)
source§fn assert_is_zero(&mut self, assert_equals_zero: 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.source§fn assert_equal(&mut self, x: Self::Variable, y: Self::Variable)
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)
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)
unsafe fn push_register(&mut self, idx: &Self::Variable, value: Self::Variable)
source§unsafe fn push_register_access(
&mut self,
idx: &Self::Variable,
value: Self::Variable
)
unsafe fn push_register_access( &mut self, idx: &Self::Variable, value: Self::Variable )
source§unsafe fn access_register_if(
&mut self,
idx: &Self::Variable,
old_value: &Self::Variable,
new_value: &Self::Variable,
if_is_true: &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 )
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. Read morefn 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
)
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
. Read morefn 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)
source§unsafe fn access_memory(
&mut self,
addr: &Self::Variable,
old_value: &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
. Read morefn read_memory(&mut self, addr: &Self::Variable) -> Self::Variable
fn write_memory(&mut self, addr: &Self::Variable, new_value: Self::Variable)
source§fn lookup_16bits(&mut self, value: &Self::Variable)
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)
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)
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)
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)
fn lookup_2bits(&mut self, value: &Self::Variable)
Adds a lookup to the AtMost4Lookup table
source§fn range_check2(&mut self, value: &Self::Variable)
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
source§impl Tracer<N_MIPS_REL_COLS, DecomposableMIPSFoldingConfig, Env<<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField>> for MIPSTrace
impl Tracer<N_MIPS_REL_COLS, DecomposableMIPSFoldingConfig, Env<<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField>> for MIPSTrace
type Selector = ()
source§fn init(
domain_size: usize,
instr: Instruction,
env: &mut Env<<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField>
) -> Self
fn init( domain_size: usize, instr: Instruction, env: &mut Env<<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField> ) -> Self
Initialize a new trace with the given domain size, selector, and environment.
source§fn push_row(
&mut self,
_selector: Self::Selector,
row: &[<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField; 100]
)
fn push_row( &mut self, _selector: Self::Selector, row: &[<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField; 100] )
Add a witness row to the circuit (only for relation columns)
source§fn pad_with_row(
&mut self,
_selector: Self::Selector,
row: &[<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField; 100]
) -> usize
fn pad_with_row( &mut self, _selector: Self::Selector, row: &[<<DecomposableMIPSFoldingConfig as FoldingConfig>::Curve as AffineCurve>::ScalarField; 100] ) -> usize
Pad the rows of one opcode with the given row until
reaching the domain size if needed.
Returns the number of rows that were added.
It does not add selector columns.
source§fn pad_with_zeros(&mut self, _selector: Self::Selector) -> usize
fn pad_with_zeros(&mut self, _selector: Self::Selector) -> usize
Pads the rows of one opcode with zero rows until
reaching the domain size if needed.
Returns the number of rows that were added.
It does not add selector columns.
Auto Trait Implementations§
impl<Fp> RefUnwindSafe for Env<Fp>where Fp: RefUnwindSafe,
impl<Fp> Send for Env<Fp>where Fp: Send,
impl<Fp> Sync for Env<Fp>where Fp: Sync,
impl<Fp> Unpin for Env<Fp>where Fp: Unpin,
impl<Fp> UnwindSafe for Env<Fp>where Fp: UnwindSafe,
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more