{- | This module was copied from the Liqwid-Labs/agora repo, and updated to work with Plutus V3 and Plutarch 1.10.1

 @since 1.0.0
-}
module Agora.AuthorityToken (singleAuthorityTokenBurned, authorityTokensValidIn) where

import Agora.Utils (psymbolValueOf)
import Plutarch.Builtin.Bool (PBool)
import Plutarch.LedgerApi.AssocMap qualified as AssocMap
import Plutarch.LedgerApi.V3 (
  AmountGuarantees,
  KeyGuarantees,
  PAddress (PAddress),
  PCredential (PPubKeyCredential, PScriptCredential),
  PCurrencySymbol,
  PTxInInfo (PTxInInfo),
  PTxOut (PTxOut),
  PValue (PValue),
 )
import Plutarch.Monadic qualified as P
import Plutarch.Prelude (
  PAsData,
  PBool (PTrue),
  PBuiltinList,
  PEq ((#==)),
  PInteger,
  PMaybe (PJust, PNothing),
  S,
  Term,
  pcon,
  pconstant,
  pfoldr,
  pfromData,
  phoistAcyclic,
  pif,
  plam,
  pmatch,
  ptraceInfoIfFalse,
  (#),
  (#&&),
  (:-->),
 )

{- | Check that all GATs are valid in a particular TxOut.

  WARNING: As of version 1.0.0, this has been weakened in order to be
  compatible with RATs. The token name is no longer checked, meaning that a
  GAT can escape from its effect script, if the effect script is vulnerable.
  In order to prevent this, all effect scripts should be implemented carefully,
  and ideally use the trusted effect base. See also 'Agora.Effect'.

  (before 1.0.0) 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 1.0.0
-}
authorityTokensValidIn :: forall (s :: S). 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, HasCallStack) =>
(Term s c -> a) -> Term s (c :--> b)
forall (c :: PType).
HasCallStack =>
(Term s c -> Term s PTxOut -> Term s PBool)
-> Term s (c :--> (PTxOut :--> PBool))
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 -> P.do
    PTxOut Term s PAddress
address Term s (PAsData (PValue 'Sorted 'Positive))
value 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
txOut
    PAddress Term s PCredential
credential 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
address
    PValue Term
  s (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger))
assetMap <- Term s (PValue 'Sorted 'Positive)
-> (PValue 'Sorted 'Positive 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 (PValue 'Sorted 'Positive)
 -> (PValue 'Sorted 'Positive s -> Term s PBool) -> Term s PBool)
-> Term s (PValue 'Sorted 'Positive)
-> (PValue 'Sorted 'Positive s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PAsData (PValue 'Sorted 'Positive))
-> Term s (PValue 'Sorted 'Positive)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (PValue 'Sorted 'Positive))
value
    Term s (PMaybe (PMap 'Sorted PTokenName PInteger))
-> (PMaybe (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
  (PCurrencySymbol
   :--> (PMap
           'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger)
         :--> PMaybe (PMap 'Sorted PTokenName PInteger)))
forall (k :: PType) (v :: PType) (any :: KeyGuarantees) (s :: S).
(PIsData k, PIsData v) =>
Term s (k :--> (PMap any k v :--> PMaybe v))
AssocMap.plookup Term
  s
  (PCurrencySymbol
   :--> (PMap
           'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger)
         :--> PMaybe (PMap 'Sorted PTokenName PInteger)))
-> Term s PCurrencySymbol
-> Term
     s
     (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger)
      :--> PMaybe (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
authorityTokenSym Term
  s
  (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger)
   :--> PMaybe (PMap 'Sorted PTokenName PInteger))
-> Term
     s (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger))
-> Term s (PMaybe (PMap 'Sorted PTokenName PInteger))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s (PMap 'Sorted PCurrencySymbol (PMap 'Sorted PTokenName PInteger))
assetMap) ((PMaybe (PMap 'Sorted PTokenName PInteger) s -> Term s PBool)
 -> Term s PBool)
-> (PMaybe (PMap 'Sorted PTokenName PInteger) s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ \case
      PJust Term s (PMap 'Sorted PTokenName PInteger)
_tokenMap ->
        -- TODO: This check only needs to happen for outputs, not inputs (performance)
        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
credential ((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 (PAsData PPubKeyHash)
_ ->
            -- GATs should only be sent to Effect validators
            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
"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
$ AsHaskell PBool -> Term s PBool
forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant Bool
AsHaskell PBool
False
          PScriptCredential Term s (PAsData PScriptHash)
_ ->
            -- NOTE: We no longer can perform a check on `TokenName` content here.
            -- Instead, the auth check system uses `TokenName`s, but it cannot
            -- check for GATs incorrectly escaping scripts. The effect scripts
            -- need to be written very carefully in order to disallow this.
            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
PTrue
      PMaybe (PMap 'Sorted PTokenName PInteger) s
PNothing ->
        -- No GATs exist at this output!
        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
PTrue

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

  @since 1.0.0
-}
singleAuthorityTokenBurned ::
  forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees) (s :: S).
  Term s PCurrencySymbol ->
  Term s (PBuiltinList (PAsData PTxInInfo)) ->
  Term s (PValue keys amounts) ->
  Term s PBool
singleAuthorityTokenBurned :: forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term s PCurrencySymbol
-> Term s (PBuiltinList (PAsData PTxInInfo))
-> Term s (PValue keys amounts)
-> Term s PBool
singleAuthorityTokenBurned Term s PCurrencySymbol
gatCs Term s (PBuiltinList (PAsData PTxInInfo))
inputs Term s (PValue keys amounts)
mint = P.do
  let gatAmountMinted :: Term _ PInteger
      gatAmountMinted :: Term s PInteger
gatAmountMinted = Term s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger))
psymbolValueOf Term s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger))
-> Term s PCurrencySymbol
-> Term s (PValue keys amounts :--> PInteger)
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)
-> Term s (PValue keys amounts) -> Term s PInteger
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PValue keys amounts)
mint

  let inputsWithGAT :: Term s PInteger
inputsWithGAT =
        Term
  s
  ((PAsData PTxInInfo :--> (PInteger :--> PInteger))
   :--> (PInteger
         :--> (PBuiltinList (PAsData PTxInInfo) :--> 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
            ( \input v -> pmatch (pfromData input) $ \case
                PTxInInfo _txOutRef resolved ->
                  pif
                    (authorityTokensValidIn # gatCs # resolved)
                    ( P.do
                        PTxOut _ value _ _ <- pmatch resolved

                        v + (psymbolValueOf # gatCs # pfromData value)
                    )
                    (P.fail "While counting GATs at inputs: all GATs must be valid")
            )
          # 0
          # inputs

  (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 PString -> Term s PBool -> Term s PBool
forall (s :: S). Term s PString -> Term s PBool -> Term s PBool
ptraceInfoIfFalse Term s PString
"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
gatAmountMinted 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
    , 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
"Only one GAT must exist at the inputs" (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$
        Term s PInteger
inputsWithGAT 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
    ]