theory Syscall_DR

lemma handle_vm_fault_wp:
  "\<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>\<lambda>rv. P\<rbrace>" apply (case_tac vmfault_type) apply (simp) apply wp apply (clarsimp simp:do_machine_op_def getDFSR_def) apply wp apply (case_tac x) apply clarsimp apply (rule_tac P="P and (\<lambda>x. snd (aa,ba) = machine_state x)" in  hoare_post_imp) apply (assumption) apply (clarsimp simp:valid_def simpler_modify_def return_def bind_def) apply wp+ apply (clarsimp simp:gets_def alternative_def get_def bind_def select_def return_def) apply (clarsimp simp:do_machine_op_def getFAR_def) apply wp apply (case_tac x) apply clarsimp apply (rule_tac P="P and (\<lambda>x. snd (aa,ba) = machine_state x)" in  hoare_post_imp) apply (assumption) apply (clarsimp simp:valid_def simpler_modify_def return_def bind_def) apply wp+ apply (clarsimp simp:gets_def alternative_def select_def bind_def get_def return_def) apply simp apply wp apply (clarsimp simp:do_machine_op_def getIFSR_def) apply wp apply (case_tac x) apply clarsimp apply (rule_tac P="P and (\<lambda>x. snd (aa,ba) = machine_state x)" in  hoare_post_imp) apply (assumption) apply (clarsimp simp:valid_def simpler_modify_def return_def bind_def) apply wp+ apply (clarsimp simp:gets_def alternative_def select_def bind_def get_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 2. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>P\<rbrace> doE addr <- liftE (do_machine_op getFAR);
fault <- liftE (do_machine_op getDFSR);
throwError (ArchFault (VMFault addr [0, fault && mask 14]))
odE \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 2. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>addr. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B3 addr\<rbrace> do_machine_op getDFSR \<lbrace>\<lambda>fault s. P s \<and> True\<rbrace>
 2. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 4. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>addr. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B3 addr\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (gets DFSR_val ms);
y <- modify (update_machine ms');
return r
od \<lbrace>\<lambda>fault. P\<rbrace>
 2. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 4. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>addr ms x. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B15 addr ms x\<rbrace> case x of (r, ms') \<Rightarrow> do y <- modify (update_machine ms');
return r
od \<lbrace>\<lambda>fault. P\<rbrace>
 2. \<And>addr ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B14 addr ms\<rbrace> select_f (gets DFSR_val ms) \<lbrace>?B15 addr ms\<rbrace>
 3. \<And>addr. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B3 addr\<rbrace> gets machine_state \<lbrace>?B14 addr\<rbrace>
 4. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 6. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>addr ms x a b. \<lbrakk>vmfault_type = ARMDataAbort; x = (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?B15 addr ms x\<rbrace> case x of (r, ms') \<Rightarrow> do y <- modify (update_machine ms');
return r
od \<lbrace>\<lambda>fault. P\<rbrace>
 2. \<And>addr ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B14 addr ms\<rbrace> select_f (gets DFSR_val ms) \<lbrace>?B15 addr ms\<rbrace>
 3. \<And>addr. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B3 addr\<rbrace> gets machine_state \<lbrace>?B14 addr\<rbrace>
 4. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 6. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>addr ms aa ba. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B15 addr ms (aa, ba)\<rbrace> do y <- modify (update_machine ba);
return aa
od \<lbrace>\<lambda>fault. P\<rbrace>
 2. \<And>addr ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B14 addr ms\<rbrace> select_f (gets DFSR_val ms) \<lbrace>?B15 addr ms\<rbrace>
 3. \<And>addr. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B3 addr\<rbrace> gets machine_state \<lbrace>?B14 addr\<rbrace>
 4. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 6. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>addr ms aa ba rv s. \<lbrakk>vmfault_type = ARMDataAbort; ?Q24 addr ms aa ba rv s\<rbrakk> \<Longrightarrow> P s
 2. \<And>addr ms aa ba. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>P and (\<lambda>x. snd (aa, ba) = machine_state x)\<rbrace> do y <- modify (update_machine ba);
return aa
od \<lbrace>?Q24 addr ms aa ba\<rbrace>
 3. \<And>addr ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B14 addr ms\<rbrace> select_f (gets DFSR_val ms) \<lbrace>\<lambda>a. P and (\<lambda>x. snd a = machine_state x)\<rbrace>
 4. \<And>addr. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B3 addr\<rbrace> gets machine_state \<lbrace>?B14 addr\<rbrace>
 5. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 7. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>addr ms aa ba. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>P and (\<lambda>x. snd (aa, ba) = machine_state x)\<rbrace> do y <- modify (update_machine ba);
return aa
od \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>addr ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B14 addr ms\<rbrace> select_f (gets DFSR_val ms) \<lbrace>\<lambda>a. P and (\<lambda>x. snd a = machine_state x)\<rbrace>
 3. \<And>addr. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B3 addr\<rbrace> gets machine_state \<lbrace>?B14 addr\<rbrace>
 4. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 6. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>addr ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B14 addr ms\<rbrace> select_f (gets DFSR_val ms) \<lbrace>\<lambda>a. P and (\<lambda>x. snd a = machine_state x)\<rbrace>
 2. \<And>addr. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B3 addr\<rbrace> gets machine_state \<lbrace>?B14 addr\<rbrace>
 3. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> liftE (do_machine_op getFAR) \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 5. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (3 subgoals):
 1. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> do_machine_op getFAR \<lbrace>\<lambda>addr s. \<forall>x\<in>fst (gets DFSR_val (machine_state s)). (P and (\<lambda>xa. snd x = machine_state xa)) s\<rbrace>
 2. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (3 subgoals):
 1. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> do_machine_op getFAR \<lbrace>\<lambda>addr. P\<rbrace>
 2. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (3 subgoals):
 1. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (gets FAR_val ms);
y <- modify (update_machine ms');
return r
od \<lbrace>\<lambda>addr. P\<rbrace>
 2. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ms x. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B40 ms x\<rbrace> case x of (r, ms') \<Rightarrow> do y <- modify (update_machine ms');
return r
od \<lbrace>\<lambda>addr. P\<rbrace>
 2. \<And>ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B39 ms\<rbrace> select_f (gets FAR_val ms) \<lbrace>?B40 ms\<rbrace>
 3. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets machine_state \<lbrace>?B39\<rbrace>
 4. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 5. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ms x a b. \<lbrakk>vmfault_type = ARMDataAbort; x = (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?B40 ms x\<rbrace> case x of (r, ms') \<Rightarrow> do y <- modify (update_machine ms');
return r
od \<lbrace>\<lambda>addr. P\<rbrace>
 2. \<And>ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B39 ms\<rbrace> select_f (gets FAR_val ms) \<lbrace>?B40 ms\<rbrace>
 3. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets machine_state \<lbrace>?B39\<rbrace>
 4. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 5. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ms aa ba. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B40 ms (aa, ba)\<rbrace> do y <- modify (update_machine ba);
return aa
od \<lbrace>\<lambda>addr. P\<rbrace>
 2. \<And>ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B39 ms\<rbrace> select_f (gets FAR_val ms) \<lbrace>?B40 ms\<rbrace>
 3. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets machine_state \<lbrace>?B39\<rbrace>
 4. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 5. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ms aa ba rv s. \<lbrakk>vmfault_type = ARMDataAbort; ?Q49 ms aa ba rv s\<rbrakk> \<Longrightarrow> P s
 2. \<And>ms aa ba. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>P and (\<lambda>x. snd (aa, ba) = machine_state x)\<rbrace> do y <- modify (update_machine ba);
return aa
od \<lbrace>?Q49 ms aa ba\<rbrace>
 3. \<And>ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B39 ms\<rbrace> select_f (gets FAR_val ms) \<lbrace>\<lambda>a. P and (\<lambda>x. snd a = machine_state x)\<rbrace>
 4. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets machine_state \<lbrace>?B39\<rbrace>
 5. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 6. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ms aa ba. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>P and (\<lambda>x. snd (aa, ba) = machine_state x)\<rbrace> do y <- modify (update_machine ba);
return aa
od \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B39 ms\<rbrace> select_f (gets FAR_val ms) \<lbrace>\<lambda>a. P and (\<lambda>x. snd a = machine_state x)\<rbrace>
 3. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets machine_state \<lbrace>?B39\<rbrace>
 4. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 5. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ms. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?B39 ms\<rbrace> select_f (gets FAR_val ms) \<lbrace>\<lambda>a. P and (\<lambda>x. snd a = machine_state x)\<rbrace>
 2. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets machine_state \<lbrace>?B39\<rbrace>
 3. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> ?Q2 s
 4. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; P s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (gets FAR_val (machine_state s)). (P and (\<lambda>xa. snd x = machine_state xa)) s
 2. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P\<rbrace> doE pc <- liftE (as_user thread getRestartPC);
fault <- liftE (do_machine_op getIFSR);
throwError (ArchFault (VMFault pc [1, fault && mask 14]))
odE \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>pc. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B57 pc\<rbrace> do_machine_op getIFSR \<lbrace>\<lambda>fault s. P s \<and> True\<rbrace>
 2. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q56\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?B57\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>s. \<lbrakk>vmfault_type = ARMPrefetchAbort; P s\<rbrakk> \<Longrightarrow> ?Q56 s proof (prove)
goal (3 subgoals):
 1. \<And>pc. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B57 pc\<rbrace> do ms <- gets machine_state;
(r, ms') <- select_f (gets IFSR_val ms);
y <- modify (update_machine ms');
return r
od \<lbrace>\<lambda>fault. P\<rbrace>
 2. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q56\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?B57\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>s. \<lbrakk>vmfault_type = ARMPrefetchAbort; P s\<rbrakk> \<Longrightarrow> ?Q56 s proof (prove)
goal (5 subgoals):
 1. \<And>pc ms x. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B68 pc ms x\<rbrace> case x of (r, ms') \<Rightarrow> do y <- modify (update_machine ms');
return r
od \<lbrace>\<lambda>fault. P\<rbrace>
 2. \<And>pc ms. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B67 pc ms\<rbrace> select_f (gets IFSR_val ms) \<lbrace>?B68 pc ms\<rbrace>
 3. \<And>pc. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B57 pc\<rbrace> gets machine_state \<lbrace>?B67 pc\<rbrace>
 4. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q56\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?B57\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>s. \<lbrakk>vmfault_type = ARMPrefetchAbort; P s\<rbrakk> \<Longrightarrow> ?Q56 s proof (prove)
goal (5 subgoals):
 1. \<And>pc ms x a b. \<lbrakk>vmfault_type = ARMPrefetchAbort; x = (a, b)\<rbrakk> \<Longrightarrow> \<lbrace>?B68 pc ms x\<rbrace> case x of (r, ms') \<Rightarrow> do y <- modify (update_machine ms');
return r
od \<lbrace>\<lambda>fault. P\<rbrace>
 2. \<And>pc ms. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B67 pc ms\<rbrace> select_f (gets IFSR_val ms) \<lbrace>?B68 pc ms\<rbrace>
 3. \<And>pc. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B57 pc\<rbrace> gets machine_state \<lbrace>?B67 pc\<rbrace>
 4. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q56\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?B57\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>s. \<lbrakk>vmfault_type = ARMPrefetchAbort; P s\<rbrakk> \<Longrightarrow> ?Q56 s proof (prove)
goal (5 subgoals):
 1. \<And>pc ms aa ba. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B68 pc ms (aa, ba)\<rbrace> do y <- modify (update_machine ba);
return aa
od \<lbrace>\<lambda>fault. P\<rbrace>
 2. \<And>pc ms. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B67 pc ms\<rbrace> select_f (gets IFSR_val ms) \<lbrace>?B68 pc ms\<rbrace>
 3. \<And>pc. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B57 pc\<rbrace> gets machine_state \<lbrace>?B67 pc\<rbrace>
 4. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q56\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?B57\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>s. \<lbrakk>vmfault_type = ARMPrefetchAbort; P s\<rbrakk> \<Longrightarrow> ?Q56 s proof (prove)
goal (6 subgoals):
 1. \<And>pc ms aa ba rv s. \<lbrakk>vmfault_type = ARMPrefetchAbort; ?Q77 pc ms aa ba rv s\<rbrakk> \<Longrightarrow> P s
 2. \<And>pc ms aa ba. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P and (\<lambda>x. snd (aa, ba) = machine_state x)\<rbrace> do y <- modify (update_machine ba);
return aa
od \<lbrace>?Q77 pc ms aa ba\<rbrace>
 3. \<And>pc ms. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B67 pc ms\<rbrace> select_f (gets IFSR_val ms) \<lbrace>\<lambda>a. P and (\<lambda>x. snd a = machine_state x)\<rbrace>
 4. \<And>pc. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B57 pc\<rbrace> gets machine_state \<lbrace>?B67 pc\<rbrace>
 5. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q56\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?B57\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<And>s. \<lbrakk>vmfault_type = ARMPrefetchAbort; P s\<rbrakk> \<Longrightarrow> ?Q56 s proof (prove)
goal (5 subgoals):
 1. \<And>pc ms aa ba. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>P and (\<lambda>x. snd (aa, ba) = machine_state x)\<rbrace> do y <- modify (update_machine ba);
return aa
od \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>pc ms. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B67 pc ms\<rbrace> select_f (gets IFSR_val ms) \<lbrace>\<lambda>a. P and (\<lambda>x. snd a = machine_state x)\<rbrace>
 3. \<And>pc. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B57 pc\<rbrace> gets machine_state \<lbrace>?B67 pc\<rbrace>
 4. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q56\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?B57\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<And>s. \<lbrakk>vmfault_type = ARMPrefetchAbort; P s\<rbrakk> \<Longrightarrow> ?Q56 s proof (prove)
goal (4 subgoals):
 1. \<And>pc ms. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B67 pc ms\<rbrace> select_f (gets IFSR_val ms) \<lbrace>\<lambda>a. P and (\<lambda>x. snd a = machine_state x)\<rbrace>
 2. \<And>pc. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?B57 pc\<rbrace> gets machine_state \<lbrace>?B67 pc\<rbrace>
 3. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>?Q56\<rbrace> liftE (as_user thread getRestartPC) \<lbrace>?B57\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>s. \<lbrakk>vmfault_type = ARMPrefetchAbort; P s\<rbrakk> \<Longrightarrow> ?Q56 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmfault_type = ARMPrefetchAbort; P s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (gets IFSR_val (machine_state s)). (P and (\<lambda>xa. snd x = machine_state xa)) s proof (prove)
goal:
No subgoals!