3 files changed, 52 insertions, 37 deletions
diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats
index 2d12dbf..17a9f72 100644
--- a/kernel/memory/paging/entry.sats
+++ b/kernel/memory/paging/entry.sats
@@ -1,16 +1,9 @@
 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
@@ -24,9 +17,9 @@ datatype entry_flag =
   | NO_EXECUTE 
 
 fn is_unused(entry_t) : bool
-fn set_unused(&entry_t) : void
+fn set_unused(&entry_t) :<!wrt> void
 
-fn contains_flag(entry_t,entry_flag) : bool
+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
diff --git a/kernel/memory/paging/table.dats b/kernel/memory/paging/table.dats
index d5029a7..e636c6c 100644
--- a/kernel/memory/paging/table.dats
+++ b/kernel/memory/paging/table.dats
@@ -8,13 +8,16 @@ staload "./entry.sats"
 staload "lib/SATS/valid.sats"
 staload "lib/DATS/valid.dats"
 
+assume table_t(c:int) = tablePtr1 c
+
+
 // 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]
+fn next_table_address{n:int|n < 3}(table : !table_t(n), index : sizeLt(ENTRY_COUNT)):<> Valid Ptr1 = let
+  val entry = table_get_at(table,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))
+      val next = g1ofg0((Ptr1_to_sz(table.3) << 9) lor (index << 12))
     in
       if next > i2sz(0) then
         create_valid(sz_to_Ptr1(next))
@@ -25,10 +28,23 @@ in
     create_unvalid()
 end
 
+implement table_get_at(table,i) = let
+  val entry = (table.3->[i]) : entry_t
+in
+  entry
+end
+
+implement table_set_at(table,i,x) = table.3->[i] := x
+
 implement set_zero(table) = let 
-  implement array_foreach$fwork<entry_t><void>(entry,v) = set_unused(entry)
+  fun loop{i:nat | i < ENTRY_COUNT}.<ENTRY_COUNT-i>.(i : size_t i,t : !Table_t):<!wrt> void = let 
+  in
+    set_unused(t.3->[i]);
+    if i < ENTRY_COUNT - 1 then
+      loop(succ(i),t)
+  end
 in
-  assertloc(array_foreach<entry_t>(table,i2sz(ENTRY_COUNT)) = i2sz(ENTRY_COUNT))
+  loop(i2sz(0),table)
 end
 
 // UNSAFE: unsafe block
@@ -38,31 +54,29 @@ local
 
 in
 
-  implement get_P4() = @{
-    ptr = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul)),
-    level = (0u | )
-  }
+  implement get_P4() =  let
+    val (pf,fpf | p) = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul))
+  in
+    (pf,fpf,0u | p)
+  end
 
-  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
+  implement next_table(table,index) = let
+    val next = next_table_address(table,index)
+    prval level = table.2
   in
+    consume(table);
     if is_valid(next) then 
       let
-        val p = unwrap_valid(next)
+        val t = unwrap_valid(next)
+        val (pf, fpf | p) = $UN.ptr_vtake(t)
       in
-        create_valid(@{
-          ptr = $UN.ptr_vtake(p),
-          level = ( succ(tp.level.0) | )
-        })
+       create_valid ((pf,fpf, succ(level) | p))
       end
     else
       let
         val () = destroy_unvalid(next)
       in
         create_unvalid()
-      end
+      end;
   end
-
 end
diff --git a/kernel/memory/paging/table.sats b/kernel/memory/paging/table.sats
index 9a103f4..491b77e 100644
--- a/kernel/memory/paging/table.sats
+++ b/kernel/memory/paging/table.sats
@@ -4,16 +4,24 @@ staload "./entry.sats"
 staload "lib/SATS/valid.sats"
 staload "lib/DATS/valid.dats"
 
-typedef table_t = @[entry_t][ENTRY_COUNT]
+vtypedef tablePtr1(level : int)  = [l : agz] (@[entry_t][ENTRY_COUNT]@l , @[entry_t][ENTRY_COUNT]@l -<lin,prf> void, uint level | ptr l)
 
-vtypedef tablePtr1(c : int)  = @{
-    ptr = [l : agz] (table_t@l , table_t@l -<lin,prf> void | ptr l),
-    level = (uint c | )
-  }
+absvt@ype table_t(level:int) = tablePtr1 level
+
+vtypedef Table_t = [level:nat | level < 4] table_t(level)
+
+fun table_get_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT)):<> entry_t
+
+fun table_set_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT), x: entry_t):<!wrt> void
+
+overload [] with table_get_at
+overload [] with table_set_at
 
 // Set all the entries in the table to unused (zero)
-fn set_zero(&table_t): void
+fn set_zero(&Table_t):<!wrt> void
+
+castfn consume(Table_t): void
 
-fun get_P4() : tablePtr1(0)
+fun get_P4() : table_t 0
 
-fun next_table{n : nat | n < 3}(tablePtr1(n), sizeLt(ENTRY_COUNT)) : Valid (tablePtr1(n+1))
+fun next_table{n : nat | n < 3}(table_t n, sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1))