feat(dronecan): v1.94 sensor ingest — float16 + esc.Status/mag/baro/battery decoders (DC-P03)#230
Merged
Merged
Conversation
…attery decoders (DC-P03) The DroneCAN sensor-ingest decoders (the SPI/I2C drivers' CAN-bus counterparts) on the v1.92 transfer layer, plus the shared float16 primitive. - float16.rs: f16_to_f32 (IEEE binary16 -> f32; normals/subnormals/inf/NaN). Decode-only (falcon reads sensor float16; never emits it). No panic surface. - sensors.rs: decode_esc_status (1034, FDI: rpm/voltage/current/temp, multi-frame 14B), decode_mag (1002, MagneticFieldStrength, single-frame), decode_baro (1028, StaticPressure float32+float16), decode_battery_info (1092 prefix: temp/voltage/current, the BatteryMonitor inputs over CAN). read_bits helper for the non-byte-aligned esc.Status fields (rpm int18, power_rating, esc_index). Architecture (spar): dronecan.aadl gains the SensorSample data type + a Decode thread; spar analyze 0 errors, the Decode thread RTA 18us <= its 2ms telemetry deadline. node.wit regenerated (sample-out port + decode export). Verification (integer-Kani / float-proptest split): - Kani DC-K08 verify_read_bits_bounded: the bit-reader is total + every result < 2^nbits (the integer floor under esc.Status). 8/8 relay-dronecan harnesses. - 36 relay-dronecan tests: float16 known IEEE-half vectors + edges; esc.Status field decode + rpm sign-extend; mag 3-axis; baro float32; battery prefix; short rejects. float16 values + full-decoder totality proptest-fuzzed. rivet: SWREQ-FALCON-DC-P03 + FV-FALCON-DC-003 (test-level, 12 steps). validate PASS, 0 gaps. Clean-room 9 confirm (2 env-blocked by a full disk, self-verified). Plus the PX4-parity roadmap (FEAT-FALCON-v1.96..v1.103: parameter system keystone, pre-arm checks, calibration, failsafes, position-UX, + backlog wind-est/multi-EKF/ autotune), from the PX4 gap analysis. Scope move: gnss.Fix2 -> v1.95. Falsification: this release is wrong if a real DroneCAN float16 telemetry value mis-decodes vs IEEE-754, if a sensor decoder panics on any payload, if read_bits returns a value >= 2^nbits, or if spar analyze errors / the decode thread misses its telemetry deadline. 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
The DroneCAN sensor-ingest decoders (the SPI/I2C drivers' CAN-bus counterparts) on the v1.92 transfer layer, plus the shared float16 primitive. Also lands the PX4-parity roadmap from the gap analysis.
float16.rs—f16_to_f32(IEEE binary16 → f32: normals/subnormals/±inf/NaN/±0). Decode-only (falcon reads sensor float16; never emits it). No panic surface, so totality is free; correctness pinned by IEEE-half vectors.sensors.rs—decode_esc_status(1034, FDI: rpm/voltage/current/temp, multi-frame 14B),decode_mag(1002),decode_baro(1028, float32+float16),decode_battery_info(1092 prefix: temp/voltage/current — the BatteryMonitor inputs over CAN).read_bitshelper for the non-byte-aligned esc.Status fields.Architecture (spar)
dronecan.aadlgains theSensorSampletype + a Decode thread;spar analyze→ 0 errors, Decode thread RTA 18µs ≤ 2ms telemetry deadline.node.witregenerated (sample-out port + decode export).Verification
< 2^nbitscargo test -p relay-dronecan: 36/36.cargo kani -p relay-dronecan: 8/8 SUCCESSFUL.SWREQ-FALCON-DC-P03+FV-FALCON-DC-003(test-level, 12 steps).rivet validatePASS, 0 gaps.PX4-parity roadmap (new)
FEAT-FALCON-v1.96..v1.103from the gap analysis: parameter system (keystone) → pre-arm checks → calibration → failsafes → position-UX, + backlog (wind-est/multi-EKF/autotune). Scope move: gnss.Fix2 (variable covariance tail) → v1.95.Falsification
Wrong if a real DroneCAN float16 telemetry value mis-decodes vs IEEE-754, a sensor decoder panics on any payload,
read_bitsreturns>= 2^nbits, orspar analyzeerrors / the decode thread misses its deadline.🤖 Generated with Claude Code