haskell+design+proof: add deletionIsSafe2 assert to deleteObjects

This assert is added in order to provide extra information regarding
liveness for objects in the region to be detyped, in preparation for
forthcoming work that will add fields to the TCB object and modify
the definition of liveness.

The assert is added separately from the current assert in deleteObjects
since these asserts are shown to hold via lemmas which occur in
different locales.

Greater use of the definition schact_is_rct is made in general, and in
particular, in some top-level theorems, but note that the guards and
preconditions of top-level theorems have not been strengthened.

Signed-off-by: Michael McInerney <[email protected]>

proof/crefine/AARCH64/Detype_C.thy

@@ -1553,8 +1553,7 @@ lemma deleteObjects_ccorres':
              doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm
              bind_assoc modify_machinestate_assert_cnodes_swap modify_machinestate_assert_ptables_swap
              modify_modify_bind)
-  apply (rule ccorres_stateAssert_fwd)
-  apply (rule ccorres_stateAssert_fwd)
+  apply (rule ccorres_stateAssert_fwd)+
   apply (rule ccorres_stateAssert_after)
   apply (rule ccorres_from_vcg)
   apply (rule allI, rule conseqPre, vcg)

proof/crefine/AARCH64/Refine_C.thy

@@ -522,7 +522,7 @@ lemma no_fail_callKernel:
   apply (rule corres_nofail)
    apply (rule corres_guard_imp)
      apply (rule kernel_corres)
-    apply (force simp: word_neq_0_conv)
+    apply (force simp: word_neq_0_conv schact_is_rct_def)
    apply (simp add: sch_act_simple_def)
   apply metis
   done

proof/crefine/ARM/Detype_C.thy

@@ -1428,7 +1428,7 @@ lemma deleteObjects_ccorres':
              doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm
              bind_assoc modify_machinestate_assert_cnodes_swap
              modify_modify_bind)
-  apply (rule ccorres_stateAssert_fwd)
+  apply (rule ccorres_stateAssert_fwd)+
   apply (rule ccorres_stateAssert_after)
   apply (rule ccorres_from_vcg)
   apply (rule allI, rule conseqPre, vcg)

proof/crefine/ARM/Refine_C.thy

@@ -516,7 +516,7 @@ lemma no_fail_callKernel:
   apply (rule corres_nofail)
    apply (rule corres_guard_imp)
      apply (rule kernel_corres)
-    apply force
+    apply (force simp: schact_is_rct_def)
    apply (simp add: sch_act_simple_def)
   apply metis
   done

proof/crefine/ARM_HYP/Detype_C.thy

@@ -1535,7 +1535,7 @@ lemma deleteObjects_ccorres':
              doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm
              bind_assoc modify_machinestate_assert_cnodes_swap
              modify_modify_bind)
-  apply (rule ccorres_stateAssert_fwd)
+  apply (rule ccorres_stateAssert_fwd)+
   apply (rule ccorres_stateAssert_after)
   apply (rule ccorres_from_vcg)
   apply (rule allI, rule conseqPre, vcg)

proof/crefine/ARM_HYP/Refine_C.thy

@@ -509,7 +509,7 @@ lemma no_fail_callKernel:
   apply (rule corres_nofail)
    apply (rule corres_guard_imp)
      apply (rule kernel_corres)
-    apply force
+    apply (force simp: schact_is_rct_def)
    apply (simp add: sch_act_simple_def)
   apply metis
   done

proof/crefine/RISCV64/Detype_C.thy

@@ -1544,7 +1544,7 @@ lemma deleteObjects_ccorres':
              doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm
              bind_assoc modify_machinestate_assert_cnodes_swap
              modify_modify_bind)
-  apply (rule ccorres_stateAssert_fwd)
+  apply (rule ccorres_stateAssert_fwd)+
   apply (rule ccorres_stateAssert_after)
   apply (rule ccorres_from_vcg)
   apply (rule allI, rule conseqPre, vcg)

proof/crefine/RISCV64/Refine_C.thy

@@ -493,7 +493,7 @@ lemma no_fail_callKernel:
   apply (rule corres_nofail)
    apply (rule corres_guard_imp)
      apply (rule kernel_corres)
-    apply (force simp: word_neq_0_conv)
+    apply (force simp: word_neq_0_conv schact_is_rct_def)
    apply (simp add: sch_act_simple_def)
   apply metis
   done

proof/crefine/X64/Detype_C.thy

@@ -1542,7 +1542,7 @@ lemma deleteObjects_ccorres':
              doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm
              bind_assoc modify_machinestate_assert_cnodes_swap
              modify_modify_bind)
-  apply (rule ccorres_stateAssert_fwd)
+  apply (rule ccorres_stateAssert_fwd)+
   apply (rule ccorres_stateAssert_after)
   apply (rule ccorres_from_vcg)
   apply (rule allI, rule conseqPre, vcg)

proof/crefine/X64/Refine_C.thy

@@ -495,7 +495,7 @@ lemma no_fail_callKernel:
   apply (rule corres_nofail)
    apply (rule corres_guard_imp)
      apply (rule kernel_corres)
-    apply (force simp: word_neq_0_conv)
+    apply (force simp: word_neq_0_conv schact_is_rct_def)
    apply (simp add: sch_act_simple_def)
   apply metis
   done

proof/infoflow/refine/ADT_IF_Refine.thy

@@ -282,8 +282,7 @@ locale ADT_IF_Refine_1 =
     "\<lbrace>K (uop_sane uop)\<rbrace> doUserOp_if uop tc \<lbrace>\<lambda>r s. (fst r) \<noteq> Some Interrupt\<rbrace>"
   and handleEvent_corres_arch_extras:
     "corres (dc \<oplus> dc)
-       (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)
-              and (\<lambda>s. scheduler_action s = resume_cur_thread))
+       (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and schact_is_rct)
        (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s)
               and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
               and arch_extras)
@@ -293,7 +292,7 @@ begin
 lemma kernel_entry_if_corres:
   "corres (prod_lift (dc \<oplus> dc))
      (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)
-            and (\<lambda>s. scheduler_action s = resume_cur_thread)
+            and schact_is_rct
             and (\<lambda>s. 0 < domain_time s) and valid_domain_list)
      (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s)
             and arch_extras
@@ -320,7 +319,7 @@ lemma kernel_entry_if_corres:
          apply (wp hoare_TrueI threadSet_invs_trivial thread_set_invs_trivial thread_set_ct_running
                    threadSet_ct_running' thread_set_not_state_valid_sched hoare_vcg_const_imp_lift
                    handle_event_domain_time_inv handle_interrupt_valid_domain_time
-                | simp add: tcb_cap_cases_def | wpc | wp (once) hoare_drop_imps)+
+                | simp add: tcb_cap_cases_def schact_is_rct_def | wpc | wp (once) hoare_drop_imps)+
    apply (fastforce simp: invs_def cur_tcb_def)
   apply force
   done
@@ -340,7 +339,7 @@ lemma kernelEntry_ex_abs[wp]:
   apply (rule_tac x=sa in exI)
   apply (clarsimp simp: domain_time_rel_eq domain_list_rel_eq)
   by (fastforce simp: ct_running_related ct_idle_related schedaction_related
-                      active_from_running' active_from_running)
+                      active_from_running' active_from_running schact_is_rct_def)
 
 lemma doUserOp_if_ct_in_state[wp]:
   "doUserOp_if f tc \<lbrace>ct_in_state' st\<rbrace>"
@@ -1272,7 +1271,7 @@ lemma haskell_to_abs:
         apply (rule corres_guard_imp)
           apply (rule kernel_entry_if_corres)
          apply clarsimp
-         apply ((clarsimp simp: full_invs_if_def full_invs_if'_def)+)[2]
+         apply ((clarsimp simp: full_invs_if_def full_invs_if'_def schact_is_rct_def)+)[2]
        apply (fastforce simp: prod_lift_def)
       apply (rule kernelEntry_if_empty_fail)
      apply (simp add: kernel_handle_preemption_if_def handlePreemption_H_if_def)

proof/infoflow/refine/ADT_IF_Refine_C.thy

@@ -384,7 +384,7 @@ lemma kernelEntry_corres_C:
    apply (erule no_fail_pre)
    apply (clarsimp simp: all_invs'_def)
    apply (rule exI, rule conjI, assumption)
-   apply clarsimp
+   apply (clarsimp simp: schact_is_rct_def)
   apply (simp only: bind_assoc)
   apply (simp add: getCurThread_def)
   apply (rule corres_guard_imp)
@@ -413,7 +413,7 @@ lemma kernelEntry_corres_C:
         apply (rule threadSet_all_invs_triv'[where e=e])
        apply (clarsimp simp: all_invs'_def)
        apply (rule exI, (rule conjI, assumption)+)
-       subgoal by force
+       subgoal by (force simp: schact_is_rct_def)
       apply simp
       apply (rule hoare_post_taut[where P=\<top>])
      apply wp+

proof/infoflow/refine/ARM/ArchADT_IF_Refine.thy

@@ -427,8 +427,7 @@ lemma doUserOp_if_no_interrupt[ADT_IF_Refine_assms]:
 
 lemma handleEvent_corres_arch_extras[ADT_IF_Refine_assms]:
     "corres (dc \<oplus> dc)
-       (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)
-              and (\<lambda>s. scheduler_action s = resume_cur_thread))
+       (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and schact_is_rct)
        (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s)
               and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
               and arch_extras)

proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy

@@ -374,8 +374,7 @@ lemma doUserOp_if_no_interrupt[ADT_IF_Refine_assms]:
 
 lemma handleEvent_corres_arch_extras[ADT_IF_Refine_assms]:
     "corres (dc \<oplus> dc)
-       (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s)
-              and (\<lambda>s. scheduler_action s = resume_cur_thread))
+       (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and schact_is_rct)
        (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s)
               and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
               and arch_extras)

proof/refine/AARCH64/Arch_R.thy

@@ -133,7 +133,7 @@ lemma set_cap_device_and_range_aligned:
 lemma performASIDControlInvocation_corres:
   "asid_ci_map i = i' \<Longrightarrow>
   corres dc
-         (einvs and ct_active and valid_aci i)
+         (einvs and ct_active and valid_aci i and schact_is_rct)
          (invs' and ct_active' and valid_aci' i')
          (perform_asid_control_invocation i)
          (performASIDControlInvocation i')"
@@ -274,6 +274,7 @@ lemma performASIDControlInvocation_corres:
          subgoal by (fastforce simp:cte_wp_at_caps_of_state descendants_range_def2 empty_descendants_range_in)
        apply (fold_subgoals (prefix))[2]
      subgoal premises prems using prems by (clarsimp simp:invs_def valid_state_def)+
+      apply (clarsimp simp: schact_is_rct_def)
      apply (clarsimp simp:cte_wp_at_caps_of_state)
     apply (drule detype_locale.non_null_present)
      apply (fastforce simp:cte_wp_at_caps_of_state)
@@ -332,26 +333,27 @@ lemma performASIDControlInvocation_corres:
          simp_all add: is_simple_cap'_def isCap_simps descendants_range'_def2
                        null_filter_descendants_of'[OF null_filter_simp']
                        capAligned_def asid_low_bits_def)
-      apply (erule descendants_range_caps_no_overlapI')
-       apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq)
-      apply (simp add:empty_descendants_range_in')
-     apply (simp add:word_bits_def bit_simps)
-    apply (rule is_aligned_weaken)
-     apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified])
-    apply (simp add:pageBits_def)
+       apply (erule descendants_range_caps_no_overlapI')
+        apply (fastforce simp:cte_wp_at_ctes_of is_aligned_neg_mask_eq)
+       apply (simp add:empty_descendants_range_in')
+      apply (simp add:word_bits_def bit_simps)
+     apply (rule is_aligned_weaken)
+      apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified])
+     apply (simp add:pageBits_def)
+    apply clarsimp
+    apply (drule(1) cte_cap_in_untyped_range)
+         apply (fastforce simp:cte_wp_at_ctes_of)
+        apply assumption+
+     apply fastforce
+    apply simp
    apply clarsimp
-   apply (drule(1) cte_cap_in_untyped_range)
-        apply (fastforce simp:cte_wp_at_ctes_of)
+   apply (drule (1) cte_cap_in_untyped_range)
+        apply (fastforce simp add: cte_wp_at_ctes_of)
        apply assumption+
+     apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of)
     apply fastforce
    apply simp
   apply clarsimp
-  apply (drule (1) cte_cap_in_untyped_range)
-       apply (fastforce simp add: cte_wp_at_ctes_of)
-      apply assumption+
-    apply (clarsimp simp: invs'_def valid_state'_def if_unsafe_then_cap'_def cte_wp_at_ctes_of)
-   apply fastforce
-  apply simp
   done
 
 definition vcpu_invocation_map :: "vcpu_invocation \<Rightarrow> vcpuinvocation" where
@@ -1378,7 +1380,7 @@ lemma performARMVCPUInvocation_corres:
 lemma arch_performInvocation_corres:
   "archinv_relation ai ai' \<Longrightarrow>
    corres (dc \<oplus> (=))
-     (einvs and ct_active and valid_arch_inv ai)
+     (einvs and ct_active and valid_arch_inv ai and schact_is_rct)
      (invs' and ct_active' and valid_arch_inv' ai')
      (arch_perform_invocation ai) (Arch.performInvocation ai')"
   apply (clarsimp simp: arch_perform_invocation_def