diff --git a/decompiler/Cargo.lock b/decompiler/Cargo.lock
index 157e7bd2..6caa4604 100644
--- a/decompiler/Cargo.lock
+++ b/decompiler/Cargo.lock
@@ -23,6 +23,12 @@ version = "0.7.8"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d3fb67a6e08acf24fdeccbac2cb6ac4305825bd1f117462e0e6f2f193345ad56"
 
+[[package]]
+name = "base64"
+version = "0.22.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6"
+
 [[package]]
 name = "bitflags"
 version = "2.13.0"
@@ -265,6 +271,8 @@ dependencies = [
 name = "kuna-cli"
 version = "0.1.0"
 dependencies = [
+ "base64",
+ "flate2",
  "kuna-analysis",
  "kuna-base",
  "kuna-console",
diff --git a/decompiler/crates/kuna-cli/Cargo.toml b/decompiler/crates/kuna-cli/Cargo.toml
index 06231a77..db79599c 100644
--- a/decompiler/crates/kuna-cli/Cargo.toml
+++ b/decompiler/crates/kuna-cli/Cargo.toml
@@ -9,6 +9,8 @@ license.workspace = true
 publish.workspace = true
 
 [dependencies]
+base64 = "=0.22.1"
+flate2 = "=1.1.9"
 kuna-decomp.workspace = true
 kuna-base.workspace = true
 kuna-console.workspace = true
diff --git a/decompiler/crates/kuna-cli/src/atomic_compression.rs b/decompiler/crates/kuna-cli/src/atomic_compression.rs
new file mode 100644
index 00000000..48631d39
--- /dev/null
+++ b/decompiler/crates/kuna-cli/src/atomic_compression.rs
@@ -0,0 +1,122 @@
+//! Bounded lossless wire encoding of logical schema-3 atomic graphs.
+use crate::jsonfmt::{dumps_compact_bounded, Json};
+use base64::{engine::general_purpose::STANDARD, Engine as _};
+use flate2::{write::GzEncoder, Compression};
+use std::io::{self, Write};
+
+const MAX_RAW_BYTES: usize = 32 * 1024 * 1024;
+struct BoundedBytes {
+    data: Vec<u8>,
+    limit: usize,
+}
+impl Write for BoundedBytes {
+    fn write(&mut self, bytes: &[u8]) -> io::Result<usize> {
+        let next = self
+            .data
+            .len()
+            .checked_add(bytes.len())
+            .filter(|n| *n <= self.limit)
+            .ok_or_else(|| io::Error::other("atomic compression capacity exceeded"))?;
+        if next > self.data.capacity() {
+            let capacity = next
+                .max(self.data.capacity().saturating_mul(2))
+                .min(self.limit);
+            self.data
+                .try_reserve_exact(capacity - self.data.len())
+                .map_err(|_| io::Error::other("atomic compression allocation failed"))?;
+        }
+        self.data.extend_from_slice(bytes);
+        Ok(bytes.len())
+    }
+    fn flush(&mut self) -> io::Result<()> {
+        Ok(())
+    }
+}
+
+pub(crate) fn encode(graph: &Json, limit: usize) -> Option<(Json, usize)> {
+    let Json::Object(fields) = graph else {
+        return None;
+    };
+    if !fields
+        .iter()
+        .any(|(key, v)| key == "schema_version" && *v == Json::Number("3".into()))
+    {
+        return None;
+    }
+    let raw = dumps_compact_bounded(graph, MAX_RAW_BYTES)?;
+    let mut envelope = Json::Object(vec![
+        ("schema_version".into(), Json::Number("4".into())),
+        ("encoding".into(), Json::Str("gzip-base64".into())),
+        ("raw_bytes".into(), Json::Number(raw.len().to_string())),
+        ("data".into(), Json::Str(String::new())),
+    ]);
+    let overhead = dumps_compact_bounded(&envelope, limit)?.len();
+    let payload_limit = limit.checked_sub(overhead)?;
+    let compressed_limit = (payload_limit / 4).checked_mul(3)?;
+    let mut gzip = GzEncoder::new(
+        BoundedBytes {
+            data: Vec::new(),
+            limit: compressed_limit,
+        },
+        Compression::fast(),
+    );
+    gzip.write_all(raw.as_bytes()).ok()?;
+    let compressed = gzip.finish().ok()?.data;
+    let encoded_len = compressed
+        .len()
+        .checked_add(2)?
+        .checked_div(3)?
+        .checked_mul(4)?;
+    if encoded_len > payload_limit {
+        return None;
+    }
+    let encoded = STANDARD.encode(compressed);
+    if let Json::Object(fields) = &mut envelope {
+        let (_, data) = fields.iter_mut().find(|(key, _)| key == "data")?;
+        *data = Json::Str(encoded);
+    }
+    Some((envelope, overhead + encoded_len))
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use std::io::Read;
+    #[test]
+    fn lossless_frame_accounts_for_escaping_and_base64_expansion() {
+        let graph = Json::Object(vec![
+            ("schema_version".into(), Json::Number("3".into())),
+            ("statement".into(), Json::Str("中文😀\0".repeat(1000))),
+        ]);
+        let (encoded, size) = encode(&graph, 2000).unwrap();
+        let text = dumps_compact_bounded(&encoded, 2000).unwrap();
+        assert_eq!(text.len(), size);
+        let frame: serde_json::Value = serde_json::from_str(&text).unwrap();
+        let bytes = STANDARD.decode(frame["data"].as_str().unwrap()).unwrap();
+        let mut restored = String::new();
+        flate2::read::GzDecoder::new(bytes.as_slice())
+            .read_to_string(&mut restored)
+            .unwrap();
+        assert_eq!(
+            restored,
+            dumps_compact_bounded(&graph, MAX_RAW_BYTES).unwrap()
+        );
+        assert_eq!(frame["raw_bytes"].as_u64().unwrap(), restored.len() as u64);
+        assert!(encode(&graph, 1).is_none());
+        assert!(encode(&graph, size - 1).is_none());
+    }
+    #[test]
+    fn archive_is_single_layer_and_raw_allocation_has_an_independent_bound() {
+        assert!(encode(&Json::Str("not a graph".into()), 1000).is_none());
+        let nested = Json::Object(vec![("schema_version".into(), Json::Number("4".into()))]);
+        assert!(encode(&nested, 1000).is_none());
+        let oversized = Json::Object(vec![
+            ("schema_version".into(), Json::Number("3".into())),
+            (
+                "statement".into(),
+                Json::Str("\0".repeat(MAX_RAW_BYTES / 6 + 1)),
+            ),
+        ]);
+        assert!(encode(&oversized, 1000).is_none());
+    }
+}
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..6005472b
--- /dev/null
+++ b/decompiler/crates/kuna-cli/src/atomic_json.rs
@@ -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.
+
+use crate::jsonfmt::{dumps_compact_bounded, Json};
+
+// Ownership is moved out while trying bounded alternatives, never cloned.
+struct RemovedFacet {
+    function: usize,
+    field: usize,
+    value: (String, Json),
+    added_error: bool,
+}
+#[derive(Clone, Copy)]
+enum Omission {
+    Capacity,
+    RedundantWithGraph,
+}
+fn function_records(document: &mut Json) -> Option<&mut Vec<Json>> {
+    let Json::Object(fields) = document else {
+        return None;
+    };
+    let (_, value) = fields.iter_mut().find(|(key, _)| key == "functions")?;
+    let Json::Array(functions) = value else {
+        return None;
+    };
+    Some(functions)
+}
+fn take_facet(document: &mut Json, name: &str, limit: usize, why: Omission) -> Vec<RemovedFacet> {
+    let mut removed = Vec::new();
+    if let Some(functions) = function_records(document) {
+        for (function, record) in functions.iter_mut().enumerate() {
+            if let Json::Object(fields) = record {
+                if matches!(why, Omission::RedundantWithGraph)
+                    && !fields.iter().any(|(key, _)| key == "atomic_facts")
+                {
+                    continue;
+                }
+                if let Some(field) = fields.iter().position(|(key, _)| key == name) {
+                    let value = fields.remove(field);
+                    let error = format!("{name}_error");
+                    let added_error = matches!(why, Omission::Capacity)
+                        && !fields.iter().any(|(key, _)| key == &error);
+                    if added_error {
+                        fields.push((error, Json::Str(format!("atomic encoded document exceeds {limit} byte capacity; {name} omitted, code retained"))));
+                    }
+                    removed.push(RemovedFacet {
+                        function,
+                        field,
+                        value,
+                        added_error,
+                    });
+                }
+            }
+        }
+    }
+    removed
+}
+fn restore_facet(document: &mut Json, removed: Vec<RemovedFacet>) {
+    if let Some(functions) = function_records(document) {
+        for facet in removed {
+            if let Json::Object(fields) = &mut functions[facet.function] {
+                if facet.added_error {
+                    let error = format!("{}_error", facet.value.0);
+                    fields.retain(|(key, _)| key != &error);
+                }
+                fields.insert(facet.field, facet.value);
+            }
+        }
+    }
+}
+struct GraphAlternative {
+    function: usize,
+    value: Json,
+}
+fn compress_graphs(document: &mut Json, budget: usize) -> Vec<GraphAlternative> {
+    let mut originals = Vec::new();
+    let mut remaining = budget;
+    if let Some(functions) = function_records(document) {
+        for (function, record) in functions.iter_mut().enumerate() {
+            if let Json::Object(fields) = record {
+                if let Some((_, graph)) = fields.iter_mut().find(|(key, _)| key == "atomic_facts") {
+                    if let Some((encoded, size)) =
+                        crate::atomic_compression::encode(graph, remaining)
+                    {
+                        remaining -= size;
+                        originals.push(GraphAlternative {
+                            function,
+                            value: std::mem::replace(graph, encoded),
+                        });
+                    }
+                }
+            }
+        }
+    }
+    originals
+}
+fn exchange_graphs(
+    document: &mut Json,
+    alternatives: Vec<GraphAlternative>,
+) -> Vec<GraphAlternative> {
+    let mut previous = Vec::new();
+    if let Some(functions) = function_records(document) {
+        for alternative in alternatives {
+            if let Json::Object(fields) = &mut functions[alternative.function] {
+                if let Some((_, graph)) = fields.iter_mut().find(|(key, _)| key == "atomic_facts") {
+                    previous.push(GraphAlternative {
+                        function: alternative.function,
+                        value: std::mem::replace(graph, alternative.value),
+                    });
+                }
+            }
+        }
+    }
+    previous
+}
+fn bounded(document: &Json, budget: usize) -> Option<String> {
+    let mut text = dumps_compact_bounded(document, budget)?;
+    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)
+        .ok_or("atomic JSON output budget is zero")?;
+    // A full graph already owns these operation/value facts. Keep its bounded
+    // projection aside in case encoded size later makes that graph unavailable.
+    let projection = take_facet(
+        &mut document,
+        "atomic_projection",
+        limit,
+        Omission::RedundantWithGraph,
+    );
+    if let Some(text) = bounded(&document, budget) {
+        return Ok(text);
+    }
+    let originals = compress_graphs(&mut document, budget);
+    let mut alternatives = if originals.is_empty() {
+        Vec::new()
+    } else {
+        if let Some(text) = bounded(&document, budget) {
+            return Ok(text);
+        }
+        exchange_graphs(&mut document, originals)
+    };
+    // 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() {
+            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,
+        "atomic_projection",
+        limit,
+        Omission::Capacity,
+    );
+    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_reclaiming(&mut document, budget, "atomic_switches", &mut switches)
+    {
+        return Ok(text);
+    }
+    take_facet(
+        &mut document,
+        "atomic_projection",
+        limit,
+        Omission::Capacity,
+    );
+    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::*;
+
+    #[test]
+    fn encoded_overflow_preserves_code_and_replaces_only_the_graph() {
+        let original = Json::Object(vec![(
+            "functions".into(),
+            Json::Array(vec![Json::Object(vec![
+                ("code".into(), Json::Str("retained C".into())),
+                ("error".into(), Json::Null),
+                ("atomic_facts".into(), Json::Str("😀".repeat(1000))),
+            ])]),
+        )]);
+        let full = render(original.clone(), 20000).unwrap();
+        assert!(full.len() > 12000); // ASCII surrogate escaping is accounted for.
+        let reduced = render(original.clone(), 256).unwrap();
+        let document: serde_json::Value = serde_json::from_str(&reduced).unwrap();
+        let function = &document["functions"][0];
+        assert_eq!(function["code"], "retained C");
+        assert_eq!(function["error"], serde_json::Value::Null);
+        assert!(function.get("atomic_facts").is_none());
+        assert!(function["atomic_facts_error"]
+            .as_str()
+            .unwrap()
+            .contains("256"));
+        assert!(reduced.len() <= 256);
+        assert!(render(original, 1).is_err());
+    }
+}
+
+#[cfg(test)]
+mod compressed_graph_tests {
+    use super::*;
+    use base64::{engine::general_purpose::STANDARD, Engine as _};
+    use std::io::Read;
+    #[test]
+    fn compressed_graph_retains_calls_and_code_before_losing_any_facet() {
+        let graph = Json::Object(vec![
+            ("schema_version".into(), Json::Number("3".into())),
+            ("payload".into(), Json::Str("x".repeat(100_000))),
+        ]);
+        let original = Json::Object(vec![(
+            "functions".into(),
+            Json::Array(vec![Json::Object(vec![
+                ("code".into(), Json::Str("retained C".into())),
+                ("atomic_facts".into(), graph.clone()),
+                ("atomic_calls".into(), Json::Str("independent calls".into())),
+                ("atomic_projection".into(), Json::Str("fallback".into())),
+            ])]),
+        )]);
+        let uncompressed: serde_json::Value =
+            serde_json::from_str(&render(original.clone(), 200_000).unwrap()).unwrap();
+        assert_eq!(
+            uncompressed["functions"][0]["atomic_facts"]["schema_version"],
+            3
+        );
+        let text = render(original.clone(), 4096).unwrap();
+        assert!(text.len() <= 4096);
+        let document: serde_json::Value = serde_json::from_str(&text).unwrap();
+        let function = &document["functions"][0];
+        assert_eq!(function["code"], "retained C");
+        assert_eq!(function["atomic_calls"], "independent calls");
+        assert!(function.get("atomic_projection").is_none());
+        assert!(function.get("atomic_facts_error").is_none());
+        let frame = &function["atomic_facts"];
+        assert_eq!(frame["schema_version"], 4);
+        let compressed = STANDARD.decode(frame["data"].as_str().unwrap()).unwrap();
+        let mut restored = String::new();
+        flate2::read::GzDecoder::new(compressed.as_slice())
+            .read_to_string(&mut restored)
+            .unwrap();
+        assert_eq!(restored, dumps_compact_bounded(&graph, 200_000).unwrap());
+        let tiny: serde_json::Value =
+            serde_json::from_str(&render(original, 512).unwrap()).unwrap();
+        assert!(tiny["functions"][0].get("atomic_facts").is_none());
+        assert_eq!(tiny["functions"][0]["atomic_projection"], "fallback");
+        assert_eq!(tiny["functions"][0]["atomic_calls"], "independent calls");
+    }
+}
+
+#[cfg(test)]
+mod independent_facet_tests {
+    use super::*;
+    fn document(graph: usize, calls: usize) -> Json {
+        Json::Object(vec![(
+            "functions".into(),
+            Json::Array(vec![Json::Object(vec![
+                ("code".into(), Json::Str("retained C".into())),
+                ("ordinary".into(), Json::Number("42".into())),
+                ("atomic_facts".into(), Json::Str("x".repeat(graph))),
+                ("atomic_calls".into(), Json::Str("y".repeat(calls))),
+            ])]),
+        )])
+    }
+    #[test]
+    fn each_facet_survives_the_others_encoded_overflow() {
+        for (graph, calls, keep) in [(2000, 1, "atomic_calls"), (1, 2000, "atomic_facts")] {
+            let rendered = render(document(graph, calls), 512).unwrap();
+            assert!(rendered.len() <= 512);
+            let d: serde_json::Value = serde_json::from_str(&rendered).unwrap();
+            let f = &d["functions"][0];
+            assert!(f.get(keep).is_some());
+            assert_eq!(f["ordinary"], 42);
+            assert_eq!(f["code"], "retained C");
+        }
+    }
+    #[test]
+    fn jointly_oversized_facets_preserve_the_existing_graph_when_it_fits() {
+        let rendered = render(document(1000, 1000), 1600).unwrap();
+        let d: serde_json::Value = serde_json::from_str(&rendered).unwrap();
+        assert!(d["functions"][0].get("atomic_facts").is_some());
+        assert!(d["functions"][0].get("atomic_calls").is_none());
+    }
+    #[test]
+    fn base_record_survives_both_overflows_or_fails_explicitly() {
+        let rendered = render(document(2000, 2000), 512).unwrap();
+        let d: serde_json::Value = serde_json::from_str(&rendered).unwrap();
+        let f = &d["functions"][0];
+        assert!(f.get("atomic_facts").is_none() && f.get("atomic_calls").is_none());
+        assert!(f["atomic_facts_error"].is_string() && f["atomic_calls_error"].is_string());
+        assert_eq!(f["code"], "retained C");
+        assert!(render(document(1, 1), 1).is_err());
+    }
+}
+
+#[cfg(test)]
+mod projection_tests {
+    use super::*;
+    fn document(graph: usize, calls: usize, projection: 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)),
+                ),
+            ])]),
+        )])
+    }
+    #[test]
+    fn full_graph_avoids_duplicate_projection_and_encoded_failure_restores_it() {
+        for (graph, retained) in [(10, "atomic_facts"), (3000, "atomic_projection")] {
+            let rendered = render(document(graph, 10, 10), 1024).unwrap();
+            let d: serde_json::Value = serde_json::from_str(&rendered).unwrap();
+            let f = &d["functions"][0];
+            assert!(f.get(retained).is_some());
+            assert!(f.get("atomic_calls").is_some());
+            assert_eq!(f["code"], "retained C");
+            if retained == "atomic_facts" {
+                assert!(f.get("atomic_projection").is_none());
+                assert!(f.get("atomic_projection_error").is_none());
+            }
+        }
+    }
+    #[test]
+    fn fallback_facets_survive_independently_without_losing_code() {
+        for (calls, projection, retained) in
+            [(3000, 10, "atomic_projection"), (10, 3000, "atomic_calls")]
+        {
+            let rendered = render(document(3000, calls, projection), 1024).unwrap();
+            let d: serde_json::Value = serde_json::from_str(&rendered).unwrap();
+            assert!(d["functions"][0].get(retained).is_some());
+            assert_eq!(d["functions"][0]["code"], "retained C");
+            assert!(rendered.len() <= 1024);
+        }
+    }
+}
diff --git a/decompiler/crates/kuna-cli/src/decompile.rs b/decompiler/crates/kuna-cli/src/decompile.rs
index ad249b04..62074996 100644
--- a/decompiler/crates/kuna-cli/src/decompile.rs
+++ b/decompiler/crates/kuna-cli/src/decompile.rs
@@ -841,6 +841,8 @@ pub fn main(argv: &[String]) -> Result<i32, String> {
     let mut target: Option<String> = None;
     let mut addr = false;
     let mut json = false;
+    let mut atomic_facts = false;
+    let mut atomic_output_bytes = None;
     let mut bfd_target: Option<String> = None;
     let mut raw = false;
     let mut regions = false;
@@ -871,6 +873,13 @@ pub fn main(argv: &[String]) -> Result<i32, String> {
         match a {
             "--addr" => addr = true,
             "--json" => json = true,
+            "--atomic-facts" => atomic_facts = true,
+            "--atomic-output-bytes" => {
+                let value = take_value(argv, &mut i, "--atomic-output-bytes")?;
+                atomic_output_bytes = Some(value.parse::<usize>()
+                    .ok().filter(|bytes| *bytes > 0)
+                    .ok_or("--atomic-output-bytes requires a positive byte count")?);
+            }
             "--raw" => raw = true,
             "--raw-image" => raw_image = true,
             "--base" => base = Some(parse_cli_address(&take_value(argv, &mut i, "--base")?)?),
@@ -979,7 +988,13 @@ pub fn main(argv: &[String]) -> Result<i32, String> {
         return Err("--base requires --raw-image".into());
     }
 
+    if atomic_output_bytes.is_some() && !atomic_facts {
+        return Err("--atomic-output-bytes requires --atomic-facts".into());
+    }
     if json {
+        if atomic_facts && (!cfg!(feature = "embed-specs") || sleighpath.is_some()) {
+            return Err("--atomic-facts requires embedded specs and does not accept --sleighpath".into());
+        }
         // Refused, not ignored: each of these is a `decomp_dbg` transcript the
         // in-process JSON path never produces, and silently dropping half a
         // request is the failure mode `--json` exists to end.
@@ -997,6 +1012,8 @@ pub fn main(argv: &[String]) -> Result<i32, String> {
             binary: &binary,
             target: &target,
             by_address: addr,
+            atomic_facts,
+            atomic_output_bytes: atomic_output_bytes.unwrap_or(8 * 1024 * 1024),
             forwarded: &forwarded,
             mode: mode.as_deref(),
             bfd_target: bfd_target.as_deref(),
@@ -1007,6 +1024,10 @@ pub fn main(argv: &[String]) -> Result<i32, String> {
         }));
     }
 
+    if atomic_facts {
+        return Err("--atomic-facts requires --json".into());
+    }
+
     // (kuna outlang, DIV-80) The auto policy -- follow the binary when the caller
     // named no language. See `decompile_all::detected_output_language`.
     if !saw_language && !options.iter().any(|(n, _)| n == "setlanguage") {
@@ -1106,6 +1127,8 @@ struct JsonRequest<'a> {
     binary: &'a str,
     target: &'a str,
     by_address: bool,
+    atomic_facts: bool,
+    atomic_output_bytes: usize,
     /// The `--option` / `--language` tokens, in argv order.
     forwarded: &'a [String],
     mode: Option<&'a str>,
@@ -1127,6 +1150,18 @@ struct JsonRequest<'a> {
 /// drift.
 fn run_json(req: &JsonRequest) -> i32 {
     let mut argv: Vec<String> = vec![req.binary.to_string(), "--json".into()];
+    if req.atomic_facts {
+        match crate::embedded_specs::tree() {
+            Some(Ok(root)) => {
+                argv.push("--sleighpath".into());
+                argv.push(root.to_string_lossy().into_owned());
+            }
+            _ => {
+                eprintln!("error: atomic facts require readable embedded specs");
+                return 2;
+            }
+        }
+    }
     if req.by_address {
         argv.push("--addr".into());
         argv.push(if looks_like_addr(req.target) {
@@ -1168,7 +1203,7 @@ fn run_json(req: &JsonRequest) -> i32 {
     // it has to reconcile against a prose stderr line — the missing error channel
     // is half of why this flag exists. The verdict follows the document, matching
     // `run`'s stdout-then-stderr ordering.
-    let (text, failure) = match decompile_json(&args, req.target) {
+    let (text, failure) = match decompile_json(&args, req.target, req.atomic_facts.then_some(req.atomic_output_bytes)) {
         Ok(answered) => answered,
         Err(message) => (
             decompile_all::render_result_json(
@@ -1197,7 +1232,7 @@ fn run_json(req: &JsonRequest) -> i32 {
 /// was asked about exactly that function — so `--json` cannot turn the text
 /// surface's non-zero verdict into a success; the reason is in the document too,
 /// as the record's `error` and as the run-level one.
-fn decompile_json(args: &AllArgs, target: &str) -> Result<(String, Option<String>), String> {
+fn decompile_json(args: &AllArgs, target: &str, atomic_limit: Option<usize>) -> Result<(String, Option<String>), String> {
     let mut prog = decompile_all::load_program(args, DriverDefaults::Decompile)?;
     let targets = decompile_all::resolve_targets(&prog, args)?;
     let interior = crate::interior::selections(&prog, args, &targets);
@@ -1217,7 +1252,7 @@ fn decompile_json(args: &AllArgs, target: &str) -> Result<(String, Option<String
         });
     }
 
-    let funcs = decompile_all::decompile_entries(&mut prog, args, targets, false);
+    let funcs = decompile_all::decompile_entries(&mut prog, args, targets, false, atomic_limit.is_some());
     let assertions = prog.assertion_outcomes();
     let mut failure = funcs.iter().find_map(|f| {
         f.error.as_ref().map(|reason| {
@@ -1235,14 +1270,18 @@ fn decompile_json(args: &AllArgs, target: &str) -> Result<(String, Option<String
     if failure.is_none() && decompile_all::any_refused_assertion(&assertions) {
         failure = Some(format!("--assert directive refused by the pipeline in {}", args.binary));
     }
-    let text = decompile_all::render_result_json(
+    let text = if let Some(limit) = atomic_limit {
+        decompile_all::render_atomic_result_json(
+            &args.binary, &funcs, &args.options, failure.as_deref(), &assertions, &interior, limit,
+        )?
+    } else { decompile_all::render_result_json(
         &args.binary,
         &funcs,
         &args.options,
         failure.as_deref(),
         &assertions,
         &interior,
-    );
+    ) };
     if failure.is_none() && args.assert_strict && rejected {
         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..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> {
                 park_recovered_proto: false,
                 single_target: false,
                 want_tokens: false,
+                want_atomic_facts: false,
                 want_pointer_arguments: args.jobs_pointerargs,
             };
             let mut pending = entries.into_iter();
@@ -1264,7 +1265,7 @@ fn decompile_all(args: &Args, filters: &Filters) -> Result<AllRun, String> {
     let funcs = if callee_first {
         decompile_entries_callee_first(&mut prog, args, targets, explicit)
     } else {
-        decompile_entries(&mut prog, args, targets, /* pointer_arguments= */ true)
+        decompile_entries(&mut prog, args, targets, /* pointer_arguments= */ true, false)
     };
     Ok(AllRun { funcs, discovered, assertions: prog.assertion_outcomes(), interior })
 }
@@ -1319,6 +1320,7 @@ pub(crate) fn decompile_entries(
     args: &Args,
     targets: Vec<FunctionEntry>,
     pointer_arguments: bool,
+    want_atomic_facts: bool,
 ) -> Vec<FuncResult> {
     arm_fn_budgets(prog, args);
     let opts = DecompileOptions {
@@ -1326,6 +1328,7 @@ pub(crate) fn decompile_entries(
         want_provenance: args.json,
         single_target: targets.len() == 1,
         want_pointer_arguments: pointer_arguments,
+        want_atomic_facts,
         ..DecompileOptions::default()
     };
     kuna_console::project::decompile_targets_with(prog, targets, &opts)
@@ -2003,6 +2006,19 @@ pub(crate) fn render_result_json(
     render_selected_json(binary, funcs, options, error, None, assertions, interior)
 }
 
+pub(crate) fn render_atomic_result_json(
+    binary: &str,
+    funcs: &[FuncResult],
+    options: &[(String, String)],
+    error: Option<&str>,
+    assertions: &[kuna_console::assertions::Outcome],
+    interior: &crate::interior::Interiors,
+    limit: usize,
+) -> Result<String, String> {
+    let language = last_option_value(options, "setlanguage").unwrap_or("c-language");
+    crate::atomic_json::render(result_json(binary, funcs, language, error, None, assertions, interior), limit)
+}
+
 /// [`render_result_json`] plus the inventory `total` a NARROWED whole-binary run
 /// answers with.
 ///
@@ -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 +3541,16 @@ mod triage_tests {
     }
 
 }
+
+// Named independent facets share serialization/failure semantics; a bad facet
+// cannot erase the ordinary C record or another valid facet.
+fn append_atomic_facet<T: serde::Serialize>(record: &mut Vec<(String, Json)>, name: &str, facts: Option<&Result<T, String>>) {
+    if let Some(facts) = facts {
+        let encoded = facts.as_ref().map_err(Clone::clone)
+            .and_then(|facts| serde_json::to_value(facts).map_err(|error| format!("atomic facet serialization failed: {error}")));
+        match encoded {
+            Ok(value) => record.push((name.into(), Json::from(value))),
+            Err(reason) => record.push((format!("{name}_error"), Json::Str(reason))),
+        }
+    }
+}
diff --git a/decompiler/crates/kuna-cli/src/decompile_all/callee_first.rs b/decompiler/crates/kuna-cli/src/decompile_all/callee_first.rs
index 3eb2a6e4..2b951ba2 100644
--- a/decompiler/crates/kuna-cli/src/decompile_all/callee_first.rs
+++ b/decompiler/crates/kuna-cli/src/decompile_all/callee_first.rs
@@ -28,6 +28,7 @@ pub(super) fn decompile_entries_callee_first(
         park_recovered_proto: false,
         single_target: targets.len() == 1,
         want_tokens: false,
+        want_atomic_facts: false,
         want_pointer_arguments: true,
     };
     decompile_callee_first(prog, args, targets, explicit, base)
diff --git a/decompiler/crates/kuna-cli/src/jsonfmt.rs b/decompiler/crates/kuna-cli/src/jsonfmt.rs
index 198b85a6..71bd9675 100644
--- a/decompiler/crates/kuna-cli/src/jsonfmt.rs
+++ b/decompiler/crates/kuna-cli/src/jsonfmt.rs
@@ -28,6 +28,19 @@ pub enum Json {
     Object(Vec<(String, Json)>),
 }
 
+impl From<serde_json::Value> for Json {
+    fn from(value: serde_json::Value) -> Self {
+        match value {
+            serde_json::Value::Null => Json::Null,
+            serde_json::Value::Bool(value) => Json::Bool(value),
+            serde_json::Value::Number(value) => Json::Number(value.to_string()),
+            serde_json::Value::String(value) => Json::Str(value),
+            serde_json::Value::Array(values) => Json::Array(values.into_iter().map(Json::from).collect()),
+            serde_json::Value::Object(values) => Json::Object(values.into_iter().map(|(key, value)| (key, Json::from(value))).collect()),
+        }
+    }
+}
+
 /// Render `v` exactly as CPython's `json.dumps(v, indent=2)` would (ASCII-safe
 /// string escaping, `", "`/`": "` item/key separators collapsed to the indent
 /// form: items separated by `,\n`, keys by `": "`).
@@ -50,6 +63,12 @@ pub fn dumps_compact(v: &Json) -> String {
     writer::render(v, Format::Compact)
 }
 
+/// Enforce the caller's encoded-byte budget before growing the output buffer.
+/// Uses the same writer and escaping as the other modes; no length estimator.
+pub fn dumps_compact_bounded(v: &Json, limit: usize) -> Option<String> {
+    writer::render_bounded(v, Format::Compact, limit)
+}
+
 /// Extract the JSON array/object span out of a `decomp_dbg` console transcript.
 ///
 /// Port of `kuna/catalog.py::_extract_json`: drop the fixed `[decomp]>` prompt
diff --git a/decompiler/crates/kuna-cli/src/jsonfmt/writer.rs b/decompiler/crates/kuna-cli/src/jsonfmt/writer.rs
index c4eca1db..06b9d024 100644
--- a/decompiler/crates/kuna-cli/src/jsonfmt/writer.rs
+++ b/decompiler/crates/kuna-cli/src/jsonfmt/writer.rs
@@ -1,7 +1,7 @@
 //! JSON layout and ASCII-safe escaping shared by all CLI output modes.
 
 use super::Json;
-use std::fmt::Write as _;
+use std::fmt::{self, Write};
 
 #[derive(Clone, Copy, PartialEq, Eq)]
 pub(super) enum Format {
@@ -12,108 +12,142 @@ pub(super) enum Format {
 
 pub(super) fn render(value: &Json, format: Format) -> String {
     let mut out = String::new();
-    write_value(&mut out, value, 0, format);
+    write_value(&mut out, value, 0, format).expect("String writer is infallible");
     out
 }
 
+struct BoundedString {
+    text: String,
+    limit: usize,
+}
+
+impl Write for BoundedString {
+    fn write_str(&mut self, value: &str) -> fmt::Result {
+        let next = self.text.len().checked_add(value.len()).ok_or(fmt::Error)?;
+        if next > self.limit {
+            return Err(fmt::Error);
+        }
+        if next > self.text.capacity() {
+            let capacity = next
+                .max(self.text.capacity().saturating_mul(2))
+                .min(self.limit);
+            self.text
+                .try_reserve_exact(capacity - self.text.len())
+                .map_err(|_| fmt::Error)?;
+        }
+        self.text.push_str(value);
+        Ok(())
+    }
+}
+
+pub(super) fn render_bounded(value: &Json, format: Format, limit: usize) -> Option<String> {
+    let mut out = BoundedString {
+        text: String::new(),
+        limit,
+    };
+    write_value(&mut out, value, 0, format).ok()?;
+    Some(out.text)
+}
+
 impl Format {
-    fn line(self, out: &mut String, indent: usize) {
+    fn line(self, out: &mut impl Write, indent: usize) -> fmt::Result {
         if self != Self::Compact {
-            out.push('\n');
+            out.write_char('\n')?;
             for _ in 0..indent {
-                out.push(' ');
+                out.write_char(' ')?;
             }
         }
+        Ok(())
     }
 }
 
-fn write_value(out: &mut String, value: &Json, indent: usize, format: Format) {
+fn write_value(out: &mut impl Write, value: &Json, indent: usize, format: Format) -> fmt::Result {
     match value {
-        Json::Null => out.push_str("null"),
-        Json::Bool(true) => out.push_str("true"),
-        Json::Bool(false) => out.push_str("false"),
-        Json::Number(number) => out.push_str(number),
+        Json::Null => out.write_str("null"),
+        Json::Bool(true) => out.write_str("true"),
+        Json::Bool(false) => out.write_str("false"),
+        Json::Number(number) => out.write_str(number),
         Json::Str(text) => write_string(out, text),
         Json::Array(items) => {
-            out.push('[');
+            out.write_char('[')?;
             for (i, item) in items.iter().enumerate() {
                 if i > 0 {
-                    out.push(',');
+                    out.write_char(',')?;
                 }
-                format.line(out, indent + 2);
-                write_value(out, item, indent + 2, format);
+                format.line(out, indent + 2)?;
+                write_value(out, item, indent + 2, format)?;
             }
             if !items.is_empty() {
-                format.line(out, indent);
+                format.line(out, indent)?;
             }
-            out.push(']');
+            out.write_char(']')
         }
         Json::Object(pairs) => {
             if format == Format::Sorted && pairs.len() > 1 {
                 let mut ordered: Vec<_> = pairs.iter().collect();
                 ordered.sort_by(|a, b| a.0.cmp(&b.0));
-                write_pairs(out, ordered.into_iter(), indent, format);
+                write_pairs(out, ordered.into_iter(), indent, format)
             } else {
-                write_pairs(out, pairs.iter(), indent, format);
+                write_pairs(out, pairs.iter(), indent, format)
             }
         }
     }
 }
 
 fn write_pairs<'a>(
-    out: &mut String,
+    out: &mut impl Write,
     pairs: impl ExactSizeIterator<Item = &'a (String, Json)>,
     indent: usize,
     format: Format,
-) {
+) -> fmt::Result {
     let nonempty = pairs.len() != 0;
-    out.push('{');
+    out.write_char('{')?;
     for (i, (key, value)) in pairs.enumerate() {
         if i > 0 {
-            out.push(',');
+            out.write_char(',')?;
         }
-        format.line(out, indent + 2);
-        write_string(out, key);
-        out.push(':');
+        format.line(out, indent + 2)?;
+        write_string(out, key)?;
+        out.write_char(':')?;
         if format != Format::Compact {
-            out.push(' ');
+            out.write_char(' ')?;
         }
-        write_value(out, value, indent + 2, format);
+        write_value(out, value, indent + 2, format)?;
     }
     if nonempty {
-        format.line(out, indent);
+        format.line(out, indent)?;
     }
-    out.push('}');
+    out.write_char('}')
 }
 
-fn write_string(out: &mut String, s: &str) {
-    out.push('"');
+fn write_string(out: &mut impl Write, s: &str) -> fmt::Result {
+    out.write_char('"')?;
     for ch in s.chars() {
         match ch {
-            '"' => out.push_str("\\\""),
-            '\\' => out.push_str("\\\\"),
-            '\n' => out.push_str("\\n"),
-            '\r' => out.push_str("\\r"),
-            '\t' => out.push_str("\\t"),
-            '\u{0008}' => out.push_str("\\b"),
-            '\u{000C}' => out.push_str("\\f"),
+            '"' => out.write_str("\\\""),
+            '\\' => out.write_str("\\\\"),
+            '\n' => out.write_str("\\n"),
+            '\r' => out.write_str("\\r"),
+            '\t' => out.write_str("\\t"),
+            '\u{0008}' => out.write_str("\\b"),
+            '\u{000C}' => out.write_str("\\f"),
             c if (c as u32) < 0x20 => {
-                let _ = write!(out, "\\u{:04x}", c as u32);
+                write!(out, "\\u{:04x}", c as u32)
             }
-            c if (c as u32) < 0x7F => out.push(c),
+            c if (c as u32) < 0x7F => out.write_char(c),
             c => {
                 // ensure_ascii: emit \uXXXX (surrogate pair for astral planes).
                 let cp = c as u32;
                 if cp <= 0xFFFF {
-                    let _ = write!(out, "\\u{:04x}", cp);
+                    write!(out, "\\u{:04x}", cp)
                 } else {
                     let v = cp - 0x10000;
                     let hi = 0xD800 + (v >> 10);
                     let lo = 0xDC00 + (v & 0x3FF);
-                    let _ = write!(out, "\\u{:04x}\\u{:04x}", hi, lo);
+                    write!(out, "\\u{:04x}\\u{:04x}", hi, lo)
                 }
             }
-        }
+        }?;
     }
-    out.push('"');
+    out.write_char('"')
 }
diff --git a/decompiler/crates/kuna-cli/src/jsonfmt/writer_tests.rs b/decompiler/crates/kuna-cli/src/jsonfmt/writer_tests.rs
index 6710e12a..ef90468c 100644
--- a/decompiler/crates/kuna-cli/src/jsonfmt/writer_tests.rs
+++ b/decompiler/crates/kuna-cli/src/jsonfmt/writer_tests.rs
@@ -94,3 +94,21 @@ fn every_unicode_scalar_round_trips_through_ascii_output() {
         assert_eq!(serde_json::from_str::<String>(&output).unwrap(), text);
     }
 }
+
+#[test]
+fn bounded_writer_counts_actual_escaped_bytes_at_every_boundary() {
+    let value = Json::Object(vec![("escaped".into(), Json::Str("\0\"\\é😀".into()))]);
+    let complete = dumps_compact(&value);
+    assert!(complete.is_ascii());
+    for limit in 0..complete.len() {
+        assert!(dumps_compact_bounded(&value, limit).is_none());
+    }
+    assert_eq!(
+        dumps_compact_bounded(&value, complete.len()),
+        Some(complete.clone())
+    );
+    assert_eq!(
+        dumps_compact_bounded(&value, complete.len() + 1),
+        Some(complete)
+    );
+}
diff --git a/decompiler/crates/kuna-cli/src/main.rs b/decompiler/crates/kuna-cli/src/main.rs
index 2345743c..3da94435 100644
--- a/decompiler/crates/kuna-cli/src/main.rs
+++ b/decompiler/crates/kuna-cli/src/main.rs
@@ -1,6 +1,8 @@
 //! Command dispatch for the kuna CLI.
 
 mod args;
+mod atomic_json;
+mod atomic_compression;
 mod callgraph;
 mod catalog;
 mod crypto;
diff --git a/decompiler/crates/kuna-cli/src/project_stream.rs b/decompiler/crates/kuna-cli/src/project_stream.rs
index e40b18c9..b8cae233 100644
--- a/decompiler/crates/kuna-cli/src/project_stream.rs
+++ b/decompiler/crates/kuna-cli/src/project_stream.rs
@@ -858,6 +858,7 @@ fn export(
         // every function of the export.
         single_target: false,
         want_tokens: false,
+        want_atomic_facts: false,
         want_pointer_arguments: false,
     };
 
diff --git a/decompiler/crates/kuna-console/src/inspect.rs b/decompiler/crates/kuna-console/src/inspect.rs
index 74024b10..a41465a6 100644
--- a/decompiler/crates/kuna-console/src/inspect.rs
+++ b/decompiler/crates/kuna-console/src/inspect.rs
@@ -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 +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) {
-            return FuncDetail { tokens: Vec::new(), tokens_error: Some(error) };
+            return FuncDetail { tokens: Vec::new(), tokens_error: Some(error), ..Default::default() };
         }
         for t in &mut tokens {
             t.address = t.address.map(|a| prog.output_code_offset(a));
             t.callee = t.callee.map(|a| prog.output_code_offset(a));
         }
-        FuncDetail { tokens, tokens_error: None }
+        FuncDetail { tokens, tokens_error: None, ..Default::default() }
     }
 }
 
diff --git a/decompiler/crates/kuna-console/src/project.rs b/decompiler/crates/kuna-console/src/project.rs
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 {
     /// Capture the token source map ([`FuncResult::detail`]); implies the
     /// provenance render.
     pub want_tokens: bool,
+    /// Retain the read-only recovered IR from the same function instance.
+    pub want_atomic_facts: bool,
     /// Record [`FuncResult::pointerargs`] for a buffered driver. A batch that
     /// returns its results ([`decompile_targets_with`]) reconciles them itself;
     /// a pulled caller owns that step.
@@ -278,6 +280,7 @@ pub fn decompile_targets(
         park_recovered_proto: false,
         single_target: targets.len() == 1,
         want_tokens: false,
+        want_atomic_facts: false,
         want_pointer_arguments: false,
     };
     decompile_batch(prog, targets, &opts)
@@ -321,6 +324,7 @@ pub fn export_options(single_target: bool) -> DecompileOptions {
         park_recovered_proto: false,
         single_target,
         want_tokens: false,
+        want_atomic_facts: false,
         want_pointer_arguments: true,
     }
 }
@@ -509,6 +513,7 @@ pub fn decompile_pulled(
         header_carries_types,
         single_target,
         want_tokens,
+        want_atomic_facts,
         want_pointer_arguments,
         ..
     } = *opts;
@@ -838,11 +843,23 @@ pub fn decompile_pulled(
                         }
                     }
                     let var_refs = provenance.apply_to_variables_with_refs(&fd, &mut variables);
-                    let detail = want_tokens.then(|| {
+                    let mut detail = want_tokens.then(|| {
                         Box::new(crate::inspect::FuncDetail::resolve(
                             prog, &fd, &var_refs, &raw_tokens, &untrimmed, &code, &variables,
                         ))
                     });
+                    if want_atomic_facts {
+                        let detail = detail.get_or_insert_with(Default::default);
+                        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)
+                            .and_then(|m| kuna_decomp::atomic_projection::collect(prog.arch(), &fd, m)));
+                    }
                     for variable in &mut variables {
                         for address in &mut variable.addresses {
                             *address = prog.output_code_offset(*address);
diff --git a/decompiler/crates/kuna-decomp/Cargo.toml b/decompiler/crates/kuna-decomp/Cargo.toml
index 40b093b6..8f03b654 100644
--- a/decompiler/crates/kuna-decomp/Cargo.toml
+++ b/decompiler/crates/kuna-decomp/Cargo.toml
@@ -15,11 +15,11 @@ kuna-sleigh.workspace = true
 thiserror.workspace = true
 smallvec.workspace = true
 slotmap.workspace = true
+serde = { version = "1", features = ["derive"] }
 
 [dev-dependencies]
 # Verifier-only: the datatest <stringmatch> engine (item w10-structure-printbody).
 regex = { workspace = true }
-serde = { version = "1", features = ["derive"] }
 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
--- /dev/null
+++ b/decompiler/crates/kuna-decomp/src/substrate/atomic_calls.rs
@@ -0,0 +1,216 @@
+//! Recovered call relations. Argument values and passing storage are separate.
+use crate::{
+    atomic_membership::{Membership, MAX_CALLS},
+    atomic_values::{self, operation_id, value_id, ValueFact},
+    context::OpId,
+    fspec::{FuncCallSpecs, OFFSET_UNKNOWN},
+    funcdata::Funcdata,
+};
+use kuna_base::address::Address;
+use serde::Serialize;
+use std::collections::{BTreeSet, HashMap};
+
+#[derive(Debug, Clone, Serialize)]
+pub struct CallFacts {
+    pub schema_version: u32,
+    pub items: Vec<CallFact>,
+    pub values: Vec<ValueFact>,
+    pub coverage: CallCoverage,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct CallCoverage {
+    pub scope: &'static str,
+    pub blocks_examined: i32,
+    pub operations_examined: usize,
+    pub value_scope: &'static str,
+    pub machine_call_equivalence: &'static str,
+}
+
+pub fn collect_all(fd: &Funcdata, membership: &Membership) -> Result<CallFacts, String> {
+    const MAX_VALUES: usize = 36_000;
+    const MAX_INPUTS: usize = 50_000;
+    if fd.bblocks_get_size() <= 0 {
+        return Err("recovered block membership is unavailable".into());
+    }
+    if fd.num_calls() < 0 || fd.num_calls() as usize > MAX_CALLS {
+        return Err("atomic call-spec capacity exceeded".into());
+    }
+    let mut specs = HashMap::new();
+    for i in 0..fd.num_calls() {
+        let spec = fd.get_call_specs(i);
+        if specs.insert(spec.get_op(), spec).is_some() {
+            return Err("duplicate native call-spec operation".into());
+        }
+    }
+    let mut items = Vec::new();
+    let mut keys = BTreeSet::new();
+    let mut inputs = 0usize;
+    let mut text = atomic_values::TextBudget::new(2 * 1024 * 1024);
+    for &key in &membership.calls {
+        let op = fd.obank().get(key).ok_or("stale call operation")?;
+        inputs = inputs
+            .checked_add(op.num_input() as usize)
+            .ok_or("atomic call input count overflow")?;
+        if inputs > MAX_INPUTS {
+            return Err("atomic call input capacity exceeded".into());
+        }
+        let spec = specs.get(&key).copied();
+        if let Some(spec) = spec {
+            text.charge(spec.get_name().len())?;
+            if spec.proto().has_model() {
+                text.charge(spec.proto().get_model_name().len())?;
+            }
+        }
+        for index in 0..op.num_input() {
+            if let Some(v) = op.get_in(index) {
+                keys.insert(v);
+            }
+        }
+        if let Some(v) = op.get_out() {
+            keys.insert(v);
+        }
+        if keys.len() > MAX_VALUES {
+            return Err("atomic call value capacity exceeded".into());
+        }
+        items.push(collect(fd, key, spec)?);
+    }
+    let values = atomic_values::collect(fd, keys, &mut text)?;
+    Ok(CallFacts {
+        schema_version: 1, items, values,
+        coverage: CallCoverage {
+            scope: "all recovered block-member CALL/CALLIND operations",
+            blocks_examined: membership.blocks_examined, operations_examined: membership.operations_examined,
+            value_scope: "call inputs including target and outputs only; definitions may be outside this facet",
+            machine_call_equivalence: "unknown",
+        },
+    })
+}
+
+#[derive(Debug, Clone, Serialize)]
+pub struct Location {
+    pub space: String,
+    pub offset: String,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct Storage {
+    #[serde(flatten)]
+    pub location: Location,
+    pub size_bytes: i32,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct Argument {
+    pub input_index: i32,
+    pub value_id: Option<String>,
+    pub storage: Option<Storage>,
+    pub storage_authority: Option<&'static str>,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct Prototype {
+    pub model: Option<String>,
+    pub model_unknown: Option<bool>,
+    pub inputs_locked: bool,
+    pub variadic: bool,
+    pub parameter_shift: i32,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct CallFact {
+    pub id: String,
+    pub origin_address: String,
+    pub block: i32,
+    pub opcode: String,
+    pub is_dead: bool,
+    pub target_value_id: Option<String>,
+    pub spec_available: bool,
+    pub target: Option<Location>,
+    pub target_name: Option<String>,
+    pub arguments: Vec<Argument>,
+    pub output: Option<String>,
+    pub prototype: Option<Prototype>,
+    pub stack_offset: Option<String>,
+}
+fn location(address: &Address) -> Option<Location> {
+    address.get_space().map(|space| Location {
+        space: space.get_name().to_string(),
+        offset: format!("0x{:x}", address.get_offset()),
+    })
+}
+fn storage(address: &Address, size_bytes: i32) -> Option<Storage> {
+    if size_bytes <= 0 {
+        return None;
+    }
+    location(address).map(|location| Storage {
+        location,
+        size_bytes,
+    })
+}
+
+fn collect(fd: &Funcdata, key: OpId, spec: Option<&FuncCallSpecs>) -> Result<CallFact, String> {
+    let op = fd.obank().get(key).ok_or("stale call operation")?;
+    let arguments = (1..op.num_input())
+        .map(|input_index| {
+            // The native owner stores finalized passing locations separately
+            // from SSA values. Admit that mapping only with matching arity.
+            // Placeholder/shifted inputs are not source parameter ordinals.
+            let binding = spec.and_then(|spec| {
+                if spec.get_paramshift() != 0 || spec.get_stack_placeholder_slot() == input_index {
+                    return None;
+                }
+                if spec.final_input_storage().len() + 1 == op.num_input() as usize {
+                    let (address, size) = &spec.final_input_storage()[(input_index - 1) as usize];
+                    return storage(address, *size).map(|s| (s, "final-input-storage"));
+                }
+                let proto = spec.proto();
+                if proto.has_store() && proto.is_input_locked() {
+                    return proto.get_param(input_index - 1).and_then(|param| {
+                        storage(&param.get_address(), param.get_size())
+                            .map(|s| (s, "locked-prototype"))
+                    });
+                }
+                None
+            });
+            let (storage, storage_authority) = match binding {
+                Some((s, authority)) => (Some(s), Some(authority)),
+                None => (None, None),
+            };
+            Argument {
+                input_index,
+                value_id: op.get_in(input_index).map(value_id),
+                storage,
+                storage_authority,
+            }
+        })
+        .collect();
+    Ok(CallFact {
+        id: operation_id(fd, key)?,
+        origin_address: format!("0x{:x}", op.get_seq_num().get_addr().get_offset()),
+        block: fd
+            .bblocks_ref()
+            .block(op.get_parent().ok_or("call has no recovered block")?)
+            .get_index(),
+        opcode: format!("{:?}", op.code()),
+        is_dead: op.is_dead(),
+        target_value_id: op.get_in(0).map(value_id),
+        spec_available: spec.is_some(),
+        target: spec.and_then(|s| location(s.get_entry_address())),
+        target_name: spec
+            .and_then(|s| (!s.get_name().is_empty()).then(|| s.get_name().to_string())),
+        arguments,
+        output: op.get_out().map(value_id),
+        prototype: spec.map(|s| {
+            let proto = s.proto();
+            Prototype {
+                model: proto
+                    .has_model()
+                    .then(|| proto.get_model_name().to_string()),
+                model_unknown: proto.has_model().then(|| proto.is_model_unknown()),
+                inputs_locked: proto.is_input_locked(),
+                variadic: proto.is_dotdotdot(),
+                parameter_shift: s.get_paramshift(),
+            }
+        }),
+        stack_offset: spec.and_then(|s| {
+            (s.get_spacebase_offset() != OFFSET_UNKNOWN)
+                .then(|| format!("0x{:x}", s.get_spacebase_offset()))
+        }),
+    })
+}
diff --git a/decompiler/crates/kuna-decomp/src/substrate/atomic_facts.rs b/decompiler/crates/kuna-decomp/src/substrate/atomic_facts.rs
new file mode 100644
index 00000000..6b9afe69
--- /dev/null
+++ b/decompiler/crates/kuna-decomp/src/substrate/atomic_facts.rs
@@ -0,0 +1,156 @@
+//! Opt-in, read-only export of the recovered function IR for the REA experiment.
+//! IDs are local to this captured model; addresses alone are not SSA identities.
+use crate::{
+    architecture::Architecture,
+    atomic_membership::Membership,
+    atomic_operations::{OperationBudget, OperationFact},
+    atomic_values::{operation_id, value_id, ValueFact},
+    funcdata::Funcdata,
+};
+use kuna_num::opcodes::OpCode;
+use serde::Serialize;
+use std::collections::BTreeSet;
+
+#[derive(Debug, Clone, Serialize)]
+pub struct FunctionFacts {
+    pub schema_version: u32,
+    pub blocks: Vec<BlockFact>,
+    pub operations: Vec<OperationFact>,
+    pub values: Vec<ValueFact>,
+    pub coverage: Coverage,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct Coverage {
+    pub scope: &'static str,
+    pub machine_semantic_equivalence: &'static str,
+    pub indirect_branch_operations: Vec<String>,
+    pub omitted_definition_ids: Vec<String>,
+    pub issues: Vec<String>,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct BlockFact {
+    pub id: i32,
+    pub start: String,
+    pub operations: Vec<String>,
+    pub predecessors: Vec<i32>,
+    pub successors: Vec<EdgeFact>,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct EdgeFact {
+    pub id: String,
+    pub target: i32,
+    pub index: i32,
+    pub polarity: Option<&'static str>,
+    pub condition_value: Option<String>,
+    pub condition_test: Option<&'static str>,
+}
+pub fn collect(
+    arch: &Architecture,
+    fd: &Funcdata,
+    membership: &Membership,
+) -> Result<FunctionFacts, String> {
+    // Bounds cover allocations before JSON serialization, independently of the
+    // transport byte budget. Overflow is an unavailable facet, not clipped IR.
+    const MAX_OPERATIONS: usize = 32_000;
+    const MAX_VALUES: usize = 36_000;
+    const MAX_INPUTS: usize = 100_000;
+    const MAX_DISPLAY_BYTES: usize = 4 * 1024 * 1024;
+    const MAX_CFG_EDGES: usize = 50_000;
+    if fd.bblocks_get_size() <= 0 {
+        return Err("recovered basic-block graph is unavailable".into());
+    }
+    if fd.bblocks_get_size() > 12_000 {
+        return Err("atomic block capacity exceeded".into());
+    }
+    if membership.operations_examined > MAX_OPERATIONS {
+        return Err("atomic operation capacity exceeded".into());
+    }
+    let mut blocks = Vec::new();
+    let mut operations = Vec::new();
+    let mut retained_ops = BTreeSet::new();
+    let mut edge_count = 0usize;
+    let mut budget = OperationBudget::new(MAX_VALUES, MAX_INPUTS, MAX_DISPLAY_BYTES);
+    let mut coverage = Coverage {
+        scope: "complete native recovered basic-block graph; block-member operations",
+        machine_semantic_equivalence: "unknown",
+        indirect_branch_operations: Vec::new(),
+        omitted_definition_ids: Vec::new(),
+        issues: Vec::new(),
+    };
+    for block_index in 0..fd.bblocks_get_size() {
+        let block_key = fd.bblocks_get_block(block_index);
+        let block = fd.bblocks_ref().block(block_key);
+        let members = fd.bb_ops(block_key);
+        if members.len() > MAX_OPERATIONS - operations.len() {
+            return Err("atomic operation capacity exceeded".into());
+        }
+        edge_count = edge_count
+            .checked_add(block.size_out() as usize)
+            .ok_or("atomic CFG edge count overflow")?;
+        if edge_count > MAX_CFG_EDGES {
+            return Err("atomic CFG edge capacity exceeded".into());
+        }
+        let tail = members.last().and_then(|id| fd.obank().get(*id));
+        let conditional =
+            tail.filter(|op| op.code() == OpCode::CPUI_CBRANCH && block.size_out() == 2);
+        let condition_value = conditional.and_then(|op| op.get_in(1)).map(value_id);
+        let condition_test = conditional.map(|op| {
+            if op.is_boolean_flip() {
+                "eq-zero"
+            } else {
+                "ne-zero"
+            }
+        });
+        let successors = (0..block.size_out())
+            .map(|i| EdgeFact {
+                id: format!("{}:{i}", block.get_index()),
+                target: fd.bblocks_ref().block(block.get_out(i)).get_index(),
+                index: i,
+                polarity: conditional.map(|_| if i == 0 { "false" } else { "true" }),
+                condition_value: condition_value.clone(),
+                condition_test,
+            })
+            .collect();
+        blocks.push(BlockFact {
+            id: block.get_index(),
+            start: format!("0x{:x}", fd.bblocks_block_start(block_key).get_offset()),
+            operations: members
+                .iter()
+                .map(|id| operation_id(fd, *id))
+                .collect::<Result<_, _>>()?,
+            predecessors: (0..block.size_in())
+                .map(|i| fd.bblocks_ref().block(block.get_in(i)).get_index())
+                .collect(),
+            successors,
+        });
+        for key in members {
+            if operations.len() >= MAX_OPERATIONS {
+                return Err("atomic operation capacity exceeded".into());
+            }
+            let op = budget.collect(arch, fd, key)?;
+            if !retained_ops.insert(op.id.clone()) {
+                return Err("operation belongs to multiple recovered blocks".into());
+            }
+            if op.opcode == "CPUI_BRANCHIND" {
+                coverage.indirect_branch_operations.push(op.id.clone());
+            }
+            operations.push(op);
+        }
+    }
+    let values = budget.values(fd)?;
+    coverage.issues = budget.issues;
+    let missing: BTreeSet<_> = values
+        .iter()
+        .filter_map(|v| v.definition.as_ref())
+        .filter(|id| !retained_ops.contains(*id))
+        .cloned()
+        .collect();
+    coverage.omitted_definition_ids = missing.into_iter().collect();
+    Ok(FunctionFacts {
+        schema_version: 3,
+        blocks,
+        operations,
+        values,
+        coverage,
+    })
+}
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..be11e472
--- /dev/null
+++ b/decompiler/crates/kuna-decomp/src/substrate/atomic_membership.rs
@@ -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,
+}
+pub fn inspect(fd: &Funcdata) -> Result<Membership, String> {
+    if fd.bblocks_get_size() <= 0 {
+        return Err("recovered block membership is unavailable".into());
+    }
+    let mut result = Membership {
+        calls: Vec::new(),
+        switches: Some(Vec::new()),
+        members: Some(HashSet::new()),
+        blocks_examined: fd.bblocks_get_size(),
+        operations_examined: 0,
+    };
+    for i in 0..fd.bblocks_get_size() {
+        let block = fd.bblocks_get_block(i);
+        let expected = fd.bb_op_len(block);
+        let mut examined = 0;
+        let mut cursor = fd.bb_op_head(block);
+        while let Some(key) = cursor {
+            if examined >= expected {
+                return Err("cyclic native block operation list".into());
+            }
+            examined += 1;
+            result.operations_examined = result
+                .operations_examined
+                .checked_add(1)
+                .ok_or("native operation count overflow")?;
+            let op = fd.obank().get(key).ok_or("stale block operation")?;
+            if op.get_parent() != Some(block) {
+                return Err("native block ownership mismatch".into());
+            }
+            cursor = op.basic_neighbours().1;
+            if let Some(members) = result.members.as_mut() {
+                if members.len() == MAX_INDEXED_OPERATIONS {
+                    result.members = None;
+                } else if !members.insert(key) {
+                    return Err("operation belongs to multiple recovered blocks".into());
+                }
+            }
+            if matches!(op.code(), OpCode::CPUI_CALL | OpCode::CPUI_CALLIND) {
+                if result.calls.len() >= MAX_CALLS {
+                    return Err("atomic call capacity exceeded".into());
+                }
+                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());
+        }
+    }
+    Ok(result)
+}
diff --git a/decompiler/crates/kuna-decomp/src/substrate/atomic_operations.rs b/decompiler/crates/kuna-decomp/src/substrate/atomic_operations.rs
new file mode 100644
index 00000000..30d6be39
--- /dev/null
+++ b/decompiler/crates/kuna-decomp/src/substrate/atomic_operations.rs
@@ -0,0 +1,119 @@
+//! Shared read-only operation/value normalization for full and selected facts.
+use crate::{
+    architecture::Architecture,
+    atomic_values::{self, operation_id, value_id, ValueFact},
+    context::{OpId, VarnodeId},
+    funcdata::Funcdata,
+};
+use kuna_num::opcodes::OpCode;
+use serde::Serialize;
+use std::collections::BTreeSet;
+
+#[derive(Debug, Clone, Serialize)]
+pub struct OperationFact {
+    pub id: String,
+    pub address: String,
+    pub block: i32,
+    pub opcode: String,
+    pub statement: String,
+    pub is_dead: bool,
+    pub inputs: Vec<InputFact>,
+    pub output: Option<String>,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct InputFact {
+    pub input_index: i32,
+    pub value_id: Option<String>,
+    pub phi_predecessor: Option<i32>,
+    pub phi_predecessor_edge: Option<String>,
+}
+pub struct OperationBudget {
+    max_values: usize,
+    max_inputs: usize,
+    keys: BTreeSet<VarnodeId>,
+    input_count: usize,
+    text: atomic_values::TextBudget,
+    pub issues: Vec<String>,
+}
+impl OperationBudget {
+    pub fn new(max_values: usize, max_inputs: usize, max_display: usize) -> Self {
+        Self {
+            max_values,
+            max_inputs,
+            keys: BTreeSet::new(),
+            input_count: 0,
+            text: atomic_values::TextBudget::new(max_display),
+            issues: Vec::new(),
+        }
+    }
+    pub fn collect(
+        &mut self,
+        arch: &Architecture,
+        fd: &Funcdata,
+        key: OpId,
+    ) -> Result<OperationFact, String> {
+        let op = fd.obank().get(key).ok_or("stale operation")?;
+        let parent = op.get_parent().ok_or("operation has no recovered block")?;
+        let block = fd.bblocks_ref().block(parent);
+        let id = operation_id(fd, key)?;
+        if op.num_input() < 0 {
+            return Err("negative native input count".into());
+        }
+        self.input_count = self
+            .input_count
+            .checked_add(op.num_input() as usize)
+            .ok_or("atomic input count overflow")?;
+        if self.input_count > self.max_inputs {
+            return Err("atomic input-edge capacity exceeded".into());
+        }
+        let phi = op.code() == OpCode::CPUI_MULTIEQUAL;
+        let phi_bound = phi && block.size_in() == op.num_input();
+        if phi && !phi_bound {
+            self.issues
+                .push(format!("{id}: phi/predecessor count mismatch"));
+        }
+        let inputs = (0..op.num_input())
+            .map(|index| {
+                let value = op.get_in(index);
+                if let Some(v) = value {
+                    self.keys.insert(v);
+                }
+                InputFact {
+                    input_index: index,
+                    value_id: value.map(value_id),
+                    phi_predecessor: phi_bound
+                        .then(|| fd.bblocks_ref().block(block.get_in(index)).get_index()),
+                    phi_predecessor_edge: phi_bound.then(|| {
+                        format!(
+                            "{}:{}",
+                            fd.bblocks_ref().block(block.get_in(index)).get_index(),
+                            block.get_in_rev_index(index)
+                        )
+                    }),
+                }
+            })
+            .collect();
+        if let Some(v) = op.get_out() {
+            self.keys.insert(v);
+        }
+        if self.keys.len() > self.max_values {
+            return Err("atomic value capacity exceeded".into());
+        }
+        let mut statement = String::new();
+        crate::funcdata_printraw::render_op(&mut statement, arch, fd, key)?;
+        self.text.charge(statement.len())?;
+        Ok(OperationFact {
+            id,
+            address: format!("0x{:x}", op.get_seq_num().get_addr().get_offset()),
+            block: block.get_index(),
+            opcode: format!("{:?}", op.code()),
+            statement,
+            is_dead: op.is_dead(),
+            inputs,
+            output: op.get_out().map(value_id),
+        })
+    }
+    pub fn values(&mut self, fd: &Funcdata) -> Result<Vec<ValueFact>, String> {
+        atomic_values::collect(fd, std::mem::take(&mut self.keys), &mut self.text)
+    }
+}
diff --git a/decompiler/crates/kuna-decomp/src/substrate/atomic_projection.rs b/decompiler/crates/kuna-decomp/src/substrate/atomic_projection.rs
new file mode 100644
index 00000000..097b153a
--- /dev/null
+++ b/decompiler/crates/kuna-decomp/src/substrate/atomic_projection.rs
@@ -0,0 +1,117 @@
+//! Bounded backward SSA facts, independent of full CFG export availability.
+use crate::{
+    architecture::Architecture,
+    atomic_membership::Membership,
+    atomic_operations::{OperationBudget, OperationFact},
+    atomic_values::{operation_id, ValueFact},
+    funcdata::Funcdata,
+};
+use serde::Serialize;
+use std::collections::{BTreeMap, HashSet, VecDeque};
+
+#[derive(Debug, Clone, Serialize)]
+pub struct Projection {
+    pub schema_version: u32,
+    pub roots: Vec<String>,
+    pub operations: Vec<OperationFact>,
+    pub values: Vec<ValueFact>,
+    pub coverage: Coverage,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct Frontier {
+    pub definition: String,
+    pub reason: &'static str,
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct Coverage {
+    pub scope: &'static str,
+    pub operation_budget: usize,
+    pub frontier: Vec<Frontier>,
+    pub issues: Vec<String>,
+    pub machine_semantic_equivalence: &'static str,
+}
+pub fn collect(
+    arch: &Architecture,
+    fd: &Funcdata,
+    membership: &Membership,
+) -> Result<Projection, String> {
+    const MAX_OPERATIONS: usize = 4096;
+    let members = membership
+        .members
+        .as_ref()
+        .ok_or("projection membership-index capacity exceeded")?;
+    if membership.calls.len() > MAX_OPERATIONS {
+        return Err("projection call-root capacity exceeded".into());
+    }
+    let roots = membership
+        .calls
+        .iter()
+        .map(|key| operation_id(fd, *key))
+        .collect::<Result<Vec<_>, _>>()?;
+    let mut queue: VecDeque<_> = membership.calls.iter().copied().collect();
+    let mut queued: HashSet<_> = membership.calls.iter().copied().collect();
+    let mut retained = HashSet::new();
+    let mut operations = Vec::new();
+    let mut budget = OperationBudget::new(12_288, 16_384, 2 * 1024 * 1024);
+    while let Some(key) = queue.pop_front() {
+        if !members.contains(&key) {
+            continue;
+        }
+        if retained.len() == MAX_OPERATIONS {
+            break;
+        }
+        if !retained.insert(key) {
+            continue;
+        }
+        operations.push(budget.collect(arch, fd, key)?);
+        let op = fd.obank().get(key).ok_or("stale projection operation")?;
+        for i in 0..op.num_input() {
+            if let Some(value) = op.get_in(i) {
+                let value = fd.vbank().get(value).ok_or("stale projection operand")?;
+                if let Some(definition) = value.get_def() {
+                    if queued.insert(definition) {
+                        queue.push_back(definition);
+                    }
+                }
+            }
+        }
+    }
+    let values = budget.values(fd)?;
+    let retained_ids: HashSet<_> = operations.iter().map(|op| op.id.as_str()).collect();
+    let mut reasons = BTreeMap::new();
+    for key in queued.difference(&retained) {
+        reasons.insert(
+            operation_id(fd, *key)?,
+            if members.contains(key) {
+                "operation-budget"
+            } else {
+                "outside-recovered-membership"
+            },
+        );
+    }
+    let missing: HashSet<_> = values
+        .iter()
+        .filter_map(|v| v.definition.as_ref())
+        .filter(|id| !retained_ids.contains(id.as_str()))
+        .cloned()
+        .collect();
+    let frontier = reasons
+        .into_iter()
+        .filter(|(id, _)| missing.contains(id))
+        .map(|(definition, reason)| Frontier { definition, reason })
+        .collect();
+    Ok(Projection {
+        schema_version: 1,
+        roots,
+        operations,
+        values,
+        coverage: Coverage {
+            scope:
+                "call-rooted bounded backward SSA definitions; not a CFG or complete use inventory",
+            operation_budget: MAX_OPERATIONS,
+            frontier,
+            issues: budget.issues,
+            machine_semantic_equivalence: "unknown",
+        },
+    })
+}
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
--- /dev/null
+++ b/decompiler/crates/kuna-decomp/src/substrate/atomic_values.rs
@@ -0,0 +1,80 @@
+//! One read-only interpretation of native value and operation identities.
+use crate::{
+    context::{OpId, VarnodeId},
+    funcdata::Funcdata,
+};
+use serde::Serialize;
+use slotmap::Key;
+use std::collections::BTreeSet;
+
+pub struct TextBudget {
+    used: usize,
+    limit: usize,
+}
+impl TextBudget {
+    pub fn new(limit: usize) -> Self {
+        Self { used: 0, limit }
+    }
+    pub fn charge(&mut self, bytes: usize) -> Result<(), String> {
+        let next = self
+            .used
+            .checked_add(bytes)
+            .ok_or("atomic text count overflow")?;
+        if next > self.limit {
+            return Err("atomic text capacity exceeded".into());
+        }
+        self.used = next;
+        Ok(())
+    }
+}
+#[derive(Debug, Clone, Serialize)]
+pub struct ValueFact {
+    pub id: String,
+    pub space: Option<String>,
+    pub offset: String,
+    pub size_bytes: i32,
+    pub is_constant: bool,
+    pub is_input: bool,
+    pub is_annotation: bool,
+    pub definition: Option<String>,
+    pub type_name: String,
+}
+pub fn value_id(id: VarnodeId) -> String {
+    format!("v{:x}", id.data().as_ffi())
+}
+pub fn operation_id(fd: &Funcdata, id: OpId) -> Result<String, String> {
+    let operation = fd.obank().get(id).ok_or("stale operation identity")?;
+    let seq = operation.get_seq_num();
+    Ok(format!(
+        "0x{:x}:{:x}",
+        seq.get_addr().get_offset(),
+        seq.get_time()
+    ))
+}
+pub fn collect(
+    fd: &Funcdata,
+    keys: BTreeSet<VarnodeId>,
+    text: &mut TextBudget,
+) -> Result<Vec<ValueFact>, String> {
+    let mut values = Vec::with_capacity(keys.len());
+    for key in keys {
+        let value = fd.vbank().get(key).ok_or("stale input/output value")?;
+        let type_name = value.get_type().get_name();
+        text.charge(type_name.len())?;
+        values.push(ValueFact {
+            id: value_id(key),
+            space: value
+                .get_addr()
+                .get_space()
+                .map(|s| s.get_name().to_string()),
+            offset: format!("0x{:x}", value.get_offset()),
+            size_bytes: value.get_size(),
+            is_constant: value.is_constant(),
+            is_input: value.is_input(),
+            is_annotation: value.is_annotation(),
+            definition: value.get_def().map(|id| operation_id(fd, id)).transpose()?,
+            type_name: type_name.to_string(),
+        });
+    }
+    Ok(values)
+}
diff --git a/decompiler/crates/kuna-decomp/src/substrate/funcdata_printraw.rs b/decompiler/crates/kuna-decomp/src/substrate/funcdata_printraw.rs
index 39927ceb..844950a6 100644
--- a/decompiler/crates/kuna-decomp/src/substrate/funcdata_printraw.rs
+++ b/decompiler/crates/kuna-decomp/src/substrate/funcdata_printraw.rs
@@ -376,7 +376,7 @@ fn callother_operator_name(
 /// dispatch.  The special op-codes (LOAD/STORE/branches/calls/RETURN/marker)
 /// match their `TypeOp*::printRaw` override; everything else falls to the
 /// generic Binary/Unary/Func shape keyed by the [`TypeOpClass`].
-fn render_op(s: &mut String, arch: &Architecture, fd: &Funcdata, op: OpId) -> Result<(), String> {
+pub(crate) fn render_op(s: &mut String, arch: &Architecture, fd: &Funcdata, op: OpId) -> Result<(), String> {
     let opc = fd.obank().get(op).ok_or_else(|| "render_op: stale op".to_string())?.code();
     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..d3f422ee 100644
--- a/decompiler/crates/kuna-decomp/src/substrate/mod.rs
+++ b/decompiler/crates/kuna-decomp/src/substrate/mod.rs
@@ -11,6 +11,13 @@ pub mod funcdata_block;
 pub mod funcdata_encode;
 pub mod funcdata_op;
 pub mod funcdata_printraw;
+pub mod atomic_facts;
+pub mod atomic_calls;
+pub mod atomic_membership;
+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..9d927aa5 100644
--- a/docs/spec/00-overview.md
+++ b/docs/spec/00-overview.md
@@ -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
+collect these records. This experiment requires embedded processor specs and
+selects those assets explicitly; a caller-provided `--sleighpath` is rejected.
+
+The export retains ordered basic-block predecessors and successors, slotmap
+value identities, operation sequence identities, operand indexes, outputs and
+phi input-to-predecessor-edge bindings. IDs belong to this captured function
+model; instruction addresses are origins, not SSA value identities. Native
+recovered graph completeness does not establish runtime successor coverage,
+memory alias dependencies or machine-semantic equivalence. Indirect-branch
+operations and definitions outside block membership remain explicit. Capacity
+failures make this facet unavailable with a reason and preserve the C record;
+they do not emit a clipped graph labeled complete.
+
+`--atomic-output-bytes N` sets the encoded document budget (default 8 MiB).
+Atomic JSON uses the ordinary record producer and the shared compact ASCII-safe
+writer. That writer checks each encoded write before growing its bounded output
+buffer, including control/surrogate escaping and the final newline. A document
+that cannot fit omits unavailable recovered facets with named errors and
+retains C, locations and ordinary metadata. If that base record also cannot fit,
+the command reports failure instead of truncating it or analyzing the target
+again. This flag requires `--atomic-facts --json`; ordinary output is unchanged.
+
+Graph schema version 3 and an independent `atomic_calls` version-1 facet are
+captured from the same live function after C rendering. The call facet scans
+all native block members without allocating a copy of every block's operations;
+it has its own call/input/value/text limits. Full-graph capacity failure leaves
+calls and their boundary values available. Shared value extraction owns the
+native value identities, flags, widths and definitions; boundary values do not
+claim a complete function value/definition graph.
+
+`FuncCallSpecs` supplies recovered targets, names, prototype flags and passing
+storage. Target input zero remains an SSA value (often an fspec annotation),
+never a callee code address. CALLIND targets can remain unknown. Storage uses
+matching-arity finalized locations or locked prototype storage; shifted inputs
+and placeholders stay unknown. Input slots are not source parameter ordinals.
+
+The encoded writer attempts bounded facet alternatives without cloning their
+contents. A raw schema-3 graph that fits keeps its existing format. Before
+dropping useful facts, an oversized graph can use a schema-4 envelope with
+`encoding: "gzip-base64"`, the exact `raw_bytes` and canonical padded `data`.
+Its decompressed JSON is the unchanged logical schema-3 graph. Raw encoding
+stops at 32 MiB; compressed output, base64 expansion and envelope overhead are
+bounded before allocation against the caller's encoded budget. All graphs in a
+document share that encoded budget. Optional compression does not analyze again.
+The independent full-graph row limits are 32,000 operations, 36,000 values,
+100,000 inputs, 4 MiB display/type text, 12,000 blocks and 50,000 CFG edges.
+They bound construction separately from wire size; exceeding them is unavailable,
+not a complete clipped graph. C and independent calls keep their own contracts.
+A full graph omits its redundant operation projection; if encoded
+capacity makes that graph unavailable, the independent projection is restored.
+A fitting graph has priority, then fitting calls, then the projection. Failed
+facets retain named errors. If C itself cannot fit, output fails explicitly
+without reanalysis. Facet errors do not fabricate empty collections or change C.
+
+`atomic_membership.rs` owns one checked scan of recovered block membership and
+call roots. Its optional index is bounded at 65,536 native operation keys; calls
+remain readable beyond that index budget. `atomic_operations.rs` normalizes
+operands, phi bindings, origins, outputs, display and values for both full and
+selected exports. Full-graph operation capacity is checked before materializing
+its rows, after the common scan.
+
+The independent version-1 `atomic_projection` retains all recovered calls as
+roots, then follows backward operand definitions within a 4,096-operation,
+12,288-value, 16,384-input and 2 MiB text budget. Too many roots or unavailable
+membership make this facet unavailable. Omitted defining operations have exact
+IDs and `operation-budget` or `outside-recovered-membership` frontier reasons.
+This does not collect CFG or complete use lists, infer memory aliases, or prove
+runtime reachability. Collection uses the same live function after C rendering;
+no second decompilation is performed. Complete source Evidence keeps the native
+frontier while callers may select a compact summary and individual facts.