1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
schema: 1
subject_requirements: requirements
documents:
- prefix: SYS
path: .
- prefix: API
path: api
- prefix: DLV
path: delivery
- prefix: PER
path: persistence
- prefix: SCH
path: scheduling
- prefix: WS
path: websocket
# Asserted (cargo test) verify route: qrusty's integration tests use test-only
# helpers gated behind `#[cfg(any(test, feature = "test-helpers"))]`, so the test
# target only compiles with the feature (mirrors `make test`). Without this the
# harness fails to compile and verdicts park on `unknown`.
verify:
cargo:
features:
# PER-0002's queue-prefix predicate lives in the C-free `qrusty_core` member
# crate so the category-1 provers (Kani/Creusot) can codegen it — the umbrella
# `qrusty` crate pulls `rocksdb` C-FFI and cannot be codegen'd. Per-requirement
# override only: every other requirement still verifies against the subject.
crates:
PER-0002: crates/qrusty_core
# SYS-0031 is a pure liveness property (drifted ~> consistent) whose
# Drifted/Consistent operators live only in the standalone sub-machine, not
# in the composed Spec — checked against the composed model it is an honest
# but useless `unknown` (Unknown operator: Drifted'). Point it at the
# standalone ReconcileSpec, whose WF_vars(Reconcile) fairness makes
# Convergence decidable. See specs/CounterReconcileModel.{tla,cfg}. The
# soundness of the sub-machine abstraction is argued in the SYS-0031 prose.
models:
SYS-0031: