kings-crown/FVELER_Isabelle huggingface dataset:
theory Invocation_DP

lemma reset_cap_twice[simp]:
  "reset_cap_asid \<circ>\<^sub>M (reset_cap_asid \<circ>\<^sub>M x)
  =  reset_cap_asid \<circ>\<^sub>M x" apply (rule ext) apply (clarsimp simp:reset_cap_asid_def) apply (simp split:cdl_cap.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid o_M (reset_cap_asid o_M x) = reset_cap_asid o_M x proof (prove)
goal (1 subgoal):
 1. \<And>xa. (reset_cap_asid o_M (reset_cap_asid o_M x)) xa = (reset_cap_asid o_M x) xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. (case case x xa of None \<Rightarrow> None | Some x \<Rightarrow> Some (case x of FrameCap dev f1 f2 f3 f4 ad \<Rightarrow> FrameCap dev f1 f2 f3 f4 None | PageTableCap f1 f2 ad \<Rightarrow> PageTableCap f1 f2 None | PageDirectoryCap f1 f2 ad \<Rightarrow> PageDirectoryCap f1 f2 None | _ \<Rightarrow> x) of None \<Rightarrow> None | Some x \<Rightarrow> Some (case x of FrameCap dev f1 f2 f3 f4 ad \<Rightarrow> FrameCap dev f1 f2 f3 f4 None | PageTableCap f1 f2 ad \<Rightarrow> PageTableCap f1 f2 None | PageDirectoryCap f1 f2 ad \<Rightarrow> PageDirectoryCap f1 f2 None | _ \<Rightarrow> x)) = (case x xa of None \<Rightarrow> None | Some x \<Rightarrow> Some (case x of FrameCap dev f1 f2 f3 f4 ad \<Rightarrow> FrameCap dev f1 f2 f3 f4 None | PageTableCap f1 f2 ad \<Rightarrow> PageTableCap f1 f2 None | PageDirectoryCap f1 f2 ad \<Rightarrow> PageDirectoryCap f1 f2 None | _ \<Rightarrow> x)) proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma asid_reset_twice[simp]:
  "(asid_reset (asid_reset x)) = asid_reset x" by (case_tac x,
    simp_all add:asid_reset_def
    update_slots_def object_slots_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_reset (asid_reset x) = asid_reset x
theory Invocation_DP

lemma object_clean_twice[simp]:
  "object_clean (object_clean x) = object_clean x" by (clarsimp simp:object_clean_def asid_reset_intent_reset_switch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_clean (object_clean x) = object_clean x
theory Invocation_DP

lemma mark_tcb_intent_error_sep_inv[wp]:
  "\<lbrace>\<lambda>s. < P >  s\<rbrace>
  mark_tcb_intent_error thread b
  \<lbrace>\<lambda>rv s. < P > s\<rbrace>" apply (rule sep_nonimpact_valid_lift) apply (simp add:mark_tcb_intent_error_def update_thread_def
     set_object_def) apply (wp | wpc | simp add:set_object_def)+ apply (clarsimp simp: object_at_def object_clean_def intent_reset_def
                         object_slots_def asid_reset_def update_slots_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift P\<rbrace> mark_tcb_intent_error thread b \<lbrace>\<lambda>rv. cdl.lift P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr P A. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> mark_tcb_intent_error thread b \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>
 2. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> mark_tcb_intent_error thread b \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr P A. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> do t <- get_object thread;
case t of Tcb tcb \<Rightarrow> set_object thread (Tcb (tcb\<lparr>cdl_tcb_intent := cdl_tcb_intent tcb\<lparr>cdl_intent_error := b\<rparr>\<rparr>)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>
 2. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> mark_tcb_intent_error thread b \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr P A s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s) \<Longrightarrow> (\<exists>y. cdl_objects s thread = Some y) \<longrightarrow> (\<forall>x. the (cdl_objects s thread) = Tcb x \<longrightarrow> A (object_at (\<lambda>obj. P (object_clean obj)) ptr (s\<lparr>cdl_objects := \<lambda>a. if a = thread then Some (Tcb (x\<lparr>cdl_tcb_intent := cdl_tcb_intent x\<lparr>cdl_intent_error := b\<rparr>\<rparr>)) else cdl_objects s a\<rparr>)))
 2. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> mark_tcb_intent_error thread b \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> mark_tcb_intent_error thread b \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma corrupt_tcb_intent_sep_helper[wp]:
  "\<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> corrupt_tcb_intent thread
  \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>" apply (simp add:corrupt_tcb_intent_def update_thread_def
     set_object_def) apply (wp | wpc | simp add:set_object_def)+ apply (clarsimp simp:object_at_def) apply (simp add:object_clean_def intent_reset_def
     object_slots_def asid_reset_def update_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> corrupt_tcb_intent thread \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> do new_intent <- select UNIV;
t <- get_object thread;
case t of Tcb tcb \<Rightarrow> set_object thread (Tcb (tcb\<lparr>cdl_tcb_intent := new_intent\<rparr>)) | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s) \<Longrightarrow> (\<exists>y. cdl_objects s thread = Some y) \<longrightarrow> (\<forall>x xa. the (cdl_objects s thread) = Tcb xa \<longrightarrow> A (object_at (\<lambda>obj. P (object_clean obj)) ptr (s\<lparr>cdl_objects := \<lambda>a. if a = thread then Some (Tcb (xa\<lparr>cdl_tcb_intent := x\<rparr>)) else cdl_objects s a\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>A (P (object_clean (Tcb xa))); cdl_objects s thread = Some (Tcb xa); ptr = thread\<rbrakk> \<Longrightarrow> A (P (object_clean (Tcb (xa\<lparr>cdl_tcb_intent := x\<rparr>)))) proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma corrupt_tcb_intent_sep_inv[wp]:
  "\<lbrace>\<lambda>s. < P >  s\<rbrace>
  corrupt_tcb_intent thread
  \<lbrace>\<lambda>rv s. < P > s\<rbrace>" by (rule sep_nonimpact_valid_lift; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift P\<rbrace> corrupt_tcb_intent thread \<lbrace>\<lambda>rv. cdl.lift P\<rbrace>
theory Invocation_DP

lemma corrupt_frame_sep_helper[wp]:
  "\<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>
  corrupt_frame a \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>" apply (simp add:corrupt_frame_def) apply wp apply (clarsimp simp:corrupt_intents_def object_at_def
    map_add_def split:option.splits cdl_object.splits) apply (simp add:object_clean_def intent_reset_def
     object_slots_def asid_reset_def update_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> corrupt_frame a \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> do f <- select UNIV;
modify (corrupt_intents f a)
od \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s) \<Longrightarrow> \<forall>x\<in>UNIV. A (object_at (\<lambda>obj. P (object_clean obj)) ptr (corrupt_intents x a s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x x3. \<lbrakk>A (P (object_clean (Tcb x3))); tcb_ipcframe_id x3 = Some a; cdl_objects s ptr = Some (Tcb x3)\<rbrakk> \<Longrightarrow> A (P (object_clean (Tcb (x3\<lparr>cdl_tcb_intent := x ptr\<rparr>)))) proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma corrupt_ipc_buffer_sep_inv[wp]:
  "\<lbrace>\<lambda>s. < P > s\<rbrace>
    corrupt_ipc_buffer cur_thread p
   \<lbrace>\<lambda>rv s. < P > s\<rbrace>" apply (rule sep_nonimpact_valid_lift) apply (simp add:corrupt_ipc_buffer_def) apply (wp hoare_drop_imps | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift P\<rbrace> corrupt_ipc_buffer cur_thread p \<lbrace>\<lambda>rv. cdl.lift P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr P A. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> corrupt_ipc_buffer cur_thread p \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>
 2. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> corrupt_ipc_buffer cur_thread p \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ptr P A. \<lbrace>\<lambda>s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace> do buffer <- get_ipc_buffer cur_thread p;
case buffer of None \<Rightarrow> corrupt_tcb_intent cur_thread | Some a \<Rightarrow> corrupt_frame a
od \<lbrace>\<lambda>rv s. A (object_at (\<lambda>obj. P (object_clean obj)) ptr s)\<rbrace>
 2. \<And>ptr P A. \<lbrace>\<lambda>s. A (cdl_irq_node s)\<rbrace> corrupt_ipc_buffer cur_thread p \<lbrace>\<lambda>rv s. A (cdl_irq_node s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma liftE_wp_no_exception:
  "\<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>;\<lbrace>P\<rbrace>f\<lbrace>\<lambda>r. P' r\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftE f >>=E g \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>" apply (simp add:liftE_bindE validE_def) including no_pre apply wp apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftE f >>=E g \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?B2 x\<rbrace> g x \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r s\<rbrace>
 2. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>?B2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>P' r\<rbrace> g r \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma handle_event_no_exception:
  "\<lbrace>P\<rbrace> handle_event  (SyscallEvent SysCall) \<lbrace>\<lambda>r. Q\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) <handle> handler \<lbrace>\<lambda>r. Q\<rbrace>" apply (rule validE_cases_valid) including no_pre apply (wp) apply (rule hoare_FalseE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) <handle> handler \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) <handle> handler \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) <handle> handler \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace> \<Longrightarrow> \<lbrace>?F2 x\<rbrace> handler x \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>?F2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> handle_event (SyscallEvent SysCall) \<lbrace>\<lambda>rv. Q\<rbrace>, \<lbrace>\<lambda>x _. False\<rbrace> proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma no_exception_conj:
  "\<lbrakk>\<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>;\<lbrace>P'\<rbrace>f\<lbrace>Q'\<rbrace>,-\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>f\<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>" apply (clarsimp simp add:validE_def validE_R_def valid_def) apply (drule_tac x = s in spec)+ apply clarsimp apply (drule(1) bspec)+ apply (auto split:sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q ra s'); \<forall>s. P' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> True | (Inr ra, s') \<Rightarrow> Q' ra s'); (a, b) \<in> fst (f s); P s; P' s\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r b \<and> Q' r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; P' s; P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q ra s'); P' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> True | (Inr ra, s') \<Rightarrow> Q' ra s')\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r b \<and> Q' r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; P' s; \<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q ra s'; \<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> True | (Inr ra, s') \<Rightarrow> Q' ra s'\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r b \<and> Q' r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; P' s; case (a, b) of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q ra s'; case (a, b) of (Inl e, s') \<Rightarrow> True | (Inr ra, s') \<Rightarrow> Q' ra s'\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r b \<and> Q' r b proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma no_exception_conj':
  "\<lbrakk>\<lbrace>P'\<rbrace>f\<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace>f\<lbrace>Q'\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>f\<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>,\<lbrace>\<lambda>r s. False\<rbrace>" apply (clarsimp simp add:validE_def validE_R_def valid_def) apply (drule_tac x = s in spec)+ apply clarsimp apply (drule(1) bspec)+ apply (auto split:sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> True | (Inr ra, s') \<Rightarrow> Q ra s'); \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q' ra s'); (a, b) \<in> fst (f s); P s; P' s\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r b \<and> Q' r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; P' s; P' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> True | (Inr ra, s') \<Rightarrow> Q ra s'); P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q' ra s')\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r b \<and> Q' r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; P' s; \<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> True | (Inr ra, s') \<Rightarrow> Q ra s'; \<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q' ra s'\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r b \<and> Q' r b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; P' s; case (a, b) of (Inl e, s') \<Rightarrow> True | (Inr ra, s') \<Rightarrow> Q ra s'; case (a, b) of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> Q' ra s'\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> False | Inr r \<Rightarrow> Q r b \<and> Q' r b proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma decode_page_table_invocation_inv[wp]:
  "\<lbrace>P\<rbrace> decode_page_table_invocation a b c d \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add:decode_page_table_invocation_def) apply (rule hoare_pre) apply (wpc|wp |simp add:throw_on_none_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_page_table_invocation a b c d \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case d of PageTableMapIntent vaddr attr \<Rightarrow> doE case cdl_get_pt_mapped_addr a of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throw;
pd <- throw_on_none $ get_index c 0;
(pd_object_id, asid) <- case fst pd of PageDirectoryCap x xa None \<Rightarrow> throw | PageDirectoryCap x xa (Some asid) \<Rightarrow> returnOk (x, asid) | _ \<Rightarrow> throw;
target_slot <- returnOk $ cdl_lookup_pd_slot pd_object_id vaddr;
returnOk $ PageTableMap (PageTableCap (cap_object a) Real (Some (asid, vaddr && ~~ mask 20))) (PageTableCap (cap_object a) Fake None) b target_slot
odE \<sqinter> throw | PageTableUnmapIntent \<Rightarrow> (case a of PageTableCap pid ctype maddr \<Rightarrow> returnOk $ PageTableUnmap maddr pid b | _ \<Rightarrow> throw) \<sqinter> throw \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case d of PageTableMapIntent vaddr attr \<Rightarrow> doE case cdl_get_pt_mapped_addr a of None \<Rightarrow> returnOk () | Some a \<Rightarrow> throw;
pd <- throw_on_none $ get_index c 0;
(pd_object_id, asid) <- case fst pd of PageDirectoryCap x xa None \<Rightarrow> throw | PageDirectoryCap x xa (Some asid) \<Rightarrow> returnOk (x, asid) | _ \<Rightarrow> throw;
target_slot <- returnOk $ cdl_lookup_pd_slot pd_object_id vaddr;
returnOk $ PageTableMap (PageTableCap (cap_object a) Real (Some (asid, vaddr && ~~ mask 20))) (PageTableCap (cap_object a) Fake None) b target_slot
odE \<sqinter> throw | PageTableUnmapIntent \<Rightarrow> (case a of PageTableCap pid ctype maddr \<Rightarrow> returnOk $ PageTableUnmap maddr pid b | _ \<Rightarrow> throw) \<sqinter> throw \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Invocation_DP

lemma decode_page_directory_invocation_inv[wp]:
  "\<lbrace>P\<rbrace> decode_page_directory_invocation a b c d \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add:decode_page_directory_invocation_def) apply (rule hoare_pre) apply (wpc|wp |simp add:throw_on_none_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_page_directory_invocation a b c d \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> returnOk PageDirectoryNothing \<sqinter> returnOk (PageDirectoryFlush Unify) \<sqinter> returnOk (PageDirectoryFlush Clean) \<sqinter> returnOk (PageDirectoryFlush CleanInvalidate) \<sqinter> returnOk (PageDirectoryFlush Invalidate) \<sqinter> throw \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> returnOk PageDirectoryNothing \<sqinter> returnOk (PageDirectoryFlush Unify) \<sqinter> returnOk (PageDirectoryFlush Clean) \<sqinter> returnOk (PageDirectoryFlush CleanInvalidate) \<sqinter> returnOk (PageDirectoryFlush Invalidate) \<sqinter> throw \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!