theory structures_proofs

lemma (in kernel_all_substitute) seL4_Fault_CapFault_get_address_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. seL4_Fault_get_tag \<acute>seL4_Fault = scast seL4_Fault_CapFault\<rbrace>
       \<acute>ret__unsigned :== PROC seL4_Fault_CapFault_get_address(\<acute>seL4_Fault)
       \<lbrace>\<acute>ret__unsigned = seL4_Fault_CapFault_CL.address_CL (seL4_Fault_CapFault_lift \<^bsup>s\<^esup>seL4_Fault)\<rbrace>" apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp:guard_simps) apply (simp add:seL4_Fault_CapFault_lift_def) apply (subst seL4_Fault_lift_CapFault) apply (simp add: o_def
                    seL4_Fault_get_tag_def
                    seL4_Fault_CapFault_def
                    mask_def word_size shift_over_ao_dists) apply (subst seL4_Fault_lift_CapFault, simp)? apply (simp add: o_def
                   seL4_Fault_get_tag_def
                   seL4_Fault_CapFault_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. seL4_Fault_get_tag \<acute>seL4_Fault = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault\<rbrace> Call seL4_Fault_CapFault_get_address_'proc \<lbrace>\<acute>ret__unsigned = seL4_Fault_CapFault_CL.address_CL (seL4_Fault_CapFault_lift \<^bsup>s\<^esup>seL4_Fault)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. seL4_Fault_get_tag \<acute>seL4_Fault = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault\<rbrace> \<subseteq> \<lbrace>\<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (seL4_Fault_C.words_C \<acute>seL4_Fault.[unat 1] && 0xFFFFFFFF >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (seL4_Fault_C.words_C \<acute>seL4_Fault.[unat 1] && 0xFFFFFFFF >> unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = seL4_Fault_CapFault_CL.address_CL (seL4_Fault_CapFault_lift \<^bsup>s\<^esup>seL4_Fault)) \<and> ((if (seL4_Fault_C.words_C \<acute>seL4_Fault.[unat 1] && 0xFFFFFFFF >> unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> seL4_Fault_C.words_C \<acute>seL4_Fault.[unat 1] && 0xFFFFFFFF >> unat 0 = seL4_Fault_CapFault_CL.address_CL (seL4_Fault_CapFault_lift \<^bsup>s\<^esup>seL4_Fault))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> seL4_Fault_C.words_C \<acute>seL4_Fault.[unat 1] && 0xFFFFFFFF >> unat 0 = seL4_Fault_CapFault_CL.address_CL (seL4_Fault_CapFault_lift \<^bsup>s\<^esup>seL4_Fault))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. seL4_Fault_get_tag (seL4_Fault_' x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault \<Longrightarrow> seL4_Fault_C.words_C (seL4_Fault_' x).[Suc 0] && 0xFFFFFFFF = seL4_Fault_CapFault_CL.address_CL (seL4_Fault_CapFault_lift (seL4_Fault_' x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. seL4_Fault_get_tag (seL4_Fault_' x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault \<Longrightarrow> seL4_Fault_C.words_C (seL4_Fault_' x).[Suc 0] && 0xFFFFFFFF = seL4_Fault_CapFault_CL.address_CL (case seL4_Fault_lift (seL4_Fault_' x) of Some (SeL4_Fault_CapFault rec) \<Rightarrow> rec) proof (prove)
goal (2 subgoals):
 1. \<And>x. seL4_Fault_get_tag (seL4_Fault_' x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault \<Longrightarrow> seL4_Fault_get_tag (seL4_Fault_' x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault
 2. \<And>x. seL4_Fault_get_tag (seL4_Fault_' x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault \<Longrightarrow> seL4_Fault_C.words_C (seL4_Fault_' x).[Suc 0] && 0xFFFFFFFF = seL4_Fault_CapFault_CL.address_CL (case Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C (seL4_Fault_' x).[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C (seL4_Fault_' x).[0] >> 31) && mask 1\<rparr>) of Some (SeL4_Fault_CapFault rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. seL4_Fault_get_tag (seL4_Fault_' x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault \<Longrightarrow> seL4_Fault_C.words_C (seL4_Fault_' x).[Suc 0] && 0xFFFFFFFF = seL4_Fault_CapFault_CL.address_CL (case Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C (seL4_Fault_' x).[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C (seL4_Fault_' x).[0] >> 31) && mask 1\<rparr>) of Some (SeL4_Fault_CapFault rec) \<Rightarrow> rec) proof (prove)
goal (1 subgoal):
 1. \<And>x. seL4_Fault_get_tag (seL4_Fault_' x) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_CapFault \<Longrightarrow> seL4_Fault_C.words_C (seL4_Fault_' x).[Suc 0] && 0xFFFFFFFF = seL4_Fault_CapFault_CL.address_CL (case Some (SeL4_Fault_CapFault \<lparr>seL4_Fault_CapFault_CL.address_CL = seL4_Fault_C.words_C (seL4_Fault_' x).[1] >> 0, inReceivePhase_CL = (seL4_Fault_C.words_C (seL4_Fault_' x).[0] >> 31) && mask 1\<rparr>) of Some (SeL4_Fault_CapFault rec) \<Rightarrow> rec) proof (prove)
goal:
No subgoals!