kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_IF

lemma get_extra_cptrs_rev:
  "reads_equiv_valid_inv A aag
     (K (ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and>
         (buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits))))
     (get_extra_cptrs buffer mi)" unfolding get_extra_cptrs_def apply (rule gen_asm_ev) apply clarsimp apply (case_tac buffer, simp_all add: return_ev_pre) apply (wp mapM_ev equiv_valid_guard_imp[OF load_word_offs_rev]
         | erule (2) aag_has_auth_to_read_cptrs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and> buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits))) (get_extra_cptrs buffer mi) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and> buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits))) (rec_option (\<lambda>mi. return []) (\<lambda>buf mi. liftM (map data_to_cptr) $ mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]) buffer mi) proof (prove)
goal (1 subgoal):
 1. ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and> buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits) \<Longrightarrow> reads_equiv_valid_inv A aag (\<lambda>_. True) (rec_option (\<lambda>mi. return []) (\<lambda>buf mi. liftM (map data_to_cptr) $ mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]) buffer mi) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ipc_buffer_has_read_auth aag (pasSubject aag) buffer; buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)\<rbrakk> \<Longrightarrow> reads_equiv_valid_inv A aag (\<lambda>_. True) (rec_option (\<lambda>mi. return []) (\<lambda>buf mi. liftM (map to_bl) (mapM (load_word_offs buf) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)])) buffer mi) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>ipc_buffer_has_read_auth aag (pasSubject aag) (Some a); buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits); buffer = Some a\<rbrakk> \<Longrightarrow> reads_equiv_valid_inv A aag (\<lambda>_. True) (liftM (map to_bl) (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)])) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma lookup_extra_caps_rev:
  "reads_equiv_valid_inv A aag
     (pas_refined aag and (K (is_subject aag thread)) and
      (\<lambda>s. ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and>
           buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits)))
     (lookup_extra_caps thread buffer mi)" unfolding lookup_extra_caps_def fun_app_def by (wpsimp wp: mapME_ev cap_fault_on_failure_rev lookup_cap_and_slot_rev get_extra_cptrs_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread) and (\<lambda>s. ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and> buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits))) (lookup_extra_caps thread buffer mi) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread) and (\<lambda>s. ipc_buffer_has_read_auth aag (pasSubject aag) buffer \<and> buffer_cptr_index + unat (mi_extra_caps mi) < 2 ^ (msg_align_bits - word_size_bits))) (liftE (get_extra_cptrs buffer mi) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot thread cptr)))
theory Ipc_IF

lemma get_mrs_rev:
  "reads_equiv_valid_inv A aag
     (K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf
                               \<and> unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits)))
     (get_mrs thread buf mi)" unfolding get_mrs_def apply (rule gen_asm_ev) apply (wp mapM_ev'' load_word_offs_rev thread_get_rev
         | wpc
         | rule aag_has_auth_to_read_msg[where mi=mi]
         | clarsimp split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf \<and> unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits))) (get_mrs thread buf mi) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf \<and> unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits))) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) thread;
cpu_mrs <- return (map context msg_registers);
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length];
return (take (unat (mi_length mi)) $ cpu_mrs @ buf_mrs)
od) proof (prove)
goal (1 subgoal):
 1. is_subject aag thread \<and> ipc_buffer_has_read_auth aag (pasSubject aag) buf \<and> unat (mi_length mi) < 2 ^ (msg_align_bits - word_size_bits) \<Longrightarrow> reads_equiv_valid_inv A aag (\<lambda>_. True) (do context <- thread_get (arch_tcb_get_registers \<circ> tcb_arch) thread;
cpu_mrs <- return (map context msg_registers);
buf_mrs <- case buf of None \<Rightarrow> return [] | Some pptr \<Rightarrow> mapM (load_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length];
return (take (unat (mi_length mi)) $ cpu_mrs @ buf_mrs)
od) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma const_on_failure_ev:
  "equiv_valid_inv I A P m
   \<Longrightarrow> equiv_valid_inv I A P (const_on_failure c m)" unfolding const_on_failure_def catch_def by (wp | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P m \<Longrightarrow> equiv_valid_inv I A P (const_on_failure c m) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P m \<Longrightarrow> equiv_valid_inv I A P (do x <- m;
case x of Inl e \<Rightarrow> return c | Inr b \<Rightarrow> return b
od)
theory Ipc_IF

lemma set_extra_badge_reads_respects:
  "reads_respects aag l \<top> (set_extra_badge buffer badge n)" unfolding set_extra_badge_def by (rule store_word_offs_reads_respects)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (set_extra_badge buffer badge n) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (\<lambda>_. True) (store_word_offs buffer (buffer_cptr_index + n) badge)
theory Ipc_IF

lemma reads_equiv_cdt_has_children:
  "\<lbrakk> pas_refined aag s; pas_refined aag s'; is_subject aag (fst slot);
     equiv_for (aag_can_read aag \<circ> fst) cdt s s' \<rbrakk>
     \<Longrightarrow> (\<exists>c. (cdt s) c = Some slot) = (\<exists>c. (cdt s') c = Some slot)" apply (rule iff_exI) by (erule reads_equiv_cdt_has_children0; force)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (fst slot); equiv_for (aag_can_read aag \<circ> fst) cdt s s'\<rbrakk> \<Longrightarrow> (\<exists>c. cdt s c = Some slot) = (\<exists>c. cdt s' c = Some slot) proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>pas_refined aag s; pas_refined aag s'; is_subject aag (fst slot); equiv_for (aag_can_read aag \<circ> fst) cdt s s'\<rbrakk> \<Longrightarrow> (cdt s c = Some slot) = (cdt s' c = Some slot)
theory Ipc_IF

lemma ball_subsetE:
  "\<lbrakk> \<forall>x \<in> S. P x; S' \<subseteq> S; \<And>x. P x \<Longrightarrow> Q x \<rbrakk>
     \<Longrightarrow> \<forall>x \<in> S'. Q x" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>S. P x; S' \<subseteq> S; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> \<forall>x\<in>S'. Q x
theory Ipc_IF

lemma derive_cap_rev':
  "reads_equiv_valid_inv A aag (\<lambda>s. (\<exists>x xa xb d. cap = cap.UntypedCap d x xa xb)
                                    \<longrightarrow> pas_refined aag s \<and> is_subject aag (fst slot))
                         (derive_cap slot cap)" unfolding derive_cap_def apply (rule equiv_valid_guard_imp) apply (wp ensure_no_children_rev arch_derive_cap_rev | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. (\<exists>x xa xb d. cap = UntypedCap d x xa xb) \<longrightarrow> pas_refined aag s \<and> is_subject aag (fst slot)) (derive_cap slot cap) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. (\<exists>x xa xb d. cap = UntypedCap d x xa xb) \<longrightarrow> pas_refined aag s \<and> is_subject aag (fst slot)) (case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap) proof (prove)
goal (2 subgoals):
 1. reads_equiv_valid_inv A aag ?Q (case cap of UntypedCap dev ptr sz f \<Rightarrow> doE ensure_no_children slot;
returnOk cap
odE | ReplyCap ptr m cr \<Rightarrow> returnOk NullCap | IRQControlCap \<Rightarrow> returnOk NullCap | Zombie ptr n sz \<Rightarrow> returnOk NullCap | ArchObjectCap c \<Rightarrow> arch_derive_cap c | _ \<Rightarrow> returnOk cap)
 2. \<And>s. (\<exists>x xa xb d. cap = UntypedCap d x xa xb) \<longrightarrow> pas_refined aag s \<and> is_subject aag (fst slot) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma derive_cap_rev:
  "reads_equiv_valid_inv A aag (\<lambda>s. pas_refined aag s \<and> is_subject aag (fst slot))
                         (derive_cap slot cap)" by (blast intro: equiv_valid_guard_imp[OF derive_cap_rev'])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. pas_refined aag s \<and> is_subject aag (fst slot)) (derive_cap slot cap)
theory Ipc_IF

lemma transfer_caps_loop_reads_respects:
  "reads_respects aag l
     (pas_refined aag and pspace_aligned and valid_vspace_objs and
      valid_arch_state and valid_mdb and valid_objs and
      (\<lambda>s. (\<forall>cap\<in>set caps. valid_cap (fst cap) s
                         \<and> is_subject aag (fst (snd cap))
                         \<and> pas_cap_cur_auth aag (fst cap)
                         \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp = fst cap) (snd cap) s)
         \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot)
                           \<and> cte_wp_at ((=) NullCap) slot s
                           \<and> real_cte_at slot s)
         \<and> distinct slots))
     (transfer_caps_loop ep rcv_buffer n caps slots mi)" apply (rule equiv_valid_guard_imp, rule transfer_caps_loop_reads_respects') by (fastforce elim: cte_wp_at_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp = fst cap) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) (transfer_caps_loop ep rcv_buffer n caps slots mi) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp = fst cap) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and valid_objs and (\<lambda>s. (\<forall>cap\<in>set caps. s \<turnstile> fst cap \<and> is_subject aag (fst (snd cap)) \<and> pas_cap_cur_auth aag (fst cap) \<and> cte_wp_at (\<lambda>cp. fst cap \<noteq> NullCap \<longrightarrow> cp \<noteq> fst cap \<longrightarrow> cp = masked_as_full (fst cap) (fst cap)) (snd cap) s) \<and> (\<forall>slot\<in>set slots. is_subject aag (fst slot) \<and> cte_wp_at ((=) NullCap) slot s \<and> real_cte_at slot s) \<and> distinct slots)) s
theory Ipc_IF

lemma empty_on_failure_ev:
  "equiv_valid_inv I A P m \<Longrightarrow>
  equiv_valid_inv I A P (empty_on_failure m)" unfolding empty_on_failure_def catch_def by (wp | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P m \<Longrightarrow> equiv_valid_inv I A P (empty_on_failure m) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P m \<Longrightarrow> equiv_valid_inv I A P (do x <- m;
case x of Inl e \<Rightarrow> return [] | Inr b \<Rightarrow> return b
od)
theory Ipc_IF

lemma unify_failure_ev:
  "equiv_valid_inv I A P m \<Longrightarrow>
  equiv_valid_inv I A P (unify_failure m)" unfolding unify_failure_def handleE'_def by (wp | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P m \<Longrightarrow> equiv_valid_inv I A P (unify_failure m) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P m \<Longrightarrow> equiv_valid_inv I A P (do v <- m;
case v of Inl e \<Rightarrow> throwError () | Inr v' \<Rightarrow> return (Inr v')
od)
theory Ipc_IF

lemma lookup_slot_for_cnode_op_rev:
  "reads_equiv_valid_inv A aag
     (\<lambda>s. (depth \<noteq> 0 \<and> depth \<le> word_bits)
          \<longrightarrow> (pas_refined aag s \<and> (is_cnode_cap croot \<longrightarrow> is_subject aag (obj_ref_of croot))))
     (lookup_slot_for_cnode_op is_source croot ptr depth)" unfolding lookup_slot_for_cnode_op_def apply (clarsimp split del: if_split) apply (wp resolve_address_bits_rev lookup_error_on_failure_rev
            whenE_throwError_wp
         | wpc
         | rule hoare_post_imp_R[OF hoare_True_E_R[where P="\<top>"]]
         | simp add: split_def split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. depth \<noteq> 0 \<and> depth \<le> word_bits \<longrightarrow> pas_refined aag s \<and> (is_cnode_cap croot \<longrightarrow> is_subject aag (obj_ref_of croot))) (lookup_slot_for_cnode_op is_source croot ptr depth) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. depth \<noteq> 0 \<and> depth \<le> word_bits \<longrightarrow> pas_refined aag s \<and> (is_cnode_cap croot \<longrightarrow> is_subject aag (obj_ref_of croot))) (if is_cnode_cap croot then doE whenE (depth < 1 \<or> word_bits < depth) $ throwError (RangeError 1 (word_of_nat word_bits));
lookup_error_on_failure is_source $ doE ptrbits_for_depth <- returnOk $ drop (length ptr - depth) ptr;
(slot, rem) <- resolve_address_bits (croot, ptrbits_for_depth);
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE
odE else throwError (FailedLookup is_source InvalidRoot)) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (\<lambda>s. 0 < depth \<and> depth \<le> word_bits \<longrightarrow> pas_refined aag s \<and> (is_cnode_cap croot \<longrightarrow> is_subject aag (obj_ref_of croot))) (if is_cnode_cap croot then doE whenE (depth < 1 \<or> word_bits < depth) $ throwError (RangeError 1 (word_of_nat word_bits));
lookup_error_on_failure is_source $ doE ptrbits_for_depth <- returnOk $ drop (length ptr - depth) ptr;
(slot, rem) <- resolve_address_bits (croot, ptrbits_for_depth);
case rem of [] \<Rightarrow> returnOk slot | a # list \<Rightarrow> throwError $ DepthMismatch (length rem) 0
odE
odE else throwError (FailedLookup is_source InvalidRoot)) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma lookup_slot_for_cnode_op_reads_respects:
  "reads_respects aag l (pas_refined aag and K (is_subject aag (obj_ref_of croot)))
     (lookup_slot_for_cnode_op is_source croot ptr depth)" apply (rule equiv_valid_guard_imp[OF lookup_slot_for_cnode_op_rev]) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and K (is_subject aag (obj_ref_of croot))) (lookup_slot_for_cnode_op is_source croot ptr depth) proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_subject aag (obj_ref_of croot))) s \<Longrightarrow> depth \<noteq> 0 \<and> depth \<le> word_bits \<longrightarrow> pas_refined aag s \<and> (is_cnode_cap croot \<longrightarrow> is_subject aag (obj_ref_of croot))
theory Ipc_IF

lemma lookup_cap_rev:
  "reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread))
     (lookup_cap thread ref)" unfolding lookup_cap_def split_def fun_app_def apply (wp lookup_slot_for_thread_rev get_cap_rev | simp | strengthen aag_can_read_self)+ apply (rule lookup_slot_for_thread_authorised) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread)) (lookup_cap thread ref) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (pas_refined aag and K (is_subject aag thread)) (doE p <- lookup_slot_for_thread thread ref;
liftE (get_cap (fst p))
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''\<rbrace> lookup_slot_for_thread thread ref \<lbrace>\<lambda>r s. is_subject aag (fst (fst r))\<rbrace>, -
 2. \<And>s. (pas_refined aag and K (is_subject aag thread)) s \<Longrightarrow> (pas_refined aag and K (is_subject aag thread)) s \<and> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and K (is_subject aag thread)) s \<Longrightarrow> (pas_refined aag and K (is_subject aag thread)) s \<and> (pas_refined aag and K (is_subject aag thread)) s proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma word_plus_power_2_offset_le:
  "\<lbrakk> is_aligned (p :: 'l :: len word) n; is_aligned q m; p < q; n \<le> m; n < len_of TYPE('l) \<rbrakk>
     \<Longrightarrow> p + 2^n \<le> q" apply (drule is_aligned_weaken, assumption) apply (clarsimp simp: is_aligned_def) apply (elim dvdE) apply (rename_tac k ka) apply (rule_tac ua=0 and n="int k" and n'="int ka" in udvd_incr') apply assumption apply (clarsimp simp: uint_nat)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned q m; p < q; n \<le> m; n < LENGTH('l)\<rbrakk> \<Longrightarrow> p + 2 ^ n \<le> q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; p < q; n \<le> m; n < LENGTH('l); is_aligned q n\<rbrakk> \<Longrightarrow> p + 2 ^ n \<le> q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 ^ n dvd unat p; p < q; n \<le> m; n < LENGTH('l); 2 ^ n dvd unat q\<rbrakk> \<Longrightarrow> p + 2 ^ n \<le> q proof (prove)
goal (1 subgoal):
 1. \<And>k ka. \<lbrakk>p < q; n \<le> m; n < LENGTH('l); unat p = 2 ^ n * k; unat q = 2 ^ n * ka\<rbrakk> \<Longrightarrow> p + 2 ^ n \<le> q proof (prove)
goal (1 subgoal):
 1. \<And>k ka. \<lbrakk>p < q; n \<le> m; n < LENGTH('l); unat p = 2 ^ n * k; unat q = 2 ^ n * ka\<rbrakk> \<Longrightarrow> p + 2 ^ n \<le> q proof (prove)
goal (3 subgoals):
 1. \<And>k ka. \<lbrakk>p < q; n \<le> m; n < LENGTH('l); unat p = 2 ^ n * k; unat q = 2 ^ n * ka\<rbrakk> \<Longrightarrow> p < q
 2. \<And>k ka. \<lbrakk>p < q; n \<le> m; n < LENGTH('l); unat p = 2 ^ n * k; unat q = 2 ^ n * ka\<rbrakk> \<Longrightarrow> uint p = 0 + int k * uint (2 ^ n)
 3. \<And>k ka. \<lbrakk>p < q; n \<le> m; n < LENGTH('l); unat p = 2 ^ n * k; unat q = 2 ^ n * ka\<rbrakk> \<Longrightarrow> uint q = 0 + int ka * uint (2 ^ n) proof (prove)
goal (2 subgoals):
 1. \<And>k ka. \<lbrakk>p < q; n \<le> m; n < LENGTH('l); unat p = 2 ^ n * k; unat q = 2 ^ n * ka\<rbrakk> \<Longrightarrow> uint p = 0 + int k * uint (2 ^ n)
 2. \<And>k ka. \<lbrakk>p < q; n \<le> m; n < LENGTH('l); unat p = 2 ^ n * k; unat q = 2 ^ n * ka\<rbrakk> \<Longrightarrow> uint q = 0 + int ka * uint (2 ^ n) proof (prove)
goal:
No subgoals!
theory Ipc_IF

lemma get_endpoint_rev:
  "reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (get_endpoint ptr)" unfolding get_simple_ko_def by (wp get_object_rev | wpc | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (get_endpoint ptr) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (do kobj <- get_object ptr;
assert (is_simple_type kobj);
case partial_inv Endpoint kobj of None \<Rightarrow> fail | Some e \<Rightarrow> return e
od)
theory Ipc_IF

lemma send_endpoint_threads_blocked:
  "\<lbrakk> valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (SendEP list)) ep s; x \<in> set list \<rbrakk>
     \<Longrightarrow> st_tcb_at (send_blocked_on ep) x s" apply (rule ep_queued_st_tcb_at'') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (SendEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> st_tcb_at (send_blocked_on ep) x s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (SendEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> ko_at (Endpoint ?ep) ?ptr s
 2. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (SendEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> (x, ?rt) \<in> ep_q_refs_of ?ep
 3. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (SendEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> valid_objs s
 4. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (SendEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 5. \<And>pl pl'. \<lbrakk>valid_objs s; (sym_refs \<circ> state_refs_of) s; ko_at (Endpoint (SendEP list)) ep s; x \<in> set list\<rbrakk> \<Longrightarrow> ?rt = EPSend \<and> send_blocked_on ep (BlockedOnSend ?ptr pl) \<or> ?rt = EPRecv \<and> send_blocked_on ep (BlockedOnReceive ?ptr pl') proof (prove)
goal:
No subgoals!