3 files changed, 87 insertions, 2 deletions
diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats
index a7f91ee..2d12dbf 100644
--- a/kernel/memory/paging/entry.sats
+++ b/kernel/memory/paging/entry.sats
@@ -1,5 +1,3 @@
-#define ENTRY_COUNT 512
-
 staload "kernel/memory/frame.sats"
 staload "lib/SATS/valid.sats"
 
diff --git a/kernel/memory/paging/table.dats b/kernel/memory/paging/table.dats
new file mode 100644
index 0000000..d5029a7
--- /dev/null
+++ b/kernel/memory/paging/table.dats
@@ -0,0 +1,68 @@
+#define ATS_DYNLOADFLAG 0
+
+#include "kernel/prelude/kernel_prelude.hats"
+
+staload "./table.sats"
+staload "./entry.sats" 
+
+staload "lib/SATS/valid.sats"
+staload "lib/DATS/valid.dats"
+
+// Calculate table address of next table based on current table and index: P4->P3->P2->P1
+fn next_table_address{l:agz}(pf : !table_t@l | p : ptr(l), index : sizeLt(ENTRY_COUNT)) : Valid Ptr1 = let
+  val entry = p->[index]
+in
+  if (contains_flag(entry,PRESENT) && ~contains_flag(entry,HUGE_PAGE)) then
+    let 
+      val next = g1ofg0((Ptr1_to_sz(p) << 9) lor (index << 12))
+    in
+      if next > i2sz(0) then
+        create_valid(sz_to_Ptr1(next))
+      else
+        create_unvalid()
+    end
+  else
+    create_unvalid()
+end
+
+implement set_zero(table) = let 
+  implement array_foreach$fwork<entry_t><void>(entry,v) = set_unused(entry)
+in
+  assertloc(array_foreach<entry_t>(table,i2sz(ENTRY_COUNT)) = i2sz(ENTRY_COUNT))
+end
+
+// UNSAFE: unsafe block
+local
+
+  staload UN = "prelude/SATS/unsafe.sats"
+
+in
+
+  implement get_P4() = @{
+    ptr = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul)),
+    level = (0u | )
+  }
+
+  implement next_table(tp,index) = let
+    val k = tp.ptr
+    val next = next_table_address(k.0 | k.2,index)
+    prval () = k.1 k.0
+  in
+    if is_valid(next) then 
+      let
+        val p = unwrap_valid(next)
+      in
+        create_valid(@{
+          ptr = $UN.ptr_vtake(p),
+          level = ( succ(tp.level.0) | )
+        })
+      end
+    else
+      let
+        val () = destroy_unvalid(next)
+      in
+        create_unvalid()
+      end
+  end
+
+end
diff --git a/kernel/memory/paging/table.sats b/kernel/memory/paging/table.sats
new file mode 100644
index 0000000..9a103f4
--- /dev/null
+++ b/kernel/memory/paging/table.sats
@@ -0,0 +1,19 @@
+#define ENTRY_COUNT 512
+
+staload "./entry.sats"
+staload "lib/SATS/valid.sats"
+staload "lib/DATS/valid.dats"
+
+typedef table_t = @[entry_t][ENTRY_COUNT]
+
+vtypedef tablePtr1(c : int)  = @{
+    ptr = [l : agz] (table_t@l , table_t@l -<lin,prf> void | ptr l),
+    level = (uint c | )
+  }
+
+// Set all the entries in the table to unused (zero)
+fn set_zero(&table_t): void
+
+fun get_P4() : tablePtr1(0)
+
+fun next_table{n : nat | n < 3}(tablePtr1(n), sizeLt(ENTRY_COUNT)) : Valid (tablePtr1(n+1))