🍃 S.v
Proofs
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_arg.
Module MINIMAL_HASH.
Definition to_Compare_S {t} (H : S.MINIMAL_HASH (t := t))
: Compare.S (t := t) := {|
Compare.S.op_eq := H.(S.MINIMAL_HASH.op_eq);
Compare.S.op_ltgt := H.(S.MINIMAL_HASH.op_ltgt);
Compare.S.op_lt := H.(S.MINIMAL_HASH.op_lt);
Compare.S.op_lteq := H.(S.MINIMAL_HASH.op_lteq);
Compare.S.op_gteq := H.(S.MINIMAL_HASH.op_gteq);
Compare.S.op_gt := H.(S.MINIMAL_HASH.op_gt);
Compare.S.compare := H.(S.MINIMAL_HASH.compare);
Compare.S.equal := H.(S.MINIMAL_HASH.equal);
Compare.S.max := H.(S.MINIMAL_HASH.max);
Compare.S.min := H.(S.MINIMAL_HASH.min);
|}.
Module Valid.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Environment.V8.Proofs.Compare.
Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_arg.
Module MINIMAL_HASH.
Definition to_Compare_S {t} (H : S.MINIMAL_HASH (t := t))
: Compare.S (t := t) := {|
Compare.S.op_eq := H.(S.MINIMAL_HASH.op_eq);
Compare.S.op_ltgt := H.(S.MINIMAL_HASH.op_ltgt);
Compare.S.op_lt := H.(S.MINIMAL_HASH.op_lt);
Compare.S.op_lteq := H.(S.MINIMAL_HASH.op_lteq);
Compare.S.op_gteq := H.(S.MINIMAL_HASH.op_gteq);
Compare.S.op_gt := H.(S.MINIMAL_HASH.op_gt);
Compare.S.compare := H.(S.MINIMAL_HASH.compare);
Compare.S.equal := H.(S.MINIMAL_HASH.equal);
Compare.S.max := H.(S.MINIMAL_HASH.max);
Compare.S.min := H.(S.MINIMAL_HASH.min);
|}.
Module Valid.
Validity predicate for the type [S.MINIMAL_HASH].
Record t {t} {H : S.MINIMAL_HASH (t := t)} : Prop := {
Compare_S : Compare.S.Valid.t (to_Compare_S H);
}.
Arguments t {_}.
End Valid.
Compare_S : Compare.S.Valid.t (to_Compare_S H);
}.
Arguments t {_}.
End Valid.
The projection [to_MINIMAL] preserves the field [equal].
Lemma to_Compare_equal_eq {t} (H : S.MINIMAL_HASH (t := t)) :
(to_Compare_S H).(Compare.S.equal) = H.(S.MINIMAL_HASH.equal).
Proof.
unfold to_Compare_S. reflexivity.
Qed.
(to_Compare_S H).(Compare.S.equal) = H.(S.MINIMAL_HASH.equal).
Proof.
unfold to_Compare_S. reflexivity.
Qed.
The [equal] field of a valid [H : S.Hash] is valid.
Lemma valid_implies_equal_valid {t} {H : S.MINIMAL_HASH (t := t)}:
Valid.t H → Compare.Equal.Valid.t (fun _ ⇒ True) H.(S.MINIMAL_HASH.equal).
Proof.
unfold Compare.Equal.Valid.t.
intros Hval.
destruct Hval as [Hval].
rewrite <- to_Compare_equal_eq.
remember (to_Compare_S H) as CH.
apply (@Compare.S.valid_implies_equal_valid t CH) in Hval.
unfold Compare.Equal.Valid.t in Hval.
apply Hval ; constructor.
Qed.
End MINIMAL_HASH.
Module RAW_DATA.
Module Valid.
Record t {t} {R : S.RAW_DATA (t := t)} : Prop := {
of_bytes_opt_to_bytes v :
R.(S.RAW_DATA.of_bytes_opt) (R.(S.RAW_DATA.to_bytes) v) =
Some v;
to_bytes_of_bytes_opt bytes :
match R.(S.RAW_DATA.of_bytes_opt) bytes with
| Some v ⇒ R.(S.RAW_DATA.to_bytes) v = bytes
| None ⇒ True
end;
}.
Arguments t {_}.
End Valid.
End RAW_DATA.
Module B58_DATA.
Module Valid.
Record t {t} (B : S.B58_DATA (t := t)) : Prop := {
of_to_b58_check value :
B.(S.B58_DATA.of_b58check_opt) (B.(S.B58_DATA.to_b58check) value) =
Some value;
to_of_b58_check string :
match B.(S.B58_DATA.of_b58check_opt) string with
| Some value ⇒ B.(S.B58_DATA.to_b58check) value = string
| None ⇒ True
end;
}.
End Valid.
End B58_DATA.
Module ENCODER.
Module Valid.
Record t {t : Set} {domain} {E : S.ENCODER (t := t)} : Prop := {
encoding : Data_encoding.Valid.t (fun _ ⇒ True) E.(S.ENCODER.encoding);
rpc_arg : RPC_arg.Valid.t domain E.(S.ENCODER.rpc_arg);
}.
Arguments t {_}.
End Valid.
End ENCODER.
Module HASH.
Definition to_MINIMAL_HASH {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.MINIMAL_HASH (t := t) := {|
S.MINIMAL_HASH.name := H.(S.HASH.name);
S.MINIMAL_HASH.title := H.(S.HASH.title);
S.MINIMAL_HASH.pp := H.(S.HASH.pp);
S.MINIMAL_HASH.pp_short := H.(S.HASH.pp_short);
S.MINIMAL_HASH.op_eq := H.(S.HASH.op_eq);
S.MINIMAL_HASH.op_ltgt := H.(S.HASH.op_ltgt);
S.MINIMAL_HASH.op_lt := H.(S.HASH.op_lt);
S.MINIMAL_HASH.op_lteq := H.(S.HASH.op_lteq);
S.MINIMAL_HASH.op_gteq := H.(S.HASH.op_gteq);
S.MINIMAL_HASH.op_gt := H.(S.HASH.op_gt);
S.MINIMAL_HASH.compare := H.(S.HASH.compare);
S.MINIMAL_HASH.equal := H.(S.HASH.equal);
S.MINIMAL_HASH.max := H.(S.HASH.max);
S.MINIMAL_HASH.min := H.(S.HASH.min);
S.MINIMAL_HASH.hash_bytes := H.(S.HASH.hash_bytes);
S.MINIMAL_HASH.hash_string := H.(S.HASH.hash_string);
S.MINIMAL_HASH.zero := H.(S.HASH.zero);
|}.
Valid.t H → Compare.Equal.Valid.t (fun _ ⇒ True) H.(S.MINIMAL_HASH.equal).
Proof.
unfold Compare.Equal.Valid.t.
intros Hval.
destruct Hval as [Hval].
rewrite <- to_Compare_equal_eq.
remember (to_Compare_S H) as CH.
apply (@Compare.S.valid_implies_equal_valid t CH) in Hval.
unfold Compare.Equal.Valid.t in Hval.
apply Hval ; constructor.
Qed.
End MINIMAL_HASH.
Module RAW_DATA.
Module Valid.
Record t {t} {R : S.RAW_DATA (t := t)} : Prop := {
of_bytes_opt_to_bytes v :
R.(S.RAW_DATA.of_bytes_opt) (R.(S.RAW_DATA.to_bytes) v) =
Some v;
to_bytes_of_bytes_opt bytes :
match R.(S.RAW_DATA.of_bytes_opt) bytes with
| Some v ⇒ R.(S.RAW_DATA.to_bytes) v = bytes
| None ⇒ True
end;
}.
Arguments t {_}.
End Valid.
End RAW_DATA.
Module B58_DATA.
Module Valid.
Record t {t} (B : S.B58_DATA (t := t)) : Prop := {
of_to_b58_check value :
B.(S.B58_DATA.of_b58check_opt) (B.(S.B58_DATA.to_b58check) value) =
Some value;
to_of_b58_check string :
match B.(S.B58_DATA.of_b58check_opt) string with
| Some value ⇒ B.(S.B58_DATA.to_b58check) value = string
| None ⇒ True
end;
}.
End Valid.
End B58_DATA.
Module ENCODER.
Module Valid.
Record t {t : Set} {domain} {E : S.ENCODER (t := t)} : Prop := {
encoding : Data_encoding.Valid.t (fun _ ⇒ True) E.(S.ENCODER.encoding);
rpc_arg : RPC_arg.Valid.t domain E.(S.ENCODER.rpc_arg);
}.
Arguments t {_}.
End Valid.
End ENCODER.
Module HASH.
Definition to_MINIMAL_HASH {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.MINIMAL_HASH (t := t) := {|
S.MINIMAL_HASH.name := H.(S.HASH.name);
S.MINIMAL_HASH.title := H.(S.HASH.title);
S.MINIMAL_HASH.pp := H.(S.HASH.pp);
S.MINIMAL_HASH.pp_short := H.(S.HASH.pp_short);
S.MINIMAL_HASH.op_eq := H.(S.HASH.op_eq);
S.MINIMAL_HASH.op_ltgt := H.(S.HASH.op_ltgt);
S.MINIMAL_HASH.op_lt := H.(S.HASH.op_lt);
S.MINIMAL_HASH.op_lteq := H.(S.HASH.op_lteq);
S.MINIMAL_HASH.op_gteq := H.(S.HASH.op_gteq);
S.MINIMAL_HASH.op_gt := H.(S.HASH.op_gt);
S.MINIMAL_HASH.compare := H.(S.HASH.compare);
S.MINIMAL_HASH.equal := H.(S.HASH.equal);
S.MINIMAL_HASH.max := H.(S.HASH.max);
S.MINIMAL_HASH.min := H.(S.HASH.min);
S.MINIMAL_HASH.hash_bytes := H.(S.HASH.hash_bytes);
S.MINIMAL_HASH.hash_string := H.(S.HASH.hash_string);
S.MINIMAL_HASH.zero := H.(S.HASH.zero);
|}.
The projection [to_MINIMAL] preserves the field [equal].
Lemma to_MINIMAL_equal_eq {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
(to_MINIMAL_HASH H).(MINIMAL_HASH.equal) = H.(S.HASH.equal).
Proof.
unfold to_MINIMAL_HASH. reflexivity.
Qed.
Definition to_RAW_DATA {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.RAW_DATA (t := t) := {|
S.RAW_DATA.size_value := H.(S.HASH.size_value);
S.RAW_DATA.to_bytes := H.(S.HASH.to_bytes);
S.RAW_DATA.of_bytes_opt := H.(S.HASH.of_bytes_opt);
S.RAW_DATA.of_bytes_exn := H.(S.HASH.of_bytes_exn);
|}.
Definition to_B58_DATA {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.B58_DATA (t := t) := {|
S.B58_DATA.to_b58check := H.(HASH.to_b58check);
S.B58_DATA.to_short_b58check := H.(HASH.to_short_b58check);
S.B58_DATA.of_b58check_exn := H.(HASH.of_b58check_exn);
S.B58_DATA.of_b58check_opt := H.(HASH.of_b58check_opt);
S.B58_DATA.b58check_encoding := H.(HASH.b58check_encoding);
|}.
Definition to_ENCODER {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.ENCODER (t := t) := {|
S.ENCODER.encoding := H.(S.HASH.encoding);
S.ENCODER.rpc_arg := H.(S.HASH.rpc_arg);
|}.
Definition to_INDEXES {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.INDEXES (t := t) := {|
S.INDEXES._Set := H.(S.HASH._Set);
S.INDEXES.Map := H.(S.HASH.Map);
|}.
Module Valid.
Record t {t Set_t Map_t} {domain}
{H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)} : Prop := {
MINIMAL_HASH : MINIMAL_HASH.Valid.t (to_MINIMAL_HASH H);
RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA H);
B58_DATA : B58_DATA.Valid.t (to_B58_DATA H);
ENCODER : ENCODER.Valid.t domain (to_ENCODER H);
}.
Arguments t {_ _ _}.
End Valid.
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
(to_MINIMAL_HASH H).(MINIMAL_HASH.equal) = H.(S.HASH.equal).
Proof.
unfold to_MINIMAL_HASH. reflexivity.
Qed.
Definition to_RAW_DATA {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.RAW_DATA (t := t) := {|
S.RAW_DATA.size_value := H.(S.HASH.size_value);
S.RAW_DATA.to_bytes := H.(S.HASH.to_bytes);
S.RAW_DATA.of_bytes_opt := H.(S.HASH.of_bytes_opt);
S.RAW_DATA.of_bytes_exn := H.(S.HASH.of_bytes_exn);
|}.
Definition to_B58_DATA {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.B58_DATA (t := t) := {|
S.B58_DATA.to_b58check := H.(HASH.to_b58check);
S.B58_DATA.to_short_b58check := H.(HASH.to_short_b58check);
S.B58_DATA.of_b58check_exn := H.(HASH.of_b58check_exn);
S.B58_DATA.of_b58check_opt := H.(HASH.of_b58check_opt);
S.B58_DATA.b58check_encoding := H.(HASH.b58check_encoding);
|}.
Definition to_ENCODER {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.ENCODER (t := t) := {|
S.ENCODER.encoding := H.(S.HASH.encoding);
S.ENCODER.rpc_arg := H.(S.HASH.rpc_arg);
|}.
Definition to_INDEXES {t Set_t Map_t}
(H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t))
: S.INDEXES (t := t) := {|
S.INDEXES._Set := H.(S.HASH._Set);
S.INDEXES.Map := H.(S.HASH.Map);
|}.
Module Valid.
Record t {t Set_t Map_t} {domain}
{H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)} : Prop := {
MINIMAL_HASH : MINIMAL_HASH.Valid.t (to_MINIMAL_HASH H);
RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA H);
B58_DATA : B58_DATA.Valid.t (to_B58_DATA H);
ENCODER : ENCODER.Valid.t domain (to_ENCODER H);
}.
Arguments t {_ _ _}.
End Valid.
The [equal] field of a valid [H : S.Hash] is valid.
Lemma valid_implies_equal_valid {t Set_t Map_t} {domain}
{H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)} :
Valid.t domain H → Compare.Equal.Valid.t (fun _ ⇒ True) H.(S.HASH.equal).
Proof.
unfold Compare.Equal.Valid.t.
intros Hval.
destruct Hval as [Hval _ _ _].
rewrite <- to_MINIMAL_equal_eq.
remember (to_MINIMAL_HASH H) as MH.
apply (@MINIMAL_HASH.valid_implies_equal_valid t MH).
assumption.
Qed.
End HASH.
Module MERKLE_TREE.
Definition to_HASH {elt t Set_t Map_t path}
(M : S.MERKLE_TREE
(elt := elt) (t := t) (Set_t := Set_t) (Map_t := Map_t) (path := path))
: S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t) := {|
S.HASH.name := M.(S.MERKLE_TREE.name);
S.HASH.title := M.(S.MERKLE_TREE.title);
S.HASH.pp := M.(S.MERKLE_TREE.pp);
S.HASH.pp_short := M.(S.MERKLE_TREE.pp_short);
S.HASH.op_eq := M.(S.MERKLE_TREE.op_eq);
S.HASH.op_ltgt := M.(S.MERKLE_TREE.op_ltgt);
S.HASH.op_lt := M.(S.MERKLE_TREE.op_lt);
S.HASH.op_lteq := M.(S.MERKLE_TREE.op_lteq);
S.HASH.op_gteq := M.(S.MERKLE_TREE.op_gteq);
S.HASH.op_gt := M.(S.MERKLE_TREE.op_gt);
S.HASH.compare := M.(S.MERKLE_TREE.compare);
S.HASH.equal := M.(S.MERKLE_TREE.equal);
S.HASH.max := M.(S.MERKLE_TREE.max);
S.HASH.min := M.(S.MERKLE_TREE.min);
S.HASH.hash_bytes := M.(S.MERKLE_TREE.hash_bytes);
S.HASH.hash_string := M.(S.MERKLE_TREE.hash_string);
S.HASH.zero := M.(S.MERKLE_TREE.zero);
S.HASH.size_value := M.(S.MERKLE_TREE.size_value);
S.HASH.to_bytes := M.(S.MERKLE_TREE.to_bytes);
S.HASH.of_bytes_opt := M.(S.MERKLE_TREE.of_bytes_opt);
S.HASH.of_bytes_exn := M.(S.MERKLE_TREE.of_bytes_exn);
S.HASH.to_b58check := M.(S.MERKLE_TREE.to_b58check);
S.HASH.to_short_b58check := M.(S.MERKLE_TREE.to_short_b58check);
S.HASH.of_b58check_exn := M.(S.MERKLE_TREE.of_b58check_exn);
S.HASH.of_b58check_opt := M.(S.MERKLE_TREE.of_b58check_opt);
S.HASH.b58check_encoding := M.(S.MERKLE_TREE.b58check_encoding);
S.HASH.encoding := M.(S.MERKLE_TREE.encoding);
S.HASH.rpc_arg := M.(S.MERKLE_TREE.rpc_arg);
S.HASH._Set := M.(S.MERKLE_TREE._Set);
S.HASH.Map := M.(S.MERKLE_TREE.Map);
|}.
Module Valid.
Record t {elt t Set_t Map_t path} {domain}
{M : S.MERKLE_TREE
(elt := elt) (t := t) (Set_t := Set_t) (Map_t := Map_t) (path := path)}
: Prop := {
HASH : HASH.Valid.t domain (to_HASH M);
path_encoding :
Data_encoding.Valid.t (fun _ ⇒ True) M.(S.MERKLE_TREE.path_encoding);
}.
Arguments t {_ _ _ _ _}.
End Valid.
End MERKLE_TREE.
Module SIGNATURE_PUBLIC_KEY_HASH.
Definition to_Compare_S {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
Compare.S (t := t) := {|
Compare.S.op_eq := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_eq);
Compare.S.op_ltgt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_ltgt);
Compare.S.op_lt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lt);
Compare.S.op_lteq := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lteq);
Compare.S.op_gteq := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gteq);
Compare.S.op_gt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gt);
Compare.S.compare := S.(S.SIGNATURE_PUBLIC_KEY_HASH.compare);
Compare.S.equal := S.(S.SIGNATURE_PUBLIC_KEY_HASH.equal);
Compare.S.max := S.(S.SIGNATURE_PUBLIC_KEY_HASH.max);
Compare.S.min := S.(S.SIGNATURE_PUBLIC_KEY_HASH.min);
|}.
Definition to_RAW_DATA {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
S.RAW_DATA (t := t) := {|
S.RAW_DATA.size_value := S.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value);
S.RAW_DATA.to_bytes := S.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes);
S.RAW_DATA.of_bytes_opt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_opt);
S.RAW_DATA.of_bytes_exn := S.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_exn);
|}.
Definition to_B58_DATA {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
S.B58_DATA (t := t) := {|
S.B58_DATA.to_b58check := S.(SIGNATURE_PUBLIC_KEY_HASH.to_b58check);
S.B58_DATA.to_short_b58check := S.(SIGNATURE_PUBLIC_KEY_HASH.to_short_b58check);
S.B58_DATA.of_b58check_exn := S.(SIGNATURE_PUBLIC_KEY_HASH.of_b58check_exn);
S.B58_DATA.of_b58check_opt := S.(SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt);
S.B58_DATA.b58check_encoding := S.(SIGNATURE_PUBLIC_KEY_HASH.b58check_encoding);
|}.
Definition to_ENCODER {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
S.ENCODER (t := t) := {|
S.ENCODER.encoding := S.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding);
S.ENCODER.rpc_arg := S.(S.SIGNATURE_PUBLIC_KEY_HASH.rpc_arg);
|}.
Definition to_INDEXES {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
S.INDEXES (t := t) := {|
S.INDEXES._Set := S.(S.SIGNATURE_PUBLIC_KEY_HASH._Set);
S.INDEXES.Map := S.(S.SIGNATURE_PUBLIC_KEY_HASH.Map);
|}.
Module Valid.
Record t {t Set_t Map_t} {domain}
{S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)} :
Prop := {
Compare_S : Compare.S.Valid.t (to_Compare_S S);
RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA S);
B58_DATA : B58_DATA.Valid.t (to_B58_DATA S);
ENCODER : ENCODER.Valid.t domain (to_ENCODER S);
}.
Arguments t {_ _ _}.
End Valid.
End SIGNATURE_PUBLIC_KEY_HASH.
Module SIGNATURE_PUBLIC_KEY.
Definition to_Compare_S {t public_key_hash_t}
(S :
S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)) :
Compare.S (t := t) := {|
Compare.S.op_eq := S.(S.SIGNATURE_PUBLIC_KEY.op_eq);
Compare.S.op_ltgt := S.(S.SIGNATURE_PUBLIC_KEY.op_ltgt);
Compare.S.op_lt := S.(S.SIGNATURE_PUBLIC_KEY.op_lt);
Compare.S.op_lteq := S.(S.SIGNATURE_PUBLIC_KEY.op_lteq);
Compare.S.op_gteq := S.(S.SIGNATURE_PUBLIC_KEY.op_gteq);
Compare.S.op_gt := S.(S.SIGNATURE_PUBLIC_KEY.op_gt);
Compare.S.compare := S.(S.SIGNATURE_PUBLIC_KEY.compare);
Compare.S.equal := S.(S.SIGNATURE_PUBLIC_KEY.equal);
Compare.S.max := S.(S.SIGNATURE_PUBLIC_KEY.max);
Compare.S.min := S.(S.SIGNATURE_PUBLIC_KEY.min);
|}.
Definition to_B58_DATA {t public_key_hash_t}
(S :
S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)) :
S.B58_DATA (t := t) := {|
S.B58_DATA.to_b58check := S.(SIGNATURE_PUBLIC_KEY.to_b58check);
S.B58_DATA.to_short_b58check := S.(SIGNATURE_PUBLIC_KEY.to_short_b58check);
S.B58_DATA.of_b58check_exn := S.(SIGNATURE_PUBLIC_KEY.of_b58check_exn);
S.B58_DATA.of_b58check_opt := S.(SIGNATURE_PUBLIC_KEY.of_b58check_opt);
S.B58_DATA.b58check_encoding := S.(SIGNATURE_PUBLIC_KEY.b58check_encoding);
|}.
Definition to_ENCODER {t public_key_hash_t}
(S :
S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)) :
S.ENCODER (t := t) := {|
S.ENCODER.encoding := S.(S.SIGNATURE_PUBLIC_KEY.encoding);
S.ENCODER.rpc_arg := S.(S.SIGNATURE_PUBLIC_KEY.rpc_arg);
|}.
Module Valid.
Record t {t public_key_hash_t} {domain}
{S :
S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)} :
Prop := {
Compare_S : Compare.S.Valid.t (to_Compare_S S);
B58_DATA : B58_DATA.Valid.t (to_B58_DATA S);
ENCODER : ENCODER.Valid.t domain (to_ENCODER S);
}.
Arguments t {_ _}.
End Valid.
End SIGNATURE_PUBLIC_KEY.
Module SIGNATURE.
Definition to_RAW_DATA {pkh pkh_set pkh_map pk t watermark}
(S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
) :
S.RAW_DATA (t := t) := {|
S.RAW_DATA.size_value := S.(S.SIGNATURE.size_value);
S.RAW_DATA.to_bytes := S.(S.SIGNATURE.to_bytes);
S.RAW_DATA.of_bytes_opt := S.(S.SIGNATURE.of_bytes_opt);
S.RAW_DATA.of_bytes_exn := S.(S.SIGNATURE.of_bytes_exn);
|}.
Definition to_Compare_S {pkh pkh_set pkh_map pk t watermark}
(S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
) :
Compare.S (t := t) := {|
Compare.S.op_eq := S.(S.SIGNATURE.op_eq);
Compare.S.op_ltgt := S.(S.SIGNATURE.op_ltgt);
Compare.S.op_lt := S.(S.SIGNATURE.op_lt);
Compare.S.op_lteq := S.(S.SIGNATURE.op_lteq);
Compare.S.op_gteq := S.(S.SIGNATURE.op_gteq);
Compare.S.op_gt := S.(S.SIGNATURE.op_gt);
Compare.S.compare := S.(S.SIGNATURE.compare);
Compare.S.equal := S.(S.SIGNATURE.equal);
Compare.S.max := S.(S.SIGNATURE.max);
Compare.S.min := S.(S.SIGNATURE.min);
|}.
Definition to_B58_DATA {pkh pkh_set pkh_map pk t watermark}
(S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
) :
S.B58_DATA (t := t) := {|
S.B58_DATA.to_b58check := S.(SIGNATURE.to_b58check);
S.B58_DATA.to_short_b58check := S.(SIGNATURE.to_short_b58check);
S.B58_DATA.of_b58check_exn := S.(SIGNATURE.of_b58check_exn);
S.B58_DATA.of_b58check_opt := S.(SIGNATURE.of_b58check_opt);
S.B58_DATA.b58check_encoding := S.(SIGNATURE.b58check_encoding);
|}.
Definition to_ENCODER {pkh pkh_set pkh_map pk t watermark}
(S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
) :
S.ENCODER (t := t) := {|
S.ENCODER.encoding := S.(S.SIGNATURE.encoding);
S.ENCODER.rpc_arg := S.(S.SIGNATURE.rpc_arg);
|}.
Module Valid.
Record t {pkh pkh_set pkh_map pk t watermark} {domain}
{S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
} :
Prop := {
Public_key_hash :
SIGNATURE_PUBLIC_KEY_HASH.Valid.t (fun _ ⇒ True)
S.(S.SIGNATURE.Public_key_hash);
Public_key :
SIGNATURE_PUBLIC_KEY.Valid.t (fun _ ⇒ True)
S.(S.SIGNATURE.Public_key);
RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA S);
Compare_S : Compare.S.Valid.t (to_Compare_S S);
B58_DATA : B58_DATA.Valid.t (to_B58_DATA S);
ENCODER : ENCODER.Valid.t domain (to_ENCODER S);
}.
Arguments t {_ _ _ _ _ _}.
End Valid.
End SIGNATURE.
{H : S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)} :
Valid.t domain H → Compare.Equal.Valid.t (fun _ ⇒ True) H.(S.HASH.equal).
Proof.
unfold Compare.Equal.Valid.t.
intros Hval.
destruct Hval as [Hval _ _ _].
rewrite <- to_MINIMAL_equal_eq.
remember (to_MINIMAL_HASH H) as MH.
apply (@MINIMAL_HASH.valid_implies_equal_valid t MH).
assumption.
Qed.
End HASH.
Module MERKLE_TREE.
Definition to_HASH {elt t Set_t Map_t path}
(M : S.MERKLE_TREE
(elt := elt) (t := t) (Set_t := Set_t) (Map_t := Map_t) (path := path))
: S.HASH (t := t) (Set_t := Set_t) (Map_t := Map_t) := {|
S.HASH.name := M.(S.MERKLE_TREE.name);
S.HASH.title := M.(S.MERKLE_TREE.title);
S.HASH.pp := M.(S.MERKLE_TREE.pp);
S.HASH.pp_short := M.(S.MERKLE_TREE.pp_short);
S.HASH.op_eq := M.(S.MERKLE_TREE.op_eq);
S.HASH.op_ltgt := M.(S.MERKLE_TREE.op_ltgt);
S.HASH.op_lt := M.(S.MERKLE_TREE.op_lt);
S.HASH.op_lteq := M.(S.MERKLE_TREE.op_lteq);
S.HASH.op_gteq := M.(S.MERKLE_TREE.op_gteq);
S.HASH.op_gt := M.(S.MERKLE_TREE.op_gt);
S.HASH.compare := M.(S.MERKLE_TREE.compare);
S.HASH.equal := M.(S.MERKLE_TREE.equal);
S.HASH.max := M.(S.MERKLE_TREE.max);
S.HASH.min := M.(S.MERKLE_TREE.min);
S.HASH.hash_bytes := M.(S.MERKLE_TREE.hash_bytes);
S.HASH.hash_string := M.(S.MERKLE_TREE.hash_string);
S.HASH.zero := M.(S.MERKLE_TREE.zero);
S.HASH.size_value := M.(S.MERKLE_TREE.size_value);
S.HASH.to_bytes := M.(S.MERKLE_TREE.to_bytes);
S.HASH.of_bytes_opt := M.(S.MERKLE_TREE.of_bytes_opt);
S.HASH.of_bytes_exn := M.(S.MERKLE_TREE.of_bytes_exn);
S.HASH.to_b58check := M.(S.MERKLE_TREE.to_b58check);
S.HASH.to_short_b58check := M.(S.MERKLE_TREE.to_short_b58check);
S.HASH.of_b58check_exn := M.(S.MERKLE_TREE.of_b58check_exn);
S.HASH.of_b58check_opt := M.(S.MERKLE_TREE.of_b58check_opt);
S.HASH.b58check_encoding := M.(S.MERKLE_TREE.b58check_encoding);
S.HASH.encoding := M.(S.MERKLE_TREE.encoding);
S.HASH.rpc_arg := M.(S.MERKLE_TREE.rpc_arg);
S.HASH._Set := M.(S.MERKLE_TREE._Set);
S.HASH.Map := M.(S.MERKLE_TREE.Map);
|}.
Module Valid.
Record t {elt t Set_t Map_t path} {domain}
{M : S.MERKLE_TREE
(elt := elt) (t := t) (Set_t := Set_t) (Map_t := Map_t) (path := path)}
: Prop := {
HASH : HASH.Valid.t domain (to_HASH M);
path_encoding :
Data_encoding.Valid.t (fun _ ⇒ True) M.(S.MERKLE_TREE.path_encoding);
}.
Arguments t {_ _ _ _ _}.
End Valid.
End MERKLE_TREE.
Module SIGNATURE_PUBLIC_KEY_HASH.
Definition to_Compare_S {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
Compare.S (t := t) := {|
Compare.S.op_eq := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_eq);
Compare.S.op_ltgt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_ltgt);
Compare.S.op_lt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lt);
Compare.S.op_lteq := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_lteq);
Compare.S.op_gteq := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gteq);
Compare.S.op_gt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.op_gt);
Compare.S.compare := S.(S.SIGNATURE_PUBLIC_KEY_HASH.compare);
Compare.S.equal := S.(S.SIGNATURE_PUBLIC_KEY_HASH.equal);
Compare.S.max := S.(S.SIGNATURE_PUBLIC_KEY_HASH.max);
Compare.S.min := S.(S.SIGNATURE_PUBLIC_KEY_HASH.min);
|}.
Definition to_RAW_DATA {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
S.RAW_DATA (t := t) := {|
S.RAW_DATA.size_value := S.(S.SIGNATURE_PUBLIC_KEY_HASH.size_value);
S.RAW_DATA.to_bytes := S.(S.SIGNATURE_PUBLIC_KEY_HASH.to_bytes);
S.RAW_DATA.of_bytes_opt := S.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_opt);
S.RAW_DATA.of_bytes_exn := S.(S.SIGNATURE_PUBLIC_KEY_HASH.of_bytes_exn);
|}.
Definition to_B58_DATA {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
S.B58_DATA (t := t) := {|
S.B58_DATA.to_b58check := S.(SIGNATURE_PUBLIC_KEY_HASH.to_b58check);
S.B58_DATA.to_short_b58check := S.(SIGNATURE_PUBLIC_KEY_HASH.to_short_b58check);
S.B58_DATA.of_b58check_exn := S.(SIGNATURE_PUBLIC_KEY_HASH.of_b58check_exn);
S.B58_DATA.of_b58check_opt := S.(SIGNATURE_PUBLIC_KEY_HASH.of_b58check_opt);
S.B58_DATA.b58check_encoding := S.(SIGNATURE_PUBLIC_KEY_HASH.b58check_encoding);
|}.
Definition to_ENCODER {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
S.ENCODER (t := t) := {|
S.ENCODER.encoding := S.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding);
S.ENCODER.rpc_arg := S.(S.SIGNATURE_PUBLIC_KEY_HASH.rpc_arg);
|}.
Definition to_INDEXES {t Set_t Map_t}
(S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)) :
S.INDEXES (t := t) := {|
S.INDEXES._Set := S.(S.SIGNATURE_PUBLIC_KEY_HASH._Set);
S.INDEXES.Map := S.(S.SIGNATURE_PUBLIC_KEY_HASH.Map);
|}.
Module Valid.
Record t {t Set_t Map_t} {domain}
{S :
S.SIGNATURE_PUBLIC_KEY_HASH (t := t) (Set_t := Set_t) (Map_t := Map_t)} :
Prop := {
Compare_S : Compare.S.Valid.t (to_Compare_S S);
RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA S);
B58_DATA : B58_DATA.Valid.t (to_B58_DATA S);
ENCODER : ENCODER.Valid.t domain (to_ENCODER S);
}.
Arguments t {_ _ _}.
End Valid.
End SIGNATURE_PUBLIC_KEY_HASH.
Module SIGNATURE_PUBLIC_KEY.
Definition to_Compare_S {t public_key_hash_t}
(S :
S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)) :
Compare.S (t := t) := {|
Compare.S.op_eq := S.(S.SIGNATURE_PUBLIC_KEY.op_eq);
Compare.S.op_ltgt := S.(S.SIGNATURE_PUBLIC_KEY.op_ltgt);
Compare.S.op_lt := S.(S.SIGNATURE_PUBLIC_KEY.op_lt);
Compare.S.op_lteq := S.(S.SIGNATURE_PUBLIC_KEY.op_lteq);
Compare.S.op_gteq := S.(S.SIGNATURE_PUBLIC_KEY.op_gteq);
Compare.S.op_gt := S.(S.SIGNATURE_PUBLIC_KEY.op_gt);
Compare.S.compare := S.(S.SIGNATURE_PUBLIC_KEY.compare);
Compare.S.equal := S.(S.SIGNATURE_PUBLIC_KEY.equal);
Compare.S.max := S.(S.SIGNATURE_PUBLIC_KEY.max);
Compare.S.min := S.(S.SIGNATURE_PUBLIC_KEY.min);
|}.
Definition to_B58_DATA {t public_key_hash_t}
(S :
S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)) :
S.B58_DATA (t := t) := {|
S.B58_DATA.to_b58check := S.(SIGNATURE_PUBLIC_KEY.to_b58check);
S.B58_DATA.to_short_b58check := S.(SIGNATURE_PUBLIC_KEY.to_short_b58check);
S.B58_DATA.of_b58check_exn := S.(SIGNATURE_PUBLIC_KEY.of_b58check_exn);
S.B58_DATA.of_b58check_opt := S.(SIGNATURE_PUBLIC_KEY.of_b58check_opt);
S.B58_DATA.b58check_encoding := S.(SIGNATURE_PUBLIC_KEY.b58check_encoding);
|}.
Definition to_ENCODER {t public_key_hash_t}
(S :
S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)) :
S.ENCODER (t := t) := {|
S.ENCODER.encoding := S.(S.SIGNATURE_PUBLIC_KEY.encoding);
S.ENCODER.rpc_arg := S.(S.SIGNATURE_PUBLIC_KEY.rpc_arg);
|}.
Module Valid.
Record t {t public_key_hash_t} {domain}
{S :
S.SIGNATURE_PUBLIC_KEY (t := t) (public_key_hash_t := public_key_hash_t)} :
Prop := {
Compare_S : Compare.S.Valid.t (to_Compare_S S);
B58_DATA : B58_DATA.Valid.t (to_B58_DATA S);
ENCODER : ENCODER.Valid.t domain (to_ENCODER S);
}.
Arguments t {_ _}.
End Valid.
End SIGNATURE_PUBLIC_KEY.
Module SIGNATURE.
Definition to_RAW_DATA {pkh pkh_set pkh_map pk t watermark}
(S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
) :
S.RAW_DATA (t := t) := {|
S.RAW_DATA.size_value := S.(S.SIGNATURE.size_value);
S.RAW_DATA.to_bytes := S.(S.SIGNATURE.to_bytes);
S.RAW_DATA.of_bytes_opt := S.(S.SIGNATURE.of_bytes_opt);
S.RAW_DATA.of_bytes_exn := S.(S.SIGNATURE.of_bytes_exn);
|}.
Definition to_Compare_S {pkh pkh_set pkh_map pk t watermark}
(S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
) :
Compare.S (t := t) := {|
Compare.S.op_eq := S.(S.SIGNATURE.op_eq);
Compare.S.op_ltgt := S.(S.SIGNATURE.op_ltgt);
Compare.S.op_lt := S.(S.SIGNATURE.op_lt);
Compare.S.op_lteq := S.(S.SIGNATURE.op_lteq);
Compare.S.op_gteq := S.(S.SIGNATURE.op_gteq);
Compare.S.op_gt := S.(S.SIGNATURE.op_gt);
Compare.S.compare := S.(S.SIGNATURE.compare);
Compare.S.equal := S.(S.SIGNATURE.equal);
Compare.S.max := S.(S.SIGNATURE.max);
Compare.S.min := S.(S.SIGNATURE.min);
|}.
Definition to_B58_DATA {pkh pkh_set pkh_map pk t watermark}
(S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
) :
S.B58_DATA (t := t) := {|
S.B58_DATA.to_b58check := S.(SIGNATURE.to_b58check);
S.B58_DATA.to_short_b58check := S.(SIGNATURE.to_short_b58check);
S.B58_DATA.of_b58check_exn := S.(SIGNATURE.of_b58check_exn);
S.B58_DATA.of_b58check_opt := S.(SIGNATURE.of_b58check_opt);
S.B58_DATA.b58check_encoding := S.(SIGNATURE.b58check_encoding);
|}.
Definition to_ENCODER {pkh pkh_set pkh_map pk t watermark}
(S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
) :
S.ENCODER (t := t) := {|
S.ENCODER.encoding := S.(S.SIGNATURE.encoding);
S.ENCODER.rpc_arg := S.(S.SIGNATURE.rpc_arg);
|}.
Module Valid.
Record t {pkh pkh_set pkh_map pk t watermark} {domain}
{S : S.SIGNATURE
(Public_key_hash_t := pkh)
(Public_key_hash_Set_t := pkh_set)
(Public_key_hash_Map_t := pkh_map)
(Public_key_t := pk)
(t := t)
(watermark := watermark)
} :
Prop := {
Public_key_hash :
SIGNATURE_PUBLIC_KEY_HASH.Valid.t (fun _ ⇒ True)
S.(S.SIGNATURE.Public_key_hash);
Public_key :
SIGNATURE_PUBLIC_KEY.Valid.t (fun _ ⇒ True)
S.(S.SIGNATURE.Public_key);
RAW_DATA : RAW_DATA.Valid.t (to_RAW_DATA S);
Compare_S : Compare.S.Valid.t (to_Compare_S S);
B58_DATA : B58_DATA.Valid.t (to_B58_DATA S);
ENCODER : ENCODER.Valid.t domain (to_ENCODER S);
}.
Arguments t {_ _ _ _ _ _}.
End Valid.
End SIGNATURE.