theory Fastpath_Equiv

lemma cteDeleteOne_replycap_rewrite:
  "monadic_rewrite True False
     (cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot)
     (cteDeleteOne slot)
     (emptySlot slot NullCap)" supply isFinalCapability_inv[wp] empty_fail_isFinalCapability[wp]  (* FIXME *)
   apply (simp add: cteDeleteOne_def) apply (rule monadic_rewrite_symb_exec_l) apply (rule_tac P="cteCap cte \<noteq> NullCap \<and> isReplyCap (cteCap cte)
                        \<and> \<not> isEndpointCap (cteCap cte)
                        \<and> \<not> isNotificationCap (cteCap cte)"
              in monadic_rewrite_gen_asm) apply (simp add: finaliseCapTrue_standin_def capRemovable_def) apply monadic_rewrite_symb_exec_l apply (rule monadic_rewrite_refl) apply (wpsimp wp: getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) (cteDeleteOne slot) (emptySlot slot capability.NullCap) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) (cteDeleteOne slot) (emptySlot slot capability.NullCap) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) (cteDeleteOne slot) (emptySlot slot capability.NullCap) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot) (do cte <- getCTE slot;
unless (cteCap cte = capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)
od) (emptySlot slot capability.NullCap) proof (prove)
goal (4 subgoals):
 1. \<And>cte. monadic_rewrite True False (?Q cte) (unless (cteCap cte = capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)) (emptySlot slot capability.NullCap)
 2. \<And>P. \<lbrace>P\<rbrace> getCTE slot \<lbrace>\<lambda>_. P\<rbrace>
 3. empty_fail (getCTE slot)
 4. \<lbrace>cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot\<rbrace> getCTE slot \<lbrace>?Q\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cte. cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte) \<Longrightarrow> monadic_rewrite True False (?Q5 cte) (unless (cteCap cte = capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder slot \<and> info = capability.NullCap);
emptySlot slot capability.NullCap
od)) (emptySlot slot capability.NullCap)
 2. \<And>P. \<lbrace>P\<rbrace> getCTE slot \<lbrace>\<lambda>_. P\<rbrace>
 3. empty_fail (getCTE slot)
 4. \<lbrace>cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte. (\<lambda>_. cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte)) and ?Q5 cte\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cte. cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte) \<Longrightarrow> monadic_rewrite True False (?Q5 cte) (do final <- isFinalCapability cte;
emptySlot slot capability.NullCap
od) (emptySlot slot capability.NullCap)
 2. \<And>P. \<lbrace>P\<rbrace> getCTE slot \<lbrace>\<lambda>_. P\<rbrace>
 3. empty_fail (getCTE slot)
 4. \<lbrace>cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte. (\<lambda>_. cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte)) and ?Q5 cte\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>cte final. cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte) \<Longrightarrow> monadic_rewrite True False (?Q17 cte final) (emptySlot slot capability.NullCap) (emptySlot slot capability.NullCap)
 2. \<And>cte. cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte) \<Longrightarrow> \<lbrace>?Q5 cte\<rbrace> isFinalCapability cte \<lbrace>?Q17 cte\<rbrace>
 3. \<And>P. \<lbrace>P\<rbrace> getCTE slot \<lbrace>\<lambda>_. P\<rbrace>
 4. empty_fail (getCTE slot)
 5. \<lbrace>cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte. (\<lambda>_. cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte)) and ?Q5 cte\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cte. cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte) \<Longrightarrow> \<lbrace>?Q5 cte\<rbrace> isFinalCapability cte \<lbrace>\<lambda>final _. True\<rbrace>
 2. \<And>P. \<lbrace>P\<rbrace> getCTE slot \<lbrace>\<lambda>_. P\<rbrace>
 3. empty_fail (getCTE slot)
 4. \<lbrace>cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot\<rbrace> getCTE slot \<lbrace>\<lambda>cte. (\<lambda>_. cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte)) and ?Q5 cte\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>cte_wp_at' (\<lambda>cte. isReplyCap (cteCap cte)) slot s; cte_wp_at' ((=) cte) slot s\<rbrakk> \<Longrightarrow> cteCap cte \<noteq> capability.NullCap \<and> isReplyCap (cteCap cte) \<and> \<not> isEndpointCap (cteCap cte) \<and> \<not> isNotificationCap (cteCap cte) proof (prove)
goal:
No subgoals!