Sulkta-OSS/agora
3
0
Fork 0
Code Issues 1 Pull requests Projects Releases Packages Wiki Activity Actions

rework SafeMoney to use tags instead of MoneyClass

Browse source
This commit is contained in:
Emily Martins 2022-03-26 11:52:52 +01:00
parent 7e780d994c
commit dee3de0a73
5 changed files with 89 additions and 121 deletions
Download patch file Download diff file Expand all files Collapse all files

2
Makefile
View file

@ -12,7 +12,7 @@ usage:
@echo " haddock -- Generate Haddock docs for project" @echo " haddock -- Generate Haddock docs for project"
hoogle: hoogle:
pkill hoogle pkill hoogle || true
hoogle generate --local=haddock --database=hoo/local.hoo hoogle generate --local=haddock --database=hoo/local.hoo
hoogle server --local -p 8081 >> /dev/null & hoogle server --local -p 8081 >> /dev/null &
hoogle server --local --database=hoo/local.hoo -p 8082 >> /dev/null & hoogle server --local --database=hoo/local.hoo -p 8082 >> /dev/null &

15
agora-test/Spec/Sample/Stake.hs
View file

@ -47,7 +47,7 @@ import Plutus.V1.Ledger.Api (
import Plutus.V1.Ledger.Contexts (TxOut (TxOut), TxOutRef (TxOutRef)) import Plutus.V1.Ledger.Contexts (TxOut (TxOut), TxOutRef (TxOutRef))
import Plutus.V1.Ledger.Interval qualified as Interval import Plutus.V1.Ledger.Interval qualified as Interval
import Plutus.V1.Ledger.Scripts (Validator) import Plutus.V1.Ledger.Scripts (Validator)
import Plutus.V1.Ledger.Value (TokenName (TokenName)) import Plutus.V1.Ledger.Value (AssetClass (AssetClass), TokenName (TokenName))
import Plutus.V1.Ledger.Value qualified as Value import Plutus.V1.Ledger.Value qualified as Value
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
@ -59,8 +59,17 @@ import Spec.Util (datumPair, toDatumHash)
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- | 'Stake' parameters for 'LQ'. -- | 'Stake' parameters for 'LQ'.
stake :: Stake LQ stake :: Stake
stake = Stake stake =
Stake
{ gtClassRef =
AssetClassRef
( AssetClass
( "da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
, "LQ"
)
)
}
-- | 'Stake' policy instance. -- | 'Stake' policy instance.
policy :: MintingPolicy policy :: MintingPolicy

105
agora/Agora/SafeMoney.hs
View file

@ -7,9 +7,14 @@ Phantom-type protected types for handling money in Plutus.
-} -}
module Agora.SafeMoney ( module Agora.SafeMoney (
-- * Types -- * Types
MoneyClass,
PDiscrete, PDiscrete,
-- * Tags and refs
AssetClassRef (..),
ADATag,
GTTag,
adaRef,
-- * Utility functions -- * Utility functions
paddDiscrete, paddDiscrete,
pgeqDiscrete, pgeqDiscrete,
@ -18,24 +23,14 @@ module Agora.SafeMoney (
-- * Conversions -- * Conversions
pdiscreteValue, pdiscreteValue,
pvalueDiscrete, pvalueDiscrete,
-- * Example MoneyClasses
LQ,
ADA,
) where ) where
import Data.Proxy (Proxy (Proxy))
import Data.String
import GHC.TypeLits (
KnownSymbol,
Nat,
Symbol,
symbolVal,
)
import Prelude import Prelude
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
import Plutarch.Api.V1 (PValue) import Plutarch.Api.V1 (PValue)
import Plutarch.Builtin () import Plutarch.Builtin ()
import Plutarch.Internal () import Plutarch.Internal ()
@ -43,39 +38,46 @@ import Plutarch.Monadic qualified as P
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
import Agora.Utils (passetClassValueOf, psingletonValue) import Agora.Utils (
passetClassValueOf',
psingletonValue,
)
--------------------------------------------------------------------------------
-- Example tags
-- | Governance token
data GTTag
-- | ADA
data ADATag
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- | Type-level unique identifier for an 'Plutus.V1.Ledger.Value.AssetClass' -- | A tagged AssetClass. Use to resolve a reference inside of a PDiscrete
type MoneyClass = data AssetClassRef (tag :: Type) = AssetClassRef {getAssetClass :: AssetClass}
( -- AssetClass
Symbol
, -- TokenName
Symbol
, -- Decimal places
Nat
)
-- | A 'PDiscrete' amount of currency tagged on the type level with the 'MoneyClass' it belongs to adaRef :: AssetClassRef ADATag
newtype PDiscrete (mc :: MoneyClass) (s :: S) adaRef = AssetClassRef (AssetClass ("", ""))
newtype PDiscrete (tag :: Type) (s :: S)
= PDiscrete (Term s PInteger) = PDiscrete (Term s PInteger)
deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (PDiscrete mc) PInteger) deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (PDiscrete tag) PInteger)
-- | Check if one 'PDiscrete' is greater than another. -- | Check if one 'PDiscrete' is greater than another.
pgeqDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc :--> PDiscrete mc :--> PBool) pgeqDiscrete :: forall (tag :: Type) (s :: S). Term s (PDiscrete tag :--> PDiscrete tag :--> PBool)
pgeqDiscrete = phoistAcyclic $ pgeqDiscrete = phoistAcyclic $
plam $ \x y -> P.do plam $ \x y -> P.do
PDiscrete x' <- pmatch x PDiscrete x' <- pmatch x
PDiscrete y' <- pmatch y PDiscrete y' <- pmatch y
y' #<= x' y' #<= x'
-- | Returns a zero-value 'PDiscrete' unit for any 'MoneyClass'. -- | Returns a zero-value 'PDiscrete' unit for any tag.
pzeroDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc) pzeroDiscrete :: forall (tag :: Type) (s :: S). Term s (PDiscrete tag)
pzeroDiscrete = phoistAcyclic $ pcon (PDiscrete 0) pzeroDiscrete = phoistAcyclic $ pcon (PDiscrete 0)
-- | Add two 'PDiscrete' values of the same 'MoneyClass'. -- | Add two 'PDiscrete' values of the same tag.
paddDiscrete :: Term s (PDiscrete mc :--> PDiscrete mc :--> PDiscrete mc) paddDiscrete :: forall (tag :: Type) (s :: S). Term s (PDiscrete tag :--> PDiscrete tag :--> PDiscrete tag)
paddDiscrete = phoistAcyclic $ paddDiscrete = phoistAcyclic $
-- In the future, this should use plutarch-numeric -- In the future, this should use plutarch-numeric
plam $ \x y -> P.do plam $ \x y -> P.do
@ -83,46 +85,29 @@ paddDiscrete = phoistAcyclic $
PDiscrete y' <- pmatch y PDiscrete y' <- pmatch y
pcon (PDiscrete $ x' + y') pcon (PDiscrete $ x' + y')
-- | The MoneyClass of LQ.
type LQ :: MoneyClass
type LQ = '("da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24", "LQ", 6)
-- | The MoneyClass of ADA.
type ADA :: MoneyClass
type ADA = '("", "", 6)
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- | Downcast a `PValue` to a `PDiscrete` unit. -- | Downcast a `PValue` to a `PDiscrete` unit.
pvalueDiscrete :: pvalueDiscrete ::
forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s. forall (tag :: Type) (s :: S).
( KnownSymbol ac AssetClassRef tag ->
, KnownSymbol n Term s (PValue :--> PDiscrete tag)
, moneyClass ~ '(ac, n, scale) pvalueDiscrete (AssetClassRef ac) = phoistAcyclic $
) =>
Term s (PValue :--> PDiscrete moneyClass)
pvalueDiscrete = phoistAcyclic $
plam $ \f -> plam $ \f ->
pcon . PDiscrete $ pcon . PDiscrete $ passetClassValueOf' ac # f
passetClassValueOf # pconstant (fromString $ symbolVal $ Proxy @ac)
# pconstant (fromString $ symbolVal $ Proxy @n)
# f
{- | Get a `PValue` from a `PDiscrete`. {- | Get a `PValue` from a `PDiscrete`.
__NOTE__: `pdiscreteValue` after `pvalueDiscrete` is not a round-trip. __NOTE__: `pdiscreteValue` after `pvalueDiscrete` is not a round-trip.
It filters for a particular 'MoneyClass'. It filters for a particular tag.
-} -}
pdiscreteValue :: pdiscreteValue ::
forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s. forall (tag :: Type) (s :: S).
( KnownSymbol ac AssetClassRef tag ->
, KnownSymbol n Term s (PDiscrete tag :--> PValue)
, moneyClass ~ '(ac, n, scale) pdiscreteValue (AssetClassRef (AssetClass (cs, tn))) = phoistAcyclic $
) =>
Term s (PDiscrete moneyClass :--> PValue)
pdiscreteValue = phoistAcyclic $
plam $ \f -> pmatch f $ \case plam $ \f -> pmatch f $ \case
PDiscrete p -> PDiscrete p ->
psingletonValue psingletonValue
# pconstant (fromString $ symbolVal $ Proxy @ac) # pconstant cs
# pconstant (fromString $ symbolVal $ Proxy @n) # pconstant tn
# p # p

8
agora/Agora/SafeMoney/QQ.hs
View file

@ -33,11 +33,11 @@ import Prelude
import Plutarch.Internal (punsafeCoerce) import Plutarch.Internal (punsafeCoerce)
import Agora.SafeMoney (MoneyClass, PDiscrete) import Agora.SafeMoney (PDiscrete)
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
{- | Generate 'PDiscrete' values tagged by a particular MoneyClass {- | Generate 'PDiscrete' values tagged by a particular tag
@ @
[discrete| 123.456 'Agora.SafeMoney.ADA' |] :: 'Term' s ('PDiscrete' 'Agora.SafeMoney.ADA') [discrete| 123.456 'Agora.SafeMoney.ADA' |] :: 'Term' s ('PDiscrete' 'Agora.SafeMoney.ADA')
@ -46,7 +46,7 @@ import Agora.SafeMoney (MoneyClass, PDiscrete)
discrete :: QuasiQuoter discrete :: QuasiQuoter
discrete = QuasiQuoter discreteExp errorDiscretePat errorDiscreteType errorDiscreteDiscretelaration discrete = QuasiQuoter discreteExp errorDiscretePat errorDiscreteType errorDiscreteDiscretelaration
discreteConstant :: forall (moneyClass :: MoneyClass) s. Integer -> Term s (PDiscrete moneyClass) discreteConstant :: forall tag s. Integer -> Term s (PDiscrete tag)
discreteConstant n = punsafeCoerce (pconstant n :: Term s PInteger) discreteConstant n = punsafeCoerce (pconstant n :: Term s PInteger)
fixedToInteger :: Integer -> (Integer, Integer) -> Integer fixedToInteger :: Integer -> (Integer, Integer) -> Integer
@ -68,7 +68,7 @@ discreteExp s = case parseDiscreteRatioExp s of
Just (num, mc) -> do Just (num, mc) -> do
mcName <- mcName <-
lookupTypeName mc >>= \case lookupTypeName mc >>= \case
Nothing -> fail $ "MoneyClass with the name " <> show mc <> " is not in scope." Nothing -> fail $ "Type with the name " <> show mc <> " is not in scope."
Just v -> pure v Just v -> pure v
reified <- reify mcName reified <- reify mcName
case reified of case reified of

80
agora/Agora/Stake.hs
View file

@ -20,13 +20,7 @@ module Agora.Stake (
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
import Data.Proxy (Proxy (Proxy))
import Data.String (IsString (fromString))
import GHC.Generics qualified as GHC import GHC.Generics qualified as GHC
import GHC.TypeLits (
KnownSymbol,
symbolVal,
)
import Generics.SOP (Generic, I (I)) import Generics.SOP (Generic, I (I))
import Prelude import Prelude
@ -59,7 +53,8 @@ import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
import Agora.SafeMoney ( import Agora.SafeMoney (
MoneyClass, AssetClassRef (..),
GTTag,
PDiscrete, PDiscrete,
paddDiscrete, paddDiscrete,
pdiscreteValue, pdiscreteValue,
@ -84,12 +79,15 @@ import Agora.Utils (
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- | Parameters for creating Stake scripts. -- | Parameters for creating Stake scripts.
data Stake (gt :: MoneyClass) = Stake data Stake = Stake
{ gtClassRef :: AssetClassRef GTTag
-- ^ Resolve governance token
}
-- | Plutarch-level redeemer for Stake scripts. -- | Plutarch-level redeemer for Stake scripts.
data PStakeRedeemer (gt :: MoneyClass) (s :: S) data PStakeRedeemer (s :: S)
= -- | Deposit or withdraw a discrete amount of the staked governance token. = -- | Deposit or withdraw a discrete amount of the staked governance token.
PDepositWithdraw (Term s (PDataRecord '["delta" ':= PDiscrete gt])) PDepositWithdraw (Term s (PDataRecord '["delta" ':= PDiscrete 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.
PDestroy (Term s (PDataRecord '[])) PDestroy (Term s (PDataRecord '[]))
deriving stock (GHC.Generic) deriving stock (GHC.Generic)
@ -97,13 +95,7 @@ data PStakeRedeemer (gt :: MoneyClass) (s :: S)
deriving anyclass (PIsDataRepr) deriving anyclass (PIsDataRepr)
deriving deriving
(PlutusType, PIsData) (PlutusType, PIsData)
via PIsDataReprInstances (PStakeRedeemer gt) via PIsDataReprInstances PStakeRedeemer
-- FIXME: 'StakeRedeemer' and 'StakeDatum' are stripped of their
-- typesafe `PDiscrete` equivalent due to issues with `makeIsDataIndexed`
-- when using the kind @gt :: MoneyClass@. This ought to be fixed with
-- a future patch in Plutarch upstream. For now, we will deal with lower
-- type safety off-chain.
-- | Haskell-level redeemer for Stake scripts. -- | Haskell-level redeemer for Stake scripts.
data StakeRedeemer data StakeRedeemer
@ -116,16 +108,16 @@ data StakeRedeemer
PlutusTx.makeIsDataIndexed ''StakeRedeemer [('DepositWithdraw, 0), ('Destroy, 1)] PlutusTx.makeIsDataIndexed ''StakeRedeemer [('DepositWithdraw, 0), ('Destroy, 1)]
-- | Plutarch-level datum for Stake scripts. -- | Plutarch-level datum for Stake scripts.
newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum newtype PStakeDatum (s :: S) = PStakeDatum
{ getStakeDatum :: { getStakeDatum ::
Term s (PDataRecord '["stakedAmount" ':= PDiscrete gt, "owner" ':= PPubKeyHash]) Term s (PDataRecord '["stakedAmount" ':= PDiscrete GTTag, "owner" ':= PPubKeyHash])
} }
deriving stock (GHC.Generic) deriving stock (GHC.Generic)
deriving anyclass (Generic) deriving anyclass (Generic)
deriving anyclass (PIsDataRepr) deriving anyclass (PIsDataRepr)
deriving deriving
(PlutusType, PIsData, PDataFields) (PlutusType, PIsData, PDataFields)
via (PIsDataReprInstances (PStakeDatum gt)) via (PIsDataReprInstances PStakeDatum)
-- | Haskell-level datum for Stake scripts. -- | Haskell-level datum for Stake scripts.
data StakeDatum = StakeDatum data StakeDatum = StakeDatum
@ -154,14 +146,10 @@ PlutusTx.makeIsDataIndexed ''StakeDatum [('StakeDatum, 0)]
-- | Policy for Stake state threads. -- | Policy for Stake state threads.
stakePolicy :: stakePolicy ::
forall (gt :: MoneyClass) ac n scale s. forall (s :: S).
( KnownSymbol ac Stake ->
, KnownSymbol n
, gt ~ '(ac, n, scale)
) =>
Stake gt ->
Term s PMintingPolicy Term s PMintingPolicy
stakePolicy _stake = stakePolicy stake =
plam $ \_redeemer ctx' -> P.do plam $ \_redeemer ctx' -> P.do
ctx <- pletFields @'["txInfo", "purpose"] ctx' ctx <- pletFields @'["txInfo", "purpose"] ctx'
txInfo' <- plet ctx.txInfo txInfo' <- plet ctx.txInfo
@ -180,7 +168,7 @@ stakePolicy _stake =
mintedST #== -1 mintedST #== -1
passert "An unlocked input existed containing an ST" $ passert "An unlocked input existed containing an ST" $
anyInput @(PStakeDatum gt) # pfromData txInfo' anyInput @PStakeDatum # pfromData txInfo'
#$ plam #$ plam
$ \value _ stakeDatum' -> P.do $ \value _ stakeDatum' -> P.do
let hasST = psymbolValueOf # ownSymbol # value #== 1 let hasST = psymbolValueOf # ownSymbol # value #== 1
@ -197,7 +185,7 @@ stakePolicy _stake =
mintedST #== 1 mintedST #== 1
passert "A UTXO must exist with the correct output" $ passert "A UTXO must exist with the correct output" $
anyOutput @(PStakeDatum gt) # pfromData txInfo' anyOutput @PStakeDatum # pfromData txInfo'
#$ plam #$ plam
$ \value address stakeDatum' -> P.do $ \value address stakeDatum' -> P.do
let cred = pfield @"credential" # address let cred = pfield @"credential" # address
@ -220,7 +208,7 @@ stakePolicy _stake =
# 1 # 1
let expectedValue = let expectedValue =
paddValue paddValue
# (pdiscreteValue # stakeDatum.stakedAmount) # (pdiscreteValue stake.gtClassRef # stakeDatum.stakedAmount)
# stValue # stValue
let ownerSignsTransaction = let ownerSignsTransaction =
ptxSignedBy ptxSignedBy
@ -234,12 +222,7 @@ stakePolicy _stake =
foldr1 foldr1
(#&&) (#&&)
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
, pgeqByClass' , pgeqByClass' stake.gtClassRef.getAssetClass
( AssetClass
( fromString . symbolVal $ Proxy @ac
, fromString . symbolVal $ Proxy @n
)
)
# value # value
# expectedValue # expectedValue
, pgeqByClass , pgeqByClass
@ -259,12 +242,8 @@ stakePolicy _stake =
-- | Validator intended for Stake UTXOs to live in. -- | Validator intended for Stake UTXOs to live in.
stakeValidator :: stakeValidator ::
forall (gt :: MoneyClass) ac n scale s. forall (s :: S).
( KnownSymbol ac Stake ->
, KnownSymbol n
, gt ~ '(ac, n, scale)
) =>
Stake gt ->
Term s PValidator Term s PValidator
stakeValidator stake = stakeValidator stake =
plam $ \datum redeemer ctx' -> P.do plam $ \datum redeemer ctx' -> P.do
@ -273,9 +252,9 @@ stakeValidator stake =
txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo' txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
-- Coercion is safe in that if coercion fails we crash hard. -- Coercion is safe in that if coercion fails we crash hard.
let stakeRedeemer :: Term _ (PStakeRedeemer gt) let stakeRedeemer :: Term _ PStakeRedeemer
stakeRedeemer = pfromData $ punsafeCoerce redeemer stakeRedeemer = pfromData $ punsafeCoerce redeemer
stakeDatum' :: Term _ (PStakeDatum gt) stakeDatum' :: Term _ PStakeDatum
stakeDatum' = pfromData $ punsafeCoerce datum stakeDatum' = pfromData $ punsafeCoerce datum
stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum' stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
@ -310,7 +289,7 @@ stakeValidator stake =
"Owner signs this transaction" "Owner signs this transaction"
ownerSignsTransaction ownerSignsTransaction
passert "A UTXO must exist with the correct output" $ passert "A UTXO must exist with the correct output" $
anyOutput @(PStakeDatum gt) # txInfo' anyOutput @PStakeDatum # txInfo'
#$ plam #$ plam
$ \value address newStakeDatum' -> P.do $ \value address newStakeDatum' -> P.do
newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum' newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum'
@ -325,7 +304,7 @@ stakeValidator stake =
-- do we need to check this, really? -- do we need to check this, really?
pgeqDiscrete # (pfromData newStakeDatum.stakedAmount) # pzeroDiscrete pgeqDiscrete # (pfromData newStakeDatum.stakedAmount) # pzeroDiscrete
] ]
let expectedValue = paddValue # continuingValue # (pdiscreteValue # delta) let expectedValue = paddValue # continuingValue # (pdiscreteValue stake.gtClassRef # delta)
-- 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,
@ -334,12 +313,7 @@ stakeValidator stake =
foldr1 foldr1
(#&&) (#&&)
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue [ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
, pgeqByClass' , pgeqByClass' stake.gtClassRef.getAssetClass
( AssetClass
( fromString . symbolVal $ Proxy @ac
, fromString . symbolVal $ Proxy @n
)
)
# value # value
# expectedValue # expectedValue
, pgeqBySymbol , pgeqBySymbol
@ -360,7 +334,7 @@ stakeValidator stake =
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
-- | Check whether a Stake is locked. If it is locked, various actions are unavailable. -- | Check whether a Stake is locked. If it is locked, various actions are unavailable.
stakeLocked :: forall (gt :: MoneyClass) s. Term s (PStakeDatum gt :--> PBool) stakeLocked :: forall (s :: S). Term s (PStakeDatum :--> PBool)
stakeLocked = phoistAcyclic $ stakeLocked = phoistAcyclic $
plam $ \_stakeDatum -> plam $ \_stakeDatum ->
-- TODO: when we extend this to support proposals, this will need to do something -- TODO: when we extend this to support proposals, this will need to do something