[squash] design: requalify comments for wordBits

seL4 · Aug 18, 2024 · 03423cb · 03423cb
1 parent 7fdff26
commit 03423cb
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 0 deletions.
diff --git a/spec/design/skel/AARCH64/State_H.thy b/spec/design/skel/AARCH64/State_H.thy
@@ -26,6 +26,8 @@ where
 
 end
 
+(* Note: while this requalify and arch-generic Haskell import of WordLib.lhs could be moved to
+   a generic theory, no good candidate theory exists at the moment. *)
 arch_requalify_consts (H)
   wordBits
 

diff --git a/spec/design/skel/ARM/State_H.thy b/spec/design/skel/ARM/State_H.thy
@@ -28,6 +28,8 @@ where
 
 end
 
+(* Note: while this requalify and arch-generic Haskell import of WordLib.lhs could be moved to
+   a generic theory, no good candidate theory exists at the moment. *)
 arch_requalify_consts (H)
   wordBits
 

diff --git a/spec/design/skel/ARM_HYP/State_H.thy b/spec/design/skel/ARM_HYP/State_H.thy
@@ -28,6 +28,8 @@ where
 
 end
 
+(* Note: while this requalify and arch-generic Haskell import of WordLib.lhs could be moved to
+   a generic theory, no good candidate theory exists at the moment. *)
 arch_requalify_consts (H)
   wordBits
 

diff --git a/spec/design/skel/RISCV64/State_H.thy b/spec/design/skel/RISCV64/State_H.thy
@@ -26,6 +26,8 @@ where
 
 end
 
+(* Note: while this requalify and arch-generic Haskell import of WordLib.lhs could be moved to
+   a generic theory, no good candidate theory exists at the moment. *)
 arch_requalify_consts (H)
   wordBits
 

diff --git a/spec/design/skel/X64/State_H.thy b/spec/design/skel/X64/State_H.thy
@@ -26,6 +26,8 @@ where
 
 end
 
+(* Note: while this requalify and arch-generic Haskell import of WordLib.lhs could be moved to
+   a generic theory, no good candidate theory exists at the moment. *)
 arch_requalify_consts (H)
   wordBits