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

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.

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.

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.

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.

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.

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

A type for trivial validators that always return true

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

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

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).

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

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

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

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

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.

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.

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

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.

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

One input with redeemer 0.

Is chunk. Is not blockchain.

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

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.

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.

Return the output-list of a TransactionF.

Return the input-list of a TransactionF.

Point a transaction at p

Form the contexts of a TransactionF.

Calculate unspent outputs.

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

Calculate unspent inputs.

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

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.

Calculate unspent input contexts.

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

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.

Version of appendTxChunk that acts directly on 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.

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

For debugging

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

Calculate the length of a Chunk

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.

Calculate the head of a chunk.

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.

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

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

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

Split a chunk into a head and a tail.

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

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

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

Check that the correct atoms are bound in a Chunk.

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

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

>>> resAppC isChunk exampleCh1
True 

>>> resAppC isChunk exampleCh2
True 

>>> isChunk exampleCh12
False

>>> isChunk exampleCh21
True

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

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 

Blockchain check for Maybe a Chunk.

Intensional equality