kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_AI

lemma set_untyped_cap_as_full_obj_at_impossible:
  "\<lbrace>\<lambda>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace>" apply (clarsimp simp:set_untyped_cap_as_full_def) apply (intro conjI impI) apply (wp set_cap_obj_at_impossible)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace>) \<and> ((obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<rbrace> return () \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace>) proof (prove)
goal (2 subgoals):
 1. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace>
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<rbrace> return () \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; P (obj_at P' p s) \<and> (\<forall>ko. P' ko \<longrightarrow> caps_of ko = {})\<rbrakk> \<Longrightarrow> P (obj_at P' p s) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma caps_of_state_cteD':
  "(caps_of_state m p = Some x \<and> P x) = cte_wp_at ((=) x and P) p m" by (clarsimp simp:cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (caps_of_state m p = Some x \<and> P x) = cte_wp_at ((=) x and P) p m
theory CSpace_AI

lemma disj_subst: "(\<not> A \<longrightarrow> B) \<Longrightarrow> A \<or> B" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> A \<longrightarrow> B \<Longrightarrow> A \<or> B
theory CSpace_AI

lemma derived_cap_master_cap_eq: "is_derived m n b c \<Longrightarrow> cap_master_cap b = cap_master_cap c" by (clarsimp simp:is_derived_def split:if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m n b c \<Longrightarrow> cap_master_cap b = cap_master_cap c
theory CSpace_AI

lemma cap_is_device_free_index_update_simp[simp]:
  "is_untyped_cap c \<Longrightarrow> cap_is_device (max_free_index_update c) = cap_is_device c" by (case_tac c,simp_all add:is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_untyped_cap c \<Longrightarrow> cap_is_device (max_free_index_update c) = cap_is_device c
theory CSpace_AI

lemma cap_insert_cap_refs_respects_device_region[wp]:
  "\<lbrace>cap_refs_respects_device_region
          and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> ((cap_range cap \<noteq> {}) \<longrightarrow> cap_is_device cap = cap_is_device c)) src\<rbrace>
     cap_insert cap src dest
   \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (simp add: cap_insert_def set_untyped_cap_as_full_def) apply (wp get_cap_wp set_cap_cte_wp_at' set_cap_cap_refs_respects_device_region_spec[where ptr = src]
    | simp split del: if_split)+ apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) src\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) src\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else cdt src));
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_refs_respects_device_region s \<and> cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device c)) src s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> cte_wp_at ((=) NullCap) dest s \<longrightarrow> is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> cte_wp_at (\<lambda>c. cap_range capa \<subseteq> cap_range c \<and> (cap_range capa \<noteq> {} \<longrightarrow> cap_is_device capa = cap_is_device c)) src s \<and> cap_range cap \<subseteq> cap_range capa \<and> (cap_range cap \<noteq> {} \<longrightarrow> cap_is_device cap = cap_is_device capa) \<and> cte_wp_at (\<lambda>_. True) src s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma is_derived_cap_range:
  "is_derived m srcptr cap cap'
    \<Longrightarrow> cap_range cap' = cap_range cap" by (clarsimp simp: is_derived_def cap_range_def is_cap_simps dest!: master_cap_cap_range
              split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m srcptr cap cap' \<Longrightarrow> cap_range cap' = cap_range cap
theory CSpace_AI

lemma is_derived_cap_is_device:
  "\<lbrakk>is_derived m srcptr cap cap'\<rbrakk>
    \<Longrightarrow> cap_is_device cap' = cap_is_device cap" apply (case_tac cap) apply (clarsimp simp: is_derived_def
    cap_range_def is_cap_simps cap_master_cap_def
              split: if_split_asm cap.splits )+ apply (drule arch_derived_is_device[rotated]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived m srcptr cap cap' \<Longrightarrow> cap_is_device cap' = cap_is_device cap proof (prove)
goal (12 subgoals):
 1. \<lbrakk>is_derived m srcptr cap cap'; cap = NullCap\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
 2. \<And>x21 x22 x23 x24. \<lbrakk>is_derived m srcptr cap cap'; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
 3. \<And>x31 x32 x33. \<lbrakk>is_derived m srcptr cap cap'; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
 4. \<And>x41 x42 x43. \<lbrakk>is_derived m srcptr cap cap'; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
 5. \<And>x51 x52 x53. \<lbrakk>is_derived m srcptr cap cap'; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
 6. \<And>x61 x62 x63. \<lbrakk>is_derived m srcptr cap cap'; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
 7. \<And>x7. \<lbrakk>is_derived m srcptr cap cap'; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
 8. \<lbrakk>is_derived m srcptr cap cap'; cap = DomainCap\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
 9. \<lbrakk>is_derived m srcptr cap cap'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
 10. \<And>x10. \<lbrakk>is_derived m srcptr cap cap'; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_is_device cap' = cap_is_device cap
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a. \<lbrakk>cap = ArchObjectCap x12; cap' = ArchObjectCap x12a; cap_master_arch_cap x12a = cap_master_arch_cap x12; is_derived_arch (ArchObjectCap x12) (ArchObjectCap x12a)\<rbrakk> \<Longrightarrow> arch_cap_is_device x12a = arch_cap_is_device x12 proof (prove)
goal (2 subgoals):
 1. \<And>x12 x12a. \<lbrakk>cap = ArchObjectCap x12; cap' = ArchObjectCap x12a; cap_master_arch_cap x12a = cap_master_arch_cap x12\<rbrakk> \<Longrightarrow> cap_master_arch_cap x12 = cap_master_arch_cap x12a
 2. \<And>x12 x12a. \<lbrakk>cap = ArchObjectCap x12; cap' = ArchObjectCap x12a; cap_master_arch_cap x12a = cap_master_arch_cap x12; arch_cap_is_device x12a = arch_cap_is_device x12\<rbrakk> \<Longrightarrow> arch_cap_is_device x12a = arch_cap_is_device x12 proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_cdt_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> set_cdt t \<lbrace>\<lambda>_. valid_ioc\<rbrace>" by (simp add: set_cdt_def, wp) (simp add: valid_ioc_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_cdt t \<lbrace>\<lambda>_. valid_ioc\<rbrace>
theory CSpace_AI

lemma set_original_valid_ioc[wp]:
  "\<lbrace>valid_ioc and cte_wp_at (\<lambda>x. val \<longrightarrow> x \<noteq> cap.NullCap) slot\<rbrace>
    set_original slot val
   \<lbrace>\<lambda>_. valid_ioc\<rbrace>" by (simp add: set_original_def, wp) (clarsimp simp: valid_ioc_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc and cte_wp_at (\<lambda>x. val \<longrightarrow> x \<noteq> NullCap) slot\<rbrace> set_original slot val \<lbrace>\<lambda>_. valid_ioc\<rbrace>
theory CSpace_AI

lemma cap_insert_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: cap_insert_def set_untyped_cap_as_full_def) apply (wp set_object_valid_ioc_caps set_cap_cte_wp_at get_cap_wp
    | clarsimp simp:is_cap_simps is_cap_revocable_def split del: if_split)+ apply (auto simp: valid_ioc_NullCap_not_original elim: cte_wp_cte_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else cdt src));
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_ioc s; cte_wp_at ((=) capa) src s; cte_wp_at ((=) NullCap) dest s\<rbrakk> \<Longrightarrow> ((\<exists>dev r bits f. capa = UntypedCap dev r bits f) \<and> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> (max_free_index_update capa = NullCap \<longrightarrow> \<not> is_original_cap s src) \<and> (cap = NullCap \<longrightarrow> \<not> is_original_cap s dest) \<and> (if dest = src then True else cte_wp_at (\<lambda>a. True) dest s) \<and> cte_wp_at (\<lambda>_. True) src s) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> (\<forall>dev r bits f. capa \<noteq> UntypedCap dev r bits f) \<or> (\<forall>dev r bits f. cap \<noteq> UntypedCap dev r bits f) \<or> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> (cap = NullCap \<longrightarrow> \<not> is_original_cap s dest) \<and> ((case cap of UntypedCap x xa xb xc \<Rightarrow> True | EndpointCap x xa xb \<Rightarrow> cap_ep_badge cap \<noteq> cap_ep_badge capa | NotificationCap x xa xb \<Rightarrow> cap_ep_badge cap \<noteq> cap_ep_badge capa | IRQHandlerCap x \<Rightarrow> capa = IRQControlCap | ArchObjectCap acap \<Rightarrow> arch_is_cap_revocable cap capa | _ \<Rightarrow> False) \<longrightarrow> cap \<noteq> NullCap) \<and> cte_wp_at (\<lambda>_. True) dest s) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_cdt_vms[wp]:
  "\<lbrace>valid_machine_state\<rbrace> set_cdt t \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" by (simp add: set_cdt_def, wp) (simp add: valid_machine_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> set_cdt t \<lbrace>\<lambda>_. valid_machine_state\<rbrace>
theory CSpace_AI

lemma cap_insert_vms[wp]:
  "\<lbrace>valid_machine_state\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" apply (simp add: cap_insert_def set_object_def set_untyped_cap_as_full_def) apply (wp get_object_wp get_cap_wp| simp only: vms_ioc_update | rule hoare_drop_imp | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else cdt src));
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma valid_irq_states_cdt_update[simp]:
  "valid_irq_states (s\<lparr>cdt := x\<rparr>) = valid_irq_states s" by(auto simp: valid_irq_states_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_states (s\<lparr>cdt := x\<rparr>) = valid_irq_states s
theory CSpace_AI

lemma valid_irq_states_is_original_cap_update[simp]:
  "valid_irq_states (s\<lparr>is_original_cap := x\<rparr>) = valid_irq_states s" by(auto simp: valid_irq_states_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_states (s\<lparr>is_original_cap := x\<rparr>) = valid_irq_states s
theory CSpace_AI

lemma valid_irq_states_exst_update[simp]:
  "valid_irq_states (s\<lparr>exst := x\<rparr>) = valid_irq_states s" by(auto simp: valid_irq_states_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_states (s\<lparr>exst := x\<rparr>) = valid_irq_states s
theory CSpace_AI

lemma prop_is_preserved_imp:
  "\<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace> \<Longrightarrow> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace> \<Longrightarrow> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>
theory CSpace_AI

lemma tcb_at_cte_at_0:
  "tcb_at tcb s \<Longrightarrow> cte_at (tcb, tcb_cnode_index 0) s" by (auto simp: obj_at_def cte_at_cases is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at tcb s \<Longrightarrow> cte_wp_at (\<lambda>_. True) (tcb, tcb_cnode_index 0) s
theory CSpace_AI

lemma tcb_at_cte_at_1:
  "tcb_at tcb s \<Longrightarrow> cte_at (tcb, tcb_cnode_index 1) s" by (auto simp: obj_at_def cte_at_cases is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at tcb s \<Longrightarrow> cte_wp_at (\<lambda>_. True) (tcb, tcb_cnode_index 1) s
theory CSpace_AI

lemma set_cdt_valid_objs:
  "\<lbrace>valid_objs\<rbrace> set_cdt m \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: set_cdt_def) apply wp apply (fastforce intro: valid_objs_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> set_cdt m \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> valid_objs (s\<lparr>cdt := m\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma get_cap_cte:
  "\<lbrace>\<top>\<rbrace> get_cap y \<lbrace>\<lambda>rv. cte_at y\<rbrace>" apply (clarsimp simp: valid_def) apply (frule get_cap_cte_at) apply (drule state_unchanged [OF get_cap_inv]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_cap y \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> fst (get_cap y s) \<Longrightarrow> cte_wp_at (\<lambda>_. True) y b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (get_cap y s); cte_wp_at (\<lambda>_. True) y s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) y b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cte_wp_at (\<lambda>_. True) y s; s = b\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) y b proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma cap_swap_typ_at:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> cap_swap c x c' y \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>" apply (simp add: cap_swap_def) apply (wp set_cdt_typ_at set_cap_typ_at
         |simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> cap_swap c x c' y \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do ya <- set_cap c' x;
ya <- set_cap c y;
slot1_p <- gets (\<lambda>s. cdt s x);
slot2_p <- gets (\<lambda>s. cdt s y);
cdt <- gets cdt;
ya <- set_cdt ((\<lambda>n. if cdt n = Some x then Some y else if cdt n = Some y then Some x else cdt n)(x := if cdt y = Some x then Some y else if cdt y = Some y then Some x else cdt y, y := if cdt x = Some x then Some y else if cdt x = Some y then Some x else cdt x));
ya <- do_extended_op (cap_swap_ext x y slot1_p slot2_p);
is_original <- gets is_original_cap;
ya <- set_original x (is_original y);
set_original y (is_original x)
od \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma cap_swap_valid_cap:
  "\<lbrace>valid_cap c\<rbrace> cap_swap cap x cap' y \<lbrace>\<lambda>_. valid_cap c\<rbrace>" by (simp add: cap_swap_typ_at valid_cap_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> cap_swap cap x cap' y \<lbrace>\<lambda>_. valid_cap c\<rbrace>
theory CSpace_AI

lemma cap_swap_cte_at:
  "\<lbrace>cte_at p\<rbrace> cap_swap c x c' y \<lbrace>\<lambda>_. cte_at p\<rbrace>" by (simp add: valid_cte_at_typ cap_swap_typ_at [where P="\<lambda>x. x"])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> cap_swap c x c' y \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace>
theory CSpace_AI

lemma tcb_cap_valid_typ_st:
  notes hoare_pre [wp_pre del]
  assumes x: "\<And>P t. \<lbrace>\<lambda>s. P (typ_at ATCB t s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at ATCB t s)\<rbrace>"
  and     y: "\<And>P t. \<lbrace>st_tcb_at P t\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>"
  and     z: "\<And>P t. \<lbrace>\<lambda>s. \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_ipc_buffer tcb)\<rbrace>
                       f \<lbrace>\<lambda>rv s. \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_ipc_buffer tcb)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. tcb_cap_valid cap p s\<rbrace> f \<lbrace>\<lambda>rv s. tcb_cap_valid cap p s\<rbrace>" apply (simp add: tcb_cap_valid_def) apply (simp only: imp_conv_disj tcb_at_typ) apply (wp hoare_vcg_disj_lift x y) apply (simp add: z) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_cap_valid cap p\<rbrace> f \<lbrace>\<lambda>rv. tcb_cap_valid cap p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (fst p) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) st cap) (fst p) s \<and> (snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))\<rbrace> f \<lbrace>\<lambda>rv s. tcb_at (fst p) s \<longrightarrow> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) st cap) (fst p) s \<and> (snd p = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) (fst p) s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> typ_at ATCB (fst p) s \<or> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) st cap) (fst p) s \<and> (snd p \<noteq> tcb_cnode_index 4 \<or> (\<forall>tcb. \<not> ko_at (TCB tcb) (fst p) s \<or> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))\<rbrace> f \<lbrace>\<lambda>rv s. \<not> typ_at ATCB (fst p) s \<or> st_tcb_at (\<lambda>st. case tcb_cap_cases (snd p) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst p) st cap) (fst p) s \<and> (snd p \<noteq> tcb_cnode_index 4 \<or> (\<forall>tcb. \<not> ko_at (TCB tcb) (fst p) s \<or> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>tcb. \<not> ko_at (TCB tcb) (fst p) s \<or> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>tcb. \<not> ko_at (TCB tcb) (fst p) s \<or> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)\<rbrace> proof (prove)
goal:
No subgoals!