git-ents.gitmain
⌘K
foforge

crates/kernel/ents-gate-rules/tests/prop.rs

prop.rs120 lines · 4.8 KB · rusthistorycomment on this file
1//! Property-based floor for the ledger's invariant claims
2//! (`verify/ledger.adoc`): `proptest` samples `Facts` over a small
3//! bounded domain — deliberately duplicated here from
4//! `crates/verify/ents-verify`'s vocabulary rather than depending on
5//! that crate, since the sink-layer rule in
6//! `crates/cli/git-ents/tests/layering.rs` is one-way: nothing may
7//! depend on `ents-verify`.
8//!
9//! Two properties below have no exemption — the rules that cover them
10//! (`unsigned_violation`, `effect_admin_violation`) are believed sound.
11//! The third carries the one *known* exemption in this crate: the
12//! refname-binding gap (`verify/ledger.adoc`, DIVERGED row;
13//! `docs/abstractions.adoc` §2). A naive "admitted implies bound
14//! correctly" property would fail on every run while that gap is open;
15//! the exemption proves it is load-bearing, not dead code, and per
16//! `tests/ledger.rs`'s convention, gets deleted in the same commit that
17//! adds `binding_violation`.
18
19use ents_gate_rules::{Facts, Role, gate};
20use proptest::prelude::*;
21
22/// The signed content's own declared kind — the same shadow annotation
23/// `ents-verify`'s search model and `verify/alloy/gate_rules.als`'s
24/// `kind` field use, kept outside `Facts` because its absence from the
25/// crate's real vocabulary *is* the gap under test.
26#[derive(Clone, Copy, Debug, PartialEq, Eq)]
27enum Kind {
28 Comment,
29 Issue,
30 Effect,
31}
32
33const ADMIN_KEY: &str = "key:admin";
34const MEMBER_KEY: &str = "key:m1";
35
36const ISSUE_REF: &str = "refs/meta/issues/g";
37const COMMENT_REF: &str = "refs/meta/comments/g2";
38const EFFECT_REF: &str = "refs/meta/effects/x";
39
40fn refs() -> impl Strategy<Value = &'static str> {
41 prop_oneof![Just(ISSUE_REF), Just(COMMENT_REF), Just(EFFECT_REF)]
42}
43
44fn signers() -> impl Strategy<Value = Option<&'static str>> {
45 prop_oneof![Just(Some(ADMIN_KEY)), Just(Some(MEMBER_KEY)), Just(None)]
46}
47
48fn kinds() -> impl Strategy<Value = Kind> {
49 prop_oneof![Just(Kind::Comment), Just(Kind::Issue), Just(Kind::Effect)]
50}
51
52/// Build a genesis transaction — the only shape the binding gap
53/// concerns, since binding is a claim about a fresh entity's placement
54/// — from sampled atoms, alongside whether the doc's binding invariant
55/// actually holds for this sample.
56fn build(ref_name: &str, signer: Option<&str>, kind: Kind) -> (Facts, bool) {
57 let mut facts = Facts {
58 member: vec![
59 (ADMIN_KEY.to_string(), Role::Admin),
60 (MEMBER_KEY.to_string(), Role::Member),
61 ],
62 ..Facts::default()
63 };
64 facts.ref_update = vec![(ref_name.to_string(), None, "g2".to_string())];
65 if let Some(key) = signer {
66 facts.signed_by = vec![("g2".to_string(), key.to_string())];
67 }
68
69 let binding_holds = match kind {
70 Kind::Effect => ref_name.starts_with("refs/meta/effects/"),
71 Kind::Comment => ref_name.starts_with("refs/meta/comments/"),
72 Kind::Issue => ref_name.starts_with("refs/meta/issues/"),
73 };
74 (facts, binding_holds)
75}
76
77proptest! {
78 /// Ledger floor (abstractions.adoc §5 tip invariant, admission
79 /// half): an admitted genesis is signed by an enrolled member. No
80 /// exemption — `unsigned_violation` covers this today.
81 #[test]
82 fn admitted_genesis_is_signed(r in refs(), signer in signers(), kind in kinds()) {
83 let (facts, _binding_holds) = build(r, signer, kind);
84 if gate(facts).is_empty() {
85 prop_assert!(signer.is_some());
86 }
87 }
88
89 /// Ledger floor (abstractions.adoc §6 / effect.admin-only): an
90 /// admitted write to `refs/meta/effects/*` is admin-signed. No
91 /// exemption — `effect_admin_violation` covers this today.
92 #[test]
93 fn admitted_effects_write_is_admin_signed(signer in signers(), kind in kinds()) {
94 let (facts, _binding_holds) = build(EFFECT_REF, signer, kind);
95 if gate(facts).is_empty() {
96 prop_assert_eq!(signer, Some(ADMIN_KEY));
97 }
98 }
99
100 /// Ledger row (DIVERGED, `docs/abstractions.adoc` §2 /
101 /// `meta-ref.identity-binding`): an admitted genesis's refname
102 /// namespace should match its signed content's declared kind.
103 /// EXEMPTED while the gap is open — delete the early return (and
104 /// this comment) in the same commit that adds `binding_violation`,
105 /// per `tests/ledger.rs`'s gap-pinning convention.
106 #[test]
107 fn admitted_genesis_binds_its_namespace(r in refs(), signer in signers(), kind in kinds()) {
108 let (facts, binding_holds) = build(r, signer, kind);
109 if gate(facts.clone()).is_empty() && !binding_holds {
110 // KNOWN GAP (verify/ledger.adoc: DIVERGED). Keeping this
111 // branch, rather than deleting the property outright, is
112 // what proves the exemption is load-bearing: comment it out
113 // locally and this property fails immediately.
114 return Ok(());
115 }
116 if gate(facts).is_empty() {
117 prop_assert!(binding_holds);
118 }
119 }
120}