Implemented entry

1 files changed, 34 insertions, 0 deletions

diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats
new file mode 100644
index 0000000..a7f91ee
--- /dev/null
+++ b/kernel/memory/paging/entry.sats
@@ -0,0 +1,34 @@
+#define ENTRY_COUNT 512
+
+staload "kernel/memory/frame.sats"
+staload "lib/SATS/valid.sats"
+
+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 contains_flag(entry_t,entry_flag) : bool
+fn pointed_frame(entry_t) : Valid frame_t
+
+fn entry_set{n:nat}(&entry_t,frame_t,&(@[entry_flag][n]),size_t n) : void