kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchSyscall_AC

lemma handle_vm_fault_integrity[Syscall_AC_assms]:
  "\<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace>
   handle_vm_fault thread vmfault_type
   \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" apply (cases vmfault_type, simp_all) apply (rule hoare_pre) apply (wp as_user_integrity_autarch dmo_wp | simp add: getDFSR_def getFAR_def getIFSR_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>rv. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag thread)\<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. integrity aag X st\<rbrace>
 2. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag thread)\<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. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. vmfault_type = ARMDataAbort \<Longrightarrow> \<lbrace>?Q2\<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. integrity aag X st\<rbrace>
 2. \<And>s. \<lbrakk>vmfault_type = ARMDataAbort; (integrity aag X st and (\<lambda>y. is_subject aag thread)) s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. vmfault_type = ARMPrefetchAbort \<Longrightarrow> \<lbrace>integrity aag X st and (\<lambda>y. is_subject aag thread)\<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. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSyscall_AC

lemma getActiveIRQ_inv[Syscall_AC_assms]:
  "\<forall>f s. P s \<longrightarrow> P (irq_state_update f s) \<Longrightarrow>
   \<lbrace>P\<rbrace> getActiveIRQ irq \<lbrace>\<lambda>rv. P\<rbrace>" by (wpsimp simp: irq_state_independent_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>f s. P s \<longrightarrow> P (irq_state_update f s) \<Longrightarrow> \<lbrace>P\<rbrace> getActiveIRQ irq \<lbrace>\<lambda>rv. P\<rbrace>
theory ArchSyscall_AC

lemma getActiveIRQ_rv_None[Syscall_AC_assms]:
  "\<lbrace>\<top>\<rbrace> getActiveIRQ True \<lbrace>\<lambda>rv ms. (rv \<noteq> None \<longrightarrow> the rv \<notin> non_kernel_IRQs)\<rbrace>" by (wpsimp simp: getActiveIRQ_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getActiveIRQ True \<lbrace>\<lambda>rv ms. rv \<noteq> None \<longrightarrow> the rv \<notin> non_kernel_IRQs\<rbrace>
theory ArchSyscall_AC

lemma arch_activate_idle_thread_respects[Syscall_AC_assms, wp]:
  "arch_activate_idle_thread t \<lbrace>integrity aag X st\<rbrace>" unfolding arch_activate_idle_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> arch_activate_idle_thread t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchSyscall_AC

lemma arch_activate_idle_thread_pas_refined[Syscall_AC_assms, wp]:
  "arch_activate_idle_thread t \<lbrace>pas_refined aag\<rbrace>" unfolding arch_activate_idle_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> arch_activate_idle_thread t \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> return () \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory ArchSyscall_AC

lemma dmo_clearExMonitor_respects_globals[Syscall_AC_assms, wp]:
  "do_machine_op clearExMonitor \<lbrace>integrity aag X st\<rbrace>" by (wpsimp wp: dmo_wp simp: clearExMonitor_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchSyscall_AC

lemma arch_switch_to_thread_respects[Syscall_AC_assms, wp]:
  "arch_switch_to_thread t \<lbrace>integrity aag X st\<rbrace>" unfolding arch_switch_to_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> do set_vm_root t;
do_machine_op $ clearExMonitor
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchSyscall_AC

lemma arch_switch_to_thread_pas_refined[Syscall_AC_assms, wp]:
  "arch_switch_to_thread t \<lbrace>pas_refined aag\<rbrace>" unfolding arch_switch_to_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> do set_vm_root t;
do_machine_op $ clearExMonitor
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory ArchSyscall_AC

lemma arch_switch_to_idle_thread_respects[Syscall_AC_assms, wp]:
  "arch_switch_to_idle_thread \<lbrace>integrity aag X st\<rbrace>" unfolding arch_switch_to_idle_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st\<rbrace> gets idle_thread >>= set_vm_root \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
theory ArchSyscall_AC

lemma arch_switch_to_idle_thread_pas_refined[Syscall_AC_assms, wp]:
  "arch_switch_to_idle_thread \<lbrace>pas_refined aag\<rbrace>" unfolding arch_switch_to_idle_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> gets idle_thread >>= set_vm_root \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
theory ArchSyscall_AC

lemma arch_mask_irq_signal_arch_state[Syscall_AC_assms, wp]:
  "arch_mask_irq_signal irq \<lbrace>\<lambda>s :: det_ext state. P (arch_state s)\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> arch_mask_irq_signal irq \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>
theory ArchSyscall_AC

lemma handle_reserved_irq_arch_state[Syscall_AC_assms, wp]:
  "handle_reserved_irq irq \<lbrace>\<lambda>s :: det_ext state. P (arch_state s)\<rbrace>" unfolding handle_reserved_irq_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> handle_reserved_irq irq \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> return () \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>
theory ADT_AC

lemma user_op_access':
  "\<lbrakk> invs s; pas_refined aag s; is_subject aag tcb;
     ptable_lift tcb s x = Some (addrFromPPtr ptr);
     auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x) \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag auth tcb ptr" by (auto dest: user_op_access simp: ptrFormPAddr_addFromPPtr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some (addrFromPPtr ptr); auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag ptr) \<in> pasPolicy aag
theory ADT_AC

lemma dmo_user_memory_update_respects_Write:
  "\<lbrace>integrity aag X st and K (\<forall>p \<in> dom um. aag_has_auth_to aag Write p)\<rbrace>
   do_machine_op (user_memory_update um)
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" unfolding user_memory_update_def apply (wp dmo_wp) apply clarsimp apply (rule integrity_underlying_mem_update; simp?) apply (simp add: dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (\<forall>p\<in>dom um. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)\<rbrace> do_machine_op (user_memory_update um) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (\<forall>p\<in>dom um. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)\<rbrace> do_machine_op (modify (\<lambda>ms. ms\<lparr>underlying_memory := \<lambda>a. case um a of None \<Rightarrow> underlying_memory ms a | Some x \<Rightarrow> x\<rparr>)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and K (\<forall>p\<in>dom um. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)) s \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<lparr>underlying_memory := \<lambda>a. case um a of None \<Rightarrow> underlying_memory (machine_state s) a | Some x \<Rightarrow> x\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<lparr>underlying_memory := \<lambda>a. case um a of None \<Rightarrow> underlying_memory (machine_state s) a | Some x \<Rightarrow> x\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x\<in>- dom um. (case um x of None \<Rightarrow> underlying_memory (machine_state s) x | Some x \<Rightarrow> x) = underlying_memory (machine_state s) x proof (prove)
goal:
No subgoals!
theory ADT_AC

lemma dmo_um_upd_machine_state:
  "do_machine_op (user_memory_update ms) \<lbrace>\<lambda>s. P (device_state (machine_state s))\<rbrace>" by (rule dmo_wp) (simp add: user_memory_update_def simpler_modify_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (device_state (machine_state s))\<rbrace> do_machine_op (user_memory_update ms) \<lbrace>\<lambda>_ s. P (device_state (machine_state s))\<rbrace>
theory ADT_AC

lemma objs_valid_tcb_vtable:
  "\<lbrakk> valid_objs s; get_tcb t s = Some tcb \<rbrakk> \<Longrightarrow> s \<turnstile> tcb_vtable tcb" apply (clarsimp simp: get_tcb_def split: option.splits Structures_A.kernel_object.splits) apply (erule cte_wp_valid_cap[rotated]) apply (rule cte_wp_at_tcbI[where t="(a, b)" for a b, where b3="tcb_cnode_index 1"]) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_vtable tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_vtable tcb proof (prove)
goal (1 subgoal):
 1. kheap s t = Some (TCB tcb) \<Longrightarrow> cte_wp_at ((=) (tcb_vtable tcb)) ?p40 s proof (prove)
goal (3 subgoals):
 1. kheap s t = Some (TCB tcb) \<Longrightarrow> kheap s (fst (?a45, tcb_cnode_index 1)) = Some (TCB ?tcb42)
 2. kheap s t = Some (TCB tcb) \<Longrightarrow> tcb_cap_cases (snd (?a45, tcb_cnode_index 1)) = Some (?getF42, ?setF42)
 3. kheap s t = Some (TCB tcb) \<Longrightarrow> tcb_vtable tcb = ?getF42 ?tcb42 proof (prove)
goal:
No subgoals!
theory ArchADT_AC

lemma invs_valid_global_pd_mappings:
  "invs s \<Longrightarrow> valid_global_vspace_mappings s" apply (simp add: invs_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_global_vspace_mappings s proof (prove)
goal:
No subgoals!
theory ArchADT_AC

lemma kernel_mappings_kernel_mapping_slots:
  "x \<notin> kernel_mappings \<Longrightarrow> ucast (x >> 20) \<notin> kernel_mapping_slots" apply (rule kernel_base_kernel_mapping_slots) apply (simp add: kernel_mappings_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> kernel_mappings \<Longrightarrow> UCAST(32 \<rightarrow> 12) (x >> 20) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. x \<notin> kernel_mappings \<Longrightarrow> x < kernel_base proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma nat_to_bl_id [simp]: "nat_to_bl (size (x :: (('a::len) word))) (unat x) = Some (to_bl x)" apply (clarsimp simp: nat_to_bl_def to_bl_def) apply (auto simp: le_def word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nat_to_bl (size x) (unat x) = Some (to_bl x) proof (prove)
goal (1 subgoal):
 1. \<not> 2 ^ size x \<le> unat x \<and> (\<not> 2 ^ size x \<le> unat x \<longrightarrow> bin_to_bl_aux (size x) (uint x) [] = bin_to_bl_aux LENGTH('a) (uint x) []) proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma tcb_cnode_index_nat_to_bl:
  "n<10 \<Longrightarrow> the_nat_to_bl_10 n \<noteq> tcb_cnode_index n" by (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def
                     tcb_cnode_index_def
                     nat_to_bl_def to_bl_def bin_to_bl_aux_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 10 \<Longrightarrow> the_nat_to_bl_10 n \<noteq> tcb_cnode_index n
theory ExampleSystem

lemma "asid_high_bits_of asid1_3065 \<noteq> asid_high_bits_of asid1_3063" by (simp add: asid1_3063_def asid_high_bits_of_def asid1_3065_def asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_high_bits_of asid1_3065 \<noteq> asid_high_bits_of asid1_3063
theory ExampleSystem

lemma caps1_7_well_formed: "well_formed_cnode_n 10 caps1_7" apply (clarsimp simp: caps1_7_def well_formed_cnode_n_def) apply (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def nat_to_bl_def) apply (clarsimp simp: empty_cnode_def dom_def) apply (rule set_eqI, clarsimp) apply (rule iffI) apply (elim disjE, insert len_bin_to_bl, simp_all)[1] apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n 10 caps1_7 proof (prove)
goal (1 subgoal):
 1. insert (the_nat_to_bl_10 318) (insert (the_nat_to_bl_10 3) (insert (the_nat_to_bl_10 2) (insert (the_nat_to_bl_10 (Suc 0)) (dom (empty_cnode 10))))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. insert [False, True, False, False, True, True, True, True, True, False] (insert [False, False, False, False, False, False, False, False, True, True] (insert [False, False, False, False, False, False, False, False, True, False] (insert [False, False, False, False, False, False, False, False, False, True] (dom (empty_cnode 10))))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. insert [False, True, False, False, True, True, True, True, True, False] (insert [False, False, False, False, False, False, False, False, True, True] (insert [False, False, False, False, False, False, False, False, True, False] (insert [False, False, False, False, False, False, False, False, False, True] {a. length a = 10}))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. \<And>x. (x = [False, True, False, False, True, True, True, True, True, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10) = (length x = 10) proof (prove)
goal (2 subgoals):
 1. \<And>x. x = [False, True, False, False, True, True, True, True, True, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 \<Longrightarrow> length x = 10
 2. \<And>x. length x = 10 \<Longrightarrow> x = [False, True, False, False, True, True, True, True, True, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 proof (prove)
goal (1 subgoal):
 1. \<And>x. length x = 10 \<Longrightarrow> x = [False, True, False, False, True, True, True, True, True, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma caps1_6_well_formed: "well_formed_cnode_n 10 caps1_6" apply (clarsimp simp: caps1_6_def well_formed_cnode_n_def) apply (clarsimp simp: the_nat_to_bl_10_def the_nat_to_bl_def nat_to_bl_def) apply (clarsimp simp: empty_cnode_def dom_def) apply (rule set_eqI, clarsimp) apply (rule iffI) apply (elim disjE, insert len_bin_to_bl, simp_all)[1] apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n 10 caps1_6 proof (prove)
goal (1 subgoal):
 1. insert (the_nat_to_bl_10 318) (insert (the_nat_to_bl_10 3) (insert (the_nat_to_bl_10 2) (insert (the_nat_to_bl_10 (Suc 0)) (dom (empty_cnode 10))))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. insert [False, True, False, False, True, True, True, True, True, False] (insert [False, False, False, False, False, False, False, False, True, True] (insert [False, False, False, False, False, False, False, False, True, False] (insert [False, False, False, False, False, False, False, False, False, True] (dom (empty_cnode 10))))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. insert [False, True, False, False, True, True, True, True, True, False] (insert [False, False, False, False, False, False, False, False, True, True] (insert [False, False, False, False, False, False, False, False, True, False] (insert [False, False, False, False, False, False, False, False, False, True] {a. length a = 10}))) = {x. length x = 10} proof (prove)
goal (1 subgoal):
 1. \<And>x. (x = [False, True, False, False, True, True, True, True, True, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10) = (length x = 10) proof (prove)
goal (2 subgoals):
 1. \<And>x. x = [False, True, False, False, True, True, True, True, True, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 \<Longrightarrow> length x = 10
 2. \<And>x. length x = 10 \<Longrightarrow> x = [False, True, False, False, True, True, True, True, True, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 proof (prove)
goal (1 subgoal):
 1. \<And>x. length x = 10 \<Longrightarrow> x = [False, True, False, False, True, True, True, True, True, False] \<or> x = [False, False, False, False, False, False, False, False, True, True] \<or> x = [False, False, False, False, False, False, False, False, True, False] \<or> x = [False, False, False, False, False, False, False, False, False, True] \<or> length x = 10 proof (prove)
goal:
No subgoals!
theory ExampleSystem

lemma empty_cnode_apply[simp]:
  "(empty_cnode n xs = Some cap) = (length xs = n \<and> cap = NullCap)" by (auto simp add: empty_cnode_def)

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

lemma tcb_states_of_state_1:
  "tcb_states_of_state s1 = [0xC08 \<mapsto> thread_state.BlockedOnReceive 9 \<lparr> receiver_can_grant = False \<rparr>,  0xC07 \<mapsto> thread_state.Running ]" unfolding s1_def tcb_states_of_state_def apply (rule ext) apply (simp add: get_tcb_def) apply (simp add: kh1_def kh1_obj_def ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_states_of_state s1 = [0xC08 \<mapsto> BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, 0xC07 \<mapsto> Running] proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. map_option tcb_state (get_tcb p \<lparr>kheap = kh1, cdt = \<lambda>x. None, is_original_cap = undefined, cur_thread = undefined, idle_thread = undefined, machine_state = undefined, interrupt_irq_node = \<lambda>_. 0xA, interrupt_states = undefined, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = undefined, arm_next_asid = undefined, arm_asid_map = undefined, arm_global_pd = undefined, arm_global_pts = undefined, arm_kernel_vspace = undefined\<rparr>, exst = exst1\<rparr>)) = [0xC08 \<mapsto> BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, 0xC07 \<mapsto> Running] proof (prove)
goal (1 subgoal):
 1. \<And>p. map_option tcb_state (get_tcb p \<lparr>kheap = kh1, cdt = \<lambda>x. None, is_original_cap = undefined, cur_thread = undefined, idle_thread = undefined, machine_state = undefined, interrupt_irq_node = \<lambda>_. 0xA, interrupt_states = undefined, arch_state = \<lparr>arm_asid_table = \<lambda>x. None, arm_hwasid_table = undefined, arm_next_asid = undefined, arm_asid_map = undefined, arm_global_pd = undefined, arm_global_pts = undefined, arm_kernel_vspace = undefined\<rparr>, exst = exst1\<rparr>) = [0xC08 \<mapsto> BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>, 0xC07 \<mapsto> Running] p proof (prove)
goal (1 subgoal):
 1. \<And>p. (p = 0xC08 \<longrightarrow> (\<exists>z. (case kh1 0xC08 of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) = Some z \<and> tcb_state z = BlockedOnReceive 9 \<lparr>receiver_can_grant = False\<rparr>)) \<and> (p \<noteq> 0xC08 \<longrightarrow> (p = 0xC07 \<longrightarrow> (\<exists>z. (case kh1 0xC07 of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) = Some z \<and> tcb_state z = Running)) \<and> (p \<noteq> 0xC07 \<longrightarrow> (case kh1 p of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) = None)) proof (prove)
goal:
No subgoals!