theory structures_proofs

lemma (in kernel_all_substitute) cap_page_table_cap_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_cap_C :== PROC cap_page_table_cap_new(\<acute>capPTIsMapped, \<acute>capPTMappedASID, \<acute>capPTMappedAddress, \<acute>capPTBasePtr)
       \<lbrace>cap_page_table_cap_lift \<acute>ret__struct_cap_C = \<lparr>
          cap_page_table_cap_CL.capPTIsMapped_CL = (\<^bsup>s\<^esup>capPTIsMapped___unsigned AND mask 1),
          cap_page_table_cap_CL.capPTMappedASID_CL = (\<^bsup>s\<^esup>capPTMappedASID___unsigned AND mask 17),
          cap_page_table_cap_CL.capPTMappedAddress_CL = (\<^bsup>s\<^esup>capPTMappedAddress___unsigned AND NOT (mask 20)),
          cap_page_table_cap_CL.capPTBasePtr_CL = (\<^bsup>s\<^esup>capPTBasePtr___unsigned AND NOT (mask 10)) \<rparr> \<and>
        cap_get_tag \<acute>ret__struct_cap_C = scast cap_page_table_cap\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps o_def mask_def shift_over_ao_dists) apply (rule context_conjI[THEN iffD1[OF conj_commute]],
         fastforce simp: cap_get_tag_eq_x cap_page_table_cap_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: cap_page_table_cap_lift_def) apply (erule cap_lift_page_table_cap[THEN subst[OF sym]]; simp?) apply ((intro conjI sign_extend_eq)?;
         (simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
                    word_ao_dist word_bw_assocs word_and_max_simps cap_page_table_cap_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call cap_page_table_cap_new_'proc \<lbrace>cap_page_table_cap_lift \<acute>ret__struct_cap_C = \<lparr>capPTIsMapped_CL = \<^bsup>s\<^esup>capPTIsMapped && mask 1, capPTMappedASID_CL = \<^bsup>s\<^esup>capPTMappedASID && mask 17, capPTMappedAddress_CL = \<^bsup>s\<^esup>capPTMappedAddress && ~~ mask 20, capPTBasePtr_CL = \<^bsup>s\<^esup>capPTBasePtr && ~~ mask 10\<rparr> \<and> cap_get_tag \<acute>ret__struct_cap_C = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 <s 2 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 0 \<le>s 0x14 \<and> 0x14 <s 0x20 \<and> 0 \<le>s 0xC \<and> 0xC <s 0x20 \<and> 0 \<le>s 0x1D \<and> 0x1D <s 0x20 \<and> cap_page_table_cap_lift (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capPTIsMapped && 1 << unat 0x1D)) || (\<acute>capPTMappedASID && 0x1FFFF << unat 0xC)) || (\<acute>capPTMappedAddress && 0xFFF00000 >> unat 0x14))) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capPTBasePtr && 0xFFFFFC00 >> unat 0)) || (SCAST(32 signed \<rightarrow> 32) cap_page_table_cap && 0xF << unat 0))) v)) = \<lparr>capPTIsMapped_CL = \<^bsup>s\<^esup>capPTIsMapped && mask 1, capPTMappedASID_CL = \<^bsup>s\<^esup>capPTMappedASID && mask 17, capPTMappedAddress_CL = \<^bsup>s\<^esup>capPTMappedAddress && ~~ mask 20, capPTBasePtr_CL = \<^bsup>s\<^esup>capPTBasePtr && ~~ mask 10\<rparr> \<and> cap_get_tag (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capPTIsMapped && 1 << unat 0x1D)) || (\<acute>capPTMappedASID && 0x1FFFF << unat 0xC)) || (\<acute>capPTMappedAddress && 0xFFF00000 >> unat 0x14))) (cap_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) ((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>capPTBasePtr && 0xFFFFFC00 >> unat 0)) || (SCAST(32 signed \<rightarrow> 32) cap_page_table_cap && 0xF << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. cap_page_table_cap_lift (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 (capPTBasePtr_' s && 0xFFFFFC00 || SCAST(32 signed \<rightarrow> 32) cap_page_table_cap && 0xF)) (Suc 0) (((capPTIsMapped_' s << 29) && 0x20000000 || (capPTMappedASID_' s << 12) && 0x1FFFF000) || (capPTMappedAddress_' s >> 20) && 0xFFF)) v) = \<lparr>capPTIsMapped_CL = capPTIsMapped_' s && 1, capPTMappedASID_CL = capPTMappedASID_' s && 0x1FFFF, capPTMappedAddress_CL = capPTMappedAddress_' s && 0xFFF00000, capPTBasePtr_CL = capPTBasePtr_' s && 0xFFFFFC00\<rparr> \<and> cap_get_tag (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 (capPTBasePtr_' s && 0xFFFFFC00 || SCAST(32 signed \<rightarrow> 32) cap_page_table_cap && 0xF)) (Suc 0) (((capPTIsMapped_' s << 29) && 0x20000000 || (capPTMappedASID_' s << 12) && 0x1FFFF000) || (capPTMappedAddress_' s >> 20) && 0xFFF)) v) = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap proof (prove)
goal (1 subgoal):
 1. \<And>s v. cap_get_tag (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 (capPTBasePtr_' s && 0xFFFFFC00 || SCAST(32 signed \<rightarrow> 32) cap_page_table_cap && 0xF)) (Suc 0) (((capPTIsMapped_' s << 29) && 0x20000000 || (capPTMappedASID_' s << 12) && 0x1FFFF000) || (capPTMappedAddress_' s >> 20) && 0xFFF)) v) = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<Longrightarrow> cap_page_table_cap_lift (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 (capPTBasePtr_' s && 0xFFFFFC00 || SCAST(32 signed \<rightarrow> 32) cap_page_table_cap && 0xF)) (Suc 0) (((capPTIsMapped_' s << 29) && 0x20000000 || (capPTMappedASID_' s << 12) && 0x1FFFF000) || (capPTMappedAddress_' s >> 20) && 0xFFF)) v) = \<lparr>capPTIsMapped_CL = capPTIsMapped_' s && 1, capPTMappedASID_CL = capPTMappedASID_' s && 0x1FFFF, capPTMappedAddress_CL = capPTMappedAddress_' s && 0xFFF00000, capPTBasePtr_CL = capPTBasePtr_' s && 0xFFFFFC00\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s v. cap_get_tag (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 (capPTBasePtr_' s && 0xFFFFFC00 || SCAST(32 signed \<rightarrow> 32) cap_page_table_cap && 0xF)) (Suc 0) (((capPTIsMapped_' s << 29) && 0x20000000 || (capPTMappedASID_' s << 12) && 0x1FFFF000) || (capPTMappedAddress_' s >> 20) && 0xFFF)) v) = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<Longrightarrow> (case cap_lift (cap_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x 0 (capPTBasePtr_' s && 0xFFFFFC00 || SCAST(32 signed \<rightarrow> 32) cap_page_table_cap && 0xF)) (Suc 0) (((capPTIsMapped_' s << 29) && 0x20000000 || (capPTMappedASID_' s << 12) && 0x1FFFF000) || (capPTMappedAddress_' s >> 20) && 0xFFF)) v) of Some (Cap_page_table_cap rec) \<Rightarrow> rec) = \<lparr>capPTIsMapped_CL = capPTIsMapped_' s && 1, capPTMappedASID_CL = capPTMappedASID_' s && 0x1FFFF, capPTMappedAddress_CL = capPTMappedAddress_' s && 0xFFF00000, capPTBasePtr_CL = capPTBasePtr_' s && 0xFFFFFC00\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. (((capPTIsMapped_' s << 29) && 0x20000000 || (capPTMappedASID_' s << 12) && 0x1FFFF000) || (capPTMappedAddress_' s >> 20) && 0xFFF >> 29) && 1 = capPTIsMapped_' s && 1 \<and> (((capPTIsMapped_' s << 29) && 0x20000000 || (capPTMappedASID_' s << 12) && 0x1FFFF000) || (capPTMappedAddress_' s >> 20) && 0xFFF >> 12) && mask 17 = capPTMappedASID_' s && 0x1FFFF \<and> (((capPTIsMapped_' s << 29) && 0x20000000 || (capPTMappedASID_' s << 12) && 0x1FFFF000) || (capPTMappedAddress_' s >> 20) && 0xFFF << 20) && ~~ mask 20 = capPTMappedAddress_' s && 0xFFF00000 \<and> (capPTBasePtr_' s && 0xFFFFFC00 || SCAST(32 signed \<rightarrow> 32) cap_page_table_cap && 0xF) && ~~ mask 10 = capPTBasePtr_' s && 0xFFFFFC00 proof (prove)
goal:
No subgoals!