disallow minting new GATs while burning

Co-authored-by: Hongrui Fang <chfanghr@gmail.com>

agora/Agora/AuthorityToken.hs

@@ -11,6 +11,11 @@ module Agora.AuthorityToken (
   singleAuthorityTokenBurned,
 ) where
 
+import Agora.Utils (
+  passert,
+  pnegativeSymbolValueOf,
+  ppositiveSymbolValueOf,
+ )
 import Plutarch.Api.V1 (
   PCredential (..),
   PCurrencySymbol (..),
@@ -32,7 +37,12 @@ import Plutarch.Extra.AssetClass (PAssetClassData, ptoScottEncoding)
 import "liqwid-plutarch-extra" Plutarch.Extra.List (plookupAssoc)
 import Plutarch.Extra.ScriptContext (pisTokenSpent)
 import Plutarch.Extra.Sum (PSum (PSum))
-import "liqwid-plutarch-extra" Plutarch.Extra.TermCont (pguardC, pletC, pletFieldsC, pmatchC)
+import "liqwid-plutarch-extra" Plutarch.Extra.TermCont (
+  pguardC,
+  pletC,
+  pletFieldsC,
+  pmatchC,
+ )
 import Plutarch.Extra.Traversable (pfoldMap)
 import Plutarch.Extra.Value (psymbolValueOf)
 
@@ -144,27 +154,29 @@ authorityTokenPolicy =
       PTxInfo txInfo' <- pmatchC $ pfromData ctx.txInfo
       txInfo <- pletFieldsC @'["inputs", "mint", "outputs"] txInfo'
       let inputs = txInfo.inputs
-          mintedValue = pfromData txInfo.mint
           govTokenSpent = pisTokenSpent # (ptoScottEncoding # atAssetClass) # inputs
 
       PMinting ownSymbol' <- pmatchC $ pfromData ctx.purpose
 
       let ownSymbol = pfromData $ pfield @"_0" # ownSymbol'
-          mintedATs =
+
-            psymbolValueOf
+      applySymbolValueOf <- pletC $ plam $ \f -> f # ownSymbol # txInfo.mint
-              # ownSymbol
+
-              # mintedValue
+      mintedATs <- pletC $ applySymbolValueOf # ppositiveSymbolValueOf
+      let burntATs = applySymbolValueOf # pnegativeSymbolValueOf
 
       pure $
+        popaque $
           pif
             (0 #< mintedATs)
             ( unTermCont $ do
+                pguardC "No GAT burnt" $ 0 #== burntATs
                 pguardC "Parent token did not move in minting GATs" govTokenSpent
                 pguardC "All outputs only emit valid GATs" $
                   pall
                     # plam
                       (authorityTokensValidIn # ownSymbol #)
                     # txInfo.outputs
-              pure $ popaque $ pconstant ()
+                pure $ pconstant ()
             )
-          (popaque $ pconstant ())
+            (passert "No GAT minted" (0 #== mintedATs) (pconstant ()))

agora/Agora/Utils.hs

@@ -33,16 +33,34 @@ module Agora.Utils (
   passert,
   pisNothing,
   pisDNothing,
+  ppositiveSymbolValueOf,
+  pnegativeSymbolValueOf,
 ) where
 
-import Plutarch.Api.V1 (KeyGuarantees (Unsorted), PPOSIXTime, PRedeemer, PTokenName, PValidatorHash)
+import Plutarch.Api.V1 (
+  KeyGuarantees (Unsorted),
+  PPOSIXTime,
+  PRedeemer,
+  PTokenName,
+  PValidatorHash,
+ )
 import Plutarch.Api.V1.AssocMap (PMap, plookup)
-import Plutarch.Api.V2 (PMaybeData (PDNothing), PScriptHash, PScriptPurpose)
+import Plutarch.Api.V2 (
+  AmountGuarantees,
+  PCurrencySymbol,
+  PMap (PMap),
+  PMaybeData (PDNothing),
+  PScriptHash,
+  PScriptPurpose,
+  PValue (PValue),
+ )
 import Plutarch.Extra.Applicative (PApplicative (ppure))
 import Plutarch.Extra.Category (PCategory (pidentity))
 import Plutarch.Extra.Functor (PFunctor (PSubcategory, pfmap))
-import Plutarch.Extra.Maybe (pjust, pnothing)
+import "liqwid-plutarch-extra" Plutarch.Extra.List (plookupAssoc)
+import Plutarch.Extra.Maybe (pexpectJustC, pjust, pnothing)
 import Plutarch.Extra.Ord (PComparator, POrdering (PLT), pcompareBy, pequateBy)
+import "liqwid-plutarch-extra" Plutarch.Extra.TermCont (pmatchC)
 import Plutarch.Extra.Time (PCurrentTime (PCurrentTime))
 import Plutarch.Unsafe (punsafeCoerce)
 import PlutusLedgerApi.V2 (
@@ -407,3 +425,68 @@ pisDNothing = phoistAcyclic $
     flip pmatch $ \case
       PDNothing _ -> pconstant True
       _ -> pconstant False
+
+psymbolValueOfHelper ::
+  forall
+    (keys :: KeyGuarantees)
+    (amounts :: AmountGuarantees)
+    (s :: S).
+  Term
+    s
+    ( (PInteger :--> PBool)
+        :--> PCurrencySymbol
+        :--> ( PValue keys amounts
+                :--> PInteger
+             )
+    )
+psymbolValueOfHelper =
+  phoistAcyclic $
+    plam $ \cond sym value'' -> unTermCont $ do
+      PValue value' <- pmatchC value''
+      PMap value <- pmatchC value'
+      m' <-
+        pexpectJustC
+          0
+          ( plookupAssoc
+              # pfstBuiltin
+              # psndBuiltin
+              # pdata sym
+              # value
+          )
+      PMap m <- pmatchC (pfromData m')
+      pure $
+        pfoldr
+          # plam
+            ( \x v ->
+                plet (pfromData $ psndBuiltin # x) $ \q ->
+                  pif
+                    (cond # q)
+                    (q + v)
+                    v
+            )
+          # 0
+          # m
+
+{- | The sum of positive entries belonging to a particular currency symbol.
+
+   @since 1.0.0
+-}
+ppositiveSymbolValueOf ::
+  forall
+    (keys :: KeyGuarantees)
+    (amounts :: AmountGuarantees)
+    (s :: S).
+  Term s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger))
+ppositiveSymbolValueOf = phoistAcyclic $ psymbolValueOfHelper #$ plam (0 #<)
+
+{- | The sum of negative entries belonging to a particular currency symbol.
+
+   @since 1.0.0
+-}
+pnegativeSymbolValueOf ::
+  forall
+    (keys :: KeyGuarantees)
+    (amounts :: AmountGuarantees)
+    (s :: S).
+  Term s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger))
+pnegativeSymbolValueOf = phoistAcyclic $ psymbolValueOfHelper #$ plam (#< 0)