Fix error in Shelley Spec regarding new pool count #2623
Conversation
The implementation was doing the correct thing. closes #2587
eras/shelley/formal-spec/utxo.tex
Outdated
| & ~~~\where \\ | ||
| & ~~~~~~~ \var{newPools} = \{\var{certs}\cap\DCertRegPool ~\mid~ \cwitness{c}\notin \var{poolParams}\} | ||
| & ~~~~~~~ \var{newPools} = \{c ~\mid~ \var{certs}\cap\DCertRegPool,\cwitness{c}\notin \var{poolParams}\} |
There was a problem hiding this comment.
I don't understand this line. Is c supposed to be an element of certs ∩ DCertRegPool? The old version doesn't make sense to me either btw.
There was a problem hiding this comment.
ah yes, it is supposed to be c \in \var{certs}\cap\DCertRegPool.
There was a problem hiding this comment.
and the extra c \in totally breaks the table spacing/corners now 😆 😭 hopefully tx is a suitable abbreviation for transaction, that lets me reclaim the white space back
| \sum\limits_{\wcard\mapsto c\in\var{pr}\circ\var{rewardAcnts}^{-1}(a)} c | ||
| \mathrel{\Bigg|} | ||
| a\in\range{rewardAcnts} | ||
| \right\} \\ |
There was a problem hiding this comment.
I think what you want is a \mapsto \sum\limits_{c\in\var{pr}(\var{rewardAcnts}^{-1}(a))} c:
- currently,
rewardAcnts'is just a set of numbers \var{rewardAcnts}^{-1}(a)is a set of hashes, so you can only apply it topr, not compose it with, which will give you a set of numbers
Also, I think the | looks a bit better if it's just Big. Finally, I think \sum\var{pr}(\var{rewardAcnts}^{-1}(a)) is a nice point-free version of the sum, but pick whichever one you like better.
There was a problem hiding this comment.
you're totally right! I had meant for rewardAcnts to be a mapping. thanks!
There was a problem hiding this comment.
your point free version is very clean, I love it, I've changed to using it
Two small changes the Shelley spec (where the code was doing the correct thing).
newPoolsis counting certificates, but should be counting unique pool ids.POOLREAPrule, we were not accounting for the fact that multiple retiring pools could have the same stake address. the old version used:the new version uses:
closes #2517
closes #2587