kings-crown/FVELER_Isabelle huggingface dataset:
theory Machine_R

lemma dmo_maskInterrupt_True:
  "\<lbrace>invs'\<rbrace> doMachineOp (maskInterrupt True irq) \<lbrace>\<lambda>_. invs'\<rbrace>" apply (wp dmo_maskInterrupt) apply (clarsimp simp: invs'_def valid_state'_def) apply (simp add: valid_irq_masks'_def valid_machine_state'_def
                   ct_not_inQ_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (maskInterrupt True irq) \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> invs' (ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := True))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> valid_irq_masks' (intStateIRQTable (ksInterruptState s)) ((irq_masks (ksMachineState s))(irq := True)) \<and> valid_machine_state' (ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := True))) s) proof (prove)
goal:
No subgoals!
theory Machine_R

lemma setIRQState_irq_states':
  "\<lbrace>valid_irq_states'\<rbrace>
      setIRQState state irq
   \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>" apply (simp add: setIRQState_def setInterruptState_def getInterruptState_def) apply (wp dmo_maskInterrupt) apply (simp add: valid_irq_masks'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> setIRQState state irq \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> do st <- gets ksInterruptState;
y <- modify (ksInterruptState_update (\<lambda>_. intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state)) st));
doMachineOp (maskInterrupt (state = irqstate.IRQInactive) irq)
od \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' (ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := state = irqstate.IRQInactive))) (s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := state)) (ksInterruptState s)\<rparr>)) proof (prove)
goal:
No subgoals!
theory Machine_R

lemma getActiveIRQ_le_maxIRQ:
  "\<lbrace>irqs_masked' and valid_irq_states'\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp apply (drule use_valid, rule getActiveIRQ_le_maxIRQ') prefer 2 apply simp apply (simp add: irqs_masked'_def valid_irq_states'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irqs_masked' and valid_irq_states'\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>irqs_masked' and valid_irq_states'\<rbrace> do ms <- gets ksMachineState;
p <- select_f (getActiveIRQ in_kernel ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (irqs_masked' and valid_irq_states') s \<Longrightarrow> \<forall>x\<in>fst (getActiveIRQ in_kernel (ksMachineState s)). \<forall>xa. fst x = Some xa \<longrightarrow> xa \<le> maxIRQ proof (prove)
goal (1 subgoal):
 1. \<And>s b x. \<lbrakk>(Some x, b) \<in> fst (getActiveIRQ in_kernel (ksMachineState s)); irqs_masked' s; valid_irq_states' s\<rbrakk> \<Longrightarrow> x \<le> maxIRQ proof (prove)
goal (2 subgoals):
 1. \<And>s b x. \<lbrakk>irqs_masked' s; valid_irq_states' s\<rbrakk> \<Longrightarrow> \<forall>irq>maxIRQ. irq_masks (ksMachineState s) irq
 2. \<And>s b x. \<lbrakk>irqs_masked' s; valid_irq_states' s; \<forall>xa. Some x = Some xa \<longrightarrow> xa \<le> maxIRQ\<rbrakk> \<Longrightarrow> x \<le> maxIRQ proof (prove)
goal (2 subgoals):
 1. \<And>s b x. \<lbrakk>irqs_masked' s; valid_irq_states' s; \<forall>xa. Some x = Some xa \<longrightarrow> xa \<le> maxIRQ\<rbrakk> \<Longrightarrow> x \<le> maxIRQ
 2. \<And>s b x. \<lbrakk>irqs_masked' s; valid_irq_states' s\<rbrakk> \<Longrightarrow> \<forall>irq>maxIRQ. irq_masks (ksMachineState s) irq proof (prove)
goal (1 subgoal):
 1. \<And>s b x. \<lbrakk>irqs_masked' s; valid_irq_states' s\<rbrakk> \<Longrightarrow> \<forall>irq>maxIRQ. irq_masks (ksMachineState s) irq proof (prove)
goal:
No subgoals!
theory Machine_R

lemma getActiveIRQ_neq_Some0xFF:
  "\<lbrace>\<top>\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp apply (drule use_valid, rule getActiveIRQ_neq_Some0xFF') apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ms <- gets ksMachineState;
p <- select_f (getActiveIRQ in_kernel ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>rv s. rv \<noteq> Some 0x3FF\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>x\<in>fst (getActiveIRQ in_kernel (ksMachineState s)). fst x \<noteq> Some 0x3FF proof (prove)
goal (1 subgoal):
 1. \<And>s b. (Some 0x3FF, b) \<in> fst (getActiveIRQ in_kernel (ksMachineState s)) \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s b. True
 2. \<And>s b. Some 0x3FF \<noteq> Some 0x3FF \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma obj_at_getObject:
  assumes R:
  "\<And>a b n ko s obj::'a::pspace_storable.
  \<lbrakk> (a, b) \<in> fst (loadObject t t n ko s); projectKO_opt ko = Some obj \<rbrakk> \<Longrightarrow> a = obj"
  shows "\<lbrace>obj_at' P t\<rbrace> getObject t \<lbrace>\<lambda>(rv::'a::pspace_storable) s. P rv\<rbrace>" by (auto simp: getObject_def obj_at'_def in_monad valid_def
                 split_def projectKOs lookupAround2_known1
           dest: R)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> getObject t \<lbrace>\<lambda>rv s. P rv\<rbrace>
theory KHeap_R

lemma loadObject_default_inv:
  "\<lbrace>P\<rbrace> loadObject_default addr addr' next obj \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: loadObject_default_def magnitudeCheck_def
                   alignCheck_def unless_def alignError_def
          | wp hoare_vcg_split_case_option
               hoare_drop_imps hoare_vcg_all_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> loadObject_default addr addr' next obj \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma getObject_inv:
  assumes x: "\<And>p q n ko. \<lbrace>P\<rbrace> loadObject p q n ko \<lbrace>\<lambda>(rv :: 'a :: pspace_storable). P\<rbrace>"
  shows      "\<lbrace>P\<rbrace> getObject p \<lbrace>\<lambda>(rv :: 'a :: pspace_storable). P\<rbrace>" by (simp add: getObject_def split_def | wp x)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getObject p \<lbrace>\<lambda>rv. P\<rbrace>
theory KHeap_R

lemma getObject_inv_tcb [wp]: "\<lbrace>P\<rbrace> getObject l \<lbrace>\<lambda>(rv :: Structures_H.tcb). P\<rbrace>" apply (rule getObject_inv) apply simp apply (rule loadObject_default_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getObject l \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>P\<rbrace> loadObject p q n ko \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>P\<rbrace> loadObject_default p q n ko \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma typ_at_to_obj_at':
  "typ_at' (koType (TYPE ('a :: pspace_storable))) p s
     = obj_at' (\<top> :: 'a \<Rightarrow> bool) p s" by (simp add: typ_at'_def obj_at'_real_def project_koType[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at' (koType TYPE('a)) p s = obj_at' (\<lambda>_. True) p s
theory KHeap_R

lemma lookupAround2_same1[simp]:
  "(fst (lookupAround2 x s) = Some (x, y)) = (s x = Some y)" apply (rule iffI) apply (simp add: lookupAround2_char1) apply (simp add: lookupAround2_known1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fst (lookupAround2 x s) = Some (x, y)) = (s x = Some y) proof (prove)
goal (2 subgoals):
 1. fst (lookupAround2 x s) = Some (x, y) \<Longrightarrow> s x = Some y
 2. s x = Some y \<Longrightarrow> fst (lookupAround2 x s) = Some (x, y) proof (prove)
goal (1 subgoal):
 1. s x = Some y \<Longrightarrow> fst (lookupAround2 x s) = Some (x, y) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma koType_objBitsKO:
  "koTypeOf k = koTypeOf k' \<Longrightarrow> objBitsKO k = objBitsKO k'" by (auto simp: objBitsKO_def archObjSize_def
          split: Structures_H.kernel_object.splits
                 ARM_H.arch_kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. koTypeOf k = koTypeOf k' \<Longrightarrow> objBitsKO k = objBitsKO k'
theory KHeap_R

lemma updateObject_objBitsKO:
    "(ko', t') \<in> fst (updateObject (val :: 'a :: pspace_storable) ko p q n t)
         \<Longrightarrow> objBitsKO ko' = objBitsKO ko" apply (drule updateObject_type) apply (erule koType_objBitsKO) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ko', t') \<in> fst (updateObject val ko p q n t) \<Longrightarrow> objBitsKO ko' = objBitsKO ko proof (prove)
goal (1 subgoal):
 1. koTypeOf ko' = koTypeOf ko \<Longrightarrow> objBitsKO ko' = objBitsKO ko proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma updateObject_default_result:
  "(x, s'') \<in> fst (updateObject_default e ko p q n s) \<Longrightarrow> x = injectKO e" by (clarsimp simp add: updateObject_default_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, s'') \<in> fst (updateObject_default e ko p q n s) \<Longrightarrow> x = injectKO e
theory KHeap_R

lemma updateObject_ep_eta:
  "updateObject (v :: endpoint) = updateObject_default v" by ((rule ext)+, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. updateObject v = updateObject_default v
theory KHeap_R

lemma updateObject_tcb_eta:
  "updateObject (v :: tcb) = updateObject_default v" by ((rule ext)+, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. updateObject v = updateObject_default v
theory KHeap_R

lemma updateObject_ntfn_eta:
  "updateObject (v :: Structures_H.notification) = updateObject_default v" by ((rule ext)+, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. updateObject v = updateObject_default v
theory KHeap_R

lemma objBits_type:
  "koTypeOf k = koTypeOf k' \<Longrightarrow> objBitsKO k = objBitsKO k'" by (erule koType_objBitsKO)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. koTypeOf k = koTypeOf k' \<Longrightarrow> objBitsKO k = objBitsKO k'
theory KHeap_R

lemma setObject_typ_at_inv:
  "\<lbrace>typ_at' T p'\<rbrace> setObject p v \<lbrace>\<lambda>r. typ_at' T p'\<rbrace>" apply (clarsimp simp: setObject_def split_def) apply (clarsimp simp: valid_def typ_at'_def ko_wp_at'_def in_monad
                        lookupAround2_char1 ps_clear_upd) apply (drule updateObject_type) apply clarsimp apply (drule objBits_type) apply (simp add: ps_clear_upd) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at' T p'\<rbrace> setObject p v \<lbrace>\<lambda>r. typ_at' T p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at' T p'\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>r. typ_at' T p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko s''a obj'. \<lbrakk>is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) s; T = koTypeOf ko; p' \<le> p; ksPSpace s p' = Some ko; \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject v ko p p' (snd (lookupAround2 p (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> is_aligned p' (objBitsKO obj') \<and> koTypeOf obj' = koTypeOf ko \<and> ps_clear p' (objBitsKO obj') s proof (prove)
goal (1 subgoal):
 1. \<And>s ko s''a obj'. \<lbrakk>is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) s; T = koTypeOf ko; p' \<le> p; ksPSpace s p' = Some ko; \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; koTypeOf obj' = koTypeOf ko\<rbrakk> \<Longrightarrow> is_aligned p' (objBitsKO obj') \<and> koTypeOf obj' = koTypeOf ko \<and> ps_clear p' (objBitsKO obj') s proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj'. \<lbrakk>is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) s; T = koTypeOf ko; p' \<le> p; ksPSpace s p' = Some ko; \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; koTypeOf obj' = koTypeOf ko\<rbrakk> \<Longrightarrow> is_aligned p' (objBitsKO obj') \<and> ps_clear p' (objBitsKO obj') s proof (prove)
goal (1 subgoal):
 1. \<And>s ko obj'. \<lbrakk>is_aligned p' (objBitsKO ko); ps_clear p' (objBitsKO ko) s; T = koTypeOf ko; p' \<le> p; ksPSpace s p' = Some ko; \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; objBitsKO obj' = objBitsKO ko\<rbrakk> \<Longrightarrow> is_aligned p' (objBitsKO obj') \<and> ps_clear p' (objBitsKO obj') s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_typ_at'[wp]:
  "\<lbrace>\<lambda>s. P (typ_at' T p' s)\<rbrace> setObject p v \<lbrace>\<lambda>r s. P (typ_at' T p' s)\<rbrace>" by (blast intro: P_bool_lift setObject_typ_at_inv setObject_typ_at_not)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p' s)\<rbrace> setObject p v \<lbrace>\<lambda>r s. P (typ_at' T p' s)\<rbrace>
theory KHeap_R

lemma setObject_cte_wp_at':
  assumes x: "\<And>x n tcb s t. \<lbrakk> t \<in> fst (updateObject v (KOTCB tcb) ptr x n s); Q s;
                               lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n) \<rbrakk>
                  \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF) \<in> ran tcb_cte_cases. getF tcb' = getF tcb)"
  assumes y: "\<And>x n cte s. fst (updateObject v (KOCTE cte) ptr x n s) = {}"
  shows      "\<lbrace>cte_wp_at' P p and Q\<rbrace> setObject ptr v \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>" unfolding pred_conj_def by (rule setObject_cte_wp_at2'[OF x y], assumption+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p and Q\<rbrace> setObject ptr v \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. cte_wp_at' P p x \<and> Q x\<rbrace> setObject ptr v \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>
theory KHeap_R

lemma obj_at_setObject3:
  fixes Q::"'a::pspace_storable \<Rightarrow> bool"
  fixes P::"'a::pspace_storable \<Rightarrow> bool"
  assumes R: "\<And>ko s x y n. (updateObject v ko p y n s)
                   = (updateObject_default v ko p y n s)"
  assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)"
  shows "\<lbrace>(\<lambda>s. P v)\<rbrace> setObject p v \<lbrace>\<lambda>rv. obj_at' P p\<rbrace>" apply (clarsimp simp add: valid_def in_monad obj_at'_def
                            setObject_def split_def projectKOs
                            project_inject objBits_def[symmetric]
                            R updateObject_default_def
                            in_magnitude_check P ps_clear_upd) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P v\<rbrace> setObject p v \<lbrace>\<lambda>rv. obj_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s uu_. \<lbrakk>P v; ksPSpace s p = Some (injectKO uu_); is_aligned p (objBits v); ps_clear p (objBits v) s\<rbrakk> \<Longrightarrow> \<exists>obj. injectKO obj = injectKO v \<and> P obj proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma getObject_obj_at':
  assumes x: "\<And>q n ko. loadObject p q n ko =
                (loadObject_default p q n ko :: ('a :: pspace_storable) kernel)"
  assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)"
  shows      "\<lbrace> \<top> \<rbrace> getObject p \<lbrace>\<lambda>r::'a::pspace_storable. obj_at' ((=) r) p\<rbrace>" by (clarsimp simp: valid_def getObject_def in_monad
                     loadObject_default_def obj_at'_def projectKOs
                     split_def in_magnitude_check lookupAround2_char1
                     x P project_inject objBits_def[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getObject p \<lbrace>\<lambda>r. obj_at' ((=) r) p\<rbrace>
theory KHeap_R

lemma getObject_valid_obj:
  assumes x: "\<And>p q n ko. loadObject p q n ko =
                (loadObject_default p q n ko :: ('a :: pspace_storable) kernel)"
  assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)"
  shows "\<lbrace> valid_objs' \<rbrace> getObject p \<lbrace>\<lambda>rv::'a::pspace_storable. valid_obj' (injectKO rv) \<rbrace>" apply (rule hoare_chain) apply (rule hoare_vcg_conj_lift) apply (rule getObject_obj_at' [OF x P]) apply (rule getObject_inv) apply (subst x) apply (rule loadObject_default_inv) apply (clarsimp, assumption) apply clarsimp apply (drule(1) obj_at_valid_objs') apply (clarsimp simp: project_inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> getObject p \<lbrace>\<lambda>rv. valid_obj' (injectKO rv)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> getObject p \<lbrace>?Q\<rbrace>
 2. \<And>s. valid_objs' s \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> valid_obj' (injectKO rv) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P4\<rbrace> getObject p \<lbrace>?Q4\<rbrace>
 2. \<lbrace>?P'4\<rbrace> getObject p \<lbrace>?Q'4\<rbrace>
 3. \<And>s. valid_objs' s \<Longrightarrow> ?P4 s \<and> ?P'4 s
 4. \<And>rv s. ?Q4 rv s \<and> ?Q'4 rv s \<Longrightarrow> valid_obj' (injectKO rv) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'4\<rbrace> getObject p \<lbrace>?Q'4\<rbrace>
 2. \<And>s. valid_objs' s \<Longrightarrow> True \<and> ?P'4 s
 3. \<And>rv s. obj_at' ((=) rv) p s \<and> ?Q'4 rv s \<Longrightarrow> valid_obj' (injectKO rv) s proof (prove)
goal (3 subgoals):
 1. \<And>p q n ko. \<lbrace>?P'4\<rbrace> loadObject p q n ko \<lbrace>\<lambda>rv. ?P'4\<rbrace>
 2. \<And>s. valid_objs' s \<Longrightarrow> True \<and> ?P'4 s
 3. \<And>rv s. obj_at' ((=) rv) p s \<and> ?P'4 s \<Longrightarrow> valid_obj' (injectKO rv) s proof (prove)
goal (3 subgoals):
 1. \<And>p q n ko. \<lbrace>?P'4\<rbrace> loadObject_default p q n ko \<lbrace>\<lambda>rv. ?P'4\<rbrace>
 2. \<And>s. valid_objs' s \<Longrightarrow> True \<and> ?P'4 s
 3. \<And>rv s. obj_at' ((=) rv) p s \<and> ?P'4 s \<Longrightarrow> valid_obj' (injectKO rv) s proof (prove)
goal (2 subgoals):
 1. \<And>s. valid_objs' s \<Longrightarrow> True \<and> ?P'4 s
 2. \<And>rv s. obj_at' ((=) rv) p s \<and> ?P'4 s \<Longrightarrow> valid_obj' (injectKO rv) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. obj_at' ((=) rv) p s \<and> valid_objs' s \<Longrightarrow> valid_obj' (injectKO rv) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>obj_at' ((=) rv) p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_obj' (injectKO rv) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>valid_objs' s; \<exists>k. rv = k \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> valid_obj' (injectKO rv) s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma typeError_inv [wp]:
  "\<lbrace>P\<rbrace> typeError x y \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: typeError_def|wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> typeError x y \<lbrace>\<lambda>rv. P\<rbrace>
theory KHeap_R

lemma getObject_cte_inv [wp]: "\<lbrace>P\<rbrace> (getObject addr :: cte kernel) \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: getObject_def loadObject_cte split_def) apply (clarsimp simp: valid_def in_monad) apply (clarsimp simp: typeError_def in_monad magnitudeCheck_def
                 split: kernel_object.split_asm if_split_asm option.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getObject addr \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 addr map));
case snd p of KOTCB tcb \<Rightarrow> do alignCheck (fst p) (objBits tcb);
magnitudeCheck (fst p) (snd (lookupAround2 addr map)) (objBits tcb);
if addr - fst p = tcbVTableSlot << objBits undefined then return (tcbVTable tcb) else if addr - fst p = tcbCTableSlot << objBits undefined then return (tcbCTable tcb) else if addr - fst p = tcbReplySlot << objBits undefined then return (tcbReply tcb) else if addr - fst p = tcbCallerSlot << objBits undefined then return (tcbCaller tcb) else if addr - fst p = tcbIPCBufferSlot << objBits undefined then return (tcbIPCBufferFrame tcb) else fail
od | KOCTE cte \<Rightarrow> do unless (addr = fst p) $ haskell_fail [];
alignCheck addr (objBits cte);
magnitudeCheck addr (snd (lookupAround2 addr map)) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd p)
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>P s; fst (lookupAround2 addr (ksPSpace s)) = Some (aa, ba); (a, b) \<in> fst ((case ba of KOTCB tcb \<Rightarrow> do alignCheck (fst (aa, ba)) (objBits tcb);
magnitudeCheck (fst (aa, ba)) (snd (lookupAround2 addr (ksPSpace s))) (objBits tcb);
if addr - fst (aa, ba) = tcbVTableSlot << objBits undefined then return (tcbVTable tcb) else if addr - fst (aa, ba) = tcbCTableSlot << objBits undefined then return (tcbCTable tcb) else if addr - fst (aa, ba) = tcbReplySlot << objBits undefined then return (tcbReply tcb) else if addr - fst (aa, ba) = tcbCallerSlot << objBits undefined then return (tcbCaller tcb) else if addr - fst (aa, ba) = tcbIPCBufferSlot << objBits undefined then return (tcbIPCBufferFrame tcb) else fail
od | KOCTE cte \<Rightarrow> do unless (addr = fst (aa, ba)) $ haskell_fail [];
alignCheck addr (objBits cte);
magnitudeCheck addr (snd (lookupAround2 addr (ksPSpace s))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (aa, ba))) s)\<rbrakk> \<Longrightarrow> P b proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma getObject_ko_at:
  assumes x: "\<And>q n ko. loadObject p q n ko =
                (loadObject_default p q n ko :: ('a :: pspace_storable) kernel)"
  assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)"
  shows      "\<lbrace> \<top> \<rbrace> getObject p \<lbrace>\<lambda>r::'a::pspace_storable. ko_at' r p\<rbrace>" by (subst eq_commute, rule getObject_obj_at' [OF x P])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getObject p \<lbrace>\<lambda>r. ko_at' r p\<rbrace>