Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Verifying invariant preservation: part 1 #635

Merged
merged 7 commits into from
Dec 11, 2024
Merged

Verifying invariant preservation: part 1 #635

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
3cfe2c8
feat: Add TypeSafetyChecker Module
0xMushow Dec 6, 2024
61dea50
feat: Add verify_instr_is_valid Lemma
0xMushow Dec 6, 2024
bdeb574
feat: Re-order Bytecode instructions
0xMushow Dec 6, 2024
8af60e5
feat: Add all instruction cases - admit. for now
0xMushow Dec 6, 2024
134d69c
draft: Start with LdUX
0xMushow Dec 6, 2024
f357e84
draft: Move further in LdU8
0xMushow Dec 6, 2024
9e338df
feat: clean up code and write LdU8, LdU16, LdU32, LdU64, LdU128, LdU2…
0xMushow Dec 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
298 changes: 292 additions & 6 deletions CoqOfRust/move_sui/proofs/move_bytecode_verifier/type_safety.v
View file
Open in desktop
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
Open in desktop
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
Loading