kings-crown/FVELER_Isabelle huggingface dataset:
theory Deterministic_AI

lemma next_sib_2_pinduct':
  "\<lbrakk>next_sib_2_dom (slot, p, s);
   \<And>slot.
      \<lbrakk>next_sib_2_dom (slot, p, s);
       \<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s);
          next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> P a t m\<rbrakk>
      \<Longrightarrow> P slot t m\<rbrakk>
  \<Longrightarrow> P slot t m" apply(induct rule: next_sib_2.pinduct) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2_dom (slot, p, s); \<And>slot. \<lbrakk>next_sib_2_dom (slot, p, s); \<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> P a t m\<rbrakk> \<Longrightarrow> P slot t m\<rbrakk> \<Longrightarrow> P slot t m proof (prove)
goal (1 subgoal):
 1. \<And>slot p s. \<lbrakk>next_sib_2_dom (slot, p, s); \<And>x2. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some x2; cdt s x2 \<noteq> Some p; \<And>slot. \<lbrakk>next_sib_2_dom (slot, p, s); \<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> P a t m\<rbrakk> \<Longrightarrow> P slot t m\<rbrakk> \<Longrightarrow> P x2 t m; \<And>slot. \<lbrakk>next_sib_2_dom (slot, p, s); \<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p\<rbrakk> \<Longrightarrow> P a t m\<rbrakk> \<Longrightarrow> P slot t m\<rbrakk> \<Longrightarrow> P slot t m proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma last_childD:
  notes split_paired_All[simp del]
  shows "\<lbrakk>last_child slot t = Some child; valid_list_2 t m\<rbrakk>
    \<Longrightarrow> m child = Some slot \<and> next_sib child t m = None" apply(rule context_conjI) apply(fastforce simp: valid_list_2_def last_child_def split: if_split_asm) apply(rule next_sib_NoneI[where p=slot]) apply(case_tac "t slot") apply(simp) apply(simp add: valid_list_2_def last_child_def split: if_split_asm) apply(erule_tac x=slot in allE)+ apply(drule after_in_list_last_None) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_child slot t = Some child; valid_list_2 t m\<rbrakk> \<Longrightarrow> m child = Some slot \<and> next_sib child t m = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>last_child slot t = Some child; valid_list_2 t m\<rbrakk> \<Longrightarrow> m child = Some slot
 2. \<lbrakk>last_child slot t = Some child; valid_list_2 t m; m child = Some slot\<rbrakk> \<Longrightarrow> next_sib child t m = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_child slot t = Some child; valid_list_2 t m; m child = Some slot\<rbrakk> \<Longrightarrow> next_sib child t m = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_child slot t = Some child; valid_list_2 t m; m child = Some slot\<rbrakk> \<Longrightarrow> m child = None \<or> m child = Some slot \<and> after_in_list (t slot) child = None proof (prove)
goal (2 subgoals):
 1. \<lbrakk>last_child slot t = Some child; valid_list_2 t m; m child = Some slot; t slot = []\<rbrakk> \<Longrightarrow> m child = None \<or> m child = Some slot \<and> after_in_list (t slot) child = None
 2. \<And>a list. \<lbrakk>last_child slot t = Some child; valid_list_2 t m; m child = Some slot; t slot = a # list\<rbrakk> \<Longrightarrow> m child = None \<or> m child = Some slot \<and> after_in_list (t slot) child = None proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>last_child slot t = Some child; valid_list_2 t m; m child = Some slot; t slot = a # list\<rbrakk> \<Longrightarrow> m child = None \<or> m child = Some slot \<and> after_in_list (t slot) child = None proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>m child = Some slot; t slot = a # list; list \<noteq> []; \<forall>p. set (t p) = {c. m c = Some p}; \<forall>p. distinct (t p); last list = child\<rbrakk> \<Longrightarrow> after_in_list (a # list) child = None proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>m child = Some slot; t slot = a # list; list \<noteq> []; last list = child; set (t slot) = {c. m c = Some slot}; distinct (t slot)\<rbrakk> \<Longrightarrow> after_in_list (a # list) child = None proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>m child = Some slot; t slot = a # list; list \<noteq> []; last list = child; set (t slot) = {c. m c = Some slot}; after_in_list (t slot) (last (t slot)) = None\<rbrakk> \<Longrightarrow> after_in_list (a # list) child = None proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma last_child_set_in_desc:
  "\<lbrakk>valid_list_2 t m; c \<in> last_child_set p t\<rbrakk> \<Longrightarrow> c \<in> descendants_of p m" apply(simp add: last_child_set_def) apply(erule trancl_induct) apply(fastforce simp: child_descendant dest: last_childD) apply(simp) apply(drule(1) last_childD) apply(erule conjE) apply(drule child_descendant) apply(rule descendants_trans) apply(simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; c \<in> last_child_set p t\<rbrakk> \<Longrightarrow> c \<in> descendants_of p m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; (c, p) \<in> {(next, c). last_child c t = Some next}\<^sup>+\<rbrakk> \<Longrightarrow> c \<in> descendants_of p m proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>valid_list_2 t m; (c, y) \<in> {(next, c). last_child c t = Some next}\<rbrakk> \<Longrightarrow> c \<in> descendants_of y m
 2. \<And>y z. \<lbrakk>valid_list_2 t m; (c, y) \<in> {(next, c). last_child c t = Some next}\<^sup>+; (y, z) \<in> {(next, c). last_child c t = Some next}; c \<in> descendants_of y m\<rbrakk> \<Longrightarrow> c \<in> descendants_of z m proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; (c, y) \<in> {(next, c). last_child c t = Some next}\<^sup>+; (y, z) \<in> {(next, c). last_child c t = Some next}; c \<in> descendants_of y m\<rbrakk> \<Longrightarrow> c \<in> descendants_of z m proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; (c, y) \<in> {(next, c). last_child c t = Some next}\<^sup>+; last_child z t = Some y; c \<in> descendants_of y m\<rbrakk> \<Longrightarrow> c \<in> descendants_of z m proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; (c, y) \<in> {(next, c). last_child c t = Some next}\<^sup>+; c \<in> descendants_of y m; m y = Some z \<and> next_sib y t m = None\<rbrakk> \<Longrightarrow> c \<in> descendants_of z m proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; (c, y) \<in> {(next, c). last_child c t = Some next}\<^sup>+; c \<in> descendants_of y m; m y = Some z; next_sib y t m = None\<rbrakk> \<Longrightarrow> c \<in> descendants_of z m proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; (c, y) \<in> {(next, c). last_child c t = Some next}\<^sup>+; c \<in> descendants_of y m; next_sib y t m = None; y \<in> descendants_of z m\<rbrakk> \<Longrightarrow> c \<in> descendants_of z m proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>valid_list_2 t m; (c, y) \<in> {(next, c). last_child c t = Some next}\<^sup>+; c \<in> descendants_of y m; next_sib y t m = None; y \<in> descendants_of z m\<rbrakk> \<Longrightarrow> c \<in> descendants_of (?b15 y z) m
 2. \<And>y z. \<lbrakk>valid_list_2 t m; (c, y) \<in> {(next, c). last_child c t = Some next}\<^sup>+; c \<in> descendants_of y m; next_sib y t m = None; y \<in> descendants_of z m\<rbrakk> \<Longrightarrow> ?b15 y z \<in> descendants_of z m proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma last_child_no_loop:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>valid_list_2 t m; no_mloop m\<rbrakk>
    \<Longrightarrow> x \<notin> last_child_set x t" apply(rule notI) apply(drule(1) last_child_set_in_desc) apply(simp add: no_mloop_descendants) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; no_mloop m\<rbrakk> \<Longrightarrow> x \<notin> last_child_set x t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; no_mloop m; x \<in> last_child_set x t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_mloop m; x \<in> last_child_set x t; x \<in> descendants_of x m\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma last_child_induct:
  "\<lbrakk>\<And>x. last_child x (cdt_list s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; P y\<rbrakk> \<Longrightarrow> P x;
    valid_mdb s; valid_list s\<rbrakk>
    \<Longrightarrow> P slot" apply(induct_tac rule: wf_induct[where r="{(next, p). last_child p (cdt_list s) = Some next}"]) apply(simp add: wf_last_child) apply(fastforce split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. last_child x (cdt_list s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; P y\<rbrakk> \<Longrightarrow> P x; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> P slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. last_child x (cdt_list s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; P y\<rbrakk> \<Longrightarrow> P x; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> wf {(next, p). last_child p (cdt_list s) = Some next}
 2. \<And>x. \<lbrakk>\<And>x. last_child x (cdt_list s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; P y\<rbrakk> \<Longrightarrow> P x; valid_mdb s; valid_list s; \<forall>y. (y, x) \<in> {(next, p). last_child p (cdt_list s) = Some next} \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. last_child x (cdt_list s) = None \<Longrightarrow> P x; \<And>x y. \<lbrakk>last_child x (cdt_list s) = Some y; P y\<rbrakk> \<Longrightarrow> P x; valid_mdb s; valid_list s; \<forall>y. (y, x) \<in> {(next, p). last_child p (cdt_list s) = Some next} \<longrightarrow> P y\<rbrakk> \<Longrightarrow> P x proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma last_last_child_termination:
  "\<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> last_last_child_dom (slot, (cdt_list s))" apply(induct_tac slot rule: last_child_induct[where s=s]) apply(fastforce intro: last_last_child.domintros)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> last_last_child_dom (slot, cdt_list s) proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>valid_mdb s; valid_list s; last_child x (cdt_list s) = None\<rbrakk> \<Longrightarrow> last_last_child_dom (x, cdt_list s)
 2. \<And>x y. \<lbrakk>valid_mdb s; valid_list s; last_child x (cdt_list s) = Some y; last_last_child_dom (y, cdt_list s)\<rbrakk> \<Longrightarrow> last_last_child_dom (x, cdt_list s)
 3. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> valid_mdb s
 4. \<lbrakk>valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> valid_list s proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma last_child_NoneD:
  "\<lbrakk>last_child x t = None; valid_list_2 t m\<rbrakk> \<Longrightarrow> descendants_of x m = {}" by(simp add: last_child_def empty_list_empty_desc split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_child x t = None; valid_list_2 t m\<rbrakk> \<Longrightarrow> descendants_of x m = {}
theory Deterministic_AI

lemma last_child_None_empty_desc:
  "\<lbrakk>last_child slot t = None; valid_list_2 t m\<rbrakk> \<Longrightarrow> descendants_of slot m = {}" by (simp add: last_child_def empty_list_empty_desc split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last_child slot t = None; valid_list_2 t m\<rbrakk> \<Longrightarrow> descendants_of slot m = {}
theory Deterministic_AI

lemma last_child_NoneI:
  "\<lbrakk>descendants_of slot m = {}; valid_list_2 t m\<rbrakk>
    \<Longrightarrow> last_child slot t = None" by (simp add: last_child_def empty_list_empty_desc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_of slot m = {}; valid_list_2 t m\<rbrakk> \<Longrightarrow> last_child slot t = None
theory Deterministic_AI

lemma finite_descendants:
  "valid_mdb s \<Longrightarrow> finite (descendants_of slot (cdt s))" apply(rule_tac B="{p. cte_at p s}" in finite_subset) apply(rule subsetI) apply(simp add: descendants_of_cte_at) apply(simp add: cte_wp_at_set_finite) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> finite (descendants_of slot (cdt s)) proof (prove)
goal (2 subgoals):
 1. valid_mdb s \<Longrightarrow> descendants_of slot (cdt s) \<subseteq> {p. cte_wp_at (\<lambda>_. True) p s}
 2. valid_mdb s \<Longrightarrow> finite {p. cte_wp_at (\<lambda>_. True) p s} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>valid_mdb s; x \<in> descendants_of slot (cdt s)\<rbrakk> \<Longrightarrow> x \<in> {p. cte_wp_at (\<lambda>_. True) p s}
 2. valid_mdb s \<Longrightarrow> finite {p. cte_wp_at (\<lambda>_. True) p s} proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> finite {p. cte_wp_at (\<lambda>_. True) p s} proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma next_sib_2_sib:
  "\<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> cdt s next = Some p" supply if_weak_cong[cong] apply(case_tac "cdt s slot = Some p") apply(simp add: next_sib_2_termination split: if_split_asm) apply(simp split: option.splits if_split_asm) apply(fastforce intro: next_sib_2_sib')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> cdt s next = Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s\<rbrakk> \<Longrightarrow> cdt s next = Some p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot = Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list s; valid_mdb s; cdt s slot = Some p; slot \<in> descendants_of p (cdt s); (case next_slot slot (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s) = Some next\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>valid_list s; valid_mdb s; cdt s slot = Some p; slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some x2; cdt s x2 \<noteq> Some p; next_sib_2 x2 p s = Some next\<rbrakk> \<Longrightarrow> cdt s next = Some p
 2. \<lbrakk>next_sib_2 slot p s = Some next; valid_list s; valid_mdb s; cdt s slot \<noteq> Some p\<rbrakk> \<Longrightarrow> cdt s next = Some p proof (prove)
goal:
No subgoals!
theory Deterministic_AI

lemma ex_imp:
  "\<lbrakk>\<forall>x. P x \<longrightarrow> Q x; \<exists>x. P x\<rbrakk> \<Longrightarrow> \<exists>x. Q x" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. P x \<longrightarrow> Q x; \<exists>x. P x\<rbrakk> \<Longrightarrow> \<exists>x. Q x
theory Deterministic_AI

lemma next_sib_def2:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows "\<lbrakk>valid_mdb s; valid_list s; cdt s slot = Some p\<rbrakk>
    \<Longrightarrow> next_sib_2 slot p s = next_sib slot (cdt_list s) (cdt s)" apply(case_tac "next_sib_2 slot p s") apply(fastforce dest: next_sib_2_None_next_sib) apply(fastforce dest: next_sib_2_eq_next_sib) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_list s; cdt s slot = Some p\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = next_sib slot (cdt_list s) (cdt s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb s; valid_list s; cdt s slot = Some p; next_sib_2 slot p s = None\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = next_sib slot (cdt_list s) (cdt s)
 2. \<And>a. \<lbrakk>valid_mdb s; valid_list s; cdt s slot = Some p; next_sib_2 slot p s = Some a\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = next_sib slot (cdt_list s) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>valid_mdb s; valid_list s; cdt s slot = Some p; next_sib_2 slot p s = Some a\<rbrakk> \<Longrightarrow> next_sib_2 slot p s = next_sib slot (cdt_list s) (cdt s) proof (prove)
goal:
No subgoals!
theory ArchDeterministic_AI

lemma perform_page_table_invocation_valid_list[wp]:
  "\<lbrace>valid_list\<rbrace> perform_page_table_invocation a \<lbrace>\<lambda>_.valid_list\<rbrace>" apply (simp add: perform_page_table_invocation_def) apply (cases a,simp_all) apply (wp mapM_x_wp' | intro impI conjI allI | wpc | simp split: cap.splits arch_cap.splits option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> perform_page_table_invocation a \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> case a of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do set_cap cap ct_slot;
store_pde pd_slot pde;
do_machine_op $ cleanByVA_PoU pd_slot (addrFromPPtr pd_slot)
od | PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap ct_slot;
set_cap (ArchObjectCap $ update_map_data cap None) ct_slot
od | PageTableUnmap (ArchObjectCap _) ct_slot \<Rightarrow> fail | PageTableUnmap _ ct_slot \<Rightarrow> fail \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 x14. a = PageTableMap x11 x12 x13 x14 \<Longrightarrow> \<lbrace>valid_list\<rbrace> do y <- set_cap x11 x12;
y <- store_pde x14 x13;
do_machine_op (cleanByVA_PoU x14 (addrFromPPtr x14))
od \<lbrace>\<lambda>_. valid_list\<rbrace>
 2. \<And>x21 x22. a = PageTableUnmap x21 x22 \<Longrightarrow> \<lbrace>valid_list\<rbrace> case x21 of ArchObjectCap (PageTableCap p mapped_address) \<Rightarrow> do case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do unmap_page_table asid vaddr p;
pte_bits <- return 2;
slots <- return [p , p + (1 << pte_bits) .e. p + (1 << pt_bits) - 1];
mapM_x (swp store_pte InvalidPTE) slots;
do_machine_op $ cleanCacheRange_PoU p (p + (1 << pt_bits) - 1) (addrFromPPtr p)
od;
cap <- liftM the_arch_cap $ get_cap x22;
set_cap (ArchObjectCap $ update_map_data cap None) x22
od | ArchObjectCap _ \<Rightarrow> fail | _ \<Rightarrow> fail \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchDeterministic_AI

lemma handle_vm_fault_valid_list[wp, Deterministic_AI_assms]:
"\<lbrace>valid_list\<rbrace> handle_vm_fault thread fault \<lbrace>\<lambda>_.valid_list\<rbrace>" apply (cases fault,simp_all) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> handle_vm_fault thread fault \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. fault = ARMDataAbort \<Longrightarrow> \<lbrace>valid_list\<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>_. valid_list\<rbrace>
 2. fault = ARMPrefetchAbort \<Longrightarrow> \<lbrace>valid_list\<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>_. valid_list\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchDeterministic_AI

lemma handle_interrupt_valid_list[wp, Deterministic_AI_assms]:
  "\<lbrace>valid_list\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_.valid_list\<rbrace>" unfolding handle_interrupt_def ackInterrupt_def apply (rule hoare_pre) by (wp get_cap_wp  do_machine_op_valid_list
       | wpc | simp add: get_irq_slot_def handle_reserved_irq_def arch_mask_irq_signal_def
       | wp (once) hoare_drop_imps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_list\<rbrace> if maxIRQ < irq then do_machine_op $ do maskInterrupt True irq;
machine_op_lift (ackInterrupt_impl irq)
od else do st <- get_irq_state irq;
case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op $ machine_op_lift (ackInterrupt_impl irq)
od \<lbrace>\<lambda>_. valid_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if maxIRQ < irq then do_machine_op $ do maskInterrupt True irq;
machine_op_lift (ackInterrupt_impl irq)
od else do st <- get_irq_state irq;
case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op $ machine_op_lift (ackInterrupt_impl irq)
od \<lbrace>\<lambda>_. valid_list\<rbrace>
 2. \<And>s. valid_list s \<Longrightarrow> ?Q s
theory DetSchedInvs_AI

lemma get_etcb_rev:
  "ekheap s p = Some etcb \<Longrightarrow> get_etcb p s = Some etcb" by (clarsimp simp: get_etcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ekheap s p = Some etcb \<Longrightarrow> get_etcb p s = Some etcb
theory DetSchedInvs_AI

lemma get_etcb_SomeD: "get_etcb ptr s = Some v \<Longrightarrow> ekheap s ptr = Some v" apply (case_tac "ekheap s ptr", simp_all add: get_etcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_etcb ptr s = Some v \<Longrightarrow> ekheap s ptr = Some v proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma obj_at_kh_simp[simp]: "obj_at_kh P ref (kheap st) = obj_at P ref st" apply (simp add: obj_at_def obj_at_kh_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at_kh P ref (kheap st) = obj_at P ref st proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma st_tcb_at_kh_simp[simp]: "st_tcb_at_kh test t (kheap st) = st_tcb_at test t st" apply (simp add: pred_tcb_at_def st_tcb_at_kh_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at_kh test t (kheap st) = st_tcb_at test t st proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma etcb_at_taut[simp]: "etcb_at' \<top> ref ekh" apply (simp add: etcb_at'_def split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. etcb_at' (\<lambda>_. True) ref ekh proof (prove)
goal:
No subgoals!