{-# LANGUAGE TemplateHaskell #-}

{- |
Module     : Agora.Effect.TreasuryWithdrawal
Maintainer : seungheon.ooh@gmail.com
Description: An Effect that withdraws treasury deposit

An Effect that withdraws treasury deposit
-}
module Agora.Effect.TreasuryWithdrawal (
  TreasuryWithdrawalDatum (..),
  PTreasuryWithdrawalDatum (..),
  treasuryWithdrawalValidator,
) where

import Agora.Effect (makeEffect)
import Agora.Plutarch.Orphans ()
import Agora.Utils (isPubKey)
import GHC.Generics qualified as GHC
import Generics.SOP (Generic, I (I))
import Plutarch.Api.V1 (
  AmountGuarantees (Positive),
  KeyGuarantees (Sorted),
  PCredential (..),
  PTuple,
  PValidator,
  PValue,
  ptuple,
 )
import Plutarch.Api.V1.ScriptContext (pfindTxInByTxOutRef)
import "plutarch" Plutarch.Api.V1.Value (pnormalize)
import Plutarch.DataRepr (
  DerivePConstantViaData (..),
  PDataFields,
  PIsDataReprInstances (..),
 )
import Plutarch.Extra.TermCont (pguardC, pletC, pmatchC)
import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (..))
import PlutusLedgerApi.V1.Credential (Credential)
import PlutusLedgerApi.V1.Value (CurrencySymbol, Value)
import PlutusTx qualified

{- | Datum that encodes behavior of Treasury Withdrawal effect.

     Note: This Datum acts like a "predefined redeemer". Which is to say that
     it encodes the properties a redeemer would, but is locked in-place until
     spend.

     @since 0.1.0
-}
data TreasuryWithdrawalDatum = TreasuryWithdrawalDatum
  { TreasuryWithdrawalDatum -> [(Credential, Value)]
receivers :: [(Credential, Value)]
  -- ^ AssocMap for Value sent to each receiver from the treasury.
  , TreasuryWithdrawalDatum -> [Credential]
treasuries :: [Credential]
  -- ^ What Credentials is spending from legal.
  }
  deriving stock
    ( -- | @since 0.1.0
      Int -> TreasuryWithdrawalDatum -> ShowS
[TreasuryWithdrawalDatum] -> ShowS
TreasuryWithdrawalDatum -> String
(Int -> TreasuryWithdrawalDatum -> ShowS)
-> (TreasuryWithdrawalDatum -> String)
-> ([TreasuryWithdrawalDatum] -> ShowS)
-> Show TreasuryWithdrawalDatum
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TreasuryWithdrawalDatum] -> ShowS
$cshowList :: [TreasuryWithdrawalDatum] -> ShowS
show :: TreasuryWithdrawalDatum -> String
$cshow :: TreasuryWithdrawalDatum -> String
showsPrec :: Int -> TreasuryWithdrawalDatum -> ShowS
$cshowsPrec :: Int -> TreasuryWithdrawalDatum -> ShowS
Show
    , -- | @since 0.1.0
      (forall x.
 TreasuryWithdrawalDatum -> Rep TreasuryWithdrawalDatum x)
-> (forall x.
    Rep TreasuryWithdrawalDatum x -> TreasuryWithdrawalDatum)
-> Generic TreasuryWithdrawalDatum
forall x. Rep TreasuryWithdrawalDatum x -> TreasuryWithdrawalDatum
forall x. TreasuryWithdrawalDatum -> Rep TreasuryWithdrawalDatum x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TreasuryWithdrawalDatum x -> TreasuryWithdrawalDatum
$cfrom :: forall x. TreasuryWithdrawalDatum -> Rep TreasuryWithdrawalDatum x
GHC.Generic
    )
  deriving anyclass
    ( -- | @since 0.1.0
      All @[Type] (SListI @Type) (Code TreasuryWithdrawalDatum)
All @[Type] (SListI @Type) (Code TreasuryWithdrawalDatum)
-> (TreasuryWithdrawalDatum -> Rep TreasuryWithdrawalDatum)
-> (Rep TreasuryWithdrawalDatum -> TreasuryWithdrawalDatum)
-> Generic TreasuryWithdrawalDatum
Rep TreasuryWithdrawalDatum -> TreasuryWithdrawalDatum
TreasuryWithdrawalDatum -> Rep TreasuryWithdrawalDatum
forall a.
All @[Type] (SListI @Type) (Code a)
-> (a -> Rep a) -> (Rep a -> a) -> Generic a
to :: Rep TreasuryWithdrawalDatum -> TreasuryWithdrawalDatum
$cto :: Rep TreasuryWithdrawalDatum -> TreasuryWithdrawalDatum
from :: TreasuryWithdrawalDatum -> Rep TreasuryWithdrawalDatum
$cfrom :: TreasuryWithdrawalDatum -> Rep TreasuryWithdrawalDatum
Generic
    )

-- | @since 0.1.0
PlutusTx.makeLift ''TreasuryWithdrawalDatum

-- | @since 0.1.0
PlutusTx.makeIsDataIndexed ''TreasuryWithdrawalDatum [('TreasuryWithdrawalDatum, 0)]

{- | Haskell-level version of 'TreasuryWithdrawalDatum'.

     @since 0.1.0
-}
newtype PTreasuryWithdrawalDatum (s :: S)
  = PTreasuryWithdrawalDatum
      ( Term
          s
          ( PDataRecord
              '[ "receivers" ':= PBuiltinList (PAsData (PTuple PCredential (PValue 'Sorted 'Positive)))
               , "treasuries" ':= PBuiltinList (PAsData PCredential)
               ]
          )
      )
  deriving stock
    ( -- | @since 0.1.0
      (forall x.
 PTreasuryWithdrawalDatum s -> Rep (PTreasuryWithdrawalDatum s) x)
-> (forall x.
    Rep (PTreasuryWithdrawalDatum s) x -> PTreasuryWithdrawalDatum s)
-> Generic (PTreasuryWithdrawalDatum s)
forall x.
Rep (PTreasuryWithdrawalDatum s) x -> PTreasuryWithdrawalDatum s
forall x.
PTreasuryWithdrawalDatum s -> Rep (PTreasuryWithdrawalDatum s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: S) x.
Rep (PTreasuryWithdrawalDatum s) x -> PTreasuryWithdrawalDatum s
forall (s :: S) x.
PTreasuryWithdrawalDatum s -> Rep (PTreasuryWithdrawalDatum s) x
$cto :: forall (s :: S) x.
Rep (PTreasuryWithdrawalDatum s) x -> PTreasuryWithdrawalDatum s
$cfrom :: forall (s :: S) x.
PTreasuryWithdrawalDatum s -> Rep (PTreasuryWithdrawalDatum s) x
GHC.Generic
    )
  deriving anyclass
    ( -- | @since 0.1.0
      All @[Type] (SListI @Type) (Code (PTreasuryWithdrawalDatum s))
All @[Type] (SListI @Type) (Code (PTreasuryWithdrawalDatum s))
-> (PTreasuryWithdrawalDatum s -> Rep (PTreasuryWithdrawalDatum s))
-> (Rep (PTreasuryWithdrawalDatum s) -> PTreasuryWithdrawalDatum s)
-> Generic (PTreasuryWithdrawalDatum s)
Rep (PTreasuryWithdrawalDatum s) -> PTreasuryWithdrawalDatum s
PTreasuryWithdrawalDatum s -> Rep (PTreasuryWithdrawalDatum 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 (PTreasuryWithdrawalDatum s))
forall (s :: S).
Rep (PTreasuryWithdrawalDatum s) -> PTreasuryWithdrawalDatum s
forall (s :: S).
PTreasuryWithdrawalDatum s -> Rep (PTreasuryWithdrawalDatum s)
to :: Rep (PTreasuryWithdrawalDatum s) -> PTreasuryWithdrawalDatum s
$cto :: forall (s :: S).
Rep (PTreasuryWithdrawalDatum s) -> PTreasuryWithdrawalDatum s
from :: PTreasuryWithdrawalDatum s -> Rep (PTreasuryWithdrawalDatum s)
$cfrom :: forall (s :: S).
PTreasuryWithdrawalDatum s -> Rep (PTreasuryWithdrawalDatum s)
Generic
    , -- | @since 0.1.0
      PIsData PTreasuryWithdrawalDatum
PlutusType PTreasuryWithdrawalDatum
PlutusType PTreasuryWithdrawalDatum
-> PIsData PTreasuryWithdrawalDatum
-> (forall (s :: S).
    PTreasuryWithdrawalDatum s
    -> Term s (PDataSum (PIsDataReprRepr PTreasuryWithdrawalDatum)))
-> (forall (s :: S) (b :: PType).
    Term s (PDataSum (PIsDataReprRepr PTreasuryWithdrawalDatum))
    -> (PTreasuryWithdrawalDatum s -> Term s b) -> Term s b)
-> PIsDataRepr PTreasuryWithdrawalDatum
forall (s :: S).
PTreasuryWithdrawalDatum s
-> Term s (PDataSum (PIsDataReprRepr PTreasuryWithdrawalDatum))
forall (s :: S) (b :: PType).
Term s (PDataSum (PIsDataReprRepr PTreasuryWithdrawalDatum))
-> (PTreasuryWithdrawalDatum s -> Term s b) -> Term s b
forall (a :: PType).
PlutusType a
-> PIsData a
-> (forall (s :: S). a s -> Term s (PDataSum (PIsDataReprRepr a)))
-> (forall (s :: S) (b :: PType).
    Term s (PDataSum (PIsDataReprRepr a))
    -> (a s -> Term s b) -> Term s b)
-> PIsDataRepr a
pmatchRepr :: forall (s :: S) (b :: PType).
Term s (PDataSum (PIsDataReprRepr PTreasuryWithdrawalDatum))
-> (PTreasuryWithdrawalDatum s -> Term s b) -> Term s b
$cpmatchRepr :: forall (s :: S) (b :: PType).
Term s (PDataSum (PIsDataReprRepr PTreasuryWithdrawalDatum))
-> (PTreasuryWithdrawalDatum s -> Term s b) -> Term s b
pconRepr :: forall (s :: S).
PTreasuryWithdrawalDatum s
-> Term s (PDataSum (PIsDataReprRepr PTreasuryWithdrawalDatum))
$cpconRepr :: forall (s :: S).
PTreasuryWithdrawalDatum s
-> Term s (PDataSum (PIsDataReprRepr PTreasuryWithdrawalDatum))
PIsDataRepr
    )
  deriving
    ( -- | @since 0.1.0
      PCon PTreasuryWithdrawalDatum
PMatch PTreasuryWithdrawalDatum
PCon PTreasuryWithdrawalDatum
-> PMatch PTreasuryWithdrawalDatum
-> (forall (s :: S) (b :: PType).
    PTreasuryWithdrawalDatum s
    -> Term s (PInner PTreasuryWithdrawalDatum b))
-> (forall (s :: S) (b :: PType).
    Term s (PInner PTreasuryWithdrawalDatum b)
    -> (PTreasuryWithdrawalDatum s -> Term s b) -> Term s b)
-> PlutusType PTreasuryWithdrawalDatum
forall (s :: S) (b :: PType).
Term s (PInner PTreasuryWithdrawalDatum b)
-> (PTreasuryWithdrawalDatum s -> Term s b) -> Term s b
forall (s :: S) (b :: PType).
PTreasuryWithdrawalDatum s
-> Term s (PInner PTreasuryWithdrawalDatum b)
forall (a :: PType).
PCon a
-> PMatch a
-> (forall (s :: S) (b :: PType). a s -> Term s (PInner a b))
-> (forall (s :: S) (b :: PType).
    Term s (PInner a b) -> (a s -> Term s b) -> Term s b)
-> PlutusType a
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PTreasuryWithdrawalDatum b)
-> (PTreasuryWithdrawalDatum s -> Term s b) -> Term s b
$cpmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PTreasuryWithdrawalDatum b)
-> (PTreasuryWithdrawalDatum s -> Term s b) -> Term s b
pcon' :: forall (s :: S) (b :: PType).
PTreasuryWithdrawalDatum s
-> Term s (PInner PTreasuryWithdrawalDatum b)
$cpcon' :: forall (s :: S) (b :: PType).
PTreasuryWithdrawalDatum s
-> Term s (PInner PTreasuryWithdrawalDatum b)
PlutusType
    , -- | @since 0.1.0
      (forall (s :: S).
 Term s (PAsData PTreasuryWithdrawalDatum)
 -> Term s PTreasuryWithdrawalDatum)
-> (forall (s :: S).
    Term s PTreasuryWithdrawalDatum -> Term s PData)
-> PIsData PTreasuryWithdrawalDatum
forall (s :: S).
Term s (PAsData PTreasuryWithdrawalDatum)
-> Term s PTreasuryWithdrawalDatum
forall (s :: S). Term s PTreasuryWithdrawalDatum -> 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
pdataImpl :: forall (s :: S). Term s PTreasuryWithdrawalDatum -> Term s PData
$cpdataImpl :: forall (s :: S). Term s PTreasuryWithdrawalDatum -> Term s PData
pfromDataImpl :: forall (s :: S).
Term s (PAsData PTreasuryWithdrawalDatum)
-> Term s PTreasuryWithdrawalDatum
$cpfromDataImpl :: forall (s :: S).
Term s (PAsData PTreasuryWithdrawalDatum)
-> Term s PTreasuryWithdrawalDatum
PIsData
    , -- | @since 0.1.0
      (forall (s :: S).
 Term s PTreasuryWithdrawalDatum
 -> Term s (PDataRecord (PFields PTreasuryWithdrawalDatum)))
-> PDataFields PTreasuryWithdrawalDatum
forall (s :: S).
Term s PTreasuryWithdrawalDatum
-> Term s (PDataRecord (PFields PTreasuryWithdrawalDatum))
forall (a :: PType).
(forall (s :: S). Term s a -> Term s (PDataRecord (PFields a)))
-> PDataFields a
ptoFields :: forall (s :: S).
Term s PTreasuryWithdrawalDatum
-> Term s (PDataRecord (PFields PTreasuryWithdrawalDatum))
$cptoFields :: forall (s :: S).
Term s PTreasuryWithdrawalDatum
-> Term s (PDataRecord (PFields PTreasuryWithdrawalDatum))
PDataFields
    )
    via PIsDataReprInstances PTreasuryWithdrawalDatum

-- | @since 0.1.0
instance PUnsafeLiftDecl PTreasuryWithdrawalDatum where
  type PLifted PTreasuryWithdrawalDatum = TreasuryWithdrawalDatum

-- | @since 0.1.0
deriving via
  (DerivePConstantViaData TreasuryWithdrawalDatum PTreasuryWithdrawalDatum)
  instance
    (PConstantDecl TreasuryWithdrawalDatum)

-- | @since 0.1.0
deriving via
  PAsData (PIsDataReprInstances PTreasuryWithdrawalDatum)
  instance
    PTryFrom PData (PAsData PTreasuryWithdrawalDatum)

{- | Withdraws given list of values to specific target addresses.
     It can be evoked by burning GAT. The transaction should have correct
     outputs to the users and any left overs should be paid back to the treasury.

     The validator does not accept any Redeemer as all "parameters" are provided
     via encoded Datum.

     NOTE: It should check...

       1. Transaction outputs should contain all of what Datum specified

       2. Left over assets should be redirected back to Treasury

     It can be more flexiable over...

     - The number of outputs themselves

     @since 0.1.0
-}
treasuryWithdrawalValidator :: forall {s :: S}. CurrencySymbol -> Term s PValidator
treasuryWithdrawalValidator :: forall {s :: S}. CurrencySymbol -> Term s PValidator
treasuryWithdrawalValidator CurrencySymbol
currSymbol = CurrencySymbol
-> (forall (s :: S).
    Term s PCurrencySymbol
    -> Term s PTreasuryWithdrawalDatum
    -> Term s PTxOutRef
    -> Term s (PAsData PTxInfo)
    -> Term s POpaque)
-> ClosedTerm PValidator
forall (datum :: PType).
(PIsData datum, PTryFrom PData (PAsData datum)) =>
CurrencySymbol
-> (forall (s :: S).
    Term s PCurrencySymbol
    -> Term s datum
    -> Term s PTxOutRef
    -> Term s (PAsData PTxInfo)
    -> Term s POpaque)
-> ClosedTerm PValidator
makeEffect CurrencySymbol
currSymbol ((forall (s :: S).
  Term s PCurrencySymbol
  -> Term s PTreasuryWithdrawalDatum
  -> Term s PTxOutRef
  -> Term s (PAsData PTxInfo)
  -> Term s POpaque)
 -> ClosedTerm PValidator)
-> (forall (s :: S).
    Term s PCurrencySymbol
    -> Term s PTreasuryWithdrawalDatum
    -> Term s PTxOutRef
    -> Term s (PAsData PTxInfo)
    -> Term s POpaque)
-> ClosedTerm PValidator
forall a b. (a -> b) -> a -> b
$
  \Term s PCurrencySymbol
_cs (Term s PTreasuryWithdrawalDatum
datum' :: Term _ PTreasuryWithdrawalDatum) Term s PTxOutRef
txOutRef' Term s (PAsData PTxInfo)
txInfo' -> 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)
     '("receivers",
       Term
         s
         (PAsData
            (PBuiltinList
               (PAsData (PTuple PCredential (PValue 'Sorted 'Positive))))))
     ((':)
        @(Symbol, Type)
        '("treasuries",
          Term s (PAsData (PBuiltinList (PAsData PCredential))))
        ('[] @(Symbol, Type))))
datum <- ((HRec
    ((':)
       @(Symbol, Type)
       '("receivers",
         Term
           s
           (PAsData
              (PBuiltinList
                 (PAsData (PTuple PCredential (PValue 'Sorted 'Positive))))))
       ((':)
          @(Symbol, Type)
          '("treasuries",
            Term s (PAsData (PBuiltinList (PAsData PCredential))))
          ('[] @(Symbol, Type))))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("receivers",
             Term
               s
               (PAsData
                  (PBuiltinList
                     (PAsData (PTuple PCredential (PValue 'Sorted 'Positive))))))
           ((':)
              @(Symbol, Type)
              '("treasuries",
                Term s (PAsData (PBuiltinList (PAsData PCredential))))
              ('[] @(Symbol, Type)))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("receivers",
          Term
            s
            (PAsData
               (PBuiltinList
                  (PAsData (PTuple PCredential (PValue 'Sorted 'Positive))))))
        ((':)
           @(Symbol, Type)
           '("treasuries",
             Term s (PAsData (PBuiltinList (PAsData PCredential))))
           ('[] @(Symbol, Type))))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("receivers",
              Term
                s
                (PAsData
                   (PBuiltinList
                      (PAsData (PTuple PCredential (PValue 'Sorted 'Positive))))))
            ((':)
               @(Symbol, Type)
               '("treasuries",
                 Term s (PAsData (PBuiltinList (PAsData PCredential))))
               ('[] @(Symbol, Type))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("receivers",
            Term
              s
              (PAsData
                 (PBuiltinList
                    (PAsData (PTuple PCredential (PValue 'Sorted 'Positive))))))
          ((':)
             @(Symbol, Type)
             '("treasuries",
               Term s (PAsData (PBuiltinList (PAsData PCredential))))
             ('[] @(Symbol, Type))))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("receivers",
             Term
               s
               (PAsData
                  (PBuiltinList
                     (PAsData (PTuple PCredential (PValue 'Sorted 'Positive))))))
           ((':)
              @(Symbol, Type)
              '("treasuries",
                Term s (PAsData (PBuiltinList (PAsData PCredential))))
              ('[] @(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 @'["receivers", "treasuries"] Term s PTreasuryWithdrawalDatum
datum'
    HRec
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ((':)
        @(Symbol, Type)
        '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
        ('[] @(Symbol, Type))))
txInfo <- ((HRec
    ((':)
       @(Symbol, Type)
       '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
       ((':)
          @(Symbol, Type)
          '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
          ('[] @(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)))))
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))))
   -> 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))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
          ((':)
             @(Symbol, Type)
             '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
             ('[] @(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)))))
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 @'["outputs", "inputs"] Term s (PAsData PTxInfo)
txInfo'
    PJust ((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 @"resolved" #) -> Term s (PAsData PTxOut)
txOut) <- Term s (PMaybe PTxInInfo)
-> TermCont @POpaque s (PMaybe PTxInInfo s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC (Term s (PMaybe PTxInInfo)
 -> TermCont @POpaque s (PMaybe PTxInInfo s))
-> Term s (PMaybe PTxInInfo)
-> TermCont @POpaque s (PMaybe PTxInInfo s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PTxOutRef
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo))
forall (s :: S).
Term
  s
  (PTxOutRef
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo))
pfindTxInByTxOutRef Term
  s
  (PTxOutRef
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo))
-> Term s PTxOutRef
-> Term s (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PTxOutRef
txOutRef' Term s (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo)
-> Term s (PBuiltinList (PAsData PTxInInfo))
-> Term s (PMaybe PTxInInfo)
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 HRec
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ((':)
        @(Symbol, Type)
        '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
        ('[] @(Symbol, Type))))
txInfo.inputs
    HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
     s)
effInput <- ((HRec
    (BoundTerms
       (PFields (PAsData PTxOut))
       (Bindings
          (PFields (PAsData PTxOut))
          ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
       s)
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
           s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     (BoundTerms
        (PFields (PAsData PTxOut))
        (Bindings
           (PFields (PAsData PTxOut))
           ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
        s)
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         (BoundTerms
            (PFields (PAsData PTxOut))
            (Bindings
               (PFields (PAsData PTxOut))
               ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PAsData PTxOut))
          (Bindings
             (PFields (PAsData PTxOut))
             ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
          s)
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
           s))
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 (PAsData PTxOut)
 -> (HRec
       (BoundTerms
          (PFields (PAsData PTxOut))
          (Bindings
             (PFields (PAsData PTxOut))
             ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
          s)
     -> Term s POpaque)
 -> Term s POpaque)
-> Term s (PAsData PTxOut)
-> (HRec
      (BoundTerms
         (PFields (PAsData PTxOut))
         (Bindings
            (PFields (PAsData PTxOut))
            ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
         s)
    -> Term s POpaque)
-> Term s POpaque
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PTxOut)
txOut
    Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))))
outputValues <-
      Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))))
-> TermCont
     @POpaque
     s
     (Term
        s
        (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term
   s
   (PBuiltinList
      (PAsData
         (PTuple
            (PUnLabel
               (IndexList
                  @PLabeledType
                  (PLabelIndex "credential" (PFields PAddress))
                  (PFields PAddress)))
            (PValue 'Sorted 'Positive))))
 -> TermCont
      @POpaque
      s
      (Term
         s
         (PBuiltinList
            (PAsData
               (PTuple
                  (PUnLabel
                     (IndexList
                        @PLabeledType
                        (PLabelIndex "credential" (PFields PAddress))
                        (PFields PAddress)))
                  (PValue 'Sorted 'Positive))))))
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
-> TermCont
     @POpaque
     s
     (Term
        s
        (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))))
forall a b. (a -> b) -> a -> b
$
        Term
  s
  ((PAsData PTxOut
    :--> PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive)))
   :--> (PBuiltinList (PAsData PTxOut)
         :--> PBuiltinList
                (PAsData
                   (PTuple
                      (PUnLabel
                         (IndexList
                            @PLabeledType
                            (PLabelIndex "credential" (PFields PAddress))
                            (PFields PAddress)))
                      (PValue 'Sorted 'Positive)))))
forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap
          # plam
            ( \(pfromData -> txOut') -> unTermCont $ do
                txOut <- tcont $ pletFields @'["address", "value"] $ txOut'
                let cred = pfield @"credential" # pfromData txOut.address
                pure . pdata $ ptuple # cred # txOut.value
            )
          # txInfo.outputs
    Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))))
inputValues <-
      Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))))
-> TermCont
     @POpaque
     s
     (Term
        s
        (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term
   s
   (PBuiltinList
      (PAsData
         (PTuple
            (PUnLabel
               (IndexList
                  @PLabeledType
                  (PLabelIndex "credential" (PFields PAddress))
                  (PFields PAddress)))
            (PValue 'Sorted 'Positive))))
 -> TermCont
      @POpaque
      s
      (Term
         s
         (PBuiltinList
            (PAsData
               (PTuple
                  (PUnLabel
                     (IndexList
                        @PLabeledType
                        (PLabelIndex "credential" (PFields PAddress))
                        (PFields PAddress)))
                  (PValue 'Sorted 'Positive))))))
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
-> TermCont
     @POpaque
     s
     (Term
        s
        (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))))
forall a b. (a -> b) -> a -> b
$
        Term
  s
  ((PAsData PTxInInfo
    :--> PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive)))
   :--> (PBuiltinList (PAsData PTxInInfo)
         :--> PBuiltinList
                (PAsData
                   (PTuple
                      (PUnLabel
                         (IndexList
                            @PLabeledType
                            (PLabelIndex "credential" (PFields PAddress))
                            (PFields PAddress)))
                      (PValue 'Sorted 'Positive)))))
forall (list :: PType -> PType) (a :: PType) (b :: PType) (s :: S).
(PListLike list, PElemConstraint list a, PElemConstraint list b) =>
Term s ((a :--> b) :--> (list a :--> list b))
pmap
          # plam
            ( \((pfield @"resolved" #) . pfromData -> txOut') -> unTermCont $ do
                txOut <- tcont $ pletFields @'["address", "value"] $ txOut'
                let cred = pfield @"credential" # pfromData txOut.address
                pure . pdata $ ptuple # cred # txOut.value
            )
          # txInfo.inputs
    let ofTreasury :: Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PBuiltinList
          (PAsData
             (PTuple
                (PUnLabel
                   (IndexList
                      @PLabeledType
                      (PLabelIndex "credential" (PFields PAddress))
                      (PFields PAddress)))
                (PValue 'Sorted 'Positive))))
ofTreasury =
          Term
  s
  ((PAsData
      (PTuple
         (PUnLabel
            (IndexList
               @PLabeledType
               (PLabelIndex "credential" (PFields PAddress))
               (PFields PAddress)))
         (PValue 'Sorted 'Positive))
    :--> PBool)
   :--> (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))
         :--> PBuiltinList
                (PAsData
                   (PTuple
                      (PUnLabel
                         (IndexList
                            @PLabeledType
                            (PLabelIndex "credential" (PFields PAddress))
                            (PFields PAddress)))
                      (PValue 'Sorted 'Positive)))))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> list a))
pfilter
            # plam (\((pfield @"_0" #) . pfromData -> cred) -> pelem # cred # datum.treasuries)
        sumValues :: Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
sumValues = ClosedTerm
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive)))
      :--> PValue 'Sorted 'NonZero)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (PBuiltinList
      (PAsData
         (PTuple
            (PUnLabel
               (IndexList
                  @PLabeledType
                  (PLabelIndex "credential" (PFields PAddress))
                  (PFields PAddress)))
            (PValue 'Sorted 'Positive)))
    :--> PValue 'Sorted 'NonZero)
 -> Term
      s
      (PBuiltinList
         (PAsData
            (PTuple
               (PUnLabel
                  (IndexList
                     @PLabeledType
                     (PLabelIndex "credential" (PFields PAddress))
                     (PFields PAddress)))
               (PValue 'Sorted 'Positive)))
       :--> PValue 'Sorted 'NonZero))
-> ClosedTerm
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive)))
      :--> PValue 'Sorted 'NonZero)
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive)))
      :--> PValue 'Sorted 'NonZero)
forall a b. (a -> b) -> a -> b
$
          (Term
   s
   (PBuiltinList
      (PAsData
         (PTuple
            (PUnLabel
               (IndexList
                  @PLabeledType
                  (PLabelIndex "credential" (PFields PAddress))
                  (PFields PAddress)))
            (PValue 'Sorted 'Positive))))
 -> Term s (PValue 'Sorted 'NonZero))
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive)))
      :--> PValue 'Sorted 'NonZero)
forall a (b :: PType) (s :: S) (c :: PType).
PLamN a b s =>
(Term s c -> a) -> Term s (c :--> b)
plam ((Term
    s
    (PBuiltinList
       (PAsData
          (PTuple
             (PUnLabel
                (IndexList
                   @PLabeledType
                   (PLabelIndex "credential" (PFields PAddress))
                   (PFields PAddress)))
             (PValue 'Sorted 'Positive))))
  -> Term s (PValue 'Sorted 'NonZero))
 -> Term
      s
      (PBuiltinList
         (PAsData
            (PTuple
               (PUnLabel
                  (IndexList
                     @PLabeledType
                     (PLabelIndex "credential" (PFields PAddress))
                     (PFields PAddress)))
               (PValue 'Sorted 'Positive)))
       :--> PValue 'Sorted 'NonZero))
-> (Term
      s
      (PBuiltinList
         (PAsData
            (PTuple
               (PUnLabel
                  (IndexList
                     @PLabeledType
                     (PLabelIndex "credential" (PFields PAddress))
                     (PFields PAddress)))
               (PValue 'Sorted 'Positive))))
    -> Term s (PValue 'Sorted 'NonZero))
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive)))
      :--> PValue 'Sorted 'NonZero)
forall a b. (a -> b) -> a -> b
$ \Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))))
v ->
            Term s (PValue 'Sorted 'Positive :--> PValue 'Sorted 'NonZero)
forall (s :: S) {w :: AmountGuarantees}.
Term s (PValue 'Sorted w :--> PValue 'Sorted 'NonZero)
pnormalize
              #$ pfoldr
              # plam (\(pfromData . (pfield @"_1" #) -> x) y -> x <> y)
              # mempty
              # v
        treasuryInputValuesSum :: Term s (PValue 'Sorted 'NonZero)
treasuryInputValuesSum = Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
ClosedTerm
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
sumValues Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
-> Term s (PValue 'Sorted 'NonZero)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PBuiltinList
          (PAsData
             (PTuple
                (PUnLabel
                   (IndexList
                      @PLabeledType
                      (PLabelIndex "credential" (PFields PAddress))
                      (PFields PAddress)))
                (PValue 'Sorted 'Positive))))
ofTreasury Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PBuiltinList
          (PAsData
             (PTuple
                (PUnLabel
                   (IndexList
                      @PLabeledType
                      (PLabelIndex "credential" (PFields PAddress))
                      (PFields PAddress)))
                (PValue 'Sorted 'Positive))))
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))))
inputValues
        treasuryOutputValuesSum :: Term s (PValue 'Sorted 'NonZero)
treasuryOutputValuesSum = Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
ClosedTerm
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
sumValues Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
-> Term s (PValue 'Sorted 'NonZero)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PBuiltinList
          (PAsData
             (PTuple
                (PUnLabel
                   (IndexList
                      @PLabeledType
                      (PLabelIndex "credential" (PFields PAddress))
                      (PFields PAddress)))
                (PValue 'Sorted 'Positive))))
ofTreasury Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PBuiltinList
          (PAsData
             (PTuple
                (PUnLabel
                   (IndexList
                      @PLabeledType
                      (PLabelIndex "credential" (PFields PAddress))
                      (PFields PAddress)))
                (PValue 'Sorted 'Positive))))
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))))
outputValues
        receiverValuesSum :: Term s (PValue 'Sorted 'NonZero)
receiverValuesSum = Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
ClosedTerm
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
sumValues Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PValue 'Sorted 'NonZero)
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
-> Term s (PValue 'Sorted 'NonZero)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  ((':)
     @(Symbol, Type)
     '("receivers",
       Term
         s
         (PAsData
            (PBuiltinList
               (PAsData (PTuple PCredential (PValue 'Sorted 'Positive))))))
     ((':)
        @(Symbol, Type)
        '("treasuries",
          Term s (PAsData (PBuiltinList (PAsData PCredential))))
        ('[] @(Symbol, Type))))
datum.receivers
        -- Constraints
        outputContentMatchesRecivers :: Term s PBool
outputContentMatchesRecivers =
          Term
  s
  ((PAsData
      (PTuple
         (PUnLabel
            (IndexList
               @PLabeledType
               (PLabelIndex "credential" (PFields PAddress))
               (PFields PAddress)))
         (PValue 'Sorted 'Positive))
    :--> PBool)
   :--> (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))
         :--> PBool))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pall Term
  s
  ((PAsData
      (PTuple
         (PUnLabel
            (IndexList
               @PLabeledType
               (PLabelIndex "credential" (PFields PAddress))
               (PFields PAddress)))
         (PValue 'Sorted 'Positive))
    :--> PBool)
   :--> (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))
         :--> PBool))
-> Term
     s
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))
      :--> PBool)
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive)))
      :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (Term
   s
   (PAsData
      (PTuple
         (PUnLabel
            (IndexList
               @PLabeledType
               (PLabelIndex "credential" (PFields PAddress))
               (PFields PAddress)))
         (PValue 'Sorted 'Positive)))
 -> Term s PBool)
-> Term
     s
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))
      :--> PBool)
forall a (b :: PType) (s :: S) (c :: PType).
PLamN a b s =>
(Term s c -> a) -> Term s (c :--> b)
plam (\Term
  s
  (PAsData
     (PTuple
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "credential" (PFields PAddress))
              (PFields PAddress)))
        (PValue 'Sorted 'Positive)))
out -> Term
  s
  (PAsData
     (PTuple
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "credential" (PFields PAddress))
              (PFields PAddress)))
        (PValue 'Sorted 'Positive))
   :--> (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))
         :--> PBool))
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PIsListLike list a, PEq a) =>
Term s (a :--> (list a :--> PBool))
pelem Term
  s
  (PAsData
     (PTuple
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "credential" (PFields PAddress))
              (PFields PAddress)))
        (PValue 'Sorted 'Positive))
   :--> (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))
         :--> PBool))
-> Term
     s
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive)))
      :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PAsData
     (PTuple
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "credential" (PFields PAddress))
              (PFields PAddress)))
        (PValue 'Sorted 'Positive)))
out Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive)))
   :--> PBool)
-> Term
     s
     (PBuiltinList
        (PAsData
           (PTuple
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "credential" (PFields PAddress))
                    (PFields PAddress)))
              (PValue 'Sorted 'Positive))))
-> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinList
     (PAsData
        (PTuple
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "credential" (PFields PAddress))
                 (PFields PAddress)))
           (PValue 'Sorted 'Positive))))
outputValues)
            #$ datum.receivers
        excessShouldBePaidToInputs :: Term s PBool
excessShouldBePaidToInputs =
          Term s (PValue 'Sorted 'NonZero)
treasuryOutputValuesSum Term s (PValue 'Sorted 'NonZero)
-> Term s (PValue 'Sorted 'NonZero)
-> Term s (PValue 'Sorted 'NonZero)
forall a. Semigroup a => a -> a -> a
<> Term s (PValue 'Sorted 'NonZero)
receiverValuesSum Term s (PValue 'Sorted 'NonZero)
-> Term s (PValue 'Sorted 'NonZero) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PValue 'Sorted 'NonZero)
treasuryInputValuesSum
        shouldNotPayToEffect :: Term s PBool
shouldNotPayToEffect =
          Term s (PBool :--> PBool)
forall (s :: S). Term s (PBool :--> PBool)
pnot Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s 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))
pany
            # plam
              ( \x ->
                  effInput.address #== pfield @"address" # pfromData x
              )
            # pfromData txInfo.outputs
        inputsAreOnlyTreasuriesOrCollateral :: Term s PBool
inputsAreOnlyTreasuriesOrCollateral =
          Term
  s
  ((PAsData
      (PTuple
         (PUnLabel
            (IndexList
               @PLabeledType
               (PLabelIndex "credential" (PFields PAddress))
               (PFields PAddress)))
         (PValue 'Sorted 'Positive))
    :--> PBool)
   :--> (PBuiltinList
           (PAsData
              (PTuple
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "credential" (PFields PAddress))
                       (PFields PAddress)))
                 (PValue 'Sorted 'Positive)))
         :--> PBool))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pall
            # plam
              ( \((pfield @"_0" #) . pfromData -> cred) ->
                  cred #== pfield @"credential" # effInput.address
                    #|| pelem # cred # datum.treasuries
                    #|| isPubKey # pfromData cred
              )
            # inputValues

    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)
"Transaction should not pay to effects" Term s PBool
shouldNotPayToEffect
    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)
"Transaction output does not match receivers" Term s PBool
outputContentMatchesRecivers
    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)
"Remainders should be returned to the treasury" Term s PBool
excessShouldBePaidToInputs
    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)
"Transaction should only have treasuries specified in the datum as input" Term s PBool
inputsAreOnlyTreasuriesOrCollateral
    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 (PUnit @S) -> Term s POpaque)
-> Term s (PUnit @S)
-> TermCont @POpaque s (Term s POpaque)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PUnit @S) -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (Term s (PUnit @S) -> TermCont @POpaque s (Term s POpaque))
-> Term s (PUnit @S) -> TermCont @POpaque 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 ()