rt spec proof: update after merge

Signed-off-by: Corey Lewis <[email protected]>

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

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 \<lbrace>valid_sched_pred_strong P\<rbrace>"
-  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 \<lbrace>valid_sched_pred_strong P\<rbrace>"
+  unfolding init_arch_objects_def
+  by (wpsimp wp: dmo_valid_sched_pred mapM_x_wp_inv)
 
 crunch init_arch_objects
   for exst[wp]: "\<lambda>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:
   "\<forall>ao. \<not> P (ArchObj ao) \<Longrightarrow>
-    \<lbrace>\<lambda>s. Q (obj_at P p s)\<rbrace> init_arch_objects a b c d e \<lbrace>\<lambda>rv s. Q (obj_at P p s)\<rbrace>"
+    \<lbrace>\<lambda>s. Q (obj_at P p s)\<rbrace> init_arch_objects a b c d e f \<lbrace>\<lambda>rv s. Q (obj_at P p s)\<rbrace>"
   by (auto intro: init_arch_objects_obj_at_non_pd)
 
 lemma perform_asid_control_etcb_at:

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'
 
 \<comment> \<open>crunch these separately so they don't appear in machine_ops_last_machine_time\<close>
-crunch cleanByVA_PoU, cleanCacheRange_PoU
+crunch cleanByVA_PoU, cleanCacheRange_PoU, cleanCacheRange_RAM
   for machine_times[wp, arch_machine_ops_last_machine_time']: "\<lambda>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']: "\<lambda>ms. P (last_machine_time ms) (time_state ms)"

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]: "\<lambda>s. P (cur_thread s)"
-  and ct_in_state[wp, Interrupt_AI_asms]: "ct_in_state P"
+  for cur_thread[wp, Interrupt_AI_assms]: "\<lambda>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

proof/invariant-abstract/ARM/ArchSchedule_AI.thy

@@ -66,7 +66,7 @@ lemma arch_stit_invs[wp, Schedule_AI_assms]:
   "\<lbrace>invs\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. invs\<rbrace>"
   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]:
   "\<lbrace>tcb_at t\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. tcb_at t\<rbrace>"
   apply (simp add: arch_switch_to_idle_thread_def )
   apply wp
@@ -78,7 +78,7 @@ crunch set_vm_root
   and scheduler_action[wp]: "\<lambda>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 \<lbrace>sc_at sc_ptr\<rbrace>"
   apply (simp add: arch_switch_to_idle_thread_def)
   apply wp

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]:
   "\<lbrace>invs and tcb_inv_wf (ThreadControlSched t sl fh mcp pr sc)\<rbrace>
    invoke_tcb (ThreadControlSched t sl fh  mcp pr sc)
    \<lbrace>\<lambda>rv. invs\<rbrace>"
@@ -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

proof/invariant-abstract/ARM/ArchUntyped_AI.thy

@@ -609,9 +609,9 @@ qed
 
 lemma init_arch_objects_obj_at_other[Untyped_AI_assms]:
   "\<lbrakk>\<forall>ptr\<in>set ptrs. is_aligned ptr (obj_bits_api ty us); p \<notin> set ptrs\<rbrakk>
-    \<Longrightarrow> init_arch_objects ty ptr n us ptrs \<lbrace>\<lambda>s. N (obj_at P p s)\<rbrace>"
-  by (wpsimp simp: init_arch_objects_def obj_bits_api_def default_arch_object_def
-                   pd_bits_def pageBits_def
+    \<Longrightarrow> init_arch_objects ty dev ptr n us ptrs \<lbrace>\<lambda>s. N (obj_at P p s)\<rbrace>"
+  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: "\<forall>ko. P ko \<longrightarrow> (\<forall>pd. ko \<noteq> ArchObj (PageDirectory pd))"
-  shows "init_arch_objects ty ptr n us ptrs \<lbrace>\<lambda>s. N (obj_at P p s)\<rbrace>"
-  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 \<lbrace>\<lambda>s. N (obj_at P p s)\<rbrace>"
+  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:
   "\<forall>ko. P ko \<longrightarrow> non_arch_obj ko \<Longrightarrow> \<forall>ko. P ko \<longrightarrow> (\<forall>pd. ko \<noteq> ArchObj (PageDirectory pd))"

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
 

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]:
-    "\<And>t p n s r. init_arch_objects t p n s r \<lbrace>\<lambda>s::'state_ext state. valid_idle s\<rbrace>"
+    "\<And>t d p n s r. init_arch_objects t d p n s r \<lbrace>\<lambda>s::'state_ext state. valid_idle s\<rbrace>"
   assumes init_arch_objects_valid_sched_pred[wp]:
-    "\<And>t p n s r P. init_arch_objects t p n s r \<lbrace>valid_sched_pred_strong P::'state_ext state \<Rightarrow> _\<rbrace>"
+    "\<And>t d p n s r P. init_arch_objects t d p n s r \<lbrace>valid_sched_pred_strong P::'state_ext state \<Rightarrow> _\<rbrace>"
   assumes init_arch_object_valid_machine_time[wp]:
-    "\<And>t p n s r. init_arch_objects t p n s r \<lbrace>valid_machine_time ::'state_ext state \<Rightarrow> _\<rbrace>"
+    "\<And>t d p n s r. init_arch_objects t d p n s r \<lbrace>valid_machine_time ::'state_ext state \<Rightarrow> _\<rbrace>"
   assumes update_time_stamp_valid_machine_time[wp]:
     "update_time_stamp \<lbrace>valid_machine_time::'state_ext state \<Rightarrow> _\<rbrace>"
   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 \<lbrace>\<lambda>s. P (tcbs_of s)\<rbrace>"
+  "init_arch_objects t d p n s r \<lbrace>\<lambda>s. P (tcbs_of s)\<rbrace>"
   apply (rule pred_map_heap_lift[where heap=tcbs_of and P=P and R=\<top>, simplified])
   apply (rule rsubst[where P="\<lambda>t. _ \<lbrace>t\<rbrace>", OF _ ext], rename_tac ref)
    apply (rule_tac N=N and P="\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> 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 \<lbrace>\<lambda>s. P (scs_of s)\<rbrace>"
+  "init_arch_objects t d p n s r \<lbrace>\<lambda>s. P (scs_of s)\<rbrace>"
   apply (rule pred_map_heap_lift[where heap=scs_of and P=P and R=\<top>, simplified])
   apply (rule rsubst[where P="\<lambda>t. _ \<lbrace>t\<rbrace>", OF _ ext], rename_tac ref)
    apply (rule_tac N=N and P="\<lambda>ko. \<exists>sc n. ko = SchedContext sc n \<and> P sc" and p=ref in init_arch_objects_obj_at_non_arch)

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

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:
    \<lbrace>\<lambda>_. cur_sc_in_release_q_imp_zero_consumed\<rbrace>"
   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)

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

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

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

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
    \<Longrightarrow> replies_with_sc (s\<lparr>kheap := (kheap s)(p \<mapsto> SchedContext (f sc v) n)\<rparr>)

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]
 

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

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 \<lbrace>valid_sched_pred_strong P\<rbrace>"
+  "init_arch_objects new_type dev ptr num_objects obj_sz refs \<lbrace>valid_sched_pred_strong P\<rbrace>"
   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:
   "\<forall>ao. \<not> P (ArchObj ao) \<Longrightarrow>
-    \<lbrace>\<lambda>s. Q (obj_at P p s)\<rbrace> init_arch_objects a b c d e \<lbrace>\<lambda>rv s. Q (obj_at P p s)\<rbrace>"
+    \<lbrace>\<lambda>s. Q (obj_at P p s)\<rbrace> init_arch_objects a b c d e f \<lbrace>\<lambda>rv s. Q (obj_at P p s)\<rbrace>"
   by (auto intro: init_arch_objects_obj_at_non_pt)
 
 lemma perform_asid_control_etcb_at:

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]:
   "\<lbrace>\<lambda>s. final \<longrightarrow> is_final_cap' cap s
          \<and> cte_wp_at ((=) cap) slot s\<rbrace>
      finalise_cap cap final

proof/invariant-abstract/RISCV64/ArchInterrupt_AI.thy

@@ -264,12 +264,12 @@ crunch arch_invoke_irq_handler
   for typ_at[wp]: "\<lambda>s. P (typ_at T p s)"
 
 crunch invoke_irq_control
-  for cur_thread[wp, Interrupt_AI_asms]: "\<lambda>s. P (cur_thread s)"
-  and ct_in_state[wp, Interrupt_AI_asms]: "ct_in_state P"
+  for cur_thread[wp, Interrupt_AI_assms]: "\<lambda>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