Polysemy Spar: Laws for DefaultSsoCode, Now, IdP and ScimExternalIdStore

changelog.d/5-internal/in-mem-specs

@@ -0,0 +1 @@
+Added laws for DefaultSsoCode, Now, IdP and ScimExternalIdStore

services/spar/package.yaml

@@ -99,7 +99,7 @@ tests:
       - QuickCheck
       - spar
       - uri-bytestring
-      - polysemy-check
+      - polysemy-check >= 0.9
 
 executables:
   spar:

services/spar/spar.cabal

@@ -4,7 +4,7 @@ cabal-version: 1.12
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 34138a2c7fa249191ae03bc1581a7c95c94b12080f104da084a9bc37ac54c9ad
+-- hash: 4a323def34cfdc7673cea02e13fe518d53d7b04bae552bff2d0784dfb6964162
 
 name:           spar
 version:        0.1
@@ -514,8 +514,11 @@ test-suite spec
       Test.Spar.Intra.BrigSpec
       Test.Spar.Roundtrip.ByteString
       Test.Spar.ScimSpec
+      Test.Spar.Sem.DefaultSsoCodeSpec
       Test.Spar.Sem.IdPRawMetadataStoreSpec
       Test.Spar.Sem.IdPSpec
+      Test.Spar.Sem.NowSpec
+      Test.Spar.Sem.ScimExternalIdStoreSpec
       Test.Spar.TypesSpec
       Paths_spar
   hs-source-dirs:
@@ -564,7 +567,7 @@ test-suite spec
     , network-uri
     , optparse-applicative
     , polysemy
-    , polysemy-check
+    , polysemy-check >=0.9
     , polysemy-plugin
     , raw-strings-qq
     , retry

services/spar/src/Spar/Sem/DefaultSsoCode.hs

@@ -9,4 +9,6 @@ data DefaultSsoCode m a where
   Store :: SAML.IdPId -> DefaultSsoCode m ()
   Delete :: DefaultSsoCode m ()
 
+deriving instance Show (DefaultSsoCode m a)
+
 makeSem ''DefaultSsoCode

services/spar/src/Spar/Sem/Now.hs

@@ -9,6 +9,8 @@ data Now m a where
 
 makeSem ''Now
 
+deriving instance Show (Now m a)
+
 -- | Check a time against 'Now', checking if it's still alive (hasn't occurred yet.)
 boolTTL ::
   Member Now r =>

services/spar/src/Spar/Sem/ScimExternalIdStore.hs

@@ -10,4 +10,6 @@ data ScimExternalIdStore m a where
   Lookup :: TeamId -> Email -> ScimExternalIdStore m (Maybe UserId)
   Delete :: TeamId -> Email -> ScimExternalIdStore m ()
 
+deriving instance Show (ScimExternalIdStore m a)
+
 makeSem ''ScimExternalIdStore

services/spar/test/Arbitrary.hs

@@ -23,7 +23,7 @@
 module Arbitrary where
 
 import Data.Aeson
-import Data.Id (TeamId)
+import Data.Id (TeamId, UserId)
 import Data.Proxy
 import Data.String.Conversions (cs)
 import Data.Swagger hiding (Header (..))
@@ -97,6 +97,8 @@ instance Arbitrary E.Replaced where
 
 instance CoArbitrary a => CoArbitrary (E.GetIdPResult a)
 
+-- TODO(sandy): IdPIds are unlikely to collide. Does the size parameter
+-- affect them?
 instance CoArbitrary IdPId
 
 instance CoArbitrary WireIdP
@@ -105,6 +107,10 @@ instance CoArbitrary WireIdPAPIVersion
 
 instance CoArbitrary TeamId
 
+instance CoArbitrary UserId
+
+instance CoArbitrary Time
+
 instance CoArbitrary Issuer where
   coarbitrary (Issuer ur) = coarbitrary $ show ur
 

services/spar/test/Test/Spar/Sem/DefaultSsoCodeSpec.hs

@@ -0,0 +1,173 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -fplugin=Polysemy.Plugin #-}
+
+module Test.Spar.Sem.DefaultSsoCodeSpec where
+
+import Arbitrary ()
+import Imports
+import Polysemy
+import Polysemy.Check
+import SAML2.WebSSO.Types
+import qualified Spar.Sem.DefaultSsoCode as E
+import Spar.Sem.DefaultSsoCode.Mem
+import Test.Hspec
+import Test.Hspec.QuickCheck
+import Test.QuickCheck
+
+deriveGenericK ''E.DefaultSsoCode
+
+propsForInterpreter ::
+  PropConstraints r f =>
+  String ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Spec
+propsForInterpreter interpreter lower = do
+  describe interpreter $ do
+    prop "delete/delete" $ prop_deleteDelete Nothing lower
+    prop "delete/get" $ prop_deleteGet Nothing lower
+    prop "delete/store" $ prop_deleteStore Nothing lower
+    prop "get/store" $ prop_getStore Nothing lower
+    prop "store/delete" $ prop_storeStore Nothing lower
+    prop "store/get" $ prop_storeGet Nothing lower
+    prop "store/store" $ prop_storeStore Nothing lower
+
+spec :: Spec
+spec = modifyMaxSuccess (const 1000) $ do
+  propsForInterpreter "defaultSsoCodeToMem" $ pure . run . defaultSsoCodeToMem
+
+-- | All the constraints we need to generalize properties in this module.
+-- A regular type synonym doesn't work due to dreaded impredicative
+-- polymorphism.
+class
+  (Functor f, Member E.DefaultSsoCode r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+instance
+  (Functor f, Member E.DefaultSsoCode r, forall z. Show z => Show (f z), forall z. Eq z => Eq (f z)) =>
+  PropConstraints r f
+
+prop_storeGet ::
+  PropConstraints r f =>
+  Maybe (f (Maybe IdPId) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_storeGet =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    s <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.store s
+            E.get
+        )
+        ( do
+            E.store s
+            pure (Just s)
+        )
+
+prop_getStore ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_getStore =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    pure $
+      simpleLaw
+        ( do
+            E.get >>= maybe (pure ()) E.store
+        )
+        ( do
+            pure ()
+        )
+
+prop_storeDelete ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_storeDelete =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    s <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.store s
+            E.delete
+        )
+        ( do
+            E.delete
+        )
+
+prop_deleteStore ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_deleteStore =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    s <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.delete
+            E.store s
+        )
+        ( do
+            E.store s
+        )
+
+prop_storeStore ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_storeStore =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    s <- arbitrary
+    s' <- arbitrary
+    pure $
+      simpleLaw
+        ( do
+            E.store s
+            E.store s'
+        )
+        ( do
+            E.store s'
+        )
+
+prop_deleteDelete ::
+  PropConstraints r f =>
+  Maybe (f () -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_deleteDelete =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    pure $
+      simpleLaw
+        ( do
+            E.delete
+            E.delete
+        )
+        ( do
+            E.delete
+        )
+
+prop_deleteGet ::
+  PropConstraints r f =>
+  Maybe (f (Maybe IdPId) -> String) ->
+  (forall a. Sem r a -> IO (f a)) ->
+  Property
+prop_deleteGet =
+  prepropLaw @'[E.DefaultSsoCode] $ do
+    pure $
+      simpleLaw
+        ( do
+            E.delete
+            E.get
+        )
+        ( do
+            E.delete
+            pure Nothing
+        )