public/kaptan
1
Fork 0
Code Issues 24 Pull Requests Actions Packages Projects Releases Wiki Activity

build: replace argument dispatch and retain source-bound verification

Browse Source 
Replace argument recovery with direct build targets. Run host, target,
board, coverage, Miri and selected Kani checks while retaining source
identities, logs and artifacts, including failed attempts.

Keep the PID proof diagnostic exception explicit and match its exact
identity alongside passing contract assertions and covers.

Validation: final-source verification matrix, assembled workflow tests
and documentation build.
This commit is contained in:
Onur Özkan committed 2026-11-07 18:12:11 +03:00
1 parent 4953f0a974
commit 62b18d5b2e
26 files changed
+2177 -1052
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

docs/Makefile
+17 -29
View File
@@ -1,38 +1,26 @@
override SHELL := /bin/sh
override MAKEFLAGS += --no-print-directory
SHELL := /bin/sh
MAKEFLAGS += --no-print-directory
.DEFAULT_GOAL := help
.DELETE_ON_ERROR:
override MDBOOK := mdbook
override PRIMARY_GOAL := $(firstword $(MAKECMDGOALS))
ifeq ($(PRIMARY_GOAL),run)
.PHONY: run
# Application arguments may also look like Make goals. The run recipe recovers
# their exact boundaries from the original invocation.
.DEFAULT:
@:
else
.PHONY: help run check
.PHONY: help build test check clean
help:
@printf '%s\n' 'Usage: make docs -- <mdbook arguments...>' '' \
'With no arguments, mdbook test and mdbook build are run.' \
'Example: make docs -- build' '' \
'Project target:' \
' check Run mdbook test and mdbook build'
@printf '%s\n' 'Usage: make -C docs build|test|check|clean' '' \
' build Build the book' \
' test Test book examples' \
' check Test and build the book' \
' clean Remove generated documentation' '' \
'For other options, run mdbook directly from docs/.'
endif
build:
mdbook build
check:
$(MDBOOK) test
$(MDBOOK) build
test:
mdbook test
run:
@exec python3 ../scripts/make-argv.py exec run $(MDBOOK)
check: test build
clean:
mdbook clean
docs/src/boards/geprc-f722-v2.md
+3 -3
View File
@@ -14,7 +14,7 @@ pins PB0/PB1/PB4/PB5 low.
From the repository root:
```sh
make firmware/boards/geprc-f722-v2
make -C firmware/boards/geprc-f722-v2 build
```
The packaging script validates the ELF against the shared F722 linker layout
@@ -31,7 +31,7 @@ listed `0483:df11` target before flashing:
```sh
dfu-util --list
make firmware/boards/geprc-f722-v2 flash
make -C firmware/boards/geprc-f722-v2 flash
```
## MAVLink over USB
@@ -41,7 +41,7 @@ enumerates as `Kaptan / GEPRC TAKER F722 V2 (ICM-42688-P)`, normally
`/dev/ttyACM*` on Linux. Run:
```sh
make firmware/tools/configurator
make configurator
```
Open `http://127.0.0.1:4861` and connect `/dev/serial/by-id/<kaptan-device>` or
docs/src/boards/kakute-f7-mini-v3.md
+3 -3
View File
@@ -15,7 +15,7 @@ motor pins PB0/PB1/PB4/PB5/PB6/PB7 low.
From the repository root:
```sh
make firmware/boards/kakute-f7-mini-v3
make -C firmware/boards/kakute-f7-mini-v3 build
```
The packaging script uses the shared F722 linker layout and prints the flash
@@ -37,7 +37,7 @@ application offset.
```sh
dfu-util --list
make firmware/boards/kakute-f7-mini-v3 flash
make -C firmware/boards/kakute-f7-mini-v3 flash
```
## MAVLink over USB
@@ -47,7 +47,7 @@ enumerates as `Kaptan / Kakute F7 Mini V3`, normally `/dev/ttyACM*` on Linux.
Then launch the target-described web UI:
```sh
make firmware/tools/configurator
make configurator
```
Open `http://127.0.0.1:4861` and connect `/dev/serial/by-id/<kaptan-device>` or
docs/src/configuration.md
+1 -1
View File
@@ -58,7 +58,7 @@ Build and flash the board image, boot normally, connect the board's USB port,
and run from the repository root:
```sh
make firmware/tools/configurator
make configurator
```
Open `http://127.0.0.1:4861`, enter the device path in the Connection section,
docs/src/development.md
+100 -39
View File
@@ -1,57 +1,118 @@
# Development and verification
## Command layout
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.
Each component owns its Makefile: the Cargo workspace, all-board workflows,
individual boards, tools, and documentation each define commands in their own
directory. The root Makefile contains repository-wide workflows and routes a
directory path to that directory's Makefile.
## Setup and required gates
The standard `--` ends Make's own options. Every following argument uses the
selected application's native command line. For example,
`make firmware -- test --workspace --locked --offline` runs `cargo test
--workspace --locked --offline` from `firmware`. Board paths are
the complete build-and-package command, so they need no invented operation
name.
## Fast host checks
From the repository root:
```sh
make firmware -- fmt --all --check
make firmware -- test --workspace --locked --offline
make firmware -- clippy --workspace --all-targets \
--exclude kaptan-geprc-f722-v2 \
--exclude kaptan-kakute-f7-mini-v3 --locked --offline -- -D warnings
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
```
## Target checks
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
make firmware/boards
make firmware -- clippy \
-p kaptan-geprc-f722-v2 -p kaptan-kakute-f7-mini-v3 \
--target thumbv7em-none-eabihf --locked --offline -- -D warnings
nix develop -c python3 firmware/scripts/verify.py all --output /tmp/kaptan-review
```
`make firmware docs` builds Rust API documentation with warnings denied.
`make docs` checks and builds the separate mdBook project. `make pre-commit`
runs both documentation checks along with repository formatting, host and
embedded Clippy, Rust and script tests. `make check`
adds a whitespace check. `make build` builds and packages release firmware and
builds the mdBook project.
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.
## Strict core coverage
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.
```sh
cd firmware
scripts/report-test-coverage.sh
```
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.
The strict gate requires 100% line and branch coverage for `kaptan-math`,
`kaptan-navigation`, `kaptan-control`, and `kaptan-safety`. It isolates each
core package's coverage artifacts, unions LCOV source-line records, and uses
full LLVM source spans to merge generic branch instantiations without lowering
the gate.
## 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
docs/src/getting-started.md
+17 -2
View File
@@ -17,14 +17,29 @@ From the repository root, discover the developer commands with:
make help
```
Run the repository checks with:
Fetch the pinned Rust dependencies once before the offline checks:
```sh
cd firmware
cargo fetch --locked
```
From the repository root, run the checks with:
```sh
make pre-commit
make coverage
```
Bare-metal board packages are not host-test targets. Check them with the
target-specific commands in [Development and verification](development.md).
Pre-commit does not run coverage. The separate required coverage gate needs
the dated nightly setup documented there. Shared navigation and sensor snapshot
conversion remain covered through `kaptan-navigation/sensor-snapshots`.
For the app, enter `nix develop .#ground-suite`. Its locked Flutter and Dart
tools are separate from the firmware shell. App analysis
and web/Linux build commands are listed in the development guide.
## Repository layout
@@ -45,7 +60,7 @@ The manual is an [mdBook](https://rust-lang.github.io/mdBook/) project. The
repository's Nix development shell provides the checked tool version:
```sh
nix develop -c make docs -- build
nix develop -c make -C docs build
```
The generated static site is written to `target/docs/`.
docs/src/index.md
+4 -15
View File
@@ -1,8 +1,6 @@
# Overview
Kaptan is an embedded Rust flight-controller project. This manual is the
single source of project documentation: board support, safety boundaries,
development workflow, and design references live here as Markdown.
Kaptan is an embedded Rust flight-controller project.
> **Status:** The board images do not yet run the flight runtime or implement
> motor drivers. Motor pins are inhibited at startup. Physical flight has not
@@ -15,19 +13,10 @@ development workflow, and design references live here as Markdown.
- Board work belongs under [Boards](boards/index.md).
- [Configuration](configuration.md) explains target-described user settings
and immutable F722 hardware policy.
- [Logs](logs.md) and [Errors](errors.md) describe the custom MAVLink
observability surface and its current safety scope.
- [Logs](logs.md) and [Errors](errors.md) describe MAVLink diagnostics.
- Before submitting changes, follow [Development and verification](development.md).
## Documentation conventions
Documentation is centralized in `docs/src/`; individual crates and board
directories do not carry README files. The top-level `firmware/README.md`
only defines the firmware workspace boundary. Keep pages in Markdown, add each
page to `SUMMARY.md`, and place commands beside the assumptions and safety
boundary they depend on.
The current configuration contract is target-described. Each F722 board exposes
only values consumed by that compiled target. Physical F722 hardware selection
remains immutable board policy. No writable
snapshot can bypass an immutable safety decision.
Keep documentation in `docs/src/`, add pages to `SUMMARY.md`, and place commands
beside their prerequisites.
docs/src/reference.md
+10 -17
View File
@@ -1,31 +1,24 @@
# Reference
This page collects stable limits and points to the detailed contracts.
| Surface | Current contract |
| --- | --- |
| F722 persistence | One bounded native-width scalar snapshot inside each slot of a power-loss-safe two-slot flash journal. |
| Public config artifact | One canonical self-describing KCFG file containing generated metadata, factory values, and the complete committed candidate. |
| Public config artifact | Canonical KCFG v3 with generated metadata, finite/nonzero flags, factory values, selected-view values and exact expected-base values. |
| Flight profile | Generated schema and required compiled installation for the portable runtime. See [Configuration](configuration.md#flight-configuration). |
| Navigation service | Fusion, prediction and initialization completion run on due 100-Hz control service. Early ticks supervise cached evidence; admission alone cannot renew capabilities. |
| Navigation model bound | Navigation-owned 25-m/s² free-flight acceleration envelope, checked against the complete profile's thrust and mass. Contact impulses are outside this bound. |
| File transfer | Custom `FILE_CONTROL` (51025) and `FILE_DATA` (51026), one owner-bound stop-and-wait transfer, 246-byte data chunks, CRC-32C. |
| Diagnostics | `LOG` (51020) for macro-produced level/text; `ERROR` (51021) for a bounded reportable `{ error_id, raised_at[96] }` firmware error. |
| Publications | Kaptan-native `HEARTBEAT` (51027), `IMU` (51028), `RANGE` (51029), and `OPTICAL_FLOW` (51030); exact integer units and monotonic `u64` microseconds. |
| Publications | Kaptan-native `HEARTBEAT` (51027), `IMU` (51028), `RANGE` (51029), and `OPTICAL_FLOW` (51030). IMU has a 28-byte payload, extra CRC 22 and `i32` mrad/s gyro axes. |
| F722 clock | Shared TIM2 1-MHz epoch, CC1 100-Hz service. DWT is reserved for the SRAM flash-poll timeout. |
| F722 configuration | `/config/user.kcfg`; target-described fields and board factory values over local USB CDC-ACM or a directly wired unsigned UART with motor outputs physically inhibited. |
Read [Configuration](configuration.md) for configuration ownership, artifact,
and file contracts, [Logs](logs.md) for receiver decoding and filtering, and
and file contracts, [Architecture](architecture.md#monotonic-time) for clock
assumptions, [Logs](logs.md) for receiver decoding and filtering, and
[Errors](errors.md) for reportable errors and panic scope.
## Verification
Before review, run:
```sh
make pre-commit
make build
```
The target-specific lint verifies the local configuration receiver and journal
path. The host suite separately asserts that configuration ingress cannot reach
an actuator path. The ELF checks prove that the flash-busy operation is linked
into executable SRAM and reject compiler-outlined control flow or PC-relative
literal loads outside that section.
Use [Development and verification](development.md) for the required gates,
tool setup and evidence limits.