Review Summary: The Transaction Graph for Modeling Blockchain Semantics

Review Summary
‡ The Transaction Graph for Modeling Blockchain Semantics. [PDF]
Christian Cachin (University of Bern), Angelo De Caro (IBM Zurich), Pedro Moreno-Sanchez (TU Wien), Bjoern Tackmann (DFINITY), Marko Vukolic (IBM Zurich)
(‡ accepted for both conference and journal)

Paper summaries from the reviewers:
“The paper models blockchain transactional semantics as directed acyclic graphs. It describes two types of vertices - states and witnesses - as well as three types of edges: consuming, producing, and observing. It then proceeds to define transactions and the transaction graph (TDAG). The transaction graph is a high-level model of transaction interdependencies in a blockchain. It contains a unique genesis state and transaction. New transactions may be appended to a transaction graph, and two graphs may be composed (primarily by composing their genesis transactions). The authors introduce generalized concepts of consistency and validity as functions on transactions within a graph, and show that any valid transaction graph satisfies these definitions, and that the composition of two valid transactions graphs satisfy them as well.”

“The paper presents a formal model for transaction semantics, built on seven simple definitions. It presents two theorems supported by straightforward proofs that build logically from the definitions. The appendices apply these to existing blockchains, and show that the transaction graph effectively models concrete systems.”

Comments on the strength of the paper:
“The paper offers an incredibly useful tool for reasoning about transaction semantics, and gives proofs of its properties, as well as practical instantiations of the model. The description of Bitcoin's transaction graph formalizes and expands a mental model common to Bitcoin engineers.”

“In an appendix, the authors apply the model to Bitcoin and Hyperledger Fabric, including in-depth discussion of the systems' respective validity rules. They show that the graph can be used to reason about whether validity rules successfully produce the chain's desired invariant properties (e.g. Bitcoin's fixed supply).”

Critiques:
“The model is less useful for reasoning about richly stateful systems as (in most state models) a transaction's input state set, output state set, and edge set are all unknown until it is applied to an existing TDAG. For example, Ethereum transactions never satisfy Definition 1. The practical exception is Nervos, in which transactions explicitly lists input states.”

“The authors mention existing work on Bitcoin-specific transaction semantics (Balzac), but do not go out of their way to explain how their model relates to that work. Generally, the transactions in this work can be seen as a generalization of Balzac that captures non-Bitcoin semantics, and Balzac could be adapted to express arbitrary transaction graphs. It would be interesting to see discussions of other work (e.g. Balzac and BitML) as high-level descriptions of sets of transactions coupled with validity rules.”

“Nit: The hash element of the Bitcoin state tuple does not accurately reflect the behavior of Bitcoin, and does not seem to uniquely identify state vertices in the graph. What purpose does the hash element of the tuple serve in the model?”

“Nit: the gas-price element of the Ethereum state tuple does not reflect Ethereum's ‘gasPrice’ semantics. The gas-price should be an element of the witness, not each state, as ‘gasPrice’ is (like ‘gasLimit’) invariant through the transaction rather than localized to the account.”