1 files changed, 52 insertions, 0 deletions
diff --git a/kernel/memory/paging/entry.dats b/kernel/memory/paging/entry.dats
new file mode 100644
index 0000000..7fa97b9
--- /dev/null
+++ b/kernel/memory/paging/entry.dats
@@ -0,0 +1,52 @@
+#define ATS_DYNLOADFLAG 0
+
+#include "kernel/prelude/kernel_prelude.hats"
+
+staload UN = "prelude/SATS/unsafe.sats"
+
+staload "./entry.sats"
+staload FRAME = "kernel/memory/frame.sats"
+staload "lib/SATS/valid.sats"
+staload "lib/DATS/valid.dats"
+
+assume entry_type = uint64
+
+val zero = u2u64(0u)
+
+fn flags2entry{n:nat}(arr : &(@[entry_flag][n]), n: size_t n) : entry_t = let
+  implement array_foreach$fwork<entry_flag><entry_t>(f,k) = k := k lor $UN.cast{entry_t}(1 << (case+ f of 
+      | PRESENT() => 0
+      | WRITABLE() => 1
+      | USER_ACCESSIBLE() => 2
+      | WRITE_THROUGH() => 3 | NO_CACHE() => 4
+      | ACCESSED() => 5
+      | DIRTY() => 6
+      | HUGE_PAGE() => 7
+      | GLOBAL() => 8
+      | NO_EXECUTE() => 63
+  ))
+  var k = g0ofg1(u2u64(0u))
+  val _ = array_foreach_env<entry_flag><entry_t>(arr,n,k)
+in
+  k
+end
+
+implement is_unused(entry) = entry = zero
+implement set_unused(entry) = entry := zero
+
+implement contains_flag(entry,flag) =  (flags2entry(flags,i2sz(1)) land entry) != zero where {
+  var flags = @[entry_flag](PRESENT)
+}
+
+implement pointed_frame(entry) = 
+  if contains_flag(entry,PRESENT) then
+    create_valid($FRAME.containing_address(u64_to_Ptr0(entry land u2u64(0x000FFFFFFFFFF000u))))
+  else
+    create_unvalid()
+
+implement entry_set(entry,frame,flags,n) = let
+  val x = Ptr0_to_u64($FRAME.start_address(frame))
+in
+  assertloc((x land u2u64(0xFFF0000000000FFFu)) = zero);
+  entry := (x lor flags2entry(flags,n))
+end