nom-0.1.0.2: Name-binding & alpha-equivalence

Safe HaskellNone
LanguageHaskell2010

Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

Contents

Description

Please read the source code to view the tests.

Synopsis

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.2-Cei0dwnsIrWHLKrPA11A4S" True) (C1 (MetaCons "ValidTx" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Transaction r d v))))

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 #

type TR = Int Source #

type TD = Int Source #

type TC' v = Chunk TR TD v 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_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.

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.

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] #