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

typedef memory_entry_t = @{
  base_addr = Ptr1, // Start of physical address
  length = uint64,  // Size of memory region in bytes
  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_map_t = @{ 
    tag = tag_t,
    entry_size = [n : nat | n > 0 && n % 8 == 0] uint n,
    entry_version = uint,
    entries = ptr // Pointer to entries
} 


typedef boot_info_t = @{
  total_size = uint, // total size of boot information 
  memory_map = memory_map_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 (p : !bootptr) : [n:nat] size_t n
fn get_memory_mapping  (p : !bootptr, n : size_t) : memory_entry_t
fn print_memory_mappings (p : !bootptr) : void