1 files changed, 34 insertions, 0 deletions
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats
new file mode 100644
index 0000000..0507241
--- /dev/null
+++ b/kernel/bootinfo/multiboot.sats
@@ -0,0 +1,34 @@
+
+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