diff --git a/agora-specs/Spec/Proposal.hs b/agora-specs/Spec/Proposal.hs
index 6ff1105..597ebcf 100644
--- a/agora-specs/Spec/Proposal.hs
+++ b/agora-specs/Spec/Proposal.hs
@@ -53,7 +53,7 @@ specs =
               Create.addInvalidLocksParameters
               True
               False
-              True
+              False
           , Create.mkTestTree
               "has reached maximum proposals limit"
               Create.exceedMaximumProposalsParameters
diff --git a/agora/Agora/Stake.hs b/agora/Agora/Stake.hs
index 0f7e7b6..083e749 100644
--- a/agora/Agora/Stake.hs
+++ b/agora/Agora/Stake.hs
@@ -45,6 +45,7 @@ module Agora.Stake (
 import Agora.Proposal (
   PProposalId,
   PProposalRedeemer,
+  PProposalStatus,
   PResultTag,
   ProposalId,
   ResultTag,
@@ -252,6 +253,8 @@ newtype PStakeDatum (s :: S) = PStakeDatum
       PEq
     , -- | @since 1.0.0
       PDataFields
+    , -- | @since 1.0.0
+      PShow
     )
 
 instance DerivePlutusType PStakeDatum where
@@ -503,9 +506,13 @@ instance DerivePlutusType PStakeRedeemerContext where
 -}
 data PProposalContext (s :: S)
   = -- | A proposal is spent.
-    PWithProposalRedeemer (Term s PProposalRedeemer)
+    PSpendProposal
+      (Term s PProposalId)
+      (Term s PProposalStatus)
+      (Term s PProposalRedeemer)
   | -- | A new proposal is created.
     PNewProposal
+      (Term s PProposalId)
   | -- | No proposal is spent or created.
     PNoProposal
   deriving stock
diff --git a/agora/Agora/Stake/Redeemers.hs b/agora/Agora/Stake/Redeemers.hs
index fa8e4c3..d4df2e2 100644
--- a/agora/Agora/Stake/Redeemers.hs
+++ b/agora/Agora/Stake/Redeemers.hs
@@ -14,12 +14,17 @@ module Agora.Stake.Redeemers (
   pdepositWithdraw,
 ) where
 
-import Agora.Proposal (PProposalRedeemer (PUnlock, PVote))
+import Agora.Proposal (
+  PProposalId,
+  PProposalRedeemer (PUnlock, PVote),
+  ProposalStatus (Finished),
+ )
 import Agora.Stake (
   PProposalContext (
     PNewProposal,
-    PWithProposalRedeemer
+    PSpendProposal
   ),
+  PProposalLock (PCreated, PVoted),
   PSigContext (owner, signedBy),
   PSignedBy (
     PSignedByDelegate,
@@ -93,26 +98,39 @@ pisSignedBy = phoistAcyclic $
 -- | Return true if only the @lockedBy@ field of the stake datum is updated.
 ponlyLocksUpdated ::
   forall (s :: S).
-  Term s (PStakeRedeemerHandlerContext :--> PBool)
+  Term
+    s
+    ( ( PBuiltinList (PAsData PProposalLock)
+          :--> PBuiltinList (PAsData PProposalLock)
+      )
+        :--> PStakeRedeemerHandlerContext
+        :--> PBool
+    )
 ponlyLocksUpdated = phoistAcyclic $
-  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
+  plam $ \f ->
+    pbatchUpdateInputs #$ plam $ \i o ->
+      pletAll i $ \iF ->
+        let newLocks = f # pfromData iF.lockedBy
+
+            expected =
+              mkRecordConstr
+                PStakeDatum
+                ( #stakedAmount .= iF.stakedAmount
+                    .& #owner .= iF.owner
+                    .& #delegatedTo .= iF.delegatedTo
+                    .& #lockedBy .= pdata newLocks
+                )
+         in expected #== o
 
 -- | Validation logic shared between 'ppermitVote' and 'retractVote'.
 pvoteHelper ::
   forall (s :: S).
   Term
     s
-    ( (PProposalContext :--> PBool)
+    ( ( PProposalContext
+          :--> PBuiltinList (PAsData PProposalLock)
+          :--> PBuiltinList (PAsData PProposalLock)
+      )
         :--> PStakeRedeemerHandler
     )
 pvoteHelper = phoistAcyclic $
@@ -125,14 +143,21 @@ pvoteHelper = phoistAcyclic $
     -- This puts trust into the Proposal. The Proposal must necessarily check
     -- that this is not abused.
 
-    pguardC "Proposal ST spent" $
-      valProposalCtx # ctxF.proposalContext
-
     pguardC "Correct outputs" $
-      ponlyLocksUpdated # ctx
+      ponlyLocksUpdated # (valProposalCtx # ctxF.proposalContext) # ctx
 
     pure $ pconstant ()
 
+paddNewLock ::
+  forall (s :: S).
+  Term
+    s
+    ( PProposalLock
+        :--> PBuiltinList (PAsData PProposalLock)
+        :--> PBuiltinList (PAsData PProposalLock)
+    )
+paddNewLock = phoistAcyclic $ plam $ \newLock -> pcons # pdata newLock
+
 {- | Default implementation of 'Agora.Stake.PermitVote'.
 
      @since 1.0.0
@@ -141,11 +166,41 @@ ppermitVote :: forall (s :: S). Term s PStakeRedeemerHandler
 ppermitVote = pvoteHelper #$ phoistAcyclic $
   plam $
     flip pmatch $ \case
-      PWithProposalRedeemer r -> pmatch r $ \case
-        PVote _ -> pconstant True
-        _ -> ptrace "Expected Vote" $ pconstant False
-      PNewProposal -> pconstant True
-      _ -> pconstant False
+      PSpendProposal pid _ r -> pmatch r $ \case
+        PVote ((pfromData . (pfield @"resultTag" #)) -> voteFor) ->
+          let newLock =
+                mkRecordConstr
+                  PVoted
+                  ( #votedOn .= pdata pid
+                      .& #votedFor .= pdata voteFor
+                  )
+           in paddNewLock # newLock
+        _ -> ptraceError "Expected Vote"
+      PNewProposal pid ->
+        let newLock =
+              mkRecordConstr
+                PCreated
+                ( #created .= pdata pid
+                )
+         in paddNewLock # newLock
+      _ -> ptraceError "Expected proposal"
+
+premoveLocks ::
+  forall (s :: S).
+  Term
+    s
+    ( PProposalId :--> PBool
+        :--> PBuiltinList (PAsData PProposalLock)
+        :--> PBuiltinList (PAsData PProposalLock)
+    )
+premoveLocks = phoistAcyclic $
+  plam $ \pid rc ->
+    pfilter
+      # plam
+        ( \(pfromData -> l) -> pnot #$ pmatch l $ \case
+            PCreated ((pfield @"created" #) -> pid') -> rc #&& pid' #== pid
+            PVoted ((pfield @"votedOn" #) -> pid') -> pid' #== pid
+        )
 
 {- | Default implementation of 'Agora.Stake.RetractVotes'.
 
@@ -155,10 +210,13 @@ pretractVote :: forall (s :: S). Term s PStakeRedeemerHandler
 pretractVote = pvoteHelper #$ phoistAcyclic $
   plam $
     flip pmatch $ \case
-      PWithProposalRedeemer r -> pmatch r $ \case
-        PUnlock _ -> pconstant True
-        _ -> ptrace "Expected Unlock" $ pconstant False
-      _ -> pconstant False
+      PSpendProposal pid s r -> pmatch r $ \case
+        PUnlock _ ->
+          let allowRemovingCreatorLock =
+                s #== pconstant Finished
+           in premoveLocks # pid # allowRemovingCreatorLock
+        _ -> ptraceError "Expected unlock"
+      _ -> ptraceError "Expected spending proposal"
 
 -- | Validation logic shared by 'pdelegateTo' and 'pclearDelegate'.
 pdelegateHelper ::
diff --git a/agora/Agora/Stake/Scripts.hs b/agora/Agora/Stake/Scripts.hs
index df8931f..57e57fb 100644
--- a/agora/Agora/Stake/Scripts.hs
+++ b/agora/Agora/Stake/Scripts.hs
@@ -12,7 +12,7 @@ module Agora.Stake.Scripts (
 ) where
 
 import Agora.Credential (authorizationContext, pauthorizedBy)
-import Agora.Proposal (PProposalRedeemer)
+import Agora.Proposal (PProposalDatum, PProposalRedeemer)
 import Agora.SafeMoney (GTTag)
 import Agora.Scripts (
   AgoraScripts,
@@ -23,7 +23,7 @@ import Agora.Stake (
   PProposalContext (
     PNewProposal,
     PNoProposal,
-    PWithProposalRedeemer
+    PSpendProposal
   ),
   PSigContext (PSigContext),
   PSignedBy (
@@ -73,10 +73,8 @@ import Plutarch.Api.V2 (
   AmountGuarantees,
   PMintingPolicy,
   PScriptPurpose (PMinting, PSpending),
-  PTxInInfo,
   PTxInfo,
   PTxOut,
-  PTxOutRef,
   PValidator,
  )
 import Plutarch.Extra.AssetClass (
@@ -84,14 +82,14 @@ import Plutarch.Extra.AssetClass (
   passetClassValueOf,
   pvalueOf,
  )
-import Plutarch.Extra.Bind (PBind ((#>>=)))
 import Plutarch.Extra.Category (PSemigroupoid ((#>>>)))
+import Plutarch.Extra.Field (pletAll)
 import Plutarch.Extra.Functor (PFunctor (pfmap))
 import "liqwid-plutarch-extra" Plutarch.Extra.List (pfindJust, pmapMaybe)
 import Plutarch.Extra.Maybe (
   passertPJust,
+  pfromMaybe,
   pjust,
-  pmaybe,
   pmaybeData,
   pnothing,
  )
@@ -402,9 +400,9 @@ mkStakeValidator
       pguardC "No new SST minted" $
         foldl1
           (#||)
-          [ ptraceIfFalse "All stakes burnt" $
+          [ ptraceIfTrue "All stakes burnt" $
               mintedST #< 0 #&& pnull # stakeOutputDatums
-          , ptraceIfFalse "Nothing burnt" $
+          , ptraceIfTrue "Nothing burnt" $
               mintedST #== 0
           ]
 
@@ -420,42 +418,67 @@ mkStakeValidator
             # pconstant propCs
             # pconstant propTn
 
+      getProposalDatum <- pletC $
+        plam $
+          flip pletAll $ \txOutF ->
+            let isProposalUTxO =
+                  passetClassValueOf
+                    # txOutF.value
+                    # proposalSTClass #== 1
+                proposalDatum =
+                  pfromData $
+                    pfromOutputDatum @(PAsData PProposalDatum)
+                      # txOutF.datum
+                      # txInfoF.datums
+             in pif isProposalUTxO (pjust # proposalDatum) pnothing
+
       let pstMinted =
             passetClassValueOf # txInfoF.mint # proposalSTClass #== 1
 
+          newProposalContext =
+            pcon $
+              PNewProposal $
+                pfield @"proposalId"
+                  #$ passertPJust # "Proposal output should present"
+                  #$ pfindJust # getProposalDatum # pfromData txInfoF.outputs
+
+          spendProposalContext =
+            let getProposalRedeemer = plam $ \ref ->
+                  flip (ptryFrom @PProposalRedeemer) fst $
+                    pto $
+                      passertPJust
+                        # "Malformed script context: propsoal input not found in redeemer map"
+                          #$ plookup
+                        # pcon
+                          ( PSpending $
+                              pdcons @_0
+                                # pdata ref
+                                # pdnil
+                          )
+                        # txInfoF.redeemers
+
+                getContext = plam $
+                  flip pletAll $ \inInfoF ->
+                    pfmap
+                      # plam
+                        ( \proposalDatum ->
+                            let id = pfield @"proposalId" # proposalDatum
+                                status = pfield @"status" # proposalDatum
+                                redeemer = getProposalRedeemer # inInfoF.outRef
+                             in pcon $ PSpendProposal id status redeemer
+                        )
+                      #$ getProposalDatum
+                      # pfromData inInfoF.resolved
+             in pfindJust # getContext # pfromData txInfoF.inputs
+
+          noProposalContext = pcon PNoProposal
+
       proposalContext <-
         pletC $
-          let convertRedeemer = plam $ \(pto -> dt) ->
-                ptryFrom @PProposalRedeemer dt fst
-
-              findRedeemer = plam $ \ref ->
-                plookup
-                  # pcon
-                    ( PSpending $
-                        pdcons @_0
-                          # pdata ref
-                          # pdnil
-                    )
-                  # txInfoF.redeemers
-
-              f :: Term _ (PTxInInfo :--> PMaybe PTxOutRef)
-              f = plam $ \inInfo ->
-                let value = pfield @"value" #$ pfield @"resolved" # inInfo
-                    ref = pfield @"outRef" # inInfo
-                 in pif
-                      (passetClassValueOf # value # proposalSTClass #== 1)
-                      (pjust # ref)
-                      pnothing
-
-              proposalRef = pfindJust # f # txInfoF.inputs
-           in pif pstMinted (pcon PNewProposal) $
-                pmaybe
-                  # pcon PNoProposal
-                  # plam
-                    ( \((convertRedeemer #) -> proposalRedeemer) ->
-                        pcon $ PWithProposalRedeemer proposalRedeemer
-                    )
-                  #$ proposalRef #>>= findRedeemer
+          pif
+            pstMinted
+            newProposalContext
+            (pfromMaybe # noProposalContext # spendProposalContext)
 
       --------------------------------------------------------------------------