Add wireframe-verification crate with placeholder Stateright model

Cargo.toml

@@ -11,7 +11,7 @@ categories = ["network-programming", "asynchronous"]
 documentation = "https://docs.rs/wireframe"
 
 [workspace]
-members = ["."]
+members = [".", "crates/wireframe-verification"]
 default-members = ["."]
 resolver = "3"
 

crates/wireframe-verification/Cargo.toml

@@ -0,0 +1,12 @@
+[package]
+name = "wireframe-verification"
+version = "0.1.0"
+edition = "2024"
+publish = false
+
+[dependencies]
+stateright = "0.31.0"
+wireframe = { path = "../..", features = ["test-support"] }
+
+[dev-dependencies]
+rstest = "0.26.1"

crates/wireframe-verification/src/connection_model/action.rs

@@ -0,0 +1,15 @@
+//! Actions in the placeholder connection-actor model.
+
+/// Nondeterministic events for the placeholder connection model.
+#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
+pub enum ConnectionAction {
+    EnqueueHigh,
+    EnqueueLow,
+    InstallResponse,
+    InstallMultiPacket,
+    EmitQueued,
+    EmitActiveFrame,
+    CompleteActiveOutput,
+    Shutdown,
+    TickFairness,
+}

crates/wireframe-verification/src/connection_model/mod.rs

@@ -0,0 +1,14 @@
+//! Placeholder Stateright model for the connection actor roadmap.
+//!
+//! The first milestone keeps the model intentionally small: it exercises the
+//! shared harness and encodes a few semantic invariants that later roadmap
+//! items can refine toward the real `ConnectionActor`.
+
+mod action;
+mod model;
+mod properties;
+mod state;
+
+pub use action::ConnectionAction;
+pub use model::PlaceholderConnectionModel;
+pub use state::{ActiveOutput, ConnectionState};

crates/wireframe-verification/src/connection_model/model.rs

@@ -0,0 +1,127 @@
+//! Stateright model implementation for the placeholder connection actor.
+
+use stateright::{Model, Property};
+
+use super::{ConnectionAction, ConnectionState, properties::properties, state::ActiveOutput};
+
+/// Small semantic model used to land the verification crate and shared harness.
+#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+pub struct PlaceholderConnectionModel {
+    max_steps: u8,
+}
+
+impl Default for PlaceholderConnectionModel {
+    fn default() -> Self { Self { max_steps: 6 } }
+}
+
+impl PlaceholderConnectionModel {
+    /// Create a model with an explicit state-space depth bound.
+    pub fn new(max_steps: u8) -> Self { Self { max_steps } }
+}
+
+impl Model for PlaceholderConnectionModel {
+    type State = ConnectionState;
+    type Action = ConnectionAction;
+
+    fn init_states(&self) -> Vec<Self::State> { vec![ConnectionState::default()] }
+
+    fn actions(&self, _state: &Self::State, actions: &mut Vec<Self::Action>) {
+        actions.extend([
+            ConnectionAction::EnqueueHigh,
+            ConnectionAction::EnqueueLow,
+            ConnectionAction::InstallResponse,
+            ConnectionAction::InstallMultiPacket,
+            ConnectionAction::EmitQueued,
+            ConnectionAction::EmitActiveFrame,
+            ConnectionAction::CompleteActiveOutput,
+            ConnectionAction::Shutdown,
+            ConnectionAction::TickFairness,
+        ]);
+    }
+
+    fn next_state(&self, state: &Self::State, action: Self::Action) -> Option<Self::State> {
+        let mut next = state.clone();
+        next.steps = next.steps.saturating_add(1);
+
+        match action {
+            ConnectionAction::EnqueueHigh if !state.high_priority_queued => {
+                next.high_priority_queued = true;
+                Some(next)
+            }
+            ConnectionAction::EnqueueLow if !state.low_priority_queued => {
+                next.low_priority_queued = true;
+                Some(next)
+            }
+            ConnectionAction::InstallResponse
+                if !state.shutdown_requested
+                    && matches!(state.active_output, ActiveOutput::Idle) =>
+            {
+                next.active_output = ActiveOutput::Response;
+                Some(next)
+            }
+            ConnectionAction::InstallMultiPacket
+                if !state.shutdown_requested
+                    && matches!(state.active_output, ActiveOutput::Idle) =>
+            {
+                next.active_output = ActiveOutput::MultiPacket;
+                next.multi_packet_terminal_count = 0;
+                Some(next)
+            }
+            ConnectionAction::EmitQueued if state.high_priority_queued => {
+                next.high_priority_queued = false;
+                next.emitted_high_priority = true;
+                next.fairness_allows_low = true;
+                Some(next)
+            }
+            ConnectionAction::EmitQueued
+                if state.low_priority_queued
+                    && (!state.high_priority_queued || state.fairness_allows_low) =>
+            {
+                next.low_priority_queued = false;
+                next.emitted_low_priority = true;
+                next.fairness_allows_low = false;
+                Some(next)
+            }
+            ConnectionAction::EmitActiveFrame
+                if !matches!(state.active_output, ActiveOutput::Idle) =>
+            {
+                if state.shutdown_requested {
+                    next.shutdown_during_output = true;
+                }
+                Some(next)
+            }
+            ConnectionAction::CompleteActiveOutput
+                if matches!(state.active_output, ActiveOutput::Response) =>
+            {
+                next.active_output = ActiveOutput::Idle;
+                next.response_completed = true;
+                Some(next)
+            }
+            ConnectionAction::CompleteActiveOutput
+                if matches!(state.active_output, ActiveOutput::MultiPacket) =>
+            {
+                next.active_output = ActiveOutput::Idle;
+                next.multi_packet_completed = true;
+                next.multi_packet_terminal_count =
+                    next.multi_packet_terminal_count.saturating_add(1);
+                Some(next)
+            }
+            ConnectionAction::Shutdown if !state.shutdown_requested => {
+                next.shutdown_requested = true;
+                if !matches!(state.active_output, ActiveOutput::Idle) {
+                    next.shutdown_during_output = true;
+                }
+                Some(next)
+            }
+            ConnectionAction::TickFairness if state.low_priority_queued => {
+                next.fairness_allows_low = true;
+                Some(next)
+            }
+            _ => None,
+        }
+    }
+
+    fn properties(&self) -> Vec<Property<Self>> { properties() }
+
+    fn within_boundary(&self, state: &Self::State) -> bool { state.steps <= self.max_steps }
+}

crates/wireframe-verification/src/connection_model/properties.rs

@@ -0,0 +1,69 @@
+//! Properties checked against the placeholder connection model.
+
+use stateright::Property;
+
+use super::{ConnectionState, PlaceholderConnectionModel};
+
+pub(super) fn properties() -> Vec<Property<PlaceholderConnectionModel>> {
+    vec![
+        Property::always(
+            "active output remains exclusive",
+            active_output_is_exclusive,
+        ),
+        Property::always(
+            "multi-packet terminator stays single",
+            multi_packet_terminator_is_single,
+        ),
+        Property::sometimes(
+            "high-priority output can make progress",
+            high_priority_progress,
+        ),
+        Property::sometimes(
+            "low-priority output can make progress",
+            low_priority_progress,
+        ),
+        Property::sometimes("response output can complete", response_completion),
+        Property::sometimes("multi-packet output can complete", multi_packet_completion),
+        Property::sometimes(
+            "shutdown can race an active output",
+            shutdown_races_active_output,
+        ),
+    ]
+}
+
+fn active_output_is_exclusive(
+    _model: &PlaceholderConnectionModel,
+    _state: &ConnectionState,
+) -> bool {
+    true
+}
+
+fn multi_packet_terminator_is_single(
+    _model: &PlaceholderConnectionModel,
+    state: &ConnectionState,
+) -> bool {
+    state.multi_packet_terminal_count <= 1
+}
+
+fn high_priority_progress(_model: &PlaceholderConnectionModel, state: &ConnectionState) -> bool {
+    state.emitted_high_priority
+}
+
+fn low_priority_progress(_model: &PlaceholderConnectionModel, state: &ConnectionState) -> bool {
+    state.emitted_low_priority
+}
+
+fn response_completion(_model: &PlaceholderConnectionModel, state: &ConnectionState) -> bool {
+    state.response_completed
+}
+
+fn multi_packet_completion(_model: &PlaceholderConnectionModel, state: &ConnectionState) -> bool {
+    state.multi_packet_completed
+}
+
+fn shutdown_races_active_output(
+    _model: &PlaceholderConnectionModel,
+    state: &ConnectionState,
+) -> bool {
+    state.shutdown_during_output
+}