kings-crown/FVELER_Isabelle huggingface dataset:
theory PageTableDuplicates

lemma cteDelete_valid_duplicates':
  "\<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and K ex\<rbrace>
  cteDelete ptr ex
  \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: cteDelete_def whenE_def split_def) apply (rule hoare_pre, wp finaliseSlot_invs) apply (rule valid_validE) apply (rule hoare_post_imp[OF _ finaliseSlot_valid_duplicates']) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and K ex\<rbrace> cteDelete ptr ex \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. ex \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple\<rbrace> cteDelete ptr ex \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. ex \<Longrightarrow> \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple\<rbrace> doE p <- finaliseSlot ptr True;
liftE (emptySlot ptr (snd p))
odE \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. ex \<Longrightarrow> \<lbrace>?Q2\<rbrace> finaliseSlot ptr True \<lbrace>\<lambda>p s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s. \<lbrakk>ex; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. ex \<Longrightarrow> \<lbrace>?Q2\<rbrace> finaliseSlot ptr True \<lbrace>\<lambda>p s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s. \<lbrakk>ex; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>ex; invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 2. \<And>s. \<lbrakk>ex; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple) s\<rbrakk> \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ex; (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple) s\<rbrakk> \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s \<and> (\<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s) proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma cteRevoke_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. invs' s
        \<and> vs_valid_duplicates' (ksPSpace s)
        \<and> sch_act_simple s \<rbrace>
    cteRevoke cte
  \<lbrace>\<lambda>_ s. invs' s
       \<and> vs_valid_duplicates' (ksPSpace s)
       \<and> sch_act_simple s \<rbrace>" apply (rule cteRevoke_preservation) apply (wp cteDelete_invs' cteDelete_valid_duplicates' cteDelete_sch_act_simple) apply (simp add:cteDelete_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s\<rbrace> cteRevoke cte \<lbrace>\<lambda>_ s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s ptr. \<lbrace>\<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s\<rbrace> cteDelete ptr True \<lbrace>\<lambda>_ s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s\<rbrace>
 2. \<And>s f sa. (invs' (ksWorkUnitsCompleted_update f sa) \<and> vs_valid_duplicates' (ksPSpace (ksWorkUnitsCompleted_update f sa)) \<and> sch_act_simple (ksWorkUnitsCompleted_update f sa)) = (invs' sa \<and> vs_valid_duplicates' (ksPSpace sa) \<and> sch_act_simple sa)
 3. \<And>s. irq_state_independent_H (\<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s) proof (prove)
goal (3 subgoals):
 1. \<And>s ptr sa. invs' sa \<and> vs_valid_duplicates' (ksPSpace sa) \<and> sch_act_simple sa \<Longrightarrow> (invs' and sch_act_simple and K True) sa \<and> (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and K True) sa \<and> (invs' and sch_act_simple and (\<lambda>s. \<not> True \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) ptr s)) sa
 2. \<And>s f sa. (invs' (ksWorkUnitsCompleted_update f sa) \<and> vs_valid_duplicates' (ksPSpace (ksWorkUnitsCompleted_update f sa)) \<and> sch_act_simple (ksWorkUnitsCompleted_update f sa)) = (invs' sa \<and> vs_valid_duplicates' (ksPSpace sa) \<and> sch_act_simple sa)
 3. \<And>s. irq_state_independent_H (\<lambda>s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> sch_act_simple s) proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma mapM_x_storePTE_invalid_whole:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and>
        s \<turnstile>' capability.ArchObjectCap (arch_capability.PageTableCap word option) \<and>
        pspace_aligned' s\<rbrace>
   mapM_x (swp storePTE InvalidPTE) [word , word + 2 ^ pteBits .e. word + 2 ^ ptBits - 1]
   \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (wp mapM_x_storePTE_update_helper[where word = word and sz = ptBits and ptr = word]) apply (clarsimp simp: valid_cap'_def capAligned_def pageBits_def ptBits_def objBits_simps
                        archObjSize_def pteBits_def) apply (simp add: mask_def field_simps pteBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<and> valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap word option)) s \<and> pspace_aligned' s\<rbrace> mapM_x (swp storePTE ARM_H.InvalidPTE) [word , word + 2 ^ pteBits .e. word + 2 ^ ptBits - 1] \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<and> valid_cap' (capability.ArchObjectCap (arch_capability.PageTableCap word option)) s \<and> pspace_aligned' s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s) \<and> pspace_aligned' s \<and> page_table_at' word s \<and> word && ~~ mask ptBits = word \<and> ptBits \<le> ptBits \<and> 6 \<le> ptBits \<and> is_aligned word ptBits \<and> [word , word + 2 ^ pteBits .e. word + 2 ^ ptBits - 1] = [word , word + 4 .e. word + mask ptBits] proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vs_valid_duplicates' (ksPSpace s); is_aligned word 10; 10 < word_bits; page_table_at' word s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase; pspace_aligned' s\<rbrakk> \<Longrightarrow> [word , word + 4 .e. 0x3FF + word] = [word , word + 4 .e. word + mask 10] proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma invokeIRQControl_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s) \<rbrace> performIRQControl a
  \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add:performIRQControl_def ) apply (rule hoare_pre) apply (wp|wpc | simp add:ARM_H.performIRQControl_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> global.performIRQControl a \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> case a of irqcontrol_invocation.ArchIRQControl invok \<Rightarrow> Arch.performIRQControl invok | Invocations_H.irqcontrol_invocation.IssueIRQHandler irq handlerSlot controlSlot \<Rightarrow> withoutPreemption $ do setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) controlSlot handlerSlot
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case a of irqcontrol_invocation.ArchIRQControl invok \<Rightarrow> Arch.performIRQControl invok | Invocations_H.irqcontrol_invocation.IssueIRQHandler irq handlerSlot controlSlot \<Rightarrow> withoutPreemption $ do setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) controlSlot handlerSlot
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma getObject_pte_sp:
  "\<lbrace>P\<rbrace> getObject r \<lbrace>\<lambda>t::pte. P and ko_at' t r\<rbrace>" apply (wp getObject_ko_at) apply (auto simp: objBits_simps archObjSize_def pteBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getObject r \<lbrace>\<lambda>t. P and ko_at' t r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>q n ko. loadObject r q n ko = loadObject_default r q n ko
 2. \<And>v. 1 < 2 ^ objBits v
 3. \<And>s. P s \<Longrightarrow> P s \<and> True proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma getObject_pde_sp:
  "\<lbrace>P\<rbrace> getObject r \<lbrace>\<lambda>t::pde. P and ko_at' t r\<rbrace>" apply (wp getObject_ko_at) apply (auto simp: objBits_simps archObjSize_def pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getObject r \<lbrace>\<lambda>t. P and ko_at' t r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>q n ko. loadObject r q n ko = loadObject_default r q n ko
 2. \<And>v. 1 < 2 ^ objBits v
 3. \<And>s. P s \<Longrightarrow> P s \<and> True proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma hi_valid_duplicates'[wp]:
  "\<lbrace>invs' and sch_act_simple and ct_active'
    and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
      handleInvocation isCall isBlocking
   \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s) \<rbrace>" apply (simp add: handleInvocation_def split_def
                   ts_Restart_case_helper') apply (wp syscall_valid' setThreadState_nonqueued_state_update
    rfk_invs' ct_in_state'_set | simp)+ apply (fastforce simp add: tcb_at_invs' ct_in_state'_def
                              simple_sane_strg
                              sch_act_simple_def
                       elim!: pred_tcb'_weakenE st_tcb_ex_cap''
                        dest: st_tcb_at_idle_thread')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> handleInvocation isCall isBlocking \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> doE thread <- liftE getCurThread;
info <- liftE (getMessageInfo thread);
ptr <- liftE (asUser thread (getRegister Thread_H.capRegister));
Syscall_H.syscall (doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when isBlocking (handleFault thread fault)) (\<lambda>p. doE args <- liftE (getMRs thread (snd (snd (snd p))) info);
global.decodeInvocation (msgLabel info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when isCall (replyFromKernel thread (msgFromSyscallError err))) (\<lambda>oper. doE y <- liftE (setThreadState Structures_H.thread_state.Restart thread);
reply <- global.performInvocation isBlocking isCall oper;
liftE (do state <- getThreadState thread;
if state = Structures_H.thread_state.Restart then do y <- when isCall (replyFromKernel thread (0, reply));
setThreadState Structures_H.thread_state.Running thread
od else return ()
od)
odE)
odE \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> sch_act_simple s \<and> ct_active' s \<and> vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> valid_objs' s \<and> tcb_at' (ksCurThread s) s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> valid_objs' s \<and> tcb_at' (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma timerTick_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
  timerTick \<lbrace>\<lambda>x s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add:timerTick_def decDomainTime_def) apply (wp hoare_drop_imps|wpc|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> timerTick \<lbrace>\<lambda>x s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> do thread <- getCurThread;
state <- getThreadState thread;
y <- case state of Structures_H.thread_state.Running \<Rightarrow> do ts <- threadGet tcbTimeSlice thread;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread;
tcbSchedAppend thread;
rescheduleRequired
od
od | _ \<Rightarrow> return ();
when (Suc 0 < numDomains) (do y <- modify (\<lambda>ks. ks\<lparr>ksDomainTime := ksDomainTime ks - 1\<rparr>);
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od \<lbrace>\<lambda>x s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma handleInterrupt_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
  handleInterrupt irq \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add: handleInterrupt_def) apply (rule conjI; rule impI) apply (wp hoare_vcg_all_lift hoare_drop_imps
             threadSet_pred_tcb_no_state getIRQState_inv haskell_fail_wp
          |wpc|simp add: handleReservedIRQ_def maskIrqSignal_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> handleInterrupt irq \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (maxIRQ < irq \<longrightarrow> \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> doMachineOp (do y <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>) \<and> (\<not> maxIRQ < irq \<longrightarrow> \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> do st <- getIRQState irq;
y <- case st of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>) proof (prove)
goal (2 subgoals):
 1. maxIRQ < irq \<Longrightarrow> \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> doMachineOp (do y <- maskInterrupt True irq;
ackInterrupt irq
od) \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<not> maxIRQ < irq \<Longrightarrow> \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> do st <- getIRQState irq;
y <- case st of irqstate.IRQInactive \<Rightarrow> haskell_fail $ [] @ show irq | irqstate.IRQSignal \<Rightarrow> do slot <- getIRQSlot irq;
cap <- getSlotCap slot;
case cap of capability.NotificationCap x xa True xb \<Rightarrow> sendSignal (capNtfnPtr cap) (capNtfnBadge cap) | capability.NotificationCap x xa False xb \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq | _ \<Rightarrow> doMachineOp $ debugPrint $ [] @ show irq;
maskIrqSignal irq
od | irqstate.IRQTimer \<Rightarrow> do timerTick;
doMachineOp resetTimer
od | irqstate.IRQReserved \<Rightarrow> handleReservedIRQ irq;
doMachineOp (ackInterrupt irq)
od \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma hs_valid_duplicates'[wp]:
  "\<lbrace>invs' and ct_active' and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>
  handleSend blocking \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (rule validE_valid) apply (simp add: handleSend_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> handleSend blocking \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> handleSend blocking \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and sch_act_simple and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> handleInvocation False blocking \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Refine

lemma device_mem_relation:
  "\<lbrakk>(s,s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk>
   \<Longrightarrow> device_mem' s' = device_mem s" apply (rule ext) apply (clarsimp simp: device_mem_def device_mem'_def pointerInUserData_relation
     pointerInDeviceData_relation) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> device_mem' s' = device_mem s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(s, s') \<in> state_relation; valid_state' s'; valid_state s\<rbrakk> \<Longrightarrow> device_mem' s' x = device_mem s x proof (prove)
goal:
No subgoals!
theory Refine

lemma activate_thread_sched_act:
  "\<lbrace>ct_in_state activatable and (\<lambda>s. P (scheduler_action s))\<rbrace>
  activate_thread
  \<lbrace>\<lambda>rs s. P (scheduler_action (s::det_state))\<rbrace>" by (simp add: activate_thread_def set_thread_state_def arch_activate_idle_thread_def
      | (wp set_thread_state_sched_act gts_wp)+ | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state activatable and (\<lambda>s. P (scheduler_action s))\<rbrace> activate_thread \<lbrace>\<lambda>rs s. P (scheduler_action s)\<rbrace>
theory Refine

lemma schedule_sched_act_rct[wp]:
  "\<lbrace>\<top>\<rbrace> Schedule_A.schedule
  \<lbrace>\<lambda>rs (s::det_state). scheduler_action s = resume_cur_thread\<rbrace>" unfolding Schedule_A.schedule_def by (wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> state_ext_sched_class.schedule \<lbrace>\<lambda>rs s. scheduler_action s = resume_cur_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od \<lbrace>\<lambda>rs s. scheduler_action s = resume_cur_thread\<rbrace>
theory Refine

lemma call_kernel_sched_act_rct[wp]:
  "\<lbrace>einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)
     and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace>
  call_kernel e
  \<lbrace>\<lambda>rs (s::det_state). scheduler_action s = resume_cur_thread\<rbrace>" apply (simp add: call_kernel_def) apply (wp activate_thread_sched_act | simp)+ apply (clarsimp simp: active_from_running) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> call_kernel e \<lbrace>\<lambda>rs s. scheduler_action s = resume_cur_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and (\<lambda>s. scheduler_action s = resume_cur_thread)\<rbrace> do y <- handle_event e <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- state_ext_sched_class.schedule;
activate_thread
od \<lbrace>\<lambda>rs s. scheduler_action s = resume_cur_thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> valid_list s \<and> valid_sched s \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running s) \<and> scheduler_action s = resume_cur_thread \<Longrightarrow> e \<noteq> Interrupt \<longrightarrow> ct_active s proof (prove)
goal:
No subgoals!
theory Refine

lemma do_user_op_valid_list:"\<lbrace>valid_list\<rbrace> do_user_op f tc \<lbrace>\<lambda>_. valid_list\<rbrace>" unfolding do_user_op_def apply (wp | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do_user_op f tc \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> do t <- gets cur_thread;
conv <- gets (ptable_lift t);
rights <- gets (ptable_rights t);
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
(e, tc', um', ds') <- select (fst (f t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va})));
do_machine_op (user_memory_update ((um' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
do_machine_op (device_memory_update ((ds' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (e, tc')
od \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal:
No subgoals!