Monad improvements #759

corlewis · 2024-05-30T12:36:33Z

This improves the structure and naming consistency of the various monad rule sets, for both the nondet and trace monads. The main benefit is improved maintainability, in particular due to making sure that the nondet and trace monad rule sets are in sync.

There are 4 main categories of changes that were visible in the proofs:

lemma renamings
more consistently using P and Q for preconditions and postconditions
the default name for bound variables produced when splitting on bind is now always rv instead of sometimes r or x. In the couple of cases where this caused confusion I added a rename_tac and fixed a useful name, but in general I kept this PR simple and just updated the uses of the bound variables.
hoare_True_E_R: : "⦃P⦄ f ⦃λ_ s. True⦄, -" was removed from the simp set due to being unsafe, with wp_post_tautE_R: ⦃λ_. True⦄ f ⦃λ_ _. True⦄ being added as a wp rule instead. This meant that some proof steps were changed from simp to wp, and that some proofs no longer needed to locally delete it from the simp set.

The lemma renamings needed in the proofs are listed in the third commit message. I have made comments in this PR showing examples of the other categories.

corlewis · 2024-05-30T12:41:33Z

proof/refine/ARM/orphanage/Orphanage.thy

-   apply (rule_tac B="\<lambda>rv s. ?PRE s \<and> ksReadyQueues_asrt s \<and> ready_qs_runnable s
+   apply (rule_tac Q'="\<lambda>rv s. ?PRE s \<and> ksReadyQueues_asrt s \<and> ready_qs_runnable s
                             \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom"
-                in hoare_seq_ext)
+                in bind_wp)


This is an example of the second category of proof changes from the PR description; the conditions in the various bind_wp rules are now P, Q' and Q, instead of A, B and C.

corlewis · 2024-05-30T12:45:26Z

proof/refine/ARM/IpcCancel_R.thy

-  apply (rule hoare_seq_ext [OF _ gts_sp'])
-  apply (case_tac x, simp_all add: isTS_defs list_case_If)
+  apply (rule bind_wp [OF _ gts_sp'])
+  apply (case_tac rv, simp_all add: isTS_defs list_case_If)


This is an example of the third category of proof changes from the PR description; the bind_wp step now names the bound variable produced rv.

corlewis · 2024-05-30T12:46:31Z

proof/refine/ARM/Ipc_R.thy

-  apply (case_tac cap)
-          apply (simp_all add: Let_def isCap_simps)
-  apply wp
-  apply simp
-  done
+  by (case_tac cap; wpsimp simp: isCap_simps)


This is an example of the fourth category of proof changes from the PR description; many of the cases here were previously solved by simp, now they are all solved by wp.

lsf37 · 2024-05-31T01:40:48Z

This is great. It'll take some time to retrain muscle memory, but it is much more consistent and easier to remember now!

corlewis · 2024-05-31T02:50:49Z

The commit updating the proofs has now been split into two, one with just the lemma renamings and the second with the more manual changes. This will hopefully make it a bit easier to review.

lsf37 · 2024-06-05T04:47:32Z

lib/Monads/nondet/Nondet_VCG.thy

+\<comment> \<open>FIXME: remove?\<close>
 lemma hoare_return_drop_var[iff]:
  "\<lbrace>Q\<rbrace> return x \<lbrace>\<lambda>r. Q\<rbrace>"


For the following lemmas as well -- if they are unused, then yes we should definitely remove them. Of course the iff and intro ones might be used implicitly somewhere.

lsf37 · 2024-06-05T04:50:12Z

lib/Monads/nondet/Nondet_VCG.thy

 lemma hoare_vcg_const_Ball_lift_R:
 "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x \<in> S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S. Q x rv s\<rbrace>,-"
  unfolding validE_R_def validE_def
  by (rule hoare_strengthen_post)
     (fastforce intro!: hoare_vcg_const_Ball_lift split: sum.splits)+

+lemma hoare_vcg_const_Ball_lift_E_E:


Just confirming the naming between fooE, foo_R, and foo_E_E: is this the way we want it? (no underscore for the E wp variant and with underscore for the specialised forms)

Good spotting, I missed that the first time through. I have some more improvements on the way that includes these lemmas; I have been trying to standardise on foo, fooE, fooE_R, and fooE_E.

Cool, happy for that to go in a separate PR.

lib/Monads/nondet/Nondet_VCG.thy

lsf37

We might be nearing actual consistency :) Thanks for doing all this cleanup work. Our future brains will be relieved.

Xaphiosis

Can't find anything beyond what's been found already. I'm going to be even more confused after the renames, but consistency is definitely good.

Signed-off-by: Corey Lewis <[email protected]>

This improves the structure and naming consistency of the various monad rule sets, for both the nondet and trace monads. Signed-off-by: Corey Lewis <[email protected]>

This involved the following sed commands, with care taken to avoid unnecessary rewrites in lib/Monads and lib/StateMonad.thy sed -i 's/hoare_post_taut/hoare_TrueI/g' **/*.thy sed -i 's/hoare_TrueI\s*\[where P=\\<top>\]/wp_post_taut/g' proof/**/*.thy sed -i 's/hoare_post_imp_R/hoare_strengthen_postE_R/g' **/*.thy sed -i 's/hoare_seq_ext\b/bind_wp/g' **/*.thy sed -i 's/bind_wp\s*\[rotated\]/bind_wp_fwd/g' **/*.thy sed -i 's/hoare_vcg_precond_imp/hoare_weaken_pre/g' **/*.thy sed -i 's/hoare_vcg_seqE/bindE_wp/g' **/*.thy sed -i 's/bindE_wp\s*\[rotated\]/bindE_wp_fwd/g' **/*.thy sed -i 's/validE_weaken/hoare_chainE/g' **/*.thy sed -i 's/validE_weaken/hoare_chainE/g' **/*.ML sed -i 's/seqE/bindE_wp_fwd/g' **/*.thy sed -i 's/bindE_wp_fwd\s*\[rotated\]/bindE_wp/g' **/*.thy sed -i 's/hoare_True_E_R/hoareE_R_TrueI/g' **/*.thy sed -i -e 's/hoareE_R_TrueI\[where P="\\<top>"\]/wp_post_tautE_R/g' **/*.thy sed -i "s/hoare_post_impErr'/hoare_strengthen_postE/g" **/*.thy sed -i 's/hoare_post_impErr/hoare_strengthen_postE/g' **/*.thy sed -i 's/hoare_vcg_all_lift_R/hoare_vcg_all_liftE_R/g' **/*.thy sed -i 's/hoare_seq_ext_skip/bind_wp_fwd_skip/g' **/*.thy sed -i 's/True_E_E/wp_post_tautE_E/g' **/*.thy sed -i 's/\bseq_ext/bind_wp_fwd/g' proof/**/*.thy Signed-off-by: Corey Lewis <[email protected]>

This mostly involved renamed variable names and one lemma being removed from the simp set. Signed-off-by: Corey Lewis <[email protected]>

corlewis · 2024-06-07T04:12:09Z

Can't find anything beyond what's been found already. I'm going to be even more confused after the renames, but consistency is definitely good.

Consistency is the main aim of all this and I'm not particularly attached to the specific names I've chosen, so if there are any that you think will be particularly confusing then please point them out.

Xaphiosis · 2024-06-07T04:16:05Z

Can't find anything beyond what's been found already. I'm going to be even more confused after the renames, but consistency is definitely good.

Consistency is the main aim of all this and I'm not particularly attached to the specific names I've chosen, so if there are any that you think will be particularly confusing then please point them out.

I don't have anything better. The main thing to re-learn on this one are the seq_ext related rules, but I think the bind*_wp[_pre] scheme is ok.

corlewis added cleanup proof engineering nicer, shorter, more maintainable etc proofs labels May 30, 2024

corlewis requested review from Xaphiosis, lsf37 and michaelmcinerney May 30, 2024 12:36

corlewis self-assigned this May 30, 2024

corlewis commented May 30, 2024

View reviewed changes

corlewis force-pushed the monad_improvements branch from 644b3e0 to d4be2ce Compare May 31, 2024 02:49

corlewis force-pushed the monad_improvements branch from d4be2ce to 8d98dd8 Compare May 31, 2024 02:57

lsf37 reviewed Jun 5, 2024

View reviewed changes

lib/Monads/nondet/Nondet_VCG.thy Show resolved Hide resolved

lsf37 approved these changes Jun 5, 2024

View reviewed changes

Xaphiosis approved these changes Jun 6, 2024

View reviewed changes

corlewis added 4 commits June 7, 2024 13:17

lib/monads: improve style in Nondet_Monad_Equations

9fcd3d8

Signed-off-by: Corey Lewis <[email protected]>

lib/monads: improve consistency of monad rule sets

2718f2b

This improves the structure and naming consistency of the various monad rule sets, for both the nondet and trace monads. Signed-off-by: Corey Lewis <[email protected]>

lib+proof+autocorres: update for monad changes

687b2c8

This mostly involved renamed variable names and one lemma being removed from the simp set. Signed-off-by: Corey Lewis <[email protected]>

corlewis force-pushed the monad_improvements branch from 8d98dd8 to 687b2c8 Compare June 7, 2024 04:12

corlewis merged commit 1d3a26c into seL4:master Jun 11, 2024
12 of 13 checks passed

corlewis deleted the monad_improvements branch June 11, 2024 00:05

corlewis mentioned this pull request Jun 11, 2024

More monad improvements #765

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Monad improvements #759

Monad improvements #759

corlewis commented May 30, 2024 •

edited

Loading

corlewis May 30, 2024

corlewis May 30, 2024

corlewis May 30, 2024

lsf37 commented May 31, 2024

corlewis commented May 31, 2024

lsf37 Jun 5, 2024

lsf37 Jun 5, 2024

corlewis Jun 5, 2024

lsf37 Jun 5, 2024

lsf37 left a comment

Xaphiosis left a comment

corlewis commented Jun 7, 2024

Xaphiosis commented Jun 7, 2024

Monad improvements #759

Monad improvements #759

Conversation

corlewis commented May 30, 2024 • edited Loading

corlewis May 30, 2024

Choose a reason for hiding this comment

corlewis May 30, 2024

Choose a reason for hiding this comment

corlewis May 30, 2024

Choose a reason for hiding this comment

lsf37 commented May 31, 2024

corlewis commented May 31, 2024

lsf37 Jun 5, 2024

Choose a reason for hiding this comment

lsf37 Jun 5, 2024

Choose a reason for hiding this comment

corlewis Jun 5, 2024

Choose a reason for hiding this comment

lsf37 Jun 5, 2024

Choose a reason for hiding this comment

lsf37 left a comment

Choose a reason for hiding this comment

Xaphiosis left a comment

Choose a reason for hiding this comment

corlewis commented Jun 7, 2024

Xaphiosis commented Jun 7, 2024

corlewis commented May 30, 2024 •

edited

Loading