diff --git a/ChangeLog.md b/ChangeLog.md new file mode 100644 --- /dev/null +++ b/ChangeLog.md @@ -0,0 +1,5 @@ +# Changelog for pairing + +## 0.1 + +* Initial release. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,164 @@ +

+ +

+ +[![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 +**G1** and **G2**, with an efficient bilinear pairing: + +*e: G1 × G2 → GT* + +# Pairing + +Let G1, G2 and GT be abelian groups of prime order `q` and let `g` and `h` elements of G1 and G2 respectively . A pairing is a non-degenerate bilinear map e: G1 × G2 → GT. + +This bilinearity property is what makes pairings such a powerful primitive in cryptography. It satisfies: +- e(g1 + g2, h) = e(g1, h) e(g2, h) +- e(g, h1 + h2) = e(g, h1) e(g, h2) + + +The non-degeneracy property guarantees non-trivial pairings for non-trivial arguments. In other words, being non-degenerate means that: +- ∀ g ≠ 1, ∃ hi ∈ G2 such that e(g, hi) ≠ 1 +- ∀ h ≠ 1, ∃ gi ∈ G1 such that e(gi, h) ≠ 1 + +An example of a pairing would be the scalar product on euclidean space <.> : Rn × Rn → R + +## Example Usage + +A simple example of calculating the optimal ate pairing given two points in G1 and G2. + +```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(Fq). E[r] is called the r-torsion and is defined as E[r] = { P ∈ E(Fq) | 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(Fq). + +G1 and G2 are subgroups of a group defined in an elliptic curve over an extension of a finite field Fq, namely E(Fqk), 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 Fqk be the smallest extension of Fq such that E(Fqk) captures more points of order `r`. +- It's the minimal value that holds r | (qk - 1). +- It's the smallest positive integer such that E[r] ⊂ E(Fqk) + +There are subtle but relevant differences in G1 and G2 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 G1 = E[r] ∩ Ker(π - [1]) and G2 = E[r] ∩ Ker(π - [q]) and there is no non-trivial map φ: G2 → G1. + +## Tate Pairing + +The Tate pairing is a map: + +tr : E(Fqk)[r] × E(Fqk) / rE(Fqk) → F*qk / (F*qk)r + +defined as: + +tr(P, Q) = f(Q) + +where P ∈ E(Fqk)[r], Q is any representative in a equivalence class in E(Fqk) / rE(Fqk) and F*qk / (F*qk)r is the set of equivalence classes of F*qk under the equivalence relation a ≡ b iff a / b ∈ (F*qk)r. 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*qk / (F*qk)r to the power of (qk - 1) / r. It maps all elements in an equivalence class to the same value. It is defined as: + +Tr(P, Q) = tr(P, Q)#Fqk / r = fr,P(Q)(qk - 1) / r. + +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 G1 and G2 are elliptic curve groups. GT 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 Fq 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 Fqk. The larger k gets, the more complex Fqk becomes and the more computationally expensive the pairing becomes. The complexity of Miller's algorithm heavily depends on the complexity of the associated Fqk-arithmetic. Therefore, the aim is to minimize the cost of arithmetic in Fqk. + +It is possible to construct an extension of a field Fqk by successively towering up intermediate fields Fqa and Fqb 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 (Fq2 and Fq3) 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) = fr,Q(P)(qk - 1) / r + +## Implementation + +We have implemented the optimal Ate pairing over the BN128 curve, i.e. we define `q` and `r` as + + * q = 36t4 + 36t3 + 24t2 + 6t + 1 + * r = 36t4 + 36t3 + 18t2 + 6t + 1 + * t = 4965661367192848881 + +The tower of finite fields we work with is defined as follows: + + * Fq is the prime field with characteristic `q` + * Fq2 := Fq[u]/u2 + 1 + * Fq6 := Fq2[v]/v3 - (9 + u) + * Fq12 := Fq6[w]/w2 - v + +The groups' definitions are: + + * G1 := E(Fq), with equation y2 = x3 + 3 + * G2 := E'(Fq2), with equation y2 = x3 + 3 / (9 + u) + * GT := μr, i.e. the `r`-th roots of unity subgroup of the multiplicative group of Fq12 + +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. +``` + diff --git a/bench/Main.hs b/bench/Main.hs new file mode 100644 --- /dev/null +++ b/bench/Main.hs @@ -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 + ] diff --git a/pairing.cabal b/pairing.cabal new file mode 100644 --- /dev/null +++ b/pairing.cabal @@ -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 diff --git a/src/Pairing/CyclicGroup.hs b/src/Pairing/CyclicGroup.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/CyclicGroup.hs @@ -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 diff --git a/src/Pairing/Fq.hs b/src/Pairing/Fq.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Fq.hs @@ -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) diff --git a/src/Pairing/Fq12.hs b/src/Pairing/Fq12.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Fq12.hs @@ -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) diff --git a/src/Pairing/Fq2.hs b/src/Pairing/Fq2.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Fq2.hs @@ -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) diff --git a/src/Pairing/Fq6.hs b/src/Pairing/Fq6.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Fq6.hs @@ -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) diff --git a/src/Pairing/Fr.hs b/src/Pairing/Fr.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Fr.hs @@ -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" diff --git a/src/Pairing/Group.hs b/src/Pairing/Group.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Group.hs @@ -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) diff --git a/src/Pairing/Jacobian.hs b/src/Pairing/Jacobian.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Jacobian.hs @@ -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 diff --git a/src/Pairing/Pairing.hs b/src/Pairing/Pairing.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Pairing.hs @@ -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)) diff --git a/src/Pairing/Params.hs b/src/Pairing/Params.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Params.hs @@ -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 diff --git a/src/Pairing/Point.hs b/src/Pairing/Point.hs new file mode 100644 --- /dev/null +++ b/src/Pairing/Point.hs @@ -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 diff --git a/tests/Driver.hs b/tests/Driver.hs new file mode 100644 --- /dev/null +++ b/tests/Driver.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-} diff --git a/tests/TestCommon.hs b/tests/TestCommon.hs new file mode 100644 --- /dev/null +++ b/tests/TestCommon.hs @@ -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) + diff --git a/tests/TestFields.hs b/tests/TestFields.hs new file mode 100644 --- /dev/null +++ b/tests/TestFields.hs @@ -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 + diff --git a/tests/TestGroups.hs b/tests/TestGroups.hs new file mode 100644 --- /dev/null +++ b/tests/TestGroups.hs @@ -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. diff --git a/tests/TestPairing.hs b/tests/TestPairing.hs new file mode 100644 --- /dev/null +++ b/tests/TestPairing.hs @@ -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