Skip to main content

🐆 Tx_rollup_message_repr.v

Proofs

See code, Gitlab , OCaml

Validity predicate for the type [deposit].
    Record t (p : Tx_rollup_message_repr.deposit) : Prop := {
      destination : Indexable.Value.Valid.t p.(destination);
      amount : Tx_rollup_l2_qty.Valid.t p.(amount);
    }.
  End Valid.
End deposit.

The encoding [deposit_encoding] is valid.
Lemma deposit_encoding_is_valid : Data_encoding.Valid.t deposit.Valid.t
  Tx_rollup_message_repr.deposit_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve deposit_encoding_is_valid : Data_encoding_db.

The encoding [batch_encoding] is valid.
Lemma batch_encoding_is_valid : Data_encoding.Valid.t (fun _True)
  Tx_rollup_message_repr.batch_encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve batch_encoding_is_valid : Data_encoding_db.

Module Valid.
Validity predicate for the type [t].
  Definition t (x : Tx_rollup_message_repr.t) : Prop :=
    match x with
    | Tx_rollup_message_repr.Batch sString.Int_length.t s
    | Tx_rollup_message_repr.Deposit ddeposit.Valid.t d
    end.
End Valid.

The encoding [encoding] is valid.
Lemma encoding_is_valid : Data_encoding.Valid.t Valid.t
  Tx_rollup_message_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

The function [size_value] is valid.
Lemma size_value_is_valid message :
  Valid.t message
  Pervasives.Int.Valid.t (Tx_rollup_message_repr.size_value message).
Proof.
  intros.
  destruct message; simpl in ×.
  { pose proof (String.length_is_valid s).
    lia.
  }
  { lia. }
Qed.