theory CSpace_C

lemma cap_small_frame_cap_set_capFMappedASID_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<^bsup>s\<^esup>cap = scast cap_small_frame_cap\<rbrace>
    Call cap_small_frame_cap_set_capFMappedASID_'proc
   \<lbrace>cap_small_frame_cap_lift \<acute>ret__struct_cap_C
         = cap_small_frame_cap_lift \<^bsup>s\<^esup>cap
               \<lparr> cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (\<^bsup>s\<^esup>asid >> asidLowBits) && mask asidHighBits,
                 cap_small_frame_cap_CL.capFMappedASIDLow_CL  := \<^bsup>s\<^esup>asid && mask asidLowBits \<rparr>
        \<and> cap_get_tag \<acute>ret__struct_cap_C = scast cap_small_frame_cap\<rbrace>" apply vcg by (clarsimp simp: Kernel_C.asidLowBits_def word_sle_def
                     Kernel_C.asidHighBits_def asid_low_bits_def asid_high_bits_def mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<^bsup>s\<^esup>cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrace> Call cap_small_frame_cap_set_capFMappedASID_'proc \<lbrace>cap_small_frame_cap_lift \<acute>ret__struct_cap_C = cap_small_frame_cap_lift \<^bsup>s\<^esup>cap\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (\<^bsup>s\<^esup>asid >> local.asidLowBits) && mask local.asidHighBits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := \<^bsup>s\<^esup>asid && mask local.asidLowBits\<rparr> \<and> cap_get_tag \<acute>ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>asid cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<and> Kernel_C.asidLowBits <s 0x20 \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<and> (\<forall>ret__struct_cap_C. cap_small_frame_cap_lift ret__struct_cap_C = cap_small_frame_cap_lift cap\<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL := UCAST(32 \<rightarrow> 32) (asid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> 0 \<le>s Kernel_C.asidHighBits \<and> Kernel_C.asidHighBits <s 0x20 \<and> 0 \<le>s Kernel_C.asidLowBits \<and> Kernel_C.asidLowBits <s 0x20 \<and> (\<forall>ret__struct_cap_C. cap_small_frame_cap_lift ret__struct_cap_C = cap_small_frame_cap_lift cap\<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL := UCAST(32 \<rightarrow> 32) (asid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, cap_small_frame_cap_CL.capFMappedASIDHigh_CL := UCAST(32 \<rightarrow> 32) ((asid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> cap_small_frame_cap_lift cap\<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL := UCAST(32 \<rightarrow> 32) (asid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, cap_small_frame_cap_CL.capFMappedASIDHigh_CL := UCAST(32 \<rightarrow> 32) ((asid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7\<rparr> = cap_small_frame_cap_lift cap\<lparr>cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asidLowBits) && mask local.asidHighBits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asidLowBits\<rparr>))