Skip to main content

🍃 Bls_signature.v

Environment

See proofs, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Proto_alpha.Environment.Bytes.

Parameter pk : Set.

Parameter pk_size_in_bytes : int.

Parameter unsafe_pk_of_bytes : Bytes.t pk.

Parameter pk_of_bytes_opt : Bytes.t option pk.

Parameter pk_to_bytes : pk Bytes.t.

Parameter signature : Set.

Parameter signature_size_in_bytes : int.

Parameter unsafe_signature_of_bytes : Bytes.t signature.

Parameter signature_of_bytes_opt : Bytes.t option signature.

Parameter signature_to_bytes : signature Bytes.t.

Parameter aggregate_signature_opt : list signature option signature.

Parameter verify : pk Bytes.t signature bool.

Parameter aggregate_verify : list (pk × Bytes.t) signature bool.