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
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.
swaits