Add replay cursor Quint contracts

.gitignore

@@ -75,3 +75,6 @@ packages/python/turbolite/turbolite
 
 # Proptest regression minimization files (generated during failing runs)
 *.proptest-regressions
+
+# Quint / Apalache model-checker output
+_apalache-out/

Cargo.toml

@@ -106,9 +106,8 @@ rmp-serde = "1.3.1"
 # Canonical encoding for the Turbolite manifest wire format. ciborium
 # produces RFC 8949 §4.2 deterministically-encoded CBOR when used with
 # `ciborium::ser::into_writer` on a serde-derived value whose field
-# order is fixed and whose integers use smallest-length encoding — the
-# property phase 004 relies on for BLAKE3-hash stability across
-# implementations.
+# order is fixed and whose integers use smallest-length encoding — needed
+# for BLAKE3 hash stability across implementations.
 ciborium = "0.2"
 # Cryptographic hash for the chain link primitive. BLAKE3 chosen for
 # canonical-byte hashing of manifest and delta objects (replay cursor

Makefile

@@ -26,6 +26,20 @@ FFI_DIR := turbolite-ffi
 # Features forwarded to cargo.
 FEATURES ?= zstd
 
+QUINT ?= npx -y @informalsystems/quint@0.32.0
+OPENJDK_PREFIX ?= $(shell brew --prefix openjdk 2>/dev/null)
+JAVA_PATH_PREFIX := $(if $(OPENJDK_PREFIX),$(OPENJDK_PREFIX)/bin:)
+SPEC_NEGATIVE_STEPS := \
+	badWrongEpochStep \
+	badWrongWriterStep \
+	badSkippedSeqStep \
+	badPrevChecksumStep \
+	badEquivocationStep \
+	badChecksumCollisionStep \
+	badStaleWriterAfterPromotionStep \
+	badPromotionCursorStep \
+	badPromotionPageCountStep
+
 # ── FFI build passthrough ─────────────────────────────────────────
 
 .PHONY: lib lib-bundled ext ext-local header
@@ -57,6 +71,83 @@ test: ## Run all tests (Rust unit + FFI)
 test-all: ## Run all tests including tiered/S3
 	cargo test --features zstd,tiered,bundled-sqlite
 
+.PHONY: specs-typecheck
+specs-typecheck: ## Typecheck Quint substrate specs
+	$(QUINT) typecheck specs/cursor_chain.qnt
+	$(QUINT) typecheck specs/cursor_chain_liveness.qnt
+
+.PHONY: specs
+specs: specs-typecheck ## Run Quint substrate specs (typecheck + simulator invariants)
+	$(QUINT) run specs/cursor_chain.qnt \
+		--max-samples=200 --max-steps=8 --invariants=safety
+
+.PHONY: specs-progress
+specs-progress: specs-typecheck ## Run deterministic Quint progress scenario
+	$(QUINT) run specs/cursor_chain.qnt \
+		--step=progressStep --max-samples=1 --max-steps=4 \
+		--invariants=safety boundedProgress
+
+.PHONY: specs-negative
+specs-negative: specs-typecheck ## Run Quint specs that are expected to violate safety
+	@for step in $(SPEC_NEGATIVE_STEPS); do \
+		out=$$(mktemp "$${TMPDIR:-/tmp}/turbolite-quint-$$step.XXXXXX") || exit 1; \
+		echo "expecting safety violation: $$step"; \
+		if $(QUINT) run specs/cursor_chain.qnt \
+			--max-samples=20 --max-steps=2 --step=$$step \
+			--invariants=safety --verbosity=0 \
+			>"$$out" 2>&1; then \
+			cat "$$out"; \
+			rm -f "$$out"; \
+			echo "expected $$step to violate safety"; \
+			exit 1; \
+		elif ! grep -q "Invariant violated" "$$out"; then \
+			cat "$$out"; \
+			rm -f "$$out"; \
+			echo "expected $$step to fail by violating safety"; \
+			exit 1; \
+		fi; \
+		rm -f "$$out"; \
+	done
+
+.PHONY: specs-all
+specs-all: specs specs-progress specs-negative specs-rust specs-verify specs-liveness specs-liveness-negative ## Run all local spec checks
+
+.PHONY: specs-verify
+specs-verify: specs-typecheck ## Run Quint bounded model checker (requires Java)
+	PATH="$(JAVA_PATH_PREFIX)$$PATH" $(QUINT) verify specs/cursor_chain.qnt \
+		--max-steps=8 --invariants=safety
+	PATH="$(JAVA_PATH_PREFIX)$$PATH" $(QUINT) verify specs/cursor_chain.qnt \
+		--step=progressStep --max-steps=4 --invariants=safety boundedProgress
+
+.PHONY: specs-rust
+specs-rust: ## Run Rust tests that bridge the Quint substrate contract
+	cargo test --features zstd,bundled-sqlite replay_cursor_contract
+
+.PHONY: specs-liveness
+specs-liveness: specs-typecheck ## Run TLC temporal liveness check under explicit fairness
+	PATH="$(JAVA_PATH_PREFIX)$$PATH" $(QUINT) verify specs/cursor_chain_liveness.qnt \
+		--backend=tlc --max-steps=8 --invariants=safety \
+		--temporal=fairStablePrefixProgress
+
+.PHONY: specs-liveness-negative
+specs-liveness-negative: specs-typecheck ## Run temporal property expected to fail without fairness
+	@out=$$(mktemp "$${TMPDIR:-/tmp}/turbolite-quint-badUnfairPollingProgress.XXXXXX") || exit 1; \
+	if PATH="$(JAVA_PATH_PREFIX)$$PATH" $(QUINT) verify specs/cursor_chain_liveness.qnt \
+		--backend=tlc --max-steps=8 --invariants=safety \
+		--temporal=badUnfairPollingProgress \
+		>"$$out" 2>&1; then \
+		cat "$$out"; \
+		rm -f "$$out"; \
+		echo "expected badUnfairPollingProgress to violate temporal progress"; \
+		exit 1; \
+	elif ! grep -q "Temporal properties were violated" "$$out"; then \
+		cat "$$out"; \
+		rm -f "$$out"; \
+		echo "expected badUnfairPollingProgress to fail by violating temporal progress"; \
+		exit 1; \
+	fi; \
+	rm -f "$$out"
+
 .PHONY: test-ext test-ffi test-ffi-tiered test-ffi-python test-ffi-c test-ffi-go test-ffi-node
 test-ext test-ffi test-ffi-tiered test-ffi-python test-ffi-c test-ffi-go test-ffi-node: ## FFI / loadable-ext tests live in turbolite-ffi now
 	$(MAKE) -C $(FFI_DIR) $@

specs/README.md

@@ -0,0 +1,229 @@
+# Turbolite Quint Specs
+
+These specs model small protocol contracts at the Turbolite/HADB
+boundary. They are not part of the normal Rust build, and they do not
+model SQLite page contents, compression, encryption, object-store
+consistency, or prefetch scheduling.
+
+The first safety spec is `cursor_chain.qnt`. It models the replay cursor
+base/delta contract: ordered delta application, writer and lease fencing,
+chain anchors, promotion, and fatal ambiguity handling.
+
+## Tools
+
+Use Quint 0.32.0 through `npx`:
+
+```sh
+npx -y @informalsystems/quint@0.32.0 --version
+```
+
+`quint run` and `quint typecheck` work without Java. `quint verify`
+uses Apalache by default for bounded safety checks and TLC for the
+temporal liveness check. Both verifier backends require a local Java
+runtime. On macOS, Homebrew OpenJDK is enough:
+
+```sh
+brew install openjdk
+```
+
+## Local Checks
+
+From the Turbolite repo root:
+
+```sh
+make specs
+```
+
+This runs:
+
+```sh
+npx -y @informalsystems/quint@0.32.0 typecheck specs/cursor_chain.qnt
+npx -y @informalsystems/quint@0.32.0 typecheck specs/cursor_chain_liveness.qnt
+npx -y @informalsystems/quint@0.32.0 run specs/cursor_chain.qnt \
+  --max-samples=200 --max-steps=8 --invariants=safety
+```
+
+Expected result: typecheck succeeds, simulator runs without invariant
+violations.
+
+The progress check is deterministic:
+
+```sh
+make specs-progress
+```
+
+This seeds a three-delta valid prefix and uses the `progressStep`
+relation. It is a bounded no-stutter scenario, not a proof of general
+fair liveness for the normal `step` relation. `boundedProgress`
+requires the follower to apply all three seeded deltas within the
+bound while preserving `safety`.
+
+To run the positive safety simulation, deterministic progress scenario,
+expected-failure counterexamples, Rust bridge tests, bounded model
+checker, and TLC liveness checks:
+
+```sh
+make specs-all
+```
+
+This is the full local verification target, not a quick smoke check. It
+requires Java for Apalache/TLC and intentionally exercises the Rust replay
+cursor bridge after real replay finalization.
+
+## Model Checker
+
+When Java is available, run the bounded model checker:
+
+```sh
+make specs-verify
+```
+
+This runs:
+
+```sh
+PATH="$(brew --prefix openjdk)/bin:$PATH" \
+  npx -y @informalsystems/quint@0.32.0 verify specs/cursor_chain.qnt \
+    --max-steps=8 --invariants=safety
+PATH="$(brew --prefix openjdk)/bin:$PATH" \
+  npx -y @informalsystems/quint@0.32.0 verify specs/cursor_chain.qnt \
+    --step=progressStep --max-steps=4 --invariants=safety boundedProgress
+```
+
+Expected result: verification succeeds over the bounded state space.
+
+## Temporal Liveness
+
+`cursor_chain_liveness.qnt` is a separate, smaller temporal model. It
+does not claim object-store, root-publish, writer-election, or full
+promotion liveness. Its environment assumptions are explicit:
+
+- the root/lease fence is stable,
+- a three-delta valid prefix remains visible,
+- no fatal equivocation/collision is present,
+- the follower keeps polling,
+- `applyNext` is weakly fair when it stays enabled.
+
+Run the positive temporal check with TLC:
+
+```sh
+make specs-liveness
+```
+
+This checks:
+
+```sh
+npx -y @informalsystems/quint@0.32.0 verify specs/cursor_chain_liveness.qnt \
+  --backend=tlc --max-steps=8 --invariants=safety \
+  --temporal=fairStablePrefixProgress
+```
+
+Expected result: TLC checks the complete small state space and finds no
+temporal violation. The property is: under weak fairness of `applyNext`,
+a stable available prefix eventually leads to the follower catching up.
+
+The companion negative check proves the fairness assumption is doing real
+work:
+
+```sh
+make specs-liveness-negative
+```
+
+Expected result: `badUnfairPollingProgress` violates temporal progress,
+because without fairness the follower can poll/stutter forever.
+
+## Negative Counterexamples
+
+The spec contains intentionally bad step actions. They should all
+violate `safety` and produce short counterexamples:
+
+```sh
+make specs-negative
+```
+
+Expected result: each named bad step reports an expected invariant
+violation:
+
+- `badWrongEpochStep`
+- `badWrongWriterStep`
+- `badSkippedSeqStep`
+- `badPrevChecksumStep`
+- `badEquivocationStep`
+- `badChecksumCollisionStep`
+- `badStaleWriterAfterPromotionStep`
+- `badPromotionCursorStep`
+- `badPromotionPageCountStep`
+
+`badChecksumCollisionStep` uses the spec's compact
+`payloadFingerprint` field to stand in for the full production delta
+envelope: changed page bytes, commit boundary, idempotency key, page
+counts, sequence, writer, epoch, and chain link. The model therefore
+checks the intended rule, "one checksum cannot name two different
+payload envelopes," without expanding page bytes in Quint.
+
+For a full counterexample trace, run an individual step without
+`--verbosity=0`, for example:
+
+```sh
+npx -y @informalsystems/quint@0.32.0 run specs/cursor_chain.qnt \
+  --max-samples=20 --max-steps=2 --step=badWrongEpochStep \
+  --invariants=safety
+```
+
+## Rust Mapping
+
+`cursor_chain.qnt` models these Rust surfaces:
+
+- `src/tiered/manifest.rs`
+  - `ReplayCursor`
+  - `Manifest::writer_id`
+- `src/tiered/wire.rs`
+  - canonical manifest bytes
+  - `base_anchor_checksum`
+- `src/tiered/vfs.rs`
+  - `manifest_bytes_with_replay_cursor_anchor`
+  - `update_replay_cursor`
+  - `publish_replayed_base_with_replay_cursor_anchor`
+- `src/tiered/replay.rs`
+  - direct page replay lifecycle
+
+The modeled Rust-facing properties have a matching Rust bridge target:
+
+```sh
+make specs-rust
+```
+
+This runs `cargo test --features zstd,bundled-sqlite replay_cursor_contract`.
+Those tests bridge the first Quint model to production Rust surfaces:
+
+- `replay_cursor_contract_manifest_bytes_stamps_cursor_writer_and_anchor`
+  checks the VFS publisher path stamps seq/epoch/writer and the base
+  chain anchor.
+- `replay_cursor_contract_begin_replay_uses_installed_cursor_floor`
+  checks the default replay handle resumes after the installed cursor,
+  not behind it.
+- `replay_cursor_contract_manifest_bytes_rejects_invalid_cursor_inputs`
+  checks anchored cursor publication rejects zero epochs, blank writers, and
+  backward cursor movement.
+- `replay_cursor_contract_update_replay_cursor_preserves_base_shape_and_writer`
+  checks follower cursor advancement does not rewrite the base shape.
+- `replay_cursor_contract_update_replay_cursor_rejects_malformed_or_backward_cursor`
+  checks follower cursor advancement rejects malformed anchors, missing
+  writer identity, and backward movement.
+- `replay_cursor_contract_publish_replayed_base_stamps_final_cursor_anchor`
+  checks promotion stamps seq/epoch/writer and recomputes the anchor
+  over the final published base.
+- `replay_cursor_contract_publish_replayed_base_after_replay_carries_post_replay_state`
+  checks the anchored publisher after a real replay finalize, including
+  non-regressing legacy change counter, exact replay cursor, writer, and
+  recomputed base anchor.
+- `replay_cursor_contract_base_anchor_binds_cursor_epoch_and_writer`
+  checks the wire hash domain includes seq, lease epoch, and writer.
+- `replay_cursor_contract_recovery_plan_applies_contiguous_prefix_and_page_counts`
+  checks a three-delta prefix advances contiguous sequence and
+  grow/shrink page counts.
+- `replay_cursor_contract_recovery_plan_rejects_stale_epoch_candidate`
+  checks stale-epoch candidates do not satisfy the root fence.
+
+Existing Sashimono tests in `src/tiered/sashimono.rs` also cover wrong
+writer, missing gaps, duplicate same-seq candidates, wrong base page
+count, page-size mismatch, and corrupt/torn delta payloads.