aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/paging.sats
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/memory/paging.sats')
-rw-r--r--kernel/memory/paging.sats33
1 files changed, 33 insertions, 0 deletions
diff --git a/kernel/memory/paging.sats b/kernel/memory/paging.sats
new file mode 100644
index 0000000..784f567
--- /dev/null
+++ b/kernel/memory/paging.sats
@@ -0,0 +1,33 @@
+#define ENTRY_COUNT 512
+
+staload "./frame.sats"
+
+abstype paddr_type(l:addr) = ptr(l)
+typedef paddr(l:addr) = paddr_type(l)
+
+abstype vaddr_type(l:addr) = ptr(l)
+typedef vaddr(l:addr) = vaddr_type(l)
+
+abst@ype entry_type = uint64
+typedef entry_t = entry_type
+
+typedef page_t = @{
+ num = size_t
+}
+
+datatype entry_flag =
+ | PRESENT
+ | WRITABLE
+ | USER_ACCESSIBLE
+ | WRITE_THROUGH
+ | NO_CACHE
+ | ACCESSED
+ | DIRTY
+ | HUGE_PAGE
+ | GLOBAL
+ | NO_EXECUTE
+
+fn is_unused(entry_t) : bool
+fn set_unused(&entry_t) : void
+
+fn flag_contains(entry_t,entry_flag) : bool