diff --git a/agora-specs/Property/Governor.hs b/agora-specs/Property/Governor.hs new file mode 100644 index 0000000..bf200b0 --- /dev/null +++ b/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 + ] diff --git a/agora-specs/Property/MultiSig.hs b/agora-specs/Property/MultiSig.hs index 1000e03..caa35cc 100644 --- a/agora-specs/Property/MultiSig.hs +++ b/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 (..), diff --git a/agora-test/Spec.hs b/agora-test/Spec.hs index 4e8399a..e11a5e1 100644 --- a/agora-test/Spec.hs +++ b/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 diff --git a/agora.cabal b/agora.cabal index a3c6d21..7cf71c2 100644 --- a/agora.cabal +++ b/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