transaction-protocol-reasoning

# Transaction Protocol Reasoning Use this skill when **a protocol is already given** (paper, spec, pseudocode, implementation notes) and you need to understand what it guarantees and how its rules imply commit/abort behavior. This skill does **not** ask you to invent a protocol. It teaches how to read a protocol description as a set of rules, turn those rules into checkable predicates/invariants, and then reason about safety vs conservatism. ## What “done” looks like By the end you should have: - a one-page **Protocol Ledger** (state + rules + invariants) - a minimal **example pack** (3–6 tiny histories) that exercises boundaries - a clear statement of: - the protocol’s **proof object** (what metadata it relies on), and - its likely **false-abort** and **unsafe-commit** failure modes ## Quick Reference (pick the next file to read) | If you need… | Read | |---|---| | A step-by-step protocol reading workflow | [protocol-analysis-workflow.md](references/protocol-analysis-workflow.md) | | Inventory protocol state + what each field proves | [state-and-metadata-modeling.md](references/state-and-metadata-modeling.md) | | Restate read/write/validate/commit/abort as explicit rules | [operation-rule-analysis.md](references/operation-rule-analysis.md) | | Extract invariants from rules (and distinguish conservative ones) | [invariant-extraction.md](references/invariant-extraction.md) | | Build a small history suite that hits boundary behavior | [example-construction.md](references/example-construction.md) | | Build minimal counterexamples (unsafe commit vs conservative abort) | [counterexample-construction.md](references/counterexample-construction.md) | | Compare two protocols by guarantees + metadata + allowed histories | [protocol-comparison.md](references/protocol-comparison.md) | ## Protocol Ledger (the “shape ledger” equivalent) Before you chase details, build a one-page protocol ledger: ```text Claimed guarantee: Global state: - per-object metadata: ... - global clock/counters: ... Per-transaction state: - read set entries: (key, version-id?, local ts fields?, ...) - write set entries: (key, buffered value?, lock?, ...) - timestamps: start_ts?, commit_ts?, bounds? Operations (as rules/predicates): read(key): preconditions, version selection, metadata recorded/updated, failure modes write(key): ... validate(txn): ... commit(txn): ... abort/retry(txn): ... Proof object: - what metadata/rules constitute the correctness argument? - what does the protocol “check” to justify commits? ``` If you cannot fill a ledger line item without hand-waving (“it probably…”), you have found an underspecified part of the protocol. That is often where conservative aborts come from. ## Workflow (operational) 1. **Extract the contract**: what does “correct” mean and what is in-scope? 2. **Inventory state**: list each field, its scope, and what history fact it is intended to prove. 3. **Restate rules**: convert prose/pseudocode into explicit “if … then … else abort/block” rules. 4. **Derive invariants**: state what must always be true if the rules are correct. 5. **Run the example pack**: step through 3–6 tiny histories and apply the rules mechanically. 6. **Locate conservative vs unsafe edges**: - conservative: rules reject a safe history (false abort / blocking) - unsafe: rules accept a history that violates the contract ## Common Failure Modes To Look For - **Metadata insufficiency**: protocol needs old-version validity but stores only latest. - **Scope mismatch**: uses per-key evidence to enforce cross-key ordering claims. - **Over-approx validation**: uses a sufficient condition (safe) that is not necessary (causes false aborts).