move-sui: add simulation for the cast_u8 instruction

formal-land · Oct 18, 2024 · ae83e46 · ae83e46
1 parent 230d00e
commit ae83e46
Show file tree

Hide file tree

Showing 2 changed files with 45 additions and 7 deletions.
diff --git 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
@@ -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;
+}.