Skip to main content

🍃 Signature.v


See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V7.

Require TezosOfOCaml.Environment.V7.Proofs.S.

Module Valid.
Validity predicate for the type [Signature.t]
  Definition t (s : Signature.t) : Prop :=
End Valid.

Axiom Included_SIGNATURE_is_valid :
  S.SIGNATURE.Valid.t (fun _True) Signature.Included_SIGNATURE.

Axiom Public_key_hash_compare_is_valid
  : Compare.Valid.t (fun _True) id
#[global] Hint Resolve Public_key_hash_compare_is_valid : Compare_db.

Axiom Public_key_hash_encoding_is_valid
  : Data_encoding.Valid.t (fun _True)
#[global] Hint Resolve Public_key_hash_encoding_is_valid : Data_encoding_db.

Axiom Public_key_compare_is_valid
  : Compare.Valid.t (fun _True) id
#[global] Hint Resolve Public_key_compare_is_valid : Compare_db.

Axiom Public_key_encoding_is_valid
  : Data_encoding.Valid.t (fun _True)
#[global] Hint Resolve Public_key_encoding_is_valid : Data_encoding_db.

Forget about the kind of signature and only keep the binary representation. Equivalent to converting a signature back and forth with bytes.
Parameter canonize : Signature.t Signature.t.

The [] function is only a pre-order because we compare the binary representation of signatures. This representation does not contain the kind of the signature.
Axiom compare_is_valid :
  Compare.Valid.t (fun _True) canonize
#[global] Hint Resolve compare_is_valid : Compare_db.

Lemma equal_like_eq (s1 s2 : Signature.t) :
  Signature.equal s1 s2 = true s1 = s2.
  assert (H_compare :=
  rewrite (H_compare
      .(Compare.S.Eq.equal)); simpl.
  scrush solve: lia.

Axiom of_b58check_opt_to_b58check
  : signature,
    Signature.of_b58check_opt (Signature.to_b58check signature) =
    Some signature.

Axiom encoding_is_valid :
  Data_encoding.Valid.t (fun _True) Signature.encoding.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.