verify/alloy/binding.als
binding.alshistorycomment on this file
| 1 | // Phase 2 — refname binding as a total function (verify/exercise.md, |
| 2 | // "Phase 2"). |
| 3 | // |
| 4 | // STUB. This file parses, declares the vocabulary, and names one |
| 5 | // derivation predicate per meta-ref namespace — it checks NOTHING. Every |
| 6 | // predicate body is deliberately empty (trivially true) until the human |
| 7 | // exercise writes each derivation from the code, not from memory. |
| 8 | // |
| 9 | // Discharges, once filled in: docs/abstractions.adoc §4 ("the refname is |
| 10 | // a total function of signed content, recomputed at verification"); |
| 11 | // docs/spec/meta-ref.adoc meta-ref.identity-binding and meta-ref.inbox. |
| 12 | // The namespace list below is enumerated from meta-ref.adoc's own |
| 13 | // binding taxonomy: fixed-name singletons, natural-key, hash-identified, |
| 14 | // composite-keyed, inbox/self signer-bound, and pins. |
| 15 | // |
| 16 | // Vocabulary: signatures mirror the EDB relations of |
| 17 | // crates/kernel/ents-gate-rules/src/lib.rs one-to-one, so the binding |
| 18 | // model composes with gate_rules.als — the composition is exactly the |
| 19 | // cross-ref replay check (Phase 4, obligation 3). |
| 20 | |
| 21 | module binding |
| 22 | |
| 23 | // ---- EDB vocabulary, one signature/field per ents-gate-rules relation ---- |
| 24 | |
| 25 | sig Oid { |
| 26 | parent: set Oid, // parent(child, parent) |
| 27 | signed_by: set Key, // signed_by(commit, key) |
| 28 | anchor: set Oid, // anchor(entity commit, anchored blob) |
| 29 | context: set Oid // context(entity commit, context blob) |
| 30 | } |
| 31 | |
| 32 | sig Key { role: lone Role } // member(Key, Role) |
| 33 | abstract sig Role {} |
| 34 | one sig Admin, Member extends Role {} |
| 35 | |
| 36 | abstract sig RefName {} |
| 37 | sig EffectsRef, OtherRef extends RefName {} |
| 38 | |
| 39 | one sig Store { object_exists: set Oid } // object_exists(Oid) |
| 40 | |
| 41 | sig RefUpdate { // ref_update(Ref, Option<Oid>, Oid) |
| 42 | ref: one RefName, |
| 43 | old: lone Oid, |
| 44 | new: one Oid |
| 45 | } |
| 46 | |
| 47 | // The binding function under study: refname derived from signed content. |
| 48 | // The exercise fills in its definition per namespace; here it is a free |
| 49 | // relation so the file parses. |
| 50 | sig Binding { binds: Oid -> lone RefName } |
| 51 | |
| 52 | // ---- Per-namespace derivation stubs (meta-ref.identity-binding) ---- |
| 53 | // Each states, once written, how that namespace's refname derives from |
| 54 | // signed content. All STUBS — they check nothing. |
| 55 | |
| 56 | // refs/meta/account — fixed name (singleton state). |
| 57 | pred binding_account { |
| 58 | // TODO(exercise) |
| 59 | } |
| 60 | |
| 61 | // refs/meta/config — fixed name (singleton state). |
| 62 | pred binding_config { |
| 63 | // TODO(exercise) |
| 64 | } |
| 65 | |
| 66 | // refs/meta/member/* — natural key: designated tree field equals the |
| 67 | // refname's final segment. |
| 68 | pred binding_member { |
| 69 | // TODO(exercise) |
| 70 | } |
| 71 | |
| 72 | // refs/meta/effects/* — natural key: the effect's name. |
| 73 | pred binding_effects { |
| 74 | // TODO(exercise) |
| 75 | } |
| 76 | |
| 77 | // refs/meta/issues/* — hash-identified: final segment equals the genesis |
| 78 | // commit oid; all parentless commits reachable from the tip are that |
| 79 | // genesis. |
| 80 | pred binding_issues { |
| 81 | // TODO(exercise) |
| 82 | } |
| 83 | |
| 84 | // refs/meta/comments/* — hash-identified, same rule as issues. |
| 85 | pred binding_comments { |
| 86 | // TODO(exercise) |
| 87 | } |
| 88 | |
| 89 | // refs/meta/reviews/<target>/<member> — composite-keyed: genesis tree's |
| 90 | // target field + genesis signer's member id. |
| 91 | pred binding_reviews { |
| 92 | // TODO(exercise) |
| 93 | } |
| 94 | |
| 95 | // refs/meta/results/<effect>/<short-oid> — composite-keyed: derived from |
| 96 | // the result's own tree fields. |
| 97 | pred binding_results { |
| 98 | // TODO(exercise) |
| 99 | } |
| 100 | |
| 101 | // refs/meta/inbox/<member>/<canonical-suffix> — owner segment equals the |
| 102 | // signer; suffix bound as its canonical namespace binds. |
| 103 | pred binding_inbox { |
| 104 | // TODO(exercise) |
| 105 | } |
| 106 | |
| 107 | // refs/meta/self/<member>/<effect>/<short-oid> — member segment equals |
| 108 | // the signer, mirroring the canonical results pattern. |
| 109 | pred binding_self { |
| 110 | // TODO(exercise) |
| 111 | } |
| 112 | |
| 113 | // refs/meta/pins/* — mirrors its entity's segments; parentless-roots walk |
| 114 | // deliberately not applied. |
| 115 | pred binding_pins { |
| 116 | // TODO(exercise) |
| 117 | } |
| 118 | |
| 119 | // ---- Phase 2 obligation stubs ---- |
| 120 | |
| 121 | // Obligation 1 aggregate: the binding is a TOTAL function over every |
| 122 | // namespace above. STUB — checks nothing. |
| 123 | pred binding_total_function { |
| 124 | // TODO(exercise) |
| 125 | } |
| 126 | |
| 127 | // Obligation 2: inbox is the one allowed second image of the same signed |
| 128 | // commit; nothing else is. STUB — checks nothing. |
| 129 | pred inbox_allowed_second_image { |
| 130 | // TODO(exercise) |
| 131 | } |
| 132 | |
| 133 | // Obligation 3: self/<member> derives from the SIGNATURE, not a tree |
| 134 | // field an author could forge. STUB — checks nothing. |
| 135 | pred self_member_from_signature { |
| 136 | // TODO(exercise) |
| 137 | } |
| 138 | |
| 139 | // Obligation 4: is repo identity anywhere in signed content? Cross-repo |
| 140 | // replay. CONDITIONAL either way — write the condition. STUB — checks |
| 141 | // nothing. |
| 142 | pred cross_repo_replay { |
| 143 | // TODO(exercise) |
| 144 | } |
| 145 | |
| 146 | // Parse-only smoke command so `check-alloy` has something to execute; |
| 147 | // it asserts nothing about the system. |
| 148 | run { some Binding } for 3 |