Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

adding missing DELEG predicate failures to spec #1725

Merged
merged 1 commit into from
Jul 28, 2020

Conversation

JaredCorduan
Copy link
Contributor

The formal spec listed only 7 predicate failures for the DELEG rule, but the implementation contained 11 (which did include the 7).

  • The predicate StakeKeyInRewards should actually be removed. It is redundant with StakeKeyAlreadyRegistered (we removed the stkCreds mapping from the implementation in remove stkcreds and stpools #1683 and from the spec in Remove the now irrelevant maps stkCreds and stpools from the formal spec #1692, making the reward mapping the source of truth for registered stake credentials). Unfortunately, we are using StakeKeyInRewards in the place where StakeKeyAlreadyRegistered is the more helpful name. I have made a TODO in the implementation to replace StakeKeyInRewards with StakeKeyAlreadyRegistered when there is a good time (right now is not).
  • I added StakeKeyNonZeroAccountBalance, MIRCertificateTooLateInEpoch, and DuplicateGenesisVRF to the spec.

closes #1719

@nc6 nc6 merged commit 3c9faf9 into master Jul 28, 2020
@iohk-bors iohk-bors bot deleted the jc/formal-spec/add-missing-deleg-predicate-failures branch July 28, 2020 06:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

DELEG Predicate Failure Inconsistency Between Formal and Executable Specs
2 participants