git-ents.gitmain
⌘K
foforge

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

lib.rs131 lines · 6.0 KB · rusthistorycomment on this file
1//! Rust-native model checking for the formal stocktake (`verify/`,
2//! `verify/exercise.md`): [`stateright`] models that call
3//! [`ents_gate_rules::gate`] directly, so the refinement mapping between
4//! model and code is the function call, not a hand-maintained
5//! translation.
6//!
7//! This crate is a sink in the workspace's layering (`docs/abstractions.
8//! adoc`'s "Layering" section, extended by `crates/cli/git-ents/tests/
9//! layering.rs`): it depends on [`ents_gate_rules`] and nothing else in
10//! the workspace, and nothing in the workspace may depend on it. It
11//! exists to be run by `cargo test -p ents-verify`, never linked into a
12//! shipped binary.
13//!
14//! # Modules
15//!
16//! - [`search`] — the Phase 0.5 replacement: an exhaustive search over a
17//! small bounded universe of transactions, checking that every
18//! admitted transaction (`gate(facts).is_empty()`) also satisfies the
19//! doc invariants the rules are supposed to encode. This is where the
20//! cross-ref replay counterexample (ledger row: DIVERGED,
21//! `docs/abstractions.adoc` §2) is rediscovered by search rather than
22//! asserted by hand.
23//! - [`receive`] — Phase 3 skeleton: state/action signatures for the
24//! gate-and-receive protocol, with the gate-check action's enabling
25//! condition wired to the real `gate()` call (the one deliberate
26//! exception to "skeleton, not solution").
27//! - [`effects`] — Phase 4 skeleton: trigger/dedup/results state shape.
28//! - [`durability`] — Phase 5 skeleton: crash/durability ordering.
29//!
30//! # The bounded universe
31//!
32//! Every model in this crate builds transactions from the same tiny,
33//! fixed set of atoms — the Rust-native analogue of Alloy's scope
34//! discipline (`verify/exercise.md`: "Alloy scopes of 4-6 atoms per
35//! signature. Almost every bug in a system like this appears with two
36//! members, two refs, three commits."). Keeping every model's universe
37//! this small is what makes exhaustive search (Phase 0.5) and bounded
38//! model checking (Phases 3-5) tractable at all.
39
40pub mod durability;
41pub mod effects;
42pub mod receive;
43pub mod search;
44
45use ents_gate_rules::{Facts, Role};
46
47/// The one admin-registered key in the bounded universe — the only
48/// signer [`effect_admin_violation`](ents_gate_rules) and the
49/// redaction-admin-only rule (`docs/spec/receive.adoc`
50/// `receive.redaction-admin-only`) accept for their namespaces.
51pub const ADMIN_KEY: &str = "key:admin";
52/// An ordinary enrolled, non-admin member key.
53pub const MEMBER_KEY_1: &str = "key:m1";
54/// A second ordinary member key — the bounded universe's "two members"
55/// atom, needed for adoption/divergence scenarios where a single key
56/// isn't enough to tell two actors apart.
57pub const MEMBER_KEY_2: &str = "key:m2";
58
59/// Every key in the bounded universe, admin first.
60pub const KEYS: [&str; 3] = [ADMIN_KEY, MEMBER_KEY_1, MEMBER_KEY_2];
61
62/// The fixed role a key in the bounded universe carries. Roles are not
63/// an independent search dimension here: enrolling a key is a single
64/// fact (present or absent), never a choice of role, exactly so search
65/// states can dedupe on plain sets instead of tracking role assignment
66/// as extra state — [`ents_gate_rules::Role`] itself has no `Ord`, which
67/// would otherwise complicate that dedup.
68#[must_use]
69pub fn role_of(key: &str) -> Role {
70 if key == ADMIN_KEY {
71 Role::Admin
72 } else {
73 Role::Member
74 }
75}
76
77/// A hash-identified namespace (`docs/spec/meta-ref.adoc`
78/// `meta-ref.identity-binding`) — genesis-oid binding, the shape
79/// `issues/*` and `comments/*` share.
80pub const ISSUE_REF: &str = "refs/meta/issues/g";
81/// The other hash-identified namespace in the bounded universe, kept
82/// distinct from [`ISSUE_REF`] so a model can distinguish "which
83/// hash-identified namespace" without adding a third dimension.
84pub const COMMENT_REF: &str = "refs/meta/comments/g2";
85/// The admin-only namespace (`effect.admin-only`) — the one the crate's
86/// `effect_admin_violation` rule protects, and the namespace the known
87/// cross-ref replay counterexample targets.
88pub const EFFECT_REF: &str = "refs/meta/effects/x";
89/// The one namespace `meta-ref.inbox` declares as an allowed *second*
90/// image of an already-bound signed commit — Phase 2 obligation 2.
91pub const INBOX_REF: &str = "refs/meta/inbox/m1/comments/g2";
92
93/// Every refname in the bounded universe.
94pub const REFS: [&str; 4] = [ISSUE_REF, COMMENT_REF, EFFECT_REF, INBOX_REF];
95
96/// Object ids in the bounded universe: enough to build a genesis
97/// (`g2`), a fast-forward advance of an existing tip (`g` -> `c1`), and
98/// a two-parent merge that smuggles in an unrelated root (`z`) — the
99/// three transaction shapes `ents_gate_rules`' own unit tests already
100/// exercise by hand, plus two blobs for anchor/context retention.
101pub const OIDS: [&str; 6] = ["g", "c1", "m", "z", "blob-a", "blob-ctx"];
102
103/// The signed content's own kind, as the *author's* signed content
104/// declares it — the derivation input `docs/abstractions.adoc` §2 says
105/// the refname recomputes from. Deliberately absent from
106/// [`ents_gate_rules::Facts`] itself: that absence is the gap under
107/// test. Every model that checks the binding invariant carries this as a
108/// shadow annotation alongside a built [`Facts`] value, never inside it,
109/// exactly mirroring `verify/alloy/gate_rules.als`'s `kind` field.
110#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
111pub enum Kind {
112 /// The signed content is a comment (`docs/spec/model.adoc`
113 /// `model.comment`).
114 Comment,
115 /// The signed content is an issue (`model.issue`).
116 Issue,
117 /// The signed content is an effect definition (`model.effect-
118 /// definition`, `effect.admin-only`).
119 Effect,
120}
121
122/// Enroll every key in [`KEYS`] into `facts.member`, at its fixed
123/// [`role_of`]. Every model in this crate treats membership as
124/// background, not a search dimension — Phase 3's `receive` skeleton is
125/// where membership *lifecycle* (enrollment, revocation) belongs.
126pub fn enroll_all(facts: &mut Facts) {
127 facts.member = KEYS
128 .iter()
129 .map(|k| ((*k).to_string(), role_of(k)))
130 .collect();
131}