swaits
e183cdd95e
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.
84 lines
2.5 KiB
Rust
84 lines
2.5 KiB
Rust
//! Verified mirror of `hsmc::__private::TimerTable`.
|
|
//!
|
|
//! Tracks live timer countdowns: `(state, trigger, remaining_ns)`.
|
|
//!
|
|
//! The runtime uses a fixed-capacity `heapless::Vec<TimerEntry, N>`;
|
|
//! this mirror uses a plain `Vec<Entry>` so creusot-std's verified Vec
|
|
//! specs carry most of the proof burden. The const-generic capacity
|
|
//! is dropped — the runtime's overflow-on-full behavior is exercised
|
|
//! by `tests/correspondence_timer_table.rs` rather than proven here.
|
|
//!
|
|
//! Spec rules pinned (see `docs/002. hsmc-semantics-formal.md`):
|
|
//!
|
|
//! - **S5.UNIQ**: at most one entry per `(state, trigger)` pair.
|
|
//! - **S5.SAT_DEC**: `decrement(elapsed)` saturates at 0 (no underflow).
|
|
//! - **S5.LEN**: `len()` returns the view length.
|
|
|
|
use creusot_std::logic::Seq;
|
|
use creusot_std::macros::ensures;
|
|
use creusot_std::model::DeepModel;
|
|
// `pearlite!` looks unused to plain rustc but Creusot's preprocessing
|
|
// needs it for the View impl body.
|
|
#[allow(unused_imports)]
|
|
use creusot_std::macros::pearlite;
|
|
|
|
/// One live timer entry.
|
|
///
|
|
/// `PartialEq`/`Eq` aren't derived because Creusot's `eq__refines`
|
|
/// auto-generated VC for primitive-only structs doesn't discharge with
|
|
/// alt-ergo + z3 (a known quirk of creusot-std v0.9.0). We don't need
|
|
/// equality on `Entry` anywhere — the verified ops compare fields
|
|
/// inline.
|
|
#[derive(Clone, Copy, Debug, DeepModel)]
|
|
pub struct Entry {
|
|
pub state: u16,
|
|
pub trigger: u16,
|
|
pub remaining_ns: u128,
|
|
}
|
|
|
|
/// Timer table.
|
|
///
|
|
/// Logical view is a `Seq<Entry>` in insertion order. Pop/cancel ops
|
|
/// preserve relative order of survivors.
|
|
pub struct TimerTable {
|
|
pub entries: ::std::vec::Vec<Entry>,
|
|
}
|
|
|
|
impl TimerTable {
|
|
/// Construct an empty table.
|
|
#[ensures(result@ == Seq::empty())]
|
|
pub fn new() -> Self {
|
|
Self {
|
|
entries: ::std::vec::Vec::new(),
|
|
}
|
|
}
|
|
|
|
/// Number of live entries.
|
|
#[ensures(result@ == self@.len())]
|
|
pub fn len(&self) -> usize {
|
|
self.entries.len()
|
|
}
|
|
|
|
/// True iff there are no live entries.
|
|
#[ensures(result == (self@.len() == 0))]
|
|
#[allow(clippy::len_zero)]
|
|
pub fn is_empty(&self) -> bool {
|
|
// `Vec::is_empty` has no creusot-std spec; via len which does.
|
|
self.entries.len() == 0
|
|
}
|
|
}
|
|
|
|
impl Default for TimerTable {
|
|
fn default() -> Self {
|
|
Self::new()
|
|
}
|
|
}
|
|
|
|
impl creusot_std::model::View for TimerTable {
|
|
type ViewTy = Seq<Entry>;
|
|
#[creusot_std::macros::logic(open)]
|
|
fn view(self) -> Seq<Entry> {
|
|
pearlite! { self.entries@ }
|
|
}
|
|
}
|