Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Draft: Complete interpreter instructions to the end #619

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Draft: Complete interpreter instructions to the end #619

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4f238d6
Draft: refactor(IntegerValue) - replace ImplValue.t with new inductiv…
Mushow Oct 17, 2024
230d00e
refactor: Replace PartialVMResult.t IntegerValue.t by PartialVMResult…
Mushow Oct 18, 2024
f73105a
feat: Add casting operations for integer types in bytecode interpreter
Mushow Oct 18, 2024
eba728b
feat: Implement VMValueCast trait for casting Value to IntegerValue
Mushow Oct 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 61 additions & 6 deletions CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1039,7 +1039,16 @@ Definition execute_instruction (pc : Z)
.push(Value::u8(integer_value.cast_u8()?))?;
}
*)
| Bytecode.CastU8 => returnS! $ Result.Ok InstrRet.Ok
| Bytecode.CastU8 =>
letS!? integer_value := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.pop_as IntegerValue.t
) in
letS!? integer_value := returnS! $ IntegerValue.cast_u8 integer_value in
doS!? liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.push $
ValueImpl.U8 integer_value
) in
returnS!? InstrRet.Ok

(*
Bytecode::CastU16 => {
Expand All @@ -1050,7 +1059,17 @@ Definition execute_instruction (pc : Z)
.push(Value::u16(integer_value.cast_u16()?))?;
}
*)
| Bytecode.CastU16 => returnS! $ Result.Ok InstrRet.Ok
| Bytecode.CastU16 =>
letS!? integer_value := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.pop_as IntegerValue.t
) in
letS!? integer_value := returnS! $ IntegerValue.cast_u16 integer_value in
doS!? liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.push $
ValueImpl.U16 integer_value
) in
returnS!? InstrRet.Ok


(*
Bytecode::CastU32 => {
Expand All @@ -1061,7 +1080,16 @@ Definition execute_instruction (pc : Z)
.push(Value::u32(integer_value.cast_u32()?))?;
}
*)
| Bytecode.CastU32 => returnS! $ Result.Ok InstrRet.Ok
| Bytecode.CastU32 =>
letS!? integer_value := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.pop_as IntegerValue.t
) in
letS!? integer_value := returnS! $ IntegerValue.cast_u32 integer_value in
doS!? liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.push $
ValueImpl.U32 integer_value
) in
returnS!? InstrRet.Ok

(*
Bytecode::CastU64 => {
Expand All @@ -1072,7 +1100,16 @@ Definition execute_instruction (pc : Z)
.push(Value::u64(integer_value.cast_u64()?))?;
}
*)
| Bytecode.CastU64 => returnS! $ Result.Ok InstrRet.Ok
| Bytecode.CastU64 =>
letS!? integer_value := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.pop_as IntegerValue.t
) in
letS!? integer_value := returnS! $ IntegerValue.cast_u64 integer_value in
doS!? liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.push $
ValueImpl.U64 integer_value
) in
returnS!? InstrRet.Ok

(*
Bytecode::CastU128 => {
Expand All @@ -1083,7 +1120,16 @@ Definition execute_instruction (pc : Z)
.push(Value::u128(integer_value.cast_u128()?))?;
}
*)
| Bytecode.CastU128 => returnS! $ Result.Ok InstrRet.Ok
| Bytecode.CastU128 =>
letS!? integer_value := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.pop_as IntegerValue.t
) in
letS!? integer_value := returnS! $ IntegerValue.cast_u128 integer_value in
doS!? liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.push $
ValueImpl.U128 integer_value
) in
returnS!? InstrRet.Ok

(*
Bytecode::CastU256 => {
Expand All @@ -1094,7 +1140,16 @@ Definition execute_instruction (pc : Z)
.push(Value::u256(integer_value.cast_u256()?))?;
}
*)
| Bytecode.CastU256 => returnS! $ Result.Ok InstrRet.Ok
| Bytecode.CastU256 =>
letS!? integer_value := liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.pop_as IntegerValue.t
) in
letS!? integer_value := returnS! $ IntegerValue.cast_u256 integer_value in
doS!? liftS! Interpreter.Lens.lens_state_self (
liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.push $
ValueImpl.U256 integer_value
) in
returnS!? InstrRet.Ok

(*
Bytecode::Add => {
Expand Down
Loading
Loading