Prove `cancelIPC_ccorres1` #831

nspin · 2024-11-30T14:30:59Z

Requires seL4/seL4#1358, which fixes an apparent potential bug that I discovered while working on this proof. That PR also sneaks in a few trivial changes that made verification a bit easier.

I weakened the preconditions in the still-unproven reply_unlink_ccorres lemma. They now correspond to those in replyUnlinkTcb_corres.

Edit: also requires seL4/seL4#1297.

Test with coliasgroup/seL4#1

Xaphiosis · 2024-12-02T21:36:28Z

proof/crefine/RISCV64/IpcCancel_C.thy

         st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st)
                            \<and> blockingObject st = ep) thread
        and ko_at' ep' ep)
-        {s. epptr_' s = Ptr ep}


Moving this from the preconditions to the assumptions might seem convenient here, but in general this move is against the flow of automation, e.g. if you want to use ctac; the idea is preconditions bubble up the stack and are resolved at the end. Is there any reason you had to change this?

I made this change because for some reason I had a feeling that I should prefer the more structured-seeming csymbr over ccorres_symb_exec_r, and using a value rather than a precondition on a variable in this helper lemma made it easier to use csymbr around it in the main proof. I've changed this lemma back to using the precondition, and I see how that results in the composition of the helper lemma and the main proof fit better into the ccorres proof flow.

Cool. You've now managed the C side of this, but you've introduced a similar thing on the Haskell side in cancelIPC_ccorres_helper via epptr = Ptr ep. It might make sense to do the same manoeuvre there. Traditionally that's been done by adding a and K (epptr = Ptr ep) to the Haskell precondition side, and then if you really need that fact immediately in the proof, using rule ccorres_grab_asm as the first proof step.

Oops! That epptr = Ptr ep assumption is actually just left over from the original PR, I missed removing it when addressing this thread.

Xaphiosis · 2024-12-02T21:38:52Z

proof/crefine/RISCV64/IpcCancel_C.thy

+       and st_tcb_at' (\<lambda>st. (\<exists>oref cg. st = Structures_H.BlockedOnReceive oref cg (Some replyPtr))
+                            \<or> st = Structures_H.BlockedOnReply (Some replyPtr))
+                      tcbPtr
+       and obj_at' (\<lambda>reply. replyTCB reply = Some tcbPtr) replyPtr)


indentation: the advantage of putting operators on the left is we can align them with the previous line in most cases (see style guide), so and should align with valid_tcbs'.
Also, the ∨ belongs under the ∃, i.e. under st =

I've fixed the indentation level of the ands.

As for the ∨, I put it under the ( that precedes the ∃ because the structure of the term is (∃ ... st = ...) ∨ st = .... Could you clarify where the ∨ belongs and why?

You put it in the right place, for exactly the reasons you stated. If you look at the ∨, it should be to the right of whatever it belongs to, i.e. the λst., and it is on the same level as the LHS argument of the ∨, which is the (∃ ... st = ...). This means that the structure can be seen at a glance, which is important when doing textual surgery on theory files (which is diffs, git conflicts, PRs, etc).

proof/crefine/RISCV64/IpcCancel_C.thy

Xaphiosis · 2024-12-02T21:46:07Z

proof/crefine/RISCV64/IpcCancel_C.thy

+
+lemma ctcb_relation_BlockedOnSend_blockingObject:
+  assumes "ctcb_relation tcb ctcb"
+  assumes "BlockedOnSend bo bib bicg bicgr biic = tcbState tcb"


did you invent these bo bib bicg bicgr biic style variable names, or did they come from other lemmas/definitions?

I invented them, but now I've switched to variable names found elsewhere in CRefine (oref badge cg cgr isc, etc.).

Xaphiosis · 2024-12-02T21:48:51Z

proof/crefine/RISCV64/IpcCancel_C.thy

+  shows "ep_at' bo s"
+  using assms
+  apply -
+  apply (drule (1) tcb_in_valid_state')


if you compress these lemmas like I outlined, you won't need the use assms, and therefore won't need to chain in the facts with apply -. There's also a chance that you might be able to fold the drule (1) tcb_in_valid_state' into the fastforce, so that the proof ends up as:
by (fastforce dest!: tcb_in_valid_state' simp: obj_at'_def valid_tcb_state'_def)

Done, thanks.

Xaphiosis · 2024-12-02T21:50:28Z

proof/crefine/RISCV64/IpcCancel_C.thy

+    "\<exists>tcb. ko_at' tcb thread s \<and> tcbState tcb = BlockedOnReceive bo bicg (Some ro)"
+    by (clarsimp simp: st_tcb_at'_def obj_at'_def)
+  from sy and vo and st and ra and ko show ?thesis
+    apply -


you don't need apply - for tactics like simp/clarsimp/fastforce/auto/etc, it's mostly for direct rule invocations (obvious, I know :/)
you can also shave off the ko by using with instead of from

Done, thanks.

Xaphiosis · 2024-12-02T21:52:08Z

proof/crefine/RISCV64/IpcCancel_C.thy

+              \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sym_refs_asrt s\<rbrace>"
+proof -
+  have sy: "threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>sym_refs_asrt\<rbrace>"
+    by - (unfold sym_refs_asrt_def, wpsimp wp: threadSet_state_refs_of', simp,


if you're doing Isar-style proofs, it makes more sense to do:

unfolding sym_refs_asrt_def by wpsimp (force simp: tcb_bound_refs'_def)+

Xaphiosis · 2024-12-02T21:53:07Z

proof/crefine/RISCV64/IpcCancel_C.thy

+
+lemma thread_state_to_tsType_eq_BlockedOnSend:
+  "(thread_state_to_tsType ts = scast ThreadState_BlockedOnSend)
+      = (\<exists>bo bib bicg bicgr biic. ts = BlockedOnSend bo bib bicg bicgr biic)"


indentation on =, also, do these rules really benefit you most as a rewrite rather than a destruction/elimination rule?

I've changed these into destruction rules so that their structure more clearly aligns with how they are used.

Xaphiosis · 2024-12-02T21:56:55Z

proof/crefine/RISCV64/IpcCancel_C.thy

+  "(thread_state_to_tsType ts = scast ThreadState_BlockedOnSend)
+      = (\<exists>bo bib bicg bicgr biic. ts = BlockedOnSend bo bib bicg bicgr biic)"
+  by (cases ts, simp_all add: ThreadState_defs)
+
 lemma cancelIPC_ccorres1:


I have more comments for the proof of this lemma, but it would be useful to know how much of the proof is copied, as a bunch of them will be style-and-compression related.

Some blocks, along with the overall structure, are copied from the non-MCS proof, but I've touched most of it. Overall, a ship of Theseus-like situation. The semantic indenting is a too much for GitHub's diff algorithm to make sense of (understandably), which makes it harder to tell which blocks are copied.

Xaphiosis · 2024-12-02T21:59:12Z

proof/crefine/RISCV64/IpcCancel_C.thy

+                               \<and> valid_tcbs' s
+                               \<and> (ro = None \<longrightarrow> True)
+                               \<and> (\<forall>x. ro = Some x \<longrightarrow> obj_at' (\<lambda>reply. replyTCB reply = Some thread) x s)"
+                        in hoare_post_imp)


This kind of explicit goal rephrasing is a sign that backwards reasoning is breaking down for some reason. Usually that's not a good sign, but it is at times unavoidable. Any thoughts on what happened?

This mess was an artifact of the approach I took to figuring out how to do this proof. It's unnecessary, and I've removed it and moved the following bit to the end of the proof where it belongs.

What happened is that I was having trouble with a lhs Hoare triple goal with an option split in the postcondition. Not having discovered hoare_case_option_wp2 yet, I tried a bunch of different things and ended up down this goal-rephrasing path in my attempt to make incremental progress. Once I finally did discover hoare_case_option_wp2 and was able move on with the rest of the proof, and again during my subsequent synthesis+streamlining passes, I missed realizing the goal rephrasing was unnecessary.

There are things done during figuring out proofs that rarely make it to the final product, but are perfectly reasonable methods to go about it. Hand-holding instantiations, splitting up the proof at a "known" juncture to understand which of the facts is actually necessary, and so on. This looked like one of those cases :)

Xaphiosis · 2024-12-02T22:03:37Z

Firstly, welcome, and huge congratulations for being one of the very very few (maybe the second person ever?) to be a third-party contributor to the verification side of seL4. The proofs look ok, comments are mainly for improvements / learning / style.

kent-mcleod · 2024-12-05T21:23:56Z

Firstly, welcome, and huge congratulations for being one of the very very few (maybe the second person ever?) to be a third-party contributor to the verification side of seL4.

Congratulations @nspin !!

Xaphiosis · 2024-12-05T23:07:46Z

proof/crefine/RISCV64/IpcCancel_C.thy

   apply (rule ccorres_move_c_guard_tcb)
-   apply csymbr
+   apply (rule ccorres_stateAssert)
+   apply (rule ccorres_stateAssert)


trivial: can say apply (rule ccorres_stateAssert)+ as a message of "we're going through all the asserts here"

Xaphiosis · 2024-12-05T23:14:28Z

proof/crefine/RISCV64/IpcCancel_C.thy

+        apply vcg
+       apply (clarsimp simp: typ_heap_simps')
+       apply (erule(1) rf_sr_tcb_update_no_queue2, (simp add: typ_heap_simps')+)[1]
+        apply (rule ball_tcb_cte_casesI, simp_all)[1]


this might be copied from and old proof, these days we can do
apply (rule ball_tcb_cte_casesI; simp) instead

Also, the erule(1) above it should be erule (1), so this might be ancient, since that line probably could also be rewritten as:
apply (erule (1) rf_sr_tcb_update_no_queue2; simp add: typ_heap_simps')

I made that first change, but the second simplification does not work.

Well, it doesn't always work out. ; processes new goals last-to-first so there might be a unification issue. Fine to leave that as is then.

Xaphiosis · 2024-12-05T23:20:48Z

proof/crefine/RISCV64/IpcCancel_C.thy

+                         and val="oref"
+                         and R="st_tcb_at' ((=) (BlockedOnReceive oref cg ro)) thread"
+                         and R'=UNIV
+                         in ccorres_symb_exec_r_known_rv)


trivial: on these you can save visual space on what's uninteresting by folding the UNIV into:
in ccorres_symb_exec_r_known_rv[where R'=UNIV]

indentation: this is sadly my fault, because there's an issue to update the style guide and I haven't done it yet (#746), but the end of the in should align with the end of and since this right-aligns the uninteresting glue bits so that the interesting bits can end up left-aligned. Applies to all the big rule_tacs in this proof.

Done, thanks.

Xaphiosis · 2024-12-05T23:23:17Z

proof/crefine/RISCV64/IpcCancel_C.thy

+                      \<comment> \<open>None\<close>
+                     apply simp
+                     apply (ctac add: setThreadState_ccorres)
+                    \<comment> \<open>Some\<close>


for these None/Some comments (good idea), would be more useful to say what they refer to; this is obvious when you have the proof open, but not so obvious when reading the text, since it comes out of wpc

Xaphiosis · 2024-12-05T23:25:19Z

proof/crefine/RISCV64/IpcCancel_C.thy

+                               \<and> st_tcb_at' ((=) threadState) thread s
+                               \<and> invs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s
+                               \<and> sym_refs_asrt s"
+                in hoare_strengthen_post)


hard to tell in this interface, but the in should right-align with the _tac

Done, thanks.

Xaphiosis · 2024-12-05T23:28:25Z

proof/crefine/RISCV64/IpcCancel_C.thy

-  apply (case_tac ts,
-           auto simp: isTS_defs cthread_state_relation_def typ_heap_simps)
-  done *)
+  subgoal by (auto simp: obj_at'_def pred_tcb_at'_def valid_ep'_def isTS_defs isSendEP_def


ok, and final nitpick, which is the most annoying to fix up: the current auto-indenter shoves subgoal was off to the left, regardless of how deep you were in the proof, which requires manually indenting the subgoal proof, i.e. it should be:

apply (rule conjI) apply (clarsimp simp: sym_refs_asrt_def invs'_implies) subgoal by (auto simp: obj_at'_def pred_tcb_at'_def valid_ep'_def isTS_defs isSendEP_def split: thread_state.splits endpoint.splits) apply (clarsimp simp: sym_refs_asrt_def invs'_implies valid_objs'_valid_tcbs' sym_ref_BlockedOnReceive_replyObject_linked)

because the subgoal discharges one subgoal. This is in the style guide, but the tool works against us here (there is of course a thread on the Isabelle mailing list about this that went nowhere). Applies wherever you used autoindenter on subgoal :/

Xaphiosis

From my side, after the other nitpicks, this is good to go.

nspin · 2024-12-09T08:03:38Z

It turns out that my assumption that the rhs preconditions for replyUnlinkTcb_corres would suffice as lhs preconditions for reply_unlink_ccorres was naive. I've added a commit to this PR that proves reply_unlink_ccorres, eliminating the need for guesswork there.

As this corner of CRefine depends on seL4/seL4#1297, so too does this PR. For now, I've changed the "Test with" link in this PR to point to a branch (coliasgroup/seL4#1) which includes seL4/seL4#1297 and the additional minor changes in seL4/seL4#1358.

Xaphiosis · 2024-12-09T08:23:30Z

proof/crefine/RISCV64/Ctac_lemmas_C.thy

+  apply clarsimp
+  apply (drule (1) reply_at_h_t_valid)
+  apply simp
+  done


probably can one-line it with clarsimp dest: reply_at_h_t_valid (or if that doesn't work, dest!, or if that doesn't work use dest! and fastforce)

That was fast. Thanks

Xaphiosis · 2024-12-09T08:27:14Z

proof/crefine/RISCV64/IpcCancel_C.thy

@@ -2913,12 +2913,120 @@ lemma reply_remove_tcb_ccorres:
    (replyRemoveTCB tptr) (Call reply_remove_tcb_'proc)"
 sorry (* FIXME RT: reply_remove_tcb_corres *)

+lemma updateReply_eq:


Not a great name, _eq lemma name would imply some kind of equality between two things... but seeing the _lemma4 below, it looks like you copied it from somewhere else?

Yes, I should have made that more clear when I pushed the commit. All of the new lemmas in the reply_unlink_ccorres commit, aside from reply_unlink_ccorres itself, are derived (in some cases very closely) from analogous lemmas found elsewhere in CRefine.

Well, then I guess you're consistent with someone's historic poor naming convention, so it's fine to leave it. Also, apart from the potential optimisation, I'm also fine with your latest commit.

updateReply_eq is mostly copied from updateSchedContext_eq, and updateReply_ccorres_lemma4 is mostly copied from updateSchedContext_ccorres_lemma4. I don't totally understand the _ccorres_lemma[234] naming convention, but I (perhaps recklessly) just went with it.

I think that's the right move. The whole lemma4 thing has something to do with handling updates of structs within structs at a pointer location, but not sure of the exact history of the 2/3/4. If we ever update it to better tech, having the lemma4's around to grep for will be useful.

Signed-off-by: Nick Spinale <[email protected]>

nspin mentioned this pull request Nov 30, 2024

Fix apparent potential bug in cancelIPC for MCS seL4/seL4#1358

Open

nspin force-pushed the pr/prove-cancelipc-ccorres-1 branch from 6ccdeb1 to 67641d4 Compare November 30, 2024 14:36

Xaphiosis reviewed Dec 2, 2024

View reviewed changes

proof/crefine/RISCV64/IpcCancel_C.thy Show resolved Hide resolved

Xaphiosis reviewed Dec 2, 2024

View reviewed changes

nspin force-pushed the pr/prove-cancelipc-ccorres-1 branch 4 times, most recently from 754cab4 to 1896367 Compare December 5, 2024 20:35

Xaphiosis reviewed Dec 5, 2024

View reviewed changes

Xaphiosis approved these changes Dec 5, 2024

View reviewed changes

nspin force-pushed the pr/prove-cancelipc-ccorres-1 branch 2 times, most recently from af73fce to d5e6bd2 Compare December 5, 2024 23:55

nspin mentioned this pull request Dec 9, 2024

Dummy PR coliasgroup/seL4#1

Open

nspin force-pushed the pr/prove-cancelipc-ccorres-1 branch from d5e6bd2 to f20acdc Compare December 9, 2024 07:46

nspin force-pushed the pr/prove-cancelipc-ccorres-1 branch from f20acdc to a1f3c18 Compare December 9, 2024 08:04

Xaphiosis reviewed Dec 9, 2024

View reviewed changes

rt crefine: prove reply_unlink_ccorres

796fd26

Signed-off-by: Nick Spinale <[email protected]>

nspin force-pushed the pr/prove-cancelipc-ccorres-1 branch from a1f3c18 to 651aa11 Compare December 9, 2024 08:53

rt crefine: prove cancelIPC_ccorres1

a22a42a

Signed-off-by: Nick Spinale <[email protected]>

nspin force-pushed the pr/prove-cancelipc-ccorres-1 branch from 651aa11 to a22a42a Compare December 10, 2024 00:58

Prove cancelIPC_ccorres1 #831

Are you sure you want to change the base?

Prove cancelIPC_ccorres1 #831

Conversation

nspin commented Nov 30, 2024 • edited Loading

Choose a reason for hiding this comment

nspin Dec 5, 2024 • 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

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nspin Dec 5, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nspin Dec 5, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis commented Dec 2, 2024

kent-mcleod commented Dec 5, 2024

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Xaphiosis Dec 5, 2024 • edited Loading

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

nspin commented Dec 9, 2024 • 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

nspin Dec 9, 2024 • 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

Prove `cancelIPC_ccorres1` #831

Prove `cancelIPC_ccorres1` #831

nspin commented Nov 30, 2024 •

edited

Loading

nspin Dec 5, 2024 •

edited

Loading

nspin Dec 5, 2024 •

edited

Loading

nspin Dec 5, 2024 •

edited

Loading

Xaphiosis Dec 5, 2024 •

edited

Loading

nspin commented Dec 9, 2024 •

edited

Loading

nspin Dec 9, 2024 •

edited

Loading