swaits/hsmc

0 Fork 0

Files

T

journal + determinism tests + Creusot verification scaffolding

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.

2026-04-27 20:15:05 -06:00

4.4 KiB

Raw Blame History

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

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.

4.4 KiB Raw Blame History Unescape Escape