-- editorconfig-checker-disable
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}

{-# OPTIONS_GHC -Wno-dodgy-imports #-}

{- | Property tests for the BLS12-381 builtins -}
module Evaluation.Builtins.BLS12_381
where

import Evaluation.Builtins.BLS12_381.TestClasses
import Evaluation.Builtins.BLS12_381.Utils
import Evaluation.Builtins.Common (PlcTerm, TypeErrorOrCekResult (..), bytestring, cekSuccessFalse,
                                   cekSuccessTrue, evalTerm, integer, mkApp2)
import PlutusCore.Crypto.BLS12_381.G1 qualified as G1
import PlutusCore.Crypto.BLS12_381.G2 qualified as G2
import PlutusCore.Default
import PlutusCore.Generators.QuickCheck.Builtin (arbitraryBuiltin)
import UntypedPlutusCore qualified as UPLC

import Cardano.Crypto.EllipticCurve.BLS12_381 (scalarPeriod)
import Control.Monad (replicateM)
import Data.ByteString as BS (empty, length, pack)
import Data.List as List (foldl', genericReplicate, length, nub)
import Text.Printf (printf)

import Test.QuickCheck hiding (Some (..))
import Test.Tasty
import Test.Tasty.QuickCheck hiding (Some (..))

import PlutusCore.MkPlc (mkConstant)

-- QuickCheck utilities

mkTestName :: forall g. TestableAbelianGroup g => String -> String
mkTestName :: forall g. TestableAbelianGroup g => String -> String
mkTestName String
s = String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"%s_%s" (forall a. TestableAbelianGroup a => String
groupName @g) String
s

withNTests :: Testable prop => prop -> Property
withNTests :: forall prop. Testable prop => prop -> Property
withNTests = Int -> prop -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
200


-- QuickCheck generators for scalars and group elements as PLC terms

-- Convert objects to terms, just for convenience.
asPlc :: DefaultUni `Contains` a => a -> PlcTerm
asPlc :: forall a. Contains DefaultUni a => a -> PlcTerm
asPlc = () -> a -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant ()

{- Generate an arbitrary scalar.  Scalars map onto elements of Z_p where p is the
   255-bit prime order of the groups involved in BLS12_381.  This generator
   supplies integers up to 10000 bits long to give us some confidence that the
   reduction is handled properly.
-}
arbitraryScalar :: Gen Integer
arbitraryScalar :: Gen Integer
arbitraryScalar =
  [(Int, Gen Integer)] -> Gen Integer
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [ (Int
1, forall a. ArbitraryBuiltin a => Gen a
arbitraryBuiltin @Integer)
            , (Int
4, (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (-Integer
b, Integer
b))]
  where b :: Integer
b = (Integer
2::Integer)Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
10000::Integer)

-- Arbitrary scalar as PLC constant
arbitraryPlcScalar :: Gen PlcTerm
arbitraryPlcScalar :: Gen PlcTerm
arbitraryPlcScalar = Integer -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc (Integer -> PlcTerm) -> Gen Integer -> Gen PlcTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Integer
arbitraryScalar

-- Arbitrary group element as PLC constant
arbitraryPlcConst :: forall g. (DefaultUni `Contains` g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst :: forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst = g -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc (g -> PlcTerm) -> Gen g -> Gen PlcTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary @g

-- Arbitrary nonzero group element as PLC constant
arbitraryNonZeroPlcConst :: forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryNonZeroPlcConst :: forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryNonZeroPlcConst = g -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc (g -> PlcTerm) -> Gen g -> Gen PlcTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall g. TestableAbelianGroup g => Gen g
arbitraryNonZero @g

{- Generic tests for the TestableAbelianGroup class.  Later these are instantiated
   at the G1 and G2 types. -}

---------------- G is an Abelian group ----------------

-- | Group addition is associative.
test_add_assoc :: forall g. TestableAbelianGroup g => TestTree
test_add_assoc :: forall g. TestableAbelianGroup g => TestTree
test_add_assoc =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"add_assoc") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p1 <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      PlcTerm
p2 <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      PlcTerm
p3 <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g PlcTerm
p1 (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g PlcTerm
p2 PlcTerm
p3)) (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g PlcTerm
p1 PlcTerm
p2) PlcTerm
p3)
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | Zero is an identity for addition.
test_add_zero :: forall g. TestableAbelianGroup g => TestTree
test_add_zero :: forall g. TestableAbelianGroup g => TestTree
test_add_zero =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"add_zero") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g  PlcTerm
p (PlcTerm -> PlcTerm) -> PlcTerm -> PlcTerm
forall a b. (a -> b) -> a -> b
$ forall g. TestableAbelianGroup g => PlcTerm
zeroTerm @g) PlcTerm
p
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | Every element has an inverse
-- | a+(-a) = 0 for all group elements.
test_neg :: forall g. TestableAbelianGroup g => TestTree
test_neg :: forall g. TestableAbelianGroup g => TestTree
test_neg =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"additive_inverse") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g PlcTerm
p (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm
negTerm @g PlcTerm
p)) (PlcTerm -> PlcTerm) -> PlcTerm -> PlcTerm
forall a b. (a -> b) -> a -> b
$ forall g. TestableAbelianGroup g => PlcTerm
zeroTerm @g
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | Group addition is commutative.
test_add_commutative :: forall g. TestableAbelianGroup g => TestTree
test_add_commutative :: forall g. TestableAbelianGroup g => TestTree
test_add_commutative =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"add_commutative") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p1 <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      PlcTerm
p2 <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g PlcTerm
p1 PlcTerm
p2) (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g PlcTerm
p2 PlcTerm
p1)
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

test_is_an_abelian_group :: forall g. TestableAbelianGroup g => TestTree
test_is_an_abelian_group :: forall g. TestableAbelianGroup g => TestTree
test_is_an_abelian_group =
    String -> [TestTree] -> TestTree
testGroup (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"is_an_abelian_group")
              [ forall g. TestableAbelianGroup g => TestTree
test_add_assoc       @g
              , forall g. TestableAbelianGroup g => TestTree
test_add_zero        @g
              , forall g. TestableAbelianGroup g => TestTree
test_neg             @g
              , forall g. TestableAbelianGroup g => TestTree
test_add_commutative @g
              ]

---------------- Z acts on G correctly ----------------

-- | (ab)p = a(bp) for all scalars a and b and all group elements p.
test_scalarMul_assoc :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_assoc :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_assoc =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"scalarMul_mul_assoc") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
m <- Gen PlcTerm
arbitraryPlcScalar
      PlcTerm
n <- Gen PlcTerm
arbitraryPlcScalar
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e1 :: PlcTerm
e1 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g (DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
MultiplyInteger PlcTerm
m PlcTerm
n) PlcTerm
p
          e2 :: PlcTerm
e2 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
m (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
n PlcTerm
p)
          e3 :: PlcTerm
e3 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g PlcTerm
e1 PlcTerm
e2
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e3 TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | (a+b)p = ap +bp for all scalars a and b and all group elements p.
test_scalarMul_distributive_left :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_distributive_left :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_distributive_left =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"scalarMul_distributive_left") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$  do
      PlcTerm
m <- Gen PlcTerm
arbitraryPlcScalar
      PlcTerm
n <- Gen PlcTerm
arbitraryPlcScalar
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e1 :: PlcTerm
e1 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g (DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
AddInteger PlcTerm
m PlcTerm
n) PlcTerm
p
          e2 :: PlcTerm
e2 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
m PlcTerm
p) (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
n PlcTerm
p)
          e3 :: PlcTerm
e3 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g PlcTerm
e1 PlcTerm
e2
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e3 TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | a(p+q) = ap + aq for all scalars a and all group elements p and q.
test_scalarMul_distributive_right :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_distributive_right :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_distributive_right =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"scalarMul_distributive_right") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$  do
      PlcTerm
n <- Gen PlcTerm
arbitraryPlcScalar
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      PlcTerm
q <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e1 :: PlcTerm
e1 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
n (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g PlcTerm
p PlcTerm
q)
          e2 :: PlcTerm
e2 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
n PlcTerm
p) (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
n PlcTerm
q)
          e3 :: PlcTerm
e3 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g PlcTerm
e1 PlcTerm
e2
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e3 TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | 0p = 0 for all group elements p.
test_scalarMul_zero :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_zero :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_zero =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"scalarMul_zero") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g (Integer -> PlcTerm
integer Integer
0) PlcTerm
p) (PlcTerm -> PlcTerm) -> PlcTerm -> PlcTerm
forall a b. (a -> b) -> a -> b
$ forall g. TestableAbelianGroup g => PlcTerm
zeroTerm @g
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | 1p = p for all group elements p.
test_scalarMul_one :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_one :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_one =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"scalarMul_one") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g (Integer -> PlcTerm
integer Integer
1) PlcTerm
p) PlcTerm
p
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | (-1)p = -p for all group elements p.
test_scalarMul_inverse :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_inverse :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_inverse =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"scalarMul_inverse") (Property -> TestTree)
-> (Gen Bool -> Property) -> Gen Bool -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Bool -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Bool -> TestTree) -> Gen Bool -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g (Integer -> PlcTerm
integer (-Integer
1)) PlcTerm
p) (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm
negTerm @g PlcTerm
p)
      Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Gen Bool) -> Bool -> Gen Bool
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Bool
forall a. Eq a => a -> a -> Bool
== TypeErrorOrCekResult
cekSuccessTrue

-- Check that scalar multiplication is repeated addition (including negative
-- scalars). We should really check this for scalars greater than the group
-- order, but that would be prohibitively slow because the order of G1 and G2
-- has 256 bits (about 5*10^76).
test_scalarMul_repeated_addition :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_repeated_addition :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_repeated_addition =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"scalarMul_repeated_addition") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      Integer
n <- Int -> Gen Integer -> Gen Integer
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Int
100 Gen Integer
forall a. Arbitrary a => Gen a
arbitrary  -- number of additions
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e1 :: PlcTerm
e1 = Integer -> PlcTerm -> PlcTerm
repeatedAdd Integer
n PlcTerm
p
          e2 :: PlcTerm
e2 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g (Integer -> PlcTerm
integer Integer
n) PlcTerm
p) PlcTerm
e1
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e2 TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue
          where
            repeatedAdd :: Integer -> PlcTerm -> PlcTerm
            repeatedAdd :: Integer -> PlcTerm -> PlcTerm
repeatedAdd Integer
n PlcTerm
t =
                if Integer
nInteger -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>=Integer
0
                then (PlcTerm -> PlcTerm -> PlcTerm) -> PlcTerm -> [PlcTerm] -> PlcTerm
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g) (forall g. TestableAbelianGroup g => PlcTerm
zeroTerm @g) ([PlcTerm] -> PlcTerm) -> [PlcTerm] -> PlcTerm
forall a b. (a -> b) -> a -> b
$ Integer -> PlcTerm -> [PlcTerm]
forall i a. Integral i => i -> a -> [a]
genericReplicate Integer
n PlcTerm
t
                else Integer -> PlcTerm -> PlcTerm
repeatedAdd (-Integer
n) (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm
negTerm @g PlcTerm
t)

-- (m + n|G|)p = mp for all group elements p and integers m and n.
-- We have |G1| = |G2| = scalarPeriod
test_scalarMul_periodic :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_periodic :: forall g. TestableAbelianGroup g => TestTree
test_scalarMul_periodic =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"scalarMul_periodic") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
m <- Gen PlcTerm
arbitraryPlcScalar
      PlcTerm
n <- Gen PlcTerm
arbitraryPlcScalar
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e1 :: PlcTerm
e1 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
m PlcTerm
p
          k :: PlcTerm
k = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
AddInteger PlcTerm
m (DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
MultiplyInteger PlcTerm
n (Integer -> PlcTerm
integer Integer
scalarPeriod))
          e2 :: PlcTerm
e2 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
k PlcTerm
p -- k = m+n|G|
          e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g PlcTerm
e1 PlcTerm
e2
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

test_Z_action_good :: forall g. TestableAbelianGroup g => TestTree
test_Z_action_good :: forall g. TestableAbelianGroup g => TestTree
test_Z_action_good =
    String -> [TestTree] -> TestTree
testGroup (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Z acts correctly on %s" (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ forall a. TestableAbelianGroup a => String
groupName @g)
         [ forall g. TestableAbelianGroup g => TestTree
test_scalarMul_assoc              @g
         , forall g. TestableAbelianGroup g => TestTree
test_scalarMul_distributive_left  @g
         , forall g. TestableAbelianGroup g => TestTree
test_scalarMul_distributive_right @g
         , forall g. TestableAbelianGroup g => TestTree
test_scalarMul_zero               @g
         , forall g. TestableAbelianGroup g => TestTree
test_scalarMul_one                @g
         , forall g. TestableAbelianGroup g => TestTree
test_scalarMul_inverse            @g
         , forall g. TestableAbelianGroup g => TestTree
test_scalarMul_repeated_addition  @g
         , forall g. TestableAbelianGroup g => TestTree
test_scalarMul_periodic           @g
         ]

---------------- Multi-scalar multiplication behaves correctly ----------------

{- Check that multiScalarMul [s_1, ..., s_m] [p_1, ..., p_n] =
      0 + (s_1*p_1) + ... + (s_r*p_r) where r = min m n
-}
test_multiScalarMul_correct :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_correct :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_correct =
  String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
  (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"multiScalarMul_is_iterated_mul_and_add") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
     [Integer]
scalars <- Gen Integer -> Gen [Integer]
forall a. Gen a -> Gen [a]
listOf Gen Integer
arbitraryScalar
     [g]
points  <- Gen g -> Gen [g]
forall a. Gen a -> Gen [a]
listOf (forall a. Arbitrary a => Gen a
arbitrary @g)
     let e1 :: PlcTerm
e1 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
multiScalarMulTerm @g ([Integer] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [Integer]
scalars) ([g] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [g]
points)
         mkMulAdd :: PlcTerm -> (PlcTerm, PlcTerm) -> PlcTerm
mkMulAdd PlcTerm
acc (PlcTerm
s, PlcTerm
x) = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @g PlcTerm
acc (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @g PlcTerm
s PlcTerm
x)
         scalarTerms :: [PlcTerm]
scalarTerms = (Integer -> PlcTerm) -> [Integer] -> [PlcTerm]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Integer -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [Integer]
scalars
         pointTerms :: [PlcTerm]
pointTerms  = (g -> PlcTerm) -> [g] -> [PlcTerm]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [g]
points
         e2 :: PlcTerm
e2 = (PlcTerm -> (PlcTerm, PlcTerm) -> PlcTerm)
-> PlcTerm -> [(PlcTerm, PlcTerm)] -> PlcTerm
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' PlcTerm -> (PlcTerm, PlcTerm) -> PlcTerm
mkMulAdd (forall g. TestableAbelianGroup g => PlcTerm
zeroTerm @g) ([PlcTerm] -> [PlcTerm] -> [(PlcTerm, PlcTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [PlcTerm]
scalarTerms [PlcTerm]
pointTerms)
         -- ^ Remember that zip truncates the longer list and `multiScalarMul`
         -- is supposed to disregard extra elements if the inputs have different
         -- lengths.
     Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e1 TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e2

-- Check that multiScalarMul returns the zero point if the list of scalars is empty
test_multiScalarMul_no_scalars :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_no_scalars :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_no_scalars =
  String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
  (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"multiScalarMul_returns_zero_if_no_scalars") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
     [g]
points <- Gen g -> Gen [g]
forall a. Gen a -> Gen [a]
listOf (forall a. Arbitrary a => Gen a
arbitrary @g)
     let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
multiScalarMulTerm @g ([Integer] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc ([] @Integer)) ([g] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [g]
points)
     Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== PlcTerm -> TypeErrorOrCekResult
evalTerm (forall g. TestableAbelianGroup g => PlcTerm
zeroTerm @g)

-- Check that multiScalarMul returns the zero point if the list of points is empty
test_multiScalarMul_no_points :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_no_points :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_no_points =
  String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
  (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"multiScalarMul_returns_zero_if_no_points") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
     [Integer]
scalars <- Gen Integer -> Gen [Integer]
forall a. Gen a -> Gen [a]
listOf Gen Integer
arbitraryScalar
     let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
multiScalarMulTerm @g ([Integer] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [Integer]
scalars) ([g] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc ([] @g))
     Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== PlcTerm -> TypeErrorOrCekResult
evalTerm (forall g. TestableAbelianGroup g => PlcTerm
zeroTerm @g)

{- Check that the result of multiScalarMul doesn't change if you permute the input
   pairs (disregarding extra inputs when the two input lists are of different
   lengths).
-}
test_multiScalarMul_permutation :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_permutation :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_permutation =
  String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
  (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"multiScalarMul_invariant_under_permutation") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
     [(Integer, g)]
l <- Gen (Integer, g) -> Gen [(Integer, g)]
forall a. Gen a -> Gen [a]
listOf ((,) (Integer -> g -> (Integer, g))
-> Gen Integer -> Gen (g -> (Integer, g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Integer
arbitraryScalar Gen (g -> (Integer, g)) -> Gen g -> Gen (Integer, g)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @g)
     [(Integer, g)]
l' <- [(Integer, g)] -> Gen [(Integer, g)]
forall a. [a] -> Gen [a]
shuffle [(Integer, g)]
l
     let ([Integer]
scalars, [g]
points) = [(Integer, g)] -> ([Integer], [g])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Integer, g)]
l
         ([Integer]
scalars', [g]
points') = [(Integer, g)] -> ([Integer], [g])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Integer, g)]
l'
         e1 :: PlcTerm
e1 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
multiScalarMulTerm @g ([Integer] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [Integer]
scalars) ([g] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [g]
points)
         e2 :: PlcTerm
e2 = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
multiScalarMulTerm @g ([Integer] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [Integer]
scalars') ([g] -> PlcTerm
forall a. Contains DefaultUni a => a -> PlcTerm
asPlc [g]
points')
     Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e1 TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e2


test_multiScalarMul :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul :: forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul =
  String -> [TestTree] -> TestTree
testGroup (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Multi-scalar multiplication behaves correctly for %s" (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ forall a. TestableAbelianGroup a => String
groupName @g)
  [ forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_correct     @g
  , forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_no_scalars  @g
  , forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_no_points   @g
  , forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul_permutation @g
  ]

{- Generic tests for the HashAndCompress class.  Later these are instantiated at
   the G1 and G2 types. -}

test_roundtrip_compression :: forall g. HashAndCompress g => TestTree
test_roundtrip_compression :: forall g. HashAndCompress g => TestTree
test_roundtrip_compression =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"roundtrip_compression") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      let e :: PlcTerm
e = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g (forall a. HashAndCompress a => PlcTerm -> PlcTerm
uncompressTerm @g (forall a. HashAndCompress a => PlcTerm -> PlcTerm
compressTerm @g PlcTerm
p)) PlcTerm
p
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | Uncompression should only accept inputs of the expected length, so we check
-- it on random inputs of the incorrect length.  Inputs of the expected length
-- are excluded by the incorrectSize predicate; however even if an input did
-- have the expected length it would be very unlikely to deserialise to a point
-- in the group because the cofactors are very big (7.6*10^37 for G1 and
-- 3.1*10^152 for G2).
test_uncompression_wrong_size :: forall g. HashAndCompress g => TestTree
test_uncompression_wrong_size :: forall g. HashAndCompress g => TestTree
test_uncompression_wrong_size =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"uncompression_wrong_size") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      ByteString
b <- Gen ByteString -> (ByteString -> Bool) -> Gen ByteString
forall a. Gen a -> (a -> Bool) -> Gen a
suchThat (Int -> Gen ByteString -> Gen ByteString
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Int
128 Gen ByteString
forall a. Arbitrary a => Gen a
arbitrary) ByteString -> Bool
incorrectSize
      let e :: PlcTerm
e = forall a. HashAndCompress a => PlcTerm -> PlcTerm
uncompressTerm @g (ByteString -> PlcTerm
bytestring ByteString
b)
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
CekError
    where incorrectSize :: ByteString -> Bool
incorrectSize ByteString
s = ByteString -> Int
BS.length ByteString
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= forall a. HashAndCompress a => Int
compressedSize @g

-- | This tests the case we've omitted in the previous test, and should fail
-- with very high probablity.  It's quite difficult to test this with random
-- inputs.  We can improve our chances of getting a bytestring which encodes a
-- point on the curve by setting the compression bit and clearing the infinity
-- bit, but about 50% of the samples will still not be the x-coordinate of a
-- point on the curve.  We can also generate points with an x-coordinate that's
-- bigger than the field size (especially for G2), which will give us a bad
-- encoding.  Maybe this just isn't a very good test.
test_uncompress_out_of_group :: forall g. HashAndCompress g => TestTree
test_uncompress_out_of_group :: forall g. HashAndCompress g => TestTree
test_uncompress_out_of_group =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"uncompress_out_of_group") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
99 (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      ByteString
b <- Gen ByteString -> (ByteString -> Bool) -> Gen ByteString
forall a. Gen a -> (a -> Bool) -> Gen a
suchThat (Int -> Gen ByteString -> Gen ByteString
forall a. HasCallStack => Int -> Gen a -> Gen a
resize  Int
128 Gen ByteString
forall a. Arbitrary a => Gen a
arbitrary) ByteString -> Bool
correctSize
      let b' :: ByteString
b' = Word8 -> ByteString -> ByteString
setBits Word8
compressionBit (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Word8 -> ByteString -> ByteString
clearBits Word8
infinityBit ByteString
b
      let e :: PlcTerm
e = forall a. HashAndCompress a => PlcTerm -> PlcTerm
uncompressTerm @g (ByteString -> PlcTerm
bytestring ByteString
b')
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
CekError
    where correctSize :: ByteString -> Bool
correctSize ByteString
s = ByteString -> Int
BS.length ByteString
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== forall a. HashAndCompress a => Int
compressedSize @g

-- | Check that the most significant bit is set for all compressed points
test_compression_bit_set :: forall g. HashAndCompress g => TestTree
test_compression_bit_set :: forall g. HashAndCompress g => TestTree
test_compression_bit_set =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"compression_bit_set") (Property -> TestTree)
-> (Gen Bool -> Property) -> Gen Bool -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Bool -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Bool -> TestTree) -> Gen Bool -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @g
      case PlcTerm -> TypeErrorOrCekResult
evalTerm (forall a. HashAndCompress a => PlcTerm -> PlcTerm
compressTerm @g PlcTerm
p) of
        CekSuccess (UPLC.Constant ()
_ (Some (ValueOf DefaultUni (Esc a)
DefaultUniByteString a
bs)))
            -> Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Gen Bool) -> Bool -> Gen Bool
forall a b. (a -> b) -> a -> b
$ Word8 -> ByteString -> Bool
isSet Word8
compressionBit a
ByteString
bs
        TypeErrorOrCekResult
_ -> Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

-- | Check that bytestrings with the compression bit clear fail to uncompress.
test_clear_compression_bit :: forall g. HashAndCompress g => TestTree
test_clear_compression_bit :: forall g. HashAndCompress g => TestTree
test_clear_compression_bit =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"clear_compression_bit") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      g
p <- forall a. Arbitrary a => Gen a
arbitrary @g
      let b :: ByteString
b = Word8 -> ByteString -> ByteString
clearBits Word8
compressionBit (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ forall a. HashAndCompress a => a -> ByteString
compress @g g
p
          e :: PlcTerm
e = forall a. HashAndCompress a => PlcTerm -> PlcTerm
uncompressTerm @g (ByteString -> PlcTerm
bytestring ByteString
b)
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
CekError

-- | Check that flipping the sign bit in a compressed nonzero point gives the
-- inverse of the point.
test_flip_sign_bit :: forall g. HashAndCompress g => TestTree
test_flip_sign_bit :: forall g. HashAndCompress g => TestTree
test_flip_sign_bit =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"flip_sign_bit") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      g
p <- forall g. TestableAbelianGroup g => Gen g
arbitraryNonZero @g
      let b1 :: ByteString
b1 = forall a. HashAndCompress a => a -> ByteString
compress @g g
p
          b2 :: ByteString
b2 = Word8 -> ByteString -> ByteString
flipBits Word8
signBit ByteString
b1
          e1 :: PlcTerm
e1 = forall a. HashAndCompress a => PlcTerm -> PlcTerm
uncompressTerm @g (ByteString -> PlcTerm
bytestring ByteString
b1)
          e2 :: PlcTerm
e2 = forall a. HashAndCompress a => PlcTerm -> PlcTerm
uncompressTerm @g (ByteString -> PlcTerm
bytestring ByteString
b2)
          e :: PlcTerm
e  = forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
eqTerm @g PlcTerm
e2 (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm
negTerm @g PlcTerm
e1)
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- | Check that bytestrings with the infinity bit set fail to uncompress.
test_set_infinity_bit :: forall g. HashAndCompress g => TestTree
test_set_infinity_bit :: forall g. HashAndCompress g => TestTree
test_set_infinity_bit =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"set_infinity_bit") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      g
p <- forall g. TestableAbelianGroup g => Gen g
arbitraryNonZero @g  -- This will have the infinity bit set.
      let b :: ByteString
b = Word8 -> ByteString -> ByteString
setBits Word8
infinityBit (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ forall a. HashAndCompress a => a -> ByteString
compress @g g
p
          e :: PlcTerm
e = forall a. HashAndCompress a => PlcTerm -> PlcTerm
uncompressTerm @g (ByteString -> PlcTerm
bytestring ByteString
b)
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
CekError


-- We test for hash collisions by generating a list of `numHashCollisionTests`
-- bytestrings, discarding duplicates, hashing the remaining bytestrings, and
-- then checking that no two of the resulting group elements are equal. The time
-- taken by the tests increases quadratically with the number of bytestrings,
-- and is quite long even for numHashCollisionTests = 50.
numHashCollisionInputs :: Int
numHashCollisionInputs :: Int
numHashCollisionInputs = Int
200

-- | Hashing into G1 or G2 should be collision-free.  A failure here would
-- suggest an implementation error somewhere.  Here we test multiple messages
-- but always use an empty Domain Separation Tag.
test_no_hash_collisions :: forall g. HashAndCompress g => TestTree
test_no_hash_collisions :: forall g. HashAndCompress g => TestTree
test_no_hash_collisions =
    let emptyBS :: PlcTerm
emptyBS = ByteString -> PlcTerm
bytestring ByteString
BS.empty
    in String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
           (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"no_hash_collisions") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
1 (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
             [ByteString]
msgs <- [ByteString] -> [ByteString]
forall a. Eq a => [a] -> [a]
nub ([ByteString] -> [ByteString])
-> Gen [ByteString] -> Gen [ByteString]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen ByteString -> Gen [ByteString]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
numHashCollisionInputs Gen ByteString
forall a. Arbitrary a => Gen a
arbitrary
             let terms :: [PlcTerm]
terms = (ByteString -> PlcTerm) -> [ByteString] -> [PlcTerm]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ByteString
msg -> forall a. HashAndCompress a => PlcTerm -> PlcTerm -> PlcTerm
hashToGroupTerm @g (ByteString -> PlcTerm
bytestring ByteString
msg) PlcTerm
emptyBS) [ByteString]
msgs
                 hashed :: [TypeErrorOrCekResult]
hashed = (PlcTerm -> TypeErrorOrCekResult)
-> [PlcTerm] -> [TypeErrorOrCekResult]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlcTerm -> TypeErrorOrCekResult
evalTerm [PlcTerm]
terms
                 noErrors :: Property
noErrors = Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ (TypeErrorOrCekResult -> Bool) -> [TypeErrorOrCekResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TypeErrorOrCekResult -> TypeErrorOrCekResult -> Bool
forall a. Eq a => a -> a -> Bool
/= TypeErrorOrCekResult
CekError) [TypeErrorOrCekResult]
hashed -- Just in case
                 noDuplicates :: Property
noDuplicates = [TypeErrorOrCekResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length [TypeErrorOrCekResult]
hashed Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== [TypeErrorOrCekResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length ([TypeErrorOrCekResult] -> [TypeErrorOrCekResult]
forall a. Eq a => [a] -> [a]
nub [TypeErrorOrCekResult]
hashed)
             Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ Property
noErrors Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. Property
noDuplicates

-- | Test that we get no collisions if we keep the message constant but vary the
-- DST.  DSTs can be at most 255 bytes long in Plutus Core; there's a test
-- elsewhere that we get a failure for longer DSTs.  This test could fail (but
-- not because of a hash collision) if we let it generate longer DSTs because
-- the final list could contain multiple occurrences of CekError.
test_no_hash_collisions_dst :: forall g. HashAndCompress g => TestTree
test_no_hash_collisions_dst :: forall g. HashAndCompress g => TestTree
test_no_hash_collisions_dst =
    let msg :: PlcTerm
msg = ByteString -> PlcTerm
bytestring (ByteString -> PlcTerm) -> ByteString -> PlcTerm
forall a b. (a -> b) -> a -> b
$ [Word8] -> ByteString
pack [Word8
0x01, Word8
0x02]
        maxDstSize :: Int
maxDstSize = Int
255
    in String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
           (forall g. TestableAbelianGroup g => String -> String
mkTestName @g String
"no_hash_collisions_dst") (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
1 (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
             [ByteString]
dsts <- [ByteString] -> [ByteString]
forall a. Eq a => [a] -> [a]
nub ([ByteString] -> [ByteString])
-> Gen [ByteString] -> Gen [ByteString]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen ByteString -> Gen [ByteString]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
numHashCollisionInputs (Int -> Gen ByteString -> Gen ByteString
forall a. HasCallStack => Int -> Gen a -> Gen a
resize Int
maxDstSize Gen ByteString
forall a. Arbitrary a => Gen a
arbitrary)
             let terms :: [PlcTerm]
terms = (ByteString -> PlcTerm) -> [ByteString] -> [PlcTerm]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ByteString
dst -> forall a. HashAndCompress a => PlcTerm -> PlcTerm -> PlcTerm
hashToGroupTerm @g PlcTerm
msg (ByteString -> PlcTerm
bytestring ByteString
dst)) [ByteString]
dsts
                 hashed :: [TypeErrorOrCekResult]
hashed = (PlcTerm -> TypeErrorOrCekResult)
-> [PlcTerm] -> [TypeErrorOrCekResult]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlcTerm -> TypeErrorOrCekResult
evalTerm [PlcTerm]
terms
                 noErrors :: Property
noErrors = Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ (TypeErrorOrCekResult -> Bool) -> [TypeErrorOrCekResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TypeErrorOrCekResult -> TypeErrorOrCekResult -> Bool
forall a. Eq a => a -> a -> Bool
/= TypeErrorOrCekResult
CekError) [TypeErrorOrCekResult]
hashed
                 noDuplicates :: Property
noDuplicates = [TypeErrorOrCekResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length [TypeErrorOrCekResult]
hashed Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== [TypeErrorOrCekResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length ([TypeErrorOrCekResult] -> [TypeErrorOrCekResult]
forall a. Eq a => [a] -> [a]
nub [TypeErrorOrCekResult]
hashed)
             Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ Property
noErrors Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&. Property
noDuplicates

test_compress_hash :: forall g. HashAndCompress g => TestTree
test_compress_hash :: forall g. HashAndCompress g => TestTree
test_compress_hash =
    String -> [TestTree] -> TestTree
testGroup (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Uncompression and hashing behave properly for %s" (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ forall a. TestableAbelianGroup a => String
groupName @g)
         [ forall g. HashAndCompress g => TestTree
test_roundtrip_compression    @g
         , forall g. HashAndCompress g => TestTree
test_uncompression_wrong_size @g
         , forall g. HashAndCompress g => TestTree
test_compression_bit_set      @g
         , forall g. HashAndCompress g => TestTree
test_clear_compression_bit    @g
         , forall g. HashAndCompress g => TestTree
test_flip_sign_bit            @g
         , forall g. HashAndCompress g => TestTree
test_set_infinity_bit         @g
         , forall g. HashAndCompress g => TestTree
test_uncompress_out_of_group  @g
         , forall g. HashAndCompress g => TestTree
test_no_hash_collisions       @g
         , forall g. HashAndCompress g => TestTree
test_no_hash_collisions_dst   @g
         ]


---------------- Pairing properties ----------------

-- Constructing pairing terms

millerLoopTerm :: PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm :: PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
Bls12_381_millerLoop

mulMlResultTerm :: PlcTerm -> PlcTerm -> PlcTerm
mulMlResultTerm :: PlcTerm -> PlcTerm -> PlcTerm
mulMlResultTerm = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
Bls12_381_mulMlResult

finalVerifyTerm :: PlcTerm -> PlcTerm -> PlcTerm
finalVerifyTerm :: PlcTerm -> PlcTerm -> PlcTerm
finalVerifyTerm = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
Bls12_381_finalVerify

-- <p1+p2,q> = <p1,q>.<p2,q>
test_pairing_left_additive :: TestTree
test_pairing_left_additive :: TestTree
test_pairing_left_additive =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    String
"pairing_left_additive" (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p1 <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @G1.Element
      PlcTerm
p2 <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @G1.Element
      PlcTerm
q  <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @G2.Element
      let e1 :: PlcTerm
e1 = PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @G1.Element PlcTerm
p1 PlcTerm
p2) PlcTerm
q
          e2 :: PlcTerm
e2 = PlcTerm -> PlcTerm -> PlcTerm
mulMlResultTerm (PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm PlcTerm
p1 PlcTerm
q) (PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm PlcTerm
p2 PlcTerm
q)
          e3 :: PlcTerm
e3 = PlcTerm -> PlcTerm -> PlcTerm
finalVerifyTerm PlcTerm
e1 PlcTerm
e2
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e3 TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- <p,q1+q2> = <p,q1>.<p,q2>
test_pairing_right_additive :: TestTree
test_pairing_right_additive :: TestTree
test_pairing_right_additive =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    String
"pairing_right_additive" (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
p  <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @G1.Element
      PlcTerm
q1 <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @G2.Element
      PlcTerm
q2 <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @G2.Element
      let e1 :: PlcTerm
e1 = PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm PlcTerm
p (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
addTerm @G2.Element PlcTerm
q1 PlcTerm
q2)
          e2 :: PlcTerm
e2 = PlcTerm -> PlcTerm -> PlcTerm
mulMlResultTerm (PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm PlcTerm
p PlcTerm
q1) (PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm PlcTerm
p PlcTerm
q2)
          e3 :: PlcTerm
e3 = PlcTerm -> PlcTerm -> PlcTerm
finalVerifyTerm PlcTerm
e1 PlcTerm
e2
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e3 TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- <[n]p,q> = <p,[n]q>
test_pairing_balanced :: TestTree
test_pairing_balanced :: TestTree
test_pairing_balanced =
     String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
     String
"pairing_balanced" (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
     Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
      PlcTerm
n <- Gen PlcTerm
arbitraryPlcScalar
      PlcTerm
p <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @G1.Element
      PlcTerm
q <- forall g. (Contains DefaultUni g, Arbitrary g) => Gen PlcTerm
arbitraryPlcConst @G2.Element
      let e1 :: PlcTerm
e1 = PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @G1.Element PlcTerm
n PlcTerm
p) PlcTerm
q
          e2 :: PlcTerm
e2 = PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm PlcTerm
p (forall a. TestableAbelianGroup a => PlcTerm -> PlcTerm -> PlcTerm
scalarMulTerm @G2.Element PlcTerm
n PlcTerm
q)
          e3 :: PlcTerm
e3 = PlcTerm -> PlcTerm -> PlcTerm
finalVerifyTerm PlcTerm
e1 PlcTerm
e2
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e3 TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessTrue

-- Check that `finalVerify` returns False for random inputs.  We exclude the
-- zero points because `millerLoop` returns 1 if either of its inputs is zero.
test_random_pairing :: TestTree
test_random_pairing :: TestTree
test_random_pairing =
    String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty
    String
"pairing_random_unequal" (Property -> TestTree)
-> (Gen Property -> Property) -> Gen Property -> TestTree
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Gen Property -> Property
forall prop. Testable prop => prop -> Property
withNTests (Gen Property -> TestTree) -> Gen Property -> TestTree
forall a b. (a -> b) -> a -> b
$ do
       PlcTerm
p1 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryNonZeroPlcConst @G1.Element
       PlcTerm
p2 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryNonZeroPlcConst @G1.Element
       PlcTerm
q1 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryNonZeroPlcConst @G2.Element
       PlcTerm
q2 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryNonZeroPlcConst @G2.Element
       Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ PlcTerm
p1 PlcTerm -> PlcTerm -> Bool
forall a. Eq a => a -> a -> Bool
/= PlcTerm
p2 Bool -> Bool -> Bool
&& PlcTerm
q1 PlcTerm -> PlcTerm -> Bool
forall a. Eq a => a -> a -> Bool
/= PlcTerm
q2 Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==>
            let e :: PlcTerm
e = PlcTerm -> PlcTerm -> PlcTerm
finalVerifyTerm (PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm PlcTerm
p1 PlcTerm
q1) (PlcTerm -> PlcTerm -> PlcTerm
millerLoopTerm PlcTerm
p2 PlcTerm
q2)
            in PlcTerm -> TypeErrorOrCekResult
evalTerm PlcTerm
e TypeErrorOrCekResult -> TypeErrorOrCekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== TypeErrorOrCekResult
cekSuccessFalse


-- All of the tests

test_BLS12_381 :: TestTree
test_BLS12_381 :: TestTree
test_BLS12_381 = String -> [TestTree] -> TestTree
testGroup String
"BLS12-381" [
         String -> [TestTree] -> TestTree
testGroup String
"G1 properties"
         [ forall g. TestableAbelianGroup g => TestTree
test_is_an_abelian_group @G1.Element
         , forall g. TestableAbelianGroup g => TestTree
test_Z_action_good       @G1.Element
         , forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul      @G1.Element
         , forall g. HashAndCompress g => TestTree
test_compress_hash       @G1.Element
         ]
        , String -> [TestTree] -> TestTree
testGroup String
"G2 properties"
         [ forall g. TestableAbelianGroup g => TestTree
test_is_an_abelian_group @G2.Element
         , forall g. TestableAbelianGroup g => TestTree
test_Z_action_good       @G2.Element
         , forall g. TestableAbelianGroup g => TestTree
test_multiScalarMul      @G2.Element
         , forall g. HashAndCompress g => TestTree
test_compress_hash       @G2.Element
         ]
        , String -> [TestTree] -> TestTree
testGroup String
"Pairing properties"
         [ TestTree
test_pairing_left_additive
         , TestTree
test_pairing_right_additive
         , TestTree
test_pairing_balanced
         , TestTree
test_random_pairing
         ]
        ]