theory structures_proofs

lemma (in kernel_all_substitute) lookup_fault_depth_mismatch_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_lookup_fault_C :== PROC lookup_fault_depth_mismatch_new(\<acute>bitsFound, \<acute>bitsLeft)
       \<lbrace>lookup_fault_depth_mismatch_lift \<acute>ret__struct_lookup_fault_C = \<lparr>
          lookup_fault_depth_mismatch_CL.bitsFound_CL = (\<^bsup>s\<^esup>bitsFound___unsigned AND mask 6),
          lookup_fault_depth_mismatch_CL.bitsLeft_CL = (\<^bsup>s\<^esup>bitsLeft___unsigned AND mask 6) \<rparr> \<and>
        lookup_fault_get_tag \<acute>ret__struct_lookup_fault_C = scast lookup_fault_depth_mismatch\<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: lookup_fault_get_tag_eq_x lookup_fault_depth_mismatch_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: lookup_fault_depth_mismatch_lift_def) apply (erule lookup_fault_lift_depth_mismatch[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 lookup_fault_depth_mismatch_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call lookup_fault_depth_mismatch_new_'proc \<lbrace>lookup_fault_depth_mismatch_lift \<acute>ret__struct_lookup_fault_C = \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = \<^bsup>s\<^esup>bitsFound && mask 6, bitsLeft_CL = \<^bsup>s\<^esup>bitsLeft && mask 6\<rparr> \<and> lookup_fault_get_tag \<acute>ret__struct_lookup_fault_C = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch\<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 2 \<and> 2 <s 0x20 \<and> 0 \<le>s 8 \<and> 8 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> lookup_fault_depth_mismatch_lift (lookup_fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (SCAST(32 signed \<rightarrow> 32) 0)) (lookup_fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>bitsFound && 0x3F << unat 8)) || (\<acute>bitsLeft && 0x3F << unat 2)) || (SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3 << unat 0))) v)) = \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = \<^bsup>s\<^esup>bitsFound && mask 6, bitsLeft_CL = \<^bsup>s\<^esup>bitsLeft && mask 6\<rparr> \<and> lookup_fault_get_tag (lookup_fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (SCAST(32 signed \<rightarrow> 32) 0)) (lookup_fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>bitsFound && 0x3F << unat 8)) || (\<acute>bitsLeft && 0x3F << unat 2)) || (SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3 << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. lookup_fault_depth_mismatch_lift (lookup_fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) 0) 0 (((bitsFound_' s << 8) && 0x3F00 || (bitsLeft_' s << 2) && 0xFC) || SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3)) v) = \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = bitsFound_' s && 0x3F, bitsLeft_CL = bitsLeft_' s && 0x3F\<rparr> \<and> lookup_fault_get_tag (lookup_fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) 0) 0 (((bitsFound_' s << 8) && 0x3F00 || (bitsLeft_' s << 2) && 0xFC) || SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3)) v) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch proof (prove)
goal (1 subgoal):
 1. \<And>s v. lookup_fault_get_tag (lookup_fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) 0) 0 (((bitsFound_' s << 8) && 0x3F00 || (bitsLeft_' s << 2) && 0xFC) || SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3)) v) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch \<Longrightarrow> lookup_fault_depth_mismatch_lift (lookup_fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) 0) 0 (((bitsFound_' s << 8) && 0x3F00 || (bitsLeft_' s << 2) && 0xFC) || SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3)) v) = \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = bitsFound_' s && 0x3F, bitsLeft_CL = bitsLeft_' s && 0x3F\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s v. lookup_fault_get_tag (lookup_fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) 0) 0 (((bitsFound_' s << 8) && 0x3F00 || (bitsLeft_' s << 2) && 0xFC) || SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3)) v) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch \<Longrightarrow> (case lookup_fault_lift (lookup_fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) 0) 0 (((bitsFound_' s << 8) && 0x3F00 || (bitsLeft_' s << 2) && 0xFC) || SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3)) v) of Some (Lookup_fault_depth_mismatch rec) \<Rightarrow> rec) = \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = bitsFound_' s && 0x3F, bitsLeft_CL = bitsLeft_' s && 0x3F\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. (((bitsFound_' s << 8) && 0x3F00 || (bitsLeft_' s << 2) && 0xFC) || SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3 >> 8) && mask 6 = bitsFound_' s && 0x3F \<and> (((bitsFound_' s << 8) && 0x3F00 || (bitsLeft_' s << 2) && 0xFC) || SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch && 3 >> 2) && mask 6 = bitsLeft_' s && 0x3F proof (prove)
goal:
No subgoals!