git-ents.gitmain
⌘K
foforge

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

search.rs432 lines · 17.3 KB · rusthistorycomment on this file
1//! Phase 0.5 — verify the verifier (`verify/exercise.md`, "Phase 0.5"),
2//! replacing `verify/alloy/gate_rules.als`'s `check` commands with an
3//! exhaustive [`stateright`] search over the crate's own vocabulary.
4//!
5//! `ents_gate_rules` can *evaluate* its seven denial rules over one
6//! supplied transaction; it cannot search for the transaction nobody
7//! thought of. This module runs that search: [`SearchModel`]'s states
8//! are a transaction under construction, one choice at a time, over the
9//! bounded universe in `crate::{REFS, OIDS, KEYS}` plus the shadow
10//! [`Kind`](crate::Kind) annotation, and its six [`Property::always`]
11//! obligations restate — independently, in hand-written Rust, not by
12//! calling `gate` a second time — exactly the five doc invariants the
13//! seven rules claim to cover, plus the refname-binding claim they do
14//! not. A property's *discovery* is a transaction `gate` admits that
15//! violates the corresponding independent check.
16//!
17//! # The bound, and why it stays this small
18//!
19//! A state is exactly five choices, made in a fixed order: refname,
20//! transaction [`Shape`], [`Signer`], [`Retention`], and the new tip's
21//! [`Kind`]. That is `4 x 4 x 3 x 4 x 3 = 576` leaf states — small enough
22//! for [`Model::checker`] to explore exhaustively in well under a
23//! second. A naive "add any single EDB atom from the domain" search (a
24//! literal transcription of Alloy's relational style) was tried first
25//! and rejected: with `parent`/`signed_by`/`anchor`/`context`/
26//! `object_exists` each ranging freely over `OIDS x OIDS` or `OIDS x
27//! KEYS`, the reachable state count is the size of the powerset of every
28//! possible atom, not the five-transaction-shapes count above — tens of
29//! thousands of atoms' worth of subsets, intractable for exhaustive BFS.
30//! [`Shape`] instead enumerates the four transaction shapes
31//! `ents_gate_rules`' own unit tests already hand-build (creation,
32//! fast-forward advance, non-fast-forward, and the second-root merge),
33//! which is everything the seven rules' *logic* actually branches on;
34//! membership is fixed background ([`crate::enroll_all`]) rather than a
35//! search dimension, since membership *lifecycle* is Phase 3's concern
36//! (`receive.rs`), not Phase 0.5's.
37
38use ents_gate_rules::{Facts, gate};
39use stateright::{Model, Property};
40
41use crate::{ADMIN_KEY, Kind, MEMBER_KEY_1, REFS, enroll_all};
42
43/// The shape of the proposed transaction — the one dimension along which
44/// the seven denial rules' *logic* actually branches, standing in for
45/// the full `parent`/`ref_update` relations' combinatorics.
46#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
47pub enum Shape {
48 /// `ref_update(r, None, new)` with `new` parentless: entity creation.
49 Genesis,
50 /// `ref_update(r, Some(old), new)` with `new` a descendant of `old`
51 /// via one intermediate commit — the admitted case.
52 FastForward,
53 /// `ref_update(r, Some(old), new)` with `new` unrelated to `old` —
54 /// `ff_violation`'s witness.
55 NonFf,
56 /// `ref_update(r, Some(old), new)` with `new` a merge of the
57 /// fast-forward chain and an unrelated parentless commit —
58 /// `second_root_violation`'s witness
59 /// (`ents_gate_rules::tests::merged_in_second_root_is_rejected`).
60 SecondRoot,
61}
62
63/// All four transaction shapes, in a fixed enumeration order.
64pub const SHAPES: [Shape; 4] = [
65 Shape::Genesis,
66 Shape::FastForward,
67 Shape::NonFf,
68 Shape::SecondRoot,
69];
70
71/// Who signs every commit the transaction introduces — one signer
72/// applies uniformly to keep the state small; per-commit signer
73/// variation is Phase 3's concern, not this search's.
74#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
75pub enum Signer {
76 /// Every introduced commit signed by [`ADMIN_KEY`].
77 Admin,
78 /// Every introduced commit signed by [`MEMBER_KEY_1`].
79 Member,
80 /// No introduced commit carries a signature.
81 Unsigned,
82}
83
84/// All three signer choices, in a fixed enumeration order.
85pub const SIGNERS: [Signer; 3] = [Signer::Admin, Signer::Member, Signer::Unsigned];
86
87/// Whether the new tip carries anchor/context retention, and whether it
88/// resolves — only meaningful for [`Shape::Genesis`] (a comment-shaped
89/// creation); every other shape treats this as absent.
90#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
91pub enum Retention {
92 /// No anchor or context blob.
93 Absent,
94 /// Anchor and context present, both resolving.
95 Resolving,
96 /// Anchor and context present; the anchored blob does not resolve.
97 DanglingAnchor,
98 /// Anchor and context present; the context blob does not resolve.
99 DanglingContext,
100}
101
102/// All four retention choices, in a fixed enumeration order.
103pub const RETENTIONS: [Retention; 4] = [
104 Retention::Absent,
105 Retention::Resolving,
106 Retention::DanglingAnchor,
107 Retention::DanglingContext,
108];
109
110/// All three [`Kind`] choices, in a fixed enumeration order.
111pub const KINDS: [Kind; 3] = [Kind::Comment, Kind::Issue, Kind::Effect];
112
113/// A transaction under construction: five independent choices, each
114/// `None` until [`SearchModel::actions`] offers it. A state with every
115/// field `Some` is complete; [`SearchModel::actions`] then offers
116/// nothing further, so the search terminates at exactly 576 leaves.
117#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)]
118pub struct State {
119 ref_name: Option<&'static str>,
120 shape: Option<Shape>,
121 signer: Option<Signer>,
122 retention: Option<Retention>,
123 kind: Option<Kind>,
124}
125
126/// One choice, made against exactly one of [`State`]'s five `None`
127/// fields, in the fixed order the field declarations above list.
128#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
129pub enum Action {
130 /// Choose the transaction's refname.
131 ChooseRef(&'static str),
132 /// Choose the transaction's [`Shape`].
133 ChooseShape(Shape),
134 /// Choose the transaction's [`Signer`].
135 ChooseSigner(Signer),
136 /// Choose the new tip's [`Retention`].
137 ChooseRetention(Retention),
138 /// Choose the new tip's signed-content [`Kind`].
139 ChooseKind(Kind),
140}
141
142/// A fully-chosen transaction, built once all five [`State`] fields are
143/// `Some` — the point at which the properties below have anything to
144/// check.
145pub struct Complete {
146 ref_name: &'static str,
147 shape: Shape,
148 signer: Signer,
149 retention: Retention,
150 kind: Kind,
151}
152
153impl State {
154 /// `Some` once every field is chosen, `None` while the transaction
155 /// is still under construction — the properties below treat `None`
156 /// as vacuously satisfying every obligation, so no discovery is
157 /// reported before there is a whole transaction to judge.
158 fn complete(&self) -> Option<Complete> {
159 Some(Complete {
160 ref_name: self.ref_name?,
161 shape: self.shape?,
162 signer: self.signer?,
163 retention: self.retention?,
164 kind: self.kind?,
165 })
166 }
167}
168
169impl Complete {
170 /// Translate this transaction into `ents_gate_rules::Facts`, exactly
171 /// as a real extractor would for each shape — same commit oids and
172 /// structure the crate's own unit tests build by hand.
173 fn to_facts(&self) -> Facts {
174 let mut f = Facts::default();
175 enroll_all(&mut f);
176
177 let signed_key = match self.signer {
178 Signer::Admin => Some(ADMIN_KEY),
179 Signer::Member => Some(MEMBER_KEY_1),
180 Signer::Unsigned => None,
181 };
182 let sign = |f: &mut Facts, oid: &str| {
183 if let Some(k) = signed_key {
184 f.signed_by.push((oid.to_string(), k.to_string()));
185 }
186 };
187
188 match self.shape {
189 Shape::Genesis => {
190 f.ref_update = vec![(self.ref_name.to_string(), None, "g2".to_string())];
191 sign(&mut f, "g2");
192 match self.retention {
193 Retention::Absent => {}
194 Retention::Resolving => {
195 f.anchor = vec![("g2".to_string(), "blob-a".to_string())];
196 f.context = vec![("g2".to_string(), "blob-ctx".to_string())];
197 f.object_exists = vec![("blob-a".to_string(),), ("blob-ctx".to_string(),)];
198 }
199 Retention::DanglingAnchor => {
200 f.anchor = vec![("g2".to_string(), "blob-a".to_string())];
201 f.context = vec![("g2".to_string(), "blob-ctx".to_string())];
202 f.object_exists = vec![("blob-ctx".to_string(),)];
203 }
204 Retention::DanglingContext => {
205 f.anchor = vec![("g2".to_string(), "blob-a".to_string())];
206 f.context = vec![("g2".to_string(), "blob-ctx".to_string())];
207 f.object_exists = vec![("blob-a".to_string(),)];
208 }
209 }
210 }
211 Shape::FastForward => {
212 f.ref_update = vec![(
213 self.ref_name.to_string(),
214 Some("g".to_string()),
215 "c1".to_string(),
216 )];
217 f.parent = vec![("c1".to_string(), "g".to_string())];
218 sign(&mut f, "g");
219 sign(&mut f, "c1");
220 }
221 Shape::NonFf => {
222 f.ref_update = vec![(
223 self.ref_name.to_string(),
224 Some("g".to_string()),
225 "x".to_string(),
226 )];
227 sign(&mut f, "x");
228 }
229 Shape::SecondRoot => {
230 f.ref_update = vec![(
231 self.ref_name.to_string(),
232 Some("g".to_string()),
233 "m".to_string(),
234 )];
235 f.parent = vec![
236 ("c1".to_string(), "g".to_string()),
237 ("m".to_string(), "c1".to_string()),
238 ("m".to_string(), "z".to_string()),
239 ];
240 for oid in ["g", "c1", "m", "z"] {
241 sign(&mut f, oid);
242 }
243 }
244 }
245 f
246 }
247
248 /// `gate(facts).is_empty()` for this transaction — the enabling
249 /// condition every property below is stated as a consequent of.
250 fn admitted(&self) -> bool {
251 gate(self.to_facts()).is_empty()
252 }
253
254 /// abstractions.adoc §4 / gate.adoc: an admitted advance descends
255 /// from its old tip. [`Shape::NonFf`] is the sole shape that
256 /// violates this; every other shape satisfies it by construction.
257 fn ff_holds(&self) -> bool {
258 !matches!(self.shape, Shape::NonFf)
259 }
260
261 /// abstractions.adoc §2 / meta-ref.identity-binding's all-roots
262 /// walk: an admitted advance introduces no second parentless commit.
263 /// [`Shape::SecondRoot`] is the sole shape that violates this.
264 fn single_root_holds(&self) -> bool {
265 !matches!(self.shape, Shape::SecondRoot)
266 }
267
268 /// abstractions.adoc §5 tip invariant, admission half: every commit
269 /// an admitted transaction introduces is signed by an enrolled
270 /// member.
271 fn tip_signed_holds(&self) -> bool {
272 !matches!(self.signer, Signer::Unsigned)
273 }
274
275 /// abstractions.adoc §3 / anchor.retention: an admitted genesis's
276 /// anchor and context both resolve. Only [`Shape::Genesis`] carries
277 /// retention in this model; every other shape is vacuously fine.
278 fn retention_holds(&self) -> bool {
279 if !matches!(self.shape, Shape::Genesis) {
280 return true;
281 }
282 !matches!(
283 self.retention,
284 Retention::DanglingAnchor | Retention::DanglingContext
285 )
286 }
287
288 /// abstractions.adoc §6 / effect.admin-only: an admitted write to
289 /// the effects namespace is admin-signed.
290 fn effect_admin_holds(&self) -> bool {
291 if !self.ref_name.starts_with("refs/meta/effects/") {
292 return true;
293 }
294 matches!(self.signer, Signer::Admin)
295 }
296
297 /// abstractions.adoc §2 / meta-ref.identity-binding: the refname's
298 /// namespace matches the signed content's own declared
299 /// [`Kind`](crate::Kind) — the claim ledger row DIVERGED covers. Only
300 /// engages at [`Shape::Genesis`]: binding is a claim about a fresh
301 /// entity's placement, not about advancing one that already exists.
302 /// [`crate::INBOX_REF`] is deliberately outside this model's binding
303 /// scope (Phase 2 obligation 2's allowed second image, not a fresh
304 /// binding decision), so it always holds trivially here.
305 fn binding_holds(&self) -> bool {
306 if !matches!(self.shape, Shape::Genesis) {
307 return true;
308 }
309 let expected = if self.ref_name.starts_with("refs/meta/effects/") {
310 Kind::Effect
311 } else if self.ref_name.starts_with("refs/meta/comments/") {
312 Kind::Comment
313 } else if self.ref_name.starts_with("refs/meta/issues/") {
314 Kind::Issue
315 } else {
316 return true;
317 };
318 self.kind == expected
319 }
320}
321
322/// The Phase 0.5 search model. Stateless: every choice comes from the
323/// bounded universe in `crate`, not from any field here.
324pub struct SearchModel;
325
326impl Model for SearchModel {
327 type State = State;
328 type Action = Action;
329
330 fn init_states(&self) -> Vec<Self::State> {
331 vec![State::default()]
332 }
333
334 fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>) {
335 if state.ref_name.is_none() {
336 actions.extend(REFS.iter().map(|r| Action::ChooseRef(r)));
337 } else if state.shape.is_none() {
338 actions.extend(SHAPES.iter().map(|s| Action::ChooseShape(*s)));
339 } else if state.signer.is_none() {
340 actions.extend(SIGNERS.iter().map(|s| Action::ChooseSigner(*s)));
341 } else if state.retention.is_none() {
342 actions.extend(RETENTIONS.iter().map(|r| Action::ChooseRetention(*r)));
343 } else if state.kind.is_none() {
344 actions.extend(KINDS.iter().map(|k| Action::ChooseKind(*k)));
345 }
346 // A complete state (every field `Some`) offers nothing further:
347 // this is a leaf, and the search terminates there.
348 }
349
350 fn next_state(&self, last_state: &Self::State, action: Self::Action) -> Option<Self::State> {
351 let mut state = last_state.clone();
352 match action {
353 Action::ChooseRef(r) if state.ref_name.is_none() => state.ref_name = Some(r),
354 Action::ChooseShape(s) if state.ref_name.is_some() && state.shape.is_none() => {
355 state.shape = Some(s)
356 }
357 Action::ChooseSigner(s) if state.shape.is_some() && state.signer.is_none() => {
358 state.signer = Some(s)
359 }
360 Action::ChooseRetention(r) if state.signer.is_some() && state.retention.is_none() => {
361 state.retention = Some(r);
362 }
363 Action::ChooseKind(k) if state.retention.is_some() && state.kind.is_none() => {
364 state.kind = Some(k)
365 }
366 _ => return None,
367 }
368 Some(state)
369 }
370
371 fn properties(&self) -> Vec<Property<Self>> {
372 /// `gate(facts).is_empty()` implies `check(complete)`, vacuously
373 /// true on an incomplete state — one property per doc invariant
374 /// the seven denial rules claim to cover, named to match
375 /// `verify/alloy/gate_rules.als`'s `check` commands one-to-one.
376 fn implication(state: &State, check: fn(&Complete) -> bool) -> bool {
377 state.complete().is_none_or(|c| !c.admitted() || check(&c))
378 }
379
380 vec![
381 Property::always("ff_only_advance", |_, s| implication(s, Complete::ff_holds)),
382 Property::always("single_root_identity", |_, s| {
383 implication(s, Complete::single_root_holds)
384 }),
385 Property::always("introduced_commits_member_signed", |_, s| {
386 implication(s, Complete::tip_signed_holds)
387 }),
388 Property::always("anchor_retention_resolves", |_, s| {
389 implication(s, Complete::retention_holds)
390 }),
391 Property::always("effects_writes_admin_signed", |_, s| {
392 implication(s, Complete::effect_admin_holds)
393 }),
394 // The one property expected to have a discovery: the known,
395 // ledger-recorded DIVERGED gap. See tests::rediscovers_cross_ref_replay_by_search.
396 Property::always("binding_refname_recomputed", |_, s| {
397 implication(s, Complete::binding_holds)
398 }),
399 ]
400 }
401}
402
403#[cfg(test)]
404mod tests {
405 use stateright::Checker;
406
407 use super::*;
408
409 /// The migration's acceptance test: search, not hand-construction,
410 /// rediscovers the cross-ref replay (ledger row DIVERGED,
411 /// `docs/abstractions.adoc` §2). Every other property must have no
412 /// discovery — the seven rules are faithful to the other five doc
413 /// invariants within this bounded universe.
414 #[test]
415 fn rediscovers_cross_ref_replay_by_search() {
416 let checker = SearchModel.checker().spawn_bfs().join();
417
418 let path = checker.assert_any_discovery("binding_refname_recomputed");
419 // Printed so a run's witness can be copied into the PR
420 // description as confirmation the harness has teeth.
421 println!(
422 "binding_refname_recomputed witness: {:?}",
423 path.into_actions()
424 );
425
426 checker.assert_no_discovery("ff_only_advance");
427 checker.assert_no_discovery("single_root_identity");
428 checker.assert_no_discovery("introduced_commits_member_signed");
429 checker.assert_no_discovery("anchor_retention_resolves");
430 checker.assert_no_discovery("effects_writes_admin_signed");
431 }
432}