Documentation integrity: the #388 correction never reached any document that tells someone what to DEPLOY

[avrabe]

An audit of comments, docs and user-facing strings against the code. Every claim
below was checked by running the check, not by reading.

The cluster that matters — fix this one first

The #388 correction (published components wrapped the legacy PID stack; the
flight core moved to geometric SE(3) + ADRC) was applied thoroughly on the
code side: cascade/src/lib.rs, native_mirror.rs, FV-FALCON-PERF-002,
BUILD.bazel, the audit script.

It was applied to none of the documents that tell someone what to deploy:

document	false claim
docs/OCI-DISTRIBUTION.md:11-21	"publishes each verified cascade stage… jess wkg oci pulls and fuses/lowers per core"; ghcr.io/…/falcon/attitude # geometric SO(3) attitude
wasm/cm/attitude/Cargo.toml:5	"Formally-verified geometric SO(3) attitude controller" — piped verbatim into the OCI annotation (#412)
scripts/meld-fuse-cascade.sh:2-6	same framing
artifacts/verification/FV-FALCON-MELD-001.yaml:8-23	same
wasm/cm/cascade/src/{stream,step,orch}.rs	still describe themselves as the flight pipeline

Who this misleads: jess — the integrator these components exist for — is
told to pull falcon/attitude per-core and fuse it, and would deploy the legacy
PID stack believing it is the verified flown law. This is the only group where
acting on the false text puts the wrong control law on a vehicle.

Tier 1 — the rest

15 files say "generated… Do not edit manually" and are hand-maintained and shipped

crates/{relay-ccsds,cfdp,cs,hk,ds,fm,md,ci,sc,mm,to,hs,sch,tbl,sca}/plain/src/engine.rs:1-2

"plain Rust (generated from Verus source via verus-strip). Source of truth: ../src/engine.rs. Do not edit manually."

Exactly one verus_strip_test exists (relay_primitives), and BUILD.bazel:32-35
says in the same file: "verus-strip currently has bugs … plain/ is hand-maintained".
Cargo.toml points [lib] path at plain/src/lib.rs — the "generated mirror"
is the shipped code. Test counts diverge sharply (ccsds 0 vs 11, cfdp 0 vs 10,
cs 10 vs 10).

Misleads: a fix goes into src/engine.rs and never reaches the artifact; or
someone hand-runs a strip and deletes up to 11 tests per file. The header is
exactly inverted.

kani.yml:77-79 tells you the wrong place to put a new harness

Claims harnesses live at crates/<engine>/plain/src/kani_proofs.rs. 12 of 45
matrix entries don't match — some at src/kani_proofs.rs with no plain/
(relay-bus, relay-hal, falcon-baromag, falcon-esc-dshot, falcon-gnss-ubx), some
inline in plain/src/lib.rs (relay-arm, relay-adrc, relay-nid, relay-iekf,
relay-geo, relay-fsm, relay-mix-quad).

Misleads: a new proof lands in a file nothing declares → never compiled,
never run. A brand-new orphaned proof, created by the workflow's own instructions.

run-falcon-verification.py:11-20 documents a skip-marker it does not implement

Verified by importing the module and calling is_bench_only directly:
'echo hi # bench-only' → False. Classification is by command shape over
37 regexes; the marker does nothing. The code's own comment at :41-43
contradicts the docstring. (Confirmed independently during v1.138 work.)

scripts/build-flight-component.sh:8-10 documents a procedure that clobbers the CI artifact

Says the emission is "MANUAL/bench… run it at release time and attach the output".
But release.yml:466-496 installs cargo-component and runs build-components.sh.
The script's last step is gh release upload … --clobber using a bare
cargo component build --release — no --target, --no-default-features,
--emit-relocs, -zstack-size, or --export=__heap_base. Following the doc
overwrites the CI asset with one missing the relocation metadata and tuned stack
whose absence already cost falcon-v1.134.0.

CLAUDE.md:53 — the command every agent reads first does not exist

$ bazel query '//:verus_test'
ERROR: no such target '//:verus_test'

There are 19 targets, all named relay_*_verus_test.

Tier 2 — misdirects investigation

• README.md:66-73 shows the verification gate passing 3 artifacts; it sweeps 192. Trains readers to accept a tiny scope as normal, so a real scope collapse reads as healthy.
• docs/VERIFICATION-CHAIN.md:63 — verify-chain.sh --all is documented as repo-wide; verify-chain.sh:16 lists 5 of 46 engines.
• docs/falcon.md — 3 bazel targets that don't exist, falcon-sim run (no such binary), 6 wrong paths including proofs/verus/ (ls proofs/ → gappa lean rocq), and "falcon-v1.27 — well past v1.0" at v1.138.
• docs/SIMULATOR.md:20 — "17 scenarios pass"; the doc's own table lists 8.
• BUILD.bazel:540-544 — describes 6 targets as blocked pending crates that "do not yet have Bazel targets"; all five are 50 lines below at :594-645.
• wit/README.md:14-19 — omits wit/param/service.wit, which IS generated and drift-gated, under an intro promising "every file maps to a world, a crate, or a generator". The mirror image of the stale "spar-derived" comment already fixed in v1.138.
• falcon-hello-demo.sh:21 — documents default port 14700; actual is a random free even base in [20000, 39000). A bench operator opens the wrong firewall ports.
• examples/falcon-sitl-hover --help hides two working scenarios (untethered, geofence).

A method note worth keeping

One near-miss false positive: wasm/cm/cascade/Cargo.toml:22 cites
audit-component-deps.rs as an active gate, and grep -rn "audit-component-deps" .github/
returns nothing — which looks like a phantom gate. It is real, one
indirection away: FV-FALCON-WASMEQ-002.yaml:53 carries it as a run: step and
verification-gate.yml:162 installs rust-script to execute it.

Gates in this repo are often not in the workflow files. Any future audit
must check the rivet artifacts too before calling a gate absent.