Expanded logicalmodel of treasury tests

agora-test/Spec/Model/Treasury.hs

@@ -22,14 +22,20 @@ import Apropos (
   (:+),
  )
 import Apropos.Script (HasScriptRunner (expect, runScriptTestsWhere, script))
+import Data.Maybe (fromMaybe)
 import Data.Set (Set)
-import Plutus.V1.Ledger.Api (
+import Plutus.V1.Ledger.Address (Address (addressCredential))
-  CurrencySymbol,
+import Plutus.V1.Ledger.Contexts (
   ScriptContext (scriptContextPurpose, scriptContextTxInfo),
   ScriptPurpose (Minting),
-  TxInfo (txInfoMint),
+  TxInfo (txInfoMint, txInfoOutputs),
-  Value,
+  TxOut (txOutAddress, txOutValue),
  )
+import Plutus.V1.Ledger.Credential (Credential (PubKeyCredential, ScriptCredential))
+import Plutus.V1.Ledger.Scripts (ValidatorHash (ValidatorHash))
+import Plutus.V1.Ledger.Value (CurrencySymbol, TokenName (unTokenName), Value (getValue))
+import PlutusTx.AssocMap (Map, elems, keys)
+import PlutusTx.AssocMap qualified as AssocMap (all, lookup)
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.Hedgehog (fromGroup)
 
@@ -57,6 +63,7 @@ data TreasuryTxModel = TreasuryTxModel
   { gatCs :: CurrencySymbol
   , ctx :: ScriptContext
   }
+  deriving stock (Show)
 
 instance Enumerable TreasuryTxProp where
   enumerated :: [TreasuryTxProp]
@@ -68,42 +75,80 @@ instance LogicalModel TreasuryTxProp where
     ExactlyOne [Var GATIsBurned, Var GATIsNotBurned]
       :&&: Var SomeGATsInvalid :->: Not (Var AllGATsValid)
 
+isMinting :: ScriptPurpose -> Bool
+isMinting (Minting _) = True
+isMinting _ = False
+
+authorityTokensValidIn :: CurrencySymbol -> TxOut -> Bool
+authorityTokensValidIn cs out =
+  let add = out.txOutAddress :: Address
+      outValue = out.txOutValue :: Value
+
+      tokenMap :: Maybe (Map TokenName Integer)
+      tokenMap = AssocMap.lookup cs $ getValue outValue
+
+      cred = add.addressCredential :: Credential
+
+      validCred :: Map TokenName Integer -> Bool
+      validCred m = case cred of
+        PubKeyCredential _ -> False
+        ScriptCredential (ValidatorHash vh) ->
+          all (\tn -> vh == unTokenName tn) $ keys m
+   in case tokenMap of
+        Nothing -> True
+        Just m -> validCred m
+
 instance HasLogicalModel TreasuryTxProp TreasuryTxModel where
   satisfiesProperty :: TreasuryTxProp -> TreasuryTxModel -> Bool
   satisfiesProperty prop model =
     let purpose = model.ctx.scriptContextPurpose :: ScriptPurpose
         txInfo = model.ctx.scriptContextTxInfo :: TxInfo
         amountMinted = txInfo.txInfoMint :: Value
+
+        csValue :: Maybe (Map TokenName Integer)
+        csValue = AssocMap.lookup model.gatCs (getValue amountMinted)
+
+        csValueSum :: Integer
+        csValueSum = case csValue of
+          Nothing -> 0
+          Just m -> sum $ elems m
      in case prop of
-          ScriptPurposeIsNotMinting -> case purpose of
+          GATIsBurned -> csValueSum <= -1
-            Minting _ -> False
+          GATIsNotBurned -> csValueSum >= 0
-            _ -> True
+          AllGATsValid ->
-          _ -> undefined
+            all
+              (authorityTokensValidIn model.gatCs)
+              txInfo.txInfoOutputs
+          SomeGATsInvalid ->
+            any
+              (not . authorityTokensValidIn model.gatCs)
+              txInfo.txInfoOutputs
+          ScriptPurposeIsNotMinting -> not $ isMinting purpose
 
--- instance HasParameterisedGenerator TreasuryTxProp Int where
+instance HasParameterisedGenerator TreasuryTxProp TreasuryTxModel where
---   parameterisedGenerator :: Set TreasuryTxProp -> Gen Int
+  parameterisedGenerator :: Set TreasuryTxProp -> Gen TreasuryTxModel
---   parameterisedGenerator = undefined
+  parameterisedGenerator = undefined
 
--- instance HasScriptRunner TreasuryTxProp Int where
+instance HasScriptRunner TreasuryTxProp TreasuryTxModel where
---   expect = undefined
+  expect = undefined
---   script = undefined
+  script = undefined
 
--- genTests :: TestTree
+genTests :: TestTree
--- genTests =
+genTests =
---   testGroup "genTests" $
+  testGroup "genTests" $
---     fromGroup
+    fromGroup
---       <$> [ runGeneratorTestsWhere
+      <$> [ runGeneratorTestsWhere
---               (Apropos :: Int :+ TreasuryTxProp)
+              (Apropos :: TreasuryTxModel :+ TreasuryTxProp)
---               "Generator"
+              "Generator"
---               Yes
+              Yes
---           ]
+          ]
 
--- plutarchTests :: TestTree
+plutarchTests :: TestTree
--- plutarchTests =
+plutarchTests =
---   testGroup "plutarchTests" $
+  testGroup "plutarchTests" $
---     fromGroup
+    fromGroup
---       <$> [ runScriptTestsWhere
+      <$> [ runScriptTestsWhere
---               (Apropos :: Int :+ TreasuryTxProp)
+              (Apropos :: TreasuryTxModel :+ TreasuryTxProp)
---               "ScriptValid"
+              "ScriptValid"
---               Yes
+              Yes
---           ]
+          ]