From 67a10e9a480e94e7d60ccb21bfad7c469714b15f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 27 May 2026 06:19:58 +0200 Subject: [PATCH 1/2] =?UTF-8?q?fix(witness-wasi-harness):=20update=20for?= =?UTF-8?q?=20wasmtime-wasi=2045=20preview1=20=E2=86=92=20p1=20rename?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- host/witness-wasi-harness/Cargo.toml | 2 +- host/witness-wasi-harness/src/main.rs | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/host/witness-wasi-harness/Cargo.toml b/host/witness-wasi-harness/Cargo.toml index 8c9b6a3..8a084ed 100644 --- a/host/witness-wasi-harness/Cargo.toml +++ b/host/witness-wasi-harness/Cargo.toml @@ -12,7 +12,7 @@ name = "witness-wasi-harness" path = "src/main.rs" [dependencies] -wasmtime = "27" +wasmtime = "45" wasmtime-wasi = "45" anyhow = "1" serde_json = "1" diff --git a/host/witness-wasi-harness/src/main.rs b/host/witness-wasi-harness/src/main.rs index 54fa940..a858ba6 100644 --- a/host/witness-wasi-harness/src/main.rs +++ b/host/witness-wasi-harness/src/main.rs @@ -27,7 +27,11 @@ use std::env; use std::fs; use std::path::PathBuf; use wasmtime::{Config, Engine, Linker, Module, Store, Val}; -use wasmtime_wasi::preview1::{self, WasiP1Ctx}; +// wasmtime-wasi 44 renamed `preview1` → `p1`; bound here as `preview1` +// so the rest of the file keeps reading naturally. PR #44 (Dependabot +// 27→45 upgrade) merged with main still importing the old path; v0.19.2 +// catches it up. +use wasmtime_wasi::p1::{self as preview1, WasiP1Ctx}; use wasmtime_wasi::WasiCtxBuilder; /// `witness-harness-v1` schema — keys are decimal branch IDs as From 39fd85779269e3845ccca2384257cd2e8cfb9088 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 27 May 2026 06:31:02 +0200 Subject: [PATCH 2/2] chore: workspace cfg(kani) lint suppression + v1.0 rollout audit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- Cargo.toml | 9 +++++++++ artifacts/features/FEAT-FALCON-rollout.yaml | 12 ++++++++---- crates/relay-ccsds/Cargo.toml | 3 +++ crates/relay-cfdp/Cargo.toml | 3 +++ crates/relay-ci/Cargo.toml | 3 +++ crates/relay-cs/Cargo.toml | 3 +++ crates/relay-ds/Cargo.toml | 3 +++ crates/relay-fm/Cargo.toml | 3 +++ crates/relay-hk/Cargo.toml | 3 +++ crates/relay-hs/Cargo.toml | 3 +++ crates/relay-lc/Cargo.toml | 3 +++ crates/relay-md/Cargo.toml | 3 +++ crates/relay-mm/Cargo.toml | 3 +++ crates/relay-nid/Cargo.toml | 3 +++ crates/relay-sc/Cargo.toml | 3 +++ crates/relay-sca/Cargo.toml | 3 +++ crates/relay-sch/Cargo.toml | 3 +++ crates/relay-tbl/Cargo.toml | 3 +++ crates/relay-to/Cargo.toml | 3 +++ 19 files changed, 68 insertions(+), 4 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index dfb9555..492574d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -51,6 +51,15 @@ rust-version = "1.85.0" wit-bindgen = { version = "0.57.1", default-features = false } proptest = "1" +# Workspace-wide lint config. Engines use `#[cfg(kani)]` for the Kani +# model-checker harness paths (they're built only under `cargo kani`, +# which sets the `kani` cfg). Stable rustc sees the cfg as unexpected +# and warns by default — declare it here so all member crates inherit +# the check-cfg whitelist without per-crate boilerplate. Member crates +# pick this up via `[lints] workspace = true` in their own Cargo.toml. +[workspace.lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } + # All guest components are no_std + no alloc. # Memory comes from Kiln's capability-based allocator (safe_managed_alloc!) # or from Gale's mem_slab / heap on embedded targets. diff --git a/artifacts/features/FEAT-FALCON-rollout.yaml b/artifacts/features/FEAT-FALCON-rollout.yaml index f3a4264..d119602 100644 --- a/artifacts/features/FEAT-FALCON-rollout.yaml +++ b/artifacts/features/FEAT-FALCON-rollout.yaml @@ -1591,9 +1591,11 @@ artifacts: status: pending description: > Full overdo matrix green across all six safety domains in - rivet validate output. Check-It checkers qualified for the - EKF and mixer (DO-330 path). falcon-coax and falcon-hex - variants ship alongside falcon-quad. + rivet validate output. Tool-qualification records (v0.14.3 + pattern) extended to DO-330-grade per tool. falcon-coax and + falcon-hex airframe variants ship alongside falcon-quad. + All bench-evidence artifacts (PX4-SITL + gz-sim) carry + reproducible setup recipes + signed manifests. Ships: - DO-178C DAL-A credit bundle @@ -1604,7 +1606,9 @@ artifacts: - EN 50128 SIL-4 credit bundle - falcon-coax world spec (Ingenuity-class) - falcon-hex world spec (fault-tolerant) - - Check-It qualified checkers for EKF + mixer + - DO-330-grade tool qualification reports for Verus / Kani + / miri / witness / spar (extends v0.14.3's auditable + starting-point TQ docs). v1.0 is when the evidence dossier clears the bar — not when the features are complete. v2.x adds falcon-vtol and diff --git a/crates/relay-ccsds/Cargo.toml b/crates/relay-ccsds/Cargo.toml index b2d676b..9710064 100644 --- a/crates/relay-ccsds/Cargo.toml +++ b/crates/relay-ccsds/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-cfdp/Cargo.toml b/crates/relay-cfdp/Cargo.toml index b2c93e5..d11e18d 100644 --- a/crates/relay-cfdp/Cargo.toml +++ b/crates/relay-cfdp/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-ci/Cargo.toml b/crates/relay-ci/Cargo.toml index da7cb53..095d8df 100644 --- a/crates/relay-ci/Cargo.toml +++ b/crates/relay-ci/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-cs/Cargo.toml b/crates/relay-cs/Cargo.toml index 975be0f..e194b12 100644 --- a/crates/relay-cs/Cargo.toml +++ b/crates/relay-cs/Cargo.toml @@ -17,3 +17,6 @@ wit-bindgen = { workspace = true, default-features = false } # no_std + no alloc: WASM components run in bounded memory. # All allocation through Kiln capability system or static buffers. + +[lints] +workspace = true diff --git a/crates/relay-ds/Cargo.toml b/crates/relay-ds/Cargo.toml index 7e9d4a0..25c63ee 100644 --- a/crates/relay-ds/Cargo.toml +++ b/crates/relay-ds/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-fm/Cargo.toml b/crates/relay-fm/Cargo.toml index 278a288..29109e0 100644 --- a/crates/relay-fm/Cargo.toml +++ b/crates/relay-fm/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-hk/Cargo.toml b/crates/relay-hk/Cargo.toml index 191ba79..a6cd2e3 100644 --- a/crates/relay-hk/Cargo.toml +++ b/crates/relay-hk/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-hs/Cargo.toml b/crates/relay-hs/Cargo.toml index 13452b5..7770afd 100644 --- a/crates/relay-hs/Cargo.toml +++ b/crates/relay-hs/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-lc/Cargo.toml b/crates/relay-lc/Cargo.toml index cb138e8..905c8e3 100644 --- a/crates/relay-lc/Cargo.toml +++ b/crates/relay-lc/Cargo.toml @@ -22,3 +22,6 @@ relay-primitives = { path = "../relay-primitives" } [dev-dependencies] proptest.workspace = true + +[lints] +workspace = true diff --git a/crates/relay-md/Cargo.toml b/crates/relay-md/Cargo.toml index 6e9f4cc..d71ce8f 100644 --- a/crates/relay-md/Cargo.toml +++ b/crates/relay-md/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-mm/Cargo.toml b/crates/relay-mm/Cargo.toml index 6878476..0b93037 100644 --- a/crates/relay-mm/Cargo.toml +++ b/crates/relay-mm/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-nid/Cargo.toml b/crates/relay-nid/Cargo.toml index 7886a2a..20d4a9b 100644 --- a/crates/relay-nid/Cargo.toml +++ b/crates/relay-nid/Cargo.toml @@ -23,3 +23,6 @@ crate-type = ["rlib"] [dev-dependencies] proptest.workspace = true + +[lints] +workspace = true diff --git a/crates/relay-sc/Cargo.toml b/crates/relay-sc/Cargo.toml index aec44be..ec1668a 100644 --- a/crates/relay-sc/Cargo.toml +++ b/crates/relay-sc/Cargo.toml @@ -17,3 +17,6 @@ wit-bindgen = { workspace = true, default-features = false } [dev-dependencies] proptest.workspace = true + +[lints] +workspace = true diff --git a/crates/relay-sca/Cargo.toml b/crates/relay-sca/Cargo.toml index 02f9320..61c47fd 100644 --- a/crates/relay-sca/Cargo.toml +++ b/crates/relay-sca/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-sch/Cargo.toml b/crates/relay-sch/Cargo.toml index fed6130..263de0f 100644 --- a/crates/relay-sch/Cargo.toml +++ b/crates/relay-sch/Cargo.toml @@ -20,3 +20,6 @@ wit-bindgen = { workspace = true, default-features = false } [dev-dependencies] proptest.workspace = true + +[lints] +workspace = true diff --git a/crates/relay-tbl/Cargo.toml b/crates/relay-tbl/Cargo.toml index 8eb5770..bf8ae7e 100644 --- a/crates/relay-tbl/Cargo.toml +++ b/crates/relay-tbl/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true diff --git a/crates/relay-to/Cargo.toml b/crates/relay-to/Cargo.toml index 1aff8ef..f3cd5cb 100644 --- a/crates/relay-to/Cargo.toml +++ b/crates/relay-to/Cargo.toml @@ -14,3 +14,6 @@ crate-type = ["rlib"] [dependencies] wit-bindgen = { workspace = true, default-features = false } + +[lints] +workspace = true