We should model the transaction fees in the ledger spec.

This should be added on top of the existing UTxO inference rule to make it compositional like the ledger rule.

The naming of this package is a bit unfortunate, but right now the crypto library here is called cardano-crypto, so we cannot reuse the name. It might be best to merge these two libraries now that we're going for a multi-repo structure.

The goal of this issue is to pull in the cardano-sl-crypto package and clean it up according to the conventions of the legacy-free codebase.

After moving cardano-prelude to an eponymous repo we need to make sure we can build referring to a specific git commit. We should also put the custom stack snapshot in this repo and other projects can refer to it via it's URL.

The new implementation needs to be able to deserialise exisiting blockchains and serialise to the same format until a hard-fork is taken. The simplest way to ensure this is to import the types from the old blockchain along with their golden/round-trip tests. We can then modify and extend those types, ensuring that all tests pass and any new serialisation is done conditionally on the software version.

Right now we're using a non-empty list, but this should really be a set and makes interaction with UTxO neater

All errors should be represented as ASTs to allow composition and maybe recovery.

The UTxO inference rule here involves Coins and the calculation of fees. We would like to change Coins to Lovelace and calculate fees in Lovelace to simplify things. To make sure the changes don't break validation, I will implement the rule with the old types, check it works on mainnet blocks, and then update the types making sure it is still correct.

This set of modules needs some clean-up. I believe some of the layout is due to module cycles, but we should be able to unravel them.

A blockchain specification with its inference rules can be found in specs/chain/latex. Write a Haskell implementation for it and place it in specs/chain/hs.

Duncan mentioned here that Coin and CoinPortion introduce rounding difficulties. We really do have a basic unit of currency, namely Lovelace, that we can treat as an Integer value. Ada or Coin then become a presentation of the underlying Lovelace.

There might be some problems when validating the old blockchain, so we need to investigate how much the validation relies of the types involved. We should look at all validation rules of existing blocks that involve Coin or CoinPortion.

This is an import and clean up of the cardano-sl-binary package in the legacy codebase. The template haskell code should be removed, as it is better to have hand-written instances for that kind of thing, and TH makes cross-compilation more tricky.

We have the pattern either (throwError . Error) pure in a bunch of places to lift between MonadError instances. We can instead use liftEither . first Error, which seems neater and less boilerplate-y.

Implement validation of the blockchain layer using the simplified validation rules

Test the blockchain layer validation and the ledger layer validation with

1. existing mainnet chain; and
2. executable spec and generator

Damian Nadales commented 24 Oct 2018 12:44
@nicholas.clarke wrote some constraints on the serialization function. We might need to change the rules accordingly: For instance instead of [| txbody tx |] we'd write txbody_s [[ tx ]].

nicholas.clarke commented 24 Oct 2018 16:15
I think we should just make a note about this in that document, and chalk it down to another abuse of notation.

Damian Nadales commented 24 Oct 2018 20:14
That's what I'm not sure about. We do want to specify that we shouldn't de-serialize only to obtain the serialized version of a field, but I'm not sure where. I cannot see far enough to understand how txbody_s [[ tx ]] would translate to a Haskell model.

They should explain the operational rules notation.

Include examples. For instance: examples of States, Transitions, Signals, Rules, etc.
Check compatibility with @duncan Coutts's document. If we have good reasons for deviating from the conventions used there, we should submit a PR against that document.
Specify how definitions are split in Figures: abstract types and functions, constraints, derived functions, state and transition types, and transition rules.
Define the notation for quantifications: for instance, for separating the term of a quantification do we use a regular dot, or a center dot \cdot.

Currently the golden files are bit disorganized. I plan to put all the binary golden files in test/golden/bi/* and all the json golden files in test/golden/json/*

There were recent changes in the specification of the delegation interface on the ledger layer's side. Update the blockchain layer's side accordingly.

Right now cardano-prelude exports Universum. We want to remove that dependency and instead use a different prelude library. The exact library is still up for discussion, but that discussion can hopefully continue here.

Main Goal

Model the evolution of the BlockVersionData parameters in the ledger state.

Aspects to be modeled

0. Authentication: the proposal needs to be properly signed.
1. Authorization: the proposal needs to be signed by the genesis keys or one of the delegates.
2. Voting: genesis key holders or delegates can only vote on a proposal after it is posted.
3. Voting deadlines: voting ends with a majority of the voters (4/7 if we assume no state) agree on a proposal. Bear in mind that a rule that finishes the voting period after 4/7 positive votes will succeed to validate the existing chain only if the distribution of the stake is roughly equal (which might not be the case, and we'd have to revisit this rule).
4. Block-version changes: when the voting ends, we need to update the block-chain parameters according to the proposed version.

Current subtasks

• Determine which information do we need to keep track of in the ledger state:
  • A subset of the information in BlockVersionData.
  • Something else?
• Determine whether software updates are related to protocol (BlockVersionData) updates.

References

• https://cardanodocs.com/technical/updater/
• https://cardanodocs.com/cardano/update-mechanism/
• https://github.com/input-output-hk/cardano-sl/blob/develop/docs/auxx.md#proposing-an-update
• https://github.com/input-output-hk/cardano-sl/blob/develop/wallet-new/docs/updates.md
• https://github.com/input-output-hk/cardano-sl/blob/develop/docs/proposals/update-downloader.md

Currently there are tests in Test.Cardano.Chain.Genesis.Json & Test.Cardano.Chain.Txp.Json that are not running. This issue brings the necessary types from the Byron release to make these tests run.

The legacy-free codebase will be using Ouroboros BFT, which doesn't require the complex slot leader schedule of Ouroboros classic. We still need to be able to decode blocks produced by the legacy codebase, so we imported the old SSC types into the new codebase. We can now remove them, but to do so safely we should make sure that old blocks decode at every step. This can be achieved by:

1. Adding a new testing primitive to check for a successful decoding using a given decoder
2. Write decoders for all deprecated types that mimic the operation of the Bi instances
3. Add tests for all deprecated types that decode old golden test values
4. Remove all types except SscPayload and SscProof
5. Write an encoder for an empty SscPayload that can be read by the legacy codebase

The ledger rules should adhere to the notation specified in the standard notation document.

This task simply involves going through the ledger spec and checking compatibility with the aforementioned document.

Aspects to model:

• Minimum fee (see IntersectMBO/cardano-ledger#102)
• Transaction fee
• Dependency of minimum fee on the protocol parameters

Constraints:

• fees should be modeled in a specific unit, probably Lovelace.

PR

Consequences

Retrospective

We use roundTrip as a prefix for round trip tests, so we should be consistent. This also satisfies some hlint suggestions, so it should be good.

At this moment Lovelace has no associated constraints, however we use the + operator, and we're assuming no negative balances. These assumptions should be written down explicitly in the model.

PR

Consequences

Retrospective

There are a number of issues with crypto testing:

• We should aim to replace hspec in all tests
• The binaryTests in Test.Cardano.Crypto.CborSpec can be dropped as we already use hedgehog
• If possible we could replace all QuickCheck things with hedgehog
• Examine the use of ArbitraryUnsafe, maybe it can be removed

Starting a fresh implementation is our opportunity to avoid any 'technical debt' we might have accrued in cardano-sl. A large chunk of code was imported from cardano-sl, so this epic aims to track and deal with any debt that may have been brought over.

Tag deserialized types with an annotation that allows the original bytes to be recovered.

This package will contain all the types necessary to represent and deserailise the Block and Undo types from cardano-sl. This also involves clean up of that code to bring it in line with the conventions of the legacy-free codebase.

The blockchain model should specify that this hash should correspond with the hash of the previous block.

Similarly to the removal of SSC types, we want to remove epoch boundary blocks, while maintaining compatibility with the old on-the-wire format. To do that we encode blocks, wrapped with the old tag for MainBlocks and we decode by either dropping boundary blocks or decoding MainBlocks as before.

To be able to check hashes of old style blocks, we only need to be able to hash the serialized representation of the header. We should be able to extract this using the new CBOR decoding-with-offsets work, without ever decoding to a Haskell type.

We want to run validation over the real blockchain to make sure we're not breaking anything as we move away from the Byron types, serialisation, and validation. We can imagine that the whole blockchain is in a sub-directory by using a submodule. Then tests can just read those files directly as long as the submodule has been updated.

Implement validation of the ledger layer using the simplified validation rules

This issue looks at a number of issues with cardano-binary testing:

• Should we remove Test.Cardano.Cbor.Canonicity after we stop reserializing data?
• Do we need Test.Cardano.Cbor.RefImpl?
• We should move the binaryTests in Test.Cardano.CborSpec to use hedgehog
• Should we add more/better testing to this package?

Deliverable: LaTeX and executable specifications of the blockchain and ledger layer for the (simplified) rules for the existing chain.

The aspects following aspects should be covered by the aforementioned specifications:

• Delegation
  • Witnessing
  • Epochs
  • Activation
• Updates
  • Witnessing
  • Proposal activation
  • Proposal deadline
  • Protocol parametes
• Utxo
  • Balance and fees
  • Witnessing
• Chain extension
  • Signers

The blockchain operational rules should be weaker than the Ourobouros BFT rules, so that the current Cardano implementation and the OBFT one can be validate by these.

However, we should write generators that generate OBFT compatible chains (chains generated according to the OBFT rules), and write QuickCheck (or hedgehog) properties stating that the generated chains are compatible with the OBFT chains.

We do not need in principle rules for the OBFT generators, but they might be nice to have.

In the legacy codebase we were using the Universum prelude. For a large project like this it makes sense to have a Cardano.Prelude. While importing code from the old codebase this can simply re-export Universum, but we can then easily replace this when we want.

Agree on how to pass delegation information between ledger and blockchain layers.

Haskell implementation of the spec for the ledger code,

Not all tests should always be run. CI, developers, and QA all have different concerns, so we should design the tests to take that into account. This could be done by adding an argument to the test executable that tells us what situation we're in. Development should be the default, so stack test runs a reasonable set of development tests. CI and QA can then have special invocations to run more comprehensive or long-running tests, or e.g. adjust sizing parameters to generators.

The blockchain rules should adhere to the notation specified in the standard notation document.

This task simply involves going through the blockchain spec and checking compatibility with the aforementioned document.

There are makefiles inside cardano-chain/specs/ledger/latex/ and cardano-chain/specs/chain/latex/ which build pdfs. It would be nice to check these builds as a part of CI.

We're using -Weverything in cardano-binary and cardano-crypto-wrapper, but not cardano-chain yet.