feature: inter-core NavState crossing oracle — 16×f32 crosses M4→SHMEM→M7 byte-exact (TEST-PIX-030, REQ-PIX-007)

.github/workflows/ci.yml

@@ -153,6 +153,8 @@ jobs:
         run: /tmp/renode/renode-test hardware/renode/synth507-brtable/brtable-507.robot
       - name: gust F100/M3 byte-exact pass-through oracle (REQ-PIX-004 PART-P02, TEST-PIX-028)
         run: /tmp/renode/renode-test hardware/renode/gust-m3/passthrough-m3.robot
+      - name: inter-core NavState crossing oracle (REQ-PIX-007, TEST-PIX-030)
+        run: /tmp/renode/renode-test hardware/renode/navstate-xcore/navstate-crossing.robot
 
   # REQ-PIX-018 leg b (TEST-PIX-022) — the DO-333 sound-static-analysis leg of
   # the V, on the CONSUMED (stripped) falcon wasm: fetch a pinned falcon

artifacts/phase2-pixhawk.yaml

@@ -1008,6 +1008,35 @@ artifacts:
       - type: traces-to
         target: REQ-PIX-021
 
+  - id: TEST-PIX-030
+    type: test-spec
+    title: Inter-core NavState crossing - the 16xf32 NavState message crosses M4 -> shared SRAM -> M7 byte-exact on the dual-core RT1176 Renode model (REQ-PIX-007)
+    status: valid
+    release: v0.9.0
+    description: >
+      hardware/renode/navstate-xcore/ - proves the payload-fidelity half of REQ-PIX-007: the 3-core
+      partition's sole M7<->M4 crossing is the NavState message (16 x f32 = 64 B, DD-025/PART), and it
+      must cross the shared-SRAM ring BYTE-EXACT (no corruption, no partial read) or the M7 flight core
+      acts on a torn estimator state. Built on the proven dual-core RT1176 model
+      (hardware/renode/vehicle/rt1176-dualcore.repl: cpu_m7 + cpu_m4 on the shared sysbus, SHMEM ring
+      @0x20400000, full NXP MU doorbell). cpu_m4 (estimator core) writes the 16-word NavState to SHMEM
+      then publishes a READY flag @0x20400040 LAST (flag-last release order); cpu_m7 (flight core) spins
+      on the flag (acquire), copies the 16 words to its DTCM @0x20010000. ORACLE (navstate-crossing.robot,
+      renode-test): asserts ALL 16 DTCM output words == the producer pattern 0x4E560000+i - so the
+      NavState survived M4 -> shared-SRAM -> M7 bit-for-bit. CONFIRMED GREEN 2026-07-23 (jess local,
+      Renode 1.16.1; 16/16 words byte-exact). WIRED into .github/workflows/ci.yml renode-smoke job.
+      Hermetic: committed producer/consumer ELFs (arm-none-eabi, build.sh regenerates; ELF addresses +
+      the robot are a matched pair). This is the inter-core IPC foundation the FIRST-FLASH 3-core model
+      needs; the MU doorbell datapath (M4->M7 RR0) is separately exercised by the vehicle multinode demo
+      (TEST-PIX-019). NEXT RUNG: WIT-type the NavState record (REQ-PIX-007 / spar codegen) + swap the
+      fixed pattern for relay's real estimator NavState when the M4 estimator lowers on-target.
+    tags: [phase-2, inter-core, ipc, navstate, shmem, dual-core, rt1176, byte-exact, on-target, ci-gate, oracle, verification, req-pix-007]
+    links:
+      - type: verifies
+        target: REQ-PIX-007
+      - type: traces-to
+        target: DD-025
+
   - id: REQ-PIX-018
     type: requirement
     title: jess CI gates the falcon wasm with witness (MC/DC branch coverage) + scry (sound abstract interpretation), on the meld-fused core

hardware/renode/navstate-xcore/build.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+# Build the M4 producer + M7 consumer images for the NavState inter-core crossing
+# oracle (TEST-PIX-030). Committed ELFs + the robot's addresses are a matched pair.
+set -euo pipefail
+D="$(cd "$(dirname "$0")" && pwd)"
+CC="${CC:-arm-none-eabi-gcc}"; LD="${LD:-arm-none-eabi-ld}"
+"$CC" -c -mcpu=cortex-m4 -mthumb "$D/nav_producer_m4.S" -o "$D/nav_producer_m4.o"
+"$LD" -T "$D/nav_producer_m4.ld" "$D/nav_producer_m4.o" -o "$D/nav_producer_m4.elf"
+"$CC" -c -mcpu=cortex-m7 -mthumb "$D/nav_consumer_m7.S" -o "$D/nav_consumer_m7.o"
+"$LD" -T "$D/nav_consumer_m7.ld" "$D/nav_consumer_m7.o" -o "$D/nav_consumer_m7.elf"
+rm -f "$D"/*.o
+echo "built nav_producer_m4.elf + nav_consumer_m7.elf"

hardware/renode/navstate-xcore/nav_consumer_m7.S

@@ -0,0 +1,29 @@
+@ NavState consumer (M7 flight core) for the inter-core crossing oracle (REQ-PIX-007,
+@ TEST-PIX-030). Polls the READY flag @0x20400040 (acquire), then copies the 16-word
+@ NavState message from the SHMEM ring @0x20400000 to its own DTCM output @0x20010000,
+@ byte-exact. Vectors/text in ITCM @0x0 (M7 boots here). The robot asserts the DTCM
+@ output equals the producer's pattern word[i]=0x4E560000+i — proving the NavState
+@ crossed M4->SHMEM->M7 byte-exact over shared SRAM.
+    .syntax unified
+    .cpu cortex-m7
+    .thumb
+    .section .vectors, "a"
+    .word _m7_stack_top
+    .word reset + 1
+    .text
+    .thumb_func
+    .global reset
+reset:
+    ldr   sp, =_m7_stack_top
+    ldr   r3, =0x20400040        @ READY flag
+1:  ldr   r1, [r3]               @ spin until producer publishes (acquire)
+    cmp   r1, #0
+    beq   1b
+    ldr   r0, =0x20400000        @ SHMEM NavState src
+    ldr   r4, =0x20010000        @ M7 DTCM output dst
+    movs  r2, #16
+2:  ldr   r1, [r0], #4
+    str   r1, [r4], #4
+    subs  r2, #1
+    bne   2b
+3:  b     3b

hardware/renode/navstate-xcore/nav_consumer_m7.ld

@@ -0,0 +1,5 @@
+MEMORY { ITCM (rwx) : ORIGIN = 0x00000000, LENGTH = 0x40000
+         DTCM (rwx) : ORIGIN = 0x20000000, LENGTH = 0x40000 }
+ENTRY(reset)
+_m7_stack_top = 0x20040000;
+SECTIONS { .vectors 0x00000000 : { KEEP(*(.vectors)) } > ITCM  .text : { *(.text*) *(.rodata*) } > ITCM }

hardware/renode/navstate-xcore/nav_producer_m4.S

@@ -0,0 +1,29 @@
+@ NavState producer (M4 estimator core, FPv4-SP) for the inter-core crossing oracle
+@ (REQ-PIX-007, TEST-PIX-030). Writes the 16-word (64 B) NavState message to the
+@ M7<->M4 SHMEM ring @0x20400000, then publishes a READY flag @0x20400040 LAST so the
+@ consumer only reads a fully-written message (flag-last release order). Vectors/text
+@ in OCRAM @0x20240000 (shared RT1176 sysbus). Pattern word[i]=0x4E560000+i (distinct,
+@ "NV"+i) — the oracle asserts the M7 side reproduces it byte-exact.
+    .syntax unified
+    .cpu cortex-m4
+    .thumb
+    .section .vectors, "a"
+    .word _m4_stack_top
+    .word reset + 1
+    .text
+    .thumb_func
+    .global reset
+reset:
+    ldr   sp, =_m4_stack_top
+    ldr   r0, =0x20400000        @ SHMEM NavState base
+    movw  r1, #0x0000
+    movt  r1, #0x4E56            @ r1 = 0x4E560000
+    movs  r2, #16
+1:  str   r1, [r0], #4           @ publish NavState word i
+    adds  r1, #1
+    subs  r2, #1
+    bne   1b
+    ldr   r0, =0x20400040        @ READY flag, written LAST
+    movs  r1, #1
+    str   r1, [r0]
+2:  b     2b

hardware/renode/navstate-xcore/nav_producer_m4.ld

@@ -0,0 +1,4 @@
+MEMORY { OCRAM (rwx) : ORIGIN = 0x20240000, LENGTH = 0x10000 }
+ENTRY(reset)
+_m4_stack_top = 0x20250000;
+SECTIONS { .vectors 0x20240000 : { KEEP(*(.vectors)) } > OCRAM  .text : { *(.text*) *(.rodata*) } > OCRAM }

hardware/renode/navstate-xcore/navstate-crossing.robot

@@ -0,0 +1,31 @@
+*** Settings ***
+Resource          ${RENODEKEYWORDS}
+
+# Hermetic inter-core NavState crossing oracle (REQ-PIX-007, TEST-PIX-030) on the
+# dual-core RT1176 model. The 3-core partition's sole M7<->M4 crossing is the NavState
+# message (16 x f32 = 64 B). This proves it crosses BYTE-EXACT over the shared-SRAM ring:
+#   - cpu_m4 (estimator core) writes the 16-word NavState to SHMEM @0x20400000, then
+#     publishes a READY flag @0x20400040 LAST (flag-last release order).
+#   - cpu_m7 (flight core) spins on the flag (acquire), then copies the 16 words from
+#     SHMEM to its own DTCM @0x20010000.
+# The robot asserts every DTCM output word == the producer pattern 0x4E560000+i — so the
+# NavState survived the M4 -> shared-SRAM -> M7 crossing bit-for-bit (no corruption, no
+# partial read). This is the payload-fidelity half of REQ-PIX-007; the MU doorbell
+# datapath is separately exercised by the vehicle multinode demo (TEST-PIX-019).
+# ELFs are committed; rebuild both together via build.sh if addresses change.
+
+*** Test Cases ***
+NavState crosses M4 -> shared SRAM -> M7 byte-exact (16 x f32)
+    Execute Command           mach create "rt1176"
+    Execute Command           machine LoadPlatformDescription @${CURDIR}/../vehicle/rt1176-dualcore.repl
+    Execute Command           sysbus LoadELF @${CURDIR}/nav_consumer_m7.elf cpu=cpu_m7
+    Execute Command           sysbus LoadELF @${CURDIR}/nav_producer_m4.elf cpu=cpu_m4
+    Execute Command           cpu_m7 VectorTableOffset 0x0
+    Execute Command           cpu_m4 VectorTableOffset 0x20240000
+    Execute Command           emulation RunFor "0.01"
+    FOR    ${i}    IN RANGE    0    16
+        ${addr}=    Evaluate    ${0x20010000} + ${i} * 4
+        ${exp}=     Evaluate    ${0x4E560000} + ${i}
+        ${got}=     Execute Command    sysbus ReadDoubleWord ${addr}
+        Should Be Equal As Integers    ${got}    ${exp}    NavState word ${i} did not cross byte-exact
+    END