Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Module 0x1::bls12381

Contains functions for:

The minimum-pubkey-size variant of Boneh-Lynn-Shacham (BLS) signatures, where public keys are BLS12-381 elliptic-curve points in $\mathbb{G}_1$ and signatures are in $\mathbb{G}_2$, as per the IETF BLS draft standard.

use 0x1::error;
use 0x1::option;

Struct PublicKey

A validated public key that: (1) is a point in the prime-order subgroup of the BLS12-381 elliptic curve, and (2) is not the identity point

This struct can be used to verify a normal (non-aggregated) signature.

This struct can be combined with a ProofOfPossession struct in order to create a PublicKeyWithPop struct, which can be used to verify a multisignature.

struct PublicKey has copy, drop, store
Fields
bytes: vector<u8>

Struct ProofOfPossession

A proof-of-possession (PoP). Given such a struct and a PublicKey struct, one can construct a PublicKeyWithPoP (see below).

struct ProofOfPossession has copy, drop, store
Fields
bytes: vector<u8>

Struct PublicKeyWithPoP

A validated public key that had a successfully-verified proof-of-possession (PoP).

A vector of these structs can be either: (1) used to verify an aggregate signature (2) aggregated with other PublicKeyWithPoP structs into an AggrPublicKeysWithPoP, which in turn can be used to verify a multisignature

struct PublicKeyWithPoP has copy, drop, store
Fields
bytes: vector<u8>

Struct AggrPublicKeysWithPoP

An aggregation of public keys with verified PoPs, which can be used to verify multisignatures.

struct AggrPublicKeysWithPoP has copy, drop, store
Fields
bytes: vector<u8>

Struct Signature

A BLS signature. This can be either a: (1) normal (non-aggregated) signature (2) signature share (for a multisignature or aggregate signature)

struct Signature has copy, drop, store
Fields
bytes: vector<u8>

Struct AggrOrMultiSignature

An aggregation of BLS signatures. This can be either a: (4) aggregated signature (i.e., an aggregation of signatures s_i, each on a message m_i) (3) multisignature (i.e., an aggregation of signatures s_i, each on the same message m)

We distinguish between a Signature type and a AggrOrMultiSignature type to prevent developers from interchangeably calling verify_multisignature and verify_signature_share to verify both multisignatures and signature shares, which could create problems down the line.

struct AggrOrMultiSignature has copy, drop, store
Fields
bytes: vector<u8>

Constants

One of the given inputs has the wrong size.s

const EWRONG_SIZE: u64 = 2;

The caller was supposed to input one or more public keys.

const EZERO_PUBKEYS: u64 = 1;

The number of signers does not match the number of messages to be signed.

const E_NUM_SIGNERS_MUST_EQ_NUM_MESSAGES: u64 = 3;

The public key size, in bytes

const PUBLIC_KEY_NUM_BYTES: u64 = 48;

Random signature generated by running cargo test – bls12381_sample_signature –nocapture –include-ignored in crates/aptos-crypto. The associated SK is 07416693b6b32c84abe45578728e2379f525729e5b94762435a31e65ecc728da.

const RANDOM_PK: vector<u8> = [138, 83, 231, 174, 82, 112, 227, 231, 101, 205, 138, 64, 50, 194, 231, 124, 111, 126, 135, 164, 78, 187, 133, 191, 40, 164, 215, 134, 85, 101, 105, 143, 151, 83, 70, 113, 66, 98, 249, 228, 124, 111, 62, 13, 93, 149, 22, 96];

Random signature generated by running cargo test – bls12381_sample_signature –nocapture –include-ignored in crates/aptos-crypto. The message signed is “Hello Aptos!” and the associated SK is 07416693b6b32c84abe45578728e2379f525729e5b94762435a31e65ecc728da.

const RANDOM_SIGNATURE: vector<u8> = [160, 26, 101, 133, 79, 152, 125, 52, 52, 20, 155, 127, 8, 247, 7, 48, 227, 11, 36, 25, 132, 232, 113, 43, 194, 172, 168, 133, 214, 50, 170, 252, 237, 76, 63, 102, 18, 9, 222, 187, 107, 28, 134, 1, 50, 102, 35, 204, 22, 202, 47, 108, 158, 220, 83, 183, 184, 139, 116, 53, 251, 107, 5, 221, 236, 228, 24, 210, 195, 77, 198, 172, 162, 245, 161, 26, 121, 230, 119, 116, 88, 44, 20, 8, 74, 1, 220, 183, 130, 14, 76, 180, 186, 208, 234, 141];

The signature size, in bytes

const SIGNATURE_SIZE: u64 = 96;

Function public_key_from_bytes

Creates a new public key from a sequence of bytes.

public fun public_key_from_bytes(bytes: vector<u8>): option::Option<bls12381::PublicKey>
Implementation 
public fun public_key_from_bytes(bytes: vector<u8>): Option<PublicKey> {
    if (validate_pubkey_internal(bytes)) {
        option::some(PublicKey {
            bytes
        })
    } else {
        option::none<PublicKey>()
    }
}

Function public_key_to_bytes

Serializes a public key into 48 bytes.

public fun public_key_to_bytes(pk: &bls12381::PublicKey): vector<u8>
Implementation 
public fun public_key_to_bytes(pk: &PublicKey): vector<u8> {
    pk.bytes
}

Function proof_of_possession_from_bytes

Creates a new proof-of-possession (PoP) which can be later used to create a PublicKeyWithPoP struct,

public fun proof_of_possession_from_bytes(bytes: vector<u8>): bls12381::ProofOfPossession
Implementation 
public fun proof_of_possession_from_bytes(bytes: vector<u8>): ProofOfPossession {
    ProofOfPossession {
        bytes
    }
}

Function proof_of_possession_to_bytes

Serializes the signature into 96 bytes.

public fun proof_of_possession_to_bytes(pop: &bls12381::ProofOfPossession): vector<u8>
Implementation 
public fun proof_of_possession_to_bytes(pop: &ProofOfPossession): vector<u8> {
    pop.bytes
}

Function public_key_from_bytes_with_pop

Creates a PoP’d public key from a normal public key and a corresponding proof-of-possession.

public fun public_key_from_bytes_with_pop(pk_bytes: vector<u8>, pop: &bls12381::ProofOfPossession): option::Option<bls12381::PublicKeyWithPoP>
Implementation 
public fun public_key_from_bytes_with_pop(pk_bytes: vector<u8>, pop: &ProofOfPossession): Option<PublicKeyWithPoP> {
    if (verify_proof_of_possession_internal(pk_bytes, pop.bytes)) {
        option::some(PublicKeyWithPoP {
            bytes: pk_bytes
        })
    } else {
        option::none<PublicKeyWithPoP>()
    }
}

Function public_key_with_pop_to_normal

Creates a normal public key from a PoP’d public key.

public fun public_key_with_pop_to_normal(pkpop: &bls12381::PublicKeyWithPoP): bls12381::PublicKey
Implementation 
public fun public_key_with_pop_to_normal(pkpop: &PublicKeyWithPoP): PublicKey {
    PublicKey {
        bytes: pkpop.bytes
    }
}

Function public_key_with_pop_to_bytes

Serializes a PoP’d public key into 48 bytes.

public fun public_key_with_pop_to_bytes(pk: &bls12381::PublicKeyWithPoP): vector<u8>
Implementation 
public fun public_key_with_pop_to_bytes(pk: &PublicKeyWithPoP): vector<u8> {
    pk.bytes
}

Function signature_from_bytes

Creates a new signature from a sequence of bytes. Does not check the signature for prime-order subgroup membership since that is done implicitly during verification.

public fun signature_from_bytes(bytes: vector<u8>): bls12381::Signature
Implementation 
public fun signature_from_bytes(bytes: vector<u8>): Signature {
    Signature {
        bytes
    }
}

Function signature_to_bytes

Serializes the signature into 96 bytes.

public fun signature_to_bytes(sig: &bls12381::Signature): vector<u8>
Implementation 
public fun signature_to_bytes(sig: &Signature): vector<u8> {
    sig.bytes
}

Function signature_subgroup_check

Checks that the group element that defines a signature is in the prime-order subgroup. This check is implicitly performed when verifying any signature via this module, but we expose this functionality in case it might be useful for applications to easily dismiss invalid signatures early on.

public fun signature_subgroup_check(signature: &bls12381::Signature): bool
Implementation 
public fun signature_subgroup_check(signature: &Signature): bool {
    signature_subgroup_check_internal(signature.bytes)
}

Function aggregate_pubkeys

Given a vector of public keys with verified PoPs, combines them into an aggregated public key which can be used to verify multisignatures using verify_multisignature and aggregate signatures using verify_aggregate_signature. Aborts if no public keys are given as input.

public fun aggregate_pubkeys(public_keys: vector<bls12381::PublicKeyWithPoP>): bls12381::AggrPublicKeysWithPoP
Implementation 
public fun aggregate_pubkeys(public_keys: vector<PublicKeyWithPoP>): AggrPublicKeysWithPoP {
    let (bytes, success) = aggregate_pubkeys_internal(public_keys);
    assert!(success, std::error::invalid_argument(EZERO_PUBKEYS));

    AggrPublicKeysWithPoP {
        bytes
    }
}

Function aggregate_pubkey_to_bytes

Serializes an aggregate public key into 48 bytes.

public fun aggregate_pubkey_to_bytes(apk: &bls12381::AggrPublicKeysWithPoP): vector<u8>
Implementation 
public fun aggregate_pubkey_to_bytes(apk: &AggrPublicKeysWithPoP): vector<u8> {
    apk.bytes
}

Function aggregate_signatures

Aggregates the input signatures into an aggregate-or-multi-signature structure, which can be later verified via verify_aggregate_signature or verify_multisignature. Returns None if zero signatures are given as input or if some of the signatures are not valid group elements.

public fun aggregate_signatures(signatures: vector<bls12381::Signature>): option::Option<bls12381::AggrOrMultiSignature>
Implementation 
public fun aggregate_signatures(signatures: vector<Signature>): Option<AggrOrMultiSignature> {
    let (bytes, success) = aggregate_signatures_internal(signatures);
    if (success) {
        option::some(
            AggrOrMultiSignature {
                bytes
            }
        )
    } else {
        option::none<AggrOrMultiSignature>()
    }
}

Function aggr_or_multi_signature_to_bytes

Serializes an aggregate-or-multi-signature into 96 bytes.

public fun aggr_or_multi_signature_to_bytes(sig: &bls12381::AggrOrMultiSignature): vector<u8>
Implementation 
public fun aggr_or_multi_signature_to_bytes(sig: &AggrOrMultiSignature): vector<u8> {
    sig.bytes
}

Function aggr_or_multi_signature_from_bytes

Deserializes an aggregate-or-multi-signature from 96 bytes.

public fun aggr_or_multi_signature_from_bytes(bytes: vector<u8>): bls12381::AggrOrMultiSignature
Implementation 
public fun aggr_or_multi_signature_from_bytes(bytes: vector<u8>): AggrOrMultiSignature {
    assert!(bytes.length() == SIGNATURE_SIZE, std::error::invalid_argument(EWRONG_SIZE));

    AggrOrMultiSignature {
        bytes
    }
}

Function aggr_or_multi_signature_subgroup_check

Checks that the group element that defines an aggregate-or-multi-signature is in the prime-order subgroup.

public fun aggr_or_multi_signature_subgroup_check(signature: &bls12381::AggrOrMultiSignature): bool
Implementation 
public fun aggr_or_multi_signature_subgroup_check(signature: &AggrOrMultiSignature): bool {
    signature_subgroup_check_internal(signature.bytes)
}

Function verify_aggregate_signature

Verifies an aggregate signature, an aggregation of many signatures s_i, each on a different message m_i.

public fun verify_aggregate_signature(aggr_sig: &bls12381::AggrOrMultiSignature, public_keys: vector<bls12381::PublicKeyWithPoP>, messages: vector<vector<u8>>): bool
Implementation 
public fun verify_aggregate_signature(
    aggr_sig: &AggrOrMultiSignature,
    public_keys: vector<PublicKeyWithPoP>,
    messages: vector<vector<u8>>,
): bool {
    verify_aggregate_signature_internal(aggr_sig.bytes, public_keys, messages)
}

Function verify_multisignature

Verifies a multisignature: an aggregation of many signatures, each on the same message m.

public fun verify_multisignature(multisig: &bls12381::AggrOrMultiSignature, aggr_public_key: &bls12381::AggrPublicKeysWithPoP, message: vector<u8>): bool
Implementation 
public fun verify_multisignature(
    multisig: &AggrOrMultiSignature,
    aggr_public_key: &AggrPublicKeysWithPoP,
    message: vector<u8>
): bool {
    verify_multisignature_internal(multisig.bytes, aggr_public_key.bytes, message)
}

Function verify_normal_signature

Verifies a normal, non-aggregated signature.

public fun verify_normal_signature(signature: &bls12381::Signature, public_key: &bls12381::PublicKey, message: vector<u8>): bool
Implementation 
public fun verify_normal_signature(
    signature: &Signature,
    public_key: &PublicKey,
    message: vector<u8>
): bool {
    verify_normal_signature_internal(signature.bytes, public_key.bytes, message)
}

Function verify_signature_share

Verifies a signature share in the multisignature share or an aggregate signature share.

public fun verify_signature_share(signature_share: &bls12381::Signature, public_key: &bls12381::PublicKeyWithPoP, message: vector<u8>): bool
Implementation 
public fun verify_signature_share(
    signature_share: &Signature,
    public_key: &PublicKeyWithPoP,
    message: vector<u8>
): bool {
    verify_signature_share_internal(signature_share.bytes, public_key.bytes, message)
}

Function aggregate_pubkeys_internal

CRYPTOGRAPHY WARNING: This function assumes that the caller verified all public keys have a valid proof-of-possesion (PoP) using verify_proof_of_possession.

Given a vector of serialized public keys, combines them into an aggregated public key, returning (bytes, true), where bytes store the serialized public key. Aborts if no public keys are given as input.

fun aggregate_pubkeys_internal(public_keys: vector<bls12381::PublicKeyWithPoP>): (vector<u8>, bool)
Implementation 
native fun aggregate_pubkeys_internal(public_keys: vector<PublicKeyWithPoP>): (vector<u8>, bool);

Function aggregate_signatures_internal

CRYPTOGRAPHY WARNING: This function can be safely called without verifying that the input signatures are elements of the prime-order subgroup of the BLS12-381 curve.

Given a vector of serialized signatures, combines them into an aggregate signature, returning (bytes, true), where bytes store the serialized signature. Does not check the input signatures nor the final aggregated signatures for prime-order subgroup membership. Returns (_, false) if no signatures are given as input. Does not abort.

fun aggregate_signatures_internal(signatures: vector<bls12381::Signature>): (vector<u8>, bool)
Implementation 
native fun aggregate_signatures_internal(signatures: vector<Signature>): (vector<u8>, bool);

Function validate_pubkey_internal

Return true if the bytes in public_key are a valid BLS12-381 public key: (1) it is NOT the identity point, and (2) it is a BLS12-381 elliptic curve point, and (3) it is a prime-order point Return false otherwise. Does not abort.

fun validate_pubkey_internal(public_key: vector<u8>): bool
Implementation 
native fun validate_pubkey_internal(public_key: vector<u8>): bool;

Function signature_subgroup_check_internal

Return true if the elliptic curve point serialized in signature: (1) is NOT the identity point, and (2) is a BLS12-381 elliptic curve point, and (3) is a prime-order point Return false otherwise. Does not abort.

fun signature_subgroup_check_internal(signature: vector<u8>): bool
Implementation 
native fun signature_subgroup_check_internal(signature: vector<u8>): bool;

Function verify_aggregate_signature_internal

CRYPTOGRAPHY WARNING: First, this function assumes all public keys have a valid proof-of-possesion (PoP). This prevents both small-subgroup attacks and rogue-key attacks. Second, this function can be safely called without verifying that the aggregate signature is in the prime-order subgroup of the BLS12-381 curve.

Returns true if the aggregate signature aggsig on messages under public_keys verifies (where messages[i] should be signed by public_keys[i]).

Returns false if either:

  • no public keys or messages are given as input,
  • number of messages does not equal number of public keys
  • aggsig (1) is the identity point, or (2) is NOT a BLS12-381 elliptic curve point, or (3) is NOT a prime-order point Does not abort.
fun verify_aggregate_signature_internal(aggsig: vector<u8>, public_keys: vector<bls12381::PublicKeyWithPoP>, messages: vector<vector<u8>>): bool
Implementation 
native fun verify_aggregate_signature_internal(
    aggsig: vector<u8>,
    public_keys: vector<PublicKeyWithPoP>,
    messages: vector<vector<u8>>,
): bool;

Function verify_multisignature_internal

CRYPTOGRAPHY WARNING: This function assumes verified proofs-of-possesion (PoP) for the public keys used in computing the aggregate public key. This prevents small-subgroup attacks and rogue-key attacks.

Return true if the BLS multisignature on message verifies against the BLS aggregate public key agg_public_key. Returns false otherwise. Does not abort.

fun verify_multisignature_internal(multisignature: vector<u8>, agg_public_key: vector<u8>, message: vector<u8>): bool
Implementation 
native fun verify_multisignature_internal(
    multisignature: vector<u8>,
    agg_public_key: vector<u8>,
    message: vector<u8>
): bool;

Function verify_normal_signature_internal

CRYPTOGRAPHY WARNING: This function WILL check that the public key is a prime-order point, in order to prevent library users from misusing the library by forgetting to validate public keys before giving them as arguments to this function.

Returns true if the signature on message verifies under public key. Returns false otherwise. Does not abort.

fun verify_normal_signature_internal(signature: vector<u8>, public_key: vector<u8>, message: vector<u8>): bool
Implementation 
native fun verify_normal_signature_internal(
    signature: vector<u8>,
    public_key: vector<u8>,
    message: vector<u8>
): bool;

Function verify_proof_of_possession_internal

Return true if the bytes in public_key are a valid bls12381 public key (as per validate_pubkey) and this public key has a valid proof-of-possesion (PoP). Return false otherwise. Does not abort.

fun verify_proof_of_possession_internal(public_key: vector<u8>, proof_of_possesion: vector<u8>): bool
Implementation 
native fun verify_proof_of_possession_internal(
    public_key: vector<u8>,
    proof_of_possesion: vector<u8>
): bool;

Function verify_signature_share_internal

CRYPTOGRAPHY WARNING: Assumes the public key has a valid proof-of-possesion (PoP). This prevents rogue-key attacks later on during signature aggregation.

Returns true if the signature_share on message verifies under public key. Returns false otherwise, similar to verify_multisignature. Does not abort.

fun verify_signature_share_internal(signature_share: vector<u8>, public_key: vector<u8>, message: vector<u8>): bool
Implementation 
native fun verify_signature_share_internal(
    signature_share: vector<u8>,
    public_key: vector<u8>,
    message: vector<u8>
): bool;

Specification

Helper functions 

fun spec_aggregate_pubkeys_internal_1(public_keys: vector<PublicKeyWithPoP>): vector<u8>;


fun spec_public_key_from_bytes_with_pop(pk_bytes: vector<u8>, pop: ProofOfPossession): Option<PublicKeyWithPoP>;


fun spec_aggregate_pubkeys_internal_2(public_keys: vector<PublicKeyWithPoP>): bool;


fun spec_aggregate_signatures_internal_1(signatures: vector<Signature>): vector<u8>;


fun spec_aggregate_signatures_internal_2(signatures: vector<Signature>): bool;


fun spec_validate_pubkey_internal(public_key: vector<u8>): bool;


fun spec_signature_subgroup_check_internal(signature: vector<u8>): bool;


fun spec_verify_aggregate_signature_internal(
   aggsig: vector<u8>,
   public_keys: vector<PublicKeyWithPoP>,
   messages: vector<vector<u8>>,
): bool;


fun spec_verify_multisignature_internal(
   multisignature: vector<u8>,
   agg_public_key: vector<u8>,
   message: vector<u8>
): bool;


fun spec_verify_normal_signature_internal(
   signature: vector<u8>,
   public_key: vector<u8>,
   message: vector<u8>
): bool;


fun spec_verify_proof_of_possession_internal(
   public_key: vector<u8>,
   proof_of_possesion: vector<u8>
): bool;


fun spec_verify_signature_share_internal(
   signature_share: vector<u8>,
   public_key: vector<u8>,
   message: vector<u8>
): bool;

Function public_key_from_bytes 

public fun public_key_from_bytes(bytes: vector<u8>): option::Option<bls12381::PublicKey>

aborts_if false;
ensures spec_validate_pubkey_internal(bytes) ==> (std::option::is_some(result) && std::option::borrow(result).bytes == bytes);
ensures !spec_validate_pubkey_internal(bytes) ==> std::option::is_none(result);

Function public_key_from_bytes_with_pop 

public fun public_key_from_bytes_with_pop(pk_bytes: vector<u8>, pop: &bls12381::ProofOfPossession): option::Option<bls12381::PublicKeyWithPoP>

pragma opaque;
aborts_if false;
ensures spec_verify_proof_of_possession_internal(pk_bytes, pop.bytes) ==> (std::option::is_some(result) && std::option::borrow(result).bytes == pk_bytes);
ensures !spec_verify_proof_of_possession_internal(pk_bytes, pop.bytes) ==> std::option::is_none(result);
ensures [abstract] result == spec_public_key_from_bytes_with_pop(pk_bytes, pop);

Function aggregate_pubkeys 

public fun aggregate_pubkeys(public_keys: vector<bls12381::PublicKeyWithPoP>): bls12381::AggrPublicKeysWithPoP

let bytes = spec_aggregate_pubkeys_internal_1(public_keys);
let success = spec_aggregate_pubkeys_internal_2(public_keys);
aborts_if !success;
ensures result.bytes == bytes;

Function aggregate_signatures 

public fun aggregate_signatures(signatures: vector<bls12381::Signature>): option::Option<bls12381::AggrOrMultiSignature>

aborts_if false;
let bytes = spec_aggregate_signatures_internal_1(signatures);
let success = spec_aggregate_signatures_internal_2(signatures);
ensures success ==> (std::option::is_some(result) && std::option::borrow(result).bytes == bytes);
ensures !success ==> std::option::is_none(result);

Function aggr_or_multi_signature_from_bytes 

public fun aggr_or_multi_signature_from_bytes(bytes: vector<u8>): bls12381::AggrOrMultiSignature

aborts_if len(bytes) != SIGNATURE_SIZE;
ensures result.bytes == bytes;

Function aggr_or_multi_signature_subgroup_check 

public fun aggr_or_multi_signature_subgroup_check(signature: &bls12381::AggrOrMultiSignature): bool

aborts_if false;
ensures result == spec_signature_subgroup_check_internal(signature.bytes);

Function verify_aggregate_signature 

public fun verify_aggregate_signature(aggr_sig: &bls12381::AggrOrMultiSignature, public_keys: vector<bls12381::PublicKeyWithPoP>, messages: vector<vector<u8>>): bool

aborts_if false;
ensures result == spec_verify_aggregate_signature_internal(aggr_sig.bytes, public_keys, messages);

Function verify_multisignature 

public fun verify_multisignature(multisig: &bls12381::AggrOrMultiSignature, aggr_public_key: &bls12381::AggrPublicKeysWithPoP, message: vector<u8>): bool

aborts_if false;
ensures result == spec_verify_multisignature_internal(multisig.bytes, aggr_public_key.bytes, message);

Function verify_normal_signature 

public fun verify_normal_signature(signature: &bls12381::Signature, public_key: &bls12381::PublicKey, message: vector<u8>): bool

aborts_if false;
ensures result == spec_verify_normal_signature_internal(signature.bytes, public_key.bytes, message);

Function verify_signature_share 

public fun verify_signature_share(signature_share: &bls12381::Signature, public_key: &bls12381::PublicKeyWithPoP, message: vector<u8>): bool

aborts_if false;
ensures result == spec_verify_signature_share_internal(signature_share.bytes, public_key.bytes, message);

Function aggregate_pubkeys_internal 

fun aggregate_pubkeys_internal(public_keys: vector<bls12381::PublicKeyWithPoP>): (vector<u8>, bool)

pragma opaque;
aborts_if [abstract] false;
ensures result_1 == spec_aggregate_pubkeys_internal_1(public_keys);
ensures result_2 == spec_aggregate_pubkeys_internal_2(public_keys);

Function aggregate_signatures_internal 

fun aggregate_signatures_internal(signatures: vector<bls12381::Signature>): (vector<u8>, bool)

pragma opaque;
aborts_if [abstract] false;
ensures result_1 == spec_aggregate_signatures_internal_1(signatures);
ensures result_2 == spec_aggregate_signatures_internal_2(signatures);

Function validate_pubkey_internal 

fun validate_pubkey_internal(public_key: vector<u8>): bool

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_validate_pubkey_internal(public_key);

Function signature_subgroup_check_internal 

fun signature_subgroup_check_internal(signature: vector<u8>): bool

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_signature_subgroup_check_internal(signature);

Function verify_aggregate_signature_internal 

fun verify_aggregate_signature_internal(aggsig: vector<u8>, public_keys: vector<bls12381::PublicKeyWithPoP>, messages: vector<vector<u8>>): bool

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_verify_aggregate_signature_internal(aggsig, public_keys, messages);

Function verify_multisignature_internal 

fun verify_multisignature_internal(multisignature: vector<u8>, agg_public_key: vector<u8>, message: vector<u8>): bool

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_verify_multisignature_internal(multisignature, agg_public_key, message);

Function verify_normal_signature_internal 

fun verify_normal_signature_internal(signature: vector<u8>, public_key: vector<u8>, message: vector<u8>): bool

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_verify_normal_signature_internal(signature, public_key, message);

Function verify_proof_of_possession_internal 

fun verify_proof_of_possession_internal(public_key: vector<u8>, proof_of_possesion: vector<u8>): bool

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_verify_proof_of_possession_internal(public_key, proof_of_possesion);

Function verify_signature_share_internal 

fun verify_signature_share_internal(signature_share: vector<u8>, public_key: vector<u8>, message: vector<u8>): bool

pragma opaque;
aborts_if [abstract] false;
ensures result == spec_verify_signature_share_internal(signature_share, public_key, message);