diff --git a/agora/Agora/AuthorityToken.hs b/agora/Agora/AuthorityToken.hs
index 57baf46..241ad13 100644
--- a/agora/Agora/AuthorityToken.hs
+++ b/agora/Agora/AuthorityToken.hs
@@ -145,7 +145,7 @@ authorityTokenPolicy params =
         ( P.do
             passert "Parent token did not move in minting GATs" govTokenSpent
             passert "All outputs only emit valid GATs" $
-              allOutputs @PUnit # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
+              allOutputs @PData # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
                 authorityTokensValidIn
                   # ownSymbol
                   # txOut
diff --git a/agora/Agora/Proposal.hs b/agora/Agora/Proposal.hs
index 8fcaa43..a383b00 100644
--- a/agora/Agora/Proposal.hs
+++ b/agora/Agora/Proposal.hs
@@ -26,6 +26,9 @@ module Agora.Proposal (
   PProposalVotes (..),
   PProposalId (..),
   PResultTag (..),
+
+  -- * Plutarch helpers
+  proposalDatumValid,
 ) where
 
 import GHC.Generics qualified as GHC
@@ -41,13 +44,17 @@ import PlutusTx.AssocMap qualified as AssocMap
 
 --------------------------------------------------------------------------------
 import Agora.SafeMoney (GTTag)
+import Agora.Utils (pnotNull)
+import Control.Applicative (Const)
 import Control.Arrow (first)
+import Plutarch.Builtin (PBuiltinMap)
 import Plutarch.DataRepr (DerivePConstantViaData (..), PDataFields, PIsDataReprInstances (..))
 import Plutarch.Lift (
   DerivePConstantViaNewtype (..),
   PConstantDecl,
   PUnsafeLiftDecl (..),
  )
+import Plutarch.Monadic qualified as P
 import Plutarch.SafeMoney (PDiscrete, Tagged)
 import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
 import Plutarch.Unsafe (punsafeCoerce)
@@ -348,6 +355,12 @@ newtype PProposalDatum (s :: S) = PProposalDatum
     (PlutusType, PIsData, PDataFields)
     via (PIsDataReprInstances PProposalDatum)
 
+-- TODO: Derive this.
+instance PTryFrom PData (PAsData PProposalDatum) where
+  type PTryFromExcess PData (PAsData PProposalDatum) = Const ()
+  ptryFrom' d k =
+    k (punsafeCoerce d, ())
+
 instance PUnsafeLiftDecl PProposalDatum where type PLifted PProposalDatum = ProposalDatum
 deriving via (DerivePConstantViaData ProposalDatum PProposalDatum) instance (PConstantDecl ProposalDatum)
 
@@ -364,6 +377,12 @@ data PProposalRedeemer (s :: S)
     (PlutusType, PIsData)
     via PIsDataReprInstances PProposalRedeemer
 
+-- See below.
+instance PTryFrom PData (PAsData PProposalRedeemer) where
+  type PTryFromExcess PData (PAsData PProposalRedeemer) = Const ()
+  ptryFrom' d k =
+    k (punsafeCoerce d, ())
+
 -- TODO: Waiting on PTryFrom for 'PPubKeyHash'
 -- deriving via
 --   PAsData (PIsDataReprInstances PProposalRedeemer)
@@ -372,3 +391,34 @@ data PProposalRedeemer (s :: S)
 
 instance PUnsafeLiftDecl PProposalRedeemer where type PLifted PProposalRedeemer = ProposalRedeemer
 deriving via (DerivePConstantViaData ProposalRedeemer PProposalRedeemer) instance (PConstantDecl ProposalRedeemer)
+
+--------------------------------------------------------------------------------
+
+{- | Check for various invariants a proposal must uphold.
+     This can be used to check both upopn creation and
+     upon any following state transitions in the proposal.
+-}
+proposalDatumValid :: Term s (Agora.Proposal.PProposalDatum :--> PBool)
+proposalDatumValid =
+  phoistAcyclic $
+    plam $ \datum' -> P.do
+      datum <- pletFields @'["effects", "cosigners"] $ datum'
+
+      let effects :: Term _ (PBuiltinMap Agora.Proposal.PResultTag (PBuiltinMap Plutarch.Api.V1.PValidatorHash Plutarch.Api.V1.PDatumHash))
+          effects =
+            -- JUSTIFICATION:
+            -- @datum.effects : PMap PResultTag (PMap PValidatorHash PDatumHash)@
+            -- @PMap PResultTag (PMap PValidatorHash PDatumHash)@ is equivalent to
+            -- @PBuiltinMap PResultTag (PBuiltinMap Plutarch.Api.V1.PValidatorHash Plutarch.Api.V1.PDatumHash)@
+            punsafeCoerce datum.effects
+
+          atLeastOneNegativeResult :: Term _ PBool
+          atLeastOneNegativeResult =
+            pany # plam (\pair -> pnull #$ pfromData $ psndBuiltin # pair) # effects
+
+      foldr1
+        (#&&)
+        [ ptraceIfFalse "Proposal has at least one ResultTag has no effects" atLeastOneNegativeResult
+        , ptraceIfFalse "Proposal has at least one cosigner" $ pnotNull # pfromData datum.cosigners
+        , ptraceIfFalse "Proposal has at most five cosigners" $ plength # (pfromData datum.cosigners) #< 6
+        ]
diff --git a/agora/Agora/Proposal/Scripts.hs b/agora/Agora/Proposal/Scripts.hs
index 417f577..44612be 100644
--- a/agora/Agora/Proposal/Scripts.hs
+++ b/agora/Agora/Proposal/Scripts.hs
@@ -8,13 +8,11 @@ Plutus Scripts for Proposals.
 module Agora.Proposal.Scripts (
   proposalValidator,
   proposalPolicy,
-  proposalDatumValid,
 ) where
 
 import Agora.Proposal (
   PProposalDatum (PProposalDatum),
   PProposalRedeemer (..),
-  PResultTag,
   Proposal (governorSTAssetClass, stakeSTAssetClass),
  )
 import Agora.Record (mkRecordConstr, (.&), (.=))
@@ -23,27 +21,23 @@ import Agora.Utils (
   anyOutput,
   findTxOutByTxOutRef,
   passert,
-  pnotNull,
   psymbolValueOf,
   ptokenSpent,
   ptxSignedBy,
   pvalueSpent,
  )
 import Plutarch.Api.V1 (
-  PDatumHash,
   PMintingPolicy,
   PScriptContext (PScriptContext),
   PScriptPurpose (PMinting, PSpending),
   PTxInfo (PTxInfo),
   PValidator,
-  PValidatorHash,
   mintingPolicySymbol,
   mkMintingPolicy,
  )
 import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
-import Plutarch.Builtin (PBuiltinMap)
 import Plutarch.Monadic qualified as P
-import Plutarch.Unsafe (punsafeCoerce)
+import Plutarch.TryFrom (ptryFrom)
 import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
 
 {- | Policy for Proposals.
@@ -94,10 +88,8 @@ proposalValidator proposal =
     PJust txOut <- pmatch $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
     txOutF <- pletFields @'["address", "value"] $ txOut
 
-    let proposalDatum :: Term _ Agora.Proposal.PProposalDatum
-        proposalDatum = pfromData $ punsafeCoerce datum
-        proposalRedeemer :: Term _ Agora.Proposal.PProposalRedeemer
-        proposalRedeemer = pfromData $ punsafeCoerce redeemer
+    (pfromData -> proposalDatum, _) <- ptryFrom @(PAsData PProposalDatum) datum
+    (pfromData -> proposalRedeemer, _) <- ptryFrom @(PAsData PProposalRedeemer) redeemer
 
     proposalF <-
       pletFields
@@ -189,27 +181,3 @@ proposalValidator proposal =
           spentST #== 1
 
         popaque (pconstant ())
-
-{- | Check for various invariants a proposal must uphold.
-     This can be used to check both upopn creation and
-     upon any following state transitions in the proposal.
--}
-proposalDatumValid :: Term s (Agora.Proposal.PProposalDatum :--> PBool)
-proposalDatumValid =
-  phoistAcyclic $
-    plam $ \datum' -> P.do
-      datum <- pletFields @'["effects", "cosigners"] $ datum'
-
-      let effects :: Term _ (PBuiltinMap Agora.Proposal.PResultTag (PBuiltinMap Plutarch.Api.V1.PValidatorHash Plutarch.Api.V1.PDatumHash))
-          effects = punsafeCoerce datum.effects
-
-          atLeastOneNegativeResult :: Term _ PBool
-          atLeastOneNegativeResult =
-            pany # plam (\pair -> pnull #$ pfromData $ psndBuiltin # pair) # effects
-
-      foldr1
-        (#&&)
-        [ ptraceIfFalse "Proposal has at least one ResultTag has no effects" atLeastOneNegativeResult
-        , ptraceIfFalse "Proposal has at least one cosigner" $ pnotNull # pfromData datum.cosigners
-        , ptraceIfFalse "Proposal has at most five cosigners" $ plength # (pfromData datum.cosigners) #< 6
-        ]
diff --git a/agora/Agora/Stake.hs b/agora/Agora/Stake.hs
index 6788f91..b25a7ef 100644
--- a/agora/Agora/Stake.hs
+++ b/agora/Agora/Stake.hs
@@ -61,16 +61,17 @@ import Plutus.V1.Ledger.Value (AssetClass)
 import Agora.Proposal (PProposalId, PResultTag, ProposalId (..), ResultTag (..))
 import Agora.SafeMoney (GTTag)
 import Agora.Utils (
-  pfindDatum,
   pnotNull,
+  ptryFindDatum,
  )
+import Control.Applicative (Const)
 import Plutarch.Api.V1.Extra (PAssetClass, passetClassValueOf)
 import Plutarch.Numeric ()
 import Plutarch.SafeMoney (
   PDiscrete,
   Tagged (..),
  )
-import Plutarch.TryFrom (PTryFrom)
+import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
 
 --------------------------------------------------------------------------------
 
@@ -191,6 +192,11 @@ newtype PStakeDatum (s :: S) = PStakeDatum
     (PlutusType, PIsData, PDataFields)
     via (PIsDataReprInstances PStakeDatum)
 
+instance PTryFrom PData (PAsData PStakeDatum) where
+  type PTryFromExcess PData (PAsData PStakeDatum) = Const ()
+  ptryFrom' d k =
+    k (punsafeCoerce d, ())
+
 instance PUnsafeLiftDecl PStakeDatum where type PLifted PStakeDatum = StakeDatum
 deriving via (DerivePConstantViaData StakeDatum PStakeDatum) instance (PConstantDecl StakeDatum)
 
@@ -262,7 +268,7 @@ findStakeOwnedBy ::
         :--> PPubKeyHash
         :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum))
         :--> PBuiltinList (PAsData PTxInInfo)
-        :--> PMaybe PTxOut
+        :--> PMaybe (PAsData PStakeDatum)
     )
 findStakeOwnedBy = phoistAcyclic $
   plam $ \ac pk datums inputs ->
@@ -273,9 +279,8 @@ findStakeOwnedBy = phoistAcyclic $
         txOutF <- pletFields @'["datumHash"] $ txOut
         pmatch txOutF.datumHash $ \case
           PDNothing _ -> pcon PNothing
-          PDJust ((pfield @"_0" #) -> dh) ->
-            -- TODO: PTryFrom here
-            punsafeCoerce $ pfindDatum # dh # datums
+          PDJust ((pfield @"_0" #) -> dh) -> P.do
+            ptryFindDatum @(PAsData PStakeDatum) # dh # datums
 
 stakeDatumOwnedBy :: Term _ (PPubKeyHash :--> PStakeDatum :--> PBool)
 stakeDatumOwnedBy =
@@ -304,8 +309,7 @@ isInputStakeOwnedBy =
       PDJust ((pfield @"_0" #) -> datumHash) ->
         pif
           (outStakeST #== 1)
-          -- TODO: use 'ptryFindDatum' instead in the future
-          ( pmatch (pfindDatum # datumHash # datums) $ \case
+          ( pmatch (ptryFindDatum @(PAsData PStakeDatum) # datumHash # datums) $ \case
               PNothing -> pcon PFalse
               PJust v -> stakeDatumOwnedBy # ss # pfromData (punsafeCoerce v)
           )
diff --git a/agora/Agora/Stake/Scripts.hs b/agora/Agora/Stake/Scripts.hs
index 44cefac..2f80d66 100644
--- a/agora/Agora/Stake/Scripts.hs
+++ b/agora/Agora/Stake/Scripts.hs
@@ -35,7 +35,7 @@ import Plutarch.Api.V1 (
   mintingPolicySymbol,
   mkMintingPolicy,
  )
-import Plutarch.Api.V1.Extra (passetClass)
+import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
 import Plutarch.Internal (punsafeCoerce)
 import Plutarch.Monadic qualified as P
 import Plutarch.Numeric
@@ -183,7 +183,12 @@ stakeValidator stake =
 
     stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake.gtClassRef)
     mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfoF.mint
-    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfoF.inputs
+    valueSpent <- plet $ pvalueSpent # txInfoF.inputs
+    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
+
+    let AssetClass (propCs, propTn) = stake.proposalSTClass
+        proposalSTClass = passetClass # pconstant propCs # pconstant propTn
+    spentProposalST <- plet $ passetClassValueOf # valueSpent # proposalSTClass
 
     -- Is the stake currently locked?
     stakeIsLocked <- plet $ stakeLocked # stakeDatum'
@@ -192,26 +197,76 @@ stakeValidator stake =
       PDestroy _ -> P.do
         passert "ST at inputs must be 1" $
           spentST #== 1
+
         passert "Should burn ST" $
           mintedST #== -1
+
         passert "Stake unlocked" $ pnot # stakeIsLocked
-        passert
-          "Owner signs this transaction"
-          ownerSignsTransaction
+
+        passert "Owner signs this transaction" ownerSignsTransaction
+
         popaque (pconstant ())
       --------------------------------------------------------------------------
       PRetractVotes _ -> P.do
         passert
           "Owner signs this transaction"
           ownerSignsTransaction
-        -- TODO: check proposal constraints
+
+        passert "ST at inputs must be 1" $
+          spentST #== 1
+
+        -- This puts trust into the Proposal. The Proposal must necessarily check
+        -- that this is not abused.
+        passert "Proposal ST spent" $
+          spentProposalST #== 1
+
+        passert "A UTXO must exist with the correct output" $
+          anyOutput @PStakeDatum # txInfo
+            #$ plam
+            $ \value address newStakeDatum' -> P.do
+              let isScriptAddress = pdata address #== ownAddress
+              let _correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
+              let valueCorrect = pdata continuingValue #== pdata value
+              pif
+                isScriptAddress
+                ( foldl1
+                    (#&&)
+                    [ ptraceIfFalse "valueCorrect" valueCorrect
+                    ]
+                )
+                (pcon PFalse)
+
         popaque (pconstant ())
       --------------------------------------------------------------------------
       PPermitVote _ -> P.do
         passert
           "Owner signs this transaction"
           ownerSignsTransaction
-        -- TODO: check proposal constraints
+
+        passert "ST at inputs must be 1" $
+          spentST #== 1
+
+        -- This puts trust into the Proposal. The Proposal must necessarily check
+        -- that this is not abused.
+        passert "Proposal ST spent" $
+          spentProposalST #== 1
+
+        passert "A UTXO must exist with the correct output" $
+          anyOutput @PStakeDatum # txInfo
+            #$ plam
+            $ \value address newStakeDatum' -> P.do
+              let isScriptAddress = pdata address #== ownAddress
+              let _correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
+              let valueCorrect = pdata continuingValue #== pdata value
+              pif
+                isScriptAddress
+                ( foldl1
+                    (#&&)
+                    [ ptraceIfFalse "valueCorrect" valueCorrect
+                    ]
+                )
+                (pcon PFalse)
+
         popaque (pconstant ())
       --------------------------------------------------------------------------
       PWitnessStake _ -> P.do
@@ -225,6 +280,9 @@ stakeValidator stake =
                 # propAssetClass
                 # txInfoF.inputs
 
+        -- In order for cosignature to be witnessed, it must be possible for a
+        -- proposal to allow this transaction to happen. This puts trust into the Proposal.
+        -- The Proposal must necessarily check that this is not abused.
         passert
           "Owner signs this transaction OR proposal token is spent"
           (ownerSignsTransaction #|| proposalTokenMoved)
diff --git a/agora/Agora/Utils.hs b/agora/Agora/Utils.hs
index f60c853..0f60dde 100644
--- a/agora/Agora/Utils.hs
+++ b/agora/Agora/Utils.hs
@@ -84,7 +84,7 @@ pfindDatum = phoistAcyclic $
   plam $ \datumHash datums -> plookupTuple # datumHash # datums
 
 -- | Find a datum with the given hash, and `ptryFrom` it.
-ptryFindDatum :: PTryFrom PData a => Term s (PDatumHash :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PMaybe a)
+ptryFindDatum :: forall (a :: PType) (s :: S). PTryFrom PData a => Term s (PDatumHash :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PMaybe a)
 ptryFindDatum = phoistAcyclic $
   plam $ \datumHash inputs -> P.do
     pmatch (pfindDatum # datumHash # inputs) $ \case
@@ -326,6 +326,7 @@ ptokenSpent =
 anyOutput ::
   forall (datum :: PType) s.
   ( PIsData datum
+  , PTryFrom PData (PAsData datum)
   ) =>
   Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
 anyOutput = phoistAcyclic $
@@ -337,7 +338,7 @@ anyOutput = phoistAcyclic $
             PTxOut txOut' <- pmatch (pfromData txOut'')
             txOut <- pletFields @'["value", "datumHash", "address"] txOut'
             PDJust dh <- pmatch txOut.datumHash
-            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo.datums) $ \case
+            pmatch (ptryFindDatum @(PAsData datum) # (pfield @"_0" # dh) # txInfo.datums) $ \case
               PJust datum -> P.do
                 predicate # txOut.value # txOut.address # pfromData datum
               PNothing -> pcon PFalse
@@ -348,6 +349,7 @@ anyOutput = phoistAcyclic $
 allOutputs ::
   forall (datum :: PType) s.
   ( PIsData datum
+  , PTryFrom PData (PAsData datum)
   ) =>
   Term s (PTxInfo :--> (PTxOut :--> PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
 allOutputs = phoistAcyclic $
@@ -359,7 +361,7 @@ allOutputs = phoistAcyclic $
             PTxOut txOut' <- pmatch (pfromData txOut'')
             txOut <- pletFields @'["value", "datumHash", "address"] txOut'
             PDJust dh <- pmatch txOut.datumHash
-            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo.datums) $ \case
+            pmatch (ptryFindDatum @(PAsData datum) # (pfield @"_0" # dh) # txInfo.datums) $ \case
               PJust datum -> P.do
                 predicate # pfromData txOut'' # txOut.value # txOut.address # pfromData datum
               PNothing -> pcon PFalse
diff --git a/docs/tech-design/proposals.md b/docs/tech-design/proposals.md
index a3a3fb1..6098795 100644
--- a/docs/tech-design/proposals.md
+++ b/docs/tech-design/proposals.md
@@ -4,7 +4,7 @@ This document gives an overview of the technical design of the proposals system
 
 | Specification | Implementation | Last revision |
 |:-----------:|:-----------:|:-------------:|
-| WIP         |  WIP        | v0.1 2022-04-11    |
+| WIP         |  WIP        | v0.1 2022-04-27    |
 
 ---
 
@@ -35,7 +35,12 @@ Initiating a proposal requires the proposer to have more than a certain amount o
 
 ### Voting stages
 
-The life-cycle of a proposal is neatly represented by a state machine, with the 'draft' phase being the initial state, and 'executed' and 'failed' being the terminating states. Please note that this state-machine representation is purely conceptual and should not be expected to reflect technical implementation.
+The life-cycle of a proposal is neatly represented by a state machine, with the 'draft' phase being the initial state, and 'executed' and 'failed' being the terminating states.
+
+**Please note that this state-machine representation is purely conceptual and should not be expected to reflect technical implementation.** This is because some state transitions in the state machine representation don't need to happen in the actual implementation as a transaction. A key example is going from the "lock" phase to the "execution" phase. The only thing that needs to happen is that time goes by. So under the hood, they are represented the same in the Proposal's datum.
+
+> Emily 2022-04-27: This is quite confusing still, I feel. @Jack, could you try to reword this and make it more clear?
+
 
 ![](../diagrams/ProposalStateMachine.svg)