packages feed

pairing (empty) → 0.1.0

raw patch · 21 files changed

+1955/−0 lines, 21 filesdep +QuickCheckdep +basedep +bytestring

Dependencies added: QuickCheck, base, bytestring, criterion, cryptonite, memory, pairing, protolude, random, tasty, tasty-discover, tasty-hunit, tasty-quickcheck, wl-pprint-text

Files

+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Changelog for pairing++## 0.1++* Initial release.
+ LICENSE view
@@ -0,0 +1,19 @@+Copyright (c) 2018-2019 Adjoint Inc.++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR+OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE+OR OTHER DEALINGS IN THE SOFTWARE.
+ README.md view
@@ -0,0 +1,164 @@+<p align="center">+  <a href="http://www.adjoint.io"><img src="https://www.adjoint.io/assets/img/adjoint-logo@2x.png" width="250"/></a>+</p>++[![CircleCI](https://circleci.com/gh/adjoint-io/pairing.svg?style=svg&circle-token=ac95d02ba07e02b88585397f91cfe92a8c833343)](https://circleci.com/gh/adjoint-io/pairing)++Implementation of the Barreto-Naehrig (BN) curve construction from+[[BCTV2015]](https://eprint.iacr.org/2013/879.pdf) to provide two cyclic groups+**G<sub>1</sub>** and **G<sub>2</sub>**, with an efficient bilinear pairing:++*e: G<sub>1</sub> × G<sub>2</sub> → G<sub>T</sub>*++# Pairing++Let G<sub>1</sub>, G<sub>2</sub> and G<sub>T</sub> be abelian groups of prime order `q` and let `g` and `h` elements of G<sub>1</sub> and G<sub>2</sub> respectively . A pairing is a non-degenerate bilinear map e: G<sub>1</sub> × G<sub>2</sub> → G<sub>T</sub>.++This bilinearity property is what makes pairings such a powerful primitive in cryptography. It satisfies:+- e(g<sub>1</sub> + g<sub>2</sub>, h) = e(g<sub>1</sub>, h) e(g<sub>2</sub>, h)+- e(g, h<sub>1</sub> + h<sub>2</sub>) = e(g, h<sub>1</sub>) e(g, h<sub>2</sub>)+++The non-degeneracy property guarantees non-trivial pairings for non-trivial arguments. In other words, being non-degenerate means that:+- ∀ g ≠ 1, ∃ h<sub>i</sub> ∈ G<sub>2</sub> such that e(g, h<sub>i</sub>) ≠ 1+- ∀ h ≠ 1, ∃ g<sub>i</sub> ∈ G<sub>1</sub> such that e(g<sub>i</sub>, h) ≠ 1++An example of a pairing would be the scalar product on euclidean space <.> : R<sup>n</sup> × R<sup>n</sup> → R++## Example Usage++A simple example of calculating the optimal ate pairing given two points in G<sub>1</sub> and G<sub>2</sub>.++```haskell+import Protolude++import Pairing.Group+import Pairing.Pairing+import Pairing.Point+import Pairing.Fq (Fq(..))+import Pairing.Fq2 (Fq2(..))++e1 :: G1+e1 = Point+        (Fq 1368015179489954701390400359078579693043519447331113978918064868415326638035)+        (Fq 9918110051302171585080402603319702774565515993150576347155970296011118125764)+++e2 :: G2+e2 = Point+        (Fq2+         (Fq 2725019753478801796453339367788033689375851816420509565303521482350756874229)+          (Fq 7273165102799931111715871471550377909735733521218303035754523677688038059653 )+          )+        (Fq2+         (Fq 2512659008974376214222774206987427162027254181373325676825515531566330959255)+         (Fq 957874124722006818841961785324909313781880061366718538693995380805373202866)+        )+++main :: IO ()+main  = do+  putText "Ate pairing:"+  print (atePairing e1 e2)+  let +    lhs = reducedPairing (gMul e1 2) (gMul e2 3)+    rhs = (reducedPairing e1 e2)^(2 * 3)+  putText "Is bilinear:" +  print (lhs == rhs)+```++## Pairings in cryptography++Pairings are used in encryption algorithms, such as identity-based encryption (IBE), attribute-based encryption (ABE), (inner-product) predicate encryption, short broadcast encryption and searchable encryption, among others. It allows strong encryption with small signature sizes.++## Admissible Pairings++A pairing `e` is called admissible pairing if it is efficiently computable. The only admissible pairings that are suitable for cryptography are the Weil and Tate pairings on algebraic curves and their variants. Let `r` be the order of a group and E[r] be the entire group of points of order `r` on E(F<sub>q</sub>). E[r] is called the r-torsion and is defined as E[r] = { P ∈ E(F<sub>q</sub>) | rP = O }. Both Weil and Tate pairings require that `P` and `Q` come from disjoint cyclic subgroups of the same prime order `r`. Lagrange's theorem states that for any finite group `G`, the order (number of elements) of every subgroup `H` of `G` divides the order of `G`. Therefore, r | #E(F<sub>q</sub>).++G<sub>1</sub> and G<sub>2</sub> are subgroups of a group defined in an elliptic curve over an extension of a finite field F<sub>q</sub>, namely E(F<sub>q<sup>k</sup></sub>), where `q` is the characteristic of the field and `k` is a positive integer called embedding degree.++The embedding degree `k` plays a crucial role in pairing cryptography:+- It's the value that makes  F<sub>q<sup>k</sup></sub> be the smallest extension of F<sub>q</sub> such that E(F<sub>q<sup>k</sup></sub>) captures more points of order `r`.+- It's the minimal value that holds r | (q<sup>k</sup> - 1).+- It's the smallest positive integer such that E[r] ⊂ E(F<sub>q<sup>k</sup></sub>)++There are subtle but relevant differences in G<sub>1</sub> and G<sub>2</sub> subgroups depending on the type of pairing. Nowadays, all of the state-of-the-art implementations of pairings take place on ordinary curves and assume a type of pairing (Type 3) where G<sub>1</sub> = E[r] ∩ Ker(π - [1]) and G<sub>2</sub> = E[r] ∩ Ker(π - [q]) and there is no non-trivial map φ: G<sub>2</sub> → G<sub>1</sub>.++## Tate Pairing++The Tate pairing is a map:++tr : E(F<sub>q<sup>k</sup></sub>)[r] × E(F<sub>q<sup>k</sup></sub>) / rE(F<sub>q<sup>k</sup></sub>) → F<sup>&ast;</sup><sub>q<sup>k</sup></sub> / (F<sup>&ast;</sup><sub>q<sup>k</sup></sub>)<sup>r</sup>++defined as:++tr(P, Q) = f(Q)++where P ∈ E(F<sub>q<sup>k</sup></sub>)[r], Q is any representative in a equivalence class in E(F<sub>q<sup>k</sup></sub>) / rE(F<sub>q<sup>k</sup></sub>) and F<sup>&ast;</sup><sub>q<sup>k</sup></sub> / (F<sup>&ast;</sup><sub>q<sup>k</sup></sub>)<sup>r</sup> is the set of equivalence classes of F<sup>&ast;</sup><sub>q<sup>k</sup></sub> under the equivalence relation a ≡ b iff a / b ∈ (F<sup>&ast;</sup><sub>q<sup>k</sup></sub>)<sup>r</sup>. The equivalence relation in the output of the Tate pairing is unfortunate. In cryptography, different parties must compute the same value under the bilinearity property.++The reduced Tate pairing solves this undesirable property by exponentiating elements in F<sup>&ast;</sup><sub>q<sup>k</sup></sub> / (F<sup>&ast;</sup><sub>q<sup>k</sup></sub>)<sup>r</sup> to the power of (q<sup>k</sup> - 1) / r. It maps all elements in an equivalence class to the same value. It is defined as:++Tr(P, Q) = t<sub>r</sub>(P, Q)<sup>#F<sub>q<sup>k</sup></sub> / r</sup> = f<sub>r</sub>,P(Q)<sup>(q<sup>k</sup> - 1) / r</sup>.++When we say Tate pairing, we normally mean the reduced Tate pairing.++## Pairing optimization++Tate pairings use Miller's algorithm, which is essentially the double-and-add algorithm for elliptic curve point multiplication combined with evaluation of the functions used in the addition process. Miller's algorithm remains the fastest algorithm for computing pairings to date.++Both G<sub>1</sub> and G<sub>2</sub> are elliptic curve groups. G<sub>T</sub> is a multiplicative subgroup of a finite field. The security an elliptic curve group offers per bit is considerably greater than the security a finite field does. In order to achieve security comparable to 128-bit security (AES-128), an elliptic curve of 256 bits will suffice, while we need a finite field of 3248 bits. The aim of a cryptographic protocol is to achieve the highest security degree with the smallest signature size, which normally leads to a more efficient computation. In pairing cryptography, significant improvements can be made by keeping all three group sizes the same. It is possible to find elliptic curves over a field F<sub>q</sub> whose largest prime order subgroup `r` has the same bit-size as the characteristic of the field `q`. The ratio between the field size `q` and the large prime group order `r` is called the φ-value. It is an important value that indicates how much (ECDLP) security a curve offers for its field size. φ=1 is the optimal value. The Barreto-Naehrig (BN) family of curves all have φ=1 and k=12. They are perfectly suited to the 128-bit security level.++Most operations in pairings happen in the extension field F<sub>q<sup>k</sup></sub>. The larger k gets, the more complex F<sub>q<sup>k</sup></sub> becomes and the more computationally expensive the pairing becomes. The complexity of Miller's algorithm heavily depends on the complexity of the associated F<sub>q<sup>k</sup></sub>-arithmetic. Therefore, the aim is to minimize the cost of arithmetic in F<sub>q<sup>k</sup></sub>.++It is possible to construct an extension of a field F<sub>q<sup>k</sup></sub> by successively towering up intermediate fields F<sub>q<sup>a</sup></sub> and F<sub>q<sup>b</sup></sub> such that k = a^i b^j, where a and b are usually 2 and 3. One of the reasons tower extensions work is that quadratic and cubic extensions (F<sub>q<sup>2</sup></sub> and F<sub>q<sup>3</sup></sub>) offer methods of performing arithmetic more efficiently.++Miller's algorithm in the Tate pairing iterates as far as the prime group order `r`, which is a large number in cryptography. The ate pairing comes up as an optimization of the Tate pairing by shortening Miller's loop. It achieves a much shorter loop of length T = t - 1 on an ordinary curve, where t is the trace of the Frobenius endomorphism. The ate pairing is defined as:++at(Q,P) = f<sub>r,Q</sub>(P)<sup>(q<sup>k</sup> - 1) / r</sup>++## Implementation++We have implemented the optimal Ate pairing over the BN128 curve, i.e. we define `q` and `r` as++ * q = 36t<sup>4</sup> + 36t<sup>3</sup> + 24t<sup>2</sup> + 6t + 1+ * r = 36t<sup>4</sup> + 36t<sup>3</sup> + 18t<sup>2</sup> + 6t + 1+ * t = 4965661367192848881++The tower of finite fields we work with is defined as follows:++ * F<sub>q</sub> is the prime field with characteristic `q`+ * F<sub>q<sup>2</sup></sub> := F<sub>q</sub>[u]/u<sup>2</sup> + 1+ * F<sub>q<sup>6</sup></sub> := F<sub>q<sup></sub>2</sup>[v]/v<sup>3</sup> - (9 + u)+ * F<sub>q<sup>12</sup></sub> := F<sub>q<sup>6</sup></sub>[w]/w<sup>2</sup> - v++The groups' definitions are:++ * G<sub>1</sub> := E(F<sub>q</sub>), with equation y<sup>2</sup> = x<sup>3</sup> + 3+ * G<sub>2</sub> := E'(F<sub>q<sup>2</sup></sub>), with equation y<sup>2</sup> = x<sup>3</sup> + 3 / (9 + u)+ * G<sub>T</sub> := μ<sub>r</sub>, i.e. the `r`-th roots of unity subgroup of the multiplicative group of F<sub>q<sup>12</sup></sub>++License+-------++```+Copyright (c) 2018-2019 Adjoint Inc.++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR+OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE+OR OTHER DEALINGS IN THE SOFTWARE.+```+
+ bench/Main.hs view
@@ -0,0 +1,15 @@+{-# LANGUAGE NoImplicitPrelude #-}++-- To get the benchmarking data, run "stack bench".++module Main where++import Protolude++import Criterion.Main++import qualified BenchPairing as Pairing++main = defaultMain+      [ bgroup "Pairing" Pairing.benchmarks+      ]
+ pairing.cabal view
@@ -0,0 +1,115 @@+-- This file has been generated from package.yaml by hpack version 0.28.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 8fd85e0fcb3e2a6242030c228d45257f9ae5fe41669788791939112410c83b41++name:           pairing+version:        0.1.0+synopsis:       Optimal ate pairing over Barreto-Naehrig curves+description:    Optimal ate pairing over Barreto-Naehrig curves+category:       Cryptography+homepage:       https://github.com/adjoint-io/pairing#readme+bug-reports:    https://github.com/adjoint-io/pairing/issues+maintainer:     Adjoint Inc (info@adjoint.io)+license:        MIT+license-file:   LICENSE+build-type:     Simple+cabal-version:  >= 1.10+extra-source-files:+    ChangeLog.md+    README.md++source-repository head+  type: git+  location: https://github.com/adjoint-io/pairing++flag optimized+  description: Perform compiler optimizations+  manual: False+  default: False++flag static+  description: Emit statically-linked binary+  manual: False+  default: False++library+  exposed-modules:+      Pairing.Params+      Pairing.Fq+      Pairing.Fr+      Pairing.Fq2+      Pairing.Fq6+      Pairing.Fq12+      Pairing.Point+      Pairing.Group+      Pairing.Pairing+      Pairing.Jacobian+  other-modules:+      Pairing.CyclicGroup+      Paths_pairing+  hs-source-dirs:+      src+  default-extensions: LambdaCase RecordWildCards OverloadedStrings NoImplicitPrelude FlexibleInstances+  ghc-options: -fwarn-tabs -fwarn-incomplete-patterns -fwarn-incomplete-record-updates -fwarn-redundant-constraints -fwarn-implicit-prelude -fwarn-overflowed-literals -fwarn-orphans -fwarn-identities -fwarn-dodgy-exports -fwarn-dodgy-imports -fwarn-duplicate-exports -fwarn-overlapping-patterns -fwarn-missing-fields -fwarn-missing-methods -fwarn-missing-signatures -fwarn-noncanonical-monad-instances -fwarn-unused-pattern-binds -fwarn-unused-type-patterns -fwarn-unrecognised-pragmas -fwarn-wrong-do-bind -fno-warn-name-shadowing -fno-warn-unused-binds -fno-warn-unused-matches -fno-warn-unused-do-bind+  build-depends:+      QuickCheck+    , base >=4.7 && <5+    , bytestring+    , cryptonite+    , memory+    , protolude >=0.2+    , random+    , wl-pprint-text+  default-language: Haskell2010++test-suite test-circuit-compiler+  type: exitcode-stdio-1.0+  main-is: Driver.hs+  other-modules:+      TestCommon+      TestFields+      TestGroups+      TestPairing+      Paths_pairing+  hs-source-dirs:+      tests+  build-depends:+      QuickCheck+    , base+    , bytestring+    , cryptonite+    , memory+    , pairing+    , protolude >=0.2+    , random+    , tasty+    , tasty-discover+    , tasty-hunit+    , tasty-quickcheck+    , wl-pprint-text+  default-language: Haskell2010++benchmark pairing-benchmarks+  type: exitcode-stdio-1.0+  main-is: Main.hs+  other-modules:+      Paths_pairing+  hs-source-dirs:+      bench, tests+  build-depends:+      QuickCheck+    , base >=4.7 && <5+    , bytestring+    , criterion+    , cryptonite+    , memory+    , pairing+    , protolude >=0.2+    , random+    , tasty+    , tasty-hunit+    , tasty-quickcheck+    , wl-pprint-text+  default-language: Haskell2010
+ src/Pairing/CyclicGroup.hs view
@@ -0,0 +1,24 @@+module Pairing.CyclicGroup+  ( AsInteger(..)+  , CyclicGroup(..)+  , sumG+  ) where++import Protolude++class AsInteger a where+  asInteger :: a -> Integer++class Monoid g => CyclicGroup g where+  generator :: g+  order :: Proxy g -> Integer+  expn :: AsInteger e => g -> e -> g+  inverse :: g -> g++-- | Sum all the elements of some container according to its group+-- structure.+sumG :: (Foldable t, CyclicGroup g) => t g -> g+sumG = fold++instance AsInteger Int where+  asInteger = toInteger
+ src/Pairing/Fq.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE Strict #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE DeriveGeneric #-}++-- | Prime field with characteristic _q, over which the elliptic curve+-- is defined and the other finite field extensions. First field in+-- the tower:+--+--   * Fq+--   * Fq2 := Fq[u]/u^2 + 1+--   * Fq6 := Fq2[v]/v^3 - (9 + u)+--   * Fq12 := Fq6[w]/w^2 - v+--+module Pairing.Fq (+  Fq(..),+  new,+  fqInv,+  fqZero,+  fqOne,+  fqNqr,+  euclidean,+  random+) where++import Protolude+import Crypto.Random (MonadRandom)+import Crypto.Number.Generate (generateMax)+import Pairing.Params as Params+import Pairing.CyclicGroup++-------------------------------------------------------------------------------+-- Types+-------------------------------------------------------------------------------++-- | Prime field with characteristic @_q@+newtype Fq = Fq Integer -- ^ Use @new@ instead of this+                        -- constructor+  deriving (Show, Eq, Bits, Generic, NFData, Ord)++instance AsInteger Fq where+  asInteger (Fq n) = n+++instance Num Fq where+  (+)           = fqAdd+  (*)           = fqMul+  abs           = fqAbs+  signum        = fqSig+  negate        = fqNeg+  fromInteger   = new++instance Fractional Fq where+  (/) = fqDiv+  fromRational (a :% b) = Fq a / Fq b++-- | Turn an integer into an @Fq@ number, should be used instead of+-- the @Fq@ constructor.+new :: Integer -> Fq+new a = Fq (a `mod` _q)++{-# INLINE norm #-}+norm :: Fq -> Fq+norm (Fq a) = Fq (a `mod` _q)++{-# INLINE fqAdd #-}+fqAdd :: Fq -> Fq -> Fq+fqAdd (Fq a) (Fq b) = norm (Fq (a+b))++{-# INLINE fqAbs #-}+fqAbs :: Fq -> Fq+fqAbs (Fq a) = Fq a++{-# INLINE fqSig #-}+fqSig :: Fq -> Fq+fqSig (Fq a) = Fq (signum a  `mod` _q)++{-# INLINE fqMul #-}+fqMul :: Fq -> Fq -> Fq+fqMul (Fq a) (Fq b) = norm (Fq (a*b))++{-# INLINE fqNeg #-}+fqNeg :: Fq -> Fq+fqNeg (Fq a) = Fq ((-a) `mod` _q)++{-# INLINE fqDiv #-}+fqDiv :: Fq -> Fq -> Fq+fqDiv a b = fqMul a (inv b)++{-# INLINE fqNqr #-}+-- | Quadratic non-residue+fqNqr :: Fq+fqNqr = Fq Params._nqr++{-# INLINE fqInv #-}+-- | Multiplicative inverse+fqInv :: Fq -> Fq+fqInv x = 1 / x++{-# INLINE fqZero #-}+-- | Additive identity+fqZero :: Fq+fqZero = Fq 0++{-# INLINE fqOne #-}+-- | Multiplicative identity+fqOne :: Fq+fqOne = Fq 1++inv :: Fq -> Fq+inv (Fq a) = Fq $ euclidean a _q `mod` _q++-- | Euclidean algorithm to compute inverse in an integral domain @a@+euclidean :: (Integral a) => a -> a -> a+euclidean a b = fst (inv' a b)++{-# INLINEABLE inv' #-}+{-# SPECIALISE inv' :: Integer -> Integer -> (Integer, Integer) #-}+inv' :: (Integral a) => a -> a -> (a, a)+inv' a b =+  case b of+   1 -> (0, 1)+   _ -> let (e, f) = inv' b d+        in (f, e - c*f)+  where c = a `div` b+        d = a `mod` b++random :: MonadRandom m => m Fq+random = do+  seed <- generateMax _q+  pure (Fq seed)
+ src/Pairing/Fq12.hs view
@@ -0,0 +1,140 @@+{-# LANGUAGE Strict #-}++-- | Final quadratic extension of the tower:+--+--   * Fq+--   * Fq2 := Fq[u]/u^2 + 1+--   * Fq6 := Fq2[v]/v^3 - (9 + u)+--   * Fq12 := Fq6[w]/w^2 - v+--+-- Implementation follows "Multiplication and Squaring on+-- Pairing-Friendly Fields" by Devigili, hEigeartaigh, Scott and+-- Dahab.+module Pairing.Fq12 (+  Fq12(..),+  new,+  deconstruct,+  fq12inv,+  fq12one,+  fq12zero,+  fq12conj,+  fq12frobenius,+  random+) where++import Protolude+import Crypto.Random (MonadRandom)++import Pairing.Fq (Fq)+import Pairing.Fq6 (Fq6(..))+import qualified Pairing.Fq2 as Fq2+import qualified Pairing.Fq6 as Fq6+import Pairing.Params++-- | Field extension defined as Fq6[w]/w^2 - v+data Fq12 = Fq12 { fq12x :: Fq6, fq12y :: Fq6 } -- ^ Use @new@ instead+                                                -- of this constructor+  deriving (Eq, Show)++instance Num Fq12 where+  (+)         = fq12add+  (*)         = fq12mul+  negate      = fq12neg+  fromInteger = fq12int+  abs         = panic "abs not defined for fq12"+  signum      = panic "signum not defined for fq12"++instance Fractional Fq12 where+  (/) = fq12div+  fromRational (a :% b) = fq12int a / fq12int b++-- | Create a new value in @Fq12@ by providing a list of twelve+-- coefficients in @Fq@, should be used instead of the @Fq12@+-- constructor.+new :: [Fq] -> Fq12+new [a,b,c,d,e,f,g,h,i,j,k,l] = Fq12+  (Fq6.new (Fq2.new a b) (Fq2.new c d) (Fq2.new e f))+  (Fq6.new (Fq2.new g h) (Fq2.new i j) (Fq2.new k l))+new _ = panic "Invalid arguments to fq12"++-- | Deconstruct a value in @Fq12@ into a list of twelve coefficients in @Fq@.+deconstruct :: Fq12 -> [Fq]+deconstruct (Fq12+  (Fq6.Fq6 (Fq2.Fq2 a b) (Fq2.Fq2 c d) (Fq2.Fq2 e f))+  (Fq6.Fq6 (Fq2.Fq2 g h) (Fq2.Fq2 i j) (Fq2.Fq2 k l)))+  = [a,b,c,d,e,f,g,h,i,j,k,l]++fq12int :: Integer -> Fq12+fq12int n = new (fromIntegral n : replicate 11 0)++-- | Multiplicative identity+fq12one :: Fq12+fq12one = fq12int 1++-- | Additive identity+fq12zero :: Fq12+fq12zero = fq12int 0++fq12add :: Fq12 -> Fq12 -> Fq12+fq12add (Fq12 x y) (Fq12 a b) = Fq12 (x+a) (y+b)++fq12neg :: Fq12 -> Fq12+fq12neg (Fq12 x y) = Fq12 (negate x) (negate y)++fq12div :: Fq12 -> Fq12 -> Fq12+fq12div a b = a * fq12inv b++fq12mul :: Fq12 -> Fq12 -> Fq12+fq12mul (Fq12 x y) (Fq12 a b) = Fq12 (Fq6.mulXi bb + aa) ((x+y) * (a+b) - aa - bb)+  where+    aa = x*a+    bb = y*b++-- | Multiplicative inverse+{-# INLINEABLE fq12inv #-}+fq12inv :: Fq12 -> Fq12+fq12inv (Fq12 a b) = Fq12 (a*t) (-(b*t))+  where+    t = Fq6.fq6inv (a^2 - Fq6.mulXi (b^2))++-- | Conjugation+fq12conj :: Fq12 -> Fq12+fq12conj (Fq12 x y) = Fq12 x (negate y)++-- | Iterated Frobenius automorphism+fq12frobenius :: Int -> Fq12 -> Fq12+fq12frobenius i a+  | i == 0 = a+  | i == 1 = fastFrobenius1 a+  | i > 1 = let prev = fq12frobenius (i - 1) a+            in fastFrobenius1 prev+  | otherwise = panic "fq12frobenius not defined for negative values of i"++fastFrobenius1 :: Fq12 -> Fq12+fastFrobenius1 (Fq12 (Fq6.Fq6 x0 x1 x2) (Fq6.Fq6 y0 y1 y2)) =+  let+    t1 = Fq2.fq2conj x0+    t2 = Fq2.fq2conj y0+    t3 = Fq2.fq2conj x1+    t4 = Fq2.fq2conj y1+    t5 = Fq2.fq2conj x2+    t6 = Fq2.fq2conj y2+    gamma1 :: Integer -> Fq2.Fq2+    gamma1 i = Fq2.xi ^ ((i * (_q - 1)) `div` 6)+    t11 = t1+    t21 = t2 * gamma1 1+    t31 = t3 * gamma1 2+    t41 = t4 * gamma1 3+    t51 = t5 * gamma1 4+    t61 = t6 * gamma1 5+    c0 = Fq6 t11 t31 t51+    c1 = Fq6 t21 t41 t61+  in Fq12 c0 c1++++random :: MonadRandom m => m Fq12+random = do+  x <- Fq6.random+  y <- Fq6.random+  pure (Fq12 x y)
+ src/Pairing/Fq2.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE Strict #-}+{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-}++-- | First quadratic extension of the tower:+--+--   * Fq+--   * Fq2 := Fq[u]/u^2 + 1+--   * Fq6 := Fq2[v]/v^3 - (9 + u)+--   * Fq12 := Fq6[w]/w^2 - v+--+-- Implementation following "Multiplication and Squaring on+-- Pairing-Friendly Fields" by Devigili, hEigeartaigh, Scott and+-- Dahab.+module Pairing.Fq2 (+  Fq2(..),+  Pairing.Fq2.new,+  fq2scalarMul,+  fq2inv,+  fq2one,+  fq2zero,+  fq2conj,+  fq2sqr,+  mulXi,+  divXi,+  xi,+  Pairing.Fq2.random+) where++import Protolude+import Crypto.Random (MonadRandom)++import Pairing.Fq as Fq+import qualified Pairing.Params as Params++-- | Quadratic extension of @Fq@ defined as @Fq[u]/x^2 + 1@+data Fq2 = Fq2 { fq2x :: Fq, fq2y :: Fq } -- ^ Use @new@ instead of+                                          -- this contructor+  deriving (Eq, Show, Generic, NFData)++-- | @new x y@ creates a value representing @x + y * u @+new :: Fq -> Fq -> Fq2+new = Fq2++instance Num Fq2 where+  (+)         = fq2add+  (*)         = fq2mul+  negate      = fq2neg+  fromInteger = fq2int+  abs         = panic "abs not defined for fq2"+  signum      = panic "signum not defined for fq2"++instance Fractional Fq2 where+  (/) = fq2div+  fromRational (a :% b) = fq2int a / fq2int b++-- | Cubic non-residue in @Fq2@+xi :: Fq2+xi = Fq2 xiA xiB+  where+    xiA, xiB :: Fq+    xiA = Fq.new Params._xiA+    xiB = Fq.new Params._xiB++-- | Multiplicative identity+fq2one :: Fq2+fq2one = fq2int 1++-- | Additive identity+fq2zero :: Fq2+fq2zero = fq2int 0++fq2int :: Integer -> Fq2+fq2int n = Fq2 (fromInteger n) fqZero++fq2neg :: Fq2 -> Fq2+fq2neg (Fq2 x y) = Fq2 (-x) (-y)++fq2add :: Fq2 -> Fq2 -> Fq2+fq2add (Fq2 x y) (Fq2 a b) = Fq2 (x+a) (y+b)++fq2div :: Fq2 -> Fq2 -> Fq2+fq2div a b = fq2mul a (fq2inv b)++fq2mul :: Fq2 -> Fq2 -> Fq2+fq2mul (Fq2 a0 a1) (Fq2 b0 b1) = Fq2 c0 c1+  where+    aa = a0 * b0+    bb = a1 * b1+    c0 = bb * fqNqr + aa+    c1 = (a0 + a1) * (b0 + b1) - aa - bb++-- | Multiplication by a scalar in @Fq@+fq2scalarMul :: Fq -> Fq2 -> Fq2+fq2scalarMul a (Fq2 x y) = Fq2 (a*x) (a*y)++-- | Multiply by @xi@+mulXi :: Fq2 -> Fq2+mulXi = (* xi)++-- | Divide by @xi@+divXi :: Fq2 -> Fq2+divXi = (/ xi)++-- | Squaring operation+fq2sqr :: Fq2 -> Fq2+fq2sqr (Fq2 a0 a1) = Fq2 c0 c1+  where+    aa = a0 * a0+    bb = a1 * a1+    c0 = bb * fqNqr + aa+    c1 = (a0 + a1) * (a0 + a1) - aa - bb++-- | Multiplicative inverse+fq2inv :: Fq2 -> Fq2+fq2inv (Fq2 a0 a1) = Fq2 c0 c1+  where+    t = fqInv ((a0 ^ 2) - ((a1 ^ 2) * fqNqr))+    c0 = a0 * t+    c1 = -(a1 * t)++-- | Conjugation+fq2conj :: Fq2 -> Fq2+fq2conj (Fq2 x y) = Fq2 x (negate y)+++random :: MonadRandom m => m Fq2+random = do+  x <- Fq.random+  y <- Fq.random+  pure (Fq2 x y)
+ src/Pairing/Fq6.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE Strict #-}++-- | Cubic extension of the tower:+--+--   * Fq+--   * Fq2 := Fq[u]/u^2 + 1+--   * Fq6 := Fq2[v]/v^3 - (9 + u)+--   * Fq12 := Fq6[w]/w^2 - v+--+-- Implementation follows "Multiplication and Squaring on+-- Pairing-Friendly Fields" by Devigili, hEigeartaigh, Scott and+-- Dahab.+module Pairing.Fq6 (+  Fq6(..),+  new,+  fq6inv,+  fq6one,+  fq6zero,+  fq6sqr,+  mulXi,+  random+) where++import Protolude+import Crypto.Random (MonadRandom)++import Pairing.Fq2 (Fq2)+import qualified Pairing.Fq2 as Fq2++-- | Field extension defined as Fq2[v]/v^3 - (9 + u)+data Fq6+  = Fq6+    { fq6x :: Fq2+    , fq6y :: Fq2+    , fq6z :: Fq2+    }+  deriving (Eq, Show)++instance Num Fq6 where+  (+)         = fq6add+  (*)         = fq6mul+  negate      = fq6neg+  fromInteger = fq6int+  abs         = panic "abs not defined for fq6"+  signum      = panic "signum not defined for fq6"++instance Fractional Fq6 where+  (/) = fq6div+  fromRational (a :% b) = fq6int a / fq6int b++-- | Create a new value in @Fq6@, should be used instead of the @Fq6@+-- constructor.+new :: Fq2 -> Fq2 -> Fq2 -> Fq6+new = Fq6++-- | Additive identity+fq6zero :: Fq6+fq6zero = Fq6 0 0 0++fq6int :: Integer -> Fq6+fq6int n = Fq6 (fromInteger n) 0 0++-- | Multiplicative identity+fq6one :: Fq6+fq6one = Fq6 1 0 0++fq6add :: Fq6 -> Fq6 -> Fq6+fq6add (Fq6 x y z) (Fq6 a b c) = Fq6 (x+a) (y+b) (z+c)++fq6neg :: Fq6 -> Fq6+fq6neg (Fq6 x y z) = Fq6 (-x) (-y) (-z)++-- | Squaring operation+fq6sqr :: Fq6 -> Fq6+fq6sqr x = x^2++fq6div :: Fq6 -> Fq6 -> Fq6+fq6div a b = a * fq6inv b++fq6mul :: Fq6 -> Fq6 -> Fq6+fq6mul (Fq6 a0 a1 a2) (Fq6 b0 b1 b2) = Fq6 c0 c1 c2+  where+    t0 = a0 * b0+    t1 = a1 * b1+    t2 = a2 * b2+    c0 = Fq2.mulXi ((a1+a2) * (b1+b2) - t1 - t2) + t0+    c1 = ((a0+a1) * (b0+b1)) - t0 - t1 + Fq2.mulXi t2+    c2 = ((a0+a2) * (b0+b2)) - t0 + t1 - t2++-- | Multiply by @xi@ (cubic nonresidue in @Fq2@) and reorder+-- coefficients+{-# INLINABLE mulXi #-}+mulXi :: Fq6 -> Fq6+mulXi (Fq6 x y z) = Fq6 (z*Fq2.xi) x y++-- | Multiplicative inverse+fq6inv :: Fq6 -> Fq6+fq6inv (Fq6 a b c) = Fq6 (t*c0) (t*c1) (t*c2)+  where+    c0 = a^2 - b * c * Fq2.xi+    c1 = c^2 * Fq2.xi - a * b+    c2 = b^2 - a*c+    t  = Fq2.fq2inv ((c * c1 + b * c2) * Fq2.xi + a*c0)+++random :: MonadRandom m => m Fq6+random = do+  a <- Fq2.random+  b <- Fq2.random+  c <- Fq2.random+  pure (Fq6 a b c)
+ src/Pairing/Fr.hs view
@@ -0,0 +1,146 @@+{-# LANGUAGE Strict #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-- | Prime field from which exponents should be chosen+module Pairing.Fr (+  Fr(..),+  new,+  frInv,+  random,+  isRootOfUnity,+  isPrimitiveRootOfUnity,+  primitiveRootOfUnity,+  precompRootOfUnity+) where++import Protolude++import Crypto.Random (MonadRandom)+import Crypto.Number.Generate (generateMax)+import Text.PrettyPrint.Leijen.Text++import Pairing.Params+import Pairing.CyclicGroup+import Pairing.Fq (euclidean)++instance AsInteger Fr where+  asInteger (Fr n) = n++instance Num Fr where+  (+)           = frAdd+  (*)           = frMul+  abs           = frAbs+  signum        = frSig+  negate        = frNeg+  fromInteger n = Fr (n `mod` _r)++instance Fractional Fr where+  (/) = frDiv+  fromRational (a :% b) = Fr a / Fr b++instance Pretty Fr where+  pretty (Fr fr) = pretty fr++-- | Prime field with characteristic @_r@+newtype Fr = Fr Integer -- ^ Use @new@ instead of this constructor+  deriving (Show, Eq, Ord, Bits, NFData)++-- | Turn an integer into an @Fr@ number, should be used instead of+-- the @Fr@ constructor.+new :: Integer -> Fr+new a = Fr (a `mod` _r)++{-# INLINE norm #-}+norm :: Fr -> Fr+norm (Fr a) = Fr (a `mod` _r)++{-# INLINE frAdd #-}+frAdd :: Fr -> Fr -> Fr+frAdd (Fr a) (Fr b) = norm (Fr (a+b))++{-# INLINE frMul #-}+frMul :: Fr -> Fr -> Fr+frMul (Fr a) (Fr b) = norm (Fr (a*b))++{-# INLINE frAbs #-}+frAbs :: Fr -> Fr+frAbs (Fr a) = Fr a++{-# INLINE frSig #-}+frSig :: Fr -> Fr+frSig (Fr a) = Fr (signum a  `mod` _r)++{-# INLINE frNeg #-}+frNeg :: Fr -> Fr+frNeg (Fr a) = Fr ((-a) `mod` _r)++{-# INLINE frDiv #-}+frDiv :: Fr -> Fr -> Fr+frDiv a b = frMul a (inv b)++inv :: Fr -> Fr+inv (Fr a) = Fr $ euclidean a _r `mod` _r++frInv :: Fr -> Fr+frInv = inv++random :: MonadRandom m => m Fr+random = do+  seed <- generateMax _r+  pure (Fr seed)++-- Roots of unity stuff++isRootOfUnity :: Integer -> Fr -> Bool+isRootOfUnity n x+  | n > 0 = x^n == 1+  | otherwise = panic "isRootOfUnity: negative powers not supported"++isPrimitiveRootOfUnity :: Integer -> Fr -> Bool+isPrimitiveRootOfUnity n x+  | n > 0 = isRootOfUnity n x && all (\m -> not $ isRootOfUnity m x) [1..n - 1]+  | otherwise = panic "isPrimitiveRootOfUnity: negative powers not supported"++-- | Compute primitive roots of unity for 2^0, 2^1, ..., 2^28. (2^28+-- is the largest power of two that divides _r - 1, therefore there+-- are no primitive roots of unity for higher powers of 2 in Fr.)+primitiveRootOfUnity+  :: Int -- ^ exponent of 2 for which we want to get the primitive+         -- root of unity+  -> Fr+primitiveRootOfUnity k+  | 0 <= k && k <= 28+    = 5 ^ ((_r - 1) `div` (2^k))+  | otherwise = panic "primitiveRootOfUnity: no primitive root for given power of 2"++precompRootOfUnity :: Int -> Fr+precompRootOfUnity 0 = 1+precompRootOfUnity 1 = 21888242871839275222246405745257275088548364400416034343698204186575808495616+precompRootOfUnity 2 = 21888242871839275217838484774961031246007050428528088939761107053157389710902+precompRootOfUnity 3 = 19540430494807482326159819597004422086093766032135589407132600596362845576832+precompRootOfUnity 4 = 14940766826517323942636479241147756311199852622225275649687664389641784935947+precompRootOfUnity 5 = 4419234939496763621076330863786513495701855246241724391626358375488475697872+precompRootOfUnity 6 = 9088801421649573101014283686030284801466796108869023335878462724291607593530+precompRootOfUnity 7 = 10359452186428527605436343203440067497552205259388878191021578220384701716497+precompRootOfUnity 8 = 3478517300119284901893091970156912948790432420133812234316178878452092729974+precompRootOfUnity 9 = 6837567842312086091520287814181175430087169027974246751610506942214842701774+precompRootOfUnity 10 = 3161067157621608152362653341354432744960400845131437947728257924963983317266+precompRootOfUnity 11 = 1120550406532664055539694724667294622065367841900378087843176726913374367458+precompRootOfUnity 12 = 4158865282786404163413953114870269622875596290766033564087307867933865333818+precompRootOfUnity 13 = 197302210312744933010843010704445784068657690384188106020011018676818793232+precompRootOfUnity 14 = 20619701001583904760601357484951574588621083236087856586626117568842480512645+precompRootOfUnity 15 = 20402931748843538985151001264530049874871572933694634836567070693966133783803+precompRootOfUnity 16 = 421743594562400382753388642386256516545992082196004333756405989743524594615+precompRootOfUnity 17 = 12650941915662020058015862023665998998969191525479888727406889100124684769509+precompRootOfUnity 18 = 11699596668367776675346610687704220591435078791727316319397053191800576917728+precompRootOfUnity 19 = 15549849457946371566896172786938980432421851627449396898353380550861104573629+precompRootOfUnity 20 = 17220337697351015657950521176323262483320249231368149235373741788599650842711+precompRootOfUnity 21 = 13536764371732269273912573961853310557438878140379554347802702086337840854307+precompRootOfUnity 22 = 12143866164239048021030917283424216263377309185099704096317235600302831912062+precompRootOfUnity 23 = 934650972362265999028062457054462628285482693704334323590406443310927365533+precompRootOfUnity 24 = 5709868443893258075976348696661355716898495876243883251619397131511003808859+precompRootOfUnity 25 = 19200870435978225707111062059747084165650991997241425080699860725083300967194+precompRootOfUnity 26 = 7419588552507395652481651088034484897579724952953562618697845598160172257810+precompRootOfUnity 27 = 2082940218526944230311718225077035922214683169814847712455127909555749686340+precompRootOfUnity 28 = 19103219067921713944291392827692070036145651957329286315305642004821462161904+precompRootOfUnity _ = panic "precompRootOfUnity: exponent too big for Fr / negative"
+ src/Pairing/Group.hs view
@@ -0,0 +1,134 @@+{-# LANGUAGE FlexibleInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | Definitions of the groups the pairing is defined on+module Pairing.Group (+  CyclicGroup(..),+  G1,+  G2,+  GT,+  isOnCurveG1,+  isOnCurveG2,+  isInGT,+  g1,+  g2,+  b1,+  b2,+) where++import Protolude+import Data.Semigroup++import Pairing.Fq as Fq+import Pairing.Fq2 as Fq2+import Pairing.Fq12 as Fq12+import Pairing.Point+import Pairing.Params+import Pairing.CyclicGroup+import Test.QuickCheck++-- | G1 is E(Fq) defined by y^2 = x^3 + b+type G1 = Point Fq++-- | G2 is E'(Fq2) defined by y^2 = x^3 + b / xi+type G2 = Point Fq2++-- | GT is subgroup of _r-th roots of unity of the multiplicative+-- group of Fq12+type GT = Fq12++instance Semigroup G1 where+  (<>) = gAdd++instance Semigroup G2 where+  (<>) = gAdd++instance Semigroup GT where+  (<>) = (*)++instance Monoid G1 where+  mappend = gAdd+  mempty = Infinity++instance CyclicGroup G1 where+  generator = g1+  order _ = _r+  expn a b = gMul a (asInteger b)+  inverse = gNeg++instance Monoid G2 where+  mappend = gAdd+  mempty = Infinity++instance CyclicGroup G2 where+  generator = g2+  order _ = _r+  expn a b = gMul a (asInteger b)+  inverse = gNeg++instance Monoid GT where+  mappend = (*)+  mempty = 1++instance CyclicGroup GT where+  generator = notImplemented -- this should be the _r-th primitive root of unity+  order = notImplemented -- should be a factor of _r+  expn a b = a ^ asInteger b+  inverse = recip++-- | Generator for G1+g1 :: G1+g1 = Point 1 2++-- | Generator for G2+g2 :: G2+g2 = Point x y+  where+    x = Fq2+      10857046999023057135944570762232829481370756359578518086990519993285655852781+      11559732032986387107991004021392285783925812861821192530917403151452391805634++    y = Fq2+      8495653923123431417604973247489272438418190587263600148770280649306958101930+      4082367875863433681332203403145435568316851327593401208105741076214120093531++-- | Test whether a value in G1 satisfies the corresponding curve+-- equation+isOnCurveG1 :: G1 -> Bool+isOnCurveG1 Infinity+  = True+isOnCurveG1 (Point x y)+  = (y ^ 2 == x ^ 3 + Fq _b)++-- | Test whether a value in G2 satisfies the corresponding curve+-- equation+isOnCurveG2 :: G2 -> Bool+isOnCurveG2 Infinity+  = True+isOnCurveG2 (Point x y)+  = (y ^ 2 == x ^ 3 + (Fq2 (b * inv_xi_a) (b * inv_xi_b)))+  where+    (Fq2 inv_xi_a inv_xi_b) = Fq2.fq2inv Fq2.xi+    b = Fq _b++-- | Test whether a value is an _r-th root of unity+isInGT :: GT -> Bool+isInGT f =  f ^ _r == Fq12.fq12one++-- | Parameter for curve on Fq+b1 :: Fq+b1 = Fq.new _b++-- | Parameter for twisted curve over Fq2+b2 :: Fq2+b2 = Fq2 b1 0 / Fq2.xi++-------------------------------------------------------------------------------+-- Generators+-------------------------------------------------------------------------------++instance Arbitrary (Point Fq) where -- G1+  arbitrary = gMul g1 . abs <$> (arbitrary :: Gen Integer)++instance Arbitrary (Point Fq2) where -- G2+  arbitrary = gMul g2 . abs <$> (arbitrary :: Gen Integer)
+ src/Pairing/Jacobian.hs view
@@ -0,0 +1,32 @@+-- | Jacobian representation of points on an elliptic curve.+--+-- In Jacobian coordinates the triple @(x, y, z)@ represents the affine point+-- @(X / Z^2, Y / Z^3)@.  Curve operations are more optimal in Jacobian+-- coordinates when the time complexity for underlying field inversions is+-- significantly higher than field multiplications.+module Pairing.Jacobian (+  JPoint,+  toJacobian,+  fromJacobian+) where++import Protolude++import Pairing.Point++-- | Jacobian coordinates for points on an elliptic curve over a field+-- @a@.+type JPoint a = (a,a,a)++-- | Convert affine coordinates to Jacobian coordinates+toJacobian :: Fractional a => Point a -> JPoint a+toJacobian Infinity = (1, 1, 0)+toJacobian (Point x y) = (x,y,1)++-- | Convert Jacobian coordinates to affine coordinates+fromJacobian :: (Eq a, Fractional a) => JPoint a -> Point a+fromJacobian (x, y, z)+  | z == 0 = Infinity+  | otherwise = Point (x * zinv^2) (y * zinv^3)+  where+    zinv = recip z
+ src/Pairing/Pairing.hs view
@@ -0,0 +1,252 @@+-- | Implementation of the optimal Ate pairing on the curve BN128++module Pairing.Pairing+  ( reducedPairing+  , atePairing+  , finalExponentiation+  , finalExponentiationNaive+  , frobeniusNaive+  , ateLoopCountBinary+  ) where++import Protolude++import Data.List ((!!))+import Pairing.Point+import Pairing.Group+import Pairing.Jacobian+import Pairing.Fq (Fq)+import qualified Pairing.Fq as Fq+import Pairing.Fq2 (Fq2)+import qualified Pairing.Fq2 as Fq2+import Pairing.Fq6 as Fq6+import Pairing.Fq12 (Fq12)+import qualified Pairing.Fq12 as Fq12+import Pairing.Params++-- G2, but using Jacobian coordinates+type JG2 = JPoint Fq2++-- ell0, ellVW, ellVV+data EllCoeffs+  = EllCoeffs Fq2 Fq2 Fq2+  deriving (Show, Eq)++-- | Optimal Ate pairing (including final exponentiation step)+reducedPairing :: G1 -> G2 -> GT+reducedPairing p@(Point _ _) q@(Point _ _)+  = finalExponentiation $ atePairing p q+reducedPairing _ _+  = Fq12.fq12one++-------------------------------------------------------------------------------+-- Miller loop+-------------------------------------------------------------------------------++-- | Optimal Ate pairing without the final exponentiation step+atePairing :: G1 -> G2 -> Fq12+atePairing p@(Point _ _) q@(Point _ _)+  = ateMillerLoop p (atePrecomputeG2 q)+atePairing _ _+  = Fq12.fq12one++-- | Binary expansion (missing the most-significant bit) representing+-- the number 6 * _t + 2.+--+-- > 29793968203157093288+-- > = 0b11001110101111001011100000011100110111110011101100011101110101000+ateLoopCountBinary :: [Bool]+ateLoopCountBinary+  = [ t, f, f, t, t, t, f, t, f, t, t, t, t, f, f, t+    , f, t, t, t, f, f, f, f, f, f, t, t, t, f, f, t+    , t, f, t, t, t, t, t, f, f, t, t, t, f, t, t, f+    , f, f, t, t, t, f, t, t, t, f, t, f, t, f, f, f+    ]+    where+      t = True+      f = False++-- | Miller loop with precomputed values for G2+ateMillerLoop :: G1 -> [EllCoeffs] -> GT+ateMillerLoop p coeffs  = let+  (postLoopIx, postLoopF) = foldl' (ateLoopBody p coeffs) (0, Fq12.fq12one) ateLoopCountBinary+  almostF = mulBy024 postLoopF (prepareCoeffs coeffs p postLoopIx)+  finalF = mulBy024 almostF (prepareCoeffs coeffs p (postLoopIx + 1))+  in finalF++ateLoopBody :: G1 -> [EllCoeffs] -> (Int, Fq12) -> Bool -> (Int, Fq12)+ateLoopBody p coeffs (oldIx, oldF) currentBit+  = let+  fFirst = mulBy024 (oldF^2) (prepareCoeffs coeffs p oldIx)+  (nextIx, nextF) = if currentBit+          then (oldIx + 2, mulBy024 fFirst (prepareCoeffs coeffs p (oldIx + 1)))+          else (oldIx + 1, fFirst)+  in (nextIx, nextF)++prepareCoeffs :: [EllCoeffs] -> G1 -> Int -> EllCoeffs+prepareCoeffs _ Infinity _ = panic "prepareCoeffs: received trivial point"+prepareCoeffs coeffs (Point px py) ix =+  let (EllCoeffs ell0 ellVW ellVV) = coeffs !! ix+  in EllCoeffs ell0 (Fq2.fq2scalarMul py ellVW) (Fq2.fq2scalarMul px ellVV)++{-# INLINEABLE mulBy024 #-}+mulBy024 :: Fq12 -> EllCoeffs -> Fq12+mulBy024 this (EllCoeffs ell0 ellVW ellVV)+  = let a = Fq12.Fq12+            (Fq6.Fq6 ell0 Fq2.fq2zero ellVV)+            (Fq6.Fq6 Fq2.fq2zero ellVW Fq2.fq2zero)+    in this * a++-------------------------------------------------------------------------------+-- Precomputation on G2+-------------------------------------------------------------------------------++-- | Iterated frobenius morphisms on fields of characteristic _q,+-- implemented naively+{-# SPECIALISE frobeniusNaive :: Int -> Fq2 -> Fq2 #-}+frobeniusNaive :: Num a => Int -> a -> a+frobeniusNaive i a+  | i == 0 = a+  | i == 1 = a ^ _q+  | i > 1 = let prev = frobeniusNaive (i - 1) a+            in prev ^ _q+  | otherwise = panic "frobeniusNaive: received negative input"++{-# INLINEABLE mulByQ  #-}+mulByQ :: JG2 -> JG2+mulByQ (x, y, z)+  = ( twistMulX * frobeniusNaive 1 x+    , twistMulY * frobeniusNaive 1 y+    , frobeniusNaive 1 z+    )++-- xi ^ ((_q - 1) `div` 3)+twistMulX :: Fq2+twistMulX = Fq2.xi ^ ((_q - 1) `div` 3) -- Fq2+--  21575463638280843010398324269430826099269044274347216827212613867836435027261+--  10307601595873709700152284273816112264069230130616436755625194854815875713954++-- xi ^ ((_q - 1) `div` 2)+twistMulY :: Fq2+twistMulY = Fq2.xi ^ ((_q - 1) `div` 2) -- Fq2+--  2821565182194536844548159561693502659359617185244120367078079554186484126554+--  3505843767911556378687030309984248845540243509899259641013678093033130930403++mirrorY :: JG2 -> JG2+mirrorY (x,y,z) = (x,-y,z)++atePrecomputeG2 :: G2 -> [EllCoeffs]+atePrecomputeG2 Infinity = []+atePrecomputeG2 origPt@(Point _ _)+  = let+  bigQ = toJacobian origPt+  (postLoopR, postLoopCoeffs)+    = runLoop bigQ+  bigQ1 = mulByQ bigQ+  bigQ2 = mirrorY $ mulByQ bigQ1++  (newR, coeffs1) = mixedAdditionStepForFlippedMillerLoop bigQ1 postLoopR+  (_, coeffs2) = mixedAdditionStepForFlippedMillerLoop bigQ2 newR+  finalCoeffs = postLoopCoeffs ++ [coeffs1, coeffs2]+  in finalCoeffs+    where+      -- Assumes q to have z coordinate to be 1+      runLoop q = foldl' (loopBody q) (q, []) ateLoopCountBinary++      loopBody :: JG2 -> (JG2, [EllCoeffs]) -> Bool -> (JG2, [EllCoeffs])+      loopBody q (oldR, oldCoeffs) currentBit+        = let+        (currentR, currentCoeff) = doublingStepForFlippedMillerLoop oldR+        currentCoeffs = oldCoeffs ++ [currentCoeff]+        (nextR, nextCoeffs) = if currentBit+                              then+                                let (resultR, resultCoeff)+                                      = mixedAdditionStepForFlippedMillerLoop q currentR+                                in (resultR, currentCoeffs ++ [resultCoeff])+                              else (currentR, currentCoeffs)+        in (nextR, nextCoeffs)++twoInv :: Fq+twoInv = Fq.fqInv $ Fq.new 2++twistCoeffB :: Fq2+twistCoeffB = Fq2.fq2scalarMul (Fq.new _b) (Fq2.fq2inv Fq2.xi)++doublingStepForFlippedMillerLoop :: JG2 -> (JG2, EllCoeffs)+doublingStepForFlippedMillerLoop (oldX, oldY, oldZ)+  = let+  a, b, c, d, e, f, g, h, i, j, eSquared :: Fq2.Fq2++  a = Fq2.fq2scalarMul twoInv (oldX * oldY)+  b = oldY * oldY+  c = oldZ * oldZ+  d = c + c + c+  e = twistCoeffB * d+  f = e + e + e+  g = Fq2.fq2scalarMul twoInv (b + f)+  h = (oldY + oldZ) * (oldY + oldZ) - (b + c)+  i = e - b+  j = oldX * oldX+  eSquared = e * e++  newX = a * (b - f)+  newY = g * g - (eSquared + eSquared + eSquared)+  newZ = b * h++  ell0 = Fq2.xi * i+  ellVV = j + j + j+  ellVW = - h++  in ( (newX, newY, newZ)+     , EllCoeffs ell0 ellVW ellVV+     )++mixedAdditionStepForFlippedMillerLoop :: JG2 -> JG2 -> (JG2, EllCoeffs)+mixedAdditionStepForFlippedMillerLoop _base@(x2, y2, _z2) _current@(x1, y1, z1)+  = let+  d, e, f, g, h, i, j :: Fq2.Fq2+  d = x1 - (x2 * z1)+  e = y1 - (y2 * z1)+  f = d * d+  g = e * e+  h = d * f+  i = x1 * f+  j = h + z1 * g - (i + i)++  newX = d * j+  newY = e * (i - j) - (h * y1)+  newZ = z1 * h++  ell0 = Fq2.xi * (e * x2 - d * y2)+  ellVV = - e+  ellVW = d++  in ( (newX, newY, newZ)+     , EllCoeffs ell0 ellVW ellVV+     )++-------------------------------------------------------------------------------+-- Final exponentiation+-------------------------------------------------------------------------------++-- | Naive implementation of the final exponentiation step+finalExponentiationNaive :: Fq12 -> GT+finalExponentiationNaive f = f ^ expVal+  where+    expVal :: Integer+    expVal = (_q ^ _k - 1) `div` _r++-- | A faster way of performing the final exponentiation step+finalExponentiation :: Fq12 -> GT+finalExponentiation f = finalExponentiationFirstChunk f ^ expVal+  where+    expVal = (_q ^ 4 - _q ^ 2 + 1) `div` _r++finalExponentiationFirstChunk :: Fq12 -> GT+finalExponentiationFirstChunk f+  | f == Fq12.fq12zero = Fq12.fq12zero+  | otherwise = let+  f1 = Fq12.fq12conj f+  f2 = Fq12.fq12inv f+  newf0 = f1 * f2 -- == f^(_q ^6 - 1)+  in Fq12.fq12frobenius 2 newf0 * newf0 -- == f^((_q ^ 6 - 1) * (_q ^ 2 + 1))
+ src/Pairing/Params.hs view
@@ -0,0 +1,61 @@+-- | Parameters chosen for the pairing. The parameters chosen here+-- correspond to the BN128 curve (aka CurveSNARK).+--+-- > a = 0+-- > b = 3+-- > k = 12+-- > t = 4965661367192848881+-- > q = 21888242871839275222246405745257275088696311157297823662689037894645226208583+-- > r = 21888242871839275222246405745257275088548364400416034343698204186575808495617+-- > ξ = 9 + u+module Pairing.Params (+  _a,+  _b,+  _q,+  _r,+  _k,+  _nqr,+  _xiA,+  _xiB,+) where++import Protolude++-- | Elliptic curve coefficent+_b  :: Integer+_b = 3++-- | Elliptic curve coefficent+_a  :: Integer+_a = 0++-- | Embedding degree+_k  :: Integer+_k = 12++-- | BN parameter that determines the prime+_t :: Integer+_t = 4965661367192848881++-- | Characteristic of the finite fields we work with+_q :: Integer+_q = 36*_t^4 + 36*_t^3 + 24*_t^2 + 6*_t + 1++-- | Order of elliptic curve E(Fq) G1, and therefore also the characteristic+-- of the prime field we choose our exponents from+_r :: Integer+_r = 36*_t^4 + 36*_t^3 + 18*_t^2 + 6*_t + 1++-- | Parameter used to define the twisted curve over Fq, with xi =+-- xi_a + xi_b * i+_xiA :: Integer+_xiA = 9++-- | Parameter used to define the twisted curve over Fq, with xi =+-- xi_a + xi_b * i+_xiB :: Integer+_xiB = 1++-- | Quadratic nonresidue in Fq+_nqr :: Integer+_nqr = 21888242871839275222246405745257275088696311157297823662689037894645226208582
+ src/Pairing/Point.hs view
@@ -0,0 +1,86 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-}+--+-- | Affine point arithmetic defining the group operation on an+-- elliptic curve E(F), for some field F. In our case the field F is+-- given as some type t with Num and Fractional instances.+module Pairing.Point (+  Point(..),+  gDouble,+  gAdd,+  gNeg,+  gMul,+) where++import Protolude+import Pairing.Fq (Fq)+import Pairing.Fq2 (Fq2)++-- | Points on a curve over a field @a@ represented as either affine+-- coordinates or as a point at infinity.+data Point a+  = Point a a -- ^ Affine point+  | Infinity -- ^ Point at infinity+  deriving (Eq, Ord, Show, Functor, Generic, NFData)++{-# SPECIALISE gDouble :: Point Fq -> Point Fq #-}+{-# SPECIALISE gDouble :: Point Fq2 -> Point Fq2 #-}++{-# SPECIALISE gAdd :: Point Fq -> Point Fq -> Point Fq #-}+{-# SPECIALISE gAdd :: Point Fq2 -> Point Fq2 -> Point Fq2 #-}++{-# SPECIALISE gNeg :: Point Fq -> Point Fq #-}+{-# SPECIALISE gNeg :: Point Fq2 -> Point Fq2 #-}++{-# SPECIALISE gMul :: Point Fq -> Integer -> Point Fq #-}+{-# SPECIALISE gMul :: Point Fq2 -> Integer -> Point Fq2 #-}++-- | Point addition, provides a group structure on an elliptic curve+-- with the point at infinity as its unit.+gAdd+  :: (Fractional t, Eq t)+  => Point t+  -> Point t+  -> Point t+gAdd Infinity a = a+gAdd a Infinity = a+gAdd (Point x1 y1) (Point x2 y2)+  | x2 == x1 && y2 == y1 = gDouble (Point x1 y1)+  | x2 == x1             = Infinity+  | otherwise            = Point x' y'+  where+    l = (y2 - y1) / (x2 - x1)+    x' = l^2 - x1 - x2+    y' = -l * x' + l * x1 - y1++-- | Point doubling+gDouble :: (Fractional t, Eq t) => Point t -> Point t+gDouble Infinity = Infinity+gDouble (Point _ 0) = Infinity+gDouble (Point x y) = Point x' y'+  where+    l = 3*x^2 / (2*y)+    x' = l^2 - 2*x+    y' = -l * x' + l * x - y++-- | Negation (flipping the y component)+gNeg+  :: (Fractional t, Eq t)+  => Point t+  -> Point t+gNeg Infinity = Infinity+gNeg (Point x y) = Point x (-y)+++-- | Multiplication by a scalar+gMul+  :: (Eq t, Integral a, Fractional t)+  => Point t+  -> a+  -> Point t+gMul _ 0 = Infinity+gMul pt 1 = pt+gMul pt n+  | n < 0     = panic "gMul: negative scalar not supported"+  | even n    = gMul (gDouble pt) (n `div` 2)+  | otherwise = gAdd (gMul (gDouble pt) (n `div` 2)) pt
+ tests/Driver.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}
+ tests/TestCommon.hs view
@@ -0,0 +1,54 @@+module TestCommon+  ( commutes+  , associates+  , isIdentity+  , isInverse+  , distributes+  ) where++import Protolude++commutes+  :: Eq a+  => (a -> a -> a)+  -> a -> a -> Bool+commutes op x y+  = (x `op` y) == (y `op` x)++associates+  :: Eq a+  => (a -> a -> a)+  -> a -> a -> a -> Bool+associates op x y z+  = (x `op` (y `op` z)) == ((x `op` y) `op` z)++isIdentity+  :: Eq a+  => (a -> a -> a)+  -> a+  -> a+  -> Bool+isIdentity op e x+  = (x `op` e == x) && (e `op` x == x)++isInverse+  :: Eq a+  => (a -> a -> a)+  -> (a -> a)+  -> a+  -> a+  -> Bool+isInverse op inv e x+  = (x `op` inv x == e) && (inv x `op` x == e)++distributes+ :: Eq a+ => (a -> a -> a)+ -> (a -> a -> a)+ -> a+ -> a+ -> a+ -> Bool+distributes mult add x y z+  = x `mult` (y `add` z) == (x `mult` y) `add` (x `mult` z)+
+ tests/TestFields.hs view
@@ -0,0 +1,128 @@+{-# LANGUAGE ScopedTypeVariables #-}++module TestFields where++import Protolude++import Pairing.Fq as Fq+import Pairing.Fr as Fr+import Pairing.Fq2 as Fq2+import Pairing.Fq6 as Fq6+import Pairing.Fq12++import Test.Tasty+import Test.Tasty.QuickCheck+import Test.Tasty.HUnit++import TestCommon++-------------------------------------------------------------------------------+-- Generators+-------------------------------------------------------------------------------++instance Arbitrary Fq where+  arbitrary = Fq.new <$> arbitrary++instance Arbitrary Fr where+  arbitrary = Fr.new <$> arbitrary++instance Arbitrary Fq2 where+  arbitrary = Fq2 <$> arbitrary <*> arbitrary++instance Arbitrary Fq6 where+  arbitrary = Fq6+    <$> arbitrary+    <*> arbitrary+    <*> arbitrary++instance Arbitrary Fq12 where+  arbitrary = Fq12 <$> arbitrary <*> arbitrary++-------------------------------------------------------------------------------+-- Laws of field operations+-------------------------------------------------------------------------------++testFieldLaws+  :: forall a . (Num a, Fractional a, Eq a, Arbitrary a, Show a)+  => Proxy a+  -> TestName+  -> TestTree+testFieldLaws _ descr+  = testGroup ("Test field laws of " <> descr)+    [ testProperty "commutativity of addition"+      $ commutes ((+) :: a -> a -> a)+    , testProperty "commutativity of multiplication"+      $ commutes ((*) :: a -> a -> a)+    , testProperty "associavity of addition"+      $ associates ((+) :: a -> a -> a)+    , testProperty "associavity of multiplication"+      $ associates ((*) :: a -> a -> a)+    , testProperty "additive identity"+      $ isIdentity ((+) :: a -> a -> a) 0+    , testProperty "multiplicative identity"+      $ isIdentity ((*) :: a -> a -> a) 1+    , testProperty "additive inverse"+      $ isInverse ((+) :: a -> a -> a) negate 0+    , testProperty "multiplicative inverse"+      $ \x -> (x /= (0 :: a)) ==> isInverse ((*) :: a -> a -> a) recip 1 x+    , testProperty "multiplication distributes over addition"+      $ distributes ((*) :: a -> a -> a) (+)+    ]++-------------------------------------------------------------------------------+-- Fq+-------------------------------------------------------------------------------++test_fieldLaws_Fq :: TestTree+test_fieldLaws_Fq = testFieldLaws (Proxy :: Proxy Fq) "Fq"++-------------------------------------------------------------------------------+-- Fr+-------------------------------------------------------------------------------++test_fieldLaws_Fr :: TestTree+test_fieldLaws_Fr = testFieldLaws (Proxy :: Proxy Fr) "Fr"++-------------------------------------------------------------------------------+-- Fq2+-------------------------------------------------------------------------------++test_fieldLaws_Fq2 :: TestTree+test_fieldLaws_Fq2 = testFieldLaws (Proxy :: Proxy Fq2) "Fq2"++-- Defining property for Fq2 as an extension over Fq: u^2 = -1+unit_uRoot :: Assertion+unit_uRoot = u^2 @=? minusOne+  where+    u = Fq2.new 0 1+    minusOne = Fq2.new (-1) 0++-------------------------------------------------------------------------------+-- Fq6+-------------------------------------------------------------------------------++test_fieldLaws_Fq6 :: TestTree+test_fieldLaws_Fq6 = testFieldLaws (Proxy :: Proxy Fq6) "Fq6"++-- Defining property for Fq6 as an extension over Fq2: v^3 = 9 + u+unit_vRoot :: Assertion+unit_vRoot = v^3 @=? ninePlusU+  where+    v = Fq6.new 0 1 0+    ninePlusU = Fq6.new (Fq2.new 9 1) 0 0+++-------------------------------------------------------------------------------+-- Fq12+-------------------------------------------------------------------------------++test_fieldLaws_Fq12 :: TestTree+test_fieldLaws_Fq12 = testFieldLaws (Proxy :: Proxy Fq12) "Fq12"++-- Defining property for Fq12 as an extension over Fq6: w^2 = v+unit_wRoot :: Assertion+unit_wRoot = w^2 @=? v+  where+    w = Fq12 0 1+    v = Fq12 (Fq6 0 1 0) 0+
+ tests/TestGroups.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE FlexibleInstances #-}++module TestGroups where++import Protolude++import Pairing.Fq as Fq+import Pairing.Fq2+import Pairing.Point+import Pairing.Group +import Pairing.Params++import Test.Tasty+import Test.Tasty.QuickCheck+import Test.Tasty.HUnit++import TestCommon++-------------------------------------------------------------------------------+-- Laws of group operations+-------------------------------------------------------------------------------++testAbelianGroupLaws+  :: (Eq a, Arbitrary a, Show a)+  => (a -> a -> a)+  -> (a -> a)+  -> a+  -> TestName+  -> TestTree+testAbelianGroupLaws binOp neg ident descr+  = testGroup ("Test Abelian group laws of " <> descr)+    [ testProperty "commutativity of addition"+      $ commutes binOp+    , testProperty "associavity of addition"+      $ associates binOp+    , testProperty "additive identity"+      $ isIdentity binOp ident+    , testProperty "additive inverse"+      $ isInverse binOp neg ident+    ]++-------------------------------------------------------------------------------+-- G1+-------------------------------------------------------------------------------++prop_g1Double :: Point Fq -> Bool+prop_g1Double a = gDouble a == gAdd a a++test_groupLaws_G1 :: TestTree+test_groupLaws_G1+  = testAbelianGroupLaws gAdd gNeg (Infinity :: G1) "G1"++-- Sanity check our generators/inputs+unit_g1_valid :: Assertion+unit_g1_valid+  = assertBool "generator g1 does not satisfy curve equation" $ isOnCurveG1 g1++unit_order_g1_valid :: Assertion+unit_order_g1_valid+  = gMul g1 _r @=? Infinity++-------------------------------------------------------------------------------+-- G2+-------------------------------------------------------------------------------++prop_g2Double :: Point Fq2 -> Bool+prop_g2Double a = gDouble a == gAdd a a++test_groupLaws_G2 :: TestTree+test_groupLaws_G2+  = testAbelianGroupLaws gAdd gNeg (Infinity :: G2) "G2"++unit_g2_valid :: Assertion+unit_g2_valid+  = assertBool "generator g2 does not satisfy curve equation" $ isOnCurveG2 g2++unit_order_g2_valid :: Assertion+unit_order_g2_valid+  = gMul g2 _r @=? Infinity++-------------------------------------------------------------------------------+-- GT+-------------------------------------------------------------------------------++-- The group laws for GT are implied by the field tests for Fq12.
+ tests/TestPairing.hs view
@@ -0,0 +1,123 @@+module TestPairing where++import Protolude++import TestFields () -- for its Arbitrary instances+import Pairing.Group+import Pairing.Pairing+import Pairing.Point+import Pairing.Fq (Fq(..))+import Pairing.Fq2 (Fq2(..))+import Pairing.Fq12 (Fq12(..))+import qualified Pairing.Fq12 as Fq12+import Test.QuickCheck+import Test.Tasty.HUnit++-- Random points in G1, G2 as generated by libff.+inpG1 :: G1+inpG1 = Point+        (Fq 1368015179489954701390400359078579693043519447331113978918064868415326638035)+        (Fq 9918110051302171585080402603319702774565515993150576347155970296011118125764)+++inpG2 :: G2+inpG2 = Point+        (Fq2+         (Fq 2725019753478801796453339367788033689375851816420509565303521482350756874229)+          (Fq 7273165102799931111715871471550377909735733521218303035754523677688038059653 )+          )+        (Fq2+         (Fq 2512659008974376214222774206987427162027254181373325676825515531566330959255)+         (Fq 957874124722006818841961785324909313781880061366718538693995380805373202866)+        )++beforeExponentiation :: Fq12+beforeExponentiation+  = Fq12.new+    [ 10244919957345566208036224388367387294947954375520342002142038721148536068658+    , 20520725903107462730350108147804326707908059028221039276493719519842949720531+    , 6086095302240468555411758663466251351417777262748587710512082696159022563215+    , 3498483043828007000664704983384438380014626741459095899124517210966193962189+    , 9839947403899670326057934148290729066991318244952536153418081752510541932805+    , 9202072764973620760720243946210007480782851719144203914690329192926361472509+    , 10396963991176748371570893144856868074352236348257264320828640725417622807401+    , 16918234646064442383576265933863121396979541666923405352165222603555475148795+    , 1146287855099517708899800840204495527878843746533321795244252048321172986641+    , 15272723827732170058231690870045992172379497733734277515700990114389642596090+    , 6026541190208646112995382377707652888403252171847993766999540977939986078453+    , 4033750506662808934164561353819561401109395743946249795674228367029912558059+    ]++afterExponentiation :: Fq12+afterExponentiation+  = Fq12.new+    [ 7297928317524675251652102644847406639091474940444702627333408876432772026640+    , 18010865284024443253481973710158529446817119443459787454101328040744995455319+    , 14179125828660221708486990054318233868908974550229474018509093903907472063156+    , 19672547343219696395323430329000470270122259521813831378125910505067755316037+    , 10811020225621941034352015694422164943041584464746963243431262955968538467312+    , 18591344525433923700278298641693487837785792806011751060570085671866249379154+    , 18214296718386486500838507024306049626571830525675768493345345883297201451077+    , 19227311731387426597265504864999881769743583647552324796732605660514141916117+    , 15463354980731838106439887363063618463783317416732018231077874458188347926701+    , 3765441250413579779915094051038487360437654739171671492016287185303087270469+    , 21029416079740174485345021549306749850075185576152640151652655104272393297142+    , 19736982780723093346009254617143639137054958583796054069884522103959451721163+    ]++-- Sanity check test inputs+unit_inpG1_valid :: Assertion+unit_inpG1_valid+  = assertBool "inpG1 does not satisfy curve equation" $ isOnCurveG1 inpG1++unit_inpG2_valid :: Assertion+unit_inpG2_valid+  = assertBool "inpG2 does not satisfy curve equation" $ isOnCurveG2 inpG2++-- Test our pairing ouput against that of libff.+unit_pairingLibff_0 :: Assertion+unit_pairingLibff_0 = beforeExponentiation @=? atePairing inpG1 inpG2++unit_pairingLibff_1 :: Assertion+unit_pairingLibff_1 = afterExponentiation @=? reducedPairing inpG1 inpG2++pairingTestCount :: Int+pairingTestCount = 10++prop_pairingBilinear :: Property+prop_pairingBilinear = withMaxSuccess pairingTestCount prop+  where+    prop :: G1 -> G2 -> Integer -> Integer -> Bool+    prop e1 e2 preExp1 preExp2+      = reducedPairing (gMul e1 exp1) (gMul e2 exp2)+        == (reducedPairing e1 e2)^(exp1 * exp2)+      where+        -- Quickcheck might give us negative integers or 0, so we+        -- take the absolute values instead and add one.+        exp1 = abs preExp1 + 1+        exp2 = abs preExp2 + 1++prop_pairingNonDegenerate :: Property+prop_pairingNonDegenerate = withMaxSuccess pairingTestCount prop+  where+    prop :: G1 -> G2 -> Bool+    prop e1 e2 = or [ e1 == Infinity+                    , e2 == Infinity+                    , reducedPairing e1 e2 /= Fq12.fq12one+                    ]++-- Output of the pairing to the power _r should be the unit of GT.+prop_pairingPowerTest :: Property+prop_pairingPowerTest = withMaxSuccess pairingTestCount prop+  where+    prop :: G1 -> G2 -> Bool+    prop e1 e2 = isInGT (reducedPairing e1 e2)++prop_frobeniusFq12Correct :: Fq12 -> Bool+prop_frobeniusFq12Correct f = frobeniusNaive 1 f == Fq12.fq12frobenius 1 f++prop_finalExponentiationCorrect :: Property+prop_finalExponentiationCorrect = withMaxSuccess 10 prop+  where+    prop :: Fq12 -> Bool+    prop f = finalExponentiation f == finalExponentiationNaive f