sui: verify Bytecode.LdConst

CoqOfRust/lib/proofs/lib.v

@@ -99,3 +99,16 @@ Module BinOp.
     Qed.
   End Error.
 End BinOp.
+
+Module List.
+  Lemma Forall_nth_error {A : Set} (P : A -> Prop) (l : list A) (n : nat)
+      (H_l : List.Forall P l) :
+    match List.nth_error l n with
+    | Some x => P x
+    | None => True
+    end.
+  Proof.
+    generalize dependent n.
+    induction H_l; intros; destruct n; cbn; sfirstorder.
+  Qed.
+End List.

CoqOfRust/move_sui/proofs/move_binary_format/file_format.v

@@ -1,11 +1,37 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.simulations.M.
-
 Require Import move_sui.simulations.move_binary_format.file_format.
+Require Import move_sui.simulations.move_vm_types.values.values_impl.
+Require Import move_sui.proofs.move_vm_types.values.values_impl.
 
 Module SignatureToken.
   Lemma t_beq_is_valid (x y : SignatureToken.t) :
     SignatureToken.t_beq x y = true <-> x = y.
   Proof.
   Admitted.
 End SignatureToken.
+
+Module Constant.
+  Module Valid.
+    Definition t (x : Constant.t) : Prop :=
+      match Impl_Value.deserialize_constant x with
+      | None => False
+      | Some value => IsValueOfType.t value x.(Constant.type_)
+      end.
+  End Valid.
+End Constant.
+
+Module ConstantPool.
+  Module Valid.
+    Definition t (x : ConstantPool.t) : Prop :=
+      List.Forall Constant.Valid.t x.
+  End Valid.
+End ConstantPool.
+
+Module CompiledModule.
+  Module Valid.
+    Record t (x : CompiledModule.t) : Prop := {
+      constant_pool : ConstantPool.Valid.t x.(CompiledModule.constant_pool);
+    }.
+  End Valid.
+End CompiledModule.

CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v

@@ -1,41 +1,29 @@
 Require Import CoqOfRust.CoqOfRust.
 Require Import CoqOfRust.simulations.M.
 Require Import CoqOfRust.lib.proofs.lib.
-Require Import move_sui.proofs.move_abstract_stack.lib.
-Require Import move_sui.proofs.move_binary_format.file_format.
 Require Import move_sui.simulations.move_abstract_stack.lib.
 Require Import move_sui.simulations.move_binary_format.file_format.
 Require Import move_sui.simulations.move_bytecode_verifier.type_safety.
 Require Import move_sui.simulations.move_vm_runtime.interpreter.
 Require Import move_sui.simulations.move_vm_types.values.values_impl.
+Require Import move_sui.proofs.move_abstract_stack.lib.
+Require Import move_sui.proofs.move_binary_format.file_format.
+Require Import move_sui.proofs.move_vm_types.values.values_impl.
 
 Import simulations.M.Notations.
 
 Module TypeSafetyChecker.
   Module Valid.
     Record t (x : TypeSafetyChecker.t) : Prop := {
+      module : CompiledModule.Valid.t x.(TypeSafetyChecker.module);
       stack : AbstractStack.Valid.t x.(TypeSafetyChecker.stack);
     }.
   End Valid.
 End TypeSafetyChecker.
 
 Module IsValueOfType.
-  Definition t (value : Value.t) (typ : SignatureToken.t) : Prop :=
-    match value, typ with
-    | ValueImpl.U8 _, SignatureToken.U8 => True
-    | ValueImpl.U16 _, SignatureToken.U16 => True
-    | ValueImpl.U32 _, SignatureToken.U32 => True
-    | ValueImpl.U64 _, SignatureToken.U64 => True
-    | ValueImpl.U128 _, SignatureToken.U128 => True
-    | ValueImpl.U256 _, SignatureToken.U256 => True
-    | ValueImpl.Bool _, SignatureToken.Bool => True
-    | ValueImpl.Address _, SignatureToken.Address => True
-    (* TODO: other cases *)
-    | _, _ => False
-    end.
-
   Lemma value_of_bool (value : Value.t) (ty : SignatureToken.t)
-    (H_value : t value ty)
+    (H_value : IsValueOfType.t value ty)
     (* This is the form in which is appears in the proofs *)
     (H_ty : ty = SignatureToken.Bool) :
     exists b, value = ValueImpl.Bool b.
@@ -46,7 +34,7 @@ Module IsValueOfType.
   Qed.
 
   Lemma value_of_integer (value : Value.t) (ty : SignatureToken.t)
-      (H_value : t value ty)
+      (H_value : IsValueOfType.t value ty)
       (H_ty : SignatureToken.is_integer ty = true) :
     exists (integer_value : IntegerValue.t),
     value = IntegerValue.to_value_impl integer_value.
@@ -195,6 +183,10 @@ Lemma progress
     (type_safety_checker : TypeSafetyChecker.t)
     (H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker)
     (H_interpreter : IsInterpreterContextOfType.t locals interpreter type_safety_checker)
+    (H_resolver :
+      resolver.(loader.Resolver.binary).(loader.BinaryType.compiled) =
+      type_safety_checker.(TypeSafetyChecker.module)
+    )
     (* This lemma is not true for [Bytecode.Ret] *)
     (H_not_Ret : instruction <> Bytecode.Ret) :
   let state := {|
@@ -230,7 +222,8 @@ Proof.
   pose proof file_format.SignatureToken.ImplEq.I_is_valid as H_Eq.
   destruct interpreter as [[stack]].
   destruct type_safety_checker as [module function_context locals_ty stack_ty]; cbn in *.
-  destruct H_type_safety_checker as [H_stack_ty]; cbn in *.
+  destruct H_type_safety_checker as [H_module H_stack_ty]; cbn in *.
+  destruct H_module as [H_constant_pool].
   destruct instruction eqn:H_instruction_eq; cbn in *.
   { guard_instruction Bytecode.Pop.
     destruct_abstract_pop.
@@ -329,7 +322,21 @@ Proof.
       sauto lq: on rew: off.
   }
   { guard_instruction (Bytecode.LdConst t).
-    admit.
+    unfold_state_monad.
+    unfold CompiledModule.constant_at.
+    match goal with
+    | |- context[List.nth_error ?l ?i] =>
+      epose proof (List.Forall_nth_error _ l i H_constant_pool)
+    end.
+    destruct List.nth_error as [constant|] eqn:H_nth_error; cbn; try easy.
+    destruct_abstract_push.
+    unfold loader.Resolver.Impl_Resolver.constant_at.
+    rewrite H_resolver.
+    unfold CompiledModule.constant_at; rewrite H_nth_error; cbn.
+    unfold Constant.Valid.t in *.
+    destruct Impl_Value.deserialize_constant as [value|]; cbn; [|easy].
+    step; cbn; try easy.
+    best.
   }
   { guard_instruction Bytecode.LdTrue.
     destruct_abstract_push.

CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v

@@ -0,0 +1,22 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.simulations.M.
+Require Import CoqOfRust.lib.proofs.lib.
+
+Require Import move_sui.simulations.move_binary_format.file_format.
+Require Import move_sui.simulations.move_vm_types.values.values_impl.
+
+Module IsValueOfType.
+  Definition t (value : Value.t) (typ : SignatureToken.t) : Prop :=
+    match value, typ with
+    | ValueImpl.U8 _, SignatureToken.U8 => True
+    | ValueImpl.U16 _, SignatureToken.U16 => True
+    | ValueImpl.U32 _, SignatureToken.U32 => True
+    | ValueImpl.U64 _, SignatureToken.U64 => True
+    | ValueImpl.U128 _, SignatureToken.U128 => True
+    | ValueImpl.U256 _, SignatureToken.U256 => True
+    | ValueImpl.Bool _, SignatureToken.Bool => True
+    | ValueImpl.Address _, SignatureToken.Address => True
+    (* TODO: other cases *)
+    | _, _ => False
+    end.
+End IsValueOfType.

CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v

@@ -606,21 +606,17 @@ Definition execute_instruction
       interpreter.operand_stack.push(val)?
   }
   *)
-  (* NOTE: paused from investigation *)
-  | Bytecode.LdConst idx => execute_instruction_TODO
-    (* let constant := Resolver.Impl_Resolver.constant_at resolver idx in
-    (* TODO: 
-      - resolve mutual dependency issue 
-      - figure out the logic to load a constant *)
-    let val := Value.Impl_Value.deserialize_constant constant in
-    let val := match val with
-    | Some v => v
-    | None => PartialVMError.new StatusCode.VERIFIER_INVARIANT_VIOLATION
-    end in
-    letS!? _ := liftS! State.Lens.interpreter (
-      liftS! Interpreter.Lens.lens_self_stack $ Stack.Impl_Stack.push val) in 
-    returnS! $ Result.Ok InstrRet.Ok *)
-
+  | Bytecode.LdConst idx =>
+    letS! constant := return!toS! $ Resolver.Impl_Resolver.constant_at resolver idx in
+    match Impl_Value.deserialize_constant constant with
+    | None =>
+      returnS! $ Result.Err $
+        PartialVMError.new StatusCode.VERIFIER_INVARIANT_VIOLATION
+    | Some val =>
+      letS!? _ := liftS! State.Lens.interpreter (
+        liftS! Interpreter.Lens.operand_stack $ Stack.Impl_Stack.push val) in
+      returnS! $ Result.Ok InstrRet.Ok
+    end
   (* 
   Bytecode::LdTrue => {
       gas_meter.charge_simple_instr(S::LdTrue)?;

CoqOfRust/move_sui/simulations/move_vm_types/values/values_impl.v

@@ -11,7 +11,7 @@ Module PartialVMError := errors.PartialVMError.
 Require CoqOfRust.move_sui.simulations.move_core_types.vm_status.
 Module StatusCode := vm_status.StatusCode.
 
-Require CoqOfRust.move_sui.simulations.move_binary_format.file_format.
+Require Import CoqOfRust.move_sui.simulations.move_binary_format.file_format.
 
 (* TODO(progress): 
   - Implement `Reference`:
@@ -21,11 +21,6 @@ Require CoqOfRust.move_sui.simulations.move_binary_format.file_format.
     - read_ref
 *)
 
-(* NOTE(STUB): Only implement if necessary *)
-Module Constant.
-  Parameter t : Set.
-End Constant.
-
 Module AccountAddress.
   Parameter t : Set.
 End AccountAddress.
@@ -492,6 +487,18 @@ Module Value.
   Definition coerce_Locals_Container (self : t) : Value.t. Admitted.
 End Value.
 
+Module Impl_Value.
+  (*
+  pub fn deserialize_constant(constant: &Constant) -> Option<Value> {
+      let layout = Self::constant_sig_token_to_layout(&constant.type_)?;
+      Value::simple_deserialize(&constant.data, &layout)
+  }
+  *)
+  (** We keep this function as axiom for now, as its definition would be quite complex and the
+      details are not required for the verification of the type-checker. *)
+  Parameter deserialize_constant : Constant.t -> option Value.t.
+End Impl_Value.
+
 (*
 impl ContainerRef {
     fn read_ref(self) -> PartialVMResult<Value> {