theory ArchInterrupt_AI

lemma resetTimer_invs_ARCH[Interrupt_AI_asms]:
  "\<lbrace>invs\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. invs\<rbrace>" apply (wp dmo_invs) apply safe apply (drule_tac Q="%_ b. underlying_memory b p = underlying_memory m p"
                 in use_valid) apply (simp add: resetTimer_def
                      machine_op_lift_def machine_rest_lift_def split_def) apply wp apply (clarsimp+)[2] apply(erule use_valid, wp no_irq_resetTimer no_irq, assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op resetTimer \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (resetTimer m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s proof (prove)
goal (2 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; ((), b) \<in> fst (resetTimer m); underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (resetTimer (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (4 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s m b p\<rbrace> resetTimer \<lbrace>\<lambda>_ b. underlying_memory b p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P19 s m b p m
 3. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 4. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (resetTimer (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (4 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s m b p\<rbrace> do mr <- gets machine_state_rest;
p <- select_f (ignore_failure resetTimer_impl mr);
modify (machine_state_rest_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_ b. underlying_memory b p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P19 s m b p m
 3. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 4. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (resetTimer (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (ignore_failure resetTimer_impl (machine_state_rest m)). underlying_memory (m\<lparr>machine_state_rest := snd x\<rparr>) p = underlying_memory m p
 2. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 3. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (resetTimer (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (1 subgoal):
 1. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (resetTimer (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal:
No subgoals!