input-output-hk / cardano-ledger-byron

A re-implementation of the Cardano ledger layer, replacing the Byron release
52 stars 13 forks source link

Violation of `ts_chainTick` property #743

Closed nc6 closed 4 years ago

nc6 commented 4 years ago

https://hydra.iohk.io/build/1932311/nixlog/4 shows us a failure of ts_chainTick property. I can successfully replicate this failure.

ts_chainTick is a property which states that, within the usual 2k-slot window, "ticking" the chain (e.g. applying the EPOCH transition and updating the delegation map, for Byron) is not affected by intermediate states - e.g. the ticks n -> n2 and n -> n1 -> n2 should be equal, for slots n < n1 < n2. Seen another way, this property expresses the idea that the chain state should not be sensitive to which specific slots are occupied.

The above test failure shows that, for Byron, this property doesn't hold. In particular, it fails in the following circumstance. Suppose the epoch length is 10, k = 5 and the number of endorsements needed for an update proposal is just 1:

If the first block arrives in slot 11, then only version 0.1 will be available, and will get adopted. If the first block arrives in slot 12, then both versions will be available, and the one to get adopted depends on the order in which they are inserted into fads.

We can resolve this by doing the epoch transition not with the current (e.g. that of the current block) slot, but with the first slot of the new epoch, regardless of the slot in which the current block arrives.

nc6 commented 4 years ago

Actually realised that this will be vital for the hard fork, because as it is we cannot satisfy the "safe zone" at all.

dcoutts commented 4 years ago

Is this critical for the Byron release or if it's about the hard fork then is it only critical for the Shelley release? Or is the concern that if we have any update proposals in the meantime, we might diverge?

nc6 commented 4 years ago

This is critical for the hard fork, and medium priority for Byron