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

Require that LedgerView family is empty #355

Closed
wants to merge 1 commit into from

Conversation

nfrisby
Copy link
Contributor

@nfrisby nfrisby commented Sep 19, 2023

Enforcing this property as in this PR is not actually necessary, but we suspect it may prevent a good deal of confusion.

@nfrisby
Copy link
Contributor Author

nfrisby commented Sep 19, 2023

This relatively large diff emerges from merely adding the invariantLedgerViewEmpty :: Proxy p -> LedgerView p -> a method to the ConsensusProtocol class. Everything else is a consequence of that---no other major decisions were made.

I had originally planned to declare data LedgerView p itself as an empty data type. However, our protocol combinators (eg ModChainSel p s) currently rely on LedgerView (ModChainSel p s) ~ LedgerView p, and that would be impossible with an injective LedgerView.

Copy link
Contributor Author

@nfrisby nfrisby left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the major alternative to this approach is to replace all occurrences of Ticked (LedgerView p) with LedgerView p.

Perhaps renaming it to TickedLedgerView p?

@@ -188,27 +191,24 @@ forgePBftFields contextDSIGN PBftIsLeader{..} toSign =
Information PBFT requires from the ledger
-------------------------------------------------------------------------------}

newtype PBftLedgerView c = PBftLedgerView {
-- | ProtocolParameters: map from genesis to delegate keys.
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I should have kept this haddock comment

@@ -438,7 +440,7 @@ append PBftConfig{} PBftWindowParams{..} =
-- avoid space leaks.
data PBftValidationErr c
= PBftInvalidSignature !Text
| PBftNotGenesisDelegate !(PBftVerKeyHash c) !(PBftLedgerView c)
| PBftNotGenesisDelegate !(PBftVerKeyHash c) !(Ticked (PBftLedgerView c))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the only aspect of the diff that I anticipate trickling down into eg cardano-node.

@amesgen
Copy link
Member

amesgen commented Sep 20, 2023

Another idea: push the evidence that LedgerView is empty into a superclass constraint instead of into a new member function, eg a simple Generic-based assertion that it has no constructors, or reusing sth like the existing Absurd class (already has Generic deriving).

@nfrisby nfrisby changed the title Requiring that LedgerView family is empty Require that LedgerView family is empty Sep 22, 2023
@nfrisby
Copy link
Contributor Author

nfrisby commented Oct 10, 2023

I much prefer this alternative idea #363, so I'm Closing this.

@nfrisby nfrisby closed this Oct 10, 2023
@amesgen amesgen deleted the nfrisby/empty-LedgerView branch October 10, 2023 12:57
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.

None yet

2 participants