#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