Skip to content
This repository has been archived by the owner on Dec 2, 2024. It is now read-only.

Commit

Permalink
ContractModel: Report symbolic values as their symbolic names (#452)
Browse files Browse the repository at this point in the history
* Report symbolic values as their symbolic names

* fix build issue in tutorial

* update golden test

* wip

* fix build issues

* dependencies

* update golden test

* wip
  • Loading branch information
MaximilianAlgehed authored May 31, 2022
1 parent 7d3e7b0 commit 83594e4
Show file tree
Hide file tree
Showing 7 changed files with 39 additions and 15 deletions.
2 changes: 1 addition & 1 deletion doc/plutus/tutorials/Escrow6.hs
Original file line number Diff line number Diff line change
Expand Up @@ -275,6 +275,6 @@ prop_CrashTolerance = CM.propRunActions_

check_propEscrowWithCoverage :: IO ()
check_propEscrowWithCoverage = do
cr <- CM.quickCheckWithCoverage stdArgs (set coverageIndex covIdx defaultCoverageOptions) $ \covopts ->
cr <- CM.quickCheckWithCoverage stdArgs (set coverageIndex covIdx $ defaultCoverageOptions) $ \covopts ->
withMaxSuccess 1000 $ CM.propRunActionsWithOptions @EscrowModel CM.defaultCheckOptionsContractModel covopts (const (pure True))
writeCoverageReport "Escrow" covIdx cr
Original file line number Diff line number Diff line change
Expand Up @@ -1620,18 +1620,24 @@ checkBalances s envOuter = Map.foldrWithKey (\ w sval p -> walletFundsChange w s
lookup st = case lookupMaybe st of
Nothing -> error $ "Trying to look up unknown symbolic token: " ++ show st ++ ",\nare you using a custom implementation of getAllSymtokens? If not, please report this as a bug."
Just tok -> tok
invert m = Map.fromList [(v, k) | (k, v) <- Map.toList m]
invLookup ac = do
(innerVar, idx) <- listToMaybe [ (innerVar, idx) | (innerVar, tm) <- Map.toList envInner
, idx <- maybeToList $ Map.lookup ac (invert tm) ]
outerVar <- invertLookupVarMaybe envOuter innerVar
return (SymToken outerVar idx)
dlt = toValue lookup sval
initialValue = fold (dist ^. at w)
finalValue = finalValue' P.+ fees
result = initialValue P.+ dlt == finalValue
unless result $ do
tell @(Doc Void) $ vsep $
[ "Expected funds of" <+> pretty w <+> "to change by"
, " " <+> viaShow dlt] ++
, " " <+> viaShow sval] ++
if initialValue == finalValue
then ["but they did not change"]
else ["but they changed by", " " <+> viaShow (finalValue P.- initialValue),
"a discrepancy of", " " <+> viaShow (finalValue P.- initialValue P.- dlt)]
else ["but they changed by", " " <+> viaShow (toSymVal invLookup (finalValue P.- initialValue)),
"a discrepancy of", " " <+> viaShow (toSymVal invLookup (finalValue P.- initialValue P.- dlt))]
pure result
_ -> error "I am the pope"

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,14 +3,15 @@
module Plutus.Contract.Test.ContractModel.Symbolics where

import Ledger.Ada qualified as Ada
import Ledger.Value (AssetClass, Value, assetClassValue, assetClassValueOf, isZero, leq)
import Ledger.Value (AssetClass, Value, assetClass, assetClassValue, assetClassValueOf, flattenValue, isZero, leq)
import PlutusTx.Monoid qualified as PlutusTx

import Data.Aeson qualified as JSON
import Data.Data
import Data.Foldable
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe

import Test.QuickCheck.StateModel hiding (Action, Actions, arbitraryAction, initialState, monitoring, nextState,
perform, precondition, shrinkAction, stateAfter)
Expand Down Expand Up @@ -60,6 +61,14 @@ symLeq (SymValue m v) (SymValue m' v') = v `leq` v' && all (<=0) (Map.unionWith
toValue :: (SymToken -> AssetClass) -> SymValue -> Value
toValue symTokenMap (SymValue m v) = v <> fold [ assetClassValue (symTokenMap t) v | (t, v) <- Map.toList m ]

-- | Invert a sym token mapping to turn a Value into a SymValue,
-- useful for error reporting
toSymVal :: (AssetClass -> Maybe SymToken) -> Value -> SymValue
toSymVal invSymTokenMap v =
let acMap = [ (assetClass cs tn, i) | (cs, tn, i) <- flattenValue v ]
in SymValue (Map.fromList [ (tn, i) | (ac, i) <- acMap, tn <- maybeToList $ invSymTokenMap ac ])
(fold [ assetClassValue ac i | (ac, i) <- acMap, invSymTokenMap ac == Nothing ])

-- Negate a symbolic value
inv :: SymValue -> SymValue
inv (SymValue m v) = SymValue (negate <$> m) (PlutusTx.inv v)
Expand Down
9 changes: 4 additions & 5 deletions plutus-use-cases/plutus-use-cases.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -75,9 +75,9 @@ library
aeson -any,
bytestring -any,
containers -any,
mtl -any,
plutus-core -any,
plutus-tx -any,
plutus-tx-plugin -any,
plutus-contract -any,
playground-common -any,
plutus-ledger -any,
Expand All @@ -90,11 +90,10 @@ library
prettyprinter -any,
hashable -any,
freer-simple -any,
streaming -any,
semigroups -any,
openapi3 -any

if !(impl(ghcjs) || os(ghcjs))
build-depends: plutus-tx-plugin -any
openapi3 -any,
freer-simple -any

if flag(defer-plugin-errors)
ghc-options: -fplugin-opt PlutusTx.Plugin:defer-errors
Expand Down
1 change: 1 addition & 0 deletions plutus-use-cases/src/Plutus/Contracts/GameStateMachine.hs
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ import Schema (ToSchema)

import Prelude qualified as Haskell


-- | Datatype for creating a parameterized validator.
data GameParam = GameParam
{ gameParamPayeePkh :: PaymentPubKeyHash
Expand Down
8 changes: 4 additions & 4 deletions plutus-use-cases/test/Spec/renderGuess.txt
Original file line number Diff line number Diff line change
Expand Up @@ -551,11 +551,11 @@ Balances Carried Forward:
Ada: Lovelace: 100000000

==== Slot #1, Tx #0 ====
TxId: 3b5055fc43eede4efa1fbe02a510c23419a1948d57451062ffd698412ba37f0e
TxId: 04dadac1ad0b6c9219817d0c888eec56e71b015925e13ea76c525743f8f4afb3
Fee: Ada: Lovelace: 184113
Mint: -
Signatures PubKey: 8d9de88fbf445b7f6c3875a14daba94caee2ffcb...
Signature: 5840804ad7b98709bf0e5a6453486b8887016b36...
Signature: 58404c181715d32388b97a7b52b0997db73da31e...
Inputs:
---- Input 0 ----
Destination: PaymentPubKeyHash: a2c20c77887ace1cd986193e4e75babd8993cfd5... (Wallet 872cb83b5ee40eb23bfdab1772660c822a48d491)
Expand All @@ -578,7 +578,7 @@ Inputs:

Outputs:
---- Output 0 ----
Destination: Script: 4ff3210533e97f6593da228013279795e2819f16dd48ed5a1739975a
Destination: Script: 9593e0301beb5d51bc3cc3a3603a8fd20d5d0f845ea612709c1e1eb3
Value:
Ada: Lovelace: 8000000

Expand Down Expand Up @@ -629,6 +629,6 @@ Balances Carried Forward:
Value:
Ada: Lovelace: 100000000

Script: 4ff3210533e97f6593da228013279795e2819f16dd48ed5a1739975a
Script: 9593e0301beb5d51bc3cc3a3603a8fd20d5d0f845ea612709c1e1eb3
Value:
Ada: Lovelace: 8000000
11 changes: 10 additions & 1 deletion quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,8 @@ module Test.QuickCheck.StateModel(
, runActionsInState
, lookUpVar
, lookUpVarMaybe
) where
, invertLookupVarMaybe
) where

import Control.Monad

Expand Down Expand Up @@ -79,11 +80,19 @@ lookUpVarMaybe ((v' :== a) : env) v =
case cast (v',a) of
Just (v'',a') | v==v'' -> Just a'
_ -> lookUpVarMaybe env v

lookUpVar :: Typeable a => Env -> Var a -> a
lookUpVar env v = case lookUpVarMaybe env v of
Nothing -> error $ "Variable "++show v++" is not bound!"
Just a -> a

invertLookupVarMaybe :: (Typeable a, Eq a) => Env -> a -> Maybe (Var a)
invertLookupVarMaybe [] _ = Nothing
invertLookupVarMaybe ((v :== a) : env) a' =
case cast (v, a) of
Just (v', a'') | a' == a'' -> Just v'
_ -> invertLookupVarMaybe env a'

data Any f where
Some :: (Show a, Typeable a, Eq (f a)) => f a -> Any f
Error :: String -> Any f
Expand Down

0 comments on commit 83594e4

Please sign in to comment.