theory Syscall_S

lemma set_cap_NullCap_separate_state [wp]:
  "\<lbrace>separate_state\<rbrace> set_cap NullCap cptr \<lbrace>\<lambda>_. separate_state\<rbrace>" unfolding separate_state_def separate_tcb_def separate_cnode_cap_def apply (simp add: tcb_at_typ) apply (rule hoare_pre) apply wps apply (wp set_cap_typ_at hoare_vcg_all_lift) apply (clarsimp simp: separate_cap_def) apply (drule spec, drule (1) mp) apply (clarsimp split: cap.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> set_cap NullCap cptr \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. tcb_at p s \<longrightarrow> (case caps_of_state s (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (p, tcb_cnode_index 3) = Some NullCap\<rbrace> set_cap NullCap cptr \<lbrace>\<lambda>_ s. \<forall>p. tcb_at p s \<longrightarrow> (case caps_of_state s (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (p, tcb_cnode_index 3) = Some NullCap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. typ_at ATCB p s \<longrightarrow> (case caps_of_state s (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (p, tcb_cnode_index 3) = Some NullCap\<rbrace> set_cap NullCap cptr \<lbrace>\<lambda>_ s. \<forall>p. typ_at ATCB p s \<longrightarrow> (case caps_of_state s (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (p, tcb_cnode_index 3) = Some NullCap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> set_cap NullCap cptr \<lbrace>\<lambda>_ s. \<forall>p. typ_at ATCB p s \<longrightarrow> (case caps_of_state s (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (p, tcb_cnode_index 3) = Some NullCap\<rbrace>
 2. \<And>s. \<forall>p. typ_at ATCB p s \<longrightarrow> (case caps_of_state s (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (p, tcb_cnode_index 3) = Some NullCap \<Longrightarrow> ?Q3 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P6 prev_s\<rbrace> set_cap NullCap cptr \<lbrace>\<lambda>rv s'. \<forall>p. typ_at ATCB p s' \<longrightarrow> (case ((caps_of_state prev_s)(cptr \<mapsto> NullCap)) (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case ((caps_of_state prev_s)(cptr \<mapsto> NullCap)) (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> ((caps_of_state prev_s)(cptr \<mapsto> NullCap)) (p, tcb_cnode_index 3) = Some NullCap\<rbrace>
 2. \<And>s. \<forall>p. typ_at ATCB p s \<longrightarrow> (case caps_of_state s (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (p, tcb_cnode_index 3) = Some NullCap \<Longrightarrow> ?P6 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>p. typ_at ATCB p s \<longrightarrow> (case caps_of_state s (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (p, tcb_cnode_index 3) = Some NullCap \<Longrightarrow> \<forall>x. typ_at ATCB x s \<longrightarrow> (case ((caps_of_state s)(cptr \<mapsto> NullCap)) (x, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case ((caps_of_state s)(cptr \<mapsto> NullCap)) (p, off) of None \<Rightarrow> True | Some a \<Rightarrow> separate_cap a) | Some _ \<Rightarrow> False) \<and> ((caps_of_state s)(cptr \<mapsto> NullCap)) (x, tcb_cnode_index 3) = Some NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<forall>p. typ_at ATCB p s \<longrightarrow> (case caps_of_state s (p, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (p, tcb_cnode_index 3) = Some NullCap; (x, tcb_cnode_index 0) \<noteq> cptr; typ_at ATCB x s\<rbrakk> \<Longrightarrow> case caps_of_state s (x, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case ((caps_of_state s)(cptr \<mapsto> NullCap)) (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>(x, tcb_cnode_index 0) \<noteq> cptr; typ_at ATCB x s; (case caps_of_state s (x, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case caps_of_state s (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False) \<and> caps_of_state s (x, tcb_cnode_index 3) = Some NullCap\<rbrakk> \<Longrightarrow> case caps_of_state s (x, tcb_cnode_index 0) of None \<Rightarrow> True | Some NullCap \<Rightarrow> True | Some (CNodeCap p bits guard) \<Rightarrow> bits + length guard = word_bits \<and> (\<forall>off. case ((caps_of_state s)(cptr \<mapsto> NullCap)) (p, off) of None \<Rightarrow> True | Some x \<Rightarrow> separate_cap x) | Some _ \<Rightarrow> False proof (prove)
goal:
No subgoals!