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

More progress on completing the trace monad rule set #696

Merged
merged 11 commits into from
Feb 21, 2024

Conversation

corlewis
Copy link
Member

This extends the rule sets for the various monad properties (no_trace, no_fail, etc.) to cover all of the monad primitives that we have. It does not touch the RG rule set.

@corlewis corlewis added the multicore anything related to multicore verification label Nov 14, 2023
@corlewis corlewis self-assigned this Nov 14, 2023
Copy link
Member

@lsf37 lsf37 left a comment

Choose a reason for hiding this comment

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

I'm glad we're doing this. These rules would be so much pain to discover and add incrementally during the proofs, and it would lead to a complete mess.

This is a relatively trivial definition, but it makes rules easier to
write and to instantiate.

Signed-off-by: Corey Lewis <[email protected]>
This adds rules for trace monad specific functions

Signed-off-by: Corey Lewis <[email protected]>
@corlewis corlewis merged commit 5fa95ea into seL4:master Feb 21, 2024
12 of 13 checks passed
@corlewis corlewis deleted the trace_more_rules branch February 21, 2024 04:59
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
multicore anything related to multicore verification
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants