-
Notifications
You must be signed in to change notification settings - Fork 477
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Move state machine code to own module
- Loading branch information
Showing
6 changed files
with
175 additions
and
166 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
61 changes: 0 additions & 61 deletions
61
plutus-use-cases/src/Language/PlutusTx/Coordination/Contracts/GameStateMachine/Stage0.hs
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,70 @@ | ||
| {-# LANGUAGE ScopedTypeVariables #-} | ||
| {-# LANGUAGE TypeApplications #-} | ||
| {-# LANGUAGE TemplateHaskell #-} | ||
| -- | On-chain code fragments for creating a state machine. First | ||
| -- define a @StateMachine s i@ with input type @i@ and state type @s@. Then | ||
| -- use 'mkValidator' in on-chain code to check the required hashes and | ||
| -- validate the transition, and 'initialState' and 'transition' in off-chain | ||
| -- code to obtain the values for data and redeemer scripts. | ||
| module Language.PlutusTx.StateMachine( | ||
| StateMachine(..) | ||
| , mkValidator | ||
| , initialState | ||
| , transition | ||
| ) where | ||
|
|
||
|
|
||
| import qualified Language.PlutusTx as P | ||
|
|
||
| import Ledger.Validation (PendingTx) | ||
| import qualified Ledger.Validation as V | ||
|
|
||
| import Language.Haskell.TH (Q, TExp) | ||
|
|
||
| -- | Specification of a state machine | ||
| data StateMachine s i = StateMachine { | ||
| smTransition :: s -> i -> s | ||
| , smStateEq :: s -> s -> Bool | ||
| } | ||
|
|
||
| -- | Create a transition script from an initial state of type | ||
| -- @s@. | ||
| initialState :: forall s i. s -> (s, Maybe i) | ||
| initialState s = (s, Nothing) | ||
|
|
||
| -- | Create a transition script from a new state of type @s@ and | ||
| -- an input of type @i@. | ||
| transition :: forall s i. s -> i -> (s, Maybe i) | ||
| transition newState input = (newState, Just input) | ||
|
|
||
| -- | Turn a transition function 's -> i -> s' into a validator script. | ||
| mkValidator :: Q (TExp (StateMachine s i -> (s, Maybe i) -> (s, Maybe i) -> PendingTx -> ())) | ||
| mkValidator = [|| | ||
| let | ||
| mkValidator' :: forall s i. StateMachine s i -> (s, Maybe i) -> (s, Maybe i) -> PendingTx -> () | ||
| mkValidator' sm (currentState, _) (newState, Just input) p = | ||
| let | ||
| StateMachine trans sEq = sm | ||
| (vh, V.RedeemerHash rh) = $$(V.ownHashes) p | ||
| expectedState = trans currentState input | ||
|
|
||
| stateOk = | ||
| $$(P.traceIfFalseH) "State transition invalid - 'expectedState' not equal to 'newState'" | ||
| (sEq expectedState newState) | ||
|
|
||
| dataScriptHashOk = | ||
| let relevantOutputs = | ||
| $$(P.map) (\(ds, _) -> ds) | ||
| ($$(V.scriptOutputsAt) vh p) | ||
| dsHashOk (V.DataScriptHash dh) = $$(P.equalsByteString) dh rh | ||
| in | ||
| $$(P.traceIfFalseH) "State transition invalid - data script hash not equal to redeemer hash" | ||
| ($$(P.all) dsHashOk relevantOutputs) | ||
| in | ||
| if $$(P.and) stateOk dataScriptHashOk | ||
| then () | ||
| else ($$(P.error) ($$(P.traceH) "State transition failed" ())) | ||
|
|
||
|
|
||
| in mkValidator' | ||
| ||] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,101 +1,101 @@ | ||
| {-# LANGUAGE FlexibleContexts #-} | ||
| module Spec.GameStateMachine(tests) where | ||
|
|
||
| import Control.Monad (void) | ||
| import qualified Data.Map as Map | ||
| import qualified Spec.Size as Size | ||
| import Test.Tasty | ||
| import qualified Test.Tasty.HUnit as HUnit | ||
|
|
||
| import Language.PlutusTx.Coordination.Contracts.GameStateMachine as G | ||
| import qualified Ledger.Ada as Ada | ||
| import Ledger.Value (Value) | ||
| import qualified Wallet.API as W | ||
| import qualified Wallet.Emulator as EM | ||
|
|
||
| tests :: TestTree | ||
| tests = | ||
| let initialState = EM.emulatorStateInitialDist | ||
| (Map.fromList [ ( EM.walletPubKey w1, initialVal) | ||
| , ( EM.walletPubKey w2, initialVal) | ||
| , ( EM.walletPubKey w3, initialVal) ]) | ||
| checkResult (result, st) step = | ||
| case result of | ||
| Left err -> do | ||
| _ <- step (show $ EM.emLog st) | ||
| _ <- step (show err) | ||
| HUnit.assertFailure "own funds not equal" | ||
| Right _ -> | ||
| Size.reasonable G.gameValidator 55000 | ||
| in | ||
| testGroup "state machine tests" [ | ||
| HUnit.testCaseSteps "run a successful game trace" | ||
| (checkResult (EM.runEmulator initialState runGameSuccess)), | ||
| HUnit.testCaseSteps "run a 2nd successful game trace" | ||
| (checkResult (EM.runEmulator initialState runGameSuccess2)), | ||
| HUnit.testCaseSteps "run a failed trace" | ||
| (checkResult (EM.runEmulator initialState runGameFailure)) | ||
| ] | ||
|
|
||
| initialVal :: Value | ||
| initialVal = Ada.adaValueOf 10 | ||
|
|
||
| w1 :: EM.Wallet | ||
| w1 = EM.Wallet 1 | ||
|
|
||
| w2 :: EM.Wallet | ||
| w2 = EM.Wallet 2 | ||
|
|
||
| w3 :: EM.Wallet | ||
| w3 = EM.Wallet 3 | ||
|
|
||
| processAndNotify :: W.WalletAPI m => EM.Trace m () | ||
| processAndNotify = void (EM.addBlocksAndNotify [w1, w2, w3] 1) | ||
|
|
||
| -- Wallet 1 locks some funds using the secret "hello". Then wallet 1 | ||
| -- transfers the token to wallet 2, and wallet 2 makes a correct guess | ||
| -- and locks the remaining funds using the secret "new secret". | ||
| runGameSuccess :: (EM.MonadEmulator m) => m () | ||
| runGameSuccess = void $ EM.processEmulated $ do | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 G.startGame | ||
| _ <- EM.runWalletAction w2 G.startGame | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (G.lock "hello" 8) | ||
| processAndNotify | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (W.payToPublicKey_ W.defaultSlotRange G.gameTokenVal (EM.walletPubKey w2)) | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w2 (guess "hello" "new secret" 3 5) | ||
| processAndNotify | ||
| EM.assertOwnFundsEq w2 (initialVal <> Ada.adaValueOf 3 <> G.gameTokenVal) | ||
|
|
||
| -- Runs 'runGameSuccess', then wallet 2 transfers the token to wallet 1, which takes | ||
| -- out another couple of Ada. | ||
| runGameSuccess2 :: (EM.MonadEmulator m) => m () | ||
| runGameSuccess2 = do | ||
| runGameSuccess | ||
|
|
||
| void $ EM.processEmulated $ do | ||
| _ <- EM.runWalletAction w2 (W.payToPublicKey_ W.defaultSlotRange G.gameTokenVal (EM.walletPubKey w1)) | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (guess "new secret" "hello" 2 3) | ||
| processAndNotify | ||
| EM.assertOwnFundsEq w1 (Ada.adaValueOf 4 <> G.gameTokenVal) | ||
|
|
||
| -- Wallet 2 makes a wrong guess and fails to take out the funds | ||
| runGameFailure :: (EM.MonadEmulator m) => m () | ||
| runGameFailure = void $ EM.processEmulated $ do | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 G.startGame | ||
| _ <- EM.runWalletAction w2 G.startGame | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (G.lock "hello" 8) | ||
| processAndNotify | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (W.payToPublicKey_ W.defaultSlotRange G.gameTokenVal (EM.walletPubKey w2)) | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w2 (guess "hola" "new secret" 3 5) | ||
| processAndNotify | ||
| EM.assertOwnFundsEq w2 (initialVal <> G.gameTokenVal) | ||
|
|
||
| {-# LANGUAGE FlexibleContexts #-} | ||
| module Spec.GameStateMachine(tests) where | ||
|
|
||
| import Control.Monad (void) | ||
| import qualified Data.Map as Map | ||
| import qualified Spec.Size as Size | ||
| import Test.Tasty | ||
| import qualified Test.Tasty.HUnit as HUnit | ||
|
|
||
| import Language.PlutusTx.Coordination.Contracts.GameStateMachine as G | ||
| import qualified Ledger.Ada as Ada | ||
| import Ledger.Value (Value) | ||
| import qualified Wallet.API as W | ||
| import qualified Wallet.Emulator as EM | ||
|
|
||
| tests :: TestTree | ||
| tests = | ||
| let initialState = EM.emulatorStateInitialDist | ||
| (Map.fromList [ ( EM.walletPubKey w1, initialVal) | ||
| , ( EM.walletPubKey w2, initialVal) | ||
| , ( EM.walletPubKey w3, initialVal) ]) | ||
| checkResult (result, st) step = | ||
| case result of | ||
| Left err -> do | ||
| _ <- step (show $ EM.emLog st) | ||
| _ <- step (show err) | ||
| HUnit.assertFailure "own funds not equal" | ||
| Right _ -> | ||
| Size.reasonable G.gameValidator 55000 | ||
| in | ||
| testGroup "state machine tests" [ | ||
| HUnit.testCaseSteps "run a successful game trace" | ||
| (checkResult (EM.runEmulator initialState runGameSuccess)), | ||
| HUnit.testCaseSteps "run a 2nd successful game trace" | ||
| (checkResult (EM.runEmulator initialState runGameSuccess2)), | ||
| HUnit.testCaseSteps "run a failed trace" | ||
| (checkResult (EM.runEmulator initialState runGameFailure)) | ||
| ] | ||
|
|
||
| initialVal :: Value | ||
| initialVal = Ada.adaValueOf 10 | ||
|
|
||
| w1 :: EM.Wallet | ||
| w1 = EM.Wallet 1 | ||
|
|
||
| w2 :: EM.Wallet | ||
| w2 = EM.Wallet 2 | ||
|
|
||
| w3 :: EM.Wallet | ||
| w3 = EM.Wallet 3 | ||
|
|
||
| processAndNotify :: W.WalletAPI m => EM.Trace m () | ||
| processAndNotify = void (EM.addBlocksAndNotify [w1, w2, w3] 1) | ||
|
|
||
| -- Wallet 1 locks some funds using the secret "hello". Then wallet 1 | ||
| -- transfers the token to wallet 2, and wallet 2 makes a correct guess | ||
| -- and locks the remaining funds using the secret "new secret". | ||
| runGameSuccess :: (EM.MonadEmulator m) => m () | ||
| runGameSuccess = void $ EM.processEmulated $ do | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 G.startGame | ||
| _ <- EM.runWalletAction w2 G.startGame | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (G.lock "hello" 8) | ||
| processAndNotify | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (W.payToPublicKey_ W.defaultSlotRange G.gameTokenVal (EM.walletPubKey w2)) | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w2 (guess "hello" "new secret" 3 5) | ||
| processAndNotify | ||
| EM.assertOwnFundsEq w2 (initialVal <> Ada.adaValueOf 3 <> G.gameTokenVal) | ||
|
|
||
| -- Runs 'runGameSuccess', then wallet 2 transfers the token to wallet 1, which takes | ||
| -- out another couple of Ada. | ||
| runGameSuccess2 :: (EM.MonadEmulator m) => m () | ||
| runGameSuccess2 = do | ||
| runGameSuccess | ||
|
|
||
| void $ EM.processEmulated $ do | ||
| _ <- EM.runWalletAction w2 (W.payToPublicKey_ W.defaultSlotRange G.gameTokenVal (EM.walletPubKey w1)) | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (guess "new secret" "hello" 2 3) | ||
| processAndNotify | ||
| EM.assertOwnFundsEq w1 (Ada.adaValueOf 4 <> G.gameTokenVal) | ||
|
|
||
| -- Wallet 2 makes a wrong guess and fails to take out the funds | ||
| runGameFailure :: (EM.MonadEmulator m) => m () | ||
| runGameFailure = void $ EM.processEmulated $ do | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 G.startGame | ||
| _ <- EM.runWalletAction w2 G.startGame | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (G.lock "hello" 8) | ||
| processAndNotify | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w1 (W.payToPublicKey_ W.defaultSlotRange G.gameTokenVal (EM.walletPubKey w2)) | ||
| processAndNotify | ||
| _ <- EM.runWalletAction w2 (guess "hola" "new secret" 3 5) | ||
| processAndNotify | ||
| EM.assertOwnFundsEq w2 (initialVal <> G.gameTokenVal) | ||
|
|