# Development and verification

Use the locked Nix shell. Run Cargo from `firmware/`, which pins Rust 1.90.0.
Keep total Cargo concurrency at two jobs. `make help` lists repository commands.

## Setup and required gates

From the repository root:

```sh
nix develop -c sh -c 'cd firmware && cargo fetch --locked'
nix develop -c rustup toolchain install nightly-2025-08-01 \
  --profile minimal --component llvm-tools-preview
nix develop -c make verification-tools
nix develop -c make verification
```

Setup needs network access. Verification uses offline dependencies and runs
host, target, board, coverage, Miri and Kani gates sequentially. Kani runs one
harness at a time. Firmware CI runs
the same command and retains evidence on failure. Keep source fixed during a run.

| Command, inside `nix develop` | Scope |
| --- | --- |
| `make pre-commit` | Formatting, host tests, host/embedded Clippy, API docs and mdBook. Does not run coverage. |
| `make -C firmware target-checks` | Sensor-free consumers, the portable runtime on ARM, and linked RTIC cross-route fixtures. |
| `make boards` | Both release board images and final-image placement checks. |
| `make coverage` | Strict core line/branch gate and informational totals for other host crates. |
| `make miri` / `make kani` | Manifest-selected checks with their own evidence receipts. |
| `make verification-inventory` | Package ownership, property claims, assumptions and gaps. |
| `env CARGO_BUILD_JOBS=1 make -j1 -C docs check` | Test examples and render mdBook. Review changed links and anchors separately. |

Host gates exclude the two bare-metal boards and include platform contracts.
They enable `kaptan-navigation/sensor-snapshots`. Navigation itself is unconditional.
Host platform tests must not invoke MMIO. Rust 1.90.0 runs all doctests and
compile-pass/fail fixtures. The test gate also runs the configurator's Node tests,
Python script tests, release-LTO final-link cases and the UTF conversion helper.

Run the native helpers separately with `make -C firmware native-test` and
`make app-native-test`. The default artifact directories are
`firmware/target/native-tests/final-link/` and `target/native-tests/utf8/`.
`CARGO_TARGET_DIR` relocates them. The UTF helper uses a host
API stub and 16-bit `wchar_t`; it does not build the Windows runner. See the
[final-link fixture](../../firmware/libs/kaptan-err-reportable-macros/tests/final_link.md)
for its archive-extraction limit.

## Evidence and proof scope

[verification.toml](../../firmware/verification.toml) owns exact tool versions,
package/harness selection, required covers, claims, assumptions and gaps. Every
workspace package must have one verification area.

By default, each run creates a new directory under `firmware/target/verification/`. It retains
tracked and nonignored untracked source, hashes, Git state, commands, tool
identities, logs, Kani exports, successful coverage reports, board ELF/binary
artifacts and `receipt.json`. Source drift fails the receipt. To choose a fresh
output directory:

```sh
nix develop -c python3 firmware/scripts/verify.py all --output /tmp/kaptan-review
```

Miri checks executed paths and schedules, not all interleavings or physical DMA.
Kani checks the manifest's component contracts with default checks and unwind
assertions enabled. Required covers must be satisfied. Missing results, timeouts,
unsupported operations and unexpected failures fail the gate.

The PID result has one qualification: finite operands can overflow to opposite
infinities whose sum is NaN. The implementation rejects that intermediate value
before changing state. Kani's raw verdict remains `Failure`. The runner accepts
only the exact declared diagnostic, function and location, with the contract
assertions and covers satisfied. Reviewed unreachable automatic checks are
recorded separately. No check is disabled or input domain narrowed. A passing
repository receipt therefore does not mean every raw Kani verdict passed.

These checks do not establish numerical accuracy, vehicle stability, arbitrary
safety histories, MMIO behavior or MCU timing. Kani's
[UB coverage](https://model-checking.github.io/kani/undefined-behaviour.html) and
[floating-point models](https://model-checking.github.io/kani/rust-feature-support.html#floating-point-operations)
have further limits. Source review and independent numerical evidence remain
required. No certification or tool qualification is claimed.

## Compiler contracts

| Contract | Enforcement and limit |
| --- | --- |
| Frames, rotation direction and position versus velocity | Distinct types and compile-fail examples. Raw sensor labeling still needs validation. |
| Allocator motor count | Const-generic dimensions. These do not establish physical mixer geometry. |
| Validated configuration and output authority | Private fields and distinct types, with compile-fail examples. Constructors and current admission policy remain responsible for validation. |
| Numerical-core unsafe operations | `forbid(unsafe_code)` in math, navigation, control, safety and runtime. Dependencies and generated export attributes remain separate boundaries. |
| Representation limits | Const assertions for navigation masks, field counts, runtime size and board storage. Object size does not measure peak stack. |
| Schemas and UART catalogs | Derive diagnostics and const validation. Received settings still need runtime validation. |
| Shared resources | Rust ownership and RTIC's resource graph. Device completion, barriers and MMIO validity remain hardware obligations. |
| Error IDs and flash-busy placement | Release final-link fixtures and packaged ELF checks, within their documented linker scope. |

Strict Clippy retains unsafe-operation and undocumented-unsafe-block lints.
A target or feature excluded from a build is not checked by that build.

## Coverage

`cargo-llvm-cov 0.8.7` comes from the locked Nix shell. The script selects
`nightly-2025-08-01`, its matching LLVM tools and the `dev` profile. Normal gates
keep Rust 1.90.0. Reports default to `firmware/target/test-coverage/`; an absolute
`CARGO_TARGET_DIR` relocates them. The verification runner uses a separate build directory.

Math, navigation, control and safety require 100% lines and branch outcomes.
Empty denominators fail. The summarizer unions LCOV source lines and LLVM branch
spans across generic instantiations. Other totals are informational, but any
test/report failure fails the gate. An absent instrumented host body is unavailable.

All host-testable members are included. Navigation enables `sensor-snapshots`
and MAVLink enables `sensor-telemetry`. Compiler-diagnostic fixtures remain on
Rust 1.90.0: coverage selects `--lib --test section` for `kaptan-config-derive`
and `--lib` for `kaptan-err-reportable-macros`. Their reported runtime coverage
does not establish compiler-phase macro coverage.

## Ground suite builds

The separate locked shell supplies Flutter, Dart and desktop dependencies:

```sh
nix develop .#ground-suite
cd ground_suite
flutter pub get --enforce-lockfile
dart format --output=none --set-exit-if-changed lib
dart analyze
flutter analyze --no-pub
flutter build web --release --no-pub
flutter build linux --release --no-pub
```

The app currently has no widget-test suite. Windows and macOS need their native
build and runtime checks.