allow spending more than one stakes in one tx

2022-09-23 14:41:58 +08:00 · 2022-09-23 14:41:58 +08:00 · dd05ab45ca
commit dd05ab45ca
parent b876774921
6 changed files with 397 additions and 325 deletions
--- a/agora-specs/Sample/Stake.hs
+++ b/agora-specs/Sample/Stake.hs
@ -138,7 +138,6 @@ stakeDepositWithdraw config =
        mconcat
          [ txId "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
          , signedWith signer
-          , mint st
          , input $
              mconcat
                [ script stakeValidatorHash
@ -147,7 +146,7 @@ stakeDepositWithdraw config =
                        st
                          <> Value.assetClassValue (untag governor.gtClassRef) (fromDiscrete stakeBefore.stakedAmount)
                    )
-                , withDatum stakeAfter
+                , withDatum stakeBefore
                , withRef stakeRef
                ]
          , output $
--- a/agora/Agora/Stake.hs
+++ b/agora/Agora/Stake.hs
@ -21,8 +21,7 @@ module Agora.Stake (
  PStakeRole (..),

  -- * Validation context
-  PStakeInputContext (..),
-  PStakeOutputContext (..),
+  PSignedBy (..),
  PSigContext (..),
  PStakeRedeemerContext (..),
  PStakeRedeemerHandlerContext (..),
@ -43,14 +42,18 @@ module Agora.Stake (
  runStakeRedeemerHandler,
 ) where

-import Agora.Proposal (PProposalId, PProposalRedeemer, PResultTag, ProposalId, ResultTag)
+import Agora.Proposal (
+  PProposalId,
+  PProposalRedeemer,
+  PResultTag,
+  ProposalId,
+  ResultTag,
+ )
 import Agora.SafeMoney (GTTag)
 import Data.Tagged (Tagged)
 import Generics.SOP qualified as SOP
-import Plutarch.Api.V1 (KeyGuarantees (Sorted), PCredential)
-import Plutarch.Api.V1.Value (PValue)
+import Plutarch.Api.V1 (PCredential)
 import Plutarch.Api.V2 (
-  AmountGuarantees (Positive),
  PMaybeData,
  PTxInfo,
 )
@ -58,7 +61,6 @@ import Plutarch.DataRepr (
  DerivePConstantViaData (DerivePConstantViaData),
  PDataFields,
 )
-import Plutarch.Extra.AssetClass (PAssetClass)
 import Plutarch.Extra.Field (pletAll)
 import Plutarch.Extra.IsData (
  DerivePConstantViaDataList (DerivePConstantViaDataList),
@ -429,61 +431,11 @@ instance DerivePlutusType PStakeRole where

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

-{- | Represent the stake being spent.
-
-     @since 1.0.0
-}
-data PStakeInputContext (s :: S) = PStakeInput
-  { ownInputDatum :: Term s PStakeDatum
-  -- ^ The stake datum of said stake.
-  , ownInputValue :: Term s (PValue 'Sorted 'Positive)
-  -- ^ The value carried by the stake UTxO.
-  }
-  deriving stock
-    ( -- | @since 1.0.0
-      Generic
-    )
-  deriving anyclass
-    ( -- | @since 1.0.0
-      PlutusType
-    )
-
-- | @since 1.0.0
-instance DerivePlutusType PStakeInputContext where
-  type DPTStrat _ = PlutusTypeScott
-
-{- | Where the stake will go?
-
-     @since 1.0.0
-}
-data PStakeOutputContext (s :: S)
-  = -- | The output stake is owned by the stake validator.
-    PStakeOutput
-      { ownOutputDatum :: Term s PStakeDatum
-      -- ^ The stake datum of the output stake.
-      , ownOutputValue :: Term s (PValue 'Sorted 'Positive)
-      -- ^ The value carried by the stake output UTxO.
-      }
-  | -- | The stake is burnt in the transaction.
-    PStakeBurnt
-  deriving stock
-    ( -- | @since 1.0.0
-      Generic
-    )
-  deriving anyclass
-    ( -- | @since 1.0.0
-      PlutusType
-    )
-
-- | @since 1.0.0
-instance DerivePlutusType PStakeOutputContext where
-  type DPTStrat _ = PlutusTypeScott
-
 {- | Who authorizes the transaction?

     @since 1.0.0
 -}
-data PSigContext (s :: S)
+data PSignedBy (s :: S)
  = -- | The stake owner authorized the transaction.
    PSignedByOwner
  | -- | The delegate authorized the transaction.
@ -499,6 +451,25 @@ data PSigContext (s :: S)
      PlutusType
    )

+-- | @since 1.0.0
+instance DerivePlutusType PSignedBy where
+  type DPTStrat _ = PlutusTypeScott
+
+-- | @since 1.0.0
+data PSigContext (s :: S) = PSigContext
+  { owner :: Term s PCredential
+  , delegate :: Term s (PMaybeData (PAsData PCredential))
+  , signedBy :: Term s PSignedBy
+  }
+  deriving stock
+    ( -- | @since 1.0.0
+      Generic
+    )
+  deriving anyclass
+    ( -- | @since 1.0.0
+      PlutusType
+    )
+
 -- | @since 1.0.0
 instance DerivePlutusType PSigContext where
  type DPTStrat _ = PlutusTypeScott
@ -555,12 +526,11 @@ instance DerivePlutusType PProposalContext where
     @1.0.0
 -}
 data PStakeRedeemerHandlerContext (s :: S) = PStakeRedeemerHandlerContext
-  { stakeInput :: Term s PStakeInputContext
-  , stakeOutput :: Term s PStakeOutputContext
+  { stakeInputDatums :: Term s (PBuiltinList PStakeDatum)
+  , stakeOutputDatums :: Term s (PBuiltinList PStakeDatum)
  , redeemerContext :: Term s PStakeRedeemerContext
  , sigContext :: Term s PSigContext
  , proposalContext :: Term s PProposalContext
-  , gtAssetClass :: Term s PAssetClass
  , extraTxContext :: Term s PTxInfo
  }
  deriving stock
@ -589,9 +559,13 @@ type PStakeRedeemerHandler = PStakeRedeemerHandlerContext :--> PUnit

     @since 1.0.0
 -}
-newtype PStakeRedeemerHandlerTerm = PStakeRedeemerHandlerTerm (ClosedTerm PStakeRedeemerHandler)
+newtype PStakeRedeemerHandlerTerm
+  = PStakeRedeemerHandlerTerm
+      (ClosedTerm PStakeRedeemerHandler)

-runStakeRedeemerHandler :: PStakeRedeemerHandlerTerm -> ClosedTerm PStakeRedeemerHandler
+runStakeRedeemerHandler ::
+  PStakeRedeemerHandlerTerm ->
+  ClosedTerm PStakeRedeemerHandler
 runStakeRedeemerHandler (PStakeRedeemerHandlerTerm t) = t

 {- | A collection of stake redeemer handlers for each stake redeemers.
@ -666,7 +640,14 @@ pisIrrelevant = phoistAcyclic $

     @since 0.2.0
 -}
-pgetStakeRole :: forall (s :: S). Term s (PProposalId :--> PBuiltinList (PAsData PProposalLock) :--> PStakeRole)
+pgetStakeRole ::
+  forall (s :: S).
+  Term
+    s
+    ( PProposalId
+        :--> PBuiltinList (PAsData PProposalLock)
+        :--> PStakeRole
+    )
 pgetStakeRole = phoistAcyclic $
  plam $ \pid locks ->
    pfoldl
@ -688,7 +669,14 @@ pgetStakeRole = phoistAcyclic $
      # pcon PIrrelevant
      # locks
  where
-    pcombineStakeRole :: forall (s :: S). Term s (PStakeRole :--> PStakeRole :--> PStakeRole)
+    pcombineStakeRole ::
+      forall (s :: S).
+      Term
+        s
+        ( PStakeRole
+            :--> PStakeRole
+            :--> PStakeRole
+        )
    pcombineStakeRole = phoistAcyclic $
      plam $ \x y ->
        let cannotCombine = ptraceError "duplicate roles"
--- a/agora/Agora/Stake/Redeemers.hs
+++ b/agora/Agora/Stake/Redeemers.hs
@ -16,75 +16,96 @@ module Agora.Stake.Redeemers (

 import Agora.Proposal (PProposalRedeemer (PUnlock, PVote))
 import Agora.Stake (
-  PProposalContext (PNewProposal, PWithProposalRedeemer),
-  PSigContext (PSignedByOwner, PUnknownSig),
+  PProposalContext (
+    PNewProposal,
+    PWithProposalRedeemer
+  ),
+  PSigContext (owner, signedBy),
+  PSignedBy (
+    PSignedByDelegate,
+    PSignedByOwner,
+    PUnknownSig
+  ),
  PStakeDatum (PStakeDatum),
-  PStakeInputContext (PStakeInput),
-  PStakeOutputContext (PStakeBurnt, PStakeOutput),
-  PStakeRedeemerContext (PDepositWithdrawDelta, PNoMetadata, PSetDelegateTo),
+  PStakeRedeemerContext (
+    PDepositWithdrawDelta,
+    PNoMetadata,
+    PSetDelegateTo
+  ),
  PStakeRedeemerHandler,
-  PStakeRedeemerHandlerContext (..),
+  PStakeRedeemerHandlerContext (
+    proposalContext,
+    redeemerContext,
+    sigContext,
+    stakeInputDatums,
+    stakeOutputDatums
+  ),
  pstakeLocked,
 )
+import Agora.Utils (pdeleteBy, pfromSingleton)
 import Plutarch.Api.V1.Address (PCredential)
-import Plutarch.Api.V1.Value (AmountGuarantees (Positive), PValue)
 import Plutarch.Api.V2 (PMaybeData)
-import Plutarch.Extra.Field (pletAllC)
+import Plutarch.Extra.Field (pletAll, pletAllC)
 import Plutarch.Extra.Maybe (pdjust, pdnothing, pmaybeData)
 import Plutarch.Extra.Record (mkRecordConstr, (.&), (.=))
 import "liqwid-plutarch-extra" Plutarch.Extra.TermCont (pguardC, pletC, pmatchC)
-import Plutarch.Extra.Value (pgeqByClass, pgeqByClass')
 import Plutarch.Numeric.Additive (AdditiveMonoid (zero), AdditiveSemigroup ((+)))
-import Plutarch.SafeMoney (pdiscreteValue)
-import PlutusLedgerApi.V1.Value (AssetClass (..))
 import Prelude hiding (Num ((+)))

-- | Return true if stake input and output carries the same value.
-pownOutputValueUnchanged ::
+pbatchUpdateInputs ::
  forall (s :: S).
-  Term s (PStakeRedeemerHandlerContext :--> PBool)
-pownOutputValueUnchanged = phoistAcyclic $
-  plam $
-    flip pmatch $ \ctxF -> unTermCont $ do
-      PStakeInput _ inVal <- pmatchC ctxF.stakeInput
-      PStakeOutput _ outVal <- pmatchC ctxF.stakeOutput
+  Term
+    s
+    ( (PStakeDatum :--> PStakeDatum :--> PBool)
+        :--> PStakeRedeemerHandlerContext
+        :--> PBool
+    )
+pbatchUpdateInputs = phoistAcyclic $
+  plam $ \f -> flip pmatch $ \ctxF ->
+    pnull #$ pfoldr
+      # (pdeleteBy # f)
+      # ctxF.stakeOutputDatums
+      # ctxF.stakeInputDatums

-      pure $ inVal #== outVal
+pgetSignedBy ::
+  forall (s :: S).
+  Term
+    s
+    (PStakeRedeemerHandlerContext :--> PSignedBy)
+pgetSignedBy = phoistAcyclic $
+  plam $ \ctx -> unTermCont $ do
+    ctxF <- pmatchC ctx
+    sctxF <- pmatchC ctxF.sigContext
+    pure sctxF.signedBy
+
+pisSignedBy ::
+  forall (s :: S).
+  Term
+    s
+    (PBool :--> PBool :--> PStakeRedeemerHandlerContext :--> PBool)
+pisSignedBy = phoistAcyclic $
+  plam $ \byOwner byDelegate ctx ->
+    pmatch (pgetSignedBy # ctx) $ \case
+      PSignedByOwner -> byOwner
+      PSignedByDelegate -> byDelegate
+      PUnknownSig -> pconstant False

 -- | Return true if only the @lockedBy@ field of the stake datum is updated.
 ponlyLocksUpdated ::
  forall (s :: S).
  Term s (PStakeRedeemerHandlerContext :--> PBool)
 ponlyLocksUpdated = phoistAcyclic $
-  plam $
-    flip pmatch $ \ctxF -> unTermCont $ do
-      PStakeInput inDat _ <- pmatchC ctxF.stakeInput
-      PStakeOutput outDat _ <- pmatchC ctxF.stakeOutput
-
-      inDatF <- pletAllC inDat
-
-      let onlyLocksUpdated =
-            let templateStakeDatum =
-                  mkRecordConstr
-                    PStakeDatum
-                    ( #stakedAmount .= inDatF.stakedAmount
-                        .& #owner .= inDatF.owner
-                        .& #delegatedTo .= inDatF.delegatedTo
-                        .& #lockedBy .= pfield @"lockedBy" # outDat
-                    )
-             in outDat #== templateStakeDatum
-
-      pure onlyLocksUpdated
-
-- | Return true if the transaction is signed by the owner of the stake.
-psignedByOwner ::
-  forall (s :: S).
-  Term s (PStakeRedeemerHandlerContext :--> PBool)
-psignedByOwner = phoistAcyclic $
-  plam $
-    flip pmatch $ \ctxF -> pmatch ctxF.sigContext $ \case
-      PSignedByOwner -> pconstant True
-      _ -> pconstant False
+  pbatchUpdateInputs #$ plam $ \i o ->
+    pletAll i $ \iF ->
+      let newLocks = pfield @"lockedBy" # o
+       in mkRecordConstr
+            PStakeDatum
+            ( #stakedAmount .= iF.stakedAmount
+                .& #owner .= iF.owner
+                .& #delegatedTo .= iF.delegatedTo
+                .& #lockedBy .= newLocks
+            )
+            #== o

 -- | Validation logic shared between 'ppermitVote' and 'retractVote'.
 pvoteHelper ::
@ -99,9 +120,7 @@ pvoteHelper = phoistAcyclic $
    ctxF <- pmatchC ctx

    pguardC "Owner or delegate signs this transaction" $
-      pmatch ctxF.sigContext $ \case
-        PUnknownSig -> pconstant False
-        _ -> pconstant True
+      pisSignedBy # pconstant True # pconstant True # ctx

    -- This puts trust into the Proposal. The Proposal must necessarily check
    -- that this is not abused.
@ -109,14 +128,8 @@ pvoteHelper = phoistAcyclic $
    pguardC "Proposal ST spent" $
      valProposalCtx # ctxF.proposalContext

-    pguardC "A UTXO must exist with the correct output" $
-      let valueCorrect = pownOutputValueUnchanged # ctx
-          outputDatumCorrect = ponlyLocksUpdated # ctx
-       in foldl1
-            (#&&)
-            [ ptraceIfFalse "valueCorrect" valueCorrect
-            , ptraceIfFalse "datumCorrect" outputDatumCorrect
-            ]
+    pguardC "Correct outputs" $
+      ponlyLocksUpdated # ctx

    pure $ pconstant ()

@ -158,38 +171,33 @@ pdelegateHelper ::
 pdelegateHelper = phoistAcyclic $
  plam $ \f ctx -> unTermCont $ do
    ctxF <- pmatchC ctx
+    sigCtxF <- pmatchC ctxF.sigContext

-    pguardC "Owner signs this transaction" $ psignedByOwner # ctx
+    pguardC "Owner signs this transaction" $
+      pisSignedBy # pconstant True # pconstant False # ctx

-    PStakeInput inpDat _ <- pmatchC ctxF.stakeInput
-    PStakeOutput outDat _ <- pmatchC ctxF.stakeOutput
-
-    inpDatF <- pletAllC inpDat
-
-    let maybePkh = f # ctxF.redeemerContext
+    let newDelegate = f # ctxF.redeemerContext

    pguardC "Cannot delegate to the owner" $
      pmaybeData
        # pcon PTrue
-        # plam (\pkh -> pnot #$ inpDatF.owner #== pkh)
-        # maybePkh
+        # plam (\pkh -> pnot #$ sigCtxF.owner #== pfromData pkh)
+        # newDelegate

-    pguardC "A UTXO must exist with the correct output" $
-      let correctOutputDatum =
-            outDat
-              #== mkRecordConstr
+    pguardC "Correct outputs" $
+      pbatchUpdateInputs
+        # plam
+          ( \i o -> pletAll i $ \iF ->
+              mkRecordConstr
                PStakeDatum
-                ( #stakedAmount .= inpDatF.stakedAmount
-                    .& #owner .= inpDatF.owner
-                    .& #delegatedTo .= pdata maybePkh
-                    .& #lockedBy .= inpDatF.lockedBy
+                ( #stakedAmount .= iF.stakedAmount
+                    .& #owner .= iF.owner
+                    .& #delegatedTo .= pdata newDelegate
+                    .& #lockedBy .= iF.lockedBy
                )
-          valueCorrect = pownOutputValueUnchanged # ctx
-       in foldl1
-            (#&&)
-            [ ptraceIfFalse "valueCorrect" valueCorrect
-            , ptraceIfFalse "datumCorrect" correctOutputDatum
-            ]
+                #== o
+          )
+        # ctx

    pure $ pconstant ()

@ -224,13 +232,11 @@ pdestroy = phoistAcyclic $
  plam $ \ctx -> unTermCont $ do
    ctxF <- pmatchC ctx

-    PStakeInput inpDat _ <- pmatchC ctxF.stakeInput
-    PStakeBurnt <- pmatchC ctxF.stakeOutput
-
    pguardC "Owner signs this transaction" $
-      psignedByOwner # ctx
+      pisSignedBy # pconstant True # pconstant False # ctx

-    pguardC "Stake unlocked" $ pnot #$ pstakeLocked # inpDat
+    pguardC "Stake unlocked" $
+      pnot #$ pany # pstakeLocked # ctxF.stakeInputDatums

    pure $ pconstant ()

@ -243,61 +249,43 @@ pdepositWithdraw = phoistAcyclic $
  plam $ \ctx -> unTermCont $ do
    ctxF <- pmatchC ctx

-    PStakeInput inpDat inpVal <- pmatchC ctxF.stakeInput
-    PStakeOutput outDat outVal <- pmatchC ctxF.stakeOutput
+    pguardC "Owner signs this transaction" $
+      pisSignedBy # pconstant True # pconstant False # ctx

-    pguardC "Stake unlocked" $ pnot #$ pstakeLocked # inpDat
+    ----------------------------------------------------------------------------

-    pguardC "Owner signs this transaction" $ psignedByOwner # ctx
+    stakeInputDatum <-
+      pletC $
+        ptrace "Single stake input" $
+          pfromSingleton # ctxF.stakeInputDatums
+    stakeInputDatumF <- pletAllC stakeInputDatum

-    pguardC
-      "A UTXO must exist with the correct output"
-      $ unTermCont $ do
-        inpDatF <- pletAllC inpDat
-        PDepositWithdrawDelta delta <- pmatchC ctxF.redeemerContext
+    let stakeOutputDatum =
+          ptrace "Single stake output" $
+            pfromSingleton # ctxF.stakeOutputDatums

-        let oldStakedAmount = pfromData $ inpDatF.stakedAmount
+    ----------------------------------------------------------------------------

-        newStakedAmount <- pletC $ oldStakedAmount + delta
+    pguardC "Stake unlocked" $
+      pnot #$ pstakeLocked # stakeInputDatum

-        pguardC "New staked amount should be greater than or equal to 0" $
-          zero #<= newStakedAmount
+    ----------------------------------------------------------------------------

-        let expectedDatum =
-              mkRecordConstr
-                PStakeDatum
-                ( #stakedAmount .= pdata newStakedAmount
-                    .& #owner .= inpDatF.owner
-                    .& #delegatedTo .= inpDatF.delegatedTo
-                    .& #lockedBy .= inpDatF.lockedBy
-                )
-            datumCorrect = outDat #== expectedDatum
+    PDepositWithdrawDelta delta <- pmatchC ctxF.redeemerContext

-        let valueDelta :: Term _ (PValue _ 'Positive)
-            valueDelta = pdiscreteValue # ctxF.gtAssetClass # delta
+    newStakedAmount <- pletC $ stakeInputDatumF.stakedAmount + delta

-            expectedValue =
-              inpVal <> valueDelta
+    pguardC "Non-negative staked amount" $ zero #<= newStakedAmount

-        gtAssetClassF <- pletAllC ctxF.gtAssetClass
+    let expectedDatum =
+          mkRecordConstr
+            PStakeDatum
+            ( #stakedAmount .= pdata newStakedAmount
+                .& #owner .= stakeInputDatumF.owner
+                .& #delegatedTo .= stakeInputDatumF.delegatedTo
+                .& #lockedBy .= stakeInputDatumF.lockedBy
+            )
+
+    pguardC "Valid output datum" $ expectedDatum #== stakeOutputDatum

-        let valueCorrect =
-              foldr1
-                (#&&)
-                [ pgeqByClass' (AssetClass ("", ""))
-                    # outVal
-                    # expectedValue
-                , pgeqByClass
-                    # gtAssetClassF.currencySymbol
-                    # gtAssetClassF.tokenName
-                    # outVal
-                    # expectedValue
-                ]
-        --
-        pure $
-          foldl1
-            (#&&)
-            [ ptraceIfFalse "valueCorrect" valueCorrect
-            , ptraceIfFalse "datumCorrect" datumCorrect
-            ]
    pure $ pconstant ()
--- a/agora/Agora/Stake/Scripts.hs
+++ b/agora/Agora/Stake/Scripts.hs
@ -25,15 +25,21 @@ import Agora.Stake (
    PNoProposal,
    PWithProposalRedeemer
  ),
-  PSigContext (
+  PSigContext (PSigContext),
+  PSignedBy (
    PSignedByDelegate,
    PSignedByOwner,
    PUnknownSig
  ),
  PStakeDatum,
-  PStakeInputContext (PStakeInput),
-  PStakeOutputContext (PStakeBurnt, PStakeOutput),
-  PStakeRedeemer (PClearDelegate, PDelegateTo, PDepositWithdraw, PDestroy, PPermitVote, PRetractVotes),
+  PStakeRedeemer (
+    PClearDelegate,
+    PDelegateTo,
+    PDepositWithdraw,
+    PDestroy,
+    PPermitVote,
+    PRetractVotes
+  ),
  PStakeRedeemerContext (
    PDepositWithdrawDelta,
    PNoMetadata,
@ -57,15 +63,19 @@ import Agora.Stake.Redeemers (
 )
 import Data.Tagged (Tagged (Tagged))
 import Plutarch.Api.V1 (
+  KeyGuarantees (Sorted),
  PCredential (PPubKeyCredential, PScriptCredential),
  PTokenName,
 )
 import Plutarch.Api.V1.AssocMap (plookup)
+import Plutarch.Api.V1.Value (PValue)
 import Plutarch.Api.V2 (
+  AmountGuarantees,
  PMintingPolicy,
  PScriptPurpose (PMinting, PSpending),
  PTxInInfo,
  PTxInfo,
+  PTxOut,
  PTxOutRef,
  PValidator,
 )
@ -75,8 +85,9 @@ import Plutarch.Extra.AssetClass (
  pvalueOf,
 )
 import Plutarch.Extra.Bind (PBind ((#>>=)))
-import Plutarch.Extra.Field (pletAllC)
-import "liqwid-plutarch-extra" Plutarch.Extra.List (pfindJust)
+import Plutarch.Extra.Category (PSemigroupoid ((#>>>)))
+import Plutarch.Extra.Functor (PFunctor (pfmap))
+import "liqwid-plutarch-extra" Plutarch.Extra.List (pfindJust, pmapMaybe)
 import Plutarch.Extra.Maybe (
  passertPJust,
  pjust,
@ -100,6 +111,7 @@ import Plutarch.Extra.Value (
  psymbolValueOf,
 )
 import Plutarch.SafeMoney (
+  pvalueDiscrete,
  pvalueDiscrete',
 )
 import Plutarch.Unsafe (punsafeCoerce)
@ -235,8 +247,14 @@ mkStakeValidator
  impl
  as
  (Tagged (AssetClass (gtSym, gtTn))) =
-    plam $ \datum redeemer ctx -> unTermCont $ do
-      gtAssetClass <- pletC $ passetClass # pconstant gtSym # pconstant gtTn
+    plam $ \_datum redeemer ctx -> unTermCont $ do
+      let sstValueOf ::
+            ( forall (ag :: AmountGuarantees) (s :: S).
+              Term s (PValue 'Sorted ag :--> PInteger)
+            )
+          sstValueOf =
+            phoistAcyclic $
+              psymbolValueOf # pconstant (stakeSTSymbol as)

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

@ -257,118 +275,138 @@ mkStakeValidator

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

-      -- Assemble the stake input context.
-
-      stakeInputDatum <- pfromData . fst <$> ptryFromC datum
-      stakeInputDatumF <- pletAllC $ pto stakeInputDatum
-
      PSpending stakeInputRef <- pmatchC $ pfromData ctxF.purpose

-      -- The UTxO we are validating, which is also the input stake.
-      stakeInput <-
-        pletC $
-          pfield @"resolved"
-            #$ passertPJust # "Malformed script context: own input not found"
-            #$ pfindTxInByTxOutRef
-              # (pfield @"_0" # stakeInputRef)
-              # txInfoF.inputs
+      let validatedInput =
+            pfield @"resolved"
+              #$ passertPJust
+                # "Malformed script context: validated input not found"
+              #$ pfindTxInByTxOutRef
+                # (pfield @"_0" # stakeInputRef)
+                # txInfoF.inputs

-      stakeInputF <- pletFieldsC @'["address", "value"] stakeInput
-
-      stakeInputContext <-
-        pletC $
-          pcon $
-            PStakeInput
-              stakeInputDatum
-              stakeInputF.value
+          stakeValidatorAddress = pfield @"address" # validatedInput

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

-      -- Assemble the signature context.
+      getStakeDatum :: Term _ (PTxOut :--> PMaybe PStakeDatum) <-
+        pletC $
+          plam $ \txOut -> unTermCont $ do
+            txOutF <- pletFieldsC @'["value", "datum", "address"] txOut

-      signedBy <- pletC $ pauthorizedBy # authorizationContext txInfoF
+            let isStakeUTxO =
+                  foldl1
+                    (#&&)
+                    [ ptraceIfFalse "Carries SST" $
+                        sstValueOf # txOutF.value #== 1
+                    , ptraceIfFalse "Owned by stake validator" $
+                        txOutF.address #== stakeValidatorAddress
+                    ]

-      let ownerSignsTransaction = signedBy # stakeInputDatumF.owner
+                datum =
+                  ptrace "Resolve stake datum" $
+                    pfromData $
+                      pfromOutputDatum @(PAsData PStakeDatum)
+                        # txOutF.datum
+                        # txInfoF.datums
+
+            pure $ pif isStakeUTxO (pjust # datum) pnothing
+
+      --------------------------------------------------------------------------
+
+      stakeInputDatums <-
+        pletC $
+          pmapMaybe
+            # ((pfield @"resolved") #>>> getStakeDatum)
+            # pfromData txInfoF.inputs
+
+      --------------------------------------------------------------------------
+
+      firstStakeInputDatumF <-
+        pletFieldsC @'["owner", "delegatedTo"] $
+          phead # stakeInputDatums
+
+      restOfStakeInputDatums <- pletC $ ptail # stakeInputDatums
+
+      pguardC "All input stakes have the same owner or delegate" $
+        let allHaveSameOwner =
+              pall
+                # ( (pfield @"owner")
+                      #>>> plam (#== firstStakeInputDatumF.owner)
+                  )
+                # restOfStakeInputDatums
+            allHaveSameDelegate =
+              pall
+                # ( (pfield @"delegatedTo")
+                      #>>> plam (#== firstStakeInputDatumF.delegatedTo)
+                  )
+                # restOfStakeInputDatums
+         in allHaveSameOwner #|| allHaveSameDelegate
+
+      authorizedBy <- pletC $ pauthorizedBy # authorizationContext txInfoF
+
+      let ownerSignsTransaction = authorizedBy # firstStakeInputDatumF.owner

          delegateSignsTransaction =
            pmaybeData
              # pconstant False
-              # plam ((signedBy #) . pfromData)
-              # pfromData stakeInputDatumF.delegatedTo
+              # plam ((authorizedBy #) . pfromData)
+              # pfromData firstStakeInputDatumF.delegatedTo
+
+          signedBy =
+            pif
+              ownerSignsTransaction
+              (pcon PSignedByOwner)
+              $ pif
+                delegateSignsTransaction
+                (pcon PSignedByDelegate)
+                $ pcon PUnknownSig

      sigContext <-
        pletC $
-          pif ownerSignsTransaction (pcon PSignedByOwner) $
-            pif delegateSignsTransaction (pcon PSignedByDelegate) $
-              pcon PUnknownSig
+          pcon $
+            PSigContext
+              firstStakeInputDatumF.owner
+              firstStakeInputDatumF.delegatedTo
+              signedBy

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

-      stCurrencySymbol <- pletC $ pconstant $ stakeSTSymbol as
-      mintedST <- pletC $ psymbolValueOf # stCurrencySymbol # txInfoF.mint
-      valueSpent <- pletC $ pvalueSpent # txInfoF.inputs
-      spentST <- pletC $ psymbolValueOf # stCurrencySymbol #$ valueSpent
+      let gtAssetClass = passetClass # pconstant gtSym # pconstant gtTn

-      -- The stake validator can only handle one stake in one transaction.
-
-      pguardC "ST at inputs must be 1" $
-        spentST #== 1
-
-      let oneStakeBurnt =
-            ptraceIfFalse "Exactly one stake st burnt" $
-              mintedST #== (-1)
-
-      --------------------------------------------------------------------------
-
-      -- Assemble the stake output context.
-
-      let -- Look for the output stake.
-          stakeOutput =
-            pfindJust
-              # plam
-                ( \output -> unTermCont $ do
-                    outputF <-
-                      pletFieldsC @'["address", "value", "datum"]
-                        output
-
-                    let isStakeOutput =
-                          -- The stake should be owned by the stake validator.
-                          outputF.address #== stakeInputF.address
-                            #&&
-                            -- The stake UTxO carries the state thread token.
-                            psymbolValueOf
-                              # stCurrencySymbol
-                              # outputF.value #== 1
-
-                        stakeOutputDatum =
-                          pfromOutputDatum
-                            # outputF.datum
-                            # txInfoF.datums
-
-                        context =
-                          pcon $
-                            PStakeOutput
-                              (pfromData stakeOutputDatum)
-                              outputF.value
-
-                    pure $
-                      pif
-                        isStakeOutput
-                        (pjust # context)
-                        pnothing
-                )
-              # pfromData txInfoF.outputs
-
-      stakeOutputContext <-
+      stakeOutputDatums <-
        pletC $
-          pmatch stakeOutput $ \case
-            -- Stake output found.
-            PJust stakeOutput' -> stakeOutput'
-            -- Stake output not found, meaning the input stake should be burnt.
-            PNothing -> unTermCont $ do
-              pguardC "One stake should be burnt" oneStakeBurnt
+          pmapMaybe
+            # plam
+              ( \output ->
+                  let validateGT = plam $ \stakeDatum ->
+                        let expected = pfield @"stakedAmount" # stakeDatum
+                            actual =
+                              pvalueDiscrete
+                                # gtAssetClass
+                                # (pfield @"value" # output)
+                         in pif
+                              (expected #== actual)
+                              stakeDatum
+                              (ptraceError "Unmatched GT value")
+                   in pfmap
+                        # validateGT
+                        # (getStakeDatum # output)
+              )
+            # pfromData txInfoF.outputs

-              pure $ pcon PStakeBurnt
+      --------------------------------------------------------------------------
+
+      mintedST <- pletC $ sstValueOf # txInfoF.mint
+
+      pguardC "No new SST minted" $
+        foldl1
+          (#||)
+          [ ptraceIfFalse "All stakes burnt" $
+              mintedST #< 0 #&& pnull # stakeOutputDatums
+          , ptraceIfFalse "Nothing burnt" $
+              mintedST #== 0
+          ]

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

@ -427,12 +465,11 @@ mkStakeValidator
        plam $ \redeemerContext ->
          pcon $
            PStakeRedeemerHandlerContext
-              stakeInputContext
-              stakeOutputContext
+              stakeInputDatums
+              stakeOutputDatums
              redeemerContext
              sigContext
              proposalContext
-              gtAssetClass
              txInfo

      noMetadataContext <-
--- a/agora/Agora/Utils.hs
+++ b/agora/Agora/Utils.hs
@ -22,13 +22,15 @@ module Agora.Utils (
  pstringIntercalate,
  punwords,
  pcurrentTimeDuration,
+  pdelete,
+  pdeleteBy,
+  pisSingleton,
+  pfromSingleton,
 ) where

 import Plutarch.Api.V1 (PPOSIXTime, PTokenName, PValidatorHash)
 import Plutarch.Api.V2 (PScriptHash)
-import "liqwid-plutarch-extra" Plutarch.Extra.TermCont (pmatchC)
 import Plutarch.Extra.Time (PCurrentTime (PCurrentTime))
-import Plutarch.List (puncons)
 import Plutarch.Unsafe (punsafeCoerce)
 import PlutusLedgerApi.V2 (
  Address (Address),
@ -57,8 +59,8 @@ validatorHashToTokenName (ValidatorHash hash) = TokenName hash

     @since 1.0.0
 -}
-pvalidatorHashToTokenName :: forall (s :: S). Term s PValidatorHash -> Term s PTokenName
-pvalidatorHashToTokenName = punsafeCoerce
+pvalidatorHashToTokenName :: forall (s :: S). Term s (PValidatorHash :--> PTokenName)
+pvalidatorHashToTokenName = phoistAcyclic $ plam punsafeCoerce

 {- | Safely convert a 'PScriptHash' into a 'PTokenName'. This can be useful for tagging
     tokens for extra safety.
@ -145,21 +147,23 @@ plistEqualsBy ::
    (b :: PType)
    (s :: S).
  (PIsListLike list1 a, PIsListLike list2 b) =>
-  Term s ((a :--> b :--> PBool) :--> list1 a :--> (list2 b :--> PBool))
-plistEqualsBy = phoistAcyclic $ pfix # go
-  where
-    go = plam $ \self eq l1 l2 -> unTermCont $ do
-      l1' <- pmatchC $ puncons # l1
-      l2' <- pmatchC $ puncons # l2
-
-      case (l1', l2') of
-        (PJust l1'', PJust l2'') -> do
-          (PPair h1 t1) <- pmatchC l1''
-          (PPair h2 t2) <- pmatchC l2''
-
-          pure $ eq # h1 # h2 #&& self # eq # t1 # t2
-        (PNothing, PNothing) -> pure $ pconstant True
-        _ -> pure $ pconstant False
+  Term s ((a :--> b :--> PBool) :--> list1 a :--> list2 b :--> PBool)
+plistEqualsBy = phoistAcyclic $
+  plam $ \eq -> pfix #$ plam $ \self l1 l2 ->
+    pelimList
+      ( \x xs ->
+          pelimList
+            ( \y ys ->
+                -- Avoid comparison if two lists have different length.
+                self # xs # ys #&& eq # x # y
+            )
+            -- l2 is empty, but l1 is not.
+            (pconstant False)
+            l2
+      )
+      -- l1 is empty, so l2 should be empty as well.
+      (pnull # l2)
+      l1

 -- | @since 1.0.0
 pstringIntercalate ::
@ -190,3 +194,59 @@ pcurrentTimeDuration = phoistAcyclic $
  plam $
    flip pmatch $
      \(PCurrentTime lb ub) -> ub - lb
+
+{- | / O(n) /. Remove the first occurance of a value from the given list.
+
+     @since 1.0.0
+-}
+pdelete ::
+  forall (a :: PType) (list :: PType -> PType) (s :: S).
+  (PEq a, PIsListLike list a) =>
+  Term s (a :--> list a :--> list a)
+pdelete = phoistAcyclic $ pdeleteBy # plam (#==)
+
+-- | @since 1.0.0
+pdeleteBy ::
+  forall (a :: PType) (list :: PType -> PType) (s :: S).
+  (PIsListLike list a) =>
+  Term s ((a :--> a :--> PBool) :--> a :--> list a :--> list a)
+pdeleteBy = phoistAcyclic $
+  plam $ \f' x -> plet (f' # x) $ \f ->
+    precList
+      ( \self h t ->
+          pif
+            (f # h)
+            t
+            (pcons # h #$ self # t)
+      )
+      (const pnil)
+
+{- | / O(1) /.Return true if the given list has only one element.
+
+     @since 1.0.0
+-}
+pisSingleton ::
+  forall (a :: PType) (list :: PType -> PType) (s :: S).
+  (PIsListLike list a) =>
+  Term s (list a :--> PBool)
+pisSingleton =
+  phoistAcyclic $
+    precList
+      (\_ _ t -> pnull # t)
+      (const $ pconstant False)
+
+-- | @since 1.0.0
+pfromSingleton ::
+  forall (a :: PType) (list :: PType -> PType) (s :: S).
+  (PIsListLike list a) =>
+  Term s (list a :--> a)
+pfromSingleton =
+  phoistAcyclic $
+    precList
+      ( \_ h t ->
+          pif
+            (pnull # t)
+            h
+            (ptraceError "More than one element")
+      )
+      (const $ ptraceError "Empty list")
--- a/flake.lock
+++ b/flake.lock
@ -11979,17 +11979,17 @@
        "plutarch": "plutarch_15"
      },
      "locked": {
-        "lastModified": 1664028810,
+        "lastModified": 1664220695,
        "narHash": "sha256-thMEO1P/ciHjnMFyL0bla781TG5C/nB5EEtebb3Boik=",
        "owner": "Liqwid-Labs",
        "repo": "plutarch-script-export",
-        "rev": "4f0da58ba67cdcfe5c7d97e6e27dc00dfb71e657",
+        "rev": "eba175e63516a4fed43ceab1826ea6522f28dd0f",
        "type": "github"
      },
      "original": {
        "owner": "Liqwid-Labs",
+        "ref": "main",
        "repo": "plutarch-script-export",
-        "rev": "4f0da58ba67cdcfe5c7d97e6e27dc00dfb71e657",
        "type": "github"
      }
    },