[squash] PR feedback

seL4 · May 30, 2024 · c1843c6 · c1843c6
1 parent fe257fe
commit c1843c6
Show file tree

Hide file tree

Showing 7 changed files with 8 additions and 9 deletions.
diff --git a/proof/crefine/ARM/IsolatedThreadAction.thy b/proof/crefine/ARM/IsolatedThreadAction.thy
@@ -247,12 +247,12 @@ lemma zipWithM_setRegister_simple:
                             simpler_modify_def fun_upd_def[symmetric])
   done
 
-(* these variant used in fastpath rewrite proof *)
+(* this variant used in fastpath rewrite proof *)
 lemma setRegister_simple_modify_registers:
   "setRegister r v = (\<lambda>con. ({((), modify_registers (\<lambda>f. f(r := v)) con)}, False))"
   by (simp add: modify_registers_def setRegister_simple)
 
-(* these variant used in fastpath rewrite proof *)
+(* this variant used in fastpath rewrite proof *)
 lemma zipWithM_setRegister_simple_modify_registers:
   "zipWithM_x setRegister rs vs
    = (\<lambda>con. ({((), modify_registers (\<lambda>regs. foldl (\<lambda>f (r,v). f(r := v)) regs (zip rs vs)) con)},

diff --git a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy
@@ -244,12 +244,12 @@ lemma zipWithM_setRegister_simple:
                             simpler_modify_def fun_upd_def[symmetric])
   done
 
-(* these variant used in fastpath rewrite proof *)
+(* this variant used in fastpath rewrite proof *)
 lemma setRegister_simple_modify_registers:
   "setRegister r v = (\<lambda>con. ({((), modify_registers (\<lambda>f. f(r := v)) con)}, False))"
   by (simp add: modify_registers_def setRegister_simple)
 
-(* these variant used in fastpath rewrite proof *)
+(* this variant used in fastpath rewrite proof *)
 lemma zipWithM_setRegister_simple_modify_registers:
   "zipWithM_x setRegister rs vs
    = (\<lambda>con. ({((), modify_registers (\<lambda>regs. foldl (\<lambda>f (r,v). f(r := v)) regs (zip rs vs)) con)},

diff --git a/proof/drefine/Schedule_DR.thy b/proof/drefine/Schedule_DR.thy
@@ -625,7 +625,6 @@ lemma transform_tcb_NextIP:
   = transform_tcb m t tcb"
   apply (rule ext)
   apply (simp add: transform_tcb_def transform_full_intent_def Let_def)
-
   by (auto simp add: transform_tcb_def transform_full_intent_def Let_def
                      cap_register_def ARM.capRegister_def
                      arch_tcb_context_get_def)

diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy
@@ -4255,7 +4255,7 @@ proof -
 
   show ?thesis using m
     unfolding setMRs_def set_mrs_def
-    apply (clarsimp  cong: option.case_cong split del: if_split)
+    apply (clarsimp cong: option.case_cong split del: if_split)
     apply (subst bind_assoc[symmetric])
     apply (fold thread_set_def[simplified])
     apply (subst thread_set_as_user_registers)

diff --git a/proof/refine/ARM_HYP/TcbAcc_R.thy b/proof/refine/ARM_HYP/TcbAcc_R.thy
@@ -4306,7 +4306,7 @@ proof -
 
   show ?thesis using m
     unfolding setMRs_def set_mrs_def
-    apply (clarsimp  cong: option.case_cong split del: if_split)
+    apply (clarsimp cong: option.case_cong split del: if_split)
     apply (subst bind_assoc[symmetric])
     apply (fold thread_set_def[simplified])
     apply (subst thread_set_as_user_registers)

diff --git a/spec/machine/ARM/MachineOps.thy b/spec/machine/ARM/MachineOps.thy
@@ -504,7 +504,7 @@ type_synonym 'a user_monad = "(user_context, 'a) nondet_monad"
 definition getRegister :: "register \<Rightarrow> machine_word user_monad" where
   "getRegister r \<equiv> gets (\<lambda>s. user_regs s r)"
 
-definition
+definition modify_registers :: "(user_regs \<Rightarrow> user_regs) \<Rightarrow> user_context \<Rightarrow> user_context" where
   "modify_registers f uc \<equiv> UserContext (f (user_regs uc))"
 
 definition setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad" where

diff --git a/spec/machine/ARM_HYP/MachineOps.thy b/spec/machine/ARM_HYP/MachineOps.thy
@@ -729,7 +729,7 @@ type_synonym 'a user_monad = "(user_context, 'a) nondet_monad"
 definition getRegister :: "register \<Rightarrow> machine_word user_monad" where
   "getRegister r \<equiv> gets (\<lambda>s. user_regs s r)"
 
-definition
+definition modify_registers :: "(user_regs \<Rightarrow> user_regs) \<Rightarrow> user_context \<Rightarrow> user_context" where
   "modify_registers f uc \<equiv> UserContext (f (user_regs uc))"
 
 definition setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad" where