Pith. sign in

REVIEW 3 major objections 7 minor 30 references

Properties of UTxO Ledgers and Programs Implemented on Them

T0 review · 3 major / 7 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper establishes a category-theoretic framework in which a stateful smart contract implemented on a UTxO ledger induces a non-expanding map from valid ledger traces to contract traces, making every contract safety property a ledger…

desk verdict Trace-mapping lemma is a keeper, but the Section 5 theorems need an explicit hash-injectivity axiom and tighter proofs. read the letter →

arxiv 2506.05832 v1 pith:UOHEENCN submitted 2025-06-06 cs.LO

Polina Vinogradova (Input Output Global) , Alexey Sorokin (Input Output Global) This is my paper
classification cs.LO
keywords UTxOledgersmartcontractstracesafetyultrametricspacesimplegraphsieve-definedhomomorphismcategorytheorytransactioncommutativity
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper gives a mathematical framework for saying when a stateful smart contract is correctly implemented on a UTxO ledger, and for transferring safety guarantees from the contract to the ledger. Valid ledger executions are represented as infinite paths in a simple graph, and valid contract executions the same; the implementation relation is a partial sieve-defined graph homomorphism that preserves initial states. Paths in these graphs carry a natural ultrametric, and the paper proves that every structured contract induces a non-expanding (hence continuous) map from ledger traces to contract traces. Because continuous preimages of closed sets are closed, and safety properties are exactly closed sets of traces, every safety property of the contract is automatically a safety property of the ledger. The paper also proves three concrete ledger safety properties in this framework: replay protection, trivial update protection, and transaction commutativity.

What carries the argument

The central object is the category $\mathrm{Graph}^{\sharp}_{*}$ of simple graphs with distinguished initial vertices, whose morphisms are partial sieve-defined homomorphisms (maps whose domain is upward closed: any edge starting in the domain ends in the domain). In this category, an infinite path in a graph is a morphism from the graph $\mathbb{N} = 0 \to 1 \to 2 \to \cdots$ with initial vertex $0$; the set of such paths carries the ultrametric $d(\vec a, \vec b) = \inf\{2^{-k} \mid a_k \neq b_k\}$. The paper shows the path-space functor factors through $\mathrm{UMet}$ (ultrametric spaces and non-expanding maps), and the trace-mapping lemma is the commutative square induced by a structured contract. The sieve condition is what makes the map well-defined on valid traces: once a trace starts inside the defined domain, it stays there.

What would settle it

Take the hash function $h$ in the LEDGER specification to be a non-injective function with a known collision (for instance, one that discards all but one byte of the transaction encoding). Then run the transition system on a well-founded initial state with two distinct transactions that produce the same hash; if the final state depends on the order in which they are applied, Theorem 5.2.1 fails, and if the same transaction hash appears twice in a valid trace, Theorem 5.1.1's conclusion is violated.

Watch

Extended reading notes

Core claim

The central discovery is the trace-mapping lemma (Corollary 4.4.6): a structured contract $\pi: \mathrm{Trc}(\mathrm{LEDGER}) \to \mathrm{Trc}(\mathrm{STRUC})$ between ultrametric spaces. This makes the ledger trace space an ultrametric refinement of the contract trace space, so any closed subset of contract traces—a safety property—pulls back to a closed subset of ledger traces. The paper constructs the category $\mathrm{Graph}^{\sharp}_{*}$ whose objects are simple graphs with distinguished initial vertices and whose morphisms are partial sieve-defined homomorphisms, and shows the representable functor $(\mathbb{N}, -)$ factors through the category of ultrametric spaces and non-expanding maps. It then proves that the property of being a valid ledger trace is a safety property, and derives replay protection, trivial update protection, and transaction commutativity for well-founded UTxO states, assuming injectivity of the output-reference hash function.

Load-bearing premise

The ledger-safety theorems hold only under the unstated assumption that the hash function $h$ identifying transaction outputs is injective, which is false for real cryptographic hashes.

Editorial extensions

If this is right

  • Any safety property (closed set of valid traces) of a correctly implemented contract is automatically a safety property of the valid ledger traces that run it.
  • Replay protection holds: no two steps of a valid trace can use the same transaction, assuming the hash function is injective.
  • Trivial update protection holds: no valid trace revisits a ledger state, under the same assumption.
  • UTxO transaction commutativity holds: applying any valid permutation of a set of transactions to a well-founded initial state yields the same final state.
  • The structured-contract implementation obligation, which previously only certified single steps, now extends to whole infinite executions.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the injectivity assumption is dropped (as it must be for real cryptographic hashes), replay protection, trivial update protection, and commutativity can fail: a hash collision can make two distinct transactions indistinguishable by output reference, letting an attacker replay a transaction or produce a state change that the safe-hash proofs exclude.
  • The category-theoretic setting suggests a uniform way to compose implementations: if contract A is implemented on the ledger and contract B is implemented on A's state space, the composition should induce a non-expanding map between trace spaces, giving a compositional safety-transfer theorem not stated in the paper.
  • The same ultrametric trace machinery could be instantiated for account-based ledgers by changing the underlying state transition graph; the safety-pullback lemma would transfer, though the ledger-specific properties like commutativity would not.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 7 minor

Summary. The paper develops a formal framework for reasoning about valid execution traces of Extended UTxO (EUTxO) ledgers and of stateful programs implemented on them via structured contracts. It defines a category Graph♯_* of simple graphs with distinguished initial vertices and partial sieve-defined homomorphisms, shows that infinite paths in such graphs form ultrametric spaces, and proves that morphisms induce non-expanding maps between path spaces. The main advertised consequences are a trace-mapping lemma (Corollary 4.4.6), which transfers safety properties from a structured contract's trace space to the ledger's trace space, and concrete ledger safety properties: replay protection, trivial update protection, and transaction commutativity (Theorems 5.1.1 and 5.2.1).

Significance. If the framework is made fully rigorous, the paper offers a useful bridge between small-step ledger semantics, trace-based program analysis, and categorical/topological language. The construction of sieves and the composition lemma are clearly presented, and the non-expanding map argument is straightforward and sound once the morphism is well defined. The safety-transfer idea is the right high-level contribution: a closed property of contract traces pulls back to a closed property of ledger traces. However, the main safety theorems currently rest on unstated assumptions about hash injectivity and about the well-definedness of the ledger update operation, so the paper's central claims are conditional as written.

major comments (3)
  1. [§2.2, Eq. (1); §4.3] The ledger transition relation is not well-defined as stated. In ApplyTx, u′ is defined as (u \ getORefs(t)) ∪ mkOuts(t), but if mkOuts(t) contains an output reference already present in u and not among the consumed inputs, the result is not a finite map: the union places two bindings at the same key. Hash injectivity alone does not prevent this, since a transaction can be valid by checkTx even if its output references collide with existing unspent outputs from a previous application of the same transaction. The sentence in §4.3, 'The constructed graph Λ is simple, as u′ is uniquely defined,' is exactly the condition that needs to be proved or assumed. Because Trc(LEDGER) is defined through paths in Λ, the trace-mapping lemma (Corollary 4.4.6) and the entire Graph♯_* model are conditional on an unstated freshness/collision-freeness axiom for output references. I recommend adding an explicit axiom that (u \ getORefs(t)) ∩ mkOuts(t) = ∅, or stating h is injective and adding a disjointness condition, before the definition of LEDGER.
  2. [§5.1, Theorem 5.1.1] Theorem 5.1.1 is stated without an injectivity hypothesis, but its proof uses injectivity of h in both Claim 1 and Claim 2 ('by the injectivity of h'). Corollary 5.1.2 then begins with 'If h : Tx → ByteString is injective', which makes the corollary conditional while the theorem is not. Since real cryptographic hash functions are not injective, the theorem as stated is not supported by the proof. The statement should either include injectivity of h as an explicit hypothesis or replace it with the output-reference freshness axiom. Additionally, the proof of part (b) contains an indexing error: the line 'If c_j ∩ c_l ≠ ∅, where 0 ≤ l ≤ i−1, then t_j = t_l' should refer to c_{j−1} and t_{j−1}; as printed it is inconsistent with the surrounding argument.
  3. [§5.2, proof of Theorem 5.2.1] The commutativity proof has a gap in the contradiction argument. After defining u∪ and r, the proof says that if a ∉ un but a ∈ u′_n, then 'a must have been re-added by another tk'. This is not justified: a might simply never have been consumed in the second ordering, while being consumed in the first ordering. The real contradiction is that the same spending transaction appears in both multisets, so it must consume a in any valid ordering, making it impossible for a to survive to the final state unless the same output reference is recreated by another transaction, which is excluded by injectivity. The proof should be rewritten to argue directly from the common multiset of transactions and Corollary 5.1.2 rather than from the unstated re-adding step.
minor comments (7)
  1. [§1, contribution list] The enumerated list jumps from item (iii) to item (v); the missing item (iv) should be restored or the numbering should be corrected.
  2. [Figure 2] The definition of mkOuts writes the output reference as (tx, ix), but the text and Section 5 correctly use (h(tx), ix). The figure should be corrected to match the surrounding formalization.
  3. [§2.2] There are typographical errors, e.g., 'can can only' and 'of a a', which should be cleaned up.
  4. [§5.1, Corollary 5.1.2] The inequality 'for any k ≤ 0' should read 'for any k ≥ 0'.
  5. [§5.2, Example 5.2.2] The line 'r6 ⊆ (u0 ⊔ c012345) ∩ (u0 ⊔ c13) = u0 ⊔ c13' is repeated, and 'Indeces' should be 'Indices'.
  6. [Remark 4.2.3] 'we identity (N, G) with' should be 'we identify (N, G) with'.
  7. [Corollary 4.4.6] The symbol π is used both for the structured-contract projection π : UTxO ⇀ State and for the induced trace map π : Trc(LEDGER) → Trc(STRUC). Using different notation for the trace map would improve readability.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation: the trace-mapping theorem is a formal consequence of the structured-contract definition, with only a non-circular correctness gap about unstated hash injectivity.

full rationale

The paper's central derivation is a logical consequence of its explicit definitions, not a restatement of them. Definition 2.3.1 (structured contract) is taken from the authors' prior work [30], but it is reproduced in full in the paper: (STRUC, π, κ) is a structured contract exactly when every LEDGER transition starting in Def π is matched by a STRUC transition. Section 4 constructs the graphs Λ and Γ and the projection morphisms explicitly; Lemma 4.4.5 and Corollary 4.4.6 then show, by the induced postcomposition functor, that a structured contract yields a non-expanding map Trc(LEDGER) → Trc(STRUC). The non-expanding property is not assumed; it is proved from the ultrametric and from the fact that f∗ applies f pointwise to paths (Proposition 4.4.4). Safety transfer is then the standard topological fact that preimages of closed sets under continuous/non-expanding maps are closed. The only self-citations ([10], [19], [30]) provide the ledger and contract formalism, but the needed definitions and equations are restated in this paper, so the argument does not reduce to the citations. There is a genuine correctness gap: the proofs of replay protection and transaction commutativity invoke injectivity of the hash function h, which is not stated as a hypothesis of Theorem 5.1.1, and the well-definedness of the graph Λ also silently relies on collision-freeness of output references; this is a missing assumption, not a circular step. No fitted parameter is renamed as a prediction, and no claimed result is defined into existence.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The framework introduces new mathematical constructs, such as partial sieve-defined homomorphisms and the category Graph♯*, but these are definitions rather than posited physical or ontological entities. The central proofs rest on the three domain assumptions listed above, especially the injective-hash assumption, which is not flagged in the main theorem statement.

assumptions (3)
  • domain assumption Hash function h : Tx -> ByteString is injective.
    Used in Claims 1-2 of Theorem 5.1.1, Corollary 5.1.2, and Theorem 5.2.1 to identify transactions from output-reference hashes. Not stated as a hypothesis in Theorem 5.1.1, and real hash functions are not injective.
  • domain assumption UTxO is well-founded: every entry in an initial state u0 originates from a transaction with an empty input list.
    Assumed at the start of Section 5 (page 13) and used in Claim 1 of Theorem 5.1.1 to show that the initial UTxO set is disjoint from all later transaction outputs.
  • domain assumption The domain of the projection map π is a sieve in the ledger graph (once a ledger state is in Def π, all successors are too).
    This follows from equation (2) in Definition 2.3.1, but it is a nontrivial closure condition on structured contracts. It is what makes the trace-mapping lemma (Corollary 4.4.6) work.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Properties of UTxO Ledgers and Programs Implemented on Them." pith.science (2026). https://pith.science/paper/UOHEENCN

@misc{pith2026250605832,
  author       = {Pith},
  title        = {Pith review of: Properties of UTxO Ledgers and Programs Implemented on Them},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/UOHEENCN}},
  note         = {Machine review of arXiv:2506.05832}
}
read the original abstract

Trace-based properties are the gold standard for program behaviour analysis. One of the domains of application of this type of analysis is cryptocurrency ledgers, both for the purpose of analyzing the behaviour of the ledger itself, and any user-defined programs called by it, known as smart contracts. The (extended) UTxO ledger model is a kind of ledger model where all smart contract code is stateless, and additional work must be done to model stateful programs. We formalize the application of trace-based analysis to UTxO ledgers and contracts, expressing it in the languages of topology, as well as graph and category theory. To describe valid traces of UTxO ledger executions, and their relation to the behaviour of stateful programs implemented on the ledger, we define a category of simple graphs, infinite paths in which form an ultra-metric space. Maps in this category are arbitrary partial sieve-define homomorphisms of simple graphs. Programs implemented on the ledger correspond to non-expanding maps out of the graph of valid UTxO execution traces. We reason about safety properties in this framework, and prove properties of valid UTxO ledger traces.

Figures

Figures reproduced from arXiv: 2506.05832 by the authors.

Figure 1
Figure 1. Non-standard map operators UTxO set. A UTxO set constitutes the state of a ledger model. It is given by a finite map (finite asso￾ciative array) (ByteString,N) 7→ Output The key in the UTxO finite map is called an output reference [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Auxiliary UTxO functions form of boolean predicates on transaction data. To reason about stateful contracts, we use the structured contract model [30]. Let STRUC be a program expressed in terms of the small-steps semantics. The state of this contract is represented (encoded) on the ledger in some specific way. This encoding is specified in terms of a (partial) projection function that computes the contract state for… view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

30 extracted references · 25 canonical work pages

  1. [1]

    Schneider (1985): Defining liveness

    Bowen Alpern & Fred B. Schneider (1985): Defining liveness . Information Processing Letters 21(4), pp. 181–185, doi: 10.1016/0020-0190(85)90056-0

    doi:10.1016/0020-0190(85)90056-0 1985

  2. [2]

    MIT Press

    Christel Baier & Joost-Pieter Katoen (2008): Principles of model checking . MIT Press

    work page 2008

  3. [3]

    A formal model of Algorand smart contracts

    Massimo Bartoletti, Andrea Bracciali, Cristian Lepore , Alceste Scalas & Roberto Zunino (2021): A formal model of Algorand smart contracts , doi:10.48550/arXiv.2009.12140. arXiv: 2009.12140

    work page Pith review arXiv doi:10.48550/arxiv.2009.12140 2021

  4. [5]

    3, Cambridge univer- sity press, doi: 10.1017/CBO9780511525865

    Francis Borceux (1994): Handbook of Categorical Algebra: V olume 3, Sheaf Theory . 3, Cambridge univer- sity press, doi: 10.1017/CBO9780511525865

    doi:10.1017/cbo9780511525865 1994

  5. [6]

    Carolyn Brown & Doug Gurr (1993): T emporal logic and categories of Petri nets . In Andrzej Lingas, Rolf Karlsson & Svante Carlsson, editors: 20th International Colloquium on Automata, Languages, and Programming (ICALP 93) , Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 570– 581, doi: 10.1007/ 3-540-56939-1_103

    work page 1993

  6. [7]

    https://ethereum.org/en/whitepaper/

    Vitalik Buterin (2014): Ethereum: A Next-Generation Smart Contract and Decentrali zed Application Plat- form. https://ethereum.org/en/whitepaper/

    work page 2014

  7. [8]

    Manuel M. T. Chakravarty, James Chapman, Kenneth MacKen zie, Orestis Melkonian, Jann M¨ uller, Michael Peyton Jones, Polina Vinogradova & Philip Wadler (2 020): Native Custom T okens in the Extended UTXO Model . In Tiziana Margaria & Bernhard Steffen, editors: Leveraging Applications of Formal Meth- ods, V erification and V alidation: Applications - 9th In...

    work page 2020

  8. [9]

    Manuel M. T. Chakravarty, James Chapman, Kenneth MacKen zie, Orestis Melkonian, Michael Peyton Jones & Philip Wadler (2020): The Extended UTXO Model . In Matthew Bernhard, Andrea Bracciali, L. Jean Camp, Shin’ichiro Matsuo, Alana Maurushat, Peter B. Rønne & Massimiliano Sala, editors: Financial Cryptography and Data Security , Springer International Publi...

    work page 2020

Show all 30 references
  1. [10]

    https://github.com/input-output-hk/cardano-ledger/r eleases/latest/download/ shelley-ledger.pdf

    Jared Corduan, Matthias G¨ udemann & Polina Vinogradov a (2019): A F ormal Specification of the Cardano Ledger. https://github.com/input-output-hk/cardano-ledger/r eleases/latest/download/ shelley-ledger.pdf

    2019

  2. [11]

    V olker Diekert & Yves M´ etivier (1997): Partial Commutation and Traces, pp. 457–533. 3, Springer Berlin Heidelberg, Berlin, Heidelberg, doi: 10.1007/978-3-642-59126-6_8

    1997 doi

  3. [12]

    https://ergoplatform.org/ docs/whitepaper.pdf

    Ergo Team (2019): Ergo: A Resilient Platform F or Contractual Money . https://ergoplatform.org/ docs/whitepaper.pdf

    2019

  4. [13]

    Gabbay (2021): Algebras of UTxO blockchains

    Murdoch J. Gabbay (2021): Algebras of UTxO blockchains . Mathematical Structures in Computer Science 31(9), p. 1034–1089, doi: 10.1017/S0960129521000438

    2021 doi

  5. [14]

    S´ eminaire Bourbaki8, pp

    Jean Giraud (1962-1964): Analysis situs. S´ eminaire Bourbaki8, pp. 189–199. Available at http://eudml. org/doc/109657

    1962

  6. [15]

    https://tezos.com/ whitepaper.pdf

    LM Goodman (2014): T ezos—a self-amending crypto-ledger White paper . https://tezos.com/ whitepaper.pdf

    2014

  7. [16]

    Courier Corporation

    Heine Halberstam & Hans Egon Richert (2013): Sieve methods. Courier Corporation

    2013

  8. [17]

    In Magne Haveraaen, Olaf Owe & Ole-Johan Dahl, editors: Recent Trends in Data Type Specification , Springer Berlin Heidelberg, Berlin, Heidelberg, pp

    Ulrich Hensel & David Spooner (1996): A view on implementing processes: Categories of circuits. In Magne Haveraaen, Olaf Owe & Ole-Johan Dahl, editors: Recent Trends in Data Type Specification , Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 237–254, doi: 10.1007/3-540-61629-2_46

    1996 doi

  9. [18]

    Andre Knispel, Orestis Melkonian, James Chapman, Alas dair Hill, Joosep J¨ a¨ ager, William DeMeo & Ulf Norell (2024): F ormal Specification of the Cardano Blockchain Ledger , Mech anized in Agda . In Bruno Bernardo & Diego Marmsoler, editors: 5th International Workshop on Form...

    2024

  10. [19]

    https://github.com/input-output-hk/cardano-ledger/r eleases/latest/download/ alonzo-ledger.pdf

    Andre Knispel & Polina Vinogradova (2021): A F ormal Specification of the Cardano Ledger integrating Plu - tus Core. https://github.com/input-output-hk/cardano-ledger/r eleases/latest/download/ alonzo-ledger.pdf

    2021

  11. [20]

    Comptes-Rendus de l’Acad´ emie des Sciences 2, p

    Marc Krasner (1944): Nombres semi-r ´eels et espaces ultram ´etriques. Comptes-Rendus de l’Acad´ emie des Sciences 2, p. 219

    1944

  12. [21]

    5, Springer Science & Business Media, doi:10.1007/978-1-4757-4721-8

    Saunders Mac Lane (2013): Categories for the working mathematician . 5, Springer Science & Business Media, doi:10.1007/978-1-4757-4721-8

    2013 doi

  13. [22]

    Springer, doi: 10.1007/3-540-10235-3

    Robin Milner (1980): A calculus of communicating systems . Springer, doi: 10.1007/3-540-10235-3

    1980 doi

  14. [23]

    Nakamoto (2008): Bitcoin: A Peer-to-Peer Electronic Cash System

    S. Nakamoto (2008): Bitcoin: A Peer-to-Peer Electronic Cash System . https://bitcoin.org/en/ bitcoin-paper

    2008

  15. [24]

    Chad Nester (2020): A F oundation for Ledger Structures . In Emmanuelle Anceaume, Christophe Bisi` ere, Matthieu Bouvard, Quentin Bramas & Catherine Casamatta, ed itors: 2nd International Conference on Blockchain Economics, Security and Protocols, Tokenomics 2020, October 26-2...

    2020 doi

  16. [25]

    Smith (2003): Software Development by Refinement , pp

    Dusko Pavlovic & Douglas R. Smith (2003): Software Development by Refinement , pp. 267–286. Springer Berlin Heidelberg, Berlin, Heidelberg, doi: 10.1007/978-3-540-40007-3_17 . 20 Properties of UTxO Ledgers and Programs Implemented on Them

    2003 doi

  17. [26]

    Kristijan Rupi´ c, Lovro Roˇ zi´ c & Ante Derek (2020): Mechanized F ormal Model of Bitcoin’s Blockchain V alidation Procedures. In Bruno Bernardo & Diego Marmsoler, editors: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) , Schloss Dagstuhl – Leibniz-Zentrum f¨ ur ...

    2020 doi

  18. [27]

    J. J.M.M. Rutten (1995): A calculus of transition systems (towards universal coalge bra). https://ir.cwi. nl/pub/5060

    1995

  19. [28]

    https://docs.zilliqa.com/ whitepaper.pdf

    The ZILLIQA Team (2017): The ZILLIQA T echnical Whitepaper . https://docs.zilliqa.com/ whitepaper.pdf

    2017

  20. [29]

    Polina Vinogradova & Orestis Melkonian (2025): Message-Passing in the Extended UTxO Ledger. In Jurlind Budurushi, Oksana Kulyk, Sarah Allen, Theo Diamandis, Aria h Klages-Mundt, Andrea Bracciali, Geoffrey Goodell & Shin’ichiro Matsuo, editors: Financial Cryptography and Data S...

    2025 doi

  21. [30]

    Polina Vinogradova, Orestis Melkonian, Philip Wadler , Manuel Chakravarty, Jacco Krijnen, Michael Peyton Jones, James Chapman & Tudor Ferariu (2024): Structured Contracts in the EUTxO Ledger Model. In Bruno Bernardo & Diego Marmsoler, editors: 5th International Workshop on For...

    2024 doi

  22. [31]

    https://github.com/ nervosnetwork/rfcs/blob/master/rfcs/0002-ckb/0002-c kb.md

    Jan Xie (2018): Nervos CKB: A Common Knowledge Base for Crypto-Economy . https://github.com/ nervosnetwork/rfcs/blob/master/rfcs/0002-ckb/0002-c kb.md

    2018

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.