check that all GATs burned in treasury validator are valid

src/Agora/AuthorityToken.hs

@@ -32,7 +32,7 @@ import Prelude
 
 --------------------------------------------------------------------------------
 
-import Agora.Utils (passert, passetClassValueOf, passetClassValueOf', plookup)
+import Agora.Utils (allOutputs, passert, passetClassValueOf, passetClassValueOf', plookup)
 
 --------------------------------------------------------------------------------
 
@@ -113,5 +113,13 @@ authorityTokenPolicy params =
       let mintedATs = passetClassValueOf # ownSymbol # pconstant "" # mintedValue
       pif
         (0 #< mintedATs)
-        (passert "Authority token did not move in minting GATs" tokenMoved (pconstant ()))
+        ( P.do
+            passert "Parent token did not move in minting GATs" tokenMoved
+            passert "All outputs only emit valid GATs" $
+              allOutputs @PUnit # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
+                authorityTokensValidIn
+                  # ownSymbol
+                  # txOut
+            pconstant ()
+        )
         (pconstant ())

src/Agora/Treasury.hs

@@ -8,7 +8,6 @@ treasury.
 -}
 module Agora.Treasury (module Agora.Treasury) where
 
-import Agora.Utils (passert, passetClassValueOf)
 import GHC.Generics qualified as GHC
 import Generics.SOP
 import Plutarch.Api.V1.Contexts (PScriptContext, PScriptPurpose (PMinting))
@@ -18,7 +17,12 @@ import Plutarch.DataRepr (
   PIsDataReprInstances (PIsDataReprInstances),
  )
 import Plutarch.Monadic qualified as P
-import Plutus.V1.Ledger.Value (CurrencySymbol, TokenName)
+import Plutus.V1.Ledger.Value (CurrencySymbol)
+
+--------------------------------------------------------------------------------
+
+import Agora.AuthorityToken (authorityTokensValidIn)
+import Agora.Utils (allInputs, passert, psymbolValueOf)
 
 {- | Validator ensuring that transactions consuming the treasury
      do so in a valid manner.
@@ -26,7 +30,6 @@ import Plutus.V1.Ledger.Value (CurrencySymbol, TokenName)
 treasuryV ::
   forall {s :: S}.
   CurrencySymbol ->
-  TokenName ->
   Term
     s
     ( PAsData PTreasuryDatum
@@ -34,7 +37,7 @@ treasuryV ::
         :--> PAsData PScriptContext
         :--> PUnit
     )
-treasuryV cs tn = plam $ \_d r ctx' -> P.do
+treasuryV cs = plam $ \_d r ctx' -> P.do
   -- plet required fields from script context.
   ctx <- pletFields @["txInfo", "purpose"] ctx'
 
@@ -50,10 +53,16 @@ treasuryV cs tn = plam $ \_d r ctx' -> P.do
   let mint :: Term s PValue
       mint = txInfo.mint
       gatAmountMinted :: Term s PInteger
-      gatAmountMinted = passetClassValueOf # pconstant cs # pconstant tn # mint
+      gatAmountMinted = psymbolValueOf # pconstant cs # mint
 
   passert "GAT not burned." $ gatAmountMinted #== -1
 
+  passert "All inputs only have valid GATs" $
+    allInputs @PUnit # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
+      authorityTokensValidIn
+        # pconstant cs
+        # txOut
+
   pconstant ()
 
 {- | Plutarch level type representing datum of the treasury.

src/Agora/Utils.hs

@@ -25,7 +25,9 @@ module Agora.Utils (
 
   -- * Functions which should (probably) not be upstreamed
   anyOutput,
+  allOutputs,
   anyInput,
+  allInputs,
 ) where
 
 --------------------------------------------------------------------------------
@@ -256,7 +258,9 @@ pfindTxInByTxOutRef = phoistAcyclic $
         #$ (pfield @"inputs" # txInfo)
 
 --------------------------------------------------------------------------------
--- Functions which should (probably) not be upstreamed
+{- Functions which should (probably) not be upstreamed
+   All of these functions are quite inefficient.
+-}
 
 -- | Check if any output matches the predicate.
 anyOutput ::
@@ -280,6 +284,28 @@ anyOutput = phoistAcyclic $
         )
       # pfromData txInfo.outputs
 
+-- | Check if all outputs match the predicate.
+allOutputs ::
+  forall (datum :: PType) s.
+  ( PIsData datum
+  ) =>
+  Term s (PTxInfo :--> (PTxOut :--> PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
+allOutputs = phoistAcyclic $
+  plam $ \txInfo' predicate -> P.do
+    txInfo <- pletFields @'["outputs"] txInfo'
+    pall
+      # plam
+        ( \txOut'' -> P.do
+            PTxOut txOut' <- pmatch (pfromData txOut'')
+            txOut <- pletFields @'["value", "datumHash", "address"] txOut'
+            PDJust dh <- pmatch txOut.datumHash
+            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case
+              PJust datum -> P.do
+                predicate # (pfromData txOut'') # txOut.value # txOut.address # pfromData datum
+              PNothing -> pcon PFalse
+        )
+      # pfromData txInfo.outputs
+
 -- | Check if any (resolved) input matches the predicate.
 anyInput ::
   forall (datum :: PType) s.
@@ -304,6 +330,30 @@ anyInput = phoistAcyclic $
         )
       # pfromData txInfo.inputs
 
+-- | Check if all (resolved) inputs match the predicate.
+allInputs ::
+  forall (datum :: PType) s.
+  ( PIsData datum
+  ) =>
+  Term s (PTxInfo :--> (PTxOut :--> PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
+allInputs = phoistAcyclic $
+  plam $ \txInfo' predicate -> P.do
+    txInfo <- pletFields @'["inputs"] txInfo'
+    pall
+      # plam
+        ( \txInInfo'' -> P.do
+            PTxInInfo txInInfo' <- pmatch (pfromData txInInfo'')
+            let txOut'' = pfield @"resolved" # txInInfo'
+            PTxOut txOut' <- pmatch (pfromData txOut'')
+            txOut <- pletFields @'["value", "datumHash", "address"] txOut'
+            PDJust dh <- pmatch txOut.datumHash
+            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case
+              PJust datum -> P.do
+                predicate # pfromData txOut'' # txOut.value # txOut.address # pfromData datum
+              PNothing -> pcon PFalse
+        )
+      # pfromData txInfo.inputs
+
 -- | Create a value with a single asset class.
 psingletonValue :: forall s. Term s (PCurrencySymbol :--> PTokenName :--> PInteger :--> PValue)
 psingletonValue = phoistAcyclic $