Safe Haskell	None
Language	Haskell2010

Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

Contents

Orphan instances

Description

Please read the source code to view the tests.

Synopsis

newtype ValidTx r d v = ValidTx (Transaction r d v)
fromValidTx :: ValidTx r d v -> Transaction r d v
newtype SmallChunk r d v = SmallChunk (Chunk r d v)
class Validator r d v => Fixable r d v | v -> r d where
- fixOutput :: Context r d v -> Output d v -> Output d v
fixChunkToBlockchain :: (Arbitrary d, Arbitrary v, Fixable r d v) => Chunk r d v -> Gen (Blockchain r d v)
type TR = Int
type TD = Int
type TV = ValFin TR TD
type TC = Chunk TR TD TV
type SmallTC = SmallChunk TR TD TV
type TB = Blockchain TR TD TV
type TX = ValidTx TR TD TV
type TC' v = Chunk TR TD v
atValTriv :: Proxy (ValTriv TR TD)
atValFin :: Proxy (ValFin TR TD)
type CVal v = (Typeable v, Show v, Arbitrary v, UnifyPerm v, Validator TR TD v)
data ValProxy where
- ValProxy :: CVal v => Proxy v -> ValProxy
valTriv :: ValProxy
valFin :: ValProxy
withVal :: (forall v proxy. CVal v => proxy v -> a) -> ValProxy -> a
prop_arbitraryChunkIsValid :: TC -> Bool
prop_arbitraryChunkIsValid' :: TC -> Bool
prop_arbitraryChunkEqCheck :: TC -> Bool
prop_notEveryChunkBlockchain :: TC -> Property
prop_arbitraryTxIsValid :: TX -> Bool
prop_arbitraryBlockchainIsValid :: TB -> Bool
prop_blockchainToChunkAndBack :: TB -> Bool
prop_blockchainHasNoUTxIs :: TB -> Bool
prop_chunkrefl :: CVal v => proxy v -> TC' v -> Bool
prop_chunkneq :: TC -> TC -> Property
prop_emptyIsPrefix :: TC -> Bool
prop_chunkTail_is_chunk :: TC -> Property
prop_chunkTail_is_prefix :: TC -> Property
genChunkTail :: (UnifyPerm r, UnifyPerm d, UnifyPerm v, Validator r d v) => Chunk r d v -> Maybe (Chunk r d v)
prop_chunkTail_is_prefix_gotcha :: TC -> Property
prop_warningNotChunkTail_is_not_chunk :: TC -> Property
prop_underbinding :: TC -> Property
prop_overbinding :: TC -> Property
prop_chunkHead_chunkTail_recombine :: TC -> Property
prop_chunkHdTl_recombine :: TC -> Property
prop_reverseIsNotValid :: TC -> Property
prop_subchunksValid :: SmallChunk TR TD TV -> Bool
prop_apart_is_valid_tx :: TX -> TX -> Bool
prop_apart_is_valid_ch :: TC -> TC -> Bool
observe :: Maybe TC -> Maybe TC -> Maybe TC -> Bool
prop_chunk_apart_commutes :: SmallTC -> SmallTC -> SmallTC -> Bool
prop_validity_fresh :: TC -> Property

Documentation

newtype ValidTx r d v Source #

Constructors

ValidTx (Transaction r d v)

Instances

(Show r, Show d, Show v) => Show (ValidTx r d v) Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Methods showsPrec :: Int -> ValidTx r d v -> ShowS # show :: ValidTx r d v -> String # showList :: [ValidTx r d v] -> ShowS #
Generic (ValidTx r d v) Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Associated Types type Rep (ValidTx r d v) :: Type -> Type # Methods from :: ValidTx r d v -> Rep (ValidTx r d v) x # to :: Rep (ValidTx r d v) x -> ValidTx r d v #
(Arbitrary r, Arbitrary d, Arbitrary v) => Arbitrary (ValidTx r d v) Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Methods arbitrary :: Gen (ValidTx r d v) # shrink :: ValidTx r d v -> [ValidTx r d v] #
type Rep (ValidTx r d v) Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec type Rep (ValidTx r d v) = D1 (MetaData "ValidTx" "Language.Nominal.Properties.Examples.IdealisedEUTxOSpec" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" True) (C1 (MetaCons "ValidTx" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Transaction r d v))))

fromValidTx :: ValidTx r d v -> Transaction r d v Source #

newtype SmallChunk r d v Source #

Constructors

SmallChunk (Chunk r d v)

Instances

(Show r, Show d, Show v) => Show (SmallChunk r d v) Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Methods showsPrec :: Int -> SmallChunk r d v -> ShowS # show :: SmallChunk r d v -> String # showList :: [SmallChunk r d v] -> ShowS #
Arbitrary (Chunk r d v) => Arbitrary (SmallChunk r d v) Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Methods arbitrary :: Gen (SmallChunk r d v) # shrink :: SmallChunk r d v -> [SmallChunk r d v] #

class Validator r d v => Fixable r d v | v -> r d where Source #

Methods

fixOutput :: Context r d v -> Output d v -> Output d v Source #

Takes a context and an output and modifies the output such that it can be consumed by the context.

Instances

(Support r, Support d) => Fixable r d (ValTriv r d) Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Methods fixOutput :: Context r d (ValTriv r d) -> Output d (ValTriv r d) -> Output d (ValTriv r d) Source #
(Eq r, UnifyPerm r, Eq d, UnifyPerm d) => Fixable r d (ValFin r d) Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Methods fixOutput :: Context r d (ValFin r d) -> Output d (ValFin r d) -> Output d (ValFin r d) Source #
(Support r, Support d) => Fixable r d (Val r d) Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Methods fixOutput :: Context r d (Val r d) -> Output d (Val r d) -> Output d (Val r d) Source #

fixChunkToBlockchain :: (Arbitrary d, Arbitrary v, Fixable r d v) => Chunk r d v -> Gen (Blockchain r d v) Source #

type TR = Int Source #

type TD = Int Source #

type TV = ValFin TR TD Source #

type TC = Chunk TR TD TV Source #

type SmallTC = SmallChunk TR TD TV Source #

type TB = Blockchain TR TD TV Source #

type TX = ValidTx TR TD TV Source #

type TC' v = Chunk TR TD v Source #

atValTriv :: Proxy (ValTriv TR TD) Source #

atValFin :: Proxy (ValFin TR TD) Source #

type CVal v = (Typeable v, Show v, Arbitrary v, UnifyPerm v, Validator TR TD v) Source #

data ValProxy where Source #

Constructors

ValProxy :: CVal v => Proxy v -> ValProxy

Instances

Show ValProxy Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Methods showsPrec :: Int -> ValProxy -> ShowS # show :: ValProxy -> String # showList :: [ValProxy] -> ShowS #
Arbitrary ValProxy Source #
Instance details Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec Methods arbitrary :: Gen ValProxy # shrink :: ValProxy -> [ValProxy] #

valTriv :: ValProxy Source #

valFin :: ValProxy Source #

withVal :: (forall v proxy. CVal v => proxy v -> a) -> ValProxy -> a Source #

prop_arbitraryChunkIsValid :: TC -> Bool Source #

Sanity check: every arbitrary chunk is indeed a valid chunk.

prop_arbitraryChunkIsValid' :: TC -> Bool Source #

Sanity check: every arbitrary chunk is indeed a valid chunk (alternate test).

prop_arbitraryChunkEqCheck :: TC -> Bool Source #

Sanity check: every arbitrary chunk is equal to itself (not trivial because Eq instance is nontrivial)

prop_notEveryChunkBlockchain :: TC -> Property Source #

Sanity check: not every chunk is a blockchain (might have UTxIs)!

prop_arbitraryTxIsValid :: TX -> Bool Source #

Sanity check: an arbitrary transaction is indeed a valid transaction.

prop_arbitraryBlockchainIsValid :: TB -> Bool Source #

Sanity check: an arbitrary blockchain is indeed a valid blockchain.

prop_blockchainToChunkAndBack :: TB -> Bool Source #

Sanity check: arbitrary instance of TB generates a blockchain, which is equal to itself.

unifiablePerm must be used here, because of the local scope.

prop_blockchainHasNoUTxIs :: TB -> Bool Source #

Blockchain has no UTxIs

prop_chunkrefl :: CVal v => proxy v -> TC' v -> Bool Source #

Chunk is equal to itself

prop_chunkneq :: TC -> TC -> Property Source #

There are two different chunks

prop_emptyIsPrefix :: TC -> Bool Source #

Empty chunk is prefix of any chunk

prop_chunkTail_is_chunk :: TC -> Property Source #

The tail of a chunk, is a chunk.

prop_chunkTail_is_prefix :: TC -> Property Source #

The tail of a chunk, is a prefix of the original chunk.

genChunkTail :: (UnifyPerm r, UnifyPerm d, UnifyPerm v, Validator r d v) => Chunk r d v -> Maybe (Chunk r d v) Source #

The tail of a chunk, generating fresh atoms if required

prop_chunkTail_is_prefix_gotcha :: TC -> Property Source #

The tail of a chunk, is a prefix of the original chunk. Gotcha version, that doesn't have the Nom bindings: expect failure here.

prop_warningNotChunkTail_is_not_chunk :: TC -> Property Source #

Plausible-but-wrong warningNotChunkTail is wrong: expect failure here.

prop_underbinding :: TC -> Property Source #

Underbinding is when not enough atoms are bound in a chunk

prop_overbinding :: TC -> Property Source #

Overbinding is when too many atoms are bound in a chunk

prop_chunkHead_chunkTail_recombine :: TC -> Property Source #

Gotcha: Fails because loss of information from two Nom bindings.

prop_chunkHdTl_recombine :: TC -> Property Source #

Succeeds because one Nom binding thus no loss of information.

prop_reverseIsNotValid :: TC -> Property Source #

If you reverse the order of transactions in a chunk, it need not be valid

prop_subchunksValid :: SmallChunk TR TD TV -> Bool Source #

prop_apart_is_valid_tx :: TX -> TX -> Bool Source #

If two transactions are apart, they can be validly combined. | Corresponds to Lemma 2.14(1) of UTxO- vs account-based smart contractblockchain programming paradigms.

prop_apart_is_valid_ch :: TC -> TC -> Bool Source #

If two chunks are apart, they can be validly combined. | Extends Lemma 2.14(1) of UTxO- vs account-based smart contractblockchain programming paradigms.

observe :: Maybe TC -> Maybe TC -> Maybe TC -> Bool Source #

prop_chunk_apart_commutes :: SmallTC -> SmallTC -> SmallTC -> Bool Source #

If two chunks are apart, they can be validly commuted. | Extends Lemma 2.14(1) of UTxO- vs account-based smart contractblockchain programming paradigms. We use smaller chunks for speed.

prop_validity_fresh :: TC -> Property Source #

This corresponds to a key result, Lemma 2.14(2) of UTxO- vs account-based smart contractblockchain programming paradigms.

Orphan instances

Arbitrary r => Arbitrary (Input r) Source #
Instance details Methods arbitrary :: Gen (Input r) # shrink :: Input r -> [Input r] #
(Eq r, UnifyPerm r, Arbitrary r, Eq d, UnifyPerm d, Arbitrary d) => Arbitrary (ValFin r d) Source #
Instance details Methods arbitrary :: Gen (ValFin r d) # shrink :: ValFin r d -> [ValFin r d] #
Arbitrary (ValTriv r d) Source #
Instance details Methods arbitrary :: Gen (ValTriv r d) # shrink :: ValTriv r d -> [ValTriv r d] #
(Arbitrary d, Arbitrary v) => Arbitrary (Output d v) Source #
Instance details Methods arbitrary :: Gen (Output d v) # shrink :: Output d v -> [Output d v] #
(Arbitrary r, Support r, Arbitrary d, Support d, Arbitrary v, Fixable r d v) => Arbitrary (Blockchain r d v) Source #
Instance details Methods arbitrary :: Gen (Blockchain r d v) # shrink :: Blockchain r d v -> [Blockchain r d v] #
(Arbitrary r, Support r, Arbitrary d, Support d, Arbitrary v, Validator r d v) => Arbitrary (Chunk r d v) Source #
Instance details Methods arbitrary :: Gen (Chunk r d v) # shrink :: Chunk r d v -> [Chunk r d v] #
(Arbitrary r, Arbitrary d, Arbitrary v) => Arbitrary (Context r d v) Source #
Instance details Methods arbitrary :: Gen (Context r d v) # shrink :: Context r d v -> [Context r d v] #
(Arbitrary r, Arbitrary d, Arbitrary v) => Arbitrary (Transaction r d v) Source #
Instance details Methods arbitrary :: Gen (Transaction r d v) # shrink :: Transaction r d v -> [Transaction r d v] #