The lookup aggregation, i.e. phi
The fixed tables. The parameter is considered to the indexed table.
self and other values to be equal, and is used
by ==.!=. The default implementation is almost always
diff --git a/rustdoc/kimchi_msm/witness/struct.Witness.html b/rustdoc/kimchi_msm/witness/struct.Witness.html
index d6a8787cfd..bca4c1075f 100644
--- a/rustdoc/kimchi_msm/witness/struct.Witness.html
+++ b/rustdoc/kimchi_msm/witness/struct.Witness.html
@@ -10,7 +10,7 @@
cols: Box<[T; N_WIT]>A witness row is represented by an array of N witness columns When T is a vector, then the witness describes the rows of the circuit.
-par_iter. Read moreIterate over the columns in the circuit.
@@ -20,7 +20,7 @@ Vec<G>: IntoParallelIterator,Iterate over the columns in the circuit, in parallel.
&'data mut T reference.self. Read moreThis method takes a witness and a vector of evaluations to the zero +) -> RelaxedWitness<G, W>
This method takes a witness and a vector of evaluations to the zero polynomial, returning a relaxed witness which is composed by the extended witness and the error vector that is set to the zero polynomial.
diff --git a/rustdoc/o1vm/interpreters/riscv32im/constraints/struct.Env.html b/rustdoc/o1vm/interpreters/riscv32im/constraints/struct.Env.html index b963c51202..36d6589a93 100644 --- a/rustdoc/o1vm/interpreters/riscv32im/constraints/struct.Env.html +++ b/rustdoc/o1vm/interpreters/riscv32im/constraints/struct.Env.html @@ -221,12 +221,12 @@ )addr, adding constraints asserting that the old value was
old_value and that the new value will be new_value. Read morebits-1 (bits <= 16).bits-1 (bits <= 8).bits-1 (bits <= 8).by_amount if if_is_true is 1, and returns the previous
-value of the heap pointer.pub fn interpret_instruction<Env: InterpreterEnv>(
+interpret_instruction in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_instruction
source · pub fn interpret_instruction<Env: InterpreterEnv>(
env: &mut Env,
instr: Instruction
)
interpret_itype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_itype
source · pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: IInstruction)
Expand description
Interpret an I-type instruction.
+
interpret_itype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_itype
source · pub fn interpret_itype<Env: InterpreterEnv>(env: &mut Env, instr: IInstruction)
Expand description
Interpret an I-type instruction.
The encoding of an I-type instruction is as follows:
| 31 20 | 19 15 | 14 12 | 11 7 | 6 0 |
| immediate | rs1 | funct3 | rd | opcode |
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_mtype.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_mtype.html
index 8bfa8c8781..66963d4b7c 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_mtype.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_mtype.html
@@ -1,4 +1,4 @@
-interpret_mtype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_mtype
source · pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
Expand description
Interpret an M-type instruction.
+
interpret_mtype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_mtype
source · pub fn interpret_mtype<Env: InterpreterEnv>(env: &mut Env, instr: MInstruction)
Expand description
Interpret an M-type instruction.
The encoding of an M-type instruction is as follows:
| 31 27 | 26 25 | 24 20 | 19 15 | 14 12 | 11 7 | 6 0 |
| 00000 | 01 | rs2 | rs1 | funct3 | rd | opcode |
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_rtype.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_rtype.html
index d9aefbb2cf..530647e694 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_rtype.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_rtype.html
@@ -1,4 +1,4 @@
-interpret_rtype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_rtype
source · pub fn interpret_rtype<Env: InterpreterEnv>(env: &mut Env, instr: RInstruction)
Expand description
Interpret an R-type instruction.
+
interpret_rtype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_rtype
source · pub fn interpret_rtype<Env: InterpreterEnv>(env: &mut Env, instr: RInstruction)
Expand description
Interpret an R-type instruction.
The encoding of an R-type instruction is as follows:
| 31 25 | 24 20 | 19 15 | 14 12 | 11 7 | 6 0 |
| funct5 & funct 2 | rs2 | rs1 | funct3 | rd | opcode |
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_sbtype.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_sbtype.html
index 130ff44c44..aace3fed38 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_sbtype.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_sbtype.html
@@ -1,4 +1,4 @@
-interpret_sbtype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_sbtype
source · pub fn interpret_sbtype<Env: InterpreterEnv>(
+interpret_sbtype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_sbtype
source · pub fn interpret_sbtype<Env: InterpreterEnv>(
env: &mut Env,
instr: SBInstruction
)
Expand description
Interpret an SB-type instruction.
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_stype.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_stype.html
index 36fab47e02..8fdae80fab 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_stype.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_stype.html
@@ -1,4 +1,4 @@
-
interpret_stype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_stype
source · pub fn interpret_stype<Env: InterpreterEnv>(env: &mut Env, instr: SInstruction)
Expand description
Interpret an S-type instruction.
+
interpret_stype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_stype
source · pub fn interpret_stype<Env: InterpreterEnv>(env: &mut Env, instr: SInstruction)
Expand description
Interpret an S-type instruction.
The encoding of an S-type instruction is as follows:
| 31 25 | 24 20 | 19 15 | 14 12 | 11 7 | 6 0 |
| immediate | rs2 | rs1 | funct3 | imm | opcode |
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_syscall.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_syscall.html
index a5420f8c15..86a4fe8de3 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_syscall.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_syscall.html
@@ -1,4 +1,4 @@
-interpret_syscall in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_syscall
source · pub fn interpret_syscall<Env: InterpreterEnv>(
+interpret_syscall in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_syscall
source · pub fn interpret_syscall<Env: InterpreterEnv>(
env: &mut Env,
_instr: SyscallInstruction
)
interpret_ujtype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_ujtype
source · pub fn interpret_ujtype<Env: InterpreterEnv>(
+interpret_ujtype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_ujtype
source · pub fn interpret_ujtype<Env: InterpreterEnv>(
env: &mut Env,
instr: UJInstruction
)
Expand description
Interpret an UJ-type instruction.
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_utype.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_utype.html
index b22e751d9b..f4eb38adef 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_utype.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_utype.html
@@ -1,4 +1,4 @@
-
interpret_utype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_utype
source · pub fn interpret_utype<Env: InterpreterEnv>(env: &mut Env, instr: UInstruction)
Expand description
Interpret an U-type instruction.
+
interpret_utype in o1vm::interpreters::riscv32im::interpreter - Rust Function o1vm::interpreters::riscv32im::interpreter::interpret_utype
source · pub fn interpret_utype<Env: InterpreterEnv>(env: &mut Env, instr: UInstruction)
Expand description
Interpret an U-type instruction.
The encoding of an U-type instruction is as follows:
| 31 12 | 11 7 | 6 0 |
| immediate | rd | opcode |
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/index.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/index.html
index 14cb6fa8e8..ff128da15b 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/index.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/index.html
@@ -1,4 +1,4 @@
-o1vm::interpreters::riscv32im::interpreter - Rust Module o1vm::interpreters::riscv32im::interpreter
source · Expand description
This module implement an interpreter for the RISCV32 IM instruction set
+
o1vm::interpreters::riscv32im::interpreter - Rust Module o1vm::interpreters::riscv32im::interpreter
source · Expand description
This module implement an interpreter for the RISCV32 IM instruction set
architecture.
The implementation mostly follows (and copy) code from the MIPS interpreter
available here.
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/trait.InterpreterEnv.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/trait.InterpreterEnv.html
index 7b5af0cfdc..6794b9bbfd 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/trait.InterpreterEnv.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/trait.InterpreterEnv.html
@@ -1,4 +1,4 @@
-InterpreterEnv in o1vm::interpreters::riscv32im::interpreter - Rust Trait o1vm::interpreters::riscv32im::interpreter::InterpreterEnv
source · pub trait InterpreterEnv {
+InterpreterEnv in o1vm::interpreters::riscv32im::interpreter - Rust Trait o1vm::interpreters::riscv32im::interpreter::InterpreterEnv
source · 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;
@@ -570,7 +570,7 @@ 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(
+
sourceunsafe fn div_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
@@ -580,10 +580,7 @@ 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(
+
sourceunsafe fn mod_signed(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
@@ -593,7 +590,7 @@ 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,
@@ -603,10 +600,7 @@ 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(
+
sourceunsafe fn mod_unsigned(
&mut self,
x: &Self::Variable,
y: &Self::Variable,
@@ -616,7 +610,7 @@ 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(
+
sourceunsafe fn count_leading_ones(
+
sourcefn copy(
+
sourcefn copy(
&mut self,
x: &Self::Variable,
position: Self::Position
-) -> Self::Variable
sourcefn set_halted(&mut self, flag: Self::Variable)
sourcefn report_exit(&mut self, exit_code: &Self::Variable)
sourcefn reset(&mut self)
Provided Methods§
sourcefn 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.
+) -> Self::Variablesourcefn set_halted(&mut self, flag: Self::Variable)
sourcefn report_exit(&mut self, exit_code: &Self::Variable)
sourcefn reset(&mut self)
Provided Methods§
sourcefn 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)
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)
sourcefn 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)
Adds a lookup to the AtMost4Lookup table
-sourcefn range_check64(&mut self, _value: &Self::Variable)
sourcefn set_instruction_pointer(&mut self, ip: Self::Variable)
sourcefn get_instruction_pointer(&mut self) -> Self::Variable
sourcefn set_next_instruction_pointer(&mut self, ip: Self::Variable)
sourcefn get_next_instruction_pointer(&mut self) -> Self::Variable
sourcefn range_check64(&mut self, _value: &Self::Variable)
sourcefn set_instruction_pointer(&mut self, ip: Self::Variable)
sourcefn get_instruction_pointer(&mut self) -> Self::Variable
sourcefn set_next_instruction_pointer(&mut self, ip: Self::Variable)
sourcefn 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
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
Given a variable x, this function extends it to a signed integer of
+
sourcefn 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::riscv32im::constraints::Env<Fp>
\ No newline at end of file
diff --git a/rustdoc/o1vm/interpreters/riscv32im/witness/struct.Env.html b/rustdoc/o1vm/interpreters/riscv32im/witness/struct.Env.html
index 02cd693fae..693da7bfff 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/witness/struct.Env.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/witness/struct.Env.html
@@ -232,12 +232,12 @@
)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 moresource§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 tablesource§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 tablesource§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 tablesource§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(
+is at most 2^bits-1 (bits <= 8).
source§fn lookup_2bits(&mut self, value: &Self::Variable)
Adds a lookup to the AtMost4Lookup tablesource§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.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
diff --git a/rustdoc/settings.html b/rustdoc/settings.html
index 042ebee940..9f421508ce 100644
--- a/rustdoc/settings.html
+++ b/rustdoc/settings.html
@@ -1 +1 @@
-Rustdoc settings Rustdoc settings
BackRustdoc settings Rustdoc settings
Back
//! This module implement an interpreter for the RISCV32 IM instruction set
//! architecture.
//!
@@ -3998,10 +3970,6 @@
/// 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.
unsafe fn div_signed(
&mut self,
x: &Self::Variable,
@@ -4030,10 +3998,6 @@
/// 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.
unsafe fn div(
&mut self,
x: &Self::Variable,
@@ -5078,27 +5042,7 @@
env.set_next_instruction_pointer(addr);
}
SBInstruction::BranchGreaterThanEqualUnsigned => {
- // bgeu: if (x[rs1] >=u x[rs2]) pc += sext(offset)
- let local_rs1 = env.read_register(&rs1);
- let local_rs2 = env.read_register(&rs2);
-
- let rd_scratch = env.alloc_scratch();
- let less_than = unsafe { env.test_less_than(&local_rs1, &local_rs2, rd_scratch) };
- let offset =
- less_than.clone() * Env::constant(4) + (Env::constant(1) - less_than) * imm0_12;
-
- // greater than equal is the negation of less than
- let addr = {
- let res_scratch = env.alloc_scratch();
- let overflow_scratch = env.alloc_scratch();
- let (res, _overflow) = unsafe {
- env.add_witness(&instruction_pointer, &offset, res_scratch, overflow_scratch)
- };
- res
- };
-
- env.set_instruction_pointer(next_instruction_pointer);
- env.set_next_instruction_pointer(addr);
+ unimplemented!("BranchGreaterThanEqualUnsigned")
}
};
}