Skip to content

Commit

Permalink
Merge pull request #635 from formal-land/guillaume-claret@antoine-jam…
Browse files Browse the repository at this point in the history 
…es@verifying-invariant-preservation

Verifying invariant preservation: part 1
  • Loading branch information
@clarus
clarus authored Dec 11, 2024
2 parents 85b1ca0 + 9e338df commit 457a00a
Show file tree
Hide file tree
Showing 2 changed files with 299 additions and 13 deletions.
298 changes: 292 additions & 6 deletions CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,14 @@ Require Import move_sui.simulations.move_vm_types.values.values_impl.

Import simulations.M.Notations.

Module TypeSafetyChecker.
Module Valid.
Record t (x : TypeSafetyChecker.t) : Prop := {
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
Expand Down Expand Up @@ -57,9 +65,14 @@ Ltac guard_instruction expected_instruction :=
end.

Ltac unfold_state_monad :=
unfold StatePanicResult.bind, StatePanic.bind, StatePanic.bind,
"return!toS!", "liftS!", "readS!";
cbn.
repeat (
unfold StatePanicResult.bind, StatePanic.bind, StatePanic.bind,
"return!toS!",
"liftS!",
"readS!",
"return!toS!?";
cbn
).

Ltac destruct_abstract_push :=
unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push;
Expand Down Expand Up @@ -164,6 +177,12 @@ Proof.
rewrite H_push.
hauto l: on.
}
{ guard_instruction (Bytecode.LdU16 z).
admit.
}
{ guard_instruction (Bytecode.LdU32 z).
admit.
}
{ guard_instruction (Bytecode.LdU64 z).
destruct_abstract_push.
lib.step; cbn; [|exact I].
Expand All @@ -180,6 +199,9 @@ Proof.
rewrite H_push.
hauto l: on.
}
{ guard_instruction (Bytecode.LdU256 z).
admit.
}
{ guard_instruction Bytecode.CastU8.
destruct_abstract_pop H_interpreter.
lib.step; cbn; [exact I|].
Expand All @@ -191,6 +213,12 @@ Proof.
sauto lq: on
).
}
{ guard_instruction Bytecode.CastU16.
admit.
}
{ guard_instruction Bytecode.CastU32.
admit.
}
{ guard_instruction Bytecode.CastU64.
destruct_abstract_pop H_interpreter.
lib.step; cbn; [exact I|].
Expand All @@ -213,6 +241,9 @@ Proof.
sauto lq: on
).
}
{ guard_instruction Bytecode.CastU256.
admit.
}
{ guard_instruction (Bytecode.LdConst t).
admit.
}
Expand Down Expand Up @@ -407,13 +438,82 @@ Proof.
{ guard_instruction (Bytecode.VecSwap t).
admit.
}
{ guard_instruction (Bytecode.LdU16 z).
Admitted.

Lemma verify_instr_is_valid (instruction : Bytecode.t) (pc : Z) (type_safety_checker : TypeSafetyChecker.t)
(H_type_safety_checker : TypeSafetyChecker.Valid.t type_safety_checker) :
match verify_instr instruction pc type_safety_checker with
| Panic.Value (Result.Ok _, type_safety_checker') => TypeSafetyChecker.Valid.t type_safety_checker'
| _ => True
end.
Proof.
destruct instruction eqn:H_instruction; cbn.
{ guard_instruction Bytecode.Pop.
admit.
}
{ guard_instruction (Bytecode.LdU32 z).
{ guard_instruction Bytecode.Ret.
admit.
}
{ guard_instruction (Bytecode.BrTrue z).
admit.
}
{ guard_instruction (Bytecode.BrFalse z).
admit.
}
{ guard_instruction (Bytecode.Branch z).
admit.
}
{ guard_instruction (Bytecode.LdU8 z).
unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
with_strategy opaque [AbstractStack.push] unfold_state_monad.
pose proof (AbstractStack.push_is_valid SignatureToken.U8 type_safety_checker.(TypeSafetyChecker.stack)).
destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
destruct result; cbn; [|trivial].
sauto q: on.
}
{
guard_instruction (Bytecode.LdU16 z).
unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
with_strategy opaque [AbstractStack.push] unfold_state_monad.
pose proof (AbstractStack.push_is_valid SignatureToken.U16 type_safety_checker.(TypeSafetyChecker.stack)).
destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
destruct result; cbn; [|trivial].
sauto q: on.
}
{ guard_instruction (Bytecode.LdU32 z).
unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
with_strategy opaque [AbstractStack.push] unfold_state_monad.
pose proof (AbstractStack.push_is_valid SignatureToken.U32 type_safety_checker.(TypeSafetyChecker.stack)).
destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
destruct result; cbn; [|trivial].
sauto q: on.
}
{ guard_instruction (Bytecode.LdU64 z).
unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
with_strategy opaque [AbstractStack.push] unfold_state_monad.
pose proof (AbstractStack.push_is_valid SignatureToken.U64 type_safety_checker.(TypeSafetyChecker.stack)).
destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
destruct result; cbn; [|trivial].
sauto q: on.
}
{ guard_instruction (Bytecode.LdU128 z).
unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
with_strategy opaque [AbstractStack.push] unfold_state_monad.
pose proof (AbstractStack.push_is_valid SignatureToken.U128 type_safety_checker.(TypeSafetyChecker.stack)).
destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
destruct result; cbn; [|trivial].
sauto q: on.
}
{ guard_instruction (Bytecode.LdU256 z).
unfold TypeSafetyChecker.Impl_TypeSafetyChecker.push.
with_strategy opaque [AbstractStack.push] unfold_state_monad.
pose proof (AbstractStack.push_is_valid SignatureToken.U256 type_safety_checker.(TypeSafetyChecker.stack)).
destruct AbstractStack.push as [[result stack']|]; cbn; [|trivial].
destruct result; cbn; [|trivial].
sauto q: on.
}
{ guard_instruction Bytecode.CastU8.

admit.
}
{ guard_instruction Bytecode.CastU16.
Expand All @@ -422,7 +522,193 @@ Proof.
{ guard_instruction Bytecode.CastU32.
admit.
}
{ guard_instruction Bytecode.CastU64.
admit.
}
{ guard_instruction Bytecode.CastU128.
admit.
}
{ guard_instruction Bytecode.CastU256.
admit.
}
Admitted.
{ guard_instruction (Bytecode.LdConst t).
admit.
}
{ guard_instruction Bytecode.LdTrue.
admit.
}
{ guard_instruction Bytecode.LdFalse.
admit.
}
{ guard_instruction (Bytecode.CopyLoc z).
admit.
}
{ guard_instruction (Bytecode.MoveLoc z).
admit.
}
{ guard_instruction (Bytecode.StLoc z).
admit.
}
{ guard_instruction (Bytecode.Call t).
admit.
}
{ guard_instruction (Bytecode.CallGeneric t).
admit.
}
{ guard_instruction (Bytecode.Pack t).
admit.
}
{ guard_instruction (Bytecode.PackGeneric t).
admit.
}
{ guard_instruction (Bytecode.Unpack t).
admit.
}
{ guard_instruction (Bytecode.UnpackGeneric t).
admit.
}
{ guard_instruction Bytecode.ReadRef.
admit.
}
{ guard_instruction Bytecode.WriteRef.
admit.
}
{ guard_instruction Bytecode.FreezeRef.
admit.
}
{ guard_instruction (Bytecode.MutBorrowLoc z).
admit.
}
{ guard_instruction (Bytecode.ImmBorrowLoc z).
admit.
}
{ guard_instruction (Bytecode.MutBorrowField t).
admit.
}
{ guard_instruction (Bytecode.MutBorrowFieldGeneric t).
admit.
}
{ guard_instruction (Bytecode.ImmBorrowField t).
admit.
}
{ guard_instruction (Bytecode.ImmBorrowFieldGeneric t).
admit.
}
{ guard_instruction (Bytecode.MutBorrowGlobalDeprecated t).
admit.
}
{ guard_instruction (Bytecode.MutBorrowGlobalGenericDeprecated t).
admit.
}
{ guard_instruction (Bytecode.ImmBorrowGlobalDeprecated t).
admit.
}
{ guard_instruction (Bytecode.ImmBorrowGlobalGenericDeprecated t).
admit.
}
{ guard_instruction Bytecode.Add.
admit.
}
{ guard_instruction Bytecode.Sub.
admit.
}
{ guard_instruction Bytecode.Mul.
admit.
}
{ guard_instruction Bytecode.Mod.
admit.
}
{ guard_instruction Bytecode.Div.
admit.
}
{ guard_instruction Bytecode.BitOr.
admit.
}
{ guard_instruction Bytecode.BitAnd.
admit.
}
{ guard_instruction Bytecode.Xor.
admit.
}
{ guard_instruction Bytecode.Or.
admit.
}
{ guard_instruction Bytecode.And.
admit.
}
{ guard_instruction Bytecode.Not.
admit.
}
{ guard_instruction Bytecode.Eq.
admit.
}
{ guard_instruction Bytecode.Neq.
admit.
}
{ guard_instruction Bytecode.Lt.
admit.
}
{ guard_instruction Bytecode.Gt.
admit.
}
{ guard_instruction Bytecode.Le.
admit.
}
{ guard_instruction Bytecode.Ge.
admit.
}
{ guard_instruction Bytecode.Abort.
admit.
}
{ guard_instruction Bytecode.Nop.
admit.
}
{ guard_instruction (Bytecode.ExistsDeprecated t).
admit.
}
{ guard_instruction (Bytecode.ExistsGenericDeprecated t).
admit.
}
{ guard_instruction (Bytecode.MoveFromDeprecated t).
admit.
}
{ guard_instruction (Bytecode.MoveFromGenericDeprecated t).
admit.
}
{ guard_instruction (Bytecode.MoveToDeprecated t).
admit.
}
{ guard_instruction (Bytecode.MoveToGenericDeprecated t).
admit.
}
{ guard_instruction Bytecode.Shl.
admit.
}
{ guard_instruction Bytecode.Shr.
admit.
}
{ guard_instruction (Bytecode.VecPack t z).
admit.
}
{ guard_instruction (Bytecode.VecLen t).
admit.
}
{ guard_instruction (Bytecode.VecImmBorrow t).
admit.
}
{ guard_instruction (Bytecode.VecMutBorrow t).
admit.
}
{ guard_instruction (Bytecode.VecPushBack t).
admit.
}
{ guard_instruction (Bytecode.VecPopBack t).
admit.
}
{ guard_instruction (Bytecode.VecUnpack t z).
admit.
}
{ guard_instruction (Bytecode.VecSwap t).
admit.
}
Admitted.
14 changes: 7 additions & 7 deletions CoqOfRust/move_sui/simulations/move_binary_format/file_format.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -844,11 +844,17 @@ Module Bytecode.
| BrFalse (_ : Z)
| Branch (_ : Z)
| LdU8 (_ : Z)
| LdU16 (_ : Z)
| LdU32 (_ : Z)
| LdU64 (_ : Z)
| LdU128 (_ : Z)
| LdU256 (_ : Z)
| CastU8
| CastU16
| CastU32
| CastU64
| CastU128
| CastU256
| LdConst (_ : ConstantPoolIndex.t)
| LdTrue
| LdFalse
Expand Down Expand Up @@ -908,13 +914,7 @@ Module Bytecode.
| VecPushBack (_ : SignatureIndex.t)
| VecPopBack (_ : SignatureIndex.t)
| VecUnpack (_ : SignatureIndex.t) (_ : Z)
| VecSwap (_ : SignatureIndex.t)
| LdU16 (_ : Z)
| LdU32 (_ : Z)
| LdU256 (_ : Z)
| CastU16
| CastU32
| CastU256.
| VecSwap (_ : SignatureIndex.t).

Definition is_unconditional_branch (self : t) : bool :=
match self with
Expand Down

0 comments on commit 457a00a

Please sign in to comment.