fold/docs/research/z3-surface-vendor-research-2026-05-31.md

Z3 Surface Vendor Decision Record

Date: 2026-05-31; updated after Ghidra/P-Code integration work. Reading list: docs/research/vendor-library-study-2026-05-31.md.

Problem

Fold's Z3-backed source path already has observer hooks and bounded symbolic queries. The binary path historically relied on r2 metadata and heuristics. The risk was adding multiple vendor IRs directly to detectors, creating duplicated logic and unclear provenance.

Decision

Use a small, explicit vendor surface:

1. Ghidra/SLEIGH for binary semantics. Map raw/high P-Code into Fold's binary hazard and summary path.
2. LIEF for binary metadata, if/when r2 metadata becomes the bottleneck. LIEF should produce file-structure facts only.
3. Souffle for derived facts after stable MidIR/fact IDs. It should consume Fold-owned facts, not vendor-specific ASTs or LLVM objects.

RetDec, Remill/McSema, PhASAR, and Crab/Clam stay deferred until a fixture proves that the active lanes cannot close a specific precision or recall gap.

Current Fold surface

Surface	Current owner	Vendor implication
Source symbolic checks	Clang AST/CFG + Fold Z3 encoder	no new vendor needed now
Binary metadata	r2 session/CLI fallback	LIEF can replace/supplement this later
Binary semantics	Ghidra raw/high P-Code	primary active vendor lane
Cross-function facts	native summaries/graphs	Souffle candidate after stable facts
Numeric invariants	native summaries/ranges	Crab/Clam deferred until a concrete gap

Why not add all candidate libraries now?

• More IRs do not improve findings unless Fold can normalize provenance, location, value IDs, and precision.
• Heavy LLVM-based lanes duplicate Ghidra's current role while adding build and version constraints.
• Fact engines are only safe after stable fact IDs exist; otherwise derived facts cannot round-trip into reports or suppressions reliably.

External references

• Ghidra P-Code reference: https://ghidra.re/ghidra_docs/languages/html/pcoderef.html
• Ghidra SLEIGH manual: https://ghidra.re/ghidra_docs/languages/html/sleigh.html
• LIEF C++ API: https://lief.re/doc/latest/api/cpp/index.html
• LIEF binary abstraction parser: https://lief.re/doc/stable/api/binary_abstraction/cpp.html
• Souffle C++ interface: https://souffle-lang.github.io/interface
• Souffle execution modes: https://souffle-lang.github.io/execute

Deferred references are listed in docs/research/vendor-library-study-2026-05-31.md.

Next implementation checkpoints

1. Keep Ghidra findings provenance-tagged as ghidra-raw or ghidra-ssa.
2. Add LIEF only as a read-only metadata adapter; compare it against current r2 metadata outputs before replacing anything.
3. Define FunctionId, BlockId, OpId, and ValueId before Souffle.
4. Prototype Souffle with TSV + .dl before generated C++ embedding.
5. Require a fixture-backed revisit trigger before adding RetDec, Remill/McSema, PhASAR, or Crab/Clam scaffolding again.

Guardrails

• Do not widen core::AnalysisBackend for vendor-specific payloads.
• Do not decompile binaries to C and run source detectors on that output.
• Keep source, binary metadata, binary semantics, and derived facts separately measurable in profiles.
• Reports must preserve per-finding backend and lane provenance.