theory structures_proofs

lemma (in kernel_all_substitute) seL4_Fault_VMFault_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_seL4_Fault_C :== PROC seL4_Fault_VMFault_new(\<acute>address, \<acute>FSR, \<acute>instructionFault)
       \<lbrace>seL4_Fault_VMFault_lift \<acute>ret__struct_seL4_Fault_C = \<lparr>
          seL4_Fault_VMFault_CL.address_CL = (\<^bsup>s\<^esup>address___unsigned AND mask 32),
          seL4_Fault_VMFault_CL.FSR_CL = (\<^bsup>s\<^esup>FSR___unsigned AND mask 14),
          seL4_Fault_VMFault_CL.instructionFault_CL = (\<^bsup>s\<^esup>instructionFault___unsigned AND mask 1) \<rparr> \<and>
        seL4_Fault_get_tag \<acute>ret__struct_seL4_Fault_C = scast seL4_Fault_VMFault\<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: seL4_Fault_get_tag_eq_x seL4_Fault_VMFault_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: seL4_Fault_VMFault_lift_def) apply (erule seL4_Fault_lift_VMFault[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 seL4_Fault_VMFault_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call seL4_Fault_VMFault_new_'proc \<lbrace>seL4_Fault_VMFault_lift \<acute>ret__struct_seL4_Fault_C = \<lparr>seL4_Fault_VMFault_CL.address_CL = \<^bsup>s\<^esup>address && mask 32, FSR_CL = \<^bsup>s\<^esup>FSR && mask 14, instructionFault_CL = \<^bsup>s\<^esup>instructionFault && mask 1\<rparr> \<and> seL4_Fault_get_tag \<acute>ret__struct_seL4_Fault_C = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault\<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 0x11 \<and> 0x11 <s 0x20 \<and> 0 \<le>s 0x12 \<and> 0x12 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> seL4_Fault_VMFault_lift (seL4_Fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>address << unat 0))) (seL4_Fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>FSR && 0x3FFF << unat 0x12)) || (\<acute>instructionFault && 1 << unat 0x11)) || (SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF << unat 0))) v)) = \<lparr>seL4_Fault_VMFault_CL.address_CL = \<^bsup>s\<^esup>address && mask 32, FSR_CL = \<^bsup>s\<^esup>FSR && mask 14, instructionFault_CL = \<^bsup>s\<^esup>instructionFault && mask 1\<rparr> \<and> seL4_Fault_get_tag (seL4_Fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 1) (SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>address << unat 0))) (seL4_Fault_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>FSR && 0x3FFF << unat 0x12)) || (\<acute>instructionFault && 1 << unat 0x11)) || (SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF << unat 0))) v)) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. seL4_Fault_VMFault_lift (seL4_Fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) (address_' s)) 0 (((FSR_' s << 18) && 0xFFFC0000 || (instructionFault_' s << 17) && 0x20000) || SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF)) v) = \<lparr>seL4_Fault_VMFault_CL.address_CL = address_' s, FSR_CL = FSR_' s && 0x3FFF, instructionFault_CL = instructionFault_' s && 1\<rparr> \<and> seL4_Fault_get_tag (seL4_Fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) (address_' s)) 0 (((FSR_' s << 18) && 0xFFFC0000 || (instructionFault_' s << 17) && 0x20000) || SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF)) v) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault proof (prove)
goal (1 subgoal):
 1. \<And>s v. seL4_Fault_get_tag (seL4_Fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) (address_' s)) 0 (((FSR_' s << 18) && 0xFFFC0000 || (instructionFault_' s << 17) && 0x20000) || SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF)) v) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<Longrightarrow> seL4_Fault_VMFault_lift (seL4_Fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) (address_' s)) 0 (((FSR_' s << 18) && 0xFFFC0000 || (instructionFault_' s << 17) && 0x20000) || SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF)) v) = \<lparr>seL4_Fault_VMFault_CL.address_CL = address_' s, FSR_CL = FSR_' s && 0x3FFF, instructionFault_CL = instructionFault_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s v. seL4_Fault_get_tag (seL4_Fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) (address_' s)) 0 (((FSR_' s << 18) && 0xFFFC0000 || (instructionFault_' s << 17) && 0x20000) || SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF)) v) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<Longrightarrow> (case seL4_Fault_lift (seL4_Fault_C.words_C_update (\<lambda>x. Arrays.update (Arrays.update x (Suc 0) (address_' s)) 0 (((FSR_' s << 18) && 0xFFFC0000 || (instructionFault_' s << 17) && 0x20000) || SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF)) v) of Some (SeL4_Fault_VMFault rec) \<Rightarrow> rec) = \<lparr>seL4_Fault_VMFault_CL.address_CL = address_' s, FSR_CL = FSR_' s && 0x3FFF, instructionFault_CL = instructionFault_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. (((FSR_' s << 18) && 0xFFFC0000 || (instructionFault_' s << 17) && 0x20000) || SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF >> 18) && mask 14 = FSR_' s && 0x3FFF \<and> (((FSR_' s << 18) && 0xFFFC0000 || (instructionFault_' s << 17) && 0x20000) || SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault && 0xF >> 17) && 1 = instructionFault_' s && 1 proof (prove)
goal:
No subgoals!