From fa1a4f7254a9beacb2082a0dae07248f1e645290 Mon Sep 17 00:00:00 2001 From: dannywillems Date: Mon, 23 Dec 2024 20:10:15 +0000 Subject: [PATCH] deploy: ef1688a42ead6a94fd0f3d636423aa1522108207 --- rustdoc/help.html | 2 +- rustdoc/index.html | 2 +- .../riscv32im/constraints/struct.Env.html | 2 +- .../interpreter/fn.interpret_instruction.html | 2 +- .../interpreter/fn.interpret_itype.html | 2 +- .../interpreter/fn.interpret_mtype.html | 2 +- .../interpreter/fn.interpret_rtype.html | 2 +- .../interpreter/fn.interpret_sbtype.html | 2 +- .../interpreter/fn.interpret_stype.html | 2 +- .../interpreter/fn.interpret_syscall.html | 2 +- .../interpreter/fn.interpret_ujtype.html | 2 +- .../interpreter/fn.interpret_utype.html | 2 +- .../riscv32im/interpreter/index.html | 2 +- .../interpreter/trait.InterpreterEnv.html | 8 +-- .../interpreters/riscv32im/witness/index.html | 2 +- .../riscv32im/witness/struct.Env.html | 64 +++++++++---------- rustdoc/settings.html | 2 +- .../riscv32im/interpreter.rs.html | 16 ++++- .../interpreters/riscv32im/witness.rs.html | 16 +++++ 19 files changed, 82 insertions(+), 52 deletions(-) diff --git a/rustdoc/help.html b/rustdoc/help.html index 5b57a161fa..f74e384bbd 100644 --- a/rustdoc/help.html +++ b/rustdoc/help.html @@ -1 +1 @@ -Rustdoc help

Rustdoc help

Back
\ No newline at end of file +Rustdoc help

Rustdoc help

Back
\ No newline at end of file diff --git a/rustdoc/index.html b/rustdoc/index.html index d22507a620..5d5014a7dd 100644 --- a/rustdoc/index.html +++ b/rustdoc/index.html @@ -1 +1 @@ -Index of crates

List of all crates

\ No newline at end of file +Index of crates

List of all crates

\ No newline at end of file diff --git a/rustdoc/o1vm/interpreters/riscv32im/constraints/struct.Env.html b/rustdoc/o1vm/interpreters/riscv32im/constraints/struct.Env.html index 33db81bbd7..626db0f760 100644 --- a/rustdoc/o1vm/interpreters/riscv32im/constraints/struct.Env.html +++ b/rustdoc/o1vm/interpreters/riscv32im/constraints/struct.Env.html @@ -226,7 +226,7 @@ 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 +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.

Auto Trait Implementations§

§

impl<F> RefUnwindSafe for Env<F>where F: RefUnwindSafe,

§

impl<F> Send for Env<F>

§

impl<F> Sync for Env<F>

§

impl<F> Unpin for Env<F>where F: Unpin,

§

impl<F> UnwindSafe for Env<F>where diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_instruction.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_instruction.html index fde6026b9b..aa5e2a40f9 100644 --- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_instruction.html +++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_instruction.html @@ -1,4 +1,4 @@ -interpret_instruction in o1vm::interpreters::riscv32im::interpreter - Rust

Function o1vm::interpreters::riscv32im::interpreter::interpret_instruction

source · 
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
 )

\ No newline at end of file
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_itype.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_itype.html
index 53e0e9c71c..45b8719ffb 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_itype.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_itype.html
@@ -1,4 +1,4 @@
-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 6884e40b95..13f75cd007 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 3bfcc05847..09a94855c1 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 b832da04d2..24bed3fb73 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 fee630ac53..2be9a42917 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 4c9b748b69..67461a2837 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
 )

\ No newline at end of file
diff --git a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_ujtype.html b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_ujtype.html
index 18c421a1b0..ad6c647534 100644
--- a/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_ujtype.html
+++ b/rustdoc/o1vm/interpreters/riscv32im/interpreter/fn.interpret_ujtype.html
@@ -1,4 +1,4 @@
-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 13aeedcfa1..eec38e5458 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 5f8e641815..3c909c626c 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 1dbdaf540c..1a56f9a318 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;
 
@@ -631,7 +631,7 @@ 
Safety

     &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 reset(&mut self)

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.

+) -> Self::Variable
source

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

source

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

source

fn reset(&mut self)

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.

@@ -696,6 +696,6 @@
Safety
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 +

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::riscv32im::constraints::Env<Fp>

§

type Position = Column

§

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

source§

impl<Fp: Field> InterpreterEnv for o1vm::interpreters::riscv32im::witness::Env<Fp>

§

type Position = Column

§

type Variable = u64

\ No newline at end of file +

Implementors§

source§

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

§

type Position = Column

§

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

source§

impl<Fp: Field> InterpreterEnv for o1vm::interpreters::riscv32im::witness::Env<Fp>

§

type Position = Column

§

type Variable = u64

\ No newline at end of file diff --git a/rustdoc/o1vm/interpreters/riscv32im/witness/index.html b/rustdoc/o1vm/interpreters/riscv32im/witness/index.html index b8288e1b27..7405b9e6bc 100644 --- a/rustdoc/o1vm/interpreters/riscv32im/witness/index.html +++ b/rustdoc/o1vm/interpreters/riscv32im/witness/index.html @@ -1,4 +1,4 @@ -o1vm::interpreters::riscv32im::witness - Rust

Module o1vm::interpreters::riscv32im::witness

source ·

Structs

source§

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. Read more
source§

unsafe fn mul_signed_witness( +position_underflow respectively. Read more

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. Read more
source§

unsafe fn mul_hi_signed( +) -> Self::Variable

Returns x * y, where x and y are treated as integers, storing the result in position. Read more
source§

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. Read more
source§

unsafe fn mul_lo_signed( +) -> Self::Variable

Returns ((x * y) >> 32, storing the results in position. Read more
source§

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 Read more
source§

unsafe fn mul_hi( +) -> Self::Variable

Returns (x * y) & ((1 << 32) - 1)), storing the results in position Read more
source§

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. Read more
source§

unsafe fn mul_hi_signed_unsigned( +) -> Self::Variable

Returns ((x * y) >> 32, storing the results in position. Read more
source§

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. Read more
source§

unsafe fn div_signed( +) -> Self::Variable

Returns ((x * y) >> 32, storing the results in position. Read more
source§

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. Read more
source§

unsafe fn mul_lo( +) -> Self::Variable

Returns x / y, storing the results in position. Read more
source§

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. Read more
source§

unsafe fn mod_signed( +) -> Self::Variable

Returns (x * y) & ((1 << 32) - 1)), storing the results in position. Read more
source§

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. Read more
source§

unsafe fn div( +) -> Self::Variable

Returns x % y, storing the results in position. Read more
source§

unsafe fn div( &mut self, x: &Self::Variable, y: &Self::Variable, position: Self::Position -) -> Self::Variable

Returns x / y, storing the results in position. Read more
source§

unsafe fn mod_unsigned( +) -> Self::Variable

Returns x / y, storing the results in position. Read more
source§

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. Read more
source§

unsafe fn count_leading_zeros( +) -> Self::Variable

Returns x % y, storing the results in position. Read more
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. Read more
source§

unsafe fn count_leading_ones( +) -> Self::Variable

Returns the number of leading 0s in x, storing the result in position. Read more
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. Read more
source§

fn copy( +) -> Self::Variable

Returns the number of leading 1s in x, storing the result in position. Read more
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 reset(&mut self)

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. Read more
source§

unsafe fn push_register_access( +) -> Self::Variable

source§

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

source§

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

source§

fn reset(&mut self)

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. Read more
source§

unsafe fn push_register_access( &mut self, idx: &Self::Variable, value: Self::Variable @@ -237,7 +237,7 @@ 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 +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.

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 78856e0fed..042ebee940 100644 --- a/rustdoc/settings.html +++ b/rustdoc/settings.html @@ -1 +1 @@ -Rustdoc settings

Rustdoc settings

Back
\ No newline at end of file +Rustdoc settings

Rustdoc settings

Back
\ No newline at end of file diff --git a/rustdoc/src/o1vm/interpreters/riscv32im/interpreter.rs.html b/rustdoc/src/o1vm/interpreters/riscv32im/interpreter.rs.html index c6fdb567da..901edfce64 100644 --- a/rustdoc/src/o1vm/interpreters/riscv32im/interpreter.rs.html +++ b/rustdoc/src/o1vm/interpreters/riscv32im/interpreter.rs.html @@ -2538,6 +2538,13 @@ 2538 2539 2540 +2541 +2542 +2543 +2544 +2545 +2546 +2547 

//! This module implement an interpreter for the RISCV32 IM instruction set
 //! architecture.
 //!
@@ -3928,12 +3935,19 @@
     /// Given a variable `x`, this function extends it to a signed integer of
     /// `bitlength` bits.
     fn sign_extend(&mut self, x: &Self::Variable, bitlength: u32) -> Self::Variable {
+        assert!(bitlength <= 32);
         // FIXME: Constrain `high_bit`
         let high_bit = {
             let pos = self.alloc_scratch();
             unsafe { self.bitmask(x, bitlength, bitlength - 1, pos) }
         };
-        high_bit * Self::constant(((1 << (32 - bitlength)) - 1) << bitlength) + x.clone()
+        // Casting in u64 for special case of bitlength = 0 to avoid overflow.
+        // No condition for constant time execution.
+        // Decomposing the steps for readability.
+        let v: u64 = (1u64 << (32 - bitlength)) - 1;
+        let v: u64 = v << bitlength;
+        let v: u32 = v as u32;
+        high_bit * Self::constant(v) + x.clone()
     }
 
     fn report_exit(&mut self, exit_code: &Self::Variable);
diff --git a/rustdoc/src/o1vm/interpreters/riscv32im/witness.rs.html b/rustdoc/src/o1vm/interpreters/riscv32im/witness.rs.html
index cc3d2add55..c009f18d9b 100644
--- a/rustdoc/src/o1vm/interpreters/riscv32im/witness.rs.html
+++ b/rustdoc/src/o1vm/interpreters/riscv32im/witness.rs.html
@@ -938,6 +938,14 @@
 938
 939
 940
+941
+942
+943
+944
+945
+946
+947
+948
 
// TODO: do we want to be more restrictive and refer to the number of accesses
 //       to the SAME register/memory addrss?
 use super::{
@@ -1154,6 +1162,14 @@
         lowest_bit: u32,
         position: Self::Position,
     ) -> Self::Variable {
+        assert!(
+            lowest_bit < highest_bit,
+            "The lowest bit must be strictly lower than the highest bit"
+        );
+        assert!(
+            highest_bit <= 32,
+            "The interpreter is for a 32bits architecture"
+        );
         let x: u32 = (*x).try_into().unwrap();
         let res = (x >> lowest_bit) & ((1 << (highest_bit - lowest_bit)) - 1);
         let res = res as u64;