Byron Next Iterations
This page contains list of sub-tasks related to the main tasks that need to be carried out to deliver the Byron ledger to mainnet:
- Conformance tests of valid chains: every valid chain generated according to the rules defined in the formal specification should be valid according to the actual implementation.
- Conformance tests of invalid chains: every invalid chain generated according to the formal specification should be rejected by the actual implementation.
- Property tests for the transition system: the formal specification meets certain correctness criteria: e.g. no-double spending is possible, delegation certificates cannot be replayed, etc.
The sub-tasks described in the following sections belong to the three main
tasks described above. These tasks are prioritized every two weeks, and
included in milestones. Priorities range from A (higher) to E (lowest).
Instead of naturals. Otherwise we need to handle potential overflows when elaborating.
Moreover, shouldn’t we pack them?
Why? Because then we can copy and paste `hedgehog` counterexamples. Put the symbols that shouldn’t be used in an `Internal` module.
In the UTXOW trace generator we need a set of addresses to generate:
- an initial UTxO
- transactions
At the moment this set of addresses is hardcoded. However it’d be sensible
to allow the initEnvGen and sigGen to take an additional state that
allows to pass information that is related to the trace generation
algorithm but unrelated to the STS (such as the set of addresses above).
We need to specify global constants in such a way that we can test with
different values (e.g. test with different values of k).
This will require adaptations in several places, from specs up to actual implementation. I don’t know whether it might impact consensus as well.
We should remove the use of:
- tuples
- lenses
Why:
- Since we’re using (composable) operational rules, we don’t need to look into a nested state and update it.
- Fewer dependencies
- Named field puns work better.
- Lenses put formal spec and executable spec further from each other.
- We’re using template Haskell for making lenses.
- Template haskell breaks search though tags.
- Tuples cause compilation errors difficult to understand.
- Tuples are unwieldy.
- Check stylish haskell on CI: do not block merging. But provide warnings (for the PR author and reviewers).
- Check hlint on CI: also don’t block merging.
Each of the chain ledger rules are separated in modules, this allow us to
get a nice dependency graph of the rules using graphmod:
By having such a dependency graph we can quickly visualize the dependency among the rules, which helps breaking down work that affects a large portion of the rules, for instance writing properties for them, or syncing formal and executable specs.
This task involves reorganizing the ledger rules so that each rule is in its own module, like they are in the chain executable spec.
This requires:
- coming up with notation for specifying the initial states of the system
- adapt the STS framework accordingly
For background see this thread and this thread.
Currently the protocol parameter updates always contain Just value. We
should sometimes elaborate to Nothing (for instance, when nothing
changes).