From aa6cd6bbf290126deb4c3b342d4ac325f2a20d44 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Thu, 19 Dec 2024 22:28:40 +0100 Subject: [PATCH] sui: verify Bytecode.LdConst --- CoqOfRust/lib/proofs/lib.v | 13 +++++ .../proofs/move_binary_format/file_format.v | 28 ++++++++++- .../move_bytecode_verifier/type_safety.v | 47 +++++++++++-------- .../proofs/move_vm_types/values/values_impl.v | 22 +++++++++ .../simulations/move_vm_runtime/interpreter.v | 26 +++++----- .../move_vm_types/values/values_impl.v | 19 +++++--- 6 files changed, 113 insertions(+), 42 deletions(-) create mode 100644 CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v diff --git a/CoqOfRust/lib/proofs/lib.v b/CoqOfRust/lib/proofs/lib.v index 4e53506cb..82bb5adf0 100644 --- a/CoqOfRust/lib/proofs/lib.v +++ b/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. diff --git a/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v b/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v index 9c3efc3da..a1f5a623d 100644 --- a/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v +++ b/CoqOfRust/move_sui/proofs/move_binary_format/file_format.v @@ -1,7 +1,8 @@ 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) : @@ -9,3 +10,28 @@ Module SignatureToken. 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. diff --git a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v b/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v index 6fef3418f..ccd3befff 100644 --- a/CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v +++ b/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. diff --git a/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v b/CoqOfRust/move_sui/proofs/move_vm_types/values/values_impl.v new file mode 100644 index 000000000..255827522 --- /dev/null +++ b/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. diff --git a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v b/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v index 97e54e161..7a7584b98 100644 --- a/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v +++ b/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)?; 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 2cde27cc3..00c6f6fad 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 @@ -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 { + 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 {