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

Add a SlotUpkeep type to enforce dependencies between rules #75

Merged
merged 5 commits into from
Nov 19, 2024

Conversation

WhatisRT
Copy link
Collaborator

@WhatisRT WhatisRT commented Nov 18, 2024

We want to ensure that the Slot rule only fires if all our block production duties are completed. To do this, I've added a set that keeps track of these to the state and adjusted the rules so that they can only fire one per slot. Then, Slot checks that all duties are indeed completed. This means that if we can't produce anything, we still need to update the state to not get stuck, which is why there are now negative versions of some rules.

While doing this, I noticed that we're not keeping the state of the base chain in our state and instead always universally quantifying over all those states. I fixed that too.

Copy link
Member

@yveshauser yveshauser left a comment

Choose a reason for hiding this comment

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

lgtm (just the small thing mentioned above)

formal-spec/Leios/SimpleSpec.agda Outdated Show resolved Hide resolved
@WhatisRT WhatisRT merged commit 663a541 into main Nov 19, 2024
4 checks passed
@WhatisRT WhatisRT deleted the andre/add-upkeep branch November 19, 2024 11:54
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.

2 participants