🦏 Sc_rollup_game_repr.v

Proofs

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.

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 *)

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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 *)

The function [find_choice] is valid

Lemma find_choice_is_valid dissection_chunk tick :
  letP ? '(chunk1 , chunk2 ) :=
    Sc_rollup_game_repr.find_choice dissection_chunk tick in
  dissection_chunk.Valid.t chunk1 ∧
  dissection_chunk.Valid.t chunk2.
Proof.
Admitted.