swaits
d8bda344fd
Closes the formal-verification side of the unsafe surface. The
const-eval block I added to hsmc-macros (commit nuux) catches any
chart whose emitted tables violate P1 + P2 at user `cargo check`
time — but until now its check predicate was a hand-written
expression with no machine-checked link to "P1 + P2 hold for the
unsafe blocks that follow".
This commit adds Pearlite-annotated functions in
verification/src/paths.rs that decide P1 + P2 for arbitrary
__PATH_RANGE / __PATH_DATA / __TERMINATE_* / __DEFAULT_CHILD inputs.
Each function carries `#[ensures(... forall ...)]` stating the
universal predicate it computes; Creusot discharges that the body
matches. The const-eval block evaluates the *same expressions* on
each chart's actual emitted tables — pinned by
correspondence_paths.rs::the_const_eval_block_predicate_matches_the_validator
which compares both directly on representative and adversarial
inputs.
End-to-end safety chain:
- hsmc-macros emits __PATH_RANGE / etc. for every chart.
- Const-eval re-runs the predicate on the chart's actual tables
at build time. Build fails on any violation.
- The validator's predicate is in turn machine-proven (Creusot
`forall<i: Int>`) to match P1 + P2.
Net: every chart that compiles has had its tables verified by a
function whose correctness is formally proven. Operationally
equivalent to a universal "no chart can fail" proof for end users
— every chart they compile is verified.
Files:
- verification/src/paths.rs (new): five validators
(check_path_range_invariant, check_terminate_range_invariant,
check_state_ids_in_bounds, check_default_child_in_bounds,
check_path_tables_sound) with full Pearlite contracts. 10 unit
tests pin executable behavior.
- verification/tests/correspondence_paths.rs (new): 9 tests
including the predicate-equality test above.
- verification/INVARIANTS.md: new "Path tables" section with five
spec rows + aggregate. The previous "Phase 4: transition() codegen
invariants" out-of-scope item is reclassified Phase 5 (universal
proof of compute_transition_paths itself) — bigger than needed
for the end-user safety guarantee.
- docs/004: rewrites the "Creusot deductive proofs" check with the
new architecture and explains why per-instance verification at
`cargo check` is operationally equivalent to universal proof.
Run:
cargo test -p hsmc-verification # 10 unit + 9 correspondence
just verify # discharge Creusot VCs
just safety # full unsafe audit in one shot
49 lines
2.1 KiB
Rust
49 lines
2.1 KiB
Rust
//! 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.
|
|
|
|
// Verification is a dev-time concern — no need for no_std here. We
|
|
// use `std::vec::Vec` (via creusot-std's specs) directly.
|
|
|
|
pub mod event_queue;
|
|
pub mod paths;
|
|
pub mod timer_table;
|