theory Ipc_DR

lemma set_endpoint_valid_irq_node[wp]:
  "\<lbrace>valid_irq_node and ep_at w\<rbrace> set_endpoint w ep \<lbrace>\<lambda>rv. valid_irq_node\<rbrace>" apply (clarsimp simp:valid_irq_node_def) apply wp apply (simp add:set_simple_ko_def) apply (wp hoare_vcg_all_lift) apply (rule_tac Q="\<lambda>s. \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s \<and> ep_at w s" in hoare_vcg_precond_imp) apply (clarsimp simp: set_object_def get_object_def in_monad get_def put_def bind_def
                             return_def valid_def obj_at_def) apply (drule_tac x = irq in spec) apply (clarsimp simp: is_cap_table_def is_ep_def) apply (simp split: Structures_A.kernel_object.splits) apply wp+ apply (clarsimp simp: get_object_def|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_node and ep_at w\<rbrace> set_endpoint w ep \<lbrace>\<lambda>rv. valid_irq_node\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w\<rbrace> set_endpoint w ep \<lbrace>\<lambda>rv s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'1\<rbrace> set_endpoint w ep \<lbrace>\<lambda>rv s. \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrace>
 2. \<And>s. ((\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w) s \<Longrightarrow> inj (interrupt_irq_node s) \<and> ?P'1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'1\<rbrace> do obj <- KHeap_A.get_object w;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. kernel_object.Endpoint y = obj);
KHeap_A.set_object w (kernel_object.Endpoint ep)
od \<lbrace>\<lambda>rv s. \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrace>
 2. \<And>s. ((\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w) s \<Longrightarrow> inj (interrupt_irq_node s) \<and> ?P'1 s proof (prove)
goal (5 subgoals):
 1. \<And>irq obj y ya. \<lbrace>?B8 irq obj y ya\<rbrace> KHeap_A.set_object w (kernel_object.Endpoint ep) \<lbrace>\<lambda>rv s. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrace>
 2. \<And>irq obj y. \<lbrace>?B7 irq obj y\<rbrace> assert (\<exists>y. kernel_object.Endpoint y = obj) \<lbrace>?B8 irq obj y\<rbrace>
 3. \<And>irq obj. \<lbrace>?B6 irq obj\<rbrace> assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN) \<lbrace>?B7 irq obj\<rbrace>
 4. \<And>irq. \<lbrace>?P5 irq\<rbrace> KHeap_A.get_object w \<lbrace>?B6 irq\<rbrace>
 5. \<And>s. ((\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w) s \<Longrightarrow> inj (interrupt_irq_node s) \<and> (\<forall>x. ?P5 x s) proof (prove)
goal (6 subgoals):
 1. \<And>irq obj y ya. \<lbrace>\<lambda>s. \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s \<and> ep_at w s\<rbrace> KHeap_A.set_object w (kernel_object.Endpoint ep) \<lbrace>\<lambda>rv s. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrace>
 2. \<And>irq obj y ya s. ?B8 irq obj y ya s \<Longrightarrow> \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s \<and> ep_at w s
 3. \<And>irq obj y. \<lbrace>?B7 irq obj y\<rbrace> assert (\<exists>y. kernel_object.Endpoint y = obj) \<lbrace>?B8 irq obj y\<rbrace>
 4. \<And>irq obj. \<lbrace>?B6 irq obj\<rbrace> assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN) \<lbrace>?B7 irq obj\<rbrace>
 5. \<And>irq. \<lbrace>?P5 irq\<rbrace> KHeap_A.get_object w \<lbrace>?B6 irq\<rbrace>
 6. \<And>s. ((\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w) s \<Longrightarrow> inj (interrupt_irq_node s) \<and> (\<forall>x. ?P5 x s) proof (prove)
goal (6 subgoals):
 1. \<And>irq s epa. \<lbrakk>\<forall>irq. \<exists>ko. kheap s (interrupt_irq_node s irq) = Some ko \<and> is_cap_table 0 ko; kheap s (interrupt_irq_node s irq) = Some (kernel_object.Endpoint epa); is_ep (kernel_object.Endpoint epa); w = interrupt_irq_node s irq\<rbrakk> \<Longrightarrow> is_cap_table 0 (kernel_object.Endpoint ep)
 2. \<And>irq obj y ya s. ?B8 irq obj y ya s \<Longrightarrow> \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s \<and> ep_at w s
 3. \<And>irq obj y. \<lbrace>?B7 irq obj y\<rbrace> assert (\<exists>y. kernel_object.Endpoint y = obj) \<lbrace>?B8 irq obj y\<rbrace>
 4. \<And>irq obj. \<lbrace>?B6 irq obj\<rbrace> assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN) \<lbrace>?B7 irq obj\<rbrace>
 5. \<And>irq. \<lbrace>?P5 irq\<rbrace> KHeap_A.get_object w \<lbrace>?B6 irq\<rbrace>
 6. \<And>s. ((\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w) s \<Longrightarrow> inj (interrupt_irq_node s) \<and> (\<forall>x. ?P5 x s) proof (prove)
goal (6 subgoals):
 1. \<And>irq s epa. \<lbrakk>kheap s (interrupt_irq_node s irq) = Some (kernel_object.Endpoint epa); is_ep (kernel_object.Endpoint epa); w = interrupt_irq_node s irq; \<exists>ko. kheap s (interrupt_irq_node s irq) = Some ko \<and> is_cap_table 0 ko\<rbrakk> \<Longrightarrow> is_cap_table 0 (kernel_object.Endpoint ep)
 2. \<And>irq obj y ya s. ?B8 irq obj y ya s \<Longrightarrow> \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s \<and> ep_at w s
 3. \<And>irq obj y. \<lbrace>?B7 irq obj y\<rbrace> assert (\<exists>y. kernel_object.Endpoint y = obj) \<lbrace>?B8 irq obj y\<rbrace>
 4. \<And>irq obj. \<lbrace>?B6 irq obj\<rbrace> assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN) \<lbrace>?B7 irq obj\<rbrace>
 5. \<And>irq. \<lbrace>?P5 irq\<rbrace> KHeap_A.get_object w \<lbrace>?B6 irq\<rbrace>
 6. \<And>s. ((\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w) s \<Longrightarrow> inj (interrupt_irq_node s) \<and> (\<forall>x. ?P5 x s) proof (prove)
goal (5 subgoals):
 1. \<And>irq obj y ya s. ?B8 irq obj y ya s \<Longrightarrow> \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s \<and> ep_at w s
 2. \<And>irq obj y. \<lbrace>?B7 irq obj y\<rbrace> assert (\<exists>y. kernel_object.Endpoint y = obj) \<lbrace>?B8 irq obj y\<rbrace>
 3. \<And>irq obj. \<lbrace>?B6 irq obj\<rbrace> assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN) \<lbrace>?B7 irq obj\<rbrace>
 4. \<And>irq. \<lbrace>?P5 irq\<rbrace> KHeap_A.get_object w \<lbrace>?B6 irq\<rbrace>
 5. \<And>s. ((\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w) s \<Longrightarrow> inj (interrupt_irq_node s) \<and> (\<forall>x. ?P5 x s) proof (prove)
goal (4 subgoals):
 1. \<And>irq obj y. \<lbrace>?B7 irq obj y\<rbrace> assert (\<exists>y. kernel_object.Endpoint y = obj) \<lbrace>\<lambda>a b. (\<forall>irq. cap_table_at 0 (interrupt_irq_node b irq) b) \<and> ep_at w b\<rbrace>
 2. \<And>irq obj. \<lbrace>?B6 irq obj\<rbrace> assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN) \<lbrace>?B7 irq obj\<rbrace>
 3. \<And>irq. \<lbrace>?P5 irq\<rbrace> KHeap_A.get_object w \<lbrace>?B6 irq\<rbrace>
 4. \<And>s. ((\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w) s \<Longrightarrow> inj (interrupt_irq_node s) \<and> (\<forall>x. ?P5 x s) proof (prove)
goal (2 subgoals):
 1. \<And>irq. \<lbrace>?P5 irq\<rbrace> KHeap_A.get_object w \<lbrace>\<lambda>obj s. a_type obj = AEndpoint \<or> a_type obj = ANTFN \<longrightarrow> (\<exists>y. kernel_object.Endpoint y = obj) \<longrightarrow> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s) \<and> ep_at w s\<rbrace>
 2. \<And>s. ((\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s)) and ep_at w) s \<Longrightarrow> inj (interrupt_irq_node s) \<and> (\<forall>x. ?P5 x s) proof (prove)
goal:
No subgoals!