finding: REQ-PIX-007 typed-contract is spar-gated — spar emits opaque list<u8> for all AADL data (AFD-036 / spar#345) - #163
Merged
Conversation
…X-007 typed-contract spar-gated (AFD-036, spar#345) 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 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Feature-loop step 2 for REQ-PIX-007: I tried to WIT-type the NavState (16×f32) inter-core message so the contract reflects the real payload (not just
list<u8>). Verified thatspar codegen --format witmaps every AADL data type totype X = list<u8>regardless of structure:Data_Representation=>Array,Base_Type=>Float,Dimension=>16) and adata implementationwithBase_Types::Floatsubcomponents.Both drop the structure →
type vehicle-state = list<u8>.Decision
Rather than hand-write a structured WIT (which would violate the "derived from spar, never hand-written" discipline and break the TEST-PIX-023 derivation gate), I filed spar#345 — a respectful question/friction (spar has a data-plane marshalling feature, so this may be a missing construct) with the exact repro + jess impact + a suggested mapping (data-impl subcomponents → WIT
record;Array+Float+Dimension→list<f32>).The byte-exact NavState crossing (TEST-PIX-030) is proven and independent of this — only the typed-contract half of REQ-PIX-007 is spar-gated.
Changes
k_msgq(v0.4.0).rivet validate→ PASS. Not blocking the on-target path (falcon is #369-gated regardless).🤖 Generated with Claude Code