🍃 Bls.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.S.
Parameter Included_AGGREGATE_SIGNATURE_Public_key_hash_t : Set.
Parameter Included_AGGREGATE_SIGNATURE_Public_key_hash_Set_t : Set.
Parameter Included_AGGREGATE_SIGNATURE_Public_key_hash_Map_t : Set → Set.
Parameter Included_AGGREGATE_SIGNATURE_Public_key_t : Set.
Parameter Included_AGGREGATE_SIGNATURE_t : Set.
Parameter Included_AGGREGATE_SIGNATURE :
S.AGGREGATE_SIGNATURE
(Public_key_hash_t := Included_AGGREGATE_SIGNATURE_Public_key_hash_t)
(Public_key_hash_Set_t :=
Included_AGGREGATE_SIGNATURE_Public_key_hash_Set_t)
(Public_key_hash_Map_t :=
Included_AGGREGATE_SIGNATURE_Public_key_hash_Map_t)
(Public_key_t := Included_AGGREGATE_SIGNATURE_Public_key_t)
(t := Included_AGGREGATE_SIGNATURE_t) (watermark := bytes).
Definition Public_key_hash :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.Public_key_hash).
Definition Public_key :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.Public_key).
Definition t := Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.t).
Definition pp : Format.formatter → t → unit :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.pp).
Definition size_value : int :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.size_value).
Definition to_bytes : t → bytes :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.to_bytes).
Definition of_bytes_opt : bytes → option t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_bytes_opt).
Definition of_bytes_exn : bytes → t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_bytes_exn).
Definition op_eq : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_eq).
Definition op_ltgt : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_ltgt).
Definition op_lt : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_lt).
Definition op_lteq : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_lteq).
Definition op_gteq : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_gteq).
Definition op_gt : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_gt).
Definition compare : t → t → int :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.compare).
Definition equal : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.equal).
Definition max : t → t → t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.max).
Definition min : t → t → t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.min).
Definition to_b58check : t → string :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.to_b58check).
Definition to_short_b58check : t → string :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.to_short_b58check).
Definition of_b58check_exn : string → t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_b58check_exn).
Definition of_b58check_opt : string → option t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_b58check_opt).
Definition b58check_encoding : Base58.encoding t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.b58check_encoding).
Definition encoding : Data_encoding.t t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.encoding).
Definition rpc_arg : RPC_arg.t t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.rpc_arg).
Definition zero : t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.zero).
Definition check :
option bytes → Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → t → bytes → bool
:= Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.check).
Definition aggregate_check :
list (Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × option bytes × bytes) → t →
bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.aggregate_check).
Definition aggregate_signature_opt : list t → option t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.aggregate_signature_opt).
Module Primitive.
Parameter Fr_t : Set.
Parameter Fr : S.PRIME_FIELD (t := Fr_t).
Parameter G1_t : Set.
Parameter G1 : S.CURVE (t := G1_t) (Scalar_t := Fr.(S.PRIME_FIELD.t)).
Parameter G2_t : Set.
Parameter G2 : S.CURVE (t := G2_t) (Scalar_t := Fr.(S.PRIME_FIELD.t)).
Parameter pairing_check : list (G1.(S.CURVE.t) × G2.(S.CURVE.t)) → bool.
End Primitive.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.S.
Parameter Included_AGGREGATE_SIGNATURE_Public_key_hash_t : Set.
Parameter Included_AGGREGATE_SIGNATURE_Public_key_hash_Set_t : Set.
Parameter Included_AGGREGATE_SIGNATURE_Public_key_hash_Map_t : Set → Set.
Parameter Included_AGGREGATE_SIGNATURE_Public_key_t : Set.
Parameter Included_AGGREGATE_SIGNATURE_t : Set.
Parameter Included_AGGREGATE_SIGNATURE :
S.AGGREGATE_SIGNATURE
(Public_key_hash_t := Included_AGGREGATE_SIGNATURE_Public_key_hash_t)
(Public_key_hash_Set_t :=
Included_AGGREGATE_SIGNATURE_Public_key_hash_Set_t)
(Public_key_hash_Map_t :=
Included_AGGREGATE_SIGNATURE_Public_key_hash_Map_t)
(Public_key_t := Included_AGGREGATE_SIGNATURE_Public_key_t)
(t := Included_AGGREGATE_SIGNATURE_t) (watermark := bytes).
Definition Public_key_hash :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.Public_key_hash).
Definition Public_key :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.Public_key).
Definition t := Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.t).
Definition pp : Format.formatter → t → unit :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.pp).
Definition size_value : int :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.size_value).
Definition to_bytes : t → bytes :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.to_bytes).
Definition of_bytes_opt : bytes → option t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_bytes_opt).
Definition of_bytes_exn : bytes → t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_bytes_exn).
Definition op_eq : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_eq).
Definition op_ltgt : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_ltgt).
Definition op_lt : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_lt).
Definition op_lteq : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_lteq).
Definition op_gteq : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_gteq).
Definition op_gt : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.op_gt).
Definition compare : t → t → int :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.compare).
Definition equal : t → t → bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.equal).
Definition max : t → t → t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.max).
Definition min : t → t → t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.min).
Definition to_b58check : t → string :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.to_b58check).
Definition to_short_b58check : t → string :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.to_short_b58check).
Definition of_b58check_exn : string → t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_b58check_exn).
Definition of_b58check_opt : string → option t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.of_b58check_opt).
Definition b58check_encoding : Base58.encoding t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.b58check_encoding).
Definition encoding : Data_encoding.t t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.encoding).
Definition rpc_arg : RPC_arg.t t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.rpc_arg).
Definition zero : t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.zero).
Definition check :
option bytes → Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → t → bytes → bool
:= Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.check).
Definition aggregate_check :
list (Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × option bytes × bytes) → t →
bool :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.aggregate_check).
Definition aggregate_signature_opt : list t → option t :=
Included_AGGREGATE_SIGNATURE.(S.AGGREGATE_SIGNATURE.aggregate_signature_opt).
Module Primitive.
Parameter Fr_t : Set.
Parameter Fr : S.PRIME_FIELD (t := Fr_t).
Parameter G1_t : Set.
Parameter G1 : S.CURVE (t := G1_t) (Scalar_t := Fr.(S.PRIME_FIELD.t)).
Parameter G2_t : Set.
Parameter G2 : S.CURVE (t := G2_t) (Scalar_t := Fr.(S.PRIME_FIELD.t)).
Parameter pairing_check : list (G1.(S.CURVE.t) × G2.(S.CURVE.t)) → bool.
End Primitive.