#define ATS_DYNLOADFLAG 0

#include "kernel/prelude/kernel_prelude.hats"

staload UN = "prelude/SATS/unsafe.sats"

staload "./paging.sats"
staload "./frame.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