theory Detype_R

lemma deleteObjects_def3:
  "deleteObjects ptr bits =
   do
     assert (is_aligned ptr bits);
     stateAssert (deletionIsSafe ptr bits) [];
     doMachineOp (freeMemory ptr bits);
     stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr .. ptr + 2 ^ bits - 1})) [];
     modify (\<lambda>s. s \<lparr> ksPSpace := \<lambda>x. if x \<in> {ptr .. ptr + 2 ^ bits - 1}
                                              then None else ksPSpace s x,
                     gsUserPages := \<lambda>x. if x \<in> {ptr .. ptr + 2 ^ bits - 1}
                                           then None else gsUserPages s x,
                     gsCNodes := \<lambda>x. if x \<in> {ptr .. ptr + 2 ^ bits - 1}
                                        then None else gsCNodes s x \<rparr>);
     stateAssert ksASIDMapSafe []
   od" apply (cases "is_aligned ptr bits") apply (simp add: deleteObjects_def2) apply (simp add: deleteObjects_def is_aligned_mask
                   unless_def alignError_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. deleteObjects ptr bits = do assert (is_aligned ptr bits);
stateAssert (deletionIsSafe ptr bits) [];
doMachineOp (freeMemory ptr bits);
stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr..ptr + 2 ^ bits - 1})) [];
modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else ksPSpace s x, gsUserPages := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsUserPages s x, gsCNodes := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od proof (prove)
goal (2 subgoals):
 1. is_aligned ptr bits \<Longrightarrow> deleteObjects ptr bits = do assert (is_aligned ptr bits);
stateAssert (deletionIsSafe ptr bits) [];
doMachineOp (freeMemory ptr bits);
stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr..ptr + 2 ^ bits - 1})) [];
modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else ksPSpace s x, gsUserPages := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsUserPages s x, gsCNodes := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od
 2. \<not> is_aligned ptr bits \<Longrightarrow> deleteObjects ptr bits = do assert (is_aligned ptr bits);
stateAssert (deletionIsSafe ptr bits) [];
doMachineOp (freeMemory ptr bits);
stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr..ptr + 2 ^ bits - 1})) [];
modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else ksPSpace s x, gsUserPages := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsUserPages s x, gsCNodes := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od proof (prove)
goal (1 subgoal):
 1. \<not> is_aligned ptr bits \<Longrightarrow> deleteObjects ptr bits = do assert (is_aligned ptr bits);
stateAssert (deletionIsSafe ptr bits) [];
doMachineOp (freeMemory ptr bits);
stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr..ptr + 2 ^ bits - 1})) [];
modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else ksPSpace s x, gsUserPages := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsUserPages s x, gsCNodes := \<lambda>x. if x \<in> {ptr..ptr + 2 ^ bits - 1} then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od proof (prove)
goal:
No subgoals!