kings-crown/FVELER_Isabelle huggingface dataset:
theory Invoke_C

lemma slotcap_in_mem_ThreadCap:
  "\<lbrakk> slotcap_in_mem cap slot (ctes_of s); (s, s') \<in> rf_sr \<rbrakk>
       \<Longrightarrow> \<exists>v. cslift s' (cte_Ptr slot) = Some v
           \<and> (cap_get_tag (cte_C.cap_C v) = scast cap_thread_cap)
              = (isThreadCap cap)
           \<and> (isThreadCap cap
                  \<longrightarrow> ccap_relation cap (cte_C.cap_C v))" apply (clarsimp simp: slotcap_in_mem_def) apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) apply (clarsimp dest!: ccte_relation_ccap_relation) apply (simp add: cap_get_tag_isCap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slotcap_in_mem cap slot (ctes_of s); (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>v. cslift s' (cte_Ptr slot) = Some v \<and> (cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = isThreadCap cap \<and> (isThreadCap cap \<longrightarrow> ccap_relation cap (cte_C.cap_C v)) proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s slot = Some cte; cap = cteCap cte\<rbrakk> \<Longrightarrow> \<exists>v. cslift s' (cte_Ptr slot) = Some v \<and> (cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = isThreadCap (cteCap cte) \<and> (isThreadCap (cteCap cte) \<longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C v)) proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>ctes_of s slot = Some cte; cap = cteCap cte; ctes_of s slot = Some cte; ccte_relation cte y'; cslift s' (cte_Ptr slot) = Some y'\<rbrakk> \<Longrightarrow> \<exists>v. cslift s' (cte_Ptr slot) = Some v \<and> (cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = isThreadCap (cteCap cte) \<and> (isThreadCap (cteCap cte) \<longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C v)) proof (prove)
goal (1 subgoal):
 1. \<And>cte y'. \<lbrakk>cap = cteCap cte; ctes_of s slot = Some cte; cslift s' (cte_Ptr slot) = Some y'; ccap_relation (cteCap cte) (cte_C.cap_C y')\<rbrakk> \<Longrightarrow> (cap_get_tag (cte_C.cap_C y') = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) = isThreadCap (cteCap cte) proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma cap_case_ThreadCap2:
  "(case cap of (ThreadCap ptr) \<Rightarrow> f ptr | _ \<Rightarrow> g)
   = (if isThreadCap cap
      then f (capTCBPtr cap)
      else g)" by (simp add: isCap_simps
         split: capability.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.ThreadCap ptr \<Rightarrow> f ptr | _ \<Rightarrow> g) = (if isThreadCap cap then f (capTCBPtr cap) else g)
theory Invoke_C

lemma active_runnable':
  "active' state \<Longrightarrow> runnable' state" by (fastforce simp: runnable'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. active' state \<Longrightarrow> runnable' state
theory Invoke_C

lemma updateCapData_spec2:
  "\<forall>cap preserve newData. \<Gamma> \<turnstile> \<lbrace> ccap_relation cap \<acute>cap \<and> preserve = to_bool (\<acute>preserve) \<and> newData = \<acute>newData\<rbrace>
  Call updateCapData_'proc
  \<lbrace>  ccap_relation (updateCapData preserve newData cap) \<acute>ret__struct_cap_C \<rbrace>" by (simp add: updateCapData_spec)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>cap preserve newData. \<Gamma>\<turnstile> \<lbrace>ccap_relation cap \<acute>cap \<and> preserve = to_bool \<acute>preserve \<and> newData = \<acute>newData\<rbrace> Call updateCapData_'proc \<lbrace>ccap_relation (global.updateCapData preserve newData cap) \<acute>ret__struct_cap_C\<rbrace>
theory Invoke_C

lemma ccorres_add_specific_return:
  "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs
        (do v \<leftarrow> return val; f v od) c
   \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (f val) c" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (return val >>= f) c \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (f val) c
theory Invoke_C

lemma ccorres_subgoal_tailE:
  "\<lbrakk> ccorres rvr xf Q Q' hs (b ()) d;
      ccorres rvr xf Q Q' hs (b ()) d \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d) \<rbrakk>
        \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c ;; d)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres rvr xf Q Q' hs (b ()) d; ccorres rvr xf Q Q' hs (b ()) d \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c;;
d)\<rbrakk> \<Longrightarrow> ccorres rvr xf P P' hs (a >>=E b) (c;;
d)
theory Invoke_C

lemma cnode_invok_case_cleanup2:
  "i \<in> set [CNodeCopy .e. CNodeMutate] \<Longrightarrow>
     (case i of CNodeRevoke \<Rightarrow> P | CNodeDelete \<Rightarrow> Q | CNodeCancelBadgedSends \<Rightarrow> R
              | CNodeRotate \<Rightarrow> S | CNodeSaveCaller \<Rightarrow> T | _ \<Rightarrow> U) = U" apply (rule cnode_invok_case_cleanup) apply (simp add: upto_enum_def fromEnum_def toEnum_def
                   enum_invocation_label enum_gen_invocation_labels) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i \<in> set [gen_invocation_labels.CNodeCopy .e. gen_invocation_labels.CNodeMutate] \<Longrightarrow> (case i of gen_invocation_labels.CNodeRevoke \<Rightarrow> P | gen_invocation_labels.CNodeDelete \<Rightarrow> Q | gen_invocation_labels.CNodeCancelBadgedSends \<Rightarrow> R | gen_invocation_labels.CNodeRotate \<Rightarrow> S | gen_invocation_labels.CNodeSaveCaller \<Rightarrow> T | _ \<Rightarrow> U) = U proof (prove)
goal (1 subgoal):
 1. i \<in> set [gen_invocation_labels.CNodeCopy .e. gen_invocation_labels.CNodeMutate] \<Longrightarrow> i \<notin> {gen_invocation_labels.CNodeRevoke, gen_invocation_labels.CNodeDelete, gen_invocation_labels.CNodeCancelBadgedSends, gen_invocation_labels.CNodeRotate, gen_invocation_labels.CNodeSaveCaller} proof (prove)
goal (1 subgoal):
 1. i = gen_invocation_labels.CNodeCopy \<or> i = gen_invocation_labels.CNodeMint \<or> i = gen_invocation_labels.CNodeMove \<or> i = gen_invocation_labels.CNodeMutate \<Longrightarrow> i \<noteq> gen_invocation_labels.CNodeRevoke \<and> i \<noteq> gen_invocation_labels.CNodeDelete \<and> i \<noteq> gen_invocation_labels.CNodeCancelBadgedSends \<and> i \<noteq> gen_invocation_labels.CNodeRotate \<and> i \<noteq> gen_invocation_labels.CNodeSaveCaller proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma deleteObjects_gsCNodes_at_pt:
  "\<lbrace>(\<lambda>s. P (gsCNodes s ptr))
      and K (ptr \<notin> {ptr_base .. ptr_base + 2 ^ sz - 1} \<and> is_aligned ptr_base sz)\<rbrace>
    deleteObjects ptr_base sz
       \<lbrace>\<lambda>rv s. P (gsCNodes s ptr)\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: deleteObjects_def2) apply (wp | simp cong: conj_cong
        | wp (once) hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (gsCNodes s ptr)) and K (ptr \<notin> {ptr_base..ptr_base + 2 ^ sz - 1} \<and> is_aligned ptr_base sz)\<rbrace> deleteObjects ptr_base sz \<lbrace>\<lambda>rv s. P (gsCNodes s ptr)\<rbrace> proof (prove)
goal (1 subgoal):
 1. ptr \<notin> {ptr_base..ptr_base + 2 ^ sz - 1} \<and> is_aligned ptr_base sz \<Longrightarrow> \<lbrace>\<lambda>s. P (gsCNodes s ptr)\<rbrace> deleteObjects ptr_base sz \<lbrace>\<lambda>rv s. P (gsCNodes s ptr)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (ptr_base \<le> ptr \<longrightarrow> \<not> ptr \<le> ptr_base + 2 ^ sz - 1) \<and> is_aligned ptr_base sz \<Longrightarrow> \<lbrace>\<lambda>s. P (gsCNodes s ptr)\<rbrace> do y <- stateAssert (deletionIsSafe ptr_base sz) [];
y <- doMachineOp (freeMemory ptr_base sz);
y <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr_base \<le> x \<and> x \<le> ptr_base + 2 ^ sz - 1)) [];
y <- modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if ptr_base \<le> x \<and> x \<le> ptr_base + 2 ^ sz - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr_base \<le> x \<and> x \<le> ptr_base + 2 ^ sz - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr_base \<le> x \<and> x \<le> ptr_base + 2 ^ sz - 1 then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>rv s. P (gsCNodes s ptr)\<rbrace> proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma range_cover_compare_bound_word:
  "range_cover ptr sz sbit n
    \<Longrightarrow> (of_nat n * 2 ^ sbit) + (ptr && mask sz) \<le> 2 ^ sz" apply (simp add: word_le_nat_alt range_cover_unat
                   add.commute) apply (frule range_cover.range_cover_compare_bound) apply (simp add: range_cover.sz range_cover.unat_of_nat_shift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz sbit n \<Longrightarrow> word_of_nat n * 2 ^ sbit + (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz sbit n \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ sbit) \<le> unat (2 ^ sz) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n * 2 ^ sbit) \<le> unat (2 ^ sz) proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma t_hrs_update_use_t_hrs:
  "t_hrs_'_update f s
    = (t_hrs_'_update (\<lambda>_. f (t_hrs_' s)) $ s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_'_update f s = (t_hrs_'_update (\<lambda>_. f (t_hrs_' s)) $ s)
theory Invoke_C

lemma typ_region_bytes_dom_s:
  "S \<subseteq> {ptr ..+ 2 ^ bits}
    \<Longrightarrow> S \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (typ_region_bytes ptr bits htd)" apply (clarsimp simp: typ_region_bytes_def dom_s_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> {ptr..+2 ^ bits} \<Longrightarrow> S \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (typ_region_bytes ptr bits htd) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>S \<subseteq> {ptr..+2 ^ bits}; \<forall>n. b = SIndexTyp n \<longrightarrow> snd (if a \<in> {ptr..+2 ^ bits} then (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) else htd a) n = None; a \<in> S; b = SIndexVal \<or> b = SIndexTyp 0\<rbrakk> \<Longrightarrow> b = SIndexVal \<and> fst (if a \<in> {ptr..+2 ^ bits} then (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) else htd a) proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma aligned_intvl_offset_subset:
  assumes al: "is_aligned (ptr :: 'a :: len word) sz" and al': "is_aligned x sz'"
  and     szv: "sz' \<le> sz" and xsz: "x < 2 ^ sz"
  shows       "{ptr + x ..+ 2 ^ sz'} \<subseteq> {ptr ..+ 2 ^ sz}" apply (simp only: upto_intvl_eq al aligned_add_aligned[OF al al' szv]) apply (rule aligned_range_offset_subset[OF al al' szv xsz]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {ptr + x..+2 ^ sz'} \<subseteq> {ptr..+2 ^ sz} proof (prove)
goal (1 subgoal):
 1. {ptr + x..ptr + x + 2 ^ sz' - 1} \<subseteq> {ptr..ptr + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma aligned_intvl_offset_subset_ran:
  assumes al: "is_aligned (ptr :: 'a :: len word) sz" and al': "is_aligned x sz'"
  and     szv: "sz' \<le> sz" and xsz: "x < 2 ^ sz"
  shows       "{ptr + x ..+ 2 ^ sz'} \<subseteq> {ptr .. ptr + 2 ^ sz - 1}" apply (simp only: upto_intvl_eq al aligned_add_aligned[OF al al' szv]) apply (rule aligned_range_offset_subset[OF al al' szv xsz]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {ptr + x..+2 ^ sz'} \<subseteq> {ptr..ptr + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. {ptr + x..ptr + x + 2 ^ sz' - 1} \<subseteq> {ptr..ptr + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma ccorres_req_Ex:
  assumes v: "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; s' \<in> P' \<rbrakk> \<Longrightarrow> \<exists>v. Q v s \<and> Q' v s' \<and> V v"
  and cc: "\<And>v. V v \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (P and Q v) (P' \<inter> {s. Q' v s}) hs H C"
  shows "ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H C" apply (rule ccorres_name_pre) apply (rule ccorres_name_pre_C) apply (case_tac "(s, sa) \<in> sr") apply (drule(2) v, clarsimp) apply (rule ccorres_guard_imp2, erule cc) apply auto[1] apply (rule ccorresI', simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf r' xf' P P' hs H C proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) P' hs H C proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>P s; sa \<in> P'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) {sa} hs H C proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>P s; sa \<in> P'; (s, sa) \<in> sr\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) {sa} hs H C
 2. \<And>s sa. \<lbrakk>P s; sa \<in> P'; (s, sa) \<notin> sr\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) {sa} hs H C proof (prove)
goal (2 subgoals):
 1. \<And>s sa v. \<lbrakk>P s; sa \<in> P'; Q v s; Q' v sa; V v\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) {sa} hs H C
 2. \<And>s sa. \<lbrakk>P s; sa \<in> P'; (s, sa) \<notin> sr\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) {sa} hs H C proof (prove)
goal (2 subgoals):
 1. \<And>s sa v sb s'. \<lbrakk>P s; sa \<in> P'; Q v s; Q' v sa; V v; (sb, s') \<in> sr; sb = s; s' \<in> {sa}\<rbrakk> \<Longrightarrow> (P and Q v) sb \<and> s' \<in> P' \<inter> {s. Q' v s}
 2. \<And>s sa. \<lbrakk>P s; sa \<in> P'; (s, sa) \<notin> sr\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) {sa} hs H C proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>P s; sa \<in> P'; (s, sa) \<notin> sr\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf r' xf' (\<lambda>s'. s' = s) {sa} hs H C proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma region_actually_is_bytes_subset_t_hrs:
  "region_actually_is_bytes ptr sz s'
    \<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz}
    \<Longrightarrow> t_hrs_' (globals s') = t_hrs_' (globals s)
    \<Longrightarrow> region_actually_is_bytes ptr' sz' s" by (auto simp: region_actually_is_bytes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>region_actually_is_bytes ptr sz s'; {ptr'..+sz'} \<subseteq> {ptr..+sz}; t_hrs_' (globals s') = t_hrs_' (globals s)\<rbrakk> \<Longrightarrow> region_actually_is_bytes ptr' sz' s
theory Invoke_C

lemma cleanByVA_preserves_bytes:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanByVA_'proc
      {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
         \<and> byte_regions_unmodified' s t}" apply (rule allI, rule conseqPost,
    rule cleanByVA_preserves_kernel_bytes[rule_format]) apply simp_all apply (clarsimp simp: byte_regions_unmodified_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanByVA_'proc \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> (\<forall>x. snd (hrs_htd \<^bsup>s\<^esup>t_hrs x) 0 \<noteq> None \<longrightarrow> hrs_mem \<acute>t_hrs x = hrs_mem \<^bsup>s\<^esup>t_hrs x)\<rbrace> \<subseteq> \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace>
 2. \<And>s. {} \<subseteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> (\<forall>x. (\<exists>a b. snd (hrs_htd \<^bsup>s\<^esup>t_hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem \<acute>t_hrs x = hrs_mem \<^bsup>s\<^esup>t_hrs x)\<rbrace> \<subseteq> \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma cleanL2Range_preserves_bytes:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call plat_cleanL2Range_'proc
      {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
         \<and> byte_regions_unmodified' s t}" apply (rule allI, rule conseqPost, rule cleanL2Range_preserves_kernel_bytes[rule_format]; simp) apply (clarsimp simp: byte_regions_unmodified_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call plat_cleanL2Range_'proc \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> (\<forall>x. (\<exists>a b. snd (hrs_htd \<^bsup>s\<^esup>t_hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem \<acute>t_hrs x = hrs_mem \<^bsup>s\<^esup>t_hrs x)\<rbrace> \<subseteq> \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma dsb_preserves_bytes:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call dsb_'proc
      {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
         \<and> byte_regions_unmodified' s t}" apply (rule allI, rule conseqPost, rule dsb_preserves_kernel_bytes[rule_format]; simp) apply (clarsimp simp: byte_regions_unmodified_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call dsb_'proc \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> (\<forall>x. (\<exists>a b. snd (hrs_htd \<^bsup>s\<^esup>t_hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem \<acute>t_hrs x = hrs_mem \<^bsup>s\<^esup>t_hrs x)\<rbrace> \<subseteq> \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma zero_bytes_heap_update:
  "heap_list_is_zero (hrs_mem hrs) ptr n
    \<Longrightarrow> region_is_bytes' ptr n (hrs_htd hrs)
    \<Longrightarrow> h_t_valid (hrs_htd hrs) c_guard (cptr :: 'a ptr)
    \<Longrightarrow> typ_uinfo_t TYPE ('a :: mem_type) \<noteq> typ_uinfo_t TYPE(8 word)
    \<Longrightarrow> heap_list_is_zero (heap_update cptr v (hrs_mem hrs)) ptr n" apply (frule(2) region_is_bytes_disjoint) apply (clarsimp simp: heap_update_def) apply (subst heap_list_update_disjoint_same, simp_all) apply (simp add: Int_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_list (hrs_mem hrs) n ptr = replicate n 0; region_is_bytes' ptr n (hrs_htd hrs); hrs_htd hrs \<Turnstile>\<^sub>t cptr; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> heap_list (heap_update cptr v (hrs_mem hrs)) n ptr = replicate n 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_list (hrs_mem hrs) n ptr = replicate n 0; region_is_bytes' ptr n (hrs_htd hrs); hrs_htd hrs \<Turnstile>\<^sub>t cptr; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); {ptr..+n} \<inter> ptr_span cptr = {}\<rbrakk> \<Longrightarrow> heap_list (heap_update cptr v (hrs_mem hrs)) n ptr = replicate n 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_list (hrs_mem hrs) n ptr = replicate n 0; region_is_bytes' ptr n (hrs_htd hrs); hrs_htd hrs \<Turnstile>\<^sub>t cptr; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); {ptr..+n} \<inter> ptr_span cptr = {}\<rbrakk> \<Longrightarrow> heap_list (heap_update_list (ptr_val cptr) (to_bytes v (heap_list (hrs_mem hrs) (size_of TYPE('a)) (ptr_val cptr))) (hrs_mem hrs)) n ptr = replicate n 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_list (hrs_mem hrs) n ptr = replicate n 0; region_is_bytes' ptr n (hrs_htd hrs); hrs_htd hrs \<Turnstile>\<^sub>t cptr; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); {ptr..+n} \<inter> ptr_span cptr = {}\<rbrakk> \<Longrightarrow> ptr_span cptr \<inter> {ptr..+n} = {} proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma injection_handler_sequenceE:
  "injection_handler injf (sequenceE xs)
    = sequenceE (map (injection_handler injf) xs)" apply (induct xs, simp_all add: sequenceE_def) apply (simp add: injection_handler_returnOk) apply (simp add: injection_bindE[OF refl refl]
                   injection_handler_returnOk
                   Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler injf (sequenceE xs) = sequenceE (map (injection_handler injf) xs) proof (prove)
goal (2 subgoals):
 1. injection_handler injf (returnOk []) = returnOk []
 2. \<And>x1 xs. injection_handler injf (foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) xs (returnOk [])) = foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map (injection_handler injf) xs) (returnOk []) \<Longrightarrow> injection_handler injf (doE x <- x1;
y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) xs (returnOk []);
returnOk (x # y)
odE) = doE x <- injection_handler injf x1;
y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map (injection_handler injf) xs) (returnOk []);
returnOk (x # y)
odE proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. injection_handler injf (foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) xs (returnOk [])) = foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map (injection_handler injf) xs) (returnOk []) \<Longrightarrow> injection_handler injf (doE x <- x1;
y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) xs (returnOk []);
returnOk (x # y)
odE) = doE x <- injection_handler injf x1;
y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map (injection_handler injf) xs) (returnOk []);
returnOk (x # y)
odE proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma capCNodeRadix_CL_less_32:
  "cap_get_tag ccap = scast cap_cnode_cap \<Longrightarrow> capCNodeRadix_CL (cap_cnode_cap_lift ccap) < 32" apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap) apply (rule order_le_less_trans, rule word_and_le1) apply (simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<Longrightarrow> capCNodeRadix_CL (cap_cnode_cap_lift ccap) < 0x20 proof (prove)
goal (1 subgoal):
 1. cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<Longrightarrow> (cap_C.words_C ccap.[Suc 0] >> 18) && mask 5 < 0x20 proof (prove)
goal (1 subgoal):
 1. cap_get_tag ccap = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<Longrightarrow> mask 5 < 0x20 proof (prove)
goal:
No subgoals!
theory Invoke_C

lemma TripleSuc:
  "Suc (Suc (Suc 0)) = 3" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc (Suc (Suc 0)) = 3
theory Invoke_C

lemma case_sum_distrib:
  "case_sum a b x >>= f = case_sum (\<lambda>x. a x >>= f) (\<lambda>x. b x >>= f) x" by (case_tac x,simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case x of Inl x \<Rightarrow> a x | Inr x \<Rightarrow> b x) >>= f = (case x of Inl x \<Rightarrow> a x >>= f | Inr x \<Rightarrow> b x >>= f)