diff --git a/libs/trusted_chunk/.gitignore b/libs/trusted_chunk/.gitignore
new file mode 100644
index 0000000000..3df278ecee
--- /dev/null
+++ b/libs/trusted_chunk/.gitignore
@@ -0,0 +1,2 @@
+target
+.vscode
diff --git a/libs/trusted_chunk/Cargo.toml b/libs/trusted_chunk/Cargo.toml
new file mode 100644
index 0000000000..893fee1eaa
--- /dev/null
+++ b/libs/trusted_chunk/Cargo.toml
@@ -0,0 +1,14 @@
+[package]
+name = "trusted_chunk"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+prusti-contracts = "^0.1"
+cfg-if = "1.0.0"
+range_inclusive = {git = "https://github.com/Ramla-I/range_inclusive"}
+spin = "0.9.4"
+
+[features]
+default = []
+std = []
diff --git a/libs/trusted_chunk/README.md b/libs/trusted_chunk/README.md
new file mode 100644
index 0000000000..3b9970edf6
--- /dev/null
+++ b/libs/trusted_chunk/README.md
@@ -0,0 +1,22 @@
+# trusted_chunk
+This crate contains a TrustedChunk type with verified methods that prevent creating chunks with overlapping ranges.
+This is done by storing information about all previously created chunks in a verified bookkeeping data structure (an array before heap initialization and a linked list after). A TrustedChunkAllocator stores the bookkeeping structures and provides the only public interface to create a TrustedChunk. All chunks created from a single TrustedChunkAllocator instance do not overlap.
+
+## Running Prusti on this crate
+1. Download the pre-compiled binary for Release v-2023-01-26 from [here](https://github.com/viperproject/prusti-dev/releases/tag/v-2023-01-26-1935)
+2. Navigate to the prusti-release folder
+3. Run this command 
+```
+./prusti-rustc <path to trusted_chunk/src/lib.rs> -Pcheck_overflows=false --crate-type=lib --cfg "prusti" --cfg "std"
+```
+
+## Notes for Prusti improvements
+1. Eq, PartialEq, Ord, etc. traits should be pure by default
+2. Functions for structs with generics lead to internal compiler errors
+
+## Working with cargo-prusti
+We can also use the cargo-prusti tool by running it in the repo with the Cargo.toml file, and adding a Prusti.toml file with the prusti flags.
+We would also have to change the syntax for conditional compilation in the crate to [cfg(feature = "prusti")]
+```
+./<path>/cargo-prusti  --features prusti
+```
\ No newline at end of file
diff --git a/libs/trusted_chunk/src/external_spec/mod.rs b/libs/trusted_chunk/src/external_spec/mod.rs
new file mode 100644
index 0000000000..16c111fdaa
--- /dev/null
+++ b/libs/trusted_chunk/src/external_spec/mod.rs
@@ -0,0 +1,9 @@
+//! The external spec files are specifications of commonly used types like `Option`, `Vec` and `RangeInclusive`.
+//! We also provide helper functions to peek into the values of the `Result` and `Option` types to be used in specifications.
+//! The specs are simple and easy to understand, and only the subset of functions used in the verification are specified.
+//! It is expected that type definitions given here are only used during verification, and the actual crates will be used when running the application.
+//! For that, we use conditional compilation.
+
+pub(crate) mod trusted_range_inclusive;
+pub(crate) mod trusted_option;
+pub(crate) mod trusted_result;
diff --git a/libs/trusted_chunk/src/external_spec/trusted_option.rs b/libs/trusted_chunk/src/external_spec/trusted_option.rs
new file mode 100644
index 0000000000..acda565f5b
--- /dev/null
+++ b/libs/trusted_chunk/src/external_spec/trusted_option.rs
@@ -0,0 +1,55 @@
+//! The specification for the `Option` type and helper functions to peek the inner value.
+
+use prusti_contracts::*;
+use crate::external_spec::trusted_range_inclusive::*;
+
+#[extern_spec]
+impl<T: PartialEq + Copy> core::option::Option<T> {
+    #[pure]
+    #[ensures(matches!(*self, Some(_)) == result)]
+    pub fn is_some(&self) -> bool;
+
+    #[pure]
+    #[ensures(self.is_some() == !result)]
+    pub fn is_none(&self) -> bool;
+
+    #[requires(self.is_some())]
+    #[ensures(result == peek_option(&self))]
+    pub fn unwrap(self) -> T;
+
+    #[ensures(result.is_some() ==> (old(self.is_some()) && old(peek_option(&self)) == peek_option(&result)))]
+    #[ensures(result.is_none() ==> old(self.is_none()))]
+    pub fn take(&mut self) -> Option<T>;
+}
+
+#[extern_spec]
+impl<T: Copy + PartialEq> PartialEq for core::option::Option<T> {
+    #[pure]
+    #[ensures(self.is_none() && other.is_none() ==> result == true)]
+    #[ensures(self.is_none() && other.is_some() ==> result == false)]
+    #[ensures(self.is_some() && other.is_none() ==> result == false)]
+    #[ensures(self.is_some() && other.is_some() ==> {
+        let val1 = peek_option(&self);
+        let val2 = peek_option(&other);
+        result == (val1 == val2)
+    })]
+    fn eq(&self, other:&Self) -> bool;
+}
+
+#[pure]
+#[requires(val.is_some())]
+pub(crate) fn peek_option<T: Copy>(val: &Option<T>) -> T {
+    match val {
+        Some(val) => *val,
+        None => unreachable!(),
+    }
+}
+
+#[pure]
+#[requires(val.is_some())]
+pub(crate) fn peek_option_ref<T>(val: &Option<T>) -> &T {
+    match val {
+        Some(val) => val,
+        None => unreachable!(),
+    }
+}
diff --git a/libs/trusted_chunk/src/external_spec/trusted_range_inclusive.rs b/libs/trusted_chunk/src/external_spec/trusted_range_inclusive.rs
new file mode 100644
index 0000000000..72ec4582e5
--- /dev/null
+++ b/libs/trusted_chunk/src/external_spec/trusted_range_inclusive.rs
@@ -0,0 +1,34 @@
+//! A specification for `RangeInclusive` which is just an actual type definition and relevant functions.
+//! We don't use a Prusti external spec here because of dependency errors when using prusti-rustc (maybe due to a git path?) 
+//! and Prusti errors about the return types of pure functions and some "unexpected panics" when using cargo-prusti.
+
+use prusti_contracts::*;
+
+#[derive(Copy, Clone, PartialEq, Eq)]
+pub struct RangeInclusive<Idx: Clone + PartialOrd> {
+    start: Idx,
+    end: Idx
+}
+
+impl<Idx: Clone + PartialOrd> RangeInclusive<Idx> {
+    #[ensures(result.start == start)]
+    #[ensures(result.end == end)]
+    pub(crate) const fn new(start: Idx, end: Idx) -> Self {
+        Self{start, end}
+    }
+
+    #[pure]
+    pub const fn start(&self) -> &Idx {
+        &self.start
+    }
+
+    #[pure]
+    pub const fn end(&self) -> &Idx {
+        &self.end
+    }
+
+    pub fn is_empty(&self) -> bool {
+        !(self.start <= self.end)
+    }
+
+}
diff --git a/libs/trusted_chunk/src/external_spec/trusted_result.rs b/libs/trusted_chunk/src/external_spec/trusted_result.rs
new file mode 100644
index 0000000000..19f3e9053a
--- /dev/null
+++ b/libs/trusted_chunk/src/external_spec/trusted_result.rs
@@ -0,0 +1,40 @@
+//! Helper functions for `Result` to peek the inner value.
+//! We don't have to write an extern spec for `Result` because it's already in prusti_contracts.
+
+use prusti_contracts::*;
+
+#[pure]
+#[requires(val.is_ok())]
+pub(crate) fn peek_result<T: Copy, E>(val: &Result<T,E>) -> T {
+    match val {
+        Ok(val) => *val,
+        Err(_) => unreachable!(),
+    }
+}
+
+#[pure]
+#[requires(val.is_ok())]
+pub(crate) fn peek_result_ref<T, E>(val: &Result<T,E>) -> &T {
+    match val {
+        Ok(val) => val,
+        Err(_) => unreachable!(),
+    }
+}
+
+#[pure]
+#[requires(val.is_err())]
+pub(crate) fn peek_err<T, E: Copy>(val: &Result<T,E>) -> E {
+    match val {
+        Ok(_) => unreachable!(),
+        Err(e) => *e,
+    }
+}
+
+#[pure]
+#[requires(val.is_err())]
+pub(crate) fn peek_err_ref<T, E>(val: &Result<T,E>) -> &E {
+    match val {
+        Ok(_) => unreachable!(),
+        Err(e) => e,
+    }
+}
diff --git a/libs/trusted_chunk/src/lib.rs b/libs/trusted_chunk/src/lib.rs
new file mode 100644
index 0000000000..845f5a57f2
--- /dev/null
+++ b/libs/trusted_chunk/src/lib.rs
@@ -0,0 +1,49 @@
+#![cfg_attr(not(std), no_std)]
+#![feature(box_patterns)]
+#![allow(unused)]
+#![feature(step_trait)]
+#![feature(rustc_private)]
+
+#[macro_use]
+extern crate prusti_contracts;
+#[macro_use]
+extern crate cfg_if;
+extern crate core;
+
+pub(crate) mod spec;
+pub(crate) mod external_spec;
+pub mod linked_list;
+pub mod static_array;
+pub mod trusted_chunk;
+mod test;
+
+cfg_if::cfg_if! {
+if #[cfg(prusti)] {
+    use crate::external_spec::trusted_range_inclusive::*;
+} else {
+    extern crate alloc;
+    extern crate range_inclusive;
+    extern crate spin;
+    use range_inclusive::*;
+
+    static INIT: spin::Once<bool> = spin::Once::new();
+}
+}
+
+
+#[cfg(not(prusti))] // prusti can't reason about fn pointers
+pub fn init() -> Result<fn(RangeInclusive<usize>) -> trusted_chunk::TrustedChunk, &'static str> {
+    if INIT.is_completed() {
+        Err("Trusted Chunk has already been initialized and callback has been returned")
+    } else {
+        INIT.call_once(|| true);
+        Ok(create_from_unmapped)
+    }
+}
+
+#[requires(*frames.start() <= *frames.end())]
+#[ensures(result.start() == *frames.start())]
+#[ensures(result.end() == *frames.end())]
+fn create_from_unmapped(frames: RangeInclusive<usize>) -> trusted_chunk::TrustedChunk {
+    trusted_chunk::TrustedChunk::trusted_new(frames)
+}
diff --git a/libs/trusted_chunk/src/linked_list.rs b/libs/trusted_chunk/src/linked_list.rs
new file mode 100644
index 0000000000..1dd23f9360
--- /dev/null
+++ b/libs/trusted_chunk/src/linked_list.rs
@@ -0,0 +1,288 @@
+//! Most of the List code is adapted from the Prusti user guide 
+//! https://viperproject.github.io/prusti-dev/user-guide/tour/summary.html
+
+
+use prusti_contracts::*;
+
+#[cfg(prusti)]
+use crate::external_spec::trusted_range_inclusive::*;
+#[cfg(not(prusti))]
+use range_inclusive::*;
+#[cfg(not(prusti))]
+use alloc::boxed::Box;
+use crate::{
+    external_spec::{trusted_option::*, trusted_result::*},
+    spec::range_overlaps::*
+};
+use core::{mem, marker::Copy, ops::Deref};
+
+
+pub struct List {
+    head: Link,
+}
+
+pub(crate) enum Link {
+    Empty,
+    More(Box<Node>)
+}
+
+pub(crate) struct Node {
+    elem: RangeInclusive<usize>,
+    next: Link,
+}
+
+
+#[trusted]
+#[requires(src.is_empty())]
+#[ensures(dest.is_empty())]
+#[ensures(old(dest.len()) == result.len())]
+#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==> 
+                old(dest.lookup(i)) == result.lookup(i)))] 
+fn replace(dest: &mut Link, src: Link) -> Link {
+    mem::replace(dest, src)
+}
+
+
+impl List {
+
+    #[pure]
+    pub fn len(&self) -> usize {
+        self.head.len()
+    }
+
+    /// Looks up an element in the list.
+    /// 
+    /// # Pre-conditions:
+    /// * index is less than the length
+    #[pure]
+    #[requires(0 <= index && index < self.len())]
+    pub fn lookup(&self, index: usize) -> RangeInclusive<usize> {
+        self.head.lookup(index)
+    }
+
+    /// Creates an empty list.
+    /// 
+    /// # Post-conditions: 
+    /// * length is zero.
+    #[ensures(result.len() == 0)]
+    pub const fn new() -> Self {
+        List { head: Link::Empty }
+    }
+
+
+    /// Adds an element to the list.
+    /// 
+    /// # Post-conditions:
+    /// * new_length = old_length + 1
+    /// * `elem` is added at index 0
+    /// * all previous elements remain in the list, just moved one index forward
+    #[ensures(self.len() == old(self.len()) + 1)] 
+    #[ensures(self.lookup(0) == elem)]
+    #[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==> old(self.lookup(i-1)) == self.lookup(i)))]
+    pub fn push(&mut self, elem: RangeInclusive<usize>) {
+        let new_node = Box::new(Node {
+            elem: elem,
+            next: replace(&mut self.head, Link::Empty)
+        });
+
+        self.head = Link::More(new_node);
+    }
+
+
+    /// Adds `elem` to the list only if it doesn't overlap with any existing member of the list.
+    /// If it fails, then it returns the index of the element that overlaps with `elem`.
+    /// 
+    /// # Post-conditions:
+    /// * If the push fails, than the returned index is less than the list length
+    /// * If the push fails, then `elem` overlaps with the element at the returned index
+    /// * If the push succeeds, then new_length = old_length + 1
+    /// * If the push succeeds, then `elem` is added at index 0
+    /// * If the push succeeds, then all previous elements remain in the list, just moved one index forward
+    /// * If the push succeeds, then `elem` doesn't overlap with any other element in the list
+    #[ensures(result.is_err() ==> peek_err(&result) < self.len())]
+    #[ensures(result.is_err() ==> {
+            let idx = peek_err(&result);
+            let range = self.lookup(idx);
+            range_overlaps(&range, &elem)
+        }
+    )]
+    #[ensures(result.is_ok() ==> self.len() == old(self.len()) + 1)] 
+    #[ensures(result.is_ok() ==> self.lookup(0) == elem)]
+    #[ensures(result.is_ok() ==> forall(|i: usize| (1 <= i && i < self.len()) ==> old(self.lookup(i-1)) == self.lookup(i)))]
+    #[ensures(result.is_ok() ==> 
+        forall(|i: usize| (1 <= i && i < self.len()) ==> {
+            let range = self.lookup(i);
+            !range_overlaps(&range, &elem)
+        })
+    )]
+    pub fn push_unique(&mut self, elem: RangeInclusive<usize>) -> Result<(),usize> {
+        match self.elem_overlaps_in_list(elem, 0) {
+            Some(idx) => Err(idx),
+            None => {
+                let new_node = Box::new(Node {
+                    elem: elem,
+                    next: replace(&mut self.head, Link::Empty)
+                });
+                self.head = Link::More(new_node);
+                Ok(())
+            }
+        }
+    }
+
+
+    /// A push function that ensures there is no overlap of list elements, given that the list originally has no overlaps.
+    /// 
+    /// # Pre-conditions:
+    /// * list elements do not overlap
+    /// 
+    /// # Post-conditions:
+    /// * If the push fails, than the returned index is less than the list length
+    /// * If the push fails, then `elem` overlaps with the element at the returned index
+    /// * If the push succeeds, then new_length = old_length + 1
+    /// * If the push succeeds, then `elem` is added at index 0
+    /// * If the push succeeds, then all previous elements remain in the list, just moved one index forward
+    /// * If the push succeeds, then list elements do not overlap
+    #[requires(forall(|i: usize, j: usize| (0 <= i && i < self.len() && 0 <= j && j < self.len()) ==> 
+        (i != j ==> !range_overlaps(&self.lookup(i), &self.lookup(j))))
+    )]
+    #[ensures(result.is_err() ==> peek_err(&result) < self.len())]
+    #[ensures(result.is_err() ==> {
+            let idx = peek_err(&result);
+            let range = self.lookup(idx);
+            range_overlaps(&range, &elem)
+        }
+    )]
+    #[ensures(result.is_ok() ==> self.len() == old(self.len()) + 1)] 
+    #[ensures(result.is_ok() ==> self.lookup(0) == elem)]
+    #[ensures(result.is_ok() ==> forall(|i: usize| (1 <= i && i < self.len()) ==> old(self.lookup(i-1)) == self.lookup(i)))]
+    #[ensures(forall(|i: usize, j: usize| (0 <= i && i < self.len() && 0 <= j && j < self.len()) ==> 
+        (i != j ==> !range_overlaps(&self.lookup(i),&self.lookup(j))))
+    )]
+    pub fn push_unique_with_precond(&mut self, elem: RangeInclusive<usize>) -> Result<(),usize> {
+        match self.elem_overlaps_in_list(elem, 0) {
+            Some(idx) => Err(idx),
+            None => {
+                let new_node = Box::new(Node {
+                    elem: elem,
+                    next: replace(&mut self.head, Link::Empty)
+                });
+                self.head = Link::More(new_node);
+                Ok(())
+            }
+        }
+    }
+
+    
+    /// Removes element at index 0 from the list.
+    /// 
+    /// Post-conditions:
+    /// * if the list is empty, returns None.
+    /// * if the list is not empty, returns Some().
+    /// * if the list is empty, the length remains 0.
+    /// * if the list is not empty, new_length = old_length - 1
+    /// * if the list is not empty, the returned element was previously at index 0
+    /// * if the list is not empty, all elements in the old list at index [1..] are still in the list, except at one index less.
+    #[ensures(old(self.len()) == 0 ==> result.is_none())]
+    #[ensures(old(self.len()) > 0 ==> result.is_some())]
+    #[ensures(old(self.len()) == 0 ==> self.len() == 0)]
+    #[ensures(old(self.len()) > 0 ==> self.len() == old(self.len()-1))]
+    #[ensures(old(self.len()) > 0 ==> *peek_option_ref(&result) == old(self.lookup(0)))]
+    #[ensures(old(self.len()) > 0 ==>
+        forall(|i: usize| (0 <= i && i < self.len()) ==> old(self.lookup(i+1)) == self.lookup(i))
+    )]
+    pub fn pop(&mut self) -> Option<RangeInclusive<usize>> {
+        match replace(&mut self.head, Link::Empty) {
+            Link::Empty => {
+                None
+            }
+            Link::More(node) => {
+                self.head = node.next;
+                Some(node.elem)
+            }
+        }
+    }
+
+
+    /// Returns the index of the first element in the list, starting from `index`, which overlaps with `elem`.
+    /// Returns None if there is no overlap.
+    /// 
+    /// # Pre-conditions:
+    /// * index is less than or equal to the list length
+    /// 
+    /// # Post-conditions:
+    /// * if the result is Some(idx), then idx is less than the list's length.
+    /// * if the result is Some(idx), then the element at idx overlaps with `elem`
+    /// * if the result is None, then no element in the lists overlaps with `elem`
+    #[requires(0 <= index && index <= self.len())]
+    #[ensures(result.is_some() ==> peek_option(&result) < self.len())]
+    #[ensures(result.is_some() ==> {
+            let idx = peek_option(&result);
+            let range = self.lookup(idx);
+            range_overlaps(&range, &elem)
+        }
+    )]
+    #[ensures(result.is_none() ==> 
+        forall(|i: usize| (index <= i && i < self.len()) ==> {
+            let range = self.lookup(i);
+            !range_overlaps(&range, &elem)
+        })
+    )]
+    pub(crate) fn elem_overlaps_in_list(&self, elem: RangeInclusive<usize>, index: usize) -> Option<usize> {
+        if index == self.len() {
+            return None;
+        }
+        let ret = if range_overlaps(&self.lookup(index),&elem) {
+            Some(index)
+        } else {
+            self.elem_overlaps_in_list(elem, index + 1)
+        };
+        ret
+    }
+
+}
+
+impl Link {
+
+    /// Recursive function that returns length of the list starting from this Link/ Node
+    /// 
+    /// # Post-conditions:
+    /// * returns 0 if the link is empty
+    /// * returns >0 if the link is not empty
+    #[pure]
+    #[ensures(self.is_empty() ==> result == 0)]
+    #[ensures(!self.is_empty() ==> result > 0)]
+    fn len(&self) -> usize {
+        match self {
+            Link::Empty => 0,
+            Link::More(box node) => 1 + node.next.len(),
+        }
+    }
+
+    #[pure]
+    fn is_empty(&self) -> bool {
+        match self {
+            Link::Empty => true,
+            Link::More(box node) => false,
+        }
+    }
+
+    /// Recursive function that returns the element at the given `index`.
+    /// 
+    /// # Pre-conditions:
+    /// * `index` is less than the list length
+    #[pure]
+    #[requires(0 <= index && index < self.len())]
+    pub fn lookup(&self, index: usize) -> RangeInclusive<usize> {
+        match self {
+            Link::Empty => unreachable!(),
+            Link::More(box node) => {
+                if index == 0 {
+                    node.elem
+                } else {
+                    node.next.lookup(index - 1)
+                }
+            }
+        }
+    }
+
+}
diff --git a/libs/trusted_chunk/src/spec/chunk_spec.rs b/libs/trusted_chunk/src/spec/chunk_spec.rs
new file mode 100644
index 0000000000..9c2e4fb8c6
--- /dev/null
+++ b/libs/trusted_chunk/src/spec/chunk_spec.rs
@@ -0,0 +1,127 @@
+//! The following are a set of pure functions that are only used in the specification of a `TrustedChunk`.
+
+use crate::trusted_chunk::*;
+use crate::external_spec::trusted_option::*;
+
+/// Checks that either `chunk1` ends before `chunk2` starts, or that `chunk2` ends before `chunk1` starts.
+/// 
+/// # Pre-conditions:
+/// * `chunk1` and `chunk2` are not empty
+#[pure]
+#[requires(!chunk1.is_empty())]
+#[requires(!chunk2.is_empty())]
+pub(crate) fn chunks_do_not_overlap(chunk1: &TrustedChunk, chunk2: &TrustedChunk) -> bool {
+    (chunk1.end() < chunk2.start()) | (chunk2.end() < chunk1.start())
+}
+
+/// Returns true if there is no overlap in the ranges of `chunk1`, `chunk2` and `chunk3`.
+/// 
+/// # Pre-conditions:
+/// * chunks are not empty
+#[pure]
+#[requires(chunk1.is_some() ==> !peek_option_ref(&chunk1).is_empty())]
+#[requires(!chunk2.is_empty())]
+#[requires(chunk3.is_some() ==> !peek_option_ref(&chunk3).is_empty())]
+pub(crate) fn split_chunk_has_no_overlapping_ranges(chunk1: &Option<TrustedChunk>, chunk2: &TrustedChunk, chunk3: &Option<TrustedChunk>) -> bool {
+    let mut no_overlap = true;
+
+    if let Some(c1) = chunk1 {
+        no_overlap &= chunks_do_not_overlap(c1, chunk2);
+        if let Some(c3) = chunk3 {
+            no_overlap &= chunks_do_not_overlap(c1, c3);
+            no_overlap &= chunks_do_not_overlap(chunk2, c3);
+        }
+    } else {
+        if let Some(c3) = chunk3 {
+            no_overlap &= chunks_do_not_overlap(chunk2, c3);
+        }
+    }
+
+    no_overlap
+}
+
+/// Returns true if the start and end of the original chunk is equal to the extreme bounds of the split chunk.
+/// 
+/// # Pre-conditions:
+/// * chunks are not empty
+#[pure]
+#[requires(!orig_chunk.is_empty())]
+#[requires(split_chunk.0.is_some() ==> !peek_option_ref(&split_chunk.0).is_empty())]
+#[requires(!split_chunk.1.is_empty())]
+#[requires(split_chunk.2.is_some() ==> !peek_option_ref(&split_chunk.2).is_empty())]
+pub(crate) fn split_chunk_has_same_range(orig_chunk: &TrustedChunk, split_chunk: &(Option<TrustedChunk>, TrustedChunk, Option<TrustedChunk>)) -> bool {
+    let (chunk1,chunk2,chunk3) = split_chunk;
+    let min_page;
+    let max_page;
+
+    if let Some(c1) = chunk1 {
+        min_page = c1.start();    
+    } else {
+        min_page = chunk2.start();
+    }
+
+    if let Some(c3) = chunk3 {
+        max_page = c3.end();    
+    } else {
+        max_page = chunk2.end();
+    }
+
+    min_page == orig_chunk.start() && max_page == orig_chunk.end()
+}
+
+
+/// Returns true if `chunk1`, `chunk2` and `chunk3` are contiguous.
+/// 
+/// # Pre-conditions:
+/// * chunks are not empty
+#[pure]
+// #[requires(end_frame_is_less_than_max_or_none(chunk1))] //only required if CHECK_OVERFLOWS flag is enabled
+// #[requires(end_frame_is_less_than_max(chunk2))] //only required if CHECK_OVERFLOWS flag is enabled
+// #[requires(end_frame_is_less_than_max_or_none(chunk3))] //only required if CHECK_OVERFLOWS flag is enabled
+#[requires(chunk1.is_some() ==> peek_option_ref(&chunk1).start() <= peek_option_ref(&chunk1).end())]
+#[requires(chunk2.start() <= chunk2.end())]
+#[requires(chunk3.is_some() ==> peek_option_ref(&chunk3).start() <= peek_option_ref(&chunk3).end())]
+pub(crate) fn split_chunk_is_contiguous(chunk1: &Option<TrustedChunk>, chunk2: &TrustedChunk, chunk3: &Option<TrustedChunk>) -> bool {
+    let mut contiguous = true;
+    if let Some(c1) = chunk1 {
+        contiguous &= c1.end() + 1 == chunk2.start()
+    } 
+    if let Some(c3) = chunk3 {
+        contiguous &= chunk2.end() + 1 == c3.start()
+    }
+    contiguous
+}
+
+
+/*** Constants taken from kernel_config crate. Only required if CHECK_OVERFLOWS flag is enabled. ***/ 
+/// The lower 12 bits of a virtual address correspond to the P1 page frame offset. 
+pub const PAGE_SHIFT: usize = 12;
+/// Page size is 4096 bytes, 4KiB pages.
+pub const PAGE_SIZE: usize = 1 << PAGE_SHIFT;
+pub const MAX_VIRTUAL_ADDRESS: usize = usize::MAX;
+pub const MAX_PAGE_NUMBER: usize = MAX_VIRTUAL_ADDRESS / PAGE_SIZE;
+
+/// Returns true if the end frame of the chunk is less than `MAX_PAGE_NUMBER`, or if the chunk is None.
+#[pure]
+pub(crate) fn end_frame_is_less_than_max_or_none(chunk: &Option<TrustedChunk>) -> bool {
+    if let Some(c) = chunk {
+        if c.end() <= MAX_PAGE_NUMBER {
+            return true;
+        } else {
+            return false;
+        }
+    } else {
+        return true;
+    }
+
+}
+
+/// Returns true if the end frame of the chunk is less than `MAX_PAGE_NUMBER`.
+#[pure]
+pub(crate) fn end_frame_is_less_than_max(chunk: &TrustedChunk) -> bool {
+    if chunk.end() <= MAX_PAGE_NUMBER {
+        return true;
+    } else {
+        return false;
+    }
+}
diff --git a/libs/trusted_chunk/src/spec/mod.rs b/libs/trusted_chunk/src/spec/mod.rs
new file mode 100644
index 0000000000..db455e1ed5
--- /dev/null
+++ b/libs/trusted_chunk/src/spec/mod.rs
@@ -0,0 +1,5 @@
+//! The spec files are functions that can be used within both specifications and code.
+//! They are used to help define what functional correctness means in this system.
+
+pub(crate) mod range_overlaps;
+pub(crate) mod chunk_spec;
diff --git a/libs/trusted_chunk/src/spec/range_overlaps.rs b/libs/trusted_chunk/src/spec/range_overlaps.rs
new file mode 100644
index 0000000000..088f44a899
--- /dev/null
+++ b/libs/trusted_chunk/src/spec/range_overlaps.rs
@@ -0,0 +1,152 @@
+//! This function defines what it means for two RangeInclusives to overlap. 
+//! It is used in both the implementation and specification.
+//! If this definition of overlapping doesn't match what the rest of the system expects, then the results of verification won't make sense.
+
+use prusti_contracts::*;
+
+#[cfg(prusti)]
+use crate::external_spec::trusted_range_inclusive::*;
+#[cfg(not(prusti))]
+use range_inclusive::*;
+
+use core::cmp::{max,min};
+
+
+/// Returns false if either of `range1` or `range2` are empty, or if there is no overlap.
+/// Returns true otherwise.
+/// 
+/// # Verification Notes:
+/// * Removing the trusted marking leads to "unexpected internal errors", I think because of issues with generics in RangeInclusive.
+/// * To make sure the post-conditions are valid, I implemented a range_overlaps_check function (EOF) which is identical except
+/// it works with a Range type without generics, and it verifies.
+#[pure]
+#[trusted] // Only trusted functions can call themselves in their contracts
+#[ensures(!result ==> (
+    *range1.start() > *range1.end() ||
+    *range2.start() > *range2.end() ||
+    (*range1.start() <= *range1.end() && *range2.start() <= *range2.end() && (*range2.start() > *range1.end() || *range1.start() > *range2.end()))
+))]
+#[ensures(result ==> (*range2.start() <= *range1.end() || *range1.start() <= *range2.end()))]
+#[ensures(result ==> range_overlaps(range2, range1))]
+pub fn range_overlaps(range1: &RangeInclusive<usize>, range2: &RangeInclusive<usize>) -> bool {
+    if range1.is_empty() || range2.is_empty() {
+        return false;
+    }
+
+    let starts = max(range1.start(), range2.start());
+    let ends = min(range1.end(), range2.end());
+    starts <= ends
+}
+
+
+
+#[cfg(test)]
+mod test {
+    use range_inclusive::RangeInclusive;
+
+    use super::range_overlaps;
+
+    #[test]
+    fn overlapping() {
+        let r1 = RangeInclusive::new(0,5);
+        let r2 = RangeInclusive::new(4, 7);
+        assert!(range_overlaps(&r1, &r2));
+
+        let r1 = RangeInclusive::new(0,5);
+        let r2 = RangeInclusive::new(5, 5);
+        assert!(range_overlaps(&r1, &r2));
+    }
+
+    #[test]
+    fn not_overlapping() {
+        // empty ranges
+        let r1 = RangeInclusive::new(5,0);
+        let r2 = RangeInclusive::new(4, 7);
+        assert!(!range_overlaps(&r1, &r2));
+
+        // empty ranges
+        let r1 = RangeInclusive::new(5,5);
+        let r2 = RangeInclusive::new(6, 5);
+        assert!(!range_overlaps(&r1, &r2));
+
+        let r1 = RangeInclusive::new(3,5);
+        let r2 = RangeInclusive::new(6, 7);
+        assert!(!range_overlaps(&r1, &r2));
+    }
+
+}
+
+
+
+// #[pure]
+// #[trusted]
+// #[ensures(result ==> range_overlaps(range2, range1))]
+// pub fn range_overlaps<Idx: Clone + PartialOrd + Ord>(range1: &RangeInclusive<Idx>, range2: &RangeInclusive<Idx>) -> bool {
+//     if range1.is_empty() || range2.is_empty() {
+//         return false;
+//     }
+
+//     let starts = if range1.start() >= range2.start() {
+//         range1.start()
+//     } else {
+//         range2.start()
+//     };
+
+//     let ends = if range1.end() <= range2.end() {
+//         range1.end()
+//     } else {
+//         range2.end()
+//     };
+
+//     starts <= ends
+// }
+
+
+
+// *** Code below is a sanity check to make sure our trusted function for range_overlaps is correct ***//
+// struct Range {
+//     start: usize,
+//     end: usize
+// }
+
+// impl Range {
+//     #[pure]
+//     fn start(&self) -> usize {
+//         self.start
+//     }
+//     #[pure]
+//     fn end(&self) -> usize {
+//         self.end
+//     }
+//     #[pure]
+//     fn is_empty(&self) -> bool {
+//         !(self.start <= self.end)
+//     }
+// }
+
+// #[pure]
+// #[ensures(!result ==> (
+//     range1.start() > range1.end() ||
+//     range2.start() > range2.end() ||
+//     (range1.start() <= range1.end() && range2.start() <= range2.end() && (range2.start() > range1.end() || range1.start() > range2.end()))
+// ))]
+// #[ensures(result ==> (range2.start() <= range1.end() || range1.start() <= range2.end()))]
+// fn range_overlaps_check(range1: &Range, range2: &Range) -> bool {
+//     if range1.is_empty() || range2.is_empty() {
+//         return false;
+//     }
+
+//     let starts = max_usize(range1.start(), range2.start());
+//     let ends = min_usize(range1.end(), range2.end());
+//     starts <= ends
+// }
+
+// #[pure]
+// fn max_usize(a: usize, b: usize) -> usize {
+//     if a >= b { a } else { b }
+// }
+
+// #[pure]
+// fn min_usize(a: usize, b: usize) -> usize {
+//     if a <= b { a } else { b }
+// }
diff --git a/libs/trusted_chunk/src/static_array.rs b/libs/trusted_chunk/src/static_array.rs
new file mode 100644
index 0000000000..bba6346c65
--- /dev/null
+++ b/libs/trusted_chunk/src/static_array.rs
@@ -0,0 +1,190 @@
+use prusti_contracts::*;
+
+#[cfg(prusti)]
+use crate::external_spec::trusted_range_inclusive::*;
+#[cfg(not(prusti))]
+use range_inclusive::*;
+
+use crate::{
+    external_spec::{trusted_option::*, trusted_result::*},
+    spec::range_overlaps::*
+};
+use core::mem;
+
+pub struct StaticArray  {
+    pub(crate) arr: [Option<RangeInclusive<usize>>; 64] // only public so it can be used in spec
+}
+
+impl StaticArray {
+    pub const fn new() -> Self {
+        StaticArray {
+            arr: [None; 64]
+        }
+    }
+
+    #[pure]
+    #[ensures(result == self.arr.len())]
+    pub const fn len(&self) -> usize {
+        self.arr.len()
+    }
+
+    /// Looks up an element in the array.
+    /// 
+    /// # Pre-conditions:
+    /// * index is less than the length
+    #[pure]
+    #[requires(0 <= index && index < self.len())]
+    #[ensures(result == self.arr[index])]
+    pub fn lookup(&self, index: usize) -> Option<RangeInclusive<usize>> {
+        self.arr[index]
+    }
+
+    // /// Sets the the element at `index` with the value `elem`.
+    // /// 
+    // /// # Pre-conditions:
+    // /// * Index is less than the length
+    // /// 
+    // /// # Post-conditions:
+    // /// * The element at `index` is equal to `elem`
+    // /// * All other elements not at `index` remain unchanged
+    // #[requires(0 <= index && index < self.len())]
+    // #[ensures(self.arr[index] == elem)]
+    // #[ensures(forall(|i: usize| ((0 <= i && i < self.arr.len()) && i != index) ==> self.arr[i] == old(self.arr[i])))]
+    // pub(crate) fn set_element(&mut self, index: usize, elem: Option<RangeInclusive<usize>>) {
+    //     self.arr[index] = elem;
+    // }
+
+
+    // /// Looks up an element in the array and returns its start and end value.
+    // /// This has to be trusted because we access the RangeInclusive start and end values
+    // /// which we've already seen leads to internal compiler errors due to generics.
+    // /// 
+    // /// # Pre-conditions:
+    // /// * Index is less than the length
+    // /// 
+    // /// # Post-conditions:
+    // /// * The returned values are the start and end of the RangeInclusive at `index`
+    // /// * If there is no element at `index`, then None is returned
+    // #[pure]
+    // #[trusted]
+    // #[requires(0 <= index && index < self.len())]
+    // #[ensures(result.is_some() ==> 
+    //     self.arr[index].is_some() && 
+    //     *peek_option(&self.arr[index]).start() == peek_option(&result).0 && 
+    //     *peek_option(&self.arr[index]).end() == peek_option(&result).1
+    // )]
+    // #[ensures(result.is_none() ==> self.arr[index].is_none())]
+    // pub fn lookup_range_bounds(&self, index: usize) -> Option<((usize, usize))> {
+    //     match self.arr[index] {
+    //         Some(val) => Some((*val.start(), *val.end())),
+    //         None => None
+    //     }
+    // }
+
+
+    /// Adds an element to the array if there's space.
+    /// 
+    /// # Pre-conditions:
+    /// * The array is ordered so that all Some(_) elements occur at the beginning of the array, followed by all None elements.
+    ///
+    /// # Post-conditions:
+    /// * If the push fails, then all elements remain unchanged
+    /// * If the push fails, then all elements were Some(_)
+    /// * If the push succeeds, then the element at the returned index is now Some(_)
+    /// * If the push succeeds, then the element at the returned index is equal to `value`
+    /// * If the push succeeds, then all the elements are unchanged except at the returned index 
+    /// * If successful, then the array remains ordered with all Some elements followed by all None elements
+    #[requires(forall(|i: usize| (0 <= i && i < self.arr.len() && self.arr[i].is_some()) ==> {
+        forall(|j: usize| (0 <= j && j < i) ==> self.arr[j].is_some())
+    }))]
+    #[requires(forall(|i: usize| (0 <= i && i < self.arr.len() && self.arr[i].is_none()) ==> {
+        forall(|j: usize| (i <= j && j < self.arr.len()) ==> self.arr[j].is_none())
+    }))]
+    #[ensures(result.is_err() ==> 
+        forall(|i: usize| (0 <= i && i < self.arr.len()) ==> old(self.arr[i]) == self.arr[i])
+    )]
+    #[ensures(result.is_err() ==> 
+        forall(|i: usize| (0 <= i && i < self.arr.len()) ==> self.arr[i].is_some())
+    )]
+    #[ensures(result.is_ok() ==> {
+        let idx = peek_result(&result);
+        self.arr[idx].is_some()
+    })]
+    #[ensures(result.is_ok() ==> {
+        let idx = peek_result(&result);
+        let val = peek_option(&self.arr[idx]);
+        val == value
+    })]
+    #[ensures(result.is_ok() ==> 
+        forall(|i: usize| ((0 <= i && i < self.arr.len()) && (i != peek_result(&result))) ==> old(self.arr[i]) == self.arr[i])
+    )] 
+    #[ensures(forall(|i: usize| (0 <= i && i < self.arr.len() && self.arr[i].is_some()) ==> {
+        forall(|j: usize| (0 <= j && j < i) ==> self.arr[j].is_some())
+    }))]
+    #[ensures(forall(|i: usize| (0 <= i && i < self.arr.len() && self.arr[i].is_none()) ==> {
+        forall(|j: usize| (i <= j && j < self.arr.len()) ==> self.arr[j].is_none())
+    }))]
+	pub(crate) fn push(&mut self, value: RangeInclusive<usize>) -> Result<usize,()> {
+        let mut i = 0;
+
+        while i < self.arr.len() {
+            body_invariant!(forall(|j: usize| ((0 <= j && j < i) ==> self.arr[j].is_some())));
+            body_invariant!(i < self.arr.len());
+            body_invariant!(i >= 0);
+
+            if self.arr[i].is_none() {
+                self.arr[i] = Some(value);
+                return Ok(i)
+            }
+            i += 1;
+        }
+        return Err(());
+	}
+
+
+    /// Returns the index of the first element in the array, starting from `index`, which overlaps with `elem`.
+    /// Returns None if there is no overlap.
+    ///  
+    /// # Pre-conditions:
+    /// * index is less than or equal to the array length
+    /// 
+    /// # Post-conditions:
+    /// * if the result is Some(idx), then idx is less than the list's length.
+    /// * if the result is Some(idx), then the element at idx is Some(_)
+    /// * if the result is Some(idx), then the element at idx overlaps with `elem`
+    /// * if the result is None, then no element in the array overlaps with `elem`
+    #[requires(0 <= index && index <= self.arr.len())]
+    #[ensures(result.is_some() ==> peek_option(&result) < self.arr.len())]
+    #[ensures(result.is_some() ==> self.arr[peek_option(&result)].is_some())]
+    #[ensures(result.is_some() ==> {
+            let idx = peek_option(&result);
+            let range = peek_option(&self.arr[idx]);
+            range_overlaps(&range, &elem)
+        }
+    )]
+    #[ensures(result.is_none() ==> 
+        forall(|i: usize| ((index <= i && i < self.arr.len()) && self.arr[i].is_some()) ==> {
+            let range = peek_option(&self.arr[i]);
+            !range_overlaps(&range, &elem)
+        })
+    )]
+    pub(crate) fn elem_overlaps_in_array(&self, elem: RangeInclusive<usize>, index: usize) -> Option<usize> {
+        if index == self.arr.len() {
+            return None;
+        }
+
+        let ret = match self.arr[index] {
+            Some(val) => {
+                if range_overlaps(&val,&elem) {
+                    Some(index)
+                } else {
+                    self.elem_overlaps_in_array(elem, index + 1)
+                }
+            },
+            None => {
+                self.elem_overlaps_in_array(elem, index + 1)
+            }
+        };
+        ret
+    }
+}
diff --git a/libs/trusted_chunk/src/test.rs b/libs/trusted_chunk/src/test.rs
new file mode 100644
index 0000000000..213fcaeb98
--- /dev/null
+++ b/libs/trusted_chunk/src/test.rs
@@ -0,0 +1,60 @@
+use crate::*;
+use crate::trusted_chunk::*;
+
+#[test]
+fn chunk_allocator_test() {
+    let mut allocator = TrustedChunkAllocator::new();
+    let mut chunk;
+    chunk = allocator.create_chunk(RangeInclusive::new(0,1));
+    assert!(chunk.is_ok());
+    chunk = allocator.create_chunk(RangeInclusive::new(0,1)); // equivalent
+    assert!(chunk.is_err());
+    chunk = allocator.create_chunk(RangeInclusive::new(5,1)); // empty range
+    assert!(chunk.is_err());
+    chunk = allocator.create_chunk(RangeInclusive::new(4,10)); // disjoint
+    assert!(chunk.is_ok());
+    chunk = allocator.create_chunk(RangeInclusive::new(10,12)); // upper range bound overlap
+    assert!(chunk.is_err());
+    chunk = allocator.create_chunk(RangeInclusive::new(3,4)); // lower range bound overlap
+    assert!(chunk.is_err());
+
+    assert_eq!(allocator.array.lookup(0), Some(RangeInclusive::new(0,1)));
+    assert_eq!(allocator.array.lookup(1), Some(RangeInclusive::new(4,10)));
+
+    for i in 2..allocator.array.len() {
+        assert_eq!(allocator.array.lookup(i), None);
+    }
+
+    let res = allocator.switch_to_heap_allocated();
+    assert!(res.is_ok());
+
+    let res = allocator.switch_to_heap_allocated();
+    assert!(res.is_err());
+
+    // for i in 0..allocator.array.len() {
+    //     assert_eq!(allocator.array.lookup(i), None);
+    // }
+
+    assert_eq!(allocator.list.len(), 2);
+    assert_eq!(allocator.list.lookup(1), RangeInclusive::new(0,1));
+    assert_eq!(allocator.list.lookup(0), RangeInclusive::new(4,10));
+
+    chunk = allocator.create_chunk(RangeInclusive::new(7,12)); // multiple overlap
+    assert!(chunk.is_err());
+    chunk = allocator.create_chunk(RangeInclusive::new(10, 11)); // start range bound overlap
+    assert!(chunk.is_err());
+    chunk = allocator.create_chunk(RangeInclusive::new(11, 11));
+    assert!(chunk.is_ok());
+    chunk = allocator.create_chunk(RangeInclusive::new(11, 15)); // end range bound overlap
+    assert!(chunk.is_err());
+    chunk = allocator.create_chunk(RangeInclusive::new(1, 0)); // empty
+    assert!(chunk.is_err());
+    chunk = allocator.create_chunk(RangeInclusive::new(12, 15));
+    assert!(chunk.is_ok());
+
+    assert_eq!(allocator.list.len(), 4);
+    assert_eq!(allocator.list.lookup(3), RangeInclusive::new(0,1));
+    assert_eq!(allocator.list.lookup(2), RangeInclusive::new(4,10));
+    assert_eq!(allocator.list.lookup(1), RangeInclusive::new(11,11));
+    assert_eq!(allocator.list.lookup(0), RangeInclusive::new(12,15));
+}
diff --git a/libs/trusted_chunk/src/trusted_chunk.rs b/libs/trusted_chunk/src/trusted_chunk.rs
new file mode 100644
index 0000000000..69306f7294
--- /dev/null
+++ b/libs/trusted_chunk/src/trusted_chunk.rs
@@ -0,0 +1,498 @@
+use prusti_contracts::*;
+
+#[cfg(prusti)]
+use crate::external_spec::trusted_range_inclusive::*;
+#[cfg(not(prusti))]
+use range_inclusive::*;
+
+use core::ops::{Deref, DerefMut};
+use crate::{
+    *,
+    external_spec::{trusted_option::*, trusted_result::*},
+    spec::{range_overlaps::range_overlaps, chunk_spec::*},
+    linked_list::*, 
+    static_array::*,
+};
+
+
+#[derive(Copy, Clone)]
+#[cfg_attr(not(prusti), derive(Debug))]
+pub enum ChunkCreationError {
+    /// There was already a `TrustedChunk` created with an overlapping range
+    Overlap(usize),
+    /// In the pre-heap-intialization phase, if there is no more space in the array
+    NoSpace,
+    /// The requested range is empty (end > start)
+    InvalidRange
+}
+
+/// An allocator that allocates `TrustedChunk` objects with the invariant that all 
+/// chunks from this allocator are unique (there is no overlap in the ranges of the chunks).
+/// 
+/// Pre-heap initialization, the allocator keeps an array to store information about all the chunks created so far.
+/// After the heap is initialized, the ranges stored in `array` are shifted to a linked list and the 
+/// linked list is used to bookkeep all further allocations.
+pub struct TrustedChunkAllocator {
+    pub(crate) heap_init: bool,
+    pub(crate) list: List,
+    pub(crate) array: StaticArray
+}
+
+impl TrustedChunkAllocator {
+    /// Creates an allocator with empty bookkeeping structures
+    pub const fn new() -> TrustedChunkAllocator {
+        TrustedChunkAllocator { heap_init: false, list: List::new(), array: StaticArray::new() }
+    }
+
+
+    /// Shifts all elements in `array` to the heap-allocated `list`.
+    /// Returns an error if the heap was already initialized and the transfer has already occured.
+    /// 
+    /// # Pre-conditions:
+    /// * The `array` is ordered so that all Some(_) elements occur at the beginning of the array, followed by all None elements.
+    /// This pre-condtion is required so that we can relate each element in the old `array` with elements in the updated `list` in the post-conditions.
+    /// Since this is a public function, the  SMT solver cannot check that the pre-condition is valid, so we use the type system. 
+    /// The only exposed function to modify the array is the StaticArray::push() function which has this 
+    /// invariant as both a pre and post condition. So everytime we add an element to an array this pre-condition is upheld.
+    /// 
+    /// # Post-conditions:
+    /// * If `heap_init` was set or the `list` was not empty, then an error is returned
+    /// * If successful, `heap_init` is set
+    /// * If successful, then no element in `list` overlaps
+    /// * If successful, then the length of the list <= length of the array
+    /// * If successful, then each element in the list was originally present in the array
+    #[requires(forall(|i: usize| (0 <= i && i < self.array.len() && self.array.arr[i].is_some()) ==> {
+        forall(|j: usize| (0 <= j && j < i) ==> self.array.arr[j].is_some())
+    }))]
+    #[requires(forall(|i: usize| (0 <= i && i < self.array.len() && self.array.arr[i].is_none()) ==> {
+        forall(|j: usize| (i <= j && j < self.array.arr.len()) ==> self.array.arr[j].is_none())
+    }))]
+    #[ensures((old(self.heap_init) || old(self.list.len() != 0)) ==> result.is_err())]
+    #[ensures(result.is_ok() ==> self.heap_init)]
+    #[ensures(result.is_ok() ==> forall(|i: usize, j: usize| (0 <= i && i < self.list.len() && 0 <= j && j < self.list.len()) ==> 
+        (i != j ==> !range_overlaps(&self.list.lookup(i), &self.list.lookup(j))))
+    )]
+    #[ensures(result.is_ok() ==> self.list.len() <= self.array.len())]
+    #[ensures(result.is_ok() ==>  forall(|i: usize| (0 <= i && i < self.list.len()) ==> peek_option(&self.array.arr[i]) == self.list.lookup(self.list.len() - 1 - i)))]
+    // #[ensures(forall(|i: usize| (self.list.len() <= i && i < self.array.arr.len()) ==> self.array.arr[i].is_none()))]
+    pub fn switch_to_heap_allocated(&mut self) -> Result<(),()> {
+        if self.heap_init || self.list.len() != 0 {
+            return Err(());
+        }
+
+        let mut i = 0;
+        while i < self.array.arr.len() {
+            body_invariant!(self.list.len() <= self.array.len());
+            body_invariant!(self.list.len() == i);
+            body_invariant!(forall(|j: usize| ((0 <= j && j < self.list.len()) ==> self.array.arr[j].is_some())));
+            body_invariant!(forall(|j: usize| ((0 <= j && j < self.list.len()) ==> peek_option(&self.array.arr[j]) == self.list.lookup(self.list.len() - 1 - j))));
+            body_invariant!(forall(|i: usize, j: usize| (0 <= i && i < self.list.len() && 0 <= j && j < self.list.len()) ==> 
+                (i != j ==> !range_overlaps(&self.list.lookup(i), &self.list.lookup(j))))
+            );
+            body_invariant!(i < self.array.arr.len());
+            body_invariant!(i >= 0);
+
+            if let Some(range) = self.array.lookup(i) {
+                match self.list.push_unique_with_precond(range) {
+                    Ok(()) => (),
+                    Err(_) => return Err(())
+                }
+            } else {
+                break;
+            }
+
+            i += 1;
+        }
+        self.heap_init = true;
+        Ok(())
+    }
+
+
+    /// The only public interface to create a `TrustedChunk`.
+    /// 
+    /// # Pre-conditions:
+    /// * The `array` is ordered so that all Some(_) elements occur at the beginning of the array, followed by all None elements.
+    /// This pre-condtion is required so that we can relate each element in the old `array` with elements in the updated `list` when we start using the heap.
+    /// Since this is a public function, the  SMT solver cannot check that the pre-condition is valid, so we use the type system. 
+    /// The only exposed function to modify the array is the StaticArray::push() function which has this 
+    /// invariant as both a pre and post condition. So everytime we add an element to an array this condition is upheld.
+    /// 
+    /// # Post-conditions:
+    /// * If ChunkCreationError::Overlap(idx) is returned, then `chunk_range` overlaps with the element at index idx
+    /// * If successful, then result is equal to `chunk_range`
+    /// * If successful, then `chunk_range` did not overlap with any element in the old array/ list
+    /// * If successful, then `chunk_range` has been added to the array/ list
+    /// * If successful, then the `array` remains ordered with all Some elements followed by all None elements
+    /// 
+    /// # Verification Notes:
+    /// We could bring all post-conditions from the TrustedChunk::new functions as post-conditions here
+    /// but it gets extremenly verbose
+    #[requires(forall(|i: usize| (0 <= i && i < self.array.len() && self.array.arr[i].is_some()) ==> {
+        forall(|j: usize| (0 <= j && j < i) ==> self.array.arr[j].is_some())
+    }))]
+    #[requires(forall(|i: usize| (0 <= i && i < self.array.len() && self.array.arr[i].is_none()) ==> {
+        forall(|j: usize| (i <= j && j < self.array.arr.len()) ==> self.array.arr[j].is_none())
+    }))]
+    #[ensures(result.is_err() ==> {
+        match peek_err(&result) {
+            ChunkCreationError::Overlap(idx) => {
+                (self.heap_init && (idx < self.list.len()) & range_overlaps(&self.list.lookup(idx), &chunk_range)) ||
+                (!self.heap_init && (idx < self.array.len()) && (self.array.lookup(idx).is_some()) && range_overlaps(&peek_option(&self.array.lookup(idx)), &chunk_range))
+            },
+            _ => true
+        }
+    })]
+    #[ensures(result.is_ok() ==> {
+        let (new_chunk, _) = peek_result_ref(&result);
+        new_chunk.start() == *chunk_range.start() && new_chunk.end() == *chunk_range.end()
+    })]
+    #[ensures(result.is_ok() ==> {
+        (self.heap_init && forall(|i: usize| (0 <= i && i < old(self.list.len())) ==> !range_overlaps(&old(self.list.lookup(i)), &chunk_range)))
+        ||
+        (!self.heap_init && forall(|i: usize| (0 <= i && i < old(self.array.len())) && old(self.array.lookup(i)).is_some()
+            ==> !range_overlaps(&peek_option(&old(self.array.lookup(i))), &chunk_range)))
+    })]
+    #[ensures(result.is_ok() ==> {
+        (self.heap_init && self.list.len() >= 1 && self.list.lookup(0) == chunk_range)
+        ||
+        (!self.heap_init && {
+            let idx = peek_result_ref(&result).1;
+            idx < self.array.len() && self.array.lookup(idx).is_some() && peek_option(&self.array.lookup(idx)) == chunk_range
+        })
+    })]
+
+    #[ensures(forall(|i: usize| (0 <= i && i < self.array.len() && self.array.arr[i].is_some()) ==> {
+        forall(|j: usize| (0 <= j && j < i) ==> self.array.arr[j].is_some())
+    }))]
+    #[ensures(forall(|i: usize| (0 <= i && i < self.array.len() && self.array.arr[i].is_none()) ==> {
+        forall(|j: usize| (i <= j && j < self.array.arr.len()) ==> self.array.arr[j].is_none())
+    }))]
+    pub fn create_chunk(&mut self, chunk_range: RangeInclusive<usize>) -> Result<(TrustedChunk, usize), ChunkCreationError> {
+        if self.heap_init {
+            match TrustedChunk::new(chunk_range, &mut self.list) { // can't use map because Prusti can't reason about the return value then
+                Ok(chunk) => Ok((chunk, 0)),
+                Err(e) => Err(e)
+            }
+        } else {
+            TrustedChunk::new_pre_heap(chunk_range, &mut self.array)
+        }
+    }
+}
+
+
+/// A struct representing an unallocated region in memory.
+/// Its functions are formally verified to prevent range overlaps between chunks.
+#[cfg_attr(not(prusti), derive(Debug, PartialEq, Eq))]
+pub struct TrustedChunk {
+    frames: RangeInclusive<usize>
+}
+
+// assert_not_impl_any!(TrustedChunk: DerefMut, Clone);
+
+impl TrustedChunk {
+    #[pure]
+    #[trusted]
+    #[ensures(result == *self.frames.start())]
+    pub fn start(&self) -> usize {
+        *self.frames.start()
+    }
+
+    #[pure]
+    #[trusted]
+    #[ensures(result == *self.frames.end())]
+    pub fn end(&self) -> usize {
+        *self.frames.end()
+    }
+
+    pub fn frames(&self) -> RangeInclusive<usize> {
+        self.frames
+    }
+
+    #[ensures(result.is_empty())]
+    pub const fn empty() -> TrustedChunk {
+        TrustedChunk { frames: RangeInclusive::new(1, 0) }
+    }
+
+    #[pure]
+    #[ensures(result ==> self.end() < self.start())]
+    pub fn is_empty(&self) -> bool {
+        !(self.start() <= self.end())
+
+    }
+
+    /// Creates a new `TrustedChunk` with `chunk_range` if no other range in `chunk_list` overlaps with `chunk_range`
+    /// and adds the range of the newly created `TrustedChunk` to `chunk_list`.
+    /// Returns an Err if there is an overlap, with the error value being the index in `chunk_list` of the element which overlaps with `frames`.
+    /// 
+    /// # Post-conditions:
+    /// * If it fails than there was an overlap with an existing chunk or an empty range was passed as an argument
+    /// * If it succeeds, then the newly created chunk has the same bounds as `chunk_range`
+    /// * If it succeeds, then `chunk_range` is added to the list
+    /// * If it succeeds, then the length of `chunk_list` has increased by 1
+    /// * If it succeeds, then all other elements in the `chunk_list` remain unchanged
+    /// * If it succeeds, then `chunk_range` did not overlap with any element in the old `chunk_list`
+    #[ensures(result.is_err() ==> {
+        match peek_err(&result) {
+            ChunkCreationError::Overlap(idx) => (idx < chunk_list.len()) & range_overlaps(&chunk_list.lookup(idx), &chunk_range),
+            _ => true
+        }
+    })]
+    #[ensures(result.is_ok() ==> {
+        let new_chunk = peek_result_ref(&result);
+        new_chunk.start() == *chunk_range.start() && new_chunk.end() == *chunk_range.end()
+    })]
+    #[ensures(result.is_ok() ==> {
+        chunk_list.len() >= 1 && chunk_list.lookup(0) == chunk_range
+    })]
+    #[ensures(result.is_ok() ==> chunk_list.len() == old(chunk_list.len()) + 1)] 
+    #[ensures(result.is_ok() ==> {
+        forall(|i: usize| (1 <= i && i < chunk_list.len()) ==> old(chunk_list.lookup(i-1)) == chunk_list.lookup(i))
+    })]
+    #[ensures(result.is_ok() ==> {
+        forall(|i: usize| (0 <= i && i < old(chunk_list.len())) ==> !range_overlaps(&old(chunk_list.lookup(i)), &chunk_range))
+    })]
+    fn new(chunk_range: RangeInclusive<usize>, chunk_list: &mut List) -> Result<TrustedChunk, ChunkCreationError> {
+        if chunk_range.is_empty() {
+            return Err(ChunkCreationError::InvalidRange);
+        }
+
+        let overlap_idx = chunk_list.elem_overlaps_in_list(chunk_range, 0);
+        if let Some(idx) = overlap_idx {
+            Err(ChunkCreationError::Overlap(idx))
+        } else {
+            chunk_list.push(chunk_range);
+            Ok(TrustedChunk { frames: chunk_range })
+        }
+    }
+
+
+    /// Creates a new `TrustedChunk` with `chunk_range` if no other range in `chunk_list` overlaps with `chunk_range`
+    /// and adds the range of the newly created `TrustedChunk` to `chunk_list`.
+    /// Returns an Err if there is an overlap, with the error value being the index in `chunk_list` of the element which overlaps with `frames`.
+    /// Also returns an error if the `chunk_list` is full and no new element can be added.
+    /// 
+    ///  # Pre-conditions:
+    /// * The `chunk_list` is ordered so that all Some(_) elements occur at the beginning of the array, followed by all None elements.
+    ///
+    /// # Post-conditions:
+    /// * If it fails than there was an overlap with an existing chunk, there's no more room in the array or an empty range was passed as an argument
+    /// * If it succeeds, then the newly created chunk has the same bounds as `chunk_range`
+    /// * If it succeeds, then `chunk_range` is added to the list
+    /// * If it succeeds, then all other elements in the `chunk_list` remain unchanged
+    /// * If it succeeds, then `chunk_range` did not overlap with any element in the old `chunk_list`
+    /// * If successful, then the `chunk_list` remains ordered with all Some elements followed by all None elements
+    #[requires(forall(|i: usize| (0 <= i && i < chunk_list.arr.len() && chunk_list.arr[i].is_some()) ==> {
+        forall(|j: usize| (0 <= j && j < i) ==> chunk_list.arr[j].is_some())
+    }))]
+    #[requires(forall(|i: usize| (0 <= i && i < chunk_list.arr.len() && chunk_list.arr[i].is_none()) ==> {
+        forall(|j: usize| (i <= j && j < chunk_list.arr.len()) ==> chunk_list.arr[j].is_none())
+    }))]
+    #[ensures(result.is_err() ==> {
+        match peek_err(&result) {
+            ChunkCreationError::Overlap(idx) => (idx < chunk_list.len()) && (chunk_list.lookup(idx).is_some()) && range_overlaps(&peek_option(&chunk_list.lookup(idx)), &chunk_range),
+            _ => true
+        }
+    })]
+    #[ensures(result.is_ok() ==> {
+        let (new_chunk, _) = peek_result_ref(&result);
+        new_chunk.start() == *chunk_range.start() && new_chunk.end() == *chunk_range.end()
+    })]
+    #[ensures(result.is_ok() ==> {
+        let idx = peek_result_ref(&result).1;
+        idx < chunk_list.len() && chunk_list.lookup(idx).is_some() && peek_option(&chunk_list.lookup(idx)) == chunk_range
+    })]
+    #[ensures(result.is_ok() ==> 
+        forall(|i: usize| ((0 <= i && i < chunk_list.len()) && (i != peek_result_ref(&result).1)) ==> old(chunk_list.lookup(i)) == chunk_list.lookup(i))
+    )] 
+    #[ensures(result.is_ok() ==> 
+        forall(|i: usize| ((0 <= i && i < chunk_list.len()) ) && old(chunk_list.lookup(i)).is_some()
+            ==> !range_overlaps(&peek_option(&old(chunk_list.lookup(i))), &chunk_range))
+    )] 
+    #[ensures(forall(|i: usize| (0 <= i && i < chunk_list.arr.len() && chunk_list.arr[i].is_some()) ==> {
+        forall(|j: usize| (0 <= j && j < i) ==> chunk_list.arr[j].is_some())
+    }))]
+    #[ensures(forall(|i: usize| (0 <= i && i < chunk_list.arr.len() && chunk_list.arr[i].is_none()) ==> {
+        forall(|j: usize| (i <= j && j < chunk_list.arr.len()) ==> chunk_list.arr[j].is_none())
+    }))]
+    fn new_pre_heap(chunk_range: RangeInclusive<usize>, chunk_list: &mut StaticArray) -> Result<(TrustedChunk, usize), ChunkCreationError> {
+        if chunk_range.is_empty() {
+            return Err(ChunkCreationError::InvalidRange);
+        }
+
+        let overlap_idx = chunk_list.elem_overlaps_in_array(chunk_range, 0);
+        if let Some(idx) = overlap_idx {
+            Err(ChunkCreationError::Overlap(idx))
+        } else {
+            match chunk_list.push(chunk_range){
+                Ok(idx) => Ok((TrustedChunk { frames: chunk_range }, idx)),
+                Err(()) => Err(ChunkCreationError::NoSpace)
+            }
+        }
+    }
+
+    /// Private function that creates a chunk without any checks.
+    /// 
+    /// Only used within other verified functions, or registered as a callback
+    #[requires(*frames.start() <= *frames.end())]
+    #[ensures(result.start() == *frames.start())]
+    #[ensures(result.end() == *frames.end())]
+    pub(crate) fn trusted_new(frames: RangeInclusive<usize>) -> TrustedChunk {
+        TrustedChunk{frames}
+    }
+
+
+    /// Splits a chunk into 1-3 chunks, depending on where the split is at.
+    /// It is formally verified that the resulting chunks are disjoint, contiguous and their start/end is equal to that of the original chunk.
+    /// 
+    /// # Post-conditions:
+    /// * If it succeeds, then the resulting chunks have no overlapping ranges
+    /// * If it succeeds, then the resulting chunks are contiguous
+    /// * If it succeeds, then the resulting chunks combined have the same range as `self`
+    /// * If it fails, then the original chunk is returned
+    #[ensures(result.is_ok() ==> {
+        let split_chunk = peek_result_ref(&result);
+        split_chunk_has_no_overlapping_ranges(&split_chunk.0, &split_chunk.1, &split_chunk.2)
+    })]
+    #[ensures(result.is_ok() ==> {
+        let split_chunk = peek_result_ref(&result);
+        split_chunk_is_contiguous(&split_chunk.0, &split_chunk.1, &split_chunk.2)
+    })]
+    #[ensures(result.is_ok() ==> split_chunk_has_same_range(&self, peek_result_ref(&result)))]
+    #[ensures(result.is_err() ==> {
+        let orig_chunk = peek_err_ref(&result);
+        (orig_chunk.start() == self.start()) && (orig_chunk.end() == self.end())
+    })]
+    pub fn split(self, start_frame: usize, num_frames: usize) -> Result<(Option<TrustedChunk>, TrustedChunk, Option<TrustedChunk>), TrustedChunk> {
+        if (start_frame < self.start()) || (start_frame + num_frames -1 > self.end()) || (num_frames <= 0) {
+            return Err(self);
+        }
+
+        let first_chunk = if start_frame == self.start()  {
+            None
+        } else {
+            Some(TrustedChunk::trusted_new(RangeInclusive::new(self.start(), start_frame - 1)))
+        };
+        let second_chunk = TrustedChunk::trusted_new(RangeInclusive::new(start_frame, start_frame + num_frames - 1));
+
+        let third_chunk = if start_frame + num_frames - 1 == self.end() {
+            None
+        } else {
+            Some(TrustedChunk::trusted_new(RangeInclusive::new(start_frame + num_frames, self.end())))
+        };
+
+        Ok((first_chunk, second_chunk, third_chunk))
+    }
+
+
+    /// Splits a chunk into 2 chunks at the frame with number `at_frame`.
+    /// It is formally verified that the resulting chunks are disjoint, contiguous and their start/end is equal to that of the original chunk.
+    /// 
+    /// # Post-conditions:
+    /// * If it succeeds, then both chunks can't be empty
+    /// * If it succeeds and the first chunk is empty, then the second chunk is equal to `self`
+    /// * If it succeeds and the second chunk is empty, then the first chunk is equal to `self`
+    /// * If it succeeds and both chunks aren't empty, then the chunks are contiguous and their combined range is equal to the range of `self`
+    /// * If it fails, then the original chunk is returned
+    #[ensures(result.is_ok() ==> {
+        let split_chunk = peek_result_ref(&result);
+        split_chunk.0.is_empty() && !split_chunk.1.is_empty() ||
+        !split_chunk.0.is_empty() && split_chunk.1.is_empty() ||
+        !split_chunk.0.is_empty() && !split_chunk.1.is_empty()
+    })]
+    #[ensures(result.is_ok() ==> {
+        let split_chunk = peek_result_ref(&result);
+        split_chunk.0.is_empty() ==> (split_chunk.1.start() == old(self.start()) && split_chunk.1.end() == old(self.end()))
+    })]
+    #[ensures(result.is_ok() ==> {
+        let split_chunk = peek_result_ref(&result);
+        split_chunk.1.is_empty() ==> (split_chunk.0.start() == old(self.start()) && split_chunk.0.end() == old(self.end()))
+    })]
+    #[ensures(result.is_ok() ==> {
+        let split_chunk = peek_result_ref(&result);
+        (!split_chunk.0.is_empty() && !split_chunk.1.is_empty()) ==> {
+            split_chunk.0.start() == old(self.start()) && split_chunk.0.end() == at_frame - 1 &&
+            split_chunk.1.start() == at_frame && split_chunk.1.end() == old(self.end())
+        }
+    })]
+    #[ensures(result.is_err() ==> {
+        let orig_chunk = peek_err_ref(&result);
+        (orig_chunk.start() == self.start()) && (orig_chunk.end() == self.end())
+    })]
+    pub fn split_at(mut self, at_frame: usize) -> Result<(TrustedChunk, TrustedChunk), TrustedChunk> {
+       let end_of_first = at_frame - 1;
+
+        let (first, second) = if at_frame == self.start() && at_frame <= self.end() {
+            let first  = TrustedChunk::empty();
+            let second = TrustedChunk::trusted_new(RangeInclusive::new(at_frame, self.end()));
+            (first, second)
+        } 
+        else if at_frame == (self.end() + 1) && end_of_first >= self.start() {
+            let first  = TrustedChunk::trusted_new(RangeInclusive::new(self.start(), self.end())); 
+            let second = TrustedChunk::empty();
+            (first, second)
+        }
+        else if at_frame > self.start() && end_of_first <= self.end() {
+            let first  = TrustedChunk::trusted_new(RangeInclusive::new(self.start(), end_of_first));
+            let second = TrustedChunk::trusted_new(RangeInclusive::new(at_frame, self.end()));
+            (first, second)
+        }
+        else {
+            return Err(self);
+        };
+
+        core::mem::forget(self);   
+        Ok(( first, second ))
+    }
+
+
+    /// Merges `other` into `self`.
+    /// Succeeds if `other` lies right before `self` or right after.
+    /// 
+    /// # Post-conditions:
+    /// * If it succeeds, then `other` and `self` were contiguous, and either `self`'s start bound has been updated to `other`'s start 
+    /// or `self`s end has been updated to `other`'s end
+    /// * If it fails, then `self` remains unchanged and `other` is returned
+    #[ensures(result.is_ok() ==> 
+        (old(self.start()) == other.end() + 1 && self.start() == other.start() && self.end() == old(self.end())) 
+        || 
+        (old(self.end()) + 1 == other.start() && self.end() == other.end() && self.start() == old(self.start()))
+    )]
+    #[ensures(result.is_err() ==> {
+        let chunk = peek_err_ref(&result);
+        (chunk.start() == other.start()) && (chunk.end() == other.end()) 
+    })]
+    #[ensures(result.is_err() ==> {
+        (self.start() == old(self.start())) && (self.end() == old(self.end())) 
+    })]
+    pub fn merge(&mut self, other: TrustedChunk) -> Result<(), TrustedChunk> {
+        if self.is_empty() | other.is_empty() {
+            return Err(other);
+        }
+
+        if self.start() == other.end() + 1 {
+            // `other` comes contiguously before `self`
+            self.frames = RangeInclusive::new(other.start(), self.end());
+        } 
+        else if self.end() + 1 == other.start() {
+            // `self` comes contiguously before `other`
+            self.frames = RangeInclusive::new(self.start(), other.end());
+        }
+        else {
+            // non-contiguous
+            return Err(other);
+        }
+
+        // ensure the now-merged TrustedChunk doesn't run its drop handler (currently not implemented, but to prevent any future issues.)
+        core::mem::forget(other); 
+        Ok(())
+    }
+}
+
+
+impl Deref for TrustedChunk {
+    type Target = RangeInclusive<usize>;
+    #[pure]
+    fn deref(&self) -> &RangeInclusive<usize> {
+        &self.frames
+    }
+}