kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_R

lemma retype_region2_valid_etcbs[wp]:"\<lbrace>valid_etcbs\<rbrace> retype_region2 a b c d dev \<lbrace>\<lambda>_. valid_etcbs\<rbrace>" apply (simp add: retype_region2_def) apply (simp add: retype_region2_ext_def bind_assoc) apply wp apply (clarsimp simp del: fun_upd_apply) apply (blast intro: valid_etcb_fold_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> retype_region2 a b c d dev \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> do y <- when (d \<noteq> Structures_A.apiobject_type.Untyped) (do kh <- gets kheap;
y <- retype_region2_ext (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) d;
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) kh))
od);
return (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b])
od \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> do y <- when (d \<noteq> Structures_A.apiobject_type.Untyped) (do kh <- gets kheap;
y <- modify (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext d default_domain)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b])));
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) kh))
od);
return (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b])
od \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_etcbs s \<Longrightarrow> (if d \<noteq> Structures_A.apiobject_type.Untyped then \<lambda>s. valid_etcbs (ekheap_update (foldr (\<lambda>p ekh. ekh(p := default_ext d default_domain)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b])) s\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (kheap s)\<rparr>) else valid_etcbs) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_etcbs s; d \<noteq> Structures_A.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> valid_etcbs_2 (foldr (\<lambda>p ekh. ekh(p := default_ext d default_domain)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (ekheap s)) (foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (kheap s)) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma retype_region2_obj_at:
  assumes tytcb: "ty = Structures_A.apiobject_type.TCBObject"
  shows "\<lbrace>\<top>\<rbrace> retype_region2 ptr n us ty dev \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. tcb_at x s\<rbrace>" using tytcb unfolding retype_region2_def apply (simp only: return_bind bind_return foldr_upd_app_if fun_app_def K_bind_def) apply (wp dxo_wp_weak | simp)+ apply (auto simp: obj_at_def default_object_def is_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> retype_region2 ptr n us ty dev \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. tcb_at x s\<rbrace> proof (prove)
using this:
ty = Structures_A.apiobject_type.TCBObject

goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> retype_region2 ptr n us ty dev \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. tcb_at x s\<rbrace> proof (prove)
using this:
ty = Structures_A.apiobject_type.TCBObject

goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do obj_size <- return $ 2 ^ obj_bits_api ty us;
ptrs <- return $ map (\<lambda>p. ptr_add ptr (p * obj_size)) [0..<n];
when (ty \<noteq> Structures_A.apiobject_type.Untyped) (do kh <- gets kheap;
kh' <- return $ foldr (\<lambda>p kh. kh(p \<mapsto> default_object ty dev us)) ptrs kh;
do_extended_op (retype_region2_ext ptrs ty);
modify $ kheap_update (K kh')
od);
return $ ptrs
od \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. tcb_at x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do y <- when (Structures_A.apiobject_type.TCBObject \<noteq> Structures_A.apiobject_type.Untyped) (do kh <- gets kheap;
y <- do_extended_op (retype_region2_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.TCBObject us)) [0..<n]) Structures_A.apiobject_type.TCBObject);
modify (kheap_update (K (\<lambda>x. if x \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.TCBObject us)) [0..<n]) then Some (default_object Structures_A.apiobject_type.TCBObject dev us) else kh x)))
od);
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.TCBObject us)) [0..<n])
od \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. tcb_at x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ty = Structures_A.apiobject_type.TCBObject \<Longrightarrow> \<forall>x\<in>{0..<n}. tcb_at (ptr_add ptr (x * 2 ^ obj_bits_api Structures_A.apiobject_type.TCBObject us)) (s\<lparr>kheap := \<lambda>x. if x \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api Structures_A.apiobject_type.TCBObject us)) ` {0..<n} then Some (default_object Structures_A.apiobject_type.TCBObject dev us) else kheap s x\<rparr>) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma createObjects_tcb_at':
  "\<lbrakk>range_cover ptr sz (objBitsKO (injectKOS (makeObject::tcb))) n; n \<noteq> 0\<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace>
   createObjects ptr n (KOTCB makeObject) 0 \<lbrace>\<lambda>ptrs s. \<forall>addr\<in>set ptrs. tcb_at' addr s\<rbrace>" apply (rule hoare_strengthen_post[OF createObjects_ko_at_strg[where val = "(makeObject :: tcb)"]]) apply (auto simp: obj_at'_def projectKOs project_inject objBitsKO_def objBits_def makeObject_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (objBitsKO (injectKOS makeObject)) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> createObjects ptr n (KOTCB makeObject) 0 \<lbrace>\<lambda>ptrs s. \<forall>addr\<in>set ptrs. tcb_at' addr s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrakk>range_cover ptr sz (objBitsKO (injectKOS makeObject)) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> range_cover ptr sz (objBitsKO (KOTCB makeObject) + 0) n
 2. \<lbrakk>range_cover ptr sz (objBitsKO (injectKOS makeObject)) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<lbrakk>range_cover ptr sz (objBitsKO (injectKOS makeObject)) n; n \<noteq> 0\<rbrakk> \<Longrightarrow> projectKO_opt (KOTCB makeObject) = Some makeObject
 4. \<And>rv s. \<lbrakk>range_cover ptr sz (objBitsKO (injectKOS makeObject)) n; n \<noteq> 0; \<forall>x\<in>set rv. \<forall>offs<2 ^ 0. ko_at' makeObject (x + (offs << objBitsKO (KOTCB makeObject))) s\<rbrakk> \<Longrightarrow> \<forall>addr\<in>set rv. tcb_at' addr s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma init_arch_objects_APIType_map2_noop:
  "tp \<noteq> Inr PageDirectoryObject
   \<longrightarrow> init_arch_objects (APIType_map2 tp) ptr n m addrs
    = return ()" apply (simp add: init_arch_objects_def APIType_map2_def) apply (cases tp, simp_all split: kernel_object.split arch_kernel_object.split
    object_type.split apiobject_type.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tp \<noteq> Inr PageDirectoryObject \<longrightarrow> init_arch_objects (APIType_map2 tp) ptr n m addrs = return () proof (prove)
goal (1 subgoal):
 1. (case tp of Inl (KOArch (KOASIDPool x)) \<Rightarrow> ArchObject ASIDPoolObj | Inl (KOArch _) \<Rightarrow> ArchObject SmallPageObj | Inl _ \<Rightarrow> ArchObject SmallPageObj | Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped) \<Rightarrow> Structures_A.apiobject_type.Untyped | Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<Rightarrow> Structures_A.apiobject_type.TCBObject | Inr (APIObjectType ArchTypes_H.apiobject_type.EndpointObject) \<Rightarrow> Structures_A.apiobject_type.EndpointObject | Inr (APIObjectType ArchTypes_H.apiobject_type.NotificationObject) \<Rightarrow> Structures_A.apiobject_type.NotificationObject | Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<Rightarrow> Structures_A.apiobject_type.CapTableObject | Inr SmallPageObject \<Rightarrow> ArchObject SmallPageObj | Inr LargePageObject \<Rightarrow> ArchObject LargePageObj | Inr SectionObject \<Rightarrow> ArchObject SectionObj | Inr SuperSectionObject \<Rightarrow> ArchObject SuperSectionObj | Inr PageTableObject \<Rightarrow> ArchObject PageTableObj | Inr PageDirectoryObject \<Rightarrow> ArchObject PageDirectoryObj) = ArchObject PageDirectoryObj \<longrightarrow> tp \<noteq> Inr PageDirectoryObject \<longrightarrow> do y <- mapM_x copy_global_mappings addrs;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) addrs)
od = return () proof (prove)
goal:
No subgoals!
theory Retype_R

lemma data_page_relation_retype:
  "obj_relation_retype (ArchObj (DataPage False pgsz)) KOUserData"
  "obj_relation_retype (ArchObj (DataPage True pgsz)) KOUserDataDevice" apply (simp_all add: obj_relation_retype_def
                   objBits_simps archObjSize_def
                   pbfs_atleast_pageBits) apply (clarsimp simp: image_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_relation_retype (ArchObj (DataPage False pgsz)) KOUserData &&& obj_relation_retype (ArchObj (DataPage True pgsz)) KOUserDataDevice proof (prove)
goal (2 subgoals):
 1. \<forall>p. fst ` {(p + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserData) |n. n < 2 ^ (pageBitsForSize pgsz - pageBits)} = {p + x * 2 ^ pageBits |x. x < 2 ^ (pageBitsForSize pgsz - pageBits)} \<and> (\<forall>a b. (\<exists>n. a = p + n * 2 ^ pageBits \<and> b = (\<lambda>_ obj. obj = KOUserData) \<and> n < 2 ^ (pageBitsForSize pgsz - pageBits)) \<longrightarrow> b (ArchObj (DataPage False pgsz)) KOUserData)
 2. \<forall>p. fst ` {(p + n * 2 ^ pageBits, \<lambda>_ obj. obj = KOUserDataDevice) |n. n < 2 ^ (pageBitsForSize pgsz - pageBits)} = {p + x * 2 ^ pageBits |x. x < 2 ^ (pageBitsForSize pgsz - pageBits)} \<and> (\<forall>a b. (\<exists>n. a = p + n * 2 ^ pageBits \<and> b = (\<lambda>_ obj. obj = KOUserDataDevice) \<and> n < 2 ^ (pageBitsForSize pgsz - pageBits)) \<longrightarrow> b (ArchObj (DataPage True pgsz)) KOUserDataDevice) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma case_Null_If:
  "(case c of NullCap \<Rightarrow> a | _ \<Rightarrow> b) = (if c = NullCap then a else b)" by (case_tac c, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case c of capability.NullCap \<Rightarrow> a | _ \<Rightarrow> b) = (if c = capability.NullCap then a else b)
theory Finalise_R

lemma updateCap_cte_wp_at_cases:
  "\<lbrace>\<lambda>s. (ptr = ptr' \<longrightarrow> cte_wp_at' (P \<circ> cteCap_update (K cap)) ptr' s) \<and> (ptr \<noteq> ptr' \<longrightarrow> cte_wp_at' P ptr' s)\<rbrace>
     updateCap ptr cap
   \<lbrace>\<lambda>rv. cte_wp_at' P ptr'\<rbrace>" apply (clarsimp simp: valid_def) apply (drule updateCap_stuff) apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (ptr = ptr' \<longrightarrow> cte_wp_at' (P \<circ> cteCap_update (K cap)) ptr' s) \<and> (ptr \<noteq> ptr' \<longrightarrow> cte_wp_at' P ptr' s)\<rbrace> updateCap ptr cap \<lbrace>\<lambda>rv. cte_wp_at' P ptr'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>((), b) \<in> fst (updateCap ptr cap s); ptr = ptr' \<longrightarrow> cte_wp_at' (P \<circ> cteCap_update (\<lambda>y. cap)) ptr' s; ptr \<noteq> ptr' \<longrightarrow> cte_wp_at' P ptr' s\<rbrakk> \<Longrightarrow> cte_wp_at' P ptr' b proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>ptr = ptr' \<longrightarrow> cte_wp_at' (P \<circ> cteCap_update (\<lambda>y. cap)) ptr' s; ptr \<noteq> ptr' \<longrightarrow> cte_wp_at' P ptr' s; ctes_of b = modify_map (ctes_of s) ptr (cteCap_update (K cap)) \<and> gsUserPages b = gsUserPages s \<and> gsCNodes b = gsCNodes s \<and> ksMachineState b = ksMachineState s \<and> ksWorkUnitsCompleted b = ksWorkUnitsCompleted s \<and> ksCurThread b = ksCurThread s \<and> ksIdleThread b = ksIdleThread s \<and> ksReadyQueues b = ksReadyQueues s \<and> ksSchedulerAction b = ksSchedulerAction s \<and> ksArchState b = ksArchState s \<and> (pspace_aligned' s \<longrightarrow> pspace_aligned' b) \<and> (pspace_distinct' s \<longrightarrow> pspace_distinct' b)\<rbrakk> \<Longrightarrow> cte_wp_at' P ptr' b proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma emptySlot_cte_wp_cap_other:
  "\<lbrace>(\<lambda>s. cte_wp_at' (\<lambda>c. P (cteCap c)) p s) and K (p \<noteq> p')\<rbrace>
  emptySlot p' opt
  \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: emptySlot_def clearUntypedFreeIndex_def getSlotCap_def) apply (rule hoare_pre) apply (wp updateMDB_weak_cte_wp_at updateCap_cte_wp_at_cases
             updateFreeIndex_cte_wp_at getCTE_wp' hoare_vcg_all_lift
              | simp add:  | wpc
              | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. P (cteCap c)) p and K (p \<noteq> p')\<rbrace> emptySlot p' opt \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> emptySlot p' opt \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> do y <- do cte <- getCTE p';
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex p' (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()
od;
newCTE <- getCTE p';
case cteCap newCTE of capability.NullCap \<Rightarrow> return () | _ \<Rightarrow> do updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
updateCap p' capability.NullCap;
updateMDB p' (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>?Q2\<rbrace> do y <- do cte <- getCTE p';
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex p' (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()
od;
newCTE <- getCTE p';
case cteCap newCTE of capability.NullCap \<Rightarrow> return () | _ \<Rightarrow> do updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
updateCap p' capability.NullCap;
updateMDB p' (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
 2. \<And>s. \<lbrakk>p \<noteq> p'; cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma emptySlot_queues [wp]:
  "\<lbrace>Invariants_H.valid_queues\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" unfolding emptySlot_def by (wp | wpcw | wp valid_queues_lift | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> do clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
mdbNode <- return (cteMDBNode newCTE);
prev <- return (mdbPrev mdbNode);
next <- return (mdbNext mdbNode);
case cteCap newCTE of capability.NullCap \<Rightarrow> return () | _ \<Rightarrow> do updateMDB prev (mdbNext_update (\<lambda>_. next));
updateMDB next (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged mdbNode) (mdbPrev_update (\<lambda>_. prev) mdb));
updateCap sl capability.NullCap;
updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>
theory Finalise_R

lemma emptySlot_sch_act_wf [wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
  emptySlot sl opt
  \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: emptySlot_def case_Null_If) apply (wp sch_act_wf_lift tcb_in_cur_domain'_lift | wpcw | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> do y <- clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma updateCap_valid_objs' [wp]:
  "\<lbrace>valid_objs' and valid_cap' cap\<rbrace>
  updateCap ptr cap \<lbrace>\<lambda>r. valid_objs'\<rbrace>" unfolding updateCap_def by (wp setCTE_valid_objs getCTE_wp) (clarsimp dest!: cte_at_cte_wp_atD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> updateCap ptr cap \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_cap' cap\<rbrace> do cte <- getCTE ptr;
setCTE ptr (cteCap_update (\<lambda>_. cap) cte)
od \<lbrace>\<lambda>r. valid_objs'\<rbrace>
theory Finalise_R

lemma updateFreeIndex_valid_objs' [wp]:
  "\<lbrace>valid_objs'\<rbrace> clearUntypedFreeIndex ptr \<lbrace>\<lambda>r. valid_objs'\<rbrace>" apply (simp add: clearUntypedFreeIndex_def getSlotCap_def) apply (wp getCTE_wp' | wpc | simp add: updateTrackedFreeIndex_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> clearUntypedFreeIndex ptr \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do cte <- getCTE ptr;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex ptr (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma nullPointer_eq_0_simp[simp]:
  "(nullPointer = 0) = True"
  "(0 = nullPointer) = True" by (simp add: nullPointer_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (nullPointer = 0) = True &&& (0 = nullPointer) = True
theory Finalise_R

lemma no_0_no_0_lhs_trancl [simp]:
  "no_0 m \<Longrightarrow> \<not> m \<turnstile> 0 \<leadsto>\<^sup>+ x" by (rule, drule tranclD, clarsimp simp: next_unfold')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 m \<Longrightarrow> (0, x) \<notin> (mdb_next_rel m)\<^sup>+
theory Finalise_R

lemma no_0_no_0_lhs_rtrancl [simp]:
  "\<lbrakk> no_0 m; x \<noteq> 0 \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> 0 \<leadsto>\<^sup>* x" by (clarsimp dest!: rtranclD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 m; x \<noteq> 0\<rbrakk> \<Longrightarrow> (0, x) \<notin> (mdb_next_rel m)\<^sup>*
theory Finalise_R

lemma n_revokable:
  "n p = Some (CTE cap node) \<Longrightarrow>
  (\<exists>cap' node'. m p = Some (CTE cap' node') \<and>
              (if p = slot
               then \<not> mdbRevocable node
               else mdbRevocable node = mdbRevocable node'))" by (auto simp add: n_def modify_map_if nullMDBNode_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable node else mdbRevocable node = mdbRevocable node')
theory Finalise_R

lemma no_0_n:
  "no_0 n" using no_0 by (simp add: n_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 n proof (prove)
using this:
no_0 m

goal (1 subgoal):
 1. no_0 n
theory Finalise_R

lemma n_cap:
  "n p = Some (CTE cap node) \<Longrightarrow>
  \<exists>cap' node'. m p = Some (CTE cap' node') \<and>
              (if p = slot
               then cap = NullCap
               else cap' = cap)" apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm) apply (cases node) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then cap = capability.NullCap else cap' = cap) proof (prove)
goal (2 subgoals):
 1. \<And>nodea capa. \<lbrakk>slot = p; mdbPrev s_node \<noteq> p; cap = capability.NullCap; node = nullMDBNode; mdbNext s_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE capa node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = nodea); mdbNext s_node = p \<or> m p = Some (CTE capa nodea)\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node')
 2. \<And>nodea. \<lbrakk>p = mdbNext s_node; mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0; mdbPrev s_node = 0 \<and> mdbNext s_node = 0 \<or> m (mdbNext s_node) = Some (CTE cap nodea) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged nodea \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) nodea) = node\<rbrakk> \<Longrightarrow> \<exists>node'. m (mdbNext s_node) = Some (CTE cap node') proof (prove)
goal (2 subgoals):
 1. \<And>nodea capa x1 x2 x3 x4. \<lbrakk>slot = p; mdbPrev s_node \<noteq> p; cap = capability.NullCap; node = nullMDBNode; mdbNext s_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE capa node) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged node \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) node) = nodea); mdbNext s_node = p \<or> m p = Some (CTE capa nodea); node = MDB x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node')
 2. \<And>nodea. \<lbrakk>p = mdbNext s_node; mdbPrev s_node = 0 \<longrightarrow> mdbNext s_node \<noteq> 0; mdbPrev s_node = 0 \<and> mdbNext s_node = 0 \<or> m (mdbNext s_node) = Some (CTE cap nodea) \<and> mdbFirstBadged_update (\<lambda>_. mdbFirstBadged nodea \<or> mdbFirstBadged s_node) (mdbPrev_update (\<lambda>_. mdbPrev s_node) nodea) = node\<rbrakk> \<Longrightarrow> \<exists>node'. m (mdbNext s_node) = Some (CTE cap node') proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma chunked:
  "mdb_chunked m" using valid by (simp add: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. mdb_chunked m
theory Finalise_R

lemma valid_badges:
  "valid_badges m" using valid ..

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_badges m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_badges m