kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_R

lemma createObjects_pspace_domain_valid:
  "\<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0
      \<and> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {}
      \<and> pspace_domain_valid s\<rbrace>
       createObjects ptr n val gbits
   \<lbrace>\<lambda>_. pspace_domain_valid\<rbrace>" apply (simp add: createObjects_def) apply (wp createObjects_pspace_domain_valid'[where sz=sz]) apply (simp add: objBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> pspace_domain_valid s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>_. pspace_domain_valid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> pspace_domain_valid s\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_. pspace_domain_valid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> pspace_domain_valid s \<Longrightarrow> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> kernel_data_refs = {} \<and> pspace_domain_valid s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createNewCaps_ct_idle_or_in_cur_domain':
  "\<lbrace>ct_idle_or_in_cur_domain' and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and ct_active' and K (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n) \<rbrace>
    createNewCaps ty ptr n us dev
   \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace>" apply (wp ct_idle_or_in_cur_domain'_lift_futz createNewCaps_obj_at'[where sz=sz] | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain' and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and ct_active' and K (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createNewCaps_sch_act_wf:
  "\<lbrace>(\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace>
     createNewCaps ty ptr n us dev
   \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (wp sch_act_wf_lift_asm_futz
            createNewCaps_pred_tcb_at'[where sz=sz]
            createNewCaps_obj_at'[where sz=sz]
       | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and K (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace> createNewCaps ty ptr n us dev \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects'_ksDomSchedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> createObjects' ptr numObjects val gSize \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>" apply (simp add: createObjects'_def unless_def alignError_def) apply (wp | wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> createObjects' ptr numObjects val gSize \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> do y <- when (ptr && mask (objBitsKO val + gSize) \<noteq> 0) fail;
ps <- gets ksPSpace;
case lookupAround2 (ptr + word_of_nat (shiftL numObjects (objBitsKO val + gSize) - Suc 0)) ps of (before, uu_) \<Rightarrow> do y <- case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat numObjects << gSize) - 1]) ps))
od
od \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksDomSchedule s) \<Longrightarrow> (if ptr && mask (objBitsKO val + gSize) \<noteq> 0 then \<lambda>_. True else (\<lambda>s. \<forall>x xa. lookupAround2 (ptr + word_of_nat (shiftL numObjects (objBitsKO val + gSize) - Suc 0)) (ksPSpace s) = (x, xa) \<longrightarrow> (x = None \<longrightarrow> P (ksDomSchedule (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat numObjects << gSize) - 1]) (ksPSpace s)\<rparr>))) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> x < ptr \<longrightarrow> P (ksDomSchedule (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat numObjects << gSize) - 1]) (ksPSpace s)\<rparr>)))))) s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects'_ksDomScheduleIdx[wp]:
  "\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> createObjects' ptr numObjects val gSize \<lbrace>\<lambda>_ s. P (ksDomScheduleIdx s)\<rbrace>" apply (simp add: createObjects'_def unless_def alignError_def) apply (wp | wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> createObjects' ptr numObjects val gSize \<lbrace>\<lambda>_ s. P (ksDomScheduleIdx s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> do y <- when (ptr && mask (objBitsKO val + gSize) \<noteq> 0) fail;
ps <- gets ksPSpace;
case lookupAround2 (ptr + word_of_nat (shiftL numObjects (objBitsKO val + gSize) - Suc 0)) ps of (before, uu_) \<Rightarrow> do y <- case before of None \<Rightarrow> return () | Some (x, xa) \<Rightarrow> assert (x < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat numObjects << gSize) - 1]) ps))
od
od \<lbrace>\<lambda>_ s. P (ksDomScheduleIdx s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksDomScheduleIdx s) \<Longrightarrow> (if ptr && mask (objBitsKO val + gSize) \<noteq> 0 then \<lambda>_. True else (\<lambda>s. \<forall>x xa. lookupAround2 (ptr + word_of_nat (shiftL numObjects (objBitsKO val + gSize) - Suc 0)) (ksPSpace s) = (x, xa) \<longrightarrow> (x = None \<longrightarrow> P (ksDomScheduleIdx (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat numObjects << gSize) - 1]) (ksPSpace s)\<rparr>))) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (\<forall>x xb. xa = (x, xb) \<longrightarrow> x < ptr \<longrightarrow> P (ksDomScheduleIdx (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> val)) (map (\<lambda>n. ptr + (n << objBitsKO val)) [0 .e. (word_of_nat numObjects << gSize) - 1]) (ksPSpace s)\<rparr>)))))) s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma untyped_ranges_zero_inv_null_filter_cteCaps_of:
  "untyped_ranges_zero_inv (cteCaps_of s)
    = untyped_ranges_zero_inv (option_map cteCap o null_filter' (ctes_of s))" by (simp add: untyped_ranges_zero_inv_null_filter cteCaps_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_ranges_zero_inv (cteCaps_of s) = untyped_ranges_zero_inv (map_option cteCap \<circ> null_filter' (ctes_of s))
theory Retype_R

lemma createObjects_pred_tcb_at':
  "\<lbrace>pred_tcb_at' proj P t and K (range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0)
     and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace>
  createObjects ptr n val gbits \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>" apply (simp add: pred_tcb_at'_def createObjects_def) apply (wp createObjects_orig_obj_at') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t and K (range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t and (\<lambda>y. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t and (\<lambda>y. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz) s \<Longrightarrow> n \<noteq> 0 \<and> range_cover ptr ?sz3 (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s \<and> pspace_no_overlap' ptr ?sz3 s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_orig_obj_at3:
  "\<lbrace>\<lambda>s. obj_at' P p s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and>
        pspace_aligned' s \<and>
        pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace>
  createObjects ptr n val gbits \<lbrace>\<lambda>r. obj_at' P p\<rbrace>" by (wp createObjects_orig_obj_at'[where sz = sz] | simp add: createObjects_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' P p s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>r. obj_at' P p\<rbrace>
theory Retype_R

lemma createObjects_irq_state:
  "\<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and>
        pspace_no_overlap' ptr sz s \<and>
        range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and>
        valid_irq_node' (irq_node' s) s\<rbrace>
      createObjects ptr n val gbits
   \<lbrace>\<lambda>rv s. valid_irq_node' (irq_node' s) s\<rbrace>" apply (wp valid_irq_node_lift_asm [unfolded pred_conj_def, OF _ createObjects_orig_obj_at3]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> valid_irq_node' (irq_node' s) s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. valid_irq_node' (irq_node' s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> valid_irq_node' (irq_node' s) s \<Longrightarrow> valid_irq_node' (irq_node' s) s \<and> range_cover ptr ?sz10 (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz10 s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_cur':
  "\<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and>
        pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and>
        cur_tcb' s\<rbrace>
      createObjects ptr n val gbits
   \<lbrace>\<lambda>rv s. cur_tcb' s\<rbrace>" apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<exists>t. ksCurThread s = t \<and> tcb_at' t s"]) apply (simp add: cur_tcb'_def) apply (wp hoare_vcg_ex_lift createObjects_orig_obj_at3) apply (clarsimp simp: cur_tcb'_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> cur_tcb' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<exists>t. ksCurThread s = t \<and> tcb_at' t s \<Longrightarrow> cur_tcb' s
 2. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> cur_tcb' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. \<exists>t. ksCurThread s = t \<and> tcb_at' t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> cur_tcb' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. \<exists>t. ksCurThread s = t \<and> tcb_at' t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> cur_tcb' s \<Longrightarrow> \<exists>x. ksCurThread s = x \<and> tcb_at' x s \<and> range_cover ptr (?sz7 x) (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz7 x) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; tcb_at' (ksCurThread s) s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz7 (ksCurThread s)) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz7 (ksCurThread s)) s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_vms'[wp]:
  "\<lbrace>(\<lambda>_.  (range_cover ptr sz  (objBitsKO val + gbits) n \<and> 0 < n)) and pspace_aligned' and
     pspace_distinct' and pspace_no_overlap' ptr sz and valid_machine_state'\<rbrace>
      createObjects ptr n val gbits
   \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace>" apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def
                   typ_at'_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift createObjects_orig_ko_wp_at2'
         | simp add: createObjects_def)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>_. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and valid_machine_state'\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>_. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz and (\<lambda>s. \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0)\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. \<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>p. ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataT) (p && ~~ mask pageBits) s \<or> ko_wp_at' (\<lambda>ko. koTypeOf ko = UserDataDeviceT) (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0) \<Longrightarrow> \<forall>x. range_cover ptr (?sz6 x) (objBitsKO val + gbits) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataT) (x && ~~ mask pageBits) s \<and> pspace_no_overlap' ptr (?sz6 x) s \<or> range_cover ptr (?sz14 x) (objBitsKO val + gbits) n \<and> ko_wp_at' (\<lambda>a. koTypeOf a = UserDataDeviceT) (x && ~~ mask pageBits) s \<and> pspace_no_overlap' ptr (?sz14 x) s \<or> underlying_memory (ksMachineState s) x = 0 proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_ct_idle_or_in_cur_domain':
  "\<lbrace>ct_active' and valid_pspace' and pspace_no_overlap' ptr sz
       and ct_idle_or_in_cur_domain'
       and K (range_cover ptr sz (objBitsKO val + gSize) n \<and> n \<noteq> 0)\<rbrace>
     createObjects ptr n val gSize
   \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" apply (rule hoare_gen_asm) apply (wp ct_idle_or_in_cur_domain'_lift_futz createObjects_obj_at_other[where sz=sz]) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and ct_idle_or_in_cur_domain' and K (range_cover ptr sz (objBitsKO val + gSize) n \<and> n \<noteq> 0)\<rbrace> createObjects ptr n val gSize \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val + gSize) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and ct_idle_or_in_cur_domain'\<rbrace> createObjects ptr n val gSize \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>d t. range_cover ptr sz (objBitsKO val + gSize) n \<and> n \<noteq> 0 \<Longrightarrow> range_cover ptr sz (objBitsKO val + gSize) n
 2. \<And>d t. range_cover ptr sz (objBitsKO val + gSize) n \<and> n \<noteq> 0 \<Longrightarrow> n \<noteq> 0
 3. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gSize) n \<and> n \<noteq> 0; (ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and ct_idle_or_in_cur_domain') s\<rbrakk> \<Longrightarrow> (ct_idle_or_in_cur_domain' and ct_active' and (\<lambda>s. valid_pspace' s \<and> pspace_no_overlap' ptr sz s)) s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma untyped_zero_ranges_cte_def:
  "untyped_ranges_zero_inv (cteCaps_of s) rs
    = (\<forall>r. (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some r) p s)
        = (r \<in> rs))" apply (clarsimp simp: untyped_ranges_zero_inv_def cte_wp_at_ctes_of
                        cteCaps_of_def set_eq_iff ran_def map_comp_Some_iff) apply (safe, metis+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_ranges_zero_inv (cteCaps_of s) rs = (\<forall>r. (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some r) p s) = (r \<in> rs)) proof (prove)
goal (1 subgoal):
 1. (\<forall>a b. ((a, b) \<in> rs) = (\<exists>aa k'. (\<exists>z. ctes_of s aa = Some z \<and> cteCap z = k') \<and> untypedZeroRange k' = Some (a, b))) = (\<forall>a b. (\<exists>p cte. ctes_of s p = Some cte \<and> untypedZeroRange (cteCap cte) = Some (a, b)) = ((a, b) \<in> rs)) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma corres_retype_update_gsI:
  assumes not_zero: "n \<noteq> 0"
  and      aligned: "is_aligned ptr (objBitsKO ko + gbits)"
  and obj_bits_api: "obj_bits_api (APIType_map2 ty) us =
                     objBitsKO ko + gbits"
  and        check: "sz < obj_bits_api (APIType_map2 ty) us \<longleftrightarrow>
                     sz < objBitsKO ko + gbits"
  and          usv: "APIType_map2 ty = Structures_A.CapTableObject \<Longrightarrow> 0 < us"
  and           ko: "makeObjectKO dev ty = Some ko"
  and          orr: "obj_bits_api (APIType_map2 ty) us \<le> sz \<Longrightarrow>
                     obj_relation_retype
                       (default_object (APIType_map2 ty) dev us) ko"
  and        cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n"
  and            f: "f = update_gs (APIType_map2 ty) us"
  shows "corres (\<lambda>rv rv'. rv' = g rv)
         (\<lambda>s. valid_pspace s \<and> pspace_no_overlap_range_cover ptr sz s
            \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s)
         (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and>
              pspace_no_overlap' ptr sz s)
         (retype_region2 ptr n us (APIType_map2 ty) dev)
         (do addrs \<leftarrow> createObjects ptr n ko gbits;
             _ \<leftarrow> modify (f (set addrs));
             return (g addrs)
          od)" using corres_retype' [OF not_zero aligned obj_bits_api check usv ko orr cover] by (simp add: f)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (f (set addrs));
return (g addrs)
od) proof (prove)
using this:
\<lbrakk>APIType_map2 ty = Structures_A.apiobject_type.CapTableObject \<Longrightarrow> APIType_map2 ty = Structures_A.apiobject_type.CapTableObject; obj_bits_api (APIType_map2 ty) us \<le> sz \<Longrightarrow> obj_bits_api (APIType_map2 ty) us \<le> sz\<rbrakk> \<Longrightarrow> corres (\<lambda>rv rv'. rv' = ?g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (update_gs (APIType_map2 ty) us (set addrs));
return (?g addrs)
od)

goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv' = g rv) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) (retype_region2 ptr n us (APIType_map2 ty) dev) (do addrs <- createObjects ptr n ko gbits;
_ <- modify (f (set addrs));
return (g addrs)
od)
theory Retype_R

lemma gcd_corres: "corres (=) \<top> \<top> (gets cur_domain) curDomain" by (simp add: curDomain_def state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets cur_domain) curDomain
theory Retype_R

lemma retype_region2_extra_ext_trivial:
  "ty \<noteq> APIType_map2 (Inr (APIObjectType apiobject_type.TCBObject))
      \<Longrightarrow> retype_region2_extra_ext ptrs ty = return ()" by (simp add: retype_region2_extra_ext_def when_def APIType_map2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ty \<noteq> APIType_map2 (Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject)) \<Longrightarrow> retype_region2_extra_ext ptrs ty = return ()
theory Retype_R

lemma retype_region2_ext_retype_region_ArchObject_PageDirectoryObj:
  "retype_region ptr n us (APIType_map2 (Inr PageDirectoryObject)) dev =
  (retype_region2 ptr n us (APIType_map2 (Inr PageDirectoryObject)) dev :: obj_ref list det_ext_monad)" by (simp add: retype_region2_ext_retype_region retype_region2_extra_ext_def when_def APIType_map2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retype_region ptr n us (APIType_map2 (Inr PageDirectoryObject)) dev = retype_region2 ptr n us (APIType_map2 (Inr PageDirectoryObject)) dev