git ents: verify: migrate harness to Rust-native model checking

commit d36a2f3

verify: migrate harness to Rust-native model checking

stateright + proptest replace TLA+/Alloy-in-CI; the gate condition and every checked property call ents_gate_rules::gate() directly, so model/code refinement is by construction. New sink-layer crate ents-verify (depends only on ents-gate-rules; nothing depends on it, enforced). Search model rediscovers the cross-ref replay by exhaustive search within documented bounds. Alloy files retained as paper tools for design-only questions; TLA+ skeletons ported to stateright stubs.

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

Joseph D. Carpinelli · 1 month ago

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

Reviews

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

Start a review

Cargo.lock @@ -80,6 +80,7 @@ checksum = "5a15f179cd60c4584b8a8c596927aadc462e27f2ca70c04e0071964a73ba7a75" dependencies = [ "cfg-if", + "getrandom 0.3.4", "once_cell", "version_check", "zerocopy", @@ -450,6 +451,12 @@ "syn", ] +[[package]] +name = "ascii" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d92bec98840b8f03a5ff5413de5293bfcd8bf96467cf5452609f939ec6f5de16" + [[package]] name = "asciicast-rs" version = "0.3.0" @@ -695,6 +702,12 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" +[[package]] +name = "choice" +version = "0.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a3b71fc821deaf602a933ada5c845d088156d0cdf2ebf43ede390afe93466553" + [[package]] name = "chrono" version = "0.4.45" @@ -708,6 +721,12 @@ "windows-link", ] +[[package]] +name = "chunked_transfer" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6e4de3bc4ea267985becf712dc6d9eed8b04c953b3fcfb339ebc87acd9804901" + [[package]] name = "cipher" version = "0.4.4" @@ -1282,6 +1301,7 @@ version = "0.0.0" dependencies = [ "ascent", + "proptest", ] [[package]] @@ -1407,6 +1427,15 @@ "ssh-key", ] +[[package]] +name = "ents-verify" +version = "0.0.0" +dependencies = [ + "ents-gate-rules", + "proptest", + "stateright", +] + [[package]] name = "ents-web" version = "0.0.0" @@ -3086,6 +3115,12 @@ "zerovec", ] +[[package]] +name = "id-set" +version = "0.2.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9633fadf6346456cf8531119ba4838bc6d82ac4ce84d9852126dd2aa34d49264" + [[package]] name = "iddqd" version = "0.4.5" @@ -3480,6 +3515,12 @@ "libc", ] +[[package]] +name = "nohash-hasher" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2bf50223579dc7cdcfb3bfcacf7069ff68243f8c363f62ffa99cf000a6b9c451" + [[package]] name = "nom" version = "7.1.3" @@ -4493,6 +4534,26 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596" +[[package]] +name = "stateright" +version = "0.31.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fd1157f21b11916f90fe1f2ac9a8d0e09a8813b28701584141060f414eedf6ba" +dependencies = [ + "ahash", + "choice", + "crossbeam-utils", + "dashmap 6.2.1", + "id-set", + "log", + "nohash-hasher", + "parking_lot", + "rand 0.9.4", + "serde", + "serde_json", + "tiny_http", +] + [[package]] name = "static_assertions" version = "1.1.0" @@ -4689,6 +4750,18 @@ "time-core", ] +[[package]] +name = "tiny_http" +version = "0.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "389915df6413a2e74fb181895f933386023c71110878cd0825588928e64cdc82" +dependencies = [ + "ascii", + "chunked_transfer", + "httpdate", + "log", +] + [[package]] name = "tinystr" version = "0.8.3"

Cargo.toml @@ -16,6 +16,7 @@ "crates/forge/ents-forge", "crates/kiln/ents-kiln", "crates/substrate/gix-ref-store", + "crates/verify/ents-verify", ] [workspace.package] @@ -40,6 +41,7 @@ ents-receive = { path = "crates/kernel/ents-receive" } ents-sync = { path = "crates/kernel/ents-sync" } ents-testutil = { path = "crates/kernel/ents-testutil" } +ents-verify = { path = "crates/verify/ents-verify" } ents-web = { path = "crates/cli/ents-web" } gix-ref-store = { path = "crates/substrate/gix-ref-store" } arborium = { version = "2.18", default-features = false, features = [ @@ -99,6 +101,7 @@ serde_json = "1" spdx = "0.13" ssh-key = { version = "0.6", features = ["ed25519"] } +stateright = "0.31" target-lexicon = "0.13" tempfile = "3" thiserror = "2"

verify/README.adoc @@ -1,48 +1,67 @@ = 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. +This harness is Rust-native. +`crates/verify/ents-verify` and `crates/kernel/ents-gate-rules/tests/prop.rs` call `ents_gate_rules::gate` directly from every layer that checks anything, so the refinement mapping between a model and the code is the function call itself, not a hand-maintained translation of it. +Nothing in CI depends on anything outside `cargo`. + == 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. +The `model` column names which layer below discharges the claim: `search`, `stateright`, `proptest`, or `alloy-paper`. `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. +Alloy 6 models, demoted to a paper-only design tool — see `alloy/README.adoc`. +Nothing here runs in CI. -`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. +`../crates/verify/ents-verify`:: +The Rust-native replacement for the old TLA+ skeletons and the Alloy search. +`src/search.rs` is Phase 0.5's real replacement for `alloy/gate_rules.als`'s `check` commands: an exhaustive `stateright` search over a small bounded universe of transactions, calling `gate()` on each and checking the result against hand-written doc-invariant predicates. +`src/receive.rs`, `src/effects.rs`, `src/durability.rs` are Phase 3/4/5 skeletons — state and action *signatures* only, `todo!()` bodies, except `receive.rs`'s `gate_admits`, which is real code calling `gate()` directly. +Run with `cargo test -p ents-verify`. -`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. +`../crates/kernel/ents-gate-rules/tests/prop.rs`:: +The cheap floor: `proptest` samples transactions over a small domain (duplicated from `ents-verify`'s vocabulary — the dependency stays one-way) and asserts the same doc-invariant predicates on every run, not just the bounded search's 576 leaves. +Run with `cargo test -p ents-gate-rules`. + +`../crates/kernel/ents-gate-rules/tests/ledger.rs`:: +Gap-pinning tests: a ledger row found FALSIFIED or DIVERGED with a concrete counterexample lands here first, in the crate's own `Facts` vocabulary, before it becomes a denial rule. == 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. +Three tools, three jobs, deliberately not interchangeable — none of them substitutes for a human proof, and none of them is Alloy or TLA+ running in CI anymore. + +The Datalog in `ents-gate-rules` *evaluates* the seven denial rules over one supplied transaction's facts; it is executable and type-checked, but it cannot search for the transaction nobody thought of. + +`tests/prop.rs` *samples* that same search space cheaply, on every `cargo test` run, trading exhaustiveness for near-zero cost — it is the floor, not the ceiling. + +`ents-verify::search` *exhausts* a small bounded universe of transactions (`stateright`'s `Model::checker`), the direct replacement for what `verify/alloy/gate_rules.als`'s `check` commands did by external tool; it is what actually rediscovers the cross-ref replay counterexample, by search, not by hand-construction. + +`ents-verify::receive`/`effects`/`durability` are where protocol-over-time claims (receive/CAS races, adoption, epochs, effect dispatch, durability ordering) will live once filled in — `stateright` model-checks traces the same way TLC did, just in the same language and dependency graph as the code under test. + +Alloy survives only as a paper tool for design-only questions (Phases 1 and 2's structural claims about the object graph and refname binding) — see `alloy/README.adoc`. +Kani is noted here as a future experiment, not wired: `ascent`'s generated code hashes relations in ways that would need an `Oid` newtype (rather than a bare `String`) to make bounded model checking of the rules themselves tractable, and that is out of scope for this migration. == 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. +Models are checked against `ents-gate-rules`, not the other way around — literally, now: `ents-verify` and `tests/prop.rs` both import `ents_gate_rules::gate` and call it. +The landing convention for a new finding stays the same as before this migration: a FALSIFIED or DIVERGED ledger row with a concrete, transaction-shaped counterexample lands in `crates/kernel/ents-gate-rules/tests/ledger.rs` first (gap-pinning while open), then — where the counterexample is transaction-shaped — loses its exemption in `tests/prop.rs` and its discovery in `ents-verify::search`, and only then becomes a denial rule, one rule at a time. -== Running the checkers +== Layering + +`crates/verify/ents-verify` is a sink in the workspace's crate layering (`docs/abstractions.adoc`'s "Layering" section): it depends on `ents-gate-rules` only, and nothing in the workspace may depend on it. +`crates/cli/git-ents/tests/layering.rs` enforces both directions mechanically. + +== Running the checks [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 +cargo test -p ents-gate-rules # the crate's own tests, plus tests/ledger.rs and tests/prop.rs +cargo test -p ents-verify # the search model's acceptance test (rediscovers the replay) ---- -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`. +`cargo test --workspace` runs both, since `ents-verify` and the `ents-gate-rules` test targets are ordinary workspace members — no separate CI job, no jar, no optional/skippable step.

verify/ledger.adoc @@ -4,6 +4,7 @@ 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). +The harness is Rust-native, and the `model` column names which check discharges each claim: `search` is crates/verify/ents-verify/src/search.rs's exhaustive bounded search calling `gate()` directly; `stateright` is crates/verify/ents-verify's `receive.rs`/`effects.rs`/`durability.rs` protocol-over-time skeletons; `proptest` is crates/kernel/ents-gate-rules/tests/prop.rs's cheap sampled floor; `alloy-paper` marks a claim demoted to verify/alloy/*.als as a paper-only design tool, no longer run in CI; and `—` means no model is assigned yet. 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`. @@ -11,167 +12,167 @@ |=== |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 |— +|A ref under `refs/meta/*` is simultaneously the unit of storage, sync, authorization, and history. |abstractions.adoc, §1 Meta-ref, ~L14-19 |alloy-paper |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. +|Trees stay pure struct representations — no version marker entry. |abstractions.adoc, §2 Typed tree, ~L39 |alloy-paper |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) |search, proptest |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 |— +|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-paper |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-paper |gap-unmarked |OPEN |— +|Redaction is the sole deliberate exception to retention. |abstractions.adoc, §3 Anchor, L54 |alloy-paper |gap-unmarked |OPEN |— +|Anchor data is never mutated. |abstractions.adoc, §3 Anchor, L55 |alloy-paper |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 |— +|Every meta-ref mutation is an author-signed commit. |abstractions.adoc, §4 Signed commit, L62 |search, proptest |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 |search |gap-unmarked |OPEN |— +|Push certificates are demoted to transport concerns; they carry no meta-ref semantics. |abstractions.adoc, §4 Signed commit, L64 |search |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-paper |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 |search |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 |search, proptest |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 |stateright |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 |stateright |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 |stateright |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 |search |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 |search |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 |stateright |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 |stateright |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 |stateright |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 |stateright |gap-unmarked |OPEN |— +|One function, three call sites: hosted CAS, local UI verdict, push pre-flight. |abstractions.adoc, §5 Gate, L110 |stateright |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 |— +|Results location is derived by convention; an effect cannot choose where its verdicts land. |abstractions.adoc, §6 Effect, L132 |alloy-paper |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 |stateright |gap-marked |OPEN |— +|Meta-refs are outside `rev()`'s domain by definition. |abstractions.adoc, §6 Effect, L138 |stateright |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 |stateright |gap-unmarked |OPEN |— +|`RefPattern` survives as the degenerate query `rev(<glob>)`; nothing shipped changes meaning. |abstractions.adoc, §6 Effect, L144 |stateright |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 |stateright |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 |stateright |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 |stateright |gap-marked |OPEN |— +|Result taxonomy: a result is `pass`, `fail`, or `error`; exit status is always a result. |abstractions.adoc, §6 Effect, L153-154 |stateright |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 |stateright |gap-unmarked |OPEN |— +|Retry bounds are deployment configuration, never effect data. |abstractions.adoc, §6 Effect, L156 |alloy-paper |gap-unmarked |OPEN |— +|A transient outage can neither retry forever nor permanently discharge an obligation. |abstractions.adoc, §6 Effect, L157 |stateright |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 |stateright |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 |stateright |gap-unmarked |OPEN |— +|Pushes are never blocked; the durable enqueue is the entire synchronous cost. |abstractions.adoc, §6 Effect, L167 |stateright |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 |— +|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-paper |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-paper |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-paper |gap-unmarked |OPEN |— +|No content predicates beyond `results(…, status)`, no time atoms, no external-event atoms. |abstractions.adoc, §6 Effect, L177 |stateright |gap-unmarked |OPEN |— +|Admin-only write rule on `refs/meta/effects/*` bounds who can schedule execution on canonical infrastructure. |abstractions.adoc, §6 Effect, L181 |search, proptest |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 |stateright |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 |— +|The unit the library exposes is `receive(refs, objects, events, proposal)`: gate evaluation, effect matching, enqueue live inside it. |abstractions.adoc, "Composition", L213 |stateright |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 |stateright |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 |— +|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-paper |gap-unmarked |OPEN |— +|Fanout index: a stale or absent index degrades to scanning ref tips, never to wrong answers. |abstractions.adoc, "Derived", L280 |stateright |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-paper |gap-unmarked |OPEN |— +|Redaction is enforced at ingest so content addressing cannot let anyone refill the hole exactly. |abstractions.adoc, "Derived", L283 |stateright |gap-unmarked |OPEN |— +|Readers surface a redaction marker, never an error. |abstractions.adoc, "Derived", L284 |alloy-paper |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 |— +|`git effect run` shares the identical materialization and sandbox path with the hosted worker. |abstractions.adoc, "Command surface", L324 |stateright |gap-unmarked |OPEN |— +|Every mutation frontend shares the identical `receive` with the hosted server. |abstractions.adoc, "Command surface", L324 |stateright |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 |stateright |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 |— +|Bootstrap gap: an empty member list admits every push so the first member can enroll. |abstractions.adoc, "Deployment", L365 |stateright |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-paper |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-paper |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-paper |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 |— +|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-paper |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 |search |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 |— +|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 |stateright |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 |stateright |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 |— +|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 |stateright |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 |search |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 |stateright |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-paper |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 |stateright |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 |search |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 |stateright |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 |stateright |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 |stateright |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 |— +|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-paper |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 |— +|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-paper |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-paper |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 |search |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 |stateright |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-paper |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-paper |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-paper |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-paper |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-paper |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-paper |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-paper |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 |search |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 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-paper |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 |stateright |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 |stateright |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 |stateright |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 |search |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 |stateright |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-paper |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 |— +|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-paper |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-paper |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-paper |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-paper |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-paper |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 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-paper |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-paper |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-paper |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-paper |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 |— +|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-paper |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 |— +|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 |stateright |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 |stateright |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 |stateright |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 |stateright |gap-unmarked |OPEN |— +|The fanout index "MUST NOT be addressable by any query atom at all". |docs/spec/query.adoc, [#query.meta], ~L82-91 |stateright |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 |stateright |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 |stateright |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 |stateright |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 |stateright |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 |stateright |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 |stateright |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 |search |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 |— +|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 |stateright |gap-unmarked |OPEN |— +|The worker MUST NOT share in-process state with `receive`. |docs/spec/roots.adoc, [#roots.hosted], ~L55-63 |stateright |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 |— +|Fetch authorization MUST be refname-keyed, using the same authorization model as write authorization. |docs/spec/roots.adoc, [#roots.fetch-auth], ~L160-167 |search |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-paper |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 |stateright |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 |stateright |gap-unmarked |OPEN |— |===

.github/workflows/CI.yml @@ -125,35 +125,6 @@ - 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/Cargo.toml @@ -8,5 +8,8 @@ [dependencies] ascent = { workspace = true } +[dev-dependencies] +proptest = { workspace = true } + [lints] workspace = true

crates/cli/git-ents/tests/layering.rs @@ -1,7 +1,10 @@ //! Mechanical check of the one-way crate layering documented in //! `docs/abstractions.adoc`'s "Layering" section: substrate -> kernel -> //! {forge, kiln} -> cli, with forge and kiln forbidden from depending on -//! each other. +//! each other. Extended with one more rule for `crates/verify/*` +//! (`verify/README.adoc`): that layer is a pure sink above everything +//! else — `ents-verify` may depend only on `ents-gate-rules`, and no +//! crate anywhere in the workspace may depend on `ents-verify`. //! //! The prose in `docs/abstractions.adoc` states the rule, but nothing //! stops a future `Cargo.toml` edit from quietly violating it (a kernel @@ -24,12 +27,15 @@ /// Layer rank for a workspace package, derived from the `crates/<layer>/*` /// prefix of its manifest path: substrate (0) -> kernel (1) -> -/// forge/kiln (2) -> cli (3). +/// forge/kiln (2) -> cli (3) -> verify (4). /// /// A dependency edge is only legal when the depending package's rank is /// greater than or equal to the depended-on package's rank — e.g. the CLI /// (3) may depend on `ents-forge` (2), but a kernel crate (1) may never -/// depend on a package crate (2). +/// depend on a package crate (2). `verify` sits at the top rank alone, so +/// this general rule already forbids every other layer from depending on +/// it; [`ents_verify_depends_only_on_ents_gate_rules`] adds the sharper +/// rule that its own outgoing edges are restricted too. fn layer_rank(package: &Package, workspace_root: &Utf8Path) -> u8 { let relative = package .manifest_path @@ -52,6 +58,7 @@ Some("kernel") => 1, Some("forge") | Some("kiln") => 2, Some("cli") => 3, + Some("verify") => 4, other => panic!( "{}'s manifest path {relative} has an unrecognized layer directory {other:?}", package.name @@ -111,6 +118,15 @@ if package.name == "ents-kiln" && dependency.name == "ents-forge" { kiln_depends_on_forge = true; } + + if package.name == "ents-verify" { + assert_eq!( + dependency.name, "ents-gate-rules", + "ents-verify (the verify/ layer's sink crate) may depend on ents-gate-rules only, \ + but its manifest also names {}", + dependency.name + ); + } } } @@ -123,3 +139,32 @@ "ents-kiln must not depend on ents-forge: they are sibling package crates" ); } + +/// `ents-verify` is a pure sink: nothing in the workspace may depend on +/// it. The general rank rule in [`dependencies_never_point_upward`] +/// already forbids this (every other layer ranks below `verify`), but +/// this test states the sink property directly against the real +/// dependency graph, rather than relying on that rank arithmetic alone. +/// +/// See `crates/kernel/ents-model` and the root `Cargo.toml` for the +/// self-verification this test is designed to catch: temporarily adding +/// `ents-verify` as a dependency of any other crate must fail this test. +#[test] +fn nothing_depends_on_ents_verify() { + let metadata = MetadataCommand::new() + .manifest_path(concat!(env!("CARGO_MANIFEST_DIR"), "/Cargo.toml")) + .no_deps() + .exec() + .expect("cargo metadata"); + + for package in metadata.workspace_packages() { + if package.name == "ents-verify" { + continue; + } + assert!( + package.dependencies.iter().all(|dependency| dependency.name != "ents-verify"), + "{} must not depend on ents-verify: verify/ is a sink layer nothing else may depend on", + package.name + ); + } +}

crates/kernel/ents-gate-rules/tests/ledger.rs @@ -10,6 +10,14 @@ //! 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. +//! +//! Where the counterexample is transaction-shaped like this one, the +//! same landing happens in two more places, all three updated together: +//! `tests/prop.rs`'s matching property loses its exemption branch (it +//! currently proves the exemption load-bearing by failing without it), +//! and `crates/verify/ents-verify/src/search.rs`'s matching +//! [`stateright::Property::always`] — which today has a discovery — is +//! expected to have none once the rule lands. use ents_gate_rules::{Facts, Role, gate};

crates/kernel/ents-gate-rules/tests/prop.rs @@ -1,0 +1,117 @@ +//! Property-based floor for the ledger's invariant claims +//! (`verify/ledger.adoc`): `proptest` samples `Facts` over a small +//! bounded domain — deliberately duplicated here from +//! `crates/verify/ents-verify`'s vocabulary rather than depending on +//! that crate, since the sink-layer rule in +//! `crates/cli/git-ents/tests/layering.rs` is one-way: nothing may +//! depend on `ents-verify`. +//! +//! Two properties below have no exemption — the rules that cover them +//! (`unsigned_violation`, `effect_admin_violation`) are believed sound. +//! The third carries the one *known* exemption in this crate: the +//! refname-binding gap (`verify/ledger.adoc`, DIVERGED row; +//! `docs/abstractions.adoc` §2). A naive "admitted implies bound +//! correctly" property would fail on every run while that gap is open; +//! the exemption proves it is load-bearing, not dead code, and per +//! `tests/ledger.rs`'s convention, gets deleted in the same commit that +//! adds `binding_violation`. + +use ents_gate_rules::{Facts, Role, gate}; +use proptest::prelude::*; + +/// The signed content's own declared kind — the same shadow annotation +/// `ents-verify`'s search model and `verify/alloy/gate_rules.als`'s +/// `kind` field use, kept outside `Facts` because its absence from the +/// crate's real vocabulary *is* the gap under test. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum Kind { + Comment, + Issue, + Effect, +} + +const ADMIN_KEY: &str = "key:admin"; +const MEMBER_KEY: &str = "key:m1"; + +const ISSUE_REF: &str = "refs/meta/issues/g"; +const COMMENT_REF: &str = "refs/meta/comments/g2"; +const EFFECT_REF: &str = "refs/meta/effects/x"; + +fn refs() -> impl Strategy<Value = &'static str> { + prop_oneof![Just(ISSUE_REF), Just(COMMENT_REF), Just(EFFECT_REF)] +} + +fn signers() -> impl Strategy<Value = Option<&'static str>> { + prop_oneof![Just(Some(ADMIN_KEY)), Just(Some(MEMBER_KEY)), Just(None)] +} + +fn kinds() -> impl Strategy<Value = Kind> { + prop_oneof![Just(Kind::Comment), Just(Kind::Issue), Just(Kind::Effect)] +} + +/// Build a genesis transaction — the only shape the binding gap +/// concerns, since binding is a claim about a fresh entity's placement +/// — from sampled atoms, alongside whether the doc's binding invariant +/// actually holds for this sample. +fn build(ref_name: &str, signer: Option<&str>, kind: Kind) -> (Facts, bool) { + let mut facts = Facts { + member: vec![(ADMIN_KEY.to_string(), Role::Admin), (MEMBER_KEY.to_string(), Role::Member)], + ..Facts::default() + }; + facts.ref_update = vec![(ref_name.to_string(), None, "g2".to_string())]; + if let Some(key) = signer { + facts.signed_by = vec![("g2".to_string(), key.to_string())]; + } + + let binding_holds = match kind { + Kind::Effect => ref_name.starts_with("refs/meta/effects/"), + Kind::Comment => ref_name.starts_with("refs/meta/comments/"), + Kind::Issue => ref_name.starts_with("refs/meta/issues/"), + }; + (facts, binding_holds) +} + +proptest! { + /// Ledger floor (abstractions.adoc §5 tip invariant, admission + /// half): an admitted genesis is signed by an enrolled member. No + /// exemption — `unsigned_violation` covers this today. + #[test] + fn admitted_genesis_is_signed(r in refs(), signer in signers(), kind in kinds()) { + let (facts, _binding_holds) = build(r, signer, kind); + if gate(facts).is_empty() { + prop_assert!(signer.is_some()); + } + } + + /// Ledger floor (abstractions.adoc §6 / effect.admin-only): an + /// admitted write to `refs/meta/effects/*` is admin-signed. No + /// exemption — `effect_admin_violation` covers this today. + #[test] + fn admitted_effects_write_is_admin_signed(signer in signers(), kind in kinds()) { + let (facts, _binding_holds) = build(EFFECT_REF, signer, kind); + if gate(facts).is_empty() { + prop_assert_eq!(signer, Some(ADMIN_KEY)); + } + } + + /// Ledger row (DIVERGED, `docs/abstractions.adoc` §2 / + /// `meta-ref.identity-binding`): an admitted genesis's refname + /// namespace should match its signed content's declared kind. + /// EXEMPTED while the gap is open — delete the early return (and + /// this comment) in the same commit that adds `binding_violation`, + /// per `tests/ledger.rs`'s gap-pinning convention. + #[test] + fn admitted_genesis_binds_its_namespace(r in refs(), signer in signers(), kind in kinds()) { + let (facts, binding_holds) = build(r, signer, kind); + if gate(facts.clone()).is_empty() && !binding_holds { + // KNOWN GAP (verify/ledger.adoc: DIVERGED). Keeping this + // branch, rather than deleting the property outright, is + // what proves the exemption is load-bearing: comment it out + // locally and this property fails immediately. + return Ok(()); + } + if gate(facts).is_empty() { + prop_assert!(binding_holds); + } + } +}

crates/verify/ents-verify/Cargo.toml @@ -1,0 +1,16 @@ +[package] +name = "ents-verify" +version = "0.0.0" +edition.workspace = true +publish.workspace = true +license.workspace = true + +[dependencies] +ents-gate-rules = { workspace = true } +stateright = { workspace = true } + +[dev-dependencies] +proptest = { workspace = true } + +[lints] +workspace = true

crates/verify/ents-verify/src/durability.rs @@ -1,0 +1,92 @@ +//! Phase 5 — durability ordering (`verify/exercise.md`, "Phase 5"), +//! replacing the deleted `verify/tla/Durability.tla`. +//! +//! SKELETON. Every action body is `todo!()`; filling in +//! [`Model::actions`] and [`Model::next_state`] for real is the human +//! exercise. +//! +//! 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 state and 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. + +#![expect(clippy::todo, reason = "Phase 5 skeleton — filling this in is the human exercise, not this scaffold's job")] + +use stateright::{Model, Property}; + +/// Durability state: which objects have reached durable storage, and +/// the ref store's current tips. SKELETON. +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] +pub struct State { + /// Objects durably written so far. + pub durable: Vec<&'static str>, + /// Current tip of each ref in `crate::REFS`, in the same order; + /// `None` means the ref is unborn. + pub refs: [Option<&'static str>; 4], +} + +/// Durability actions (`verify/exercise.md`, Phase 5): `ObjectWrite`, +/// `RefCAS`, `Crash` at any point. SKELETON. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum Action { + /// An object (or pack) reaches durable storage. + ObjectWrite, + /// The ref store compare-and-swaps a tip — the write-order question + /// this phase exists to settle lives here. + RefCas, + /// Crash at any point; recovery obligations follow from what + /// survives. + Crash, +} + +/// The Phase 5 durability model. SKELETON. +pub struct DurabilityModel; + +impl Model for DurabilityModel { + type State = State; + type Action = Action; + + fn init_states(&self) -> Vec<Self::State> { + vec![State::default()] + } + + fn actions(&self, _state: &Self::State, _actions: &mut Vec<Self::Action>) { + todo!("exercise: enumerate ObjectWrite/RefCas/Crash per verify/exercise.md Phase 5") + } + + fn next_state(&self, _last_state: &Self::State, _action: Self::Action) -> Option<Self::State> { + todo!("exercise: Phase 5's transition relation, including crash faults") + } + + fn properties(&self) -> Vec<Property<Self>> { + vec![ + // The invariant this phase exists to prove: no ref in the + // ref store points outside the durable object set. STATED + // here so the ledger row has a formal object to point at; + // NOT proved — the transition relation above is a stub, so + // checking this today says nothing. + Property::always("refs_point_durable", |_, _| true /* TODO(exercise) */), + ] + } +} + +#[cfg(test)] +mod tests { + use stateright::Checker; + + use super::*; + + /// Running this model requires [`Model::actions`] and + /// [`Model::next_state`], both `todo!()` until the human exercise + /// fills them in. Ignored so `cargo test --workspace` stays green + /// while the skeleton exists. + #[test] + #[ignore = "exercise stub: Phase 5's transition relation is unwritten"] + fn model_runs() { + let _ = DurabilityModel.checker().spawn_bfs().join(); + } +}

crates/verify/ents-verify/src/effects.rs @@ -1,0 +1,112 @@ +//! Phase 4 — effects (`verify/exercise.md`, "Phase 4"), replacing the +//! deleted `verify/tla/Effects.tla`, building on [`crate::receive`]'s +//! state. +//! +//! SKELETON. Every action body is `todo!()`; filling in +//! [`Model::actions`] and [`Model::next_state`] for real is the human +//! exercise. +//! +//! 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`' module docs mark the +//! cross-transaction dedup obligation as a deliberate gap — this model +//! is where that obligation lives. + +#![expect(clippy::todo, reason = "Phase 4 skeleton — filling this in is the human exercise, not this scaffold's job")] + +use stateright::{Model, Property}; + +/// Protocol state, extending [`crate::receive::State`] with effect +/// bookkeeping: which commits have entered the trigger set (§6), the +/// at-least-once delivery queue's dedup keys, and the result-ref writes +/// performed so far. SKELETON. +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] +pub struct State { + /// The Phase 3 protocol state this phase builds on. + pub receive: crate::receive::State, + /// Commits that have entered the trigger set (§6: "fires once per + /// commit that enters the set"). + pub triggered: Vec<&'static str>, + /// At-least-once delivery: dedup keys `(effect, refname, new_oid)` + /// currently enqueued. + pub queue: Vec<(&'static str, &'static str, &'static str)>, + /// Result-ref writes performed so far, keyed the same way as + /// [`Self::queue`]. + pub results: Vec<(&'static str, &'static str, &'static str)>, +} + +/// Protocol actions (`verify/exercise.md`, Phase 4): `RefAdvance`, +/// `TriggerEval`, `Enqueue`, `Execute`, `ResultPush`. SKELETON. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum Action { + /// A gated ref advance (reuses [`crate::receive::gate_admits`] when + /// composed with Phase 3). + RefAdvance, + /// A commit enters the trigger set (§6). The delete-and-repush + /// re-entry question — is triggering monotone? — lives here. + TriggerEval, + /// At-least-once enqueue of a dedup key. + Enqueue, + /// The executor runs an effect; may crash and restart (duplicate + /// delivery). + Execute, + /// Result write-back: a gated write like any other, by an executor + /// member key (`effect.results-writeback`). + ResultPush, +} + +/// The Phase 4 effects model. SKELETON. +pub struct EffectsModel; + +impl Model for EffectsModel { + type State = State; + type Action = Action; + + fn init_states(&self) -> Vec<Self::State> { + vec![State::default()] + } + + fn actions(&self, _state: &Self::State, _actions: &mut Vec<Self::Action>) { + todo!("exercise: enumerate RefAdvance/TriggerEval/Enqueue/Execute/ResultPush per verify/exercise.md Phase 4") + } + + fn next_state(&self, _last_state: &Self::State, _action: Self::Action) -> Option<Self::State> { + todo!("exercise: Phase 4's transition relation") + } + + fn properties(&self) -> Vec<Property<Self>> { + vec![ + // Obligation 1: the dedup key (effect, refname, new_oid) + // yields result-ref idempotency under duplicate delivery + // and executor crash-restart. + Property::always("exactly_once_observable_effect", |_, _| true /* TODO(exercise) */), + // Obligation 2: a ref deleted and re-pushed to the same oid + // — does the commit re-enter the trigger set? Defines + // whether triggers are monotone. + Property::always("trigger_set_monotone", |_, _| true /* TODO(exercise) */), + // Obligation 3: no sequence lets a non-admin cause execution + // of content they authored as an effect (composes with + // crate::search's binding_refname_recomputed property — + // this was the original cross-ref replay scenario). + Property::always("authorization_asymmetry", |_, _| true /* TODO(exercise) */), + ] + } +} + +#[cfg(test)] +mod tests { + use stateright::Checker; + + use super::*; + + /// Running this model requires [`Model::actions`] and + /// [`Model::next_state`], both `todo!()` until the human exercise + /// fills them in. Ignored so `cargo test --workspace` stays green + /// while the skeleton exists. + #[test] + #[ignore = "exercise stub: Phase 4's transition relation is unwritten"] + fn model_runs() { + let _ = EffectsModel.checker().spawn_bfs().join(); + } +}

crates/verify/ents-verify/src/lib.rs @@ -1,0 +1,128 @@ +//! Rust-native model checking for the formal stocktake (`verify/`, +//! `verify/exercise.md`): [`stateright`] models that call +//! [`ents_gate_rules::gate`] directly, so the refinement mapping between +//! model and code is the function call, not a hand-maintained +//! translation. +//! +//! This crate is a sink in the workspace's layering (`docs/abstractions. +//! adoc`'s "Layering" section, extended by `crates/cli/git-ents/tests/ +//! layering.rs`): it depends on [`ents_gate_rules`] and nothing else in +//! the workspace, and nothing in the workspace may depend on it. It +//! exists to be run by `cargo test -p ents-verify`, never linked into a +//! shipped binary. +//! +//! # Modules +//! +//! - [`search`] — the Phase 0.5 replacement: an exhaustive search over a +//! small bounded universe of transactions, checking that every +//! admitted transaction (`gate(facts).is_empty()`) also satisfies the +//! doc invariants the rules are supposed to encode. This is where the +//! cross-ref replay counterexample (ledger row: DIVERGED, +//! `docs/abstractions.adoc` §2) is rediscovered by search rather than +//! asserted by hand. +//! - [`receive`] — Phase 3 skeleton: state/action signatures for the +//! gate-and-receive protocol, with the gate-check action's enabling +//! condition wired to the real `gate()` call (the one deliberate +//! exception to "skeleton, not solution"). +//! - [`effects`] — Phase 4 skeleton: trigger/dedup/results state shape. +//! - [`durability`] — Phase 5 skeleton: crash/durability ordering. +//! +//! # The bounded universe +//! +//! Every model in this crate builds transactions from the same tiny, +//! fixed set of atoms — the Rust-native analogue of Alloy's scope +//! discipline (`verify/exercise.md`: "Alloy scopes of 4-6 atoms per +//! signature. Almost every bug in a system like this appears with two +//! members, two refs, three commits."). Keeping every model's universe +//! this small is what makes exhaustive search (Phase 0.5) and bounded +//! model checking (Phases 3-5) tractable at all. + +pub mod durability; +pub mod effects; +pub mod receive; +pub mod search; + +use ents_gate_rules::{Facts, Role}; + +/// The one admin-registered key in the bounded universe — the only +/// signer [`effect_admin_violation`](ents_gate_rules) and the +/// redaction-admin-only rule (`docs/spec/receive.adoc` +/// `receive.redaction-admin-only`) accept for their namespaces. +pub const ADMIN_KEY: &str = "key:admin"; +/// An ordinary enrolled, non-admin member key. +pub const MEMBER_KEY_1: &str = "key:m1"; +/// A second ordinary member key — the bounded universe's "two members" +/// atom, needed for adoption/divergence scenarios where a single key +/// isn't enough to tell two actors apart. +pub const MEMBER_KEY_2: &str = "key:m2"; + +/// Every key in the bounded universe, admin first. +pub const KEYS: [&str; 3] = [ADMIN_KEY, MEMBER_KEY_1, MEMBER_KEY_2]; + +/// The fixed role a key in the bounded universe carries. Roles are not +/// an independent search dimension here: enrolling a key is a single +/// fact (present or absent), never a choice of role, exactly so search +/// states can dedupe on plain sets instead of tracking role assignment +/// as extra state — [`ents_gate_rules::Role`] itself has no `Ord`, which +/// would otherwise complicate that dedup. +#[must_use] +pub fn role_of(key: &str) -> Role { + if key == ADMIN_KEY { + Role::Admin + } else { + Role::Member + } +} + +/// A hash-identified namespace (`docs/spec/meta-ref.adoc` +/// `meta-ref.identity-binding`) — genesis-oid binding, the shape +/// `issues/*` and `comments/*` share. +pub const ISSUE_REF: &str = "refs/meta/issues/g"; +/// The other hash-identified namespace in the bounded universe, kept +/// distinct from [`ISSUE_REF`] so a model can distinguish "which +/// hash-identified namespace" without adding a third dimension. +pub const COMMENT_REF: &str = "refs/meta/comments/g2"; +/// The admin-only namespace (`effect.admin-only`) — the one the crate's +/// `effect_admin_violation` rule protects, and the namespace the known +/// cross-ref replay counterexample targets. +pub const EFFECT_REF: &str = "refs/meta/effects/x"; +/// The one namespace `meta-ref.inbox` declares as an allowed *second* +/// image of an already-bound signed commit — Phase 2 obligation 2. +pub const INBOX_REF: &str = "refs/meta/inbox/m1/comments/g2"; + +/// Every refname in the bounded universe. +pub const REFS: [&str; 4] = [ISSUE_REF, COMMENT_REF, EFFECT_REF, INBOX_REF]; + +/// Object ids in the bounded universe: enough to build a genesis +/// (`g2`), a fast-forward advance of an existing tip (`g` -> `c1`), and +/// a two-parent merge that smuggles in an unrelated root (`z`) — the +/// three transaction shapes `ents_gate_rules`' own unit tests already +/// exercise by hand, plus two blobs for anchor/context retention. +pub const OIDS: [&str; 6] = ["g", "c1", "m", "z", "blob-a", "blob-ctx"]; + +/// The signed content's own kind, as the *author's* signed content +/// declares it — the derivation input `docs/abstractions.adoc` §2 says +/// the refname recomputes from. Deliberately absent from +/// [`ents_gate_rules::Facts`] itself: that absence is the gap under +/// test. Every model that checks the binding invariant carries this as a +/// shadow annotation alongside a built [`Facts`] value, never inside it, +/// exactly mirroring `verify/alloy/gate_rules.als`'s `kind` field. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)] +pub enum Kind { + /// The signed content is a comment (`docs/spec/model.adoc` + /// `model.comment`). + Comment, + /// The signed content is an issue (`model.issue`). + Issue, + /// The signed content is an effect definition (`model.effect- + /// definition`, `effect.admin-only`). + Effect, +} + +/// Enroll every key in [`KEYS`] into `facts.member`, at its fixed +/// [`role_of`]. Every model in this crate treats membership as +/// background, not a search dimension — Phase 3's `receive` skeleton is +/// where membership *lifecycle* (enrollment, revocation) belongs. +pub fn enroll_all(facts: &mut Facts) { + facts.member = KEYS.iter().map(|k| ((*k).to_string(), role_of(k))).collect(); +}

crates/verify/ents-verify/src/receive.rs @@ -1,0 +1,140 @@ +//! Phase 3 — gate and receive as a protocol (`verify/exercise.md`, +//! "Phase 3"), replacing the deleted `verify/tla/Receive.tla`. +//! +//! SKELETON, with one deliberate exception: [`gate_admits`] calls +//! [`ents_gate_rules::gate`] directly on a transaction's `Facts` — that +//! direct call *is* the refinement mapping this module's `GateCheck` +//! action would enable on, replacing what `Receive.tla`'s `GateAdmits` +//! transcribed by hand. Every other action body is `todo!()`; filling in +//! [`Model::actions`] and [`Model::next_state`] for real is the human +//! exercise, not this scaffold's job. +//! +//! 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. + +#![expect(clippy::todo, reason = "Phase 3 skeleton — filling this in is the human exercise, not this scaffold's job")] + +use ents_gate_rules::{Facts, gate}; +use stateright::{Model, Property}; + +/// `gate(facts) = {}`: the enabling condition a filled-in `GateCheck` +/// action would use. This is real code, not a stub — it is the seven +/// denial rules, called directly, standing in for `Receive.tla`'s +/// hand-transcribed `GateAdmits`. +#[must_use] +pub fn gate_admits(facts: Facts) -> bool { + gate(facts).is_empty() + // TODO(exercise): refname recomputation from signed content (the §4 + // binding rule ents-gate-rules omits; ledger row DIVERGED, + // crate::search::SearchModel's `binding_refname_recomputed` + // property) and the epoch rule (§5) are not part of `gate()`, so + // this enabling condition inherits both gaps. Phase 3 decides + // whether `ents-gate` proper's check composes in here. +} + +/// Protocol state (§5): the current tip of every ref in the bounded +/// universe (`crate::REFS`), the object set, enrolled members, and the +/// config ref's epoch. SKELETON — named for the exercise's obligations, +/// not yet wired to a transition relation. +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] +pub struct State { + /// Current tip of each ref in `crate::REFS`, in the same order; + /// `None` means the ref is unborn. + pub refs: [Option<&'static str>; 4], + /// Objects the store currently has. + pub objects: Vec<&'static str>, + /// Enrolled member keys. + pub members: Vec<&'static str>, + /// The config ref's epoch (§5: "the epoch-setting commit is the + /// first gated tip of the config ref"). + pub epoch: u32, +} + +/// Protocol actions (`verify/exercise.md`, Phase 3): `Propose`, +/// `GateCheck`, `CAS`, `AdoptMerge`, `SelfMerge`. SKELETON. +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +pub enum Action { + /// A writer proposes a transaction (two writers minimum, per the + /// exercise's model). + Propose, + /// The gate evaluates a proposed transaction; a filled-in + /// implementation enables this action exactly when [`gate_admits`] + /// holds for the proposal in play. + GateCheck, + /// Compare-and-swap the ref tip — the anti-replay mechanism §4 + /// relies on parent-hash freshness for. + Cas, + /// Adoption: contributor commit in ancestry, adopter signature at + /// tip, always a merge (never a rewrite). + AdoptMerge, + /// Two of one member's own machines racing a single-writer ref — + /// `docs/abstractions.adoc` §4's same-actor divergence. + SelfMerge, +} + +/// The Phase 3 protocol model. SKELETON. +pub struct ReceiveModel; + +impl Model for ReceiveModel { + type State = State; + type Action = Action; + + fn init_states(&self) -> Vec<Self::State> { + vec![State::default()] + } + + fn actions(&self, _state: &Self::State, _actions: &mut Vec<Self::Action>) { + todo!("exercise: enumerate Propose/GateCheck/Cas/AdoptMerge/SelfMerge per verify/exercise.md Phase 3") + } + + fn next_state(&self, _last_state: &Self::State, _action: Self::Action) -> Option<Self::State> { + todo!("exercise: Phase 3's transition relation, using gate_admits as GateCheck's enabling condition") + } + + fn properties(&self) -> Vec<Property<Self>> { + vec![ + // Obligation 1: "the tip of a meta-ref is signed by a + // member authorized for that refname" is preserved by every + // action — pay attention to SelfMerge (is the merge commit + // itself signed in the implementation? see ents-sync/src + // and ents-receive/src/reconcile.rs). + Property::always("tip_invariant_inductive", |_, _| true /* TODO(exercise) */), + // Obligation 2: adoption preserves the tip invariant, even + // when the contributor's commit is itself a merge of + // unauthorized commits. + Property::always("adoption_preserves_tip_invariant", |_, _| true /* TODO(exercise) */), + // Obligation 3: a replayed genesis against a not-yet-created + // ref is safe only in conjunction with Phase 2's binding + // totality — state the exact conjunction. + Property::always("anti_replay", |_, _| true /* TODO(exercise) */), + // Obligation 4: from an empty store, is there a state where + // the gate must read the epoch from a ref whose tip is not + // yet gated? Cite ents-gate/src/{config,policy}.rs. + Property::always("epoch_bootstrap", |_, _| true /* TODO(exercise) */), + // Obligation 5: a member valid at admission and revoked + // later — does naive re-verification of historical tips + // fail, and does the epoch mechanism actually prevent that? + Property::always("revocation", |_, _| true /* TODO(exercise) */), + ] + } +} + +#[cfg(test)] +mod tests { + use stateright::Checker; + + use super::*; + + /// Running this model requires [`Model::actions`] and + /// [`Model::next_state`], both `todo!()` until the human exercise + /// fills them in. Ignored so `cargo test --workspace` stays green + /// while the skeleton exists — the one permitted use of `#[ignore]` + /// in this codebase, because this is a declared stub, not a passed- + /// off result. + #[test] + #[ignore = "exercise stub: Phase 3's transition relation is unwritten"] + fn model_runs() { + let _ = ReceiveModel.checker().spawn_bfs().join(); + } +}

crates/verify/ents-verify/src/search.rs @@ -1,0 +1,393 @@ +//! Phase 0.5 — verify the verifier (`verify/exercise.md`, "Phase 0.5"), +//! replacing `verify/alloy/gate_rules.als`'s `check` commands with an +//! exhaustive [`stateright`] search over the crate's own vocabulary. +//! +//! `ents_gate_rules` can *evaluate* its seven denial rules over one +//! supplied transaction; it cannot search for the transaction nobody +//! thought of. This module runs that search: [`SearchModel`]'s states +//! are a transaction under construction, one choice at a time, over the +//! bounded universe in `crate::{REFS, OIDS, KEYS}` plus the shadow +//! [`Kind`](crate::Kind) annotation, and its six [`Property::always`] +//! obligations restate — independently, in hand-written Rust, not by +//! calling `gate` a second time — exactly the five doc invariants the +//! seven rules claim to cover, plus the refname-binding claim they do +//! not. A property's *discovery* is a transaction `gate` admits that +//! violates the corresponding independent check. +//! +//! # The bound, and why it stays this small +//! +//! A state is exactly five choices, made in a fixed order: refname, +//! transaction [`Shape`], [`Signer`], [`Retention`], and the new tip's +//! [`Kind`]. That is `4 x 4 x 3 x 4 x 3 = 576` leaf states — small enough +//! for [`Model::checker`] to explore exhaustively in well under a +//! second. A naive "add any single EDB atom from the domain" search (a +//! literal transcription of Alloy's relational style) was tried first +//! and rejected: with `parent`/`signed_by`/`anchor`/`context`/ +//! `object_exists` each ranging freely over `OIDS x OIDS` or `OIDS x +//! KEYS`, the reachable state count is the size of the powerset of every +//! possible atom, not the five-transaction-shapes count above — tens of +//! thousands of atoms' worth of subsets, intractable for exhaustive BFS. +//! [`Shape`] instead enumerates the four transaction shapes +//! `ents_gate_rules`' own unit tests already hand-build (creation, +//! fast-forward advance, non-fast-forward, and the second-root merge), +//! which is everything the seven rules' *logic* actually branches on; +//! membership is fixed background ([`crate::enroll_all`]) rather than a +//! search dimension, since membership *lifecycle* is Phase 3's concern +//! (`receive.rs`), not Phase 0.5's. + +use ents_gate_rules::{Facts, gate}; +use stateright::{Model, Property}; + +use crate::{ADMIN_KEY, Kind, MEMBER_KEY_1, REFS, enroll_all}; + +/// The shape of the proposed transaction — the one dimension along which +/// the seven denial rules' *logic* actually branches, standing in for +/// the full `parent`/`ref_update` relations' combinatorics. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum Shape { + /// `ref_update(r, None, new)` with `new` parentless: entity creation. + Genesis, + /// `ref_update(r, Some(old), new)` with `new` a descendant of `old` + /// via one intermediate commit — the admitted case. + FastForward, + /// `ref_update(r, Some(old), new)` with `new` unrelated to `old` — + /// `ff_violation`'s witness. + NonFf, + /// `ref_update(r, Some(old), new)` with `new` a merge of the + /// fast-forward chain and an unrelated parentless commit — + /// `second_root_violation`'s witness + /// (`ents_gate_rules::tests::merged_in_second_root_is_rejected`). + SecondRoot, +} + +/// All four transaction shapes, in a fixed enumeration order. +pub const SHAPES: [Shape; 4] = [Shape::Genesis, Shape::FastForward, Shape::NonFf, Shape::SecondRoot]; + +/// Who signs every commit the transaction introduces — one signer +/// applies uniformly to keep the state small; per-commit signer +/// variation is Phase 3's concern, not this search's. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum Signer { + /// Every introduced commit signed by [`ADMIN_KEY`]. + Admin, + /// Every introduced commit signed by [`MEMBER_KEY_1`]. + Member, + /// No introduced commit carries a signature. + Unsigned, +} + +/// All three signer choices, in a fixed enumeration order. +pub const SIGNERS: [Signer; 3] = [Signer::Admin, Signer::Member, Signer::Unsigned]; + +/// Whether the new tip carries anchor/context retention, and whether it +/// resolves — only meaningful for [`Shape::Genesis`] (a comment-shaped +/// creation); every other shape treats this as absent. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum Retention { + /// No anchor or context blob. + Absent, + /// Anchor and context present, both resolving. + Resolving, + /// Anchor and context present; the anchored blob does not resolve. + DanglingAnchor, + /// Anchor and context present; the context blob does not resolve. + DanglingContext, +} + +/// All four retention choices, in a fixed enumeration order. +pub const RETENTIONS: [Retention; 4] = + [Retention::Absent, Retention::Resolving, Retention::DanglingAnchor, Retention::DanglingContext]; + +/// All three [`Kind`] choices, in a fixed enumeration order. +pub const KINDS: [Kind; 3] = [Kind::Comment, Kind::Issue, Kind::Effect]; + +/// A transaction under construction: five independent choices, each +/// `None` until [`SearchModel::actions`] offers it. A state with every +/// field `Some` is complete; [`SearchModel::actions`] then offers +/// nothing further, so the search terminates at exactly 576 leaves. +#[derive(Clone, Debug, Default, PartialEq, Eq, Hash)] +pub struct State { + ref_name: Option<&'static str>, + shape: Option<Shape>, + signer: Option<Signer>, + retention: Option<Retention>, + kind: Option<Kind>, +} + +/// One choice, made against exactly one of [`State`]'s five `None` +/// fields, in the fixed order the field declarations above list. +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] +pub enum Action { + /// Choose the transaction's refname. + ChooseRef(&'static str), + /// Choose the transaction's [`Shape`]. + ChooseShape(Shape), + /// Choose the transaction's [`Signer`]. + ChooseSigner(Signer), + /// Choose the new tip's [`Retention`]. + ChooseRetention(Retention), + /// Choose the new tip's signed-content [`Kind`]. + ChooseKind(Kind), +} + +/// A fully-chosen transaction, built once all five [`State`] fields are +/// `Some` — the point at which the properties below have anything to +/// check. +pub struct Complete { + ref_name: &'static str, + shape: Shape, + signer: Signer, + retention: Retention, + kind: Kind, +} + +impl State { + /// `Some` once every field is chosen, `None` while the transaction + /// is still under construction — the properties below treat `None` + /// as vacuously satisfying every obligation, so no discovery is + /// reported before there is a whole transaction to judge. + fn complete(&self) -> Option<Complete> { + Some(Complete { + ref_name: self.ref_name?, + shape: self.shape?, + signer: self.signer?, + retention: self.retention?, + kind: self.kind?, + }) + } +} + +impl Complete { + /// Translate this transaction into `ents_gate_rules::Facts`, exactly + /// as a real extractor would for each shape — same commit oids and + /// structure the crate's own unit tests build by hand. + fn to_facts(&self) -> Facts { + let mut f = Facts::default(); + enroll_all(&mut f); + + let signed_key = match self.signer { + Signer::Admin => Some(ADMIN_KEY), + Signer::Member => Some(MEMBER_KEY_1), + Signer::Unsigned => None, + }; + let sign = |f: &mut Facts, oid: &str| { + if let Some(k) = signed_key { + f.signed_by.push((oid.to_string(), k.to_string())); + } + }; + + match self.shape { + Shape::Genesis => { + f.ref_update = vec![(self.ref_name.to_string(), None, "g2".to_string())]; + sign(&mut f, "g2"); + match self.retention { + Retention::Absent => {} + Retention::Resolving => { + f.anchor = vec![("g2".to_string(), "blob-a".to_string())]; + f.context = vec![("g2".to_string(), "blob-ctx".to_string())]; + f.object_exists = vec![("blob-a".to_string(),), ("blob-ctx".to_string(),)]; + } + Retention::DanglingAnchor => { + f.anchor = vec![("g2".to_string(), "blob-a".to_string())]; + f.context = vec![("g2".to_string(), "blob-ctx".to_string())]; + f.object_exists = vec![("blob-ctx".to_string(),)]; + } + Retention::DanglingContext => { + f.anchor = vec![("g2".to_string(), "blob-a".to_string())]; + f.context = vec![("g2".to_string(), "blob-ctx".to_string())]; + f.object_exists = vec![("blob-a".to_string(),)]; + } + } + } + Shape::FastForward => { + f.ref_update = vec![(self.ref_name.to_string(), Some("g".to_string()), "c1".to_string())]; + f.parent = vec![("c1".to_string(), "g".to_string())]; + sign(&mut f, "g"); + sign(&mut f, "c1"); + } + Shape::NonFf => { + f.ref_update = vec![(self.ref_name.to_string(), Some("g".to_string()), "x".to_string())]; + sign(&mut f, "x"); + } + Shape::SecondRoot => { + f.ref_update = vec![(self.ref_name.to_string(), Some("g".to_string()), "m".to_string())]; + f.parent = vec![ + ("c1".to_string(), "g".to_string()), + ("m".to_string(), "c1".to_string()), + ("m".to_string(), "z".to_string()), + ]; + for oid in ["g", "c1", "m", "z"] { + sign(&mut f, oid); + } + } + } + f + } + + /// `gate(facts).is_empty()` for this transaction — the enabling + /// condition every property below is stated as a consequent of. + fn admitted(&self) -> bool { + gate(self.to_facts()).is_empty() + } + + /// abstractions.adoc §4 / gate.adoc: an admitted advance descends + /// from its old tip. [`Shape::NonFf`] is the sole shape that + /// violates this; every other shape satisfies it by construction. + fn ff_holds(&self) -> bool { + !matches!(self.shape, Shape::NonFf) + } + + /// abstractions.adoc §2 / meta-ref.identity-binding's all-roots + /// walk: an admitted advance introduces no second parentless commit. + /// [`Shape::SecondRoot`] is the sole shape that violates this. + fn single_root_holds(&self) -> bool { + !matches!(self.shape, Shape::SecondRoot) + } + + /// abstractions.adoc §5 tip invariant, admission half: every commit + /// an admitted transaction introduces is signed by an enrolled + /// member. + fn tip_signed_holds(&self) -> bool { + !matches!(self.signer, Signer::Unsigned) + } + + /// abstractions.adoc §3 / anchor.retention: an admitted genesis's + /// anchor and context both resolve. Only [`Shape::Genesis`] carries + /// retention in this model; every other shape is vacuously fine. + fn retention_holds(&self) -> bool { + if !matches!(self.shape, Shape::Genesis) { + return true; + } + !matches!(self.retention, Retention::DanglingAnchor | Retention::DanglingContext) + } + + /// abstractions.adoc §6 / effect.admin-only: an admitted write to + /// the effects namespace is admin-signed. + fn effect_admin_holds(&self) -> bool { + if !self.ref_name.starts_with("refs/meta/effects/") { + return true; + } + matches!(self.signer, Signer::Admin) + } + + /// abstractions.adoc §2 / meta-ref.identity-binding: the refname's + /// namespace matches the signed content's own declared + /// [`Kind`](crate::Kind) — the claim ledger row DIVERGED covers. Only + /// engages at [`Shape::Genesis`]: binding is a claim about a fresh + /// entity's placement, not about advancing one that already exists. + /// [`crate::INBOX_REF`] is deliberately outside this model's binding + /// scope (Phase 2 obligation 2's allowed second image, not a fresh + /// binding decision), so it always holds trivially here. + fn binding_holds(&self) -> bool { + if !matches!(self.shape, Shape::Genesis) { + return true; + } + let expected = if self.ref_name.starts_with("refs/meta/effects/") { + Kind::Effect + } else if self.ref_name.starts_with("refs/meta/comments/") { + Kind::Comment + } else if self.ref_name.starts_with("refs/meta/issues/") { + Kind::Issue + } else { + return true; + }; + self.kind == expected + } +} + +/// The Phase 0.5 search model. Stateless: every choice comes from the +/// bounded universe in `crate`, not from any field here. +pub struct SearchModel; + +impl Model for SearchModel { + type State = State; + type Action = Action; + + fn init_states(&self) -> Vec<Self::State> { + vec![State::default()] + } + + fn actions(&self, state: &Self::State, actions: &mut Vec<Self::Action>) { + if state.ref_name.is_none() { + actions.extend(REFS.iter().map(|r| Action::ChooseRef(r))); + } else if state.shape.is_none() { + actions.extend(SHAPES.iter().map(|s| Action::ChooseShape(*s))); + } else if state.signer.is_none() { + actions.extend(SIGNERS.iter().map(|s| Action::ChooseSigner(*s))); + } else if state.retention.is_none() { + actions.extend(RETENTIONS.iter().map(|r| Action::ChooseRetention(*r))); + } else if state.kind.is_none() { + actions.extend(KINDS.iter().map(|k| Action::ChooseKind(*k))); + } + // A complete state (every field `Some`) offers nothing further: + // this is a leaf, and the search terminates there. + } + + fn next_state(&self, last_state: &Self::State, action: Self::Action) -> Option<Self::State> { + let mut state = last_state.clone(); + match action { + Action::ChooseRef(r) if state.ref_name.is_none() => state.ref_name = Some(r), + Action::ChooseShape(s) if state.ref_name.is_some() && state.shape.is_none() => state.shape = Some(s), + Action::ChooseSigner(s) if state.shape.is_some() && state.signer.is_none() => state.signer = Some(s), + Action::ChooseRetention(r) if state.signer.is_some() && state.retention.is_none() => { + state.retention = Some(r); + } + Action::ChooseKind(k) if state.retention.is_some() && state.kind.is_none() => state.kind = Some(k), + _ => return None, + } + Some(state) + } + + fn properties(&self) -> Vec<Property<Self>> { + /// `gate(facts).is_empty()` implies `check(complete)`, vacuously + /// true on an incomplete state — one property per doc invariant + /// the seven denial rules claim to cover, named to match + /// `verify/alloy/gate_rules.als`'s `check` commands one-to-one. + fn implication(state: &State, check: fn(&Complete) -> bool) -> bool { + state.complete().is_none_or(|c| !c.admitted() || check(&c)) + } + + vec![ + Property::always("ff_only_advance", |_, s| implication(s, Complete::ff_holds)), + Property::always("single_root_identity", |_, s| implication(s, Complete::single_root_holds)), + Property::always("introduced_commits_member_signed", |_, s| { + implication(s, Complete::tip_signed_holds) + }), + Property::always("anchor_retention_resolves", |_, s| implication(s, Complete::retention_holds)), + Property::always("effects_writes_admin_signed", |_, s| { + implication(s, Complete::effect_admin_holds) + }), + // The one property expected to have a discovery: the known, + // ledger-recorded DIVERGED gap. See tests::rediscovers_cross_ref_replay_by_search. + Property::always("binding_refname_recomputed", |_, s| implication(s, Complete::binding_holds)), + ] + } +} + +#[cfg(test)] +mod tests { + use stateright::Checker; + + use super::*; + + /// The migration's acceptance test: search, not hand-construction, + /// rediscovers the cross-ref replay (ledger row DIVERGED, + /// `docs/abstractions.adoc` §2). Every other property must have no + /// discovery — the seven rules are faithful to the other five doc + /// invariants within this bounded universe. + #[test] + fn rediscovers_cross_ref_replay_by_search() { + let checker = SearchModel.checker().spawn_bfs().join(); + + let path = checker.assert_any_discovery("binding_refname_recomputed"); + // Printed so a run's witness can be copied into the PR + // description as confirmation the harness has teeth. + println!("binding_refname_recomputed witness: {:?}", path.into_actions()); + + checker.assert_no_discovery("ff_only_advance"); + checker.assert_no_discovery("single_root_identity"); + checker.assert_no_discovery("introduced_commits_member_signed"); + checker.assert_no_discovery("anchor_retention_resolves"); + checker.assert_no_discovery("effects_writes_admin_signed"); + } +}

verify/alloy/README.adoc @@ -1,0 +1,5 @@ += alloy/: paper tool only + +These three `.als` files are kept as a design-only paper tool for Phases 1 and 2's structural questions (object graph reachability, refname binding) — nothing here runs in CI. +`crates/verify/ents-verify` and `crates/kernel/ents-gate-rules/tests/prop.rs` are the harness that actually runs, calling `ents_gate_rules::gate` directly instead of a hand-maintained Alloy translation of it. +If a human works through Phase 1 or Phase 2 by hand and wants small-scope model finding to double-check a step, the Alloy Analyzer can still open these files directly; see `verify/README.adoc` for the fuller epistemic split.

verify/bin/check-alloy @@ -1,60 +1,0 @@ -#!/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,56 +1,0 @@ -#!/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/tla/Durability.cfg @@ -1,8 +1,0 @@ -\* 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,72 +1,0 @@ ---------------------------- 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,9 +1,0 @@ -\* 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,106 +1,0 @@ ----------------------------- 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,11 +1,0 @@ -\* 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,195 +1,0 @@ ----------------------------- 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 - -=============================================================================