Add wireframe-verification crate with placeholder Stateright model#527
Open
leynos wants to merge 7 commits into
Open
Add wireframe-verification crate with placeholder Stateright model#527leynos wants to merge 7 commits into
leynos wants to merge 7 commits into
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
|
ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (1)
SummaryThis PR implements roadmap item 15.1.2 by adding an internal Stateright-based verification crate at crates/wireframe-verification, a shared bounded-checker harness, a placeholder connection-actor model, and related workspace, test, and documentation updates. New verification crate
ExecPlan & documentation
Workspace, tests and fixtures
Lint and test-helper adjustments
Complexity & refactor notes (review comments)
How to test / validation
Outcomes
WalkthroughAdd an internal verification crate ChangesVerification Crate Infrastructure & Workspace
Placeholder Connection Model
Verification Tests & Integration
Documentation & ExecPlans
Test Lint/Clippy Adjustments
sequenceDiagram sequenceDiagram
participant Test as Integration Test
participant Harness as Verification Harness
participant Builder as CheckerBuilder
participant Checker as Spawned Checker
participant Model as PlaceholderConnectionModel
Test->>Harness: call assert_model_properties(model)
Harness->>Builder: checker(model, bounds)
Builder->>Checker: spawn_bfs()
Checker->>Model: invoke next_state / actions
Model-->>Checker: return next states / properties
Checker-->>Harness: report results
Harness-->>Test: assert_properties()
Important Pre-merge checks failedPlease resolve all errors before merging. Addressing warnings is optional. ❌ Failed checks (3 warnings, 1 inconclusive)
✅ Passed checks (14 passed)
✨ 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}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Owner
Author
|
@coderabbitai Please suggest a fix for this issue and supply a prompt for an AI coding agent to enable it to apply the fix. Include the file and symbol names indicated in the issue at the head of your response. crates/wireframe-verification/src/connection_model/model.rs 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,
}
}❌ New issue: Complex Method |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Owner
Author
|
@coderabbitai Please suggest a fix for this issue and supply a prompt for an AI coding agent to enable it to apply the fix. Include the file and symbol names indicated in the issue at the head of your response. crates/wireframe-verification/src/connection_model/model.rs Comment on lines +77 to +78 if state.low_priority_queued
&& (!state.high_priority_queued || state.fairness_allows_low) =>❌ New issue: Complex Conditional |
Owner
Author
|
@coderabbitai Please suggest a fix for this issue and supply a prompt for an AI coding agent to enable it to apply the fix. Include the file and symbol names indicated in the issue at the head of your response. crates/wireframe-verification/src/connection_model/model.rs 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,
}
}❌ New issue: Bumpy Road Ahead |
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as resolved.
Extract per-action transition logic in `PlaceholderConnectionModel` into eleven `apply_*` helpers with early-return guards, plus a `stepped` helper that owns the step counter increment. The `next_state` body becomes a flat dispatch match; `EmitQueued` and `CompleteActiveOutput` use `or_else` chaining to preserve high-priority-first ordering and the response-then-multi-packet completion order. Add three predicate methods on `ConnectionState` (`is_output_idle`, `can_install_output`, `can_emit_low_priority`) to replace inline compound boolean expressions and a duplicated `!shutdown_requested && active_output == Idle` guard, addressing the CodeScene Complex Method (CC=19), Complex Conditional, and Bumpy Road Ahead findings. No behaviour change; `cargo test -p wireframe-verification` and `cargo clippy -p wireframe-verification --all-targets --all-features -- -D warnings` both pass.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Owner
Author
|
@coderabbitai Please suggest a fix for this issue and supply a prompt for an AI coding agent to enable it to apply the fix. Include the file and symbol names indicated in the issue at the head of your response. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. crates/wireframe-verification/src/connection_model/model.rs Comment on lines +64 to +73 fn apply_emit_high(state: &ConnectionState) -> Option<ConnectionState> {
if !state.high_priority_queued {
return None;
}
let mut next = Self::stepped(state);
next.high_priority_queued = false;
next.emitted_high_priority = true;
next.fairness_allows_low = true;
Some(next)
}❌ New issue: Code Duplication |
This comment was marked as resolved.
This comment was marked as resolved.
Introduce a single `apply_if` combinator on
`PlaceholderConnectionModel` that owns the guard check, the
`stepped` clone, and the field-mutation closure. Rewrite all
eleven `apply_*` helpers as one-line delegations through the
combinator, eliminating the duplicated
`if !guard { return None; } let mut next = Self::stepped(state); …
Some(next)` skeleton flagged by CodeScene's Code Duplication
finding (apply_emit_active_frame, apply_emit_high, apply_emit_low,
apply_shutdown).
Two helpers gain flat boolean assignments equivalent to the
prior conditionals, since `shutdown_during_output` is only
written under shutdown semantics that already enforce
monotonicity:
- apply_emit_active_frame:
next.shutdown_during_output = state.shutdown_requested;
- apply_shutdown:
next.shutdown_during_output = !state.is_output_idle();
No behaviour change: `cargo test -p wireframe-verification` and
`cargo clippy -p wireframe-verification --all-targets --all-features
-- -D warnings` both pass.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Owner
Author
|
@coderabbitai Please suggest a fix for the following concern and provide an AI coding agent prompt for the fix: |
This comment was marked as resolved.
This comment was marked as resolved.
Convert `.expect("...")` to `.unwrap()` in test helper functions that
are not themselves annotated `#[test]`. Whitaker's
`no_expect_outside_tests` lint targets `.expect` only and bypasses
standard `#[allow]`/`#[expect]` suppression, so the only working fix
is to replace the call. Sites covered:
- `fairness.rs`: `MockClock::advance` and `MockClock::now`. The
attached `#[expect]` switches from `clippy::expect_used` to
`clippy::unwrap_used`, preserving the existing "fail loudly on
poisoned lock" rationale.
- `fragment/payload.rs`: `assert_fragment_decode_error`.
- `message_assembler/tests.rs`: `parse_header`.
- `message_assembler/budget_tests.rs`: `nz` and the
`create_first_frame_input!` macro body that `submit_first` and
`submit_first_at` expand.
- `message_assembler/state_tests.rs`: `state_with_defaults`.
- `server/runtime/tests.rs`: `setup_backoff_mock_listener` (lock
guard and socket-address parse).
Add `allow-unwrap-in-tests = true` to `clippy.toml` so the new
`.unwrap()` calls satisfy `clippy::unwrap_used` in the `#[test]`
contexts that already enjoy `allow-expect-in-tests`. Helpers not
directly annotated `#[test]` still need the `#[expect]` attribute
on the function (preserved on the two `MockClock` methods).
Verified with `cargo fmt --all -- --check`,
`cargo clippy --all-targets --all-features -- -D warnings`,
`RUSTFLAGS="-D warnings" whitaker --all -- --all-targets --all-features`,
and `RUSTFLAGS="-D warnings" cargo test --all-targets --all-features`.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 09ffd11a7b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+39
to
+40
| .target_max_depth(bounds.max_depth) | ||
| .target_state_count(bounds.max_state_count) |
There was a problem hiding this comment.
VerificationBounds accepts usize, but target_max_depth/target_state_count in Stateright treat 0 as None (unbounded) via NonZeroUsize::new(...). With the current pass-through, a caller that sets either bound to 0 to mean “disable exploration” will instead remove that limit and may trigger unexpectedly large or non-terminating checks in CI. Validate these fields as non-zero (or model them as NonZeroUsize) before passing them into the checker builder.
Useful? React with 👍 / 👎.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 4
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@clippy.toml`:
- Line 8: Remove the global "allow-unwrap-in-tests = true" entry from
clippy.toml and instead apply narrow allowances only to the specific test
helpers that legitimately need unwraps by annotating those helper functions with
#[allow(clippy::unwrap_used)]; also remove or update the stale
#[expect(clippy::unwrap_used)] annotations in src/fairness.rs so they reflect
actual local allowances rather than relying on a blanket test suppression.
Ensure you reference the lint name unwrap_used and the specific helper functions
you change so the change is narrowly scoped.
In `@crates/wireframe-verification/src/connection_model/action.rs`:
- Around line 5-15: Add Rustdoc comments for every public variant of the
ConnectionAction enum so generated docs are self-describing: for each variant
(EnqueueHigh, EnqueueLow, InstallResponse, InstallMultiPacket, EmitQueued,
EmitActiveFrame, CompleteActiveOutput, Shutdown, TickFairness) add a short ///
comment above the variant describing its purpose and when it is emitted/handled;
place the docs directly above each variant in the ConnectionAction enum
declaration and use concise sentences that explain intent and any important
semantics (e.g., priority difference between EnqueueHigh/EnqueueLow, what
InstallResponse/InstallMultiPacket represent, what EmitQueued/EmitActiveFrame
do, meaning of CompleteActiveOutput, Shutdown behavior, and TickFairness role).
In `@crates/wireframe-verification/src/connection_model/properties.rs`:
- Around line 9-12: The invariant Property::always("active output remains
exclusive", active_output_is_exclusive) is vacuous because
active_output_is_exclusive always returns true; remove or replace this
Property::always invocation (and the duplicate at the other occurrence) with a
meaningful check: either delete the Property::always line(s) referring to
active_output_is_exclusive, or implement/plug in a real predicate function
(e.g., active_output_exclusive_predicate) that inspects the model state and
returns false when exclusivity is violated; locate the Property::always calls
and the active_output_is_exclusive function to update or remove them
accordingly.
In `@docs/execplans/15-1-2-wireframe-verification-crate.md`:
- Around line 130-133: Update the Decision sentence that currently reads
"Decision: use `stateright = "0.31.0"` because that is the current published
release..." to use "currently published release" instead of "current published
release" so it reads: "Decision: use `stateright = \"0.31.0\"` because that is
the currently published release..." — modify the string in the Decision block
(the line starting with "Decision: use") to replace the phrase accordingly.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 80a6fdfd-fd35-4023-95d6-a9f97224d2f9
⛔ Files ignored due to path filters (1)
Cargo.lockis excluded by!**/*.lock
📒 Files selected for processing (28)
Cargo.tomlclippy.tomlcrates/wireframe-verification/Cargo.tomlcrates/wireframe-verification/src/connection_model/action.rscrates/wireframe-verification/src/connection_model/mod.rscrates/wireframe-verification/src/connection_model/model.rscrates/wireframe-verification/src/connection_model/properties.rscrates/wireframe-verification/src/connection_model/state.rscrates/wireframe-verification/src/harness.rscrates/wireframe-verification/src/lib.rscrates/wireframe-verification/tests/connection_actor.rscrates/wireframe-verification/tests/verification_harness.rsdocs/developers-guide.mddocs/execplans/15-1-2-wireframe-verification-crate.mddocs/formal-verification-methods-in-wireframe.mddocs/roadmap.mdsrc/fairness.rssrc/fragment/payload.rssrc/message_assembler/budget_tests.rssrc/message_assembler/state_tests.rssrc/message_assembler/tests.rssrc/server/runtime/tests.rstests/common/workspace_manifest_support.rstests/features/workspace_manifest.featuretests/fixtures/workspace_manifest.rstests/scenarios/workspace_manifest_scenarios.rstests/steps/workspace_manifest_steps.rstests/workspace_manifest.rs
Reject zero verification bounds at compile time by modelling
VerificationBounds fields as NonZeroUsize, preventing callers from
inadvertently triggering unbounded Stateright exploration when they
intended to disable a bound.
Remove the blanket allow-unwrap-in-tests from clippy.toml and replace
it with narrowly scoped #[expect(clippy::unwrap_used)] on the six
test helpers that legitimately need .unwrap(). The fairness.rs
helpers already carried local permits so they stay unchanged.
Also:
- Add Rustdoc to every ConnectionAction variant.
- Remove the vacuous Property::always("active output remains exclusive")
whose predicate always returned true.
- Fix wording in the 15.1.2 execplan.
Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Use unwrap_or(NonZeroUsize::MIN) instead of .unwrap() or .expect() to sidestep both clippy::unwrap_used (which #[expect] spuriously reports as unfulfilled on NonZeroUsize::new(const).unwrap()) and Whitaker's no_expect_outside_tests (which fires on .expect() in #[fixture] functions that aren't recognised as tests). Co-authored-by: factory-droid[bot] <138933559+factory-droid[bot]@users.noreply.github.com>
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/v0-2-0-to-v0-3-0-migration-guide.md`:
- Around line 895-897: The sentence "It holds an exclusive borrow of the client
for the duration of the stream, preventing concurrent sends. The terminator
frame is consumed internally and the stream returns `None` once it arrives."
should have a comma added before "and" to separate the two independent clauses;
locate the paragraph describing `Item = Result<Frame, ClientError>` and change
"The terminator frame is consumed internally and the stream returns `None` once
it arrives." to "The terminator frame is consumed internally, and the stream
returns `None` once it arrives." to improve clarity.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 4527ffcb-9e3b-4a81-9569-6bf5ad640816
📒 Files selected for processing (13)
crates/wireframe-verification/src/connection_model/action.rscrates/wireframe-verification/src/connection_model/properties.rscrates/wireframe-verification/src/harness.rscrates/wireframe-verification/tests/verification_harness.rsdocs/execplans/10-1-1-convert-root-manifest-into-hybrid-workspace.mddocs/execplans/15-1-2-wireframe-verification-crate.mddocs/formal-verification-methods-in-wireframe.mddocs/v0-2-0-to-v0-3-0-migration-guide.mdsrc/fragment/payload.rssrc/message_assembler/budget_tests.rssrc/message_assembler/state_tests.rssrc/message_assembler/tests.rssrc/server/runtime/tests.rs
Add the missing comma in the migration guide sentence describing ResponseStream terminator handling so the two independent clauses read cleanly.
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.