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
Inventory protocol state + what each field proves	state-and-metadata-modeling.md
Restate read/write/validate/commit/abort as explicit rules	operation-rule-analysis.md
Extract invariants from rules (and distinguish conservative ones)	invariant-extraction.md
Build a small history suite that hits boundary behavior	example-construction.md
Build minimal counterexamples (unsafe commit vs conservative abort)	counterexample-construction.md
Compare two protocols by guarantees + metadata + allowed histories	protocol-comparison.md

Protocol Ledger (the “shape ledger” equivalent)

Before you chase details, build a one-page protocol ledger:

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).