add authorityTokensValidIn function

src/Agora/AuthorityToken.hs

@@ -7,16 +7,23 @@ Tokens acting as redeemable proofs of DAO authority.
 -}
 module Agora.AuthorityToken (
   authorityTokenPolicy,
+  authorityTokensValidIn,
   AuthorityToken (..),
 ) where
 
 import Plutarch.Api.V1 (
+  PAddress (..),
+  PCredential (..),
+  PCurrencySymbol (..),
+  PMap (..),
   PScriptContext (..),
   PScriptPurpose (..),
   PTxInInfo (..),
   PTxInfo (..),
   PTxOut (..),
+  PValue (..),
  )
+import Plutarch.Builtin (pforgetData)
 import Plutarch.List (pfoldr')
 import Plutarch.Monadic qualified as P
 import Plutus.V1.Ledger.Value (AssetClass)
@@ -25,7 +32,7 @@ import Prelude
 
 --------------------------------------------------------------------------------
 
-import Agora.Utils (passert, passetClassValueOf, passetClassValueOf')
+import Agora.Utils (passert, passetClassValueOf, passetClassValueOf', plookup)
 
 --------------------------------------------------------------------------------
 
@@ -42,6 +49,41 @@ newtype AuthorityToken = AuthorityToken
 
 --------------------------------------------------------------------------------
 
+{- | Check that all GATs are valid in a particular TxOut.
+     How this is checked: an AuthorityToken should never leave
+     the Effect it was initially sent to, so we simply check that
+     the script address the token resides in matches the TokenName.
+     Since the TokenName was tagged upon mint with the Effect script
+     it was sent to, this is enough to prove validity.
+
+     In other words, check that all assets of a particular currency symbol
+     are tagged with a TokenName that matches where they live.
+-}
+authorityTokensValidIn :: Term s (PCurrencySymbol :--> PTxOut :--> PBool)
+authorityTokensValidIn = phoistAcyclic $
+  plam $ \authorityTokenSym txOut'' -> P.do
+    PTxOut txOut' <- pmatch txOut''
+    txOut <- pletFields @'["address", "value"] $ txOut'
+    PAddress address <- pmatch txOut.address
+    PValue value' <- pmatch txOut.value
+    PMap value <- pmatch value'
+    pmatch (plookup # pdata authorityTokenSym # value) $ \case
+      PJust (pfromData -> tokenMap') ->
+        pmatch (pfield @"credential" # address) $ \case
+          PPubKeyCredential _ ->
+            -- GATs should only be sent to Effect validators
+            pconstant False
+          PScriptCredential ((pfromData . (pfield @"_0" #)) -> cred) -> P.do
+            PMap tokenMap <- pmatch tokenMap'
+            pall
+              # ( plam $ \pair ->
+                    pforgetData (pfstBuiltin # pair) #== pforgetData (pdata cred)
+                )
+              # tokenMap
+      PNothing ->
+        -- No GATs exist at this output!
+        pconstant True
+
 -- | Policy given 'AuthorityToken' params.
 authorityTokenPolicy ::
   AuthorityToken ->

src/Agora/Treasury.hs

@@ -8,7 +8,7 @@ treasury.
 -}
 module Agora.Treasury (module Agora.Treasury) where
 
-import Agora.Utils (passetClassValueOf)
+import Agora.Utils (passert, passetClassValueOf)
 import GHC.Generics qualified as GHC
 import Generics.SOP
 import Plutarch.Api.V1.Contexts (PScriptContext, PScriptPurpose (PMinting))
@@ -52,10 +52,9 @@ treasuryV cs tn = plam $ \_d r ctx' -> P.do
       gatAmountMinted :: Term s PInteger
       gatAmountMinted = passetClassValueOf # pconstant cs # pconstant tn # mint
 
-  pif
+  passert "GAT not burned." $ gatAmountMinted #== -1
-    (gatAmountMinted #== -1) -- If the amount of GATS burned is not one, ...
+
-    (ptraceError "GAT not burned.") -- ... then error.
+  pconstant ()
-    (pconstant ()) -- ... else success.
 
 {- | Plutarch level type representing datum of the treasury.
      Contains: