chore: workspace cfg(kani) lint config + v1.0 rollout audit#47
Conversation
…rename PR #44 (Dependabot upgrade from wasmtime-wasi 27 to 45) merged with main still importing wasmtime_wasi::preview1, breaking all CI jobs that hit witness-wasi-harness compile (Test ubuntu/macos/windows, llvm-cov, Verification gate). Diagnosis: wasmtime-wasi 44 renamed the module preview1 → p1; the type WasiP1Ctx now lives at wasmtime_wasi::p1::WasiP1Ctx. The fix is a single import line: -use wasmtime_wasi::preview1::{self, WasiP1Ctx}; +use wasmtime_wasi::p1::{self as preview1, WasiP1Ctx}; The 'as preview1' alias keeps the rest of the file unchanged. Also: Cargo.toml bumped to wasmtime = '45' / wasmtime-wasi = '45' to match main's actual resolution (PR #44 only updated wasmtime-wasi, not wasmtime; the two MUST stay in lock-step or wasmtime trait impls don't satisfy the wasmtime-wasi signatures). Verification: - cargo build -p witness-wasi-harness --tests → green. - cargo test --workspace --all-targets → 405 passing (preserved). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three small cleanups for trailing-edge tidiness: 1. **cfg(kani) warnings** — every engine using #[cfg(kani)] for its Kani model-checker harness was emitting an 'unexpected_cfgs' warning on every cargo build (default rustc behavior). Added a workspace-level [workspace.lints.rust] check-cfg = ['cfg(kani)'] declaration; engines inherit via [lints] workspace = true. Build noise gone, kani path still recognised. Crates wired: ccsds, cfdp, ci, cs, ds, fm, hk, hs, lc, md, mm, nid, sc, sca, sch, tbl, to. 2. **v1.0 rollout audit** — removed 'Check-It qualified checkers' line. Check-It was pre-v0.7 aspirational; it isn't in the actual PulseEngine toolchain (rivet/spar/witness/sigil/meld/synth/loom/kiln/smithy/wohl). Replaced with the v0.14.3-derived TQ-record path (DO-330-grade Tool Qualification Reports for Verus/Kani/miri/witness/spar). 3. **Inherited from cherry-pick of v0.19.2 fix** — wasmtime-wasi 45's preview1 → p1 rename. Required because PR #44 (Dependabot 27→45) landed without updating the harness import. Identical to the fix on v0.19.2 branch; whichever lands first carries it. Verification: - cargo build --workspace → 0 cfg(kani) warnings (was 17). - cargo test --workspace --all-targets → 405 passing. - rivet validate → PASS. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 1 test test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 16 filtered out; finished in 0.02s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.06s [falcon-hello-demo] building release binary... running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.05s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 16 tests test result: ok. 16 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.78s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 5 tests test result: ok. 5 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s --- noise=0 (deterministic) --- running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.05s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.07s running 7 tests test result: ok. 7 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 9 tests test result: ok. 9 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.07s Kani-TQ.md running 20 tests test result: ok. 20 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 20 tests test result: ok. 20 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.29s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 1 test test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 16 filtered out; finished in 0.04s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s falcon-hitl-rfspoof: backend=stub duration=5s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.11s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.07s --- scenario: attitude --- running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 10 tests test result: ok. 10 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 7 tests test result: ok. 7 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s falcon-sitl-gz: backend=mock scenario=hover duration=5s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.04s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 13 tests test result: ok. 13 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.60s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s running 17 tests test result: ok. 17 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.07s --- scenario: step --- running 55 tests test result: ok. 55 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.03s running 0 tests test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s Filename Regions Missed Regions Cover Functions Missed Functions Executed Lines Missed Lines Cover Branches Missed Branches Covercoverage_subjects/geofence_subject_rs/src/lib.rs 48 48 0.00% 5 5 0.00% 23 23 0.00% 0 0 -
|
| count | |
|---|---|
| Passed | 27 |
| Failed | -2 |
| Skipped (bench-only — needs hardware / sim) | 7 |
| Skipped (no steps) | 2 |
Failed artifacts
Bench-only artifacts (not run by CI)
FV-FALCON-ARCH-002— spar codegen --format wit recheck — works at v0.10.0 (v0.15.0)FV-FALCON-SIM-001— PX4-SITL end-to-end loop — recipe + preset + smoke (v0.14.0)FV-FALCON-COV-001— witness MC/DC structural coverage — falcon pipeline wired (v0.13)FV-FALCON-GEO-003— Geofence safety path — miri UB/overflow check (v0.12, AI substitute)FV-FALCON-ARCH-001— spar AADL architectural model — falcon cascade (v0.13)FV-FALCON-SIM-005— gz-transport NavSat + Home projection — position-dependent loops (v0.18.1)FV-FALCON-COV-003— witness MC/DC on real Rust source — Geofence subject (v0.14.1)
Source of truth: artifacts/verification/FV-FALCON-*.yaml.
1 participant
Summary
Three trailing-edge cleanups noticed during v0.19.0–v0.19.2 work.
1. cfg(kani) warnings silenced
Every engine using `#[cfg(kani)]` for its Kani model-checker harness was emitting an `unexpected_cfgs` warning on every `cargo build`. Added a workspace-level lint config:
```toml
[workspace.lints.rust]
unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
```
Each engine inherits via `[lints] workspace = true`. 17 crates wired (ccsds, cfdp, ci, cs, ds, fm, hk, hs, lc, md, mm, nid, sc, sca, sch, tbl, to). Build noise gone, kani path still recognised under `cargo kani`.
2. v1.0 rollout audit
Removed `Check-It qualified checkers` line. Check-It was pre-v0.7 aspirational; it isn't in the actual PulseEngine toolchain (rivet/spar/witness/sigil/meld/synth/loom/kiln/smithy/wohl). Replaced with the v0.14.3-derived TQ-record path: DO-330-grade Tool Qualification Reports for Verus/Kani/miri/witness/spar.
3. wasmtime-wasi preview1 → p1 (cherry-pick from v0.19.2 PR #46)
PR #44 (Dependabot upgrade of wasmtime-wasi 27 → 45) merged with main still importing the old `preview1` module path. Witness-wasi-harness needs to use `p1` instead. Identical fix shipped on the v0.19.2 PR #46; whichever lands first carries it (the other becomes a no-op via cherry-pick deduplication on rebase).
Verification
🤖 Generated with Claude Code