diff --git a/experiments/atomic-codemode/README.md b/experiments/atomic-codemode/README.md
index cd24661b02..d81dfcb3ac 100644
--- a/experiments/atomic-codemode/README.md
+++ b/experiments/atomic-codemode/README.md
@@ -291,5 +291,7 @@ repeat, answer both local guards correctly without a whole-report fetch. Code
 Mode uses fewer MCP requests, but whole-task costs are mixed and a large capture
 time variation remains unexplained. Both clients already provide JavaScript
 orchestration. Source fidelity is not machine equivalence, provider parity or a
-general speedup. Case labels on the 149-way recovered dispatch remain a fact-export
-question; they cannot be inferred from edge ordinals.
+general speedup. The [native switch experiment](switch-study.md) now exports and independently checks
+182 labels over those 149 targets, exposes selected case-to-edge relations and
+keeps them readable when a 2 MiB native output budget omits the full graph.
+New real-model case/default verification is pending.
diff --git a/experiments/atomic-codemode/api.mjs b/experiments/atomic-codemode/api.mjs
index e1e0d21b2e..8731d0e9b4 100644
--- a/experiments/atomic-codemode/api.mjs
+++ b/experiments/atomic-codemode/api.mjs
@@ -50,6 +50,14 @@ const definition = (description, input, method, example) => ({
 });
 const operationSeeds = z.array(z.string()).min(1).max(128);
 const relationInput = z.discriminatedUnion("kind", [
+  z.strictObject({
+    snapshot,
+    kind: z.literal("cases"),
+    seeds: operationSeeds,
+    case_values: z.array(hex).max(128).optional(),
+    case_indices: z.array(z.number().int().nonnegative()).max(128).optional(),
+    ...page,
+  }),
   z.strictObject({
     snapshot,
     kind: z.literal("operands"),
@@ -71,6 +79,18 @@ const relationInput = z.discriminatedUnion("kind", [
   }),
 ]);
 export const methods = {
+  switches: definition(
+    "Inspect recovered indirect branches and their independent native jump-table metadata, without returning all case rows. Selector is the current recovered BRANCHIND input, which may be normalized rather than the machine jump address. Native consumed mask and signed rendering hint are not complete runtime/signedness proofs. Null tables/defaults stay unknown. The native model default out-edge is separate from any machine out-of-range guard destination. Use relations kind:cases for selected raw table rows, labels and their native mapping to recovered edges; row/edge ordinals are not case values. Available even when the full graph is unavailable if this independent facet was captured.",
+    {
+      snapshot,
+      ids: z.array(z.string()).max(128).optional(),
+      origin_addresses: z.array(hex).max(128).optional(),
+      fields: z.array(z.enum(["selector", "table"])).optional(),
+      ...page,
+    },
+    "switches",
+    'await rea.switches({snapshot:s,origin_addresses:["0x1000"]})',
+  ),
   functions: definition(
     "Search retained native callable entries by literal name/alias, exact name, or entry addresses. Names can match several entries, including PLT/import stubs and implementations; preserve all matches and select by address. A name does not establish runtime symbol binding.",
     {
@@ -158,7 +178,7 @@ export const methods = {
   ),
   relations: {
     description:
-      "Read native operands or definitions/uses for operation IDs, incoming/outgoing CFG edges or derived controllers for block IDs. operands pages every selected input slot, including constants, function inputs and null slots; input_indices optionally selects slots in caller order. Identity is snapshot + operation + input_index; value_id/definition and exact phi predecessor/edge bindings remain separate. Out-of-range slots of retained operations are absent; unretained_seeds remain unknown. A bounded call-rooted projection supports operands/definitions/uses but no CFG; uses cover retained selected operations only. Diagnostic SSA lacks native operands and has partial CFG/printed occurrences. controllers requires a complete recovered graph and concerns finite paths to recovered exits, not runtime feasibility.",
+      "Read native operands, definitions/uses or case rows for operation IDs; incoming/outgoing CFG edges or derived controllers for block IDs. cases pages one relation per case/out-edge, with a stable case_id; an unmapped case has one explicit unknown-edge row. total counts relations, not table rows. cases filters optional case_values (native labels tagged value) and case_indices (original row ordinals); both filters intersect and paging spans deduplicated seeds in caller order. Rows preserve missing/no-label status, original recovered target, and separate recovered edges. Partial/unavailable tables and unmapped rows are explicit; no runtime feasibility claim. operands pages every selected input slot, including constants, function inputs and null slots; input_indices optionally selects slots in caller order. Identity is snapshot + operation + input_index; value_id/definition and exact phi predecessor/edge bindings remain separate. Out-of-range slots of retained operations are absent; unretained_seeds remain unknown. A bounded call-rooted projection supports operands/definitions/uses but no CFG; uses cover retained selected operations only. Diagnostic SSA lacks native operands and has partial CFG/printed occurrences. controllers requires a complete recovered graph and concerns finite paths to recovered exits, not runtime feasibility.",
     input: relationInput,
     method: "relations",
     example:
diff --git a/experiments/atomic-codemode/api.test.mjs b/experiments/atomic-codemode/api.test.mjs
index 327463cfe2..598052d02f 100644
--- a/experiments/atomic-codemode/api.test.mjs
+++ b/experiments/atomic-codemode/api.test.mjs
@@ -29,6 +29,17 @@ test("relation identity and operand-only selectors agree in runtime and advertis
     [{ kind: "operands", seeds: ["0x1:0"], input_indices: [0, 155] }, true],
     [{ kind: "operands", seeds: ["0x1:0"], input_indices: [] }, true],
     [{ kind: "uses", seeds: ["0x1:0"] }, true],
+    [
+      {
+        kind: "cases",
+        seeds: ["0x1:0"],
+        case_values: ["0xffffffffffffffff"],
+        case_indices: [0, 155],
+      },
+      true,
+    ],
+    [{ kind: "cases", seeds: [0] }, false],
+    [{ kind: "cases", seeds: ["0x1:0"], case_values: ["0X1"] }, false],
     [{ kind: "incoming", seeds: [0] }, true],
     [{ kind: "incoming", seeds: ["0"] }, false],
     [{ kind: "operands", seeds: [0] }, false],
diff --git a/experiments/atomic-codemode/kuna-native-ir.patch b/experiments/atomic-codemode/kuna-native-ir.patch
index 1e10aa667e..2ec9a073ca 100644
--- a/experiments/atomic-codemode/kuna-native-ir.patch
+++ b/experiments/atomic-codemode/kuna-native-ir.patch
@@ -167,10 +167,10 @@ index 00000000..48631d39
 +}
 diff --git a/decompiler/crates/kuna-cli/src/atomic_json.rs b/decompiler/crates/kuna-cli/src/atomic_json.rs
 new file mode 100644
-index 00000000..7077bc56
+index 00000000..6005472b
 --- /dev/null
 +++ b/decompiler/crates/kuna-cli/src/atomic_json.rs
-@@ -0,0 +1,359 @@
+@@ -0,0 +1,456 @@
 +//! Opt-in atomic documents share the ordinary record producer and JSON writer.
 +//! A graph that cannot fit must not discard otherwise readable reconstructed C.
 +
@@ -291,6 +291,25 @@ index 00000000..7077bc56
 +    text.push('\n');
 +    Some(text)
 +}
++// Reclaim a saved independent facet when other omissions have made room.
++// Only bounded encoded strings coexist here, never cloned graph/facet trees.
++fn bounded_reclaiming(
++    document: &mut Json,
++    budget: usize,
++    name: &str,
++    saved: &mut Vec<RemovedFacet>,
++) -> Option<String> {
++    let base = bounded(document, budget)?;
++    if saved.is_empty() {
++        return Some(base);
++    }
++    restore_facet(document, std::mem::take(saved));
++    if let Some(complete) = bounded(document, budget) {
++        return Some(complete);
++    }
++    *saved = take_facet(document, name, budget + 1, Omission::Capacity);
++    Some(base)
++}
 +pub(crate) fn render(mut document: Json, limit: usize) -> Result<String, String> {
 +    let budget = limit
 +        .checked_sub(1)
@@ -307,7 +326,7 @@ index 00000000..7077bc56
 +        return Ok(text);
 +    }
 +    let originals = compress_graphs(&mut document, budget);
-+    let alternatives = if originals.is_empty() {
++    let mut alternatives = if originals.is_empty() {
 +        Vec::new()
 +    } else {
 +        if let Some(text) = bounded(&document, budget) {
@@ -315,24 +334,50 @@ index 00000000..7077bc56
 +        }
 +        exchange_graphs(&mut document, originals)
 +    };
-+    let calls = take_facet(&mut document, "atomic_calls", limit, Omission::Capacity);
-+    if !calls.is_empty() {
++    // New switch rows must not displace previously available graph/call facts.
++    // Retry without that independent facet before weakening existing coverage.
++    let mut switches = take_facet(&mut document, "atomic_switches", limit, Omission::Capacity);
++    if !switches.is_empty() {
 +        if let Some(text) = bounded(&document, budget) {
 +            return Ok(text);
 +        }
 +        if !alternatives.is_empty() {
-+            drop(exchange_graphs(&mut document, alternatives));
++            let originals = exchange_graphs(&mut document, alternatives);
 +            if let Some(text) = bounded(&document, budget) {
 +                return Ok(text);
 +            }
++            alternatives = exchange_graphs(&mut document, originals);
++        }
++    }
++    let calls = take_facet(&mut document, "atomic_calls", limit, Omission::Capacity);
++    if !calls.is_empty() {
++        if let Some(text) =
++            bounded_reclaiming(&mut document, budget, "atomic_switches", &mut switches)
++        {
++            return Ok(text);
++        }
++        if !alternatives.is_empty() {
++            drop(exchange_graphs(&mut document, alternatives));
++            if let Some(text) =
++                bounded_reclaiming(&mut document, budget, "atomic_switches", &mut switches)
++            {
++                return Ok(text);
++            }
 +        }
 +    }
 +    restore_facet(&mut document, calls);
 +    take_facet(&mut document, "atomic_facts", limit, Omission::Capacity);
 +    restore_facet(&mut document, projection);
++    restore_facet(&mut document, std::mem::take(&mut switches));
 +    if let Some(text) = bounded(&document, budget) {
 +        return Ok(text);
 +    }
++    switches = take_facet(&mut document, "atomic_switches", limit, Omission::Capacity);
++    if !switches.is_empty() {
++        if let Some(text) = bounded(&document, budget) {
++            return Ok(text);
++        }
++    }
 +    // Independent calls retain priority when the combined fallback is too big.
 +    let projection = take_facet(
 +        &mut document,
@@ -340,12 +385,14 @@ index 00000000..7077bc56
 +        limit,
 +        Omission::Capacity,
 +    );
-+    if let Some(text) = bounded(&document, budget) {
++    if let Some(text) = bounded_reclaiming(&mut document, budget, "atomic_switches", &mut switches)
++    {
 +        return Ok(text);
 +    }
 +    restore_facet(&mut document, projection);
 +    take_facet(&mut document, "atomic_calls", limit, Omission::Capacity);
-+    if let Some(text) = bounded(&document, budget) {
++    if let Some(text) = bounded_reclaiming(&mut document, budget, "atomic_switches", &mut switches)
++    {
 +        return Ok(text);
 +    }
 +    take_facet(
@@ -354,12 +401,62 @@ index 00000000..7077bc56
 +        limit,
 +        Omission::Capacity,
 +    );
-+    bounded(&document, budget).ok_or_else(|| {
++    bounded_reclaiming(&mut document, budget, "atomic_switches", &mut switches).ok_or_else(|| {
 +        format!("atomic JSON exceeds {limit} byte capacity even without recovered facets")
 +    })
 +}
 +
 +#[cfg(test)]
++mod switch_facet_tests {
++    use super::*;
++    fn document(graph: usize, calls: usize, projection: usize, switches: usize) -> Json {
++        Json::Object(vec![(
++            "functions".into(),
++            Json::Array(vec![Json::Object(vec![
++                ("code".into(), Json::Str("retained C".into())),
++                ("atomic_facts".into(), Json::Str("g".repeat(graph))),
++                ("atomic_calls".into(), Json::Str("c".repeat(calls))),
++                (
++                    "atomic_projection".into(),
++                    Json::Str("p".repeat(projection)),
++                ),
++                ("atomic_switches".into(), Json::Str("s".repeat(switches))),
++            ])]),
++        )])
++    }
++    #[test]
++    fn oversized_switches_do_not_displace_existing_graph_and_calls() {
++        let text = render(document(600, 20, 10, 5000), 1500).unwrap();
++        let d: serde_json::Value = serde_json::from_str(&text).unwrap();
++        let f = &d["functions"][0];
++        assert_eq!(f["code"], "retained C");
++        assert_eq!(f["atomic_facts"].as_str().unwrap().len(), 600);
++        assert_eq!(f["atomic_calls"].as_str().unwrap().len(), 20);
++        assert!(f.get("atomic_switches").is_none());
++        assert!(f["atomic_switches_error"].is_string());
++    }
++    #[test]
++    fn reclaim_switches_after_a_large_projection_is_omitted() {
++        let text = render(document(5000, 100, 3000, 100), 2000).unwrap();
++        let d: serde_json::Value = serde_json::from_str(&text).unwrap();
++        let f = &d["functions"][0];
++        assert_eq!(f["atomic_calls"].as_str().unwrap().len(), 100);
++        assert_eq!(f["atomic_switches"].as_str().unwrap().len(), 100);
++        assert!(f.get("atomic_projection").is_none());
++        assert!(f.get("atomic_switches_error").is_none());
++    }
++    #[test]
++    fn independent_switch_rows_survive_when_all_other_facets_overflow() {
++        let text = render(document(5000, 5000, 5000, 1200), 2000).unwrap();
++        let d: serde_json::Value = serde_json::from_str(&text).unwrap();
++        let f = &d["functions"][0];
++        assert_eq!(f["code"], "retained C");
++        assert_eq!(f["atomic_switches"].as_str().unwrap().len(), 1200);
++        assert!(f.get("atomic_switches_error").is_none());
++    }
++}
++
++#[cfg(test)]
 +mod tests {
 +    use super::*;
 +
@@ -668,7 +765,7 @@ index ad249b04..62074996 100644
          failure = Some(format!("--assert directive rejected in {}", args.binary));
      }
 diff --git a/decompiler/crates/kuna-cli/src/decompile_all.rs b/decompiler/crates/kuna-cli/src/decompile_all.rs
-index 698c7243..330c0f3f 100644
+index 698c7243..21147ba5 100644
 --- a/decompiler/crates/kuna-cli/src/decompile_all.rs
 +++ b/decompiler/crates/kuna-cli/src/decompile_all.rs
 @@ -744,6 +744,7 @@ fn run_jobs_worker(args: &Args) -> Result<(), String> {
@@ -724,19 +821,20 @@ index 698c7243..330c0f3f 100644
  /// [`render_result_json`] plus the inventory `total` a NARROWED whole-binary run
  /// answers with.
  ///
-@@ -2152,6 +2168,11 @@ fn result_json(
+@@ -2152,6 +2168,12 @@ fn result_json(
                      // Always present, `[]` unless the option is on.
                      ("types".into(), types),
                  ];
 +                if let Some(detail) = f.detail.as_ref() {
 +                    append_atomic_facet(&mut record, "atomic_facts", detail.atomic_facts.as_ref());
 +                    append_atomic_facet(&mut record, "atomic_calls", detail.atomic_calls.as_ref());
++                    append_atomic_facet(&mut record, "atomic_switches", detail.atomic_switches.as_ref());
 +                    append_atomic_facet(&mut record, "atomic_projection", detail.atomic_projection.as_ref());
 +                }
                  if !f.stack_objects.is_empty() {
                      record.push(("stack_objects".into(), Json::Array(
                          f.stack_objects.iter().map(stack_object_json).collect(),
-@@ -3519,3 +3540,16 @@ mod triage_tests {
+@@ -3519,3 +3541,16 @@ mod triage_tests {
      }
  
  }
@@ -1053,20 +1151,21 @@ index e40b18c9..b8cae233 100644
      };
  
 diff --git a/decompiler/crates/kuna-console/src/inspect.rs b/decompiler/crates/kuna-console/src/inspect.rs
-index 74024b10..72e4ec24 100644
+index 74024b10..a41465a6 100644
 --- a/decompiler/crates/kuna-console/src/inspect.rs
 +++ b/decompiler/crates/kuna-console/src/inspect.rs
-@@ -24,6 +24,9 @@ pub const FUNCTION_ROW_CAP: usize = 4096;
+@@ -24,6 +24,10 @@ pub const FUNCTION_ROW_CAP: usize = 4096;
  pub struct FuncDetail {
      pub tokens: Vec<CodeToken>,
      pub tokens_error: Option<String>,
 +    pub atomic_facts: Option<Result<kuna_decomp::atomic_facts::FunctionFacts, String>>,
 +    pub atomic_calls: Option<Result<kuna_decomp::atomic_calls::CallFacts, String>>,
++    pub atomic_switches: Option<Result<kuna_decomp::atomic_switches::SwitchFacts, String>>,
 +    pub atomic_projection: Option<Result<kuna_decomp::atomic_projection::Projection, String>>,
  }
  
  impl FuncDetail {
-@@ -40,13 +43,13 @@ impl FuncDetail {
+@@ -40,13 +44,13 @@ impl FuncDetail {
      ) -> Self {
          let mut tokens = kuna_srcmap::resolve(fd, var_refs, raw, untrimmed, variables);
          if let Err(error) = kuna_srcmap::verify(&tokens, code) {
@@ -1083,7 +1182,7 @@ index 74024b10..72e4ec24 100644
  }
  
 diff --git a/decompiler/crates/kuna-console/src/project.rs b/decompiler/crates/kuna-console/src/project.rs
-index bc401db2..1b53ccf1 100644
+index bc401db2..7b7c7c24 100644
 --- a/decompiler/crates/kuna-console/src/project.rs
 +++ b/decompiler/crates/kuna-console/src/project.rs
 @@ -245,6 +245,8 @@ pub struct DecompileOptions {
@@ -1119,7 +1218,7 @@ index bc401db2..1b53ccf1 100644
          want_pointer_arguments,
          ..
      } = *opts;
-@@ -838,11 +843,21 @@ pub fn decompile_pulled(
+@@ -838,11 +843,23 @@ pub fn decompile_pulled(
                          }
                      }
                      let var_refs = provenance.apply_to_variables_with_refs(&fd, &mut variables);
@@ -1134,6 +1233,8 @@ index bc401db2..1b53ccf1 100644
 +                        let membership = kuna_decomp::atomic_membership::inspect(&fd);
 +                        detail.atomic_calls = Some(membership.as_ref().map_err(Clone::clone)
 +                            .and_then(|m| kuna_decomp::atomic_calls::collect_all(&fd, m)));
++                        detail.atomic_switches = Some(membership.as_ref().map_err(Clone::clone)
++                            .and_then(|m| kuna_decomp::atomic_switches::collect(&fd, m)));
 +                        detail.atomic_facts = Some(membership.as_ref().map_err(Clone::clone)
 +                            .and_then(|m| kuna_decomp::atomic_facts::collect(prog.arch(), &fd, m)));
 +                        detail.atomic_projection = Some(membership.as_ref().map_err(Clone::clone)
@@ -1159,6 +1260,59 @@ index 40b093b6..8f03b654 100644
  toml = { version = "1.1", default-features = false, features = ["parse", "serde", "std"] }
  
  [build-dependencies]
+diff --git a/decompiler/crates/kuna-decomp/src/p2_lift/jumptable.rs b/decompiler/crates/kuna-decomp/src/p2_lift/jumptable.rs
+index b2677f6c..5e913130 100644
+--- a/decompiler/crates/kuna-decomp/src/p2_lift/jumptable.rs
++++ b/decompiler/crates/kuna-decomp/src/p2_lift/jumptable.rs
+@@ -5481,6 +5481,22 @@ impl JumpTable {
+         self.label[index as usize]
+     }
+ 
++    /// Borrow observed rows for read-only analysis without indexing absent labels.
++    /// Row order, labels and recovered out-edge positions are separate identities.
++    pub fn case_rows(&self) -> KunaResult<impl ExactSizeIterator<Item = (usize, &Address, Option<uintb>)>> {
++        if self.label.len() > self.addresstable.len() {
++            return Err(KunaError::lowlevel("jump-table labels exceed address rows"));
++        }
++        Ok(self.addresstable.iter().enumerate().map(|(index, address)| {
++            (index, address, self.label.get(index).copied())
++        }))
++    }
++
++    /// Borrow the native row-to-out-edge mapping; never infer it from addresses.
++    pub fn case_edge_rows(&self) -> impl ExactSizeIterator<Item = (int4, int4)> + '_ {
++        self.block2addr.iter().map(|pair| (pair.address_index, pair.block_position))
++    }
++
+     /// Force a given basic-block to be a switch destination
+     /// (C++ `JumpTable::addBlockToSwitch`, `jumptable.cc:2663`).
+     pub fn add_block_to_switch(&mut self, fd: &Funcdata, bl: BlockId, lab: uintb) -> KunaResult<()> {
+diff --git a/decompiler/crates/kuna-decomp/src/p2_lift/jumptable/tests.rs b/decompiler/crates/kuna-decomp/src/p2_lift/jumptable/tests.rs
+index 8aad0172..2f69df2d 100644
+--- a/decompiler/crates/kuna-decomp/src/p2_lift/jumptable/tests.rs
++++ b/decompiler/crates/kuna-decomp/src/p2_lift/jumptable/tests.rs
+@@ -725,3 +725,21 @@ fn guard_range_retry_keeps_both_wrapped_bounds() {
+     model.calc_range(&fd, input, &mut range);
+     assert_eq!((range.get_min(), range.get_end(), range.get_size()), (58, 62, 4));
+ }
++
++#[test]
++fn atomic_case_rows_keep_ordinals_labels_and_edges_separate() {
++    let manage = build_manager();
++    let ram = Rc::clone(manage.get_space_by_name("ram").unwrap());
++    let mut table = JumpTable::new(Address::new(Rc::clone(&ram), 0x1000));
++    table.kuna_push_entry(Address::new(Rc::clone(&ram), 0x3000), 2, 0x77);
++    table.kuna_push_entry(Address::new(Rc::clone(&ram), 0x4000), 0, NO_LABEL);
++    table.kuna_finalize(0);
++    let rows: Vec<_> = table.case_rows().unwrap()
++        .map(|(index, address, label)| (index, address.get_offset(), label)).collect();
++    assert_eq!(rows, vec![(0, 0x3000, Some(0x77)), (1, 0x4000, Some(NO_LABEL))]);
++    assert_eq!(table.case_edge_rows().collect::<Vec<_>>(), vec![(1, 0), (0, 2)]);
++    table.label.pop();
++    assert_eq!(table.case_rows().unwrap().nth(1).unwrap().2, None);
++    table.label.extend([1, 2]);
++    assert!(table.case_rows().is_err());
++}
 diff --git a/decompiler/crates/kuna-decomp/src/substrate/atomic_calls.rs b/decompiler/crates/kuna-decomp/src/substrate/atomic_calls.rs
 new file mode 100644
 index 00000000..2b7ced64
@@ -1545,21 +1699,23 @@ index 00000000..6b9afe69
 +}
 diff --git a/decompiler/crates/kuna-decomp/src/substrate/atomic_membership.rs b/decompiler/crates/kuna-decomp/src/substrate/atomic_membership.rs
 new file mode 100644
-index 00000000..6628ddd7
+index 00000000..be11e472
 --- /dev/null
 +++ b/decompiler/crates/kuna-decomp/src/substrate/atomic_membership.rs
-@@ -0,0 +1,64 @@
+@@ -0,0 +1,76 @@
 +//! One validated membership scan for independent recovered fact facets.
 +use crate::{context::OpId, funcdata::Funcdata};
 +use kuna_num::opcodes::OpCode;
 +use std::collections::HashSet;
 +
 +pub const MAX_CALLS: usize = 12_000;
++const MAX_SWITCHES: usize = 12_000;
 +// Bound the optional membership index separately from call discovery. Crossing
 +// this resource budget disables projections, without discarding known calls.
 +const MAX_INDEXED_OPERATIONS: usize = 65_536;
 +pub struct Membership {
 +    pub calls: Vec<OpId>,
++    pub switches: Option<Vec<OpId>>,
 +    pub members: Option<HashSet<OpId>>,
 +    pub blocks_examined: i32,
 +    pub operations_examined: usize,
@@ -1570,6 +1726,7 @@ index 00000000..6628ddd7
 +    }
 +    let mut result = Membership {
 +        calls: Vec::new(),
++        switches: Some(Vec::new()),
 +        members: Some(HashSet::new()),
 +        blocks_examined: fd.bblocks_get_size(),
 +        operations_examined: 0,
@@ -1606,6 +1763,15 @@ index 00000000..6628ddd7
 +                }
 +                result.calls.push(key);
 +            }
++            if op.code() == OpCode::CPUI_BRANCHIND {
++                if let Some(switches) = result.switches.as_mut() {
++                    if switches.len() == MAX_SWITCHES {
++                        result.switches = None;
++                    } else {
++                        switches.push(key);
++                    }
++                }
++            }
 +        }
 +        if examined != expected {
 +            return Err("native block operation count mismatch".into());
@@ -1861,6 +2027,210 @@ index 00000000..097b153a
 +        },
 +    })
 +}
+diff --git a/decompiler/crates/kuna-decomp/src/substrate/atomic_switches.rs b/decompiler/crates/kuna-decomp/src/substrate/atomic_switches.rs
+new file mode 100644
+index 00000000..e8992d5d
+--- /dev/null
++++ b/decompiler/crates/kuna-decomp/src/substrate/atomic_switches.rs
+@@ -0,0 +1,198 @@
++//! Read-only native jump-table facts; row ordinals are not case values.
++use crate::{
++    atomic_membership::Membership,
++    atomic_values::{self, operation_id, ValueFact},
++    funcdata::Funcdata,
++    jumptable::NO_LABEL,
++};
++use kuna_base::address::Address;
++use serde::Serialize;
++use std::collections::{BTreeMap, BTreeSet};
++
++const MAX_ROWS: usize = 100_000;
++const MAX_MAPPINGS: usize = 100_000;
++#[derive(Debug, Clone, Serialize)]
++pub struct SwitchFacts {
++    pub schema_version: u32,
++    pub items: Vec<SwitchFact>,
++    pub coverage: Coverage,
++}
++#[derive(Debug, Clone, Serialize)]
++pub struct Coverage {
++    pub scope: &'static str,
++    pub blocks_examined: i32,
++    pub operations_examined: usize,
++    pub machine_semantic_equivalence: &'static str,
++}
++#[derive(Debug, Clone, Serialize)]
++pub struct SwitchFact {
++    pub id: String,
++    pub origin_address: String,
++    pub block: i32,
++    pub selector: Option<ValueFact>,
++    pub table: Option<Table>,
++}
++#[derive(Debug, Clone, Serialize)]
++pub struct Table {
++    pub partial: bool,
++    pub labelled: bool,
++    pub consumed_mask: String,
++    pub signed_render_hint: bool,
++    pub default_raw_index: i32,
++    pub default_edge: Option<Edge>,
++    pub default_is_folded: bool,
++    pub rows: Vec<Row>,
++}
++#[derive(Debug, Clone, Serialize)]
++pub struct Edge {
++    pub id: String,
++    pub index: i32,
++    pub target: i32,
++}
++#[derive(Debug, Clone, Serialize)]
++pub struct Row {
++    pub index: usize,
++    pub label: Option<Label>,
++    pub recovered_target: Option<Location>,
++    pub edges: Vec<Edge>,
++}
++#[derive(Debug, Clone, Serialize)]
++pub struct Label {
++    pub status: &'static str,
++    pub raw_bits: String,
++}
++#[derive(Debug, Clone, Serialize)]
++pub struct Location {
++    pub space: String,
++    pub offset: String,
++}
++fn location(
++    address: &Address,
++    text: &mut atomic_values::TextBudget,
++) -> Result<Option<Location>, String> {
++    let Some(space) = address.get_space() else {
++        return Ok(None);
++    };
++    text.charge(space.get_name().len())?;
++    Ok(Some(Location {
++        space: space.get_name().to_string(),
++        offset: format!("0x{:x}", address.get_offset()),
++    }))
++}
++fn edge(fd: &Funcdata, parent: crate::context::BlockId, index: i32) -> Result<Edge, String> {
++    let block = fd.bblocks_ref().block(parent);
++    if index < 0 || index >= block.size_out() {
++        return Err("native switch out-edge index is outside its block".into());
++    }
++    Ok(Edge {
++        id: format!("{}:{index}", block.get_index()),
++        index,
++        target: fd.bblocks_ref().block(block.get_out(index)).get_index(),
++    })
++}
++pub fn collect(fd: &Funcdata, membership: &Membership) -> Result<SwitchFacts, String> {
++    let switches = membership
++        .switches
++        .as_ref()
++        .ok_or("atomic switch capacity exceeded")?;
++    let mut items = Vec::with_capacity(switches.len());
++    let mut row_count = 0usize;
++    let mut mapping_count = 0usize;
++    let mut text = atomic_values::TextBudget::new(2 * 1024 * 1024);
++    for &key in switches {
++        let op = fd.obank().get(key).ok_or("stale switch operation")?;
++        let parent = op.get_parent().ok_or("native switch has no block")?;
++        let mut values = BTreeSet::new();
++        if let Some(value) = op.get_in(0) {
++            values.insert(value);
++        }
++        let selector = atomic_values::collect(fd, values, &mut text)?.pop();
++        if let Some(space) = selector.as_ref().and_then(|value| value.space.as_ref()) {
++            text.charge(space.len())?;
++        }
++        let table = if let Some(table) = fd.find_jump_table(key) {
++            if table.get_indirect_op() != Some(key) {
++                return Err("native jump-table operation identity is unresolved".into());
++            }
++            let observed = table.case_rows().map_err(|e| e.to_string())?;
++            row_count = row_count
++                .checked_add(observed.len())
++                .ok_or("atomic case count overflow")?;
++            let mappings = table.case_edge_rows();
++            mapping_count = mapping_count
++                .checked_add(mappings.len())
++                .ok_or("atomic case edge count overflow")?;
++            if row_count > MAX_ROWS || mapping_count > MAX_MAPPINGS {
++                return Err("atomic switch row/mapping capacity exceeded".into());
++            }
++            let mut by_row: BTreeMap<usize, Vec<Edge>> = BTreeMap::new();
++            let mut seen = BTreeSet::new();
++            for (row, position) in mappings {
++                if row < 0 || row as usize >= observed.len() {
++                    return Err("native switch mapping names an absent address row".into());
++                }
++                if !seen.insert((row, position)) {
++                    return Err("duplicate native switch row/out-edge mapping".into());
++                }
++                by_row
++                    .entry(row as usize)
++                    .or_default()
++                    .push(edge(fd, parent, position)?);
++            }
++            let rows = observed
++                .map(|(index, address, label)| {
++                    Ok(Row {
++                        index,
++                        label: label.map(|bits| Label {
++                            status: if bits == NO_LABEL {
++                                "no-label"
++                            } else {
++                                "value"
++                            },
++                            raw_bits: format!("0x{bits:x}"),
++                        }),
++                        recovered_target: location(address, &mut text)?,
++                        edges: by_row.remove(&index).unwrap_or_default(),
++                    })
++                })
++                .collect::<Result<Vec<_>, String>>()?;
++            let raw_default = table.get_default_block();
++            if raw_default < -1 {
++                return Err("invalid native default out-edge index".into());
++            }
++            Some(Table {
++                partial: table.is_partial(),
++                labelled: table.is_labelled(),
++                consumed_mask: format!("0x{:x}", table.get_switch_var_consume()),
++                signed_render_hint: table.kuna_has_signed_labels(),
++                default_raw_index: raw_default,
++                default_edge: if raw_default == -1 {
++                    None
++                } else {
++                    Some(edge(fd, parent, raw_default)?)
++                },
++                default_is_folded: table.has_folded_default(),
++                rows,
++            })
++        } else {
++            None
++        };
++        items.push(SwitchFact {
++            id: operation_id(fd, key)?,
++            origin_address: format!("0x{:x}", op.get_addr().get_offset()),
++            block: fd.bblocks_ref().block(parent).get_index(),
++            selector,
++            table,
++        });
++    }
++    Ok(SwitchFacts {
++        schema_version: 1,
++        items,
++        coverage: Coverage {
++            scope: "all recovered block-member BRANCHIND operations and native jump-table rows",
++            blocks_examined: membership.blocks_examined,
++            operations_examined: membership.operations_examined,
++            machine_semantic_equivalence: "unknown",
++        },
++    })
++}
 diff --git a/decompiler/crates/kuna-decomp/src/substrate/atomic_values.rs b/decompiler/crates/kuna-decomp/src/substrate/atomic_values.rs
 new file mode 100644
 index 00000000..6d23954c
@@ -1961,10 +2331,10 @@ index 39927ceb..844950a6 100644
      let num_input = fd.obank().get(op).ok_or_else(|| "render_op: stale op".to_string())?.num_input();
      let in_at = |i: int4| -> Option<VarnodeId> { fd.obank().get(op).and_then(|o| o.get_in(i)) };
 diff --git a/decompiler/crates/kuna-decomp/src/substrate/mod.rs b/decompiler/crates/kuna-decomp/src/substrate/mod.rs
-index 00528cb5..b019a174 100644
+index 00528cb5..d3f422ee 100644
 --- a/decompiler/crates/kuna-decomp/src/substrate/mod.rs
 +++ b/decompiler/crates/kuna-decomp/src/substrate/mod.rs
-@@ -11,6 +11,12 @@ pub mod funcdata_block;
+@@ -11,6 +11,13 @@ pub mod funcdata_block;
  pub mod funcdata_encode;
  pub mod funcdata_op;
  pub mod funcdata_printraw;
@@ -1974,20 +2344,40 @@ index 00528cb5..b019a174 100644
 +pub mod atomic_operations;
 +pub mod atomic_projection;
 +pub mod atomic_values;
++pub mod atomic_switches;
  pub mod funcdata_varnode;
  pub mod dtype;
  pub mod context;
 diff --git a/docs/spec/00-overview.md b/docs/spec/00-overview.md
-index ce499c4f..b3b53dcf 100644
+index ce499c4f..9d927aa5 100644
 --- a/docs/spec/00-overview.md
 +++ b/docs/spec/00-overview.md
-@@ -3431,3 +3431,79 @@ Reserving it creates no analysis varnode and changes no physical mapping or
+@@ -3431,3 +3431,98 @@ Reserving it creates no analysis varnode and changes no physical mapping or
  emitted C. Ghidra receives temporary storage for the logical local, rather than
  a persistable ordinary stack-variable location; ordinary symbol storage and
  register-plus-stack parameter JOINs keep their existing encoding.
 +
 +## Experimental read-only atomic facts
 +
++The same opt-in capture also exports an independent version-1 `atomic_switches`
++facet. One membership scan supplies recovered BRANCHIND identities. Native
++jump-table rows retain their original index, optional label/status, original
++target address and native row-to-out-edge mapping. Indexes are never treated as
++case values or mapped by comparing optimized block start addresses. Missing
++tables/labels/mappings, the reserved no-label marker and partial tables remain
++explicit. A native model default out-edge is separate from any machine
++out-of-range guard destination. Selector values and consumed-bit masks do not establish runtime
++feasibility or machine semantic equivalence; the native signed-label flag is a
++render hint, not a general signedness proof.
++
++Construction admits 12,000 switches, 100,000 rows and row/edge mappings, and a
++2 MiB shared selector/type/address-space text budget. Mapping is indexed once
++instead of scanning every edge for every case. New switch rows cannot displace
++otherwise fitting existing graph/call facts: the bounded document writer retries
++without this facet first, retains explicit capacity errors, and can still keep
++the independent rows if other facets overflow. Ordinary non-opt-in analysis and
++executable bytes are unchanged.
++
 +The opt-in `decompile --json --atomic-facts` surface captures the same live
 +function after C rendering (`decompiler/crates/kuna-decomp/src/substrate/atomic_facts.rs`).
 +It does not change the analysis phases or C output. The default path does not
diff --git a/experiments/atomic-codemode/native-call-views.mjs b/experiments/atomic-codemode/native-call-views.mjs
index 92d4a5fcf5..535b996d57 100644
--- a/experiments/atomic-codemode/native-call-views.mjs
+++ b/experiments/atomic-codemode/native-call-views.mjs
@@ -1,5 +1,5 @@
 import { callCoverage } from "./native-calls.mjs";
-import { requireFact } from "./native-contract.mjs";
+import { requireFact, requireSameNativeValue } from "./native-contract.mjs";
 import { uniqueNative, readNativeIdentities } from "./native-reads.mjs";
 import { freezeFacts } from "./fact-reads.mjs";
 
@@ -82,10 +82,9 @@ export function validateCallGraph(callIndex, graphIndex) {
     );
   }
   for (const value of values.values())
-    requireFact(
-      Object.entries(value).every(
-        ([key, v]) => graphIndex.values.get(value.id)?.[key] === v,
-      ),
+    requireSameNativeValue(
+      value,
+      graphIndex.values.get(value.id),
       "Native call/graph value mismatch",
     );
   for (const op of operations.values())
diff --git a/experiments/atomic-codemode/native-contract.mjs b/experiments/atomic-codemode/native-contract.mjs
index 81198a6d7f..f8da20fce0 100644
--- a/experiments/atomic-codemode/native-contract.mjs
+++ b/experiments/atomic-codemode/native-contract.mjs
@@ -23,6 +23,12 @@ export const value = z.strictObject({
   definition: operationId.nullable(),
   type_name: z.string(),
 });
+export const requireSameNativeValue = (value, reference, message) =>
+  requireFact(
+    reference &&
+      Object.entries(value).every(([key, v]) => reference[key] === v),
+    message,
+  );
 export const rowParser = (schema, arrays, fields = {}) => {
   const metadata = schema.omit(
     Object.fromEntries(
diff --git a/experiments/atomic-codemode/native-engine.md b/experiments/atomic-codemode/native-engine.md
index aff2497880..3c1a33320c 100644
--- a/experiments/atomic-codemode/native-engine.md
+++ b/experiments/atomic-codemode/native-engine.md
@@ -673,5 +673,10 @@ lossless encoding probe also puts the earlier full 17.8 MB diagnostic record
 inside the unchanged 8 MiB transport. The [subsequent codec study](native-graph-transport-study.md)
 now implements and verifies this through both public experimental MCP adapters,
 including complete decoded Evidence and shared text-budget ownership. Actual
-model behavior remains to be tested. Model comparisons share the same
-computation/fact owners, avoiding a capability difference between adapters.
+guard/control model behavior is now checked in two real-model pairs. Model
+comparisons share the same computation/fact owners, avoiding a capability
+difference between adapters. The [switch extension](switch-study.md) adds an
+independent native table facet with exact labels and row/edge mapping, selected
+queries and a verified 2 MiB fallback that retains cases without a full graph.
+Its final engine is `a9ca8a8ac224936afb08a9d4be9c1225feb69473ad9f35764e8d1c4f04875b5b`;
+the fixed case/default model question is separate from the earlier guard pairs.
diff --git a/experiments/atomic-codemode/native-graph-transport-study.md b/experiments/atomic-codemode/native-graph-transport-study.md
index 3fa1ea0474..abc18b3d6d 100644
--- a/experiments/atomic-codemode/native-graph-transport-study.md
+++ b/experiments/atomic-codemode/native-graph-transport-study.md
@@ -41,6 +41,10 @@ keys the view; successful close clears it. All adapters share these owners.
 
 ## Real verification
 
+These graph-only engine/patch measurements use commit `e2205313a` and its
+version of `kuna-native-ir.patch`. The subsequent [switch extension](switch-study.md)
+has its own pinned engine/patch and retains the same logical graph fields.
+
 Kuna upstream: `fe01d6294eb0d1053ce343c8943646df88e143fc`.
 Final preserved engine:
 `677b9795d49a65e459054ecbd3c0df37d603b541d72df9f74b46778947ed3936`.
diff --git a/experiments/atomic-codemode/native-ir-contract.mjs b/experiments/atomic-codemode/native-ir-contract.mjs
index 2c4c6cc744..bf86d2a5ca 100644
--- a/experiments/atomic-codemode/native-ir-contract.mjs
+++ b/experiments/atomic-codemode/native-ir-contract.mjs
@@ -4,6 +4,7 @@ import { FactFailure } from "./fact-error.mjs";
 import { NATIVE_OUTPUT_BYTES } from "./limits.mjs";
 import { readCallFacet } from "./native-call-contract.mjs";
 import { readProjectionFacet } from "./native-projection-contract.mjs";
+import { readSwitchFacet } from "./native-switch-contract.mjs";
 import { operation, parseOperation } from "./native-operation-contract.mjs";
 import {
   decodeGraphArchive,
@@ -69,6 +70,8 @@ const documentSchema = z.object({
         atomic_facts_error: z.string().optional(),
         atomic_calls: z.unknown().optional(),
         atomic_calls_error: z.string().optional(),
+        atomic_switches: z.unknown().optional(),
+        atomic_switches_error: z.string().optional(),
         atomic_projection: z.unknown().optional(),
         atomic_projection_error: z.string().optional(),
       }),
@@ -216,6 +219,7 @@ export function parseNativeFunction(text, entry, expectedInput) {
       language: doc.language,
       facts: readGraph(fn),
       calls: readCallFacet(fn),
+      switches: readSwitchFacet(fn),
       projection: readProjectionFacet(fn),
     };
   } catch (error) {
diff --git a/experiments/atomic-codemode/native-ir.mjs b/experiments/atomic-codemode/native-ir.mjs
index 2ca673415b..e39e9f1c1c 100644
--- a/experiments/atomic-codemode/native-ir.mjs
+++ b/experiments/atomic-codemode/native-ir.mjs
@@ -1,6 +1,12 @@
 // The native-format boundary owns validation and indexes; consumers never parse
 // diagnostic statements to recover value identity, operand indexes or CFG edges.
 import { FactFailure } from "./fact-error.mjs";
+import {
+  indexSwitchFacet,
+  validateSwitchGraph,
+  validateSwitchValues,
+  createSwitchViews,
+} from "./native-switch-views.mjs";
 import { parseNativeFunction } from "./native-ir-contract.mjs";
 import { controlDependencies } from "./control-dependence.mjs";
 import { freezeFacts as freeze } from "./fact-reads.mjs";
@@ -185,6 +191,8 @@ const captureFacets = ({
   graphError,
   operationError,
   callError,
+  switches,
+  switchError,
 }) =>
   freeze({
     code: { availability: "available" },
@@ -213,6 +221,9 @@ const captureFacets = ({
     calls: calls
       ? { availability: "available", ...calls.summary }
       : { availability: "unavailable", error: callError },
+    switches: switches
+      ? { availability: "available", ...switches.summary }
+      : { availability: "unavailable", error: switchError },
     values: graph
       ? {
           availability: "available",
@@ -270,6 +281,7 @@ export function parseNativeIR(text, entry, expectedInput) {
         // Without a full graph, the independent call owner validates the projection.
         if (calls.view) validateCallGraph(calls.index, index);
         return {
+          index,
           view: createProjectionViews(
             facts,
             capture.code,
@@ -279,6 +291,16 @@ export function parseNativeIR(text, entry, expectedInput) {
         };
       });
   const unavailableCalls = unavailable("calls", calls.error);
+  const switches = loadFacet(capture.switches, (facts) => {
+    const index = indexSwitchFacet(facts);
+    if (graph.view) validateSwitchGraph(index, graph.index);
+    else {
+      validateSwitchValues(index, calls.index?.values);
+      validateSwitchValues(index, projection.index?.values);
+    }
+    return { view: createSwitchViews(facts, index) };
+  });
+  const unavailableSwitches = unavailable("switches", switches.error);
   const operationError = operationFailure(projection.error, graph.error);
   const unavailableOperations = unavailable("operations", operationError);
   const fallback = {
@@ -307,8 +329,13 @@ export function parseNativeIR(text, entry, expectedInput) {
   };
   return Object.freeze({
     ...(graph.view ?? projection.view ?? fallback),
+    edges: (input) =>
+      input.kind === "cases"
+        ? (switches.view?.cases ?? unavailableSwitches)(input)
+        : (graph.view ?? projection.view ?? fallback).edges(input),
     language: capture.language,
     calls: calls.view?.calls ?? unavailableCalls,
+    switches: switches.view?.switches ?? unavailableSwitches,
     values:
       graph.view?.values ??
       projection.view?.values ??
@@ -321,6 +348,8 @@ export function parseNativeIR(text, entry, expectedInput) {
       graphError: graph.error,
       operationError,
       callError: calls.error,
+      switches: switches.view,
+      switchError: switches.error,
     }),
   });
 }
diff --git a/experiments/atomic-codemode/native-switch-contract.mjs b/experiments/atomic-codemode/native-switch-contract.mjs
new file mode 100644
index 0000000000..eca4eaca23
--- /dev/null
+++ b/experiments/atomic-codemode/native-switch-contract.mjs
@@ -0,0 +1,104 @@
+// Native switch framing/rows are admitted independently of graph and calls.
+import { z } from "zod";
+import {
+  hex,
+  ordinal,
+  edgeId,
+  operationId,
+  value,
+  rowParser,
+  readNativeFacet,
+  requireFact,
+} from "./native-contract.mjs";
+
+const edge = z.strictObject({ id: edgeId, index: ordinal, target: ordinal });
+const location = z.strictObject({ space: z.string(), offset: hex });
+const row = z.strictObject({
+  index: ordinal,
+  label: z
+    .strictObject({ status: z.enum(["value", "no-label"]), raw_bits: hex })
+    .nullable(),
+  recovered_target: location.nullable(),
+  edges: z.array(edge),
+});
+const table = z.strictObject({
+  partial: z.boolean(),
+  labelled: z.boolean(),
+  consumed_mask: hex,
+  signed_render_hint: z.boolean(),
+  default_raw_index: z.number().int().min(-1).max(0x7fffffff),
+  default_edge: edge.nullable(),
+  default_is_folded: z.boolean(),
+  rows: z.array(row),
+});
+const item = z.strictObject({
+  id: operationId,
+  origin_address: hex,
+  block: ordinal,
+  selector: value.nullable(),
+  table: table.nullable(),
+});
+const facet = z.strictObject({
+  schema_version: z.literal(1),
+  items: z.array(item).max(12000),
+  coverage: z.strictObject({
+    scope: z.string(),
+    blocks_examined: ordinal.min(1),
+    operations_examined: z
+      .number()
+      .int()
+      .nonnegative()
+      .max(Number.MAX_SAFE_INTEGER),
+    machine_semantic_equivalence: z.literal("unknown"),
+  }),
+});
+const parseTable = rowParser(table, {
+  rows: rowParser(row, { edges: (v) => edge.parse(v) }),
+});
+const parseItem = rowParser(
+  item,
+  {},
+  { table: (v) => (v === null ? null : parseTable(v)) },
+);
+const parseFacet = rowParser(facet, { items: parseItem });
+
+export const readSwitchFacet = (fn) =>
+  readNativeFacet(fn, "atomic_switches", "recovered switches", (raw) => {
+    requireFact(
+      raw?.schema_version === 1,
+      "Unsupported native switch facet schema; expected 1",
+    );
+    requireFact(
+      Array.isArray(raw.items) && raw.items.length <= 12000,
+      "Native switch count exceeds capacity or has invalid shape",
+    );
+    let rows = 0,
+      mappings = 0,
+      text = 0;
+    for (const item of raw.items) {
+      for (const s of [item?.selector?.space, item?.selector?.type_name])
+        if (typeof s === "string") text += Buffer.byteLength(s);
+      if (item?.table === null) continue;
+      requireFact(
+        Array.isArray(item?.table?.rows),
+        "Native switch rows must be an array",
+      );
+      rows += item.table.rows.length;
+      requireFact(rows <= 100000, "Native switch rows exceed capacity");
+      for (const row of item.table.rows) {
+        requireFact(
+          Array.isArray(row?.edges),
+          "Native case edges must be an array",
+        );
+        mappings += row.edges.length;
+        requireFact(
+          mappings <= 100000,
+          "Native switch mappings exceed capacity",
+        );
+        if (typeof row?.recovered_target?.space === "string")
+          text += Buffer.byteLength(row.recovered_target.space);
+      }
+    }
+    requireFact(text <= 2 * 1024 * 1024, "Native switch text exceeds capacity");
+    return parseFacet(raw);
+  });
diff --git a/experiments/atomic-codemode/native-switch-views.mjs b/experiments/atomic-codemode/native-switch-views.mjs
new file mode 100644
index 0000000000..50d6f00064
--- /dev/null
+++ b/experiments/atomic-codemode/native-switch-views.mjs
@@ -0,0 +1,320 @@
+// Native table ownership is separate from optimized CFG and machine transfers.
+import { requireFact, requireSameNativeValue } from "./native-contract.mjs";
+import { uniqueNative, readNativeIdentities } from "./native-reads.mjs";
+import { freezeFacts } from "./fact-reads.mjs";
+
+function validateEdge(edge, block) {
+  requireFact(
+    edge.id === `${block}:${edge.index}`,
+    "Native switch edge identity mismatch",
+  );
+}
+function indexTable(sw) {
+  const { rows, ...metadata } = sw.table;
+  requireFact(
+    (metadata.default_raw_index === -1) === (metadata.default_edge === null),
+    "Native switch default availability mismatch",
+  );
+  if (metadata.default_edge) {
+    validateEdge(metadata.default_edge, sw.block);
+    requireFact(
+      metadata.default_edge.index === metadata.default_raw_index,
+      "Native switch default index mismatch",
+    );
+  }
+  const counts = {
+    case_count: rows.length,
+    mapping_count: 0,
+    known_label_count: 0,
+    missing_label_count: 0,
+    no_label_count: 0,
+    unmapped_row_count: 0,
+    unknown_target_count: 0,
+  };
+  const byLabel = new Map();
+  for (const [i, row] of rows.entries()) {
+    requireFact(row.index === i, "Native case row ordinal mismatch");
+    const edges = new Set();
+    for (const edge of row.edges) {
+      validateEdge(edge, sw.block);
+      requireFact(
+        !edges.has(edge.id),
+        "Duplicate native case/out-edge binding",
+      );
+      edges.add(edge.id);
+    }
+    if (row.label === null) counts.missing_label_count++;
+    else if (row.label.status === "no-label") counts.no_label_count++;
+    else {
+      counts.known_label_count++;
+      if (!byLabel.has(row.label.raw_bits)) byLabel.set(row.label.raw_bits, []);
+      byLabel.get(row.label.raw_bits).push(row);
+    }
+    counts.mapping_count += row.edges.length;
+    if (row.edges.length === 0) counts.unmapped_row_count++;
+    if (row.recovered_target === null) counts.unknown_target_count++;
+  }
+  const hasRawLabels = counts.missing_label_count < rows.length;
+  requireFact(
+    metadata.labelled === hasRawLabels,
+    "Native switch label availability mismatch",
+  );
+  const prefix = caseOffsets(rows);
+  const table = { ...metadata, ...counts, relation_count: prefix.at(-1) };
+  // Retain source rows and label references, not a second full row projection.
+  // A numeric row lookup is O(1); selected label reads use this index.
+  return { table, lookup: { rows, prefix, byLabel, labelOffsets: new Map() } };
+}
+
+export function indexSwitchFacet(facts) {
+  freezeFacts(facts);
+  const switches = uniqueNative(facts.items),
+    summaries = new Map(),
+    cases = new Map();
+  requireFact(
+    switches.size <= facts.coverage.operations_examined,
+    "Native switch count exceeds examined operations",
+  );
+  for (const sw of switches.values()) {
+    requireFact(
+      sw.id.split(":")[0] === sw.origin_address,
+      "Native switch origin/identity mismatch",
+    );
+    let table = null;
+    if (sw.table) {
+      const indexed = indexTable(sw);
+      table = indexed.table;
+      cases.set(sw.id, indexed.lookup);
+    }
+    summaries.set(
+      sw.id,
+      freezeFacts({
+        id: sw.id,
+        origin_address: sw.origin_address,
+        block: sw.block,
+        selector: sw.selector,
+        table,
+      }),
+    );
+  }
+  return { switches, summaries, cases };
+}
+export function validateSwitchGraph(index, graph) {
+  for (const sw of index.switches.values()) {
+    const op = graph.operations.get(sw.id),
+      block = graph.blocks.get(sw.block);
+    requireFact(
+      op?.opcode === "CPUI_BRANCHIND" &&
+        op.block === sw.block &&
+        op.address === sw.origin_address &&
+        block,
+      "Native switch/graph ownership mismatch",
+    );
+    requireFact(
+      (op.inputs[0]?.value_id ?? null) === (sw.selector?.id ?? null),
+      "Native switch/graph selector mismatch",
+    );
+    if (sw.selector)
+      requireSameNativeValue(
+        sw.selector,
+        graph.values.get(sw.selector.id),
+        "Native switch/graph selector value mismatch",
+      );
+    const checkEdge = (edge) =>
+      requireFact(
+        block.successors[edge.index]?.id === edge.id &&
+          block.successors[edge.index]?.target === edge.target,
+        "Native switch/graph edge mapping mismatch",
+      );
+    if (sw.table?.default_edge) checkEdge(sw.table.default_edge);
+    for (const row of sw.table?.rows ?? [])
+      for (const edge of row.edges) checkEdge(edge);
+  }
+  for (const op of graph.operations.values())
+    requireFact(
+      op.opcode !== "CPUI_BRANCHIND" || index.switches.has(op.id),
+      "Native indirect branch omitted from switch coverage",
+    );
+}
+export function validateSwitchValues(index, values) {
+  if (!values) return;
+  for (const sw of index.switches.values())
+    if (sw.selector && values.has(sw.selector.id))
+      requireSameNativeValue(
+        sw.selector,
+        values.get(sw.selector.id),
+        "Native switch/shared value mismatch",
+      );
+}
+function caseOffsets(rows) {
+  const prefix = new Uint32Array(rows.length + 1);
+  for (let i = 0; i < rows.length; i++)
+    prefix[i + 1] = prefix[i] + Math.max(1, rows[i].edges.length);
+  return prefix;
+}
+function selectCaseRows(lookup, labels, indices) {
+  if (!labels && !indices) return lookup;
+  if (!indices && labels?.size === 1) {
+    const label = labels.values().next().value;
+    const rows = lookup.byLabel.get(label) ?? [];
+    if (!lookup.labelOffsets.has(label) && lookup.byLabel.has(label))
+      lookup.labelOffsets.set(label, caseOffsets(rows));
+    return {
+      rows,
+      prefix: lookup.labelOffsets.get(label) ?? new Uint32Array(1),
+    };
+  }
+  const rows = indices
+    ? indices
+        .flatMap((i) => lookup.rows[i] ?? [])
+        .filter(
+          (r) =>
+            !labels ||
+            (r.label?.status === "value" && labels.has(r.label.raw_bits)),
+        )
+    : [...labels]
+        .flatMap((label) => lookup.byLabel.get(label) ?? [])
+        .sort((a, b) => a.index - b.index);
+  return { rows, prefix: caseOffsets(rows) };
+}
+function firstCaseAt(prefix, offset) {
+  let low = 0,
+    high = prefix.length - 1;
+  while (low < high) {
+    const mid = (low + high) >>> 1;
+    if (prefix[mid + 1] <= offset) low = mid + 1;
+    else high = mid;
+  }
+  return low;
+}
+function casePage(sw, selected, start, end) {
+  const { id, block } = sw;
+  const items = [];
+  for (
+    let i = firstCaseAt(selected.prefix, start);
+    i < selected.rows.length && selected.prefix[i] < end;
+    i++
+  ) {
+    const r = selected.rows[i],
+      case_id = `${id}:case:${r.index}`;
+    const begin = Math.max(0, start - selected.prefix[i]);
+    const finish = Math.min(
+      Math.max(1, r.edges.length),
+      end - selected.prefix[i],
+    );
+    for (let j = begin; j < finish; j++) {
+      const edge = r.edges[j] ?? null;
+      items.push({
+        id: `${case_id}:edge:${edge?.index ?? "unknown"}`,
+        case_id,
+        switch: id,
+        block,
+        case_index: r.index,
+        label: r.label,
+        recovered_target: r.recovered_target,
+        edge,
+      });
+    }
+  }
+  return items;
+}
+function selectedCaseCoverage(seeds, summaries) {
+  return seeds.flatMap((id) => {
+    const sw = summaries.get(id),
+      t = sw?.table;
+    return sw
+      ? [
+          {
+            id,
+            table_available: t !== null,
+            partial: t?.partial ?? null,
+            case_count: t?.case_count ?? null,
+            relation_count: t?.relation_count ?? null,
+            mapping_count: t?.mapping_count ?? null,
+            known_label_count: t?.known_label_count ?? null,
+            missing_label_count: t?.missing_label_count ?? null,
+            no_label_count: t?.no_label_count ?? null,
+            unmapped_row_count: t?.unmapped_row_count ?? null,
+          },
+        ]
+      : [];
+  });
+}
+function readCases(index, coverage, input) {
+  const seeds = [...new Set(input.seeds)],
+    labels = input.case_values && new Set(input.case_values),
+    indices =
+      input.case_indices &&
+      [...new Set(input.case_indices)].sort((a, b) => a - b),
+    offset = input.offset ?? 0,
+    limit = input.limit ?? 20,
+    items = [];
+  let total = 0;
+  for (const id of seeds) {
+    const lookup = index.cases.get(id);
+    if (!lookup) continue;
+    const selected = selectCaseRows(lookup, labels, indices),
+      count = selected.prefix.at(-1);
+    const start = Math.max(0, offset - total),
+      end = Math.min(count, offset + limit - total);
+    if (start < end)
+      items.push(...casePage(index.summaries.get(id), selected, start, end));
+    total += count;
+  }
+  return {
+    items,
+    total,
+    next_offset: offset + limit < total ? offset + limit : null,
+    unretained_seeds: seeds.filter((id) => !index.switches.has(id)),
+    coverage,
+    relation_coverage: {
+      scope:
+        "one relation per captured case/out-edge; an unmapped case has one explicit unknown-edge row; not all feasible runtime cases",
+      switches: selectedCaseCoverage(seeds, index.summaries),
+    },
+  };
+}
+
+export function createSwitchViews(facts, index) {
+  const coverage = freezeFacts({
+    ...facts.coverage,
+    case_identity:
+      "snapshot + switch operation + native address-table row index",
+    relation_identity:
+      "case_id + native out-edge index, or one explicit unknown-edge row",
+    label_authority:
+      "native recovered label and explicit reserved-no-label status; row/edge indexes are not label values",
+    selector_authority:
+      "native current BRANCHIND input; may be a normalized selector rather than a machine jump address",
+    target_authority:
+      "native address-table target and separate recovered out-edge mapping; optimized block origins may differ",
+    default_authority:
+      "native model default out-edge, not necessarily a machine out-of-range guard destination",
+    signedness: "signed_render_hint is only a native rendering hint",
+    runtime_feasibility: "unknown",
+    memory_alias_dependencies: "unknown",
+  });
+  const tables = [...index.summaries.values()].map((s) => s.table);
+  const summary = freezeFacts({
+    count: index.switches.size,
+    table_count: tables.filter(Boolean).length,
+    partial_table_count: tables.filter((t) => t?.partial).length,
+    case_count: tables.reduce((n, t) => n + (t?.case_count ?? 0), 0),
+    relation_count: tables.reduce((n, t) => n + (t?.relation_count ?? 0), 0),
+    coverage,
+  });
+  return {
+    summary,
+    switches: (input) => ({
+      ...readNativeIdentities(
+        index.summaries,
+        input,
+        (sw) =>
+          !input.origin_addresses ||
+          input.origin_addresses.includes(sw.origin_address),
+      ),
+      coverage,
+    }),
+    cases: (input) => readCases(index, coverage, input),
+  };
+}
diff --git a/experiments/atomic-codemode/native-switches.test.mjs b/experiments/atomic-codemode/native-switches.test.mjs
new file mode 100644
index 0000000000..c633bf9ee6
--- /dev/null
+++ b/experiments/atomic-codemode/native-switches.test.mjs
@@ -0,0 +1,351 @@
+import assert from "node:assert/strict";
+import test from "node:test";
+import { parseNativeIR } from "./native-ir.mjs";
+
+const switchID = "0x1000:1";
+const edge = (index, target) => ({ id: `0:${index}`, index, target });
+function tableFixture() {
+  return {
+    partial: true,
+    labelled: true,
+    consumed_mask: "0xff",
+    signed_render_hint: true,
+    default_raw_index: 1,
+    default_edge: edge(1, 2),
+    default_is_folded: true,
+    rows: [
+      {
+        index: 0,
+        label: { status: "value", raw_bits: "0x42" },
+        recovered_target: { space: "ram", offset: "0xabc" },
+        edges: [edge(0, 1)],
+      },
+      {
+        index: 1,
+        label: { status: "value", raw_bits: "0x7" },
+        recovered_target: { space: "ram", offset: "0xdef" },
+        edges: [edge(0, 1)],
+      },
+      {
+        index: 2,
+        label: { status: "no-label", raw_bits: "0xbad1abe1bad1abe1" },
+        recovered_target: { space: "ram", offset: "0xf00" },
+        edges: [edge(1, 2)],
+      },
+      { index: 3, label: null, recovered_target: null, edges: [] },
+    ],
+  };
+}
+function graphFixture(selector) {
+  const operation = (address, block, opcode, inputs = []) => ({
+    id: `${address}:1`,
+    address,
+    block,
+    opcode,
+    inputs,
+    output: null,
+    statement: "uninterpreted display",
+    is_dead: false,
+  });
+  return {
+    schema_version: 3,
+    blocks: [
+      {
+        id: 0,
+        start: "0x1000",
+        operations: [switchID],
+        predecessors: [],
+        successors: [edge(0, 1), edge(1, 2)].map((e) => ({
+          ...e,
+          polarity: null,
+          condition_value: null,
+          condition_test: null,
+        })),
+      },
+      {
+        id: 1,
+        start: "0x1010",
+        operations: ["0x1010:1"],
+        predecessors: [0],
+        successors: [],
+      },
+      {
+        id: 2,
+        start: "0x1020",
+        operations: ["0x1020:1"],
+        predecessors: [0],
+        successors: [],
+      },
+    ],
+    operations: [
+      operation("0x1000", 0, "CPUI_BRANCHIND", [
+        {
+          input_index: 0,
+          value_id: "v1",
+          phi_predecessor: null,
+          phi_predecessor_edge: null,
+        },
+      ]),
+      operation("0x1010", 1, "CPUI_RETURN"),
+      operation("0x1020", 2, "CPUI_RETURN"),
+    ],
+    values: [{ ...selector }],
+    coverage: {
+      scope: "fixture recovered graph",
+      machine_semantic_equivalence: "unknown",
+      indirect_branch_operations: [switchID],
+      omitted_definition_ids: [],
+      issues: [],
+    },
+  };
+}
+function fixture() {
+  const selector = {
+    id: "v1",
+    space: "register",
+    offset: "0x10",
+    size_bytes: 8,
+    is_constant: false,
+    is_input: true,
+    is_annotation: false,
+    definition: null,
+    type_name: "uint64",
+  };
+  return {
+    binary: "/input",
+    count: 1,
+    language: "c",
+    error: null,
+    functions: [
+      {
+        address_hex: "0x1000",
+        code: "retained C",
+        error: null,
+        atomic_facts: graphFixture(selector),
+        atomic_switches: {
+          schema_version: 1,
+          items: [
+            {
+              id: switchID,
+              origin_address: "0x1000",
+              block: 0,
+              selector,
+              table: tableFixture(),
+            },
+          ],
+          coverage: {
+            scope: "captured native tables",
+            blocks_examined: 3,
+            operations_examined: 3,
+            machine_semantic_equivalence: "unknown",
+          },
+        },
+      },
+    ],
+  };
+}
+const load = (doc) => parseNativeIR(JSON.stringify(doc), "0x1000");
+const cases = (model, extra = {}) =>
+  model.edges({ kind: "cases", seeds: [switchID], ...extra });
+
+test("case-to-edge paging bounds a single case with several mappings and keeps a stable case identity", () => {
+  const doc = fixture();
+  doc.functions[0].atomic_switches.items[0].table.rows[0].edges.push(
+    edge(1, 2),
+  );
+  const model = load(doc),
+    first = cases(model, { case_values: ["0x42"], limit: 1 }),
+    second = cases(model, { case_values: ["0x42"], offset: 1, limit: 1 });
+  assert.equal(model.switches({}).items[0].table.case_count, 4);
+  assert.equal(model.switches({}).items[0].table.relation_count, 5);
+  assert.equal(first.total, 2);
+  assert.equal(first.items.length, 1);
+  assert.equal(first.next_offset, 1);
+  assert.equal(first.items[0].case_id, second.items[0].case_id);
+  assert.notEqual(first.items[0].id, second.items[0].id);
+  assert.equal(first.items[0].edge.index, 0);
+  assert.equal(second.items[0].edge.index, 1);
+  assert.equal(second.next_offset, null);
+});
+
+test("a late two-edge page does not materialize thousands of unrequested mappings", () => {
+  const doc = fixture(),
+    fn = doc.functions[0];
+  delete fn.atomic_facts;
+  const table = fn.atomic_switches.items[0].table;
+  table.rows = table.rows.slice(0, 1);
+  table.rows[0].edges = Array.from({ length: 4096 }, (_, i) => edge(i, i + 1));
+  fn.atomic_switches.coverage.blocks_examined = 4097;
+  fn.atomic_switches.coverage.operations_examined = 4097;
+  const model = load(doc);
+  const page = cases(model, { case_values: ["0x42"], offset: 4090, limit: 2 });
+  assert.equal(page.total, 4096);
+  assert.equal(page.next_offset, 4092);
+  assert.deepEqual(
+    page.items.map((r) => r.edge.index),
+    [4090, 4091],
+  );
+  assert.equal(page.items[0].case_id, page.items[1].case_id);
+  assert.ok(Buffer.byteLength(JSON.stringify(page.items)) < 1024);
+});
+
+test("case ordinals, labels, original targets and optimized edges remain distinct and paged", () => {
+  const model = load(fixture());
+  assert.equal(model.facets.switches.availability, "available");
+  const sw = model.switches({ fields: ["table"] }).items[0];
+  assert.equal(sw.selector, undefined);
+  assert.equal(sw.table.case_count, 4);
+  assert.equal(sw.table.known_label_count, 2);
+  assert.equal(sw.table.missing_label_count, 1);
+  assert.equal(sw.table.no_label_count, 1);
+  assert.equal(sw.table.unmapped_row_count, 1);
+  assert.equal(sw.table.default_edge.id, "0:1");
+  const page = cases(model, {
+    seeds: [switchID, switchID, "unknown"],
+    case_values: ["0x7", "0x42", "0xbad1abe1bad1abe1"],
+    limit: 1,
+  });
+  assert.equal(page.total, 2);
+  assert.equal(page.next_offset, 1);
+  assert.deepEqual(page.unretained_seeds, ["unknown"]);
+  assert.equal(page.items[0].case_index, 0);
+  assert.equal(page.items[0].label.raw_bits, "0x42");
+  assert.equal(page.items[0].recovered_target.offset, "0xabc");
+  assert.equal(page.items[0].edge.target, 1);
+  assert.throws(() => {
+    page.items[0].edge.target = 2;
+  }, TypeError);
+  assert.equal(cases(model, { case_indices: [0] }).items[0].edge.target, 1);
+  assert.equal(model.block(1).origin_start, "0x1010");
+  const second = cases(model, {
+    case_values: ["0x42", "0x7"],
+    offset: 1,
+    limit: 1,
+  });
+  assert.equal(second.items[0].case_index, 1);
+  assert.equal(second.next_offset, null);
+  assert.deepEqual(
+    cases(model, { case_indices: [2, 0, 1], case_values: ["0x7"] }).items.map(
+      (r) => r.case_index,
+    ),
+    [1],
+  );
+  assert.equal(cases(model, { case_values: [] }).total, 0);
+});
+test("unlabelled/unmapped and partial or unavailable tables do not become absent runtime cases", () => {
+  const doc = fixture(),
+    model = load(doc);
+  assert.equal(cases(model, { case_values: ["0xbad1abe1bad1abe1"] }).total, 0);
+  const source = cases(model, { case_indices: [2, 3] });
+  assert.equal(source.items[0].label.status, "no-label");
+  assert.equal(source.items[1].label, null);
+  assert.deepEqual(source.items[1].edge, null);
+  assert.equal(source.relation_coverage.switches[0].partial, true);
+  assert.equal(source.coverage.runtime_feasibility, "unknown");
+  doc.functions[0].atomic_switches.items[0].table = null;
+  const unknown = cases(load(doc));
+  assert.equal(unknown.relation_coverage.switches[0].table_available, false);
+  assert.equal(unknown.relation_coverage.switches[0].case_count, null);
+});
+test("switch rows survive graph failure and missing old-engine capture remains unavailable", () => {
+  const doc = fixture();
+  delete doc.functions[0].atomic_facts;
+  doc.functions[0].atomic_facts_error = "graph capacity";
+  const model = load(doc);
+  assert.equal(model.facets.recovered_ir.availability, "unavailable");
+  assert.equal(model.switches({}).items[0].selector.size_bytes, 8);
+  assert.equal(cases(model).total, 4);
+  delete doc.functions[0].atomic_switches;
+  const legacy = load(doc);
+  assert.equal(legacy.facets.switches.availability, "unavailable");
+  assert.throws(() => cases(legacy));
+  assert.equal(legacy.code, "retained C");
+  doc.functions[0].atomic_switches = {
+    schema_version: 1,
+    items: [],
+    coverage: {
+      scope: "all recovered switches",
+      blocks_examined: 3,
+      operations_examined: 3,
+      machine_semantic_equivalence: "unknown",
+    },
+  };
+  const empty = load(doc);
+  assert.equal(empty.facets.switches.availability, "available");
+  assert.equal(empty.facets.switches.count, 0);
+});
+test("contradictory switch ownership or values fail only that independent facet", () => {
+  for (const change of [
+    (sw) => (sw.table.rows[0].edges[0].target = 2),
+    (sw) => (sw.table.rows[0].index = 1),
+    (sw) => (sw.selector.size_bytes = 4),
+    (sw) => (sw.table.default_raw_index = 0),
+    (sw) => sw.table.rows[0].edges.push(edge(0, 1)),
+  ]) {
+    const doc = fixture();
+    change(doc.functions[0].atomic_switches.items[0]);
+    const model = load(doc);
+    assert.equal(model.facets.switches.availability, "unavailable");
+    assert.equal(model.facets.recovered_ir.availability, "available");
+    assert.equal(model.code, "retained C");
+  }
+});
+test("partial facets cannot disagree about a shared value identity when the graph is unavailable", () => {
+  const doc = fixture(),
+    fn = doc.functions[0];
+  delete fn.atomic_facts;
+  fn.atomic_calls = {
+    schema_version: 1,
+    items: [
+      {
+        id: "0x1100:0",
+        origin_address: "0x1100",
+        block: 0,
+        opcode: "CPUI_CALL",
+        is_dead: false,
+        target_value_id: null,
+        spec_available: false,
+        target: null,
+        target_name: null,
+        arguments: [
+          {
+            input_index: 1,
+            value_id: "v1",
+            storage: null,
+            storage_authority: null,
+          },
+        ],
+        output: null,
+        prototype: null,
+        stack_offset: null,
+      },
+    ],
+    values: [{ ...fn.atomic_switches.items[0].selector }],
+    coverage: {
+      scope: "all recovered calls",
+      blocks_examined: 3,
+      operations_examined: 3,
+      value_scope: "call inputs and outputs",
+      machine_call_equivalence: "unknown",
+    },
+  };
+  assert.equal(load(doc).facets.switches.availability, "available");
+  fn.atomic_switches.items[0].selector.size_bytes = 4;
+  const invalid = load(doc);
+  assert.equal(invalid.facets.switches.availability, "unavailable");
+  assert.equal(invalid.facets.calls.availability, "available");
+  assert.equal(invalid.calls({}).total, 1);
+});
+test("switch capacity rejection precedes row validation and preserves the valid graph", () => {
+  for (const oversized of [
+    (table) => (table.rows = Array(100001).fill({})),
+    (table) => (table.rows[0].edges = Array(100001).fill({})),
+  ]) {
+    const doc = fixture();
+    oversized(doc.functions[0].atomic_switches.items[0].table);
+    const model = load(doc);
+    assert.equal(model.facets.switches.availability, "unavailable");
+    assert.match(model.facets.switches.error.message, /capacity/);
+    assert.equal(model.facets.recovered_ir.availability, "available");
+  }
+});
diff --git a/experiments/atomic-codemode/profile-native.mjs b/experiments/atomic-codemode/profile-native.mjs
index 902ef9d209..ce876d3688 100644
--- a/experiments/atomic-codemode/profile-native.mjs
+++ b/experiments/atomic-codemode/profile-native.mjs
@@ -11,6 +11,7 @@ import { PrivateRuntimeRoot } from "../../dist/process/PrivateRuntimeRoot.js";
 import { spawnOwnedProviderProcess } from "../../dist/process/ProviderProcess.js";
 import { requireResult } from "./fact-error.mjs";
 import { parseNativeIR } from "./native-ir.mjs";
+import { NATIVE_OUTPUT_BYTES } from "./limits.mjs";
 import {
   createVerifierRun,
   completeVerifierRun,
@@ -19,11 +20,21 @@ import {
 
 const { values: options, positionals } = parseArgs({
   allowPositionals: true,
-  options: { "without-timing": { type: "boolean", default: false } },
+  options: {
+    "without-timing": { type: "boolean", default: false },
+    "output-bytes": { type: "string", default: String(NATIVE_OUTPUT_BYTES) },
+  },
 });
 const [engine, binary, entry, output, goldenPath] = positionals;
 const timingEnabled = !options["without-timing"];
 assert.ok(engine && binary && entry && output);
+const outputBytes = Number(options["output-bytes"]);
+assert.ok(
+  Number.isSafeInteger(outputBytes) &&
+    outputBytes > 0 &&
+    outputBytes <= NATIVE_OUTPUT_BYTES,
+  "Choose a positive native output budget within the supervisor's 8 MiB capture capacity",
+);
 const sha = (s) => createHash("sha256").update(s).digest("hex");
 const expectedPhases = [
   "decompile_drive",
@@ -79,11 +90,11 @@ try {
           "--json",
           "--atomic-facts",
           "--atomic-output-bytes",
-          "8388608",
+          String(outputBytes),
           "--max-fn-memory",
           "1024",
         ],
-        outputBytes: 8 * 1024 * 1024,
+        outputBytes: NATIVE_OUTPUT_BYTES,
         timeoutMs: 120000,
         signal: new AbortController().signal,
       }),
@@ -193,6 +204,8 @@ await writeFile(
       target: target && { path: target.path, sha256: target.sha256 },
       entry,
       timing_enabled: timingEnabled,
+      output_budget_bytes: outputBytes,
+      supervisor_capture_budget_bytes: NATIVE_OUTPUT_BYTES,
       runs,
       failures,
       lifecycle,
diff --git a/experiments/atomic-codemode/provider.mjs b/experiments/atomic-codemode/provider.mjs
index 3e63be60d0..814d5f19a9 100644
--- a/experiments/atomic-codemode/provider.mjs
+++ b/experiments/atomic-codemode/provider.mjs
@@ -381,11 +381,11 @@ export class KunaFactOwner {
     }));
   }
   async relations(input) {
-    if (["controllers", "operands"].includes(input.kind))
+    if (["controllers", "operands", "cases"].includes(input.kind))
       this.#requireNativeIR(input.snapshot);
     return this.#query(input, (model) => ({
-      ...model.edges(input),
       coverage: model.coverage,
+      ...model.edges(input),
     }));
   }
   async slice(input) {
@@ -428,6 +428,10 @@ export class KunaFactOwner {
     this.#requireNativeIR(input.snapshot);
     return this.#query(input, (model) => model.calls(input));
   }
+  async switches(input) {
+    this.#requireNativeIR(input.snapshot);
+    return this.#query(input, (model) => model.switches(input));
+  }
   async blocks(input) {
     this.#requireNativeIR(input.snapshot);
     return this.#query(input, (model) => ({
diff --git a/experiments/atomic-codemode/reference.mjs b/experiments/atomic-codemode/reference.mjs
index 99d6d07037..2dcdd253c3 100644
--- a/experiments/atomic-codemode/reference.mjs
+++ b/experiments/atomic-codemode/reference.mjs
@@ -10,6 +10,8 @@ export const referenceInput = z.strictObject({
 
 // Compact return contracts let code compose before first observing a response.
 const returns = {
+  switches:
+    "data:{items:[{id,origin_address,block,selector:{native value fields}|null,table:{partial,labelled,consumed_mask,signed_render_hint,default_raw_index,default_edge:{id,index,target}|null,default_is_folded,case_count,mapping_count,relation_count,known_label_count,missing_label_count,no_label_count,unmapped_row_count,unknown_target_count}|null}],total,next_offset,missing,evidence_id,coverage}. No case inventory is embedded. selector is the native current BRANCHIND input and can be normalized; default_raw_index=-1/default_edge:null means undefined, not proof of no default. signed_render_hint does not establish general signedness. default_edge is the native model default, not necessarily the machine out-of-range guard destination. relations kind:cases reads selected original rows and mappings, even without a full graph if the independent switch facet exists.",
   bytes:
     "data:{results:[{ok,address,source:{evidence_id,sha256},hex,returned_bytes,end_address,coverage:{status,requested_bytes,provider_truncated,notes,original_file_mapping,runtime_memory}}|{ok:false,address,error}]}; ranges are [address,end_address). Completeness concerns requested bytes, not the provider truncation flag or adjacent bytes. Complete native hexdump and metadata remain in Evidence.",
   functions:
@@ -25,7 +27,7 @@ const returns = {
   operations:
     "data:{items:[{id,origin_address,block,is_dead,kind,opcode,output,input_count,definition_count,constant_count}],total,next_offset,evidence_id,coverage}. Native defaults are compact summaries; fields optionally selects statement,inputs,definitions,constants or summary columns; identity/is_dead stay. Native inputs:[{input_index,value_id,phi_predecessor,phi_predecessor_edge}], output:value_id|null; constants:[{value_id,input_index,value,printed_size_bytes,is_annotation}] retain exact u64 offsets, not arbitrary-width computed values; definitions:[{definition,use,input_index,value_id,phi_predecessor,phi_predecessor_edge}]. Page large input lists with relations kind:operands. Diagnostic rows retain legacy printed statements/occurrences and omit unavailable native counts. Projection scope is partial, with unknown CFG and definition frontier coverage.",
   relations:
-    "data:{items:operands{operation,input_index,value_id,definition,phi_predecessor,phi_predecessor_edge} OR definition/use edges OR CFG edges{from,to,operation,polarity?,condition_value?,condition_test?} OR controllers{controller,dependent,edge},total,next_offset,evidence_id,coverage,relation_coverage?,unretained_seeds?}. operands/definitions/uses seeds are operation-ID strings; CFG/controller seeds are numeric block IDs. operands accepts optional input_indices; deduplicates seeds/indices in caller order, otherwise keeps native slot order. All selected slots include constants/function inputs/nulls; values provides their metadata. For retained seeds, a requested out-of-range slot is absent; unretained seeds remain unknown. total is the filtered relation count before paging. Native def/use edges retain exact input/value/phi bindings; diagnostic edges include printed occurrence only.",
+    "data:{items:operands{operation,input_index,value_id,definition,phi_predecessor,phi_predecessor_edge} OR definition/use edges OR CFG edges{from,to,operation,polarity?,condition_value?,condition_test?} OR controllers{controller,dependent,edge} OR cases{id,case_id,switch,block,case_index,label:{status:value|no-label,raw_bits}|null,recovered_target:{space,offset}|null,edge:{id,index,target}|null},total,next_offset,evidence_id,coverage,relation_coverage?,unretained_seeds?}. Cases page individual case/out-edge relations; unmapped cases contribute one unknown-edge row. case_id stays the same across multiple edges and total counts relations, not native table rows. Cases use switch operation-ID seeds; case_values selects native labels tagged value, case_indices selects original row ordinals. Filters intersect; seeds are deduplicated in caller order and rows keep native table order. Missing/no-label/unmapped and partial/unavailable tables stay explicit in relation_coverage, not proof of absent runtime cases. operands/definitions/uses seeds are operation-ID strings; CFG/controller seeds are numeric block IDs. operands accepts optional input_indices; deduplicates seeds/indices in caller order, otherwise keeps native slot order. All selected slots include constants/function inputs/nulls; values provides their metadata. For retained seeds, a requested out-of-range slot is absent; unretained seeds remain unknown. total is the filtered relation count before paging. Native def/use edges retain exact input/value/phi bindings; diagnostic edges include printed occurrence only.",
   values:
     "data:{items:[{id,space,offset,size_bytes,is_constant,is_input,is_annotation,definition,type_name}],total,next_offset,evidence_id,coverage}; definitions are operation IDs, offsets are exact hex strings. When the graph is unavailable, values may come from a bounded definition projection or only the call boundary; coverage states that scope and operations/definitions may be unreadable.",
   calls:
diff --git a/experiments/atomic-codemode/reference.test.mjs b/experiments/atomic-codemode/reference.test.mjs
index ead36d564b..f9ef895019 100644
--- a/experiments/atomic-codemode/reference.test.mjs
+++ b/experiments/atomic-codemode/reference.test.mjs
@@ -33,7 +33,7 @@ test("reference index discovers named methods without constructing unrequested s
     /Unknown reference view/,
   );
   const all = reference("", { view: "index" });
-  assert.equal(all.methods.length, 14);
+  assert.equal(all.methods.length, 15);
   assert.ok(
     all.methods.some(
       (m) => m.method === "relations" && m.description.includes("operands"),
@@ -67,7 +67,7 @@ test("named reference lists preserve caller order and exact schemas across prese
     ["facts_values", "facts_snapshot"],
   );
   assert.deepEqual(result.unmatched_queries, ["unknown"]);
-  assert.equal(result.coverage.declared_methods, 14);
+  assert.equal(result.coverage.declared_methods, 15);
   assert.equal(result.coverage.matched_methods, 2);
   assert.equal(result.coverage.selection, "named");
   const javascript = reference("rea.values snapshot");
@@ -96,7 +96,7 @@ test("named reference lists preserve caller order and exact schemas across prese
 });
 
 test("topic/all reference selection and shared schema ownership remain explicit", () => {
-  assert.equal(reference().methods.length, 14);
+  assert.equal(reference().methods.length, 15);
   assert.equal(reference("no-such-topic").coverage.matched_methods, 0);
   assert.ok(
     reference("memory aliases").methods.some((m) => m.method === "slice"),
diff --git a/experiments/atomic-codemode/savepoint-control-study.md b/experiments/atomic-codemode/savepoint-control-study.md
index b5adea74a7..e3bb63fcfb 100644
--- a/experiments/atomic-codemode/savepoint-control-study.md
+++ b/experiments/atomic-codemode/savepoint-control-study.md
@@ -165,3 +165,5 @@ variation also needs a bounded, matched diagnostic before further speed claims.
 The [subsequent four-case public MCP diagnostic](overlap-study.md) confirms
 provider admission is serialized and does not reproduce the long capture;
 the original cause remains unknown rather than being declared fixed.
+The [native switch extension](switch-study.md) now exports the case labels and
+checks all 182 original targets independently; its new model question is separate.
diff --git a/experiments/atomic-codemode/sqlite-switch-question.txt b/experiments/atomic-codemode/sqlite-switch-question.txt
new file mode 100644
index 0000000000..53cffc8986
--- /dev/null
+++ b/experiments/atomic-codemode/sqlite-switch-question.txt
@@ -0,0 +1,31 @@
+Investigate the format-owning sqlite3VdbeExec implementation in {{artifact_path}},
+starting from its callable name and these observed formats:
+- cannot open savepoint - SQL statements in progress
+- cannot release savepoint - SQL statements in progress
+
+Establish the implementation from references before deep analysis; a name may
+identify several entries. Reuse one retained VM capture and selected structured
+facts. Find its recovered indirect dispatch and distinguish the original byte
+selector from the width/identity of the retained normalized selector SSA value
+and from the machine's computed jump address.
+
+For case values 0x0, 0x2a, 0x34, 0x39 and 0xb5, report the original table-row
+identity, native case-to-edge identity/destination, and original recovered target.
+Check whether 0x34 and 0x39 share a target and edge. Do not infer labels from edge
+ordinals or optimized block origins. Query only the selected cases; do not fetch
+the complete case inventory, C report or graph.
+
+Use focused instructions to establish the machine dispatch: input width,
+unsigned range guard, table base, entry width/signedness and relative target
+calculation. Read the selected table bytes in a batch and derive the selected
+machine targets from those bytes, comparing with the retained native facts.
+Determine what the selected byte 0xb6 would do at that local guard, whether it
+has a captured explicit table case, and whether the native model's default
+out-edge is the same as the machine out-of-range guard destination. Keep those
+defaults, representations and identities separate.
+
+Return a focused answer with real Evidence IDs, target digest and necessary
+coverage. Native full-graph/table recovery does not establish complete machine
+flow, aliases, nontermination or feasible runtime inputs. Do not invent source
+member/opcode names, arbitrary loaded contents, a SQL trigger or runtime binding.
+Complete retained Evidence has paged source/decoded-graph access.
diff --git a/experiments/atomic-codemode/switch-oracle.md b/experiments/atomic-codemode/switch-oracle.md
new file mode 100644
index 0000000000..0167452573
--- /dev/null
+++ b/experiments/atomic-codemode/switch-oracle.md
@@ -0,0 +1,76 @@
+# SQLite indirect-dispatch oracle
+
+Freeze this question/oracle before measured model launches. The question supplies
+a function name, two formats and selected case values, without code/table/graph
+addresses. This is a scoped investigation. Both atomic adapters share facts;
+no traditional-provider cell exists for its required native identities. The
+direct client also has its own JavaScript executor.
+
+Target: Debian SQLite `3.40.1-2+deb12u2` amd64,
+`/usr/lib/x86_64-linux-gnu/libsqlite3.so.0` -> `.0.8.6`, SHA-256
+`2e6eef9a727f081f0d453b4e5e6cbd8b9ef8b6f86cbf7681cbad444d3b0b55c8`.
+Final engine SHA-256:
+`a9ca8a8ac224936afb08a9d4be9c1225feb69473ad9f35764e8d1c4f04875b5b`.
+
+Callable entries `0x288f0` and `0xea6d0` share the VDBE name; the two format
+references establish owning entry `0xea6d0` before deep analysis. Names do not
+establish runtime binding. One snapshot has 21,349 recovered operations, 35,755
+values, 1,229 blocks, zero omitted definitions and one indirect branch:
+`0xea801:fe`, block 8. The switch facet has 182 labelled rows and mappings,
+149 distinct targets/edges, partial=false, and zero missing/no-label/unmapped/
+unknown-target rows. Consumed mask is `0xff`; signed_render_hint=false is not
+itself an unsignedness proof.
+
+The current selector is eight-byte `v100031675` at `register:0x10`, defined by
+`0xea7f6:c353 CPUI_INT_ZEXT`. Its one-byte input `v10000024f` is defined by LOAD
+`0xea7e1:de`. Those widths/definitions are verified in structured native facts.
+The machine reads one byte, indexes through R15B/EDX, computes a target in RAX
+and jumps through RAX. The normalized BRANCHIND input is not that jump address.
+Storage offsets do not specify arbitrary computed contents.
+
+Independent GNU disassembly and ELF program-header/file reads establish:
+
+| Address | Bytes          | Machine fact                    |
+| ------- | -------------- | ------------------------------- |
+| 0xea7e1 | 440fb638       | MOVZX R15D,byte [RAX]           |
+| 0xea7e5 | 4180ffb5       | CMP R15B,0xb5                   |
+| 0xea7e9 | 0f87a9010000   | JA 0xea998; fallthrough 0xea7ef |
+| 0xea7ef | 488d0d121f0400 | LEA RCX,[0x12c708]              |
+| 0xea7f6 | 410fb6d7       | MOVZX EDX,R15B                  |
+| 0xea7fa | 48630491       | MOVSXD RAX,dword [RCX+RDX*4]    |
+| 0xea7fe | 4801c8         | ADD RAX,RCX                     |
+| 0xea801 | ffe0           | JMP RAX                         |
+
+Table base is `0x12c708`: 182 entries for zero-extended byte values `0..0xb5`,
+each a signed little-endian 32-bit displacement added to the base. Local
+`.cache/atomic-codemode/sqlite-switch-machine-oracle.json` records all bytes,
+file offsets and 149 unique targets, reconstructed before native verification.
+Both MCP paths compare all 182 native labelled rows to that independent table.
+
+| Case / row | Table address | Raw bytes / signed displacement | Native edge -> block | Original target |
+| ---------- | ------------- | ------------------------------- | -------------------- | --------------- |
+| 0x0 / 0    | 0x12c708      | d814fcff / -256808              | 8:0 -> 1140          | 0xedbe0         |
+| 0x2a / 42  | 0x12c7b0      | a8e7fbff / -268376              | 8:34 -> 864          | 0xeaeb0         |
+| 0x34 / 52  | 0x12c7d8      | e8e5fbff / -268824              | 8:42 -> 778          | 0xeacf0         |
+| 0x39 / 57  | 0x12c7ec      | e8e5fbff / -268824              | 8:42 -> 778          | 0xeacf0         |
+| 0xb5 / 181 | 0x12c9dc      | 16eefbff / -266730              | 8:8 -> 1011          | 0xeb51e         |
+
+The middle pair shares an edge/target but keeps distinct case identities.
+Row and edge ordinals differ: row 181 maps to edge 8. Relations carry case_id
+and a separate relation id; multiple edges share case_id and page separately.
+
+Native model default: `8:42`, block 778, origin `0xeacf0`, raw default index 42,
+default_is_folded=false. Known values `0x34..0x39` share it. It is not the
+machine out-of-range guard destination `0xea998`. No explicit native row is
+labelled `0xb6`. If the selected local byte were `0xb6`, unsigned JA bypasses
+the table and reaches `0xea998`; this does not prove that such input occurs.
+
+Grade the complete answer and trace: correct ownership before one VM capture,
+selected case reads, source-byte versus normalized-selector widths, row/edge
+identities and shared targets, selected raw displacement arithmetic, the two
+different defaults, real source IDs/digest and static coverage limitations.
+No whole case inventory/C report/graph fetch, source field/opcode-name guesses,
+SQL trigger or runtime binding claim. Full recovery does not prove complete
+machine flow, memory aliases, nontermination or feasible inputs. Producer
+equality is not independent machine/IR equivalence. Include discovery, schema
+reads, errors/retries, all responses and final answers in whole-task costs.
diff --git a/experiments/atomic-codemode/switch-study.md b/experiments/atomic-codemode/switch-study.md
new file mode 100644
index 0000000000..da4d38aa27
--- /dev/null
+++ b/experiments/atomic-codemode/switch-study.md
@@ -0,0 +1,131 @@
+# Native cases as composable facts
+
+The SQLite VM has 182 table entries and 149 distinct targets. Its native
+jump-table owner already knows labels and exact row-to-out-edge mappings;
+the experiment previously exported only the optimized CFG. This closes that
+export/query gap without deriving labels from edge order or block addresses.
+It remains an opt-in experiment, not stock-provider parity or integration.
+
+## Owners and contracts
+
+`atomic_membership` gathers BRANCHIND identities during its existing checked
+membership scan. Read-only `JumpTable` accessors borrow native address/label
+rows and edge positions. `atomic_switches` checks the exact linked operation,
+indexes mappings once and exports an independent version-1 facet alongside
+unchanged graph schema 3 and its optional schema-4 compression envelope.
+Ordinary non-opt-in analysis and target executable bytes are unchanged.
+
+Native limits are 12,000 switches, 100,000 rows/mappings and a shared 2 MiB
+selector/type/address-space text budget, within the existing supervised process
+and 8 MiB document bounds. Source labels stay exact hex strings. Missing tables,
+labels, targets/mappings and the native reserved no-label marker remain explicit.
+No-label status comes from the native owner; it is not guessed from an integer.
+
+`native-switch-contract` admits rows before expanding validation errors;
+`native-switch-views` owns identity checks, partial coverage and indexes. A full
+graph cross-checks operation/value/edge ownership; without it, shared values are
+checked against available calls/projection facts. Bad switch data makes that
+facet unavailable while preserving independently valid graph/calls/C.
+
+`switches` returns metadata and selector facts, never an embedded case inventory.
+`relations(kind:cases)` selects labels or original row indexes and pages
+individual case-to-edge relations. A case has a stable case_id; distinct edges
+have distinct relation IDs. Unmapped cases produce one explicit unknown-edge
+row. Relation totals are separate from native row and mapping counts. This
+avoids an unbounded edge array even when limit=1; a regression reads a late
+two-edge page from a 4,096-mapping case in under 1 KiB of returned items.
+
+Raw rows are retained once. Row lookup is direct, labels have an index, and
+prefix offsets permit paging without constructing all relation projections.
+Single-label offsets are cached only for existing labels, bounded by the
+retained source; arbitrary missing labels and filter combinations do not grow
+that cache. The validated model/lease owns its lifetime. Both MCP adapters and
+the JavaScript CLI consume these same owners.
+
+The native writer keeps old graph/call coverage ahead of the new facet when
+space is scarce. A source review found that a later projection omission could
+free space without restoring saved switch facts. `bounded_reclaiming` retries
+that saved facet whenever a preferred smaller combination fits. It moves trees,
+does not clone them, and bounds both encoded string alternatives. A focused
+native regression and real 2 MiB CLI captures verify the restored facts.
+
+## Real provider evidence
+
+Upstream: `fe01d6294eb0d1053ce343c8943646df88e143fc`.
+Final preserved engine:
+`a9ca8a8ac224936afb08a9d4be9c1225feb69473ad9f35764e8d1c4f04875b5b`.
+Patch SHA-256:
+`9b6642f498f3c9f356b253a2b8b14daf2154cde8eae2d4ab0696f018566e9b73`.
+The initial public checks used preserved `ac6bc7ab...`, before the formatter
+reclamation fix. Binaries are copied outside mutable Cargo outputs and not
+committed. Target/digest and independent machine oracle are in
+[switch-oracle.md](switch-oracle.md).
+
+Both final actual MCP paths compare every one of the 182 labelled original
+targets with independently reconstructed ELF table entries. Selected loaded
+bytes and dispatch instructions also agree. The native mappings cross-check
+against the full recovered graph; graph and ordinary C/metadata/calls match the
+prior complete golden. That producer comparison does not independently prove
+whole machine/IR equivalence. Each route executes fourteen MCP requests.
+
+The final wire document is 3,818,818 bytes. Two real native CLI processes with
+an explicit 2 MiB output budget instead produce identical 823,908-byte records:
+graph and projection are explicitly unavailable, while C, 416 calls and all
+182 cases survive. Replaying their retained source through the shared decoder
+again verifies every original target. This establishes the native CLI/decoder
+boundary, not a public MCP no-graph run; the MCP owner keeps its 8 MiB budget.
+
+The recovered selector is eight bytes but comes from a one-byte LOAD/ZEXT. The
+machine computes its jump address in a different register. Native default edge
+`8:42` points to block 778, origin `0xeacf0`; the unsigned machine out-of-range
+guard instead jumps to `0xea998`. Defaults, original addresses and optimized
+edge identities have separate authority, now stated in the contracts.
+
+## Executed checks and costs
+
+The shared JS suites pass 73 cases. Selected native CLI tests pass thirteen;
+one native jump-table test separately checks nonmatching ordinals/labels/edges,
+missing labels and inconsistent row lengths. Focused source lint passes without
+warnings; upstream compiler warnings are outside this patch. Full native corpus,
+stages/workspace and whole-REA gates remain unexecuted or previously resource
+limited; no integration readiness is claimed.
+
+| Executed scope                            | Family wall s | Family CPU s | Kernel peak MiB |
+| ----------------------------------------- | ------------: | -----------: | --------------: |
+| First native export build                 |       397.637 |      366.618 |         2,169.6 |
+| Identity/text-budget build                |       432.413 |      388.136 |         2,130.6 |
+| Initial twelve CLI tests                  |       100.723 |       99.982 |           647.3 |
+| Native jump-table test, including compile |       277.247 |      276.646 |         2,855.5 |
+| Final thirteen CLI tests                  |        52.204 |       40.984 |           476.4 |
+| Formatter-fix build                       |        63.414 |       50.208 |           524.5 |
+| Cached final build                        |         0.522 |        0.189 |            30.1 |
+| Initial Code MCP, ac6bc7ab                |        41.698 |       41.415 |           656.5 |
+| Initial direct MCP, ac6bc7ab              |        96.920 |       75.949 |           639.2 |
+| Two 2 MiB native CLI captures             |        79.377 |       79.060 |           514.7 |
+| Final direct MCP                          |        44.440 |       44.201 |           635.0 |
+| Final Code MCP                            |        43.828 |       43.504 |           643.0 |
+| Both catalog/reference checks             |         2.033 |        1.839 |           144.4 |
+| Real CLI empty switch/ID selection        |         3.646 |        3.397 |           188.8 |
+
+All resource runs use one CPU, 4 GiB hard / 3 GiB early-stop memory bounds,
+verified cleanup and OOM 0. Peaks include charged file cache, not RSS. Final
+same-lease snapshot plus selected-case reuse takes 4.8 ms / 0.006 CPU seconds
+direct and 8.2 ms / 0.009 Code; cumulative memory peaks only upper-bound isolated
+warm memory. OS caches and host contention are uncontrolled. These scripted
+measurements do not establish token savings or model outcomes.
+
+The initial direct capture also ran slowly (about 90 seconds), despite
+sequential requests and no model. This shows the earlier long capture is not
+unique to Code Mode or model interaction. The [overlap diagnostic](overlap-study.md)
+did not reproduce it. Its native/host cause remains unresolved; no speed fix or
+causal dispatch comparison is claimed.
+
+## Model question
+
+The [question](sqlite-switch-question.txt) and [oracle](switch-oracle.md) must be
+committed before either real model launch. They ask for selected labels,
+source-byte/normalized-selector widths, signed relative target arithmetic and
+the native-default versus machine-guard distinction, starting from function
+name/messages. Both lanes get the full catalog and the same exact discovery,
+envelope and stopping guidance; reverse engineering facts are not precomputed
+for the measured models. Real-model results are pending.
diff --git a/experiments/atomic-codemode/verify-discovery.mjs b/experiments/atomic-codemode/verify-discovery.mjs
index bf03b285eb..723998c1a4 100644
--- a/experiments/atomic-codemode/verify-discovery.mjs
+++ b/experiments/atomic-codemode/verify-discovery.mjs
@@ -38,6 +38,7 @@ for (const direct of [false, true]) {
     const catalog = await client.listTools();
     const prefix = direct ? "facts_" : "rea.";
     const ids = [
+      "switches",
       "snapshot",
       "operations",
       "relations",
@@ -52,7 +53,7 @@ for (const direct of [false, true]) {
       ids,
     );
     assert.deepEqual(selected.unmatched_queries, []);
-    assert.equal(selected.coverage.declared_methods, 14);
+    assert.equal(selected.coverage.declared_methods, 15);
     const ajv = new Ajv2020({ strict: false });
     for (const tool of catalog.tools) ajv.compile(tool.inputSchema);
     for (const method of selected.methods) {
@@ -63,7 +64,27 @@ for (const direct of [false, true]) {
     }
     for (const [name, good, bad] of [
       ["snapshot", { entry: "0xea6d0" }, { snapshot: "snap_other" }],
+      [
+        "switches",
+        {
+          snapshot: "snap_other",
+          origin_addresses: ["0xea801"],
+          fields: ["selector", "table"],
+        },
+        { snapshot: "snap_other", fields: ["rows"] },
+      ],
       ["values", { snapshot: "snap_other", ids: ["v1"] }, { entry: "0xea6d0" }],
+      [
+        "relations",
+        {
+          snapshot: "snap_other",
+          kind: "cases",
+          seeds: ["0xea801:fe"],
+          case_values: ["0xb5"],
+          case_indices: [181],
+        },
+        { snapshot: "snap_other", kind: "cases", seeds: [8] },
+      ],
       [
         "relations",
         {
@@ -105,7 +126,7 @@ for (const direct of [false, true]) {
     );
     assert.deepEqual(missing.unmatched_queries, ["unknown"]);
     const all = await call("");
-    assert.equal(all.methods.length, 14);
+    assert.equal(all.methods.length, 15);
     for (const method of all.methods) ajv.compile(method.input_schema);
     const index = await call("", "index");
     assert.equal(index.coverage.view, "index");
diff --git a/experiments/atomic-codemode/verify-switches.mjs b/experiments/atomic-codemode/verify-switches.mjs
new file mode 100644
index 0000000000..1d7a893084
--- /dev/null
+++ b/experiments/atomic-codemode/verify-switches.mjs
@@ -0,0 +1,253 @@
+// Real MCP switch facts against an independent ELF table/guard oracle.
+import assert from "node:assert/strict";
+import { readFile, writeFile } from "node:fs/promises";
+import { resolve, join } from "node:path";
+import { Client } from "@modelcontextprotocol/client";
+import { StdioClientTransport } from "@modelcontextprotocol/client/stdio";
+import Ajv2020 from "ajv/dist/2020.js";
+import { familyCounters } from "./family-counters.mjs";
+import { readNativeGraphEvidence } from "./native-ir-contract.mjs";
+import {
+  createVerifierRun,
+  completeVerifierRun,
+  assertVerifierCleanupComplete,
+} from "../../scripts/lib/verifier-run.mjs";
+
+const [binary, output, oraclePath, goldenPath] = process.argv.slice(2);
+assert.equal(process.versions.node, (await readFile(".nvmrc", "utf8")).trim());
+const oracle = JSON.parse(await readFile(oraclePath, "utf8")),
+  golden = JSON.parse(await readFile(goldenPath, "utf8")).functions[0];
+const run = createVerifierRun(),
+  calls = [],
+  failures = [],
+  phases = [];
+const direct = process.env.REA_ATOMIC_ADAPTER === "direct";
+const client = new Client({ name: "rea-switch-verifier", version: "0.1.0" });
+const transport = new StdioClientTransport({
+  command: process.execPath,
+  args: [resolve("experiments/atomic-codemode/server.mjs")],
+  env: { ...process.env },
+  stderr: "pipe",
+});
+async function call(name, input) {
+  const result = await client.callTool(
+    { name, arguments: input },
+    { timeout: 180000 },
+  );
+  const value = JSON.parse(result.content[0].text);
+  calls.push({
+    name,
+    input,
+    value,
+    content_bytes: Buffer.byteLength(result.content[0].text),
+  });
+  assert.equal(value.ok, true, JSON.stringify(value));
+  return value;
+}
+async function read(name, input) {
+  const result = direct
+    ? await call(`facts_${name}`, input)
+    : (
+        await call("execute_javascript", {
+          code: `return await rea.${name}(${JSON.stringify(input)});`,
+        })
+      ).value;
+  assert.equal(result.ok, true, JSON.stringify(result));
+  return result.data;
+}
+async function measure(phase, work) {
+  const before = await familyCounters(),
+    started = performance.now(),
+    value = await work();
+  const elapsed_ms = performance.now() - started,
+    after = await familyCounters();
+  phases.push({
+    phase,
+    elapsed_ms,
+    family_cpu_seconds: (after.cpu - before.cpu) / 1e6,
+    cumulative_family_memory_peak_bytes: after.peak,
+  });
+  return value;
+}
+let comparison;
+try {
+  await client.connect(transport);
+  const catalog = await client.listTools(),
+    ajv = new Ajv2020({ strict: false });
+  for (const tool of catalog.tools) ajv.compile(tool.inputSchema);
+  const opened = await call("open_binary", { path: binary });
+  assert.equal(opened.context.artifact_sha256, oracle.sha256);
+  const capture = await measure("fresh-snapshot", () =>
+    read("snapshot", { entry: "0xea6d0" }),
+  );
+  assert.equal(capture.facets.recovered_ir.availability, "available");
+  assert.equal(
+    capture.facets.switches.availability,
+    "available",
+    JSON.stringify(capture.facets.switches),
+  );
+  const snapshot = capture.snapshot,
+    listed = await read("switches", { snapshot });
+  assert.equal(listed.total, 1);
+  const sw = listed.items[0];
+  assert.equal(sw.id, "0xea801:fe");
+  assert.equal(sw.block, 8);
+  assert.equal(sw.selector.size_bytes, 8);
+  assert.equal(sw.selector.definition, "0xea7f6:c353");
+  assert.ok(sw.table && !("rows" in sw.table));
+  const all = [];
+  let offset = 0;
+  do {
+    const page = await read("relations", {
+      snapshot,
+      kind: "cases",
+      seeds: [sw.id],
+      offset,
+      limit: 64,
+    });
+    all.push(...page.items);
+    assert.ok(page.next_offset === null || page.next_offset > offset);
+    offset = page.next_offset;
+  } while (offset !== null);
+  assert.equal(all.length, sw.table.relation_count);
+  assert.equal(new Set(all.map((r) => r.id)).size, all.length);
+  assert.equal(new Set(all.map((r) => r.case_id)).size, sw.table.case_count);
+  const machine = new Map(oracle.rows.map((r) => [r.case_value, r])),
+    verified = new Set(),
+    outside = [];
+  for (const row of all) {
+    if (row.label?.status !== "value") continue;
+    const expected = machine.get(row.label.raw_bits);
+    if (!expected) {
+      outside.push(row);
+      continue;
+    }
+    assert.equal(row.recovered_target?.space, "ram");
+    assert.equal(
+      row.recovered_target?.offset,
+      expected.machine_target,
+      JSON.stringify(row),
+    );
+    verified.add(row.label.raw_bits);
+  }
+  comparison = {
+    native_table: sw.table,
+    verified_machine_labels: verified.size,
+    missing_machine_labels: [...machine.keys()].filter((v) => !verified.has(v)),
+    outside_table_labels: outside,
+  };
+  assert.deepEqual(comparison.missing_machine_labels, []);
+  const chosen = ["0x0", "0x1", "0x2a", "0xb5"],
+    selected = await read("relations", {
+      snapshot,
+      kind: "cases",
+      seeds: [sw.id, sw.id],
+      case_values: chosen,
+      limit: 64,
+    });
+  assert.equal(selected.next_offset, null);
+  assert.deepEqual(
+    selected.items,
+    all.filter(
+      (r) => r.label?.status === "value" && chosen.includes(r.label.raw_bits),
+    ),
+  );
+  const byIndex = await read("relations", {
+    snapshot,
+    kind: "cases",
+    seeds: [sw.id],
+    case_indices: [0, 181, 182, 0],
+    limit: 64,
+  });
+  assert.deepEqual(
+    byIndex.items,
+    all.filter((r) => [0, 181, 182].includes(r.case_index)),
+  );
+  const projected = await read("switches", {
+    snapshot,
+    ids: [sw.id],
+    fields: ["table"],
+  });
+  assert.equal(projected.items[0].selector, undefined);
+  const bytes = await read("bytes", {
+    windows: [
+      { address: oracle.machine_table_base, length: oracle.rows.length * 4 },
+    ],
+  });
+  assert.equal(bytes.results[0].ok, true);
+  assert.equal(bytes.results[0].hex, oracle.rows.map((r) => r.bytes).join(""));
+  const instructions = await read("instructions", {
+    windows: [{ address: "0xea7e1", count: 8 }],
+    fields: ["bytes", "text"],
+  });
+  assert.ok(
+    instructions.results[0].items.some(
+      (r) => r.address === "0xea801" && r.bytes === "ffe0",
+    ),
+  );
+  await measure("same-lease-reuse", async () => {
+    const repeat = await read("snapshot", { entry: "0xea6d0" });
+    assert.equal(repeat.snapshot, snapshot);
+    assert.deepEqual(
+      await read("relations", {
+        snapshot,
+        kind: "cases",
+        seeds: [sw.id],
+        case_values: chosen,
+        limit: 64,
+      }),
+      selected,
+    );
+  });
+  const source = await readFile(
+    join(
+      process.env.REA_ATOMIC_EVIDENCE_DIR,
+      `${capture.source.evidence_id}.txt`,
+    ),
+    "utf8",
+  );
+  const {
+    atomic_facts: _graph,
+    atomic_switches: _switches,
+    ...ordinary
+  } = JSON.parse(source).functions[0];
+  const { atomic_facts: expectedGraph, ...expectedOrdinary } = golden;
+  assert.deepEqual(
+    JSON.parse(readNativeGraphEvidence(source).text),
+    expectedGraph,
+  );
+  assert.deepEqual(ordinary, expectedOrdinary);
+  comparison.graph_and_ordinary_fields_match_golden = true;
+  await call("close_binary", {});
+} catch (error) {
+  failures.push(error.stack ?? String(error));
+} finally {
+  try {
+    await client.close();
+  } catch (error) {
+    failures.push(String(error));
+  }
+  try {
+    await transport.close();
+  } catch (error) {
+    failures.push(String(error));
+  }
+}
+const lifecycle = await completeVerifierRun(run);
+assertVerifierCleanupComplete(lifecycle.process_lineage);
+await writeFile(
+  output,
+  JSON.stringify({ direct, calls, comparison, phases, failures, lifecycle }),
+  { flag: "wx" },
+);
+console.log(
+  JSON.stringify({
+    output,
+    direct,
+    calls: calls.length,
+    comparison,
+    phases,
+    failures,
+  }),
+);
+if (failures.length) process.exitCode = 1;