theory VSpace_C

lemma generic_frame_cap_set_capFMappedAddress_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap \<or>
                cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace>
       Call generic_frame_cap_set_capFMappedAddress_'proc
       \<lbrace> cap_lift \<acute>ret__struct_cap_C
         = generic_frame_cap_set_capFMappedAddress_CL (cap_lift \<^bsup>s\<^esup>cap)  (\<^bsup>s\<^esup>asid ) (\<^bsup>s\<^esup>addr )  \<rbrace>" apply vcg apply (clarsimp simp: generic_frame_cap_set_capFMappedAddress_CL_def) apply (intro conjI impI) by (clarsimp simp: cap_lift_small_frame_cap cap_small_frame_cap_lift_def
                       cap_lift_frame_cap cap_frame_cap_lift_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<or> cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrace> Call generic_frame_cap_set_capFMappedAddress_'proc \<lbrace>cap_lift \<acute>ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (cap_lift \<^bsup>s\<^esup>cap) \<^bsup>s\<^esup>asid \<^bsup>s\<^esup>addr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>asid addr cap. 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 \<Longrightarrow> \<forall>ret__unsigned. ret__unsigned = cap_get_tag cap \<longrightarrow> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) = cap_small_frame_cap \<longrightarrow> 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.capFMappedASIDHigh_CL := (asid >> local.asidLowBits) && mask local.asidHighBits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asidLowBits\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (\<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.capFMappedASIDHigh_CL := (asid >> local.asidLowBits) && mask local.asidHighBits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asidLowBits, cap_small_frame_cap_CL.capFMappedAddress_CL := UCAST(32 \<rightarrow> 32) addr && ~~ mask 12\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> cap_lift ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (cap_lift cap) asid addr))) \<and> (UCAST(32 \<rightarrow> 32 signed) (cap_get_tag cap) \<noteq> cap_small_frame_cap \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> (\<forall>ret__struct_cap_C. cap_frame_cap_lift ret__struct_cap_C = cap_frame_cap_lift cap\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asidLowBits) && mask local.asidHighBits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asidLowBits\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> (\<forall>ret__struct_cap_C. cap_frame_cap_lift ret__struct_cap_C = cap_frame_cap_lift cap\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asidLowBits) && mask local.asidHighBits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asidLowBits, cap_frame_cap_CL.capFMappedAddress_CL := UCAST(32 \<rightarrow> 32) addr && ~~ mask 14\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> cap_lift ret__struct_cap_C = generic_frame_cap_set_capFMappedAddress_CL (cap_lift cap) asid addr))) proof (prove)
goal (1 subgoal):
 1. \<And>asid addr cap. 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 \<Longrightarrow> (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> (\<exists>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.capFMappedASIDHigh_CL := (asid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asid_low_bits\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap) \<longrightarrow> (\<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.capFMappedASIDHigh_CL := (asid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asid_low_bits, cap_small_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 12\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> cap_lift ret__struct_cap_C = (case cap_lift cap of Some Cap_null_cap \<Rightarrow> Some Cap_null_cap | Some (Cap_untyped_cap cap_untyped_cap_CL_ext) \<Rightarrow> Some (Cap_untyped_cap cap_untyped_cap_CL_ext) | Some (Cap_endpoint_cap cap_endpoint_cap_CL_ext) \<Rightarrow> Some (Cap_endpoint_cap cap_endpoint_cap_CL_ext) | Some (Cap_notification_cap cap_notification_cap_CL_ext) \<Rightarrow> Some (Cap_notification_cap cap_notification_cap_CL_ext) | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> Some (Cap_reply_cap cap_reply_cap_CL_ext) | Some (Cap_cnode_cap cap_cnode_cap_CL_ext) \<Rightarrow> Some (Cap_cnode_cap cap_cnode_cap_CL_ext) | Some (Cap_thread_cap cap_thread_cap_CL_ext) \<Rightarrow> Some (Cap_thread_cap cap_thread_cap_CL_ext) | Some (Cap_small_frame_cap c) \<Rightarrow> Some (Cap_small_frame_cap (c\<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, cap_small_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 12\<rparr>)) | Some (Cap_frame_cap c) \<Rightarrow> Some (Cap_frame_cap (c\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asidLowBits) && mask local.asidHighBits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asidLowBits, cap_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 14\<rparr>)) | Some (Cap_asid_pool_cap cap_asid_pool_cap_CL_ext) \<Rightarrow> Some (Cap_asid_pool_cap cap_asid_pool_cap_CL_ext) | Some (Cap_page_table_cap cap_page_table_cap_CL_ext) \<Rightarrow> Some (Cap_page_table_cap cap_page_table_cap_CL_ext) | Some (Cap_page_directory_cap cap_page_directory_cap_CL_ext) \<Rightarrow> Some (Cap_page_directory_cap cap_page_directory_cap_CL_ext) | Some Cap_asid_control_cap \<Rightarrow> Some Cap_asid_control_cap | Some Cap_irq_control_cap \<Rightarrow> Some Cap_irq_control_cap | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) | Some (Cap_zombie_cap cap_zombie_cap_CL_ext) \<Rightarrow> Some (Cap_zombie_cap cap_zombie_cap_CL_ext) | Some Cap_domain_cap \<Rightarrow> Some Cap_domain_cap))) \<and> (cap_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> ((\<exists>ret__struct_cap_C. cap_frame_cap_lift ret__struct_cap_C = cap_frame_cap_lift cap\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asid_low_bits\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_frame_cap) \<longrightarrow> (\<forall>ret__struct_cap_C. cap_frame_cap_lift ret__struct_cap_C = cap_frame_cap_lift cap\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asid_low_bits, cap_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 14\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> cap_lift ret__struct_cap_C = (case cap_lift cap of Some Cap_null_cap \<Rightarrow> Some Cap_null_cap | Some (Cap_untyped_cap cap_untyped_cap_CL_ext) \<Rightarrow> Some (Cap_untyped_cap cap_untyped_cap_CL_ext) | Some (Cap_endpoint_cap cap_endpoint_cap_CL_ext) \<Rightarrow> Some (Cap_endpoint_cap cap_endpoint_cap_CL_ext) | Some (Cap_notification_cap cap_notification_cap_CL_ext) \<Rightarrow> Some (Cap_notification_cap cap_notification_cap_CL_ext) | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> Some (Cap_reply_cap cap_reply_cap_CL_ext) | Some (Cap_cnode_cap cap_cnode_cap_CL_ext) \<Rightarrow> Some (Cap_cnode_cap cap_cnode_cap_CL_ext) | Some (Cap_thread_cap cap_thread_cap_CL_ext) \<Rightarrow> Some (Cap_thread_cap cap_thread_cap_CL_ext) | Some (Cap_small_frame_cap c) \<Rightarrow> Some (Cap_small_frame_cap (c\<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, cap_small_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 12\<rparr>)) | Some (Cap_frame_cap c) \<Rightarrow> Some (Cap_frame_cap (c\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asidLowBits) && mask local.asidHighBits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asidLowBits, cap_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 14\<rparr>)) | Some (Cap_asid_pool_cap cap_asid_pool_cap_CL_ext) \<Rightarrow> Some (Cap_asid_pool_cap cap_asid_pool_cap_CL_ext) | Some (Cap_page_table_cap cap_page_table_cap_CL_ext) \<Rightarrow> Some (Cap_page_table_cap cap_page_table_cap_CL_ext) | Some (Cap_page_directory_cap cap_page_directory_cap_CL_ext) \<Rightarrow> Some (Cap_page_directory_cap cap_page_directory_cap_CL_ext) | Some Cap_asid_control_cap \<Rightarrow> Some Cap_asid_control_cap | Some Cap_irq_control_cap \<Rightarrow> Some Cap_irq_control_cap | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) | Some (Cap_zombie_cap cap_zombie_cap_CL_ext) \<Rightarrow> Some (Cap_zombie_cap cap_zombie_cap_CL_ext) | Some Cap_domain_cap \<Rightarrow> Some Cap_domain_cap)))) proof (prove)
goal (3 subgoals):
 1. \<And>asid addr cap. \<lbrakk>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_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; \<exists>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.capFMappedASIDHigh_CL := (asid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asid_low_bits\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> \<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.capFMappedASIDHigh_CL := (asid >> local.asid_low_bits) && mask local.asid_high_bits, cap_small_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asid_low_bits, cap_small_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 12\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> cap_lift ret__struct_cap_C = (case cap_lift cap of Some Cap_null_cap \<Rightarrow> Some Cap_null_cap | Some (Cap_untyped_cap cap_untyped_cap_CL_ext) \<Rightarrow> Some (Cap_untyped_cap cap_untyped_cap_CL_ext) | Some (Cap_endpoint_cap cap_endpoint_cap_CL_ext) \<Rightarrow> Some (Cap_endpoint_cap cap_endpoint_cap_CL_ext) | Some (Cap_notification_cap cap_notification_cap_CL_ext) \<Rightarrow> Some (Cap_notification_cap cap_notification_cap_CL_ext) | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> Some (Cap_reply_cap cap_reply_cap_CL_ext) | Some (Cap_cnode_cap cap_cnode_cap_CL_ext) \<Rightarrow> Some (Cap_cnode_cap cap_cnode_cap_CL_ext) | Some (Cap_thread_cap cap_thread_cap_CL_ext) \<Rightarrow> Some (Cap_thread_cap cap_thread_cap_CL_ext) | Some (Cap_small_frame_cap c) \<Rightarrow> Some (Cap_small_frame_cap (c\<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, cap_small_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 12\<rparr>)) | Some (Cap_frame_cap c) \<Rightarrow> Some (Cap_frame_cap (c\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asidLowBits) && mask local.asidHighBits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asidLowBits, cap_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 14\<rparr>)) | Some (Cap_asid_pool_cap cap_asid_pool_cap_CL_ext) \<Rightarrow> Some (Cap_asid_pool_cap cap_asid_pool_cap_CL_ext) | Some (Cap_page_table_cap cap_page_table_cap_CL_ext) \<Rightarrow> Some (Cap_page_table_cap cap_page_table_cap_CL_ext) | Some (Cap_page_directory_cap cap_page_directory_cap_CL_ext) \<Rightarrow> Some (Cap_page_directory_cap cap_page_directory_cap_CL_ext) | Some Cap_asid_control_cap \<Rightarrow> Some Cap_asid_control_cap | Some Cap_irq_control_cap \<Rightarrow> Some Cap_irq_control_cap | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) | Some (Cap_zombie_cap cap_zombie_cap_CL_ext) \<Rightarrow> Some (Cap_zombie_cap cap_zombie_cap_CL_ext) | Some Cap_domain_cap \<Rightarrow> Some Cap_domain_cap)
 2. \<And>asid addr cap. \<lbrakk>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_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap\<rbrakk> \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap
 3. \<And>asid addr cap. \<lbrakk>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_get_tag cap \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; \<exists>ret__struct_cap_C. cap_frame_cap_lift ret__struct_cap_C = cap_frame_cap_lift cap\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asid_low_bits\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> \<forall>ret__struct_cap_C. cap_frame_cap_lift ret__struct_cap_C = cap_frame_cap_lift cap\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asid_low_bits) && mask local.asid_high_bits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asid_low_bits, cap_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 14\<rparr> \<and> cap_get_tag ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> cap_lift ret__struct_cap_C = (case cap_lift cap of Some Cap_null_cap \<Rightarrow> Some Cap_null_cap | Some (Cap_untyped_cap cap_untyped_cap_CL_ext) \<Rightarrow> Some (Cap_untyped_cap cap_untyped_cap_CL_ext) | Some (Cap_endpoint_cap cap_endpoint_cap_CL_ext) \<Rightarrow> Some (Cap_endpoint_cap cap_endpoint_cap_CL_ext) | Some (Cap_notification_cap cap_notification_cap_CL_ext) \<Rightarrow> Some (Cap_notification_cap cap_notification_cap_CL_ext) | Some (Cap_reply_cap cap_reply_cap_CL_ext) \<Rightarrow> Some (Cap_reply_cap cap_reply_cap_CL_ext) | Some (Cap_cnode_cap cap_cnode_cap_CL_ext) \<Rightarrow> Some (Cap_cnode_cap cap_cnode_cap_CL_ext) | Some (Cap_thread_cap cap_thread_cap_CL_ext) \<Rightarrow> Some (Cap_thread_cap cap_thread_cap_CL_ext) | Some (Cap_small_frame_cap c) \<Rightarrow> Some (Cap_small_frame_cap (c\<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, cap_small_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 12\<rparr>)) | Some (Cap_frame_cap c) \<Rightarrow> Some (Cap_frame_cap (c\<lparr>cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> local.asidLowBits) && mask local.asidHighBits, cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask local.asidLowBits, cap_frame_cap_CL.capFMappedAddress_CL := addr && ~~ mask 14\<rparr>)) | Some (Cap_asid_pool_cap cap_asid_pool_cap_CL_ext) \<Rightarrow> Some (Cap_asid_pool_cap cap_asid_pool_cap_CL_ext) | Some (Cap_page_table_cap cap_page_table_cap_CL_ext) \<Rightarrow> Some (Cap_page_table_cap cap_page_table_cap_CL_ext) | Some (Cap_page_directory_cap cap_page_directory_cap_CL_ext) \<Rightarrow> Some (Cap_page_directory_cap cap_page_directory_cap_CL_ext) | Some Cap_asid_control_cap \<Rightarrow> Some Cap_asid_control_cap | Some Cap_irq_control_cap \<Rightarrow> Some Cap_irq_control_cap | Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) \<Rightarrow> Some (Cap_irq_handler_cap cap_irq_handler_cap_CL_ext) | Some (Cap_zombie_cap cap_zombie_cap_CL_ext) \<Rightarrow> Some (Cap_zombie_cap cap_zombie_cap_CL_ext) | Some Cap_domain_cap \<Rightarrow> Some Cap_domain_cap)