Merge branch 'master' into flake-update
This commit is contained in:
Emily Martins
commit
9c1a4c20bd
16 changed files with 662 additions and 196 deletions
|
|
@ -10,6 +10,7 @@ A basic N of M multisignature validation function.
|
|||
module Agora.MultiSig (
|
||||
validatedByMultisig,
|
||||
pvalidatedByMultisig,
|
||||
PMultiSig (..),
|
||||
MultiSig (..),
|
||||
) where
|
||||
|
||||
|
|
@ -47,7 +48,7 @@ data MultiSig = MultiSig
|
|||
-- ^ List of PubKeyHashes that must be present in the list of signatories.
|
||||
, minSigs :: Integer
|
||||
}
|
||||
deriving stock (GHC.Generic)
|
||||
deriving stock (GHC.Generic, Eq, Show)
|
||||
deriving anyclass (Generic)
|
||||
|
||||
PlutusTx.makeLift ''MultiSig
|
||||
|
|
|
|||
|
|
@ -9,10 +9,11 @@ module Agora.SafeMoney (
|
|||
-- * Types
|
||||
MoneyClass,
|
||||
PDiscrete,
|
||||
Discrete,
|
||||
|
||||
-- * Utility functions
|
||||
paddDiscrete,
|
||||
pgeqDiscrete,
|
||||
pzeroDiscrete,
|
||||
|
||||
-- * Conversions
|
||||
pdiscreteValue,
|
||||
|
|
@ -42,11 +43,11 @@ import Plutarch.Monadic qualified as P
|
|||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Agora.Utils
|
||||
import Agora.Utils (passetClassValueOf, psingletonValue)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | Type-level unique identifier for an `AssetClass`
|
||||
-- | Type-level unique identifier for an 'Plutus.V1.Ledger.Value.AssetClass'
|
||||
type MoneyClass =
|
||||
( -- AssetClass
|
||||
Symbol
|
||||
|
|
@ -56,16 +57,24 @@ type MoneyClass =
|
|||
Nat
|
||||
)
|
||||
|
||||
-- | A `PDiscrete` amount of currency tagged on the type level with the `MoneyClass` it belong sto
|
||||
-- | A 'PDiscrete' amount of currency tagged on the type level with the 'MoneyClass' it belongs to
|
||||
newtype PDiscrete (mc :: MoneyClass) (s :: S)
|
||||
= PDiscrete (Term s PInteger)
|
||||
deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (PDiscrete mc) PInteger)
|
||||
|
||||
newtype Discrete (mc :: MoneyClass)
|
||||
= Discrete Integer
|
||||
deriving stock (Show)
|
||||
-- | Check if one 'PDiscrete' is greater than another.
|
||||
pgeqDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc :--> PDiscrete mc :--> PBool)
|
||||
pgeqDiscrete = phoistAcyclic $
|
||||
plam $ \x y -> P.do
|
||||
PDiscrete x' <- pmatch x
|
||||
PDiscrete y' <- pmatch y
|
||||
y' #<= x'
|
||||
|
||||
-- | Add two `PDiscrete` values of the same `MoneyClass`.
|
||||
-- | Returns a zero-value 'PDiscrete' unit for any 'MoneyClass'.
|
||||
pzeroDiscrete :: forall (mc :: MoneyClass) (s :: S). Term s (PDiscrete mc)
|
||||
pzeroDiscrete = phoistAcyclic $ pcon (PDiscrete 0)
|
||||
|
||||
-- | Add two 'PDiscrete' values of the same 'MoneyClass'.
|
||||
paddDiscrete :: Term s (PDiscrete mc :--> PDiscrete mc :--> PDiscrete mc)
|
||||
paddDiscrete = phoistAcyclic $
|
||||
-- In the future, this should use plutarch-numeric
|
||||
|
|
@ -100,7 +109,8 @@ pvalueDiscrete = phoistAcyclic $
|
|||
# f
|
||||
|
||||
{- | Get a `PValue` from a `PDiscrete`.
|
||||
__NOTE__: `pdiscreteValue` after `pvalueDiscrete` is loses information
|
||||
__NOTE__: `pdiscreteValue` after `pvalueDiscrete` is not a round-trip.
|
||||
It filters for a particular 'MoneyClass'.
|
||||
-}
|
||||
pdiscreteValue ::
|
||||
forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ import Agora.SafeMoney (MoneyClass, PDiscrete)
|
|||
{- | Generate 'PDiscrete' values tagged by a particular MoneyClass
|
||||
|
||||
@
|
||||
[discrete| 123.456 ADA |] :: 'Term' s ('PDiscrete' 'ADA')
|
||||
[discrete| 123.456 'Agora.SafeMoney.ADA' |] :: 'Term' s ('PDiscrete' 'Agora.SafeMoney.ADA')
|
||||
@
|
||||
-}
|
||||
discrete :: QuasiQuoter
|
||||
|
|
|
|||
|
|
@ -9,8 +9,9 @@ Vote-lockable stake UTXOs holding GT.
|
|||
-}
|
||||
module Agora.Stake (
|
||||
PStakeDatum (..),
|
||||
PStakeAction (..),
|
||||
PStakeRedeemer (..),
|
||||
StakeDatum (..),
|
||||
StakeRedeemer (..),
|
||||
Stake (..),
|
||||
stakePolicy,
|
||||
stakeValidator,
|
||||
|
|
@ -19,9 +20,12 @@ 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
|
||||
|
|
@ -50,6 +54,7 @@ import Plutarch.DataRepr (
|
|||
)
|
||||
import Plutarch.Internal (punsafeCoerce)
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
|
@ -58,6 +63,8 @@ import Agora.SafeMoney (
|
|||
PDiscrete,
|
||||
paddDiscrete,
|
||||
pdiscreteValue,
|
||||
pgeqDiscrete,
|
||||
pzeroDiscrete,
|
||||
)
|
||||
import Agora.Utils (
|
||||
anyInput,
|
||||
|
|
@ -65,6 +72,9 @@ import Agora.Utils (
|
|||
paddValue,
|
||||
passert,
|
||||
pfindTxInByTxOutRef,
|
||||
pgeqByClass,
|
||||
pgeqByClass',
|
||||
pgeqBySymbol,
|
||||
psingletonValue,
|
||||
psymbolValueOf,
|
||||
ptxSignedBy,
|
||||
|
|
@ -77,7 +87,7 @@ import Agora.Utils (
|
|||
data Stake (gt :: MoneyClass) = Stake
|
||||
|
||||
-- | Plutarch-level redeemer for Stake scripts.
|
||||
data PStakeAction (gt :: MoneyClass) (s :: S)
|
||||
data PStakeRedeemer (gt :: MoneyClass) (s :: S)
|
||||
= -- | Deposit or withdraw a discrete amount of the staked governance token.
|
||||
PDepositWithdraw (Term s (PDataRecord '["delta" ':= PDiscrete gt]))
|
||||
| -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets.
|
||||
|
|
@ -87,7 +97,23 @@ data PStakeAction (gt :: MoneyClass) (s :: S)
|
|||
deriving anyclass (PIsDataRepr)
|
||||
deriving
|
||||
(PlutusType, PIsData)
|
||||
via PIsDataReprInstances (PStakeAction gt)
|
||||
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.
|
||||
|
||||
-- | Haskell-level redeemer for Stake scripts.
|
||||
data StakeRedeemer
|
||||
= -- | Deposit or withdraw a discrete amount of the staked governance token.
|
||||
DepositWithdraw 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)]
|
||||
|
||||
-- | Plutarch-level datum for Stake scripts.
|
||||
newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum
|
||||
|
|
@ -103,7 +129,8 @@ newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum
|
|||
|
||||
-- | Haskell-level datum for Stake scripts.
|
||||
data StakeDatum = StakeDatum
|
||||
{ stakedAmount :: Integer
|
||||
{ -- FIXME: This needs to be gt
|
||||
stakedAmount :: Integer
|
||||
, owner :: PubKeyHash
|
||||
}
|
||||
deriving stock (Show, GHC.Generic)
|
||||
|
|
@ -200,8 +227,28 @@ stakePolicy _stake =
|
|||
# ctx.txInfo
|
||||
# stakeDatum.owner
|
||||
|
||||
-- TODO: Needs to be >=, rather than ==
|
||||
let valueCorrect = pdata value #== pdata expectedValue
|
||||
-- TODO: 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.
|
||||
let valueCorrect =
|
||||
foldr1
|
||||
(#&&)
|
||||
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
|
||||
, pgeqByClass'
|
||||
( AssetClass
|
||||
( fromString . symbolVal $ Proxy @ac
|
||||
, fromString . symbolVal $ Proxy @n
|
||||
)
|
||||
)
|
||||
# value
|
||||
# expectedValue
|
||||
, pgeqByClass
|
||||
# ownSymbol
|
||||
# tn
|
||||
# value
|
||||
# expectedValue
|
||||
]
|
||||
|
||||
ownerSignsTransaction
|
||||
#&& valueCorrect
|
||||
popaque (pconstant ())
|
||||
|
|
@ -226,8 +273,8 @@ stakeValidator stake =
|
|||
txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo'
|
||||
|
||||
-- Coercion is safe in that if coercion fails we crash hard.
|
||||
let stakeAction :: Term _ (PStakeAction gt)
|
||||
stakeAction = pfromData $ punsafeCoerce redeemer
|
||||
let stakeRedeemer :: Term _ (PStakeRedeemer gt)
|
||||
stakeRedeemer = pfromData $ punsafeCoerce redeemer
|
||||
stakeDatum' :: Term _ (PStakeDatum gt)
|
||||
stakeDatum' = pfromData $ punsafeCoerce datum
|
||||
stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
|
||||
|
|
@ -242,7 +289,7 @@ stakeValidator stake =
|
|||
mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfo.mint
|
||||
spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfo'
|
||||
|
||||
pmatch stakeAction $ \case
|
||||
pmatch stakeRedeemer $ \case
|
||||
PDestroy _ -> P.do
|
||||
passert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
|
|
@ -270,13 +317,43 @@ stakeValidator stake =
|
|||
delta <- plet $ pfield @"delta" # r
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
let correctOutputDatum =
|
||||
stakeDatum.owner #== newStakeDatum.owner
|
||||
#&& (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount
|
||||
foldr1
|
||||
(#&&)
|
||||
[ stakeDatum.owner #== newStakeDatum.owner
|
||||
, (paddDiscrete # 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
|
||||
]
|
||||
let expectedValue = paddValue # continuingValue # (pdiscreteValue # delta)
|
||||
|
||||
-- TODO: As above, needs to be >=, rather than ==
|
||||
let correctValue = pdata value #== pdata expectedValue
|
||||
isScriptAddress #&& correctOutputDatum #&& correctValue
|
||||
-- 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.
|
||||
let valueCorrect =
|
||||
foldr1
|
||||
(#&&)
|
||||
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
|
||||
, pgeqByClass'
|
||||
( AssetClass
|
||||
( fromString . symbolVal $ Proxy @ac
|
||||
, fromString . symbolVal $ Proxy @n
|
||||
)
|
||||
)
|
||||
# value
|
||||
# expectedValue
|
||||
, pgeqBySymbol
|
||||
# stCurrencySymbol
|
||||
# value
|
||||
# expectedValue
|
||||
]
|
||||
|
||||
foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "isScriptAddress" isScriptAddress
|
||||
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
|
||||
, ptraceIfFalse "valueCorrect" valueCorrect
|
||||
]
|
||||
|
||||
popaque (pconstant ())
|
||||
|
||||
|
|
|
|||
|
|
@ -19,6 +19,9 @@ module Agora.Utils (
|
|||
psymbolValueOf,
|
||||
passetClassValueOf,
|
||||
passetClassValueOf',
|
||||
pgeqByClass,
|
||||
pgeqBySymbol,
|
||||
pgeqByClass',
|
||||
pfindTxInByTxOutRef,
|
||||
psingletonValue,
|
||||
pfindMap,
|
||||
|
|
@ -180,6 +183,27 @@ passetClassValueOf' :: AssetClass -> Term s (PValue :--> PInteger)
|
|||
passetClassValueOf' (AssetClass (sym, token)) =
|
||||
passetClassValueOf # pconstant sym # pconstant token
|
||||
|
||||
-- | Return '>=' on two values comparing by only a particular AssetClass
|
||||
pgeqByClass :: Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PValue :--> PBool)
|
||||
pgeqByClass =
|
||||
phoistAcyclic $
|
||||
plam $ \cs tn a b ->
|
||||
passetClassValueOf # cs # tn # b #<= passetClassValueOf # cs # tn # a
|
||||
|
||||
-- | Return '>=' on two values comparing by only a particular CurrencySymbol
|
||||
pgeqBySymbol :: Term s (PCurrencySymbol :--> PValue :--> PValue :--> PBool)
|
||||
pgeqBySymbol =
|
||||
phoistAcyclic $
|
||||
plam $ \cs a b ->
|
||||
psymbolValueOf # cs # b #<= psymbolValueOf # cs # a
|
||||
|
||||
-- | Return '>=' on two values comparing by only a particular Haskell-level AssetClass
|
||||
pgeqByClass' :: AssetClass -> Term s (PValue :--> PValue :--> PBool)
|
||||
pgeqByClass' ac =
|
||||
phoistAcyclic $
|
||||
plam $ \a b ->
|
||||
passetClassValueOf' ac # b #<= passetClassValueOf' ac # a
|
||||
|
||||
-- | Union two maps using a merge function on collisions.
|
||||
pmapUnionWith :: forall k v s. PIsData v => Term s ((v :--> v :--> v) :--> PMap k v :--> PMap k v :--> PMap k v)
|
||||
pmapUnionWith = phoistAcyclic $
|
||||
|
|
|
|||
|
|
@ -1,7 +1,17 @@
|
|||
{- |
|
||||
Module : PPrelude
|
||||
Maintainer : emi@haskell.fyi
|
||||
Description: Prelude imported throughout this project
|
||||
|
||||
Prelude imported throughout this project
|
||||
-}
|
||||
module PPrelude (
|
||||
module Prelude,
|
||||
module Plutarch.Prelude,
|
||||
module Plutarch,
|
||||
) where
|
||||
|
||||
-- These are not exported by Plutarch.Prelude, for some reason. Maybe we can 'fix' this upstream?
|
||||
import Plutarch (ClosedTerm, compile)
|
||||
import Plutarch.Prelude
|
||||
import Prelude
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue