Add wireframe-verification crate with placeholder Stateright model#527
Draft
Add wireframe-verification crate with placeholder Stateright model#527
Conversation
…aceholder Stateright model - Add `crates/wireframe-verification` as an internal crate for formal verification. - Include a small semantic placeholder connection model using Stateright. - Provide a shared bounded-checker harness and integration tests with rstest. - Update root workspace manifest to include the verification crate without widening default members. - Update documentation and regression tests to reflect new verification crate and workspace changes. - Align stateright dependency to 0.31.0 and use normal wireframe features to ensure compatibility. This foundational change introduces the dedicated formal verification crate to the workspace, enabling subsequent roadmap items to build more detailed connection actor models and verification tooling. Co-authored-by: devboxerhub[bot] <devboxerhub[bot]@users.noreply.github.com>
Contributor
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
Contributor
Reviewer's GuideIntroduces a new internal crate Sequence diagram for asserting Stateright properties via the shared harnesssequenceDiagram
actor Developer
participant TestRunner
participant ConnectionActorTest
participant VerificationHarness as VerificationHarnessHelpers
participant Model as PlaceholderConnectionModel
participant Stateright as Checker
Developer->>TestRunner: cargo test -p wireframe-verification
TestRunner->>ConnectionActorTest: run tests
ConnectionActorTest->>Model: create PlaceholderConnectionModel::default()
ConnectionActorTest->>VerificationHarness: assert_model_properties(model)
VerificationHarness->>VerificationHarness: create VerificationBounds::default()
VerificationHarness->>VerificationHarness: checker(model, bounds)
VerificationHarness->>Stateright: spawn_bfs()
Stateright-->>VerificationHarness: Checker result
VerificationHarness->>Stateright: assert_properties()
Stateright-->>VerificationHarness: all properties hold
VerificationHarness-->>ConnectionActorTest: return
ConnectionActorTest-->>TestRunner: test pass
TestRunner-->>Developer: report success
Class diagram for wireframe-verification placeholder connection model and harnessclassDiagram
class ActiveOutput {
<<enum>>
Idle
Response
MultiPacket
}
class ConnectionState {
+u8 steps
+bool high_priority_queued
+bool low_priority_queued
+bool fairness_allows_low
+ActiveOutput active_output
+bool shutdown_requested
+bool emitted_high_priority
+bool emitted_low_priority
+bool response_completed
+bool multi_packet_completed
+bool shutdown_during_output
+u8 multi_packet_terminal_count
}
class ConnectionAction {
<<enum>>
EnqueueHigh
EnqueueLow
InstallResponse
InstallMultiPacket
EmitQueued
EmitActiveFrame
CompleteActiveOutput
Shutdown
TickFairness
}
class PlaceholderConnectionModel {
-u8 max_steps
+PlaceholderConnectionModel()
+PlaceholderConnectionModel new(max_steps u8)
+Vec~ConnectionState~ init_states()
+void actions(state ConnectionState, actions Vec~ConnectionAction~)
+Option~ConnectionState~ next_state(state ConnectionState, action ConnectionAction)
+Vec~Property~ properties()
+bool within_boundary(state ConnectionState)
}
class VerificationBounds {
+usize max_depth
+usize max_state_count
+VerificationBounds()
}
class VerificationHarnessHelpers {
<<utility>>
+CheckerBuilder~PlaceholderConnectionModel~ checker(model PlaceholderConnectionModel, bounds VerificationBounds)
+void assert_model_properties(model PlaceholderConnectionModel)
+void assert_model_properties_with_bounds(model PlaceholderConnectionModel, bounds VerificationBounds)
}
ActiveOutput <.. ConnectionState : uses
ConnectionAction <.. PlaceholderConnectionModel : uses
ConnectionState <.. PlaceholderConnectionModel : uses
VerificationBounds <.. VerificationHarnessHelpers : uses
PlaceholderConnectionModel <.. VerificationHarnessHelpers : uses
File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
![codescene-delta-analysis[bot]](https://avatars.githubusercontent.com/in/53921?s=60&v=4){kind=small}
There was a problem hiding this comment.
Gates Failed
(1 file with Bumpy Road Ahead)
(1 file with Complex Method, Complex Conditional)
Gates Passed
See analysis details in CodeScene
Reason for failure
| Enforce critical code health rules | Violations | Code Health Impact | |
|---|---|---|---|
| model.rs | 1 critical rule | 9.11 | Suppress |
| Enforce advisory code health rules | Violations | Code Health Impact | |
|---|---|---|---|
| model.rs | 2 advisory rules | 9.11 | Suppress |
Quality Gate Profile: Pay Down Tech Debt
Install CodeScene MCP: safeguard and uplift AI-generated code. Catch issues early with our IDE extension and CLI tool.
Comment on lines
+42
to
+122
| 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, | ||
| } | ||
| } |
There was a problem hiding this comment.
❌ New issue: Complex Method
Model.next_state has a cyclomatic complexity of 19, threshold = 9
Comment on lines
+77
to
+78
| if state.low_priority_queued | ||
| && (!state.high_priority_queued || state.fairness_allows_low) => |
There was a problem hiding this comment.
❌ New issue: Complex Conditional
Model.next_state has 1 complex conditionals with 2 branches, threshold = 2
Comment on lines
+42
to
+122
| 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, | ||
| } | ||
| } |
There was a problem hiding this comment.
❌ New issue: Bumpy Road Ahead
Model.next_state has 3 blocks with nested conditional logic. Any nesting of 2 or deeper is considered. Threshold is 2 blocks per function
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Introduce an internal crate for formal verification support:
crates/wireframe-verification. It provides a shared Stateright harness, a placeholder connection model, and tests to exercise the verification workflow. This lays the groundwork for roadmap item 15.1.2 and later extensions toward the real ConnectionActor model.Changes
crates/wireframe-verificationCargo.toml: addcrates/wireframe-verificationto workspace members; keep default member as rootdocs/execplans/15-1-2-wireframe-verification-crate.mddescribing purpose, constraints, and validation goalsdocs/formal-verification-methods-in-wireframe.md,docs/roadmap.md, and related sections to reflect the new cradle and its scopeWhy
This implements the 15.1.2 milestone: an internal, non-published crate to host Stateright models and a reusable bounded-checker harness, enabling safe, repeatable verification workflows while the real ConnectionActor model matures in follow-up roadmap items.
How to test
Next steps
Validation plan (from ExecPlan)
cargo test -p wireframe-verificationpassespublish = false)◳ Generated by DevBoxer ◰
ℹ️ Tag @devboxerhub to ask questions and address PR feedback
📎 Task: https://www.devboxer.com/task/7849551b-1b21-4381-a196-34d9041706d2
Summary by Sourcery
Introduce an internal
wireframe-verificationcrate for Stateright-based formal models and a shared verification harness, and wire it into the workspace, tests, and documentation as the home for connection-actor verification work.New Features:
wireframe-verificationcrate providing a placeholder connection-actor Stateright model and shared bounded-checker harness.Enhancements:
Build:
Cargo.tomlworkspace members to includecrates/wireframe-verificationwithout changing default members.Documentation:
wireframedependency features and workspace metadata behavior after adding the verification crate.Tests:
rstest.