💍 Commitment_repr.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Blinded_public_key_hash.

Require TezosOfOCaml.Proto_alpha.Commitment_repr.

Module Valid.
  Definition t (x : Commitment_repr.t) : Prop :=
    Tez_repr.Valid.t x.(Commitment_repr.t.amount).
End Valid.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t Commitment_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.