🍃 Signature.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.S.
Module Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.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.
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.
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.is_Make)
.(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.
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.is_Make)
.(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.