diff --git a/.ghcid b/.ghcid index e46612f..cfc065d 100644 --- a/.ghcid +++ b/.ghcid @@ -1 +1 @@ ---command="cabal repl test-suite:cem-sdk-test" -W -T ":main --failure-report=/tmp/hspec-report.txt -r" +--command="cabal repl test-suite:cem-sdk-test" -W -T ":main" diff --git a/.hlint.yaml b/.hlint.yaml index 054580b..a91e670 100644 --- a/.hlint.yaml +++ b/.hlint.yaml @@ -16,3 +16,4 @@ - ignore: {name: Use unless} - ignore: {name: "Use asks"} - ignore: {name: "Eta reduce"} +- ignore: {name: Use concatMap} diff --git a/cem-script.cabal b/cem-script.cabal index 2533d76..442e771 100644 --- a/cem-script.cabal +++ b/cem-script.cabal @@ -28,6 +28,7 @@ common common-lang build-depends: , base + , containers , mtl , transformers @@ -41,9 +42,10 @@ common common-lang GADTs LambdaCase NoImplicitPrelude - NoPolyKinds + OverloadedRecordDot OverloadedStrings PatternSynonyms + PolyKinds QuantifiedConstraints StrictData TemplateHaskell @@ -98,11 +100,12 @@ common common-offchain , cardano-ledger-babbage , cardano-ledger-core , cardano-ledger-shelley - , containers , filepath , ouroboros-network-protocols , pretty-show + , prettyprinter , retry + , singletons-th , text , time , unix @@ -114,7 +117,10 @@ common common-executable library data-spine import: common-lang hs-source-dirs: src-lib/data-spine + + -- FIXME: was not meant to be dependent on Plutus... build-depends: + , plutus-tx , singletons , template-haskell @@ -129,6 +135,7 @@ library cardano-extras build-depends: template-haskell exposed-modules: Cardano.Extras + Plutarch.Extras Plutus.Deriving Plutus.Extras @@ -141,6 +148,7 @@ library exposed-modules: Cardano.CEM Cardano.CEM.Documentation + Cardano.CEM.DSL Cardano.CEM.Examples.Auction Cardano.CEM.Examples.Compilation Cardano.CEM.Examples.Voting @@ -149,7 +157,6 @@ library Cardano.CEM.Monads.L1 Cardano.CEM.OffChain Cardano.CEM.OnChain - Cardano.CEM.Stages Cardano.CEM.Testing.StateMachine Cardano.CEM.TH diff --git a/src-lib/cardano-extras/Plutarch/Extras.hs b/src-lib/cardano-extras/Plutarch/Extras.hs new file mode 100644 index 0000000..b2c61af --- /dev/null +++ b/src-lib/cardano-extras/Plutarch/Extras.hs @@ -0,0 +1,42 @@ +{-# LANGUAGE QualifiedDo #-} + +module Plutarch.Extras where + +import Prelude + +import Plutarch +import Plutarch.Builtin +import Plutarch.LedgerApi +import Plutarch.LedgerApi.Value +import Plutarch.Maybe (pfromJust) +import Plutarch.Monadic qualified as P +import Plutarch.Prelude + +pMkAdaOnlyValue :: Term s (PInteger :--> PValue Unsorted NonZero) +pMkAdaOnlyValue = phoistAcyclic $ plam $ \lovelaces -> + pforgetSorted $ + psingletonData # padaSymbolData # pdata padaToken # pdata lovelaces + +pscriptHashAddress :: Term s (PAsData PScriptHash :--> PAddress) +pscriptHashAddress = plam $ \datahash -> + let credential = pcon (PScriptCredential (pdcons @"_0" # datahash #$ pdnil)) + nothing = pdata $ pcon (PDNothing pdnil) + inner = pdcons @"credential" # pdata credential #$ pdcons @"stakingCredential" # nothing #$ pdnil + in pcon (PAddress inner) + +ppkhAddress :: Term s (PAsData PPubKeyHash :--> PAddress) +ppkhAddress = plam $ \datahash -> + let credential = pcon (PPubKeyCredential (pdcons @"_0" # datahash #$ pdnil)) + nothing = pdata $ pcon (PDNothing pdnil) + inner = pdcons @"credential" # pdata credential #$ pdcons @"stakingCredential" # nothing #$ pdnil + in pcon (PAddress inner) + +getOwnAddress :: ClosedTerm (PAsData PScriptContext :--> PAsData PAddress) +getOwnAddress = phoistAcyclic $ plam $ \ctx -> P.do + PSpending outRef' <- pmatch $ pfromData $ pfield @"purpose" # ctx + pfield @"address" + #$ pfield @"resolved" + #$ pfromJust + #$ (pfindOwnInput # (pfield @"inputs" #$ pfield @"txInfo" # ctx)) + #$ pfield @"_0" + # outRef' diff --git a/src-lib/data-spine/Data/Spine.hs b/src-lib/data-spine/Data/Spine.hs index 82ebcfa..438156a 100644 --- a/src-lib/data-spine/Data/Spine.hs +++ b/src-lib/data-spine/Data/Spine.hs @@ -3,13 +3,29 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE PolyKinds #-} -module Data.Spine (HasSpine (..), deriveSpine, OfSpine (..)) where +{- | +Note about design decision on nested spines. +`getSpine (Just Value) = JustSpine ValueSpine` - looks more usable, +than `getSpine (Just Value) = JustSpine`. +But it seem to break deriving for parametised types like `Maybe a`, +and can be done with `fmap getSpine mValue`. Probably it actually +works exaclty for functorial parameters. +-} +module Data.Spine where import Prelude +import Data.Data (Proxy) +import Data.List (elemIndex) +import Data.Map qualified as Map +import Data.Maybe (mapMaybe) +import GHC.Natural (Natural) +import GHC.TypeLits (KnownSymbol, symbolVal) import Language.Haskell.TH import Language.Haskell.TH.Syntax +import PlutusTx (FromData, ToData, UnsafeFromData, unstableMakeIsData) + -- | Definitions {- | Spine is datatype, which tags constructors of ADT. @@ -19,29 +35,66 @@ import Language.Haskell.TH.Syntax class ( Ord (Spine sop) , Show (Spine sop) + , Enum (Spine sop) + , Bounded (Spine sop) ) => HasSpine sop where - type Spine sop + type Spine sop = spine | spine -> sop getSpine :: sop -> Spine sop -instance (HasSpine sop1, HasSpine sop2) => HasSpine (sop1, sop2) where - type Spine (sop1, sop2) = (Spine sop1, Spine sop2) - getSpine (d1, d2) = (getSpine d1, getSpine d2) +-- | Version of `HasSpine` knowing its Plutus Data encoding +class + ( HasSpine sop + , UnsafeFromData sop + , ToData sop + , FromData sop + ) => + HasPlutusSpine sop + where + fieldsMap :: Map.Map (Spine sop) [String] + +toNat :: Int -> Natural +toNat = fromInteger . toInteger + +spineFieldsNum :: forall sop. (HasPlutusSpine sop) => Spine sop -> Natural +spineFieldsNum spine = + toNat $ length $ (fieldsMap @sop) Map.! spine + +-- FIXME: use spine do discriminate +fieldNum :: + forall sop label. + (HasPlutusSpine sop, KnownSymbol label) => + Proxy label -> + Natural +fieldNum proxyLabel = + head $ mapMaybe fieldIndex x + where + x = Map.elems $ fieldsMap @sop + fieldName = symbolVal proxyLabel + fieldIndex dict = toNat <$> elemIndex fieldName dict -instance (HasSpine sop) => HasSpine (Maybe sop) where - type Spine (Maybe sop) = Maybe (Spine sop) - getSpine = fmap getSpine +allSpines :: forall sop. (HasPlutusSpine sop) => [Spine sop] +allSpines = [Prelude.minBound .. Prelude.maxBound] --- | Newtype encoding sop value of fixed known spine -newtype OfSpine (x :: Spine datatype) = UnsafeMkOfSpine {getValue :: datatype} +-- | Phantom type param is required for `HasSpine` injectivity +data MaybeSpine a = JustSpine | NothingSpine + deriving stock (Eq, Ord, Show, Bounded, Enum) + +-- FIXME: could such types be derived? +instance HasSpine (Maybe x) where + type Spine (Maybe x) = MaybeSpine x + getSpine Just {} = JustSpine + getSpine Nothing = NothingSpine + +-- Deriving utils --- | Deriving utils addSuffix :: Name -> String -> Name addSuffix (Name (OccName name) flavour) suffix = Name (OccName $ name <> suffix) flavour -reifyDatatype :: Name -> Q (Name, [Name]) +-- FIXME: cleaner return type +reifyDatatype :: Name -> Q (Name, [Name], [[Name]]) reifyDatatype ty = do (TyConI tyCon) <- reify ty (name, cs :: [Con]) <- @@ -50,7 +103,17 @@ reifyDatatype ty = do NewtypeD _ n _ _ cs _ -> pure (n, [cs]) _ -> fail "deriveTags: only 'data' and 'newtype' are supported" csNames <- mapM consName cs - return (name, csNames) + csFields <- mapM consFields cs + return (name, csNames, csFields) + where + fieldName (name, _, _) = name + consFields (RecC _ fields) = return $ map fieldName fields + consFields (NormalC _ fields) | length fields == 0 = return [] + consFields _ = + fail $ + "Spine: only Sum-of-Products are supported, but " + <> show ty + <> " is not" consName :: (MonadFail m) => Con -> m Name consName cons = @@ -61,7 +124,7 @@ consName cons = deriveTags :: Name -> String -> [Name] -> Q [Dec] deriveTags ty suff classes = do - (tyName, csNames) <- reifyDatatype ty + (tyName, csNames, _) <- reifyDatatype ty -- XXX: Quasi-quote splice does not work for case matches list let cs = map (\name -> NormalC (addSuffix name suff) []) csNames v = @@ -70,7 +133,7 @@ deriveTags ty suff classes = do deriveMapping :: Name -> String -> Q Exp deriveMapping ty suff = do - (_, csNames) <- reifyDatatype ty + (_, csNames, _) <- reifyDatatype ty -- XXX: Quasi-quote splice does not work for case matches list let matches = @@ -87,9 +150,7 @@ deriveSpine name = do let suffix = "Spine" spineName = addSuffix name suffix - spineDec <- deriveTags name suffix [''Eq, ''Ord, ''Enum, ''Show] - -- TODO: derive Sing - -- TODO: derive HasField (OfSpine ...) + spineDec <- deriveTags name suffix [''Eq, ''Ord, ''Enum, ''Show, ''Bounded] decls <- [d| @@ -98,3 +159,19 @@ deriveSpine name = do getSpine = $(deriveMapping name suffix) |] return $ spineDec <> decls + +derivePlutusSpine :: Name -> Q [Dec] +derivePlutusSpine name = do + decls <- deriveSpine name + isDataDecls <- unstableMakeIsData name + + (_, _, fieldsNames') <- reifyDatatype name + let fieldsNames = map (map nameBase) fieldsNames' + instanceDecls <- + [d| + instance HasPlutusSpine $(conT name) where + fieldsMap = + Map.fromList $ zip (allSpines @($(conT name))) fieldsNames + |] + + return $ decls <> isDataDecls <> instanceDecls diff --git a/src/Cardano/CEM.hs b/src/Cardano/CEM.hs index 7bcc618..2410a0f 100644 --- a/src/Cardano/CEM.hs +++ b/src/Cardano/CEM.hs @@ -1,99 +1,466 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE NoPolyKinds #-} +-- FIXME: move all lib functions (`LiftPlutarch`s) to another module module Cardano.CEM where -import PlutusTx.Prelude -import Prelude (Show) -import Prelude qualified +import Prelude -import Data.Data (Proxy) import Data.Map qualified as Map +import Data.Maybe (fromJust) +import GHC.OverloadedLabels (IsLabel (..)) +import GHC.Records (HasField (..)) +import GHC.TypeLits (KnownSymbol, Symbol, symbolVal) +import Unsafe.Coerce (unsafeCoerce) -- Plutus imports -import PlutusLedgerApi.V1.Address (Address, pubKeyHashAddress) import PlutusLedgerApi.V1.Crypto (PubKeyHash) import PlutusLedgerApi.V2 (ToData (..), Value) -import PlutusTx.Show.TH (deriveShow) +import PlutusTx qualified +import PlutusTx.Builtins qualified as PlutusTx + +import Data.Singletons.TH +import Data.Text (Text) +import Plutarch (Config (..), (#)) +import Plutarch.Builtin (PIsData) +import Plutarch.Evaluate (evalTerm) +import Plutarch.LedgerApi (KeyGuarantees (..)) +import Plutarch.LedgerApi.Value +import Plutarch.Lift (PUnsafeLiftDecl (..), pconstant, plift) +import Plutarch.Prelude ( + ClosedTerm, + PLift, + PPartialOrd (..), + PShow, + Term, + pnot, + (#&&), + (:-->), + ) +import PlutusLedgerApi.V2.Contexts (TxInfo) -- Project imports -import Cardano.CEM.Stages -import Data.Spine - --- | This is different ways to specify address -data AddressSpec - = ByAddress Address - | ByPubKey PubKeyHash - | BySameScript - deriving stock (Show, Prelude.Eq) - -{-# INLINEABLE addressSpecToAddress #-} -addressSpecToAddress :: Address -> AddressSpec -> Address -addressSpecToAddress ownAddress addressSpec = case addressSpec of - ByAddress address -> address - ByPubKey pubKey -> pubKeyHashAddress pubKey - BySameScript -> ownAddress - -data TxFanFilter script = MkTxFanFilter - { address :: AddressSpec - , rest :: TxFanFilter' script - } - deriving stock (Show, Prelude.Eq) - -data TxFanFilter' script - = Anything - | -- | To be used via `bySameCem` - UnsafeBySameCEM BuiltinData - | ByDatum BuiltinData - deriving stock (Show, Prelude.Eq) - -{-# INLINEABLE bySameCEM #-} - --- | Constraint enforcing state of script mentioning this constraint -bySameCEM :: - (ToData (State script), CEMScript script) => - State script -> - TxFanFilter' script -bySameCEM = UnsafeBySameCEM . toBuiltinData - --- TODO: use natural numbers -data Quantor = Exist Integer | SumValueEq Value +import Data.Spine (HasPlutusSpine, HasSpine (..), derivePlutusSpine, spineFieldsNum) +import Plutarch.Extras + +data CVar = CParams | CState | CTransition | CComp | CTxInfo deriving stock (Show) +genSingletons [''CVar] + +type family DSLValue (resolved :: Bool) script value where + DSLValue False script value = ConstraintDSL script value + DSLValue True _ value = value + +-- | This value should not used on resolved constraint +type family DSLPattern (resolved :: Bool) script value where + DSLPattern False script value = ConstraintDSL script value + DSLPattern True _ value = Void + data TxFanKind = In | InRef | Out deriving stock (Prelude.Eq, Prelude.Show) -data TxFanConstraint script = MkTxFanC - { txFanCKind :: TxFanKind - , txFanCFilter :: TxFanFilter script - , txFanCQuantor :: Quantor - } - deriving stock (Show) +data TxFanFilterNew (resolved :: Bool) script + = UserAddress (DSLValue resolved script PubKeyHash) + | -- FIXME: should have spine been specified known statically + SameScript (DSLValue resolved script (State script)) + +deriving stock instance (CEMScript script) => (Show (TxFanFilterNew True script)) +deriving stock instance (Show (TxFanFilterNew False script)) + +data TxConstraint (resolved :: Bool) script + = TxFan + { kind :: TxFanKind + , cFilter :: TxFanFilterNew resolved script + , value :: DSLValue resolved script Value + } + | MainSignerCoinSelect + { user :: DSLValue resolved script PubKeyHash + , inValue :: DSLValue resolved script Value + , outValue :: DSLValue resolved script Value + } + | MainSignerNoValue (DSLValue resolved script PubKeyHash) + | Error Text + | If + -- | Condition + (DSLPattern resolved script Bool) + -- | Then block + (TxConstraint resolved script) + -- | Else block + (TxConstraint resolved script) + | forall sop. + (HasPlutusSpine sop) => + MatchBySpine + -- | Value being matched by its Spine + (DSLPattern resolved script sop) + -- | Case switch + -- FIXME: might use function instead, will bring `_` syntax, + -- reusing matched var and probably implicitly type-checking spine + -- by saving it to such var DSL value + (Map.Map (Spine sop) (TxConstraint resolved script)) + | Noop + +deriving stock instance (CEMScript script) => (Show (TxConstraint True script)) +deriving stock instance (Show (TxConstraint False script)) + +type family CVarType (cvar :: CVar) script where + CVarType CParams script = Params script + CVarType CState script = State script + CVarType CTransition script = Transition script + CVarType CComp script = TransitionComp script + CVarType CTxInfo script = TxInfo + +type HasFieldPlutus (a :: Symbol) d v = + ( HasField a d v + , HasPlutusSpine d + , KnownSymbol a + , ToData v + ) + +type PlutarchData x = (PShow x, PLift x, PIsData x) + +data ConstraintDSL script value where + Ask :: + forall (var :: CVar) datatype script. + ( SingI var + , datatype Prelude.~ CVarType var script + ) => + Proxy var -> + ConstraintDSL script datatype + Pure :: + (Show value', ToData value') => + value' -> + ConstraintDSL script value' + IsOnChain :: ConstraintDSL script Bool + -- FIXME: should have Spine typechecked on DSL compilation, + -- see `MatchBySpine` + GetField :: + forall (label :: Symbol) sop script value. + (HasFieldPlutus label sop value) => + ConstraintDSL script sop -> + Proxy label -> + ConstraintDSL script value + UnsafeOfSpine :: + forall script datatype spine. + ( spine Prelude.~ Spine datatype + , HasPlutusSpine datatype + ) => + Spine datatype -> + [RecordSetter (ConstraintDSL script) datatype] -> + ConstraintDSL script datatype + UnsafeUpdateOfSpine :: + forall script datatype spine. + ( spine Prelude.~ Spine datatype + , HasPlutusSpine datatype + , PlutusTx.FromData datatype + ) => + ConstraintDSL script datatype -> + Spine datatype -> + [RecordSetter (ConstraintDSL script) datatype] -> + ConstraintDSL script datatype + -- Primitives + Anything :: ConstraintDSL script x + Eq :: + forall x script. + (Eq x) => + ConstraintDSL script x -> + ConstraintDSL script x -> + ConstraintDSL script Bool + LiftPlutarch :: + forall px py script. + (PlutarchData px, PlutarchData py) => + (ClosedTerm (px :--> py)) -> + ConstraintDSL script (PLifted px) -> + ConstraintDSL script (PLifted py) + LiftPlutarch2 :: + forall px1 px2 py script. + (PlutarchData px1, PlutarchData px2, PlutarchData py) => + (forall s. Term s px1 -> Term s px2 -> Term s py) -> + ConstraintDSL script (PLifted px1) -> + ConstraintDSL script (PLifted px2) -> + ConstraintDSL script (PLifted py) + +cOfSpine :: + (HasPlutusSpine datatype) => + Spine datatype -> + [RecordSetter (ConstraintDSL script) datatype] -> + ConstraintDSL script datatype +-- FIXME: should it be ordered? +cOfSpine spine setters = + if toInteger (length setters) == toInteger (spineFieldsNum spine) + then UnsafeOfSpine spine setters + else + error $ + "OfSpine got less setters when number of fields (" + <> show (spineFieldsNum spine) + <> ")" + +cUpdateOfSpine :: + (HasPlutusSpine datatype) => + ConstraintDSL script datatype -> + Spine datatype -> + [RecordSetter (ConstraintDSL script) datatype] -> + ConstraintDSL script datatype +cUpdateOfSpine = UnsafeUpdateOfSpine + +-- FIXME: use some pretty printer lib +instance Prelude.Show (ConstraintDSL x y) where + show dsl = case dsl of + (Ask @cvar Proxy) -> + "Ask " <> drop 1 (show (fromSing $ sing @cvar)) + (GetField valueDsl proxyLabel) -> + Prelude.show valueDsl <> "." <> symbolVal proxyLabel + Eq x y -> show x <> " @== " <> show y + -- FIXME: add user annotations + LiftPlutarch _ x -> "somePlutarchCode (" <> show x <> ")" + LiftPlutarch2 _ x y -> + "somePlutarchCode (" <> show x <> ") (" <> show y <> ")" + IsOnChain -> "IsOnChain" + Anything -> "Anything" + Pure x -> "Pure (" <> show x <> ")" + UnsafeOfSpine spine setters -> + "OfSpine " <> show spine <> show setters + UnsafeUpdateOfSpine spine _ _ -> "UnsafeUpdateOfSpine " <> show spine + +compileConstraint :: + forall script. + (CEMScript script) => + CEMScriptDatum script -> + Transition script -> + TxConstraint False script -> + Either String (TxConstraint True script) +compileConstraint datum transition c = case c of + If condDsl thenConstr elseConstr -> do + value <- compileDslRecur condDsl + if value + then recur thenConstr + else recur elseConstr + MatchBySpine value caseSwitch -> + recur . (caseSwitch Map.!) . getSpine =<< compileDslRecur value + MainSignerNoValue signerDsl -> + MainSignerNoValue <$> compileDslRecur signerDsl + MainSignerCoinSelect pkhDsl inValueDsl outValueDsl -> + MainSignerCoinSelect + <$> compileDslRecur pkhDsl + <*> compileDslRecur inValueDsl + <*> compileDslRecur outValueDsl + TxFan kind fanFilter valueDsl -> + TxFan kind <$> compileFanFilter fanFilter <*> compileDslRecur valueDsl + Noop -> Right Noop + -- XXX: changing resolved type param of Error + e@(Error {}) -> Right $ unsafeCoerce e + where + compileDslRecur :: ConstraintDSL script x -> Either String x + compileDslRecur = compileDsl @script datum transition + recur = compileConstraint @script datum transition + compileFanFilter fanFilter = case fanFilter of + UserAddress dsl -> UserAddress <$> compileDslRecur dsl + SameScript stateDsl -> SameScript <$> compileDslRecur stateDsl + +compileDsl :: + forall script x. + (CEMScript script) => + CEMScriptDatum script -> + Transition script -> + ConstraintDSL script x -> + Either String x +compileDsl datum@(params, state) transition dsl = case dsl of + Pure x -> Right x + Ask @cvar @_ @dt Proxy -> + case sing @cvar of + SCParams -> Right params + SCState -> Right state + SCTransition -> Right transition + SCComp -> case transitionComp @script of + Just go -> Right $ go params state transition + Nothing -> Prelude.error "Unreachable" + SCTxInfo -> raiseOnchainErrorMessage ("TxInfo reference" :: String) + IsOnChain -> Right False + GetField @label @datatype @_ @value recordDsl _ -> do + recordValue <- recur recordDsl + Right $ getField @label @datatype @value recordValue + Eq @v xDsl yDsl -> (==) <$> (recur @v) xDsl <*> (recur @v) yDsl + UnsafeOfSpine spine recs -> do + rs <- mapM compileRecordSetter recs + Right $ + fromJust . PlutusTx.fromData . PlutusTx.builtinDataToData $ + PlutusTx.mkConstr + (toInteger $ Prelude.fromEnum spine) + rs + where + compileRecordSetter (_ ::= valueDsl) = do + value <- recur valueDsl + Right $ PlutusTx.toBuiltinData value + UnsafeUpdateOfSpine valueDsl _spine setters -> do + case setters of + [] -> recur valueDsl + _ -> error "FIXME: not implemented" + LiftPlutarch pterm argDsl -> do + arg <- recur argDsl + case evalTerm NoTracing $ pterm # pconstant arg of + Right (Right resultTerm, _, _) -> Right $ plift resultTerm + Right (Left message, _, _) -> + Left $ "Unreachable: plutach running error " <> show message + Left message -> Left $ "Unreachable: plutach running error " <> show message + LiftPlutarch2 pterm arg1Dsl arg2Dsl -> do + arg1 <- recur arg1Dsl + arg2 <- recur arg2Dsl + case evalTerm NoTracing $ pterm (pconstant arg1) (pconstant arg2) of + Right (Right resultTerm, _, _) -> Right $ plift resultTerm + Right (Left message, _, _) -> + Left $ "Unreachable: plutach running error " <> show message + Left message -> Left $ "Unreachable: plutach running error " <> show message + Anything -> raiseOnchainErrorMessage dsl + where + raiseOnchainErrorMessage :: (Show a) => a -> Either String x + raiseOnchainErrorMessage x = + Left $ + "On-chain only feature was reached while off-chain constraints compilation " + <> "(should be guarded to only triggered onchain): " + <> show x + recur :: ConstraintDSL script x1 -> Either String x1 + recur = compileDsl @script datum transition + +cMkAdaOnlyValue :: + ConstraintDSL script Integer -> ConstraintDSL script Value +cMkAdaOnlyValue = LiftPlutarch pMkAdaOnlyValue + +cEmptyValue :: ConstraintDSL script Value +cEmptyValue = cMkAdaOnlyValue $ Pure 0 + +cMinLovelace :: ConstraintDSL script Value +cMinLovelace = cMkAdaOnlyValue $ Pure 3_000_000 + +(@==) :: + (Eq x) => ConstraintDSL script x -> ConstraintDSL script x -> ConstraintDSL script Bool +(@==) = Eq + +(@<=) :: + forall px script. + (PlutarchData px, PPartialOrd px) => + ConstraintDSL script (PLifted px) -> + ConstraintDSL script (PLifted px) -> + ConstraintDSL script Bool +(@<=) = LiftPlutarch2 (#<=) + +(@<) :: + forall px script. + (PlutarchData px, PPartialOrd px) => + ConstraintDSL script (PLifted px) -> + ConstraintDSL script (PLifted px) -> + ConstraintDSL script Bool +(@<) = LiftPlutarch2 (#<) + +(@>=) :: + forall px script. + (PlutarchData px, PPartialOrd px) => + ConstraintDSL script (PLifted px) -> + ConstraintDSL script (PLifted px) -> + ConstraintDSL script Bool +(@>=) = flip (@<=) + +(@>) :: + forall px script. + (PlutarchData px, PPartialOrd px) => + ConstraintDSL script (PLifted px) -> + ConstraintDSL script (PLifted px) -> + ConstraintDSL script Bool +(@>) = flip (@<) + +(@<>) :: + ConstraintDSL script Value -> + ConstraintDSL script Value -> + ConstraintDSL script Value +(@<>) = + LiftPlutarch2 @(PValue 'Unsorted 'NonZero) @_ @_ merge + where + merge x y = + pforgetSorted $ + (<>) + (passertSorted # x) + (passertSorted # y) + +infixr 3 @&& + +(@&&) :: + ConstraintDSL script Bool -> + ConstraintDSL script Bool -> + ConstraintDSL script Bool +(@&&) = LiftPlutarch2 (#&&) + +cNot :: ConstraintDSL script Bool -> ConstraintDSL script Bool +cNot = LiftPlutarch pnot + +offchainOnly :: TxConstraint False script -> TxConstraint False script +offchainOnly c = If IsOnChain Noop c + +byFlagError :: + ConstraintDSL script Bool -> Text -> TxConstraint False script +byFlagError flag message = If flag (Error message) Noop + +data RecordLabel (label :: Symbol) = MkRecordLabel + +instance + (KnownSymbol s1, s1 ~ s2) => + IsLabel (s1 :: Symbol) (RecordLabel s2) + where + fromLabel :: RecordLabel s2 + fromLabel = MkRecordLabel + +data RecordSetter f datatype where + (::=) :: + forall (label :: Symbol) datatype value f. + (HasFieldPlutus label datatype value) => + RecordLabel label -> + f value -> + RecordSetter f datatype + +instance (forall x. Show (f x)) => Show (RecordSetter f datatype) where + show ((::=) @label _label value) = + symbolVal (Proxy @label) <> " ::= " <> show value + +instance + (HasFieldPlutus label datatype value) => + HasField label (ConstraintDSL script datatype) (ConstraintDSL script value) + where + getField recordDsl = + GetField @label @datatype @script @value recordDsl Proxy + +askC :: + forall (var :: CVar) script. + (SingI var) => + ConstraintDSL script (CVarType var script) +askC = Ask @var @_ @script (Proxy :: Proxy var) + +ctxParams :: ConstraintDSL script (Params script) +ctxTransition :: ConstraintDSL script (Transition script) +ctxParams = askC @CParams +ctxTransition = askC @CTransition +ctxState :: ConstraintDSL script (State script) +ctxState = askC @CState +ctxComp :: ConstraintDSL script (TransitionComp script) +ctxComp = askC @CComp -- Main API --- FIXME: move IsData here (now it breaks Plutus compilation) +data NoTransitionComp = MkNoTransitionComp + deriving stock (Prelude.Eq, Prelude.Show) + type DefaultConstraints datatype = ( Prelude.Eq datatype , Prelude.Show datatype + , PlutusTx.UnsafeFromData datatype + , PlutusTx.FromData datatype + , PlutusTx.ToData datatype ) {- | All associated types for `CEMScript` They are separated to simplify TH deriving -} class CEMScriptTypes script where - -- \| `Params` is immutable part of script Datum, - -- \| it should be used to encode all + -- \| `Params` is immutable part of script Datum type Params script = params | params -> script - -- | `Stage` is datatype encoding all `Interval`s specified by script. - -- | `Stage` logic is encoded by separate `Stages` type class. - -- | It have separate `StageParams` datatype, - -- | which is stored immutable in script Datum as well. - type Stage script - - type Stage script = SingleStage - -- | `State` is changing part of script Datum. -- | It is in type State script = params | params -> script @@ -101,69 +468,53 @@ class CEMScriptTypes script where -- | Transitions for deterministic CEM-machine type Transition script = transition | transition -> script + -- | See `transitionComp` + type TransitionComp script + + type TransitionComp script = NoTransitionComp + +type CEMScriptSpec resolved script = + ( Map.Map + (Spine (Transition script)) + [TxConstraint resolved script] + ) + +data CompilationConfig = MkCompilationConfig + { errorCodesPrefix :: String + } + class - ( HasSpine (Transition script) + ( HasPlutusSpine (Transition script) , HasSpine (State script) - , Stages (Stage script) - , DefaultConstraints (Stage script) + , HasSpine (Params script) , DefaultConstraints (Transition script) , DefaultConstraints (State script) , DefaultConstraints (Params script) - , DefaultConstraints (StageParams (Stage script)) + , DefaultConstraints (TransitionComp script) , CEMScriptTypes script ) => CEMScript script where - -- | Each kind of Transition has statically associated Stage - -- from/to `State`s spines - transitionStage :: - Proxy script -> - Map.Map - (Spine (Transition script)) - ( Stage script - , Maybe (Spine (State script)) - , Maybe (Spine (State script)) + -- | Plutus script to calculate things, + -- if DSL and inlining Plutarch functions are not expresisble enough + transitionComp :: + Maybe + ( Params script -> + State script -> + Transition script -> + TransitionComp script ) + {-# INLINEABLE transitionComp #-} + transitionComp = Nothing - -- This functions define domain logic - transitionSpec :: - Params script -> - Maybe (State script) -> - Transition script -> - Either BuiltinString (TransitionSpec script) - -data TransitionSpec script = MkTransitionSpec - { constraints :: [TxFanConstraint script] - , -- List of additional signers (in addition to one required by TxIns) - signers :: [PubKeyHash] - } - deriving stock (Show) - --- | List of all signing keys required for transition spec -getAllSpecSigners :: TransitionSpec script -> [PubKeyHash] -getAllSpecSigners spec = signers spec ++ txInPKHs - where - txInPKHs = mapMaybe getPubKey $ filter ((Prelude.== In) . txFanCKind) $ constraints spec - getPubKey c = case address (txFanCFilter c) of - ByPubKey key -> Just key - _ -> Nothing - -{- | Static part of CEMScript datum. -Datatype is actually used only by off-chain code due to Plutus limitations. --} -data CEMParams script = MkCEMParams - { scriptParams :: Params script - , stagesParams :: StageParams (Stage script) - } + -- | This map defines constraints for each transition via DSL + perTransitionScriptSpec :: CEMScriptSpec False script -deriving stock instance (CEMScript script) => (Show (CEMParams script)) -deriving stock instance (CEMScript script) => (Prelude.Eq (CEMParams script)) + compilationConfig :: CompilationConfig --- FIXME: documentation -type CEMScriptDatum script = - (StageParams (Stage script), Params script, State script) +-- FIXME: No need to use type synonym anymore (was needed due to Plutus) +type CEMScriptDatum script = (Params script, State script) -- TH deriving done at end of file for GHC staging reasons -deriveShow ''TxFanKind -deriveShow ''TxFanFilter' +derivePlutusSpine ''NoTransitionComp diff --git a/src/Cardano/CEM/DSL.hs b/src/Cardano/CEM/DSL.hs new file mode 100644 index 0000000..bbdf0f9 --- /dev/null +++ b/src/Cardano/CEM/DSL.hs @@ -0,0 +1,171 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE RecordWildCards #-} + +module Cardano.CEM.DSL where + +import Prelude + +import Data.Map qualified as Map + +import Data.Text (pack, unpack) +import Text.Show.Pretty (ppShowList) + +import Cardano.CEM +import Data.Maybe (listToMaybe, mapMaybe) +import Data.Spine (HasSpine (..)) +import PlutusLedgerApi.V1 (PubKeyHash) + +-- Generic check datatypes + +-- | We have abstract interpretator at home +data CheckResult = Yes | No | Maybe + deriving stock (Eq, Show) + +opposite :: Ordering -> Ordering +opposite EQ = EQ +opposite LT = GT +opposite GT = LT + +instance Ord CheckResult where + compare Yes No = EQ + compare Yes Maybe = GT + compare No Maybe = GT + compare Yes Yes = EQ + compare No No = EQ + compare Maybe Maybe = EQ + compare x y = opposite $ compare y x + +-- Checks + +sameScriptStateSpinesOfKind :: + forall script. + (CEMScript script) => + TxFanKind -> + TxConstraint False script -> + [Spine (State script)] +sameScriptStateSpinesOfKind xKind constr = case constr of + TxFan kind (SameScript state) _ -> + if kind == xKind then [parseSpine state] else [] + If _ t e -> recur t <> (recur e) + MatchBySpine _ caseSwitch -> + foldMap recur (Map.elems caseSwitch) + _ -> [] + where + recur = sameScriptStateSpinesOfKind xKind + parseSpine :: + ConstraintDSL script (State script) -> Spine (State script) + parseSpine (Pure state) = getSpine state + parseSpine (UnsafeOfSpine spine _) = spine + parseSpine (UnsafeUpdateOfSpine _ spine _) = spine + -- FIXME: yet another not-properly DSL type encoded place + parseSpine _ = + error "SameScript is too complex to statically know its spine" + +isSameScriptOfKind :: TxFanKind -> TxConstraint resolved script -> CheckResult +isSameScriptOfKind xKind constr = case constr of + TxFan kind (SameScript _) _ -> + if kind == xKind then Yes else No + If _ t e -> min (recur t) (recur e) + MatchBySpine _ caseSwitch -> + minimum $ map recur (Map.elems caseSwitch) + _ -> No + where + recur = isSameScriptOfKind xKind + +transitionInState :: + [TxConstraint True script] -> Maybe (State script) +transitionInState c = listToMaybe $ mapMaybe f c + where + f (TxFan In (SameScript state) _) = Just state + f _ = Nothing + +transitionStateSpines :: (CEMScript script) => TxFanKind -> [TxConstraint False script] -> [Spine (State script)] +transitionStateSpines kind spec = concat $ map (sameScriptStateSpinesOfKind kind) spec + +transitionInStateSpine :: + (CEMScript script) => + [TxConstraint False script] -> + Maybe (Spine (State script)) +transitionInStateSpine spec = case transitionStateSpines In spec of + [x] -> Just x + [] -> Nothing + _ -> + error + "Transition should not have more than one SameScript In constraint" + +maybeIsCreator :: [TxConstraint resolved script] -> Bool +maybeIsCreator constrs = + not (maybeHasSameScriptFanOfKind In) + && maybeHasSameScriptFanOfKind Out + where + maybeHasSameScriptFanOfKind kind = + any ((/= No) . isSameScriptOfKind kind) constrs + +getMainSigner :: [TxConstraint True script] -> PubKeyHash +getMainSigner cs = case mapMaybe f cs of + [pkh] -> pkh + _ -> + error + "Transition should have exactly one MainSignerCoinSelection constraint" + where + f (MainSignerNoValue pkh) = Just pkh + f (MainSignerCoinSelect pkh _ _) = Just pkh + f _ = Nothing + +-- FIXME: support for reusing error message between transitions in codes +-- FIXME: add golden tests +parseErrorCodes :: + String -> + Map.Map k [TxConstraint resolved script] -> + [(String, String)] +parseErrorCodes prefix spec = + go [] $ concat $ Map.elems spec + where + go table (constraint : rest) = + case constraint of + Error message -> + let + code = prefix <> show (length table) + in + go ((code, unpack message) : table) rest + If _ t e -> go table (t : e : rest) + (MatchBySpine _ caseSwitch) -> + go table (Map.elems caseSwitch ++ rest) + _ -> go table rest + go table [] = reverse table + +substErrors :: + Map.Map String String -> + Map.Map k [TxConstraint a b] -> + Map.Map k [TxConstraint a b] +substErrors mapping spec = + Map.map (map go) spec + where + go (Error message) = Error $ pack $ mapping Map.! unpack message + go (If x t e) = If x (go t) (go e) + go (MatchBySpine @a @b @c s caseSwitch) = + MatchBySpine @a @b @c s $ Map.map go caseSwitch + go x = x + +-- FIXME: check MainSignerCoinSelect, ... + +-- | Checking for errors and normaliing +preProcessForOnChainCompilation :: + (CEMScript script, Show a) => + Map.Map a [TxConstraint False script] -> + Map.Map a [TxConstraint False script] +preProcessForOnChainCompilation spec = + if length possibleCreators == 1 + then + let + -- FIXME: relies on `error` inside... + !_ = map transitionInStateSpine $ Map.elems spec + in + spec + else + error $ + "CEMScript should have exactly 1 creating transition, " + <> "while possible creators are " + <> ppShowList possibleCreators + where + possibleCreators = filter (maybeIsCreator . snd) (Map.toList spec) diff --git a/src/Cardano/CEM/Documentation.hs b/src/Cardano/CEM/Documentation.hs index f9a7faf..4e1a7f2 100644 --- a/src/Cardano/CEM/Documentation.hs +++ b/src/Cardano/CEM/Documentation.hs @@ -7,17 +7,21 @@ import Data.Map qualified as Map import Data.Proxy import Cardano.CEM +import Cardano.CEM.DSL (transitionStateSpines) +import Data.Spine (allSpines) dotStyling :: String dotStyling = "rankdir=LR;\n" <> "node [shape=\"dot\",fontsize=14,fixedsize=true,width=1.5];\n" - <> "edge [fontsize=11];" - <> "\"Void In\" [color=\"orange\"];" - <> "\"Void Out\" [color=\"orange\"];" + <> "edge [fontsize=11];\n" + <> "\"Void In\" [color=\"orange\"];\n" + <> "\"Void Out\" [color=\"orange\"];\n" -cemDotGraphString :: (CEMScript script) => String -> Proxy script -> String -cemDotGraphString name proxy = +-- FIXME: cover with golden test +cemDotGraphString :: + forall script. (CEMScript script) => String -> Proxy script -> String +cemDotGraphString name _proxy = "digraph " <> name <> " {\n" @@ -30,15 +34,18 @@ cemDotGraphString name proxy = stripSpineSuffix = reverse . drop 5 . reverse edges = fold $ - [ maybe "\"Void In\"" showSpine from + [ from <> " -> " - <> maybe "\"Void Out\"" showSpine to + <> to <> " [label=\"" <> showSpine transition - <> " (stage " - <> show stage - <> ")" <> "\"]; \n" - | (transition, (stage, from, to)) <- - Map.assocs $ transitionStage proxy + | transition <- allSpines @(Transition script) + , from <- get In transition + , to <- get Out transition ] + get kind transition = + case transitionStateSpines kind $ + perTransitionScriptSpec @script Map.! transition of + [] -> ["\"Void " <> show kind <> "\""] + x -> map showSpine x diff --git a/src/Cardano/CEM/Examples/Auction.hs b/src/Cardano/CEM/Examples/Auction.hs index 3e69e04..c98a580 100644 --- a/src/Cardano/CEM/Examples/Auction.hs +++ b/src/Cardano/CEM/Examples/Auction.hs @@ -1,23 +1,19 @@ -{-# LANGUAGE NoPolyKinds #-} +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE OverloadedRecordDot #-} module Cardano.CEM.Examples.Auction where import PlutusTx.Prelude import Prelude qualified -import Data.Data (Proxy (..)) import Data.Map qualified as Map import PlutusLedgerApi.V1.Crypto (PubKeyHash) -import PlutusLedgerApi.V1.Interval qualified as Interval -import PlutusLedgerApi.V1.Time (POSIXTime) -import PlutusLedgerApi.V1.Value (CurrencySymbol (..), TokenName (..), singleton) import PlutusLedgerApi.V2 (Value) -import PlutusTx qualified import Cardano.CEM -import Cardano.CEM.Stages (Stages (..)) -import Cardano.CEM.TH (deriveCEMAssociatedTypes, deriveStageAssociatedTypes) +import Cardano.CEM.TH (deriveCEMAssociatedTypes) +import Data.Spine -- Simple no-deposit auction @@ -29,25 +25,16 @@ data Bid = MkBet } deriving stock (Prelude.Eq, Prelude.Show) -data SimpleAuctionStage = Open | Closed - deriving stock (Prelude.Eq, Prelude.Show) - -data SimpleAuctionStageParams - = NoControl - | CanCloseAt POSIXTime - deriving stock (Prelude.Eq, Prelude.Show) - -instance Stages SimpleAuctionStage where - type StageParams SimpleAuctionStage = SimpleAuctionStageParams - stageToOnChainInterval NoControl _ = Interval.always - -- Example: logical error - stageToOnChainInterval (CanCloseAt time) Open = Interval.to time - stageToOnChainInterval (CanCloseAt time) Closed = Interval.from time +derivePlutusSpine ''Bid data SimpleAuctionState = NotStarted - | CurrentBid Bid - | Winner Bid + | CurrentBid + { bid :: Bid + } + | Winner + { bid :: Bid + } deriving stock (Prelude.Eq, Prelude.Show) data SimpleAuctionParams = MkAuctionParams @@ -59,96 +46,115 @@ data SimpleAuctionParams = MkAuctionParams data SimpleAuctionTransition = Create | Start - | MakeBid Bid + | MakeBid + { bid :: Bid + } | Close | Buyout deriving stock (Prelude.Eq, Prelude.Show) -PlutusTx.unstableMakeIsData ''Bid - instance CEMScriptTypes SimpleAuction where - type Stage SimpleAuction = SimpleAuctionStage type Params SimpleAuction = SimpleAuctionParams type State SimpleAuction = SimpleAuctionState type Transition SimpleAuction = SimpleAuctionTransition -$(deriveStageAssociatedTypes ''SimpleAuctionStage) $(deriveCEMAssociatedTypes False ''SimpleAuction) instance CEMScript SimpleAuction where - transitionStage Proxy = + compilationConfig = MkCompilationConfig "AUC" + + perTransitionScriptSpec = Map.fromList - [ (CreateSpine, (Open, Nothing, Just NotStartedSpine)) - , (StartSpine, (Open, Just NotStartedSpine, Just CurrentBidSpine)) - , (MakeBidSpine, (Open, Just CurrentBidSpine, Just CurrentBidSpine)) - , (CloseSpine, (Closed, Just CurrentBidSpine, Just WinnerSpine)) - , (BuyoutSpine, (Closed, Just WinnerSpine, Nothing)) + [ + ( CreateSpine + , + [ MainSignerCoinSelect ctxParams.seller cMinLovelace cEmptyValue + , TxFan Out (SameScript $ Pure NotStarted) scriptStateValue + ] + ) + , + ( StartSpine + , + [ sameScriptIncOfSpine NotStartedSpine + , -- TxFan + -- In + -- (SameScript $ Pure NotStarted) + -- scriptStateValue + TxFan + Out + ( SameScript + $ cOfSpine CurrentBidSpine [#bid ::= initialBid] + ) + scriptStateValue + , MainSignerNoValue ctxParams.seller + ] + ) + , + ( MakeBidSpine + , + [ sameScriptIncOfSpine CurrentBidSpine + , byFlagError + (ctxTransition.bid.betAmount @<= ctxState.bid.betAmount) + "Bid amount is less or equal to current bid" + , TxFan + Out + ( SameScript + $ cOfSpine + CurrentBidSpine + [#bid ::= ctxTransition.bid] + ) + scriptStateValue + , MainSignerNoValue ctxTransition.bid.better + ] + ) + , + ( CloseSpine + , + [ sameScriptIncOfSpine CurrentBidSpine + , TxFan + Out + ( SameScript + $ cOfSpine WinnerSpine [#bid ::= ctxState.bid] + ) + scriptStateValue + , MainSignerNoValue ctxParams.seller + ] + ) + , + ( BuyoutSpine + , + [ sameScriptIncOfSpine WinnerSpine + , -- Example: In constraints redundant for on-chain + offchainOnly + ( MainSignerCoinSelect + buyoutBid.better + ( cMkAdaOnlyValue buyoutBid.betAmount + @<> cMinLovelace + ) + cEmptyValue + ) + , TxFan + Out + (UserAddress ctxParams.seller) + (cMinLovelace @<> cMkAdaOnlyValue buyoutBid.betAmount) + , TxFan + Out + (UserAddress buyoutBid.better) + (cMinLovelace @<> ctxParams.lot) + ] + ) ] - - {-# INLINEABLE transitionSpec #-} - transitionSpec params state transition = case (state, transition) of - (Nothing, Create) -> - Right - $ MkTransitionSpec - { constraints = - [ MkTxFanC - In - (MkTxFanFilter (ByPubKey $ seller params) Anything) - (SumValueEq $ lot params) - , nextState NotStarted - ] - , signers = [] - } - (Just NotStarted, Start) -> - Right - $ MkTransitionSpec - { constraints = [nextState (CurrentBid initialBid)] - , signers = [seller params] - } - (Just (CurrentBid currentBet), MakeBid newBet) -> - -- Example: could be parametrized with param or typeclass - if betAmount newBet > betAmount currentBet - then - Right - $ MkTransitionSpec - { constraints = [nextState (CurrentBid newBet)] - , signers = [better newBet] - } - else Left "Wrong Bid amount" - (Just (CurrentBid currentBet), Close) -> - Right - $ MkTransitionSpec - { constraints = [nextState (Winner currentBet)] - , signers = [seller params] - } - (Just (Winner winnerBet), Buyout {}) -> - Right - $ MkTransitionSpec - { constraints = - [ -- Example: In constraints redundant for on-chain - MkTxFanC - In - (MkTxFanFilter (ByPubKey (better winnerBet)) Anything) - (SumValueEq $ betAdaValue winnerBet) - , MkTxFanC - Out - (MkTxFanFilter (ByPubKey (better winnerBet)) Anything) - (SumValueEq $ lot params) - , MkTxFanC - Out - (MkTxFanFilter (ByPubKey (seller params)) Anything) - (SumValueEq $ betAdaValue winnerBet) - ] - , signers = [] - } - _ -> Left "Incorrect state for transition" where - initialBid = MkBet (seller params) 0 - nextState state' = - MkTxFanC - Out - (MkTxFanFilter BySameScript (bySameCEM state')) - (SumValueEq $ lot params) - betAdaValue = adaValue . betAmount - adaValue = - singleton (CurrencySymbol emptyByteString) (TokenName emptyByteString) + buyoutBid = ctxState.bid + initialBid = + cOfSpine + MkBetSpine + [ #better ::= ctxParams.seller + , #betAmount ::= Pure 0 + ] + scriptStateValue = cMinLovelace @<> ctxParams.lot + sameScriptIncOfSpine spine = + TxFan + In + (SameScript $ cUpdateOfSpine ctxState spine []) + scriptStateValue diff --git a/src/Cardano/CEM/Examples/Compilation.hs b/src/Cardano/CEM/Examples/Compilation.hs index ffcac47..065af4c 100644 --- a/src/Cardano/CEM/Examples/Compilation.hs +++ b/src/Cardano/CEM/Examples/Compilation.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE NoPolyKinds #-} +-- FIXME +{-# OPTIONS_GHC -Wno-missing-signatures #-} {-# OPTIONS_GHC -Wno-orphans #-} -- This warnings work incorrectly in presence of our Plutus code {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} @@ -6,11 +7,11 @@ module Cardano.CEM.Examples.Compilation where -import PlutusLedgerApi.V2 (serialiseCompiledCode) +import Prelude -import Cardano.CEM.Examples.Auction -import Cardano.CEM.Examples.Voting -import Cardano.CEM.TH +import Cardano.CEM.Examples.Auction (SimpleAuction) +import Cardano.CEM.Examples.Voting (SimpleVoting) +import Cardano.CEM.TH (compileCEM) -$(compileCEM ''SimpleAuction) -$(compileCEM ''SimpleVoting) +$(compileCEM True ''SimpleAuction) +$(compileCEM False ''SimpleVoting) diff --git a/src/Cardano/CEM/Examples/Voting.hs b/src/Cardano/CEM/Examples/Voting.hs index a155e6b..56fd19a 100644 --- a/src/Cardano/CEM/Examples/Voting.hs +++ b/src/Cardano/CEM/Examples/Voting.hs @@ -1,6 +1,7 @@ -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} - +{-# LANGUAGE OverloadedLabels #-} +{-# LANGUAGE OverloadedRecordDot #-} {-# HLINT ignore "Use when" #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} module Cardano.CEM.Examples.Voting where @@ -11,12 +12,11 @@ import Data.Map qualified as Map import PlutusLedgerApi.V1.Crypto (PubKeyHash) import PlutusLedgerApi.V2 (Value) -import PlutusTx qualified import PlutusTx.AssocMap qualified as PMap import Cardano.CEM -import Cardano.CEM.Stages import Cardano.CEM.TH (deriveCEMAssociatedTypes) +import Data.Spine -- Voting @@ -25,25 +25,43 @@ data SimpleVoting data VoteValue = Yes | No | Abstain deriving stock (Prelude.Show, Prelude.Eq) +derivePlutusSpine ''VoteValue + instance Eq VoteValue where Yes == Yes = True No == No = True Abstain == Abstain = True _ == _ = False --- | Policy determinig who can vote -data JuryPolicy = Anyone | FixedJuryList [PubKeyHash] | WithToken Value +-- | Policy determining who can vote +data JuryPolicy + = Anyone + | FixedJuryList + { juryList :: [PubKeyHash] + } + | WithToken + { juryAuthTokenValue :: Value + } deriving stock (Prelude.Show, Prelude.Eq) +derivePlutusSpine ''JuryPolicy + -- Votes storage -- | Map from jury to their decision type VoteStorage = PMap.Map PubKeyHash VoteValue -addVote :: PubKeyHash -> VoteValue -> VoteStorage -> Either BuiltinString VoteStorage +data VoteAddResult + = DuplicateVote + | Success {newVoteStorage :: VoteStorage} + deriving stock (Prelude.Eq, Prelude.Show) + +derivePlutusSpine ''VoteAddResult + +addVote :: PubKeyHash -> VoteValue -> VoteStorage -> VoteAddResult addVote jury vote storage = case PMap.lookup jury storage of - Just _ -> traceError "You already casted vote" - Nothing -> Right $ PMap.insert jury vote storage + Nothing -> Success $ PMap.insert jury vote storage + Just {} -> DuplicateVote {-# INLINEABLE countVotes #-} countVotes :: SimpleVotingParams -> VoteStorage -> VoteValue @@ -74,90 +92,140 @@ data SimpleVotingParams = MkVotingParams data SimpleVotingState = NotStarted - | InProgress VoteStorage - | Finalized VoteValue + | InProgress + { votes :: VoteStorage + } + | Finalized + { votingResult :: VoteValue + } deriving stock (Prelude.Show, Prelude.Eq) data SimpleVotingTransition = Create | Start - | Vote PubKeyHash VoteValue + | Vote + { votingJury :: PubKeyHash + , voteValue :: VoteValue + } | Finalize deriving stock (Prelude.Show, Prelude.Eq) -PlutusTx.unstableMakeIsData ''VoteValue -PlutusTx.unstableMakeIsData ''JuryPolicy +data SimpleVotingCalc + = VoteCalc + { votingNotAllowed :: Bool + , voteAddResult :: VoteAddResult + } + | FinalizeCalc {result :: VoteValue} + | NoCalc + deriving stock (Prelude.Eq, Prelude.Show) instance CEMScriptTypes SimpleVoting where type Params SimpleVoting = SimpleVotingParams type State SimpleVoting = SimpleVotingState type Transition SimpleVoting = SimpleVotingTransition + type TransitionComp SimpleVoting = SimpleVotingCalc +derivePlutusSpine ''SimpleVotingCalc $(deriveCEMAssociatedTypes False ''SimpleVoting) instance CEMScript SimpleVoting where - transitionStage _ = - Map.fromList - [ (CreateSpine, (Always, Nothing, Just NotStartedSpine)) - , (StartSpine, (Always, Just NotStartedSpine, Just InProgressSpine)) - , (VoteSpine, (Always, Just InProgressSpine, Just InProgressSpine)) - , (FinalizeSpine, (Always, Just InProgressSpine, Nothing)) - ] + compilationConfig = MkCompilationConfig "VOT" - {-# INLINEABLE transitionSpec #-} - transitionSpec params state transition = - case (state, transition) of - (Nothing, Create) -> - Right - $ MkTransitionSpec - { constraints = [nextScriptState NotStarted] - , signers = [creator params] - } - (Just NotStarted, Start) -> - Right - $ MkTransitionSpec - { constraints = [nextScriptState (InProgress PMap.empty)] - , signers = [creator params] - } - (Just (InProgress votes), Vote jury vote) -> do - -- Check if you can vote - case juryPolicy params of - FixedJuryList allowedJury -> - if jury `notElem` allowedJury - then Left "You are not allowed to vote, not on list" - else return () - _ -> return () - if not (abstainAllowed params) && vote == Abstain - then Left "You cannot vote Abstain in this vote" - else return () - - let allowedToVoteConstraints = - case juryPolicy params of - WithToken value -> - [ MkTxFanC + {-# INLINEABLE transitionComp #-} + transitionComp = Just go + where + go params (InProgress votes) transition = + case transition of + Vote jury vote -> + VoteCalc + { votingNotAllowed = + case juryPolicy params of + FixedJuryList allowedJury -> + jury `notElem` allowedJury + _ -> False + , voteAddResult = addVote jury vote votes + } + Finalize -> FinalizeCalc $ countVotes params votes + _ -> NoCalc + go _ _ _ = NoCalc + + perTransitionScriptSpec = + Map.fromList + [ + ( CreateSpine + , + [ TxFan Out (SameScript $ Pure NotStarted) cMinLovelace + , MainSignerNoValue ctxParams.creator + ] + ) + , + ( StartSpine + , + [ TxFan In (SameScript $ Pure NotStarted) cMinLovelace + , TxFan Out (SameScript $ Pure $ InProgress PMap.empty) cMinLovelace + , MainSignerNoValue ctxParams.creator + ] + ) + , + ( VoteSpine + , + [ sameScriptIncOfSpine InProgressSpine + , MatchBySpine ctxComp.voteAddResult + $ Map.fromList + [ (DuplicateVoteSpine, Error "You already casted vote") + , + ( SuccessSpine + , TxFan + Out + ( SameScript + $ cOfSpine + InProgressSpine + [ #votes + ::= ctxComp.voteAddResult.newVoteStorage + ] + ) + cMinLovelace + ) + ] + , MainSignerNoValue ctxTransition.votingJury + , MatchBySpine ctxParams.juryPolicy + $ Map.fromList + [ + ( WithTokenSpine + , TxFan InRef - (MkTxFanFilter (ByPubKey jury) Anything) - (SumValueEq value) - ] - _ -> [] - - -- Update state - newVoteStorage <- addVote jury vote votes - Right - $ MkTransitionSpec - { constraints = - nextScriptState (InProgress newVoteStorage) - : allowedToVoteConstraints - , signers = [jury] - } - (Just (InProgress votes), Finalize) -> - Right - $ MkTransitionSpec - { constraints = - [nextScriptState $ Finalized (countVotes params votes)] - , signers = [creator params] - } - _ -> Left "Wrong state transition" where + (UserAddress ctxTransition.votingJury) + ctxParams.juryPolicy.juryAuthTokenValue + ) + , (FixedJuryListSpine, Noop) + , (AnyoneSpine, Noop) + ] + , byFlagError + ctxComp.votingNotAllowed + "You are not allowed to vote, not on list" + , byFlagError + ( cNot ctxParams.abstainAllowed + @&& (ctxTransition.voteValue @== Pure Abstain) + ) + "You cannot vote Abstain in this vote" + ] + ) + , + ( FinalizeSpine + , + [ sameScriptIncOfSpine InProgressSpine + , TxFan + Out + ( SameScript + $ cOfSpine + FinalizedSpine + [#votingResult ::= ctxComp.result] + ) + cMinLovelace + , MainSignerNoValue ctxParams.creator + ] + ) + ] where - nextScriptState state' = - MkTxFanC Out (MkTxFanFilter BySameScript (bySameCEM state')) (Exist 1) + sameScriptIncOfSpine spine = + TxFan In (SameScript $ cUpdateOfSpine ctxState spine []) cMinLovelace diff --git a/src/Cardano/CEM/Monads.hs b/src/Cardano/CEM/Monads.hs index 301da94..d4f08fa 100644 --- a/src/Cardano/CEM/Monads.hs +++ b/src/Cardano/CEM/Monads.hs @@ -23,11 +23,9 @@ import Cardano.Extras -- CEMAction and TxSpec -data CEMAction script - = MkCEMAction (CEMParams script) (Transition script) +data CEMAction script = MkCEMAction (Params script) (Transition script) -deriving stock instance - (CEMScript script) => Show (CEMAction script) +deriving stock instance (CEMScript script) => Show (CEMAction script) -- FIXME: use generic Some data SomeCEMAction where @@ -104,7 +102,7 @@ class (MonadBlockchainParams m) => MonadQueryUtxo m where data ResolvedTx = MkResolvedTx { txIns :: [(TxIn, TxInWitness)] - , txInsReference :: [TxIn] + , txInRefs :: [TxIn] , txOuts :: [TxOut CtxTx Era] , toMint :: TxMintValue BuildTx Era , interval :: Interval POSIXTime @@ -126,16 +124,17 @@ data TxSubmittingError -- | Error occurred while trying to execute CEMScript transition data TransitionError - = StateMachineError - { errorMessage :: String - } - | MissingTransitionInput + = CannotFindTransitionInput + | CompilationError String + | SpecExecutionError {errorMessage :: String} deriving stock (Show, Eq) data TxResolutionError - = TxSpecIsIncorrect - | MkTransitionError SomeCEMAction TransitionError - | UnhandledSubmittingError TxSubmittingError + = CEMScriptTxInResolutionError + | -- FIXME: record transition and action involved + PerTransitionErrors [TransitionError] + | -- FIXME: this is weird + UnhandledSubmittingError TxSubmittingError deriving stock (Show) -- | Ability to send transaction to chain diff --git a/src/Cardano/CEM/Monads/L1Commons.hs b/src/Cardano/CEM/Monads/L1Commons.hs index ff38b70..7379f1d 100644 --- a/src/Cardano/CEM/Monads/L1Commons.hs +++ b/src/Cardano/CEM/Monads/L1Commons.hs @@ -10,7 +10,7 @@ import Data.Map qualified as Map -- Cardano imports import Cardano.Api hiding (queryUtxo) -import Cardano.Api.Shelley (LedgerProtocolParameters (..), Tx (..)) +import Cardano.Api.Shelley (LedgerProtocolParameters (..)) -- Project imports import Cardano.CEM.Monads @@ -46,7 +46,7 @@ cardanoTxBodyFromResolvedTx (MkResolvedTx {..}) = do , txInsCollateral = TxInsCollateral AlonzoEraOnwardsBabbage feeTxIns , txInsReference = - TxInsReference BabbageEraOnwardsBabbage txInsReference + TxInsReference BabbageEraOnwardsBabbage txInRefs , txOuts , txMintValue = toMint , -- Adding all keys here, cuz other way `txSignedBy` does not see those diff --git a/src/Cardano/CEM/OffChain.hs b/src/Cardano/CEM/OffChain.hs index c4c5caf..79cd54e 100644 --- a/src/Cardano/CEM/OffChain.hs +++ b/src/Cardano/CEM/OffChain.hs @@ -7,19 +7,18 @@ import Prelude -- Haskell imports import Control.Concurrent (threadDelay) +import Control.Monad (when) import Data.Bifunctor (Bifunctor (..)) import Data.Data (Proxy (..)) -import Data.List (find) +import Data.List (find, nub) import Data.Map qualified as Map +import Data.Maybe (fromJust) +import Data.Spine (HasSpine (getSpine)) -import PlutusLedgerApi.V1.Address (Address) -import PlutusLedgerApi.V2 ( - UnsafeFromData (..), - always, - fromData, - ) +import PlutusLedgerApi.V1.Address (Address, pubKeyHashAddress) +import PlutusLedgerApi.V2 (PubKeyHash, always, fromData) -import Cardano.Api hiding (Address, In, Out, queryUtxo, txIns) +import Cardano.Api hiding (Address, In, Out, queryUtxo, txIns, txOuts) import Cardano.Api.Shelley ( PlutusScript (..), ReferenceScript (..), @@ -27,13 +26,15 @@ import Cardano.Api.Shelley ( toPlutusData, ) +import Plutarch.Script (serialiseScript) + -- Project imports import Cardano.CEM +import Cardano.CEM.DSL import Cardano.CEM.Monads import Cardano.CEM.OnChain (CEMScriptCompiled (..), cemScriptAddress) import Cardano.Extras -import Data.Spine (HasSpine (getSpine)) fromPlutusAddressInMonad :: (MonadBlockchainParams m) => Address -> m (AddressInEra Era) @@ -63,24 +64,20 @@ failLeft :: (MonadFail m, Show s) => Either s a -> m a failLeft (Left errorMsg) = fail $ show errorMsg failLeft (Right value) = return value --- TODO: use regular CEMScript -cemTxOutDatum :: (CEMScriptCompiled script) => TxOut ctx Era -> Maybe (CEMScriptDatum script) +cemTxOutDatum :: + (CEMScript script) => TxOut ctx Era -> Maybe (CEMScriptDatum script) cemTxOutDatum txOut = fromData =<< toPlutusData <$> getScriptData <$> mTxOutDatum txOut cemTxOutState :: (CEMScriptCompiled script) => TxOut ctx Era -> Maybe (State script) -cemTxOutState txOut = - let - getState (_, _, state) = state - in - getState <$> cemTxOutDatum txOut +cemTxOutState txOut = snd <$> cemTxOutDatum txOut queryScriptTxInOut :: forall m script. ( MonadQueryUtxo m , CEMScriptCompiled script ) => - CEMParams script -> + Params script -> m (Maybe (TxIn, TxOut CtxUTxO Era)) queryScriptTxInOut params = do utxo <- queryUtxo $ ByAddresses [scriptAddress] @@ -90,7 +87,7 @@ queryScriptTxInOut params = do pairs -> find hasSameParams pairs hasSameParams (_, txOut) = case cemTxOutDatum txOut of - Just (p1, p2, _) -> params == MkCEMParams p2 p1 + Just (p, _) -> params == p Nothing -> False -- May happen in case of changed Datum encoding return mScriptTxIn where @@ -101,121 +98,170 @@ queryScriptState :: ( MonadQueryUtxo m , CEMScriptCompiled script ) => - CEMParams script -> + Params script -> m (Maybe (State script)) queryScriptState params = do mTxInOut <- queryScriptTxInOut params return (cemTxOutState . snd =<< mTxInOut) -resolveAction :: - forall m. - (MonadQueryUtxo m, MonadSubmitTx m) => - SomeCEMAction -> - m (Either TxResolutionError ResolvedTx) -resolveAction - someAction@(MkSomeCEMAction @script (MkCEMAction params transition)) = - -- Add script TxIn +-- FIXME: doc, naming +data Resolution + = TxInR (TxIn, TxInWitness) + | TxInRefR (TxIn, TxInWitness) + | TxOutR (TxOut CtxTx Era) + | AdditionalSignerR PubKeyHash + | NoopR + deriving stock (Show, Eq) - runExceptT $ do - mScriptTxIn' <- lift $ queryScriptTxInOut params +construct :: [Resolution] -> ResolvedTx +construct rs = constructGo rs emptyResolvedTx + where + emptyResolvedTx = + MkResolvedTx + { txIns = [] + , txInRefs = [] + , txOuts = [] + , toMint = TxMintNone + , additionalSigners = [] + , signer = error "TODO: Unreachable laziness trick" + , -- FIXME + interval = always + } + constructGo (r : rest) !acc = + let newAcc = case r of + TxInR x -> acc {txIns = x : txIns acc} + TxInRefR x -> acc {txInRefs = fst x : txInRefs acc} + TxOutR x -> acc {txOuts = x : txOuts acc} + AdditionalSignerR s -> + acc {additionalSigners = s : additionalSigners acc} + NoopR -> acc + in constructGo rest newAcc + constructGo [] !acc = acc +compileActionConstraints :: + forall script. + (CEMScriptCompiled script) => + Maybe (State script) -> + CEMAction script -> + Either TxResolutionError [TxConstraint True script] +compileActionConstraints + mState + (MkCEMAction params transition) = + runExcept $ do let - -- TODO - mScriptTxIn = case transitionStage (Proxy :: Proxy script) Map.! getSpine transition of - (_, Nothing, _) -> Nothing - _ -> mScriptTxIn' - mState = cemTxOutState =<< snd <$> mScriptTxIn - witnesedScriptTxIns = - case mScriptTxIn of - Just (txIn, _) -> - let - scriptWitness = - mkInlinedDatumScriptWitness - (PlutusScriptSerialised @PlutusLang script) - transition - in - [(txIn, scriptWitness)] - Nothing -> [] - - scriptTransition <- case transitionSpec (scriptParams params) mState transition of - Left errorMessage -> - throwError $ - MkTransitionError someAction (StateMachineError $ show errorMessage) - Right result -> return result - - -- Coin-select + uncompiled = + perTransitionScriptSpec @script + Map.! getSpine transition + xSpine = transitionInStateSpine uncompiled + + when (fmap getSpine mState /= xSpine) $ + throwError CEMScriptTxInResolutionError let - byKind kind = - filter (\x -> txFanCKind x == kind) $ - constraints scriptTransition - - txInsPairs <- concat <$> mapM resolveTxIn (byKind In) - txOuts <- concat <$> mapM compileTxConstraint (byKind Out) - - return $ - MkResolvedTx - { txIns = witnesedScriptTxIns <> map fst txInsPairs - , txInsReference = [] - , txOuts - , toMint = TxMintNone - , additionalSigners = signers scriptTransition - , signer = error "TODO" - , interval = always - } - where - script = cemScriptCompiled (Proxy :: Proxy script) - scriptAddress = cemScriptAddress (Proxy :: Proxy script) - resolveTxIn (MkTxFanC _ (MkTxFanFilter addressSpec _) _) = do + -- FIXME: fromJust laziness trick + datum = (params, fromJust mState) + compiled' = map (compileConstraint datum transition) uncompiled + + -- FIXME: raise lefts from compiled + let f x = case x of + Left message -> throwError $ PerTransitionErrors [CompilationError message] + Right x' -> return x' + -- FIXME: add resolution logging + mapM f compiled' + +process :: + forall script m. + (MonadQueryUtxo m, CEMScriptCompiled script) => + CEMAction script -> + TxConstraint True script -> + ExceptT TxResolutionError m Resolution +process (MkCEMAction params transition) ec = case ec of + Noop -> return NoopR + c@MainSignerCoinSelect {} -> do + utxo <- lift $ queryUtxo $ ByAddresses [pubKeyHashAddress $ user c] + let utxoPairs = + map (withKeyWitness . fst) $ Map.toList $ unUTxO utxo + -- FIXME: do actuall coin selection + return $ TxInR $ head utxoPairs + (TxFan kind fanFilter value) -> do + case kind of + Out -> do + let value' = convertTxOut $ fromPlutusValue value + address' <- lift $ fromPlutusAddressInMonad address + return $ + TxOutR $ + TxOut address' value' outTxDatum ReferenceScriptNone + someIn -> do utxo <- lift $ queryUtxo $ ByAddresses [address] - return $ map (\(x, y) -> (withKeyWitness x, y)) $ Map.toList $ unUTxO utxo + let + utxoPairs = Map.toList $ unUTxO utxo + matchingUtxos = + map (addWittness . fst) $ filter predicate utxoPairs + case matchingUtxos of + x : _ -> return $ case someIn of + -- FIXME: log/fail on >1 options to choose for script + In -> TxInR x + InRef -> TxInRefR x + [] -> + throwError $ PerTransitionErrors [CannotFindTransitionInput] + where + predicate (_, txOut) = + txOutValue txOut == fromPlutusValue value + && case fanFilter of + -- FIXME: refactor DRY + SameScript state -> + cemTxOutDatum txOut + == Just + ( params + , state + ) + UserAddress {} -> True + + (address, outTxDatum) = case fanFilter of + UserAddress pkh -> (pubKeyHashAddress pkh, TxOutDatumNone) + SameScript state -> + ( scriptAddress + , mkInlineDatum + ( params + , state + ) + ) + -- FIXME: understand what is happening + convertTxOut x = + TxOutValueShelleyBased shelleyBasedEra $ toMaryValue x + addWittness = case fanFilter of + UserAddress {} -> withKeyWitness + SameScript {} -> (,scriptWitness) where - address = addressSpecToAddress scriptAddress addressSpec - compileTxConstraint - (MkTxFanC _ (MkTxFanFilter addressSpec filterSpec) quantor) = do - address' <- lift $ fromPlutusAddressInMonad address - let compiledTxOut value = - TxOut address' value datum ReferenceScriptNone - return $ case quantor of - Exist n -> replicate (fromInteger n) $ compiledTxOut minUtxoValue - SumValueEq value -> [compiledTxOut $ (convertTxOut $ fromPlutusValue value) <> minUtxoValue] - where - datum = case filterSpec of - Anything -> TxOutDatumNone - ByDatum datum' -> mkInlineDatum datum' - -- FIXME: Can be optimized via Plutarch - UnsafeBySameCEM newState -> - let - cemDatum :: CEMScriptDatum script - cemDatum = - ( stagesParams params - , scriptParams params - , unsafeFromBuiltinData newState - ) - in - mkInlineDatum cemDatum - address = addressSpecToAddress scriptAddress addressSpec - -- TODO: protocol params - -- calculateMinimumUTxO era txout bpp - minUtxoValue = convertTxOut $ lovelaceToValue 3_000_000 - -- TODO - convertTxOut x = - TxOutValueShelleyBased shelleyBasedEra $ toMaryValue x + scriptWitness = + mkInlinedDatumScriptWitness + (PlutusScriptSerialised @PlutusLang $ serialiseScript script) + transition + MainSignerNoValue pkh -> return $ AdditionalSignerR pkh + Error message -> + throwError $ + PerTransitionErrors [SpecExecutionError $ show message] + where + script = cemScriptCompiled (Proxy :: Proxy script) + scriptAddress = cemScriptAddress (Proxy :: Proxy script) resolveTx :: + forall m. (MonadQueryUtxo m, MonadSubmitTx m, MonadIO m) => TxSpec -> m (Either TxResolutionError ResolvedTx) resolveTx spec = runExceptT $ do - -- Get specs - !actionsSpecs <- mapM (ExceptT . resolveAction) $ actions spec - - -- Merge specs - let - mergedSpec' = head actionsSpecs - mergedSpec = (mergedSpec' :: ResolvedTx) {signer = specSigner spec} - - return mergedSpec + !resolutions <- mapM resolveSomeAction (actions spec) + let resolvedTx = construct $ nub $ concat resolutions + return $ resolvedTx {signer = specSigner spec} + where + resolveSomeAction :: + SomeCEMAction -> (ExceptT TxResolutionError m) [Resolution] + resolveSomeAction (MkSomeCEMAction @script action) = do + let MkCEMAction params _ = action + mScript <- lift $ queryScriptState params + cs <- ExceptT $ return $ compileActionConstraints mScript action + mapM (process action) cs resolveTxAndSubmit :: (MonadQueryUtxo m, MonadSubmitTx m, MonadIO m) => diff --git a/src/Cardano/CEM/OnChain.hs b/src/Cardano/CEM/OnChain.hs index 44ef329..275a573 100644 --- a/src/Cardano/CEM/OnChain.hs +++ b/src/Cardano/CEM/OnChain.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE NoPolyKinds #-} +{-# LANGUAGE OverloadedRecordDot #-} +{-# LANGUAGE QualifiedDo #-} -- This warnings work incorrectly in presence of our Plutus code {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} {-# OPTIONS_GHC -Wno-unused-local-binds #-} @@ -8,157 +9,356 @@ module Cardano.CEM.OnChain ( CEMScriptCompiled (..), cemScriptAddress, - genericCEMScript, + genericPlutarchScript, ) where -import PlutusTx.Prelude +import Prelude -import Data.Proxy (Proxy) -import Language.Haskell.TH (conT) -import Language.Haskell.TH.Syntax (Exp, Name, Q) +import PlutusTx qualified -import PlutusLedgerApi.Common (SerialisedScript) -import PlutusLedgerApi.V1.Address (Address, scriptHashAddress) -import PlutusLedgerApi.V1.Interval (always, contains) -import PlutusLedgerApi.V1.Scripts (Datum (..)) -import PlutusLedgerApi.V1.Value (geq) -import PlutusLedgerApi.V2.Contexts ( - TxInInfo (..), - TxInfo (..), - TxOut (..), - findOwnInput, - scriptContextTxInfo, - ) -import PlutusLedgerApi.V2.Tx (OutputDatum (..)) -import PlutusTx.IsData (FromData, ToData (toBuiltinData), UnsafeFromData (..)) -import PlutusTx.Show (Show (..)) +import Data.Map qualified as Map +import Data.Singletons +import Data.String (IsString (..)) -import Cardano.CEM -import Cardano.CEM.Stages +import Plutarch +import Plutarch.Bool +import Plutarch.Builtin +import Plutarch.Extras +import Plutarch.FFI (foreignImport) +import Plutarch.LedgerApi +import Plutarch.LedgerApi.AssocMap qualified as PMap +import Plutarch.LedgerApi.Value +import Plutarch.List +import Plutarch.Monadic qualified as P +import Plutarch.Prelude +import Plutarch.Script (serialiseScript) +import Plutarch.Unsafe (punsafeCoerce) import Plutus.Extras (scriptValidatorHash) +import PlutusLedgerApi.V1.Address (Address, scriptHashAddress) +import PlutusLedgerApi.V2 (BuiltinData) +import Text.Show.Pretty (ppShow) + +import Cardano.CEM hiding (compileDsl) +import Data.Spine + +-- Interfaces + +class (CEMScript script) => CEMScriptCompiled script where + -- | Code, original error message + -- FIXME: track transition it might be raised + errorCodes :: Proxy script -> [(String, String)] -class (CEMScript script, CEMScriptIsData script) => CEMScriptCompiled script where - cemScriptCompiled :: Proxy script -> SerialisedScript + cemScriptCompiled :: Proxy script -> Script {-# INLINEABLE cemScriptAddress #-} cemScriptAddress :: forall script. (CEMScriptCompiled script) => Proxy script -> Address cemScriptAddress = - scriptHashAddress . scriptValidatorHash . cemScriptCompiled + scriptHashAddress . scriptValidatorHash . serialiseScript . cemScriptCompiled -type IsData x = (UnsafeFromData x, FromData x, ToData x) +-- Compilation -type CEMScriptIsData script = - ( UnsafeFromData (Transition script) - , IsData (StageParams (Stage script)) - , IsData (Params script) - , IsData (Transition script) - , IsData (State script) - ) +commonChecks :: Term s (PTxInfo :--> PUnit) +commonChecks = plam go + where + go :: Term s1 PTxInfo -> Term s1 PUnit + go txInfo = + pif + (stackingStuffDisabled txInfo) + (pconstant ()) + (ptraceInfo "Stacking feature used" perror) + stackingStuffDisabled :: Term s1 PTxInfo -> Term s1 PBool + stackingStuffDisabled txInfo = + (pnull # pfromData (pfield @"dcert" # txInfo)) + #&& (PMap.pnull #$ pfromData (pfield @"wdrl" # txInfo)) --- Various hacks and type annotations are done due to Plutus limitations --- Typed quasi-quotes do not allow type splicing, so we need use untyped --- Fields bug - https://gitlab.haskell.org/ghc/ghc/-/merge_requests/8686 --- Data family - not supported - --- https://github.com/IntersectMBO/plutus/issues/5768 --- Type family mentioning: https://github.com/IntersectMBO/plutus/issues/5769 +compileSpineCaseSwitch :: + forall x sop s. + (HasPlutusSpine sop) => + Term s PInteger -> + (Spine sop -> Term s x) -> + Term s x +compileSpineCaseSwitch spineIndex caseSwitchFunc = + go [Prelude.minBound .. Prelude.maxBound] + where + go [] = perror + go (spine : ss) = (checkSpineIf spine) (go ss) + checkSpineIf !spine !cont = + ( pif + (spineIndex #== pconstant (Prelude.toInteger $ Prelude.fromEnum spine)) + ( ptraceDebug + ( pconstant $ + fromString $ + "Matched spine: " <> Prelude.show spine + ) + (caseSwitchFunc spine) + ) + cont + ) -{-# INLINEABLE genericCEMScript #-} -genericCEMScript :: - Name -> - Name -> - Q Exp -genericCEMScript script scriptStage = - [| - \datum' redeemer' context' -> - let - checkTxFan' filterSpec' fan = - case filterSpec' of - Anything -> True - UnsafeBySameCEM stateData -> - let - -- FIXUP: do not decode unnecessary - changedState = - unsafeFromBuiltinData stateData :: State $(conT script) - stateChangeDatum = (stageParams, params, stateData) - stateChangeDatumBS = toBuiltinData stateChangeDatum - in - checkTxFan' (ByDatum stateChangeDatumBS) fan - ByDatum expectedDatum -> - let - TxOut _ _ datum _ = fan - in - case datum of - OutputDatum datumContent -> - getDatum datumContent == expectedDatum - OutputDatumHash _ -> traceError "Hash datum not supported" - _ -> False - checkConstraint (MkTxFanC fanKind filterSpec quantifier) = - traceIfFalse ("Checking constraint " <> show fanKind <> " " <> show datumSpec) - $ checkQuantifier - $ filter checkTxFan fans +genericPlutarchScript :: + forall script. + (CEMScript script) => + CEMScriptSpec False script -> + (Maybe (PlutusTx.CompiledCode (BuiltinData -> BuiltinData -> BuiltinData -> BuiltinData))) -> + ClosedTerm (PData :--> PData :--> PAsData PScriptContext :--> PUnit) +genericPlutarchScript spec code = + phoistAcyclic $ plam main + where + main :: + forall s. + Term s PData -> + Term s PData -> + Term s (PAsData PScriptContext) -> + Term s PUnit + main datum redm ctx' = P.do + ctx <- pletFields @'["txInfo"] ctx' + ownAddress <- plet $ getOwnAddress # ctx' + spineIndex <- plet $ pfstBuiltin # (pasConstr # redm) + comp <- plet $ pdelay $ case code of + Just x -> + let + script :: ClosedTerm (PData :--> PData :--> PData :--> PData) + script = foreignImport x + in + script # params # state # redm + Nothing -> ptraceInfo "Unreachable" perror + perSpineChecks ctx.txInfo ownAddress comp spineIndex + where + params = datumTupleOf 0 + state = datumTupleOf 1 + datumTupleOf ix = getRecordField ix datum + getRecordField ix d = ptryIndex ix $ psndBuiltin # (pasConstr # d) + perSpineChecks txInfo ownAddress comp spineIndex = + compileSpineCaseSwitch spineIndex f where - MkTxFanFilter addressSpec datumSpec = filterSpec - checkTxFan fan = - checkTxFanAddress ownAddress addressSpec fan - && checkTxFan' datumSpec fan - fans = case fanKind of - In -> map txInInfoResolved $ txInfoInputs info - InRef -> map txInInfoResolved $ txInfoReferenceInputs info - Out -> txInfoOutputs info - checkQuantifier txFans = - case quantifier of - SumValueEq value -> - foldMap txOutValue txFans `geq` value - Exist n -> length txFans == n - - params :: Params $(conT script) - stageParams :: StageParams ($(conT scriptStage)) - ownDatum :: CEMScriptDatum $(conT script) - ownDatum = unsafeFromBuiltinData datum' - (stageParams, params, state) = ownDatum - transition :: Transition $(conT script) - transition = unsafeFromBuiltinData redeemer' - context = unsafeFromBuiltinData context' - info = scriptContextTxInfo context - ownAddress = case findOwnInput context of - Just x -> txOutAddress $ txInInfoResolved x - Nothing -> traceError "Impossible happened" - transitionSpec' = transitionSpec @($(conT script)) - stageToOnChainInterval' = stageToOnChainInterval @($(conT scriptStage)) - result = - case transitionSpec' params (Just state) transition of - Right (MkTransitionSpec @($(conT script)) constraints signers) -> - -- do transition - traceIfFalse - "Some constraint not matching" - (all checkConstraint constraints) - -- check signers - && traceIfFalse - "Wrong signers list" - (signers `isSubSetOf` txInfoSignatories info) - -- check stage - && let - expectedInterval = - always - in - -- stageToOnChainInterval' stageParams (traceError "TODO") - - traceIfFalse "Wrong interval for transition stage" - $ expectedInterval - `contains` txInfoValidRange info - Left _ -> traceIfFalse "Wrong transition" False - in - if result - then () - else error () - |] - -{-# INLINEABLE checkTxFanAddress #-} -checkTxFanAddress :: Address -> AddressSpec -> TxOut -> Bool -checkTxFanAddress ownAddress addressSpec fan = - txOutAddress fan == addressSpecToAddress ownAddress addressSpec - -{-# INLINEABLE isSubSetOf #-} -isSubSetOf :: (Eq a) => [a] -> [a] -> Bool -isSubSetOf xs ys = all (`elem` ys) xs + f = perTransitionCheck txInfo ownAddress redm comp + perTransitionCheck txInfo ownAddress transition comp transitionSpine = P.do + ptraceDebug (pconstant $ fromString $ "Checking transition " <> Prelude.show transitionSpine) $ + constraintChecks + where + -- FIXME: fold better + constraintChecks = P.do + pif + ( foldr (\x y -> pand' # x # y) (pconstant True) $ + map compileConstr constrs + ) + (commonChecks # pfromData txInfo) + (ptraceInfoError "Constraint check failed") + compileConstr :: TxConstraint False script -> Term s PBool + compileConstr c = + ptraceInfoIfFalse + ( pconstant $ fromString $ "Checking constraint " <> Prelude.show c + ) + $ case c of + MainSignerCoinSelect pkhDsl inValueDsl outValueDsl -> + P.do + -- FIXME: check final difference + -- FIXME: DRY with TxSpec implemenation + let + txIns = resolve #$ pfromData $ pfield @"inputs" # txInfo + txOuts = pfromData $ pfield @"outputs" # txInfo + punsafeCoerce (compileDsl inValueDsl) + #<= (txFansValue txIns) + #&& (punsafeCoerce (compileDsl outValueDsl) #<= (txFansValue txOuts)) + where + merge :: + Term + s + ( PValue Unsorted NonZero + :--> ( (PValue Sorted NonZero) + :--> PValue Sorted NonZero + ) + ) + merge = plam $ \x y -> ((passertSorted # x) <> y) + mapGetValues :: + Term + s + (PBuiltinList PTxOut :--> PBuiltinList (PValue Unsorted NonZero)) + mapGetValues = + pmap + # plam (\x -> pforgetSorted $ pforgetPositive $ pfromData $ pfield @"value" # x) + resolve = + pmap # plam (\x -> pfromData $ pfield @"resolved" # x) + predicate :: Term s (PTxOut :--> PBool) + predicate = plam $ \txOut -> + (ppkhAddress #$ punsafeCoerce $ compileDsl pkhDsl) + #== pfromData (pfield @"address" # txOut) + txFansValue txIns = + let validTxIns = pfilter # predicate # txIns + in pfoldr + # merge + # (passertSorted #$ pMkAdaOnlyValue # 0) + #$ mapGetValues + # validTxIns + TxFan fanKind fanSpec value -> + let + resolve = + pmap # plam (\x -> pfromData $ pfield @"resolved" # x) + fanList :: Term s (PBuiltinList PTxOut) + fanList = case fanKind of + In -> + resolve #$ pfromData $ pfield @"inputs" # txInfo + InRef -> resolve #$ pfield @"referenceInputs" # txInfo + Out -> pfromData $ pfield @"outputs" # txInfo + predicate = plam $ \txOut -> case fanSpec of + UserAddress pkhDsl -> + let + correctAddress = + (ppkhAddress #$ punsafeCoerce $ compileDsl pkhDsl) + #== pfromData (pfield @"address" # txOut) + in + correctAddress + SameScript expectedState -> + pmatch (pfromData (pfield @"datum" # txOut)) $ \case + POutputDatum datum' -> P.do + PDatum fanDatum <- + pmatch $ pfromData $ pfield @"outputDatum" # datum' + let + fanParams = getRecordField 0 fanDatum + fanState = getRecordField 1 fanDatum + ( (ownAddress #== pfield @"address" # txOut) + #&& ( (checkDsl expectedState fanState) + #&& fanParams + #== params + ) + ) + _ -> pconstant False + in + -- FIXME: do not use phead + checkDsl + value + (punsafeCoerce $ pfield @"value" #$ phead #$ pfilter # predicate # fanList) + MainSignerNoValue dsl -> + let + signatories = pfromData $ pfield @"signatories" # txInfo + xSigner = punsafeCoerce $ pdata (compileDsl dsl) + in + ptraceInfoIfFalse (pshow xSigner) $ + ptraceInfoIfFalse (pshow signatories) $ + pelem # xSigner # signatories + Noop -> pconstant True + Error message -> ptraceInfoError $ pconstant message + If condDsl thenDsl elseDsl -> + pif + (pfromData $ punsafeCoerce $ compileDsl condDsl) + (compileConstr thenDsl) + (compileConstr elseDsl) + MatchBySpine valueDsl caseSwitch -> + let + value = punsafeCoerce $ compileDsl valueDsl + valueSpineNum = pfstBuiltin # (pasConstr # value) + in + compileSpineCaseSwitch + valueSpineNum + (compileConstr . (caseSwitch Map.!)) + checkDsl :: + ConstraintDSL script1 x -> + Term s PData -> + Term s PBool + checkDsl expectationDsl value = + case expectationDsl of + Anything -> pconstant True + UnsafeOfSpine spine setters -> + (pfstBuiltin #$ pasConstr # xValue) + #== pconstant (Prelude.toInteger $ Prelude.fromEnum spine) + #&& let + fields = (psndBuiltin #$ pasConstr # xValue) + ixAndSetters = zip [(0 :: Integer) ..] setters + perIxCheck (ix, (_ ::= fieldValueDsl)) = + checkDsl fieldValueDsl $ ptryIndex (fromInteger ix) fields + foldAnd (!x : xs) = x #&& (foldAnd xs) + foldAnd [] = pconstant True + in + foldAnd $ + map perIxCheck ixAndSetters + _ -> xValue #== value + where + xValue = compileDsl expectationDsl + -- FIXME: Some typing? `newtype MyPData x`? + -- ConstraintDSL script1 (PLifted x) -> Term s (AsData x) + compileDsl :: forall script1 x. ConstraintDSL script1 x -> Term s PData + compileDsl dsl = punsafeCoerce $ case dsl of + Pure x -> pconstant $ PlutusTx.toData x + IsOnChain -> compileDsl $ Pure True + -- XXX: returns PBuiltinList PData in fact + Ask @cvar @_ @dt Proxy -> + case sing @cvar of + SCParams -> params + SCState -> state + SCTransition -> transition + -- FIXME: is this force good? + SCComp -> pforce comp + SCTxInfo -> pforgetData txInfo + GetField @_ @y @_ @value valueDsl proxyLabel -> + getRecordField + (fieldNum @y proxyLabel) + (compileDsl valueDsl) + UnsafeOfSpine spine setters -> + punsafeCoerce + $ pconstrBuiltin + # pconstant (Prelude.toInteger $ Prelude.fromEnum spine) + #$ foldr pcons' pnil + $ map fieldValue setters + where + pcons' x y = pcons # x # y + fieldValue (_ ::= valueDsl) = compileDsl valueDsl + -- FIXME: Should we lift AsData functins? + LiftPlutarch @_ @py plutrachFunc valueDsl -> + let + x = pfromDataImpl $ punsafeCoerce $ compileDsl valueDsl + in + pdataImpl @py $ punsafeCoerce $ plutrachFunc # x + LiftPlutarch2 @_ @_ @py plutarchFunc vDsl1 vDsl2 -> + let + x = pfromDataImpl $ punsafeCoerce $ compileDsl vDsl1 + y = pfromDataImpl $ punsafeCoerce $ compileDsl vDsl2 + in + pdataImpl @py $ + punsafeCoerce $ + plutarchFunc x y + Eq xDsl yDsl -> case (xDsl, yDsl) of + (Anything, _) -> compileDsl $ Pure True + (_, Anything) -> compileDsl $ Pure True + (_, _) -> + pdataImpl $ (compileDsl xDsl) #== (compileDsl yDsl) + UnsafeUpdateOfSpine @_ @datatype notUpdatedValueDsl spine setters -> + pmatch + ( (pfstBuiltin #$ pasConstr # notUpdatedValue) + #== pconstant (Prelude.toInteger $ Prelude.fromEnum spine) + ) + $ \case + PTrue -> + if length setters == 0 + then notUpdatedValue + else + punsafeCoerce + $ pconstrBuiltin + # pconstant (Prelude.toInteger $ Prelude.fromEnum spine) + #$ foldr pcons' pnil + $ map perIxValue [0 .. (toInteger (spineFieldsNum spine) - 1)] + -- FIXME: use error code + PFalse -> ptraceInfoError "Spines not matching" + where + pcons' x y = pcons # x # y + notUpdatedValue = compileDsl notUpdatedValueDsl + notUpdatedFields = (psndBuiltin #$ pasConstr # notUpdatedValue) + updatedFields = + Map.fromList + [ ( toInteger $ fieldNum @datatype (Proxy @label) + , compileDsl valueDsl + ) + | (MkRecordLabel @label) ::= valueDsl <- setters + ] + perIxValue ix = case updatedFields Map.!? ix of + Just value -> value + Nothing -> ptryIndex (fromInteger ix) notUpdatedFields + Anything -> nonDetMessage dsl + nonDetMessage dsl = + error $ + "Non-deterministic code in place it should not be " + <> " while compiling on-chain: \n" + <> ppShow dsl + constrs = case Map.lookup transitionSpine spec of + Just x -> x + Nothing -> error "Compilation error: some spine lacks spec" diff --git a/src/Cardano/CEM/Stages.hs b/src/Cardano/CEM/Stages.hs deleted file mode 100644 index d9071bf..0000000 --- a/src/Cardano/CEM/Stages.hs +++ /dev/null @@ -1,41 +0,0 @@ -{-# LANGUAGE NoPolyKinds #-} - -module Cardano.CEM.Stages where - -import PlutusTx qualified -import Prelude qualified - -import PlutusLedgerApi.V2 ( - Interval (..), - POSIXTime (..), - always, - ) - --- Stages - --- This covers constraints on blockchain slot time, --- used by both on- and off-chain code -class Stages stage where - type StageParams stage = params | params -> stage - stageToOnChainInterval :: - StageParams stage -> stage -> Interval POSIXTime - --- Common - --- TODO: rename -data SingleStage = Always - deriving stock (Prelude.Show, Prelude.Eq) - -data SingleStageParams - = NoSingleStageParams - | AllowedInterval (Interval POSIXTime) - deriving stock (Prelude.Show, Prelude.Eq) - -instance Stages SingleStage where - type StageParams SingleStage = SingleStageParams - - stageToOnChainInterval NoSingleStageParams Always = always - stageToOnChainInterval (AllowedInterval interval) Always = interval - -PlutusTx.unstableMakeIsData ''SingleStage -PlutusTx.unstableMakeIsData 'NoSingleStageParams diff --git a/src/Cardano/CEM/TH.hs b/src/Cardano/CEM/TH.hs index efe23f1..1e78329 100644 --- a/src/Cardano/CEM/TH.hs +++ b/src/Cardano/CEM/TH.hs @@ -1,8 +1,8 @@ module Cardano.CEM.TH ( deriveCEMAssociatedTypes, + resolveFamily, compileCEM, unstableMakeIsDataSchema, - deriveStageAssociatedTypes, defaultIndex, unstableMakeHasSchemaInstance, ) where @@ -10,24 +10,28 @@ module Cardano.CEM.TH ( import Prelude import Data.Data (Proxy (..)) +import Data.Map qualified as Map +import Data.Tuple (swap) import GHC.Num.Natural (Natural) import Language.Haskell.TH import Language.Haskell.TH.Syntax (sequenceQ) import PlutusTx qualified import PlutusTx.Blueprint.TH +import PlutusTx.IsData (unsafeFromBuiltinData) +import PlutusTx.Show (deriveShow) import Language.Haskell.TH.Datatype ( ConstructorInfo (..), DatatypeInfo (..), reifyDatatype, ) +import Plutarch (Config (..), LogLevel (..), TracingMode (..), compile) -import Cardano.CEM (CEMScriptTypes (..)) -import Cardano.CEM.OnChain (CEMScriptCompiled (..), genericCEMScript) -import Cardano.CEM.Stages (Stages (..)) -import Data.Spine (deriveSpine) -import PlutusTx.Show (deriveShow) +import Cardano.CEM (CEMScript (..), CEMScriptTypes (..), CompilationConfig (..)) +import Cardano.CEM.DSL +import Cardano.CEM.OnChain (CEMScriptCompiled (..), genericPlutarchScript) +import Data.Spine (derivePlutusSpine) defaultIndex :: Name -> Q [(Name, Natural)] defaultIndex name = do @@ -53,46 +57,70 @@ resolveFamily familyName argName = do reifyInstances familyName [argType] return name -deriveStageAssociatedTypes :: Name -> Q [Dec] -deriveStageAssociatedTypes stageName = do - stageParamsName <- resolveFamily ''StageParams stageName - declss <- - sequenceQ - [ PlutusTx.unstableMakeIsData stageName - , PlutusTx.unstableMakeIsData stageParamsName - ] - return $ concat declss - deriveCEMAssociatedTypes :: Bool -> Name -> Q [Dec] -deriveCEMAssociatedTypes deriveBlueprint scriptName = do +deriveCEMAssociatedTypes _deriveBlueprint scriptName = do declss <- sequenceQ - [ -- Data - deriveFamily isDataDeriver ''Params - , deriveFamily isDataDeriver ''State - , deriveFamily isDataDeriver ''Transition - , -- Spines - deriveFamily deriveSpine ''State - , deriveFamily deriveSpine ''Transition + [ -- Data and Spines + deriveFamily derivePlutusSpine ''State + , deriveFamily derivePlutusSpine ''Transition + , deriveFamily derivePlutusSpine ''Params , -- Other deriveShow scriptName ] return $ concat declss where - isDataDeriver = - if deriveBlueprint - then unstableMakeIsDataSchema - else PlutusTx.unstableMakeIsData deriveFamily deriver family = do name <- resolveFamily family scriptName deriver name -compileCEM :: Name -> Q [Dec] -compileCEM name = do - stageName <- resolveFamily ''Stage name - let compiled = PlutusTx.compileUntyped $ genericCEMScript name stageName +compileCEM :: Bool -> Name -> Q [Dec] +compileCEM debugBuild name = do + -- FIXIT: two duplicating cases on `transitionComp` + let plutusScript = + [| + \a b c -> case transitionComp @($(conT name)) of + Just f -> + PlutusTx.toBuiltinData $ + f + (unsafeFromBuiltinData a) + (unsafeFromBuiltinData b) + (unsafeFromBuiltinData c) + Nothing -> PlutusTx.toBuiltinData () + |] + + compiledName <- newName $ "compiled_" <> nameBase name + [d| + $(varP compiledName) = case compiled of + Right x -> (errorCodes', x) + Left message -> + error $ "Plutarch compilation error: " <> show message + where + mPlutusScript = case transitionComp @($(conT name)) of + Just _ -> Just $(PlutusTx.compileUntyped plutusScript) + Nothing -> Nothing + spec' = + preProcessForOnChainCompilation $ + perTransitionScriptSpec @($(conT name)) + MkCompilationConfig prefix = compilationConfig @($(conT name)) + errorCodes' = parseErrorCodes prefix spec' + spec = + if debugBuild + then spec' + else substErrors (Map.fromList $ map swap errorCodes') spec' + script = + genericPlutarchScript + @($(conT name)) + spec + mPlutusScript + plutarchConfig = + if debugBuild + then Tracing LogDebug DoTracing + else Tracing LogInfo DoTracing + compiled = compile plutarchConfig script + instance CEMScriptCompiled $(conT name) where - {-# INLINEABLE cemScriptCompiled #-} - cemScriptCompiled Proxy = serialiseCompiledCode $(compiled) + errorCodes Proxy = fst $(varE compiledName) + cemScriptCompiled Proxy = snd $(varE compiledName) |] diff --git a/src/Cardano/CEM/Testing/StateMachine.hs b/src/Cardano/CEM/Testing/StateMachine.hs index 22265d8..7626875 100644 --- a/src/Cardano/CEM/Testing/StateMachine.hs +++ b/src/Cardano/CEM/Testing/StateMachine.hs @@ -9,7 +9,7 @@ import Prelude import Control.Monad (void) import Control.Monad.Except (ExceptT (..), runExceptT) -import Control.Monad.Trans (MonadIO (..)) +import Control.Monad.Trans (MonadIO (..), MonadTrans (..)) import Data.Bifunctor (Bifunctor (..)) import Data.Data (Typeable) import Data.List (permutations) @@ -17,9 +17,8 @@ import Data.Maybe (mapMaybe) import Data.Set qualified as Set import PlutusLedgerApi.V1 (PubKeyHash) -import PlutusTx.IsData (FromData (..)) -import Cardano.Api (PaymentKey, SigningKey, Value) +import Cardano.Api (PaymentKey, SigningKey, TxId, Value) import Clb (ClbT) import Test.QuickCheck @@ -38,9 +37,18 @@ import Test.QuickCheck.StateModel ( ) import Text.Show.Pretty (ppShow) -import Cardano.CEM (CEMParams (..)) -import Cardano.CEM hiding (scriptParams) -import Cardano.CEM.Monads (CEMAction (..), MonadSubmitTx (..), ResolvedTx (..), SomeCEMAction (..), TxSpec (..)) +import Cardano.CEM +import Cardano.CEM.DSL (getMainSigner) +import Cardano.CEM.Monads ( + BlockchainMonadEvent (..), + CEMAction (..), + MonadBlockchainParams (..), + MonadSubmitTx (..), + ResolvedTx (..), + SomeCEMAction (..), + TxResolutionError (..), + TxSpec (..), + ) import Cardano.CEM.Monads.CLB (ClbRunner, execOnIsolatedClb) import Cardano.CEM.OffChain import Cardano.CEM.OnChain (CEMScriptCompiled) @@ -48,15 +56,18 @@ import Cardano.Extras (signingKeyToPKH) import Data.Spine (HasSpine (..), deriveSpine) -- FIXME: add more mutations and documentation -data TxMutation = RemoveTxFan TxFanKind | ShuffleTxFan TxFanKind Int +data TxMutation + = RemoveConstraint {num :: Int} + | ShuffleConstraints + {shift :: Int} deriving stock (Eq, Show) deriveSpine ''TxMutation isNegativeMutation :: Maybe TxMutation -> Bool isNegativeMutation Nothing = False -isNegativeMutation (Just (RemoveTxFan _)) = True -isNegativeMutation (Just (ShuffleTxFan {})) = False +isNegativeMutation (Just (RemoveConstraint _)) = True +isNegativeMutation (Just (ShuffleConstraints {})) = False permute :: Int -> [a] -> [a] permute num arr = @@ -64,18 +75,14 @@ permute num arr = where pms = permutations arr -applyMutation :: Maybe TxMutation -> ResolvedTx -> ResolvedTx -applyMutation Nothing tx = tx -applyMutation (Just (RemoveTxFan In)) tx = tx {txIns = tail $ txIns tx} -applyMutation (Just (RemoveTxFan Out)) tx = tx {txOuts = tail $ txOuts tx} -applyMutation (Just (RemoveTxFan InRef)) tx = - tx {txInsReference = tail $ txInsReference tx} -applyMutation (Just (ShuffleTxFan In num)) tx = - tx {txIns = permute num $ txIns tx} -applyMutation (Just (ShuffleTxFan Out num)) tx = - tx {txOuts = permute num $ txOuts tx} -applyMutation (Just (ShuffleTxFan InRef num)) tx = - tx {txInsReference = permute num $ txInsReference tx} +applyMutation :: + Maybe TxMutation -> + [TxConstraint True script] -> + [TxConstraint True script] +applyMutation Nothing cs = cs +applyMutation (Just (RemoveConstraint num)) cs = + take num cs ++ tail (drop num cs) +applyMutation (Just (ShuffleConstraints shift)) cs = permute shift cs data TestConfig = MkTestConfig { actors :: [SigningKey PaymentKey] @@ -85,13 +92,10 @@ data TestConfig = MkTestConfig data ScriptStateParams a = MkScriptStateParams { config :: TestConfig - , cemParams :: CEMParams a + , params :: Params a } deriving stock (Generic) -params :: ScriptStateParams script -> Params script -params = scriptParams . cemParams - deriving stock instance (CEMScript a) => Eq (ScriptStateParams a) deriving stock instance (CEMScript a) => Show (ScriptStateParams a) @@ -119,14 +123,14 @@ class (CEMScriptCompiled script) => CEMScriptArbitrary script where - arbitraryCEMParams :: [SigningKey PaymentKey] -> Gen (CEMParams script) + arbitraryParams :: [SigningKey PaymentKey] -> Gen (Params script) arbitraryTransition :: ScriptStateParams script -> Maybe (State script) -> Gen (Transition script) instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where data Action (ScriptState script) output where SetupConfig :: TestConfig -> Action (ScriptState script) () - SetupCEMParams :: CEMParams script -> Action (ScriptState script) () + SetupParams :: Params script -> Action (ScriptState script) () ScriptTransition :: Transition script -> Maybe TxMutation -> @@ -139,44 +143,45 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where actionName (ScriptTransition transition _) = head . words . show $ transition actionName SetupConfig {} = "SetupConfig" - actionName SetupCEMParams {} = "SetupCEMParams" + actionName SetupParams {} = "SetupParams" arbitraryAction _varCtx modelState = case modelState of -- SetupConfig action should be called manually Void {} -> Gen.oneof [] ConfigSet config -> - Some . SetupCEMParams <$> arbitraryCEMParams (actors config) + Some . SetupParams <$> arbitraryParams (actors config) ScriptState {dappParams, state} -> do transition <- arbitraryTransition dappParams state Some <$> (ScriptTransition transition <$> genMutation transition) where - genTxKind = Gen.elements [In, Out] genMutation transition = - if not $ doMutationTesting $ config dappParams - then return Nothing - else case transitionSpec @script (params dappParams) state transition of - Left _ -> return Nothing - Right _spec -> - Gen.oneof - [ return Nothing - , Just . RemoveTxFan <$> genTxKind - , Just - <$> ( ShuffleTxFan - <$> genTxKind - <*> Gen.chooseInt (1, 10) - ) - ] + let cemAction = MkCEMAction (params dappParams) transition + in case compileActionConstraints state cemAction of + Right cs -> + Gen.oneof + [ return Nothing + , Just . RemoveConstraint + <$> Gen.chooseInt (0, length cs - 1) + , Just + <$> ( ShuffleConstraints + <$> Gen.chooseInt (1, length cs) + ) + ] + Left _ -> return Nothing precondition Void (SetupConfig {}) = True - precondition (ConfigSet {}) (SetupCEMParams {}) = True + precondition (ConfigSet {}) (SetupParams {}) = True precondition (ScriptState {dappParams, state, finished}) (ScriptTransition transition mutation) = - case transitionSpec @script (params dappParams) state transition of - Right _ -> - not finished && not (isNegativeMutation mutation) - Left _ -> False + let + cemAction = MkCEMAction (params dappParams) transition + compiled = compileActionConstraints state cemAction + in + case compiled of + Right _ -> not finished && not (isNegativeMutation mutation) + Left _ -> False -- Unreachable precondition _ _ = False @@ -187,9 +192,9 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where validFailingAction _ _ = False nextState Void (SetupConfig config) _var = ConfigSet config - nextState (ConfigSet config) (SetupCEMParams cemParams) _var = + nextState (ConfigSet config) (SetupParams params) _var = ScriptState - { dappParams = MkScriptStateParams {config, cemParams} + { dappParams = MkScriptStateParams {config, params} , state = Nothing , involvedActors = Set.empty , finished = False @@ -198,34 +203,34 @@ instance (CEMScriptArbitrary script) => StateModel (ScriptState script) where as@ScriptState {dappParams, state} (ScriptTransition transition _mutation) _var = - case transitionSpec (params dappParams) state transition of - Right spec -> - as - { state = nextCEMState spec - , involvedActors = - involvedActors as - <> Set.fromList (getAllSpecSigners spec) - , finished = nextCEMState spec == Nothing - } - Left _ -> error "Unreachable" + let + cemAction = MkCEMAction (params dappParams) transition + cs = case compileActionConstraints state cemAction of + Right x -> x + Left _ -> error "Unreachable: by preconditions" + in + as + { state = nextCEMState cs + , involvedActors = + involvedActors as + <> Set.fromList [getMainSigner cs] + , finished = nextCEMState cs == Nothing + } where - nextCEMState spec = case outStates spec of + nextCEMState cs = case mapMaybe f cs of + [x] -> Just x [] -> Nothing - [state'] -> Just state' _ -> error - "This StateModel instance support only with single-output scripts" - outStates spec = mapMaybe decodeOutState $ constraints spec - decodeOutState c = case rest (txFanCFilter c) of - UnsafeBySameCEM stateBS -> - fromBuiltinData @(State script) stateBS - _ -> Nothing + "Scripts with >1 SameScript outputs are not supported by QD" + f (TxFan Out (SameScript outState) _) = Just outState + f _ = Nothing nextState _ _ _ = error "Unreachable" instance (CEMScriptArbitrary script) => Show (Action (ScriptState script) a) where show (ScriptTransition t m) = "ScriptTransition " <> show t <> " mutated as " <> show m show (SetupConfig {}) = "SetupConfig" - show (SetupCEMParams {}) = "SetupCEMParams" + show (SetupParams {}) = "SetupParams" deriving stock instance (CEMScriptArbitrary script) => Eq (Action (ScriptState script) a) @@ -260,38 +265,38 @@ instance (Void, SetupConfig {}) -> do _ <- performHook modelState action return $ Right () - (ConfigSet {}, SetupCEMParams {}) -> do + (ConfigSet {}, SetupParams {}) -> do _ <- performHook modelState action return $ Right () ( ScriptState {dappParams, state} , ScriptTransition transition mutation ) -> do _ <- performHook modelState action - case transitionSpec (params dappParams) state transition of - Right spec -> do - r <- runExceptT $ do - resolved <- - ExceptT $ - first show - <$> ( resolveTx $ - MkTxSpec - { actions = - [ MkSomeCEMAction $ MkCEMAction (cemParams dappParams) transition - ] - , specSigner = - findSkForPKH (actors $ config dappParams) $ signerPKH spec - } - ) - ExceptT $ - first show - <$> submitResolvedTx (applyMutation mutation resolved) - return $ second (const ()) r - Left err -> return $ Left $ show err + bimap show (const ()) <$> mutatedResolveAndSubmit where - signerPKH spec = case getAllSpecSigners spec of - [singleSigner] -> singleSigner - _ -> error "Transition should have exactly one signer" - (_, _) -> error $ "Unreachable" + -- This should work like `resolveAndSubmit` + -- FIXME: DRY it and move Mutations to main implementation + mutatedResolveAndSubmit :: m (Either TxResolutionError TxId) + mutatedResolveAndSubmit = runExceptT $ do + let cemAction = MkCEMAction (params dappParams) transition + -- FIXME: refactor all ExceptT mess + cs' <- ExceptT $ return $ compileActionConstraints state cemAction + let + cs = applyMutation mutation cs' + signerPKH = getMainSigner cs + specSigner = + findSkForPKH (actors $ config dappParams) signerPKH + resolutions <- mapM (process cemAction) cs + let resolvedTx = (construct resolutions) {signer = specSigner} + result <- + first UnhandledSubmittingError + <$> lift (submitResolvedTx resolvedTx) + let spec = MkTxSpec [MkSomeCEMAction cemAction] specSigner + lift $ + logEvent $ + SubmittedTxSpec spec result + ExceptT $ return result + (_, _) -> error "Unreachable" monitoring (stateFrom, stateTo) action _ _ prop = do tabMutations $ tabStateFrom $ labelIfFinished prop diff --git a/test/Auction.hs b/test/Auction.hs index 194bf2c..3afb52d 100644 --- a/test/Auction.hs +++ b/test/Auction.hs @@ -3,36 +3,40 @@ module Auction where import Prelude import Control.Monad.Trans (MonadIO (..)) -import PlutusLedgerApi.V1.Value (assetClassValue) - -import Cardano.CEM +import Data.Proxy (Proxy (..)) +import GHC.IsList import Cardano.CEM.Examples.Auction import Cardano.CEM.Examples.Compilation () import Cardano.CEM.Monads import Cardano.CEM.OffChain +import Cardano.CEM.OnChain (CEMScriptCompiled (..)) import Cardano.Extras +import Plutarch.Script +import PlutusLedgerApi.V1.Value (assetClassValue) + import Test.Hspec (describe, it, shouldBe) import TestNFT (testNftAssetClass) import Utils (execClb, mintTestTokens, submitAndCheck) -auctionSpec = describe "Auction" $ do +auctionSpec = describe "AuctionSpec" $ do + it "Serialise" $ do + let script = cemScriptCompiled (Proxy :: Proxy SimpleAuction) + putStrLn $ + "Script bytes: " + <> show (length $ toList $ serialiseScript script) it "Wrong transition resolution error" $ execClb $ do seller <- (!! 0) <$> getTestWalletSks bidder1 <- (!! 1) <$> getTestWalletSks let auctionParams = - MkCEMParams - { scriptParams = - MkAuctionParams - { seller = signingKeyToPKH seller - , lot = - assetClassValue - testNftAssetClass - 1 - } - , stagesParams = NoControl + MkAuctionParams + { seller = signingKeyToPKH seller + , lot = + assetClassValue + testNftAssetClass + 1 } mintTestTokens seller 1 @@ -61,12 +65,11 @@ auctionSpec = describe "Auction" $ do ] , specSigner = bidder1 } - ~( Left - ( MkTransitionError - _ - (StateMachineError "\"Incorrect state for transition\"") - ) - ) <- + ~(Left _) <- + -- ( MkTransitionError + -- _ + -- (StateMachineError "\"Incorrect state for transition\"") + -- ) return result return () @@ -76,16 +79,12 @@ auctionSpec = describe "Auction" $ do bidder1 <- (!! 1) <$> getTestWalletSks let auctionParams = - MkCEMParams - { scriptParams = - MkAuctionParams - { seller = signingKeyToPKH seller - , lot = - assetClassValue - testNftAssetClass - 10 - } - , stagesParams = NoControl + MkAuctionParams + { seller = signingKeyToPKH seller + , lot = + assetClassValue + testNftAssetClass + 10 } mintTestTokens seller 10 @@ -124,11 +123,12 @@ auctionSpec = describe "Auction" $ do , specSigner = bidder1 } ~( Left - ( MkTransitionError - _ - (StateMachineError "\"Incorrect state for transition\"") - ) + _ ) <- + -- ( MkTransitionError + -- _ + -- (StateMachineError "\"Incorrect state for transition\"") + -- ) return result return () @@ -139,16 +139,12 @@ auctionSpec = describe "Auction" $ do let auctionParams = - MkCEMParams - { scriptParams = - MkAuctionParams - { seller = signingKeyToPKH seller - , lot = - assetClassValue - testNftAssetClass - 10 - } - , stagesParams = NoControl + MkAuctionParams + { seller = signingKeyToPKH seller + , lot = + assetClassValue + testNftAssetClass + 10 } mintTestTokens seller 10 diff --git a/test/Dynamic.hs b/test/Dynamic.hs index dc2da8c..bcb3281 100644 --- a/test/Dynamic.hs +++ b/test/Dynamic.hs @@ -12,7 +12,6 @@ import Test.Hspec (describe, it, shouldBe) import Test.QuickCheck import Test.QuickCheck.DynamicLogic -import Cardano.CEM (CEMParams (..)) import Cardano.CEM.Examples.Auction import Cardano.CEM.Examples.Compilation () import Cardano.CEM.Monads (MonadTest (..)) @@ -25,16 +24,13 @@ import Utils (execClb, mintTestTokens) -- Defining generic instances instance CEMScriptArbitrary SimpleAuction where - arbitraryCEMParams actors = do + arbitraryParams actors = do seller <- elements actors return $ - MkCEMParams - ( MkAuctionParams - { seller = signingKeyToPKH seller - , lot = assetClassValue testNftAssetClass 1 - } - ) - NoControl + MkAuctionParams + { seller = signingKeyToPKH seller + , lot = assetClassValue testNftAssetClass 1 + } arbitraryTransition dappParams state = case state of Nothing -> return Create @@ -55,8 +51,8 @@ instance CEMScriptArbitrary SimpleAuction where instance CEMScriptRunModel SimpleAuction where performHook (ConfigSet (MkTestConfig {actors})) - (SetupCEMParams cemParams) = do - let s = seller $ scriptParams cemParams + (SetupParams cemParams) = do + let s = seller cemParams mintTestTokens (findSkForPKH actors s) 1 return () performHook _ _ = return () diff --git a/test/Main.hs b/test/Main.hs index ddbae9a..de77212 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -11,7 +11,7 @@ import Voting (votingSpec) main :: IO () main = hspec $ do - dynamicSpec offChainSpec auctionSpec votingSpec + dynamicSpec diff --git a/test/OffChain.hs b/test/OffChain.hs index 7bc147e..b6e7d72 100644 --- a/test/OffChain.hs +++ b/test/OffChain.hs @@ -57,7 +57,7 @@ offChainSpec = describe "Checking monad works" $ do tx = MkResolvedTx { txIns = map withKeyWitness user1TxIns - , txInsReference = [] + , txInRefs = [] , txOuts = [ out user1Address , out user2Address diff --git a/test/Utils.hs b/test/Utils.hs index eb4ca8f..68477e9 100644 --- a/test/Utils.hs +++ b/test/Utils.hs @@ -73,7 +73,7 @@ mintTestTokens userSk numMint = do tx = MkResolvedTx { txIns = map withKeyWitness user1TxIns - , txInsReference = [] + , txInRefs = [] , txOuts = [out] , toMint = mintedTokens @@ -90,7 +90,7 @@ mintTestTokens userSk numMint = do checkTxCreated :: (MonadQueryUtxo m, MonadIO m) => TxId -> m () checkTxCreated txId = do - -- TODO: better out checks + -- FIXME: better checks for tests awaitTx txId let txIn = TxIn txId (TxIx 0) @@ -104,7 +104,6 @@ awaitEitherTx eitherTx = case eitherTx of Right txId -> do awaitTx txId - -- liftIO $ putStrLn $ "Awaited " <> show txId Left errorMsg -> error $ "Failed to send tx: " <> ppShow errorMsg submitAndCheck :: (MonadSubmitTx m, MonadIO m) => TxSpec -> m () diff --git a/test/Voting.hs b/test/Voting.hs index b0d3e35..af256b9 100644 --- a/test/Voting.hs +++ b/test/Voting.hs @@ -3,28 +3,35 @@ module Voting (votingSpec) where import Prelude hiding (readFile) import Control.Monad.IO.Class (MonadIO (..)) +import Data.Proxy -import Test.Hspec (describe, shouldBe) +import GHC.IsList +import Text.Show.Pretty (ppShow) + +import Plutarch.Script + +import Test.Hspec (describe, it, shouldBe) -import Cardano.CEM import Cardano.CEM.Examples.Compilation () import Cardano.CEM.Examples.Voting import Cardano.CEM.Monads import Cardano.CEM.OffChain -import Cardano.CEM.Stages +import Cardano.CEM.OnChain import Cardano.Extras (signingKeyToPKH) import Utils votingSpec = describe "Voting" $ do - let ignoreTest (_name :: String) = const (return ()) - - -- FIXME: fix Voting budget - ignoreTest "Successfull flow" $ + it "Serialise" $ do + let !script = cemScriptCompiled (Proxy :: Proxy SimpleVoting) + putStrLn $ + "Script bytes: " + <> show (length $ toList $ serialiseScript script) + it "Successful flow" $ execClb $ do jury1 : jury2 : creator : _ <- getTestWalletSks let - params' = + params = MkVotingParams { disputeDescription = "Test dispute" , creator = signingKeyToPKH creator @@ -33,7 +40,6 @@ votingSpec = describe "Voting" $ do , abstainAllowed = True , drawDecision = Abstain } - params = MkCEMParams params' NoSingleStageParams mkAction = MkSomeCEMAction . MkCEMAction params -- Start submitAndCheck $ @@ -56,6 +62,9 @@ votingSpec = describe "Voting" $ do , specSigner = jury1 } + stats <- perTransitionStats + liftIO $ putStrLn $ ppShow stats + submitAndCheck $ MkTxSpec { actions = [mkAction $ Vote (signingKeyToPKH jury2) No] @@ -67,8 +76,8 @@ votingSpec = describe "Voting" $ do submitAndCheck $ MkTxSpec { actions = [mkAction Finalize] - , specSigner = jury2 + , specSigner = creator } Just state <- queryScriptState params - liftIO $ state `shouldBe` (Finalized Abstain) + liftIO $ state `shouldBe` Finalized Abstain