🦏 Sc_rollup_game_repr.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_dissection_chunk_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Context_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Option.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_proof_repr.
Module V1.
Module dissection.
Module Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_game_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_dissection_chunk_repr.
Require TezosOfOCaml.Environment.V8.Proofs.Context_hash.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Option.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_tick_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_proof_repr.
Module V1.
Module dissection.
Module Valid.
Validity predicate for the [list
Sc_rollup_game_repr.dissection_chunk] type.
Definition t (x : list Sc_rollup_game_repr.dissection_chunk) : Prop :=
List.Forall (fun y : Sc_rollup_dissection_chunk_repr.t ⇒
Sc_rollup_tick_repr.Valid.t
y.(Sc_rollup_dissection_chunk_repr.t.tick)) x.
End Valid.
End dissection.
Module Valid.
Import Sc_rollup_game_repr.t.
List.Forall (fun y : Sc_rollup_dissection_chunk_repr.t ⇒
Sc_rollup_tick_repr.Valid.t
y.(Sc_rollup_dissection_chunk_repr.t.tick)) x.
End Valid.
End dissection.
Module Valid.
Import Sc_rollup_game_repr.t.
Validity predicate for the type [Sc_rollup_game_repr.t]
Record t (x : Sc_rollup_game_repr.t) : Prop := {
inbox_snapshot : x.(inbox_snapshot).(Skip_list_repr.Make.cell
.back_pointers).(FallbackArray.t.default) = None;
inbox_snapshot_forall :
List.Forall (fun x0 : M× Sc_rollup_inbox_repr.Hash.t ⇒ x0 ≠ None)
x.(Sc_rollup_game_repr.t.inbox_snapshot)
.(Skip_list_repr.Make.cell.back_pointers)
.(FallbackArray.t.items);
inbox_snapshot_int31 :
Pervasives.Int31.Valid.t
x.(Sc_rollup_game_repr.t.inbox_snapshot)
.(Skip_list_repr.Make.cell.index);
}.
End Valid.
End V1.
Module dissection_chunk.
Module Valid.
(* @TODO *)
inbox_snapshot : x.(inbox_snapshot).(Skip_list_repr.Make.cell
.back_pointers).(FallbackArray.t.default) = None;
inbox_snapshot_forall :
List.Forall (fun x0 : M× Sc_rollup_inbox_repr.Hash.t ⇒ x0 ≠ None)
x.(Sc_rollup_game_repr.t.inbox_snapshot)
.(Skip_list_repr.Make.cell.back_pointers)
.(FallbackArray.t.items);
inbox_snapshot_int31 :
Pervasives.Int31.Valid.t
x.(Sc_rollup_game_repr.t.inbox_snapshot)
.(Skip_list_repr.Make.cell.index);
}.
End Valid.
End V1.
Module dissection_chunk.
Module Valid.
(* @TODO *)
The validity predicate for the [dissection_chunk] type
Parameter t : Sc_rollup_game_repr.dissection_chunk → Prop.
End Valid.
End dissection_chunk.
Module versioned.
Module Valid.
End Valid.
End dissection_chunk.
Module versioned.
Module Valid.
The validity predicate for the [Sc_rollup_game_repr.versioned] type
Record t (x : Sc_rollup_game_repr.versioned) : Prop := {
valid : ∀ t, x = Sc_rollup_game_repr.V1 t → V1.Valid.t t
}.
End Valid.
End versioned.
Module Index.
Module Valid.
valid : ∀ t, x = Sc_rollup_game_repr.V1 t → V1.Valid.t t
}.
End Valid.
End versioned.
Module Index.
Module Valid.
Validity predicate for [Sc_rollup_game_repr.Index.t].
Definition t (x : Sc_rollup_game_repr.Index.t) : Prop :=
Sc_rollup_repr.Staker.(SIGNATURE_PUBLIC_KEY_HASH.compare)
x.(Sc_rollup_game_repr.Index.t.alice)
x.(Sc_rollup_game_repr.Index.t.bob) ≤ 0.
End Valid.
End Index.
Sc_rollup_repr.Staker.(SIGNATURE_PUBLIC_KEY_HASH.compare)
x.(Sc_rollup_game_repr.Index.t.alice)
x.(Sc_rollup_game_repr.Index.t.bob) ≤ 0.
End Valid.
End Index.
The validity predicate for [step_encoding_is_valid] is valid
Module step.
Module Valid.
Record t (x : Sc_rollup_game_repr.step) : Prop := {
step : ∀ l,
x = Sc_rollup_game_repr.Dissection l → V1.dissection.Valid.t l
}.
End Valid.
End step.
Module refutation.
Module Valid.
Module Valid.
Record t (x : Sc_rollup_game_repr.step) : Prop := {
step : ∀ l,
x = Sc_rollup_game_repr.Dissection l → V1.dissection.Valid.t l
}.
End Valid.
End step.
Module refutation.
Module Valid.
Validity predicate for [Sc_rollup_game_repr.refutation].
Record t (x : Sc_rollup_game_repr.refutation) : Prop := {
choice : Sc_rollup_tick_repr.Valid.t
x.(Sc_rollup_game_repr.refutation.choice);
all : ∀ l, x.(Sc_rollup_game_repr.refutation.step) =
Sc_rollup_game_repr.Dissection l →
List.Forall (fun y : Sc_rollup_dissection_chunk_repr.t ⇒
Sc_rollup_tick_repr.Valid.t
y.(Sc_rollup_dissection_chunk_repr.t.tick)) l
}.
End Valid.
End refutation.
Module timeout.
Module Valid.
Import Proto_alpha.Sc_rollup_game_repr.timeout.
choice : Sc_rollup_tick_repr.Valid.t
x.(Sc_rollup_game_repr.refutation.choice);
all : ∀ l, x.(Sc_rollup_game_repr.refutation.step) =
Sc_rollup_game_repr.Dissection l →
List.Forall (fun y : Sc_rollup_dissection_chunk_repr.t ⇒
Sc_rollup_tick_repr.Valid.t
y.(Sc_rollup_dissection_chunk_repr.t.tick)) l
}.
End Valid.
End refutation.
Module timeout.
Module Valid.
Import Proto_alpha.Sc_rollup_game_repr.timeout.
The validity predicate for the [Sc_rollup_game_repr.timeout]
type.
Record t (x : Sc_rollup_game_repr.timeout) : Prop := {
alice : Pervasives.Int31.Valid.t x.(alice);
bob : Pervasives.Int31.Valid.t x.(bob);
last_turn_level : Raw_level_repr.Valid.t x.(last_turn_level);
}.
End Valid.
End timeout.
alice : Pervasives.Int31.Valid.t x.(alice);
bob : Pervasives.Int31.Valid.t x.(bob);
last_turn_level : Raw_level_repr.Valid.t x.(last_turn_level);
}.
End Valid.
End timeout.
The encoding [player_encoding_is_valid] is valid
Lemma player_encoding_is_valid :
Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_game_repr.player_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve player_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t (fun _ ⇒ True) Sc_rollup_game_repr.player_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve player_encoding_is_valid : Data_encoding_db.
The encoding [dissection_encoding_is_valid] is valid
Lemma dissection_encoding_is_valid :
Data_encoding.Valid.t
V1.dissection.Valid.t Sc_rollup_game_repr.dissection_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto. (*
intros x H. repeat apply Forall_and.
apply Forall_impl with (fun _ => True).
intros. step; trivial. apply List.Forall_True; sfirstorder.
apply H. apply Forall_impl with (fun _ => True). intros. reflexivity.
apply List.Forall_True. sfirstorder.
Qed.*)
Admitted.
#[global] Hint Resolve dissection_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t
V1.dissection.Valid.t Sc_rollup_game_repr.dissection_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto. (*
intros x H. repeat apply Forall_and.
apply Forall_impl with (fun _ => True).
intros. step; trivial. apply List.Forall_True; sfirstorder.
apply H. apply Forall_impl with (fun _ => True). intros. reflexivity.
apply List.Forall_True. sfirstorder.
Qed.*)
Admitted.
#[global] Hint Resolve dissection_encoding_is_valid : Data_encoding_db.
The encoding [encoding_is_valid] is valid
Lemma encoding_is_valid :
Data_encoding.Valid.t V1.Valid.t Sc_rollup_game_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Admitted.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t V1.Valid.t Sc_rollup_game_repr.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Admitted.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.
The encoding [versioned_encoding_is_valid] is valid
Lemma versioned_encoding_is_valid :
Data_encoding.Valid.t
versioned.Valid.t Sc_rollup_game_repr.versioned_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros x H. step. split; try reflexivity.
apply H; scongruence.
Qed.
#[global] Hint Resolve versioned_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t
versioned.Valid.t Sc_rollup_game_repr.versioned_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros x H. step. split; try reflexivity.
apply H; scongruence.
Qed.
#[global] Hint Resolve versioned_encoding_is_valid : Data_encoding_db.
The function [make] is valid.
Lemma make_is_valid a_value b_value :
Index.Valid.t (Sc_rollup_game_repr.Index.make a_value b_value).
Proof.
Admitted.
Index.Valid.t (Sc_rollup_game_repr.Index.make a_value b_value).
Proof.
Admitted.
The encoding [Index.encoding] is valid
Lemma Index_encoding_is_valid :
Data_encoding.Valid.t
Index.Valid.t Sc_rollup_game_repr.Index.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intuition.
unfold Sc_rollup_game_repr.Index.make.
destruct x eqn:H_x; unfold Index.Valid.t in H;
simpl in ×.
now replace (_ >? 0) with false by lia.
Qed.
#[global] Hint Resolve Index_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t
Index.Valid.t Sc_rollup_game_repr.Index.encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intuition.
unfold Sc_rollup_game_repr.Index.make.
destruct x eqn:H_x; unfold Index.Valid.t in H;
simpl in ×.
now replace (_ >? 0) with false by lia.
Qed.
#[global] Hint Resolve Index_encoding_is_valid : Data_encoding_db.
The encoding [step_encoding_is_valid] is valid
Lemma step_encoding_is_valid :
Data_encoding.Valid.t step.Valid.t Sc_rollup_game_repr.step_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros. step; split; trivial. sfirstorder.
Qed.
#[global] Hint Resolve step_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t step.Valid.t Sc_rollup_game_repr.step_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
intros. step; split; trivial. sfirstorder.
Qed.
#[global] Hint Resolve step_encoding_is_valid : Data_encoding_db.
The encoding [encoding_is_valid] is valid
Lemma refutation_encoding_is_valid :
Data_encoding.Valid.t
refutation.Valid.t Sc_rollup_game_repr.refutation_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve refutation_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t
refutation.Valid.t Sc_rollup_game_repr.refutation_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve refutation_encoding_is_valid : Data_encoding_db.
The encoding [reason_encoding] is valid
Lemma reason_encoding_is_valid :
Data_encoding.Valid.t
(fun _ ⇒ True) Sc_rollup_game_repr.reason_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve reason_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t
(fun _ ⇒ True) Sc_rollup_game_repr.reason_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve reason_encoding_is_valid : Data_encoding_db.
The encoding [game_result] is valid
Lemma game_result_encoding_is_valid :
Data_encoding.Valid.t
(fun _ ⇒ True) Sc_rollup_game_repr.game_result_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve game_result_encoding_is_valid
: Data_encoding_db.
Data_encoding.Valid.t
(fun _ ⇒ True) Sc_rollup_game_repr.game_result_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve game_result_encoding_is_valid
: Data_encoding_db.
The encoding [status] is valid
Lemma status_encoding_is_valid :
Data_encoding.Valid.t
(fun _ ⇒ True) Sc_rollup_game_repr.status_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve status_encoding_is_valid : Data_encoding_db.
Data_encoding.Valid.t
(fun _ ⇒ True) Sc_rollup_game_repr.status_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve status_encoding_is_valid : Data_encoding_db.
The encoding [timeout] is valid.
Lemma timeout_encoding_is_valid :
Data_encoding.Valid.t
timeout.Valid.t Sc_rollup_game_repr.timeout_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve timeout_encoding_is_valid : Data_encoding_db.
(* @TODO *)
Data_encoding.Valid.t
timeout.Valid.t Sc_rollup_game_repr.timeout_encoding.
Proof.
Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve timeout_encoding_is_valid : Data_encoding_db.
(* @TODO *)
The function [find_choice] is valid