From 19c4fbd935cb46686a58b962e525e1868e19c4f5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 12:48:26 +0200 Subject: [PATCH] =?UTF-8?q?feature:=20WIT-type=20the=20inter-core=20contra?= =?UTF-8?q?ct=20=E2=80=94=20NavState=20(16xf32)=20+=20ActuatorCmd=20(4xf32?= =?UTF-8?q?)=20records=20(REQ-PIX-007=20typed-contract=20half;=20AFD-036?= =?UTF-8?q?=20resolved)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes REQ-PIX-007's WIT-TYPED-CONTRACT half (the byte-exact crossing was proven in TEST-PIX-030 last tick; this adds the typed record). The spar maintainer answered spar#345 and split it honestly: the data-IMPLEMENTATION record path already works on the CI-pinned spar v0.24.0 — my last-tick "spar emits list for all data" was a MODELING ERROR (I bound the port to the BARE type, not the implementation). Fix (feature-loop: architecture -> spar -> WIT): - hardware/pixhawk6x-rt.aadl: add a local `data F32` (Data_Size 4 Bytes, Float), VehicleState.nav (16 f32 IEKF fields: quat/pos/vel/gyro-bias/accel-bias) + ActuatorCmd.pwm (4 f32 per-motor); bind the 4 inter-core ports to the IMPLEMENTATIONS. - wit/ regenerated via spar v0.24.0 (the CI pin): falcon/estimator/failsafe.wit now carry `record vehicle-state-nav {qw..baz: f32}` + `record actuator-cmd-pwm {m0..m3: f32}` instead of opaque list. The TEST-PIX-023 WIT-derivation gate passes (committed wit/ == spar codegen). - AFD-036 -> resolved (records were always available — my modeling error; the separate Data_Representation=>Array gap was fixed upstream in spar PR#346, not needed here). - TEST-PIX-030 note: WIT-typing DONE; REQ-PIX-007 now has both crossing + typed contract. Verified: rivet validate PASS; spar parse + instance OK; WIT-derivation gate OK. RELEASE-WATCH (same tick): kiln v0.4.4 (resource_limits, SR-45) + spar v0.31.0 - neither jess-critical; falcon still v1.127 / 14 skips (AFD-035); no inbound. Co-Authored-By: Claude Opus 4.8 --- artifacts/findings.yaml | 23 +++++++++++++++++----- artifacts/phase2-pixhawk.yaml | 12 +++++++----- hardware/pixhawk6x-rt.aadl | 36 ++++++++++++++++++++++++++++------- wit/estimator.wit | 21 ++++++++++++++++++-- wit/failsafe.wit | 9 +++++++-- wit/falcon.wit | 30 +++++++++++++++++++++++++---- 6 files changed, 106 insertions(+), 25 deletions(-) diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml index f017713..d63c136 100644 --- 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 for every AADL data type - no structured WIT record/list, 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` 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) - the maintainer fixed it in spar PR#346 (-> `list`, 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 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 index 3ddc042..2820880 100644 --- 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 for every AADL data type, not a structured - record/list), 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 index b9bab23..b74c5bd 100644 --- 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) - 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 index 7889e22..d77abfe 100644 --- 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; + 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 index 9b8018b..92c5dc1 100644 --- 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; + 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 index f2e7b68..14d10fb 100644 --- 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; - type vehicle-state = list; + 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 {