Kwxm/test/extra integer property tests

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

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

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
 
 

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

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)

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