{- |
Module     : Agora.Governor.Scripts
Maintainer : connor@mlabs.city
Description: Plutus scripts for Governors.

Plutus scripts for Governors.
-}
module Agora.Governor.Scripts (
  -- * GST
  -- $gst

  -- * Scripts
  governorPolicy,
  governorValidator,

  -- * Bridges
  governorSTSymbolFromGovernor,
  governorSTAssetClassFromGovernor,
  proposalSTAssetClassFromGovernor,
  stakeSTSymbolFromGovernor,
  stakeFromGovernor,
  stakeValidatorHashFromGovernor,
  proposalFromGovernor,
  proposalValidatorHashFromGovernor,
  proposalSTSymbolFromGovernor,
  stakeSTAssetClassFromGovernor,
  governorValidatorHash,
  authorityTokenFromGovernor,
  authorityTokenSymbolFromGovernor,
) where

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

import Agora.AuthorityToken (
  AuthorityToken (..),
  authorityTokenPolicy,
  authorityTokensValidIn,
  singleAuthorityTokenBurned,
 )
import Agora.Governor (
  Governor (gstOutRef, gtClassRef, maximumCosigners),
  PGovernorDatum (PGovernorDatum),
  PGovernorRedeemer (PCreateProposal, PMintGATs, PMutateGovernor),
  governorDatumValid,
  pgetNextProposalId,
 )
import Agora.Proposal (
  PProposalDatum (..),
  PProposalId (..),
  PProposalStatus (PFinished),
  PResultTag,
  Proposal (..),
  ProposalStatus (Draft, Locked),
  pemptyVotesFor,
  pneutralOption,
  proposalDatumValid,
  pwinner,
 )
import Agora.Proposal.Scripts (
  proposalPolicy,
  proposalValidator,
 )
import Agora.Proposal.Time (createProposalStartingTime)
import Agora.SafeMoney (GTTag)
import Agora.Stake (
  PProposalLock (..),
  PStakeDatum (..),
  Stake (..),
 )
import Agora.Stake.Scripts (
  stakePolicy,
  stakeValidator,
 )
import Agora.Utils (
  findOutputsToAddress,
  hasOnlyOneTokenOfCurrencySymbol,
  mustBePDJust,
  mustBePJust,
  mustFindDatum',
  scriptHashFromAddress,
  validatorHashToAddress,
  validatorHashToTokenName,
 )
import Plutarch.Extra.Record

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

import Plutarch.Api.V1 (
  PAddress,
  PCurrencySymbol,
  PDatumHash,
  PMap,
  PMintingPolicy,
  PScriptPurpose (PMinting, PSpending),
  PTxOut,
  PValidator,
  PValidatorHash,
  PValue,
  mintingPolicySymbol,
  mkMintingPolicy,
  mkValidator,
  validatorHash,
 )
import Plutarch.Api.V1.AssetClass (
  passetClass,
  passetClassValueOf,
 )
import Plutarch.Extra.Map (
  pkeys,
  plookup,
  plookup',
 )
import Plutarch.SafeMoney (PDiscrete (..), pvalueDiscrete')
import Plutarch.TryFrom ()

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

import Plutarch.Api.V1.ScriptContext (pfindTxInByTxOutRef, pisUTXOSpent, ptryFindDatum, ptxSignedBy, pvalueSpent)
import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (psymbolValueOf)
import Plutarch.Extra.Maybe (pisDJust)
import Plutarch.Extra.TermCont
import PlutusLedgerApi.V1 (
  CurrencySymbol (..),
  MintingPolicy,
 )
import PlutusLedgerApi.V1.Scripts (ValidatorHash (..))
import PlutusLedgerApi.V1.Value (
  AssetClass (..),
 )

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

{- $gst
   Governance state token, aka. GST, is an NFT that identifies a UTXO that
    carries the state datum of the Governance script.

   This token is minted by a one-shot monetary policy 'governorPolicy',
    meaning that the token has guaranteed uniqueness.

   The 'governorValidator' ensures that exactly one GST stays
    at the address of itself forever.
-}

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

{- | Policy for minting GSTs.

   This policy perform the following checks:

    - The UTXO referenced in the parameter is spent in the transaction.
    - Exactly one GST is minted.
    - Ensure the token name is empty.
    - Said UTXO should carry a valid 'Agora.Governor.GovernorDatum'.

  NOTE: It's user's responsibility to make sure the token is sent to the corresponding governor validator.
        We /can't/ really check this in the policy, otherwise we create a cyclic reference issue.

  @since 0.1.0
-}
governorPolicy :: Governor -> ClosedTerm PMintingPolicy
governorPolicy :: Governor -> ClosedTerm PMintingPolicy
governorPolicy Governor
gov =
  (Term s PData -> Term s PScriptContext -> Term s POpaque)
-> Term s PMintingPolicy
forall a (b :: PType) (s :: S) (c :: PType).
PLamN a b s =>
(Term s c -> a) -> Term s (c :--> b)
plam ((Term s PData -> Term s PScriptContext -> Term s POpaque)
 -> Term s PMintingPolicy)
-> (Term s PData -> Term s PScriptContext -> Term s POpaque)
-> Term s PMintingPolicy
forall a b. (a -> b) -> a -> b
$ \Term s PData
_ Term s PScriptContext
ctx' -> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @POpaque s (Term s POpaque) -> Term s POpaque)
-> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ do
    let oref :: Term s PTxOutRef
oref = PLifted PTxOutRef -> Term s PTxOutRef
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant Governor
gov.gstOutRef

    PMinting ((forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" #) -> Term s PCurrencySymbol
ownSymbol) <- Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC (Term s (PAsData PScriptPurpose) -> Term s PScriptPurpose
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PScriptPurpose) -> Term s PScriptPurpose)
-> Term s (PAsData PScriptPurpose) -> Term s PScriptPurpose
forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"purpose" Term s (PScriptContext :--> PAsData PScriptPurpose)
-> Term s PScriptContext -> Term s (PAsData PScriptPurpose)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PScriptContext
ctx')
    let ownAssetClass :: Term s PAssetClass
ownAssetClass = Term s (PCurrencySymbol :--> (PTokenName :--> PAssetClass))
forall (s :: S).
Term s (PCurrencySymbol :--> (PTokenName :--> PAssetClass))
passetClass Term s (PCurrencySymbol :--> (PTokenName :--> PAssetClass))
-> Term s PCurrencySymbol -> Term s (PTokenName :--> PAssetClass)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
ownSymbol Term s (PTokenName :--> PAssetClass)
-> Term s PTokenName -> Term s PAssetClass
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# PLifted PTokenName -> Term s PTokenName
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PTokenName
TokenName
""
        txInfo :: Term s PTxInfo
txInfo = Term s (PAsData PTxInfo) -> Term s PTxInfo
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PTxInfo) -> Term s PTxInfo)
-> Term s (PAsData PTxInfo) -> Term s PTxInfo
forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"txInfo" Term s (PScriptContext :--> PAsData PTxInfo)
-> Term s PScriptContext -> Term s (PAsData PTxInfo)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PScriptContext
ctx'

    HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol "datums" ((':) @Symbol "validRange" ('[] @Symbol)))))))
     s)
txInfoF <- ((HRec
    (BoundTerms
       (PFields PTxInfo)
       (Bindings
          (PFields PTxInfo)
          ((':)
             @Symbol
             "mint"
             ((':)
                @Symbol
                "inputs"
                ((':)
                   @Symbol
                   "outputs"
                   ((':)
                      @Symbol "datums" ((':) @Symbol "validRange" ('[] @Symbol)))))))
       s)
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields PTxInfo)
           (Bindings
              (PFields PTxInfo)
              ((':)
                 @Symbol
                 "mint"
                 ((':)
                    @Symbol
                    "inputs"
                    ((':)
                       @Symbol
                       "outputs"
                       ((':)
                          @Symbol "datums" ((':) @Symbol "validRange" ('[] @Symbol)))))))
           s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     (BoundTerms
        (PFields PTxInfo)
        (Bindings
           (PFields PTxInfo)
           ((':)
              @Symbol
              "mint"
              ((':)
                 @Symbol
                 "inputs"
                 ((':)
                    @Symbol
                    "outputs"
                    ((':)
                       @Symbol "datums" ((':) @Symbol "validRange" ('[] @Symbol)))))))
        s)
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         (BoundTerms
            (PFields PTxInfo)
            (Bindings
               (PFields PTxInfo)
               ((':)
                  @Symbol
                  "mint"
                  ((':)
                     @Symbol
                     "inputs"
                     ((':)
                        @Symbol
                        "outputs"
                        ((':)
                           @Symbol "datums" ((':) @Symbol "validRange" ('[] @Symbol)))))))
            s)))
-> ((HRec
       (BoundTerms
          (PFields PTxInfo)
          (Bindings
             (PFields PTxInfo)
             ((':)
                @Symbol
                "mint"
                ((':)
                   @Symbol
                   "inputs"
                   ((':)
                      @Symbol
                      "outputs"
                      ((':)
                         @Symbol "datums" ((':) @Symbol "validRange" ('[] @Symbol)))))))
          s)
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields PTxInfo)
           (Bindings
              (PFields PTxInfo)
              ((':)
                 @Symbol
                 "mint"
                 ((':)
                    @Symbol
                    "inputs"
                    ((':)
                       @Symbol
                       "outputs"
                       ((':)
                          @Symbol "datums" ((':) @Symbol "validRange" ('[] @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 @'["mint", "inputs", "outputs", "datums", "validRange"] Term s PTxInfo
txInfo

    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)
"Referenced utxo should be spent" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
      Term
  s (PTxOutRef :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
forall (s :: S).
Term
  s (PTxOutRef :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
pisUTXOSpent Term
  s (PTxOutRef :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
-> Term s PTxOutRef
-> Term s (PBuiltinList (PAsData PTxInInfo) :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PTxOutRef
oref Term s (PBuiltinList (PAsData PTxInInfo) :--> PBool)
-> Term s (PBuiltinList (PAsData PTxInInfo)) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol "datums" ((':) @Symbol "validRange" ('[] @Symbol)))))))
     s)
txInfoF.inputs

    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)
"Exactly one token should be minted" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
      Term
  s
  (PCurrencySymbol
   :--> (PValue 'Sorted 'NoGuarantees :--> PInteger @S))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term
  s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger @S))
psymbolValueOf Term
  s
  (PCurrencySymbol
   :--> (PValue 'Sorted 'NoGuarantees :--> PInteger @S))
-> Term s PCurrencySymbol
-> Term s (PValue 'Sorted 'NoGuarantees :--> PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
ownSymbol Term s (PValue 'Sorted 'NoGuarantees :--> PInteger @S)
-> Term s (PValue 'Sorted 'NoGuarantees) -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol "datums" ((':) @Symbol "validRange" ('[] @Symbol)))))))
     s)
txInfoF.mint Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PInteger @S)
1
        #&& passetClassValueOf # txInfoF.mint # ownAssetClass #== 1

    Term s (PAsData PTxOut)
govOutput <-
      Term s (PAsData PTxOut)
-> TermCont @POpaque s (Term s (PAsData PTxOut))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PAsData PTxOut)
 -> TermCont @POpaque s (Term s (PAsData PTxOut)))
-> Term s (PAsData PTxOut)
-> TermCont @POpaque s (Term s (PAsData PTxOut))
forall a b. (a -> b) -> a -> b
$
        Term
  s (PString @S :--> (PMaybe (PAsData PTxOut) :--> PAsData PTxOut))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust
          # "Governor output not found"
            #$ pfind
          # plam
            ( \((pfield @"value" #) . pfromData -> value) ->
                psymbolValueOf # ownSymbol # value #== 1
            )
          # pfromData txInfoF.outputs

    let datumHash :: Term s (PMaybeData PDatumHash)
datumHash = 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 @"datumHash" Term s (PTxOut :--> PMaybeData PDatumHash)
-> Term s PTxOut -> Term s (PMaybeData PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PTxOut) -> Term s PTxOut
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData Term s (PAsData PTxOut)
govOutput
        datum :: Term s PGovernorDatum
datum = forall (datum :: PType) (s :: S).
(PIsData datum, PTryFrom PData (PAsData datum)) =>
Term
  s
  (PMaybeData PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> datum))
mustFindDatum' @PGovernorDatum Term
  s
  (PMaybeData PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> PGovernorDatum))
-> Term s (PMaybeData PDatumHash)
-> Term
     s
     (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
      :--> PGovernorDatum)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMaybeData PDatumHash)
datumHash Term
  s
  (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
   :--> PGovernorDatum)
-> Term s (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))
-> Term s PGovernorDatum
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol "datums" ((':) @Symbol "validRange" ('[] @Symbol)))))))
     s)
txInfoF.datums

    Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s POpaque -> TermCont @POpaque s (Term s POpaque))
-> Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (Term s PBool -> Term s POpaque) -> Term s PBool -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ Term s (PGovernorDatum :--> PBool)
forall (s :: S). Term s (PGovernorDatum :--> PBool)
governorDatumValid Term s (PGovernorDatum :--> PBool)
-> Term s PGovernorDatum -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PGovernorDatum
datum

{- | Validator for Governors.

     == Common checks

     The validator always ensures:

       - The UTXO which holds the GST must be spent.
       - The GST always stays at the validator's address.
       - The new state UTXO has a valid datum of type 'Agora.Governor.GovernorDatum'.

     == Creating a Proposal

     When the redeemer is 'Agora.Governor.CreateProposal', the script will check:

     - For governor's state datum:

         * 'Agora.Governor.nextProposalId' is advanced.
         * Nothing is changed other that that.

     - Exactly one stake (the "input stake") must be provided in the input:
         * At least 'Agora.Stake.stackedAmount' of GT must be spent in the transaction.
         * The transaction must be signed by the stake owner.

     - Exactly one new proposal state token is minted.
     - An UTXO which holds the newly minted proposal state token is sent to the proposal validator.
       This UTXO must have a valid datum of type 'Agora.Proposal.ProposalDatum', the datum must:

         * Copy its id and thresholds from the governor's state.
         * Have status set to 'Proposal.Draft'.
         * Have zero votes.
         * Have exactly one cosigner - the stake owner

     - An UTXO which holds the stake state token is sent back to the stake validator.
       This UTXO must have a valid datum of type 'Agora.Stake.StakeDatum':

         * The 'Agora.Stake.stakedAmount' and 'Agora.Stake.owner' should not be changed,
            comparing to the input stake.
         * The new proposal locks must be appended to the 'Agora.Stake.lockedBy'.

     == Minting GATs

     When the redeemer is 'Agora.Governor.MintGATs', the script will check:

     - Governor's state is not changed.
     - Exactly only one proposal is in the inputs. Let's call this the /input proposal/.
     - The proposal is in the 'Proposal.Executable' state.

     NOTE: The input proposal is found by looking for the UTXO with a proposal state token in the inputs.

     === Effect Group Selection

     Currently a proposal can have two or more than two options to vote on,
       meaning that it can contains two or more effect groups,
       according to [#39](https://github.com/Liqwid-Labs/agora/issues/39).

     Either way, the shapes of 'Proposal.votes' and 'Proposal.effects' should be the same.
       This is checked by 'Proposal.proposalDatumValid'.

     The script will look at the the 'Proposal.votes' to determine which group has the highest votes,
       said group shoud be executed.

     During the process, minimum votes requirement will also be enforced.

     Next, the script will:

     - Ensure that for every effect in the said effect group,
       exactly one valid GAT is minted and sent to the effect.
     - The amount of GAT minted in the transaction should be equal to the number of effects.
     - A new UTXO is sent to the proposal validator, this UTXO should:

         * Include the one proposal state token.
         * Have a valid datum of type 'Proposal.ProposalDatum'.
           This datum should be as same as the one of the input proposal,
           except its status should be 'Proposal.Finished'.

     == Changing the State

     Redeemer 'Agora.Governor.MutateGovernor' allows the state datum to be changed by an external effect.

     In this case, the script will check

     - Exactly one GAT is burnt in the transaction.
     - Said GAT is tagged by the effect.

     @since 0.1.0
-}
governorValidator :: Governor -> ClosedTerm PValidator
governorValidator :: Governor -> ClosedTerm PValidator
governorValidator Governor
gov =
  (Term s PData
 -> Term s PData -> Term s PScriptContext -> Term s POpaque)
-> Term s PValidator
forall a (b :: PType) (s :: S) (c :: PType).
PLamN a b s =>
(Term s c -> a) -> Term s (c :--> b)
plam ((Term s PData
  -> Term s PData -> Term s PScriptContext -> Term s POpaque)
 -> Term s PValidator)
-> (Term s PData
    -> Term s PData -> Term s PScriptContext -> Term s POpaque)
-> Term s PValidator
forall a b. (a -> b) -> a -> b
$ \Term s PData
datum' Term s PData
redeemer' Term s PScriptContext
ctx' -> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @POpaque s (Term s POpaque) -> Term s POpaque)
-> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ do
    (Term s (PAsData PGovernorRedeemer) -> Term s PGovernorRedeemer
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData -> Term s PGovernorRedeemer
redeemer, Reduce @Type (PTryFromExcess PData (PAsData PGovernorRedeemer) s)
_) <- (((Term s (PAsData PGovernorRedeemer),
   Reduce @Type (PTryFromExcess PData (PAsData PGovernorRedeemer) s))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (Term s (PAsData PGovernorRedeemer),
      Reduce @Type (PTryFromExcess PData (PAsData PGovernorRedeemer) s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PAsData PGovernorRedeemer),
    Reduce @Type (PTryFromExcess PData (PAsData PGovernorRedeemer) s))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (Term s (PAsData PGovernorRedeemer),
       Reduce @Type (PTryFromExcess PData (PAsData PGovernorRedeemer) s)))
-> (((Term s (PAsData PGovernorRedeemer),
      Reduce @Type (PTryFromExcess PData (PAsData PGovernorRedeemer) s))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (Term s (PAsData PGovernorRedeemer),
      Reduce @Type (PTryFromExcess PData (PAsData PGovernorRedeemer) s))
forall a b. (a -> b) -> a -> b
$ Term s PData
-> ((Term s (PAsData PGovernorRedeemer),
     Reduce @Type (PTryFromExcess PData (PAsData PGovernorRedeemer) s))
    -> Term s POpaque)
-> Term s POpaque
forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce @Type (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom Term s PData
redeemer'
    HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctxF <- ((HRec
    (BoundTerms
       (PFields PScriptContext)
       (Bindings
          (PFields PScriptContext)
          ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
       s)
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields PScriptContext)
           (Bindings
              (PFields PScriptContext)
              ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
           s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     (BoundTerms
        (PFields PScriptContext)
        (Bindings
           (PFields PScriptContext)
           ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
        s)
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         (BoundTerms
            (PFields PScriptContext)
            (Bindings
               (PFields PScriptContext)
               ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
            s)))
-> ((HRec
       (BoundTerms
          (PFields PScriptContext)
          (Bindings
             (PFields PScriptContext)
             ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
          s)
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields PScriptContext)
           (Bindings
              (PFields PScriptContext)
              ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @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 @'["txInfo", "purpose"] Term s PScriptContext
ctx'

    Term s PTxInfo
txInfo' <- Term s PTxInfo -> TermCont @POpaque s (Term s PTxInfo)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PTxInfo -> TermCont @POpaque s (Term s PTxInfo))
-> Term s PTxInfo -> TermCont @POpaque s (Term s PTxInfo)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PTxInfo) -> Term s PTxInfo
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PTxInfo) -> Term s PTxInfo)
-> Term s (PAsData PTxInfo) -> Term s PTxInfo
forall a b. (a -> b) -> a -> b
$ HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctxF.txInfo
    HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol
                    "datums"
                    ((':)
                       @Symbol
                       "signatories"
                       ((':) @Symbol "validRange" ('[] @Symbol))))))))
     s)
txInfoF <- ((HRec
    (BoundTerms
       (PFields PTxInfo)
       (Bindings
          (PFields PTxInfo)
          ((':)
             @Symbol
             "mint"
             ((':)
                @Symbol
                "inputs"
                ((':)
                   @Symbol
                   "outputs"
                   ((':)
                      @Symbol
                      "datums"
                      ((':)
                         @Symbol
                         "signatories"
                         ((':) @Symbol "validRange" ('[] @Symbol))))))))
       s)
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields PTxInfo)
           (Bindings
              (PFields PTxInfo)
              ((':)
                 @Symbol
                 "mint"
                 ((':)
                    @Symbol
                    "inputs"
                    ((':)
                       @Symbol
                       "outputs"
                       ((':)
                          @Symbol
                          "datums"
                          ((':)
                             @Symbol
                             "signatories"
                             ((':) @Symbol "validRange" ('[] @Symbol))))))))
           s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     (BoundTerms
        (PFields PTxInfo)
        (Bindings
           (PFields PTxInfo)
           ((':)
              @Symbol
              "mint"
              ((':)
                 @Symbol
                 "inputs"
                 ((':)
                    @Symbol
                    "outputs"
                    ((':)
                       @Symbol
                       "datums"
                       ((':)
                          @Symbol
                          "signatories"
                          ((':) @Symbol "validRange" ('[] @Symbol))))))))
        s)
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         (BoundTerms
            (PFields PTxInfo)
            (Bindings
               (PFields PTxInfo)
               ((':)
                  @Symbol
                  "mint"
                  ((':)
                     @Symbol
                     "inputs"
                     ((':)
                        @Symbol
                        "outputs"
                        ((':)
                           @Symbol
                           "datums"
                           ((':)
                              @Symbol
                              "signatories"
                              ((':) @Symbol "validRange" ('[] @Symbol))))))))
            s)))
-> ((HRec
       (BoundTerms
          (PFields PTxInfo)
          (Bindings
             (PFields PTxInfo)
             ((':)
                @Symbol
                "mint"
                ((':)
                   @Symbol
                   "inputs"
                   ((':)
                      @Symbol
                      "outputs"
                      ((':)
                         @Symbol
                         "datums"
                         ((':)
                            @Symbol
                            "signatories"
                            ((':) @Symbol "validRange" ('[] @Symbol))))))))
          s)
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields PTxInfo)
           (Bindings
              (PFields PTxInfo)
              ((':)
                 @Symbol
                 "mint"
                 ((':)
                    @Symbol
                    "inputs"
                    ((':)
                       @Symbol
                       "outputs"
                       ((':)
                          @Symbol
                          "datums"
                          ((':)
                             @Symbol
                             "signatories"
                             ((':) @Symbol "validRange" ('[] @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 @'["mint", "inputs", "outputs", "datums", "signatories", "validRange"] Term s PTxInfo
txInfo'

    PSpending (Term s (PAsData PTxOutRef) -> Term s PTxOutRef
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PTxOutRef) -> Term s PTxOutRef)
-> (Term
      s
      (PDataRecord
         ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType)))
    -> Term s (PAsData PTxOutRef))
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType)))
-> Term s PTxOutRef
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"_0" #) -> Term s PTxOutRef
ownInputRef) <- Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC (Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s))
-> Term s PScriptPurpose -> TermCont @POpaque s (PScriptPurpose s)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PScriptPurpose) -> Term s PScriptPurpose
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctxF.purpose

    ((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)
ownInput) <-
      Term s PTxInInfo -> TermCont @POpaque s (Term s PTxInInfo)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PTxInInfo -> TermCont @POpaque s (Term s PTxInInfo))
-> Term s PTxInInfo -> TermCont @POpaque s (Term s PTxInInfo)
forall a b. (a -> b) -> a -> b
$
        Term s (PString @S :--> (PMaybe PTxInInfo :--> PTxInInfo))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust Term s (PString @S :--> (PMaybe PTxInInfo :--> PTxInInfo))
-> Term s (PString @S) -> Term s (PMaybe PTxInInfo :--> PTxInInfo)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"Own input not found"
          #$ pfindTxInByTxOutRef # ownInputRef # txInfoF.inputs
    HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
     s)
ownInputF <- ((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)
ownInput
    let ownAddress :: Term s PAddress
ownAddress = Term s (PAsData PAddress) -> Term s PAddress
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PAddress) -> Term s PAddress)
-> Term s (PAsData PAddress) -> Term s PAddress
forall a b. (a -> b) -> a -> b
$ HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
     s)
ownInputF.address

    (Term s (PAsData PGovernorDatum) -> Term s PGovernorDatum
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData -> (Term s PGovernorDatum
oldGovernorDatum :: Term _ PGovernorDatum), Reduce @Type (PTryFromExcess PData (PAsData PGovernorDatum) s)
_) <- (((Term s (PAsData PGovernorDatum),
   Reduce @Type (PTryFromExcess PData (PAsData PGovernorDatum) s))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (Term s (PAsData PGovernorDatum),
      Reduce @Type (PTryFromExcess PData (PAsData PGovernorDatum) s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont ((((Term s (PAsData PGovernorDatum),
    Reduce @Type (PTryFromExcess PData (PAsData PGovernorDatum) s))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (Term s (PAsData PGovernorDatum),
       Reduce @Type (PTryFromExcess PData (PAsData PGovernorDatum) s)))
-> (((Term s (PAsData PGovernorDatum),
      Reduce @Type (PTryFromExcess PData (PAsData PGovernorDatum) s))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (Term s (PAsData PGovernorDatum),
      Reduce @Type (PTryFromExcess PData (PAsData PGovernorDatum) s))
forall a b. (a -> b) -> a -> b
$ Term s PData
-> ((Term s (PAsData PGovernorDatum),
     Reduce @Type (PTryFromExcess PData (PAsData PGovernorDatum) s))
    -> Term s POpaque)
-> Term s POpaque
forall (b :: PType) (a :: PType) (s :: S) (r :: PType).
PTryFrom a b =>
Term s a
-> ((Term s b, Reduce @Type (PTryFromExcess a b s)) -> Term s r)
-> Term s r
ptryFrom Term s PData
datum'
    HRec
  ((':)
     @(Symbol, Type)
     '("proposalThresholds", Term s (PAsData PProposalThresholds))
     ((':)
        @(Symbol, Type)
        '("nextProposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("proposalTimings", Term s (PAsData PProposalTimingConfig))
           ((':)
              @(Symbol, Type)
              '("createProposalTimeRangeMaxWidth",
                Term s (PAsData PMaxTimeRangeWidth))
              ('[] @(Symbol, Type))))))
oldGovernorDatumF <-
      ((HRec
    ((':)
       @(Symbol, Type)
       '("proposalThresholds", Term s (PAsData PProposalThresholds))
       ((':)
          @(Symbol, Type)
          '("nextProposalId", Term s (PAsData PProposalId))
          ((':)
             @(Symbol, Type)
             '("proposalTimings", Term s (PAsData PProposalTimingConfig))
             ((':)
                @(Symbol, Type)
                '("createProposalTimeRangeMaxWidth",
                  Term s (PAsData PMaxTimeRangeWidth))
                ('[] @(Symbol, Type))))))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("proposalThresholds", Term s (PAsData PProposalThresholds))
           ((':)
              @(Symbol, Type)
              '("nextProposalId", Term s (PAsData PProposalId))
              ((':)
                 @(Symbol, Type)
                 '("proposalTimings", Term s (PAsData PProposalTimingConfig))
                 ((':)
                    @(Symbol, Type)
                    '("createProposalTimeRangeMaxWidth",
                      Term s (PAsData PMaxTimeRangeWidth))
                    ('[] @(Symbol, Type)))))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("proposalThresholds", Term s (PAsData PProposalThresholds))
        ((':)
           @(Symbol, Type)
           '("nextProposalId", Term s (PAsData PProposalId))
           ((':)
              @(Symbol, Type)
              '("proposalTimings", Term s (PAsData PProposalTimingConfig))
              ((':)
                 @(Symbol, Type)
                 '("createProposalTimeRangeMaxWidth",
                   Term s (PAsData PMaxTimeRangeWidth))
                 ('[] @(Symbol, Type))))))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("proposalThresholds", Term s (PAsData PProposalThresholds))
            ((':)
               @(Symbol, Type)
               '("nextProposalId", Term s (PAsData PProposalId))
               ((':)
                  @(Symbol, Type)
                  '("proposalTimings", Term s (PAsData PProposalTimingConfig))
                  ((':)
                     @(Symbol, Type)
                     '("createProposalTimeRangeMaxWidth",
                       Term s (PAsData PMaxTimeRangeWidth))
                     ('[] @(Symbol, Type))))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("proposalThresholds", Term s (PAsData PProposalThresholds))
          ((':)
             @(Symbol, Type)
             '("nextProposalId", Term s (PAsData PProposalId))
             ((':)
                @(Symbol, Type)
                '("proposalTimings", Term s (PAsData PProposalTimingConfig))
                ((':)
                   @(Symbol, Type)
                   '("createProposalTimeRangeMaxWidth",
                     Term s (PAsData PMaxTimeRangeWidth))
                   ('[] @(Symbol, Type))))))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("proposalThresholds", Term s (PAsData PProposalThresholds))
           ((':)
              @(Symbol, Type)
              '("nextProposalId", Term s (PAsData PProposalId))
              ((':)
                 @(Symbol, Type)
                 '("proposalTimings", Term s (PAsData PProposalTimingConfig))
                 ((':)
                    @(Symbol, Type)
                    '("createProposalTimeRangeMaxWidth",
                      Term s (PAsData PMaxTimeRangeWidth))
                    ('[] @(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
          @'[ "proposalThresholds"
            , "nextProposalId"
            , "proposalTimings"
            , "createProposalTimeRangeMaxWidth"
            ]
          Term s PGovernorDatum
oldGovernorDatum

    -- Check that GST will be returned to the governor.
    let ownInputGSTAmount :: Term s (PInteger @S)
ownInputGSTAmount = Term
  s
  (PCurrencySymbol :--> (PValue 'Sorted 'Positive :--> PInteger @S))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term
  s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger @S))
psymbolValueOf Term
  s
  (PCurrencySymbol :--> (PValue 'Sorted 'Positive :--> PInteger @S))
-> Term s PCurrencySymbol
-> Term s (PValue 'Sorted 'Positive :--> PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
forall (s :: S). Term s PCurrencySymbol
pgstSymbol Term s (PValue 'Sorted 'Positive :--> PInteger @S)
-> Term s (PValue 'Sorted 'Positive) -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "address" ((':) @Symbol "value" ('[] @Symbol))))
     s)
ownInputF.value
    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)
"Own input should have exactly one state token" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
      Term s (PInteger @S)
ownInputGSTAmount Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PInteger @S)
1

    Term s (PBuiltinList (PAsData PTxOut))
ownOutputs <- Term s (PBuiltinList (PAsData PTxOut))
-> TermCont @POpaque s (Term s (PBuiltinList (PAsData PTxOut)))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PBuiltinList (PAsData PTxOut))
 -> TermCont @POpaque s (Term s (PBuiltinList (PAsData PTxOut))))
-> Term s (PBuiltinList (PAsData PTxOut))
-> TermCont @POpaque s (Term s (PBuiltinList (PAsData PTxOut)))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinList (PAsData PTxOut)
   :--> (PAddress :--> PBuiltinList (PAsData PTxOut)))
forall (s :: S).
Term
  s
  (PBuiltinList (PAsData PTxOut)
   :--> (PAddress :--> PBuiltinList (PAsData PTxOut)))
findOutputsToAddress Term
  s
  (PBuiltinList (PAsData PTxOut)
   :--> (PAddress :--> PBuiltinList (PAsData PTxOut)))
-> Term s (PBuiltinList (PAsData PTxOut))
-> Term s (PAddress :--> PBuiltinList (PAsData PTxOut))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol
                    "datums"
                    ((':)
                       @Symbol
                       "signatories"
                       ((':) @Symbol "validRange" ('[] @Symbol))))))))
     s)
txInfoF.outputs Term s (PAddress :--> PBuiltinList (PAsData PTxOut))
-> Term s PAddress -> Term s (PBuiltinList (PAsData PTxOut))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PAddress
ownAddress
    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)
"Exactly one utxo should be sent to the governor" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
      Term s (PBuiltinList (PAsData PTxOut) :--> PInteger @S)
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> PInteger @S)
plength Term s (PBuiltinList (PAsData PTxOut) :--> PInteger @S)
-> Term s (PBuiltinList (PAsData PTxOut)) -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PAsData PTxOut))
ownOutputs Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PInteger @S)
1

    HRec
  ((':)
     @(Symbol, Type)
     '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
     ((':)
        @(Symbol, Type)
        '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
        ('[] @(Symbol, Type))))
ownOutput <- ((HRec
    ((':)
       @(Symbol, Type)
       '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
       ((':)
          @(Symbol, Type)
          '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
          ('[] @(Symbol, Type))))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
           ((':)
              @(Symbol, Type)
              '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
              ('[] @(Symbol, Type)))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
        ((':)
           @(Symbol, Type)
           '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
           ('[] @(Symbol, Type))))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
            ((':)
               @(Symbol, Type)
               '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
               ('[] @(Symbol, Type))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
          ((':)
             @(Symbol, Type)
             '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
             ('[] @(Symbol, Type))))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
           ((':)
              @(Symbol, Type)
              '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
              ('[] @(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 @'["value", "datumHash"] (Term s (PAsData PTxOut)
 -> (HRecOf
       (PAsData PTxOut)
       ((':) @Symbol "value" ((':) @Symbol "datumHash" ('[] @Symbol)))
       s
     -> Term s POpaque)
 -> Term s POpaque)
-> Term s (PAsData PTxOut)
-> (HRecOf
      (PAsData PTxOut)
      ((':) @Symbol "value" ((':) @Symbol "datumHash" ('[] @Symbol)))
      s
    -> Term s POpaque)
-> Term s POpaque
forall a b. (a -> b) -> a -> b
$ Term s (PBuiltinList (PAsData PTxOut) :--> PAsData PTxOut)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (PBuiltinList (PAsData PTxOut) :--> PAsData PTxOut)
-> Term s (PBuiltinList (PAsData PTxOut))
-> Term s (PAsData PTxOut)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PAsData PTxOut))
ownOutputs
    let ownOuputGSTAmount :: Term s (PInteger @S)
ownOuputGSTAmount = Term
  s
  (PCurrencySymbol :--> (PValue 'Sorted 'Positive :--> PInteger @S))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term
  s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger @S))
psymbolValueOf Term
  s
  (PCurrencySymbol :--> (PValue 'Sorted 'Positive :--> PInteger @S))
-> Term s PCurrencySymbol
-> Term s (PValue 'Sorted 'Positive :--> PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
forall (s :: S). Term s PCurrencySymbol
pgstSymbol Term s (PValue 'Sorted 'Positive :--> PInteger @S)
-> Term s (PValue 'Sorted 'Positive) -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  ((':)
     @(Symbol, Type)
     '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
     ((':)
        @(Symbol, Type)
        '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
        ('[] @(Symbol, Type))))
ownOutput.value
    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)
"State token should stay at governor's address" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
      Term s (PInteger @S)
ownOuputGSTAmount Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PInteger @S)
1

    -- Check that own output have datum of type 'GovernorDatum'.
    let outputGovernorStateDatumHash :: Term s PDatumHash
outputGovernorStateDatumHash =
          Term s (PString @S :--> (PMaybeData PDatumHash :--> PDatumHash))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PString @S :--> (PMaybeData a :--> a))
mustBePDJust Term s (PString @S :--> (PMaybeData PDatumHash :--> PDatumHash))
-> Term s (PString @S)
-> Term s (PMaybeData PDatumHash :--> PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"Governor output doesn't have datum" Term s (PMaybeData PDatumHash :--> PDatumHash)
-> Term s (PMaybeData PDatumHash) -> Term s PDatumHash
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  ((':)
     @(Symbol, Type)
     '("value", Term s (PAsData (PValue 'Sorted 'Positive)))
     ((':)
        @(Symbol, Type)
        '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
        ('[] @(Symbol, Type))))
ownOutput.datumHash
    Term s PGovernorDatum
newGovernorDatum <-
      Term s PGovernorDatum
-> TermCont @POpaque s (Term s PGovernorDatum)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PGovernorDatum
 -> TermCont @POpaque s (Term s PGovernorDatum))
-> Term s PGovernorDatum
-> TermCont @POpaque s (Term s PGovernorDatum)
forall a b. (a -> b) -> a -> b
$
        Term s (PAsData PGovernorDatum) -> Term s PGovernorDatum
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PGovernorDatum) -> Term s PGovernorDatum)
-> Term s (PAsData PGovernorDatum) -> Term s PGovernorDatum
forall a b. (a -> b) -> a -> b
$
          Term
  s
  (PString @S
   :--> (PMaybe (PAsData PGovernorDatum) :--> PAsData PGovernorDatum))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust Term
  s
  (PString @S
   :--> (PMaybe (PAsData PGovernorDatum) :--> PAsData PGovernorDatum))
-> Term s (PString @S)
-> Term
     s (PMaybe (PAsData PGovernorDatum) :--> PAsData PGovernorDatum)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"Ouput governor state datum not found"
            #$ ptryFindDatum # outputGovernorStateDatumHash # txInfoF.datums
    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)
"New datum is not valid" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$ Term s (PGovernorDatum :--> PBool)
forall (s :: S). Term s (PGovernorDatum :--> PBool)
governorDatumValid Term s (PGovernorDatum :--> PBool)
-> Term s PGovernorDatum -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PGovernorDatum
newGovernorDatum

    Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s POpaque -> TermCont @POpaque s (Term s POpaque))
-> Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$
      Term s PGovernorRedeemer
-> (PGovernorRedeemer s -> Term s POpaque) -> Term s POpaque
forall (a :: PType) (s :: S) (b :: PType).
PMatch a =>
Term s a -> (a s -> Term s b) -> Term s b
pmatch Term s PGovernorRedeemer
redeemer ((PGovernorRedeemer s -> Term s POpaque) -> Term s POpaque)
-> (PGovernorRedeemer s -> Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ \case
        PCreateProposal Term s (PDataRecord ('[] @PLabeledType))
_ -> 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
          -- Check that the transaction advances proposal id.

          let expectedNextProposalId :: Term s PProposalId
expectedNextProposalId = Term s (PProposalId :--> PProposalId)
forall (s :: S). Term s (PProposalId :--> PProposalId)
pgetNextProposalId Term s (PProposalId :--> PProposalId)
-> Term s PProposalId -> Term s PProposalId
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  ((':)
     @(Symbol, Type)
     '("proposalThresholds", Term s (PAsData PProposalThresholds))
     ((':)
        @(Symbol, Type)
        '("nextProposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("proposalTimings", Term s (PAsData PProposalTimingConfig))
           ((':)
              @(Symbol, Type)
              '("createProposalTimeRangeMaxWidth",
                Term s (PAsData PMaxTimeRangeWidth))
              ('[] @(Symbol, Type))))))
oldGovernorDatumF.nextProposalId
              expectedNewDatum :: Term s PGovernorDatum
expectedNewDatum =
                (forall (s' :: S).
 Term
   s'
   (PDataRecord
      ((':)
         @PLabeledType
         ("proposalThresholds" ':= PProposalThresholds)
         ((':)
            @PLabeledType
            ("nextProposalId" ':= PProposalId)
            ((':)
               @PLabeledType
               ("proposalTimings" ':= PProposalTimingConfig)
               ((':)
                  @PLabeledType
                  ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
                  ('[] @PLabeledType))))))
 -> PGovernorDatum s')
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("proposalThresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("nextProposalId" ':= PProposalId)
           ((':)
              @PLabeledType
              ("proposalTimings" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
                 ('[] @PLabeledType)))))
-> Term s PGovernorDatum
forall (r :: [PLabeledType]) (s :: S) (pt :: PType).
PlutusType pt =>
(forall (s' :: S). Term s' (PDataRecord r) -> pt s')
-> RecordMorphism s ('[] @PLabeledType) r -> Term s pt
mkRecordConstr
                  forall (s' :: S).
Term
  s'
  (PDataRecord
     ((':)
        @PLabeledType
        ("proposalThresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("nextProposalId" ':= PProposalId)
           ((':)
              @PLabeledType
              ("proposalTimings" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
                 ('[] @PLabeledType))))))
-> PGovernorDatum s'
PGovernorDatum
                  ( FieldName "proposalThresholds"
#proposalThresholds FieldName "proposalThresholds"
-> Term s (PAsData PProposalThresholds)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("nextProposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("proposalTimings" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
              ('[] @PLabeledType))))
     ((':)
        @PLabeledType
        ("proposalThresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("nextProposalId" ':= PProposalId)
           ((':)
              @PLabeledType
              ("proposalTimings" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
                 ('[] @PLabeledType)))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalThresholds", Term s (PAsData PProposalThresholds))
     ((':)
        @(Symbol, Type)
        '("nextProposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("proposalTimings", Term s (PAsData PProposalTimingConfig))
           ((':)
              @(Symbol, Type)
              '("createProposalTimeRangeMaxWidth",
                Term s (PAsData PMaxTimeRangeWidth))
              ('[] @(Symbol, Type))))))
oldGovernorDatumF.proposalThresholds
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("nextProposalId" ':= PProposalId)
     ((':)
        @PLabeledType
        ("proposalTimings" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
           ('[] @PLabeledType))))
  ((':)
     @PLabeledType
     ("proposalThresholds" ':= PProposalThresholds)
     ((':)
        @PLabeledType
        ("nextProposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("proposalTimings" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
              ('[] @PLabeledType)))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("nextProposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("proposalTimings" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
              ('[] @PLabeledType))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("proposalThresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("nextProposalId" ':= PProposalId)
           ((':)
              @PLabeledType
              ("proposalTimings" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
                 ('[] @PLabeledType)))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "nextProposalId"
#nextProposalId FieldName "nextProposalId"
-> Term s (PAsData PProposalId)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("proposalTimings" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
           ('[] @PLabeledType)))
     ((':)
        @PLabeledType
        ("nextProposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("proposalTimings" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
              ('[] @PLabeledType))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= Term s PProposalId -> Term s (PAsData PProposalId)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PProposalId
expectedNextProposalId
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("proposalTimings" ':= PProposalTimingConfig)
     ((':)
        @PLabeledType
        ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
        ('[] @PLabeledType)))
  ((':)
     @PLabeledType
     ("nextProposalId" ':= PProposalId)
     ((':)
        @PLabeledType
        ("proposalTimings" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
           ('[] @PLabeledType))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("proposalTimings" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
           ('[] @PLabeledType)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("nextProposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("proposalTimings" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
              ('[] @PLabeledType))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "proposalTimings"
#proposalTimings FieldName "proposalTimings"
-> Term s (PAsData PProposalTimingConfig)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
        ('[] @PLabeledType))
     ((':)
        @PLabeledType
        ("proposalTimings" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
           ('[] @PLabeledType)))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalThresholds", Term s (PAsData PProposalThresholds))
     ((':)
        @(Symbol, Type)
        '("nextProposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("proposalTimings", Term s (PAsData PProposalTimingConfig))
           ((':)
              @(Symbol, Type)
              '("createProposalTimeRangeMaxWidth",
                Term s (PAsData PMaxTimeRangeWidth))
              ('[] @(Symbol, Type))))))
oldGovernorDatumF.proposalTimings
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
     ('[] @PLabeledType))
  ((':)
     @PLabeledType
     ("proposalTimings" ':= PProposalTimingConfig)
     ((':)
        @PLabeledType
        ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
        ('[] @PLabeledType)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
        ('[] @PLabeledType))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("proposalTimings" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
           ('[] @PLabeledType)))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "createProposalTimeRangeMaxWidth"
#createProposalTimeRangeMaxWidth
                        FieldName "createProposalTimeRangeMaxWidth"
-> Term s (PAsData PMaxTimeRangeWidth)
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("createProposalTimeRangeMaxWidth" ':= PMaxTimeRangeWidth)
        ('[] @PLabeledType))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalThresholds", Term s (PAsData PProposalThresholds))
     ((':)
        @(Symbol, Type)
        '("nextProposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("proposalTimings", Term s (PAsData PProposalTimingConfig))
           ((':)
              @(Symbol, Type)
              '("createProposalTimeRangeMaxWidth",
                Term s (PAsData PMaxTimeRangeWidth))
              ('[] @(Symbol, Type))))))
oldGovernorDatumF.createProposalTimeRangeMaxWidth
                  )
          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)
"Unexpected governor state datum" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s PGovernorDatum
newGovernorDatum Term s PGovernorDatum -> Term s PGovernorDatum -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PGovernorDatum
expectedNewDatum

          -- Check that exactly one proposal token is being minted.

          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)
"Exactly one proposal token must be minted" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term
  s (PCurrencySymbol :--> (PValue 'Sorted 'NoGuarantees :--> PBool))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term s (PCurrencySymbol :--> (PValue keys amounts :--> PBool))
hasOnlyOneTokenOfCurrencySymbol Term
  s (PCurrencySymbol :--> (PValue 'Sorted 'NoGuarantees :--> PBool))
-> Term s PCurrencySymbol
-> Term s (PValue 'Sorted 'NoGuarantees :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
forall (s :: S). Term s PCurrencySymbol
ppstSymbol Term s (PValue 'Sorted 'NoGuarantees :--> PBool)
-> Term s (PValue 'Sorted 'NoGuarantees) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol
                    "datums"
                    ((':)
                       @Symbol
                       "signatories"
                       ((':) @Symbol "validRange" ('[] @Symbol))))))))
     s)
txInfoF.mint

          -- Check that a stake is spent to create the propsal,
          --   and the value it contains meets the requirement.

          Term s (PAsData PTxInInfo)
stakeInput <-
            Term s (PAsData PTxInInfo)
-> TermCont @POpaque s (Term s (PAsData PTxInInfo))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PAsData PTxInInfo)
 -> TermCont @POpaque s (Term s (PAsData PTxInInfo)))
-> Term s (PAsData PTxInInfo)
-> TermCont @POpaque s (Term s (PAsData PTxInInfo))
forall a b. (a -> b) -> a -> b
$
              Term
  s
  (PString @S
   :--> (PMaybe (PAsData PTxInInfo) :--> PAsData PTxInInfo))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust Term
  s
  (PString @S
   :--> (PMaybe (PAsData PTxInInfo) :--> PAsData PTxInInfo))
-> Term s (PString @S)
-> Term s (PMaybe (PAsData PTxInInfo) :--> PAsData PTxInInfo)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"Stake input not found" Term s (PMaybe (PAsData PTxInInfo) :--> PAsData PTxInInfo)
-> Term s (PMaybe (PAsData PTxInInfo))
-> Term s (PAsData PTxInInfo)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  ((PAsData PTxInInfo :--> PBool)
   :--> (PBuiltinList (PAsData PTxInInfo)
         :--> PMaybe (PAsData PTxInInfo)))
forall (l :: PType -> PType) (a :: PType) (s :: S).
PIsListLike l a =>
Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
pfind
                # phoistAcyclic
                  ( plam $
                      \((pfield @"resolved" #) -> txOut') -> unTermCont $ do
                        txOut <- tcont $ pletFields @'["address", "value"] txOut'

                        pure $
                          txOut.address #== pdata pstakeValidatorAddress
                            #&& psymbolValueOf # psstSymbol # txOut.value #== 1
                  )
                # pfromData txInfoF.inputs

          HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
     s)
stakeInputF <- ((HRec
    (BoundTerms
       (PFields (PAsData PTxOut))
       (Bindings
          (PFields (PAsData PTxOut))
          ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
       s)
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':) @Symbol "datumHash" ((':) @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 "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
        s)
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         (BoundTerms
            (PFields (PAsData PTxOut))
            (Bindings
               (PFields (PAsData PTxOut))
               ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PAsData PTxOut))
          (Bindings
             (PFields (PAsData PTxOut))
             ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
          s)
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':) @Symbol "datumHash" ((':) @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 @'["datumHash", "value"] (Term s (PAsData PTxOut)
 -> (HRec
       (BoundTerms
          (PFields (PAsData PTxOut))
          (Bindings
             (PFields (PAsData PTxOut))
             ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
          s)
     -> Term s POpaque)
 -> Term s POpaque)
-> Term s (PAsData PTxOut)
-> (HRec
      (BoundTerms
         (PFields (PAsData PTxOut))
         (Bindings
            (PFields (PAsData PTxOut))
            ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
         s)
    -> Term s POpaque)
-> Term s POpaque
forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"resolved" Term s (PAsData PTxInInfo :--> PAsData PTxOut)
-> Term s (PAsData PTxInInfo) -> Term s (PAsData PTxOut)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PTxInInfo)
stakeInput

          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)
"Stake input doesn't have datum" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PMaybeData PDatumHash :--> PBool)
forall (a :: PType) (s :: S). Term s (PMaybeData a :--> PBool)
pisDJust Term s (PMaybeData PDatumHash :--> PBool)
-> Term s (PMaybeData PDatumHash) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
     s)
stakeInputF.datumHash

          let stakeInputDatum :: Term s PStakeDatum
stakeInputDatum = forall (datum :: PType) (s :: S).
(PIsData datum, PTryFrom PData (PAsData datum)) =>
Term
  s
  (PMaybeData PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> datum))
mustFindDatum' @PStakeDatum Term
  s
  (PMaybeData PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> PStakeDatum))
-> Term s (PMaybeData PDatumHash)
-> Term
     s
     (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
      :--> PStakeDatum)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
     s)
stakeInputF.datumHash Term
  s
  (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
   :--> PStakeDatum)
-> Term s (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))
-> Term s PStakeDatum
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol
                    "datums"
                    ((':)
                       @Symbol
                       "signatories"
                       ((':) @Symbol "validRange" ('[] @Symbol))))))))
     s)
txInfoF.datums

          HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ((':)
           @(Symbol, Type)
           '("lockedBy",
             Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
           ('[] @(Symbol, Type)))))
stakeInputDatumF <-
            ((HRec
    ((':)
       @(Symbol, Type)
       '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
       ((':)
          @(Symbol, Type)
          '("owner", Term s (PAsData PPubKeyHash))
          ((':)
             @(Symbol, Type)
             '("lockedBy",
               Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
             ('[] @(Symbol, Type)))))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
           ((':)
              @(Symbol, Type)
              '("owner", Term s (PAsData PPubKeyHash))
              ((':)
                 @(Symbol, Type)
                 '("lockedBy",
                   Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
                 ('[] @(Symbol, Type))))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
        ((':)
           @(Symbol, Type)
           '("owner", Term s (PAsData PPubKeyHash))
           ((':)
              @(Symbol, Type)
              '("lockedBy",
                Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
              ('[] @(Symbol, Type)))))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
            ((':)
               @(Symbol, Type)
               '("owner", Term s (PAsData PPubKeyHash))
               ((':)
                  @(Symbol, Type)
                  '("lockedBy",
                    Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
                  ('[] @(Symbol, Type)))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
          ((':)
             @(Symbol, Type)
             '("owner", Term s (PAsData PPubKeyHash))
             ((':)
                @(Symbol, Type)
                '("lockedBy",
                  Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
                ('[] @(Symbol, Type)))))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
           ((':)
              @(Symbol, Type)
              '("owner", Term s (PAsData PPubKeyHash))
              ((':)
                 @(Symbol, Type)
                 '("lockedBy",
                   Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
                 ('[] @(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 @["stakedAmount", "owner", "lockedBy"] Term s PStakeDatum
stakeInputDatum

          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)
"Required amount of stake GTs should be presented" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ((':)
           @(Symbol, Type)
           '("lockedBy",
             Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
           ('[] @(Symbol, Type)))))
stakeInputDatumF.stakedAmount Term s (PDiscrete @Type GTTag)
-> Term s (PDiscrete @Type GTTag) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (Term s (PValue 'Sorted 'Positive :--> PDiscrete @Type GTTag)
forall (s :: S) {w :: KeyGuarantees} {w :: AmountGuarantees}.
Term s (PValue w w :--> PDiscrete @Type GTTag)
pgtValueOf Term s (PValue 'Sorted 'Positive :--> PDiscrete @Type GTTag)
-> Term s (PValue 'Sorted 'Positive)
-> Term s (PDiscrete @Type GTTag)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
     s)
stakeInputF.value)

          -- TODO: Is this required?
          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)
"Tx should be signed by the stake owner" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term
  s
  (PBuiltinList (PAsData PPubKeyHash)
   :--> (PAsData PPubKeyHash :--> PBool))
forall (s :: S).
Term
  s
  (PBuiltinList (PAsData PPubKeyHash)
   :--> (PAsData PPubKeyHash :--> PBool))
ptxSignedBy Term
  s
  (PBuiltinList (PAsData PPubKeyHash)
   :--> (PAsData PPubKeyHash :--> PBool))
-> Term s (PBuiltinList (PAsData PPubKeyHash))
-> Term s (PAsData PPubKeyHash :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol
                    "datums"
                    ((':)
                       @Symbol
                       "signatories"
                       ((':) @Symbol "validRange" ('[] @Symbol))))))))
     s)
txInfoF.signatories Term s (PAsData PPubKeyHash :--> PBool)
-> Term s (PAsData PPubKeyHash) -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ((':)
           @(Symbol, Type)
           '("lockedBy",
             Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
           ('[] @(Symbol, Type)))))
stakeInputDatumF.owner

          -- Check that the newly minted PST is sent to the proposal validator,
          --   and the datum it carries is legal.

          Term s (PBuiltinList (PAsData PTxOut))
outputsToProposalValidatorWithStateToken <-
            Term s (PBuiltinList (PAsData PTxOut))
-> TermCont @POpaque s (Term s (PBuiltinList (PAsData PTxOut)))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PBuiltinList (PAsData PTxOut))
 -> TermCont @POpaque s (Term s (PBuiltinList (PAsData PTxOut))))
-> Term s (PBuiltinList (PAsData PTxOut))
-> TermCont @POpaque s (Term s (PBuiltinList (PAsData PTxOut)))
forall a b. (a -> b) -> a -> b
$
              Term
  s
  ((PAsData PTxOut :--> PBool)
   :--> (PBuiltinList (PAsData PTxOut)
         :--> PBuiltinList (PAsData PTxOut)))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> list a))
pfilter
                # phoistAcyclic
                  ( plam $
                      \txOut' -> unTermCont $ do
                        txOut <- tcont $ pletFields @'["address", "value"] txOut'

                        pure $
                          txOut.address #== pdata pproposalValidatorAddress
                            #&& psymbolValueOf # ppstSymbol # txOut.value #== 1
                  )
                # pfromData txInfoF.outputs

          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)
"Exactly one UTXO with proposal state token should be sent to the proposal validator" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PBuiltinList (PAsData PTxOut) :--> PInteger @S)
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> PInteger @S)
plength Term s (PBuiltinList (PAsData PTxOut) :--> PInteger @S)
-> Term s (PBuiltinList (PAsData PTxOut)) -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PAsData PTxOut))
outputsToProposalValidatorWithStateToken Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PInteger @S)
1

          Term s (PMaybeData PDatumHash)
outputDatumHash <- Term s (PMaybeData PDatumHash)
-> TermCont @POpaque s (Term s (PMaybeData PDatumHash))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PMaybeData PDatumHash)
 -> TermCont @POpaque s (Term s (PMaybeData PDatumHash)))
-> Term s (PMaybeData PDatumHash)
-> TermCont @POpaque s (Term s (PMaybeData PDatumHash))
forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"datumHash" Term s (PAsData PTxOut :--> PMaybeData PDatumHash)
-> Term s (PAsData PTxOut) -> Term s (PMaybeData PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s (PBuiltinList (PAsData PTxOut) :--> PAsData PTxOut)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term s (PBuiltinList (PAsData PTxOut) :--> PAsData PTxOut)
-> Term s (PBuiltinList (PAsData PTxOut))
-> Term s (PAsData PTxOut)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PAsData PTxOut))
outputsToProposalValidatorWithStateToken

          Term s PProposalDatum
proposalOutputDatum' <-
            Term s PProposalDatum
-> TermCont @POpaque s (Term s PProposalDatum)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PProposalDatum
 -> TermCont @POpaque s (Term s PProposalDatum))
-> Term s PProposalDatum
-> TermCont @POpaque s (Term s PProposalDatum)
forall a b. (a -> b) -> a -> b
$
              forall (datum :: PType) (s :: S).
(PIsData datum, PTryFrom PData (PAsData datum)) =>
Term
  s
  (PMaybeData PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> datum))
mustFindDatum' @PProposalDatum
                # outputDatumHash
                # txInfoF.datums

          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)
"Proposal datum must be valid" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PProposalDatum :--> PBool)
forall (s :: S). Term s (PProposalDatum :--> PBool)
proposalDatumValid' Term s (PProposalDatum :--> PBool)
-> Term s PProposalDatum -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PProposalDatum
proposalOutputDatum'

          HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("cosigners",
             Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
           ((':)
              @(Symbol, Type)
              '("votes", Term s (PAsData PProposalVotes))
              ('[] @(Symbol, Type))))))
proposalOutputDatum <-
            ((HRec
    ((':)
       @(Symbol, Type)
       '("proposalId", Term s (PAsData PProposalId))
       ((':)
          @(Symbol, Type)
          '("effects",
            Term
              s
              (PAsData
                 (PMap
                    'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
          ((':)
             @(Symbol, Type)
             '("cosigners",
               Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
             ((':)
                @(Symbol, Type)
                '("votes", Term s (PAsData PProposalVotes))
                ('[] @(Symbol, Type))))))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("proposalId", Term s (PAsData PProposalId))
           ((':)
              @(Symbol, Type)
              '("effects",
                Term
                  s
                  (PAsData
                     (PMap
                        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
              ((':)
                 @(Symbol, Type)
                 '("cosigners",
                   Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ('[] @(Symbol, Type)))))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("proposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("effects",
             Term
               s
               (PAsData
                  (PMap
                     'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("votes", Term s (PAsData PProposalVotes))
                 ('[] @(Symbol, Type))))))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("proposalId", Term s (PAsData PProposalId))
            ((':)
               @(Symbol, Type)
               '("effects",
                 Term
                   s
                   (PAsData
                      (PMap
                         'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
               ((':)
                  @(Symbol, Type)
                  '("cosigners",
                    Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                  ((':)
                     @(Symbol, Type)
                     '("votes", Term s (PAsData PProposalVotes))
                     ('[] @(Symbol, Type))))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("proposalId", Term s (PAsData PProposalId))
          ((':)
             @(Symbol, Type)
             '("effects",
               Term
                 s
                 (PAsData
                    (PMap
                       'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
             ((':)
                @(Symbol, Type)
                '("cosigners",
                  Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                ((':)
                   @(Symbol, Type)
                   '("votes", Term s (PAsData PProposalVotes))
                   ('[] @(Symbol, Type))))))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("proposalId", Term s (PAsData PProposalId))
           ((':)
              @(Symbol, Type)
              '("effects",
                Term
                  s
                  (PAsData
                     (PMap
                        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
              ((':)
                 @(Symbol, Type)
                 '("cosigners",
                   Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ('[] @(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
                @'["effects", "cosigners", "proposalId", "votes"]
                Term s PProposalDatum
proposalOutputDatum'

          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)
"Proposal should have only one cosigner" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PBuiltinList (PAsData PPubKeyHash) :--> PInteger @S)
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> PInteger @S)
plength Term s (PBuiltinList (PAsData PPubKeyHash) :--> PInteger @S)
-> Term s (PBuiltinList (PAsData PPubKeyHash))
-> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData (PBuiltinList (PAsData PPubKeyHash)))
-> Term s (PBuiltinList (PAsData PPubKeyHash))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("cosigners",
             Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
           ((':)
              @(Symbol, Type)
              '("votes", Term s (PAsData PProposalVotes))
              ('[] @(Symbol, Type))))))
proposalOutputDatum.cosigners Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PInteger @S)
1

          let -- Votes should be empty at this point
              expectedVotes :: Term s PProposalVotes
expectedVotes = Term
  s
  (PMap
     'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)
   :--> PProposalVotes)
forall (s :: S) (a :: PType).
PIsData a =>
Term s (PMap 'Unsorted PResultTag a :--> PProposalVotes)
pemptyVotesFor Term
  s
  (PMap
     'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)
   :--> PProposalVotes)
-> Term
     s
     (PMap
        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
-> Term s PProposalVotes
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PAsData
     (PMap
        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)))
-> Term
     s
     (PMap
        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("cosigners",
             Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
           ((':)
              @(Symbol, Type)
              '("votes", Term s (PAsData PProposalVotes))
              ('[] @(Symbol, Type))))))
proposalOutputDatum.effects
              expectedStartingTime :: Term s PProposalStartingTime
expectedStartingTime =
                Term
  s
  (PMaxTimeRangeWidth
   :--> (PPOSIXTimeRange :--> PProposalStartingTime))
forall (s :: S).
Term
  s
  (PMaxTimeRangeWidth
   :--> (PPOSIXTimeRange :--> PProposalStartingTime))
createProposalStartingTime
                  # oldGovernorDatumF.createProposalTimeRangeMaxWidth
                  # txInfoF.validRange
              -- Id, thresholds and timings should be copied from the old governor state datum.
              expectedProposalOut :: Term s PProposalDatum
expectedProposalOut =
                (forall (s' :: S).
 Term
   s'
   (PDataRecord
      ((':)
         @PLabeledType
         ("proposalId" ':= PProposalId)
         ((':)
            @PLabeledType
            ("effects"
             ':= PMap
                   'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
            ((':)
               @PLabeledType
               ("status" ':= PProposalStatus)
               ((':)
                  @PLabeledType
                  ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                  ((':)
                     @PLabeledType
                     ("thresholds" ':= PProposalThresholds)
                     ((':)
                        @PLabeledType
                        ("votes" ':= PProposalVotes)
                        ((':)
                           @PLabeledType
                           ("timingConfig" ':= PProposalTimingConfig)
                           ((':)
                              @PLabeledType
                              ("startingTime" ':= PProposalStartingTime)
                              ('[] @PLabeledType))))))))))
 -> PProposalDatum s')
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("proposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("effects"
            ':= PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
           ((':)
              @PLabeledType
              ("status" ':= PProposalStatus)
              ((':)
                 @PLabeledType
                 ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                 ((':)
                    @PLabeledType
                    ("thresholds" ':= PProposalThresholds)
                    ((':)
                       @PLabeledType
                       ("votes" ':= PProposalVotes)
                       ((':)
                          @PLabeledType
                          ("timingConfig" ':= PProposalTimingConfig)
                          ((':)
                             @PLabeledType
                             ("startingTime" ':= PProposalStartingTime)
                             ('[] @PLabeledType)))))))))
-> Term s PProposalDatum
forall (r :: [PLabeledType]) (s :: S) (pt :: PType).
PlutusType pt =>
(forall (s' :: S). Term s' (PDataRecord r) -> pt s')
-> RecordMorphism s ('[] @PLabeledType) r -> Term s pt
mkRecordConstr
                  forall (s' :: S).
Term
  s'
  (PDataRecord
     ((':)
        @PLabeledType
        ("proposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("effects"
            ':= PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
           ((':)
              @PLabeledType
              ("status" ':= PProposalStatus)
              ((':)
                 @PLabeledType
                 ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                 ((':)
                    @PLabeledType
                    ("thresholds" ':= PProposalThresholds)
                    ((':)
                       @PLabeledType
                       ("votes" ':= PProposalVotes)
                       ((':)
                          @PLabeledType
                          ("timingConfig" ':= PProposalTimingConfig)
                          ((':)
                             @PLabeledType
                             ("startingTime" ':= PProposalStartingTime)
                             ('[] @PLabeledType))))))))))
-> PProposalDatum s'
PProposalDatum
                  ( FieldName "proposalId"
#proposalId FieldName "proposalId"
-> Term s (PAsData PProposalId)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType))))))))
     ((':)
        @PLabeledType
        ("proposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("effects"
            ':= PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
           ((':)
              @PLabeledType
              ("status" ':= PProposalStatus)
              ((':)
                 @PLabeledType
                 ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                 ((':)
                    @PLabeledType
                    ("thresholds" ':= PProposalThresholds)
                    ((':)
                       @PLabeledType
                       ("votes" ':= PProposalVotes)
                       ((':)
                          @PLabeledType
                          ("timingConfig" ':= PProposalTimingConfig)
                          ((':)
                             @PLabeledType
                             ("startingTime" ':= PProposalStartingTime)
                             ('[] @PLabeledType)))))))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalThresholds", Term s (PAsData PProposalThresholds))
     ((':)
        @(Symbol, Type)
        '("nextProposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("proposalTimings", Term s (PAsData PProposalTimingConfig))
           ((':)
              @(Symbol, Type)
              '("createProposalTimeRangeMaxWidth",
                Term s (PAsData PMaxTimeRangeWidth))
              ('[] @(Symbol, Type))))))
oldGovernorDatumF.nextProposalId
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("effects"
      ':= PMap
            'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType))))))))
  ((':)
     @PLabeledType
     ("proposalId" ':= PProposalId)
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType)))))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType))))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("proposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("effects"
            ':= PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
           ((':)
              @PLabeledType
              ("status" ':= PProposalStatus)
              ((':)
                 @PLabeledType
                 ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                 ((':)
                    @PLabeledType
                    ("thresholds" ':= PProposalThresholds)
                    ((':)
                       @PLabeledType
                       ("votes" ':= PProposalVotes)
                       ((':)
                          @PLabeledType
                          ("timingConfig" ':= PProposalTimingConfig)
                          ((':)
                             @PLabeledType
                             ("startingTime" ':= PProposalStartingTime)
                             ('[] @PLabeledType)))))))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "effects"
#effects FieldName "effects"
-> Term
     s
     (PAsData
        (PMap
           'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)))
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType)))))))
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType))))))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("cosigners",
             Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
           ((':)
              @(Symbol, Type)
              '("votes", Term s (PAsData PProposalVotes))
              ('[] @(Symbol, Type))))))
proposalOutputDatum.effects
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("status" ':= PProposalStatus)
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType)))))))
  ((':)
     @PLabeledType
     ("effects"
      ':= PMap
            'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType))))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType)))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType))))))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "status"
#status FieldName "status"
-> Term s (PAsData PProposalStatus)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType))))))
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType)))))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= ProposalStatus -> Term s (PAsData PProposalStatus)
forall (p :: PType) h (s :: S).
(ToData h, (PLifted p :: Type) ~ (h :: Type),
 (PConstanted h :: PType) ~ (p :: PType)) =>
h -> Term s (PAsData p)
pconstantData ProposalStatus
Draft
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType))))))
  ((':)
     @PLabeledType
     ("status" ':= PProposalStatus)
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType)))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType)))))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "cosigners"
#cosigners FieldName "cosigners"
-> Term s (PAsData (PBuiltinList (PAsData PPubKeyHash)))
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType)))))
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType))))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("cosigners",
             Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
           ((':)
              @(Symbol, Type)
              '("votes", Term s (PAsData PProposalVotes))
              ('[] @(Symbol, Type))))))
proposalOutputDatum.cosigners
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("thresholds" ':= PProposalThresholds)
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType)))))
  ((':)
     @PLabeledType
     ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType)))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType))))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "thresholds"
#thresholds FieldName "thresholds"
-> Term s (PAsData PProposalThresholds)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType))))
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType)))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalThresholds", Term s (PAsData PProposalThresholds))
     ((':)
        @(Symbol, Type)
        '("nextProposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("proposalTimings", Term s (PAsData PProposalTimingConfig))
           ((':)
              @(Symbol, Type)
              '("createProposalTimeRangeMaxWidth",
                Term s (PAsData PMaxTimeRangeWidth))
              ('[] @(Symbol, Type))))))
oldGovernorDatumF.proposalThresholds
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("votes" ':= PProposalVotes)
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType))))
  ((':)
     @PLabeledType
     ("thresholds" ':= PProposalThresholds)
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType)))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType)))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "votes"
#votes FieldName "votes"
-> Term s (PAsData PProposalVotes)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType)))
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= Term s PProposalVotes -> Term s (PAsData PProposalVotes)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PProposalVotes
expectedVotes
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("timingConfig" ':= PProposalTimingConfig)
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType)))
  ((':)
     @PLabeledType
     ("votes" ':= PProposalVotes)
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "timingConfig"
#timingConfig FieldName "timingConfig"
-> Term s (PAsData PProposalTimingConfig)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType))
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType)))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalThresholds", Term s (PAsData PProposalThresholds))
     ((':)
        @(Symbol, Type)
        '("nextProposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("proposalTimings", Term s (PAsData PProposalTimingConfig))
           ((':)
              @(Symbol, Type)
              '("createProposalTimeRangeMaxWidth",
                Term s (PAsData PMaxTimeRangeWidth))
              ('[] @(Symbol, Type))))))
oldGovernorDatumF.proposalTimings
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("startingTime" ':= PProposalStartingTime)
     ('[] @PLabeledType))
  ((':)
     @PLabeledType
     ("timingConfig" ':= PProposalTimingConfig)
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType)))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "startingTime"
#startingTime FieldName "startingTime"
-> Term s (PAsData PProposalStartingTime)
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= Term s PProposalStartingTime
-> Term s (PAsData PProposalStartingTime)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PProposalStartingTime
expectedStartingTime
                  )

          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)
"Datum correct" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$ Term s PProposalDatum
expectedProposalOut Term s PProposalDatum -> Term s PProposalDatum -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PProposalDatum
proposalOutputDatum'

          let cosigner :: Term s (PAsData PPubKeyHash)
cosigner = Term
  s (PBuiltinList (PAsData PPubKeyHash) :--> PAsData PPubKeyHash)
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (list a :--> a)
phead Term
  s (PBuiltinList (PAsData PPubKeyHash) :--> PAsData PPubKeyHash)
-> Term s (PBuiltinList (PAsData PPubKeyHash))
-> Term s (PAsData PPubKeyHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData (PBuiltinList (PAsData PPubKeyHash)))
-> Term s (PBuiltinList (PAsData PPubKeyHash))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("cosigners",
             Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
           ((':)
              @(Symbol, Type)
              '("votes", Term s (PAsData PProposalVotes))
              ('[] @(Symbol, Type))))))
proposalOutputDatum.cosigners

          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)
"Cosigner should be the stake owner" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s PPubKeyHash -> Term s (PAsData PPubKeyHash)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ((':)
           @(Symbol, Type)
           '("lockedBy",
             Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
           ('[] @(Symbol, Type)))))
stakeInputDatumF.owner Term s (PAsData PPubKeyHash)
-> Term s (PAsData PPubKeyHash) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData PPubKeyHash)
cosigner

          -- Check the output stake has been proposly updated.

          Term s (PAsData PTxOut)
stakeOutput <-
            Term s (PAsData PTxOut)
-> TermCont @POpaque s (Term s (PAsData PTxOut))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PAsData PTxOut)
 -> TermCont @POpaque s (Term s (PAsData PTxOut)))
-> Term s (PAsData PTxOut)
-> TermCont @POpaque s (Term s (PAsData PTxOut))
forall a b. (a -> b) -> a -> b
$
              Term
  s (PString @S :--> (PMaybe (PAsData PTxOut) :--> PAsData PTxOut))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust
                # "Stake output not found"
                  #$ pfind
                # phoistAcyclic
                  ( plam $
                      \txOut' -> unTermCont $ do
                        txOut <- tcont $ pletFields @'["address", "value"] txOut'

                        pure $
                          txOut.address #== pdata pstakeValidatorAddress
                            #&& psymbolValueOf # psstSymbol # txOut.value #== 1
                  )
                # pfromData txInfoF.outputs

          HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
     s)
stakeOutputF <- ((HRec
    (BoundTerms
       (PFields (PAsData PTxOut))
       (Bindings
          (PFields (PAsData PTxOut))
          ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
       s)
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':) @Symbol "datumHash" ((':) @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 "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
        s)
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         (BoundTerms
            (PFields (PAsData PTxOut))
            (Bindings
               (PFields (PAsData PTxOut))
               ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PAsData PTxOut))
          (Bindings
             (PFields (PAsData PTxOut))
             ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
          s)
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':) @Symbol "datumHash" ((':) @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 @'["datumHash", "value"] (Term s (PAsData PTxOut)
 -> (HRec
       (BoundTerms
          (PFields (PAsData PTxOut))
          (Bindings
             (PFields (PAsData PTxOut))
             ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
          s)
     -> Term s POpaque)
 -> Term s POpaque)
-> Term s (PAsData PTxOut)
-> (HRec
      (BoundTerms
         (PFields (PAsData PTxOut))
         (Bindings
            (PFields (PAsData PTxOut))
            ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
         s)
    -> Term s POpaque)
-> Term s POpaque
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PTxOut)
stakeOutput

          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)
"Staked GTs should be sent back to stake validator" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ((':)
           @(Symbol, Type)
           '("lockedBy",
             Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
           ('[] @(Symbol, Type)))))
stakeInputDatumF.stakedAmount Term s (PDiscrete @Type GTTag)
-> Term s (PDiscrete @Type GTTag) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== (Term s (PValue 'Sorted 'Positive :--> PDiscrete @Type GTTag)
forall (s :: S) {w :: KeyGuarantees} {w :: AmountGuarantees}.
Term s (PValue w w :--> PDiscrete @Type GTTag)
pgtValueOf Term s (PValue 'Sorted 'Positive :--> PDiscrete @Type GTTag)
-> Term s (PValue 'Sorted 'Positive)
-> Term s (PDiscrete @Type GTTag)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
     s)
stakeOutputF.value)

          let stakeOutputDatumHash :: Term s PDatumHash
stakeOutputDatumHash = Term s (PString @S :--> (PMaybeData PDatumHash :--> PDatumHash))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PString @S :--> (PMaybeData a :--> a))
mustBePDJust Term s (PString @S :--> (PMaybeData PDatumHash :--> PDatumHash))
-> Term s (PString @S)
-> Term s (PMaybeData PDatumHash :--> PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"Stake output should have datum" Term s (PMaybeData PDatumHash :--> PDatumHash)
-> Term s (PMaybeData PDatumHash) -> Term s PDatumHash
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "datumHash" ((':) @Symbol "value" ('[] @Symbol))))
     s)
stakeOutputF.datumHash

              stakeOutputDatum :: Term s (PAsData PStakeDatum)
stakeOutputDatum =
                Term
  s
  (PString @S
   :--> (PMaybe (PAsData PStakeDatum) :--> PAsData PStakeDatum))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust Term
  s
  (PString @S
   :--> (PMaybe (PAsData PStakeDatum) :--> PAsData PStakeDatum))
-> Term s (PString @S)
-> Term s (PMaybe (PAsData PStakeDatum) :--> PAsData PStakeDatum)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"Stake output not found" Term s (PMaybe (PAsData PStakeDatum) :--> PAsData PStakeDatum)
-> Term s (PMaybe (PAsData PStakeDatum))
-> Term s (PAsData PStakeDatum)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> PMaybe (PAsData PStakeDatum)))
forall (a :: PType) (s :: S).
PTryFrom PData a =>
Term
  s
  (PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> PMaybe a))
ptryFindDatum Term
  s
  (PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> PMaybe (PAsData PStakeDatum)))
-> Term s PDatumHash
-> Term
     s
     (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
      :--> PMaybe (PAsData PStakeDatum))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PDatumHash
stakeOutputDatumHash Term
  s
  (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
   :--> PMaybe (PAsData PStakeDatum))
-> Term s (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))
-> Term s (PMaybe (PAsData PStakeDatum))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol
                    "datums"
                    ((':)
                       @Symbol
                       "signatories"
                       ((':) @Symbol "validRange" ('[] @Symbol))))))))
     s)
txInfoF.datums

          -- The stake should be locked by the newly created proposal.

          let possibleVoteResults :: Term s (PBuiltinList (PAsData PResultTag))
possibleVoteResults = Term
  s
  (PMap 'Unsorted PResultTag (PInteger @S)
   :--> PBuiltinList (PAsData PResultTag))
forall (k :: PType) (v :: PType) (keys :: KeyGuarantees) (s :: S).
Term s (PMap keys k v :--> PBuiltinList (PAsData k))
pkeys Term
  s
  (PMap 'Unsorted PResultTag (PInteger @S)
   :--> PBuiltinList (PAsData PResultTag))
-> Term s (PMap 'Unsorted PResultTag (PInteger @S))
-> Term s (PBuiltinList (PAsData PResultTag))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s PProposalVotes
-> forall (b :: PType). Term s (PInner PProposalVotes b)
forall (s :: S) (a :: PType).
Term s a -> forall (b :: PType). Term s (PInner a b)
pto (Term s PProposalVotes
 -> forall (b :: PType). Term s (PInner PProposalVotes b))
-> Term s PProposalVotes
-> forall (b :: PType). Term s (PInner PProposalVotes b)
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PProposalVotes) -> Term s PProposalVotes
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("cosigners",
             Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
           ((':)
              @(Symbol, Type)
              '("votes", Term s (PAsData PProposalVotes))
              ('[] @(Symbol, Type))))))
proposalOutputDatum.votes

              mkProposalLock :: Term _ (PProposalId :--> PAsData PResultTag :--> PAsData PProposalLock)
              mkProposalLock :: Term
  w
  (PProposalId :--> (PAsData PResultTag :--> PAsData PProposalLock))
mkProposalLock =
                ClosedTerm
  (PProposalId :--> (PAsData PResultTag :--> PAsData PProposalLock))
-> Term
     w
     (PProposalId :--> (PAsData PResultTag :--> PAsData PProposalLock))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (PProposalId :--> (PAsData PResultTag :--> PAsData PProposalLock))
 -> Term
      w
      (PProposalId :--> (PAsData PResultTag :--> PAsData PProposalLock)))
-> ClosedTerm
     (PProposalId :--> (PAsData PResultTag :--> PAsData PProposalLock))
-> Term
     w
     (PProposalId :--> (PAsData PResultTag :--> PAsData PProposalLock))
forall a b. (a -> b) -> a -> b
$
                  (Term s PProposalId
 -> Term s (PAsData PResultTag) -> Term s (PAsData PProposalLock))
-> Term
     s
     (PProposalId :--> (PAsData PResultTag :--> PAsData PProposalLock))
forall a (b :: PType) (s :: S) (c :: PType).
PLamN a b s =>
(Term s c -> a) -> Term s (c :--> b)
plam
                    ( \Term s PProposalId
pid Term s (PAsData PResultTag)
rt' ->
                        Term s PProposalLock -> Term s (PAsData PProposalLock)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s PProposalLock -> Term s (PAsData PProposalLock))
-> Term s PProposalLock -> Term s (PAsData PProposalLock)
forall a b. (a -> b) -> a -> b
$
                          (forall (s' :: S).
 Term
   s'
   (PDataRecord
      ((':)
         @PLabeledType
         ("vote" ':= PResultTag)
         ((':)
            @PLabeledType
            ("proposalTag" ':= PProposalId)
            ('[] @PLabeledType))))
 -> PProposalLock s')
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("vote" ':= PResultTag)
        ((':)
           @PLabeledType ("proposalTag" ':= PProposalId) ('[] @PLabeledType)))
-> Term s PProposalLock
forall (r :: [PLabeledType]) (s :: S) (pt :: PType).
PlutusType pt =>
(forall (s' :: S). Term s' (PDataRecord r) -> pt s')
-> RecordMorphism s ('[] @PLabeledType) r -> Term s pt
mkRecordConstr
                            forall (s' :: S).
Term
  s'
  (PDataRecord
     ((':)
        @PLabeledType
        ("vote" ':= PResultTag)
        ((':)
           @PLabeledType
           ("proposalTag" ':= PProposalId)
           ('[] @PLabeledType))))
-> PProposalLock s'
PProposalLock
                            ( FieldName "vote"
#vote FieldName "vote"
-> Term s (PAsData PResultTag)
-> RecordMorphism
     s
     ((':)
        @PLabeledType ("proposalTag" ':= PProposalId) ('[] @PLabeledType))
     ((':)
        @PLabeledType
        ("vote" ':= PResultTag)
        ((':)
           @PLabeledType ("proposalTag" ':= PProposalId) ('[] @PLabeledType)))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= Term s (PAsData PResultTag)
rt' RecordMorphism
  s
  ((':)
     @PLabeledType ("proposalTag" ':= PProposalId) ('[] @PLabeledType))
  ((':)
     @PLabeledType
     ("vote" ':= PResultTag)
     ((':)
        @PLabeledType ("proposalTag" ':= PProposalId) ('[] @PLabeledType)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType ("proposalTag" ':= PProposalId) ('[] @PLabeledType))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("vote" ':= PResultTag)
        ((':)
           @PLabeledType ("proposalTag" ':= PProposalId) ('[] @PLabeledType)))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "proposalTag"
#proposalTag FieldName "proposalTag"
-> Term s (PAsData PProposalId)
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType ("proposalTag" ':= PProposalId) ('[] @PLabeledType))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= Term s PProposalId -> Term s (PAsData PProposalId)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PProposalId
pid
                            )
                    )

              -- Append new locks to existing locks
              expectedProposalLocks :: Term s (PBuiltinList (PAsData PProposalLock))
expectedProposalLocks =
                Term
  s
  (PBuiltinList (PAsData PProposalLock)
   :--> (PBuiltinList (PAsData PProposalLock)
         :--> PBuiltinList (PAsData PProposalLock)))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> (list a :--> list a))
pconcat Term
  s
  (PBuiltinList (PAsData PProposalLock)
   :--> (PBuiltinList (PAsData PProposalLock)
         :--> PBuiltinList (PAsData PProposalLock)))
-> Term s (PBuiltinList (PAsData PProposalLock))
-> Term
     s
     (PBuiltinList (PAsData PProposalLock)
      :--> PBuiltinList (PAsData PProposalLock))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ((':)
           @(Symbol, Type)
           '("lockedBy",
             Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
           ('[] @(Symbol, Type)))))
stakeInputDatumF.lockedBy
                  #$ pmap # (mkProposalLock # proposalOutputDatum.proposalId) # possibleVoteResults

              expectedStakeOutputDatum :: Term s (PAsData PStakeDatum)
expectedStakeOutputDatum =
                Term s PStakeDatum -> Term s (PAsData PStakeDatum)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (Term s PStakeDatum -> Term s (PAsData PStakeDatum))
-> Term s PStakeDatum -> Term s (PAsData PStakeDatum)
forall a b. (a -> b) -> a -> b
$
                  (forall (s' :: S).
 Term
   s'
   (PDataRecord
      ((':)
         @PLabeledType
         ("stakedAmount" ':= PDiscrete @Type GTTag)
         ((':)
            @PLabeledType
            ("owner" ':= PPubKeyHash)
            ((':)
               @PLabeledType
               ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
               ('[] @PLabeledType)))))
 -> PStakeDatum s')
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("stakedAmount" ':= PDiscrete @Type GTTag)
        ((':)
           @PLabeledType
           ("owner" ':= PPubKeyHash)
           ((':)
              @PLabeledType
              ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
              ('[] @PLabeledType))))
-> Term s PStakeDatum
forall (r :: [PLabeledType]) (s :: S) (pt :: PType).
PlutusType pt =>
(forall (s' :: S). Term s' (PDataRecord r) -> pt s')
-> RecordMorphism s ('[] @PLabeledType) r -> Term s pt
mkRecordConstr
                    forall (s' :: S).
Term
  s'
  (PDataRecord
     ((':)
        @PLabeledType
        ("stakedAmount" ':= PDiscrete @Type GTTag)
        ((':)
           @PLabeledType
           ("owner" ':= PPubKeyHash)
           ((':)
              @PLabeledType
              ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
              ('[] @PLabeledType)))))
-> PStakeDatum s'
PStakeDatum
                    ( FieldName "stakedAmount"
#stakedAmount FieldName "stakedAmount"
-> Term s (PAsData (PDiscrete @Type GTTag))
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("owner" ':= PPubKeyHash)
        ((':)
           @PLabeledType
           ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
           ('[] @PLabeledType)))
     ((':)
        @PLabeledType
        ("stakedAmount" ':= PDiscrete @Type GTTag)
        ((':)
           @PLabeledType
           ("owner" ':= PPubKeyHash)
           ((':)
              @PLabeledType
              ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
              ('[] @PLabeledType))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ((':)
           @(Symbol, Type)
           '("lockedBy",
             Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
           ('[] @(Symbol, Type)))))
stakeInputDatumF.stakedAmount
                        RecordMorphism
  s
  ((':)
     @PLabeledType
     ("owner" ':= PPubKeyHash)
     ((':)
        @PLabeledType
        ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
        ('[] @PLabeledType)))
  ((':)
     @PLabeledType
     ("stakedAmount" ':= PDiscrete @Type GTTag)
     ((':)
        @PLabeledType
        ("owner" ':= PPubKeyHash)
        ((':)
           @PLabeledType
           ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
           ('[] @PLabeledType))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("owner" ':= PPubKeyHash)
        ((':)
           @PLabeledType
           ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
           ('[] @PLabeledType)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("stakedAmount" ':= PDiscrete @Type GTTag)
        ((':)
           @PLabeledType
           ("owner" ':= PPubKeyHash)
           ((':)
              @PLabeledType
              ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
              ('[] @PLabeledType))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "owner"
#owner FieldName "owner"
-> Term s (PAsData PPubKeyHash)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
        ('[] @PLabeledType))
     ((':)
        @PLabeledType
        ("owner" ':= PPubKeyHash)
        ((':)
           @PLabeledType
           ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
           ('[] @PLabeledType)))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ((':)
           @(Symbol, Type)
           '("lockedBy",
             Term s (PAsData (PBuiltinList (PAsData PProposalLock))))
           ('[] @(Symbol, Type)))))
stakeInputDatumF.owner
                        RecordMorphism
  s
  ((':)
     @PLabeledType
     ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
     ('[] @PLabeledType))
  ((':)
     @PLabeledType
     ("owner" ':= PPubKeyHash)
     ((':)
        @PLabeledType
        ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
        ('[] @PLabeledType)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
        ('[] @PLabeledType))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("owner" ':= PPubKeyHash)
        ((':)
           @PLabeledType
           ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
           ('[] @PLabeledType)))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "lockedBy"
#lockedBy FieldName "lockedBy"
-> Term s (PAsData (PBuiltinList (PAsData PProposalLock)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("lockedBy" ':= PBuiltinList (PAsData PProposalLock))
        ('[] @PLabeledType))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= Term s (PBuiltinList (PAsData PProposalLock))
-> Term s (PAsData (PBuiltinList (PAsData PProposalLock)))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PBuiltinList (PAsData PProposalLock))
expectedProposalLocks
                    )

          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)
"Unexpected stake output datum" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$ Term s (PAsData PStakeDatum)
expectedStakeOutputDatum Term s (PAsData PStakeDatum)
-> Term s (PAsData PStakeDatum) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PAsData PStakeDatum)
stakeOutputDatum

          Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s POpaque -> TermCont @POpaque s (Term s POpaque))
-> Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$ Term s (PUnit @S) -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (Term s (PUnit @S) -> Term s POpaque)
-> Term s (PUnit @S) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ()

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

        PMintGATs Term s (PDataRecord ('[] @PLabeledType))
_ -> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @POpaque s (Term s POpaque) -> Term s POpaque)
-> TermCont @POpaque s (Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ do
          Term s (PString @S) -> Term s PBool -> TermCont @POpaque s ()
forall {r :: PType} (s :: S).
Term s (PString @S) -> Term s PBool -> TermCont @r s ()
pguardC Term s (PString @S)
"Governor state should not be changed" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$ Term s PGovernorDatum
newGovernorDatum Term s PGovernorDatum -> Term s PGovernorDatum -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PGovernorDatum
oldGovernorDatum

          -- Filter out proposal inputs and ouputs using PST and the address of proposal validator.

          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)
"The governor can only process one proposal at a time" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            (Term
  s
  (PCurrencySymbol :--> (PValue 'Sorted 'Positive :--> PInteger @S))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term
  s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger @S))
psymbolValueOf Term
  s
  (PCurrencySymbol :--> (PValue 'Sorted 'Positive :--> PInteger @S))
-> Term s PCurrencySymbol
-> Term s (PValue 'Sorted 'Positive :--> PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
forall (s :: S). Term s PCurrencySymbol
ppstSymbol Term s (PValue 'Sorted 'Positive :--> PInteger @S)
-> Term s (PValue 'Sorted 'Positive) -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s (PBuiltinList (PAsData PTxInInfo) :--> PValue 'Sorted 'Positive)
forall (s :: S).
Term
  s (PBuiltinList (PAsData PTxInInfo) :--> PValue 'Sorted 'Positive)
pvalueSpent Term
  s (PBuiltinList (PAsData PTxInInfo) :--> PValue 'Sorted 'Positive)
-> Term s (PBuiltinList (PAsData PTxInInfo))
-> Term s (PValue 'Sorted 'Positive)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol
                    "datums"
                    ((':)
                       @Symbol
                       "signatories"
                       ((':) @Symbol "validRange" ('[] @Symbol))))))))
     s)
txInfoF.inputs) Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PInteger @S)
1

          HRec
  (BoundTerms
     (PFields
        (PAsData
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "resolved" (PFields PTxInInfo))
                 (PFields PTxInInfo)))))
     (Bindings
        (PFields
           (PAsData
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "resolved" (PFields PTxInInfo))
                    (PFields PTxInInfo)))))
        ((':) @Symbol "datumHash" ('[] @Symbol)))
     s)
proposalInputF <-
            ((HRec
    (BoundTerms
       (PFields
          (PAsData
             (PUnLabel
                (IndexList
                   @PLabeledType
                   (PLabelIndex "resolved" (PFields PTxInInfo))
                   (PFields PTxInInfo)))))
       (Bindings
          (PFields
             (PAsData
                (PUnLabel
                   (IndexList
                      @PLabeledType
                      (PLabelIndex "resolved" (PFields PTxInInfo))
                      (PFields PTxInInfo)))))
          ((':) @Symbol "datumHash" ('[] @Symbol)))
       s)
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields
              (PAsData
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "resolved" (PFields PTxInInfo))
                       (PFields PTxInInfo)))))
           (Bindings
              (PFields
                 (PAsData
                    (PUnLabel
                       (IndexList
                          @PLabeledType
                          (PLabelIndex "resolved" (PFields PTxInInfo))
                          (PFields PTxInInfo)))))
              ((':) @Symbol "datumHash" ('[] @Symbol)))
           s))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     (BoundTerms
        (PFields
           (PAsData
              (PUnLabel
                 (IndexList
                    @PLabeledType
                    (PLabelIndex "resolved" (PFields PTxInInfo))
                    (PFields PTxInInfo)))))
        (Bindings
           (PFields
              (PAsData
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "resolved" (PFields PTxInInfo))
                       (PFields PTxInInfo)))))
           ((':) @Symbol "datumHash" ('[] @Symbol)))
        s)
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         (BoundTerms
            (PFields
               (PAsData
                  (PUnLabel
                     (IndexList
                        @PLabeledType
                        (PLabelIndex "resolved" (PFields PTxInInfo))
                        (PFields PTxInInfo)))))
            (Bindings
               (PFields
                  (PAsData
                     (PUnLabel
                        (IndexList
                           @PLabeledType
                           (PLabelIndex "resolved" (PFields PTxInInfo))
                           (PFields PTxInInfo)))))
               ((':) @Symbol "datumHash" ('[] @Symbol)))
            s)))
-> ((HRec
       (BoundTerms
          (PFields
             (PAsData
                (PUnLabel
                   (IndexList
                      @PLabeledType
                      (PLabelIndex "resolved" (PFields PTxInInfo))
                      (PFields PTxInInfo)))))
          (Bindings
             (PFields
                (PAsData
                   (PUnLabel
                      (IndexList
                         @PLabeledType
                         (PLabelIndex "resolved" (PFields PTxInInfo))
                         (PFields PTxInInfo)))))
             ((':) @Symbol "datumHash" ('[] @Symbol)))
          s)
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields
              (PAsData
                 (PUnLabel
                    (IndexList
                       @PLabeledType
                       (PLabelIndex "resolved" (PFields PTxInInfo))
                       (PFields PTxInInfo)))))
           (Bindings
              (PFields
                 (PAsData
                    (PUnLabel
                       (IndexList
                          @PLabeledType
                          (PLabelIndex "resolved" (PFields PTxInInfo))
                          (PFields PTxInInfo)))))
              ((':) @Symbol "datumHash" ('[] @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 @'["datumHash"] (Term
   s
   (PAsData
      (PUnLabel
         (IndexList
            @PLabeledType
            (PLabelIndex "resolved" (PFields PTxInInfo))
            (PFields PTxInInfo))))
 -> (HRec
       (BoundTerms
          (PFields
             (PAsData
                (PUnLabel
                   (IndexList
                      @PLabeledType
                      (PLabelIndex "resolved" (PFields PTxInInfo))
                      (PFields PTxInInfo)))))
          (Bindings
             (PFields
                (PAsData
                   (PUnLabel
                      (IndexList
                         @PLabeledType
                         (PLabelIndex "resolved" (PFields PTxInInfo))
                         (PFields PTxInInfo)))))
             ((':) @Symbol "datumHash" ('[] @Symbol)))
          s)
     -> Term s POpaque)
 -> Term s POpaque)
-> Term
     s
     (PAsData
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "resolved" (PFields PTxInInfo))
              (PFields PTxInInfo))))
-> (HRec
      (BoundTerms
         (PFields
            (PAsData
               (PUnLabel
                  (IndexList
                     @PLabeledType
                     (PLabelIndex "resolved" (PFields PTxInInfo))
                     (PFields PTxInInfo)))))
         (Bindings
            (PFields
               (PAsData
                  (PUnLabel
                     (IndexList
                        @PLabeledType
                        (PLabelIndex "resolved" (PFields PTxInInfo))
                        (PFields PTxInInfo)))))
            ((':) @Symbol "datumHash" ('[] @Symbol)))
         s)
    -> Term s POpaque)
-> Term s POpaque
forall a b. (a -> b) -> a -> b
$
                forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"resolved"
                  #$ pfromData
                  $ mustBePJust
                    # "Proposal input not found"
                      #$ pfind
                    # plam
                      ( \((pfield @"resolved" #) -> txOut) -> unTermCont $ do
                          txOutF <- tcont $ pletFields @'["address", "value"] txOut

                          pure $
                            psymbolValueOf # ppstSymbol # txOutF.value #== 1
                              #&& txOutF.address #== pdata pproposalValidatorAddress
                      )
                    # pfromData txInfoF.inputs

          HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':) @Symbol "datumHash" ('[] @Symbol)))
     s)
proposalOutputF <-
            ((HRec
    (BoundTerms
       (PFields (PAsData PTxOut))
       (Bindings
          (PFields (PAsData PTxOut))
          ((':) @Symbol "datumHash" ('[] @Symbol)))
       s)
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':) @Symbol "datumHash" ('[] @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 "datumHash" ('[] @Symbol)))
        s)
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         (BoundTerms
            (PFields (PAsData PTxOut))
            (Bindings
               (PFields (PAsData PTxOut))
               ((':) @Symbol "datumHash" ('[] @Symbol)))
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PAsData PTxOut))
          (Bindings
             (PFields (PAsData PTxOut))
             ((':) @Symbol "datumHash" ('[] @Symbol)))
          s)
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':) @Symbol "datumHash" ('[] @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 @'["datumHash"] (Term s (PAsData PTxOut)
 -> (HRec
       (BoundTerms
          (PFields (PAsData PTxOut))
          (Bindings
             (PFields (PAsData PTxOut))
             ((':) @Symbol "datumHash" ('[] @Symbol)))
          s)
     -> Term s POpaque)
 -> Term s POpaque)
-> Term s (PAsData PTxOut)
-> (HRec
      (BoundTerms
         (PFields (PAsData PTxOut))
         (Bindings
            (PFields (PAsData PTxOut))
            ((':) @Symbol "datumHash" ('[] @Symbol)))
         s)
    -> Term s POpaque)
-> Term s POpaque
forall a b. (a -> b) -> a -> b
$
                Term
  s (PString @S :--> (PMaybe (PAsData PTxOut) :--> PAsData PTxOut))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust Term
  s (PString @S :--> (PMaybe (PAsData PTxOut) :--> PAsData PTxOut))
-> Term s (PString @S)
-> Term s (PMaybe (PAsData PTxOut) :--> PAsData PTxOut)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"Proposal output not found"
                  #$ pfind
                    # plam
                      ( \txOut -> unTermCont $ do
                          txOutF <- tcont $ pletFields @'["address", "value"] txOut
                          pure $
                            psymbolValueOf # ppstSymbol # txOutF.value #== 1
                              #&& txOutF.address #== pdata pproposalValidatorAddress
                      )
                    # pfromData txInfoF.outputs

          Term s PProposalDatum
proposalInputDatum <-
            Term s PProposalDatum
-> TermCont @POpaque s (Term s PProposalDatum)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PProposalDatum
 -> TermCont @POpaque s (Term s PProposalDatum))
-> Term s PProposalDatum
-> TermCont @POpaque s (Term s PProposalDatum)
forall a b. (a -> b) -> a -> b
$
              forall (datum :: PType) (s :: S).
(PIsData datum, PTryFrom PData (PAsData datum)) =>
Term
  s
  (PMaybeData PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> datum))
mustFindDatum' @PProposalDatum
                # proposalInputF.datumHash
                # txInfoF.datums
          Term s PProposalDatum
proposalOutputDatum <-
            Term s PProposalDatum
-> TermCont @POpaque s (Term s PProposalDatum)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PProposalDatum
 -> TermCont @POpaque s (Term s PProposalDatum))
-> Term s PProposalDatum
-> TermCont @POpaque s (Term s PProposalDatum)
forall a b. (a -> b) -> a -> b
$
              forall (datum :: PType) (s :: S).
(PIsData datum, PTryFrom PData (PAsData datum)) =>
Term
  s
  (PMaybeData PDatumHash
   :--> (PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> datum))
mustFindDatum' @PProposalDatum
                # proposalOutputF.datumHash
                # txInfoF.datums

          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)
"Proposal datum must be valid" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PProposalDatum :--> PBool)
forall (s :: S). Term s (PProposalDatum :--> PBool)
proposalDatumValid' Term s (PProposalDatum :--> PBool)
-> Term s PProposalDatum -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PProposalDatum
proposalInputDatum
              #&& proposalDatumValid' # proposalOutputDatum

          HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF <-
            ((HRec
    ((':)
       @(Symbol, Type)
       '("proposalId", Term s (PAsData PProposalId))
       ((':)
          @(Symbol, Type)
          '("effects",
            Term
              s
              (PAsData
                 (PMap
                    'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
          ((':)
             @(Symbol, Type)
             '("status", Term s (PAsData PProposalStatus))
             ((':)
                @(Symbol, Type)
                '("cosigners",
                  Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                ((':)
                   @(Symbol, Type)
                   '("thresholds", Term s (PAsData PProposalThresholds))
                   ((':)
                      @(Symbol, Type)
                      '("votes", Term s (PAsData PProposalVotes))
                      ((':)
                         @(Symbol, Type)
                         '("timingConfig", Term s (PAsData PProposalTimingConfig))
                         ((':)
                            @(Symbol, Type)
                            '("startingTime", Term s (PAsData PProposalStartingTime))
                            ('[] @(Symbol, Type))))))))))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("proposalId", Term s (PAsData PProposalId))
           ((':)
              @(Symbol, Type)
              '("effects",
                Term
                  s
                  (PAsData
                     (PMap
                        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
              ((':)
                 @(Symbol, Type)
                 '("status", Term s (PAsData PProposalStatus))
                 ((':)
                    @(Symbol, Type)
                    '("cosigners",
                      Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                    ((':)
                       @(Symbol, Type)
                       '("thresholds", Term s (PAsData PProposalThresholds))
                       ((':)
                          @(Symbol, Type)
                          '("votes", Term s (PAsData PProposalVotes))
                          ((':)
                             @(Symbol, Type)
                             '("timingConfig", Term s (PAsData PProposalTimingConfig))
                             ((':)
                                @(Symbol, Type)
                                '("startingTime", Term s (PAsData PProposalStartingTime))
                                ('[] @(Symbol, Type)))))))))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("proposalId", Term s (PAsData PProposalId))
        ((':)
           @(Symbol, Type)
           '("effects",
             Term
               s
               (PAsData
                  (PMap
                     'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
           ((':)
              @(Symbol, Type)
              '("status", Term s (PAsData PProposalStatus))
              ((':)
                 @(Symbol, Type)
                 '("cosigners",
                   Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                 ((':)
                    @(Symbol, Type)
                    '("thresholds", Term s (PAsData PProposalThresholds))
                    ((':)
                       @(Symbol, Type)
                       '("votes", Term s (PAsData PProposalVotes))
                       ((':)
                          @(Symbol, Type)
                          '("timingConfig", Term s (PAsData PProposalTimingConfig))
                          ((':)
                             @(Symbol, Type)
                             '("startingTime", Term s (PAsData PProposalStartingTime))
                             ('[] @(Symbol, Type))))))))))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("proposalId", Term s (PAsData PProposalId))
            ((':)
               @(Symbol, Type)
               '("effects",
                 Term
                   s
                   (PAsData
                      (PMap
                         'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
               ((':)
                  @(Symbol, Type)
                  '("status", Term s (PAsData PProposalStatus))
                  ((':)
                     @(Symbol, Type)
                     '("cosigners",
                       Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                     ((':)
                        @(Symbol, Type)
                        '("thresholds", Term s (PAsData PProposalThresholds))
                        ((':)
                           @(Symbol, Type)
                           '("votes", Term s (PAsData PProposalVotes))
                           ((':)
                              @(Symbol, Type)
                              '("timingConfig", Term s (PAsData PProposalTimingConfig))
                              ((':)
                                 @(Symbol, Type)
                                 '("startingTime", Term s (PAsData PProposalStartingTime))
                                 ('[] @(Symbol, Type))))))))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("proposalId", Term s (PAsData PProposalId))
          ((':)
             @(Symbol, Type)
             '("effects",
               Term
                 s
                 (PAsData
                    (PMap
                       'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
             ((':)
                @(Symbol, Type)
                '("status", Term s (PAsData PProposalStatus))
                ((':)
                   @(Symbol, Type)
                   '("cosigners",
                     Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                   ((':)
                      @(Symbol, Type)
                      '("thresholds", Term s (PAsData PProposalThresholds))
                      ((':)
                         @(Symbol, Type)
                         '("votes", Term s (PAsData PProposalVotes))
                         ((':)
                            @(Symbol, Type)
                            '("timingConfig", Term s (PAsData PProposalTimingConfig))
                            ((':)
                               @(Symbol, Type)
                               '("startingTime", Term s (PAsData PProposalStartingTime))
                               ('[] @(Symbol, Type))))))))))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("proposalId", Term s (PAsData PProposalId))
           ((':)
              @(Symbol, Type)
              '("effects",
                Term
                  s
                  (PAsData
                     (PMap
                        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
              ((':)
                 @(Symbol, Type)
                 '("status", Term s (PAsData PProposalStatus))
                 ((':)
                    @(Symbol, Type)
                    '("cosigners",
                      Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                    ((':)
                       @(Symbol, Type)
                       '("thresholds", Term s (PAsData PProposalThresholds))
                       ((':)
                          @(Symbol, Type)
                          '("votes", Term s (PAsData PProposalVotes))
                          ((':)
                             @(Symbol, Type)
                             '("timingConfig", Term s (PAsData PProposalTimingConfig))
                             ((':)
                                @(Symbol, Type)
                                '("startingTime", Term s (PAsData PProposalStartingTime))
                                ('[] @(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 @'["proposalId", "effects", "status", "cosigners", "thresholds", "votes", "timingConfig", "startingTime"]
                Term s PProposalDatum
proposalInputDatum

          -- Check that the proposal state is advanced so that a proposal cannot be executed twice.

          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)
"Proposal must be in locked(executable) state in order to execute effects" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.status Term s (PAsData PProposalStatus)
-> Term s (PAsData PProposalStatus) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== ProposalStatus -> Term s (PAsData PProposalStatus)
forall (p :: PType) h (s :: S).
(ToData h, (PLifted p :: Type) ~ (h :: Type),
 (PConstanted h :: PType) ~ (p :: PType)) =>
h -> Term s (PAsData p)
pconstantData ProposalStatus
Locked

          let expectedOutputProposalDatum :: Term s PProposalDatum
expectedOutputProposalDatum =
                (forall (s' :: S).
 Term
   s'
   (PDataRecord
      ((':)
         @PLabeledType
         ("proposalId" ':= PProposalId)
         ((':)
            @PLabeledType
            ("effects"
             ':= PMap
                   'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
            ((':)
               @PLabeledType
               ("status" ':= PProposalStatus)
               ((':)
                  @PLabeledType
                  ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                  ((':)
                     @PLabeledType
                     ("thresholds" ':= PProposalThresholds)
                     ((':)
                        @PLabeledType
                        ("votes" ':= PProposalVotes)
                        ((':)
                           @PLabeledType
                           ("timingConfig" ':= PProposalTimingConfig)
                           ((':)
                              @PLabeledType
                              ("startingTime" ':= PProposalStartingTime)
                              ('[] @PLabeledType))))))))))
 -> PProposalDatum s')
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("proposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("effects"
            ':= PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
           ((':)
              @PLabeledType
              ("status" ':= PProposalStatus)
              ((':)
                 @PLabeledType
                 ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                 ((':)
                    @PLabeledType
                    ("thresholds" ':= PProposalThresholds)
                    ((':)
                       @PLabeledType
                       ("votes" ':= PProposalVotes)
                       ((':)
                          @PLabeledType
                          ("timingConfig" ':= PProposalTimingConfig)
                          ((':)
                             @PLabeledType
                             ("startingTime" ':= PProposalStartingTime)
                             ('[] @PLabeledType)))))))))
-> Term s PProposalDatum
forall (r :: [PLabeledType]) (s :: S) (pt :: PType).
PlutusType pt =>
(forall (s' :: S). Term s' (PDataRecord r) -> pt s')
-> RecordMorphism s ('[] @PLabeledType) r -> Term s pt
mkRecordConstr
                  forall (s' :: S).
Term
  s'
  (PDataRecord
     ((':)
        @PLabeledType
        ("proposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("effects"
            ':= PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
           ((':)
              @PLabeledType
              ("status" ':= PProposalStatus)
              ((':)
                 @PLabeledType
                 ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                 ((':)
                    @PLabeledType
                    ("thresholds" ':= PProposalThresholds)
                    ((':)
                       @PLabeledType
                       ("votes" ':= PProposalVotes)
                       ((':)
                          @PLabeledType
                          ("timingConfig" ':= PProposalTimingConfig)
                          ((':)
                             @PLabeledType
                             ("startingTime" ':= PProposalStartingTime)
                             ('[] @PLabeledType))))))))))
-> PProposalDatum s'
PProposalDatum
                  ( FieldName "proposalId"
#proposalId FieldName "proposalId"
-> Term s (PAsData PProposalId)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType))))))))
     ((':)
        @PLabeledType
        ("proposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("effects"
            ':= PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
           ((':)
              @PLabeledType
              ("status" ':= PProposalStatus)
              ((':)
                 @PLabeledType
                 ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                 ((':)
                    @PLabeledType
                    ("thresholds" ':= PProposalThresholds)
                    ((':)
                       @PLabeledType
                       ("votes" ':= PProposalVotes)
                       ((':)
                          @PLabeledType
                          ("timingConfig" ':= PProposalTimingConfig)
                          ((':)
                             @PLabeledType
                             ("startingTime" ':= PProposalStartingTime)
                             ('[] @PLabeledType)))))))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.proposalId
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("effects"
      ':= PMap
            'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType))))))))
  ((':)
     @PLabeledType
     ("proposalId" ':= PProposalId)
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType)))))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType))))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("proposalId" ':= PProposalId)
        ((':)
           @PLabeledType
           ("effects"
            ':= PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
           ((':)
              @PLabeledType
              ("status" ':= PProposalStatus)
              ((':)
                 @PLabeledType
                 ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
                 ((':)
                    @PLabeledType
                    ("thresholds" ':= PProposalThresholds)
                    ((':)
                       @PLabeledType
                       ("votes" ':= PProposalVotes)
                       ((':)
                          @PLabeledType
                          ("timingConfig" ':= PProposalTimingConfig)
                          ((':)
                             @PLabeledType
                             ("startingTime" ':= PProposalStartingTime)
                             ('[] @PLabeledType)))))))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "effects"
#effects FieldName "effects"
-> Term
     s
     (PAsData
        (PMap
           'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)))
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType)))))))
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType))))))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.effects
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("status" ':= PProposalStatus)
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType)))))))
  ((':)
     @PLabeledType
     ("effects"
      ':= PMap
            'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType))))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType)))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("effects"
         ':= PMap
               'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
        ((':)
           @PLabeledType
           ("status" ':= PProposalStatus)
           ((':)
              @PLabeledType
              ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
              ((':)
                 @PLabeledType
                 ("thresholds" ':= PProposalThresholds)
                 ((':)
                    @PLabeledType
                    ("votes" ':= PProposalVotes)
                    ((':)
                       @PLabeledType
                       ("timingConfig" ':= PProposalTimingConfig)
                       ((':)
                          @PLabeledType
                          ("startingTime" ':= PProposalStartingTime)
                          ('[] @PLabeledType))))))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "status"
#status FieldName "status"
-> Term s (PAsData PProposalStatus)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType))))))
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType)))))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= Term s PProposalStatus -> Term s (PAsData PProposalStatus)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata (PProposalStatus s -> Term s PProposalStatus
forall (a :: PType) (s :: S). PCon a => a s -> Term s a
pcon (PProposalStatus s -> Term s PProposalStatus)
-> PProposalStatus s -> Term s PProposalStatus
forall a b. (a -> b) -> a -> b
$ Term s (PDataRecord ('[] @PLabeledType)) -> PProposalStatus s
forall (s :: S).
Term s (PDataRecord ('[] @PLabeledType)) -> PProposalStatus s
PFinished Term s (PDataRecord ('[] @PLabeledType))
forall (s :: S). Term s (PDataRecord ('[] @PLabeledType))
pdnil)
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType))))))
  ((':)
     @PLabeledType
     ("status" ':= PProposalStatus)
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType)))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("status" ':= PProposalStatus)
        ((':)
           @PLabeledType
           ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
           ((':)
              @PLabeledType
              ("thresholds" ':= PProposalThresholds)
              ((':)
                 @PLabeledType
                 ("votes" ':= PProposalVotes)
                 ((':)
                    @PLabeledType
                    ("timingConfig" ':= PProposalTimingConfig)
                    ((':)
                       @PLabeledType
                       ("startingTime" ':= PProposalStartingTime)
                       ('[] @PLabeledType)))))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "cosigners"
#cosigners FieldName "cosigners"
-> Term s (PAsData (PBuiltinList (PAsData PPubKeyHash)))
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType)))))
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType))))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.cosigners
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("thresholds" ':= PProposalThresholds)
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType)))))
  ((':)
     @PLabeledType
     ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType))))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType)))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("cosigners" ':= PBuiltinList (PAsData PPubKeyHash))
        ((':)
           @PLabeledType
           ("thresholds" ':= PProposalThresholds)
           ((':)
              @PLabeledType
              ("votes" ':= PProposalVotes)
              ((':)
                 @PLabeledType
                 ("timingConfig" ':= PProposalTimingConfig)
                 ((':)
                    @PLabeledType
                    ("startingTime" ':= PProposalStartingTime)
                    ('[] @PLabeledType))))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "thresholds"
#thresholds FieldName "thresholds"
-> Term s (PAsData PProposalThresholds)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType))))
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType)))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.thresholds
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("votes" ':= PProposalVotes)
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType))))
  ((':)
     @PLabeledType
     ("thresholds" ':= PProposalThresholds)
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType)))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("thresholds" ':= PProposalThresholds)
        ((':)
           @PLabeledType
           ("votes" ':= PProposalVotes)
           ((':)
              @PLabeledType
              ("timingConfig" ':= PProposalTimingConfig)
              ((':)
                 @PLabeledType
                 ("startingTime" ':= PProposalStartingTime)
                 ('[] @PLabeledType)))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "votes"
#votes FieldName "votes"
-> Term s (PAsData PProposalVotes)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType)))
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType))))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.votes
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("timingConfig" ':= PProposalTimingConfig)
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType)))
  ((':)
     @PLabeledType
     ("votes" ':= PProposalVotes)
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType))))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("votes" ':= PProposalVotes)
        ((':)
           @PLabeledType
           ("timingConfig" ':= PProposalTimingConfig)
           ((':)
              @PLabeledType
              ("startingTime" ':= PProposalStartingTime)
              ('[] @PLabeledType))))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "timingConfig"
#timingConfig FieldName "timingConfig"
-> Term s (PAsData PProposalTimingConfig)
-> RecordMorphism
     s
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType))
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType)))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.timingConfig
                      RecordMorphism
  s
  ((':)
     @PLabeledType
     ("startingTime" ':= PProposalStartingTime)
     ('[] @PLabeledType))
  ((':)
     @PLabeledType
     ("timingConfig" ':= PProposalTimingConfig)
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType)))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType))
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("timingConfig" ':= PProposalTimingConfig)
        ((':)
           @PLabeledType
           ("startingTime" ':= PProposalStartingTime)
           ('[] @PLabeledType)))
forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
.& FieldName "startingTime"
#startingTime FieldName "startingTime"
-> Term s (PAsData PProposalStartingTime)
-> RecordMorphism
     s
     ('[] @PLabeledType)
     ((':)
        @PLabeledType
        ("startingTime" ':= PProposalStartingTime)
        ('[] @PLabeledType))
forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a)
-> RecordMorphism s as ((':) @PLabeledType (sym ':= a) as)
.= HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.startingTime
                  )

          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)
"Unexpected output proposal datum" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s PProposalDatum -> Term s (PAsData PProposalDatum)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PProposalDatum
proposalOutputDatum Term s (PAsData PProposalDatum)
-> Term s (PAsData PProposalDatum) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PProposalDatum -> Term s (PAsData PProposalDatum)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PProposalDatum
expectedOutputProposalDatum

          -- TODO: anything else to check here?

          -- Find the highest votes and the corresponding tag.
          let quorum :: Term
  s
  (PInner
     (PInner
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
              (PFields (PAsData PProposalThresholds))))
        (Any @PType))
     (Any @PType))
quorum = Term
  s
  (PInner
     (PUnLabel
        (IndexList
           @PLabeledType
           (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
           (PFields (PAsData PProposalThresholds))))
     (Any @PType))
-> forall (b :: PType).
   Term
     s
     (PInner
        (PInner
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
                 (PFields (PAsData PProposalThresholds))))
           (Any @PType))
        b)
forall (s :: S) (a :: PType).
Term s a -> forall (b :: PType). Term s (PInner a b)
pto (Term
   s
   (PInner
      (PUnLabel
         (IndexList
            @PLabeledType
            (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
            (PFields (PAsData PProposalThresholds))))
      (Any @PType))
 -> forall (b :: PType).
    Term
      s
      (PInner
         (PInner
            (PUnLabel
               (IndexList
                  @PLabeledType
                  (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
                  (PFields (PAsData PProposalThresholds))))
            (Any @PType))
         b))
-> Term
     s
     (PInner
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
              (PFields (PAsData PProposalThresholds))))
        (Any @PType))
-> forall (b :: PType).
   Term
     s
     (PInner
        (PInner
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
                 (PFields (PAsData PProposalThresholds))))
           (Any @PType))
        b)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PUnLabel
     (IndexList
        @PLabeledType
        (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
        (PFields (PAsData PProposalThresholds))))
-> forall (b :: PType).
   Term
     s
     (PInner
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
              (PFields (PAsData PProposalThresholds))))
        b)
forall (s :: S) (a :: PType).
Term s a -> forall (b :: PType). Term s (PInner a b)
pto (Term
   s
   (PUnLabel
      (IndexList
         @PLabeledType
         (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
         (PFields (PAsData PProposalThresholds))))
 -> forall (b :: PType).
    Term
      s
      (PInner
         (PUnLabel
            (IndexList
               @PLabeledType
               (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
               (PFields (PAsData PProposalThresholds))))
         b))
-> Term
     s
     (PUnLabel
        (IndexList
           @PLabeledType
           (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
           (PFields (PAsData PProposalThresholds))))
-> forall (b :: PType).
   Term
     s
     (PInner
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
              (PFields (PAsData PProposalThresholds))))
        b)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PAsData
     (PUnLabel
        (IndexList
           @PLabeledType
           (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
           (PFields (PAsData PProposalThresholds)))))
-> Term
     s
     (PUnLabel
        (IndexList
           @PLabeledType
           (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
           (PFields (PAsData PProposalThresholds))))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term
   s
   (PAsData
      (PUnLabel
         (IndexList
            @PLabeledType
            (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
            (PFields (PAsData PProposalThresholds)))))
 -> Term
      s
      (PUnLabel
         (IndexList
            @PLabeledType
            (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
            (PFields (PAsData PProposalThresholds)))))
-> Term
     s
     (PAsData
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
              (PFields (PAsData PProposalThresholds)))))
-> Term
     s
     (PUnLabel
        (IndexList
           @PLabeledType
           (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
           (PFields (PAsData PProposalThresholds))))
forall a b. (a -> b) -> a -> b
$ forall (name :: Symbol) (p :: PType) (s :: S) (a :: PType)
       (as :: [PLabeledType]) (n :: Nat) (b :: PType).
(PDataFields p,
 (as :: [PLabeledType]) ~ (PFields p :: [PLabeledType]),
 (n :: Nat) ~ (PLabelIndex name as :: Nat), KnownNat n,
 (a :: PType) ~ (PUnLabel (IndexList @PLabeledType n as) :: PType),
 PFromDataable a b) =>
Term s (p :--> b)
pfield @"execute" Term
  s
  (PAsData PProposalThresholds
   :--> PAsData
          (PUnLabel
             (IndexList
                @PLabeledType
                (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
                (PFields (PAsData PProposalThresholds)))))
-> Term s (PAsData PProposalThresholds)
-> Term
     s
     (PAsData
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
              (PFields (PAsData PProposalThresholds)))))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.thresholds
              neutralOption :: Term s PResultTag
neutralOption = Term
  s
  (PMap
     'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)
   :--> PResultTag)
forall (s :: S).
Term
  s
  (PMap
     'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)
   :--> PResultTag)
pneutralOption Term
  s
  (PMap
     'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)
   :--> PResultTag)
-> Term
     s
     (PMap
        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
-> Term s PResultTag
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.effects
              finalResultTag :: Term s PResultTag
finalResultTag = Term
  s
  (PProposalVotes
   :--> (PInteger @S :--> (PResultTag :--> PResultTag)))
forall (s :: S).
Term
  s
  (PProposalVotes
   :--> (PInteger @S :--> (PResultTag :--> PResultTag)))
pwinner Term
  s
  (PProposalVotes
   :--> (PInteger @S :--> (PResultTag :--> PResultTag)))
-> Term s PProposalVotes
-> Term s (PInteger @S :--> (PResultTag :--> PResultTag))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.votes Term s (PInteger @S :--> (PResultTag :--> PResultTag))
-> Term s (PInteger @S) -> Term s (PResultTag :--> PResultTag)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PInteger @S)
Term
  s
  (PInner
     (PInner
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "execute" (PFields (PAsData PProposalThresholds)))
              (PFields (PAsData PProposalThresholds))))
        (Any @PType))
     (Any @PType))
quorum Term s (PResultTag :--> PResultTag)
-> Term s PResultTag -> Term s PResultTag
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PResultTag
neutralOption

          -- The effects of the winner outcome.
          Term s (PMap 'Unsorted PValidatorHash PDatumHash)
effectGroup <- Term s (PMap 'Unsorted PValidatorHash PDatumHash)
-> TermCont
     @POpaque s (Term s (PMap 'Unsorted PValidatorHash PDatumHash))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PMap 'Unsorted PValidatorHash PDatumHash)
 -> TermCont
      @POpaque s (Term s (PMap 'Unsorted PValidatorHash PDatumHash)))
-> Term s (PMap 'Unsorted PValidatorHash PDatumHash)
-> TermCont
     @POpaque s (Term s (PMap 'Unsorted PValidatorHash PDatumHash))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PResultTag
   :--> (PMap
           'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)
         :--> PMap 'Unsorted PValidatorHash PDatumHash))
forall (k :: PType) (v :: PType) (keys :: KeyGuarantees) (s :: S).
(PIsData v, PIsData k, PEq k) =>
Term s (k :--> (PMap keys k v :--> v))
plookup' Term
  s
  (PResultTag
   :--> (PMap
           'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)
         :--> PMap 'Unsorted PValidatorHash PDatumHash))
-> Term s PResultTag
-> Term
     s
     (PMap
        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)
      :--> PMap 'Unsorted PValidatorHash PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PResultTag
finalResultTag Term
  s
  (PMap
     'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash)
   :--> PMap 'Unsorted PValidatorHash PDatumHash)
-> Term
     s
     (PMap
        'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))
-> Term s (PMap 'Unsorted PValidatorHash PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ HRec
  ((':)
     @(Symbol, Type)
     '("proposalId", Term s (PAsData PProposalId))
     ((':)
        @(Symbol, Type)
        '("effects",
          Term
            s
            (PAsData
               (PMap
                  'Unsorted PResultTag (PMap 'Unsorted PValidatorHash PDatumHash))))
        ((':)
           @(Symbol, Type)
           '("status", Term s (PAsData PProposalStatus))
           ((':)
              @(Symbol, Type)
              '("cosigners",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("thresholds", Term s (PAsData PProposalThresholds))
                 ((':)
                    @(Symbol, Type)
                    '("votes", Term s (PAsData PProposalVotes))
                    ((':)
                       @(Symbol, Type)
                       '("timingConfig", Term s (PAsData PProposalTimingConfig))
                       ((':)
                          @(Symbol, Type)
                          '("startingTime", Term s (PAsData PProposalStartingTime))
                          ('[] @(Symbol, Type))))))))))
proposalInputDatumF.effects

          Term s (PInteger @S)
gatCount <- Term s (PInteger @S) -> TermCont @POpaque s (Term s (PInteger @S))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PInteger @S)
 -> TermCont @POpaque s (Term s (PInteger @S)))
-> Term s (PInteger @S)
-> TermCont @POpaque s (Term s (PInteger @S))
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PValidatorHash) (PAsData PDatumHash))
   :--> PInteger @S)
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> PInteger @S)
plength Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PValidatorHash) (PAsData PDatumHash))
   :--> PInteger @S)
-> Term
     s
     (PBuiltinList
        (PBuiltinPair (PAsData PValidatorHash) (PAsData PDatumHash)))
-> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term
  s
  (PBuiltinList
     (PBuiltinPair (PAsData PValidatorHash) (PAsData PDatumHash)))
-> forall (b :: PType).
   Term
     s
     (PInner
        (PBuiltinList
           (PBuiltinPair (PAsData PValidatorHash) (PAsData PDatumHash)))
        b)
forall (s :: S) (a :: PType).
Term s a -> forall (b :: PType). Term s (PInner a b)
pto (Term
   s
   (PBuiltinList
      (PBuiltinPair (PAsData PValidatorHash) (PAsData PDatumHash)))
 -> forall (b :: PType).
    Term
      s
      (PInner
         (PBuiltinList
            (PBuiltinPair (PAsData PValidatorHash) (PAsData PDatumHash)))
         b))
-> Term
     s
     (PBuiltinList
        (PBuiltinPair (PAsData PValidatorHash) (PAsData PDatumHash)))
-> forall (b :: PType).
   Term
     s
     (PInner
        (PBuiltinList
           (PBuiltinPair (PAsData PValidatorHash) (PAsData PDatumHash)))
        b)
forall a b. (a -> b) -> a -> b
$ Term s (PMap 'Unsorted PValidatorHash PDatumHash)
-> forall (b :: PType).
   Term s (PInner (PMap 'Unsorted PValidatorHash PDatumHash) b)
forall (s :: S) (a :: PType).
Term s a -> forall (b :: PType). Term s (PInner a b)
pto Term s (PMap 'Unsorted PValidatorHash PDatumHash)
effectGroup

          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)
"Required amount of GATs should be minted" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term
  s
  (PCurrencySymbol
   :--> (PValue 'Sorted 'NoGuarantees :--> PInteger @S))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term
  s (PCurrencySymbol :--> (PValue keys amounts :--> PInteger @S))
psymbolValueOf Term
  s
  (PCurrencySymbol
   :--> (PValue 'Sorted 'NoGuarantees :--> PInteger @S))
-> Term s PCurrencySymbol
-> Term s (PValue 'Sorted 'NoGuarantees :--> PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
forall (s :: S). Term s PCurrencySymbol
patSymbol Term s (PValue 'Sorted 'NoGuarantees :--> PInteger @S)
-> Term s (PValue 'Sorted 'NoGuarantees) -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol
                    "datums"
                    ((':)
                       @Symbol
                       "signatories"
                       ((':) @Symbol "validRange" ('[] @Symbol))))))))
     s)
txInfoF.mint Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PInteger @S)
gatCount

          -- Ensure that every GAT goes to one of the effects in the winner effect group.
          Term s (PBuiltinList (PAsData PTxOut))
outputsWithGAT <-
            Term s (PBuiltinList (PAsData PTxOut))
-> TermCont @POpaque s (Term s (PBuiltinList (PAsData PTxOut)))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PBuiltinList (PAsData PTxOut))
 -> TermCont @POpaque s (Term s (PBuiltinList (PAsData PTxOut))))
-> Term s (PBuiltinList (PAsData PTxOut))
-> TermCont @POpaque s (Term s (PBuiltinList (PAsData PTxOut)))
forall a b. (a -> b) -> a -> b
$
              Term
  s
  ((PAsData PTxOut :--> PBool)
   :--> (PBuiltinList (PAsData PTxOut)
         :--> PBuiltinList (PAsData PTxOut)))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> list a))
pfilter
                # phoistAcyclic
                  ( plam
                      ( \((pfield @"value" #) -> value) ->
                          0 #< psymbolValueOf # patSymbol # value
                      )
                  )
                # pfromData txInfoF.outputs

          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)
"Output GATs is more than minted GATs" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PBuiltinList (PAsData PTxOut) :--> PInteger @S)
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s (list a :--> PInteger @S)
plength Term s (PBuiltinList (PAsData PTxOut) :--> PInteger @S)
-> Term s (PBuiltinList (PAsData PTxOut)) -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PBuiltinList (PAsData PTxOut))
outputsWithGAT Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PInteger @S)
gatCount

          let gatOutputValidator' :: Term s (PMap _ PValidatorHash PDatumHash :--> PAsData PTxOut :--> PBool)
              gatOutputValidator' :: Term
  s
  (PMap w PValidatorHash PDatumHash :--> (PAsData PTxOut :--> PBool))
gatOutputValidator' =
                ClosedTerm
  (PMap w PValidatorHash PDatumHash :--> (PAsData PTxOut :--> PBool))
-> Term
     s
     (PMap w PValidatorHash PDatumHash :--> (PAsData PTxOut :--> PBool))
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm
   (PMap w PValidatorHash PDatumHash :--> (PAsData PTxOut :--> PBool))
 -> Term
      s
      (PMap w PValidatorHash PDatumHash
       :--> (PAsData PTxOut :--> PBool)))
-> ClosedTerm
     (PMap w PValidatorHash PDatumHash :--> (PAsData PTxOut :--> PBool))
-> Term
     s
     (PMap w PValidatorHash PDatumHash :--> (PAsData PTxOut :--> PBool))
forall a b. (a -> b) -> a -> b
$
                  (Term s (PMap w PValidatorHash PDatumHash)
 -> Term s (PAsData PTxOut) -> Term s PBool)
-> Term
     s
     (PMap w PValidatorHash PDatumHash :--> (PAsData PTxOut :--> PBool))
forall a (b :: PType) (s :: S) (c :: PType).
PLamN a b s =>
(Term s c -> a) -> Term s (c :--> b)
plam
                    ( \Term s (PMap w PValidatorHash PDatumHash)
effects (Term s (PAsData PTxOut) -> Term s PTxOut
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData -> Term s PTxOut
output') -> TermCont @PBool s (Term s PBool) -> Term s PBool
forall (a :: PType) (s :: S). TermCont @a s (Term s a) -> Term s a
unTermCont (TermCont @PBool s (Term s PBool) -> Term s PBool)
-> TermCont @PBool s (Term s PBool) -> Term s PBool
forall a b. (a -> b) -> a -> b
$ do
                        HRec
  ((':)
     @(Symbol, Type)
     '("address", Term s (PAsData PAddress))
     ((':)
        @(Symbol, Type)
        '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
        ('[] @(Symbol, Type))))
output <- ((HRec
    ((':)
       @(Symbol, Type)
       '("address", Term s (PAsData PAddress))
       ((':)
          @(Symbol, Type)
          '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
          ('[] @(Symbol, Type))))
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("address", Term s (PAsData PAddress))
           ((':)
              @(Symbol, Type)
              '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
              ('[] @(Symbol, Type)))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("address", Term s (PAsData PAddress))
        ((':)
           @(Symbol, Type)
           '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
           ('[] @(Symbol, Type))))
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("address", Term s (PAsData PAddress))
            ((':)
               @(Symbol, Type)
               '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
               ('[] @(Symbol, Type))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("address", Term s (PAsData PAddress))
          ((':)
             @(Symbol, Type)
             '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
             ('[] @(Symbol, Type))))
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("address", Term s (PAsData PAddress))
           ((':)
              @(Symbol, Type)
              '("datumHash", Term s (PAsData (PMaybeData PDatumHash)))
              ('[] @(Symbol, Type)))))
forall a b. (a -> b) -> a -> b
$ forall (fs :: [Symbol]) (a :: PType) (s :: S) (b :: PType)
       (ps :: [PLabeledType]) (bs :: [ToBind]).
(PDataFields a,
 (ps :: [PLabeledType]) ~ (PFields a :: [PLabeledType]),
 (bs :: [ToBind]) ~ (Bindings ps fs :: [ToBind]),
 BindFields ps bs) =>
Term s a -> (HRecOf a fs s -> Term s b) -> Term s b
pletFields @'["address", "datumHash"] (Term s PTxOut
 -> (HRecOf
       PTxOut
       ((':) @Symbol "address" ((':) @Symbol "datumHash" ('[] @Symbol)))
       s
     -> Term s PBool)
 -> Term s PBool)
-> Term s PTxOut
-> (HRecOf
      PTxOut
      ((':) @Symbol "address" ((':) @Symbol "datumHash" ('[] @Symbol)))
      s
    -> Term s PBool)
-> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s PTxOut
output'

                        let scriptHash :: Term s PValidatorHash
scriptHash =
                              Term
  s (PString @S :--> (PMaybe PValidatorHash :--> PValidatorHash))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust Term
  s (PString @S :--> (PMaybe PValidatorHash :--> PValidatorHash))
-> Term s (PString @S)
-> Term s (PMaybe PValidatorHash :--> PValidatorHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"GAT receiver is not a script"
                                #$ scriptHashFromAddress # output.address
                            datumHash :: Term s PDatumHash
datumHash =
                              Term s (PString @S :--> (PMaybeData PDatumHash :--> PDatumHash))
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PString @S :--> (PMaybeData a :--> a))
mustBePDJust Term s (PString @S :--> (PMaybeData PDatumHash :--> PDatumHash))
-> Term s (PString @S)
-> Term s (PMaybeData PDatumHash :--> PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"Output to effect should have datum"
                                #$ output.datumHash

                            expectedDatumHash :: Term s PDatumHash
expectedDatumHash =
                              Term s (PString @S :--> (PMaybe PDatumHash :--> PDatumHash))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust Term s (PString @S :--> (PMaybe PDatumHash :--> PDatumHash))
-> Term s (PString @S)
-> Term s (PMaybe PDatumHash :--> PDatumHash)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PString @S)
"Receiver is not in the effect list"
                                #$ plookup # scriptHash # effects

                        Term s PBool -> TermCont @PBool s (Term s PBool)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s PBool -> TermCont @PBool s (Term s PBool))
-> Term s PBool -> TermCont @PBool s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
                          (Term s PBool -> Term s PBool -> Term s PBool)
-> [Term s PBool] -> Term s PBool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldr1
                            Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
(#&&)
                            [ Term s (PString @S) -> Term s PBool -> Term s PBool
forall (s :: S).
Term s (PString @S) -> Term s PBool -> Term s PBool
ptraceIfFalse Term s (PString @S)
"GAT must be tagged by the effect hash" (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s (PCurrencySymbol :--> (PTxOut :--> PBool))
forall (s :: S). Term s (PCurrencySymbol :--> (PTxOut :--> PBool))
authorityTokensValidIn Term s (PCurrencySymbol :--> (PTxOut :--> PBool))
-> Term s PCurrencySymbol -> Term s (PTxOut :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PCurrencySymbol
forall (s :: S). Term s PCurrencySymbol
patSymbol Term s (PTxOut :--> PBool) -> Term s PTxOut -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PTxOut
output'
                            , Term s (PString @S) -> Term s PBool -> Term s PBool
forall (s :: S).
Term s (PString @S) -> Term s PBool -> Term s PBool
ptraceIfFalse Term s (PString @S)
"Unexpected datum" (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$ Term s PDatumHash
datumHash Term s PDatumHash -> Term s PDatumHash -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PDatumHash
expectedDatumHash
                            ]
                    )

              gatOutputValidator :: Term s (PAsData PTxOut :--> PBool)
gatOutputValidator = Term
  s
  (PMap 'Unsorted PValidatorHash PDatumHash
   :--> (PAsData PTxOut :--> PBool))
forall (s :: S) {w :: KeyGuarantees}.
Term
  s
  (PMap w PValidatorHash PDatumHash :--> (PAsData PTxOut :--> PBool))
gatOutputValidator' Term
  s
  (PMap 'Unsorted PValidatorHash PDatumHash
   :--> (PAsData PTxOut :--> PBool))
-> Term s (PMap 'Unsorted PValidatorHash PDatumHash)
-> Term s (PAsData PTxOut :--> PBool)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PMap 'Unsorted PValidatorHash PDatumHash)
effectGroup

          Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s POpaque -> TermCont @POpaque s (Term s POpaque))
-> Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$
            Term s PBool -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (Term s PBool -> Term s POpaque) -> Term s PBool -> Term s POpaque
forall a b. (a -> b) -> a -> b
$
              Term
  s
  ((PAsData PTxOut :--> (PBool :--> PBool))
   :--> (PBool :--> (PBuiltinList (PAsData PTxOut) :--> PBool)))
forall (list :: PType -> PType) (a :: PType) (s :: S) (b :: PType).
PIsListLike list a =>
Term s ((a :--> (b :--> b)) :--> (b :--> (list a :--> b)))
pfoldr
                # plam
                  ( \txOut r ->
                      let value = pfield @"value" # txOut
                          atValue = psymbolValueOf # patSymbol # value
                       in pif (atValue #== 0) r $
                            pif (atValue #== 1) (r #&& gatOutputValidator # txOut) $ pconstant False
                  )
                # pconstant True
                # pfromData txInfoF.outputs

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

        PMutateGovernor Term s (PDataRecord ('[] @PLabeledType))
_ -> 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
          -- Check that a GAT is burnt.
          Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Term s POpaque -> TermCont @POpaque s (Term s POpaque))
-> Term s POpaque -> TermCont @POpaque s (Term s POpaque)
forall a b. (a -> b) -> a -> b
$ Term s PBool -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (Term s PBool -> Term s POpaque) -> Term s PBool -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ Term s PCurrencySymbol
-> Term s (PAsData PTxInfo)
-> Term s (PValue 'Sorted 'NoGuarantees)
-> Term s PBool
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term s PCurrencySymbol
-> Term s (PAsData PTxInfo)
-> Term s (PValue keys amounts)
-> Term s PBool
singleAuthorityTokenBurned Term s PCurrencySymbol
forall (s :: S). Term s PCurrencySymbol
patSymbol HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctxF.txInfo HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol
                    "datums"
                    ((':)
                       @Symbol
                       "signatories"
                       ((':) @Symbol "validRange" ('[] @Symbol))))))))
     s)
txInfoF.mint
  where
    -- Get th amount of governance tokens in a value.
    pgtValueOf :: Term s (PValue _ _ :--> PDiscrete GTTag)
    pgtValueOf :: Term s (PValue w w :--> PDiscrete @Type GTTag)
pgtValueOf = ClosedTerm (PValue w w :--> PDiscrete @Type GTTag)
-> Term s (PValue w w :--> PDiscrete @Type GTTag)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic (ClosedTerm (PValue w w :--> PDiscrete @Type GTTag)
 -> Term s (PValue w w :--> PDiscrete @Type GTTag))
-> ClosedTerm (PValue w w :--> PDiscrete @Type GTTag)
-> Term s (PValue w w :--> PDiscrete @Type GTTag)
forall a b. (a -> b) -> a -> b
$ Tagged @Type GTTag AssetClass
-> Term s (PValue w w :--> PDiscrete @Type GTTag)
forall k (tag :: k) (keys :: KeyGuarantees)
       (amounts :: AmountGuarantees) (s :: S).
Tagged @k tag AssetClass
-> Term s (PValue keys amounts :--> PDiscrete @k tag)
pvalueDiscrete' Governor
gov.gtClassRef

    -- The currency symbol of authority token.
    patSymbol :: Term s PCurrencySymbol
    patSymbol :: forall (s :: S). Term s PCurrencySymbol
patSymbol = (forall (s :: S). Term s PCurrencySymbol) -> Term s PCurrencySymbol
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s PCurrencySymbol)
 -> Term s PCurrencySymbol)
-> (forall (s :: S). Term s PCurrencySymbol)
-> Term s PCurrencySymbol
forall a b. (a -> b) -> a -> b
$ PLifted PCurrencySymbol -> Term s PCurrencySymbol
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant (PLifted PCurrencySymbol -> Term s PCurrencySymbol)
-> PLifted PCurrencySymbol -> Term s PCurrencySymbol
forall a b. (a -> b) -> a -> b
$ Governor -> CurrencySymbol
authorityTokenSymbolFromGovernor Governor
gov

    -- The currency symbol of the proposal state token.
    ppstSymbol :: Term s PCurrencySymbol
    ppstSymbol :: forall (s :: S). Term s PCurrencySymbol
ppstSymbol =
      let AssetClass (CurrencySymbol
sym, TokenName
_) = Governor -> AssetClass
proposalSTAssetClassFromGovernor Governor
gov
       in (forall (s :: S). Term s PCurrencySymbol) -> Term s PCurrencySymbol
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s PCurrencySymbol)
 -> Term s PCurrencySymbol)
-> (forall (s :: S). Term s PCurrencySymbol)
-> Term s PCurrencySymbol
forall a b. (a -> b) -> a -> b
$ PLifted PCurrencySymbol -> Term s PCurrencySymbol
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PCurrencySymbol
CurrencySymbol
sym

    -- Is a proposal state datum valid?
    proposalDatumValid' :: Term s (PProposalDatum :--> PBool)
    proposalDatumValid' :: forall (s :: S). Term s (PProposalDatum :--> PBool)
proposalDatumValid' =
      let params :: Proposal
params = Governor -> Proposal
proposalFromGovernor Governor
gov
       in (forall (s :: S). Term s (PProposalDatum :--> PBool))
-> Term s (PProposalDatum :--> PBool)
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s (PProposalDatum :--> PBool))
 -> Term s (PProposalDatum :--> PBool))
-> (forall (s :: S). Term s (PProposalDatum :--> PBool))
-> Term s (PProposalDatum :--> PBool)
forall a b. (a -> b) -> a -> b
$ Proposal -> Term s (PProposalDatum :--> PBool)
forall (s :: S). Proposal -> Term s (PProposalDatum :--> PBool)
proposalDatumValid Proposal
params

    -- The address of the proposal validator.
    pproposalValidatorAddress :: Term s PAddress
    pproposalValidatorAddress :: forall (s :: S). Term s PAddress
pproposalValidatorAddress =
      let vh :: ValidatorHash
vh = Governor -> ValidatorHash
proposalValidatorHashFromGovernor Governor
gov
       in (forall (s :: S). Term s PAddress) -> Term s PAddress
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s PAddress) -> Term s PAddress)
-> (forall (s :: S). Term s PAddress) -> Term s PAddress
forall a b. (a -> b) -> a -> b
$ PLifted PAddress -> Term s PAddress
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant (PLifted PAddress -> Term s PAddress)
-> PLifted PAddress -> Term s PAddress
forall a b. (a -> b) -> a -> b
$ ValidatorHash -> Address
validatorHashToAddress ValidatorHash
vh

    -- The address of the stake validator.
    pstakeValidatorAddress :: Term s PAddress
    pstakeValidatorAddress :: forall (s :: S). Term s PAddress
pstakeValidatorAddress =
      let vh :: ValidatorHash
vh = Governor -> ValidatorHash
stakeValidatorHashFromGovernor Governor
gov
       in (forall (s :: S). Term s PAddress) -> Term s PAddress
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s PAddress) -> Term s PAddress)
-> (forall (s :: S). Term s PAddress) -> Term s PAddress
forall a b. (a -> b) -> a -> b
$ PLifted PAddress -> Term s PAddress
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant (PLifted PAddress -> Term s PAddress)
-> PLifted PAddress -> Term s PAddress
forall a b. (a -> b) -> a -> b
$ ValidatorHash -> Address
validatorHashToAddress ValidatorHash
vh

    -- The currency symbol of the stake state token.
    psstSymbol :: Term s PCurrencySymbol
    psstSymbol :: forall (s :: S). Term s PCurrencySymbol
psstSymbol =
      let sym :: CurrencySymbol
sym = Governor -> CurrencySymbol
stakeSTSymbolFromGovernor Governor
gov
       in (forall (s :: S). Term s PCurrencySymbol) -> Term s PCurrencySymbol
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s PCurrencySymbol)
 -> Term s PCurrencySymbol)
-> (forall (s :: S). Term s PCurrencySymbol)
-> Term s PCurrencySymbol
forall a b. (a -> b) -> a -> b
$ PLifted PCurrencySymbol -> Term s PCurrencySymbol
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PCurrencySymbol
CurrencySymbol
sym

    -- The currency symbol of the governor state token.
    pgstSymbol :: Term s PCurrencySymbol
    pgstSymbol :: forall (s :: S). Term s PCurrencySymbol
pgstSymbol =
      let sym :: CurrencySymbol
sym = Governor -> CurrencySymbol
governorSTSymbolFromGovernor Governor
gov
       in (forall (s :: S). Term s PCurrencySymbol) -> Term s PCurrencySymbol
forall (a :: PType) (s :: S).
HasCallStack =>
ClosedTerm a -> Term s a
phoistAcyclic ((forall (s :: S). Term s PCurrencySymbol)
 -> Term s PCurrencySymbol)
-> (forall (s :: S). Term s PCurrencySymbol)
-> Term s PCurrencySymbol
forall a b. (a -> b) -> a -> b
$ PLifted PCurrencySymbol -> Term s PCurrencySymbol
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PCurrencySymbol
CurrencySymbol
sym

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

{- | Get the 'CurrencySymbol' of GST.

     @since 0.1.0
-}
governorSTSymbolFromGovernor :: Governor -> CurrencySymbol
governorSTSymbolFromGovernor :: Governor -> CurrencySymbol
governorSTSymbolFromGovernor Governor
gov = MintingPolicy -> CurrencySymbol
mintingPolicySymbol MintingPolicy
policy
  where
    policy :: MintingPolicy
    policy :: MintingPolicy
policy = ClosedTerm PMintingPolicy -> MintingPolicy
mkMintingPolicy (ClosedTerm PMintingPolicy -> MintingPolicy)
-> ClosedTerm PMintingPolicy -> MintingPolicy
forall a b. (a -> b) -> a -> b
$ Governor -> ClosedTerm PMintingPolicy
governorPolicy Governor
gov

{- | Get the 'AssetClass' of GST.

     @since 0.1.0
-}
governorSTAssetClassFromGovernor :: Governor -> AssetClass
governorSTAssetClassFromGovernor :: Governor -> AssetClass
governorSTAssetClassFromGovernor Governor
gov = (CurrencySymbol, TokenName) -> AssetClass
AssetClass (CurrencySymbol
symbol, TokenName
"")
  where
    symbol :: CurrencySymbol
    symbol :: CurrencySymbol
symbol = Governor -> CurrencySymbol
governorSTSymbolFromGovernor Governor
gov

{- | Get the 'CurrencySymbol' of the proposal state token.

     @since 0.1.0
-}
proposalSTSymbolFromGovernor :: Governor -> CurrencySymbol
proposalSTSymbolFromGovernor :: Governor -> CurrencySymbol
proposalSTSymbolFromGovernor Governor
gov = CurrencySymbol
symbol
  where
    gstAC :: AssetClass
gstAC = Governor -> AssetClass
governorSTAssetClassFromGovernor Governor
gov
    policy :: MintingPolicy
policy = ClosedTerm PMintingPolicy -> MintingPolicy
mkMintingPolicy (ClosedTerm PMintingPolicy -> MintingPolicy)
-> ClosedTerm PMintingPolicy -> MintingPolicy
forall a b. (a -> b) -> a -> b
$ AssetClass -> ClosedTerm PMintingPolicy
proposalPolicy AssetClass
gstAC
    symbol :: CurrencySymbol
symbol = MintingPolicy -> CurrencySymbol
mintingPolicySymbol MintingPolicy
policy

{- | Get the 'AssetClass' of the proposal state token.

     @since 0.1.0
-}
proposalSTAssetClassFromGovernor :: Governor -> AssetClass
proposalSTAssetClassFromGovernor :: Governor -> AssetClass
proposalSTAssetClassFromGovernor Governor
gov = (CurrencySymbol, TokenName) -> AssetClass
AssetClass (CurrencySymbol
symbol, TokenName
"")
  where
    symbol :: CurrencySymbol
symbol = Governor -> CurrencySymbol
proposalSTSymbolFromGovernor Governor
gov

{- | Get the 'CurrencySymbol' of the stake token/

     @since 0.1.0
-}
stakeSTSymbolFromGovernor :: Governor -> CurrencySymbol
stakeSTSymbolFromGovernor :: Governor -> CurrencySymbol
stakeSTSymbolFromGovernor Governor
gov = MintingPolicy -> CurrencySymbol
mintingPolicySymbol MintingPolicy
policy
  where
    policy :: MintingPolicy
policy = ClosedTerm PMintingPolicy -> MintingPolicy
mkMintingPolicy (ClosedTerm PMintingPolicy -> MintingPolicy)
-> ClosedTerm PMintingPolicy -> MintingPolicy
forall a b. (a -> b) -> a -> b
$ Tagged @Type GTTag AssetClass -> ClosedTerm PMintingPolicy
stakePolicy Governor
gov.gtClassRef

{- | Get the 'AssetClass' of the stake token.

   Note that the token is tagged with the hash of the stake validator.
   See 'Agora.Stake.Script.stakePolicy'.

    @since 0.1.0
-}
stakeSTAssetClassFromGovernor :: Governor -> AssetClass
stakeSTAssetClassFromGovernor :: Governor -> AssetClass
stakeSTAssetClassFromGovernor Governor
gov = (CurrencySymbol, TokenName) -> AssetClass
AssetClass (CurrencySymbol
symbol, TokenName
tokenName)
  where
    symbol :: CurrencySymbol
symbol = Governor -> CurrencySymbol
stakeSTSymbolFromGovernor Governor
gov

    -- Tag with the address where the token is being sent to.
    tokenName :: TokenName
tokenName = ValidatorHash -> TokenName
validatorHashToTokenName (ValidatorHash -> TokenName) -> ValidatorHash -> TokenName
forall a b. (a -> b) -> a -> b
$ Governor -> ValidatorHash
stakeValidatorHashFromGovernor Governor
gov

{- | Get the 'Stake' parameter, given the 'Governor' parameter.

     @since 0.1.0
-}
stakeFromGovernor :: Governor -> Stake
stakeFromGovernor :: Governor -> Stake
stakeFromGovernor Governor
gov =
  Tagged @Type GTTag AssetClass -> AssetClass -> Stake
Stake Governor
gov.gtClassRef (AssetClass -> Stake) -> AssetClass -> Stake
forall a b. (a -> b) -> a -> b
$
    Governor -> AssetClass
proposalSTAssetClassFromGovernor Governor
gov

{- | Get the hash of 'Agora.Stake.Script.stakePolicy'.

     @since 0.1.0
-}
stakeValidatorHashFromGovernor :: Governor -> ValidatorHash
stakeValidatorHashFromGovernor :: Governor -> ValidatorHash
stakeValidatorHashFromGovernor Governor
gov = Validator -> ValidatorHash
validatorHash Validator
validator
  where
    params :: Stake
params = Governor -> Stake
stakeFromGovernor Governor
gov
    validator :: Validator
validator = ClosedTerm PValidator -> Validator
mkValidator (ClosedTerm PValidator -> Validator)
-> ClosedTerm PValidator -> Validator
forall a b. (a -> b) -> a -> b
$ Stake -> ClosedTerm PValidator
stakeValidator Stake
params

{- | Get the 'Proposal' parameter, given the 'Governor' parameter.

     @since 0.1.0
-}
proposalFromGovernor :: Governor -> Proposal
proposalFromGovernor :: Governor -> Proposal
proposalFromGovernor Governor
gov = AssetClass -> AssetClass -> Integer -> Proposal
Proposal AssetClass
gstAC AssetClass
sstAC Integer
mc
  where
    gstAC :: AssetClass
gstAC = Governor -> AssetClass
governorSTAssetClassFromGovernor Governor
gov
    mc :: Integer
mc = Governor
gov.maximumCosigners
    sstAC :: AssetClass
sstAC = Governor -> AssetClass
stakeSTAssetClassFromGovernor Governor
gov

{- | Get the hash of 'Agora.Proposal.proposalPolicy'.

     @since 0.1.0
-}
proposalValidatorHashFromGovernor :: Governor -> ValidatorHash
proposalValidatorHashFromGovernor :: Governor -> ValidatorHash
proposalValidatorHashFromGovernor Governor
gov = Validator -> ValidatorHash
validatorHash Validator
validator
  where
    params :: Proposal
params = Governor -> Proposal
proposalFromGovernor Governor
gov
    validator :: Validator
validator = ClosedTerm PValidator -> Validator
mkValidator (ClosedTerm PValidator -> Validator)
-> ClosedTerm PValidator -> Validator
forall a b. (a -> b) -> a -> b
$ Proposal -> ClosedTerm PValidator
proposalValidator Proposal
params

{- | Get the hash of 'Agora.Proposal.proposalValidator'.

     @since 0.1.0
-}
governorValidatorHash :: Governor -> ValidatorHash
governorValidatorHash :: Governor -> ValidatorHash
governorValidatorHash Governor
gov = Validator -> ValidatorHash
validatorHash Validator
validator
  where
    validator :: Validator
validator = ClosedTerm PValidator -> Validator
mkValidator (ClosedTerm PValidator -> Validator)
-> ClosedTerm PValidator -> Validator
forall a b. (a -> b) -> a -> b
$ Governor -> ClosedTerm PValidator
governorValidator Governor
gov

{- | Get the 'AuthorityToken' parameter given the 'Governor' parameter.

     @since 0.1.0
-}
authorityTokenFromGovernor :: Governor -> AuthorityToken
authorityTokenFromGovernor :: Governor -> AuthorityToken
authorityTokenFromGovernor Governor
gov = AssetClass -> AuthorityToken
AuthorityToken (AssetClass -> AuthorityToken) -> AssetClass -> AuthorityToken
forall a b. (a -> b) -> a -> b
$ Governor -> AssetClass
governorSTAssetClassFromGovernor Governor
gov

{- | Get the 'CurrencySymbol' of the authority token.

     @since 0.1.0
-}
authorityTokenSymbolFromGovernor :: Governor -> CurrencySymbol
authorityTokenSymbolFromGovernor :: Governor -> CurrencySymbol
authorityTokenSymbolFromGovernor Governor
gov = MintingPolicy -> CurrencySymbol
mintingPolicySymbol MintingPolicy
policy
  where
    policy :: MintingPolicy
policy = ClosedTerm PMintingPolicy -> MintingPolicy
mkMintingPolicy (ClosedTerm PMintingPolicy -> MintingPolicy)
-> ClosedTerm PMintingPolicy -> MintingPolicy
forall a b. (a -> b) -> a -> b
$ AuthorityToken -> ClosedTerm PMintingPolicy
authorityTokenPolicy AuthorityToken
params
    params :: AuthorityToken
params = Governor -> AuthorityToken
authorityTokenFromGovernor Governor
gov