theory structures_proofs

lemma (in kernel_all_substitute) lookup_fault_depth_mismatch_get_bitsLeft_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. lookup_fault_get_tag \<acute>lookup_fault = scast lookup_fault_depth_mismatch\<rbrace>
       \<acute>ret__unsigned :== PROC lookup_fault_depth_mismatch_get_bitsLeft(\<acute>lookup_fault)
       \<lbrace>\<acute>ret__unsigned = lookup_fault_depth_mismatch_CL.bitsLeft_CL (lookup_fault_depth_mismatch_lift \<^bsup>s\<^esup>lookup_fault)\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp:guard_simps) apply (simp add:lookup_fault_depth_mismatch_lift_def) apply (subst lookup_fault_lift_depth_mismatch) apply (simp add: o_def
                    lookup_fault_get_tag_def
                    lookup_fault_depth_mismatch_def
                    mask_def word_size shift_over_ao_dists) apply (subst lookup_fault_lift_depth_mismatch, simp)? apply (simp add: o_def
                   lookup_fault_get_tag_def
                   lookup_fault_depth_mismatch_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. lookup_fault_get_tag \<acute>lookup_fault = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch\<rbrace> Call lookup_fault_depth_mismatch_get_bitsLeft_'proc \<lbrace>\<acute>ret__unsigned = lookup_fault_depth_mismatch_CL.bitsLeft_CL (lookup_fault_depth_mismatch_lift \<^bsup>s\<^esup>lookup_fault)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. lookup_fault_get_tag \<acute>lookup_fault = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch\<rbrace> \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 2 \<and> 2 <s 0x20 \<and> 0 <s 2 \<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 (lookup_fault_C.words_C \<acute>lookup_fault.[unat 0] && 0xFC >> unat 2) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (lookup_fault_C.words_C \<acute>lookup_fault.[unat 0] && 0xFC >> unat 2) || SCAST(32 signed \<rightarrow> 32) 0 = lookup_fault_depth_mismatch_CL.bitsLeft_CL (lookup_fault_depth_mismatch_lift \<^bsup>s\<^esup>lookup_fault)) \<and> ((if (lookup_fault_C.words_C \<acute>lookup_fault.[unat 0] && 0xFC >> unat 2) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> lookup_fault_C.words_C \<acute>lookup_fault.[unat 0] && 0xFC >> unat 2 = lookup_fault_depth_mismatch_CL.bitsLeft_CL (lookup_fault_depth_mismatch_lift \<^bsup>s\<^esup>lookup_fault))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> lookup_fault_C.words_C \<acute>lookup_fault.[unat 0] && 0xFC >> unat 2 = lookup_fault_depth_mismatch_CL.bitsLeft_CL (lookup_fault_depth_mismatch_lift \<^bsup>s\<^esup>lookup_fault))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. lookup_fault_get_tag (lookup_fault_' x) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch \<Longrightarrow> lookup_fault_C.words_C (lookup_fault_' x).[0] && 0xFC >> 2 = lookup_fault_depth_mismatch_CL.bitsLeft_CL (lookup_fault_depth_mismatch_lift (lookup_fault_' x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. lookup_fault_get_tag (lookup_fault_' x) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch \<Longrightarrow> lookup_fault_C.words_C (lookup_fault_' x).[0] && 0xFC >> 2 = lookup_fault_depth_mismatch_CL.bitsLeft_CL (case lookup_fault_lift (lookup_fault_' x) of Some (Lookup_fault_depth_mismatch rec) \<Rightarrow> rec) proof (prove)
goal (2 subgoals):
 1. \<And>x. lookup_fault_get_tag (lookup_fault_' x) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch \<Longrightarrow> lookup_fault_get_tag (lookup_fault_' x) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch
 2. \<And>x. lookup_fault_get_tag (lookup_fault_' x) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch \<Longrightarrow> lookup_fault_C.words_C (lookup_fault_' x).[0] && 0xFC >> 2 = lookup_fault_depth_mismatch_CL.bitsLeft_CL (case Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C (lookup_fault_' x).[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C (lookup_fault_' x).[0] >> 2) && mask 6\<rparr>) of Some (Lookup_fault_depth_mismatch rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. lookup_fault_get_tag (lookup_fault_' x) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch \<Longrightarrow> lookup_fault_C.words_C (lookup_fault_' x).[0] && 0xFC >> 2 = lookup_fault_depth_mismatch_CL.bitsLeft_CL (case Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C (lookup_fault_' x).[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C (lookup_fault_' x).[0] >> 2) && mask 6\<rparr>) of Some (Lookup_fault_depth_mismatch rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. lookup_fault_get_tag (lookup_fault_' x) = SCAST(32 signed \<rightarrow> 32) lookup_fault_depth_mismatch \<Longrightarrow> lookup_fault_C.words_C (lookup_fault_' x).[0] && 0xFC >> 2 = lookup_fault_depth_mismatch_CL.bitsLeft_CL (case Some (Lookup_fault_depth_mismatch \<lparr>lookup_fault_depth_mismatch_CL.bitsFound_CL = (lookup_fault_C.words_C (lookup_fault_' x).[0] >> 8) && mask 6, bitsLeft_CL = (lookup_fault_C.words_C (lookup_fault_' x).[0] >> 2) && mask 6\<rparr>) of Some (Lookup_fault_depth_mismatch rec) \<Rightarrow> rec) proof (prove)
goal:
No subgoals!