diff --git a/Makefile b/Makefile
index da13647..6a3164c 100644
--- a/Makefile
+++ b/Makefile
@@ -10,6 +10,7 @@ usage:
 	@echo "  hoogle -- Start local hoogle"
 	@echo "  format -- Format the project"
 	@echo "  haddock -- Generate Haddock docs for project"
+	@echo "  tag -- Generate CTAGS and ETAGS files for project"
 
 hoogle:
 	pkill hoogle || true
@@ -35,3 +36,7 @@ format_check:
 
 haddock:
 	cabal haddock --haddock-html --haddock-hoogle --builddir=haddock
+
+tag:
+	hasktags -x agora agora-bench agora-test
+
diff --git a/agora-test/Spec.hs b/agora-test/Spec.hs
index 40a7b7f..22c5b49 100644
--- a/agora-test/Spec.hs
+++ b/agora-test/Spec.hs
@@ -11,6 +11,7 @@ import Test.Tasty (defaultMain, testGroup)
 import Spec.AuthorityToken qualified as AuthorityToken
 import Spec.Effect.TreasuryWithdrawal qualified as TreasuryWithdrawal
 import Spec.Model.MultiSig qualified as MultiSig
+import Spec.Proposal qualified as Proposal
 import Spec.Stake qualified as Stake
 
 -- | The Agora test suite.
@@ -28,6 +29,9 @@ main =
       , testGroup
           "Stake tests"
           Stake.tests
+      , testGroup
+          "Proposal tests"
+          Proposal.tests
       , testGroup
           "Multisig tests"
           [ testGroup
diff --git a/agora-test/Spec/Effect/TreasuryWithdrawal.hs b/agora-test/Spec/Effect/TreasuryWithdrawal.hs
index db0aed6..27310d9 100644
--- a/agora-test/Spec/Effect/TreasuryWithdrawal.hs
+++ b/agora-test/Spec/Effect/TreasuryWithdrawal.hs
@@ -7,6 +7,11 @@ This module tests the Treasury Withdrawal Effect.
 -}
 module Spec.Effect.TreasuryWithdrawal (tests) where
 
+import Agora.Effect.TreasuryWithdrawal (
+  TreasuryWithdrawalDatum (TreasuryWithdrawalDatum),
+  treasuryWithdrawalValidator,
+ )
+import Plutus.V1.Ledger.Value qualified as Value
 import Spec.Sample.Effect.TreasuryWithdrawal (
   buildReceiversOutputFromDatum,
   buildScriptContext,
@@ -20,15 +25,7 @@ import Spec.Sample.Effect.TreasuryWithdrawal (
   treasuries,
   users,
  )
-
-import Agora.Effect.TreasuryWithdrawal (
-  TreasuryWithdrawalDatum (TreasuryWithdrawalDatum),
-  treasuryWithdrawalValidator,
- )
-
-import Plutus.V1.Ledger.Value qualified as Value
 import Spec.Util (effectFailsWith, effectSucceedsWith)
-
 import Test.Tasty (TestTree, testGroup)
 
 tests :: [TestTree]
diff --git a/agora-test/Spec/Proposal.hs b/agora-test/Spec/Proposal.hs
new file mode 100644
index 0000000..bd79762
--- /dev/null
+++ b/agora-test/Spec/Proposal.hs
@@ -0,0 +1,91 @@
+{-# LANGUAGE QuasiQuotes #-}
+
+{- |
+Module     : Spec.Proposal
+Maintainer : emi@haskell.fyi
+Description: Tests for Proposal policy and validator
+
+Tests for Proposal policy and validator
+-}
+module Spec.Proposal (tests) where
+
+--------------------------------------------------------------------------------
+
+import Agora.Proposal (
+  ProposalDatum (ProposalDatum),
+  ProposalId (ProposalId),
+  ProposalRedeemer (Cosign),
+  ProposalStatus (Draft),
+  ResultTag (ResultTag),
+  cosigners,
+  effects,
+  emptyVotesFor,
+  proposalId,
+  status,
+  thresholds,
+  votes,
+ )
+import Agora.Proposal.Scripts (
+  proposalPolicy,
+  proposalValidator,
+ )
+import Agora.Stake (StakeDatum (StakeDatum), StakeRedeemer (WitnessStake))
+import Agora.Stake.Scripts (stakeValidator)
+import Plutarch.SafeMoney (Tagged (Tagged))
+import Plutus.V1.Ledger.Api (ScriptContext (..), ScriptPurpose (..))
+import PlutusTx.AssocMap qualified as AssocMap
+import Spec.Sample.Proposal qualified as Proposal
+import Spec.Sample.Shared (signer, signer2)
+import Spec.Sample.Shared qualified as Shared
+import Spec.Util (policySucceedsWith, validatorSucceedsWith)
+import Test.Tasty (TestTree, testGroup)
+
+--------------------------------------------------------------------------------
+
+-- | Stake tests.
+tests :: [TestTree]
+tests =
+  [ testGroup
+      "policy"
+      [ policySucceedsWith
+          "proposalCreation"
+          (proposalPolicy Shared.proposal)
+          ()
+          Proposal.proposalCreation
+      ]
+  , testGroup
+      "validator"
+      [ testGroup
+          "cosignature"
+          [ validatorSucceedsWith
+              "proposal"
+              (proposalValidator Shared.proposal)
+              ( ProposalDatum
+                  { proposalId = ProposalId 0
+                  , effects =
+                      AssocMap.fromList
+                        [ (ResultTag 0, [])
+                        , (ResultTag 1, [])
+                        ]
+                  , status = Draft
+                  , cosigners = [signer]
+                  , thresholds = Shared.defaultProposalThresholds
+                  , votes =
+                      emptyVotesFor $
+                        AssocMap.fromList
+                          [ (ResultTag 0, [])
+                          , (ResultTag 1, [])
+                          ]
+                  }
+              )
+              (Cosign [signer2])
+              (ScriptContext (Proposal.cosignProposal [signer2]) (Spending Proposal.proposalRef))
+          , validatorSucceedsWith
+              "stake"
+              (stakeValidator Shared.stake)
+              (StakeDatum (Tagged 50_000_000) signer2 [])
+              WitnessStake
+              (ScriptContext (Proposal.cosignProposal [signer2]) (Spending Proposal.stakeRef))
+          ]
+      ]
+  ]
diff --git a/agora-test/Spec/Sample/Proposal.hs b/agora-test/Spec/Sample/Proposal.hs
new file mode 100644
index 0000000..6112ec0
--- /dev/null
+++ b/agora-test/Spec/Sample/Proposal.hs
@@ -0,0 +1,234 @@
+{- |
+Module     : Spec.Sample.Proposal
+Maintainer : emi@haskell.fyi
+Description: Sample based testing for Proposal utxos
+
+This module tests primarily the happy path for Proposal interactions
+-}
+module Spec.Sample.Proposal (
+  -- * Script contexts
+  proposalCreation,
+  cosignProposal,
+  proposalRef,
+  stakeRef,
+) where
+
+--------------------------------------------------------------------------------
+import Plutarch.Api.V1 (
+  validatorHash,
+ )
+import Plutus.V1.Ledger.Api (
+  Address (Address),
+  Credential (ScriptCredential),
+  Datum (Datum),
+  PubKeyHash,
+  ScriptContext (..),
+  ScriptPurpose (..),
+  ToData (toBuiltinData),
+  TxInInfo (TxInInfo),
+  TxInfo (..),
+  TxOut (TxOut, txOutAddress, txOutDatumHash, txOutValue),
+  TxOutRef (TxOutRef),
+ )
+import Plutus.V1.Ledger.Interval qualified as Interval
+import Plutus.V1.Ledger.Value qualified as Value
+
+--------------------------------------------------------------------------------
+
+import Agora.Governor (
+  GovernorDatum (GovernorDatum, nextProposalId, proposalThresholds),
+ )
+import Agora.Proposal (
+  Proposal (..),
+  ProposalDatum (..),
+  ProposalId (..),
+  ProposalStatus (..),
+  ResultTag (..),
+  emptyVotesFor,
+ )
+import Agora.Stake (Stake (..), StakeDatum (StakeDatum))
+import Plutarch.SafeMoney (Tagged (Tagged), untag)
+import PlutusTx.AssocMap qualified as AssocMap
+import Spec.Sample.Shared
+import Spec.Util (datumPair, toDatumHash)
+
+--------------------------------------------------------------------------------
+
+-- | This script context should be a valid transaction.
+proposalCreation :: ScriptContext
+proposalCreation =
+  let st = Value.singleton proposalPolicySymbol "" 1 -- Proposal ST
+      effects =
+        AssocMap.fromList
+          [ (ResultTag 0, [])
+          , (ResultTag 1, [])
+          ]
+      proposalDatum :: Datum
+      proposalDatum =
+        Datum
+          ( toBuiltinData $
+              ProposalDatum
+                { proposalId = ProposalId 0
+                , effects = effects
+                , status = Draft
+                , cosigners = [signer]
+                , thresholds = defaultProposalThresholds
+                , votes = emptyVotesFor effects
+                }
+          )
+
+      govBefore :: Datum
+      govBefore =
+        Datum
+          ( toBuiltinData $
+              GovernorDatum
+                { proposalThresholds = defaultProposalThresholds
+                , nextProposalId = ProposalId 0
+                }
+          )
+      govAfter :: Datum
+      govAfter =
+        Datum
+          ( toBuiltinData $
+              GovernorDatum
+                { proposalThresholds = defaultProposalThresholds
+                , nextProposalId = ProposalId 1
+                }
+          )
+   in ScriptContext
+        { scriptContextTxInfo =
+            TxInfo
+              { txInfoInputs =
+                  [ TxInInfo
+                      (TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1)
+                      TxOut
+                        { txOutAddress = Address (ScriptCredential $ validatorHash govValidator) Nothing
+                        , txOutValue = Value.assetClassValue proposal.governorSTAssetClass 1
+                        , txOutDatumHash = Just (toDatumHash govBefore)
+                        }
+                  ]
+              , txInfoOutputs =
+                  [ TxOut
+                      { txOutAddress = Address (ScriptCredential proposalValidatorHash) Nothing
+                      , txOutValue =
+                          mconcat
+                            [ st
+                            , Value.singleton "" "" 10_000_000
+                            ]
+                      , txOutDatumHash = Just (toDatumHash proposalDatum)
+                      }
+                  , TxOut
+                      { txOutAddress = Address (ScriptCredential $ validatorHash govValidator) Nothing
+                      , txOutValue =
+                          mconcat
+                            [ Value.assetClassValue proposal.governorSTAssetClass 1
+                            , Value.singleton "" "" 10_000_000
+                            ]
+                      , txOutDatumHash = Just (toDatumHash govAfter)
+                      }
+                  ]
+              , txInfoFee = Value.singleton "" "" 2
+              , txInfoMint = st
+              , txInfoDCert = []
+              , txInfoWdrl = []
+              , txInfoValidRange = Interval.always
+              , txInfoSignatories = [signer]
+              , txInfoData =
+                  [ datumPair proposalDatum
+                  , datumPair govBefore
+                  , datumPair govAfter
+                  ]
+              , txInfoId = "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
+              }
+        , scriptContextPurpose = Minting proposalPolicySymbol
+        }
+
+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 =
+  let st = Value.singleton proposalPolicySymbol "" 1 -- Proposal ST
+      effects =
+        AssocMap.fromList
+          [ (ResultTag 0, [])
+          , (ResultTag 1, [])
+          ]
+      proposalBefore :: ProposalDatum
+      proposalBefore =
+        ProposalDatum
+          { proposalId = ProposalId 0
+          , effects = effects
+          , status = Draft
+          , cosigners = [signer]
+          , thresholds = defaultProposalThresholds
+          , votes = emptyVotesFor effects
+          }
+      stakeDatum :: StakeDatum
+      stakeDatum = StakeDatum (Tagged 50_000_000) signer2 []
+      proposalAfter :: ProposalDatum
+      proposalAfter = proposalBefore {cosigners = newSigners <> proposalBefore.cosigners}
+   in TxInfo
+        { txInfoInputs =
+            [ TxInInfo
+                proposalRef
+                TxOut
+                  { txOutAddress = proposalValidatorAddress
+                  , txOutValue =
+                      mconcat
+                        [ st
+                        , Value.singleton "" "" 10_000_000
+                        ]
+                  , txOutDatumHash = Just (toDatumHash proposalBefore)
+                  }
+            , TxInInfo
+                stakeRef
+                TxOut
+                  { txOutAddress = stakeAddress
+                  , txOutValue =
+                      mconcat
+                        [ Value.singleton "" "" 10_000_000
+                        , Value.assetClassValue (untag stake.gtClassRef) 50_000_000
+                        , Value.singleton stakeSymbol "" 1
+                        ]
+                  , txOutDatumHash = Just (toDatumHash stakeDatum)
+                  }
+            ]
+        , txInfoOutputs =
+            [ TxOut
+                { txOutAddress = Address (ScriptCredential proposalValidatorHash) Nothing
+                , txOutValue =
+                    mconcat
+                      [ st
+                      , Value.singleton "" "" 10_000_000
+                      ]
+                , txOutDatumHash = Just (toDatumHash . Datum $ toBuiltinData proposalAfter)
+                }
+            , TxOut
+                { txOutAddress = stakeAddress
+                , txOutValue =
+                    mconcat
+                      [ Value.singleton "" "" 10_000_000
+                      , Value.assetClassValue (untag stake.gtClassRef) 50_000_000
+                      , Value.singleton stakeSymbol "" 1
+                      ]
+                , txOutDatumHash = Just (toDatumHash stakeDatum)
+                }
+            ]
+        , txInfoFee = Value.singleton "" "" 2
+        , txInfoMint = st
+        , txInfoDCert = []
+        , txInfoWdrl = []
+        , txInfoValidRange = Interval.always
+        , txInfoSignatories = newSigners
+        , txInfoData =
+            [ datumPair . Datum $ toBuiltinData proposalBefore
+            , datumPair . Datum $ toBuiltinData proposalAfter
+            , datumPair . Datum $ toBuiltinData stakeDatum
+            ]
+        , txInfoId = "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
+        }
diff --git a/agora-test/Spec/Sample/Shared.hs b/agora-test/Spec/Sample/Shared.hs
new file mode 100644
index 0000000..bd4957f
--- /dev/null
+++ b/agora-test/Spec/Sample/Shared.hs
@@ -0,0 +1,133 @@
+{- |
+Module     : Spec.Sample.Shared
+Maintainer : emi@haskell.fyi
+Description: Shared useful values for creating Samples for testing.
+
+Shared useful values for creating Samples for testing.
+-}
+module Spec.Sample.Shared (
+  -- * Misc
+  signer,
+  signer2,
+
+  -- * Components
+
+  -- ** Stake
+  stake,
+  stakeSymbol,
+  stakeValidatorHash,
+  stakeAddress,
+
+  -- ** Governor
+  governor,
+  govPolicy,
+  govValidator,
+  govSymbol,
+
+  -- ** Proposal
+  defaultProposalThresholds,
+  proposal,
+  proposalPolicySymbol,
+  proposalValidatorHash,
+  proposalValidatorAddress,
+) where
+
+import Agora.Governor (
+  Governor (Governor),
+  governorPolicy,
+  governorValidator,
+ )
+import Agora.Proposal (
+  Proposal (..),
+  ProposalThresholds (..),
+ )
+import Agora.Proposal.Scripts (
+  proposalPolicy,
+  proposalValidator,
+ )
+import Agora.Stake (Stake (..))
+import Agora.Stake.Scripts (stakePolicy, stakeValidator)
+import Plutarch.Api.V1 (
+  mintingPolicySymbol,
+  mkMintingPolicy,
+  mkValidator,
+  validatorHash,
+ )
+import Plutarch.SafeMoney
+import Plutus.V1.Ledger.Address (scriptHashAddress)
+import Plutus.V1.Ledger.Api (
+  Address (Address),
+  Credential (ScriptCredential),
+  CurrencySymbol,
+  MintingPolicy (..),
+  PubKeyHash,
+ )
+import Plutus.V1.Ledger.Scripts (Validator, ValidatorHash)
+import Plutus.V1.Ledger.Value qualified as Value
+
+--------------------------------------------------------------------------------
+
+stake :: Stake
+stake =
+  Stake
+    { gtClassRef =
+        Tagged $
+          Value.assetClass
+            "da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
+            "LQ"
+    , proposalSTClass = Value.assetClass proposalPolicySymbol ""
+    }
+
+stakeSymbol :: CurrencySymbol
+stakeSymbol = mintingPolicySymbol $ mkMintingPolicy $ stakePolicy stake.gtClassRef
+
+stakeValidatorHash :: ValidatorHash
+stakeValidatorHash = validatorHash $ mkValidator (stakeValidator stake)
+
+stakeAddress :: Address
+stakeAddress = Address (ScriptCredential stakeValidatorHash) Nothing
+
+governor :: Governor
+governor = Governor
+
+govPolicy :: MintingPolicy
+govPolicy = mkMintingPolicy (governorPolicy governor)
+
+govValidator :: Validator
+govValidator = mkValidator (governorValidator governor)
+
+govSymbol :: CurrencySymbol
+govSymbol = mintingPolicySymbol govPolicy
+
+proposal :: Proposal
+proposal =
+  Proposal
+    { governorSTAssetClass = Value.assetClass govSymbol ""
+    , stakeSTAssetClass = Value.assetClass stakeSymbol ""
+    , maximumCosigners = 6
+    }
+
+proposalPolicySymbol :: CurrencySymbol
+proposalPolicySymbol = mintingPolicySymbol $ mkMintingPolicy (proposalPolicy proposal)
+
+-- | A sample 'PubKeyHash'.
+signer :: PubKeyHash
+signer = "8a30896c4fd5e79843e4ca1bd2cdbaa36f8c0bc3be7401214142019c"
+
+-- | Another sample 'PubKeyHash'.
+signer2 :: PubKeyHash
+signer2 = "8a30896c4fd5e79843e4ca1bd2cdbaa36f8c0bc3be74012141420192"
+
+proposalValidatorHash :: ValidatorHash
+proposalValidatorHash = validatorHash (mkValidator $ proposalValidator proposal)
+
+proposalValidatorAddress :: Address
+proposalValidatorAddress = scriptHashAddress proposalValidatorHash
+
+defaultProposalThresholds :: ProposalThresholds
+defaultProposalThresholds =
+  ProposalThresholds
+    { countVoting = Tagged 1000
+    , create = Tagged 1
+    , startVoting = Tagged 10
+    }
diff --git a/agora-test/Spec/Sample/Stake.hs b/agora-test/Spec/Sample/Stake.hs
index 08bd0e1..07af063 100644
--- a/agora-test/Spec/Sample/Stake.hs
+++ b/agora-test/Spec/Sample/Stake.hs
@@ -7,8 +7,7 @@ This module tests primarily the happy path for Stake creation
 -}
 module Spec.Sample.Stake (
   stake,
-  policy,
-  policySymbol,
+  stakeSymbol,
   validatorHashTN,
   signer,
 
@@ -22,19 +21,14 @@ module Spec.Sample.Stake (
 
 --------------------------------------------------------------------------------
 import Plutarch.Api.V1 (
-  mintingPolicySymbol,
-  mkMintingPolicy,
   mkValidator,
   validatorHash,
  )
 import Plutus.V1.Ledger.Api (
   Address (Address),
   Credential (ScriptCredential),
-  CurrencySymbol,
   Datum (Datum),
   DatumHash (DatumHash),
-  MintingPolicy (..),
-  PubKeyHash,
   ScriptContext (..),
   ScriptPurpose (..),
   ToData (toBuiltinData),
@@ -45,55 +39,28 @@ import Plutus.V1.Ledger.Api (
  )
 import Plutus.V1.Ledger.Contexts (TxOut (TxOut), TxOutRef (TxOutRef))
 import Plutus.V1.Ledger.Interval qualified as Interval
-import Plutus.V1.Ledger.Scripts (Validator)
-import Plutus.V1.Ledger.Value (AssetClass (AssetClass), TokenName (TokenName))
+import Plutus.V1.Ledger.Value (TokenName (TokenName))
 import Plutus.V1.Ledger.Value qualified as Value
 
 --------------------------------------------------------------------------------
 
 import Agora.SafeMoney (GTTag)
 import Agora.Stake
+import Agora.Stake.Scripts (stakeValidator)
 import Plutarch.SafeMoney
+import Spec.Sample.Shared
 import Spec.Util (datumPair, toDatumHash)
 
 --------------------------------------------------------------------------------
 
--- | 'Stake' parameters for 'LQ'.
-stake :: Stake
-stake =
-  Stake
-    { gtClassRef =
-        Tagged
-          ( AssetClass
-              ( "da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
-              , "LQ"
-              )
-          )
-    }
-
--- | 'Stake' policy instance.
-policy :: MintingPolicy
-policy = mkMintingPolicy (stakePolicy stake)
-
-policySymbol :: CurrencySymbol
-policySymbol = mintingPolicySymbol policy
-
--- | A sample 'PubKeyHash'.
-signer :: PubKeyHash
-signer = "8a30896c4fd5e79843e4ca1bd2cdbaa36f8c0bc3be7401214142019c"
-
--- | 'Stake' validator instance.
-validator :: Validator
-validator = mkValidator (stakeValidator stake)
-
 -- | 'TokenName' that represents the hash of the 'Stake' validator.
 validatorHashTN :: TokenName
-validatorHashTN = let ValidatorHash vh = validatorHash validator in TokenName vh
+validatorHashTN = let ValidatorHash vh = validatorHash (mkValidator $ stakeValidator stake) in TokenName vh
 
 -- | This script context should be a valid transaction.
 stakeCreation :: ScriptContext
 stakeCreation =
-  let st = Value.singleton policySymbol validatorHashTN 1 -- Stake ST
+  let st = Value.singleton stakeSymbol validatorHashTN 1 -- Stake ST
       datum :: Datum
       datum = Datum (toBuiltinData $ StakeDatum 424242424242 signer [])
    in ScriptContext
@@ -102,7 +69,7 @@ stakeCreation =
               { txInfoInputs = []
               , txInfoOutputs =
                   [ TxOut
-                      { txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
+                      { txOutAddress = Address (ScriptCredential stakeValidatorHash) Nothing
                       , txOutValue = st <> Value.singleton "da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24" "LQ" 424242424242
                       , txOutDatumHash = Just (DatumHash "")
                       }
@@ -116,7 +83,7 @@ stakeCreation =
               , txInfoData = [("", datum)]
               , txInfoId = "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
               }
-        , scriptContextPurpose = Minting policySymbol
+        , scriptContextPurpose = Minting stakeSymbol
         }
 
 -- | This ScriptContext should fail because the datum has too much GT.
@@ -126,7 +93,7 @@ stakeCreationWrongDatum =
       datum = Datum (toBuiltinData $ StakeDatum 4242424242424242 signer []) -- Too much GT
    in ScriptContext
         { scriptContextTxInfo = stakeCreation.scriptContextTxInfo {txInfoData = [("", datum)]}
-        , scriptContextPurpose = Minting policySymbol
+        , scriptContextPurpose = Minting stakeSymbol
         }
 
 -- | This ScriptContext should fail because the datum has too much GT.
@@ -137,7 +104,7 @@ stakeCreationUnsigned =
         stakeCreation.scriptContextTxInfo
           { txInfoSignatories = []
           }
-    , scriptContextPurpose = Minting policySymbol
+    , scriptContextPurpose = Minting stakeSymbol
     }
 
 --------------------------------------------------------------------------------
@@ -153,7 +120,7 @@ data DepositWithdrawExample = DepositWithdrawExample
 -- | Create a ScriptContext that deposits or withdraws, given the config for it.
 stakeDepositWithdraw :: DepositWithdrawExample -> ScriptContext
 stakeDepositWithdraw config =
-  let st = Value.singleton policySymbol validatorHashTN 1 -- Stake ST
+  let st = Value.singleton stakeSymbol validatorHashTN 1 -- Stake ST
       stakeBefore :: StakeDatum
       stakeBefore = StakeDatum config.startAmount signer []
 
@@ -166,7 +133,7 @@ stakeDepositWithdraw config =
                   [ TxInInfo
                       (TxOutRef "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be" 1)
                       TxOut
-                        { txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
+                        { txOutAddress = Address (ScriptCredential stakeValidatorHash) Nothing
                         , txOutValue =
                             st
                               <> Value.assetClassValue (untag stake.gtClassRef) (untag stakeBefore.stakedAmount)
@@ -175,10 +142,9 @@ stakeDepositWithdraw config =
                   ]
               , txInfoOutputs =
                   [ TxOut
-                      { txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
+                      { txOutAddress = Address (ScriptCredential stakeValidatorHash) Nothing
                       , txOutValue =
-                          st
-                            <> Value.assetClassValue (untag stake.gtClassRef) (untag stakeAfter.stakedAmount)
+                          st <> Value.assetClassValue (untag stake.gtClassRef) (untag stakeAfter.stakedAmount)
                       , txOutDatumHash = Just (toDatumHash stakeAfter)
                       }
                   ]
diff --git a/agora-test/Spec/Stake.hs b/agora-test/Spec/Stake.hs
index 8f2538d..6824b80 100644
--- a/agora-test/Spec/Stake.hs
+++ b/agora-test/Spec/Stake.hs
@@ -19,7 +19,8 @@ import Test.Tasty (TestTree, testGroup)
 
 --------------------------------------------------------------------------------
 
-import Agora.Stake (StakeDatum (StakeDatum), StakeRedeemer (DepositWithdraw), stakePolicy, stakeValidator)
+import Agora.Stake (Stake (..), StakeDatum (StakeDatum), StakeRedeemer (DepositWithdraw))
+import Agora.Stake.Scripts (stakePolicy, stakeValidator)
 
 --------------------------------------------------------------------------------
 
@@ -36,20 +37,23 @@ tests =
       "policy"
       [ policySucceedsWith
           "stakeCreation"
-          (stakePolicy Stake.stake)
+          (stakePolicy Stake.stake.gtClassRef)
           ()
           Stake.stakeCreation
       , policyFailsWith
           "stakeCreationWrongDatum"
-          (stakePolicy Stake.stake)
+          (stakePolicy Stake.stake.gtClassRef)
           ()
           Stake.stakeCreationWrongDatum
       , policyFailsWith
           "stakeCreationUnsigned"
-          (stakePolicy Stake.stake)
+          (stakePolicy Stake.stake.gtClassRef)
           ()
           Stake.stakeCreationUnsigned
-      , validatorSucceedsWith
+      ]
+  , testGroup
+      "validator"
+      [ validatorSucceedsWith
           "stakeDepositWithdraw deposit"
           (stakeValidator Stake.stake)
           (toDatum $ StakeDatum 100_000 signer [])
diff --git a/agora-test/Spec/Util.hs b/agora-test/Spec/Util.hs
index f36b3ba..365ad50 100644
--- a/agora-test/Spec/Util.hs
+++ b/agora-test/Spec/Util.hs
@@ -100,10 +100,10 @@ validatorSucceedsWith ::
   PLifted redeemer ->
   ScriptContext ->
   TestTree
-validatorSucceedsWith tag policy datum redeemer scriptContext =
+validatorSucceedsWith tag validator datum redeemer scriptContext =
   scriptSucceeds tag $
     compile
-      ( policy
+      ( validator
           # pforgetData (pconstantData datum)
           # pforgetData (pconstantData redeemer)
           # pconstant scriptContext
@@ -122,10 +122,10 @@ validatorFailsWith ::
   PLifted redeemer ->
   ScriptContext ->
   TestTree
-validatorFailsWith tag policy datum redeemer scriptContext =
+validatorFailsWith tag validator datum redeemer scriptContext =
   scriptFails tag $
     compile
-      ( policy
+      ( validator
           # pforgetData (pconstantData datum)
           # pforgetData (pconstantData redeemer)
           # pconstant scriptContext
diff --git a/agora.cabal b/agora.cabal
index c1729d0..b55630b 100644
--- a/agora.cabal
+++ b/agora.cabal
@@ -60,6 +60,7 @@ common lang
     NamedFieldPuns
     NamedWildCards
     NumericUnderscores
+    OverloadedLabels
     OverloadedStrings
     PartialTypeSignatures
     PatternGuards
@@ -128,8 +129,12 @@ library
     Agora.Governor
     Agora.MultiSig
     Agora.Proposal
+    Agora.Proposal.Scripts
+    Agora.Proposal.Time
+    Agora.Record
     Agora.SafeMoney
     Agora.Stake
+    Agora.Stake.Scripts
     Agora.Treasury
 
   other-modules:
@@ -156,7 +161,10 @@ test-suite agora-test
     Spec.AuthorityToken
     Spec.Effect.TreasuryWithdrawal
     Spec.Model.MultiSig
+    Spec.Proposal
     Spec.Sample.Effect.TreasuryWithdrawal
+    Spec.Sample.Proposal
+    Spec.Sample.Shared
     Spec.Sample.Stake
     Spec.Stake
     Spec.Util
diff --git a/agora/Agora/AuthorityToken.hs b/agora/Agora/AuthorityToken.hs
index 8239242..241ad13 100644
--- a/agora/Agora/AuthorityToken.hs
+++ b/agora/Agora/AuthorityToken.hs
@@ -18,16 +18,15 @@ import Plutarch.Api.V1 (
   PCurrencySymbol (..),
   PScriptContext (..),
   PScriptPurpose (..),
-  PTxInInfo (..),
+  PTxInInfo (PTxInInfo),
   PTxInfo (..),
   PTxOut (..),
  )
 import Plutarch.Api.V1.AssocMap (PMap (PMap))
 import Plutarch.Api.V1.Value (PValue (PValue))
 import Plutarch.Builtin (pforgetData)
-import Plutarch.List (pfoldr')
 import Plutarch.Monadic qualified as P
-import Plutus.V1.Ledger.Value (AssetClass)
+import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
 
 import Prelude
 
@@ -36,11 +35,11 @@ import Prelude
 import Agora.Utils (
   allOutputs,
   passert,
-  passetClassValueOf,
-  passetClassValueOf',
   plookup,
   psymbolValueOf,
+  ptokenSpent,
  )
+import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
 
 --------------------------------------------------------------------------------
 
@@ -132,28 +131,21 @@ authorityTokenPolicy params =
       PTxInfo txInfo' <- pmatch $ pfromData ctx.txInfo
       txInfo <- pletFields @'["inputs", "mint"] txInfo'
       let inputs = txInfo.inputs
-      let authorityTokenInputs =
-            pfoldr' @PBuiltinList
-              ( \txInInfo' acc -> P.do
-                  PTxInInfo txInInfo <- pmatch (pfromData txInInfo')
-                  PTxOut txOut' <- pmatch $ pfromData $ pfield @"resolved" # txInInfo
-                  txOut <- pletFields @'["value"] txOut'
-                  let txOutValue = pfromData txOut.value
-                  passetClassValueOf' params.authority # txOutValue + acc
-              )
-              # 0
-              # inputs
-      let mintedValue = pfromData txInfo.mint
-      let tokenMoved = 0 #< authorityTokenInputs
+          mintedValue = pfromData txInfo.mint
+          AssetClass (govCs, govTn) = params.authority
+          govAc = passetClass # pconstant govCs # pconstant govTn
+          govTokenSpent = ptokenSpent # govAc # inputs
+
       PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
+
       let ownSymbol = pfromData $ pfield @"_0" # ownSymbol'
-      let mintedATs = passetClassValueOf # ownSymbol # pconstant "" # mintedValue
+          mintedATs = passetClassValueOf # mintedValue # (passetClass # ownSymbol # pconstant "")
       pif
         (0 #< mintedATs)
         ( P.do
-            passert "Parent token did not move in minting GATs" tokenMoved
+            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/Effect/NoOp.hs b/agora/Agora/Effect/NoOp.hs
index 90782e9..82069b9 100644
--- a/agora/Agora/Effect/NoOp.hs
+++ b/agora/Agora/Effect/NoOp.hs
@@ -10,11 +10,11 @@ module Agora.Effect.NoOp (noOpValidator, PNoOp) where
 import Control.Applicative (Const)
 
 import Agora.Effect (makeEffect)
-import Plutarch (popaque)
 import Plutarch.Api.V1 (PValidator)
 import Plutarch.TryFrom (PTryFrom (..))
 import Plutus.V1.Ledger.Value (CurrencySymbol)
 
+-- | Dummy datum for NoOp effect.
 newtype PNoOp (s :: S) = PNoOp (Term s PUnit)
   deriving (PlutusType, PIsData) via (DerivePNewtype PNoOp PUnit)
 
diff --git a/agora/Agora/Effect/TreasuryWithdrawal.hs b/agora/Agora/Effect/TreasuryWithdrawal.hs
index 209877f..e9957a4 100644
--- a/agora/Agora/Effect/TreasuryWithdrawal.hs
+++ b/agora/Agora/Effect/TreasuryWithdrawal.hs
@@ -19,7 +19,6 @@ import Generics.SOP (Generic, I (I))
 
 import Agora.Effect (makeEffect)
 import Agora.Utils (findTxOutByTxOutRef, paddValue, passert)
-import Plutarch (popaque)
 import Plutarch.Api.V1 (
   PCredential (..),
   PTuple,
@@ -34,23 +33,32 @@ import Plutarch.DataRepr (
   PDataFields,
   PIsDataReprInstances (..),
  )
-import Plutarch.Lift (PUnsafeLiftDecl (..))
+import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (..))
 import Plutarch.Monadic qualified as P
 import Plutarch.TryFrom (PTryFrom (..))
 import Plutus.V1.Ledger.Credential (Credential)
 import Plutus.V1.Ledger.Value (CurrencySymbol, Value)
 import PlutusTx qualified
 
+{- | Datum that encodes behavior of Treasury Withdrawal effect.
+
+Note: This Datum acts like a "predefined redeemer". Which is to say that
+it encodes the properties a redeemer would, but is locked in-place until
+spend.
+-}
 data TreasuryWithdrawalDatum = TreasuryWithdrawalDatum
   { receivers :: [(Credential, Value)]
+  -- ^ AssocMap for Value sent to each receiver from the treasury.
   , treasuries :: [Credential]
+  -- ^ What Credentials is spending from legal.
   }
   deriving stock (Show, GHC.Generic)
   deriving anyclass (Generic)
 
 PlutusTx.makeLift ''TreasuryWithdrawalDatum
-PlutusTx.unstableMakeIsData ''TreasuryWithdrawalDatum
+PlutusTx.makeIsDataIndexed ''TreasuryWithdrawalDatum [('TreasuryWithdrawalDatum, 0)]
 
+-- | Haskell-level version of 'TreasuryWithdrawalDatum'.
 newtype PTreasuryWithdrawalDatum (s :: S)
   = PTreasuryWithdrawalDatum
       ( Term
@@ -69,15 +77,17 @@ newtype PTreasuryWithdrawalDatum (s :: S)
 
 instance PUnsafeLiftDecl PTreasuryWithdrawalDatum where
   type PLifted PTreasuryWithdrawalDatum = TreasuryWithdrawalDatum
+
 deriving via
   (DerivePConstantViaData TreasuryWithdrawalDatum PTreasuryWithdrawalDatum)
   instance
-    (PConstant TreasuryWithdrawalDatum)
+    (PConstantDecl TreasuryWithdrawalDatum)
 
 instance PTryFrom PData PTreasuryWithdrawalDatum where
   type PTryFromExcess PData PTreasuryWithdrawalDatum = Const ()
   ptryFrom' opq cont =
-    -- this will need to not use punsafeCoerce...
+    -- TODO: This should not use 'punsafeCoerce'.
+    -- Blocked by 'PCredential', and 'PTuple'.
     cont (punsafeCoerce opq, ())
 
 {- | Withdraws given list of values to specific target addresses.
@@ -90,7 +100,7 @@ instance PTryFrom PData PTreasuryWithdrawalDatum where
      Note:
      It should check...
      1. Transaction outputs should contain all of what Datum specified
-     2. Left over assests should be redirected back to Treasury
+     2. Left over assets should be redirected back to Treasury
      It can be more flexiable over...
      - The number of outputs themselves
 -}
@@ -99,7 +109,7 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
   \_cs (datum' :: Term _ PTreasuryWithdrawalDatum) txOutRef' txInfo' -> P.do
     datum <- pletFields @'["receivers", "treasuries"] datum'
     txInfo <- pletFields @'["outputs", "inputs"] txInfo'
-    PJust txOut <- pmatch $ findTxOutByTxOutRef # txOutRef' # pfromData txInfo'
+    PJust txOut <- pmatch $ findTxOutByTxOutRef # txOutRef' # pfromData txInfo.inputs
     effInput <- pletFields @'["address", "value"] $ txOut
     outputValues <-
       plet $
diff --git a/agora/Agora/Governor.hs b/agora/Agora/Governor.hs
index 8f12181..24f52ad 100644
--- a/agora/Agora/Governor.hs
+++ b/agora/Agora/Governor.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE TemplateHaskell #-}
+
 {- |
 Module     : Agora.Governor
 Maintainer : emi@haskell.fyi
@@ -19,8 +21,8 @@ module Agora.Governor (
 ) where
 
 import Agora.Proposal (ProposalId, ProposalThresholds)
-import Plutarch (popaque)
 import Plutarch.Api.V1 (PMintingPolicy, PValidator)
+import PlutusTx qualified
 
 -- | Datum for the Governor script.
 data GovernorDatum = GovernorDatum
@@ -30,6 +32,8 @@ data GovernorDatum = GovernorDatum
   -- ^ What tag the next proposal will get upon creating.
   }
 
+PlutusTx.makeIsDataIndexed ''GovernorDatum [('GovernorDatum, 0)]
+
 {- | Redeemer for Governor script. The governor has two primary
      responsibilities:
 
@@ -43,6 +47,8 @@ data GovernorRedeemer
     --   and allows minting GATs for each effect script.
     MintGATs
 
+PlutusTx.makeIsDataIndexed ''GovernorRedeemer [('CreateProposal, 0), ('MintGATs, 1)]
+
 -- | Parameters for creating Governor scripts.
 data Governor
   = Governor
diff --git a/agora/Agora/MultiSig.hs b/agora/Agora/MultiSig.hs
index 93cf3e6..a65d0f0 100644
--- a/agora/Agora/MultiSig.hs
+++ b/agora/Agora/MultiSig.hs
@@ -24,6 +24,7 @@ import Plutarch.DataRepr (
   PIsDataReprInstances (PIsDataReprInstances),
  )
 import Plutarch.Lift (
+  PConstantDecl,
   PLifted,
   PUnsafeLiftDecl,
  )
@@ -73,7 +74,7 @@ newtype PMultiSig (s :: S) = PMultiSig
     via (PIsDataReprInstances PMultiSig)
 
 instance PUnsafeLiftDecl PMultiSig where type PLifted PMultiSig = MultiSig
-deriving via (DerivePConstantViaData MultiSig PMultiSig) instance (PConstant MultiSig)
+deriving via (DerivePConstantViaData MultiSig PMultiSig) instance (PConstantDecl MultiSig)
 
 --------------------------------------------------------------------------------
 
diff --git a/agora/Agora/Proposal.hs b/agora/Agora/Proposal.hs
index 7125da0..c5e0068 100644
--- a/agora/Agora/Proposal.hs
+++ b/agora/Agora/Proposal.hs
@@ -11,23 +11,25 @@ module Agora.Proposal (
   -- * Haskell-land
   Proposal (..),
   ProposalDatum (..),
+  ProposalRedeemer (..),
   ProposalStatus (..),
   ProposalThresholds (..),
   ProposalVotes (..),
   ProposalId (..),
   ResultTag (..),
+  emptyVotesFor,
 
   -- * Plutarch-land
   PProposalDatum (..),
+  PProposalRedeemer (..),
   PProposalStatus (..),
   PProposalThresholds (..),
   PProposalVotes (..),
   PProposalId (..),
   PResultTag (..),
 
-  -- * Scripts
-  proposalValidator,
-  proposalPolicy,
+  -- * Plutarch helpers
+  proposalDatumValid,
 ) where
 
 import GHC.Generics qualified as GHC
@@ -35,30 +37,44 @@ import Generics.SOP (Generic, I (I))
 import Plutarch.Api.V1 (
   PDatumHash,
   PMap,
-  PMintingPolicy,
   PPubKeyHash,
-  PValidator,
   PValidatorHash,
  )
-import Plutarch.DataRepr (
-  DerivePConstantViaData (..),
-  PDataFields,
-  PIsDataReprInstances (PIsDataReprInstances),
- )
-import Plutus.V1.Ledger.Api (DatumHash, PubKeyHash, ValidatorHash)
 import PlutusTx qualified
 import PlutusTx.AssocMap qualified as AssocMap
 
 --------------------------------------------------------------------------------
-
 import Agora.SafeMoney (GTTag)
-import Plutarch (popaque)
-import Plutarch.Lift (DerivePConstantViaNewtype (..), PUnsafeLiftDecl (..))
+import Agora.Utils (pkeysEqual, 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)
+import Plutus.V1.Ledger.Api (DatumHash, PubKeyHash, ValidatorHash)
+import Plutus.V1.Ledger.Value (AssetClass)
 
 --------------------------------------------------------------------------------
 -- Haskell-land
 
+{- | Identifies a Proposal, issued upon creation of a proposal. In practice,
+     this number starts at zero, and increments by one for each proposal.
+     The 100th proposal will be @'ProposalId' 99@. This counter lives
+     in the 'Agora.Governor.Governor'. See 'Agora.Governor.nextProposalId', and
+     'Agora.Governor.pgetNextProposalId'.
+-}
+newtype ProposalId = ProposalId {proposalTag :: Integer}
+  deriving newtype (PlutusTx.ToData, PlutusTx.FromData, PlutusTx.UnsafeFromData)
+  deriving stock (Eq, Show, GHC.Generic)
+
 {- | Encodes a result. Typically, for a Yes/No proposal, we encode it like this:
 
 @
@@ -70,8 +86,10 @@ newtype ResultTag = ResultTag {getResultTag :: Integer}
   deriving stock (Eq, Show, Ord)
   deriving newtype (PlutusTx.ToData, PlutusTx.FromData, PlutusTx.UnsafeFromData)
 
-{- | The "status" of the proposal. This is only useful for state transitions,
-     as opposed to time-based "phases".
+{- | The "status" of the proposal. This is only useful for state transitions that
+     need to happen as a result of a transaction as opposed to time-based "periods".
+
+     See the note on wording & the state machine in the tech-design.
 
      If the proposal is 'VotingReady', for instance, that doesn't necessarily
      mean that voting is possible, as this also requires the timing to be right.
@@ -92,28 +110,39 @@ data ProposalStatus
     --   This means that once the timing requirements align,
     --   proposal will be able to be voted on.
     VotingReady
+  | -- | The proposal has been voted on, and the votes have been locked
+    --   permanently. The proposal now goes into a locking time after the
+    --   normal voting time. After this, it's possible to execute the proposal.
+    Locked
   | -- | The proposal has finished.
     --
     --   This can mean it's been voted on and completed, but it can also mean
-    --   the proposal failed due to  time constraints or didn't
+    --   the proposal failed due to time constraints or didn't
     --   get to 'VotingReady' first.
     --
+    --   At this stage, the 'votes' field of 'ProposalDatum' is frozen.
+    --
+    --   See 'AdvanceProposal' for documentation on state transitions.
+    --
     --   TODO: The owner of the proposal may choose to reclaim their proposal.
     Finished
   deriving stock (Eq, Show, GHC.Generic)
 
-PlutusTx.makeIsDataIndexed ''ProposalStatus [('Draft, 0), ('VotingReady, 1), ('Finished, 2)]
+PlutusTx.makeIsDataIndexed ''ProposalStatus [('Draft, 0), ('VotingReady, 1), ('Locked, 2), ('Finished, 3)]
 
 {- | The threshold values for various state transitions to happen.
      This data is stored centrally (in the 'Agora.Governor.Governor') and copied over
      to 'Proposal's when they are created.
 -}
 data ProposalThresholds = ProposalThresholds
-  { execute :: Tagged GTTag Integer
+  { countVoting :: Tagged GTTag Integer
   -- ^ How much GT minimum must a particular 'ResultTag' accumulate for it to pass.
-  , draft :: Tagged GTTag Integer
+  , create :: Tagged GTTag Integer
   -- ^ How much GT required to "create" a proposal.
-  , vote :: Tagged GTTag Integer
+  --
+  -- It is recommended this be a high enough amount, in order to prevent DOS from bad
+  -- actors.
+  , startVoting :: Tagged GTTag Integer
   -- ^ How much GT required to allow voting to happen.
   -- (i.e. to move into 'VotingReady')
   }
@@ -138,9 +167,15 @@ newtype ProposalVotes = ProposalVotes
   deriving newtype (PlutusTx.ToData, PlutusTx.FromData, PlutusTx.UnsafeFromData)
   deriving stock (Eq, Show, GHC.Generic)
 
+-- | Create a 'ProposalVotes' that has the same shape as the 'effects' field.
+emptyVotesFor :: forall a. AssocMap.Map ResultTag a -> ProposalVotes
+emptyVotesFor = ProposalVotes . AssocMap.mapWithKey (const . const 0)
+
 -- | Haskell-level datum for Proposal scripts.
 data ProposalDatum = ProposalDatum
-  { -- TODO: could we encode this more efficiently?
+  { proposalId :: ProposalId
+  -- ^ Identification of the proposal.
+  , -- TODO: could we encode this more efficiently?
   -- This is shaped this way for future proofing.
   -- See https://github.com/Liqwid-Labs/agora/issues/39
   effects :: AssocMap.Map ResultTag [(ValidatorHash, DatumHash)]
@@ -158,17 +193,62 @@ data ProposalDatum = ProposalDatum
 
 PlutusTx.makeIsDataIndexed ''ProposalDatum [('ProposalDatum, 0)]
 
-{- | Identifies a Proposal, issued upon creation of a proposal.
-     In practice, this number starts at zero, and increments by one
-     for each proposal. The 100th proposal will be @'ProposalId' 99@.
-     This counter lives in the 'Governor', see 'nextProposalId'.
--}
-newtype ProposalId = ProposalId {proposalTag :: Integer}
-  deriving newtype (PlutusTx.ToData, PlutusTx.FromData, PlutusTx.UnsafeFromData)
+-- | Haskell-level redeemer for Proposal scripts.
+data ProposalRedeemer
+  = -- | Cast one or more votes towards a particular 'ResultTag'.
+    Vote ResultTag
+  | -- | Add one or more public keys to the cosignature list.
+    --   Must be signed by those cosigning.
+    --
+    --   This is particularly used in the 'Draft' 'ProposalStatus',
+    --   where matching 'Agora.Stake.Stake's can be called to advance the proposal,
+    --   provided enough GT is shared  among them.
+    Cosign [PubKeyHash]
+  | -- | Allow unlocking one or more stakes with votes towards particular 'ResultTag'.
+    Unlock ResultTag
+  | -- | Advance the proposal, performing the required checks for whether that is legal.
+    --
+    --   These are roughly the checks for each possible transition:
+    --
+    --   === @'Draft' -> 'VotingReady'@:
+    --
+    --     1. The sum of all of the cosigner's GT is larger than the 'startVoting' field of 'ProposalThresholds'.
+    --     2. The proposal's current time ensures 'isDraftPeriod'.
+    --
+    --   === @'VotingReady' -> 'Locked'@:
+    --
+    --     1. The sum of all votes is larger than 'countVoting'.
+    --     2. The winning 'ResultTag' has more votes than all other 'ResultTag's.
+    --     3. The proposal's current time ensures 'isVotingPeriod'.
+    --
+    --   === @'Locked' -> 'Finished'@:
+    --
+    --     1. The proposal's current time ensures 'isExecutionPeriod'.
+    --     2. The transaction mints the GATs to the receiving effects.
+    --
+    --   === @* -> 'Finished'@:
+    --
+    --     If the proposal has run out of time for the current 'ProposalStatus', it will always be possible
+    --     to transition into 'Finished' status, because it has expired (and failed).
+    AdvanceProposal
   deriving stock (Eq, Show, GHC.Generic)
 
+PlutusTx.makeIsDataIndexed
+  ''ProposalRedeemer
+  [ ('Vote, 0)
+  , ('Cosign, 1)
+  , ('Unlock, 2)
+  , ('AdvanceProposal, 3)
+  ]
+
 -- | Parameters that identify the Proposal validator script.
 data Proposal = Proposal
+  { governorSTAssetClass :: AssetClass
+  , stakeSTAssetClass :: AssetClass
+  , maximumCosigners :: Integer
+  -- ^ Arbitrary limit for maximum amount of cosigners on a proposal.
+  }
+  deriving stock (Show, Eq)
 
 --------------------------------------------------------------------------------
 -- Plutarch-land
@@ -181,17 +261,37 @@ instance PUnsafeLiftDecl PResultTag where type PLifted PResultTag = ResultTag
 deriving via
   (DerivePConstantViaNewtype ResultTag PResultTag PInteger)
   instance
-    (PConstant ResultTag)
+    (PConstantDecl ResultTag)
+
+-- FIXME: This instance and the one below, for 'PProposalId', should be derived.
+-- Soon this will be possible through 'DerivePNewtype'.
+instance PTryFrom PData (PAsData PResultTag) where
+  type PTryFromExcess PData (PAsData PResultTag) = PTryFromExcess PData (PAsData PInteger)
+  ptryFrom' d k =
+    ptryFrom' @_ @(PAsData PInteger) d $
+      -- JUSTIFICATION:
+      -- We are coercing from @PAsData PInteger@ to @PAsData PResultTag@.
+      -- Since 'PResultTag' is a simple newtype, their shape is the same.
+      k . first punsafeCoerce
 
 -- | Plutarch-level version of 'PProposalId'.
 newtype PProposalId (s :: S) = PProposalId (Term s PInteger)
   deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype PProposalId PInteger)
 
+instance PTryFrom PData (PAsData PProposalId) where
+  type PTryFromExcess PData (PAsData PProposalId) = PTryFromExcess PData (PAsData PInteger)
+  ptryFrom' d k =
+    ptryFrom' @_ @(PAsData PInteger) d $
+      -- JUSTIFICATION:
+      -- We are coercing from @PAsData PInteger@ to @PAsData PProposalId@.
+      -- Since 'PProposalId' is a simple newtype, their shape is the same.
+      k . first punsafeCoerce
+
 instance PUnsafeLiftDecl PProposalId where type PLifted PProposalId = ProposalId
 deriving via
   (DerivePConstantViaNewtype ProposalId PProposalId PInteger)
   instance
-    (PConstant ProposalId)
+    (PConstantDecl ProposalId)
 
 -- | Plutarch-level version of 'ProposalStatus'.
 data PProposalStatus (s :: S)
@@ -199,6 +299,7 @@ data PProposalStatus (s :: S)
     -- e.g. like Tilde used 'pmatchEnum'.
     PDraft (Term s (PDataRecord '[]))
   | PVotingReady (Term s (PDataRecord '[]))
+  | PLocked (Term s (PDataRecord '[]))
   | PFinished (Term s (PDataRecord '[]))
   deriving stock (GHC.Generic)
   deriving anyclass (Generic)
@@ -208,7 +309,7 @@ data PProposalStatus (s :: S)
     via PIsDataReprInstances PProposalStatus
 
 instance PUnsafeLiftDecl PProposalStatus where type PLifted PProposalStatus = ProposalStatus
-deriving via (DerivePConstantViaData ProposalStatus PProposalStatus) instance (PConstant ProposalStatus)
+deriving via (DerivePConstantViaData ProposalStatus PProposalStatus) instance (PConstantDecl ProposalStatus)
 
 -- | Plutarch-level version of 'ProposalThresholds'.
 newtype PProposalThresholds (s :: S) = PProposalThresholds
@@ -230,7 +331,7 @@ newtype PProposalThresholds (s :: S) = PProposalThresholds
     via (PIsDataReprInstances PProposalThresholds)
 
 instance PUnsafeLiftDecl PProposalThresholds where type PLifted PProposalThresholds = ProposalThresholds
-deriving via (DerivePConstantViaData ProposalThresholds PProposalThresholds) instance (PConstant ProposalThresholds)
+deriving via (DerivePConstantViaData ProposalThresholds PProposalThresholds) instance (PConstantDecl ProposalThresholds)
 
 -- | Plutarch-level version of 'ProposalVotes'.
 newtype PProposalVotes (s :: S)
@@ -241,7 +342,7 @@ instance PUnsafeLiftDecl PProposalVotes where type PLifted PProposalVotes = Prop
 deriving via
   (DerivePConstantViaNewtype ProposalVotes PProposalVotes (PMap PResultTag PInteger))
   instance
-    (PConstant ProposalVotes)
+    (PConstantDecl ProposalVotes)
 
 -- | Plutarch-level version of 'ProposalDatum'.
 newtype PProposalDatum (s :: S) = PProposalDatum
@@ -249,9 +350,10 @@ newtype PProposalDatum (s :: S) = PProposalDatum
     Term
       s
       ( PDataRecord
-          '[ "effects" ':= PMap PResultTag (PMap PValidatorHash PDatumHash)
+          '[ "proposalId" ':= PProposalId
+           , "effects" ':= PMap PResultTag (PMap PValidatorHash PDatumHash)
            , "status" ':= PProposalStatus
-           , "cosigners" ':= PBuiltinList PPubKeyHash
+           , "cosigners" ':= PBuiltinList (PAsData PPubKeyHash)
            , "thresholds" ':= PProposalThresholds
            , "votes" ':= PProposalVotes
            ]
@@ -264,19 +366,71 @@ 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 (PConstant ProposalDatum)
+deriving via (DerivePConstantViaData ProposalDatum PProposalDatum) instance (PConstantDecl ProposalDatum)
+
+-- | Plutarch-level version of 'ProposalRedeemer'.
+data PProposalRedeemer (s :: S)
+  = PVote (Term s (PDataRecord '["resultTag" ':= PResultTag]))
+  | PCosign (Term s (PDataRecord '["newCosigners" ':= PBuiltinList (PAsData PPubKeyHash)]))
+  | PUnlock (Term s (PDataRecord '["resultTag" ':= PResultTag]))
+  | PAdvanceProposal (Term s (PDataRecord '[]))
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic)
+  deriving anyclass (PIsDataRepr)
+  deriving
+    (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)
+--   instance
+--     PTryFrom PData (PAsData PProposalRedeemer)
+
+instance PUnsafeLiftDecl PProposalRedeemer where type PLifted PProposalRedeemer = ProposalRedeemer
+deriving via (DerivePConstantViaData ProposalRedeemer PProposalRedeemer) instance (PConstantDecl ProposalRedeemer)
 
 --------------------------------------------------------------------------------
 
--- | Policy for Proposals.
-proposalPolicy :: Proposal -> ClosedTerm PMintingPolicy
-proposalPolicy _ =
-  plam $ \_redeemer _ctx' -> P.do
-    popaque (pconstant ())
+{- | Check for various invariants a proposal must uphold.
+     This can be used to check both upon creation and
+     upon any following state transitions in the proposal.
+-}
+proposalDatumValid :: Proposal -> Term s (Agora.Proposal.PProposalDatum :--> PBool)
+proposalDatumValid proposal =
+  phoistAcyclic $
+    plam $ \datum' -> P.do
+      datum <- pletFields @'["effects", "cosigners", "votes"] $ datum'
 
--- | Validator for Proposals.
-proposalValidator :: Proposal -> ClosedTerm PValidator
-proposalValidator _ =
-  plam $ \_datum _redeemer _ctx' -> P.do
-    popaque (pconstant ())
+      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 fewer cosigners than the limit" $ plength # (pfromData datum.cosigners) #<= pconstant proposal.maximumCosigners
+        , ptraceIfFalse "Proposal votes and effects are compatible with each other" $ pkeysEqual # datum.effects # pto (pfromData datum.votes)
+        ]
diff --git a/agora/Agora/Proposal/Scripts.hs b/agora/Agora/Proposal/Scripts.hs
new file mode 100644
index 0000000..2e7a52d
--- /dev/null
+++ b/agora/Agora/Proposal/Scripts.hs
@@ -0,0 +1,228 @@
+{- |
+Module     : Agora.Proposal.Scripts
+Maintainer : emi@haskell.fyi
+Description: Plutus Scripts for Proposals.
+
+Plutus Scripts for Proposals.
+-}
+module Agora.Proposal.Scripts (
+  proposalValidator,
+  proposalPolicy,
+) where
+
+import Agora.Proposal (
+  PProposalDatum (PProposalDatum),
+  PProposalRedeemer (..),
+  Proposal (governorSTAssetClass, stakeSTAssetClass),
+ )
+import Agora.Record (mkRecordConstr, (.&), (.=))
+import Agora.Stake (findStakeOwnedBy)
+import Agora.Utils (
+  anyOutput,
+  findTxOutByTxOutRef,
+  getMintingPolicySymbol,
+  passert,
+  pisUniq,
+  psymbolValueOf,
+  ptokenSpent,
+  ptxSignedBy,
+  pvalueSpent,
+ )
+import Plutarch.Api.V1 (
+  PMintingPolicy,
+  PScriptContext (PScriptContext),
+  PScriptPurpose (PMinting, PSpending),
+  PTxInfo (PTxInfo),
+  PValidator,
+ )
+import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
+import Plutarch.Monadic qualified as P
+import Plutarch.TryFrom (ptryFrom)
+import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
+
+{- | Policy for Proposals.
+
+   == What this policy does
+
+   === For minting:
+
+   - Governor is happy with mint.
+
+     * The governor must do most of the checking for the validity of the
+       transaction. For example, the governor must check that the datum
+       is correct, and that the ST is correctly paid to the right validator.
+
+   - Exactly 1 token is minted.
+
+   === For burning:
+
+   - This policy cannot be burned.
+-}
+proposalPolicy :: Proposal -> ClosedTerm PMintingPolicy
+proposalPolicy proposal =
+  plam $ \_redeemer ctx' -> P.do
+    PScriptContext ctx' <- pmatch ctx'
+    ctx <- pletFields @'["txInfo", "purpose"] ctx'
+    PTxInfo txInfo' <- pmatch $ pfromData ctx.txInfo
+    txInfo <- pletFields @'["inputs", "mint"] txInfo'
+    PMinting _ownSymbol <- pmatch $ pfromData ctx.purpose
+
+    let inputs = txInfo.inputs
+        mintedValue = pfromData txInfo.mint
+        AssetClass (govCs, govTn) = proposal.governorSTAssetClass
+
+    PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
+    let mintedProposalST =
+          passetClassValueOf
+            # mintedValue
+            # (passetClass # (pfield @"_0" # ownSymbol') # pconstant "")
+
+    passert "Governance state-thread token must move" $
+      ptokenSpent
+        # (passetClass # pconstant govCs # pconstant govTn)
+        # inputs
+
+    passert "Minted exactly one proposal ST" $
+      mintedProposalST #== 1
+
+    popaque (pconstant ())
+
+{- | The validator for Proposals.
+
+The documentation for various of the redeemers lives at 'Agora.Proposal.ProposalRedeemer'.
+
+== What this validator does
+
+=== Voting/unlocking
+
+When voting and unlocking, the proposal must witness a state transition
+occuring in the relevant Stake. This transition must place a lock on
+the stake that is tagged with the right 'Agora.Proposal.ResultTag', and 'Agora.Proposal.ProposalId'.
+
+=== Periods
+
+Most redeemers are time-sensitive.
+
+A list of all time-sensitive redeemers and their requirements:
+
+- 'Agora.Proposal.Vote' can only be used when both the status is in 'Agora.Proposal.VotingReady',
+  and 'Agora.Proposal.Time.isVotingPeriod' is true.
+- 'Agora.Proposal.Cosign' can only be used when both the status is in 'Agora.Proposal.Draft',
+  and 'Agora.Proposal.Time.isDraftPeriod' is true.
+- 'Agora.Proposal.AdvanceProposal' can only be used when the status can be advanced
+  (see 'Agora.Proposal.AdvanceProposal' docs).
+- 'Agora.Proposal.Unlock' is always valid.
+-}
+proposalValidator :: Proposal -> ClosedTerm PValidator
+proposalValidator proposal =
+  plam $ \datum redeemer ctx' -> P.do
+    PScriptContext ctx' <- pmatch ctx'
+    ctx <- pletFields @'["txInfo", "purpose"] ctx'
+    txInfo <- plet $ pfromData ctx.txInfo
+    PTxInfo txInfo' <- pmatch txInfo
+    txInfoF <- pletFields @'["inputs", "mint", "datums", "signatories"] txInfo'
+    PSpending ((pfield @"_0" #) -> txOutRef) <- pmatch $ pfromData ctx.purpose
+
+    PJust txOut <- pmatch $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
+    txOutF <- pletFields @'["address", "value"] $ txOut
+
+    (pfromData -> proposalDatum, _) <-
+      ptryFrom @(PAsData PProposalDatum) datum
+    (pfromData -> proposalRedeemer, _) <-
+      ptryFrom @(PAsData PProposalRedeemer) redeemer
+
+    proposalF <-
+      pletFields
+        @'[ "proposalId"
+          , "effects"
+          , "status"
+          , "cosigners"
+          , "thresholds"
+          , "votes"
+          ]
+        proposalDatum
+
+    ownAddress <- plet $ txOutF.address
+
+    let stCurrencySymbol =
+          pconstant $ getMintingPolicySymbol (proposalPolicy proposal)
+    valueSpent <- plet $ pvalueSpent # txInfoF.inputs
+    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
+    let AssetClass (stakeSym, stakeTn) = proposal.stakeSTAssetClass
+    stakeSTAssetClass <-
+      plet $ passetClass # pconstant stakeSym # pconstant stakeTn
+    spentStakeST <-
+      plet $ passetClassValueOf # valueSpent # stakeSTAssetClass
+
+    signedBy <- plet $ ptxSignedBy # txInfoF.signatories
+
+    passert "ST at inputs must be 1" $
+      spentST #== 1
+
+    pmatch proposalRedeemer $ \case
+      PVote _r -> P.do
+        popaque (pconstant ())
+      --------------------------------------------------------------------------
+      PCosign r -> P.do
+        newSigs <- plet $ pfield @"newCosigners" # r
+
+        passert "Cosigners are unique" $
+          pisUniq # newSigs
+
+        passert "Signed by all new cosigners" $
+          pall # signedBy # newSigs
+
+        passert "As many new cosigners as Stake datums" $
+          spentStakeST #== plength # newSigs
+
+        passert "All new cosigners are witnessed by their Stake datums" $
+          pall
+            # plam
+              ( \sig ->
+                  pmatch
+                    ( findStakeOwnedBy # stakeSTAssetClass
+                        # pfromData sig
+                        # txInfoF.datums
+                        # txInfoF.inputs
+                    )
+                    $ \case
+                      PNothing -> pcon PFalse
+                      PJust _ -> pcon PTrue
+              )
+            # newSigs
+
+        passert "Signatures are correctly added to cosignature list" $
+          anyOutput @PProposalDatum # ctx.txInfo
+            #$ plam
+            $ \newValue address newProposalDatum -> P.do
+              let updatedSigs = pconcat # newSigs # proposalF.cosigners
+                  correctDatum =
+                    pdata newProposalDatum
+                      #== pdata
+                        ( mkRecordConstr
+                            PProposalDatum
+                            ( #proposalId .= proposalF.proposalId
+                                .& #effects .= proposalF.effects
+                                .& #status .= proposalF.status
+                                .& #cosigners .= pdata updatedSigs
+                                .& #thresholds .= proposalF.thresholds
+                                .& #votes .= proposalF.votes
+                            )
+                        )
+
+              foldr1
+                (#&&)
+                [ ptraceIfFalse "Datum must be correct" correctDatum
+                , ptraceIfFalse "Value should be correct" $
+                    pdata txOutF.value #== pdata newValue
+                , ptraceIfFalse "Must be sent to Proposal's address" $
+                    ownAddress #== pdata address
+                ]
+
+        popaque (pconstant ())
+      --------------------------------------------------------------------------
+      PUnlock _r -> P.do
+        popaque (pconstant ())
+      --------------------------------------------------------------------------
+      PAdvanceProposal _r -> P.do
+        popaque (pconstant ())
diff --git a/agora/Agora/Proposal/Time.hs b/agora/Agora/Proposal/Time.hs
new file mode 100644
index 0000000..ec20f53
--- /dev/null
+++ b/agora/Agora/Proposal/Time.hs
@@ -0,0 +1,262 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+{- |
+Module     : Agora.Proposal.Time
+Maintainer : emi@haskell.fyi
+Description: Time functions for proposal phases.
+
+Time functions for proposal phases.
+-}
+module Agora.Proposal.Time (
+  -- * Haskell-land
+  ProposalTime (..),
+  ProposalTimingConfig (..),
+  ProposalStartingTime (..),
+
+  -- * Plutarch-land
+  PProposalTime (..),
+  PProposalTimingConfig (..),
+  PProposalStartingTime (..),
+
+  -- * Compute periods given config and starting time.
+  currentProposalTime,
+  isDraftPeriod,
+  isVotingPeriod,
+  isLockingPeriod,
+  isExecutionPeriod,
+) where
+
+import Agora.Record (mkRecordConstr, (.&), (.=))
+import GHC.Generics qualified as GHC
+import Generics.SOP (Generic, I (I))
+import Plutarch.Api.V1 (
+  PExtended (PFinite),
+  PInterval (PInterval),
+  PLowerBound (PLowerBound),
+  PPOSIXTime,
+  PPOSIXTimeRange,
+  PUpperBound (PUpperBound),
+ )
+import Plutarch.DataRepr (PDataFields, PIsDataReprInstances (..))
+import Plutarch.Monadic qualified as P
+import Plutarch.Numeric (AdditiveSemigroup ((+)))
+import Plutarch.Unsafe (punsafeCoerce)
+import Plutus.V1.Ledger.Time (POSIXTime)
+import PlutusTx qualified
+import Prelude hiding ((+))
+
+--------------------------------------------------------------------------------
+
+{- | == Establishing timing in Proposal interactions.
+
+   In Plutus, it's impossible to determine time exactly. It's also impossible
+   to get a single point in time, yet often we need to check
+   various constraints on time.
+
+   For the purposes of proposals, there's a single most important feature:
+   The ability to determine if we can perform an action. In order to correctly
+   determine if we are able to perform certain actions, we need to know what
+   time it roughly is, compared to when the proposal was created.
+
+   'ProposalTime' represents "the time according to the proposal".
+   Its representation is opaque, and doesn't matter.
+
+   Various functions work simply on 'ProposalTime' and 'ProposalTimingConfig'.
+   In particular, 'currentProposalTime' is useful for extracting the time
+   from the 'Plutus.V1.Ledger.Api.txInfoValidPeriod' field
+   of 'Plutus.V1.Ledger.Api.TxInfo'.
+
+   We avoid 'PPOSIXTimeRange' where we can in order to save on operations.
+-}
+data ProposalTime = ProposalTime
+  { lowerBound :: POSIXTime
+  , upperBound :: POSIXTime
+  }
+  deriving stock (Eq, Show, GHC.Generic)
+
+PlutusTx.makeIsDataIndexed ''ProposalTime [('ProposalTime, 0)]
+
+-- | Represents the starting time of the proposal.
+newtype ProposalStartingTime = ProposalStartingTime
+  { getProposalStartingTime :: POSIXTime
+  }
+  deriving newtype (PlutusTx.ToData, PlutusTx.FromData, PlutusTx.UnsafeFromData)
+  deriving stock (Eq, Show, GHC.Generic)
+
+{- | Configuration of proposal timings.
+
+ See: https://github.com/Liqwid-Labs/agora/blob/master/docs/tech-design/proposals.md#when-may-interactions-occur
+-}
+data ProposalTimingConfig = ProposalTimingConfig
+  { draftTime :: POSIXTime
+  -- ^ "D": the length of the draft period.
+  , votingTime :: POSIXTime
+  -- ^ "V": the length of the voting period.
+  , lockingTime :: POSIXTime
+  -- ^ "L": the length of the locking period.
+  , executingTime :: POSIXTime
+  -- ^ "E": the length of the execution period.
+  }
+  deriving stock (Eq, Show, GHC.Generic)
+
+PlutusTx.makeIsDataIndexed ''ProposalTimingConfig [('ProposalTimingConfig, 0)]
+
+--------------------------------------------------------------------------------
+
+-- | Plutarch-level version of 'ProposalTime'.
+newtype PProposalTime (s :: S)
+  = PProposalTime
+      ( Term
+          s
+          ( PDataRecord
+              '[ "lowerBound" ':= PPOSIXTime
+               , "upperBound" ':= PPOSIXTime
+               ]
+          )
+      )
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic)
+  deriving anyclass (PIsDataRepr)
+  deriving
+    (PlutusType, PIsData, PDataFields)
+    via (PIsDataReprInstances PProposalTime)
+
+-- | Plutarch-level version of 'ProposalStartingTime'.
+newtype PProposalStartingTime (s :: S) = PProposalStartingTime (Term s PPOSIXTime)
+  deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype PProposalStartingTime PPOSIXTime)
+
+-- | Plutarch-level version of 'ProposalTimingConfig'.
+newtype PProposalTimingConfig (s :: S) = PProposalTimingConfig
+  { getProposalTimingConfig ::
+    Term
+      s
+      ( PDataRecord
+          '[ "draftTime" ':= PPOSIXTime
+           , "votingTime" ':= PPOSIXTime
+           , "lockingTime" ':= PPOSIXTime
+           , "executingTime" ':= PPOSIXTime
+           ]
+      )
+  }
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic)
+  deriving anyclass (PIsDataRepr)
+  deriving
+    (PlutusType, PIsData, PDataFields)
+    via (PIsDataReprInstances PProposalTimingConfig)
+
+--------------------------------------------------------------------------------
+
+-- FIXME: Orphan instance, move this to plutarch-extra.
+instance AdditiveSemigroup (Term s PPOSIXTime) where
+  (punsafeCoerce @_ @_ @PInteger -> x) + (punsafeCoerce @_ @_ @PInteger -> y) = punsafeCoerce $ x + y
+
+{- | Get the current proposal time, from the 'Plutus.V1.Ledger.Api.txInfoValidPeriod' field.
+
+ If it's impossible to get a fully-bounded time, (e.g. either end of the 'PPOSIXTimeRange' is
+ an infinity) then we error out.
+-}
+currentProposalTime :: forall (s :: S). Term s (PPOSIXTimeRange :--> PProposalTime)
+currentProposalTime = phoistAcyclic $
+  plam $ \iv -> P.do
+    PInterval iv' <- pmatch iv
+    ivf <- pletFields @'["from", "to"] iv'
+    PLowerBound lb <- pmatch ivf.from
+    PUpperBound ub <- pmatch ivf.to
+    lbf <- pletFields @'["_0", "_1"] lb
+    ubf <- pletFields @'["_0", "_1"] ub
+    mkRecordConstr PProposalTime $
+      #lowerBound
+        .= pmatch
+          lbf._0
+          ( \case
+              PFinite ((pfield @"_0" #) -> d) -> d
+              _ -> ptraceError "currentProposalTime: Can't get fully-bounded proposal time."
+          )
+        .& #upperBound
+        .= pmatch
+          ubf._0
+          ( \case
+              PFinite ((pfield @"_0" #) -> d) -> d
+              _ -> ptraceError "currentProposalTime: Can't get fully-bounded proposal time."
+          )
+
+-- | Check if 'PProposalTime' is within two 'PPOSIXTime'. Inclusive.
+proposalTimeWithin ::
+  Term
+    s
+    ( PPOSIXTime
+        :--> PPOSIXTime
+        :--> PProposalTime
+        :--> PBool
+    )
+proposalTimeWithin = phoistAcyclic $
+  plam $ \l h proposalTime' -> P.do
+    PProposalTime proposalTime <- pmatch proposalTime'
+    ptf <- pletFields @'["lowerBound", "upperBound"] proposalTime
+    foldr1
+      (#&&)
+      [ l #<= pfromData ptf.lowerBound
+      , pfromData ptf.upperBound #<= h
+      ]
+
+-- | True if the 'PProposalTime' is in the draft period.
+isDraftPeriod ::
+  forall (s :: S).
+  Term
+    s
+    ( PProposalTimingConfig
+        :--> PProposalStartingTime
+        :--> PProposalTime
+        :--> PBool
+    )
+isDraftPeriod = phoistAcyclic $
+  plam $ \config s' -> pmatch s' $ \(PProposalStartingTime s) ->
+    proposalTimeWithin # s # (s + pfield @"draftTime" # config)
+
+-- | True if the 'PProposalTime' is in the voting period.
+isVotingPeriod ::
+  forall (s :: S).
+  Term
+    s
+    ( PProposalTimingConfig
+        :--> PProposalStartingTime
+        :--> PProposalTime
+        :--> PBool
+    )
+isVotingPeriod = phoistAcyclic $
+  plam $ \config s' -> pmatch s' $ \(PProposalStartingTime s) ->
+    pletFields @'["draftTime", "votingTime"] config $ \f ->
+      proposalTimeWithin # s # (s + f.draftTime + f.votingTime)
+
+-- | True if the 'PProposalTime' is in the locking period.
+isLockingPeriod ::
+  forall (s :: S).
+  Term
+    s
+    ( PProposalTimingConfig
+        :--> PProposalStartingTime
+        :--> PProposalTime
+        :--> PBool
+    )
+isLockingPeriod = phoistAcyclic $
+  plam $ \config s' -> pmatch s' $ \(PProposalStartingTime s) ->
+    pletFields @'["draftTime", "votingTime", "lockingTime"] config $ \f ->
+      proposalTimeWithin # s # (s + f.draftTime + f.votingTime + f.lockingTime)
+
+-- | True if the 'PProposalTime' is in the execution period.
+isExecutionPeriod ::
+  forall (s :: S).
+  Term
+    s
+    ( PProposalTimingConfig
+        :--> PProposalStartingTime
+        :--> PProposalTime
+        :--> PBool
+    )
+isExecutionPeriod = phoistAcyclic $
+  plam $ \config s' -> pmatch s' $ \(PProposalStartingTime s) ->
+    pletFields @'["draftTime", "votingTime", "lockingTime", "executingTime"] config $ \f ->
+      proposalTimeWithin # s
+        # (s + f.draftTime + f.votingTime + f.lockingTime + f.executingTime)
diff --git a/agora/Agora/Record.hs b/agora/Agora/Record.hs
new file mode 100644
index 0000000..30d7490
--- /dev/null
+++ b/agora/Agora/Record.hs
@@ -0,0 +1,108 @@
+{- |
+Module     : Agora.Record
+Maintainer : emi@haskell.fyi
+Description: PDataRecord helper functions.
+
+'PDataRecord' helper functions.
+-}
+module Agora.Record (
+  mkRecord,
+  mkRecordConstr,
+  (.=),
+  (.&),
+  RecordMorphism,
+  FieldName,
+) where
+
+import Control.Category (Category (..))
+import Data.Coerce (coerce)
+import GHC.OverloadedLabels (IsLabel (fromLabel))
+import GHC.TypeLits (Symbol)
+import Plutarch.DataRepr (PDataRecord (PDCons))
+import Prelude hiding (id, (.))
+
+-- | Like 'Data.Proxy.Proxy' but local to this module.
+data FieldName (sym :: Symbol) = FieldName
+
+{- | The use of two different 'Symbol's here allows unification to happen,
+     ensuring 'FieldName' has a fully inferred 'Symbol'.
+
+     For example, @'mkRecord' (#foo .= 'pconstantData' (42 :: 'Integer'))@ gets
+     the correct type. Namely, @'Term' s ('PDataRecord' '["foo" ':= 'PInteger'])@.
+-}
+instance forall (sym :: Symbol) (sym' :: Symbol). sym ~ sym' => IsLabel sym (FieldName sym) where
+  fromLabel = FieldName
+
+-- | Turn a constant 'RecordMorphism' into a fully built 'PDataRecord'.
+mkRecord :: forall (r :: [PLabeledType]) (s :: S). RecordMorphism s '[] r -> Term s (PDataRecord r)
+mkRecord f = f.runRecordMorphism pdnil
+
+{- | 'mkRecord' but for known data-types.
+
+This allows you to dynamically construct a record type constructor.
+
+=== Example:
+@
+'mkRecordConstr'
+  'Agora.Stake.PStakeDatum'
+  ( #stakedAmount '.=' 'pconstantData' ('Plutarch.SafeMoney.Tagged' @GTTag 42)
+      '.&' #owner '.=' 'pconstantData' "aabbcc"
+      '.&' #lockedBy '.=' 'pdata' pnil
+  )
+@
+Is the same as
+
+@
+'pconstant' ('Agora.Stake.StakeDatum' ('Plutarch.SafeMoney.Tagged' 42) "aabbcc" [])
+@
+-}
+mkRecordConstr ::
+  forall (r :: [PLabeledType]) (s :: S) (pt :: PType).
+  PlutusType pt =>
+  -- | The constructor. This is just the Haskell-level constructor for the type.
+  --   For 'Plutarch.Api.V1.Maybe.PMaybeData', this would
+  --   be 'Plutarch.Api.V1.Maybe.PDJust', or 'Plutarch.Api.V1.Maybe.PNothing'.
+  (forall s'. Term s' (PDataRecord r) -> pt s') ->
+  -- | The morphism that builds the record.
+  RecordMorphism s '[] r ->
+  Term s pt
+mkRecordConstr ctr = pcon . ctr . mkRecord
+
+-- | A morphism from one 'PDataRecord' to another, representing some sort of consing of data.
+newtype RecordMorphism (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType]) = RecordMorphism
+  { runRecordMorphism ::
+    Term s (PDataRecord as) ->
+    Term s (PDataRecord bs)
+  }
+
+instance Category (RecordMorphism s) where
+  id = RecordMorphism id
+  f . g = coerce $ f.runRecordMorphism . g.runRecordMorphism
+
+infix 7 .=
+
+-- | Cons a labeled type as a 'RecordMorphism'.
+(.=) ::
+  forall (sym :: Symbol) (a :: PType) (as :: [PLabeledType]) (s :: S).
+  -- | The field name. You can use @-XOverloadedLabels@ to enable the syntax:
+  --   @#hello ~ 'FieldName' "hello"@
+  FieldName sym ->
+  -- | The value at that field. This must be 'PAsData', because the underlying
+  --   type is @'PlutusCore.Data.Constr' 'Integer' ['PlutusCore.Data.Data']@.
+  Term s (PAsData a) ->
+  RecordMorphism s as ((sym ':= a) ': as)
+_ .= x = RecordMorphism $ pcon . PDCons x
+
+infixr 6 .&
+
+-- | Compose two 'RecordMorphism's.
+(.&) ::
+  forall
+    (s :: S)
+    (a :: [PLabeledType])
+    (b :: [PLabeledType])
+    (c :: [PLabeledType]).
+  RecordMorphism s b c ->
+  RecordMorphism s a b ->
+  RecordMorphism s a c
+(.&) = (.)
diff --git a/agora/Agora/Stake.hs b/agora/Agora/Stake.hs
index 8327d57..b25a7ef 100644
--- a/agora/Agora/Stake.hs
+++ b/agora/Agora/Stake.hs
@@ -8,16 +8,20 @@ Description: Vote-lockable stake UTXOs holding GT.
 Vote-lockable stake UTXOs holding GT.
 -}
 module Agora.Stake (
-  PStakeDatum (..),
-  PStakeRedeemer (..),
+  -- * Haskell-land
   StakeDatum (..),
   StakeRedeemer (..),
-  ProposalLock (..),
-  PProposalLock (..),
   Stake (..),
-  stakePolicy,
-  stakeValidator,
+  ProposalLock (..),
+
+  -- * Plutarch-land
+  PStakeDatum (..),
+  PStakeRedeemer (..),
+  PProposalLock (..),
+
+  -- * Utility functions
   stakeLocked,
+  findStakeOwnedBy,
 ) where
 
 --------------------------------------------------------------------------------
@@ -33,16 +37,14 @@ import PlutusTx qualified
 
 --------------------------------------------------------------------------------
 
-import Plutarch (popaque)
 import Plutarch.Api.V1 (
-  PCredential (PPubKeyCredential, PScriptCredential),
-  PMintingPolicy,
+  PDatum,
+  PDatumHash,
+  PMaybeData (PDJust, PDNothing),
   PPubKeyHash,
-  PScriptPurpose (PMinting, PSpending),
-  PTokenName,
-  PValidator,
-  mintingPolicySymbol,
-  mkMintingPolicy,
+  PTuple,
+  PTxInInfo (PTxInInfo),
+  PTxOut (PTxOut),
  )
 import Plutarch.DataRepr (
   DerivePConstantViaData (..),
@@ -50,43 +52,34 @@ import Plutarch.DataRepr (
   PIsDataReprInstances (PIsDataReprInstances),
  )
 import Plutarch.Internal (punsafeCoerce)
-import Plutarch.Lift (PUnsafeLiftDecl (..))
+import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (..))
 import Plutarch.Monadic qualified as P
-import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
+import Plutus.V1.Ledger.Value (AssetClass)
 
 --------------------------------------------------------------------------------
 
 import Agora.Proposal (PProposalId, PResultTag, ProposalId (..), ResultTag (..))
 import Agora.SafeMoney (GTTag)
 import Agora.Utils (
-  anyInput,
-  anyOutput,
-  paddValue,
-  passert,
-  pfindTxInByTxOutRef,
-  pgeqByClass,
-  pgeqByClass',
-  pgeqBySymbol,
   pnotNull,
-  psingletonValue,
-  psymbolValueOf,
-  ptxSignedBy,
-  pvalueSpent,
+  ptryFindDatum,
  )
-import Plutarch.Numeric
+import Control.Applicative (Const)
+import Plutarch.Api.V1.Extra (PAssetClass, passetClassValueOf)
+import Plutarch.Numeric ()
 import Plutarch.SafeMoney (
   PDiscrete,
   Tagged (..),
-  pdiscreteValue,
-  untag,
  )
+import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
 
 --------------------------------------------------------------------------------
 
 -- | Parameters for creating Stake scripts.
-newtype Stake = Stake
+data Stake = Stake
   { gtClassRef :: Tagged GTTag AssetClass
   -- ^ Used when inlining the AssetClass of a 'PDiscrete' in the script code.
+  , proposalSTClass :: AssetClass
   }
 
 {- | A lock placed on a Stake datum in order to prevent
@@ -135,17 +128,20 @@ data StakeRedeemer
   | -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
     --   Stake must be unlocked.
     Destroy
-  | -- | Permit a Vote to be added onto a 'Proposal'.
+  | -- | Permit a Vote to be added onto a 'Agora.Proposal.Proposal'.
     --   This also adds a lock to the 'lockedBy' field. See 'ProposalLock'.
     --   This needs to be done in sync with casting a vote, otherwise
     --   it's possible for a lock to be permanently placed on the stake,
     --   and then the funds are lost.
     PermitVote ProposalLock
   | -- | Retract a vote, removing it from the 'lockedBy' field. See 'ProposalLock'.
-    --   This action checks for permission of the 'Proposal'. Finished proposals are
+    --   This action checks for permission of the 'Agora.Proposal.Proposal'. Finished proposals are
     --   always allowed to have votes retracted and won't affect the Proposal datum,
     --   allowing 'Stake's to be unlocked.
     RetractVotes [ProposalLock]
+  | -- | The owner can consume stake if nothing is changed about it.
+    --   If the proposal token moves, this is equivalent to the owner consuming it.
+    WitnessStake
   deriving stock (Show, GHC.Generic)
 
 PlutusTx.makeIsDataIndexed
@@ -154,13 +150,14 @@ PlutusTx.makeIsDataIndexed
   , ('Destroy, 1)
   , ('PermitVote, 2)
   , ('RetractVotes, 3)
+  , ('WitnessStake, 4)
   ]
 
 -- | Haskell-level datum for Stake scripts.
 data StakeDatum = StakeDatum
   { stakedAmount :: Tagged GTTag Integer
   -- ^ Tracks the amount of governance token staked in the datum.
-  -- This also acts as the voting weight for 'Proposal's.
+  -- This also acts as the voting weight for 'Agora.Proposal.Proposal's.
   , owner :: PubKeyHash
   -- ^ The hash of the public key this stake belongs to.
   --
@@ -195,8 +192,13 @@ 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 (PConstant StakeDatum)
+deriving via (DerivePConstantViaData StakeDatum PStakeDatum) instance (PConstantDecl StakeDatum)
 
 -- | Plutarch-level redeemer for Stake scripts.
 data PStakeRedeemer (s :: S)
@@ -205,7 +207,8 @@ data PStakeRedeemer (s :: S)
   | -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
     PDestroy (Term s (PDataRecord '[]))
   | PPermitVote (Term s (PDataRecord '["lock" ':= PProposalLock]))
-  | PRetractVotes (Term s (PDataRecord '["locks" ':= PBuiltinList PProposalLock]))
+  | PRetractVotes (Term s (PDataRecord '["locks" ':= PBuiltinList (PAsData PProposalLock)]))
+  | PWitnessStake (Term s (PDataRecord '[]))
   deriving stock (GHC.Generic)
   deriving anyclass (Generic)
   deriving anyclass (PIsDataRepr)
@@ -213,9 +216,15 @@ data PStakeRedeemer (s :: S)
     (PlutusType, PIsData)
     via PIsDataReprInstances PStakeRedeemer
 
-instance PUnsafeLiftDecl PStakeRedeemer where type PLifted PStakeRedeemer = StakeRedeemer
-deriving via (DerivePConstantViaData StakeRedeemer PStakeRedeemer) instance (PConstant StakeRedeemer)
+deriving via
+  PAsData (PIsDataReprInstances PStakeRedeemer)
+  instance
+    PTryFrom PData (PAsData PStakeRedeemer)
 
+instance PUnsafeLiftDecl PStakeRedeemer where type PLifted PStakeRedeemer = StakeRedeemer
+deriving via (DerivePConstantViaData StakeRedeemer PStakeRedeemer) instance (PConstantDecl StakeRedeemer)
+
+-- | Plutarch-level version of 'ProposalLock'.
 newtype PProposalLock (s :: S) = PProposalLock
   { getProposalLock ::
     Term
@@ -233,224 +242,13 @@ newtype PProposalLock (s :: S) = PProposalLock
     (PlutusType, PIsData, PDataFields)
     via (PIsDataReprInstances PProposalLock)
 
+deriving via
+  PAsData (PIsDataReprInstances PProposalLock)
+  instance
+    PTryFrom PData (PAsData PProposalLock)
+
 instance PUnsafeLiftDecl PProposalLock where type PLifted PProposalLock = ProposalLock
-deriving via (DerivePConstantViaData ProposalLock PProposalLock) instance (PConstant ProposalLock)
-
---------------------------------------------------------------------------------
-{- What this Policy does
-
-   For minting:
-     Check that exactly one state thread is minted
-     Check that an output exists with a state thread and a valid datum
-     Check that no state thread is an input
-     assert TokenName == ValidatorHash of the script that we pay to
-
-   For burning:
-     Check that exactly one state thread is burned
-     Check that datum at state thread is valid and not locked
--}
---------------------------------------------------------------------------------
-
--- | Policy for Stake state threads.
-stakePolicy :: Stake -> ClosedTerm PMintingPolicy
-stakePolicy stake =
-  plam $ \_redeemer ctx' -> P.do
-    ctx <- pletFields @'["txInfo", "purpose"] ctx'
-    txInfo' <- plet ctx.txInfo
-    txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
-
-    PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
-    ownSymbol <- plet $ pfield @"_0" # ownSymbol'
-    spentST <- plet $ psymbolValueOf # ownSymbol #$ pvalueSpent # pfromData txInfo'
-    mintedST <- plet $ psymbolValueOf # ownSymbol # txInfo.mint
-
-    let burning = P.do
-          passert "ST at inputs must be 1" $
-            spentST #== 1
-
-          passert "ST burned" $
-            mintedST #== -1
-
-          passert "An unlocked input existed containing an ST" $
-            anyInput @PStakeDatum # pfromData txInfo'
-              #$ plam
-              $ \value _ stakeDatum' -> P.do
-                let hasST = psymbolValueOf # ownSymbol # value #== 1
-                let unlocked = pnot # (stakeLocked # stakeDatum')
-                hasST #&& unlocked
-
-          popaque (pconstant ())
-
-    let minting = P.do
-          passert "ST at inputs must be 0" $
-            spentST #== 0
-
-          passert "Minted ST must be exactly 1" $
-            mintedST #== 1
-
-          passert "A UTXO must exist with the correct output" $
-            anyOutput @PStakeDatum # pfromData txInfo'
-              #$ plam
-              $ \value address stakeDatum' -> P.do
-                let cred = pfield @"credential" # address
-                pmatch cred $ \case
-                  -- Should pay to a script address
-                  PPubKeyCredential _ -> pcon PFalse
-                  PScriptCredential validatorHash' -> P.do
-                    validatorHash <- pletFields @'["_0"] validatorHash'
-                    stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
-
-                    -- TODO: figure out why this is required :/ (specifically, why `validatorHash._0` is `PData`)
-                    tn <- plet (pfromData (punsafeCoerce validatorHash._0 :: Term _ (PAsData PTokenName)))
-
-                    let stValue =
-                          psingletonValue
-                            # ownSymbol
-                            -- This coerce is safe because the structure
-                            -- of PValidatorHash is the same as PTokenName.
-                            # tn
-                            # 1
-                    let expectedValue =
-                          paddValue
-                            # (pdiscreteValue stake.gtClassRef # stakeDatum.stakedAmount)
-                            # stValue
-                    let ownerSignsTransaction =
-                          ptxSignedBy
-                            # ctx.txInfo
-                            # stakeDatum.owner
-
-                    -- TODO: This is quite inefficient now, as it does two lookups
-                    -- instead of a more efficient single pass,
-                    -- but it doesn't really matter for this. At least it's correct.
-                    let valueCorrect =
-                          foldr1
-                            (#&&)
-                            [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
-                            , pgeqByClass' (untag stake.gtClassRef)
-                                # value
-                                # expectedValue
-                            , pgeqByClass
-                                # ownSymbol
-                                # tn
-                                # value
-                                # expectedValue
-                            ]
-
-                    ownerSignsTransaction
-                      #&& valueCorrect
-          popaque (pconstant ())
-
-    pif (0 #< mintedST) minting burning
-
---------------------------------------------------------------------------------
-
--- | Validator intended for Stake UTXOs to live in.
-stakeValidator :: Stake -> ClosedTerm PValidator
-stakeValidator stake =
-  plam $ \datum redeemer ctx' -> P.do
-    ctx <- pletFields @'["txInfo", "purpose"] ctx'
-    txInfo' <- plet ctx.txInfo
-    txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
-
-    -- TODO: Use PTryFrom
-    let stakeRedeemer :: Term _ PStakeRedeemer
-        stakeRedeemer = pfromData $ punsafeCoerce redeemer
-        stakeDatum' :: Term _ PStakeDatum
-        stakeDatum' = pfromData $ punsafeCoerce datum
-    stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
-
-    PSpending txOutRef <- pmatch $ pfromData ctx.purpose
-
-    PJust txInInfo <- pmatch $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfo'
-    ownAddress <- plet $ pfield @"address" #$ pfield @"resolved" # txInInfo
-    let continuingValue = pfield @"value" #$ pfield @"resolved" # txInInfo
-
-    -- Whether the owner signs this transaction or not.
-    ownerSignsTransaction <- plet $ ptxSignedBy # ctx.txInfo # stakeDatum.owner
-
-    stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake)
-    mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfo.mint
-    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfo'
-
-    -- Is the stake currently locked?
-    stakeIsLocked <- plet $ stakeLocked # stakeDatum'
-
-    pmatch stakeRedeemer $ \case
-      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
-        popaque (pconstant ())
-      --------------------------------------------------------------------------
-      PRetractVotes _ -> P.do
-        passert
-          "Owner signs this transaction"
-          ownerSignsTransaction
-        -- TODO: check proposal constraints
-        popaque (pconstant ())
-      --------------------------------------------------------------------------
-      PPermitVote _ -> P.do
-        passert
-          "Owner signs this transaction"
-          ownerSignsTransaction
-        -- TODO: check proposal constraints
-        popaque (pconstant ())
-      --------------------------------------------------------------------------
-      PDepositWithdraw r -> P.do
-        passert "ST at inputs must be 1" $
-          spentST #== 1
-        passert "Stake unlocked" $
-          pnot #$ stakeIsLocked
-        passert
-          "Owner signs this transaction"
-          ownerSignsTransaction
-        passert "A UTXO must exist with the correct output" $
-          anyOutput @PStakeDatum # txInfo'
-            #$ plam
-            $ \value address newStakeDatum' -> P.do
-              newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum'
-              delta <- plet $ pfield @"delta" # r
-              let isScriptAddress = pdata address #== ownAddress
-              let correctOutputDatum =
-                    foldr1
-                      (#&&)
-                      [ stakeDatum.owner #== newStakeDatum.owner
-                      , (stakeDatum.stakedAmount + delta) #== newStakeDatum.stakedAmount
-                      , -- We can't magically conjure GT anyway (no input to spend!)
-                        -- do we need to check this, really?
-                        zero #<= pfromData newStakeDatum.stakedAmount
-                      ]
-              let expectedValue = paddValue # continuingValue # (pdiscreteValue stake.gtClassRef # delta)
-
-              -- TODO: Same as above. This is quite inefficient now, as it does two lookups
-              -- instead of a more efficient single pass,
-              -- but it doesn't really matter for this. At least it's correct.
-              let valueCorrect =
-                    foldr1
-                      (#&&)
-                      [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
-                      , pgeqByClass' (untag stake.gtClassRef)
-                          # value
-                          # expectedValue
-                      , pgeqBySymbol
-                          # stCurrencySymbol
-                          # value
-                          # expectedValue
-                      ]
-
-              foldr1
-                (#&&)
-                [ ptraceIfFalse "isScriptAddress" isScriptAddress
-                , ptraceIfFalse "correctOutputDatum" correctOutputDatum
-                , ptraceIfFalse "valueCorrect" valueCorrect
-                ]
-
-        popaque (pconstant ())
+deriving via (DerivePConstantViaData ProposalLock PProposalLock) instance (PConstantDecl ProposalLock)
 
 --------------------------------------------------------------------------------
 
@@ -461,3 +259,58 @@ stakeLocked = phoistAcyclic $
     let locks :: Term _ (PBuiltinList (PAsData PProposalLock))
         locks = pfield @"lockedBy" # stakeDatum
      in pnotNull # locks
+
+-- | Find a stake owned by a particular PK.
+findStakeOwnedBy ::
+  Term
+    s
+    ( PAssetClass
+        :--> PPubKeyHash
+        :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum))
+        :--> PBuiltinList (PAsData PTxInInfo)
+        :--> PMaybe (PAsData PStakeDatum)
+    )
+findStakeOwnedBy = phoistAcyclic $
+  plam $ \ac pk datums inputs ->
+    pmatch (pfind # (isInputStakeOwnedBy # ac # pk # datums) # inputs) $ \case
+      PNothing -> pcon PNothing
+      PJust (pfromData -> v) -> P.do
+        let txOut = pfield @"resolved" # pto v
+        txOutF <- pletFields @'["datumHash"] $ txOut
+        pmatch txOutF.datumHash $ \case
+          PDNothing _ -> pcon PNothing
+          PDJust ((pfield @"_0" #) -> dh) -> P.do
+            ptryFindDatum @(PAsData PStakeDatum) # dh # datums
+
+stakeDatumOwnedBy :: Term _ (PPubKeyHash :--> PStakeDatum :--> PBool)
+stakeDatumOwnedBy =
+  phoistAcyclic $
+    plam $ \pk stakeDatum -> P.do
+      stakeDatumF <- pletFields @'["owner"] $ pto stakeDatum
+      stakeDatumF.owner #== pdata pk
+
+-- Does the input have a `Stake` owned by a particular PK?
+isInputStakeOwnedBy ::
+  Term
+    _
+    ( PAssetClass :--> PPubKeyHash
+        :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum))
+        :--> PAsData PTxInInfo
+        :--> PBool
+    )
+isInputStakeOwnedBy =
+  plam $ \ac ss datums txInInfo' -> P.do
+    PTxInInfo ((pfield @"resolved" #) -> txOut) <- pmatch $ pfromData txInInfo'
+    PTxOut txOut' <- pmatch txOut
+    txOutF <- pletFields @'["value", "datumHash"] txOut'
+    outStakeST <- plet $ passetClassValueOf # txOutF.value # ac
+    pmatch txOutF.datumHash $ \case
+      PDNothing _ -> pcon PFalse
+      PDJust ((pfield @"_0" #) -> datumHash) ->
+        pif
+          (outStakeST #== 1)
+          ( pmatch (ptryFindDatum @(PAsData PStakeDatum) # datumHash # datums) $ \case
+              PNothing -> pcon PFalse
+              PJust v -> stakeDatumOwnedBy # ss # pfromData (punsafeCoerce v)
+          )
+          (pcon PFalse)
diff --git a/agora/Agora/Stake/Scripts.hs b/agora/Agora/Stake/Scripts.hs
new file mode 100644
index 0000000..10e0df9
--- /dev/null
+++ b/agora/Agora/Stake/Scripts.hs
@@ -0,0 +1,405 @@
+{- |
+Module     : Agora.Stake.Scripts
+Maintainer : emi@haskell.fyi
+Description: Plutus Scripts for Stakes.
+
+Plutus Scripts for Stakes.
+-}
+module Agora.Stake.Scripts (stakePolicy, stakeValidator) where
+
+import Agora.SafeMoney (GTTag)
+import Agora.Stake
+import Agora.Utils (
+  anyInput,
+  anyOutput,
+  paddValue,
+  passert,
+  pfindTxInByTxOutRef,
+  pgeqByClass,
+  pgeqByClass',
+  pgeqBySymbol,
+  psingletonValue,
+  psymbolValueOf,
+  ptokenSpent,
+  ptxSignedBy,
+  pvalueSpent,
+  validatorHashToTokenName,
+ )
+import Plutarch.Api.V1 (
+  PCredential (PPubKeyCredential, PScriptCredential),
+  PMintingPolicy,
+  PScriptPurpose (PMinting, PSpending),
+  PTokenName,
+  PTxInfo,
+  PValidator,
+  mintingPolicySymbol,
+  mkMintingPolicy,
+ )
+import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
+import Plutarch.Internal (punsafeCoerce)
+import Plutarch.Monadic qualified as P
+import Plutarch.Numeric
+import Plutarch.SafeMoney (
+  Tagged (..),
+  pdiscreteValue',
+  untag,
+ )
+import Plutarch.TryFrom (ptryFrom)
+import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
+import Prelude hiding (Num (..))
+
+{- | Policy for Stake state threads.
+
+   == What this Policy does
+
+   === For minting:
+
+   - Check that exactly one state thread is minted.
+   - Check that an output exists with a state thread and a valid datum.
+   - Check that no state thread is an input.
+   - assert @'Plutus.V1.Ledger.Api.TokenName' == 'Plutus.V1.Ledger.Api.ValidatorHash'@
+     of the script that we pay to.
+
+   === For burning:
+
+   - Check that exactly one state thread is burned.
+   - Check that datum at state thread is valid and not locked.
+-}
+stakePolicy ::
+  -- | The (governance) token that a Stake can store.
+  Tagged GTTag AssetClass ->
+  ClosedTerm PMintingPolicy
+stakePolicy gtClassRef =
+  plam $ \_redeemer ctx' -> P.do
+    ctx <- pletFields @'["txInfo", "purpose"] ctx'
+    txInfo <- plet $ ctx.txInfo
+    let _a :: Term _ PTxInfo
+        _a = txInfo
+    txInfoF <- pletFields @'["mint", "inputs", "outputs", "signatories"] txInfo
+
+    PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
+    ownSymbol <- plet $ pfield @"_0" # ownSymbol'
+    spentST <- plet $ psymbolValueOf # ownSymbol #$ pvalueSpent # txInfoF.inputs
+    mintedST <- plet $ psymbolValueOf # ownSymbol # txInfoF.mint
+
+    let burning = P.do
+          passert "ST at inputs must be 1" $
+            spentST #== 1
+
+          passert "ST burned" $
+            mintedST #== -1
+
+          passert "An unlocked input existed containing an ST" $
+            anyInput @PStakeDatum # txInfo
+              #$ plam
+              $ \value _ stakeDatum' -> P.do
+                let hasST = psymbolValueOf # ownSymbol # value #== 1
+                let unlocked = pnot # (stakeLocked # stakeDatum')
+                hasST #&& unlocked
+
+          popaque (pconstant ())
+
+    let minting = P.do
+          passert "ST at inputs must be 0" $
+            spentST #== 0
+
+          passert "Minted ST must be exactly 1" $
+            mintedST #== 1
+
+          passert "A UTXO must exist with the correct output" $
+            anyOutput @PStakeDatum # txInfo
+              #$ plam
+              $ \value address stakeDatum' -> P.do
+                let cred = pfield @"credential" # address
+                pmatch cred $ \case
+                  -- Should pay to a script address
+                  PPubKeyCredential _ -> pcon PFalse
+                  PScriptCredential validatorHash -> P.do
+                    stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
+
+                    tn :: Term _ PTokenName <- plet (validatorHashToTokenName $ pfromData $ pfield @"_0" # validatorHash)
+
+                    let stValue =
+                          psingletonValue
+                            # ownSymbol
+                            -- This coerce is safe because the structure
+                            -- of PValidatorHash is the same as PTokenName.
+                            # tn
+                            # 1
+                    let expectedValue =
+                          paddValue
+                            # (pdiscreteValue' gtClassRef # stakeDatum.stakedAmount)
+                            # stValue
+                    let ownerSignsTransaction =
+                          ptxSignedBy
+                            # txInfoF.signatories
+                            # stakeDatum.owner
+
+                    -- TODO: This is quite inefficient now, as it does two lookups
+                    -- instead of a more efficient single pass,
+                    -- but it doesn't really matter for this. At least it's correct.
+                    let valueCorrect =
+                          foldr1
+                            (#&&)
+                            [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
+                            , pgeqByClass' (untag gtClassRef)
+                                # value
+                                # expectedValue
+                            , pgeqByClass
+                                # ownSymbol
+                                # tn
+                                # value
+                                # expectedValue
+                            ]
+
+                    ownerSignsTransaction
+                      #&& valueCorrect
+          popaque (pconstant ())
+
+    pif (0 #< mintedST) minting burning
+
+--------------------------------------------------------------------------------
+
+{- | Validator intended for Stake UTXOs to be locked by.
+
+== What this Validator does:
+
+=== 'DepositWithdraw'
+
+Deposit or withdraw some GT to the stake.
+
+- Tx must be signed by the owner.
+- The 'stakedAmount' field must be updated.
+- The stake must not be locked.
+- The new UTXO must have the previous value plus the difference
+  as stated by the redeemer.
+
+=== 'PermitVote'
+
+Allow a 'ProposalLock' to be put on the stake in order to vote
+on a proposal.
+
+- A proposal token must be spent alongside the stake.
+
+  * Its total votes must be correctly updated to include this stake's
+    contribution.
+
+- Tx must be signed by the owner.
+
+=== 'RetractVotes'
+
+Remove a 'ProposalLock' set when voting on a proposal.
+
+- A proposal token must be spent alongside the stake.
+- Tx must be signed by the owner.
+
+=== 'Destroy'
+
+Destroy the stake in order to reclaim the min ADA.
+
+- The stake must not be locked.
+- Tx must be signed by the owner.
+
+=== 'WitnessStake'
+
+Allow this Stake to be included in a transaction without making
+any changes to it. In the future,
+this could use [CIP-31](https://cips.cardano.org/cips/cip31/) instead.
+
+- Tx must be signed by the owner __or__ a proposal ST token must be spent
+  alongside the stake.
+- The datum and value must remain unchanged.
+-}
+stakeValidator :: Stake -> ClosedTerm PValidator
+stakeValidator stake =
+  plam $ \datum redeemer ctx' -> P.do
+    ctx <- pletFields @'["txInfo", "purpose"] ctx'
+    txInfo <- plet $ pfromData ctx.txInfo
+    txInfoF <- pletFields @'["mint", "inputs", "outputs", "signatories"] txInfo
+
+    (pfromData -> stakeRedeemer, _) <- ptryFrom redeemer
+
+    -- TODO: Use PTryFrom
+    let stakeDatum' :: Term _ PStakeDatum
+        stakeDatum' = pfromData $ punsafeCoerce datum
+    stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
+
+    PSpending txOutRef <- pmatch $ pfromData ctx.purpose
+
+    PJust txInInfo <- pmatch $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfoF.inputs
+    ownAddress <- plet $ pfield @"address" #$ pfield @"resolved" # txInInfo
+    let continuingValue = pfield @"value" #$ pfield @"resolved" # txInInfo
+
+    -- Whether the owner signs this transaction or not.
+    ownerSignsTransaction <- plet $ ptxSignedBy # txInfoF.signatories # stakeDatum.owner
+
+    stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake.gtClassRef)
+    mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfoF.mint
+    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'
+
+    pmatch stakeRedeemer $ \case
+      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
+
+        popaque (pconstant ())
+      --------------------------------------------------------------------------
+      PRetractVotes _ -> P.do
+        passert
+          "Owner signs this transaction"
+          ownerSignsTransaction
+
+        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
+
+        -- 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
+        passert "ST at inputs must be 1" $
+          spentST #== 1
+
+        let AssetClass (propCs, propTn) = stake.proposalSTClass
+            propAssetClass = passetClass # pconstant propCs # pconstant propTn
+            proposalTokenMoved =
+              ptokenSpent
+                # 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)
+
+        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
+                    , ptraceIfFalse "correctOutputDatum" correctOutputDatum
+                    ]
+                )
+                (pcon PFalse)
+        popaque (pconstant ())
+      PDepositWithdraw r -> P.do
+        passert "ST at inputs must be 1" $
+          spentST #== 1
+        passert "Stake unlocked" $
+          pnot #$ stakeIsLocked
+        passert
+          "Owner signs this transaction"
+          ownerSignsTransaction
+        passert "A UTXO must exist with the correct output" $
+          anyOutput @PStakeDatum # txInfo
+            #$ plam
+            $ \value address newStakeDatum' -> P.do
+              newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum'
+              delta <- plet $ pfield @"delta" # r
+              let isScriptAddress = pdata address #== ownAddress
+              let correctOutputDatum =
+                    foldr1
+                      (#&&)
+                      [ stakeDatum.owner #== newStakeDatum.owner
+                      , (stakeDatum.stakedAmount + delta) #== newStakeDatum.stakedAmount
+                      , -- We can't magically conjure GT anyway (no input to spend!)
+                        -- do we need to check this, really?
+                        zero #<= pfromData newStakeDatum.stakedAmount
+                      ]
+              let expectedValue = paddValue # continuingValue # (pdiscreteValue' stake.gtClassRef # delta)
+
+              -- TODO: Same as above. This is quite inefficient now, as it does two lookups
+              -- instead of a more efficient single pass,
+              -- but it doesn't really matter for this. At least it's correct.
+              let valueCorrect =
+                    foldr1
+                      (#&&)
+                      [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
+                      , pgeqByClass' (untag stake.gtClassRef)
+                          # value
+                          # expectedValue
+                      , pgeqBySymbol
+                          # stCurrencySymbol
+                          # value
+                          # expectedValue
+                      ]
+
+              foldr1
+                (#&&)
+                [ ptraceIfFalse "isScriptAddress" isScriptAddress
+                , ptraceIfFalse "correctOutputDatum" correctOutputDatum
+                , ptraceIfFalse "valueCorrect" valueCorrect
+                ]
+
+        popaque (pconstant ())
diff --git a/agora/Agora/Treasury.hs b/agora/Agora/Treasury.hs
index 3f48a1f..f3ff441 100644
--- a/agora/Agora/Treasury.hs
+++ b/agora/Agora/Treasury.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE TemplateHaskell #-}
+
 {- |
 Module: Agora.Treasury
 Maintainer: jack@mlabs.city
@@ -8,24 +10,60 @@ treasury.
 -}
 module Agora.Treasury (module Agora.Treasury) where
 
+import Agora.AuthorityToken (singleAuthorityTokenBurned)
+import Agora.Utils (passert)
 import GHC.Generics qualified as GHC
 import Generics.SOP
+import Plutarch.Api.V1 (PValidator)
 import Plutarch.Api.V1.Contexts (PScriptPurpose (PMinting))
-import Plutarch.Api.V1.Value (PCurrencySymbol, PValue)
+import Plutarch.Api.V1.Value (PValue)
 import Plutarch.DataRepr (
-  PDataFields,
+  DerivePConstantViaData (..),
   PIsDataReprInstances (PIsDataReprInstances),
  )
+import Plutarch.Lift (PConstantDecl (..), PLifted (..), PUnsafeLiftDecl)
 import Plutarch.Monadic qualified as P
+import Plutarch.TryFrom (PTryFrom, ptryFrom)
 import Plutus.V1.Ledger.Value (CurrencySymbol)
+import PlutusTx qualified
 
 --------------------------------------------------------------------------------
 
-import Agora.AuthorityToken (singleAuthorityTokenBurned)
-import Agora.Utils (passert)
-import Plutarch (popaque)
-import Plutarch.Api.V1 (PValidator)
-import Plutarch.Unsafe (punsafeCoerce)
+-- | Redeemer for Treasury actions.
+data TreasuryRedeemer
+  = -- | Allow transaction to pass by delegating to GAT burn.
+    SpendTreasuryGAT
+  deriving stock (Eq, Show, GHC.Generic)
+
+PlutusTx.makeIsDataIndexed
+  ''TreasuryRedeemer
+  [ ('SpendTreasuryGAT, 0)
+  ]
+
+--------------------------------------------------------------------------------
+
+{- | Plutarch level type representing valid redeemers of the
+     treasury.
+-}
+newtype PTreasuryRedeemer (s :: S)
+  = -- | Alters treasury parameters, subject to the burning of a
+    --   governance authority token.
+    PSpendTreasuryGAT (Term s (PDataRecord '[]))
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic, PIsDataRepr)
+  deriving
+    (PlutusType, PIsData)
+    via PIsDataReprInstances PTreasuryRedeemer
+
+deriving via
+  PAsData (PIsDataReprInstances PTreasuryRedeemer)
+  instance
+    PTryFrom PData (PAsData PTreasuryRedeemer)
+
+instance PUnsafeLiftDecl PTreasuryRedeemer where type PLifted PTreasuryRedeemer = TreasuryRedeemer
+deriving via (DerivePConstantViaData TreasuryRedeemer PTreasuryRedeemer) instance (PConstantDecl TreasuryRedeemer)
+
+--------------------------------------------------------------------------------
 
 {- | Validator ensuring that transactions consuming the treasury
      do so in a valid manner.
@@ -33,12 +71,8 @@ import Plutarch.Unsafe (punsafeCoerce)
 treasuryValidator ::
   CurrencySymbol ->
   ClosedTerm PValidator
-treasuryValidator gatCs' = plam $ \datum redeemer ctx' -> P.do
-  -- TODO: Use PTryFrom
-  let treasuryRedeemer :: Term _ (PAsData PTreasuryRedeemer)
-      treasuryRedeemer = punsafeCoerce redeemer
-      _treasuryDatum' :: Term _ (PAsData PTreasuryDatum)
-      _treasuryDatum' = punsafeCoerce datum
+treasuryValidator gatCs' = plam $ \_datum redeemer ctx' -> P.do
+  (treasuryRedeemer, _) <- ptryFrom redeemer
 
   -- plet required fields from script context.
   ctx <- pletFields @["txInfo", "purpose"] ctx'
@@ -47,7 +81,7 @@ treasuryValidator gatCs' = plam $ \datum redeemer ctx' -> P.do
   PMinting _ <- pmatch ctx.purpose
 
   -- Ensure redeemer type is valid.
-  PAlterTreasuryParams _ <- pmatch $ pfromData treasuryRedeemer
+  PSpendTreasuryGAT _ <- pmatch $ pfromData treasuryRedeemer
 
   -- Get the minted value from txInfo.
   txInfo' <- plet ctx.txInfo
@@ -60,37 +94,3 @@ treasuryValidator gatCs' = plam $ \datum redeemer ctx' -> P.do
   passert "A single authority token has been burned" $ singleAuthorityTokenBurned gatCs txInfo' mint
 
   popaque $ pconstant ()
-
-{- | Plutarch level type representing datum of the treasury.
-     Contains:
-
-       - @stateThread@ representing the asset class of the
-         treasury's state thread token.
--}
-newtype PTreasuryDatum (s :: S)
-  = PTreasuryDatum
-      ( Term
-          s
-          ( PDataRecord
-              '[ "stateThread" ':= PCurrencySymbol
-               ]
-          )
-      )
-  deriving stock (GHC.Generic)
-  deriving anyclass (Generic, PIsDataRepr)
-  deriving
-    (PlutusType, PIsData, PDataFields)
-    via PIsDataReprInstances PTreasuryDatum
-
-{- | Plutarch level type representing valid redeemers of the
-     treasury.
--}
-newtype PTreasuryRedeemer (s :: S)
-  = -- | Alters treasury parameters, subject to the burning of a
-    --   governance authority token.
-    PAlterTreasuryParams (Term s (PDataRecord '[]))
-  deriving stock (GHC.Generic)
-  deriving anyclass (Generic, PIsDataRepr)
-  deriving
-    (PlutusType, PIsData)
-    via PIsDataReprInstances PTreasuryRedeemer
diff --git a/agora/Agora/Utils.hs b/agora/Agora/Utils.hs
index 48e5af3..874ecfe 100644
--- a/agora/Agora/Utils.hs
+++ b/agora/Agora/Utils.hs
@@ -10,15 +10,13 @@ module Agora.Utils (
   passert,
   pfind',
   pfindDatum,
-  pfindDatum',
+  ptryFindDatum,
   pvalueSpent,
   ptxSignedBy,
   paddValue,
   plookup,
   pfromMaybe,
   psymbolValueOf,
-  passetClassValueOf,
-  passetClassValueOf',
   pgeqByClass,
   pgeqBySymbol,
   pgeqByClass',
@@ -27,6 +25,10 @@ module Agora.Utils (
   pfindMap,
   pnotNull,
   pisJust,
+  ptokenSpent,
+  pkeysEqual,
+  pnub,
+  pisUniq,
 
   -- * Functions which should (probably) not be upstreamed
   anyOutput,
@@ -36,6 +38,8 @@ module Agora.Utils (
   scriptHashFromAddress,
   findOutputsToAddress,
   findTxOutDatum,
+  validatorHashToTokenName,
+  getMintingPolicySymbol,
 ) where
 
 --------------------------------------------------------------------------------
@@ -52,21 +56,27 @@ import Plutarch.Api.V1 (
   PDatumHash,
   PMap,
   PMaybeData (PDJust),
+  PMintingPolicy,
   PPubKeyHash,
-  PTokenName,
+  PTokenName (PTokenName),
   PTuple,
   PTxInInfo (PTxInInfo),
-  PTxInfo (PTxInfo),
+  PTxInfo,
   PTxOut (PTxOut),
   PTxOutRef,
   PValidatorHash,
   PValue,
+  mintingPolicySymbol,
+  mkMintingPolicy,
  )
 import Plutarch.Api.V1.AssocMap (PMap (PMap))
+import Plutarch.Api.V1.Extra (PAssetClass, passetClassValueOf, pvalueOf)
 import Plutarch.Api.V1.Value (PValue (PValue))
 import Plutarch.Builtin (ppairDataBuiltin)
-import Plutarch.Internal (punsafeCoerce)
+import Plutarch.Map.Extra (pkeys)
 import Plutarch.Monadic qualified as P
+import Plutarch.TryFrom (PTryFrom, ptryFrom)
+import Plutus.V1.Ledger.Api (CurrencySymbol)
 
 --------------------------------------------------------------------------------
 -- Validator-level utility functions
@@ -76,24 +86,24 @@ passert :: Term s PString -> Term s PBool -> Term s k -> Term s k
 passert errorMessage check k = pif check k (ptraceError errorMessage)
 
 -- | Find a datum with the given hash.
-pfindDatum :: Term s (PDatumHash :--> PTxInfo :--> PMaybe PDatum)
+pfindDatum :: Term s (PDatumHash :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PMaybe PDatum)
 pfindDatum = phoistAcyclic $
-  plam $ \datumHash txInfo'' -> P.do
-    PTxInfo txInfo' <- pmatch txInfo''
-    plookupTuple # datumHash #$ pfield @"data" # txInfo'
+  plam $ \datumHash datums -> plookupTuple # datumHash # datums
 
-{- | Find a datum with the given hash.
-NOTE: this is unsafe in the sense that, if the data layout is wrong, this is UB.
--}
-pfindDatum' :: PIsData a => Term s (PDatumHash :--> PTxInfo :--> PMaybe (PAsData a))
-pfindDatum' = phoistAcyclic $ plam $ \dh x -> punsafeCoerce $ pfindDatum # dh # x
+-- | Find a datum with the given hash, and `ptryFrom` it.
+ptryFindDatum :: forall (a :: PType) (s :: S). PTryFrom PData a => Term s (PDatumHash :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PMaybe a)
+ptryFindDatum = phoistAcyclic $
+  plam $ \datumHash inputs ->
+    pmatch (pfindDatum # datumHash # inputs) $ \case
+      PNothing -> pcon PNothing
+      PJust datum -> P.do
+        (datum', _) <- ptryFrom (pto datum)
+        pcon (PJust datum')
 
 -- | Check if a PubKeyHash signs this transaction.
-ptxSignedBy :: Term s (PTxInfo :--> PAsData PPubKeyHash :--> PBool)
+ptxSignedBy :: Term s (PBuiltinList (PAsData PPubKeyHash) :--> PAsData PPubKeyHash :--> PBool)
 ptxSignedBy = phoistAcyclic $
-  plam $ \txInfo' pkh -> P.do
-    txInfo <- pletFields @'["signatories"] txInfo'
-    pelem @PBuiltinList # pkh # txInfo.signatories
+  plam $ \sigs sig -> pelem # sig # sigs
 
 -- | Get the first element that matches a predicate or return Nothing.
 pfind' ::
@@ -183,30 +193,17 @@ psymbolValueOf =
       PMap m <- pmatch (pfromData m')
       pfoldr # plam (\x v -> pfromData (psndBuiltin # x) + v) # 0 # m
 
--- | Extract amount from PValue belonging to a Plutarch-level asset class.
-passetClassValueOf ::
-  Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PInteger)
-passetClassValueOf =
-  phoistAcyclic $
-    plam $ \sym token value'' -> P.do
-      PValue value' <- pmatch value''
-      PMap value <- pmatch value'
-      m' <- pexpectJust 0 (plookup # pdata sym # value)
-      PMap m <- pmatch (pfromData m')
-      v <- pexpectJust 0 (plookup # pdata token # m)
-      pfromData v
-
 -- | Extract amount from PValue belonging to a Haskell-level AssetClass.
 passetClassValueOf' :: AssetClass -> Term s (PValue :--> PInteger)
 passetClassValueOf' (AssetClass (sym, token)) =
-  passetClassValueOf # pconstant sym # pconstant token
+  phoistAcyclic $ plam $ \value -> pvalueOf # value # pconstant sym # pconstant token
 
 -- | Return '>=' on two values comparing by only a particular AssetClass.
 pgeqByClass :: Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PValue :--> PBool)
 pgeqByClass =
   phoistAcyclic $
     plam $ \cs tn a b ->
-      passetClassValueOf # cs # tn # b #<= passetClassValueOf # cs # tn # a
+      pvalueOf # b # cs # tn #<= pvalueOf # a # cs # tn
 
 -- | Return '>=' on two values comparing by only a particular CurrencySymbol.
 pgeqBySymbol :: Term s (PCurrencySymbol :--> PValue :--> PValue :--> PBool)
@@ -262,46 +259,100 @@ paddValue = phoistAcyclic $
       )
 
 -- | Sum of all value at input.
-pvalueSpent :: Term s (PTxInfo :--> PValue)
+pvalueSpent :: Term s (PBuiltinList (PAsData PTxInInfo) :--> PValue)
 pvalueSpent = phoistAcyclic $
-  plam $ \txInfo' ->
-    pmatch txInfo' $ \(PTxInfo txInfo) ->
-      pfoldr
-        # plam
-          ( \txInInfo' v ->
-              pmatch
-                (pfromData txInInfo')
-                $ \(PTxInInfo txInInfo) ->
-                  paddValue
-                    # pmatch
-                      (pfield @"resolved" # txInInfo)
-                      (\(PTxOut o) -> pfromData $ pfield @"value" # o)
-                    # v
-          )
-        # pconstant mempty
-        # (pfield @"inputs" # txInfo)
+  plam $ \inputs ->
+    pfoldr
+      # plam
+        ( \txInInfo' v ->
+            pmatch
+              (pfromData txInInfo')
+              $ \(PTxInInfo txInInfo) ->
+                paddValue
+                  # pmatch
+                    (pfield @"resolved" # txInInfo)
+                    (\(PTxOut o) -> pfromData $ pfield @"value" # o)
+                  # v
+        )
+      # pconstant mempty
+      # inputs
 
 -- | Find the TxInInfo by a TxOutRef.
-pfindTxInByTxOutRef :: Term s (PTxOutRef :--> PTxInfo :--> PMaybe PTxInInfo)
+pfindTxInByTxOutRef :: Term s (PTxOutRef :--> PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxInInfo)
 pfindTxInByTxOutRef = phoistAcyclic $
-  plam $ \txOutRef txInfo' ->
-    pmatch txInfo' $ \(PTxInfo txInfo) ->
-      pfindMap
-        # plam
-          ( \txInInfo' ->
-              plet (pfromData txInInfo') $ \r ->
-                pmatch r $ \(PTxInInfo txInInfo) ->
-                  pif
-                    (pdata txOutRef #== pfield @"outRef" # txInInfo)
-                    (pcon (PJust r))
-                    (pcon PNothing)
-          )
-        #$ (pfield @"inputs" # txInfo)
+  plam $ \txOutRef inputs ->
+    pfindMap
+      # plam
+        ( \txInInfo' ->
+            plet (pfromData txInInfo') $ \r ->
+              pmatch r $ \(PTxInInfo txInInfo) ->
+                pif
+                  (pdata txOutRef #== pfield @"outRef" # txInInfo)
+                  (pcon (PJust r))
+                  (pcon PNothing)
+        )
+      #$ inputs
 
 -- | True if a list is not empty.
 pnotNull :: forall list a. PIsListLike list a => Term _ (list a :--> PBool)
 pnotNull = phoistAcyclic $ plam $ pelimList (\_ _ -> pcon PTrue) (pcon PFalse)
 
+{- | Check if a particular asset class has been spent in the input list.
+
+     When using this as an authority check, you __MUST__ ensure the authority
+     knows how to ensure its end of the contract.
+-}
+ptokenSpent :: forall {s :: S}. Term s (PAssetClass :--> PBuiltinList (PAsData PTxInInfo) :--> PBool)
+ptokenSpent =
+  plam $ \tokenClass inputs ->
+    0
+      #< pfoldr @PBuiltinList
+        # plam
+          ( \txInInfo' acc -> P.do
+              PTxInInfo txInInfo <- pmatch (pfromData txInInfo')
+              PTxOut txOut' <- pmatch $ pfromData $ pfield @"resolved" # txInInfo
+              txOut <- pletFields @'["value"] txOut'
+              let txOutValue = pfromData txOut.value
+              acc + passetClassValueOf # txOutValue # tokenClass
+          )
+        # 0
+        # inputs
+
+{- | True if both maps have exactly the same keys.
+     Using @'#=='@ is not sufficient, because keys returned are not ordered.
+-}
+pkeysEqual :: forall (s :: S) k a b. Term s (PMap k a :--> PMap k b :--> PBool)
+pkeysEqual = phoistAcyclic $
+  plam $ \p q -> P.do
+    pks <- plet $ pkeys # p
+    qks <- plet $ pkeys # q
+    pall # plam (\pk -> pelem # pk # qks) # pks
+      #&& pall # plam (\qk -> pelem # qk # pks) # qks
+
+-- | / O(n^2) /. Clear out duplicates in a list. The order is not preserved.
+pnub :: forall list a (s :: S). (PEq a, PIsListLike list a) => Term s (list a :--> list a)
+pnub =
+  phoistAcyclic $
+    precList
+      ( \self x xs ->
+          pif
+            (pnot #$ pelem # x # xs)
+            (pcons # x # (self # xs))
+            (self # xs)
+      )
+      (const pnil)
+
+-- | / O(n^2) /. Check if a list contains no duplicates.
+pisUniq :: forall list a (s :: S). (PEq a, PIsListLike list a) => Term s (list a :--> PBool)
+pisUniq =
+  phoistAcyclic $
+    precList
+      ( \self x xs ->
+          (pnot #$ pelem # x # xs)
+            #&& (self # xs)
+      )
+      (const $ pcon PTrue)
+
 --------------------------------------------------------------------------------
 {- Functions which should (probably) not be upstreamed
    All of these functions are quite inefficient.
@@ -311,18 +362,19 @@ pnotNull = phoistAcyclic $ plam $ pelimList (\_ _ -> pcon PTrue) (pcon PFalse)
 anyOutput ::
   forall (datum :: PType) s.
   ( PIsData datum
+  , PTryFrom PData (PAsData datum)
   ) =>
   Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
 anyOutput = phoistAcyclic $
   plam $ \txInfo' predicate -> P.do
-    txInfo <- pletFields @'["outputs"] txInfo'
+    txInfo <- pletFields @'["outputs", "datums"] txInfo'
     pany
       # plam
         ( \txOut'' -> P.do
             PTxOut txOut' <- pmatch (pfromData txOut'')
             txOut <- pletFields @'["value", "datumHash", "address"] txOut'
             PDJust dh <- pmatch txOut.datumHash
-            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \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
@@ -333,18 +385,19 @@ anyOutput = phoistAcyclic $
 allOutputs ::
   forall (datum :: PType) s.
   ( PIsData datum
+  , PTryFrom PData (PAsData datum)
   ) =>
   Term s (PTxInfo :--> (PTxOut :--> PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
 allOutputs = phoistAcyclic $
   plam $ \txInfo' predicate -> P.do
-    txInfo <- pletFields @'["outputs"] txInfo'
+    txInfo <- pletFields @'["outputs", "datums"] txInfo'
     pall
       # plam
         ( \txOut'' -> P.do
             PTxOut txOut' <- pmatch (pfromData txOut'')
             txOut <- pletFields @'["value", "datumHash", "address"] txOut'
             PDJust dh <- pmatch txOut.datumHash
-            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \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
@@ -355,11 +408,12 @@ allOutputs = phoistAcyclic $
 anyInput ::
   forall (datum :: PType) s.
   ( PIsData datum
+  , PTryFrom PData (PAsData datum)
   ) =>
   Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
 anyInput = phoistAcyclic $
   plam $ \txInfo' predicate -> P.do
-    txInfo <- pletFields @'["inputs"] txInfo'
+    txInfo <- pletFields @'["inputs", "datums"] txInfo'
     pany
       # plam
         ( \txInInfo'' -> P.do
@@ -368,7 +422,7 @@ anyInput = phoistAcyclic $
             PTxOut txOut' <- pmatch (pfromData txOut'')
             txOut <- pletFields @'["value", "datumHash", "address"] txOut'
             PDJust dh <- pmatch txOut.datumHash
-            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \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
@@ -385,10 +439,10 @@ psingletonValue = phoistAcyclic $
      in res
 
 -- | Finds the TxOut of an effect from TxInfo and TxOutRef
-findTxOutByTxOutRef :: Term s (PTxOutRef :--> PTxInfo :--> PMaybe PTxOut)
+findTxOutByTxOutRef :: Term s (PTxOutRef :--> PBuiltinList (PAsData PTxInInfo) :--> PMaybe PTxOut)
 findTxOutByTxOutRef = phoistAcyclic $
-  plam $ \txOutRef txInfo ->
-    pmatch (pfindTxInByTxOutRef # txOutRef # txInfo) $ \case
+  plam $ \txOutRef inputs ->
+    pmatch (pfindTxInByTxOutRef # txOutRef # inputs) $ \case
       PJust ((pfield @"resolved" #) -> txOut) -> pcon $ PJust txOut
       PNothing -> pcon PNothing
 
@@ -401,23 +455,28 @@ scriptHashFromAddress = phoistAcyclic $
       _ -> pcon PNothing
 
 -- | Find all TxOuts sent to an Address
-findOutputsToAddress :: Term s (PTxInfo :--> PAddress :--> PBuiltinList (PAsData PTxOut))
+findOutputsToAddress :: Term s (PBuiltinList (PAsData PTxOut) :--> PAddress :--> PBuiltinList (PAsData PTxOut))
 findOutputsToAddress = phoistAcyclic $
-  plam $ \info address' -> P.do
+  plam $ \outputs address' -> P.do
     address <- plet $ pdata address'
-    let outputs = pfromData $ pfield @"outputs" # info
-        filteredOutputs =
-          pfilter
-            # plam
-              (\(pfromData -> txOut) -> pfield @"address" # txOut #== address)
-            # outputs
-    filteredOutputs
+    pfilter # plam (\(pfromData -> txOut) -> pfield @"address" # txOut #== address)
+      # outputs
 
 -- | Find the data corresponding to a TxOut, if there is one
-findTxOutDatum :: Term s (PTxInfo :--> PTxOut :--> PMaybe PDatum)
+findTxOutDatum :: Term s (PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PTxOut :--> PMaybe PDatum)
 findTxOutDatum = phoistAcyclic $
-  plam $ \info out -> P.do
+  plam $ \datums out -> P.do
     datumHash' <- pmatch $ pfromData $ pfield @"datumHash" # out
     case datumHash' of
-      PDJust ((pfield @"_0" #) -> datumHash) -> pfindDatum # datumHash # info
+      PDJust ((pfield @"_0" #) -> datumHash) -> pfindDatum # datumHash # datums
       _ -> pcon PNothing
+
+{- | Safely convert a 'PValidatorHash' into a 'PTokenName'. This can be useful for tagging
+     tokens for extra safety.
+-}
+validatorHashToTokenName :: forall (s :: S). Term s PValidatorHash -> Term s PTokenName
+validatorHashToTokenName vh = pcon (PTokenName (pto vh))
+
+-- | Get the CurrencySymbol of a PMintingPolicy.
+getMintingPolicySymbol :: ClosedTerm PMintingPolicy -> CurrencySymbol
+getMintingPolicySymbol v = mintingPolicySymbol $ mkMintingPolicy v
diff --git a/agora/PPrelude.hs b/agora/PPrelude.hs
index 3232cf9..5878ff4 100644
--- a/agora/PPrelude.hs
+++ b/agora/PPrelude.hs
@@ -11,8 +11,7 @@ module PPrelude (
   module Plutarch,
 ) where
 
--- NOTE: These are not exported by Plutarch.Prelude, for some reason.
--- Maybe we can 'fix' this upstream?
-import Plutarch (ClosedTerm, POpaque, compile)
+-- 'compile' is not exported by Plutarch.Prelude.
+import Plutarch (compile)
 import Plutarch.Prelude
 import Prelude
diff --git a/docs/tech-design/proposals.md b/docs/tech-design/proposals.md
index a3a3fb1..3a4a82d 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,35 +35,31 @@ 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' state being the initial state, and 'executed' and 'failed' being the terminating states.
+
+Note: this state-machine representation is purely conceptual and should not be expected to reflect technical implementation.
+**Please note that this state-machine representation is purely conceptual and should not be expected to reflect technical implementation.** This is because some transitions in the state machine representation don't need to happen on-chain, as a transaction. A key example of this is a proposal going from the "lock" phase to the "execution" phase. No on-chain transition takes place: it is simply that we have reached the time in the real-world, when the proposal is allowed to be executed.
+
+To make the following diagram clear, we employ the following terminology:
+
+
+> state
+> A 'state' in our conceptual FSM representation above. Useful for thinking about proposals. Does not necessarily reflect a change occurring on-chain.
+
+
+> period
+> A segment of real-world, POSIX time. As we transition from one period to another, a proposal's status (see below) will not be updated.
+
+
+> status
+> The 'status' of a proposal is stored in the proposal's datum and is thus always represented on-chain. Changing this requires a transaction to take place.
+
 
 ![](../diagrams/ProposalStateMachine.svg)
 
-#### When may interactions occur?
-
-Consider the following 'stages' of a proposal:
-
--   `S`: when the proposal was created.
--   `D`: the length of the draft period.
--   `V`: the length of the voting period.
--   `L`: the length of the locking period.
--   `E`: the length of the execution period.
-
-| Action                              | Valid POSIXTimeRange                | Valid _stored_ state(s) |
-|-------------------------------------|-------------------------------------|-------------------------|
-| Witness                             | \[S, ∞)                             | \*                      |
-| Cosign                              | \[S, S + D)                         | Draft                   |
-| AdvanceProposal                     | \[S, S + D)                         | Draft                   |
-| Vote                                | \[S + D, S + D + V)                 | Voting                  |
-| Unlock                              | \[S + D, ∞)                         | \*                      |
-| CountVotes                          | \[S + D + V, S + D + V + L)         | Voting                  |
-| ExecuteProposal (if quorum reached) | \[S + D + V + L, S + D + V + L + E) | Voting                  |
-
-> Jack 2022-02-02: I will consider revising this table further at a later time.
-
 #### Draft phase
 
-During the draft phase, a new UTXO at the proposal script  has been created. At this stage, only votes in favor of co-signing the draft are counted. For the proposal to transition to the voting phase, a threshold of GT will have to be staked backing the proposal. This threshold will be determined on a per-system basis and could itself be a 'governable' parameter. It's important to note that cosignatures are not locking votes. Cosignatures are more like a delegated approval to a proposal. The sum of all cosignatures must tally to the threshold, and all cosigner stake datums must fit into a single transaction to witness their size.
+During the draft phase, a new UTXO at the proposal script  has been created. At this stage, only votes in favor of co-signing the draft are counted. For the proposal to transition to the voting phase, a threshold of GT will have to be staked backing the proposal. This threshold will be determined on a per-system basis and could itself be a 'governable' parameter. It's important to note that cosignatures are not locking votes. Cosignatures are more like a delegated approval to a proposal. The sum of all cosignatures must tally to the threshold, and all cosigner stake datums must fit into a single transaction to witness their size. A limit on the maximum amount of cosigners is placed in order to prevent a situation where the stake datums no longer fit in the transaction. The number doesn't matter and may be expressed in a parameterized way.
 
 #### Voting phase
 
diff --git a/flake.lock b/flake.lock
index 73e7d0d..00c46fe 100644
--- a/flake.lock
+++ b/flake.lock
@@ -117,23 +117,6 @@
         "type": "github"
       }
     },
-    "autodocodec": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1644358110,
-        "narHash": "sha256-X1TNZlmO2qDFk3OL4Z1v/gzvd3ouoACAiMweutsYek4=",
-        "owner": "srid",
-        "repo": "autodocodec",
-        "rev": "42b42a7407f33c6c74fa4e8c84906aebfed28daf",
-        "type": "github"
-      },
-      "original": {
-        "owner": "srid",
-        "ref": "ghc921",
-        "repo": "autodocodec",
-        "type": "github"
-      }
-    },
     "cabal-32": {
       "flake": false,
       "locked": {
@@ -463,21 +446,6 @@
         "type": "github"
       }
     },
-    "flake-compat-ci_3": {
-      "locked": {
-        "lastModified": 1641672839,
-        "narHash": "sha256-Bdwv+DKeEMlRNPDpZxSz0sSrqQBvdKO5fZ8LmvrgCOU=",
-        "owner": "hercules-ci",
-        "repo": "flake-compat-ci",
-        "rev": "e832114bc18376c0f3fa13c19bf5ff253cc6570a",
-        "type": "github"
-      },
-      "original": {
-        "owner": "hercules-ci",
-        "repo": "flake-compat-ci",
-        "type": "github"
-      }
-    },
     "flake-compat_2": {
       "flake": false,
       "locked": {
@@ -495,22 +463,6 @@
       }
     },
     "flake-compat_3": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1641205782,
-        "narHash": "sha256-4jY7RCWUoZ9cKD8co0/4tFARpWB+57+r1bLLvXNJliY=",
-        "owner": "edolstra",
-        "repo": "flake-compat",
-        "rev": "b7547d3eed6f32d06102ead8991ec52ab0a4f1a7",
-        "type": "github"
-      },
-      "original": {
-        "owner": "edolstra",
-        "repo": "flake-compat",
-        "type": "github"
-      }
-    },
-    "flake-compat_4": {
       "flake": false,
       "locked": {
         "lastModified": 1606424373,
@@ -527,7 +479,7 @@
         "type": "github"
       }
     },
-    "flake-compat_5": {
+    "flake-compat_4": {
       "flake": false,
       "locked": {
         "lastModified": 1606424373,
@@ -981,7 +933,7 @@
     },
     "hercules-ci-agent": {
       "inputs": {
-        "flake-compat": "flake-compat_5",
+        "flake-compat": "flake-compat_4",
         "nix-darwin": "nix-darwin",
         "nixos-20_09": "nixos-20_09",
         "nixos-unstable": "nixos-unstable",
@@ -1004,7 +956,7 @@
     },
     "hercules-ci-effects": {
       "inputs": {
-        "flake-compat": "flake-compat_4",
+        "flake-compat": "flake-compat_3",
         "hercules-ci-agent": "hercules-ci-agent",
         "nixpkgs": "nixpkgs_3",
         "nixpkgs-nixops": "nixpkgs-nixops"
@@ -1088,6 +1040,55 @@
         "type": "github"
       }
     },
+    "hspec": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1649095108,
+        "narHash": "sha256-cPmt4hvmdh727VT6UAL8yFArmm4FAWeg3K5Qi3XtU4g=",
+        "owner": "srid",
+        "repo": "hspec",
+        "rev": "44f2a143e10c93df237af428457d0e4b74ae270a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "srid",
+        "ref": "askAncestors",
+        "repo": "hspec",
+        "type": "github"
+      }
+    },
+    "hspec-golden": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1648755064,
+        "narHash": "sha256-5a6BksZx00o2iL0Ei/L1Kkou2BsnsIagN+tTmqYyKfs=",
+        "owner": "stackbuilders",
+        "repo": "hspec-golden",
+        "rev": "4b0ad56b2de0254a7b1e0feda917656f78a5bcda",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stackbuilders",
+        "repo": "hspec-golden",
+        "type": "github"
+      }
+    },
+    "hspec-hedgehog": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1602603478,
+        "narHash": "sha256-XnS3zjQ7eh3iBOWq+Z/YcwrfWI55hV6k8LsZ8qm/qOc=",
+        "owner": "parsonsmatt",
+        "repo": "hspec-hedgehog",
+        "rev": "eb617d854542510f0129acdea4bf52e50b13042e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "parsonsmatt",
+        "repo": "hspec-hedgehog",
+        "type": "github"
+      }
+    },
     "iohk-nix": {
       "flake": false,
       "locked": {
@@ -1592,19 +1593,24 @@
     "plutarch": {
       "inputs": {
         "Shrinker": "Shrinker",
-        "autodocodec": "autodocodec",
         "cardano-base": "cardano-base",
         "cardano-crypto": "cardano-crypto",
         "cardano-prelude": "cardano-prelude",
         "cryptonite": "cryptonite",
-        "flake-compat": "flake-compat_3",
-        "flake-compat-ci": "flake-compat-ci_3",
+        "emanote": [
+          "plutarch",
+          "haskell-nix",
+          "nixpkgs-unstable"
+        ],
         "flat": "flat",
         "foundation": "foundation",
         "haskell-language-server": "haskell-language-server_2",
         "haskell-nix": "haskell-nix_4",
         "hercules-ci-effects": "hercules-ci-effects",
         "hs-memory": "hs-memory",
+        "hspec": "hspec",
+        "hspec-golden": "hspec-golden",
+        "hspec-hedgehog": "hspec-hedgehog",
         "iohk-nix": "iohk-nix_2",
         "nixpkgs": [
           "plutarch",
@@ -1614,24 +1620,21 @@
         "nixpkgs-2111": "nixpkgs-2111_5",
         "plutus": "plutus_2",
         "protolude": "protolude",
-        "safe-coloured-text": "safe-coloured-text",
         "sized-functors": "sized-functors",
-        "sydtest": "sydtest",
-        "th-extras": "th-extras",
-        "validity": "validity"
+        "th-extras": "th-extras"
       },
       "locked": {
-        "lastModified": 1648639396,
-        "narHash": "sha256-pAkEsIDXJckVYufVPUzD/4sq4/uE7iyV0IR2BuLhZjY=",
+        "lastModified": 1650382454,
+        "narHash": "sha256-b31DK+E/0MtR45+Z+F5U1E8jjcewvZ42UmFLZlXDAYM=",
         "owner": "peter-mlabs",
         "repo": "plutarch",
-        "rev": "a7a410da209b9c14c834a41e07b1c197c2a4dcd6",
+        "rev": "6ef18aacd02050fc07398e399cff5e8734c1045e",
         "type": "github"
       },
       "original": {
         "owner": "peter-mlabs",
         "repo": "plutarch",
-        "rev": "a7a410da209b9c14c834a41e07b1c197c2a4dcd6",
+        "rev": "6ef18aacd02050fc07398e399cff5e8734c1045e",
         "type": "github"
       }
     },
@@ -1771,23 +1774,6 @@
         "plutarch": "plutarch"
       }
     },
-    "safe-coloured-text": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1644357337,
-        "narHash": "sha256-sXSKw8m6O9K/H2BBiYqO5e4sJIo+9UP+UvEukRn28d8=",
-        "owner": "srid",
-        "repo": "safe-coloured-text",
-        "rev": "034f3612525568b422e0c62b52417d77b7cf31c2",
-        "type": "github"
-      },
-      "original": {
-        "owner": "srid",
-        "ref": "ghc921",
-        "repo": "safe-coloured-text",
-        "type": "github"
-      }
-    },
     "sized-functors": {
       "flake": false,
       "locked": {
@@ -1917,23 +1903,6 @@
         "type": "github"
       }
     },
-    "sydtest": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1645114028,
-        "narHash": "sha256-P6ZwwfFeN8fpi3fziz9yERTn7BfxdE/j/OofUu+4GdA=",
-        "owner": "srid",
-        "repo": "sydtest",
-        "rev": "9c6c7678f7aabe22e075aab810a6a2e304591d24",
-        "type": "github"
-      },
-      "original": {
-        "owner": "srid",
-        "ref": "ghc921",
-        "repo": "sydtest",
-        "type": "github"
-      }
-    },
     "th-extras": {
       "flake": false,
       "locked": {
@@ -1950,23 +1919,6 @@
         "rev": "787ed752c1e5d41b5903b74e171ed087de38bffa",
         "type": "github"
       }
-    },
-    "validity": {
-      "flake": false,
-      "locked": {
-        "lastModified": 1644358698,
-        "narHash": "sha256-dpMIu08qXMzy8Kilk/2VWpuwIsfqFtpg/3mkwt5pdjA=",
-        "owner": "srid",
-        "repo": "validity",
-        "rev": "f7982549b95d0ab727950dc876ca06b1862135ba",
-        "type": "github"
-      },
-      "original": {
-        "owner": "srid",
-        "ref": "ghc921",
-        "repo": "validity",
-        "type": "github"
-      }
     }
   },
   "root": "root",
diff --git a/flake.nix b/flake.nix
index 3b1756a..3da51ee 100644
--- a/flake.nix
+++ b/flake.nix
@@ -7,9 +7,10 @@
   # see https://github.com/NixOS/nix/issues/6013
   inputs.nixpkgs-2111 = { url = "github:NixOS/nixpkgs/nixpkgs-21.11-darwin"; };
 
-  # Rev is this PR https://github.com/peter-mlabs/plutarch/pull/5.
   inputs.plutarch.url =
-    "github:peter-mlabs/plutarch?rev=a7a410da209b9c14c834a41e07b1c197c2a4dcd6";
+    "github:peter-mlabs/plutarch?rev=6ef18aacd02050fc07398e399cff5e8734c1045e";
+  inputs.plutarch.inputs.emanote.follows =
+    "plutarch/haskell-nix/nixpkgs-unstable";
   inputs.plutarch.inputs.nixpkgs.follows =
     "plutarch/haskell-nix/nixpkgs-unstable";
 
diff --git a/hie.yaml b/hie.yaml
index 6020af6..04cd243 100644
--- a/hie.yaml
+++ b/hie.yaml
@@ -1,8 +1,2 @@
 cradle:
   cabal:
-    - path: "./agora"
-      component: "lib:agora"
-    - path: "./agora-bench"
-      component: "benchmark:agora-bench"
-    - path: "./agora-test"
-      component: "test:agora-test"