Add validity checks for IntSet and IntMap (#456)
authorMatt Renaud <matt@m-renaud.com>
Sat, 30 Dec 2017 17:08:11 +0000 (09:08 -0800)
committerGitHub <noreply@github.com>
Sat, 30 Dec 2017 17:08:11 +0000 (09:08 -0800)
These checks codify the invariants laid out in the IntSet and IntMap comments. We
add validity checks for constructed IntSets and IntMaps as well as union,
intersection, and difference operations on them.

* Add validity tests for functions producing IntSets/IntMaps.
* Add field comments for IntMap Bin constructor.
* Move validity checks into tests/.

Data/IntMap/Internal.hs
Data/IntSet/Internal.hs
containers.cabal
tests/IntMapValidity.hs [new file with mode: 0644]
tests/IntSetValidity.hs [new file with mode: 0644]
tests/intmap-properties.hs
tests/intset-properties.hs

index c0b7570..9767a96 100644 (file)
@@ -353,6 +353,15 @@ data IntMap a = Bin {-# UNPACK #-} !Prefix
                     {-# UNPACK #-} !Mask
                     !(IntMap a)
                     !(IntMap a)
+-- Fields:
+--   prefix: The most significant bits shared by all keys in this Bin.
+--   mask: The switching bit to determine if a key should follow the left
+--         or right subtree of a 'Bin'.
+-- Invariant: Nil is never found as a child of Bin.
+-- Invariant: Prefix is the common high-order bits that all elements share to
+--            the left of the Mask bit.
+-- Invariant: In Bin prefix mask left right, left consists of the elements that
+--            don't have the mask bit set; right is all the elements that do.
               | Tip {-# UNPACK #-} !Key a
               | Nil
 
index e0e6c5c..e8de60e 100644 (file)
@@ -180,6 +180,7 @@ module Data.IntSet.Internal (
     , suffixBitMask
     , prefixBitMask
     , bitmapOf
+    , zero
     ) where
 
 import Control.DeepSeq (NFData(rnf))
@@ -250,8 +251,8 @@ data IntSet = Bin {-# UNPACK #-} !Prefix {-# UNPACK #-} !Mask !IntSet !IntSet
 -- Invariant: In Bin prefix mask left right, left consists of the elements that
 --            don't have the mask bit set; right is all the elements that do.
             | Tip {-# UNPACK #-} !Prefix {-# UNPACK #-} !BitMap
--- Invariant: The Prefix is zero for all but the last 5 (on 32 bit arches) or 6
---            bits (on 64 bit arches). The values of the map represented by a tip
+-- Invariant: The Prefix is zero for the last 5 (on 32 bit arches) or 6 bits
+--            (on 64 bit arches). The values of the set represented by a tip
 --            are the prefix plus the indices of the set bits in the bit map.
             | Nil
 
@@ -323,7 +324,7 @@ size = go 0
 
 -- | /O(min(n,W))/. Is the value a member of the set?
 
--- See Note: Local 'go' functions and capturing]
+-- See Note: Local 'go' functions and capturing.
 member :: Key -> IntSet -> Bool
 member !x = go
   where
@@ -1250,6 +1251,7 @@ bitmapOf x = bitmapOfSuffix (suffixOf x)
 {--------------------------------------------------------------------
   Endian independent bit twiddling
 --------------------------------------------------------------------}
+-- Returns True iff the bits set in i and the Mask m are disjoint.
 zero :: Int -> Mask -> Bool
 zero i m
   = (natFromInt i) .&. (natFromInt m) == 0
index e28f196..19e670f 100644 (file)
@@ -371,6 +371,7 @@ Test-suite intmap-lazy-properties
         Data.IntMap.Lazy
         Data.IntSet
         Data.IntSet.Internal
+        IntMapValidity
         Utils.Containers.Internal.BitUtil
         Utils.Containers.Internal.StrictFold
         Utils.Containers.Internal.StrictPair
@@ -399,6 +400,7 @@ Test-suite intmap-strict-properties
         Data.IntMap.Strict
         Data.IntSet
         Data.IntSet.Internal
+        IntMapValidity
         Utils.Containers.Internal.BitUtil
         Utils.Containers.Internal.StrictFold
         Utils.Containers.Internal.StrictPair
@@ -425,6 +427,7 @@ Test-suite intset-properties
         Data.IntSet.Internal
         Data.Set
         Data.Set.Internal
+        IntSetValidity
         Utils.Containers.Internal.BitUtil
         Utils.Containers.Internal.PtrEquality
         Utils.Containers.Internal.StrictFold
diff --git a/tests/IntMapValidity.hs b/tests/IntMapValidity.hs
new file mode 100644 (file)
index 0000000..f33e128
--- /dev/null
@@ -0,0 +1,52 @@
+module IntMapValidity (valid) where
+
+import Data.Bits (xor, (.&.))
+import Data.IntMap.Internal
+import Test.QuickCheck (Property, counterexample, property, (.&&.))
+
+{--------------------------------------------------------------------
+  Assertions
+--------------------------------------------------------------------}
+-- | Returns true iff the internal structure of the IntMap is valid.
+valid :: IntMap a -> Property
+valid t =
+  counterexample "nilNeverChildOfBin" (nilNeverChildOfBin t) .&&.
+  counterexample "commonPrefix" (commonPrefix t) .&&.
+  counterexample "maskRespected" (maskRespected t)
+
+-- Invariant: Nil is never found as a child of Bin.
+nilNeverChildOfBin :: IntMap a  -> Bool
+nilNeverChildOfBin t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ _ l r -> noNilInSet l && noNilInSet r
+  where
+    noNilInSet t' =
+      case t' of
+        Nil -> False
+        Tip _ _ -> True
+        Bin _ _ l' r' -> noNilInSet l' && noNilInSet r'
+
+-- Invariant: Prefix is the common high-order bits that all elements share to
+--            the left of the Mask bit.
+commonPrefix :: IntMap a -> Bool
+commonPrefix t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    b@(Bin p _ _ _) -> all (sharedPrefix p) (keys b)
+  where
+    sharedPrefix :: Prefix -> Int -> Bool
+    sharedPrefix p a = 0 == (p `xor` (p .&. a))
+
+-- Invariant: In Bin prefix mask left right, left consists of the elements that
+--            don't have the mask bit set; right is all the elements that do.
+maskRespected :: IntMap a -> Bool
+maskRespected t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ binMask l r ->
+      all (\x -> zero x binMask) (keys l) &&
+      all (\x -> not (zero x binMask)) (keys r)
diff --git a/tests/IntSetValidity.hs b/tests/IntSetValidity.hs
new file mode 100644 (file)
index 0000000..3f8c2c2
--- /dev/null
@@ -0,0 +1,86 @@
+{-# LANGUAGE CPP #-}
+module IntSetValidity (valid) where
+
+import Data.Bits (xor, (.&.))
+import Data.IntSet.Internal
+import Test.QuickCheck (Property, counterexample, property, (.&&.))
+
+{--------------------------------------------------------------------
+  Assertions
+--------------------------------------------------------------------}
+-- | Returns true iff the internal structure of the IntSet is valid.
+valid :: IntSet -> Property
+valid t =
+  counterexample "nilNeverChildOfBin" (nilNeverChildOfBin t) .&&.
+  counterexample "maskPowerOfTwo" (maskPowerOfTwo t) .&&.
+  counterexample "commonPrefix" (commonPrefix t) .&&.
+  counterexample "markRespected" (maskRespected t) .&&.
+  counterexample "tipsValid" (tipsValid t)
+
+-- Invariant: Nil is never found as a child of Bin.
+nilNeverChildOfBin :: IntSet -> Bool
+nilNeverChildOfBin t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ _ l r -> noNilInSet l && noNilInSet r
+  where
+    noNilInSet t' =
+      case t' of
+        Nil -> False
+        Tip _ _ -> True
+        Bin _ _ l' r' -> noNilInSet l' && noNilInSet r'
+
+-- Invariant: The Mask is a power of 2.  It is the largest bit position at which
+--            two elements of the set differ.
+maskPowerOfTwo :: IntSet -> Bool
+maskPowerOfTwo t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ m l r ->
+      (m `mod` 2 == 0) && maskPowerOfTwo l && maskPowerOfTwo r
+
+-- Invariant: Prefix is the common high-order bits that all elements share to
+--            the left of the Mask bit.
+commonPrefix :: IntSet -> Bool
+commonPrefix t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    b@(Bin p _ _ _) -> all (sharedPrefix p) (elems b)
+  where
+    sharedPrefix :: Prefix -> Int -> Bool
+    sharedPrefix p a = 0 == (p `xor` (p .&. a))
+
+-- Invariant: In Bin prefix mask left right, left consists of the elements that
+--            don't have the mask bit set; right is all the elements that do.
+maskRespected :: IntSet -> Bool
+maskRespected t =
+  case t of
+    Nil -> True
+    Tip _ _ -> True
+    Bin _ binMask l r ->
+      all (\x -> zero x binMask) (elems l) &&
+      all (\x -> not (zero x binMask)) (elems r)
+
+-- Invariant: The Prefix is zero for the last 5 (on 32 bit arches) or 6 bits
+--            (on 64 bit arches). The values of the set represented by a tip
+--            are the prefix plus the indices of the set bits in the bit map.
+--
+-- Note: Valid entries stored in tip omitted.
+tipsValid :: IntSet -> Bool
+tipsValid t =
+  case t of
+    Nil -> True
+    tip@(Tip p b) -> validTipPrefix p
+    Bin _ _ l r -> tipsValid l && tipsValid r
+
+validTipPrefix :: Prefix -> Bool
+#if WORD_SIZE_IN_BITS==32
+-- Last 5 bits of the prefix must be zero for 32 bit arches.
+validTipPrefix p = (0x0000001F .&. p) == 0
+#else
+-- Last 6 bits of the prefix must be zero 64 bit anches.
+validTipPrefix p = (0x000000000000003F .&. p) == 0
+#endif
index 3875ec6..18c55e6 100644 (file)
@@ -6,6 +6,7 @@ import Data.IntMap.Strict as Data.IntMap hiding (showTree)
 import Data.IntMap.Lazy as Data.IntMap hiding (showTree)
 #endif
 import Data.IntMap.Internal.Debug (showTree)
+import IntMapValidity (valid)
 
 import Data.Monoid
 import Data.Maybe hiding (mapMaybe)
@@ -123,6 +124,8 @@ main = defaultMain
              , testCase "maxView" test_maxView
              , testCase "minViewWithKey" test_minViewWithKey
              , testCase "maxViewWithKey" test_maxViewWithKey
+             , testProperty "valid"                prop_valid
+             , testProperty "empty valid"          prop_emptyValid
              , testProperty "insert to singleton"  prop_singleton
              , testProperty "insert then lookup"   prop_insertLookup
              , testProperty "insert then delete"   prop_insertDelete
@@ -771,27 +774,56 @@ test_maxViewWithKey = do
     maxViewWithKey (empty :: SMap) @?= Nothing
 
 ----------------------------------------------------------------
+-- Valid IntMaps
+----------------------------------------------------------------
+
+forValid :: Testable b => (SMap -> b) -> Property
+forValid f = forAll arbitrary $ \t ->
+    classify (size t == 0) "empty" $
+    classify (size t > 0 && size t <= 10) "small" $
+    classify (size t > 10 && size t <= 64) "medium" $
+    classify (size t > 64) "large" $ f t
+
+forValidUnitTree :: Testable b => (SMap -> b) -> Property
+forValidUnitTree f = forValid f
+
+prop_valid :: Property
+prop_valid = forValidUnitTree $ \t -> valid t
+
+----------------------------------------------------------------
 -- QuickCheck
 ----------------------------------------------------------------
 
-prop_singleton :: Int -> Int -> Bool
-prop_singleton k x = insert k x empty == singleton k x
+prop_emptyValid :: Property
+prop_emptyValid = valid empty
+
+prop_singleton :: Int -> Int -> Property
+prop_singleton k x =
+  case singleton k x of
+    s ->
+      valid s .&&.
+      s === insert k x empty
 
 prop_insertLookup :: Int -> UMap -> Bool
 prop_insertLookup k t = lookup k (insert k () t) /= Nothing
 
 prop_insertDelete :: Int -> UMap -> Property
-prop_insertDelete k t = (lookup k t == Nothing) ==> (delete k (insert k () t) == t)
+prop_insertDelete k t =
+  lookup k t == Nothing ==>
+    case delete k (insert k () t) of
+      t' -> valid t' .&&. t' === t
 
 prop_deleteNonMember :: Int -> UMap -> Property
 prop_deleteNonMember k t = (lookup k t == Nothing) ==> (delete k t == t)
 
 ----------------------------------------------------------------
 
-prop_unionModel :: [(Int,Int)] -> [(Int,Int)] -> Bool
-prop_unionModel xs ys
-  = sort (keys (union (fromList xs) (fromList ys)))
-    == sort (nub (Prelude.map fst xs ++ Prelude.map fst ys))
+prop_unionModel :: [(Int,Int)] -> [(Int,Int)] -> Property
+prop_unionModel xs ys =
+  case union (fromList xs) (fromList ys) of
+    t ->
+      valid t .&&.
+      sort (keys t) === sort (nub (Prelude.map fst xs ++ Prelude.map fst ys))
 
 prop_unionSingleton :: IMap -> Int -> Int -> Bool
 prop_unionSingleton t k x = union (singleton k x) t == insert k x t
@@ -807,15 +839,23 @@ prop_unionSum xs ys
   = sum (elems (unionWith (+) (fromListWith (+) xs) (fromListWith (+) ys)))
     == (sum (Prelude.map snd xs) + sum (Prelude.map snd ys))
 
-prop_differenceModel :: [(Int,Int)] -> [(Int,Int)] -> Bool
-prop_differenceModel xs ys
-  = sort (keys (difference (fromListWith (+) xs) (fromListWith (+) ys)))
-    == sort ((List.\\) (nub (Prelude.map fst xs)) (nub (Prelude.map fst ys)))
-
-prop_intersectionModel :: [(Int,Int)] -> [(Int,Int)] -> Bool
-prop_intersectionModel xs ys
-  = sort (keys (intersection (fromListWith (+) xs) (fromListWith (+) ys)))
-    == sort (nub ((List.intersect) (Prelude.map fst xs) (Prelude.map fst ys)))
+prop_differenceModel :: [(Int,Int)] -> [(Int,Int)] -> Property
+prop_differenceModel xs ys =
+  case difference (fromListWith (+) xs) (fromListWith (+) ys) of
+    t ->
+      valid t .&&.
+      sort (keys t) === sort ((List.\\)
+                                 (nub (Prelude.map fst xs))
+                                 (nub (Prelude.map fst ys)))
+
+prop_intersectionModel :: [(Int,Int)] -> [(Int,Int)] -> Property
+prop_intersectionModel xs ys =
+  case intersection (fromListWith (+) xs) (fromListWith (+) ys) of
+    t ->
+      valid t .&&.
+      sort (keys t) === sort (nub ((List.intersect)
+                                      (Prelude.map fst xs)
+                                      (Prelude.map fst ys)))
 
 prop_intersectionWithModel :: [(Int,Int)] -> [(Int,Int)] -> Bool
 prop_intersectionWithModel xs ys
@@ -902,19 +942,20 @@ prop_ascDescList :: [Int] -> Bool
 prop_ascDescList xs = toAscList m == reverse (toDescList m)
   where m = fromList $ zip xs $ repeat ()
 
-prop_fromList :: [Int] -> Bool
+prop_fromList :: [Int] -> Property
 prop_fromList xs
   = case fromList (zip xs xs) of
-      t -> t == fromAscList (zip sort_xs sort_xs) &&
-           t == fromDistinctAscList (zip nub_sort_xs nub_sort_xs) &&
-           t == List.foldr (uncurry insert) empty (zip xs xs)
+      t -> valid t .&&.
+           t === fromAscList (zip sort_xs sort_xs) .&&.
+           t === fromDistinctAscList (zip nub_sort_xs nub_sort_xs) .&&.
+           t === List.foldr (uncurry insert) empty (zip xs xs)
   where sort_xs = sort xs
         nub_sort_xs = List.map List.head $ List.group sort_xs
 
 ----------------------------------------------------------------
 
-prop_alter :: UMap -> Int -> Bool
-prop_alter t k = case lookup k t of
+prop_alter :: UMap -> Int -> Property
+prop_alter t k = valid t' .&&. case lookup k t of
     Just _  -> (size t - 1) == size t' && lookup k t' == Nothing
     Nothing -> (size t + 1) == size t' && lookup k t' /= Nothing
   where
@@ -1024,14 +1065,18 @@ prop_deleteMaxModel ys = length ys > 0 ==>
 prop_filter :: Fun Int Bool -> [(Int, Int)] -> Property
 prop_filter p ys = length ys > 0 ==>
   let xs = List.nubBy ((==) `on` fst) ys
-      m  = fromList xs
-  in  filter (apply p) m == fromList (List.filter (apply p . snd) xs)
+      m  = filter (apply p) (fromList xs)
+  in  valid m .&&.
+      m === fromList (List.filter (apply p . snd) xs)
 
 prop_partition :: Fun Int Bool -> [(Int, Int)] -> Property
 prop_partition p ys = length ys > 0 ==>
   let xs = List.nubBy ((==) `on` fst) ys
-      m  = fromList xs
-  in  partition (apply p) m == let (a,b) = (List.partition (apply p . snd) xs) in (fromList a, fromList b)
+      m@(l, r) = partition (apply p) (fromList xs)
+  in  valid l .&&.
+      valid r .&&.
+      m === let (a,b) = (List.partition (apply p . snd) xs)
+            in (fromList a, fromList b)
 
 prop_map :: Fun Int Int -> [(Int, Int)] -> Property
 prop_map f ys = length ys > 0 ==>
@@ -1055,8 +1100,10 @@ prop_splitModel :: Int -> [(Int, Int)] -> Property
 prop_splitModel n ys = length ys > 0 ==>
   let xs = List.nubBy ((==) `on` fst) ys
       (l, r) = split n $ fromList xs
-  in  toAscList l == sort [(k, v) | (k,v) <- xs, k < n] &&
-      toAscList r == sort [(k, v) | (k,v) <- xs, k > n]
+  in  valid l .&&.
+      valid r .&&.
+      toAscList l === sort [(k, v) | (k,v) <- xs, k < n] .&&.
+      toAscList r === sort [(k, v) | (k,v) <- xs, k > n]
 
 prop_splitRoot :: IMap -> Bool
 prop_splitRoot s = loop ls && (s == unions ls)
index 0cf2504..56283c0 100644 (file)
@@ -10,6 +10,7 @@ import Data.List (nub,sort)
 import qualified Data.List as List
 import Data.Monoid (mempty)
 import qualified Data.Set as Set
+import IntSetValidity (valid)
 import Prelude hiding (lookup, null, map, filter, foldr, foldl)
 import Test.Framework
 import Test.Framework.Providers.HUnit
@@ -23,6 +24,10 @@ main = defaultMain [ testCase "lookupLT" test_lookupLT
                    , testCase "lookupLE" test_lookupLE
                    , testCase "lookupGE" test_lookupGE
                    , testCase "split" test_split
+                   , testProperty "prop_Valid" prop_Valid
+                   , testProperty "prop_EmptyValid" prop_EmptyValid
+                   , testProperty "prop_SingletonValid" prop_SingletonValid
+                   , testProperty "prop_InsertIntoEmptyValid" prop_InsertIntoEmptyValid
                    , testProperty "prop_Single" prop_Single
                    , testProperty "prop_Member" prop_Member
                    , testProperty "prop_NotMember" prop_NotMember
@@ -109,6 +114,37 @@ instance Arbitrary IntSet where
                 ; return (fromList xs)
                 }
 
+{--------------------------------------------------------------------
+  Valid IntMaps
+--------------------------------------------------------------------}
+forValid :: Testable a => (IntSet -> a) -> Property
+forValid f = forAll arbitrary $ \t ->
+    classify (size t == 0) "empty" $
+    classify (size t > 0 && size t <= 10) "small" $
+    classify (size t > 10 && size t <= 64) "medium" $
+    classify (size t > 64) "large" $ f t
+
+forValidUnitTree :: Testable a => (IntSet -> a) -> Property
+forValidUnitTree f = forValid f
+
+prop_Valid :: Property
+prop_Valid = forValidUnitTree $ \t -> valid t
+
+{--------------------------------------------------------------------
+  Construction validity
+--------------------------------------------------------------------}
+
+prop_EmptyValid :: Property
+prop_EmptyValid =
+    valid empty
+
+prop_SingletonValid :: Int -> Property
+prop_SingletonValid x =
+    valid (singleton x)
+
+prop_InsertIntoEmptyValid :: Int -> Property
+prop_InsertIntoEmptyValid x =
+    valid (insert x empty)
 
 {--------------------------------------------------------------------
   Single, Member, Insert, Delete, Member, FromList
@@ -155,7 +191,9 @@ prop_LookupGE = test_LookupSomething lookupGE (>=)
 
 prop_InsertDelete :: Int -> IntSet -> Property
 prop_InsertDelete k t
-  = not (member k t) ==> delete k (insert k t) == t
+  = not (member k t) ==>
+      case delete k (insert k t) of
+        t' -> valid t' .&&. t' === t
 
 prop_MemberFromList :: [Int] -> Bool
 prop_MemberFromList xs
@@ -166,9 +204,12 @@ prop_MemberFromList xs
 {--------------------------------------------------------------------
   Union
 --------------------------------------------------------------------}
-prop_UnionInsert :: Int -> IntSet -> Bool
-prop_UnionInsert x t
-  = union t (singleton x) == insert x t
+prop_UnionInsert :: Int -> IntSet -> Property
+prop_UnionInsert x t =
+  case union t (singleton x) of
+    t' ->
+      valid t' .&&.
+      t' === insert x t
 
 prop_UnionAssoc :: IntSet -> IntSet -> IntSet -> Bool
 prop_UnionAssoc t1 t2 t3
@@ -178,15 +219,19 @@ prop_UnionComm :: IntSet -> IntSet -> Bool
 prop_UnionComm t1 t2
   = (union t1 t2 == union t2 t1)
 
-prop_Diff :: [Int] -> [Int] -> Bool
-prop_Diff xs ys
-  =  toAscList (difference (fromList xs) (fromList ys))
-    == List.sort ((List.\\) (nub xs)  (nub ys))
+prop_Diff :: [Int] -> [Int] -> Property
+prop_Diff xs ys =
+  case difference (fromList xs) (fromList ys) of
+    t ->
+      valid t .&&.
+      toAscList t === List.sort ((List.\\) (nub xs)  (nub ys))
 
-prop_Int :: [Int] -> [Int] -> Bool
-prop_Int xs ys
-  =  toAscList (intersection (fromList xs) (fromList ys))
-    == List.sort (nub ((List.intersect) (xs)  (ys)))
+prop_Int :: [Int] -> [Int] -> Property
+prop_Int xs ys =
+  case intersection (fromList xs) (fromList ys) of
+    t ->
+      valid t .&&.
+      toAscList t === List.sort (nub ((List.intersect) (xs)  (ys)))
 
 {--------------------------------------------------------------------
   Lists
@@ -207,12 +252,13 @@ prop_AscDescList :: [Int] -> Bool
 prop_AscDescList xs = toAscList s == reverse (toDescList s)
   where s = fromList xs
 
-prop_fromList :: [Int] -> Bool
+prop_fromList :: [Int] -> Property
 prop_fromList xs
   = case fromList xs of
-      t -> t == fromAscList sort_xs &&
-           t == fromDistinctAscList nub_sort_xs &&
-           t == List.foldr insert empty xs
+      t -> valid t .&&.
+           t === fromAscList sort_xs .&&.
+           t === fromDistinctAscList nub_sort_xs .&&.
+           t === List.foldr insert empty xs
   where sort_xs = sort xs
         nub_sort_xs = List.map List.head $ List.group sort_xs
 
@@ -303,13 +349,22 @@ prop_minView s = case minView s of
     Nothing -> null s
     Just (m,s') -> m == minimum (toList s) && s == insert m s' && m `notMember` s'
 
-prop_split :: IntSet -> Int -> Bool
+prop_split :: IntSet -> Int -> Property
 prop_split s i = case split i s of
-    (s1,s2) -> all (<i) (toList s1) && all (>i) (toList s2) && i `delete` s == union s1 s2
+    (s1,s2) -> valid s1 .&&.
+               valid s2 .&&.
+               all (<i) (toList s1) .&&.
+               all (>i) (toList s2) .&&.
+               i `delete` s === union s1 s2
 
-prop_splitMember :: IntSet -> Int -> Bool
+prop_splitMember :: IntSet -> Int -> Property
 prop_splitMember s i = case splitMember i s of
-    (s1,t,s2) -> all (<i) (toList s1) && all (>i) (toList s2) && t == i `member` s && i `delete` s == union s1 s2
+    (s1,t,s2) -> valid s1 .&&.
+                 valid s2 .&&.
+                 all (<i) (toList s1) .&&.
+                 all (>i) (toList s2) .&&.
+                 t === i `member` s .&&.
+                 i `delete` s === union s1 s2
 
 prop_splitRoot :: IntSet -> Bool
 prop_splitRoot s = loop ls && (s == unions ls)
@@ -321,12 +376,22 @@ prop_splitRoot s = loop ls && (s == unions ls)
                           , y <- toList (unions rst)
                           , x > y ]
 
-prop_partition :: IntSet -> Int -> Bool
+prop_partition :: IntSet -> Int -> Property
 prop_partition s i = case partition odd s of
-    (s1,s2) -> all odd (toList s1) && all even (toList s2) && s == s1 `union` s2
-
-prop_filter :: IntSet -> Int -> Bool
-prop_filter s i = partition odd s == (filter odd s, filter even s)
+    (s1,s2) -> valid s1 .&&.
+               valid s2 .&&.
+               all odd (toList s1) .&&.
+               all even (toList s2) .&&.
+               s === s1 `union` s2
+
+prop_filter :: IntSet -> Int -> Property
+prop_filter s i =
+  let parts = partition odd s
+      odds = filter odd s
+      evens = filter even s
+  in valid odds .&&.
+     valid evens .&&.
+     parts === (odds, evens)
 
 #if MIN_VERSION_base(4,5,0)
 prop_bitcount :: Int -> Word -> Bool