diff --git a/plutus-core/plutus-core.cabal b/plutus-core/plutus-core.cabal index ee0ade59b73..51cf096b080 100644 --- a/plutus-core/plutus-core.cabal +++ b/plutus-core/plutus-core.cabal @@ -449,7 +449,12 @@ library untyped-plutus-core-testlib Evaluation.Builtins.Conversion Evaluation.Builtins.Costing Evaluation.Builtins.Definition - Evaluation.Builtins.Integer.ExpModInteger + Evaluation.Builtins.Integer.Common + Evaluation.Builtins.Integer.DivModProperties + Evaluation.Builtins.Integer.ExpModIntegerProperties + Evaluation.Builtins.Integer.OrderProperties + Evaluation.Builtins.Integer.QuotRemProperties + Evaluation.Builtins.Integer.RingProperties Evaluation.Builtins.MakeRead Evaluation.Builtins.SignatureVerification Evaluation.Debug diff --git a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/Builtin.hs b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/Builtin.hs index 91968d09e34..3ee10b96526 100644 --- a/plutus-core/testlib/PlutusCore/Generators/QuickCheck/Builtin.hs +++ b/plutus-core/testlib/PlutusCore/Generators/QuickCheck/Builtin.hs @@ -278,7 +278,7 @@ instance ArbitraryBuiltin BLS12_381.Pairing.MlResult where -- the 'Arbitrary' class and the logic for handling elements from 'ArbitraryBuiltin'. newtype AsArbitraryBuiltin a = AsArbitraryBuiltin { unAsArbitraryBuiltin :: a - } deriving newtype (Show) + } deriving newtype (Show, Eq, Ord, Num) instance ArbitraryBuiltin a => Arbitrary (AsArbitraryBuiltin a) where arbitrary = coerce $ arbitraryBuiltin @a diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Common.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Common.hs index b21a89916f9..8407b2a1420 100644 --- a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Common.hs +++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Common.hs @@ -12,6 +12,7 @@ module Evaluation.Builtins.Common , typecheckEvaluateCek , typecheckEvaluateCekNoEmit , typecheckReadKnownCek + , PlcType , PlcTerm , UplcTerm , CekResult (..) @@ -21,6 +22,7 @@ module Evaluation.Builtins.Common , ok , fails , evalOkEq + , evalOkTrue , integer , bytestring , zero @@ -117,6 +119,7 @@ typecheckReadKnownCek semvar = -- TPLC/UPLC utilities +type PlcType = TPLC.Type TPLC.TyName TPLC.DefaultUni () type PlcTerm = TPLC.Term TPLC.TyName TPLC.Name TPLC.DefaultUni TPLC.DefaultFun () type PlcError = TPLC.Error TPLC.DefaultUni TPLC.DefaultFun () type UplcTerm = UPLC.Term TPLC.Name TPLC.DefaultUni TPLC.DefaultFun () @@ -187,5 +190,7 @@ evalOkEq t1 t2 = r@(CekSuccess _) -> r === evalTerm t2 _ -> property False +evalOkTrue :: PlcTerm -> Property +evalOkTrue t = evalOkEq t true diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Definition.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Definition.hs index 691c57a9dcd..01ef4f2765e 100644 --- a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Definition.hs +++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Definition.hs @@ -24,7 +24,11 @@ import Evaluation.Builtins.BLS12_381 (test_BLS12_381) import Evaluation.Builtins.Common (typecheckAnd, typecheckEvaluateCek, typecheckEvaluateCekNoEmit, typecheckReadKnownCek) import Evaluation.Builtins.Conversion qualified as Conversion -import Evaluation.Builtins.Integer.ExpModInteger (test_expModInteger_properties) +import Evaluation.Builtins.Integer.DivModProperties (test_integer_div_mod_properties) +import Evaluation.Builtins.Integer.ExpModIntegerProperties (test_integer_exp_mod_properties) +import Evaluation.Builtins.Integer.OrderProperties (test_integer_order_properties) +import Evaluation.Builtins.Integer.QuotRemProperties (test_integer_quot_rem_properties) +import Evaluation.Builtins.Integer.RingProperties (test_integer_ring_properties) import Evaluation.Builtins.SignatureVerification (ecdsaSecp256k1Prop, ed25519_VariantAProp, ed25519_VariantBProp, ed25519_VariantCProp, schnorrSecp256k1Prop) @@ -1215,6 +1219,17 @@ test_Bitwise_CIP0123 = ] ] +test_integer_properties :: TestTree +test_integer_properties = + testGroup "test_integer_properties" + [ test_integer_ring_properties + , test_integer_div_mod_properties + , test_integer_quot_rem_properties + , test_integer_order_properties + , test_integer_ring_properties + , test_integer_exp_mod_properties + ] + test_definition :: TestTree test_definition = testGroup "definition" @@ -1251,7 +1266,7 @@ test_definition = , test_HashSizes , test_SignatureVerification , test_BLS12_381 - , test_expModInteger_properties + , test_integer_properties , test_Other , test_Version , test_ConsByteString diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/Common.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/Common.hs new file mode 100644 index 00000000000..a94e5a3d7fe --- /dev/null +++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/Common.hs @@ -0,0 +1,98 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +module Evaluation.Builtins.Integer.Common +where + +import Prelude hiding (and, not, or) + +import PlutusCore qualified as PLC +import PlutusCore.Generators.QuickCheck.Builtin (AsArbitraryBuiltin (..)) +import PlutusCore.MkPlc (builtin, mkIterAppNoAnn, mkTyBuiltin, tyInst) + +import Evaluation.Builtins.Common + +import Test.QuickCheck (Gen, arbitrary) + +-- For property tests, we don't want to use the standard QuickCheck generator +-- for Integers because that only produces values in [-99..99]. Here are some +-- utilities to make it easier to use the better generator for +-- AsArbitraryBuiltin Integer. +type BigInteger = AsArbitraryBuiltin Integer + +biginteger :: BigInteger -> PlcTerm +biginteger (AsArbitraryBuiltin n) = integer n + +arbitraryBigInteger :: Gen Integer +arbitraryBigInteger = unAsArbitraryBuiltin <$> arbitrary + +-- Functions creating terms that are applications of various builtins, for +-- convenience. + +addInteger :: PlcTerm -> PlcTerm -> PlcTerm +addInteger a b = mkIterAppNoAnn (builtin () PLC.AddInteger) [a, b] + +subtractInteger :: PlcTerm -> PlcTerm -> PlcTerm +subtractInteger a b = mkIterAppNoAnn (builtin () PLC.SubtractInteger) [a, b] + +divideInteger :: PlcTerm -> PlcTerm -> PlcTerm +divideInteger a b = mkIterAppNoAnn (builtin () PLC.DivideInteger) [a, b] + +modInteger :: PlcTerm -> PlcTerm -> PlcTerm +modInteger a b = mkIterAppNoAnn (builtin () PLC.ModInteger) [a, b] + +multiplyInteger :: PlcTerm -> PlcTerm -> PlcTerm +multiplyInteger a b = mkIterAppNoAnn (builtin () PLC.MultiplyInteger) [a, b] + +quotientInteger :: PlcTerm -> PlcTerm -> PlcTerm +quotientInteger a b = mkIterAppNoAnn (builtin () PLC.QuotientInteger) [a, b] + +remainderInteger :: PlcTerm -> PlcTerm -> PlcTerm +remainderInteger a b = mkIterAppNoAnn (builtin () PLC.RemainderInteger) [a, b] + +equalsInteger :: PlcTerm -> PlcTerm -> PlcTerm +equalsInteger a b = mkIterAppNoAnn (builtin () PLC.EqualsInteger) [a, b] + +lessThanInteger :: PlcTerm -> PlcTerm -> PlcTerm +lessThanInteger a b = mkIterAppNoAnn (builtin () PLC.LessThanInteger) [a, b] + +lessThanEqualsInteger :: PlcTerm -> PlcTerm -> PlcTerm +lessThanEqualsInteger a b = mkIterAppNoAnn (builtin () PLC.LessThanEqualsInteger) [a, b] + +le0 :: PlcTerm -> PlcTerm +le0 t = lessThanEqualsInteger t zero + +ge0 :: PlcTerm -> PlcTerm +ge0 t = lessThanEqualsInteger zero t + +ite + :: forall a + . PLC.DefaultUni `PLC.HasTypeLevel` a + => PlcTerm -> PlcTerm -> PlcTerm -> PlcTerm +ite b t f = + let ty = mkTyBuiltin @_ @a () + iteInst = tyInst () (builtin () PLC.IfThenElse) ty + in mkIterAppNoAnn iteInst [b, t, f] + +-- Various logical combinations of boolean terms. + +abs :: PlcTerm -> PlcTerm +abs t = ite @Integer (lessThanEqualsInteger zero t) t (subtractInteger zero t) + +not :: PlcTerm -> PlcTerm +not t = ite @Bool t false true + +and :: PlcTerm -> PlcTerm -> PlcTerm +and t1 t2 = ite @Bool t1 (ite @Bool t2 true false) false + +or :: PlcTerm -> PlcTerm -> PlcTerm +or t1 t2 = ite @Bool t1 true (ite @Bool t2 true false) + +xor :: PlcTerm -> PlcTerm -> PlcTerm +xor t1 t2 = ite @Bool t1 (ite @Bool t2 false true) t2 + +implies :: PlcTerm -> PlcTerm -> PlcTerm +implies t1 t2 = (not t1) `or` t2 + +iff :: PlcTerm -> PlcTerm -> PlcTerm +iff t1 t2 = (t1 `implies` t2) `and` (t2 `implies` t1) diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/DivModProperties.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/DivModProperties.hs new file mode 100644 index 00000000000..2e3461f5d33 --- /dev/null +++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/DivModProperties.hs @@ -0,0 +1,134 @@ +-- editorconfig-checker-disable +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ViewPatterns #-} + +{- | Property tests for the `divideInteger` and `modInteger` builtins -} +module Evaluation.Builtins.Integer.DivModProperties (test_integer_div_mod_properties) +where + +import Evaluation.Builtins.Common +import Evaluation.Builtins.Integer.Common + +import Test.Tasty (TestName, TestTree, testGroup) +import Test.Tasty.QuickCheck + +numberOfTests :: Int +numberOfTests = 200 + +testProp :: Testable prop => TestName -> prop -> TestTree +testProp s p = testProperty s $ withMaxSuccess numberOfTests p + +-- `divideInteger _ 0` always fails. +prop_div_0_fails :: BigInteger -> Property +prop_div_0_fails (biginteger -> a) = + fails $ divideInteger a zero + +-- `modInteger _ 0` always fails. +prop_mod_0_fails :: BigInteger -> Property +prop_mod_0_fails (biginteger -> a) = + fails $ modInteger a zero + +-- b /= 0 => a = b * (a `div` b) + (a `mod` b) +-- This is the crucial property relating `divideInteger` and `modInteger`. +prop_div_mod_compatible :: BigInteger -> NonZero BigInteger -> Property +prop_div_mod_compatible (biginteger -> a) (NonZero (biginteger -> b)) = + let t = addInteger (multiplyInteger b (divideInteger a b) ) (modInteger a b) + in evalOkEq t a + +-- (k*b) `div` b = b and (k*b) `mod` b = 0 for all k +prop_div_mod_multiple :: BigInteger -> NonZero BigInteger -> Property +prop_div_mod_multiple (biginteger -> k) (NonZero (biginteger -> b)) = + let t1 = divideInteger (multiplyInteger k b) b + t2 = modInteger (multiplyInteger k b) b + in evalOkEq t1 k .&&. evalOkEq t2 zero + +-- For fixed b, `modInteger _ b` is an additive homomorphism: +-- (a+a') `mod` b = ((a `mod` b) + (a' `mod` b)) `mod` b +-- Together with prop_div_mod_multiple this means that `mod _ b` is +-- periodic: (a+k*b) `mod` b = a mod b` for all k. +prop_mod_additive :: BigInteger -> BigInteger -> NonZero BigInteger -> Property +prop_mod_additive (biginteger -> a) (biginteger -> a') (NonZero (biginteger -> b)) = + let t1 = modInteger (addInteger a a') b + t2 = modInteger (addInteger (modInteger a b) (modInteger a' b)) b + in evalOkEq t1 t2 + +-- For fixed b, `modInteger _ b` is a multiplicative homomorphism: +-- (a*a') `mod` b = ((a `mod` b) * (a' `mod` b)) `mod` b +prop_mod_multiplicative :: BigInteger -> BigInteger -> NonZero BigInteger -> Property +prop_mod_multiplicative (biginteger -> a) (biginteger -> a') (NonZero (biginteger -> b)) = + let t1 = modInteger (multiplyInteger a a') b + t2 = modInteger (multiplyInteger (modInteger a b) (modInteger a' b)) b + in evalOkEq t1 t2 + +-- For b > 0, 0 <= a `mod` b < b; +prop_mod_size_pos :: BigInteger -> Positive BigInteger -> Property +prop_mod_size_pos (biginteger -> a) (Positive (biginteger -> b)) = + let t1 = lessThanEqualsInteger zero (modInteger a b) + t2 = lessThanInteger (modInteger a b) b + in evalOkTrue t1 .&&. evalOkTrue t2 + +-- For b < 0, b < a `mod` b <= 0 +prop_mod_size_neg :: BigInteger -> Negative BigInteger -> Property +prop_mod_size_neg (biginteger -> a) (Negative (biginteger -> b)) = + let t1 = lessThanEqualsInteger (modInteger a b) zero + t2 = lessThanInteger b (modInteger a b) + in evalOkTrue t1 .&&. evalOkTrue t2 + +-- a >= 0 && b > 0 => a `div` b >= 0 and a `mod` b >= 0 +-- a <= 0 && b > 0 => a `div` b <= 0 and a `mod` b >= 0 +-- a >= 0 && b < 0 => a `div` b <= 0 and a `mod` b <= 0 +-- a < 0 && b < 0 => a `div` b >= 0 and a `mod` b <= 0 + +prop_div_pos_pos :: (NonNegative BigInteger) -> (Positive BigInteger) -> Property +prop_div_pos_pos (NonNegative (biginteger -> a)) (Positive (biginteger -> b)) = + evalOkTrue $ ge0 (divideInteger a b) + +prop_div_neg_pos :: (NonPositive BigInteger) -> (Positive BigInteger) -> Property +prop_div_neg_pos (NonPositive (biginteger -> a)) (Positive (biginteger -> b)) = + evalOkTrue $ le0 (divideInteger a b) + +prop_div_pos_neg :: (NonNegative BigInteger) -> (Negative BigInteger) -> Property +prop_div_pos_neg (NonNegative (biginteger -> a)) (Negative (biginteger -> b)) = + evalOkTrue $ le0 (divideInteger a b) + +prop_div_neg_neg :: (NonPositive BigInteger) -> (Negative BigInteger) -> Property +prop_div_neg_neg (NonPositive (biginteger -> a)) (Negative (biginteger -> b)) = + evalOkTrue $ ge0 (divideInteger a b) + +prop_mod_pos_pos :: (NonNegative BigInteger) -> (Positive BigInteger) -> Property +prop_mod_pos_pos (NonNegative (biginteger -> a)) (Positive (biginteger -> b)) = + evalOkTrue $ ge0 (modInteger a b) + +prop_mod_neg_pos :: (NonPositive BigInteger) -> (Positive BigInteger) -> Property +prop_mod_neg_pos (NonPositive (biginteger -> a)) (Positive (biginteger -> b)) = + evalOkTrue $ ge0 (modInteger a b) + +prop_mod_pos_neg :: (NonNegative BigInteger) -> (Negative BigInteger) -> Property +prop_mod_pos_neg (NonNegative (biginteger -> a)) (Negative (biginteger -> b)) = + evalOkTrue $ le0 (modInteger a b) + +prop_mod_neg_neg :: (NonPositive BigInteger) -> (Negative BigInteger) -> Property +prop_mod_neg_neg (NonPositive (biginteger -> a)) (Negative (biginteger -> b)) = + evalOkTrue $ le0 (modInteger a b) + +test_integer_div_mod_properties :: TestTree +test_integer_div_mod_properties = + testGroup "Property tests for divideInteger and modInteger" + [ testProp "divideInteger _ 0 always fails" prop_div_0_fails + , testProp "modInteger _ 0 always fails" prop_mod_0_fails + , testProp "divideInteger and modInteger are compatible" prop_div_mod_compatible + , testProp "divideInteger and modInteger behave sensibly on multiples of the divisor" prop_div_mod_multiple + , testProp "mod is an additive homomorphism" prop_mod_additive + , testProp "mod is a multiplicative homomorphism" prop_mod_multiplicative + , testProp "modInteger size is correct for positive modulus" prop_mod_size_pos + , testProp "modInteger size is correct for negative modulus" prop_mod_size_neg + , testProp "divideInteger (>= 0) (> 0) >= 0" prop_div_pos_pos + , testProp "divideInteger (<= 0) (> 0) <= 0" prop_div_neg_pos + , testProp "divideInteger (>= 0) (< 0) <= 0" prop_div_pos_neg + , testProp "divideInteger (<= 0) (< 0) >= 0" prop_div_neg_neg + , testProp "modInteger (>= 0) (> 0) >= 0 " prop_mod_pos_pos + , testProp "modInteger (>= 0) (< 0) >= 0" prop_mod_neg_pos + , testProp "modInteger (<= 0) (> 0) <= 0" prop_mod_pos_neg + , testProp "modInteger (<= 0) (< 0) <= 0" prop_mod_neg_neg + ] + diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/ExpModInteger.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/ExpModInteger.hs deleted file mode 100644 index 25818e3a514..00000000000 --- a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/ExpModInteger.hs +++ /dev/null @@ -1,230 +0,0 @@ --- 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 = withMaxSuccess 250 - -mkExpMod :: Integer -> Integer -> Integer -> PlcTerm -mkExpMod a e m = - let a' = integer a - e' = integer e - m' = integer m - in mkIterAppNoAnn (builtin () PLC.ExpModInteger) [a',e',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 a e m = - e>=0 || (e < 0 && gcd a m == 1) - --- expModInteger a e m always fails if m<=0 -test_bad_modulus :: TestTree -test_bad_modulus = - testProperty - "modulus <= 0 -> error" . - withNTests $ do - a <- arbitrary - e <- arbitrary - m <- arbitrary `suchThat` (<=0) - let t = mkExpMod a e m - pure $ fails t - --- expModInteger a e 1 = 0 for all b and e -test_modulus_one :: TestTree -test_modulus_one = - testProperty - "a^e mod 1 == 0 for all a and e" . - withNTests $ do - a <- arbitrary - e <- arbitrary - let t = mkExpMod a e 1 - pure $ evalOkEq t zero - --- Test that expModInteger a e m always lies between 0 and m-1 (inclusive) -test_in_range :: TestTree -test_in_range = - testProperty - "Result lies between 0 and m-1" . - withNTests $ do - m <- arbitrary `suchThat` (>=1) - e <- arbitrary - a <- arbitrary `suchThat` (\a -> powerExists a e m) - let t = mkExpMod a e m - lb = mkApp2 PLC.LessThanEqualsInteger (integer 0) t - ub = mkApp2 PLC.LessThanEqualsInteger t (mkApp2 PLC.SubtractInteger (integer m) (integer 1)) - pure $ (evalOkEq lb true) .&&. (evalOkEq ub true) - --- For m>1, a^0 = 1 (equals 1, not congruent to 1) -test_power_zero :: TestTree -test_power_zero = - testProperty - "a^0 mod m == 1" . - withNTests $ do - a <- arbitrary - m <- arbitrary `suchThat` (>1) - let t = mkExpMod a 0 m - pure $ evalOkEq t one - --- For m>=1, expModInteger a 1 m = a (mod m) for all a -test_power_one :: TestTree -test_power_one = - testProperty - "a^1 mod m == a mod m" . - withNTests $ do - a <- arbitrary - m <- arbitrary `suchThat` (>=1) - let t1 = mkExpMod a 1 m - t2 = mkApp2 PLC.ModInteger (mkConstant () a) (mkConstant () m) - pure $ evalOkEq t1 t2 - --- For m >= 1 and e>=0, expModInteger a e m exists for all a -test_positive_exponent :: TestTree -test_positive_exponent = - testProperty - "e >= 0 => a^e mod m exists" . - withNTests $ do - e <- arbitrary `suchThat` (>=0) - m <- arbitrary `suchThat` (>=1) - a <- arbitrary - let t = mkExpMod a e m - pure $ ok 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 = - testProperty - "e < 0 && gcd a m == 1 => a^e mod m exists" . - withNTests $ do - m <- arbitrary `suchThat` (>1) - a <- arbitrary `suchThat` (\a -> gcd a m == 1) - e <- arbitrary `suchThat` (<0) - let t = mkExpMod a e m - pure $ ok 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 = - testProperty - "e < 0 && gcd a m > 1 => a^e mod m does not exist" . - withNTests $ do - m <- arbitrary `suchThat` (>1) - a <- arbitrary `suchThat` (\a -> gcd a m /= 1) - e <- arbitrary `suchThat` (<0) - let t = mkExpMod a e m - pure $ fails 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 = - testProperty - "e < 0 && gcd a m == 1 => (a^e mod m) * (a^(-e) mod m) = 1 mod m" . - withNTests $ do - m <- arbitrary `suchThat` (>1) - a <- arbitrary `suchThat` (\a -> gcd a m == 1) - e <- arbitrary -- Positive or negative - let t1 = mkExpMod a e m - t2 = mkExpMod a (-e) m - t = mkApp2 PLC.ModInteger (mkApp2 PLC.MultiplyInteger t1 t2) (mkConstant () m) - pure $ evalOkEq t one -- For m=1 this would zero. - --- (ab)^e mod m = a^e * b^e mod m -test_multiplicative :: TestTree -test_multiplicative = - testProperty - "(ab)^e mod m == (a^e * b^e) mod m" . - withNTests $ do - m <- arbitrary `suchThat` (>1) - e <- arbitrary - a <- arbitrary `suchThat` (\a -> powerExists a e m) - b <- arbitrary `suchThat` (\b -> powerExists b e m) - let t1 = mkExpMod (a*b) e m - t2 = mkApp2 PLC.ModInteger (mkApp2 PLC.MultiplyInteger (mkExpMod a e m) (mkExpMod b e m)) (integer m) - pure $ evalOkEq t1 t2 - --- a^(e+e') = a^e*a^e' whenever both powers exist -test_exponent_additive :: TestTree -test_exponent_additive = - testProperty - "a^(e+e') mod m == (a^e * a^e') mod m" . - withNTests $ do - e <- arbitrary - f <- arbitrary - m <- arbitrary `suchThat` (>1) - a <- arbitrary `suchThat` (\a -> powerExists a e m && powerExists a f m) - let t1 = mkExpMod a (e+f) m - t2 = mkApp2 PLC.ModInteger (mkApp2 PLC.MultiplyInteger (mkExpMod a e m) (mkExpMod a f m)) (integer m) - pure $ evalOkEq t1 t2 - --- a^e mod m is the same for all members of a particular congruence class. -test_periodic :: TestTree -test_periodic = - testProperty - "(a+k*m)^e mod m == a^e mod m for all k" . - withNTests $ do - m <- arbitrary `suchThat` (>1) - e <- arbitrary - k <- arbitrary - a <- arbitrary `suchThat` (\a -> powerExists a e m) - let t1 = mkExpMod a e m - t2 = mkExpMod (a+k*m) e m - pure $ evalOkEq t1 t2 - --- Test that a power exists when it should. This overlaps with some of the --- earlier tests. -test_power_exists :: TestTree -test_power_exists = - testProperty - "Power exists" . - withNTests $ do - m <- arbitrary `suchThat` (>1) - e <- arbitrary - a <- arbitrary `suchThat` (\a -> powerExists a e m) - let t = mkExpMod a e m - pure $ ok 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 = - testProperty - "Power does not exist" . - withNTests $ do - m <- arbitrary `suchThat` (>1) - e <- arbitrary - a <- arbitrary - let t = mkExpMod a e m - pure $ not (powerExists a e m) ==> fails t - -test_expModInteger_properties :: TestTree -test_expModInteger_properties = - testGroup "expModInteger properties" - [ test_bad_modulus - , test_modulus_one - , test_in_range - , test_power_zero - , test_power_one - , test_positive_exponent - , test_negative_exponent_good - , test_negative_exponent_bad - , test_negated_exponent_inverse - , test_multiplicative - , test_exponent_additive - , test_periodic - , test_power_exists - , test_power_does_not_exist - ] diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/ExpModIntegerProperties.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/ExpModIntegerProperties.hs new file mode 100644 index 00000000000..ddd347bca73 --- /dev/null +++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/ExpModIntegerProperties.hs @@ -0,0 +1,188 @@ +-- 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 = 400 + +testProp :: Testable prop => TestName -> prop -> TestTree +testProp s p = testProperty s $ withMaxSuccess numberOfTests p + +expModInteger :: Integer -> Integer -> Integer -> PlcTerm +expModInteger (integer -> a) (integer -> e) (integer -> m) = + mkIterAppNoAnn (builtin () PLC.ExpModInteger) [a, e ,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 a e m = + e>=0 || (e < 0 && gcd a m == 1) + +-- expModInteger a e m always fails if m<=0 +prop_bad_modulus :: Gen Property +prop_bad_modulus = do + a <- arbitraryBigInteger + e <- arbitraryBigInteger + m <- arbitraryBigInteger `suchThat` (<=0) + let t = expModInteger a e m + pure $ fails t + +-- expModInteger a e 1 = 0 for all b and e +prop_modulus_one :: Gen Property +prop_modulus_one = do + a <- arbitraryBigInteger + e <- arbitraryBigInteger + let t = expModInteger a e 1 + pure $ evalOkEq t zero + +-- Test that expModInteger a e m always lies between 0 and m-1 (inclusive) +prop_in_range :: Gen Property +prop_in_range = do + m <- arbitraryBigInteger `suchThat` (>=1) + e <- arbitraryBigInteger + a <- arbitraryBigInteger `suchThat` (\a -> powerExists a e m) + let t = expModInteger a e m + lb = mkApp2 PLC.LessThanEqualsInteger (integer 0) t + ub = mkApp2 PLC.LessThanEqualsInteger t (mkApp2 PLC.SubtractInteger (integer m) (integer 1)) + pure $ evalOkTrue lb .&&. evalOkTrue ub + +-- For m > 1, a^0 = 1 (equals 1, not congruent to 1) +prop_power_zero :: Gen Property +prop_power_zero = do + a <- arbitraryBigInteger + m <- arbitraryBigInteger `suchThat` (>1) + let t = expModInteger a 0 m + pure $ evalOkEq t one + +-- For m >= 1, expModInteger a 1 m = a (mod m) for all a +prop_power_one :: Gen Property +prop_power_one = do + a <- arbitraryBigInteger + m <- arbitraryBigInteger `suchThat` (>=1) + let t1 = expModInteger a 1 m + t2 = mkApp2 PLC.ModInteger (mkConstant () a) (mkConstant () m) + pure $ evalOkEq t1 t2 + +-- For m >= 1 and e >= 0, expModInteger a e m exists for all a +prop_positive_exponent :: Gen Property +prop_positive_exponent = do + e <- arbitraryBigInteger `suchThat` (>=0) + m <- arbitraryBigInteger `suchThat` (>=1) + a <- arbitraryBigInteger + let t = expModInteger a e m + pure $ ok 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 = do + m <- arbitraryBigInteger `suchThat` (>1) + a <- arbitraryBigInteger `suchThat` (\a -> gcd a m == 1) + e <- arbitraryBigInteger `suchThat` (<0) + let t = expModInteger a e m + pure $ ok 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 = do + m <- arbitraryBigInteger `suchThat` (>1) + a <- arbitraryBigInteger `suchThat` (\a -> gcd a m /= 1) + e <- arbitraryBigInteger `suchThat` (<0) + let t = expModInteger a e m + pure $ fails 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 = do + m <- arbitraryBigInteger `suchThat` (>1) + a <- arbitraryBigInteger `suchThat` (\a -> gcd a m == 1) + e <- arbitraryBigInteger -- Positive or negative + let t1 = expModInteger a e m + t2 = expModInteger a (-e) m + t = mkApp2 PLC.ModInteger (mkApp2 PLC.MultiplyInteger t1 t2) (mkConstant () m) + pure $ evalOkEq t one -- For m=1 this would be zero. + +-- (ab)^e mod m = a^e * b^e mod m +prop_multiplicative :: Gen Property +prop_multiplicative = do + m <- arbitraryBigInteger `suchThat` (>1) + e <- arbitraryBigInteger + a <- arbitraryBigInteger `suchThat` (\a -> powerExists a e m) + b <- arbitraryBigInteger `suchThat` (\b -> powerExists b e m) + let t1 = expModInteger (a*b) e m + t2 = mkApp2 PLC.ModInteger (mkApp2 PLC.MultiplyInteger (expModInteger a e m) (expModInteger b e m)) (integer m) + pure $ evalOkEq t1 t2 + +-- a^(e+e') = a^e*a^e' whenever both powers exist +prop_exponent_additive :: Gen Property +prop_exponent_additive = do + e <- arbitraryBigInteger + f <- arbitraryBigInteger + m <- arbitraryBigInteger `suchThat` (>1) + a <- arbitraryBigInteger `suchThat` (\a -> powerExists a e m && powerExists a f m) + let t1 = expModInteger a (e+f) m + t2 = mkApp2 PLC.ModInteger (mkApp2 PLC.MultiplyInteger (expModInteger a e m) (expModInteger a f m)) (integer m) + pure $ evalOkEq t1 t2 + +-- a^e mod m is the same for all members of a particular congruence class. +prop_periodic :: Gen Property +prop_periodic = do + m <- arbitraryBigInteger `suchThat` (>1) + e <- arbitraryBigInteger + k <- arbitraryBigInteger + a <- arbitraryBigInteger `suchThat` (\a -> powerExists a e m) + let t1 = expModInteger a e m + t2 = expModInteger (a+k*m) e m + pure $ evalOkEq t1 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 = do + m <- arbitraryBigInteger `suchThat` (>1) + e <- arbitraryBigInteger + a <- arbitraryBigInteger `suchThat` (\a -> powerExists a e m) + let t = expModInteger a e m + pure $ ok 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 = do + m <- arbitraryBigInteger `suchThat` (>1) + e <- arbitraryBigInteger + a <- arbitraryBigInteger + let t = expModInteger a e m + pure $ not (powerExists a e m) ==> fails t + +test_integer_exp_mod_properties :: TestTree +test_integer_exp_mod_properties = + testGroup "Property tests for expModInteger" + [ testProp "modulus <= 0 -> error" prop_bad_modulus + , testProp "a^e mod 1 == 0 for all a and e" prop_modulus_one + , testProp "Result lies between 0 and m-1" prop_in_range + , testProp "a^0 mod m == 1" prop_power_zero + , testProp "a^1 mod m == a mod m" prop_power_one + , testProp "e >= 0 => a^e mod m exists" prop_positive_exponent + , testProp "e < 0 && gcd a m == 1 => a^e mod m exists" prop_negative_exponent_good + , testProp "e < 0 && gcd a m > 1 => a^e mod m does not exist" prop_negative_exponent_bad + , testProp "e < 0 && gcd a m == 1 => (a^e mod m) * (a^(-e) mod m) = 1 mod m" prop_negated_exponent_inverse + , testProp "(ab)^e mod m == (a^e * b^e) mod m" prop_multiplicative + , testProp "a^(e+e') mod m == (a^e * a^e') mod m" prop_exponent_additive + , testProp "(a+k*m)^e mod m == a^e mod m for all k" prop_periodic + , testProp "Power exists" prop_power_exists + , testProp "Power does not exist" prop_power_does_not_exist + ] diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/OrderProperties.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/OrderProperties.hs new file mode 100644 index 00000000000..9736edf4ea5 --- /dev/null +++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/OrderProperties.hs @@ -0,0 +1,107 @@ +-- editorconfig-checker-disable +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ViewPatterns #-} + +{- | Property tests for the `lessThanInteger` and `lessThanEqualsInteger` builtins + and their interaction with the arithmetic functions. -} +module Evaluation.Builtins.Integer.OrderProperties (test_integer_order_properties) +where + +import Prelude hiding (and, not, or) + +import Evaluation.Builtins.Common +import Evaluation.Builtins.Integer.Common + +import Test.Tasty (TestName, TestTree, testGroup) +import Test.Tasty.QuickCheck + +numberOfTests :: Int +numberOfTests = 200 + +testProp :: Testable prop => TestName -> prop -> TestTree +testProp s p = testProperty s $ withMaxSuccess numberOfTests p + +{- Tests for standard properties of order relations. In most of these we create + totally random inputs and then create terms checking that the expected + properties are satisfied. The inputs are completely random, so in some cases + we'll be checking vacuous implications (for example, in `add_pairs`, where + only one quarter of the cases will be checking the property that we really + want to check). Instead we could have used `suchThat` to generate inputs + that always satisified the preconditions and then created terms to check that + the conclusion holds. It's arguable which of these is better, but the way + it's done here exercises the comparison builtins more so perhaps increases + the probability of detecting unexpected behaviour. -} + +lte_reflexive :: BigInteger -> Property +lte_reflexive (biginteger -> a) = + evalOkTrue $ lessThanEqualsInteger a a + +lte_antisymmetric :: BigInteger -> BigInteger -> Property +lte_antisymmetric (biginteger -> a) (biginteger -> b) = + evalOkTrue $ + (lessThanEqualsInteger a b `and` lessThanEqualsInteger b a) + `implies` equalsInteger a b + +lte_transitive :: BigInteger -> BigInteger -> BigInteger -> Property +lte_transitive (biginteger -> a) (biginteger -> b) (biginteger -> c) = + evalOkTrue $ + (lessThanEqualsInteger a b `and` lessThanEqualsInteger b c) + `implies` lessThanEqualsInteger a c + +-- This implies that lessThanEqualsInteger is a total order. +trichotomy :: BigInteger -> BigInteger -> Property +trichotomy (biginteger -> a) (biginteger -> b) = + evalOkTrue $ + lessThanInteger a b `xor` equalsInteger a b `xor` lessThanInteger b a + +-- This establishes a connection between < and <=, allowing us to limit +-- ourselves to checking properties of <=. +lt_versus_lte :: BigInteger -> BigInteger -> Property +lt_versus_lte (biginteger -> a) (biginteger -> b) = + evalOkTrue $ + lessThanEqualsInteger a b `iff` (lessThanInteger a b `xor` equalsInteger a b) + +-- Tests of some relations between the comparison operators and the arithmetic +-- operators. + +-- Check that a <= b and c <= d => a+c <= b+d. In conjunction with the ring +-- properties this implies, for example, that the sum of two positive integers +-- is positive and the sum of two negative integers is negative, and that a <= +-- a+k for positive k. +add_pairs :: BigInteger -> BigInteger -> BigInteger -> BigInteger -> Property +add_pairs (biginteger -> a) (biginteger -> b) (biginteger -> c) (biginteger -> d) = + evalOkTrue $ + (lessThanEqualsInteger a b `and` lessThanEqualsInteger c d) + `implies` lessThanEqualsInteger (addInteger a c) (addInteger b d) + +-- Test that the signs of various types of product are correct. +mul_pos_pos :: NonNegative BigInteger -> NonNegative BigInteger -> Property +mul_pos_pos (NonNegative (biginteger -> a)) (NonNegative (biginteger -> b)) = + evalOkTrue $ lessThanEqualsInteger zero (multiplyInteger a b) + +mul_pos_neg :: NonNegative BigInteger -> NonPositive BigInteger -> Property +mul_pos_neg (NonNegative (biginteger -> a)) (NonPositive (biginteger -> b)) = + evalOkTrue $ lessThanEqualsInteger (multiplyInteger a b) zero + +mul_neg_pos :: NonPositive BigInteger -> NonNegative BigInteger -> Property +mul_neg_pos (NonPositive (biginteger -> a)) (NonNegative (biginteger -> b)) = + evalOkTrue $ lessThanEqualsInteger (multiplyInteger a b) zero + +mul_neg_neg :: NonPositive BigInteger -> NonPositive BigInteger -> Property +mul_neg_neg (NonPositive (biginteger -> a)) (NonPositive (biginteger -> b)) = + evalOkTrue $ lessThanEqualsInteger zero (multiplyInteger a b) + +test_integer_order_properties :: TestTree +test_integer_order_properties = + testGroup "Property tests involving integer ordering" + [ testProp "lessThanEqualsInteger is reflexive" lte_reflexive + , testProp "lessThanEqualsInteger is antisymmetric" lte_antisymmetric + , testProp "lessThanEqualsInteger is transitive" lte_transitive + , testProp "a <= b <=> a < b or a = b" lt_versus_lte + , testProp "a < b or a = b or b < a" trichotomy + , testProp "a <= b and c <= d => addInteger a c <= addInteger b d" add_pairs + , testProp "multiplyInteger (>= 0) (>= 0) >= 0" mul_pos_pos + , testProp "multiplyInteger (>= 0) (<= 0) <= 0" mul_pos_neg + , testProp "multiplyInteger (<= 0) (>= 0) <= 0" mul_neg_pos + , testProp "multiplyInteger (<= 0) (<= 0) >= 0" mul_neg_neg + ] diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/QuotRemProperties.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/QuotRemProperties.hs new file mode 100644 index 00000000000..187cf188b53 --- /dev/null +++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/QuotRemProperties.hs @@ -0,0 +1,147 @@ +-- editorconfig-checker-disable +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ViewPatterns #-} + +{- | Property tests for the `quotientInteger` and `remainderInteger` builtins -} +module Evaluation.Builtins.Integer.QuotRemProperties (test_integer_quot_rem_properties) +where + +import Prelude hiding (abs) + +import Evaluation.Builtins.Common +import Evaluation.Builtins.Integer.Common + +import Test.Tasty (TestName, TestTree, testGroup) +import Test.Tasty.QuickCheck + +numberOfTests :: Int +numberOfTests = 200 + +testProp :: Testable prop => TestName -> prop -> TestTree +testProp s p = testProperty s $ withMaxSuccess numberOfTests p + +-- `quotientInteger _ 0` always fails. +prop_quot_0_fails :: BigInteger -> Property +prop_quot_0_fails (biginteger -> a) = + fails $ quotientInteger a zero + +-- `remainderInteger _ 0` always fails. +prop_rem_0_fails :: BigInteger -> Property +prop_rem_0_fails (biginteger -> a) = + fails $ remainderInteger a zero + +-- b /= 0 => a = b * (a `quot` b) + (a `rem` b) +-- This is the crucial property relating `quotientInteger` and `remainderInteger`. +prop_quot_rem_compatible :: BigInteger -> NonZero BigInteger -> Property +prop_quot_rem_compatible (biginteger -> a) (NonZero (biginteger -> b)) = + let t = addInteger (multiplyInteger b (quotientInteger a b) ) (remainderInteger a b) + in evalOkEq t a + +-- (k*b) `quot` b = b and (k*b) `rem` b = 0 for all k +prop_quot_rem_multiple :: BigInteger -> NonZero BigInteger -> Property +prop_quot_rem_multiple (biginteger -> k) (NonZero (biginteger -> b)) = + let t1 = quotientInteger (multiplyInteger k b) b + t2 = remainderInteger (multiplyInteger k b) b + in evalOkEq t1 k .&&. evalOkEq t2 zero + +-- `remainderInteger _ b` is not an additive homomorphism in general (and hence +-- not periodic) because the sign of `remainderInteger a b` is different for +-- positive and negative a. For example (writing `rem` for short instead of +-- `remainderInteger`) `rem (-1) 5 = -1` and `rem 5 5 = 0` but `rem (-1+5) 5 = +-- 4`. However, rem (a + a') b = rem ((rem a b) + (rem a' b)) b if a and a' +-- have the same sign, so we test that instead of checking for arbitrary a and +-- a'. + +-- For fixed b, `remainderInteger _ b` is an additive homomorphism on non-negative integers +-- (a+a') `rem` b = ((a `rem` b) + (a' `rem` b)) `rem` b +prop_rem_additive_pos :: NonNegative BigInteger -> NonNegative BigInteger -> NonZero BigInteger -> Property +prop_rem_additive_pos (NonNegative (biginteger -> a)) (NonNegative (biginteger -> a')) (NonZero (biginteger -> b)) = + let t1 = remainderInteger (addInteger a a') b + t2 = remainderInteger (addInteger (remainderInteger a b) (remainderInteger a' b)) b + in evalOkEq t1 t2 + +-- For fixed b, `remainderInteger _ b` is an additive homomorphism on non-postive integers +-- (a+a') `rem` b = ((a `rem` b) + (a' `rem` b)) `rem` b +prop_rem_additive_neg :: NonPositive BigInteger -> NonPositive BigInteger -> NonZero BigInteger -> Property +prop_rem_additive_neg (NonPositive (biginteger -> a)) (NonPositive (biginteger -> a')) (NonZero (biginteger -> b)) = + let t1 = remainderInteger (addInteger a a') b + t2 = remainderInteger (addInteger (remainderInteger a b) (remainderInteger a' b)) b + in evalOkEq t1 t2 + +-- Somewhat unexpectedly, for fixed b, `remainderInteger _ b` is a +-- multiplicative homomorphism: : (a*a') `rem` b = ((a `rem` b) * (a' `rem` b)) +-- `rem` b +prop_rem_multiplicative :: BigInteger -> BigInteger -> NonZero BigInteger -> Property +prop_rem_multiplicative (biginteger -> a) (biginteger -> a') (NonZero (biginteger -> b)) = + let t1 = remainderInteger (multiplyInteger a a') b + t2 = remainderInteger (multiplyInteger (remainderInteger a b) (remainderInteger a' b)) b + in evalOkEq t1 t2 + +-- For a >= 0 and b > 0, 0 <= |a `rem` b| < |b| +-- The sign of the remainder is a bit tricky in this case. We test that the +-- absolute value of the remainder is in the expected range and leave the sign +-- to later tests. +prop_rem_size :: BigInteger -> NonZero BigInteger -> Property +prop_rem_size (biginteger -> a) (NonZero (biginteger -> b)) = + let r = abs (remainderInteger a b) + t1 = lessThanEqualsInteger zero r + t2 = lessThanInteger r (abs b) + in evalOkTrue t1 .&&. evalOkTrue t2 + +-- a >= 0 && b > 0 => a `quot` b >= 0 and a `rem` b >= 0 +-- a <= 0 && b > 0 => a `quot` b <= 0 and a `rem` b <= 0 +-- a >= 0 && b < 0 => a `quot` b <= 0 and a `rem` b >= 0 +-- a <= 0 && b < 0 => a `quot` b >= 0 and a `rem` b <= 0 + +prop_quot_pos_pos :: NonNegative BigInteger -> Positive BigInteger -> Property +prop_quot_pos_pos (NonNegative (biginteger -> a)) (Positive (biginteger -> b)) = + evalOkTrue $ ge0 (quotientInteger a b) + +prop_quot_neg_pos :: NonPositive BigInteger -> Positive BigInteger -> Property +prop_quot_neg_pos (NonPositive (biginteger -> a)) (Positive (biginteger -> b)) = + evalOkTrue $ le0 (quotientInteger a b) + +prop_quot_pos_neg :: NonNegative BigInteger -> Negative BigInteger -> Property +prop_quot_pos_neg (NonNegative (biginteger -> a)) (Negative (biginteger -> b)) = + evalOkTrue $ le0 (quotientInteger a b) + +prop_quot_neg_neg :: NonPositive BigInteger -> Negative BigInteger -> Property +prop_quot_neg_neg (NonPositive (biginteger -> a)) (Negative (biginteger -> b)) = + evalOkTrue $ ge0 (quotientInteger a b) + +prop_rem_pos_pos :: (NonNegative BigInteger) -> (Positive BigInteger) -> Property +prop_rem_pos_pos (NonNegative (biginteger -> a)) (Positive (biginteger -> b)) = + evalOkTrue $ ge0 (remainderInteger a b) + +prop_rem_neg_pos :: (NonPositive BigInteger) -> (Positive BigInteger) -> Property +prop_rem_neg_pos (NonPositive (biginteger -> a)) (Positive (biginteger -> b)) = + evalOkTrue $ le0 (remainderInteger a b) + +prop_rem_pos_neg :: (NonNegative BigInteger) -> (Negative BigInteger) -> Property +prop_rem_pos_neg (NonNegative (biginteger -> a)) (Negative (biginteger -> b)) = + evalOkTrue $ ge0 (remainderInteger a b) + +prop_rem_neg_neg :: (NonPositive BigInteger) -> (Negative BigInteger) -> Property +prop_rem_neg_neg (NonPositive (biginteger -> a)) (Negative (biginteger -> b)) = + evalOkTrue $ le0 (remainderInteger a b) + +test_integer_quot_rem_properties :: TestTree +test_integer_quot_rem_properties = + testGroup "Property tests for quotientInteger and remainderInteger" + [ testProp "quotientInteger _ 0 always fails" prop_quot_0_fails + , testProp "remainderInteger _ 0 always fails" prop_rem_0_fails + , testProp "quotientInteger and remainderInteger are compatible" prop_quot_rem_compatible + , testProp "quotientInteger and remainderInteger behave sensibly on multiples of the divisor" prop_quot_rem_multiple + , testProp "remainderInteger _ b is additive on non-negative inputs" prop_rem_additive_pos + , testProp "remainderInteger _ b is additive on non-positive inputs" prop_rem_additive_neg + , testProp "remainderInteger is a multiplicative homomorphism" prop_rem_multiplicative + , testProp "remainderInteger size correct" prop_rem_size + , testProp "quotientInteger (>= 0) (> 0) >= 0" prop_quot_pos_pos + , testProp "quotientInteger (<= 0) (> 0) <= 0" prop_quot_neg_pos + , testProp "quotientInteger (>= 0) (< 0) <= 0" prop_quot_pos_neg + , testProp "quotientInteger (<= 0) (< 0) >= 0" prop_quot_neg_neg + , testProp "remainderInteger (>= 0) (> 0) >= 0" prop_rem_pos_pos + , testProp "remainderInteger (<= 0) (> 0) <= 0" prop_rem_neg_pos + , testProp "remainderInteger (>= 0) (< 0) >= 0" prop_rem_pos_neg + , testProp "remainderInteger (<= 0) (< 0) <= 0" prop_rem_neg_neg + ] diff --git a/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/RingProperties.hs b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/RingProperties.hs new file mode 100644 index 00000000000..79e2255fc80 --- /dev/null +++ b/plutus-core/untyped-plutus-core/testlib/Evaluation/Builtins/Integer/RingProperties.hs @@ -0,0 +1,76 @@ +-- editorconfig-checker-disable +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} + +{- | Property tests for the `addInteger`, `subtractInteger`, and `multiplyInteger` builtins -} +module Evaluation.Builtins.Integer.RingProperties (test_integer_ring_properties) +where + +import Evaluation.Builtins.Common +import Evaluation.Builtins.Integer.Common + +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck + +-- a+(b+c) = (a+b)+c +prop_addition_associative :: BigInteger -> BigInteger -> BigInteger -> Property +prop_addition_associative (biginteger -> a) (biginteger -> b) (biginteger -> c) = + let t1 = addInteger a (addInteger b c) + t2 = addInteger (addInteger a b) c + in evalOkEq t1 t2 + +-- a+b = b+a +prop_addition_commutative :: BigInteger -> BigInteger -> Property +prop_addition_commutative (biginteger -> a) (biginteger -> b) = + evalOkEq (addInteger a b) (addInteger b a) + +-- a+0 = a +prop_zero_additive_identity :: BigInteger -> Property +prop_zero_additive_identity (biginteger -> a) = + evalOkEq (addInteger a zero) a + +-- (a+b)-b = a +prop_add_subtract_inverse :: BigInteger -> BigInteger -> Property +prop_add_subtract_inverse (biginteger -> a) (biginteger -> b) = + evalOkEq (subtractInteger (addInteger a b) b) a + +-- a*(b*c) = (a*b)*c +prop_multiplication_associative :: BigInteger -> BigInteger -> BigInteger -> Property +prop_multiplication_associative (biginteger -> a) (biginteger -> b) (biginteger -> c) = + let t1 = multiplyInteger a (multiplyInteger b c) + t2 = multiplyInteger (multiplyInteger a b) c + in evalOkEq t1 t2 + +-- a*b = b*a +prop_multiplication_commutative :: BigInteger -> BigInteger -> Property +prop_multiplication_commutative (biginteger -> a) (biginteger -> b) = + let t1 = multiplyInteger a b + t2 = multiplyInteger b a + in evalOkEq t1 t2 + +-- a*1 = a +prop_one_multiplicative_identity :: BigInteger -> Property +prop_one_multiplicative_identity (biginteger -> a) = + let t = multiplyInteger a one + in evalOkEq t a + +-- a*(b+c) = a*b + a*c +prop_distibutive :: BigInteger -> BigInteger -> BigInteger -> Property +prop_distibutive (biginteger -> a) (biginteger -> b) (biginteger -> c) = + let t1 = multiplyInteger a (addInteger b c) + t2 = addInteger (multiplyInteger a b) (multiplyInteger a c) + in evalOkEq t1 t2 + +test_integer_ring_properties :: TestTree +test_integer_ring_properties = + testGroup "Ring properties for integer arithmetic builtins" + [ testProperty "addInteger is associative" prop_addition_associative + , testProperty "addInteger is commutative" prop_addition_commutative + , testProperty "0 is an identity element for addInteger" prop_zero_additive_identity + , testProperty "subtraction is the inverse of addition" prop_add_subtract_inverse + , testProperty "multiplyInteger is associative" prop_multiplication_associative + , testProperty "multiplyInteger is commutative" prop_multiplication_commutative + , testProperty "1 is a multiplicative identity" prop_one_multiplicative_identity + , testProperty "multiplyInteger distributes over addInteger" prop_distibutive + ]