Sulkta-Coop/agora
2
0
Fork 0
Code Issues 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 87ff8ba343
commit 8a98ec9ec3
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"
hoogle:
pkill hoogle
pkill hoogle || true
hoogle generate --local=haddock --database=hoo/local.hoo
hoogle server --local -p 8081 >> /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.Interval qualified as Interval
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
--------------------------------------------------------------------------------
@ -59,8 +59,17 @@ import Spec.Util (datumPair, toDatumHash)
--------------------------------------------------------------------------------
-- | 'Stake' parameters for 'LQ'.
stake :: Stake LQ
stake = Stake
stake :: Stake
stake =
Stake
{ gtClassRef =
AssetClassRef
( AssetClass
( "da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24"
, "LQ"
)
)
}
-- | 'Stake' policy instance.
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 (
-- * Types
MoneyClass,
PDiscrete,
-- * Tags and refs
AssetClassRef (..),
ADATag,
GTTag,
adaRef,
-- * Utility functions
paddDiscrete,
pgeqDiscrete,
@ -18,24 +23,14 @@ module Agora.SafeMoney (
-- * Conversions
pdiscreteValue,
pvalueDiscrete,
-- * Example MoneyClasses
LQ,
ADA,
) where
import Data.Proxy (Proxy (Proxy))
import Data.String
import GHC.TypeLits (
KnownSymbol,
Nat,
Symbol,
symbolVal,
)
import Prelude
--------------------------------------------------------------------------------
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
import Plutarch.Api.V1 (PValue)
import Plutarch.Builtin ()
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'
type MoneyClass =
( -- AssetClass
Symbol
, -- TokenName
Symbol
, -- Decimal places
Nat
)
-- | A tagged AssetClass. Use to resolve a reference inside of a PDiscrete
data AssetClassRef (tag :: Type) = AssetClassRef {getAssetClass :: AssetClass}
-- | A 'PDiscrete' amount of currency tagged on the type level with the 'MoneyClass' it belongs to
newtype PDiscrete (mc :: MoneyClass) (s :: S)
adaRef :: AssetClassRef ADATag
adaRef = AssetClassRef (AssetClass ("", ""))
newtype PDiscrete (tag :: Type) (s :: S)
= 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.
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 $
plam $ \x y -> P.do
PDiscrete x' <- pmatch x
PDiscrete y' <- pmatch y
y' #<= x'
-- | Returns a zero-value 'PDiscrete' unit for any 'MoneyClass'.
pzeroDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc)
-- | Returns a zero-value 'PDiscrete' unit for any tag.
pzeroDiscrete :: forall (tag :: Type) (s :: S). Term s (PDiscrete tag)
pzeroDiscrete = phoistAcyclic $ pcon (PDiscrete 0)
-- | Add two 'PDiscrete' values of the same 'MoneyClass'.
paddDiscrete :: Term s (PDiscrete mc :--> PDiscrete mc :--> PDiscrete mc)
-- | Add two 'PDiscrete' values of the same tag.
paddDiscrete :: forall (tag :: Type) (s :: S). Term s (PDiscrete tag :--> PDiscrete tag :--> PDiscrete tag)
paddDiscrete = phoistAcyclic $
-- In the future, this should use plutarch-numeric
plam $ \x y -> P.do
@ -83,46 +85,29 @@ paddDiscrete = phoistAcyclic $
PDiscrete y' <- pmatch 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.
pvalueDiscrete ::
forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
( KnownSymbol ac
, KnownSymbol n
, moneyClass ~ '(ac, n, scale)
) =>
Term s (PValue :--> PDiscrete moneyClass)
pvalueDiscrete = phoistAcyclic $
forall (tag :: Type) (s :: S).
AssetClassRef tag ->
Term s (PValue :--> PDiscrete tag)
pvalueDiscrete (AssetClassRef ac) = phoistAcyclic $
plam $ \f ->
pcon . PDiscrete $
passetClassValueOf # pconstant (fromString $ symbolVal $ Proxy @ac)
# pconstant (fromString $ symbolVal $ Proxy @n)
# f
pcon . PDiscrete $ passetClassValueOf' ac # f
{- | Get a `PValue` from a `PDiscrete`.
__NOTE__: `pdiscreteValue` after `pvalueDiscrete` is not a round-trip.
It filters for a particular 'MoneyClass'.
It filters for a particular tag.
-}
pdiscreteValue ::
forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
( KnownSymbol ac
, KnownSymbol n
, moneyClass ~ '(ac, n, scale)
) =>
Term s (PDiscrete moneyClass :--> PValue)
pdiscreteValue = phoistAcyclic $
forall (tag :: Type) (s :: S).
AssetClassRef tag ->
Term s (PDiscrete tag :--> PValue)
pdiscreteValue (AssetClassRef (AssetClass (cs, tn))) = phoistAcyclic $
plam $ \f -> pmatch f $ \case
PDiscrete p ->
psingletonValue
# pconstant (fromString $ symbolVal $ Proxy @ac)
# pconstant (fromString $ symbolVal $ Proxy @n)
# pconstant cs
# pconstant tn
# p

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

@ -33,11 +33,11 @@ import Prelude
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')
@ -46,7 +46,7 @@ import Agora.SafeMoney (MoneyClass, PDiscrete)
discrete :: QuasiQuoter
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)
fixedToInteger :: Integer -> (Integer, Integer) -> Integer
@ -68,7 +68,7 @@ discreteExp s = case parseDiscreteRatioExp s of
Just (num, mc) -> do
mcName <-
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
reified <- reify mcName
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.TypeLits (
KnownSymbol,
symbolVal,
)
import Generics.SOP (Generic, I (I))
import Prelude
@ -59,7 +53,8 @@ import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
--------------------------------------------------------------------------------
import Agora.SafeMoney (
MoneyClass,
AssetClassRef (..),
GTTag,
PDiscrete,
paddDiscrete,
pdiscreteValue,
@ -84,12 +79,15 @@ import Agora.Utils (
--------------------------------------------------------------------------------
-- | 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.
data PStakeRedeemer (gt :: MoneyClass) (s :: S)
data PStakeRedeemer (s :: S)
= -- | 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.
PDestroy (Term s (PDataRecord '[]))
deriving stock (GHC.Generic)
@ -97,13 +95,7 @@ data PStakeRedeemer (gt :: MoneyClass) (s :: S)
deriving anyclass (PIsDataRepr)
deriving
(PlutusType, PIsData)
via PIsDataReprInstances (PStakeRedeemer gt)
-- 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.
via PIsDataReprInstances PStakeRedeemer
-- | Haskell-level redeemer for Stake scripts.
data StakeRedeemer
@ -116,16 +108,16 @@ data StakeRedeemer
PlutusTx.makeIsDataIndexed ''StakeRedeemer [('DepositWithdraw, 0), ('Destroy, 1)]
-- | Plutarch-level datum for Stake scripts.
newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum
newtype PStakeDatum (s :: S) = PStakeDatum
{ getStakeDatum ::
Term s (PDataRecord '["stakedAmount" ':= PDiscrete gt, "owner" ':= PPubKeyHash])
Term s (PDataRecord '["stakedAmount" ':= PDiscrete GTTag, "owner" ':= PPubKeyHash])
}
deriving stock (GHC.Generic)
deriving anyclass (Generic)
deriving anyclass (PIsDataRepr)
deriving
(PlutusType, PIsData, PDataFields)
via (PIsDataReprInstances (PStakeDatum gt))
via (PIsDataReprInstances PStakeDatum)
-- | Haskell-level datum for Stake scripts.
data StakeDatum = StakeDatum
@ -154,14 +146,10 @@ PlutusTx.makeIsDataIndexed ''StakeDatum [('StakeDatum, 0)]
-- | Policy for Stake state threads.
stakePolicy ::
forall (gt :: MoneyClass) ac n scale s.
( KnownSymbol ac
, KnownSymbol n
, gt ~ '(ac, n, scale)
) =>
Stake gt ->
forall (s :: S).
Stake ->
Term s PMintingPolicy
stakePolicy _stake =
stakePolicy stake =
plam $ \_redeemer ctx' -> P.do
ctx <- pletFields @'["txInfo", "purpose"] ctx'
txInfo' <- plet ctx.txInfo
@ -180,7 +168,7 @@ stakePolicy _stake =
mintedST #== -1
passert "An unlocked input existed containing an ST" $
anyInput @(PStakeDatum gt) # pfromData txInfo'
anyInput @PStakeDatum # pfromData txInfo'
#$ plam
$ \value _ stakeDatum' -> P.do
let hasST = psymbolValueOf # ownSymbol # value #== 1
@ -197,7 +185,7 @@ stakePolicy _stake =
mintedST #== 1
passert "A UTXO must exist with the correct output" $
anyOutput @(PStakeDatum gt) # pfromData txInfo'
anyOutput @PStakeDatum # pfromData txInfo'
#$ plam
$ \value address stakeDatum' -> P.do
let cred = pfield @"credential" # address
@ -220,7 +208,7 @@ stakePolicy _stake =
# 1
let expectedValue =
paddValue
# (pdiscreteValue # stakeDatum.stakedAmount)
# (pdiscreteValue stake.gtClassRef # stakeDatum.stakedAmount)
# stValue
let ownerSignsTransaction =
ptxSignedBy
@ -234,12 +222,7 @@ stakePolicy _stake =
foldr1
(#&&)
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
, pgeqByClass'
( AssetClass
( fromString . symbolVal $ Proxy @ac
, fromString . symbolVal $ Proxy @n
)
)
, pgeqByClass' stake.gtClassRef.getAssetClass
# value
# expectedValue
, pgeqByClass
@ -259,12 +242,8 @@ stakePolicy _stake =
-- | Validator intended for Stake UTXOs to live in.
stakeValidator ::
forall (gt :: MoneyClass) ac n scale s.
( KnownSymbol ac
, KnownSymbol n
, gt ~ '(ac, n, scale)
) =>
Stake gt ->
forall (s :: S).
Stake ->
Term s PValidator
stakeValidator stake =
plam $ \datum redeemer ctx' -> P.do
@ -273,9 +252,9 @@ stakeValidator stake =
txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
-- Coercion is safe in that if coercion fails we crash hard.
let stakeRedeemer :: Term _ (PStakeRedeemer gt)
let stakeRedeemer :: Term _ PStakeRedeemer
stakeRedeemer = pfromData $ punsafeCoerce redeemer
stakeDatum' :: Term _ (PStakeDatum gt)
stakeDatum' :: Term _ PStakeDatum
stakeDatum' = pfromData $ punsafeCoerce datum
stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
@ -310,7 +289,7 @@ stakeValidator stake =
"Owner signs this transaction"
ownerSignsTransaction
passert "A UTXO must exist with the correct output" $
anyOutput @(PStakeDatum gt) # txInfo'
anyOutput @PStakeDatum # txInfo'
#$ plam
$ \value address newStakeDatum' -> P.do
newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum'
@ -325,7 +304,7 @@ stakeValidator stake =
-- do we need to check this, really?
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
-- instead of a more efficient single pass,
@ -334,12 +313,7 @@ stakeValidator stake =
foldr1
(#&&)
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
, pgeqByClass'
( AssetClass
( fromString . symbolVal $ Proxy @ac
, fromString . symbolVal $ Proxy @n
)
)
, pgeqByClass' stake.gtClassRef.getAssetClass
# value
# expectedValue
, pgeqBySymbol
@ -360,7 +334,7 @@ stakeValidator stake =
--------------------------------------------------------------------------------
-- | 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 $
plam $ \_stakeDatum ->
-- TODO: when we extend this to support proposals, this will need to do something