kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbQueue_C

lemma tcb_queue_relation_ptr_rel':
  assumes   tq: "tcb_queue_relation getNext getPrev mp queue NULL qhead"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and   cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb"
  and in_queue: "tcbp \<in> set queue"
  shows "tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb
         \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb)" using tq valid_ep cs_tcb null_not_in [OF tq valid_ep(1) valid_ep(2)] in_queue by (rule tcb_queue_relation_ptr_rel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb) proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue NULL qhead
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
ctcb_ptr_to_tcb_ptr NULL \<notin> set queue
tcbp \<in> set queue

goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr tcbp \<noteq> getNext tcb \<and> tcb_ptr_to_ctcb_ptr tcbp \<noteq> getPrev tcb \<and> (getNext tcb \<noteq> NULL \<longrightarrow> getNext tcb \<noteq> getPrev tcb)
theory TcbQueue_C

lemma tcb_queue_head_empty_iff:
  "\<lbrakk> tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t \<in> set queue. tcb_at' t s \<rbrakk> \<Longrightarrow>
  (qhead = NULL) = (queue = [])" apply (rule classical) apply (cases queue) apply simp apply (frule (1) tcb_queue_relation_not_NULL) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t\<in>set queue. tcb_at' t s\<rbrakk> \<Longrightarrow> (qhead = NULL) = (queue = []) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t\<in>set queue. tcb_at' t s; (qhead = NULL) \<noteq> (queue = [])\<rbrakk> \<Longrightarrow> (qhead = NULL) = (queue = []) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t\<in>set queue. tcb_at' t s; (qhead = NULL) \<noteq> (queue = []); queue = []\<rbrakk> \<Longrightarrow> (qhead = NULL) = (queue = [])
 2. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t\<in>set queue. tcb_at' t s; (qhead = NULL) \<noteq> (queue = []); queue = a # list\<rbrakk> \<Longrightarrow> (qhead = NULL) = (queue = []) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t\<in>set queue. tcb_at' t s; (qhead = NULL) \<noteq> (queue = []); queue = a # list\<rbrakk> \<Longrightarrow> (qhead = NULL) = (queue = []) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t\<in>set queue. tcb_at' t s; (qhead = NULL) \<noteq> (queue = []); queue = a # list; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL\<rbrakk> \<Longrightarrow> (qhead = NULL) = (queue = []) proof (prove)
goal:
No subgoals!
theory TcbQueue_C

lemma ctcb_ptr_to_tcb_ptr_aligned:
  assumes al: "is_aligned (ctcb_ptr_to_tcb_ptr ptr) tcbBlockSizeBits"
  shows   "is_aligned (ptr_val ptr) ctcb_size_bits" proof - have "is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr ptr))) ctcb_size_bits" unfolding tcb_ptr_to_ctcb_ptr_def using al apply simp apply (erule aligned_add_aligned) apply (unfold ctcb_offset_defs, rule is_aligned_triv) apply (simp add: word_bits_conv objBits_defs)+ done thus ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (ptr_val ptr) ctcb_size_bits proof (state)
goal (1 subgoal):
 1. is_aligned (ptr_val ptr) ctcb_size_bits proof (prove)
goal (1 subgoal):
 1. is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr ptr))) ctcb_size_bits proof (prove)
goal (1 subgoal):
 1. is_aligned (ptr_val (tcb_Ptr (ctcb_ptr_to_tcb_ptr ptr + ctcb_offset))) ctcb_size_bits proof (prove)
using this:
is_aligned (ctcb_ptr_to_tcb_ptr ptr) tcbBlockSizeBits

goal (1 subgoal):
 1. is_aligned (ptr_val (tcb_Ptr (ctcb_ptr_to_tcb_ptr ptr + ctcb_offset))) ctcb_size_bits proof (prove)
goal (1 subgoal):
 1. is_aligned (ctcb_ptr_to_tcb_ptr ptr) tcbBlockSizeBits \<Longrightarrow> is_aligned (ctcb_ptr_to_tcb_ptr ptr + ctcb_offset) ctcb_size_bits proof (prove)
goal (2 subgoals):
 1. is_aligned ctcb_offset ctcb_size_bits
 2. ctcb_size_bits \<le> tcbBlockSizeBits proof (prove)
goal (1 subgoal):
 1. 8 \<le> tcbBlockSizeBits proof (prove)
goal:
No subgoals! proof (state)
this:
is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr ptr))) ctcb_size_bits

goal (1 subgoal):
 1. is_aligned (ptr_val ptr) ctcb_size_bits proof (prove)
using this:
is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr ptr))) ctcb_size_bits

goal (1 subgoal):
 1. is_aligned (ptr_val ptr) ctcb_size_bits proof (state)
this:
is_aligned (ptr_val ptr) ctcb_size_bits

goal:
No subgoals!
theory TcbQueue_C

lemma ctcb_size_bits_ge_4: "4 \<le> ctcb_size_bits" by (simp add: ctcb_size_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 4 \<le> ctcb_size_bits
theory TcbQueue_C

lemma tcb_queue_relation'_next_mask:
  assumes   tq: "tcb_queue_relation' getNext getPrev mp queue qhead qend"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and   cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb"
  and in_queue: "tcbp \<in> set queue"
  and     bits: "bits \<le> ctcb_size_bits"
  shows "ptr_val (getNext tcb) && ~~ mask bits = ptr_val (getNext tcb)" by (rule tcb_queue_relation_next_mask [OF tcb_queue_relation'_queue_rel], fact+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_val (getNext tcb) && ~~ mask bits = ptr_val (getNext tcb)
theory TcbQueue_C

lemma tcb_queue_relation'_prev_mask:
  assumes   tq: "tcb_queue_relation' getNext getPrev mp queue qhead qend"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and   cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb"
  and in_queue: "tcbp \<in> set queue"
  and     bits: "bits \<le> ctcb_size_bits"
  shows "ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)" by (rule tcb_queue_relation_prev_mask [OF tcb_queue_relation'_queue_rel], fact+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)
theory TcbQueue_C

lemma tcb_queue_relation'_empty[simp]:
  "tcb_queue_relation' getNext getPrev mp [] qhead qend =
      (qend = tcb_Ptr 0 \<and> qhead = tcb_Ptr 0)" by (simp add: tcb_queue_relation'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation' getNext getPrev mp [] qhead qend = (qend = NULL \<and> qhead = NULL)
theory TcbQueue_C

lemma cvariable_relation_upd_const:
  "m x \<noteq> None
    \<Longrightarrow> cvariable_array_map_relation (m (x \<mapsto> y)) (\<lambda>x. n)
        = cvariable_array_map_relation m (\<lambda>x. n)" by (auto simp: fun_eq_iff cvariable_array_map_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m x \<noteq> None \<Longrightarrow> cvariable_array_map_relation (m(x \<mapsto> y)) (\<lambda>x. n) = cvariable_array_map_relation m (\<lambda>x. n)
theory TcbQueue_C

lemma rf_sr_tcb_update_no_queue_helper:
  "(s, s'\<lparr> globals := globals s' \<lparr> t_hrs_' := t_hrs_' (globals (undefined
              \<lparr> globals := (undefined \<lparr> t_hrs_' := f (globals s') (t_hrs_' (globals s')) \<rparr>)\<rparr>))\<rparr>\<rparr>) \<in> rf_sr
          \<Longrightarrow> (s, globals_update (\<lambda>v. t_hrs_'_update (f v) v) s') \<in> rf_sr" by (simp cong: StateSpace.state.fold_congs globals.fold_congs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals (undefined\<lparr>globals := undefined\<lparr>t_hrs_' := f (globals s') (t_hrs_' (globals s'))\<rparr>\<rparr>))\<rparr>\<rparr>) \<in> rf_sr \<Longrightarrow> (s, globals_update (\<lambda>v. t_hrs_'_update (f v) v) s') \<in> rf_sr
theory TcbAcc_C

lemma threadGet_eq:
  "ko_at' tcb thread s \<Longrightarrow> (f tcb, s) \<in> fst (threadGet f thread s)" unfolding threadGet_def apply (simp add: liftM_def in_monad) apply (rule exI [where x = tcb]) apply simp apply (subst getObject_eq) apply simp apply (simp add: objBits_simps') apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' tcb thread s \<Longrightarrow> (f tcb, s) \<in> fst (threadGet f thread s) proof (prove)
goal (1 subgoal):
 1. ko_at' tcb thread s \<Longrightarrow> (f tcb, s) \<in> fst ((liftM f $ getObject thread) s) proof (prove)
goal (1 subgoal):
 1. ko_at' tcb thread s \<Longrightarrow> \<exists>x. (x, s) \<in> fst (getObject thread s) \<and> f tcb = f x proof (prove)
goal (1 subgoal):
 1. ko_at' tcb thread s \<Longrightarrow> (tcb, s) \<in> fst (getObject thread s) \<and> f tcb = f tcb proof (prove)
goal (1 subgoal):
 1. ko_at' tcb thread s \<Longrightarrow> (tcb, s) \<in> fst (getObject thread s) proof (prove)
goal (4 subgoals):
 1. \<And>q n ko. ko_at' tcb thread s \<Longrightarrow> loadObject thread q n ko = loadObject_default thread q n ko
 2. \<And>v. ko_at' tcb thread s \<Longrightarrow> 1 < 2 ^ objBits v
 3. ko_at' tcb thread s \<Longrightarrow> ko_at' tcb thread s
 4. ko_at' tcb thread s \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>v. ko_at' tcb thread s \<Longrightarrow> 1 < 2 ^ objBits v
 2. ko_at' tcb thread s \<Longrightarrow> ko_at' tcb thread s
 3. ko_at' tcb thread s \<Longrightarrow> True proof (prove)
goal (2 subgoals):
 1. ko_at' tcb thread s \<Longrightarrow> ko_at' tcb thread s
 2. ko_at' tcb thread s \<Longrightarrow> True proof (prove)
goal (1 subgoal):
 1. ko_at' tcb thread s \<Longrightarrow> True proof (prove)
goal:
No subgoals!
theory TcbAcc_C

lemma register_from_H_less:
  "register_from_H hr < 20" by (cases hr, simp_all add: "StrictC'_register_defs")

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. register_from_H hr < 0x14
theory TcbAcc_C

lemma is_aligned_tcb_ptr_to_ctcb_ptr:
  "obj_at' (P :: tcb \<Rightarrow> bool) p s
     \<Longrightarrow> is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr p)) ctcb_size_bits" apply (clarsimp simp: obj_at'_def objBits_simps' projectKOs
                        tcb_ptr_to_ctcb_ptr_def ctcb_offset_defs) apply (erule aligned_add_aligned, simp_all add: word_bits_conv) apply (simp add: is_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P p s \<Longrightarrow> is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr p)) ctcb_size_bits proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (KOTCB obj); is_aligned p 9; P obj; ps_clear p 9 s\<rbrakk> \<Longrightarrow> is_aligned (p + 0x100) 8 proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (KOTCB obj); P obj; ps_clear p 9 s\<rbrakk> \<Longrightarrow> is_aligned 0x100 8 proof (prove)
goal:
No subgoals!
theory PSpace_C

lemma carray_map_relation_upd_triv:
  "f x = Some (v :: 'a :: pspace_storable)
    \<Longrightarrow> carray_map_relation n (f (x \<mapsto> y)) hp ptrf = carray_map_relation n f hp ptrf" by (simp add: carray_map_relation_def objBits_def objBitsT_koTypeOf[symmetric]
                koTypeOf_injectKO
           del: objBitsT_koTypeOf)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x = Some v \<Longrightarrow> carray_map_relation n (f(x \<mapsto> y)) hp ptrf = carray_map_relation n f hp ptrf
theory PSpace_C

lemma storePTE_Basic_ccorres:
  "\<lbrakk> cpte_relation pte pte' \<rbrakk> \<Longrightarrow>
   ccorres dc xfdc \<top> {s. f s = p} hs
     (storePTE p pte)
     (Guard C_Guard {s. s \<Turnstile>\<^sub>c pte_Ptr (f s)}
        (Basic (\<lambda>s. globals_update( t_hrs_'_update
            (hrs_mem_update (heap_update (pte_Ptr (f s)) pte'))) s)))" apply (rule ccorres_guard_imp2) apply (erule storePTE_Basic_ccorres') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cpte_relation pte pte' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) {s. f s = p} hs (storePTE p pte) (Guard C_Guard {s. s \<Turnstile>\<^sub>c pte_Ptr (f s)} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr \<acute>f) pte')))) proof (prove)
goal (2 subgoals):
 1. cpte_relation pte pte' \<Longrightarrow> ccorres dc xfdc ?Q ?Q' hs (storePTE p pte) (Guard C_Guard {s. s \<Turnstile>\<^sub>c pte_Ptr (f s)} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (pte_Ptr \<acute>f) pte'))))
 2. \<And>s s'. \<lbrakk>cpte_relation pte pte'; (s, s') \<in> rf_sr; True; s' \<in> {s. f s = p}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>cpte_relation pte pte'; (s, s') \<in> rf_sr; True; s' \<in> {s. f s = p}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. ptr_val (pte_Ptr (f s)) = p} proof (prove)
goal:
No subgoals!
theory PSpace_C

lemma pde_stored_asid_update_valid_offset:
  "valid_pde_mapping_offset' (ptr_val p && mask pdBits)
      \<Longrightarrow> (pde_stored_asid  \<circ>\<^sub>m (clift (t_hrs_' cstate))(p \<mapsto> pde) \<circ>\<^sub>m pd_pointer_to_asid_slot)
            = (pde_stored_asid  \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot)" apply (rule ext, clarsimp simp add: pd_pointer_to_asid_slot_def map_comp_eq) apply (simp add: valid_pde_mapping_offset'_def mask_add_aligned) apply (simp add: pd_asid_slot_def pdBits_def pageBits_def mask_def pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pde_mapping_offset' (ptr_val p && mask pdBits) \<Longrightarrow> pde_stored_asid \<circ>\<^sub>m (clift (t_hrs_' cstate))(p \<mapsto> pde) \<circ>\<^sub>m pd_pointer_to_asid_slot = pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_pde_mapping_offset' (x + 0x3FC0 && mask pdBits); p = pde_Ptr (x + 0x3FC0); is_aligned x pdBits\<rbrakk> \<Longrightarrow> pde_stored_asid pde = (case clift (t_hrs_' cstate) (pde_Ptr (x + 0x3FC0)) of None \<Rightarrow> None | Some x \<Rightarrow> pde_stored_asid x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>0x3FC0 && mask pdBits \<noteq> pd_asid_slot * 4; p = pde_Ptr (x + 0x3FC0); is_aligned x pdBits\<rbrakk> \<Longrightarrow> pde_stored_asid pde = (case clift (t_hrs_' cstate) (pde_Ptr (x + 0x3FC0)) of None \<Rightarrow> None | Some x \<Rightarrow> pde_stored_asid x) proof (prove)
goal:
No subgoals!
theory PSpace_C

lemma storePDE_Basic_ccorres:
  "\<lbrakk> cpde_relation pde pde' \<rbrakk> \<Longrightarrow>
   ccorres dc xfdc (\<lambda>_. valid_pde_mapping_offset' (p && mask pdBits)) {s. f s = p} hs
     (storePDE p pde)
     (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (f s)}
        (Basic (\<lambda>s. globals_update(t_hrs_'_update
            (hrs_mem_update (heap_update (pde_Ptr (f s)) pde'))) s)))" apply (rule ccorres_guard_imp2) apply (erule storePDE_Basic_ccorres') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cpde_relation pde pde' \<Longrightarrow> ccorres dc xfdc (\<lambda>_. valid_pde_mapping_offset' (p && mask pdBits)) {s. f s = p} hs (storePDE p pde) (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (f s)} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr \<acute>f) pde')))) proof (prove)
goal (2 subgoals):
 1. cpde_relation pde pde' \<Longrightarrow> ccorres dc xfdc ?Q ?Q' hs (storePDE p pde) (Guard C_Guard {s. s \<Turnstile>\<^sub>c pde_Ptr (f s)} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (pde_Ptr \<acute>f) pde'))))
 2. \<And>s s'. \<lbrakk>cpde_relation pde pde'; (s, s') \<in> rf_sr; valid_pde_mapping_offset' (p && mask pdBits); s' \<in> {s. f s = p}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>cpde_relation pde pde'; (s, s') \<in> rf_sr; valid_pde_mapping_offset' (p && mask pdBits); s' \<in> {s. f s = p}\<rbrakk> \<Longrightarrow> valid_pde_mapping_offset' (p && mask pdBits) \<and> s' \<in> {s. ptr_val (pde_Ptr (f s)) = p} proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma pageBitsForSize_le:
  "pageBitsForSize x \<le> 24" by (simp add: pageBitsForSize_def split: vmpage_size.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBitsForSize x \<le> 24
theory VSpace_C

lemma unat_of_nat_pageBitsForSize [simp]:
  "unat (of_nat (pageBitsForSize x)::word32) = pageBitsForSize x" apply (subst unat_of_nat32) apply (rule order_le_less_trans, rule pageBitsForSize_le) apply (simp add: word_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat (pageBitsForSize x)) = pageBitsForSize x proof (prove)
goal (2 subgoals):
 1. pageBitsForSize x < 2 ^ word_bits
 2. pageBitsForSize x = pageBitsForSize x proof (prove)
goal (2 subgoals):
 1. 24 < 2 ^ word_bits
 2. pageBitsForSize x = pageBitsForSize x proof (prove)
goal (1 subgoal):
 1. pageBitsForSize x = pageBitsForSize x proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma asidLowBits_handy_convs:
  "sint Kernel_C.asidLowBits = 10"
  "Kernel_C.asidLowBits \<noteq> 0x20"
  "unat Kernel_C.asidLowBits = asid_low_bits" by (simp add: Kernel_C.asidLowBits_def asid_low_bits_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint Kernel_C.asidLowBits = 10 &&& Kernel_C.asidLowBits \<noteq> 0x20 &&& unat Kernel_C.asidLowBits = local.asid_low_bits
theory VSpace_C

lemma rf_sr_armKSASIDTable:
  "\<lbrakk> (s, s') \<in> rf_sr; n \<le> 2 ^ asid_high_bits - 1 \<rbrakk>
       \<Longrightarrow> index (armKSASIDTable_' (globals s')) (unat n)
               = option_to_ptr (armKSASIDTable (ksArchState s) n)" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                     carch_state_relation_def array_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; n \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> armKSASIDTable_' (globals s').[unat n] = option_to_ptr (armKSASIDTable (ksArchState s) n)
theory VSpace_C

lemma asid_high_bits_word_bits:
  "asid_high_bits < word_bits" by (simp add: asid_high_bits_def word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.asid_high_bits < word_bits
theory VSpace_C

lemma rf_sr_asid_map_pd_to_hwasids:
  "(s, s') \<in> rf_sr \<Longrightarrow>
   asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s))
       = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot)" by (simp add: rf_sr_def cstate_relation_def Let_def
                carch_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot)
theory VSpace_C

lemma asid_shiftr_low_bits_less:
  "(asid :: word32) \<le> mask asid_bits \<Longrightarrow> asid >> asid_low_bits < 0x80" apply (rule_tac y="2 ^ 7" in order_less_le_trans) apply (rule shiftr_less_t2n) apply (simp add: le_mask_iff_lt_2n[THEN iffD1] asid_bits_def asid_low_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> asid >> local.asid_low_bits < 0x80 proof (prove)
goal (2 subgoals):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> asid >> local.asid_low_bits < 2 ^ 7
 2. asid \<le> mask local.asid_bits \<Longrightarrow> 2 ^ 7 \<le> 0x80 proof (prove)
goal (2 subgoals):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> asid < 2 ^ (local.asid_low_bits + 7)
 2. asid \<le> mask local.asid_bits \<Longrightarrow> 2 ^ 7 \<le> 0x80 proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> 2 ^ 7 \<le> 0x80 proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma array_relation_update:
  "\<lbrakk> array_relation R bnd table (arr :: 'a['b :: finite]);
               x' = unat (x :: ('td :: len) word); R v v';
               unat bnd < card (UNIV :: 'b set) \<rbrakk>
     \<Longrightarrow> array_relation R bnd (table (x := v))
               (Arrays.update arr x' v')" by (simp add: array_relation_def word_le_nat_alt split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>array_relation R bnd table arr; x' = unat x; R v v'; unat bnd < CARD('b)\<rbrakk> \<Longrightarrow> array_relation R bnd (table(x := v)) (Arrays.update arr x' v')
theory VSpace_C

lemma unat_asidLowBits [simp]:
  "unat Kernel_C.asidLowBits = asidLowBits" by (simp add: asidLowBits_def Kernel_C.asidLowBits_def asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat Kernel_C.asidLowBits = local.asidLowBits
theory VSpace_C

lemma leq_asid_bits_shift:
  "x \<le> mask asid_bits \<Longrightarrow> (x::word32) >> asid_low_bits \<le> mask asid_high_bits" apply (rule word_leI) apply (simp add: nth_shiftr word_size) apply (rule ccontr) apply (clarsimp simp: linorder_not_less asid_high_bits_def asid_low_bits_def) apply (simp add: mask_def) apply (simp add: upper_bits_unset_is_l2p_32 [symmetric]) apply (simp add: asid_bits_def word_bits_def) apply (erule_tac x="10+n" in allE) apply (simp add: linorder_not_less) apply (drule test_bit_size) apply (simp add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> mask local.asid_bits \<Longrightarrow> x >> local.asid_low_bits \<le> mask local.asid_high_bits proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<le> mask local.asid_bits; n < size (x >> local.asid_low_bits); (x >> local.asid_low_bits) !! n\<rbrakk> \<Longrightarrow> mask local.asid_high_bits !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<le> mask local.asid_bits; n < 32; x !! (local.asid_low_bits + n)\<rbrakk> \<Longrightarrow> n < local.asid_high_bits proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<le> mask local.asid_bits; n < 32; x !! (local.asid_low_bits + n); \<not> n < local.asid_high_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x \<le> mask local.asid_bits; n < 32; x !! (10 + n); 7 \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_bits; n < 32; x !! (10 + n); 7 \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n'\<ge>local.asid_bits. n' < word_bits \<longrightarrow> \<not> x !! n'; n < 32; x !! (10 + n); 7 \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n'\<ge>17. n' < 32 \<longrightarrow> \<not> x !! n'; n < 32; x !! (10 + n); 7 \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 32; x !! (10 + n); 7 \<le> n; 17 \<le> 10 + n \<longrightarrow> 10 + n < 32 \<longrightarrow> \<not> x !! (10 + n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 32; x !! (10 + n); 22 \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>n < 32; 22 \<le> n; 10 + n < size x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!