{-# LANGUAGE AllowAmbiguousTypes        #-}
{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DerivingVia                #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImportQualifiedPost        #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE NumericUnderscores         #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE QuantifiedConstraints      #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE ViewPatterns               #-}
{-# OPTIONS_GHC -Wno-redundant-constraints -fno-warn-name-shadowing -Wno-orphans #-}


module Plutus.Contract.Test.ContractModel.Interface
    ( -- * Contract models
      --
      -- $contractModel
      ContractModel(..)
    , Actions
    , SomeContractInstanceKey(..)
    , QCCM.HasSymbolics(..)
      -- ** Model state
    , QCCM.ModelState
    , QCCM.contractState
    , currentSlot
    , QCCM.balanceChanges
    , balanceChange
    , QCCM.minted
    , QCCM.lockedValue
    , QCCM.symIsZero
    , QCCM.GetModelState
    , QCCM.viewModelState
    , viewContractState
    , QCCM.SymToken
    , QCCM.SymValueLike(..)
    , QCCM.TokenLike(..)
    , invSymValue
    , QCCM.toValue

    -- ** The Spec monad
    --
    -- $specMonad
    , QCCM.Spec(..)
    , wait
    , waitUntil
    , QCCM.mint
    , QCCM.burn
    , deposit
    , withdraw
    , transfer
    , QCCM.createToken
    , QCCM.createTxOut
    , QCCM.createTxIn
    , QCCM.createSymbolic
    , QCCM.assertSpec
    , SpecificationEmulatorTrace
    , registerToken
    , registerTxOut
    , registerTxIn
    , registerSymbolic
    , delay
    , fromSlotNo
    , toSlotNo

    -- * Test scenarios
    --
    -- $dynamicLogic
    , DL
    , action
    , waitUntilDL
    , QCCM.observe
    , QCCM.anyAction
    , QCCM.anyActions
    , QCCM.anyActions_
    , QCD.forAllQ
    , QCD.elementsQ
    , QCD.chooseQ

    -- ** Failures
    --
    -- $dynamicLogic_errors
    , QCD.assert
    , assertModel
    , QCCM.stopping
    , QCCM.weight
    , QCCM.getSize
    , QCCM.monitor

    -- * Properties
    -- ** Wallet contract handles
    --
    -- $walletHandles
    , CMI.SchemaConstraints
    , StartContract(..)
    , HandleFun
    -- ** Model properties
    , propSanityCheckModel
    , propSanityCheckAssertions
    , propSanityCheckReactive
    -- ** Coverage checking options
    , module Coverage
    , CMI.CoverageOptions
    , CMI.defaultCoverageOptions
    , CMI.endpointCoverageReq
    , CMI.checkCoverage
    , CMI.coverageIndex
    , CMI.quickCheckWithCoverage
    , CMI.quickCheckWithCoverageAndResult
    -- ** Emulator properties
    , propRunActions_
    , propRunActions
    , propRunActionsWithOptions
    , CMI.defaultCheckOptionsContractModel
    , CMI.checkThreatModel
    , CMI.checkThreatModelWithOptions
    -- ** DL properties
    , QCCM.forAllDL

    -- ** Standard properties
    --
    -- $noLockedFunds
    , NoLockedFundsProof
    , pattern CMI.NoLockedFundsProof
    , CMI.nlfpMainStrategy
    , CMI.nlfpWalletStrategy
    , CMI.nlfpOverhead
    , CMI.nlfpErrorMargin
    , CMI.defaultNLFP
    , CMI.checkNoLockedFundsProof
    , CMI.checkNoLockedFundsProofFast
    , NoLockedFundsProofLight
    , pattern CMI.NoLockedFundsProofLight
    , CMI.nlfplMainStrategy
    , CMI.checkNoLockedFundsProofLight
    , CMI.checkNoLockedFundsProofWithOptions
    , CMI.checkNoLockedFundsProofFastWithOptions
    -- $checkNoPartiality
    , CMI.Whitelist
    , CMI.whitelistOk
    , CMI.mkWhitelist
    , CMI.errorPrefixes
    , CMI.defaultWhitelist
    , checkErrorWhitelist
    , checkErrorWhitelistWithOptions
    -- To make GHC understand coercibility
    , CMI.WithInstances(..)
    , WrappedState(..)
    , checkDoubleSatisfaction
    , checkDoubleSatisfactionWithOptions
    , Generic

    -- ** Utils
    , fromAssetId
    , toAssetId
    ) where

import Control.Monad.Freer.Reader (ask)
import Control.Monad.Freer.Writer (Writer, runWriter, tell)
import Data.Row (Row)
import Plutus.Trace.Effects.RunContract (walletInstanceTag)
import Plutus.Trace.Emulator.Types (ContractHandle (..), ContractInstanceTag)
import PlutusTx.AssocMap qualified as AssocMap

import Control.Lens
import Control.Monad.Cont
import Control.Monad.Freer (Eff, raise)
import Data.Coerce
import Data.Data
import GHC.Generics hiding (to)

import Cardano.Api qualified as CardanoAPI
import Ledger.Slot
import Plutus.Contract (Contract)
import Plutus.Contract.Test hiding (not)
import Plutus.Script.Utils.Ada qualified as Ada
import Plutus.Script.Utils.Value
import Plutus.Trace.Emulator as Trace (BaseEmulatorEffects, waitNSlots)
import PlutusTx.Builtins qualified as Builtins


import Test.QuickCheck hiding (ShrinkState, checkCoverage, getSize, (.&&.), (.||.))
import Test.QuickCheck qualified as QC

import Plutus.Contract.Test.ContractModel.Internal qualified as CMI
import Plutus.Contract.Test.Coverage as Coverage
import Test.QuickCheck.ContractModel qualified as QCCM
import Test.QuickCheck.ContractModel.ThreatModel.DoubleSatisfaction qualified as QCCM
import Test.QuickCheck.DynamicLogic qualified as QCD
import Test.QuickCheck.StateModel qualified as QCSM

-- | A function returning the `ContractHandle` corresponding to a `ContractInstanceKey`. A
--   `HandleFun` is provided to the `perform` function to enable calling contract endpoints with
--   `Plutus.Trace.Emulator.callEndpoint`.
type HandleFun state = forall w schema err params. (Typeable w, Typeable schema, Typeable err, Typeable params)
                        => ContractInstanceKey state w schema err params -> ContractHandle w schema err

data StartContract state where
  StartContract :: (CMI.SchemaConstraints w s e, Typeable p) => ContractInstanceKey state w s e p -> p -> StartContract state

type SpecificationEmulatorTrace = Eff (Writer [(String, SomethingWithSymbolicRep)] ': BaseEmulatorEffects)

data SomethingWithSymbolicRep where
  WithSymbolicRep :: QCCM.HasSymbolicRep t => t -> SomethingWithSymbolicRep

-- | A `ContractModel` instance captures everything that is needed to generate and run tests of a
--   contract or set of contracts. It specifies among other things
--
--  * what operations are supported by the contract (`Action`),
--  * when they are valid (`precondition`),
--  * how to generate random actions (`arbitraryAction`),
--  * how the operations affect the state (`nextState`), and
--  * how to run the operations in the emulator (`perform`)

class ( Typeable state
      , Show state
      , Show (Action state)
      , Eq (Action state)
      , QCCM.HasSymbolics (Action state)
      , QCSM.HasVariables (Action state)
      , QCSM.HasVariables state
      , Generic state
      , (forall w s e p. Eq (ContractInstanceKey state w s e p))
      , (forall w s e p. Show (ContractInstanceKey state w s e p))
      ) => ContractModel state where

    -- | The type of actions that are supported by the contract. An action usually represents a single
    --   `Plutus.Trace.Emulator.callEndpoint` or a transfer of tokens, but it can be anything
    --   that can be interpreted in the `EmulatorTrace` monad.
    data Action state

    -- | To be able to call a contract endpoint from a wallet a `ContractHandle` is required. These
    --   are managed by the test framework and all the user needs to do is provide this contract
    --   instance key type representing the different contract instances that a test needs to work
    --   with, and when creating a property (see `propRunActions_`) provide a list of contract
    --   instance keys together with their wallets and contracts (a `ContractInstanceSpec`).
    --   Contract instance keys are indexed by the observable state, schema, and error type of the
    --   contract and should be defined as a GADT. For example, a handle type for a contract with
    --   one seller and multiple buyers could look like this.
    --
    --   >  data ContractInstanceKey MyModel w s e where
    --   >      Buyer  :: Wallet -> ContractInstanceKey MyModel MyObsState MySchema MyError MyParams
    --   >      Seller :: ContractInstanceKey MyModel MyObsState MySchema MyError MyParams
    data ContractInstanceKey state :: * -> Row * -> * -> * -> *

    -- | Get the wallet that the contract running at a specific `ContractInstanceKey` should run
    -- in
    instanceWallet :: ContractInstanceKey state w s e p -> Wallet

    -- | The 'ContractInstanceTag' of an instance key for a wallet. Defaults to 'walletInstanceTag'.
    --   You must override this if you have multiple instances per wallet.
    instanceTag :: forall w s e p. CMI.SchemaConstraints w s e => ContractInstanceKey state w s e p -> ContractInstanceTag
    instanceTag = Wallet -> ContractInstanceTag
walletInstanceTag (Wallet -> ContractInstanceTag)
-> (ContractInstanceKey state w s e p -> Wallet)
-> ContractInstanceKey state w s e p
-> ContractInstanceTag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractInstanceKey state w s e p -> Wallet
forall state w (s :: Row *) e p.
ContractModel state =>
ContractInstanceKey state w s e p -> Wallet
instanceWallet

    -- | Given the current model state, provide a QuickCheck generator for a random next action.
    --   This is used in the `Arbitrary` instance for `Actions`s as well as by `anyAction` and
    --   `anyActions`.
    arbitraryAction :: QCCM.ModelState state -> Gen (Action state)

    -- | The name of an Action, used to report statistics.
    actionName :: Action state -> String
    actionName = [String] -> String
forall a. [a] -> a
head ([String] -> String)
-> (Action state -> [String]) -> Action state -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words (String -> [String])
-> (Action state -> String) -> Action state -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action state -> String
forall a. Show a => a -> String
show

    -- | The probability that we will generate a `WaitUntil` in a given state
    waitProbability :: QCCM.ModelState state -> Double
    waitProbability ModelState state
_ = Double
0.1

    -- | Control the distribution of how long `WaitUntil` waits
    arbitraryWaitInterval :: QCCM.ModelState state -> Gen Slot
    arbitraryWaitInterval ModelState state
s = Integer -> Slot
Slot (Integer -> Slot) -> Gen Integer -> Gen Slot
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
1,Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
10 ([Integer] -> Integer
forall a. [a] -> a
head [ Integer
5Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
*(Integer
kInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) | Integer
k <- [Integer
0..], Word64
2Word64 -> Integer -> Word64
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
k Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
n]))
      where
        CardanoAPI.SlotNo Word64
n = ModelState state
s ModelState state
-> Getting SlotNo (ModelState state) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (ModelState state) SlotNo
forall state. Getter (ModelState state) SlotNo
QCCM.currentSlot

    -- | The initial state, before any actions have been performed.
    initialState :: state

    -- | The initial handles
    initialInstances :: [StartContract state]
    initialInstances = []

    -- | The `precondition` function decides if a given action is valid in a given state. Typically
    --   actions generated by `arbitraryAction` will satisfy the precondition, but if they don't
    --   they will be discarded and another action will be generated. More importantly, the
    --   preconditions are used when shrinking (see `shrinkAction`) to ensure that shrunk test cases
    --   still make sense.
    --
    --   If an explicit `action` in a `DL` scenario violates the precondition an error is raised.
    precondition :: QCCM.ModelState state -> Action state -> Bool
    precondition ModelState state
_ Action state
_ = Bool
True

    -- | `nextReactiveState` is run every time the model `wait`s for a slot to be reached. This
    --   can be used to model reactive components of off-chain code.
    nextReactiveState :: Slot -> QCCM.Spec state ()
    nextReactiveState Slot
_ = () -> Spec state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    -- | This is where the model logic is defined. Given an action, `nextState` specifies the
    --   effects running that action has on the model state. It runs in the `QCCM.Spec` monad, which is a
    --   state monad over the `QCCM.ModelState`.
    nextState :: Action state -> QCCM.Spec state ()

    -- | Start new contract instances
    startInstances :: QCCM.ModelState state
                   -> Action state
                   -> [StartContract state]
    startInstances ModelState state
_ Action state
_ = []

    -- | Map a `ContractInstanceKey` `k` to the `Contract` that is started when we start
    -- `k` in a given `QCCM.ModelState` with a given semantics of `SymToken`s
    instanceContract :: (forall t. QCCM.HasSymbolicRep t => QCCM.Symbolic t -> t)
                     -> ContractInstanceKey state w s e p
                     -> p
                     -> Contract w s e ()

    -- | While `nextState` models the behaviour of the actions, `perform` contains the code for
    --   running the actions in the emulator (see "Plutus.Trace.Emulator"). It gets access to the
    --   wallet contract handles, the current model state, and the action to be performed.
    perform :: HandleFun state  -- ^ Function from `ContractInstanceKey` to `ContractHandle`
            -> (forall t. QCCM.HasSymbolicRep t => QCCM.Symbolic t -> t)
                -- ^ Map from symbolic things (that may appear in actions or the state)
                -- to actual things that appear at runtime
            -> QCCM.ModelState state -- ^ The model state before peforming the action
            -> Action state     -- ^ The action to perform
            -> SpecificationEmulatorTrace ()

    -- | When a test involving random sequences of actions fails, the framework tries to find a
    --   minimal failing test case by shrinking the original failure. Action sequences are shrunk by
    --   removing individual actions, or by replacing an action by one of the (simpler) actions
    --   returned by `shrinkAction`.
    --
    --   See `Test.QuickCheck.shrink` for more information on shrinking.
    shrinkAction :: QCCM.ModelState state -> Action state -> [Action state]
    shrinkAction ModelState state
_ Action state
_ = []

    -- | The `monitoring` function allows you to collect statistics of your testing using QuickCheck
    --   functions like `Test.QuickCheck.label`, `Test.QuickCheck.collect`,
    --   `Test.QuickCheck.classify`, and `Test.QuickCheck.tabulate`. This function is called by
    --   `propRunActions` (and friends) for any actions in the given `Actions`.
    --
    --   Statistics on which actions are executed are always collected.
    monitoring :: (QCCM.ModelState state, QCCM.ModelState state)  -- ^ Model state before and after the action
               -> Action state                          -- ^ The action that was performed
               -> Property -> Property
    monitoring (ModelState state, ModelState state)
_ Action state
_ = Property -> Property
forall a. a -> a
id

    -- | In some scenarios it's useful to have actions that are never generated randomly, but only
    --   used explicitly in `DL` scenario `action`s. To avoid these actions matching an `anyAction`
    --   when shrinking, they can be marked `restricted`.
    restricted :: Action state -> Bool
    restricted Action state
_ = Bool
False

newtype WrappedState state = WrapState { WrappedState state -> state
unwrapState :: state }
  deriving (Eq (WrappedState state)
Eq (WrappedState state)
-> (WrappedState state -> WrappedState state -> Ordering)
-> (WrappedState state -> WrappedState state -> Bool)
-> (WrappedState state -> WrappedState state -> Bool)
-> (WrappedState state -> WrappedState state -> Bool)
-> (WrappedState state -> WrappedState state -> Bool)
-> (WrappedState state -> WrappedState state -> WrappedState state)
-> (WrappedState state -> WrappedState state -> WrappedState state)
-> Ord (WrappedState state)
WrappedState state -> WrappedState state -> Bool
WrappedState state -> WrappedState state -> Ordering
WrappedState state -> WrappedState state -> WrappedState state
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall state. Ord state => Eq (WrappedState state)
forall state.
Ord state =>
WrappedState state -> WrappedState state -> Bool
forall state.
Ord state =>
WrappedState state -> WrappedState state -> Ordering
forall state.
Ord state =>
WrappedState state -> WrappedState state -> WrappedState state
min :: WrappedState state -> WrappedState state -> WrappedState state
$cmin :: forall state.
Ord state =>
WrappedState state -> WrappedState state -> WrappedState state
max :: WrappedState state -> WrappedState state -> WrappedState state
$cmax :: forall state.
Ord state =>
WrappedState state -> WrappedState state -> WrappedState state
>= :: WrappedState state -> WrappedState state -> Bool
$c>= :: forall state.
Ord state =>
WrappedState state -> WrappedState state -> Bool
> :: WrappedState state -> WrappedState state -> Bool
$c> :: forall state.
Ord state =>
WrappedState state -> WrappedState state -> Bool
<= :: WrappedState state -> WrappedState state -> Bool
$c<= :: forall state.
Ord state =>
WrappedState state -> WrappedState state -> Bool
< :: WrappedState state -> WrappedState state -> Bool
$c< :: forall state.
Ord state =>
WrappedState state -> WrappedState state -> Bool
compare :: WrappedState state -> WrappedState state -> Ordering
$ccompare :: forall state.
Ord state =>
WrappedState state -> WrappedState state -> Ordering
$cp1Ord :: forall state. Ord state => Eq (WrappedState state)
Ord, WrappedState state -> WrappedState state -> Bool
(WrappedState state -> WrappedState state -> Bool)
-> (WrappedState state -> WrappedState state -> Bool)
-> Eq (WrappedState state)
forall state.
Eq state =>
WrappedState state -> WrappedState state -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WrappedState state -> WrappedState state -> Bool
$c/= :: forall state.
Eq state =>
WrappedState state -> WrappedState state -> Bool
== :: WrappedState state -> WrappedState state -> Bool
$c== :: forall state.
Eq state =>
WrappedState state -> WrappedState state -> Bool
Eq, (forall x. WrappedState state -> Rep (WrappedState state) x)
-> (forall x. Rep (WrappedState state) x -> WrappedState state)
-> Generic (WrappedState state)
forall x. Rep (WrappedState state) x -> WrappedState state
forall x. WrappedState state -> Rep (WrappedState state) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall state x. Rep (WrappedState state) x -> WrappedState state
forall state x. WrappedState state -> Rep (WrappedState state) x
$cto :: forall state x. Rep (WrappedState state) x -> WrappedState state
$cfrom :: forall state x. WrappedState state -> Rep (WrappedState state) x
Generic)
  deriving newtype (Int -> WrappedState state -> ShowS
[WrappedState state] -> ShowS
WrappedState state -> String
(Int -> WrappedState state -> ShowS)
-> (WrappedState state -> String)
-> ([WrappedState state] -> ShowS)
-> Show (WrappedState state)
forall state. Show state => Int -> WrappedState state -> ShowS
forall state. Show state => [WrappedState state] -> ShowS
forall state. Show state => WrappedState state -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WrappedState state] -> ShowS
$cshowList :: forall state. Show state => [WrappedState state] -> ShowS
show :: WrappedState state -> String
$cshow :: forall state. Show state => WrappedState state -> String
showsPrec :: Int -> WrappedState state -> ShowS
$cshowsPrec :: forall state. Show state => Int -> WrappedState state -> ShowS
Show)

deriving instance Eq (ContractInstanceKey state w s e p) => Eq (CMI.ContractInstanceKey (WrappedState state) w s e p)
deriving newtype instance Show (ContractInstanceKey state w s e p) => Show (CMI.ContractInstanceKey (WrappedState state) w s e p)

-- TODO: This instance and the duplicated StartContract above is one of many good indications that going
-- via this indirection is fugly and smelly. Instead of running in `WithInstances (WrappedState state)` we
-- should perhaps ditch this particular indirection and just run in `WithInstances state`. Now, you
-- can't just naively implement that - you would need to remove the `ContractInstanceModel` class and
-- move all the derived machinery from internal to here to make it work. Painful but doable...
instance ContractModel state => CMI.ContractInstanceModel (WrappedState state) where
  newtype ContractInstanceKey (WrappedState state) w s e p =
            WrapContractInstanceKey { ContractInstanceKey (WrappedState state) w s e p
-> ContractInstanceKey state w s e p
unwrapContractInstanceKey :: ContractInstanceKey state w s e p }
  instanceWallet :: ContractInstanceKey (WrappedState state) w s e p -> Wallet
instanceWallet = ContractInstanceKey state w s e p -> Wallet
forall state w (s :: Row *) e p.
ContractModel state =>
ContractInstanceKey state w s e p -> Wallet
instanceWallet (ContractInstanceKey state w s e p -> Wallet)
-> (ContractInstanceKey (WrappedState state) w s e p
    -> ContractInstanceKey state w s e p)
-> ContractInstanceKey (WrappedState state) w s e p
-> Wallet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractInstanceKey (WrappedState state) w s e p
-> ContractInstanceKey state w s e p
forall state w (s :: Row *) e p.
ContractInstanceKey (WrappedState state) w s e p
-> ContractInstanceKey state w s e p
unwrapContractInstanceKey
  instanceTag :: ContractInstanceKey (WrappedState state) w s e p
-> ContractInstanceTag
instanceTag = ContractInstanceKey state w s e p -> ContractInstanceTag
forall state w (s :: Row *) e p.
(ContractModel state, SchemaConstraints w s e) =>
ContractInstanceKey state w s e p -> ContractInstanceTag
instanceTag (ContractInstanceKey state w s e p -> ContractInstanceTag)
-> (ContractInstanceKey (WrappedState state) w s e p
    -> ContractInstanceKey state w s e p)
-> ContractInstanceKey (WrappedState state) w s e p
-> ContractInstanceTag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractInstanceKey (WrappedState state) w s e p
-> ContractInstanceKey state w s e p
forall state w (s :: Row *) e p.
ContractInstanceKey (WrappedState state) w s e p
-> ContractInstanceKey state w s e p
unwrapContractInstanceKey
  initialInstances :: [StartContract (WrappedState state)]
initialInstances = (StartContract state -> StartContract (WrappedState state))
-> [StartContract state] -> [StartContract (WrappedState state)]
forall a b. (a -> b) -> [a] -> [b]
map StartContract state -> StartContract (WrappedState state)
forall state.
StartContract state -> StartContract (WrappedState state)
wrapStartContract ([StartContract state] -> [StartContract (WrappedState state)])
-> [StartContract state] -> [StartContract (WrappedState state)]
forall a b. (a -> b) -> a -> b
$ ContractModel state => [StartContract state]
forall state. ContractModel state => [StartContract state]
initialInstances @state
  startInstances :: ModelState (WrappedState state)
-> Action (WrappedState state)
-> [StartContract (WrappedState state)]
startInstances ModelState (WrappedState state)
m Action (WrappedState state)
a = (StartContract state -> StartContract (WrappedState state))
-> [StartContract state] -> [StartContract (WrappedState state)]
forall a b. (a -> b) -> [a] -> [b]
map StartContract state -> StartContract (WrappedState state)
forall state.
StartContract state -> StartContract (WrappedState state)
wrapStartContract ([StartContract state] -> [StartContract (WrappedState state)])
-> [StartContract state] -> [StartContract (WrappedState state)]
forall a b. (a -> b) -> a -> b
$ ModelState state -> Action state -> [StartContract state]
forall state.
ContractModel state =>
ModelState state -> Action state -> [StartContract state]
startInstances ((WrappedState state -> state)
-> ModelState (WrappedState state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WrappedState state -> state
forall state. WrappedState state -> state
unwrapState ModelState (WrappedState state)
m) (Action (WrappedState state) -> Action state
forall state. Action (WrappedState state) -> Action state
unwrapAction Action (WrappedState state)
a)
  instanceContract :: (forall t. HasSymbolicRep t => Symbolic t -> t)
-> ContractInstanceKey (WrappedState state) w s e p
-> p
-> Contract w s e ()
instanceContract forall t. HasSymbolicRep t => Symbolic t -> t
e ContractInstanceKey (WrappedState state) w s e p
k p
p = (forall t. HasSymbolicRep t => Symbolic t -> t)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
forall state w (s :: Row *) e p.
ContractModel state =>
(forall t. HasSymbolicRep t => Symbolic t -> t)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
instanceContract forall t. HasSymbolicRep t => Symbolic t -> t
e (ContractInstanceKey (WrappedState state) w s e p
-> ContractInstanceKey state w s e p
forall state w (s :: Row *) e p.
ContractInstanceKey (WrappedState state) w s e p
-> ContractInstanceKey state w s e p
unwrapContractInstanceKey ContractInstanceKey (WrappedState state) w s e p
k) p
p

wrapStartContract :: StartContract state -> CMI.StartContract (WrappedState state)
wrapStartContract :: StartContract state -> StartContract (WrappedState state)
wrapStartContract (StartContract ContractInstanceKey state w s e p
k p
p) = ContractInstanceKey (WrappedState state) w s e p
-> p -> StartContract (WrappedState state)
forall w (s :: Row *) e p state.
(SchemaConstraints w s e, Typeable p) =>
ContractInstanceKey state w s e p -> p -> StartContract state
CMI.StartContract (ContractInstanceKey state w s e p
-> ContractInstanceKey (WrappedState state) w s e p
forall state w (s :: Row *) e p.
ContractInstanceKey state w s e p
-> ContractInstanceKey (WrappedState state) w s e p
WrapContractInstanceKey ContractInstanceKey state w s e p
k) p
p

deriving instance Eq (Action state) => Eq (QCCM.Action (WrappedState state))
deriving newtype instance Show (Action state) => Show (QCCM.Action (WrappedState state))
deriving instance Generic (QCCM.Action (WrappedState state))

instance ContractModel state => QCCM.ContractModel (WrappedState state) where
  newtype Action (WrappedState state) = WrapAction{ Action (WrappedState state) -> Action state
unwrapAction :: Action state }
  arbitraryAction :: ModelState (WrappedState state)
-> Gen (Action (WrappedState state))
arbitraryAction = (Action state -> Action (WrappedState state))
-> Gen (Action state) -> Gen (Action (WrappedState state))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Action state -> Action (WrappedState state)
forall state. Action state -> Action (WrappedState state)
WrapAction (Gen (Action state) -> Gen (Action (WrappedState state)))
-> (ModelState (WrappedState state) -> Gen (Action state))
-> ModelState (WrappedState state)
-> Gen (Action (WrappedState state))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelState state -> Gen (Action state)
forall state.
ContractModel state =>
ModelState state -> Gen (Action state)
arbitraryAction (ModelState state -> Gen (Action state))
-> (ModelState (WrappedState state) -> ModelState state)
-> ModelState (WrappedState state)
-> Gen (Action state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WrappedState state -> state)
-> ModelState (WrappedState state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WrappedState state -> state
forall state. WrappedState state -> state
unwrapState
  actionName :: Action (WrappedState state) -> String
actionName = Action state -> String
forall state. ContractModel state => Action state -> String
actionName (Action state -> String)
-> (Action (WrappedState state) -> Action state)
-> Action (WrappedState state)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action (WrappedState state) -> Action state
forall state. Action (WrappedState state) -> Action state
unwrapAction
  waitProbability :: ModelState (WrappedState state) -> Double
waitProbability = ModelState state -> Double
forall state. ContractModel state => ModelState state -> Double
waitProbability (ModelState state -> Double)
-> (ModelState (WrappedState state) -> ModelState state)
-> ModelState (WrappedState state)
-> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WrappedState state -> state)
-> ModelState (WrappedState state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WrappedState state -> state
forall state. WrappedState state -> state
unwrapState
  arbitraryWaitInterval :: ModelState (WrappedState state) -> Gen SlotNo
arbitraryWaitInterval = (Slot -> SlotNo) -> Gen Slot -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Slot -> SlotNo
toSlotNo (Gen Slot -> Gen SlotNo)
-> (ModelState (WrappedState state) -> Gen Slot)
-> ModelState (WrappedState state)
-> Gen SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModelState state -> Gen Slot
forall state. ContractModel state => ModelState state -> Gen Slot
arbitraryWaitInterval (ModelState state -> Gen Slot)
-> (ModelState (WrappedState state) -> ModelState state)
-> ModelState (WrappedState state)
-> Gen Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WrappedState state -> state)
-> ModelState (WrappedState state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WrappedState state -> state
forall state. WrappedState state -> state
unwrapState
  initialState :: WrappedState state
initialState = state -> WrappedState state
forall state. state -> WrappedState state
WrapState state
forall state. ContractModel state => state
initialState
  precondition :: ModelState (WrappedState state)
-> Action (WrappedState state) -> Bool
precondition ModelState (WrappedState state)
s Action (WrappedState state)
a = ModelState state -> Action state -> Bool
forall state.
ContractModel state =>
ModelState state -> Action state -> Bool
precondition ((WrappedState state -> state)
-> ModelState (WrappedState state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WrappedState state -> state
forall state. WrappedState state -> state
unwrapState ModelState (WrappedState state)
s) (Action (WrappedState state) -> Action state
forall state. Action (WrappedState state) -> Action state
unwrapAction Action (WrappedState state)
a)
  nextReactiveState :: SlotNo -> Spec (WrappedState state) ()
nextReactiveState = Spec state () -> Spec (WrappedState state) ()
forall s s' a. Coercible s s' => Spec s a -> Spec s' a
QCCM.coerceSpec (Spec state () -> Spec (WrappedState state) ())
-> (SlotNo -> Spec state ())
-> SlotNo
-> Spec (WrappedState state) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractModel state => Slot -> Spec state ()
forall state. ContractModel state => Slot -> Spec state ()
nextReactiveState @state (Slot -> Spec state ())
-> (SlotNo -> Slot) -> SlotNo -> Spec state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> Slot
fromSlotNo
  nextState :: Action (WrappedState state) -> Spec (WrappedState state) ()
nextState = Spec state () -> Spec (WrappedState state) ()
forall s s' a. Coercible s s' => Spec s a -> Spec s' a
QCCM.coerceSpec (Spec state () -> Spec (WrappedState state) ())
-> (Action (WrappedState state) -> Spec state ())
-> Action (WrappedState state)
-> Spec (WrappedState state) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action state -> Spec state ()
forall state. ContractModel state => Action state -> Spec state ()
nextState (Action state -> Spec state ())
-> (Action (WrappedState state) -> Action state)
-> Action (WrappedState state)
-> Spec state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action (WrappedState state) -> Action state
forall state. Action (WrappedState state) -> Action state
unwrapAction
  shrinkAction :: ModelState (WrappedState state)
-> Action (WrappedState state) -> [Action (WrappedState state)]
shrinkAction ModelState (WrappedState state)
s Action (WrappedState state)
a = Action state -> Action (WrappedState state)
forall state. Action state -> Action (WrappedState state)
WrapAction (Action state -> Action (WrappedState state))
-> [Action state] -> [Action (WrappedState state)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState state -> Action state -> [Action state]
forall state.
ContractModel state =>
ModelState state -> Action state -> [Action state]
shrinkAction ((WrappedState state -> state)
-> ModelState (WrappedState state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WrappedState state -> state
forall state. WrappedState state -> state
unwrapState ModelState (WrappedState state)
s) (Action (WrappedState state) -> Action state
forall state. Action (WrappedState state) -> Action state
unwrapAction Action (WrappedState state)
a)
  restricted :: Action (WrappedState state) -> Bool
restricted = Action state -> Bool
forall state. ContractModel state => Action state -> Bool
restricted (Action state -> Bool)
-> (Action (WrappedState state) -> Action state)
-> Action (WrappedState state)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action (WrappedState state) -> Action state
forall state. Action (WrappedState state) -> Action state
unwrapAction

instance ContractModel state => QCCM.RunModel (WrappedState state) (CMI.SpecificationEmulatorTrace (WrappedState state)) where
  perform :: ModelState (WrappedState state)
-> Action (WrappedState state)
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> RunMonad (SpecificationEmulatorTrace (WrappedState state)) ()
perform ModelState (WrappedState state)
s Action (WrappedState state)
a forall t. HasSymbolicRep t => Symbolic t -> t
e = do
    Handles (WrappedState state)
handles <- Eff
  (Reader (Handles (WrappedState state)) : BaseEmulatorEffects)
  (Handles (WrappedState state))
-> RunMonad
     (SpecificationEmulatorTrace (WrappedState state))
     (Handles (WrappedState state))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff
   (Reader (Handles (WrappedState state)) : BaseEmulatorEffects)
   (Handles (WrappedState state))
 -> RunMonad
      (SpecificationEmulatorTrace (WrappedState state))
      (Handles (WrappedState state)))
-> Eff
     (Reader (Handles (WrappedState state)) : BaseEmulatorEffects)
     (Handles (WrappedState state))
-> RunMonad
     (SpecificationEmulatorTrace (WrappedState state))
     (Handles (WrappedState state))
forall a b. (a -> b) -> a -> b
$ forall (effs :: [* -> *]).
Member (Reader (Handles (WrappedState state))) effs =>
Eff effs (Handles (WrappedState state))
forall r (effs :: [* -> *]). Member (Reader r) effs => Eff effs r
ask @(CMI.Handles (WrappedState state))
    let lookup :: HandleFun state
        lookup :: ContractInstanceKey state w schema err params
-> ContractHandle w schema err
lookup ContractInstanceKey state w schema err params
key =
          case ContractInstanceKey (WrappedState state) w schema err params
-> Handles (WrappedState state)
-> Maybe (WalletContractHandle w schema err)
forall i1 j1 k1 l1 (i2 :: i1) (j2 :: j1) (k2 :: k1) (l2 :: l1)
       (key :: i1 -> j1 -> k1 -> l1 -> *) (val :: i1 -> j1 -> k1 -> *).
(Typeable i2, Typeable j2, Typeable k2, Typeable l2, Typeable key,
 Typeable val, Eq (key i2 j2 k2 l2)) =>
key i2 j2 k2 l2 -> IMap key val -> Maybe (val i2 j2 k2)
CMI.imLookup (ContractInstanceKey state w schema err params
-> ContractInstanceKey (WrappedState state) w schema err params
forall state w (s :: Row *) e p.
ContractInstanceKey state w s e p
-> ContractInstanceKey (WrappedState state) w s e p
WrapContractInstanceKey ContractInstanceKey state w schema err params
key) Handles (WrappedState state)
handles of
            Just (CMI.WalletContractHandle Wallet
_ ContractHandle w schema err
h) -> ContractHandle w schema err
h
            Maybe (WalletContractHandle w schema err)
Nothing                             -> String -> ContractHandle w schema err
forall a. HasCallStack => String -> a
error (String -> ContractHandle w schema err)
-> String -> ContractHandle w schema err
forall a b. (a -> b) -> a -> b
$ String
"contractHandle: No handle for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ContractInstanceKey state w schema err params -> String
forall a. Show a => a -> String
show ContractInstanceKey state w schema err params
key
    (()
_, [(String, SomethingWithSymbolicRep)]
ts) <- Eff
  (Reader (Handles (WrappedState state)) : BaseEmulatorEffects)
  ((), [(String, SomethingWithSymbolicRep)])
-> RunMonad
     (SpecificationEmulatorTrace (WrappedState state))
     ((), [(String, SomethingWithSymbolicRep)])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Eff
   (Reader (Handles (WrappedState state)) : BaseEmulatorEffects)
   ((), [(String, SomethingWithSymbolicRep)])
 -> RunMonad
      (SpecificationEmulatorTrace (WrappedState state))
      ((), [(String, SomethingWithSymbolicRep)]))
-> Eff
     (Reader (Handles (WrappedState state)) : BaseEmulatorEffects)
     ((), [(String, SomethingWithSymbolicRep)])
-> RunMonad
     (SpecificationEmulatorTrace (WrappedState state))
     ((), [(String, SomethingWithSymbolicRep)])
forall a b. (a -> b) -> a -> b
$ Eff BaseEmulatorEffects ((), [(String, SomethingWithSymbolicRep)])
-> Eff
     (Reader (Handles (WrappedState state)) : BaseEmulatorEffects)
     ((), [(String, SomethingWithSymbolicRep)])
forall (effs :: [* -> *]) a (e :: * -> *).
Eff effs a -> Eff (e : effs) a
raise (Eff BaseEmulatorEffects ((), [(String, SomethingWithSymbolicRep)])
 -> Eff
      (Reader (Handles (WrappedState state)) : BaseEmulatorEffects)
      ((), [(String, SomethingWithSymbolicRep)]))
-> Eff
     BaseEmulatorEffects ((), [(String, SomethingWithSymbolicRep)])
-> Eff
     (Reader (Handles (WrappedState state)) : BaseEmulatorEffects)
     ((), [(String, SomethingWithSymbolicRep)])
forall a b. (a -> b) -> a -> b
$ Eff
  (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
  ()
-> Eff
     BaseEmulatorEffects ((), [(String, SomethingWithSymbolicRep)])
forall w (effs :: [* -> *]) a.
Monoid w =>
Eff (Writer w : effs) a -> Eff effs (a, w)
runWriter (Eff
   (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
   ()
 -> Eff
      BaseEmulatorEffects ((), [(String, SomethingWithSymbolicRep)]))
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
-> Eff
     BaseEmulatorEffects ((), [(String, SomethingWithSymbolicRep)])
forall a b. (a -> b) -> a -> b
$ HandleFun state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> ModelState state
-> Action state
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
forall state.
ContractModel state =>
HandleFun state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> ModelState state
-> Action state
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
perform HandleFun state
lookup forall t. HasSymbolicRep t => Symbolic t -> t
e ((WrappedState state -> state)
-> ModelState (WrappedState state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WrappedState state -> state
forall state. WrappedState state -> state
unwrapState ModelState (WrappedState state)
s) (Action (WrappedState state) -> Action state
forall state. Action (WrappedState state) -> Action state
unwrapAction Action (WrappedState state)
a)
    [RunMonad (SpecificationEmulatorTrace (WrappedState state)) ()]
-> RunMonad (SpecificationEmulatorTrace (WrappedState state)) ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ String
-> t
-> RunMonad (SpecificationEmulatorTrace (WrappedState state)) ()
forall (m :: * -> *) t.
(Monad m, HasSymbolicRep t) =>
String -> t -> RunMonad m ()
QCCM.registerSymbolic String
s t
t | (String
s, WithSymbolicRep t
t) <- [(String, SomethingWithSymbolicRep)]
ts ]
  monitoring :: (ModelState (WrappedState state), ModelState (WrappedState state))
-> Action (WrappedState state)
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> SymIndex
-> Property
-> Property
monitoring (ModelState (WrappedState state)
s, ModelState (WrappedState state)
s') Action (WrappedState state)
a forall t. HasSymbolicRep t => Symbolic t -> t
_ SymIndex
_ = (ModelState state, ModelState state)
-> Action state -> Property -> Property
forall state.
ContractModel state =>
(ModelState state, ModelState state)
-> Action state -> Property -> Property
monitoring ((WrappedState state -> state)
-> ModelState (WrappedState state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WrappedState state -> state
forall state. WrappedState state -> state
unwrapState ModelState (WrappedState state)
s, (WrappedState state -> state)
-> ModelState (WrappedState state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WrappedState state -> state
forall state. WrappedState state -> state
unwrapState ModelState (WrappedState state)
s')
                                        (Action (WrappedState state) -> Action state
forall state. Action (WrappedState state) -> Action state
unwrapAction Action (WrappedState state)
a)

toAssetId :: AssetClass -> CardanoAPI.AssetId
toAssetId :: AssetClass -> AssetId
toAssetId (AssetClass (CurrencySymbol
sym, TokenName
tok))
  | CurrencySymbol
sym CurrencySymbol -> CurrencySymbol -> Bool
forall a. Eq a => a -> a -> Bool
== CurrencySymbol
Ada.adaSymbol, TokenName
tok TokenName -> TokenName -> Bool
forall a. Eq a => a -> a -> Bool
== TokenName
Ada.adaToken = AssetId
CardanoAPI.AdaAssetId
  | Bool
otherwise                                 = PolicyId -> AssetName -> AssetId
CardanoAPI.AssetId (CurrencySymbol -> PolicyId
toPolicyId CurrencySymbol
sym) (TokenName -> AssetName
toAssetName TokenName
tok)

toPolicyId :: CurrencySymbol -> CardanoAPI.PolicyId
toPolicyId :: CurrencySymbol -> PolicyId
toPolicyId sym :: CurrencySymbol
sym@(CurrencySymbol BuiltinByteString
bs)
  | Just ScriptHash
hash <- AsType ScriptHash -> ByteString -> Maybe ScriptHash
forall a.
SerialiseAsRawBytes a =>
AsType a -> ByteString -> Maybe a
CardanoAPI.deserialiseFromRawBytes AsType ScriptHash
CardanoAPI.AsScriptHash
                                                    (BuiltinByteString -> ByteString
forall arep a. FromBuiltin arep a => arep -> a
Builtins.fromBuiltin BuiltinByteString
bs) = ScriptHash -> PolicyId
CardanoAPI.PolicyId ScriptHash
hash
  | Bool
otherwise = String -> PolicyId
forall a. HasCallStack => String -> a
error (String -> PolicyId) -> String -> PolicyId
forall a b. (a -> b) -> a -> b
$ String
"Bad policy id: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ CurrencySymbol -> String
forall a. Show a => a -> String
show CurrencySymbol
sym

toAssetName :: TokenName -> CardanoAPI.AssetName
toAssetName :: TokenName -> AssetName
toAssetName (TokenName BuiltinByteString
bs) = ByteString -> AssetName
CardanoAPI.AssetName (ByteString -> AssetName) -> ByteString -> AssetName
forall a b. (a -> b) -> a -> b
$ BuiltinByteString -> ByteString
forall arep a. FromBuiltin arep a => arep -> a
Builtins.fromBuiltin BuiltinByteString
bs

fromAssetId :: CardanoAPI.AssetId -> AssetClass
fromAssetId :: AssetId -> AssetClass
fromAssetId AssetId
CardanoAPI.AdaAssetId            = (CurrencySymbol, TokenName) -> AssetClass
AssetClass (CurrencySymbol
Ada.adaSymbol, TokenName
Ada.adaToken)
fromAssetId (CardanoAPI.AssetId PolicyId
policy AssetName
name) = (CurrencySymbol, TokenName) -> AssetClass
AssetClass (PolicyId -> CurrencySymbol
fromPolicyId PolicyId
policy, AssetName -> TokenName
fromAssetName AssetName
name)

fromPolicyId :: CardanoAPI.PolicyId -> CurrencySymbol
fromPolicyId :: PolicyId -> CurrencySymbol
fromPolicyId (CardanoAPI.PolicyId ScriptHash
hash) = BuiltinByteString -> CurrencySymbol
CurrencySymbol (BuiltinByteString -> CurrencySymbol)
-> (ByteString -> BuiltinByteString)
-> ByteString
-> CurrencySymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> BuiltinByteString
forall a arep. ToBuiltin a arep => a -> arep
Builtins.toBuiltin (ByteString -> CurrencySymbol) -> ByteString -> CurrencySymbol
forall a b. (a -> b) -> a -> b
$ ScriptHash -> ByteString
forall a. SerialiseAsRawBytes a => a -> ByteString
CardanoAPI.serialiseToRawBytes ScriptHash
hash

fromAssetName :: CardanoAPI.AssetName -> TokenName
fromAssetName :: AssetName -> TokenName
fromAssetName (CardanoAPI.AssetName ByteString
bs) = BuiltinByteString -> TokenName
TokenName (BuiltinByteString -> TokenName) -> BuiltinByteString -> TokenName
forall a b. (a -> b) -> a -> b
$ ByteString -> BuiltinByteString
forall a arep. ToBuiltin a arep => a -> arep
Builtins.toBuiltin ByteString
bs

fromSlotNo :: CardanoAPI.SlotNo -> Slot
fromSlotNo :: SlotNo -> Slot
fromSlotNo (CardanoAPI.SlotNo Word64
n) = Integer -> Slot
Slot (Integer -> Slot) -> Integer -> Slot
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n

toSlotNo :: Slot -> CardanoAPI.SlotNo
toSlotNo :: Slot -> SlotNo
toSlotNo (Slot Integer
n) = Word64 -> SlotNo
CardanoAPI.SlotNo (Word64 -> SlotNo) -> Word64 -> SlotNo
forall a b. (a -> b) -> a -> b
$ Integer -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n

type RunsIn state = CMI.WithInstances (WrappedState state)

wait :: forall state. ContractModel state => Integer -> QCCM.Spec state ()
wait :: Integer -> Spec state ()
wait = Spec (RunsIn state) () -> Spec state ()
forall s s' a. Coercible s s' => Spec s a -> Spec s' a
QCCM.coerceSpec (Spec (RunsIn state) () -> Spec state ())
-> (Integer -> Spec (RunsIn state) ()) -> Integer -> Spec state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractModel (RunsIn state) => Integer -> Spec (RunsIn state) ()
forall state. ContractModel state => Integer -> Spec state ()
QCCM.wait @(RunsIn state)

waitUntil :: forall state. ContractModel state => Slot -> QCCM.Spec state ()
waitUntil :: Slot -> Spec state ()
waitUntil = Spec (RunsIn state) () -> Spec state ()
forall s s' a. Coercible s s' => Spec s a -> Spec s' a
QCCM.coerceSpec (Spec (RunsIn state) () -> Spec state ())
-> (Slot -> Spec (RunsIn state) ()) -> Slot -> Spec state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractModel (RunsIn state) => SlotNo -> Spec (RunsIn state) ()
forall state. ContractModel state => SlotNo -> Spec state ()
QCCM.waitUntil @(RunsIn state) (SlotNo -> Spec (RunsIn state) ())
-> (Slot -> SlotNo) -> Slot -> Spec (RunsIn state) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Slot -> SlotNo
toSlotNo

-- | Add tokens to the `balanceChange` of a wallet. The added tokens are subtracted from the
--   `lockedValue` of tokens held by contracts.
deposit :: QCCM.SymValueLike v => Wallet -> v -> QCCM.Spec state ()
deposit :: Wallet -> v -> Spec state ()
deposit = AddressInEra Era -> v -> Spec state ()
forall v state.
SymValueLike v =>
AddressInEra Era -> v -> Spec state ()
QCCM.deposit (AddressInEra Era -> v -> Spec state ())
-> (Wallet -> AddressInEra Era) -> Wallet -> v -> Spec state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wallet -> AddressInEra Era
CMI.walletAddress

-- | Withdraw tokens from a wallet. The withdrawn tokens are added to the `lockedValue` of tokens
--   held by contracts.
withdraw :: QCCM.SymValueLike v => Wallet -> v -> QCCM.Spec state ()
withdraw :: Wallet -> v -> Spec state ()
withdraw = AddressInEra Era -> v -> Spec state ()
forall v state.
SymValueLike v =>
AddressInEra Era -> v -> Spec state ()
QCCM.withdraw (AddressInEra Era -> v -> Spec state ())
-> (Wallet -> AddressInEra Era) -> Wallet -> v -> Spec state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wallet -> AddressInEra Era
CMI.walletAddress

-- | Transfer tokens between wallets, updating their `balances`.
transfer :: QCCM.SymValueLike v
         => Wallet  -- ^ Transfer from this wallet
         -> Wallet  -- ^ to this wallet
         -> v   -- ^ this many tokens
         -> QCCM.Spec state ()
transfer :: Wallet -> Wallet -> v -> Spec state ()
transfer Wallet
w1 Wallet
w2 = AddressInEra Era -> AddressInEra Era -> v -> Spec state ()
forall v state.
SymValueLike v =>
AddressInEra Era -> AddressInEra Era -> v -> Spec state ()
QCCM.transfer (Wallet -> AddressInEra Era
CMI.walletAddress Wallet
w1) (Wallet -> AddressInEra Era
CMI.walletAddress Wallet
w2)

-- | Register the real token corresponding to a symbolic token created
-- in `createToken`.
registerToken :: String -> CardanoAPI.AssetId -> SpecificationEmulatorTrace ()
registerToken :: String
-> AssetId
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
registerToken = String
-> AssetId
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
forall t.
HasSymbolicRep t =>
String
-> t
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
registerSymbolic

-- | Register the real TxOut corresponding to a symbolic TxOut created
-- in `createTxOut`.
registerTxOut :: String -> CardanoAPI.TxOut CardanoAPI.CtxUTxO QCCM.Era -> SpecificationEmulatorTrace ()
registerTxOut :: String
-> TxOut CtxUTxO Era
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
registerTxOut = String
-> TxOut CtxUTxO Era
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
forall t.
HasSymbolicRep t =>
String
-> t
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
registerSymbolic

-- | Register the real TxIn corresponding to a symbolic TxIn created
-- in `createTxIn`.
registerTxIn :: String -> CardanoAPI.TxIn -> SpecificationEmulatorTrace ()
registerTxIn :: String
-> TxIn
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
registerTxIn = String
-> TxIn
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
forall t.
HasSymbolicRep t =>
String
-> t
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
registerSymbolic

registerSymbolic :: QCCM.HasSymbolicRep t => String -> t -> SpecificationEmulatorTrace ()
registerSymbolic :: String
-> t
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
registerSymbolic String
s t
t = [(String, SomethingWithSymbolicRep)]
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
forall w (effs :: [* -> *]).
Member (Writer w) effs =>
w -> Eff effs ()
tell [(String
s, t -> SomethingWithSymbolicRep
forall t. HasSymbolicRep t => t -> SomethingWithSymbolicRep
WithSymbolicRep t
t)]

-- | `delay n` delays emulator execution by `n` slots
delay :: Integer -> SpecificationEmulatorTrace ()
delay :: Integer
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
delay = Eff
  (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
  Slot
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Eff
   (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
   Slot
 -> Eff
      (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
      ())
-> (Integer
    -> Eff
         (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
         Slot)
-> Integer
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     Slot
forall (effs :: [* -> *]).
Member Waiting effs =>
Natural -> Eff effs Slot
Trace.waitNSlots (Natural
 -> Eff
      (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
      Slot)
-> (Integer -> Natural)
-> Integer
-> Eff
     (Writer [(String, SomethingWithSymbolicRep)] : BaseEmulatorEffects)
     Slot
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger

-- TODO: more evidence that we should torch WithInstances and fuse it with WrappedState
type DL state = QCCM.DL (CMI.WithInstances (WrappedState state))

action :: ContractModel state => Action state -> DL state ()
action :: Action state -> DL state ()
action = Action (WithInstances (WrappedState state)) -> DL state ()
forall state a. ActionLike state a => a -> DL state ()
QCCM.action (Action (WithInstances (WrappedState state)) -> DL state ())
-> (Action state -> Action (WithInstances (WrappedState state)))
-> Action state
-> DL state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action (WrappedState state)
-> Action (WithInstances (WrappedState state))
forall s. Action s -> Action (WithInstances s)
CMI.UnderlyingAction (Action (WrappedState state)
 -> Action (WithInstances (WrappedState state)))
-> (Action state -> Action (WrappedState state))
-> Action state
-> Action (WithInstances (WrappedState state))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action state -> Action (WrappedState state)
forall state. Action state -> Action (WrappedState state)
WrapAction

waitUntilDL :: ContractModel state => Slot -> DL state ()
waitUntilDL :: Slot -> DL state ()
waitUntilDL = SlotNo -> DL state ()
forall state. ContractModel state => SlotNo -> DL state ()
QCCM.waitUntilDL (SlotNo -> DL state ()) -> (Slot -> SlotNo) -> Slot -> DL state ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Slot -> SlotNo
toSlotNo

assertModel :: String -> (QCCM.ModelState state -> Bool) -> DL state ()
assertModel :: String -> (ModelState state -> Bool) -> DL state ()
assertModel String
s ModelState state -> Bool
p = String
-> (ModelState (WithInstances (WrappedState state)) -> Bool)
-> DL state ()
forall state. String -> (ModelState state -> Bool) -> DL state ()
QCCM.assertModel String
s (ModelState state -> Bool
p (ModelState state -> Bool)
-> (ModelState (WithInstances (WrappedState state))
    -> ModelState state)
-> ModelState (WithInstances (WrappedState state))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WithInstances (WrappedState state) -> state)
-> ModelState (WithInstances (WrappedState state))
-> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WithInstances (WrappedState state) -> state
coerce)

type Actions state = QCCM.Actions (CMI.WithInstances (WrappedState state))

-- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final
--   wallet balance changes. Equivalent to
--
-- @
-- propRunActions_ hs actions = `propRunActions` hs (`const` `$` `pure` `True`) actions
-- @
propRunActions_ ::
    ContractModel state
    => Actions state                 -- ^ The actions to run
    -> Property
propRunActions_ :: Actions state -> Property
propRunActions_ Actions state
actions =
    (ModelState state -> TracePredicate) -> Actions state -> Property
forall state.
ContractModel state =>
(ModelState state -> TracePredicate) -> Actions state -> Property
propRunActions (\ ModelState state
_ -> Bool -> TracePredicate
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) Actions state
actions

-- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final
--   wallet balance changes, and that the given `TracePredicate` holds at the end. Equivalent to:
--
-- @
-- propRunActions = `propRunActionsWithOptions` `defaultCheckOptionsContractModel` `defaultCoverageOptions`
-- @
propRunActions ::
    ContractModel state
    => (QCCM.ModelState state -> TracePredicate) -- ^ Predicate to check at the end
    -> Actions state                         -- ^ The actions to run
    -> Property
propRunActions :: (ModelState state -> TracePredicate) -> Actions state -> Property
propRunActions = CheckOptions
-> CoverageOptions
-> (ModelState state -> TracePredicate)
-> Actions state
-> Property
forall state.
ContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState state -> TracePredicate)
-> Actions state
-> Property
propRunActionsWithOptions CheckOptions
CMI.defaultCheckOptionsContractModel CoverageOptions
CMI.defaultCoverageOptions

-- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final
--   wallet balance changes, that no off-chain contract instance crashed, and that the given
--   `TracePredicate` holds at the end. The predicate has access to the final model state.
--
--   The `Actions` argument can be generated by a `forAllDL` from a `DL` scenario, or using the
--   `Arbitrary` instance for actions which generates random actions using `arbitraryAction`:
--
-- >>> quickCheck $ propRunActions_ handles
-- +++ OK, passed 100 tests
-- >>> quickCheck $ forAllDL dl $ propRunActions_ handles
-- +++ OK, passed 100 tests
--
--   The options argument can be used to configure the emulator--setting initial wallet balances,
--   the maximum number of slots to run for, and the log level for the emulator trace printed on
--   failing tests:
--
-- @
-- options :: `Map` `Wallet` `Value` -> `Slot` -> `Control.Monad.Freer.Extras.Log.LogLevel` -> `CheckOptions`
-- options dist slot logLevel =
--     `defaultCheckOptions` `&` `emulatorConfig` . `Plutus.Trace.Emulator.initialChainState` `.~` `Left` dist
--                           `&` `minLogLevel`                        `.~` logLevel
-- @
--
propRunActionsWithOptions ::
    ContractModel state
    => CheckOptions                               -- ^ Emulator options
    -> CMI.CoverageOptions                        -- ^ Coverage options
    -> (QCCM.ModelState state -> TracePredicate)  -- ^ Predicate to check at the end
    -> Actions state                              -- ^ The actions to run
    -> Property
propRunActionsWithOptions :: CheckOptions
-> CoverageOptions
-> (ModelState state -> TracePredicate)
-> Actions state
-> Property
propRunActionsWithOptions CheckOptions
opts CoverageOptions
copts ModelState state -> TracePredicate
predicate Actions state
actions =
  CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances (WrappedState state))
    -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances (WrappedState state))
    -> Property)
-> Actions state
-> Property
forall state.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> (ModelState (WithInstances state) -> TracePredicate)
-> (ProtocolParameters
    -> ContractModelResult (WithInstances state) -> Property)
-> Actions (WithInstances state)
-> Property
CMI.propRunActionsWithOptions CheckOptions
opts CoverageOptions
copts (ModelState state -> TracePredicate
predicate (ModelState state -> TracePredicate)
-> (ModelState (WithInstances (WrappedState state))
    -> ModelState state)
-> ModelState (WithInstances (WrappedState state))
-> TracePredicate
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (WithInstances (WrappedState state) -> state)
-> ModelState (WithInstances (WrappedState state))
-> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WithInstances (WrappedState state) -> state
coerce) ProtocolParameters
-> ContractModelResult (WithInstances (WrappedState state))
-> Property
forall state.
ProtocolParameters -> ContractModelResult state -> Property
CMI.balanceChangePredicate Actions state
actions

-- | Sanity check a `ContractModel`. Ensures that wallet balances are not always unchanged.
propSanityCheckModel :: forall state. ContractModel state => Property
propSanityCheckModel :: Property
propSanityCheckModel =
  (Actions (WithInstances (WrappedState state)) -> Bool) -> Property
forall prop. Testable prop => prop -> Property
QC.expectFailure (ModelState (WithInstances (WrappedState state)) -> Bool
forall state. ModelState state -> Bool
noBalanceChanges (ModelState (WithInstances (WrappedState state)) -> Bool)
-> (Actions (WithInstances (WrappedState state))
    -> ModelState (WithInstances (WrappedState state)))
-> Actions (WithInstances (WrappedState state))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractModel (WithInstances (WrappedState state)) =>
Actions (WithInstances (WrappedState state))
-> ModelState (WithInstances (WrappedState state))
forall state.
ContractModel state =>
Actions state -> ModelState state
QCCM.stateAfter @(CMI.WithInstances (WrappedState state)))
  where
    noBalanceChanges :: ModelState state -> Bool
noBalanceChanges ModelState state
s = (SymValue -> Bool) -> Map (AddressInEra Era) SymValue -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SymValue -> Bool
QCCM.symIsZero (ModelState state
s ModelState state
-> Getting
     (Map (AddressInEra Era) SymValue)
     (ModelState state)
     (Map (AddressInEra Era) SymValue)
-> Map (AddressInEra Era) SymValue
forall s a. s -> Getting a s a -> a
^. Getting
  (Map (AddressInEra Era) SymValue)
  (ModelState state)
  (Map (AddressInEra Era) SymValue)
forall state.
Getter (ModelState state) (Map (AddressInEra Era) SymValue)
QCCM.balanceChanges)

-- | Sanity check a `ContractModel`. Ensures that all assertions in
-- the property generation succeed.
propSanityCheckAssertions :: forall state. ContractModel state => Actions state -> Property
propSanityCheckAssertions :: Actions state -> Property
propSanityCheckAssertions Actions state
as = ModelState (WithInstances (WrappedState state)) -> Property
forall state. ModelState state -> Property
QCCM.asserts (ModelState (WithInstances (WrappedState state)) -> Property)
-> ModelState (WithInstances (WrappedState state)) -> Property
forall a b. (a -> b) -> a -> b
$ Actions state -> ModelState (WithInstances (WrappedState state))
forall state.
ContractModel state =>
Actions state -> ModelState state
QCCM.stateAfter Actions state
as

-- | Sanity check a `ContractModel`. Ensures that `nextReactiveState` is idempotent.
propSanityCheckReactive :: forall state. (ContractModel state, Eq state) => Actions state -> Positive Integer -> Positive Integer -> Property
propSanityCheckReactive :: Actions state -> Positive Integer -> Positive Integer -> Property
propSanityCheckReactive Actions state
as (Positive Integer
sl) (Positive Integer
sl') =
    let s0 :: ModelState (WithInstances (WrappedState state))
s0 = Actions state -> ModelState (WithInstances (WrappedState state))
forall state.
ContractModel state =>
Actions state -> ModelState state
QCCM.stateAfter Actions state
as
        sl1 :: SlotNo
sl1 = ModelState (WithInstances (WrappedState state))
s0 ModelState (WithInstances (WrappedState state))
-> Getting
     SlotNo (ModelState (WithInstances (WrappedState state))) SlotNo
-> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting
  SlotNo (ModelState (WithInstances (WrappedState state))) SlotNo
forall state. Getter (ModelState state) SlotNo
QCCM.currentSlot SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ Word64 -> SlotNo
CardanoAPI.SlotNo (Integer -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sl)
        sl2 :: SlotNo
sl2 = SlotNo
sl1 SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ Word64 -> SlotNo
CardanoAPI.SlotNo (Integer -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sl')
        s1 :: ModelState (WithInstances (WrappedState state))
s1 = Spec (WithInstances (WrappedState state)) ()
-> Var SymIndex
-> ModelState (WithInstances (WrappedState state))
-> ModelState (WithInstances (WrappedState state))
forall state.
Spec state ()
-> Var SymIndex -> ModelState state -> ModelState state
QCCM.runSpec (Spec state () -> Spec (WithInstances (WrappedState state)) ()
forall s s' a. Coercible s s' => Spec s a -> Spec s' a
QCCM.coerceSpec (Spec state () -> Spec (WithInstances (WrappedState state)) ())
-> Spec state () -> Spec (WithInstances (WrappedState state)) ()
forall a b. (a -> b) -> a -> b
$ Slot -> Spec state ()
forall state. ContractModel state => Slot -> Spec state ()
nextReactiveState @state (SlotNo -> Slot
fromSlotNo SlotNo
sl1) Spec state () -> Spec state () -> Spec state ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Slot -> Spec state ()
forall state. ContractModel state => Slot -> Spec state ()
nextReactiveState (SlotNo -> Slot
fromSlotNo SlotNo
sl2)) (String -> Var SymIndex
forall a. HasCallStack => String -> a
error String
"unreachable") ModelState (WithInstances (WrappedState state))
s0
        s2 :: ModelState (WithInstances (WrappedState state))
s2 = Spec (WithInstances (WrappedState state)) ()
-> Var SymIndex
-> ModelState (WithInstances (WrappedState state))
-> ModelState (WithInstances (WrappedState state))
forall state.
Spec state ()
-> Var SymIndex -> ModelState state -> ModelState state
QCCM.runSpec (Spec state () -> Spec (WithInstances (WrappedState state)) ()
forall s s' a. Coercible s s' => Spec s a -> Spec s' a
QCCM.coerceSpec (Spec state () -> Spec (WithInstances (WrappedState state)) ())
-> Spec state () -> Spec (WithInstances (WrappedState state)) ()
forall a b. (a -> b) -> a -> b
$ Slot -> Spec state ()
forall state. ContractModel state => Slot -> Spec state ()
nextReactiveState @state (SlotNo -> Slot
fromSlotNo SlotNo
sl2)) (String -> Var SymIndex
forall a. HasCallStack => String -> a
error String
"unreachable") ModelState (WithInstances (WrappedState state))
s0
    in String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Balance changes not idempotent"        (ModelState (WithInstances (WrappedState state))
s1 ModelState (WithInstances (WrappedState state))
-> Getting
     (Map (AddressInEra Era) SymValue)
     (ModelState (WithInstances (WrappedState state)))
     (Map (AddressInEra Era) SymValue)
-> Map (AddressInEra Era) SymValue
forall s a. s -> Getting a s a -> a
^. Getting
  (Map (AddressInEra Era) SymValue)
  (ModelState (WithInstances (WrappedState state)))
  (Map (AddressInEra Era) SymValue)
forall state.
Getter (ModelState state) (Map (AddressInEra Era) SymValue)
QCCM.balanceChanges Map (AddressInEra Era) SymValue
-> Map (AddressInEra Era) SymValue -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ModelState (WithInstances (WrappedState state))
s2 ModelState (WithInstances (WrappedState state))
-> Getting
     (Map (AddressInEra Era) SymValue)
     (ModelState (WithInstances (WrappedState state)))
     (Map (AddressInEra Era) SymValue)
-> Map (AddressInEra Era) SymValue
forall s a. s -> Getting a s a -> a
^. Getting
  (Map (AddressInEra Era) SymValue)
  (ModelState (WithInstances (WrappedState state)))
  (Map (AddressInEra Era) SymValue)
forall state.
Getter (ModelState state) (Map (AddressInEra Era) SymValue)
QCCM.balanceChanges) Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&.
       String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"Contract state changes not idempotent" (ModelState (WithInstances (WrappedState state))
s1 ModelState (WithInstances (WrappedState state))
-> Getting
     (WithInstances (WrappedState state))
     (ModelState (WithInstances (WrappedState state)))
     (WithInstances (WrappedState state))
-> WithInstances (WrappedState state)
forall s a. s -> Getting a s a -> a
^. Getting
  (WithInstances (WrappedState state))
  (ModelState (WithInstances (WrappedState state)))
  (WithInstances (WrappedState state))
forall state1 state2.
Lens (ModelState state1) (ModelState state2) state1 state2
QCCM.contractState  WithInstances (WrappedState state)
-> WithInstances (WrappedState state) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ModelState (WithInstances (WrappedState state))
s2 ModelState (WithInstances (WrappedState state))
-> Getting
     (WithInstances (WrappedState state))
     (ModelState (WithInstances (WrappedState state)))
     (WithInstances (WrappedState state))
-> WithInstances (WrappedState state)
forall s a. s -> Getting a s a -> a
^. Getting
  (WithInstances (WrappedState state))
  (ModelState (WithInstances (WrappedState state)))
  (WithInstances (WrappedState state))
forall state1 state2.
Lens (ModelState state1) (ModelState state2) state1 state2
QCCM.contractState)

fromValue :: Value -> CardanoAPI.Value
fromValue :: Value -> Value
fromValue (Value Map CurrencySymbol (Map TokenName Integer)
m) = [(AssetId, Quantity)] -> Value
CardanoAPI.valueFromList [ (AssetClass -> AssetId
toAssetId ((CurrencySymbol, TokenName) -> AssetClass
AssetClass (CurrencySymbol
cls, TokenName
sym)), Integer -> Quantity
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
                                               | (CurrencySymbol
cls, Map TokenName Integer
toks) <- Map CurrencySymbol (Map TokenName Integer)
-> [(CurrencySymbol, Map TokenName Integer)]
forall k v. Map k v -> [(k, v)]
AssocMap.toList Map CurrencySymbol (Map TokenName Integer)
m
                                               , (TokenName
sym, Integer
n)    <- Map TokenName Integer -> [(TokenName, Integer)]
forall k v. Map k v -> [(k, v)]
AssocMap.toList Map TokenName Integer
toks
                                               ]
instance QCCM.SymValueLike Value where
  toSymValue :: Value -> SymValue
toSymValue = Value -> SymValue
forall v. SymValueLike v => v -> SymValue
QCCM.toSymValue (Value -> SymValue) -> (Value -> Value) -> Value -> SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Value
fromValue

instance QCCM.TokenLike AssetClass where
  symAssetIdValueOf :: SymValue -> AssetClass -> Quantity
symAssetIdValueOf SymValue
v = SymValue -> AssetId -> Quantity
forall t. TokenLike t => SymValue -> t -> Quantity
QCCM.symAssetIdValueOf SymValue
v (AssetId -> Quantity)
-> (AssetClass -> AssetId) -> AssetClass -> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AssetClass -> AssetId
toAssetId
  symAssetIdValue :: AssetClass -> Quantity -> SymValue
symAssetIdValue = AssetId -> Quantity -> SymValue
forall t. TokenLike t => t -> Quantity -> SymValue
QCCM.symAssetIdValue (AssetId -> Quantity -> SymValue)
-> (AssetClass -> AssetId) -> AssetClass -> Quantity -> SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AssetClass -> AssetId
toAssetId

instance QCCM.SymValueLike Ada.Ada where
  toSymValue :: Ada -> SymValue
toSymValue = Value -> SymValue
forall v. SymValueLike v => v -> SymValue
QCCM.toSymValue (Value -> SymValue) -> (Ada -> Value) -> Ada -> SymValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ada -> Value
Ada.toValue

type NoLockedFundsProof state = CMI.NoLockedFundsProof (WrappedState state)
type NoLockedFundsProofLight state = CMI.NoLockedFundsProofLight (WrappedState state)

-- | Get a component of the model state.
askModelState :: (Coercible (QCCM.StateType m) state, QCCM.GetModelState m) => (QCCM.ModelState state -> a) -> m a
askModelState :: (ModelState state -> a) -> m a
askModelState ModelState state -> a
f = (ModelState state -> a
f (ModelState state -> a)
-> (ModelState (StateType m) -> ModelState state)
-> ModelState (StateType m)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateType m -> state)
-> ModelState (StateType m) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap StateType m -> state
coerce) (ModelState (StateType m) -> a)
-> m (ModelState (StateType m)) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (ModelState (StateType m))
forall (m :: * -> *).
GetModelState m =>
m (ModelState (StateType m))
QCCM.getModelState

-- | Get a component of the contract state using a lens.
viewContractState :: (Coercible (QCCM.StateType m) state, QCCM.GetModelState m) => Getting a state a -> m a
viewContractState :: Getting a state a -> m a
viewContractState Getting a state a
l = (ModelState state -> a) -> m a
forall (m :: * -> *) state a.
(Coercible (StateType m) state, GetModelState m) =>
(ModelState state -> a) -> m a
askModelState (Getting a (ModelState state) a -> ModelState state -> a
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Getting a (ModelState state) a -> ModelState state -> a)
-> Getting a (ModelState state) a -> ModelState state -> a
forall a b. (a -> b) -> a -> b
$ (state -> Const a state)
-> ModelState state -> Const a (ModelState state)
forall state1 state2.
Lens (ModelState state1) (ModelState state2) state1 state2
QCCM.contractState ((state -> Const a state)
 -> ModelState state -> Const a (ModelState state))
-> Getting a state a -> Getting a (ModelState state) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting a state a
l)

currentSlot :: Getter (QCCM.ModelState state) Slot
currentSlot :: (Slot -> f Slot) -> ModelState state -> f (ModelState state)
currentSlot = (SlotNo -> f SlotNo) -> ModelState state -> f (ModelState state)
forall state. Getter (ModelState state) SlotNo
QCCM.currentSlot ((SlotNo -> f SlotNo) -> ModelState state -> f (ModelState state))
-> ((Slot -> f Slot) -> SlotNo -> f SlotNo)
-> (Slot -> f Slot)
-> ModelState state
-> f (ModelState state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SlotNo -> Slot) -> (Slot -> f Slot) -> SlotNo -> f SlotNo
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to SlotNo -> Slot
fromSlotNo

balanceChange :: Wallet -> Getter (QCCM.ModelState state) QCCM.SymValue
balanceChange :: Wallet -> Getter (ModelState state) SymValue
balanceChange = AddressInEra Era
-> (SymValue -> f SymValue)
-> ModelState state
-> f (ModelState state)
forall state.
Ord (AddressInEra Era) =>
AddressInEra Era -> Getter (ModelState state) SymValue
QCCM.balanceChange (AddressInEra Era
 -> (SymValue -> f SymValue)
 -> ModelState state
 -> f (ModelState state))
-> (Wallet -> AddressInEra Era)
-> Wallet
-> (SymValue -> f SymValue)
-> ModelState state
-> f (ModelState state)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wallet -> AddressInEra Era
CMI.walletAddress

-- | Check that running a contract model does not result in validation
-- failures that are not accepted by the whitelist.
checkErrorWhitelist :: ContractModel m
                    => CMI.Whitelist
                    -> Actions m
                    -> Property
checkErrorWhitelist :: Whitelist -> Actions m -> Property
checkErrorWhitelist = CheckOptions
-> CoverageOptions -> Whitelist -> Actions m -> Property
forall m.
ContractModel m =>
CheckOptions
-> CoverageOptions -> Whitelist -> Actions m -> Property
checkErrorWhitelistWithOptions CheckOptions
CMI.defaultCheckOptionsContractModel CoverageOptions
CMI.defaultCoverageOptions

-- | Check that running a contract model does not result in validation
-- failures that are not accepted by the whitelist.
checkErrorWhitelistWithOptions :: forall m. ContractModel m
                               => CheckOptions
                               -> CMI.CoverageOptions
                               -> CMI.Whitelist
                               -> Actions m
                               -> Property
checkErrorWhitelistWithOptions :: CheckOptions
-> CoverageOptions -> Whitelist -> Actions m -> Property
checkErrorWhitelistWithOptions = CheckOptions
-> CoverageOptions -> Whitelist -> Actions m -> Property
forall m.
CheckableContractModel m =>
CheckOptions
-> CoverageOptions
-> Whitelist
-> Actions (WithInstances m)
-> Property
CMI.checkErrorWhitelistWithOptions

-- | Perform a light-weight check to find egregious double satisfaction
-- vulnerabilities in contracts.
--
-- A counterexample to this property consists of three transactions.
-- * The first transaction is a valid transaction from the trace generated by the contract model.
-- * The second transaction, generated by redirecting
--   a non-datum pubkey output from a non-signer to a signer in the first transaction,
--   fails to validate. This demonstrates that funds can't simply be stolen.
-- * The third transaction goes through and manages to steal funds by altering the first transaction.
--   It is generated by adding another script input (with the same value as the non-signer non-stealable
--   pubkey output) and adding a datum to the non-signer non-stealable pubkey output, and giving the
--   extra value from the new script input to a signer.
checkDoubleSatisfaction :: forall m. ContractModel m
                        => Actions m
                        -> Property
checkDoubleSatisfaction :: Actions m -> Property
checkDoubleSatisfaction = CheckOptions -> CoverageOptions -> Actions m -> Property
forall m.
ContractModel m =>
CheckOptions -> CoverageOptions -> Actions m -> Property
checkDoubleSatisfactionWithOptions CheckOptions
CMI.defaultCheckOptionsContractModel
                                                             CoverageOptions
CMI.defaultCoverageOptions

-- | Perform a light-weight check to find egregious double satisfaction
-- vulnerabilities in contracts, with options.
checkDoubleSatisfactionWithOptions :: forall m. ContractModel m
                                   => CheckOptions
                                   -> CMI.CoverageOptions
                                   -> Actions m
                                   -> Property
checkDoubleSatisfactionWithOptions :: CheckOptions -> CoverageOptions -> Actions m -> Property
checkDoubleSatisfactionWithOptions CheckOptions
opts CoverageOptions
covopts Actions m
acts =
  CheckOptions
-> CoverageOptions -> ThreatModel () -> Actions m -> Property
forall state a.
CheckableContractModel state =>
CheckOptions
-> CoverageOptions
-> ThreatModel a
-> Actions (WithInstances state)
-> Property
CMI.checkThreatModelWithOptions CheckOptions
opts CoverageOptions
covopts ThreatModel ()
QCCM.doubleSatisfaction Actions m
acts

instance QCCM.HasSymbolics Wallet where
  getAllSymbolics :: Wallet -> SymCollectionIndex
getAllSymbolics Wallet
_ = SymCollectionIndex
forall a. Monoid a => a
mempty
instance QCCM.HasSymbolics Value where
  getAllSymbolics :: Value -> SymCollectionIndex
getAllSymbolics Value
_ = SymCollectionIndex
forall a. Monoid a => a
mempty

data SomeContractInstanceKey state where
  Key :: (CMI.SchemaConstraints w s e, Typeable p)
      => ContractInstanceKey state w s e p
      -> SomeContractInstanceKey state

instance ContractModel state => Eq (SomeContractInstanceKey state) where
  Key ContractInstanceKey state w s e p
k == :: SomeContractInstanceKey state
-> SomeContractInstanceKey state -> Bool
== Key ContractInstanceKey state w s e p
k' = ContractInstanceKey state w s e p
-> Maybe (ContractInstanceKey state w s e p)
forall a. a -> Maybe a
Just ContractInstanceKey state w s e p
k Maybe (ContractInstanceKey state w s e p)
-> Maybe (ContractInstanceKey state w s e p) -> Bool
forall a. Eq a => a -> a -> Bool
== ContractInstanceKey state w s e p
-> Maybe (ContractInstanceKey state w s e p)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast ContractInstanceKey state w s e p
k'

instance ContractModel state => Show (SomeContractInstanceKey state) where
  showsPrec :: Int -> SomeContractInstanceKey state -> ShowS
showsPrec Int
d (Key ContractInstanceKey state w s e p
k) = Int -> ContractInstanceKey state w s e p -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d ContractInstanceKey state w s e p
k

invSymValue :: QCCM.SymValue -> QCCM.SymValue
invSymValue :: SymValue -> SymValue
invSymValue = SymValue -> SymValue
QCCM.inv

instance QCCM.HasSymbolics Builtins.BuiltinByteString where
  getAllSymbolics :: BuiltinByteString -> SymCollectionIndex
getAllSymbolics BuiltinByteString
_ = SymCollectionIndex
forall a. Monoid a => a
mempty
deriving via QCSM.HasNoVariables Builtins.BuiltinByteString instance QCSM.HasVariables Builtins.BuiltinByteString