🍃 Bls12_381.v

Environment

Gitlab

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

Require TezosOfOCaml.Environment.Structs.V0.S.

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.