safe-money proof of concept
This commit is contained in:
Emily Martins
parent
c6c87b4b11
commit
c5e17dddeb
4 changed files with 239 additions and 41 deletions
|
|
@ -92,7 +92,10 @@ common test-deps
|
|||
|
||||
library
|
||||
import: lang, deps
|
||||
exposed-modules: Agora.AuthorityToken
|
||||
exposed-modules:
|
||||
Agora.AuthorityToken
|
||||
Agora.SafeMoney
|
||||
Agora.SafeMoney.QQ
|
||||
other-modules:
|
||||
hs-source-dirs: src
|
||||
|
||||
|
|
|
|||
|
|
@ -1,3 +1,5 @@
|
|||
{-# LANGUAGE PolyKinds #-}
|
||||
|
||||
module Agora.AuthorityToken (
|
||||
authorityTokenPolicy,
|
||||
AuthorityToken (..),
|
||||
|
|
@ -16,6 +18,8 @@ import Plutarch.Api.V1
|
|||
import Plutarch.List (pfoldr')
|
||||
import Plutarch.Prelude
|
||||
|
||||
import Agora.SafeMoney
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
{- | An AuthorityToken represents a proof that a particular token
|
||||
|
|
@ -31,46 +35,6 @@ data AuthorityToken = AuthorityToken
|
|||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- TODO: upstream something like this
|
||||
pfind' ::
|
||||
PIsListLike list a =>
|
||||
(Term s a -> Term s PBool) ->
|
||||
Term s (list a :--> PMaybe a)
|
||||
pfind' p =
|
||||
precList
|
||||
(\self x xs -> pif (p x) (pcon (PJust x)) (self # xs))
|
||||
(const $ pcon PNothing)
|
||||
|
||||
-- TODO: upstream something like this
|
||||
plookup ::
|
||||
(PEq a, PIsListLike list (PBuiltinPair a b)) =>
|
||||
Term s (a :--> list (PBuiltinPair a b) :--> PMaybe b)
|
||||
plookup =
|
||||
phoistAcyclic $
|
||||
plam $ \k xs ->
|
||||
pmatch (pfind' (\p -> pfstBuiltin # p #== k) # xs) $ \case
|
||||
PNothing -> pcon PNothing
|
||||
PJust p -> pcon (PJust (psndBuiltin # p))
|
||||
|
||||
passetClassValueOf' :: AssetClass -> Term s (PValue :--> PInteger)
|
||||
passetClassValueOf' (AssetClass (sym, token)) =
|
||||
passetClassValueOf # pconstant sym # pconstant token
|
||||
|
||||
passetClassValueOf ::
|
||||
Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PInteger)
|
||||
passetClassValueOf =
|
||||
phoistAcyclic $
|
||||
plam $ \sym token value'' ->
|
||||
pmatch value'' $ \(PValue value') ->
|
||||
pmatch value' $ \(PMap value) ->
|
||||
pmatch (plookup # pdata sym # value) $ \case
|
||||
PNothing -> 0
|
||||
PJust m' ->
|
||||
pmatch (pfromData m') $ \(PMap m) ->
|
||||
pmatch (plookup # pdata token # m) $ \case
|
||||
PNothing -> 0
|
||||
PJust v -> pfromData v
|
||||
|
||||
authorityTokenPolicy ::
|
||||
AuthorityToken ->
|
||||
Term s (PData :--> PData :--> PScriptContext :--> PUnit)
|
||||
|
|
|
|||
143
src/Agora/SafeMoney.hs
Normal file
143
src/Agora/SafeMoney.hs
Normal file
|
|
@ -0,0 +1,143 @@
|
|||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE StandaloneKindSignatures #-}
|
||||
{-# OPTIONS_GHC -Wwarn=missing-methods #-}
|
||||
{-# OPTIONS_GHC -Wwarn=unused-imports #-}
|
||||
|
||||
module Agora.SafeMoney (module Agora.SafeMoney) where
|
||||
|
||||
import Data.Proxy (Proxy (Proxy))
|
||||
import Data.String
|
||||
import GHC.TypeLits (
|
||||
CmpNat,
|
||||
KnownNat,
|
||||
KnownSymbol,
|
||||
Nat,
|
||||
SomeNat (..),
|
||||
SomeSymbol (..),
|
||||
Symbol,
|
||||
natVal,
|
||||
someNatVal,
|
||||
someSymbolVal,
|
||||
symbolVal,
|
||||
)
|
||||
import Prelude
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Plutus.V1.Ledger.Value (AssetClass (..))
|
||||
import Plutus.V1.Ledger.Value qualified as Ledger
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Plutarch.Api.V1
|
||||
import Plutarch.Internal
|
||||
import Plutarch.Prelude
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- | Type-level unique identifier for an AssetClass
|
||||
type MoneyClass =
|
||||
( -- AssetClass
|
||||
Symbol
|
||||
, -- TokenName
|
||||
Symbol
|
||||
, -- Decimal places
|
||||
Nat
|
||||
)
|
||||
|
||||
newtype Discrete (mc :: MoneyClass) (s :: S)
|
||||
= Discrete (Term s PInteger)
|
||||
deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (Discrete mc) PInteger)
|
||||
|
||||
instance Num (Term s (Discrete mc)) where
|
||||
(+) x y = pcon $
|
||||
Discrete . unTermCont $ do
|
||||
Discrete x' <- tcont $ pmatch x
|
||||
Discrete y' <- tcont $ pmatch y
|
||||
pure (x' + y')
|
||||
abs x = pcon $
|
||||
Discrete . unTermCont $ do
|
||||
Discrete x' <- tcont $ pmatch x
|
||||
pure (abs x')
|
||||
negate x = pcon $
|
||||
Discrete . unTermCont $ do
|
||||
Discrete x' <- tcont $ pmatch x
|
||||
pure (negate x')
|
||||
(*) x y = pcon $
|
||||
Discrete . unTermCont $ do
|
||||
Discrete x' <- tcont $ pmatch x
|
||||
Discrete y' <- tcont $ pmatch y
|
||||
pure (x' * y')
|
||||
fromInteger = error "Tried to `fromInteger` for a Discrete type. use `discrete` quasiquoter instead."
|
||||
|
||||
(^*) :: Term s (Discrete mc) -> Term s PInteger -> Term s (Discrete mc)
|
||||
(^*) x y = pcon $
|
||||
Discrete . unTermCont $ do
|
||||
Discrete x' <- tcont $ pmatch x
|
||||
pure (x' * y)
|
||||
|
||||
type LQ :: MoneyClass
|
||||
type LQ = '("da8c30857834c6ae7203935b89278c532b3995245295456f993e1d24", "LQ", 6)
|
||||
|
||||
type ADA :: MoneyClass
|
||||
type ADA = '("", "", 6)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- TODO: upstream something like this
|
||||
pfind' ::
|
||||
PIsListLike list a =>
|
||||
(Term s a -> Term s PBool) ->
|
||||
Term s (list a :--> PMaybe a)
|
||||
pfind' p =
|
||||
precList
|
||||
(\self x xs -> pif (p x) (pcon (PJust x)) (self # xs))
|
||||
(const $ pcon PNothing)
|
||||
|
||||
-- TODO: upstream something like this
|
||||
plookup ::
|
||||
(PEq a, PIsListLike list (PBuiltinPair a b)) =>
|
||||
Term s (a :--> list (PBuiltinPair a b) :--> PMaybe b)
|
||||
plookup =
|
||||
phoistAcyclic $
|
||||
plam $ \k xs ->
|
||||
pmatch (pfind' (\p -> pfstBuiltin # p #== k) # xs) $ \case
|
||||
PNothing -> pcon PNothing
|
||||
PJust p -> pcon (PJust (psndBuiltin # p))
|
||||
|
||||
matchMaybe :: Term s r -> Term s (PMaybe a) -> TermCont @r s (Term s a)
|
||||
matchMaybe r f = TermCont $ \k ->
|
||||
pmatch f $ \case
|
||||
PJust v -> k v
|
||||
PNothing -> r
|
||||
|
||||
passetClassValueOf ::
|
||||
Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PInteger)
|
||||
passetClassValueOf =
|
||||
phoistAcyclic $
|
||||
plam $ \sym token value'' -> unTermCont $ do
|
||||
PValue value' <- tcont $ pmatch value''
|
||||
PMap value <- tcont $ pmatch value'
|
||||
m' <- matchMaybe 0 (plookup # pdata sym # value)
|
||||
PMap m <- tcont (pmatch (pfromData m'))
|
||||
v <- matchMaybe 0 (plookup # pdata token # m)
|
||||
pure (pfromData v)
|
||||
|
||||
passetClassValueOf' :: AssetClass -> Term s (PValue :--> PInteger)
|
||||
passetClassValueOf' (AssetClass (sym, token)) =
|
||||
passetClassValueOf # pconstant sym # pconstant token
|
||||
|
||||
-- | Downcast a 'PValue' to a 'Discrete' unit
|
||||
valueDiscrete ::
|
||||
forall (moneyClass :: MoneyClass) (ac :: Symbol) (n :: Symbol) (scale :: Nat) s.
|
||||
( KnownSymbol ac
|
||||
, KnownSymbol n
|
||||
, moneyClass ~ '(ac, n, scale)
|
||||
) =>
|
||||
Term s (PValue :--> Discrete moneyClass)
|
||||
valueDiscrete = phoistAcyclic $
|
||||
plam $ \f ->
|
||||
pcon . Discrete $
|
||||
passetClassValueOf # (pconstant $ fromString $ symbolVal $ Proxy @ac)
|
||||
# (pconstant $ fromString $ symbolVal $ Proxy @n)
|
||||
# f
|
||||
88
src/Agora/SafeMoney/QQ.hs
Normal file
88
src/Agora/SafeMoney/QQ.hs
Normal file
|
|
@ -0,0 +1,88 @@
|
|||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# OPTIONS_GHC -Wwarn=missing-methods #-}
|
||||
{-# OPTIONS_GHC -Wwarn=unused-imports #-}
|
||||
|
||||
module Agora.SafeMoney.QQ (discrete) where
|
||||
|
||||
import Control.Arrow ((&&&))
|
||||
import Data.Ratio (denominator, numerator)
|
||||
import Debug.Trace
|
||||
import GHC.Real (Ratio ((:%)))
|
||||
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,
|
||||
reifyType,
|
||||
)
|
||||
import PlutusTx.Ratio (unsafeRatio)
|
||||
import Text.ParserCombinators.ReadP (readP_to_S, skipSpaces)
|
||||
import Text.Read (lexP, readMaybe, readPrec_to_P)
|
||||
import Text.Read.Lex (Lexeme (Ident, Number), Number, numberToFixed, numberToRational)
|
||||
import Prelude
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
import Plutarch.Internal (punsafeCoerce)
|
||||
import Plutarch.Prelude hiding (Type)
|
||||
|
||||
import Agora.SafeMoney
|
||||
|
||||
discrete :: QuasiQuoter
|
||||
discrete = QuasiQuoter discreteExp errorDiscretePat errorDiscreteType errorDiscreteDiscretelaration
|
||||
|
||||
discreteConstant :: forall (moneyClass :: MoneyClass) s. Integer -> Term s (Discrete moneyClass)
|
||||
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 $ "MoneyClass 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 Type
|
||||
errorDiscreteType _ = fail "Cannot use 'discrete' in a type context."
|
||||
|
||||
errorDiscreteDiscretelaration :: String -> Q [Dec]
|
||||
errorDiscreteDiscretelaration _ = fail "Cannot use 'discrete' in a declaration context."
|
||||
Loading…
Add table
Add a link
Reference in a new issue