git-ents.gitmain
⌘K
foforge

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

effects.rs126 lines · 4.6 KB · rusthistorycomment on this file
1//! Phase 4 — effects (`verify/exercise.md`, "Phase 4"), replacing the
2//! deleted `verify/tla/Effects.tla`, building on [`crate::receive`]'s
3//! state.
4//!
5//! SKELETON. Every action body is `todo!()`; filling in
6//! [`Model::actions`] and [`Model::next_state`] for real is the human
7//! exercise.
8//!
9//! Discharges, once filled in: `docs/abstractions.adoc` §6 (monotone,
10//! exactly-once effects); `docs/spec/effect.adoc` (trigger set, dedup
11//! key `(effect, refname, new_oid)`, results write-back, admin-only
12//! authoring). Note `ents_gate_rules`' module docs mark the
13//! cross-transaction dedup obligation as a deliberate gap — this model
14//! is where that obligation lives.
15
16#![expect(
17 clippy::todo,
18 reason = "Phase 4 skeleton — filling this in is the human exercise, not this scaffold's job"
19)]
20
21use stateright::{Model, Property};
22
23/// Protocol state, extending [`crate::receive::State`] with effect
24/// bookkeeping: which commits have entered the trigger set (§6), the
25/// at-least-once delivery queue's dedup keys, and the result-ref writes
26/// performed so far. SKELETON.
27#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
28pub struct State {
29 /// The Phase 3 protocol state this phase builds on.
30 pub receive: crate::receive::State,
31 /// Commits that have entered the trigger set (§6: "fires once per
32 /// commit that enters the set").
33 pub triggered: Vec<&'static str>,
34 /// At-least-once delivery: dedup keys `(effect, refname, new_oid)`
35 /// currently enqueued.
36 pub queue: Vec<(&'static str, &'static str, &'static str)>,
37 /// Result-ref writes performed so far, keyed the same way as
38 /// [`Self::queue`].
39 pub results: Vec<(&'static str, &'static str, &'static str)>,
40}
41
42/// Protocol actions (`verify/exercise.md`, Phase 4): `RefAdvance`,
43/// `TriggerEval`, `Enqueue`, `Execute`, `ResultPush`. SKELETON.
44#[derive(Clone, Debug, PartialEq, Eq, Hash)]
45pub enum Action {
46 /// A gated ref advance (reuses [`crate::receive::gate_admits`] when
47 /// composed with Phase 3).
48 RefAdvance,
49 /// A commit enters the trigger set (§6). The delete-and-repush
50 /// re-entry question — is triggering monotone? — lives here.
51 TriggerEval,
52 /// At-least-once enqueue of a dedup key.
53 Enqueue,
54 /// The executor runs an effect; may crash and restart (duplicate
55 /// delivery).
56 Execute,
57 /// Result write-back: a gated write like any other, by an executor
58 /// member key (`effect.results-writeback`).
59 ResultPush,
60}
61
62/// The Phase 4 effects model. SKELETON.
63pub struct EffectsModel;
64
65impl Model for EffectsModel {
66 type State = State;
67 type Action = Action;
68
69 fn init_states(&self) -> Vec<Self::State> {
70 vec![State::default()]
71 }
72
73 fn actions(&self, _state: &Self::State, _actions: &mut Vec<Self::Action>) {
74 todo!(
75 "exercise: enumerate RefAdvance/TriggerEval/Enqueue/Execute/ResultPush per verify/exercise.md Phase 4"
76 )
77 }
78
79 fn next_state(&self, _last_state: &Self::State, _action: Self::Action) -> Option<Self::State> {
80 todo!("exercise: Phase 4's transition relation")
81 }
82
83 fn properties(&self) -> Vec<Property<Self>> {
84 vec![
85 // Obligation 1: the dedup key (effect, refname, new_oid)
86 // yields result-ref idempotency under duplicate delivery
87 // and executor crash-restart.
88 Property::always(
89 "exactly_once_observable_effect",
90 |_, _| true, /* TODO(exercise) */
91 ),
92 // Obligation 2: a ref deleted and re-pushed to the same oid
93 // — does the commit re-enter the trigger set? Defines
94 // whether triggers are monotone.
95 Property::always(
96 "trigger_set_monotone",
97 |_, _| true, /* TODO(exercise) */
98 ),
99 // Obligation 3: no sequence lets a non-admin cause execution
100 // of content they authored as an effect (composes with
101 // crate::search's binding_refname_recomputed property —
102 // this was the original cross-ref replay scenario).
103 Property::always(
104 "authorization_asymmetry",
105 |_, _| true, /* TODO(exercise) */
106 ),
107 ]
108 }
109}
110
111#[cfg(test)]
112mod tests {
113 use stateright::Checker;
114
115 use super::*;
116
117 /// Running this model requires [`Model::actions`] and
118 /// [`Model::next_state`], both `todo!()` until the human exercise
119 /// fills them in. Ignored so `cargo test --workspace` stays green
120 /// while the skeleton exists.
121 #[test]
122 #[ignore = "exercise stub: Phase 4's transition relation is unwritten"]
123 fn model_runs() {
124 let _ = EffectsModel.checker().spawn_bfs().join();
125 }
126}