Add select_wp and alternative_wp to wp #661

corlewis · 2023-08-08T04:24:10Z

No description provided.

corlewis · 2023-08-08T04:31:01Z

proof/access-control/ADT_AC.thy

-                            hoare_vcg_all_lift hoare_vcg_imp_lift)+
+                            hoare_vcg_all_lift hoare_vcg_imp_lift
+                    wp_del: select_wp)+
          apply (rule hoare_pre_cont)
         apply (wpsimp wp: select_wp)+


There's a few places like this where existing proofs made use of the fact that select_wp wasn't in the wp set and were broken by this change. I could probably restructure the proof to avoid this but for now I've just deleted select_wp wherever required for the original proofs to continue working.

It looks like you were right and this situation is the rare one, so this is fine by me.

Xaphiosis · 2023-08-08T06:27:26Z

would the monads: add select_wp and alternative_wp to wp commit message be more instructive if it has a lib: prefix? Also the other commit message only mentions select_wp but you're doing alternative_wp as well

Xaphiosis · 2023-08-08T06:31:45Z

tools/autocorres/L1Defs.thy

@@ -334,7 +334,7 @@ lemma no_throw_L1_init [simp]: "no_throw P (L1_init f)"
  apply (rule no_throw_bindE [where B=\<top>])
    apply simp
   apply simp
-  apply wp
+  apply wpsimp


any thoughts on why the switch to wpsimp was required?

I'd have to go in to check this lemma specifically, but generally that switch was needed when the proof used to work with some rule that could directly solve the hoare triple, instead of the more general *_wp which leaves behind a final goal. I guess an alternative would be to explicitly add that other rule again here so that it is used first, but that feels more clunky.

Got it, thanks for the explanation. No need to dive back in.

Xaphiosis · 2023-08-08T06:38:30Z

proof/capDL-api/Retype_DP.thy

-crunch cdt[wp]: corrupt_ipc_buffer "\<lambda>s. P (cdl_cdt s)"
-(wp:select_wp simp:crunch_simps corrupt_intents_def)
+crunches corrupt_frame, corrupt_tcb_intent, corrupt_ipc_buffer
+  for cdt[wp]: "\<lambda>s. P (cdl_cdt s)"


Off-topic, but would there be any benefit to making crunches look for a free s in the term and adding a λs. in front? Would that be something that makes things nicer, or more confusing?

Hmm, interesting. It would definitely save a lot of repetition and make things a bit nicer for experienced users but my first reaction is that it would be more confusing for people who are encountering it for the first time.

I don't think it would work, unless you encode the name s as something special. If you look at the statements, P is a legitimate free variable in the term and would look the same as an s to Isabelle unless you start analysing for types etc.

Xaphiosis · 2023-08-08T06:45:56Z

proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy

  done

 lemma doUserOp_if_cur_thread[ADT_IF_Refine_assms, wp]:
  "doUserOp_if f tc \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace>"
  apply (simp add: doUserOp_if_def)
-  apply (wp select_wp | wpc | simp)+
+  apply (wp | wpc | simp)+


probably too late now, but isn't this equivalent to wpsimp+ or wpsimp?

Yep, it definitely is. In cases like this where it really was just deleting the rule from wp, the process I was using to make these changes made it easier to just keep on moving. Beyond that, it was basically random which lemmas I would stop at and clean up and which I would just remove the rules and move on.

Xaphiosis

This was a bigger improvement than I expected. Thanks!

There are a fair few opportunities this created to collapse apply statements into a wpsimp, and you caught some of them, but I'm wondering whether it's possible to make a heuristic that can find the more common cases. Another day perhaps.

corlewis · 2023-08-08T07:27:04Z

There are a fair few opportunities this created to collapse apply statements into a wpsimp, and you caught some of them, but I'm wondering whether it's possible to make a heuristic that can find the more common cases. Another day perhaps.

That would be nice, along with something for automating converting all of the old uses of crunch to crunches.

corlewis · 2023-08-08T07:31:36Z

would the monads: add select_wp and alternative_wp to wp commit message be more instructive if it has a lib: prefix? Also the other commit message only mentions select_wp but you're doing alternative_wp as well

Hmm, I was originally trying to distinguish the commit prefix in the Monads refactor PR where there's a commit that just touches the monads directory and then one which updates lib (and other directories). I don't mind that much either way, this made a bit more sense to me but maybe it could be lib/monads.

Thanks for pointing out the second commit message only mentioning select_wp, that was the original work and then I added alternative_wp later.

Xaphiosis · 2023-08-08T08:04:27Z

would the monads: add select_wp and alternative_wp to wp commit message be more instructive if it has a lib: prefix? Also the other commit message only mentions select_wp but you're doing alternative_wp as well

Hmm, I was originally trying to distinguish the commit prefix in the Monads refactor PR where there's a commit that just touches the monads directory and then one which updates lib (and other directories). I don't mind that much either way, this made a bit more sense to me but maybe it could be lib/monads.

Hmm. Yeah lib/monads: or lib: monads: would work. Then again you're only touching nondet/Nondet_VCG.thy, so is that "monads" in general?

corlewis · 2023-08-08T08:20:19Z

would the monads: add select_wp and alternative_wp to wp commit message be more instructive if it has a lib: prefix? Also the other commit message only mentions select_wp but you're doing alternative_wp as well

Hmm, I was originally trying to distinguish the commit prefix in the Monads refactor PR where there's a commit that just touches the monads directory and then one which updates lib (and other directories). I don't mind that much either way, this made a bit more sense to me but maybe it could be lib/monads.

Hmm. Yeah lib/monads: or lib: monads: would work. Then again you're only touching nondet/Nondet_VCG.thy, so is that "monads" in general?

True, now I'm not sure whether it should be more specific in this case. My first reaction was that mentioning nondet in the prefix wouldn't help, but now I think that it would, since otherwise there's no way to tell from the commit message whether this is for the trace monad or the nondet monad. However, I don't like lib/monads/nondet. Thoughts?

Xaphiosis · 2023-08-08T08:34:58Z

would the monads: add select_wp and alternative_wp to wp commit message be more instructive if it has a lib: prefix? Also the other commit message only mentions select_wp but you're doing alternative_wp as well

Hmm, I was originally trying to distinguish the commit prefix in the Monads refactor PR where there's a commit that just touches the monads directory and then one which updates lib (and other directories). I don't mind that much either way, this made a bit more sense to me but maybe it could be lib/monads.

Hmm. Yeah lib/monads: or lib: monads: would work. Then again you're only touching nondet/Nondet_VCG.thy, so is that "monads" in general?

True, now I'm not sure whether it should be more specific in this case. My first reaction was that mentioning nondet in the prefix wouldn't help, but now I think that it would, since otherwise there's no way to tell from the commit message whether this is for the trace monad or the nondet monad. However, I don't like lib/monads/nondet. Thoughts?

Looking at the commit history, there's a bunch prefixed with lib/monads:. Also, not everything has to go on one line, and some stuff is obvious once we look at the commit, so long as it's not misleading.
lib/monads: add select_wp and alternative_wp to wp set for Nondet monad or something like that is still short enough. If we're reasonably sure that select_wp or alternative_wp can't be added to some other monad's wp rule set, then can drop the "for Nondet ..." as well. I'm thinking with there only being one wp set, that might be the simplest option.

lsf37

Very nice. I had not realised that we are using select that often. It's good, it's a sign that there is some actual abstraction going on :-)

lsf37 · 2023-08-08T11:15:43Z

proof/access-control/ADT_AC.thy

-                            hoare_vcg_all_lift hoare_vcg_imp_lift)+
+                            hoare_vcg_all_lift hoare_vcg_imp_lift
+                    wp_del: select_wp)+
          apply (rule hoare_pre_cont)
         apply (wpsimp wp: select_wp)+


lsf37 · 2023-08-08T11:19:13Z

proof/capDL-api/Retype_DP.thy

-crunch cdt[wp]: corrupt_ipc_buffer "\<lambda>s. P (cdl_cdt s)"
-(wp:select_wp simp:crunch_simps corrupt_intents_def)
+crunches corrupt_frame, corrupt_tcb_intent, corrupt_ipc_buffer
+  for cdt[wp]: "\<lambda>s. P (cdl_cdt s)"


I don't think it would work, unless you encode the name s as something special. If you look at the statements, P is a legitimate free variable in the term and would look the same as an s to Isabelle unless you start analysing for types etc.

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

corlewis added the proof engineering nicer, shorter, more maintainable etc proofs label Aug 8, 2023

corlewis requested review from Xaphiosis, lsf37 and michaelmcinerney August 8, 2023 04:24

corlewis self-assigned this Aug 8, 2023

corlewis commented Aug 8, 2023

View reviewed changes

Xaphiosis reviewed Aug 8, 2023

View reviewed changes

Xaphiosis approved these changes Aug 8, 2023

View reviewed changes

lsf37 approved these changes Aug 8, 2023

View reviewed changes

corlewis changed the base branch from monads_refactor to master August 9, 2023 02:08

corlewis force-pushed the nondet_add_wp branch from b154b6a to 0de5a12 Compare August 9, 2023 02:10

corlewis added 2 commits August 9, 2023 12:11

lib/monads: add select_wp and alternative_wp to wp set for Nondet monad

a3e8b33

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

proof+autocorres: update for select_wp and alternative_wp

2da36ce

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

corlewis force-pushed the nondet_add_wp branch from 0de5a12 to 2da36ce Compare August 9, 2023 02:12

corlewis merged commit 0211681 into seL4:master Aug 9, 2023
13 checks passed

corlewis deleted the nondet_add_wp branch August 9, 2023 06:42

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add select_wp and alternative_wp to wp #661

Add select_wp and alternative_wp to wp #661

corlewis commented Aug 8, 2023

corlewis Aug 8, 2023

Xaphiosis Aug 8, 2023

lsf37 Aug 8, 2023

Xaphiosis commented Aug 8, 2023 •

edited

Loading

Xaphiosis Aug 8, 2023

corlewis Aug 8, 2023

Xaphiosis Aug 8, 2023

Xaphiosis Aug 8, 2023

corlewis Aug 8, 2023

lsf37 Aug 8, 2023

Xaphiosis Aug 8, 2023

corlewis Aug 8, 2023

Xaphiosis left a comment

corlewis commented Aug 8, 2023 •

edited

Loading

corlewis commented Aug 8, 2023

Xaphiosis commented Aug 8, 2023

corlewis commented Aug 8, 2023

Xaphiosis commented Aug 8, 2023

lsf37 left a comment

lsf37 Aug 8, 2023

lsf37 Aug 8, 2023

Add select_wp and alternative_wp to wp #661

Add select_wp and alternative_wp to wp #661

Conversation

corlewis commented Aug 8, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis commented Aug 8, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis left a comment

Choose a reason for hiding this comment

corlewis commented Aug 8, 2023 • edited Loading

corlewis commented Aug 8, 2023

Xaphiosis commented Aug 8, 2023

corlewis commented Aug 8, 2023

Xaphiosis commented Aug 8, 2023

lsf37 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis commented Aug 8, 2023 •

edited

Loading

corlewis commented Aug 8, 2023 •

edited

Loading