Trait VerifiedStateMachine 

pub trait VerifiedStateMachine {
    type State: ElicitComplete;
    type Invariant: Prop;

    // Provided methods
    fn transition_harnesses() -> Vec<TokenStream> { ... }
    fn vsm_kani_proof() -> TokenStream { ... }
    fn transition_kani_closure_proofs(_inv_fn: &str) -> Vec<TokenStream> { ... }
    fn transition_creusot_contracts(_inv_fn: &str) -> Vec<TokenStream> { ... }
    fn transition_verus_contracts(_inv_fn: &str) -> Vec<TokenStream> { ... }
    fn transition_verus_stubs() -> Vec<TokenStream> { ... }
    fn vsm_creusot_proof() -> TokenStream { ... }
    fn vsm_verus_proof() -> TokenStream { ... }
    fn vsm_verus_transitions() -> TokenStream { ... }
}

A state machine whose states are fully described and whose transitions preserve a declared invariant.

Contract

A VerifiedStateMachine declares two associated types:

• State — must be ElicitComplete: fully introspectable, serialisable, and reasoned about by elicitation tooling.
• Invariant — a Prop that every valid transition must preserve.

Transitions are FormalMethods with signature (State, Established<Invariant>) -> (State, Established<Invariant>). The type system guarantees that a transition cannot produce a new state without presenting proof that the invariant still holds.

“Gated community” for formal verification

Declaring a VerifiedStateMachine is the top-level compiler-enforced claim that a system preserves its invariants. Outside a VSM any piece of the contracts stack can be used freely; inside, every transition must be a FormalMethod.

Required Associated Types

type State: ElicitComplete

The state type. Must be ElicitComplete.

type Invariant: Prop

The invariant that every transition must preserve.

Provided Methods

fn transition_harnesses() -> Vec<TokenStream>

Return the Kani harness proc_macro2::TokenStream for every transition in this machine.

Override this in each VerifiedStateMachine implementation, listing the companion structs generated by formal_method:

fn transition_harnesses() -> Vec<proc_macro2::TokenStream> {
    vec![
        MyTransitionATransition::kani_harness(),
        MyTransitionBTransition::kani_harness(),
    ]
}

The default implementation returns an empty list (no harnesses).

fn vsm_kani_proof() -> TokenStream

Compose the full VSM Kani proof: the invariant proposition proof followed by all proof_for_contract closure harnesses for each registered transition.

This is the token stream that a build.rs should write to a generated .rs file so that Kani can verify the entire state machine end-to-end.

The composition says: “the invariant is a valid proposition AND every transition preserves it without panicking for any reachable input.”

fn transition_kani_closure_proofs(_inv_fn: &str) -> Vec<TokenStream>

Return one proof_for_contract closure harness per transition in this machine.

Each entry is a #[kani::proof_for_contract(fn_name)] harness using the forgive-and-forget pattern. Contracts on the original function (emitted by #[formal_method] via cfg_attr(kani, kani::requires/ensures)) are verified by DFCC. Once verified, each transition can be replaced with stub_verified(fn_name) in multi-step composition harnesses.

When inv_fn is empty, all entries are empty TokenStreams.

The default implementation returns an empty list.

fn transition_creusot_contracts(_inv_fn: &str) -> Vec<TokenStream>

Return one Creusot companion contract per transition in this machine.

Each entry is a #[cfg(creusot)] function with #[requires]/#[ensures] annotations. When the invariant type’s Prop::creusot_invariant_fn_name returns a non-empty string, the contracts are real (no #[trusted]). Otherwise they fall back to #[trusted] placeholders.

The default implementation returns an empty list.

fn transition_verus_contracts(_inv_fn: &str) -> Vec<TokenStream>

Return one Verus assume_specification block per transition in this machine.

When inv_fn is non-empty, each entry constrains the transition with requires inv_fn(&state) / ensures inv_fn(&r.0). When inv_fn is empty, trivially-true requires true, ensures true stubs are emitted.

The default implementation returns an empty list.

fn transition_verus_stubs() -> Vec<TokenStream>

Return one #[verifier::external] stub function per transition.

Used by vsm_verus_standalone_proof() to generate self-contained Verus source files where no external crate rlibs are available. Each stub declares the function with a todo!() body so that assume_specification has a concrete symbol to axiomatise.

The default implementation returns an empty list.

fn vsm_creusot_proof() -> TokenStream

Compose the full VSM Creusot proof: the invariant proposition proof followed by one contract per registered transition.

When Self::Invariant::creusot_invariant_fn_name() is non-empty, the generated companions use real #[requires]/#[ensures] annotations and Creusot will verify the function bodies. Otherwise trusted placeholders are emitted (same as the stub path).

fn vsm_verus_proof() -> TokenStream

Compose the full VSM Verus proof: the invariant proposition proof followed by one assume_specification block per registered transition.

When Self::Invariant::verus_invariant_fn_name() is non-empty, the generated companions emit real requires/ensures Verus contracts. Otherwise trivially-true stubs are emitted.

fn vsm_verus_transitions() -> TokenStream

Compose the transition portion of a self-contained Verus proof file: all #[verifier::external] stubs followed by all assume_specification contracts.

Used by strictly_verus/build.rs to build files that do not import external crate rlibs (which the Verus toolchain cannot link). The caller is responsible for prepending the inline type definitions and the invariant spec function before this output.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors