kings-crown/FVELER_Isabelle huggingface dataset:
theory SR_lemmas_C

lemma update_ep_map_tos:
  fixes P :: "endpoint \<Rightarrow> bool"
  assumes at: "obj_at' P p s"
  shows   "map_to_ntfns ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_ntfns (ksPSpace s)"
  and     "map_to_tcbs ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_tcbs (ksPSpace s)"
  and     "map_to_ctes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_ctes (ksPSpace s)"
  and     "map_to_pdes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_pdes (ksPSpace s)"
  and     "map_to_ptes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_ptes (ksPSpace s)"
  and     "map_to_asidpools ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_asidpools (ksPSpace s)"
  and     "map_to_user_data ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_user_data (ksPSpace s)"
  and     "map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_user_data_device (ksPSpace s)" using at by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
    simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((map_to_ntfns ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_ntfns (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = ctes_of s &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_pdes (ksPSpace s)) &&& (map_to_ptes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_ptes (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_user_data_device (ksPSpace s) proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. ((map_to_ntfns ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_ntfns (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = ctes_of s &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_pdes (ksPSpace s)) &&& (map_to_ptes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_ptes (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_user_data_device (ksPSpace s)
theory SR_lemmas_C

lemma update_tcb_map_tos:
  fixes P :: "tcb \<Rightarrow> bool"
  assumes at: "obj_at' P p s"
  shows   "map_to_eps ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_eps (ksPSpace s)"
  and     "map_to_ntfns ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_ntfns (ksPSpace s)"
  and     "map_to_pdes ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_pdes (ksPSpace s)"
  and     "map_to_ptes ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_ptes (ksPSpace s)"
  and     "map_to_asidpools ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_asidpools (ksPSpace s)"
  and     "map_to_user_data ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_user_data (ksPSpace s)"
  and     "map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_user_data_device (ksPSpace s)" using at by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
    simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (map_to_eps ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_eps (ksPSpace s) &&& map_to_ntfns ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_ntfns (ksPSpace s) &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_pdes (ksPSpace s)) &&& (map_to_ptes ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_ptes (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_user_data_device (ksPSpace s) proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. (map_to_eps ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_eps (ksPSpace s) &&& map_to_ntfns ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_ntfns (ksPSpace s) &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_pdes (ksPSpace s)) &&& (map_to_ptes ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_ptes (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOTCB ko)) = map_to_user_data_device (ksPSpace s)
theory SR_lemmas_C

lemma update_asidpool_map_tos:
  fixes P :: "asidpool \<Rightarrow> bool"
  assumes at: "obj_at' P p s"
  shows   "map_to_ntfns ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ntfns (ksPSpace s)"
  and     "map_to_tcbs ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_tcbs (ksPSpace s)"
  and     "map_to_ctes ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ctes (ksPSpace s)"
  and     "map_to_pdes ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_pdes (ksPSpace s)"
  and     "map_to_ptes ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ptes (ksPSpace s)"
  and     "map_to_eps  ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_eps (ksPSpace s)"
  and     "map_to_user_data ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data (ksPSpace s)"
  and     "map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data_device (ksPSpace s)" using at by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
      simp: projectKOs projectKO_opts_defs
     split: if_split if_split_asm Structures_H.kernel_object.split_asm
            arch_kernel_object.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((map_to_ntfns ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ntfns (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = ctes_of s &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_pdes (ksPSpace s)) &&& (map_to_ptes ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ptes (ksPSpace s) &&& map_to_eps ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_eps (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data_device (ksPSpace s) proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. ((map_to_ntfns ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ntfns (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = ctes_of s &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_pdes (ksPSpace s)) &&& (map_to_ptes ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ptes (ksPSpace s) &&& map_to_eps ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_eps (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data_device (ksPSpace s)
theory SR_lemmas_C

lemma update_asidpool_map_to_asidpools:
  "map_to_asidpools ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap)))
             = (map_to_asidpools (ksPSpace s))(p \<mapsto> ap)" by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_asidpools ((ksPSpace s)(p \<mapsto> KOArch (KOASIDPool ap))) = (map_to_asidpools (ksPSpace s))(p \<mapsto> ap)
theory SR_lemmas_C

lemma update_pte_map_to_ptes:
  "map_to_ptes ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte)))
             = (map_to_ptes (ksPSpace s))(p \<mapsto> pte)" by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_ptes ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = (map_to_ptes (ksPSpace s))(p \<mapsto> pte)
theory SR_lemmas_C

lemma update_pte_map_tos:
  fixes P :: "pte \<Rightarrow> bool"
  assumes at: "obj_at' P p s"
  shows   "map_to_ntfns ((ksPSpace s)(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_ntfns (ksPSpace s)"
  and     "map_to_tcbs ((ksPSpace s)(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_tcbs (ksPSpace s)"
  and     "map_to_ctes ((ksPSpace s)(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_ctes (ksPSpace s)"
  and     "map_to_pdes ((ksPSpace s)(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_pdes (ksPSpace s)"
  and     "map_to_eps  ((ksPSpace s)(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_eps (ksPSpace s)"
  and     "map_to_asidpools ((ksPSpace s)(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_asidpools (ksPSpace s)"
  and     "map_to_user_data ((ksPSpace s)(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_user_data (ksPSpace s)"
  and     "map_to_user_data_device ((ksPSpace s)(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_user_data_device (ksPSpace s)" using at by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other
           split: if_split_asm if_split
            simp: projectKOs,
       auto simp: projectKO_opts_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((map_to_ntfns ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_ntfns (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = ctes_of s &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_pdes (ksPSpace s)) &&& (map_to_eps ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_eps (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_user_data_device (ksPSpace s) proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. ((map_to_ntfns ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_ntfns (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = ctes_of s &&& map_to_pdes ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_pdes (ksPSpace s)) &&& (map_to_eps ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_eps (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOArch (KOPTE pte))) = map_to_user_data_device (ksPSpace s)
theory SR_lemmas_C

lemma update_pde_map_to_pdes:
  "map_to_pdes ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde)))
             = (map_to_pdes (ksPSpace s))(p \<mapsto> pde)" by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_pdes ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = (map_to_pdes (ksPSpace s))(p \<mapsto> pde)
theory SR_lemmas_C

lemma update_pde_map_tos:
  fixes P :: "pde \<Rightarrow> bool"
  assumes at: "obj_at' P p s"
  shows   "map_to_ntfns ((ksPSpace s)(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_ntfns (ksPSpace s)"
  and     "map_to_tcbs ((ksPSpace s)(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_tcbs (ksPSpace s)"
  and     "map_to_ctes ((ksPSpace s)(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_ctes (ksPSpace s)"
  and     "map_to_ptes ((ksPSpace s)(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_ptes (ksPSpace s)"
  and     "map_to_eps  ((ksPSpace s)(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_eps (ksPSpace s)"
  and     "map_to_asidpools ((ksPSpace s)(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_asidpools (ksPSpace s)"
  and     "map_to_user_data ((ksPSpace s)(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_user_data (ksPSpace s)"
  and     "map_to_user_data_device ((ksPSpace s)(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_user_data_device (ksPSpace s)" using at by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other
           split: if_split_asm if_split
            simp: projectKOs,
       auto simp: projectKO_opts_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((map_to_ntfns ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_ntfns (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = ctes_of s &&& map_to_ptes ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_ptes (ksPSpace s)) &&& (map_to_eps ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_eps (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_user_data_device (ksPSpace s) proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. ((map_to_ntfns ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_ntfns (ksPSpace s) &&& map_to_tcbs ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_tcbs (ksPSpace s)) &&& map_to_ctes ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = ctes_of s &&& map_to_ptes ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_ptes (ksPSpace s)) &&& (map_to_eps ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_eps (ksPSpace s) &&& map_to_asidpools ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_asidpools (ksPSpace s)) &&& map_to_user_data ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_user_data (ksPSpace s) &&& map_to_user_data_device ((ksPSpace s)(p \<mapsto> KOArch (KOPDE pde))) = map_to_user_data_device (ksPSpace s)
theory SR_lemmas_C

lemma heap_to_page_data_cong [cong]:
  "\<lbrakk> map_to_user_data ks = map_to_user_data ks'; bhp = bhp' \<rbrakk>
  \<Longrightarrow> heap_to_user_data ks bhp = heap_to_user_data ks' bhp'" unfolding heap_to_user_data_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_to_user_data ks = map_to_user_data ks'; bhp = bhp'\<rbrakk> \<Longrightarrow> heap_to_user_data ks bhp = heap_to_user_data ks' bhp' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_to_user_data ks = map_to_user_data ks'; bhp = bhp'\<rbrakk> \<Longrightarrow> (\<lambda>p. let uhp = map_to_user_data ks in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p)) = (\<lambda>p. let uhp = map_to_user_data ks' in map_option (\<lambda>_. byte_to_word_heap bhp' p) (uhp p))
theory SR_lemmas_C

lemma map_leD:
  "\<lbrakk> map_le m m'; m x = Some y \<rbrakk> \<Longrightarrow> m' x = Some y" by (simp add: map_le_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<subseteq>\<^sub>m m'; m x = Some y\<rbrakk> \<Longrightarrow> m' x = Some y
theory SR_lemmas_C

lemma region_actually_is_bytes:
  "region_actually_is_bytes' ptr len htd
    \<Longrightarrow> region_is_bytes' ptr len htd" by (simp add: region_is_bytes'_def region_actually_is_bytes'_def
         split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. region_actually_is_bytes' ptr len htd \<Longrightarrow> region_is_bytes' ptr len htd
theory SR_lemmas_C

lemma zero_ranges_are_zero_update[simp]:
  "h_t_valid (hrs_htd hrs) c_guard (ptr :: 'a ptr)
    \<Longrightarrow> typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8)
    \<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_update ptr v) hrs)
        = zero_ranges_are_zero rs hrs" apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update
        intro!: ball_cong[OF refl] conj_cong[OF refl]) apply (drule region_actually_is_bytes) apply (drule(2) region_is_bytes_disjoint) apply (simp add: heap_update_def heap_list_update_disjoint_same Int_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hrs_htd hrs \<Turnstile>\<^sub>t ptr; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word)\<rbrakk> \<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_update ptr v) hrs) = zero_ranges_are_zero rs hrs proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>hrs_htd hrs \<Turnstile>\<^sub>t ptr; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); (a, b) \<in> rs; region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs)\<rbrakk> \<Longrightarrow> (heap_list (heap_update ptr v (hrs_mem hrs)) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) = (heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>hrs_htd hrs \<Turnstile>\<^sub>t ptr; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); (a, b) \<in> rs; region_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs)\<rbrakk> \<Longrightarrow> (heap_list (heap_update ptr v (hrs_mem hrs)) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) = (heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>hrs_htd hrs \<Turnstile>\<^sub>t ptr; typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE(8 word); (a, b) \<in> rs; {a..+unat (b + 1 - a)} \<inter> {ptr_val ptr..+size_of TYPE('a)} = {}\<rbrakk> \<Longrightarrow> (heap_list (heap_update ptr v (hrs_mem hrs)) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) = (heap_list (hrs_mem hrs) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma inj_tcb_ptr_to_ctcb_ptr [simp]:
  "inj tcb_ptr_to_ctcb_ptr" apply (rule injI) apply (simp add: tcb_ptr_to_ctcb_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj tcb_ptr_to_ctcb_ptr proof (prove)
goal (1 subgoal):
 1. \<And>x y. tcb_ptr_to_ctcb_ptr x = tcb_ptr_to_ctcb_ptr y \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma obj_at_cslift_tcb:
  fixes P :: "tcb \<Rightarrow> bool"
  shows "\<lbrakk>obj_at' P thread s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow>
  \<exists>ko ko'. ko_at' ko thread s \<and> P ko \<and>
        cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and>
        ctcb_relation ko ko'" apply (frule obj_at_ko_at') apply clarsimp apply (frule cmap_relation_tcb) apply (drule (1) cmap_relation_ko_atD) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P thread s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>ko ko'. ko_at' ko thread s \<and> P ko \<and> cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P thread s; (s, s') \<in> rf_sr; \<exists>ko. ko_at' ko thread s \<and> P ko\<rbrakk> \<Longrightarrow> \<exists>ko ko'. ko_at' ko thread s \<and> P ko \<and> cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko' proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>obj_at' P thread s; (s, s') \<in> rf_sr; ko_at' ko thread s; P ko\<rbrakk> \<Longrightarrow> \<exists>ko. ko_at' ko thread s \<and> P ko \<and> (\<exists>ko'. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko') proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>obj_at' P thread s; (s, s') \<in> rf_sr; ko_at' ko thread s; P ko; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation\<rbrakk> \<Longrightarrow> \<exists>ko. ko_at' ko thread s \<and> P ko \<and> (\<exists>ko'. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko') proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>obj_at' P thread s; (s, s') \<in> rf_sr; ko_at' ko thread s; P ko; \<exists>ko'. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> \<exists>ko. ko_at' ko thread s \<and> P ko \<and> (\<exists>ko'. cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> ctcb_relation ko ko') proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma ctcb_relation_thread_state_to_tsType:
  "ctcb_relation tcb ctcb \<Longrightarrow> tsType_CL (thread_state_lift (tcbState_C ctcb)) = thread_state_to_tsType (tcbState tcb)" unfolding ctcb_relation_def cthread_state_relation_def by (cases "(tcbState tcb)", simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_relation tcb ctcb \<Longrightarrow> tsType_CL (thread_state_lift (tcbState_C ctcb)) = thread_state_to_tsType (tcbState tcb) proof (prove)
goal (1 subgoal):
 1. tcbFaultHandler tcb = tcbFaultHandler_C ctcb \<and> (case (tcbState_C ctcb, tcbFault_C ctcb) of (cs, cf) \<Rightarrow> cthread_state_relation_lifted (tcbState tcb) (thread_state_lift cs, seL4_Fault_lift cf)) \<and> tcbIPCBuffer tcb = tcbIPCBuffer_C ctcb \<and> carch_tcb_relation (tcbArch tcb) (tcbArch_C ctcb) \<and> tcbQueued tcb = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ctcb))) \<and> UCAST(8 \<rightarrow> 32) (tcbDomain tcb) = tcbDomain_C ctcb \<and> UCAST(8 \<rightarrow> 32) (tcbPriority tcb) = tcbPriority_C ctcb \<and> UCAST(8 \<rightarrow> 32) (tcbMCP tcb) = tcbMCP_C ctcb \<and> tcbTimeSlice tcb = unat (tcbTimeSlice_C ctcb) \<and> cfault_rel (tcbFault tcb) (seL4_Fault_lift (tcbFault_C ctcb)) (lookup_fault_lift (tcbLookupFailure_C ctcb)) \<and> option_to_ptr (tcbBoundNotification tcb) = tcbBoundNotification_C ctcb \<Longrightarrow> tsType_CL (thread_state_lift (tcbState_C ctcb)) = thread_state_to_tsType (tcbState tcb)
theory SR_lemmas_C

lemma ctcb_ptr_to_ctcb_ptr [simp]:
  "ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr x) = x" unfolding ctcb_ptr_to_tcb_ptr_def tcb_ptr_to_ctcb_ptr_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr x) = x proof (prove)
goal (1 subgoal):
 1. ptr_val (tcb_Ptr (x + ctcb_offset)) - ctcb_offset = x
theory SR_lemmas_C

lemma cmap_relation_updI2:
  fixes am :: "word32 \<rightharpoonup> 'a" and cm :: "'b typ_heap"
  assumes cr: "cmap_relation am cm f rel"
  and   cof: "am dest = None"
  and   cc:  "rel nv nv'"
  and   inj: "inj f"
  shows "cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel" using cr cof cc inj by (clarsimp simp add: cmap_relation_def inj_eq split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel proof (prove)
using this:
cmap_relation am cm f rel
am dest = None
rel nv nv'
inj f

goal (1 subgoal):
 1. cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel
theory SR_lemmas_C

lemma rf_sr_heap_user_data_relation:
  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation
      (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s)))
      (cslift s') Ptr cuser_user_data_relation" by (clarsimp simp: user_word_at_def rf_sr_def
                     cstate_relation_def Let_def
                     cpspace_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation