typedef tag_t = @{
  type = uint32,                      // Identifier of tag
  size = [n : nat | n >= 8] uint n   // Size of tag (not including padding)
}

typedef memory_area_t = @{
  base_addr = Ptr, // Start of physical address
  length = [n : nat | n > 0 ] size_t n ,  // Size of memory region in bytes (64 bits)
  type = uint,      // Variety of address range represented. 1: available RAM, 3: usable memory holding ACPI information, 
                    // 4: reserved memory (preserved on hibernation), Other: reserved area
  reserved = uint 0
}

typedef memory_areas_t = @{ 
    tag = tag_t,
    entry_size = [n : nat | n > 0 && n % 8 == 0] uint n,
    entry_version = uint,
    entries = ptr // Pointer to entries
} 

typedef elf_tag_t = @{
  tag = tag_t,
  num = uint,     // Number of elf entries
  entsize = uint 64, // Size of entry
  shndx = uint,   // Index of the section containing the string table 
  headers = ptr   // Pointer to entries
}

typedef elf64_shdr_t = @{
  name      =  uint,   // Index into seaction header string table
  type      =  uint,   // Type of section (code,data,symbol,...)
  flags     =  uint64, // Attributes and flags of section
  addr      =  Ptr1,   // (virtual) address of section in memory
  offset    =  Ptr1,   // Offset of seaction in ELF executable file
  size      =  size_t, // Size of section in bytes
  link      =  uint,   // Extra informaion
  info      =  uint,   // Additional information
  addralign =  uint64, // Alignment requirements of section's address
  entsize   =  size_t 64  // Size of each entry in section
}

typedef boot_info_t = @{
  total_size = uint,    // total size of boot information 
  memory_map = memory_areas_t,
  elf_tag = elf_tag_t
}

vtypedef bootptr  = [l : agz] (boot_info_t@l , boot_info_t@l -<lin,prf> void | ptr l)

fun boot_info_init(p : Ptr1) : bootptr

fn get_memory_mappings_n {l : agz} (pf : !boot_info_t@l | p : ptr l) :<> [n:nat] size_t n
fn get_memory_mapping {l:agz} (pf : !boot_info_t @ l | p : ptr l, n : size_t) :<> memory_area_t
fn print_memory_mappings (p : !bootptr) : void // Print all available memory area's

fn get_elf_headers_n (p : !bootptr) : [n:nat] size_t n
fn get_elf_header  (p : !bootptr, n : size_t) : elf64_shdr_t
fn print_elf_headers (p : !bootptr) : void

fn get_kernel_ranges (p : !bootptr) : (Ptr,Ptr) // (kernel start, kernel end)
fn get_multiboot_ranges (p : !bootptr) : (Ptr0,Ptr0) // (bootinfo start, bootinfo end)

macdef invalid_area = @{
  base_addr = the_null_ptr,
  length = i2sz(1),
  type = 0u,
  reserved = 0u
}