Add an initial formal specification

[javierdiaz72]

This PR adds an initial version of a formal specification. This version includes the relevant material from the Shelley and Babbage ledger specs, plus the following fixes:

1. There is an oversight in the Decentralized rule in Fig. 68 of the Shelley ledger spec, namely that no environment was passed in the call to the OCERT transition system.
2. The OCERT rule has a new predicate failure: We newly require (in the context of Fig. 66 in the Shelley ledger spec) the condition n ≤ m + 1, a violation of which corresponds to a CounterOverIncremented failure.
3. There is an error in Fig. 69 of the Shelley ledger spec: Instead of ℙ PrtclEnv, it should be PrtclEnv.
4. There is an error in Sec. 12.13 of the Shelley ledger spec: Instead of "It calls BHEAD, PRTCL, and BBODY as sub-rules." it should be "It calls TICK, TICKN, PRTCL, and BBODY as sub-rules."; and similarly in the introduction paragraph of Sec. 12.
5. The former VRFKeyBadLeaderValue and VRFKeyBadNonce failures are replaced by the new single VRFKeyBadProof failure.

See https://ci.iog.io/job/IntersectMBO-ouroboros-consensus/pullrequest-982/x86_64-linux.native.consensus-pdfs/latest/download/1/consensus-spec.pdf for a rendered version of the latest state of the PDF in this PR.

[javierdiaz72]

Note: No integration with Nix is added yet so, in order to build the PDF file, you need to:

1. Install the latexmk package.
2. Run make.

[jorisdral]

One nice follow-up for this work would be to have GHA render and upload this doc to the github-pages website

[amesgen]

Rendered pdf for this PR: https://ci.iog.io/job/IntersectMBO-ouroboros-consensus/pullrequest-982/x86_64-linux.native.consensus-pdfs/latest/download/1/consensus-spec.pdf

[javierdiaz72]

FTR: The following is the list of changes to be included in the next iteration of the spec, according to what was discussed during the mob review:

1. Remove all references to block bodies
2. Remove the BBODY transition system (and, consequently, remove the LEDGERS transition system from the Common Interface section)
3. Replace the CHAIN transition system with the CHAINHEAD transition system, and, consequently: 3.1. Add the NEWEPOCH transition system to the Common Interface section 3.2. Remove the TICK transition system from the Common Interface section
4. Keep the Properties section but add a reference to the CHAIN transition system in the Ledger spec

[javierdiaz72]

FTR: There are two mistakes in Fig. 11 of the Babbage spec: It should say bhbody bh instead of bheader bh and bnonce bhb instead of bnonce (bhbody bhb). I'll include appropriate fixes in the upcoming iteration of the spec.

[javierdiaz72]

FTR: There are two mistake in Fig. 75 of the Shelley spec: It should say (e2, _, bcur, es, _, pd) instead of (e2, _, bcur, es, _, _, pd) and bhash bhb instead of bhash bh. I'll include appropriate fixes in the upcoming iteration of the spec.

[javierdiaz72]

Please find a new version of the spec ready for review at 7e885c501644710bd6a0a11e1c791c396828e2ae. This version includes the changes mentioned in the last 3 comments.

[jasagredo]

I'm going to dump here some questions that I got when reading the PDF. After I'm done with the read, I will put these comments if applicable in the exact source code lines they refer to.

Section 1.1: New epoch transition

• I would add the name of the rule to the header of the section.
• From the point of view of the Consensus layer, are the details of the transition that happens in the new epoch transition irrelevant or why is only the type shown?
• Why is this one defined before presenting the diagram of rule dependencies, or rather why is this one here and the other rules after the diagram?

Section 2: Transition rule dependencies

• This is very different from the diagram in the shelley specs, why? In particular TICKF is not shown in the shelley diagram.
• There are no recursive rules in this diagram, shouldn't we remove that explanation?

Section 3.1: Block definitions

• I find it confusing that sometimes b means block, sometimes block body. Same with vrf, sometimes it appears sometimes it doesn't. I think we should either expand the prefix or make it unique. In particular I propose:
  • Block Header Body
    • prev -> prevHeader
    • vk -> issuerVk
    • blockno -> blockNo
    • prf -> vrfPrf
    • bsize -> bodySize
    • bhash -> bodyHash
  • Abstract functions
    • bhHash -> headerHash
    • bHeaderSize -> headerSize
  • Accessor functions
    • bheader -> blockHeader
    • hsig -> headerSig
    • bhbody -> headerBody
    • I would list first blockHeader, headerSig and headerBody
    • As we are ignoring the block body, the prefix body is not confusing (as it could be between block body and block header body), so I also suggest prefixing the rest of functions with body, so bslot -> bodySlot, bVrfRes -> bodyVrfRes, etc.
    • Also all these functions can be composed with headerBody to give types ${\tt BHeader} \rightarrow {\tt X}$ so it would also be plausible to say headerSlot instead of bodySlot.
    • TODO: present a screenshot of what I mean

Section 3.2: Tick Nonce Transition

• I see that nonce and seed is used interchangeably, why is this? Couldn't we set with one?
• Reference to figure is broken. Says Fig 3.2 but does not exist.
• I would add the rule name in the header of the section for clarity.

Section 3.3: Update Nonce Transition

• I would add the rule name in the header.
• nonce candidate -> candidate nonce
• I would not put the explanation for the entropy in parenthesis. I find it relevant.

Section 3.4: Operational certificate transition

• I would add the rule name in the header
• Could annotate the predicate failures with numbers, for later correlating with the list of failures $$c_0 \overset{(1)}{\leq} {\tt kesPeriod~} s$$

Section 3.5: Verifiable Random Function

• VRF helper functions in the figure.
• hashKey is used without it being defined anywhere.
• Where is verifyVrf_seed defined?

Section 3.6: Protocol transition

• Add rule name in header
• Typo: canditate -> candidate
• slot is undefined, I imagine there should be a $slot := {\tt bslot~} bhb$
• Failures could be numbered in the transition diagram.
• I wonder if the failures described here are not actually failures of the VRF function instead?
• What happens if failures happen in the inner OCERT rule? don't failures bubble up?

Section 3.7: Tick forecast transition

• Add rule name in header
• Here we destructure the NewEpochState, but this product type was never defined. Same with EpochState, ds which I imagine is DelegationState or some such, the type of fGenDelegs and genDelegs.
• This might be just my lack of knowledge, but what does $\overset{\cup}{\rightarrow}$ mean?

Section 3.8 Chain Head Transition

• Add rule name in header
• Could failures be numbered also here?
• Figure 16: acnt and ls are unused, aren't they?

[jasagredo]

Comments on properties:

• 4.1: Isn't it clearer to say that as $s \rightarrow s'$, then $\tilde{s} \rightarrow \tilde{s}'$ instead of $s''$?
• 4.2: in the explanation you say initial state s but then nes appears, probably just missing a s = (nes, \tilde{s}) or some such? It is known by the context, but still.
• 4.2: You mention the BBODY rule, which I guess is also defined in SL-D5?
• I did not quite understand property 4.2.

[javierdiaz72]

During today's Consensus Office Hours meeting, we discussed about the interface between the consensus spec and the ledger spec. Here's the big-picture structure we've come up with (thanks @WhatisRT):

Interface
- Block
- BBodyEnv -> PParams (in Conway, have TriggerHF action)
- BBodyState (LState abstract?)
- NewEpochState (possibly abstract?)
- Slot


                  (BBODY, TICK, ...)
                /---- Ledger <------\
Interface Lib <-                     -- Node (CHAIN)
                \---- Consensus <---/
               (TICKF, CHAINHEAD, ...)

[javierdiaz72]

FTR, the following change will be included in the next iteration of the spec: The removal of the $extraEntropy$ in the $\mathsf{TICKN}$ rules as dictated by the Babbage spec makes the inclusion of $pp$ in the environment useless, so it should be removed.

[javierdiaz72]

Hi, @jasagredo! Please find below my responses to your review comments:

Section 1.1: New epoch transition

• I would add the name of the rule to the header of the section.

Fixed in 940560c8a514f6ba2e6277863fd944a2c17d42ad.

• From the point of view of the Consensus layer, are the details of the transition that happens in the new epoch transition irrelevant or why is only the type shown?

IMO, the details should be irrelevant to the Consensus layer since those are regarded as implementation details.

• Why is this one defined before presenting the diagram of rule dependencies, or rather why is this one here and the other rules after the diagram?

Fixed in 940560c8a514f6ba2e6277863fd944a2c17d42ad.

Section 2: Transition rule dependencies

• This is very different from the diagram in the shelley specs, why? In particular TICKF is not shown in the shelley diagram.

This diagram includes only the transition systems (and their dependencies) related to the Consensus layer.

• There are no recursive rules in this diagram, shouldn't we remove that explanation?

Fixed in baa85e5813f089396491d3aa2c233ce6fa750b97.

Section 3.1: Block definitions

• I find it confusing that sometimes b means block, sometimes block body. Same with vrf, sometimes it appears sometimes it doesn't. I think we should either expand the prefix or make it unique. In particular I propose:

  * Block Header Body
  
    * `prev` -> `prevHeader`
    * `vk` -> `issuerVk`
    * `blockno` -> `blockNo`
    * `prf` -> `vrfPrf`
    * `bsize` -> `bodySize`
    * `bhash` -> `bodyHash`
  * Abstract functions
  
    * `bhHash` -> `headerHash`
    * `bHeaderSize` -> `headerSize`
  * Accessor functions
  
    * `bheader` -> `blockHeader`
    * `hsig` -> `headerSig`
    * `bhbody` -> `headerBody`
  

Fixed in 659cd85013d6be52f31951120c54472bf2c569ec.

• I would list first blockHeader, headerSig and headerBody

Actually they are already listed in that order: The list is read from left to right.

• As we are ignoring the block body, the prefix body is not confusing (as it could be between block body and block header body), so I also suggest prefixing the rest of functions with body, so bslot -> bodySlot, bVrfRes -> bodyVrfRes, etc.

I agree about the inconsistency in the use of the prefixes. However, the problem I see with the prefix $body$ is that it's confusing when used for the fields $bodySize$ and $bodyHash$ (e.g., $bodyBodySize$ looks weird). Therefore, I prefer to choose your second option, i.e., use a unique prefix.

• Also all these functions can be composed with headerBody to give types BHeader→X so it would also be plausible to say headerSlot instead of bodySlot.

That's true, however these functions are mostly used when only header bodies are available.

Section 3.2: Tick Nonce Transition

• I see that nonce and seed is used interchangeably, why is this? Couldn't we set with one?
• Reference to figure is broken. Says Fig 3.2 but does not exist.
• I would add the rule name in the header of the section for clarity.

Fixed in 7bd1fdf51affb38f2728681fdf2816614df63b46.

Section 3.3: Update Nonce Transition

• I would add the rule name in the header.
• nonce candidate -> candidate nonce
• I would not put the explanation for the entropy in parenthesis. I find it relevant.

Fixed in b9f53081074b943d9151fdd718b1c8aa4d35bdb2.

Section 3.4: Operational certificate transition

• I would add the rule name in the header
• Could annotate the predicate failures with numbers, for later correlating with the list of failures $$c_0 \overset{(1)}{\leq} {\tt kesPeriod~} s$$

Fixed in f4b8ec5e96082c88935770a84e173b7d4d65de84.

Section 3.5: Verifiable Random Function

• VRF helper function_s_ in the figure.

Fixed in 2d69d91d4371601cf145b6f56f0f0f71d9e10129.

• hashKey is used without it being defined anywhere.
• Where is verifyVrf_seed defined?

These are currently defined in the ledger spec but should be included in the new "base" (or "library") spec, see https://github.com/IntersectMBO/ouroboros-consensus/pull/982#issuecomment-2077689225.

Section 3.6: Protocol transition

• Add rule name in header
• Typo: canditate -> candidate
• slot is undefined, I imagine there should be a slot:=bslot bhb
• Failures could be numbered in the transition diagram.
• I wonder if the failures described here are not actually failures of the VRF function instead?
• What happens if failures happen in the inner OCERT rule? don't failures bubble up?

Fixed in 84510796dcda3d95b9c85fcc0b0c8f7d16a662a9.

Section 3.7: Tick forecast transition

• Add rule name in header

Fixed in 19468102df496977ee943787c1196543f1a9e5d8.

• Here we destructure the NewEpochState, but this product type was never defined. Same with EpochState, ds which I imagine is DelegationState or some such, the type of fGenDelegs and genDelegs.

These are currently defined in the ledger spec but should be included in the new "base" (or "library") spec, see https://github.com/IntersectMBO/ouroboros-consensus/pull/982#issuecomment-2077689225.

• This might be just my lack of knowledge, but what does →∪ mean?

It's the union override right operator on maps, that is, union on maps with a bias towards the right operand in case of key clashes. This is currently defined in the ledger spec.

Section 3.8 Chain Head Transition

• Add rule name in header
• Could failures be numbered also here?
• Figure 16: acnt and ls are unused, aren't they?

Fixed in bc6f767b4851149f3b8bd996c0a8eee695ba16c8.

Comments on properties:

• 4.1: Isn't it clearer to say that as $s \rightarrow s'$, then $\tilde{s} \rightarrow \tilde{s}'$ instead >of $s''$?
• 4.2: in the explanation you say initial state s but then nes appears, probably just missing a s >= (nes, \tilde{s}) or some such? It is known by the context, but still.
• 4.2: You mention the BBODY rule, which I guess is also defined in SL-D5?

Fixed in 70a46f3d315c84100dac900c84dae56d2983a78e.

• I did not quite understand property 4.2.

I understand it as a sort of converse of Property 4.1.

[javierdiaz72]

FTR, the following change will be included in the next iteration of the spec: The removal of the extraEntropy in the TICKN rules as dictated by the Babbage spec makes the inclusion of pp in the environment useless, so it should be removed.

Fixed in 7c07c27880cfc4eda58b21a7a932316ce9d55562.

[javierdiaz72]

Hi, team! We now have an improved version of the spec which is quite close to the code. Could you please review it? Thanks!

[jasagredo]

I think all my concerns above were resolved and/or answered. Thanks Javier!

[javierdiaz72]

Note: f9b03fa9e62968d4a278e6b48bb5763f0c2d7602 fixes a mistake found originally in the Babbage spec (see https://github.com/IntersectMBO/cardano-ledger/pull/4287#issuecomment-2098975761).

[javierdiaz72]

I think all my concerns above were resolved and/or answered. Thanks Javier!

That's great to hear, thank you, @jasagredo ! Could you perhaps give your approval to this PR?

[javierdiaz72]

Hi, Team! Are you satisfied with the spec or is there still anything preventing this PR from being merged?

[amesgen]

Ah, the only thing was that the commits aren't signed (which is required). I rebased and squashed, should now enter the merge queue once CI passed :+1: