rt spec+proof: prove refill_budget_check_ccorres

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

proof/crefine/RISCV64/SchedContext_C.thy

@@ -11,90 +11,6 @@ begin
 
 context kernel_m begin
 
-lemma getRefillSize_exs_valid[wp]:
-  "\<lbrace>(=) s\<rbrace> getRefillSize scPtr \<lbrace>\<lambda>r. (=) s\<rbrace>"
-  by (wpsimp simp: getRefillSize_def)
-
-crunch getRefillSize
- for (empty_fail) empty_fail[wp]
-
-lemma refill_add_tail_ccorres:
-  "ccorres dc xfdc
-     (active_sc_at' scPtr and invs')
-     (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> {s'. crefill_relation new (refill_' s')}) []
-     (refillAddTail scPtr new) (Call refill_add_tail_'proc)"
-  supply sched_context_C_size[simp del] refill_C_size[simp del] len_bit0[simp del]
-
-  apply (simp add: refillAddTail_def)
-  apply (rule ccorres_symb_exec_l'[rotated, OF _ getRefillSize_sp]; wpsimp)
-  apply (rule ccorres_symb_exec_l'[rotated, OF _ get_sc_sp']; wpsimp?)
-  apply (rule ccorres_symb_exec_l'[rotated, OF _ assert_sp]; wpsimp)
-
-  apply (cinit' lift: sc_' refill_' simp: updateRefillIndex_def)
-   apply (rule ccorres_move_c_guard_sc)
-   apply (ctac add: refill_next_ccorres)
-     apply (rule ccorres_move_c_guard_sc)
-     apply clarsimp
-     apply (rule ccorres_split_nothrow[where r'=dc and xf'=xfdc])
-         apply (rule_tac P=\<top> in updateSchedContext_ccorres_lemma2)
-           apply vcg
-          apply fastforce
-         apply clarsimp
-         apply (rule_tac sc'="scRefillTail_C_update (\<lambda>_. new_tail) sc'"
-                      in rf_sr_sc_update_no_refill_buffer_update2;
-                fastforce?)
-           apply (clarsimp simp: typ_heap_simps')
-          apply (clarsimp simp: csched_context_relation_def)
-         apply (fastforce intro: refill_buffer_relation_sc_no_refills_update)
-        apply ceqv
-       apply (rule_tac P="\<lambda>sc. scRefillTail sc = unat new_tail"
-                   and P'="active_sc_at' scPtr and invs'"
-                    in updateSchedContext_ccorres_lemma3)
-         apply vcg
-        apply fastforce
-       apply normalise_obj_at'
-       apply (frule (1) sc_ko_at_valid_objs_valid_sc'[OF _ invs_valid_objs'])
-       apply (intro conjI)
-          apply (fastforce dest: sc_at_h_t_valid[rotated])
-         apply (rule disjCI2)
-         apply (rule_tac n="length (scRefills sc)" in array_assertion_shrink_right)
-          apply (fastforce intro: sc_at_array_assertion'
-                            simp: valid_sched_context'_def MIN_REFILLS_def)
-         apply (clarsimp simp: typ_heap_simps valid_sched_context'_def obj_at_simps
-                               active_sc_at'_def csched_context_relation_def)
-        apply (frule rf_sr_refill_buffer_relation)
-        apply (frule_tac n="scRefillTail sc" in h_t_valid_refill; fastforce?)
-          apply (clarsimp simp: valid_sched_context'_def active_sc_at'_def obj_at'_def)
-         apply fastforce
-        apply (clarsimp simp: sc_ptr_to_crefill_ptr_def typ_heap_simps csched_context_relation_def)
-       apply (clarsimp simp: ret__ptr_to_struct_refill_C_'_update_rf_sr_helper
-                       cong: StateSpace.state.fold_congs)
-       apply (rule_tac old_sc=sc and n="scRefillTail sc" and refill=new and refill'=refill
-                    in rf_sr_refill_update2;
-              fastforce?)
-          apply (clarsimp simp: valid_sched_context'_def active_sc_at'_def obj_at'_def)
-         apply (fastforce simp: sched_context.expand)
-        apply (clarsimp simp: typ_heap_simps sc_ptr_to_crefill_ptr_def csched_context_relation_def)
-       apply (clarsimp simp: csched_context_relation_def)
-      apply ((rule hoare_vcg_conj_lift
-              | wpsimp wp: updateSchedContext_active_sc_at' updateSchedContext_refills_invs'
-              | wpsimp wp: updateSchedContext_wp)+)[1]
-     apply vcg
-    apply (wpsimp wp: getRefillNext_wp)
-   apply vcg
-  apply normalise_obj_at'
-  apply (frule (1) sc_ko_at_valid_objs_valid_sc'[OF _ invs_valid_objs'])
-  apply (elim conjE)
-  apply (frule (1) length_scRefills_bounded)
-  apply (intro conjI)
-       apply fastforce
-      apply (clarsimp simp: valid_sched_context'_def word_bits_len_of refillSizeBytes_def)
-     apply (fastforce simp: obj_at'_def objBits_simps opt_map_def ps_clear_def)
-    apply (fastforce simp: valid_sched_context'_def refillNext_def refillSize_def split: if_splits)
-   apply (clarsimp simp: valid_sched_context_size'_def)
-  apply (fastforce dest: obj_at_cslift_sc simp: csched_context_relation_def typ_heap_simps)
-  done
-
 lemma maybe_add_empty_tail_ccorres:
   "ccorres dc xfdc
      (active_sc_at' scPtr and invs') \<lbrace>\<acute>sc = Ptr scPtr\<rbrace> []