theory Retype_C

lemma placeNewDataObject_ccorres:
  "ccorresG rf_sr \<Gamma> dc xfdc
  (createObject_hs_preconds regionBase newType us devMem
      and K (APIType_capBits newType us = pageBits + us))
  ({s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s
      \<and> (\<not> devMem \<longrightarrow> heap_list_is_zero (hrs_mem (t_hrs_' (globals s))) regionBase
          (2 ^ (pageBits + us)))})
  hs
  (placeNewDataObject regionBase us devMem)
  (Cond {s. devMem}
    (global_htd_update (\<lambda>s. (ptr_retyps (2^us) (Ptr regionBase :: user_data_device_C ptr))))
    (global_htd_update (\<lambda>s. (ptr_retyps (2^us) (Ptr regionBase :: user_data_C ptr))))
  )" apply (cases devMem) apply (simp add: placeNewDataObject_def ccorres_cond_univ_iff) apply (rule ccorres_guard_imp, rule placeNewObject_user_data_device, simp_all) apply (clarsimp simp: createObject_hs_preconds_def invs'_def
                         valid_state'_def valid_pspace'_def) apply (simp add: placeNewDataObject_def ccorres_cond_empty_iff) apply (rule ccorres_guard_imp, rule placeNewObject_user_data, simp_all) apply (clarsimp simp: createObject_hs_preconds_def invs'_def
                        valid_state'_def valid_pspace'_def) apply (frule range_cover.sz(1), simp add: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (createObject_hs_preconds regionBase newType us devMem and K (APIType_capBits newType us = pageBits + us)) {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> (\<not> devMem \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0)} hs (placeNewDataObject regionBase us devMem) (IF devMem THEN
  Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase))))
ELSE
  Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase))))
FI) proof (prove)
goal (2 subgoals):
 1. devMem \<Longrightarrow> ccorres dc xfdc (createObject_hs_preconds regionBase newType us devMem and K (APIType_capBits newType us = pageBits + us)) {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> (\<not> devMem \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0)} hs (placeNewDataObject regionBase us devMem) (IF devMem THEN
  Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase))))
ELSE
  Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase))))
FI)
 2. \<not> devMem \<Longrightarrow> ccorres dc xfdc (createObject_hs_preconds regionBase newType us devMem and K (APIType_capBits newType us = pageBits + us)) {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> (\<not> devMem \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0)} hs (placeNewDataObject regionBase us devMem) (IF devMem THEN
  Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase))))
ELSE
  Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase))))
FI) proof (prove)
goal (2 subgoals):
 1. devMem \<Longrightarrow> ccorres dc xfdc (createObject_hs_preconds regionBase newType us True and (\<lambda>y. APIType_capBits newType us = pageBits + us)) {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s} hs (placeNewObject regionBase UserDataDevice us) (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase)))))
 2. \<not> devMem \<Longrightarrow> ccorres dc xfdc (createObject_hs_preconds regionBase newType us devMem and K (APIType_capBits newType us = pageBits + us)) {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> (\<not> devMem \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0)} hs (placeNewDataObject regionBase us devMem) (IF devMem THEN
  Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase))))
ELSE
  Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase))))
FI) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>devMem; createObject_hs_preconds regionBase newType us True s \<and> APIType_capBits newType us = pageBits + us\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> valid_objs' s \<and> untyped_ranges_zero' s \<and> caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} s \<and> pspace_no_overlap' regionBase (pageBits + us) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> 2 ^ (pageBits + us) \<le> gsMaxObjectSize s \<and> regionBase \<noteq> 0 \<and> range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0) \<and> {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}
 2. \<not> devMem \<Longrightarrow> ccorres dc xfdc (createObject_hs_preconds regionBase newType us False and (\<lambda>y. APIType_capBits newType us = pageBits + us)) {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0} hs (placeNewDataObject regionBase us False) (Cond {} (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase))))) (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))))) proof (prove)
goal (1 subgoal):
 1. \<not> devMem \<Longrightarrow> ccorres dc xfdc (createObject_hs_preconds regionBase newType us False and (\<lambda>y. APIType_capBits newType us = pageBits + us)) {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0} hs (placeNewDataObject regionBase us False) (Cond {} (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_device_C) regionBase))))) (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase)))))) proof (prove)
goal (1 subgoal):
 1. \<not> devMem \<Longrightarrow> ccorres dc xfdc (createObject_hs_preconds regionBase newType us False and (\<lambda>y. APIType_capBits newType us = pageBits + us)) {s. region_actually_is_bytes regionBase (2 ^ (pageBits + us)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ (pageBits + us)) regionBase = replicate (2 ^ (pageBits + us)) 0} hs (placeNewObject regionBase UserData us) (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase) (hrs_htd \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps (2 ^ us) (PTR(user_data_C) regionBase))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> devMem; createObject_hs_preconds regionBase newType us False s \<and> APIType_capBits newType us = pageBits + us\<rbrakk> \<Longrightarrow> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' regionBase (pageBits + us) s \<and> Invariants_H.valid_queues s \<and> valid_machine_state' s \<and> valid_objs' s \<and> untyped_ranges_zero' s \<and> caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} s \<and> sym_refs (state_refs_of' s) \<and> 2 ^ (pageBits + us) \<le> gsMaxObjectSize s \<and> regionBase \<noteq> 0 \<and> range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0) \<and> us < word_bits \<and> {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> devMem; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; kernel_state.ksDomSchedule s = kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (kernel_state.ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; pspace_no_overlap' regionBase (pageBits + us) s; caps_overlap_reserved' {regionBase..+2 ^ (pageBits + us)} s; 2 ^ (pageBits + us) \<le> gsMaxObjectSize s; regionBase \<noteq> 0; {regionBase..+2 ^ (pageBits + us)} \<inter> kernel_data_refs = {}; range_cover regionBase (pageBits + us) (pageBits + us) (Suc 0); newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> us \<le> maxUntypedSizeBits; newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28; newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> us; newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; APIType_capBits newType us = pageBits + us\<rbrakk> \<Longrightarrow> us < word_bits proof (prove)
goal:
No subgoals!