theory TcbAcc_R

lemma load_word_corres:
  "corres (=) \<top>
     (typ_at' UserDataT (a && ~~ mask pageBits) and (\<lambda>s. is_aligned a 2))
     (do_machine_op (loadWord a)) (loadWordUser a)" unfolding loadWordUser_def apply (rule corres_gen_asm2) apply (rule corres_stateAssert_assume [rotated]) apply (simp add: pointerInUserData_def) apply (rule corres_guard_imp) apply simp apply (rule corres_machine_op) apply (rule corres_Id [OF refl refl]) apply (rule no_fail_pre) apply wp apply assumption apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (typ_at' UserDataT (a && ~~ mask pageBits) and (\<lambda>s. is_aligned a 2)) (do_machine_op (loadWord a)) (loadWordUser a) proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (typ_at' UserDataT (a && ~~ mask pageBits) and (\<lambda>s. is_aligned a 2)) (do_machine_op (loadWord a)) (do stateAssert (pointerInUserData a) [];
doMachineOp $ loadWord a
od) proof (prove)
goal (1 subgoal):
 1. is_aligned a 2 \<Longrightarrow> corres (=) (\<lambda>_. True) (typ_at' UserDataT (a && ~~ mask pageBits)) (do_machine_op (loadWord a)) (do stateAssert (pointerInUserData a) [];
doMachineOp $ loadWord a
od) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned a 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> pointerInUserData a s
 2. is_aligned a 2 \<Longrightarrow> corres (=) (\<lambda>_. True) (typ_at' UserDataT (a && ~~ mask pageBits)) (do_machine_op (loadWord a)) (K_bind (doMachineOp $ loadWord a) ()) proof (prove)
goal (1 subgoal):
 1. is_aligned a 2 \<Longrightarrow> corres (=) (\<lambda>_. True) (typ_at' UserDataT (a && ~~ mask pageBits)) (do_machine_op (loadWord a)) (K_bind (doMachineOp $ loadWord a) ()) proof (prove)
goal (3 subgoals):
 1. is_aligned a 2 \<Longrightarrow> corres (=) ?Q5 ?Q'5 (do_machine_op (loadWord a)) (K_bind (doMachineOp $ loadWord a) ())
 2. \<And>s. \<lbrakk>is_aligned a 2; True\<rbrakk> \<Longrightarrow> ?Q5 s
 3. \<And>s. \<lbrakk>is_aligned a 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> ?Q'5 s proof (prove)
goal (3 subgoals):
 1. is_aligned a 2 \<Longrightarrow> corres (=) ?Q5 ?Q'5 (do_machine_op (loadWord a)) (doMachineOp (loadWord a))
 2. \<And>s. \<lbrakk>is_aligned a 2; True\<rbrakk> \<Longrightarrow> ?Q5 s
 3. \<And>s. \<lbrakk>is_aligned a 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> ?Q'5 s proof (prove)
goal (3 subgoals):
 1. is_aligned a 2 \<Longrightarrow> corres_underlying Id False True (=) (\<lambda>_. True) (\<lambda>_. True) (loadWord a) (loadWord a)
 2. \<And>s. \<lbrakk>is_aligned a 2; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>is_aligned a 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned a 2; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (loadWord a)
 2. \<And>s. \<lbrakk>is_aligned a 2; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>is_aligned a 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned a 2; True\<rbrakk> \<Longrightarrow> no_fail ?P17 (loadWord a)
 2. \<And>s. \<lbrakk>is_aligned a 2; True; True\<rbrakk> \<Longrightarrow> ?P17 s
 3. \<And>s. \<lbrakk>is_aligned a 2; True\<rbrakk> \<Longrightarrow> True
 4. \<And>s. \<lbrakk>is_aligned a 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>is_aligned a 2; True; True\<rbrakk> \<Longrightarrow> is_aligned a 2
 2. \<And>s. \<lbrakk>is_aligned a 2; True\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>is_aligned a 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_aligned a 2; True\<rbrakk> \<Longrightarrow> True
 2. \<And>s. \<lbrakk>is_aligned a 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> True proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned a 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!