theory VSpace_C

lemma generic_frame_cap_ptr_set_capFMappedAddress_spec:
  "\<forall>s cte_slot.
    \<Gamma> \<turnstile> \<lbrace>s. (\<exists> cap. cslift s \<^bsup>s\<^esup>cap_ptr = Some cap \<and> cap_lift cap \<noteq> None \<and>
                     (cap_get_tag cap = scast cap_small_frame_cap \<or>
                      cap_get_tag cap = scast cap_frame_cap)) \<and>
               \<acute>cap_ptr = cap_Ptr &(cte_slot\<rightarrow>[''cap_C'']) \<and>
               cslift s cte_slot \<noteq> None\<rbrace>
       Call generic_frame_cap_ptr_set_capFMappedAddress_'proc
       {t. (\<exists>cte' cap'.
           generic_frame_cap_set_capFMappedAddress_CL (cap_lift (the (cslift s \<^bsup>s\<^esup>cap_ptr))) \<^bsup>s\<^esup>asid \<^bsup>s\<^esup>addr = Some cap' \<and>
           cte_lift cte' = option_map (cap_CL_update (K cap')) (cte_lift (the (cslift s cte_slot))) \<and>
           t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte')
               (t_hrs_' (globals s)))}" apply vcg apply (clarsimp simp: typ_heap_simps) apply (subgoal_tac "cap_lift ret__struct_cap_C \<noteq> None") prefer 2 apply (clarsimp simp: generic_frame_cap_set_capFMappedAddress_CL_def split: cap_CL.splits) apply (clarsimp simp: typ_heap_simps) apply (rule_tac x="cte_C.cap_C_update (\<lambda>_. ret__struct_cap_C) y" in exI) apply (case_tac y) apply (clarsimp simp: cte_lift_def typ_heap_simps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s cte_slot. \<Gamma>\<turnstile> \<lbrace>s. (\<exists>cap. cslift s \<^bsup>s\<^esup>cap_ptr = Some cap \<and> cap_lift cap \<noteq> None \<and> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap)) \<and> \<acute>cap_ptr = cap_Ptr &(cte_slot\<rightarrow>[''cap_C'']) \<and> cslift s cte_slot \<noteq> None\<rbrace> Call generic_frame_cap_ptr_set_capFMappedAddress_'proc \<lbrace>\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (cap_lift (the (cslift s \<^bsup>s\<^esup>cap_ptr))) \<^bsup>s\<^esup>asid \<^bsup>s\<^esup>addr = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (K cap')) (cte_lift (the (cslift s cte_slot))) \<and> \<acute>t_hrs = hrs_mem_update (heap_update cte_slot cte') \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte_slot t_hrs cap_ptr asid addr. \<lbrakk>\<exists>cap. clift t_hrs cap_ptr = Some cap \<and> cap_lift cap \<noteq> None \<and> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap); cap_ptr = cap_Ptr &(cte_slot\<rightarrow>[''cap_C'']); clift t_hrs cte_slot \<noteq> None\<rbrakk> \<Longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t cap_ptr \<and> (cap_get_tag (h_val (hrs_mem t_hrs) cap_ptr) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (h_val (hrs_mem t_hrs) cap_ptr) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) \<and> (\<forall>ret__struct_cap_C. cap_lift ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (cap_lift (h_val (hrs_mem t_hrs) cap_ptr)) asid addr \<longrightarrow> hrs_htd t_hrs \<Turnstile>\<^sub>t cap_ptr \<and> (\<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (cap_lift (the (clift t_hrs cap_ptr))) asid addr = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (K cap')) (cte_lift (the (clift t_hrs cte_slot))) \<and> hrs_mem_update (heap_update cap_ptr ret__struct_cap_C) t_hrs = hrs_mem_update (heap_update cte_slot cte') t_hrs)) proof (prove)
goal (1 subgoal):
 1. \<And>cte_slot a b asid addr y ya ret__struct_cap_C. \<lbrakk>clift (a, b) cte_slot = Some y; cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C y) = Some ya; cap_lift ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr\<rbrakk> \<Longrightarrow> \<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift y) \<and> hrs_mem_update (heap_update (cap_Ptr &(cte_slot\<rightarrow>[''cap_C''])) ret__struct_cap_C) (a, b) = hrs_mem_update (heap_update cte_slot cte') (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>cte_slot a b asid addr y ya ret__struct_cap_C. \<lbrakk>clift (a, b) cte_slot = Some y; cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C y) = Some ya; cap_lift ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr; cap_lift ret__struct_cap_C \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift y) \<and> hrs_mem_update (heap_update (cap_Ptr &(cte_slot\<rightarrow>[''cap_C''])) ret__struct_cap_C) (a, b) = hrs_mem_update (heap_update cte_slot cte') (a, b)
 2. \<And>cte_slot a b asid addr y ya ret__struct_cap_C. \<lbrakk>clift (a, b) cte_slot = Some y; cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C y) = Some ya; cap_lift ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr\<rbrakk> \<Longrightarrow> cap_lift ret__struct_cap_C \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>cte_slot a b asid addr y ya ret__struct_cap_C. \<lbrakk>clift (a, b) cte_slot = Some y; cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C y) = Some ya; cap_lift ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr\<rbrakk> \<Longrightarrow> cap_lift ret__struct_cap_C \<noteq> None
 2. \<And>cte_slot a b asid addr y ya ret__struct_cap_C. \<lbrakk>clift (a, b) cte_slot = Some y; cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C y) = Some ya; cap_lift ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr; cap_lift ret__struct_cap_C \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift y) \<and> hrs_mem_update (heap_update (cap_Ptr &(cte_slot\<rightarrow>[''cap_C''])) ret__struct_cap_C) (a, b) = hrs_mem_update (heap_update cte_slot cte') (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>cte_slot a b asid addr y ya ret__struct_cap_C. \<lbrakk>clift (a, b) cte_slot = Some y; cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C y) = Some ya; cap_lift ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr; cap_lift ret__struct_cap_C \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>cte' cap'. generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr = Some cap' \<and> cte_lift cte' = map_option (cap_CL_update (\<lambda>y. cap')) (cte_lift y) \<and> hrs_mem_update (heap_update (cap_Ptr &(cte_slot\<rightarrow>[''cap_C''])) ret__struct_cap_C) (a, b) = hrs_mem_update (heap_update cte_slot cte') (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>cte_slot a b asid addr y ya ret__struct_cap_C yb. \<lbrakk>clift (a, b) cte_slot = Some y; cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C y) = Some ya; cap_lift ret__struct_cap_C = Some yb; generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr = Some yb\<rbrakk> \<Longrightarrow> \<exists>cte'. cte_lift cte' = map_option (cap_CL_update (\<lambda>y. yb)) (cte_lift y) \<and> hrs_mem_update (heap_update (cap_Ptr &(cte_slot\<rightarrow>[''cap_C''])) ret__struct_cap_C) (a, b) = hrs_mem_update (heap_update cte_slot cte') (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>cte_slot a b asid addr y ya ret__struct_cap_C yb. \<lbrakk>clift (a, b) cte_slot = Some y; cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C y) = Some ya; cap_lift ret__struct_cap_C = Some yb; generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr = Some yb\<rbrakk> \<Longrightarrow> cte_lift (cte_C.cap_C_update (\<lambda>_. ret__struct_cap_C) y) = map_option (cap_CL_update (\<lambda>y. yb)) (cte_lift y) \<and> hrs_mem_update (heap_update (cap_Ptr &(cte_slot\<rightarrow>[''cap_C''])) ret__struct_cap_C) (a, b) = hrs_mem_update (heap_update cte_slot (cte_C.cap_C_update (\<lambda>_. ret__struct_cap_C) y)) (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>cte_slot a b asid addr y ya ret__struct_cap_C yb x1 x2. \<lbrakk>clift (a, b) cte_slot = Some y; cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag (cte_C.cap_C y) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap; cap_lift (cte_C.cap_C y) = Some ya; cap_lift ret__struct_cap_C = Some yb; generic_frame_cap_set_capFMappedAddress_CL (Some ya) asid addr = Some yb; y = cte_C x1 x2\<rbrakk> \<Longrightarrow> cte_lift (cte_C.cap_C_update (\<lambda>_. ret__struct_cap_C) y) = map_option (cap_CL_update (\<lambda>y. yb)) (cte_lift y) \<and> hrs_mem_update (heap_update (cap_Ptr &(cte_slot\<rightarrow>[''cap_C''])) ret__struct_cap_C) (a, b) = hrs_mem_update (heap_update cte_slot (cte_C.cap_C_update (\<lambda>_. ret__struct_cap_C) y)) (a, b) proof (prove)
goal:
No subgoals!