🎯 Destination_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require Import TezosOfOCaml.Proto_alpha.Destination_repr.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_repr.

The [compare] function is valid.

Lemma compare_is_valid :
  Compare.Valid.t (fun _ ⇒ True) id Destination_repr.compare.
Proof.
  apply (Compare.equality (
    let proj_tx_rollup x :=
      match x with
      | Destination_repr.Tx_rollup x ⇒ Some x
      | _ ⇒ None
      end in
    let proj_contract x :=
      match x with
      | Destination_repr.Contract x ⇒ Some x
      | _ ⇒ None
      end in
    let proj x :=
      (proj_tx_rollup x, proj_contract x) in
    Compare.projection proj (
      Compare.lexicographic
        (Compare.Option.compare Tx_rollup_repr.compare)
        (Compare.Option.compare Contract_repr.compare)
    )
  )); [intros [] []; cbn; hauto lq: on |].
  Compare.valid_auto.
  unfold id; sauto lq: on.
Qed.
#[global] Hint Resolve compare_is_valid : Compare_db.

Axiom of_b58_to_b58_eq : ∀ v, ∃ error,
  Contract_repr.of_b58check (Tx_rollup_repr.to_b58check v) =
  Pervasives.Error error.

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Destination_repr.encoding.
Proof.
  Data_encoding.Valid.data_encoding_auto.
  intros [] ?;
    unfold Destination_repr.of_b58check, Destination_repr.to_b58check.
  { rewrite Contract_repr.of_b58_to_b58_eq.
    dtauto.
  }
  { match goal with
    | v : Tx_rollup_repr.t |- _ ⇒
      destruct (of_b58_to_b58_eq v) as [? H_eq];
      rewrite H_eq
    end.
    rewrite Tx_rollup_repr.of_b58_to_b58_eq; simpl.
    tauto.
  }
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.