Epoch Transition Formal Spec <-> Executable Spec Discrepancies

[xenocidewiki]

Found a couple of issues regarding Epoch.hs in the executable spec, and pages 55-56 in the formal spec.

• It is mentioned that "votedValue is only well-defined if Quorum is greater than half thenumber of core nodes, i.e. Quorum>|genDelegs|/2" -> I could not find such a check anywhere in the code.

• The formal spec function votedValue is named votedValuePParams in the code (L79). The code also implements the function using 3 parameters as opposed to 1 (as specified in the formal spec).

  • This function in the code uses the parameter types "PParams" as opposed to "PParamsUpdate" as defined in the formal spec.
  • The function is used on L129 in the code and takes ppup (should be pup, look comment below), pp, and quorumN. -> Is it not better to make the function use 1 parameter just like in the formal spec, grab the quorumN value from inside votedValue, and use the "union override right" infix function just like the spec defines it in Fig. 45? I believe the functionality should be the same.

• On L128 of the code we are reading the utxo state and getting ppup, this should be pup because that's what utxo state contains, and according to the formal spec this is also what we are getting, seems like a small typo.

  • This is further reflected in the votedValue helper function, where the parameter is propagated as ppup.
  • The formal spec says that we read pup from utxoSt' not utxoSt -> the code seems wrong in this case, where the ' is missing.

Some questions:

• What is the NonMyopic value in the EpochState? This is not reflected in the formal specification.
• In Fig. 44 you specify votedValue to return p if one exists in the range of pup (specified as vs) such that a consensus is met (vote count is >= quorum). In the code however you only return "p" if the length of consensus is 1, otherwise you return Nothing. Perhaps I have difficulties interpreting the code, but is a possibility of the length of consensus being >1 ? In which case a p would exist, but the length of the consensus variable would be more than 1 and the function would return Nothing despite the formal spec condition being satisfied.

[JaredCorduan]

thank you for raising all of this @xenocidewiki !

It is mentioned that "votedValue is only well-defined if Quorum is greater than half the number of core nodes, i.e. Quorum>|genDelegs|/2" -> I could not find such a check anywhere in the code.

There is currently no check for this, but I agree that it makes sense to add one. Quorum is a global constant (it will be 5 for shelley mainnet), and as such we should have the function that validates a genesis config (named validateGenesis in Shelley.Spec.Ledger.Genesis check this property.

The formal spec function votedValue is named votedValuePParams in the code (L79). The code also implements the function using 3 parameters as opposed to 1 (as specified in the formal spec).

I propose we change the name of the function to votedValue in the implementation, and change the definition of votedValue in the spec to take all threes parameters and include the union override right operation. In the formal spec, the "union override right" is done outside of votedValue, whereas in the implementation, it is done inside. Note that the use of union override right is a bit of an abuse of notation, since we are doing this operation on a record type and not a finite map (but should hopefully be clear otherwise). In other words, updatePParams is the union override right in the implementation. (I think this also addresses all the sub-bullet points you raised).

On L128 of the code we are reading the utxo state and getting ppup, this should be pup because that's what utxo state contains, and according to the formal spec this is also what we are getting, seems like a small typo.

yes indeed, I will change the implementation to use pup in both the STS rule here and as parameters to votedValue.

The formal spec says that we read pup from utxoSt' not utxoSt -> the code seems wrong in this case, where the ' is missing.

It actually doesn't matter if we use utxoSt or utxoSt', since POOLREAP does not mutate pup. But it is probably much less error prone to use utxoSt' (as you suggest) in case this were to change. And in any case, the formal spec and the implementation should agree.

What is the NonMyopic value in the EpochState? This is not reflected in the formal specification.

This will be addresses by #1319, I just haven't had any time to get to it, but hope to do so very soon. Note that this data is entirely independent of any chain validation, and is only used for pool ranking by wallets.

... consensus is 1 ...

Yes, this is a bit akward in the haskell code. If the global constant Quorum is greater than half the number of core nodes (the number of core nodes is also fixed), then it is always true that either there is exactly one agree upon value, or there is not consensus. The list consensus should always (otherwise there is a bug) either be empty or have size 1.