haskell+design+proof: add deletionIsSafe2 assert to deleteObjects

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