theory structures_proofs

lemma (in kernel_all_substitute) pde_pde_invalid_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_pde_C :== PROC pde_pde_invalid_new(\<acute>stored_hw_asid, \<acute>stored_asid_valid)
       \<lbrace>pde_pde_invalid_lift \<acute>ret__struct_pde_C = \<lparr>
          pde_pde_invalid_CL.stored_hw_asid_CL = (\<^bsup>s\<^esup>stored_hw_asid___unsigned AND mask 8),
          pde_pde_invalid_CL.stored_asid_valid_CL = (\<^bsup>s\<^esup>stored_asid_valid___unsigned AND mask 1) \<rparr> \<and>
        pde_get_tag \<acute>ret__struct_pde_C = scast pde_pde_invalid\<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: pde_get_tag_eq_x pde_pde_invalid_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: pde_pde_invalid_lift_def) apply (erule pde_lift_pde_invalid[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 pde_pde_invalid_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call pde_pde_invalid_new_'proc \<lbrace>pde_pde_invalid_lift \<acute>ret__struct_pde_C = \<lparr>stored_hw_asid_CL = \<^bsup>s\<^esup>stored_hw_asid && mask 8, stored_asid_valid_CL = \<^bsup>s\<^esup>stored_asid_valid && mask 1\<rparr> \<and> pde_get_tag \<acute>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 0x17 \<and> 0x17 <s 0x20 \<and> 0 \<le>s 0x18 \<and> 0x18 <s 0x20 \<and> pde_pde_invalid_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>stored_hw_asid && 0xFF << unat 0x18)) || (\<acute>stored_asid_valid && 1 << unat 0x17)) || (SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3 << unat 0))) v) = \<lparr>stored_hw_asid_CL = \<^bsup>s\<^esup>stored_hw_asid && mask 8, stored_asid_valid_CL = \<^bsup>s\<^esup>stored_asid_valid && mask 1\<rparr> \<and> pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>stored_hw_asid && 0xFF << unat 0x18)) || (\<acute>stored_asid_valid && 1 << unat 0x17)) || (SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3 << unat 0))) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. pde_pde_invalid_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((stored_hw_asid_' s << 24) && 0xFF000000 || (stored_asid_valid_' s << 23) && 0x800000) || SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3)) v) = \<lparr>stored_hw_asid_CL = stored_hw_asid_' s && 0xFF, stored_asid_valid_CL = stored_asid_valid_' s && 1\<rparr> \<and> pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((stored_hw_asid_' s << 24) && 0xFF000000 || (stored_asid_valid_' s << 23) && 0x800000) || SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3)) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid proof (prove)
goal (1 subgoal):
 1. \<And>s v. pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((stored_hw_asid_' s << 24) && 0xFF000000 || (stored_asid_valid_' s << 23) && 0x800000) || SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3)) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> pde_pde_invalid_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((stored_hw_asid_' s << 24) && 0xFF000000 || (stored_asid_valid_' s << 23) && 0x800000) || SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3)) v) = \<lparr>stored_hw_asid_CL = stored_hw_asid_' s && 0xFF, stored_asid_valid_CL = stored_asid_valid_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s v. pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((stored_hw_asid_' s << 24) && 0xFF000000 || (stored_asid_valid_' s << 23) && 0x800000) || SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3)) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> (case pde_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 (((stored_hw_asid_' s << 24) && 0xFF000000 || (stored_asid_valid_' s << 23) && 0x800000) || SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3)) v) of Some (Pde_pde_invalid rec) \<Rightarrow> rec) = \<lparr>stored_hw_asid_CL = stored_hw_asid_' s && 0xFF, stored_asid_valid_CL = stored_asid_valid_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. (((stored_hw_asid_' s << 24) && 0xFF000000 || (stored_asid_valid_' s << 23) && 0x800000) || SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3 >> 24) && mask 8 = stored_hw_asid_' s && 0xFF \<and> (((stored_hw_asid_' s << 24) && 0xFF000000 || (stored_asid_valid_' s << 23) && 0x800000) || SCAST(32 signed \<rightarrow> 32) pde_pde_invalid && 3 >> 23) && 1 = stored_asid_valid_' s && 1 proof (prove)
goal:
No subgoals!