rt haskell+refine+crefine: several sorries in IpcCancel_C

This proves ccorres rules for isSchedulable, rescheduleRequired, possibleSwitchTo, and setThreadState, including variants for when sch_act_simple holds. This also changes the Haskell definition of isSchedulable to more closely align with the C, to ease the proof of isSchedulable_ccorres. Signed-off-by: Michael McInerney <[email protected]>
seL4 · Jul 12, 2024 · eecc6ee · eecc6ee
1 parent da19275
commit eecc6ee
Show file tree

Hide file tree

Showing 19 changed files with 692 additions and 662 deletions.
diff --git a/proof/crefine/RISCV64/Arch_C.thy b/proof/crefine/RISCV64/Arch_C.thy
@@ -1087,7 +1087,7 @@ lemma decodeRISCVPageTableInvocation_ccorres:
     apply (clarsimp simp: ct_in_state'_def isCap_simps valid_tcb_state'_def)
     apply (case_tac v1; clarsimp) (* is PT mapped *)
      apply (auto simp: ct_in_state'_def isCap_simps valid_tcb_state'_def valid_cap'_def
-                       wellformed_mapdata'_def sch_act_wf_def sch_act_simple_def
+                       wellformed_mapdata'_def weak_sch_act_wf_def sch_act_simple_def
                 elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')
     done
   apply (rule conjI)
@@ -1102,7 +1102,7 @@ lemma decodeRISCVPageTableInvocation_ccorres:
                            slotcap_in_mem_def dest!: ctes_of_valid')
     by (auto simp: ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def
                    valid_cap'_def wellformed_acap'_def wellformed_mapdata'_def
-                   sch_act_wf_def sch_act_simple_def
+                   weak_sch_act_wf_def sch_act_simple_def
              elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')[1]
 
   apply (rule conjI)
@@ -2105,15 +2105,15 @@ lemma decodeRISCVFrameInvocation_ccorres:
   subgoal
     by (auto simp: ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def
                    valid_cap'_def wellformed_acap'_def wellformed_mapdata'_def
-                   sch_act_wf_def sch_act_simple_def
+                   weak_sch_act_wf_def sch_act_simple_def
              elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')
 
   (* RISCVPageUnMap, Haskell side *)
   apply (rule conjI)
   subgoal
     by (auto simp: isCap_simps comp_def ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def
                    valid_cap'_def wellformed_acap'_def wellformed_mapdata'_def
-                   sch_act_wf_def sch_act_simple_def
+                   weak_sch_act_wf_def sch_act_simple_def
              elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')
 
   (* C side of precondition satisfaction *)
@@ -2847,6 +2847,10 @@ lemma decodeRISCVMMUInvocation_ccorres:
     apply (rule conjI; clarsimp)+
     apply (rule conjI, erule ctes_of_valid', clarsimp)
     apply (intro conjI)
+             apply fastforce
+            apply fastforce
+           apply fastforce
+          apply fastforce
          apply fastforce
         apply (fastforce elim!: pred_tcb'_weakenE)
        apply (clarsimp simp: excaps_in_mem_def slotcap_in_mem_def)
@@ -2864,6 +2868,10 @@ lemma decodeRISCVMMUInvocation_ccorres:
    apply (clarsimp simp: isCap_simps valid_tcb_state'_def)
    apply (frule invs_arch_state', clarsimp)
    apply (intro conjI)
+           apply (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE)
+          apply fastforce
+         apply fastforce
+        apply fastforce
        apply (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE)
       apply (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE)
      apply (cases extraCaps; simp)

diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy
@@ -1173,17 +1173,18 @@ lemma tcb_queue_relation2_cong:
 
 context kernel_m begin
 
-lemma setThreadState_ccorres_valid_queues'_simple:
+lemma setThreadState_ccorres_simple:
   "ccorres dc xfdc
-     (tcb_at' thread)
-     ({s'. (\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := ts_' s' && mask 4\<rparr>, fl))}
-      \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) []
+     (\<lambda>s. tcb_at' thread s \<and> sch_act_simple s \<and> no_0_obj' s
+          \<and> weak_sch_act_wf (ksSchedulerAction s) s)
+     (\<lbrace>\<forall>cl fl. cthread_state_relation_lifted st (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace>
+      \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) []
      (setThreadState st thread) (Call setThreadState_'proc)"
   apply (cinit lift: tptr_' cong add: call_ignore_cong)
-    apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres)
-   apply (ctac add: scheduleTCB_ccorres_valid_queues'_simple)
-  apply wpsimp
-  apply (clarsimp simp: weak_sch_act_wf_def)
+   apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres)
+    apply (ctac add: scheduleTCB_ccorres_simple)
+   apply (wpsimp wp: threadSet_valid_objs')
+  apply clarsimp
   done
 
 lemma updateRestartPC_ccorres:
@@ -1401,23 +1402,27 @@ lemma active_runnable':
 
 crunches updateRestartPC
   for no_0_obj'[wp]: no_0_obj'
+  and weak_sch_act_wf[wp]: "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s"
   (wp: crunch_wps)
 
 lemma suspend_ccorres:
   assumes cteDeleteOne_ccorres:
-  "\<And>w slot. ccorres dc xfdc
-   (invs' and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap
-        \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)
-   ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w}
+  "\<And>w slot.
+   ccorres dc xfdc
+     (invs'
+      and cte_wp_at' (\<lambda>ct. w = -1 \<or> cteCap ct = NullCap
+          \<or> (\<forall>cap'. ccap_relation (cteCap ct) cap' \<longrightarrow> cap_get_tag cap' = w)) slot)
+     ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w}
         \<inter> {s. slot_' s = Ptr slot}) []
    (cteDeleteOne slot) (Call cteDeleteOne_'proc)"
   shows
   "ccorres dc xfdc
-   (invs' and tcb_at' thread and (\<lambda>s. thread \<noteq> ksIdleThread s))
-   (UNIV \<inter> {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) []
-   (suspend thread) (Call suspend_'proc)"
+     (invs' and sch_act_simple and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and tcb_at' thread
+      and (\<lambda>s. thread \<noteq> ksIdleThread s))
+     \<lbrace>\<acute>target = tcb_ptr_to_ctcb_ptr thread\<rbrace> []
+     (suspend thread) (Call suspend_'proc)"
   apply (cinit lift: target_')
-  apply (rule ccorres_stateAssert)
+   apply (rule ccorres_stateAssert)
    apply (ctac(no_vcg) add: cancelIPC_ccorres1 [OF cteDeleteOne_ccorres])
     apply (rule getThreadState_ccorres_foo)
     apply (rename_tac threadState)
@@ -1444,7 +1449,7 @@ lemma suspend_ccorres:
           apply (ctac (no_vcg) add: updateRestartPC_ccorres)
          apply (rule ccorres_return_Skip)
         apply ceqv
-       apply (ctac(no_vcg) add: setThreadState_ccorres_valid_queues'_simple)
+       apply (ctac(no_vcg) add: setThreadState_ccorres_simple)
         apply (ctac (no_vcg) add: tcbSchedDequeue_ccorres)
          apply (ctac (no_vcg) add: tcbReleaseRemove_ccorres)
           apply (ctac (no_vcg) add: schedContext_cancelYieldTo_ccorres)
@@ -1454,10 +1459,12 @@ lemma suspend_ccorres:
     apply clarsimp
     apply (rule conseqPre, vcg)
     apply (rule subset_refl)
-   apply (rule_tac Q="\<lambda>_. invs' and tcb_at' thread" in hoare_post_imp)
+   apply (rule_tac Q="\<lambda>_ s. invs' s \<and> tcb_at' thread s \<and> sch_act_simple s
+                            \<and> weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp)
     apply fastforce
    apply (wpsimp wp: hoare_vcg_all_lift)
-  by (auto simp: ThreadState_defs)[1]
+  apply (auto simp: ThreadState_defs)
+  done
 
 lemma cap_to_H_NTFNCap_tag:
   "\<lbrakk> cap_to_H cap = NotificationCap word1 word2 a b;

diff --git a/proof/crefine/RISCV64/Interrupt_C.thy b/proof/crefine/RISCV64/Interrupt_C.thy
@@ -250,13 +250,13 @@ lemma decodeIRQHandlerInvocation_ccorres:
       apply (rule ccorres_alternative2)
       apply (rule ccorres_return_CE, simp+)[1]
      apply (wp sts_invs_minor')+
-    apply (rule ccorres_equals_throwError)
-     apply (fastforce simp: invocationCatch_def throwError_bind
-                      split: gen_invocation_labels.split)
-    apply (simp add: ccorres_cond_iffs cong: StateSpace.state.fold_congs globals.fold_congs)
-    apply (rule syscall_error_throwError_ccorres_n)
-    apply (simp add: syscall_error_to_H_cases)
-   apply simp
+   apply (rule ccorres_equals_throwError)
+    apply (fastforce simp: invocationCatch_def throwError_bind
+                     split: gen_invocation_labels.split)
+   apply (simp add: ccorres_cond_iffs cong: StateSpace.state.fold_congs globals.fold_congs)
+   apply (rule syscall_error_throwError_ccorres_n)
+   apply (simp add: syscall_error_to_H_cases)
+  apply simp
   apply (clarsimp simp: Collect_const_mem)
   apply (clarsimp simp: invs_valid_objs'
                         ct_in_state'_def
@@ -270,16 +270,18 @@ lemma decodeIRQHandlerInvocation_ccorres:
                     slotcap_in_mem_def valid_tcb_state'_def
              dest!: interpret_excaps_eq split: bool.splits)
   apply (intro conjI impI allI)
-  apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def
-                    excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth
-                    slotcap_in_mem_def valid_tcb_state'_def
-             dest!: interpret_excaps_eq split: bool.splits)+
-     apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')[6]
+                 apply (clarsimp simp: cte_wp_at_ctes_of neq_Nil_conv sysargs_rel_def n_msgRegisters_def
+                                   excaps_map_def excaps_in_mem_def word_less_nat_alt hd_conv_nth
+                                   slotcap_in_mem_def valid_tcb_state'_def
+                            dest!: interpret_excaps_eq split: bool.splits)+
+            apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')[6]
+      apply fastforce
+     apply fastforce
     apply (drule ctes_of_valid')
      apply fastforce
     apply (clarsimp simp add:valid_cap_simps' RISCV64.maxIRQ_def)
     apply (erule order.trans,simp)
-  apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')
+   apply (auto dest: st_tcb_at_idle_thread' ctes_of_valid')
   done
 
 declare mask_of_mask[simp]

diff --git a/proof/crefine/RISCV64/Invoke_C.thy b/proof/crefine/RISCV64/Invoke_C.thy
@@ -40,9 +40,12 @@ lemma cap_case_ThreadCap2:
   by (simp add: isCap_simps
          split: capability.split)
 
+crunches tcbSchedEnqueue
+  for weak_sch_act_wf[wp]: "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s"
+
 lemma setDomain_ccorres:
   "ccorres dc xfdc
-      (invs' and tcb_at' t and (\<lambda>s. d \<le> maxDomain))
+      (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and tcb_at' t and (\<lambda>s. d \<le> maxDomain))
       (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. dom_' s = ucast d})
       [] (setDomain t d) (Call setDomain_'proc)"
   apply (rule ccorres_gen_asm)
@@ -75,12 +78,14 @@ lemma setDomain_ccorres:
        apply (simp add: guard_is_UNIV_def)
       apply simp
       apply wp
-     apply (rule_tac Q="\<lambda>rv'. invs' and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
+     apply (rule_tac Q="\<lambda>rv'. invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
+                              and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
                   in hoare_strengthen_post)
        apply (wpsimp wp: isSchedulable_wp)
       apply (fastforce simp: valid_pspace_valid_objs' weak_sch_act_wf_def
                       split: if_splits)
-     apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
+     apply (rule_tac Q="\<lambda>_. invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
+                            and tcb_at' t and (\<lambda>s. curThread = ksCurThread s)"
                   in hoare_strengthen_post)
       apply (wpsimp wp: threadSet_tcbDomain_update_invs' hoare_vcg_imp_lift'
                         threadSet_isSchedulable_bool)+