migrate Haskell-level datums to use Discrete

This commit is contained in:
Emily Martins 2022-03-26 15:08:11 +01:00
parent 48541836c7
commit 15d25f314b
8 changed files with 44 additions and 140 deletions

View file

@ -21,7 +21,6 @@ module Spec.Sample.Stake (
) where
--------------------------------------------------------------------------------
import Plutarch.Api.V1 (
mintingPolicySymbol,
mkMintingPolicy,
@ -144,9 +143,9 @@ stakeCreationUnsigned =
-- | Config for creating a ScriptContext that deposits or withdraws.
data DepositWithdrawExample = DepositWithdrawExample
{ startAmount :: Integer
{ startAmount :: Discrete GTTag
-- ^ The amount of GT stored before the transaction.
, delta :: Integer
, delta :: Discrete GTTag
-- ^ The amount of GT deposited or withdrawn from the Stake.
}
@ -169,10 +168,7 @@ stakeDepositWithdraw config =
{ txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
, txOutValue =
st
<> Value.singleton
"da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
"LQ"
stakeBefore.stakedAmount
<> discreteValue stake.gtClassRef stakeBefore.stakedAmount
, txOutDatumHash = Just (toDatumHash stakeAfter)
}
]
@ -181,10 +177,7 @@ stakeDepositWithdraw config =
{ txOutAddress = Address (ScriptCredential $ validatorHash validator) Nothing
, txOutValue =
st
<> Value.singleton
"da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
"LQ"
stakeAfter.stakedAmount
<> discreteValue stake.gtClassRef stakeAfter.stakedAmount
, txOutDatumHash = Just (toDatumHash stakeAfter)
}
]

View file

@ -1,3 +1,5 @@
{-# LANGUAGE QuasiQuotes #-}
{- |
Module : Spec.Stake
Maintainer : emi@haskell.fyi
@ -57,13 +59,13 @@ tests =
"stakeDepositWithdraw withdraw"
(stakeValidator Stake.stake)
(toDatum $ StakeDatum 100_000 signer)
(toDatum $ DepositWithdraw (negate 100_000))
(toDatum $ DepositWithdraw $ negate 100_000)
(Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 100_000})
, validatorFailsWith
"stakeDepositWithdraw negative GT"
(stakeValidator Stake.stake)
(toDatum $ StakeDatum 100_000 signer)
(toDatum $ DepositWithdraw (negate 1_000_000))
(toDatum $ DepositWithdraw 1_000_000)
(Stake.stakeDepositWithdraw $ DepositWithdrawExample {startAmount = 100_000, delta = negate 1_000_000})
]
]

View file

@ -121,7 +121,6 @@ library
Agora.AuthorityToken
Agora.MultiSig
Agora.SafeMoney
Agora.SafeMoney.QQ
Agora.Stake
Agora.Treasury
Agora.Governor

View file

@ -22,8 +22,8 @@ import Plutus.V1.Ledger.Api (DatumHash, PubKeyHash, ValidatorHash)
-}
newtype ResultTag = ResultTag {getResultTag :: Integer}
{- | The 'status' of the proposal. This is only useful for __actual__
state transitions, as opposed to time-based 'phases'.
{- | The "status" of the proposal. This is only useful for __actual__
state transitions, as opposed to time-based "phases".
If the proposal is 'VotingReady', for instance, that doesn't necessarily
mean that voting is possible, as this also requires the timing to be right.
@ -48,6 +48,7 @@ data ProposalStatus
-- TODO: The owner of the proposal may choose to reclaim their proposal.
Finished
-- | Haskell-level datum for Proposal scripts.
data ProposalDatum = ProposalDatum
{ -- TODO: could we encode this more efficiently?
-- This is shaped this way for future proofing.

View file

@ -7,7 +7,8 @@ Phantom-type protected types for handling money in Plutus.
-}
module Agora.SafeMoney (
-- * Types
PDiscrete,
PDiscrete (..),
Discrete (..),
-- * Tags and refs
AssetClassRef (..),
@ -23,15 +24,16 @@ module Agora.SafeMoney (
-- * Conversions
pdiscreteValue,
pvalueDiscrete,
discreteValue,
) where
import Prelude
--------------------------------------------------------------------------------
import Plutus.V1.Ledger.Api (BuiltinData (..), Data (..))
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
import PlutusTx.IsData.Class (FromData (..), ToData (..))
import Plutus.V1.Ledger.Value (AssetClass (AssetClass), Value)
import Plutus.V1.Ledger.Value qualified as Value
import PlutusTx qualified
import Plutarch.Api.V1 (PValue)
import Plutarch.Builtin ()
@ -63,22 +65,21 @@ newtype AssetClassRef (tag :: Type) = AssetClassRef {getAssetClass :: AssetClass
adaRef :: AssetClassRef ADATag
adaRef = AssetClassRef (AssetClass ("", ""))
{- | Represents a single asset in a 'Value' related to a particular 'AssetClass'
-- TODO: Currently it's possible to transmute from one discrete to another.
-- How do we prevent this?
--
-- @
-- transmute :: forall (a :: Type) (b :: Type). Discrete a -> Discrete b
-- transmute = Discrete . getDiscrete
-- @
{- | Represents a single asset in a 'Plutus.V1.Ledger.Value.Value' related to a particular 'AssetClass'
through 'AssetClassRef'.
-}
newtype Discrete (tag :: Type)
= Discrete Integer
newtype Discrete (tag :: Type) = Discrete {getDiscrete :: Integer}
deriving stock (Show, Eq)
{- We have to manually write these instances because the `tag` will confuse
`makeIsDataIndexed`.
-}
instance forall tag. FromData (Discrete tag) where
fromBuiltinData (BuiltinData (I x)) = Just (Discrete x)
fromBuiltinData _ = Nothing
instance forall tag. ToData (Discrete tag) where
toBuiltinData (Discrete x) = BuiltinData (I x)
deriving newtype (PlutusTx.ToData, PlutusTx.FromData, PlutusTx.UnsafeFromData)
deriving newtype (Num) -- TODO: Use plutarch-numeric
{- | Represents a single asset in a 'PValue' related to a particular 'AssetClass'
through 'AssetClassRef'.
@ -134,3 +135,11 @@ pdiscreteValue (AssetClassRef (AssetClass (cs, tn))) = phoistAcyclic $
# pconstant cs
# pconstant tn
# p
discreteValue ::
forall (tag :: Type).
AssetClassRef tag ->
Discrete tag ->
Value
discreteValue (AssetClassRef (AssetClass (cs, tn))) (Discrete v) =
Value.singleton cs tn v

View file

@ -1,96 +0,0 @@
{-# 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 (PDiscrete)
--------------------------------------------------------------------------------
{- | Generate 'PDiscrete' values tagged by a particular tag
@
[discrete| 123.456 'Agora.SafeMoney.ADA' |] :: 'Term' s ('PDiscrete' 'Agora.SafeMoney.ADA')
@
-}
discrete :: QuasiQuoter
discrete = QuasiQuoter discreteExp errorDiscretePat errorDiscreteType errorDiscreteDiscretelaration
discreteConstant :: forall tag s. Integer -> Term s (PDiscrete tag)
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 $ "Type 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."

View file

@ -54,6 +54,7 @@ import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
import Agora.SafeMoney (
AssetClassRef (..),
Discrete,
GTTag,
PDiscrete,
paddDiscrete,
@ -66,6 +67,7 @@ import Agora.Utils (
anyOutput,
paddValue,
passert,
passetClassValueOf',
pfindTxInByTxOutRef,
pgeqByClass,
pgeqByClass',
@ -100,7 +102,7 @@ data PStakeRedeemer (s :: S)
-- | Haskell-level redeemer for Stake scripts.
data StakeRedeemer
= -- | Deposit or withdraw a discrete amount of the staked governance token.
DepositWithdraw Integer
DepositWithdraw (Discrete GTTag)
| -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
Destroy
deriving stock (Show, GHC.Generic)
@ -121,8 +123,7 @@ newtype PStakeDatum (s :: S) = PStakeDatum
-- | Haskell-level datum for Stake scripts.
data StakeDatum = StakeDatum
{ -- FIXME: This needs to be gt
stakedAmount :: Integer
{ stakedAmount :: Discrete GTTag
, owner :: PubKeyHash
}
deriving stock (Show, GHC.Generic)
@ -306,6 +307,9 @@ stakeValidator stake =
]
let expectedValue = paddValue # continuingValue # (pdiscreteValue stake.gtClassRef # delta)
ptrace (pshow $ passetClassValueOf' stake.gtClassRef.getAssetClass # value)
ptrace (pshow $ passetClassValueOf' stake.gtClassRef.getAssetClass # expectedValue)
-- TODO: Same as above. This is quite inefficient now, as it does two lookups
-- instead of a more efficient single pass,
-- but it doesn't really matter for this. At least it's correct.

View file

@ -1,8 +0,0 @@
{- |
Module : Agora.Voting
Maintainer : emi@haskell.fyi
Description: Types for votes and vote counting
-}
module Agora.Voting (
Vote (..),
) where