Skip to content

Add replay cursor Quint contracts#41

Merged
russellromney merged 1 commit into
mainfrom
codex/replay-cursor-quint
Jun 9, 2026
Merged

Add replay cursor Quint contracts#41
russellromney merged 1 commit into
mainfrom
codex/replay-cursor-quint

Conversation

@russellromney

Copy link
Copy Markdown
Owner

Summary

  • add Quint replay-cursor safety/progress specs and Makefile targets
  • add Rust replay-cursor bridge/contract tests
  • harden replay cursor publishing/resume semantics in the tiered VFS
  • remove planning-artifact names from the touched replay-cursor implementation surface

Tests

  • make specs-all
  • cargo test --features zstd,bundled-sqlite replay_cursor_contract
  • cargo test --features zstd,bundled-sqlite tiered::wire::tests
  • git diff --check

Notes

  • Requires local Java/Quint/Apalache tooling for the formal spec targets.
  • This is the Turbolite dependency for the haqlite replay-cursor orchestration PR.

@russellromney russellromney merged commit 79b38c5 into main Jun 9, 2026
4 checks passed
@russellromney russellromney deleted the codex/replay-cursor-quint branch June 9, 2026 06:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant