theory CNodeInv_AI

lemma rec_del_emptyable:
 "\<And>args.
    \<lbrace>invs and valid_rec_del_call args
          and (\<lambda>s. \<not> exposed_rdcall args
                     \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s)
          and emptyable (slot_rdcall args)
          and (\<lambda>s. case args of ReduceZombieCall cap sl ex \<Rightarrow>
                             \<not> cap_removeable cap sl
                             \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s)
                      | _ \<Rightarrow> True)\<rbrace>
      rec_del args
    \<lbrace>\<lambda>rv. emptyable (slot_rdcall args) :: 'state_ext state \<Rightarrow> bool\<rbrace>, -" apply (rule validE_validE_R) apply (rule hoare_post_impErr) apply (rule hoare_pre) apply (rule use_spec) apply (rule rec_del_invs') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>args. \<lbrace>invs and valid_rec_del_call args and (\<lambda>s. \<not> exposed_rdcall args \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s) and emptyable (slot_rdcall args) and (\<lambda>s. case args of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)\<rbrace> rec_del args \<lbrace>\<lambda>rv. emptyable (slot_rdcall args)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>args. \<lbrace>invs and valid_rec_del_call args and (\<lambda>s. \<not> exposed_rdcall args \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s) and emptyable (slot_rdcall args) and (\<lambda>s. case args of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)\<rbrace> rec_del args \<lbrace>\<lambda>rv. emptyable (slot_rdcall args)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>args. \<lbrace>invs and valid_rec_del_call args and (\<lambda>s. \<not> exposed_rdcall args \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s) and emptyable (slot_rdcall args) and (\<lambda>s. case args of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)\<rbrace> rec_del args \<lbrace>?Q2 args\<rbrace>, \<lbrace>?E2 args\<rbrace>
 2. \<And>args rv s. ?Q2 args rv s \<Longrightarrow> emptyable (slot_rdcall args) s
 3. \<And>args e s. ?E2 args e s \<Longrightarrow> True proof (prove)
goal (4 subgoals):
 1. \<And>args. \<lbrace>?Q6 args\<rbrace> rec_del args \<lbrace>?Q2 args\<rbrace>, \<lbrace>?E2 args\<rbrace>
 2. \<And>args s. (invs and valid_rec_del_call args and (\<lambda>s. \<not> exposed_rdcall args \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s) and emptyable (slot_rdcall args) and (\<lambda>s. case args of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) s \<Longrightarrow> ?Q6 args s
 3. \<And>args rv s. ?Q2 args rv s \<Longrightarrow> emptyable (slot_rdcall args) s
 4. \<And>args e s. ?E2 args e s \<Longrightarrow> True proof (prove)
goal (4 subgoals):
 1. \<And>args s. s \<turnstile> \<lbrace>?Q6 args\<rbrace> rec_del args \<lbrace>?Q2 args\<rbrace>, \<lbrace>?E2 args\<rbrace>
 2. \<And>args s. (invs and valid_rec_del_call args and (\<lambda>s. \<not> exposed_rdcall args \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s) and emptyable (slot_rdcall args) and (\<lambda>s. case args of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) s \<Longrightarrow> ?Q6 args s
 3. \<And>args rv s. ?Q2 args rv s \<Longrightarrow> emptyable (slot_rdcall args) s
 4. \<And>args e s. ?E2 args e s \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>args s. (invs and valid_rec_del_call args and (\<lambda>s. \<not> exposed_rdcall args \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s) and emptyable (slot_rdcall args) and (\<lambda>s. case args of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) s \<Longrightarrow> invs s \<and> valid_rec_del_call args s \<and> (\<not> exposed_rdcall args \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s) \<and> emptyable (slot_rdcall args) s \<and> (case args of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)
 2. \<And>args rv s. invs s \<and> (case args of CTEDeleteCall x bool \<Rightarrow> True | FinaliseSlotCall sl x \<Rightarrow> (fst rv \<or> x \<longrightarrow> cte_wp_at (replaceable s sl NullCap) sl s) \<and> (snd rv \<noteq> NullCap \<longrightarrow> post_cap_delete_pre (snd rv) ((caps_of_state s)(sl \<mapsto> NullCap))) | ReduceZombieCall cap sl x \<Rightarrow> \<not> x \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) sl s) \<and> emptyable (slot_rdcall args) s \<Longrightarrow> emptyable (slot_rdcall args) s
 3. \<And>args e s. invs s \<Longrightarrow> True proof (prove)
goal:
No subgoals!