kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_AI

lemma handle_fault_st_tcb_at_runnable:
  "\<lbrace>st_tcb_at runnable t and invs and K (t' \<noteq> t) \<rbrace> handle_fault t' x \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: handle_fault_def handle_double_fault_def) apply wp apply (simp add: handle_fault_def handle_double_fault_def) apply (wp sts_st_tcb_at_other send_fault_ipc_st_tcb_at_runnable | simp)+ apply (clarsimp dest!: get_tcb_SomeD simp: obj_at_def is_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable t and invs and K (t' \<noteq> t)\<rbrace> handle_fault t' x \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. t' \<noteq> t \<Longrightarrow> \<lbrace>st_tcb_at runnable t and invs\<rbrace> handle_fault t' x \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. t' \<noteq> t \<Longrightarrow> \<lbrace>st_tcb_at runnable t and invs\<rbrace> do _ <- gets_the (get_tcb t');
send_fault_ipc t' x <catch> handle_double_fault t' x
od \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>uu_ xa. t' \<noteq> t \<Longrightarrow> \<lbrace>?E4 uu_ xa\<rbrace> handle_double_fault t' x xa \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 2. \<And>uu_. t' \<noteq> t \<Longrightarrow> \<lbrace>?B3 uu_\<rbrace> send_fault_ipc t' x \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>?E4 uu_\<rbrace>
 3. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets_the (get_tcb t') \<lbrace>?B3\<rbrace>
 4. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and invs) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>uu_ x. t' \<noteq> t \<Longrightarrow> \<lbrace>?E4 uu_ x\<rbrace> set_thread_state t' Inactive \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>
 2. \<And>uu_. t' \<noteq> t \<Longrightarrow> \<lbrace>?B3 uu_\<rbrace> send_fault_ipc t' x \<lbrace>\<lambda>rv. st_tcb_at runnable t\<rbrace>, \<lbrace>?E4 uu_\<rbrace>
 3. t' \<noteq> t \<Longrightarrow> \<lbrace>?Q2\<rbrace> gets_the (get_tcb t') \<lbrace>?B3\<rbrace>
 4. \<And>s. \<lbrakk>t' \<noteq> t; (st_tcb_at runnable t and invs) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t' \<noteq> t; st_tcb_at runnable t s \<and> invs s\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t' s = Some y) \<longrightarrow> sym_refs (state_refs_of s) \<and> tcb_at t' s proof (prove)
goal:
No subgoals!
theory ArchSyscall_AI

lemma obj_refs_cap_rights_update[simp, Syscall_AI_assms]:
  "obj_refs (cap_rights_update rs cap) = obj_refs cap" by (auto simp: cap_rights_update_def acap_rights_update_def
          split: cap.split arch_cap.split bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_refs (cap_rights_update rs cap) = obj_refs cap
theory ArchSyscall_AI

lemma table_cap_ref_mask_cap [Syscall_AI_assms]:
  "table_cap_ref (mask_cap R cap) = table_cap_ref cap" by (clarsimp simp add:mask_cap_def table_cap_ref_def acap_rights_update_def
    cap_rights_update_def split:cap.splits arch_cap.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. table_cap_ref (mask_cap R cap) = table_cap_ref cap
theory ArchSyscall_AI

lemma eq_no_cap_to_obj_with_diff_ref [Syscall_AI_assms]:
  "\<lbrakk> cte_wp_at ((=) cap) p s; valid_arch_caps s \<rbrakk>
      \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s" apply (clarsimp simp: cte_wp_at_caps_of_state valid_arch_caps_def) apply (frule(1) unique_table_refs_no_cap_asidD) apply (clarsimp simp add: no_cap_to_obj_with_diff_ref_def table_cap_ref_mask_cap Ball_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap) p s; valid_arch_caps s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); no_cap_to_obj_dr_emp cap s\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s proof (prove)
goal:
No subgoals!
theory ArchSyscall_AI

lemma getDFSR_invs[wp]:
  "valid invs (do_machine_op getDFSR) (\<lambda>_. invs)" by (simp add: getDFSR_def do_machine_op_def split_def select_f_returns | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op getDFSR \<lbrace>\<lambda>_. invs\<rbrace>
theory ArchSyscall_AI

lemma getFAR_invs[wp]:
  "valid invs (do_machine_op getFAR) (\<lambda>_. invs)" by (simp add: getFAR_def do_machine_op_def split_def select_f_returns | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op getFAR \<lbrace>\<lambda>_. invs\<rbrace>
theory ArchSyscall_AI

lemma getIFSR_invs[wp]:
  "valid invs (do_machine_op getIFSR) (\<lambda>_. invs)" by (simp add: getIFSR_def do_machine_op_def split_def select_f_returns | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op getIFSR \<lbrace>\<lambda>_. invs\<rbrace>
theory ArchSyscall_AI

lemma hv_invs[wp, Syscall_AI_assms]: "\<lbrace>invs\<rbrace> handle_vm_fault t' flt \<lbrace>\<lambda>r. invs\<rbrace>" apply (cases flt, simp_all) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> handle_vm_fault t' flt \<lbrace>\<lambda>r. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. flt = ARMDataAbort \<Longrightarrow> \<lbrace>invs\<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>r. invs\<rbrace>
 2. flt = ARMPrefetchAbort \<Longrightarrow> \<lbrace>invs\<rbrace> doE pc <- liftE (as_user t' getRestartPC);
fault <- liftE (do_machine_op getIFSR);
throwError (ArchFault (VMFault pc [1, fault && mask 14]))
odE \<lbrace>\<lambda>r. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSyscall_AI

lemma handle_vm_fault_valid_fault[wp, Syscall_AI_assms]:
  "\<lbrace>\<top>\<rbrace> handle_vm_fault thread ft -,\<lbrace>\<lambda>rv s. valid_fault rv\<rbrace>" apply (cases ft, simp_all) apply (wp no_irq_getDFSR no_irq_getIFSR| simp add: valid_fault_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> handle_vm_fault thread ft -, \<lbrace>\<lambda>rv s. valid_fault rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. ft = ARMDataAbort \<Longrightarrow> \<lbrace>\<lambda>_. True\<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>rv s. valid_fault rv\<rbrace>
 2. ft = ARMPrefetchAbort \<Longrightarrow> \<lbrace>\<lambda>_. True\<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>rv s. valid_fault rv\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSyscall_AI

lemma hvmf_active [Syscall_AI_assms]:
  "\<lbrace>st_tcb_at active t\<rbrace> handle_vm_fault t w \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace>" apply (cases w, simp_all) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at active t\<rbrace> handle_vm_fault t w \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace> proof (prove)
goal (2 subgoals):
 1. w = ARMDataAbort \<Longrightarrow> \<lbrace>st_tcb_at active t\<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>rv. st_tcb_at active t\<rbrace>
 2. w = ARMPrefetchAbort \<Longrightarrow> \<lbrace>st_tcb_at active t\<rbrace> doE pc <- liftE (as_user t getRestartPC);
fault <- liftE (do_machine_op getIFSR);
throwError (ArchFault (VMFault pc [1, fault && mask 14]))
odE \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSyscall_AI

lemma hvmf_ex_cap[wp, Syscall_AI_assms]:
  "\<lbrace>ex_nonz_cap_to p\<rbrace> handle_vm_fault t b \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" apply (cases b, simp_all) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to p\<rbrace> handle_vm_fault t b \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (2 subgoals):
 1. b = ARMDataAbort \<Longrightarrow> \<lbrace>ex_nonz_cap_to 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>rv. ex_nonz_cap_to p\<rbrace>
 2. b = ARMPrefetchAbort \<Longrightarrow> \<lbrace>ex_nonz_cap_to p\<rbrace> doE pc <- liftE (as_user t getRestartPC);
fault <- liftE (do_machine_op getIFSR);
throwError (ArchFault (VMFault pc [1, fault && mask 14]))
odE \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSyscall_AI

lemma hh_invs[wp, Syscall_AI_assms]:
  "\<lbrace>invs and ct_active and st_tcb_at active thread and ex_nonz_cap_to thread\<rbrace>
     handle_hypervisor_fault thread fault
   \<lbrace>\<lambda>rv. invs\<rbrace>" by (cases fault; wpsimp simp: valid_fault_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and st_tcb_at active thread and ex_nonz_cap_to thread\<rbrace> handle_hypervisor_fault thread fault \<lbrace>\<lambda>rv. invs\<rbrace>
theory VSpaceEntries_AI

lemma vaid_entries_overwrite_0_weak:
  assumes ve: "valid_entries rg tab"
  assumes disjoint: "rg v x \<subseteq> rg (tab x) x"
  shows "valid_entries rg (tab (x := v))" using assms apply (subst valid_entries_def) apply clarsimp apply (intro allI impI conjI) apply (fastforce simp:valid_entries_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_entries rg (tab(x := v)) proof (prove)
using this:
valid_entries rg tab
rg v x \<subseteq> rg (tab x) x

goal (1 subgoal):
 1. valid_entries rg (tab(x := v)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_entries rg tab; rg v x \<subseteq> rg (tab x) x\<rbrakk> \<Longrightarrow> \<forall>xa y. xa \<noteq> y \<longrightarrow> rg ((tab(x := v)) xa) xa \<inter> rg ((tab(x := v)) y) y = {} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>valid_entries rg tab; rg v x \<subseteq> rg (tab x) x\<rbrakk> \<Longrightarrow> (xa = x \<longrightarrow> (\<forall>y. x \<noteq> y \<longrightarrow> rg v x \<inter> rg (tab y) y = {})) \<and> (xa \<noteq> x \<longrightarrow> (\<forall>y. (y = x \<longrightarrow> rg (tab xa) xa \<inter> rg v x = {}) \<and> (y \<noteq> x \<longrightarrow> xa \<noteq> y \<longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {}))) proof (prove)
goal (3 subgoals):
 1. \<And>xa y. \<lbrakk>valid_entries rg tab; rg v x \<subseteq> rg (tab x) x; xa = x; x \<noteq> y\<rbrakk> \<Longrightarrow> rg v x \<inter> rg (tab y) y = {}
 2. \<And>xa y. \<lbrakk>valid_entries rg tab; rg v x \<subseteq> rg (tab x) x; xa \<noteq> x; y = x\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg v x = {}
 3. \<And>xa y. \<lbrakk>valid_entries rg tab; rg v x \<subseteq> rg (tab x) x; xa \<noteq> x; y \<noteq> x; xa \<noteq> y\<rbrakk> \<Longrightarrow> rg (tab xa) xa \<inter> rg (tab y) y = {} proof (prove)
goal:
No subgoals!
theory VSpaceEntries_AI

lemma valid_entries_overwrite_groups:
  "\<lbrakk>valid_entries rg tab; valid_entries rg (\<lambda>_. v);
    \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S;
    \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}\<rbrakk>
       \<Longrightarrow> valid_entries rg (\<lambda>x. if P x then v else tab x)" by (rule valid_entries_partial_copy)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_entries rg tab; valid_entries rg (\<lambda>_. v); \<forall>v x. P x \<longrightarrow> rg v x \<subseteq> S; \<forall>v x. \<not> P x \<longrightarrow> rg v x \<inter> S = {}\<rbrakk> \<Longrightarrow> valid_entries rg (\<lambda>x. if P x then v else tab x)
theory VSpaceEntries_AI

lemma valid_entriesD:
  "\<lbrakk>x \<noteq> y; valid_entries rg fun\<rbrakk> \<Longrightarrow> rg (fun x) x \<inter> rg (fun y) y = {}" by (simp add:valid_entries_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; valid_entries rg fun\<rbrakk> \<Longrightarrow> rg (fun x) x \<inter> rg (fun y) y = {}
theory VSpaceEntries_AI

lemma ucast_neg_mask:
  "len_of TYPE('a) \<le> len_of TYPE ('b)
   \<Longrightarrow> ((ucast ptr && ~~ mask n)::('a :: len) word) = ucast ((ptr::('b :: len) word) && ~~ mask n)" apply (rule word_eqI) apply (auto simp:nth_ucast neg_mask_test_bit word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> UCAST('b \<rightarrow> 'a) ptr && ~~ mask n = UCAST('b \<rightarrow> 'a) (ptr && ~~ mask n) proof (prove)
goal (1 subgoal):
 1. \<And>na. LENGTH('a) \<le> LENGTH('b) \<Longrightarrow> na < size (UCAST('b \<rightarrow> 'a) ptr && ~~ mask n) \<longrightarrow> (UCAST('b \<rightarrow> 'a) ptr && ~~ mask n) !! na = UCAST('b \<rightarrow> 'a) (ptr && ~~ mask n) !! na proof (prove)
goal:
No subgoals!
theory VSpaceEntries_AI

lemma upto_0_to_n:
  "0 < n \<Longrightarrow> tl [0..<n] = [1..<n]" apply (erule(1) impE[rotated]) apply (induct_tac n) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> tl [0..<n] = [1..<n] proof (prove)
goal (1 subgoal):
 1. 0 < n \<longrightarrow> tl [0..<n] = [1..<n] proof (prove)
goal (2 subgoals):
 1. 0 < 0 \<longrightarrow> tl [0..<0] = [1..<0]
 2. \<And>n. 0 < n \<longrightarrow> tl [0..<n] = [1..<n] \<Longrightarrow> 0 < Suc n \<longrightarrow> tl [0..<Suc n] = [1..<Suc n] proof (prove)
goal (1 subgoal):
 1. \<And>n. 0 < n \<longrightarrow> tl [0..<n] = [1..<n] \<Longrightarrow> 0 < Suc n \<longrightarrow> tl [0..<Suc n] = [1..<Suc n] proof (prove)
goal:
No subgoals!
theory VSpaceEntries_AI

lemma upto_0_to_n2:
  "0 < n \<Longrightarrow> [0..<n] = 0 # [1..<n]" apply (erule(1) impE[rotated]) apply (induct_tac n) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> [0..<n] = 0 # [1..<n] proof (prove)
goal (1 subgoal):
 1. 0 < n \<longrightarrow> [0..<n] = 0 # [1..<n] proof (prove)
goal (2 subgoals):
 1. 0 < 0 \<longrightarrow> [0..<0] = 0 # [1..<0]
 2. \<And>n. 0 < n \<longrightarrow> [0..<n] = 0 # [1..<n] \<Longrightarrow> 0 < Suc n \<longrightarrow> [0..<Suc n] = 0 # [1..<Suc n] proof (prove)
goal (1 subgoal):
 1. \<And>n. 0 < n \<longrightarrow> [0..<n] = 0 # [1..<n] \<Longrightarrow> 0 < Suc n \<longrightarrow> [0..<Suc n] = 0 # [1..<Suc n] proof (prove)
goal:
No subgoals!
theory VSpaceEntries_AI

lemma neg_mask_add_mask:
  "((a && ~~ mask b) + c && mask b) = c && mask b" by (subst mask_add_aligned[OF is_aligned_neg_mask],simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a && ~~ mask b) + c && mask b = c && mask b
theory VSpaceEntries_AI

lemma all_imp_ko_at_from_ex_strg:
  "((\<exists>v. ko_at (f v) p s \<and> P v) \<and> inj f) \<longrightarrow> (\<forall>v. ko_at (f v) p s \<longrightarrow> P v)" apply (clarsimp simp add: obj_at_def) apply (auto dest: inj_onD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>v. ko_at (f v) p s \<and> P v) \<and> inj f \<longrightarrow> (\<forall>v. ko_at (f v) p s \<longrightarrow> P v) proof (prove)
goal (1 subgoal):
 1. \<And>v va. \<lbrakk>inj f; f v = f va; P va; kheap s p = Some (f va)\<rbrakk> \<Longrightarrow> P v proof (prove)
goal:
No subgoals!
theory VSpaceEntries_AI

lemma mapME_x_Nil:
  "mapME_x f [] = returnOk ()" unfolding mapME_x_def sequenceE_x_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x f [] = returnOk () proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. doE _ <- x;
y
odE) (map f []) (returnOk ()) = returnOk ()
theory VSpaceEntries_AI

lemma mapME_x_mapME:
  "mapME_x m l = (mapME m l >>=E (%_. returnOk ()))" apply (simp add: mapME_x_def sequenceE_x_def mapME_def sequenceE_def) apply (induct l, simp_all add: Let_def bindE_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x m l = doE _ <- mapME m l;
returnOk ()
odE proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. doE _ <- x;
y
odE) (map m l) (returnOk ()) = doE _ <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map m l) (returnOk []);
returnOk ()
odE proof (prove)
goal:
No subgoals!
theory VSpaceEntries_AI

lemma mapME_x_wp:
  assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>"
  shows      "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace>" apply (subst mapME_x_mapME) apply wp apply (rule mapME_wp) apply (rule x) apply assumption+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> doE _ <- mapME f xs;
returnOk ()
odE \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>?Q\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s. \<lbrakk>set xs \<subseteq> S; P s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>set xs \<subseteq> S; x \<in> ?S3\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>
 2. set xs \<subseteq> S \<Longrightarrow> set xs \<subseteq> ?S3
 3. \<And>s. \<lbrakk>set xs \<subseteq> S; P s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>set xs \<subseteq> S; x \<in> ?S3\<rbrakk> \<Longrightarrow> x \<in> S
 2. set xs \<subseteq> S \<Longrightarrow> set xs \<subseteq> ?S3
 3. \<And>s. \<lbrakk>set xs \<subseteq> S; P s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory VSpaceEntries_AI

lemma hoare_vcg_ex_liftE:
  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>" by (fastforce simp: validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>, \<lbrace>E\<rbrace>
theory VSpaceEntries_AI

lemma mapME_singleton:
  "mapME_x f [x] = f x" by (simp add:mapME_x_def sequenceE_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x f [x] = f x
theory ArchVSpaceEntries_AI

lemma a_type_pdD:
  "a_type ko = AArch APageDirectory \<Longrightarrow> \<exists>pd. ko = ArchObj (PageDirectory pd)" by (clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a_type ko = AArch APageDirectory \<Longrightarrow> \<exists>pd. ko = ArchObj (PageDirectory pd)
theory ArchVSpaceEntries_AI

lemma valid_pdpt_init[iff]:
  "valid_pdpt_objs init_A_st" proof - have P: "valid_pd_entries (global_pd :: 12 word \<Rightarrow> _)" by (clarsimp simp: valid_entries_def) also have Q: "entries_align pde_range_sz (global_pd :: 12 word \<Rightarrow> _)" by (clarsimp simp: entries_align_def) thus ?thesis using P by (auto simp: init_A_st_def init_kheap_def
            elim!: ranE split: if_split_asm) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>ran (kheap init_A_st). obj_valid_pdpt x proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>ran (kheap init_A_st). obj_valid_pdpt x proof (prove)
goal (1 subgoal):
 1. valid_entries pde_range global_pd proof (state)
this:
valid_entries pde_range global_pd

goal (1 subgoal):
 1. \<forall>x\<in>ran (kheap init_A_st). obj_valid_pdpt x proof (state)
this:
valid_entries pde_range global_pd

goal (1 subgoal):
 1. \<forall>x\<in>ran (kheap init_A_st). obj_valid_pdpt x proof (prove)
goal (1 subgoal):
 1. entries_align pde_range_sz global_pd proof (state)
this:
entries_align pde_range_sz global_pd

goal (1 subgoal):
 1. \<forall>x\<in>ran (kheap init_A_st). obj_valid_pdpt x proof (prove)
using this:
entries_align pde_range_sz global_pd

goal (1 subgoal):
 1. \<forall>x\<in>ran (kheap init_A_st). obj_valid_pdpt x proof (prove)
using this:
entries_align pde_range_sz global_pd
valid_entries pde_range global_pd

goal (1 subgoal):
 1. \<forall>x\<in>ran (kheap init_A_st). obj_valid_pdpt x proof (state)
this:
\<forall>x\<in>ran (kheap init_A_st). obj_valid_pdpt x

goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma set_object_valid_pdpt[wp]:
  "\<lbrace>valid_pdpt_objs and K (obj_valid_pdpt obj)\<rbrace>
      set_object ptr obj
   \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" apply (simp add: set_object_def get_object_def, wp) apply (auto simp: fun_upd_def[symmetric] del: ballI elim: ball_ran_updI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and K (obj_valid_pdpt obj)\<rbrace> set_object ptr obj \<lbrace>\<lambda>rv s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and (\<lambda>y. obj_valid_pdpt obj)) s \<Longrightarrow> (\<exists>y. kheap s ptr = Some y) \<longrightarrow> a_type (the (kheap s ptr)) = a_type obj \<longrightarrow> (\<forall>x\<in>ran (kheap (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>)). obj_valid_pdpt x) proof (prove)
goal:
No subgoals!
theory ArchVSpaceEntries_AI

lemma valid_pd_entries_invalid[simp]:
  "valid_pd_entries (\<lambda>x. InvalidPDE)" by (simp add:valid_entries_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_entries pde_range (\<lambda>x. InvalidPDE)
theory ArchVSpaceEntries_AI

lemma entries_align_pte_update:
 "\<lbrakk>entries_align pte_range_sz pt;
  (\<forall>y. (P y) \<longrightarrow> is_aligned y (pte_range_sz pte))\<rbrakk>
  \<Longrightarrow> entries_align pte_range_sz (\<lambda>y. if (P y) then pte else pt y)" by (simp add:entries_align_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>entries_align pte_range_sz pt; \<forall>y. P y \<longrightarrow> is_aligned y (pte_range_sz pte)\<rbrakk> \<Longrightarrow> entries_align pte_range_sz (\<lambda>y. if P y then pte else pt y)
theory ArchVSpaceEntries_AI

lemma valid_pdpt_objs_pdD:
  "\<lbrakk>valid_pdpt_objs s;
    kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory pd))\<rbrakk>
   \<Longrightarrow> valid_pd_entries pd \<and> entries_align pde_range_sz pd" by (fastforce simp:ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s ptr = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> valid_entries pde_range pd \<and> entries_align pde_range_sz pd
theory ArchVSpaceEntries_AI

lemma valid_pdpt_objs_ptD:
  "\<lbrakk>valid_pdpt_objs s;
    kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable pt))\<rbrakk>
   \<Longrightarrow> valid_pt_entries pt \<and> entries_align pte_range_sz pt" by (fastforce simp:ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; kheap s ptr = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> valid_entries pte_range pt \<and> entries_align pte_range_sz pt