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 75 methods
// Required methods
fn alloc_scratch(&mut self) -> Self::Position;
fn alloc_scratch_inverse(&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 assert_boolean(&mut self, 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;
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_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable;
unsafe fn mul_lo_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable;
unsafe fn mul_hi(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable;
unsafe fn mul_lo(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable;
unsafe fn mul_hi_signed_unsigned(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable;
unsafe fn div_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable;
unsafe fn mod_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable;
unsafe fn div(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable;
unsafe fn mod_unsigned(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> 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 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) { ... }
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_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§
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§
Sourcefn 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::interpreters::riscv32im::SCRATCH_SIZE elements can be allocated. If more temporary variables are required for an instruction, increase the value crate::interpreters::riscv32im::SCRATCH_SIZE
fn alloc_scratch_inverse(&mut self) -> Self::Position
fn variable(&self, column: Self::Position) -> Self::Variable
Sourcefn 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.
Sourcefn activate_selector(&mut self, selector: Instruction)
fn activate_selector(&mut self, selector: Instruction)
Activate the selector for the given instruction.
Sourcefn 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.
Sourcefn 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.
Sourcefn 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.
fn add_lookup(&mut self, lookup: RAMLookup<Self::Variable, LookupTableIDs>)
fn instruction_counter(&self) -> Self::Variable
fn increase_instruction_counter(&mut self)
Sourceunsafe 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
.
§Safety
No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this operation.
Sourceunsafe 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, )
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.
Sourceunsafe 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
.
§Safety
No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this operation.
Sourceunsafe 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.
§Safety
No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this operation.
Sourceunsafe 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
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.
Sourceunsafe fn push_memory(&mut self, addr: &Self::Variable, value: Self::Variable)
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.
Sourceunsafe 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
.
§Safety
No lookups or other constraints are added as part of this operation. The caller must manually add the lookups for this memory operation.
Sourceunsafe 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, )
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.
fn constant(x: u32) -> Self::Variable
Sourceunsafe 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.
§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.
Sourceunsafe 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
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
.
Sourceunsafe 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
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
.
Sourceunsafe 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
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
.
Sourceunsafe 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
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
.
fn is_zero(&mut self, x: &Self::Variable) -> Self::Variable
Sourcefn 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
.
Sourceunsafe 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
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
Sourceunsafe 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
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
Sourceunsafe 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
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.
Sourceunsafe 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
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.
Sourceunsafe 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
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.
Sourceunsafe 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
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.
Sourceunsafe 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.
§Safety
There are no constraints on the returned values; callers must manually add constraints to ensure that they are correctly constructed.
Sourceunsafe 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.
§Safety
There are no constraints on the returned values; callers must manually add constraints to ensure that they are correctly constructed.
Sourceunsafe 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
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.
Sourceunsafe fn mul_hi_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable
unsafe fn mul_hi_signed( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position, ) -> Self::Variable
Returns ((x * y) >> 32
, storing the results in position
.
§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.
Sourceunsafe fn mul_lo_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable
unsafe fn mul_lo_signed( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position, ) -> Self::Variable
Returns (x * y) & ((1 << 32) - 1))
, storing the results in position
§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.
Sourceunsafe fn mul_hi(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable
unsafe fn mul_hi( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position, ) -> Self::Variable
Returns ((x * y) >> 32
, storing the results in position
.
§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.
Sourceunsafe fn mul_lo(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable
unsafe fn mul_lo( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position, ) -> Self::Variable
Returns (x * y) & ((1 << 32) - 1))
, storing the results in position
.
§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.
Sourceunsafe fn mul_hi_signed_unsigned(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable
unsafe fn mul_hi_signed_unsigned( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position, ) -> Self::Variable
Returns ((x * y) >> 32
, storing the results in position
.
§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.
Sourceunsafe fn div_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable
unsafe fn div_signed( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position, ) -> Self::Variable
Returns x / y
, storing the results in position
.
§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.
Division by zero will create a panic! exception. The RISC-V specification leaves the case unspecified, and therefore we prefer to forbid this case while building the witness.
Sourceunsafe fn mod_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable
unsafe fn mod_signed( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position, ) -> Self::Variable
Returns x % y
, storing the results in position
.
§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.
Sourceunsafe fn div(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable
unsafe fn div( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position, ) -> Self::Variable
Returns x / y
, storing the results in position
.
§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.
Division by zero will create a panic! exception. The RISC-V specification leaves the case unspecified, and therefore we prefer to forbid this case while building the witness.
Sourceunsafe fn mod_unsigned(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
position: Self::Position,
) -> Self::Variable
unsafe fn mod_unsigned( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position, ) -> Self::Variable
Returns x % y
, storing the results in position
.
§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.
Sourceunsafe 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
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.
Sourceunsafe 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
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.
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)
Provided Methods§
Sourcefn 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.
Sourcefn 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.
Sourceunsafe fn push_register(&mut self, idx: &Self::Variable, value: Self::Variable)
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.
Sourceunsafe 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, )
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.
Sourceunsafe 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.
§Safety
Callers of this function must manually update the registers if required, this function will only update the access counter.
fn read_register(&mut self, idx: &Self::Variable) -> Self::Variable
Sourceunsafe 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
.
§Safety
Callers of this function must manually update the registers if required, this function will only update the access counter.
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)
Sourceunsafe 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
.
§Safety
Callers of this function must manually update the memory if required, this function will only update the access counter.
fn read_memory(&mut self, addr: &Self::Variable) -> Self::Variable
fn write_memory(&mut self, addr: &Self::Variable, new_value: Self::Variable)
Sourcefn lookup_16bits(&mut self, value: &Self::Variable)
fn lookup_16bits(&mut self, value: &Self::Variable)
Adds a lookup to the RangeCheck16Lookup table
Sourcefn 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).
Sourcefn lookup_8bits(&mut self, value: &Self::Variable)
fn lookup_8bits(&mut self, value: &Self::Variable)
Adds a lookup to the ByteLookup table
Sourcefn 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).
Sourcefn lookup_2bits(&mut self, value: &Self::Variable)
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
Sourcefn increase_heap_pointer(
&mut self,
by_amount: &Self::Variable,
if_is_true: &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.
Sourcefn sign_extend(&mut self, x: &Self::Variable, bitlength: u32) -> Self::Variable
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.
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.