pulseengine · avrabe · Jul 23, 2026 · Jul 23, 2026
diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml
@@ -1240,8 +1240,8 @@ artifacts:
 
   - id: AFD-036
     type: ai-found-defect
-    title: spar codegen --format wit emits opaque list<u8> for every AADL data type - no structured WIT record/list<f32>, gating REQ-PIX-007's typed inter-core contract
-    status: open
+    title: spar codegen WIT structuring - the data-IMPLEMENTATION record path works today (jess modeling error, now corrected); the Data_Representation=>Array path was a real gap (spar#346)
+    status: resolved
     description: >
       Found 2026-07-23 (feature-loop step 2, deriving the inter-core WIT for REQ-PIX-007). The 3-core
       partition's M4->M7 crossing is a NavState = 16 x f32 (64 B) message (byte-exact crossing PROVEN
@@ -1261,11 +1261,24 @@ artifacts:
       is proven (TEST-PIX-030) but the TYPED-contract half of REQ-PIX-007 is spar-GATED - the current
       opaque `list<u8>` WIT is the state until spar#345 lands or the construct is clarified. NOT
       blocking the on-target path (falcon is #369-gated regardless), but blocks the REQ-PIX-007 refinement.
-    tags: [feature-loop, spar, aadl, wit, codegen, inter-core, navstate, req-pix-007, filed-upstream]
+      RESOLVED 2026-07-23 (spar maintainer answered spar#345, honestly split into a real gap + a jess
+      modeling error): (b) the data-IMPLEMENTATION record path ALREADY WORKS on the CI-pinned spar
+      v0.24.0 (REQ-CODEGEN-WIT-RECORDS-001) - my case-(b) failure was a MODELING ERROR: I bound the PORT
+      to the BARE type (`out data port VehicleState`) while the subcomponents lived on the IMPLEMENTATION
+      (VehicleState.nav). Binding the port to `.nav` + typing fields via a local `data F32` (Data_Size =>
+      4 Bytes; Data_Representation => Float) emits the record TODAY. jess ADOPTED this: VehicleState.nav
+      (16xf32) + ActuatorCmd.pwm (4xf32) in hardware/pixhawk6x-rt.aadl, ports bound to the impls, wit/
+      regenerated -> `record vehicle-state-nav {qw:f32..baz:f32}` + `record actuator-cmd-pwm {m0..m3:f32}`;
+      the WIT-derivation gate (TEST-PIX-023) passes. So REQ-PIX-007's typed-contract half is now DELIVERED,
+      NOT gated. (a) the `Data_Representation=>Array` path was a genuine gap (element type/Base_Type/
+      Dimension dropped to list<u8>) - the maintainer fixed it in spar PR#346 (-> `list<f32, 16>`, needs
+      Float_32 not the unsized Float); jess does not need it since the record path is cleaner. Corrects
+      the original "opaque for EVERY data type" framing - that held only for my mis-bound port.
+    tags: [feature-loop, spar, aadl, wit, codegen, inter-core, navstate, req-pix-007, resolved]
     fields:
-      detected-by: jess feature-loop (REQ-PIX-007 WIT-typing) - spar v0.24.0 + v0.30.0 both emit list<u8> for structured AADL data (Data_Model + data-impl subcomponents); filed spar#345
+      detected-by: jess feature-loop (REQ-PIX-007 WIT-typing); spar#345 answered - record path was a jess modeling error (bind port to the data IMPLEMENTATION), Array path fixed in spar PR#346; jess adopted the record path
       severity: minor
-      triage-status: filed-upstream
+      triage-status: resolved
     links:
       - type: defect-against
         target: EXTERNALANCHOR-008

diff --git a/artifacts/phase2-pixhawk.yaml b/artifacts/phase2-pixhawk.yaml
@@ -1028,11 +1028,13 @@ artifacts:
       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) - currently spar-GATED
-      (AFD-036/spar#345: spar codegen emits opaque list<u8> for every AADL data type, not a structured
-      record/list<f32>), so the typed-contract half of REQ-PIX-007 waits on spar; the byte-exact
-      crossing (this test) is independent of it. Then swap the fixed pattern for gale's verified k_msgq
-      (gale v0.4.0, DD-023) + relay's real estimator NavState when the M4 estimator lowers on-target.
+      (TEST-PIX-019). WIT-TYPING DONE 2026-07-23 (AFD-036 resolved): the NavState is now a structured
+      WIT record - hardware/pixhawk6x-rt.aadl carries VehicleState.nav (16xf32) + ActuatorCmd.pwm (4xf32),
+      ports bound to the data implementations, and `spar codegen` emits `record vehicle-state-nav {qw:f32
+      ..baz:f32}` + `record actuator-cmd-pwm {m0..m3:f32}` (verified by the TEST-PIX-023 WIT-derivation
+      gate). So REQ-PIX-007 now has BOTH halves: the byte-exact crossing (this test) + the typed contract
+      (the record). NEXT RUNG: swap the fixed pattern for gale's verified k_msgq (gale v0.4.0, DD-023) +
+      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

diff --git a/hardware/pixhawk6x-rt.aadl b/hardware/pixhawk6x-rt.aadl
@@ -101,10 +101,32 @@ public
   bus VBAT      end VBAT;       -- Gens Ace 4S 5000 mAh main rail (ESC power + monitored)
 
   --------------------------------------------------------------------------
-  -- Data carried across cores (sized so spar emits WIT type aliases)
+  -- Data carried across cores. Ports bind the data IMPLEMENTATIONS (.nav / .pwm) so
+  -- spar codegen emits STRUCTURED WIT records (not opaque list<u8>) - the typed inter-
+  -- core contract of REQ-PIX-007. Field width comes from F32's Data_Size (4 B) +
+  -- Data_Representation (Float) -> f32 (spar REQ-CODEGEN-WIT-RECORDS-001).
   --------------------------------------------------------------------------
-  data VehicleState end VehicleState;   -- estimator -> controller (pose/rates)
-  data ActuatorCmd  end ActuatorCmd;    -- controller -> failsafe/mixer (PWM setpoints)
+  data F32
+    properties
+      Data_Model::Data_Representation => Float;
+      Data_Size => 4 Bytes;
+  end F32;
+
+  data VehicleState end VehicleState;   -- estimator -> controller (the M4->M7 NavState)
+  data implementation VehicleState.nav  -- 16 x f32 IEKF state (quat, pos, vel, gyro-bias, accel-bias) = 64 B
+  subcomponents
+    qw : data F32;  qx : data F32;  qy : data F32;  qz : data F32;
+    px : data F32;  py : data F32;  pz : data F32;
+    vx : data F32;  vy : data F32;  vz : data F32;
+    bgx : data F32; bgy : data F32; bgz : data F32;
+    bax : data F32; bay : data F32; baz : data F32;
+  end VehicleState.nav;
+
+  data ActuatorCmd end ActuatorCmd;     -- controller -> failsafe/mixer (per-motor setpoints)
+  data implementation ActuatorCmd.pwm   -- 4 x f32 per-motor commands (the M7->F100 gust crossing)
+  subcomponents
+    m0 : data F32;  m1 : data F32;  m2 : data F32;  m3 : data F32;
+  end ActuatorCmd.pwm;
 
   --------------------------------------------------------------------------
   -- Sensor + power devices
@@ -247,8 +269,8 @@ public
   --  to the I/O MCU over IO_LINK. Same WIT contract whether fused or RPC'd.
   process Falcon_Flight
   features
-    state_in : in data port VehicleState;     -- <- estimator (cross-core RPC)
-    cmd_out  : out data port ActuatorCmd;     -- -> failsafe (cross-MCU RPC)
+    state_in : in data port VehicleState.nav;     -- <- estimator (cross-core RPC)
+    cmd_out  : out data port ActuatorCmd.pwm;     -- -> failsafe (cross-MCU RPC)
   end Falcon_Flight;
   process implementation Falcon_Flight.cascade
   end Falcon_Flight.cascade;
@@ -257,7 +279,7 @@ public
   --  M4 core as its own fused component. Emits VehicleState to the M7.
   process Estimator
   features
-    state_out : out data port VehicleState;
+    state_out : out data port VehicleState.nav;
   end Estimator;
   process implementation Estimator.iekf
   end Estimator.iekf;
@@ -266,7 +288,7 @@ public
   --  from the FMU over the LPUART link.
   process IO_Failsafe
   features
-    cmd_in : in data port ActuatorCmd;
+    cmd_in : in data port ActuatorCmd.pwm;
   end IO_Failsafe;
   process implementation IO_Failsafe.pwm
   end IO_Failsafe.pwm;

diff --git a/wit/estimator.wit b/wit/estimator.wit
@@ -2,9 +2,26 @@
 package pixhawk6-x-r-t:estimator;
 
 interface estimator-ports {
-    type vehicle-state = list<u8>;
+    record vehicle-state-nav {
+        qw: f32,
+        qx: f32,
+        qy: f32,
+        qz: f32,
+        px: f32,
+        py: f32,
+        pz: f32,
+        vx: f32,
+        vy: f32,
+        vz: f32,
+        bgx: f32,
+        bgy: f32,
+        bgz: f32,
+        bax: f32,
+        bay: f32,
+        baz: f32,
+    }
 
-    set-state-out: func(val: vehicle-state);
+    set-state-out: func(val: vehicle-state-nav);
 }
 
 world estimator-world {

diff --git a/wit/failsafe.wit b/wit/failsafe.wit
@@ -2,9 +2,14 @@
 package pixhawk6-x-r-t:failsafe;
 
 interface failsafe-ports {
-    type actuator-cmd = list<u8>;
+    record actuator-cmd-pwm {
+        m0: f32,
+        m1: f32,
+        m2: f32,
+        m3: f32,
+    }
 
-    cmd-in: func() -> actuator-cmd;
+    cmd-in: func() -> actuator-cmd-pwm;
 }
 
 world failsafe-world {

diff --git a/wit/falcon.wit b/wit/falcon.wit
@@ -2,11 +2,33 @@
 package pixhawk6-x-r-t:falcon;
 
 interface falcon-ports {
-    type actuator-cmd = list<u8>;
-    type vehicle-state = list<u8>;
+    record actuator-cmd-pwm {
+        m0: f32,
+        m1: f32,
+        m2: f32,
+        m3: f32,
+    }
+    record vehicle-state-nav {
+        qw: f32,
+        qx: f32,
+        qy: f32,
+        qz: f32,
+        px: f32,
+        py: f32,
+        pz: f32,
+        vx: f32,
+        vy: f32,
+        vz: f32,
+        bgx: f32,
+        bgy: f32,
+        bgz: f32,
+        bax: f32,
+        bay: f32,
+        baz: f32,
+    }
 
-    state-in: func() -> vehicle-state;
-    set-cmd-out: func(val: actuator-cmd);
+    state-in: func() -> vehicle-state-nav;
+    set-cmd-out: func(val: actuator-cmd-pwm);
 }
 
 world falcon-world {