2 files changed, 8 insertions, 0 deletions
diff --git a/kernel/memory/paging.dats b/kernel/memory/paging.dats
index 9b55624..84a8bf4 100644
--- a/kernel/memory/paging.dats
+++ b/kernel/memory/paging.dats
@@ -6,6 +6,7 @@ staload UN = "prelude/SATS/unsafe.sats"
 
 staload "./paging.sats"
 staload "./frame.sats"
+staload "lib/SATS/valid.sats"
 
 assume entry_type = uint64
 
@@ -28,3 +29,8 @@ implement flag_contains(entry,flag) =
       | NO_EXECUTE() => 63
     ))) != zero
 
+(* implement test()  = let *)
+(* in *)
+(*   (5,true) *)
+(* end *)
+
diff --git a/kernel/memory/paging.sats b/kernel/memory/paging.sats
index 784f567..477e942 100644
--- a/kernel/memory/paging.sats
+++ b/kernel/memory/paging.sats
@@ -1,6 +1,7 @@
 #define ENTRY_COUNT 512
 
 staload "./frame.sats"
+staload "lib/SATS/valid.sats"
 
 abstype paddr_type(l:addr) = ptr(l)
 typedef paddr(l:addr) = paddr_type(l)
@@ -31,3 +32,4 @@ fn is_unused(entry_t) : bool
 fn set_unused(&entry_t) : void
 
 fn flag_contains(entry_t,entry_flag) : bool
+fn test() : [b : bool] valid(int,b)