use plutarch-safemoney instead of local Agora.SafeMoney
This commit is contained in:
Emily Martins
parent
281926b67b
commit
8c9225c1f1
7 changed files with 75 additions and 179 deletions
|
|
@ -38,7 +38,8 @@ import PlutusTx qualified
|
|||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Agora.SafeMoney (Discrete, GTTag, PDiscrete)
|
||||
import Agora.SafeMoney (GTTag)
|
||||
import Plutarch.SafeMoney (PDiscrete, Tagged)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Haskell-land
|
||||
|
|
@ -92,11 +93,11 @@ PlutusTx.makeIsDataIndexed ''ProposalStatus [('Draft, 0), ('VotingReady, 1), ('F
|
|||
to 'Proposal's when they are created.
|
||||
-}
|
||||
data ProposalThresholds = ProposalThresholds
|
||||
{ execute :: Discrete GTTag
|
||||
{ execute :: Tagged GTTag Integer
|
||||
-- ^ How much GT minimum must a particular 'ResultTag' accumulate for it to pass.
|
||||
, draft :: Discrete GTTag
|
||||
, draft :: Tagged GTTag Integer
|
||||
-- ^ How much GT required to "create" a proposal.
|
||||
, vote :: Discrete GTTag
|
||||
, vote :: Tagged GTTag Integer
|
||||
-- ^ How much GT required to allow voting to happen.
|
||||
-- (i.e. to move into 'VotingReady')
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,51 +1,21 @@
|
|||
{- |
|
||||
Module : Agora.SafeMoney
|
||||
Maintainer : emi@haskell.fyi
|
||||
Description: Phantom-type protected types for handling money in Plutus.
|
||||
Description: Tags and bonuses for Plutarch.SafeMoney.
|
||||
|
||||
Phantom-type protected types for handling money in Plutus.
|
||||
Tags and bonuses for "Plutarch.SafeMoney".
|
||||
-}
|
||||
module Agora.SafeMoney (
|
||||
-- * Types
|
||||
PDiscrete (..),
|
||||
Discrete (..),
|
||||
|
||||
-- * Tags and refs
|
||||
AssetClassRef (..),
|
||||
ADATag,
|
||||
GTTag,
|
||||
adaRef,
|
||||
|
||||
-- * Utility functions
|
||||
paddDiscrete,
|
||||
pgeqDiscrete,
|
||||
pzeroDiscrete,
|
||||
|
||||
-- * Conversions
|
||||
pdiscreteValue,
|
||||
pvalueDiscrete,
|
||||
discreteValue,
|
||||
) where
|
||||
|
||||
import Prelude
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Plutus.V1.Ledger.Value (AssetClass (AssetClass), Value)
|
||||
import Plutus.V1.Ledger.Value qualified as Value
|
||||
import PlutusTx qualified
|
||||
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
|
||||
|
||||
import Plutarch.Api.V1 (PValue)
|
||||
import Plutarch.Builtin ()
|
||||
import Plutarch.Internal ()
|
||||
import Plutarch.Monadic qualified as P
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Agora.Utils (
|
||||
passetClassValueOf',
|
||||
psingletonValue,
|
||||
)
|
||||
import Plutarch.SafeMoney
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Example tags
|
||||
|
|
@ -58,89 +28,6 @@ data ADATag
|
|||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | A tagged AssetClass. Use to resolve a reference inside of a PDiscrete
|
||||
newtype AssetClassRef (tag :: Type) = AssetClassRef {getAssetClass :: AssetClass}
|
||||
|
||||
-- | Resolves ada tags.
|
||||
adaRef :: AssetClassRef ADATag
|
||||
adaRef = AssetClassRef (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 {getDiscrete :: Integer}
|
||||
deriving stock (Show, Eq)
|
||||
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'.
|
||||
-}
|
||||
newtype PDiscrete (tag :: Type) (s :: S)
|
||||
= PDiscrete (Term s PInteger)
|
||||
deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (PDiscrete tag) PInteger)
|
||||
|
||||
-- | Check if one 'PDiscrete' is greater than another.
|
||||
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 tag.
|
||||
pzeroDiscrete :: forall (tag :: Type) (s :: S). Term s (PDiscrete tag)
|
||||
pzeroDiscrete = phoistAcyclic $ pcon (PDiscrete 0)
|
||||
|
||||
-- | 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
|
||||
PDiscrete x' <- pmatch x
|
||||
PDiscrete y' <- pmatch y
|
||||
pcon (PDiscrete $ x' + y')
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | Downcast a `PValue` to a `PDiscrete` unit.
|
||||
pvalueDiscrete ::
|
||||
forall (tag :: Type) (s :: S).
|
||||
AssetClassRef tag ->
|
||||
Term s (PValue :--> PDiscrete tag)
|
||||
pvalueDiscrete (AssetClassRef ac) = phoistAcyclic $
|
||||
plam $ \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 tag.
|
||||
-}
|
||||
pdiscreteValue ::
|
||||
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 cs
|
||||
# pconstant tn
|
||||
# p
|
||||
|
||||
-- | Get a `Value` from a `Discrete`.
|
||||
discreteValue ::
|
||||
forall (tag :: Type).
|
||||
AssetClassRef tag ->
|
||||
Discrete tag ->
|
||||
Value
|
||||
discreteValue (AssetClassRef (AssetClass (cs, tn))) (Discrete v) =
|
||||
Value.singleton cs tn v
|
||||
adaRef :: Tagged ADATag AssetClass
|
||||
adaRef = Tagged (AssetClass ("", ""))
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ module Agora.Stake (
|
|||
|
||||
import GHC.Generics qualified as GHC
|
||||
import Generics.SOP (Generic, I (I))
|
||||
import Prelude
|
||||
import Prelude hiding (Num (..))
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
|
@ -52,16 +52,7 @@ import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
|
|||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Agora.SafeMoney (
|
||||
AssetClassRef (..),
|
||||
Discrete,
|
||||
GTTag,
|
||||
PDiscrete,
|
||||
paddDiscrete,
|
||||
pdiscreteValue,
|
||||
pgeqDiscrete,
|
||||
pzeroDiscrete,
|
||||
)
|
||||
import Agora.SafeMoney (GTTag)
|
||||
import Agora.Utils (
|
||||
anyInput,
|
||||
anyOutput,
|
||||
|
|
@ -77,38 +68,41 @@ import Agora.Utils (
|
|||
ptxSignedBy,
|
||||
pvalueSpent,
|
||||
)
|
||||
import Plutarch.Numeric
|
||||
import Plutarch.SafeMoney (
|
||||
PDiscrete,
|
||||
Tagged (..),
|
||||
pdiscreteValue,
|
||||
untag,
|
||||
)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | Parameters for creating Stake scripts.
|
||||
newtype Stake = Stake
|
||||
{ gtClassRef :: AssetClassRef GTTag
|
||||
{ gtClassRef :: Tagged GTTag AssetClass
|
||||
-- ^ Used when inlining the AssetClass of a 'PDiscrete' in the script code.
|
||||
}
|
||||
|
||||
-- | Plutarch-level redeemer for Stake scripts.
|
||||
data PStakeRedeemer (s :: S)
|
||||
= -- | Deposit or withdraw a discrete amount of the staked governance token.
|
||||
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)
|
||||
deriving anyclass (Generic)
|
||||
deriving anyclass (PIsDataRepr)
|
||||
deriving
|
||||
(PlutusType, PIsData)
|
||||
via PIsDataReprInstances PStakeRedeemer
|
||||
|
||||
-- | Haskell-level redeemer for Stake scripts.
|
||||
data StakeRedeemer
|
||||
= -- | Deposit or withdraw a discrete amount of the staked governance token.
|
||||
DepositWithdraw (Discrete GTTag)
|
||||
DepositWithdraw (Tagged GTTag Integer)
|
||||
| -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
|
||||
Destroy
|
||||
deriving stock (Show, GHC.Generic)
|
||||
|
||||
PlutusTx.makeIsDataIndexed ''StakeRedeemer [('DepositWithdraw, 0), ('Destroy, 1)]
|
||||
|
||||
-- | Haskell-level datum for Stake scripts.
|
||||
data StakeDatum = StakeDatum
|
||||
{ stakedAmount :: Tagged GTTag Integer
|
||||
, owner :: PubKeyHash
|
||||
}
|
||||
deriving stock (Show, GHC.Generic)
|
||||
|
||||
PlutusTx.makeIsDataIndexed ''StakeDatum [('StakeDatum, 0)]
|
||||
|
||||
-- | Plutarch-level datum for Stake scripts.
|
||||
newtype PStakeDatum (s :: S) = PStakeDatum
|
||||
{ getStakeDatum ::
|
||||
|
|
@ -121,14 +115,18 @@ newtype PStakeDatum (s :: S) = PStakeDatum
|
|||
(PlutusType, PIsData, PDataFields)
|
||||
via (PIsDataReprInstances PStakeDatum)
|
||||
|
||||
-- | Haskell-level datum for Stake scripts.
|
||||
data StakeDatum = StakeDatum
|
||||
{ stakedAmount :: Discrete GTTag
|
||||
, owner :: PubKeyHash
|
||||
}
|
||||
deriving stock (Show, GHC.Generic)
|
||||
|
||||
PlutusTx.makeIsDataIndexed ''StakeDatum [('StakeDatum, 0)]
|
||||
-- | Plutarch-level redeemer for Stake scripts.
|
||||
data PStakeRedeemer (s :: S)
|
||||
= -- | Deposit or withdraw a discrete amount of the staked governance token.
|
||||
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)
|
||||
deriving anyclass (Generic)
|
||||
deriving anyclass (PIsDataRepr)
|
||||
deriving
|
||||
(PlutusType, PIsData)
|
||||
via PIsDataReprInstances PStakeRedeemer
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
{- What this Policy does
|
||||
|
|
@ -223,7 +221,7 @@ stakePolicy stake =
|
|||
foldr1
|
||||
(#&&)
|
||||
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
|
||||
, pgeqByClass' stake.gtClassRef.getAssetClass
|
||||
, pgeqByClass' (untag stake.gtClassRef)
|
||||
# value
|
||||
# expectedValue
|
||||
, pgeqByClass
|
||||
|
|
@ -300,15 +298,15 @@ stakeValidator stake =
|
|||
foldr1
|
||||
(#&&)
|
||||
[ stakeDatum.owner #== newStakeDatum.owner
|
||||
, (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
|
||||
, (stakeDatum.stakedAmount + delta) #== newStakeDatum.stakedAmount
|
||||
, -- We can't magically conjure GT anyway (no input to spend!)
|
||||
-- do we need to check this, really?
|
||||
pgeqDiscrete # (pfromData newStakeDatum.stakedAmount) # pzeroDiscrete
|
||||
zero #<= pfromData newStakeDatum.stakedAmount
|
||||
]
|
||||
let expectedValue = paddValue # continuingValue # (pdiscreteValue stake.gtClassRef # delta)
|
||||
|
||||
ptrace (pshow $ passetClassValueOf' stake.gtClassRef.getAssetClass # value)
|
||||
ptrace (pshow $ passetClassValueOf' stake.gtClassRef.getAssetClass # expectedValue)
|
||||
ptrace (pshow $ passetClassValueOf' (untag stake.gtClassRef) # value)
|
||||
ptrace (pshow $ passetClassValueOf' (untag stake.gtClassRef) # expectedValue)
|
||||
|
||||
-- TODO: Same as above. This is quite inefficient now, as it does two lookups
|
||||
-- instead of a more efficient single pass,
|
||||
|
|
@ -317,7 +315,7 @@ stakeValidator stake =
|
|||
foldr1
|
||||
(#&&)
|
||||
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
|
||||
, pgeqByClass' stake.gtClassRef.getAssetClass
|
||||
, pgeqByClass' (untag stake.gtClassRef)
|
||||
# value
|
||||
# expectedValue
|
||||
, pgeqBySymbol
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue