governorDatumValid property

agora-specs/Property/Governor.hs

@@ -0,0 +1,121 @@
+{- |
+Module     : Property.Governor
+Maintainer : seungheon.ooh@gmail.com
+Description: Property tests for 'Governor' related functions.
+
+Property model and tests for 'Governor' related functions
+-}
+module Property.Governor (props) where
+
+import Agora.Governor (
+  GovernorDatum (GovernorDatum, proposalThresholds),
+  governorDatumValid,
+ )
+import Agora.Proposal (
+  ProposalId (ProposalId),
+  ProposalThresholds (ProposalThresholds),
+ )
+import Agora.Proposal.Time (
+  MaxTimeRangeWidth (MaxTimeRangeWidth),
+  ProposalTimingConfig (ProposalTimingConfig),
+ )
+import Data.Tagged (Tagged (Tagged), untag)
+import Data.Universe (Finite (..), Universe (..))
+import Test.Tasty (TestTree)
+import Test.Tasty.Plutarch.Property (classifiedPropertyNative)
+import Test.Tasty.QuickCheck (
+  Gen,
+  Property,
+  chooseInteger,
+  testProperty,
+ )
+
+data GovernorDatumCases
+  = ExecuteLE0
+  | CreateLE0
+  | VoteLE0
+  | CreateLEVote
+  | ExecuteLVote
+  | Correct
+  deriving stock (Eq, Show)
+
+instance Universe GovernorDatumCases where
+  universe =
+    [ ExecuteLE0
+    , CreateLE0
+    , VoteLE0
+    , CreateLEVote
+    , ExecuteLVote
+    , Correct
+    ]
+
+instance Finite GovernorDatumCases where
+  universeF = universe
+  cardinality = Tagged 6
+
+{- | Property that checks `governorDatumValid`.
+ `governorDatumValid` determines if given governor datum is valid or not. This property
+ ensures `governorDatumValid` is checking the datum correctly and ruling out improper datum.
+-}
+governorDatumValidProperty :: Property
+governorDatumValidProperty =
+  classifiedPropertyNative gen (const []) expected classifier governorDatumValid
+  where
+    classifier :: GovernorDatum -> GovernorDatumCases
+    classifier (proposalThresholds -> ProposalThresholds e c v)
+      | e < 0 = ExecuteLE0
+      | c < 0 = CreateLE0
+      | v < 0 = VoteLE0
+      | c > v = CreateLEVote
+      | v >= e = ExecuteLVote
+      | otherwise = Correct
+
+    expected :: GovernorDatum -> Maybe Bool
+    expected c = Just $ classifier c == Correct
+
+    gen :: GovernorDatumCases -> Gen GovernorDatum
+    gen c = do
+      thres <- genProposalThresholds c
+
+      let timing = ProposalTimingConfig 0 0 0 0
+      return $ GovernorDatum thres (ProposalId 0) timing (MaxTimeRangeWidth 0)
+      where
+        taggedInteger p = Tagged <$> chooseInteger p
+        genProposalThresholds :: GovernorDatumCases -> Gen ProposalThresholds
+        genProposalThresholds c = do
+          let validGT = taggedInteger (0, 1000000000)
+          execute <- validGT
+          create <- validGT
+          vote <- validGT
+          le0 <- taggedInteger (-1000, -1)
+
+          case c of
+            ExecuteLE0 ->
+              -- execute < 0
+              return $ ProposalThresholds le0 create vote
+            CreateLE0 ->
+              -- c < 0
+              return $ ProposalThresholds execute le0 vote
+            VoteLE0 ->
+              -- vote < 0
+              return $ ProposalThresholds execute create le0
+            CreateLEVote -> do
+              -- c > vote
+              nv <- taggedInteger (0, untag create - 1)
+              ne <- taggedInteger (untag nv + 1, 1000000000)
+              return $ ProposalThresholds ne create nv
+            ExecuteLVote -> do
+              -- vote >= execute
+              ne <- taggedInteger (0, untag vote)
+              nc <- taggedInteger (0, untag vote)
+              return $ ProposalThresholds ne nc vote
+            Correct -> do
+              -- c <= vote < execute
+              nv <- taggedInteger (0, untag execute - 1)
+              nc <- taggedInteger (0, untag nv)
+              return $ ProposalThresholds execute nc nv
+
+props :: [TestTree]
+props =
+  [ testProperty "governorDatumValid" governorDatumValidProperty
+  ]

agora-specs/Property/MultiSig.hs

@@ -12,11 +12,11 @@ import Agora.MultiSig (
   PMultiSig,
   pvalidatedByMultisig,
  )
-import Plutarch.Extra.TermCont (pletC)
 import Data.Tagged (Tagged (Tagged))
 import Data.Universe (Finite (..), Universe (..))
 import Plutarch.Api.V1 (PScriptContext)
 import Plutarch.Context
+import Plutarch.Extra.TermCont (pletC)
 import PlutusLedgerApi.V1 (
   ScriptContext (..),
   ScriptPurpose (..),

agora-test/Spec.hs

@@ -7,6 +7,7 @@ import Test.Tasty (defaultMain, testGroup)
 
 --------------------------------------------------------------------------------
 
+import Property.Governor qualified as Governer
 import Property.MultiSig qualified as MultiSig
 import Spec.AuthorityToken qualified as AuthorityToken
 import Spec.Effect.GovernorMutation qualified as GovernorMutation
@@ -37,6 +38,7 @@ main = do
       , toTestTree $ group "Treasury tests" Treasury.specs
       , toTestTree $ group "AuthorityToken tests" AuthorityToken.specs
       , toTestTree $ group "Governor tests" Governor.specs
+      , testGroup "Governor properties" Governer.props
       , testGroup
           "Utility tests"
           Utils.tests

agora.cabal

@@ -176,6 +176,7 @@ library agora-specs
   import:          lang, deps, test-deps
   exposed-modules:
     Property.Generator
+    Property.Governor
     Property.MultiSig
     Sample.Effect.GovernorMutation
     Sample.Effect.TreasuryWithdrawal