{- |
Module     : Agora.Stake.Scripts
Maintainer : emi@haskell.fyi
Description: Plutus Scripts for Stakes.

Plutus Scripts for Stakes.
-}
module Agora.Stake.Scripts (stakePolicy, stakeValidator) where

import Agora.SafeMoney (GTTag)
import Agora.Stake
import Agora.Utils (
  mustBePJust,
  mustFindDatum',
  pvalidatorHashToTokenName,
 )
import Data.Tagged (Tagged (..), untag)
import Plutarch.Api.V1 (
  AmountGuarantees (Positive),
  PCredential (PPubKeyCredential, PScriptCredential),
  PMintingPolicy,
  PScriptPurpose (PMinting, PSpending),
  PTokenName,
  PTxInfo,
  PValidator,
  PValue,
  mintingPolicySymbol,
  mkMintingPolicy,
 )
import Plutarch.Api.V1.AssetClass (passetClass, passetClassValueOf, pvalueOf)
import Plutarch.Api.V1.ScriptContext (pfindTxInByTxOutRef, pisTokenSpent, ptxSignedBy, pvalueSpent)
import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (pgeqByClass', pgeqBySymbol, psymbolValueOf)
import Plutarch.Extra.Record (mkRecordConstr, (.&), (.=))
import Plutarch.Extra.TermCont (pguardC, pletC, pmatchC, ptryFromC)
import Plutarch.Internal (punsafeCoerce)
import Plutarch.Numeric.Additive (AdditiveMonoid (zero), AdditiveSemigroup ((+)))
import Plutarch.SafeMoney (
  pdiscreteValue',
  pvalueDiscrete',
 )
import PlutusLedgerApi.V1.Value (AssetClass (AssetClass))
import Prelude hiding (Num (..))

{- | Policy for Stake state threads.

   == What this Policy does

   === For minting:

   - Check that exactly one state thread is minted.
   - Check that an output exists with a state thread and a valid datum.
   - Check that no state thread is an input.
   - assert @'PlutusLedgerApi.V1.TokenName' == 'PlutusLedgerApi.V1.ValidatorHash'@
     of the script that we pay to.

   === For burning:

   - Check that exactly one state thread is burned.
   - Check that datum at state thread is valid and not locked.

   @since 0.1.0
-}
stakePolicy ::
  -- | The (governance) token that a Stake can store.
  Tagged GTTag AssetClass ->
  ClosedTerm PMintingPolicy
stakePolicy :: Tagged @Type GTTag AssetClass -> ClosedTerm PMintingPolicy
stakePolicy Tagged @Type GTTag AssetClass
gtClassRef =
  (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
_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
    HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctx <- ((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
$ HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctx.txInfo
    let _a :: Term _ PTxInfo
        _a :: Term s PTxInfo
_a = Term s PTxInfo
txInfo
    HRec
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ((':)
        @(Symbol, Type)
        '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
        ((':)
           @(Symbol, Type)
           '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
           ((':)
              @(Symbol, Type)
              '("signatories",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("datums",
                   Term
                     s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                 ('[] @(Symbol, Type)))))))
txInfoF <- ((HRec
    ((':)
       @(Symbol, Type)
       '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
       ((':)
          @(Symbol, Type)
          '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
          ((':)
             @(Symbol, Type)
             '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
             ((':)
                @(Symbol, Type)
                '("signatories",
                  Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                ((':)
                   @(Symbol, Type)
                   '("datums",
                     Term
                       s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                   ('[] @(Symbol, Type)))))))
  -> Term s POpaque)
 -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
           ((':)
              @(Symbol, Type)
              '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
              ((':)
                 @(Symbol, Type)
                 '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
                 ((':)
                    @(Symbol, Type)
                    '("signatories",
                      Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                    ((':)
                       @(Symbol, Type)
                       '("datums",
                         Term
                           s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                       ('[] @(Symbol, Type))))))))
forall a (s :: S) (r :: PType).
((a -> Term s r) -> Term s r) -> TermCont @r s a
tcont (((HRec
     ((':)
        @(Symbol, Type)
        '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
        ((':)
           @(Symbol, Type)
           '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
           ((':)
              @(Symbol, Type)
              '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
              ((':)
                 @(Symbol, Type)
                 '("signatories",
                   Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                 ((':)
                    @(Symbol, Type)
                    '("datums",
                      Term
                        s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                    ('[] @(Symbol, Type)))))))
   -> Term s POpaque)
  -> Term s POpaque)
 -> TermCont
      @POpaque
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
            ((':)
               @(Symbol, Type)
               '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
               ((':)
                  @(Symbol, Type)
                  '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
                  ((':)
                     @(Symbol, Type)
                     '("signatories",
                       Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                     ((':)
                        @(Symbol, Type)
                        '("datums",
                          Term
                            s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                        ('[] @(Symbol, Type)))))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
          ((':)
             @(Symbol, Type)
             '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
             ((':)
                @(Symbol, Type)
                '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
                ((':)
                   @(Symbol, Type)
                   '("signatories",
                     Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                   ((':)
                      @(Symbol, Type)
                      '("datums",
                        Term
                          s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                      ('[] @(Symbol, Type)))))))
     -> Term s POpaque)
    -> Term s POpaque)
-> TermCont
     @POpaque
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
           ((':)
              @(Symbol, Type)
              '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
              ((':)
                 @(Symbol, Type)
                 '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
                 ((':)
                    @(Symbol, Type)
                    '("signatories",
                      Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
                    ((':)
                       @(Symbol, Type)
                       '("datums",
                         Term
                           s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                       ('[] @(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 @'["mint", "inputs", "outputs", "signatories", "datums"] Term s PTxInfo
txInfo

    PMinting Term
  s
  (PDataRecord
     ((':)
        @PLabeledType ("_0" ':= PCurrencySymbol) ('[] @PLabeledType)))
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 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)
ctx.purpose
    Term s PCurrencySymbol
ownSymbol <- Term s PCurrencySymbol
-> TermCont @POpaque s (Term s PCurrencySymbol)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PCurrencySymbol
 -> TermCont @POpaque s (Term s PCurrencySymbol))
-> Term s PCurrencySymbol
-> TermCont @POpaque s (Term s PCurrencySymbol)
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 @"_0" Term
  s
  (PDataRecord
     ((':) @PLabeledType ("_0" ':= PCurrencySymbol) ('[] @PLabeledType))
   :--> PCurrencySymbol)
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType ("_0" ':= PCurrencySymbol) ('[] @PLabeledType)))
-> Term s PCurrencySymbol
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord
     ((':)
        @PLabeledType ("_0" ':= PCurrencySymbol) ('[] @PLabeledType)))
ownSymbol'
    Term s (PInteger @S)
spentST <- 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
  (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
ownSymbol 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
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ((':)
        @(Symbol, Type)
        '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
        ((':)
           @(Symbol, Type)
           '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
           ((':)
              @(Symbol, Type)
              '("signatories",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("datums",
                   Term
                     s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                 ('[] @(Symbol, Type)))))))
txInfoF.inputs
    Term s (PInteger @S)
mintedST <- 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
  (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
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ((':)
        @(Symbol, Type)
        '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
        ((':)
           @(Symbol, Type)
           '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
           ((':)
              @(Symbol, Type)
              '("signatories",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("datums",
                   Term
                     s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                 ('[] @(Symbol, Type)))))))
txInfoF.mint

    let burning :: Term s POpaque
burning = 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)
"ST at inputs must be 1" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PInteger @S)
spentST 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 (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)
"ST burned" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PInteger @S)
mintedST 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 (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)
"An unlocked input existed containing an ST" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term
  s
  ((PAsData PTxInInfo :--> PBool)
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
forall (list :: PType -> PType) (a :: PType) (s :: S).
PIsListLike list a =>
Term s ((a :--> PBool) :--> (list a :--> PBool))
pany
              # plam
                ( \((pfield @"resolved" #) -> txOut) -> unTermCont $ do
                    txOutF <- tcont $ pletFields @'["value", "datumHash"] txOut
                    pure $
                      pif
                        (psymbolValueOf # ownSymbol # txOutF.value #== 1)
                        ( let datum = mustFindDatum' @PStakeDatum # txOutF.datumHash # txInfoF.datums
                           in pnot # (stakeLocked # datum)
                        )
                        (pconstant False)
                )
              # pfromData txInfoF.inputs

          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 (PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ())

    let minting :: Term s POpaque
minting = 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)
"ST at inputs must be 0" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PInteger @S)
spentST 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)
0

          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)
"Minted ST must be exactly 1" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PInteger @S)
mintedST 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 (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)
"A UTXO must exist with the correct output" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            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
              let scriptOutputWithStakeST :: Term s (PAsData PTxOut)
scriptOutputWithStakeST =
                    Term
  s (PString @S :--> (PMaybe (PAsData PTxOut) :--> PAsData PTxOut))
forall (a :: PType) (s :: S).
Term s (PString @S :--> (PMaybe a :--> a))
mustBePJust
                      # "Output to script not found"
                        #$ pfind
                      # plam
                        ( \output -> unTermCont $ do
                            outputF <- tcont $ pletFields @'["value", "address"] output
                            pure $
                              pmatch (pfromData $ pfield @"credential" # outputF.address) $ \case
                                -- Should pay to a script address
                                PPubKeyCredential _ -> pcon PFalse
                                PScriptCredential ((pfield @"_0" #) -> validatorHash) ->
                                  let tn :: Term _ PTokenName
                                      tn = pvalidatorHashToTokenName validatorHash
                                   in pvalueOf # outputF.value # ownSymbol # tn #== 1
                        )
                      # pfromData txInfoF.outputs

              HRec
  (BoundTerms
     (PFields (PAsData PTxOut))
     (Bindings
        (PFields (PAsData PTxOut))
        ((':)
           @Symbol
           "value"
           ((':) @Symbol "address" ((':) @Symbol "datumHash" ('[] @Symbol)))))
     s)
outputF <-
                ((HRec
    (BoundTerms
       (PFields (PAsData PTxOut))
       (Bindings
          (PFields (PAsData PTxOut))
          ((':)
             @Symbol
             "value"
             ((':) @Symbol "address" ((':) @Symbol "datumHash" ('[] @Symbol)))))
       s)
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':)
                 @Symbol
                 "value"
                 ((':) @Symbol "address" ((':) @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
              "value"
              ((':) @Symbol "address" ((':) @Symbol "datumHash" ('[] @Symbol)))))
        s)
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (HRec
         (BoundTerms
            (PFields (PAsData PTxOut))
            (Bindings
               (PFields (PAsData PTxOut))
               ((':)
                  @Symbol
                  "value"
                  ((':) @Symbol "address" ((':) @Symbol "datumHash" ('[] @Symbol)))))
            s)))
-> ((HRec
       (BoundTerms
          (PFields (PAsData PTxOut))
          (Bindings
             (PFields (PAsData PTxOut))
             ((':)
                @Symbol
                "value"
                ((':) @Symbol "address" ((':) @Symbol "datumHash" ('[] @Symbol)))))
          s)
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        (BoundTerms
           (PFields (PAsData PTxOut))
           (Bindings
              (PFields (PAsData PTxOut))
              ((':)
                 @Symbol
                 "value"
                 ((':) @Symbol "address" ((':) @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 @'["value", "address", "datumHash"] Term s (PAsData PTxOut)
scriptOutputWithStakeST
              HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ('[] @(Symbol, Type))))
datumF <-
                ((HRec
    ((':)
       @(Symbol, Type)
       '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
       ((':)
          @(Symbol, Type)
          '("owner", Term s (PAsData PPubKeyHash))
          ('[] @(Symbol, Type))))
  -> Term s PBool)
 -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
           ((':)
              @(Symbol, Type)
              '("owner", Term s (PAsData PPubKeyHash))
              ('[] @(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))))
   -> Term s PBool)
  -> Term s PBool)
 -> TermCont
      @PBool
      s
      (HRec
         ((':)
            @(Symbol, Type)
            '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
            ((':)
               @(Symbol, Type)
               '("owner", Term s (PAsData PPubKeyHash))
               ('[] @(Symbol, Type))))))
-> ((HRec
       ((':)
          @(Symbol, Type)
          '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
          ((':)
             @(Symbol, Type)
             '("owner", Term s (PAsData PPubKeyHash))
             ('[] @(Symbol, Type))))
     -> Term s PBool)
    -> Term s PBool)
-> TermCont
     @PBool
     s
     (HRec
        ((':)
           @(Symbol, Type)
           '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
           ((':)
              @(Symbol, Type)
              '("owner", Term s (PAsData PPubKeyHash))
              ('[] @(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 @'["owner", "stakedAmount"] (Term s PStakeDatum
 -> (HRecOf
       PStakeDatum
       ((':) @Symbol "owner" ((':) @Symbol "stakedAmount" ('[] @Symbol)))
       s
     -> Term s PBool)
 -> Term s PBool)
-> Term s PStakeDatum
-> (HRecOf
      PStakeDatum
      ((':) @Symbol "owner" ((':) @Symbol "stakedAmount" ('[] @Symbol)))
      s
    -> Term s PBool)
-> Term s PBool
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' @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
           "value"
           ((':) @Symbol "address" ((':) @Symbol "datumHash" ('[] @Symbol)))))
     s)
outputF.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
  ((':)
     @(Symbol, Type)
     '("inputs", Term s (PAsData (PBuiltinList (PAsData PTxInInfo))))
     ((':)
        @(Symbol, Type)
        '("outputs", Term s (PAsData (PBuiltinList (PAsData PTxOut))))
        ((':)
           @(Symbol, Type)
           '("mint", Term s (PAsData (PValue 'Sorted 'NoGuarantees)))
           ((':)
              @(Symbol, Type)
              '("signatories",
                Term s (PAsData (PBuiltinList (PAsData PPubKeyHash))))
              ((':)
                 @(Symbol, Type)
                 '("datums",
                   Term
                     s (PAsData (PBuiltinList (PAsData (PTuple PDatumHash PDatum)))))
                 ('[] @(Symbol, Type)))))))
txInfoF.datums

              let hasExpectedStake :: Term s PBool
hasExpectedStake =
                    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)
"Stake ouput has expected amount of stake token" (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
forall a b. (a -> b) -> a -> b
$
                      Tagged @Type GTTag AssetClass
-> Term s (PValue 'Sorted 'Positive :--> 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' Tagged @Type GTTag AssetClass
gtClassRef 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
           "value"
           ((':) @Symbol "address" ((':) @Symbol "datumHash" ('[] @Symbol)))))
     s)
outputF.value 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
#== HRec
  ((':)
     @(Symbol, Type)
     '("stakedAmount", Term s (PAsData (PDiscrete @Type GTTag)))
     ((':)
        @(Symbol, Type)
        '("owner", Term s (PAsData PPubKeyHash))
        ('[] @(Symbol, Type))))
datumF.stakedAmount
              let ownerSignsTransaction :: Term s PBool
ownerSignsTransaction =
                    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)
"Stake Owner should sign the transaction" (Term s PBool -> Term s PBool) -> Term s PBool -> Term s PBool
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
                        # txInfoF.signatories
                        # datumF.owner

              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
hasExpectedStake Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#&& Term s PBool
ownerSignsTransaction

          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 (PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ())

    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 -> Term s POpaque -> Term s POpaque
forall (s :: S) (a :: PType).
Term s PBool -> Term s a -> Term s a -> Term s a
pif (Term s (PInteger @S)
0 Term s (PInteger @S) -> Term s (PInteger @S) -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#< Term s (PInteger @S)
mintedST) Term s POpaque
minting Term s POpaque
burning

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

{- | Validator intended for Stake UTXOs to be locked by.

     == What this Validator does:

     === 'DepositWithdraw'

     Deposit or withdraw some GT to the stake.

     - Tx must be signed by the owner.
     - The 'stakedAmount' field must be updated.
     - The stake must not be locked.
     - The new UTXO must have the previous value plus the difference
       as stated by the redeemer.

     === 'PermitVote'

     Allow a 'ProposalLock' to be put on the stake in order to vote
     on a proposal.

     - A proposal token must be spent alongside the stake.

       * Its total votes must be correctly updated to include this stake's
         contribution.

     - Tx must be signed by the owner.

     === 'RetractVotes'

     Remove a 'ProposalLock' set when voting on a proposal.

     - A proposal token must be spent alongside the stake.
     - Tx must be signed by the owner.

     === 'Destroy'

     Destroy the stake in order to reclaim the min ADA.

     - The stake must not be locked.
     - Tx must be signed by the owner.

     === 'WitnessStake'

     Allow this Stake to be included in a transaction without making
     any changes to it. In the future,
     this could use [CIP-31](https://cips.cardano.org/cips/cip31/) instead.

     - Tx must be signed by the owner __or__ a proposal ST token must be spent
       alongside the stake.
     - The datum and value must remain unchanged.

     @since 0.1.0
-}
stakeValidator :: Stake -> ClosedTerm PValidator
stakeValidator :: Stake -> ClosedTerm PValidator
stakeValidator Stake
stake =
  (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
    HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctx <- ((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 HRec
  (BoundTerms
     (PFields PScriptContext)
     (Bindings
        (PFields PScriptContext)
        ((':) @Symbol "txInfo" ((':) @Symbol "purpose" ('[] @Symbol))))
     s)
ctx.txInfo
    HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol "signatories" ((':) @Symbol "datums" ('[] @Symbol)))))))
     s)
txInfoF <- ((HRec
    (BoundTerms
       (PFields PTxInfo)
       (Bindings
          (PFields PTxInfo)
          ((':)
             @Symbol
             "mint"
             ((':)
                @Symbol
                "inputs"
                ((':)
                   @Symbol
                   "outputs"
                   ((':)
                      @Symbol "signatories" ((':) @Symbol "datums" ('[] @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 "signatories" ((':) @Symbol "datums" ('[] @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 "signatories" ((':) @Symbol "datums" ('[] @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 "signatories" ((':) @Symbol "datums" ('[] @Symbol)))))))
            s)))
-> ((HRec
       (BoundTerms
          (PFields PTxInfo)
          (Bindings
             (PFields PTxInfo)
             ((':)
                @Symbol
                "mint"
                ((':)
                   @Symbol
                   "inputs"
                   ((':)
                      @Symbol
                      "outputs"
                      ((':)
                         @Symbol "signatories" ((':) @Symbol "datums" ('[] @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 "signatories" ((':) @Symbol "datums" ('[] @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", "signatories", "datums"] Term s PTxInfo
txInfo

    (Term s (PAsData PStakeRedeemer) -> Term s PStakeRedeemer
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData -> Term s PStakeRedeemer
stakeRedeemer, Reduce @Type (PTryFromExcess PData (PAsData PStakeRedeemer) s)
_) <- Term s PData
-> TermCont
     @POpaque
     s
     (Term s (PAsData PStakeRedeemer),
      Reduce @Type (PTryFromExcess PData (PAsData PStakeRedeemer) s))
forall (b :: PType) (r :: PType) (a :: PType) (s :: S).
PTryFrom a b =>
Term s a
-> TermCont @r s (Term s b, Reduce @Type (PTryFromExcess a b s))
ptryFromC Term s PData
redeemer

    -- TODO: Use PTryFrom
    let stakeDatum' :: Term _ PStakeDatum
        stakeDatum' :: Term s PStakeDatum
stakeDatum' = Term s (PAsData PStakeDatum) -> Term s PStakeDatum
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData PStakeDatum) -> Term s PStakeDatum)
-> Term s (PAsData PStakeDatum) -> Term s PStakeDatum
forall a b. (a -> b) -> a -> b
$ Term s PData -> Term s (PAsData PStakeDatum)
forall (s :: S) (a :: PType) (b :: PType). Term s a -> Term s b
punsafeCoerce Term s PData
datum
    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)))))
stakeDatum <- ((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 @'["owner", "stakedAmount", "lockedBy"] Term s PStakeDatum
stakeDatum'

    PSpending Term
  s
  (PDataRecord
     ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType)))
txOutRef <- 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)
ctx.purpose

    PJust Term s PTxInInfo
txInInfo <- Term s (PMaybe PTxInInfo)
-> TermCont @POpaque s (PMaybe PTxInInfo s)
forall {r :: PType} (a :: PType) (s :: S).
PMatch a =>
Term s a -> TermCont @r s (a s)
pmatchC (Term s (PMaybe PTxInInfo)
 -> TermCont @POpaque s (PMaybe PTxInInfo s))
-> Term s (PMaybe PTxInInfo)
-> TermCont @POpaque s (PMaybe PTxInInfo s)
forall a b. (a -> b) -> a -> b
$ Term
  s
  (PTxOutRef
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo))
forall (s :: S).
Term
  s
  (PTxOutRef
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo))
pfindTxInByTxOutRef Term
  s
  (PTxOutRef
   :--> (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo))
-> Term s PTxOutRef
-> Term s (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# (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
  (PDataRecord
     ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType))
   :--> PTxOutRef)
-> Term
     s
     (PDataRecord
        ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType)))
-> Term s PTxOutRef
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord
     ((':) @PLabeledType ("_0" ':= PTxOutRef) ('[] @PLabeledType)))
txOutRef) Term s (PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo)
-> Term s (PBuiltinList (PAsData PTxInInfo))
-> Term s (PMaybe PTxInInfo)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# HRec
  (BoundTerms
     (PFields PTxInfo)
     (Bindings
        (PFields PTxInfo)
        ((':)
           @Symbol
           "mint"
           ((':)
              @Symbol
              "inputs"
              ((':)
                 @Symbol
                 "outputs"
                 ((':)
                    @Symbol "signatories" ((':) @Symbol "datums" ('[] @Symbol)))))))
     s)
txInfoF.inputs
    Term
  s
  (PAsData
     (PUnLabel
        (IndexList
           @PLabeledType
           (PLabelIndex "address" (PFields (PAsData PTxOut)))
           (PFields (PAsData PTxOut)))))
ownAddress <- Term
  s
  (PAsData
     (PUnLabel
        (IndexList
           @PLabeledType
           (PLabelIndex "address" (PFields (PAsData PTxOut)))
           (PFields (PAsData PTxOut)))))
-> TermCont
     @POpaque
     s
     (Term
        s
        (PAsData
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "address" (PFields (PAsData PTxOut)))
                 (PFields (PAsData PTxOut))))))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term
   s
   (PAsData
      (PUnLabel
         (IndexList
            @PLabeledType
            (PLabelIndex "address" (PFields (PAsData PTxOut)))
            (PFields (PAsData PTxOut)))))
 -> TermCont
      @POpaque
      s
      (Term
         s
         (PAsData
            (PUnLabel
               (IndexList
                  @PLabeledType
                  (PLabelIndex "address" (PFields (PAsData PTxOut)))
                  (PFields (PAsData PTxOut)))))))
-> Term
     s
     (PAsData
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "address" (PFields (PAsData PTxOut)))
              (PFields (PAsData PTxOut)))))
-> TermCont
     @POpaque
     s
     (Term
        s
        (PAsData
           (PUnLabel
              (IndexList
                 @PLabeledType
                 (PLabelIndex "address" (PFields (PAsData PTxOut)))
                 (PFields (PAsData PTxOut))))))
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 @"address" Term
  s
  (PAsData PTxOut
   :--> PAsData
          (PUnLabel
             (IndexList
                @PLabeledType
                (PLabelIndex "address" (PFields (PAsData PTxOut)))
                (PFields (PAsData PTxOut)))))
-> Term s (PAsData PTxOut)
-> Term
     s
     (PAsData
        (PUnLabel
           (IndexList
              @PLabeledType
              (PLabelIndex "address" (PFields (PAsData PTxOut)))
              (PFields (PAsData PTxOut)))))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s 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 (PTxInInfo :--> PAsData PTxOut)
-> Term s PTxInInfo -> Term s (PAsData PTxOut)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PTxInInfo
txInInfo
    let continuingValue :: Term _ (PValue _ _)
        continuingValue :: Term s (PValue 'Sorted 'Positive)
continuingValue = 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 @"value" Term s (PAsData PTxOut :--> PValue 'Sorted 'Positive)
-> Term s (PAsData PTxOut) -> Term s (PValue 'Sorted 'Positive)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s 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 (PTxInInfo :--> PAsData PTxOut)
-> Term s PTxInInfo -> Term s (PAsData PTxOut)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PTxInInfo
txInInfo

    -- Whether the owner signs this transaction or not.
    Term s PBool
ownerSignsTransaction <- Term s PBool -> TermCont @POpaque s (Term s PBool)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PBool -> TermCont @POpaque s (Term s PBool))
-> Term s PBool -> TermCont @POpaque s (Term s PBool)
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 "signatories" ((':) @Symbol "datums" ('[] @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)))))
stakeDatum.owner

    Term s PCurrencySymbol
stCurrencySymbol <- Term s PCurrencySymbol
-> TermCont @POpaque s (Term s PCurrencySymbol)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PCurrencySymbol
 -> TermCont @POpaque s (Term s PCurrencySymbol))
-> Term s PCurrencySymbol
-> TermCont @POpaque s (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
$ MintingPolicy -> CurrencySymbol
mintingPolicySymbol (MintingPolicy -> CurrencySymbol)
-> MintingPolicy -> CurrencySymbol
forall a b. (a -> b) -> a -> b
$ ClosedTerm PMintingPolicy -> MintingPolicy
mkMintingPolicy (Tagged @Type GTTag AssetClass -> ClosedTerm PMintingPolicy
stakePolicy Stake
stake.gtClassRef)
    Term s (PInteger @S)
mintedST <- 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
  (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
stCurrencySymbol 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 "signatories" ((':) @Symbol "datums" ('[] @Symbol)))))))
     s)
txInfoF.mint
    Term s (PValue 'Sorted 'Positive)
valueSpent <- Term s (PValue 'Sorted 'Positive)
-> TermCont @POpaque s (Term s (PValue 'Sorted 'Positive))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PValue 'Sorted 'Positive)
 -> TermCont @POpaque s (Term s (PValue 'Sorted 'Positive)))
-> Term s (PValue 'Sorted 'Positive)
-> TermCont @POpaque s (Term s (PValue 'Sorted 'Positive))
forall a b. (a -> b) -> a -> 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 "signatories" ((':) @Symbol "datums" ('[] @Symbol)))))))
     s)
txInfoF.inputs
    Term s (PInteger @S)
spentST <- 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
  (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
stCurrencySymbol 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 (PValue 'Sorted 'Positive)
valueSpent

    let AssetClass (CurrencySymbol
propCs, TokenName
propTn) = Stake
stake.proposalSTClass
        proposalSTClass :: Term s PAssetClass
proposalSTClass = 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
# PLifted PCurrencySymbol -> Term s PCurrencySymbol
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PCurrencySymbol
CurrencySymbol
propCs 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
propTn
    Term s (PInteger @S)
spentProposalST <- 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 (PValue 'Sorted 'Positive :--> (PAssetClass :--> PInteger @S))
forall (s :: S) (keys :: KeyGuarantees)
       (amounts :: AmountGuarantees).
Term s (PValue keys amounts :--> (PAssetClass :--> PInteger @S))
passetClassValueOf Term
  s (PValue 'Sorted 'Positive :--> (PAssetClass :--> PInteger @S))
-> Term s (PValue 'Sorted 'Positive)
-> Term s (PAssetClass :--> PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PValue 'Sorted 'Positive)
valueSpent Term s (PAssetClass :--> PInteger @S)
-> Term s PAssetClass -> Term s (PInteger @S)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PAssetClass
proposalSTClass

    -- Is the stake currently locked?
    Term s PBool
stakeIsLocked <- Term s PBool -> TermCont @POpaque s (Term s PBool)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PBool -> TermCont @POpaque s (Term s PBool))
-> Term s PBool -> TermCont @POpaque s (Term s PBool)
forall a b. (a -> b) -> a -> b
$ Term s (PStakeDatum :--> PBool)
forall (s :: S). Term s (PStakeDatum :--> PBool)
stakeLocked Term s (PStakeDatum :--> PBool)
-> Term s PStakeDatum -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PStakeDatum
stakeDatum'

    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 PStakeRedeemer
-> (PStakeRedeemer 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 PStakeRedeemer
stakeRedeemer ((PStakeRedeemer s -> Term s POpaque) -> Term s POpaque)
-> (PStakeRedeemer s -> Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ \case
        PDestroy 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)
"ST at inputs must be 1" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PInteger @S)
spentST 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 (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)
"Should burn ST" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
            Term s (PInteger @S)
mintedST 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 (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 unlocked" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$ Term s (PBool :--> PBool)
forall (s :: S). Term s (PBool :--> PBool)
pnot Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s PBool
stakeIsLocked

          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)
"Owner signs this transaction" Term s PBool
ownerSignsTransaction

          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 (PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ())
        --------------------------------------------------------------------------
        -- Handle redeemers that require own stake output.
        PStakeRedeemer s
_ -> 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
          -- Filter out own output with own address and PST.
          Term s (PAsData PTxOut)
ownOutput <-
            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 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)
"Own output should be present" Term s (PMaybe (PAsData PTxOut) :--> PAsData PTxOut)
-> Term s (PMaybe (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
  ((PAsData PTxOut :--> PBool)
   :--> (PBuiltinList (PAsData PTxOut) :--> PMaybe (PAsData PTxOut)))
forall (l :: PType -> PType) (a :: PType) (s :: S).
PIsListLike l a =>
Term s ((a :--> PBool) :--> (l a :--> PMaybe a))
pfind
                # plam
                  ( \input -> unTermCont $ do
                      inputF <- tcont $ pletFields @'["address", "value"] input
                      pure $
                        inputF.address #== ownAddress
                          #&& psymbolValueOf # stCurrencySymbol # inputF.value #== 1
                  )
                # pfromData txInfoF.outputs

          Term s PStakeDatum
stakeOut <-
            Term s PStakeDatum -> TermCont @POpaque s (Term s PStakeDatum)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PStakeDatum -> TermCont @POpaque s (Term s PStakeDatum))
-> Term s PStakeDatum -> TermCont @POpaque s (Term s PStakeDatum)
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' @PStakeDatum
                # (pfield @"datumHash" # ownOutput)
                # txInfoF.datums

          Term s (PValue 'Sorted 'Positive)
ownOutputValue <-
            Term s (PValue 'Sorted 'Positive)
-> TermCont @POpaque s (Term s (PValue 'Sorted 'Positive))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PValue 'Sorted 'Positive)
 -> TermCont @POpaque s (Term s (PValue 'Sorted 'Positive)))
-> Term s (PValue 'Sorted 'Positive)
-> TermCont @POpaque s (Term s (PValue 'Sorted 'Positive))
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 @"value" Term s (PAsData PTxOut :--> PValue 'Sorted 'Positive)
-> Term s (PAsData PTxOut) -> Term s (PValue 'Sorted 'Positive)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData PTxOut)
ownOutput

          Term s PBool
ownOutputValueUnchanged <-
            Term s PBool -> TermCont @POpaque s (Term s PBool)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PBool -> TermCont @POpaque s (Term s PBool))
-> Term s PBool -> TermCont @POpaque s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
              Term s (PValue 'Sorted 'Positive)
-> Term s (PAsData (PValue 'Sorted 'Positive))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PValue 'Sorted 'Positive)
continuingValue Term s (PAsData (PValue 'Sorted 'Positive))
-> Term s (PAsData (PValue 'Sorted 'Positive)) -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s (PValue 'Sorted 'Positive)
-> Term s (PAsData (PValue 'Sorted 'Positive))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PValue 'Sorted 'Positive)
ownOutputValue

          Term s PBool
stakeOutUnchanged <-
            Term s PBool -> TermCont @POpaque s (Term s PBool)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PBool -> TermCont @POpaque s (Term s PBool))
-> Term s PBool -> TermCont @POpaque s (Term s PBool)
forall a b. (a -> b) -> a -> b
$
              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
stakeOut 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 PStakeDatum -> Term s (PAsData PStakeDatum)
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s PStakeDatum
stakeDatum'

          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 PStakeRedeemer
-> (PStakeRedeemer 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 PStakeRedeemer
stakeRedeemer ((PStakeRedeemer s -> Term s POpaque) -> Term s POpaque)
-> (PStakeRedeemer s -> Term s POpaque) -> Term s POpaque
forall a b. (a -> b) -> a -> b
$ \case
              PRetractVotes Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("locks" ':= PBuiltinList (PAsData PProposalLock))
        ('[] @PLabeledType)))
l -> 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)
"Owner signs this transaction"
                  Term s PBool
ownerSignsTransaction

                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)
"ST at inputs must be 1" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  Term s (PInteger @S)
spentST 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

                -- This puts trust into the Proposal. The Proposal must necessarily check
                -- that this is not abused.
                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 ST spent" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  Term s (PInteger @S)
spentProposalST 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 (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)
"A UTXO must exist with the correct output" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  let expectedLocks :: Term s (PAsData (PBuiltinList (PAsData PProposalLock)))
expectedLocks = 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 @"locks" Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("locks" ':= PBuiltinList (PAsData PProposalLock))
        ('[] @PLabeledType))
   :--> PAsData (PBuiltinList (PAsData PProposalLock)))
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           ("locks" ':= PBuiltinList (PAsData PProposalLock))
           ('[] @PLabeledType)))
-> Term s (PAsData (PBuiltinList (PAsData PProposalLock)))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("locks" ':= PBuiltinList (PAsData PProposalLock))
        ('[] @PLabeledType)))
l

                      expectedDatum :: Term s PStakeDatum
expectedDatum =
                        (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)))))
stakeDatum.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)))))
stakeDatum.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 (PAsData (PBuiltinList (PAsData PProposalLock)))
expectedLocks
                          )

                      valueCorrect :: Term s PBool
valueCorrect = Term s PBool
ownOutputValueUnchanged
                      outputDatumCorrect :: Term s PBool
outputDatumCorrect = Term s PStakeDatum
stakeOut Term s PStakeDatum -> Term s PStakeDatum -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PStakeDatum
expectedDatum
                   in (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
foldl1
                        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)
"valueCorrect" Term s PBool
valueCorrect
                        , 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)
"datumCorrect" Term s PBool
outputDatumCorrect
                        ]

                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 (PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ())
              --------------------------------------------------------------------------
              PPermitVote Term
  s
  (PDataRecord
     ((':)
        @PLabeledType ("lock" ':= PProposalLock) ('[] @PLabeledType)))
l -> 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)
"Owner signs this transaction"
                  Term s PBool
ownerSignsTransaction

                -- This puts trust into the Proposal. The Proposal must necessarily check
                -- that this is not abused.
                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 ST spent" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  Term s (PInteger @S)
spentProposalST 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

                -- Update the stake datum, but only the 'lockedBy' field.

                let -- We actually don't know whether the given lock is valid or not.
                    -- This is checked in the proposal validator.
                    newLock :: Term s (PAsData PProposalLock)
newLock = 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 @"lock" Term
  s
  (PDataRecord
     ((':) @PLabeledType ("lock" ':= PProposalLock) ('[] @PLabeledType))
   :--> PAsData PProposalLock)
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType ("lock" ':= PProposalLock) ('[] @PLabeledType)))
-> Term s (PAsData PProposalLock)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord
     ((':)
        @PLabeledType ("lock" ':= PProposalLock) ('[] @PLabeledType)))
l
                    -- Prepend the new lock to the existing locks.
                    expectedLocks :: Term s (PBuiltinList (PAsData PProposalLock))
expectedLocks = Term
  s
  (PAsData PProposalLock
   :--> (PBuiltinList (PAsData PProposalLock)
         :--> PBuiltinList (PAsData PProposalLock)))
forall (list :: PType -> PType) (a :: PType) (s :: S).
(PListLike list, PElemConstraint list a) =>
Term s (a :--> (list a :--> list a))
pcons Term
  s
  (PAsData PProposalLock
   :--> (PBuiltinList (PAsData PProposalLock)
         :--> PBuiltinList (PAsData PProposalLock)))
-> Term s (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
# Term s (PAsData PProposalLock)
newLock Term
  s
  (PBuiltinList (PAsData PProposalLock)
   :--> PBuiltinList (PAsData PProposalLock))
-> Term s (PBuiltinList (PAsData PProposalLock))
-> Term s (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)))))
stakeDatum.lockedBy

                Term s PStakeDatum
expectedDatum <-
                  Term s PStakeDatum -> TermCont @POpaque s (Term s PStakeDatum)
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s PStakeDatum -> TermCont @POpaque s (Term s PStakeDatum))
-> Term s PStakeDatum -> TermCont @POpaque s (Term s 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)))))
stakeDatum.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)))))
stakeDatum.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))
expectedLocks
                      )

                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)
"A UTXO must exist with the correct output" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  let correctOutputDatum :: Term s PBool
correctOutputDatum = Term s PStakeDatum
stakeOut Term s PStakeDatum -> Term s PStakeDatum -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PStakeDatum
expectedDatum
                      valueCorrect :: Term s PBool
valueCorrect = Term s PBool
ownOutputValueUnchanged
                   in (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
foldl1
                        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)
"valueCorrect" Term s PBool
valueCorrect
                        , 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)
"datumCorrect" Term s PBool
correctOutputDatum
                        ]

                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 (PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ())
              --------------------------------------------------------------------------
              PWitnessStake 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)
"ST at inputs must be 1" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  Term s (PInteger @S)
spentST 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 AssetClass (CurrencySymbol
propCs, TokenName
propTn) = Stake
stake.proposalSTClass
                    propAssetClass :: Term s PAssetClass
propAssetClass = 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
# PLifted PCurrencySymbol -> Term s PCurrencySymbol
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant PLifted PCurrencySymbol
CurrencySymbol
propCs 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
propTn
                    proposalTokenMoved :: Term s PBool
proposalTokenMoved =
                      Term
  s (PAssetClass :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
forall {s :: S}.
Term
  s (PAssetClass :--> (PBuiltinList (PAsData PTxInInfo) :--> PBool))
pisTokenSpent
                        # propAssetClass
                        # txInfoF.inputs

                -- In order for cosignature to be witnessed, it must be possible for a
                -- proposal to allow this transaction to happen. This puts trust into the Proposal.
                -- The Proposal must necessarily check that this is not abused.
                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)
"Owner signs this transaction OR proposal token is spent"
                  (Term s PBool
ownerSignsTransaction Term s PBool -> Term s PBool -> Term s PBool
forall (s :: S). Term s PBool -> Term s PBool -> Term s PBool
#|| Term s PBool
proposalTokenMoved)

                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)
"A UTXO must exist with the correct output" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  let correctOutputDatum :: Term s PBool
correctOutputDatum = Term s PBool
stakeOutUnchanged
                      valueCorrect :: Term s PBool
valueCorrect = Term s PBool
ownOutputValueUnchanged
                   in (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
foldl1
                        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)
"valueCorrect" Term s PBool
valueCorrect
                        , 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)
"correctOutputDatum" Term s PBool
correctOutputDatum
                        ]
                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 (PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ())
              --------------------------------------------------------------------------
              PDepositWithdraw Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("delta" ':= PDiscrete @Type GTTag)
        ('[] @PLabeledType)))
r -> 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)
"ST at inputs must be 1" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  Term s (PInteger @S)
spentST 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 (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 unlocked" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  Term s (PBool :--> PBool)
forall (s :: S). Term s (PBool :--> PBool)
pnot Term s (PBool :--> PBool) -> Term s PBool -> Term s PBool
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
#$ Term s PBool
stakeIsLocked
                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)
"Owner signs this transaction"
                  Term s PBool
ownerSignsTransaction
                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)
"A UTXO must exist with the correct output" (Term s PBool -> TermCont @POpaque s ())
-> Term s PBool -> TermCont @POpaque s ()
forall a b. (a -> b) -> a -> b
$
                  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
                    let oldStakedAmount :: Term s (PDiscrete @Type GTTag)
oldStakedAmount = Term s (PAsData (PDiscrete @Type GTTag))
-> Term s (PDiscrete @Type GTTag)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData (PDiscrete @Type GTTag))
 -> Term s (PDiscrete @Type GTTag))
-> Term s (PAsData (PDiscrete @Type GTTag))
-> Term s (PDiscrete @Type GTTag)
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)))))
stakeDatum.stakedAmount
                        delta :: Term s (PDiscrete @Type GTTag)
delta = Term s (PAsData (PDiscrete @Type GTTag))
-> Term s (PDiscrete @Type GTTag)
forall (a :: PType) (s :: S).
PIsData a =>
Term s (PAsData a) -> Term s a
pfromData (Term s (PAsData (PDiscrete @Type GTTag))
 -> Term s (PDiscrete @Type GTTag))
-> Term s (PAsData (PDiscrete @Type GTTag))
-> Term s (PDiscrete @Type GTTag)
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 @"delta" Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("delta" ':= PDiscrete @Type GTTag)
        ('[] @PLabeledType))
   :--> PAsData (PDiscrete @Type GTTag))
-> Term
     s
     (PDataRecord
        ((':)
           @PLabeledType
           ("delta" ':= PDiscrete @Type GTTag)
           ('[] @PLabeledType)))
-> Term s (PAsData (PDiscrete @Type GTTag))
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term
  s
  (PDataRecord
     ((':)
        @PLabeledType
        ("delta" ':= PDiscrete @Type GTTag)
        ('[] @PLabeledType)))
r

                    Term s (PDiscrete @Type GTTag)
newStakedAmount <- Term s (PDiscrete @Type GTTag)
-> TermCont @PBool s (Term s (PDiscrete @Type GTTag))
forall {r :: PType} (s :: S) (a :: PType).
Term s a -> TermCont @r s (Term s a)
pletC (Term s (PDiscrete @Type GTTag)
 -> TermCont @PBool s (Term s (PDiscrete @Type GTTag)))
-> Term s (PDiscrete @Type GTTag)
-> TermCont @PBool s (Term s (PDiscrete @Type GTTag))
forall a b. (a -> b) -> a -> b
$ Term s (PDiscrete @Type GTTag)
oldStakedAmount Term s (PDiscrete @Type GTTag)
-> Term s (PDiscrete @Type GTTag) -> Term s (PDiscrete @Type GTTag)
forall a. AdditiveSemigroup a => a -> a -> a
+ Term s (PDiscrete @Type GTTag)
delta

                    Term s (PString @S) -> Term s PBool -> TermCont @PBool s ()
forall {r :: PType} (s :: S).
Term s (PString @S) -> Term s PBool -> TermCont @r s ()
pguardC Term s (PString @S)
"New staked amount shoudl be greater than or equal to 0" (Term s PBool -> TermCont @PBool s ())
-> Term s PBool -> TermCont @PBool s ()
forall a b. (a -> b) -> a -> b
$
                      Term s (PDiscrete @Type GTTag)
forall a. AdditiveMonoid a => a
zero Term s (PDiscrete @Type GTTag)
-> Term s (PDiscrete @Type GTTag) -> Term s PBool
forall (t :: PType) (s :: S).
POrd t =>
Term s t -> Term s t -> Term s PBool
#<= Term s (PDiscrete @Type GTTag)
newStakedAmount

                    let expectedDatum :: Term s PStakeDatum
expectedDatum =
                          (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)
.= Term s (PDiscrete @Type GTTag)
-> Term s (PAsData (PDiscrete @Type GTTag))
forall (a :: PType) (s :: S).
PIsData a =>
Term s a -> Term s (PAsData a)
pdata Term s (PDiscrete @Type GTTag)
newStakedAmount
                                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)))))
stakeDatum.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)
.= 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)))))
stakeDatum.lockedBy
                            )
                        datumCorrect :: Term s PBool
datumCorrect = Term s PStakeDatum
stakeOut Term s PStakeDatum -> Term s PStakeDatum -> Term s PBool
forall (t :: PType) (s :: S).
PEq t =>
Term s t -> Term s t -> Term s PBool
#== Term s PStakeDatum
expectedDatum

                    let valueDelta :: Term _ (PValue _ 'Positive)
                        valueDelta :: Term s (PValue w 'Positive)
valueDelta = Tagged @Type GTTag AssetClass
-> Term s (PDiscrete @Type GTTag :--> PValue w 'Positive)
forall tag (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Tagged @Type tag AssetClass
-> Term s (PDiscrete @Type tag :--> PValue keys amounts)
pdiscreteValue' Stake
stake.gtClassRef Term s (PDiscrete @Type GTTag :--> PValue w 'Positive)
-> Term s (PDiscrete @Type GTTag) -> Term s (PValue w 'Positive)
forall (s :: S) (a :: PType) (b :: PType).
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDiscrete @Type GTTag)
delta

                        expectedValue :: Term s (PValue 'Sorted 'Positive)
expectedValue =
                          Term s (PValue 'Sorted 'Positive)
continuingValue Term s (PValue 'Sorted 'Positive)
-> Term s (PValue 'Sorted 'Positive)
-> Term s (PValue 'Sorted 'Positive)
forall a. Semigroup a => a -> a -> a
<> Term s (PValue 'Sorted 'Positive)
forall {w :: KeyGuarantees}. Term s (PValue w 'Positive)
valueDelta

                        valueCorrect :: Term s PBool
valueCorrect =
                          (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
(#&&)
                            [ AssetClass
-> Term
     s
     (PValue 'Sorted 'Positive
      :--> (PValue 'Sorted 'Positive :--> PBool))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
AssetClass
-> Term
     s (PValue keys amounts :--> (PValue keys amounts :--> PBool))
pgeqByClass' ((CurrencySymbol, TokenName) -> AssetClass
AssetClass (CurrencySymbol
"", TokenName
""))
                                # ownOutputValue
                                # expectedValue
                            , AssetClass
-> Term
     s
     (PValue 'Sorted 'Positive
      :--> (PValue 'Sorted 'Positive :--> PBool))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
AssetClass
-> Term
     s (PValue keys amounts :--> (PValue keys amounts :--> PBool))
pgeqByClass' (Tagged @Type GTTag AssetClass -> AssetClass
forall {k} (s :: k) b. Tagged @k s b -> b
untag Stake
stake.gtClassRef)
                                # ownOutputValue
                                # expectedValue
                            , Term
  s
  (PCurrencySymbol
   :--> (PValue 'Sorted 'Positive
         :--> (PValue 'Sorted 'Positive :--> PBool)))
forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees)
       (s :: S).
Term
  s
  (PCurrencySymbol
   :--> (PValue keys amounts :--> (PValue keys amounts :--> PBool)))
pgeqBySymbol
                                # stCurrencySymbol
                                # ownOutputValue
                                # expectedValue
                            ]
                    --
                    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
foldl1
                        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)
"valueCorrect" Term s PBool
valueCorrect
                        , 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)
"datumCorrect" Term s PBool
datumCorrect
                        ]
                --
                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 (PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ())
              PStakeRedeemer s
_ -> Term s (PUnit @S) -> Term s POpaque
forall (s :: S) (a :: PType). Term s a -> Term s POpaque
popaque (PLifted (PUnit @S) -> Term s (PUnit @S)
forall (p :: PType) (s :: S). PLift p => PLifted p -> Term s p
pconstant ())