-
Notifications
You must be signed in to change notification settings - Fork 13
Byron Roadmap
The tasks detailed in the following sections are broadly prioritized.
- ✔️ Validate Valid Generated Chains against Full Specification
- ✔️ Validate Invalid Generated Chains against Full Specification
- ✔️ Multiple Validation Modes
- ✔️ Formulate and Implement Properties for our Operational Rules
- ✔️ Performance Optimisation
This task is about testing that the
cardano-ledger
implementation actually conforms to the
specifications.
For carrying out this validation, the idea is to generate random chains of blocks according to our formal specification. These blocks are then elaborated into concrete blocks, and the actual ledger validation is run on those blocks to check that the generated valid blocks are also valid according to the concrete implementation.
This task can be broken down into the following sub-tasks:
- Make a generator for (valid) abstract blocks
- Elaboration abstract blocks into concrete blocks
- Audit the generators and tests to make sure we cover all the important cases
The following table shows the progress of the work in this area, where the symbols have the following meaning:
- 🚧: not started yet
- 🔨: work in progress
- ✔️: done
Generators | Elaborators | Tests | |
---|---|---|---|
Delegation | ✔️ | ✔️ | ✔️ |
Update | ✔️ | ✔️ | ✔️ |
UTxO | ✔️ | ✔️ | ✔️ |
This task extends our conformance tests to cover the case of invalid chains. Here we want to check that the executable specification and concrete implementation agree on when the validation should fail.
Manual invalid generators | Goblins generators | Tests with manual generators | Tests with Goblins | |
---|---|---|---|---|
Delegation | ✔️ | ✔️ | ✔️ | ✔️ |
Update | ✔️ | ✔️ | ✔️ | ✔️ |
UTxO | ➖ | ✔️ | ➖ | ✔️ |
Block headers | ✔️ | ➖ | ✔️ | ➖ |
Note that goblins generators are complementary to manual invalid-chain generators. Since the work on goblins took place in parallel with the work on manual invalid generators, some tests make use of only one of these.
For instance, since we have goblins generators for UTxO, we skipped conformance testing with manually written generators. Having both generators (manual and goblins) is a nice to have, but by no means required for completing this task. By only having one kind of generators we might be exploring less test cases, but it is difficult to know whether this is the case and what is the portion of the state space we're failing to explore.
Related to input-output-hk/ouroboros-network#440
- We need to be able to run validation with a signal that may have been previously applied
- There should be three scenarios: NewSignal/NewState, OldSignal/NewState, OldSignal/OldState
- We should customise which predicates should be run depending on the situation
To make sure our rules are sound we should test them against some desirable properties. Depending on the time left these are some properties we want to check:
delegation certificates cannot be replayedevery valid protocol update allows to produce new blocksutxo and transaction outputs must be disjointno double spending and utxo is inputs minus outputs
- Profile chain validation and identify performance hot-spots
- Audit memory-use during a bulk validation (ensure there aren’t any leaks)
- Ensure that the ledger state does not contain any thunks at each step after applying state update rules