Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 29 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -313,3 +313,32 @@ jobs:
env:
CARGO_BAZEL_REPIN: "1"
run: bazel build //:all

# SWARCH-WOHL-008 C4 execution gate: prove the verified Matter core
# actually RUNS — not just builds — by executing a full SPAKE2+ PASE
# handshake across the wac_compose'd WIT boundary inside wasmtime. The
# composed component (//:wohl-matter-composed) exports a bare `run`
# world func returning true on handshake success; `wasmtime run
# --invoke 'run()'` reaches it (interface-nested exports are not
# CLI-invokable, hence the bare shape). Turns the locally-proven
# spike2c result into a live CI gate.
- name: Run composed PASE handshake under wasmtime (C4 execution gate)
working-directory: wohl
run: |
set -euo pipefail
bazel build //:wohl-matter-composed
WASM=$(find "$(bazel info bazel-bin)" -name 'wohl-matter-composed.wasm' | head -1)
test -n "$WASM"
# Reuse the wasmtime the rules_wasm_component toolchain already
# fetched (integrity-verified by bazel via MODULE.bazel.lock) — no
# unpinned curl|bash download of an external install script.
WT=$(find "$(bazel info output_base)/external" -type f -name wasmtime -path '*wasmtime*' 2>/dev/null | head -1)
echo "composed=$WASM wasmtime=$WT"
test -n "$WT"
OUT=$("$WT" run --invoke 'run()' "$WASM")
echo "run() => $OUT"
if [ "$OUT" != "true" ]; then
echo "::error::PASE handshake did NOT succeed in the composed graph"
exit 1
fi
echo "PASE-RUNS-OK in CI: SPAKE2+ handshake completed across the wac-composed WIT seam"
65 changes: 65 additions & 0 deletions BUILD.bazel
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
load("@rules_wasm_component//rust:defs.bzl", "rust_wasm_component_bindgen")
load("@rules_wasm_component//wac:defs.bzl", "wac_plug")
load("@rules_wasm_component//wit:defs.bzl", "wit_library")

package(default_visibility = ["//visibility:public"])
Expand Down Expand Up @@ -155,3 +156,67 @@ rust_wasm_component_bindgen(
wasi_version = "p3",
profiles = ["release"],
)

# ═══════════════════════════════════════════════════════════════
# Matter verified-core COMPOSED graph (SWARCH-WOHL-008 C4 landing)
#
# Bazel / rules_wasm_component landing of the locally-proven
# spike2c-compose graph (PASE handshake runs across a wac_compose'd WIT
# boundary). Two components over the `wire` seam (wasi p2 = sync, busy-
# polled by the core's block_on executor):
# - matter-transport-shell exports `wire` (the host packet queues)
# - wohl-matter-core-composed imports `wire`, exports `run` (the PASE
# handshake; returns true on success)
# composed via wac_compose. Landed incrementally — transport shell first.
# ═══════════════════════════════════════════════════════════════

wit_library(
name = "matter_compose_wit",
srcs = ["crates/wohl-matter-core/compose/wit/compose.wit"],
package_name = "wohl:matter-compose",
world = "transport",
)

rust_wasm_component_bindgen(
name = "wohl-matter-transport",
srcs = ["crates/wohl-matter-core/compose/src/transport.rs"],
# No `world` attr here — rust_wasm_component_bindgen forwards kwargs to
# rust_shared_library, which has no `world`. The bound world is selected
# by the wit_library above (world = "transport").
wit = ":matter_compose_wit",
profiles = ["release"],
)

# Same compose.wit, but bound to the `matter-core` world (imports wire,
# exports runner). A separate wit_library because the bound world is a
# wit_library attribute, not a bindgen one.
wit_library(
name = "matter_compose_core_wit",
srcs = ["crates/wohl-matter-core/compose/wit/compose.wit"],
package_name = "wohl:matter-compose",
world = "matter-core",
)

rust_wasm_component_bindgen(
name = "wohl-matter-core-composed",
srcs = ["crates/wohl-matter-core/compose/src/mcore.rs"],
wit = ":matter_compose_core_wit",
deps = [
"@wohl_crates//:rs-matter",
"@wohl_crates//:embassy-futures",
"@wohl_crates//:embassy-time-driver",
"@wohl_crates//:critical-section",
],
profiles = ["release"],
)

# Plug the transport shell (exports wire) into the verified core's wire
# import — the bazel realisation of the locally-proven
# `wac plug mcore --plug transport`. The composed component exports the
# runner; a wasmtime step (added next) invokes `run` to prove the PASE
# handshake runs across the seam in CI.
wac_plug(
name = "wohl-matter-composed",
plugs = [":wohl-matter-transport"],
socket = ":wohl-matter-core-composed",
)
26 changes: 19 additions & 7 deletions artifacts/swarch/SWARCH-WOHL-008.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ artifacts:
- id: SWARCH-WOHL-008
type: sw-arch-component
title: "Matter verified-core split: protocol+crypto in a WASM component"
status: proposed
status: approved
description: >
Architectural decision (0.3.0, next version) that refines the
SWARCH-WOHL-007 rs-matter integration shape in light of Spike 2.
Expand Down Expand Up @@ -45,12 +45,24 @@ artifacts:
seam added to the AADL (Wohl_Matter::MatterBridgeProcess). The
host shell and the verified core compose via wac_compose.

STATUS: proposed. Compile is CI-gated (PR #35). Execution is
locally reproduced (PR #36 harness, cargo wasip2 + wasmtime) but
not yet a CI gate, and the wac_compose graph + rules_wasm_component
landing are not yet built. Promotes to approved when the composed
graph builds via rules_wasm_component AND a wasmtime execution of
the PASE handshake runs in CI (see SWV-MATTER-002).
STATUS: approved. Both promotion criteria are met and CI-gated:
(1) the composed graph builds via rules_wasm_component
(//:wohl-matter-transport + //:wohl-matter-core-composed plugged via
wac_plug into //:wohl-matter-composed), and (2) a wasmtime execution
step runs the full SPAKE2+ PASE handshake on the composed component
(`wasmtime run --invoke 'run()'` -> true) on every PR — proving the
verified protocol+crypto core RUNS across a wac-composed WIT boundary
built by the production toolchain. (Compile was already CI-gated by
PR #35.)

REFINEMENT STILL OWED (does not block this decision — the claim is
about WHERE the code runs and HOW it is built, not the exact WIT
signatures): the landed seam is a simplified channelled `wire`
interface, not yet the exact spar-generated matter-world seam
(on-message_in/emit-message_out + on-clock_in + on-entropy_in), and
clock/entropy are still core-internal rather than crossing their own
seam funcs. Binding the faithful spar seam is tracked in
SWV-MATTER-002 (C5/refinement).
tags: [architecture, matter, rs-matter, wasm, verified-core, decision]
fields:
interfaces:
Expand Down
23 changes: 18 additions & 5 deletions artifacts/verification/SWV-MATTER-002.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -40,13 +40,26 @@ artifacts:
stay component-internal — so this proves the architecture is
runnable; the faithful spar-seam binding is part of C4.

- C4 "the composed graph builds via rules_wasm_component and a
wasmtime execution of the PASE handshake runs in CI" — DONE,
CI-GATED. BUILD.bazel defines //:wohl-matter-transport (exports
wire) + //:wohl-matter-core-composed (rs-matter, imports wire,
exports runner.run), plugged via wac_plug into
//:wohl-matter-composed. The bazel-build CI job builds it and runs
`wasmtime run --invoke 'run()'` (toolchain wasmtime), asserting
true — a full SPAKE2+ PASE handshake across the wac-composed WIT
seam, on every PR. This promoted SWARCH-WOHL-008 to approved.
FIDELITY: the seam landed is the simplified channelled `wire`
interface, not yet the exact spar matter-world seam, and
clock/entropy stay core-internal — see the refinement below.

OWED before this artifact can be `approved`:

- C4 "the composed graph builds via rules_wasm_component (binding
the real spar-generated matter-world seam: on-message_in /
emit-message_out + on-clock_in + on-entropy_in) and a
wasmtime execution of the PASE handshake runs in CI" — turns C2
from a local reproduction into a live gate.
- C4b spar-seam fidelity: rebind the composed graph to the exact
spar-generated matter-world seam (on-message_in / emit-message_out
= NetworkReceive / NetworkSend, plus on-clock_in / on-entropy_in)
instead of the simplified `wire` interface, routing clock + entropy
across their own seam funcs.

- C5 MC/DC: SWV-MATTER-001 scoped out witness MC/DC truth tables
because "the bridge runs host-side and is not yet
Expand Down
7 changes: 5 additions & 2 deletions crates/wohl-leak/wasm/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

9 changes: 9 additions & 0 deletions crates/wohl-leak/wasm/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -14,4 +14,13 @@ wit-bindgen = "0.41.0"
# monitors' compiled closure is unchanged. See the
# matter-core-wasm-buildable finding + SWARCH-WOHL-008 (spike).
rs-matter = { git = "https://github.com/project-chip/rs-matter", rev = "0030ba4a99", default-features = false, features = ["rustcrypto"] }
# Direct deps so @wohl_crates exposes them as bindgen `deps` for the
# wohl-matter-core-composed component (SWARCH-WOHL-008 C4). These are already
# transitive via rs-matter, but crate_universe only aliases DIRECT manifest
# deps as @wohl_crates//:<name> targets. embassy-time-driver: the wasip2
# clock driver; embassy-futures: block_on; critical-section/std: the sole
# critical-section impl in the component (rs-matter without `os` provides none).
embassy-futures = "0.1"
embassy-time-driver = "0.2"
critical-section = { version = "1", features = ["std"] }
[workspace]
163 changes: 163 additions & 0 deletions crates/wohl-matter-core/compose/src/mcore.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,163 @@
//! Verified Matter core component (bazel / rules_wasm_component landing of the
//! locally-proven spike2c-compose `mcore`; SWARCH-WOHL-008 C4).
//!
//! Imports the `wire` seam and exports `runner.run`, which drives the same full
//! SPAKE2+ PASE handshake as Spike 2a/2c with every packet crossing the
//! wac-composed WIT boundary into the transport shell. Returns true on success.
//! A CI wasmtime step invokes `run` on the composed graph.
//!
//! Uses the rule-generated bindings (`wohl_matter_core_composed_bindings`),
//! not `wit_bindgen::generate!` — matching the existing components' convention.
//! wasi p2 (sync seam funcs), so the cross-component calls are ordinary
//! synchronous imports from inside rs-matter's async `poll_fn`, busy-polled by
//! `embassy_futures::block_on`.

use core::future::poll_fn;
use core::task::{Poll, Waker};
use std::sync::OnceLock;
use std::time::Instant as StdInstant;

use embassy_futures::block_on;
use embassy_futures::select::{select, Either};

use rs_matter::crypto::test_only_crypto;
use rs_matter::dm::devices::test::{TEST_DEV_ATT, TEST_DEV_COMM, TEST_DEV_DET};
use rs_matter::error::Error;
use rs_matter::respond::Responder;
use rs_matter::sc::pase::{PaseInitiator, MAX_COMM_WINDOW_TIMEOUT_SECS};
use rs_matter::sc::SecureChannel;
use rs_matter::transport::exchange::Exchange;
use rs_matter::transport::network::{
Address, IpAddr, Ipv6Addr, NetworkReceive, NetworkSend, NoNetwork, SocketAddr,
};
use rs_matter::utils::select::Coalesce;
use rs_matter::Matter;

// Export `runner` interface → Guest at exports::…::runner. Import `wire`
// interface → free functions. `wasmtime run --invoke 'run()'` reaches the
// runner.run export in CI.
use wohl_matter_core_composed_bindings::exports::wohl::matter_compose::runner::Guest;
use wohl_matter_core_composed_bindings::wohl::matter_compose::wire;

// ── embassy-time driver (wasip2; see Spike 2a) ──
struct WasiDriver;
static START: OnceLock<StdInstant> = OnceLock::new();
impl embassy_time_driver::Driver for WasiDriver {
fn now(&self) -> u64 {
let start = *START.get_or_init(StdInstant::now);
(start.elapsed().as_nanos() * embassy_time_driver::TICK_HZ as u128 / 1_000_000_000u128)
as u64
}
fn schedule_wake(&self, _at: u64, _waker: &Waker) {}
}
embassy_time_driver::time_driver_impl!(static DRIVER: WasiDriver = WasiDriver);

// ── transport endpoint backed by the imported `wire` seam ──
struct Endpoint {
send_channel: u8,
recv_channel: u8,
peer_addr: Address,
}

impl NetworkSend for &Endpoint {
async fn send_to(&mut self, data: &[u8], _addr: Address) -> Result<(), Error> {
wire::push(self.send_channel, data); // crosses the WIT boundary
Ok(())
}
}

impl NetworkReceive for &Endpoint {
async fn wait_available(&mut self) -> Result<(), Error> {
poll_fn(|_| {
if wire::peek(self.recv_channel) {
Poll::Ready(Ok(()))
} else {
Poll::Pending
}
})
.await
}

async fn recv_from(&mut self, buffer: &mut [u8]) -> Result<(usize, Address), Error> {
poll_fn(|_| match wire::pop(self.recv_channel) {
Some(data) => {
let n = data.len();
buffer[..n].copy_from_slice(&data);
Poll::Ready(Ok((n, self.peer_addr)))
}
None => Poll::Pending,
})
.await
}
}

fn addr(port: u16) -> Address {
Address::Udp(SocketAddr::new(IpAddr::V6(Ipv6Addr::LOCALHOST), port))
}

async fn run_handshake() -> bool {
let device_matter = Matter::new(&TEST_DEV_DET, TEST_DEV_COMM, &TEST_DEV_ATT, 0);
let controller_matter = Matter::new(&TEST_DEV_DET, TEST_DEV_COMM, &TEST_DEV_ATT, 0);
let crypto = test_only_crypto();

let device_addr = addr(5540);
let controller_addr = addr(5541);
let device_ep = Endpoint {
send_channel: 1,
recv_channel: 0,
peer_addr: controller_addr,
};
let controller_ep = Endpoint {
send_channel: 0,
recv_channel: 1,
peer_addr: device_addr,
};

if device_matter
.open_basic_comm_window(MAX_COMM_WINDOW_TIMEOUT_SECS, &crypto, &())
.is_err()
{
return false;
}

let sc = SecureChannel::new(&crypto, &());
let responder = Responder::new("device", sc, &device_matter, 0);
let device_fut = async {
select(
device_matter.run(&crypto, &device_ep, &device_ep, NoNetwork),
responder.run::<4>(),
)
.coalesce()
.await
};

let controller_fut = async {
let transport =
controller_matter.run(&crypto, &controller_ep, &controller_ep, NoNetwork);
let handshake = async {
let mut exchange =
Exchange::initiate_unsecured(&controller_matter, &crypto, device_addr).await?;
PaseInitiator::initiate(&mut exchange, &crypto, 20202021).await?;
Ok::<(), Error>(())
};
match select(transport, handshake).await {
Either::First(_) => Err::<(), Error>(rs_matter::error::ErrorCode::Invalid.into()),
Either::Second(r) => r,
}
};

matches!(
select(device_fut, controller_fut).await,
Either::Second(Ok(()))
)
}

struct Component;

impl Guest for Component {
fn run() -> bool {
block_on(run_handshake())
}
}

wohl_matter_core_composed_bindings::export!(Component with_types_in wohl_matter_core_composed_bindings);
Loading
Loading