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.

Sign up for GitHub

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

Jump to bottom

Monads: resync trace monad with nondet #782

Merged
merged 1 commit into from
Jul 17, 2024
Merged

Monads: resync trace monad with nondet #782

merged 1 commit into from
Jul 17, 2024

Conversation

corlewis
Copy link
Member

@corlewis corlewis commented Jul 9, 2024

Some local changes I had that I forgot to add to #765. Now that I'm not removing these lemmas from the Nondet Monad, the Trace Monad should have them as well.

@corlewis corlewis self-assigned this Jul 9, 2024
lsf37
lsf37 reviewed Jul 9, 2024
View reviewed changes
lib/Monads/trace/Trace_More_RG.thy Outdated
Comment on lines 141 to 143
lemma gets_inv_rg[simp]:
"\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> gets f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
by (simp add: gets_def, wp)
Copy link
Member

Choose a reason for hiding this comment

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

Do we want to replicate the simp/iff etc attributes in the trace monad? Might be our chance for getting a cleaner setup on the trace side.

Copy link
Member Author

Choose a reason for hiding this comment

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

Good point, although in that case I'd be tempted to remove these inv rules again. In these cases the standard wp rules should be fine, if not better.

lsf37
lsf37 reviewed Jul 9, 2024
View reviewed changes
lib/Monads/trace/Trace_RG.thy Outdated
Comment on lines 365 to 366
lemma return_inv_rg[iff]:
"\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> return x \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>"
Copy link
Member

Choose a reason for hiding this comment

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

If we decide to not do the attributes, this is another one

lsf37
lsf37 approved these changes Jul 9, 2024
View reviewed changes
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.

Looks good, modulo the simp/iff attribute question. I think I'd prefer to try without, but am open to arguments.

Xaphiosis
Xaphiosis approved these changes Jul 10, 2024
View reviewed changes
Copy link
Member

@Xaphiosis Xaphiosis left a comment

Choose a reason for hiding this comment

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

Looks good. Not quite following what Gerwin's saying about the attributes, but it sounds like a good idea.

@corlewis
Copy link
Member Author

Looks good. Not quite following what Gerwin's saying about the attributes, but it sounds like a good idea.

Roughly, my interpretation of it is that these lemmas being [simp] and [iff] is very old and not how we would want it if were doing it all now, since it can lead to unexpected behaviour when simplifying. It's probably not worth fixing in the existing proofs, where we have sometimes accidentally depended on that behaviour, but it probably is worth improving how the trace monad is setup. This does have trade-offs, in particular with there being even more breakages when the existing proofs are moved to the trace monad, but so much is already going to be breaking that it shouldn't make too much of a difference.

@corlewis corlewis force-pushed the monad_improvements3 branch from 1bc2a87 to 3bf5137 Compare July 14, 2024 23:01
@corlewis
Copy link
Member Author

Changes since the reviews are that I've removed the inv lemmas pointed out by @lsf37, which I think are unnecessary, and pulled in new lemmas to Trace_Reader_Option.thy which were recently added in the nondet monad. There's an argument that the equivalents to those inv lemmas should also be removed from the trace monad's valid ruleset in Trace_VCG.thy, but so far we have been keeping that ruleset very close to the nondet monad's so I think it would be best to leave exploring that for a later PR.

@lsf37
Copy link
Member

lsf37 commented Jul 15, 2024

Changes since the reviews are that I've removed the inv lemmas pointed out by @lsf37, which I think are unnecessary, and pulled in new lemmas to Trace_Reader_Option.thy which were recently added in the nondet monad. There's an argument that the equivalents to those inv lemmas should also be removed from the trace monad's valid ruleset in Trace_VCG.thy, but so far we have been keeping that ruleset very close to the nondet monad's so I think it would be best to leave exploring that for a later PR.

👍 Happy with that.

@corlewis corlewis force-pushed the monad_improvements3 branch from 3bf5137 to 4b0305e Compare July 17, 2024 03:36
@corlewis corlewis merged commit f00bbb7 into seL4:master Jul 17, 2024
9 of 14 checks passed
@corlewis corlewis deleted the monad_improvements3 branch July 17, 2024 03:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lsf37 lsf37 lsf37 approved these changes

@Xaphiosis Xaphiosis Xaphiosis approved these changes

@michaelmcinerney michaelmcinerney Awaiting requested review from michaelmcinerney

Assignees

@corlewis corlewis

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@corlewis @lsf37 @Xaphiosis