migrate Haskell-level datums to use Discrete

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

View file

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

View file

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

View file

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

View file

@ -22,8 +22,8 @@ import Plutus.V1.Ledger.Api (DatumHash, PubKeyHash, ValidatorHash)
-} -}
newtype ResultTag = ResultTag {getResultTag :: Integer} newtype ResultTag = ResultTag {getResultTag :: Integer}
{- | The 'status' of the proposal. This is only useful for __actual__ {- | The "status" of the proposal. This is only useful for __actual__
state transitions, as opposed to time-based 'phases'. state transitions, as opposed to time-based "phases".
If the proposal is 'VotingReady', for instance, that doesn't necessarily 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. 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. -- TODO: The owner of the proposal may choose to reclaim their proposal.
Finished Finished
-- | Haskell-level datum for Proposal scripts.
data ProposalDatum = ProposalDatum data ProposalDatum = ProposalDatum
{ -- TODO: could we encode this more efficiently? { -- TODO: could we encode this more efficiently?
-- This is shaped this way for future proofing. -- 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 ( module Agora.SafeMoney (
-- * Types -- * Types
PDiscrete, PDiscrete (..),
Discrete (..),
-- * Tags and refs -- * Tags and refs
AssetClassRef (..), AssetClassRef (..),
@ -23,15 +24,16 @@ module Agora.SafeMoney (
-- * Conversions -- * Conversions
pdiscreteValue, pdiscreteValue,
pvalueDiscrete, pvalueDiscrete,
discreteValue,
) where ) where
import Prelude import Prelude
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
import Plutus.V1.Ledger.Api (BuiltinData (..), Data (..)) import Plutus.V1.Ledger.Value (AssetClass (AssetClass), Value)
import Plutus.V1.Ledger.Value (AssetClass (AssetClass)) import Plutus.V1.Ledger.Value qualified as Value
import PlutusTx.IsData.Class (FromData (..), ToData (..)) import PlutusTx qualified
import Plutarch.Api.V1 (PValue) import Plutarch.Api.V1 (PValue)
import Plutarch.Builtin () import Plutarch.Builtin ()
@ -63,22 +65,21 @@ newtype AssetClassRef (tag :: Type) = AssetClassRef {getAssetClass :: AssetClass
adaRef :: AssetClassRef ADATag adaRef :: AssetClassRef ADATag
adaRef = AssetClassRef (AssetClass ("", "")) 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'. through 'AssetClassRef'.
-} -}
newtype Discrete (tag :: Type) newtype Discrete (tag :: Type) = Discrete {getDiscrete :: Integer}
= Discrete Integer
deriving stock (Show, Eq) deriving stock (Show, Eq)
deriving newtype (PlutusTx.ToData, PlutusTx.FromData, PlutusTx.UnsafeFromData)
{- We have to manually write these instances because the `tag` will confuse deriving newtype (Num) -- TODO: Use plutarch-numeric
`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)
{- | Represents a single asset in a 'PValue' related to a particular 'AssetClass' {- | Represents a single asset in a 'PValue' related to a particular 'AssetClass'
through 'AssetClassRef'. through 'AssetClassRef'.
@ -134,3 +135,11 @@ pdiscreteValue (AssetClassRef (AssetClass (cs, tn))) = phoistAcyclic $
# pconstant cs # pconstant cs
# pconstant tn # pconstant tn
# p # 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 ( import Agora.SafeMoney (
AssetClassRef (..), AssetClassRef (..),
Discrete,
GTTag, GTTag,
PDiscrete, PDiscrete,
paddDiscrete, paddDiscrete,
@ -66,6 +67,7 @@ import Agora.Utils (
anyOutput, anyOutput,
paddValue, paddValue,
passert, passert,
passetClassValueOf',
pfindTxInByTxOutRef, pfindTxInByTxOutRef,
pgeqByClass, pgeqByClass,
pgeqByClass', pgeqByClass',
@ -100,7 +102,7 @@ data PStakeRedeemer (s :: S)
-- | Haskell-level redeemer for Stake scripts. -- | Haskell-level redeemer for Stake scripts.
data StakeRedeemer data StakeRedeemer
= -- | Deposit or withdraw a discrete amount of the staked governance token. = -- | 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 a stake, retrieving its LQ, the minimum ADA and any other assets.
Destroy Destroy
deriving stock (Show, GHC.Generic) deriving stock (Show, GHC.Generic)
@ -121,8 +123,7 @@ newtype PStakeDatum (s :: S) = PStakeDatum
-- | Haskell-level datum for Stake scripts. -- | Haskell-level datum for Stake scripts.
data StakeDatum = StakeDatum data StakeDatum = StakeDatum
{ -- FIXME: This needs to be gt { stakedAmount :: Discrete GTTag
stakedAmount :: Integer
, owner :: PubKeyHash , owner :: PubKeyHash
} }
deriving stock (Show, GHC.Generic) deriving stock (Show, GHC.Generic)
@ -306,6 +307,9 @@ stakeValidator stake =
] ]
let expectedValue = paddValue # continuingValue # (pdiscreteValue stake.gtClassRef # delta) 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 -- TODO: Same as above. This is quite inefficient now, as it does two lookups
-- instead of a more efficient single pass, -- instead of a more efficient single pass,
-- but it doesn't really matter for this. At least it's correct. -- 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