🍃 Signature.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Chain_id.
Require TezosOfOCaml.Environment.Structs.V0.Ed25519.
Require TezosOfOCaml.Environment.Structs.V0.P256.
Require TezosOfOCaml.Environment.Structs.V0.S.
Require TezosOfOCaml.Environment.Structs.V0.Secp256k1.
Inductive public_key_hash : Set :=
| Ed25519Hash :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) → public_key_hash
| Secp256k1Hash :
Secp256k1.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) → public_key_hash
| P256Hash :
P256.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) → public_key_hash.
Inductive public_key : Set :=
| Ed25519 : Ed25519.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → public_key
| Secp256k1 : Secp256k1.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → public_key
| P256 : P256.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → public_key.
Inductive watermark : Set :=
| Block_header : Chain_id.t → watermark
| Endorsement : Chain_id.t → watermark
| Generic_operation : watermark
| Custom : bytes → watermark.
Parameter Included_SIGNATURE_Public_key_hash_Set_t : Set.
Parameter Included_SIGNATURE_Public_key_hash_Map_t : Set → Set.
Parameter Included_SIGNATURE_t : Set.
Parameter Included_SIGNATURE :
S.SIGNATURE (Public_key_hash_t := public_key_hash)
(Public_key_hash_Set_t := Included_SIGNATURE_Public_key_hash_Set_t)
(Public_key_hash_Map_t := Included_SIGNATURE_Public_key_hash_Map_t)
(Public_key_t := public_key) (t := Included_SIGNATURE_t)
(watermark := watermark).
Definition Public_key_hash :=
Included_SIGNATURE.(S.SIGNATURE.Public_key_hash).
Definition Public_key := Included_SIGNATURE.(S.SIGNATURE.Public_key).
Definition t := Included_SIGNATURE.(S.SIGNATURE.t).
Definition pp : Format.formatter → t → unit :=
Included_SIGNATURE.(S.SIGNATURE.pp).
Definition size_value : int := Included_SIGNATURE.(S.SIGNATURE.size_value).
Definition to_bytes : t → bytes := Included_SIGNATURE.(S.SIGNATURE.to_bytes).
Definition of_bytes_opt : bytes → option t :=
Included_SIGNATURE.(S.SIGNATURE.of_bytes_opt).
Definition of_bytes_exn : bytes → t :=
Included_SIGNATURE.(S.SIGNATURE.of_bytes_exn).
Definition op_eq : t → t → bool := Included_SIGNATURE.(S.SIGNATURE.op_eq).
Definition op_ltgt : t → t → bool :=
Included_SIGNATURE.(S.SIGNATURE.op_ltgt).
Definition op_lt : t → t → bool := Included_SIGNATURE.(S.SIGNATURE.op_lt).
Definition op_lteq : t → t → bool :=
Included_SIGNATURE.(S.SIGNATURE.op_lteq).
Definition op_gteq : t → t → bool :=
Included_SIGNATURE.(S.SIGNATURE.op_gteq).
Definition op_gt : t → t → bool := Included_SIGNATURE.(S.SIGNATURE.op_gt).
Definition compare : t → t → int :=
Included_SIGNATURE.(S.SIGNATURE.compare).
Definition equal : t → t → bool := Included_SIGNATURE.(S.SIGNATURE.equal).
Definition max : t → t → t := Included_SIGNATURE.(S.SIGNATURE.max).
Definition min : t → t → t := Included_SIGNATURE.(S.SIGNATURE.min).
Definition to_b58check : t → string :=
Included_SIGNATURE.(S.SIGNATURE.to_b58check).
Definition to_short_b58check : t → string :=
Included_SIGNATURE.(S.SIGNATURE.to_short_b58check).
Definition of_b58check_exn : string → t :=
Included_SIGNATURE.(S.SIGNATURE.of_b58check_exn).
Definition of_b58check_opt : string → option t :=
Included_SIGNATURE.(S.SIGNATURE.of_b58check_opt).
Definition b58check_encoding : Base58.encoding t :=
Included_SIGNATURE.(S.SIGNATURE.b58check_encoding).
Definition encoding : Data_encoding.t t :=
Included_SIGNATURE.(S.SIGNATURE.encoding).
Definition rpc_arg : RPC_arg.t t := Included_SIGNATURE.(S.SIGNATURE.rpc_arg).
Definition zero : t := Included_SIGNATURE.(S.SIGNATURE.zero).
Definition check : option watermark → public_key → t → bytes → bool :=
Included_SIGNATURE.(S.SIGNATURE.check).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Chain_id.
Require TezosOfOCaml.Environment.Structs.V0.Ed25519.
Require TezosOfOCaml.Environment.Structs.V0.P256.
Require TezosOfOCaml.Environment.Structs.V0.S.
Require TezosOfOCaml.Environment.Structs.V0.Secp256k1.
Inductive public_key_hash : Set :=
| Ed25519Hash :
Ed25519.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) → public_key_hash
| Secp256k1Hash :
Secp256k1.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) → public_key_hash
| P256Hash :
P256.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.t) → public_key_hash.
Inductive public_key : Set :=
| Ed25519 : Ed25519.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → public_key
| Secp256k1 : Secp256k1.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → public_key
| P256 : P256.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → public_key.
Inductive watermark : Set :=
| Block_header : Chain_id.t → watermark
| Endorsement : Chain_id.t → watermark
| Generic_operation : watermark
| Custom : bytes → watermark.
Parameter Included_SIGNATURE_Public_key_hash_Set_t : Set.
Parameter Included_SIGNATURE_Public_key_hash_Map_t : Set → Set.
Parameter Included_SIGNATURE_t : Set.
Parameter Included_SIGNATURE :
S.SIGNATURE (Public_key_hash_t := public_key_hash)
(Public_key_hash_Set_t := Included_SIGNATURE_Public_key_hash_Set_t)
(Public_key_hash_Map_t := Included_SIGNATURE_Public_key_hash_Map_t)
(Public_key_t := public_key) (t := Included_SIGNATURE_t)
(watermark := watermark).
Definition Public_key_hash :=
Included_SIGNATURE.(S.SIGNATURE.Public_key_hash).
Definition Public_key := Included_SIGNATURE.(S.SIGNATURE.Public_key).
Definition t := Included_SIGNATURE.(S.SIGNATURE.t).
Definition pp : Format.formatter → t → unit :=
Included_SIGNATURE.(S.SIGNATURE.pp).
Definition size_value : int := Included_SIGNATURE.(S.SIGNATURE.size_value).
Definition to_bytes : t → bytes := Included_SIGNATURE.(S.SIGNATURE.to_bytes).
Definition of_bytes_opt : bytes → option t :=
Included_SIGNATURE.(S.SIGNATURE.of_bytes_opt).
Definition of_bytes_exn : bytes → t :=
Included_SIGNATURE.(S.SIGNATURE.of_bytes_exn).
Definition op_eq : t → t → bool := Included_SIGNATURE.(S.SIGNATURE.op_eq).
Definition op_ltgt : t → t → bool :=
Included_SIGNATURE.(S.SIGNATURE.op_ltgt).
Definition op_lt : t → t → bool := Included_SIGNATURE.(S.SIGNATURE.op_lt).
Definition op_lteq : t → t → bool :=
Included_SIGNATURE.(S.SIGNATURE.op_lteq).
Definition op_gteq : t → t → bool :=
Included_SIGNATURE.(S.SIGNATURE.op_gteq).
Definition op_gt : t → t → bool := Included_SIGNATURE.(S.SIGNATURE.op_gt).
Definition compare : t → t → int :=
Included_SIGNATURE.(S.SIGNATURE.compare).
Definition equal : t → t → bool := Included_SIGNATURE.(S.SIGNATURE.equal).
Definition max : t → t → t := Included_SIGNATURE.(S.SIGNATURE.max).
Definition min : t → t → t := Included_SIGNATURE.(S.SIGNATURE.min).
Definition to_b58check : t → string :=
Included_SIGNATURE.(S.SIGNATURE.to_b58check).
Definition to_short_b58check : t → string :=
Included_SIGNATURE.(S.SIGNATURE.to_short_b58check).
Definition of_b58check_exn : string → t :=
Included_SIGNATURE.(S.SIGNATURE.of_b58check_exn).
Definition of_b58check_opt : string → option t :=
Included_SIGNATURE.(S.SIGNATURE.of_b58check_opt).
Definition b58check_encoding : Base58.encoding t :=
Included_SIGNATURE.(S.SIGNATURE.b58check_encoding).
Definition encoding : Data_encoding.t t :=
Included_SIGNATURE.(S.SIGNATURE.encoding).
Definition rpc_arg : RPC_arg.t t := Included_SIGNATURE.(S.SIGNATURE.rpc_arg).
Definition zero : t := Included_SIGNATURE.(S.SIGNATURE.zero).
Definition check : option watermark → public_key → t → bytes → bool :=
Included_SIGNATURE.(S.SIGNATURE.check).