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

{- | Property tests for the `expModInteger` builtin -}
module Evaluation.Builtins.Integer.ExpModInteger (test_expModInteger_properties)
where

import Evaluation.Builtins.Common

import PlutusCore qualified as PLC
import PlutusCore.MkPlc (builtin, mkConstant, mkIterAppNoAnn)

import Test.QuickCheck
import Test.Tasty
import Test.Tasty.QuickCheck

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
250

mkExpMod :: Integer -> Integer -> Integer -> PlcTerm
mkExpMod :: Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m =
    let a' :: PlcTerm
a' = Integer -> PlcTerm
integer Integer
a
        e' :: PlcTerm
e' = Integer -> PlcTerm
integer Integer
e
        m' :: PlcTerm
m' = Integer -> PlcTerm
integer Integer
m
    in PlcTerm -> [PlcTerm] -> PlcTerm
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> DefaultFun -> PlcTerm
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
PLC.ExpModInteger) [PlcTerm
a',PlcTerm
e',PlcTerm
m']

-- Is a^e defined modulo m?  This depends on the properties of gcd, which we
-- just assume behaves properly.
powerExists :: Integer -> Integer -> Integer -> Bool
powerExists :: Integer -> Integer -> Integer -> Bool
powerExists Integer
a Integer
e Integer
m =
    Integer
eInteger -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>=Integer
0 Bool -> Bool -> Bool
|| (Integer
e Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
&& Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
a Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1)

-- expModInteger a e m always fails if m<=0
test_bad_modulus :: TestTree
test_bad_modulus :: TestTree
test_bad_modulus =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"modulus <= 0 -> error" (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
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<=Integer
0)
      let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m
      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 -> Property
fails PlcTerm
t

-- expModInteger a e 1 = 0 for all b and e
test_modulus_one :: TestTree
test_modulus_one :: TestTree
test_modulus_one =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"a^e mod 1 == 0 for all a and e" (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
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
1
      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 -> PlcTerm -> Property
evalOkEq PlcTerm
t PlcTerm
zero

-- Test that expModInteger a e m always lies between 0 and m-1 (inclusive)
test_in_range :: TestTree
test_in_range :: TestTree
test_in_range =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"Result lies between 0 and m-1" (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
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>=Integer
1)
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\Integer
a -> Integer -> Integer -> Integer -> Bool
powerExists Integer
a Integer
e Integer
m)
      let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m
          lb :: PlcTerm
lb = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.LessThanEqualsInteger (Integer -> PlcTerm
integer Integer
0) PlcTerm
t
          ub :: PlcTerm
ub = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.LessThanEqualsInteger PlcTerm
t (DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.SubtractInteger (Integer -> PlcTerm
integer Integer
m) (Integer -> PlcTerm
integer Integer
1))
      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 -> PlcTerm -> Property
evalOkEq PlcTerm
lb PlcTerm
true) Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. (PlcTerm -> PlcTerm -> Property
evalOkEq PlcTerm
ub PlcTerm
true)

-- For m>1, a^0 = 1 (equals 1, not congruent to 1)
test_power_zero :: TestTree
test_power_zero :: TestTree
test_power_zero =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"a^0 mod m == 1" (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
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1)
      let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
0 Integer
m
      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 -> PlcTerm -> Property
evalOkEq PlcTerm
t PlcTerm
one

-- For m>=1, expModInteger a 1 m = a (mod m) for all a
test_power_one :: TestTree
test_power_one :: TestTree
test_power_one =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"a^1 mod m == a mod m" (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
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>=Integer
1)
      let t1 :: PlcTerm
t1 = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
1 Integer
m
          t2 :: PlcTerm
t2 = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.ModInteger (() -> Integer -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () Integer
a) (() -> Integer -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () Integer
m)
      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 -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- For m >= 1 and e>=0, expModInteger a e m exists for all a
test_positive_exponent :: TestTree
test_positive_exponent :: TestTree
test_positive_exponent =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"e >= 0  => a^e mod m exists" (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
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>=Integer
0)
      Integer
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>=Integer
1)
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m
      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 -> Property
ok PlcTerm
t

-- If m>1, e<0, and gcd a m = 1, expModInteger a e m succeeds
test_negative_exponent_good :: TestTree
test_negative_exponent_good :: TestTree
test_negative_exponent_good =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"e < 0 && gcd a m == 1 => a^e mod m exists" (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
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1)
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\Integer
a -> Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
a Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1)
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<Integer
0)
      let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m
      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 -> Property
ok PlcTerm
t

-- If m>1, e<0, and gcd a m /= 1, expModInteger a e m fails
test_negative_exponent_bad :: TestTree
test_negative_exponent_bad :: TestTree
test_negative_exponent_bad =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"e < 0 && gcd a m > 1 => a^e mod m does not exist" (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
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1)
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\Integer
a -> Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
a Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
1)
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<Integer
0)
      let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m
      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 -> Property
fails PlcTerm
t

-- If m>1 and gcd a m = 1, expModInteger a e m succeeds for all e and is the
-- multiplicative inverse of expModInteger a (-e) m modulo m.
test_negated_exponent_inverse :: TestTree
test_negated_exponent_inverse :: TestTree
test_negated_exponent_inverse =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"e < 0 && gcd a m == 1 => (a^e mod m) * (a^(-e) mod m) = 1 mod m" (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
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1)
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\Integer
a -> Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
a Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1)
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary -- Positive or negative
      let t1 :: PlcTerm
t1 = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m
          t2 :: PlcTerm
t2 = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a (-Integer
e) Integer
m
          t :: PlcTerm
t = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.ModInteger (DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.MultiplyInteger PlcTerm
t1 PlcTerm
t2) (() -> Integer -> PlcTerm
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant () Integer
m)
      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 -> PlcTerm -> Property
evalOkEq PlcTerm
t PlcTerm
one  -- For m=1 this would zero.

-- (ab)^e mod m = a^e * b^e mod m
test_multiplicative :: TestTree
test_multiplicative :: TestTree
test_multiplicative =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"(ab)^e mod m == (a^e * b^e) mod m" (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
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1)
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\Integer
a -> Integer -> Integer -> Integer -> Bool
powerExists Integer
a Integer
e Integer
m)
      Integer
b <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\Integer
b -> Integer -> Integer -> Integer -> Bool
powerExists Integer
b Integer
e Integer
m)
      let t1 :: PlcTerm
t1 = Integer -> Integer -> Integer -> PlcTerm
mkExpMod (Integer
aInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
b) Integer
e Integer
m
          t2 :: PlcTerm
t2 = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.ModInteger (DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.MultiplyInteger (Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m) (Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
b Integer
e Integer
m)) (Integer -> PlcTerm
integer Integer
m)
      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 -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- a^(e+e') = a^e*a^e' whenever both powers exist
test_exponent_additive :: TestTree
test_exponent_additive :: TestTree
test_exponent_additive =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"a^(e+e') mod m == (a^e * a^e') mod m" (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
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
f <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1)
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\Integer
a -> Integer -> Integer -> Integer -> Bool
powerExists Integer
a Integer
e Integer
m Bool -> Bool -> Bool
&& Integer -> Integer -> Integer -> Bool
powerExists Integer
a Integer
f Integer
m)
      let t1 :: PlcTerm
t1 = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a (Integer
eInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
f) Integer
m
          t2 :: PlcTerm
t2 = DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.ModInteger (DefaultFun -> PlcTerm -> PlcTerm -> PlcTerm
mkApp2 DefaultFun
PLC.MultiplyInteger (Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m) (Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
f Integer
m)) (Integer -> PlcTerm
integer Integer
m)
      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 -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- a^e mod m is the same for all members of a particular congruence class.
test_periodic :: TestTree
test_periodic :: TestTree
test_periodic =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"(a+k*m)^e mod m == a^e mod m for all k" (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
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1)
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
k <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\Integer
a -> Integer -> Integer -> Integer -> Bool
powerExists Integer
a Integer
e Integer
m)
      let t1 :: PlcTerm
t1 = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m
          t2 :: PlcTerm
t2 = Integer -> Integer -> Integer -> PlcTerm
mkExpMod (Integer
aInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
kInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
*Integer
m) Integer
e  Integer
m
      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 -> PlcTerm -> Property
evalOkEq PlcTerm
t1 PlcTerm
t2

-- Test that a power exists when it should. This overlaps with some of the
-- earlier tests.
test_power_exists :: TestTree
test_power_exists :: TestTree
test_power_exists =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"Power exists" (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
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1)
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (\Integer
a -> Integer -> Integer -> Integer -> Bool
powerExists Integer
a Integer
e Integer
m)
      let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m
      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 -> Property
ok PlcTerm
t

-- Test that a power doesn't exist when it shouldn't. This overlaps with some of
-- the earlier tests.
test_power_does_not_exist :: TestTree
test_power_does_not_exist :: TestTree
test_power_does_not_exist =
    TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
    TestName
"Power does not exist" (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
m <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary Gen Integer -> (Integer -> Bool) -> Gen Integer
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>Integer
1)
      Integer
e <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      Integer
a <- Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
      let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
mkExpMod Integer
a Integer
e Integer
m
      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
$ Bool -> Bool
not (Integer -> Integer -> Integer -> Bool
powerExists Integer
a Integer
e Integer
m) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> PlcTerm -> Property
fails PlcTerm
t

test_expModInteger_properties :: TestTree
test_expModInteger_properties :: TestTree
test_expModInteger_properties =
    TestName -> [TestTree] -> TestTree
testGroup TestName
"expModInteger properties"
                  [ TestTree
test_bad_modulus
                  , TestTree
test_modulus_one
                  , TestTree
test_in_range
                  , TestTree
test_power_zero
                  , TestTree
test_power_one
                  , TestTree
test_positive_exponent
                  , TestTree
test_negative_exponent_good
                  , TestTree
test_negative_exponent_bad
                  , TestTree
test_negated_exponent_inverse
                  , TestTree
test_multiplicative
                  , TestTree
test_exponent_additive
                  , TestTree
test_periodic
                  , TestTree
test_power_exists
                  , TestTree
test_power_does_not_exist
                  ]