theory FinalCaps

lemma set_simple_ko_silc_inv[wp]:
  "\<lbrace>silc_inv aag st\<rbrace>
   set_simple_ko f ptr ep
   \<lbrace>\<lambda> _. silc_inv aag st\<rbrace>" unfolding set_simple_ko_def apply (rule silc_inv_pres) apply (wpsimp wp: set_object_wp_strong get_object_wp simp: obj_at_def) apply (fastforce simp: silc_inv_def obj_at_def is_cap_table_def) apply (wpsimp wp: set_object_wp get_object_wp) apply (wpsimp wp: set_object_wp_strong get_object_wp simp: obj_at_def) apply (case_tac "ptr = fst (a,b)") apply (fastforce elim: cte_wp_atE simp: obj_at_def) apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> set_simple_ko f ptr ep \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptra P. \<lbrace>silc_inv aag st and (\<lambda>s. P (kheap s ptra)) and K (pasObjectAbs aag ptra = SilcLabel)\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_ s. P (kheap s ptra)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P s ko. \<lbrakk>silc_inv aag st s; P (Some ko); pasObjectAbs aag ptr = SilcLabel; kheap s ptr = Some ko\<rbrakk> \<Longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = AEndpoint \<longrightarrow> P (Some (f ep))) \<and> (a_type ko = ANTFN \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = ANTFN \<longrightarrow> P (Some (f ep)))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do obj <- get_object ptr;
assert (is_simple_type obj);
assert (partial_inv f obj \<noteq> None);
set_object ptr (f ep)
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P a b s ko. \<lbrakk>\<not> cte_wp_at P (a, b) s; kheap s ptr = Some ko\<rbrakk> \<Longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = AEndpoint \<longrightarrow> \<not> cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f ep)\<rparr>)) \<and> (a_type ko = ANTFN \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = ANTFN \<longrightarrow> \<not> cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f ep)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P a b s ko. \<lbrakk>\<not> cte_wp_at P (a, b) s; kheap s ptr = Some ko; ptr = fst (a, b)\<rbrakk> \<Longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = AEndpoint \<longrightarrow> \<not> cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f ep)\<rparr>)) \<and> (a_type ko = ANTFN \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = ANTFN \<longrightarrow> \<not> cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f ep)\<rparr>))
 2. \<And>P a b s ko. \<lbrakk>\<not> cte_wp_at P (a, b) s; kheap s ptr = Some ko; ptr \<noteq> fst (a, b)\<rbrakk> \<Longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = AEndpoint \<longrightarrow> \<not> cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f ep)\<rparr>)) \<and> (a_type ko = ANTFN \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = ANTFN \<longrightarrow> \<not> cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f ep)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>P a b s ko. \<lbrakk>\<not> cte_wp_at P (a, b) s; kheap s ptr = Some ko; ptr \<noteq> fst (a, b)\<rbrakk> \<Longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = AEndpoint \<longrightarrow> \<not> cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f ep)\<rparr>)) \<and> (a_type ko = ANTFN \<longrightarrow> (\<exists>y. partial_inv f ko = Some y) \<longrightarrow> a_type (f ep) = ANTFN \<longrightarrow> \<not> cte_wp_at P (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> f ep)\<rparr>)) proof (prove)
goal:
No subgoals!