From c5e17dddeb471b357965201c57a0ba6f9228e425 Mon Sep 17 00:00:00 2001 From: Emily Martins Date: Mon, 7 Feb 2022 22:45:09 +0100 Subject: [PATCH] safe-money proof of concept --- agora.cabal | 5 +- src/Agora/AuthorityToken.hs | 44 +---------- src/Agora/SafeMoney.hs | 143 ++++++++++++++++++++++++++++++++++++ src/Agora/SafeMoney/QQ.hs | 88 ++++++++++++++++++++++ 4 files changed, 239 insertions(+), 41 deletions(-) create mode 100644 src/Agora/SafeMoney.hs create mode 100644 src/Agora/SafeMoney/QQ.hs diff --git a/agora.cabal b/agora.cabal index bc8e01d..6e40499 100644 --- a/agora.cabal +++ b/agora.cabal @@ -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 diff --git a/src/Agora/AuthorityToken.hs b/src/Agora/AuthorityToken.hs index bbd2849..c51f8e6 100644 --- a/src/Agora/AuthorityToken.hs +++ b/src/Agora/AuthorityToken.hs @@ -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) diff --git a/src/Agora/SafeMoney.hs b/src/Agora/SafeMoney.hs new file mode 100644 index 0000000..f4107fb --- /dev/null +++ b/src/Agora/SafeMoney.hs @@ -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 diff --git a/src/Agora/SafeMoney/QQ.hs b/src/Agora/SafeMoney/QQ.hs new file mode 100644 index 0000000..29a5213 --- /dev/null +++ b/src/Agora/SafeMoney/QQ.hs @@ -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."