-- 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 hiding (Some (..))
import Test.Tasty
import Test.Tasty.QuickCheck hiding (Some (..))

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