Conformance tests against formal specification

[dnadales]

Why

As part of MS4.5 - Formal Specification and Conformance Tests, we need to achieve the following:

1. Develop Node Conformance Tests against the Leios formal specification.
2. Document the procedure for running these tests and interpreting their results.

What

To this end, a possible approach is to input a node trace to the Leios trace verifier to determine the node's conformance with the Leios formal specification.

How

• Translate traces between Cardano Tracer and Leios trace verifier #593
• Improve semantics of the verifier to ensure conformance to the Leios spec
• Define set of "things" a node would do to give us decent coverage of the spec

[javierdiaz72]

Regarding "Next steps" in the description:

The JSON format of the trace log file that the trace verifier expects is described here.

As described in the link above, each trace log event has the following format:

{
  "message": …
, "time_s": …
}

where the value of message contains the information about the specific trace event, and the value of time_s is a timestamp.

The only trace events that seem relevant to a Praos node are the following:

• Slot: Emitted whenever a slot ends. Its format is the following:

  {
    "type": "Slot"
  , "node": "…" 
  , "slot": … 
  }

  where the value of node is the node ID and the value of slot is the slot number in which the event was emitted.

• RBGenerated: Emitted whenever a slot leader generates a ranking block (i.e., a Praos block). Its format is the following:

  {
    "type": "RBGenerated"
  , "producer": "…"
  , "slot": … 
  , "id": "…"
  , "endorsement": null
  , "parent": "…"
  , "size_bytes": …
  , "tx_payload_bytes": …
  }

  where the value of producer is the node ID, the value of slot is the slot number in which the event was emitted, the value of id is the block ID, the value of parent is the ID of the parent block (or null if no parent block exists), the value of size_bytes is the total size of the block (in bytes), and the value of tx_payload_bytes is the size of the block payload (in bytes).

• RBReceived: Emitted whenever a node receives a ranking block. Its format is the following:

  {
    "type": "RBReceived"
  , "recipient": "…"
  , "id": "…"
  }

  where the value of recipient is the node ID and the value of id is the ID of the received block.

Example of a trace log file:

{"message":{"type":"RBGenerated","slot":0,"producer":"node-0","id":"123","endorsement":null,"parent":null,"size_bytes":1025,"tx_payload_bytes":0},"time_s":0}
{"message":{"type":"Slot","node":"node-0","slot":0},"time_s":0}
{"message":{"type":"Slot","node":"node-1","slot":0},"time_s":0}
{"message":{"type":"RBReceived","recipient":"node-1","id":"123"},"time_s":0}
{"message":{"type":"Slot","node":"node-0","slot":1},"time_s":0.1}
{"message":{"type":"Slot","node":"node-1","slot":1},"time_s":0.2}

[ch1bo]

Can we scope this item so it makes sense to be done as a first step on conformance tests, with the goal to demonstrate something by end of November for example.

Concretely this could mean that we take a trace from the prototype and feed it into the formal model's trace verifier. Which might fail, depending on how far the prototype progressed.