diff --git a/agora.cabal b/agora.cabal
index ab38454..53d3ed8 100644
--- a/agora.cabal
+++ b/agora.cabal
@@ -23,7 +23,6 @@ common lang
     pprelude (PPrelude as Prelude)
 
   default-extensions:
-    UndecidableInstances
     NoStarIsType
     BangPatterns
     BinaryLiterals
@@ -76,6 +75,8 @@ common lang
     TypeFamilies
     TypeOperators
     TypeSynonymInstances
+    UndecidableInstances
+    UndecidableInstances
     ViewPatterns
     OverloadedRecordDot
     QualifiedDo
@@ -116,9 +117,13 @@ library
   import:          lang, deps
   exposed-modules:
     Agora.AuthorityToken
+    Agora.SafeMoney
+    Agora.SafeMoney.QQ
+    Agora.Stake
     Agora.Treasury
+    Agora.Voting
 
-  other-modules:
+  other-modules:   Agora.Utils
   hs-source-dirs:  src
 
 library pprelude
diff --git a/bench.csv b/bench.csv
index c4fe975..a467473 100644
--- a/bench.csv
+++ b/bench.csv
@@ -1,2 +1,4 @@
-name,cpu,mem,size
-full_scripts:authorityTokenPolicy,1280339,4400,284
+name,cpu,mem,size
+full_scripts:authorityTokenPolicy,1399431,4800,421
+full_scripts:stakePolicy,3751498,12700,1610
+full_scripts:stakeValidator,3126265,10600,1500
diff --git a/bench/Main.hs b/bench/Main.hs
index ec50558..150f528 100644
--- a/bench/Main.hs
+++ b/bench/Main.hs
@@ -4,12 +4,24 @@ import Prelude
 
 --------------------------------------------------------------------------------
 
-import Plutarch.Benchmark
 import Plutus.V1.Ledger.Value qualified as Value
 
 --------------------------------------------------------------------------------
 
-import Agora.AuthorityToken qualified as Agora
+import Plutarch.Benchmark
+
+--------------------------------------------------------------------------------
+
+import Agora.AuthorityToken (
+  AuthorityToken (AuthorityToken),
+  authorityTokenPolicy,
+ )
+import Agora.SafeMoney (LQ)
+import Agora.Stake (
+  Stake (Stake),
+  stakePolicy,
+  stakeValidator,
+ )
 
 --------------------------------------------------------------------------------
 
@@ -21,5 +33,10 @@ benchmarks :: [NamedBenchmark]
 benchmarks =
   benchGroup
     "full_scripts"
-    [ bench "authorityTokenPolicy" $ Agora.authorityTokenPolicy (Agora.AuthorityToken (Value.assetClass "" ""))
+    [ bench "authorityTokenPolicy" $ authorityTokenPolicy authorityToken
+    , bench "stakePolicy" $ stakePolicy (Stake @LQ)
+    , bench "stakeValidator" $ stakeValidator (Stake @LQ)
     ]
+
+authorityToken :: AuthorityToken
+authorityToken = AuthorityToken (Value.assetClass "" "")
diff --git a/cabal.project b/cabal.project
index ec42141..86a0b28 100644
--- a/cabal.project
+++ b/cabal.project
@@ -2,3 +2,6 @@ packages: ./.
 
 benchmarks: true
 tests: true
+
+package plutarch
+  flags: +development
\ No newline at end of file
diff --git a/flake.lock b/flake.lock
index e68b47a..6247424 100644
--- a/flake.lock
+++ b/flake.lock
@@ -440,8 +440,6 @@
         "hpc-coveralls": "hpc-coveralls",
         "nix-tools": "nix-tools",
         "nixpkgs": [
-          "plutarch",
-          "haskell-nix",
           "nixpkgs-2111"
         ],
         "nixpkgs-2003": "nixpkgs-2003",
@@ -832,11 +830,11 @@
         "validity": "validity"
       },
       "locked": {
-        "lastModified": 1645006916,
-        "narHash": "sha256-j8o0D48LfDYqf07bi34474lkFnMZ5TNvcZmACVMw3yA=",
+        "lastModified": 1645200363,
+        "narHash": "sha256-k/ecf2uasWwBV+zq3daJVGY3xnsYkLe3zmT+k+iZ++A=",
         "owner": "Plutonomicon",
         "repo": "plutarch",
-        "rev": "c77fcd605269bd8183d5496e297eb38503ea0e29",
+        "rev": "473424c89b4457e58e009e65d411ace1efc3ea9e",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index e574172..103fea2 100644
--- a/flake.nix
+++ b/flake.nix
@@ -76,15 +76,18 @@
         let
           pkgs = nixpkgsFor system;
           pkgs' = nixpkgsFor' system;
+          inherit (pkgs.haskell-nix.tools ghcVersion {
+            inherit (plutarch.tools) fourmolu hlint;
+          })
+            fourmolu hlint;
         in pkgs.runCommand "format-check" {
           nativeBuildInputs = [
             pkgs'.git
             pkgs'.fd
             pkgs'.haskellPackages.cabal-fmt
             pkgs'.nixpkgs-fmt
-            (pkgs.haskell-nix.tools ghcVersion {
-              inherit (plutarch.tools) fourmolu;
-            }).fourmolu
+            fourmolu
+            hlint
           ];
         } ''
           export LC_CTYPE=C.UTF-8
diff --git a/src/Agora/AuthorityToken.hs b/src/Agora/AuthorityToken.hs
index e84c04d..64dcfc7 100644
--- a/src/Agora/AuthorityToken.hs
+++ b/src/Agora/AuthorityToken.hs
@@ -1,31 +1,39 @@
+{- |
+Module     : Agora.AuthorityToken
+Maintainer : emi@haskell.fyi
+Description: Tokens acting as redeemable proofs of DAO authority.
+
+Tokens acting as redeemable proofs of DAO authority.
+-}
 module Agora.AuthorityToken (
   authorityTokenPolicy,
   AuthorityToken (..),
 ) where
 
 import Plutarch.Api.V1 (
-  PCurrencySymbol,
-  PMap (..),
   PScriptContext (..),
   PScriptPurpose (..),
-  PTokenName,
   PTxInInfo (..),
   PTxInfo (..),
   PTxOut (..),
-  PValue (..),
  )
 import Plutarch.List (pfoldr')
-import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
+import Plutarch.Monadic qualified as P
+import Plutus.V1.Ledger.Value (AssetClass)
 
 import Prelude
 
 --------------------------------------------------------------------------------
 
+import Agora.Utils (passert, passetClassValueOf, passetClassValueOf')
+
+--------------------------------------------------------------------------------
+
 {- | An AuthorityToken represents a proof that a particular token
      moved while this token was minted. In effect, this means that
      the validator that locked such a token must have approved
      said transaction. Said validator should be made aware of
-     _this_ token's existence in order to prevent incorrect minting.
+     *this* token's existence in order to prevent incorrect minting.
 -}
 newtype AuthorityToken = AuthorityToken
   { authority :: AssetClass
@@ -34,94 +42,34 @@ newtype AuthorityToken = AuthorityToken
 
 --------------------------------------------------------------------------------
 
--- TODO: upstream something like this
-pfind' ::
-  PIsListLike list a =>
-  (Term s a -> Term s PBool) ->
-  Term s (list a :--> PMaybe a)
-pfind' p =
-  precList
-    (\self x xs -> pif (p x) (pcon (PJust x)) (self # xs))
-    (const $ pcon PNothing)
-
--- TODO: upstream something like this
-plookup ::
-  (PEq a, PIsListLike list (PBuiltinPair a b)) =>
-  Term s (a :--> list (PBuiltinPair a b) :--> PMaybe b)
-plookup =
-  phoistAcyclic $
-    plam $ \k xs ->
-      pmatch (pfind' (\p -> pfstBuiltin # p #== k) # xs) $ \case
-        PNothing -> pcon PNothing
-        PJust p -> pcon (PJust (psndBuiltin # p))
-
-passetClassValueOf' :: AssetClass -> Term s (PValue :--> PInteger)
-passetClassValueOf' (AssetClass (sym, token)) =
-  passetClassValueOf # pconstant sym # pconstant token
-
-passetClassValueOf ::
-  Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PInteger)
-passetClassValueOf =
-  phoistAcyclic $
-    plam $ \sym token value'' ->
-      pmatch value'' $ \(PValue value') ->
-        pmatch value' $ \(PMap value) ->
-          pmatch (plookup # pdata sym # value) $ \case
-            PNothing -> 0
-            PJust m' ->
-              pmatch (pfromData m') $ \(PMap m) ->
-                pmatch (plookup # pdata token # m) $ \case
-                  PNothing -> 0
-                  PJust v -> pfromData v
-
+-- | Policy given 'AuthorityToken' params.
 authorityTokenPolicy ::
   AuthorityToken ->
-  Term s (PData :--> PData :--> PScriptContext :--> PUnit)
+  Term s (PData :--> PScriptContext :--> PUnit)
 authorityTokenPolicy params =
-  plam $ \_datum _redeemer ctx' ->
-    pmatch ctx' $ \(PScriptContext ctx) ->
-      let txInfo' = pfromData $ pfield @"txInfo" # ctx
-          purpose' = pfromData $ pfield @"purpose" # ctx
-
-          inputs =
-            pmatch txInfo' $ \(PTxInfo txInfo) ->
-              pfromData $ pfield @"inputs" # txInfo
-
-          authorityTokenInputs =
-            pfoldr'
-              ( \txInInfo' acc ->
-                  pmatch (pfromData txInInfo') $ \(PTxInInfo txInInfo) ->
-                    let txOut' =
-                          pfromData $ pfield @"resolved" # txInInfo
-                        txOutValue =
-                          pmatch txOut' $
-                            \(PTxOut txOut) ->
-                              pfromData $ pfield @"value" # txOut
-                     in passetClassValueOf' params.authority # txOutValue + acc
+  plam $ \_redeemer ctx' ->
+    pmatch ctx' $ \(PScriptContext ctx') -> P.do
+      ctx <- pletFields @'["txInfo", "purpose"] ctx'
+      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 :: Term s PInteger)
+              # 0
               # inputs
-
-          -- We incur the cost twice here. This will be fixed upstream in Plutarch.
-          mintedValue =
-            pmatch txInfo' $ \(PTxInfo txInfo) ->
-              pfromData $ pfield @"mint" # txInfo
-
-          tokenMoved = 0 #< authorityTokenInputs
-       in pmatch purpose' $ \case
-            PMinting sym' ->
-              let sym = pfromData $ pfield @"_0" # sym'
-                  mintedATs = passetClassValueOf # sym # pconstant "" # mintedValue
-               in pif
-                    (0 #< mintedATs)
-                    ( pif
-                        tokenMoved
-                        -- The authority token moved, we are good to go for minting.
-                        (pconstant ())
-                        (ptraceError "Authority token did not move in minting GATs")
-                    )
-                    -- We minted 0 or less Authority Tokens, we are good to go.
-                    -- Burning is always allowed.
-                    (pconstant ())
-            _ ->
-              ptraceError "Wrong script type"
+      let mintedValue = pfromData txInfo.mint
+      let tokenMoved = 0 #< authorityTokenInputs
+      PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
+      let ownSymbol = pfromData $ pfield @"_0" # ownSymbol'
+      let mintedATs = passetClassValueOf # ownSymbol # pconstant "" # mintedValue
+      pif
+        (0 #< mintedATs)
+        (passert "Authority token did not move in minting GATs" tokenMoved (pconstant ()))
+        (pconstant ())
diff --git a/src/Agora/SafeMoney.hs b/src/Agora/SafeMoney.hs
new file mode 100644
index 0000000..f361e22
--- /dev/null
+++ b/src/Agora/SafeMoney.hs
@@ -0,0 +1,113 @@
+{- |
+Module     : Agora.SafeMoney
+Maintainer : emi@haskell.fyi
+Description: Phantom-type protected types for handling money in Plutus.
+
+Phantom-type protected types for handling money in Plutus.
+-}
+module Agora.SafeMoney (
+  -- * Types
+  MoneyClass,
+  PDiscrete,
+
+  -- * Utility functions
+  paddDiscrete,
+
+  -- * Conversions
+  pdiscreteValue,
+  pvalueDiscrete,
+
+  -- * Example MoneyClasses
+  LQ,
+  ADA,
+) where
+
+import Data.Proxy (Proxy (Proxy))
+import Data.String
+import GHC.TypeLits (
+  KnownSymbol,
+  Nat,
+  Symbol,
+  symbolVal,
+ )
+import Prelude
+
+--------------------------------------------------------------------------------
+
+import Plutarch.Api.V1 (PValue)
+import Plutarch.Builtin ()
+import Plutarch.Internal ()
+import Plutarch.Monadic qualified as P
+
+--------------------------------------------------------------------------------
+
+import Agora.Utils
+
+--------------------------------------------------------------------------------
+
+-- | Type-level unique identifier for an `AssetClass`
+type MoneyClass =
+  ( -- AssetClass
+    Symbol
+  , -- TokenName
+    Symbol
+  , -- Decimal places
+    Nat
+  )
+
+-- | A `PDiscrete` amount of currency tagged on the type level with the `MoneyClass` it belong sto
+newtype PDiscrete (mc :: MoneyClass) (s :: S)
+  = PDiscrete (Term s PInteger)
+  deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (PDiscrete mc) PInteger)
+
+-- | Add two `PDiscrete` values of the same `MoneyClass`.
+paddDiscrete :: Term s (PDiscrete mc :--> PDiscrete mc :--> PDiscrete mc)
+paddDiscrete = phoistAcyclic $
+  -- In the future, this should use plutarch-numeric
+  plam $ \x y -> P.do
+    PDiscrete x' <- pmatch x
+    PDiscrete y' <- pmatch y
+    pcon (PDiscrete $ x' + y')
+
+-- | The MoneyClass of LQ.
+type LQ :: MoneyClass
+type LQ = '("da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24", "LQ", 6)
+
+-- | The MoneyClass of ADA.
+type ADA :: MoneyClass
+type ADA = '("", "", 6)
+
+--------------------------------------------------------------------------------
+
+-- | Downcast a `PValue` to a `PDiscrete` unit.
+pvalueDiscrete ::
+  forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
+  ( KnownSymbol ac
+  , KnownSymbol n
+  , moneyClass ~ '(ac, n, scale)
+  ) =>
+  Term s (PValue :--> PDiscrete moneyClass)
+pvalueDiscrete = phoistAcyclic $
+  plam $ \f ->
+    pcon . PDiscrete $
+      passetClassValueOf # pconstant (fromString $ symbolVal $ Proxy @ac)
+        # pconstant (fromString $ symbolVal $ Proxy @n)
+        # f
+
+{- | Get a `PValue` from a `PDiscrete`.
+     __NOTE__: `pdiscreteValue` after `pvalueDiscrete` is loses information
+-}
+pdiscreteValue ::
+  forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
+  ( KnownSymbol ac
+  , KnownSymbol n
+  , moneyClass ~ '(ac, n, scale)
+  ) =>
+  Term s (PDiscrete moneyClass :--> PValue)
+pdiscreteValue = phoistAcyclic $
+  plam $ \f -> pmatch f $ \case
+    PDiscrete p ->
+      psingletonValue
+        # pconstant (fromString $ symbolVal $ Proxy @ac)
+        # pconstant (fromString $ symbolVal $ Proxy @n)
+        # p
diff --git a/src/Agora/SafeMoney/QQ.hs b/src/Agora/SafeMoney/QQ.hs
new file mode 100644
index 0000000..96ec4c7
--- /dev/null
+++ b/src/Agora/SafeMoney/QQ.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+{- |
+Module     : Agora.SafeMoney.QQ
+Maintainer : emi@haskell.fyi
+Description: Quasiquoter for SafeMoney types.
+
+Quasiquoter for SafeMoney types.
+-}
+module Agora.SafeMoney.QQ (discrete) where
+
+import GHC.Real (Ratio ((:%)))
+import Language.Haskell.TH qualified as TH (Type)
+import Language.Haskell.TH.Quote (QuasiQuoter (QuasiQuoter))
+import Language.Haskell.TH.Syntax (
+  Dec (TySynD),
+  Exp (AppE, AppTypeE, LitE, VarE),
+  Info (TyConI),
+  Lit (IntegerL),
+  Pat,
+  Q,
+  TyLit (NumTyLit, StrTyLit),
+  Type (AppT, ConT, LitT, PromotedTupleT),
+  lookupTypeName,
+  reify,
+ )
+import Text.ParserCombinators.ReadP (readP_to_S, skipSpaces)
+import Text.Read (lexP, readPrec_to_P)
+import Text.Read.Lex (Lexeme (Ident, Number), Number, numberToFixed, numberToRational)
+import Prelude
+
+--------------------------------------------------------------------------------
+
+import Plutarch.Internal (punsafeCoerce)
+
+import Agora.SafeMoney (MoneyClass, PDiscrete)
+
+--------------------------------------------------------------------------------
+
+{- | Generate 'PDiscrete' values tagged by a particular MoneyClass
+
+@
+  [discrete| 123.456 ADA |] :: 'Term' s ('PDiscrete' 'ADA')
+@
+-}
+discrete :: QuasiQuoter
+discrete = QuasiQuoter discreteExp errorDiscretePat errorDiscreteType errorDiscreteDiscretelaration
+
+discreteConstant :: forall (moneyClass :: MoneyClass) s. Integer -> Term s (PDiscrete moneyClass)
+discreteConstant n = punsafeCoerce (pconstant n :: Term s PInteger)
+
+fixedToInteger :: Integer -> (Integer, Integer) -> Integer
+fixedToInteger places (i, f) = i * 10 ^ places + f
+
+safeIntegerUpcast :: Integer -> Number -> Either String Integer
+safeIntegerUpcast places num =
+  case (numberToFixed places num, numberToRational num * 10 ^ places) of
+    (Just (i, f), _n :% 1) ->
+      Right $ fixedToInteger places (i, f)
+    (Just (i, f), _n :% _d) ->
+      Left $ "Using more than the available decimal places (" <> show places <> "). Would round to " <> show i <> "." <> show f
+    _ -> Left "Some error occurred while getting number"
+
+discreteExp :: String -> Q Exp
+discreteExp s = case parseDiscreteRatioExp s of
+  Nothing ->
+    fail $ "Input malformed. Got: " <> s
+  Just (num, mc) -> do
+    mcName <-
+      lookupTypeName mc >>= \case
+        Nothing -> fail $ "MoneyClass with the name " <> show mc <> " is not in scope."
+        Just v -> pure v
+    reified <- reify mcName
+    case reified of
+      TyConI (TySynD tyName [] (AppT (AppT (AppT (PromotedTupleT 3) (LitT (StrTyLit _))) (LitT _)) (LitT (NumTyLit n)))) ->
+        case safeIntegerUpcast n num of
+          Right i ->
+            pure $ AppE (AppTypeE (VarE 'discreteConstant) (ConT tyName)) (LitE (IntegerL i))
+          Left e -> fail e
+      ty' -> fail $ "Could not reify type, got: " <> show ty'
+
+parseDiscreteRatioExp :: String -> Maybe (Number, String)
+parseDiscreteRatioExp s =
+  let p = skipSpaces *> ((,) <$> readPrec_to_P lexP 0 <* skipSpaces <*> readPrec_to_P lexP 0) <* skipSpaces
+   in case readP_to_S p s of
+        [((Number n, Ident i), "")] -> Just (n, i)
+        _ -> Nothing
+
+errorDiscretePat :: String -> Q Pat
+errorDiscretePat _ = fail "Cannot use 'discrete' in a pattern context."
+
+errorDiscreteType :: String -> Q TH.Type
+errorDiscreteType _ = fail "Cannot use 'discrete' in a type context."
+
+errorDiscreteDiscretelaration :: String -> Q [Dec]
+errorDiscreteDiscretelaration _ = fail "Cannot use 'discrete' in a declaration context."
diff --git a/src/Agora/Stake.hs b/src/Agora/Stake.hs
new file mode 100644
index 0000000..a4dcc24
--- /dev/null
+++ b/src/Agora/Stake.hs
@@ -0,0 +1,261 @@
+{- |
+Module     : Agora.Stake
+Maintainer : emi@haskell.fyi
+Description: Vote-lockable stake UTXOs holding GT.
+
+Vote-lockable stake UTXOs holding GT.
+-}
+module Agora.Stake (
+  PStakeDatum (..),
+  PStakeAction (..),
+  Stake (..),
+  stakePolicy,
+  stakeValidator,
+  stakeLocked,
+) where
+
+--------------------------------------------------------------------------------
+
+import GHC.Generics qualified as GHC
+import GHC.TypeLits (
+  KnownSymbol,
+ )
+import Generics.SOP (Generic, I (I))
+import Prelude
+
+--------------------------------------------------------------------------------
+
+import Plutarch (popaque)
+import Plutarch.Api.V1 (
+  PCredential (PPubKeyCredential, PScriptCredential),
+  PMintingPolicy,
+  PPubKeyHash,
+  PScriptPurpose (PMinting, PSpending),
+  PValidator,
+  mintingPolicySymbol,
+  mkMintingPolicy,
+ )
+import Plutarch.DataRepr (
+  PDataFields,
+  PIsDataReprInstances (PIsDataReprInstances),
+ )
+import Plutarch.Internal (punsafeCoerce)
+import Plutarch.Monadic qualified as P
+
+--------------------------------------------------------------------------------
+
+import Agora.SafeMoney (
+  MoneyClass,
+  PDiscrete,
+  paddDiscrete,
+  pdiscreteValue,
+ )
+import Agora.Utils (
+  anyInput,
+  anyOutput,
+  paddValue,
+  passert,
+  pfindTxInByTxOutRef,
+  psingletonValue,
+  psymbolValueOf,
+  ptxSignedBy,
+  pvalueSpent,
+ )
+
+--------------------------------------------------------------------------------
+
+-- | Parameters for creating Stake scripts.
+data Stake (gt :: MoneyClass) = Stake
+
+-- | Plutarch-level redeemer for Stake scripts.
+data PStakeAction (gt :: MoneyClass) (s :: S)
+  = -- | Deposit or withdraw a discrete amount of the staked governance token.
+    PDepositWithdraw (Term s (PDataRecord '["delta" ':= PDiscrete gt]))
+  | -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
+    PDestroy (Term s (PDataRecord '[]))
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic)
+  deriving anyclass (PIsDataRepr)
+  deriving
+    (PlutusType, PIsData)
+    via PIsDataReprInstances (PStakeAction gt)
+
+-- | Plutarch-level datum for Stake scripts.
+newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum
+  { getStakeDatum ::
+    Term s (PDataRecord '["stakedAmount" ':= PDiscrete gt, "owner" ':= PPubKeyHash])
+  }
+  deriving stock (GHC.Generic)
+  deriving anyclass (Generic)
+  deriving anyclass (PIsDataRepr)
+  deriving
+    (PlutusType, PIsData, PDataFields)
+    via (PIsDataReprInstances (PStakeDatum gt))
+
+--------------------------------------------------------------------------------
+{- 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 ::
+  forall (gt :: MoneyClass) ac n scale s.
+  ( KnownSymbol ac
+  , KnownSymbol n
+  , gt ~ '(ac, n, scale)
+  ) =>
+  Stake gt ->
+  Term s 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 gt) # 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 gt) # 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'
+                    let stValue =
+                          psingletonValue
+                            # ownSymbol
+                            -- This coerce is safe because the structure
+                            -- of PValidatorHash is the same as PTokenName.
+                            # punsafeCoerce validatorHash._0
+                            # 1
+                    let expectedValue =
+                          paddValue
+                            # (pdiscreteValue # stakeDatum.stakedAmount)
+                            # stValue
+                    let ownerSignsTransaction =
+                          ptxSignedBy
+                            # ctx.txInfo
+                            # stakeDatum.owner
+
+                    -- TODO: Needs to be >=, rather than ==
+                    let valueCorrect = pdata value #== pdata expectedValue
+                    ownerSignsTransaction #&& valueCorrect
+
+          popaque (pconstant ())
+
+    pif (0 #< mintedST) minting burning
+
+--------------------------------------------------------------------------------
+
+-- | Validator intended for Stake UTXOs to live in.
+stakeValidator ::
+  forall (gt :: MoneyClass) ac n scale s.
+  ( KnownSymbol ac
+  , KnownSymbol n
+  , gt ~ '(ac, n, scale)
+  ) =>
+  Stake gt ->
+  Term s PValidator
+stakeValidator stake =
+  plam $ \datum redeemer ctx' -> P.do
+    ctx <- pletFields @'["txInfo", "purpose"] ctx'
+    txInfo' <- plet ctx.txInfo
+    txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
+
+    -- Coercion is safe in that if coercion fails we crash hard.
+    let stakeAction :: Term _ (PStakeAction gt)
+        stakeAction = pfromData $ punsafeCoerce redeemer
+        stakeDatum' :: Term _ (PStakeDatum gt)
+        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
+    stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake)
+    mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfo.mint
+    spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfo'
+
+    pmatch stakeAction $ \case
+      PDestroy _ -> P.do
+        passert "ST at inputs must be 1" $
+          spentST #== 1
+        passert "Should burn ST" $
+          mintedST #== -1
+        passert "Stake unlocked" $
+          pnot #$ stakeLocked # stakeDatum'
+        popaque (pconstant ())
+      PDepositWithdraw r -> P.do
+        passert "ST at inputs must be 1" $
+          spentST #== 1
+        passert "Stake unlocked" $
+          pnot #$ stakeLocked # stakeDatum'
+        passert "A UTXO must exist with the correct output" $
+          anyOutput @(PStakeDatum gt) # txInfo'
+            #$ plam
+            $ \value address newStakeDatum' -> P.do
+              newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum'
+              delta <- plet $ pfield @"delta" # r
+              let isScriptAddress = pdata address #== ownAddress
+              let correctOutputDatum =
+                    stakeDatum.owner #== newStakeDatum.owner
+                      #&& (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
+              let expectedValue = paddValue # continuingValue # (pdiscreteValue # delta)
+
+              -- TODO: As above, needs to be >=, rather than ==
+              let correctValue = pdata value #== pdata expectedValue
+              isScriptAddress #&& correctOutputDatum #&& correctValue
+
+        popaque (pconstant ())
+
+--------------------------------------------------------------------------------
+
+-- | Check whether a Stake is locked. If it is locked, various actions are unavailable.
+stakeLocked :: forall (gt :: MoneyClass) s. Term s (PStakeDatum gt :--> PBool)
+stakeLocked = phoistAcyclic $
+  plam $ \_stakeDatum ->
+    -- TODO: when we extend this to support proposals, this will need to do something
+    pcon PFalse
diff --git a/src/Agora/Utils.hs b/src/Agora/Utils.hs
new file mode 100644
index 0000000..124c57b
--- /dev/null
+++ b/src/Agora/Utils.hs
@@ -0,0 +1,314 @@
+{- |
+Module     : Agora.Utils
+Maintainer : emi@haskell.fyi
+Description: Plutarch utility functions that should be upstreamed or don't belong anywhere else.
+
+Plutarch utility functions that should be upstreamed or don't belong anywhere else.
+-}
+module Agora.Utils (
+  -- * Validator-level utility functions
+  passert,
+  pfind',
+  pfindDatum,
+  pfindDatum',
+  pvalueSpent,
+  ptxSignedBy,
+  paddValue,
+  plookup,
+  pfromMaybe,
+  psymbolValueOf,
+  passetClassValueOf,
+  passetClassValueOf',
+  pfindTxInByTxOutRef,
+  psingletonValue,
+  pfindMap,
+
+  -- * Functions which should (probably) not be upstreamed
+  anyOutput,
+  anyInput,
+) where
+
+--------------------------------------------------------------------------------
+
+import Plutus.V1.Ledger.Value (AssetClass (..))
+
+--------------------------------------------------------------------------------
+
+import Plutarch.Api.V1 (
+  PAddress,
+  PCurrencySymbol,
+  PDatum,
+  PDatumHash,
+  PMap (PMap),
+  PMaybeData (PDJust),
+  PPubKeyHash,
+  PTokenName,
+  PTuple,
+  PTxInInfo (PTxInInfo),
+  PTxInfo (PTxInfo),
+  PTxOut (PTxOut),
+  PTxOutRef,
+  PValue (PValue),
+ )
+import Plutarch.Builtin (ppairDataBuiltin)
+import Plutarch.Internal (punsafeCoerce)
+import Plutarch.Monadic qualified as P
+
+--------------------------------------------------------------------------------
+-- Validator-level utility functions
+
+-- | Assert a particular 'PBool', trace if false. Use in monadic context.
+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 = phoistAcyclic $
+  plam $ \datumHash txInfo'' -> P.do
+    PTxInfo txInfo' <- pmatch txInfo''
+    plookupTuple # datumHash #$ pfield @"data" # txInfo'
+
+{- | 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
+
+-- | Check if a PubKeyHash signs this transaction.
+ptxSignedBy :: Term s (PTxInfo :--> PAsData PPubKeyHash :--> PBool)
+ptxSignedBy = phoistAcyclic $
+  plam $ \txInfo' pkh -> P.do
+    txInfo <- pletFields @'["signatories"] txInfo'
+    pelem @PBuiltinList # pkh # txInfo.signatories
+
+-- | Get the first element that matches a predicate or return Nothing.
+pfind' ::
+  PIsListLike list a =>
+  (Term s a -> Term s PBool) ->
+  Term s (list a :--> PMaybe a)
+pfind' p =
+  precList
+    (\self x xs -> pif (p x) (pcon (PJust x)) (self # xs))
+    (const $ pcon PNothing)
+
+-- | Get the first element that maps to a PJust in a list.
+pfindMap ::
+  PIsListLike list a =>
+  Term s ((a :--> PMaybe b) :--> list a :--> PMaybe b)
+pfindMap =
+  phoistAcyclic $
+    plam $ \p ->
+      precList
+        ( \self x xs ->
+            -- In the future, this should use `pmatchSum`, I believe?
+            pmatch (p # x) $ \case
+              PNothing -> self # xs
+              PJust v -> pcon (PJust v)
+        )
+        (const $ pcon PNothing)
+
+-- | Find the value for a given key in an associative list.
+plookup ::
+  (PEq a, PIsListLike list (PBuiltinPair a b)) =>
+  Term s (a :--> list (PBuiltinPair a b) :--> PMaybe b)
+plookup =
+  phoistAcyclic $
+    plam $ \k xs ->
+      pmatch (pfind' (\p -> pfstBuiltin # p #== k) # xs) $ \case
+        PNothing -> pcon PNothing
+        PJust p -> pcon (PJust (psndBuiltin # p))
+
+-- | Find the value for a given key in an assoclist which uses 'PTuple's.
+plookupTuple ::
+  (PEq a, PIsListLike list (PAsData (PTuple a b)), PIsData a, PIsData b) =>
+  Term s (a :--> list (PAsData (PTuple a b)) :--> PMaybe b)
+plookupTuple =
+  phoistAcyclic $
+    plam $ \k xs ->
+      pmatch (pfind' (\p -> (pfield @"_0" # pfromData p) #== k) # xs) $ \case
+        PNothing -> pcon PNothing
+        PJust p -> pcon (PJust (pfield @"_1" # pfromData p))
+
+-- | Extract a Maybe by providing a default value in case of Just.
+pfromMaybe :: forall a s. Term s (a :--> PMaybe a :--> a)
+pfromMaybe = phoistAcyclic $
+  plam $ \e a ->
+    pmatch a $ \case
+      PJust a' -> a'
+      PNothing -> e
+
+-- | Escape with a particular value on expecting 'Just'. For use in monadic context.
+pexpectJust ::
+  forall r a s.
+  Term s r ->
+  Term s (PMaybe a) ->
+  (Term s a -> Term s r) ->
+  Term s r
+pexpectJust escape ma f =
+  pmatch ma $ \case
+    PJust v -> f v
+    PNothing -> escape
+
+-- | Get the sum of all values belonging to a particular CurrencySymbol.
+psymbolValueOf :: Term s (PCurrencySymbol :--> PValue :--> PInteger)
+psymbolValueOf =
+  phoistAcyclic $
+    plam $ \sym value'' -> P.do
+      PValue value' <- pmatch value''
+      PMap value <- pmatch value'
+      m' <- pexpectJust 0 (plookup # pdata sym # value)
+      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
+
+-- | Union two maps using a merge function on collisions.
+pmapUnionWith :: forall k v s. PIsData v => Term s ((v :--> v :--> v) :--> PMap k v :--> PMap k v :--> PMap k v)
+pmapUnionWith = phoistAcyclic $
+  -- TODO: this function is kinda suspect. I feel like a lot of optimizations could be done here
+  plam $ \f xs' ys' -> P.do
+    PMap xs <- pmatch xs'
+    PMap ys <- pmatch ys'
+    let ls =
+          pmap
+            # plam
+              ( \p -> P.do
+                  pf <- plet $ pfstBuiltin # p
+                  ps <- plet $ psndBuiltin # p
+                  pmatch (plookup # pf # ys) $ \case
+                    PJust v ->
+                      -- Data conversions here are silly, aren't they?
+                      ppairDataBuiltin # pf # pdata (f # pfromData ps # pfromData v)
+                    PNothing -> p
+              )
+            # xs
+        rs =
+          pfilter
+            # plam
+              ( \p ->
+                  pnot #$ pany # plam (\p' -> pfstBuiltin # p' #== pfstBuiltin # p) # xs
+              )
+            # ys
+    pcon (PMap $ pconcat # ls # rs)
+
+-- | Add two 'PValue's together
+paddValue :: forall s. Term s (PValue :--> PValue :--> PValue)
+paddValue = phoistAcyclic $
+  plam $ \a' b' -> P.do
+    PValue a <- pmatch a'
+    PValue b <- pmatch b'
+    pcon
+      ( PValue $
+          pmapUnionWith # plam (\a' b' -> pmapUnionWith # plam (+) # a' # b') # a # b
+      )
+
+-- | Sum of all value at input.
+pvalueSpent :: Term s (PTxInfo :--> 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)
+
+-- | Find the TxInInfo by a TxOutRef.
+pfindTxInByTxOutRef :: Term s (PTxOutRef :--> PTxInfo :--> 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)
+
+--------------------------------------------------------------------------------
+-- Functions which should (probably) not be upstreamed
+
+-- | Check if any output matches the predicate.
+anyOutput ::
+  forall (datum :: PType) s.
+  ( PIsData datum
+  ) =>
+  Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
+anyOutput = phoistAcyclic $
+  plam $ \txInfo' predicate -> P.do
+    txInfo <- pletFields @'["outputs"] 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
+              PJust datum -> P.do
+                predicate # txOut.value # txOut.address # pfromData datum
+              PNothing -> pcon PFalse
+        )
+      # pfromData txInfo.outputs
+
+-- | Check if any (resolved) input matches the predicate.
+anyInput ::
+  forall (datum :: PType) s.
+  ( PIsData datum
+  ) =>
+  Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
+anyInput = phoistAcyclic $
+  plam $ \txInfo' predicate -> P.do
+    txInfo <- pletFields @'["inputs"] txInfo'
+    pany
+      # plam
+        ( \txInInfo'' -> P.do
+            PTxInInfo txInInfo' <- pmatch (pfromData txInInfo'')
+            let txOut'' = pfield @"resolved" # txInInfo'
+            PTxOut txOut' <- pmatch (pfromData txOut'')
+            txOut <- pletFields @'["value", "datumHash", "address"] txOut'
+            PDJust dh <- pmatch txOut.datumHash
+            pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case
+              PJust datum -> P.do
+                predicate # txOut.value # txOut.address # pfromData datum
+              PNothing -> pcon PFalse
+        )
+      # pfromData txInfo.inputs
+
+-- | Create a value with a single asset class.
+psingletonValue :: forall s. Term s (PCurrencySymbol :--> PTokenName :--> PInteger :--> PValue)
+psingletonValue = phoistAcyclic $
+  plam $ \sym tok int ->
+    let innerTup = pcon $ PMap $ psingleton #$ ppairDataBuiltin # pdata tok # pdata int
+        outerTup = pcon $ PMap $ psingleton #$ ppairDataBuiltin # pdata sym # pdata innerTup
+        res = pcon $ PValue outerTup
+     in res
diff --git a/src/Agora/Voting.hs b/src/Agora/Voting.hs
new file mode 100644
index 0000000..5436960
--- /dev/null
+++ b/src/Agora/Voting.hs
@@ -0,0 +1,11 @@
+{- |
+Module     : Agora.Voting
+Maintainer : emi@haskell.fyi
+Description: Types for votes and vote counting
+-}
+module Agora.Voting (
+  Vote (..),
+) where
+
+-- | Type representing direction of vote.
+data Vote = InFavorOf | OpposedTo