theory Arch_DP

lemma decode_invocation_asid_pool_assign:
  "\<lbrace> \<lambda>s. (c = AsidPoolCap p base) \<rbrace>
  decode_invocation c ref [(PageDirectoryCap pd is_real sz,pd_ref)]
  (AsidPoolIntent AsidPoolAssignIntent)
  \<lbrace>\<lambda>iv s. \<exists>x. x < 2 ^ asid_low_bits \<and> iv = InvokeAsidPool (Assign (base, x) pd_ref (p, x)) \<rbrace>, -" apply (rule hoare_pre) apply (rule hoare_gen_asmE[where P =" c = AsidPoolCap p base"]) apply (simp add:decode_invocation_def get_asid_pool_intent_def
     decode_asid_pool_invocation_def get_index_def
     throw_opt_def throw_on_none_def) apply (rule validE_validE_R) apply wp apply (clarsimp simp:cap_object_def cap_has_object_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. c = AsidPoolCap p base\<rbrace> decode_invocation c ref [(PageDirectoryCap pd is_real sz, pd_ref)] (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>iv s. \<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) pd_ref (p, x))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> decode_invocation c ref [(PageDirectoryCap pd is_real sz, pd_ref)] (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>iv s. \<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) pd_ref (p, x))\<rbrace>, -
 2. \<And>s. c = AsidPoolCap p base \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. c = AsidPoolCap p base \<Longrightarrow> \<lbrace>?P'3\<rbrace> decode_invocation c ref [(PageDirectoryCap pd is_real sz, pd_ref)] (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>iv s. \<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) pd_ref (p, x))\<rbrace>, -
 2. \<And>s. c = AsidPoolCap p base \<Longrightarrow> (?P'3 and K (c = AsidPoolCap p base)) s proof (prove)
goal (2 subgoals):
 1. c = AsidPoolCap p base \<Longrightarrow> \<lbrace>?P'3\<rbrace> liftME InvokeAsidPool (doE offset <- liftE (select {x. x < 2 ^ asid_low_bits});
returnOk (Assign (base, offset) pd_ref (p, offset))
odE \<sqinter> throw) \<lbrace>\<lambda>iv s. \<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) pd_ref (p, x))\<rbrace>, -
 2. \<And>s. c = AsidPoolCap p base \<Longrightarrow> (?P'3 and K (c = AsidPoolCap p base)) s proof (prove)
goal (2 subgoals):
 1. c = AsidPoolCap p base \<Longrightarrow> \<lbrace>?P'3\<rbrace> liftME InvokeAsidPool (doE offset <- liftE (select {x. x < 2 ^ asid_low_bits});
returnOk (Assign (base, offset) pd_ref (p, offset))
odE \<sqinter> throw) \<lbrace>\<lambda>iv s. \<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) pd_ref (p, x))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. c = AsidPoolCap p base \<Longrightarrow> (?P'3 and K (c = AsidPoolCap p base)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. c = AsidPoolCap p base \<Longrightarrow> ((\<lambda>s. True \<and> ((\<lambda>s. True \<and> True \<and> (\<forall>x\<in>{x. x < 2 ^ asid_low_bits}. ((\<lambda>iv s. \<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) pd_ref (p, x))) \<circ> InvokeAsidPool) (Assign (base, x) pd_ref (p, x)) s)) and (\<lambda>s. True \<and> True)) s) and K (c = AsidPoolCap p base)) s proof (prove)
goal:
No subgoals!