Roadmap

[WhatisRT]

This issue is for discussing the high-level roadmap for this project. Note that we may drop things off of here if we decide against them in the future.

Features

Properly dealing with multiple eras/subprojects

A long time ago, we decided that the easiest way to deal with this would be code copy. E.g. for the Alonzo era, we could copy our entire codebase into a Ledger.Alonzo subtree and properly change the logic to reflect the Alonzo logic. Then we prove some theorems relating it the the main version of the ledger. For example, that some STS behaves identically, or that it is equivalent up to some specified thing. Ideally, in the end we'd have a relation between the CHAIN STSs, but it remains to be seen how feasible that is. By including these proofs, we prevent bit-rotting: if we change something somewhere, those proofs force us to make the correct adjustments everywhere else.

Implement previous eras

This is self-explanatory. A lot has been done already, but especially Shelley is still missing many pieces.

Simplified ledger

There are many checks and subsystems in the ledger that are somewhat irrelevant for most users, especially smart contract authors. The idea of this project is to make another copy of this project in a subtree, remove the logic that most people don't care about and then prove a theorem relating that simplified ledger to the original one. This would probably something like "if you have a block that doesn't use certain features, CHAIN and simplified CHAIN are equivalent".

Using Agda as a Plutus substitute

This is already WIP with some small examples working. The idea is that since we're completely generic in our interface to Plutus, we can instantiate it with a type of Agda functions. Then, a script can be implemented in Agda and we can prove properties about that script in the context of the real ledger. It is then natural to attempt to reason about these scripts in the manner of the 'Structured Contracts' paper.

Verifying mainnet

Technically this has a larger scope than just this project, but it is still greatly affected. This is purely aspirational, there are no plans for working on this right now. The idea is to make the Plutus core formalization compatible with the formal ledger (or alternatively the Plutus implementation), hooking everything up with proper deserialization libraries and actually using the ledger formalization to verify the history of mainnet. Since we don't ever plan on implementing Byron this would probably have to start at a snapshot, but we could in principle go as early as the first Shelley block. Actually running this would require many performance and memory improvements, but it doesn't have to be fast.

Refactorings

These are all comparatively small, but that doesn't make them less important.

Simplify UTXOS

In principle there is no need for a UTXOS STS. This is because the relational approach has no notion of time, so when we say that we have to run the scripts after everything else that doesn't mean that we need to structure our relations that way. It would make more sense to return to updating the state to UTXO and to check the scripts in UTXOW. The implementation might not follow this approach, so we still might have to provide the version we're currently using.

Revisit the general structure

The ledger has been growing organically for a while, and we just keep adding things wherever they fit. We should properly review that structure, decide what structures we like and what we want to change and write those decisions down. This gives us a guideline for the future. Here are some questions to ask:

• Are all the XStructure records useful? Can we get rid of some?
• How do we want to deal with opening of records? Do we want to open some publically?
• More generally, how do we deal with name clashes that can't be fixed by type classes?

Factor out things into libraries

This is less useful for this project specifically, but we have some things that should live in libraries instead, first and foremost the set theory. Other projects use parts of the Ledger codebase as a library and it would be better if that wasn't necessary.