squitter 0.1.1

no_std, no_alloc parser and encoder for 1090ES/DF17 (ADS-B extended squitter) messages
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134

# squitter

[![CI](https://github.com/hz2/squitter/actions/workflows/ci.yml/badge.svg)](https://github.com/hz2/squitter/actions/workflows/ci.yml)
[![license: MIT](https://img.shields.io/badge/license-MIT-blue.svg)](LICENSE)
[![no_std](https://img.shields.io/badge/no__std-yes-brightgreen.svg)](#)

A `no_std`, allocation-free parser and encoder for **1090ES** (1090 MHz
Extended Squitter, the ADS-B link layer carried in Mode S **DF17**
frames), commonly represented as raw hex (e.g. `dump1090`'s
`*8D4840D6202CC371C32CE0576098;` format).

- **Four message families**, decode and encode: aircraft identification,
  surface position, airborne position, and airborne velocity. Every test
  fixture is a real captured hex frame, cross-checked against
  [`pyModeS`](https://github.com/junzis/pyModeS)'s own test suite, not
  synthetic round trips. `tests/real_world_corpus.rs` additionally
  cross-checks against an independent bulk decode (via pyModeS itself) of
  over a thousand unique real captured frames.
- **Fuzz-tested with [proptest](https://docs.rs/proptest)**: message
  decode/encode never panics on arbitrary bytes, and reaches a fixed point
  after one encode/decode pass, over the full space of raw `ME` payloads
  (not just the handful of fixed fixtures above).
- **CPR position decoding**, including the harder surface-CPR case (which
  needs a nearby reference position to disambiguate its 90° latitude zone),
  verified against real airborne and surface position pairs.
- **`no_std`, no `alloc`**: works on bare-metal targets with no allocator.
  `core` has no `floor`/`sqrt`/`acos` without a `libm` dependency, so the CPR
  math and ground-speed magnitude use a hardcoded latitude-zone table and a
  hand-rolled Newton-Raphson `sqrt` instead of pulling one in.
- **Zero mandatory dependencies.** The bit-level codec is hand-rolled, same
  as the CPR/velocity math above.
- **`#![forbid(unsafe_code)]`.**
- **Formal verification** of the bit engine with [Kani](#formal-verification),
  not just tests.

## Crates

| Crate | Description |
| --- | --- |
| [`squitter`](crates/squitter) | The `no_std`, no-`alloc` parser/encoder library. |
| [`squitter-cli`](crates/squitter-cli) | A small command-line decoder (installs as `squitter`). |

## Quick start

```rust
let msg = squitter::decode_line("8D4840D6202CC371C32CE0576098")?;

let squitter::AdsbMessage::Identification(id) = msg else {
    panic!("expected an identification message");
};

println!("callsign={}", id.callsign);
```

Encoding mirrors decoding, given the transmitting aircraft's ICAO address
and transponder capability level:

```rust
let frame = squitter::encode_frame(&msg, 0x4840D6, 5)?;
let mut buf = [0u8; 28];
let hex = frame.write_hex(&mut buf);
```

Add it to a project with:

```sh
cargo add squitter
```

## Message type coverage

| Type codes | What |
| --- | --- |
| 1-4 | Aircraft Identification and Category |
| 5-8 | Surface Position |
| 9-18, 20-22 | Airborne Position (barometric altitude / GNSS height) |
| 19 | Airborne Velocity (ground speed / airspeed, vertical rate) |

A few things are deliberately left undecoded/deferred rather than
approximated, and documented as such in the source: the legacy
Gillham/gray-code altitude encoding (rare in modern traffic), single-frame
CPR position decode against a known reference (only the even/odd-pair
global decode is implemented), and a ground-track-angle accessor for
airborne velocity (needs `atan2`, which doesn't have the same clean
small-table shortcut `NL(lat)` does).

See [`crates/squitter/src/lib.rs`](crates/squitter/src/lib.rs) for the
crate's module layout and [`crates/squitter/src/message`](crates/squitter/src/message)
for each message type, each with its own real-fixture tests.

## Building

This project is built and checked with [Nix](https://nixos.org/):

```sh
nix develop        # dev shell: toolchain, rust-analyzer
nix flake check -L # fmt, clippy (pedantic), tests, no_std/no_alloc cross-compile
nix build           # squitter-cli (default package)
nix build .#squitter
```

CI runs the identical `nix flake check -L`, so there is one source of truth
for what "passing" means, locally and in GitHub Actions.

Without Nix, a standard `cargo build` / `cargo test` from the workspace root
also works with a recent stable Rust toolchain (edition 2024, MSRV tracked
in `Cargo.toml`).

## Formal verification

The bit-level codec (`src/bits/`) is proven, not just tested, using
[Kani](https://github.com/model-checking/kani), a bounded model checker for
Rust. Where the test suite samples inputs, these harnesses (gated behind
`#[cfg(kani)]`, so they add nothing to normal builds) prove properties over
*every* input in a bounded space:

- `BitReader`/`BitWriter` never panic, for any input, including malformed
  `nbits`/buffer combinations a caller isn't supposed to pass.
- Writing a value and reading it back recovers the original value exactly,
  for every bit width `1..=64`.

Kani requires its own toolchain download (a pinned nightly + CBMC), which
needs network access and isn't run inside the hermetic Nix sandbox, so it's
a manual step rather than part of `nix flake check`:

```sh
cargo install --locked kani-verifier
cargo kani setup
cargo kani -p squitter
```

## License

MIT. See [LICENSE](LICENSE).