🎯 Destination_repr.v

Proofs

See code, Gitlab , OCaml

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

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

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.Signature.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Proofs.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Sc_rollup_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_sc_rollup x :=
      match x with
      | Destination_repr.Sc_rollup x ⇒ Some x
      | _ ⇒ None
      end in
    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_sc_rollup x, (proj_tx_rollup x, proj_contract x)) in
    Compare.projection proj (
      Compare.lexicographic
        (Compare.Option.compare Sc_rollup_repr.Address.compare)
      (
        Compare.lexicographic
          (Compare.Option.compare Tx_rollup_repr.compare)
          (Compare.Option.compare Contract_repr.compare)
      ))
        )); [intros [] []; cbn; try hauto lq: on |].
Admitted.
  (* Compare.valid_auto. *)
  (* unfold id; sauto lq: on. *)

#[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.

Axiom of_b58_Contract_to_b58_eq : ∀ v,
  of_b58check (Contract_repr.to_b58check v) = return? (Contract v).

Axiom of_b58_Tx_rollup_to_b58_eq : ∀ v,
  of_b58check (Tx_rollup_repr.to_b58check v) = return? (Tx_rollup v).

Axiom of_b58_Sc_rollup_Address_to_b58_eq : ∀ v,
  of_b58check (Sc_rollup_repr.Address.to_b58check v) = return? (Sc_rollup v).

Lemma encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Destination_repr.encoding.
(* TODO: requires defining Base58.decode
         and proving that Destination_repr.of_b58check is an inverse
         of Contract_repr.to_b58check, Tx_rollup_repr.to_b58check
         and Sc_rollup_repr.Address.to_b58check
         (axioms above) *)
Proof.
  Data_encoding.Valid.data_encoding_auto.
  simpl.
  (*
  intros [] ?;
    unfold Destination_repr.to_b58check;
    (rewrite of_b58_Contract_to_b58_eq ||
     rewrite of_b58_Tx_rollup_to_b58_eq ||
     rewrite of_b58_Sc_rollup_Address_to_b58_eq); sauto lq: on. *)
Admitted.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.