staload FRAME = "kernel/memory/frame.sats"

staload "lib/SATS/valid.sats"
staload "./entry.sats"

typedef vaddr = Ptr0

typedef page_t = @{
  num = size_t
}

fn translate(vaddr) : Valid $FRAME.paddr

fn containing_address(vaddr) : page_t

fn map_to{n:nat}(page_t,$FRAME.frame_t,&(@[entry_flag][n]),size : size_t n): void

fn map{n:nat}(page_t,&(@[entry_flag][n]),size : size_t n) : void