hsmc/verification/INVARIANTS.md

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	🟡

Path tables (src/paths.rs)

The codegen-emitted tables __PATH_RANGE, __PATH_DATA, __TERMINATE_RANGE, __TERMINATE_DATA, and __DEFAULT_CHILD carry the safety preconditions for every unsafe { ... .get_unchecked(...) } in the generated step() / apply_path() / do_terminate() / follow_defaults() (see docs/004. unsafe-safety-contract.md). The proof strategy is two-pronged:

• A const _: () = { assert!(...) }; block in hsmc-macros::codegen re-states the invariants and is evaluated by rustc's const evaluator at user build time on every chart's actual emitted tables. Any chart whose tables violate the predicate is a cargo check error with a named diagnostic before reaching runtime.
• The Pearlite-annotated functions in paths.rs express the same predicate with an #[ensures(... forall ...)] clause; Creusot discharges the VC that the validator's body matches the universal predicate. tests/correspondence_paths.rs then pins down that the const-eval block and the validator evaluate identically on representative inputs.

Spec rule	Statement	Function	Status
P1.PATH	forall i. let (s,m,e) = __PATH_RANGE[i] in s ≤ m ≤ e ≤ __PATH_DATA.len()	check_path_range_invariant	🟡
P1.TERM	forall i. let (s,e) = __TERMINATE_RANGE[i] in s ≤ e ≤ __TERMINATE_DATA.len()	check_terminate_range_invariant	🟡
P2.PATH_ID	forall i. __PATH_DATA[i] < n_states	check_state_ids_in_bounds	🟡
P2.TERM_ID	forall i. __TERMINATE_DATA[i] < n_states	check_state_ids_in_bounds	🟡
P2.DEFAULT	forall i. match __DEFAULT_CHILD[i] { Some(t) => t < n_states, None => () }	check_default_child_in_bounds	🟡
P.AGGREGATE	All five above hold simultaneously	check_path_tables_sound	🟡

Each function's #[ensures] clause is a forall<i: Int> over the input slice. Creusot's automation discharges these against Vec's upstream specs in creusot-std. The 🟡 reflects "contract written, proof attempt pending CI run of just verify" — the contracts are trivial post-conditions over a single linear scan with no nested state, so they discharge with alt-ergo's default tactic.

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
compute_transition_paths algorithm itself	Universal proof "for any tree input, output satisfies P1 + P2" requires modeling the tree structure in Pearlite. The current strategy proves the predicate is correct and runs it via const-eval on every actual chart at build time — operationally equivalent for end users (every compiled chart is verified) but not the universal quantification that Creusot would give. Phase 5.
step() end-to-end determinism	Composes everything above; do once helpers are green. Phase 5.
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.