Merge pull request #84 from Liqwid-Labs/connor/proposal-voting

Voting on Proposals

agora-sample/Sample/Governor.hs

@@ -73,12 +73,14 @@ import Sample.Shared (
   gstUTXORef,
   minAda,
   proposalPolicySymbol,
+  proposalTimingConfig,
   proposalValidatorAddress,
   signer,
   signer2,
   stake,
   stakeAddress,
   stakeAssetClass,
+  tmpProposalStartingTime,
  )
 import Test.Util (datumPair, toDatumHash)
 
@@ -234,6 +236,8 @@ createProposal =
                 , cosigners = [signer]
                 , thresholds = defaultProposalThresholds
                 , votes = emptyVotesFor effects
+                , timingConfig = proposalTimingConfig
+                , startingTime = tmpProposalStartingTime
                 }
           )
       proposalOutput :: TxOut
@@ -408,6 +412,8 @@ mintGATs =
           , cosigners = [signer, signer2]
           , thresholds = defaultProposalThresholds
           , votes = proposalVotes
+          , timingConfig = proposalTimingConfig
+          , startingTime = tmpProposalStartingTime
           }
       proposalInputDatum :: Datum
       proposalInputDatum = Datum $ toBuiltinData proposalInputDatum'

agora-sample/Sample/Proposal.hs

@@ -11,6 +11,8 @@ module Sample.Proposal (
   cosignProposal,
   proposalRef,
   stakeRef,
+  voteOnProposal,
+  VotingParameters (..),
 ) where
 
 --------------------------------------------------------------------------------
@@ -21,6 +23,7 @@ import Plutus.V1.Ledger.Api (
   Address (Address),
   Credential (ScriptCredential),
   Datum (Datum),
+  POSIXTimeRange,
   PubKeyHash,
   ScriptContext (..),
   ScriptPurpose (..),
@@ -43,14 +46,16 @@ import Agora.Proposal (
   ProposalDatum (..),
   ProposalId (..),
   ProposalStatus (..),
+  ProposalVotes (..),
   ResultTag (..),
   emptyVotesFor,
  )
-import Agora.Stake (Stake (..), StakeDatum (StakeDatum))
+import Agora.Proposal.Time (ProposalTimingConfig (..))
+import Agora.Stake (ProposalLock (ProposalLock), Stake (..), StakeDatum (..))
 import Plutarch.SafeMoney (Tagged (Tagged), untag)
 import PlutusTx.AssocMap qualified as AssocMap
 import Sample.Shared
-import Test.Util (datumPair, toDatumHash)
+import Test.Util (closedBoundedInterval, datumPair, toDatumHash, updateMap)
 
 --------------------------------------------------------------------------------
 
@@ -74,6 +79,8 @@ proposalCreation =
                 , cosigners = [signer]
                 , thresholds = defaultProposalThresholds
                 , votes = emptyVotesFor effects
+                , timingConfig = proposalTimingConfig
+                , startingTime = tmpProposalStartingTime
                 }
           )
 
@@ -167,11 +174,18 @@ cosignProposal newSigners =
           , cosigners = [signer]
           , thresholds = defaultProposalThresholds
           , votes = emptyVotesFor effects
+          , timingConfig = proposalTimingConfig
+          , startingTime = tmpProposalStartingTime
           }
       stakeDatum :: StakeDatum
       stakeDatum = StakeDatum (Tagged 50_000_000) signer2 []
       proposalAfter :: ProposalDatum
       proposalAfter = proposalBefore {cosigners = newSigners <> proposalBefore.cosigners}
+      validTimeRange :: POSIXTimeRange
+      validTimeRange =
+        closedBoundedInterval
+          10
+          (proposalTimingConfig.draftTime - 10)
    in TxInfo
         { txInfoInputs =
             [ TxInInfo
@@ -223,7 +237,7 @@ cosignProposal newSigners =
         , txInfoMint = st
         , txInfoDCert = []
         , txInfoWdrl = []
-        , txInfoValidRange = Interval.always
+        , txInfoValidRange = validTimeRange
         , txInfoSignatories = newSigners
         , txInfoData =
             [ datumPair . Datum $ toBuiltinData proposalBefore
@@ -232,3 +246,157 @@ cosignProposal newSigners =
             ]
         , txInfoId = "0b2086cbf8b6900f8cb65e012de4516cb66b5cb08a9aaba12a8b88be"
         }
+
+--------------------------------------------------------------------------------
+
+-- | Parameters for creating a voting transaction.
+data VotingParameters = VotingParameters
+  { voteFor :: ResultTag
+  -- ^ The outcome the transaction is voting for.
+  , voteCount :: Integer
+  -- ^ The count of votes.
+  }
+
+-- | Create a valid transaction that votes on a propsal, given the parameters.
+voteOnProposal :: VotingParameters -> TxInfo
+voteOnProposal params =
+  let pst = Value.singleton proposalPolicySymbol "" 1
+      sst = Value.assetClassValue stakeAssetClass 1
+
+      ---
+
+      stakeOwner = signer
+
+      ---
+
+      effects =
+        AssocMap.fromList
+          [ (ResultTag 0, AssocMap.empty)
+          , (ResultTag 1, AssocMap.empty)
+          ]
+
+      ---
+
+      initialVotes :: AssocMap.Map ResultTag Integer
+      initialVotes =
+        AssocMap.fromList
+          [ (ResultTag 0, 42)
+          , (ResultTag 1, 4242)
+          ]
+
+      ---
+
+      proposalInputDatum' :: ProposalDatum
+      proposalInputDatum' =
+        ProposalDatum
+          { proposalId = ProposalId 42
+          , effects = effects
+          , status = VotingReady
+          , cosigners = [stakeOwner]
+          , thresholds = defaultProposalThresholds
+          , votes = ProposalVotes initialVotes
+          , timingConfig = proposalTimingConfig
+          , startingTime = tmpProposalStartingTime
+          }
+      proposalInputDatum :: Datum
+      proposalInputDatum = Datum $ toBuiltinData proposalInputDatum'
+      proposalInput :: TxOut
+      proposalInput =
+        TxOut
+          { txOutAddress = proposalValidatorAddress
+          , txOutValue = pst
+          , txOutDatumHash = Just $ toDatumHash proposalInputDatum
+          }
+
+      ---
+
+      existingLocks :: [ProposalLock]
+      existingLocks =
+        [ ProposalLock (ResultTag 0) (ProposalId 0)
+        , ProposalLock (ResultTag 2) (ProposalId 1)
+        ]
+
+      ---
+
+      stakeInputDatum' :: StakeDatum
+      stakeInputDatum' =
+        StakeDatum
+          { stakedAmount = Tagged params.voteCount
+          , owner = stakeOwner
+          , lockedBy = existingLocks
+          }
+      stakeInputDatum :: Datum
+      stakeInputDatum = Datum $ toBuiltinData stakeInputDatum'
+      stakeInput :: TxOut
+      stakeInput =
+        TxOut
+          { txOutAddress = stakeAddress
+          , txOutValue =
+              mconcat
+                [ sst
+                , Value.assetClassValue (untag stake.gtClassRef) params.voteCount
+                , minAda
+                ]
+          , txOutDatumHash = Just $ toDatumHash stakeInputDatum
+          }
+
+      ---
+
+      updatedVotes :: AssocMap.Map ResultTag Integer
+      updatedVotes = updateMap (Just . (+ params.voteCount)) params.voteFor initialVotes
+
+      ---
+
+      proposalOutputDatum' :: ProposalDatum
+      proposalOutputDatum' =
+        proposalInputDatum'
+          { votes = ProposalVotes updatedVotes
+          }
+      proposalOutputDatum :: Datum
+      proposalOutputDatum = Datum $ toBuiltinData proposalOutputDatum'
+      proposalOutput :: TxOut
+      proposalOutput =
+        proposalInput
+          { txOutDatumHash = Just $ toDatumHash proposalOutputDatum
+          }
+
+      ---
+
+      -- Off-chain code should do exactly like this: prepend new lock to the list.
+      updatedLocks :: [ProposalLock]
+      updatedLocks = ProposalLock params.voteFor proposalInputDatum'.proposalId : existingLocks
+
+      ---
+
+      stakeOutputDatum' :: StakeDatum
+      stakeOutputDatum' =
+        stakeInputDatum'
+          { lockedBy = updatedLocks
+          }
+      stakeOutputDatum :: Datum
+      stakeOutputDatum = Datum $ toBuiltinData stakeOutputDatum'
+      stakeOutput :: TxOut
+      stakeOutput =
+        stakeInput
+          { txOutDatumHash = Just $ toDatumHash stakeOutputDatum
+          }
+
+      ---
+
+      validTimeRange =
+        closedBoundedInterval (proposalTimingConfig.draftTime + 1) (proposalTimingConfig.votingTime - 1)
+   in TxInfo
+        { txInfoInputs =
+            [ TxInInfo proposalRef proposalInput
+            , TxInInfo stakeRef stakeInput
+            ]
+        , txInfoOutputs = [proposalOutput, stakeOutput]
+        , txInfoFee = Value.singleton "" "" 2
+        , txInfoMint = mempty
+        , txInfoDCert = []
+        , txInfoWdrl = []
+        , txInfoValidRange = validTimeRange
+        , txInfoSignatories = [stakeOwner]
+        , txInfoData = datumPair <$> [proposalInputDatum, proposalOutputDatum, stakeInputDatum, stakeOutputDatum]
+        , txInfoId = "827598fb2d69a896bbd9e645bb14c307df907f422b39eecbe4d6329bc30b428c"
+        }

agora-sample/Sample/Shared.hs

@@ -36,6 +36,8 @@ module Sample.Shared (
   proposalPolicySymbol,
   proposalValidatorHash,
   proposalValidatorAddress,
+  proposalTimingConfig,
+  tmpProposalStartingTime,
 
   -- ** Authority
   authorityToken,
@@ -74,6 +76,10 @@ import Agora.Proposal (
   Proposal (..),
   ProposalThresholds (..),
  )
+import Agora.Proposal.Time (
+  ProposalStartingTime (..),
+  ProposalTimingConfig (..),
+ )
 import Agora.Stake (Stake (..))
 import Agora.Treasury (treasuryValidator)
 import Agora.Utils (validatorHashToTokenName)
@@ -184,6 +190,22 @@ authorityToken = authorityTokenFromGovernor governor
 authorityTokenSymbol :: CurrencySymbol
 authorityTokenSymbol = authorityTokenSymbolFromGovernor governor
 
+proposalTimingConfig :: ProposalTimingConfig
+proposalTimingConfig =
+  ProposalTimingConfig
+    { draftTime = 50
+    , votingTime = 1000
+    , lockingTime = 2000
+    , executingTime = 3000
+    }
+
+{- | Hard coded starting time of every propoal.
+    This will be calculated by the governor in the future.
+    FIXME: Remove this.
+-}
+tmpProposalStartingTime :: ProposalStartingTime
+tmpProposalStartingTime = ProposalStartingTime 0
+
 ------------------------------------------------------------------
 
 treasuryOut :: TxOut

agora-test/Spec/Proposal.hs

@@ -13,10 +13,11 @@ module Spec.Proposal (tests) where
 
 import Agora.Proposal (
   Proposal (..),
-  ProposalDatum (ProposalDatum),
+  ProposalDatum (..),
   ProposalId (ProposalId),
-  ProposalRedeemer (Cosign),
+  ProposalRedeemer (Cosign, Vote),
-  ProposalStatus (Draft),
+  ProposalStatus (Draft, VotingReady),
+  ProposalVotes (ProposalVotes),
   ResultTag (ResultTag),
   cosigners,
   effects,
@@ -30,7 +31,11 @@ import Agora.Proposal.Scripts (
   proposalPolicy,
   proposalValidator,
  )
-import Agora.Stake (StakeDatum (StakeDatum), StakeRedeemer (WitnessStake))
+import Agora.Stake (
+  ProposalLock (ProposalLock),
+  StakeDatum (StakeDatum),
+  StakeRedeemer (PermitVote, WitnessStake),
+ )
 import Agora.Stake.Scripts (stakeValidator)
 import Plutarch.SafeMoney (Tagged (Tagged))
 import Plutus.V1.Ledger.Api (ScriptContext (..), ScriptPurpose (..))
@@ -77,6 +82,8 @@ tests =
                           [ (ResultTag 0, AssocMap.empty)
                           , (ResultTag 1, AssocMap.empty)
                           ]
+                  , timingConfig = Shared.proposalTimingConfig
+                  , startingTime = Shared.tmpProposalStartingTime
                   }
               )
               (Cosign [signer2])
@@ -88,5 +95,62 @@ tests =
               WitnessStake
               (ScriptContext (Proposal.cosignProposal [signer2]) (Spending Proposal.stakeRef))
           ]
+      , testGroup
+          "voting"
+          [ validatorSucceedsWith
+              "proposal"
+              (proposalValidator Shared.proposal)
+              ( ProposalDatum
+                  { proposalId = ProposalId 42
+                  , effects =
+                      AssocMap.fromList
+                        [ (ResultTag 0, AssocMap.empty)
+                        , (ResultTag 1, AssocMap.empty)
+                        ]
+                  , status = VotingReady
+                  , cosigners = [signer]
+                  , thresholds = Shared.defaultProposalThresholds
+                  , votes =
+                      ProposalVotes
+                        ( AssocMap.fromList
+                            [ (ResultTag 0, 42)
+                            , (ResultTag 1, 4242)
+                            ]
+                        )
+                  , timingConfig = Shared.proposalTimingConfig
+                  , startingTime = Shared.tmpProposalStartingTime
+                  }
+              )
+              (Vote (ResultTag 0))
+              ( ScriptContext
+                  ( Proposal.voteOnProposal
+                      Proposal.VotingParameters
+                        { Proposal.voteFor = ResultTag 0
+                        , Proposal.voteCount = 27
+                        }
+                  )
+                  (Spending Proposal.proposalRef)
+              )
+          , validatorSucceedsWith
+              "stake"
+              (stakeValidator Shared.stake)
+              ( StakeDatum
+                  (Tagged 27)
+                  signer
+                  [ ProposalLock (ResultTag 0) (ProposalId 0)
+                  , ProposalLock (ResultTag 2) (ProposalId 1)
+                  ]
+              )
+              (PermitVote $ ProposalLock (ResultTag 0) (ProposalId 42))
+              ( ScriptContext
+                  ( Proposal.voteOnProposal
+                      Proposal.VotingParameters
+                        { Proposal.voteFor = ResultTag 0
+                        , Proposal.voteCount = 27
+                        }
+                  )
+                  (Spending Proposal.stakeRef)
+              )
+          ]
       ]
   ]

agora-test/Spec/Utils.hs

@@ -9,17 +9,33 @@ module Spec.Utils (tests) where
 
 --------------------------------------------------------------------------------
 
-import Agora.Utils (phalve, pisUniq, pmergeBy, pmsort, pnubSort)
+import Agora.Utils (phalve, pisUniq, pmergeBy, pmsort, pnubSort, pupdate)
 
 --------------------------------------------------------------------------------
 
 import Data.List (nub, sort)
-import Data.Set as S
+import Data.Map qualified as M
+import Data.Set qualified as S
 
 --------------------------------------------------------------------------------
 
+import Control.Monad.Cont (cont, runCont)
 import Test.Tasty (TestTree)
-import Test.Tasty.QuickCheck (testProperty)
+import Test.Tasty.QuickCheck (
+  Arbitrary (arbitrary),
+  Property,
+  Testable (property),
+  elements,
+  forAll,
+  suchThat,
+  testProperty,
+  (.&&.),
+ )
+import Test.Util (updateMap)
+
+--------------------------------------------------------------------------------
+
+import PlutusTx.AssocMap qualified as AssocMap
 
 --------------------------------------------------------------------------------
 
@@ -30,6 +46,7 @@ tests =
   , testProperty "'phalve' splits a list in half as expected" prop_halveCorrect
   , testProperty "'pnubSort' sorts a list and remove duplicate elements" prop_nubSortProperly
   , testProperty "'pisUniq' can tell whether all elements in a list are unique" prop_uniqueList
+  , testProperty "'pupdate' updates assoc maps as 'updateMap' does" prop_updateAssocMapParity
   ]
 
 --------------------------------------------------------------------------------
@@ -142,3 +159,68 @@ prop_uniqueList l = isUnique == expected
     --
 
     isUnique = plift $ pisUniq # pconstant l
+
+{- | Test the parity between 'updateMap' and 'pupdate',
+     also ensure they both work correctly.
+-}
+prop_updateAssocMapParity :: Property
+prop_updateAssocMapParity =
+  runCont
+    ( do
+        -- Generate a bunch unique keys.
+        keys <-
+          cont $
+            forAll $
+              arbitrary @(S.Set Integer) `suchThat` (not . S.null)
+
+        -- Generate key-value pairs.
+        kvPairs <- cont $ forAll $ mapM (\k -> (k,) <$> (arbitrary @Integer)) $ S.toList keys
+
+        let initialMap = AssocMap.fromList kvPairs
+
+            pinitialMap :: Term _ _
+            pinitialMap = phoistAcyclic $ pconstant initialMap
+
+            referenceMap = M.fromList kvPairs
+
+        let pupdatedValue :: Maybe Integer -> Term _ (PMaybe PInteger)
+            pupdatedValue updatedValue = phoistAcyclic $ case updatedValue of
+              Nothing -> pcon PNothing
+              Just v -> pcon $ PJust $ pconstant v
+
+            -- Given the key and the updated value, test the parity
+            parity key updatedValue =
+              let native = updateMap (const updatedValue) key initialMap
+
+                  plutarch :: AssocMap.Map Integer Integer
+                  plutarch =
+                    plift $
+                      pupdate
+                        # plam (\_ -> pupdatedValue updatedValue)
+                        # pconstant key
+                        # pinitialMap
+
+                  expected =
+                    AssocMap.fromList $
+                      M.toList $
+                        M.update (const updatedValue) key referenceMap
+               in expected == native
+                    && expected == plutarch
+
+        -- Select a key, generate a maybe value.
+        -- The value at the key should be set to the new value or removed.
+        (targetKey, _) <- cont $ forAll $ elements kvPairs
+        updatedValue <- cont $ forAll $ arbitrary @(Maybe Integer)
+
+        -- Now what if the key doesn't exist in our map?
+        nonexistentKey <-
+          cont $
+            forAll $
+              arbitrary @Integer `suchThat` (\k -> not $ S.member k keys)
+
+        pure
+          ( property (parity targetKey updatedValue)
+              .&&. property (parity nonexistentKey updatedValue)
+          )
+    )
+    id

agora-testlib/Test/Util.hs

@@ -38,6 +38,8 @@ module Test.Util (
   toDatum,
   toDatumHash,
   datumPair,
+  closedBoundedInterval,
+  updateMap,
 ) where
 
 --------------------------------------------------------------------------------
@@ -62,9 +64,12 @@ import Plutarch.Crypto (pblake2b_256)
 import Plutarch.Evaluate (evalScript)
 import Plutarch.Lift (PUnsafeLiftDecl (PLifted))
 import Plutus.V1.Ledger.Contexts (ScriptContext)
+import Plutus.V1.Ledger.Interval as PlutusTx
 import Plutus.V1.Ledger.Scripts (Datum (Datum), DatumHash (DatumHash), Script)
+import PlutusTx.AssocMap qualified as AssocMap
 import PlutusTx.Builtins qualified as PlutusTx
 import PlutusTx.IsData qualified as PlutusTx
+import PlutusTx.Ord qualified as PlutusTx
 
 --------------------------------------------------------------------------------
 
@@ -231,3 +236,24 @@ toDatumHash datum =
       plift $
         pblake2b_256
           # pconstant (ByteString.Lazy.toStrict $ serialise $ PlutusTx.toData datum)
+
+--------------------------------------------------------------------------------
+
+-- | Create a closed bounded `Interval`.
+closedBoundedInterval :: PlutusTx.Ord a => a -> a -> PlutusTx.Interval a
+closedBoundedInterval from to = PlutusTx.intersection (PlutusTx.from from) (PlutusTx.to to)
+
+--------------------------------------------------------------------------------
+
+{- | / O(n) /. The expression @'updateMap' f k v@ will update the value @x@ at key @k@.
+    If @f x@ is Nothing, the key-value pair will be deleted from the map, otherwise the
+     value will be updated.
+-}
+updateMap :: Eq k => (v -> Maybe v) -> k -> AssocMap.Map k v -> AssocMap.Map k v
+updateMap f k =
+  AssocMap.mapMaybeWithKey
+    ( \k' v ->
+        if k' == k
+          then f v
+          else Just v
+    )

agora.cabal

@@ -114,6 +114,7 @@ common test-deps
     , agora
     , apropos
     , apropos-tx
+    , mtl
     , QuickCheck
     , quickcheck-instances
     , tasty

agora/Agora/Governor/Scripts.hs

@@ -126,6 +126,7 @@ import Plutarch.TryFrom (ptryFrom)
 
 --------------------------------------------------------------------------------
 
+import Agora.Proposal.Time (ProposalStartingTime (..), ProposalTimingConfig (..))
 import Plutus.V1.Ledger.Api (
   CurrencySymbol (..),
   MintingPolicy,
@@ -576,6 +577,10 @@ governorValidator gov =
                       .& #cosigners .= proposalInputDatumF.cosigners
                       .& #thresholds .= proposalInputDatumF.thresholds
                       .& #votes .= proposalInputDatumF.votes
+                      -- FIXME: copy from the governor datum
+                      .& #timingConfig .= pdata (pconstant tmpTimingConfig)
+                      -- FIXME: calculate from 'txInfoValidRange'
+                      .& #startingTime .= pdata (pconstant tmpProposalStartingTime)
                   )
 
           tcassert "Unexpected output proposal datum" $
@@ -727,6 +732,20 @@ governorValidator gov =
       let sym = governorSTSymbolFromGovernor gov
        in phoistAcyclic $ pconstant sym
 
+    -- TODO: remove this. This is temperary.
+    tmpTimingConfig :: ProposalTimingConfig
+    tmpTimingConfig =
+      ProposalTimingConfig
+        { draftTime = 50
+        , votingTime = 1000
+        , lockingTime = 2000
+        , executingTime = 3000
+        }
+
+    -- TODO: remove this.
+    tmpProposalStartingTime :: ProposalStartingTime
+    tmpProposalStartingTime = ProposalStartingTime 0
+
 --------------------------------------------------------------------------------
 
 -- | Get the 'CurrencySymbol' of GST.

agora/Agora/Proposal.hs

@@ -44,6 +44,8 @@ import PlutusTx qualified
 import PlutusTx.AssocMap qualified as AssocMap
 
 --------------------------------------------------------------------------------
+
+import Agora.Proposal.Time (PProposalStartingTime, PProposalTimingConfig, ProposalStartingTime, ProposalTimingConfig)
 import Agora.SafeMoney (GTTag)
 import Agora.Utils (pkeysEqual, pnotNull)
 import Control.Applicative (Const)
@@ -186,6 +188,10 @@ data ProposalDatum = ProposalDatum
   -- ^ Thresholds copied over on initialization.
   , votes :: ProposalVotes
   -- ^ Vote tally on the proposal
+  , timingConfig :: ProposalTimingConfig
+  -- ^ Timing configuration copied over on initialization.
+  , startingTime :: ProposalStartingTime
+  -- ^ The time upon the creation of the proposal.
   }
   deriving stock (Eq, Show, GHC.Generic)
 
@@ -303,7 +309,7 @@ data PProposalStatus (s :: S)
   deriving anyclass (Generic)
   deriving anyclass (PIsDataRepr)
   deriving
-    (PlutusType, PIsData)
+    (PlutusType, PIsData, PEq)
     via PIsDataReprInstances PProposalStatus
 
 instance PUnsafeLiftDecl PProposalStatus where type PLifted PProposalStatus = ProposalStatus
@@ -354,6 +360,8 @@ newtype PProposalDatum (s :: S) = PProposalDatum
            , "cosigners" ':= PBuiltinList (PAsData PPubKeyHash)
            , "thresholds" ':= PProposalThresholds
            , "votes" ':= PProposalVotes
+           , "timingConfig" ':= PProposalTimingConfig
+           , "startingTime" ':= PProposalStartingTime
            ]
       )
   }
@@ -361,7 +369,7 @@ newtype PProposalDatum (s :: S) = PProposalDatum
   deriving anyclass (Generic)
   deriving anyclass (PIsDataRepr)
   deriving
-    (PlutusType, PIsData, PDataFields)
+    (PlutusType, PIsData, PDataFields, PEq)
     via (PIsDataReprInstances PProposalDatum)
 
 -- TODO: Derive this.

agora/Agora/Proposal/Scripts.hs

@@ -13,18 +13,25 @@ module Agora.Proposal.Scripts (
 import Agora.Proposal (
   PProposalDatum (PProposalDatum),
   PProposalRedeemer (..),
+  PProposalVotes (PProposalVotes),
   Proposal (governorSTAssetClass, stakeSTAssetClass),
+  ProposalStatus (VotingReady),
  )
+import Agora.Proposal.Time (currentProposalTime, isVotingPeriod)
 import Agora.Record (mkRecordConstr, (.&), (.=))
-import Agora.Stake (findStakeOwnedBy)
+import Agora.Stake (PProposalLock (..), PStakeDatum (..), findStakeOwnedBy)
 import Agora.Utils (
   anyOutput,
   findTxOutByTxOutRef,
   getMintingPolicySymbol,
+  mustBePJust,
+  mustFindDatum',
+  pisJust,
   pisUniqBy,
   psymbolValueOf,
   ptokenSpent,
   ptxSignedBy,
+  pupdate,
   pvalueSpent,
   tcassert,
   tclet,
@@ -39,6 +46,8 @@ import Plutarch.Api.V1 (
   PValidator,
  )
 import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
+import Plutarch.Map.Extra (plookup)
+import Plutarch.SafeMoney (puntag)
 import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
 
 {- | Policy for Proposals.
@@ -123,7 +132,17 @@ proposalValidator proposal =
     ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
     txInfo <- tclet $ pfromData ctx.txInfo
     PTxInfo txInfo' <- tcmatch txInfo
-    txInfoF <- tcont $ pletFields @'["inputs", "mint", "datums", "signatories"] txInfo'
+    txInfoF <-
+      tcont $
+        pletFields
+          @'[ "inputs"
+            , "outputs"
+            , "mint"
+            , "datums"
+            , "signatories"
+            , "validRange"
+            ]
+          txInfo'
     PSpending ((pfield @"_0" #) -> txOutRef) <- tcmatch $ pfromData ctx.purpose
 
     PJust txOut <- tcmatch $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
@@ -143,6 +162,8 @@ proposalValidator proposal =
             , "cosigners"
             , "thresholds"
             , "votes"
+            , "timingConfig"
+            , "startingTime"
             ]
           proposalDatum
 
@@ -163,9 +184,136 @@ proposalValidator proposal =
 
     tcassert "ST at inputs must be 1" (spentST #== 1)
 
+    currentTime <- tclet $ currentProposalTime # txInfoF.validRange
+
+    -- Filter out own output with own address and PST.
+    -- Delay the evaluation cause in some cases there won't be any continuing output.
+    ownOutputD <-
+      tclet $
+        pdelay $
+          mustBePJust # "Own output should be present" #$ pfind
+            # plam
+              ( \input -> unTermCont $ do
+                  inputF <- tcont $ pletFields @'["address", "value"] input
+                  pure $
+                    inputF.address #== ownAddress
+                      #&& psymbolValueOf # stCurrencySymbol # inputF.value #== 1
+              )
+            # pfromData txInfoF.outputs
+
+    proposalOutD <-
+      tclet $
+        pdelay $
+          mustFindDatum' @PProposalDatum
+            # (pfield @"datumHash" # pforce ownOutputD)
+            # txInfoF.datums
+
     pure $
       pmatch proposalRedeemer $ \case
-        PVote _r -> popaque (pconstant ())
+        PVote r -> unTermCont $ do
+          tcassert "Input proposal must be in VotingReady state" $
+            proposalF.status #== pconstant VotingReady
+
+          tcassert "Proposal time should be wthin the voting period" $
+            isVotingPeriod # proposalF.timingConfig # proposalF.startingTime # currentTime
+
+          -- Ensure the transaction is voting to a valid 'ResultTag'(outcome).
+          PProposalVotes voteMap <- tcmatch proposalF.votes
+          voteFor <- tclet $ pfromData $ pfield @"resultTag" # r
+
+          tcassert "Vote option should be valid" $
+            pisJust #$ plookup # voteFor # voteMap
+
+          -- Find the input stake, the amount of new votes should be the 'stakedAmount'.
+          let stakeInput =
+                pfield @"resolved"
+                  #$ mustBePJust
+                  # "Stake input should be present"
+                    #$ pfind
+                  # plam
+                    ( \(pfromData . (pfield @"value" #) . (pfield @"resolved" #) -> value) ->
+                        passetClassValueOf # value # stakeSTAssetClass #== 1
+                    )
+                  # pfromData txInfoF.inputs
+
+              stakeIn :: Term _ PStakeDatum
+              stakeIn = mustFindDatum' # (pfield @"datumHash" # stakeInput) # txInfoF.datums
+
+          stakeInF <- tcont $ pletFields @'["stakedAmount", "lockedBy", "owner"] stakeIn
+
+          -- Ensure that no lock with the current proposal id has been put on the stake.
+          tcassert "Same stake shouldn't vote on the same propsoal twice" $
+            pnot #$ pany
+              # plam
+                ( \((pfield @"proposalTag" #) . pfromData -> pid) ->
+                    pid #== proposalF.proposalId
+                )
+              # pfromData stakeInF.lockedBy
+
+          let -- Update the vote counter of the proposal, and leave other stuff as is.
+              expectedNewVotes = pmatch (pfromData proposalF.votes) $ \(PProposalVotes m) ->
+                pcon $
+                  PProposalVotes $
+                    pupdate
+                      # plam
+                        ( \votes ->
+                            pcon $ PJust $ votes + (puntag stakeInF.stakedAmount)
+                        )
+                      # voteFor
+                      # m
+              expectedProposalOut =
+                mkRecordConstr
+                  PProposalDatum
+                  ( #proposalId .= proposalF.proposalId
+                      .& #effects .= proposalF.effects
+                      .& #status .= proposalF.status
+                      .& #cosigners .= proposalF.cosigners
+                      .& #thresholds .= proposalF.thresholds
+                      .& #votes .= pdata expectedNewVotes
+                      .& #timingConfig .= proposalF.timingConfig
+                      .& #startingTime .= proposalF.startingTime
+                  )
+
+          tcassert "Output proposal should be valid" $ pforce proposalOutD #== expectedProposalOut
+
+          -- We validate the output stake datum here as well: We need the vote option
+          -- to create a valid 'ProposalLock', however the vote option is encoded
+          -- in the proposal redeemer, which is invisible for the stake validator.
+
+          let stakeOutput =
+                mustBePJust # "Stake output should be present"
+                  #$ pfind
+                  # plam
+                    ( \(pfromData . (pfield @"value" #) -> value) ->
+                        passetClassValueOf # value # stakeSTAssetClass #== 1
+                    )
+                  # pfromData txInfoF.outputs
+
+              stakeOut :: Term _ PStakeDatum
+              stakeOut = mustFindDatum' # (pfield @"datumHash" # stakeOutput) # txInfoF.datums
+
+          let newProposalLock =
+                mkRecordConstr
+                  PProposalLock
+                  ( #vote .= pdata voteFor
+                      .& #proposalTag .= proposalF.proposalId
+                  )
+              -- Prepend the new lock to existing locks
+              expectedProposalLocks =
+                pcons
+                  # pdata newProposalLock
+                  # pfromData stakeInF.lockedBy
+              expectedStakeOut =
+                mkRecordConstr
+                  PStakeDatum
+                  ( #stakedAmount .= stakeInF.stakedAmount
+                      .& #owner .= stakeInF.owner
+                      .& #lockedBy .= pdata expectedProposalLocks
+                  )
+
+          tcassert "Output stake should be locked by the proposal" $ expectedStakeOut #== stakeOut
+
+          pure $ popaque (pconstant ())
         --------------------------------------------------------------------------
         PCosign r -> unTermCont $ do
           newSigs <- tclet $ pfield @"newCosigners" # r
@@ -214,6 +362,8 @@ proposalValidator proposal =
                                   .& #cosigners .= pdata updatedSigs
                                   .& #thresholds .= proposalF.thresholds
                                   .& #votes .= proposalF.votes
+                                  .& #timingConfig .= proposalF.timingConfig
+                                  .& #startingTime .= proposalF.startingTime
                               )
                           )
                  in foldr1

agora/Agora/Proposal/Time.hs

@@ -39,7 +39,12 @@ import Plutarch.Api.V1 (
   PPOSIXTimeRange,
   PUpperBound (PUpperBound),
  )
-import Plutarch.DataRepr (PDataFields, PIsDataReprInstances (..))
+import Plutarch.DataRepr (DerivePConstantViaData (..), PDataFields, PIsDataReprInstances (..))
+import Plutarch.Lift (
+  DerivePConstantViaNewtype (..),
+  PConstantDecl,
+  PUnsafeLiftDecl (..),
+ )
 import Plutarch.Numeric (AdditiveSemigroup ((+)))
 import Plutarch.Unsafe (punsafeCoerce)
 import Plutus.V1.Ledger.Time (POSIXTime)
@@ -122,10 +127,24 @@ newtype PProposalTime (s :: S)
     (PlutusType, PIsData, PDataFields)
     via (PIsDataReprInstances PProposalTime)
 
+instance PUnsafeLiftDecl PProposalTime where
+  type PLifted PProposalTime = ProposalTime
+deriving via
+  (DerivePConstantViaData ProposalTime PProposalTime)
+  instance
+    (PConstantDecl ProposalTime)
+
 -- | Plutarch-level version of 'ProposalStartingTime'.
 newtype PProposalStartingTime (s :: S) = PProposalStartingTime (Term s PPOSIXTime)
   deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype PProposalStartingTime PPOSIXTime)
 
+instance PUnsafeLiftDecl PProposalStartingTime where
+  type PLifted PProposalStartingTime = ProposalStartingTime
+deriving via
+  (DerivePConstantViaNewtype ProposalStartingTime PProposalStartingTime PPOSIXTime)
+  instance
+    (PConstantDecl ProposalStartingTime)
+
 -- | Plutarch-level version of 'ProposalTimingConfig'.
 newtype PProposalTimingConfig (s :: S) = PProposalTimingConfig
   { getProposalTimingConfig ::
@@ -146,6 +165,13 @@ newtype PProposalTimingConfig (s :: S) = PProposalTimingConfig
     (PlutusType, PIsData, PDataFields)
     via (PIsDataReprInstances PProposalTimingConfig)
 
+instance PUnsafeLiftDecl PProposalTimingConfig where
+  type PLifted PProposalTimingConfig = ProposalTimingConfig
+deriving via
+  (DerivePConstantViaData ProposalTimingConfig PProposalTimingConfig)
+  instance
+    (PConstantDecl ProposalTimingConfig)
+
 --------------------------------------------------------------------------------
 
 -- FIXME: Orphan instance, move this to plutarch-extra.

agora/Agora/Stake.hs

@@ -191,7 +191,7 @@ newtype PStakeDatum (s :: S) = PStakeDatum
   deriving anyclass (Generic)
   deriving anyclass (PIsDataRepr)
   deriving
-    (PlutusType, PIsData, PDataFields)
+    (PlutusType, PIsData, PDataFields, PEq)
     via (PIsDataReprInstances PStakeDatum)
 
 instance PTryFrom PData (PAsData PStakeDatum) where
@@ -241,7 +241,7 @@ newtype PProposalLock (s :: S) = PProposalLock
   deriving anyclass (Generic)
   deriving anyclass (PIsDataRepr)
   deriving
-    (PlutusType, PIsData, PDataFields)
+    (PlutusType, PIsData, PDataFields, PEq)
     via (PIsDataReprInstances PProposalLock)
 
 deriving via

agora/Agora/Stake/Scripts.hs

@@ -7,6 +7,7 @@ Plutus Scripts for Stakes.
 -}
 module Agora.Stake.Scripts (stakePolicy, stakeValidator) where
 
+import Agora.Record (mkRecordConstr, (.&), (.=))
 import Agora.SafeMoney (GTTag)
 import Agora.Stake
 import Agora.Utils (
@@ -222,7 +223,7 @@ stakeValidator stake =
     -- TODO: Use PTryFrom
     let stakeDatum' :: Term _ PStakeDatum
         stakeDatum' = pfromData $ punsafeCoerce datum
-    stakeDatum <- tcont $ pletFields @'["owner", "stakedAmount"] stakeDatum'
+    stakeDatum <- tcont $ pletFields @'["owner", "stakedAmount", "lockedBy"] stakeDatum'
 
     PSpending txOutRef <- tcmatch $ pfromData ctx.purpose
 
@@ -291,7 +292,7 @@ stakeValidator stake =
 
           pure $ popaque (pconstant ())
         --------------------------------------------------------------------------
-        PPermitVote _ -> unTermCont $ do
+        PPermitVote l -> unTermCont $ do
           tcassert
             "Owner signs this transaction"
             ownerSignsTransaction
@@ -301,18 +302,38 @@ stakeValidator stake =
           tcassert "Proposal ST spent" $
             spentProposalST #== 1
 
+          -- Update the stake datum, but only the 'lockedBy' field.
+
+          let -- We actually don't know whether the given lock is valid or not.
+              -- This is checked in the proposal validator.
+              newLock = pfield @"lock" # l
+              -- Prepend the new lock to the existing locks.
+              expectedLocks = pcons # newLock # stakeDatum.lockedBy
+
+          expectedDatum <-
+            tclet $
+              pdata $
+                mkRecordConstr
+                  PStakeDatum
+                  ( #stakedAmount .= stakeDatum.stakedAmount
+                      .& #owner .= stakeDatum.owner
+                      .& #lockedBy .= pdata expectedLocks
+                  )
+
           tcassert "A UTXO must exist with the correct output" $
+            -- FIXME: no need to pass the whole txInfo to 'anyOutput'.
             anyOutput @PStakeDatum # txInfo
               #$ plam
               $ \value address newStakeDatum' ->
                 let isScriptAddress = pdata address #== ownAddress
-                    _correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
+                    correctOutputDatum = pdata newStakeDatum' #== expectedDatum
                     valueCorrect = pdata continuingValue #== pdata value
                  in pif
                       isScriptAddress
                       ( foldl1
                           (#&&)
                           [ ptraceIfFalse "valueCorrect" valueCorrect
+                          , ptraceIfFalse "datumCorrect" correctOutputDatum
                           ]
                       )
                       (pcon PFalse)

agora/Agora/Utils.hs

@@ -40,6 +40,8 @@ module Agora.Utils (
   pmsortBy,
   pmsort,
   pnubSort,
+  pupdate,
+  pmapMaybe,
 
   -- * Functions which should (probably) not be upstreamed
   anyOutput,
@@ -286,6 +288,42 @@ pmapUnionWith = phoistAcyclic $
             # ys
     pure $ pcon (PMap $ pconcat # ls # rs)
 
+-- | A special version of `pmap` which allows list elements to be thrown out.
+pmapMaybe :: forall s a list. (PIsListLike list a) => Term s ((a :--> PMaybe a) :--> list a :--> list a)
+pmapMaybe = phoistAcyclic $
+  pfix #$ plam $ \self f l -> pif (pnull # l) pnil $
+    unTermCont $ do
+      x <- tclet $ phead # l
+      xs <- tclet $ ptail # l
+
+      pure $
+        pmatch (f # x) $ \case
+          PJust ux -> pcons # ux #$ self # f # xs
+          _ -> self # f # xs
+
+-- | / O(n) /. Update the value at a given key in a `PMap`, have the same functionalities as 'Data.Map.update'.
+pupdate :: forall s k v. (PIsData k, PIsData v) => Term s ((v :--> PMaybe v) :--> k :--> PMap k v :--> PMap k v)
+pupdate = phoistAcyclic $
+  plam $ \f (pdata -> tk) (pto -> (ps :: Term _ (PBuiltinList _))) ->
+    pcon $
+      PMap $
+        pmapMaybe
+          # plam
+            ( \kv ->
+                let k = pfstBuiltin # kv
+                    v = pfromData $ psndBuiltin # kv
+                 in pif
+                      (k #== tk)
+                      -- 'PBuiltinPair' doesn't have 'PFunctor', so:
+                      ( pmatch (f # v) $
+                          \case
+                            PJust uv -> pcon $ PJust $ ppairDataBuiltin # k # pdata uv
+                            _ -> pcon PNothing
+                      )
+                      (pcon $ PJust kv)
+            )
+          # ps
+
 -- | Add two 'PValue's together.
 paddValue :: forall s. Term s (PValue :--> PValue :--> PValue)
 paddValue = phoistAcyclic $