🍃 Signature.v

Proofs

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 :=
    s ≠ Signature.zero.
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
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.compare).
#[global] Hint Resolve Public_key_hash_compare_is_valid : Compare_db.

Axiom Public_key_hash_encoding_is_valid
  : Data_encoding.Valid.t (fun _ ⇒ True)
    Public_key_hash.(SIGNATURE_PUBLIC_KEY_HASH.encoding).
#[global] Hint Resolve Public_key_hash_encoding_is_valid : Data_encoding_db.

Axiom Public_key_compare_is_valid
  : Compare.Valid.t (fun _ ⇒ True) id
    Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.compare).
#[global] Hint Resolve Public_key_compare_is_valid : Compare_db.

Axiom Public_key_encoding_is_valid
  : Data_encoding.Valid.t (fun _ ⇒ True)
    Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding).
#[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 [Signature.compare] 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 Signature.compare.
#[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 :=
    Included_SIGNATURE_is_valid.(S.SIGNATURE.Valid.Compare_S)).
  rewrite (H_compare
      .(Compare.S.Valid.eq)
      .(Compare.S.Eq.equal)); simpl.
  scrush solve: lia.
Qed.

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.