swaits
081bd28cca
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.
43 lines
1.9 KiB
TOML
43 lines
1.9 KiB
TOML
# 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 }}"]
|