Implement governor mintint policy property tests.

agora-specs/Property/Governor.hs

@@ -7,19 +7,85 @@ Property model and tests for 'Governor' related functions
 -}
 module Property.Governor (props) where
 
-import Test.Tasty (TestTree)
+import Agora.Governor (
-import Test.QuickCheck (Property, Gen, Arbitrary (arbitrary), arbitraryBoundedEnum, chooseInteger)
+  GovernorDatum (
-import Test.Tasty.QuickCheck (testProperty)
+    GovernorDatum,
+    createProposalTimeRangeMaxWidth,
+    maximumProposalsPerStake,
+    nextProposalId,
+    proposalThresholds,
+    proposalTimings
+  ),
+  PGovernorDatum,
+  pisGovernorDatumValid,
+ )
+import Agora.Governor.Scripts (governorPolicy)
+import Agora.Proposal (
+  ProposalId (ProposalId),
+  ProposalThresholds (
+    ProposalThresholds
+  ),
+ )
+import Agora.Proposal.Time (
+  MaxTimeRangeWidth (MaxTimeRangeWidth),
+  ProposalTimingConfig (ProposalTimingConfig),
+ )
+import Data.Default (def)
+import Data.Tagged (Tagged (Tagged))
 import Data.Universe (Universe)
 import Data.Universe.Class (Finite)
-import Plutarch.Test.QuickCheck (Equality (OnPEq), Partiality (ByComplete), haskEquiv, TestableTerm (TestableTerm), pconstantT)
+import Generics.SOP.NP (NP (Nil, (:*)))
-import Agora.Governor (pisGovernorDatumValid, GovernorDatum(GovernorDatum), PGovernorDatum)
-import Agora.Proposal (ProposalThresholds(ProposalThresholds), ProposalId (ProposalId))
-import Agora.Proposal.Time (ProposalTimingConfig(ProposalTimingConfig), MaxTimeRangeWidth (MaxTimeRangeWidth))
-import Data.Tagged (Tagged(Tagged))
-import Generics.SOP.NP (NP(Nil, (:*)))
 import Optics (view)
-
+import Plutarch.Api.V2 (PScriptContext)
+import Plutarch.Builtin (pforgetData)
+import Plutarch.Context (
+  MintingBuilder,
+  buildMinting',
+  input,
+  mint,
+  output,
+  script,
+  withDatum,
+  withMinting,
+  withRef,
+  withValue,
+ )
+import Plutarch.Evaluate (evalTerm)
+import Plutarch.Extra.AssetClass (assetClassValue)
+import Plutarch.Extra.Compile (mustCompile)
+import Plutarch.Test.QuickCheck (
+  Equality (OnPEq),
+  Partiality (ByComplete),
+  TestableTerm (TestableTerm),
+  haskEquiv,
+  pconstantT,
+  shouldCrash,
+  shouldRun,
+ )
+import PlutusLedgerApi.V2 (Script, ScriptContext)
+import Property.Generator (genInput, genOutput)
+import Sample.Shared (
+  deterministicTracingConfig,
+  governor,
+  governorAssetClass,
+  governorSymbol,
+  governorValidatorHash,
+  gstUTXORef,
+ )
+import Test.QuickCheck (
+  Arbitrary (arbitrary),
+  Gen,
+  Property,
+  arbitraryBoundedEnum,
+  checkCoverage,
+  choose,
+  chooseInteger,
+  cover,
+  forAll,
+  listOf1,
+ )
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.QuickCheck (testProperty)
 
 data GovernorDatumCases
   = ExecuteLE0
@@ -34,17 +100,16 @@ data GovernorDatumCases
 instance Arbitrary GovernorDatumCases where
   arbitrary = arbitraryBoundedEnum
 
-{- | Property that checks `pisGovernorDatumValid` behaves as intended by comparing it
+{- | Property that checks `pisGovernorDatumValid` behaves as intended by
-  to a simple haskell implementation.
+     comparing it to a simple haskell implementation.
 -}
 governorDatumValidProperty :: Property
 governorDatumValidProperty =
-  haskEquiv @'OnPEq @'ByComplete
+  haskEquiv @( 'OnPEq) @( 'ByComplete)
     isValidModelImpl
     (TestableTerm pisGovernorDatumValid)
     (genDatum :* Nil)
   where
-
     genDatum :: Gen (TestableTerm PGovernorDatum)
     genDatum = pconstantT <$> (arbitrary >>= genDatumForCase)
       where
@@ -53,7 +118,8 @@ governorDatumValidProperty =
           thres <- genProposalThresholds c
 
           let timing = ProposalTimingConfig 0 0 0 0
-          return $ GovernorDatum thres (ProposalId 0) timing (MaxTimeRangeWidth 1) 3
+          pure $
+            GovernorDatum thres (ProposalId 0) timing (MaxTimeRangeWidth 1) 3
           where
             taggedInteger p = Tagged <$> chooseInteger p
             genProposalThresholds :: GovernorDatumCases -> Gen ProposalThresholds
@@ -83,7 +149,7 @@ governorDatumValidProperty =
                 Correct ->
                   return $ ProposalThresholds execute create toVoting vote cosign
 
-    -- | This is a model Haskell implementation of `pisGovernorDatumValid`.
+    -- \| This is a model Haskell implementation of `pisGovernorDatumValid`.
     isValidModelImpl :: GovernorDatum -> Bool
     isValidModelImpl = correctCase . classifier
       where
@@ -108,99 +174,130 @@ governorDatumValidProperty =
             | cosign < 0 = CosignLE0
             | otherwise = Correct
 
----
+--------------------------------------------------------------------------------
 
--- data GovernorPolicyCases
+data GovernorPolicyCases
---   = ReferenceUTXONotSpent
+  = ReferenceUTXONotSpent
---   | IncorrectAmountOfTokenMinted
+  | IncorrectAmountOfTokenMinted
---   | GovernorOutputNotFound
+  | GovernorOutputNotFound
---   | GovernorPolicyCorrect
+  deriving stock (Eq, Show)
---   deriving stock (Eq, Show)
 
--- instance Universe GovernorPolicyCases where
+governorMintingPolicyTests :: [TestTree]
---   universe =
+governorMintingPolicyTests =
---     [ ReferenceUTXONotSpent
+  [ mkGovMintingCasePropertyTest
---     , IncorrectAmountOfTokenMinted
+      "Reference input spend test"
---     , GovernorOutputNotFound
+      ReferenceUTXONotSpent
---     , GovernorPolicyCorrect
+      "Spent"
---     ]
+      "Not spent"
+  , mkGovMintingCasePropertyTest
+      "Amount of token minted test"
+      IncorrectAmountOfTokenMinted
+      "Correct"
+      "Incorrect"
+  , mkGovMintingCasePropertyTest
+      "Governor output presense"
+      GovernorOutputNotFound
+      "Present"
+      "Absent"
+  ]
 
--- instance Finite GovernorPolicyCases where
+{- | Creates a property by compiling governorPolicy script with given arguments
---   universeF = universe
+   and checking if it runs as expected by a test.
---   cardinality = Tagged 4
+-}
+governorPolicyValid :: ScriptContext -> Bool -> Property
+governorPolicyValid ctx shouldSuceed =
+  let mp = mkPolicyScript ctx in if shouldSuceed then shouldRun mp else shouldCrash mp
 
--- governorMintingProperty :: Property
+{-# INLINEABLE mkPolicyScript #-}
--- governorMintingProperty =
+mkPolicyScript :: ScriptContext -> Script
---   classifiedPropertyNative gen (const []) expected classifier actual
+mkPolicyScript ctx = mustCompile (go # pconstant ctx)
---   where
+  where
---     {- Note:
+    go :: forall (s :: S). Term s (PScriptContext :--> POpaque)
---     I don't think it's easily possible to randomize orefs. We can't really pass pass `Governor` type to `actual` function.
+    go = loudEval $
---     -}
+      plam $ \sc ->
---     gst = assetClassValue governorAssetClass 1
+        governorPolicy
---     mintAmount x = mint . mconcat $ replicate x gst
+          # pconstant (view #gstOutRef governor)
---     outputToGov =
+          # pforgetData (pconstantData ())
---       output $
+          # sc
---         mconcat
---           [ script governorValidatorHash
---           , withValue gst
---           , withDatum govDatum
---           ]
---     referencedInput = input $ withRef gstUTXORef
 
---     govDatum :: GovernorDatum
+{- | Prepares a minting policy test for given policy error case.
---     govDatum =
+ NOTE
---       GovernorDatum
+-}
---         { proposalThresholds = def
+mkGovMintingCasePropertyTest ::
---         , nextProposalId = ProposalId 0
+  String ->
---         , proposalTimings = def
+  GovernorPolicyCases ->
---         , createProposalTimeRangeMaxWidth = def
+  String ->
---         , maximumProposalsPerStake = 3
+  String ->
---         }
+  TestTree
+mkGovMintingCasePropertyTest name case' positiveCaseName negativeCaseName =
+  testProperty name $
+    forAll (gen case') $
+      \(ctx, valid) ->
+        checkCoverage $
+          cover 48 valid positiveCaseName $
+            cover 48 (not valid) negativeCaseName $
+              governorPolicyValid ctx valid
+  where
+    gen :: GovernorPolicyCases -> Gen (ScriptContext, Bool)
+    gen c = do
+      inputs <- fmap mconcat . listOf1 $ genInput @MintingBuilder
+      outputs <- fmap mconcat . listOf1 $ genOutput @MintingBuilder
+      toks <- choose (2, 100)
 
---     gen :: GovernorPolicyCases -> Gen ScriptContext
+      valid <- arbitrary
---     gen c = do
+      let comp =
---       inputs <- fmap mconcat . listOf1 $ genInput @MintingBuilder
+            if valid
---       outputs <- fmap mconcat . listOf1 $ genOutput @MintingBuilder
+              then referencedInput <> outputToGov <> mintAmount 1
---       toks <- choose (2, 100)
+              else case c of
+                ReferenceUTXONotSpent -> outputToGov <> mintAmount 1
+                IncorrectAmountOfTokenMinted ->
+                  referencedInput
+                    <> outputToGov
+                    <> mintAmount toks
+                GovernorOutputNotFound -> referencedInput <> mintAmount 1
 
---       let comp =
+      let ctx =
---             case c of
+            buildMinting' $
---               ReferenceUTXONotSpent -> outputToGov <> mintAmount 1
+              inputs
---               IncorrectAmountOfTokenMinted -> referencedInput <> outputToGov <> mintAmount toks
+                <> outputs
---               GovernorOutputNotFound -> referencedInput <> mintAmount 1
+                <> comp
---               GovernorPolicyCorrect -> referencedInput <> outputToGov <> mintAmount 1
+                <> withMinting
+                  governorSymbol
+      pure (ctx, valid)
+      where
+        govDatum :: GovernorDatum
+        govDatum =
+          GovernorDatum
+            { proposalThresholds = def
+            , nextProposalId = ProposalId 0
+            , proposalTimings = def
+            , createProposalTimeRangeMaxWidth = def
+            , maximumProposalsPerStake = 3
+            }
 
---       return . buildMinting' $ inputs <> outputs <> comp <> withMinting governorSymbol
+        gst = assetClassValue governorAssetClass 1
-
+        mintAmount x = mint . mconcat $ replicate x gst
---     expected :: ScriptContext -> Maybe ()
+        referencedInput = input $ withRef gstUTXORef
---     expected sc =
+        outputToGov =
---       case classifier sc of
+          output $
---         GovernorPolicyCorrect -> Just ()
+            mconcat
---         _ -> Nothing
+              [ script governorValidatorHash
-
+              , withValue gst
---     opaqueToUnit :: Term s (POpaque :--> PUnit)
+              , withDatum govDatum
---     opaqueToUnit = plam $ \_ -> pconstant ()
+              ]
-
---     actual :: Term s (PScriptContext :--> PUnit)
---     actual = plam $ \sc -> opaqueToUnit #$ governorPolicy # pconstant governor.gstOutRef # pforgetData (pconstantData ()) # sc
-
---     classifier :: ScriptContext -> GovernorPolicyCases
---     classifier sc
---       | minted /= gst = IncorrectAmountOfTokenMinted
---       | refInputNotExists = ReferenceUTXONotSpent
---       | govOutputNotExists = GovernorOutputNotFound
---       | otherwise = GovernorPolicyCorrect
---       where
---         txinfo = scriptContextTxInfo sc
---         minted = txInfoMint txinfo
---         refInputNotExists = gstUTXORef `notElem` (txInInfoOutRef <$> txInfoInputs txinfo)
---         govOutputNotExists = gst `notElem` (txOutValue <$> txInfoOutputs txinfo)
 
 props :: [TestTree]
 props =
   [ testProperty "governorDatumValid" governorDatumValidProperty
-  -- , testProperty "governorPolicy" governorMintingProperty
+  , testGroup "governorPolicy" governorMintingPolicyTests
   ]
 
--- props :: [TestTree]
+loudEval ::
--- props = []
+  forall (p :: S -> Type).
+  ClosedTerm p ->
+  ClosedTerm p
+loudEval x =
+  case evalTerm deterministicTracingConfig x of
+    Right (Right t, _, _) -> t
+    Right (Left err, _, trace) -> error $ show err <> show trace
+    Left err -> error $ show err

agora-specs/Sample/Governor/Initialize.hs

@@ -58,7 +58,7 @@ import PlutusLedgerApi.V2 (
   ValidatorHash,
  )
 import Sample.Shared (
-  deterministicTracingConfing,
+  deterministicTracingConfig,
   minAda,
  )
 import Sample.Shared qualified as Shared
@@ -124,7 +124,7 @@ scripts =
     (view #scripts)
     ( runLinker
         linker
-        (agoraScripts deterministicTracingConfing)
+        (agoraScripts deterministicTracingConfig)
         governor
     )
 

agora-specs/Sample/Shared.hs

@@ -12,7 +12,7 @@ module Sample.Shared (
   signer,
   signer2,
   minAda,
-  deterministicTracingConfing,
+  deterministicTracingConfig,
   mkRedeemer,
 
   -- * Agora Scripts
@@ -121,8 +121,8 @@ import ScriptExport.ScriptInfo (runLinker)
 -- Plutarch compiler configauration.
 -- TODO: add the ability to change this value. Maybe wrap everything in a
 --        Reader monad?
-deterministicTracingConfing :: Config
+deterministicTracingConfig :: Config
-deterministicTracingConfing = Config DetTracing
+deterministicTracingConfig = Config DetTracing
 
 governor :: Governor
 governor = Governor oref gt mc
@@ -142,7 +142,7 @@ agoraScripts =
     (view #scripts)
     ( runLinker
         linker
-        (Bootstrap.agoraScripts deterministicTracingConfing)
+        (Bootstrap.agoraScripts deterministicTracingConfig)
         governor
     )
 

agora/Agora/Governor.hs

@@ -42,6 +42,7 @@ import Agora.Proposal.Time (
 import Agora.SafeMoney (GTTag)
 import Data.Aeson qualified as Aeson
 import Data.Tagged (Tagged)
+import Optics.TH (makeFieldLabelsNoPrefix)
 import Plutarch.DataRepr (
   DerivePConstantViaData (DerivePConstantViaData),
   PDataFields,
@@ -56,7 +57,6 @@ import "liqwid-plutarch-extra" Plutarch.Extra.TermCont (pletFieldsC)
 import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (PLifted))
 import PlutusLedgerApi.V1 (TxOutRef)
 import PlutusTx qualified
-import Optics.TH (makeFieldLabelsNoPrefix)
 
 --------------------------------------------------------------------------------
 
@@ -88,7 +88,6 @@ data GovernorDatum = GovernorDatum
 -- | @since 0.2.1
 makeFieldLabelsNoPrefix ''GovernorDatum
 
-
 -- | @since 0.1.0
 PlutusTx.makeIsDataIndexed ''GovernorDatum [('GovernorDatum, 0)]
 
@@ -154,6 +153,8 @@ data Governor = Governor
       Aeson.FromJSON
     )
 
+makeFieldLabelsNoPrefix ''Governor
+
 --------------------------------------------------------------------------------
 
 {- | Plutarch-level datum for the Governor script.