From faf326f9c30c4cbae73e2c97040de69ba159b9c4 Mon Sep 17 00:00:00 2001 From: Emily Martins Date: Fri, 15 Apr 2022 22:22:22 +0200 Subject: [PATCH] implement Agora.Record, implement Agora.Proposal.Time --- agora.cabal | 3 + agora/Agora/Proposal.hs | 11 +-- agora/Agora/Proposal/Time.hs | 160 +++++++++++++++++++++++++++++++++++ agora/Agora/Record.hs | 67 +++++++++++++++ 4 files changed, 236 insertions(+), 5 deletions(-) create mode 100644 agora/Agora/Proposal/Time.hs create mode 100644 agora/Agora/Record.hs diff --git a/agora.cabal b/agora.cabal index c1729d0..bd07338 100644 --- a/agora.cabal +++ b/agora.cabal @@ -78,6 +78,7 @@ common lang UndecidableInstances ViewPatterns OverloadedRecordDot + OverloadedLabels QualifiedDo default-language: Haskell2010 @@ -128,9 +129,11 @@ library Agora.Governor Agora.MultiSig Agora.Proposal + Agora.Proposal.Time Agora.SafeMoney Agora.Stake Agora.Treasury + Agora.Record other-modules: Agora.Utils diff --git a/agora/Agora/Proposal.hs b/agora/Agora/Proposal.hs index d4b6c4d..5399e95 100644 --- a/agora/Agora/Proposal.hs +++ b/agora/Agora/Proposal.hs @@ -105,8 +105,9 @@ data ProposalStatus -- proposal will be able to be voted on. VotingReady | -- | The proposal has been voted on, and the votes have been locked - -- permanently. The proposal can now be executed. - Voted + -- 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 @@ -121,7 +122,7 @@ data ProposalStatus Finished deriving stock (Eq, Show, GHC.Generic) -PlutusTx.makeIsDataIndexed ''ProposalStatus [('Draft, 0), ('VotingReady, 1), ('Voted, 2), ('Finished, 3)] +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 @@ -198,12 +199,12 @@ data ProposalRedeemer -- 1. The sum of all of the cosigner's GT is larger than the 'vote' field of 'ProposalThresholds'. -- 2. The proposal hasn't been alive for longer than the review time. -- - -- @'VotingReady' -> 'Voted'@: + -- @'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 hasn't been alive for longer than the voting time. -- - -- @'Voted' -> 'Finished'@: + -- @'Locked' -> 'Finished'@: -- Always valid provided the conditions for the transition are met. -- -- @* -> 'Finished'@: diff --git a/agora/Agora/Proposal/Time.hs b/agora/Agora/Proposal/Time.hs new file mode 100644 index 0000000..7245dd0 --- /dev/null +++ b/agora/Agora/Proposal/Time.hs @@ -0,0 +1,160 @@ +{-# 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 ranges given config and starting time. + proposalDraftRange, + + -- * Upstreamables + plowerBound, + pupperBound, + pstrictLowerBound, + pstrictUpperBound, +) where + +import Agora.Record (build, (.&), (.=)) +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.Numeric (AdditiveSemigroup ((+))) +import Plutarch.Unsafe (punsafeCoerce) +import Plutus.V1.Ledger.Time (POSIXTime, POSIXTimeRange) +import PlutusTx qualified +import Prelude hiding ((+)) + +-------------------------------------------------------------------------------- + +-- | Represents the current time, as far as the proposal is concerned. +newtype ProposalTime = ProposalTime + { getProposalTime :: POSIXTimeRange + } + deriving newtype (PlutusTx.ToData, PlutusTx.FromData, PlutusTx.UnsafeFromData) + deriving stock (Eq, Show, GHC.Generic) + +-- | 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. +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 PPOSIXTime) + deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype PProposalTime PPOSIXTime) + +-- | 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) + +-------------------------------------------------------------------------------- + +-- -- Need to move these away from here +pstrictLowerBound :: PIsData a => Term s (a :--> PLowerBound a) +pstrictLowerBound = phoistAcyclic $ + plam $ \a -> + pcon + ( PLowerBound $ + build $ + #_0 .= pdata (pcon (PFinite $ build $ #_0 .= pdata a)) + .& #_1 .= pdata (pcon PFalse) + ) + +pstrictUpperBound :: PIsData a => Term s (a :--> PUpperBound a) +pstrictUpperBound = phoistAcyclic $ + plam $ \a -> + pcon + ( PUpperBound $ + build $ + #_0 .= pdata (pcon (PFinite $ build $ #_0 .= pdata a)) + .& #_1 .= pdata (pcon PFalse) + ) + +plowerBound :: PIsData a => Term s (a :--> PLowerBound a) +plowerBound = phoistAcyclic $ + plam $ \a -> + pcon + ( PLowerBound $ + build $ + #_0 .= pdata (pcon (PFinite $ build $ #_0 .= pdata a)) + .& #_1 .= pdata (pcon PTrue) + ) + +pupperBound :: PIsData a => Term s (a :--> PUpperBound a) +pupperBound = phoistAcyclic $ + plam $ \a -> + pcon + ( PUpperBound $ + build $ + #_0 .= pdata (pcon (PFinite $ build $ #_0 .= pdata a)) + .& #_1 .= pdata (pcon PTrue) + ) + +-- Move this to plutarch-extra. +instance AdditiveSemigroup (Term s PPOSIXTime) where + (punsafeCoerce @_ @_ @PInteger -> x) + (punsafeCoerce @_ @_ @PInteger -> y) = punsafeCoerce $ x + y + +-- | Compute the range of time during which cosigning is legal. +proposalDraftRange :: Term s (PPOSIXTime :--> PProposalTimingConfig :--> PPOSIXTimeRange) +proposalDraftRange = phoistAcyclic $ + plam $ \s config -> + pcon + ( PInterval $ + build $ + #from .= pdata (pstrictLowerBound # s) + .& #to .= pdata (pstrictUpperBound #$ s + pfield @"draftTime" # config) + ) diff --git a/agora/Agora/Record.hs b/agora/Agora/Record.hs new file mode 100644 index 0000000..3cd0723 --- /dev/null +++ b/agora/Agora/Record.hs @@ -0,0 +1,67 @@ +{- | +Module : Agora.Record +Maintainer : emi@haskell.fyi +Description: PDataRecord helper functions. + +PDataRecord helper functions. +-} +module Agora.Record (build, (.=), (.&)) 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, @'build' (#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 builder into a fully built 'PDataRecord'. +build :: forall (s :: S) (r :: [PLabeledType]). RecordMorphism s '[] r -> Term s (PDataRecord r) +build f = coerce f pdnil + +-- | 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). + FieldName sym -> + Term s (PAsData a) -> + ( RecordMorphism s as ((sym ':= a) ': as) + ) +_ .= x = RecordMorphism $ pcon . PDCons x + +infixr 6 .& + +-- | Compose two morphisms between records. +(.&) :: + forall + (s :: S) + (a :: [PLabeledType]) + (b :: [PLabeledType]) + (c :: [PLabeledType]). + (RecordMorphism s b c) -> + (RecordMorphism s a b) -> + (RecordMorphism s a c) +(.&) = (.)