Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
implements model based testing framework.
- duplicate types of many Ledger details, with no crypto details. - duplicate model implementation of ledger spec - add a class EraElaborator to apply era-agnostic blockchain model interactions to real ledger implementations - instance of EraElaborator for Alonzo as Shelley eras. - simple unit test which applies simple transactions using EraElaborator to any era. - model supports basic spending, multi-asset minting, delegation, rewards, and plutus scripts. - end-to-end generated model test, with basic shrinking.
- Loading branch information
1 parent
60e820d
commit a2ef27b
Showing
22 changed files
with
9,149 additions
and
7 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
6 changes: 6 additions & 0 deletions
6
eras/alonzo/test-suite/src/Test/Cardano/Ledger/Alonzo/Scripts.hs
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,19 +1,25 @@ | ||
| module Test.Cardano.Ledger.Alonzo.Scripts | ||
| ( alwaysSucceeds, | ||
| alwaysFails, | ||
| saltFunction, | ||
| ) | ||
| where | ||
|
|
||
| import Cardano.Ledger.Alonzo.Language (Language (..)) | ||
| import Cardano.Ledger.Alonzo.Scripts (Script (..)) | ||
| import Data.ByteString.Short (ShortByteString) | ||
| import Numeric.Natural (Natural) | ||
| import qualified Plutus.V1.Ledger.Examples as Plutus | ||
| ( alwaysFailingNAryFunction, | ||
| alwaysSucceedingNAryFunction, | ||
| saltFunction, | ||
| ) | ||
|
|
||
| alwaysSucceeds :: Language -> Natural -> Script era | ||
| alwaysSucceeds lang n = PlutusScript lang (Plutus.alwaysSucceedingNAryFunction n) | ||
|
|
||
| alwaysFails :: Language -> Natural -> Script era | ||
| alwaysFails lang n = PlutusScript lang (Plutus.alwaysFailingNAryFunction n) | ||
|
|
||
| saltFunction :: Language -> Integer -> ShortByteString -> Script era | ||
| saltFunction lang n ps = PlutusScript lang (Plutus.saltFunction n ps) |
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
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
125 changes: 125 additions & 0 deletions
125
libs/cardano-ledger-test/src/Data/Functor/PiecewiseConstant.hs
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,125 @@ | ||
| {-# LANGUAGE DeriveTraversable #-} | ||
| {-# LANGUAGE DerivingVia #-} | ||
| {-# LANGUAGE MultiParamTypeClasses #-} | ||
| {-# LANGUAGE RankNTypes #-} | ||
| {-# LANGUAGE StandaloneDeriving #-} | ||
|
|
||
| module Data.Functor.PiecewiseConstant where | ||
|
|
||
| import Control.Applicative (liftA2) | ||
| import Control.Lens.Fold (Fold, folding) | ||
| import Control.Lens.Indexed (FoldableWithIndex (..), FunctorWithIndex (..), TraversableWithIndex (..)) | ||
| import Data.Foldable (Foldable (..)) | ||
| import Data.Functor.Identity (Identity (..)) | ||
| import Data.Group | ||
| import Data.Map.Strict as Map | ||
| import Data.Monoid (Ap (..)) | ||
|
|
||
| data PieceInterval a = PieceInterval | ||
| { _pieceInterval_lowerBound :: Maybe a, | ||
| _pieceInterval_upperBound :: Maybe a | ||
| } | ||
| deriving (Eq, Ord, Show, Functor, Foldable, Traversable) | ||
|
|
||
| -- | a datatype which represents a finitely supported total function; consisting | ||
| -- of constant pieces of the form [lb,ub) | ||
| data PiecewiseConstantMap a b = MkPiecewiseConstantMap b (Map.Map a b) | ||
| deriving (Show, Functor, Foldable, Traversable) | ||
|
|
||
| deriving via | ||
| (Ap (PiecewiseConstantMap k) a) | ||
| instance | ||
| (Ord k, Semigroup a) => | ||
| Semigroup (PiecewiseConstantMap k a) | ||
|
|
||
| deriving via | ||
| (Ap (PiecewiseConstantMap k) a) | ||
| instance | ||
| (Ord k, Monoid a) => | ||
| Monoid (PiecewiseConstantMap k a) | ||
|
|
||
| instance (Ord k, Group a) => Group (PiecewiseConstantMap k a) where | ||
| invert = fmap invert | ||
| (~~) = liftA2 (~~) | ||
|
|
||
| instance (Ord k, Abelian a) => Abelian (PiecewiseConstantMap k a) | ||
|
|
||
| instance (Ord k, Eq a) => Eq (PiecewiseConstantMap k a) where | ||
| xs == ys = and $ liftA2 (==) xs ys | ||
|
|
||
| instance (Ord k, Ord a) => Ord (PiecewiseConstantMap k a) where | ||
| compare xs ys = fold $ liftA2 compare xs ys | ||
|
|
||
| instance Ord k => Applicative (PiecewiseConstantMap k) where | ||
| (<*>) = liftA2 id | ||
| {-# INLINE (<*>) #-} | ||
| pure x = MkPiecewiseConstantMap x Map.empty | ||
| liftA2 f = \(MkPiecewiseConstantMap a0 as0) (MkPiecewiseConstantMap b0 bs0) -> | ||
| MkPiecewiseConstantMap (f a0 b0) $ Map.fromAscList $ go a0 b0 (Map.toAscList as0) (Map.toAscList bs0) | ||
| where | ||
| go _ _ [] [] = [] | ||
| go _ b as@(_ : _) [] = (fmap . fmap) (flip f b) as | ||
| go a _ [] bs@(_ : _) = (fmap . fmap) (f a) bs | ||
| go a b as@((ak, av) : aRest) bs@((bk, bv) : bRest) = case compare ak bk of | ||
| LT -> (ak, f av b) : go av b aRest bs | ||
| EQ -> (ak, f av bv) : go av bv aRest bRest | ||
| GT -> (bk, f a bv) : go a bv as bRest | ||
| {-# INLINE liftA2 #-} | ||
|
|
||
| -- | Piecewise constant maps do not form a category; consider `id :: PiecewiseConstantMap Rational Rational` cannot be finitely supported. | ||
| composePiecewiseConstantMap :: | ||
| Ord b => | ||
| PiecewiseConstantMap b c -> | ||
| PiecewiseConstantMap a b -> | ||
| PiecewiseConstantMap a c | ||
| composePiecewiseConstantMap = fmap . liftPiecewiseConstantMap | ||
|
|
||
| liftPiecewiseConstantMap :: Ord a => PiecewiseConstantMap a b -> a -> b | ||
| liftPiecewiseConstantMap (MkPiecewiseConstantMap x xs) = maybe x snd . flip Map.lookupLE xs | ||
|
|
||
| -- it's not quite possible to have a pointwise lens in a piecewise constant map | ||
| -- because the pieces can't be "thin" enough without something like Enum; | ||
| ixPiecewiseConstantMap :: | ||
| forall k a. Ord k => k -> Fold (PiecewiseConstantMap k a) a | ||
| ixPiecewiseConstantMap k = folding (\s -> Identity $ liftPiecewiseConstantMap s k) | ||
| {-# INLINE ixPiecewiseConstantMap #-} | ||
|
|
||
| -- combine two PiecewiseConstantMaps such that the range matches the first map | ||
| -- for the part of it's domain < k, and the second for parts >= k | ||
| splicePiecewiseConstantMap :: | ||
| Ord k => | ||
| k -> | ||
| PiecewiseConstantMap k a -> | ||
| PiecewiseConstantMap k a -> | ||
| PiecewiseConstantMap k a | ||
| splicePiecewiseConstantMap k (MkPiecewiseConstantMap x xs) y@(MkPiecewiseConstantMap _ ys) = | ||
| MkPiecewiseConstantMap x (Map.unions [lower, middle, upper]) | ||
| where | ||
| (lower, _) = Map.split k xs | ||
| (_, upper) = Map.split k ys | ||
| middle = Map.singleton k $ liftPiecewiseConstantMap y k | ||
|
|
||
| instance Ord k => Monad (PiecewiseConstantMap k) where | ||
| MkPiecewiseConstantMap x0 xs >>= f = | ||
| ifoldl | ||
| (\k ys x -> splicePiecewiseConstantMap k ys $ f x) | ||
| (f x0) | ||
| xs | ||
|
|
||
| instance Ord k => FunctorWithIndex (PieceInterval k) (PiecewiseConstantMap k) | ||
|
|
||
| instance Ord k => FoldableWithIndex (PieceInterval k) (PiecewiseConstantMap k) where | ||
| ifoldMap f (MkPiecewiseConstantMap x0 xs) = case Map.toAscList xs of | ||
| [] -> f (PieceInterval Nothing Nothing) x0 | ||
| ((k, x') : ks) -> f (PieceInterval Nothing (Just k)) x0 <> go k x' ks | ||
| where | ||
| go k x [] = f (PieceInterval (Just k) Nothing) x | ||
| go k x ((k', x') : rest) = f (PieceInterval (Just k) (Just k')) x <> go k' x' rest | ||
|
|
||
| instance Ord k => TraversableWithIndex (PieceInterval k) (PiecewiseConstantMap k) where | ||
| itraverse f (MkPiecewiseConstantMap x0 xs) = case Map.toAscList xs of | ||
| [] -> MkPiecewiseConstantMap <$> f (PieceInterval Nothing Nothing) x0 <*> pure Map.empty | ||
| ((k, x') : ks) -> MkPiecewiseConstantMap <$> f (PieceInterval Nothing (Just k)) x0 <*> (Map.fromAscList <$> go k x' ks) | ||
| where | ||
| go k x [] = (\y -> [(k, y)]) <$> f (PieceInterval (Just k) Nothing) x | ||
| go k x ((k', x') : rest) = (:) <$> fmap ((,) k) (f (PieceInterval (Just k) (Just k')) x) <*> go k' x' rest |
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,112 @@ | ||
| {-# LANGUAGE DataKinds #-} | ||
| {-# LANGUAGE DeriveFoldable #-} | ||
| {-# LANGUAGE DeriveGeneric #-} | ||
| {-# LANGUAGE FlexibleInstances #-} | ||
| {-# LANGUAGE MultiParamTypeClasses #-} | ||
| {-# LANGUAGE RankNTypes #-} | ||
| {-# LANGUAGE UndecidableInstances #-} | ||
|
|
||
| module Data.Group.GrpMap where | ||
|
|
||
| import Control.DeepSeq (NFData) | ||
| import Control.Lens (Iso', Lens', at, iso, set) | ||
| import Control.Lens.Indexed (FoldableWithIndex (..)) | ||
| import Control.Monad (guard) | ||
| import Data.Functor.Const (Const (..)) | ||
| import Data.Group (Abelian, Group (..)) | ||
| import qualified Data.Map as Map | ||
| import qualified Data.Map.Merge.Lazy as MapLazy | ||
| import qualified Data.Map.Merge.Strict as Map | ||
| import Data.Monoid (All (..)) | ||
| import qualified Data.Set as Set | ||
| import GHC.Generics (Generic) | ||
| import qualified GHC.TypeLits as GHC | ||
|
|
||
| -- TODO: groups/monoidal-containers/some other place? | ||
| newtype GrpMap k v = GrpMap {unGrpMap :: Map.Map k v} | ||
| deriving (Foldable, Eq, Ord, Show, Generic) | ||
|
|
||
| instance (NFData k, NFData v) => NFData (GrpMap k v) | ||
|
|
||
| restrictKeysGrpMap :: Ord k => GrpMap k a -> Set.Set k -> GrpMap k a | ||
| restrictKeysGrpMap (GrpMap xs) = GrpMap . Map.restrictKeys xs | ||
|
|
||
| grpMapSingleton :: (Eq v, Monoid v) => k -> v -> GrpMap k v | ||
| grpMapSingleton k v | ||
| | v == mempty = GrpMap Map.empty | ||
| | otherwise = GrpMap $ Map.singleton k v | ||
|
|
||
| mkGrpMap :: (Eq v, Monoid v) => Map.Map k v -> GrpMap k v | ||
| mkGrpMap = GrpMap . Map.filter (mempty /=) | ||
|
|
||
| _GrpMap :: (Eq a, Monoid a) => Iso' (GrpMap k a) (Map.Map k a) | ||
| _GrpMap = iso unGrpMap mkGrpMap | ||
|
|
||
| grpMap :: (Ord k, Eq a, Monoid a) => k -> Lens' (GrpMap k a) a | ||
| grpMap k a2fb (GrpMap s) = (\y -> GrpMap $ set (at k) (y <$ guard (y /= mempty)) s) <$> a2fb (maybe mempty id $ Map.lookup k s) | ||
|
|
||
| instance GHC.TypeError ('GHC.Text "GrpMap is not a Functor, use mapGrpMap") => Functor (GrpMap k) where | ||
| fmap = error "GrpMap is not a Functor, use mapGrpMap" | ||
|
|
||
| instance GHC.TypeError ('GHC.Text "GrpMap is not a Functor, use mapGrpMap") => Traversable (GrpMap k) where | ||
| traverse = error "GrpMap is not Traversable, use traverseGrpMap" | ||
|
|
||
| mapGrpMap :: (Eq b, Monoid b) => (a -> b) -> GrpMap k a -> GrpMap k b | ||
| mapGrpMap f = GrpMap . Map.mapMaybe f' . unGrpMap | ||
| where | ||
| f' x = let y = f x in y <$ guard (y /= mempty) | ||
| {-# INLINE mapGrpMap #-} | ||
|
|
||
| zipWithGrpMap :: (Ord k, Eq c, Monoid a, Monoid b, Monoid c) => (a -> b -> c) -> GrpMap k a -> GrpMap k b -> GrpMap k c | ||
| zipWithGrpMap f = \(GrpMap xs) (GrpMap ys) -> | ||
| GrpMap $ | ||
| Map.merge | ||
| (Map.mapMaybeMissing $ \_ x -> f' x mempty) | ||
| (Map.mapMaybeMissing $ \_ y -> f' mempty y) | ||
| (Map.zipWithMaybeMatched $ \_ -> f') | ||
| xs | ||
| ys | ||
| where | ||
| f' x y = let z = f x y in z <$ guard (z /= mempty) | ||
| {-# INLINE zipWithGrpMap #-} | ||
|
|
||
| -- | laws: traverseGrpMap (f . const mempty) xs === pure mempty | ||
| traverseGrpMap :: (Eq b, Monoid b, Applicative m) => (a -> m b) -> GrpMap k a -> m (GrpMap k b) | ||
| traverseGrpMap f = fmap GrpMap . Map.traverseMaybeWithKey f' . unGrpMap | ||
| where | ||
| f' _ x = (\y -> y <$ guard (y /= mempty)) <$> f x | ||
| {-# INLINE traverseGrpMap #-} | ||
|
|
||
| instance FoldableWithIndex k (GrpMap k) where | ||
| ifoldMap f = ifoldMap f . unGrpMap | ||
|
|
||
| instance (Ord k, Eq v, Monoid v) => Semigroup (GrpMap k v) where | ||
| GrpMap xs <> GrpMap ys = GrpMap $ Map.merge Map.preserveMissing Map.preserveMissing (Map.zipWithMaybeMatched f) xs ys | ||
| where | ||
| f _ x y = let z = x <> y in z <$ guard (z /= mempty) | ||
| {-# INLINE (<>) #-} | ||
|
|
||
| instance (Ord k, Eq v, Monoid v) => Monoid (GrpMap k v) where | ||
| mempty = GrpMap Map.empty | ||
| {-# INLINE mempty #-} | ||
|
|
||
| instance (Ord k, Eq v, Group v) => Group (GrpMap k v) where | ||
| invert = GrpMap . fmap invert . unGrpMap | ||
| {-# INLINE invert #-} | ||
| GrpMap xs ~~ GrpMap ys = GrpMap $ Map.merge Map.preserveMissing (Map.mapMissing $ const invert) (Map.zipWithMaybeMatched f) xs ys | ||
| where | ||
| f _ x y = let z = x ~~ y in z <$ guard (z /= mempty) | ||
| {-# INLINE (~~) #-} | ||
|
|
||
| instance (Ord k, Eq v, Abelian v) => Abelian (GrpMap k v) | ||
|
|
||
| pointWise' :: Ord k => v -> (v -> v -> Bool) -> Map.Map k v -> Map.Map k v -> Bool | ||
| pointWise' z p = \xs ys -> | ||
| getAll $! getConst $ | ||
| MapLazy.mergeA | ||
| (MapLazy.traverseMissing $ \_ x -> Const $ All $ p x z) | ||
| (MapLazy.traverseMissing $ \_ y -> Const $ All $ p z y) | ||
| (MapLazy.zipWithAMatched $ \_ x y -> Const $ All $ p x y) | ||
| xs | ||
| ys | ||
| {-# INLINE pointWise' #-} |
Oops, something went wrong.