6 files changed, 69 insertions, 45 deletions
diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats
index aa02134..867096a 100644
--- a/kernel/memory/frame.dats
+++ b/kernel/memory/frame.dats
@@ -12,8 +12,10 @@ staload UN = "prelude/SATS/unsafe.sats"
 
 implement containing_address(address) = 
   @{ 
-    counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE)
-  }
+    num = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE)
+   }
+
+implement start_address(frame) = sz_to_Ptr0(frame.num * PAGE_SIZE)
 
 fn containing_area(area : $BOOT.memory_area_t) :<> frame_t = containing_address(ptr_add<uint8>(area.base_addr,area.length - i2sz(1)))
 
diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats
index dfd422e..6580ab0 100644
--- a/kernel/memory/frame.sats
+++ b/kernel/memory/frame.sats
@@ -2,6 +2,9 @@
 
 staload "kernel/bootinfo/multiboot.sats"
 
+// Physical address type
+typedef paddr = Ptr0
+
 typedef frame_t = @{
   num = size_t
 }
@@ -16,6 +19,7 @@ typedef frame_allocator_t = @{
 }
 
 fn containing_address{l:addr}(ptr l):<> frame_t
+fn start_address(frame_t):<> paddr
 
 fn allocate_frame () : frame_t
 fn deallocate_frame () : void
diff --git a/kernel/memory/paging.dats b/kernel/memory/paging.dats
deleted file mode 100644
index 84a8bf4..0000000
--- a/kernel/memory/paging.dats
+++ /dev/null
@@ -1,36 +0,0 @@
-#define ATS_DYNLOADFLAG 0
-
-#include "kernel/prelude/kernel_prelude.hats"
-
-staload UN = "prelude/SATS/unsafe.sats"
-
-staload "./paging.sats"
-staload "./frame.sats"
-staload "lib/SATS/valid.sats"
-
-assume entry_type = uint64
-
-val zero = u2uint64(0u)
-
-implement is_unused(entry) = entry = zero
-implement set_unused(entry) = entry := zero
-
-implement flag_contains(entry,flag) = 
-    (entry land $UN.cast{uint64}(1 << (case+ flag 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
-    ))) != zero
-
-(* implement test()  = let *)
-(* in *)
-(*   (5,true) *)
-(* end *)
-
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
diff --git a/kernel/memory/paging.sats b/kernel/memory/paging/entry.sats
index 477e942..a7f91ee 100644
--- a/kernel/memory/paging.sats
+++ b/kernel/memory/paging/entry.sats
@@ -1,11 +1,8 @@
 #define ENTRY_COUNT 512
 
-staload "./frame.sats"
+staload "kernel/memory/frame.sats"
 staload "lib/SATS/valid.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)
 
@@ -31,5 +28,7 @@ datatype entry_flag =
 fn is_unused(entry_t) : bool
 fn set_unused(&entry_t) : void
 
-fn flag_contains(entry_t,entry_flag) : bool
-fn test() : [b : bool] valid(int,b)
+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/prelude/SATS/safe_casts.sats b/kernel/prelude/SATS/safe_casts.sats
index 50a68a8..f8e34db 100644
--- a/kernel/prelude/SATS/safe_casts.sats
+++ b/kernel/prelude/SATS/safe_casts.sats
@@ -1 +1,4 @@
-castfn u2uint64{v : nat | v <= 0xFFFFFFFFFFFFFFFF}(v : uint v) : uint64 v
+castfn u2u64{v : nat | v <= 0xFFFFFFFFFFFFFFFF}(v : uint v) :<> uint64 v
+castfn u64_to_Ptr0(v : uint64):<> Ptr0
+castfn Ptr0_to_u64(v : Ptr0):<> uint64
+castfn sz_to_Ptr0(v : size_t):<> Ptr0