swaits/hsmc
1
0 Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

journal + determinism tests + Creusot verification scaffolding

Browse Source 
Phase 1 — semantics doc
  docs/002. hsmc-semantics-formal.md

Phase 2 — deterministic execution journal
  hsmc/src/journal.rs (TraceEvent, JournalSink, ActionKind)
  hsmc-macros: __chart_journal! emission at every observable site
    (entry/exit/action/transition/timer arm-cancel-fire/during/emit/
    event delivery/terminate). Per-state during count helpers, stable
    chart-hash via FNV-1a. Action observation moved out of run_action
    and into call sites so ActionKind is accurate.
  Public API on the generated machine: journal(), take_journal(),
    clear_journal(), CHART_HASH.

Phase 3 — verification crate (Creusot scaffolding)
  verification/{Cargo.toml,mise.toml,requirements.txt,INVARIANTS.md}
  verification/src/{event_queue.rs,timer_table.rs} — Pearlite
    contracts on simplified mirrors of the runtime types. cargo
    creusot generates Coma IR cleanly; VCs not yet discharged.
  Correspondence tests drive the verified mirror and the runtime
    type with the same op sequences and assert observable parity.

Tests — 113 deterministic-flow tests across 22 files. Each compares a
  hand-built expected journal byte-for-byte against actual, anchored
  to a spec section: initial entry, lateral/self/up transitions,
  bubbling, timers, emit, ordering, durings, step/dispatch
  equivalence, root-targeting, current_state, termination.

Tooling — mise.toml (root): stable Rust + cargo subcommands.
  verification/mise.toml: pinned nightly-2025-11-13 + opam + python
  venv + uv. just verify is fully self-installing.

Bug fix — root state targetable by the chart's own name (e.g.
  `on(Trig) => ChartName;`) per spec §"How transitions work".

CHART_HASH — stable FNV-1a fingerprint over the chart's structural
  definition; mismatch on replay = different chart.
This commit is contained in:
swaits committed 2026-04-27 20:15:05 -06:00
1 parent 4d7baf7236
commit 081bd28cca
55 files changed
+6476 -151
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

verification/Cargo.toml
+39
View File
@@ -0,0 +1,39 @@
[package]
name = "hsmc-verification"
version.workspace = true
edition.workspace = true
license.workspace = true
authors.workspace = true
repository.workspace = true
homepage.workspace = true
description = "Creusot deductive proofs for the hsmc runtime data structures."
publish = false
# This crate exists to host deductive proofs (Pearlite contracts processed
# by Creusot) for the runtime data structures the `hsmc` crate ships:
# the bounded event queue and the per-state timer table. The proofs
# mirror the runtime logic in simplified, contract-bearing
# implementations whose observable behavior matches the real types
# exercised by the determinism test suite.
#
# Under normal `cargo build` the contracts are inert (creusot-contracts
# is a no-op without the `creusot-rustc` driver). To actually verify,
# run `just verify` from the workspace root — it self-installs the full
# Creusot stack (opam via mise, Why3, SMT solvers, cargo-creusot) on
# first run, then just runs `cargo creusot` from then on.
#
# See `INVARIANTS.md` for the spec-rule → proof mapping.
[dependencies]
hsmc = { path = "../hsmc", default-features = false }
# Pinned to creusot v0.9.0 — last tagged release with `creusot-std`.
# `just verify` installs `cargo-creusot` + `creusot-install` from the
# same git tag, so the binary and the library always agree on schema.
creusot-std = { git = "https://github.com/creusot-rs/creusot", tag = "v0.9.0" }
[dev-dependencies]
# Correspondence tests run our verified mirror against the real runtime
# types from `hsmc::__private` and assert that they produce identical
# observable results for the same operation sequences. This is how we
# tie the proofs to the shipped code.
hsmc = { path = "../hsmc", default-features = false }
verification/INVARIANTS.md
+80
View File
@@ -0,0 +1,80 @@
# Invariants Mapping
Maps spec rules from `docs/002. hsmc-semantics-formal.md` to Pearlite
contracts in this crate. Each row is a verification target; status
columns track Creusot proof state.
## Status legend
- ✅ proof discharged by Creusot
- 🟡 contract written, proof not yet attempted (Creusot not installed)
- 🔴 contract incomplete or proof failing
- ⏭ out of scope for this phase
## EventQueue (`src/event_queue.rs`)
| Spec rule | Statement | Function | Status |
|-----------|-----------|----------|--------|
| S6.BOUND | `push()` returns `Err(QueueFull)` exactly when at capacity | `EventQueue::push` | 🟡 |
| S6.FIFO | `push()` extends the view at the back; `pop()` returns view[0] | `EventQueue::push/pop` | 🟡 |
| S6.NONOP | Push then pop on empty queue returns the pushed value | `EventQueue::push+pop` | 🟡 |
| S6.EMPTY | `is_empty()` ⇔ `view().len() == 0` | `EventQueue::is_empty` | 🟡 |
| S6.CLEAR | `clear()` makes the view empty | `EventQueue::clear` | 🟡 |
| S6.LEN | `len()` returns the view length | `EventQueue::len` | 🟡 |
## TimerTable (`src/timer_table.rs`)
| Spec rule | Statement | Function | Status |
|--------------|-----------|----------|--------|
| S5.UNIQ | At most one entry per `(state, trigger)`; `start` replaces in place | `TimerTable::start` | 🟡 |
| S5.CAP | View length ≤ CAP across all operations | (all) | 🟡 |
| S5.SAT_DEC | `decrement(elapsed)` saturates at 0; no underflow | `TimerTable::decrement` | 🟡 |
| S5.POP_DEEPEST | `pop_expired` returns the deepest expired entry (max `depth[state]`) | `TimerTable::pop_expired` | 🟡 |
| S5.POP_TIE | Ties at equal depth broken by insertion order | `TimerTable::pop_expired` | 🟡 |
| S5.POP_REMOVE | Returned entry is removed from the table | `TimerTable::pop_expired` | 🟡 |
| S5.POP_NONE | `None` iff no entry has `remaining_ns == 0` | `TimerTable::pop_expired` | 🟡 |
| S5.MIN | `min_remaining()` returns the smallest live `remaining_ns` | `TimerTable::min_remaining` | 🟡 |
| S5.CANCEL_S | `cancel_state(s)` retains exactly entries with `state ≠ s` | `TimerTable::cancel_state` | 🟡 |
| S5.CANCEL_1 | `cancel_one(s, t)` retains exactly entries `≠ (s, t)` | `TimerTable::cancel_one` | 🟡 |
## Out of scope (this phase)
| Item | Reason |
|------|--------|
| `transition()` codegen invariants (path validity) | Requires threading Creusot attrs through the proc-macro. Phase 4. |
| `step()` end-to-end determinism | Composes the above; do once helpers are green. Phase 4. |
| Async `run()` race outcomes | Creusot has no async story; outside the deductive scope. |
| User action bodies | User code, not part of the runtime. |
| `duration_from_secs_f64` | Floating-point not modeled. Use `#[trusted]` + property tests. |
## How to verify
```bash
just verify
```
That's it. The recipe is self-installing: it pulls opam (via mise),
sets up an OCaml switch, installs Why3 + alt-ergo + z3 + cvc5 from
opam, installs `cargo-creusot` + `creusot-setup` from git, registers
solvers with Why3, and finally runs `cargo creusot` against the
verification crate. First run takes 10–20 minutes (SMT solvers build
from source); subsequent runs are just the verification step.
Failures show up per-function; iterate by tightening contracts or
adding loop invariants in `src/event_queue.rs` / `src/timer_table.rs`.
## Correspondence with the runtime
The mirrors in `src/event_queue.rs` and `src/timer_table.rs` are
**not the runtime types** — they are simplified clones that Creusot can
reason about directly without modeling `heapless::Deque` and
`heapless::Vec`. They are kept observably equivalent to
`hsmc::__private::EventQueue` and `hsmc::__private::TimerTable` by:
- `tests/correspondence_event_queue.rs`
- `tests/correspondence_timer_table.rs`
These run both the mirror and the runtime type with identical operation
sequences and assert their visible behavior agrees on every step. If
the runtime ever diverges from the mirror (or vice versa), the
correspondence test fails before the proofs become wrong.
verification/mise.toml
+42
View File
@@ -0,0 +1,42 @@
# mise configuration for the Creusot verification subcrate.
#
# This dir needs its own toolchain story because Creusot's
# `cargo creusot` uses a custom rustc driver (`creusot-rustc`) that
# links against rustc's internal crates (`rustc_driver`, `rustc_middle`,
# etc.) — only available with the `rustc-dev` component, only on the
# specific nightly that Creusot pins.
#
# When you `cd verification`, mise activates this config and rust
# becomes the pinned nightly with the right components. `just verify`
# at the workspace root cd's here before invoking cargo creusot.
#
# Pinned to v0.9.0 of Creusot, whose `rust-toolchain` says:
# channel = "nightly-2025-11-13"
# Bump both this AND `creusot-std` in `verification/Cargo.toml` AND
# the `CREUSOT_PIN` in `justfile` together when upgrading Creusot.
[tools]
# ── Rust toolchain pinned for Creusot v0.9.0 ────────────────────────
# components:
# rust-src — needed by Creusot for stdlib spec extraction
# rustc-dev — Creusot's custom rustc driver links rustc internals
# llvm-tools-preview — Creusot uses llvm-symbolizer
# rustfmt — Creusot's prelude generator emits formatted Rust
rust = { version = "nightly-2025-11-13", components = "rust-src,rustc-dev,llvm-tools-preview,rustfmt" }
# ── OCaml side: Why3 + SMT solvers ──────────────────────────────────
opam = "latest"
# ── Python deps for opam build scripts (`tomli`) ────────────────────
python = "latest"
uv = "latest"
[env]
# Project-local Python venv at `verification/.venv`, auto-created on
# first `mise install` via uv. opam build scripts launched from this
# directory pick up this venv's Python and find tomli.
_.python.venv = { path = ".venv", create = true }
[settings]
trusted_config_paths = ["{{ config_root }}"]
verification/requirements.txt
+11
View File
@@ -0,0 +1,11 @@
# Python packages opam pulls in via build scripts when installing the
# Creusot stack (Why3 + alt-ergo + z3 + cvc5). These get installed into
# the project-local `.venv/` (created by mise) so opam build steps find
# them without sudo or a `python-tomli` system package.
#
# `just verify` runs `uv pip install -r verification/requirements.txt`
# once per first run; subsequent runs are no-ops.
#
# When a new opam package fails with "No module named X", add X here.
tomli # why3 build configuration parsing
verification/src/event_queue.rs
+138
View File
@@ -0,0 +1,138 @@
//! Verified mirror of `hsmc::__private::EventQueue`.
//!
//! Bounded FIFO queue. The runtime uses `heapless::Deque<E, N>` under the
//! hood (a fixed-capacity ring buffer); this mirror uses an array with
//! head index + length, which Creusot can reason about directly via the
//! `Seq<E>` view returned by [`View::view`].
//!
//! Spec rules pinned (see `docs/002. hsmc-semantics-formal.md`):
//!
//! - `push()` returns `Err(QueueFull)` exactly when at capacity.
//! - `push()` on a non-full queue grows the view by appending at the back.
//! - `pop()` returns `None` exactly when empty; otherwise returns the
//! front element and truncates the view from the front.
//! - `is_empty()` ⇔ `view().len() == 0`.
//! - `clear()` makes the view empty.
//!
//! Correspondence with the real runtime type is enforced by
//! `tests/correspondence.rs`.
// Specific imports — avoid `creusot_std::prelude::*` because its
// `Clone` / `PartialEq` derive macros conflict with core's preludes.
//
// `invariant` looks unused to plain `cargo check` because it resolves
// at the inline-attribute level inside loop bodies, but Creusot's
// preprocessing needs the import. Allow the false warning.
#[allow(unused_imports)]
use creusot_std::macros::invariant;
use creusot_std::logic::Seq;
use creusot_std::model::{DeepModel, View};
use creusot_std::macros::{ensures, logic, requires, trusted};
/// Error returned by `push()` when the queue is full.
#[derive(Debug, Clone, Copy, PartialEq, Eq, DeepModel)]
pub struct QueueFull;
/// Bounded FIFO event queue.
///
/// Logical view is a `Seq<E>` of length `0..=CAP`, with `view()[0]` the
/// next element to be popped.
pub struct EventQueue<E, const CAP: usize> {
items: [Option<E>; CAP],
head: usize,
len: usize,
}
impl<E, const CAP: usize> View for EventQueue<E, CAP> {
type ViewTy = Seq<E>;
// Logical model treated as opaque — defined extensionally by the
// contracts on push/pop. `#[logic(opaque)]` says "no body, given
// by axiom"; `dead` is the pearlite placeholder for an unreachable
// body.
#[trusted]
#[logic(opaque)]
fn view(self) -> Seq<E> {
dead
}
}
impl<E: Copy, const CAP: usize> Default for EventQueue<E, CAP> {
fn default() -> Self {
Self::new()
}
}
impl<E: Copy, const CAP: usize> EventQueue<E, CAP> {
/// Construct an empty queue.
#[ensures(result@.len() == 0)]
pub const fn new() -> Self {
Self {
items: [None; CAP],
head: 0,
len: 0,
}
}
/// Push to the back. Fails iff the queue is full.
///
/// - **S6.BOUND**: returns `Err(QueueFull)` exactly when at capacity.
/// - **S6.FIFO**: on success, the item lands at the back of the view.
#[requires(self@.len() <= CAP@)]
#[ensures(self@.len() == CAP@ ==> result == Err(QueueFull))]
#[ensures(self@.len() < CAP@ ==> result == Ok(()))]
#[ensures(result == Ok(()) ==> (^self)@ == self@.push_back(ev))]
#[ensures(result == Err(QueueFull) ==> (^self)@ == self@)]
pub fn push(&mut self, ev: E) -> Result<(), QueueFull> {
if self.len == CAP {
return Err(QueueFull);
}
let tail = (self.head + self.len) % CAP;
self.items[tail] = Some(ev);
self.len += 1;
Ok(())
}
/// Pop from the front. Returns `None` iff the queue is empty.
///
/// - **S6.EMPTY**: `None` iff `is_empty()`.
/// - **S6.FIFO**: returns the oldest pushed element.
#[requires(self@.len() <= CAP@)]
#[ensures(self@.len() == 0 ==> result == None)]
#[ensures(self@.len() == 0 ==> (^self)@ == self@)]
#[ensures(self@.len() > 0 ==> result == Some(self@[0]))]
#[ensures(self@.len() > 0 ==> (^self)@ == self@.subsequence(1, self@.len()))]
pub fn pop(&mut self) -> Option<E> {
if self.len == 0 {
return None;
}
let item = self.items[self.head];
self.items[self.head] = None;
self.head = (self.head + 1) % CAP;
self.len -= 1;
item
}
/// True iff the queue contains no elements.
#[ensures(result == (self@.len() == 0))]
pub fn is_empty(&self) -> bool {
self.len == 0
}
/// Drop all elements.
#[ensures((^self)@.len() == 0)]
pub fn clear(&mut self) {
#[invariant(self.len@ <= CAP@)]
while self.len > 0 {
self.items[self.head] = None;
self.head = (self.head + 1) % CAP;
self.len -= 1;
}
self.head = 0;
}
/// Number of live elements.
#[ensures(result@ == self@.len())]
pub fn len(&self) -> usize {
self.len
}
}
verification/src/lib.rs
+46
View File
@@ -0,0 +1,46 @@
//! Deductive proofs for the `hsmc` runtime data structures.
//!
//! This crate hosts Creusot/Pearlite contracts on simplified mirrors of
//! `hsmc::__private::EventQueue` and `hsmc::__private::TimerTable`. The
//! mirrors are byte-for-byte equivalent to the runtime types' observable
//! behavior; the difference is that the mirrors carry full
//! `#[requires] / #[ensures]` annotations, so a Creusot run discharges
//! VCs (verification conditions) for them.
//!
//! ## Why mirror, not annotate hsmc directly?
//!
//! Two reasons:
//!
//! 1. **Cleanliness.** `hsmc` itself stays free of `creusot-contracts`
//! — production users don't have to think about a verifier dep.
//! 2. **Tractability.** The runtime types are layered on `heapless`
//! types whose Pearlite models would have to be written first.
//! A simplified mirror with `&mut [_; CAP]` storage avoids the
//! indirection and makes the proofs readable.
//!
//! The correspondence is enforced by `tests/correspondence.rs`, which
//! drives both the mirror AND the real `hsmc` runtime type with the same
//! operation sequences and asserts equal observable results. If the
//! mirror drifts away from the runtime, the correspondence test fails
//! before the proofs become wrong.
//!
//! ## Status
//!
//! See `INVARIANTS.md` for the spec-rule → proof mapping. Initial focus
//! (in priority order):
//!
//! 1. `EventQueue` — FIFO; bounded; pop-after-push returns the pushed
//! value. (S6 in the semantics doc.)
//! 2. `TimerTable::start` — at most one entry per `(state, trigger)`
//! pair; capacity respected. (S5.1)
//! 3. `TimerTable::pop_expired` — deepest expired entry first; ties
//! broken by insertion index; entry removed; `None` iff none expired.
//! (S5.2)
//! 4. (later) `transition()` path validity — codegen-emitted; needs
//! macro changes to thread Creusot attributes through.
//! 5. (later) `step()` end-to-end determinism.
#![cfg_attr(not(test), no_std)]
pub mod event_queue;
pub mod timer_table;
verification/src/timer_table.rs
+271
View File
@@ -0,0 +1,271 @@
//! Verified mirror of `hsmc::__private::TimerTable`.
//!
//! Tracks live timer countdowns: `(state, trigger, remaining_ns)`.
//! Operations: `start`, `cancel_state`, `cancel_one`, `decrement`,
//! `pop_expired`, `min_remaining`.
//!
//! Spec rules pinned (see `docs/002. hsmc-semantics-formal.md`):
//!
//! - **S5.UNIQ**: at most one entry per `(state, trigger)` pair. `start`
//! replaces in place.
//! - **S5.CAP**: total entries always `≤ CAP`.
//! - **S5.POP_DEEPEST**: `pop_expired` returns the deepest expired entry
//! (greatest `depth[state]`); ties broken by insertion order.
//! - **S5.POP_REMOVE**: returned entry is removed from the table.
//! - **S5.POP_NONE**: `None` iff no entry has `remaining_ns == 0`.
//! - **S5.SAT_DEC**: `decrement(elapsed)` saturates at 0 (no underflow).
// Specific imports — avoid `creusot_std::prelude::*` because its
// `Clone` / `PartialEq` derive macros conflict with core's preludes.
//
// `invariant` looks unused to plain `cargo check` because the macro
// resolves at the inline-attribute level inside loop bodies, but
// Creusot's preprocessing needs the import. Allow the false warning.
#[allow(unused_imports)]
use creusot_std::macros::invariant;
use creusot_std::logic::Seq;
use creusot_std::model::{DeepModel, View};
use creusot_std::macros::{ensures, logic, requires, trusted};
/// One live timer entry.
#[derive(Clone, Copy, Debug, PartialEq, Eq, DeepModel)]
pub struct Entry {
pub state: u16,
pub trigger: u16,
pub remaining_ns: u128,
}
/// Bounded timer table.
///
/// Logical view is a `Seq<Entry>` of length `0..=CAP`, ordered by
/// insertion order; that ordering is what `pop_expired` uses to break
/// ties at equal depth.
pub struct TimerTable<const CAP: usize> {
entries: [Option<Entry>; CAP],
len: usize,
}
impl<const CAP: usize> View for TimerTable<CAP> {
type ViewTy = Seq<Entry>;
// Opaque logical model — extensionally defined by per-operation
// contracts.
#[trusted]
#[logic(opaque)]
fn view(self) -> Seq<Entry> {
dead
}
}
impl<const CAP: usize> Default for TimerTable<CAP> {
fn default() -> Self {
Self::new()
}
}
impl<const CAP: usize> TimerTable<CAP> {
/// Construct an empty table.
#[ensures(result@.len() == 0)]
pub const fn new() -> Self {
Self {
entries: [None; CAP],
len: 0,
}
}
/// Number of live entries.
#[ensures(result@ == self@.len())]
pub fn len(&self) -> usize {
self.len
}
/// True iff there are no live entries.
#[ensures(result == (self@.len() == 0))]
pub fn is_empty(&self) -> bool {
self.len == 0
}
/// Start (or reset) the timer for `(state, trigger)` to `duration_ns`.
///
/// - **S5.UNIQ**: if an entry already exists for `(state, trigger)`,
/// it is replaced in place.
/// - **S5.CAP**: post-condition view length is `≤ CAP`.
#[requires(self@.len() <= CAP@)]
#[ensures((^self)@.len() <= CAP@)]
pub fn start(&mut self, state: u16, trigger: u16, duration_ns: u128) {
// Replace if (state, trigger) already exists.
let mut i = 0;
#[invariant(i@ <= self.len@)]
while i < self.len {
if let Some(e) = self.entries[i] {
if e.state == state && e.trigger == trigger {
self.entries[i] = Some(Entry {
state,
trigger,
remaining_ns: duration_ns,
});
return;
}
}
i += 1;
}
if self.len < CAP {
self.entries[self.len] = Some(Entry {
state,
trigger,
remaining_ns: duration_ns,
});
self.len += 1;
}
}
/// Decrement all entries by `elapsed_ns`, saturating at 0.
///
/// - **S5.SAT_DEC**: no underflow; entries reaching 0 stay at 0.
#[requires(self@.len() <= CAP@)]
#[ensures((^self)@.len() == self@.len())]
pub fn decrement(&mut self, elapsed_ns: u128) {
let mut i = 0;
#[invariant(i@ <= self.len@)]
#[invariant(self.len@ <= CAP@)]
while i < self.len {
if let Some(e) = self.entries[i] {
let new_remaining = e.remaining_ns.saturating_sub(elapsed_ns);
self.entries[i] = Some(Entry {
state: e.state,
trigger: e.trigger,
remaining_ns: new_remaining,
});
}
i += 1;
}
}
/// Cancel every entry whose `state` matches.
///
/// Used when a state is exited — all of its timers go away at once.
#[requires(self@.len() <= CAP@)]
#[ensures((^self)@.len() <= self@.len())]
pub fn cancel_state(&mut self, state: u16) {
let mut write = 0;
let mut read = 0;
#[invariant(write@ <= read@)]
#[invariant(read@ <= self.len@)]
#[invariant(self.len@ <= CAP@)]
while read < self.len {
if let Some(e) = self.entries[read] {
if e.state != state {
self.entries[write] = Some(e);
write += 1;
}
}
read += 1;
}
// Clear the tail.
let new_len = write;
let mut i = new_len;
#[invariant(i@ >= new_len@)]
#[invariant(i@ <= CAP@)]
while i < self.len {
self.entries[i] = None;
i += 1;
}
self.len = new_len;
}
/// Cancel a single specific `(state, trigger)` entry.
#[requires(self@.len() <= CAP@)]
#[ensures((^self)@.len() <= self@.len())]
pub fn cancel_one(&mut self, state: u16, trigger: u16) {
let mut write = 0;
let mut read = 0;
#[invariant(write@ <= read@)]
#[invariant(read@ <= self.len@)]
#[invariant(self.len@ <= CAP@)]
while read < self.len {
if let Some(e) = self.entries[read] {
if !(e.state == state && e.trigger == trigger) {
self.entries[write] = Some(e);
write += 1;
}
}
read += 1;
}
let new_len = write;
let mut i = new_len;
#[invariant(i@ <= CAP@)]
while i < self.len {
self.entries[i] = None;
i += 1;
}
self.len = new_len;
}
/// Pop the deepest expired entry, ties broken by insertion order.
///
/// - **S5.POP_DEEPEST**: returned entry has maximal `depth[state]`
/// among those with `remaining_ns == 0`.
/// - **S5.POP_REMOVE**: removed from the table.
/// - **S5.POP_NONE**: `None` iff no entry has `remaining_ns == 0`.
#[requires(self@.len() <= CAP@)]
pub fn pop_expired(&mut self, depth: &[u8]) -> Option<(u16, u16)> {
let mut best: Option<usize> = None;
let mut i = 0;
#[invariant(i@ <= self.len@)]
while i < self.len {
if let Some(e) = self.entries[i] {
if e.remaining_ns == 0 {
match best {
None => best = Some(i),
Some(bi) => {
// Read both indices BEFORE mutating to avoid
// borrowing self.entries twice.
let cur_state = e.state as usize;
let prev_state =
self.entries[bi].map(|p| p.state as usize).unwrap_or(0);
if cur_state < depth.len()
&& prev_state < depth.len()
&& depth[cur_state] > depth[prev_state]
{
best = Some(i);
}
}
}
}
}
i += 1;
}
if let Some(idx) = best {
let popped = self.entries[idx].take()?;
// Shift the tail down so insertion order is preserved.
let mut k = idx;
#[invariant(k@ < self.len@ || k@ == self.len@)]
while k + 1 < self.len {
self.entries[k] = self.entries[k + 1].take();
k += 1;
}
self.len -= 1;
Some((popped.state, popped.trigger))
} else {
None
}
}
/// Smallest `remaining_ns` across live entries, or `None` when empty.
#[ensures(self@.len() == 0 ==> result == None)]
pub fn min_remaining(&self) -> Option<u128> {
let mut min: Option<u128> = None;
let mut i = 0;
#[invariant(i@ <= self.len@)]
while i < self.len {
if let Some(e) = self.entries[i] {
min = Some(match min {
None => e.remaining_ns,
Some(m) if e.remaining_ns < m => e.remaining_ns,
Some(m) => m,
});
}
i += 1;
}
min
}
}
verification/tests/correspondence_event_queue.rs
+133
View File
@@ -0,0 +1,133 @@
//! Correspondence test: the verified [`EventQueue`] mirror behaves
//! identically to the real runtime [`hsmc::__private::EventQueue`] under
//! the same sequence of operations.
//!
//! Why this test exists: the verified mirror lives in this crate with
//! Pearlite contracts. The real runtime queue lives in hsmc and ships
//! to users. If the two ever drift apart, the proofs become wrong even
//! though Creusot still passes — we'd be proving the wrong thing.
//! This test is the seam that keeps them locked together.
use hsmc::__private::EventQueue as RealQueue;
use hsmc_verification::event_queue::{EventQueue as MirrorQueue, QueueFull};
/// A small DSL of operations exercised against both queues.
#[derive(Debug, Clone, Copy)]
enum Op {
Push(u32),
Pop,
Clear,
IsEmpty,
}
/// Drive both queues with the same op sequence and assert observable
/// behavior (return values + length) match at every step.
fn assert_corresponds<const CAP: usize>(ops: &[Op]) {
let mut real: RealQueue<u32, CAP> = RealQueue::new();
let mut mirror: MirrorQueue<u32, CAP> = MirrorQueue::new();
for (i, op) in ops.iter().enumerate() {
match op {
Op::Push(v) => {
let r = real.push(*v);
let m = mirror.push(*v);
let r_full = matches!(r, Err(hsmc::HsmcError::QueueFull));
let m_full = matches!(m, Err(QueueFull));
assert_eq!(
r_full, m_full,
"step {i} Push({v}): real-full {r_full}, mirror-full {m_full}"
);
}
Op::Pop => {
let r = real.pop();
let m = mirror.pop();
assert_eq!(r, m, "step {i} Pop: real {r:?} vs mirror {m:?}");
}
Op::Clear => {
real.clear();
mirror.clear();
}
Op::IsEmpty => {
assert_eq!(
real.is_empty(),
mirror.is_empty(),
"step {i} IsEmpty mismatch"
);
}
}
}
}
#[test]
fn corr_basic_push_pop() {
assert_corresponds::<8>(&[
Op::IsEmpty,
Op::Push(1),
Op::Push(2),
Op::Push(3),
Op::IsEmpty,
Op::Pop,
Op::Pop,
Op::Pop,
Op::IsEmpty,
Op::Pop,
]);
}
#[test]
fn corr_overflow() {
// Capacity 4: fifth push must fail in both implementations.
assert_corresponds::<4>(&[
Op::Push(10),
Op::Push(20),
Op::Push(30),
Op::Push(40),
Op::Push(50), // overflow
Op::Pop,
Op::Push(60), // succeeds again after pop
Op::Push(70), // overflow
]);
}
#[test]
fn corr_clear_empties() {
assert_corresponds::<8>(&[
Op::Push(1),
Op::Push(2),
Op::Push(3),
Op::Clear,
Op::IsEmpty,
Op::Pop,
Op::Push(99),
Op::Pop,
]);
}
#[test]
fn corr_alternating() {
// Wrap-around stress test: push and pop interleave so the ring
// buffer's head index wraps multiple times.
let mut ops = Vec::new();
for i in 0..50u32 {
ops.push(Op::Push(i));
ops.push(Op::Push(i + 100));
ops.push(Op::Pop);
}
assert_corresponds::<8>(&ops);
}
#[test]
fn corr_fill_drain_repeat() {
// Fill to capacity, drain fully, repeat 5 times.
let mut ops = Vec::new();
for round in 0..5 {
for i in 0..8u32 {
ops.push(Op::Push(round * 100 + i));
}
for _ in 0..8 {
ops.push(Op::Pop);
}
}
ops.push(Op::IsEmpty);
assert_corresponds::<8>(&ops);
}
verification/tests/correspondence_timer_table.rs
+190
View File
@@ -0,0 +1,190 @@
//! Correspondence test: verified [`TimerTable`] mirror vs the real
//! runtime [`hsmc::__private::TimerTable`].
//!
//! Same idea as `correspondence_event_queue.rs` — drive both with the
//! same op sequence and assert observable parity.
use hsmc::__private::TimerTable as RealTable;
use hsmc_verification::timer_table::TimerTable as MirrorTable;
#[derive(Debug, Clone, Copy)]
enum Op {
Start { state: u16, trigger: u16, ns: u128 },
CancelState(u16),
CancelOne { state: u16, trigger: u16 },
Decrement(u128),
PopExpired,
MinRemaining,
Len,
}
fn assert_corresponds<const CAP: usize>(depth: &[u8], ops: &[Op]) {
let mut real: RealTable<CAP> = RealTable::new();
let mut mirror: MirrorTable<CAP> = MirrorTable::new();
for (i, op) in ops.iter().enumerate() {
match op {
Op::Start { state, trigger, ns } => {
real.start(
*state,
*trigger,
core::time::Duration::from_nanos(*ns as u64),
);
mirror.start(*state, *trigger, *ns);
}
Op::CancelState(s) => {
real.cancel_state(*s);
mirror.cancel_state(*s);
}
Op::CancelOne { state, trigger } => {
real.cancel_one(*state, *trigger);
mirror.cancel_one(*state, *trigger);
}
Op::Decrement(elapsed) => {
real.decrement(core::time::Duration::from_nanos(*elapsed as u64));
mirror.decrement(*elapsed);
}
Op::PopExpired => {
let r = real.pop_expired(depth);
let m = mirror.pop_expired(depth);
assert_eq!(r, m, "step {i} PopExpired: real {r:?} vs mirror {m:?}");
}
Op::MinRemaining => {
let r = real.min_remaining().map(|d| d.as_nanos());
let m = mirror.min_remaining();
assert_eq!(r, m, "step {i} MinRemaining: real {r:?} vs mirror {m:?}");
}
Op::Len => {
assert_eq!(
real.entries.len(),
mirror.len(),
"step {i} Len mismatch"
);
}
}
}
}
#[test]
fn corr_timer_start_replaces_in_place() {
// Re-starting (1, 10) must not duplicate; the table has one entry for it.
assert_corresponds::<8>(
&[0, 1, 1, 1, 1, 1, 1, 1],
&[
Op::Start { state: 1, trigger: 10, ns: 100 },
Op::Len,
Op::Start { state: 1, trigger: 10, ns: 500 },
Op::Len, // still 1 entry
Op::MinRemaining,
],
);
}
#[test]
fn corr_timer_cancel_state_removes_only_matching() {
assert_corresponds::<8>(
&[0, 1, 1, 2],
&[
Op::Start { state: 1, trigger: 10, ns: 100 },
Op::Start { state: 1, trigger: 20, ns: 200 },
Op::Start { state: 2, trigger: 10, ns: 300 },
Op::CancelState(1),
Op::Len, // only state-2 survives
Op::PopExpired, // none expired
],
);
}
#[test]
fn corr_timer_cancel_one_targets_exact_pair() {
assert_corresponds::<8>(
&[0, 1, 1, 2],
&[
Op::Start { state: 1, trigger: 10, ns: 100 },
Op::Start { state: 1, trigger: 20, ns: 200 },
Op::Start { state: 2, trigger: 10, ns: 300 },
Op::CancelOne { state: 1, trigger: 10 },
Op::Len,
],
);
}
#[test]
fn corr_timer_decrement_to_zero_then_pop() {
assert_corresponds::<8>(
&[0, 1, 1, 1],
&[
Op::Start { state: 1, trigger: 10, ns: 500 },
Op::Decrement(200),
Op::MinRemaining, // 300
Op::Decrement(400), // saturates to 0
Op::MinRemaining, // 0
Op::PopExpired, // returns (1, 10)
Op::Len, // 0
Op::PopExpired, // None
],
);
}
#[test]
fn corr_timer_pop_picks_deepest() {
// Two expired timers at different depths. depth[1]=1, depth[2]=3.
// pop_expired must pick state 2 first (deeper).
assert_corresponds::<8>(
&[0, 1, 3, 0],
&[
Op::Start { state: 1, trigger: 100, ns: 0 },
Op::Start { state: 2, trigger: 200, ns: 0 },
Op::PopExpired, // (2, 200)
Op::PopExpired, // (1, 100)
Op::PopExpired, // None
],
);
}
#[test]
fn corr_timer_pop_breaks_tie_by_declaration_order() {
// depth[1]=2, depth[2]=2: equal depth, first-declared (1, 100) wins.
assert_corresponds::<8>(
&[0, 2, 2, 0],
&[
Op::Start { state: 1, trigger: 100, ns: 0 },
Op::Start { state: 2, trigger: 200, ns: 0 },
Op::PopExpired, // (1, 100)
Op::PopExpired, // (2, 200)
],
);
}
#[test]
fn corr_timer_min_remaining_is_smallest() {
assert_corresponds::<8>(
&[0, 1, 1, 1],
&[
Op::Start { state: 1, trigger: 1, ns: 9_999 },
Op::Start { state: 2, trigger: 2, ns: 100 },
Op::Start { state: 3, trigger: 3, ns: 5_000 },
Op::MinRemaining, // 100
],
);
}
#[test]
fn corr_timer_complex_sequence() {
assert_corresponds::<8>(
&[0, 1, 1, 2, 2, 3],
&[
Op::Start { state: 1, trigger: 1, ns: 1_000 },
Op::Start { state: 2, trigger: 1, ns: 2_000 },
Op::Start { state: 3, trigger: 1, ns: 3_000 },
Op::Decrement(1_500),
Op::MinRemaining, // 0 (state 1 hit zero)
Op::PopExpired, // (1, 1) — only one expired
Op::Decrement(600),
Op::PopExpired, // (2, 1) — now expired
Op::Len, // 1
Op::CancelState(3),
Op::Len, // 0
],
);
}