spar's codegen maps an AADL data implementation → WIT record → wasm canonical-ABI byte layout, but the width/offset table (spar-codegen/src/wit_gen.rs, spar-transform/src/wit.rs) is syntactic and never checked — #319 shows a 9-byte EepromSnapshot collapsing to an opaque list<u8>.
Proposal: use ordeal prove_equiv to prove each generated encoding faithfully represents the source layout (field offsets/widths, enum/tag discriminants, scalar padding/alignment) — the "does a WIT record faithfully encode an AADL data impl" check, currently unimplemented.
Enablers: byte-layout helpers — ordeal roadmap pulseengine/ordeal#64 (v0.10.0) — + the equivalence toolkit pulseengine/ordeal#66 (v0.12.0). Note: spar has no ordeal usage today (this is greenfield; #38 is the Lean scheduling kernel, not layout). Boundary: byte-layout is QF_BV; deployment MILP, RTA/EDF, TSN/WCTT, ARINC 653 are LP/real arithmetic and stay on HiGHS/good_lp.
spar's codegen maps an AADL
data implementation→ WITrecord→ wasm canonical-ABI byte layout, but the width/offset table (spar-codegen/src/wit_gen.rs,spar-transform/src/wit.rs) is syntactic and never checked — #319 shows a 9-byteEepromSnapshotcollapsing to an opaquelist<u8>.Proposal: use ordeal
prove_equivto prove each generated encoding faithfully represents the source layout (field offsets/widths, enum/tag discriminants, scalar padding/alignment) — the "does a WIT record faithfully encode an AADL data impl" check, currently unimplemented.Enablers: byte-layout helpers — ordeal roadmap pulseengine/ordeal#64 (v0.10.0) — + the equivalence toolkit pulseengine/ordeal#66 (v0.12.0). Note: spar has no ordeal usage today (this is greenfield; #38 is the Lean scheduling kernel, not layout). Boundary: byte-layout is QF_BV; deployment MILP, RTA/EDF, TSN/WCTT, ARINC 653 are LP/real arithmetic and stay on HiGHS/good_lp.