theory Syscall_S

lemma call_kernel_bisim:
  "bisim (=) \<top> (separate_state and cur_tcb and valid_objs) (call_kernel ev) (Syscall_A.call_kernel ev)" unfolding call_kernel_def Syscall_A.call_kernel_def apply (rule bisim_guard_imp_both) apply simp apply (rule bisim_split) apply (rule bisim_split_handle) apply (rule handle_event_bisim) apply simp apply (rule bisim_refl') apply wp+ apply (rule bisim_refl') apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (Syscall_SA.call_kernel ev) (Syscall_A.call_kernel ev) proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (separate_state and cur_tcb and valid_objs) (do Syscall_SA.handle_event ev <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op (getActiveIRQ True);
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od) (do Syscall_A.handle_event ev <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od) proof (prove)
goal (2 subgoals):
 1. bisim (=) ?P ?P' (do Syscall_SA.handle_event ev <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op (getActiveIRQ True);
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od) (do Syscall_A.handle_event ev <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od)
 2. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (2 subgoals):
 1. bisim (=) ?P ?P' (do y <- Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od) (do y <- Syscall_A.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od)
 2. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (5 subgoals):
 1. bisim ?R'3 ?P3 ?P'3 (Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od))) (Syscall_A.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)))
 2. \<And>r r'. ?R'3 r r' \<Longrightarrow> bisim (=) (?Q3 r) (?Q'3 r') (do y <- schedule;
activate_thread
od) (do y <- schedule;
activate_thread
od)
 3. \<lbrace>?S3\<rbrace> Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q3\<rbrace>
 4. \<lbrace>?S'3\<rbrace> Syscall_A.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q'3\<rbrace>
 5. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> (?P3 and ?S3) s \<and> (?P'3 and ?S'3) s proof (prove)
goal (8 subgoals):
 1. bisim (?f'8 \<oplus> ?r8) ?Pn8 ?Pn'8 (Syscall_SA.handle_event ev) (Syscall_A.handle_event ev)
 2. \<And>x x'. ?f'8 x x' \<Longrightarrow> bisim (?f8 \<oplus> ?r8) (?Pf8 x) (?Pf'8 x') (liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) (liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od))
 3. \<lbrace>?P8\<rbrace> Syscall_SA.handle_event ev \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?Pf8\<rbrace>
 4. \<lbrace>?P'8\<rbrace> Syscall_A.handle_event ev \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?Pf'8\<rbrace>
 5. \<And>r r'. (?f8 \<oplus> ?r8) r r' \<Longrightarrow> bisim (=) (?Q3 r) (?Q'3 r') (do y <- schedule;
activate_thread
od) (do y <- schedule;
activate_thread
od)
 6. \<lbrace>?S3\<rbrace> Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q3\<rbrace>
 7. \<lbrace>?S'3\<rbrace> Syscall_A.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q'3\<rbrace>
 8. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> (?Pn8 and ?P8 and ?S3) s \<and> (?Pn'8 and ?P'8 and ?S'3) s proof (prove)
goal (7 subgoals):
 1. \<And>x x'. dc x x' \<Longrightarrow> bisim (?f8 \<oplus> (=)) (?Pf8 x) (?Pf'8 x') (liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) (liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od))
 2. \<lbrace>?P8\<rbrace> Syscall_SA.handle_event ev \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?Pf8\<rbrace>
 3. \<lbrace>?P'8\<rbrace> Syscall_A.handle_event ev \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?Pf'8\<rbrace>
 4. \<And>r r'. (?f8 \<oplus> (=)) r r' \<Longrightarrow> bisim (=) (?Q3 r) (?Q'3 r') (do y <- schedule;
activate_thread
od) (do y <- schedule;
activate_thread
od)
 5. \<lbrace>?S3\<rbrace> Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q3\<rbrace>
 6. \<lbrace>?S'3\<rbrace> Syscall_A.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q'3\<rbrace>
 7. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?P8 and ?S3) s \<and> (separate_state and cur_tcb and valid_objs and ?P'8 and ?S'3) s proof (prove)
goal (7 subgoals):
 1. bisim (=) (?Pf8 ()) (?Pf'8 ()) (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od) (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)
 2. \<lbrace>?P8\<rbrace> Syscall_SA.handle_event ev \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?Pf8\<rbrace>
 3. \<lbrace>?P'8\<rbrace> Syscall_A.handle_event ev \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?Pf'8\<rbrace>
 4. \<And>r r'. (?f8 \<oplus> (=)) r r' \<Longrightarrow> bisim (=) (?Q3 r) (?Q'3 r') (do y <- schedule;
activate_thread
od) (do y <- schedule;
activate_thread
od)
 5. \<lbrace>?S3\<rbrace> Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q3\<rbrace>
 6. \<lbrace>?S'3\<rbrace> Syscall_A.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q'3\<rbrace>
 7. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?P8 and ?S3) s \<and> (separate_state and cur_tcb and valid_objs and ?P'8 and ?S'3) s proof (prove)
goal (6 subgoals):
 1. \<lbrace>?P8\<rbrace> Syscall_SA.handle_event ev \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<lbrace>?P'8\<rbrace> Syscall_A.handle_event ev \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>r r'. (?f8 \<oplus> (=)) r r' \<Longrightarrow> bisim (=) (?Q3 r) (?Q'3 r') (do y <- schedule;
activate_thread
od) (do y <- schedule;
activate_thread
od)
 4. \<lbrace>?S3\<rbrace> Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q3\<rbrace>
 5. \<lbrace>?S'3\<rbrace> Syscall_A.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q'3\<rbrace>
 6. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?P8 and ?S3) s \<and> (separate_state and cur_tcb and valid_objs and ?P'8 and ?S'3) s proof (prove)
goal (4 subgoals):
 1. \<And>r r'. (?f8 \<oplus> (=)) r r' \<Longrightarrow> bisim (=) (?Q3 r) (?Q'3 r') (do y <- schedule;
activate_thread
od) (do y <- schedule;
activate_thread
od)
 2. \<lbrace>?S3\<rbrace> Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q3\<rbrace>
 3. \<lbrace>?S'3\<rbrace> Syscall_A.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>?Q'3\<rbrace>
 4. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True) and ?S3) s \<and> (separate_state and cur_tcb and valid_objs and (\<lambda>s. True \<and> True) and ?S'3) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?S3\<rbrace> Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>\<lambda>r _. True\<rbrace>
 2. \<lbrace>?S'3\<rbrace> Syscall_A.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od)) \<lbrace>\<lambda>r' _. True\<rbrace>
 3. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True) and ?S3) s \<and> (separate_state and cur_tcb and valid_objs and (\<lambda>s. True \<and> True) and ?S'3) s proof (prove)
goal:
No subgoals!