theory structures_proofs

lemma (in kernel_all_substitute) thread_state_ptr_get_blockingObject_spec:
           defines "ptrval s \<equiv> cslift s (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''] :: tcb_C ptr)"
           shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''] :: tcb_C ptr)\<rbrace>
            \<acute>ret__unsigned :== PROC thread_state_ptr_get_blockingObject(\<acute>thread_state_ptr)
            \<lbrace>\<acute>ret__unsigned = thread_state_CL.blockingObject_CL (thread_state_lift ((tcb_C.tcbState_C (the (ptrval s)))))\<rbrace> " unfolding ptrval_def apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps) apply (frule iffD1[OF h_t_valid_clift_Some_iff], rule exE, assumption, simp) apply (frule clift_subtype, simp, simp, simp) apply (simp add: typ_heap_simps) apply (simp add: thread_state_lift_def) apply (simp add: sign_extend_def' mask_def nth_is_and_neq_0 word_bw_assocs
                   shift_over_ao_dists word_oa_dist word_and_max_simps)? apply (simp add: mask_shift_simps)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']\<rbrace> Call thread_state_ptr_get_blockingObject_'proc \<lbrace>\<acute>ret__unsigned = blockingObject_CL (thread_state_lift (tcbState_C (the (ptrval s))))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']\<rbrace> Call thread_state_ptr_get_blockingObject_'proc \<lbrace>\<acute>ret__unsigned = blockingObject_CL (thread_state_lift (tcbState_C (the (cslift s (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''])))))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']\<rbrace> \<subseteq> {sa. \<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 3 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c thread_state_ptr_' sa \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFFFFFF0 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFFFFFF0 << unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = blockingObject_CL (thread_state_lift (tcbState_C (the (cslift s (cparent (thread_state_ptr_' s) [''tcbState_C''])))))) \<and> ((if (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFFFFFF0 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFFFFFF0 << unat 0 = blockingObject_CL (thread_state_lift (tcbState_C (the (cslift s (cparent (thread_state_ptr_' s) [''tcbState_C'']))))))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFFFFFF0 << unat 0 = blockingObject_CL (thread_state_lift (tcbState_C (the (cslift s (cparent (thread_state_ptr_' s) [''tcbState_C'']))))))} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C''] \<Longrightarrow> x \<Turnstile>\<^sub>c thread_state_ptr_' x \<and> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xFFFFFFF0 = blockingObject_CL (thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c thread_state_ptr_' x \<and> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xFFFFFFF0 = blockingObject_CL (thread_state_lift (tcbState_C xa)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa)\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c thread_state_ptr_' x \<and> h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xFFFFFFF0 = blockingObject_CL (thread_state_lift (tcbState_C xa)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa)\<rbrakk> \<Longrightarrow> thread_state_C.words_C (tcbState_C xa).[0] && 0xFFFFFFF0 = blockingObject_CL (thread_state_lift (tcbState_C xa)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa)\<rbrakk> \<Longrightarrow> thread_state_C.words_C (tcbState_C xa).[0] && 0xFFFFFFF0 = thread_state_C.words_C (tcbState_C xa).[0] && ~~ mask 4 proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!