proof: update for removed hoare_gets

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Jul 9, 2024 · 1576f11 · 1576f11
1 parent f4107b6
commit 1576f11
Show file tree

Hide file tree

Showing 14 changed files with 62 additions and 66 deletions.
diff --git a/proof/drefine/Syscall_DR.thy b/proof/drefine/Syscall_DR.thy
@@ -1645,9 +1645,9 @@ lemma handle_event_corres:
         apply wp[1]
         apply clarsimp
         apply (frule (1) ct_running_not_idle_etc)
-        apply (fastforce simp: st_tcb_at_def obj_at_def generates_pending_def gets_def get_def
-                               valid_fault_def
-                        split: Structures_A.thread_state.splits)+
+        apply (fastforce simp: st_tcb_at_def obj_at_def generates_pending_def valid_fault_def
+                        split: Structures_A.thread_state.splits)
+       apply wpsimp+
      apply (rule corres_symb_exec_r[OF handle_fault_corres])
        apply wp[1]
        apply clarsimp

diff --git a/proof/infoflow/ARM/ArchArch_IF.thy b/proof/infoflow/ARM/ArchArch_IF.thy
@@ -804,9 +804,10 @@ lemma arm_asid_table_update_reads_respects:
    apply (rule modify_ev2)
    apply clarsimp
    apply (drule (1) is_subject_kheap_eq[rotated])
-   apply (auto simp: reads_equiv_def2 affects_equiv_def2 states_equiv_for_def equiv_for_def
-             intro!: equiv_asids_arm_asid_table_update)
-   done
+   apply (fastforce simp: reads_equiv_def2 affects_equiv_def2 states_equiv_for_def equiv_for_def
+                  intro!: equiv_asids_arm_asid_table_update)
+  apply wpsimp
+  done
 
 lemma perform_asid_control_invocation_reads_respects:
   notes K_bind_ev[wp del]

diff --git a/proof/infoflow/InfoFlow_IF.thy b/proof/infoflow/InfoFlow_IF.thy
@@ -957,8 +957,9 @@ lemma do_machine_op_rev:
        apply (clarsimp simp: select_f_def equiv_valid_2_def)
        apply (insert equiv_dmo, clarsimp simp: equiv_valid_def2 equiv_valid_2_def)[1]
        apply blast
-    apply (wp select_f_inv)+
+      apply (wpsimp wp: select_f_inv)+
     apply (fastforce simp: select_f_def dest: state_unchanged[OF mo_inv])+
+  apply wpsimp
   done
 
 end

diff --git a/proof/infoflow/RISCV64/ArchArch_IF.thy b/proof/infoflow/RISCV64/ArchArch_IF.thy
@@ -425,8 +425,9 @@ lemma riscv_asid_table_update_reads_respects:
    apply (rule modify_ev2)
    apply clarsimp
    apply (drule (1) is_subject_kheap_eq[rotated])
-   apply (auto simp: reads_equiv_def2 affects_equiv_def2 states_equiv_for_def equiv_for_def
-             intro!: equiv_asids_riscv_asid_table_update)
+   apply (fastforce simp: reads_equiv_def2 affects_equiv_def2 states_equiv_for_def equiv_for_def
+                  intro!: equiv_asids_riscv_asid_table_update)
+  apply wpsimp
   done
 
 lemma perform_asid_control_invocation_reads_respects:

diff --git a/proof/refine/AARCH64/Retype_R.thy b/proof/refine/AARCH64/Retype_R.thy
@@ -4296,20 +4296,21 @@ lemma createNewCaps_idle'[wp]:
              split del: if_split)
   apply (cases ty, simp_all add: Arch_createNewCaps_def
                       split del: if_split)
-         apply (rename_tac apiobject_type)
-         apply (case_tac apiobject_type, simp_all split del: if_split)[1]
-             apply (wp, simp)
+        apply (rename_tac apiobject_type)
+        apply (case_tac apiobject_type, simp_all split del: if_split)[1]
+            apply wpsimp
+           (* The following step does not use wpsimp to avoid clarsimp_no_cond, which for some reason
+              leads to a failed proof state. If this could be fixed then the inclusion of
+              classic_wp_pre could also be removed. *)
            including classic_wp_pre
-           apply (wp mapM_x_wp'
-                     createObjects_idle'
-                     threadSet_idle'
-                   | simp add: projectKO_opt_tcb projectKO_opt_cte mult_2
-                               makeObject_cte makeObject_tcb archObjSize_def
-                               tcb_cte_cases_def objBitsKO_def APIType_capBits_def
-                               objBits_def createObjects_def cteSizeBits_def
-                   | simp add: field_simps
-                   | intro conjI impI
-                   | fastforce simp: curDomain_def)+
+           apply (wp mapM_x_wp' createObjects_idle' threadSet_idle'
+                  | simp add: projectKO_opt_tcb projectKO_opt_cte mult_2
+                              makeObject_cte makeObject_tcb archObjSize_def
+                              tcb_cte_cases_def objBitsKO_def APIType_capBits_def
+                              objBits_def createObjects_def cteSizeBits_def
+                  | simp add: field_simps
+                  | intro conjI impI
+                  | clarsimp simp: curDomain_def)+
   done
 
 crunch createNewCaps

diff --git a/proof/refine/AARCH64/Schedule_R.thy b/proof/refine/AARCH64/Schedule_R.thy
@@ -2124,7 +2124,7 @@ lemma schedule_corres:
                           tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp
                      del: gets_wp
                   | strengthen valid_objs'_valid_tcbs')+
-       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets)
+       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong)
        apply (wp gets_wp)+
 
    (* abstract final subgoal *)

diff --git a/proof/refine/ARM/Retype_R.thy b/proof/refine/ARM/Retype_R.thy
@@ -4277,20 +4277,17 @@ lemma createNewCaps_idle'[wp]:
              split del: if_split)
   apply (cases ty, simp_all add: Arch_createNewCaps_def
                       split del: if_split)
-         apply (rename_tac apiobject_type)
-         apply (case_tac apiobject_type, simp_all split del: if_split)[1]
-             apply (wp, simp)
-           including classic_wp_pre
-           apply (wp mapM_x_wp'
-                     createObjects_idle'
-                     threadSet_idle'
-                   | simp add: projectKO_opt_tcb projectKO_opt_cte
-                               makeObject_cte makeObject_tcb archObjSize_def
-                               tcb_cte_cases_def objBitsKO_def APIType_capBits_def
-                               ptBits_def pdBits_def pageBits_def objBits_def
-                               createObjects_def pteBits_def pdeBits_def
-                   | intro conjI impI
-                   | fastforce simp: curDomain_def)+
+        apply (rename_tac apiobject_type)
+        apply (case_tac apiobject_type, simp_all split del: if_split)[1]
+            apply wpsimp
+           apply (wpsimp wp: mapM_x_wp' createObjects_idle' threadSet_idle'
+                  | simp add: projectKO_opt_tcb projectKO_opt_cte
+                              makeObject_cte makeObject_tcb archObjSize_def
+                              tcb_cte_cases_def objBitsKO_def APIType_capBits_def
+                              ptBits_def pdBits_def pageBits_def objBits_def
+                              createObjects_def pteBits_def pdeBits_def
+                  | intro conjI impI
+                  | clarsimp simp: curDomain_def)+
   done
 
 crunch createNewCaps

diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy
@@ -1910,7 +1910,7 @@ lemma schedule_corres:
                           tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp
                      del: gets_wp
                   | strengthen valid_objs'_valid_tcbs')+
-       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets)
+       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong)
        apply (wp gets_wp)+
 
    (* abstract final subgoal *)

diff --git a/proof/refine/ARM_HYP/Retype_R.thy b/proof/refine/ARM_HYP/Retype_R.thy
@@ -4351,18 +4351,19 @@ lemma createNewCaps_idle'[wp]:
                       split del: if_split)
          apply (rename_tac apiobject_type)
          apply (case_tac apiobject_type, simp_all split del: if_split)[1]
-             apply (wp, simp)
-           including classic_wp_pre
-           apply (wp mapM_x_wp'
-                     createObjects_idle'
-                     threadSet_idle'
+             apply wpsimp
+            (* The following step does not use wpsimp to avoid clarsimp_no_cond, which for some reason
+               leads to a failed proof state. If this could be fixed then the inclusion of
+               classic_wp_pre could also be removed. *)
+            including classic_wp_pre
+            apply (wp mapM_x_wp' createObjects_idle' threadSet_idle'
                    | simp add: projectKO_opt_tcb projectKO_opt_cte
                                makeObject_cte makeObject_tcb archObjSize_def
                                tcb_cte_cases_def objBitsKO_def APIType_capBits_def
                                vspace_bits_defs objBits_def
                                createObjects_def
                    | intro conjI impI
-                   | fastforce simp: curDomain_def)+
+                   | clarsimp simp: curDomain_def)+
   done
 
 crunch createNewCaps

diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy
@@ -2109,7 +2109,7 @@ lemma schedule_corres:
                           tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp
                      del: gets_wp
                   | strengthen valid_objs'_valid_tcbs' invs_valid_pspace')+
-       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets)
+       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong)
        apply (wp gets_wp)+
 
    (* abstract final subgoal *)

diff --git a/proof/refine/RISCV64/Retype_R.thy b/proof/refine/RISCV64/Retype_R.thy
@@ -4223,19 +4223,16 @@ lemma createNewCaps_idle'[wp]:
              split del: if_split)
   apply (cases ty, simp_all add: Arch_createNewCaps_def
                       split del: if_split)
-         apply (rename_tac apiobject_type)
-         apply (case_tac apiobject_type, simp_all split del: if_split)[1]
-             apply (wp, simp)
-           including classic_wp_pre
-           apply (wp mapM_x_wp'
-                     createObjects_idle'
-                     threadSet_idle'
-                   | simp add: projectKO_opt_tcb projectKO_opt_cte
-                               makeObject_cte makeObject_tcb archObjSize_def
-                               tcb_cte_cases_def objBitsKO_def APIType_capBits_def
-                               objBits_def createObjects_def bit_simps cteSizeBits_def
-                   | intro conjI impI
-                   | fastforce simp: curDomain_def)+
+      apply (rename_tac apiobject_type)
+      apply (case_tac apiobject_type, simp_all split del: if_split)[1]
+          apply wpsimp
+         apply (wpsimp wp: mapM_x_wp' createObjects_idle' threadSet_idle'
+                | simp add: projectKO_opt_tcb projectKO_opt_cte
+                            makeObject_cte makeObject_tcb archObjSize_def
+                            tcb_cte_cases_def objBitsKO_def APIType_capBits_def
+                            objBits_def createObjects_def bit_simps cteSizeBits_def
+                | intro conjI impI
+                | clarsimp simp: curDomain_def)+
   done
 
 crunch createNewCaps

diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy
@@ -1967,7 +1967,7 @@ lemma schedule_corres:
                           tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp
                      del: gets_wp
                   | strengthen valid_objs'_valid_tcbs')+
-       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets)
+       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong)
        apply (wp gets_wp)+
 
    (* abstract final subgoal *)

diff --git a/proof/refine/X64/Retype_R.thy b/proof/refine/X64/Retype_R.thy
@@ -4396,17 +4396,14 @@ lemma createNewCaps_idle'[wp]:
                       split del: if_split)
          apply (rename_tac apiobject_type)
          apply (case_tac apiobject_type, simp_all split del: if_split)[1]
-             apply (wp, simp)
-           including classic_wp_pre
-           apply (wp mapM_x_wp'
-                     createObjects_idle'
-                     threadSet_idle'
+             apply wpsimp
+            apply (wpsimp wp: mapM_x_wp' createObjects_idle' threadSet_idle'
                    | simp add: projectKO_opt_tcb projectKO_opt_cte
                                makeObject_cte makeObject_tcb archObjSize_def
                                tcb_cte_cases_def objBitsKO_def APIType_capBits_def
                                objBits_def createObjects_def bit_simps
                    | intro conjI impI
-                   | fastforce simp: curDomain_def)+
+                   | clarsimp simp: curDomain_def)+
   done
 
 crunch createNewCaps

diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy
@@ -1911,7 +1911,7 @@ lemma schedule_corres:
                           tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp
                      del: gets_wp
                   | strengthen valid_objs'_valid_tcbs')+
-       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets)
+       apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong)
        apply (wp gets_wp)+
 
    (* abstract final subgoal *)