kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_AI

lemma valid_untyped_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>valid_untyped (UntypedCap dev r n fr)\<rbrace> f
         \<lbrace>\<lambda>rv. valid_untyped (UntypedCap dev r n fr)\<rbrace>" unfolding valid_untyped_T apply (rule hoare_vcg_all_lift) apply (rule hoare_vcg_all_lift) apply (rule hoare_vcg_disj_lift [OF P]) apply (rule hoare_vcg_prop) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_untyped (UntypedCap dev r n fr)\<rbrace> f \<lbrace>\<lambda>rv. valid_untyped (UntypedCap dev r n fr)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>T p. \<not> typ_at T p s \<or> typ_range p T \<inter> untyped_range (UntypedCap dev r n fr) = {} \<or> typ_range p T \<subseteq> untyped_range (UntypedCap dev r n fr) \<and> typ_range p T \<inter> usable_untyped_range (UntypedCap dev r n fr) = {}\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>T p. \<not> typ_at T p s \<or> typ_range p T \<inter> untyped_range (UntypedCap dev r n fr) = {} \<or> typ_range p T \<subseteq> untyped_range (UntypedCap dev r n fr) \<and> typ_range p T \<inter> usable_untyped_range (UntypedCap dev r n fr) = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>T. \<lbrace>\<lambda>s. \<forall>p. \<not> typ_at T p s \<or> typ_range p T \<inter> untyped_range (UntypedCap dev r n fr) = {} \<or> typ_range p T \<subseteq> untyped_range (UntypedCap dev r n fr) \<and> typ_range p T \<inter> usable_untyped_range (UntypedCap dev r n fr) = {}\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>p. \<not> typ_at T p s \<or> typ_range p T \<inter> untyped_range (UntypedCap dev r n fr) = {} \<or> typ_range p T \<subseteq> untyped_range (UntypedCap dev r n fr) \<and> typ_range p T \<inter> usable_untyped_range (UntypedCap dev r n fr) = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>T p. \<lbrace>\<lambda>s. \<not> typ_at T p s \<or> typ_range p T \<inter> untyped_range (UntypedCap dev r n fr) = {} \<or> typ_range p T \<subseteq> untyped_range (UntypedCap dev r n fr) \<and> typ_range p T \<inter> usable_untyped_range (UntypedCap dev r n fr) = {}\<rbrace> f \<lbrace>\<lambda>rv s. \<not> typ_at T p s \<or> typ_range p T \<inter> untyped_range (UntypedCap dev r n fr) = {} \<or> typ_range p T \<subseteq> untyped_range (UntypedCap dev r n fr) \<and> typ_range p T \<inter> usable_untyped_range (UntypedCap dev r n fr) = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>T p. \<lbrace>\<lambda>s. typ_range p T \<inter> untyped_range (UntypedCap dev r n fr) = {} \<or> typ_range p T \<subseteq> untyped_range (UntypedCap dev r n fr) \<and> typ_range p T \<inter> usable_untyped_range (UntypedCap dev r n fr) = {}\<rbrace> f \<lbrace>\<lambda>rv s. typ_range p T \<inter> untyped_range (UntypedCap dev r n fr) = {} \<or> typ_range p T \<subseteq> untyped_range (UntypedCap dev r n fr) \<and> typ_range p T \<inter> usable_untyped_range (UntypedCap dev r n fr) = {}\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma cap_aligned_Null [simp]:
  "cap_aligned (NullCap)" by (simp add: cap_aligned_def word_bits_def is_aligned_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_aligned NullCap
theory Invariants_AI

lemma valid_tcb_state_typ:
  assumes P: "\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at T p\<rbrace>"
  shows      "\<lbrace>\<lambda>s. valid_tcb_state st s\<rbrace> f \<lbrace>\<lambda>rv s. valid_tcb_state st s\<rbrace>" by (case_tac st,
      simp_all add: valid_tcb_state_def hoare_post_taut
                    ep_at_typ P tcb_at_typ ntfn_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_tcb_state st\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb_state st\<rbrace>
theory Invariants_AI

lemma ntfn_at_typ_at:
  "(\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at T p\<rbrace>) \<Longrightarrow> \<lbrace>ntfn_at c\<rbrace> f \<lbrace>\<lambda>rv. ntfn_at c\<rbrace>" by (simp add: ntfn_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at T p\<rbrace>) \<Longrightarrow> \<lbrace>ntfn_at c\<rbrace> f \<lbrace>\<lambda>rv. ntfn_at c\<rbrace>
theory Invariants_AI

lemma valid_tcb_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_tcb p tcb s\<rbrace> f \<lbrace>\<lambda>rv s. valid_tcb p tcb s\<rbrace>" apply (simp add: valid_tcb_def valid_bound_ntfn_def split_def) apply (wp valid_tcb_state_typ valid_cap_typ P hoare_vcg_const_Ball_lift
            valid_case_option_post_wp ntfn_at_typ_at valid_arch_tcb_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_tcb p tcb\<rbrace> f \<lbrace>\<lambda>rv. valid_tcb p tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>x\<in>ran tcb_cap_cases. s \<turnstile> fst x tcb \<and> snd (snd x) p (tcb_state tcb) (fst x tcb)) \<and> valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb) \<and> valid_tcb_state (tcb_state tcb) s \<and> (case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f) \<and> length (tcb_fault_handler tcb) = word_bits \<and> (case tcb_bound_notification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) \<and> valid_arch_tcb (tcb_arch tcb) s\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>x\<in>ran tcb_cap_cases. s \<turnstile> fst x tcb \<and> snd (snd x) p (tcb_state tcb) (fst x tcb)) \<and> valid_ipc_buffer_cap (tcb_ipcframe tcb) (tcb_ipc_buffer tcb) \<and> valid_tcb_state (tcb_state tcb) s \<and> (case tcb_fault tcb of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f) \<and> length (tcb_fault_handler tcb) = word_bits \<and> (case tcb_bound_notification tcb of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s) \<and> valid_arch_tcb (tcb_arch tcb) s\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma valid_cs_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_cs sz cs s\<rbrace> f \<lbrace>\<lambda>rv s. valid_cs sz cs s\<rbrace>" apply (simp add: valid_cs_def) apply (rule hoare_vcg_conj_lift [OF _ hoare_vcg_prop]) apply (rule hoare_vcg_const_Ball_lift) apply (rule valid_cap_typ [OF P]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cs sz cs\<rbrace> f \<lbrace>\<lambda>rv. valid_cs sz cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>cap\<in>ran cs. s \<turnstile> cap) \<and> valid_cs_size sz cs\<rbrace> f \<lbrace>\<lambda>rv s. (\<forall>cap\<in>ran cs. s \<turnstile> cap) \<and> valid_cs_size sz cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap\<in>ran cs. s \<turnstile> cap\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran cs. s \<turnstile> cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap \<in> ran cs \<Longrightarrow> \<lbrace>\<lambda>s. s \<turnstile> cap\<rbrace> f \<lbrace>\<lambda>rv s. s \<turnstile> cap\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma valid_obj_typ:
  assumes P: "\<And>P p T. \<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_obj p ob s\<rbrace> f \<lbrace>\<lambda>rv s. valid_obj p ob s\<rbrace>" apply (case_tac ob, simp_all add: valid_obj_def P P [where P=id, simplified]
         wellformed_arch_typ
         valid_cs_typ valid_tcb_typ valid_ep_typ valid_ntfn_typ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_obj p ob\<rbrace> f \<lbrace>\<lambda>rv. valid_obj p ob\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma valid_irq_node_typ:
  assumes P: "\<And>p. \<lbrace>\<lambda>s. typ_at (ACapTable 0) p s\<rbrace> f \<lbrace>\<lambda>rv s. typ_at (ACapTable 0) p s\<rbrace>"
  assumes Q: "\<And>P. \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> f \<lbrace>\<lambda>rv s. P (interrupt_irq_node s)\<rbrace>"
  shows      "\<lbrace>valid_irq_node\<rbrace> f \<lbrace>\<lambda>rv. valid_irq_node\<rbrace>" apply (simp add: valid_irq_node_def cap_table_at_typ) apply (wp Q hoare_use_eq [OF Q P] hoare_vcg_all_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_node\<rbrace> f \<lbrace>\<lambda>rv. valid_irq_node\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. typ_at (ACapTable 0) (interrupt_irq_node s irq) s)\<rbrace> f \<lbrace>\<lambda>rv s. inj (interrupt_irq_node s) \<and> (\<forall>irq. typ_at (ACapTable 0) (interrupt_irq_node s irq) s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma wf_cs_upd:
  "\<lbrakk> cs x = Some y \<rbrakk> \<Longrightarrow>
     well_formed_cnode_n n (cs (x \<mapsto> z)) = well_formed_cnode_n n cs" apply (clarsimp simp: well_formed_cnode_n_def) apply (subst insert_absorb) apply (erule domI) apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cs x = Some y \<Longrightarrow> well_formed_cnode_n n (cs(x \<mapsto> z)) = well_formed_cnode_n n cs proof (prove)
goal (1 subgoal):
 1. cs x = Some y \<Longrightarrow> (insert x (dom cs) = {x. length x = n}) = (dom cs = {x. length x = n}) proof (prove)
goal (2 subgoals):
 1. cs x = Some y \<Longrightarrow> x \<in> dom cs
 2. cs x = Some y \<Longrightarrow> (dom cs = {x. length x = n}) = (dom cs = {x. length x = n}) proof (prove)
goal (1 subgoal):
 1. cs x = Some y \<Longrightarrow> (dom cs = {x. length x = n}) = (dom cs = {x. length x = n}) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma is_cap_simps:
  "is_cnode_cap cap = (\<exists>r bits g. cap = CNodeCap r bits g)"
  "is_thread_cap cap = (\<exists>r. cap = ThreadCap r)"
  "is_domain_cap cap = (cap = DomainCap)"
  "is_untyped_cap cap = (\<exists>dev r bits f. cap = UntypedCap dev r bits f)"
  "is_ep_cap cap = (\<exists>r b R. cap = EndpointCap r b R)"
  "is_ntfn_cap cap = (\<exists>r b R. cap = NotificationCap r b R)"
  "is_zombie cap = (\<exists>r b n. cap = Zombie r b n)"
  "is_arch_cap cap = (\<exists>a. cap = ArchObjectCap a)"
  "is_reply_cap cap = (\<exists>x R. cap = ReplyCap x False R)"
  "is_master_reply_cap cap = (\<exists>x R. cap = ReplyCap x True R)" by (cases cap, auto simp: is_zombie_def is_arch_cap_def
                            is_reply_cap_def is_master_reply_cap_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((is_cnode_cap cap = (\<exists>r bits g. cap = CNodeCap r bits g) &&& is_thread_cap cap = (\<exists>r. cap = ThreadCap r)) &&& is_domain_cap cap = (cap = DomainCap) &&& is_untyped_cap cap = (\<exists>dev r bits f. cap = UntypedCap dev r bits f) &&& is_ep_cap cap = (\<exists>r b R. cap = EndpointCap r b R)) &&& (is_ntfn_cap cap = (\<exists>r b R. cap = NotificationCap r b R) &&& is_zombie cap = (\<exists>r b n. cap = Zombie r b n)) &&& is_arch_cap cap = (\<exists>a. cap = ArchObjectCap a) &&& is_reply_cap cap = (\<exists>x R. cap = ReplyCap x False R) &&& is_master_reply_cap cap = (\<exists>x R. cap = ReplyCap x True R)
theory Invariants_AI

lemma wf_unique:
  "well_formed_cnode_n bits f \<Longrightarrow>
  (THE n. well_formed_cnode_n n f) = bits" by (clarsimp simp: well_formed_cnode_n_def length_set_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n bits f \<Longrightarrow> (THE n. well_formed_cnode_n n f) = bits
theory Invariants_AI

lemma wf_obj_bits:
  "well_formed_cnode_n bits f \<Longrightarrow> obj_bits (CNode bits f) = cte_level_bits + bits" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n bits f \<Longrightarrow> obj_bits (CNode bits f) = cte_level_bits + bits
theory Invariants_AI

lemma wf_cs_n_unique:
  "\<lbrakk> well_formed_cnode_n n f; well_formed_cnode_n n' f \<rbrakk>
  \<Longrightarrow> n = n'" by (clarsimp simp: well_formed_cnode_n_def length_set_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed_cnode_n n f; well_formed_cnode_n n' f\<rbrakk> \<Longrightarrow> n = n'
theory Invariants_AI

lemma typ_at_eq_kheap_obj:
  "typ_at ATCB p s \<longleftrightarrow> (\<exists>tcb. kheap s p = Some (TCB tcb))"
  "typ_at AEndpoint p s \<longleftrightarrow> (\<exists>ep. kheap s p = Some (Endpoint ep))"
  "typ_at ANTFN p s \<longleftrightarrow> (\<exists>ntfn. kheap s p = Some (Notification ntfn))"
  "typ_at (ACapTable n) p s \<longleftrightarrow>
   (\<exists>cs. kheap s p = Some (CNode n cs) \<and> well_formed_cnode_n n cs)"
  "typ_at (AGarbage n) p s \<longleftrightarrow>
   (\<exists>cs. n \<ge> cte_level_bits \<and> kheap s p = Some (CNode (n - cte_level_bits) cs) \<and> \<not> well_formed_cnode_n (n - cte_level_bits) cs)" by ((clarsimp simp add: obj_at_def a_type_def; rule iffI; clarsimp),
      case_tac ko; fastforce simp: wf_unique
                             split: if_split_asm kernel_object.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (typ_at ATCB p s = (\<exists>tcb. kheap s p = Some (TCB tcb)) &&& typ_at AEndpoint p s = (\<exists>ep. kheap s p = Some (Endpoint ep))) &&& typ_at ANTFN p s = (\<exists>ntfn. kheap s p = Some (Notification ntfn)) &&& typ_at (ACapTable n) p s = (\<exists>cs. kheap s p = Some (CNode n cs) \<and> well_formed_cnode_n n cs) &&& typ_at (AGarbage n) p s = (\<exists>cs. cte_level_bits \<le> n \<and> kheap s p = Some (CNode (n - cte_level_bits) cs) \<and> \<not> well_formed_cnode_n (n - cte_level_bits) cs)
theory Invariants_AI

lemma a_type_ACapTableE:
  "\<lbrakk>a_type ko = ACapTable n;
    (!!cs. \<lbrakk>ko = CNode n cs; well_formed_cnode_n n cs\<rbrakk> \<Longrightarrow> R)\<rbrakk>
   \<Longrightarrow> R" by (case_tac ko, simp_all add: a_type_simps split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_type ko = ACapTable n; \<And>cs. \<lbrakk>ko = CNode n cs; well_formed_cnode_n n cs\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Invariants_AI

lemma a_type_AGarbageE:
  "\<lbrakk>a_type ko = AGarbage n;
    (!!cs. \<lbrakk>n \<ge> cte_level_bits; ko = CNode (n - cte_level_bits) cs; \<not>well_formed_cnode_n (n - cte_level_bits) cs\<rbrakk> \<Longrightarrow> R)\<rbrakk>
   \<Longrightarrow> R" by (case_tac ko, simp_all add: a_type_simps split: if_split_asm, fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_type ko = AGarbage n; \<And>cs. \<lbrakk>cte_level_bits \<le> n; ko = CNode (n - cte_level_bits) cs; \<not> well_formed_cnode_n (n - cte_level_bits) cs\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Invariants_AI

lemma a_type_ATCBE:
  "\<lbrakk>a_type ko = ATCB; (!!tcb. ko = TCB tcb \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R" by (case_tac ko, simp_all add: a_type_simps split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_type ko = ATCB; \<And>tcb. ko = TCB tcb \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Invariants_AI

lemma a_type_AEndpointE:
  "\<lbrakk>a_type ko = AEndpoint; (!!ep. ko = Endpoint ep \<Longrightarrow> R)\<rbrakk> \<Longrightarrow> R" by (case_tac ko, simp_all add: a_type_simps split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a_type ko = AEndpoint; \<And>ep. ko = Endpoint ep \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Invariants_AI

lemma P_null_filter_caps_of_cte_wp_at:
  "\<not> P NullCap \<Longrightarrow>
   (null_filter (caps_of_state s) x \<noteq> None \<and> P (the (null_filter (caps_of_state s) x)))
     = (cte_wp_at P x s)" by (simp add: cte_wp_at_caps_of_state null_filter_def, fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> P NullCap \<Longrightarrow> (null_filter (caps_of_state s) x \<noteq> None \<and> P (the (null_filter (caps_of_state s) x))) = cte_wp_at P x s
theory Invariants_AI

lemma cte_wp_at_cte_at:
  "cte_wp_at P p s \<Longrightarrow> cte_at p s" by (erule cte_wp_at_weakenE, rule TrueI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P p s \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
theory Invariants_AI

lemma real_cte_at_cte:
  "real_cte_at cref s \<Longrightarrow> cte_at cref s" by (cases cref, clarsimp simp: cap_table_at_cte_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. real_cte_at cref s \<Longrightarrow> cte_wp_at (\<lambda>_. True) cref s
theory Invariants_AI

lemma swp_cte_at_caps_of:
  "swp (cte_wp_at P) s = (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> P c)" apply (rule ext) apply (simp add: cte_wp_at_caps_of_state swp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. swp (cte_wp_at P) s = (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> P c) proof (prove)
goal (1 subgoal):
 1. \<And>p. swp (cte_wp_at P) s p = (\<exists>c. caps_of_state s p = Some c \<and> P c) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma valid_mdb_def2:
  "valid_mdb = (\<lambda>s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and>
                    untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and>
                    no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and>
                    ut_revocable (is_original_cap s) (caps_of_state s) \<and>
                    irq_revocable (is_original_cap s) (caps_of_state s) \<and>
                    reply_master_revocable (is_original_cap s) (caps_of_state s) \<and>
                    reply_mdb (cdt s) (caps_of_state s) \<and>
                    valid_arch_mdb (is_original_cap s) (caps_of_state s))" by (auto simp add: valid_mdb_def swp_cte_at_caps_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb = (\<lambda>s. mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> NullCap \<noteq> c) (cdt s) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s))
theory Invariants_AI

lemma caps_of_state_cte_at:
  "caps_of_state s p = Some c \<Longrightarrow> cte_at p s" by (simp add: cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s p = Some c \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
theory Invariants_AI

lemma cte_wp_cte_at:
  "cte_wp_at P p s \<Longrightarrow> cte_at p s" by (auto simp add: cte_wp_at_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P p s \<Longrightarrow> cte_wp_at (\<lambda>_. True) p s
theory Invariants_AI

lemma cte_wp_at_update [iff]:
  "cte_wp_at P p (f s) = cte_wp_at P p s" by (fastforce intro: cte_wp_at_pspaceI simp: pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P p (f s) = cte_wp_at P p s
theory Invariants_AI

lemma iflive_update [iff]:
  "if_live_then_nonz_cap (f s) = if_live_then_nonz_cap s" by (simp add: if_live_then_nonz_cap_def ex_nonz_cap_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_live_then_nonz_cap (f s) = if_live_then_nonz_cap s
theory Invariants_AI

lemma valid_objs_update [iff]:
  "valid_objs (f s) = valid_objs s" by (fastforce intro: valid_objs_pspaceI simp: pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_objs (f s) = valid_objs s
theory Invariants_AI

lemma pspace_aligned_update [iff]:
  "pspace_aligned (f s) = pspace_aligned s" by (simp add: pspace_aligned_def pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_aligned (f s) = pspace_aligned s
theory Invariants_AI

lemma pred_tcb_at_update [iff]:
  "pred_tcb_at proj P p (f s) = pred_tcb_at proj P p s" by (simp add: pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj P p (f s) = pred_tcb_at proj P p s
theory Invariants_AI

lemma valid_cap_update [iff]:
  "(f s) \<turnstile> c = s \<turnstile> c" by (auto intro: valid_cap_pspaceI simp: pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f s \<turnstile> c = s \<turnstile> c
theory Invariants_AI

lemma valid_refs_update [iff]:
  "valid_refs R (f s) = valid_refs R s" by (simp add: valid_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_refs R (f s) = valid_refs R s
theory Invariants_AI

lemma has_reply_cap_update [iff]:
  "has_reply_cap t (f s) = has_reply_cap t s" by (simp add: has_reply_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. has_reply_cap t (f s) = has_reply_cap t s
theory Invariants_AI

lemma valid_reply_caps_update [iff]:
  "valid_reply_caps (f s) = valid_reply_caps s" by (simp add: valid_reply_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_reply_caps (f s) = valid_reply_caps s
theory Invariants_AI

lemma valid_reply_masters_update [iff]:
  "valid_reply_masters (f s) = valid_reply_masters s" by (simp add: valid_reply_masters_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_reply_masters (f s) = valid_reply_masters s
theory Invariants_AI

lemma valid_vspace_objs_update [iff]:
  "valid_vspace_objs (f s) = valid_vspace_objs s" by (simp add: valid_vspace_objs_def arch pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs (f s) = valid_vspace_objs s
theory Invariants_AI

lemma valid_arch_cap_update [iff]:
  "valid_arch_caps (f s) = valid_arch_caps s" by (simp add: valid_arch_caps_def pspace arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_caps (f s) = valid_arch_caps s
theory Invariants_AI

lemma valid_global_objs_update [iff]:
  "valid_global_objs (f s) = valid_global_objs s" by (simp add: valid_global_objs_def arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_objs (f s) = valid_global_objs s
theory Invariants_AI

lemma valid_global_vspace_mappings_update [iff]:
  "valid_global_vspace_mappings (f s) = valid_global_vspace_mappings s" unfolding valid_global_vspace_mappings_def by (simp add: arch Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_vspace_mappings (f s) = valid_global_vspace_mappings s proof (prove)
goal (1 subgoal):
 1. obj_at (valid_pd_kernel_mappings (arm_kernel_vspace (arch_state (f s))) (f s)) (arm_global_pd (arch_state (f s))) (f s) = obj_at (valid_pd_kernel_mappings (arm_kernel_vspace (arch_state s)) s) (arm_global_pd (arch_state s)) s
theory Invariants_AI

lemma pspace_in_kernel_window_update [iff]:
  "pspace_in_kernel_window (f s) = pspace_in_kernel_window s" by (simp add: pspace_in_kernel_window_def arch pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_in_kernel_window (f s) = pspace_in_kernel_window s
theory Invariants_AI

lemma cap_refs_in_kernel_window_update [iff]:
  "cap_refs_in_kernel_window (f s) = cap_refs_in_kernel_window s" by (simp add: cap_refs_in_kernel_window_def arch pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_refs_in_kernel_window (f s) = cap_refs_in_kernel_window s
theory Invariants_AI

lemma valid_ioports_update[iff]:
  "valid_ioports (f s) = valid_ioports s" by (simp add: valid_ioports_def arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioports (f s) = valid_ioports s
theory Invariants_AI

lemma ifunsafe_update [iff]:
  "if_unsafe_then_cap (f s) = if_unsafe_then_cap s" by (simp add: if_unsafe_then_cap_def ex_cte_cap_wp_to_def irq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap (f s) = if_unsafe_then_cap s