rt crefine: fixup after removing assumption from ccorres_While

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Jul 15, 2024 · b2733e7 · b2733e7
1 parent eb57a8f
commit b2733e7
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 31 deletions.
diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy
@@ -716,22 +716,22 @@ lemma refill_unblock_check_ccorres:
                                        carch_state_relation_def cmachine_state_relation_def)
                 apply ceqv
                apply (clarsimp simp: whileAnno_def refillHeadOverlappingLoop_def)
+               apply (rule ccorres_handlers_weaken)
                apply (rule_tac G="\<lambda>_. ?abs and active_sc_at' scPtr" and G'=UNIV in ccorres_While')
-                     apply (rule ccorres_guard_imp)
-                       apply (ctac add: merge_overlapping_head_refill_ccorres)
-                      apply (clarsimp simp: active_sc_at'_rewrite runReaderT_def)
-                      apply (fastforce dest: use_ovalid[OF refillHeadOverlapping_refillSize]
-                                      intro: valid_objs'_valid_refills')
-                     apply clarsimp
-                    apply (clarsimp simp: runReaderT_def)
                     apply (rule ccorres_guard_imp)
-                      apply (ctac add: refill_head_overlapping_ccorres)
-                     apply clarsimp
+                      apply (ctac add: merge_overlapping_head_refill_ccorres)
+                     apply (clarsimp simp: active_sc_at'_rewrite runReaderT_def)
+                     apply (fastforce dest: use_ovalid[OF refillHeadOverlapping_refillSize]
+                                     intro: valid_objs'_valid_refills')
                     apply clarsimp
-                   apply wpsimp
-                   apply (clarsimp simp: active_sc_at'_def)
-                  apply (wpsimp wp: no_ofail_refillHeadOverlapping simp: runReaderT_def)
+                   apply (clarsimp simp: runReaderT_def)
+                   apply (rule ccorres_guard_imp)
+                     apply (ctac add: refill_head_overlapping_ccorres)
+                    apply clarsimp
+                   apply clarsimp
+                  apply wpsimp
                   apply (clarsimp simp: active_sc_at'_def)
+                  apply (wpsimp wp: no_ofail_refillHeadOverlapping simp: runReaderT_def)
                  apply (wpsimp wp: updateRefillHd_valid_objs' mergeOverlappingRefills_valid_objs')
                  apply (clarsimp simp: active_sc_at'_rewrite runReaderT_def)
                  apply (fastforce dest: use_ovalid[OF refillHeadOverlapping_refillSize]

diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy
@@ -4967,27 +4967,24 @@ lemma find_time_after_ccorres:
                                   \<and> (\<forall>ptr. r = Some ptr \<longrightarrow> (tcbInReleaseQueue |< tcbs_of' s) ptr)"
                      and G'=UNIV
                       in ccorres_While')
-                prefer 2
-                apply (rule ccorres_guard_imp)
-                 apply (ctac add: time_after_ccorres)
-                apply fastforce
+              prefer 2
+              apply (rule ccorres_guard_imp)
+                apply (ctac add: time_after_ccorres)
                apply fastforce
-              apply (rule stronger_ccorres_guard_imp)
-                apply (rule ccorres_pre_getObject_tcb)
-                apply (rule ccorres_Guard)
-                apply (rule ccorres_return[where R=\<top>])
-                apply vcg
-                apply clarsimp
-                apply (erule CollectD)
-               apply fastforce
-              apply (clarsimp simp: typ_heap_simps)
-              apply (frule timeAfter_SomeTrueD)
-              apply (clarsimp simp: typ_heap_simps option_to_ctcb_ptr_def opt_pred_def opt_map_def
-                                    obj_at'_def ctcb_relation_def
-                             split: option.splits)
-             apply wpsimp
+              apply fastforce
+             apply (rule stronger_ccorres_guard_imp)
+               apply (rule ccorres_pre_getObject_tcb)
+               apply (rule ccorres_Guard)
+               apply (rule ccorres_return[where R=\<top>])
+               apply vcg
+               apply clarsimp
+               apply (erule CollectD)
+              apply fastforce
+             apply (clarsimp simp: typ_heap_simps)
              apply (frule timeAfter_SomeTrueD)
-             apply clarsimp
+             apply (clarsimp simp: typ_heap_simps option_to_ctcb_ptr_def opt_pred_def opt_map_def
+                                   obj_at'_def ctcb_relation_def
+                            split: option.splits)
             apply (wpsimp wp: no_ofail_timeAfter)
            apply (wpsimp wp: getTCB_wp)
            apply (frule timeAfter_SomeTrueD)