search

IntersectMBO / cardano-ledger

The ledger implementation and specifications of the Cardano blockchain.
Apache License 2.0
250 stars 157 forks source link

Conway conformance track #4427

Open aniketd opened 2 weeks ago

aniketd commented 2 weeks ago

Tracking issue for Conway conformance

Here we attempt to consolidate coverage for all testable rule transitions, starting from the "leaves" of the transition graph.

For each of the rules below, we should follow these steps:

  1. Plumbing the test to pass type-checking and compilation, but tests fail - so we mark them pending, by xprop, xit , xdescribe, etc.
  2. Translate. Make the translations between the types as complete as possible. Related issue: https://github.com/IntersectMBO/cardano-ledger/issues/4254
  3. Adjust the constrained-generators to precisely capture exact structural and interrelational requirements for inputs, only. Remember that the conformance tests should allow all inputs that do and do not result in PredicateFailures, so that the implementation and specification agree on when to pass and when to fail, identically.
  4. Review by a team member other than the one who adjusted the generators. The reviewer should pay particular attention to whether the generators are over constrained and also whether the translations are omitting something important.

The "levels" are ordered by their dependencies.

Some more TODO are captured here https://github.com/IntersectMBO/cardano-ledger/issues/3914, but we can use this issue to track them all. Please feel free to edit this issue to keep it up-to-date.

NOTE: In order to work on an item, convert it to an issue and assign it to yourself.

Blocks branch

Level 1
Level 2
Level 3
Level 4

Ticks branch

Level 1
Level 2
Level 3
Level 4

How-to


  Everything under src/Ledger/Foreign/ is important, it pays to be
  familiar with it, as all the intermediate data-types and rule-runners
  are defined there. The translations import the common data types qualified
  under an `F` for Foreign.

AGDA 
-------------- conformsToImpl: read and understand -----------------------------
HASKELL 

  In each of our haskell modules, mostly,
    we import
      from cardano-ledger-executable-spec
        - module `Lib` qualified under the name `Agda`
          - This gives us the intermediate/common data-types that we need to 
            translate our Haskell types to
      from constrained-generators
        - module `Constrained` to use the constrained generators framework
          - This is just to generate the values to run the tests
      from cardano-ledger-conformance
        - module `Test.Cardano.Ledger.Conformance` for the classes we need to 
          make instances for
          - class ExecSpecRule
            - Implement everything you need by understanding the data 
              dependencies between the env, state and signal for a given rule
          - class SpecTranslate
            - Implement the translations from Haskell data types to 
              Agda/intermediate/common data-types
        - These classes form the test framework that we should write our 
          conformance tests using
      from cardano-ledger-test
        - module `Test.Cardano.Ledger.Constrained.Conway` 
          - to get the constrained generators already written by 
            @Max for most of the rules