[squash] design: comment on arch_invocation_label requalify

(can't be moved)
seL4 · Aug 18, 2024 · 7fdff26 · 7fdff26
1 parent c3a92bf
commit 7fdff26
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 0 deletions.
diff --git a/spec/design/skel/AARCH64/ArchInvocationLabels_H.thy b/spec/design/skel/AARCH64/ArchInvocationLabels_H.thy
@@ -21,6 +21,8 @@ text \<open>
 
 end
 
+(* not possible to move this requalification to generic, since enum instance proofs must
+   be done outside of Arch locale *)
 arch_requalify_types (H)
   arch_invocation_label
 

diff --git a/spec/design/skel/ARM/ArchInvocationLabels_H.thy b/spec/design/skel/ARM/ArchInvocationLabels_H.thy
@@ -21,6 +21,8 @@ text \<open>
 
 end
 
+(* not possible to move this requalification to generic, since enum instance proofs must
+   be done outside of Arch locale *)
 arch_requalify_types (H)
   arch_invocation_label
 

diff --git a/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy b/spec/design/skel/ARM_HYP/ArchInvocationLabels_H.thy
@@ -21,6 +21,8 @@ text \<open>
 
 end
 
+(* not possible to move this requalification to generic, since enum instance proofs must
+   be done outside of Arch locale *)
 arch_requalify_types (H)
   arch_invocation_label
 

diff --git a/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy b/spec/design/skel/RISCV64/ArchInvocationLabels_H.thy
@@ -21,6 +21,8 @@ text \<open>
 
 end
 
+(* not possible to move this requalification to generic, since enum instance proofs must
+   be done outside of Arch locale *)
 arch_requalify_types (H)
   arch_invocation_label
 

diff --git a/spec/design/skel/X64/ArchInvocationLabels_H.thy b/spec/design/skel/X64/ArchInvocationLabels_H.thy
@@ -21,6 +21,8 @@ text \<open>
 
 end
 
+(* not possible to move this requalification to generic, since enum instance proofs must
+   be done outside of Arch locale *)
 arch_requalify_types (H)
   arch_invocation_label