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

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

import Evaluation.Builtins.Common
import Evaluation.Builtins.Integer.Common (arbitraryBigInteger)

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

import Test.Tasty (TestName, TestTree, testGroup)
import Test.Tasty.QuickCheck

numberOfTests :: Int
numberOfTests :: Int
numberOfTests = Int
400

testProp :: Testable prop => TestName -> prop -> TestTree
testProp :: forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
s prop
p = TestName -> Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProperty TestName
s (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Int -> prop -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
numberOfTests prop
p

expModInteger :: Integer -> Integer -> Integer -> PlcTerm
expModInteger :: Integer -> Integer -> Integer -> PlcTerm
expModInteger (Integer -> PlcTerm
integer -> PlcTerm
a) (Integer -> PlcTerm
integer -> PlcTerm
e) (Integer -> PlcTerm
integer -> PlcTerm
m) =
  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
prop_bad_modulus :: Gen Property
prop_bad_modulus :: Gen Property
prop_bad_modulus = do
  Integer
a <- Gen Integer
arbitraryBigInteger
  Integer
e <- Gen Integer
arbitraryBigInteger
  Integer
m <- Gen Integer
arbitraryBigInteger 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
expModInteger 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
prop_modulus_one :: Gen Property
prop_modulus_one :: Gen Property
prop_modulus_one = do
  Integer
a <- Gen Integer
arbitraryBigInteger
  Integer
e <- Gen Integer
arbitraryBigInteger
  let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
expModInteger 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)
prop_in_range :: Gen Property
prop_in_range :: Gen Property
prop_in_range = do
  Integer
m <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger
  Integer
a <- Gen Integer
arbitraryBigInteger 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
expModInteger 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 -> Property
evalOkTrue PlcTerm
lb Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. PlcTerm -> Property
evalOkTrue PlcTerm
ub

-- For m > 1, a^0 = 1 (equals 1, not congruent to 1)
prop_power_zero :: Gen Property
prop_power_zero :: Gen Property
prop_power_zero = do
  Integer
a <- Gen Integer
arbitraryBigInteger
  Integer
m <- Gen Integer
arbitraryBigInteger 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
expModInteger 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
prop_power_one :: Gen Property
prop_power_one :: Gen Property
prop_power_one = do
  Integer
a <- Gen Integer
arbitraryBigInteger
  Integer
m <- Gen Integer
arbitraryBigInteger 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
expModInteger 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
prop_positive_exponent :: Gen Property
prop_positive_exponent :: Gen Property
prop_positive_exponent = do
  Integer
e <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger 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
arbitraryBigInteger
  let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
expModInteger 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
prop_negative_exponent_good :: Gen Property
prop_negative_exponent_good :: Gen Property
prop_negative_exponent_good = do
  Integer
m <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger 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
arbitraryBigInteger 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
expModInteger 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
prop_negative_exponent_bad :: Gen Property
prop_negative_exponent_bad :: Gen Property
prop_negative_exponent_bad = do
  Integer
m <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger 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
arbitraryBigInteger 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
expModInteger 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.
prop_negated_exponent_inverse :: Gen Property
prop_negated_exponent_inverse :: Gen Property
prop_negated_exponent_inverse = do
  Integer
m <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger 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
arbitraryBigInteger -- Positive or negative
  let t1 :: PlcTerm
t1 = Integer -> Integer -> Integer -> PlcTerm
expModInteger Integer
a Integer
e Integer
m
      t2 :: PlcTerm
t2 = Integer -> Integer -> Integer -> PlcTerm
expModInteger 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 be zero.

-- (ab)^e mod m = a^e * b^e mod m
prop_multiplicative :: Gen Property
prop_multiplicative :: Gen Property
prop_multiplicative = do
  Integer
m <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger
  Integer
a <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger 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
expModInteger (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
expModInteger Integer
a Integer
e Integer
m) (Integer -> Integer -> Integer -> PlcTerm
expModInteger 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
prop_exponent_additive :: Gen Property
prop_exponent_additive :: Gen Property
prop_exponent_additive = do
  Integer
e <- Gen Integer
arbitraryBigInteger
  Integer
f <- Gen Integer
arbitraryBigInteger
  Integer
m <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger 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
expModInteger 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
expModInteger Integer
a Integer
e Integer
m) (Integer -> Integer -> Integer -> PlcTerm
expModInteger 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.
prop_periodic :: Gen Property
prop_periodic :: Gen Property
prop_periodic = do
  Integer
m <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger
  Integer
k <- Gen Integer
arbitraryBigInteger
  Integer
a <- Gen Integer
arbitraryBigInteger 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
expModInteger Integer
a Integer
e Integer
m
      t2 :: PlcTerm
t2 = Integer -> Integer -> Integer -> PlcTerm
expModInteger (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.
prop_power_exists :: Gen Property
prop_power_exists :: Gen Property
prop_power_exists = do
   Integer
m <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger
   Integer
a <- Gen Integer
arbitraryBigInteger 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
expModInteger 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.
prop_power_does_not_exist :: Gen Property
prop_power_does_not_exist :: Gen Property
prop_power_does_not_exist = do
  Integer
m <- Gen Integer
arbitraryBigInteger 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
arbitraryBigInteger
  Integer
a <- Gen Integer
arbitraryBigInteger
  let t :: PlcTerm
t = Integer -> Integer -> Integer -> PlcTerm
expModInteger 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_integer_exp_mod_properties :: TestTree
test_integer_exp_mod_properties :: TestTree
test_integer_exp_mod_properties =
  TestName -> [TestTree] -> TestTree
testGroup TestName
"Property tests for expModInteger"
    [ TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"modulus <= 0 -> error" Gen Property
prop_bad_modulus
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"a^e mod 1 == 0 for all a and e" Gen Property
prop_modulus_one
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"Result lies between 0 and m-1" Gen Property
prop_in_range
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"a^0 mod m == 1" Gen Property
prop_power_zero
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"a^1 mod m == a mod m" Gen Property
prop_power_one
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"e >= 0  => a^e mod m exists" Gen Property
prop_positive_exponent
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"e < 0 && gcd a m == 1 => a^e mod m exists" Gen Property
prop_negative_exponent_good
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"e < 0 && gcd a m > 1 => a^e mod m does not exist" Gen Property
prop_negative_exponent_bad
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"e < 0 && gcd a m == 1 => (a^e mod m) * (a^(-e) mod m) = 1 mod m" Gen Property
prop_negated_exponent_inverse
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"(ab)^e mod m == (a^e * b^e) mod m" Gen Property
prop_multiplicative
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"a^(e+e') mod m == (a^e * a^e') mod m" Gen Property
prop_exponent_additive
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"(a+k*m)^e mod m == a^e mod m for all k" Gen Property
prop_periodic
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"Power exists" Gen Property
prop_power_exists
    , TestName -> Gen Property -> TestTree
forall prop. Testable prop => TestName -> prop -> TestTree
testProp TestName
"Power does not exist" Gen Property
prop_power_does_not_exist
    ]