ARM ainvs: proof update for user_context refactor

proof/invariant-abstract/ARM/ArchAcc_AI.thy

@@ -3359,6 +3359,35 @@ crunch device_state_inv[wp]: storeWord "\<lambda>ms. P (device_state ms)"
 crunch device_state_inv[wp]: cleanByVA_PoU "\<lambda>ms. P (device_state ms)"
 crunch device_state_inv[wp]: cleanL2Range "\<lambda>ms. P (device_state ms)"
 
+lemma as_user_inv:
+  assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
+  shows      "\<lbrace>P\<rbrace> as_user t f \<lbrace>\<lambda>x. P\<rbrace>"
+proof -
+  have P: "\<And>a b input. (a, b) \<in> fst (f input) \<Longrightarrow> b = input"
+    by (rule use_valid [OF _ x], assumption, rule refl)
+  have Q: "\<And>s ps. ps (kheap s) = kheap s \<Longrightarrow> kheap_update ps s = s"
+    by simp
+  show ?thesis
+    apply (simp add: as_user_def gets_the_def assert_opt_def set_object_def split_def)
+    apply wp
+    apply (clarsimp dest!: P)
+    apply (subst Q)
+     prefer 2
+     apply assumption
+    apply (rule ext)
+    apply (simp add: get_tcb_def)
+    apply (case_tac "kheap s t"; simp)
+    apply (case_tac a; simp)
+    apply (clarsimp simp: arch_tcb_context_set_def arch_tcb_context_get_def)
+    done
+qed
+
+lemma user_getreg_inv[wp]:
+  "\<lbrace>P\<rbrace> as_user t (getRegister r) \<lbrace>\<lambda>x. P\<rbrace>"
+  apply (rule as_user_inv)
+  apply (simp add: getRegister_def)
+  done
+
 end
 
 end

proof/invariant-abstract/ARM/ArchBCorres2_AI.thy

@@ -86,8 +86,8 @@ lemmas schedule_bcorres[wp] = schedule_bcorres1[OF BCorres2_AI_axioms]
 context Arch begin global_naming ARM
 
 crunch (bcorres)bcorres[wp]: send_ipc,send_signal,do_reply_transfer,arch_perform_invocation truncate_state
-  (simp: gets_the_def swp_def ignore: freeMemory clearMemory get_register loadWord cap_fault_on_failure
-         set_register storeWord lookup_error_on_failure getRestartPC getRegister mapME)
+  (simp: gets_the_def swp_def ignore: freeMemory clearMemory loadWord cap_fault_on_failure
+         storeWord lookup_error_on_failure getRestartPC getRegister mapME)
 
 lemma perform_invocation_bcorres[wp]: "bcorres (perform_invocation a b c) (perform_invocation a b c)"
   apply (cases c)
@@ -124,8 +124,8 @@ lemma ensure_safe_mapping_bcorres[wp]: "bcorres (ensure_safe_mapping a) (ensure_
   done
 
 crunch (bcorres)bcorres[wp]: handle_invocation truncate_state
-  (simp: syscall_def Let_def gets_the_def ignore: get_register syscall cap_fault_on_failure
-         set_register without_preemption const_on_failure)
+  (simp: syscall_def Let_def gets_the_def ignore: syscall cap_fault_on_failure
+         without_preemption const_on_failure)
 
 crunch (bcorres)bcorres[wp]: receive_ipc,receive_signal,delete_caller_cap truncate_state
 

proof/invariant-abstract/ARM/ArchInvariants_AI.thy

@@ -2290,6 +2290,14 @@ lemma tcb_arch_ref_context_update:
   "tcb_arch_ref (t\<lparr>tcb_arch := (arch_tcb_context_set a (tcb_arch t))\<rparr>) = tcb_arch_ref t"
   by (simp add: tcb_arch_ref_def arch_tcb_context_set_def)
 
+lemma tcb_arch_ref_set_registers:
+  "tcb_arch_ref (tcb\<lparr>tcb_arch := arch_tcb_set_registers regs (tcb_arch tcb)\<rparr>) = tcb_arch_ref tcb"
+  by (simp add: tcb_arch_ref_def)
+
+lemma valid_arch_arch_tcb_set_registers[simp]:
+  "valid_arch_tcb (arch_tcb_set_registers a t) = valid_arch_tcb t"
+   by (simp add: arch_tcb_set_registers_def)
+
 lemma tcb_arch_ref_ipc_buffer_update: "\<And>tcb.
        tcb_arch_ref (tcb_ipc_buffer_update f tcb) = tcb_arch_ref tcb"
   by (simp add: tcb_arch_ref_def)
@@ -2339,7 +2347,7 @@ lemmas tcb_arch_ref_simps[simp] = tcb_arch_ref_ipc_buffer_update tcb_arch_ref_mc
   tcb_arch_ref_ctable_update tcb_arch_ref_vtable_update tcb_arch_ref_reply_update
   tcb_arch_ref_caller_update tcb_arch_ref_ipcframe_update tcb_arch_ref_state_update
   tcb_arch_ref_fault_handler_update tcb_arch_ref_fault_update tcb_arch_ref_bound_notification_update
-  tcb_arch_ref_context_update
+  tcb_arch_ref_context_update tcb_arch_ref_set_registers
 
 lemma hyp_live_tcb_def: "hyp_live (TCB tcb) = bound (tcb_arch_ref tcb)"
   by (clarsimp simp: hyp_live_def tcb_arch_ref_def)

proof/invariant-abstract/ARM/ArchIpc_AI.thy

@@ -257,13 +257,8 @@ lemma copy_mrs_in_user_frame[wp, Ipc_AI_assms]:
   "\<lbrace>in_user_frame p\<rbrace> copy_mrs t buf t' buf' n \<lbrace>\<lambda>rv. in_user_frame p\<rbrace>"
   by (simp add: in_user_frame_def) (wp hoare_vcg_ex_lift)
 
-lemma get_register_eq : "getRegister r = get_register r"
-  apply (simp add: getRegister_def get_register_def)
-  done
-
 lemma as_user_getRestart_invs[wp]: "\<lbrace>P\<rbrace> as_user t getRestartPC \<lbrace>\<lambda>_. P\<rbrace>"
-  apply (simp add: get_register_eq getRestartPC_def ; rule user_getreg_inv)
-  done
+  by (simp add: getRestartPC_def, rule user_getreg_inv)
 
 lemma make_arch_fault_msg_inv[wp]: "\<lbrace>P\<rbrace> make_arch_fault_msg f t \<lbrace>\<lambda>_. P\<rbrace>"
   apply (cases f)