🦏 Sc_rollup_PVM_sig.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Bytes.
Require Import TezosOfOCaml.Proto_alpha.Sc_rollup_PVM_sig.

Require TezosOfOCaml.Proto_alpha.Proofs.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_metadata_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_outbox_message_repr.

Module inbox_message.
  Module Valid.
    Import Proto_alpha.Sc_rollup_PVM_sig.inbox_message.

Validity predicate for the type [inbox_message].

    Record t (x : inbox_message) : Prop := {
      inbox_level : Raw_level_repr.Valid.t x.(inbox_level);
      message_counter : 0 ≤ x.(message_counter);
    }.
  End Valid.
End inbox_message.

The encoding [inbox_message_encoding] is valid.

Lemma inbox_message_encoding_is_valid :
  Data_encoding.Valid.t inbox_message.Valid.t inbox_message_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve inbox_message_encoding_is_valid : Data_encoding_db.

Module reveal_data.
  Module Valid.

Validity predicate for the type [reveal_data].

    Definition t (x : reveal_data) : Prop :=
      match x with
      | Raw_data s ⇒ True
      | Metadata meta ⇒ Sc_rollup_metadata_repr.Valid.t meta
      | Dal_page dal_page ⇒ True
      end.
  End Valid.
End reveal_data.

The encoding [reveal_data_encoding] is valid.

Lemma reveal_data_encoding_is_valid :
  Data_encoding.Valid.t reveal_data.Valid.t reveal_data_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros reveal_data H.
  step.
  { repeat split . }
  { do 2 split ; [ constructor |].
    inversion H.
    constructor. assumption.
  }
  { do 2 split ; [ constructor |]. step ; constructor. }
Qed.
#[global] Hint Resolve reveal_data_encoding_is_valid : Data_encoding_db.

Module input.
  Module Valid.

Validity predicate for the type [input].

    Definition t (x : input) : Prop :=
      match x with
      | Inbox_message i ⇒ inbox_message.Valid.t i
      | Reveal j ⇒ reveal_data.Valid.t j
      end.
  End Valid.
End input.

The encoding [input_encoding] is valid.

Lemma input_encoding_is_valid :
  Data_encoding.Valid.t input.Valid.t Sc_rollup_PVM_sig.input_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve input_encoding_is_valid : Data_encoding_db.

The equality function [inbox_message_equal] is valid.

Lemma inbox_message_equal_is_valid :
  Compare.Equal.Valid.t (fun _ ⇒ True) inbox_message_equal.
Proof.
  unfold Compare.Equal.Valid.t.
  intros x y H H0.
  split; intro H_eq.
  { unfold inbox_message_equal.
    apply Bool.andb_true_iff.
    split. {
      destruct x; destruct y.
      injection H_eq as H_eq.
      unfold Raw_level_repr.equal.
      subst; simpl.
      apply Z.eqb_eq.
      reflexivity.
    }
    apply Bool.andb_true_iff.
    split. {
      destruct x; destruct y.
      injection H_eq as H_eq.
      unfold Z.equal.
      subst; simpl.
      apply Z.eqb_eq.
      reflexivity.
    }
    destruct x; destruct y.
    injection H_eq as H_eq.
    unfold String.equal.
    subst; simpl.
    apply eqb_eq.
    reflexivity.
  }
  { unfold inbox_message_equal in H_eq.
    apply Bool.andb_true_iff in H_eq.
    destruct H_eq as [H1 H2].
    apply Bool.andb_true_iff in H2.
    destruct H2 as [H2 H3].
    destruct x; destruct y.
    simpl in ×.
    unfold Raw_level_repr.equal in H1.
    simpl in H1.
    apply Z.eqb_eq in H1.
    unfold Z.equal in H2.
    apply Z.eqb_eq in H2.
    unfold String.equal in H3.
    apply eqb_eq in H3.
    subst.
    reflexivity.
  }
Qed.

The equality function [reveal_data_equal] is valid.

Lemma reveal_data_equal_is_valid :
  Compare.Equal.Valid.t (fun _ ⇒ True) reveal_data_equal.
Proof.
  unfold Compare.Equal.Valid.t.
  intros x y _ _.

Currently, we ignore [True] hypotheses.

  split ; intro H2.
  { unfold reveal_data_equal.
    destruct x, y ; try inversion H2 as [H0].
    { apply String.equal_is_valid ; try constructor. }
    { apply Sc_rollup_metadata_repr.equal_is_valid ; try constructor. }
    { destruct o, o0 ; try (inversion H0) ; try reflexivity.
      apply Bytes.equal_reflexive.
    }
  }
  { destruct x, y ; try inversion H2 as [H0] ; apply f_equal ; clear H0 ;
      unfold reveal_data_equal in H2.
    { apply String.equal_is_valid ; try constructor. assumption. }
    { apply Sc_rollup_metadata_repr.equal_is_valid ; try constructor.
      assumption. }
    { destruct o, o0 ; try (inversion H2); try reflexivity.
      apply f_equal.
      apply Bytes.equal_is_valid ; try constructor. assumption.
    }
  }
Qed.

The equality function [input_equal] is valid.

Lemma input_equal_is_valid :
  Compare.Equal.Valid.t (fun _ ⇒ True) Sc_rollup_PVM_sig.input_equal.
Proof.

@TODO : clean proof

  unfold Compare.Equal.Valid.t.
  intros x y H H0.
  split.
  { intro H1.
    unfold input_equal.
    step. {
      step; [| discriminate].
      injection H1 as H1.
      subst.
      pose proof inbox_message_equal_is_valid.
      unfold Compare.Equal.Valid.t in H1.
      pose proof (H1 i0 i0).
      apply H2; trivial.
    }
    step; [discriminate |].
    injection H1 as H1.
    subst.
    pose proof reveal_data_equal_is_valid.
    unfold Compare.Equal.Valid.t in H1.
    pose proof (H1 r0 r0).
    apply H2; trivial.
  }
  { intro H1.
    unfold input_equal in H1.
    destruct x eqn:X.
    { destruct y; [| discriminate].
      pose proof inbox_message_equal_is_valid.
      unfold Compare.Equal.Valid.t in H2.
      pose proof (H2 i i0).
      apply H3 in H1; trivial.
      sfirstorder.
    }
    { destruct y; [discriminate |].
      pose proof reveal_data_equal_is_valid.
      unfold Compare.Equal.Valid.t in H2.
      pose proof (H2 r r0).
      apply H2 in H1; trivial.
      sfirstorder.
    }
  }
Qed.

Module Reveal_hash.

[V0] is valid.

  Lemma V0_is_valid : S.HASH.Valid.t (fun _ ⇒ True) Reveal_hash.V0.
  Proof.
    apply Blake2B.Make_is_valid.
  Qed.

The equality function [equal] on [Reveal_Hash] is valid, i.e. captures propositional equality.

  Lemma equal_is_valid :
    Compare.Equal.Valid.t (fun _ ⇒ True) Reveal_hash.equal.
  Proof.
    apply Blake2B.Make_equal_is_valid.
  Qed.

The encoding of [Reveal_hash] is valid

  Lemma encoding_is_valid :
    Data_encoding.Valid.t (fun _ ⇒ True)
      Sc_rollup_PVM_sig.Reveal_hash.encoding.
  Proof.
    Data_encoding.Valid.data_encoding_auto ; [ apply V0_is_valid |].
    dtauto.
  Qed.
  #[global] Hint Resolve encoding_is_valid : Data_encoding_db.
End Reveal_hash.

Module reveal.
  Module Valid.

Validity predicate for the type [reveal].

    Definition t (reveal : Sc_rollup_PVM_sig.reveal) : Prop :=
      match reveal with
      | Reveal_raw_data _
      | Reveal_metadata ⇒ True
      | Request_dal_page page ⇒ Dal_slot_repr.Page.Valid.t page
      end.
  End Valid.
End reveal.

The encoding [reveal_encoding] is valid.

Lemma reveal_encoding_is_valid :
  Data_encoding.Valid.t reveal.Valid.t Sc_rollup_PVM_sig.reveal_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve reveal_encoding_is_valid : Data_encoding_db.

Module input_request.
  Module Valid.

Validity predicate for [input_request].

    Definition t (x : Sc_rollup_PVM_sig.input_request) : Prop :=
      match x with
      | No_input_required ⇒ True
      | Initial ⇒ True
      | First_after level counter ⇒
        Raw_level_repr.Valid.t level ∧
          0 ≤ counter
      | Needs_reveal r ⇒ reveal.Valid.t r
      end.
  End Valid.
End input_request.

The encoding [input_request_encoding] is valid.

Lemma input_request_encoding_is_valid :
  Data_encoding.Valid.t input_request.Valid.t
    Sc_rollup_PVM_sig.input_request_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros [] ?; simpl in × ; try split ; try constructor ; try reflexivity ;
  try assumption.
Qed.
#[global] Hint Resolve input_encoding_is_valid : Data_encoding_db.

The equality function [reveal_equal] is valid.

Lemma reveal_equal_is_valid :
  Compare.Equal.Valid.t (fun _ ⇒ True) reveal_equal.
Proof.
  unfold Compare.Equal.Valid.t.
  intros reveal1 reveal2 _ _.
  destruct reveal1, reveal2 ;
  split ; intro H ; try inversion H ; unfold reveal_equal ; unfold reveal_equal in H
  ; subst; try reflexivity.
  { apply Reveal_hash.equal_is_valid ; try constructor ; reflexivity.
  }
  { apply Reveal_hash.equal_is_valid in H ; try constructor ;
    rewrite H. reflexivity. }
  { apply Dal_slot_repr.Page.equal_is_valid ; constructor. }
  { apply Dal_slot_repr.Page.equal_is_valid in H1 ; try constructor.
    subst. reflexivity.
  }
Qed.

The equality [input_request_equal] is valid.

Lemma input_request_equal_is_valid :
  Compare.Equal.Valid.t input_request.Valid.t
    Sc_rollup_PVM_sig.input_request_equal.
Proof.
  unfold Sc_rollup_PVM_sig.input_request_equal, Raw_level_repr.equal; simpl.
  constructor.
  { destruct_all Sc_rollup_PVM_sig.input_request; try congruence.
    intros.
    replace t1 with t by congruence.
    replace t2 with t0 by congruence.
    lia.
    intro H1. injection H1 as H1.
    pose proof reveal_equal_is_valid.
    unfold Compare.Equal.Valid.t in H2.
    subst.
    sfirstorder.
  }
  { destruct_all Sc_rollup_PVM_sig.input_request; try congruence.
    intros.
    replace t1 with t by lia.
    replace t2 with t0 by lia.
    reflexivity.
    intro H1.
    pose proof reveal_equal_is_valid.
    unfold Compare.Equal.Valid.t in H2.
    sfirstorder.
  }
Qed.

Module output.
  Module Valid.
    Import Proto_alpha.Sc_rollup_PVM_sig.output.

Validity predicate for the type [output].

    Record t (x : Sc_rollup_PVM_sig.output) : Prop := {
      outbox_level : Raw_level_repr.Valid.t x.(outbox_level);
      message_index : 0 ≤ x.(message_index);
      message : Sc_rollup_outbox_message_repr.Valid.t x.(message);
    }.
  End Valid.
End output.

The encoding [output_encoding] is valid.

Lemma output_encoding_is_valid :
  Data_encoding.Valid.t output.Valid.t Sc_rollup_PVM_sig.output_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve output_encoding_is_valid : Data_encoding_db.