Crate quint_connect

Expand description

§Quint Connect

A model-based testing framework for Rust that connects Quint specifications with Rust applications.

§Overview

Quint Connect enables rigorous testing of Rust code against formal specifications written in Quint. By automatically generating traces from your Quint specifications and replaying them against your Rust implementation, you can verify that your code behaves exactly as specified.

§Key Features

Automatic Trace Generation: Generates test cases from Quint specifications
State Validation: Automatically verifies that implementation state matches specification state
Model-Based Testing: Leverage Quint’s powerful specification language for comprehensive testing
Declarative Test Definition: Simple macros for defining model-based tests
Detailed Error Reporting: Clear diffs when implementation diverges from specification

§Requirements

Rust 1.70 or later
Quint installed and available in PATH

§Quick Start

§1. Define Your Specification

Write your system specification in Quint (e.g., spec.qnt).

§2. Implement the Test Driver

Create a test driver that connects your Rust implementation to the test framework:

use quint_connect::*;
use serde::Deserialize;

#[derive(Eq, PartialEq, Deserialize, Debug)]
struct MyState {
    // Fields matching your Quint variables
}

impl State<MyDriver> for MyState {
    fn from_driver(driver: &MyDriver) -> Result<Self> {
        // Convert driver's state to specification state
        todo!()
    }
}

#[derive(Default)]
struct MyDriver {
    // Your implementation state
}

impl Driver for MyDriver {
    type State = MyState;

    fn step(&mut self, step: &Step) -> Result {
        switch!(step {
            init => self.init(),
            MyAction(param1, param2?) => {
                self.my_action(param1, param2);
            }
        })
    }
}

impl MyDriver {
    fn init(&mut self) {
        // Initialize the implementation state
    }
    
    fn my_action(&mut self, param1: String, param: Option<usize>) {
        // Call equivalent code in your implementation
    }
}

§3. Create Tests

Use the provided macros to create model-based tests:

use quint_connect::*;

// Run a single test as specified by a Quint run 
#[quint_test(spec = "spec.qnt", test = "myTest")]
fn my_test() -> impl Driver {
    MyDriver::default()
}

// Run multiple traces in simulation mode
#[quint_run(spec = "spec.qnt")]
fn simulation() -> impl Driver {
    MyDriver::default()
}

§4. Run Test

Run tests with:

cargo test -- --nocapture

Increase verbosity to see step’s actions and nondeterministic choices available:

QUINT_VERBOSE=1 cargo test -- --nocapture

§Tips and Tricks

§Nondeterminism

Quint detects nondeterminism in the specification’s step action. For example:

action step = any {
  action1,
  // ...
}

action action1 = {
  nondet node = NODES.oneOf()
  // ...
}

When collecting traces, Quint keeps track of action names and their set of nondet values as it runs simulations or tests. These become available to Quint Connect automatically. However, if an anonymous action is detected, Quint Connect will fail to run steps:

action step = any {
  action1,
  all {  // <- anonymous action!
    action2,
    action3
  }
}

In those cases, simply rewrite the spec so that all actions in step are properly named:

action step = any {
  action1,
  action2_and_3
}

action action2_and_3 = all {
  action2,
  action3
}

§Enums

Quint sum types are serialized by Quint as records with the tag and value fields representing the type variant and its arguments, respectively. For example:

type SumType = 
  | Variant1
  | Variant2
  
// Serializes as:
// { tag: "Variant1", value: [] }

The previous Quint sum type can be deserialized in Rust with:

use serde::Deserialize;

#[derive(Deserialize)]
#[serde(tag = "tag")]
enum SumType {
  Variant1,
  Variant2
}

Sum types with associated values require specifying serde’s content attribute. For example:

type SumType = 
  | Variant1(int)
  | Variant2(str)

The sum type above must be deserialized as:

use serde::Deserialize;

#[derive(Deserialize)]
#[serde(tag = "tag", content = "value")] // <- note the `content` attribute
enum SumType {
  Variant1(usize),
  Variant2(String)
}

§Optional Fields

Optional types in Quint are defined as a sum type:

type Option[a] = Some(a) | None

The itf crate has utilities to help deserializing optional fields:

use serde::Deserialize;
use itf::de::{self, As};

#[derive(Deserialize)]
struct MyState {
    #[serde(with = "As::<de::Option::<_>>")]
    pub optional_field: Option<String>
}

§Configuration

§Driver Configuration

In some cases the state that you want to check is nested within some global variable. To narrow down the verifiable state, override the Driver config method with the path to the variable that holds the state to check:

use quint_connect::*;

fn config() -> Config {
    Config {
        state: &["global_var", "nested_record", "my_state"],
        ..Config::default()
    }
}

Similarly, in some scenarios the user may choose to track nondeterminism manually other than using Quint’s builtin variables. In those cases, track nondeterminism as a sum type where each variant holds a record containing nondeterministic choices, then specify its path in the driver’s configuration:

use quint_connect::*;

fn config() -> Config {
    Config {
        nondet: &["global_var", "nondet_choices"],
        ..Config::default()
    }
}

These driver configurations are most commonly used when checking traces from specifications using the Choreo library. See the two_phase_commit example in the examples folder for details on how its implementation is checked with Quint connect.

§Verbosity Control

Set the QUINT_VERBOSE environment variable to control output verbosity:

QUINT_VERBOSE=0: Minimal output
QUINT_VERBOSE=1: Show trace and step information
QUINT_VERBOSE=2: Show detailed state and step derivation

§Reproducible Tests

Failed tests display the random seed used:

Reproduce this error with `QUINT_SEED=42`

Set the seed to reproduce exact test traces:

QUINT_SEED=42 cargo test

§Examples

See the connect/examples/ directory for complete examples:

tictactoe: A simple tic-tac-toe game implementation
two_phase_commit: A simplified version of the two-phase commit protocol using Choreo

§License

Licensed under the Apache License, Version 2.0 (the “License”); you may not use this file except in compliance with the License. You may obtain a copy of the License at

http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an “AS IS” BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.

Macros§

switch: Pattern-matches on action names and extracts nondeterministic picks from a Step.

Structs§

Config: Configuration for a Driver that specifies where to find state and nondeterministic picks within a Quint specification.
Step: Represents a single step in a trace generated from a Quint specification.

Traits§

Driver: Core trait for connecting Rust implementations to Quint specifications.
State: Trait for extracting and comparing state between a Quint specification and a Rust implementation.

Type Aliases§

Path: A static path used to navigate nested structures in Quint specifications.
Result: A convenience type alias for anyhow::Result used throughout this crate.

Attribute Macros§

quint_run: Generates a test that runs multiple random traces by simulating a Quint specification.
quint_test: Generates a test that runs traces from a specific Quint test.