kings-crown/FVELER_Isabelle huggingface dataset:
theory Bits_R

lemma getIdleThread_corres [corres]:
  "corres (=) \<top> \<top> (gets idle_thread) getIdleThread" by (simp add: getIdleThread_def state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets idle_thread) getIdleThread
theory Bits_R

lemma git_wp [wp]: "\<lbrace>\<lambda>s. P (ksIdleThread s) s\<rbrace> getIdleThread \<lbrace>P\<rbrace>" by (unfold getIdleThread_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s) s\<rbrace> getIdleThread \<lbrace>P\<rbrace>
theory Bits_R

lemma gsa_wp [wp]: "\<lbrace>\<lambda>s. P (ksSchedulerAction s) s\<rbrace> getSchedulerAction \<lbrace>P\<rbrace>" by (unfold getSchedulerAction_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s) s\<rbrace> getSchedulerAction \<lbrace>P\<rbrace>
theory Bits_R

lemma rethrowFailure_injection:
  "rethrowFailure = injection_handler" by (intro ext, simp add: rethrowFailure_def injection_handler_def o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rethrowFailure = injection_handler
theory Bits_R

lemma lookupError_injection:
 "lookupErrorOnFailure b = injection_handler (Fault_H.FailedLookup b)" apply (rule ext) apply (simp add: lookupErrorOnFailure_def rethrowFailure_injection) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lookupErrorOnFailure b = injection_handler (Fault_H.syscall_error.FailedLookup b) proof (prove)
goal (1 subgoal):
 1. \<And>x. lookupErrorOnFailure b x = injection_handler (Fault_H.syscall_error.FailedLookup b) x proof (prove)
goal:
No subgoals!
theory Bits_R

lemma corres_cap_fault:
  "corres (lfr \<oplus> r) P P' f g \<Longrightarrow>
   corres (fr \<oplus> r) P P' (cap_fault_on_failure addr b f)
                        (capFaultOnFailure addr b g)" by (fastforce intro: corres_injection[where f'=lfr]
         simp: cap_fault_injection capFault_injection)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> r) P P' f g \<Longrightarrow> corres (fr \<oplus> r) P P' (cap_fault_on_failure addr b f) (capFaultOnFailure addr b g)
theory Bits_R

lemma corres_lookup_error:
  "\<lbrakk> corres (lfr \<oplus> r) P P' f g \<rbrakk>
     \<Longrightarrow> corres (ser \<oplus> r) P P' (lookup_error_on_failure b f) (lookupErrorOnFailure b g)" by (fastforce intro: corres_injection[where f'=lfr]
         simp: lookup_error_injection lookupError_injection)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (lfr \<oplus> r) P P' f g \<Longrightarrow> corres (ser \<oplus> r) P P' (lookup_error_on_failure b f) (lookupErrorOnFailure b g)
theory Bits_R

lemma unifyFailure_injection:
  "unifyFailure = injection_handler (\<lambda>x. ())" by (rule ext,
      simp add: unifyFailure_def injection_handler_def
                rethrowFailure_def o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unifyFailure = injection_handler (\<lambda>x. ())
theory Bits_R

lemma ignoreFailure_wp[wp_split]:
  "\<lbrace>P\<rbrace> v \<lbrace>\<lambda>rv. Q ()\<rbrace>,\<lbrace>\<lambda>rv. Q ()\<rbrace> \<Longrightarrow>
    \<lbrace>P\<rbrace> ignoreFailure v \<lbrace>Q\<rbrace>" by (simp add: ignoreFailure_def const_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> v \<lbrace>\<lambda>rv. Q ()\<rbrace>, \<lbrace>\<lambda>rv. Q ()\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> ignoreFailure v \<lbrace>Q\<rbrace>
theory Bits_R

lemma ep'_cases_weak_wp:
  assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
  assumes "\<And>q. \<lbrace>P_B\<rbrace> b q \<lbrace>Q\<rbrace>"
  assumes "\<And>q. \<lbrace>P_C\<rbrace> c q \<lbrace>Q\<rbrace>"
  shows
  "\<lbrace>P_A and P_B and P_C\<rbrace>
    case ts of
      IdleEP \<Rightarrow> a
    | SendEP q \<Rightarrow> b q
    | RecvEP q \<Rightarrow> c q \<lbrace>Q\<rbrace>" apply (cases ts) apply (simp, rule hoare_weaken_pre, rule assms, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P_A and P_B and P_C\<rbrace> case ts of Structures_H.endpoint.RecvEP q \<Rightarrow> c q | Structures_H.endpoint.IdleEP \<Rightarrow> a | Structures_H.endpoint.SendEP q \<Rightarrow> b q \<lbrace>Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. ts = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of Structures_H.endpoint.RecvEP q \<Rightarrow> c q | Structures_H.endpoint.IdleEP \<Rightarrow> a | Structures_H.endpoint.SendEP q \<Rightarrow> b q \<lbrace>Q\<rbrace>
 2. ts = Structures_H.endpoint.IdleEP \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of Structures_H.endpoint.RecvEP q \<Rightarrow> c q | Structures_H.endpoint.IdleEP \<Rightarrow> a | Structures_H.endpoint.SendEP q \<Rightarrow> b q \<lbrace>Q\<rbrace>
 3. \<And>x3. ts = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of Structures_H.endpoint.RecvEP q \<Rightarrow> c q | Structures_H.endpoint.IdleEP \<Rightarrow> a | Structures_H.endpoint.SendEP q \<Rightarrow> b q \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Bits_R

lemma ntfn'_cases_weak_wp:
  assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
  assumes "\<And>q. \<lbrace>P_B\<rbrace> b q \<lbrace>Q\<rbrace>"
  assumes "\<And>bdg. \<lbrace>P_C\<rbrace> c bdg \<lbrace>Q\<rbrace>"
  shows
  "\<lbrace>P_A and P_B and P_C\<rbrace>
    case ts of
      IdleNtfn \<Rightarrow> a
    | WaitingNtfn q \<Rightarrow> b q
    | ActiveNtfn bdg \<Rightarrow> c bdg \<lbrace>Q\<rbrace>" apply (cases ts) apply (simp, rule hoare_weaken_pre, rule assms, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P_A and P_B and P_C\<rbrace> case ts of Structures_H.ntfn.IdleNtfn \<Rightarrow> a | Structures_H.ntfn.ActiveNtfn bdg \<Rightarrow> c bdg | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> b q \<lbrace>Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. ts = Structures_H.ntfn.IdleNtfn \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of Structures_H.ntfn.IdleNtfn \<Rightarrow> a | Structures_H.ntfn.ActiveNtfn bdg \<Rightarrow> c bdg | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> b q \<lbrace>Q\<rbrace>
 2. \<And>x2. ts = Structures_H.ntfn.ActiveNtfn x2 \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of Structures_H.ntfn.IdleNtfn \<Rightarrow> a | Structures_H.ntfn.ActiveNtfn bdg \<Rightarrow> c bdg | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> b q \<lbrace>Q\<rbrace>
 3. \<And>x3. ts = Structures_H.ntfn.WaitingNtfn x3 \<Longrightarrow> \<lbrace>P_A and P_B and P_C\<rbrace> case ts of Structures_H.ntfn.IdleNtfn \<Rightarrow> a | Structures_H.ntfn.ActiveNtfn bdg \<Rightarrow> c bdg | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> b q \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Bits_R

lemma ko_at_imp_cte_wp_at':
  fixes x :: cte
  shows "\<lbrakk> ko_at' x ptr s \<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cte = x) ptr s" apply (erule obj_atE') apply (clarsimp simp: projectKOs objBits_simps') apply (erule cte_wp_at_cteI') apply (simp add: cte_level_bits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' x ptr s \<Longrightarrow> cte_wp_at' (\<lambda>cte. cte = x) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; obj = x; ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cte = x) ptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr = Some (KOCTE x); is_aligned ptr 4; ps_clear ptr 4 s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cte = x) ptr s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr 4; ps_clear ptr 4 s\<rbrakk> \<Longrightarrow> is_aligned ptr cte_level_bits
 2. \<lbrakk>is_aligned ptr 4; ps_clear ptr 4 s\<rbrakk> \<Longrightarrow> ps_clear ptr cte_level_bits s
 3. \<lbrakk>is_aligned ptr 4; ps_clear ptr 4 s\<rbrakk> \<Longrightarrow> x = x proof (prove)
goal:
No subgoals!
theory Bits_R

lemma modify_map_casesE:
  "\<lbrakk> modify_map m p f p' = Some cte;
     \<lbrakk> p \<noteq> p'; m p' = Some cte \<rbrakk> \<Longrightarrow> P;
     \<And>cap node. \<lbrakk> p = p'; m p = Some (CTE cap node); cte = f (CTE cap node) \<rbrakk> \<Longrightarrow> P
  \<rbrakk> \<Longrightarrow> P" by (auto dest: modify_map_casesD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>modify_map m p f p' = Some cte; \<lbrakk>p \<noteq> p'; m p' = Some cte\<rbrakk> \<Longrightarrow> P; \<And>cap node. \<lbrakk>p = p'; m p = Some (CTE cap node); cte = f (CTE cap node)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Bits_R

lemma modify_map_cases:
  "(modify_map m p f p' = Some cte) =
  ((p \<noteq> p' \<longrightarrow> m p' = Some cte) \<and>
   (p = p' \<longrightarrow> (\<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte)))" apply (rule iffI) apply (erule modify_map_casesD) apply (clarsimp simp: modify_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (modify_map m p f p' = Some cte) = ((p \<noteq> p' \<longrightarrow> m p' = Some cte) \<and> (p = p' \<longrightarrow> (\<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte))) proof (prove)
goal (2 subgoals):
 1. modify_map m p f p' = Some cte \<Longrightarrow> (p \<noteq> p' \<longrightarrow> m p' = Some cte) \<and> (p = p' \<longrightarrow> (\<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte))
 2. (p \<noteq> p' \<longrightarrow> m p' = Some cte) \<and> (p = p' \<longrightarrow> (\<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte)) \<Longrightarrow> modify_map m p f p' = Some cte proof (prove)
goal (1 subgoal):
 1. (p \<noteq> p' \<longrightarrow> m p' = Some cte) \<and> (p = p' \<longrightarrow> (\<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte)) \<Longrightarrow> modify_map m p f p' = Some cte proof (prove)
goal:
No subgoals!
theory Bits_R

lemma no_0_modify_map [simp]:
  "no_0 (modify_map m p f) = no_0 m" by (simp add: no_0_def modify_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 (modify_map m p f) = no_0 m
theory Bits_R

lemma modify_map_0 [simp]:
  "no_0 m \<Longrightarrow> modify_map m 0 f = m" by (rule ext) (auto simp add: modify_map_def no_0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 m \<Longrightarrow> modify_map m (0::'a) f = m
theory Bits_R

lemma modify_map_exists:
  "\<exists>cap node. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. modify_map m q f p = Some (CTE cap' node')" apply clarsimp apply (case_tac "f (CTE cap node)") apply (cases "q=p") apply (auto simp add: modify_map_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>cap node. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. modify_map m q f p = Some (CTE cap' node') proof (prove)
goal (1 subgoal):
 1. \<And>cap node. m p = Some (CTE cap node) \<Longrightarrow> \<exists>cap' node'. modify_map m q f p = Some (CTE cap' node') proof (prove)
goal (1 subgoal):
 1. \<And>cap node x1 x2. \<lbrakk>m p = Some (CTE cap node); f (CTE cap node) = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>cap' node'. modify_map m q f p = Some (CTE cap' node') proof (prove)
goal (2 subgoals):
 1. \<And>cap node x1 x2. \<lbrakk>m p = Some (CTE cap node); f (CTE cap node) = CTE x1 x2; q = p\<rbrakk> \<Longrightarrow> \<exists>cap' node'. modify_map m q f p = Some (CTE cap' node')
 2. \<And>cap node x1 x2. \<lbrakk>m p = Some (CTE cap node); f (CTE cap node) = CTE x1 x2; q \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>cap' node'. modify_map m q f p = Some (CTE cap' node') proof (prove)
goal:
No subgoals!
theory Bits_R

lemma modify_map_if:
  "(modify_map m p f p' = Some cte) =
   (if p = p'
    then \<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte
    else \<exists>cap node. m p' = Some (CTE cap node) \<and> cte = CTE cap node)" apply (cases cte) apply (rule iffI) apply (drule modify_map_casesD) apply auto[1] apply (auto simp: modify_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (modify_map m p f p' = Some cte) = (if p = p' then \<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte else \<exists>cap node. m p' = Some (CTE cap node) \<and> cte = CTE cap node) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. cte = CTE x1 x2 \<Longrightarrow> (modify_map m p f p' = Some cte) = (if p = p' then \<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte else \<exists>cap node. m p' = Some (CTE cap node) \<and> cte = CTE cap node) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>cte = CTE x1 x2; modify_map m p f p' = Some cte\<rbrakk> \<Longrightarrow> if p = p' then \<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte else \<exists>cap node. m p' = Some (CTE cap node) \<and> cte = CTE cap node
 2. \<And>x1 x2. \<lbrakk>cte = CTE x1 x2; if p = p' then \<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte else \<exists>cap node. m p' = Some (CTE cap node) \<and> cte = CTE cap node\<rbrakk> \<Longrightarrow> modify_map m p f p' = Some cte proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>cte = CTE x1 x2; (p \<noteq> p' \<longrightarrow> m p' = Some cte) \<and> (p = p' \<longrightarrow> (\<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte))\<rbrakk> \<Longrightarrow> if p = p' then \<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte else \<exists>cap node. m p' = Some (CTE cap node) \<and> cte = CTE cap node
 2. \<And>x1 x2. \<lbrakk>cte = CTE x1 x2; if p = p' then \<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte else \<exists>cap node. m p' = Some (CTE cap node) \<and> cte = CTE cap node\<rbrakk> \<Longrightarrow> modify_map m p f p' = Some cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>cte = CTE x1 x2; if p = p' then \<exists>cap node. m p = Some (CTE cap node) \<and> f (CTE cap node) = cte else \<exists>cap node. m p' = Some (CTE cap node) \<and> cte = CTE cap node\<rbrakk> \<Longrightarrow> modify_map m p f p' = Some cte proof (prove)
goal:
No subgoals!
theory Bits_R

lemma emptyOnFailure_wp[wp]:
  "\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv. Q []\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> emptyOnFailure m \<lbrace>Q\<rbrace>" by (simp add: emptyOnFailure_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q []\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> emptyOnFailure m \<lbrace>Q\<rbrace>
theory Bits_R

lemma withoutPreemption_lift:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> withoutPreemption f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> withoutPreemption f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Bits_R

lemma ko_at_cte_ipcbuffer:
  "ko_at' tcb p s \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbIPCBufferFrame tcb) (p + tcbIPCBufferSlot * 0x10) s" apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (erule (2) cte_wp_at_tcbI') apply (fastforce simp add: tcb_cte_cases_def tcbIPCBufferSlot_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' tcb p s \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbIPCBufferFrame tcb) (p + tcbIPCBufferSlot * 0x10) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>x. x = tcbIPCBufferFrame tcb) (p + tcbIPCBufferSlot * 0x10) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcb_cte_cases (p + tcbIPCBufferSlot * 0x10 - p) = Some (?getF2, ?setF2)
 2. \<lbrakk>is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> ?getF2 tcb = tcbIPCBufferFrame tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p tcbBlockSizeBits; ps_clear p tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> tcbIPCBufferFrame tcb = tcbIPCBufferFrame tcb proof (prove)
goal:
No subgoals!
theory Bits_R

lemma constOnFailure_wp :
  "\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q n\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> constOnFailure n m \<lbrace>Q\<rbrace>" apply (simp add: constOnFailure_def const_def) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q n\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> constOnFailure n m \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q n\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> m <catch> (\<lambda>y. return n) \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Machine_R

lemma irq_state_independent_HI[intro!, simp]:
  "\<lbrakk>\<And>s f. P (s\<lparr>ksMachineState := ksMachineState s
              \<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = P s\<rbrakk>
   \<Longrightarrow> irq_state_independent_H P" by (simp add: irq_state_independent_H_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s f. P (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = P s) \<Longrightarrow> irq_state_independent_H P
theory Machine_R

lemma dmo_getirq_inv[wp]:
  "irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: getActiveIRQ_def doMachineOp_def split_def exec_gets
                   select_f_select[simplified liftM_def]
                   select_modify_comm gets_machine_state_modify) apply wp apply (clarsimp simp: irq_state_independent_H_def in_monad return_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> doMachineOp (getActiveIRQ in_kernel) \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. irq_state_independent_H P \<Longrightarrow> \<lbrace>P\<rbrace> do ms <- gets ksMachineState;
p <- select_f ((do y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if irq_masks ms active_irq \<or> active_irq = 0x3FF \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od) ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>irq_state_independent_H P; P s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((do y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if irq_masks (ksMachineState s) active_irq \<or> active_irq = 0x3FF \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od) (ksMachineState s)). P (s\<lparr>ksMachineState := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory Machine_R

lemma getActiveIRQ_masked:
  "\<lbrace>\<lambda>s. valid_irq_masks' table (irq_masks s)\<rbrace> getActiveIRQ in_kernel
  \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> table irq \<noteq> IRQInactive\<rbrace>" apply (simp add: getActiveIRQ_def) apply wp apply (clarsimp simp: valid_irq_masks'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_masks' table (irq_masks s)\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> table irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_masks' table (irq_masks s)\<rbrace> do is_masked <- gets irq_masks;
y <- modify (\<lambda>s. s\<lparr>irq_state := Suc (irq_state s)\<rparr>);
active_irq <- gets (irq_oracle \<circ> irq_state);
if is_masked active_irq \<or> active_irq = 0x3FF \<or> in_kernel \<and> active_irq \<in> non_kernel_IRQs then return None else return (Some active_irq)
od \<lbrace>\<lambda>rv s. \<forall>irq. rv = Some irq \<longrightarrow> table irq \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_masks' table (irq_masks s) \<Longrightarrow> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs \<longrightarrow> (\<forall>irq. None = Some irq \<longrightarrow> table irq \<noteq> irqstate.IRQInactive)) \<and> (\<not> (irq_masks s ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) \<or> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) = 0x3FF \<or> in_kernel \<and> (irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>) \<in> non_kernel_IRQs) \<longrightarrow> (\<forall>irq. Some ((irq_oracle \<circ> irq_state) (s\<lparr>irq_state := Suc (irq_state s)\<rparr>)) = Some irq \<longrightarrow> table irq \<noteq> irqstate.IRQInactive)) proof (prove)
goal:
No subgoals!
theory Machine_R

lemma dmo_maskInterrupt:
  "\<lbrace>\<lambda>s. P (ksMachineState_update (irq_masks_update (\<lambda>t. t (irq := m))) s)\<rbrace>
  doMachineOp (maskInterrupt m irq) \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply (clarsimp simp: maskInterrupt_def in_monad) apply (erule rsubst [where P=P]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := m))) s)\<rbrace> doMachineOp (maskInterrupt m irq) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := m))) s)\<rbrace> do ms <- gets ksMachineState;
p <- select_f (maskInterrupt m irq ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := m))) s) \<Longrightarrow> \<forall>x\<in>fst (maskInterrupt m irq (ksMachineState s)). P (s\<lparr>ksMachineState := snd x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := m))) s) \<Longrightarrow> P (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_masks := (irq_masks (ksMachineState s))(irq := m)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. ksMachineState_update (irq_masks_update (\<lambda>t. t(irq := m))) s = s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_masks := (irq_masks (ksMachineState s))(irq := m)\<rparr>\<rparr> proof (prove)
goal:
No subgoals!