git ents: verify: scaffold the formal stocktake harness

commit cba33fb

verify: scaffold the formal stocktake harness

verify/ holds the Alloy/TLA+ models and the verdict ledger; stubs match ents-gate-rules' fact vocabulary one-to-one, with the seven denial rules translated as the refinement anchor. ents-gate-rules gains gap-pinning ledger tests (cross-ref replay pinned open). Checkers wired as an optional, skippable CI job. No shipped-crate src changes; no proofs — the exercise is done on paper.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Joseph D. Carpinelli · 1 month ago

tree browse at HEAD · parents: b5b708b · comment on this commit

Reviews

No reviews of this commit yet — record a verdict below.

Start a review

.config/committed.toml @@ -18,6 +18,7 @@ "receive", "roots", "sync", + "verify", "docs", "spec", "checks",

.config/rumdl.toml @@ -7,6 +7,8 @@ "dist", "build", "CHANGELOG.md", + # Copied verbatim from the source exercise; must not be reformatted. + "verify/exercise.md", ] respect-gitignore = true

.config/typos.toml @@ -48,3 +48,5 @@ [default.extend-words] # COSE (CBOR Object Signing and Encryption) — a real WebAuthn term, not a typo cose = "cose" +# als — the Alloy model file extension (verify/alloy/*.als), not "also" +als = "als"

.github/workflows/CI.yml @@ -125,6 +125,35 @@ - name: Run doctests run: cargo test --doc --workspace --all-features + # Formal-model harness (verify/). Best-effort and optional: the check + # scripts warn and exit 0 when the jars are absent, downloads are + # tolerated to fail, and the job is continue-on-error and deliberately + # NOT in the `ci` aggregator's needs — it must never block the + # pipeline or become a required check. Note: gate_rules.als's binding + # check is EXPECTED to report the known cross-ref replay counterexample + # (see verify/ledger.adoc), so a red step here can be the harness + # working as intended. + formal-models: + runs-on: ubuntu-latest + if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'push' || (github.event_name == 'pull_request' && github.event.pull_request.draft == false) }} + continue-on-error: true + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-java@v4 + with: + distribution: temurin + java-version: '21' + - name: Fetch checker jars (best-effort, never vendored) + run: | + curl -fsSL -o /tmp/tla2tools.jar \ + https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar || true + curl -fsSL -o /tmp/org.alloytools.alloy.dist.jar \ + https://github.com/AlloyTools/org.alloytools.alloy/releases/latest/download/org.alloytools.alloy.dist.jar || true + - name: Check TLA+ models + run: TLA_TOOLS_JAR=/tmp/tla2tools.jar verify/bin/check-tla + - name: Check Alloy models + run: ALLOY_JAR=/tmp/org.alloytools.alloy.dist.jar verify/bin/check-alloy + ci: name: CI if: ${{ always() && (github.event_name == 'workflow_dispatch' || github.event_name == 'push' || (github.event_name == 'pull_request' && github.event.pull_request.draft == false)) }}

crates/kernel/ents-gate-rules/tests/ledger.rs @@ -1,0 +1,68 @@ +//! Counterexample tests for `verify/ledger.adoc` — the formal-stocktake +//! verdict ledger's landing strip in code. +//! +//! Convention (see `verify/README.adoc`): a ledger row found FALSIFIED or +//! DIVERGED with a concrete, transaction-shaped counterexample lands here +//! first, expressed in this crate's own [`Facts`] vocabulary. While the +//! gap is open, the test is a *gap-pinning* test: it asserts the current +//! (wrong-per-the-docs) behavior, so the suite stays green and the gap +//! stays visible. When the missing denial rule is added — one rule at a +//! time, red test first, per this crate's own discipline — the pinned +//! assertion is swapped for the inverted one kept alongside it, and the +//! ledger row's verdict is updated. + +use ents_gate_rules::{Facts, Role, gate}; + +/// Cross-ref replay through the missing refname-binding rule. +/// +/// Ledger row: `docs/abstractions.adoc` §4 / `docs/spec/meta-ref.adoc` +/// `meta-ref.identity-binding` — "the refname is a total function of +/// signed content, recomputed at verification". Verdict: DIVERGED (the +/// doc claims it; no rule checks it; no gap marker declares the +/// omission). Missing rule: `binding_violation`. Alloy witness: +/// `verify/alloy/gate_rules.als`, check `binding_refname_recomputed`. +/// +/// The transaction: an admin-signed, parentless commit whose signed +/// content is a *comment* (anchor + context blobs present and resolving), +/// replayed as the creation of `refs/meta/effects/x`. Every current rule +/// is satisfied: `genesis` (parentless), `unsigned` (member-signed), +/// `effect_admin` (admin-signed), `ff` (vacuous — creation), the root and +/// anchor rules likewise. Nothing recomputes the refname from the signed +/// content, so the comment is admitted as an effect definition. +/// +/// This test PINS the open gap: it asserts the replay is admitted today. +/// Fixing it is out of scope for the stocktake scaffolding. When +/// `binding_violation` lands, this assertion flips — swap it for the +/// commented one below. +#[test] +fn cross_ref_replay_of_comment_as_effect_is_admitted_today() { + let mut facts = Facts { + member: vec![("key:admin".into(), Role::Admin)], + ..Facts::default() + }; + // A comment-shaped genesis: parentless, admin-signed, embedding its + // anchored blob and context blob — but pushed as the creation of an + // effects ref, a namespace its signed content does not derive. + facts.ref_update = vec![("refs/meta/effects/x".into(), None, "g2".into())]; + facts.signed_by = vec![("g2".into(), "key:admin".into())]; + facts.anchor = vec![("g2".into(), "blob:a".into())]; + facts.context = vec![("g2".into(), "blob:ctx".into())]; + facts.object_exists = vec![("blob:a".into(),), ("blob:ctx".into(),)]; + + let verdicts = gate(facts); + + // Pinned current behavior: admitted. This is the gap, kept green on + // purpose so CI never normalizes ignoring it. + assert!( + verdicts.is_empty(), + "the binding gap appears to have closed: a rule now denies the \ + cross-ref replay ({verdicts:?}) — flip this test to the inverted \ + assertion below and update verify/ledger.adoc" + ); + + // Ready to swap in when `binding_violation` exists: + // assert!( + // verdicts.iter().any(|v| v.starts_with("binding:")), + // "binding_violation must deny the cross-ref replay: {verdicts:?}" + // ); +}

verify/README.adoc @@ -1,0 +1,48 @@ += verify: the formal stocktake harness + +This directory holds the scaffolding for the formal stocktaking exercise described in `exercise.md` (copied verbatim; it is the source of truth for phases, obligations, and verdict rules). +It is documentation-and-tooling only: nothing here is a crate, nothing here appears in any `Cargo.toml`, and nothing here touches refs, trailers, tree layouts, or any string that ends up in a Git object. +The exercise itself is done by a human, on paper first; these files are the harness, not the proofs. + +== What lives here + +`ledger.adoc`:: +The verdict ledger — the exercise's one deliverable. +One row per invariant claim extracted from `docs/abstractions.adoc` and `docs/spec/*.adoc`, with verdicts filled in as the exercise progresses. + +`alloy/`:: +Alloy 6 models for the structural claims. +`objects.als` (Phase 1) and `binding.als` (Phase 2) are deliberately empty stubs that parse but check nothing. +`gate_rules.als` (Phase 0.5) is the exception: it translates the seven denial rules of `crates/kernel/ents-gate-rules` faithfully and its binding check is expected to produce the known cross-ref replay counterexample. + +`tla/`:: +TLA+ skeletons for the protocol claims: `Receive.tla` (Phase 3), `Effects.tla` (Phase 4), `Durability.tla` (Phase 5), each with a small TLC `.cfg`. +Variables and action signatures only; `Receive.tla`'s `GateAdmits` transcribes the seven rules as the gate's enabling condition. + +`bin/`:: +`check-alloy` and `check-tla`, best-effort wrappers that run every model headless when a checker jar is available and warn-and-skip when it is not. + +== The epistemic split + +Three tools, three jobs, deliberately not interchangeable. +The Datalog in `ents-gate-rules` *evaluates* the admission rules over one supplied transaction's facts; it is executable and type-checked, but it cannot search for the transaction you didn't think of. +Alloy *searches* for counterexamples: small-scope model finding over the same vocabulary, looking for admitted transactions that break a doc invariant. +TLA+ checks the *protocol over time*: receive/CAS races, adoption, epochs, effect dispatch, durability ordering — claims about traces, not single transactions. + +== The refinement anchor + +Models are checked against `ents-gate-rules`, not the other way around. +Every signature and variable here mirrors the crate's EDB relations one-to-one (`ref_update`, `parent`, `signed_by`, `member`, `anchor`, `context`, `object_exists`), and the seven denial rules are transcribed under their crate names, so a finding in a model is expressible as a `Facts` test in the crate. +That is also the landing convention: a FALSIFIED or DIVERGED ledger row with a concrete counterexample becomes a test in `crates/kernel/ents-gate-rules/tests/ledger.rs` first (gap-pinning while open), then a denial rule, one rule at a time. + +== Running the checkers + +[source,shell] +---- +verify/bin/check-alloy # every .als, headless; needs ALLOY_JAR or a well-known path +verify/bin/check-tla # SANY-parse every .tla, TLC-run every .cfg; needs TLA_TOOLS_JAR +---- + +Both scripts exit 0 with a warning when no jar or no Java runtime is found, so they never block anything; CI runs them in an optional, non-required job. +Do not vendor the jars into the repo. +When `check-alloy` reports a counterexample for `binding_refname_recomputed` in `gate_rules.als`, that is the documented open gap, not a harness failure — see the DIVERGED row in `ledger.adoc`.

verify/alloy/binding.als @@ -1,0 +1,148 @@ +// Phase 2 — refname binding as a total function (verify/exercise.md, +// "Phase 2"). +// +// STUB. This file parses, declares the vocabulary, and names one +// derivation predicate per meta-ref namespace — it checks NOTHING. Every +// predicate body is deliberately empty (trivially true) until the human +// exercise writes each derivation from the code, not from memory. +// +// Discharges, once filled in: docs/abstractions.adoc §4 ("the refname is +// a total function of signed content, recomputed at verification"); +// docs/spec/meta-ref.adoc meta-ref.identity-binding and meta-ref.inbox. +// The namespace list below is enumerated from meta-ref.adoc's own +// binding taxonomy: fixed-name singletons, natural-key, hash-identified, +// composite-keyed, inbox/self signer-bound, and pins. +// +// Vocabulary: signatures mirror the EDB relations of +// crates/kernel/ents-gate-rules/src/lib.rs one-to-one, so the binding +// model composes with gate_rules.als — the composition is exactly the +// cross-ref replay check (Phase 4, obligation 3). + +module binding + +// ---- EDB vocabulary, one signature/field per ents-gate-rules relation ---- + +sig Oid { + parent: set Oid, // parent(child, parent) + signed_by: set Key, // signed_by(commit, key) + anchor: set Oid, // anchor(entity commit, anchored blob) + context: set Oid // context(entity commit, context blob) +} + +sig Key { role: lone Role } // member(Key, Role) +abstract sig Role {} +one sig Admin, Member extends Role {} + +abstract sig RefName {} +sig EffectsRef, OtherRef extends RefName {} + +one sig Store { object_exists: set Oid } // object_exists(Oid) + +sig RefUpdate { // ref_update(Ref, Option<Oid>, Oid) + ref: one RefName, + old: lone Oid, + new: one Oid +} + +// The binding function under study: refname derived from signed content. +// The exercise fills in its definition per namespace; here it is a free +// relation so the file parses. +sig Binding { binds: Oid -> lone RefName } + +// ---- Per-namespace derivation stubs (meta-ref.identity-binding) ---- +// Each states, once written, how that namespace's refname derives from +// signed content. All STUBS — they check nothing. + +// refs/meta/account — fixed name (singleton state). +pred binding_account { + // TODO(exercise) +} + +// refs/meta/config — fixed name (singleton state). +pred binding_config { + // TODO(exercise) +} + +// refs/meta/member/* — natural key: designated tree field equals the +// refname's final segment. +pred binding_member { + // TODO(exercise) +} + +// refs/meta/effects/* — natural key: the effect's name. +pred binding_effects { + // TODO(exercise) +} + +// refs/meta/issues/* — hash-identified: final segment equals the genesis +// commit oid; all parentless commits reachable from the tip are that +// genesis. +pred binding_issues { + // TODO(exercise) +} + +// refs/meta/comments/* — hash-identified, same rule as issues. +pred binding_comments { + // TODO(exercise) +} + +// refs/meta/reviews/<target>/<member> — composite-keyed: genesis tree's +// target field + genesis signer's member id. +pred binding_reviews { + // TODO(exercise) +} + +// refs/meta/results/<effect>/<short-oid> — composite-keyed: derived from +// the result's own tree fields. +pred binding_results { + // TODO(exercise) +} + +// refs/meta/inbox/<member>/<canonical-suffix> — owner segment equals the +// signer; suffix bound as its canonical namespace binds. +pred binding_inbox { + // TODO(exercise) +} + +// refs/meta/self/<member>/<effect>/<short-oid> — member segment equals +// the signer, mirroring the canonical results pattern. +pred binding_self { + // TODO(exercise) +} + +// refs/meta/pins/* — mirrors its entity's segments; parentless-roots walk +// deliberately not applied. +pred binding_pins { + // TODO(exercise) +} + +// ---- Phase 2 obligation stubs ---- + +// Obligation 1 aggregate: the binding is a TOTAL function over every +// namespace above. STUB — checks nothing. +pred binding_total_function { + // TODO(exercise) +} + +// Obligation 2: inbox is the one allowed second image of the same signed +// commit; nothing else is. STUB — checks nothing. +pred inbox_allowed_second_image { + // TODO(exercise) +} + +// Obligation 3: self/<member> derives from the SIGNATURE, not a tree +// field an author could forge. STUB — checks nothing. +pred self_member_from_signature { + // TODO(exercise) +} + +// Obligation 4: is repo identity anywhere in signed content? Cross-repo +// replay. CONDITIONAL either way — write the condition. STUB — checks +// nothing. +pred cross_repo_replay { + // TODO(exercise) +} + +// Parse-only smoke command so `check-alloy` has something to execute; +// it asserts nothing about the system. +run { some Binding } for 3

verify/alloy/gate_rules.als @@ -1,0 +1,196 @@ +// Phase 0.5 — verify the verifier (verify/exercise.md, "Phase 0.5"). +// +// This file is NOT a stub. It translates the seven denial rules of +// crates/kernel/ents-gate-rules/src/lib.rs into Alloy, one predicate per +// rule, same names, and then runs the check the crate cannot run on +// itself: search for transactions with zero violations that break a doc +// invariant (docs/abstractions.adoc; docs/spec/meta-ref.adoc, +// meta-ref.identity-binding; docs/spec/gate.adoc). +// +// The crate is ground truth for the translation: every signature below +// mirrors one EDB relation of ents-gate-rules one-to-one, and every +// denial predicate is a mechanical transcription of the corresponding +// ascent rule. The one extra field, `kind`, models what the *signed +// content* of a commit says it is — the derivation input for refname +// recomputation. It is deliberately absent from the rule vocabulary, +// because that absence is the gap under test. +// +// Expected outcome: every check passes EXCEPT binding_refname_recomputed, +// which must produce the known cross-ref replay counterexample (an +// admin-signed parentless comment commit created at refs/meta/effects/x). +// That failure is the harness working, not the harness broken. It is +// pinned on the code side by crates/kernel/ents-gate-rules/tests/ledger.rs +// and recorded in verify/ledger.adoc (verdict DIVERGED). + +module gate_rules + +// ---- EDB vocabulary, one signature/field per ents-gate-rules relation ---- + +// Oid: an object id. `parent`, `signed_by`, `anchor`, `context` mirror the +// crate's relations parent(Oid, Oid), signed_by(Oid, Key), anchor(Oid, Oid), +// context(Oid, Oid). +sig Oid { + parent: set Oid, + signed_by: set Key, + anchor: set Oid, + context: set Oid, + // NOT part of the crate's vocabulary: the entity kind the signed + // content carries, from which meta-ref.identity-binding says the + // refname recomputes. Modeling it here is what lets Alloy state the + // doc invariant the rules do not check. + kind: lone Kind +} + +// member(Key, Role): a key is enrolled iff `role` is nonempty. +sig Key { role: lone Role } +abstract sig Role {} +one sig Admin, Member extends Role {} + +abstract sig Kind {} +one sig CommentKind, IssueKind, EffectKind extends Kind {} + +// Refnames, abstracted to the one distinction the rules make: +// `r.starts_with("refs/meta/effects/")`. +abstract sig RefName {} +sig EffectsRef, OtherRef extends RefName {} + +// object_exists(Oid): objects the repository already has, or that arrive +// in this pack. +one sig Store { object_exists: set Oid } + +// ref_update(Ref, Option<Oid>, Oid): `no old` is entity creation. +sig RefUpdate { + ref: one RefName, + old: lone Oid, + new: one Oid +} + +// ---- IDB: derived relations, transcribed ---- + +// ancestor: transitive ancestry. +fun ancestors[c: Oid]: set Oid { c.^parent } + +// has_parent(Oid) +pred has_parent[c: Oid] { some c.parent } + +// covered(Ref, Oid): commits already covered by a ref's old tip. +fun covered[u: RefUpdate]: set Oid { u.old + ancestors[u.old] } + +// introduced(Ref, Oid): the new tip and its ancestors, minus everything +// the old tip already reached. +fun introduced[u: RefUpdate]: set Oid { (u.new + ancestors[u.new]) - covered[u] } + +// member_signed(Oid) +pred member_signed[c: Oid] { some k: c.signed_by | some k.role } + +// admin_signed(Oid) +pred admin_signed[c: Oid] { some k: c.signed_by | k.role = Admin } + +// ---- The seven denial rules, same names as the crate ---- + +// Fast-forward-only: the new tip must descend from the old tip. +pred ff_violation[u: RefUpdate] { + some u.old and u.old != u.new and u.old not in ancestors[u.new] +} + +// Creation must point at a parentless genesis commit. +pred genesis_violation[u: RefUpdate] { + no u.old and has_parent[u.new] +} + +// One entity, one root: past genesis, an update may not introduce a +// second parentless commit. +pred second_root_violation[u: RefUpdate] { + some u.old and some c: introduced[u] | not has_parent[c] +} + +// Every introduced commit must carry a signature from a currently +// enrolled member. +pred unsigned_violation[u: RefUpdate] { + some c: introduced[u] | not member_signed[c] +} + +// An anchored blob must resolve to an object the repository will contain. +pred dangling_anchor_violation[u: RefUpdate] { + some c: introduced[u] | some (c.anchor - Store.object_exists) +} + +// The paired context blob must resolve too. +pred dangling_context_violation[u: RefUpdate] { + some c: introduced[u] | some (c.context - Store.object_exists) +} + +// A write to refs/meta/effects/* must be signed by an admin-registered +// member. +pred effect_admin_violation[u: RefUpdate] { + u.ref in EffectsRef and some c: introduced[u] | not admin_signed[c] +} + +// admitted: the crate's `gate(facts).is_empty()` — no denial relation +// holds any row for this update. +pred admitted[u: RefUpdate] { + not ff_violation[u] + not genesis_violation[u] + not second_root_violation[u] + not unsigned_violation[u] + not dangling_anchor_violation[u] + not dangling_context_violation[u] + not effect_admin_violation[u] +} + +// ---- Checks: one per doc invariant the rules claim to cover ---- + +// abstractions §4 / gate: fast-forward-only advance (ff_violation). +assert ff_only_advance { + all u: RefUpdate | (admitted[u] and some u.old and u.old != u.new) + implies u.old in ancestors[u.new] +} +check ff_only_advance for 6 + +// abstractions §2 / meta-ref.identity-binding all-roots walk: an admitted +// update never introduces a second parentless commit +// (genesis_violation + second_root_violation). +assert single_root_identity { + all u: RefUpdate | (admitted[u] and some u.old) + implies (no c: introduced[u] | not has_parent[c]) +} +check single_root_identity for 6 + +// abstractions §5 tip invariant, admission half: every commit an admitted +// transaction introduces is member-signed (unsigned_violation). +assert introduced_commits_member_signed { + all u: RefUpdate | admitted[u] + implies (all c: introduced[u] | member_signed[c]) +} +check introduced_commits_member_signed for 6 + +// abstractions §3 / anchor.retention: both embedded objects of every +// introduced anchor resolve (dangling_anchor_violation + +// dangling_context_violation). +assert anchor_retention_resolves { + all u: RefUpdate | admitted[u] + implies (all c: introduced[u] | (c.anchor + c.context) in Store.object_exists) +} +check anchor_retention_resolves for 6 + +// abstractions §6 / effect.admin-only: an admitted write to +// refs/meta/effects/* is admin-signed (effect_admin_violation). +assert effects_writes_admin_signed { + all u: RefUpdate | (admitted[u] and u.ref in EffectsRef) + implies (all c: introduced[u] | admin_signed[c]) +} +check effects_writes_admin_signed for 6 + +// abstractions §4 / meta-ref.identity-binding: "the refname is a total +// function of signed content, recomputed at verification." No rule in +// ents-gate-rules covers this, and no gap marker declares the omission. +// EXPECTED TO FAIL with the cross-ref replay counterexample: an +// admin-signed parentless commit whose signed content is a comment +// (kind = CommentKind, anchor + context present and resolving), replayed +// as the creation of an effects ref — genesis, unsigned, and effect_admin +// are all satisfied, ff vacuously. Ledger row: DIVERGED. +assert binding_refname_recomputed { + all u: RefUpdate | (admitted[u] and no u.old and u.ref in EffectsRef) + implies u.new.kind = EffectKind +} +check binding_refname_recomputed for 6

verify/alloy/objects.als @@ -1,0 +1,86 @@ +// Phase 1 — the object-graph substrate (verify/exercise.md, "Phase 1"). +// +// STUB. This file is scaffolding for a paper-first exercise: it parses, +// it declares the vocabulary, and it names the obligations — it checks +// NOTHING. Every predicate below is deliberately empty (trivially true) +// until a human writes the model longhand and transcribes it here. +// +// Discharges, once filled in: docs/abstractions.adoc §2 (typed tree, +// schema pinning), §3 (anchor retention, redaction); docs/spec/anchor.adoc +// anchor.retention; the schema-pinning string-OID/gitlink negatives. +// +// Vocabulary: the signatures mirror the EDB relations of +// crates/kernel/ents-gate-rules/src/lib.rs one-to-one (ref_update, parent, +// signed_by, member, anchor, context, object_exists), so a claim proved +// here composes with gate_rules.als without renaming. Phase 1 will refine +// Oid into Blob + Tree + Commit with tree entries; that refinement is the +// human's first move, not the harness's. + +module objects + +// ---- EDB vocabulary, one signature/field per ents-gate-rules relation ---- + +sig Oid { + parent: set Oid, // parent(child, parent) + signed_by: set Key, // signed_by(commit, key) + anchor: set Oid, // anchor(entity commit, anchored blob) + context: set Oid // context(entity commit, context blob) +} + +sig Key { role: lone Role } // member(Key, Role) +abstract sig Role {} +one sig Admin, Member extends Role {} + +abstract sig RefName {} +sig EffectsRef, OtherRef extends RefName {} + +one sig Store { object_exists: set Oid } // object_exists(Oid) + +sig RefUpdate { // ref_update(Ref, Option<Oid>, Oid) + ref: one RefName, + old: lone Oid, + new: one Oid +} + +// ---- Obligation stubs: named, empty, trivially true. Not checked. ---- + +// Obligation 1: entity tree embeds schema as a real entry => schema in +// reach[entityTip]. STUB — checks nothing. +pred schema_pinning { + // TODO(exercise) +} + +// Obligation 1, negative: the string-OID variant does NOT retain the +// schema (reachability fails). STUB — checks nothing. +pred schema_pinning_string_oid_fails { + // TODO(exercise) +} + +// Obligation 1, negative: the gitlink variant does NOT retain the schema. +// STUB — checks nothing. +pred schema_pinning_gitlink_fails { + // TODO(exercise) +} + +// Obligation 2: embedded anchored blob + context blob reachable from the +// meta-ref (anchor.retention). STUB — checks nothing. +pred anchor_retention { + // TODO(exercise) +} + +// Obligation 2, degraded trace: anchored commit gc'd, anchor still +// projects from its embedded objects. STUB — checks nothing. +pred anchor_degraded_projection { + // TODO(exercise) +} + +// Obligation 3: redaction as object withholding — can withholding one +// entity's blob break another entity's closure via dedup sharing? +// CONDITIONAL candidate. STUB — checks nothing. +pred redaction_vs_retention { + // TODO(exercise) +} + +// Parse-only smoke command so `check-alloy` has something to execute; +// it asserts nothing about the system. +run { some Oid } for 3

verify/bin/check-alloy @@ -1,0 +1,60 @@ +#!/bin/sh +# Run every Alloy model in verify/alloy/ headless. Best-effort and +# optional: if no Alloy jar (or no java) is available this script warns +# and exits 0 so it never blocks a pipeline. +# +# Jar discovery: $ALLOY_JAR, then a few well-known paths. Do NOT vendor +# the jar into the repo. +# +# Expected today: gate_rules.als's binding_refname_recomputed check FAILS +# with the cross-ref replay counterexample. That is the harness working — +# see verify/ledger.adoc (DIVERGED row) and +# crates/kernel/ents-gate-rules/tests/ledger.rs. +set -u + +dir=$(CDPATH= cd -- "$(dirname -- "$0")/.." && pwd) + +warn_skip() { + echo "check-alloy: $1" >&2 + echo "check-alloy: skipping (this is a warning, not a failure)." >&2 + echo "check-alloy: install: download org.alloytools.alloy.dist.jar from" >&2 + echo " https://github.com/AlloyTools/org.alloytools.alloy/releases" >&2 + echo " and set ALLOY_JAR=/path/to/org.alloytools.alloy.dist.jar" >&2 + exit 0 +} + +jar="${ALLOY_JAR:-}" +if [ -z "$jar" ]; then + for candidate in \ + "$HOME/.local/share/alloy/org.alloytools.alloy.dist.jar" \ + /usr/local/share/alloy/org.alloytools.alloy.dist.jar \ + /opt/homebrew/share/alloy/org.alloytools.alloy.dist.jar \ + /usr/share/java/org.alloytools.alloy.dist.jar; do + if [ -f "$candidate" ]; then + jar=$candidate + break + fi + done +fi +[ -n "$jar" ] && [ -f "$jar" ] || warn_skip "no Alloy jar found (ALLOY_JAR unset, no well-known path hit)" +command -v java >/dev/null 2>&1 || warn_skip "no java runtime on PATH" + +# `exec` writes per-command solution files; send them to a scratch dir so +# they never litter the working tree, and clean up on exit. +out=$(mktemp -d "${TMPDIR:-/tmp}/check-alloy.XXXXXX") +trap 'rm -rf "$out"' EXIT + +status=0 +for als in "$dir"/alloy/*.als; do + echo "== check-alloy: $als" + # The Alloy 6 dist jar ships a CLI; `exec` runs every command in the + # file headless. A found counterexample for a `check` is reported in + # the output — read it against the expectations in the file headers. + # A `check` that finds a counterexample is still a successful run + # (exit 0), so only a parse error or a jar failure fails this script. + if ! java -jar "$jar" exec -f -o "$out/$(basename "$als")" "$als"; then + echo "check-alloy: $als: non-zero exit (parse error or jar failure — see above)" >&2 + status=1 + fi +done +exit "$status"

verify/bin/check-tla @@ -1,0 +1,56 @@ +#!/bin/sh +# Parse every TLA+ module in verify/tla/ with SANY, then model-check each +# module that has a .cfg with TLC. Best-effort and optional: if no +# tla2tools jar (or no java) is available this script warns and exits 0 +# so it never blocks a pipeline. +# +# Jar discovery: $TLA_TOOLS_JAR, then a few well-known paths. Do NOT +# vendor the jar into the repo. +set -u + +dir=$(CDPATH= cd -- "$(dirname -- "$0")/.." && pwd) + +warn_skip() { + echo "check-tla: $1" >&2 + echo "check-tla: skipping (this is a warning, not a failure)." >&2 + echo "check-tla: install: download tla2tools.jar from" >&2 + echo " https://github.com/tlaplus/tlaplus/releases" >&2 + echo " and set TLA_TOOLS_JAR=/path/to/tla2tools.jar" >&2 + exit 0 +} + +jar="${TLA_TOOLS_JAR:-}" +if [ -z "$jar" ]; then + for candidate in \ + "$HOME/.local/share/tlaplus/tla2tools.jar" \ + /usr/local/share/tlaplus/tla2tools.jar \ + /opt/homebrew/share/tlaplus/tla2tools.jar \ + /usr/share/java/tla2tools.jar; do + if [ -f "$candidate" ]; then + jar=$candidate + break + fi + done +fi +[ -n "$jar" ] && [ -f "$jar" ] || warn_skip "no tla2tools jar found (TLA_TOOLS_JAR unset, no well-known path hit)" +command -v java >/dev/null 2>&1 || warn_skip "no java runtime on PATH" + +status=0 +cd "$dir/tla" || exit 1 +for tla in *.tla; do + echo "== check-tla: SANY $tla" + if ! java -cp "$jar" tla2sany.SANY "$tla"; then + echo "check-tla: $tla: SANY parse failure" >&2 + status=1 + continue + fi + cfg="${tla%.tla}.cfg" + if [ -f "$cfg" ]; then + echo "== check-tla: TLC $tla ($cfg)" + if ! java -cp "$jar" tlc2.TLC -config "$cfg" -deadlock "$tla"; then + echo "check-tla: $tla: TLC failure" >&2 + status=1 + fi + fi +done +exit "$status"

verify/exercise.md @@ -1,0 +1,266 @@ +# Stocktaking git-ents by formal verification + +A paper exercise. The repo's own claim — `docs/abstractions.adoc` opens with +"the load-bearing abstractions, stated as invariants" — is taken literally: +every invariant becomes a formal obligation, the code becomes the +implementation you check the model against, and the output is a verdict +ledger that *is* the stocktake. + +Tools: **Alloy 6** for structural/relational claims (object graph, +reachability, refname binding — small-scope model finding excels at +producing the counterexample you didn't think of) and **TLA+** for the +protocol claims (receive/CAS, adoption races, effect dispatch). Paper-first: +write every model longhand before touching a checker; the checker is for +the claims you can't settle by hand. + +The repo now contains its own formalization artifact: +`crates/kernel/ents-gate-rules` states seven admission invariants as +compiled Datalog (ascent). Treat it as a **fourth source** with a specific +epistemic status: it is executable and type-checked, but it *evaluates* +rules over supplied facts — it cannot search for the transaction you +didn't think of, prove inductiveness, or reason about time. Alloy/TLA+ +still own those jobs; the rules crate becomes the refinement anchor the +paper models are checked against. + +Rules of engagement: +- The **doc is the claim source**, the **code is ground truth**, and *you* + (your recent design conversations) are a third, unwritten source. Every + obligation gets a verdict from: PROVED (inductive in the model), + FALSIFIED (counterexample, written out as a concrete Git-object diagram), + CONDITIONAL (holds only under an assumption the doc doesn't state — write + the assumption down; these are the real findings), or DIVERGED (doc, code, + and/or head disagree — cite file and line). +- Scope discipline: Alloy scopes of 4–6 atoms per signature. Almost every + bug in a system like this appears with two members, two refs, three + commits. +- No fixing. This exercise produces the ledger, not patches. + +--- + +## Phase 0 — Adjudicate abstraction 4 (half a day) + +Two write-path models are in play: + +- **Model C (doc, §4):** author-signed commits; refname a total function of + signed content; FF-only + CAS as anti-replay; certs are transport only. +- **Model P (stated in conversation):** `push --signed`; the cert signs + `(refname, old, new)`; certs archived reachably in a server-side op-log. + +Formalize both in Alloy: signatures `Commit`, `Tree`, `Ref`, `Member`, +`Sig`, plus `Cert` in Model P. Define one predicate each system claims: + +> `Auditable`: for every historical tip of every meta-ref, a verifier +> holding only the object closure of `refs/meta/*` (plus, in P, the op-log +> ref) can decide *who* placed it *there*. + +Obligations: +1. Prove or refute `Auditable` in each model. +2. In P, state precisely what the op-log ref's own integrity rests on — + what signs the op-log tip, and is that circular with the gate? +3. In C, check the doc's own caveat: "a commit signature proves authorship; + it does not prove placement" — verify the recovery (refname recomputation) + is *total* (Phase 2 depends on this). +4. Verdict: are C and P equivalent for `Auditable`? If not, which property + separates them — and which one does the repo actually implement? Read + `ents-gate/src/{verify,signature}.rs` and `ents-receive/src/receive.rs` + and cite the lines. Update the ledger with DIVERGED entries as needed. + +Standing evidence: `ents-gate-rules::unsigned_violation` requires every +introduced *commit* to be member-signed, and no `Cert` fact exists in the +schema — the executable rules encode Model C. The doc and the rules agree; +the conversational claim (`push --signed`, certs in the op-log) is the +outlier. Phase 0's burden is therefore: either produce the argument that +overturns two shipped artifacts, or record Model C as canonical and file +the op-log-cert idea as transport forensics only. + +Everything downstream assumes whichever model wins. Do not proceed with +both. + +## Phase 0.5 — Verify the verifier (one day) + +`ents-gate-rules` is small enough to model whole. Translate each EDB +relation into an Alloy signature and each denial rule into a predicate, +then run the check the crate cannot run on itself: **search for +transactions with zero violations that break a doc invariant.** + +Obligations: +1. **Refname binding is missing and unmarked.** The module docs declare + two deliberate gaps (granularity, effect dedup) — but §4's placement + recovery ("refname recomputes from signed content") has no rule and no + gap marker. Confirm the concrete counterexample: an admin-signed + parentless entity commit authored as a comment, replayed as the + creation of `refs/meta/effects/x`, passes `genesis`, `unsigned`, and + `effect_admin` (vacuous FF). Write it as a red test in the crate's own + `Facts` vocabulary. Verdict for §4's binding claim: DIVERGED + (doc claims it, rules don't check it, and per Phase 0 decide whether + `ents-gate` proper does). +2. **Extractor contract = trusted computing base.** Every negated + relation (`!ancestor`, `!covered`, `!member_signed`, `!object_exists`) + is sound only under closed-world completeness of the supplied facts. + The EDB comments say `parent` is "bounded at the old tips." For each + negation, state the completeness assumption and its failure direction: + under-supplied `parent` makes `ff_violation` fail *closed* (spurious + deny — safe), but under-supplied `member`/`signed_by` also denies, while + over-supplied `object_exists` admits dangling anchors — fail *open*. + The table of (relation, assumption, failure direction) is a ledger + deliverable; the fail-open rows are extractor obligations that + currently live nowhere. +3. **Creation admits exactly one commit.** `genesis_violation` denies any + creation whose tip has parents, and `ref_update` cannot express + create-then-advance in one tuple — so an entity with initial history + cannot be pushed atomically. Decide: intended (creation is always a + bare genesis) or gap. If intended, it belongs in §2/§4 as a stated + invariant; it currently isn't. +4. **Merge-commit signatures.** `unsigned_violation` requires *every* + introduced commit signed, which answers Phase 3's sync question in the + strict direction: an unsigned auto-merge from `ents-sync` would be + denied. Check whether sync actually signs its merges; if not, the rules + crate and the sync path are on a collision course — DIVERGED, with the + resolution belonging to Phase 3 obligation 1. + +## Phase 1 — The object-graph substrate (one day) + +Alloy model of just enough Git: `Obj = Blob + Tree + Commit`, `Tree` +entries as a relation `entries: Tree -> Name -> Obj`, `parents: Commit -> +set Commit`, `reach = ^(parents + tree-closure)`. Facts: acyclicity, +content addressing as atom identity (two structurally identical trees are +the same atom — model this deliberately; dedup is load-bearing for schema +pinning). + +Obligations (all from §2, §3, and the schema-pinning decision): +1. **Schema pinning:** entity tree embeds schema as a real entry ⇒ schema + in `reach[entityTip]`. Then the negative: model the *string-OID* and + *gitlink* variants and show reachability fails — the counterexample you + already reasoned about informally becomes a checked fact. +2. **Anchor retention (§3):** embedded blob + context blob reachable from + the meta-ref; anchored *commit* oid recorded as data only ⇒ show a trace + where the anchored commit is gc'd but the anchor still projects + (degraded). Then check the doc's parenthetical: gitlinks retain nothing. +3. **Redaction vs. retention:** §3 calls redaction "the sole deliberate + exception." Model redaction as object withholding and check: can + withholding one entity's blob break *another* entity's closure (shared + blob via dedup)? This is a CONDITIONAL candidate — dedup and redaction + pull in opposite directions. + +## Phase 2 — Refname binding as a total function (one day) + +The doc (§2, §4) claims: "the refname is a total function of signed +content, recomputed at verification." Totality is the whole game — one +entity kind whose refname carries information not in its signed content +reopens cross-ref replay for that kind. + +In Alloy: `binding: Commit -> lone RefName` derived from content atoms. +Enumerate every namespace in `docs/spec/meta-ref.adoc` and +`ents-model/src`: +`member/*, issues/*, comments/*, effects/*, results/*, inbox/*, +self/<member>/*, account, config`. + +Obligations: +1. For each namespace, write the derivation (genesis oid / natural key / + signer composite) from the code, not from memory. Any namespace where + you cannot write it: DIVERGED or FALSIFIED. +2. **Inbox:** an entity sits at `refs/meta/inbox/*` *before* adoption and + at canonical *after*, with the same signed commit in ancestry. The + function is therefore not injective over placement — check that the gate + treats inbox as an allowed second image, and that nothing else is. +3. **`self/<member>`:** the member component derives from the signer — + confirm in code that it derives from the *signature*, not from a tree + field an author could set to someone else. +4. **Cross-repo replay:** is repo identity anywhere in signed content? If + not, a validly signed genesis commit for repo A verifies in repo B. + State whether that is a real threat in your deployment model + (multi-tenant hosted store!) or acceptable. CONDITIONAL either way — + write the condition. + +## Phase 3 — Gate and receive as a protocol (two days) + +TLA+ spec. Variables: `refs` (name → oid), `objects` (set), `members`, +`epoch`; actions: `Propose`, `GateCheck`, `CAS`, `AdoptMerge`, +`SelfMerge`. `GateCheck`'s enabling condition is now concrete: it is +`gate(facts) = {}` — transcribe the seven denial rules from +`ents-gate-rules` verbatim, plus the §5 rules the crate omits (refname +recomputation, epoch). The refinement mapping between this spec and the +crate is Phase 0.5's model reused, which is the point. Model *two* writers +and *one* hosted store minimum; add a local store (advisory gate) as a +second instance with no enforcement. + +Obligations: +1. **Tip invariant is inductive:** "the tip of a meta-ref is signed by a + member authorized for that refname" — prove it's preserved by every + action. Pay attention to `SelfMerge` (two of your machines racing): + *is the merge commit itself signed in the implementation?* Check + `ents-sync/src` and `ents-receive/src/reconcile.rs`. If sync + auto-merges without a signature, the invariant breaks at exactly the + step the doc waves through. +2. **Adoption preserves it:** contributor commit in ancestry, adopter + signature at tip. Then the sharper check: contributor's commit is + itself a merge of unauthorized commits — still fine? (It should be; + prove it, don't assume it.) +3. **Anti-replay:** doc claims parent-hash freshness ⇒ no nonce needed. + Model a replayed genesis (parentless!) — CAS with old = ∅ against an + existing ref fails, but against a *not-yet-created* ref? Combined with + Phase 2 totality this should be safe; the proof forces you to state the + exact conjunction that makes it safe. +4. **Epoch bootstrap (§5):** "the epoch-setting commit is the first gated + tip of the config ref." Model the store from empty: is there a state + where the gate must read the epoch from a ref whose tip is not yet + gated? Either the bootstrap is a real fixpoint or there's an ungated + first write — find which, cite `ents-gate/src/{config,policy}.rs`. +5. **Revocation:** revoked member's key "must never validate again" — but + the tip invariant is checked against member state *when*? At gate time + or by later re-verifiers against *current* member state? A member valid + at admission and revoked later makes historical tips fail naive + re-verification. The epoch mechanism is supposed to answer this — + check that it actually does. + +## Phase 4 — Effects (one day) + +TLA+, building on Phase 3's state. Actions: `RefAdvance`, +`TriggerEval` (commit *enters* the set, §6), `Enqueue` (at-least-once), +`Execute`, `ResultPush` (a gated write like any other). + +Obligations: +1. **Exactly-once observable effect from at-least-once queue:** the dedup + key is `(effect, refname, new_oid)` — prove result-ref idempotency under + duplicate delivery and executor crash-restart. +2. **"Fires once per commit that enters the set":** model a ref deleted + and re-pushed to the same oid. Does the commit *re-enter* the set? + The spec's answer defines whether triggers are monotone; if they aren't, + the cached-query-advanceability argument (FF-only ⇒ results advance) + has a hole. This connects to the op-log deletion-as-data design. +3. **Authorization asymmetry:** effects are admin-writable + (authoring an effect schedules execution); results are written by + executor member keys. Prove no sequence lets a non-admin cause + execution of content they authored *as* an effect (the Phase 2 binding + should close this — compose the two models and check, since this was + the original cross-ref replay scenario). + +## Phase 5 — Durability ordering (half a day, optional) + +TLA+ with crash faults for the hosted deployment: `TigrisWrite`, +`PgCAS`, `Crash` at any point. Prove the invariant "no ref in Postgres +points outside the durable object set," and show the recovery obligation +if the write order were inverted. Small spec, high value — it's the +invariant your whole hosted story rests on. + +## Deliverable + +One ledger table: claim · source (doc §, spec file, code file:line) · +model (Alloy/TLA+) · **encoded in ents-gate-rules?** (rule name / gap +marked / gap unmarked) · verdict · assumption-or-counterexample. Plus the +Phase 0 decision memo — which write-path model is canonical — because +every DIVERGED entry downstream resolves against it. + +Rules found FALSIFIED or gap-unmarked have a natural landing spot the +exercise didn't have before: each becomes a red test plus a new denial +rule in `ents-gate-rules`, in the crate's own one-rule-at-a-time +discipline. Still out of scope for the exercise itself — record them as +ledger rows with a `rule-candidate` note. + +Expected yield, honestly: the first FALSIFIED is already in hand +(cross-ref replay through the missing binding rule, Phase 0.5.1); expect +1–3 more (likeliest: unsigned sync merges colliding with +`unsigned_violation`, inbox binding edge, trigger re-entry), a handful of +CONDITIONAL that become one-line doc amendments or extractor-contract +rows, and one genuine decision (Phase 0) that no amount of model checking +makes for you — though the rules crate has already cast its vote.

verify/ledger.adoc @@ -1,0 +1,177 @@ += verify: the formal-stocktake verdict ledger + +This is the deliverable of the formal-stocktake exercise. +Each row is one invariant claim extracted from `docs/abstractions.adoc` and `docs/spec/*.adoc`, paraphrased faithfully with key phrases quoted. +Every verdict stays `OPEN` until the paper exercise discharges the claim against a formal model. +The code is ground truth: `crates/kernel/ents-gate-rules` is the compiled Datalog rule set, and the `encoded-in-ents-gate-rules?` column classifies each claim against its seven denial rules (`ff_violation`, `genesis_violation`, `second_root_violation`, `unsigned_violation`, `dangling_anchor_violation`, `dangling_context_violation`, `effect_admin_violation`) and its two deliberately-marked gaps (abstraction 1's granularity rule, abstraction 6's monotone exactly-once effect dedup). +A row that turns `FALSIFIED` or `DIVERGED` lands a concrete counterexample as a test in `crates/kernel/ents-gate-rules/tests/ledger.rs` first, before anything else. +The ledger carries 163 rows; exactly one is non-`OPEN` — the refname-binding claim, marked `DIVERGED`. + +[cols="3,3,2,2,1,2", options="header"] +|=== +|claim |source |model |encoded-in-ents-gate-rules? |verdict |assumption-or-counterexample + +|A ref under `refs/meta/*` is simultaneously the unit of storage, sync, authorization, and history. |abstractions.adoc, §1 Meta-ref, ~L14-19 |alloy/objects.als |gap-unmarked |OPEN |— +|Granularity rule: one ref per independently-authored entity; entities different actors write concurrently must not share a ref; writes stay conflict-free. |abstractions.adoc, §1 Meta-ref, ~L21-23 |— |gap-marked |OPEN |— +|Trees stay pure struct representations — no version marker entry. |abstractions.adoc, §2 Typed tree, ~L39 |alloy/objects.als |gap-unmarked |OPEN |— +|"Refname binding needs no stored metadata at all: the refname is a total function of signed content, recomputed at verification." |abstractions.adoc, §2 Typed tree, L42 (normative twin: meta-ref.identity-binding) |alloy/binding.als |gap-unmarked |DIVERGED |Cross-ref replay: an admin-signed parentless comment commit (anchor+context resolving) replayed as creation of refs/meta/effects/x passes genesis, unsigned, effect_admin (ff vacuous). Missing rule: binding_violation. Pinned by crates/kernel/ents-gate-rules/tests/ledger.rs; Alloy witness verify/alloy/gate_rules.als check binding_refname_recomputed. +|Tip invariant: the tip of a meta-ref is always readable by the binary that owns the entity type; non-owning binary degrades to generic display, never an error (redaction is the sole qualification). |abstractions.adoc, §2 Typed tree, ~L44-45 |— |gap-unmarked |OPEN |— +|Retention invariant: the tree storing an anchor embeds the anchored blob plus a context blob; anchored content is reachable from `refs/meta/*` and survives force-push/branch-deletion/gc, with no gc special-casing and no pinned ancestry. |abstractions.adoc, §3 Anchor, ~L51-53 |alloy/objects.als |dangling_anchor_violation, dangling_context_violation |OPEN |— +|Gitlinks are not reachability edges and retain nothing; embedding is the only mechanism that works. |abstractions.adoc, §3 Anchor, L53 |alloy/objects.als |gap-unmarked |OPEN |— +|Redaction is the sole deliberate exception to retention. |abstractions.adoc, §3 Anchor, L54 |alloy/objects.als |gap-unmarked |OPEN |— +|Anchor data is never mutated. |abstractions.adoc, §3 Anchor, L55 |alloy/objects.als |gap-unmarked |OPEN |— +|Anchors project onto newer commits at read time via blame plus fuzzy matching; when the anchored commit is gc'd, projection degrades to context matching instead of breaking. |abstractions.adoc, §3 Anchor, L55-56 |— |gap-unmarked |OPEN |— +|Every meta-ref mutation is an author-signed commit. |abstractions.adoc, §4 Signed commit, L62 |alloy/gate_rules.als |unsigned_violation |OPEN |— +|The signature is a data artifact, not a transport artifact: it replicates with the repo and verifies offline in every clone, so verification evidence is itself repository state. |abstractions.adoc, §4 Signed commit, L63 |alloy/gate_rules.als |gap-unmarked |OPEN |— +|Push certificates are demoted to transport concerns; they carry no meta-ref semantics. |abstractions.adoc, §4 Signed commit, L64 |alloy/gate_rules.als |gap-unmarked |OPEN |— +|Refname binding is recomputed from the commit's own signed content; a mismatch refuses (without this a signed commit could be replayed as the tip of a different meta-ref). |abstractions.adoc, §4 Signed commit, L69 |alloy/binding.als |gap-unmarked |OPEN |— +|Anti-replay: meta-refs advance fast-forward-only (new tip descends from old), enforced by atomic CAS; parent hash is the freshness binding, no nonce needed. |abstractions.adoc, §4 Signed commit, L70 |alloy/gate_rules.als |ff_violation (FF part only; CAS mechanism itself not a Datalog rule) |OPEN |— +|Tip invariant: the tip of a meta-ref is signed by a member authorized for that refname; checkable after the fact by anyone with a clone. |abstractions.adoc, §4 Signed commit, L72-73 |alloy/gate_rules.als |unsigned_violation (partial: enrolled-member only, not refname-specific authorization) |OPEN |— +|Adoption is always a merge, never rewrite: when author and placer differ, the authorized member merges the contributor's commit onto the canonical ref, even trivially; the merge commit satisfies the tip invariant. |abstractions.adoc, §4 Signed commit, L75-76,78 |tla/Receive.tla |gap-unmarked |OPEN |— +|Cherry-picking is forbidden as an adoption mechanism: it creates a new commit object and destroys the author's signature. |abstractions.adoc, §4 Signed commit, L77 |tla/Receive.tla |gap-unmarked |OPEN |— +|Same-actor divergence: two of a member's own machines racing a single-writer ref is resolved by merging own heads, never erroring; typed trees merge schema-aware, not textually. |abstractions.adoc, §4 Signed commit, L80-81 |tla/Receive.tla |gap-unmarked |OPEN |— +|Principled split: content signatures carry authorization only where mutations are author-signed single-writer appends (granularity-guaranteed); `refs/heads/*` keeps transport-level auth instead. |abstractions.adoc, §4 Signed commit, L83-84 |alloy/gate_rules.als |gap-unmarked |OPEN |— +|Gate's four-part verification: tip signed by authorized member; refname recomputes from signed content; new tip descends from old tip; update commits via atomic CAS. |abstractions.adoc, §5 Gate, L92-95 |alloy/gate_rules.als |ff_violation (descent part); rest gap-unmarked |OPEN |— +|Because members/refname rules live under `refs/meta/*`, policy is repository state: any frontend evaluates the actual policy offline, staleness bounded by last fetch. |abstractions.adoc, §5 Gate, L97 |tla/Receive.tla |gap-unmarked |OPEN |— +|Verification epoch: gate applies the tip invariant from an epoch recorded in `refs/meta/config`; history before is archival; epoch-setting commit is the first gated tip of the config ref. |abstractions.adoc, §5 Gate, L99-100 |tla/Receive.tla |gap-unmarked |OPEN |— +|Gate is a property of the store: hosted runs the gate at CAS time and aborts on failure (mandatory); local accepts any write and runs the gate as an annotating verdict (advisory). |abstractions.adoc, §5 Gate, L104-106 |tla/Receive.tla |gap-unmarked |OPEN |— +|The moment a verdict predicts rejection, sync offers to route the commit to the inbox instead — not only after actual rejection. |abstractions.adoc, §5 Gate, L108 |tla/Receive.tla |gap-unmarked |OPEN |— +|One function, three call sites: hosted CAS, local UI verdict, push pre-flight. |abstractions.adoc, §5 Gate, L110 |tla/Receive.tla |gap-unmarked |OPEN |— +|A verdict is never a bare pass/fail: on failure it carries which rule failed and for which refname. |abstractions.adoc, §5 Gate, L111 |— |gap-unmarked |OPEN |— +|Local web UI signs as the user with the user's own member key; server-key signing is a hosted-only necessity, must not be imported locally. |abstractions.adoc, §5 Gate, L114-115 |— |gap-unmarked |OPEN |— +|Results location is derived by convention; an effect cannot choose where its verdicts land. |abstractions.adoc, §6 Effect, L132 |alloy/binding.als |gap-unmarked |OPEN |— +|Trigger semantics: the trigger denotes a set of commits; the effect fires once per commit that enters the set. |abstractions.adoc, §6 Effect, L134 |tla/Effects.tla |gap-marked |OPEN |— +|Meta-refs are outside `rev()`'s domain by definition. |abstractions.adoc, §6 Effect, L138 |tla/Effects.tla |gap-unmarked |OPEN |— +|`meta(glob)` can never match effect-written namespaces (`refs/meta/results/*`, `refs/meta/index/*`); those are reachable only through `results(…)`. |abstractions.adoc, §6 Effect, L140-141 |tla/Effects.tla |gap-unmarked |OPEN |— +|`RefPattern` survives as the degenerate query `rev(<glob>)`; nothing shipped changes meaning. |abstractions.adoc, §6 Effect, L144 |tla/Effects.tla |gap-unmarked |OPEN |— +|Monotone, entry-only: a force-push can shrink a set, but a commit leaving the set retracts nothing — results are immutable history. |abstractions.adoc, §6 Effect, L147 |tla/Effects.tla |gap-marked |OPEN |— +|No pipeline state: the work set is `trigger − results(self, any)` — the results ref is the sole materialization marker. |abstractions.adoc, §6 Effect, L150 |tla/Effects.tla |gap-marked |OPEN |— +|Dedup key `(effect, oid)` over an at-least-once queue yields exactly-once outcomes with zero state outside the repository. |abstractions.adoc, §6 Effect, L151 |tla/Effects.tla |gap-marked |OPEN |— +|Result taxonomy: a result is `pass`, `fail`, or `error`; exit status is always a result. |abstractions.adoc, §6 Effect, L153-154 |tla/Effects.tla |gap-unmarked |OPEN |— +|Infrastructure failure is not a result; only retry exhaustion writes a terminal `error`, signed by the worker's key like any other. |abstractions.adoc, §6 Effect, L155 |tla/Durability.tla |gap-unmarked |OPEN |— +|Retry bounds are deployment configuration, never effect data. |abstractions.adoc, §6 Effect, L156 |alloy/objects.als |gap-unmarked |OPEN |— +|A transient outage can neither retry forever nor permanently discharge an obligation. |abstractions.adoc, §6 Effect, L157 |tla/Durability.tla |gap-unmarked |OPEN |— +|Recursion is structure: downstream-of-effects is syntactically visible; because `rev()`/`meta()` cannot name an effect-written ref, an accidental fork bomb is unreachable by construction. |abstractions.adoc, §6 Effect, L159-160 |tla/Effects.tla |gap-unmarked |OPEN |— +|`post-receive` remains a dumb matcher: ref footprint is statically extractable; set entry computed incrementally from `old..new`, bounded by generation numbers. |abstractions.adoc, §6 Effect, L165-166 |tla/Effects.tla |gap-unmarked |OPEN |— +|Pushes are never blocked; the durable enqueue is the entire synchronous cost. |abstractions.adoc, §6 Effect, L167 |tla/Durability.tla |gap-unmarked |OPEN |— +|A worker dequeues, materializes toolchains, executes in a sandbox; host-direct requires explicit `--unsandboxed`. |abstractions.adoc, §6 Effect, L168-169 |— |gap-unmarked |OPEN |— +|Results return only as signed commits pushed to one ref per tested commit (`refs/meta/results/<effect>/<short-oid>`), so concurrent results never conflict. |abstractions.adoc, §6 Effect, L170 |alloy/binding.als |gap-marked |OPEN |— +|Identity discipline: the runner is a member, not an ambient authority; official results are official only because canonical refs are writable solely by designated worker keys. |abstractions.adoc, §6 Effect, L172-173 |alloy/binding.als |gap-unmarked |OPEN |— +|Any member may self-run any effect; results land in `refs/meta/self/<member>/*` or the inbox, adoptable by merge with the trust decision explicit. |abstractions.adoc, §6 Effect, L174 |alloy/binding.als |gap-unmarked |OPEN |— +|No content predicates beyond `results(…, status)`, no time atoms, no external-event atoms. |abstractions.adoc, §6 Effect, L177 |tla/Effects.tla |gap-unmarked |OPEN |— +|Admin-only write rule on `refs/meta/effects/*` bounds who can schedule execution on canonical infrastructure. |abstractions.adoc, §6 Effect, L181 |alloy/gate_rules.als |effect_admin_violation |OPEN |— +|Abstractions 4/5/6 close: all state changes, human or machine, flow through one verified, audited channel; the repository is the message bus. |abstractions.adoc, "The loop", L188-189 |tla/Receive.tla |gap-unmarked |OPEN |— +|No code knows where it is running; an `if hosted` branch inside the library is the design failing. |abstractions.adoc, "Composition", L196-197 |— |gap-unmarked |OPEN |— +|Crates that extend git carry the `gix-` prefix, import nothing from the forge, and stay upstream-shaped by construction. |abstractions.adoc, "Composition", L209-210 |— |gap-unmarked |OPEN |— +|The unit the library exposes is `receive(refs, objects, events, proposal)`: gate evaluation, effect matching, enqueue live inside it. |abstractions.adoc, "Composition", L213 |tla/Receive.tla |gap-unmarked |OPEN |— +|Local and hosted do not share a push path; they share `receive`, with only trait impls swapped — the correctness anchor for writes. |abstractions.adoc, "Composition", L215-216 |tla/Receive.tla |gap-unmarked |OPEN |— +|Dependencies point one way; a lower layer never depends on a higher one, checked mechanically. |abstractions.adoc, "Layering", L238 |— |gap-unmarked |OPEN |— +|A package depends on kernel crates freely and on other packages never (`ents-forge`/`ents-kiln` never depend on each other). |abstractions.adoc, "Layering", L247 |— |gap-unmarked |OPEN |— +|`ents-web`'s generic rendering path must never match on which concrete entity type it was handed. |abstractions.adoc, "Layering", L252-253 |— |gap-unmarked |OPEN |— +|`ents-web` never depends back on `git-ents`. |abstractions.adoc, "Layering", L254 |— |gap-unmarked |OPEN |— +|A kernel crate must not depend on a package crate in any form (normal, dev, build, or feature-flagged). |abstractions.adoc, "Layering", L256 |— |gap-unmarked |OPEN |— +|`ents-testutil` must not know a package's types. |abstractions.adoc, "Layering", L257 |— |gap-unmarked |OPEN |— +|Every ref namespace is minted by one function in `ents_model::namespace`; a package calls that function rather than inventing its own layout. |abstractions.adoc, "Layering", L259 |alloy/binding.als |gap-unmarked |OPEN |— +|Fanout index: a stale or absent index degrades to scanning ref tips, never to wrong answers. |abstractions.adoc, "Derived", L280 |tla/Effects.tla |gap-unmarked |OPEN |— +|Redacted bytes are withheld from the store and generated packs; the oid stays in history as evidence; signatures and the tip invariant are untouched because verification never reads withheld bytes. |abstractions.adoc, "Derived", L282 |alloy/objects.als |gap-unmarked |OPEN |— +|Redaction is enforced at ingest so content addressing cannot let anyone refill the hole exactly. |abstractions.adoc, "Derived", L283 |tla/Receive.tla |gap-unmarked |OPEN |— +|Readers surface a redaction marker, never an error. |abstractions.adoc, "Derived", L284 |alloy/objects.als |gap-unmarked |OPEN |— +|Embeddable server: keeping authorization/effect-matching logic in the library, never smeared across subprocess boundaries. |abstractions.adoc, "Derived", L289-290 |— |gap-unmarked |OPEN |— +|`git effect run` shares the identical materialization and sandbox path with the hosted worker. |abstractions.adoc, "Command surface", L324 |tla/Effects.tla |gap-unmarked |OPEN |— +|Every mutation frontend shares the identical `receive` with the hosted server. |abstractions.adoc, "Command surface", L324 |tla/Receive.tla |gap-unmarked |OPEN |— +|Revocation is a state on the member entity, not deletion; a revoked key must be explicitly rejected. |abstractions.adoc, "Command surface", L341 |tla/Receive.tla |gap-unmarked |OPEN |— +|Pushes to `refs/meta/*` never touch the working tree, so metadata behaves identically in both deployment modes. |abstractions.adoc, "Deployment", L363 |— |gap-unmarked |OPEN |— +|Worktree update happens only after `receive` accepts; core never touches a worktree. |abstractions.adoc, "Deployment", L361 |— |gap-unmarked |OPEN |— +|Bootstrap gap: an empty member list admits every push so the first member can enroll. |abstractions.adoc, "Deployment", L365 |tla/Receive.tla |gap-unmarked |OPEN |— +|An anchor MUST identify the exact content it was captured against (commit, path, blob oid, optional 1-based inclusive range); creation MUST validate path and range against the revision's actual content. |docs/spec/anchor.adoc, [#anchor.definition], ~L9-17 |alloy/objects.als |gap-unmarked |OPEN |— +|Anchored text MUST be fully derivable from the blob and line range, derived at read time, never stored redundantly; the anchored commit's id is recorded only as a plain data field, and MAY be gc'd. |docs/spec/anchor.adoc, [#anchor.immutable], ~L19-28 |alloy/objects.als |gap-unmarked |OPEN |— +|The anchoring document MUST embed the anchored blob "referenced by the existing blob's own object id rather than copied" plus a context blob "written fresh", as ordinary tree entries, keeping content reachable "for as long as the document's ref exists". |docs/spec/anchor.adoc, [#anchor.retention], ~L30-45 |alloy/objects.als |dangling_anchor_violation, dangling_context_violation |OPEN |— +|Projection MUST report one of exactly four outcomes (current/relocated/outdated/deleted), MUST follow renames, and MUST work between any two commits — forwards, backwards, or across unrelated history — while the anchor's own commit exists. |docs/spec/anchor.adoc, [#anchor.projection], ~L48-61 |— |gap-unmarked |OPEN |— +|After the anchored commit is gc'd, fuzzy fallback recovers the same four outcomes approximately; "an outdated or deleted projection MUST NOT lose the anchor". |docs/spec/anchor.adoc, [#anchor.fuzzy-fallback], ~L63-74 |— |gap-unmarked |OPEN |— +|A working-tree anchor survives its content being "committed, amended, or discarded"; it records HEAD only as a "best-effort, never-load-bearing" field; projection MUST support the working tree as target. |docs/spec/anchor.adoc, [#anchor.working-tree], ~L76-93 |alloy/objects.als |gap-unmarked |OPEN |— +|An effect definition MUST be rejected before storage when a toolchain name is not a valid ref-path segment or the trigger fails to parse (including `rev()` naming `refs/meta/*` or `meta()` naming an effect-written namespace). |docs/spec/effect.adoc, [#effect.validation], ~L41-50 |alloy/gate_rules.als |gap-unmarked |OPEN |— +|Host-direct execution MUST require an explicit `--unsandboxed` flag and MUST be "available only locally, never on canonical hosted infrastructure". |docs/spec/effect.adoc, [#effect.execution], ~L54-68 |— |gap-unmarked |OPEN |— +|An effect's stored data MUST NOT select its own executor, demand `--unsandboxed`, or set retry bounds; those are deployment configuration, "never a field an effect definition can carry". |docs/spec/effect.adoc, [#effect.deployment-property], ~L70-78 |— |gap-unmarked |OPEN |— +|A member running `git effect run` locally MUST see "the same outcome a canonical worker would record"; only the queue is skipped, and the queue carries no correctness content. |docs/spec/effect.adoc, [#effect.local-run], ~L80-89 |tla/Effects.tla |gap-unmarked |OPEN |— +|Result write-back MUST be "an ordinary receive client, never a privileged write outside the gate". |docs/spec/effect.adoc, [#effect.results-writeback], ~L93-106 |tla/Receive.tla |gap-unmarked |OPEN |— +|Only the sandbox MAY touch a toolchain's extracted bytes; declared components MUST be resolved during effect execution, "never by any other code path". |docs/spec/effect.adoc, [#effect.toolchains], ~L161-168 |— |gap-unmarked |OPEN |— +|A fanout index MUST be rebuilt only by an effect and written back only as a worker-signed commit, "never by any privileged out-of-band writer". |docs/spec/effect.adoc, [#effect.fanout-index], ~L174-184 |tla/Effects.tla |gap-unmarked |OPEN |— +|Verification MUST depend only on the read half of the RefStore seam, never on write access or on any state outside `refs/meta/*`. |docs/spec/gate.adoc, intro (also [#arch.refstore-read-cas-split]), ~L3-5 |alloy/gate_rules.als |gap-unmarked |OPEN |— +|Authorization is judged against the member entity in force at acceptance time — the member ref's tip in the same snapshot the gate reads. |docs/spec/gate.adoc, [#gate.tip-signed], ~L12-23 |tla/Receive.tla |unsigned_violation (partial: enrolled-membership only, not snapshot-scoped refname authorization) |OPEN |— +|A gate-owned hash-identified entity's creation MUST strictly decode as its type, an unknown tree entry refusing; the gate-owned entity structs MUST stay pairwise disjoint under this decode. |docs/spec/gate.adoc, [#gate.identity-binding], ~L36-40 |alloy/binding.als |gap-unmarked |OPEN |— +|When an object the binding needs is withheld by redaction, the binding MUST be vouched by the admin-signed redaction record, and a redacted object MUST NOT be re-admitted. |docs/spec/gate.adoc, [#gate.identity-binding], ~L47-51 |tla/Receive.tla |gap-unmarked |OPEN |— +|Advancing a hash-identified entity's ref is authorized only for the genesis signer or an admin; a review ref advances only under the signature of the member its refname names. |docs/spec/gate.adoc, [#gate.owner-mutation], ~L54-67 |alloy/gate_rules.als |gap-unmarked |OPEN |— +|A pre-flight verdict "is a prediction that can only go stale; it MUST NOT diverge from the rules the hosted store will actually apply". |docs/spec/gate.adoc, [#gate.call-sites], ~L188-196 |tla/Receive.tla |gap-unmarked |OPEN |— +|Transport-auth evidence MUST be threaded through uninterpreted — "never substituted for the tip invariant on a `refs/meta/*` update"; no advisory call site MAY render a `refs/heads/*` verdict meanwhile. |docs/spec/gate.adoc, [#gate.branch-acl-undefined], ~L267-284 |tla/Receive.tla |gap-unmarked |OPEN |— +|With no `refs/meta/member/*` ref, first enrollment is self-admitting; but a member set whose keys are all revoked "MUST fail closed: revoking every key MUST NOT reopen this self-admitting window". |docs/spec/gate.adoc, [#gate.bootstrap], ~L288-296 |tla/Receive.tla |gap-unmarked |OPEN |— +|`git ents lsp` MUST NOT bind a network socket, MUST NOT add a git-serving transport, and MUST receive its signing identity by injection from the composition root. |docs/spec/lens.adoc, [#lens.serve], ~L13-24 |— |gap-unmarked |OPEN |— +|Lens ranges are derived at request time via projection and "never cached across mutations of the comment's ref"; non-`open` comments omitted unless asked. |docs/spec/lens.adoc, [#lens.lenses], ~L26-39 |— |gap-unmarked |OPEN |— +|Comment diagnostics "MUST NEVER use warning or error severity" and MUST be suppressible without affecting the lenses. |docs/spec/lens.adoc, [#lens.diagnostics], ~L41-50 |— |gap-unmarked |OPEN |— +|Composing MUST require no client-specific extension; a richer input surface "MUST be sugar over the same create operation, never a second mechanism". |docs/spec/lens.adoc, [#lens.compose], ~L61-75 |— |gap-unmarked |OPEN |— +|Editor-composed comments MUST anchor to the working tree's content when it differs from HEAD — "exactly the bytes the author was reading". |docs/spec/lens.adoc, [#lens.working-tree], ~L77-87 |alloy/objects.als |gap-unmarked |OPEN |— +|Every lens operation MUST be the same library call the `git ents comment` porcelain exposes; the CLI listing MUST offer a machine-readable form sufficient for an agent with no editor attached. |docs/spec/lens.adoc, [#lens.parity], ~L89-101 |— |gap-unmarked |OPEN |— +|All forge state MUST live under `refs/meta/*`; retention pins under `refs/meta/pins/*` are "the sole exception" to tree-is-the-entity, carrying the empty tree, never an entity. |docs/spec/meta-ref.adoc, [#meta-ref.namespace], ~L15-27 |alloy/objects.als |gap-unmarked |OPEN |— +|Inbox routing preserves the canonical ref's entire path below `refs/meta/` so "two different entity kinds can never collide under the same inbox id"; `<member>` is the leading segment so authorization keys off the refname alone. |docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L45-61 |alloy/binding.als |gap-unmarked |OPEN |— +|A member is authorized only for its own `refs/meta/inbox/<member>/*` segment; "no member, including an admin-registered one, MAY write into another member's inbox segment". |docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L62-68 |alloy/gate_rules.als |gap-unmarked |OPEN |— +|An inbox ref MUST NOT be deleted on adoption or at any other time — it remains the contributor's audit trail. |docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L69-71 |tla/Receive.tla |gap-unmarked |OPEN |— +|`self` is its own top-level namespace, keeping the canonical results glob and the self-run glob "disjoint by construction"; both namespaces hold the same typed trees as canonical, only the refname rule differs. |docs/spec/meta-ref.adoc, [#meta-ref.inbox], ~L72-85 |alloy/binding.als |gap-unmarked |OPEN |— +|For a hash-identified entity, "every parentless commit reachable from the proposed tip MUST be that genesis" — the reachability form makes doppelgänger replay impossible and holds across divergence merges. |docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L117-124 |alloy/binding.als |genesis_violation, second_root_violation |OPEN |— +|The parentless-roots walk MUST NOT be applied to pins: a pin's ancestry deliberately reaches into code history. |docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L132-135 |alloy/binding.als |gap-unmarked |OPEN |— +|Who authored a state, and when, MUST come from the commit itself, never from duplicated tree fields: "each datum has exactly one signed home". |docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L144-147 |alloy/objects.als |gap-unmarked |OPEN |— +|Within a meta-ref's history a commit parent means exactly one thing — the prior state of the same entity (pin retained-commit parents sole exception); a cross-entity relationship MUST be tree data, never a parent edge. |docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L147-150 |alloy/objects.als |gap-unmarked |OPEN |— +|A genesis commit is frozen by the identity derived from it, so hash-identified/composite-keyed structs MUST evolve additively only — "new fields optional, required fields never added, renamed, or removed". |docs/spec/meta-ref.adoc, [#meta-ref.identity-binding], ~L149-153 |alloy/objects.als |gap-unmarked |OPEN |— +|A struct change is a migration committed on top of the old tip; history keeps the old encoding, and a struct change "MUST NOT rewrite or delete a prior commit on the ref". |docs/spec/meta-ref.adoc, [#meta-ref.migration], ~L172-180 |alloy/objects.als |gap-unmarked |OPEN |— +|The gate and `receive` are content-agnostic: verification depends on "signature, refname, trailer, and DAG descent, never on tree contents", so a stock server MUST carry entity types it cannot parse. |docs/spec/model.adoc, [#model.extensibility], ~L8-22 |alloy/gate_rules.als |gap-unmarked |OPEN |— +|A facet shape MUST be compile-time-defined: runtime-readable, never runtime-constructible. |docs/spec/model.adoc, [#model.extensibility], ~L13-15 |— |gap-unmarked |OPEN |— +|A member's id binds to its key-carrying entity's refname final segment; enrollment occurs as a signed commit — the member is forge state "with no user database separate from the repository". |docs/spec/model.adoc, [#model.member-identity], ~L31-40 |alloy/binding.als |gap-unmarked |OPEN |— +|Admission consults the member entity currently in force, so a revoked key's new pushes are refused "from the moment the revocation lands, regardless of any committer timestamp the pushed commit claims". |docs/spec/model.adoc, [#model.member-revocation], ~L47-50 |tla/Receive.tla |gap-unmarked |OPEN |— +|A ref accepted before the revocation landed remains valid: "acceptance is never re-judged". |docs/spec/model.adoc, [#model.member-revocation], ~L51-52 |tla/Receive.tla |gap-unmarked |OPEN |— +|Unrevoking returns the key to authorizing new signatures "without altering the record of the period it was revoked". |docs/spec/model.adoc, [#model.member-revocation], ~L60-61 |tla/Receive.tla |gap-unmarked |OPEN |— +|A self-attested member MUST NOT be authorized for canonical refs — writes limited to its own inbox and self-run namespaces — until an admin-registered member promotes it. |docs/spec/model.adoc, [#model.member-provenance], ~L64-75 |alloy/gate_rules.als |gap-unmarked (effect_admin_violation covers only the effects namespace, not the provenance tier generally) |OPEN |— +|A machine actor is an ordinary Member entity, revocable like any human key; "a privileged write path for a machine actor MUST NOT exist outside this model". |docs/spec/model.adoc, [#model.member-worker], ~L77-86 |tla/Receive.tla |gap-unmarked |OPEN |— +|A comment's identity is the oid of its genesis commit and "MUST NEVER change afterward: edits advance the ref, they do not rename it". |docs/spec/model.adoc, [#model.comment], ~L99-102 |alloy/binding.als |gap-unmarked |OPEN |— +|A comment about nothing MUST be refused at creation by the writing tool, "though never by the gate, which stays content-agnostic". |docs/spec/model.adoc, [#model.comment], ~L93-98 |— |gap-unmarked |OPEN |— +|A new comment's state is `open`; resolving records `resolved` as an ordinary mutation commit — "never a deletion, so the conversation stays auditable" — and reopening is supported the same way. |docs/spec/model.adoc, [#model.comment-state], ~L109-121 |— |gap-unmarked |OPEN |— +|A state-changing mutation by an enrolled key MUST carry a `Key-for-<member-id>` trailer whose value is the member ref's tip oid at mutation time, pinning the enrolled record across later rotation or revocation. |docs/spec/model.adoc, [#model.comment-provenance], ~L123-129 |— |gap-unmarked |OPEN |— +|An entity's thread MUST be an aggregation query over comment refs; a context entity MUST NOT store its comment list, so concurrent commenters "never race a shared ref". |docs/spec/model.adoc, [#model.comment-context], ~L132-142 |alloy/objects.als |gap-marked (instance of abstraction 1's granularity rule) |OPEN |— +|A reply's parent MUST exist when the reply is created; aboutness is inherited from the thread root; no comment stores a list of its replies. |docs/spec/model.adoc, [#model.comment-thread], ~L144-154 |alloy/objects.als |gap-unmarked |OPEN |— +|An issue's identity is its genesis oid — no sequential counter exists — and machine-readable output (including `--porcelain`) MUST carry the full id. |docs/spec/model.adoc, [#model.issue], ~L158-177 |alloy/binding.als |gap-unmarked |OPEN |— +|A review binds by composite key `reviews/<target>/<member>`; at genesis the reviewed-commit tree field equals the `<target>` segment and binds it; re-reviewing advances the field while the refname stays keyed by genesis. |docs/spec/model.adoc, [#model.review], ~L181-198 |alloy/binding.als |gap-unmarked |OPEN |— +|Every review MUST occupy exactly two refs: the entity ref and its retention pin. |docs/spec/model.adoc, [#model.review], ~L191-193 |alloy/objects.als |gap-unmarked |OPEN |— +|A review's verdict MUST be a hard enum — `approve`, `request-changes`, or `comment`: "a verdict gates decisions, so its vocabulary is platform, not schema". |docs/spec/model.adoc, [#model.review], ~L199-202 |— |gap-unmarked |OPEN |— +|A pin's tip is a reviewer-signed commit whose parents include the reviewed commit, so that commit and its ancestry "survive force-push, branch deletion, and gc for as long as the review exists". |docs/spec/model.adoc, [#model.review-pin], ~L213-224 |alloy/objects.als |gap-unmarked |OPEN |— +|Re-reviewing MUST advance the pin fast-forward with parents = previous pin tip + newly reviewed commit, so every reviewed round stays retained and the pin's history is the audit trail. |docs/spec/model.adoc, [#model.review-pin], ~L225-229 |alloy/objects.als |gap-unmarked |OPEN |— +|A result MUST carry the effect's name and the judged commit's full oid as tree fields from which the refname derives — "a result MUST mean something with the refname stripped away" (a signed `pass` cannot be replayed against another effect/commit). |docs/spec/model.adoc, [#model.result-identity], ~L260-270 |alloy/binding.als |gap-unmarked |OPEN |— +|Result fields are not parent edges: a result ref's parents stay prior states of the same result, and a result MUST NOT retain the judged commit's ancestry the way a pin does. |docs/spec/model.adoc, [#model.result-identity], ~L271-274 |alloy/objects.als |gap-unmarked |OPEN |— +|A toolchain is a hash-pinned ~1KB manifest carrying its own provenance, "a resource an effect declares as a dependency … never a trigger condition in its own right". |docs/spec/model.adoc, [#model.toolchain], ~L279-289 |— |gap-unmarked |OPEN |— +|A Redaction entity carries the target oid, a reason, and the admin signature; it "MUST NOT carry the redacted content itself". |docs/spec/model.adoc, [#model.redaction], ~L294-300 |alloy/objects.als |gap-unmarked |OPEN |— +|Authentication state MUST live in the repository as ordinary forge state; "a session database or token table MUST NOT back it". |docs/spec/model.adoc, [#model.account], ~L308-313 |— |gap-unmarked |OPEN |— +|The library MUST NOT define its own ObjectStore trait — gitoxide's `Find`/`Exists`/`Write` ARE the seam; a new trait exists only where gitoxide is silent. |docs/spec/overview.adoc, [#arch.no-object-store-trait], ~L180-189 |— |gap-unmarked |OPEN |— +|The gate's pure verify function MUST live in a crate separate from `receive`; advisory call sites MUST be answerable without linking effect-matching and enqueue logic. |docs/spec/overview.adoc, [#arch.gate-receive-split], ~L191-199 |— |gap-unmarked |OPEN |— +|The query algebra MUST live apart from executor code; `receive` MUST NOT depend on the effect crate, "so no push path links executor code". |docs/spec/overview.adoc, [#arch.query-effect-split], ~L201-208 |— |gap-unmarked |OPEN |— +|A concrete store implementation is wired only inside a composition root, never a library crate, and is not promoted to a shared library crate until a second root consumes it. |docs/spec/overview.adoc, [#arch.store-composition-root], ~L211-219 |— |gap-unmarked |OPEN |— +|A loose-ref RefStore MUST write refs through its own CAS discipline and MUST NOT shell out to `git update-ref`, so local mutations honor the same CAS guarantee as hosted. |docs/spec/overview.adoc, [#arch.loose-cas-discipline], ~L239-245 |tla/Receive.tla |gap-unmarked |OPEN |— +|A CommitQuery MUST parse per the fixed grammar; `\|`/`&`/`-` denote union/intersection/difference, left-associative at a single precedence level, parentheses the only override. |docs/spec/query.adoc, [#query.grammar] (+ [#query.set-ops]), ~L12-35 |tla/Effects.tla |gap-unmarked |OPEN |— +|Unsupported rev syntax (`~n`/`^n`, `A...B`, `@{...}`, abbreviated hex) and any `refs/meta/*` pattern MUST be rejected as malformed — "never silently evaluated to the empty set or to the wrong set". |docs/spec/query.adoc, [#query.rev], ~L39-58 |tla/Effects.tla |gap-unmarked |OPEN |— +|Membership in `results(effect, status)` is decided solely by existence of a matching results ref — never by reachability from `refs/heads/*` or any ref outside the query's footprint — and resolution is a refname scan, never a history walk. |docs/spec/query.adoc, [#query.results], ~L61-79 |tla/Effects.tla |gap-unmarked |OPEN |— +|The fanout index "MUST NOT be addressable by any query atom at all". |docs/spec/query.adoc, [#query.meta], ~L82-91 |tla/Effects.tla |gap-unmarked |OPEN |— +|`self` in the work set is evaluation-time notation, "not a keyword an author may write in a trigger"; work-set evaluation inherits incremental bounds and refname-scan resolution, never a full-history walk. |docs/spec/query.adoc, [#query.workset], ~L159-173 |tla/Effects.tla |gap-marked (work-set/dedup materialization is the declared cross-transaction gap) |OPEN |— +|Replicating refs a trusted remote already admitted MAY apply directly (re-verification on fetch is opt-in audit); commits the replicating machinery authors itself — divergence and adoption merges — are origination, not replication. |docs/spec/receive.adoc, [#receive.unit], ~L10-27 |tla/Receive.tla |gap-unmarked |OPEN |— +|Gate evaluation MUST be checkable against exactly the proposal shape, frontend-independent; meta-ref admission "MUST ignore [transport-auth evidence] entirely and MUST NOT consult it in place of the tip invariant". |docs/spec/receive.adoc, [#receive.proposal-shape], ~L29-47 |tla/Receive.tla |gap-unmarked |OPEN |— +|An entity declared across multiple refs MUST write them in a single Proposal through one `receive` call; the atomic multi-ref CAS admits or refuses the whole batch, "so such an entity is never observable with only some of its refs written". |docs/spec/receive.adoc, [#receive.multi-ref-atomicity], ~L49-66 |tla/Receive.tla |gap-unmarked |OPEN |— +|A `receive` inside a git hook reads existing state through the common object directory, never git's quarantine directory: quarantined objects "MUST NOT be treated as stored until the transaction commits". |docs/spec/receive.adoc, [#receive.object-access], ~L93-105 |tla/Durability.tla |gap-unmarked |OPEN |— +|Pending obligations MUST be derivable from repository state alone; an EventSink MAY lose events on crash provided the root reconciles at startup before serving pushes; "a durable queue MUST be treated as a performance optimization, never a correctness requirement". |docs/spec/receive.adoc, [#receive.reconstructible], ~L134-146 |tla/Durability.tla |gap-marked (cross-transaction queue/materialization state is the declared dedup gap) |OPEN |— +|A push to `refs/meta/redactions/*` MUST be rejected unless the member is admin-registered, regardless of any other role rule, statable as a single refname glob. |docs/spec/receive.adoc, [#receive.redaction-admin-only], ~L148-158 |alloy/gate_rules.als |gap-unmarked (effect_admin_violation covers only `refs/meta/effects/*`; no redactions-namespace rule exists) |OPEN |— +|The local root wires loose refs, the odb, Docker, null EventSink, and the advisory gate; `git ents serve` MUST NOT expose git's smart-HTTP wire protocol; local effect execution is pull, "never a daemon watching refs". |docs/spec/roots.adoc, [#roots.local], ~L20-32 |— |gap-unmarked |OPEN |— +|The single-node hosted root's hooks call the gate and reconcile around `receive-pack`'s own ref update, "never through this crate's own `RefStore::transaction`, to avoid a double-write race". |docs/spec/roots.adoc, [#roots.single-node-hosted], ~L34-52 |tla/Receive.tla |gap-unmarked |OPEN |— +|The worker MUST NOT share in-process state with `receive`. |docs/spec/roots.adoc, [#roots.hosted], ~L55-63 |tla/Effects.tla |gap-unmarked |OPEN |— +|Wiring the scale-out root (Postgres/Tigris/durable queue) MUST require zero modification to any library crate — the seam design's honesty test, proven by an actual production migration. |docs/spec/roots.adoc, [#roots.honesty-test], ~L66-75 |— |gap-unmarked |OPEN |— +|Configuration selects trait implementations only at the composition root and MUST NOT leak past it. |docs/spec/roots.adoc, [#roots.config-isolation], ~L78-83 |— |gap-unmarked |OPEN |— +|`ents-web` receives its signing identity by injection and MUST NOT assume a network; in-process webview embedding remains a supported deployment. |docs/spec/roots.adoc, [#roots.web-agnostic], ~L96-103 |— |gap-unmarked |OPEN |— +|A hosted web session is held only in server memory; every state-changing request carries a per-session CSRF token verified before acting; a web edit is signed only on behalf of an authenticated session. |docs/spec/roots.adoc, [#roots.web-session], ~L141-148 |— |gap-unmarked |OPEN |— +|Every repository-path segment MUST be validated before filesystem or subprocess use, rejecting escapes, nesting inside an existing repository, or namespace-directory collisions. |docs/spec/roots.adoc, [#roots.path-validation], ~L151-158 |— |gap-unmarked |OPEN |— +|Fetch authorization MUST be refname-keyed, using the same authorization model as write authorization. |docs/spec/roots.adoc, [#roots.fetch-auth], ~L160-167 |alloy/gate_rules.als |gap-unmarked |OPEN |— +|A clone plus `refs/meta/*` MUST carry the complete audit history and the signatures needed to verify it, "with no server-side data left behind". |docs/spec/sync.adoc, [#sync.forge-transfer], ~L9-16 |alloy/objects.als |gap-unmarked |OPEN |— +|Inbox adoption and self-run adoption MUST both go through the same merge machinery as divergence resolution, "not a separate adoption code path". |docs/spec/sync.adoc, [#sync.adoption-machinery], ~L50-57 |tla/Receive.tla |gap-unmarked |OPEN |— +|"Nothing in the resulting ref-store state lets a pure verifier tell" a cherry-picked adoption from a hand-authored commit — attribution preservation binds the merge machinery, never the gate. |docs/spec/sync.adoc, [#sync.adoption-no-cherry-pick] (also gate.adoc Adoption intro ~L218-224), ~L59-73 |tla/Receive.tla |gap-unmarked |OPEN |— +|===

verify/tla/Durability.cfg @@ -1,0 +1,8 @@ +\* TLC configuration for the Durability skeleton (verify/exercise.md, +\* Phase 5). +SPECIFICATION Spec +CONSTANTS + Oids = {o1, o2} + RefNames = {r1} + NoOid = NoOid +INVARIANTS TypeOK RefsPointDurable

verify/tla/Durability.tla @@ -1,0 +1,72 @@ +--------------------------- MODULE Durability --------------------------- +(***************************************************************************) +(* Phase 5 — durability ordering (verify/exercise.md, "Phase 5"). *) +(* *) +(* SKELETON. Variables and action signatures only; every body is a *) +(* TODO(exercise) stub that changes no state. This module checks NOTHING *) +(* until the human exercise fills it in. *) +(* *) +(* Deployment note: the exercise document frames this phase around a *) +(* hosted Tigris-object-store + Postgres-CAS split. The project currently *) +(* deploys neither — serving is plain git http-backend over one *) +(* filesystem — so the actions here are named for the general shape *) +(* (object write, ref CAS, crash), and the Tigris/Pg instantiation is *) +(* deferred until such a deployment exists. The invariant under study is *) +(* unchanged: no ref points outside the durable object set. *) +(* *) +(* Vocabulary: object ids and refnames as in the other modules, matching *) +(* ents-gate-rules' EDB vocabulary. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + Oids, \* object ids in play + RefNames, \* meta-ref names in play + NoOid \* model value: unborn ref + +OldOids == Oids \cup {NoOid} + +VARIABLES + durable, \* SUBSET Oids: objects durably written + refstore \* RefNames -> OldOids: the ref store's current tips + +vars == <<durable, refstore>> + +----------------------------------------------------------------------------- +(* Actions. SKELETONS: signatures and intent only. *) + +\* An object (or pack) reaches durable storage. +ObjectWrite == + /\ TRUE \* TODO(exercise) + /\ UNCHANGED vars + +\* The ref store compare-and-swaps a tip. +RefCAS == + /\ TRUE \* TODO(exercise): the write-order question lives here + /\ UNCHANGED vars + +\* Crash at any point; recovery obligations follow from what survives. +Crash == + /\ TRUE \* TODO(exercise) + /\ UNCHANGED vars + +----------------------------------------------------------------------------- +Init == + /\ durable = {} + /\ refstore = [r \in RefNames |-> NoOid] + +Next == ObjectWrite \/ RefCAS \/ Crash + +Spec == Init /\ [][Next]_vars + +TypeOK == + /\ durable \subseteq Oids + /\ refstore \in [RefNames -> OldOids] + +\* The invariant this phase exists to prove. STATED here so the ledger +\* row has a formal object to point at; NOT proved — the actions above +\* are stubs, so checking it today says nothing. TODO(exercise). +RefsPointDurable == + \A r \in RefNames : refstore[r] # NoOid => refstore[r] \in durable + +=============================================================================

verify/tla/Effects.cfg @@ -1,0 +1,9 @@ +\* TLC configuration for the Effects skeleton (verify/exercise.md, Phase 4). +SPECIFICATION Spec +CONSTANTS + Oids = {o1, o2, o3} + RefNames = {r1, r2} + EffectRefs = {r2} + Keys = {k1, k2} + NoOid = NoOid +INVARIANT TypeOK

verify/tla/Effects.tla @@ -1,0 +1,106 @@ +---------------------------- MODULE Effects ---------------------------- +(***************************************************************************) +(* Phase 4 — effects (verify/exercise.md, "Phase 4"). *) +(* *) +(* SKELETON. Variables and action signatures only; every body is a *) +(* TODO(exercise) stub that changes no state. This module checks NOTHING *) +(* until the human exercise fills it in on top of Phase 3's state. *) +(* *) +(* Discharges, once filled in: docs/abstractions.adoc §6 (monotone, *) +(* exactly-once effects); docs/spec/effect.adoc (trigger set, dedup key *) +(* (effect, refname, new_oid), results write-back, admin-only authoring). *) +(* Note ents-gate-rules marks the cross-transaction dedup obligation as *) +(* a deliberate gap — this model is where that obligation lives. *) +(* *) +(* Vocabulary: the transaction record mirrors ents-gate-rules' EDB *) +(* relations one-to-one, as in Receive.tla. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + Oids, \* object ids in play + RefNames, \* meta-ref names in play + EffectRefs, \* the RefNames under refs/meta/effects/* + Keys, \* signing keys in play + NoOid \* model value: absent old tip / unborn ref + +ASSUME EffectRefs \subseteq RefNames + +Roles == {"admin", "member"} +OldOids == Oids \cup {NoOid} + +VARIABLES + refs, \* RefNames -> OldOids: current tips (Phase 3 state) + objects, \* SUBSET Oids + members, \* SUBSET (Keys \X Roles) + epoch, \* Nat + triggered, \* commits that have entered the trigger set (§6) + queue, \* at-least-once delivery: dedup keys <<effect, ref, new_oid>> + results \* result-ref writes performed so far + +vars == <<refs, objects, members, epoch, triggered, queue, results>> + +(* The transaction record type: ents-gate-rules' Facts, field for field. *) +Txns == [ref_update : SUBSET (RefNames \X OldOids \X Oids), + parent : SUBSET (Oids \X Oids), + signed_by : SUBSET (Oids \X Keys), + anchor : SUBSET (Oids \X Oids), + context : SUBSET (Oids \X Oids), + object_exists : SUBSET Oids] + +\* The dedup key the doc claims yields exactly-once observable effects. +DedupKeys == EffectRefs \X RefNames \X Oids + +----------------------------------------------------------------------------- +(* Actions. SKELETONS: signatures and intent only. *) + +\* A gated ref advance (reuses Phase 3's GateAdmits when composed). +RefAdvance == + /\ TRUE \* TODO(exercise) + /\ UNCHANGED vars + +\* A commit ENTERS the trigger set (§6 "fires once per commit that enters +\* the set") — the delete-and-repush re-entry question lives here. +TriggerEval == + /\ TRUE \* TODO(exercise) + /\ UNCHANGED vars + +\* At-least-once enqueue of a dedup key. +Enqueue == + /\ TRUE \* TODO(exercise) + /\ UNCHANGED vars + +\* Executor runs an effect; may crash and restart (duplicate delivery). +Execute == + /\ TRUE \* TODO(exercise) + /\ UNCHANGED vars + +\* Result write-back: a gated write like any other, by an executor key. +ResultPush == + /\ TRUE \* TODO(exercise) + /\ UNCHANGED vars + +----------------------------------------------------------------------------- +Init == + /\ refs = [r \in RefNames |-> NoOid] + /\ objects = {} + /\ members = {} + /\ epoch = 0 + /\ triggered = {} + /\ queue = {} + /\ results = {} + +Next == RefAdvance \/ TriggerEval \/ Enqueue \/ Execute \/ ResultPush + +Spec == Init /\ [][Next]_vars + +TypeOK == + /\ refs \in [RefNames -> OldOids] + /\ objects \subseteq Oids + /\ members \subseteq (Keys \X Roles) + /\ epoch \in Nat + /\ triggered \subseteq Oids + /\ queue \subseteq DedupKeys + /\ results \subseteq DedupKeys + +=============================================================================

verify/tla/Receive.cfg @@ -1,0 +1,11 @@ +\* TLC configuration for the Receive skeleton (verify/exercise.md, Phase 3). +\* Scope discipline per the exercise: tiny universes; two members, two +\* refs, three commits is where the bugs live. +SPECIFICATION Spec +CONSTANTS + Oids = {o1, o2, o3} + RefNames = {r1, r2} + EffectRefs = {r2} + Keys = {k1, k2} + NoOid = NoOid +INVARIANT TypeOK

verify/tla/Receive.tla @@ -1,0 +1,195 @@ +---------------------------- MODULE Receive ---------------------------- +(***************************************************************************) +(* Phase 3 — gate and receive as a protocol (verify/exercise.md, *) +(* "Phase 3"). *) +(* *) +(* SKELETON. Variables and action signatures only. The one definition *) +(* with real content is GateAdmits: the seven denial rules of *) +(* crates/kernel/ents-gate-rules/src/lib.rs transcribed mechanically — *) +(* that transcription is the refinement anchor (Phase 0.5's model *) +(* reused). Every action body is a TODO(exercise) stub that changes no *) +(* state; this module checks NOTHING about the protocol until the human *) +(* exercise fills the actions in. *) +(* *) +(* Discharges, once filled in: docs/abstractions.adoc §5 (tip invariant, *) +(* adoption, revocation), §4 (anti-replay); docs/spec/receive.adoc; *) +(* docs/spec/gate.adoc epoch bootstrap. *) +(* *) +(* Vocabulary: a transaction is a record whose fields mirror the EDB *) +(* relations of ents-gate-rules one-to-one: ref_update, parent, *) +(* signed_by, anchor, context, object_exists — with member supplied from *) +(* the protocol-state variable `members`, exactly as the crate's *) +(* extractor would supply it. *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS + Oids, \* object ids in play + RefNames, \* meta-ref names in play + EffectRefs, \* the RefNames under refs/meta/effects/* + Keys, \* signing keys in play + NoOid \* model value: absent old tip (entity creation) + +ASSUME EffectRefs \subseteq RefNames + +Roles == {"admin", "member"} +OldOids == Oids \cup {NoOid} + +VARIABLES + refs, \* RefNames -> OldOids: current tips (NoOid = unborn) + objects, \* SUBSET Oids: the store's object set + members, \* SUBSET (Keys \X Roles): enrolled keys and provenance + epoch, \* Nat: the config ref's epoch (§5) — placeholder until Phase 3 + proposed \* transactions in flight, each a record over the EDB fields + +vars == <<refs, objects, members, epoch, proposed>> + +(* The transaction record type: ents-gate-rules' Facts, field for field. *) +Txns == [ref_update : SUBSET (RefNames \X OldOids \X Oids), + parent : SUBSET (Oids \X Oids), + signed_by : SUBSET (Oids \X Keys), + anchor : SUBSET (Oids \X Oids), + context : SUBSET (Oids \X Oids), + object_exists : SUBSET Oids] + +----------------------------------------------------------------------------- +(* IDB relations of ents-gate-rules, transcribed. *) + +\* ancestor: transitive ancestry over the transaction's parent edges. +TC(R) == + LET N == {p[1] : p \in R} \cup {p[2] : p \in R} + IN { ab \in N \X N : + \E n \in 1..Cardinality(N) : + \E f \in [1..(n+1) -> N] : + /\ f[1] = ab[1] + /\ f[n+1] = ab[2] + /\ \A i \in 1..n : <<f[i], f[i+1]>> \in R } + +Ancestors(t, c) == {a \in Oids : <<c, a>> \in TC(t.parent)} + +HasParent(t, c) == \E p \in Oids : <<c, p>> \in t.parent + +\* covered: commits already covered by a ref's old tip. +Covered(t, old) == IF old = NoOid THEN {} ELSE {old} \cup Ancestors(t, old) + +\* introduced: the new tip and its ancestors, minus everything covered. +Introduced(t, old, new) == ({new} \cup Ancestors(t, new)) \ Covered(t, old) + +MemberSigned(t, mem, c) == + \E k \in Keys : /\ <<c, k>> \in t.signed_by + /\ \E r \in Roles : <<k, r>> \in mem + +AdminSigned(t, mem, c) == + \E k \in Keys : /\ <<c, k>> \in t.signed_by + /\ <<k, "admin">> \in mem + +----------------------------------------------------------------------------- +(* The seven denial rules, same names as the crate. *) + +\* Fast-forward-only: the new tip must descend from the old tip. +FfViolation(t) == + \E u \in t.ref_update : /\ u[2] # NoOid + /\ u[2] # u[3] + /\ u[2] \notin Ancestors(t, u[3]) + +\* Creation must point at a parentless genesis commit. +GenesisViolation(t) == + \E u \in t.ref_update : /\ u[2] = NoOid + /\ HasParent(t, u[3]) + +\* One entity, one root: past genesis, no second parentless commit. +SecondRootViolation(t) == + \E u \in t.ref_update : + /\ u[2] # NoOid + /\ \E c \in Introduced(t, u[2], u[3]) : ~HasParent(t, c) + +\* Every introduced commit carries an enrolled member's signature. +UnsignedViolation(t, mem) == + \E u \in t.ref_update : + \E c \in Introduced(t, u[2], u[3]) : ~MemberSigned(t, mem, c) + +\* An anchored blob must resolve. +DanglingAnchorViolation(t) == + \E u \in t.ref_update : + \E c \in Introduced(t, u[2], u[3]) : + \E b \in Oids : /\ <<c, b>> \in t.anchor + /\ b \notin t.object_exists + +\* The paired context blob must resolve too. +DanglingContextViolation(t) == + \E u \in t.ref_update : + \E c \in Introduced(t, u[2], u[3]) : + \E b \in Oids : /\ <<c, b>> \in t.context + /\ b \notin t.object_exists + +\* A write to refs/meta/effects/* must be admin-signed. +EffectAdminViolation(t, mem) == + \E u \in t.ref_update : + /\ u[1] \in EffectRefs + /\ \E c \in Introduced(t, u[2], u[3]) : ~AdminSigned(t, mem, c) + +(* gate(facts) = {}: the conjunction that admits a transaction. *) +GateAdmits(t, mem) == + /\ ~FfViolation(t) + /\ ~GenesisViolation(t) + /\ ~SecondRootViolation(t) + /\ ~UnsignedViolation(t, mem) + /\ ~DanglingAnchorViolation(t) + /\ ~DanglingContextViolation(t) + /\ ~EffectAdminViolation(t, mem) + \* TODO(exercise): refname recomputation from signed content — the §4 + \* binding rule ents-gate-rules omits (ledger row: DIVERGED). Phase 3 + \* decides whether ents-gate proper enforces it and adds it here. + \* TODO(exercise): epoch rule (§5) — also omitted from the crate. + +----------------------------------------------------------------------------- +(* Actions. SKELETONS: signatures and intent only; every body leaves the *) +(* state unchanged. TODO(exercise) throughout — nothing here is checked. *) + +\* A writer proposes a transaction (two writers minimum in the model). +Propose == + /\ TRUE \* TODO(exercise): choose t \in Txns, add to proposed + /\ UNCHANGED vars + +\* The gate evaluates a proposed transaction; enabling condition is the +\* seven-rule conjunction above. +GateCheck == + /\ \E t \in proposed : GateAdmits(t, members) + /\ TRUE \* TODO(exercise): mark t admitted for CAS + /\ UNCHANGED vars + +\* Compare-and-swap on the ref tip (anti-replay, §4). +CAS == + /\ TRUE \* TODO(exercise): refs' = [refs EXCEPT ...] guarded on old tip + /\ UNCHANGED vars + +\* Adoption: contributor commit in ancestry, adopter signature at tip. +AdoptMerge == + /\ TRUE \* TODO(exercise) + /\ UNCHANGED vars + +\* Two of one member's machines racing (is the merge commit signed?). +SelfMerge == + /\ TRUE \* TODO(exercise): check ents-sync/ents-receive reconcile path + /\ UNCHANGED vars + +----------------------------------------------------------------------------- +Init == + /\ refs = [r \in RefNames |-> NoOid] + /\ objects = {} + /\ members = {} + /\ epoch = 0 + /\ proposed = {} + +Next == Propose \/ GateCheck \/ CAS \/ AdoptMerge \/ SelfMerge + +Spec == Init /\ [][Next]_vars + +TypeOK == + /\ refs \in [RefNames -> OldOids] + /\ objects \subseteq Oids + /\ members \subseteq (Keys \X Roles) + /\ epoch \in Nat + /\ \A t \in proposed : t \in Txns + +=============================================================================