Type mismatch present in the ShelleyMA/Shelley formal specs when calculating the stake relation in the Rewards and the Epoch Boundary #2174
Labels
Comments
yellowtides
changed the title
yellowtides
changed the title
JaredCorduan
pushed a commit
that referenced
this issue
Jun 16, 2021
The reward mapping does not have keys that are wrapped in the stake address constructor. See github issue #2174
|
closed by #2341 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In figure 7 of the ShelleyMA formal spec, in the calculation of the stake relation, there seems to be a composition performed between
stakeCred_r^{-1}andrewards.In figure 5 of the Shelley formal spec, we see that
stakeCred_ris a map fromAddrtoCred. This would imply thatstakeCred_r^{-1}is a map fromCredtoAddr.In figure 21 of the Shelley formal spec, we see that
rewardsis a map fromCredtoCoin.Since this is the case (and that we define the composition of two maps, one of type A -> B, and the other B -> C as a resulting map of type A -> C), it would not make sense to compose
stakeCred_r^{-1}(which is of typeCred -> Addr) withrewards(which is of typeCred -> Coin). This composition (and mismatch) seems to also be present in the Shelley spec.The executable spec seems to be implementing the stake relation calculation correctly, ignoring
stakeCred_r^{-1}(and the composition) entirely, unionising the left side with just therewards.The text was updated successfully, but these errors were encountered: