theory Ipc_R

lemma cteInsert_cte_cap_to':
  "\<lbrace>ex_cte_cap_to' p and cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) dest\<rbrace>
   cteInsert cap src dest
   \<lbrace>\<lambda>rv. ex_cte_cap_to' p\<rbrace>" apply (simp add: ex_cte_cap_to'_def) apply (rule hoare_pre) apply (rule hoare_use_eq_irq_node' [OF cteInsert_ksInterruptState]) apply (clarsimp simp:cteInsert_def) apply (wp hoare_vcg_ex_lift  updateMDB_weak_cte_wp_at updateCap_cte_wp_at_cases
      setUntypedCapAsFull_cte_wp_at getCTE_wp hoare_weak_lift_imp) apply (clarsimp simp:cte_wp_at_ctes_of) apply (rule_tac x = "cref" in exI) apply (rule conjI) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True) p and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) f) cref s\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest) s \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) f) cref s\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest) s \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) and cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest) s \<Longrightarrow> \<exists>x. cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (dest = x \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) src and (\<lambda>sa. cte_wp_at' ((\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) \<circ> cteCap_update (K cap)) x sa \<and> x \<noteq> src \<or> x = src \<and> cte_wp_at' (\<lambda>c. ((\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) \<circ> cteCap_update (K cap)) (CTE (maskedAsFull (cteCap c) cap) (cteMDBNode c))) src sa)) s) \<and> (dest \<noteq> x \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) src and (\<lambda>sa. cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap c) (irq_node' s)) x sa \<and> x \<noteq> src \<or> x = src \<and> cte_wp_at' (\<lambda>c. p \<in> cte_refs' (cteCap (CTE (maskedAsFull (cteCap c) cap) (cteMDBNode c))) (irq_node' s)) src sa)) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; p \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb\<rbrakk> \<Longrightarrow> \<exists>x. (dest = x \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> p \<in> cte_refs' cap (irq_node' s) \<and> x \<noteq> src \<or> x = src \<and> p \<in> cte_refs' cap (irq_node' s)) \<and> (dest \<noteq> x \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte \<and> p \<in> cte_refs' (cteCap cte) (irq_node' s)) \<and> x \<noteq> src \<or> x = src \<and> p \<in> cte_refs' (cteCap cteb) (irq_node' s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; p \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb\<rbrakk> \<Longrightarrow> (dest = cref \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte) \<and> p \<in> cte_refs' cap (irq_node' s) \<and> cref \<noteq> src \<or> cref = src \<and> p \<in> cte_refs' cap (irq_node' s)) \<and> (dest \<noteq> cref \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> p \<in> cte_refs' (cteCap cte) (irq_node' s)) \<and> cref \<noteq> src \<or> cref = src \<and> p \<in> cte_refs' (cteCap cteb) (irq_node' s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; p \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb\<rbrakk> \<Longrightarrow> dest = cref \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte) \<and> p \<in> cte_refs' cap (irq_node' s) \<and> cref \<noteq> src \<or> cref = src \<and> p \<in> cte_refs' cap (irq_node' s)
 2. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s dest = Some cte; cteCap cte = capability.NullCap; ctes_of s cref = Some ctea; p \<in> cte_refs' (cteCap ctea) (irq_node' s); ctes_of s src = Some cteb\<rbrakk> \<Longrightarrow> dest \<noteq> cref \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte \<and> p \<in> cte_refs' (cteCap cte) (irq_node' s)) \<and> cref \<noteq> src \<or> cref = src \<and> p \<in> cte_refs' (cteCap cteb) (irq_node' s) proof (prove)
goal:
No subgoals!