kings-crown/FVELER_Isabelle huggingface dataset:
theory Example_Valid_State

lemma empty_cnode_eq_Some [simp]:
    "(empty_cnode n x = Some y) = (length x = n \<and> y = NullCap)" by (clarsimp simp: empty_cnode_def, metis)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (empty_cnode n x = Some y) = (length x = n \<and> y = NullCap)
theory Example_Valid_State

lemma empty_cnode_eq_None [simp]:
    "(empty_cnode n x = None) = (length x \<noteq> n)" by (clarsimp simp: empty_cnode_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (empty_cnode n x = None) = (length x \<noteq> n)
theory Example_Valid_State

lemma ran_empty_cnode [simp]:
    "ran (empty_cnode C) = {NullCap}" by (auto simp: empty_cnode_def ran_def Ex_list_of_length intro: set_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran (empty_cnode C) = {NullCap}
theory Example_Valid_State

lemma empty_cnode_app [simp]:
    "length x = n \<Longrightarrow> empty_cnode n x = Some NullCap" by (auto simp: empty_cnode_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length x = n \<Longrightarrow> empty_cnode n x = Some NullCap
theory Example_Valid_State

lemma in_ran_If [simp]:
      "(x \<in> ran (\<lambda>n. if P n then A n else B n))
            \<longleftrightarrow>  (\<exists>n. P n \<and> A n = Some x) \<or> (\<exists>n. \<not> P n \<and> B n = Some x)" by (auto simp: ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<in> ran (\<lambda>n. if P n then A n else B n)) = ((\<exists>n. P n \<and> A n = Some x) \<or> (\<exists>n. \<not> P n \<and> B n = Some x))
theory Example_Valid_State

lemma Low_caps_ran:
  "ran Low_caps = {ThreadCap Low_tcb_ptr,
                   CNodeCap Low_cnode_ptr 10 (the_nat_to_bl_10 2),
                   ArchObjectCap (PageDirectoryCap Low_pd_ptr
                                              (Some Low_asid)),
                   NotificationCap ntfn_ptr 0 {AllowSend},
                   NullCap}" apply (rule equalityI) apply (clarsimp simp: Low_caps_def fun_upd_def empty_cnode_def split: if_split_asm) apply (clarsimp simp: Low_caps_def fun_upd_def empty_cnode_def split: if_split_asm
                  cong: conj_cong) apply (rule exI [where x="the_nat_to_bl_10 0"]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran Low_caps = {ThreadCap Low_tcb_ptr, CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), NotificationCap ntfn_ptr 0 {AllowSend}, NullCap} proof (prove)
goal (2 subgoals):
 1. ran Low_caps \<subseteq> {ThreadCap Low_tcb_ptr, CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), NotificationCap ntfn_ptr 0 {AllowSend}, NullCap}
 2. {ThreadCap Low_tcb_ptr, CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), NotificationCap ntfn_ptr 0 {AllowSend}, NullCap} \<subseteq> ran Low_caps proof (prove)
goal (1 subgoal):
 1. {ThreadCap Low_tcb_ptr, CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid)), NotificationCap ntfn_ptr 0 {AllowSend}, NullCap} \<subseteq> ran Low_caps proof (prove)
goal (1 subgoal):
 1. \<exists>x. (length x = 10 \<longrightarrow> x \<noteq> the_nat_to_bl 10 (Suc 0) \<and> x \<noteq> the_nat_to_bl 10 2 \<and> x \<noteq> the_nat_to_bl 10 3 \<and> x \<noteq> the_nat_to_bl 10 318) \<and> length x = 10 proof (prove)
goal (1 subgoal):
 1. (length (the_nat_to_bl 10 0) = 10 \<longrightarrow> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 (Suc 0) \<and> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 2 \<and> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 3 \<and> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 318) \<and> length (the_nat_to_bl 10 0) = 10 proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma High_caps_ran:
  "ran High_caps = {ThreadCap High_tcb_ptr,
                    CNodeCap High_cnode_ptr 10 (the_nat_to_bl_10 2),
                    ArchObjectCap (PageDirectoryCap High_pd_ptr
                                               (Some High_asid)),
                    NotificationCap ntfn_ptr 0 {AllowRecv},
                    NullCap}" apply (rule equalityI) apply (clarsimp simp: High_caps_def ran_def empty_cnode_def split: if_split_asm) apply (clarsimp simp: High_caps_def ran_def empty_cnode_def split: if_split_asm
                  cong: conj_cong) apply (rule exI [where x="the_nat_to_bl_10 0"]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran High_caps = {ThreadCap High_tcb_ptr, CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), NotificationCap ntfn_ptr 0 {AllowRecv}, NullCap} proof (prove)
goal (2 subgoals):
 1. ran High_caps \<subseteq> {ThreadCap High_tcb_ptr, CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), NotificationCap ntfn_ptr 0 {AllowRecv}, NullCap}
 2. {ThreadCap High_tcb_ptr, CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), NotificationCap ntfn_ptr 0 {AllowRecv}, NullCap} \<subseteq> ran High_caps proof (prove)
goal (1 subgoal):
 1. {ThreadCap High_tcb_ptr, CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid)), NotificationCap ntfn_ptr 0 {AllowRecv}, NullCap} \<subseteq> ran High_caps proof (prove)
goal (1 subgoal):
 1. \<exists>a. (length a = 10 \<longrightarrow> a \<noteq> the_nat_to_bl 10 (Suc 0) \<and> a \<noteq> the_nat_to_bl 10 2 \<and> a \<noteq> the_nat_to_bl 10 3 \<and> a \<noteq> the_nat_to_bl 10 318) \<and> length a = 10 proof (prove)
goal (1 subgoal):
 1. (length (the_nat_to_bl 10 0) = 10 \<longrightarrow> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 (Suc 0) \<and> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 2 \<and> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 3 \<and> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 318) \<and> length (the_nat_to_bl 10 0) = 10 proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma Silc_caps_ran:
  "ran Silc_caps = {CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl_10 2),
                    NotificationCap ntfn_ptr 0 {AllowSend},
                    NullCap}" apply (rule equalityI) apply (clarsimp simp: Silc_caps_def ran_def empty_cnode_def) apply (clarsimp simp: ran_def Silc_caps_def empty_cnode_def cong: conj_cong) apply (rule_tac x="the_nat_to_bl_10 0" in exI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran Silc_caps = {CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2), NotificationCap ntfn_ptr 0 {AllowSend}, NullCap} proof (prove)
goal (2 subgoals):
 1. ran Silc_caps \<subseteq> {CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2), NotificationCap ntfn_ptr 0 {AllowSend}, NullCap}
 2. {CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2), NotificationCap ntfn_ptr 0 {AllowSend}, NullCap} \<subseteq> ran Silc_caps proof (prove)
goal (1 subgoal):
 1. {CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2), NotificationCap ntfn_ptr 0 {AllowSend}, NullCap} \<subseteq> ran Silc_caps proof (prove)
goal (1 subgoal):
 1. \<exists>a. (length a = 10 \<longrightarrow> a \<noteq> the_nat_to_bl 10 2 \<and> a \<noteq> the_nat_to_bl 10 318) \<and> length a = 10 proof (prove)
goal (1 subgoal):
 1. (length (the_nat_to_bl 10 0) = 10 \<longrightarrow> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 2 \<and> the_nat_to_bl 10 0 \<noteq> the_nat_to_bl 10 318) \<and> length (the_nat_to_bl 10 0) = 10 proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma irq_node_offs_max:
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) < init_irq_node_ptr + 0x4000" apply (simp add: s0_ptr_defs cte_level_bits_def shiftl_t2n) apply (cut_tac x=irq and 'a=32 in ucast_less) apply simp apply (simp add: word_less_nat_alt unat_word_ariths) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) < init_irq_node_ptr + 0x4000 proof (prove)
goal (1 subgoal):
 1. 0xE0008000 + 0x10 * UCAST(10 \<rightarrow> 32) irq < 0xE000C000 proof (prove)
goal (2 subgoals):
 1. LENGTH(10) < LENGTH(32)
 2. UCAST(10 \<rightarrow> 32) irq < 2 ^ LENGTH(10) \<Longrightarrow> 0xE0008000 + 0x10 * UCAST(10 \<rightarrow> 32) irq < 0xE000C000 proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) irq < 2 ^ LENGTH(10) \<Longrightarrow> 0xE0008000 + 0x10 * UCAST(10 \<rightarrow> 32) irq < 0xE000C000 proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma irq_node_offs_in_range:
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits)
     \<in> irq_node_offs_range" apply (clarsimp simp: irq_node_offs_min irq_node_offs_max irq_node_offs_range_def) apply (rule is_aligned_add[OF _ is_aligned_shift]) apply (simp add: is_aligned_def s0_ptr_defs cte_level_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<in> irq_node_offs_range proof (prove)
goal (1 subgoal):
 1. is_aligned (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits)) cte_level_bits proof (prove)
goal (1 subgoal):
 1. is_aligned init_irq_node_ptr cte_level_bits proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma irq_node_offs_range_distinct[simp]:
  "Low_cnode_ptr \<notin> irq_node_offs_range"
  "High_cnode_ptr \<notin> irq_node_offs_range"
  "Silc_cnode_ptr \<notin> irq_node_offs_range"
  "ntfn_ptr \<notin> irq_node_offs_range"
  "irq_cnode_ptr \<notin> irq_node_offs_range"
  "Low_pd_ptr \<notin> irq_node_offs_range"
  "High_pd_ptr \<notin> irq_node_offs_range"
  "Low_pt_ptr \<notin> irq_node_offs_range"
  "High_pt_ptr \<notin> irq_node_offs_range"
  "Low_tcb_ptr \<notin> irq_node_offs_range"
  "High_tcb_ptr \<notin> irq_node_offs_range"
  "idle_tcb_ptr \<notin> irq_node_offs_range"
  "init_globals_frame \<notin> irq_node_offs_range"
  "init_global_pd \<notin> irq_node_offs_range" by(simp add:irq_node_offs_range_def s0_ptr_defs)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Low_cnode_ptr \<notin> irq_node_offs_range &&& High_cnode_ptr \<notin> irq_node_offs_range &&& Silc_cnode_ptr \<notin> irq_node_offs_range) &&& (ntfn_ptr \<notin> irq_node_offs_range &&& irq_cnode_ptr \<notin> irq_node_offs_range) &&& Low_pd_ptr \<notin> irq_node_offs_range &&& High_pd_ptr \<notin> irq_node_offs_range) &&& (Low_pt_ptr \<notin> irq_node_offs_range &&& High_pt_ptr \<notin> irq_node_offs_range &&& Low_tcb_ptr \<notin> irq_node_offs_range) &&& (High_tcb_ptr \<notin> irq_node_offs_range &&& idle_tcb_ptr \<notin> irq_node_offs_range) &&& init_globals_frame \<notin> irq_node_offs_range &&& init_global_pd \<notin> irq_node_offs_range
theory Example_Valid_State

lemma irq_node_offs_distinct[simp]:
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> Low_cnode_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> High_cnode_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> Silc_cnode_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> ntfn_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> irq_cnode_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> Low_pd_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> High_pd_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> Low_pt_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> High_pt_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> Low_tcb_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> High_tcb_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> idle_tcb_ptr"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> init_globals_frame"
  "init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits) \<noteq> init_global_pd" by (simp add:not_inD[symmetric, OF _ irq_node_offs_in_range])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> Low_cnode_ptr &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> High_cnode_ptr &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> Silc_cnode_ptr) &&& (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> ntfn_ptr &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> irq_cnode_ptr) &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> Low_pd_ptr &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> High_pd_ptr) &&& (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> Low_pt_ptr &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> High_pt_ptr &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> Low_tcb_ptr) &&& (init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> High_tcb_ptr &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> idle_tcb_ptr) &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> init_globals_frame &&& init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) \<noteq> init_global_pd
theory Example_Valid_State

lemma kh0_SomeD:
  "kh0 x = Some y \<Longrightarrow>
        x = init_globals_frame \<and> y = ArchObj (DataPage False ARMSmallPage) \<or>
        x = init_global_pd \<and> y = ArchObj (PageDirectory global_pd) \<or>
        x = idle_tcb_ptr \<and> y = idle_tcb \<or>
        x = High_tcb_ptr \<and> y = High_tcb \<or>
        x = Low_tcb_ptr \<and> y = Low_tcb \<or>
        x = High_pt_ptr \<and> y = High_pt \<or>
        x = Low_pt_ptr \<and> y = Low_pt \<or>
        x = High_pd_ptr \<and> y = High_pd \<or>
        x = Low_pd_ptr \<and> y = Low_pd \<or>
        x = irq_cnode_ptr \<and> y = irq_cnode \<or>
        x = ntfn_ptr \<and> y = ntfn \<or>
        x = Silc_cnode_ptr \<and> y = Silc_cnode \<or>
        x = High_cnode_ptr \<and> y = High_cnode \<or>
        x = Low_cnode_ptr \<and> y = Low_cnode \<or>
        x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0)" apply (frule kh0_SomeD') apply (erule disjE, simp add: kh0_def
        | force simp: kh0_def split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kh0 x = Some y \<Longrightarrow> x = init_globals_frame \<and> y = ArchObj (DataPage False ARMSmallPage) \<or> x = init_global_pd \<and> y = ArchObj (PageDirectory global_pd) \<or> x = idle_tcb_ptr \<and> y = idle_tcb \<or> x = High_tcb_ptr \<and> y = High_tcb \<or> x = Low_tcb_ptr \<and> y = Low_tcb \<or> x = High_pt_ptr \<and> y = High_pt \<or> x = Low_pt_ptr \<and> y = Low_pt \<or> x = High_pd_ptr \<and> y = High_pd \<or> x = Low_pd_ptr \<and> y = Low_pd \<or> x = irq_cnode_ptr \<and> y = irq_cnode \<or> x = ntfn_ptr \<and> y = ntfn \<or> x = Silc_cnode_ptr \<and> y = Silc_cnode \<or> x = High_cnode_ptr \<and> y = High_cnode \<or> x = Low_cnode_ptr \<and> y = Low_cnode \<or> x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh0 x = Some y; x = init_globals_frame \<or> x = init_global_pd \<or> x = idle_tcb_ptr \<or> x = High_tcb_ptr \<or> x = Low_tcb_ptr \<or> x = High_pt_ptr \<or> x = Low_pt_ptr \<or> x = High_pd_ptr \<or> x = Low_pd_ptr \<or> x = irq_cnode_ptr \<or> x = ntfn_ptr \<or> x = Silc_cnode_ptr \<or> x = High_cnode_ptr \<or> x = Low_cnode_ptr \<or> x \<in> irq_node_offs_range\<rbrakk> \<Longrightarrow> x = init_globals_frame \<and> y = ArchObj (DataPage False ARMSmallPage) \<or> x = init_global_pd \<and> y = ArchObj (PageDirectory global_pd) \<or> x = idle_tcb_ptr \<and> y = idle_tcb \<or> x = High_tcb_ptr \<and> y = High_tcb \<or> x = Low_tcb_ptr \<and> y = Low_tcb \<or> x = High_pt_ptr \<and> y = High_pt \<or> x = Low_pt_ptr \<and> y = Low_pt \<or> x = High_pd_ptr \<and> y = High_pd \<or> x = Low_pd_ptr \<and> y = Low_pd \<or> x = irq_cnode_ptr \<and> y = irq_cnode \<or> x = ntfn_ptr \<and> y = ntfn \<or> x = Silc_cnode_ptr \<and> y = Silc_cnode \<or> x = High_cnode_ptr \<and> y = High_cnode \<or> x = Low_cnode_ptr \<and> y = Low_cnode \<or> x \<in> irq_node_offs_range \<and> y = CNode 0 (empty_cnode 0) proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma High_caps_well_formed: "well_formed_cnode_n 10 High_caps" by (auto simp: High_caps_def well_formed_cnode_n_def  split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n 10 High_caps
theory Example_Valid_State

lemma Low_caps_well_formed: "well_formed_cnode_n 10 Low_caps" by (auto simp: Low_caps_def well_formed_cnode_n_def  split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n 10 Low_caps
theory Example_Valid_State

lemma Silc_caps_well_formed: "well_formed_cnode_n 10 Silc_caps" by (auto simp: Silc_caps_def well_formed_cnode_n_def  split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n 10 Silc_caps
theory Example_Valid_State

lemma tcb_states_of_state_s0:
  "tcb_states_of_state s0_internal = [High_tcb_ptr \<mapsto> thread_state.BlockedOnNotification ntfn_ptr,  Low_tcb_ptr \<mapsto> thread_state.Running, idle_tcb_ptr \<mapsto> thread_state.IdleThreadState ]" unfolding s0_internal_def tcb_states_of_state_def apply (rule ext) apply (simp add: get_tcb_def) apply (simp add: kh0_def kh0_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_states_of_state s0_internal = [High_tcb_ptr \<mapsto> BlockedOnNotification ntfn_ptr, Low_tcb_ptr \<mapsto> Running, idle_tcb_ptr \<mapsto> IdleThreadState] proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. map_option tcb_state (get_tcb p \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>)) = [High_tcb_ptr \<mapsto> BlockedOnNotification ntfn_ptr, Low_tcb_ptr \<mapsto> Running, idle_tcb_ptr \<mapsto> IdleThreadState] proof (prove)
goal (1 subgoal):
 1. \<And>p. map_option tcb_state (get_tcb p \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr>) = [High_tcb_ptr \<mapsto> BlockedOnNotification ntfn_ptr, Low_tcb_ptr \<mapsto> Running, idle_tcb_ptr \<mapsto> IdleThreadState] p proof (prove)
goal (1 subgoal):
 1. \<And>p. (p = High_tcb_ptr \<longrightarrow> (\<exists>z. (case kh0 High_tcb_ptr of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) = Some z \<and> tcb_state z = BlockedOnNotification ntfn_ptr)) \<and> (p \<noteq> High_tcb_ptr \<longrightarrow> (p = Low_tcb_ptr \<longrightarrow> (\<exists>z. (case kh0 Low_tcb_ptr of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) = Some z \<and> tcb_state z = Running)) \<and> (p \<noteq> Low_tcb_ptr \<longrightarrow> (p = idle_tcb_ptr \<longrightarrow> (\<exists>z. (case kh0 idle_tcb_ptr of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) = Some z \<and> idle (tcb_state z))) \<and> (p \<noteq> idle_tcb_ptr \<longrightarrow> (case kh0 p of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) = None))) proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma thread_bounds_of_state_s0:
  "thread_bound_ntfns s0_internal = Map.empty" unfolding s0_internal_def thread_bound_ntfns_def apply (rule ext) apply (simp add: get_tcb_def) apply (simp add: kh0_def kh0_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_bound_ntfns s0_internal = (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. case get_tcb p \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr> of None \<Rightarrow> None | Some x \<Rightarrow> tcb_bound_notification x) = (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<And>p. (case get_tcb p \<lparr>kheap = kh0, cdt = \<lambda>x. None, is_original_cap = (\<lambda>_. False)((Low_tcb_ptr, tcb_cnode_index 2) := True, (High_tcb_ptr, tcb_cnode_index 2) := True), cur_thread = Low_tcb_ptr, idle_thread = idle_tcb_ptr, machine_state = machine_state0, interrupt_irq_node = \<lambda>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits), interrupt_states = (\<lambda>_. IRQInactive)(timer_irq := IRQTimer), arch_state = arch_state0, exst = exst0\<rparr> of None \<Rightarrow> None | Some x \<Rightarrow> tcb_bound_notification x) = None proof (prove)
goal (1 subgoal):
 1. \<And>p. (case case kh0 p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | Some _ \<Rightarrow> None of None \<Rightarrow> None | Some x \<Rightarrow> tcb_bound_notification x) = None proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma Sys1_wellformed':
  "policy_wellformed (pasPolicy Sys1PAS) False irqs x" apply (clarsimp simp: Sys1PAS_def policy_wellformed_def Sys1AuthGraph_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. policy_wellformed (pasPolicy Sys1PAS) False irqs x proof (prove)
goal:
No subgoals!
theory Example_Valid_State

lemma Sys1_pas_wellformed:
  "pas_wellformed Sys1PAS" apply (clarsimp simp: Sys1PAS_def policy_wellformed_def Sys1AuthGraph_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_wellformed Sys1PAS proof (prove)
goal:
No subgoals!