diff --git a/agora-specs/Sample/Proposal.hs b/agora-specs/Sample/Proposal.hs
index 0ec892d..3aa30c7 100644
--- a/agora-specs/Sample/Proposal.hs
+++ b/agora-specs/Sample/Proposal.hs
@@ -16,9 +16,9 @@ module Sample.Proposal (
   advanceProposalSuccess,
   advanceProposalFailureTimeout,
   TransitionParameters (..),
-  advanceFinishedPropsoal,
+  advanceFinishedProposal,
   advanceProposalInsufficientVotes,
-  advancePropsoalWithsStake,
+  advanceProposalWithInvalidOutputStake,
 ) where
 
 import Agora.Governor (GovernorDatum (..))
@@ -78,11 +78,8 @@ import PlutusLedgerApi.V1.Value qualified as Value (
   assetClassValue,
   singleton,
  )
-import PlutusTx.AssocMap qualified as AssocMap (
-  Map,
-  empty,
-  fromList,
- )
+import PlutusTx.AssocMap qualified as AssocMap
+import Sample.Proposal.Shared (proposalRef, stakeRef)
 import Sample.Shared (
   govValidatorHash,
   minAda,
@@ -164,12 +161,6 @@ proposalCreation =
           ]
    in buildMintingUnsafe builder
 
-proposalRef :: TxOutRef
-proposalRef = TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1
-
-stakeRef :: TxOutRef
-stakeRef = TxOutRef "0ca36f3a357bc69579ab2531aecd1e7d3714d993c7820f40b864be15" 0
-
 -- | This script context should be a valid transaction.
 cosignProposal :: [PubKeyHash] -> TxInfo
 cosignProposal newSigners =
@@ -383,9 +374,9 @@ voteOnProposal params =
 
 -- | Parameters for state transition of proposals.
 data TransitionParameters = TransitionParameters
-  { -- The initial status of the propsoal.
+  { -- The initial status of the proposal.
     initialProposalStatus :: ProposalStatus
-  , -- The starting time of the propsoal.
+  , -- The starting time of the proposal.
     proposalStartingTime :: ProposalStartingTime
   }
 
@@ -403,9 +394,12 @@ mkTransitionTxInfo ::
   ProposalStartingTime ->
   -- | Valid time range of the transaction.
   POSIXTimeRange ->
+  -- | Whether to add an unchanged stake or not.
+  Bool ->
   TxInfo
-mkTransitionTxInfo from to effects votes startingTime validTime =
+mkTransitionTxInfo from to effects votes startingTime validTime shouldAddUnchangedStake =
   let pst = Value.singleton proposalPolicySymbol "" 1
+      sst = Value.assetClassValue stakeAssetClass 1
 
       proposalInputDatum :: ProposalDatum
       proposalInputDatum =
@@ -426,11 +420,48 @@ mkTransitionTxInfo from to effects votes startingTime validTime =
           { status = to
           }
 
+      stakeOwner = signer
+      stakedAmount = 200
+
+      existingLocks :: [ProposalLock]
+      existingLocks =
+        [ ProposalLock (ResultTag 0) (ProposalId 0)
+        , ProposalLock (ResultTag 2) (ProposalId 1)
+        ]
+
+      stakeInputDatum :: StakeDatum
+      stakeInputDatum =
+        StakeDatum
+          { stakedAmount = Tagged stakedAmount
+          , owner = stakeOwner
+          , lockedBy = existingLocks
+          }
+
+      stakeOutputDatum :: StakeDatum
+      stakeOutputDatum = stakeInputDatum
+
+      stakeBuilder :: BaseBuilder
+      stakeBuilder =
+        if shouldAddUnchangedStake
+          then
+            mconcat
+              [ input $
+                  script stakeValidatorHash
+                    . withValue sst
+                    . withDatum stakeInputDatum
+                    . withTxId (txOutRefId stakeRef)
+              , output $
+                  script stakeValidatorHash
+                    . withValue (sst <> minAda)
+                    . withDatum stakeOutputDatum
+              ]
+          else mempty
+
       builder :: BaseBuilder
       builder =
         mconcat
           [ txId "95ba4015e30aef16a3461ea97a779f814aeea6b8009d99a94add4b8293be737a"
-          , signedWith signer
+          , signedWith stakeOwner
           , timeRange validTime
           , input $
               script proposalValidatorHash
@@ -442,13 +473,19 @@ mkTransitionTxInfo from to effects votes startingTime validTime =
                 . withValue (pst <> minAda)
                 . withDatum proposalOutputDatum
           ]
-   in buildTxInfoUnsafe builder
+   in buildTxInfoUnsafe $ builder <> stakeBuilder
+
+-- | Wrapper around 'advanceProposalSuccess'', with valid stake.
+advanceProposalSuccess :: TransitionParameters -> TxInfo
+advanceProposalSuccess ps = advanceProposalSuccess' ps True
 
 {- | Create a valid 'TxInfo' that advances a proposal, given the parameters.
+     The second parameter determines wherther valid stake should be included.
+
      Note that 'TransitionParameters.initialProposalStatus' should not be 'Finished'.
 -}
-advanceProposalSuccess :: TransitionParameters -> TxInfo
-advanceProposalSuccess params =
+advanceProposalSuccess' :: TransitionParameters -> Bool -> TxInfo
+advanceProposalSuccess' params =
   let -- Status of the output proposal.
       toStatus :: ProposalStatus
       toStatus = case params.initialProposalStatus of
@@ -615,6 +652,7 @@ advanceProposalFailureTimeout params =
         votes
         params.proposalStartingTime
         timeRange
+        True
 
 -- | An invalid 'TxInfo' that tries to advance a 'VotingReady' proposal without sufficient votes.
 advanceProposalInsufficientVotes :: TxInfo
@@ -643,10 +681,11 @@ advanceProposalInsufficientVotes =
         votes
         (ProposalStartingTime proposalStartingTime)
         timeRange
+        True
 
 -- | An invalid 'TxInfo' that tries to advance a 'Finished' proposal.
-advanceFinishedPropsoal :: TxInfo
-advanceFinishedPropsoal =
+advanceFinishedProposal :: TxInfo
+advanceFinishedProposal =
   let effects =
         AssocMap.fromList
           [ (ResultTag 0, AssocMap.empty)
@@ -675,19 +714,21 @@ advanceFinishedPropsoal =
         outcome0WinningVotes
         (ProposalStartingTime 0)
         timeRange
+        True
 
-{- | An illegal 'TxInfo' that tries to use 'AdvanceProposal' with a stake.
-     From the perspective of stake validator, the transition is valid,
+{- | An illegal 'TxInfo' that tries to output a changed stake with 'AdvanceProposal'.
+     From the perspective of stake validator, the transition is totally valid,
        so the proposal validator should reject this.
 -}
-advancePropsoalWithsStake :: TxInfo
-advancePropsoalWithsStake =
+advanceProposalWithInvalidOutputStake :: TxInfo
+advanceProposalWithInvalidOutputStake =
   let templateTxInfo =
-        advanceProposalSuccess
+        advanceProposalSuccess'
           TransitionParameters
             { initialProposalStatus = VotingReady
             , proposalStartingTime = ProposalStartingTime 0
             }
+          False
 
       ---
       -- Now we create a new lock on an arbitrary stake
diff --git a/agora-specs/Sample/Proposal/Shared.hs b/agora-specs/Sample/Proposal/Shared.hs
new file mode 100644
index 0000000..1a2ee64
--- /dev/null
+++ b/agora-specs/Sample/Proposal/Shared.hs
@@ -0,0 +1,9 @@
+module Sample.Proposal.Shared (proposalRef, stakeRef) where
+
+import PlutusLedgerApi.V1 (TxOutRef (..))
+
+proposalRef :: TxOutRef
+proposalRef = TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1
+
+stakeRef :: TxOutRef
+stakeRef = TxOutRef "0ca36f3a357bc69579ab2531aecd1e7d3714d993c7820f40b864be15" 0
diff --git a/agora-specs/Sample/Proposal/UnlockStake.hs b/agora-specs/Sample/Proposal/UnlockStake.hs
new file mode 100644
index 0000000..d8ac396
--- /dev/null
+++ b/agora-specs/Sample/Proposal/UnlockStake.hs
@@ -0,0 +1,276 @@
+module Sample.Proposal.UnlockStake (
+  unlockStake,
+  StakeRole (..),
+  UnlockStakeParameters (..),
+  votesTemplate,
+  emptyEffectFor,
+  mkProposalInputDatum,
+  mkStakeInputDatum,
+  mkProposalValidatorTestCase,
+) where
+
+--------------------------------------------------------------------------------
+
+import PlutusLedgerApi.V1 (
+  DatumHash,
+  ScriptContext (..),
+  ScriptPurpose (Spending),
+  TxInfo (..),
+  TxOutRef (..),
+  ValidatorHash,
+ )
+import PlutusLedgerApi.V1.Value qualified as Value
+import PlutusTx.AssocMap qualified as AssocMap
+
+--------------------------------------------------------------------------------
+
+import Agora.Proposal (
+  ProposalDatum (..),
+  ProposalId (..),
+  ProposalRedeemer (Unlock),
+  ProposalStatus (..),
+  ProposalVotes (..),
+  ResultTag (..),
+ )
+import Agora.Proposal.Time (ProposalStartingTime (ProposalStartingTime))
+import Agora.Stake (ProposalLock (ProposalLock), Stake (..), StakeDatum (..))
+import Sample.Shared (
+  minAda,
+  proposalPolicySymbol,
+  proposalValidatorHash,
+  signer,
+  stake,
+  stakeAssetClass,
+  stakeValidatorHash,
+ )
+import Test.Util (sortValue, updateMap)
+
+--------------------------------------------------------------------------------
+
+import Agora.Proposal.Scripts (proposalValidator)
+import Control.Monad (join)
+import Data.Coerce (coerce)
+import Data.Default.Class (Default (def))
+import Data.Tagged (Tagged (..), untag)
+import Plutarch.Context (BaseBuilder, buildTxInfoUnsafe, input, output, script, txId, withDatum, withRefIndex, withTxId, withValue)
+import Sample.Proposal.Shared (proposalRef, stakeRef)
+import Sample.Shared qualified as Shared
+import Test.Specification (SpecificationTree, validatorFailsWith, validatorSucceedsWith)
+
+--------------------------------------------------------------------------------
+
+-- | The template "shape" that votes of proposals generated by 'mkProposalDatumPair' have.
+votesTemplate :: ProposalVotes
+votesTemplate =
+  ProposalVotes $
+    AssocMap.fromList
+      [ (ResultTag 0, 0)
+      , (ResultTag 1, 0)
+      ]
+
+-- | Create empty effects for every result tag given the votes.
+emptyEffectFor ::
+  ProposalVotes ->
+  AssocMap.Map ResultTag (AssocMap.Map ValidatorHash DatumHash)
+emptyEffectFor (ProposalVotes vs) =
+  AssocMap.fromList $
+    map (,AssocMap.empty) (AssocMap.keys vs)
+
+-- | The default vote option that will be used by functions in this module.
+defaultVoteFor :: ResultTag
+defaultVoteFor = ResultTag 0
+
+-- | The default number of GTs the stake will have.
+defaultStakedGTs :: Tagged _ Integer
+defaultStakedGTs = Tagged 100000
+
+-- | How a stake has been used on a particular proposal.
+data StakeRole
+  = -- | The stake was spent to vote for a paraticular option.
+    Voter
+  | -- | The stake was used to created the proposal.
+    Creator
+  | -- | The stake has nothing to do with the proposal.
+    Irrelevant
+
+-- | Parameters for creating a 'TxOut' that unlocks a stake.
+data UnlockStakeParameters = UnlockStakeParameters
+  { proposalCount :: Integer
+  -- ^ The number of proposals in the 'TxOut'.
+  , stakeUsage :: StakeRole
+  -- ^ The role of the stake we're unlocking.
+  , retractVotes :: Bool
+  -- ^ Whether to retract votes or not.
+  , proposalStatus :: ProposalStatus
+  -- ^ The state of all the proposals.
+  }
+
+instance Show UnlockStakeParameters where
+  show p =
+    let role = case p.stakeUsage of
+          Voter -> "voter"
+          Creator -> "creator"
+          _ -> "irrelevant stake"
+
+        action =
+          if p.retractVotes
+            then "unlock stake + retract votes"
+            else "unlock stake"
+
+        while = show p.proposalStatus
+
+        proposalInfo = mconcat [show p.proposalCount, " proposals"]
+     in mconcat [proposalInfo, ", ", role, ", ", action, ", ", while]
+
+-- | Generate some input proposals and their corresponding output proposals.
+mkProposals :: UnlockStakeParameters -> [(ProposalDatum, ProposalDatum)]
+mkProposals p = forEachProposalId p.proposalCount $ mkProposalDatumPair p
+
+-- | Iterate over the proposal id of every proposal, given the number of proposals.
+forEachProposalId :: Integer -> (ProposalId -> a) -> [a]
+forEachProposalId 0 _ = error "zero proposal"
+forEachProposalId n f = f . ProposalId <$> [0 .. n - 1]
+
+-- | Create the input stake and its corresponding output stake.
+mkStakeDatumPair :: UnlockStakeParameters -> (StakeDatum, StakeDatum)
+mkStakeDatumPair c =
+  let output =
+        StakeDatum
+          { stakedAmount = defaultStakedGTs
+          , owner = signer
+          , lockedBy = []
+          }
+
+      inputLocks = join $ forEachProposalId c.proposalCount (mkStakeLocks c.stakeUsage)
+
+      input = output {lockedBy = inputLocks}
+   in (input, output)
+  where
+    mkStakeLocks :: StakeRole -> ProposalId -> [ProposalLock]
+    mkStakeLocks Voter pid = [ProposalLock defaultVoteFor pid]
+    mkStakeLocks Creator pid =
+      map (`ProposalLock` pid) $
+        AssocMap.keys $ getProposalVotes votesTemplate
+    mkStakeLocks _ _ = []
+
+-- | Create the input proposal datum.
+mkProposalInputDatum :: UnlockStakeParameters -> ProposalId -> ProposalDatum
+mkProposalInputDatum p pid = fst $ mkProposalDatumPair p pid
+
+-- | Create the input stake datum.
+mkStakeInputDatum :: UnlockStakeParameters -> StakeDatum
+mkStakeInputDatum = fst . mkStakeDatumPair
+
+-- | Create a input proposal and its corresponding output proposal.
+mkProposalDatumPair ::
+  UnlockStakeParameters ->
+  ProposalId ->
+  (ProposalDatum, ProposalDatum)
+mkProposalDatumPair params pid =
+  let owner = signer
+
+      inputVotes = mkInputVotes params.stakeUsage $ untag defaultStakedGTs
+
+      input =
+        ProposalDatum
+          { proposalId = pid
+          , effects = emptyEffectFor votesTemplate
+          , status = params.proposalStatus
+          , cosigners = [owner]
+          , thresholds = def
+          , votes = inputVotes
+          , timingConfig = def
+          , startingTime = ProposalStartingTime 0
+          }
+
+      output =
+        if params.retractVotes
+          then input {votes = votesTemplate}
+          else input
+   in (input, output)
+  where
+    -- Assemble the votes of the input proposal based on 'votesTemplate'.
+    mkInputVotes ::
+      StakeRole ->
+      -- The staked amount/votes.
+      Integer ->
+      ProposalVotes
+    mkInputVotes Voter vc =
+      ProposalVotes $
+        updateMap (Just . const vc) defaultVoteFor $
+          getProposalVotes votesTemplate
+    mkInputVotes Creator _ =
+      ProposalVotes $
+        updateMap (Just . const 1000) defaultVoteFor $
+          getProposalVotes votesTemplate
+    mkInputVotes _ _ = votesTemplate
+
+-- | Create a 'TxInfo' that tries to unlock a stake.
+unlockStake :: UnlockStakeParameters -> TxInfo
+unlockStake p =
+  let pst = Value.singleton proposalPolicySymbol "" 1
+      sst = Value.assetClassValue stakeAssetClass 1
+
+      pIODatums = mkProposals p
+      (sInDatum, sOutDatum) = mkStakeDatumPair p
+
+      proposals =
+        foldMap
+          ( \(i, o) ->
+              mconcat
+                @BaseBuilder
+                [ input $
+                    script proposalValidatorHash
+                      . withValue pst
+                      . withDatum i
+                      . withTxId (txOutRefId proposalRef)
+                      . withRefIndex (txOutRefIdx proposalRef + coerce i.proposalId)
+                , output $
+                    script proposalValidatorHash
+                      . withValue (sortValue $ pst <> minAda)
+                      . withDatum o
+                ]
+          )
+          pIODatums
+
+      stakeValue =
+        sortValue $
+          mconcat
+            [ Value.assetClassValue
+                (untag stake.gtClassRef)
+                (untag defaultStakedGTs)
+            , sst
+            , minAda
+            ]
+
+      stakes =
+        mconcat @BaseBuilder
+          [ input $
+              script stakeValidatorHash
+                . withValue stakeValue
+                . withDatum sInDatum
+                . withTxId (txOutRefId stakeRef)
+                . withRefIndex (txOutRefIdx stakeRef)
+          , output $
+              script stakeValidatorHash
+                . withValue stakeValue
+                . withDatum sOutDatum
+          ]
+
+      builder =
+        mconcat @BaseBuilder
+          [ txId "388bc0b897b3dadcd479da4c88291de4113a50b72ddbed001faf7fc03f11bc52"
+          , proposals
+          , stakes
+          ]
+   in buildTxInfoUnsafe builder
+
+-- | Create a test case that tests the proposal validator's @'Unlock' _@ redeemer.
+mkProposalValidatorTestCase :: UnlockStakeParameters -> Bool -> SpecificationTree
+mkProposalValidatorTestCase p shouldSucceed =
+  let datum = mkProposalInputDatum p $ ProposalId 0
+      redeemer = Unlock (ResultTag 0)
+      name = show p
+      scriptContext = ScriptContext (unlockStake p) (Spending proposalRef)
+      f = if shouldSucceed then validatorSucceedsWith else validatorFailsWith
+   in f name (proposalValidator Shared.proposal) datum redeemer scriptContext
diff --git a/agora-specs/Spec/Proposal.hs b/agora-specs/Spec/Proposal.hs
index fa1fd1c..85d8b96 100644
--- a/agora-specs/Spec/Proposal.hs
+++ b/agora-specs/Spec/Proposal.hs
@@ -39,25 +39,9 @@ import Agora.Stake.Scripts (stakeValidator)
 import Data.Default.Class (Default (def))
 import Data.Tagged (Tagged (Tagged), untag)
 import PlutusLedgerApi.V1 (ScriptContext (..), ScriptPurpose (..))
-import PlutusTx.AssocMap qualified as AssocMap (empty, fromList)
-import Sample.Proposal qualified as Proposal (
-  TransitionParameters (
-    TransitionParameters,
-    initialProposalStatus,
-    proposalStartingTime
-  ),
-  VotingParameters (VotingParameters, voteCount, voteFor),
-  advanceFinishedPropsoal,
-  advanceProposalFailureTimeout,
-  advanceProposalInsufficientVotes,
-  advanceProposalSuccess,
-  advancePropsoalWithsStake,
-  cosignProposal,
-  proposalCreation,
-  proposalRef,
-  stakeRef,
-  voteOnProposal,
- )
+import PlutusTx.AssocMap qualified as AssocMap
+import Sample.Proposal qualified as Proposal
+import Sample.Proposal.UnlockStake qualified as UnlockStake
 import Sample.Shared (signer, signer2)
 import Sample.Shared qualified as Shared (proposal, stake)
 import Test.Specification (
@@ -323,7 +307,7 @@ specs =
               )
               AdvanceProposal
               ( ScriptContext
-                  Proposal.advanceFinishedPropsoal
+                  Proposal.advanceFinishedProposal
                   (Spending Proposal.proposalRef)
               )
           , validatorFailsWith
@@ -352,9 +336,114 @@ specs =
               )
               AdvanceProposal
               ( ScriptContext
-                  Proposal.advancePropsoalWithsStake
+                  Proposal.advanceProposalWithInvalidOutputStake
                   (Spending Proposal.proposalRef)
               )
           ]
+      , group "unlocking" $ do
+          proposalCount <- [1, 42]
+
+          let legalGroup = group "legal" $ do
+                let voterRetractVotesAndUnlockStakeWhileVoting =
+                      UnlockStake.mkProposalValidatorTestCase
+                        UnlockStake.UnlockStakeParameters
+                          { UnlockStake.proposalCount = proposalCount
+                          , UnlockStake.stakeUsage = UnlockStake.Voter
+                          , UnlockStake.retractVotes = True
+                          , UnlockStake.proposalStatus = VotingReady
+                          }
+                        True
+                    creatorUnlockStakeWhileFinished =
+                      UnlockStake.mkProposalValidatorTestCase
+                        UnlockStake.UnlockStakeParameters
+                          { UnlockStake.proposalCount = proposalCount
+                          , UnlockStake.stakeUsage = UnlockStake.Creator
+                          , UnlockStake.retractVotes = False
+                          , UnlockStake.proposalStatus = Finished
+                          }
+                        True
+
+                let voterUnlockStakeAfterVoting = group "voter unlocks stake after voting" $ do
+                      status <- [Finished, Locked]
+
+                      pure $
+                        UnlockStake.mkProposalValidatorTestCase
+                          UnlockStake.UnlockStakeParameters
+                            { UnlockStake.proposalCount = proposalCount
+                            , UnlockStake.stakeUsage = UnlockStake.Voter
+                            , UnlockStake.retractVotes = False
+                            , UnlockStake.proposalStatus = status
+                            }
+                          True
+
+                [ voterRetractVotesAndUnlockStakeWhileVoting
+                  , creatorUnlockStakeWhileFinished
+                  , voterUnlockStakeAfterVoting
+                  ]
+
+          let illegalGroup = group "illegal" $ do
+                let retractsVotesWhileNotVotingReady =
+                      group "voter retracts votes while not voting" $ do
+                        status <- [Draft, Locked, Finished]
+
+                        pure $
+                          UnlockStake.mkProposalValidatorTestCase
+                            UnlockStake.UnlockStakeParameters
+                              { UnlockStake.proposalCount = proposalCount
+                              , UnlockStake.stakeUsage = UnlockStake.Voter
+                              , UnlockStake.retractVotes = True
+                              , UnlockStake.proposalStatus = status
+                              }
+                            False
+
+                    unlockIrrelevantStake =
+                      group "unlock an irrelevant stake" $ do
+                        status <- [Draft, VotingReady, Locked, Finished]
+                        shouldRetractVotes <- [True, False]
+
+                        pure $
+                          UnlockStake.mkProposalValidatorTestCase
+                            UnlockStake.UnlockStakeParameters
+                              { UnlockStake.proposalCount = proposalCount
+                              , UnlockStake.stakeUsage = UnlockStake.Irrelevant
+                              , UnlockStake.retractVotes = shouldRetractVotes
+                              , UnlockStake.proposalStatus = status
+                              }
+                            False
+
+                    unlockCreatorStakeBeforeFinished =
+                      group "unlock creator stake before finished" $ do
+                        status <- [Draft, VotingReady, Locked]
+
+                        pure $
+                          UnlockStake.mkProposalValidatorTestCase
+                            UnlockStake.UnlockStakeParameters
+                              { UnlockStake.proposalCount = proposalCount
+                              , UnlockStake.stakeUsage = UnlockStake.Creator
+                              , UnlockStake.retractVotes = False
+                              , UnlockStake.proposalStatus = status
+                              }
+                            False
+                    retractVotesWithCreatorStake =
+                      group "creator stake retracts votes" $ do
+                        status <- [Draft, VotingReady, Locked, Finished]
+
+                        pure $
+                          UnlockStake.mkProposalValidatorTestCase
+                            UnlockStake.UnlockStakeParameters
+                              { UnlockStake.proposalCount = proposalCount
+                              , UnlockStake.stakeUsage = UnlockStake.Creator
+                              , UnlockStake.retractVotes = True
+                              , UnlockStake.proposalStatus = status
+                              }
+                            False
+
+                [ retractsVotesWhileNotVotingReady
+                  , unlockIrrelevantStake
+                  , unlockCreatorStakeBeforeFinished
+                  , retractVotesWithCreatorStake
+                  ]
+
+          [legalGroup, illegalGroup]
       ]
   ]
diff --git a/agora-testlib/Test/Util.hs b/agora-testlib/Test/Util.hs
index 50fb1e4..78600a5 100644
--- a/agora-testlib/Test/Util.hs
+++ b/agora-testlib/Test/Util.hs
@@ -11,6 +11,8 @@ module Test.Util (
   datumPair,
   closedBoundedInterval,
   updateMap,
+  sortMap,
+  sortValue,
 ) where
 
 --------------------------------------------------------------------------------
@@ -24,9 +26,12 @@ import Data.ByteString.Lazy qualified as ByteString.Lazy
 
 --------------------------------------------------------------------------------
 
+import Data.Bifunctor (second)
+import Data.List (sortOn)
 import Plutarch.Crypto (pblake2b_256)
-import PlutusLedgerApi.V1.Interval as PlutusTx
+import PlutusLedgerApi.V1.Interval qualified as PlutusTx
 import PlutusLedgerApi.V1.Scripts (Datum (Datum), DatumHash (DatumHash))
+import PlutusLedgerApi.V1.Value (Value (..))
 import PlutusTx.AssocMap qualified as AssocMap
 import PlutusTx.Builtins qualified as PlutusTx
 import PlutusTx.IsData qualified as PlutusTx
@@ -84,3 +89,20 @@ updateMap f k =
           then f v
           else Just v
     )
+
+--------------------------------------------------------------------------------
+
+sortMap :: forall k v. Ord k => AssocMap.Map k v -> AssocMap.Map k v
+sortMap =
+  AssocMap.fromList
+    . sortOn fst
+    . AssocMap.toList
+
+sortValue :: Value -> Value
+sortValue =
+  Value
+    . sortMap
+    . AssocMap.fromList
+    . fmap (second sortMap)
+    . AssocMap.toList
+    . getValue
diff --git a/agora.cabal b/agora.cabal
index 7cf71c2..143f880 100644
--- a/agora.cabal
+++ b/agora.cabal
@@ -182,6 +182,8 @@ library agora-specs
     Sample.Effect.TreasuryWithdrawal
     Sample.Governor
     Sample.Proposal
+    Sample.Proposal.Shared
+    Sample.Proposal.UnlockStake
     Sample.Shared
     Sample.Stake
     Sample.Treasury
diff --git a/agora/Agora/Effect/TreasuryWithdrawal.hs b/agora/Agora/Effect/TreasuryWithdrawal.hs
index 1024e9b..9104e33 100644
--- a/agora/Agora/Effect/TreasuryWithdrawal.hs
+++ b/agora/Agora/Effect/TreasuryWithdrawal.hs
@@ -18,7 +18,7 @@ import GHC.Generics qualified as GHC
 import Generics.SOP (Generic, I (I))
 
 import Agora.Effect (makeEffect)
-import Agora.Utils (findTxOutByTxOutRef, isPubKey)
+import Agora.Utils (isPubKey)
 import Plutarch.Api.V1 (
   AmountGuarantees (Positive),
   KeyGuarantees (Sorted),
@@ -30,6 +30,7 @@ import Plutarch.Api.V1 (
  )
 import Plutarch.Internal (punsafeCoerce)
 
+import Plutarch.Api.V1.ScriptContext (pfindTxInByTxOutRef)
 import "plutarch" Plutarch.Api.V1.Value (pnormalize)
 import Plutarch.DataRepr (
   DerivePConstantViaData (..),
@@ -112,7 +113,7 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
   \_cs (datum' :: Term _ PTreasuryWithdrawalDatum) txOutRef' txInfo' -> unTermCont $ do
     datum <- tcont $ pletFields @'["receivers", "treasuries"] datum'
     txInfo <- tcont $ pletFields @'["outputs", "inputs"] txInfo'
-    PJust txOut <- pmatchC $ findTxOutByTxOutRef # txOutRef' # pfromData txInfo.inputs
+    PJust ((pfield @"resolved" #) -> txOut) <- pmatchC $ pfindTxInByTxOutRef # txOutRef' # pfromData txInfo.inputs
     effInput <- tcont $ pletFields @'["address", "value"] $ txOut
     outputValues <-
       pletC $
diff --git a/agora/Agora/Proposal.hs b/agora/Agora/Proposal.hs
index 9202bcc..2705291 100644
--- a/agora/Agora/Proposal.hs
+++ b/agora/Agora/Proposal.hs
@@ -33,6 +33,7 @@ module Agora.Proposal (
   pemptyVotesFor,
   pwinner,
   pneutralOption,
+  pretractVotes,
 ) where
 
 --------------------------------------------------------------------------------
@@ -63,7 +64,7 @@ import Plutarch.DataRepr (DerivePConstantViaData (..), PDataFields, PIsDataReprI
 import Plutarch.Extra.List (pnotNull)
 import Plutarch.Extra.Map qualified as PM
 import Plutarch.Extra.Map.Unsorted qualified as PUM
-import Plutarch.Extra.TermCont (pletC)
+import Plutarch.Extra.TermCont (pguardC, pletC)
 import Plutarch.Lift (
   DerivePConstantViaNewtype (..),
   PConstantDecl,
@@ -367,6 +368,24 @@ newtype PProposalVotes (s :: S)
   = PProposalVotes (Term s (PMap 'Unsorted PResultTag PInteger))
   deriving (PlutusType, PIsData) via (DerivePNewtype PProposalVotes (PMap 'Unsorted PResultTag PInteger))
 
+-- | Retract votes given the option and the amount of votes.
+pretractVotes :: Term s (PResultTag :--> PInteger :--> PProposalVotes :--> PProposalVotes)
+pretractVotes = phoistAcyclic $
+  plam $ \rt count votes ->
+    let voteMap :: Term _ (PMap 'Unsorted PResultTag PInteger)
+        voteMap = pto votes
+     in pcon $
+          PProposalVotes $
+            PM.pupdate
+              # plam
+                ( \oldCount -> unTermCont $ do
+                    newCount <- pletC $ oldCount - count
+                    pguardC "Resulting vote count greater or equal to 0" $ 0 #<= newCount
+                    pure $ pcon $ PJust newCount
+                )
+              # rt
+              # voteMap
+
 instance PUnsafeLiftDecl PProposalVotes where type PLifted PProposalVotes = ProposalVotes
 deriving via
   (DerivePConstantViaNewtype ProposalVotes PProposalVotes (PMap 'Unsorted PResultTag PInteger))
diff --git a/agora/Agora/Proposal/Scripts.hs b/agora/Agora/Proposal/Scripts.hs
index f35e95f..c560e1b 100644
--- a/agora/Agora/Proposal/Scripts.hs
+++ b/agora/Agora/Proposal/Scripts.hs
@@ -17,6 +17,7 @@ import Agora.Proposal (
   PProposalVotes (PProposalVotes),
   Proposal (governorSTAssetClass, stakeSTAssetClass),
   ProposalStatus (..),
+  pretractVotes,
  )
 import Agora.Proposal.Time (
   currentProposalTime,
@@ -25,9 +26,14 @@ import Agora.Proposal.Time (
   isLockingPeriod,
   isVotingPeriod,
  )
-import Agora.Stake (PProposalLock (..), PStakeDatum (..), findStakeOwnedBy)
+import Agora.Stake (
+  PProposalLock (..),
+  PStakeDatum (..),
+  PStakeUsage (..),
+  findStakeOwnedBy,
+  pgetStakeUsage,
+ )
 import Agora.Utils (
-  findTxOutByTxOutRef,
   getMintingPolicySymbol,
   mustBePJust,
   mustFindDatum',
@@ -41,6 +47,7 @@ import Plutarch.Api.V1 (
  )
 import Plutarch.Api.V1.AssetClass (passetClass, passetClassValueOf)
 import Plutarch.Api.V1.ScriptContext (
+  pfindTxInByTxOutRef,
   pisTokenSpent,
   ptxSignedBy,
   pvalueSpent,
@@ -54,6 +61,7 @@ import Plutarch.Extra.Record (mkRecordConstr, (.&), (.=))
 import Plutarch.Extra.TermCont (
   pguardC,
   pletC,
+  pletFieldsC,
   pmatchC,
   ptryFromC,
  )
@@ -155,7 +163,7 @@ proposalValidator proposal =
           txInfo'
     PSpending ((pfield @"_0" #) -> txOutRef) <- pmatchC $ pfromData ctx.purpose
 
-    PJust txOut <- pmatchC $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
+    PJust ((pfield @"resolved" #) -> txOut) <- pmatchC $ pfindTxInByTxOutRef # txOutRef # txInfoF.inputs
     txOutF <- tcont $ pletFields @'["address", "value"] $ txOut
 
     (pfromData -> proposalDatum, _) <-
@@ -182,31 +190,38 @@ proposalValidator proposal =
     let stCurrencySymbol =
           pconstant $ getMintingPolicySymbol (proposalPolicy proposal.governorSTAssetClass)
     valueSpent <- pletC $ pvalueSpent # txInfoF.inputs
-    spentST <- pletC $ psymbolValueOf # stCurrencySymbol #$ valueSpent
-
-    let AssetClass (stakeSym, stakeTn) = proposal.stakeSTAssetClass
-    stakeSTAssetClass <-
-      pletC $ passetClass # pconstant stakeSym # pconstant stakeTn
-    spentStakeST <-
-      pletC $ passetClassValueOf # valueSpent # stakeSTAssetClass
 
     signedBy <- pletC $ ptxSignedBy # txInfoF.signatories
 
-    pguardC "ST at inputs must be 1" (spentST #== 1)
-
     currentTime <- pletC $ currentProposalTime # txInfoF.validRange
 
-    -- Filter out own output with own address and PST.
-    -- Delay the evaluation cause in some cases there won't be any continuing output.
+    -- Own output is an output that
+    --  * is sent to the address of the proposal validator
+    --  * has an PST
+    --  * has the same proposal id as the proposal input
+    --
+    -- We match the proposal id here so that we can support multiple
+    --  proposal inputs in one thansaction.
     ownOutput <-
       pletC $
         mustBePJust # "Own output should be present" #$ pfind
           # plam
             ( \input -> unTermCont $ do
-                inputF <- tcont $ pletFields @'["address", "value"] input
+                inputF <- tcont $ pletFields @'["address", "value", "datumHash"] input
+
+                -- TODO: this is highly inefficient: O(n) for every output,
+                --       Maybe we can cache the sorted datum map?
+                let datum =
+                      mustFindDatum' @PProposalDatum
+                        # inputF.datumHash
+                        # txInfoF.datums
+
+                    proposalId = pfield @"proposalId" # datum
+
                 pure $
                   inputF.address #== ownAddress
                     #&& psymbolValueOf # stCurrencySymbol # inputF.value #== 1
+                    #&& proposalId #== proposalF.proposalId
             )
           # pfromData txInfoF.outputs
 
@@ -216,6 +231,45 @@ proposalValidator proposal =
           # (pfield @"datumHash" # ownOutput)
           # txInfoF.datums
 
+    proposalUnchanged <- pletC $ proposalOut #== proposalDatum
+    --------------------------------------------------------------------------
+    -- Find the stake input and stake output by SST.
+
+    let AssetClass (stakeSym, stakeTn) = proposal.stakeSTAssetClass
+    stakeSTAssetClass <-
+      pletC $ passetClass # pconstant stakeSym # pconstant stakeTn
+    spentStakeST <-
+      pletC $ passetClassValueOf # valueSpent # stakeSTAssetClass
+
+    let stakeInput =
+          pfield @"resolved"
+            #$ mustBePJust
+            # "Stake input should be present"
+              #$ pfind
+            # plam
+              ( \(pfromData . (pfield @"value" #) . (pfield @"resolved" #) -> value) ->
+                  passetClassValueOf # value # stakeSTAssetClass #== 1
+              )
+            # pfromData txInfoF.inputs
+
+    stakeIn <- pletC $ mustFindDatum' @PStakeDatum # (pfield @"datumHash" # stakeInput) # txInfoF.datums
+    stakeInF <- pletFieldsC @'["stakedAmount", "lockedBy", "owner"] stakeIn
+
+    let stakeOutput =
+          mustBePJust # "Stake output should be present"
+            #$ pfind
+            # plam
+              ( \(pfromData . (pfield @"value" #) -> value) ->
+                  passetClassValueOf # value # stakeSTAssetClass #== 1
+              )
+            # pfromData txInfoF.outputs
+
+    stakeOut <- pletC $ mustFindDatum' @PStakeDatum # (pfield @"datumHash" # stakeOutput) # txInfoF.datums
+
+    stakeUnchanged <- pletC $ stakeIn #== stakeOut
+
+    --------------------------------------------------------------------------
+
     pure $
       pmatch proposalRedeemer $ \case
         PVote r -> unTermCont $ do
@@ -232,25 +286,8 @@ proposalValidator proposal =
           pguardC "Vote option should be valid" $
             pisJust #$ plookup # voteFor # voteMap
 
-          -- Find the input stake, the amount of new votes should be the 'stakedAmount'.
-          let stakeInput =
-                pfield @"resolved"
-                  #$ mustBePJust
-                  # "Stake input should be present"
-                    #$ pfind
-                  # plam
-                    ( \(pfromData . (pfield @"value" #) . (pfield @"resolved" #) -> value) ->
-                        passetClassValueOf # value # stakeSTAssetClass #== 1
-                    )
-                  # pfromData txInfoF.inputs
-
-              stakeIn :: Term _ PStakeDatum
-              stakeIn = mustFindDatum' # (pfield @"datumHash" # stakeInput) # txInfoF.datums
-
-          stakeInF <- tcont $ pletFields @'["stakedAmount", "lockedBy", "owner"] stakeIn
-
           -- Ensure that no lock with the current proposal id has been put on the stake.
-          pguardC "Same stake shouldn't vote on the same propsoal twice" $
+          pguardC "Same stake shouldn't vote on the same proposal twice" $
             pnot #$ pany
               # plam
                 ( \((pfield @"proposalTag" #) . pfromData -> pid) ->
@@ -258,7 +295,8 @@ proposalValidator proposal =
                 )
               # pfromData stakeInF.lockedBy
 
-          let -- Update the vote counter of the proposal, and leave other stuff as is.
+          let -- The amount of new votes should be the 'stakedAmount'.
+              -- Update the vote counter of the proposal, and leave other stuff as is.
               expectedNewVotes = pmatch (pfromData proposalF.votes) $ \(PProposalVotes m) ->
                 pcon $
                   PProposalVotes $
@@ -289,18 +327,6 @@ proposalValidator proposal =
           -- to create a valid 'ProposalLock', however the vote option is encoded
           -- in the proposal redeemer, which is invisible for the stake validator.
 
-          let stakeOutput =
-                mustBePJust # "Stake output should be present"
-                  #$ pfind
-                  # plam
-                    ( \(pfromData . (pfield @"value" #) -> value) ->
-                        passetClassValueOf # value # stakeSTAssetClass #== 1
-                    )
-                  # pfromData txInfoF.outputs
-
-              stakeOut :: Term _ PStakeDatum
-              stakeOut = mustFindDatum' # (pfield @"datumHash" # stakeOutput) # txInfoF.datums
-
           let newProposalLock =
                 mkRecordConstr
                   PProposalLock
@@ -325,6 +351,8 @@ proposalValidator proposal =
           pure $ popaque (pconstant ())
         --------------------------------------------------------------------------
         PCosign r -> unTermCont $ do
+          pguardC "Stake should not change" stakeUnchanged
+
           newSigs <- pletC $ pfield @"newCosigners" # r
 
           pguardC "Cosigners are unique" $
@@ -374,13 +402,86 @@ proposalValidator proposal =
 
           pure $ popaque (pconstant ())
         --------------------------------------------------------------------------
-        PUnlock _r ->
-          popaque (pconstant ())
+        PUnlock r -> unTermCont $ do
+          -- At draft stage, the votes should be empty.
+          pguardC "Shouldn't retract votes from a draft proposal" $
+            pnot #$ proposalF.status #== pconstantData Draft
+
+          -- This is the vote option we're retracting from.
+          retractFrom <- pletC $ pfield @"resultTag" # r
+
+          -- Determine if the input stake is actually locked by this proposal.
+          stakeUsage <- pletC $ pgetStakeUsage # stakeInF.lockedBy # proposalF.proposalId
+
+          pguardC "Stake input relevant" $
+            pmatch stakeUsage $ \case
+              PDidNothing ->
+                ptraceIfFalse "Stake should be relevant" $
+                  pconstant False
+              PCreated ->
+                ptraceIfFalse "Removing creator's locks means status is Finished" $
+                  proposalF.status #== pconstantData Finished
+              PVotedFor rt ->
+                ptraceIfFalse "Result tag should match the one given in the redeemer" $
+                  rt #== retractFrom
+
+          -- The count of removing votes is equal to the 'stakeAmount' of input stake.
+          retractCount <-
+            pletC $
+              pmatch stakeInF.stakedAmount $ \(PDiscrete v) -> pextract # v
+
+          -- The votes can only change when the proposal still allows voting.
+          let shouldUpdateVotes =
+                proposalF.status #== pconstantData VotingReady
+                  #&& pnot # (pcon PCreated #== stakeUsage)
+
+          pguardC "Proposal output correct" $
+            pif
+              shouldUpdateVotes
+              ( let -- Remove votes and leave other parts of the proposal as it.
+                    expectedVotes = pretractVotes # retractFrom # retractCount # proposalF.votes
+
+                    expectedProposalOut =
+                      mkRecordConstr
+                        PProposalDatum
+                        ( #proposalId .= proposalF.proposalId
+                            .& #effects .= proposalF.effects
+                            .& #status .= proposalF.status
+                            .& #cosigners .= proposalF.cosigners
+                            .& #thresholds .= proposalF.thresholds
+                            .& #votes .= pdata expectedVotes
+                            .& #timingConfig .= proposalF.timingConfig
+                            .& #startingTime .= proposalF.startingTime
+                        )
+                 in ptraceIfFalse "Update votes" $
+                      expectedProposalOut #== proposalOut
+              )
+              -- No change to the proposal is allowed.
+              $ ptraceIfFalse "Proposal unchanged" proposalUnchanged
+
+          -- At last, we ensure that all locks belong to this proposal will be removed.
+          stakeOutputLocks <- pletC $ pfield @"lockedBy" # stakeOut
+
+          let templateStakeOut =
+                mkRecordConstr
+                  PStakeDatum
+                  ( #stakedAmount .= stakeInF.stakedAmount
+                      .& #owner .= stakeInF.owner
+                      .& #lockedBy .= stakeOutputLocks
+                  )
+
+          pguardC "Only locks updated in the output stake" $
+            templateStakeOut #== stakeOut
+
+          pguardC "All relevant locks removed from the stake" $
+            pgetStakeUsage # pfromData stakeOutputLocks
+              # proposalF.proposalId #== pcon PDidNothing
+
+          pure $ popaque (pconstant ())
         --------------------------------------------------------------------------
         PAdvanceProposal _r -> unTermCont $ do
-          pguardC "No stake input is allowed" $ spentStakeST #== 0
+          pguardC "Stake should not change" stakeUnchanged
 
-          currentTime <- pletC $ currentProposalTime # txInfoF.validRange
           proposalOutStatus <- pletC $ pfield @"status" # proposalOut
 
           let -- Only the status of proposals should be updated in this case.
diff --git a/agora/Agora/Stake.hs b/agora/Agora/Stake.hs
index 3558d9e..61b6b68 100644
--- a/agora/Agora/Stake.hs
+++ b/agora/Agora/Stake.hs
@@ -18,10 +18,12 @@ module Agora.Stake (
   PStakeDatum (..),
   PStakeRedeemer (..),
   PProposalLock (..),
+  PStakeUsage (..),
 
   -- * Utility functions
   stakeLocked,
   findStakeOwnedBy,
+  pgetStakeUsage,
 ) where
 
 --------------------------------------------------------------------------------
@@ -29,7 +31,7 @@ module Agora.Stake (
 import Control.Applicative (Const)
 import Data.Tagged (Tagged (..))
 import GHC.Generics qualified as GHC
-import Generics.SOP (Generic, I (I))
+import Generics.SOP (Generic, HasDatatypeInfo, I (I))
 import Prelude hiding (Num (..))
 
 --------------------------------------------------------------------------------
@@ -56,8 +58,8 @@ import Plutarch.DataRepr (
   PDataFields,
   PIsDataReprInstances (PIsDataReprInstances),
  )
-import Plutarch.Extra.List (pnotNull)
-import Plutarch.Extra.TermCont (pletC, pmatchC)
+import Plutarch.Extra.List (pmapMaybe, pnotNull)
+import Plutarch.Extra.TermCont (pletC, pletFieldsC, pmatchC)
 import Plutarch.Internal (punsafeCoerce)
 import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (..))
 import Plutarch.SafeMoney (PDiscrete)
@@ -286,7 +288,7 @@ stakeDatumOwnedBy =
       pletFields @'["owner"] (pto stakeDatum) $ \stakeDatumF ->
         stakeDatumF.owner #== pdata pk
 
--- Does the input have a `Stake` owned by a particular PK?
+-- | Does the input have a `Stake` owned by a particular PK?
 isInputStakeOwnedBy ::
   Term
     _
@@ -299,7 +301,7 @@ isInputStakeOwnedBy =
   plam $ \ac ss datums txInInfo' -> unTermCont $ do
     PTxInInfo ((pfield @"resolved" #) -> txOut) <- pmatchC $ pfromData txInInfo'
     PTxOut txOut' <- pmatchC txOut
-    txOutF <- tcont $ pletFields @'["value", "datumHash"] txOut'
+    txOutF <- pletFieldsC @'["value", "datumHash"] txOut'
     outStakeST <- pletC $ passetClassValueOf # txOutF.value # ac
     pure $
       pmatch txOutF.datumHash $ \case
@@ -312,3 +314,53 @@ isInputStakeOwnedBy =
                 PJust v -> stakeDatumOwnedBy # ss # pfromData (punsafeCoerce v)
             )
             (pcon PFalse)
+
+{- | Represent the usage of a stake on a particular proposal.
+     A stake can be used to either create or vote on a proposal.
+-}
+data PStakeUsage (s :: S)
+  = PVotedFor (Term s PResultTag)
+  | PCreated
+  | PDidNothing
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic, PlutusType, HasDatatypeInfo, PEq)
+
+{- | / O(n) /.Return the usage of a stake on a particular proposal,
+      given the 'lockedBy' field of a stake and the target proposal.
+-}
+pgetStakeUsage ::
+  Term
+    _
+    ( PBuiltinList (PAsData PProposalLock)
+        :--> PProposalId
+        :--> PStakeUsage
+    )
+pgetStakeUsage = phoistAcyclic $
+  plam $ \locks pid ->
+    let -- All locks from the given proposal.
+        filteredLocks =
+          pmapMaybe
+            # plam
+              ( \lock'@(pfromData -> lock) -> unTermCont $ do
+                  lockF <- pletFieldsC @'["proposalTag"] lock
+
+                  pure $
+                    pif
+                      (lockF.proposalTag #== pid)
+                      (pcon $ PJust lock')
+                      (pcon PNothing)
+              )
+            # locks
+
+        lockCount' = plength # filteredLocks
+     in plet lockCount' $ \lockCount ->
+          pif (lockCount #== 0) (pcon PDidNothing) $
+            pif
+              (lockCount #== 1)
+              ( pcon $
+                  PVotedFor $
+                    pfromData $
+                      pfield @"vote" #$ phead # filteredLocks
+              )
+              -- Note: see the implementation of the governor.
+              (pcon PCreated)
diff --git a/agora/Agora/Stake/Scripts.hs b/agora/Agora/Stake/Scripts.hs
index d0ca147..a1c8c3f 100644
--- a/agora/Agora/Stake/Scripts.hs
+++ b/agora/Agora/Stake/Scripts.hs
@@ -287,7 +287,7 @@ stakeValidator stake =
 
           pure $
             pmatch stakeRedeemer $ \case
-              PRetractVotes _ -> unTermCont $ do
+              PRetractVotes l -> unTermCont $ do
                 pguardC
                   "Owner signs this transaction"
                   ownerSignsTransaction
@@ -301,15 +301,22 @@ stakeValidator stake =
                   spentProposalST #== 1
 
                 pguardC "A UTXO must exist with the correct output" $
-                  unTermCont $ do
-                    let valueCorrect = ownOutputValueUnchanged
+                  let expectedLocks = pfield @"locks" # l
 
-                    -- TODO: check output datum is expected.
+                      expectedDatum =
+                        mkRecordConstr
+                          PStakeDatum
+                          ( #stakedAmount .= stakeDatum.stakedAmount
+                              .& #owner .= stakeDatum.owner
+                              .& #lockedBy .= expectedLocks
+                          )
 
-                    pure $
-                      foldl1
+                      valueCorrect = ownOutputValueUnchanged
+                      outputDatumCorrect = stakeOut #== expectedDatum
+                   in foldl1
                         (#&&)
                         [ ptraceIfFalse "valueCorrect" valueCorrect
+                        , ptraceIfFalse "datumCorrect" outputDatumCorrect
                         ]
 
                 pure $ popaque (pconstant ())
diff --git a/agora/Agora/Utils.hs b/agora/Agora/Utils.hs
index 9425da2..b772445 100644
--- a/agora/Agora/Utils.hs
+++ b/agora/Agora/Utils.hs
@@ -6,7 +6,6 @@ Description: Plutarch utility functions that should be upstreamed or don't belon
 Plutarch utility functions that should be upstreamed or don't belong anywhere else.
 -}
 module Agora.Utils (
-  findTxOutByTxOutRef,
   scriptHashFromAddress,
   findOutputsToAddress,
   findTxOutDatum,
@@ -20,7 +19,6 @@ module Agora.Utils (
   validatorHashToAddress,
   isScriptAddress,
   isPubKey,
-  psingletonValue,
 ) where
 
 --------------------------------------------------------------------------------
@@ -47,19 +45,15 @@ import Plutarch.Api.V1 (
   PMintingPolicy,
   PTokenName (PTokenName),
   PTuple,
-  PTxInInfo,
   PTxOut,
-  PTxOutRef,
   PValidatorHash,
   PValue,
   mintingPolicySymbol,
   mkMintingPolicy,
  )
-import Plutarch.Api.V1.AssocMap (PMap (PMap))
-import Plutarch.Api.V1.ScriptContext (pfindDatum, pfindTxInByTxOutRef)
+import Plutarch.Api.V1.ScriptContext (pfindDatum)
 import "liqwid-plutarch-extra" Plutarch.Api.V1.Value (psymbolValueOf)
-import "plutarch" Plutarch.Api.V1.Value (PValue (PValue))
-import Plutarch.Builtin (pforgetData, ppairDataBuiltin)
+import Plutarch.Builtin (pforgetData)
 import Plutarch.Extra.List (plookupTuple)
 import Plutarch.Extra.TermCont (pletC, pmatchC)
 
@@ -67,25 +61,6 @@ import Plutarch.Extra.TermCont (pletC, pmatchC)
    All of these functions are quite inefficient.
 -}
 
--- | Create a value with a single asset class.
-psingletonValue ::
-  forall (keys :: KeyGuarantees) (amounts :: AmountGuarantees) (s :: S).
-  Term s (PCurrencySymbol :--> PTokenName :--> PInteger :--> PValue keys amounts)
-psingletonValue = phoistAcyclic $
-  plam $ \sym tok int ->
-    let innerTup = pcon $ PMap $ psingleton #$ ppairDataBuiltin # pdata tok # pdata int
-        outerTup = pcon $ PMap $ psingleton #$ ppairDataBuiltin # pdata sym # pdata innerTup
-        res = pcon $ PValue outerTup
-     in res
-
--- | Finds the TxOut of an effect from TxInfo and TxOutRef
-findTxOutByTxOutRef :: Term s (PTxOutRef :--> PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxOut)
-findTxOutByTxOutRef = phoistAcyclic $
-  plam $ \txOutRef inputs ->
-    pmatch (pfindTxInByTxOutRef # txOutRef # inputs) $ \case
-      PJust ((pfield @"resolved" #) -> txOut) -> pcon $ PJust txOut
-      PNothing -> pcon PNothing
-
 -- | Get script hash from an Address.
 scriptHashFromAddress :: Term s (PAddress :--> PMaybe PValidatorHash)
 scriptHashFromAddress = phoistAcyclic $
diff --git a/bench.csv b/bench.csv
index 08cfa2c..e69de29 100644
--- a/bench.csv
+++ b/bench.csv
@@ -1,29 +0,0 @@
-name,cpu,mem,size
-Agora/Effects/Treasury Withdrawal Effect/effect/Simple,289461528,703055,3191
-Agora/Effects/Treasury Withdrawal Effect/effect/Simple with multiple treasuries ,448521458,1070167,3518
-Agora/Effects/Treasury Withdrawal Effect/effect/Mixed Assets,408085321,966048,3383
-Agora/Effects/Governor Mutation Effect/validator/valid new governor datum/governor validator should pass,83758582,229228,7665
-Agora/Effects/Governor Mutation Effect/validator/valid new governor datum/effect validator should pass,97345575,266935,3358
-Agora/Stake/policy/stakeCreation,43114795,124549,2156
-Agora/Stake/validator/stakeDepositWithdraw deposit,171823342,464745,4144
-Agora/Stake/validator/stakeDepositWithdraw withdraw,171823342,464745,4132
-Agora/Proposal/policy/proposalCreation,23140177,69194,1517
-Agora/Proposal/validator/cosignature/proposal,145357978,397941,5721
-Agora/Proposal/validator/cosignature/stake,115369581,282557,4681
-Agora/Proposal/validator/voting/proposal,154824944,415642,5650
-Agora/Proposal/validator/voting/stake,99545453,256941,4655
-Agora/Proposal/validator/advancing/successfully advance to next state/Draft -> VotringReady,94701799,249495,5027
-Agora/Proposal/validator/advancing/successfully advance to next state/VotingReady -> Locked,93858377,247992,5030
-Agora/Proposal/validator/advancing/successfully advance to next state/Locked -> Finished,95554844,251598,5030
-Agora/Proposal/validator/advancing/successfully advance to failed state: timeout/Draft -> Finished,93571998,246765,5029
-Agora/Proposal/validator/advancing/successfully advance to failed state: timeout/VotingReady -> Finished,92163087,244060,5030
-Agora/Proposal/validator/advancing/successfully advance to failed state: timeout/Locked -> Finished,93294065,246464,5030
-Agora/AuthorityToken/singleAuthorityTokenBurned/Correct simple,21017788,55883,806
-Agora/AuthorityToken/singleAuthorityTokenBurned/Correct many inputs,33204186,88241,900
-Agora/Treasury/Validator/Positive/Allows for effect changes,29938856,79744,1390
-Agora/AuthorityToken/singleAuthorityTokenBurned/Correct simple,21017788,55883,806
-Agora/AuthorityToken/singleAuthorityTokenBurned/Correct many inputs,33204186,88241,900
-Agora/Governor/policy/GST minting,43087287,120125,1829
-Agora/Governor/validator/proposal creation,261928725,689487,8181
-Agora/Governor/validator/GATs minting,349849353,933334,8302
-Agora/Governor/validator/mutate governor state,84905433,234687,7766