coord: synth v0.50 (13 skips) + REQ-PIX-007 → implemented (both halves proven) + gale k_msgq kernel-seam need

artifacts/design-decisions.yaml

@@ -1244,7 +1244,14 @@ artifacts:
           jess CONSEQUENCE: the msgq is the VERIFIED inter-core IPC carrier for the NavState crossing
           (REQ-PIX-007 / TEST-PIX-030) - jess's current oracle uses a hand-rolled SHMEM flag handshake;
           the next rung grounds it on gale's k_msgq (over the shmem vring + the MU doorbell already in
-          rt1176-dualcore.repl), closing gale#65's gust ipc-rx on jess's side. The gust:os seam +
+          rt1176-dualcore.repl), closing gale#65's gust ipc-rx on jess's side. WHAT JESS NEEDS TO CONSUME
+          k_msgq (found 2026-07-24, RECORD not file - jess is float-gated, not ready-to-bind): the
+          gale-wasm-msgq-v0.4.0-cortex-m4f.o has 9 UNDEFINED scheduler-seam symbols (gale_w_msgq_pend /
+          ready_thread / reschedule / thread_swap_data / unpend_first_thread / spin_lock/unlock /
+          arch_thread_return_value_set / memcpy) - the gale kernel, which the v0.4.0 release does NOT
+          ship as standalone linkable objects. So to LINK+RUN k_msgq jess needs gale to also expose the
+          kernel-seam .o (or jess links the fused gale-nano core that already contains it) - the concrete
+          gale ask to FILE when jess can bind. The gust:os seam +
           executor are the gale-nano substrate for REQ-PIX-002 (M7 native base) / REQ-PIX-009 (F100).
           TRACK DISCIPLINE (do NOT treat proposed-as-delivered): the above are on gale's CUT v0.4.0
           FUNCTIONAL line (SHA-verified assets on the release). gale's SAFETY line is a SEPARATE

artifacts/findings.yaml

@@ -1227,6 +1227,12 @@ artifacts:
       codegen-affecting flight change or synth moves. Also handed synth a minimal #345 repro (large fn ->
       literal pool >4095 B from the ldr; a function-SIZE effect, not global-count) on synth#782 for the
       falcon-skip-to-zero lane; 2 concrete fixes offered (movw/movt pair, or constant-island pool flush).
+      UPDATE 2026-07-24 (synth v0.50.0, falcon-v1.127): 14 -> 13 skips. v0.50 is mostly deps + verified-
+      codegen infra (VCR-WASM-001 i64 add/sub/mul/and/or/xor exec wiring; RV32 RA validator) - NOT
+      falcon-lane float fixes; the incidental -1 is likely an i64 op cleared by the i64-exec wiring.
+      run-stabilization still lowers. #345 (my minimal repro) NOT yet actioned (3x #345 remain); no new
+      pole. Remaining 13 = 3x #345 literal-pool + 2x #503 + #518 + VFP-f32-exhaustion + VCR-RA-003 +
+      no-free-callee + i64-spill + #331. Progression 26->16->14->13. Gate STILL OPEN (13>0).
     tags: [release-watch, synth, arm, hard-float, gi-fpu, trunc-sat, on-target, falcon, blocking]
     fields:
       detected-by: jess release-watch chain-measure on synth v0.45.1 (meld v0.41.1, falcon-flight-v1.123); real-fused-core 26/156 skips vs the "#369 closed" claim; confirmed trunc_sat minimal repro; filed synth#782

artifacts/phase2-pixhawk.yaml

@@ -190,7 +190,7 @@ artifacts:
   - id: REQ-PIX-007
     type: requirement
     title: Inter-core/inter-component comms - WIT-typed contracts, fused same-core / RPC cross-core over a shared-memory transport
-    status: draft
+    status: implemented
     release: v0.7.0
     description: >
       Same-core components are meld-fused (WIT seams -> direct calls); cross-core (M4<->M7,
@@ -217,10 +217,22 @@ artifacts:
       estimator(M4)->falcon(M7) crossing datum is NavState = the IEKF state {q, v, p, b_g, b_a} =
       16x f32 = 64 bytes - a single fixed-size MU/SHMEM message (the `vehicle-state` in the
       spar-generated estimator/falcon.wit). relay-iekf is a separable no_std crate with no hidden
-      back-edges, so this is the whole inter-core estimator contract; the byte payload (list<u8>)
-      will gain this structure as the AADL feature types refine. falcon(M7)->failsafe(F100) carries
+      back-edges, so this is the whole inter-core estimator contract. falcon(M7)->failsafe(F100) carries
       the per-motor actuator commands (byte-exact pass-through, REQ-PIX-004 PART-P02).
-      category: functional
+      STATUS draft->IMPLEMENTED 2026-07-24: both halves of the requirement now have green CI-gated
+      evidence. (1) WIT-TYPED CONTRACTS - the AADL data types are now STRUCTURED (VehicleState.nav =
+      record of 16 f32; ActuatorCmd.pwm = record of 4 f32), spar codegen emits `record vehicle-state-nav`
+      / `record actuator-cmd-pwm` (not opaque list<u8>), gated by TEST-PIX-023 (the "will gain structure"
+      note above is DONE; AFD-036 resolved). (2) RPC CROSS-CORE over the shared-SRAM transport - the 16xf32
+      NavState crosses M4->SHMEM->M7 BYTE-EXACT on the dual-core RT1176 Renode model, gated by TEST-PIX-030.
+      Fused same-core (meld -> direct calls) is exercised by the scry gate on the fused core. REMAINING TO
+      `verified`: ground the transport on gale's VERIFIED k_msgq (gale v0.4.0 gale-wasm-msgq, DD-023)
+      instead of the current hand-rolled SHMEM flag handshake - BLOCKED this tick: the msgq .o needs the
+      gale scheduler seam (gale_w_msgq_pend/ready_thread/reschedule/thread_swap_data/unpend_first_thread/
+      spin_lock/memcpy = 9 undefined syms) which the v0.4.0 release does NOT ship as standalone objects.
+      RECORD (not file, per DD-022/023 sequencing - jess is #369/float-gated, not ready-to-bind): to
+      consume k_msgq jess needs gale to also expose the kernel-seam objects (or link the fused gale-nano
+      core); tracked on the DD-023 GALE row + gale#65. category: functional
       priority: should
     links:
       - type: traces-to