Skip to content

Commit 6050ed4

Browse files
Add formal state-transition verification
1 parent f062558 commit 6050ed4

33 files changed

Lines changed: 5791 additions & 552 deletions

.github/workflows/formal.yaml

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
name: formal
2+
on:
3+
pull_request:
4+
workflow_dispatch:
5+
concurrency:
6+
group: ${{ github.workflow }}-${{ github.ref }}-formal
7+
cancel-in-progress: true
8+
permissions:
9+
contents: read
10+
actions: write
11+
id-token: write
12+
jobs:
13+
verify:
14+
runs-on: ubuntu-slim
15+
steps:
16+
- uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
17+
- uses: ./.github/actions/setup-nix
18+
- run: nix build .#checks.x86_64-linux.formal --print-build-logs

.github/workflows/rust-macos.yaml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,10 @@ jobs:
3333
xcrun --find metal
3434
- uses: ./.github/actions/setup-nix
3535
- uses: ./.github/actions/setup-rust-cache
36+
- run: swift test --package-path native/WispAudioKit
3637
# Builds the WispAudioKit Swift static library through build.rs and
3738
# exercises the FFI round-trip via the smoke test in wisp-audiokit.
3839
- run: nix develop .#ci --quiet --command cargo test -p wisp-audiokit
40+
# Exercises AppModel/session reducer regressions where GPUI and the
41+
# WispAudioKit bridge can link against the Metal toolchain.
42+
- run: nix develop .#ci --quiet --command cargo test -p wisp-desktop --all-targets

.github/workflows/swift.yaml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,4 +20,4 @@ jobs:
2020
steps:
2121
- uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
2222
- uses: ./.github/actions/setup-nix
23-
- run: nix develop .#ci --quiet --command swiftformat --lint native/WispAudioKit/Sources
23+
- run: nix develop .#ci --quiet --command swiftformat --lint native/WispAudioKit/Sources native/WispAudioKit/Tests

.gitignore

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,3 +2,6 @@
22
native/**/.build/
33
native/**/build/
44
native/**/.swiftpm/
5+
/formal/tla/states/
6+
/formal/tla/MC*.out
7+
/formal/tla/SpecTE*

Cargo.lock

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ serde = { version = "1.0.228", features = ["derive"] }
1818
serde_json = "1.0.150"
1919
tempfile = "3.27.0"
2020
thiserror = "2.0.18"
21+
uuid = { version = "1.23.1", features = ["v4"] }
2122

2223
[workspace.lints.clippy]
2324
all = { level = "warn", priority = -1 }

README.md

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -72,11 +72,31 @@ If you'd rather use Rust + Xcode directly:
7272
cargo build -p wisp-desktop --release
7373
```
7474

75+
### Formal verification
76+
77+
The session worker protocol and the whole-app navigation/session workflow have
78+
executable TLA+ models plus symbolic one-step invariant proofs in Z3:
79+
80+
```bash
81+
nix develop .#formal --command bash formal/check.sh
82+
```
83+
84+
See [`formal/README.md`](formal/README.md) for the verified properties,
85+
implementation mapping, assumptions, and extension workflow.
86+
7587
See `.github/workflows/release.yaml` for how the release `.app` bundle is produced — pushing a `v*` tag builds `Wisp.app` on a macOS 26 runner.
7688

77-
### Custom output directory
89+
### Custom data directory
90+
91+
Set `WISP_DATA_DIR` to override where `sessions.db` and the `recordings/`
92+
directory are stored. When unset, Wisp uses
93+
`~/Library/Application Support/dev.mokmok.wisp`.
7894

79-
Set `WISP_OUTPUT_DIR` to override where recordings are written. When unset, Wisp uses `~/Library/Application Support/dev.mokmok.wisp/recordings`.
95+
If a completed transcript cannot be committed to SQLite, Wisp writes an
96+
atomic `transcript-recovery.json` beside that session's WAV files, blocks a
97+
new recording, and retries reconciliation immediately or on the next launch.
98+
Wisp exits before recording if the durable database cannot be opened; it never
99+
treats an in-memory fallback as successful persistence.
80100

81101
### Local MCP bridge
82102

@@ -96,7 +116,7 @@ MCP hosts should run the bundled `wisp-mcp` binary over stdio, for example `/App
96116

97117
## Contributing
98118

99-
Issues and pull requests are welcome. Before sending a PR, please make sure `cargo fmt`, `cargo clippy --workspace --all-targets`, and `cargo test --workspace` pass under the same conditions as CI. For the Swift side, `make -C native/WispAudioKit` runs the equivalent checks.
119+
Issues and pull requests are welcome. Before sending a PR, please make sure `cargo fmt`, `cargo clippy --workspace --all-targets`, `cargo test --workspace`, and `nix develop .#formal --command bash formal/check.sh` pass under the same conditions as CI. For the Swift side, `make -C native/WispAudioKit` runs the equivalent checks.
100120

101121
## License
102122

apps/wisp-desktop/Cargo.toml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,7 @@ wisp-audiokit = { path = "../../crates/wisp-audiokit" }
3333
chrono = { workspace = true }
3434
serde = { workspace = true }
3535
serde_json = { workspace = true }
36+
uuid = { workspace = true }
3637

3738
# GPU-accelerated UI framework by the Zed team. macOS-only in practice;
3839
# Ubuntu CI excludes this crate (see .github/workflows/rust.yaml).

apps/wisp-desktop/src/app.rs

Lines changed: 111 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
//! marked `final` (the speech engine has locked it in).
1010
1111
use std::collections::VecDeque;
12-
use std::path::Path;
12+
use std::path::{Path, PathBuf};
1313
use std::time::Instant;
1414

1515
use chrono::{DateTime, Utc};
@@ -59,7 +59,7 @@ impl SessionState {
5959
/// While this is true the live transcript is the persistence source and
6060
/// must not be replaced by another view's segments.
6161
#[must_use]
62-
pub fn is_active(self) -> bool {
62+
pub const fn is_active(self) -> bool {
6363
matches!(
6464
self,
6565
Self::Starting | Self::Recording { .. } | Self::Stopping
@@ -263,13 +263,24 @@ pub struct AppModel {
263263
/// refreshed whenever a recording finishes or the user returns to the
264264
/// library.
265265
pub library: Vec<StoredSession>,
266-
/// `Some` while a session row exists in the database for the current
267-
/// live transcript. Allocated before audio starts and retained after a
268-
/// successful stop until the user navigates away or starts a new session.
266+
/// Open database row owned by an active or not-yet-persisted recording.
267+
/// Cleared only when finalisation commits or an unstarted row is deleted.
269268
pub current_session_id: Option<SessionId>,
269+
/// Persisted row associated with the transcript currently shown in the
270+
/// live view. Unlike the open handle, this remains after a successful
271+
/// finalisation so IPC/export metadata cannot drift to another session.
272+
pub linked_session_id: Option<SessionId>,
270273
/// A failed storage operation that must be retried before the live
271274
/// transcript can be discarded or another session can start.
272275
pub pending_session_write: Option<PendingSessionWrite>,
276+
/// Launch metadata retained until the transcript transaction commits.
277+
/// It lets a stop/retry create the database row if the initial `Started`
278+
/// update could not acquire or write storage.
279+
pub current_session_started_at: Option<DateTime<Utc>>,
280+
pub current_session_dir_name: Option<String>,
281+
/// Per-run audio directory. Retained with the transcript after a storage
282+
/// failure so a durable recovery snapshot can be written beside the WAVs.
283+
pub current_output_dir: Option<PathBuf>,
273284
/// The session being viewed in `View::History`, kept around so the
274285
/// header can render its title without re-querying.
275286
pub viewed_session: Option<StoredSession>,
@@ -288,7 +299,11 @@ impl AppModel {
288299
segments: Vec::new(),
289300
library: Vec::new(),
290301
current_session_id: None,
302+
linked_session_id: None,
291303
pending_session_write: None,
304+
current_session_started_at: None,
305+
current_session_dir_name: None,
306+
current_output_dir: None,
292307
viewed_session: None,
293308
recent_log: VecDeque::new(),
294309
last_error: None,
@@ -313,6 +328,20 @@ impl AppModel {
313328
model
314329
}
315330

331+
/// Whether the live transcript still owns worker or persistence state.
332+
/// A retained database handle after a failed finalization is deliberately
333+
/// treated as unsettled so navigation cannot silently discard it.
334+
pub fn has_unsettled_session(&self) -> bool {
335+
self.state.is_active()
336+
|| self.pending_session_write.is_some()
337+
|| self.current_output_dir.is_some()
338+
}
339+
340+
/// A stopped worker whose transcript transaction needs to be retried.
341+
pub fn has_pending_persistence(&self) -> bool {
342+
matches!(self.state, SessionState::Failed) && self.pending_session_write.is_some()
343+
}
344+
316345
/// Replace the cached library list. Called after storage reads (launch,
317346
/// recording end, post-delete).
318347
pub fn set_library(
@@ -323,31 +352,42 @@ impl AppModel {
323352
}
324353

325354
/// Move to the library screen and drop any live/historical segments so
326-
/// the next view enter starts from a clean slate.
355+
/// the next view enter starts from a clean slate. Navigation is ignored
356+
/// while a worker session is active; otherwise its future events could be
357+
/// attached to the library or to a historical transcript.
327358
pub fn show_library(&mut self) {
328-
if self.live_session_is_protected() {
359+
if self.has_unsettled_session() {
329360
return;
330361
}
331362
self.view = View::Library;
332363
self.segments.clear();
333364
self.viewed_session = None;
334365
self.current_session_id = None;
366+
self.linked_session_id = None;
335367
self.pending_session_write = None;
368+
self.current_session_started_at = None;
369+
self.current_session_dir_name = None;
370+
self.current_output_dir = None;
336371
self.last_error = None;
337372
}
338373

339374
/// Move to the live recording screen in idle state. Used by the
340-
/// library's "New Session" button.
375+
/// library's "New Session" button. An active session owns this view and
376+
/// cannot be replaced with a new one until it settles.
341377
pub fn show_new_session(&mut self) {
342-
if self.live_session_is_protected() {
378+
if self.has_unsettled_session() {
343379
return;
344380
}
345381
self.view = View::LiveSession;
346382
self.state = SessionState::Idle;
347383
self.segments.clear();
348384
self.viewed_session = None;
349385
self.current_session_id = None;
386+
self.linked_session_id = None;
350387
self.pending_session_write = None;
388+
self.current_session_started_at = None;
389+
self.current_session_dir_name = None;
390+
self.current_output_dir = None;
351391
self.last_error = None;
352392
}
353393

@@ -358,7 +398,7 @@ impl AppModel {
358398
session: StoredSession,
359399
segments: Vec<Segment>,
360400
) {
361-
if self.live_session_is_protected() {
401+
if self.has_unsettled_session() {
362402
return;
363403
}
364404
self.view = View::History {
@@ -367,37 +407,35 @@ impl AppModel {
367407
self.segments = segments;
368408
self.viewed_session = Some(session);
369409
self.current_session_id = None;
410+
self.linked_session_id = None;
370411
self.pending_session_write = None;
412+
self.current_session_started_at = None;
413+
self.current_session_dir_name = None;
414+
self.current_output_dir = None;
371415
// Historical segments are already finalized.
372416
self.finalize_all_segments();
373417
for seg in &mut self.segments {
374418
seg.refresh_display();
375419
}
376420
}
377421

378-
/// Prepare a fresh recording while preserving the invariant that the
379-
/// visible segments and `current_session_id` always describe the same
380-
/// live session. This also makes menu/shortcut starts from Library or
381-
/// History enter the live view before runner updates arrive.
382-
pub fn begin_session(&mut self) {
383-
if self.live_session_is_protected() {
384-
return;
422+
/// Normalize any terminal screen to a fresh live transcript, then enter
423+
/// the Starting phase. Global shortcuts call this before enqueueing Start
424+
/// so Library/History can never remain the owner of live worker events.
425+
#[must_use]
426+
pub fn begin_session_start(&mut self) -> bool {
427+
if self.has_unsettled_session() {
428+
return false;
385429
}
386-
self.view = View::LiveSession;
430+
self.show_new_session();
387431
self.state = SessionState::Starting;
388-
self.segments.clear();
389-
self.viewed_session = None;
390-
self.current_session_id = None;
391-
self.pending_session_write = None;
392-
self.last_error = None;
432+
true
393433
}
394434

395-
/// Whether leaving the live view could discard an in-flight or not-yet
396-
/// persisted transcript. A failed finalisation keeps its session id so it
397-
/// can be retried without mixing it into a subsequent recording.
398-
#[must_use]
399-
pub fn live_session_is_protected(&self) -> bool {
400-
self.state.is_active() || self.pending_session_write.is_some()
435+
/// Compatibility wrapper for callers that do not need the acceptance
436+
/// result. Prefer `begin_session_start` before enqueueing worker commands.
437+
pub fn begin_session(&mut self) {
438+
let _ = self.begin_session_start();
401439
}
402440

403441
pub fn set_state(
@@ -841,6 +879,50 @@ mod tests {
841879
assert!(m.needs_live_ui_tick());
842880
}
843881

882+
#[test]
883+
fn active_session_rejects_top_level_navigation() {
884+
let active_states = [
885+
SessionState::Starting,
886+
SessionState::Recording {
887+
started_at: std::time::Instant::now(),
888+
},
889+
SessionState::Stopping,
890+
];
891+
892+
for state in active_states {
893+
let mut m = AppModel::new();
894+
m.show_new_session();
895+
m.ingest(Event::Result(r(SourceLabel::Mic, 1, "live")));
896+
m.current_session_id = Some(SessionId::from(42));
897+
m.state = state;
898+
899+
m.show_library();
900+
m.show_new_session();
901+
m.show_history(stored_session(7), Vec::new());
902+
903+
assert_eq!(m.view, View::LiveSession);
904+
assert_eq!(m.state, state);
905+
assert_eq!(m.current_session_id, Some(SessionId::from(42)));
906+
assert_eq!(m.segments.len(), 1);
907+
assert_eq!(m.segments[0].text, "live");
908+
}
909+
}
910+
911+
#[test]
912+
fn global_start_normalizes_history_to_a_fresh_live_view() {
913+
let mut m = AppModel::new();
914+
m.show_history(stored_session(7), Vec::new());
915+
assert!(matches!(m.view, View::History { .. }));
916+
917+
assert!(m.begin_session_start());
918+
919+
assert_eq!(m.view, View::LiveSession);
920+
assert_eq!(m.state, SessionState::Starting);
921+
assert!(m.segments.is_empty());
922+
assert!(m.viewed_session.is_none());
923+
assert!(m.current_session_id.is_none());
924+
}
925+
844926
#[test]
845927
fn log_buffer_is_bounded() {
846928
let mut m = AppModel::new();

0 commit comments

Comments
 (0)