Skip to main content

🎯 Destination_repr.v

Proofs

See code, Gitlab , OCaml

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 xSome x
      | _None
      end in
    let proj_contract x :=
      match x with
      | Destination_repr.Contract xSome 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.