theory Fastpath_Equiv

lemma clearUntypedFreeIndex_simple_rewrite:
  "monadic_rewrite True False
    (cte_wp_at' (Not o isUntypedCap o cteCap) slot)
        (clearUntypedFreeIndex slot) (return ())" apply (simp add: clearUntypedFreeIndex_def getSlotCap_def) apply (rule monadic_rewrite_name_pre) apply (clarsimp simp: cte_wp_at_ctes_of) apply (monadic_rewrite_symb_exec_l_known cte) apply (simp split: capability.split, strengthen monadic_rewrite_refl) apply (wpsimp wp: getCTE_wp' simp: cte_wp_at_ctes_of)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot) (clearUntypedFreeIndex slot) (return ()) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot) (do cte <- getCTE slot;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()
od) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (Not \<circ> isUntypedCap \<circ> cteCap) slot s \<Longrightarrow> monadic_rewrite True False ((=) s) (do cte <- getCTE slot;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()
od) (return ()) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>ctes_of s slot = Some cte; \<not> isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> monadic_rewrite True False ((=) s) (do cte <- getCTE slot;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()
od) (return ()) proof (prove)
goal (3 subgoals):
 1. \<And>s cte. \<lbrakk>ctes_of s slot = Some cte; \<not> isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q8 s cte) (case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()) (return ())
 2. \<And>s cte. \<lbrakk>ctes_of s slot = Some cte; \<not> isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?P8 s cte\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 3. \<And>s cte sa. \<lbrakk>ctes_of s slot = Some cte; \<not> isUntypedCap (cteCap cte); s = sa\<rbrakk> \<Longrightarrow> (?P8 s cte and ?Q8 s cte) sa proof (prove)
goal (3 subgoals):
 1. \<And>s cte. \<lbrakk>ctes_of s slot = Some cte; \<not> isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> ((\<exists>x1. cteCap cte = capability.ThreadCap x1) \<longrightarrow> True) \<and> (cteCap cte = capability.NullCap \<longrightarrow> True) \<and> ((\<exists>x31 x32 x33 x34. cteCap cte = capability.NotificationCap x31 x32 x33 x34) \<longrightarrow> True) \<and> ((\<exists>x4. cteCap cte = capability.IRQHandlerCap x4) \<longrightarrow> True) \<and> ((\<exists>x51 x52 x53 x54 x55 x56. cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56) \<longrightarrow> True) \<and> (cteCap cte = capability.DomainCap \<longrightarrow> True) \<and> ((\<exists>x71 x72 x73. cteCap cte = capability.Zombie x71 x72 x73) \<longrightarrow> True) \<and> ((\<exists>x8. cteCap cte = capability.ArchObjectCap x8) \<longrightarrow> True) \<and> ((\<exists>x91 x92 x93. cteCap cte = capability.ReplyCap x91 x92 x93) \<longrightarrow> True) \<and> (\<forall>x101 x102 x103. (\<exists>x104. cteCap cte = capability.UntypedCap x101 x102 x103 x104) \<longrightarrow> monadic_rewrite True False (\<lambda>_. True) (updateTrackedFreeIndex slot (max_free_index x103)) (return ())) \<and> ((\<exists>x111 x112 x113 x114. cteCap cte = capability.CNodeCap x111 x112 x113 x114) \<longrightarrow> True) \<and> (cteCap cte = capability.IRQControlCap \<longrightarrow> True)
 2. \<And>s cte. \<lbrakk>ctes_of s slot = Some cte; \<not> isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> \<lbrace>?P8 s cte\<rbrace> getCTE slot \<lbrace>\<lambda>rv' _. rv' = cte\<rbrace>
 3. \<And>s cte sa. \<lbrakk>ctes_of s slot = Some cte; \<not> isUntypedCap (cteCap cte); s = sa\<rbrakk> \<Longrightarrow> (?P8 s cte and (\<lambda>_. True)) sa proof (prove)
goal:
No subgoals!