{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
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 (..))
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
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)
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
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
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
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
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
]
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
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
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
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
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
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
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)
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
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
]
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
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
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
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
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
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
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
numHashCollisionInputs :: Int
numHashCollisionInputs :: Int
numHashCollisionInputs = Int
200
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
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_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
]
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
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
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
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
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
]
]