theory Invariants_AI

lemma valid_cap_typ:
  assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_cap c s\<rbrace> f \<lbrace>\<lambda>rv s. valid_cap c s\<rbrace>" apply (simp add: valid_cap_def) apply (rule hoare_vcg_conj_lift) apply (simp add: valid_def) apply (case_tac c,
         simp_all add: valid_cap_def P P[where P=id, simplified]
                       ep_at_typ tcb_at_typ ntfn_at_typ
                       cap_table_at_typ hoare_vcg_prop) apply (rule hoare_vcg_conj_lift [OF valid_untyped_typ[OF P]]) apply (simp add: valid_def) apply (rule hoare_vcg_conj_lift [OF P hoare_vcg_prop])+ apply (rename_tac option nat) apply (case_tac option, simp_all add: tcb_at_typ cap_table_at_typ)[1] apply (rule hoare_vcg_conj_lift [OF P]) apply (rule hoare_vcg_prop) apply (rule hoare_vcg_conj_lift [OF P]) apply (rule hoare_vcg_prop) apply (wp valid_arch_cap_typ P) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s \<turnstile> c\<rbrace> f \<lbrace>\<lambda>rv s. s \<turnstile> c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_aligned c \<and> (case c of UntypedCap dev p b f \<Rightarrow> valid_untyped c s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True)\<rbrace> f \<lbrace>\<lambda>rv s. cap_aligned c \<and> (case c of UntypedCap dev p b f \<Rightarrow> valid_untyped c s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. cap_aligned c\<rbrace> f \<lbrace>\<lambda>rv s. cap_aligned c\<rbrace>
 2. \<lbrace>\<lambda>s. case c of UntypedCap dev p b f \<Rightarrow> valid_untyped c s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True\<rbrace> f \<lbrace>\<lambda>rv s. case c of UntypedCap dev p b f \<Rightarrow> valid_untyped c s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case c of UntypedCap dev p b f \<Rightarrow> valid_untyped c s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True\<rbrace> f \<lbrace>\<lambda>rv s. case c of UntypedCap dev p b f \<Rightarrow> valid_untyped c s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24. c = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>s. valid_untyped (UntypedCap x21 x22 x23 x24) s \<and> untyped_min_bits \<le> x23 \<and> x24 \<le> 2 ^ x23 \<and> x22 \<noteq> 0\<rbrace> f \<lbrace>\<lambda>rv s. valid_untyped (UntypedCap x21 x22 x23 x24) s \<and> untyped_min_bits \<le> x23 \<and> x24 \<le> 2 ^ x23 \<and> x22 \<noteq> 0\<rbrace>
 2. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at ANTFN x41 s \<and> AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43\<rbrace> f \<lbrace>\<lambda>rv s. typ_at ANTFN x41 s \<and> AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43\<rbrace>
 3. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at ATCB x51 s \<and> AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53\<rbrace> f \<lbrace>\<lambda>rv s. typ_at ATCB x51 s \<and> AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53\<rbrace>
 4. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (ACapTable x62) x61 s \<and> 0 < x62 \<and> length x63 \<le> word_bits\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (ACapTable x62) x61 s \<and> 0 < x62 \<and> length x63 \<le> word_bits\<rbrace>
 5. \<And>x111 x112 x113. c = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>s. case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace> f \<lbrace>\<lambda>rv s. case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace>
 6. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24. c = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>s. untyped_min_bits \<le> x23 \<and> x24 \<le> 2 ^ x23 \<and> x22 \<noteq> 0\<rbrace> f \<lbrace>\<lambda>rv s. untyped_min_bits \<le> x23 \<and> x24 \<le> 2 ^ x23 \<and> x22 \<noteq> 0\<rbrace>
 2. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at ANTFN x41 s \<and> AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43\<rbrace> f \<lbrace>\<lambda>rv s. typ_at ANTFN x41 s \<and> AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43\<rbrace>
 3. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at ATCB x51 s \<and> AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53\<rbrace> f \<lbrace>\<lambda>rv s. typ_at ATCB x51 s \<and> AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53\<rbrace>
 4. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (ACapTable x62) x61 s \<and> 0 < x62 \<and> length x63 \<le> word_bits\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (ACapTable x62) x61 s \<and> 0 < x62 \<and> length x63 \<le> word_bits\<rbrace>
 5. \<And>x111 x112 x113. c = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>s. case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace> f \<lbrace>\<lambda>rv s. case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace>
 6. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at ANTFN x41 s \<and> AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43\<rbrace> f \<lbrace>\<lambda>rv s. typ_at ANTFN x41 s \<and> AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43\<rbrace>
 2. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at ATCB x51 s \<and> AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53\<rbrace> f \<lbrace>\<lambda>rv s. typ_at ATCB x51 s \<and> AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53\<rbrace>
 3. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (ACapTable x62) x61 s \<and> 0 < x62 \<and> length x63 \<le> word_bits\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (ACapTable x62) x61 s \<and> 0 < x62 \<and> length x63 \<le> word_bits\<rbrace>
 4. \<And>x111 x112 x113. c = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>s. case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace> f \<lbrace>\<lambda>rv s. case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace>
 5. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. c = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>s. case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace> f \<lbrace>\<lambda>rv s. case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace>
 2. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x111 option nat. c = Zombie x111 option nat \<Longrightarrow> \<lbrace>\<lambda>s. case option of None \<Rightarrow> tcb_at x111 s \<and> nat \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> nat \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace> f \<lbrace>\<lambda>rv s. case option of None \<Rightarrow> tcb_at x111 s \<and> nat \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> nat \<le> 2 ^ b \<and> b \<noteq> 0\<rbrace>
 2. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x111 option nat. \<lbrakk>c = Zombie x111 None nat; option = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at ATCB x111 s \<and> nat \<le> 5\<rbrace> f \<lbrace>\<lambda>rv s. typ_at ATCB x111 s \<and> nat \<le> 5\<rbrace>
 2. \<And>x111 option nat a. \<lbrakk>c = Zombie x111 (Some a) nat; option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (ACapTable a) x111 s \<and> nat \<le> 2 ^ a \<and> 0 < a\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (ACapTable a) x111 s \<and> nat \<le> 2 ^ a \<and> 0 < a\<rbrace>
 3. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x111 option nat. \<lbrakk>c = Zombie x111 None nat; option = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. nat \<le> 5\<rbrace> f \<lbrace>\<lambda>rv s. nat \<le> 5\<rbrace>
 2. \<And>x111 option nat a. \<lbrakk>c = Zombie x111 (Some a) nat; option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (ACapTable a) x111 s \<and> nat \<le> 2 ^ a \<and> 0 < a\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (ACapTable a) x111 s \<and> nat \<le> 2 ^ a \<and> 0 < a\<rbrace>
 3. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x111 option nat a. \<lbrakk>c = Zombie x111 (Some a) nat; option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. typ_at (ACapTable a) x111 s \<and> nat \<le> 2 ^ a \<and> 0 < a\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (ACapTable a) x111 s \<and> nat \<le> 2 ^ a \<and> 0 < a\<rbrace>
 2. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x111 option nat a. \<lbrakk>c = Zombie x111 (Some a) nat; option = Some a\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. nat \<le> 2 ^ a \<and> 0 < a\<rbrace> f \<lbrace>\<lambda>rv s. nat \<le> 2 ^ a \<and> 0 < a\<rbrace>
 2. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> \<lbrace>valid_arch_cap x12\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_cap x12\<rbrace> proof (prove)
goal:
No subgoals!