crates/kernel/ents-gate-rules/tests/ledger.rs
ledger.rshistorycomment on this file
| 1 | //! Counterexample tests for `verify/ledger.adoc` — the formal-stocktake |
| 2 | //! verdict ledger's landing strip in code. |
| 3 | //! |
| 4 | //! Convention (see `verify/README.adoc`): a ledger row found FALSIFIED or |
| 5 | //! DIVERGED with a concrete, transaction-shaped counterexample lands here |
| 6 | //! first, expressed in this crate's own [`Facts`] vocabulary. While the |
| 7 | //! gap is open, the test is a *gap-pinning* test: it asserts the current |
| 8 | //! (wrong-per-the-docs) behavior, so the suite stays green and the gap |
| 9 | //! stays visible. When the missing denial rule is added — one rule at a |
| 10 | //! time, red test first, per this crate's own discipline — the pinned |
| 11 | //! assertion is swapped for the inverted one kept alongside it, and the |
| 12 | //! ledger row's verdict is updated. |
| 13 | //! |
| 14 | //! Where the counterexample is transaction-shaped like this one, the |
| 15 | //! same landing happens in two more places, all three updated together: |
| 16 | //! `tests/prop.rs`'s matching property loses its exemption branch (it |
| 17 | //! currently proves the exemption load-bearing by failing without it), |
| 18 | //! and `crates/verify/ents-verify/src/search.rs`'s matching |
| 19 | //! [`stateright::Property::always`] — which today has a discovery — is |
| 20 | //! expected to have none once the rule lands. |
| 21 | |
| 22 | use ents_gate_rules::{Facts, Role, gate}; |
| 23 | |
| 24 | /// Cross-ref replay through the missing refname-binding rule. |
| 25 | /// |
| 26 | /// Ledger row: `docs/abstractions.adoc` §4 / `docs/spec/meta-ref.adoc` |
| 27 | /// `meta-ref.identity-binding` — "the refname is a total function of |
| 28 | /// signed content, recomputed at verification". Verdict: DIVERGED (the |
| 29 | /// doc claims it; no rule checks it; no gap marker declares the |
| 30 | /// omission). Missing rule: `binding_violation`. Alloy witness: |
| 31 | /// `verify/alloy/gate_rules.als`, check `binding_refname_recomputed`. |
| 32 | /// |
| 33 | /// The transaction: an admin-signed, parentless commit whose signed |
| 34 | /// content is a *comment* (anchor + context blobs present and resolving), |
| 35 | /// replayed as the creation of `refs/meta/effects/x`. Every current rule |
| 36 | /// is satisfied: `genesis` (parentless), `unsigned` (member-signed), |
| 37 | /// `effect_admin` (admin-signed), `ff` (vacuous — creation), the root and |
| 38 | /// anchor rules likewise. Nothing recomputes the refname from the signed |
| 39 | /// content, so the comment is admitted as an effect definition. |
| 40 | /// |
| 41 | /// This test PINS the open gap: it asserts the replay is admitted today. |
| 42 | /// Fixing it is out of scope for the stocktake scaffolding. When |
| 43 | /// `binding_violation` lands, this assertion flips — swap it for the |
| 44 | /// commented one below. |
| 45 | #[test] |
| 46 | fn cross_ref_replay_of_comment_as_effect_is_admitted_today() { |
| 47 | let mut facts = Facts { |
| 48 | member: vec![("key:admin".into(), Role::Admin)], |
| 49 | ..Facts::default() |
| 50 | }; |
| 51 | // A comment-shaped genesis: parentless, admin-signed, embedding its |
| 52 | // anchored blob and context blob — but pushed as the creation of an |
| 53 | // effects ref, a namespace its signed content does not derive. |
| 54 | facts.ref_update = vec![("refs/meta/effects/x".into(), None, "g2".into())]; |
| 55 | facts.signed_by = vec![("g2".into(), "key:admin".into())]; |
| 56 | facts.anchor = vec![("g2".into(), "blob:a".into())]; |
| 57 | facts.context = vec![("g2".into(), "blob:ctx".into())]; |
| 58 | facts.object_exists = vec![("blob:a".into(),), ("blob:ctx".into(),)]; |
| 59 | |
| 60 | let verdicts = gate(facts); |
| 61 | |
| 62 | // Pinned current behavior: admitted. This is the gap, kept green on |
| 63 | // purpose so CI never normalizes ignoring it. |
| 64 | assert!( |
| 65 | verdicts.is_empty(), |
| 66 | "the binding gap appears to have closed: a rule now denies the \ |
| 67 | cross-ref replay ({verdicts:?}) — flip this test to the inverted \ |
| 68 | assertion below and update verify/ledger.adoc" |
| 69 | ); |
| 70 | |
| 71 | // Ready to swap in when `binding_violation` exists: |
| 72 | // assert!( |
| 73 | // verdicts.iter().any(|v| v.starts_with("binding:")), |
| 74 | // "binding_violation must deny the cross-ref replay: {verdicts:?}" |
| 75 | // ); |
| 76 | } |