theory Detype_R

lemma deleteObject_no_overlap[wp]:
  "\<lbrace>valid_cap' (UntypedCap d ptr bits idx) and valid_pspace'\<rbrace>
     deleteObjects ptr bits
   \<lbrace>\<lambda>rv s. pspace_no_overlap' ptr bits s\<rbrace>" apply (simp add: deleteObjects_def3 doMachineOp_def split_def) apply wp apply (clarsimp simp: valid_cap'_def cong:if_cong) apply (drule (2) valid_untyped_no_overlap) apply (subgoal_tac
     "s\<lparr>ksMachineState := b,
        ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None
                        else ksPSpace s x\<rparr> =
      ksMachineState_update (\<lambda>_. b)
      (s\<lparr>ksPSpace := ksPSpace s |` (- {ptr..ptr + 2 ^ bits - 1})\<rparr>)", simp) apply (case_tac s, simp) apply (rule ext) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' (capability.UntypedCap d ptr bits idx) and valid_pspace'\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. pspace_no_overlap' ptr bits\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' (capability.UntypedCap d ptr bits idx) and valid_pspace'\<rbrace> do y <- assert (is_aligned ptr bits);
y <- stateAssert (deletionIsSafe ptr bits) [];
y <- do ms <- gets ksMachineState;
p <- select_f (freeMemory ptr bits ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od;
y <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1)) [];
y <- modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>rv. pspace_no_overlap' ptr bits\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_cap' (capability.UntypedCap d ptr bits idx) and valid_pspace') s \<Longrightarrow> is_aligned ptr bits \<longrightarrow> deletionIsSafe ptr bits s \<longrightarrow> (\<forall>x\<in>fst (freeMemory ptr bits (ksMachineState s)). \<not> cNodePartialOverlap (gsCNodes (s\<lparr>ksMachineState := snd x\<rparr>)) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1) \<longrightarrow> ksASIDMapSafe (s\<lparr>ksMachineState := snd x, ksPSpace := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsUserPages := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsCNodes := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd x\<rparr>) xa\<rparr>) \<longrightarrow> pspace_no_overlap' ptr bits (s\<lparr>ksMachineState := snd x, ksPSpace := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsUserPages := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsCNodes := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd x\<rparr>) xa\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>capAligned (capability.UntypedCap d ptr bits idx); valid_untyped' d ptr bits idx s; ptr \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; idx \<le> 2 ^ bits; is_aligned (word_of_nat idx) minUntypedSizeBits; valid_pspace' s; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>)\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr bits (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>capAligned (capability.UntypedCap d ptr bits idx); ptr \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; idx \<le> 2 ^ bits; is_aligned (word_of_nat idx) minUntypedSizeBits; valid_pspace' s; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>); pspace_no_overlap' ptr bits (s\<lparr>ksPSpace := ksPSpace s |` (- {ptr..ptr + 2 ^ bits - 1})\<rparr>)\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr bits (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>capAligned (capability.UntypedCap d ptr bits idx); ptr \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; idx \<le> 2 ^ bits; is_aligned (word_of_nat idx) minUntypedSizeBits; valid_pspace' s; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>); pspace_no_overlap' ptr bits (s\<lparr>ksPSpace := ksPSpace s |` (- {ptr..ptr + 2 ^ bits - 1})\<rparr>)\<rbrakk> \<Longrightarrow> s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr> = s\<lparr>ksPSpace := ksPSpace s |` (- {ptr..ptr + 2 ^ bits - 1}), ksMachineState := b\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s b ksPSpacea gsUserPagesa gsCNodesa gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. \<lbrakk>capAligned (capability.UntypedCap d ptr bits idx); ptr \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; idx \<le> 2 ^ bits; is_aligned (word_of_nat idx) minUntypedSizeBits; valid_pspace' \<lparr>ksPSpace = ksPSpacea, gsUserPages = gsUserPagesa, gsCNodes = gsCNodesa, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; is_aligned ptr bits; deletionIsSafe ptr bits \<lparr>ksPSpace = ksPSpacea, gsUserPages = gsUserPagesa, gsCNodes = gsCNodesa, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; \<not> cNodePartialOverlap gsCNodesa (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits ksMachineState); ksASIDMapSafe \<lparr>ksPSpace = \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages = \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes = \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = b\<rparr>; pspace_no_overlap' ptr bits \<lparr>ksPSpace = ksPSpacea |` (- {ptr..ptr + 2 ^ bits - 1}), gsUserPages = gsUserPagesa, gsCNodes = gsCNodesa, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; s = \<lparr>ksPSpace = ksPSpacea, gsUserPages = gsUserPagesa, gsCNodes = gsCNodesa, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> (\<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x) = ksPSpacea |` (- {ptr..ptr + 2 ^ bits - 1}) proof (prove)
goal (1 subgoal):
 1. \<And>s b ksPSpacea gsUserPagesa gsCNodesa gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState x. \<lbrakk>capAligned (capability.UntypedCap d ptr bits idx); ptr \<noteq> 0; minUntypedSizeBits \<le> bits; bits \<le> maxUntypedSizeBits; idx \<le> 2 ^ bits; is_aligned (word_of_nat idx) minUntypedSizeBits; valid_pspace' \<lparr>ksPSpace = ksPSpacea, gsUserPages = gsUserPagesa, gsCNodes = gsCNodesa, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; is_aligned ptr bits; deletionIsSafe ptr bits \<lparr>ksPSpace = ksPSpacea, gsUserPages = gsUserPagesa, gsCNodes = gsCNodesa, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; \<not> cNodePartialOverlap gsCNodesa (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits ksMachineState); ksASIDMapSafe \<lparr>ksPSpace = \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages = \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes = \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = b\<rparr>; pspace_no_overlap' ptr bits \<lparr>ksPSpace = ksPSpacea |` (- {ptr..ptr + 2 ^ bits - 1}), gsUserPages = gsUserPagesa, gsCNodes = gsCNodesa, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>; s = \<lparr>ksPSpace = ksPSpacea, gsUserPages = gsUserPagesa, gsCNodes = gsCNodesa, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr>\<rbrakk> \<Longrightarrow> (if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x) = (ksPSpacea |` (- {ptr..ptr + 2 ^ bits - 1})) x proof (prove)
goal:
No subgoals!