diff --git a/proof/invariant-abstract/ARM/ArchArch_AI.thy b/proof/invariant-abstract/ARM/ArchArch_AI.thy index f09367a9a4..89132a5352 100644 --- a/proof/invariant-abstract/ARM/ArchArch_AI.thy +++ b/proof/invariant-abstract/ARM/ArchArch_AI.thy @@ -1524,13 +1524,4 @@ lemma arch_pinv_ct_active: end -context begin interpretation Arch . - -requalify_facts - arch_pinv_ct_active - -end - -declare arch_pinv_ct_active[wp] - end diff --git a/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy index 1dd8860cd6..1ab432c4d3 100644 --- a/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy @@ -39,8 +39,9 @@ lemma copy_global_mappings_valid_sched_pred[wp]: by (wpsimp simp: copy_global_mappings_def store_pde_def wp: mapM_x_wp_inv) lemma init_arch_objects_valid_sched_pred[wp, DetSchedAux_AI_assms]: - "init_arch_objects new_type ptr num_objects obj_sz refs \valid_sched_pred_strong P\" - by (wpsimp simp: init_arch_objects_def wp: dmo_valid_sched_pred mapM_x_wp_inv) + "init_arch_objects new_type dev ptr num_objects obj_sz refs \valid_sched_pred_strong P\" + unfolding init_arch_objects_def + by (wpsimp wp: dmo_valid_sched_pred mapM_x_wp_inv) crunch init_arch_objects for exst[wp]: "\s. P (exst s)" @@ -134,12 +135,12 @@ global_interpretation DetSchedAux_AI?: DetSchedAux_AI case 1 show ?case by (unfold_locales; (fact DetSchedAux_AI_assms)?) qed -context Arch begin global_naming ARM +context Arch begin arch_global_naming (* FIXME: move? *) lemma init_arch_objects_obj_at_impossible: "\ao. \ P (ArchObj ao) \ - \\s. Q (obj_at P p s)\ init_arch_objects a b c d e \\rv s. Q (obj_at P p s)\" + \\s. Q (obj_at P p s)\ init_arch_objects a b c d e f \\rv s. Q (obj_at P p s)\" by (auto intro: init_arch_objects_obj_at_non_pd) lemma perform_asid_control_etcb_at: diff --git a/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy b/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy index 43e9b4b497..f81abe088e 100644 --- a/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy @@ -114,9 +114,9 @@ named_theorems machine_ops_last_machine_time' named_theorems arch_machine_ops_last_machine_time' \ \crunch these separately so they don't appear in machine_ops_last_machine_time\ -crunch cleanByVA_PoU, cleanCacheRange_PoU +crunch cleanByVA_PoU, cleanCacheRange_PoU, cleanCacheRange_RAM for machine_times[wp, arch_machine_ops_last_machine_time']: "\ms. P (last_machine_time ms) (time_state ms)" - (wp: crunch_wps simp: crunch_simps ignore_del: cleanByVA_PoU) + (wp: crunch_wps simp: crunch_simps ignore_del: cleanByVA_PoU cleanL2Range cleanByVA) crunch storeWord, clearMemory, freeMemory, ackDeadlineIRQ, ackInterrupt, maskInterrupt, setDeadline for machine_times[wp, machine_ops_last_machine_time']: "\ms. P (last_machine_time ms) (time_state ms)" diff --git a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy index ce7db438c9..22a09ebe32 100644 --- a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy @@ -228,12 +228,12 @@ lemma sts_arch_irq_control_inv_valid[wp, Interrupt_AI_assms]: done crunch invoke_irq_control - for cur_thread[wp, Interrupt_AI_asms]: "\s. P (cur_thread s)" - and ct_in_state[wp, Interrupt_AI_asms]: "ct_in_state P" + for cur_thread[wp, Interrupt_AI_assms]: "\s. P (cur_thread s)" + and ct_in_state[wp, Interrupt_AI_assms]: "ct_in_state P" (wp: crunch_wps simp: crunch_simps) crunch invoke_irq_handler - for ct_active[wp, Interrupt_AI_asms]: "ct_active" + for ct_active[wp, Interrupt_AI_assms]: "ct_active" (wp: gts_wp get_simple_ko_wp crunch_wps simp: crunch_simps) end diff --git a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy index eb612626e3..4a40f517d4 100644 --- a/proof/invariant-abstract/ARM/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/ARM/ArchSchedule_AI.thy @@ -66,7 +66,7 @@ lemma arch_stit_invs[wp, Schedule_AI_assms]: "\invs\ arch_switch_to_idle_thread \\r. invs\" by (wpsimp wp: svr_invs simp: arch_switch_to_idle_thread_def) -lemma arch_stit_tcb_at[wp, Schedule_AI_asms]: +lemma arch_stit_tcb_at[wp, Schedule_AI_assms]: "\tcb_at t\ arch_switch_to_idle_thread \\r. tcb_at t\" apply (simp add: arch_switch_to_idle_thread_def ) apply wp @@ -78,7 +78,7 @@ crunch set_vm_root and scheduler_action[wp]: "\s. P (scheduler_action s)" (simp: crunch_simps) -lemma arch_stit_sc_at[wp, Schedule_AI_asms]: +lemma arch_stit_sc_at[wp, Schedule_AI_assms]: "arch_switch_to_idle_thread \sc_at sc_ptr\" apply (simp add: arch_switch_to_idle_thread_def) apply wp diff --git a/proof/invariant-abstract/ARM/ArchTcb_AI.thy b/proof/invariant-abstract/ARM/ArchTcb_AI.thy index ed8e495d35..e48136dca7 100644 --- a/proof/invariant-abstract/ARM/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM/ArchTcb_AI.thy @@ -382,7 +382,7 @@ lemma install_tcb_cap_sc_tcb_sc_at[wp]: apply (wpsimp wp: check_cap_inv cap_delete_fh_lift hoare_vcg_if_lift2 | simp)+ done -lemma tcs_invs[Tcb_AI_asms]: +lemma tcs_invs[Tcb_AI_assms]: "\invs and tcb_inv_wf (ThreadControlSched t sl fh mcp pr sc)\ invoke_tcb (ThreadControlSched t sl fh mcp pr sc) \\rv. invs\" @@ -516,12 +516,6 @@ crunch invoke_tcb end -context begin interpretation Arch . - -requalify_facts install_tcb_cap_invs is_cnode_or_valid_arch_is_cap_simps - -end - global_interpretation Tcb_AI?: Tcb_AI where is_cnode_or_valid_arch = ARM.is_cnode_or_valid_arch proof goal_cases diff --git a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy index f0402534e4..43568a58b6 100644 --- a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy @@ -609,9 +609,9 @@ qed lemma init_arch_objects_obj_at_other[Untyped_AI_assms]: "\\ptr\set ptrs. is_aligned ptr (obj_bits_api ty us); p \ set ptrs\ - \ init_arch_objects ty ptr n us ptrs \\s. N (obj_at P p s)\" - by (wpsimp simp: init_arch_objects_def obj_bits_api_def default_arch_object_def - pd_bits_def pageBits_def + \ init_arch_objects ty dev ptr n us ptrs \\s. N (obj_at P p s)\" + unfolding init_arch_objects_def + by (wpsimp simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def wp: mapM_x_wp' copy_global_mappings_obj_at_other) lemma copy_global_mappings_obj_at_non_pd: @@ -628,10 +628,9 @@ lemma copy_global_mappings_obj_at_non_pd: lemma init_arch_objects_obj_at_non_pd: assumes non_pd: "\ko. P ko \ (\pd. ko \ ArchObj (PageDirectory pd))" - shows "init_arch_objects ty ptr n us ptrs \\s. N (obj_at P p s)\" - by (wpsimp simp: init_arch_objects_def obj_bits_api_def default_arch_object_def - pd_bits_def pageBits_def - wp: mapM_x_wp' copy_global_mappings_obj_at_non_pd[OF non_pd]) + shows "init_arch_objects ty dev ptr n us ptrs \\s. N (obj_at P p s)\" + unfolding init_arch_objects_def + by (wpsimp wp: mapM_x_wp' copy_global_mappings_obj_at_non_pd[OF non_pd]) lemma non_arch_non_pd: "\ko. P ko \ non_arch_obj ko \ \ko. P ko \ (\pd. ko \ ArchObj (PageDirectory pd))" diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index 58bcd5a84d..419c0be924 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -15,10 +15,6 @@ begin arch_requalify_consts irq_state_update irq_state - time_state_update - time_state - last_machine_time_update - last_machine_time final_matters_arch ups_of_heap diff --git a/proof/invariant-abstract/DetSchedAux_AI.thy b/proof/invariant-abstract/DetSchedAux_AI.thy index 547980acdf..cdb7a7cab0 100644 --- a/proof/invariant-abstract/DetSchedAux_AI.thy +++ b/proof/invariant-abstract/DetSchedAux_AI.thy @@ -8,14 +8,11 @@ theory DetSchedAux_AI imports DetSchedInvs_AI begin -context begin interpretation Arch . -requalify_facts - invoke_untyped_pred_tcb_at +arch_requalify_facts init_arch_objects_typ_at init_arch_objects_pred_tcb_at init_arch_objects_cur_thread hyp_live_default_object -end lemmas [wp] = init_arch_objects_typ_at @@ -73,11 +70,11 @@ global_interpretation cap_insert: valid_sched_pred_locale _ "cap_insert new_cap locale DetSchedAux_AI = fixes state_ext_t :: "'state_ext::state_ext itself" assumes init_arch_objects_valid_idle[wp]: - "\t p n s r. init_arch_objects t p n s r \\s::'state_ext state. valid_idle s\" + "\t d p n s r. init_arch_objects t d p n s r \\s::'state_ext state. valid_idle s\" assumes init_arch_objects_valid_sched_pred[wp]: - "\t p n s r P. init_arch_objects t p n s r \valid_sched_pred_strong P::'state_ext state \ _\" + "\t d p n s r P. init_arch_objects t d p n s r \valid_sched_pred_strong P::'state_ext state \ _\" assumes init_arch_object_valid_machine_time[wp]: - "\t p n s r. init_arch_objects t p n s r \valid_machine_time ::'state_ext state \ _\" + "\t d p n s r. init_arch_objects t d p n s r \valid_machine_time ::'state_ext state \ _\" assumes update_time_stamp_valid_machine_time[wp]: "update_time_stamp \valid_machine_time::'state_ext state \ _\" assumes dmo_getCurrentTime_vmt_sp: @@ -89,7 +86,7 @@ lemmas mapM_x_defsym = mapM_x_def[symmetric] context DetSchedAux_AI begin -sublocale init_arch_objects: valid_sched_pred_locale _ "init_arch_objects t p n s r" +sublocale init_arch_objects: valid_sched_pred_locale _ "init_arch_objects t d p n s r" by unfold_locales (rule init_arch_objects_valid_sched_pred) crunch delete_objects @@ -113,7 +110,7 @@ crunch invoke_untyped end lemma init_arch_objects_tcb_heap[wp]: - "init_arch_objects t p n s r \\s. P (tcbs_of s)\" + "init_arch_objects t d p n s r \\s. P (tcbs_of s)\" apply (rule pred_map_heap_lift[where heap=tcbs_of and P=P and R=\, simplified]) apply (rule rsubst[where P="\t. _ \t\", OF _ ext], rename_tac ref) apply (rule_tac N=N and P="\ko. \tcb. ko = TCB tcb \ P tcb" and p=ref in init_arch_objects_obj_at_non_arch) @@ -122,7 +119,7 @@ lemma init_arch_objects_tcb_heap[wp]: by (auto simp: obj_at_kh_kheap_simps pred_map_simps vs_heap_simps) lemma init_arch_objects_sc_heap[wp]: - "init_arch_objects t p n s r \\s. P (scs_of s)\" + "init_arch_objects t d p n s r \\s. P (scs_of s)\" apply (rule pred_map_heap_lift[where heap=scs_of and P=P and R=\, simplified]) apply (rule rsubst[where P="\t. _ \t\", OF _ ext], rename_tac ref) apply (rule_tac N=N and P="\ko. \sc n. ko = SchedContext sc n \ P sc" and p=ref in init_arch_objects_obj_at_non_arch) diff --git a/proof/invariant-abstract/DetSchedInvs_AI.thy b/proof/invariant-abstract/DetSchedInvs_AI.thy index c4bcdb477b..f6e6d0b15b 100644 --- a/proof/invariant-abstract/DetSchedInvs_AI.thy +++ b/proof/invariant-abstract/DetSchedInvs_AI.thy @@ -8,11 +8,9 @@ theory DetSchedInvs_AI imports ArchDeterministic_AI begin -context begin interpretation Arch . -requalify_facts +arch_requalify_facts machine_op_lift_machine_times machine_ops_last_machine_time -end lemmas [wp] = machine_op_lift_machine_times diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 79f069d9ae..2eaf948e64 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -8,26 +8,21 @@ theory DetSchedSchedule_AI imports ArchDetSchedDomainTime_AI begin -context begin interpretation Arch . - -requalify_consts +arch_requalify_consts time_oracle -requalify_facts +arch_requalify_facts kernelWCET_us_non_zero kernelWCET_ticks_non_zero - do_ipc_transfer_cur_thread - machine_ops_last_machine_time - handle_arch_fault_reply_typ_at getCurrentTime_def install_tcb_cap_sc_tcb_sc_at - -end + set_simple_ko_ioports lemmas [wp] = do_ipc_transfer_cur_thread handle_arch_fault_reply_typ_at machine_ops_last_machine_time + set_simple_ko_ioports (* FIXME RT: move and rename *) lemma hoare_drop_assertion: @@ -22891,7 +22886,7 @@ lemma update_waiting_ntfn_cur_sc_in_release_q_imp_zero_consumed: \\_. cur_sc_in_release_q_imp_zero_consumed\" supply if_split[split del] if_cong[cong] apply (clarsimp simp: update_waiting_ntfn_def) - apply (wpsimp wp: set_thread_state_invs set_ntfn_minor_invs Arch.set_simple_ko_ioports + apply (wpsimp wp: set_thread_state_invs set_ntfn_minor_invs maybe_donate_sc_cur_sc_in_release_q_imp_zero_consumed refill_unblock_check_active_scs_valid maybeM_inv simp: invs_def valid_state_def valid_pspace_def) diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index a30a4e9b7b..985b81689d 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -30,7 +30,6 @@ arch_requalify_consts arch_requalify_facts no_irq_clearMemory final_cap_lift - valid_global_refsD arch_post_cap_deletion_valid_objs arch_post_cap_deletion_cte_wp_at arch_post_cap_deletion_caps_of_state diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy index 97c97250cc..9f04e347f6 100644 --- a/proof/invariant-abstract/Invariants_AI.thy +++ b/proof/invariant-abstract/Invariants_AI.thy @@ -22,6 +22,7 @@ arch_requalify_facts (A) tcb_bits_def endpoint_bits_def ntfn_bits_def + reply_bits_def arch_requalify_consts not_kernel_window @@ -53,7 +54,9 @@ arch_requalify_consts valid_global_vspace_mappings pspace_in_kernel_window + last_machine_time_update last_machine_time + time_state_update time_state valid_vs_lookup diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index 2302df1fdb..d012d54109 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -9,7 +9,6 @@ imports ArchSchedule_AI begin arch_requalify_facts - arch_stit_invs arch_post_cap_deletion_pred_tcb_at arch_post_cap_deletion_cur_thread as_user_hyp_refs_of diff --git a/proof/invariant-abstract/IpcDet_AI.thy b/proof/invariant-abstract/IpcDet_AI.thy index 995af624df..22a236a90e 100644 --- a/proof/invariant-abstract/IpcDet_AI.thy +++ b/proof/invariant-abstract/IpcDet_AI.thy @@ -10,17 +10,9 @@ imports "./$L4V_ARCH/ArchIpc_AI" begin -context begin interpretation Arch . - -requalify_consts - make_arch_fault_msg - -requalify_facts - make_arch_fault_msg_invs +arch_requalify_facts make_arch_fault_msg_valid_replies -end - lemma replies_with_sc_kh_update_sc: "sc_replies (f sc v) = sc_replies sc \ replies_with_sc (s\kheap := (kheap s)(p \ SchedContext (f sc v) n)\) diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index 0f121e1d5f..47f067d43e 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -12,19 +12,16 @@ begin arch_requalify_consts in_device_frame + arch_requalify_facts set_mrs_ioports - as_user_ioports set_message_info_ioports copy_mrs_ioports store_word_offs_ioports make_arch_fault_msg_ioports arch_derive_cap_notzombie arch_derive_cap_notIRQ - lookup_ipc_buffer_inv set_mi_invs - as_user_hyp_refs_of - valid_arch_arch_tcb_set_registers declare set_mi_invs[wp] diff --git a/proof/invariant-abstract/RISCV64/ArchArch_AI.thy b/proof/invariant-abstract/RISCV64/ArchArch_AI.thy index ab037413ed..2ad047b514 100644 --- a/proof/invariant-abstract/RISCV64/ArchArch_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchArch_AI.thy @@ -1346,14 +1346,4 @@ lemma arch_pinv_ct_active: end - -context begin interpretation Arch . - -requalify_facts - arch_pinv_ct_active - -end - -lemmas [wp] = arch_pinv_ct_active - end diff --git a/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy index 8e6e14cca5..68bea77d3d 100644 --- a/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchDetSchedAux_AI.thy @@ -33,7 +33,7 @@ lemma copy_global_mappings_valid_sched_pred[wp]: by (wpsimp simp: copy_global_mappings_def store_pte_def wp: mapM_x_wp_inv) lemma init_arch_objects_valid_sched_pred[wp, DetSchedAux_AI_assms]: - "init_arch_objects new_type ptr num_objects obj_sz refs \valid_sched_pred_strong P\" + "init_arch_objects new_type dev ptr num_objects obj_sz refs \valid_sched_pred_strong P\" by (wpsimp simp: init_arch_objects_def wp: dmo_valid_sched_pred mapM_x_wp_inv) crunch init_arch_objects @@ -127,12 +127,12 @@ proof goal_cases case 1 show ?case by (unfold_locales; (fact DetSchedAux_AI_assms)?) qed -context Arch begin global_naming RISCV64 +context Arch begin arch_global_naming (* FIXME: move? *) lemma init_arch_objects_obj_at_impossible: "\ao. \ P (ArchObj ao) \ - \\s. Q (obj_at P p s)\ init_arch_objects a b c d e \\rv s. Q (obj_at P p s)\" + \\s. Q (obj_at P p s)\ init_arch_objects a b c d e f \\rv s. Q (obj_at P p s)\" by (auto intro: init_arch_objects_obj_at_non_pt) lemma perform_asid_control_etcb_at: diff --git a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy index f13d5fe73f..7de95b9c34 100644 --- a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy @@ -291,7 +291,7 @@ lemma length_and_unat_of_bl_length: lemmas unbind_from_sc_final_cap[wp] = final_cap_lift [OF unbind_from_sc_caps_of_state] -lemma (* finalise_cap_cases1 *)[Finalise_AI_asms]: +lemma (* finalise_cap_cases1 *)[Finalise_AI_assms]: "\\s. final \ is_final_cap' cap s \ cte_wp_at ((=) cap) slot s\ finalise_cap cap final diff --git a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy index a2272185e9..578b856ac1 100644 --- a/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy @@ -264,12 +264,12 @@ crunch arch_invoke_irq_handler for typ_at[wp]: "\s. P (typ_at T p s)" crunch invoke_irq_control - for cur_thread[wp, Interrupt_AI_asms]: "\s. P (cur_thread s)" - and ct_in_state[wp, Interrupt_AI_asms]: "ct_in_state P" + for cur_thread[wp, Interrupt_AI_assms]: "\s. P (cur_thread s)" + and ct_in_state[wp, Interrupt_AI_assms]: "ct_in_state P" (wp: crunch_wps simp: crunch_simps) crunch invoke_irq_handler - for ct_active[wp, Interrupt_AI_asms]: "ct_active" + for ct_active[wp, Interrupt_AI_assms]: "ct_active" (wp: gts_wp get_simple_ko_wp crunch_wps simp: crunch_simps) end diff --git a/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy b/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy index 33c882a67b..3ae4776efb 100644 --- a/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchSchedule_AI.thy @@ -48,7 +48,7 @@ lemma arch_stt_sc_at[wp,Schedule_AI_assms]: apply wp done -lemma arch_stt_runnable[Schedule_AI_asms]: +lemma arch_stt_runnable[Schedule_AI_assms]: "\st_tcb_at Q t\ arch_switch_to_thread t \\r . st_tcb_at Q t\" apply (simp add: arch_switch_to_thread_def) apply wp @@ -58,13 +58,13 @@ lemma arch_stit_invs[wp, Schedule_AI_assms]: "\invs\ arch_switch_to_idle_thread \\r. invs\" by (wpsimp simp: arch_switch_to_idle_thread_def) -lemma arch_stit_tcb_at[wp, Schedule_AI_asms]: +lemma arch_stit_tcb_at[wp, Schedule_AI_assms]: "\tcb_at t\ arch_switch_to_idle_thread \\r. tcb_at t\" apply (simp add: arch_switch_to_idle_thread_def ) apply (wp tcb_at_typ_at) done -lemma arch_stit_sc_at[wp, Schedule_AI_asms]: +lemma arch_stit_sc_at[wp, Schedule_AI_assms]: "arch_switch_to_idle_thread \sc_at sc_ptr\" apply (simp add: arch_switch_to_idle_thread_def) apply wp diff --git a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy index c302f26348..e29c0a0e84 100644 --- a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy @@ -262,7 +262,7 @@ lemma install_tcb_cap_invs: elim!: cte_wp_at_weakenE) done -lemma install_tcb_cap_no_cap_to_obj_dr_emp[wp, Tcb_AI_asms]: +lemma install_tcb_cap_no_cap_to_obj_dr_emp[wp, Tcb_AI_assms]: "\no_cap_to_obj_dr_emp cap and (\s. \new_cap src_slot. slot_opt = Some (new_cap, src_slot) \ no_cap_to_obj_dr_emp new_cap s)\ @@ -309,7 +309,7 @@ lemma install_tcb_frame_cap_invs: | wp cap_delete_ep)+)[1] by (clarsimp simp: is_cap_simps' valid_fault_handler_def is_cnode_or_valid_arch_def) -lemma tcc_invs[Tcb_AI_asms]: +lemma tcc_invs[Tcb_AI_assms]: "\invs and tcb_inv_wf (ThreadControlCaps t sl fh th croot vroot buf)\ invoke_tcb (ThreadControlCaps t sl fh th croot vroot buf) \\rv. invs\" @@ -372,7 +372,7 @@ lemma install_tcb_cap_sc_tcb_sc_at[wp]: apply (wpsimp wp: check_cap_inv cap_delete_fh_lift hoare_vcg_if_lift2 | simp)+ done -lemma tcs_invs[Tcb_AI_asms]: +lemma tcs_invs[Tcb_AI_assms]: "\invs and tcb_inv_wf (ThreadControlSched t sl fh mcp pr sc)\ invoke_tcb (ThreadControlSched t sl fh mcp pr sc) \\rv. invs\" @@ -506,10 +506,6 @@ crunch invoke_tcb end -context begin interpretation Arch . -requalify_facts install_tcb_cap_invs is_cnode_or_valid_arch_is_cap_simps -end - global_interpretation Tcb_AI?: Tcb_AI where is_cnode_or_valid_arch = RISCV64.is_cnode_or_valid_arch proof goal_cases diff --git a/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy b/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy index d42517e81b..ca0d9a3b6a 100644 --- a/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy @@ -387,7 +387,7 @@ qed lemma init_arch_objects_obj_at_other[Untyped_AI_assms]: "\\ptr\set ptrs. is_aligned ptr (obj_bits_api ty us); p \ set ptrs\ - \ init_arch_objects ty ptr n us ptrs \\s. N (obj_at P p s)\" + \ init_arch_objects ty dev ptr n us ptrs \\s. N (obj_at P p s)\" by (wpsimp simp: init_arch_objects_def obj_bits_api_def default_arch_object_def wp: mapM_x_wp' copy_global_mappings_obj_at_other) @@ -405,7 +405,7 @@ lemma copy_global_mappings_obj_at_non_pt: lemma init_arch_objects_obj_at_non_pt: assumes non_pt: "\ko. P ko \ (\pd. ko \ ArchObj (PageTable pd))" - shows "init_arch_objects ty ptr n us ptrs \\s. N (obj_at P p s)\" + shows "init_arch_objects ty dev ptr n us ptrs \\s. N (obj_at P p s)\" by (wpsimp simp: init_arch_objects_def obj_bits_api_def default_arch_object_def wp: mapM_x_wp' copy_global_mappings_obj_at_non_pt[OF non_pt]) diff --git a/proof/invariant-abstract/SchedContext_AI.thy b/proof/invariant-abstract/SchedContext_AI.thy index 159d0c9452..2f024c9a3c 100644 --- a/proof/invariant-abstract/SchedContext_AI.thy +++ b/proof/invariant-abstract/SchedContext_AI.thy @@ -11,13 +11,9 @@ imports begin -context begin interpretation Arch . - -requalify_facts +arch_requalify_facts valid_global_refsD -end - lemma no_cap_to_idle_sc_ptr: "\cte_wp_at ((=) (SchedContextCap a b)) slot s; invs s\ \ a \ idle_sc_ptr" by (fastforce simp: invs_def valid_state_def cap_range_def dest!: valid_global_refsD) diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index 68de0a8754..6ea3854dcb 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -26,7 +26,6 @@ arch_requalify_consts arch_requalify_facts resetTimer_device_state_inv arch_decode_invocation_inv - arch_post_cap_deletion_cur_thread arch_post_cap_deletion_state_refs_of arch_invoke_irq_handler_typ_at invoke_tcb_typ_at @@ -36,6 +35,9 @@ arch_requalify_facts arch_decode_inv_wf arch_pinv_st_tcb_at getCurrentTime_invs + install_tcb_cap_invs + is_cnode_or_valid_arch_is_cap_simps + arch_pinv_ct_active lemmas [wp] = arch_decode_invocation_inv @@ -43,6 +45,7 @@ lemmas [wp] = invoke_arch_invs arch_decode_inv_wf getCurrentTime_invs + arch_pinv_ct_active lemmas [simp] = data_to_cptr_def diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index 3d645bc99c..8dbb199051 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -294,17 +294,17 @@ locale Untyped_AI_arch = \ obj_is_device tp dev = dev" (* FIXME: not needed? *) assumes init_arch_objects_obj_at_other: - "\ptrs ty us p ptr n N P. + "\ptrs ty dev us p ptr n N P. \\ptr\set ptrs. is_aligned ptr (obj_bits_api ty us); p \ set ptrs\ - \ init_arch_objects ty ptr n us ptrs \\s::'state_ext state. N (obj_at P p s)\" + \ init_arch_objects ty dev ptr n us ptrs \\s::'state_ext state. N (obj_at P p s)\" assumes init_arch_objects_obj_at_live: - "\ptrs ty us p ptr n N P. + "\ptrs ty dev us p ptr n N P. \ko. P ko \ live ko - \ init_arch_objects ty ptr n us ptrs \\s::'state_ext state. N (obj_at P p s)\" + \ init_arch_objects ty dev ptr n us ptrs \\s::'state_ext state. N (obj_at P p s)\" assumes init_arch_objects_obj_at_non_arch: - "\ptrs ty us p ptr n N P. + "\ptrs ty dev us p ptr n N P. \ko. P ko \ non_arch_obj ko - \ init_arch_objects ty ptr n us ptrs \\s::'state_ext state. N (obj_at P p s)\" + \ init_arch_objects ty dev ptr n us ptrs \\s::'state_ext state. N (obj_at P p s)\" lemmas is_aligned_triv2 = Aligned.is_aligned_triv diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy index 5aae852725..49a4b87ffa 100644 --- a/spec/abstract/Structures_A.thy +++ b/spec/abstract/Structures_A.thy @@ -49,7 +49,7 @@ arch_requalify_consts (A) untyped_max_bits msg_label_bits -arch_requalify_facts (A) +arch_requalify_facts kernelWCET_ticks_pos2 text \ diff --git a/spec/abstract/TcbAcc_A.thy b/spec/abstract/TcbAcc_A.thy index 1254bde31d..e0de8e4a38 100644 --- a/spec/abstract/TcbAcc_A.thy +++ b/spec/abstract/TcbAcc_A.thy @@ -16,8 +16,6 @@ begin arch_requalify_consts (A) in_user_frame - as_user - msg_max_length lookup_ipc_buffer text \Store or load a word at an offset from an IPC buffer.\ diff --git a/spec/design/skel/Interrupt_H.thy b/spec/design/skel/Interrupt_H.thy index 133349bdc4..654cedefdf 100644 --- a/spec/design/skel/Interrupt_H.thy +++ b/spec/design/skel/Interrupt_H.thy @@ -39,10 +39,12 @@ requalify_consts (aliasing) end end +arch_requalify_consts + deadlineIRQ + (* override Kernel_Config const with constrained abbreviation from Hardware_H *) arch_requalify_consts (aliasing, H) maxIRQ - deadlineIRQ #INCLUDE_HASKELL_PREPARSE SEL4/Object/Structures.lhs #INCLUDE_HASKELL SEL4/Object/Interrupt.lhs bodies_only diff --git a/spec/design/skel/KernelStateData_H.thy b/spec/design/skel/KernelStateData_H.thy index 5ee0462738..7a7b8f656d 100644 --- a/spec/design/skel/KernelStateData_H.thy +++ b/spec/design/skel/KernelStateData_H.thy @@ -19,13 +19,9 @@ imports ArchStateData_H begin -context begin interpretation Arch . - -requalify_consts +arch_requalify_consts (H) usToTicks -end - requalify_types (in Arch) kernel_state diff --git a/spec/design/skel/Notification_H.thy b/spec/design/skel/Notification_H.thy index e5e152ebab..be5a7f23be 100644 --- a/spec/design/skel/Notification_H.thy +++ b/spec/design/skel/Notification_H.thy @@ -14,9 +14,6 @@ theory Notification_H imports "NotificationDecls_H" ObjectInstances_H begin -arch_requalify_consts (H) - badgeRegister - #INCLUDE_HASKELL SEL4/Object/Notification.lhs bodies_only end diff --git a/spec/design/skel/SchedContext_H.thy b/spec/design/skel/SchedContext_H.thy index 359b360d60..c1ece838a6 100644 --- a/spec/design/skel/SchedContext_H.thy +++ b/spec/design/skel/SchedContext_H.thy @@ -24,7 +24,6 @@ requalify_consts kernelWCETUs ticksToUs maxTicksToUs - getCurrentTime maxPeriodUs end diff --git a/spec/design/skel/TCB_H.thy b/spec/design/skel/TCB_H.thy index 3452f4b2a6..f72713f3de 100644 --- a/spec/design/skel/TCB_H.thy +++ b/spec/design/skel/TCB_H.thy @@ -35,7 +35,6 @@ arch_requalify_consts (aliasing, H) tlsBaseRegister maxUsToTicks timerIRQ -end abbreviation "mapMaybe \ option_map" diff --git a/spec/machine/ARM/MachineOps.thy b/spec/machine/ARM/MachineOps.thy index e1e1d3abab..955be62d06 100644 --- a/spec/machine/ARM/MachineOps.thy +++ b/spec/machine/ARM/MachineOps.thy @@ -28,7 +28,7 @@ text \ All this is done only to avoid a large number of axioms (2 for each operation). \ -context Arch begin global_naming ARM +context Arch begin arch_global_naming section "The Operations" @@ -118,11 +118,6 @@ consts' timerPrecision :: "64 word" consts' max_ticks_to_us :: "64 word" consts' max_us_to_ticks :: "64 word" -end - - -qualify ARM (in Arch) - type_synonym ticks = "64 word" type_synonym time = "64 word" @@ -136,6 +131,10 @@ text \ This matches @{text "60 * 60 * MS_IN_S * US_IN_MS"} because it shou definition MAX_PERIOD_US :: "64 word" where "MAX_PERIOD_US \ 60 * 60 * 1000 * 1000" +end + +qualify ARM (in Arch) + \ \The following notepad shows that the axioms introduced below, which provide various results about several constants and their conversion via us_to_ticks, are consistent.\ @@ -150,13 +149,13 @@ define us_to_ticks :: "64 word \ 64 word" where have kernelWCET_us_pos2: "0 < 2 * kernelWCET_us" by (simp add: kernelWCET_us_def) -have MIN_BUDGET_le_MAX_PERIOD: "2 * kernelWCET_us \ MAX_PERIOD_US" - by (simp add: kernelWCET_us_def MAX_PERIOD_US_def) +have MIN_BUDGET_le_MAX_PERIOD: "2 * kernelWCET_us \ ARM.MAX_PERIOD_US" + by (simp add: kernelWCET_us_def ARM.MAX_PERIOD_US_def) have ticks_per_timer_unit_non_zero: "ticks_per_timer_unit \ 0" by (simp add: ticks_per_timer_unit_def) -have MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < unat max_time" +have MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < unat ARM.max_time" apply (subst unat_max_word[symmetric]) apply clarsimp apply (prop_tac "unat kernelWCET_us \ 100") @@ -169,8 +168,8 @@ have MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < una done have getCurrentTime_buffer_bound: - "5 * unat MAX_PERIOD_US * unat ticks_per_timer_unit < unat max_time" - apply (fastforce simp: unat_max_word[symmetric] ticks_per_timer_unit_def MAX_PERIOD_US_def) + "5 * unat ARM.MAX_PERIOD_US * unat ticks_per_timer_unit < unat ARM.max_time" + apply (fastforce simp: unat_max_word[symmetric] ticks_per_timer_unit_def ARM.MAX_PERIOD_US_def) done have kernelWCET_pos': "0 < us_to_ticks kernelWCET_us" @@ -185,34 +184,34 @@ have MIN_BUDGET_pos': "0 < 2 * us_to_ticks kernelWCET_us" | fastforce simp: kernelWCET_us_def ticks_per_timer_unit_def timer_unit_def unat_minus_one_word)+ done -have init_domain_time_pos: "0 < us_to_ticks (15 * \s_in_ms)" +have init_domain_time_pos: "0 < us_to_ticks (15 * ARM.\s_in_ms)" apply (clarsimp simp: us_to_ticks_def word_less_nat_alt) apply (subst unat_mult_lem' | subst unat_div - | fastforce simp: \s_in_ms_def ticks_per_timer_unit_def timer_unit_def unat_minus_one_word)+ + | fastforce simp: ARM.\s_in_ms_def ticks_per_timer_unit_def timer_unit_def unat_minus_one_word)+ done -have init_domain_time_bound: "15 * unat \s_in_ms * unat ticks_per_timer_unit < unat max_time" +have init_domain_time_bound: "15 * unat ARM.\s_in_ms * unat ticks_per_timer_unit < unat ARM.max_time" apply (subst unat_mult_lem' - | fastforce simp: \s_in_ms_def ticks_per_timer_unit_def unat_minus_one_word)+ + | fastforce simp: ARM.\s_in_ms_def ticks_per_timer_unit_def unat_minus_one_word)+ done have getCurrentTime_buffer_pos: - "0 < 5 * us_to_ticks MAX_PERIOD_US" - apply (fastforce simp: us_to_ticks_def word_less_nat_alt MAX_PERIOD_US_def + "0 < 5 * us_to_ticks ARM.MAX_PERIOD_US" + apply (fastforce simp: us_to_ticks_def word_less_nat_alt ARM.MAX_PERIOD_US_def ticks_per_timer_unit_def timer_unit_def) done end -consts' kernelWCET_us :: ticks +consts' kernelWCET_us :: ARM.ticks axiomatization where kernelWCET_us_pos2: "0 < 2 * kernelWCET_us" and - MIN_BUDGET_le_MAX_PERIOD: "2 * kernelWCET_us \ MAX_PERIOD_US" + MIN_BUDGET_le_MAX_PERIOD: "2 * kernelWCET_us \ ARM.MAX_PERIOD_US" -consts' ticks_per_timer_unit :: ticks -consts' timer_unit :: ticks +consts' ticks_per_timer_unit :: ARM.ticks +consts' timer_unit :: ARM.ticks definition "us_to_ticks us = (us * ticks_per_timer_unit) div timer_unit" @@ -220,29 +219,29 @@ definition axiomatization where ticks_per_timer_unit_non_zero: "ticks_per_timer_unit \ 0" and - MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < unat max_time" + MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < unat ARM.max_time" and \ \the 5 is from time_buffer_const (defined below)\ getCurrentTime_buffer_bound: - "5 * unat MAX_PERIOD_US * unat ticks_per_timer_unit < unat max_time" + "5 * unat ARM.MAX_PERIOD_US * unat ticks_per_timer_unit < unat ARM.max_time" and kernelWCET_pos': "0 < us_to_ticks kernelWCET_us" and MIN_BUDGET_pos': "0 < 2 * us_to_ticks kernelWCET_us" and \ \the 15 is from the domain time of the initial state\ - init_domain_time_pos: "0 < us_to_ticks (15 * \s_in_ms)" + init_domain_time_pos: "0 < us_to_ticks (15 * ARM.\s_in_ms)" and \ \the 15 is from the domain time of the initial state\ - init_domain_time_bound: "15 * unat \s_in_ms * unat ticks_per_timer_unit < unat max_time" + init_domain_time_bound: "15 * unat ARM.\s_in_ms * unat ticks_per_timer_unit < unat ARM.max_time" and \ \the 5 is from time_buffer_const (defined below)\ - getCurrentTime_buffer_pos: "0 < 5 * us_to_ticks MAX_PERIOD_US" + getCurrentTime_buffer_pos: "0 < 5 * us_to_ticks ARM.MAX_PERIOD_US" -definition "MAX_PERIOD = us_to_ticks MAX_PERIOD_US" +definition "MAX_PERIOD = us_to_ticks ARM.MAX_PERIOD_US" axiomatization - ticks_to_us :: "ticks \ ticks" + ticks_to_us :: "ARM.ticks \ ARM.ticks" end_qualify diff --git a/spec/machine/MachineExports.thy b/spec/machine/MachineExports.thy index 1d1e63f89e..5ac2632b7a 100644 --- a/spec/machine/MachineExports.thy +++ b/spec/machine/MachineExports.thy @@ -16,6 +16,8 @@ arch_requalify_types vmfault_type hyp_fault_type irq + user_monad + user_context ticks time @@ -70,7 +72,7 @@ arch_requalify_consts time_buffer_const \s_in_ms -requalify_facts +arch_requalify_facts MAX_PERIOD_US_def MAX_PERIOD_def kernelWCET_ticks_def diff --git a/spec/machine/RISCV64/MachineOps.thy b/spec/machine/RISCV64/MachineOps.thy index 8846817d74..99edec082c 100644 --- a/spec/machine/RISCV64/MachineOps.thy +++ b/spec/machine/RISCV64/MachineOps.thy @@ -27,7 +27,7 @@ text \ All this is done only to avoid a large number of axioms (2 for each operation). \ -context Arch begin global_naming RISCV64 +context Arch begin arch_global_naming section "The Operations" @@ -84,10 +84,6 @@ consts' timerPrecision :: "64 word" consts' max_ticks_to_us :: "64 word" consts' max_us_to_ticks :: "64 word" -end - -qualify RISCV64 (in Arch) - type_synonym ticks = "64 word" type_synonym time = "64 word" @@ -101,6 +97,10 @@ text \ This matches @{text "60 * 60 * MS_IN_S * US_IN_MS"} because it shou definition MAX_PERIOD_US :: "64 word" where "MAX_PERIOD_US \ 60 * 60 * 1000 * 1000" +end + +qualify RISCV64 (in Arch) + \ \The following notepad shows that the axioms introduced below, which provide various results about several constants and their conversion via us_to_ticks, are consistent.\ @@ -115,13 +115,13 @@ define us_to_ticks :: "64 word \ 64 word" where have kernelWCET_us_pos2: "0 < 2 * kernelWCET_us" by (simp add: kernelWCET_us_def) -have MIN_BUDGET_le_MAX_PERIOD: "2 * kernelWCET_us \ MAX_PERIOD_US" - by (simp add: kernelWCET_us_def MAX_PERIOD_US_def) +have MIN_BUDGET_le_MAX_PERIOD: "2 * kernelWCET_us \ RISCV64.MAX_PERIOD_US" + by (simp add: kernelWCET_us_def RISCV64.MAX_PERIOD_US_def) have ticks_per_timer_unit_non_zero: "ticks_per_timer_unit \ 0" by (simp add: ticks_per_timer_unit_def) -have MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < unat max_time" +have MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < unat RISCV64.max_time" apply (subst unat_max_word[symmetric]) apply clarsimp apply (prop_tac "unat kernelWCET_us \ 100") @@ -134,8 +134,8 @@ have MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < una done have getCurrentTime_buffer_bound: - "5 * unat MAX_PERIOD_US * unat ticks_per_timer_unit < unat max_time" - apply (fastforce simp: unat_max_word[symmetric] ticks_per_timer_unit_def MAX_PERIOD_US_def) + "5 * unat RISCV64.MAX_PERIOD_US * unat ticks_per_timer_unit < unat RISCV64.max_time" + apply (fastforce simp: unat_max_word[symmetric] ticks_per_timer_unit_def RISCV64.MAX_PERIOD_US_def) done have kernelWCET_pos': "0 < us_to_ticks kernelWCET_us" @@ -150,34 +150,34 @@ have MIN_BUDGET_pos': "0 < 2 * us_to_ticks kernelWCET_us" | fastforce simp: kernelWCET_us_def ticks_per_timer_unit_def timer_unit_def unat_minus_one_word)+ done -have init_domain_time_pos: "0 < us_to_ticks (15 * \s_in_ms)" +have init_domain_time_pos: "0 < us_to_ticks (15 * RISCV64.\s_in_ms)" apply (clarsimp simp: us_to_ticks_def word_less_nat_alt) apply (subst unat_mult_lem' | subst unat_div - | fastforce simp: \s_in_ms_def ticks_per_timer_unit_def timer_unit_def unat_minus_one_word)+ + | fastforce simp: RISCV64.\s_in_ms_def ticks_per_timer_unit_def timer_unit_def unat_minus_one_word)+ done -have init_domain_time_bound: "15 * unat \s_in_ms * unat ticks_per_timer_unit < unat max_time" +have init_domain_time_bound: "15 * unat RISCV64.\s_in_ms * unat ticks_per_timer_unit < unat RISCV64.max_time" apply (subst unat_mult_lem' - | fastforce simp: \s_in_ms_def ticks_per_timer_unit_def unat_minus_one_word)+ + | fastforce simp: RISCV64.\s_in_ms_def ticks_per_timer_unit_def unat_minus_one_word)+ done have getCurrentTime_buffer_pos: - "0 < 5 * us_to_ticks MAX_PERIOD_US" - apply (fastforce simp: us_to_ticks_def word_less_nat_alt MAX_PERIOD_US_def + "0 < 5 * us_to_ticks RISCV64.MAX_PERIOD_US" + apply (fastforce simp: us_to_ticks_def word_less_nat_alt RISCV64.MAX_PERIOD_US_def ticks_per_timer_unit_def timer_unit_def) done end -consts' kernelWCET_us :: ticks +consts' kernelWCET_us :: RISCV64.ticks axiomatization where kernelWCET_us_pos2: "0 < 2 * kernelWCET_us" and - MIN_BUDGET_le_MAX_PERIOD: "2 * kernelWCET_us \ MAX_PERIOD_US" + MIN_BUDGET_le_MAX_PERIOD: "2 * kernelWCET_us \ RISCV64.MAX_PERIOD_US" -consts' ticks_per_timer_unit :: ticks -consts' timer_unit :: ticks +consts' ticks_per_timer_unit :: RISCV64.ticks +consts' timer_unit :: RISCV64.ticks definition "us_to_ticks us = (us * ticks_per_timer_unit) div timer_unit" @@ -185,29 +185,29 @@ definition axiomatization where ticks_per_timer_unit_non_zero: "ticks_per_timer_unit \ 0" and - MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < unat max_time" + MIN_BUDGET_bound: "2 * unat kernelWCET_us * unat ticks_per_timer_unit < unat RISCV64.max_time" and \ \the 5 is from time_buffer_const (defined below)\ getCurrentTime_buffer_bound: - "5 * unat MAX_PERIOD_US * unat ticks_per_timer_unit < unat max_time" + "5 * unat RISCV64.MAX_PERIOD_US * unat ticks_per_timer_unit < unat RISCV64.max_time" and kernelWCET_pos': "0 < us_to_ticks kernelWCET_us" and MIN_BUDGET_pos': "0 < 2 * us_to_ticks kernelWCET_us" and \ \the 15 is from the domain time of the initial state\ - init_domain_time_pos: "0 < us_to_ticks (15 * \s_in_ms)" + init_domain_time_pos: "0 < us_to_ticks (15 * RISCV64.\s_in_ms)" and \ \the 15 is from the domain time of the initial state\ - init_domain_time_bound: "15 * unat \s_in_ms * unat ticks_per_timer_unit < unat max_time" + init_domain_time_bound: "15 * unat RISCV64.\s_in_ms * unat ticks_per_timer_unit < unat RISCV64.max_time" and \ \the 5 is from time_buffer_const (defined below)\ - getCurrentTime_buffer_pos: "0 < 5 * us_to_ticks MAX_PERIOD_US" + getCurrentTime_buffer_pos: "0 < 5 * us_to_ticks RISCV64.MAX_PERIOD_US" -definition "MAX_PERIOD = us_to_ticks MAX_PERIOD_US" +definition "MAX_PERIOD = us_to_ticks RISCV64.MAX_PERIOD_US" axiomatization - ticks_to_us :: "ticks \ ticks" + ticks_to_us :: "RISCV64.ticks \ RISCV64.ticks" end_qualify