more work on treasury testing!

agora-test/Spec.hs

@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -Wwarn #-}
+
 --------------------------------------------------------------------------------
 
 import Prelude
@@ -9,6 +11,7 @@ import Test.Tasty (defaultMain, testGroup)
 --------------------------------------------------------------------------------
 
 import Spec.Model.MultiSig qualified as MultiSig
+import Spec.Model.Treasury qualified as Treasury
 import Spec.Stake qualified as Stake
 
 -- | The Agora test suite.
@@ -28,4 +31,11 @@ main =
               , MultiSig.genTests
               ]
           ]
+      , testGroup
+          "Treasury tests"
+          [ testGroup
+              "Treasury"
+              [ Treasury.genTests
+              ]
+          ]
       ]

agora-test/Spec/Model/Treasury.hs

@@ -1,64 +1,97 @@
 {-# OPTIONS_GHC -Wwarn #-}
 
-module Spec.Model.Treasury (
-  ) where
+{- |
+Module: Spec.Model.Treasury
+Description: `apropos-tx` tests for Treasury validator.
+Maintainer: jack@mlabs.city
 
+This module contains `apropos-tx` tests for ensuring that
+the `Agora.Treasury` validator acts as desired. Notes on desired
+behaviour and invluded in this description.
+
+A Treasury transaction should pass if:
+
+  1. A GAT is burned.
+
+  2. All GATs are valid.
+
+  3. The script purpose is Minting.
+
+If either of these things do /not/ hold, then the transaction
+should fail.
+-}
+module Spec.Model.Treasury (
+  plutarchTests,
+  genTests,
+) where
+
+import Agora.Treasury (
+  PTreasuryDatum (PTreasuryDatum),
+  PTreasuryRedeemer (PAlterTreasuryParams),
+  treasuryValidator,
+ )
 import Apropos (
   Apropos (Apropos),
+  Contract,
   Enumerable (enumerated),
   Formula (
-    ExactlyOne,
     Not,
+    Some,
     Var,
     Yes,
-    (:&&:),
-    (:->:)
+    (:&&:)
   ),
   Gen,
   HasLogicalModel (satisfiesProperty),
   HasParameterisedGenerator (parameterisedGenerator),
+  HasPermutationGenerator (buildGen, generators),
   LogicalModel (logic),
+  Morphism (Morphism, contract, match, morphism, name),
+  add,
   runGeneratorTestsWhere,
   (:+),
  )
+import Apropos.Gen.Contexts (scriptContext, txInInfo)
+import Apropos.Gen.Value (currencySymbol)
 import Apropos.Script (ScriptModel (expect, runScriptTestsWhere, script))
-import Data.Maybe (fromMaybe)
 import Data.Set (Set)
+import Plutarch.Api.V1 (PCurrencySymbol, PScriptContext)
+import Plutarch.Builtin (pforgetData)
 import Plutus.V1.Ledger.Address (Address (addressCredential))
 import Plutus.V1.Ledger.Contexts (
   ScriptContext (scriptContextPurpose, scriptContextTxInfo),
   ScriptPurpose (Minting),
-  TxInfo (txInfoMint, txInfoOutputs),
+  TxInInfo (txInInfoResolved),
+  TxInfo (txInfoInputs, txInfoMint, txInfoOutputs),
   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 Plutus.V1.Ledger.Scripts (Script, ValidatorHash (ValidatorHash))
+import Plutus.V1.Ledger.Value (
+  CurrencySymbol (CurrencySymbol),
+  TokenName (unTokenName),
+  Value (Value, getValue),
+ )
+import PlutusTx.AssocMap (Map, elems, fromList, keys, singleton, toList, unionWith)
+import PlutusTx.AssocMap qualified as AssocMap (lookup)
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.Hedgehog (fromGroup)
 
-{-
-
-A Treasury transaction should pass if:
-
-1. A GAT is burned.
-2. All GATs are valid.
-
-If either of these things do _not_ hold, then the transaction
-should fail.
-
--}
-
 data TreasuryTxProp
   = GATIsBurned
-  | GATIsNotBurned
   | AllGATsValid
-  | SomeGATsInvalid
-  | ScriptPurposeIsNotMinting
+  | ScriptPurposeIsMinting
   deriving stock (Show, Eq, Ord, Enum, Bounded)
 
+instance LogicalModel TreasuryTxProp where
+  logic :: Formula TreasuryTxProp
+  logic =
+    Some
+      [ Var GATIsBurned
+      , Var AllGATsValid
+      , Var ScriptPurposeIsMinting
+      ]
+
 data TreasuryTxModel = TreasuryTxModel
   { gatCs :: CurrencySymbol
   , ctx :: ScriptContext
@@ -69,12 +102,6 @@ instance Enumerable TreasuryTxProp where
   enumerated :: [TreasuryTxProp]
   enumerated = [minBound .. maxBound]
 
-instance LogicalModel TreasuryTxProp where
-  logic :: Formula TreasuryTxProp
-  logic =
-    ExactlyOne [Var GATIsBurned, Var GATIsNotBurned]
-      :&&: Var SomeGATsInvalid :->: Not (Var AllGATsValid)
-
 isMinting :: ScriptPurpose -> Bool
 isMinting (Minting _) = True
 isMinting _ = False
@@ -113,30 +140,158 @@ instance HasLogicalModel TreasuryTxProp TreasuryTxModel where
           Nothing -> 0
           Just m -> sum $ elems m
      in case prop of
-          GATIsBurned -> csValueSum <= -1
-          GATIsNotBurned -> csValueSum >= 0
+          GATIsBurned -> csValueSum == -1
           AllGATsValid ->
             all
-              (authorityTokensValidIn model.gatCs)
-              txInfo.txInfoOutputs
-          SomeGATsInvalid ->
-            any
-              (not . authorityTokensValidIn model.gatCs)
-              txInfo.txInfoOutputs
-          ScriptPurposeIsNotMinting -> not $ isMinting purpose
+              (authorityTokensValidIn model.gatCs . txInInfoResolved)
+              txInfo.txInfoInputs
+          ScriptPurposeIsMinting -> isMinting purpose
 
 instance HasParameterisedGenerator TreasuryTxProp TreasuryTxModel where
   parameterisedGenerator :: Set TreasuryTxProp -> Gen TreasuryTxModel
-  parameterisedGenerator propSet = do
-    purpose <-
-      if ScriptPurposeIsNotMinting `elem` propSet
-        then undefined
-        else undefined
-    undefined
+  parameterisedGenerator = buildGen baseGen
+    where
+      baseGen :: Gen TreasuryTxModel
+      baseGen = do
+        cs <- currencySymbol
+        ctx <- scriptContext
+        return $ TreasuryTxModel cs ctx
+
+{- | Updates the `Integer` and `TokenName` for a given
+     `CurrencySymbol` for a given value.
+-}
+replaceValue ::
+  -- | The value whose entry to update.
+  Value ->
+  -- | The currency symbol of the entry to update.
+  CurrencySymbol ->
+  -- | The token name of the entry to place in the new value.
+  TokenName ->
+  -- | The number of tokens to place in the new value.
+  Integer ->
+  -- | The updated value.
+  Value
+replaceValue (Value v) cs tn n = Value $ unionWith (\_ x -> x) v v'
+  where
+    v' :: Map CurrencySymbol (Map TokenName Integer)
+    v' = singleton cs $ singleton tn n
+
+kmap :: (k -> k') -> Map k v -> Map k' v
+kmap g = fromList . fmap (\(x, y) -> (g x, y)) . toList
+
+fixTokenNames :: TxInInfo -> TxInInfo
+fixTokenNames inf =
+  let cred = inf.txInInfoResolved.txOutAddress.addressCredential
+      val = inf.txInInfoResolved.txOutValue
+   in case cred of
+        PubKeyCredential _ -> inf
+        ScriptCredential (ValidatorHash bs) -> undefined
+
+-- | TODO: Define.
+instance HasPermutationGenerator TreasuryTxProp TreasuryTxModel where
+  generators :: [Morphism TreasuryTxProp TreasuryTxModel]
+  generators =
+    [ Morphism
+        { name = "Ensure GAT is burned"
+        , match = Not $ Var GATIsBurned
+        , contract = add GATIsBurned
+        , morphism = \m ->
+            let ctx' = m.ctx
+                txInfo = ctx'.scriptContextTxInfo
+                mint = txInfo.txInfoMint
+                newMint = replaceValue mint m.gatCs "gat" (-1)
+             in return
+                  m
+                    { ctx =
+                        ctx'
+                          { scriptContextTxInfo =
+                              txInfo
+                                { txInfoMint = newMint
+                                }
+                          }
+                    }
+        }
+    , Morphism
+        { name = "Ensure all GATs are valid"
+        , match = Not $ Var AllGATsValid
+        , contract = add AllGATsValid
+        , {- For every GAT to be considered "valid", their
+             `TokenName`s have to be equal to the address
+             of their script. To represent this as a `Morphism`:
+
+             - FOR every UTXO input in the transaction:
+               - FOR every value in the input:
+                 - IF the currency symbol matches the recognised
+                   GAT currency symbol:
+                     - THEN: set the `TokenName` to be equal to
+                       the UTXO's address.
+                 - ELSE: ignore it.
+          -}
+          morphism = \m ->
+            let ctx' = m.ctx
+                txInfo = ctx'.scriptContextTxInfo
+                infoInputs :: [TxInInfo] = txInfo.txInfoInputs
+             in return $
+                  m
+                    { ctx =
+                        ctx'
+                          { scriptContextTxInfo =
+                              txInfo
+                                { txInfoInputs =
+                                    fixTokenNames <$> infoInputs
+                                }
+                          }
+                    }
+        }
+    , Morphism
+        { name = "Ensure script purpose is minting"
+        , match = Not $ Var ScriptPurposeIsMinting
+        , contract = add ScriptPurposeIsMinting
+        , morphism = \m ->
+            return
+              m
+                { ctx =
+                    m.ctx
+                      { scriptContextPurpose = Minting m.gatCs
+                      }
+                }
+        }
+    ]
 
 instance ScriptModel TreasuryTxProp TreasuryTxModel where
-  expect = undefined
-  script = undefined
+  expect :: (TreasuryTxModel :+ TreasuryTxProp) -> Formula TreasuryTxProp
+  expect _ =
+    Var GATIsBurned
+      :&&: Var AllGATsValid
+      :&&: Var ScriptPurposeIsMinting
+
+  script :: (TreasuryTxModel :+ TreasuryTxProp) -> TreasuryTxModel -> Script
+  script _ m = compile result
+    where
+      result :: Term s POpaque
+      result =
+        treasuryValidator cs
+          # (pforgetData $ pdata d)
+          # (pforgetData $ pdata r)
+          # ctx
+
+      cs :: CurrencySymbol
+      cs = m.gatCs
+
+      d :: Term s PTreasuryDatum
+      d = pcon $ PTreasuryDatum fields
+        where
+          adaStateThread :: Term _ PCurrencySymbol
+          adaStateThread = pconstant $ CurrencySymbol ""
+
+          fields :: Term _ (PDataRecord '["stateThread" ':= PCurrencySymbol])
+          fields = pdcons # (pdata adaStateThread) # pdnil
+
+      r :: Term s PTreasuryRedeemer
+      r = pcon $ PAlterTreasuryParams pdnil
+
+      ctx :: Term s PScriptContext
+      ctx = pconstant m.ctx
 
 genTests :: TestTree
 genTests =

agora/Agora/AuthorityToken.hs

@@ -69,30 +69,48 @@ newtype AuthorityToken = AuthorityToken
      are tagged with a TokenName that matches where they live.
 -}
 authorityTokensValidIn :: Term s (PCurrencySymbol :--> PTxOut :--> PBool)
-authorityTokensValidIn = phoistAcyclic $
+authorityTokensValidIn = phoistAcyclic $ -- /Lift/ the `Term`.
   plam $ \authorityTokenSym txOut'' -> P.do
+    -- Extract the desired fields: address and value, from the
+    -- transaction output info.
     PTxOut txOut' <- pmatch txOut''
     txOut <- pletFields @'["address", "value"] $ txOut'
     PAddress address <- pmatch txOut.address
     PValue value' <- pmatch txOut.value
     PMap value <- pmatch value'
+
+    -- Search the transaction output info's value for the
+    -- provided currency symbol for the authority token.
     pmatch (plookup # pdata authorityTokenSym # value) $ \case
+      -- In the case of `PNothing`, no GATs exist at this output
+      -- and ipso facto they are all valid.
+      PNothing -> pconstant True
+      -- This is the case wherein a TokenName/Integer map /has/
+      -- been found for the given currency symbol.
       PJust (pfromData -> tokenMap') ->
+        -- Now we need to look at the transaction output's
+        -- address.
         pmatch (pfield @"credential" # address) $ \case
-          PPubKeyCredential _ ->
-            -- GATs should only be sent to Effect validators
-            pconstant False
+          -- GATs should only be sent to Effect validators,
+          -- therefore we consider this invalid and return False.
+          PPubKeyCredential _ -> pconstant False
+          -- This is a script address. We need to ensure that
+          -- the the `TokenName`s associated with the given
+          -- currency symbol are all equal to this script
+          -- address.
           PScriptCredential ((pfromData . (pfield @"_0" #)) -> cred) -> P.do
+            -- Unwrap the `TokenName`/`Integer` map.
             PMap tokenMap <- pmatch tokenMap'
+
+            -- Check that the `TokenName` is equal to the validator
+            -- hash for all of the `TokenName` keys in the map.
             pall
               # plam
-                ( \pair ->
-                    pforgetData (pfstBuiltin # pair) #== pforgetData (pdata cred)
+                ( \tnMap ->
+                    pforgetData (pfstBuiltin # tnMap)
+                      #== pforgetData (pdata cred)
                 )
               # tokenMap
-      PNothing ->
-        -- No GATs exist at this output!
-        pconstant True
 
 -- | Assert that a single authority token has been burned.
 singleAuthorityTokenBurned ::

agora/Agora/Treasury.hs

@@ -57,7 +57,8 @@ treasuryValidator gatCs' = plam $ \datum redeemer ctx' -> P.do
 
   gatCs <- plet $ pconstant gatCs'
 
-  passert "A single authority token has been burned" $ singleAuthorityTokenBurned gatCs txInfo' mint
+  passert "A single authority token has been burned" $
+    singleAuthorityTokenBurned gatCs txInfo' mint
 
   popaque $ pconstant ()
 

flake.lock

@@ -103,17 +103,17 @@
         "plutus": "plutus"
       },
       "locked": {
-        "lastModified": 1649421738,
-        "narHash": "sha256-07LdyHykRDObI984W04lIXgvh6sWKDEW8enAGhIijQU=",
+        "lastModified": 1649673880,
+        "narHash": "sha256-LpR+F+fHB6Mh1NHI2O+3zeeSE+ZzyVBwuP9T12X3rek=",
         "owner": "mlabs-haskell",
         "repo": "apropos-tx",
-        "rev": "5257325e3dd2603d09c0ebe468eec676eeb233b8",
+        "rev": "dd292b49a29f8a259bdc3e35cf4ab1dbbc73582f",
         "type": "github"
       },
       "original": {
         "owner": "mlabs-haskell",
         "repo": "apropos-tx",
-        "rev": "5257325e3dd2603d09c0ebe468eec676eeb233b8",
+        "rev": "dd292b49a29f8a259bdc3e35cf4ab1dbbc73582f",
         "type": "github"
       }
     },

flake.nix

@@ -19,7 +19,7 @@
   # inputs to follow a commit on those master branches. For more
   # info, see: https://github.com/mlabs-haskell/apropos-tx/pull/37
   inputs.apropos-tx.url =
-    "github:mlabs-haskell/apropos-tx?rev=5257325e3dd2603d09c0ebe468eec676eeb233b8";
+    "github:mlabs-haskell/apropos-tx?rev=dd292b49a29f8a259bdc3e35cf4ab1dbbc73582f";
   inputs.apropos-tx.inputs.nixpkgs.follows =
     "plutarch/haskell-nix/nixpkgs-unstable";
   inputs.apropos.url =