{- | Agora DRep Voting Effect script

@since 1.0.0
-}
module Agora.Effect.Voting (votingEffectScript, VotingDatum (..)) where

import Agora.AuthorityToken (singleAuthorityTokenBurned)
import Data.Kind (Type)
import GHC.Generics qualified as GHC
import Generics.SOP qualified as SOP
import Plutarch.LedgerApi.V3 (
  PAddress (PAddress),
  PCredential (PScriptCredential),
  PCurrencySymbol,
  PDRepCredential (PDRepCredential),
  PDatum (PDatum),
  PDatumHash,
  PGovernanceActionId,
  PMap (PMap),
  PMaybeData (PDNothing),
  POutputDatum (POutputDatumHash),
  PScriptContext (PScriptContext),
  PScriptHash,
  PScriptInfo (PCertifyingScript, PSpendingScript, PVotingScript),
  PTxCert (PTxCertRegDRep),
  PTxInInfo (PTxInInfo),
  PTxInfo (PTxInfo),
  PTxOut (PTxOut),
  PVote,
  PVoter (PDRepVoter),
 )
import Plutarch.Maybe (pjust)
import Plutarch.Monadic qualified as P
import Plutarch.Prelude (
  ClosedTerm,
  PAsData,
  PBool (PFalse, PTrue),
  PBuiltinList (PCons, PNil),
  PData,
  PEq ((#==)),
  PIsData,
  PMaybe (PJust, PNothing),
  PTryFrom,
  PUnit (PUnit),
  PlutusType,
  S,
  Term,
  pcon,
  pconstant,
  perror,
  pfromData,
  pfstBuiltin,
  pif,
  plam,
  pmatch,
  precList,
  psndBuiltin,
  ptryFrom,
  tcont,
  unTermCont,
  (#),
  (#&&),
  (:-->),
 )
import Plutarch.Repr.Data (DeriveAsDataRec (DeriveAsDataRec))
import PlutusLedgerApi.V3 (
  FromData (fromBuiltinData),
  GovernanceActionId,
  Vote,
  toBuiltin,
  toData,
 )
import PlutusTx qualified
import PlutusTx.Builtins (chooseData, unsafeDataAsList)

{- | Haskell-level datum for the Voting Effect Validator script.

@since 1.0.0
-}
data VotingDatum = VotingDatum
  { VotingDatum -> GovernanceActionId
vdGovernanceActionId :: GovernanceActionId
  , VotingDatum -> Vote
vdVote :: Vote
  }

-- | @since 1.0.0
instance PlutusTx.FromData VotingDatum where
  {-# INLINEABLE fromBuiltinData #-}
  fromBuiltinData :: BuiltinData -> Maybe VotingDatum
fromBuiltinData BuiltinData
d =
    BuiltinData
-> (BuiltinData -> Maybe VotingDatum)
-> (BuiltinData -> Maybe VotingDatum)
-> (BuiltinData -> Maybe VotingDatum)
-> (BuiltinData -> Maybe VotingDatum)
-> (BuiltinData -> Maybe VotingDatum)
-> BuiltinData
-> Maybe VotingDatum
forall a. BuiltinData -> a -> a -> a -> a -> a -> a
chooseData
      BuiltinData
d
      (Maybe VotingDatum -> BuiltinData -> Maybe VotingDatum
forall a b. a -> b -> a
const Maybe VotingDatum
forall a. Maybe a
Nothing)
      (Maybe VotingDatum -> BuiltinData -> Maybe VotingDatum
forall a b. a -> b -> a
const Maybe VotingDatum
forall a. Maybe a
Nothing)
      ( \BuiltinData
d' ->
          case BuiltinData -> [BuiltinData]
unsafeDataAsList BuiltinData
d' of
            [BuiltinData
governanceActionId, BuiltinData
vote] ->
              GovernanceActionId -> Vote -> VotingDatum
VotingDatum
                (GovernanceActionId -> Vote -> VotingDatum)
-> Maybe GovernanceActionId -> Maybe (Vote -> VotingDatum)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinData -> Maybe GovernanceActionId
forall a. FromData a => BuiltinData -> Maybe a
fromBuiltinData BuiltinData
governanceActionId
                Maybe (Vote -> VotingDatum) -> Maybe Vote -> Maybe VotingDatum
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 Vote
forall a. FromData a => BuiltinData -> Maybe a
fromBuiltinData BuiltinData
vote
            [BuiltinData]
_ -> Maybe VotingDatum
forall a. Maybe a
Nothing
      )
      (Maybe VotingDatum -> BuiltinData -> Maybe VotingDatum
forall a b. a -> b -> a
const Maybe VotingDatum
forall a. Maybe a
Nothing)
      (Maybe VotingDatum -> BuiltinData -> Maybe VotingDatum
forall a b. a -> b -> a
const Maybe VotingDatum
forall a. Maybe a
Nothing)
      BuiltinData
d

-- | @since 1.0.0
instance PlutusTx.ToData VotingDatum where
  {-# INLINEABLE toBuiltinData #-}
  toBuiltinData :: VotingDatum -> BuiltinData
toBuiltinData (VotingDatum GovernanceActionId
governanceActionId Vote
vote) =
    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 [GovernanceActionId -> Data
forall a. ToData a => a -> Data
toData GovernanceActionId
governanceActionId, Vote -> Data
forall a. ToData a => a -> Data
toData Vote
vote]

{- | Voting Effect Datum

This script serves both validator script and certifying script purposes.

@since 1.0.0
-}
type PVotingDatum :: S -> Type
data PVotingDatum s = PVotingDatum
  { forall (s :: S).
PVotingDatum s -> Term s (PAsData PGovernanceActionId)
governanceActionId :: Term s (PAsData PGovernanceActionId)
  -- ^ Id of the governance action the vote is casted for
  , forall (s :: S). PVotingDatum s -> Term s (PAsData PVote)
vote :: Term s (PAsData PVote)
  -- ^ Vote for the governance action
  }
  deriving stock ((forall x. PVotingDatum s -> Rep (PVotingDatum s) x)
-> (forall x. Rep (PVotingDatum s) x -> PVotingDatum s)
-> Generic (PVotingDatum s)
forall x. Rep (PVotingDatum s) x -> PVotingDatum s
forall x. PVotingDatum s -> Rep (PVotingDatum s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: S) x. Rep (PVotingDatum s) x -> PVotingDatum s
forall (s :: S) x. PVotingDatum s -> Rep (PVotingDatum s) x
$cfrom :: forall (s :: S) x. PVotingDatum s -> Rep (PVotingDatum s) x
from :: forall x. PVotingDatum s -> Rep (PVotingDatum s) x
$cto :: forall (s :: S) x. Rep (PVotingDatum s) x -> PVotingDatum s
to :: forall x. Rep (PVotingDatum s) x -> PVotingDatum s
GHC.Generic)
  deriving anyclass (All @[Type] (SListI @Type) (Code (PVotingDatum s))
All @[Type] (SListI @Type) (Code (PVotingDatum s)) =>
(PVotingDatum s -> Rep (PVotingDatum s))
-> (Rep (PVotingDatum s) -> PVotingDatum s)
-> Generic (PVotingDatum s)
Rep (PVotingDatum s) -> PVotingDatum s
PVotingDatum s -> Rep (PVotingDatum 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 (PVotingDatum s))
forall (s :: S). Rep (PVotingDatum s) -> PVotingDatum s
forall (s :: S). PVotingDatum s -> Rep (PVotingDatum s)
$cfrom :: forall (s :: S). PVotingDatum s -> Rep (PVotingDatum s)
from :: PVotingDatum s -> Rep (PVotingDatum s)
$cto :: forall (s :: S). Rep (PVotingDatum s) -> PVotingDatum s
to :: Rep (PVotingDatum s) -> PVotingDatum s
SOP.Generic, (forall (s :: S).
 Term s PVotingDatum -> Term s PVotingDatum -> Term s PBool)
-> PEq PVotingDatum
forall (s :: S).
Term s PVotingDatum -> Term s PVotingDatum -> 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 PVotingDatum -> Term s PVotingDatum -> Term s PBool
#== :: forall (s :: S).
Term s PVotingDatum -> Term s PVotingDatum -> Term s PBool
PEq, (forall (s :: S).
 Term s (PAsData PVotingDatum) -> Term s PVotingDatum)
-> (forall (s :: S). Term s PVotingDatum -> Term s PData)
-> PIsData PVotingDatum
forall (s :: S).
Term s (PAsData PVotingDatum) -> Term s PVotingDatum
forall (s :: S). Term s PVotingDatum -> 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 PVotingDatum) -> Term s PVotingDatum
pfromDataImpl :: forall (s :: S).
Term s (PAsData PVotingDatum) -> Term s PVotingDatum
$cpdataImpl :: forall (s :: S). Term s PVotingDatum -> Term s PData
pdataImpl :: forall (s :: S). Term s PVotingDatum -> Term s PData
PIsData)
  deriving ((forall (s :: S). PVotingDatum s -> Term s (PInner PVotingDatum))
-> (forall (s :: S) (b :: PType).
    Term s (PInner PVotingDatum)
    -> (PVotingDatum s -> Term s b) -> Term s b)
-> PlutusType PVotingDatum
forall (s :: S). PVotingDatum s -> Term s (PInner PVotingDatum)
forall (s :: S) (b :: PType).
Term s (PInner PVotingDatum)
-> (PVotingDatum 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). PVotingDatum s -> Term s (PInner PVotingDatum)
pcon' :: forall (s :: S). PVotingDatum s -> Term s (PInner PVotingDatum)
$cpmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PVotingDatum)
-> (PVotingDatum s -> Term s b) -> Term s b
pmatch' :: forall (s :: S) (b :: PType).
Term s (PInner PVotingDatum)
-> (PVotingDatum s -> Term s b) -> Term s b
PlutusType) via (DeriveAsDataRec PVotingDatum)

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

{- | Voting Effect Plutarch script
 -
This script is used to:
  - certify new DRep registration
  - verify the DRep vote on behalf of the DRep based on the Agora voting result

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

@since 1.0.0
-}
votingEffectScript :: ClosedTerm (PAsData PCurrencySymbol :--> PAsData PScriptContext :--> PUnit)
votingEffectScript :: ClosedTerm
  (PAsData PCurrencySymbol :--> (PAsData PScriptContext :--> PUnit))
votingEffectScript = (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

  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))
datums' Term s (PAsData PTxId)
_ Term
  s
  (PAsData
     (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote)))
votes' Term s (PAsData (PBuiltinList (PAsData PProposalProcedure)))
pprocs' Term s (PMaybeData PLovelace)
_ Term s (PMaybeData PLovelace)
trDonations <- Term s PTxInfo -> (PTxInfo 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 PTxInfo
txInfo

  let txCerts :: Term s (PBuiltinList (PAsData PTxCert))
txCerts = 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'
  let votes :: Term
  s
  (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
votes = Term
  s
  (PAsData
     (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote)))
-> Term
     s
     (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term
  s
  (PAsData
     (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote)))
votes'
  let pprocs :: Term s (PBuiltinList (PAsData PProposalProcedure))
pprocs = Term s (PAsData (PBuiltinList (PAsData PProposalProcedure)))
-> Term s (PBuiltinList (PAsData PProposalProcedure))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (PBuiltinList (PAsData PProposalProcedure)))
pprocs'
  let datums :: Term s (PMap 'Unsorted PDatumHash PDatum)
datums = Term s (PAsData (PMap 'Unsorted PDatumHash PDatum))
-> Term s (PMap 'Unsorted PDatumHash PDatum)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData (PMap 'Unsorted PDatumHash PDatum))
datums'

  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)
_datum -> P.do
            let mint :: Term s (PValue 'Sorted 'NonZero)
mint = 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'

            let authSymbol :: Term s PCurrencySymbol
authSymbol = Term s (PAsData PCurrencySymbol) -> Term s PCurrencySymbol
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PCurrencySymbol)
authSymbol'
            -- Spending Condition 1: Transaction burns one GAT
            -- Spending Condition 2: Spent UTxO contains GAT

            -- Spending condition 6: Transaction does not include script inputs other than own input.
            -- If there is only one script input and we are running that means that we are that input
            -- so no need to check explicitly
            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))
 -> (PMaybe (PAsData PScriptHash) s -> Term s PBool)
 -> Term s PBool)
-> Term s (PMaybe (PAsData PScriptHash))
-> (PMaybe (PAsData PScriptHash) s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$
                (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

            PMap Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
voteList <- Term
  s
  (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
-> (PMap
      'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote) 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 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
votes
            PCons Term
  s
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
votePair Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
voteList' <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PVoter)
         (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
      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 PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
voteList
            PBuiltinList
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
  s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PVoter)
         (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
      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 PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
voteList'

            PDRepVoter Term s PDRepCredential
voter <- Term s PVoter -> (PVoter 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 PVoter -> (PVoter s -> Term s PBool) -> Term s PBool)
-> (Term s (PAsData PVoter) -> Term s PVoter)
-> Term s (PAsData PVoter)
-> (PVoter s -> Term s PBool)
-> Term s PBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s (PAsData PVoter) -> Term s PVoter
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PVoter)
 -> (PVoter s -> Term s PBool) -> Term s PBool)
-> Term s (PAsData PVoter)
-> (PVoter s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote))
   :--> PAsData PVoter)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote))
   :--> PAsData PVoter)
-> Term
     s
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
-> Term s (PAsData PVoter)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
votePair
            PDRepCredential Term s PCredential
cred <- Term s PDRepCredential
-> (PDRepCredential 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 PDRepCredential
voter
            PScriptCredential Term s (PAsData PScriptHash)
scriptHash <- 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

            Term s PCurrencySymbol
-> Term s (PBuiltinList (PAsData PTxInInfo))
-> Term s (PValue 'Sorted 'NonZero)
-> Term s PBool
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
authSymbol (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 (PValue 'Sorted 'NonZero)
mint
              #&& (scriptHash #== ownScriptHash)
          PCertifyingScript Term s (PAsData PInteger)
_ Term s PTxCert
txCert -> P.do
            let votes :: Term
  s
  (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
votes = Term
  s
  (PAsData
     (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote)))
-> Term
     s
     (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term
  s
  (PAsData
     (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote)))
votes'

            -- Transaction must not contain any votes.
            PMap Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
votesList <- Term
  s
  (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
-> (PMap
      'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote) 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 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
votes
            PBuiltinList
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
  s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PVoter)
         (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
      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 PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
votesList

            -- Transaction must not contain any proposal procedures.
            PBuiltinList (PAsData PProposalProcedure) s
PNil <- Term s (PBuiltinList (PAsData PProposalProcedure))
-> (PBuiltinList (PAsData PProposalProcedure) 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 (PAsData PProposalProcedure))
pprocs

            -- Transaction must not contain any treasury donations.
            PMaybeData PLovelace s
PDNothing <- Term s (PMaybeData PLovelace)
-> (PMaybeData PLovelace 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 PLovelace)
trDonations

            -- Transaction must contain exactly 1 transaction certificate.
            PCons Term s (PAsData PTxCert)
_txCert Term s (PBuiltinList (PAsData PTxCert))
txCerts' <- 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 (PBuiltinList (PAsData PTxCert))
txCerts
            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 (PBuiltinList (PAsData PTxCert))
txCerts'

            -- Transaction certificate must be a DRep registration
            PTxCertRegDRep Term s PDRepCredential
_ Term s (PAsData PLovelace)
_ <- Term s PTxCert -> (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 PTxCert
txCert

            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
          PVotingScript Term s PVoter
_voter -> P.do
            -- Transaction must not contain any proposal procedures.
            PBuiltinList (PAsData PProposalProcedure) s
PNil <- Term s (PBuiltinList (PAsData PProposalProcedure))
-> (PBuiltinList (PAsData PProposalProcedure) 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 (PAsData PProposalProcedure))
pprocs

            -- Transaction must not contain any treasury donations.
            PMaybeData PLovelace s
PDNothing <- Term s (PMaybeData PLovelace)
-> (PMaybeData PLovelace 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 PLovelace)
trDonations

            -- The spending script ensures that there is only one script input
            -- The spending input will contain a datum, and we don't allow any
            -- more datums in the transaction
            PJust Term s (PAsData PDatumHash)
datumHash <-
              Term s (PMaybe (PAsData PDatumHash))
-> (PMaybe (PAsData PDatumHash) 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 PDatumHash))
 -> (PMaybe (PAsData PDatumHash) s -> Term s PBool) -> Term s PBool)
-> Term s (PMaybe (PAsData PDatumHash))
-> (PMaybe (PAsData PDatumHash) s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$
                (Term
   s
   (PBuiltinList (PAsData PTxInInfo) :--> PMaybe (PAsData PDatumHash))
 -> Term s (PAsData PTxInInfo)
 -> Term s (PBuiltinList (PAsData PTxInInfo))
 -> Term s (PMaybe (PAsData PDatumHash)))
-> (Term
      s
      (PBuiltinList (PAsData PTxInInfo) :--> PMaybe (PAsData PDatumHash))
    -> Term s (PMaybe (PAsData PDatumHash)))
-> Term
     s
     (PBuiltinList (PAsData PTxInInfo) :--> PMaybe (PAsData PDatumHash))
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 PDatumHash))
self Term s (PAsData PTxInInfo)
input Term s (PBuiltinList (PAsData PTxInInfo))
rest -> Term s PTxInInfo
-> (PTxInInfo s -> Term s (PMaybe (PAsData PDatumHash)))
-> Term s (PMaybe (PAsData PDatumHash))
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 PDatumHash)))
 -> Term s (PMaybe (PAsData PDatumHash)))
-> (PTxInInfo s -> Term s (PMaybe (PAsData PDatumHash)))
-> Term s (PMaybe (PAsData PDatumHash))
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
datum Term s (PMaybeData PScriptHash)
_ <- Term s PTxOut
-> (PTxOut s -> Term s (PMaybe (PAsData PDatumHash)))
-> Term s (PMaybe (PAsData PDatumHash))
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 PDatumHash)))
-> Term s (PMaybe (PAsData PDatumHash))
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 PDatumHash)))
-> Term s (PMaybe (PAsData PDatumHash))
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 PDatumHash)))
 -> Term s (PMaybe (PAsData PDatumHash)))
-> (PCredential s -> Term s (PMaybe (PAsData PDatumHash)))
-> Term s (PMaybe (PAsData PDatumHash))
forall a b. (a -> b) -> a -> b
$ \case
                          PScriptCredential Term s (PAsData PScriptHash)
_ -> P.do
                            POutputDatumHash Term s (PAsData PDatumHash)
datumHash <- Term s POutputDatum
-> (POutputDatum s -> Term s (PMaybe (PAsData PDatumHash)))
-> Term s (PMaybe (PAsData PDatumHash))
forall (a :: PType) (s :: S) (b :: PType).
PlutusType a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s POutputDatum
datum
                            Term s (PMaybe (PAsData PDatumHash))
-> (PMaybe (PAsData PDatumHash) s
    -> Term s (PMaybe (PAsData PDatumHash)))
-> Term s (PMaybe (PAsData PDatumHash))
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 PDatumHash))
self Term
  s
  (PBuiltinList (PAsData PTxInInfo) :--> PMaybe (PAsData PDatumHash))
-> Term s (PBuiltinList (PAsData PTxInInfo))
-> Term s (PMaybe (PAsData PDatumHash))
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 PDatumHash) s
  -> Term s (PMaybe (PAsData PDatumHash)))
 -> Term s (PMaybe (PAsData PDatumHash)))
-> (PMaybe (PAsData PDatumHash) s
    -> Term s (PMaybe (PAsData PDatumHash)))
-> Term s (PMaybe (PAsData PDatumHash))
forall a b. (a -> b) -> a -> b
$ \case
                              PMaybe (PAsData PDatumHash) s
PNothing -> Term s (PAsData PDatumHash :--> PMaybe (PAsData PDatumHash))
forall (a :: PType) (s :: S). Term s (a :--> PMaybe a)
pjust Term s (PAsData PDatumHash :--> PMaybe (PAsData PDatumHash))
-> Term s (PAsData PDatumHash)
-> Term s (PMaybe (PAsData PDatumHash))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PDatumHash)
datumHash
                              PJust Term s (PAsData PDatumHash)
_ -> Term s (PMaybe (PAsData PDatumHash))
forall (s :: S) (a :: PType). Term s a
perror
                          PCredential s
_ -> Term
  s
  (PBuiltinList (PAsData PTxInInfo) :--> PMaybe (PAsData PDatumHash))
self Term
  s
  (PBuiltinList (PAsData PTxInInfo) :--> PMaybe (PAsData PDatumHash))
-> Term s (PBuiltinList (PAsData PTxInInfo))
-> Term s (PMaybe (PAsData PDatumHash))
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 PDatumHash))
-> Term
     s
     (PBuiltinList (PAsData PTxInInfo) :--> PMaybe (PAsData PDatumHash))
-> Term s (PMaybe (PAsData PDatumHash))
forall a b. a -> b -> a
const (forall (a :: PType) (s :: S).
PLiftable a =>
AsHaskell a -> Term s a
pconstant @(PMaybe (PAsData PDatumHash)) Maybe DatumHash
AsHaskell (PMaybe (PAsData PDatumHash))
forall a. Maybe a
Nothing))
                  # pfromData inputs

            -- There must be exactly 1 vote. As we're in a Voting context, this is guaranteed
            -- to be the vote with the current script as DRep voter
            PMap Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
voteList <- Term
  s
  (PMap 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
-> (PMap
      'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote) 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 'Unsorted PVoter (PMap 'Unsorted PGovernanceActionId PVote))
votes
            PCons Term
  s
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
votePair Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
voteList' <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PVoter)
         (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
      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 PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
voteList
            PBuiltinList
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
  s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
-> (PBuiltinList
      (PBuiltinPair
         (PAsData PVoter)
         (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
      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 PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote))))
voteList'
            let ownVotes :: Term s (PMap 'Unsorted PGovernanceActionId PVote)
ownVotes = Term s (PAsData (PMap 'Unsorted PGovernanceActionId PVote))
-> Term s (PMap 'Unsorted PGovernanceActionId PVote)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData (PMap 'Unsorted PGovernanceActionId PVote))
 -> Term s (PMap 'Unsorted PGovernanceActionId PVote))
-> Term s (PAsData (PMap 'Unsorted PGovernanceActionId PVote))
-> Term s (PMap 'Unsorted PGovernanceActionId PVote)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote))
   :--> PAsData (PMap 'Unsorted PGovernanceActionId PVote))
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote))
   :--> PAsData (PMap 'Unsorted PGovernanceActionId PVote))
-> Term
     s
     (PBuiltinPair
        (PAsData PVoter)
        (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
-> Term s (PAsData (PMap 'Unsorted PGovernanceActionId PVote))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PBuiltinPair
     (PAsData PVoter)
     (PAsData (PMap 'Unsorted PGovernanceActionId PVote)))
votePair

            PMap Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)))
ownVoteList <- Term s (PMap 'Unsorted PGovernanceActionId PVote)
-> (PMap 'Unsorted PGovernanceActionId PVote 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 'Unsorted PGovernanceActionId PVote)
ownVotes
            PCons Term s (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote))
ownVote Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)))
ownVoteList' <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)) 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 PGovernanceActionId) (PAsData PVote)))
ownVoteList
            PBuiltinList
  (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)) s
PNil <- Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)) 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 PGovernanceActionId) (PAsData PVote)))
ownVoteList'

            let govActionId :: Term s (PAsData PGovernanceActionId)
govActionId = Term
  s
  (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)
   :--> PAsData PGovernanceActionId)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)
   :--> PAsData PGovernanceActionId)
-> Term
     s (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote))
-> Term s (PAsData PGovernanceActionId)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote))
ownVote
            let vote :: Term s (PAsData PVote)
vote = Term
  s
  (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)
   :--> PAsData PVote)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote)
   :--> PAsData PVote)
-> Term
     s (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote))
-> Term s (PAsData PVote)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData PGovernanceActionId) (PAsData PVote))
ownVote

            PMap Term
  s
  (PBuiltinList (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)))
datumList <- Term s (PMap 'Unsorted PDatumHash PDatum)
-> (PMap 'Unsorted PDatumHash 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 (PMap 'Unsorted PDatumHash PDatum)
datums
            PCons Term s (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum))
datum Term
  s
  (PBuiltinList (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)))
datumList' <- Term
  s
  (PBuiltinList (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PDatumHash) (PAsData 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
  (PBuiltinList (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)))
datumList
            PBuiltinList (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)) s
PNil <- Term
  s
  (PBuiltinList (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)))
-> (PBuiltinList
      (PBuiltinPair (PAsData PDatumHash) (PAsData 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
  (PBuiltinList (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)))
datumList'

            let datumHash' :: Term s (PAsData PDatumHash)
datumHash' = Term
  s
  (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)
   :--> PAsData PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> a)
pfstBuiltin Term
  s
  (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)
   :--> PAsData PDatumHash)
-> Term s (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum))
-> Term s (PAsData PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum))
datum
            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 PDatum -> (PDatum s -> Term s PBool) -> Term s PBool)
-> (Term s (PAsData PDatum) -> Term s PDatum)
-> Term s (PAsData PDatum)
-> (PDatum s -> Term s PBool)
-> Term s PBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
 -> (PDatum s -> Term s PBool) -> Term s PBool)
-> Term s (PAsData PDatum)
-> (PDatum s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)
   :--> PAsData PDatum)
forall (s :: S) (a :: PType) (b :: PType).
Term s (PBuiltinPair a b :--> b)
psndBuiltin Term
  s
  (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum)
   :--> PAsData PDatum)
-> Term s (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum))
-> Term s (PAsData PDatum)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinPair (PAsData PDatumHash) (PAsData PDatum))
datum

            let rawVotingDatum :: Term s (PAsData PVotingDatum)
rawVotingDatum = TermCont @(PAsData PVotingDatum) s (Term s (PAsData PVotingDatum))
-> Term s (PAsData PVotingDatum)
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @(PAsData PVotingDatum) s (Term s (PAsData PVotingDatum))
 -> Term s (PAsData PVotingDatum))
-> TermCont
     @(PAsData PVotingDatum) s (Term s (PAsData PVotingDatum))
-> Term s (PAsData PVotingDatum)
forall a b. (a -> b) -> a -> b
$ (Term s (PAsData PVotingDatum), ())
-> Term s (PAsData PVotingDatum)
forall a b. (a, b) -> a
fst ((Term s (PAsData PVotingDatum), ())
 -> Term s (PAsData PVotingDatum))
-> TermCont
     @(PAsData PVotingDatum) s (Term s (PAsData PVotingDatum), ())
-> TermCont
     @(PAsData PVotingDatum) s (Term s (PAsData PVotingDatum))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Term s (PAsData PVotingDatum), ())
  -> Term s (PAsData PVotingDatum))
 -> Term s (PAsData PVotingDatum))
-> TermCont
     @(PAsData PVotingDatum) s (Term s (PAsData PVotingDatum), ())
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 PVotingDatum) Term s PData
rawDatum)
            PVotingDatum Term s (PAsData PGovernanceActionId)
govActionId' Term s (PAsData PVote)
vote' <- Term s PVotingDatum
-> (PVotingDatum 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 PVotingDatum
 -> (PVotingDatum s -> Term s PBool) -> Term s PBool)
-> Term s PVotingDatum
-> (PVotingDatum s -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PVotingDatum) -> Term s PVotingDatum
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PVotingDatum)
rawVotingDatum

            -- Transaction must not contain transaction certificate.
            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 (PBuiltinList (PAsData PTxCert))
txCerts

            -- Governance Action Id and Vote must match the values in the datum
            (Term s (PAsData PDatumHash)
datumHash Term s (PAsData PDatumHash)
-> Term s (PAsData PDatumHash) -> Term s PBool
forall (s :: S).
Term s (PAsData PDatumHash)
-> Term s (PAsData PDatumHash) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData PDatumHash)
datumHash')
              #&& (govActionId #== govActionId')
              #&& (vote #== vote')
          PScriptInfo 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

  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