diff --git a/scripts/dot_from_switcher.lua b/scripts/dot_from_switcher.lua
new file mode 100644
index 0000000..387ec66
--- /dev/null
+++ b/scripts/dot_from_switcher.lua
@@ -0,0 +1,414 @@
+#!/usr/bin/env lua5.3
+-- Copyright CHERIoT Contributors.
+-- SPDX-License-Identifier: MIT
+
+local infile = io.input()
+
+local labels = {}     -- label |-> style array
+local label_outs = {} -- label |-> label |-> style
+local label_ins = {}  -- label |-> label |-> ()
+
+local label_irq_assume  = {}  -- label |-> { "deferred", "enabled" }
+local label_irq_require = {}  -- label |-> { "deferred", "enabled" }
+
+local exports = {}    -- label |-> ()
+
+local lastlabels = {}
+
+local function debug() end
+if true then
+  function debug(...)
+    io.stderr:write(string.format("DBG %s\n",
+                                  table.concat(table.pack(...), " ")))
+  end
+end
+
+local function end_label(clear)
+  -- At the end of a lable, if we haven't been told that we've assumed a
+  -- different IRQ disposition than required on the way in, then inherit
+  -- assumptions from requirements
+  local lastlabel = lastlabels[#lastlabels]
+  if label_irq_assume[lastlabel] == nil then
+    label_irq_assume[lastlabel] =
+     assert(label_irq_require[lastlabel],
+      "Missing IRQ requirement for prior label, cannot inherit assumption")
+  end
+
+  if clear then lastlabels = {} end
+end
+
+local function found_label(label, where)
+  assert(label)
+  assert(where)
+
+  assert(labels[label] == nil, label)
+  labels[label] = { ("tooltip=%s"):format(where) }
+
+  if label_ins[label] == nil then
+    label_ins[label] = {}
+  end
+
+  if label_outs[label] == nil then
+    label_outs[label] = {}
+  end
+
+  if #lastlabels > 0 then end_label(false) end
+
+  table.insert(lastlabels, label)
+  if #lastlabels > 2 then table.remove(lastlabels, 1) end
+  assert(#lastlabels <= 2)
+end
+
+local function found_edge_from(from, to, style)
+  assert(from)
+  assert(to)
+
+  debug("", "EDGE FROM", from, to)
+
+  if label_outs[from] == nil then label_outs[from] = {} end
+  label_outs[from][to] = {style}
+end
+
+local function found_edge_to(from, to)
+  assert(from)
+  assert(to)
+
+  debug("", "EDGE TO", from, to)
+
+  if label_ins[to] == nil then label_ins[to] = {} end
+  label_ins[to][from] = true
+end
+
+local lineix = 1
+
+-- Read and discard until we get to the good stuff
+for line in infile:lines("*l") do
+  debug("HUNT", line)
+  if line:match(".globl __Z26compartment_switcher_entryz") then break end
+  lineix = lineix + 1
+end
+
+local IRQ_dispositions =
+  { ["any"] = true
+  , ["deferred"] = true
+  , ["enabled"] = true
+  }
+
+-- And here we go
+for line in infile:lines("*l") do
+  local label
+
+  debug("LINE", line)
+
+  -- numeric labels are suppresed
+  label = line:match("^(%d+):$")
+  if label then
+    debug("", "Numeric label")
+    goto nextline
+  end
+
+  -- local labels
+  label = line:match("^(%.L.*):$")
+  if label then
+    debug("", "Local label")
+    found_label(label, lineix)
+    if #lastlabels > 1 then
+      found_edge_to(lastlabels[#lastlabels-1], lastlabels[#lastlabels])
+    end
+    goto nextline
+  end
+
+  -- documentation-only labels
+  label = line:match("^//(%.L.*):$")
+  if label then
+    debug("", "Documentation label", #lastlabels)
+    found_label(label, lineix)
+
+    -- Documentation labels are presumed to be fall-through and do not need the
+    -- clutter of "FROM: above"
+    assert(#lastlabels > 1)
+    found_edge_from(lastlabels[#lastlabels-1], lastlabels[#lastlabels])
+    found_edge_to(lastlabels[#lastlabels-1], lastlabels[#lastlabels])
+
+    -- Documentation labels are presumed to inherit the IRQ disposition from
+    -- "above" as well.
+    label_irq_require[lastlabels[#lastlabels]] =
+      assert(label_irq_assume[lastlabels[#lastlabels-1]],
+             "Missing IRQ disposition for prior label")
+
+    goto nextline
+  end
+
+  -- other global labels
+  label = line:match("^([%w_]*):$")
+  if label then
+    debug("", "global label")
+    found_label(label, lineix)
+    if #lastlabels > 1 then
+      found_edge_to(lastlabels[#lastlabels-1], lastlabels[#lastlabels])
+    end
+    exports[label] = true
+    goto nextline
+  end
+
+  -- [cm]ret clear the last label, preventing fallthru
+  if line:match("^%s+[cm]ret$") then
+    debug("", "[cm]ret")
+    end_label(true)
+    goto nextline
+  end
+
+  -- unconditonal jumps add an edge and clear the last label, since we cannot
+  -- be coming "FROM: above"
+  label = line:match("^%s+j%s+(%g*)$")
+  if label then
+    debug("", "Jump")
+    assert(#lastlabels > 0)
+    found_edge_to(lastlabels[#lastlabels], label)
+    end_label(true)
+    goto nextline
+  end
+
+  -- branches add edges to local labels
+  label = line:match("^%s+b.*,%s*(%.L%g*)$")
+  if label then
+    debug("", "Branch")
+    assert(#lastlabels > 0)
+    found_edge_to(lastlabels[#lastlabels], label)
+    goto nextline
+  end
+
+  -- OK, now hunt for structured comments.
+  line = line:match("^%s*%*%s*(%S.*)$") or line:match("^%s*//%s*(%S.*)$")
+  if not line then goto nextline end
+
+  -- "FROM: malice" annotations promote lastlabel to being exported
+  label = line:match("^FROM:%s+malice%s*")
+  if label then
+    debug("", "Malice", #lastlabels)
+    assert(#lastlabels > 0)
+    exports[lastlabels[#lastlabels]] = true
+    goto nextline
+  end
+
+  -- "FROM: above"
+  label = line:match("^FROM:%s+above%s*")
+  if label then
+    debug("", "Above")
+    assert(#lastlabels > 1)
+    found_edge_from(lastlabels[#lastlabels-1], lastlabels[#lastlabels])
+
+    -- "FROM: above" implies IRQ requirements, too
+    label_irq_require[lastlabels[#lastlabels]] =
+      assert(label_irq_assume[lastlabels[#lastlabels-1]],
+             "Missing IRQ disposition for prior label")
+
+    goto nextline
+  end
+
+  -- "IFROM: above"
+  label = line:match("^IFROM:%s+above%s*")
+  if label then
+    debug("", "Above")
+    assert(#lastlabels > 1)
+    found_edge_from(lastlabels[#lastlabels-1],
+                    lastlabels[#lastlabels],
+                    "style=dashed")
+
+    -- "IFROM: above" implies IRQ requirements, too
+    label_irq_require[lastlabels[#lastlabels]] =
+      assert(label_irq_assume[lastlabels[#lastlabels-1]],
+             "Missing IRQ disposition for prior label")
+
+    goto nextline
+  end
+
+  -- "FROM: cross-call" no-op
+  label = line:match("^FROM:%s+cross%-call%s*")
+  if label then
+    goto nextline
+  end
+
+  -- "FROM: interrupt" no-op
+  label = line:match("^FROM:%s+interrupt%s*")
+  if label then
+    goto nextline
+  end
+
+  -- "FROM: error" no-op
+  label = line:match("^FROM:%s+interrupt%s*")
+  if label then
+    goto nextline
+  end
+
+  -- "FROM: $symbol"
+  label = line:match("^FROM:%s+(%S+)%s*")
+  if label then
+    debug("", "FROM", lastlabels[#lastlabels], label)
+    assert(#lastlabels > 0)
+    found_edge_from(label, lastlabels[#lastlabels])
+    goto nextline
+  end
+
+  -- "IFROM: $symbol"
+  label = line:match("^IFROM:%s+(%S+)%s*")
+  if label then
+    debug("", "IFROM", lastlabels[#lastlabels], label)
+    assert(#lastlabels > 0)
+    found_edge_from(label, lastlabels[#lastlabels], "style=dashed")
+    goto nextline
+  end
+
+  -- "IFROM: $symbol"
+  label = line:match("^ITO:%s+(%S+)%s*")
+  if label then
+    debug("", "ITO", lastlabels[#lastlabels], label)
+    assert(#lastlabels > 0)
+    found_edge_to(lastlabels[#lastlabels], label, "style=dashed")
+    goto nextline
+  end
+
+  -- "IRQ ASSUME: {deferred,enabled}"
+  label = line:match("^IRQ ASSUME:%s+(%S+)%s*")
+  if label then
+    debug("", "IRQ ASSUME", lastlabels[#lastlabels], label)
+    assert (IRQ_dispositions[label])
+    label_irq_assume[lastlabels[#lastlabels]] = label
+    goto nextline
+  end
+
+  -- "IRQ REQURE: {deferred,enabled}"
+  label = line:match("^IRQ REQUIRE:%s+(%S+)%s*")
+  if label then
+    debug("", "IRQ", lastlabels[#lastlabels], label)
+    assert (IRQ_dispositions[label])
+    label_irq_require[lastlabels[#lastlabels]] = label
+    goto nextline
+  end
+
+  -- Stop reading when we get to the uninteresting library exports
+  if line:match("Switcher%-exported library functions%.$") then
+    debug("", "Break")
+    break
+  end
+
+  ::nextline::
+  lineix = lineix + 1
+end
+
+-- Take adjacency matrix representation and add lists.
+label_inls = {}
+label_outls = {}
+for focus, _ in pairs(labels) do
+  label_inls[focus] = {}
+  label_outls[focus] = {}
+
+  for from, _ in pairs(label_ins[focus]) do
+    assert(labels[from])
+    assert(label_outs[from][focus],
+      string.format("%s in from %s but no out edge", focus, from))
+    assert(   label_irq_require[focus] == "any"
+           or label_irq_assume[from] == label_irq_require[focus],
+           string.format("IRQ-invalid arc from %s (%s) to %s (%s)",
+             from, label_irq_assume[from], focus, label_irq_require[focus]))
+
+    table.insert(label_inls[focus], from)
+  end
+  for to, _ in pairs(label_outs[focus]) do
+    assert(labels[to])
+    assert(label_ins[to][focus],
+      string.format("%s out to %s but no in edge", focus, to))
+    assert(   label_irq_require[to] == "any"
+           or label_irq_assume[focus] == label_irq_require[to],
+           string.format("IRQ-invalid arc from %s (%s) to %s (%s)",
+             focus, label_irq_assume[focus], to, label_irq_require[to]))
+
+    table.insert(label_outls[focus], to)
+  end
+end
+
+local function render_exports(...)
+  local args = {...}
+
+  local nexports = 0
+  for export, _ in pairs(exports) do nexports = nexports + 1 end
+  assert(nexports == #args,
+         ("Wrong number of exports: %d != %d"):format(nexports, #args))
+
+  print(" { rank=min; edge [style=invis]; ")
+
+  for _, export in ipairs(args) do
+    assert(exports[export], "Purported export isn't")
+    print("", ("%q"):format(export), ";")
+  end
+
+  for i = 1, #args-1 do
+    print("", ("%q -> %q ;"):format(args[i], args[i+1]))
+  end
+
+  print(" }")
+end
+
+print("digraph switcher {")
+
+-- Put all our exports at the top of the graph, in a fixed order.
+render_exports(".Lhandle_error_handler_return",
+               "exception_entry_asm",
+               "switcher_after_compartment_call",
+               "__Z26compartment_switcher_entryz")
+
+for from, from_params in pairs(labels) do
+
+  if exports[from] then
+    table.insert(from_params, "shape=box")
+  elseif #label_inls[from] == 1 then
+    -- Indegree 1, this is either an exit, a decision node, or just a waypoint
+    if #label_outls[from] == 0 then
+      -- Exit
+      table.insert(from_params, "shape=octagon")
+    elseif #label_outls[from] == 1 then
+      -- Waypoint
+      table.insert(from_params, "shape=oval")
+    else
+      -- Decision
+      table.insert(from_params, "shape=trapezium")
+    end
+  else
+    if #label_outls[from] == 0 then
+      -- Exit
+      table.insert(from_params, "shape=octagon")
+    elseif #label_outls[from] == 1 then
+      table.insert(from_params, "shape=invtrapezium")
+    else
+      table.insert(from_params, "shape=hexagon")
+    end
+  end
+
+  table.insert(from_params,
+    ({ ["any"] = "fontname=\"Times\""
+    , ["deferred"] = "fontname=\"Times-Bold\""
+    , ["enabled"] = "fontname=\"Times-Italic\""
+    })[label_irq_assume[from]])
+
+  if    from:match("^%.?L?switch")
+     or from == "__Z26compartment_switcher_entryz" then
+    table.insert(from_params, "style=filled")
+    table.insert(from_params, "fillcolor=cyan")
+  elseif from:match("^%.?L?exception") then
+    table.insert(from_params, "style=filled")
+    table.insert(from_params, "fillcolor=red")
+  elseif from:match("^%.?L?handle") then
+    table.insert(from_params, "style=filled")
+    table.insert(from_params, "fillcolor=orange")
+  end
+
+  print("", ("%q [%s];"):format(from, table.concat(from_params,",")))
+
+  for to, style in pairs(label_outs[from]) do
+    print("", ("%q"):format(from),
+              ("-> %q [%s];"):format(to, table.concat(style,",")))
+  end
+  print("")
+end
+
+print("}")
diff --git a/sdk/boards/sonata-0.2.json b/sdk/boards/sonata-0.2.json
index 308904a..9747b93 100644
--- a/sdk/boards/sonata-0.2.json
+++ b/sdk/boards/sonata-0.2.json
@@ -76,6 +76,7 @@
         "ipconfigDRIVER_INCLUDED_TX_IP_CHECKSUM=1"
     ],
     "driver_includes" : [
+        "../include/platform/sunburst/v0.2",
         "../include/platform/sunburst",
         "../include/platform/generic-riscv"
     ],
diff --git a/sdk/boards/sonata-prerelease.json b/sdk/boards/sonata-prerelease.json
index d82e122..01b4058 100644
--- a/sdk/boards/sonata-prerelease.json
+++ b/sdk/boards/sonata-prerelease.json
@@ -4,9 +4,21 @@
             "start" : 0x30000000,
             "end"   : 0x30004000
         },
-        "gpio" : {
-            "start" : 0x80000000,
-            "end"   : 0x80000020
+        "pwm": {
+            "start" : 0x80001000,
+            "length": 0x00001000
+        },
+        "rgbled" : {
+            "start" : 0x80009000,
+            "end"   : 0x80009020
+        },
+        "revoker": {
+            "start" : 0x8000A000,
+            "length": 0x00001000
+        },
+        "adc": {
+            "start" : 0x8000B000,
+            "length": 0x00001000
         },
         "clint": {
             "start" : 0x80040000,
@@ -24,53 +36,13 @@
             "start" : 0x80102000,
             "end"   : 0x80102034
         },
-        "uart3": {
-            "start" : 0x80103000,
-            "end"   : 0x80103034
-        },
-        "uart4": {
-            "start" : 0x80104000,
-            "end"   : 0x80104034
-        },
-        "i2c0": {
-            "start" : 0x80200000,
-            "end"   : 0x80200080
-        },
-        "i2c1": {
-            "start" : 0x80201000,
-            "end"   : 0x80201080
-        },
-        "spi0": {
-            "start" : 0x80300000,
-            "end"   : 0x80301000
-        },
-        "spi1": {
-            "start" : 0x80301000,
-            "end"   : 0x80302000
-        },
-        "spi2": {
-            "start" : 0x80302000,
-            "end"   : 0x80303000
-        },
-        "rgbled" : {
-            "start" : 0x80009000,
-            "end"   : 0x80009020
-        },
-        "revoker": {
-            "start": 0x8000A000,
-            "length": 0x1000
+        "usbdev": {
+            "start" : 0x80400000,
+            "end"   : 0x80401000
         },
         "plic": {
             "start" : 0x88000000,
             "end"   : 0x88400000
-        },
-        "pwm": {
-            "start" : 0x80001000,
-            "length": 0x00001000
-        },
-        "adc": {
-            "start" : 0x8000B000,
-            "length": 0x00001000
         }
     },
     "instruction_memory": {
@@ -94,7 +66,7 @@
         "../include/platform/ibex",
         "../include/platform/generic-riscv"
     ],
-    "timer_hz" : 30000000,
+    "timer_hz" : 40000000,
     "tickrate_hz" : 100,
     "revoker" : "hardware",
     "stack_high_water_mark" : true,
@@ -102,62 +74,69 @@
     "simulation": false,
     "interrupts": [
         {
-            "name": "Uart0TxWatermark",
+            "name": "RevokerInterrupt",
             "number": 1,
-            "priority": 3,
-            "edge_triggered": true
-        },
-        {
-            "name": "Uart0RxWatermark",
-            "number": 2,
-            "priority": 3,
-            "edge_triggered": true
-        },
-        {
-            "name": "Uart0TxEmpty",
-            "number": 3,
-            "priority": 3,
-            "edge_triggered": true
-        },
-        {
-            "name": "Uart0RxOverflow",
-            "number": 4,
-            "priority": 3,
-            "edge_triggered": true
-        },
-        {
-            "name": "Uart1TxWatermark",
-            "number": 9,
-            "priority": 3,
-            "edge_triggered": true
-        },
-        {
-            "name": "Uart1RxWatermark",
-            "number": 10,
-            "priority": 3,
-            "edge_triggered": true
-        },
-        {
-            "name": "Uart1TxEmpty",
-            "number": 11,
-            "priority": 3,
-            "edge_triggered": true
-        },
-        {
-            "name": "Uart1RxOverflow",
-            "number": 12,
-            "priority": 3,
-            "edge_triggered": true
+            "priority": 2
         },
         {
             "name": "EthernetInterrupt",
-            "number": 47,
+            "number": 2,
             "priority": 3
         },
         {
-            "name": "RevokerInterrupt",
-            "number": 72,
-            "priority": 2
+            "name": "UsbDevInterrupt",
+            "number": 3,
+            "priority": 3
+        },
+        {
+            "name": "Uart0Interrupt",
+            "number": 8,
+            "priority": 3
+        },
+        {
+            "name": "Uart1Interrupt",
+            "number": 9,
+            "priority": 3
+        },
+        {
+            "name": "Uart2Interrupt",
+            "number": 10,
+            "priority": 3
+        },
+        {
+            "name": "I2c0Interrupt",
+            "number": 16,
+            "priority": 3
+        },
+        {
+            "name": "I2c1Interrupt",
+            "number": 17,
+            "priority": 3
+        },
+        {
+            "name": "SpiLcdInterrupt",
+            "number": 24,
+            "priority": 3
+        },
+        {
+            "name": "SpiEthmacInterrupt",
+            "number": 25,
+            "priority": 3
+        },
+        {
+            "name": "Spi0Interrupt",
+            "number": 26,
+            "priority": 3
+        },
+        {
+            "name": "Spi1Interrupt",
+            "number": 27,
+            "priority": 3
+        },
+        {
+            "name": "Spi2Interrupt",
+            "number": 28,
+            "priority": 3
         }
     ]
 }
diff --git a/sdk/core/allocator/alloc.h b/sdk/core/allocator/alloc.h
index 8ab0c09..69f2726 100644
--- a/sdk/core/allocator/alloc.h
+++ b/sdk/core/allocator/alloc.h
@@ -683,6 +683,8 @@
 // the minimum size of a chunk (excluding the header)
 constexpr size_t MinRequest = MinChunkSize - sizeof(MChunkHeader);
 
+static_assert(MinChunkSize == CHERIOTHeapMinChunkSize);
+
 // true if cap address a has acceptable alignment
 static inline bool is_aligned(CHERI::Capability<void> a)
 {
diff --git a/sdk/core/loader/boot.cc b/sdk/core/loader/boot.cc
index e41038a..bc67535 100644
--- a/sdk/core/loader/boot.cc
+++ b/sdk/core/loader/boot.cc
@@ -460,7 +460,7 @@
 	 * The sealing key for the switcher, used to seal all jump targets in the
 	 * import tables.
 	 */
-	Capability<void> switcherKey;
+	Capability<void> exportSealingKey;
 
 	/**
 	 * The sealing key for sealing trusted stacks.
@@ -568,7 +568,7 @@
 			                 "Functions exported from compartments must have "
 			                 "an explicit interrupt posture");
 			return build(compartment.exportTable, entry.address)
-			  .seal(switcherKey);
+			  .seal(exportSealingKey);
 		};
 
 		// If the low bit is 1, then this is either an MMIO region or direct
@@ -596,9 +596,9 @@
 			{
 				if (contains<ExportEntry>(lib.exportTable, possibleLibcall))
 				{
-					// TODO: Library export tables are not used after the
-					// loader has run, we could move them to the end of the
-					// image and make that space available for the heap.
+					// Library export tables are not used after the loader has
+					// run; our linker script places them to the end of the
+					// image, which we make available for the heap.
 					return createLibCall(build_pcc(lib));
 				}
 			}
@@ -850,6 +850,8 @@
 		 * than by fiat of initial construction.  The switcher will detect the
 		 * trusted stack underflow and will signal the scheduler that the thread
 		 * has exited and should not be brought back on core.
+		 *
+		 * See core/switcher/entry.S:/^switcher_after_compartment_call.
 		 */
 		auto threadInitialReturn =
 		  build<void, Root::Type::Execute, SwitcherPccPermissions>(
@@ -1250,24 +1252,46 @@
 	  };
 
 	// Set up the sealing keys for the privileged components.
-	switcherKey =
-	  setSealingKey(imgHdr.switcher, Sentry, SealedTrustedStacks - Sentry + 1);
-	// We need only the rights to seal things with the switcher's data sealing
-	// types, so drop all others and store those two types separately.
-	trustedStackKey           = switcherKey;
-	trustedStackKey.address() = SealedTrustedStacks;
-	trustedStackKey.bounds()  = 1;
-	switcherKey.address()     = SealedImportTableEntries;
-	switcherKey.bounds()      = 1;
-	setSealingKey(imgHdr.allocator(), Allocator);
+	exportSealingKey = CHERI::Capability{
+	  build<void,
+	        Root::Type::Seal,
+	        PermissionSet{Permission::Global, Permission::Seal}>(
+	    SealedImportTableEntries, 1)};
+
+	// We and the switcher both seal (and the switcher unseals) trusted stacks
+	trustedStackKey = setSealingKey(imgHdr.switcher, SealedTrustedStacks, 1, 0);
+	// The switcher unseals import entries built with exportSealingKey above
+	setSealingKey(imgHdr.switcher,
+	              SealedImportTableEntries,
+	              1,
+	              sizeof(void *),
+	              PermissionSet{Permission::Global, Permission::Unseal});
+
+	/*
+	 * The token library unseals both static and dynamic objects, sometimes
+	 * either and sometimes with static knowledge of which is expected.  To
+	 * avoid `li; csetaddr; csetbounds` sequences, we give it a separate cap
+	 * for each case.
+	 */
 	setSealingKey(imgHdr.token_library(),
 	              Allocator,
 	              2, // Allocator and StaticToken
 	              0,
 	              PermissionSet{Permission::Global, Permission::Unseal});
+	setSealingKey(imgHdr.token_library(),
+	              StaticToken,
+	              1,
+	              sizeof(void *),
+	              PermissionSet{Permission::Global, Permission::Unseal});
+	setSealingKey(imgHdr.token_library(),
+	              Allocator,
+	              1,
+	              2 * sizeof(void *),
+	              PermissionSet{Permission::Global, Permission::Unseal});
+
 	constexpr size_t DynamicSealingLength =
 	  std::numeric_limits<ptraddr_t>::max() - FirstDynamicSoftware + 1;
-
+	setSealingKey(imgHdr.allocator(), Allocator);
 	setSealingKey(imgHdr.allocator(),
 	              FirstDynamicSoftware,
 	              DynamicSealingLength,
diff --git a/sdk/core/loader/types.h b/sdk/core/loader/types.h
index 7a29847..3b96b39 100644
--- a/sdk/core/loader/types.h
+++ b/sdk/core/loader/types.h
@@ -365,6 +365,7 @@
 			/**
 			 * The PCC-relative location of the cross-compartment call return
 			 * path, used to build the initial return addresses for threads.
+			 * That is, "switcher_after_compartment_call".
 			 */
 			uint16_t crossCallReturnEntry;
 
@@ -1097,7 +1098,7 @@
 
 		/**
 		 * Flags.  The low three bits indicate the number of registers that
-		 * should be cleared in the compartment switcher.  The next two bits
+		 * should be passed in the compartment switcher.  The next two bits
 		 * indicate the interrupt status.  The remaining three are currently
 		 * unused.
 		 */
diff --git a/sdk/core/switcher/entry.S b/sdk/core/switcher/entry.S
index 387a2d1..b139892 100644
--- a/sdk/core/switcher/entry.S
+++ b/sdk/core/switcher/entry.S
@@ -45,6 +45,49 @@
  * purpose, &c), one should not read too much of the psABI calling convention
  * into the code here.  Within the switcher, the machine is a raw register
  * machine and C is a distant, high-level language.
+ *
+ * Since this is the part of the map labeled "here be dragons", we have added
+ * "Register Atlas" comments throughout.  Lines within an atlas consist of a
+ * comma-whitespace-separated list of registers, a colon, and descriptive text.
+ * In general, atlases should cover all (including dead) registers.  Point
+ * changes to the atlas are denoted with "Atlas update", to emphasize that
+ * registers not named are not dead but instead retain their meaning from the
+ * last full atlas.
+ *
+ * Labels associated with interesting control flow are annotated with
+ *
+ *  - "FROM:", which may be repeated once for each predecessor label or these:
+ *    - "above": the immediately prior block
+ *    - "cross-call": untrusted code making a cross-compartment call
+ *    - "malice": untrusted code outside the switcher
+ *    - "interrupt": an asynchronous external event
+ *    - "error": a trap from within the switcher
+ *
+ *  - "IFROM:", which indicates an indirect transfer of control (through cjalr
+ *    or mepcc/mret, for example).
+ *
+ *  - "ITO:", the other direction of "IFROM:"
+ *
+ *  - "IRQ ASSUME:", "any", "deferred" or "enabled".  This declares the state of
+ *    the machine, either from explicit instructions or implicit aspects of the
+ *    architecture.
+ *
+ *  - "IRQ REQUIRE:", "any", "deferred" or "enabled".  If not "any", then all
+ *    paths into this label must have the indicated IRQ disposition.
+ *
+ *  - "LIVE IN:", a list of live (in) registers at this point of the code and/or
+ *    - "*": the entire general purpose register file (no CSRs or SCRs implied)
+ *    - "mcause"
+ *    - "mtdc"
+ *    - "mtval"
+ *    - "mepcc"
+ *
+ * Control flow instructions may be annotated with "LIVE OUT:" labels.  These
+ * capture the subset of live registers meant to be available to the target.
+ *
+ * For all annotations, optional commentary given in parentheses and may
+ * continue onto adjacent lines.
+ *
  */
 
 switcher_code_start:
@@ -54,24 +97,28 @@
 	.globl compartment_switcher_sealing_key
 	.p2align 3
 compartment_switcher_sealing_key:
+.Lsealing_key_trusted_stacks:
+	.long 0
+	.long 0
+.Lunsealing_key_import_tables:
 	.long 0
 	.long 0
 # Global for the scheduler's PCC.  Stored in the switcher's code section.
-.section .text, "ax", @progbits
+	.section .text, "ax", @progbits
 	.globl switcher_scheduler_entry_pcc
 	.p2align 3
 switcher_scheduler_entry_pcc:
 	.long 0
 	.long 0
 # Global for the scheduler's CGP.  Stored in the switcher's code section.
-.section .text, "ax", @progbits
+	.section .text, "ax", @progbits
 	.globl switcher_scheduler_entry_cgp
 	.p2align 3
 switcher_scheduler_entry_cgp:
 	.long 0
 	.long 0
 # Global for the scheduler's CSP.  Stored in the switcher's code section.
-.section .text, "ax", @progbits
+	.section .text, "ax", @progbits
 	.globl switcher_scheduler_entry_csp
 	.p2align 2
 switcher_scheduler_entry_csp:
@@ -121,32 +168,11 @@
 .endm
 
 /**
- * Verify the compartment stack is valid, with the expected permissions and
- * unsealed.
- * This macro assumes t2 and tp are available to use.
- */
-.macro check_compartment_stack_integrity reg
-	// Check that the caller's CSP is a tagged, unsealed capability (with at
-	// least load permission - we'll check the other permissions properly
-	// later) by loading a byte.  If this doesn't work, we'll fall off this
-	// path into the exception handler and force unwind.
-	clb                t2, 0(\reg)
-	// make sure the caller's CSP has the expected permissions
-	cgetperm           t2, \reg
-	li                 tp, COMPARTMENT_STACK_PERMISSIONS
-	bne                tp, t2, .Lforce_unwind
-	// Check that the top and base are 16-byte aligned
-	cgetbase           t2, csp
-	or                 t2, t2, sp
-	andi               t2, t2, 0xf
-	bnez               t2, .Lforce_unwind
-.endm
-
-/**
  * Zero the stack.  The three operands are the base address, the top address,
  * and a scratch register to use.  The base must be a capability but it must
  * be provided without the c prefix because it is used as both a capability
- * and integer register.  All three registers are clobbered.
+ * and integer register.  All three registers are clobbered but should not be
+ * considered safe to expose outside the TCB.
  */
 .macro zero_stack base top scratch
 	addi               \scratch, \top, -32
@@ -169,9 +195,12 @@
 .endm
 
 /**
- * Clear the hazard pointers associated with this thread.  We don't care about
- * leaks here (they're store-only from anywhere except the allocator), so just
- * write a 32-bit zero over half of each one to clobber the tags.
+ * Clear the hazard pointers associated with this thread.  (See
+ * include/stdlib.h:/heap_claim_fast, and its implementation in
+ * lib/compartment_helpers/claim_fast.cc for more about hazard pointers.)  We
+ * don't care about leaks here (they're store-only from anywhere except the
+ * allocator), so just write a 32-bit zero over half of each one to clobber the
+ * tags.
  */
 .macro clear_hazard_slots trustedStack, scratch
 	clc                \scratch, TrustedStack_offset_hazardPointers(\trustedStack)
@@ -185,99 +214,293 @@
 	.type __Z26compartment_switcher_entryz,@function
 __Z26compartment_switcher_entryz:
 	/*
-	 * Spill caller-save registers carefully.  If we find ourselves unable to do
-	 * so, we'll return an error to the caller (via the exception path; see
-	 * .Lhandle_error_in_switcher).  The error handling path assumes that the
-	 * first spill is to the lowest address and guaranteed to trap if any would.
+	 * FROM: cross-call
+	 * FROM: malice
+	 * IRQ ASSUME: deferred (exposed as IRQ-deferring sentry; see the 'export'
+	 *             macro at the end of this file)
+	 * LIVE IN: mtdc, ra, sp, gp, s0, s1, t0, t1, a0, a1, a2, a3, a4, a5
+	 *          (that is, all registers except tp and t2)
+	 *
+	 * Atlas:
+	 *  mtdc: pointer to this thread's TrustedStack
+	 *        (may be 0 from buggy/malicious scheduler thread)
+	 *  ra: caller return address
+	 *      (at the moment, this is ensured because we enter via an
+	 *      IRQ-disabling forward sentry, which requires ra as the destination
+	 *      register of the cjalr the caller used, but we are not relying on
+	 *      this property, and we hope to relax the switcher's IRQ posture)
+	 *  sp: nominally, caller's stack pointer; will check integrity below
+	 *  gp: caller state, to be spilled, value unused in switcher
+	 *  s0, s1: caller state, to be spilled, value unused in switcher
+	 *  t0: possible caller argument to callee, passed or zered in switcher
+	 *      (specifically, this is the pointer to arguments beyond a0-a5 and/or
+	 *      variadic arguments)
+	 *  t1: sealed export table entry for the target callee
+	 *      (see LLVM's RISCVExpandPseudo::expandCompartmentCall and, more
+	 *      generally, the ABI chapter of the CHERIoT ISA document,
+	 *      https://cheriot.org/cheriot-sail/cheriot-architecture.pdf)
+	 *  a0, a1, a2, a3, a4, a5: possible caller arguments to callee, passed or
+	 *                          zeroed in switcher.
+	 *  tp, t2: dead
+	 */
+	/*
+	 * By virtue of making a call, the caller is indicating that all caller-save
+	 * registers are dead.  Because we are crossing a trust boundary, the
+	 * switcher must spill callee-save registers.  If we find ourselves unable
+	 * to do so for "plausibly accidental" reasons, we'll return an error to the
+	 * caller (via the exception path; see .Lhandle_error_in_switcher).
+	 * Specifically, the first spill here is to the lowest address and so
+	 * guaranteed to raise a bounds fault if any of the stores here would access
+	 * below the base (lowest address) of the stack capability.
+	 *
+	 * Certain other kinds of less plausibly accidental malice (for example, an
+	 * untagged or sealed or SD-permission-less capability in sp) will also be
+	 * caught by this first spill.  In some sense we should forcibly unwind the
+	 * caller, but it's acceptable, in the sense that no would-be-callee can be
+	 * harmed, to just return an error instead.
+	 *
+	 * Yet other kinds of less plausibly accidental malice can survive the first
+	 * spill.  For example, consider a MC-permission-less capability in sp and a
+	 * non-capability value in s0.  While the first spill will not trap, these
+	 * forms of malice will certainly be detected in a few instructions, when we
+	 * scrutinize sp in detail.  They might (or might not) cause an intervening
+	 * (specifically, spill) instruction to trap.  Either way will result in us
+	 * ending up in .Lcommon_force_unwind, either directly or via the exception
+	 * handler.
+	 *
+	 * At entry, the register file is safe to expose to the caller, and so if
+	 * and when we take the "just return an error" option, no changes, beyond
+	 * populating the error return values in a0 and a1, are required.
+	 */
+	/*
+	 * TODO: We'd like to relax the interrupt posture of the switcher where
+	 * possible.  Specifically, unless both the caller and callee are running
+	 * and to be run with interrupts deferred, we'd like the switcher, and
+	 * especially its stack-zeroing, to be preemtable.
 	 */
 	cincoffset        ct2, csp, -SPILL_SLOT_SIZE
-.Lswitcher_entry_first_spill:
+.Lswitch_entry_first_spill:
+	/*
+	 * FROM: above
+	 * ITO: .Lswitch_just_return (via .Lhandle_error_in_switcher)
+	 */
 	csc               cs0, SPILL_SLOT_cs0(ct2)
 	csc               cs1, SPILL_SLOT_cs1(ct2)
 	csc               cgp, SPILL_SLOT_cgp(ct2)
 	csc               cra, SPILL_SLOT_pcc(ct2)
 	cmove             csp, ct2
-	// before we access any privileged state, we can verify the
-	// compartment's csp is valid. If not, force unwind.
-	// Note that this check is purely to protect the callee, not the switcher
-	// itself.
-	check_compartment_stack_integrity csp
-	// The caller should back up all callee saved registers.
+	/*
+	 * Atlas update:
+	 *  ra, gp, s0, s1: dead (presently, redundant caller values)
+	 *  t2: dead (presently, a copy of csp)
+	 */
+
+	/*
+	 * Before we access any privileged state, we can verify the compartment's
+	 * csp is valid. If not, force unwind.  Note that these checks are purely to
+	 * protect the callee, not the switcher itself, which can always bail and
+	 * forcibly unwind the caller.
+	 *
+	 * Make sure the caller's CSP has the expected permissions (including that
+	 * it is a stack pointer, by virtue of being local and bearing SL) and that
+	 * its top and base are at least 16-byte aligned.  We have already checked
+	 * that it is tagged and unsealed and at least 8-byte aligned by virtue of
+	 * surviving the stores above.
+	 *
+	 * TODO for formal verification: it should be the case that after these
+	 * tests and the size checks below, no csp-authorized instruction in the
+	 * switcher can fault.
+	 */
+//.Lswitch_csp_check:
+	cgetperm           t2, csp
+	li                 tp, COMPARTMENT_STACK_PERMISSIONS
+	bne                tp, t2, .Lcommon_force_unwind
+	cgetbase           t2, csp
+	or                 t2, t2, sp
+	andi               t2, t2, 0xf
+	bnez               t2, .Lcommon_force_unwind
+	/*
+	 * Atlas update:
+	 *  t2, tp: dead (again)
+	 *  sp: the caller's untrusted stack pointer, now validated and pointing at
+	 *      the callee-save register spill area we made above
+	 */
+
 	// mtdc should always have an offset of 0.
 	cspecialr          ct2, mtdc
-#ifndef NDEBUG
-	// XXX: This line is useless, only for mtdc to show up in debugging.
-	cmove              ct2, ct2
-#endif
-	clear_hazard_slots ct2, ctp
+	// Atlas update: t2: a pointer to this thread's TrustedStack structure
+	/*
+	 * This is our first access via mtdc, and so it might trap, if the scheduler
+	 * tries a cross-compartment call.  That will be a fairly short trip to an
+	 * infinite loop (see commentary in exception_entry_asm).
+	 */
+	clear_hazard_slots /* trusted stack = */ ct2, /* scratch = */ ctp
+	// Atlas update: tp: dead (again)
 
-	// make sure the trusted stack is still in bounds
+//.Lswitch_trusted_stack_push:
+	/*
+	 * TrustedStack::frames[] is a flexible array member at the end of the
+	 * structure, and the stack of frames it represents grows *upwards* (with
+	 * [0] the initial activation, [1] the first cross-compartment call, and so
+	 * on).  Thus, if the frame offset points "one past the end" (or futher
+	 * out), we have no more frames available, so off we go to
+	 * .Lswitch_trusted_stack_exhausted .
+	 */
 	clhu               tp, TrustedStack_offset_frameoffset(ct2)
-	cgetlen            t2, ct2
-	bgeu               tp, t2, .Lout_of_trusted_stack
-	// we are past the stacks checks. Reload ct2; tp is still as it was
-	cspecialr          ct2, mtdc
-	// ctp points to the current available trusted stack frame.
+	cgetlen            s0, ct2
+	/*
+	 * Atlas update:
+	 *  s0: scalar length of the TrustedStack structure
+	 *  tp: scalar offset of the next available TrustedStack::frames[] element
+	 */
+	// LIVE OUT: mtdc, sp
+	bgeu               tp, s0, .Lswitch_trusted_stack_exhausted
+	// Atlas update: s0: dead
+	// we are past the stacks checks.
 	cincoffset         ctp, ct2, tp
+	// Atlas update: tp: pointer to the next available TrustedStackFrame
+	/*
+	 * Populate that stack frame by...
+	 * 1. spilling the caller's stack pointer, as modified by the spills at the
+	 *    start of this function.
+	 */
 	csc                csp, TrustedStackFrame_offset_csp(ctp)
-	// We have just entered this call, so no faults triggered during this call
-	// yet.
+	/*
+	 * 2. zeroing the number of error handler invocations (we have just entered
+	 *    this call, so no faults triggered during this call yet).
+	 */
 	csh                zero, TrustedStackFrame_offset_errorHandlerCount(ctp)
-	// For now, store a null export entry so that we don't ever try to pass
-	// switcher state to an error handler.
+	/*
+	 * 3. For now, store a null export entry.  This is largely cosmetic; we will
+	 *    not attempt to access this value before it is set to the real export
+	 *    table entry below.  Should we trap, the logic at
+	 *    .Lhandle_error_switcher_pcc will cause us to force unwind, popping
+	 *    this frame before any subsequent action.
+	 *
+	 *    TODO for formal verification: prove that this store is dead and can
+	 *    be eliminated.
+	 */
 	csc                cnull, TrustedStackFrame_offset_calleeExportTable(ctp)
+	/*
+	 * Update the frame offset, using s1 to hold a scratch scalar.  Any fault
+	 * before this point (wrong target cap, unaligned stack, etc.) is seen as a
+	 * fault in the caller. After writing the new TrustedSstack::frameoffset,
+	 * any fault is seen as a callee fault.
+	 */
 	clhu               s1, TrustedStack_offset_frameoffset(ct2)
 	addi               s1, s1, TrustedStackFrame_size
-	// Update the frame offset.
-	// Any fault before this point (wrong target cap, unaligned stack, etc.) is
-	// seen as a fault in the caller. From this point after writing the new
-	// tstack offset, any fault is seen as a callee fault.  With a null export
-	// table entry on the trusted stack, a fault here will cause a forced
-	// unwind until we set the correct one.
 	csh                s1, TrustedStack_offset_frameoffset(ct2)
-	// Chop off the stack.
+
+	/*
+	 * Chop off the stack, using...
+	 *  - s0 for the current untrusted stack base address (the lowest address of
+	 *    the register spill we created at .Lswitch_entry_first_spill)
+	 *  - s1 for the length of the stack suffix to which the callee is entitled
+	 */
+//.Lswitch_stack_chop:
 	cgetaddr           s0, csp
 	cgetbase           s1, csp
 	csetaddr           csp, csp, s1
 	sub                s1, s0, s1
 	csetboundsexact    ct2, csp, s1
 	csetaddr           csp, ct2, s0
+	/*
+	 * Atlas:
+	 *  s0: address of stack boundary between caller and callee frames, that is,
+	 *      the lowest address of the register spill from
+	 *      .Lswitch_entry_first_spill)
+	 *  sp: pointer to stack, with its limit and address set to the address in
+	 *      s0.  The base and permissions have not been altered from sp at
+	 *      entry, and the tag remains set since all manipulations have been
+	 *      monotone non-increasing of, and within, bounds.
+	 *  tp: pointer to the freshly populated TrustedStackFrame (still)
+	 *  t1: sealed export table entry for the target callee (still)
+	 *  a0, a1, a2, a3, a4, a5, t0: call argument values / to be zeroed (still)
+	 *  t2, s1: dead (again)
+	 *  ra, gp: dead (still)
+	 */
 #ifdef CONFIG_MSHWM
 	// Read the stack high water mark (which is 16-byte aligned)
 	csrr               gp, CSR_MSHWM
 	// Skip zeroing if high water mark >= stack pointer
-	bge                gp, sp, .Lafter_zero
-	// Use stack high water mark as base address for zeroing.  If this faults
-	// then it will trigger a force unwind.  This can happen only if the caller
-	// is doing something bad.
+//.Lswitch_shwm_skip_zero:
+	bge                gp, sp, .Lswitch_after_zero
+	/*
+	 * Use stack high water mark as base address for zeroing.  If this faults
+	 * then it will trigger a force unwind.  This can happen only if the caller
+	 * is doing something bad.
+	 */
 	csetaddr           ct2, csp, gp
 #endif
-	zero_stack         t2, s0, gp
-.Lafter_zero:
+	zero_stack         /* base = */ t2, /* top = */ s0, /* scratch = */ gp
+.Lswitch_after_zero:
+	/*
+	 * FROM: above
+	 * FROM: .Lswitch_shwm_skip_zero
+	 * LIVE IN: mtdc, sp, tp, t0, t1, a0, a1, a2, a3, a4, a5
+	 *
+	 * Atlas:
+	 *  sp: pointer to stack, with bounds as t2, cursor at boundary in s0
+	 *      (still)
+	 *  tp: pointer to the freshly populated TrustedStackFrame (still)
+	 *  t1: sealed export table entry for the target callee (still)
+	 *  a0, a1, a2, a3, a4, a5, t0: call argument values / to be zeroed (still)
+	 *  ra, s1: dead (still)
+	 *  s0, t2, gp: dead (again)
+	 */
 
-	// Fetch the sealing key
-	LoadCapPCC         cs0, compartment_switcher_sealing_key
-	li                 gp, SEAL_TYPE_SealedImportTableEntries
-	csetaddr           cs0, cs0, gp
-	// The target capability is in ct1. Unseal, check tag and load the entry point offset.
+	// Fetch the sealing key, using gp as a scratch scalar
+	LoadCapPCC         cs0, .Lunsealing_key_import_tables
+	// Atlas update: s0: switcher sealing key
+	/*
+	 * The caller's handle to the callee (the sealed capability to the export
+	 * table entry) is in t1, which has been kept live all this time.  Unseal
+	 * and load the entry point offset.
+	 */
+//.Lswitch_unseal_entry:
 	cunseal            ct1, ct1, cs0
-	// Load the entry point offset.  If cunseal failed then this will fault and
-	// we will force unwind.
+	/*
+	 * Atlas update:
+	 *  t1: if tagged, an unsealed pointer with bounds encompassing callee
+	 *      compartment ExportTable and ExportEntry array and cursor pointing at
+	 *      the callee ExportEntry; if untagged, the caller is malicious or
+	 *      deeply confused, the next instruction will trap, and we'll
+	 *      .Lcommon_force_unwind via exception_entry_asm and
+	 *      .Lhandle_error_in_switcher.
+	 */
+	/*
+	 * Load the entry point offset.  If cunseal failed then this will fault and
+	 * we will force unwind; see .Lhandle_error_switcher_pcc_check.
+	 */
 	clhu               s0, ExportEntry_offset_functionStart(ct1)
-	// At this point, we know that the cunseal has succeeded (we didn't trap on
-	// the load) and so it's safe to store the unsealed value of the export
-	// table pointer.  Nothing between this point and transition to the callee
-	// should fault.
+	// Atlas update: s0: callee compartment function entrypoint offset
+	/*
+	 * At this point, we know that the cunseal has succeeded (we didn't trap on
+	 * the load) and so it's safe to store the unsealed value of the export
+	 * table pointer.
+	 *
+	 * TODO for formal verification: Nothing between this point and transition
+	 * to the callee should fault.
+	 */
 	csc                ct1, TrustedStackFrame_offset_calleeExportTable(ctp)
 
-	// Load the minimum stack size required by the callee.
+//.Lswitch_stack_check_length:
+	/*
+	 * Load the minimum stack size required by the callee, clobbering tp, which
+	 * holds a capability to the TrustedStackFrame, bringing us closer to a
+	 * register file that is not holding values kept secret from the callee.
+	 */
 	clbu               tp, ExportEntry_offset_minimumStackSize(ct1)
-	// The stack size is in 8-byte units, so multiply by 8.
+	// Atlas update: tp: minimum stack size, in units of 8 bytes.
 	slli               tp, tp, 3
-	// Check that the stack is large enough for the callee.
-	// At this point, we have already truncated the stack and so the length of
-	// the stack is the length that the callee can use.
+	// Atlas update: tp: minimum stack size, in bytes.
+	/*
+	 * Check that the stack is large enough for the callee.
+	 * At this point, we have already truncated the stack and so the length of
+	 * the stack is the length that the callee can use.
+	 */
 	cgetlen            t2, csp
+	// Atlas update: t2: length of available stack
 	/*
 	 * Include the space we reserved for the unwind state.
 	 *
@@ -286,11 +509,17 @@
 	 * extremely limited range, adding STACK_ENTRY_RESERVED_SPACE will not cause
 	 * overflow (while instead subtracting it from the available length, in t2,
 	 * might underflow).
+	 *
+	 * TODO for formal verification: prove the above.
 	 */
 	addi               tp, tp, STACK_ENTRY_RESERVED_SPACE
-	bgtu               tp, t2, .Lstack_too_small
+	// LIVE OUT: mtdc
+	bgtu               tp, t2, .Lswitch_stack_too_small
 
-	// Reserve space for unwind state and so on.
+	/*
+	 * Reserve space for unwind state and so on; this cannot take sp out of
+	 * bounds, in light of the check we just performed.
+	 */
 	cincoffset 	       csp, csp, -STACK_ENTRY_RESERVED_SPACE
 #ifdef CONFIG_MSHWM
 	// store new stack top as stack high water mark
@@ -299,98 +528,210 @@
 
 	// Get the flags field into tp
 	clbu               tp, ExportEntry_offset_flags(ct1)
+	// Atlas update: tp: callee entry flags field
+
+	// All ExportEntry state has been consulted; move to ExportTable header
 	cgetbase           s1, ct1
 	csetaddr           ct1, ct1, s1
-	// Load the target CGP
+	/*
+	 * Atlas update:
+	 *  t1: pointer to the callee compartment ExportTable structure.  Bounds
+	 *      still inclusive of ExportEntry array, but that will not be accessed.
+	 */
+//.Lswitch_callee_load:
+	// At this point we begin loading callee compartment state.
 	clc                cgp, ExportTable_offset_cgp(ct1)
-	// Load the target PCC and point to the function.
+	// Atlas update: gp: target compartment CGP
 	clc                cra, ExportTable_offset_pcc(ct1)
 	cincoffset         cra, cra, s0
-	// Get the number of registers to zero in t2
-	andi               t2, tp, 0x7
-	// Get the interrupt-disable bit in t1
-	andi               t1, tp, 0x10
+	// Atlas update: ra: target function entrypoint (pcc base + offset from s0)
+
 	// Zero any unused argument registers
-	// The low 3 bits of the flags field contain the number of arguments to
-	// pass.  We create a small sled that zeroes them and jump into the middle
-	// of it at an offset defined by the number of registers that the export
-	// entry told us to pass.
-.Lload_zero_arguments_start:
-	auipcc             cs0, %cheriot_compartment_hi(.Lzero_arguments_start)
-	cincoffset         cs0, cs0, %cheriot_compartment_lo_i(.Lload_zero_arguments_start)
-	// Change from the number of registers to pass into the number of 2-byte
-	// instructions to skip.
+	/*
+	 * The low 3 bits of the flags field (tp) contain the number of argument
+	 * registers to pass.  We create a small sled that zeroes them in the order
+	 * they are used as argument registers, and we jump into the middle of it at
+	 * an offset defined by that value, preserving the prefix of the sequence.
+	 */
+.Lswitch_load_zero_arguments_start:
+	// FROM: above
+	auipcc             cs0, %cheriot_compartment_hi(.Lswitch_zero_arguments_start)
+	cincoffset         cs0, cs0, %cheriot_compartment_lo_i(.Lswitch_load_zero_arguments_start)
+	// Atlas update: s0: .Lzero_arguments_start
+	andi               t2, tp, 0x7 // loader/types.h's ExportEntry::flags
+	/*
+	 * Change from the number of registers to pass into the number of 2-byte
+	 * instructions to skip.
+	 */
 	sll                t2, t2, 1
-	// Offset the jump target by the number of registers that we should be
-	// passing.
+	// Offset the jump target by the number of instructions to skip
 	cincoffset         cs0, cs0, t2
 	// Jump into the sled.
 	cjr                cs0
-.Lzero_arguments_start:
+.Lswitch_zero_arguments_start:
+	// IFROM: above
 	zeroRegisters      a0, a1, a2, a3, a4, a5, t0
-	// Enable interrupts of the interrupt-disable bit is not set in flags
-	bnez               t1, .Lskip_interrupt_disable
+
+	/*
+	 * Enable interrupts if the interrupt-disable bit is not set in flags.  See
+	 * loader/types.h's InterruptStatus and ExportEntry::InterruptStatusMask
+	 */
+	andi               t1, tp, 0x10
+	bnez               t1, .Lswitch_skip_interrupt_enable
 	csrsi              mstatus, 0x8
-.Lskip_interrupt_disable:
-	// Registers passed to the callee are:
-	// cra (c1), csp (c2), and cgp (c3) are passed unconditionally.
-	// ca0-ca5 (c10-c15) and ct0 (c5) are either passed as arguments or cleared
-	// above.  This should add up to 10 registers, with the remaining 5 being
-	// cleared now:
+.Lswitch_skip_interrupt_enable:
+	/*
+	 * FROM: above
+	 * IRQ REQUIRE: any (have adopted callee disposition)
+	 *
+	 * Atlas:
+	 *  ra: (still) target function entrypoint
+	 *  sp: (still) pointer to stack, below compartment invocation local storage
+	 *  gp: (still) target compartment CGP
+	 *  a0, a1, a2, a3, a4, a5, t0: arguments or zeroed, as above
+	 *  tp, t1, t2, s0, s1: dead
+	 */
+	/*
+	 * Up to 10 registers are carrying state for the callee or are properly
+	 * zeroed.  Clear the remaining 5 now.
+	 */
+//.Lswitch_caller_dead_zeros:
 	zeroRegisters      tp, t1, t2, s0, s1
+//.Lswitch_callee_call:
+	/*
+	 * "cjalr cra" simultaneously moves the live-in ra value into the *next*
+	 * program counter and the program counter (of the instruction itself) into
+	 * ra (while sealing it to be a backwards-arc sentry).  That is, the value
+	 * we have so carefully been keeping in ra is clobbered, but only after it
+	 * becomes the next program counter.
+	 */
+	// LIVE OUT: *
 	cjalr              cra
 
-	.globl switcher_skip_compartment_call
-switcher_skip_compartment_call:
-	// If we are doing a forced unwind of the trusted stack then we do almost
-	// exactly the same as a normal unwind.  We will jump here from the
-	// exception path (.Lforce_unwind)
-
+	.globl switcher_after_compartment_call
+switcher_after_compartment_call:
+	/*
+	 * FROM: malice
+	 * IFROM: above
+	 * FROM: .Lswitch_stack_too_small
+	 * FROM: .Lcommon_force_unwind
+	 * IRQ ASSUME: any (both IRQ-deferring and IRQ-enabling sentries are
+	 *             provided to the callees and can escape for malice's use, and
+	 *             the TrustedStack spill frame is not precious, and nothing
+	 *             that would happen were we are preempted would shift our
+	 *             TrustedStack::frameoffset or the contents of ::frames)
+	 * LIVE IN: mtdc, a0, a1
+	 *
+	 * Atlas:
+	 *  mtdc: pointer to this thread's TrustedStack
+	 *  a0, a1: return value(s).  The callee function must ensure that it clears
+	 *          these as appropriate if it is returning 0 or 1 values and not 2.
+	 *  ra, sp, gp: dead or callee state (to be replaced by caller state)
+	 *  tp, s0, s1, t0, t1, t2, a2, a3, a4, a5: dead or callee state (to be
+	 *                                          zeroed before return to caller)
+	 */
 	/*
 	 * Pop a frame from the trusted stack, leaving all registers in the state
 	 * expected by the caller of a cross-compartment call.  The callee is
 	 * responsible for zeroing argument and temporary registers.
 	 *
-	 * The below should not fault before returning back to the caller. If a
-	 * fault occurs there must be a serious bug elsewhere.
+	 * This unwind path is common to both ordinary return (from above), benign
+	 * errors after we'd set up the trusted frame (.Lswitch_stack_too_small),
+	 * and forced unwinds (.Lcommon_force_unwind).
+	 *
+	 * TODO for formal verification: the below should not fault before returning
+	 * back to the caller. If a fault occurs there must be a serious bug
+	 * elsewhere.
+	 */
+	/*
+	 * The return sentry given to the callee as part of that cjalr could be
+	 * captured by the callee or passed between compartments arbitrarily for
+	 * later use.  That is, in some sense, we cannot assume that any use of this
+	 * sentry corresponds to the most recent derivation of it by this thread.
+	 * Phrased differently, the sentry created by the "cjalr" above is not tied
+	 * to the topmost TrustedStackFrame at the time of its creation.  Invoking
+	 * this sentry, regardless of how one comes to hold it, and even if
+	 * invocation is not matched to the call that constructed any given instance
+	 * of it, will always result in popping the topmost trusted stack frame (at
+	 * the time of invocation) and returning to its caller.  Thus, the
+	 * possibility of more than one of these sentries in scope at any moment is
+	 * not concerning.
+	 *
+	 * Additionally, threads are given a manufactured, interrupt-deferring
+	 * sentry to here as part of their initial activation frame (so that
+	 * returning acts as an orderly unwind).  See
+	 * loader/boot.cc:/boot_threads_create .
+	 *
+	 * Being robust to malicious or "unusual" entry here is facilitated by the
+	 * requirements of the next block of code being minimal: mtdc must be a
+	 * TrustedStack pointer.  The contents of a0 and a1 will be exposed to the
+	 * compartment above the one currently executing, or the thread will be
+	 * terminated if there is no such.
 	 */
 
 	cspecialr          ctp, mtdc
+
 	clear_hazard_slots ctp, ct2
-	// make sure there is a frame left in the trusted stack
+
+	/*
+	 * Make sure there is a frame left in the trusted stack by...
+	 *
+	 * 1. Loading TrustedStack::frameoffset and offsetof(TrustedStack, frames)
+	 */
 	clhu               t2, TrustedStack_offset_frameoffset(ctp)
-	li                 tp, TrustedStack_offset_frames
-	// Move to the previous trusted stack frame.
+	li                 t0, TrustedStack_offset_frames
+	/*
+	 * 2. Decreasing frameoffset by one frame.  This will go below
+	 *    offsetof(TrustedStack, frames) if there are no active frames.
+	 */
 	addi               t2, t2, -TrustedStackFrame_size
-	// If this is the first trusted stack frame, then the csp that we would be
-	// loading is the csp on entry, which does not have a spilled area.  In
-	// this case, we would fault when loading, so would exit the thread, but we
-	// should instead gracefully exit the thread.
-	bgeu               tp, t2, .Lcommon_defer_irqs_and_thread_exit
-	cspecialr          ctp, mtdc
+	/*
+	 * 3. Comparing.  If this is the first trusted stack frame, then the csp
+	 * that we would be loading is the csp on entry, which does not have a
+	 * spilled area.  In this case, we would fault when loading (because the
+	 * stack cursor is at its limit), so would exit the thread, but we should
+	 * instead gracefully exit the thread.
+	 */
+	bgeu               t0, t2, .Lcommon_defer_irqs_and_thread_exit
 	cincoffset         ct1, ctp, t2
-	// Restore the stack pointer.  All other spilled values are spilled there.
+	// Atlas update: t1: pointer to the TrustedStackFrame to bring on core
+
+	/*
+	 * Restore the untrusted stack pointer from the trusted stack.  This points
+	 * at the spill frame, created by .Lswitch_entry_first_spill and following
+	 * instructions, holding caller register values.
+	 */
 	clc                csp, TrustedStackFrame_offset_csp(ct1)
-	// Update the current frame offset.
+	/*
+	 * Atlas update:
+	 *  sp: pointer to untrusted stack (the spill frame created by
+	 *      .Lswitch_entry_first_spill)
+	 */
+	// Update the current frame offset in the TrustedStack
 	csh                t2, TrustedStack_offset_frameoffset(ctp)
-	// Do the loads *after* moving the trusted stack pointer.  In theory, the
-	// checks in `check_compartment_stack_integrity` make it impossible for
-	// this to fault, but if we do fault here then we'd end up in an infinite
-	// loop trying repeatedly to pop the same trusted stack frame.  This would
-	// be bad.  Instead, we move the trusted stack pointer *first* and so, if
-	// the accesses to the untrusted stack fault, we will detect a fault in the
-	// switcher, enter the force-unwind path, and pop the frame for the
-	// compartment that gave us a malicious csp.
+	/*
+	 * Do the loads *after* moving the trusted stack pointer.  In theory, the
+	 * checks after `.Lswitch_entry_first_spill` make it impossible for this to
+	 * fault, but if we do fault here and hadn't moved the frame offset, then
+	 * we'd end up in an infinite loop trying repeatedly to pop the same
+	 * trusted stack frame.  This would be bad.  Instead, we move the trusted
+	 * stack pointer *first* and so, if the accesses to the untrusted stack
+	 * fault, we will detect a fault in the switcher, enter the force-unwind
+	 * path, and pop the frame for the compartment that gave us a malicious
+	 * csp.
+	 */
 	clc                cs0, SPILL_SLOT_cs0(csp)
 	clc                cs1, SPILL_SLOT_cs1(csp)
 	clc                cra, SPILL_SLOT_pcc(csp)
 	clc                cgp, SPILL_SLOT_cgp(csp)
 	cincoffset         csp, csp, SPILL_SLOT_SIZE
 #ifdef CONFIG_MSHWM
-	// read the stack high water mark, which is 16-byte aligned
-	// we will use this as base address for stack clearing
-	// note that it cannot be greater than stack top as we
-	// we set it to stack top when we pushed to trusted stack frame
+	/*
+	 * Read the stack high water mark, which is 16-byte aligned.  We will use
+	 * this as base address for stack clearing.  Note that it cannot be greater
+	 * than stack top as we set it to stack top when we pushed to the trusted
+	 * stack frame, and it is a monotonically non-increasing value.
+	 */
 	csrr               tp, CSR_MSHWM
 #else
 	cgetbase           tp, csp
@@ -402,76 +743,167 @@
 	csrw               CSR_MSHWM, sp
 #endif
 
-	// Zero all registers apart from RA, GP, SP and return args.
-	// cra, csp and cgp needed for the compartment
-	// cs0 saved and restored on trusted stack
-	// cs1 saved and restored on trusted stack
-	// ca0, used for first return value
-	// ca1, used for second return value
+	// Zero all registers not holding state intended for caller; see atlas below
+//.Lswitch_callee_dead_zeros:
 	zeroAllRegistersExcept ra, sp, gp, s0, s1, a0, a1
-.Ljust_return:
+.Lswitch_just_return:
+	/*
+	 * FROM: above
+	 * IFROM: .Lswitch_entry_first_spill (via .Lhandle_error_in_switcher)
+	 * LIVE IN: mtdc, ra, sp, gp, s0, s1, a0, a1
+	 *
+	 * Atlas:
+	 *  mtdc: pointer to this thread's TrustedStack
+	 *  a0, a1: return value(s) (still)
+	 *  ra, sp, gp, s0, s1: caller state
+	 *  tp, t0, t1, t2, a2, a3, a4, a5: zero (if from above) or caller state (if
+	 *                                  from .Lhandle_error_in_switcher via
+	 *                                  .Lhandle_return_context_install)
+	 */
 	cret
 
-	// If the stack is too small, we don't do the call, but to avoid leaking
-	// any other state we still go through the same return path as normal.  We
-	// set the return registers to -ENOTENOUGHSTACK and 0, so users can see
-	// that this is the failure reason.
-.Lstack_too_small:
+	/*
+	 * If the stack is too small, we don't do the call, but to avoid leaking
+	 * any other state we still go through the same return path as normal.  We
+	 * set the return registers to -ENOTENOUGHSTACK and 0, so users can see
+	 * that this is the failure reason.
+	 */
+.Lswitch_stack_too_small:
+	/*
+	 * FROM: .Lswitch_stack_check_length
+	 * IRQ REQUIRE: any (TrustedStack spill frame is not precious)
+	 * LIVE IN: mtdc
+	 *
+	 * Atlas:
+	 *  mtdc: thread trusted stack pointer
+	 */
 	li                 a0, -ENOTENOUGHSTACK
 	li                 a1, 0
-	j                  switcher_skip_compartment_call
+	// Atlas update: a0, a1: error return values
+	// LIVE OUT: mtdc, a0, a1
+	j                  switcher_after_compartment_call
+
+	/*
+	 * If we have run out of trusted stack, then just restore the caller's state
+	 * (mostly, the callee-save registers from the spills we did at the top of
+	 * __Z26compartment_switcher_entryz) and return an error value.
+	 */
+.Lswitch_trusted_stack_exhausted:
+	/*
+	 * FROM: .Lswitch_trusted_stack_push
+	 * IRQ REQUIRE: any (all state is in registers, TrustedStack spill frame is
+	 *              not precious)
+	 * LIVE IN: mtdc, sp
+	 *
+	 * Atlas:
+	 *  mtdc: TrustedStack pointer
+	 *  sp: Caller stack pointer, pointing at switcher spill frame, after
+	 *      validation
+	 */
+	/*
+	 * Restore the spilled values.  Because csp has survived being spilled to
+	 * and the permission validations, these will not fault.
+	 */
+	clc                cs0, SPILL_SLOT_cs0(csp)
+	clc                cs1, SPILL_SLOT_cs1(csp)
+	clc                cra, SPILL_SLOT_pcc(csp)
+	clc                cgp, SPILL_SLOT_cgp(csp)
+	cincoffset         csp, csp, SPILL_SLOT_SIZE
+	// Set the first return register (a0) and zero the other (a1) below
+	li                 a0, -ENOTENOUGHTRUSTEDSTACK
+	// Zero everything else
+	zeroAllRegistersExcept ra, sp, gp, s0, s1, a0
+	cret
+
 .size compartment_switcher_entry, . - compartment_switcher_entry
 
-	// the entry point of all exceptions and interrupts
-	// For now, the entire routine is run with interrupts disabled.
 	.global  exception_entry_asm
 	.p2align 2
+/**
+ * The entry point of all exceptions and interrupts
+ *
+ * For now, the entire routine is run with interrupts disabled.
+ */
 exception_entry_asm:
-	// We do not trust the interruptee's context. We cannot use its stack in any way.
-	// The save reg frame we can use is fetched from the tStack.
-	// In general, mtdc holds the trusted stack register.  We are here with
-	// interrupts off and precious few registers available to us, so swap it
-	// with the csp (we'll put it back, later).
+	/*
+	 * FROM: malice
+	 * FROM: interrupt
+	 * FROM: error
+	 * IRQ ASSUME: deferred (sole entry is via architectural exception path,
+	 *             which unconditionally, atomically defers IRQs)
+	 * LIVE IN: mcause, mtval, mtdc, *
+	 *
+	 * Atlas:
+	 *  mtdc: either pointer to TrustedStack or zero
+	 *  mcause, mtval: architecture-specified exception information.  These are
+	 *                 assumed correct -- for example, that it is impossible for
+	 *                 untrusted code to enter the exception path with
+	 *                 arbitrarily chosen values.
+	 *  *: The GPRs at the time of exception.
+	 */
+	/*
+	 * We do not trust the interruptee's context. We cannot use its stack in any
+	 * way.  The save register frame we can use is fetched from the
+	 * TrustedStack.  In general, mtdc holds the trusted stack register.  We are
+	 * here with interrupts off and precious few registers available to us, so
+	 * swap it with the csp (we'll put it back, later).
+	 */
 	cspecialrw         csp, mtdc, csp
-#ifndef NDEBUG
-	// XXX: This move is useless, but just for debugging in the simulator.
-	cmove              csp, csp
-#endif
 
-	// If we read out zero, we've reentered the exception and are about to
-	// trap.  Make sure that we end up in an architectural trap loop: clobber
-	// mtcc, so that trapping attempts to vector to an untagged PCC, thereby
-	// causing another (i.e., a third) trap in spillRegisters, below.
-	//
-	// While that's a good start, it does not guarantee that we end up in a
-	// trap loop: the reentry will probably have put something non-zero into
-	// mtdc, so we wouldn't hit this, and wouldn't loop, when we take that
-	// third trap.  (Exactly what we'd do instead is hard to say; we'd try
-	// spilling registers to an attacker-controlled pointer, at the very
-	// least.) Therefore, clobber mtcc (!) to ensure that the certainly
-	// upcoming third trap puts us in an architectural trap loop.  This is
-	// slightly preferable to clearing mtdc, which would also ensure that we
-	// looped, because the architectural loop is tighter and involves no
-	// program text, making it easier for microarchitecture to detect.
-	bnez               sp, .Lexception_entry_still_alive
-	cspecialw          mtcc, csp
-.Lexception_entry_still_alive:
+	/*
+	 * If we read out zero, we've reentered the exception and are about to trap
+	 * (in spillRegisters, which uses sp as its authority).
+	 *
+	 * Failure to guard here would mean that the trap in spillRegisters below
+	 * would re-enter the trap-handler with an unknown value (the first trap's
+	 * sp) in mtdc, which the rest of this code would take to be a valid
+	 * TrustedStack.  Exactly what would happen then is hard to say; we'd try
+	 * spilling registers to a potentially attacker-controlled pointer, at the
+	 * very least, and that's something to avoid.
+	 */
+	beqz               sp, .Lexception_reentered
 
-	// csp now points to the save reg frame that we can use.
-	// The guest csp (c2) is now in mtdc. Will be spilled later, but we
-	// spill all the other 14 registers now.
+	/*
+	 * The guest sp/csp (x2/c2) is now in mtdc. Will be spilled later, but we
+	 * spill all the other 14 registers now.
+	 */
 	spillRegisters     cra, cgp, ctp, ct0, ct1, ct2, cs0, cs1, ca0, ca1, ca2, ca3, ca4, ca5
 
-	// If a thread has exited then it will set a fake value in the mcause so
-	// that the scheduler knows not to try to resume it.
-.Lthread_exit:
-	// mtdc got swapped with the thread's csp, store it and clobber mtdc with
-	// zero.  The trusted stack pointer is solely in csp, now; if we take
-	// another trap before a new one is installed, or if the scheduler enables
-	// interrupts and we take one, we'll pull this zero out of mtdc, above.
+	/*
+	 * The control flow of an exiting thread rejoins us (that is, running
+	 * threads which have taken an exception, be that a trap or an interrupt)
+	 * here, as if it had taken an exception.  We even use the mcause register
+	 * to signal the exit "exception"; see .Lcommon_thread_exit.
+	 */
+.Lexception_exiting_threads_rejoin:
+	/*
+	 * FROM: above
+	 * FROM: .Lcommon_thread_exit
+	 * IRQ REQUIRE: deferred (about to set MTDC to nullptr)
+	 * LIVE IN: mcause, mtval, mtdc, sp
+	 *
+	 * Atlas:
+	 *  mtdc: the interrupted context's sp (or zero, if coming from
+	 *        .Lcommon_thread_exit)
+	 *  sp: TrustedStack pointer (and in particular a spill frame we can use)
+	 */
+
+	/*
+	 * mtdc got swapped with the thread's csp, store it and clobber mtdc with
+	 * zero (using t1 as a scratch register, because using source register index
+	 * 0 with cspecialrw means "don't write" rather than "write zero").  The
+	 * trusted stack pointer is solely in csp, now; if we take another trap
+	 * before a new one is installed, or if the scheduler enables interrupts and
+	 * we take one, we'll pull this zero out of mtdc, above.
+	 */
 	zeroOne            t1
 	cspecialrw         ct1, mtdc, ct1
 	csc                ct1, TrustedStack_offset_csp(csp)
+	/*
+	 * Atlas update:
+	 *  mtdc: zero
+	 *  sp: (still) TrustedStack pointer
+	 */
 
 	// Store the rest of the special registers
 	cspecialr          ct0, mepcc
@@ -487,29 +919,42 @@
 	csrr               t1, mcause
 	csw                t1, TrustedStack_offset_mcause(csp)
 
-	// If we hit one of the exception conditions that we should let
-	// compartments handle then deliver it to the compartment.
-	// CHERI exception code.
+	/*
+	 * If we hit one of the exception conditions that we should let compartments
+	 * handle then maybe deliver it to the compartment (if it has a handler that
+	 * we have the resources to invoke).
+	 */
+//.Lexception_might_handle:
 	li                 a0, MCAUSE_CHERI
+	// LIVE OUT: sp
 	beq                a0, t1, .Lhandle_error
-	// Misaligned instruction, instruction access, illegal instruction,
-	// breakpoint, misaligned load, load fault, misaligned store, and store
-	// access faults are in the range 0-7
+	/*
+	 * A single test suffices to catch all of...
+	 *  - MCAUSE_INST_MISALINED (0),
+	 *  - MCAUSE_INST_ACCESS_FAULT (1),
+	 *  - MCAUSE_ILLEGAL_INSTRUCTION (2),
+	 *  - MCAUSE_BREAKPOINT (3),
+	 *  - MCAUSE_LOAD_MISALIGNED (4),
+	 *  - MCAUSE_LOAD_ACCESS_FAULT (5),
+	 *  - MCAUSE_STORE_MISALIGNED (6),
+	 *  - MCAUSE_STORE_ACCESS_FAULT (7)
+	 */
 	li                 a0, 0x8
+	// LIVE OUT: sp
 	bltu               t1, a0, .Lhandle_error
 
+//.Lexception_scheduler_call:
 	// TODO: On an ecall, we don't need to save any caller-save registers
 
-	// At this point, thread state is completely saved. Now prepare the
-	// scheduler context.
-	// Function signature of the scheduler entry point:
-	// TrustedStack *exception_entry(TrustedStack *sealedTStack,
-	//     size_t mcause, size_t mepc, size_t mtval)
-
-	LoadCapPCC         ca5, compartment_switcher_sealing_key
-	li                 gp, 10
-	csetaddr           ca5, ca5, gp
-	cseal              ca0, csp, ca5 // sealed trusted stack
+	/*
+	 * At this point, thread state is completely saved. Now prepare the
+	 * scheduler context.
+	 * Function signature of the scheduler entry point:
+	 * TrustedStack *exception_entry(TrustedStack *sealedTStack,
+	 *     size_t mcause, size_t mepc, size_t mtval)
+	 */
+	LoadCapPCC         ca0, .Lsealing_key_trusted_stacks
+	cseal              ca0, csp, ca0 // sealed trusted stack
 	mv                 a1, t1 // mcause
 	cgetaddr           a2, ct0 // mepcc address
 	csrr               a3, mtval
@@ -517,57 +962,114 @@
 	LoadCapPCC         csp, switcher_scheduler_entry_csp
 	LoadCapPCC         cgp, switcher_scheduler_entry_cgp
 	LoadCapPCC         cra, switcher_scheduler_entry_pcc
+	/*
+	 * Atlas:
+	 *  ra, gp: scheduler compartment context
+	 *  sp: scheduler thread context
+	 *  a0: sealed trusted stack pointer (opaque thread handle)
+	 *  a1: copy of mcause
+	 *  a2: copy of mepc
+	 *  a3: copy of mtval
+	 *  tp, t0, t1, t2, s0, s1, a4, a5: dead
+	 */
 
 	// Zero everything apart from things explicitly passed to scheduler.
-	// cra, csp and cgp needed for the scheduler compartment
-	// ca0, used for the sealed trusted stack argument
-	// ca1, used for mcause
-	// ca2, used for mepc
-	// ca3, used for mtval
 	zeroAllRegistersExcept ra, sp, gp, a0, a1, a2, a3
 
 	// Call the scheduler.  This returns the new thread in ca0.
 	cjalr              cra
-	// The scheduler may change interrupt posture or may trap, but if it
-	// returns to us (that is, we reach here), the use of the sentry created by
-	// cjalr will have restored us to deferring interrupts, and we will remain
-	// in that posture until the mret in install_context.
 
-	// Switch onto the new thread's trusted stack
-	LoadCapPCC         ct0, compartment_switcher_sealing_key
-	li                 gp, SEAL_TYPE_SealedTrustedStacks
-	csetaddr           ct0, ct0, gp
-	cunseal            csp, ca0, ct0
+.Lexception_scheduler_return:
+	/*
+	 * IFROM: above
+	 * IRQ ASSUME: deferred (reachable only by IRQ-deferring reverse sentry)
+	 * IRQ REQUIRE: deferred (mtdc is zero)
+	 * LIVE IN: a0
+	 *
+	 * Atlas:
+	 *  mtdc: (still) zero
+	 *  a0: sealed trusted stack pointer to bring onto core
+	 */
+	/*
+	 * The interrupts-disabling return sentry handed to the scheduler as part of
+	 * that cjalr may be captured on its stack, but as the scheduler is the
+	 * topmost and only compartment in its thread (as it cannot make
+	 * cross-compartment calls without faulting, due to the null presently in
+	 * mtdc), there is very little that can go wrong as as a result of that
+	 * capture.
+	 */
+	/*
+	 * The scheduler may change interrupt posture or may trap (and infinite loop
+	 * if it does so; see the top of exception_entry_asm and recall that mtdc is
+	 * 0 at this point), but if it returns to us (that is, we reach here), the
+	 * use of the sentry created by cjalr will have restored us to deferring
+	 * interrupts, and we will remain in that posture until the mret in
+	 * .Lcommon_context_install.
+	 */
+
+	// Switch onto the new thread's trusted stack, using gp as a scratch scalar
+	LoadCapPCC         csp, .Lsealing_key_trusted_stacks
+	cunseal            csp, ca0, csp
+	// Atlas update: sp: unsealed target thread trusted stack pointer
+
 	clw                t0, TrustedStack_offset_mcause(csp)
+	// Atlas update: t0: stored mcause for the target thread
 
-	// Only now that we have done something that actually requires the tag of
-	// csp be set, put it into mtdc.  If the scheduler has returned something
-	// untagged or something with the wrong otype, the cunseal will have left
-	// csp untagged and clw will trap with mtdc still 0.  If we made it here,
-	// though, csp is tagged and so was tagged and correctly typed, and so it
-	// is safe to install it to mtdc.  We won't cause traps between here and
-	// mret, so reentrancy is no longer a concern.
+	/*
+	 * Only now that we have done something that actually requires the tag of
+	 * csp be set, put it into mtdc.  If the scheduler has returned something
+	 * untagged or something with the wrong otype, the cunseal will have left
+	 * csp untagged and clw will trap with mtdc still 0.  If we made it here,
+	 * though, csp is tagged and so was tagged and correctly typed, and so it
+	 * is safe to install it to mtdc.  We won't cause traps between here and
+	 * mret, so reentrancy is no longer a concern.
+	 */
 	cspecialw          mtdc, csp
+//.Lexception_scheduler_return_installed:
+	/*
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * Atlas update: mtdc: TrustedStack pointer
+	 */
 
-	// If mcause is MCAUSE_THREAD_INTERRUPT, then we will jump into the error
-	// handler: another thread has signalled that this thread should be
-	// interrupted.  MCAUSE_THREAD_INTERRUPT is a reserved exception number that
-	// we repurpose to indicate explicit interruption.
+	/*
+	 * If mcause is MCAUSE_THREAD_INTERRUPT, then we will jump into the error
+	 * handler: another thread has signalled that this thread should be
+	 * interrupted.  MCAUSE_THREAD_INTERRUPT is a reserved exception number that
+	 * we repurpose to indicate explicit interruption.
+	 */
 	li                 t1, MCAUSE_THREAD_INTERRUPT
+	// LIVE OUT: mtdc, sp
 	beq                t0, t1, .Lhandle_injected_error
 
-	// Environment call from M-mode is exception code 11.
-	// We need to skip the ecall instruction to avoid an infinite loop.
+	/*
+	 * Environment call from M-mode is exception code 11.
+	 * We need to skip the ecall instruction to avoid an infinite loop.
+	 */
 	li                 t1, 11
 	clc                ct2, TrustedStack_offset_mepcc(csp)
-	bne                t0, t1, .Linstall_context
+	// Atlas update: t2: interrupted program counter to resume
+	// LIVE OUT: mtdc, sp, t2
+	bne                t0, t1, .Lcommon_context_install
 	cincoffset         ct2, ct2, 4
 	// Fall through to install context
 
-// Install context expects csp and mtdc to point to the trusted stack and for
-// ct2 to be the pcc to jump to.  All other registers are in unspecified states
-// and will be overwritten when we install the context.
-.Linstall_context:
+.Lcommon_context_install:
+	/*
+	 * FROM: above
+	 * FROM: .Lhandle_error_install_context
+	 * FROM: .Lhandle_return_context_install
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * LIVE IN: mtdc, sp, t2
+	 *
+	 * Atlas:
+	 *  mtdc, sp: TrustedStack pointer
+	 *  t2: target pcc to resume
+	 *  ra, gp, tp, t0, t1, s0, s1, a0, a1, a2, a3, a4, a5: dead
+	 */
+	/*
+	 * All registers other than sp and t2 are in unspecified states and will be
+	 * overwritten when we install the context.
+	 */
 	clw                ra, TrustedStack_offset_mstatus(csp)
 	csrw               mstatus, ra
 #ifdef CONFIG_MSHWM
@@ -577,198 +1079,347 @@
 	csrw               CSR_MSHWMB, ra
 #endif
 	cspecialw          mepcc, ct2
-	// csp (c2) will be loaded last and will overwrite the trusted stack pointer
-	// with the thread's stack pointer.
+
+	/*
+	 * reloadRegisters restores registers in the order given, and we ensure that
+	 * sp/csp (x2/c2) will be loaded last and will overwrite the trusted stack
+	 * pointer with the thread's stack pointer.
+	 */
 	reloadRegisters cra, cgp, ctp, ct0, ct1, ct2, cs0, cs1, ca0, ca1, ca2, ca3, ca4, ca5, csp
 	mret
 
-// We are starting a forced unwind.  This is reached either when we are unable
-// to run an error handler, or when we do run an error handler and it instructs
-// us to return.  This treats all register values as undefined on entry.
-.Lforce_unwind:
+/**
+ * We are starting a forced unwind.  This is reached either when we are unable
+ * to run an error handler, or when we do run an error handler and it instructs
+ * us to return.  This treats all register values as undefined on entry.
+ */
+.Lcommon_force_unwind:
+	/*
+	 * FROM: .Lhandle_error_handler_return_irqs
+	 * FROM: .Lhandle_error_in_switcher
+	 * FROM: .Lhandle_error_test_double_fault
+	 * FROM: .Lhandle_error_test_too_many
+	 * FROM: .Lhandle_error_try_stackless
+	 * FROM: .Lswitch_csp_check
+	 * IRQ REQUIRE: any
+	 * LIVE IN: mtdc
+	 *
+	 * Atlas:
+	 *  mtdc:  pointer to TrustedStack
+	 */
 	li                 a0, -ECOMPARTMENTFAIL
 	li                 a1, 0
-	j                  switcher_skip_compartment_call
+	j                  switcher_after_compartment_call
 
-
-// If we have run out of trusted stack, then just restore the caller's state
-// and return an error value.
-.Lout_of_trusted_stack:
-	// Restore the spilled values
-	clc                cs0, SPILL_SLOT_cs0(csp)
-	clc                cs1, SPILL_SLOT_cs1(csp)
-	clc                cra, SPILL_SLOT_pcc(csp)
-	clc                cgp, SPILL_SLOT_cgp(csp)
-	cincoffset         csp, csp, SPILL_SLOT_SIZE
-	// Set the return registers
-	li                 a0, -ENOTENOUGHTRUSTEDSTACK
-	li                 a1, 0
-	// Zero everything else
-	zeroAllRegistersExcept ra, sp, gp, s0, s1, a0, a1
-	cret
-
-// If we have a possibly recoverable error, see if we have a useful error
-// handler.  At this point, the register state will have been saved in the
-// register-save area and so we just need to set up the environment.
-// 
-// On entry to this block, csp contains the trusted stack pointer, all other
-// registers are undefined.
-// 
-// The handler will have this type signature:
-// enum ErrorRecoveryBehaviour compartment_error_handler(struct ErrorState *frame,
-//                                                       size_t             mcause,
-//                                                       size_t             mtval);
+/**
+ * If we have a possibly recoverable error, see if we have a useful error
+ * handler.  At this point, the register state will have been saved in the
+ * register-save area and so we just need to set up the environment.
+ * The handler will have this type signature:
+ *
+ * enum ErrorRecoveryBehaviour
+ * compartment_error_handler(struct ErrorState *frame,
+ *                           size_t             mcause,
+ *                           size_t             mtval);
+ */
 .Lhandle_error:
-	// We're now out of the exception path, so make sure that mtdc contains
-	// the trusted stack pointer.
+	/*
+	 * FROM: .Lexception_might_handle
+	 * FROM: .Lhandle_injected_error
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * LIVE IN: sp
+	 *
+	 * Atlas:
+	 *  sp: pointer to TrustedStack
+	 */
+	/*
+	 * We're now out of the exception path, so make sure that mtdc contains
+	 * the trusted stack pointer.
+	 */
 	cspecialw   mtdc, csp
-	// Store an error value in return registers, which will be passed to the
-	// caller on unwind.  They are currently undefined, if we leave this path
-	// for a forced unwind then we will return whatever is in ca0 and ca1 to
-	// the caller so must ensure that we don't leak anything.
-	li                 a0, -1
-	li                 a1, 0
+	/*
+	 * Atlas update:
+	 *  mtdc: pointer to TrustedStack
+	 *  sp: (still) pointer to TrustedStack
+	 */
 
-	// We want to make sure we can't leak any switcher state into error
-	// handlers, so if we're faulting in the switcher then we should force
-	// unwind.  We never change the base of PCC in the switcher, so we can
-	// check for this case by ensuring that the spilled mepcc and our current
-	// pcc have the same base.
+//.Lhandle_error_switcher_pcc:
+	/*
+	 * We want to make sure we can't leak any switcher state into error
+	 * handlers, so if we're faulting in the switcher then we should force
+	 * unwind.  We never change the base of PCC in the switcher, so we can
+	 * check for this case by ensuring that the spilled mepcc and our current
+	 * pcc have the same base.
+	 */
 	auipcc             ct0, 0
 	clc                ct1, TrustedStack_offset_mepcc(csp)
 	cgetbase           t0, ct0
 	cgetbase           tp, ct1
 	beq                t0, tp, .Lhandle_error_in_switcher
+	// Atlas update: t1: a copy of mepcc
 
+//.Lhandle_error_not_switcher:
 	// Load the interrupted thread's stack pointer into ct0
 	clc                ct0, TrustedStack_offset_csp(csp)
-	// See if we can find a handler:
+	// Atlas update: t0: interrupted thread's stack pointer
+
+	/*
+	 * If we have already unwound so far that the TrustedStack::frameoffset is
+	 * pointing at TrustedStack::frames[0] -- that is, if the stack has no
+	 * active frames on it -- then just go back to the context we came from,
+	 * effectively parking this thread in a (slow) infinite loop.
+	 */
 	clhu               tp, TrustedStack_offset_frameoffset(csp)
 	li                 t1, TrustedStack_offset_frames
-	beq                tp, t1, .Lset_mcause_and_exit_thread
-	addi               tp, tp, -TrustedStackFrame_size
+	// LIVE OUT: sp
+	beq                tp, t1, .Lcommon_thread_exit
 
-	// ctp points to the current available trusted stack frame.
+	addi               tp, tp, -TrustedStackFrame_size
 	cincoffset         ctp, csp, tp
+	// Atlas update: tp: pointer to current TrustedStackFrame
+
 	// a0 indicates whether we're calling a stackless error handler (0: stack,
 	// 1: stackless)
 	li                 a0, 0
+	// Atlas update: a0: stackful (0) or stackless (1) indicator, currently 0
 
 	// Allocate space for the register save frame on the stack.
 	cincoffset         ct0, ct0, -(16*8)
 
-	// WARNING: ENCODING SPECIFIC.
-	// The following depends on the fact that before-the-start values are not
-	// representable in the CHERIoT encoding and so will clear the tag.  If
-	// this property changes then this will need to be replaced by a check that
-	// against the base of the stack.  Note that this check can't be a simple
-	// cgetbase on ct0, because moving the address below the base sufficiently
-	// far that it's out of *representable* bounds will move the reported base
-	// value (base is a displacement from the address).
+//.Lhandle_error_stack_oob:
+	/*
+	 * WARNING: ENCODING SPECIFIC.
+	 *
+	 * The following depends on the fact that before-the-start values are not
+	 * representable in the CHERIoT encoding and so will clear the tag.  If
+	 * this property changes then this will need to be replaced by a check that
+	 * against the base of the stack.  Note that this check can't be a simple
+	 * cgetbase on ct0, because moving the address below the base sufficiently
+	 * far that it's out of *representable* bounds will move the reported base
+	 * value (base is a displacement from the address).
+	 */
 	cgettag            t1, ct0
-	// If there isn't enough space on the stack, see if there's a stackless
-	// handler.
-	beqz               t1, .Ltry_stackless_handler
+	/*
+	 * If there isn't enough space on the stack, see if there's a stackless
+	 * handler.
+	 */
+	// LIVE OUT: sp, tp, t0
+	beqz               t1, .Lhandle_error_try_stackless
 
 	clc                ct1, TrustedStackFrame_offset_calleeExportTable(ctp)
-	// Set the export table pointer to point to the *start* of the export
-	// table.  It will currently point to the entry point that was raised.
-	// TODO: We might want to pass this to the error handler, it might be
-	// useful for providing per-entry-point error results.
+	// Atlas: t1: pointer to callee's invoked export table entry
+	/*
+	 * Set the export table pointer to point to the *start* of the export
+	 * table.  It will currently point to the entry point that was raised.
+	 *
+	 * TODO: We might want to pass this to the error handler, it might be
+	 * useful for providing per-entry-point error results.
+	 */
 	cgetbase           s0, ct1
 	csetaddr           ct1, ct1, s0
 	clhu               s0, ExportTable_offset_errorHandler(ct1)
-	// A value of 0xffff indicates no error handler
-	// If we found one, use it, otherwise fall through and try to find a
-	// stackless handler.
-	li                 s1, 0xffff
-	bne                s0, s1, .Lhandler_found
 
-.Ltry_stackless_handler:
+//.Lhandle_error_try_stackful:
+	/*
+	 * A value of 0xffff indicates no error handler.  If we found one, use it,
+	 * otherwise fall through and try to find a stackless handler.
+	 */
+	li                 s1, 0xffff
+	// LIVE OUT: sp, tp, t0, t1, s0, a0
+	bne                s0, s1, .Lhandle_error_found
+
+.Lhandle_error_try_stackless:
+	/*
+	 * FROM: above
+	 * FROM: .Lhandle_error_stack_oob
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * LIVE IN: sp, tp, t0
+	 * Atlas:
+	 *  sp: pointer to TrustedStack
+	 *  tp: pointer to current TrustedStackFrame
+	 *  t0: interrupted thread's stack pointer
+	 */
+
 	clc                ct1, TrustedStackFrame_offset_calleeExportTable(ctp)
-	// Set the export table pointer to point to the *start* of the export
-	// table.  It will currently point to the entry point that was raised.
+	/*
+	 * Set the export table pointer to point to the *start* of the export
+	 * table.  It will currently point to the entry point that was raised.
+	 */
 	cgetbase           s0, ct1
 	csetaddr           ct1, ct1, s0
+	// Atlas: t1: pointer to callee's export table
 	clhu               s0, ExportTable_offset_errorHandlerStackless(ct1)
-	// A value of 0xffff indicates no error handler
-	// Give up if there is no error handler for this compartment.
+	/*
+	 * A value of 0xffff indicates no error handler.  Give up if there is no
+	 * error handler for this compartment, having already tried any stackful
+	 * handler.
+	 */
 	li                 s1, 0xffff
-	beq                s0, s1, .Lforce_unwind
+	// LIVE OUT: mtdc
+	beq                s0, s1, .Lcommon_force_unwind
 
-	// The stack may have had its tag cleared at this point, so for stackless
-	// handlers we need to restore the on-entry stack.
-	// Get the previous trusted stack frame
-
-	// Load the caller's csp
+	/*
+	 * The stack may have had its tag cleared at this point, so for stackless
+	 * handlers we need to restore the on-entry stack.
+	 */
 	clc                ct0, TrustedStackFrame_offset_csp(ctp)
+	// Atlas: t0: target invocation's stack pointer, as of invocation start
 
-	// If this is the top stack frame, then the csp field is the value on
-	// entry.  If it's any other frame then we need to go to the previous one
+	/*
+	 * If this is the top (initial) stack frame, then the csp field is the value
+	 * on entry and it is safe to use directly.  Otherwise, we reconstruct the
+	 * stack as it would have been on compartment invocation.
+	 */
 	cincoffset         cs1, csp, TrustedStack_offset_frames
-	beq                s1, tp, .Lrecovered_stack
+	beq                s1, tp, .Lhandle_stack_recovered
 
-	// The address of the stack pointer will point to the bottom of the
-	// caller's save area, so we set the bounds to be the base up to the
-	// current address.
+//.Lhandle_stack_rebound:
+	/*
+	 * The address of the stack pointer will point to the bottom of the
+	 * caller's save area created by .Lswitch_entry_first_spill and following
+	 * instructions, so we set the bounds to be the base up to the current
+	 * address, giving the handler access to the entirety of this invocation's
+	 * activation frame (except the caller save registers we spilled).
+	 */
 	cgetaddr           a1, ct0
 	cgetbase           a2, ct0
 	sub                a1, a1, a2
 	csetaddr           ct0, ct0, a2
-	// The code that installs the context expects csp to be in ct0
+	// The code that installs the context expects the target stack to be in ct0
 	csetboundsexact    ct0, ct0, a1
-.Lrecovered_stack:
+.Lhandle_stack_recovered:
+	/*
+	 * FROM: above
+	 * FROM: .Lhandle_error_try_stackless
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * LIVE IN: sp, tp, t0, t1, s0
+	 *
+	 * Atlas:
+	 *  sp: pointer to TrustedStack
+	 *  tp: pointer to current TrustedStackFrame
+	 *  t0: pointer to the untrusted stack to use on invocation.  Either below
+	 *      all activations, in the stackful handler case, or the entire
+	 *      invocation's stack (below the spill frame created by
+	 *      .Lswitch_entry_first_spill and following instructions).
+	 *  t1: pointer to callee's export table
+	 *  s0: offset from compartment PCC base to handler
+	 */
 	li                 a0, 1
 
-.Lhandler_found:
+.Lhandle_error_found:
+	/*
+	 * FROM: above
+	 * FROM: .Lhandle_error_try_stackful
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * LIVE IN: sp, tp, t0, t1, s0, a0
+	 *
+	 * Atlas:
+	 *  sp: pointer to TrustedStack
+	 *  tp: pointer to current TrustedStackFrame
+	 *  t0: pointer to the untrusted stack to use on invocation.  Either below
+	 *      all activations, in the stackful handler case, or the entire
+	 *      invocation's stack (below the spill frame created by
+	 *      .Lswitch_entry_first_spill and following instructions).
+	 *  t1: pointer to callee's export table
+	 *  s0: offset from compartment PCC base to handler
+	 *  a0: stackful (0) or stackless (1) indicator
+	 */
 
 	// Increment the handler invocation count.
 	clhu               s1, TrustedStackFrame_offset_errorHandlerCount(ctp)
 	addi               s1, s1, 1
 	csh                s1, TrustedStackFrame_offset_errorHandlerCount(ctp)
 
-	// If we are in a double fault, unwind now.  The low bit should be 1 while
-	// we are handling a fault.
+	/*
+	 * The low bit should be 1 while we are handling a fault.  If we are in a
+	 * double fault (that is, the value we just wrote back has its low bit 0),
+	 * unwind now.
+	 */
+//.Lhandle_error_test_double_fault:
 	andi               ra, s1, 1
-	beqz               ra, .Lforce_unwind
-	// If we have reached some arbitrary limit on the number of faults in a
-	// singe compartment calls, give up now.
-	// TODO: Make this a number based on something sensible, possibly something
-	// set per entry point.  Some compartments (especially top-level ones)
-	// should be allowed to fault an unbounded number of times.
+	// LIVE OUT: mtdc
+	beqz               ra, .Lcommon_force_unwind
+
+	/*
+	 * If we have reached some arbitrary limit on the number of faults in a
+	 * singe compartment calls, give up now.
+	 *
+	 * TODO: Make this a number based on something sensible, possibly something
+	 * set per entry point.  Some compartments (especially top-level ones)
+	 * should be allowed to fault an unbounded number of times.
+	 */
+//.Lhandle_error_test_too_many:
 	li                 ra, MAX_FAULTS_PER_COMPARTMENT_CALL
-	bgtu               s1, ra, .Lforce_unwind
+	// LIVE OUT: mtdc
+	bgtu               s1, ra, .Lcommon_force_unwind
 
 	// Load the pristine pcc and cgp for the invoked compartment.
 	clc                cra, ExportTable_offset_pcc(ct1)
 	clc                cgp, ExportTable_offset_cgp(ct1)
-	// Set the jump target to the error handler entry point
-	// This may result in something out-of-bounds if the compartment has a
-	// malicious value for their error handler (hopefully caught at link or
-	// load time), but if it does then we will double-fault and force unwind.
+	/*
+	 * Set the jump target to the error handler entry point.  This may result in
+	 * something out-of-bounds if the compartment has a malicious value for
+	 * their error handler (hopefully caught at link or load time), but if it
+	 * does then we will fault when attempting the cjalr below and force unwind
+	 * (either because the cjalr itself will raise a fault, because ra is
+	 * untagged, or because the resulting PCC is out of bounds and instruction
+	 * fetch fails; either case results in a forced unwind, albeit by slightly
+	 * different paths, with .Lhandle_error_switcher_pcc relevant for the former
+	 * and .Lhandle_error_test_double_fault for the latter.
+	 */
 	cgetbase           s1, cra
 	csetaddr           cra, cra, s1
 	cincoffset         cra, cra, s0
 
-	// If we're in an error handler with a stack, set up the stack, otherwise
-	// we just need to set up argument registers.
-	beqz               a0, .Lset_up_stack_handler
+	/*
+	 * If we're in an error handler with a stack, set up the stack, otherwise
+	 * we just need to set up argument registers.
+	 */
+//.Lhandle_error_test_stackful:
+	beqz               a0, .Lhandle_error_stack_setup
+
+//.Lhandle_error_stackless_setup:
 	clw                a0, TrustedStack_offset_mcause(csp)
 	csrr               a1, mtval
 	li                 a2, 0
 	cmove              csp, ct0
-	j                  .Linvoke_error_handler
+	// Atlas: sp: taget compartment invocation stack pointer
+	j                  .Lhandle_error_handler_invoke
 
-.Lset_up_stack_handler:
-	// Set up the on-stack context for the callee
-	clc                cs1, 0(csp)
+.Lhandle_error_stack_setup:
+	/*
+	 * FROM: .Lhandle_error_test_stackful
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * LIVE IN: ra, sp, gp, t0
+	 *
+	 * Atlas:
+	 *  ra: handler entrypoint (with bounds of compartment's .text)
+	 *  sp: pointer to TrustedStack
+	 *  gp: target compartment cgp
+	 *  t0: pointer to the untrusted stack to use on invocation.  This is
+	 *      presently sufficiently below all activations to provide space for an
+	 *      ErrorState structure.
+	 */
+	/*
+	 * Set up the on-stack context, a compartment.h:/struct ErrorState value,
+	 * which has the same layout at a TrustedStack spill frame.
+	 *
+	 * These begin with a PCC.  To ensure that handlers do not have access to
+	 * values (especially, capabilities) reachable through the trapping PCC,
+	 * we clear the tag.  Handlers of course retain access to values reachable
+	 * through their own PCC and CGP.
+	 */
+	clc                cs1, TrustedStack_offset_mepcc(csp)
 	ccleartag          cs1, cs1
-	csc                cs1, 0(ct0)
-	// Source for context copy.
+	csc                cs1, TrustedStack_offset_mepcc(ct0)
+	/*
+	 * Now copy the 15 GPRs from the trusted stack (sp).  We use a2 as the
+	 * source of the copy and a3 as the destination, preserving sp (TrustedStack
+	 * pointer) and t0 (untrusted stack pointer to the base of the spill area).
+	 */
 	cincoffset         ca2, csp, TrustedStack_offset_cra
-	// Destination for context copy
 	cincoffset         ca3, ct0, TrustedStack_offset_cra
-	copyContext        ca3, ca2, cs1, a4
+	copyContext        /* dst = */ ca3, /* src = */ ca2, /* scratch = */ cs1, /* counter = */ a4
 
 	// Set up the arguments for the call
 	cmove              ca0, ct0
@@ -776,18 +1427,80 @@
 	csrr               a2, mtval
 	cmove              csp, ca0
 
-.Linvoke_error_handler:
-	// Enable interrupts before invoking the handler
+.Lhandle_error_handler_invoke:
+	/*
+	 * FROM: above
+	 * FROM: .Lhandle_error_stackless_setup
+	 * IRQ REQUIRE: any (see below)
+	 * LIVE IN: mtdc, ra, sp, gp, a0, a1, a2
+	 *
+	 * Atlas:
+	 *  mtdc: TrustedStack pointer
+	 *  ra: handler entrypoint (with bounds of compartment's .text)
+	 *  gp: target compartment cgp
+	 *  sp: target compartment invocation stack pointer
+	 *  a0, a1, a2: arguments to handler (see below)
+	 *  tp, t0, t1, t2, s0, s1, a3, a4, a5: dead (to be zeroed)
+	 */
+	/*
+	 * At this point, the TrustedStack spill frame is no longer precious: either
+	 * we have copied it down to the untrusted stack for the stackful handler's
+	 * use or we have abandoned it in deciding to use the stackless handler.
+	 * Thus, our "IRQ REQUIRE: any" above: it's safe to be preemptive here,
+	 * though all paths to us in fact run with IRQs deferred.
+	 *
+	 * Since we are not using a sentry, but rather a capability constructed from
+	 * the compartment's PCC (and handler offset value) to enter the
+	 * compartment, enable interrupts now.
+	 */
+	/*
+	 * For a stackful handler, the arguments are:
+	 *  - a0: equal to the invocation stack (sp), with a register spill frame
+	 *        here and above (the stack grows down!)
+	 *  - a1: mcause
+	 *  - a2: mtval
+	 *
+	 * While for stackless, the arguments are:
+	 *  - a0: mcause
+	 *  - a1: mtval
+	 *  - a2: zero
+	 */
 	csrsi              mstatus, 0x8
+//.Lhandle_error_handler_invoke_irqs:
+	// IRQ ASSUME: enabled
 
-	// Clear all registers except:
-	// cra is set by cjalr.  csp and cgp are needed for the called compartment.
-	// ca0, used for the register state
-	// ca1, used for mcause
-	// ca2, used for mtval
+	// Clear all other registers and invoke the handler
 	zeroAllRegistersExcept ra, sp, gp, a0, a1, a2
-	// Call the handler.
 	cjalr              cra
+//.Lhandle_error_handler_return:
+	/*
+	 * IFROM: above
+	 * FROM: malice
+	 * IRQ ASSUME: enabled (only IRQ-enabling reverse sentries given out)
+	 * LIVE IN: mtdc, a0, sp
+	 *
+	 * Atlas:
+	 *  mtdc: pointer to this thread's TrustedStack
+	 *  a0: handler return value
+	 *  sp: target compartment invocation stack pointer
+	 *  gp, tp, t0, t1, t2, s0, s1, a1, a2, a3, a4, a5: dead (to be clobbered
+	 *                                                  by replacement context
+	 *                                                  or .Lcommon_force_unwind)
+	 */
+	/*
+	 * The return sentry given to the handler as part of that cjalr could be
+	 * captured in that compartment or any of its callers (recall similar
+	 * commentary in switcher_after_compartment_call).  Invoking this sentry,
+	 * regardless of how one comes to hold it, and even if invocation is not
+	 * matched to the call that constructed any given instance of it, will
+	 * always result in popping the topmost trusted stack frame (at the time of
+	 * invocation) and returning to its caller.
+	 *
+	 * Being robust to malicious entry here is facilitated by the requirements
+	 * of the next block of code being minimal: mtdc must be a TrustedStack
+	 * pointer, and we may try to dereference the provided sp, but we are
+	 * prepared for that to trap (and induce forced-unwinding).
+	 */
 
 	/*
 	 * Now that we're back, defer interrupts again before we do anything that
@@ -797,69 +1510,116 @@
 	 * actually matters and let most of this code run with IRQs enabled.
 	 */
 	csrci              mstatus, 0x8
+//.Lhandle_error_handler_return_irqs:
+	// IRQ ASSUME: deferred
 
-	// Move the return value to a register that will be cleared in a forced
-	// unwind and zero the return registers.
-	move               s0, a0
-	// Store an error value in return registers, which will be passed to the
-	// caller on unwind.
-	li                 a0, -1
-	li                 a1, 0
-	// Return values are 0 for install context, 1 for forced unwind.  Anything
-	// that is not either of these is invalid and so we should do a forced
-	// unwind anyway.
-	bne                s0, zero, .Lforce_unwind
+	/*
+	 * Return values are compartment.h's enum ErrorRecoveryBehaviour :
+	 *  - InstallContext (0)
+	 *  - ForceUnwind (1)
+	 * Other values are invalid and so we should do a forced unwind anyway.
+	 */
+	// LIVE OUT: mtdc
+	bnez               a0, .Lcommon_force_unwind
 
-	// We have been asked to install the new register context and resume.
-	// We do this by copying the register frame over the save area and entering
-	// the exception resume path.  This may fault, but if it does then we will
-	// detect it as a double fault and forcibly unwind.
+//.Lhandle_error_install_context:
+	// IRQ REQUIRE: deferred (TrustedStack spill frame precious, once populated)
+	/*
+	 * We have been asked to install the new register context and resume.  We do
+	 * this by copying the register frame over the save area and entering the
+	 * exception resume path.  This may fault, but if it does then we will
+	 * detect it as a double fault and forcibly unwind.
+	 *
+	 * The state of the target stack (sp) is expected to be common across both
+	 * stackful and stackless handlers in the case of an InstallContext return.
+	 * Above, in .Lhandle_error_stack_setup, we arranged for sp to point to a
+	 * register spill frame (also passed in a0 for convenience from C).
+	 * Stackless handlers are expected to arrange for sp to point to a register
+	 * spill area before returning; compartments availing themselves of
+	 * stackless handlers must also manage reserving space for such.
+	 */
 
-	// Load the trusted stack pointer to ct1
 	cspecialr          ct1, mtdc
+	// Atlas update: t1: pointer to TrustedStack
 #ifdef CONFIG_MSHWM
-	// Update the spilled copy of the stack high water mark to ensure that we
-	// will clear all of the stack used by the error handler and the spilled
-	// context.
+	/*
+	 * Update the spilled copy of the stack high water mark to ensure that we
+	 * will clear all of the stack used by the error handler and the spilled
+	 * context.
+	 */
 	csrr               t0, CSR_MSHWM
 	csw                t0, TrustedStack_offset_mshwm(ct1)
 #endif
 	clhu               tp, TrustedStack_offset_frameoffset(ct1)
 	addi               tp, tp, -TrustedStackFrame_size
-	// ctp points to the current available trusted stack frame.
+	// Atlas update: tp: pointer to the current available trusted stack frame.
 	cincoffset         ctp, ct1, tp
 
-	// ct0 now contains the export table for the callee
+	/*
+	 * The PCC the handler has given to us is not particularly trusted and might
+	 * be an attempt to escape from the compartment.  Confine it to being
+	 * derived from the compartment's (static) PCC.  This is a multi-step
+	 * process, in which we...
+	 *
+	 * 1. Load the (tagged) PCC for the compartment, which is the 0th word in
+	 *    the ExportTable.
+	 */
 	clc                ct0, TrustedStackFrame_offset_calleeExportTable(ctp)
 	cgetbase           s0, ct0
 	csetaddr           ct0, ct0, s0
-	// ct0 now contains the PCC for the returning compartment.
 	clc                ct0, ExportTable_offset_pcc(ct0)
-	// This is the *untagged* destination pcc.  Install its address into the
-	// real one
-	clc                cra, 0(csp)
+	// Atlas update: t0: compartment .text / PCC
+
+	// 2. Load the untrusted PCC from the handler's returned spill area (sp).
+	clc                cra, TrustedStack_offset_mepcc(csp)
+
+	/*
+	 * 3. Copy the address from the returned PCC into the compartment's PCC,
+	 *    which will result in an out-of-bounds capability if the handler was
+	 *    trying anything fishy.
+	 */
 	cgetaddr           ra, cra
 	csetaddr           ct2, ct0, ra
-	// Now copy everything else from the stack into the saved context
-	// Source
+	// Atlas update: t2: program counter to resume
+
+	/*
+	 * Now copy everything else from the stack up into the trusted saved
+	 * context, using a2 as the source and a3 as the destination, preserving sp
+	 * (the untrusted stack pointer) and t1 (TrustedStack pointer).
+	 */
 	cincoffset         ca2, csp, TrustedStack_offset_cra
-	// Destination
 	cincoffset         ca3, ct1, TrustedStack_offset_cra
-	copyContext        ca3, ca2, cs1, a4
-	// Increment the handler invocation count.  We have now returned and
-	// finished touching any data from the error handler that might cause a
-	// fault.  Any subsequent fault is not treated as a double fault.  It might
-	// be a fault loop, but that will be caught by the fault limit check.
+	copyContext        /* dst = */ ca3, /* src = */ ca2, /* scratch = */ cs1, /* counter = */ a4
+
+	/*
+	 * Increment the handler invocation count.  We have now returned and
+	 * finished touching any data from the error handler that might cause a
+	 * fault.  Any subsequent fault is not treated as a double fault.  It might
+	 * be a fault loop, but that will be caught by the fault limit check.
+	 */
 	clh                s1, TrustedStackFrame_offset_errorHandlerCount(ctp)
 	addi               s1, s1, 1
 	csh                s1, TrustedStackFrame_offset_errorHandlerCount(ctp)
 
-	// Now that the context is set up, let the exception handler code deal with
-	// it.  It expects the context to be in csp, so move the context pointer there.
+	/*
+	 * Now that the context is set up, let the exception handler code deal with
+	 * it.  It expects the context to be in csp, so move the context pointer
+	 * there.
+	 */
 	cmove              csp, ct1
-	j                  .Linstall_context
+	// LIVE OUT: mtdc, sp, t2
+	j                  .Lcommon_context_install
 
 .Lhandle_injected_error:
+	/*
+	 * FROM: .Lexception_scheduler_return_installed
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * LIVE IN: mtdc, sp
+	 *
+	 * Atlas:
+	 *  mtdc: TrustedStack pointer
+	 *  sp: TrustedStack pointer (a copy of mtdc)
+	 */
 #ifdef CONFIG_MSHWM
 	clw                ra, TrustedStack_offset_mshwm(csp)
 	csrw               CSR_MSHWM, ra
@@ -869,27 +1629,54 @@
 	j                  .Lhandle_error
 
 .Lcommon_defer_irqs_and_thread_exit:
+	/*
+	 * FROM: switcher_after_compartment_call
+	 * IRQ REQUIRE: any
+	 */
 	csrci               mstatus, 0x8
-	// Fall-through, now that IRQs are off
+//.Lcommon_deferred_irqs_and_thread_exit:
+	// IRQ ASSUME: deferred
 
-	// Value 24 is reserved for custom use.
-.Lset_mcause_and_exit_thread:
+/**
+ * Signal to the scheduler that the current thread is finished
+ */
+.Lcommon_thread_exit:
+	/*
+	 * FROM: above
+	 * FROM: .Lhandle_error_not_switcher
+	 * IRQ REQUIRE: deferred (about to zero out MTDC and join exception path)
+	 * LIVE IN: mtdc
+	 *
+	 * Atlas:
+	 *  mtdc: pointer to TrustedStack
+	 */
 	csrw               mcause, MCAUSE_THREAD_EXIT
-	// The thread exit code expects the trusted stack pointer to be in csp and
-	// the stack pointer to be in mtdc.  After thread exit, we don't need the
-	// stack pointer so just put zero there.
+	/*
+	 * The thread exit code expects the TrustedStack pointer to be in csp and
+	 * the thread's stack pointer to be in mtdc.  After thread exit, we don't
+	 * need the stack pointer so just put zero there.
+	 */
 	zeroOne            sp
 	cspecialrw         csp, mtdc, csp
-	j                  .Lthread_exit
+	// LIVE OUT: mtdc, sp
+	j                  .Lexception_exiting_threads_rejoin
 
 	/*
 	 * Some switcher instructions' traps are handled specially, by looking at
 	 * the offset of mepcc.  Otherwise, we're off to a force unwind.
 	 */
 .Lhandle_error_in_switcher:
-	auipcc             ctp, %cheriot_compartment_hi(.Lswitcher_entry_first_spill)
+	/*
+	 * FROM: .Lhandle_error_switcher_pcc
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * LIVE IN: mtdc
+	 *
+	 * Atlas:
+	 *  mtdc:  pointer to TrustedStack
+	 */
+	auipcc             ctp, %cheriot_compartment_hi(.Lswitch_entry_first_spill)
 	cincoffset         ctp, ctp, %cheriot_compartment_lo_i(.Lhandle_error_in_switcher)
-	bne                t1, tp, .Lforce_unwind
+	bne                t1, tp, .Lcommon_force_unwind
 	li                 a0, -ENOTENOUGHSTACK
 	li                 a1, 0
 
@@ -898,15 +1685,52 @@
 	 * We do this by vectoring to a `cjalr ra` (`cret`) instruction through
 	 * `mepcc`; whee!  Overwrites the stored context a0 and a1 with the current
 	 * values of those registers, effectively passing them through
-	 * .Linstall_context.
+	 * .Lcommon_context_install.
 	 */
-.Linstall_return_context:
-	auipcc             ct2, %cheriot_compartment_hi(.Ljust_return)
-	cincoffset         ct2, ct2, %cheriot_compartment_lo_i(.Linstall_return_context)
+.Lhandle_return_context_install:
+	/*
+	 * FROM: above
+	 * IRQ REQUIRE: deferred (TrustedStack spill frame is precious)
+	 * LIVE IN: sp, a0, a1
+	 *
+	 * Atlas:
+	 *  sp: pointer to TrustedStack
+	 *  a0, a1: return values to the caller
+	 */
+	auipcc             ct2, %cheriot_compartment_hi(.Lswitch_just_return)
+	cincoffset         ct2, ct2, %cheriot_compartment_lo_i(.Lhandle_return_context_install)
 	csc                ca0, TrustedStack_offset_ca0(csp)
 	csc                ca1, TrustedStack_offset_ca1(csp)
-	j                  .Linstall_context
+	// LIVE OUT: sp, t2
+	j                  .Lcommon_context_install
 
+.Lexception_reentered:
+	/*
+	 * FROM: exception_entry_asm
+	 * FROM: .Lexception_reentered
+	 * IRQ REQUIRE: deferred (an IRQ before we reprogram MTCC could escape
+	 *              looping)
+	 */
+	/*
+	 * We've reentered our exception handler, a "double fault" of sorts.  Make
+	 * sure that we end up in an architectural trap loop: clobber mtcc, so that
+	 * that trap attempts to vector to an untagged PCC, thereby causing another
+	 * trap, which immediately traps, and so on.
+	 *
+	 * We could instead zero mtdc, ensuring that we spin through several
+	 * instructions (taking a trap then running enough of exception_entry_asm
+	 * until we again trapped), but this is less architecturally visible.
+	 */
+	/*
+	 * Writing cnull to mtcc takes two instructions because cspecialw is an
+	 * alias for cspecialrw with a zero source, which means "don't write".  So,
+	 * put nullptr in a register with non-zero index, and then put that in mtcc.
+	 */
+	cmove              csp, cnull
+	cspecialw          mtcc, csp
+	// Take a trap and wedge the machine on that null MTCC
+	clc                csp, 0(csp)
+	j                  .Lexception_reentered
 
 .size exception_entry_asm, . - exception_entry_asm
 
@@ -934,43 +1758,82 @@
 	.p2align 2
 	.type __Z23trusted_stack_has_spacei,@function
 __Z23trusted_stack_has_spacei:
+	/*
+	 * LIVE IN: mtdc, a0
+	 *
+	 * Atlas:
+	 *  mtdc: pointer to TrustedStack (or nullptr if from buggy scheduler)
+	 *  a0: requested number of trusted stack frames
+	 */
 	li                 a2, TrustedStackFrame_size
 	mul                a2, a0, a2
-	// Load the trusted stack into a register that we will clobber on the way
-	// out.
+	// Atlas update: a2: requested number trusted stack frames, in bytes
+	/*
+	 * Load the trusted stack into the return register, so that we clobber it on
+	 * the way out.  Nothing here should trap, but if it does we'll forcibly
+	 * unwind (see .Lhandle_error_in_switcher) and also clobber this pointer.
+	 */
 	cspecialr          ca0, mtdc
+	/*
+	 * TrustedStack::frames[] is a FAM at the end of the structure, and
+	 * ::frameoffset codes for our current position therein (by counting bytes
+	 * relative to the start of the TrustedStack).  We have sufficiently many
+	 * frames if the TrustedStack length minus ::frameoffset is greater than
+	 * the requested number of bytes.
+	 */
 	clhu               a1, TrustedStack_offset_frameoffset(ca0)
+	// Atlas update: a1: this thread's TrustedStack::frameoffset
 	cgetlen            a0, ca0
+	// Atlas update: a0: length of this thread's TrustedStack
 	sub                a0, a0, a1
 	sltu               a0, a2, a0
+	// LIVE OUT: mtdc, a0
 	cret
 
 	.section .text, "ax", @progbits
 	.p2align 2
 	.type __Z22switcher_recover_stackv,@function
 __Z22switcher_recover_stackv:
-	// Load the trusted stack pointer into a register that we will clobber in
-	// two instructions.
+	/*
+	 * LIVE IN: mtdc
+	 *
+	 * Atlas:
+	 *  mtdc: pointer to TrustedStack (or nullptr if buggy scheduler)
+	 */
+	/*
+	 * Load the trusted stack pointer into a register that we will clobber after
+	 * two instructions.
+	 */
 	cspecialr          ca0, mtdc
+	// Atlas update: a0: pointer to TrustedStack
 	clhu               a1, TrustedStack_offset_frameoffset(ca0)
+	// Atlas update: a1: TrustedStack::frameoffset
 	addi               a1, a1, -TrustedStackFrame_size
+	// Atlas update: a1: offset of current TrustedStackFrame
 	cincoffset         ca0, ca0, a1
+	// Atlas update: a0: pointer to current TrustedStackFrame
 	clc                ca0, TrustedStackFrame_offset_csp(ca0)
-	// If this is the first frame, then the recovered stack will be the stack
-	// on entry.  If this is not the first frame then then we need to find the
-	// saved CSP from the caller and reset the bounds.  The address of the
-	// saved CSP will be the value after the switcher spilled registers and so
-	// will be the top of the callee's stack.
+	// Atlas update: a0: saved stack pointer at time of frame creation
+	/*
+	 * If this is the first frame, then the recovered stack will be the stack
+	 * on entry, and can be returned directly.
+	 */
 	li                 a2, TrustedStack_offset_frames
 	beq                a1, a2, 0f
 
-	// Find the previous frame's csp and reset the bounds
+	/*
+	 * Otherwise, this is not the first frame, and the TrustedStackFrame::csp
+	 * value is pointing to the spills done at .Lswitch_entry_first_spill.  Redo
+	 * the stack chopping done at .Lswitch_stack_chop to recompute the bounds
+	 * we would have given to the callee.
+	 */
 	cgetaddr           a1, ca0
 	cgetbase           a2, ca0
 	sub                a1, a1, a2
 	csetaddr           ca0, ca0, a2
 	csetboundsexact    ca0, ca0, a1
 0:
+	// LIVE OUT: mtdc, a0
 	cret
 
 	.section .text, "ax", @progbits
@@ -979,21 +1842,22 @@
 __Z25switcher_interrupt_threadPv:
 	// Load the unsealing key into a register that we will clobber two
 	// instructions later.
-	LoadCapPCC         ca1, compartment_switcher_sealing_key
-	li                 a2, SEAL_TYPE_SealedTrustedStacks
-	csetaddr           ca1, ca1, a2
-	// The target capability is in ct1. Unseal, check tag and load the entry point offset.
+	LoadCapPCC         ca1, .Lsealing_key_trusted_stacks
+	/*
+	 * The target capability is in ca0.  Unseal, check tag and load the entry
+	 * point offset.
+	 */
 	cunseal            ca1, ca0, ca1
 	cgettag            a0, ca1
 	// a0 (return register) now contains the tag.  We return false on failure
 	// so can just branch to the place where we zero non-return registers from
 	// here and it will contain faluse on failure.
-	beqz               a0, .Lreturn
+	beqz               a0, .Lswitcher_interrupt_thread_return
 
 	// A thread can't interrupt itself, return failure if it tries.
 	cspecialr          ca2, mtdc
 	li                 a0, 0
-	beq                a2, a1, .Lreturn
+	beq                a2, a1, .Lswitcher_interrupt_thread_return
 
 	// ca1 now contains the unsealed capability for the target thread.  We
 	// allow the target thread to be interrupted if (and only if) the caller is
@@ -1021,7 +1885,7 @@
 	li                 a0, 42
 
 	// If the two export table entries differ, return.
-	bne                a2, a3, .Lreturn
+	bne                a2, a3, .Lswitcher_interrupt_thread_return
 	// After this point, we no longer care about the values in a0, a2, and a3.
 
 	// Mark the thread as interrupted.
@@ -1030,7 +1894,7 @@
 	csw                a2, TrustedStack_offset_mcause(ca1)
 	// Return success
 	li                 a0, 1
-.Lreturn:
+.Lswitcher_interrupt_thread_return:
 	zeroRegisters      a1, a2, a3
 	cret
 
@@ -1038,9 +1902,7 @@
 	.p2align 2
 	.type __Z23switcher_current_threadv,@function
 __Z23switcher_current_threadv:
-	LoadCapPCC         ca0, compartment_switcher_sealing_key
-	li                 a1, SEAL_TYPE_SealedTrustedStacks
-	csetaddr           ca0, ca0, a1
+	LoadCapPCC         ca0, .Lsealing_key_trusted_stacks
 	cspecialr          ca1, mtdc
 	cseal              ca0, ca1, ca0
 	li                 a1, 0
@@ -1067,9 +1929,9 @@
 	// If this is a null pointer, don't try to dereference it and report that
 	// we are thread 0.  This permits the debug code to work even from things
 	// that are not real threads.
-	beqz               a1, .Lend
+	beqz               a1, 0f
 	clh                a0, TrustedStack_offset_threadID(ca0)
-.Lend:
+0:
 	cret
 
 
diff --git a/sdk/core/switcher/tstack.h b/sdk/core/switcher/tstack.h
index dc8338b..c48f4a0 100644
--- a/sdk/core/switcher/tstack.h
+++ b/sdk/core/switcher/tstack.h
@@ -10,7 +10,13 @@
 
 struct TrustedStackFrame
 {
-	/// caller's stack
+	/**
+	 * Caller's stack pointer, at time of cross-compartment entry, pointing at
+	 * switcher's register spills (.Lswitch_entry_first_spill and following).
+	 *
+	 * The address of this pointer is the (upper) limit of the stack capability
+	 * given to the callee.
+	 */
 	void *csp;
 	/**
 	 * The callee's export table.  This is stored here so that we can find the
@@ -28,6 +34,13 @@
 	uint16_t errorHandlerCount;
 };
 
+/**
+ * Each thread in the system has, and is identified by, its Trusted Stack.
+ * These structures hold an activation frame (a TrustedStackFrame) for each
+ * active cross-compartment call as well as a "spill" register context, used
+ * mostly for preemption (but also as staging space when a thread is adopting a
+ * new context as part of exception handlng).
+ */
 template<size_t NFrames>
 struct TrustedStackGeneric
 {
diff --git a/sdk/core/token_library/token_unseal.S b/sdk/core/token_library/token_unseal.S
index 1dccc04..a9dfd67 100644
--- a/sdk/core/token_library/token_unseal.S
+++ b/sdk/core/token_library/token_unseal.S
@@ -2,15 +2,34 @@
 #include <cheri-builtins.h>
 #include "../allocator/token.h"
 
-	.hidden __sealingkey
-	.type   __sealingkey,@object
-	.section    .sealing_key1,"aw",@progbits
-	.globl  __sealingkey
-	.p2align    3
-__sealingkey:
-	.chericap   0
-	.size   __sealingkey, 8
+.include "assembly-helpers.s"
 
+	.hidden __sealingkey_either
+	.type   __sealingkey_either,@object
+	.section    .sealing_key1,"aw",@progbits
+	.globl  __sealingkey_either
+	.p2align    3
+__sealingkey_either:
+	.chericap   0
+	.size   __sealingkey_either, 8
+
+	.hidden __sealingkey_static
+	.type   __sealingkey_static,@object
+	.section    .sealing_key2,"aw",@progbits
+	.globl  __sealingkey_static
+	.p2align    3
+__sealingkey_static:
+	.chericap   0
+	.size   __sealingkey_static, 8
+
+	.hidden __sealingkey_dynamic
+	.type   __sealingkey_dynamic,@object
+	.section    .sealing_key3,"aw",@progbits
+	.globl  __sealingkey_dynamic
+	.p2align    3
+__sealingkey_dynamic:
+	.chericap   0
+	.size   __sealingkey_dynamic, 8
 
 .section .text,"ax",@progbits
 
@@ -19,87 +38,74 @@
 /**
  * The core of unsealing:
  *
- *   void *token_unseal_internal(struct SKeyStruct *, struct SObjStruct *, int);
+ *   void *token_unseal_internal(
+ *     struct SKeyStruct *, struct SObjStruct *, void *);
  */
-
 .Ltoken_unseal_internal:
   /*
    * Register allocation:
    *
-   *  - ca0 holds a sealing key, either the user's or the real deal, and is
-   *    replaced with the unsealed value or NULL
+   *  - ca0 holds the user's sealing key, and is replaced with the unsealed
+   *    value or NULL
    *
    *  - ca1 holds the user's sealed object pointer
    *
-   *  - a2 contains the expected sealing type.
+   *  - ca2 holds the unsealing authority and is clobbered on failure
+   *    explicitly and on success with a scalar (the sealed payload's length)
    *
-   *  - t0 holds a copy of the user key's address field (authorized type)
-   *
-   *  - t1 is used within each local computation and never holds secrets
+   *  - a3 is used within each local computation and never holds secrets
    */
 
   /* Verify key tag */
-  cgettag t1, ca0
-  beqz    t1, .Lexit_failure
+  cgettag a3, ca0
+  beqz    a3, .Lexit_failure
 
   /* Verify key address == base and len > 0 */
-  cgetbase t1, ca0
-  bne      a0, t1, .Lexit_failure // as-integer access to ca0 gives address
-  cgetlen  t1, ca0
-  beqz     t1, .Lexit_failure
+  cgetbase a3, ca0
+  bne      a0, a3, .Lexit_failure // as-integer access to ca0 gives address
+  cgetlen  a3, ca0
+  beqz     a3, .Lexit_failure
 
   /* Verify key has unseal permission */
-  cgetperm t1, ca0
-  andi     t1, t1, CHERI_PERM_UNSEAL
-  beqz     t1, .Lexit_failure
-
-  /* Copy key type to scratch register */
-  cgetaddr t0, ca0
-
-  /*
-   * Load unsealing root capability, to be clobbered by return value
-   * This faults only if something has gone very, very wrong, and exposes no
-   * secrets if so.
-   */
-.Lload_sealing_key:
-  auipcc ca0, %cheriot_compartment_hi(__sealingkey)
-  clc    ca0, %cheriot_compartment_lo_i(.Lload_sealing_key)(ca0)
-  csetaddr ca0, ca0, a2
+  cgetperm a3, ca0
+  andi     a3, a3, CHERI_PERM_UNSEAL
+  beqz     a3, .Lexit_failure
 
   /* Unseal, clobbering authority */
-  cunseal ca0, ca1, ca0
+  cunseal ca2, ca1, ca2
 
   /* Verify tag of unsealed form */
-  cgettag t1, ca0
-  beqz    t1, .Lexit_failure
+  cgettag a3, ca2
+  beqz    a3, .Lexit_failure
 
   /*
    * Load software type tag.  This will not trap, thanks to above tag check and
    * because IRQs are deferred (see our export entry below)
    */
-  clw t1, TokenSObj_offset_type(ca0)
+  clw a3, TokenSObj_offset_type(ca2)
 
   /* Verify that the loaded value matches the address of the key. */
-  bne t0, t1, .Lexit_failure
+  bne a0, a3, .Lexit_failure
 
   /* Subset bounds to ->data */
-  // Get the top into t1
-  cgettop         t1, ca0
-  // Move the address to the start of the data
-  cincoffset      ca0, ca0, TokenSObj_offset_data
+  // Get the top into a3
+  cgettop         a3, ca2
+  // Move the address to the start of the data, clobber the user's sealing key
+  cincoffset      ca0, ca2, TokenSObj_offset_data
   // Subtract the address of the (to-be-returned-unsealed) data from the top to
-  // give the length.
-  sub             t1, t1, a0
+  // give the length, clobbering our unsealing key.
+  sub             a2, a3, a0
   // Set the new bounds, using an exact setting so that any errors in the
   // allocator's alignment turn into an untagged capability here.
-  csetboundsexact ca0, ca0, t1
+  csetboundsexact ca0, ca0, a2
 
   /* And that's an unwrap. */
   cret
 
 .Lexit_failure:
-  /* Failure; clobber potential sensitive state in ca0 and return null */
-  cmove ca0, cnull
+  /* Failure; clobber potential sensitive state in ca2 and return null */
+  zeroOne a2
+  zeroOne a0
   cret
 
 /**
@@ -113,7 +119,16 @@
 	.hidden _Z16token_obj_unsealP10SKeyStructP10SObjStruct
 	.globl  _Z16token_obj_unsealP10SKeyStructP10SObjStruct
 _Z16token_obj_unsealP10SKeyStructP10SObjStruct:
-	cgettype a2, ca1
+	LoadCapPCC ca2, __sealingkey_either
+
+	/*
+	 * Backwards compatibility with CUnseal that requires address match.
+	 * This can (and should) be removed once everyone's caught up with
+	 * https://github.com/CHERIoT-Platform/cheriot-sail/pull/87 .
+	 */
+	cgettype   a3, ca1
+	csetaddr   ca2, ca2, a3
+
 	j        .Ltoken_unseal_internal
 
 /**
@@ -127,8 +142,8 @@
 	.hidden  _Z23token_obj_unseal_staticP10SKeyStructP10SObjStruct
 	.globl   _Z23token_obj_unseal_staticP10SKeyStructP10SObjStruct
 _Z23token_obj_unseal_staticP10SKeyStructP10SObjStruct:
-	li       a2, CheriSealTypeStaticToken
-	j        .Ltoken_unseal_internal
+	LoadCapPCC ca2, __sealingkey_static
+	j          .Ltoken_unseal_internal
 
 /**
  * An in-assembler implementation of
@@ -138,11 +153,11 @@
  *
  * The name has been manually mangled as per the C++ rules.
  */
-	.hidden  _Z16token_obj_unsealP10SKeyStructP10SObjStruct
-	.globl   _Z16token_obj_unsealP10SKeyStructP10SObjStruct
+	.hidden  _Z24token_obj_unseal_dynamicP10SKeyStructP10SObjStruct
+	.globl   _Z24token_obj_unseal_dynamicP10SKeyStructP10SObjStruct
 _Z24token_obj_unseal_dynamicP10SKeyStructP10SObjStruct:
-	li       a2, CheriSealTypeAllocator
-	j        .Ltoken_unseal_internal
+	LoadCapPCC ca2, __sealingkey_dynamic
+	j          .Ltoken_unseal_internal
 
 /* TODO: Eventually this goes away, when the assembler can generate it for us */
 CHERIOT_EXPORT_LIBCALL \
diff --git a/sdk/firmware.ldscript.in b/sdk/firmware.ldscript.in
index a9a3956..0730217 100644
--- a/sdk/firmware.ldscript.in
+++ b/sdk/firmware.ldscript.in
@@ -163,8 +163,8 @@
 		# Compartment switcher end
 		SHORT(.compartment_switcher_end - .compartment_switcher_start);
 		# Cross-compartment call return path
-		SHORT(switcher_skip_compartment_call - .compartment_switcher_start);
-		# Compartment switcher sealing key
+		SHORT(switcher_after_compartment_call - .compartment_switcher_start);
+		# Compartment switcher sealing keys
 		SHORT(compartment_switcher_sealing_key - .compartment_switcher_start);
 		# Switcher's copy of the scheduler's PCC.
 		SHORT(switcher_scheduler_entry_pcc - .compartment_switcher_start);
diff --git a/sdk/include/assembly-helpers.h b/sdk/include/assembly-helpers.h
index 73b0a68..a747f09 100644
--- a/sdk/include/assembly-helpers.h
+++ b/sdk/include/assembly-helpers.h
@@ -92,7 +92,7 @@
 #else
 #	define EXPORT_ASSEMBLY_NAME(name, value)
 #	define EXPORT_ASSEMBLY_EXPRESSION(name, expression, value)
-#	define EXPORT_ASSEMBLY_OFFSET(structure, field, name)
+#	define EXPORT_ASSEMBLY_OFFSET(structure, field, value)
 #	define EXPORT_ASSEMBLY_SIZE(structure, name, value)
 #	define EXPORT_ASSEMBLY_OFFSET_NAMED(structure, field, value, name)
 #endif
diff --git a/sdk/include/platform/sunburst/platform-i2c.hh b/sdk/include/platform/sunburst/platform-i2c.hh
index 2332a8a..ef93eee 100644
--- a/sdk/include/platform/sunburst/platform-i2c.hh
+++ b/sdk/include/platform/sunburst/platform-i2c.hh
@@ -4,101 +4,10 @@
 #include <stdint.h>
 
 /**
- * The interrupts of the OpenTitan's I2C block.
- *
- * Documentation source can be found at:
- * https://github.com/lowRISC/opentitan/blob/9ddf276c64e2974ed8e528e8b2feb00b977861de/hw/ip/i2c/doc/interfaces.md
- */
-enum class OpenTitanI2cInterrupt
-{
-	/**
-	 * A host mode interrupt. This is asserted whilst the Format FIFO level is
-	 * below the low threshold. This is a level status interrupt.
-	 */
-	FormatThreshold,
-	/**
-	 * A host mode interrupt. This is asserted whilst the Receive FIFO level is
-	 * above the high threshold. This is a level status interrupt.
-	 */
-	ReceiveThreshold,
-	/**
-	 * A target mode interrupt. This is asserted whilst the Aquired FIFO level
-	 * is above the high threshold. This is a level status interrupt.
-	 */
-	AcquiredThreshold,
-	/**
-	 * A host mode interrupt. This is raised if the Receive FIFO has overflowed.
-	 */
-	ReceiveOverflow,
-	/**
-	 * A host mode interrupt. This is raised if there is no ACK in response to
-	 * an address or data.
-	 */
-	Nak,
-	/**
-	 * A host mode interrupt. This is raised if the SCL line drops early (not
-	 * supported without clock synchronization).
-	 */
-	SclInterference,
-	/**
-	 * A host mode interrupt. This is raised if the SDA line goes low when host
-	 * is trying to assert high.
-	 */
-	SdaInterference,
-	/**
-	 * A host mode interrupt. This is raised if target stretches the clock
-	 * beyond the allowed timeout period.
-	 */
-	StretchTimeout,
-	/**
-	 * A host mode interrupt. This is raised if the target does not assert a
-	 * constant value of SDA during transmission.
-	 */
-	SdaUnstable,
-	/**
-	 * A host and target mode interrupt. In host mode, raised if the host issues
-	 * a repeated START or terminates the transaction by issuing STOP. In target
-	 * mode, raised if the external host issues a STOP or repeated START.
-	 */
-	CommandComplete,
-	/**
-	 * A target mode interrupt. This is raised if the target is stretching
-	 * clocks for a read command. This is a level status interrupt.
-	 */
-	TransmitStretch,
-	/**
-	 * A target mode interrupt. This is asserted whilst the Transmit FIFO level
-	 * is below the low threshold. This is a level status interrupt.
-	 */
-	TransmitThreshold,
-	/**
-	 * A target mode interrupt. This is raised if the target is stretching
-	 * clocks due to full Aquired FIFO or zero count in targetAckControl.NBYTES
-	 * (if enabled). This is a level status interrupt.
-	 */
-	AcquiredFull,
-	/**
-	 * A target mode interrupt. This is raised if STOP is received without a
-	 * preceding NACK during an external host read.
-	 */
-	UnexpectedStop,
-	/**
-	 * A target mode interrupt. This is raised if the host stops sending the
-	 * clock during an ongoing transaction.
-	 */
-	HostTimeout,
-};
-
-static constexpr uint32_t interrupt_bit(const OpenTitanI2cInterrupt Interrupt)
-{
-	return 1 << static_cast<uint32_t>(Interrupt);
-};
-
-/**
  * Driver for the OpenTitan's I2C block.
  *
  * Documentation source can be found at:
- * https://github.com/lowRISC/opentitan/tree/9ddf276c64e2974ed8e528e8b2feb00b977861de/hw/ip/i2c
+ * https://github.com/lowRISC/opentitan/tree/4fe1b8dd1a09af9dbc242434481ae031955dfd85/hw/ip/i2c
  */
 struct OpenTitanI2c
 {
@@ -158,10 +67,119 @@
 	 */
 	uint32_t targetNackCount;
 	/**
+	 * Controls for mid-transfer (N)ACK phase handling.
+	 */
+	uint32_t targetAckControl;
+	/// The data byte pending to be written to the Acquire (ACQ) FIFO.
+	uint32_t acquireFifoNextData;
+	/**
 	 * Timeout in Host-Mode for an unhandled NACK before hardware automatically
 	 * ends the transaction.
 	 */
-	uint32_t targetAckControl;
+	uint32_t hostNackHandlerTimeout;
+	/// Latched events that explain why the controller halted.
+	uint32_t controllerEvents;
+	/**
+	 * Latched events that can cause the target module to stretch the clock at
+	 * the beginning of a read transfer.
+	 */
+	uint32_t targetEvents;
+
+	/**
+	 * The interrupts of the OpenTitan's I2C block.
+	 *
+	 * Documentation source can be found at:
+	 * https://github.com/lowRISC/opentitan/blob/4fe1b8dd1a09af9dbc242434481ae031955dfd85/hw/ip/i2c/doc/interfaces.md
+	 */
+	enum class Interrupt
+	{
+		/**
+		 * A host mode interrupt. This is asserted whilst the Format FIFO level
+		 * is below the low threshold. This is a level status interrupt.
+		 */
+		FormatThreshold,
+		/**
+		 * A host mode interrupt. This is asserted whilst the Receive FIFO level
+		 * is above the high threshold. This is a level status interrupt.
+		 */
+		ReceiveThreshold,
+		/**
+		 * A target mode interrupt. This is asserted whilst the Aquired FIFO
+		 * level is above the high threshold. This is a level status interrupt.
+		 */
+		AcquiredThreshold,
+		/**
+		 * A host mode interrupt. This is raised if the Receive FIFO has
+		 * overflowed.
+		 */
+		ReceiveOverflow,
+		/**
+		 * A host mode interrupt. This is raised if the controller FSM is
+		 * halted, such as on an unexpected NACK or lost arbitration. Check the
+		 * `controllerEvents` register for the reason. The interrupt will only
+		 * be released when the bits in `controllerEvents` are cleared.
+		 */
+		ControllerHalt,
+		/**
+		 * A host mode interrupt. This is raised if the SCL line drops early
+		 * (not supported without clock synchronization).
+		 */
+		SclInterference,
+		/**
+		 * A host mode interrupt. This is raised if the SDA line goes low when
+		 * host is trying to assert high.
+		 */
+		SdaInterference,
+		/**
+		 * A host mode interrupt. This is raised if target stretches the clock
+		 * beyond the allowed timeout period.
+		 */
+		StretchTimeout,
+		/**
+		 * A host mode interrupt. This is raised if the target does not assert a
+		 * constant value of SDA during transmission.
+		 */
+		SdaUnstable,
+		/**
+		 * A host and target mode interrupt. In host mode, raised if the host
+		 * issues a repeated START or terminates the transaction by issuing
+		 * STOP. In target mode, raised if the external host issues a STOP or
+		 * repeated START.
+		 */
+		CommandComplete,
+		/**
+		 * A target mode interrupt. This is raised if the target is stretching
+		 * clocks for a read command. This is a level status interrupt.
+		 */
+		TransmitStretch,
+		/**
+		 * A target mode interrupt. This is asserted whilst the Transmit FIFO
+		 * level is below the low threshold. This is a level status interrupt.
+		 */
+		TransmitThreshold,
+		/**
+		 * A target mode interrupt. This is raised if the target is stretching
+		 * clocks due to full Aquired FIFO or zero count in
+		 * targetAckControl.NBYTES (if enabled). This is a level status
+		 * interrupt.
+		 */
+		AcquiredFull,
+		/**
+		 * A target mode interrupt. This is raised if STOP is received without a
+		 * preceding NACK during an external host read.
+		 */
+		UnexpectedStop,
+		/**
+		 * A target mode interrupt. This is raised if the host stops sending the
+		 * clock during an ongoing transaction.
+		 */
+		HostTimeout,
+	};
+
+	static constexpr uint32_t interrupt_bit(const Interrupt Interrupt)
+	{
+		return 1 << static_cast<uint32_t>(Interrupt);
+	};
 
 	/// Control Register Fields
 	enum [[clang::flag_enum]] : uint32_t{
@@ -172,6 +190,20 @@
 	  /// Enable I2C line loopback test If line loopback is enabled, the
 	  /// internal design sees ACQ and RX data as "1"
 	  ControlLineLoopback = 1 << 2,
+	  /// Enable NACKing the address on a stretch timeout. This is a target
+	  /// mode feature. If enabled, a stretch timeout will cause the device to
+	  /// NACK the address byte. If disabled, it will ACK instead.
+	  ControlNackAddressAfterTimeout = 1 << 3,
+	  /// Enable ACK Control Mode, which works with the `targetAckControl`
+	  /// register to allow software to control upper-layer (N)ACKing.
+	  ControlAckControlEnable = 1 << 4,
+	  /// Enable the bus monitor in multi-controller mode.
+	  ControlMultiControllerMonitorEnable = 1 << 5,
+	  /// If set, causes a read transfer addressed to the this target to set
+	  /// the corresponding bit in the `targetEvents` register. While the
+	  /// `transmitPending` field is 1, subsequent read transactions will
+	  /// stretch the clock, even if there is data in the Transmit FIFO.
+	  ControlTransmitStretchEnable = 1 << 6,
 	};
 
 	/// Status Register Fields
@@ -190,18 +222,15 @@
 	  SmatusReceiveEmpty = 1 << 5,
 	  /// Target mode Transmit FIFO is full
 	  StatusTransmitFull = 1 << 6,
-	  /// Target mode Receive FIFO is full
+	  /// Target mode Acquired FIFO is full
 	  StatusAcquiredFull = 1 << 7,
 	  /// Target mode Transmit FIFO is empty
 	  StatusTransmitEmpty = 1 << 8,
-	  /// Target mode Aquired FIFO is empty
+	  /// Target mode Acquired FIFO is empty
 	  StatusAcquiredEmpty = 1 << 9,
-	  /**
-	   * A Host-Mode active transaction has been ended by the
-	   * HostNackHandlerTimeout mechanism. This bit is cleared when
-	   * Control.EnableHost is set by software to start a new transaction.
-	   */
-	  StatusHostDisabledNackTimeout = 1 << 10,
+	  /// Target mode stretching at (N)ACK phase due to zero count
+	  /// in the `targetAckControl` register.
+	  StatusAckControlStretch = 1 << 10,
 	};
 
 	/// FormatData Register Fields
@@ -227,12 +256,36 @@
 	  FifoControlReceiveReset = 1 << 0,
 	  /// Format fifo reset. Write 1 to the register resets it. Read returns 0
 	  FifoControlFormatReset = 1 << 1,
-	  /// Aquired FIFO reset. Write 1 to the register resets it. Read returns 0
+	  /// Acquired FIFO reset. Write 1 to the register resets it. Read returns 0
 	  FifoControlAcquiredReset = 1 << 7,
 	  /// Transmit FIFO reset. Write 1 to the register resets it. Read returns 0
 	  FifoControlTransmitReset = 1 << 8,
 	};
 
+	/// ControllerEvents Register Fields
+	enum [[clang::flag_enum]] : uint32_t{
+	  /// Controller FSM is halted due to receiving an unexpected NACK.
+	  ControllerEventsNack = 1 << 0,
+	  /**
+	   * Controller FSM is halted due to a Host-Mode active transaction being
+	   * ended by the `hostNackHandlerTimeout` mechanism.
+	   */
+	  ControllerEventsUnhandledNackTimeout = 1 << 1,
+	  /**
+	   * Controller FSM is halted due to a Host-Mode active transaction being
+	   * terminated because of a bus timeout activated by `timeoutControl`.
+	   */
+	  ControllerEventsBusTimeout = 1 << 2,
+	  /**
+	   * Controller FSM is halted due to a Host-Mode active transaction being
+	   * terminated because of lost arbitration.
+	   */
+	  ControllerEventsArbitrationLost = 1 << 3,
+	};
+
+	// Referred to as 'RX FIFO' in the documentation
+	static constexpr uint32_t ReceiveFifoDepth = 8;
+
 	/// Flag set when we're debugging this driver.
 	static constexpr bool DebugOpenTitanI2c = true;
 
@@ -257,6 +310,26 @@
 		return static_cast<uint16_t>(Res);
 	}
 
+	/**
+	 * Reset the controller Events so that the `ControllerHalt` interrupt will
+	 * be released, allowing the I2C driver to continue after the controller
+	 * FSM has halted due to e.g. a NACK, configured timeout, or loss of
+	 * arbitration.
+	 *
+	 * Returns the (masked) result of reading the register before clearing
+	 * the controller events, so that you can use the `controllerEvent`
+	 * register fields to determine why the Controller FSM was halted.
+	 */
+	uint32_t reset_controller_events() volatile
+	{
+		constexpr uint32_t FieldMask =
+		  (ControllerEventsNack | ControllerEventsUnhandledNackTimeout |
+		   ControllerEventsBusTimeout | ControllerEventsArbitrationLost);
+		uint32_t events  = controllerEvents & FieldMask;
+		controllerEvents = FieldMask;
+		return events;
+	}
+
 	/// Reset all of the fifos.
 	void reset_fifos() volatile
 	{
@@ -336,14 +409,14 @@
 		return 0 != (StatusFormatEmpty & status);
 	}
 
-	void blocking_write(const uint8_t  Addr7,
-	                    const uint8_t  data[],
-	                    const uint32_t NumBytes,
-	                    const bool     SkipStop) volatile
+	[[nodiscard]] bool blocking_write(const uint8_t  Addr7,
+	                                  const uint8_t  data[],
+	                                  const uint32_t NumBytes,
+	                                  const bool     SkipStop) volatile
 	{
 		if (NumBytes == 0)
 		{
-			return;
+			return true;
 		}
 		blocking_write_byte(FormatDataStart | (Addr7 << 1) | 0u);
 		for (uint32_t i = 0; i < NumBytes - 1; ++i)
@@ -352,25 +425,34 @@
 		}
 		blocking_write_byte((SkipStop ? 0u : FormatDataStop) |
 		                    data[NumBytes - 1]);
+		while (!format_is_empty())
+		{
+			if (interrupt_is_asserted(Interrupt::ControllerHalt))
+			{
+				reset_controller_events();
+				return false;
+			}
+		}
+		return true;
 	}
 
 	[[nodiscard]] bool blocking_read(const uint8_t  Addr7,
 	                                 uint8_t        buf[],
 	                                 const uint32_t NumBytes) volatile
 	{
-		for (uint32_t idx = 0; idx < NumBytes; idx += UINT8_MAX)
+		for (uint32_t idx = 0; idx < NumBytes; idx += ReceiveFifoDepth)
 		{
 			blocking_write_byte(FormatDataStart | (Addr7 << 1) | 1u);
 			while (!format_is_empty()) {}
-			if (interrupt_is_asserted(OpenTitanI2cInterrupt::Nak))
+			if (interrupt_is_asserted(Interrupt::ControllerHalt))
 			{
-				interrupt_clear(OpenTitanI2cInterrupt::Nak);
+				reset_controller_events();
 				return false;
 			}
 			uint32_t bytesRemaining = NumBytes - idx;
-			bool     lastChunk      = UINT8_MAX >= bytesRemaining;
-			uint8_t  chunkSize =
-              lastChunk ? static_cast<uint8_t>(bytesRemaining) : UINT8_MAX;
+			bool     lastChunk      = ReceiveFifoDepth >= bytesRemaining;
+			uint8_t chunkSize = lastChunk ? static_cast<uint8_t>(bytesRemaining)
+			                              : ReceiveFifoDepth;
 
 			blocking_write_byte((lastChunk ? FormatDataStop : 0) |
 			                    FormatDataReadBytes | chunkSize);
@@ -385,26 +467,25 @@
 	}
 
 	/// Returns true if the given interrupt is asserted.
-	[[nodiscard]] bool
-	interrupt_is_asserted(OpenTitanI2cInterrupt interrupt) volatile
+	[[nodiscard]] bool interrupt_is_asserted(Interrupt interrupt) volatile
 	{
 		return 0 != (interruptState & interrupt_bit(interrupt));
 	}
 
 	/// Clears the given interrupt.
-	void interrupt_clear(OpenTitanI2cInterrupt interrupt) volatile
+	void interrupt_clear(Interrupt interrupt) volatile
 	{
 		interruptState = interrupt_bit(interrupt);
 	}
 
 	/// Enables the given interrupt.
-	void interrupt_enable(OpenTitanI2cInterrupt interrupt) volatile
+	void interrupt_enable(Interrupt interrupt) volatile
 	{
 		interruptEnable = interruptEnable | interrupt_bit(interrupt);
 	}
 
 	/// Disables the given interrupt.
-	void interrupt_disable(OpenTitanI2cInterrupt interrupt) volatile
+	void interrupt_disable(Interrupt interrupt) volatile
 	{
 		interruptEnable = interruptEnable & ~interrupt_bit(interrupt);
 	}
diff --git a/sdk/include/platform/sunburst/v0.2/platform-i2c.hh b/sdk/include/platform/sunburst/v0.2/platform-i2c.hh
new file mode 100644
index 0000000..2332a8a
--- /dev/null
+++ b/sdk/include/platform/sunburst/v0.2/platform-i2c.hh
@@ -0,0 +1,421 @@
+#pragma once
+#include <cdefs.h>
+#include <debug.hh>
+#include <stdint.h>
+
+/**
+ * The interrupts of the OpenTitan's I2C block.
+ *
+ * Documentation source can be found at:
+ * https://github.com/lowRISC/opentitan/blob/9ddf276c64e2974ed8e528e8b2feb00b977861de/hw/ip/i2c/doc/interfaces.md
+ */
+enum class OpenTitanI2cInterrupt
+{
+	/**
+	 * A host mode interrupt. This is asserted whilst the Format FIFO level is
+	 * below the low threshold. This is a level status interrupt.
+	 */
+	FormatThreshold,
+	/**
+	 * A host mode interrupt. This is asserted whilst the Receive FIFO level is
+	 * above the high threshold. This is a level status interrupt.
+	 */
+	ReceiveThreshold,
+	/**
+	 * A target mode interrupt. This is asserted whilst the Aquired FIFO level
+	 * is above the high threshold. This is a level status interrupt.
+	 */
+	AcquiredThreshold,
+	/**
+	 * A host mode interrupt. This is raised if the Receive FIFO has overflowed.
+	 */
+	ReceiveOverflow,
+	/**
+	 * A host mode interrupt. This is raised if there is no ACK in response to
+	 * an address or data.
+	 */
+	Nak,
+	/**
+	 * A host mode interrupt. This is raised if the SCL line drops early (not
+	 * supported without clock synchronization).
+	 */
+	SclInterference,
+	/**
+	 * A host mode interrupt. This is raised if the SDA line goes low when host
+	 * is trying to assert high.
+	 */
+	SdaInterference,
+	/**
+	 * A host mode interrupt. This is raised if target stretches the clock
+	 * beyond the allowed timeout period.
+	 */
+	StretchTimeout,
+	/**
+	 * A host mode interrupt. This is raised if the target does not assert a
+	 * constant value of SDA during transmission.
+	 */
+	SdaUnstable,
+	/**
+	 * A host and target mode interrupt. In host mode, raised if the host issues
+	 * a repeated START or terminates the transaction by issuing STOP. In target
+	 * mode, raised if the external host issues a STOP or repeated START.
+	 */
+	CommandComplete,
+	/**
+	 * A target mode interrupt. This is raised if the target is stretching
+	 * clocks for a read command. This is a level status interrupt.
+	 */
+	TransmitStretch,
+	/**
+	 * A target mode interrupt. This is asserted whilst the Transmit FIFO level
+	 * is below the low threshold. This is a level status interrupt.
+	 */
+	TransmitThreshold,
+	/**
+	 * A target mode interrupt. This is raised if the target is stretching
+	 * clocks due to full Aquired FIFO or zero count in targetAckControl.NBYTES
+	 * (if enabled). This is a level status interrupt.
+	 */
+	AcquiredFull,
+	/**
+	 * A target mode interrupt. This is raised if STOP is received without a
+	 * preceding NACK during an external host read.
+	 */
+	UnexpectedStop,
+	/**
+	 * A target mode interrupt. This is raised if the host stops sending the
+	 * clock during an ongoing transaction.
+	 */
+	HostTimeout,
+};
+
+static constexpr uint32_t interrupt_bit(const OpenTitanI2cInterrupt Interrupt)
+{
+	return 1 << static_cast<uint32_t>(Interrupt);
+};
+
+/**
+ * Driver for the OpenTitan's I2C block.
+ *
+ * Documentation source can be found at:
+ * https://github.com/lowRISC/opentitan/tree/9ddf276c64e2974ed8e528e8b2feb00b977861de/hw/ip/i2c
+ */
+struct OpenTitanI2c
+{
+	/// Interrupt State Register
+	uint32_t interruptState;
+	/// Interrupt Enable Register
+	uint32_t interruptEnable;
+	/// Interrupt Test Register
+	uint32_t interruptTest;
+	/// Alert Test Register (Unused in Sonata)
+	uint32_t alertTest;
+	/// I2C Control Register
+	uint32_t control;
+	/// I2C Live Status Register for Host and Target modes
+	uint32_t status;
+	/// I2C Read Data
+	uint32_t readData;
+	/// I2C Host Format Data
+	uint32_t formatData;
+	/// I2C FIFO control register
+	uint32_t fifoCtrl;
+	/// Host mode FIFO configuration
+	uint32_t hostFifoConfiguration;
+	/// Target mode FIFO configuration
+	uint32_t targetFifoConfiguration;
+	/// Host mode FIFO status register
+	uint32_t hostFifoStatus;
+	/// Target mode FIFO status register
+	uint32_t targetFifoStatus;
+	/// I2C Override Control Register
+	uint32_t override;
+	/// Oversampled Receive values
+	uint32_t values;
+	/**
+	 * Detailed I2C Timings (directly corresponding to table 10 in the I2C
+	 * Specification).
+	 */
+	uint32_t timing[5];
+	/// I2C clock stretching timeout control.
+	uint32_t timeoutControl;
+	/// I2C target address and mask pairs
+	uint32_t targetId;
+	/// I2C target acquired data
+	uint32_t acquiredData;
+	/// I2C target transmit data
+	uint32_t transmitData;
+	/**
+	 * I2C host clock generation timeout value (in units of input clock
+	 * frequency).
+	 */
+	uint32_t hostTimeoutControl;
+	/// I2C target internal stretching timeout control.
+	uint32_t targetTimeoutControl;
+	/**
+	 * Number of times the I2C target has NACK'ed a new transaction since the
+	 * last read of this register.
+	 */
+	uint32_t targetNackCount;
+	/**
+	 * Timeout in Host-Mode for an unhandled NACK before hardware automatically
+	 * ends the transaction.
+	 */
+	uint32_t targetAckControl;
+
+	/// Control Register Fields
+	enum [[clang::flag_enum]] : uint32_t{
+	  /// Enable Host I2C functionality
+	  ControlEnableHost = 1 << 0,
+	  /// Enable Target I2C functionality
+	  ControlEnableTarget = 1 << 1,
+	  /// Enable I2C line loopback test If line loopback is enabled, the
+	  /// internal design sees ACQ and RX data as "1"
+	  ControlLineLoopback = 1 << 2,
+	};
+
+	/// Status Register Fields
+	enum [[clang::flag_enum]] : uint32_t{
+	  /// Host mode Format FIFO is full
+	  StatusFormatFull = 1 << 0,
+	  /// Host mode Receive FIFO is full
+	  StatusReceiveFull = 1 << 1,
+	  /// Host mode Format FIFO is empty
+	  StatusFormatEmpty = 1 << 2,
+	  /// Host functionality is idle. No Host transaction is in progress
+	  StatusHostIdle = 1 << 3,
+	  /// Target functionality is idle. No Target transaction is in progress
+	  StatusTargetIdle = 1 << 4,
+	  /// Host mode Receive FIFO is empty
+	  SmatusReceiveEmpty = 1 << 5,
+	  /// Target mode Transmit FIFO is full
+	  StatusTransmitFull = 1 << 6,
+	  /// Target mode Receive FIFO is full
+	  StatusAcquiredFull = 1 << 7,
+	  /// Target mode Transmit FIFO is empty
+	  StatusTransmitEmpty = 1 << 8,
+	  /// Target mode Aquired FIFO is empty
+	  StatusAcquiredEmpty = 1 << 9,
+	  /**
+	   * A Host-Mode active transaction has been ended by the
+	   * HostNackHandlerTimeout mechanism. This bit is cleared when
+	   * Control.EnableHost is set by software to start a new transaction.
+	   */
+	  StatusHostDisabledNackTimeout = 1 << 10,
+	};
+
+	/// FormatData Register Fields
+	enum [[clang::flag_enum]] : uint32_t{
+	  /// Issue a START condition before transmitting BYTE.
+	  FormatDataStart = 1 << 8,
+	  /// Issue a STOP condition after this operation
+	  FormatDataStop = 1 << 9,
+	  /// Read BYTE bytes from I2C. (256 if BYTE==0)
+	  FormatDataReadBytes = 1 << 10,
+	  /**
+	   * Do not NACK the last byte read, let the read
+	   * operation continue
+	   */
+	  FormatDataReadCount = 1 << 11,
+	  /// Do not signal an exception if the current byte is not ACK’d
+	  FormatDataNakOk = 1 << 12,
+	};
+
+	/// FifoControl Register Fields
+	enum [[clang::flag_enum]] : uint32_t{
+	  /// Receive fifo reset. Write 1 to the register resets it. Read returns 0
+	  FifoControlReceiveReset = 1 << 0,
+	  /// Format fifo reset. Write 1 to the register resets it. Read returns 0
+	  FifoControlFormatReset = 1 << 1,
+	  /// Aquired FIFO reset. Write 1 to the register resets it. Read returns 0
+	  FifoControlAcquiredReset = 1 << 7,
+	  /// Transmit FIFO reset. Write 1 to the register resets it. Read returns 0
+	  FifoControlTransmitReset = 1 << 8,
+	};
+
+	/// Flag set when we're debugging this driver.
+	static constexpr bool DebugOpenTitanI2c = true;
+
+	/// Helper for conditional debug logs and assertions.
+	using Debug = ConditionalDebug<DebugOpenTitanI2c, "OpenTitan I2C">;
+
+	/**
+	 * Performs a 32-bit integer unsigned division, rounding up. The bottom
+	 * 16 bits of the result are then returned.
+	 *
+	 * As usual, a divisor of 0 is still Undefined Behavior.
+	 */
+	static uint16_t round_up_divide(uint32_t a, uint32_t b)
+	{
+		if (a == 0)
+		{
+			return 0;
+		}
+		const uint32_t Res = ((a - 1) / b) + 1;
+		Debug::Assert(Res <= UINT16_MAX,
+		              "Division result too large to fit in uint16_t.");
+		return static_cast<uint16_t>(Res);
+	}
+
+	/// Reset all of the fifos.
+	void reset_fifos() volatile
+	{
+		fifoCtrl = (FifoControlReceiveReset | FifoControlFormatReset |
+		            FifoControlAcquiredReset | FifoControlTransmitReset);
+	}
+
+	/// Configure the I2C block to be in host mode.
+	void host_mode_set() volatile
+	{
+		control = ControlEnableHost;
+	}
+
+	/**
+	 * Set the I2C timing parameters appropriately for the given bit rate.
+	 * Distilled from:
+	 * https://github.com/lowRISC/opentitan/blob/9ddf276c64e2974ed8e528e8b2feb00b977861de/hw/ip/i2c/doc/programmers_guide.md
+	 */
+	void speed_set(const uint32_t SpeedKhz) volatile
+	{
+		// We must round up the system clock frequency to lengthen intervals.
+		const uint16_t SystemClockKhz = round_up_divide(CPU_TIMER_HZ, 1000);
+		// We want to underestimate the clock period, to lengthen the timings.
+		const uint16_t ClockPeriod = (1000 * 1000) / SystemClockKhz;
+
+		// Decide which bus mode this represents
+		uint32_t mode = (SpeedKhz > 100u) + (SpeedKhz > 400u);
+
+		// Minimum fall time when V_DD is 3.3V
+		constexpr uint16_t MinimumFallTime = 20 * 3 / 5;
+		// Specification minimum timings (Table 10) in nanoseconds for each bus
+		// mode.
+		constexpr uint16_t MinimumTimeValues[5][2][3] = {
+		  {
+		    {4700u, 1300u, 150u}, // Low Period
+		    {4000u, 600u, 260u},  // High Period
+		  },
+		  {
+		    // Fall time of SDA and SCL signals
+		    {MinimumFallTime, MinimumFallTime, MinimumFallTime},
+		    // Rise time of SDA and SCL signals
+		    {120, 120, 120},
+		  },
+		  {
+		    {4700u, 600u, 260u}, // Hold time for a repeated start condition
+		    {4000u, 600u, 260u}, // Set-up time for a repeated start condition
+		  },
+		  {
+		    {4000u, 1u, 1u},   // Data hold time
+		    {500u, 100u, 50u}, // Data set-up time
+		  },
+		  {
+		    // Bus free time between a STOP and START condition
+		    {4700u, 1300u, 500u},
+		    // Set-up time for a STOP condition
+		    {4000u, 600u, 260u},
+		  },
+		};
+		for (uint32_t i = 0; i < 5; ++i)
+		{
+			timing[i] =
+			  (round_up_divide(MinimumTimeValues[i][0][mode], ClockPeriod)
+			   << 16) |
+			  round_up_divide(MinimumTimeValues[i][1][mode], ClockPeriod);
+		}
+	}
+
+	void blocking_write_byte(const uint32_t Fmt) volatile
+	{
+		while (0 != (StatusFormatFull & status)) {}
+		formatData = Fmt;
+	}
+
+	/// Returns true when the format fifo is empty
+	[[nodiscard]] bool format_is_empty() volatile
+	{
+		return 0 != (StatusFormatEmpty & status);
+	}
+
+	void blocking_write(const uint8_t  Addr7,
+	                    const uint8_t  data[],
+	                    const uint32_t NumBytes,
+	                    const bool     SkipStop) volatile
+	{
+		if (NumBytes == 0)
+		{
+			return;
+		}
+		blocking_write_byte(FormatDataStart | (Addr7 << 1) | 0u);
+		for (uint32_t i = 0; i < NumBytes - 1; ++i)
+		{
+			blocking_write_byte(data[i]);
+		}
+		blocking_write_byte((SkipStop ? 0u : FormatDataStop) |
+		                    data[NumBytes - 1]);
+	}
+
+	[[nodiscard]] bool blocking_read(const uint8_t  Addr7,
+	                                 uint8_t        buf[],
+	                                 const uint32_t NumBytes) volatile
+	{
+		for (uint32_t idx = 0; idx < NumBytes; idx += UINT8_MAX)
+		{
+			blocking_write_byte(FormatDataStart | (Addr7 << 1) | 1u);
+			while (!format_is_empty()) {}
+			if (interrupt_is_asserted(OpenTitanI2cInterrupt::Nak))
+			{
+				interrupt_clear(OpenTitanI2cInterrupt::Nak);
+				return false;
+			}
+			uint32_t bytesRemaining = NumBytes - idx;
+			bool     lastChunk      = UINT8_MAX >= bytesRemaining;
+			uint8_t  chunkSize =
+              lastChunk ? static_cast<uint8_t>(bytesRemaining) : UINT8_MAX;
+
+			blocking_write_byte((lastChunk ? FormatDataStop : 0) |
+			                    FormatDataReadBytes | chunkSize);
+			while (!format_is_empty()) {}
+
+			for (uint32_t chunkIdx = 0; chunkIdx < chunkSize; ++chunkIdx)
+			{
+				buf[idx + chunkIdx] = readData;
+			}
+		}
+		return true;
+	}
+
+	/// Returns true if the given interrupt is asserted.
+	[[nodiscard]] bool
+	interrupt_is_asserted(OpenTitanI2cInterrupt interrupt) volatile
+	{
+		return 0 != (interruptState & interrupt_bit(interrupt));
+	}
+
+	/// Clears the given interrupt.
+	void interrupt_clear(OpenTitanI2cInterrupt interrupt) volatile
+	{
+		interruptState = interrupt_bit(interrupt);
+	}
+
+	/// Enables the given interrupt.
+	void interrupt_enable(OpenTitanI2cInterrupt interrupt) volatile
+	{
+		interruptEnable = interruptEnable | interrupt_bit(interrupt);
+	}
+
+	/// Disables the given interrupt.
+	void interrupt_disable(OpenTitanI2cInterrupt interrupt) volatile
+	{
+		interruptEnable = interruptEnable & ~interrupt_bit(interrupt);
+	}
+
+	/**
+	 * Sets the thresholds for the format and receive fifos.
+	 */
+	void host_thresholds_set(uint16_t formatThreshold,
+	                         uint16_t receiveThreshold) volatile
+	{
+		hostFifoConfiguration =
+		  (formatThreshold & 0xfff) << 16 | (receiveThreshold & 0xfff);
+	}
+};
diff --git a/sdk/include/stdlib.h b/sdk/include/stdlib.h
index adc2143..54a9dc6 100644
--- a/sdk/include/stdlib.h
+++ b/sdk/include/stdlib.h
@@ -11,6 +11,13 @@
 #include <timeout.h>
 
 /**
+ * The SDK allocator implementation works in terms of "chunks" and has minimum
+ * size requirements for these.  This is occasionally visible to its clients,
+ * as documented on interface functions below.
+ */
+static const size_t CHERIOTHeapMinChunkSize = 16;
+
+/**
  * `MALLOC_QUOTA` sets the quota for the current compartment for use with
  * malloc and free.  This defaults to 4 KiB.
  */
@@ -135,9 +142,16 @@
 };
 
 /**
- * Non-standard allocation API.  Allocates `size` bytes.  Blocking behaviour is
- * controlled by the `flags` and the `timeout` parameters.
+ * Non-standard allocation API.  Allocates `size` bytes.
  *
+ * The `heapCapability` quota object must have remaining capacity sufficient
+ * for the requested `size` as well as any padding required by the CHERIoT
+ * capability encoding (see its ISA document for details) and any additional
+ * space required by the allocator's internal layout, which may be up to
+ * `CHERIOTHeapMinChunkSize` bytes.  Not all of these padding bytes may be
+ * available for use via the returned capability.
+ *
+ * Blocking behaviour is controlled by the `flags` and the `timeout` parameters.
  * Specifically, the `flags` parameter defines on which conditions to wait, and
  * the `timeout` parameter how long to wait.
  *
@@ -172,11 +186,11 @@
  * checking for arithmetic overflow. Similarly to `heap_allocate`, blocking
  * behaviour is controlled by the `flags` and the `timeout` parameters.
  *
- * See `heap_allocate` for more information on the blocking behavior.  One
- * difference between this and `heap_allocate` is the definition of when the
- * allocation cannot be satisfied under any circumstances, which is here if
- * `nmemb` * `size` is larger than the total heap size, or if `nmemb` * `size`
- * overflows.
+ * See `heap_allocate` for more information on the padding and blocking
+ * behavior.  One difference between this and `heap_allocate` is the definition
+ * of when the allocation cannot be satisfied under any circumstances, which is
+ * here if `nmemb` * `size` is larger than the total heap size, or if `nmemb` *
+ * `size` overflows.
  *
  * Similarly to `heap_allocate`, `-ENOTENOUGHSTACK` may be returned if the
  * stack is insufficiently large to run the function. See `heap_allocate`.
@@ -195,9 +209,11 @@
  * provided by the first argument until a corresponding call to `heap_free`.
  * Note that this can be used with interior pointers.
  *
- * This will return the size of the allocation claimed on success, 0 on error
- * (if `heapCapability` or `pointer` is not valid, etc.), or `-ENOTENOUGHSTACK`
- * if the stack is insufficiently large to run the function.
+ * This will return the size of the allocation claimed on success (which may be
+ * larger than the size requested in the original `heap_allocate` call; see its
+ * documentation for more information), 0 on error (if `heapCapability` or
+ * `pointer` is not valid, etc.), or `-ENOTENOUGHSTACK` if the stack is
+ * insufficiently large to run the function.
  */
 ssize_t __cheri_compartment("alloc")
   heap_claim(struct SObjStruct *heapCapability, void *pointer);
diff --git a/sdk/lib/crt/arith64.c b/sdk/lib/crt/arith64.c
index bb64553..611602c 100644
--- a/sdk/lib/crt/arith64.c
+++ b/sdk/lib/crt/arith64.c
@@ -25,6 +25,7 @@
 // - Add asm labels so that the compiler doesn't need to know the C++ type encodings for builtins.
 // - Use standard integer types.
 // - Add SPDX tags for license from the upstream repository (commit 426b7578ecfb5ce7c841e738613cff2a261214eb)
+// - Add the implementation of __multi3() 
 //
 // This file is *not* formatted, to make it easier to track changes from upstream (if there are any).
 
@@ -54,6 +55,7 @@
 int __cheri_libcall __popcountdi2(arith64_u64 a) __asm__("__popcountdi2");
 arith64_u64 __cheri_libcall __udivdi3(arith64_u64 a, arith64_u64 b) __asm__("__udivdi3");
 arith64_u64 __cheri_libcall __umoddi3(arith64_u64 a, arith64_u64 b) __asm__("__umoddi3");
+arith64_s64 __cheri_libcall __multi3(arith64_s64 a, arith64_s64 b) __asm__("__multi3");
 
 typedef union
 {
@@ -300,3 +302,9 @@
     __divmoddi4(a, b, &r);
     return r;
 }
+
+// Return the product of a and b
+[[clang::no_builtin]] arith64_s64 __multi3(arith64_s64 a, arith64_s64 b)
+{
+    return a * b;
+}
\ No newline at end of file
diff --git a/sdk/lib/unwind_error_handler/unwind.S b/sdk/lib/unwind_error_handler/unwind.S
index 6c74c06..8f179bb 100644
--- a/sdk/lib/unwind_error_handler/unwind.S
+++ b/sdk/lib/unwind_error_handler/unwind.S
@@ -6,7 +6,7 @@
  *
  * If there is no registered CleanupList structure (equivalently, there's no
  * CHERIOT_DURING block active at the time of the fault), then this requests
- * unwnding out of the compartment.  Otherwise, we will longjmp() out to the
+ * unwinding out of the compartment.  Otherwise, we will longjmp() out to the
  * indicated handler (that is, the CHERIOT_HANDLER block associated with the
  * current CHERIOT_DURING block), having reset the compartment error handler
  * invocation counter to zero.
diff --git a/sdk/privileged-compartment.ldscript b/sdk/privileged-compartment.ldscript
index c8f1b0a..ba0fdef 100644
--- a/sdk/privileged-compartment.ldscript
+++ b/sdk/privileged-compartment.ldscript
@@ -25,6 +25,7 @@
 		# The sealing keys for this compartment is before the import table, if they exist
 		*(.sealing_key1*)
 		*(.sealing_key2*)
+		*(.sealing_key3*)
 	}
 	# Lay out the compartment imports section.  This will end up on PCC.
 	.compartment_import_table : ALIGN(8)
diff --git a/tests/allocator-test.cc b/tests/allocator-test.cc
index 17faf66..05a4ac8 100644
--- a/tests/allocator-test.cc
+++ b/tests/allocator-test.cc
@@ -313,6 +313,13 @@
 		     "running claims tests",
 		     MALLOC_QUOTA,
 		     quotaLeft);
+		/*
+		 * Allocate sufficiently small objects that no additional alignment or
+		 * padding requirements arise from capability encoding.  Nevertheless,
+		 * because our allocator imposes minimal chunk sizes, we cannot be sure
+		 * that the underlying object is exactly this size.  When probing,
+		 * permit some slack, up to CHERIOTHeapMinChunkSize.
+		 */
 		size_t allocSize       = 128;
 		auto   mallocQuotaLeft = heap_quota_remaining(MALLOC_CAPABILITY);
 		CHERI::Capability alloc{
@@ -322,7 +329,8 @@
 		auto claim      = [&]() {
             ssize_t claimSize = heap_claim(SECOND_HEAP, alloc);
             claimCount++;
-            TEST(claimSize == allocSize,
+            TEST((allocSize <= claimSize) &&
+			            (claimSize <= allocSize + CHERIOTHeapMinChunkSize),
 			          "{}-byte allocation claimed as {} bytes (claim number {})",
 			          allocSize,
 			          claimSize,
diff --git a/tests/crash_recovery-test.cc b/tests/crash_recovery-test.cc
index 48dc278..cc67b24 100644
--- a/tests/crash_recovery-test.cc
+++ b/tests/crash_recovery-test.cc
@@ -13,8 +13,9 @@
 static void test_irqs_are_enabled()
 {
 	void *r = __builtin_return_address(0);
-	TEST(__builtin_cheri_type_get(r) == CheriSealTypeReturnSentryEnabling,
-	     "Calling context has IRQs disabled");
+	TEST_EQUAL(__builtin_cheri_type_get(r),
+	           CheriSealTypeReturnSentryEnabling,
+	           "Calling context has IRQs disabled");
 }
 
 extern "C" enum ErrorRecoveryBehaviour