theory PageTableDuplicates

lemma callKernel_valid_duplicates':
  "\<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
    (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
    (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)\<rbrace>
   callKernel e
   \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add: callKernel_def fastpathKernelAssertions_def) apply (rule hoare_pre) apply (wp activate_invs' activate_sch_act schedule_sch
             schedule_sch_act_simple he_invs'
          | simp add: no_irq_getActiveIRQ
          | wp (once) hoare_drop_imps )+ apply (rule hoare_post_impErr) apply (rule valid_validE) prefer 2 apply assumption apply (wp handleEvent_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 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)\<rbrace> callKernel e \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)\<rbrace> do y <- handleEvent e <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od));
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- handleEvent e <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od));
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'31\<rbrace> handleEvent e \<lbrace>\<lambda>x s. invs' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>, \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> ?P'31 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'31\<rbrace> handleEvent e \<lbrace>?Q34\<rbrace>, \<lbrace>?E34\<rbrace>
 2. \<And>rv s. ?Q34 rv s \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s)
 3. \<And>e s. ?E34 e s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 4. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> ?P'31 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'31\<rbrace> handleEvent e \<lbrace>\<lambda>_. ?E40\<rbrace>
 2. \<And>rv s. ?E40 s \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s)
 3. \<And>e s. ?E40 s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 4. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> ?P'31 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. ?E40 s \<Longrightarrow> invs' s \<and> vs_valid_duplicates' (ksPSpace s)
 2. \<lbrace>?P'31\<rbrace> handleEvent e \<lbrace>\<lambda>_. ?E40\<rbrace>
 3. \<And>e s. ?E40 s \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 4. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> ?P'31 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'31\<rbrace> handleEvent e \<lbrace>\<lambda>_ s. invs' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>e s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 3. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> ?P'31 s proof (prove)
goal (2 subgoals):
 1. \<And>e s. invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 2. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s \<Longrightarrow> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<and> (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and sch_act_simple and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s)) s proof (prove)
goal:
No subgoals!