Make `just verify` actually invoke Why3 + alt-ergo + z3 against every
Pearlite VC, and fix the mutant + miri pipelines along the way.
Verification crate
- Drop the const-generic CAP types for EventQueue / TimerTable.
Mirror with std::vec::Vec, whose creusot-std specs carry the
proof burden. Capacity behavior is exercised by the runtime's
own unit tests + correspondence tests.
- View impls are #[logic(open)] over a pub field so contracts on
push/pop/etc. can see the link to the inner Vec's @ view.
- 14/14 VCs discharge: EventQueue {new, push, pop, is_empty, len,
clear, Default}; TimerTable {new, len, is_empty, Default};
Entry derives.
- `cargo creusot prove --no-cache` always runs the SMT solvers;
`time` shows ~7s CPU on ~1.2s wall-clock = real parallel work.
Tooling
- verification/mise.toml pins nightly-2025-11-13 + rust-src,
rustc-dev, llvm-tools-preview, rustfmt; declares opam, python,
uv, and the project-local .venv. Inherits root mise.toml's just
+ cargo-* tools.
- just verify clones creusot v0.9.0 to ~/.local/share/hsmc-verify/
and runs the canonical ./INSTALL — that's the only way the
bundled prelude-generator + creusot-rustc actually build.
- just verify --no-cache forces SMT re-runs every time.
- Drop bespoke pin/install of cargo-creusot from mise.toml; the
cargo backend goes through cargo-binstall which can't pin a
multi-bin git workspace at a tag.
Mutants — was missing every JournalSink mutant
- Recipe runs with --features tokio,journal so journal_* and det_*
tests (gated on both) actually execute.
- Add clear_journal_empties_the_journal test in journal_smoke.rs
to kill the JournalSink::clear with-() mutant.
- Remove dead JournalSink::len + is_empty (called nowhere; only
existed as mutation-bait).
Result: 0 missed, 42 caught, 211 unviable (proc-macro emitted
code that mutants can't standalone-compile).
Miri — was hitting the trybuild glob isolation issue
- --exclude hsmc-macros (trybuild ui test isn't UB-relevant)
- --exclude hsmc-verification (different pinned toolchain)
- 66 tests pass under Miri, 0 UB.
Gitignore
- /verif/, /why3find.json, /.why3find/, **/.venv/ — all
regenerated by `just verify`. Repo stays clean of per-machine
prover timings + venv artifacts.
Misc
- Fix root-state targetability: `on(Trig) => <ChartName>;` resolves
to root id 0 in both ir.rs::resolve_transitions and
validate.rs's separate name_map.
- `set shell` and `set script-interpreter` route every justfile
recipe through `mise exec`, so all subshells see the right
Rust + opam + cargo-* tools regardless of how `just` was
invoked. No shebangs anywhere.
148 lines
4.5 KiB
Rust
148 lines
4.5 KiB
Rust
#![allow(dead_code)]
|
|
//! Deterministic-flow tests for `step()` vs `dispatch()` equivalence.
|
|
//!
|
|
//! Spec section "step() vs run() vs dispatch()":
|
|
//! For the same external event sequence and the same elapsed-time inputs,
|
|
//! the three produce the same observable trace.
|
|
|
|
#![cfg(all(feature = "tokio", feature = "journal"))]
|
|
#![allow(unexpected_cfgs)]
|
|
|
|
use hsmc::{statechart, TraceEvent};
|
|
|
|
#[derive(Default)]
|
|
pub struct Ctx;
|
|
|
|
#[derive(Debug, Clone)]
|
|
pub enum Ev {
|
|
Tick,
|
|
Halt,
|
|
}
|
|
|
|
statechart! {
|
|
Eq {
|
|
context: Ctx;
|
|
events: Ev;
|
|
default(A);
|
|
terminate(Halt);
|
|
|
|
state A {
|
|
entry: a_in;
|
|
exit: a_out;
|
|
on(Tick) => B;
|
|
}
|
|
state B {
|
|
entry: b_in;
|
|
exit: b_out;
|
|
on(Tick) => A;
|
|
}
|
|
}
|
|
}
|
|
|
|
impl EqActions for EqActionContext<'_> {
|
|
async fn a_in(&mut self) {}
|
|
async fn a_out(&mut self) {}
|
|
async fn b_in(&mut self) {}
|
|
async fn b_out(&mut self) {}
|
|
}
|
|
|
|
#[tokio::test(flavor = "current_thread")]
|
|
async fn det_dispatch_drains_to_quiescence() {
|
|
// dispatch(ev) processes ev plus any events emitted while handling ev.
|
|
// After the await returns, the queue is empty.
|
|
tokio::task::LocalSet::new()
|
|
.run_until(async {
|
|
let mut m = Eq::new(Ctx);
|
|
let _ = m.dispatch(Ev::Tick).await;
|
|
assert!(!m.has_pending_events());
|
|
})
|
|
.await;
|
|
}
|
|
|
|
#[tokio::test(flavor = "current_thread")]
|
|
async fn det_step_and_dispatch_produce_same_journal() {
|
|
// Drive one machine via dispatch, another via send + step until queue empty.
|
|
// The journals must match.
|
|
tokio::task::LocalSet::new()
|
|
.run_until(async {
|
|
// Path 1: dispatch.
|
|
let mut m1 = Eq::new(Ctx);
|
|
let _ = m1.dispatch(Ev::Tick).await;
|
|
let _ = m1.dispatch(Ev::Tick).await;
|
|
let _ = m1.dispatch(Ev::Halt).await;
|
|
let j_dispatch = m1.take_journal();
|
|
|
|
// Path 2: send + step.
|
|
let mut m2 = Eq::new(Ctx);
|
|
m2.send(Ev::Tick).unwrap();
|
|
m2.send(Ev::Tick).unwrap();
|
|
m2.send(Ev::Halt).unwrap();
|
|
// Drive to quiescence with explicit steps.
|
|
for _ in 0..20 {
|
|
let _ = m2.step(::hsmc::Duration::ZERO).await;
|
|
if m2.is_terminated() {
|
|
break;
|
|
}
|
|
}
|
|
let j_step = m2.take_journal();
|
|
|
|
assert_eq!(
|
|
j_dispatch, j_step,
|
|
"step and dispatch must produce identical journals for the same event sequence"
|
|
);
|
|
})
|
|
.await;
|
|
}
|
|
|
|
#[tokio::test(flavor = "current_thread")]
|
|
async fn det_step_is_at_most_one_unit_of_work() {
|
|
// Each step() processes at most one event or one timer.
|
|
tokio::task::LocalSet::new()
|
|
.run_until(async {
|
|
let mut m = Eq::new(Ctx);
|
|
m.send(Ev::Tick).unwrap();
|
|
m.send(Ev::Tick).unwrap();
|
|
m.send(Ev::Halt).unwrap();
|
|
|
|
// After the first step (initial enter): chart enters root → A.
|
|
let _ = m.step(::hsmc::Duration::ZERO).await;
|
|
// After the second step: process Tick #1 (A → B).
|
|
let len_after_2 = {
|
|
let _ = m.step(::hsmc::Duration::ZERO).await;
|
|
m.journal().len()
|
|
};
|
|
// After the third step: process Tick #2 (B → A).
|
|
let _ = m.step(::hsmc::Duration::ZERO).await;
|
|
let len_after_3 = m.journal().len();
|
|
|
|
assert!(
|
|
len_after_3 > len_after_2,
|
|
"step processes additional events"
|
|
);
|
|
})
|
|
.await;
|
|
}
|
|
|
|
#[tokio::test(flavor = "current_thread")]
|
|
async fn det_step_repeated_idempotent_when_queue_empty() {
|
|
// Once initial-enter is done and queue is empty, additional steps
|
|
// (with elapsed=ZERO) are no-ops.
|
|
tokio::task::LocalSet::new()
|
|
.run_until(async {
|
|
let mut m = Eq::new(Ctx);
|
|
let _ = m.step(::hsmc::Duration::ZERO).await; // initial entry
|
|
let len_after_first = m.journal().len();
|
|
for _ in 0..10 {
|
|
let _ = m.step(::hsmc::Duration::ZERO).await;
|
|
}
|
|
// After the first step, no events are pending, so additional
|
|
// step(ZERO) calls do nothing.
|
|
assert_eq!(
|
|
m.journal().len(),
|
|
len_after_first,
|
|
"step(ZERO) on empty queue must not change journal"
|
|
);
|
|
})
|
|
.await;
|
|
}
|