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

{- | 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 (CekResult (..), PlcTerm, 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 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
import Test.Tasty
import Test.Tasty.QuickCheck

-- 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

arbitraryConstant :: forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant :: forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant = g -> PlcTerm
forall a. TestableAbelianGroup a => a -> PlcTerm
toTerm (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)

arbitraryScalar :: Gen PlcTerm
arbitraryScalar :: Gen PlcTerm
arbitraryScalar = Integer -> PlcTerm
integer (Integer -> PlcTerm) -> Gen Integer -> Gen PlcTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Arbitrary a => Gen a
arbitrary @Integer)

-- 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


{- 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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @g
      PlcTerm
p2 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @g
      PlcTerm
p3 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 a. TestableAbelianGroup a => 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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 a. TestableAbelianGroup a => 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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @g
      PlcTerm
p2 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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
arbitraryScalar
      PlcTerm
n <- Gen PlcTerm
arbitraryScalar
      PlcTerm
p <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e3 CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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
arbitraryScalar
      PlcTerm
n <- Gen PlcTerm
arbitraryScalar
      PlcTerm
p <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e3 CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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
arbitraryScalar
      PlcTerm
p <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @g
      PlcTerm
q <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e3 CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 a. TestableAbelianGroup a => 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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Bool
forall a. Eq a => a -> a -> Bool
== CekResult
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
      PlcTerm
p <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e2 CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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 a. TestableAbelianGroup a => 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
arbitraryScalar
      PlcTerm
n <- Gen PlcTerm
arbitraryScalar
      PlcTerm
p <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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
         ]


{- 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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @g
      case PlcTerm -> CekResult
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
        CekResult
_ -> 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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
CekError

-- | Check that flipping the sign bit in a compressed 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 a. Arbitrary a => Gen a
arbitrary @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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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 a. Arbitrary a => Gen a
arbitrary @g
      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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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 :: [CekResult]
hashed = (PlcTerm -> CekResult) -> [PlcTerm] -> [CekResult]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlcTerm -> CekResult
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
$ (CekResult -> Bool) -> [CekResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (CekResult -> CekResult -> Bool
forall a. Eq a => a -> a -> Bool
/= CekResult
CekError) [CekResult]
hashed -- Just in case
                 noDuplicates :: Property
noDuplicates = [CekResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length [CekResult]
hashed Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== [CekResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length ([CekResult] -> [CekResult]
forall a. Eq a => [a] -> [a]
nub [CekResult]
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 :: [CekResult]
hashed = (PlcTerm -> CekResult) -> [PlcTerm] -> [CekResult]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PlcTerm -> CekResult
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
$ (CekResult -> Bool) -> [CekResult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (CekResult -> CekResult -> Bool
forall a. Eq a => a -> a -> Bool
/= CekResult
CekError) [CekResult]
hashed
                 noDuplicates :: Property
noDuplicates = [CekResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length [CekResult]
hashed Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== [CekResult] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
List.length ([CekResult] -> [CekResult]
forall a. Eq a => [a] -> [a]
nub [CekResult]
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 ----------------

-- <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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @G1.Element
      PlcTerm
p2 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @G1.Element
      PlcTerm
q  <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e3 CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @G1.Element
      PlcTerm
q1 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @G2.Element
      PlcTerm
q2 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e3 CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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
arbitraryScalar
      PlcTerm
p <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @G1.Element
      PlcTerm
q <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e3 CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
cekSuccessTrue

-- finalVerify returns False for random inputs
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
arbitraryConstant @G1.Element
       PlcTerm
p2 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @G1.Element
       PlcTerm
q1 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @G2.Element
       PlcTerm
q2 <- forall g. TestableAbelianGroup g => Gen PlcTerm
arbitraryConstant @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 -> CekResult
evalTerm PlcTerm
e CekResult -> CekResult -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CekResult
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. 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. 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
         ]
        ]