{- | Agora DRep Proxy script

@since 1.0.0
-}
module Agora.Proxy (proxyScript, PProxyDatum (..), ProxyDatum (..)) where

import Agora.Utils (pcountIf, pcurrencySymbolToScriptHash, pscriptHashToCurrencySymbol)
import Data.Kind (Type)
import GHC.Generics qualified as GHC
import Generics.SOP qualified as SOP
import Plutarch.Internal.Term (Term)
import Plutarch.LedgerApi.Utils (PMaybeData (PDJust))
import Plutarch.LedgerApi.V3 (
  PAddress (PAddress),
  PCredential (PScriptCredential),
  PCurrencySymbol,
  PDatum (PDatum),
  PDatumHash,
  PMap (PMap),
  POutputDatum (POutputDatumHash),
  PScriptContext (PScriptContext),
  PScriptHash,
  PScriptInfo (PMintingScript, PSpendingScript),
  PTxInInfo (PTxInInfo),
  PTxInfo (PTxInfo),
  PTxOut (PTxOut),
  PValue (PValue),
 )
import Plutarch.Maybe (PMaybe (PNothing), pjust)
import Plutarch.Monadic qualified as P
import Plutarch.Prelude (
  PAsData,
  PBool (PFalse),
  PBuiltinList (PCons, PNil),
  PData,
  PEq ((#==)),
  PInteger,
  PIsData,
  PMaybe (PJust),
  PTryFrom,
  PUnit (PUnit),
  PlutusType,
  S,
  pcon,
  pconstant,
  perror,
  pfoldr,
  pfromData,
  pfstBuiltin,
  pif,
  plam,
  pmatch,
  precList,
  psndBuiltin,
  ptraceInfoIfFalse,
  ptryFrom,
  tcont,
  unTermCont,
  (#),
  (#&&),
  (:-->),
 )
import Plutarch.Repr.Data (DeriveAsDataRec (DeriveAsDataRec))
import PlutusLedgerApi.V3 (DatumHash, FromData (fromBuiltinData), ScriptHash, adaToken, toBuiltin, toData)
import PlutusTx (ToData (toBuiltinData))
import PlutusTx qualified
import PlutusTx.Builtins (chooseData, unsafeDataAsList)

{- | Haskell-level datum for the Proxy Validator script.

@since 1.0.0
-}
data ProxyDatum = ProxyDatum
  { ProxyDatum -> ScriptHash
pdReceiverScript :: ScriptHash
  , ProxyDatum -> DatumHash
pdDatumHash :: DatumHash
  }
  deriving stock
    ( -- | @since 1.0.0
      Int -> ProxyDatum -> ShowS
[ProxyDatum] -> ShowS
ProxyDatum -> String
(Int -> ProxyDatum -> ShowS)
-> (ProxyDatum -> String)
-> ([ProxyDatum] -> ShowS)
-> Show ProxyDatum
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProxyDatum -> ShowS
showsPrec :: Int -> ProxyDatum -> ShowS
$cshow :: ProxyDatum -> String
show :: ProxyDatum -> String
$cshowList :: [ProxyDatum] -> ShowS
showList :: [ProxyDatum] -> ShowS
Show
    , -- | @since 1.0.0
      (forall x. ProxyDatum -> Rep ProxyDatum x)
-> (forall x. Rep ProxyDatum x -> ProxyDatum) -> Generic ProxyDatum
forall x. Rep ProxyDatum x -> ProxyDatum
forall x. ProxyDatum -> Rep ProxyDatum x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ProxyDatum -> Rep ProxyDatum x
from :: forall x. ProxyDatum -> Rep ProxyDatum x
$cto :: forall x. Rep ProxyDatum x -> ProxyDatum
to :: forall x. Rep ProxyDatum x -> ProxyDatum
GHC.Generic
    )
  deriving anyclass
    ( -- | @since 1.0.0
      All @[Type] (SListI @Type) (Code ProxyDatum)
All @[Type] (SListI @Type) (Code ProxyDatum) =>
(ProxyDatum -> Rep ProxyDatum)
-> (Rep ProxyDatum -> ProxyDatum) -> Generic ProxyDatum
Rep ProxyDatum -> ProxyDatum
ProxyDatum -> Rep ProxyDatum
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
$cfrom :: ProxyDatum -> Rep ProxyDatum
from :: ProxyDatum -> Rep ProxyDatum
$cto :: Rep ProxyDatum -> ProxyDatum
to :: Rep ProxyDatum -> ProxyDatum
SOP.Generic
    )

-- | @since 1.0.0
instance PlutusTx.FromData ProxyDatum where
  {-# INLINEABLE fromBuiltinData #-}
  fromBuiltinData :: BuiltinData -> Maybe ProxyDatum
fromBuiltinData BuiltinData
d =
    BuiltinData
-> (BuiltinData -> Maybe ProxyDatum)
-> (BuiltinData -> Maybe ProxyDatum)
-> (BuiltinData -> Maybe ProxyDatum)
-> (BuiltinData -> Maybe ProxyDatum)
-> (BuiltinData -> Maybe ProxyDatum)
-> BuiltinData
-> Maybe ProxyDatum
forall a. BuiltinData -> a -> a -> a -> a -> a -> a
chooseData
      BuiltinData
d
      (Maybe ProxyDatum -> BuiltinData -> Maybe ProxyDatum
forall a b. a -> b -> a
const Maybe ProxyDatum
forall a. Maybe a
Nothing)
      (Maybe ProxyDatum -> BuiltinData -> Maybe ProxyDatum
forall a b. a -> b -> a
const Maybe ProxyDatum
forall a. Maybe a
Nothing)
      ( \BuiltinData
d' ->
          case BuiltinData -> [BuiltinData]
unsafeDataAsList BuiltinData
d' of
            [BuiltinData
receiverScript, BuiltinData
datumHash] ->
              ScriptHash -> DatumHash -> ProxyDatum
ProxyDatum
                (ScriptHash -> DatumHash -> ProxyDatum)
-> Maybe ScriptHash -> Maybe (DatumHash -> ProxyDatum)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinData -> Maybe ScriptHash
forall a. FromData a => BuiltinData -> Maybe a
fromBuiltinData BuiltinData
receiverScript
                Maybe (DatumHash -> ProxyDatum)
-> Maybe DatumHash -> Maybe ProxyDatum
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> BuiltinData -> Maybe DatumHash
forall a. FromData a => BuiltinData -> Maybe a
fromBuiltinData BuiltinData
datumHash
            [BuiltinData]
_ -> Maybe ProxyDatum
forall a. Maybe a
Nothing
      )
      (Maybe ProxyDatum -> BuiltinData -> Maybe ProxyDatum
forall a b. a -> b -> a
const Maybe ProxyDatum
forall a. Maybe a
Nothing)
      (Maybe ProxyDatum -> BuiltinData -> Maybe ProxyDatum
forall a b. a -> b -> a
const Maybe ProxyDatum
forall a. Maybe a
Nothing)
      BuiltinData
d

-- | @since 1.0.0
instance PlutusTx.ToData ProxyDatum where
  {-# INLINEABLE toBuiltinData #-}
  toBuiltinData :: ProxyDatum -> BuiltinData
toBuiltinData (ProxyDatum ScriptHash
receiverScript DatumHash
datumHash) =
    Data -> ToBuiltin Data
forall a. HasToBuiltin a => a -> ToBuiltin a
toBuiltin (Data -> ToBuiltin Data) -> Data -> ToBuiltin Data
forall a b. (a -> b) -> a -> b
$ [Data] -> Data
PlutusTx.List [ScriptHash -> Data
forall a. ToData a => a -> Data
toData ScriptHash
receiverScript, DatumHash -> Data
forall a. ToData a => a -> Data
toData DatumHash
datumHash]

{- | Datum stored at the proxy validator script

@since 1.0.0
-}
type PProxyDatum :: S -> Type
data PProxyDatum s = PProxyDatum
  { forall (s :: S). PProxyDatum s -> Term s (PAsData PScriptHash)
receiverScript :: Term s (PAsData PScriptHash)
  -- ^ Script hash of the Plutus V3 effect
  , forall (s :: S). PProxyDatum s -> Term s (PAsData PDatumHash)
datumHash :: Term s (PAsData PDatumHash)
  -- ^ Hash of the datum that must be created at the receiver script
  }
  deriving stock ((forall x. PProxyDatum s -> Rep (PProxyDatum s) x)
-> (forall x. Rep (PProxyDatum s) x -> PProxyDatum s)
-> Generic (PProxyDatum s)
forall x. Rep (PProxyDatum s) x -> PProxyDatum s
forall x. PProxyDatum s -> Rep (PProxyDatum s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: S) x. Rep (PProxyDatum s) x -> PProxyDatum s
forall (s :: S) x. PProxyDatum s -> Rep (PProxyDatum s) x
$cfrom :: forall (s :: S) x. PProxyDatum s -> Rep (PProxyDatum s) x
from :: forall x. PProxyDatum s -> Rep (PProxyDatum s) x
$cto :: forall (s :: S) x. Rep (PProxyDatum s) x -> PProxyDatum s
to :: forall x. Rep (PProxyDatum s) x -> PProxyDatum s
GHC.Generic)
  deriving anyclass (All @[Type] (SListI @Type) (Code (PProxyDatum s))
All @[Type] (SListI @Type) (Code (PProxyDatum s)) =>
(PProxyDatum s -> Rep (PProxyDatum s))
-> (Rep (PProxyDatum s) -> PProxyDatum s)
-> Generic (PProxyDatum s)
Rep (PProxyDatum s) -> PProxyDatum s
PProxyDatum s -> Rep (PProxyDatum s)
forall a.
All @[Type] (SListI @Type) (Code a) =>
(a -> Rep a) -> (Rep a -> a) -> Generic a
forall (s :: S). All @[Type] (SListI @Type) (Code (PProxyDatum s))
forall (s :: S). Rep (PProxyDatum s) -> PProxyDatum s
forall (s :: S). PProxyDatum s -> Rep (PProxyDatum s)
$cfrom :: forall (s :: S). PProxyDatum s -> Rep (PProxyDatum s)
from :: PProxyDatum s -> Rep (PProxyDatum s)
$cto :: forall (s :: S). Rep (PProxyDatum s) -> PProxyDatum s
to :: Rep (PProxyDatum s) -> PProxyDatum s
SOP.Generic, (forall (s :: S).
 Term s PProxyDatum -> Term s PProxyDatum -> Term s PBool)
-> PEq PProxyDatum
forall (s :: S).
Term s PProxyDatum -> Term s PProxyDatum -> Term s PBool
forall (t :: PType).
(forall (s :: S). Term s t -> Term s t -> Term s PBool) -> PEq t
$c#== :: forall (s :: S).
Term s PProxyDatum -> Term s PProxyDatum -> Term s PBool
#== :: forall (s :: S).
Term s PProxyDatum -> Term s PProxyDatum -> Term s PBool
PEq, (forall (s :: S).
 Term s (PAsData PProxyDatum) -> Term s PProxyDatum)
-> (forall (s :: S). Term s PProxyDatum -> Term s PData)
-> PIsData PProxyDatum
forall (s :: S). Term s (PAsData PProxyDatum) -> Term s PProxyDatum
forall (s :: S). Term s PProxyDatum -> Term s PData
forall (a :: PType).
(forall (s :: S). Term s (PAsData a) -> Term s a)
-> (forall (s :: S). Term s a -> Term s PData) -> PIsData a
$cpfromDataImpl :: forall (s :: S). Term s (PAsData PProxyDatum) -> Term s PProxyDatum
pfromDataImpl :: forall (s :: S). Term s (PAsData PProxyDatum) -> Term s PProxyDatum
$cpdataImpl :: forall (s :: S). Term s PProxyDatum -> Term s PData
pdataImpl :: forall (s :: S). Term s PProxyDatum -> Term s PData
PIsData)
  deriving ((forall (s :: S). PProxyDatum s -> Term s (PInner PProxyDatum))
-> (forall (s :: S) (b :: PType).
    Term s (PInner PProxyDatum)
    -> (PProxyDatum s -> Term s b) -> Term s b)
-> PlutusType PProxyDatum
forall (s :: S). PProxyDatum s -> Term s (PInner PProxyDatum)
forall (s :: S) (b :: PType).
Term s (PInner PProxyDatum)
-> (PProxyDatum s -> Term s b) -> Term s b
forall (a :: PType).
(forall (s :: S). a s -> Term s (PInner a))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
$cpcon' :: forall (s :: S). PProxyDatum s -> Term s (PInner PProxyDatum)
pcon' :: forall (s :: S). PProxyDatum s -> Term s (PInner PProxyDatum)
$cpmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PProxyDatum)
-> (PProxyDatum s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PProxyDatum)
-> (PProxyDatum s -> Term s b) -> Term s b
PlutusType) via (DeriveAsDataRec PProxyDatum)

-- | @since 1.0.0
instance PTryFrom PData (PAsData PProxyDatum)

{- | Proxy script

This script serves both validator script and minting script purposes.
  - Mint a Proxied Governance Authority Token
  - Verify spending from the proxy effect script address

See details in the [specification](https://mlabs-haskell.github.io/agora-drep/static/agora-drep-specification.pdf).

@since 1.0.0
-}
proxyScript :: (forall (s :: S). Term s (PAsData PCurrencySymbol :--> PAsData PScriptContext :--> PUnit))
proxyScript :: forall (s :: S).
Term
  s
  (PAsData PCurrencySymbol :--> (PAsData PScriptContext :--> PUnit))
proxyScript = (Term s (PAsData PCurrencySymbol)
 -> Term s (PAsData PScriptContext) -> Term s PUnit)
-> Term
     s
     (PAsData PCurrencySymbol :--> (PAsData PScriptContext :--> PUnit))
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s (PAsData PScriptContext) -> Term s PUnit)
-> Term s (c :--> (PAsData PScriptContext :--> PUnit))
plam ((Term s (PAsData PCurrencySymbol)
  -> Term s (PAsData PScriptContext) -> Term s PUnit)
 -> Term
      s
      (PAsData PCurrencySymbol :--> (PAsData PScriptContext :--> PUnit)))
-> (Term s (PAsData PCurrencySymbol)
    -> Term s (PAsData PScriptContext) -> Term s PUnit)
-> Term
     s
     (PAsData PCurrencySymbol :--> (PAsData PScriptContext :--> PUnit))
forall a b. (a -> b) -> a -> b
$ \Term s (PAsData PCurrencySymbol)
authSymbol' Term s (PAsData PScriptContext)
ctx -> P.do
  PScriptContext Term s PTxInfo
txInfo Term s PRedeemer
_redeemer Term s PScriptInfo
scriptInfo <- Term s PScriptContext
-> (PScriptContext s -> Term s PUnit) -> Term s PUnit
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s PScriptContext
 -> (PScriptContext s -> Term s PUnit) -> Term s PUnit)
-> Term s PScriptContext
-> (PScriptContext s -> Term s PUnit)
-> Term s PUnit
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PScriptContext) -> Term s PScriptContext
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PScriptContext)
ctx

  let valid :: Term s PBool
valid =
        Term s PScriptInfo
-> (PScriptInfo s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PScriptInfo
scriptInfo ((PScriptInfo s -> Term s PBool) -> Term s PBool)
-> (PScriptInfo s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
          PSpendingScript Term s PTxOutRef
_txOutRef Term s (PMaybeData PDatum)
mayDatum -> P.do
            -- When this script runs also V2 GAT gets burned so that guarantees that no V3 thing happens
            PTxInfo Term s (PAsData (PBuiltinList (PAsData PTxInInfo)))
inputs Term s (PAsData (PBuiltinList (PAsData PTxInInfo)))
_ Term s (PAsData (PBuiltinList (PAsData PTxOut)))
outputs Term s (PAsData PLovelace)
_ Term s (PAsData (PValue 'Sorted 'NonZero))
mint Term s (PAsData (PBuiltinList (PAsData PTxCert)))
txCerts Term s (PAsData (PMap 'Unsorted PCredential PLovelace))
_ Term s (PInterval PPosixTime)
_ Term s (PAsData (PBuiltinList (PAsData PPubKeyHash)))
_ Term s (PAsData (PMap 'Unsorted PScriptPurpose PRedeemer))
_ Term s (PAsData (PMap 'Unsorted PDatumHash PDatum))
_ Term s (PAsData PTxId)
_ Term
  s
  (PAsData
     (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote)))
_ Term s (PAsData (PBuiltinList (PAsData PProposalProcedure)))
_ Term s (PMaybeData PLovelace)
_ Term s (PMaybeData PLovelace)
_ <- Term s PTxInfo -> (PTxInfo s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PTxInfo
txInfo

            PDJust Term s (PAsData PDatum)
datum <- Term s (PMaybeData PDatum)
-> (PMaybeData PDatum s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybeData PDatum)
mayDatum
            PDatum Term s PData
rawDatum <- Term s PDatum -> (PDatum s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PAsData PDatum) -> Term s PDatum
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PDatum)
datum)

            let rawProxyDatum :: Term s (PAsData PProxyDatum)
rawProxyDatum = TermCont @(PAsData PProxyDatum) s (Term s (PAsData PProxyDatum))
-> Term s (PAsData PProxyDatum)
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @(PAsData PProxyDatum) s (Term s (PAsData PProxyDatum))
 -> Term s (PAsData PProxyDatum))
-> TermCont @(PAsData PProxyDatum) s (Term s (PAsData PProxyDatum))
-> Term s (PAsData PProxyDatum)
forall a b. (a -> b) -> a -> b
$ (Term s (PAsData PProxyDatum), ()) -> Term s (PAsData PProxyDatum)
forall a b. (a, b) -> a
fst ((Term s (PAsData PProxyDatum), ())
 -> Term s (PAsData PProxyDatum))
-> TermCont
     @(PAsData PProxyDatum) s (Term s (PAsData PProxyDatum), ())
-> TermCont @(PAsData PProxyDatum) s (Term s (PAsData PProxyDatum))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Term s (PAsData PProxyDatum), ())
  -> Term s (PAsData PProxyDatum))
 -> Term s (PAsData PProxyDatum))
-> TermCont
     @(PAsData PProxyDatum) s (Term s (PAsData PProxyDatum), ())
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom @(PAsData PProxyDatum) Term s PData
rawDatum)
            PProxyDatum Term s (PAsData PScriptHash)
receiverScript Term s (PAsData PDatumHash)
datumHash <- Term s PProxyDatum
-> (PProxyDatum s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s PProxyDatum
 -> (PProxyDatum s -> Term s PBool) -> Term s PBool)
-> Term s PProxyDatum
-> (PProxyDatum s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PProxyDatum) -> Term s PProxyDatum
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PProxyDatum)
rawProxyDatum

            let receiverScriptAddr :: Term s PAddress
receiverScriptAddr =
                  PAddress s -> Term s PAddress
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PAddress s -> Term s PAddress) -> PAddress s -> Term s PAddress
forall a b. (a -> b) -> a -> b
$ Term s PCredential
-> Term s (PMaybeData PStakingCredential) -> PAddress s
forall (s :: S).
Term s PCredential
-> Term s (PMaybeData PStakingCredential) -> PAddress s
PAddress (PCredential s -> Term s PCredential
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon (PCredential s -> Term s PCredential)
-> PCredential s -> Term s PCredential
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PScriptHash) -> PCredential s
forall (s :: S). Term s (PAsData PScriptHash) -> PCredential s
PScriptCredential Term s (PAsData PScriptHash)
receiverScript) (AsHaskell (PMaybeData PStakingCredential)
-> Term s (PMaybeData PStakingCredential)
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Maybe StakingCredential
AsHaskell (PMaybeData PStakingCredential)
forall a. Maybe a
Nothing)

            let outputsAtReceiver :: Term s PInteger
outputsAtReceiver =
                  Term
  s
  ((PAsData PTxOut :--> (PInteger :--> PInteger))
   :--> (PInteger :--> (PBuiltinList (PAsData PTxOut) :--> PInteger)))
forall (list :: PType -> PType) (a :: PType) (s :: S) (b :: PType).
PIsListLike list a =>
Term s ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
pfoldr
                    # plam
                      ( \output v -> P.do
                          PTxOut address _ outputDatum _ <- pmatch (pfromData output)
                          pif
                            (address #== receiverScriptAddr)
                            ( P.do
                                POutputDatumHash datumHash' <- pmatch outputDatum

                                pif
                                  (datumHash' #== datumHash)
                                  (v + 1)
                                  (P.fail "While counting outputs at receiver address: datum hash invalid.")
                            )
                            v
                      )
                    # (0 :: Term _ PInteger)
                    # pfromData outputs
            -- Spending Condition 3: Transaction creates a UTxO at address of
            -- receiverScript with empty staking part and reference datum
            -- with hash equal to datumHash.
            let singleOutputWithDatum :: Term s PBool
singleOutputWithDatum =
                  Term s PString -> Term s PBool -> Term s PBool
forall (s :: S). Term s PString -> Term s PBool -> Term s PBool
ptraceInfoIfFalse Term s PString
"Exactly one output at the receiver script address should exist with datum hash defined in ProxyDatum." (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$
                    Term s PInteger
outputsAtReceiver Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
1

            -- If there is only one script input and we are running that means that we are that input
            -- so no need to check explicitly
            let scriptInputs :: Term s (PMaybe (PAsData PScriptHash))
scriptInputs =
                  (Term
   s
   (PBuiltinList (PAsData PTxInInfo)
    :--> PMaybe (PAsData PScriptHash))
 -> Term s (PAsData PTxInInfo)
 -> Term s (PBuiltinList (PAsData PTxInInfo))
 -> Term s (PMaybe (PAsData PScriptHash)))
-> (Term
      s
      (PBuiltinList (PAsData PTxInInfo)
       :--> PMaybe (PAsData PScriptHash))
    -> Term s (PMaybe (PAsData PScriptHash)))
-> Term
     s
     (PBuiltinList (PAsData PTxInInfo)
      :--> PMaybe (PAsData PScriptHash))
forall (list :: PType -> PType) (a :: PType) (s :: S) (r :: PType).
PIsListLike list a =>
(Term s (list a :--> r) -> Term s a -> Term s (list a) -> Term s r)
-> (Term s (list a :--> r) -> Term s r) -> Term s (list a :--> r)
precList
                    ( \Term
  s
  (PBuiltinList (PAsData PTxInInfo)
   :--> PMaybe (PAsData PScriptHash))
self Term s (PAsData PTxInInfo)
input Term s (PBuiltinList (PAsData PTxInInfo))
rest -> Term s PTxInInfo
-> (PTxInInfo s -> Term s (PMaybe (PAsData PScriptHash)))
-> Term s (PMaybe (PAsData PScriptHash))
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PAsData PTxInInfo) -> Term s PTxInInfo
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PTxInInfo)
input) ((PTxInInfo s -> Term s (PMaybe (PAsData PScriptHash)))
 -> Term s (PMaybe (PAsData PScriptHash)))
-> (PTxInInfo s -> Term s (PMaybe (PAsData PScriptHash)))
-> Term s (PMaybe (PAsData PScriptHash))
forall a b. (a -> b) -> a -> b
$ \case
                        PTxInInfo Term s PTxOutRef
_ Term s PTxOut
resolved -> P.do
                          PTxOut Term s PAddress
addr Term s (PAsData (PValue 'Sorted 'Positive))
_ Term s POutputDatum
_ Term s (PMaybeData PScriptHash)
_ <- Term s PTxOut
-> (PTxOut s -> Term s (PMaybe (PAsData PScriptHash)))
-> Term s (PMaybe (PAsData PScriptHash))
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PTxOut
resolved
                          PAddress Term s PCredential
cred Term s (PMaybeData PStakingCredential)
_ <- Term s PAddress
-> (PAddress s -> Term s (PMaybe (PAsData PScriptHash)))
-> Term s (PMaybe (PAsData PScriptHash))
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PAddress
addr
                          Term s PCredential
-> (PCredential s -> Term s (PMaybe (PAsData PScriptHash)))
-> Term s (PMaybe (PAsData PScriptHash))
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PCredential
cred ((PCredential s -> Term s (PMaybe (PAsData PScriptHash)))
 -> Term s (PMaybe (PAsData PScriptHash)))
-> (PCredential s -> Term s (PMaybe (PAsData PScriptHash)))
-> Term s (PMaybe (PAsData PScriptHash))
forall a b. (a -> b) -> a -> b
$ \case
                            PScriptCredential Term s (PAsData PScriptHash)
hash -> Term s (PMaybe (PAsData PScriptHash))
-> (PMaybe (PAsData PScriptHash) s
    -> Term s (PMaybe (PAsData PScriptHash)))
-> Term s (PMaybe (PAsData PScriptHash))
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term
  s
  (PBuiltinList (PAsData PTxInInfo)
   :--> PMaybe (PAsData PScriptHash))
self Term
  s
  (PBuiltinList (PAsData PTxInInfo)
   :--> PMaybe (PAsData PScriptHash))
-> Term s (PBuiltinList (PAsData PTxInInfo))
-> Term s (PMaybe (PAsData PScriptHash))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PAsData PTxInInfo))
rest) ((PMaybe (PAsData PScriptHash) s
  -> Term s (PMaybe (PAsData PScriptHash)))
 -> Term s (PMaybe (PAsData PScriptHash)))
-> (PMaybe (PAsData PScriptHash) s
    -> Term s (PMaybe (PAsData PScriptHash)))
-> Term s (PMaybe (PAsData PScriptHash))
forall a b. (a -> b) -> a -> b
$ \case
                              PMaybe (PAsData PScriptHash) s
PNothing -> Term s (PAsData PScriptHash :--> PMaybe (PAsData PScriptHash))
forall (a :: PType) (s :: S). Term s (a :--> PMaybe a)
pjust Term s (PAsData PScriptHash :--> PMaybe (PAsData PScriptHash))
-> Term s (PAsData PScriptHash)
-> Term s (PMaybe (PAsData PScriptHash))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PScriptHash)
hash
                              PJust Term s (PAsData PScriptHash)
_ -> Term s (PMaybe (PAsData PScriptHash))
forall (s :: S) (a :: PType). Term s a
perror
                            PCredential s
_ -> Term
  s
  (PBuiltinList (PAsData PTxInInfo)
   :--> PMaybe (PAsData PScriptHash))
self Term
  s
  (PBuiltinList (PAsData PTxInInfo)
   :--> PMaybe (PAsData PScriptHash))
-> Term s (PBuiltinList (PAsData PTxInInfo))
-> Term s (PMaybe (PAsData PScriptHash))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PAsData PTxInInfo))
rest
                    )
                    (Term s (PMaybe (PAsData PScriptHash))
-> Term
     s
     (PBuiltinList (PAsData PTxInInfo)
      :--> PMaybe (PAsData PScriptHash))
-> Term s (PMaybe (PAsData PScriptHash))
forall a b. a -> b -> a
const (forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @(PMaybe (PAsData PScriptHash)) Maybe ScriptHash
AsHaskell (PMaybe (PAsData PScriptHash))
forall a. Maybe a
Nothing))
                    # pfromData inputs

            -- Spending condition 6: Transaction does not include script inputs other than own input.
            PJust Term s (PAsData PScriptHash)
ownScriptHash <- Term s (PMaybe (PAsData PScriptHash))
-> (PMaybe (PAsData PScriptHash) s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s (PMaybe (PAsData PScriptHash))
scriptInputs
            let ownCurrencySymbol :: Term s (PAsData PCurrencySymbol)
ownCurrencySymbol = Term s (PAsData PScriptHash) -> Term s (PAsData PCurrencySymbol)
forall (s :: S).
Term s (PAsData PScriptHash) -> Term s (PAsData PCurrencySymbol)
pscriptHashToCurrencySymbol Term s (PAsData PScriptHash)
ownScriptHash

            -- Spending Condition 1: Transaction burns one GAT (symbol is known from script parameter)
            -- Spending Condition 2: Spent UTxO contains GAT
            -- Spending condition 4: Transaction does not mint or burn any tokens other than V2 and V3 GATs.

            -- There is a bit to unpack here:
            -- Fact that we are burning a V2 GAT combined with Condition 6 ensures that there is a
            -- V2 GAT in the inputs. There is only one script input so it either comes from the
            -- currently validated input OR that there is a pubkey address that had V2 GAT.
            -- If it is the latter that means that the whole setup is already compromised so it
            -- does not matter what happens here anyway.
            -- No need to check for name of V2 token as GAT policy enforces that
            -- Pattern matching asserts that there are only two symbols minted and `mintCheck`
            -- asserts that they are V2 and V3 gats.
            PValue Term
  s (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger))
mintAssetMap <- Term s (PValue 'Sorted 'NonZero)
-> (PValue 'Sorted 'NonZero s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PAsData (PValue 'Sorted 'NonZero))
-> Term s (PValue 'Sorted 'NonZero)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (PValue 'Sorted 'NonZero))
mint)
            PMap Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetList <- Term
  s (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger))
-> (PMap
      'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger))
mintAssetMap
            PCons Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair1 Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetListRest1 <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PCurrencySymbol)
         (PAsData (PMap 'Sorted PTokenName PInteger)))
      s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetList
            PCons Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair2 Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetListRest2 <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PCurrencySymbol)
         (PAsData (PMap 'Sorted PTokenName PInteger)))
      s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetListRest1
            PBuiltinList
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
  s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PCurrencySymbol)
         (PAsData (PMap 'Sorted PTokenName PInteger)))
      s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetListRest2
            let mintCs1 :: Term s (PAsData PCurrencySymbol)
mintCs1 = Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData PCurrencySymbol)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData PCurrencySymbol)
-> Term
     s
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger)))
-> Term s (PAsData PCurrencySymbol)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair1
            PMap Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens1 <- Term s (PMap 'Sorted PTokenName PInteger)
-> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PMap 'Sorted PTokenName PInteger)
 -> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
 -> Term s PBool)
-> Term s (PMap 'Sorted PTokenName PInteger)
-> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PMap 'Sorted PTokenName PInteger))
-> Term s (PMap 'Sorted PTokenName PInteger)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData (PMap 'Sorted PTokenName PInteger))
-> Term
     s
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger)))
-> Term s (PAsData (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair1)
            PCons Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
mintTokenPair1 Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens1Rest <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens1
            PBuiltinList
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens1Rest
            let mintCs2 :: Term s (PAsData PCurrencySymbol)
mintCs2 = Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData PCurrencySymbol)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData PCurrencySymbol)
-> Term
     s
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger)))
-> Term s (PAsData PCurrencySymbol)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair2
            PMap Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens2 <- Term s (PMap 'Sorted PTokenName PInteger)
-> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PMap 'Sorted PTokenName PInteger)
 -> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
 -> Term s PBool)
-> Term s (PMap 'Sorted PTokenName PInteger)
-> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PMap 'Sorted PTokenName PInteger))
-> Term s (PMap 'Sorted PTokenName PInteger)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData (PMap 'Sorted PTokenName PInteger))
-> Term
     s
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger)))
-> Term s (PAsData (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair2)
            PCons Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
mintTokenPair2 Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens2Rest <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens2
            PBuiltinList
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens2Rest

            let mintCheck :: Term s PBool
mintCheck =
                  Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                    (Term s (PAsData PCurrencySymbol)
mintCs1 Term s (PAsData PCurrencySymbol)
-> Term s (PAsData PCurrencySymbol) -> Term s PBool
forall (s :: S).
Term s (PAsData PCurrencySymbol)
-> Term s (PAsData PCurrencySymbol) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData PCurrencySymbol)
ownCurrencySymbol)
                    ( ((Term
  s
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)
   :--> PAsData PTokenName)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)
   :--> PAsData PTokenName)
-> Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
-> Term s (PAsData PTokenName)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
mintTokenPair1) Term s (PAsData PTokenName)
-> Term s (PAsData PTokenName) -> Term s PBool
forall (s :: S).
Term s (PAsData PTokenName)
-> Term s (PAsData PTokenName) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== AsHaskell (PAsData PTokenName) -> Term s (PAsData PTokenName)
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant AsHaskell (PAsData PTokenName)
TokenName
adaToken)
                        #&& (pfromData (psndBuiltin # mintTokenPair1) #== pconstant 1)
                        #&& (mintCs2 #== authSymbol')
                        #&& (pfromData (psndBuiltin # mintTokenPair2) #== pconstant (-1))
                    )
                    ( ((Term
  s
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)
   :--> PAsData PTokenName)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)
   :--> PAsData PTokenName)
-> Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
-> Term s (PAsData PTokenName)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
mintTokenPair2) Term s (PAsData PTokenName)
-> Term s (PAsData PTokenName) -> Term s PBool
forall (s :: S).
Term s (PAsData PTokenName)
-> Term s (PAsData PTokenName) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== AsHaskell (PAsData PTokenName) -> Term s (PAsData PTokenName)
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant AsHaskell (PAsData PTokenName)
TokenName
adaToken)
                        #&& (pfromData (psndBuiltin # mintTokenPair2) #== pconstant 1)
                        #&& (mintCs2 #== ownCurrencySymbol)
                        #&& (mintCs1 #== authSymbol')
                        #&& (pfromData (psndBuiltin # mintTokenPair1) #== pconstant (-1))
                    )

            -- Spending condition 5: Transaction does not include any certificates
            PBuiltinList (PAsData PTxCert) s
PNil <- Term s (PBuiltinList (PAsData PTxCert))
-> (PBuiltinList (PAsData PTxCert) s -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PAsData (PBuiltinList (PAsData PTxCert)))
-> Term s (PBuiltinList (PAsData PTxCert))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (PBuiltinList (PAsData PTxCert)))
txCerts)

            (Term s PBool -> Term s PBool -> Term s PBool)
-> [Term s PBool] -> Term s PBool
forall a. (a -> a -> a) -> [a] -> a
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 PBool
singleOutputWithDatum
              , Term s PBool
mintCheck
              ]
          PMintingScript Term s (PAsData PCurrencySymbol)
currencySymbol -> P.do
            -- When this script runs also V2 GAT gets burned so that guarantees that no V3 thing happens
            PTxInfo Term s (PAsData (PBuiltinList (PAsData PTxInInfo)))
inputs Term s (PAsData (PBuiltinList (PAsData PTxInInfo)))
_ Term s (PAsData (PBuiltinList (PAsData PTxOut)))
_ Term s (PAsData PLovelace)
_ Term s (PAsData (PValue 'Sorted 'NonZero))
mint Term s (PAsData (PBuiltinList (PAsData PTxCert)))
_ Term s (PAsData (PMap 'Unsorted PCredential PLovelace))
_ Term s (PInterval PPosixTime)
_ Term s (PAsData (PBuiltinList (PAsData PPubKeyHash)))
_ Term s (PAsData (PMap 'Unsorted PScriptPurpose PRedeemer))
_ Term s (PAsData (PMap 'Unsorted PDatumHash PDatum))
_ Term s (PAsData PTxId)
_ Term
  s
  (PAsData
     (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote)))
_ Term s (PAsData (PBuiltinList (PAsData PProposalProcedure)))
_ Term s (PMaybeData PLovelace)
_ Term s (PMaybeData PLovelace)
_ <- Term s PTxInfo -> (PTxInfo s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PTxInfo
txInfo

            let isValidatorInput :: Term s (PAsData PTxInInfo :--> PBool)
isValidatorInput =
                  (Term s (PAsData PTxInInfo) -> Term s PBool)
-> Term s (PAsData PTxInInfo :--> PBool)
forall a (b :: PType) (s :: S) (c :: PType).
(PLamN a b s, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PBool) -> Term s (c :--> PBool)
plam
                    ( \Term s (PAsData PTxInInfo)
input -> Term s PTxInInfo -> (PTxInInfo s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PAsData PTxInInfo) -> Term s PTxInInfo
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PTxInInfo)
input) ((PTxInInfo s -> Term s PBool) -> Term s PBool)
-> (PTxInInfo s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
                        PTxInInfo Term s PTxOutRef
_ Term s PTxOut
resolved -> P.do
                          PTxOut Term s PAddress
addr Term s (PAsData (PValue 'Sorted 'Positive))
_ Term s POutputDatum
_ Term s (PMaybeData PScriptHash)
_ <- Term s PTxOut -> (PTxOut s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PTxOut
resolved
                          PAddress Term s PCredential
cred Term s (PMaybeData PStakingCredential)
_ <- Term s PAddress -> (PAddress s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PAddress
addr
                          Term s PCredential
-> (PCredential s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PCredential
cred ((PCredential s -> Term s PBool) -> Term s PBool)
-> (PCredential s -> Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
                            PScriptCredential Term s (PAsData PScriptHash)
scriptHash ->
                              Term s (PAsData PScriptHash)
scriptHash Term s (PAsData PScriptHash)
-> Term s (PAsData PScriptHash) -> Term s PBool
forall (s :: S).
Term s (PAsData PScriptHash)
-> Term s (PAsData PScriptHash) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData PCurrencySymbol) -> Term s (PAsData PScriptHash)
forall (s :: S).
Term s (PAsData PCurrencySymbol) -> Term s (PAsData PScriptHash)
pcurrencySymbolToScriptHash Term s (PAsData PCurrencySymbol)
currencySymbol
                            PCredential s
_ -> PBool s -> Term s PBool
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PBool s
forall (s :: S). PBool s
PFalse
                    )

            PValue Term
  s (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger))
mintAssetMap <- Term s (PValue 'Sorted 'NonZero)
-> (PValue 'Sorted 'NonZero s -> Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PAsData (PValue 'Sorted 'NonZero))
-> Term s (PValue 'Sorted 'NonZero)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (PValue 'Sorted 'NonZero))
mint)
            PMap Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetList <- Term
  s (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger))
-> (PMap
      'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger))
mintAssetMap
            PCons Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair1 Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetListRest1 <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PCurrencySymbol)
         (PAsData (PMap 'Sorted PTokenName PInteger)))
      s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetList
            let mintCs1 :: Term s (PAsData PCurrencySymbol)
mintCs1 = Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData PCurrencySymbol)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData PCurrencySymbol)
-> Term
     s
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger)))
-> Term s (PAsData PCurrencySymbol)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair1
            PMap Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens1 <- Term s (PMap 'Sorted PTokenName PInteger)
-> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PMap 'Sorted PTokenName PInteger)
 -> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
 -> Term s PBool)
-> Term s (PMap 'Sorted PTokenName PInteger)
-> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PMap 'Sorted PTokenName PInteger))
-> Term s (PMap 'Sorted PTokenName PInteger)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData (PMap 'Sorted PTokenName PInteger))
-> Term
     s
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger)))
-> Term s (PAsData (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair1)
            PCons Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
mintTokenPair1 Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens1Rest <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens1
            PBuiltinList
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens1Rest

            -- We have to account for minting and burning scenarios. Minting must
            -- Minting:
            --  - must have two asset classes (GAT burn and pGAT mint)
            --  - rules are enforced in the spending validator
            -- Burning:
            --  - must have exactly one asset class (pGAT burn)
            --  - transaction must contain an input from the Proxy script validator
            Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
              (Term s (PAsData PCurrencySymbol)
mintCs1 Term s (PAsData PCurrencySymbol)
-> Term s (PAsData PCurrencySymbol) -> Term s PBool
forall (s :: S).
Term s (PAsData PCurrencySymbol)
-> Term s (PAsData PCurrencySymbol) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData PCurrencySymbol)
currencySymbol)
              ( Term s PBool -> Term s PBool -> Term s PBool -> Term s PBool
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif
                  (Term s (PAsData PInteger) -> Term s PInteger
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
  s
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)
   :--> PAsData PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)
   :--> PAsData PInteger)
-> Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
-> Term s (PAsData PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
mintTokenPair1) Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== AsHaskell PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Integer
AsHaskell PInteger
1)
                  ((Term
  s
  ((PAsData PTxInInfo :--> PBool)
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PInteger))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PInteger))
pcountIf Term
  s
  ((PAsData PTxInInfo :--> PBool)
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PInteger))
-> Term s (PAsData PTxInInfo :--> PBool)
-> Term s (PBuiltinList (PAsData PTxInInfo) :--> PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PTxInInfo :--> PBool)
isValidatorInput Term s (PBuiltinList (PAsData PTxInInfo) :--> PInteger)
-> Term s (PBuiltinList (PAsData PTxInInfo)) -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData (PBuiltinList (PAsData PTxInInfo)))
-> Term s (PBuiltinList (PAsData PTxInInfo))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (PBuiltinList (PAsData PTxInInfo)))
inputs) Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PInteger
1)
                  ( P.do
                      PBuiltinList
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
  s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PCurrencySymbol)
         (PAsData (PMap 'Sorted PTokenName PInteger)))
      s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetListRest1
                      Term s (PAsData PInteger) -> Term s PInteger
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
  s
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)
   :--> PAsData PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)
   :--> PAsData PInteger)
-> Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
-> Term s (PAsData PInteger)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
mintTokenPair1) Term s PInteger -> Term s PInteger -> Term s PBool
forall (s :: S). Term s PInteger -> Term s PInteger -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== AsHaskell PInteger -> Term s PInteger
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant (-Integer
1)
                  )
              )
              ( P.do
                  PCons Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair2 Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetListRest2 <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PCurrencySymbol)
         (PAsData (PMap 'Sorted PTokenName PInteger)))
      s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetListRest1
                  PBuiltinList
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
  s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PCurrencySymbol)
         (PAsData (PMap 'Sorted PTokenName PInteger)))
      s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger))))
mintAssetListRest2
                  let mintCs2 :: Term s (PAsData PCurrencySymbol)
mintCs2 = Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData PCurrencySymbol)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData PCurrencySymbol)
-> Term
     s
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger)))
-> Term s (PAsData PCurrencySymbol)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair2
                  PMap Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens2 <- Term s (PMap 'Sorted PTokenName PInteger)
-> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch (Term s (PMap 'Sorted PTokenName PInteger)
 -> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
 -> Term s PBool)
-> Term s (PMap 'Sorted PTokenName PInteger)
-> (PMap 'Sorted PTokenName PInteger s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PMap 'Sorted PTokenName PInteger))
-> Term s (PMap 'Sorted PTokenName PInteger)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger))
   :--> PAsData (PMap 'Sorted PTokenName PInteger))
-> Term
     s
     (PBuiltinPair
        (PAsData PCurrencySymbol)
        (PAsData (PMap 'Sorted PTokenName PInteger)))
-> Term s (PAsData (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PCurrencySymbol)
     (PAsData (PMap 'Sorted PTokenName PInteger)))
mintAssetPair2)
                  PCons Term s (PBuiltinPair (PAsData PTokenName) (PAsData PInteger))
mintTokenPair2 Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens2Rest <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens2
                  PBuiltinList
  (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)) s
    -> Term s PBool)
-> Term s PBool
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PTokenName) (PAsData PInteger)))
mintTokens2Rest

                  (Term s (PAsData PCurrencySymbol)
mintCs2 Term s (PAsData PCurrencySymbol)
-> Term s (PAsData PCurrencySymbol) -> Term s PBool
forall (s :: S).
Term s (PAsData PCurrencySymbol)
-> Term s (PAsData PCurrencySymbol) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData PCurrencySymbol)
currencySymbol)
                    #&& ((pcountIf # isValidatorInput # pfromData inputs) #== 1)
                    #&& (pfromData (psndBuiltin # mintTokenPair2) #== 1)
              )
          PScriptInfo s
_ -> Term s PBool
forall (s :: S) (a :: PType). Term s a
perror

  Term s PBool -> Term s PUnit -> Term s PUnit -> Term s PUnit
forall (a :: PType) (s :: S).
Term s PBool -> Term s a -> Term s a -> Term s a
pif Term s PBool
valid (PUnit s -> Term s PUnit
forall (a :: PType) (s :: S). PlutusType a => a s -> Term s a
pcon PUnit s
forall (s :: S). PUnit s
PUnit) Term s PUnit
forall (s :: S) (a :: PType). Term s a
perror