kings-crown/FVELER_Isabelle huggingface dataset:
theory SR_lemmas_C

lemma mdb_node_to_H_mdbFirstBadged_update[simp]:
  "mdb_node_to_H (mdbFirstBadged_CL_update (\<lambda>_. x) m)
  = mdbFirstBadged_update (\<lambda>_. to_bool x) (mdb_node_to_H m)" unfolding mdb_node_to_H_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_node_to_H (m\<lparr>mdbFirstBadged_CL := x\<rparr>) = mdbFirstBadged_update (\<lambda>_. to_bool x) (mdb_node_to_H m) proof (prove)
goal (1 subgoal):
 1. MDB (mdbNext_CL (m\<lparr>mdbFirstBadged_CL := x\<rparr>)) (mdbPrev_CL (m\<lparr>mdbFirstBadged_CL := x\<rparr>)) (to_bool (mdbRevocable_CL (m\<lparr>mdbFirstBadged_CL := x\<rparr>))) (to_bool (mdbFirstBadged_CL (m\<lparr>mdbFirstBadged_CL := x\<rparr>))) = mdbFirstBadged_update (\<lambda>_. to_bool x) (MDB (mdbNext_CL m) (mdbPrev_CL m) (to_bool (mdbRevocable_CL m)) (to_bool (mdbFirstBadged_CL m)))
theory SR_lemmas_C

lemma mdbNext_to_H [simp]:
  "mdbNext (mdb_node_to_H n) = mdbNext_CL n" unfolding mdb_node_to_H_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext (mdb_node_to_H n) = mdbNext_CL n proof (prove)
goal (1 subgoal):
 1. mdbNext (MDB (mdbNext_CL n) (mdbPrev_CL n) (to_bool (mdbRevocable_CL n)) (to_bool (mdbFirstBadged_CL n))) = mdbNext_CL n
theory SR_lemmas_C

lemma mdbPrev_to_H [simp]:
  "mdbPrev (mdb_node_to_H n) = mdbPrev_CL n" unfolding mdb_node_to_H_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev (mdb_node_to_H n) = mdbPrev_CL n proof (prove)
goal (1 subgoal):
 1. mdbPrev (MDB (mdbNext_CL n) (mdbPrev_CL n) (to_bool (mdbRevocable_CL n)) (to_bool (mdbFirstBadged_CL n))) = mdbPrev_CL n
theory SR_lemmas_C

lemma cte_bits_le_3 [simp]: "3 \<le> cte_level_bits" by (simp add: objBits_defs cte_level_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 3 \<le> cte_level_bits
theory SR_lemmas_C

lemma cte_bits_le_tcb_bits: "cte_level_bits \<le> tcbBlockSizeBits" by (simp add: cte_level_bits_def objBits_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_level_bits \<le> tcbBlockSizeBits
theory SR_lemmas_C

lemma mdbNext_not_zero_eq:
  "cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<comment> \<open>*ja \<and> (is_aligned (mdbNext n) 3)\<close>
  \<longrightarrow> (mdbNext n \<noteq> 0) = (s' \<in> {_. mdbNext_CL (mdb_node_lift n') \<noteq> 0})" apply clarsimp apply (erule cmdbnode_relationE) apply (fastforce simp: mdbNext_to_H) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<longrightarrow> (mdbNext n \<noteq> 0) = (s' \<in> \<lbrace>mdbNext_CL (mdb_node_lift n') \<noteq> 0\<rbrace>) proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> (0 < mdbNext_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> 0 < mdbNext n) \<and> (\<not> 0 < mdbNext_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> \<not> 0 < mdbNext n) proof (prove)
goal (1 subgoal):
 1. n = mdb_node_to_H (mdb_node_lift n') \<Longrightarrow> (0 < mdbNext_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> 0 < mdbNext n) \<and> (\<not> 0 < mdbNext_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> \<not> 0 < mdbNext n) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma mdbPrev_not_zero_eq:
  "cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<comment> \<open>ja\<and> (is_aligned (mdbPrev n) 3)\<close>
  \<longrightarrow> (mdbPrev n \<noteq> 0) = (s' \<in> {_. mdbPrev_CL (mdb_node_lift n') \<noteq> 0})" apply clarsimp apply (erule cmdbnode_relationE) apply (unfold mdb_node_to_H_def) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<longrightarrow> (mdbPrev n \<noteq> 0) = (s' \<in> \<lbrace>mdbPrev_CL (mdb_node_lift n') \<noteq> 0\<rbrace>) proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> (0 < mdbPrev_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> 0 < mdbPrev n) \<and> (\<not> 0 < mdbPrev_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> \<not> 0 < mdbPrev n) proof (prove)
goal (1 subgoal):
 1. n = mdb_node_to_H (mdb_node_lift n') \<Longrightarrow> (0 < mdbPrev_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> 0 < mdbPrev n) \<and> (\<not> 0 < mdbPrev_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> \<not> 0 < mdbPrev n) proof (prove)
goal (1 subgoal):
 1. n = MDB (mdbNext_CL (mdb_node_lift n')) (mdbPrev_CL (mdb_node_lift n')) (to_bool (mdbRevocable_CL (mdb_node_lift n'))) (to_bool (mdbFirstBadged_CL (mdb_node_lift n'))) \<Longrightarrow> (0 < mdbPrev_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> 0 < mdbPrev n) \<and> (\<not> 0 < mdbPrev_CL (mdb_node_lift n') \<longrightarrow> (\<exists>s s'. (s, s') \<in> rf_sr) \<longrightarrow> \<not> 0 < mdbPrev n) proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma valid_mdb_ctes_of_next:
  "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> cte_at' (mdbNext (cteMDBNode cte)) s" unfolding valid_mdb'_def valid_mdb_ctes_def supply word_neq_0_conv[simp del] apply clarsimp apply (erule (2) valid_dlistE) apply (simp add: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb' s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) s proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s (mdbNext (cteMDBNode cte)) = Some cte'; mdbPrev (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) s proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma valid_mdb_ctes_of_prev:
  "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> cte_at' (mdbPrev (cteMDBNode cte)) s" unfolding valid_mdb'_def valid_mdb_ctes_def supply word_neq_0_conv[simp del] apply clarsimp apply (erule (2) valid_dlistE) apply (simp add: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb' s; ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev (cteMDBNode cte)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev (cteMDBNode cte)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev (cteMDBNode cte)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev (cteMDBNode cte)) s proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s (mdbPrev (cteMDBNode cte)) = Some cte'; mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (mdbPrev (cteMDBNode cte)) s proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma rf_sr_cpspace_asidpool_relation:
  "(s, s') \<in> rf_sr
    \<Longrightarrow> cpspace_asidpool_relation (ksPSpace s) (t_hrs_' (globals s'))" by (clarsimp simp: rf_sr_def cstate_relation_def
                     cpspace_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation
theory SR_lemmas_C

lemma rf_sr_cpte_relation:
  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_ptes (ksPSpace s))
                         (cslift s') pte_Ptr cpte_relation" by (clarsimp simp: 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 (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation
theory SR_lemmas_C

lemma rf_sr_cpde_relation:
  "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_pdes (ksPSpace s))
                         (cslift s') pde_Ptr cpde_relation" by (clarsimp simp: 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 (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation
theory SR_lemmas_C

lemma rf_sr_cte_relation:
  "\<lbrakk> (s, s') \<in> rf_sr; ctes_of s src = Some cte; cslift s' (Ptr src) = Some cte' \<rbrakk> \<Longrightarrow> ccte_relation cte cte'" apply (drule cmap_relation_cte) apply (erule (2) cmap_relation_relI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; ctes_of s src = Some cte; cslift s' (cte_Ptr src) = Some cte'\<rbrakk> \<Longrightarrow> ccte_relation cte cte' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s src = Some cte; cslift s' (cte_Ptr src) = Some cte'; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation\<rbrakk> \<Longrightarrow> ccte_relation cte cte' proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma ccte_relation_ccap_relation:
  "ccte_relation cte cte' \<Longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C cte')" unfolding ccte_relation_def ccap_relation_def c_valid_cte_def cl_valid_cte_def c_valid_cap_def cl_valid_cap_def by (clarsimp simp: map_option_Some_eq2 if_bool_eq_conj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccte_relation cte cte' \<Longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C cte') proof (prove)
goal (1 subgoal):
 1. Some cte = map_option cte_to_H (cte_lift cte') \<and> (case cap_lift (cte_C.cap_C cte') of None \<Rightarrow> True | Some (Cap_frame_cap fc) \<Rightarrow> capFSize_CL fc \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_irq_handler_cap fc) \<Rightarrow> capIRQ_CL fc && mask 10 = capIRQ_CL fc | Some _ \<Rightarrow> True) \<Longrightarrow> Some (cteCap cte) = map_option cap_to_H (cap_lift (cte_C.cap_C cte')) \<and> (case cap_lift (cte_C.cap_C cte') of None \<Rightarrow> True | Some (Cap_frame_cap fc) \<Rightarrow> capFSize_CL fc \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage | Some (Cap_irq_handler_cap fc) \<Rightarrow> capIRQ_CL fc && mask 10 = capIRQ_CL fc | Some _ \<Rightarrow> True)
theory SR_lemmas_C

lemma ccte_relation_cmdbnode_relation:
  "ccte_relation cte cte' \<Longrightarrow> cmdbnode_relation (cteMDBNode cte) (cte_C.cteMDBNode_C cte')" unfolding ccte_relation_def ccap_relation_def by (clarsimp simp: map_option_Some_eq2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccte_relation cte cte' \<Longrightarrow> cmdbnode_relation (cteMDBNode cte) (cteMDBNode_C cte') proof (prove)
goal (1 subgoal):
 1. Some cte = map_option cte_to_H (cte_lift cte') \<and> c_valid_cte cte' \<Longrightarrow> cmdbnode_relation (cteMDBNode cte) (cteMDBNode_C cte')
theory SR_lemmas_C

lemma rf_sr_ctes_of_clift:
  assumes sr: "(s, s') \<in> rf_sr"
  and    cof: "ctes_of s p = Some cte"
  shows "\<exists>cte'. cslift s' (Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte'))
         \<and> c_valid_cte cte'" proof - from sr have "cpspace_cte_relation (ksPSpace s) (t_hrs_' (globals s'))" .. thus ?thesis using cof apply (rule cspace_cte_relationE) apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>cte'. cslift s' (cte_Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte' proof (state)
goal (1 subgoal):
 1. \<exists>cte'. cslift s' (cte_Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte' proof (chain)
picking this:
(s, s') \<in> rf_sr proof (prove)
using this:
(s, s') \<in> rf_sr

goal (1 subgoal):
 1. cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation proof (state)
this:
cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation

goal (1 subgoal):
 1. \<exists>cte'. cslift s' (cte_Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte' proof (prove)
using this:
cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation

goal (1 subgoal):
 1. \<exists>cte'. cslift s' (cte_Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte' proof (prove)
using this:
cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation
ctes_of s p = Some cte

goal (1 subgoal):
 1. \<exists>cte'. cslift s' (cte_Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte' proof (prove)
goal (1 subgoal):
 1. \<And>z k'. \<lbrakk>cslift s' (cte_Ptr p) = Some k'; cte_lift k' = Some z; cte_to_H z = cte; c_valid_cte k'\<rbrakk> \<Longrightarrow> \<exists>cte'. cslift s' (cte_Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte' proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>cte'. cslift s' (cte_Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) \<and> c_valid_cte cte'

goal:
No subgoals!
theory SR_lemmas_C

lemma c_valid_cte_eq:
 "c_valid_cte c = case_option True cl_valid_cte (cte_lift c)" apply (clarsimp simp: c_valid_cte_def cl_valid_cte_def c_valid_cap_def  split: option.splits) apply (unfold cte_lift_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c_valid_cte c = (case cte_lift c of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cte x) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>cap_lift (cte_C.cap_C c) = Some x2; cte_lift c = None\<rbrakk> \<Longrightarrow> cl_valid_cap x2 proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>cap_lift (cte_C.cap_C c) = Some x2; (case cap_lift (cte_C.cap_C c) of None \<Rightarrow> None | Some cap \<Rightarrow> Some \<lparr>cap_CL = cap, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C c)\<rparr>) = None\<rbrakk> \<Longrightarrow> cl_valid_cap x2 proof (prove)
goal:
No subgoals!
theory SR_lemmas_C

lemma rf_sr_upd:
  assumes
    "(t_hrs_' (globals x)) = (t_hrs_' (globals y))"
    "(ksReadyQueues_' (globals x)) = (ksReadyQueues_' (globals y))"
    "(ksReadyQueuesL1Bitmap_' (globals x)) = (ksReadyQueuesL1Bitmap_' (globals y))"
    "(ksReadyQueuesL2Bitmap_' (globals x)) = (ksReadyQueuesL2Bitmap_' (globals y))"
    "(ksSchedulerAction_' (globals x)) = (ksSchedulerAction_' (globals y))"
    "(ksCurThread_' (globals x)) = (ksCurThread_' (globals y))"
    "(ksIdleThread_' (globals x)) = (ksIdleThread_' (globals y))"
    "(ksWorkUnitsCompleted_' (globals x)) = (ksWorkUnitsCompleted_' (globals y))"
    "intStateIRQNode_'(globals x) = intStateIRQNode_' (globals y)"
    "intStateIRQTable_'(globals x) = intStateIRQTable_' (globals y)"
    "armKSHWASIDTable_' (globals x) = armKSHWASIDTable_' (globals y)"
    "armKSASIDTable_' (globals x) = armKSASIDTable_' (globals y)"
    "armKSNextASID_' (globals x) = armKSNextASID_' (globals y)"
    "phantom_machine_state_' (globals x) = phantom_machine_state_' (globals y)"
    "ghost'state_' (globals x) = ghost'state_' (globals y)"
    "ksDomScheduleIdx_' (globals x) = ksDomScheduleIdx_' (globals y)"
    "ksCurDomain_' (globals x) = ksCurDomain_' (globals y)"
    "ksDomainTime_' (globals x) = ksDomainTime_' (globals y)"
  shows "((a, x) \<in> rf_sr) = ((a, y) \<in> rf_sr)" unfolding rf_sr_def using assms by simp (rule cstate_relation_only_t_hrs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a, x) \<in> rf_sr) = ((a, y) \<in> rf_sr) proof (prove)
goal (1 subgoal):
 1. ((a, x) \<in> {(s, s'). cstate_relation s (globals s')}) = ((a, y) \<in> {(s, s'). cstate_relation s (globals s')}) proof (prove)
using this:
t_hrs_' (globals x) = t_hrs_' (globals y)
ksReadyQueues_' (globals x) = ksReadyQueues_' (globals y)
ksReadyQueuesL1Bitmap_' (globals x) = ksReadyQueuesL1Bitmap_' (globals y)
ksReadyQueuesL2Bitmap_' (globals x) = ksReadyQueuesL2Bitmap_' (globals y)
ksSchedulerAction_' (globals x) = ksSchedulerAction_' (globals y)
ksCurThread_' (globals x) = ksCurThread_' (globals y)
ksIdleThread_' (globals x) = ksIdleThread_' (globals y)
ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted_' (globals y)
intStateIRQNode_' (globals x) = intStateIRQNode_' (globals y)
intStateIRQTable_' (globals x) = intStateIRQTable_' (globals y)
armKSHWASIDTable_' (globals x) = armKSHWASIDTable_' (globals y)
armKSASIDTable_' (globals x) = armKSASIDTable_' (globals y)
armKSNextASID_' (globals x) = armKSNextASID_' (globals y)
phantom_machine_state_' (globals x) = phantom_machine_state_' (globals y)
ghost'state_' (globals x) = ghost'state_' (globals y)
ksDomScheduleIdx_' (globals x) = ksDomScheduleIdx_' (globals y)
ksCurDomain_' (globals x) = ksCurDomain_' (globals y)
ksDomainTime_' (globals x) = ksDomainTime_' (globals y)

goal (1 subgoal):
 1. ((a, x) \<in> {(s, s'). cstate_relation s (globals s')}) = ((a, y) \<in> {(s, s'). cstate_relation s (globals s')})