mirror/rea
1
0
Fork 0
mirror of https://github.com/morluto/rea synced 2026-10-28 15:07:26 -04:00
Code Issues Packages Projects Releases Wiki Activity

feat(experiment): expose native case-to-edge facts

Browse Source 
Share exact jump-table metadata and paged case relationships across CLI,
MCP and Code Mode. Keep labels, row identities, recovered edges and machine
defaults separate; reclaim independent facts under output capacity.

Verify all 182 SQLite table targets against ELF bytes through both MCP
adapters and retain cases/calls when a real 2 MiB native budget omits IR.
Freeze the next analyst question and oracle before real-model trials.

[AUTOMATED] Experimental native patch; no upstream integration or PR.

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