Language.Nominal.Examples.IdealisedEUTxO

Haskell rendering of the mathematical idealisation of the Extended UTxO model.

Types for inputs, outputs, and transaction lists

These are the basic types of our development.

• A Position is just an KAtom (a unique identifier). It identifies a location on the blockchain.
• Inputs point backwards towards outputs. Inputs and outputs identify one another by position.
• Outputs point wait for future inputs to point to them by naming the position they carry. Outputs carry validators, to check whether they like any input that tries to point to them.
• A TransactionF is a list of inputs (pointing backwards) and a list of outputs (pointing forwards).
• A Context is a transaction with a distinguished designated input, i.e. an input-in-context. In fact, outputs validate contexts; this is what makes it EUTxO, for Extended UTxO, instead of just UTxO.
• We also introduce the notion of Chunk, which is a valid list of transactions under a name-binding, and a notion of UTxI, meaning an input that does not refer to a preceding output in its chunk.
• A Blockchain is then a Chunk with no UTxIs. The benefit of working with Chunks as primitive is that valid Chunks form a monoid and are down-closed under taking sublists.

These are all novel observations which are original to this development and the associated paper(s). Then mathematically, the types below solve and make operational the following equations, parameterised over types r and d of redeemers and data:

Input       =  Position x r 
Output      =  d x Validator
Transaction =  Input-list x Output-list
Context     =  Input-nonempty-list x Output-list
Validator   (d x Context) - Bool -- Val and ValFin are 
                                 -- two solutions to this subset inclusion

More exposition follows in the code. See also the tests in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec:

type Position = Atom

Positions are atoms. These identify locations in a Chunk or Blockchain.

data Input r

An input has a position and a redeemer r. Think of the redeemer is a key which we use to unlock access to whatever output this input wants to connect to.

Here r is a type parameter, to be instantiated later.

Constructors

Input Position r

Instances

Support r => KSupport Tom (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Input r -> Set (KAtom Tom)

UnifyPerm r => KUnifyPerm Tom (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Input r -> Input r -> KRen Tom

ren :: KRen Tom -> Input r -> Input r

Eq r => Eq (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(==) :: Input r -> Input r -> Bool

(/=) :: Input r -> Input r -> Bool

Ord r => Ord (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

compare :: Input r -> Input r -> Ordering

(<) :: Input r -> Input r -> Bool

(<=) :: Input r -> Input r -> Bool

(>) :: Input r -> Input r -> Bool

(>=) :: Input r -> Input r -> Bool

max :: Input r -> Input r -> Input r

min :: Input r -> Input r -> Input r

Show r => Show (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

showsPrec :: Int -> Input r -> ShowS

show :: Input r -> String

showList :: [Input r] -> ShowS

Generic (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Associated Types

type Rep (Input r) :: Type -> Type

Methods

from :: Input r -> Rep (Input r) x

to :: Rep (Input r) x -> Input r

Arbitrary r => Arbitrary (Input r)

Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

Methods

arbitrary :: Gen (Input r)

shrink :: Input r -> [Input r]

Swappable r => Swappable (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Input r -> Input r

Eq r => IEq (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

iEq :: Input r -> Input r -> IO Bool

HasOutputPositions (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: Input r -> [Position]

HasInputPositions (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

inputPositions :: Input r -> [Position]

type Rep (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

type Rep (Input r) = D1 (MetaData "Input" "Language.Nominal.Examples.IdealisedEUTxO" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" False) (C1 (MetaCons "Input" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Position) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 r)))

data Output d v

An output has a position, a datum d, and a validator v.

• Think of the datum as a fragment of state data which is attached to this output.
• Think of the validator as a machine which, if given a suitable redeemer (along with other stuff), with authorise or forbid access to this output.

d and v are type parameters, to be instantiated later.

Constructors

Output Position d v

Instances

(Support d, Support v) => KSupport Tom (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Output d v -> Set (KAtom Tom)

(UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Output d v -> Output d v -> KRen Tom

ren :: KRen Tom -> Output d v -> Output d v

(Eq d, Eq v) => Eq (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(==) :: Output d v -> Output d v -> Bool

(/=) :: Output d v -> Output d v -> Bool

(Ord d, Ord v) => Ord (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

compare :: Output d v -> Output d v -> Ordering

(<) :: Output d v -> Output d v -> Bool

(<=) :: Output d v -> Output d v -> Bool

(>) :: Output d v -> Output d v -> Bool

(>=) :: Output d v -> Output d v -> Bool

max :: Output d v -> Output d v -> Output d v

min :: Output d v -> Output d v -> Output d v

(Show d, Show v) => Show (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

showsPrec :: Int -> Output d v -> ShowS

show :: Output d v -> String

showList :: [Output d v] -> ShowS

Generic (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Associated Types

type Rep (Output d v) :: Type -> Type

Methods

from :: Output d v -> Rep (Output d v) x

to :: Rep (Output d v) x -> Output d v

(Arbitrary d, Arbitrary v) => Arbitrary (Output d v)

Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

Methods

arbitrary :: Gen (Output d v)

shrink :: Output d v -> [Output d v]

(Swappable d, Swappable v) => Swappable (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Output d v -> Output d v

(Eq d, IEq v) => IEq (Output d v)

Equality on validators is intensional; (Validator f == Validator f') when f and f' happen to point to the same bit of memory when the equality runs. Thus if iEq f f' returns True this means that f and f' represent the same mathematical function, and indeed are also the same code. If iEq f f' returns False this does not mean that f and f' represent distinct mathematical functions. It just means they were represented by distinct code when iEq is called. This may be useful for running tests where we check that gobs of code get put in the right places and assembled in the right ways, without necessarily caring to execute them (or even without necessarily instantiating executable values). instance IEq Value where

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

iEq :: Output d v -> Output d v -> IO Bool

HasOutputPositions (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: Output d v -> [Position]

HasInputPositions (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

inputPositions :: Output d v -> [Position]

type Rep (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

type Rep (Output d v) = D1 (MetaData "Output" "Language.Nominal.Examples.IdealisedEUTxO" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" False) (C1 (MetaCons "Output" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Position) :*: (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 d) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 v))))

data TransactionF f r d v

A TransactionF consists of an f of inputs, and a list of outputs.

Type parameters are:

• f a parameter which can be instantiated to a type-constructor (higher-kinded types). In this file, f will be either list or nonempty list.
• r a parameter for the redeemer.
• d a parameter for the datum.
• v a parameter for the validator.

Constructors

Transaction (f (Input r)) [Output d v]

Instances

(Support d, Support r, Support v) => KSupport Tom (Context r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Context r d v -> Set (KAtom Tom)

(Support d, Support r, Support v) => KSupport Tom (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Transaction r d v -> Set (KAtom Tom)

(UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Context r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Context r d v -> Context r d v -> KRen Tom

ren :: KRen Tom -> Context r d v -> Context r d v

(UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Transaction r d v -> Transaction r d v -> KRen Tom

ren :: KRen Tom -> Transaction r d v -> Transaction r d v

(Arbitrary r, Arbitrary d, Arbitrary v) => Arbitrary (Context r d v)

Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

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)

Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

Methods

arbitrary :: Gen (Transaction r d v)

shrink :: Transaction r d v -> [Transaction r d v]

(Swappable r, Swappable d, Swappable v) => Swappable (Context r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Context r d v -> Context r d v

(Swappable r, Swappable d, Swappable v) => Swappable (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Transaction r d v -> Transaction r d v

HasOutputPositions (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: Transaction r d v -> [Position]

HasInputPositions (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

inputPositions :: Transaction r d v -> [Position]

Validator r d v => Binder (Chunk r d v) [Atom] [Transaction r d v] Tom

Acts on a Chunk by unpacking it as a transaction-list and a list of locally bound atoms, and applying a function.

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(@@) :: Chunk r d v -> ([Atom] -> [Transaction r d v] -> b) -> KNom Tom b

(@>) :: [Atom] -> [Transaction r d v] -> Chunk r d v

resMay :: [Atom] -> [Transaction r d v] -> Maybe (Chunk r d v)

(Eq r, Eq d, Eq v) => Eq (TransactionF [] r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(==) :: TransactionF [] r d v -> TransactionF [] r d v -> Bool

(/=) :: TransactionF [] r d v -> TransactionF [] r d v -> Bool

(Eq r, Eq d, Eq v) => Eq (TransactionF NonEmpty r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(==) :: TransactionF NonEmpty r d v -> TransactionF NonEmpty r d v -> Bool

(/=) :: TransactionF NonEmpty r d v -> TransactionF NonEmpty r d v -> Bool

(Show (f (Input r)), Show d, Show v) => Show (TransactionF f r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

showsPrec :: Int -> TransactionF f r d v -> ShowS

show :: TransactionF f r d v -> String

showList :: [TransactionF f r d v] -> ShowS

Generic (TransactionF f r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Associated Types

type Rep (TransactionF f r d v) :: Type -> Type

Methods

from :: TransactionF f r d v -> Rep (TransactionF f r d v) x

to :: Rep (TransactionF f r d v) x -> TransactionF f r d v

type Rep (TransactionF f r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

type Rep (TransactionF f r d v) = D1 (MetaData "TransactionF" "Language.Nominal.Examples.IdealisedEUTxO" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" False) (C1 (MetaCons "Transaction" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (f (Input r))) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Output d v])))

type Transaction = TransactionF []

type Context = TransactionF NonEmpty

Calculating input and output positions

A technical matter: we exploit the Haskell typeclass mechanisms to set up some machinery to calculate the input and output positions mentioned in a data structure. This resembles the development of Support, but specialised to intputs and outputs.

class HasInputPositions a where

A typeclass for types for which we can calculate input positions.

inputPositions just traverses a's type structure, looking for subtypes of the form Input p _, and collecting the ps. The only interesting instance is that of KNom a, where bound ps get garbage-collected.

Minimal complete definition

Nothing

Methods

inputPositions :: a -> [Position]

inputPositions :: (Generic a, GHasInputPositions (Rep a)) => a -> [Position]

Instances

HasInputPositions a => HasInputPositions [a]

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

inputPositions :: [a] -> [Position]

HasInputPositions a => HasInputPositions (NonEmpty a)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

inputPositions :: NonEmpty a -> [Position]

HasInputPositions (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

inputPositions :: Input r -> [Position]

(HasInputPositions a, HasInputPositions b) => HasInputPositions (a, b)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

inputPositions :: (a, b) -> [Position]

HasInputPositions (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

inputPositions :: Output d v -> [Position]

HasInputPositions (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

inputPositions :: Transaction r d v -> [Position]

class HasOutputPositions a where

A typeclass for types for which we can calculate output positions.

outputPositions just traverses a's type structure, looking for subtypes of the form Output p _ _, and collecting the ps. The only interesting instance is that of KNom a, where bound ps get garbage-collected.

Minimal complete definition

Nothing

Methods

outputPositions :: a -> [Position]

outputPositions :: (Generic a, GHasOutputPositions (Rep a)) => a -> [Position]

Instances

HasOutputPositions a => HasOutputPositions [a]

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: [a] -> [Position]

HasOutputPositions a => HasOutputPositions (NonEmpty a)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: NonEmpty a -> [Position]

(Swappable a, HasOutputPositions a) => HasOutputPositions (Nom a)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: Nom a -> [Position]

HasOutputPositions (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: Input r -> [Position]

(HasOutputPositions a, HasOutputPositions b) => HasOutputPositions (a, b)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: (a, b) -> [Position]

HasOutputPositions (Output d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: Output d v -> [Position]

HasOutputPositions (Transaction r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

outputPositions :: Transaction r d v -> [Position]

Validators

Our types for Output, TransactionF, and Context are parameterised over a type of validators. We now build a typeclass Validator to hold validators, and build two instances Val and ValFin:

• Val is just a type of functions wrapped up in a wrapper saying "I am a validator". If you have a function and it's a validator, you can put it here.
• ValFin is an equivariant orbit-finite map type, intended to be used with the machinery in Language.Nominal.Equivar. A significant difference from Val is that ValFin can support equality Eq.

class (Support r, Support d, Support v) => Validator r d v | v -> r d where

A typeclass for validators. A validator is an equivariant object that takes a datum and a Context, and returns a Bool.

Methods

validate :: v -> d -> Context r d v -> Bool

Instances

(UnifyPerm r, UnifyPerm d) => Validator r d (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

validate :: ValFin r d -> d -> Context r d (ValFin r d) -> Bool

(Support r, Support d) => Validator r d (Val r d)

Val is a Validator

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

validate :: Val r d -> d -> Context r d (Val r d) -> Bool

(Support r, Support d) => Validator r d (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

validate :: ValTriv r d -> d -> Context r d (ValTriv r d) -> Bool

data ValTriv r d

A type for trivial validators that always return true

Constructors

ValTriv

Instances

(Support r, Support d) => Validator r d (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

validate :: ValTriv r d -> d -> Context r d (ValTriv r d) -> Bool

(Support r, Support d) => Fixable r d (ValTriv r d)

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)

KSupport Tom (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> ValTriv r d -> Set (KAtom Tom)

KUnifyPerm Tom (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> ValTriv r d -> ValTriv r d -> KRen Tom

ren :: KRen Tom -> ValTriv r d -> ValTriv r d

Eq (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(==) :: ValTriv r d -> ValTriv r d -> Bool

(/=) :: ValTriv r d -> ValTriv r d -> Bool

Ord (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

compare :: ValTriv r d -> ValTriv r d -> Ordering

(<) :: ValTriv r d -> ValTriv r d -> Bool

(<=) :: ValTriv r d -> ValTriv r d -> Bool

(>) :: ValTriv r d -> ValTriv r d -> Bool

(>=) :: ValTriv r d -> ValTriv r d -> Bool

max :: ValTriv r d -> ValTriv r d -> ValTriv r d

min :: ValTriv r d -> ValTriv r d -> ValTriv r d

Read (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

readsPrec :: Int -> ReadS (ValTriv r d)

readList :: ReadS [ValTriv r d]

readPrec :: ReadPrec (ValTriv r d)

readListPrec :: ReadPrec [ValTriv r d]

Show (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

showsPrec :: Int -> ValTriv r d -> ShowS

show :: ValTriv r d -> String

showList :: [ValTriv r d] -> ShowS

Arbitrary (ValTriv r d)

Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

Methods

arbitrary :: Gen (ValTriv r d)

shrink :: ValTriv r d -> [ValTriv r d]

Swappable (ValTriv r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> ValTriv r d -> ValTriv r d

newtype Val r d

A Val is an equivariant predicate on datum and context. For convenience we make it Nameless.

Constructors

Val (EvFun (d, Context r d (Val r d)) Bool)

Instances

(Support r, Support d) => Validator r d (Val r d)

Val is a Validator

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

validate :: Val r d -> d -> Context r d (Val r d) -> Bool

(Support r, Support d) => Fixable r d (Val r d)

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)

KRestrict Tom (Val r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

restrict :: [KAtom Tom] -> Val r d -> Val r d

KSupport Tom (Val r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Val r d -> Set (KAtom Tom)

Show (Val r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

showsPrec :: Int -> Val r d -> ShowS

show :: Val r d -> String

showList :: [Val r d] -> ShowS

Swappable (Val r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Val r d -> Val r d

IEq (Val r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

iEq :: Val r d -> Val r d -> IO Bool

newtype ValFin r d

A ValFin is an equivariant orbit-finite predicate on datum and context. For convenience we make it Nameless.

Constructors

ValFin (EvFinMap (d, Context r d (ValFin r d)) Bool)

Instances

(UnifyPerm r, UnifyPerm d) => Validator r d (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

validate :: ValFin r d -> d -> Context r d (ValFin r d) -> Bool

(Eq r, UnifyPerm r, Eq d, UnifyPerm d) => Fixable r d (ValFin r d)

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)

KRestrict Tom (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

restrict :: [KAtom Tom] -> ValFin r d -> ValFin r d

KSupport Tom (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> ValFin r d -> Set (KAtom Tom)

(UnifyPerm r, UnifyPerm d) => KUnifyPerm Tom (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> ValFin r d -> ValFin r d -> KRen Tom

ren :: KRen Tom -> ValFin r d -> ValFin r d

(UnifyPerm r, UnifyPerm d) => Eq (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(==) :: ValFin r d -> ValFin r d -> Bool

(/=) :: ValFin r d -> ValFin r d -> Bool

(Show d, Show r) => Show (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

showsPrec :: Int -> ValFin r d -> ShowS

show :: ValFin r d -> String

showList :: [ValFin r d] -> ShowS

Generic (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Associated Types

type Rep (ValFin r d) :: Type -> Type

Methods

from :: ValFin r d -> Rep (ValFin r d) x

to :: Rep (ValFin r d) x -> ValFin r d

(Eq r, UnifyPerm r, Arbitrary r, Eq d, UnifyPerm d, Arbitrary d) => Arbitrary (ValFin r d)

Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

Methods

arbitrary :: Gen (ValFin r d)

shrink :: ValFin r d -> [ValFin r d]

Swappable (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> ValFin r d -> ValFin r d

type Rep (ValFin r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

type Rep (ValFin r d) = Rep (EvFinMap (d, Context r d (ValFin r d)) Bool)

Chunks

A Chunk is a valid list of transactions in a local name-binding context. Validity is enforced by the constructor appendTxChunk, which imposes a validity check.

Chunk, not Blockchain, is the fundamental abstraction of our development. A blockchain is just a chunk without any UTxIs (see isBlockchain and utxisOfChunk); conversely a chunk is "like a blockchain, but may have UTxIs as well as UTxOs".

Chunks have properties that blockchains don't. For instance:

• If we slice a chunk up into pieces, we get another chunk.
• A subchunk of a chunk is still a chunk.

In contrast, if we slice up a blockchain, we get chunks, not blockchains. Thus, blockchains are not naturally compositional and structured in the way that chunks are.

This is a benefit of making the datatype of chunks our primary abstraction.

newtype Chunk r d v

A Chunk is a valid list of transactions in a local name-binding context. Think of it as a generalisation of blockhains that allows UTxIs (unspent transaction inputs).

Constructors

Chunk

Fields

• chunkToTxList :: Nom [Transaction r d v]

Instances

(Swappable r, Swappable d, Swappable v) => KRestrict Tom (Chunk r d v)

Restrict atoms in a Chunk.

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

restrict :: [KAtom Tom] -> Chunk r d v -> Chunk r d v

(Support r, Support d, Support v) => KSupport Tom (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Chunk r d v -> Set (KAtom Tom)

(UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Chunk r d v -> Chunk r d v -> KRen Tom

ren :: KRen Tom -> Chunk r d v -> Chunk r d v

Validator r d v => Semigroup (Maybe (Chunk r d v))

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(<>) :: Maybe (Chunk r d v) -> Maybe (Chunk r d v) -> Maybe (Chunk r d v)

sconcat :: NonEmpty (Maybe (Chunk r d v)) -> Maybe (Chunk r d v)

stimes :: Integral b => b -> Maybe (Chunk r d v) -> Maybe (Chunk r d v)

Validator r d v => Monoid (Maybe (Chunk r d v))

Maybe Chunk forms a monoid, with unit being the empty chunk.

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

mempty :: Maybe (Chunk r d v)

mappend :: Maybe (Chunk r d v) -> Maybe (Chunk r d v) -> Maybe (Chunk r d v)

mconcat :: [Maybe (Chunk r d v)] -> Maybe (Chunk r d v)

(UnifyPerm r, UnifyPerm d, UnifyPerm v, Validator r d v) => Eq (Chunk r d v)

Chunk equality tests for equality, with permutative unification on the local names

(==) = unifiablePerm would be wrong; we should only unify bound atoms.

Note: KRen equality compares nubs (non-identity mappings)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(==) :: Chunk r d v -> Chunk r d v -> Bool

(/=) :: Chunk r d v -> Chunk r d v -> Bool

(Show r, Show d, Show v) => Show (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

showsPrec :: Int -> Chunk r d v -> ShowS

show :: Chunk r d v -> String

showList :: [Chunk r d v] -> ShowS

Generic (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Associated Types

type Rep (Chunk r d v) :: Type -> Type

Methods

from :: Chunk r d v -> Rep (Chunk r d v) x

to :: Rep (Chunk r d v) x -> Chunk r d v

(Arbitrary r, Support r, Arbitrary d, Support d, Arbitrary v, Validator r d v) => Arbitrary (Chunk r d v)

Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

Methods

arbitrary :: Gen (Chunk r d v)

shrink :: Chunk r d v -> [Chunk r d v]

Validator r d v => PartialMonoid (Chunk r d v)

Chunk forms a partial monoid

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

pzero :: Chunk r d v

Validator r d v => PartialSemigroup (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

padd :: Chunk r d v -> Chunk r d v -> Maybe (Chunk r d v)

(Swappable r, Swappable d, Swappable v) => Swappable (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Chunk r d v -> Chunk r d v

Validator r d v => Binder (Chunk r d v) [Atom] [Transaction r d v] Tom

Acts on a Chunk by unpacking it as a transaction-list and a list of locally bound atoms, and applying a function.

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

(@@) :: Chunk r d v -> ([Atom] -> [Transaction r d v] -> b) -> KNom Tom b

(@>) :: [Atom] -> [Transaction r d v] -> Chunk r d v

resMay :: [Atom] -> [Transaction r d v] -> Maybe (Chunk r d v)

type Rep (Chunk r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

type Rep (Chunk r d v) = D1 (MetaData "Chunk" "Language.Nominal.Examples.IdealisedEUTxO" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" True) (C1 (MetaCons "Chunk" PrefixI True) (S1 (MetaSel (Just "chunkToTxList") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Nom [Transaction r d v]))))

transactionValid :: Transaction r d v -> Bool

A transaction is valid if (at least) all positions are disjoint

singletonChunk :: Transaction r d v -> Maybe (Chunk r d v)

Tries to create a valid Chunk from a single TransactionF. If it fails, we get Nothing.

unsafeSingletonChunk :: HasCallStack => Transaction r d v -> Chunk r d v

Creates a valid Chunk from a single TransactionF. If it fails (because the transaction is invalid), it raises an error.

txListToChunk :: Validator r d v => [Transaction r d v] -> Maybe (Chunk r d v)

Combine a list of transactions into a Chunk. Return Nothing if list does not represent a valid chunk.

nomTxListToNomChunk :: (HasCallStack, Validator r d v) => Nom [Transaction r d v] -> Maybe (Nom (Chunk r d v))

Combines a list of TransactionFs in a KNom binding context, into a Chunk.

• Gathers any excess positions (those not linking inputs to outputs) in the KNom binding.
• Returns Nothing if the transaction list doesn't form a valid Chunk.

nomTxListToChunk :: (HasCallStack, Validator r d v) => Nom [Transaction r d v] -> Maybe (Chunk r d v)

Combines a list of transactions in a binding context, into a Chunk, with a check that no excess positions are bound. Returns Nothing if check fails.

Examples

Some example chunks for the reader's convenience and for unit tests.

• exampleCh0 is the chunk containing a trivial transaction with no inputs and no outputs (and one locally bound name, which is not used).
• exampleCh1 is an output with trivial validator. Wrapped in a Nom binding to store its position.
• exampleCh2 is an input. Wrapped in a Nom binding to store its position.
• exampleCh12 is exampleCh1 <> exampleCh 2. Note their positions don't line up. Also has overbinding!
• exampleCh21 is exampleCh1 <> exampleCh 2 with positions lined up.
• exampleCh12' is exampleCh2 <> exampleCh 1 with positions lined up. Name-clash: fails.

See isChunk and isBlockchain for unit tests.

exampleCh0 :: Chunk Int Int (ValTriv Int Int)

Example chunk 0: "Chunk [p] [Transaction [] []]"

A chunk containing an empty transaction, with a vacuous binding by some p.

Is chunk. Is blockchain.

>>> isChunk exampleCh0
True

>>> isBlockchain exampleCh0
True

exampleCh1 :: Nom (Chunk Int Int (ValTriv Int Int))

Example chunk 1: "Chunk [p] [Transaction [] [Output p 0 (const True)]]"

One output with datum 0 and trivial validator that always returns True.

Is chunk. Is blockchain.

exampleCh2 :: Nom (Chunk Int Int (ValTriv Int Int))

Example chunk 2: "Chunk [p] [Transaction [Input p 0] []]"

One input with redeemer 0.

Is chunk. Is not blockchain.

exampleCh12 :: Chunk Int Int (ValTriv Int Int)

Example chunk obtained by concatenating chunks 1 and 2. Concat succeeds but positions don't line up. Is not blockchain, and also is not valid chunk because of overbinding.

"Chunk [p1, p2] [Transaction [Input p2 0] [], Transaction [] [Output p1 0 (const True)])]"

(Note: we write lists with their head to the left, so time flows from right to left above.)

>>> isChunk exampleCh12
False

exampleCh21 :: Chunk Int Int (ValTriv Int Int)

Example chunk obtained by combining chunks 1 and 2, now on same name so input points to output.

"Chunk [p] [Transaction [Input p 0] [], Transaction [] [Output p 0 (const True)])]"

(Note: we write lists with their head to the left, so time flows from right to left above.)

Is chunk. Is blockchain.

exampleCh12' :: Maybe (Chunk Int Int (ValTriv Int Int))

Example chunk obtained by combining chunks 1 and 2, on same name. But output comes after input, not before. Concat fails because nameclash is detected.

Unspent (dangling) elements: UTxO, UTxI, UTxC

We care about which inputs point to earlier outputs, and which outputs point to later inputs, and which do not. Specifically, we introduce three functions:

• utxosOfChunk, calculating those outputs that do not point to a later input in a chunk. This is standard (albeit for chunks, not blockchains).
• utxisOfChunk, calculating those inputs that do not point to an earlier output in a chunk. While not complicated to define, the explicit emphasis on this as an interesting value to calculate comes from our shift from working with Blockchains to working with Chunks.
• utxcsOfChunk, calculating those contexts (inputs-in-their-transaction) that do not point to an earlier output in a chunk. Again, the explicit emphasis on this as an interesting value to calculate comes from our shift from working with Blockchains to working with Chunks.

outputsOfTx :: Transaction r d v -> [Output d v]

Return the output-list of a TransactionF.

inputsOfTx :: Transaction r d v -> [Input r]

Return the input-list of a TransactionF.

txPoint :: Support r => Transaction r d v -> Position -> Context r d v

Point a transaction at p

contextsOfTx :: Support r => Transaction r d v -> [Context r d v]

Form the contexts of a TransactionF.

utxosOfChunk :: Validator r d v => Chunk r d v -> [Output d v]

Calculate unspent outputs.

We tell an output is unspent when its position isn't bound in the enclosing KNom name-context.

utxisOfChunk :: Validator r d v => Chunk r d v -> [Input r]

Calculate unspent inputs.

Because we're dealing with transaction lists, we care about dangling inputs (which we call UTxIs) as well as UTxOs.

contextPos :: Context r d v -> Position

What's the point of my context? The position p of the first element of the input list of a context is deemed to be the "call site" from which the context tries to find a preceding output (with position p) in its Chunk.

utxcsOfChunk :: Validator r d v => Chunk r d v -> Nom [Context r d v]

Calculate unspent input contexts.

Because we're dealing with transaction lists, we care about dangling contexts (which we call UTxCs).

Combining and extending chunks

appendTxChunk :: (HasCallStack, Validator r d v) => Transaction r d v -> Chunk r d v -> Maybe (Chunk r d v)

appendTxChunk tx txs adds tx to txs, provided that:

• tx is valid
• there is no position name-clash and
• validators are happy.

This is the core of this file. In a certain sense, everything is just different ways of wiring into this function.

appendTxMaybeChunk :: Validator r d v => Transaction r d v -> Maybe (Chunk r d v) -> Maybe (Chunk r d v)

Version of appendTxChunk that acts directly on Maybe (Chunk r d v).

concatChunk :: Validator r d v => Chunk r d v -> Chunk r d v -> Maybe (Chunk r d v)

Concatenate two Chunks, merging their binding contexts in a capture-avoiding manner. If concatenation is impossible (e.g. because validation fails), defaults to Chunk Nothing.

Note: No explicit checks are made here that inputs are valid chunks. In particular, no overbinding protection (overbinding = Nom binder in Chunk binds excess positions not involved in UTxO-UTxI linkage). If you want such checks, look at isChunk and isBlockchain.

Works by unpacking first chunk as a list of transactions and appending them to Just the second argument. Local binding of first chunk gets carried over automatically; new local bindings may get generated during the append.

safeConcatChunk :: Validator r d v => Chunk r d v -> Chunk r d v -> Maybe (Chunk r d v)

A version of concatChunk that performs explicit validity checks on its inputs and result.

Splitting chunks up

genUnNomChunk :: Validator r d v => Chunk r d v -> Chunk r d v

For debugging

isPrefixChunk :: (UnifyPerm r, UnifyPerm d, UnifyPerm v, Validator r d v) => Nom (Chunk r d v) -> Chunk r d v -> Bool

Check whether one chunk is a prefix of another. See chunkTail to understand why the KNom binding on the first argument is required.

chunkLength :: Validator r d v => Chunk r d v -> Int

Calculate the length of a Chunk

chunkTail :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Maybe (Nom (Chunk r d v))

Calculate the tail of a chunk. Two monads here:

• Maybe, because the underlying list of transactions might be empty and so have no tail. And if it's not empty ...
• KNom ... to bind the names of any positions in newly-exposed UTxOs.

chunkHead :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Maybe (Nom (Transaction r d v))

Calculate the head of a chunk.

warningNotChunkTail :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Maybe (Chunk r d v)

Compare the code for this function with the code for chunkTail. It looks plausible ... but it's wrong.

It looks like it returns the tail of a chunk, and indeed it does. However, the result is not a chunk because positions get exposed.

See the test prop_warningNotChunkTail_is_not_chunk.

chunkTakeEnd :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Int -> Chunk r d v -> Nom (Chunk r d v)

take, for chunks. The KNom binding captures any dangling UTxOs or UTxIs that are left after truncating the chunk.

subTxListOf :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Nom [[Transaction r d v]]

List of subchunks. KNom binding is to capture dangling UTxOs or UTxIs.

reverseTxsOf :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Maybe (Chunk r d v)

Take a chunk and reverse its transactions. Usually this will result in an invalid chunk, in which case we get Nothing. Used for testing.

chunkToHdTl :: Validator r d v => Chunk r d v -> Maybe (Nom (Transaction r d v, Chunk r d v))

Split a chunk into a head and a tail.

chunkToHdHdTl :: Validator r d v => Chunk r d v -> Maybe (Nom (Transaction r d v, Transaction r d v, Chunk r d v))

Split a chunk into a head and a head and a tail.

Blockchain

data Blockchain r d v

A blockchain is a valid Chunk, with no unspent inputs.

Instances

(Support r, Support d, Support v) => KSupport Tom (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

ksupp :: proxy Tom -> Blockchain r d v -> Set (KAtom Tom)

(UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kunifyPerm :: proxy Tom -> Blockchain r d v -> Blockchain r d v -> KRen Tom

ren :: KRen Tom -> Blockchain r d v -> Blockchain r d v

(Show r, Show d, Show v) => Show (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

showsPrec :: Int -> Blockchain r d v -> ShowS

show :: Blockchain r d v -> String

showList :: [Blockchain r d v] -> ShowS

Generic (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Associated Types

type Rep (Blockchain r d v) :: Type -> Type

Methods

from :: Blockchain r d v -> Rep (Blockchain r d v) x

to :: Rep (Blockchain r d v) x -> Blockchain r d v

(Arbitrary r, Support r, Arbitrary d, Support d, Arbitrary v, Fixable r d v) => Arbitrary (Blockchain r d v)

Defined in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec

Methods

arbitrary :: Gen (Blockchain r d v)

shrink :: Blockchain r d v -> [Blockchain r d v]

(Swappable r, Swappable d, Swappable v) => Swappable (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Blockchain r d v -> Blockchain r d v

type Rep (Blockchain r d v)

Defined in Language.Nominal.Examples.IdealisedEUTxO

type Rep (Blockchain r d v) = D1 (MetaData "Blockchain" "Language.Nominal.Examples.IdealisedEUTxO" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" True) (C1 (MetaCons "Blockchain" PrefixI True) (S1 (MetaSel (Just "getBlockchain") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Chunk r d v))))

getBlockchain :: Blockchain r d v -> Chunk r d v

blockchain :: (HasCallStack, Validator r d v) => Chunk r d v -> Blockchain r d v

Smart constructor for a Blockchain. Ensures only valid blockchains are constructed, by testing for isBlockchain.

Is Chunk / Blockchain check

chunkBindingOK :: Validator r d v => Chunk r d v -> Bool

Check that the correct atoms are bound in a Chunk.

chunkValidatorsOK :: Validator r d v => Chunk r d v -> Bool

Check that validators are happy, by taking a Chunk apart and putting it together again.

isChunk :: Validator r d v => Chunk r d v -> Bool

Is this a valid chunk? (exampleCh1, exampleCh2, exampleCh12, exampleCh21)

>>> resAppC isChunk exampleCh1
True 

>>> resAppC isChunk exampleCh2
True 

>>> isChunk exampleCh12
False

>>> isChunk exampleCh21
True

isChunk' :: (Validator r d v, UnifyPerm r, UnifyPerm d, UnifyPerm v) => Chunk r d v -> Bool

Is this a valid chunk? Test by splitting it into a transaction list and putting it back together again.

isBlockchain :: Validator r d v => Chunk r d v -> Bool

A blockchain is a valid Chunk with no UTxI (unspent transaction inputs). (exampleCh1, exampleCh2, exampleCh12, exampleCh21)

>>> isBlockchain exampleCh0
True

>>> resAppC isBlockchain exampleCh1
True

>>> resAppC isBlockchain exampleCh2
False 

>>> isBlockchain exampleCh12
False 

>>> isBlockchain exampleCh21
True 

isBlockchain' :: Validator r d v => Maybe (Chunk r d v) -> Bool

Blockchain check for Maybe a Chunk.

Intensional equality of Chunk

Modelled on a post by Oleg Kiselyov An intensional equality allows us to compare Chunks for equality of UTxOs, even if the type of validators does not have an Eq instance.

We don't do this at the moment (we use ValFin instead), but we still provide the facility in case it is useful for a user running e.g. QuickCheck tests where we care that structure gets put in the right place and assembled in the right ways, without caring too much about executing that structure for values of specific interest.

class IEq a

Instances

IEq a => IEq [a]

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

iEq :: [a] -> [a] -> IO Bool

Eq r => IEq (Input r)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

iEq :: Input r -> Input r -> IO Bool

IEq (a -> b)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

iEq :: (a -> b) -> (a -> b) -> IO Bool

IEq (Val r d)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

iEq :: Val r d -> Val r d -> IO Bool

(Eq d, IEq v) => IEq (Output d v)

Equality on validators is intensional; (Validator f == Validator f') when f and f' happen to point to the same bit of memory when the equality runs. Thus if iEq f f' returns True this means that f and f' represent the same mathematical function, and indeed are also the same code. If iEq f f' returns False this does not mean that f and f' represent distinct mathematical functions. It just means they were represented by distinct code when iEq is called. This may be useful for running tests where we check that gobs of code get put in the right places and assembled in the right ways, without necessarily caring to execute them (or even without necessarily instantiating executable values). instance IEq Value where

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

iEq :: Output d v -> Output d v -> IO Bool

IEq (KEvFun k a b)

Defined in Language.Nominal.Examples.IdealisedEUTxO

Methods

iEq :: KEvFun k a b -> KEvFun k a b -> IO Bool

equivChunk :: (Eq r, Eq d, IEq v, Validator r d v) => Chunk r d v -> Chunk r d v -> IO Bool

Intensional equality

Tests

Property-based tests are in Language.Nominal.Properties.Examples.IdealisedEUTxOSpec.