theory Ipc_R

lemma cteInsert_weak_cte_wp_at2:
  assumes weak:"\<And>c cap. P (maskedAsFull c cap) = P c"
  shows
    "\<lbrace>\<lambda>s. if p = dest then P cap else cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace>
     cteInsert cap src dest
     \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>" 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 weak) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if p = dest then P cap else cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
 2. \<And>s. if p = dest then P cap else cte_wp_at' (\<lambda>c. P (cteCap c)) p s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
 2. \<And>s. if p = dest then P cap else cte_wp_at' (\<lambda>c. P (cteCap c)) p 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>uu. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
 2. \<And>s. if p = dest then P cap else cte_wp_at' (\<lambda>c. P (cteCap c)) p s \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. if p = dest then P cap else cte_wp_at' (\<lambda>c. P (cteCap c)) p s \<Longrightarrow> 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 = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) src and (\<lambda>s. cte_wp_at' ((\<lambda>c. P (cteCap c)) \<circ> cteCap_update (K cap)) p s \<and> p \<noteq> src \<or> p = src \<and> cte_wp_at' (\<lambda>c. ((\<lambda>c. P (cteCap c)) \<circ> cteCap_update (K cap)) (CTE (maskedAsFull (cteCap c) cap) (cteMDBNode c))) src s)) s) \<and> (dest \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> (cte_wp_at' ((=) cte) src and (\<lambda>s. cte_wp_at' (\<lambda>c. P (cteCap c)) p s \<and> p \<noteq> src \<or> p = src \<and> cte_wp_at' (\<lambda>c. P (cteCap (CTE (maskedAsFull (cteCap c) cap) (cteMDBNode c)))) src s)) s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>if p = dest then P cap else \<exists>cte. ctes_of s p = Some cte \<and> P (cteCap cte); ctes_of s src = Some cte; ctes_of s dest = Some ctea\<rbrakk> \<Longrightarrow> (dest = p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> (\<exists>cte. ctes_of s p = Some cte) \<and> p \<noteq> src \<or> p = src) \<and> (dest \<noteq> p \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> p = src \<longrightarrow> P (cteCap cte)) proof (prove)
goal:
No subgoals!