theory ADT_C

lemma (in kernel_m) cstate_to_H_correct:
  assumes valid: "valid_state' as"
  assumes cstate_rel: "cstate_relation as cs"
  shows "cstate_to_H cs = as \<lparr>ksMachineState:=  observable_memory (ksMachineState as) (user_mem' as)\<rparr>" apply (subgoal_tac "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)") apply (rule kernel_state.equality, simp_all add: cstate_to_H_def) apply (rule cstate_to_pspace_H_correct) using valid apply (simp add: valid_state'_def) using cstate_rel valid apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def
                      observable_memory_def valid_state'_def
                      valid_pspace'_def) using cstate_rel apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def prod_eq_iff) using cstate_rel apply (clarsimp simp: cstate_relation_def cpspace_relation_def  Let_def prod_eq_iff) using valid cstate_rel apply (rule mk_gsUntypedZeroRanges_correct) using cstate_rel apply (fastforce simp: cstate_relation_def cpspace_relation_def
                  Let_def ghost_size_rel_def unat_eq_0
                            split: if_split) using valid cstate_rel apply (rule cDomScheduleIdx_to_H_correct) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using valid cstate_rel apply (rule cDomSchedule_to_H_correct) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def ucast_up_ucast_id is_up_8_32) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) apply (rule cready_queues_to_H_correct) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) apply (rule cbitmap_L1_to_H_correct) apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) apply (rule cbitmap_L2_to_H_correct) apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) apply (rule csch_act_rel_to_H[THEN iffD1]) apply (case_tac "ksSchedulerAction as", simp+) using valid apply (clarsimp simp: valid_state'_def st_tcb_at'_def
                             obj_at'_real_def ko_wp_at'_def objBitsKO_def projectKO_opt_tcb
                       split: kernel_object.splits) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) apply (rule cint_rel_to_H) using valid apply (simp add: valid_state'_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) apply (rule carch_state_to_H_correct) using valid apply (simp add: valid_state'_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def carch_state_relation_def carch_globals_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def carch_state_relation_def carch_globals_def) apply (rule cstate_to_machine_H_correct[simplified]) using valid apply (simp add: valid_state'_def) using cstate_rel apply (simp add: cstate_relation_def Let_def) using cstate_rel apply (simp add: cstate_relation_def Let_def cpspace_relation_def) using cstate_rel apply (simp add: cstate_relation_def Let_def cpspace_relation_def) using valid apply (clarsimp simp add: valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cstate_to_H cs = as\<lparr>ksMachineState := observable_memory (ksMachineState as) (user_mem' as)\<rparr> proof (prove)
goal (2 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cstate_to_H cs = as\<lparr>ksMachineState := observable_memory (ksMachineState as) (user_mem' as)\<rparr>
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (19 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cstate_to_pspace_H cs = ksPSpace as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (ghost'state_' cs) = gsUserPages as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (snd (ghost'state_' cs)) = gsCNodes as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
A total of 19 subgoals... proof (prove)
goal (20 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> valid_pspace' as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cpspace_relation (ksPSpace as) (underlying_memory (cstate_to_machine_H cs)) (t_hrs_' cs)
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (ghost'state_' cs) = gsUserPages as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (snd (ghost'state_' cs)) = gsCNodes as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
A total of 20 subgoals... proof (prove)
using this:
valid_state' as

goal (20 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> valid_pspace' as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cpspace_relation (ksPSpace as) (underlying_memory (cstate_to_machine_H cs)) (t_hrs_' cs)
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (ghost'state_' cs) = gsUserPages as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (snd (ghost'state_' cs)) = gsCNodes as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
A total of 20 subgoals... proof (prove)
goal (19 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cpspace_relation (ksPSpace as) (underlying_memory (cstate_to_machine_H cs)) (t_hrs_' cs)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (ghost'state_' cs) = gsUserPages as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (snd (ghost'state_' cs)) = gsCNodes as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
A total of 19 subgoals... proof (prove)
using this:
cstate_relation as cs
valid_state' as

goal (19 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cpspace_relation (ksPSpace as) (underlying_memory (cstate_to_machine_H cs)) (t_hrs_' cs)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (ghost'state_' cs) = gsUserPages as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (snd (ghost'state_' cs)) = gsCNodes as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
A total of 19 subgoals... proof (prove)
goal (18 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (ghost'state_' cs) = gsUserPages as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (snd (ghost'state_' cs)) = gsCNodes as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
A total of 18 subgoals... proof (prove)
using this:
cstate_relation as cs

goal (18 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (ghost'state_' cs) = gsUserPages as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (snd (ghost'state_' cs)) = gsCNodes as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (snd (ghost'state_' cs)) = gsCNodes as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
A total of 17 subgoals... proof (prove)
using this:
cstate_relation as cs

goal (17 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> fst (snd (ghost'state_' cs)) = gsCNodes as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
A total of 16 subgoals... proof (prove)
using this:
valid_state' as
cstate_relation as cs

goal (16 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> mk_gsUntypedZeroRanges cs = gsUntypedZeroRanges as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
A total of 15 subgoals... proof (prove)
using this:
cstate_relation as cs

goal (15 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> (let v = unat (gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' cs)) in if v = 0 then CARD(32 word) else v) = gsMaxObjectSize as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
A total of 14 subgoals... proof (prove)
using this:
valid_state' as
cstate_relation as cs

goal (14 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
A total of 14 subgoals... proof (prove)
using this:
cstate_relation as cs

goal (14 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
A total of 13 subgoals... proof (prove)
using this:
valid_state' as
cstate_relation as cs

goal (13 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
A total of 13 subgoals... proof (prove)
using this:
cstate_relation as cs

goal (13 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
A total of 12 subgoals... proof (prove)
using this:
cstate_relation as cs

goal (12 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> UCAST(32 \<rightarrow> 8) (ksCurDomain_' cs) = ksCurDomain as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
A total of 11 subgoals... proof (prove)
using this:
cstate_relation as cs

goal (11 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksDomainTime_' cs = ksDomainTime as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_to_H (clift (t_hrs_' cs)) (ksReadyQueues_' cs) = ksReadyQueues as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (10 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (10 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 10. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (9 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (9 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (9 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (9 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (9 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' cs) = ksReadyQueuesL1Bitmap as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (9 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 9. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (8 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (8 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (8 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' cs) = ksReadyQueuesL2Bitmap as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (8 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 8. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (7 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (7 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksCurThread_' cs) = ksCurThread as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 7. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (6 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (6 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (ksIdleThread_' cs) = ksIdleThread as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (5 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (5 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cscheduler_action_to_H (ksSchedulerAction_' cs) = ksSchedulerAction as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> \<forall>t. ksSchedulerAction as = SwitchToThread t \<longrightarrow> is_aligned t tcbBlockSizeBits
 2. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs)
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (6 subgoals):
 1. \<And>x3. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (SwitchToThread x3) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; ksSchedulerAction as = SwitchToThread x3\<rbrakk> \<Longrightarrow> is_aligned x3 tcbBlockSizeBits
 2. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs)
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
valid_state' as

goal (6 subgoals):
 1. \<And>x3. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (SwitchToThread x3) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; ksSchedulerAction as = SwitchToThread x3\<rbrakk> \<Longrightarrow> is_aligned x3 tcbBlockSizeBits
 2. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs)
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 6. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (5 subgoals):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); carch_state_relation (ksArchState as) cs; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (4 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cint_state_to_H intStateIRQNode_array_Ptr (intStateIRQTable_' cs) = ksInterruptState as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (5 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> irqs_masked' as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs)
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
valid_state' as

goal (5 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> irqs_masked' as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs)
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 5. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (4 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (4 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs)
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (3 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (3 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (2 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_to_H cs = ksArchState as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (4 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> valid_arch_state' as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_relation (ksArchState as) cs
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
valid_state' as

goal (4 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> valid_arch_state' as
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_relation (ksArchState as) cs
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']
 4. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (3 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_relation (ksArchState as) cs
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (3 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> carch_state_relation (ksArchState as) cs
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']
 3. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (2 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (2 subgoals):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) \<Longrightarrow> armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']
 2. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (1 subgoal):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
using this:
cstate_relation as cs

goal (1 subgoal):
 1. cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> valid_machine_state' as
 2. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState as) cs
 3. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)
 4. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
using this:
valid_state' as

goal (4 subgoals):
 1. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> valid_machine_state' as
 2. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState as) cs
 3. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)
 4. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState as) cs
 2. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)
 3. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
using this:
cstate_relation as cs

goal (3 subgoals):
 1. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cmachine_state_relation (ksMachineState as) cs
 2. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)
 3. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)
 2. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
using this:
cstate_relation as cs

goal (2 subgoals):
 1. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs)
 2. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
using this:
cstate_relation as cs

goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of as) (clift (t_hrs_' cs)) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (ksPSpace as) (t_hrs_' cs) \<and> cmap_relation (map_to_eps (ksPSpace as)) (clift (t_hrs_' cs)) ep_Ptr (cendpoint_relation (clift (t_hrs_' cs))) \<and> cmap_relation (map_to_ntfns (ksPSpace as)) (clift (t_hrs_' cs)) ntfn_Ptr (cnotification_relation (clift (t_hrs_' cs))) \<and> cmap_relation (map_to_pdes (ksPSpace as)) (clift (t_hrs_' cs)) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace as)) (clift (t_hrs_' cs)) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace as)) (clift (t_hrs_' cs)) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs) \<and> cpspace_device_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs) \<and> cpspace_pde_array_relation (ksPSpace as) (t_hrs_' cs) \<and> cpspace_pte_array_relation (ksPSpace as) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; state_rel.cstate_relation symbol_table domain (armKSKernelVSpace (ksArchState as)) as cs\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
using this:
valid_state' as

goal (1 subgoal):
 1. \<lbrakk>cmap_relation (ctes_of as) (clift (t_hrs_' cs)) cte_Ptr ccte_relation \<and> cpspace_tcb_relation (ksPSpace as) (t_hrs_' cs) \<and> cmap_relation (map_to_eps (ksPSpace as)) (clift (t_hrs_' cs)) ep_Ptr (cendpoint_relation (clift (t_hrs_' cs))) \<and> cmap_relation (map_to_ntfns (ksPSpace as)) (clift (t_hrs_' cs)) ntfn_Ptr (cnotification_relation (clift (t_hrs_' cs))) \<and> cmap_relation (map_to_pdes (ksPSpace as)) (clift (t_hrs_' cs)) pde_Ptr cpde_relation \<and> cmap_relation (map_to_ptes (ksPSpace as)) (clift (t_hrs_' cs)) pte_Ptr cpte_relation \<and> cmap_relation (map_to_asidpools (ksPSpace as)) (clift (t_hrs_' cs)) ap_Ptr casid_pool_relation \<and> cpspace_user_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs) \<and> cpspace_device_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs) \<and> cpspace_pde_array_relation (ksPSpace as) (t_hrs_' cs) \<and> cpspace_pte_array_relation (ksPSpace as) (t_hrs_' cs); cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); armKSNextASID_' cs = armKSNextASID (ksArchState as); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState as); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState as)) (armKSHWASIDTable_' cs); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState as)) (armKSASIDTable_' cs); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState as)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cs) \<circ>\<^sub>m pd_pointer_to_asid_slot); armKSGlobalPD (ksArchState as) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState as) = [symbol_table ''armKSGlobalPT'']; cmachine_state_relation (ksMachineState as) cs; cte_array_relation as cs; tcb_cte_array_relation as cs; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' cs)); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule as) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; state_rel.cstate_relation symbol_table domain (armKSKernelVSpace (ksArchState as)) as cs\<rbrakk> \<Longrightarrow> pspace_distinct' as proof (prove)
goal:
No subgoals!