From a29554885df7b505fdab0611dfeac29350068da0 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 08:52:57 +0200 Subject: [PATCH] =?UTF-8?q?finding:=20spar=20codegen=20emits=20opaque=20li?= =?UTF-8?q?st=20u8=20for=20all=20AADL=20data=20=E2=80=94=20REQ-PIX-007=20t?= =?UTF-8?q?yped-contract=20spar-gated=20(AFD-036,=20spar#345)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Feature-loop step 2 for REQ-PIX-007: tried to WIT-TYPE the NavState (16xf32) inter-core message so the contract reflects the real payload. spar codegen --format wit maps EVERY AADL data type to an opaque byte-list type regardless of structure — verified on spar v0.24.0 (CI pin) AND v0.30.0 (latest) across two AADL constructs (Data_Model Array/Float/Dim16; data implementation with Float subcomponents). Both drop the structure. Rather than hand-write a structured WIT (violates derived-from-spar + breaks the TEST-PIX-023 gate), filed spar#345 (respectful, exact repro + suggested mapping). The byte-exact NavState crossing (TEST-PIX-030) is proven and independent; only the TYPED-contract half of REQ-PIX-007 is spar-gated. - EXTERNALANCHOR-008 (spar supplier boundary) + AFD-036 (open, filed-upstream). - TEST-PIX-030 next-rung note updated (WIT-typing spar-gated; carrier -> gale k_msgq). rivet validate PASS. Co-Authored-By: Claude Opus 4.8 --- artifacts/findings.yaml | 34 ++++++++++++++++++++++++++++++++++ artifacts/phase2-pixhawk.yaml | 7 +++++-- artifacts/suppliers.yaml | 15 +++++++++++++++ 3 files changed, 54 insertions(+), 2 deletions(-) diff --git a/artifacts/findings.yaml b/artifacts/findings.yaml index 91b8f01..f017713 100644 --- a/artifacts/findings.yaml +++ b/artifacts/findings.yaml @@ -1237,3 +1237,37 @@ artifacts: target: EXTERNALANCHOR-002 - type: traces-to target: REQ-PIX-001 + + - 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 + 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 + in TEST-PIX-030). Tried to make the WIT CONTRACT structured (a record / list) by enriching + the AADL VehicleState data type, so the typed ABI reflects the real payload. spar codegen maps + EVERY AADL data type to `type X = list` regardless of structure - verified on TWO spar + versions (v0.24.0 = CI pin, and v0.30.0 = latest) x TWO AADL constructs: (a) Data_Model + properties (Data_Representation=>Array, Base_Type=>Float, Dimension=>16) and (b) a data + implementation with Base_Types::Float subcomponents. Both drop the structure and emit + `type vehicle-state = list`. So REQ-PIX-007's "WIT-typed contracts" can only be OPAQUE bytes + with spar's current codegen; jess must NOT hand-write a structured WIT (that violates the + derived-from-spar-never-hand-written discipline + breaks the TEST-PIX-023 derivation gate). Filed + spar#345 (respectful question/friction; spar HAS a data-plane marshalling feature + REQ-CODEGEN-WIT-DATAPLANE-001, so this may be a missing construct rather than a pure gap) with the + exact repro + jess impact + the suggested mapping (data-impl subcomponents -> WIT record; + Data_Model Array+Float+Dimension -> list). jess CONSEQUENCE: the byte-exact NavState crossing + 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] + 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 + severity: minor + triage-status: filed-upstream + links: + - type: defect-against + target: EXTERNALANCHOR-008 + - type: traces-to + target: REQ-PIX-007 diff --git a/artifacts/phase2-pixhawk.yaml b/artifacts/phase2-pixhawk.yaml index 1680ecf..3ddc042 100644 --- a/artifacts/phase2-pixhawk.yaml +++ b/artifacts/phase2-pixhawk.yaml @@ -1028,8 +1028,11 @@ 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 / spar codegen) + swap the - fixed pattern for relay's real estimator NavState when the M4 estimator lowers on-target. + (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. 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/artifacts/suppliers.yaml b/artifacts/suppliers.yaml index 235a9a0..a5e9d2c 100644 --- a/artifacts/suppliers.yaml +++ b/artifacts/suppliers.yaml @@ -103,3 +103,18 @@ artifacts: links: - type: traces-to target: REQ-001 + + - id: EXTERNALANCHOR-008 + type: external-anchor + title: spar (AADL→WIT/analysis) — architecture-model supplier boundary + status: accepted + description: > + pulseengine/spar is the AADL modeling + analysis tool: jess's hardware/pixhawk6x-rt.aadl is the source of truth for the 3-core + peripheral architecture, and `spar codegen --format wit` DERIVES the inter-core WIT contracts from it (REQ-PIX-007 / TEST-PIX-023, the WIT-derivation CI gate). An external supplier; its internal implementation is not traced here. Defects affecting jess's model->WIT derivation (e.g. structured data types) are recorded as ai-found-defects against this boundary. + tags: [supplier, spar, aadl, wit, codegen] + fields: + expected-derived-types: ["ai-found-defect"] + received-status: not-received + source-of-truth: {"org": "pulseengine", "doc-id": "spar-codegen-wit"} + links: + - type: traces-to + target: REQ-PIX-007