kings-crown/FVELER_Isabelle huggingface dataset:
theory Intent_DR

lemma weak_det_spec_storeWord:
  "weak_det_spec P (storeWord a b)" apply (simp add:storeWord_def) apply (rule weak_det_spec_compose)+ apply (simp_all add:weak_det_spec_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (storeWord a b) proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (do y <- assert (a && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(a := word_rsplit b ! 3, a + 1 := word_rsplit b ! 2, a + 2 := word_rsplit b ! Suc 0, a + 3 := word_rsplit b ! 0)))
od) proof (prove)
goal (2 subgoals):
 1. \<And>Q r. weak_det_spec (Q r) (modify (underlying_memory_update (\<lambda>m. m(a := word_rsplit b ! 3, a + 1 := word_rsplit b ! 2, a + 2 := word_rsplit b ! Suc 0, a + 3 := word_rsplit b ! 0))))
 2. \<And>P. weak_det_spec P (assert (a && mask 2 = 0)) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma weak_det_spec_thread_get:
  "weak_det_spec P (thread_get f x)" apply (simp add:thread_get_def) apply (rule weak_det_spec_compose) apply (clarsimp simp:weak_det_spec_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (thread_get f x) proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (do tcb <- gets_the (get_tcb x);
return (f tcb)
od) proof (prove)
goal (2 subgoals):
 1. \<And>Q r. weak_det_spec (Q r) (return (f r))
 2. \<And>P. weak_det_spec P (gets_the (get_tcb x)) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma weak_det_spec_load_word_offs:
  "weak_det_spec P (load_word_offs buf r)" apply (clarsimp simp:load_word_offs_def) apply (clarsimp simp:do_machine_op_def) apply (rule weak_det_spec_compose)+ apply clarsimp apply (rule weak_det_spec_compose)+ apply (rule det_imply_weak_det[OF det_spec_return]) apply (rule det_imply_weak_det[OF det_spec_modify]) apply (rule weak_det_spec_select_f) apply (rule weak_det_spec_loadWord) apply (rule det_imply_weak_det[OF det_spec_gets]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (load_word_offs buf r) proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (do_machine_op (loadWord (buf + word_of_nat r * word_of_nat word_size))) proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (do ms <- gets machine_state;
(r, ms') <- select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ms);
y <- modify (update_machine ms');
return r
od) proof (prove)
goal (3 subgoals):
 1. \<And>Q r Qa ra. weak_det_spec (Qa ra) (case ra of (r, ms') \<Rightarrow> do y <- modify (update_machine ms');
return r
od)
 2. \<And>Q ra P. weak_det_spec P (select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra))
 3. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (3 subgoals):
 1. \<And>Qa a b. weak_det_spec (Qa (a, b)) (do y <- modify (update_machine b);
return a
od)
 2. \<And>Q ra P. weak_det_spec P (select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra))
 3. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (4 subgoals):
 1. \<And>Qa a b Q r. weak_det_spec (Q r) (return a)
 2. \<And>Qa a b P. weak_det_spec P (modify (update_machine b))
 3. \<And>Q ra P. weak_det_spec P (select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra))
 4. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (3 subgoals):
 1. \<And>Qa a b P. weak_det_spec P (modify (update_machine b))
 2. \<And>Q ra P. weak_det_spec P (select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra))
 3. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (2 subgoals):
 1. \<And>Q ra P. weak_det_spec P (select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra))
 2. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (2 subgoals):
 1. \<And>Q ra P Pa. weak_det_spec Pa (loadWord (buf + word_of_nat r * word_of_nat word_size))
 2. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (1 subgoal):
 1. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma empty_when_fail_fail:
  "empty_when_fail fail" by (clarsimp simp:empty_when_fail_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail fail
theory Intent_DR

lemma empty_when_fail_get:
  "empty_when_fail get" by (clarsimp simp:empty_when_fail_def get_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail get
theory Intent_DR

lemma empty_when_fail_gets:
  "empty_when_fail (gets x)" by (clarsimp simp:empty_when_fail_def get_def return_def gets_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (gets x)
theory Intent_DR

lemma empty_when_fail_assert:
  "empty_when_fail (assert x)" by(clarsimp simp:empty_when_fail_def assert_def fail_def return_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (assert x)
theory Intent_DR

lemma empty_when_fail_assert_opt:
  "empty_when_fail (assert_opt x)" by (auto simp:assert_opt_def fail_def return_def empty_when_fail_def split:option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (assert_opt x)
theory Intent_DR

lemma empty_when_fail_gets_the:
  "empty_when_fail (gets_the f)" apply (clarsimp simp:gets_the_def) apply (rule empty_when_fail_compose)+ apply (rule empty_when_fail_assert_opt) apply (rule empty_when_fail_gets)+ apply (rule det_imply_weak_det[OF det_spec_gets]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (gets_the f) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (gets f >>= assert_opt) proof (prove)
goal (3 subgoals):
 1. \<And>r. empty_when_fail (assert_opt r)
 2. empty_when_fail (gets f)
 3. \<And>P. weak_det_spec P (gets f) proof (prove)
goal (2 subgoals):
 1. empty_when_fail (gets f)
 2. \<And>P. weak_det_spec P (gets f) proof (prove)
goal (1 subgoal):
 1. \<And>P. weak_det_spec P (gets f) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma empty_when_fail_loadWord:
  "empty_when_fail (loadWord x)" apply (simp add:loadWord_def) apply (rule empty_when_fail_compose[OF _ empty_when_fail_gets]) apply (rule empty_when_fail_compose[OF empty_when_fail_return]) apply (simp_all add: weak_det_spec_simps empty_when_fail_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (loadWord x) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (do m <- gets underlying_memory;
y <- assert (x && mask 2 = 0);
return (word_rcat [m (x + 3), m (x + 2), m (x + 1), m x])
od) proof (prove)
goal (2 subgoals):
 1. \<And>r. empty_when_fail (do y <- assert (x && mask 2 = 0);
return (word_rcat [r (x + 3), r (x + 2), r (x + 1), r x])
od)
 2. \<And>P. weak_det_spec P (gets underlying_memory) proof (prove)
goal (3 subgoals):
 1. \<And>r. empty_when_fail (assert (x && mask 2 = 0))
 2. \<And>r P. weak_det_spec P (assert (x && mask 2 = 0))
 3. \<And>P. weak_det_spec P (gets underlying_memory) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma empty_when_fail_storeWord:
  "empty_when_fail (storeWord a b)" apply (simp add:storeWord_def) apply (rule empty_when_fail_compose)+ apply (simp_all add:empty_when_fail_simps weak_det_spec_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (storeWord a b) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (do y <- assert (a && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(a := word_rsplit b ! 3, a + 1 := word_rsplit b ! 2, a + 2 := word_rsplit b ! Suc 0, a + 3 := word_rsplit b ! 0)))
od) proof (prove)
goal (3 subgoals):
 1. \<And>r. empty_when_fail (modify (underlying_memory_update (\<lambda>m. m(a := word_rsplit b ! 3, a + 1 := word_rsplit b ! 2, a + 2 := word_rsplit b ! Suc 0, a + 3 := word_rsplit b ! 0))))
 2. empty_when_fail (assert (a && mask 2 = 0))
 3. \<And>P. weak_det_spec P (assert (a && mask 2 = 0)) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma empty_when_fail_select_f:
  "\<lbrakk>empty_when_fail f\<rbrakk> \<Longrightarrow> empty_when_fail (select_f (f a))" by (clarsimp simp:empty_when_fail_def select_f_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail f \<Longrightarrow> empty_when_fail (select_f (f a))
theory Intent_DR

lemma empty_when_fail_thread_get:
  "empty_when_fail (thread_get f x)" apply (clarsimp simp:thread_get_def) apply (rule empty_when_fail_compose) apply (clarsimp simp:empty_when_fail_simps weak_det_spec_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (thread_get f x) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (do tcb <- gets_the (get_tcb x);
return (f tcb)
od) proof (prove)
goal (3 subgoals):
 1. \<And>r. empty_when_fail (return (f r))
 2. empty_when_fail (gets_the (get_tcb x))
 3. \<And>P. weak_det_spec P (gets_the (get_tcb x)) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma empty_when_fail_load_word_offs:
  "empty_when_fail  (load_word_offs buf r)" apply (clarsimp simp:load_word_offs_def) apply (clarsimp simp:do_machine_op_def) apply (rule empty_when_fail_compose[OF _ empty_when_fail_gets]) apply (rule empty_when_fail_compose[OF _ empty_when_fail_select_f]) apply clarsimp apply (rule empty_when_fail_compose[OF empty_when_fail_return]) apply (simp_all add:empty_when_fail_simps weak_det_spec_simps empty_when_fail_loadWord) apply (rule weak_det_spec_select_f[OF weak_det_spec_loadWord]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (load_word_offs buf r) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (do_machine_op (loadWord (buf + word_of_nat r * word_of_nat word_size))) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (do ms <- gets machine_state;
(r, ms') <- select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ms);
y <- modify (update_machine ms');
return r
od) proof (prove)
goal (2 subgoals):
 1. \<And>ra. empty_when_fail (do (r, ms') <- select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra);
y <- modify (update_machine ms');
return r
od)
 2. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (4 subgoals):
 1. \<And>r ra. empty_when_fail (case ra of (r, ms') \<Rightarrow> do y <- modify (update_machine ms');
return r
od)
 2. \<And>ra. empty_when_fail (loadWord (buf + word_of_nat r * word_of_nat word_size))
 3. \<And>ra P. weak_det_spec P (select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra))
 4. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (4 subgoals):
 1. \<And>a b. empty_when_fail (do y <- modify (update_machine b);
return a
od)
 2. \<And>ra. empty_when_fail (loadWord (buf + word_of_nat r * word_of_nat word_size))
 3. \<And>ra P. weak_det_spec P (select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra))
 4. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (5 subgoals):
 1. \<And>a b. empty_when_fail (modify (update_machine b))
 2. \<And>a b P. weak_det_spec P (modify (update_machine b))
 3. \<And>ra. empty_when_fail (loadWord (buf + word_of_nat r * word_of_nat word_size))
 4. \<And>ra P. weak_det_spec P (select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra))
 5. \<And>P. weak_det_spec P (gets machine_state) proof (prove)
goal (1 subgoal):
 1. \<And>ra P. weak_det_spec P (select_f (loadWord (buf + word_of_nat r * word_of_nat word_size) ra)) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma empty_when_fail_get_object:
  "empty_when_fail (get_object x)" apply (simp add:get_object_def) apply (rule empty_when_fail_compose)+ apply (simp add:empty_when_fail_simps weak_det_spec_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (KHeap_A.get_object x) proof (prove)
goal (1 subgoal):
 1. empty_when_fail (do kh <- gets kheap;
y <- assert (\<exists>y. kh x = Some y);
return (the (kh x))
od) proof (prove)
goal (5 subgoals):
 1. \<And>r ra. empty_when_fail (return (the (r x)))
 2. \<And>r. empty_when_fail (assert (\<exists>y. r x = Some y))
 3. \<And>r P. weak_det_spec P (assert (\<exists>y. r x = Some y))
 4. empty_when_fail (gets kheap)
 5. \<And>P. weak_det_spec P (gets kheap) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma weak_det_spec_get_object:
  "weak_det_spec P (get_object x)" apply (simp add:get_object_def) apply (rule weak_det_spec_compose)+ apply (simp add:weak_det_spec_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (KHeap_A.get_object x) proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (do kh <- gets kheap;
y <- assert (\<exists>y. kh x = Some y);
return (the (kh x))
od) proof (prove)
goal (3 subgoals):
 1. \<And>Q r Qa ra. weak_det_spec (Qa ra) (return (the (r x)))
 2. \<And>Q r P. weak_det_spec P (assert (\<exists>y. r x = Some y))
 3. \<And>P. weak_det_spec P (gets kheap) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma not_emptyI: "a\<noteq>{} \<Longrightarrow>\<exists>x. x\<in> a" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> a
theory Intent_DR

lemma evalMonad_wp:
  "\<lbrakk>empty_when_fail f; weak_det_spec ((=) pres) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) pres \<rbrace>f\<lbrace>\<lambda>rv s. evalMonad f pres = Some rv\<rbrace>" apply (clarsimp simp:valid_def weak_det_spec_def no_fail_def empty_when_fail_def) apply (drule_tac x = pres in spec) apply (clarsimp simp:evalMonad_def notemptyI det_spec_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_when_fail f; weak_det_spec ((=) pres) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) pres\<rbrace> f \<lbrace>\<lambda>rv s. evalMonad f pres = Some rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>s. snd (f s) \<longrightarrow> fst (f s) = {}; \<not> snd (f pres) \<longrightarrow> det_spec ((=) pres) f; (a, b) \<in> fst (f pres)\<rbrakk> \<Longrightarrow> evalMonad f pres = Some a proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<not> snd (f pres) \<longrightarrow> det_spec ((=) pres) f; (a, b) \<in> fst (f pres); snd (f pres) \<longrightarrow> fst (f pres) = {}\<rbrakk> \<Longrightarrow> evalMonad f pres = Some a proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma evalMonad_thread_get:
  "evalMonad (thread_get f thread) sa = Some x \<Longrightarrow>  \<exists>tcb. get_tcb thread sa = Some tcb \<and> f tcb = x" by (clarsimp simp:thread_get_def evalMonad_def gets_def gets_the_def
    assert_opt_def bind_def get_def return_def get_tcb_def fail_def
    split:option.splits Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (thread_get f thread) sa = Some x \<Longrightarrow> \<exists>tcb. get_tcb thread sa = Some tcb \<and> f tcb = x
theory Intent_DR

lemma evalMonad_get_cap:
  "evalMonad (get_cap slot) s = caps_of_state s slot" using weak_det_spec_get_cap[where P ="(=) s" and slot = slot] using empty_when_fail_get_cap[where slot = slot] apply (clarsimp simp:evalMonad_def caps_of_state_def empty_when_fail_def
    weak_det_spec_def no_fail_def det_spec_def) apply (drule_tac x = s in spec) apply clarsimp apply (subgoal_tac "\<lbrace>(=) s\<rbrace>get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>") apply (clarsimp simp:valid_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (CSpaceAcc_A.get_cap slot) s = caps_of_state s slot proof (prove)
using this:
weak_det_spec ((=) s) (CSpaceAcc_A.get_cap slot)

goal (1 subgoal):
 1. evalMonad (CSpaceAcc_A.get_cap slot) s = caps_of_state s slot proof (prove)
using this:
weak_det_spec ((=) s) (CSpaceAcc_A.get_cap slot)
empty_when_fail (CSpaceAcc_A.get_cap slot)

goal (1 subgoal):
 1. evalMonad (CSpaceAcc_A.get_cap slot) s = caps_of_state s slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (CSpaceAcc_A.get_cap slot s) \<longrightarrow> (\<exists>a b. CSpaceAcc_A.get_cap slot s = ({(a, b)}, False)); \<forall>s. snd (CSpaceAcc_A.get_cap slot s) \<longrightarrow> fst (CSpaceAcc_A.get_cap slot s) = {}; fst (CSpaceAcc_A.get_cap slot s) \<noteq> {}\<rbrakk> \<Longrightarrow> ((\<exists>cap. fst (CSpaceAcc_A.get_cap slot s) = {(cap, s)}) \<longrightarrow> pick (fst ` fst (CSpaceAcc_A.get_cap slot s)) = (THE cap. fst (CSpaceAcc_A.get_cap slot s) = {(cap, s)})) \<and> (\<exists>cap. fst (CSpaceAcc_A.get_cap slot s) = {(cap, s)}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (CSpaceAcc_A.get_cap slot s) \<longrightarrow> (\<exists>a b. CSpaceAcc_A.get_cap slot s = ({(a, b)}, False)); fst (CSpaceAcc_A.get_cap slot s) \<noteq> {}; snd (CSpaceAcc_A.get_cap slot s) \<longrightarrow> fst (CSpaceAcc_A.get_cap slot s) = {}\<rbrakk> \<Longrightarrow> ((\<exists>cap. fst (CSpaceAcc_A.get_cap slot s) = {(cap, s)}) \<longrightarrow> pick (fst ` fst (CSpaceAcc_A.get_cap slot s)) = (THE cap. fst (CSpaceAcc_A.get_cap slot s) = {(cap, s)})) \<and> (\<exists>cap. fst (CSpaceAcc_A.get_cap slot s) = {(cap, s)}) proof (prove)
goal (1 subgoal):
 1. \<And>a b. CSpaceAcc_A.get_cap slot s = ({(a, b)}, False) \<Longrightarrow> b = s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>CSpaceAcc_A.get_cap slot s = ({(a, b)}, False); \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> b = s
 2. \<And>a b. CSpaceAcc_A.get_cap slot s = ({(a, b)}, False) \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. CSpaceAcc_A.get_cap slot s = ({(a, b)}, False) \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma evalMonad_loadWord:
  "evalMonad (loadWord x) ms =
    (if x && mask 2 = 0 then
      Some (word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x])
    else None)" by (clarsimp simp: loadWord_def gets_def get_def return_def bind_def assert_def fail_def evalMonad_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (loadWord x) ms = (if x && mask 2 = 0 then Some (word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x]) else None)
theory Intent_DR

lemma weak_det_spec_lookup_ipc_buffer:
  "weak_det_spec P (lookup_ipc_buffer a b)" apply (simp add:lookup_ipc_buffer_def) apply (rule weak_det_spec_compose)+ apply (simp_all add: empty_when_fail_simps empty_when_fail_get_cap empty_when_fail_thread_get
                         weak_det_spec_simps weak_det_spec_thread_get weak_det_spec_get_cap) apply (case_tac ra; simp add:weak_det_spec_simps) apply (rename_tac arch_cap) apply (case_tac arch_cap; simp add:weak_det_spec_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (lookup_ipc_buffer a b) proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (do buffer_ptr <- thread_get tcb_ipc_buffer b;
CSpaceAcc_A.get_cap (b, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) proof (prove)
goal (3 subgoals):
 1. \<And>Q r Qa ra. weak_det_spec (Qa ra) (case ra of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None)
 2. \<And>Q r P. weak_det_spec P (CSpaceAcc_A.get_cap (b, tcb_cnode_index 4))
 3. \<And>P. weak_det_spec P (thread_get tcb_ipc_buffer b) proof (prove)
goal (1 subgoal):
 1. \<And>r Qa ra. weak_det_spec (Qa ra) (case ra of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) proof (prove)
goal (1 subgoal):
 1. \<And>r Qa ra x12. ra = ArchObjectCap x12 \<Longrightarrow> weak_det_spec (Qa (ArchObjectCap x12)) (case x12 of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) proof (prove)
goal (1 subgoal):
 1. \<And>r Qa ra arch_cap. ra = ArchObjectCap arch_cap \<Longrightarrow> weak_det_spec (Qa (ArchObjectCap arch_cap)) (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> a then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) proof (prove)
goal:
No subgoals!