verify/alloy/gate_rules.als
gate_rules.alshistorycomment on this file
| 1 | // Phase 0.5 — verify the verifier (verify/exercise.md, "Phase 0.5"). |
| 2 | // |
| 3 | // This file is NOT a stub. It translates the seven denial rules of |
| 4 | // crates/kernel/ents-gate-rules/src/lib.rs into Alloy, one predicate per |
| 5 | // rule, same names, and then runs the check the crate cannot run on |
| 6 | // itself: search for transactions with zero violations that break a doc |
| 7 | // invariant (docs/abstractions.adoc; docs/spec/meta-ref.adoc, |
| 8 | // meta-ref.identity-binding; docs/spec/gate.adoc). |
| 9 | // |
| 10 | // The crate is ground truth for the translation: every signature below |
| 11 | // mirrors one EDB relation of ents-gate-rules one-to-one, and every |
| 12 | // denial predicate is a mechanical transcription of the corresponding |
| 13 | // ascent rule. The one extra field, `kind`, models what the *signed |
| 14 | // content* of a commit says it is — the derivation input for refname |
| 15 | // recomputation. It is deliberately absent from the rule vocabulary, |
| 16 | // because that absence is the gap under test. |
| 17 | // |
| 18 | // Expected outcome: every check passes EXCEPT binding_refname_recomputed, |
| 19 | // which must produce the known cross-ref replay counterexample (an |
| 20 | // admin-signed parentless comment commit created at refs/meta/effects/x). |
| 21 | // That failure is the harness working, not the harness broken. It is |
| 22 | // pinned on the code side by crates/kernel/ents-gate-rules/tests/ledger.rs |
| 23 | // and recorded in verify/ledger.adoc (verdict DIVERGED). |
| 24 | |
| 25 | module gate_rules |
| 26 | |
| 27 | // ---- EDB vocabulary, one signature/field per ents-gate-rules relation ---- |
| 28 | |
| 29 | // Oid: an object id. `parent`, `signed_by`, `anchor`, `context` mirror the |
| 30 | // crate's relations parent(Oid, Oid), signed_by(Oid, Key), anchor(Oid, Oid), |
| 31 | // context(Oid, Oid). |
| 32 | sig Oid { |
| 33 | parent: set Oid, |
| 34 | signed_by: set Key, |
| 35 | anchor: set Oid, |
| 36 | context: set Oid, |
| 37 | // NOT part of the crate's vocabulary: the entity kind the signed |
| 38 | // content carries, from which meta-ref.identity-binding says the |
| 39 | // refname recomputes. Modeling it here is what lets Alloy state the |
| 40 | // doc invariant the rules do not check. |
| 41 | kind: lone Kind |
| 42 | } |
| 43 | |
| 44 | // member(Key, Role): a key is enrolled iff `role` is nonempty. |
| 45 | sig Key { role: lone Role } |
| 46 | abstract sig Role {} |
| 47 | one sig Admin, Member extends Role {} |
| 48 | |
| 49 | abstract sig Kind {} |
| 50 | one sig CommentKind, IssueKind, EffectKind extends Kind {} |
| 51 | |
| 52 | // Refnames, abstracted to the one distinction the rules make: |
| 53 | // `r.starts_with("refs/meta/effects/")`. |
| 54 | abstract sig RefName {} |
| 55 | sig EffectsRef, OtherRef extends RefName {} |
| 56 | |
| 57 | // object_exists(Oid): objects the repository already has, or that arrive |
| 58 | // in this pack. |
| 59 | one sig Store { object_exists: set Oid } |
| 60 | |
| 61 | // ref_update(Ref, Option<Oid>, Oid): `no old` is entity creation. |
| 62 | sig RefUpdate { |
| 63 | ref: one RefName, |
| 64 | old: lone Oid, |
| 65 | new: one Oid |
| 66 | } |
| 67 | |
| 68 | // ---- IDB: derived relations, transcribed ---- |
| 69 | |
| 70 | // ancestor: transitive ancestry. |
| 71 | fun ancestors[c: Oid]: set Oid { c.^parent } |
| 72 | |
| 73 | // has_parent(Oid) |
| 74 | pred has_parent[c: Oid] { some c.parent } |
| 75 | |
| 76 | // covered(Ref, Oid): commits already covered by a ref's old tip. |
| 77 | fun covered[u: RefUpdate]: set Oid { u.old + ancestors[u.old] } |
| 78 | |
| 79 | // introduced(Ref, Oid): the new tip and its ancestors, minus everything |
| 80 | // the old tip already reached. |
| 81 | fun introduced[u: RefUpdate]: set Oid { (u.new + ancestors[u.new]) - covered[u] } |
| 82 | |
| 83 | // member_signed(Oid) |
| 84 | pred member_signed[c: Oid] { some k: c.signed_by | some k.role } |
| 85 | |
| 86 | // admin_signed(Oid) |
| 87 | pred admin_signed[c: Oid] { some k: c.signed_by | k.role = Admin } |
| 88 | |
| 89 | // ---- The seven denial rules, same names as the crate ---- |
| 90 | |
| 91 | // Fast-forward-only: the new tip must descend from the old tip. |
| 92 | pred ff_violation[u: RefUpdate] { |
| 93 | some u.old and u.old != u.new and u.old not in ancestors[u.new] |
| 94 | } |
| 95 | |
| 96 | // Creation must point at a parentless genesis commit. |
| 97 | pred genesis_violation[u: RefUpdate] { |
| 98 | no u.old and has_parent[u.new] |
| 99 | } |
| 100 | |
| 101 | // One entity, one root: past genesis, an update may not introduce a |
| 102 | // second parentless commit. |
| 103 | pred second_root_violation[u: RefUpdate] { |
| 104 | some u.old and some c: introduced[u] | not has_parent[c] |
| 105 | } |
| 106 | |
| 107 | // Every introduced commit must carry a signature from a currently |
| 108 | // enrolled member. |
| 109 | pred unsigned_violation[u: RefUpdate] { |
| 110 | some c: introduced[u] | not member_signed[c] |
| 111 | } |
| 112 | |
| 113 | // An anchored blob must resolve to an object the repository will contain. |
| 114 | pred dangling_anchor_violation[u: RefUpdate] { |
| 115 | some c: introduced[u] | some (c.anchor - Store.object_exists) |
| 116 | } |
| 117 | |
| 118 | // The paired context blob must resolve too. |
| 119 | pred dangling_context_violation[u: RefUpdate] { |
| 120 | some c: introduced[u] | some (c.context - Store.object_exists) |
| 121 | } |
| 122 | |
| 123 | // A write to refs/meta/effects/* must be signed by an admin-registered |
| 124 | // member. |
| 125 | pred effect_admin_violation[u: RefUpdate] { |
| 126 | u.ref in EffectsRef and some c: introduced[u] | not admin_signed[c] |
| 127 | } |
| 128 | |
| 129 | // admitted: the crate's `gate(facts).is_empty()` — no denial relation |
| 130 | // holds any row for this update. |
| 131 | pred admitted[u: RefUpdate] { |
| 132 | not ff_violation[u] |
| 133 | not genesis_violation[u] |
| 134 | not second_root_violation[u] |
| 135 | not unsigned_violation[u] |
| 136 | not dangling_anchor_violation[u] |
| 137 | not dangling_context_violation[u] |
| 138 | not effect_admin_violation[u] |
| 139 | } |
| 140 | |
| 141 | // ---- Checks: one per doc invariant the rules claim to cover ---- |
| 142 | |
| 143 | // abstractions §4 / gate: fast-forward-only advance (ff_violation). |
| 144 | assert ff_only_advance { |
| 145 | all u: RefUpdate | (admitted[u] and some u.old and u.old != u.new) |
| 146 | implies u.old in ancestors[u.new] |
| 147 | } |
| 148 | check ff_only_advance for 6 |
| 149 | |
| 150 | // abstractions §2 / meta-ref.identity-binding all-roots walk: an admitted |
| 151 | // update never introduces a second parentless commit |
| 152 | // (genesis_violation + second_root_violation). |
| 153 | assert single_root_identity { |
| 154 | all u: RefUpdate | (admitted[u] and some u.old) |
| 155 | implies (no c: introduced[u] | not has_parent[c]) |
| 156 | } |
| 157 | check single_root_identity for 6 |
| 158 | |
| 159 | // abstractions §5 tip invariant, admission half: every commit an admitted |
| 160 | // transaction introduces is member-signed (unsigned_violation). |
| 161 | assert introduced_commits_member_signed { |
| 162 | all u: RefUpdate | admitted[u] |
| 163 | implies (all c: introduced[u] | member_signed[c]) |
| 164 | } |
| 165 | check introduced_commits_member_signed for 6 |
| 166 | |
| 167 | // abstractions §3 / anchor.retention: both embedded objects of every |
| 168 | // introduced anchor resolve (dangling_anchor_violation + |
| 169 | // dangling_context_violation). |
| 170 | assert anchor_retention_resolves { |
| 171 | all u: RefUpdate | admitted[u] |
| 172 | implies (all c: introduced[u] | (c.anchor + c.context) in Store.object_exists) |
| 173 | } |
| 174 | check anchor_retention_resolves for 6 |
| 175 | |
| 176 | // abstractions §6 / effect.admin-only: an admitted write to |
| 177 | // refs/meta/effects/* is admin-signed (effect_admin_violation). |
| 178 | assert effects_writes_admin_signed { |
| 179 | all u: RefUpdate | (admitted[u] and u.ref in EffectsRef) |
| 180 | implies (all c: introduced[u] | admin_signed[c]) |
| 181 | } |
| 182 | check effects_writes_admin_signed for 6 |
| 183 | |
| 184 | // abstractions §4 / meta-ref.identity-binding: "the refname is a total |
| 185 | // function of signed content, recomputed at verification." No rule in |
| 186 | // ents-gate-rules covers this, and no gap marker declares the omission. |
| 187 | // EXPECTED TO FAIL with the cross-ref replay counterexample: an |
| 188 | // admin-signed parentless commit whose signed content is a comment |
| 189 | // (kind = CommentKind, anchor + context present and resolving), replayed |
| 190 | // as the creation of an effects ref — genesis, unsigned, and effect_admin |
| 191 | // are all satisfied, ff vacuously. Ledger row: DIVERGED. |
| 192 | assert binding_refname_recomputed { |
| 193 | all u: RefUpdate | (admitted[u] and no u.old and u.ref in EffectsRef) |
| 194 | implies u.new.kind = EffectKind |
| 195 | } |
| 196 | check binding_refname_recomputed for 6 |