🦏 Sc_rollup_refutation_storage.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_refutation_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_dissection_chunk_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_stake_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Token.
Import Error.Tactics_letP.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_refutation_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_context.
Require TezosOfOCaml.Proto_alpha.Proofs.Receipt_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_commitment_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_dissection_chunk_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_stake_storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Storage.
Require TezosOfOCaml.Proto_alpha.Proofs.Token.
Import Error.Tactics_letP.
Helper tactic to destruct
[(Storage_sigs.Indexed_map.Map
(Raw_context.of_description_index Sc_rollup_repr.Index))
.(S.find) key map] terms. Without [change b a]
Coq will not eliminate the match in the goal
#[local] Ltac destruct_find H :=
match type of H with
| match ?a ?key ?map with _ ⇒ _ end ⇒
match goal with
| |- context [match ?b key map with _ ⇒ _ end] ⇒
change b with a in *; destruct a
end
end.
match type of H with
| match ?a ?key ?map with _ ⇒ _ end ⇒
match goal with
| |- context [match ?b key map with _ ⇒ _ end] ⇒
change b with a in *; destruct a
end
end.
Finds and destruct the last [Raw_context.Valid.t ctxt] hypothesis
#[local] Ltac destruct_last_ctxt :=
match goal with
| H : Raw_context.Valid.t _ |- _ ⇒
Raw_context.Valid.destruct_rewrite H
| H : Raw_context.Valid.on _ _ |- _ ⇒
Raw_context.Valid.destruct_rewrite H
end.
match goal with
| H : Raw_context.Valid.t _ |- _ ⇒
Raw_context.Valid.destruct_rewrite H
| H : Raw_context.Valid.on _ _ |- _ ⇒
Raw_context.Valid.destruct_rewrite H
end.
Finish a goal by applying [Raw_context.on_impl_t]
#[local] Ltac by_Raw_context_on_impl_t :=
match goal with
| H : Raw_context.Valid.on _ (Raw_context.to_t ?sim_ctxt)
|- Raw_context.Valid.t (Raw_context.to_t ?sim_ctxt) ⇒
now apply Raw_context.on_impl_t in H
| H : Raw_context.Valid.on _ ?ctxt
|- Raw_context.Valid.t ?ctxt ⇒
Raw_context.Valid.destruct_rewrite H;
now apply Raw_context.on_impl_t in H
end.
Module point.
Module Valid.
Import Proto_alpha.Sc_rollup_refutation_storage.point.
match goal with
| H : Raw_context.Valid.on _ (Raw_context.to_t ?sim_ctxt)
|- Raw_context.Valid.t (Raw_context.to_t ?sim_ctxt) ⇒
now apply Raw_context.on_impl_t in H
| H : Raw_context.Valid.on _ ?ctxt
|- Raw_context.Valid.t ?ctxt ⇒
Raw_context.Valid.destruct_rewrite H;
now apply Raw_context.on_impl_t in H
end.
Module point.
Module Valid.
Import Proto_alpha.Sc_rollup_refutation_storage.point.
Validity predicate for the type [point].
Record t (x : Sc_rollup_refutation_storage.point) : Prop := {
commitment : Sc_rollup_commitment_repr.V1.Valid.t x.(commitment);
}.
End Valid.
End point.
Module conflict_point.
Module Valid.
commitment : Sc_rollup_commitment_repr.V1.Valid.t x.(commitment);
}.
End Valid.
End point.
Module conflict_point.
Module Valid.
Validity predicate for the type [conflict_point].
Definition t (x : Sc_rollup_refutation_storage.conflict_point)
: Prop :=
point.Valid.t (fst x) ∧ point.Valid.t (snd x).
End Valid.
End conflict_point.
: Prop :=
point.Valid.t (fst x) ∧ point.Valid.t (snd x).
End Valid.
End conflict_point.
The function [initial_timeout] is valid.
Lemma initial_timeout_is_valid ctxt
(H_ctxt : Raw_context.Valid.t ctxt) :
Sc_rollup_game_repr.timeout.Valid.t (
Sc_rollup_refutation_storage.initial_timeout ctxt
).
Proof.
Raw_context.Valid.destruct_rewrite H_ctxt.
split; cbn in *; apply H_sim_ctxt.
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
Sc_rollup_game_repr.timeout.Valid.t (
Sc_rollup_refutation_storage.initial_timeout ctxt
).
Proof.
Raw_context.Valid.destruct_rewrite H_ctxt.
split; cbn in *; apply H_sim_ctxt.
Qed.
The function [update_timeout] is valid.
Lemma update_timeout_is_valid ctxt rollup game idx
(H_ctxt : Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.value_exists
(fun timeout ⇒ Sc_rollup_game_repr.timeout.Valid.t timeout)
rollup idx sim_ctxt.(Raw_context.Sc_rollup_Game_timeout))
ctxt)
(H_game : Sc_rollup_game_repr.V1.Valid.t game)
(H_idx : Sc_rollup_game_repr.Index.Valid.t idx) :
letP? ctxt :=
Sc_rollup_refutation_storage.update_timeout
ctxt rollup game idx in
Raw_context.Valid.t ctxt.
Proof.
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Sc_rollup_refutation_storage.update_timeout.
esplit_letP. {
rewrite Storage_generated.Sc_rollup.Game_timeout.get.
cbn in ×.
do 2 (destruct_find H_sim_ctxt_domain; [|contradiction]).
match type of H_ctxt with
| Raw_context.Valid.on ?domain _ ⇒
instantiate (1 :=
fun '(ctxt, timeout) ⇒
Raw_context.Valid.on domain ctxt ∧
Sc_rollup_game_repr.timeout.Valid.t timeout)
end.
cbn; split; easy.
}
intros [? ?] [? ?].
esplit_letP. {
destruct_last_ctxt.
cbn.
(* The size is the difference in the storage size before and after
the update. The aximatization doesn't take it into account (it receives
as an argument). *)
rewrite Storage_generated.Sc_rollup.Game_timeout.update with (size := 0).
simpl.
match goal with
| _ : match ?a with _ ⇒ _ end |- _ ⇒
match goal with
| |- context [match ?b with _ ⇒ _ end] ⇒
change a with b in × (* I don't know why I need this *)
end
end.
step; [|contradiction].
match goal with
| _ : match ?a with _ ⇒ _ end |- _ ⇒ destruct a eqn:?; [|contradiction]
end.
rename_by_type Sc_rollup_game_repr.timeout into timeout.
rename_by_type (_ = Some timeout) into H_find.
apply Map.find_mem_eq in H_find.
unfold Storage_sigs.Indexed_map.Map.
with_strategy transparent [Map.Make] unfold Map.Make in *; cbn in ×.
rewrite H_find. cbn.
instantiate (1 := fun '(ctxt', size) ⇒ Raw_context.Valid.t ctxt').
apply (Raw_context.f_preserves_context_trivial_validity
ltac:(assumption) Raw_context.Sc_rollup_Game_timeout ltac:(auto)).
by_Raw_context_on_impl_t.
}
intros. step; easy.
Qed.
(H_ctxt : Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.value_exists
(fun timeout ⇒ Sc_rollup_game_repr.timeout.Valid.t timeout)
rollup idx sim_ctxt.(Raw_context.Sc_rollup_Game_timeout))
ctxt)
(H_game : Sc_rollup_game_repr.V1.Valid.t game)
(H_idx : Sc_rollup_game_repr.Index.Valid.t idx) :
letP? ctxt :=
Sc_rollup_refutation_storage.update_timeout
ctxt rollup game idx in
Raw_context.Valid.t ctxt.
Proof.
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Sc_rollup_refutation_storage.update_timeout.
esplit_letP. {
rewrite Storage_generated.Sc_rollup.Game_timeout.get.
cbn in ×.
do 2 (destruct_find H_sim_ctxt_domain; [|contradiction]).
match type of H_ctxt with
| Raw_context.Valid.on ?domain _ ⇒
instantiate (1 :=
fun '(ctxt, timeout) ⇒
Raw_context.Valid.on domain ctxt ∧
Sc_rollup_game_repr.timeout.Valid.t timeout)
end.
cbn; split; easy.
}
intros [? ?] [? ?].
esplit_letP. {
destruct_last_ctxt.
cbn.
(* The size is the difference in the storage size before and after
the update. The aximatization doesn't take it into account (it receives
as an argument). *)
rewrite Storage_generated.Sc_rollup.Game_timeout.update with (size := 0).
simpl.
match goal with
| _ : match ?a with _ ⇒ _ end |- _ ⇒
match goal with
| |- context [match ?b with _ ⇒ _ end] ⇒
change a with b in × (* I don't know why I need this *)
end
end.
step; [|contradiction].
match goal with
| _ : match ?a with _ ⇒ _ end |- _ ⇒ destruct a eqn:?; [|contradiction]
end.
rename_by_type Sc_rollup_game_repr.timeout into timeout.
rename_by_type (_ = Some timeout) into H_find.
apply Map.find_mem_eq in H_find.
unfold Storage_sigs.Indexed_map.Map.
with_strategy transparent [Map.Make] unfold Map.Make in *; cbn in ×.
rewrite H_find. cbn.
instantiate (1 := fun '(ctxt', size) ⇒ Raw_context.Valid.t ctxt').
apply (Raw_context.f_preserves_context_trivial_validity
ltac:(assumption) Raw_context.Sc_rollup_Game_timeout ltac:(auto)).
by_Raw_context_on_impl_t.
}
intros. step; easy.
Qed.
The function [get_ongoing_game] is valid.
Lemma get_ongoing_game_is_valid ctxt rollup staker1 staker2
(ctxt_domain := (fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.key_exists
rollup (Sc_rollup_game_repr.Index.make staker1 staker2)
sim_ctxt.(Raw_context.Sc_rollup_Game)))
(H_ctxt : Raw_context.Valid.on ctxt_domain ctxt) :
letP? '(answer, ctxt) :=
Sc_rollup_refutation_storage.get_ongoing_game
ctxt rollup staker1 staker2 in
Option.Forall
(fun '(game, idx) ⇒
Sc_rollup_game_repr.V1.Valid.t game ∧
Sc_rollup_game_repr.Index.Valid.t idx)
answer ∧
Raw_context.Valid.t ctxt.
Proof.
subst ctxt_domain.
assert (H_game_is_valid :
Raw_context.Valid.on
(fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.V1.Valid.t
rollup
(Sc_rollup_game_repr.Index.make staker1 staker2)
sim_ctxt.(Raw_context.Sc_rollup_Game)) ctxt).
{ Raw_context.Valid.destruct_rewrite H_ctxt.
red. ∃ sim_ctxt. split_conj; try easy.
set (index := Sc_rollup_game_repr.Index.make _ _).
destruct H_sim_ctxt.
red in Sc_rollup_Game.
specialize (Sc_rollup_Game rollup index).
now apply Raw_context
.Nested_indexed_data_storage
.key_exists_and_if_value_exists_impl_value_exists.
}
unfold Sc_rollup_refutation_storage.get_ongoing_game.
clear H_ctxt. rename H_game_is_valid into H_ctxt.
esplit_letP. {
destruct_last_ctxt.
rewrite Storage_generated.Sc_rollup.Game.find. cbn.
unshelve instantiate (1 :=
fun '(ctxt, game) ⇒ Raw_context.Valid.t ctxt ∧ _ game).
{ refine (fun game ⇒
Option.Forall
(fun '(game, idx) ⇒
Sc_rollup_game_repr.V1.Valid.t game ∧
Sc_rollup_game_repr.Index.Valid.t idx)
(Option.map
(fun game : Sc_rollup_game_repr.V1.t ⇒
(game,
Sc_rollup_game_repr.Index.make staker1 staker2))
game)).
}
cbn. split; [by_Raw_context_on_impl_t|].
cbn in ×. unfold Option.bind.
do 2 (destruct_find H_sim_ctxt_domain; [|contradiction]).
split; [easy|].
apply Sc_rollup_game_repr.make_is_valid.
}
intros [ctxt' opt_game] [H_valid_ctxt H_opt_game]; cbn.
now split.
Qed.
Module game_exists.
(ctxt_domain := (fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.key_exists
rollup (Sc_rollup_game_repr.Index.make staker1 staker2)
sim_ctxt.(Raw_context.Sc_rollup_Game)))
(H_ctxt : Raw_context.Valid.on ctxt_domain ctxt) :
letP? '(answer, ctxt) :=
Sc_rollup_refutation_storage.get_ongoing_game
ctxt rollup staker1 staker2 in
Option.Forall
(fun '(game, idx) ⇒
Sc_rollup_game_repr.V1.Valid.t game ∧
Sc_rollup_game_repr.Index.Valid.t idx)
answer ∧
Raw_context.Valid.t ctxt.
Proof.
subst ctxt_domain.
assert (H_game_is_valid :
Raw_context.Valid.on
(fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.V1.Valid.t
rollup
(Sc_rollup_game_repr.Index.make staker1 staker2)
sim_ctxt.(Raw_context.Sc_rollup_Game)) ctxt).
{ Raw_context.Valid.destruct_rewrite H_ctxt.
red. ∃ sim_ctxt. split_conj; try easy.
set (index := Sc_rollup_game_repr.Index.make _ _).
destruct H_sim_ctxt.
red in Sc_rollup_Game.
specialize (Sc_rollup_Game rollup index).
now apply Raw_context
.Nested_indexed_data_storage
.key_exists_and_if_value_exists_impl_value_exists.
}
unfold Sc_rollup_refutation_storage.get_ongoing_game.
clear H_ctxt. rename H_game_is_valid into H_ctxt.
esplit_letP. {
destruct_last_ctxt.
rewrite Storage_generated.Sc_rollup.Game.find. cbn.
unshelve instantiate (1 :=
fun '(ctxt, game) ⇒ Raw_context.Valid.t ctxt ∧ _ game).
{ refine (fun game ⇒
Option.Forall
(fun '(game, idx) ⇒
Sc_rollup_game_repr.V1.Valid.t game ∧
Sc_rollup_game_repr.Index.Valid.t idx)
(Option.map
(fun game : Sc_rollup_game_repr.V1.t ⇒
(game,
Sc_rollup_game_repr.Index.make staker1 staker2))
game)).
}
cbn. split; [by_Raw_context_on_impl_t|].
cbn in ×. unfold Option.bind.
do 2 (destruct_find H_sim_ctxt_domain; [|contradiction]).
split; [easy|].
apply Sc_rollup_game_repr.make_is_valid.
}
intros [ctxt' opt_game] [H_valid_ctxt H_opt_game]; cbn.
now split.
Qed.
Module game_exists.
A game exists betwwen the player [staker] and its
opponent, regarding the address [rollup]
Definition t (sim_ctxt : Raw_context.t)
(rollup : Sc_rollup_repr.Address.t) (staker : public_key_hash)
: Prop :=
Raw_context.Nested_indexed_data_storage.value_exists
(fun opponent ⇒
Raw_context.Nested_indexed_data_storage.key_exists
rollup
(Sc_rollup_game_repr.Index.make staker opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game))
rollup staker sim_ctxt.(Raw_context.Sc_rollup_Opponent).
End game_exists.
(rollup : Sc_rollup_repr.Address.t) (staker : public_key_hash)
: Prop :=
Raw_context.Nested_indexed_data_storage.value_exists
(fun opponent ⇒
Raw_context.Nested_indexed_data_storage.key_exists
rollup
(Sc_rollup_game_repr.Index.make staker opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game))
rollup staker sim_ctxt.(Raw_context.Sc_rollup_Opponent).
End game_exists.
The function [get_ongoing_game_for_staker] is valid.
Lemma get_ongoing_game_for_staker_is_valid ctxt rollup staker
(H_ctxt :
Raw_context.Valid.on
(fun sim_ctxt ⇒ game_exists.t sim_ctxt rollup staker)
ctxt) :
letP? '(answer, ctxt) :=
Sc_rollup_refutation_storage.get_ongoing_game_for_staker
ctxt rollup staker in
Option.Forall
(fun '(game, idx) ⇒
Sc_rollup_game_repr.V1.Valid.t game ∧
Sc_rollup_game_repr.Index.Valid.t idx)
answer ∧
Raw_context.Valid.t ctxt.
Proof.
unfold
Sc_rollup_refutation_storage.get_ongoing_game_for_staker,
game_exists.t in ×.
destruct_last_ctxt.
rewrite_db storage_db. simpl.
cbn in H_sim_ctxt_domain. unfold Option.bind.
do 2 (destruct_find H_sim_ctxt_domain; [|contradiction]).
pose proof get_ongoing_game_is_valid (Raw_context.to_t sim_ctxt)
rollup staker p as H_game.
cbn zeta in H_game.
apply H_game.
match type of H_ctxt with
| Raw_context.Valid.on ?domain _ ⇒ set (domain1 := domain)
end.
match goal with
| |- Raw_context.Valid.on ?domain _ ⇒ set (domain2 := domain)
end.
assert (H_impl : domain1 sim_ctxt → domain2 sim_ctxt).
{ intros. subst domain1 domain2. simpl in ×.
dtauto.
}
now apply (Raw_context.domain_impl_sim_ctxt domain1 domain2
sim_ctxt).
Qed.
(H_ctxt :
Raw_context.Valid.on
(fun sim_ctxt ⇒ game_exists.t sim_ctxt rollup staker)
ctxt) :
letP? '(answer, ctxt) :=
Sc_rollup_refutation_storage.get_ongoing_game_for_staker
ctxt rollup staker in
Option.Forall
(fun '(game, idx) ⇒
Sc_rollup_game_repr.V1.Valid.t game ∧
Sc_rollup_game_repr.Index.Valid.t idx)
answer ∧
Raw_context.Valid.t ctxt.
Proof.
unfold
Sc_rollup_refutation_storage.get_ongoing_game_for_staker,
game_exists.t in ×.
destruct_last_ctxt.
rewrite_db storage_db. simpl.
cbn in H_sim_ctxt_domain. unfold Option.bind.
do 2 (destruct_find H_sim_ctxt_domain; [|contradiction]).
pose proof get_ongoing_game_is_valid (Raw_context.to_t sim_ctxt)
rollup staker p as H_game.
cbn zeta in H_game.
apply H_game.
match type of H_ctxt with
| Raw_context.Valid.on ?domain _ ⇒ set (domain1 := domain)
end.
match goal with
| |- Raw_context.Valid.on ?domain _ ⇒ set (domain2 := domain)
end.
assert (H_impl : domain1 sim_ctxt → domain2 sim_ctxt).
{ intros. subst domain1 domain2. simpl in ×.
dtauto.
}
now apply (Raw_context.domain_impl_sim_ctxt domain1 domain2
sim_ctxt).
Qed.
The function [goto_inbox_level] is valid.
Lemma goto_inbox_level_is_valid ctxt rollup inbox_level commit
(H_ctxt : Raw_context.Valid.t ctxt)
(H_level : Raw_level_repr.Valid.t inbox_level) :
letP? '(_, ctxt) :=
Sc_rollup_refutation_storage.goto_inbox_level
ctxt rollup inbox_level commit in
Raw_context.Valid.t ctxt.
Proof.
intros.
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Sc_rollup_refutation_storage.goto_inbox_level.
(* Here we have a go closure which iterate over the commits in the
storage
In pseudocode
{[
let rec go ctxt commit =
let (info, ctxt') = read_commitment_from_the_storage
ctxt commit in
if info.inbox_level <= inbox_level
then
if info.inbox_level = inbox_level
then return? (commit, ctxt')
else assert false
else
go ctxt' info.predecessor
]}
It should finish assuming that the precessors level [in the
storage] are always lesser than the current commit levels, and
that all levels stop a 0 [genesis]
*)
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt)
(H_level : Raw_level_repr.Valid.t inbox_level) :
letP? '(_, ctxt) :=
Sc_rollup_refutation_storage.goto_inbox_level
ctxt rollup inbox_level commit in
Raw_context.Valid.t ctxt.
Proof.
intros.
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Sc_rollup_refutation_storage.goto_inbox_level.
(* Here we have a go closure which iterate over the commits in the
storage
In pseudocode
{[
let rec go ctxt commit =
let (info, ctxt') = read_commitment_from_the_storage
ctxt commit in
if info.inbox_level <= inbox_level
then
if info.inbox_level = inbox_level
then return? (commit, ctxt')
else assert false
else
go ctxt' info.predecessor
]}
It should finish assuming that the precessors level [in the
storage] are always lesser than the current commit levels, and
that all levels stop a 0 [genesis]
*)
Admitted.
The function [get_conflict_point] is valid.
Lemma get_conflict_point_is_valid ctxt rollup staker1 staker2
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(conflict, ctxt) :=
Sc_rollup_refutation_storage.get_conflict_point
ctxt rollup staker1 staker2 in
conflict_point.Valid.t conflict ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_refutation_storage.get_conflict_point.
(* Here we have another recursive function that Coq can't
check for termination *)
Admitted.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(conflict, ctxt) :=
Sc_rollup_refutation_storage.get_conflict_point
ctxt rollup staker1 staker2 in
conflict_point.Valid.t conflict ∧
Raw_context.Valid.t ctxt.
Proof.
unfold Sc_rollup_refutation_storage.get_conflict_point.
(* Here we have another recursive function that Coq can't
check for termination *)
Admitted.
The function [get_game] is valid.
Lemma get_game_is_valid ctxt rollup stakers
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(game, ctxt') :=
Sc_rollup_refutation_storage.get_game ctxt rollup stakers in
Sc_rollup_game_repr.V1.Valid.t game ∧
let ctxt_domain' sim_ctxt :=
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.V1.Valid.t rollup stakers
sim_ctxt.(Raw_context.Sc_rollup_Game) in
Raw_context.Valid.on ctxt_domain' ctxt'.
Proof.
unfold Sc_rollup_refutation_storage.get_game.
Raw_context.Valid.destruct_rewrite H_ctxt.
inversion H_sim_ctxt.
red in Sc_rollup_Game.
specialize (Sc_rollup_Game rollup stakers).
rewrite_db storage_db. cbn in ×.
unfold Option.bind.
match type of Sc_rollup_Game with
| match ?a with _ ⇒ _ end ⇒
match goal with
| |- context [match ?b with _ ⇒ _ end] ⇒
change b with a; destruct a eqn:H_find1; cbn in ×
end
end; [|reflexivity].
match type of Sc_rollup_Game with
| match ?a with _ ⇒ _ end ⇒ destruct a eqn:H_find2; cbn in ×
end; [|reflexivity..].
split; [assumption|].
unfold Raw_context.Valid.on.
∃ sim_ctxt. split_conj; [easy|easy|].
match type of H_find1 with
| ?a rollup _ = _ ⇒
match goal with
| |- context [match ?b rollup _ with _ ⇒ _ end] ⇒
change b with a; rewrite H_find1
end
end.
match type of H_find2 with
| ?a stakers _ = _ ⇒
match goal with
| |- context [match ?b stakers _ with _ ⇒ _ end] ⇒
change b with a; rewrite H_find2
end
end.
easy.
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(game, ctxt') :=
Sc_rollup_refutation_storage.get_game ctxt rollup stakers in
Sc_rollup_game_repr.V1.Valid.t game ∧
let ctxt_domain' sim_ctxt :=
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.V1.Valid.t rollup stakers
sim_ctxt.(Raw_context.Sc_rollup_Game) in
Raw_context.Valid.on ctxt_domain' ctxt'.
Proof.
unfold Sc_rollup_refutation_storage.get_game.
Raw_context.Valid.destruct_rewrite H_ctxt.
inversion H_sim_ctxt.
red in Sc_rollup_Game.
specialize (Sc_rollup_Game rollup stakers).
rewrite_db storage_db. cbn in ×.
unfold Option.bind.
match type of Sc_rollup_Game with
| match ?a with _ ⇒ _ end ⇒
match goal with
| |- context [match ?b with _ ⇒ _ end] ⇒
change b with a; destruct a eqn:H_find1; cbn in ×
end
end; [|reflexivity].
match type of Sc_rollup_Game with
| match ?a with _ ⇒ _ end ⇒ destruct a eqn:H_find2; cbn in ×
end; [|reflexivity..].
split; [assumption|].
unfold Raw_context.Valid.on.
∃ sim_ctxt. split_conj; [easy|easy|].
match type of H_find1 with
| ?a rollup _ = _ ⇒
match goal with
| |- context [match ?b rollup _ with _ ⇒ _ end] ⇒
change b with a; rewrite H_find1
end
end.
match type of H_find2 with
| ?a stakers _ = _ ⇒
match goal with
| |- context [match ?b stakers _ with _ ⇒ _ end] ⇒
change b with a; rewrite H_find2
end
end.
easy.
Qed.
The function [get_game] preserves all context properties
Lemma get_game_preserves_domain ctxt rollup index domain
(H_ctxt : Raw_context.Valid.on domain ctxt) :
letP? '(game, ctxt') := Sc_rollup_refutation_storage.get_game
ctxt rollup index in
Raw_context.Valid.on domain ctxt'.
Proof.
unfold Sc_rollup_refutation_storage.get_game.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db.
simpl.
step; [|easy].
simpl. scongruence.
Qed.
(H_ctxt : Raw_context.Valid.on domain ctxt) :
letP? '(game, ctxt') := Sc_rollup_refutation_storage.get_game
ctxt rollup index in
Raw_context.Valid.on domain ctxt'.
Proof.
unfold Sc_rollup_refutation_storage.get_game.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db.
simpl.
step; [|easy].
simpl. scongruence.
Qed.
The function [start_game] is valid.
Lemma start_game_is_valid ctxt rollup refuter defender
(ctxt_domain := (fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.value_exists
(fun _ ⇒ True)
rollup
defender
sim_ctxt.(Raw_context.Sc_rollup_Opponent)
))
(H_ctxt : Raw_context.Valid.on ctxt_domain ctxt) :
letP? ctxt :=
Sc_rollup_refutation_storage.start_game
ctxt rollup refuter defender in
Raw_context.Valid.t ctxt.
Proof.
subst ctxt_domain.
unfold Sc_rollup_refutation_storage.start_game.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db. cbn.
step; cbn; unfold fail_when; [step; cbn; try reflexivity|];
do 2 (rewrite_db storage_db; simpl);
simpl in *;
step; simpl;
match type of H_sim_ctxt_domain with
| match ?a with _ ⇒ _ end ⇒
match goal with
| |- context [let× _ := ?b in _] ⇒
change b with a; destruct a; simpl; [|contradiction]
end
end;
match goal with
| |- context [let× _ := ?a in _] ⇒
destruct a; simpl; [|contradiction]
end; reflexivity.
Qed.
(ctxt_domain := (fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage.value_exists
(fun _ ⇒ True)
rollup
defender
sim_ctxt.(Raw_context.Sc_rollup_Opponent)
))
(H_ctxt : Raw_context.Valid.on ctxt_domain ctxt) :
letP? ctxt :=
Sc_rollup_refutation_storage.start_game
ctxt rollup refuter defender in
Raw_context.Valid.t ctxt.
Proof.
subst ctxt_domain.
unfold Sc_rollup_refutation_storage.start_game.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db. cbn.
step; cbn; unfold fail_when; [step; cbn; try reflexivity|];
do 2 (rewrite_db storage_db; simpl);
simpl in *;
step; simpl;
match type of H_sim_ctxt_domain with
| match ?a with _ ⇒ _ end ⇒
match goal with
| |- context [let× _ := ?b in _] ⇒
change b with a; destruct a; simpl; [|contradiction]
end
end;
match goal with
| |- context [let× _ := ?a in _] ⇒
destruct a; simpl; [|contradiction]
end; reflexivity.
Qed.
The function [get_metadata] is valid
Lemma get_metadata_is_valid ctxt rollup :
Raw_context.Valid.t ctxt →
letP? '(ctxt', metadata) :=
Sc_rollup_storage.get_metadata ctxt rollup in
Raw_context.Valid.t ctxt'.
Proof.
intros H_ctxt. unfold Sc_rollup_storage.get_metadata,
Sc_rollup_storage.genesis_info.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db. simpl.
now step.
Qed.
Raw_context.Valid.t ctxt →
letP? '(ctxt', metadata) :=
Sc_rollup_storage.get_metadata ctxt rollup in
Raw_context.Valid.t ctxt'.
Proof.
intros H_ctxt. unfold Sc_rollup_storage.get_metadata,
Sc_rollup_storage.genesis_info.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db. simpl.
now step.
Qed.
The function [get_metadata] is read only
Lemma get_metadata_is_ready_only ctxt domain rollup :
Raw_context.Valid.on domain ctxt →
letP? '(ctxt', metadata) := Sc_rollup_storage.get_metadata ctxt rollup in
Raw_context.Valid.on domain ctxt'.
Proof.
intros H_ctxt.
unfold Sc_rollup_storage.get_metadata,
Sc_rollup_storage.genesis_info.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db.
simpl. step; simpl in *; [|reflexivity].
easy.
Qed.
Raw_context.Valid.on domain ctxt →
letP? '(ctxt', metadata) := Sc_rollup_storage.get_metadata ctxt rollup in
Raw_context.Valid.on domain ctxt'.
Proof.
intros H_ctxt.
unfold Sc_rollup_storage.get_metadata,
Sc_rollup_storage.genesis_info.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db.
simpl. step; simpl in *; [|reflexivity].
easy.
Qed.
The function [game_move] is valid.
Lemma game_move_is_valid ctxt rollup player_value opponent refutation
(ctxt_domain := (fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.key_exists
rollup
(Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game) ∧
Raw_context.Nested_indexed_data_storage.key_exists
rollup (Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout)
))
(H_ctxt : Raw_context.Valid.on ctxt_domain ctxt)
(H_refutation :
Sc_rollup_game_repr.refutation.Valid.t refutation) :
letP? '(outcome, ctxt) :=
Sc_rollup_refutation_storage.game_move
ctxt rollup player_value opponent refutation in
Raw_context.Valid.t ctxt.
Proof.
subst ctxt_domain.
assert (H_ctxt' :
Raw_context.Valid.on
(fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.V1.Valid.t
rollup
(Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game) ∧
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.timeout.Valid.t
rollup
(Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout)) ctxt).
{ Raw_context.Valid.destruct_rewrite H_ctxt.
red. ∃ sim_ctxt. split_conj; try easy;
destruct H_sim_ctxt;
red in Sc_rollup_Game;
red in Sc_rollup_Game_timeout;
set (index := (Sc_rollup_game_repr.Index.make _ _));
specialize (Sc_rollup_Game rollup index);
specialize (Sc_rollup_Game_timeout rollup index);
now apply Raw_context
.Nested_indexed_data_storage
.key_exists_and_if_value_exists_impl_value_exists.
} clear H_ctxt. rename H_ctxt' into H_ctxt.
unfold Sc_rollup_refutation_storage.game_move.
set (index := Sc_rollup_game_repr.Index.make _ _).
match type of H_ctxt with
| Raw_context.Valid.on ?domain _ ⇒
pose proof get_game_preserves_domain ctxt rollup index domain
H_ctxt
as H_get_game_presv_domain;
pose proof get_game_is_valid ctxt rollup index
as H_get_game_is_valid
end.
cbn zeta in H_get_game_is_valid.
match type of H_get_game_is_valid with
| ?premisse → _ ⇒
assert (Htmp : premisse)
end; [by_Raw_context_on_impl_t|].
specialize (H_get_game_is_valid Htmp). clear Htmp.
ez destruct (Sc_rollup_refutation_storage.get_game _ _).
destruct p as [game ctxt'].
cbn - [Raw_context.Nested_indexed_data_storage.value_exists] in ×.
unfold fail_unless. step; cbn; [|reflexivity].
esplit_letP. {
match type of H_ctxt with
| Raw_context.Valid.on ?domain' _ ⇒
now apply get_metadata_is_ready_only with (domain := domain')
end.
}
clear ctxt H_ctxt.
intros [ctxt metadata] H_ctxt.
esplit_letP. {
do 2 step; simpl in *; try reflexivity; remaining_goals 3.
{ esplit_letP. {
apply Sc_rollup_game_repr.find_choice_is_valid.
} intros [chunk1 chunk2] H_chunk.
esplit_letP. {
apply Sc_rollup_dissection_chunk_repr.default_check_is_valid.
} intros _ _. simpl.
now instantiate (1 := fun _ ⇒ True).
}
{ esplit_letP. {
apply Sc_rollup_game_repr.find_choice_is_valid.
} intros [chunk1 chunk2] H_chunk.
step; easy.
}
{ step; easy. }
}
intros either_game_result P_game_result.
step; simpl; [now apply Raw_context.on_impl_t in H_ctxt|].
esplit_letP. {
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite Storage_generated.Sc_rollup.Game.update with (size := 0).
simpl in ×.
destruct H_sim_ctxt_domain as [H_game H_timeout].
match type of H_game with
| match ?a with _ ⇒ _ end ⇒
match goal with
| |- context [match ?b with _ ⇒ _ end] ⇒
change b with a; destruct a; [|contradiction]
end
end.
match type of H_game with
| match ?a with _ ⇒ _ end ⇒ destruct a eqn:H_domain_eq
end; [|contradiction].
apply Map.find_mem_eq in H_domain_eq.
match type of H_domain_eq with
| ?a = true ⇒
match goal with
| |- context [if ?b then _ else _] ⇒
change b with a; rewrite H_domain_eq; simpl
end
end.
instantiate (1 := fun '(ctxt, _) ⇒
Raw_context.Valid.on
(fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.value_exists
(fun timeout : Sc_rollup_game_repr.timeout ⇒
Sc_rollup_game_repr.timeout.Valid.t timeout)
rollup
(Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout))
ctxt).
cbn beta zeta.
match goal with
| |- let ' _ := ?pair in _ ⇒
destruct pair eqn:?
end.
rename_by_type ((Raw_context.to_t _, _) = (_, _)) into H_pair.
injection H_pair as Hinj. subst.
unfold Raw_context.Valid.on.
∃ sim_ctxt. split_conj; [easy..|].
cbn.
easy.
}
clear dependent ctxt.
intros [ctxt _] H_valid_ctxt.
esplit_letP. {
apply update_timeout_is_valid.
{ easy. }
{ easy. }
{ apply Sc_rollup_game_repr.make_is_valid. }
}
easy.
Qed.
(ctxt_domain := (fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.key_exists
rollup
(Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game) ∧
Raw_context.Nested_indexed_data_storage.key_exists
rollup (Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout)
))
(H_ctxt : Raw_context.Valid.on ctxt_domain ctxt)
(H_refutation :
Sc_rollup_game_repr.refutation.Valid.t refutation) :
letP? '(outcome, ctxt) :=
Sc_rollup_refutation_storage.game_move
ctxt rollup player_value opponent refutation in
Raw_context.Valid.t ctxt.
Proof.
subst ctxt_domain.
assert (H_ctxt' :
Raw_context.Valid.on
(fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.V1.Valid.t
rollup
(Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game) ∧
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.timeout.Valid.t
rollup
(Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout)) ctxt).
{ Raw_context.Valid.destruct_rewrite H_ctxt.
red. ∃ sim_ctxt. split_conj; try easy;
destruct H_sim_ctxt;
red in Sc_rollup_Game;
red in Sc_rollup_Game_timeout;
set (index := (Sc_rollup_game_repr.Index.make _ _));
specialize (Sc_rollup_Game rollup index);
specialize (Sc_rollup_Game_timeout rollup index);
now apply Raw_context
.Nested_indexed_data_storage
.key_exists_and_if_value_exists_impl_value_exists.
} clear H_ctxt. rename H_ctxt' into H_ctxt.
unfold Sc_rollup_refutation_storage.game_move.
set (index := Sc_rollup_game_repr.Index.make _ _).
match type of H_ctxt with
| Raw_context.Valid.on ?domain _ ⇒
pose proof get_game_preserves_domain ctxt rollup index domain
H_ctxt
as H_get_game_presv_domain;
pose proof get_game_is_valid ctxt rollup index
as H_get_game_is_valid
end.
cbn zeta in H_get_game_is_valid.
match type of H_get_game_is_valid with
| ?premisse → _ ⇒
assert (Htmp : premisse)
end; [by_Raw_context_on_impl_t|].
specialize (H_get_game_is_valid Htmp). clear Htmp.
ez destruct (Sc_rollup_refutation_storage.get_game _ _).
destruct p as [game ctxt'].
cbn - [Raw_context.Nested_indexed_data_storage.value_exists] in ×.
unfold fail_unless. step; cbn; [|reflexivity].
esplit_letP. {
match type of H_ctxt with
| Raw_context.Valid.on ?domain' _ ⇒
now apply get_metadata_is_ready_only with (domain := domain')
end.
}
clear ctxt H_ctxt.
intros [ctxt metadata] H_ctxt.
esplit_letP. {
do 2 step; simpl in *; try reflexivity; remaining_goals 3.
{ esplit_letP. {
apply Sc_rollup_game_repr.find_choice_is_valid.
} intros [chunk1 chunk2] H_chunk.
esplit_letP. {
apply Sc_rollup_dissection_chunk_repr.default_check_is_valid.
} intros _ _. simpl.
now instantiate (1 := fun _ ⇒ True).
}
{ esplit_letP. {
apply Sc_rollup_game_repr.find_choice_is_valid.
} intros [chunk1 chunk2] H_chunk.
step; easy.
}
{ step; easy. }
}
intros either_game_result P_game_result.
step; simpl; [now apply Raw_context.on_impl_t in H_ctxt|].
esplit_letP. {
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite Storage_generated.Sc_rollup.Game.update with (size := 0).
simpl in ×.
destruct H_sim_ctxt_domain as [H_game H_timeout].
match type of H_game with
| match ?a with _ ⇒ _ end ⇒
match goal with
| |- context [match ?b with _ ⇒ _ end] ⇒
change b with a; destruct a; [|contradiction]
end
end.
match type of H_game with
| match ?a with _ ⇒ _ end ⇒ destruct a eqn:H_domain_eq
end; [|contradiction].
apply Map.find_mem_eq in H_domain_eq.
match type of H_domain_eq with
| ?a = true ⇒
match goal with
| |- context [if ?b then _ else _] ⇒
change b with a; rewrite H_domain_eq; simpl
end
end.
instantiate (1 := fun '(ctxt, _) ⇒
Raw_context.Valid.on
(fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.value_exists
(fun timeout : Sc_rollup_game_repr.timeout ⇒
Sc_rollup_game_repr.timeout.Valid.t timeout)
rollup
(Sc_rollup_game_repr.Index.make player_value opponent)
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout))
ctxt).
cbn beta zeta.
match goal with
| |- let ' _ := ?pair in _ ⇒
destruct pair eqn:?
end.
rename_by_type ((Raw_context.to_t _, _) = (_, _)) into H_pair.
injection H_pair as Hinj. subst.
unfold Raw_context.Valid.on.
∃ sim_ctxt. split_conj; [easy..|].
cbn.
easy.
}
clear dependent ctxt.
intros [ctxt _] H_valid_ctxt.
esplit_letP. {
apply update_timeout_is_valid.
{ easy. }
{ easy. }
{ apply Sc_rollup_game_repr.make_is_valid. }
}
easy.
Qed.
The function [get_timeout] is valid.
Lemma get_timeout_is_valid ctxt rollup stakers
(H_ctxt : Raw_context.Valid.t ctxt)
(H_index : Sc_rollup_game_repr.Index.Valid.t stakers) :
letP? '(timeout, ctxt) :=
Sc_rollup_refutation_storage.get_timeout ctxt rollup stakers in
Sc_rollup_game_repr.timeout.Valid.t timeout ∧
Raw_context.Valid.t ctxt.
Proof.
Raw_context.Valid.destruct_rewrite H_ctxt.
destruct H_sim_ctxt.
red in Sc_rollup_Game_timeout.
specialize (Sc_rollup_Game_timeout rollup stakers).
unfold Sc_rollup_refutation_storage.get_timeout.
rewrite_db storage_db. simpl in ×.
unfold Option.bind.
do 2 match goal with
| |- context [match ?a _ _ with _ ⇒ _ end] ⇒
destruct a; [|reflexivity]
end. simpl. now split.
Qed.
(H_ctxt : Raw_context.Valid.t ctxt)
(H_index : Sc_rollup_game_repr.Index.Valid.t stakers) :
letP? '(timeout, ctxt) :=
Sc_rollup_refutation_storage.get_timeout ctxt rollup stakers in
Sc_rollup_game_repr.timeout.Valid.t timeout ∧
Raw_context.Valid.t ctxt.
Proof.
Raw_context.Valid.destruct_rewrite H_ctxt.
destruct H_sim_ctxt.
red in Sc_rollup_Game_timeout.
specialize (Sc_rollup_Game_timeout rollup stakers).
unfold Sc_rollup_refutation_storage.get_timeout.
rewrite_db storage_db. simpl in ×.
unfold Option.bind.
do 2 match goal with
| |- context [match ?a _ _ with _ ⇒ _ end] ⇒
destruct a; [|reflexivity]
end. simpl. now split.
Qed.
The function [timeout] is valid.
Lemma timeout_is_valid ctxt rollup stakers
(H_ctxt : Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage
.key_exists
rollup stakers sim_ctxt.(Raw_context.Sc_rollup_Game_timeout))
ctxt)
(H_index : Sc_rollup_game_repr.Index.Valid.t stakers) :
letP? '(outcome, ctxt) :=
Sc_rollup_refutation_storage.timeout ctxt rollup stakers in
Raw_context.Valid.t ctxt.
Proof.
Raw_context.Valid.destruct_rewrite H_ctxt.
destruct H_sim_ctxt.
red in Sc_rollup_Game_timeout.
specialize (Sc_rollup_Game_timeout rollup stakers).
unfold Sc_rollup_refutation_storage.timeout.
unshelve match type of H_ctxt with
| Raw_context.Valid.on ?domain _ ⇒
pose proof get_game_preserves_domain _ rollup stakers
domain H_ctxt as H_game_presv;
pose proof get_game_is_valid (Raw_context.to_t sim_ctxt)
rollup stakers
ltac:(now apply Raw_context.on_impl_t in H_ctxt)
as H_game_is_valid
end.
ez destruct (Sc_rollup_refutation_storage.get_game _ _ _) as [p|].
destruct p as [game ctxt'].
clear dependent ctxt.
rename ctxt' into ctxt.
assert (H_ctxt' :
Raw_context.Valid.on
(fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.timeout.Valid.t
rollup stakers
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout) ∧
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.V1.Valid.t
rollup stakers sim_ctxt.(Raw_context.Sc_rollup_Game))
ctxt).
{ cbn - [
Raw_context.Nested_indexed_data_storage.value_exists
Raw_context.Nested_indexed_data_storage.key_exists] in ×.
destruct H_game_is_valid as [H_game_is_valid H_ctxt_game_value_exists].
unshelve epose proof Raw_context.key_exists_impl_value_exists
rollup stakers ctxt Sc_rollup_game_repr.timeout.Valid.t
H_game_presv _
as H_ctxt_game_timeout_if_exists.
{ Raw_context.Valid.destruct_rewrite H_game_presv.
inversion H_sim_ctxt.
red in Sc_rollup_Game_timeout0.
specialize (Sc_rollup_Game_timeout0 rollup stakers).
unfold Raw_context.Valid.on.
∃ sim_ctxt0; now split_conj.
}
clear H_ctxt.
pose proof Raw_context.domain_conj H_ctxt_game_timeout_if_exists
H_ctxt_game_value_exists as H_ctxt.
clear - H_ctxt.
cbn - [
Raw_context.Nested_indexed_data_storage.value_exists
Raw_context.Nested_indexed_data_storage.key_exists] in ×.
easy.
}
clear H_ctxt. rename H_ctxt' into H_ctxt.
clear - H_ctxt.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db. simpl.
destruct H_sim_ctxt_domain as [H_timeout_exists H_game_exists].
simpl in ×.
do 2 (destruct_find H_timeout_exists; [|easy]).
simpl.
esplit_letP. {
esplit_letP. {
destruct game, turn; simpl;
apply Raw_level_repr.add_is_valid;
try apply H_timeout_exists;
destruct t; simpl in *;
destruct H_timeout_exists; simpl in *; lia.
}
intros raw_level H_raw_level.
unfold fail_unless. unfold Raw_level_repr.op_gt.
step; cbn; [|easy].
now instantiate (1 := fun _ ⇒ True).
}
intros. simpl.
by_Raw_context_on_impl_t.
Qed.
(H_ctxt : Raw_context.Valid.on
(fun sim_ctxt ⇒
Raw_context.Nested_indexed_data_storage
.key_exists
rollup stakers sim_ctxt.(Raw_context.Sc_rollup_Game_timeout))
ctxt)
(H_index : Sc_rollup_game_repr.Index.Valid.t stakers) :
letP? '(outcome, ctxt) :=
Sc_rollup_refutation_storage.timeout ctxt rollup stakers in
Raw_context.Valid.t ctxt.
Proof.
Raw_context.Valid.destruct_rewrite H_ctxt.
destruct H_sim_ctxt.
red in Sc_rollup_Game_timeout.
specialize (Sc_rollup_Game_timeout rollup stakers).
unfold Sc_rollup_refutation_storage.timeout.
unshelve match type of H_ctxt with
| Raw_context.Valid.on ?domain _ ⇒
pose proof get_game_preserves_domain _ rollup stakers
domain H_ctxt as H_game_presv;
pose proof get_game_is_valid (Raw_context.to_t sim_ctxt)
rollup stakers
ltac:(now apply Raw_context.on_impl_t in H_ctxt)
as H_game_is_valid
end.
ez destruct (Sc_rollup_refutation_storage.get_game _ _ _) as [p|].
destruct p as [game ctxt'].
clear dependent ctxt.
rename ctxt' into ctxt.
assert (H_ctxt' :
Raw_context.Valid.on
(fun sim_ctxt : Raw_context.t ⇒
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.timeout.Valid.t
rollup stakers
sim_ctxt.(Raw_context.Sc_rollup_Game_timeout) ∧
Raw_context.Nested_indexed_data_storage.value_exists
Sc_rollup_game_repr.V1.Valid.t
rollup stakers sim_ctxt.(Raw_context.Sc_rollup_Game))
ctxt).
{ cbn - [
Raw_context.Nested_indexed_data_storage.value_exists
Raw_context.Nested_indexed_data_storage.key_exists] in ×.
destruct H_game_is_valid as [H_game_is_valid H_ctxt_game_value_exists].
unshelve epose proof Raw_context.key_exists_impl_value_exists
rollup stakers ctxt Sc_rollup_game_repr.timeout.Valid.t
H_game_presv _
as H_ctxt_game_timeout_if_exists.
{ Raw_context.Valid.destruct_rewrite H_game_presv.
inversion H_sim_ctxt.
red in Sc_rollup_Game_timeout0.
specialize (Sc_rollup_Game_timeout0 rollup stakers).
unfold Raw_context.Valid.on.
∃ sim_ctxt0; now split_conj.
}
clear H_ctxt.
pose proof Raw_context.domain_conj H_ctxt_game_timeout_if_exists
H_ctxt_game_value_exists as H_ctxt.
clear - H_ctxt.
cbn - [
Raw_context.Nested_indexed_data_storage.value_exists
Raw_context.Nested_indexed_data_storage.key_exists] in ×.
easy.
}
clear H_ctxt. rename H_ctxt' into H_ctxt.
clear - H_ctxt.
Raw_context.Valid.destruct_rewrite H_ctxt.
rewrite_db storage_db. simpl.
destruct H_sim_ctxt_domain as [H_timeout_exists H_game_exists].
simpl in ×.
do 2 (destruct_find H_timeout_exists; [|easy]).
simpl.
esplit_letP. {
esplit_letP. {
destruct game, turn; simpl;
apply Raw_level_repr.add_is_valid;
try apply H_timeout_exists;
destruct t; simpl in *;
destruct H_timeout_exists; simpl in *; lia.
}
intros raw_level H_raw_level.
unfold fail_unless. unfold Raw_level_repr.op_gt.
step; cbn; [|easy].
now instantiate (1 := fun _ ⇒ True).
}
intros. simpl.
by_Raw_context_on_impl_t.
Qed.
The function [reward] is valid.
Lemma reward_is_valid ctxt winner
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, updates) := Sc_rollup_refutation_storage.reward ctxt winner in
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
unfold Sc_rollup_refutation_storage.reward.
esplit_letP. {
apply Tez_repr.op_divquestion_is_valid'; [|lia].
unfold Constants_storage.sc_rollup_stake_amount.
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Raw_context.sc_rollup.
apply H_sim_ctxt.
}
intros tez H_tez.
now apply Token.transfer_is_valid.
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? '(ctxt, updates) := Sc_rollup_refutation_storage.reward ctxt winner in
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
unfold Sc_rollup_refutation_storage.reward.
esplit_letP. {
apply Tez_repr.op_divquestion_is_valid'; [|lia].
unfold Constants_storage.sc_rollup_stake_amount.
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Raw_context.sc_rollup.
apply H_sim_ctxt.
}
intros tez H_tez.
now apply Token.transfer_is_valid.
Qed.
The function [apply_game_result] is valid.
Lemma apply_game_result_is_valid ctxt rollup stakers game_result :
Raw_context.Valid.t ctxt →
letP? '(_, ctxt, updates) :=
Sc_rollup_refutation_storage.apply_game_result
ctxt rollup stakers game_result in
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
intros H_ctxt.
unfold Sc_rollup_refutation_storage.apply_game_result.
pose (P := fun '(ctxt, updates) ⇒
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates).
esplit_letP. {
destruct game_result.
{ esplit_letP. {
step; now apply reward_is_valid.
} intros [ctxt1 balance_updates'] [H_ctxt1 H_balance_updates1].
clear H_ctxt.
Raw_context.Valid.destruct_rewrite H_ctxt1.
rewrite Storage_generated.Sc_rollup.Game.remove with (size := 0).
simpl.
step; simpl.
{ esplit_letP. {
instantiate (1 := P).
simpl.
apply Sc_rollup_stake_storage.remove_staker_is_valid.
apply (Raw_context.f_preserves_context_trivial_validity
sim_ctxt Raw_context.Sc_rollup_Game ltac:(eauto)).
easy.
}
{ intros [ctxt2 balance_updates2]
[H_ctxt2 H_balance_updates2]. simpl.
instantiate (1 := P).
subst P. simpl. split; [easy|].
red.
apply Lists.List.Forall_app.
now split.
}
}
esplit_letP. {
now apply Sc_rollup_stake_storage.remove_staker_is_valid.
}
intros [ctxt3 balance_updates3]
[H_ctxt3 H_balance_updates3].
simpl. split; [easy|].
now apply Lists.List.Forall_app.
}
esplit_letP. {
now apply Sc_rollup_stake_storage.remove_staker_is_valid.
}
clear ctxt H_ctxt.
intros [ctxt balance_updates] [H_ctxt H_balance_updates].
esplit_letP. {
now apply Sc_rollup_stake_storage.remove_staker_is_valid.
}
intros. step. simpl. split; [easy|].
now apply Forall_app.
}
intros [? ?] [? ?].
esplit_letP. {
destruct_last_ctxt.
rewrite Storage_generated.Sc_rollup.Game_timeout.remove
with (size := 0). simpl.
instantiate (1 := (fun '(ctxt, _, _) ⇒ Raw_context.Valid.t ctxt)).
step; simpl;
now apply (Raw_context.f_preserves_context_trivial_validity
sim_ctxt Raw_context.Sc_rollup_Game ltac:(eauto)).
}
intros [[? ?] ?] ?.
esplit_letP. {
destruct_last_ctxt.
rewrite Storage_generated.Sc_rollup.Opponent.remove
with (size := 0); simpl.
instantiate (1 := (fun '(ctxt, _, _) ⇒ Raw_context.Valid.t ctxt)).
step; simpl; [|easy].
now apply (Raw_context.f_preserves_context_trivial_validity
sim_ctxt Raw_context.Sc_rollup_Game ltac:(eauto)).
}
intros [[? ?] ?] ?.
esplit_letP. {
destruct_last_ctxt.
rewrite Storage_generated.Sc_rollup.Opponent.remove
with (size := 0); simpl.
instantiate (1 := (fun '(ctxt, _, _) ⇒ Raw_context.Valid.t ctxt)).
step; simpl; [|easy].
now apply (Raw_context.f_preserves_context_trivial_validity
sim_ctxt Raw_context.Sc_rollup_Game ltac:(eauto)).
}
intros. do 2 step. simpl. now split.
Qed.
Module conflict.
Module Valid.
Import Proto_alpha.Sc_rollup_refutation_storage.conflict.
Raw_context.Valid.t ctxt →
letP? '(_, ctxt, updates) :=
Sc_rollup_refutation_storage.apply_game_result
ctxt rollup stakers game_result in
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates.
Proof.
intros H_ctxt.
unfold Sc_rollup_refutation_storage.apply_game_result.
pose (P := fun '(ctxt, updates) ⇒
Raw_context.Valid.t ctxt ∧
Receipt_repr.balance_updates.Valid.t updates).
esplit_letP. {
destruct game_result.
{ esplit_letP. {
step; now apply reward_is_valid.
} intros [ctxt1 balance_updates'] [H_ctxt1 H_balance_updates1].
clear H_ctxt.
Raw_context.Valid.destruct_rewrite H_ctxt1.
rewrite Storage_generated.Sc_rollup.Game.remove with (size := 0).
simpl.
step; simpl.
{ esplit_letP. {
instantiate (1 := P).
simpl.
apply Sc_rollup_stake_storage.remove_staker_is_valid.
apply (Raw_context.f_preserves_context_trivial_validity
sim_ctxt Raw_context.Sc_rollup_Game ltac:(eauto)).
easy.
}
{ intros [ctxt2 balance_updates2]
[H_ctxt2 H_balance_updates2]. simpl.
instantiate (1 := P).
subst P. simpl. split; [easy|].
red.
apply Lists.List.Forall_app.
now split.
}
}
esplit_letP. {
now apply Sc_rollup_stake_storage.remove_staker_is_valid.
}
intros [ctxt3 balance_updates3]
[H_ctxt3 H_balance_updates3].
simpl. split; [easy|].
now apply Lists.List.Forall_app.
}
esplit_letP. {
now apply Sc_rollup_stake_storage.remove_staker_is_valid.
}
clear ctxt H_ctxt.
intros [ctxt balance_updates] [H_ctxt H_balance_updates].
esplit_letP. {
now apply Sc_rollup_stake_storage.remove_staker_is_valid.
}
intros. step. simpl. split; [easy|].
now apply Forall_app.
}
intros [? ?] [? ?].
esplit_letP. {
destruct_last_ctxt.
rewrite Storage_generated.Sc_rollup.Game_timeout.remove
with (size := 0). simpl.
instantiate (1 := (fun '(ctxt, _, _) ⇒ Raw_context.Valid.t ctxt)).
step; simpl;
now apply (Raw_context.f_preserves_context_trivial_validity
sim_ctxt Raw_context.Sc_rollup_Game ltac:(eauto)).
}
intros [[? ?] ?] ?.
esplit_letP. {
destruct_last_ctxt.
rewrite Storage_generated.Sc_rollup.Opponent.remove
with (size := 0); simpl.
instantiate (1 := (fun '(ctxt, _, _) ⇒ Raw_context.Valid.t ctxt)).
step; simpl; [|easy].
now apply (Raw_context.f_preserves_context_trivial_validity
sim_ctxt Raw_context.Sc_rollup_Game ltac:(eauto)).
}
intros [[? ?] ?] ?.
esplit_letP. {
destruct_last_ctxt.
rewrite Storage_generated.Sc_rollup.Opponent.remove
with (size := 0); simpl.
instantiate (1 := (fun '(ctxt, _, _) ⇒ Raw_context.Valid.t ctxt)).
step; simpl; [|easy].
now apply (Raw_context.f_preserves_context_trivial_validity
sim_ctxt Raw_context.Sc_rollup_Game ltac:(eauto)).
}
intros. do 2 step. simpl. now split.
Qed.
Module conflict.
Module Valid.
Import Proto_alpha.Sc_rollup_refutation_storage.conflict.
Validity predicate for [conflict].
Record t (x : Sc_rollup_refutation_storage.conflict) : Prop := {
their_commitment :
Sc_rollup_commitment_repr.V1.Valid.t x.(their_commitment);
our_commitment :
Sc_rollup_commitment_repr.V1.Valid.t x.(our_commitment);
}.
End Valid.
End conflict.
their_commitment :
Sc_rollup_commitment_repr.V1.Valid.t x.(their_commitment);
our_commitment :
Sc_rollup_commitment_repr.V1.Valid.t x.(our_commitment);
}.
End Valid.
End conflict.
The encoding [conflict_encoding] is valid.
Lemma conflict_encoding_is_valid :
Data_encoding.Valid.t conflict.Valid.t
Sc_rollup_refutation_storage.conflict_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve conflict_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t conflict.Valid.t
Sc_rollup_refutation_storage.conflict_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve conflict_encoding_is_valid : Data_encoding_db.
The function [conflicting_stakers_uncarbonated] is valid.
Lemma conflicting_stakers_uncarbonated_is_valid ctxt rollup staker
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? conflicts :=
Sc_rollup_refutation_storage.conflicting_stakers_uncarbonated
ctxt rollup staker in
List.Forall conflict.Valid.t conflicts.
Proof.
unfold Sc_rollup_refutation_storage.conflicting_stakers_uncarbonated.
esplit_letP. {
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Sc_rollup_refutation_storage.Store.stakers.
rewrite Storage_generated.Sc_rollup.Stakers.list_key_values.
instantiate (1 := fun '(ctxt, _) ⇒
Raw_context.Valid.t ctxt); simpl.
simpl. step; simpl; easy.
}
intros [? ?] ?.
unfold fold_left_es, fold_left_e.
rewrite List.fold_left_rev_right_eq.
induction (rev _).
{ constructor. }
{ simpl.
unfold Error_monad.op_gtgtquestion in ×.
step; simpl in *; [|easy].
do 2 step; [|easy].
do 2 (step; simpl).
esplit_letP. {
esplit_letP. {
now apply Sc_rollup_commitment_storage.get_commitment_unsafe_is_valid.
}
intros [? ?] ?.
esplit_letP. {
now apply Sc_rollup_commitment_storage.get_commitment_unsafe_is_valid.
}
intros [? ?] [? ?].
simpl.
instantiate (1 := conflict.Valid.t).
split; simpl;
easy.
}
intros conflicts H_conflicts. simpl.
constructor.
{ eauto. }
{ easy. }
}
Qed.
(H_ctxt : Raw_context.Valid.t ctxt) :
letP? conflicts :=
Sc_rollup_refutation_storage.conflicting_stakers_uncarbonated
ctxt rollup staker in
List.Forall conflict.Valid.t conflicts.
Proof.
unfold Sc_rollup_refutation_storage.conflicting_stakers_uncarbonated.
esplit_letP. {
Raw_context.Valid.destruct_rewrite H_ctxt.
unfold Sc_rollup_refutation_storage.Store.stakers.
rewrite Storage_generated.Sc_rollup.Stakers.list_key_values.
instantiate (1 := fun '(ctxt, _) ⇒
Raw_context.Valid.t ctxt); simpl.
simpl. step; simpl; easy.
}
intros [? ?] ?.
unfold fold_left_es, fold_left_e.
rewrite List.fold_left_rev_right_eq.
induction (rev _).
{ constructor. }
{ simpl.
unfold Error_monad.op_gtgtquestion in ×.
step; simpl in *; [|easy].
do 2 step; [|easy].
do 2 (step; simpl).
esplit_letP. {
esplit_letP. {
now apply Sc_rollup_commitment_storage.get_commitment_unsafe_is_valid.
}
intros [? ?] ?.
esplit_letP. {
now apply Sc_rollup_commitment_storage.get_commitment_unsafe_is_valid.
}
intros [? ?] [? ?].
simpl.
instantiate (1 := conflict.Valid.t).
split; simpl;
easy.
}
intros conflicts H_conflicts. simpl.
constructor.
{ eauto. }
{ easy. }
}
Qed.