kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_R

lemma setObject_pspace_domain_valid[wp]:
  "\<lbrace>pspace_domain_valid\<rbrace>
    setObject ptr val
   \<lbrace>\<lambda>rv. pspace_domain_valid\<rbrace>" apply (clarsimp simp: setObject_def split_def pspace_domain_valid_def
                        valid_def in_monad
                 split: if_split_asm) apply (drule updateObject_objBitsKO) apply (clarsimp simp: lookupAround2_char1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_domain_valid\<rbrace> setObject ptr val \<lbrace>\<lambda>rv. pspace_domain_valid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko a ba s''. \<lbrakk>fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); (ko, s'') \<in> fst (updateObject val ba ptr a (snd (lookupAround2 ptr (ksPSpace s))) s); \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}\<rbrakk> \<Longrightarrow> {a..a + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {} proof (prove)
goal (1 subgoal):
 1. \<And>s ko a ba s''. \<lbrakk>fst (lookupAround2 ptr (ksPSpace s)) = Some (a, ba); \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {}; objBitsKO ko = objBitsKO ba\<rbrakk> \<Longrightarrow> {a..a + 2 ^ objBitsKO ko - 1} \<inter> kernel_data_refs = {} proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma ct_not_inQ_lift:
  assumes sch_act: "\<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>"
      and not_inQ: "\<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
                    f \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>"
  shows "\<lbrace>ct_not_inQ\<rbrace> f \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" unfolding ct_not_inQ_def by (rule hoare_convert_imp [OF sch_act not_inQ])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> f \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> f \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
theory KHeap_R

lemma setNotification_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> setNotification ptr rval \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (rule ct_not_inQ_lift [OF setNotification_nosch]) apply (simp add: setNotification_def ct_not_inQ_def) apply (rule hoare_weaken_pre) apply (wps setObject_ntfn_ct) apply (rule obj_at_setObject2) apply (clarsimp simp add: updateObject_default_def in_monad)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> setNotification ptr rval \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> setNotification ptr rval \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> setObject ptr rval \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q10\<rbrace> setObject ptr rval \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q10 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P13 prev_s\<rbrace> setObject ptr rval \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?P13 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb)
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setNotification_ksCurThread[wp]:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setNotification a b \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>" apply (simp add: setNotification_def setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setNotification a b \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 a ps));
obj' <- updateObject_default b (snd p) a (fst p) (snd (lookupAround2 a ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setNotification_ksDomSchedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setNotification a b \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>" apply (simp add: setNotification_def setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setNotification a b \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 a ps));
obj' <- updateObject_default b (snd p) a (fst p) (snd (lookupAround2 a ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setNotification_ksDomScheduleId[wp]:
  "\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setNotification a b \<lbrace>\<lambda>rv s. P (ksDomScheduleIdx s)\<rbrace>" apply (simp add: setNotification_def setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setNotification a b \<lbrace>\<lambda>rv s. P (ksDomScheduleIdx s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 a ps));
obj' <- updateObject_default b (snd p) a (fst p) (snd (lookupAround2 a ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksDomScheduleIdx s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setNotification_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace> ct_idle_or_in_cur_domain' \<rbrace> setNotification ptr ntfn \<lbrace> \<lambda>_. ct_idle_or_in_cur_domain' \<rbrace>" apply (rule ct_idle_or_in_cur_domain'_lift) apply (wp hoare_vcg_disj_lift| rule obj_at_setObject2
           | clarsimp simp: updateObject_default_def in_monad setNotification_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 5. \<And>d a t t'. \<lbrace>\<lambda>s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace> setNotification ptr ntfn \<lbrace>\<lambda>_ s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma getEndpoint_wp:
  "\<lbrace>\<lambda>s. \<forall>ep. ko_at' ep e s \<longrightarrow> P ep s\<rbrace> getEndpoint e \<lbrace>P\<rbrace>" apply (rule hoare_strengthen_post) apply (rule get_ep_sp') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ep. ko_at' ep e s \<longrightarrow> P ep s\<rbrace> getEndpoint e \<lbrace>P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>ep. ko_at' ep e s \<longrightarrow> P ep s\<rbrace> getEndpoint e \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> P rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. ((\<lambda>s. \<forall>ep. ko_at' ep e s \<longrightarrow> P ep s) and ko_at' rv e) s \<Longrightarrow> P rv s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma getNotification_wp:
  "\<lbrace>\<lambda>s. \<forall>ntfn. ko_at' ntfn e s \<longrightarrow> P ntfn s\<rbrace> getNotification e \<lbrace>P\<rbrace>" apply (rule hoare_strengthen_post) apply (rule get_ntfn_sp') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ntfn. ko_at' ntfn e s \<longrightarrow> P ntfn s\<rbrace> getNotification e \<lbrace>P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>ntfn. ko_at' ntfn e s \<longrightarrow> P ntfn s\<rbrace> getNotification e \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> P rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. ((\<lambda>s. \<forall>ntfn. ko_at' ntfn e s \<longrightarrow> P ntfn s) and ko_at' rv e) s \<Longrightarrow> P rv s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma ep_redux_simps':
  "ep_q_refs_of' (case xs of [] \<Rightarrow> IdleEP | y # ys \<Rightarrow> SendEP xs)
        = (set xs \<times> {EPSend})"
  "ep_q_refs_of' (case xs of [] \<Rightarrow> IdleEP | y # ys \<Rightarrow> RecvEP xs)
        = (set xs \<times> {EPRecv})"
  "ntfn_q_refs_of' (case xs of [] \<Rightarrow> IdleNtfn | y # ys \<Rightarrow> WaitingNtfn xs)
        = (set xs \<times> {NTFNSignal})" by (fastforce split: list.splits
                simp: valid_ep_def valid_ntfn_def
              intro!: ext)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_q_refs_of' (case xs of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> Structures_H.endpoint.SendEP xs) = set xs \<times> {EPSend} &&& ep_q_refs_of' (case xs of [] \<Rightarrow> Structures_H.endpoint.IdleEP | y # ys \<Rightarrow> Structures_H.endpoint.RecvEP xs) = set xs \<times> {EPRecv} &&& ntfn_q_refs_of' (case xs of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn | y # ys \<Rightarrow> Structures_H.ntfn.WaitingNtfn xs) = set xs \<times> {NTFNSignal}
theory KHeap_R

lemma valid_refs'_def2:
  "valid_refs' R (ctes_of s) = (\<forall>cref. \<not>cte_wp_at' (\<lambda>c. R \<inter> capRange (cteCap c) \<noteq> {}) cref s)" by (auto simp: valid_refs'_def cte_wp_at_ctes_of ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_refs' R (ctes_of s) = (\<forall>cref. \<not> cte_wp_at' (\<lambda>c. R \<inter> capRange (cteCap c) \<noteq> {}) cref s)
theory KHeap_R

lemma idle_is_global [intro!]:
  "ksIdleThread s \<in> global_refs' s" by (simp add: global_refs'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksIdleThread s \<in> global_refs' s
theory KHeap_R

lemma valid_globals_cte_wpD':
  "\<lbrakk> valid_global_refs' s; cte_wp_at' P p s \<rbrakk>
       \<Longrightarrow> \<exists>cte. P cte \<and> ksIdleThread s \<notin> capRange (cteCap cte)" by (fastforce simp: valid_global_refs'_def valid_refs'_def  cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_refs' s; cte_wp_at' P p s\<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> ksIdleThread s \<notin> capRange (cteCap cte)
theory KHeap_R

lemma dmo_aligned'[wp]:
  "\<lbrace>pspace_aligned'\<rbrace> doMachineOp f \<lbrace>\<lambda>_. pspace_aligned'\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> doMachineOp f \<lbrace>\<lambda>_. pspace_aligned'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. pspace_aligned'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned' s \<Longrightarrow> \<forall>x\<in>fst (f (ksMachineState s)). pspace_aligned' (s\<lparr>ksMachineState := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma dmo_distinct'[wp]:
  "\<lbrace>pspace_distinct'\<rbrace> doMachineOp f \<lbrace>\<lambda>_. pspace_distinct'\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct'\<rbrace> doMachineOp f \<lbrace>\<lambda>_. pspace_distinct'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct'\<rbrace> do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. pspace_distinct'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_distinct' s \<Longrightarrow> \<forall>x\<in>fst (f (ksMachineState s)). pspace_distinct' (s\<lparr>ksMachineState := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma dmo_valid_objs'[wp]:
  "\<lbrace>valid_objs'\<rbrace> doMachineOp f \<lbrace>\<lambda>_. valid_objs'\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> doMachineOp f \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<Longrightarrow> \<forall>x\<in>fst (f (ksMachineState s)). valid_objs' (s\<lparr>ksMachineState := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma dmo_inv':
  assumes R: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  shows "\<lbrace>P\<rbrace> doMachineOp f \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp apply (drule in_inv_by_hoareD [OF R]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doMachineOp f \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> \<forall>x\<in>fst (f (ksMachineState s)). P (s\<lparr>ksMachineState := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f (ksMachineState s))\<rbrakk> \<Longrightarrow> P (s\<lparr>ksMachineState := b\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; b = ksMachineState s\<rbrakk> \<Longrightarrow> P (s\<lparr>ksMachineState := b\<rparr>) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma doMachineOp_invs_bits[wp]:
  "\<lbrace>valid_pspace'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>"
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
     doMachineOp m \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>"
  "\<lbrace>Invariants_H.valid_queues\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>"
  "\<lbrace>valid_queues'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. valid_queues'\<rbrace>"
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>
      doMachineOp m
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>"
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>"
  "\<lbrace>cur_tcb'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>"
  "\<lbrace>if_unsafe_then_cap'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" by (simp add: doMachineOp_def split_def
                valid_pspace'_def valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs
       | wp cur_tcb_lift sch_act_wf_lift tcb_in_cur_domain'_lift
       | fastforce elim: state_refs_of'_pspaceI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lbrace>valid_pspace'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> &&& \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> doMachineOp m \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>) &&& \<lbrace>Invariants_H.valid_queues\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> &&& \<lbrace>valid_queues'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. valid_queues'\<rbrace>) &&& (\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> doMachineOp m \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> &&& \<lbrace>if_live_then_nonz_cap'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>) &&& \<lbrace>cur_tcb'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> &&& \<lbrace>if_unsafe_then_cap'\<rbrace> doMachineOp m \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>
theory KHeap_R

lemma setEndpoint_ksMachine:
  "\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>" by (simp add: setEndpoint_def | wp setObject_ksMachine updateObject_default_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>
theory KHeap_R

lemma setEndpoint_ct':
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setEndpoint a b \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>" apply (simp add: setEndpoint_def setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setEndpoint a b \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 a ps));
obj' <- updateObject_default b (snd p) a (fst p) (snd (lookupAround2 a ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory EmptyFail

lemma empty_fail_projectKO [simp, intro!]:
  "empty_fail (projectKO v)" unfolding empty_fail_def projectKO_def by (simp add: return_def fail_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (projectKO v) proof (prove)
goal (1 subgoal):
 1. \<forall>s. fst ((case projectKO_opt v of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {} \<longrightarrow> snd ((case projectKO_opt v of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s)
theory EmptyFail

lemma empty_fail_alignCheck [intro!, wp, simp]:
  "empty_fail (alignCheck a b)" unfolding alignCheck_def by (fastforce simp: alignError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (alignCheck a b) proof (prove)
goal (1 subgoal):
 1. empty_fail (unless (a && mask b = 0) $ alignError b)
theory EmptyFail

lemma empty_fail_magnitudeCheck [intro!, wp, simp]:
  "empty_fail (magnitudeCheck a b c)" unfolding magnitudeCheck_def by (fastforce split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (magnitudeCheck a b c) proof (prove)
goal (1 subgoal):
 1. empty_fail (case b of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - a < 1 << c) fail)
theory EmptyFail

lemma empty_fail_loadObject_default [intro!, wp, simp]:
  shows "empty_fail (loadObject_default x b c d)" by (auto simp: loadObject_default_def
           split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (loadObject_default x b c d)
theory EmptyFail

lemma empty_fail_threadGet [intro!, wp, simp]:
  "empty_fail (threadGet f p)" by (fastforce simp: threadGet_def getObject_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (threadGet f p)
theory EmptyFail

lemma empty_fail_setCTE [intro!, wp, simp]:
  "empty_fail (setCTE p cte)" unfolding setCTE_def by (fastforce simp: setObject_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (setCTE p cte) proof (prove)
goal (1 subgoal):
 1. empty_fail (setObject p cte)
theory EmptyFail

lemma empty_fail_updateMDB [intro!, wp, simp]:
  "empty_fail (updateMDB a b)" unfolding updateMDB_def Let_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (updateMDB a b) proof (prove)
goal (1 subgoal):
 1. empty_fail (if a = 0 then return () else do cte <- getCTE a;
mdb <- return (cteMDBNode cte);
mdb' <- return (b mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE a
od)
theory EmptyFail

lemma empty_fail_getSlotCap [intro!, wp, simp]:
  "empty_fail (getSlotCap a)" unfolding getSlotCap_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getSlotCap a) proof (prove)
goal (1 subgoal):
 1. empty_fail (do cte <- getCTE a;
return $ cteCap cte
od)
theory EmptyFail

lemma empty_fail_getObject:
  assumes "\<And>b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel)"
  shows "empty_fail (getObject x :: 'a :: pspace_storable kernel)" apply (simp add: getObject_def split_def) apply (safe intro!: assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getObject x) proof (prove)
goal (1 subgoal):
 1. empty_fail (do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 x map));
loadObject x (fst p) (snd (lookupAround2 x map)) (snd p)
od) proof (prove)
goal:
No subgoals!
theory EmptyFail

lemma empty_fail_getObject_tcb [intro!, wp, simp]:
  shows "empty_fail (getObject x :: tcb kernel)" by (auto intro: empty_fail_getObject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getObject x)
theory EmptyFail

lemma empty_fail_updateTrackedFreeIndex [intro!, wp, simp]:
  shows "empty_fail (updateTrackedFreeIndex p idx)" by (fastforce simp add: updateTrackedFreeIndex_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (updateTrackedFreeIndex p idx)
theory EmptyFail

lemma empty_fail_insertNewCap [intro!, wp, simp]:
  "empty_fail (insertNewCap p p' cap)" unfolding insertNewCap_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (insertNewCap p p' cap) proof (prove)
goal (1 subgoal):
 1. empty_fail (do next <- liftM (mdbNext \<circ> cteMDBNode) $ getCTE p;
oldCTE <- getCTE p';
haskell_assert (isNullCap (cteCap oldCTE) \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer) [];
setCTE p' $ CTE cap (MDB next p True True);
updateMDB next $ mdbPrev_update (\<lambda>_. p');
updateMDB p $ mdbNext_update (\<lambda>_. p');
updateNewFreeIndex p'
od)
theory EmptyFail

lemma empty_fail_getIRQSlot [intro!, wp, simp]:
  "empty_fail (getIRQSlot irq)" by (fastforce simp: getIRQSlot_def getInterruptState_def locateSlot_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getIRQSlot irq)
theory EmptyFail

lemma empty_fail_getObject_ntfn [intro!, wp, simp]:
  "empty_fail (getObject p :: Structures_H.notification kernel)" by (simp add: empty_fail_getObject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getObject p)