diff --git a/app/layout_matcha.ld b/app/layout_matcha.ld
index 8f8ad71..57e2378 100644
--- a/app/layout_matcha.ld
+++ b/app/layout_matcha.ld
@@ -10,7 +10,7 @@
    * the kernel binary, check for the actual address of APP_MEMORY!
    */
   FLASH (rx) : ORIGIN = 0x20080040, LENGTH = 0x80000 - 0x40
-  SRAM (rwx) : ORIGIN = 0x10006000, LENGTH = 0x1a000
+  SRAM (rwx) : ORIGIN = 0x10006800, LENGTH = 0x19800
 }
 
 MPU_MIN_ALIGN = 1K;
diff --git a/capsules/Cargo.toml b/capsules/Cargo.toml
index 65f7cf5..49ad333 100644
--- a/capsules/Cargo.toml
+++ b/capsules/Cargo.toml
@@ -7,4 +7,5 @@
 kernel          = { path = "../../tock/kernel" }
 matcha_hal      = { path = "../hal" }
 matcha_utils    = { path = "../utils" }
-matcha_config   = { path = "../config" }
\ No newline at end of file
+matcha_config   = { path = "../config" }
+capsules        = { path = "../../tock/capsules" }
diff --git a/capsules/src/elfloader_capsule.rs b/capsules/src/elfloader_capsule.rs
index 5cd6780..42ace5c 100644
--- a/capsules/src/elfloader_capsule.rs
+++ b/capsules/src/elfloader_capsule.rs
@@ -1,34 +1,755 @@
 //! Trivial Shodan elf loader capsule
 
+// TODO(sleffler): cleanup panic msgs (currently fuzzy line numbers)
+
+use core::cell::Cell;
+use core::marker::PhantomData;
+use kernel::common::cells::{OptionalCell, TakeCell};
+use kernel::hil;
+use kernel::hil::flash::Flash;
 use kernel::{AppId, AppSlice, Callback, Driver, ReturnCode, Shared};
 use matcha_hal::dprintf;
 use matcha_hal::mailbox_hal::MailboxHAL;
+use matcha_hal::smc_ctrl_hal;
+use matcha_utils::elf_loader::{Elf32Header, Elf32Phdr};
+use matcha_utils::smc_ram_memcpy;
+use matcha_utils::tar_loader::TarHeader;
 
-pub struct ElfLoaderCapsule {
+const PT_LOAD: u32 = 1;  // Loadable segment
+
+pub struct ElfLoaderCapsule<'a, F: hil::flash::Flash + 'static> {
     mailbox_hal: Option<&'static dyn MailboxHAL>,
+    smc_ctrl_hal: Option<&'static dyn smc_ctrl_hal::SmcCtrlHal>,
+    fpga: bool,
+    flash: Option<&'static capsules::virtual_flash::FlashUser<'static, F>>,
+    flash_busy: Cell<bool>,
+    read_page: TakeCell<'static, F::Page>,
+    page_len: u32,
+    state: Cell<ElfLoaderState>,
+    phantom: PhantomData<&'a ()>,
+    tasks: Cell<[(LoadTasks, bool); 9]>,
+    current_task: OptionalCell<LoadTasks>,
+    sel4_state: Cell<SEL4State>,
 }
 
-impl ElfLoaderCapsule {
-    pub fn new() -> Self {
-        Self { mailbox_hal: None }
+#[derive(Clone, Copy, PartialEq)]
+enum LoadTasks {
+    FindFile(&'static str /* name */),
+    LoadElfHeaders(&'static str /* name */),
+    LoadElf(&'static str /* name */, u32 /* offset */),
+    LoadBinary(&'static str /* name */, u32 /* base */),
+    StartSmc,
+}
+
+#[derive(Clone, Copy)]
+struct SEL4State {
+    kernel_offset: u32,
+    capdl_loader_offset: u32,
+    cantrip_builtins_offset: u32,
+    cantrip_builtins_size: u32,
+    kernel_entry_point: u32,
+    capdl_loader_entry_point: u32,
+    kernel_headers: [Option<Elf32Phdr>; 4],
+    capdl_loader_headers: [Option<Elf32Phdr>; 4],
+    kernel_bss_start: u32,
+    kernel_bss_size: u32,
+    capdl_bss_start: u32,
+    capdl_bss_size: u32,
+}
+
+impl Default for SEL4State {
+    fn default() -> SEL4State {
+        SEL4State {
+            kernel_offset: 0,
+            capdl_loader_offset: 0,
+            cantrip_builtins_offset: 0,
+            cantrip_builtins_size: 0,
+            kernel_entry_point: 0,
+            capdl_loader_entry_point: 0,
+            kernel_headers: [None, None, None, None],
+            capdl_loader_headers: [None, None, None, None],
+            kernel_bss_start: 0,
+            kernel_bss_size: 0,
+            capdl_bss_start: 0,
+            capdl_bss_size: 0,
+        }
+    }
+}
+
+// Should I be part of self?
+static LOAD_SEL4_TASKS: [(LoadTasks, bool); 9] = [
+    (LoadTasks::FindFile("kernel"), false),
+    (LoadTasks::FindFile("capdl-loader"), false),
+    (LoadTasks::FindFile("cantrip-builtins"), false),
+    (LoadTasks::LoadElfHeaders("kernel"), false),
+    (LoadTasks::LoadElfHeaders("capdl-loader"), false),
+    (LoadTasks::LoadElf("kernel", 0), false),
+    (
+        LoadTasks::LoadElf(
+            "capdl-loader",
+            0, /* this should get mutated after previous */
+        ),
+        false,
+    ),
+    // Hack: load the builtins bundle into the last .5M of memory; this
+    // can go away when the Mailbox protocol supports fetching files in
+    // the bundle from flash.
+    (LoadTasks::LoadBinary("cantrip-builtins", 0x50380000), false),
+    (LoadTasks::StartSmc, false),
+];
+
+#[derive(Clone, Copy, PartialEq)]
+enum ElfLoaderState {
+    Idle,
+    FindingFile(&'static str /* name */, u32 /* cursor */),
+    LoadElfHeader(u32 /* cursor */),
+    LoadProgramHeaderTable(
+        u32, /* cursor */
+        u32, /* offset */
+        u16, /* num */
+        u16, /* index */
+    ),
+    LoadSegmentsNew(
+        &'static str, /* name */
+        Elf32Phdr,    /* phdr */
+        usize,        /* index */
+        u32,          /* cursor */
+        u32,          /* dst offset */
+        u32,          /* offset_in_page */
+        u32,          /* already loaded */
+    ),
+    LoadBinary(
+        &'static str, /* name */
+        u32,          /* base */
+        u32,          /* cursor */
+        u32,          /* bytes_read */
+    ),
+}
+
+impl<'a, F: hil::flash::Flash> ElfLoaderCapsule<'a, F> {
+    pub fn new(fpga: bool) -> Self {
+        Self {
+            mailbox_hal: None,
+            smc_ctrl_hal: None,
+            fpga: fpga,
+            flash: None,
+            flash_busy: Cell::new(false),
+            read_page: TakeCell::empty(),
+            page_len: 0,
+            state: Cell::new(ElfLoaderState::Idle),
+            phantom: PhantomData,
+            tasks: Cell::new(LOAD_SEL4_TASKS.clone()),
+            current_task: OptionalCell::empty(),
+            sel4_state: Cell::new(SEL4State::default()),
+        }
+    }
+
+    pub fn set_smc_ctrl(&mut self, smc_ctrl: &'static dyn smc_ctrl_hal::SmcCtrlHal) {
+        self.smc_ctrl_hal = Some(smc_ctrl);
     }
 
     pub fn set_mailbox(&mut self, mailbox: &'static dyn MailboxHAL) {
         self.mailbox_hal = Some(mailbox);
     }
+
+    pub fn set_flash(
+        &mut self,
+        flash: &'static capsules::virtual_flash::FlashUser<'static, F>,
+        read_page: &'static mut F::Page,
+    ) {
+        self.flash = Some(flash);
+        self.read_page.replace(read_page);
+        let mut page_len = 0;
+        self.read_page.map(|page| {
+            let mut_page = page.as_mut();
+            page_len = mut_page.len() as u32;
+        });
+        self.page_len = page_len;
+    }
+
+    pub fn run_next_task(&self) {
+        self.current_task.clear();
+        let mut tasks = self.tasks.get();
+        for i in 0..tasks.len() {
+            let (task, done) = tasks[i];
+            if !done {
+                tasks[i] = (task, true);
+                self.current_task.replace(task);
+                break;
+            }
+        }
+        self.tasks.replace(tasks);
+
+        self.current_task.map_or_else(
+            || {
+                // dprintf!("no current task\r\n");
+                loop {}
+            },
+            |task| match task {
+                LoadTasks::FindFile(file) => {
+                    self.find_file(file);
+                }
+                LoadTasks::LoadElfHeaders(file) => {
+                    self.load_elf_headers(file);
+                }
+                LoadTasks::LoadElf("kernel", _) => {
+                    dprintf!("Loading seL4 kernel\r\n");
+                    self.load_elf("kernel", 0);
+                }
+                LoadTasks::LoadElf("capdl-loader", _) => {
+                    dprintf!("Loading capdl-loader to the page after seL4\r\n");
+                    let sel4_pend =
+                        matcha_utils::round_up_to_page(matcha_utils::elf_loader::elf_phys_max_opt(
+                            &self.sel4_state.get().kernel_headers,
+                        ));
+                    let offset = sel4_pend
+                        - matcha_utils::elf_loader::elf_phys_min_opt(
+                            &self.sel4_state.get().capdl_loader_headers,
+                        );
+                    self.load_elf("capdl-loader", offset);
+                }
+                LoadTasks::LoadBinary(name, base) => {
+                    dprintf!("Loading {} to {:X}\r\n", name, base);
+                    self.load_binary(name, *base);
+                }
+                LoadTasks::StartSmc => {
+                    // NB: ui_p_reg_start & co. come from the code in seL4
+                    //    the processes these values.
+                    let ui_p_reg_start =
+                        matcha_utils::round_up_to_page(matcha_utils::elf_loader::elf_phys_max_opt(
+                            &self.sel4_state.get().kernel_headers,
+                        ));
+                    let ui_p_reg_end = ui_p_reg_start
+                        + matcha_utils::round_up_to_page(
+                            matcha_utils::elf_loader::elf_phys_max_opt(
+                                &self.sel4_state.get().capdl_loader_headers,
+                            ) - matcha_utils::elf_loader::elf_phys_min_opt(
+                                &self.sel4_state.get().capdl_loader_headers,
+                            ),
+                        );
+                    let pv_offset = ui_p_reg_start
+                        - matcha_utils::elf_loader::elf_phys_min_opt(
+                            &self.sel4_state.get().capdl_loader_headers,
+                        );
+                    let v_entry = self.sel4_state.get().capdl_loader_entry_point;
+/*
+                    dprintf!(
+                        "{:X} {:X} {:X} {:X}\r\n",
+                        ui_p_reg_start,
+                        ui_p_reg_end,
+                        pv_offset,
+                        v_entry
+                    );
+                    dprintf!(
+                        "{:X} {:X} {:X}\r\n",
+                        ui_p_reg_start,
+                        matcha_utils::elf_loader::elf_phys_max_opt(
+                            &self.sel4_state.get().capdl_loader_headers
+                        ),
+                        matcha_utils::elf_loader::elf_phys_min_opt(
+                            &self.sel4_state.get().capdl_loader_headers
+                        ),
+                    );
+*/
+                    matcha_utils::smc_ram_zero(
+                        self.sel4_state.get().kernel_bss_start,
+                        self.sel4_state.get().kernel_bss_size as usize
+                    );
+                    matcha_utils::smc_ram_zero(
+                        self.sel4_state.get().capdl_bss_start,
+                        self.sel4_state.get().capdl_bss_size as usize
+                    );
+                    match self.smc_ctrl_hal {
+                        Some(smc_ctrl) => {
+                            self.mailbox_hal.map(|mb| {
+                                matcha_utils::smc_send_bootmsg(mb, [
+                                      ui_p_reg_start,
+                                      ui_p_reg_end,
+                                      pv_offset,
+                                      v_entry,
+                                ])
+                            });
+                            smc_ctrl.smc_ctrl_start();
+                        }
+                        None => {
+                            panic!("221");
+                        }
+                    }
+                }
+                _ => {
+                    panic!("225");
+                }
+            },
+        );
+    }
+
+    pub fn load_sel4(&self) {
+        // May be able to remove this, if we clean up after done.
+        let tasks = LOAD_SEL4_TASKS.clone();
+        self.tasks.replace(tasks);
+        self.run_next_task();
+    }
+
+    fn load_elf_headers(&self, name: &'static str) {
+        match name {
+            "kernel" => self.state.set(ElfLoaderState::LoadElfHeader(
+                self.sel4_state.get().kernel_offset,
+            )),
+            "capdl-loader" => self.state.set(ElfLoaderState::LoadElfHeader(
+                self.sel4_state.get().capdl_loader_offset,
+            )),
+            _ => {
+                panic!("207");
+            }
+        }
+        match self.state.get() {
+            ElfLoaderState::LoadElfHeader(cursor) => {
+                self.read_page(cursor);
+            }
+            _ => {
+                panic!("214");
+            }
+        }
+    }
+
+    fn load_binary(&self, name: &'static str, base: u32) {
+        let cursor = match name {
+            "cantrip-builtins" => self.sel4_state.get().cantrip_builtins_offset,
+            _ => panic!("258"),
+        };
+        let new_state = ElfLoaderState::LoadBinary(name, base, cursor, 0);
+        self.state.set(new_state);
+        self.read_page(cursor);
+    }
+
+    fn load_elf(&self, name: &'static str, offset: u32) {
+        let phdr = match name {
+            "kernel" => self.sel4_state.get().kernel_headers[0].unwrap(),
+            "capdl-loader" => self.sel4_state.get().capdl_loader_headers[0].unwrap(),
+            _ => panic!("290"),
+        };
+        let mod_offset = phdr.p_offset % self.page_len;
+        let div_offset = phdr.p_offset / self.page_len;
+        let cursor = match name {
+            "kernel" => self.sel4_state.get().kernel_offset,
+            "capdl-loader" => self.sel4_state.get().capdl_loader_offset,
+            _ => panic!("295"),
+        } + (div_offset * self.page_len);
+        let new_state =
+            ElfLoaderState::LoadSegmentsNew(name, phdr, 0, cursor, offset, mod_offset, 0);
+        self.state.set(new_state);
+        if phdr.p_type == PT_LOAD && phdr.p_filesz != 0 {
+            dprintf!(
+                "seg 0:{:X} -> {:X}:{:X} ({} bytes)\r\n",
+                cursor,
+                phdr.p_paddr + offset,
+                phdr.p_paddr + offset + phdr.p_filesz,
+                { phdr.p_filesz },
+            );
+            let bss_size = phdr.p_memsz - phdr.p_filesz;
+            let bss_start = phdr.p_paddr + offset + phdr.p_filesz;
+            let bss_end = bss_start + bss_size;
+
+            dprintf!(
+                "bss 0:{:X} -> {:X}:{:X} ({} bytes)\r\n",
+                cursor,
+                bss_start,
+                bss_end,
+                bss_size
+            );
+            match name {
+                "kernel" => {
+                        let mut sel4_state = self.sel4_state.get();
+                        sel4_state.kernel_bss_start = bss_start;
+                        sel4_state.kernel_bss_size = bss_size;
+                        self.sel4_state.replace(sel4_state);
+                },
+                "capdl-loader" => {
+                        let mut sel4_state = self.sel4_state.get();
+                        sel4_state.capdl_bss_start = bss_start;
+                        sel4_state.capdl_bss_size = bss_size;
+                        self.sel4_state.replace(sel4_state);
+                },
+                _ => panic!("349"),
+            };
+            // matcha_utils::smc_ram_zero(bss_start, bss_size as usize);
+            self.read_page(cursor);
+        } else {
+            panic!("295");
+        }
+    }
+
+    fn find_file(&self, name: &'static str) {
+        self.state.set(ElfLoaderState::FindingFile(name, 0));
+        self.read_page(0);
+    }
+
+    fn load_elf_header_callback(&self) {
+        self.read_page.map(|page| {
+            let mut_page = page.as_mut();
+            let elf_header = Elf32Header::from_bytes(mut_page);
+            if !elf_header.check_magic() {
+                dprintf!("bad elf magic\r\n");
+                panic!("233");
+            }
+            self.current_task.map(|task| {
+                match task {
+                    LoadTasks::LoadElfHeaders("kernel") => {
+                        let mut sel4_state = self.sel4_state.get();
+                        sel4_state.kernel_entry_point = elf_header.e_entry;
+                        self.sel4_state.replace(sel4_state);
+                    }
+                    LoadTasks::LoadElfHeaders("capdl-loader") => {
+                        let mut sel4_state = self.sel4_state.get();
+                        sel4_state.capdl_loader_entry_point = elf_header.e_entry;
+                        self.sel4_state.replace(sel4_state);
+                    }
+                    _ => {
+                        panic!("290");
+                    }
+                };
+            });
+            match self.state.get() {
+                ElfLoaderState::LoadElfHeader(cursor) => {
+                    self.state.set(ElfLoaderState::LoadProgramHeaderTable(
+                        cursor,
+                        elf_header.phoff(),
+                        elf_header.phnum(),
+                        0,
+                    ));
+                }
+                _ => {
+                    panic!("245");
+                }
+            }
+        });
+        match self.state.get() {
+            ElfLoaderState::LoadProgramHeaderTable(cursor, _, _, _) => {
+                self.read_page(cursor);
+            }
+            _ => {
+                panic!("254");
+            }
+        }
+    }
+
+    fn load_program_header_table_callback(&self) {
+        self.read_page.map(|page| {
+            let mut_page = page.as_mut();
+            match self.state.get() {
+                ElfLoaderState::LoadProgramHeaderTable(_, offset, _, index) => {
+                    let phdr = Elf32Phdr::from_bytes(
+                        &mut mut_page[(((offset as usize)
+                            + (index as usize * core::mem::size_of::<Elf32Phdr>()))
+                            as usize)..],
+                    );
+                    if phdr.p_type == PT_LOAD
+                    /* && (phdr.p_filesz != 0)*/
+                    {
+                        self.current_task.map(|task| {
+                            match task {
+                                LoadTasks::LoadElfHeaders("kernel") => {
+                                    let mut sel4_state = self.sel4_state.get();
+                                    let mut next_slot: Option<usize> = None;
+                                    for i in 0..sel4_state.kernel_headers.len() {
+                                        if sel4_state.kernel_headers[i] == None {
+                                            next_slot = Some(i);
+                                            break;
+                                        }
+                                    }
+                                    match next_slot {
+                                        Some(slot) => {
+                                            sel4_state.kernel_headers[slot] = Some(phdr);
+                                        }
+                                        None => {
+                                            panic!("380");
+                                        }
+                                    }
+                                    self.sel4_state.replace(sel4_state);
+                                }
+                                LoadTasks::LoadElfHeaders("capdl-loader") => {
+                                    let mut sel4_state = self.sel4_state.get();
+                                    let mut next_slot: Option<usize> = None;
+                                    for i in 0..sel4_state.capdl_loader_headers.len() {
+                                        if sel4_state.capdl_loader_headers[i] == None {
+                                            next_slot = Some(i);
+                                            break;
+                                        }
+                                    }
+                                    match next_slot {
+                                        Some(slot) => {
+                                            sel4_state.capdl_loader_headers[slot] = Some(phdr);
+                                        }
+                                        None => {
+                                            panic!("380");
+                                        }
+                                    }
+                                    self.sel4_state.replace(sel4_state);
+                                }
+                                _ => {
+                                    panic!("317");
+                                }
+                            };
+                        });
+                    }
+                }
+                _ => {
+                    panic!("335");
+                }
+            };
+        });
+        match self.state.get() {
+            ElfLoaderState::LoadProgramHeaderTable(cursor, offset, count, index) => {
+                if index + 1 < count {
+                    self.state.set(ElfLoaderState::LoadProgramHeaderTable(
+                        cursor,
+                        offset,
+                        count,
+                        index + 1,
+                    ));
+                    self.read_page(cursor);
+                } else {
+                    self.state.set(ElfLoaderState::Idle);
+                    self.run_next_task();
+                }
+            }
+            _ => {
+                panic!("375");
+            }
+        }
+    }
+
+    fn load_binary_callback(&self) {
+        match self.state.get() {
+            ElfLoaderState::LoadBinary(name, base, cursor, bytes_read) => {
+                let size = match name {
+                    "cantrip-builtins" => self.sel4_state.get().cantrip_builtins_size,
+                    _ => panic!("463"),
+                };
+                self.read_page.map(|page| {
+                    let mut_page = page.as_mut();
+                    let remaining = size - bytes_read;
+                    let bytes_in_this_page = core::cmp::min(remaining, self.page_len);
+                    smc_ram_memcpy(
+                        &mut mut_page[0..],
+                        base + bytes_read,
+                        bytes_in_this_page as usize,
+                    );
+                });
+
+                let new_state = if (bytes_read + self.page_len) >= size {
+                    ElfLoaderState::Idle
+                } else {
+                    ElfLoaderState::LoadBinary(
+                        name,
+                        base,
+                        cursor + self.page_len,
+                        bytes_read + self.page_len,
+                    )
+                };
+                self.state.set(new_state);
+                match self.state.get() {
+                    ElfLoaderState::Idle => {
+                        self.run_next_task();
+                    }
+                    ElfLoaderState::LoadBinary(_, _, cursor, _) => {
+                        self.read_page(cursor);
+                    }
+                    _ => {
+                        panic!("477");
+                    }
+                };
+            }
+            _ => {
+                panic!("464");
+            }
+        }
+    }
+
+    fn load_segment_callback(&self) {
+        match self.state.get() {
+            ElfLoaderState::LoadSegmentsNew(
+                name,
+                phdr,
+                index,
+                cursor,
+                offset,
+                mod_offset,
+                loaded,
+            ) => {
+                let bytes_in_this_page = self.page_len - mod_offset;
+                // Copy data into SMC ram.
+                self.read_page.map(|page| {
+                    let mut_page = page.as_mut();
+                    smc_ram_memcpy(
+                        &mut mut_page[(mod_offset as usize)..],
+                        phdr.p_paddr + offset + loaded,
+                        bytes_in_this_page as usize,
+                    );
+                });
+                let progress = loaded + bytes_in_this_page;
+                if progress < phdr.p_filesz {
+                    // Another page
+                    let new_cursor = cursor + self.page_len;
+                    let new_state = ElfLoaderState::LoadSegmentsNew(
+                        name, phdr, index, new_cursor, offset, 0, progress,
+                    );
+                    self.state.set(new_state);
+                    self.read_page(new_cursor);
+                } else {
+                    let segments = match name {
+                        "kernel" => self.sel4_state.get().kernel_headers,
+                        "capdl-loader" => self.sel4_state.get().capdl_loader_headers,
+                        _ => {
+                            panic!("461");
+                        }
+                    };
+                    let next_index = index + 1;
+                    let mut last_segment = false;
+                    if next_index == segments.len() {
+                        last_segment = true;
+                    }
+                    if !last_segment {
+                        last_segment = match segments[next_index] {
+                            Some(_) => false,
+                            None => true,
+                        };
+                    }
+                    if last_segment {
+                        self.state.set(ElfLoaderState::Idle);
+                        self.run_next_task();
+                    } else {
+                        let next_segment = segments[next_index].unwrap();
+                        if next_segment.p_memsz != 0 && next_segment.p_filesz == 0 {
+                            // some bss segment, let's clear the memory.
+                            matcha_utils::smc_ram_zero(next_segment.p_paddr + offset, next_segment.p_memsz as usize);
+                        }
+                        self.state.set(ElfLoaderState::Idle);
+                        self.run_next_task();
+                        // TODO(atv): Finish this here.
+                        // panic!("476");
+                        // let next_segment = segments[next_index];
+                        // let new_cursor = ?;
+                        // let mod_offset = ?;
+                        // let new_state = ElfLoaderState::LoadSegmentsNew(name, next_segment, next_index, new_cursor, offset, mod_offset, 0);
+                        // self.state.set(new_state);
+                        // self.read_page(new_cursor);
+                    }
+                }
+            }
+            _ => {
+                panic!("445");
+            }
+        }
+    }
+
+    fn find_file_callback(&self) {
+        self.read_page.map(|page| {
+            let mut_page = page.as_mut();
+            let tar_header = TarHeader::from_bytes(mut_page);
+            match self.state.get() {
+                ElfLoaderState::FindingFile(name, cursor) => {
+                    let found_file = tar_header.name().contains(name);
+                    let size = tar_header.size();
+                    self.current_task.map(|task| match task {
+                        LoadTasks::FindFile(_file) => {
+                            if found_file {
+                                let mut sel4_state = self.sel4_state.get();
+                                match name {
+                                    "kernel" => {
+                                        sel4_state.kernel_offset = cursor + self.page_len;
+                                    }
+                                    "capdl-loader" => {
+                                        sel4_state.capdl_loader_offset = cursor + self.page_len;
+                                    }
+                                    "cantrip-builtins" => {
+                                        sel4_state.cantrip_builtins_offset = cursor + self.page_len;
+                                        sel4_state.cantrip_builtins_size = size;
+                                    }
+                                    _ => {}
+                                }
+                                self.sel4_state.replace(sel4_state);
+                                self.state.set(ElfLoaderState::Idle);
+                            } else {
+                                let new_cursor =
+                                    self.page_len + cursor + ((tar_header.size() + 511) & !511);
+                                self.state
+                                    .set(ElfLoaderState::FindingFile(name, new_cursor));
+                            }
+                        }
+                        LoadTasks::LoadElf(_file, _) => {
+                            if found_file {
+                                self.state
+                                    .set(ElfLoaderState::LoadElfHeader(cursor + self.page_len));
+                            } else {
+                                let new_cursor =
+                                    self.page_len + cursor + ((tar_header.size() + 511) & !511);
+                                self.state
+                                    .set(ElfLoaderState::FindingFile(name, new_cursor));
+                            }
+                        }
+                        _ => {
+                            panic!("487");
+                        }
+                    })
+                }
+                _ => {
+                    panic!("491");
+                }
+            };
+        });
+
+        match self.state.get() {
+            ElfLoaderState::FindingFile(_, cursor) => {
+                self.read_page(cursor);
+            }
+            ElfLoaderState::LoadElfHeader(cursor) => {
+                self.read_page(cursor);
+            }
+            ElfLoaderState::Idle => {
+                self.run_next_task();
+            }
+            _ => {
+                panic!("507");
+            }
+        }
+    }
+
+    fn read_page(&self, page: u32) {
+        self.flash.map(|flash| {
+            self.read_page.take().map(|read_page| {
+                self.flash_busy.set(true);
+                if let Err((_, buf)) = flash.read_page((page / self.page_len) as usize, read_page) {
+                    self.read_page.replace(buf);
+                }
+            });
+        });
+    }
 }
 
-impl Driver for ElfLoaderCapsule {
+impl<'a, F: hil::flash::Flash> Driver for ElfLoaderCapsule<'a, F> {
     fn subscribe(&self, _: usize, _: Option<Callback>, _: AppId) -> ReturnCode {
         return ReturnCode::EINVAL;
     }
 
     fn command(&self, minor_num: usize, _r2: usize, _r3: usize, _app_id: AppId) -> ReturnCode {
-        dprintf!("ElfLoaderCapsule::command()\n");
-
         if minor_num == matcha_config::CMD_ELFLOADER_BOOT_SEL4 {
-            self.mailbox_hal.map(|mb| matcha_utils::load_sel4(mb));
-            return ReturnCode::SUCCESS;
+            match self.flash {
+                Some(_) => {
+                    if self.fpga {
+                        self.load_sel4();
+                    } else {
+                        self.mailbox_hal.map(|mb| {
+                            matcha_utils::load_sel4(mb);
+                        });
+                    }
+                    return ReturnCode::SUCCESS;
+                }
+                None => {
+                    dprintf!("No flash available\r\n");
+                    return ReturnCode::EINVAL;
+                }
+            }
         }
 
         return ReturnCode::EINVAL;
@@ -38,3 +759,42 @@
         return ReturnCode::EINVAL;
     }
 }
+
+impl<'a, F: hil::flash::Flash> hil::flash::Client<capsules::virtual_flash::FlashUser<'a, F>>
+    for ElfLoaderCapsule<'a, F>
+{
+    fn read_complete(&self, read_page: &'static mut F::Page, _err: kernel::hil::flash::Error) {
+        self.read_page.replace(read_page);
+        self.flash_busy.set(false);
+        match self.state.get() {
+            ElfLoaderState::FindingFile(_, _) => {
+                self.find_file_callback();
+            }
+            ElfLoaderState::LoadElfHeader(_) => {
+                self.load_elf_header_callback();
+            }
+            ElfLoaderState::LoadProgramHeaderTable(_, _, _, _) => {
+                self.load_program_header_table_callback();
+            }
+            ElfLoaderState::LoadSegmentsNew(_, _, _, _, _, _, _) => {
+                self.load_segment_callback();
+            }
+            ElfLoaderState::LoadBinary(_, _, _, _) => {
+                self.load_binary_callback();
+            }
+            _ => {
+                panic!("583");
+            }
+        }
+    }
+    fn write_complete(
+        &self,
+        _: &'static mut <F as kernel::hil::flash::Flash>::Page,
+        _: kernel::hil::flash::Error,
+    ) {
+        todo!()
+    }
+    fn erase_complete(&self, _: kernel::hil::flash::Error) {
+        todo!()
+    }
+}
diff --git a/platform/src/main.rs b/platform/src/main.rs
index e56403f..0d96a7e 100644
--- a/platform/src/main.rs
+++ b/platform/src/main.rs
@@ -13,6 +13,7 @@
 use kernel::common::dynamic_deferred_call::{DynamicDeferredCall, DynamicDeferredCallClientState};
 use kernel::component::Component;
 use kernel::hil;
+use kernel::hil::flash::HasClient;
 use kernel::hil::time::Alarm;
 use kernel::Chip;
 use kernel::Platform;
@@ -23,9 +24,11 @@
 use matcha_capsules::mailbox_capsule::MailboxCapsule;
 use matcha_capsules::storage_capsule::StorageCapsule;
 use matcha_config::*;
-use matcha_hal::dprintf;
+use matcha_hal::spi_host_hal;
 use matcha_hal::timer_hal;
 use matcha_hal::uart_hal;
+use matcha_hal::smc_ctrl_hal;
+use matcha_hal::rv_core_ibex_hal;
 use rv32i::csr;
 
 pub mod chip;
@@ -101,7 +104,6 @@
     &'static crate::chip::Matcha<VirtualMuxAlarm<'static, timer_hal::RvTimer>>,
 > = None;
 
-
 /// Dummy buffer that causes the linker to reserve enough space for the stack.
 /// Must be at least 16k in debug builds (@aappleby - not sure why, what's so large?)
 #[no_mangle]
@@ -118,7 +120,13 @@
     >,
     dprintf_capsule: &'static DprintfCapsule,
     storage_capsule: &'static StorageCapsule,
-    elfloader_capsule: &'static ElfLoaderCapsule,
+    elfloader_capsule: &'static ElfLoaderCapsule<
+        'static,
+        matcha_capsules::nexus_spiflash::NexusSpiflash<
+            'static,
+            capsules::virtual_spi::VirtualSpiMasterDevice<'static, spi_host_hal::SpiHw>,
+        >,
+    >,
     mailbox_capsule: &'static MailboxCapsule,
     lldb_capsule: &'static capsules::low_level_debug::LowLevelDebug<
         'static,
@@ -156,8 +164,6 @@
     // Ibex-specific handler
     crate::chip::configure_trap_handler();
 
-    dprintf!("sw/matcha/platform/src/main.rs::reset_handler()\n");
-
     // initialize capabilities
     let process_mgmt_cap = create_capability!(capabilities::ProcessManagementCapability);
     let memory_allocation_cap = create_capability!(capabilities::MemoryAllocationCapability);
@@ -258,9 +264,15 @@
         )
     );
 
+    let fpga_version = rv_core_ibex_hal::RV_CORE_IBEX_SEC.fpga_version();
     let elfloader_capsule = static_init!(
-        matcha_capsules::elfloader_capsule::ElfLoaderCapsule,
-        matcha_capsules::elfloader_capsule::ElfLoaderCapsule::new()
+             matcha_capsules::elfloader_capsule::ElfLoaderCapsule<
+                 'static,
+             matcha_capsules::nexus_spiflash::NexusSpiflash<
+                 'static,
+                 capsules::virtual_spi::VirtualSpiMasterDevice<'static, spi_host_hal::SpiHw>,
+             >>,
+             matcha_capsules::elfloader_capsule::ElfLoaderCapsule::new(fpga_version != 0)
     );
 
     let mailbox_capsule = static_init!(
@@ -279,6 +291,57 @@
     elfloader_capsule.set_mailbox(mailbox_hal);
     chip.set_mailbox_isr(mailbox_hal);
 
+    let mux_spi = components::spi::SpiMuxComponent::new(
+        &spi_host_hal::SPI_HOST0
+    ).finalize(components::spi_mux_component_helper!(spi_host_hal::SpiHw));
+    let nexus_spiflash_spi = static_init!(
+        capsules::virtual_spi::VirtualSpiMasterDevice<'static, spi_host_hal::SpiHw>,
+        capsules::virtual_spi::VirtualSpiMasterDevice::new(mux_spi, 0)
+    );
+    let nexus_spiflash_virtual_alarm = static_init!(
+        VirtualMuxAlarm<'static, timer_hal::RvTimer>,
+        VirtualMuxAlarm::new(mux_alarm)
+    );
+    let nexus_spiflash = static_init!(
+        matcha_capsules::nexus_spiflash::NexusSpiflash<
+            'static,
+            capsules::virtual_spi::VirtualSpiMasterDevice<'static, spi_host_hal::SpiHw>,
+        >,
+        matcha_capsules::nexus_spiflash::NexusSpiflash::new(
+            nexus_spiflash_spi,
+            &mut matcha_capsules::nexus_spiflash::TXBUFFER,
+            &mut matcha_capsules::nexus_spiflash::RXBUFFER,
+        )
+    );
+    nexus_spiflash_spi.set_client(nexus_spiflash);
+    nexus_spiflash_virtual_alarm.set_alarm_client(nexus_spiflash);
+
+
+    let mux_flash = static_init!(
+        capsules::virtual_flash::MuxFlash<'static, matcha_capsules::nexus_spiflash::NexusSpiflash<
+            'static,
+            capsules::virtual_spi::VirtualSpiMasterDevice<'static, spi_host_hal::SpiHw>,
+        >>,
+        capsules::virtual_flash::MuxFlash::new(nexus_spiflash)
+    );
+    hil::flash::HasClient::set_client(nexus_spiflash, mux_flash);
+    let virtual_flash = static_init!(
+        capsules::virtual_flash::FlashUser<'static, matcha_capsules::nexus_spiflash::NexusSpiflash<
+            'static,
+            capsules::virtual_spi::VirtualSpiMasterDevice<'static, spi_host_hal::SpiHw>,
+        >>,
+        capsules::virtual_flash::FlashUser::new(mux_flash)
+    );
+    let flash_read_page: &'static mut matcha_capsules::nexus_spiflash::NexusSpiflashPage = static_init!(
+        matcha_capsules::nexus_spiflash::NexusSpiflashPage,
+        matcha_capsules::nexus_spiflash::NexusSpiflashPage::default()
+    );
+
+    elfloader_capsule.set_flash(virtual_flash, flash_read_page);
+    elfloader_capsule.set_smc_ctrl(&smc_ctrl_hal::SMC_CTRL);
+    virtual_flash.set_client(elfloader_capsule);
+    // elfloader_capsule.load_sel4();
+
     let platform = MatchaPlatform {
         console_capsule: console_capsule,
         alarm_capsule: alarm_capsule,
diff --git a/utils/Cargo.toml b/utils/Cargo.toml
index 8d773c0..2dc93d6 100644
--- a/utils/Cargo.toml
+++ b/utils/Cargo.toml
@@ -4,5 +4,6 @@
 edition = "2018"
 
 [dependencies]
-
 matcha_hal = { path = "../hal" }
+capsules = { path = "../../tock/capsules" }
+kernel = { path = "../../tock/kernel" }
diff --git a/utils/src/elf_loader.rs b/utils/src/elf_loader.rs
index 219fd63..1a12a61 100644
--- a/utils/src/elf_loader.rs
+++ b/utils/src/elf_loader.rs
@@ -32,7 +32,7 @@
 }
 
 #[repr(C, packed)]
-#[derive(Debug, Copy, Clone)]
+#[derive(Debug, Copy, Clone, PartialEq)]
 pub struct Elf32Phdr {
     pub p_type: u32,   /* Segment type: Loadable segment = 1 */
     pub p_offset: u32, /* Offset of segment in file */
@@ -44,6 +44,36 @@
     pub p_align: u32,  /* Reqd alignment of segment in memory */
 }
 
+impl Elf32Phdr {
+    pub fn from_bytes(b: &mut [u8]) -> Elf32Phdr {
+        unsafe { ptr::read(b.as_ptr() as *const Elf32Phdr) }
+    }
+}
+
+impl Elf32Header {
+    pub fn from_bytes(b: &mut [u8]) -> Elf32Header {
+        unsafe { ptr::read(b.as_ptr() as *const Elf32Header) }
+    }
+
+    pub fn check_magic(&self) -> bool {
+        unsafe {
+            let pmagic: *const u32 = transmute(&self.e_ident[0]);
+            if pmagic.read_volatile() == ELF_MAGIC {
+                return true;
+            }
+        }
+        false
+    }
+
+    pub fn phoff(&self) -> u32 {
+        self.e_phoff
+    }
+
+    pub fn phnum(&self) -> u16 {
+        self.e_phnum
+    }
+}
+
 pub fn elf_phys_min(segments: &[Elf32Phdr]) -> u32 {
     return segments.iter().fold(0xFFFFFFFF, |acc, seg| {
         if seg.p_type != 1 {
@@ -54,6 +84,36 @@
     });
 }
 
+pub fn elf_phys_min_opt(segments: &[Option<Elf32Phdr>]) -> u32 {
+    return segments.iter().fold(0xFFFFFFFF, |acc, seg| match seg {
+        Some(seg) => {
+            if seg.p_type != 1 {
+                return acc;
+            } else {
+                return cmp::min(acc, seg.p_paddr);
+            }
+        }
+        None => {
+            return acc;
+        }
+    });
+}
+
+pub fn elf_phys_max_opt(segments: &[Option<Elf32Phdr>]) -> u32 {
+    return segments.iter().fold(0, |acc, seg| match seg {
+        Some(seg) => {
+            if seg.p_type != 1 {
+                return acc;
+            } else {
+                return cmp::max(acc, seg.p_paddr + seg.p_memsz);
+            }
+        }
+        None => {
+            return acc;
+        }
+    });
+}
+
 pub fn elf_phys_max(segments: &[Elf32Phdr]) -> u32 {
     return segments.iter().fold(0, |acc, seg| {
         if seg.p_type != 1 {
@@ -74,6 +134,21 @@
     });
 }
 
+pub fn elf_virt_min_opt(segments: &[Option<Elf32Phdr>]) -> u32 {
+    return segments.iter().fold(0xFFFFFFFF, |acc, seg| match seg {
+        Some(seg) => {
+            if seg.p_type != 1 {
+                return acc;
+            } else {
+                return cmp::min(acc, seg.p_vaddr);
+            }
+        }
+        None => {
+            return acc;
+        }
+    });
+}
+
 pub fn elf_virt_max(segments: &[Elf32Phdr]) -> u32 {
     return segments.iter().fold(0, |acc, seg| {
         if seg.p_type != 1 {
@@ -84,6 +159,21 @@
     });
 }
 
+pub fn elf_virt_max_opt(segments: &[Option<Elf32Phdr>]) -> u32 {
+    return segments.iter().fold(0, |acc, seg| match seg {
+        Some(seg) => {
+            if seg.p_type != 1 {
+                return acc;
+            } else {
+                return cmp::max(acc, seg.p_vaddr + seg.p_memsz);
+            }
+        }
+        None => {
+            return acc;
+        }
+    });
+}
+
 pub unsafe fn elf_get_segments(elf: *const Elf32Header) -> &'static [Elf32Phdr] {
     let base: *const u8 = transmute(elf);
     let seg_count = (*elf).e_phnum as usize;
@@ -132,11 +222,11 @@
         let txt_end = txt_start.offset(txt_size as isize);
 
         dprintf!(
-            "seg {}: {:?} -> {:?}:{:?} ({} bytes)\n",
+            "seg {}: {:X} -> {:X}:{:X} ({} bytes)\n",
             i,
-            src,
-            txt_start,
-            txt_end,
+            src as usize,
+            txt_start as usize,
+            txt_end as usize,
             txt_size
         );
         ptr::copy_nonoverlapping(src, txt_start, txt_size);
@@ -146,11 +236,11 @@
         let bss_end = bss_start.offset(bss_size as isize);
 
         dprintf!(
-            "bss {}: {:?} -> {:?}:{:?} ({} bytes)\n",
+            "bss {}: {:X} -> {:X}:{:X} ({} bytes)\n",
             i,
-            src,
-            bss_start,
-            bss_end,
+            src as usize,
+            bss_start as usize,
+            bss_end as usize,
             bss_size
         );
         ptr::write_bytes(bss_start, 0, bss_size as usize);
diff --git a/utils/src/lib.rs b/utils/src/lib.rs
index bb6f8f1..e792644 100644
--- a/utils/src/lib.rs
+++ b/utils/src/lib.rs
@@ -8,25 +8,31 @@
 
 pub const SMC_CONTROL_BLOCK: *mut u32 = 0x54020000 as *mut u32;
 
-fn round_up_to_page(addr: u32) -> u32 {
+pub fn round_up_to_page(addr: u32) -> u32 {
     return (addr + 4095) & !4095;
 }
 
 // TODO(aappleby): Break this down into smaller pieces and move into app/main
-pub fn load_sel4(mailbox : &'static dyn MailboxHAL) {
+pub fn load_sel4(mailbox: &'static dyn MailboxHAL) {
     unsafe {
         // Look in our tar file for the ELFs we need to boot Shodan.
         let sel4_elf = elf_loader::find_elf("kernel");
         let capdl_elf = elf_loader::find_elf("capdl-loader");
+        let (_, builtins_size) = tar_loader::find_file("cantrip-builtins");
 
         if sel4_elf.is_null() {
-          dprintf!("Boot failure, seL4 kernel ELF missing.\n");
-          return;
+            dprintf!("Boot failure, seL4 kernel ELF missing in FLASH.\n");
+            return;
         }
 
         if capdl_elf.is_null() {
-          dprintf!("Boot failure seL4 CapDL ELF missing.\n");
-          return;
+            dprintf!("Boot failure capdl-loader ELF missing in FLASH.\n");
+            return;
+        }
+
+        if builtins_size == 0 {
+            // NB: not present on Renode where the file is loaded directly.
+            dprintf!("WARNING, cantrip-builtins missing in FLASH; ignoring\r\n");
         }
 
         // If we found all of them, boot in Shodan mode.
@@ -36,32 +42,55 @@
         let sel4_segments = elf_loader::elf_get_segments(sel4_elf);
         let capdl_segments = elf_loader::elf_get_segments(capdl_elf);
 
-        let sel4_pend = round_up_to_page(elf_loader::elf_phys_max(sel4_segments));
+        let ui_p_reg_start = round_up_to_page(elf_loader::elf_phys_max(sel4_segments));
 
         dprintf!("Loading capdl-loader to the page after seL4\n");
         elf_loader::load_elf_segments(
             capdl_elf.as_ref().unwrap(),
-            sel4_pend - elf_loader::elf_phys_min(capdl_segments),
+            ui_p_reg_start - elf_loader::elf_phys_min(capdl_segments),
         );
 
+        if builtins_size != 0 {
+            tar_loader::copy_file("cantrip-builtins", 0x50380000);
+        }
+
         dprintf!("Starting management core\n");
 
         let entry_point: u32 = (*sel4_elf).e_entry
-            - (elf_loader::elf_virt_min(sel4_segments)
-                - elf_loader::elf_phys_min(sel4_segments));
+            - (elf_loader::elf_virt_min(sel4_segments) - elf_loader::elf_phys_min(sel4_segments));
 
-        let message : [u32; 4] = [
-            sel4_pend,
-            sel4_pend + round_up_to_page(elf_loader::elf_phys_max(capdl_segments) - elf_loader::elf_phys_min(capdl_segments)),
-            sel4_pend - elf_loader::elf_phys_min(capdl_segments),
+        smc_send_bootmsg(mailbox, [
+            ui_p_reg_start,
+            ui_p_reg_start
+                + round_up_to_page(
+                    elf_loader::elf_phys_max(capdl_segments)
+                        - elf_loader::elf_phys_min(capdl_segments),
+                ),
+            ui_p_reg_start - elf_loader::elf_phys_min(capdl_segments),
             (*capdl_elf).e_entry,
-        ];
-        let _ = mailbox.send_message_sync(16, core::mem::transmute(message.as_ref()));
-        dprintf!("seL4 boot message posted\n");
+        ]);
 
         SMC_CONTROL_BLOCK.write_volatile(entry_point);
+    }
+}
 
-        // This message is checked in shodan_boot.robot - keep in sync.
-        dprintf!("load_sel4() completed successfully\n");
+pub fn smc_send_bootmsg(mailbox: &'static dyn MailboxHAL, message: [u32; 4]) {
+    unsafe {
+        let _ = mailbox.send_message_sync(16, core::mem::transmute(message.as_ref()));
+    }
+}
+
+pub fn smc_ram_memcpy(src: &mut [u8], dst: u32, count: usize) {
+    unsafe {
+        core::ptr::copy_nonoverlapping::<u8>(
+            core::mem::transmute(src.as_ptr()),
+            core::mem::transmute(dst),
+            count,
+        );
+    }
+}
+pub fn smc_ram_zero(dst: u32, count: usize) {
+    unsafe {
+        core::ptr::write_bytes::<u8>(core::mem::transmute(dst), 0, count);
     }
 }