theory structures_proofs

lemma (in kernel_all_substitute) pde_pde_invalid_get_stored_hw_asid_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. pde_get_tag \<acute>pde = scast pde_pde_invalid\<rbrace>
       \<acute>ret__unsigned :== PROC pde_pde_invalid_get_stored_hw_asid(\<acute>pde)
       \<lbrace>\<acute>ret__unsigned = pde_pde_invalid_CL.stored_hw_asid_CL (pde_pde_invalid_lift \<^bsup>s\<^esup>pde)\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp:guard_simps) apply (simp add:pde_pde_invalid_lift_def) apply (subst pde_lift_pde_invalid) apply (simp add: o_def
                    pde_get_tag_def
                    pde_pde_invalid_def
                    mask_def word_size shift_over_ao_dists) apply (subst pde_lift_pde_invalid, simp)? apply (simp add: o_def
                   pde_get_tag_def
                   pde_pde_invalid_def
                   mask_def word_size shift_over_ao_dists multi_shift_simps
                   word_bw_assocs word_oa_dist word_and_max_simps ucast_def
                   sign_extend_def' nth_is_and_neq_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. pde_get_tag \<acute>pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrace> Call pde_pde_invalid_get_stored_hw_asid_'proc \<lbrace>\<acute>ret__unsigned = stored_hw_asid_CL (pde_pde_invalid_lift \<^bsup>s\<^esup>pde)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. pde_get_tag \<acute>pde = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid\<rbrace> \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 0x18 \<and> 0x18 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (pde_C.words_C \<acute>pde.[unat 0] && 0xFF000000 >> unat 0x18) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (pde_C.words_C \<acute>pde.[unat 0] && 0xFF000000 >> unat 0x18) || SCAST(32 signed \<rightarrow> 32) 0 = stored_hw_asid_CL (pde_pde_invalid_lift \<^bsup>s\<^esup>pde)) \<and> ((if (pde_C.words_C \<acute>pde.[unat 0] && 0xFF000000 >> unat 0x18) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> pde_C.words_C \<acute>pde.[unat 0] && 0xFF000000 >> unat 0x18 = stored_hw_asid_CL (pde_pde_invalid_lift \<^bsup>s\<^esup>pde))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> pde_C.words_C \<acute>pde.[unat 0] && 0xFF000000 >> unat 0x18 = stored_hw_asid_CL (pde_pde_invalid_lift \<^bsup>s\<^esup>pde))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. pde_get_tag (pde_' x) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> pde_C.words_C (pde_' x).[0] && 0xFF000000 >> 24 = stored_hw_asid_CL (pde_pde_invalid_lift (pde_' x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. pde_get_tag (pde_' x) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> pde_C.words_C (pde_' x).[0] && 0xFF000000 >> 24 = stored_hw_asid_CL (case pde_lift (pde_' x) of Some (Pde_pde_invalid rec) \<Rightarrow> rec) proof (prove)
goal (2 subgoals):
 1. \<And>x. pde_get_tag (pde_' x) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> pde_get_tag (pde_' x) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid
 2. \<And>x. pde_get_tag (pde_' x) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> pde_C.words_C (pde_' x).[0] && 0xFF000000 >> 24 = stored_hw_asid_CL (case Some (Pde_pde_invalid \<lparr>stored_hw_asid_CL = (pde_C.words_C (pde_' x).[0] >> 24) && mask 8, stored_asid_valid_CL = (pde_C.words_C (pde_' x).[0] >> 23) && mask 1\<rparr>) of Some (Pde_pde_invalid rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. pde_get_tag (pde_' x) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> pde_C.words_C (pde_' x).[0] && 0xFF000000 >> 24 = stored_hw_asid_CL (case Some (Pde_pde_invalid \<lparr>stored_hw_asid_CL = (pde_C.words_C (pde_' x).[0] >> 24) && mask 8, stored_asid_valid_CL = (pde_C.words_C (pde_' x).[0] >> 23) && mask 1\<rparr>) of Some (Pde_pde_invalid rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. pde_get_tag (pde_' x) = SCAST(32 signed \<rightarrow> 32) pde_pde_invalid \<Longrightarrow> pde_C.words_C (pde_' x).[0] && 0xFF000000 >> 24 = stored_hw_asid_CL (case Some (Pde_pde_invalid \<lparr>stored_hw_asid_CL = (pde_C.words_C (pde_' x).[0] >> 24) && mask 8, stored_asid_valid_CL = (pde_C.words_C (pde_' x).[0] >> 23) && mask 1\<rparr>) of Some (Pde_pde_invalid rec) \<Rightarrow> rec) proof (prove)
goal:
No subgoals!