{- |
Module     : Agora.AuthorityToken
Maintainer : emi@haskell.fyi
Description: Tokens acting as redeemable proofs of DAO authority.

Tokens acting as redeemable proofs of DAO authority.
-}
module Agora.AuthorityToken (
  authorityTokenPolicy,
  authorityTokensValidIn,
  singleAuthorityTokenBurned,
  AuthorityToken (..),
) where

import GHC.Generics qualified as GHC
import Plutarch.Api.V1 (
  AmountGuarantees,
  KeyGuarantees,
  PAddress (..),
  PCredential (..),
  PCurrencySymbol (..),
  PMintingPolicy,
  PScriptContext (..),
  PScriptPurpose (..),
  PTxInInfo (PTxInInfo),
  PTxInfo (..),
  PTxOut (..),
 )
import Plutarch.Api.V1.AssetClass (passetClass, passetClassValueOf)
import Plutarch.Api.V1.AssocMap (PMap (PMap))
import Plutarch.Api.V1.ScriptContext (pisTokenSpent)
import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (psymbolValueOf)
import "plutarch" Plutarch.Api.V1.Value (PValue (PValue))
import Plutarch.Builtin (pforgetData)
import Plutarch.Extra.List (plookup)
import Plutarch.Extra.TermCont (pguardC, pmatchC)
import PlutusLedgerApi.V1.Value (AssetClass (AssetClass))

--------------------------------------------------------------------------------

{- | An AuthorityToken represents a proof that a particular token
     spent in the same transaction the AuthorityToken was minted.
     In effect, this means that the validator that locked such a token
     must have approved the transaction in which an AuthorityToken is minted.
     Said validator should be made aware of an AuthorityToken token's existence
     in order to prevent incorrect minting.

     @since 0.1.0
-}
newtype AuthorityToken = AuthorityToken
  { AuthorityToken -> AssetClass
authority :: AssetClass
  -- ^ Token that must move in order for minting this to be valid.
  }
  deriving stock
    ( -- | @since 0.1.0
      (forall x. AuthorityToken -> Rep AuthorityToken x)
-> (forall x. Rep AuthorityToken x -> AuthorityToken)
-> Generic AuthorityToken
forall x. Rep AuthorityToken x -> AuthorityToken
forall x. AuthorityToken -> Rep AuthorityToken x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep AuthorityToken x -> AuthorityToken
$cfrom :: forall x. AuthorityToken -> Rep AuthorityToken x
GHC.Generic
    )

--------------------------------------------------------------------------------

{- | 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.

     @since 0.1.0
-}
authorityTokensValidIn :: Term s (PCurrencySymbol :--> PTxOut :--> PBool)
authorityTokensValidIn :: forall (s :: S). Term s (PCurrencySymbol :--> (PTxOut :--> PBool))
authorityTokensValidIn = (forall (s :: S).
 Term s (PCurrencySymbol :--> (PTxOut :--> PBool)))
-> Term s (PCurrencySymbol :--> (PTxOut :--> PBool))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S).
  Term s (PCurrencySymbol :--> (PTxOut :--> PBool)))
 -> Term s (PCurrencySymbol :--> (PTxOut :--> PBool)))
-> (forall (s :: S).
    Term s (PCurrencySymbol :--> (PTxOut :--> PBool)))
-> Term s (PCurrencySymbol :--> (PTxOut :--> PBool))
forall a b. (a -> b) -> a -> b
$
  (Term s PCurrencySymbol -> Term s PTxOut -> Term s PBool)
-> Term s (PCurrencySymbol :--> (PTxOut :--> PBool))
forall a (b :: PType) (s :: S) (c :: PType).
PLamN a b s =>
(Term s c -> a) -> Term s (c :--> b)
plam ((Term s PCurrencySymbol -> Term s PTxOut -> Term s PBool)
 -> Term s (PCurrencySymbol :--> (PTxOut :--> PBool)))
-> (Term s PCurrencySymbol -> Term s PTxOut -> Term s PBool)
-> Term s (PCurrencySymbol :--> (PTxOut :--> PBool))
forall a b. (a -> b) -> a -> b
$ \Term s PCurrencySymbol
authorityTokenSym Term s PTxOut
txOut'' -> TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
    PTxOut Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("address" ':= PAddress)
        ((':)
           @PLabeledType
           ("value" ':= PValue 'Sorted 'Positive)
           ((':)
              @PLabeledType
              ("datumHash" ':= PMaybeData PDatumHash)
              ('[] @PLabeledType)))))
txOut' <- Term s PTxOut -> TermCont @PBool s (PTxOut s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC Term s PTxOut
txOut''
    HRec
  ((':)
     @(Symbol, Type)
     '("address", Term s (PAsData PAddress))
     ((':)
        @(Symbol, Type)
        '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
        ('[] @(Symbol, Type))))
txOut <- ((HRec
    ((':)
       @(Symbol, Type)
       '("address", Term s (PAsData PAddress))
       ((':)
          @(Symbol, Type)
          '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
          ('[] @(Symbol, Type))))
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("address", Term s (PAsData PAddress))
           ((':)
              @(Symbol, Type)
              '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
              ('[] @(Symbol, Type)))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("address", Term s (PAsData PAddress))
        ((':)
           @(Symbol, Type)
           '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
           ('[] @(Symbol, Type))))
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("address", Term s (PAsData PAddress))
            ((':)
               @(Symbol, Type)
               '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
               ('[] @(Symbol, Type))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("address", Term s (PAsData PAddress))
          ((':)
             @(Symbol, Type)
             '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
             ('[] @(Symbol, Type))))
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("address", Term s (PAsData PAddress))
           ((':)
              @(Symbol, Type)
              '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
              ('[] @(Symbol, Type)))))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["address", "value"] (Term
   s
   (PDataRecord
      ((':)
         @PLabeledType
         ("address" ':= PAddress)
         ((':)
            @PLabeledType
            ("value" ':= PValue 'Sorted 'Positive)
            ((':)
               @PLabeledType
               ("datumHash" ':= PMaybeData PDatumHash)
               ('[] @PLabeledType)))))
 -> (HRecOf
       (PDataRecord
          ((':)
             @PLabeledType
             ("address" ':= PAddress)
             ((':)
                @PLabeledType
                ("value" ':= PValue 'Sorted 'Positive)
                ((':)
                   @PLabeledType
                   ("datumHash" ':= PMaybeData PDatumHash)
                   ('[] @PLabeledType)))))
       ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol)))
       s
     -> Term s PBool)
 -> Term s PBool)
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           ("address" ':= PAddress)
           ((':)
              @PLabeledType
              ("value" ':= PValue 'Sorted 'Positive)
              ((':)
                 @PLabeledType
                 ("datumHash" ':= PMaybeData PDatumHash)
                 ('[] @PLabeledType)))))
-> (HRecOf
      (PDataRecord
         ((':)
            @PLabeledType
            ("address" ':= PAddress)
            ((':)
               @PLabeledType
               ("value" ':= PValue 'Sorted 'Positive)
               ((':)
                  @PLabeledType
                  ("datumHash" ':= PMaybeData PDatumHash)
                  ('[] @PLabeledType)))))
      ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol)))
      s
    -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("address" ':= PAddress)
        ((':)
           @PLabeledType
           ("value" ':= PValue 'Sorted 'Positive)
           ((':)
              @PLabeledType
              ("datumHash" ':= PMaybeData PDatumHash)
              ('[] @PLabeledType)))))
txOut'
    PAddress Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("credential" ':= PCredential)
        ((':)
           @PLabeledType
           ("stakingCredential" ':= PMaybeData PStakingCredential)
           ('[] @PLabeledType))))
address <- Term s PAddress -> TermCont @PBool s (PAddress s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC HRec
  ((':)
     @(Symbol, Type)
     '("address", Term s (PAsData PAddress))
     ((':)
        @(Symbol, Type)
        '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
        ('[] @(Symbol, Type))))
txOut.address
    PValue Term
  s
  (PMap
     'Sorted PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S)))
value' <- Term s (PValue 'Sorted 'Positive)
-> TermCont @PBool s (PValue 'Sorted 'Positive s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC HRec
  ((':)
     @(Symbol, Type)
     '("address", Term s (PAsData PAddress))
     ((':)
        @(Symbol, Type)
        '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
        ('[] @(Symbol, Type))))
txOut.value
    PMap Term
  s
  (PBuiltinMap
     PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S)))
value <- Term
  s
  (PMap
     'Sorted PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S)))
-> TermCont
     @PBool
     s
     (PMap
        'Sorted PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S)) s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC Term
  s
  (PMap
     'Sorted PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S)))
value'
    Term s PBool -> TermCont @PBool s (Term s PBool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
      Term s (PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S))))
-> (PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S))) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PMatch a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term
  s
  (PAsData PCurrencySymbol
   :--> (PBuiltinMap
           PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S))
         :--> PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S)))))
forall (a :: PType) (b :: PType) (s :: S) (list :: PType -> PType).
(PEq a, PIsListLike list (PBuiltinPair a b)) =>
Term s (a :--> (list (PBuiltinPair a b) :--> PMaybe b))
plookup Term
  s
  (PAsData PCurrencySymbol
   :--> (PBuiltinMap
           PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S))
         :--> PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S)))))
-> Term s (PAsData PCurrencySymbol)
-> Term
     s
     (PBuiltinMap
        PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S))
      :--> PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S))))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol -> Term s (PAsData PCurrencySymbol)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PCurrencySymbol
authorityTokenSym Term
  s
  (PBuiltinMap
     PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S))
   :--> PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S))))
-> Term
     s
     (PBuiltinMap
        PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S)))
-> Term
     s (PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S))))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinMap
     PCurrencySymbol (PMap 'Sorted PTokenName (PInteger @S)))
value) ((PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S))) s
  -> Term s PBool)
 -> Term s PBool)
-> (PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S))) s
    -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
        PJust (Term s (PAsData (PMap 'Sorted PTokenName (PInteger @S)))
-> Term s (PMap 'Sorted PTokenName (PInteger @S))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData -> Term s (PMap 'Sorted PTokenName (PInteger @S))
tokenMap') ->
          Term s PCredential
-> (PCredential s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PMatch a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"credential" Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("credential" ':= PCredential)
        ((':)
           @PLabeledType
           ("stakingCredential" ':= PMaybeData PStakingCredential)
           ('[] @PLabeledType)))
   :--> PCredential)
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           ("credential" ':= PCredential)
           ((':)
              @PLabeledType
              ("stakingCredential" ':= PMaybeData PStakingCredential)
              ('[] @PLabeledType))))
-> Term s PCredential
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("credential" ':= PCredential)
        ((':)
           @PLabeledType
           ("stakingCredential" ':= PMaybeData PStakingCredential)
           ('[] @PLabeledType))))
address) ((PCredential s -> Term s PBool) -> Term s PBool)
-> (PCredential s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
            PPubKeyCredential Term
  s
  (PDataRecord
     ((':) @PLabeledType ("_0" ':= PPubKeyHash) ('[] @PLabeledType)))
_ ->
              -- GATs should only be sent to Effect validators
              Term s (PString @S) -> Term s PBool -> Term s PBool
forall (s :: S).
Term s (PString @S) -> Term s PBool -> Term s PBool
ptraceIfFalse Term s (PString @S)
"authorityTokensValidIn: GAT incorrectly lives at PubKey" (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ PLifted PBool -> Term s PBool
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
PLifted PBool
False
            PScriptCredential ((Term s (PAsData PValidatorHash) -> Term s PValidatorHash
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PValidatorHash) -> Term s PValidatorHash)
-> (Term
      s
      (PDataRecord
         ((':) @PLabeledType ("_0" ':= PValidatorHash) ('[] @PLabeledType)))
    -> Term s (PAsData PValidatorHash))
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType ("_0" ':= PValidatorHash) ('[] @PLabeledType)))
-> Term s PValidatorHash
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" #)) -> Term s PValidatorHash
cred) -> TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
              PMap Term s (PBuiltinMap PTokenName (PInteger @S))
tokenMap <- Term s (PMap 'Sorted PTokenName (PInteger @S))
-> TermCont @PBool s (PMap 'Sorted PTokenName (PInteger @S) s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC Term s (PMap 'Sorted PTokenName (PInteger @S))
tokenMap'
              Term s PBool -> TermCont @PBool s (Term s PBool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
                Term s (PString @S) -> Term s PBool -> Term s PBool
forall (s :: S).
Term s (PString @S) -> Term s PBool -> Term s PBool
ptraceIfFalse Term s (PString @S)
"authorityTokensValidIn: GAT TokenName doesn't match ScriptHash" (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$
                  Term
  s
  ((PBuiltinPair (PAsData PTokenName) (PAsData (PInteger @S))
    :--> PBool)
   :--> (PBuiltinMap PTokenName (PInteger @S) :--> PBool))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pall
                    # plam
                      ( \pair ->
                          pforgetData (pfstBuiltin # pair) #== pforgetData (pdata cred)
                      )
                    # tokenMap
        PMaybe (PAsData (PMap 'Sorted PTokenName (PInteger @S))) s
PNothing ->
          -- No GATs exist at this output!
          PLifted PBool -> Term s PBool
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Bool
PLifted PBool
True

{- | Assert that a single authority token has been burned.

     @since 0.1.0
-}
singleAuthorityTokenBurned ::
  forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees) (s :: S).
  Term s PCurrencySymbol ->
  Term s (PAsData PTxInfo) ->
  Term s (PValue keys amounts) ->
  Term s PBool
singleAuthorityTokenBurned :: forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term s PCurrencySymbol
-> Term s (PAsData PTxInfo)
-> Term s (PValue keys amounts)
-> Term s PBool
singleAuthorityTokenBurned Term s PCurrencySymbol
gatCs Term s (PAsData PTxInfo)
txInfo Term s (PValue keys amounts)
mint = TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
  let gatAmountMinted :: Term _ PInteger
      gatAmountMinted :: Term s (PInteger @S)
gatAmountMinted = Term
  s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger @S))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term
  s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger @S))
psymbolValueOf Term
  s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger @S))
-> Term s PCurrencySymbol
-> Term s (PValue keys amounts :--> PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
gatCs Term s (PValue keys amounts :--> PInteger @S)
-> Term s (PValue keys amounts) -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PValue keys amounts)
mint

  HRec
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ('[] @(Symbol, Type)))
txInfoF <- ((HRec
    ((':)
       @(Symbol, Type)
       '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
       ('[] @(Symbol, Type)))
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
           ('[] @(Symbol, Type))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
        ('[] @(Symbol, Type)))
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
            ('[] @(Symbol, Type)))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
          ('[] @(Symbol, Type)))
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
           ('[] @(Symbol, Type))))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["inputs"] (Term s (PAsData PTxInfo)
 -> (HRecOf
       (PAsData PTxInfo) ((':) @Symbol "inputs" ('[] @Symbol)) s
     -> Term s PBool)
 -> Term s PBool)
-> Term s (PAsData PTxInfo)
-> (HRecOf
      (PAsData PTxInfo) ((':) @Symbol "inputs" ('[] @Symbol)) s
    -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PTxInfo)
txInfo

  Term s PBool -> TermCont @PBool s (Term s PBool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
    (Term s PBool -> Term s PBool -> Term s PBool)
-> [Term s PBool] -> Term s PBool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1
      Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
(#&&)
      [ Term s (PString @S) -> Term s PBool -> Term s PBool
forall (s :: S).
Term s (PString @S) -> Term s PBool -> Term s PBool
ptraceIfFalse Term s (PString @S)
"singleAuthorityTokenBurned: Must burn exactly 1 GAT" (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PInteger @S)
gatAmountMinted Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== -Term s (PInteger @S)
1
      , Term s (PString @S) -> Term s PBool -> Term s PBool
forall (s :: S).
Term s (PString @S) -> Term s PBool -> Term s PBool
ptraceIfFalse Term s (PString @S)
"singleAuthorityTokenBurned: All GAT tokens must be valid at the inputs" (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$
          Term
  s
  ((PAsData PTxInInfo :--> PBool)
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pall
            # plam
              ( \txInInfo' -> unTermCont $ do
                  PTxInInfo txInInfo <- pmatchC (pfromData txInInfo')
                  let txOut' = pfield @"resolved" # txInInfo
                  pure $ authorityTokensValidIn # gatCs # pfromData txOut'
              )
            # txInfoF.inputs
      ]

{- | Policy given 'AuthorityToken' params.

     @since 0.1.0
-}
authorityTokenPolicy :: AuthorityToken -> ClosedTerm PMintingPolicy
authorityTokenPolicy :: AuthorityToken -> ClosedTerm PMintingPolicy
authorityTokenPolicy AuthorityToken
params =
  (Term s PData -> Term s PScriptContext -> Term s POpaque)
-> Term s PMintingPolicy
forall a (b :: PType) (s :: S) (c :: PType).
PLamN a b s =>
(Term s c -> a) -> Term s (c :--> b)
plam ((Term s PData -> Term s PScriptContext -> Term s POpaque)
 -> Term s PMintingPolicy)
-> (Term s PData -> Term s PScriptContext -> Term s POpaque)
-> Term s PMintingPolicy
forall a b. (a -> b) -> a -> b
$ \Term s PData
_redeemer Term s PScriptContext
ctx' ->
    Term s PScriptContext
-> (PScriptContext s -> Term s POpaque) -> Term s POpaque
forall (a :: PType) (s :: S) (b :: PType).
PMatch a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PScriptContext
ctx' ((PScriptContext s -> Term s POpaque) -> Term s POpaque)
-> (PScriptContext s -> Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ \(PScriptContext Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("txInfo" ':= PTxInfo)
        ((':)
           @PLabeledType ("purpose" ':= PScriptPurpose) ('[] @PLabeledType))))
ctx') -> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @POpaque s (Term s POpaque) -> Term s POpaque)
-> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ do
      HRec
  ((':)
     @(Symbol, Type)
     '("txInfo", Term s (PAsData PTxInfo))
     ((':)
        @(Symbol, Type)
        '("purpose", Term s (PAsData PScriptPurpose))
        ('[] @(Symbol, Type))))
ctx <- ((HRec
    ((':)
       @(Symbol, Type)
       '("txInfo", Term s (PAsData PTxInfo))
       ((':)
          @(Symbol, Type)
          '("purpose", Term s (PAsData PScriptPurpose))
          ('[] @(Symbol, Type))))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("txInfo", Term s (PAsData PTxInfo))
           ((':)
              @(Symbol, Type)
              '("purpose", Term s (PAsData PScriptPurpose))
              ('[] @(Symbol, Type)))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("txInfo", Term s (PAsData PTxInfo))
        ((':)
           @(Symbol, Type)
           '("purpose", Term s (PAsData PScriptPurpose))
           ('[] @(Symbol, Type))))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("txInfo", Term s (PAsData PTxInfo))
            ((':)
               @(Symbol, Type)
               '("purpose", Term s (PAsData PScriptPurpose))
               ('[] @(Symbol, Type))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("txInfo", Term s (PAsData PTxInfo))
          ((':)
             @(Symbol, Type)
             '("purpose", Term s (PAsData PScriptPurpose))
             ('[] @(Symbol, Type))))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("txInfo", Term s (PAsData PTxInfo))
           ((':)
              @(Symbol, Type)
              '("purpose", Term s (PAsData PScriptPurpose))
              ('[] @(Symbol, Type)))))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["txInfo", "purpose"] Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("txInfo" ':= PTxInfo)
        ((':)
           @PLabeledType ("purpose" ':= PScriptPurpose) ('[] @PLabeledType))))
ctx'
      PTxInfo Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("inputs" ':= PBuiltinList (PAsData PTxInInfo))
        ((':)
           @PLabeledType
           ("outputs" ':= PBuiltinList (PAsData PTxOut))
           ((':)
              @PLabeledType
              ("fee" ':= PValue 'Sorted 'Positive)
              ((':)
                 @PLabeledType
                 ("mint" ':= PValue 'Sorted 'NoGuarantees)
                 ((':)
                    @PLabeledType
                    ("dcert" ':= PBuiltinList (PAsData PDCert))
                    ((':)
                       @PLabeledType
                       ("wdrl"
                        ':= PBuiltinList
                              (PAsData (PTuple PStakingCredential (PInteger @S))))
                       ((':)
                          @PLabeledType
                          ("validRange" ':= PPOSIXTimeRange)
                          ((':)
                             @PLabeledType
                             ("signatories" ':= PBuiltinList (PAsData PPubKeyHash))
                             ((':)
                                @PLabeledType
                                ("datums" ':= PBuiltinList (PAsData (PTuple PDatumHash PDatum)))
                                ((':) @PLabeledType ("id" ':= PTxId) ('[] @PLabeledType))))))))))))
txInfo' <- Term s PTxInfo -> TermCont @POpaque s (PTxInfo s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC (Term s PTxInfo -> TermCont @POpaque s (PTxInfo s))
-> Term s PTxInfo -> TermCont @POpaque s (PTxInfo s)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PTxInfo) -> Term s PTxInfo
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData HRec
  ((':)
     @(Symbol, Type)
     '("txInfo", Term s (PAsData PTxInfo))
     ((':)
        @(Symbol, Type)
        '("purpose", Term s (PAsData PScriptPurpose))
        ('[] @(Symbol, Type))))
ctx.txInfo
      HRec
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ((':)
        @(Symbol, Type)
        '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
        ((':)
           @(Symbol, Type)
           '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
           ('[] @(Symbol, Type)))))
txInfo <- ((HRec
    ((':)
       @(Symbol, Type)
       '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
       ((':)
          @(Symbol, Type)
          '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
          ((':)
             @(Symbol, Type)
             '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
             ('[] @(Symbol, Type)))))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
           ((':)
              @(Symbol, Type)
              '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
              ((':)
                 @(Symbol, Type)
                 '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
                 ('[] @(Symbol, Type))))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
        ((':)
           @(Symbol, Type)
           '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
           ((':)
              @(Symbol, Type)
              '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
              ('[] @(Symbol, Type)))))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
            ((':)
               @(Symbol, Type)
               '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
               ((':)
                  @(Symbol, Type)
                  '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
                  ('[] @(Symbol, Type)))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
          ((':)
             @(Symbol, Type)
             '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
             ((':)
                @(Symbol, Type)
                '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
                ('[] @(Symbol, Type)))))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
           ((':)
              @(Symbol, Type)
              '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
              ((':)
                 @(Symbol, Type)
                 '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
                 ('[] @(Symbol, Type))))))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["inputs", "mint", "outputs"] Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("inputs" ':= PBuiltinList (PAsData PTxInInfo))
        ((':)
           @PLabeledType
           ("outputs" ':= PBuiltinList (PAsData PTxOut))
           ((':)
              @PLabeledType
              ("fee" ':= PValue 'Sorted 'Positive)
              ((':)
                 @PLabeledType
                 ("mint" ':= PValue 'Sorted 'NoGuarantees)
                 ((':)
                    @PLabeledType
                    ("dcert" ':= PBuiltinList (PAsData PDCert))
                    ((':)
                       @PLabeledType
                       ("wdrl"
                        ':= PBuiltinList
                              (PAsData (PTuple PStakingCredential (PInteger @S))))
                       ((':)
                          @PLabeledType
                          ("validRange" ':= PPOSIXTimeRange)
                          ((':)
                             @PLabeledType
                             ("signatories" ':= PBuiltinList (PAsData PPubKeyHash))
                             ((':)
                                @PLabeledType
                                ("datums" ':= PBuiltinList (PAsData (PTuple PDatumHash PDatum)))
                                ((':) @PLabeledType ("id" ':= PTxId) ('[] @PLabeledType))))))))))))
txInfo'
      let inputs :: Term s (PBuiltinList (PAsData PTxInInfo))
inputs = HRec
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ((':)
        @(Symbol, Type)
        '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
        ((':)
           @(Symbol, Type)
           '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
           ('[] @(Symbol, Type)))))
txInfo.inputs
          mintedValue :: Term s (PValue 'Sorted 'NoGuarantees)
mintedValue = Term s (PAsData (PValue 'Sorted 'NoGuarantees))
-> Term s (PValue 'Sorted 'NoGuarantees)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData HRec
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ((':)
        @(Symbol, Type)
        '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
        ((':)
           @(Symbol, Type)
           '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
           ('[] @(Symbol, Type)))))
txInfo.mint
          AssetClass (CurrencySymbol
govCs, TokenName
govTn) = AuthorityToken
params.authority
          govAc :: Term s PAssetClass
govAc = Term s (PCurrencySymbol :--> (PTokenName :--> PAssetClass))
forall (s :: S).
Term s (PCurrencySymbol :--> (PTokenName :--> PAssetClass))
passetClass Term s (PCurrencySymbol :--> (PTokenName :--> PAssetClass))
-> Term s PCurrencySymbol -> Term s (PTokenName :--> PAssetClass)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# PLifted PCurrencySymbol -> Term s PCurrencySymbol
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PCurrencySymbol
CurrencySymbol
govCs Term s (PTokenName :--> PAssetClass)
-> Term s PTokenName -> Term s PAssetClass
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# PLifted PTokenName -> Term s PTokenName
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PTokenName
TokenName
govTn
          govTokenSpent :: Term s PBool
govTokenSpent = Term
  s (PAssetClass :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
forall {s :: S}.
Term
  s (PAssetClass :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
pisTokenSpent Term
  s (PAssetClass :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
-> Term s PAssetClass
-> Term s (PBuiltinList (PAsData PTxInInfo) :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PAssetClass
govAc Term s (PBuiltinList (PAsData PTxInInfo) :--> PBool)
-> Term s (PBuiltinList (PAsData PTxInInfo)) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PAsData PTxInInfo))
inputs

      PMinting Term
  s
  (PDataRecord
     ((':)
        @PLabeledType ("_0" ':= PCurrencySymbol) ('[] @PLabeledType)))
ownSymbol' <- Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC (Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s))
-> Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PScriptPurpose) -> Term s PScriptPurpose
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData HRec
  ((':)
     @(Symbol, Type)
     '("txInfo", Term s (PAsData PTxInfo))
     ((':)
        @(Symbol, Type)
        '("purpose", Term s (PAsData PScriptPurpose))
        ('[] @(Symbol, Type))))
ctx.purpose

      let ownSymbol :: Term s PCurrencySymbol
ownSymbol = Term s (PAsData PCurrencySymbol) -> Term s PCurrencySymbol
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PCurrencySymbol) -> Term s PCurrencySymbol)
-> Term s (PAsData PCurrencySymbol) -> Term s PCurrencySymbol
forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" Term
  s
  (PDataRecord
     ((':) @PLabeledType ("_0" ':= PCurrencySymbol) ('[] @PLabeledType))
   :--> PAsData PCurrencySymbol)
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType ("_0" ':= PCurrencySymbol) ('[] @PLabeledType)))
-> Term s (PAsData PCurrencySymbol)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord
     ((':)
        @PLabeledType ("_0" ':= PCurrencySymbol) ('[] @PLabeledType)))
ownSymbol'
          mintedATs :: Term s (PInteger @S)
mintedATs = Term
  s
  (PValue 'Sorted 'NoGuarantees :--> (PAssetClass :--> PInteger @S))
forall (s :: S) (keys :: KeyGuarantees)
       (amounts :: AmountGuarantees).
Term s (PValue keys amounts :--> (PAssetClass :--> PInteger @S))
passetClassValueOf Term
  s
  (PValue 'Sorted 'NoGuarantees :--> (PAssetClass :--> PInteger @S))
-> Term s (PValue 'Sorted 'NoGuarantees)
-> Term s (PAssetClass :--> PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PValue 'Sorted 'NoGuarantees)
mintedValue Term s (PAssetClass :--> PInteger @S)
-> Term s PAssetClass -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term s (PCurrencySymbol :--> (PTokenName :--> PAssetClass))
forall (s :: S).
Term s (PCurrencySymbol :--> (PTokenName :--> PAssetClass))
passetClass Term s (PCurrencySymbol :--> (PTokenName :--> PAssetClass))
-> Term s PCurrencySymbol -> Term s (PTokenName :--> PAssetClass)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
ownSymbol Term s (PTokenName :--> PAssetClass)
-> Term s PTokenName -> Term s PAssetClass
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# PLifted PTokenName -> Term s PTokenName
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PTokenName
TokenName
"")
      Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s POpaque -> TermCont @POpaque s (Term s POpaque))
-> Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$
        Term s PBool -> Term s POpaque -> Term s POpaque -> Term s POpaque
forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
          (Term s (PInteger @S)
0 Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PInteger @S)
mintedATs)
          ( TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @POpaque s (Term s POpaque) -> Term s POpaque)
-> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ do
              Term s (PString @S) -> Term s PBool -> TermCont @POpaque s ()
forall {r :: PType} (s :: S).
Term s (PString @S) -> Term s PBool -> TermCont @r s ()
pguardC Term s (PString @S)
"Parent token did not move in minting GATs" Term s PBool
govTokenSpent
              Term s (PString @S) -> Term s PBool -> TermCont @POpaque s ()
forall {r :: PType} (s :: S).
Term s (PString @S) -> Term s PBool -> TermCont @r s ()
pguardC Term s (PString @S)
"All outputs only emit valid GATs" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                Term
  s
  ((PAsData PTxOut :--> PBool)
   :--> (PBuiltinList (PAsData PTxOut) :--> PBool))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pall
                  # plam
                    ( (authorityTokensValidIn # ownSymbol #)
                        . pfromData
                    )
                  # txInfo.outputs
              Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s POpaque -> TermCont @POpaque s (Term s POpaque))
-> Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$ Term s (PUnit @S) -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (Term s (PUnit @S) -> Term s POpaque)
-> Term s (PUnit @S) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ()
          )
          (Term s (PUnit @S) -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (Term s (PUnit @S) -> Term s POpaque)
-> Term s (PUnit @S) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ())