536 lines
15 KiB
Haskell
536 lines
15 KiB
Haskell
{-# LANGUAGE TemplateHaskell #-}
|
|
|
|
{- |
|
|
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
|
|
ProposalTimingConfig (..),
|
|
ProposalStartingTime (..),
|
|
MaxTimeRangeWidth (..),
|
|
|
|
-- * Plutarch-land
|
|
PProposalTime,
|
|
PProposalTimingConfig (..),
|
|
PProposalStartingTime (..),
|
|
PMaxTimeRangeWidth (..),
|
|
PTimingRelation (..),
|
|
PPeriod (..),
|
|
|
|
-- * Compute periods given config and starting time.
|
|
pvalidateProposalStartingTime,
|
|
pcurrentProposalTime,
|
|
pisProposalTimingConfigValid,
|
|
pisMaxTimeRangeWidthValid,
|
|
pgetRelation,
|
|
pisWithin,
|
|
psatisfyMaximumWidth,
|
|
) where
|
|
|
|
import Data.Functor ((<&>))
|
|
import Plutarch.Api.V1 (
|
|
PExtended (PFinite),
|
|
PInterval (PInterval),
|
|
PLowerBound (PLowerBound),
|
|
PPOSIXTime,
|
|
PUpperBound (PUpperBound),
|
|
)
|
|
import Plutarch.Api.V2 (PPOSIXTimeRange)
|
|
import Plutarch.DataRepr (
|
|
DerivePConstantViaData (..),
|
|
PDataFields,
|
|
)
|
|
import Plutarch.Extra.Applicative (PApply (pliftA2))
|
|
import Plutarch.Extra.Bool (passert)
|
|
import Plutarch.Extra.Field (pletAll, pletAllC)
|
|
import Plutarch.Extra.IsData (PlutusTypeEnumData)
|
|
import Plutarch.Extra.Maybe (pjust, pmaybe, pnothing)
|
|
import Plutarch.Extra.Time (
|
|
PFullyBoundedTimeRange (PFullyBoundedTimeRange),
|
|
pisWithinTimeRange,
|
|
ptimeRangeDuration,
|
|
)
|
|
import Plutarch.Lift (
|
|
DerivePConstantViaNewtype (DerivePConstantViaNewtype),
|
|
PConstantDecl,
|
|
PUnsafeLiftDecl (PLifted),
|
|
)
|
|
import Plutarch.Num (PNum)
|
|
import PlutusLedgerApi.V1 (POSIXTime)
|
|
import PlutusTx qualified
|
|
import "liqwid-plutarch-extra" Plutarch.Extra.TermCont (pletC, pmatchC)
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
{- | Represents the starting time of the proposal.
|
|
|
|
@since 0.1.0
|
|
-}
|
|
newtype ProposalStartingTime = ProposalStartingTime
|
|
{ getProposalStartingTime :: POSIXTime
|
|
}
|
|
deriving stock
|
|
( -- | @since 0.1.0
|
|
Eq
|
|
, -- | @since 0.1.0
|
|
Show
|
|
, -- | @since 0.1.0
|
|
Generic
|
|
)
|
|
deriving newtype
|
|
( -- | @since 0.1.0
|
|
PlutusTx.ToData
|
|
, -- | @since 0.1.0
|
|
PlutusTx.FromData
|
|
, -- | @since 0.1.0
|
|
PlutusTx.UnsafeFromData
|
|
)
|
|
|
|
-- | Represents the maximum width of a 'PlutusLedgerApi.V1.Time.POSIXTimeRange'.
|
|
newtype MaxTimeRangeWidth = MaxTimeRangeWidth {getMaxWidth :: POSIXTime}
|
|
deriving stock
|
|
( -- | @since 0.1.0
|
|
Eq
|
|
, -- | @since 0.1.0
|
|
Show
|
|
, -- | @since 0.1.0
|
|
Ord
|
|
, -- | @since 0.1.0
|
|
Generic
|
|
)
|
|
deriving newtype
|
|
( -- | @since 0.1.0
|
|
PlutusTx.ToData
|
|
, -- | @since 0.1.0
|
|
PlutusTx.FromData
|
|
, -- | @since 0.1.0
|
|
PlutusTx.UnsafeFromData
|
|
, -- | @since 1.0.0
|
|
Num
|
|
)
|
|
|
|
{- | Configuration of proposal timings.
|
|
|
|
See: https://liqwid.notion.site/Proposals-589853145a994057aa77f397079f75e4#d25ea378768d4c76b52dd4c1b6bc0fcd
|
|
|
|
@since 0.1.0
|
|
-}
|
|
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.
|
|
, minStakeVotingTime :: POSIXTime
|
|
-- ^ Minimum time from creating a voting lock until it can be destroyed.
|
|
, votingTimeRangeMaxWidth :: MaxTimeRangeWidth
|
|
-- ^ The maximum width of transaction time range while voting.
|
|
}
|
|
deriving stock
|
|
( -- | @since 0.1.0
|
|
Eq
|
|
, -- | @since 0.1.0
|
|
Show
|
|
, -- | @since 0.1.0
|
|
Generic
|
|
)
|
|
|
|
PlutusTx.makeIsDataIndexed 'ProposalTimingConfig [('ProposalTimingConfig, 0)]
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
{- | == 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.
|
|
|
|
'PProposalTime' represents "the time according to the proposal".
|
|
Its representation is opaque, and doesn't matter.
|
|
|
|
Various functions work simply on 'PProposalTime' and 'ProposalTimingConfig'.
|
|
In particular, 'currentProposalTime' is useful for extracting the time
|
|
from the 'PlutusLedgerApi.V1.txInfoValidPeriod' field
|
|
of 'PlutusLedgerApi.V1.TxInfo'.
|
|
|
|
We avoid 'PPOSIXTimeRange' where we can in order to save on operations.
|
|
|
|
Note: 'PProposalTime' doesn't need a Haskell-level equivalent because it
|
|
is only used in scripts, and does not go in datums. It is also scott-encoded
|
|
which is more efficient in usage.
|
|
|
|
@since 0.1.0
|
|
-}
|
|
type PProposalTime = PFullyBoundedTimeRange
|
|
|
|
-- | Plutarch-level version of 'ProposalStartingTime'.
|
|
newtype PProposalStartingTime (s :: S) = PProposalStartingTime (Term s PPOSIXTime)
|
|
deriving stock
|
|
( -- | @since 0.1.0
|
|
Generic
|
|
)
|
|
deriving anyclass
|
|
( -- | @since 0.1.0
|
|
PlutusType
|
|
, -- | @since 0.1.0
|
|
PIsData
|
|
, -- | @since 0.1.0
|
|
PEq
|
|
)
|
|
|
|
instance DerivePlutusType PProposalStartingTime where
|
|
type DPTStrat _ = PlutusTypeNewtype
|
|
|
|
-- | @since 0.1.0
|
|
instance PUnsafeLiftDecl PProposalStartingTime where
|
|
type PLifted PProposalStartingTime = ProposalStartingTime
|
|
|
|
instance PTryFrom PData (PAsData PProposalStartingTime)
|
|
|
|
-- | @since 0.1.0
|
|
deriving via
|
|
(DerivePConstantViaNewtype ProposalStartingTime PProposalStartingTime PPOSIXTime)
|
|
instance
|
|
(PConstantDecl ProposalStartingTime)
|
|
|
|
{- | Plutarch-level version of 'ProposalTimingConfig'.
|
|
|
|
@since 0.1.0
|
|
-}
|
|
newtype PProposalTimingConfig (s :: S) = PProposalTimingConfig
|
|
{ getProposalTimingConfig ::
|
|
Term
|
|
s
|
|
( PDataRecord
|
|
'[ "draftTime" ':= PPOSIXTime
|
|
, "votingTime" ':= PPOSIXTime
|
|
, "lockingTime" ':= PPOSIXTime
|
|
, "executingTime" ':= PPOSIXTime
|
|
, "minStakeVotingTime" ':= PPOSIXTime
|
|
, "votingTimeRangeMaxWidth" ':= PMaxTimeRangeWidth
|
|
]
|
|
)
|
|
}
|
|
deriving stock
|
|
( -- | @since 0.1.0
|
|
Generic
|
|
)
|
|
deriving anyclass
|
|
( -- | @since 0.1.0
|
|
PlutusType
|
|
, -- | @since 0.1.0
|
|
PIsData
|
|
, -- | @since 0.1.0
|
|
PDataFields
|
|
, -- | @since 0.2.1
|
|
PShow
|
|
)
|
|
|
|
instance DerivePlutusType PProposalTimingConfig where
|
|
type DPTStrat _ = PlutusTypeData
|
|
|
|
-- | @since 0.1.0
|
|
instance PTryFrom PData PProposalTimingConfig
|
|
|
|
-- | @since 0.1.0
|
|
instance PUnsafeLiftDecl PProposalTimingConfig where
|
|
type PLifted PProposalTimingConfig = ProposalTimingConfig
|
|
|
|
-- | @since 0.1.0
|
|
deriving via
|
|
(DerivePConstantViaData ProposalTimingConfig PProposalTimingConfig)
|
|
instance
|
|
(PConstantDecl ProposalTimingConfig)
|
|
|
|
-- | Plutarch-level version of 'MaxTimeRangeWidth'.
|
|
newtype PMaxTimeRangeWidth (s :: S)
|
|
= PMaxTimeRangeWidth (Term s PPOSIXTime)
|
|
deriving stock
|
|
( -- | @since 0.2.0
|
|
Generic
|
|
)
|
|
deriving anyclass
|
|
( -- | @since 0.1.0
|
|
PlutusType
|
|
, -- | @since 0.1.0
|
|
PIsData
|
|
, -- | @since 0.1.0
|
|
PEq
|
|
, -- | @since 0.2.0
|
|
PPartialOrd
|
|
, -- | @since 0.1.0
|
|
POrd
|
|
, -- | @since 0.2.1
|
|
PShow
|
|
, -- | @since 1.0.0
|
|
PNum
|
|
)
|
|
|
|
instance DerivePlutusType PMaxTimeRangeWidth where
|
|
type DPTStrat _ = PlutusTypeNewtype
|
|
|
|
-- | @since 0.1.0
|
|
instance PTryFrom PData (PAsData PMaxTimeRangeWidth)
|
|
|
|
-- | @since 0.1.0
|
|
instance PUnsafeLiftDecl PMaxTimeRangeWidth where type PLifted PMaxTimeRangeWidth = MaxTimeRangeWidth
|
|
|
|
-- | @since 0.1.0
|
|
deriving via
|
|
(DerivePConstantViaNewtype MaxTimeRangeWidth PMaxTimeRangeWidth PPOSIXTime)
|
|
instance
|
|
(PConstantDecl MaxTimeRangeWidth)
|
|
|
|
--------------------------------------------------------------------------------
|
|
|
|
{- | Return true if the timing configuration is valid.
|
|
|
|
@since 0.2.0
|
|
-}
|
|
pisProposalTimingConfigValid :: forall (s :: S). Term s (PProposalTimingConfig :--> PBool)
|
|
pisProposalTimingConfigValid = phoistAcyclic $
|
|
plam $ \conf -> unTermCont $ do
|
|
confF <- pletAllC conf
|
|
|
|
-- everything is greater or equal 0
|
|
pure $
|
|
ptraceIfFalse "ge 0" $
|
|
foldr
|
|
( \t ->
|
|
(#&&)
|
|
( pconstant 0
|
|
#<= pfromData t
|
|
)
|
|
)
|
|
(pconstant True)
|
|
[ confF.draftTime
|
|
, confF.votingTime
|
|
, confF.lockingTime
|
|
, confF.executingTime
|
|
, confF.minStakeVotingTime
|
|
, pto confF.votingTimeRangeMaxWidth
|
|
]
|
|
|
|
{- | Return true if the maximum time width is greater than 0.
|
|
|
|
@since 0.2.0
|
|
-}
|
|
pisMaxTimeRangeWidthValid :: Term s (PMaxTimeRangeWidth :--> PBool)
|
|
pisMaxTimeRangeWidthValid =
|
|
phoistAcyclic $
|
|
plam $
|
|
ptraceIfFalse "greater than 0"
|
|
. (pconstant (MaxTimeRangeWidth 0) #<)
|
|
|
|
{- | Validate starting time of a proposal, from the 'PlutusLedgerApi.V1.txInfoValidPeriod' field.
|
|
For every proposal, this is only meant to run once upon creation. Given time range should be
|
|
tight enough, meaning that the width of the time range should be less than the maximum value.
|
|
|
|
@since 1.0.0
|
|
-}
|
|
pvalidateProposalStartingTime ::
|
|
forall (s :: S).
|
|
Term
|
|
s
|
|
( PMaxTimeRangeWidth
|
|
:--> PPOSIXTimeRange
|
|
:--> PProposalStartingTime
|
|
:--> PBool
|
|
)
|
|
pvalidateProposalStartingTime = phoistAcyclic $
|
|
plam $ \maxWidth iv (pto -> st) ->
|
|
pmaybe
|
|
# pconstant False
|
|
# plam
|
|
( \ct ->
|
|
let isTightEnough =
|
|
ptraceIfFalse
|
|
"createProposalStartingTime: given time range should be tight enough"
|
|
$ psatisfyMaximumWidth # maxWidth # ct
|
|
isInCurrentTimeRange =
|
|
ptraceIfFalse
|
|
"createProposalStartingTime: starting time should be in current time range"
|
|
$ pisWithinTimeRange # st # ct
|
|
in isTightEnough #&& isInCurrentTimeRange
|
|
)
|
|
# (pcurrentProposalTime # iv)
|
|
|
|
{- | Get the current proposal time, given the 'PlutusLedgerApi.V1.txInfoValidPeriod' field.
|
|
|
|
If it's impossible to get a fully-bounded time, (e.g. either end of the 'PPOSIXTimeRange' is
|
|
an infinity) then we return nothing.
|
|
|
|
Note that we ignore the inclusiveness of the upper bound. Due to the fact
|
|
that there's no place in the Cardano domain transaction type to store the
|
|
inclusiveness information, we can never get a time range with closed upper
|
|
bound. See also the ledger implementation: https://bit.ly/3BDzW5R
|
|
|
|
@since 0.1.0
|
|
-}
|
|
pcurrentProposalTime :: forall (s :: S). Term s (PPOSIXTimeRange :--> PMaybe PProposalTime)
|
|
pcurrentProposalTime = phoistAcyclic $
|
|
plam $ \iv -> unTermCont $ do
|
|
PInterval iv' <- pmatchC iv
|
|
ivf <- pletAllC iv'
|
|
PLowerBound lb <- pmatchC ivf.from
|
|
PUpperBound ub <- pmatchC ivf.to
|
|
|
|
let lowerBound = pletAll lb $ \f ->
|
|
pif
|
|
f._1
|
|
( pmatch f._0 $ \case
|
|
PFinite (pfromData . (pfield @"_0" #) -> d) -> pjust # d
|
|
_ -> ptrace "currentProposalTime: time range should be bounded" pnothing
|
|
)
|
|
(ptrace "currentProposalTime: lower bound of the time range should be inclusive" pnothing)
|
|
|
|
upperBound = pletAll ub $ \f ->
|
|
pmatch f._0 $ \case
|
|
PFinite (pfromData . (pfield @"_0" #) -> d) -> pjust # d
|
|
_ -> ptrace "currentProposalTime: time range should be bounded" pnothing
|
|
|
|
mkTime = phoistAcyclic $
|
|
plam $ \lb ub ->
|
|
passert
|
|
"Upper bound bigger than lower bound"
|
|
(lb #< ub)
|
|
(pcon $ PFullyBoundedTimeRange lb ub)
|
|
|
|
pure $ pliftA2 # mkTime # lowerBound # upperBound
|
|
|
|
{- | Represent relation between current time and a given period.
|
|
|
|
Note that the "before" relation isn't present due to the fact that
|
|
it's considered as an error in the proposal script.
|
|
|
|
@since 1.0.0
|
|
-}
|
|
data PTimingRelation (s :: S)
|
|
= PWithin
|
|
| PAfter
|
|
deriving stock
|
|
( -- | @since 1.0.0
|
|
Generic
|
|
, -- | @since 1.0.0
|
|
Enum
|
|
, -- | @since 1.0.0
|
|
Bounded
|
|
)
|
|
deriving anyclass
|
|
( -- | @since 1.0.0
|
|
PlutusType
|
|
)
|
|
|
|
-- | @since 1.0.0
|
|
instance DerivePlutusType PTimingRelation where
|
|
type DPTStrat _ = PlutusTypeEnumData
|
|
|
|
{- | Return true if a relation is 'PWithin'.
|
|
|
|
@since 1.0.0
|
|
-}
|
|
pisWithin :: forall (s :: S). Term s (PTimingRelation :--> PBool)
|
|
pisWithin = phoistAcyclic $
|
|
plam $
|
|
flip pmatch $ \case
|
|
PWithin -> pconstant True
|
|
_ -> pconstant False
|
|
|
|
{- | Represent a proposal period.
|
|
|
|
@since 1.0.0
|
|
-}
|
|
data PPeriod (s :: S)
|
|
= PDraftingPeriod
|
|
| PVotingPeriod
|
|
| PLockingPeriod
|
|
| PExecutingPeriod
|
|
deriving stock
|
|
( -- | @since 1.0.0
|
|
Generic
|
|
, -- | @since 1.0.0
|
|
Enum
|
|
, -- | @since 1.0.0
|
|
Bounded
|
|
)
|
|
deriving anyclass
|
|
( -- | @since 1.0.0
|
|
PlutusType
|
|
)
|
|
|
|
-- | @since 1.0.0
|
|
instance DerivePlutusType PPeriod where
|
|
type DPTStrat _ = PlutusTypeEnumData
|
|
|
|
{- | Compute the relation between current time range and the given peroid,
|
|
providing the starting time and timing configuration of a proposal. If the
|
|
relation cannot be determined, error out.
|
|
|
|
@since 1.0.0
|
|
-}
|
|
pgetRelation ::
|
|
forall (s :: S).
|
|
Term
|
|
s
|
|
( PProposalTimingConfig
|
|
:--> PProposalStartingTime
|
|
:--> PProposalTime
|
|
:--> PPeriod
|
|
:--> PTimingRelation
|
|
)
|
|
pgetRelation = phoistAcyclic $
|
|
plam $ \config startingTime currentTime period -> unTermCont $ do
|
|
configF <- pletAllC config
|
|
|
|
PProposalStartingTime s <- pmatchC startingTime
|
|
PFullyBoundedTimeRange lb ub <- pmatchC currentTime
|
|
|
|
dub <- pletC $ s + configF.draftTime
|
|
vub <- pletC $ dub + configF.votingTime
|
|
lub <- pletC $ vub + configF.lockingTime
|
|
eub <- pletC $ lub + configF.executingTime
|
|
|
|
(plb, pub) <-
|
|
pmatchC period
|
|
<&> ( \case
|
|
PDraftingPeriod -> (s, dub)
|
|
PVotingPeriod -> (dub, vub)
|
|
PLockingPeriod -> (vub, lub)
|
|
PExecutingPeriod -> (lub, eub)
|
|
)
|
|
|
|
pure $
|
|
pif (plb #<= lb #&& ub #<= pub) (pcon PWithin) $
|
|
pif (pub #< lb) (pcon PAfter) $
|
|
ptraceError "pgetRelation: too early or invalid current time"
|
|
|
|
{- | Return true if the width of given 'PProposalTime' is shorter than the
|
|
maximum.
|
|
|
|
@since 1.0.0
|
|
-}
|
|
psatisfyMaximumWidth ::
|
|
forall (s :: S).
|
|
Term
|
|
s
|
|
( PMaxTimeRangeWidth
|
|
:--> PProposalTime
|
|
:--> PBool
|
|
)
|
|
psatisfyMaximumWidth = phoistAcyclic $
|
|
plam $ \maxWidth time ->
|
|
let width = ptimeRangeDuration # time
|
|
max = pto maxWidth
|
|
in width #<= max
|