git-ents.gitmain
⌘K
foforge

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

receive.rs153 lines · 6.3 KB · rusthistorycomment on this file
1//! Phase 3 — gate and receive as a protocol (`verify/exercise.md`,
2//! "Phase 3"), replacing the deleted `verify/tla/Receive.tla`.
3//!
4//! SKELETON, with one deliberate exception: [`gate_admits`] calls
5//! [`ents_gate_rules::gate`] directly on a transaction's `Facts` — that
6//! direct call *is* the refinement mapping this module's `GateCheck`
7//! action would enable on, replacing what `Receive.tla`'s `GateAdmits`
8//! transcribed by hand. Every other action body is `todo!()`; filling in
9//! [`Model::actions`] and [`Model::next_state`] for real is the human
10//! exercise, not this scaffold's job.
11//!
12//! Discharges, once filled in: `docs/abstractions.adoc` §5 (tip
13//! invariant, adoption, revocation), §4 (anti-replay);
14//! `docs/spec/receive.adoc`; `docs/spec/gate.adoc` epoch bootstrap.
15
16#![expect(
17 clippy::todo,
18 reason = "Phase 3 skeleton — filling this in is the human exercise, not this scaffold's job"
19)]
20
21use ents_gate_rules::{Facts, gate};
22use stateright::{Model, Property};
23
24/// `gate(facts) = {}`: the enabling condition a filled-in `GateCheck`
25/// action would use. This is real code, not a stub — it is the seven
26/// denial rules, called directly, standing in for `Receive.tla`'s
27/// hand-transcribed `GateAdmits`.
28#[must_use]
29pub fn gate_admits(facts: Facts) -> bool {
30 gate(facts).is_empty()
31 // TODO(exercise): refname recomputation from signed content (the §4
32 // binding rule ents-gate-rules omits; ledger row DIVERGED,
33 // crate::search::SearchModel's `binding_refname_recomputed`
34 // property) and the epoch rule (§5) are not part of `gate()`, so
35 // this enabling condition inherits both gaps. Phase 3 decides
36 // whether `ents-gate` proper's check composes in here.
37}
38
39/// Protocol state (§5): the current tip of every ref in the bounded
40/// universe (`crate::REFS`), the object set, enrolled members, and the
41/// config ref's epoch. SKELETON — named for the exercise's obligations,
42/// not yet wired to a transition relation.
43#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
44pub struct State {
45 /// Current tip of each ref in `crate::REFS`, in the same order;
46 /// `None` means the ref is unborn.
47 pub refs: [Option<&'static str>; 4],
48 /// Objects the store currently has.
49 pub objects: Vec<&'static str>,
50 /// Enrolled member keys.
51 pub members: Vec<&'static str>,
52 /// The config ref's epoch (§5: "the epoch-setting commit is the
53 /// first gated tip of the config ref").
54 pub epoch: u32,
55}
56
57/// Protocol actions (`verify/exercise.md`, Phase 3): `Propose`,
58/// `GateCheck`, `CAS`, `AdoptMerge`, `SelfMerge`. SKELETON.
59#[derive(Clone, Debug, PartialEq, Eq, Hash)]
60pub enum Action {
61 /// A writer proposes a transaction (two writers minimum, per the
62 /// exercise's model).
63 Propose,
64 /// The gate evaluates a proposed transaction; a filled-in
65 /// implementation enables this action exactly when [`gate_admits`]
66 /// holds for the proposal in play.
67 GateCheck,
68 /// Compare-and-swap the ref tip — the anti-replay mechanism §4
69 /// relies on parent-hash freshness for.
70 Cas,
71 /// Adoption: contributor commit in ancestry, adopter signature at
72 /// tip, always a merge (never a rewrite).
73 AdoptMerge,
74 /// Two of one member's own machines racing a single-writer ref —
75 /// `docs/abstractions.adoc` §4's same-actor divergence.
76 SelfMerge,
77}
78
79/// The Phase 3 protocol model. SKELETON.
80pub struct ReceiveModel;
81
82impl Model for ReceiveModel {
83 type State = State;
84 type Action = Action;
85
86 fn init_states(&self) -> Vec<Self::State> {
87 vec![State::default()]
88 }
89
90 fn actions(&self, _state: &Self::State, _actions: &mut Vec<Self::Action>) {
91 todo!(
92 "exercise: enumerate Propose/GateCheck/Cas/AdoptMerge/SelfMerge per verify/exercise.md Phase 3"
93 )
94 }
95
96 fn next_state(&self, _last_state: &Self::State, _action: Self::Action) -> Option<Self::State> {
97 todo!(
98 "exercise: Phase 3's transition relation, using gate_admits as GateCheck's enabling condition"
99 )
100 }
101
102 fn properties(&self) -> Vec<Property<Self>> {
103 vec![
104 // Obligation 1: "the tip of a meta-ref is signed by a
105 // member authorized for that refname" is preserved by every
106 // action — pay attention to SelfMerge (is the merge commit
107 // itself signed in the implementation? see ents-sync/src
108 // and ents-receive/src/reconcile.rs).
109 Property::always(
110 "tip_invariant_inductive",
111 |_, _| true, /* TODO(exercise) */
112 ),
113 // Obligation 2: adoption preserves the tip invariant, even
114 // when the contributor's commit is itself a merge of
115 // unauthorized commits.
116 Property::always(
117 "adoption_preserves_tip_invariant",
118 |_, _| true, /* TODO(exercise) */
119 ),
120 // Obligation 3: a replayed genesis against a not-yet-created
121 // ref is safe only in conjunction with Phase 2's binding
122 // totality — state the exact conjunction.
123 Property::always("anti_replay", |_, _| true /* TODO(exercise) */),
124 // Obligation 4: from an empty store, is there a state where
125 // the gate must read the epoch from a ref whose tip is not
126 // yet gated? Cite ents-gate/src/{config,policy}.rs.
127 Property::always("epoch_bootstrap", |_, _| true /* TODO(exercise) */),
128 // Obligation 5: a member valid at admission and revoked
129 // later — does naive re-verification of historical tips
130 // fail, and does the epoch mechanism actually prevent that?
131 Property::always("revocation", |_, _| true /* TODO(exercise) */),
132 ]
133 }
134}
135
136#[cfg(test)]
137mod tests {
138 use stateright::Checker;
139
140 use super::*;
141
142 /// Running this model requires [`Model::actions`] and
143 /// [`Model::next_state`], both `todo!()` until the human exercise
144 /// fills them in. Ignored so `cargo test --workspace` stays green
145 /// while the skeleton exists — the one permitted use of `#[ignore]`
146 /// in this codebase, because this is a declared stub, not a passed-
147 /// off result.
148 #[test]
149 #[ignore = "exercise stub: Phase 3's transition relation is unwritten"]
150 fn model_runs() {
151 let _ = ReceiveModel.checker().spawn_bfs().join();
152 }
153}