verify/alloy/objects.als
objects.alshistorycomment on this file
| 1 | // Phase 1 — the object-graph substrate (verify/exercise.md, "Phase 1"). |
| 2 | // |
| 3 | // STUB. This file is scaffolding for a paper-first exercise: it parses, |
| 4 | // it declares the vocabulary, and it names the obligations — it checks |
| 5 | // NOTHING. Every predicate below is deliberately empty (trivially true) |
| 6 | // until a human writes the model longhand and transcribes it here. |
| 7 | // |
| 8 | // Discharges, once filled in: docs/abstractions.adoc §2 (typed tree, |
| 9 | // schema pinning), §3 (anchor retention, redaction); docs/spec/anchor.adoc |
| 10 | // anchor.retention; the schema-pinning string-OID/gitlink negatives. |
| 11 | // |
| 12 | // Vocabulary: the signatures mirror the EDB relations of |
| 13 | // crates/kernel/ents-gate-rules/src/lib.rs one-to-one (ref_update, parent, |
| 14 | // signed_by, member, anchor, context, object_exists), so a claim proved |
| 15 | // here composes with gate_rules.als without renaming. Phase 1 will refine |
| 16 | // Oid into Blob + Tree + Commit with tree entries; that refinement is the |
| 17 | // human's first move, not the harness's. |
| 18 | |
| 19 | module objects |
| 20 | |
| 21 | // ---- EDB vocabulary, one signature/field per ents-gate-rules relation ---- |
| 22 | |
| 23 | sig Oid { |
| 24 | parent: set Oid, // parent(child, parent) |
| 25 | signed_by: set Key, // signed_by(commit, key) |
| 26 | anchor: set Oid, // anchor(entity commit, anchored blob) |
| 27 | context: set Oid // context(entity commit, context blob) |
| 28 | } |
| 29 | |
| 30 | sig Key { role: lone Role } // member(Key, Role) |
| 31 | abstract sig Role {} |
| 32 | one sig Admin, Member extends Role {} |
| 33 | |
| 34 | abstract sig RefName {} |
| 35 | sig EffectsRef, OtherRef extends RefName {} |
| 36 | |
| 37 | one sig Store { object_exists: set Oid } // object_exists(Oid) |
| 38 | |
| 39 | sig RefUpdate { // ref_update(Ref, Option<Oid>, Oid) |
| 40 | ref: one RefName, |
| 41 | old: lone Oid, |
| 42 | new: one Oid |
| 43 | } |
| 44 | |
| 45 | // ---- Obligation stubs: named, empty, trivially true. Not checked. ---- |
| 46 | |
| 47 | // Obligation 1: entity tree embeds schema as a real entry => schema in |
| 48 | // reach[entityTip]. STUB — checks nothing. |
| 49 | pred schema_pinning { |
| 50 | // TODO(exercise) |
| 51 | } |
| 52 | |
| 53 | // Obligation 1, negative: the string-OID variant does NOT retain the |
| 54 | // schema (reachability fails). STUB — checks nothing. |
| 55 | pred schema_pinning_string_oid_fails { |
| 56 | // TODO(exercise) |
| 57 | } |
| 58 | |
| 59 | // Obligation 1, negative: the gitlink variant does NOT retain the schema. |
| 60 | // STUB — checks nothing. |
| 61 | pred schema_pinning_gitlink_fails { |
| 62 | // TODO(exercise) |
| 63 | } |
| 64 | |
| 65 | // Obligation 2: embedded anchored blob + context blob reachable from the |
| 66 | // meta-ref (anchor.retention). STUB — checks nothing. |
| 67 | pred anchor_retention { |
| 68 | // TODO(exercise) |
| 69 | } |
| 70 | |
| 71 | // Obligation 2, degraded trace: anchored commit gc'd, anchor still |
| 72 | // projects from its embedded objects. STUB — checks nothing. |
| 73 | pred anchor_degraded_projection { |
| 74 | // TODO(exercise) |
| 75 | } |
| 76 | |
| 77 | // Obligation 3: redaction as object withholding — can withholding one |
| 78 | // entity's blob break another entity's closure via dedup sharing? |
| 79 | // CONDITIONAL candidate. STUB — checks nothing. |
| 80 | pred redaction_vs_retention { |
| 81 | // TODO(exercise) |
| 82 | } |
| 83 | |
| 84 | // Parse-only smoke command so `check-alloy` has something to execute; |
| 85 | // it asserts nothing about the system. |
| 86 | run { some Oid } for 3 |