theory Retype_C

lemma gsCNodes_update_ccorres:
  "ccorresG rf_sr G dc xf (\<lambda>_. bits = sz + 4)
        \<lbrace> h_t_array_valid (hrs_htd \<acute>t_hrs) (cte_Ptr ptr) (2 ^ sz) \<rbrace> hs
     (modify (gsCNodes_update (\<lambda>m a. if a = ptr then Some sz else m a)))
     (Basic (globals_update (ghost'state_'_update
                  (gs_new_cnodes sz ptr bits))))" apply (rule ccorres_from_vcg) apply vcg_step apply (clarsimp simp: split_def simpler_modify_def gs_new_cnodes_def) apply (case_tac "ghost'state_' (globals x)") apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def fun_upd_def
                        carch_state_relation_def cmachine_state_relation_def
                        ghost_size_rel_def ghost_assertion_data_get_def
                 cong: if_cong) apply (rule cvariable_array_ptr_upd[unfolded fun_upd_def], simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG rf_sr G dc xf (\<lambda>_. bits = sz + 4) \<lbrace>h_t_array_valid (hrs_htd \<acute>t_hrs) (cte_Ptr ptr) (2 ^ sz)\<rbrace> hs (modify (gsCNodes_update (\<lambda>m a. if a = ptr then Some sz else m a))) (\<acute>globals :== ghost'state_'_update (gs_new_cnodes sz ptr bits)) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. G\<turnstile> {s. bits = sz + 4 \<and> s \<in> \<lbrace>h_t_array_valid (hrs_htd \<acute>t_hrs) (cte_Ptr ptr) (2 ^ sz)\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} \<acute>globals :== ghost'state_'_update (gs_new_cnodes sz ptr bits) {s. \<exists>(rv, \<sigma>')\<in>fst (modify (gsCNodes_update (\<lambda>m a. if a = ptr then Some sz else m a)) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xf s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. bits = sz + 4 \<and> h_t_array_valid (hrs_htd (t_hrs_' (globals s))) (cte_Ptr ptr) (2 ^ sz) \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (modify (gsCNodes_update (\<lambda>m a. if a = ptr then Some sz else m a)) \<sigma>). (\<sigma>', globals_update (ghost'state_'_update (gs_new_cnodes sz ptr bits)) s) \<in> rf_sr \<and> dc rv (xf (globals_update (ghost'state_'_update (gs_new_cnodes sz ptr bits)) s))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>bits = sz + 4; h_t_array_valid (hrs_htd (t_hrs_' (globals x))) (cte_Ptr ptr) (2 ^ sz); (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (gsCNodes_update (\<lambda>m a. if a = ptr then Some sz else m a) \<sigma>, globals_update (ghost'state_'_update (\<lambda>gs. (fst gs, \<lambda>x. if x = ptr then Some sz else fst (snd gs) x, snd (snd gs)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x a b c. \<lbrakk>bits = sz + 4; h_t_array_valid (hrs_htd (t_hrs_' (globals x))) (cte_Ptr ptr) (2 ^ sz); (\<sigma>, x) \<in> rf_sr; ghost'state_' (globals x) = (a, b, c)\<rbrakk> \<Longrightarrow> (gsCNodes_update (\<lambda>m a. if a = ptr then Some sz else m a) \<sigma>, globals_update (ghost'state_'_update (\<lambda>gs. (fst gs, \<lambda>x. if x = ptr then Some sz else fst (snd gs) x, snd (snd gs)))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x c. \<lbrakk>bits = sz + 4; h_t_array_valid (hrs_htd (t_hrs_' (globals x))) (cte_Ptr ptr) (2 ^ sz); ghost'state_' (globals x) = (gsUserPages \<sigma>, gsCNodes \<sigma>, c); cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); c (word_of_int cap_get_capSizeBits_'proc) = 0 \<and> gsMaxObjectSize \<sigma> = CARD(32 word) \<or> 0 < gsMaxObjectSize \<sigma> \<and> gsMaxObjectSize \<sigma> = unat (c (word_of_int cap_get_capSizeBits_'proc)); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cvariable_array_map_relation (\<lambda>a. if a = ptr then Some sz else gsCNodes \<sigma> a) ((^) 2) cte_Ptr (hrs_htd (t_hrs_' (globals x))) proof (prove)
goal:
No subgoals!