git-ents.gitmain
⌘K
foforge

crates/verify/ents-verify/src/durability.rs

durability.rs95 lines · 3.3 KB · rusthistorycomment on this file
1//! Phase 5 — durability ordering (`verify/exercise.md`, "Phase 5"),
2//! replacing the deleted `verify/tla/Durability.tla`.
3//!
4//! SKELETON. Every action body is `todo!()`; filling in
5//! [`Model::actions`] and [`Model::next_state`] for real is the human
6//! exercise.
7//!
8//! Deployment note: the exercise document frames this phase around a
9//! hosted Tigris-object-store + Postgres-CAS split. The project
10//! currently deploys neither — serving is plain git http-backend over
11//! one filesystem — so the state and actions here are named for the
12//! general shape (object write, ref CAS, crash), and the Tigris/Pg
13//! instantiation is deferred until such a deployment exists. The
14//! invariant under study is unchanged: no ref points outside the
15//! durable object set.
16
17#![expect(
18 clippy::todo,
19 reason = "Phase 5 skeleton — filling this in is the human exercise, not this scaffold's job"
20)]
21
22use stateright::{Model, Property};
23
24/// Durability state: which objects have reached durable storage, and
25/// the ref store's current tips. SKELETON.
26#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
27pub struct State {
28 /// Objects durably written so far.
29 pub durable: Vec<&'static str>,
30 /// Current tip of each ref in `crate::REFS`, in the same order;
31 /// `None` means the ref is unborn.
32 pub refs: [Option<&'static str>; 4],
33}
34
35/// Durability actions (`verify/exercise.md`, Phase 5): `ObjectWrite`,
36/// `RefCAS`, `Crash` at any point. SKELETON.
37#[derive(Clone, Debug, PartialEq, Eq, Hash)]
38pub enum Action {
39 /// An object (or pack) reaches durable storage.
40 ObjectWrite,
41 /// The ref store compare-and-swaps a tip — the write-order question
42 /// this phase exists to settle lives here.
43 RefCas,
44 /// Crash at any point; recovery obligations follow from what
45 /// survives.
46 Crash,
47}
48
49/// The Phase 5 durability model. SKELETON.
50pub struct DurabilityModel;
51
52impl Model for DurabilityModel {
53 type State = State;
54 type Action = Action;
55
56 fn init_states(&self) -> Vec<Self::State> {
57 vec![State::default()]
58 }
59
60 fn actions(&self, _state: &Self::State, _actions: &mut Vec<Self::Action>) {
61 todo!("exercise: enumerate ObjectWrite/RefCas/Crash per verify/exercise.md Phase 5")
62 }
63
64 fn next_state(&self, _last_state: &Self::State, _action: Self::Action) -> Option<Self::State> {
65 todo!("exercise: Phase 5's transition relation, including crash faults")
66 }
67
68 fn properties(&self) -> Vec<Property<Self>> {
69 vec![
70 // The invariant this phase exists to prove: no ref in the
71 // ref store points outside the durable object set. STATED
72 // here so the ledger row has a formal object to point at;
73 // NOT proved — the transition relation above is a stub, so
74 // checking this today says nothing.
75 Property::always("refs_point_durable", |_, _| true /* TODO(exercise) */),
76 ]
77 }
78}
79
80#[cfg(test)]
81mod tests {
82 use stateright::Checker;
83
84 use super::*;
85
86 /// Running this model requires [`Model::actions`] and
87 /// [`Model::next_state`], both `todo!()` until the human exercise
88 /// fills them in. Ignored so `cargo test --workspace` stays green
89 /// while the skeleton exists.
90 #[test]
91 #[ignore = "exercise stub: Phase 5's transition relation is unwritten"]
92 fn model_runs() {
93 let _ = DurabilityModel.checker().spawn_bfs().join();
94 }
95}