From f6368d823e8741abf190274ca4050e4fd4c5c046 Mon Sep 17 00:00:00 2001
From: Guillaume Claret <dev@clarus.me>
Date: Mon, 21 Oct 2024 10:24:16 +0200
Subject: [PATCH] suggestion: definition of 'binop_int'

---
 .../simulations/move_vm_runtime/interpreter.v | 84 +++++++++++--------
 .../move_vm_types/values/values_impl.v        | 29 +++++++
 2 files changed, 80 insertions(+), 33 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..c185ab173 100644
--- a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
+++ b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v
@@ -334,40 +334,58 @@ Module Interpreter.
     |}.
   End Lens.
 
-  Module Impl_Interpreter.
-    Definition Self : Set. Admitted.
-
-    (* 
-        /// Perform a binary operation to two values at the top of the stack.
-    fn binop<F, T>(&mut self, f: F) -> PartialVMResult<()>
-    where
-        Value: VMValueCast<T>,
-        F: FnOnce(T, T) -> PartialVMResult<Value>,
-    {
-        let rhs = self.operand_stack.pop_as::<T>()?;
-        let lhs = self.operand_stack.pop_as::<T>()?;
-        let result = f(lhs, rhs)?;
-        self.operand_stack.push(result)
-    }
+  (*
+  /// Perform a binary operation to two values at the top of the stack.
+  fn binop<F, T>(&mut self, f: F) -> PartialVMResult<()>
+  where
+      Value: VMValueCast<T>,
+      F: FnOnce(T, T) -> PartialVMResult<Value>,
+  {
+      let rhs = self.operand_stack.pop_as::<T>()?;
+      let lhs = self.operand_stack.pop_as::<T>()?;
+      let result = f(lhs, rhs)?;
+      self.operand_stack.push(result)
+  }
+  *)
+  Definition binop {T : Set} `{VMValueCast.Trait Value.t T}
+      (f : T -> T -> PartialVMResult.t Value.t) :
+      MS! t (PartialVMResult.t unit) :=
+    letS!? lhs := liftS! Lens.lens_self_stack $ Stack.Impl_Stack.pop_as T in
+    letS!? rhs := liftS! Lens.lens_self_stack $ Stack.Impl_Stack.pop_as T in
+    letS!? result := returnS! $ f lhs rhs in
+    liftS! Lens.lens_self_stack $ Stack.Impl_Stack.push result.
 
-    /// Perform a binary operation for integer values.
-    fn binop_int<F>(&mut self, f: F) -> PartialVMResult<()>
-    where
-        F: FnOnce(IntegerValue, IntegerValue) -> PartialVMResult<IntegerValue>,
-    {
-        self.binop(|lhs, rhs| {
-            Ok(match f(lhs, rhs)? {
-                IntegerValue::U8(x) => Value::u8(x),
-                IntegerValue::U16(x) => Value::u16(x),
-                IntegerValue::U32(x) => Value::u32(x),
-                IntegerValue::U64(x) => Value::u64(x),
-                IntegerValue::U128(x) => Value::u128(x),
-                IntegerValue::U256(x) => Value::u256(x),
-            })
-        })
-    }
-    *)
-  End Impl_Interpreter.
+  (*
+  /// Perform a binary operation for integer values.
+  fn binop_int<F>(&mut self, f: F) -> PartialVMResult<()>
+  where
+      F: FnOnce(IntegerValue, IntegerValue) -> PartialVMResult<IntegerValue>,
+  {
+      self.binop(|lhs, rhs| {
+          Ok(match f(lhs, rhs)? {
+              IntegerValue::U8(x) => Value::u8(x),
+              IntegerValue::U16(x) => Value::u16(x),
+              IntegerValue::U32(x) => Value::u32(x),
+              IntegerValue::U64(x) => Value::u64(x),
+              IntegerValue::U128(x) => Value::u128(x),
+              IntegerValue::U256(x) => Value::u256(x),
+          })
+      })
+  }
+  *)
+  Definition binop_int (f : IntegerValue.t -> IntegerValue.t -> PartialVMResult.t IntegerValue.t) :
+    MS! t (PartialVMResult.t unit) :=
+    binop (fun lhs rhs =>
+      let? result := f lhs rhs in
+      match result with
+      | IntegerValue.U8 x => return? $ ValueImpl.U8 x
+      | IntegerValue.U16 x => return? $ ValueImpl.U16 x
+      | IntegerValue.U32 x => return? $ ValueImpl.U32 x
+      | IntegerValue.U64 x => return? $ ValueImpl.U64 x
+      | IntegerValue.U128 x => return? $ ValueImpl.U128 x
+      | IntegerValue.U256 x => return? $ ValueImpl.U256 x
+      end
+    ).
 End Interpreter.
 
 (* 
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..4dab7e5ae 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
@@ -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;
+}.