test(ghidra): verify PSP VFPU prefix and vector decoding (#8614)

* test(psp): add source-owned VFPU prefix and vadd sequence

* test(psp): assert VFPU prefix and consumer decode facts

* test(psp): verify VFPU prefixes and consumers through public Ghidra MCP

* docs(psp): delimit VFPU prefix/consumer conformance coverage

* test(psp): preserve unknown when Ghidra omits high-pcode data

* style(psp): apply pinned oxfmt output to verify-real-ghidra-mips.mjs

* style(psp): apply pinned oxfmt output to psp-fixture.mjs

docs/ghidra-psp.md

@@ -93,8 +93,15 @@ The maintained PSP fixture builds from `tests/conformance/psp/`, never executes,
 and is independent of commercial game data. PSP GNU tools supply ELF/ABI,
 raw ABI-record, symbol and encoding observations; REA's parsed target and saved
 snapshot must agree with the independent ABI declaration. Public CLI/MCP must
-recover known functions, a direct
-call, the immediate `0x1234`, BITREV, a global word and a marker. The verifier
+recover known functions, a direct call, the immediate `0x1234`, BITREV, a
+global word and a marker. The additional source-owned VFPU function contains
+`vpfxs`, `vpfxt`, `vpfxd` and three `vadd.q` instructions.
+The PSP lane checks their fixed encoded bytes and Ghidra's decoded mnemonics
+through `inspect_native_instruction`; an analyzed dossier reports available
+high-p-code opaque-operation and truncation observations. Neither decoded
+instructions nor `CALLOTHER` counts establish prefix consumption, lane-level
+arithmetic or emulator/hardware equivalence.
+The verifier
 checks observed loader/language, original bytes, Evidence, snapshot reopening,
 and an A-B-A target switch with different global contents at the same address.
 A snapshot for A must not open B. Cleanup must finish before success is reported.

scripts/verify-real-ghidra-mips.mjs

@@ -38,6 +38,8 @@ import {
   buildPspFixture,
   assertPspLoadedImage,
   assertPspProbe,
+  PSP_VFPU_DECODE_CASES,
+  assertPspVfpuProbe,
 } from "../tests/conformance/ghidra/psp-fixture.mjs";
 import {
   requireMcpToolError,
@@ -541,6 +543,47 @@ try {
       });
       if (psp) assertPspProbe(move, branch);
       else assertMipsProbe(move, branch, byteOrder, probe);
+      let vfpuCoverage;
+      if (psp) {
+        const vfpuAddress = BigInt(independent.symbols.rea_psp_vfpu_probe);
+        const vfpuInstructions = [];
+        for (const { index } of PSP_VFPU_DECODE_CASES) {
+          vfpuInstructions.push(
+            await call("inspect_native_instruction", {
+              address: `0x${(vfpuAddress + 4n * BigInt(index)).toString(16)}`,
+            }),
+          );
+        }
+        assertPspVfpuProbe(vfpuInstructions);
+        const vfpuDossier = functionDossierSchema.parse(
+          await call("analyze_function", {
+            procedure: independent.symbols.rea_psp_vfpu_probe,
+            detail: "complete",
+          }),
+        );
+        assert.equal(BigInt(vfpuDossier.procedure.address), vfpuAddress);
+        const flow = vfpuDossier.native_value_flow;
+        const hasHighPcode = flow?.available === true;
+        vfpuCoverage = {
+          decoded_instructions: vfpuInstructions.length,
+          prefix_sites: 4,
+          vadd_sites: 3,
+          high_pcode: hasHighPcode ? "observed" : "unavailable",
+          opaque_high_pcode_operations: hasHighPcode
+            ? flow.operations.filter(({ opcode }) => opcode === "CALLOTHER")
+                .length
+            : null,
+          truncated: hasHighPcode ? flow.truncated : null,
+          unavailable_reason:
+            flow?.available === false
+              ? flow.reason
+              : hasHighPcode
+                ? null
+                : "Ghidra did not report a HighFunction value flow",
+          pseudocode_nonempty: vfpuDossier.pseudocode.trim().length > 0,
+          numeric_vector_semantics: "not_verified",
+        };
+      }
       const global = await call("read_bytes", {
         address: independent.symbols[`${prefix}_global`],
         length: 4,
@@ -807,6 +850,9 @@ try {
           "independent ELF/ABI and symbols",
           "loaded Ghidra identity",
           "fixed instruction bytes and immediate",
+          ...(psp
+            ? ["VFPU prefix/vadd opcode decoding (not arithmetic equivalence)"]
+            : []),
           psp
             ? "Allegrex BITREV decoding and A-B-A target identity"
             : "conditional branch destination",
@@ -816,6 +862,7 @@ try {
             ? ["soft-float o32 parameter/return storage and caller constants"]
             : []),
         ],
+        ...(vfpuCoverage === undefined ? {} : { vfpu_decode: vfpuCoverage }),
         ...(softFloat === undefined ? {} : { soft_float: softFloat }),
         procedures: procedures.length,
         carved: carved ?? {

tests/conformance/ghidra/psp-fixture.mjs

@@ -68,6 +68,7 @@ export async function buildPspFixture(directory, globalValue = 7) {
     ["rea_psp_entry", "FUNC"],
     ["rea_psp_leaf", "FUNC"],
     ["rea_psp_probe", "FUNC"],
+    ["rea_psp_vfpu_probe", "FUNC"],
     ["rea_psp_global", "OBJECT"],
     ["rea_psp_marker", "OBJECT"],
   ]) {
@@ -231,6 +232,36 @@ export function assertPspLoadedImage(image, targetSha256) {
   assert.equal(image.source_files[0].modified_sha256, targetSha256);
 }
 
+/** Static decode coverage only: neither opaque CALLOTHER nor generated C proves vector math. */
+export const PSP_VFPU_DECODE_CASES = [
+  { index: 2, word: 0xdc0000e4, mnemonic: "vpfxs" },
+  { index: 3, word: 0xdd0000e4, mnemonic: "vpfxt" },
+  { index: 4, word: 0xde000000, mnemonic: "vpfxd" },
+  { index: 5, word: 0x60048090, mnemonic: "vadd.q" },
+  { index: 7, word: 0xdc0000c6, mnemonic: "vpfxs" },
+  { index: 8, word: 0x60048090, mnemonic: "vadd.q" },
+  { index: 10, word: 0x60048090, mnemonic: "vadd.q" },
+];
+
+/** Compare actual Ghidra listing instructions against source-owned PSP words. */
+export function assertPspVfpuProbe(observations) {
+  assert.equal(observations.length, PSP_VFPU_DECODE_CASES.length);
+  for (let i = 0; i < observations.length; i++) {
+    const expected = PSP_VFPU_DECODE_CASES[i];
+    const observed = observations[i];
+    const word = Buffer.alloc(4);
+    word.writeUInt32LE(expected.word);
+    assert.equal(
+      observed.status,
+      "decoded",
+      `VFPU instruction ${expected.index} did not decode`,
+    );
+    assert.equal(observed.length, 4);
+    assert.equal(observed.bytes.toLowerCase(), word.toString("hex"));
+    assert.equal(observed.mnemonic.toLowerCase(), expected.mnemonic);
+  }
+}
+
 /** Fixed source encodings and independently chosen immediate, not pseudocode. */
 export function assertPspProbe(move, bitrev) {
   assert.equal(move.status, "decoded");

tests/conformance/psp/probe.S

@@ -12,3 +12,29 @@ rea_psp_probe:
   nop
 .end rea_psp_probe
 .size rea_psp_probe, .-rea_psp_probe
+
+/* Source-owned VFPU prefix/consumer sequence. Never executed.
+ * Encodings match the independent Allegrex headless conformance fixture;
+ * this tests static decoding, not numerical lane or prefix correctness.
+ */
+.align 2
+.globl rea_psp_vfpu_probe
+.type rea_psp_vfpu_probe, @function
+.ent rea_psp_vfpu_probe
+rea_psp_vfpu_probe:
+  .word 0xd8800000 /* lv.q */
+  .word 0xd8a40000 /* lv.q */
+  .word 0xdc0000e4 /* vpfxs, identity source */
+  .word 0xdd0000e4 /* vpfxt, identity target */
+  .word 0xde000000 /* vpfxd */
+  .word 0x60048090 /* vadd.q */
+  .word 0xf8d00000 /* sv.q */
+  .word 0xdc0000c6 /* vpfxs, swizzled source */
+  .word 0x60048090 /* vadd.q */
+  .word 0xf8d00010 /* sv.q */
+  .word 0x60048090 /* vadd.q with no new prefix */
+  .word 0xf8d00020 /* sv.q */
+  jr $ra
+  nop
+.end rea_psp_vfpu_probe
+.size rea_psp_vfpu_probe, .-rea_psp_vfpu_probe