From ae83e465f69d11e1178018a27800e4be2de8b41e Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Fri, 18 Oct 2024 11:47:47 +0200
Subject: [PATCH] move-sui: add simulation for the cast_u8 instruction

---
 .../simulations/move_vm_runtime/interpreter.v | 11 ++++-
 .../move_vm_types/values/values_impl.v        | 41 ++++++++++++++++---
 2 files changed, 45 insertions(+), 7 deletions(-)

diff --git a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
index 15e39b2c8..fb3a3b21c 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
@@ -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 => {
diff --git a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
index b74e0aebf..45d7ac8a9 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v
@@ -1034,21 +1034,21 @@ Module IntegerValue.
 
   Definition cast_u8 (self : IntegerValue.t) : PartialVMResult.t Z :=
   match self with
-  | IntegerValue.U8 l => Result.Ok (l)
+  | IntegerValue.U8 l => Result.Ok l
   | IntegerValue.U16 l => if l <=? 2^8 - 1
-    then Result.Ok (l)
+    then Result.Ok l
     else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
   | IntegerValue.U32 l => if l <=? 2^8 - 1
-    then Result.Ok (l)
+    then Result.Ok l
     else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
   | IntegerValue.U64 l => if l <=? 2^8 - 1
-    then Result.Ok (l)
+    then Result.Ok l
     else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
   | IntegerValue.U128 l => if l <=? 2^8 - 1
-    then Result.Ok ( l)
+    then Result.Ok l
     else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
   | IntegerValue.U256 l => if l <=? 2^8 - 1
-    then Result.Ok (l)
+    then Result.Ok l
     else Result.Err (PartialVMError.new StatusCode.ARITHMETIC_ERROR)
   end.
 
@@ -1614,3 +1614,32 @@ impl IntegerValue {
 }
 *)
 
+(*
+impl VMValueCast<IntegerValue> for Value {
+    fn cast(self) -> PartialVMResult<IntegerValue> {
+        match self.0 {
+            ValueImpl::U8(x) => Ok(IntegerValue::U8(x)),
+            ValueImpl::U16(x) => Ok(IntegerValue::U16(x)),
+            ValueImpl::U32(x) => Ok(IntegerValue::U32(x)),
+            ValueImpl::U64(x) => Ok(IntegerValue::U64(x)),
+            ValueImpl::U128(x) => Ok(IntegerValue::U128(x)),
+            ValueImpl::U256(x) => Ok(IntegerValue::U256(x)),
+            v => Err(PartialVMError::new(StatusCode::INTERNAL_TYPE_ERROR)
+                .with_message(format!("cannot cast {:?} to integer", v,))),
+        }
+    }
+}
+*)
+Global Instance Impl_VMValueCast_IntegerValue_for_Value :
+    VMValueCast.Trait Value.t IntegerValue.t : Set := {
+  cast self :=
+    match self with
+    | ValueImpl.U8 x => return? $ IntegerValue.U8 x
+    | ValueImpl.U16 x => return? $ IntegerValue.U16 x
+    | ValueImpl.U32 x => return? $ IntegerValue.U32 x
+    | ValueImpl.U64 x => return? $ IntegerValue.U64 x
+    | ValueImpl.U128 x => return? $ IntegerValue.U128 x
+    | ValueImpl.U256 x => return? $ IntegerValue.U256 x
+    | _ => Result.Err $ PartialVMError.new StatusCode.INTERNAL_TYPE_ERROR
+    end;
+}.