An Introduction to Proof-Carrying Data

The previous chapter described what Tachyon needs from its proofs. Proofs from many separate wallets should collapse into one proof that a miner can check quickly, and anyone should be able to continue that combining later. This chapter states that requirement precisely, as a goal called proof-carrying data (PCD). It does not yet explain how to build it.

We treat the proof as a black box throughout, and the rest of the site opens that box. Sections 2 to 7 work through a small sum on a tree, with no cryptography, so that each idea has concrete numbers. Sections 9 to 12 then use the same vocabulary to read Ragu's interface and Tachyon's aggregation.

1. The goal of proof-carrying data

A proof system lets a prover convince a verifier that a computation was carried out correctly. The verifier receives a proof, and checking it costs much less than rerunning the computation. For this chapter we rely on two promises from the proof system. An honest prover can always produce a proof that the verifier accepts, and a prover cannot produce an accepted proof of a false claim, except with negligible probability. The chapter on statements and challenges makes these promises more precise.

Now consider a miner facing thousands of shielded transactions, each built by a different wallet from its own secrets. Using a proof system once for each transaction, or once for all of them together, runs into three obstacles:

• One prover would have to hold everything. A single proof about a thousand transactions, produced in one run, would need one party holding the secrets of a thousand wallets. No such party exists, and no wallet would hand its secrets over.
• Finished proofs would not build on each other. If one more transaction arrives after the proof is done, the prover has to start again from the beginning.
• Separate proofs would keep the verifier's work high. With one proof per transaction, the miner performs one check per transaction, so the cost grows with the number of transactions.

Proof-carrying data avoids all three by changing what gets proved. We split the computation into steps arranged as a tree. Each node of the tree produces a piece of data together with a proof, and that proof covers the step at this node and every step below it. The data therefore carries evidence of its whole history, which is where the name comes from.

A PCD system should provide the following properties, each answering one of the obstacles above:

1. Distributed work. The party running a node needs the data and proofs of the nodes directly below it, plus its own private input. It does not need the private inputs of earlier nodes.
2. Extension. Anyone holding a finished node can use it as an input to a new node, and nobody repeats the earlier proving work.
3. Succinctness. The proof's size and the cost of checking it do not grow with the size of the tree.

Tachyon's aggregation is our running example. In Tachyon, a wallet proves that its transaction follows the rules and publishes the result as a stamp. An aggregator combines stamps from independent wallets into a single stamp, and validators check that one stamp in place of the separate ones. Tachyon has not activated on mainnet and its design is still changing, so everything this chapter says about it describes the Tachyon repository at commit 7e50254. That crate builds against a mock of Ragu, so when we say that a Tachyon step checks something or that a proof fails, we mean what the design expects. At this commit the step bodies run natively, with no real circuits, and we did not find a validator in the crate.

2. A toy computation

To see what each node of a tree claims, we need a computation whose intermediate results are easy to check by hand. Adding up a list has this property, because a subtotal is meaningful on its own and two subtotals combine by addition. Here is the list we will use:

The list has 8 entries, and its sum is 47.

Treat the list as fixed. A party holding position $i$ can read $L_i$, and other parties cannot. We want to reach one short statement about the total that a verifier can accept without ever seeing the list. Getting there requires deciding what each node claims, which is the subject of Section 3, and what rule a node must obey, which is the subject of Section 4. The proof itself enters in Section 6.

3. Headers

We call the data at a node its header. A header has two jobs. It has to give the next node enough information to apply its rule, and it has to stay small, because it travels up the tree with the proof.

The first candidate for a header is the subtotal alone. A join rule would then add two subtotals and output the result. This candidate fails in a way worth seeing:

Joining the entry with value 11 to itself produces a node that claims 22, and nothing in that header reveals the repeat. A tree with 8 leaves has 7 joins, and a prover can choose any entry for each leaf. Enumerating those choices gives 6435 multisets of entries, which reach 71 different root totals from 16 to 88. Only 47 is the true sum, yet every one of these trees passes a join rule that checks only addition.

The trouble is that a bare subtotal does not say which entries went into it. No rule that reads only subtotals can reject a repeated entry, so the header has to record more. Adding the range of positions it covers fixes this. Our header becomes three numbers,

$$(\ell ,h,s),\text{which claims}{L}_{\ell }+L_{\ell +1}+\cdots +L_{h-1}=s.$$

The range includes $\ell$ and excludes $h$, so a range ending at $h$ meets the next range exactly when that range starts at $h$. The header stays at three numbers however many entries it covers, because it records only the conclusion. It forgets the individual values and the order in which they were added. Choosing a header is therefore a decision about what to remember, and the guide is to keep exactly what later rules need to compare.

The stamp header

A Tachyon stamp makes the same decision. Its header has three fields:

• A commitment to the stamp's action set, which holds one digest for each action and fee the stamp covers.
• A commitment to its tachygram set. A tachygram is a published value that commits to the creation or destruction of a note.
• An anchor, which names a position in the history of the Tachyon pool.

The sets grow as stamps combine, but the header cannot, so it holds commitments instead of the sets themselves. A commitment is a short value that stands for a long list and cannot later be opened to a different one. The commitments play the part of our range, because they record what the stamp covers, and the anchor records where in the pool's history it stands.

4. Steps

A header's claim means nothing without rules saying how a header may be produced. We call such a rule a step. A step declares the headers it takes as input and the header it produces, and it states a check that must pass. It may also use private input known only to the party running it, which we call the witness.

Our computation needs two steps. The first has no inputs, and it starts a new header from a single entry. We call it Entry:

$$\text{witness }(i,v),\text{check }{L}_i=v,\text{output }(i,i+1,v).$$

The second step takes two headers and combines them. We call it Join:

$$\text{inputs }({\ell }_1,h_1,s_1),({\ell }_2,h_2,s_2),\text{check }{h}_1={\ell }_2,\text{output }({\ell }_1,h_2,s_1+s_2).$$

The check $h_1={\ell }_2$ is the part that the sum-only header could not express. It rejects any pair of ranges that repeat, overlap, or skip entries. Before attaching any proof, we can test whether these two steps are strong enough, by listing everything they can ever produce:

Start from the 8 entry headers and apply the join rule until nothing new appears. The process produces 36 headers, one for each range of positions, and each one states the correct sum for its range. Of the 1296 ordered pairs of those headers, the rule accepts 84, namely the pairs whose ranges meet. Exactly one derived header covers the whole list, and it is $(0,8,47)$.

This is the property we need from headers and steps together, because it means every header the rules can produce is true. The property has nothing to do with cryptography. It is a fact about the rules, and the application designer is responsible for it. The proof system's job comes later, and it is limited to making sure that nobody can present a header the rules could not have produced.

The stamp merge step

The Tachyon step that combines stamps is StampMerge. Its declaration names one header type for both inputs and for the output:

impl Step for StampMerge {
    type Aux<'source> = ();
    type Left = Stamp;
    type Output = Stamp;
    type Right = Stamp;

The step performs three checks. The two input anchors must be equal, which plays the role of $h_1={\ell }_2$. The set polynomials in the witness must match the commitments in the input headers. Finally, each merged set polynomial must equal the product of its two inputs. Tachyon encodes a set as a polynomial whose roots are the members, so multiplying two such polynomials produces the union of the sets, and this check plays the role of $s_1+s_2$. The chapter on pool state studies these polynomials.

5. Running the tree

We can now run the computation. Each row below is one node, with its leaves first:

Reading up the tree, each row depends only on the rows it names as inputs. A node never looks further down, because its inputs' headers already summarize everything below them.

The tree above is balanced, but the rule does not require that. A list of 8 entries has 429 binary tree shapes that keep the entries in order. Running all of them gives the same root header $(0,8,47)$ every time.

This freedom means the work can follow whoever holds the data:

Suppose Alice holds positions 0 to 3 and Bob holds the rest. Alice runs her subtree and hands over the header $(0,4,25)$ with its proof. Bob does the same with $(4,8,22)$. Carol, who holds neither half of the list, checks only that $4=4$ and $25+22=47$ before producing $(0,8,47)$.

Carol needed neither Alice's values nor Bob's, which is the first property from Section 1 in miniature.

One particular shape deserves its own name. If each new node combines the previous result with one new entry, the tree becomes a chain:

The chain form is incrementally verifiable computation (IVC), which Valiant introduced before the general tree form. Chiesa and Tromer's PCD extended the idea to nodes with several inputs. A chain suits a single party working through a sequence, but it forces independent parties to wait for each other. Tachyon's wallets and aggregators work independently, so they need the tree.

A finished node can also feed more than one later node, because a header and its proof are ordinary data that anyone can copy. For example, the same partial result could enter two different trees. The history of a proof can therefore share nodes, and the literature describes it as a directed acyclic graph. "Tree" remains the common name, and it is accurate for the way we draw the inputs of any one node.

6. Attaching a proof

So far a verifier would have to trust whoever ran the nodes, or else rerun all of them. We now attach a proof to each node, so that a node's output is the pair of a header and a proof. The proof at a node establishes the following statement:

There is a witness for which the declared step accepts these input headers and produces this output header, and each input header has a valid proof.

The last clause makes the statement recursive, which is the central idea of PCD. A node proves that its children's proofs verify, so a later verifier does not have to see those children. How a proof can contain a check of another proof is the subject of the chapter on recursive proofs. For now, we only note that this requires the verifier's own check to be small enough to include in a step.

Unwinding the statement at our root shows how much a single proof covers:

The root $(0,8,47)$ says that the Join rule accepted $(0,4,25)$ and $(4,8,22)$, and that those two headers have valid proofs. Their own proofs in turn say that $(0,2,15)$ and $(2,4,10)$ were joined into $(0,4,25)$, and likewise on the right. Following every branch to the bottom reaches 8 Entry checks, each comparing one value with the list. The root's proof therefore stands for all 15 checks in the table, of which the verifier runs none.

The verifier's procedure has two parts. It runs the proof system's check on the header and proof, and then it compares the header with the question it actually wants answered. The second part is easy to overlook:

The header $(0,7,42)$ is also true and has a valid proof, because it is one of the derived headers. A verifier who wants the sum of the whole list must still confirm that the range runs from 0 to 8, and a verifier who accepted this header without looking would conclude that the total is 42.

A valid proof shows that the rules produced this header, and the verifier still has to decide whether this header answers its question.

7. Why a false header has no valid proof

The argument rests on three assumptions:

1. The proof system keeps its promise from Section 1, so accepted proofs of false statements do not occur in practice.
2. The steps are correct, in the sense of Section 4, so a step with true input headers can only output a true header.
3. The verifier compares the final header with what it wants to know.

Suppose a prover holds an accepted proof for a false header. By assumption 1, the statement from Section 6 is true, so a declared step accepted some input headers and produced this one, and those inputs have valid proofs. By assumption 2, the inputs cannot all be true, or the output would be true as well. So at least one input is a false header with a valid proof, and the same reasoning applies to it. Each repetition moves one level down the tree. The descent eventually reaches a step with no inputs, such as Entry, whose check rejects a false entry directly. A prover therefore cannot obtain a valid proof of a false header.

This descent is informal in one respect. Soundness makes accepted proofs of false statements infeasible to find, but such proofs can still exist, so "those inputs have valid proofs" does not by itself show that anyone holds them. The argument really needs a prover who produces a proof to know the child proofs as well. That is the knowledge soundness of the next chapter, and the chapter on recursive proofs returns to this point.

Here is what each natural attempt to cheat runs into on the toy tree:

In each case the prover cannot obtain a proof for the node where the falsehood first appears, so no later node can use it as an input.

Assumption 3 matters in Tachyon, because some of its steps leave a value unconstrained at the start. For instance, the anchor is a free witness in the FeeSeed step, so the proof does not by itself show that the anchor belongs to the real chain. Validators close this gap by confirming the anchor against the consensus chain.

8. Succinctness

The statement in Section 6 could be met in a wasteful way, by having each node attach its children's proofs to its own. The pile of proofs would grow with the tree, and the verifier would check each one. We can compare that approach with the goal:

The last column shows another benefit of a tree. With enough workers, each layer of a balanced tree can run at the same time, so the number of rounds grows with the logarithm of the number of entries.

Succinctness is not only a convenience for the final verifier. Each node has to check its children's proofs as part of its own statement. If checking a proof grew with the size of the history behind it, every level of the tree would cost more to prove than the one below, and the recursion would soon become impractical. A proof system usable for PCD therefore needs a check that stays small no matter how much history the proof covers. Most of the machinery on this site exists to meet this requirement, and much of the difficulty lies in making that check cheap enough to run inside another proof.

Headers obey the same constraint. Ragu fixes a maximum header size for each application, through the HEADER_SIZE parameter. This is the practical reason that the stamp header holds commitments in place of its growing sets.

9. Fusion in Ragu

Ragu provides this model through a small set of concepts, described in the Ragu Book's chapter on PCD. A Header defines the form of a node's data, and a Step declares a left input header, a right input header, an output header, and a witness. The operation that runs a step on two inputs and produces a new node is called fuse.

Telling header types apart

A header type also has a suffix, a label that distinguishes it from other header types even when their contents look the same. To see why this is needed, extend the toy example:

Suppose a final step Charge adds a flat fee of 2. It consumes $(0,8,47)$ and outputs $(0,8,49)$. If Charge accepted its own output, a prover could apply it again to reach $(0,8,51)$, even though the fee is meant to apply once. The input and output contain three numbers of the same form, so the numbers cannot tell the two states apart. Giving the input and output different type labels, say Tally and Charged, solves this, because Charge accepts only a Tally.

Tachyon uses suffixes in the same way. Its Actions and Stamp headers contain identical fields, and Actions even reuses the encoding of Stamp. Only the suffix differs. The first represents actions before a fee is applied, and the second represents them afterward, so a step that requires a stamp cannot receive an unfinished set of actions by mistake.

Choosing among many steps

The original PCD model has a single rule, applied at every node. An application with many kinds of transition must then fit them all into that one rule, and every node pays for the whole of it. Ragu instead lets the prover choose any registered step at each node and pay only for the chosen one. The chapter on wiring and the registry explains how the protocol supports this. Our toy application uses two steps, and Tachyon's table of steps lists a few dozen.

Every node has two inputs

Supporting chains, leaves, and joins as separate cases would mean building separate mechanisms for them in the protocol. Ragu avoids this by giving every node exactly two inputs, which makes every computation a binary tree that may be unbalanced. Join fits this form directly. To fit the others, Ragu has a unit header, written (), which carries no data. A chain step such as "append one entry" declares () as its right input, and Entry declares it for both inputs.

An unused input still has to be filled with something that has a valid proof, because the unit header gets no exemption from the check on its children. So a question remains about what sits at the bottom of the recursion.

The base case

The statement in Section 6 says that each input has a valid proof, but the first node has no earlier proofs to point to. Some node must skip that part of the statement, and a skipped check could be an opening for forgery, so Ragu confines it tightly.

Ragu performs the skip in exactly one internal step, called the bootstrap step. That step declares a private header type named Dummy for both inputs, and this type is what selects the base case. It takes two synthesized proofs that would not verify on their own, skips their claims, and outputs a valid proof of a unit header that attests nothing. Application code cannot declare Dummy, so no application step can skip its children's checks. The seed operation then starts a leaf by fusing a step with this bootstrap proof as both children, and it enforces those children's claims in the ordinary way.

10. Uncompressed and compressed proofs

Section 8 asked for proofs whose size does not depend on the tree, and Ragu's proofs meet this in two different ways. The proof a node holds during fusing has a fixed shape, but the Ragu Book describes it as large, since it is not yet in succinct form. Ragu calls this the uncompressed mode. With additional work, the compress operation produces a compressed proof that the book describes as orders of magnitude smaller, and a code comment gives its size as a few kilobytes. The extra work makes compression worth doing only where a proof leaves the tree and goes to a third party. The chapter on recursion in Ragu explains how it works.

The two modes raise two questions on which the sources do not yet agree. The first concerns what can happen to a compressed proof afterward.

The second question concerns privacy. Everything in this chapter has been about correctness, and nothing has required the proof to hide its inputs.

11. Aggregation in Tachyon

With this vocabulary we can follow one aggregate from start to finish. The Tachyon book on aggregation uses three names for the states a transaction's Tachyon bundle can be in. An autonome comes from a wallet and carries a complete stamp. An aggregate comes from an aggregator and carries a merged stamp that needs inputs from other transactions. An adjunct has had its stamp stripped and points to the aggregate that covers it.

The inputs

Our example has three autonomes X, Y and Z, plus an aggregator's own bundle A. A real tachygram is a field element, and a real anchor is a hash value. In this table, three-digit numbers stand in for tachygrams, and ${\alpha }_k$ stands for the anchor at position $k$. We also write the sets out literally, which is what the real commitments stand for. An $a_k$ is an action digest, and an $f$ is a fee digest.

These sizes follow the book's rule. Each action publishes two tachygrams, and each bundle adds one more for its fee change note, so a stamp covering $N$ actions in $B$ bundles has $2N+B$ tachygrams. Bundle A has no actions of its own, which the book calls an innocent aggregate. Its stamp comes from FeeSeed, a step with unit inputs, and that step proves A's zero fee.

The tree

The wallets chose their anchors independently, and StampMerge requires equal anchors because its output has a single anchor field. The aggregator therefore lifts the older stamps to a common position first. The step that does this, StampLift, shows that a step's two inputs need not have the same header type. Its left input is a stamp and its right input is an AnchorSpan, which is a separate PCD attesting to a run of anchors. The step moves the stamp from the span's start, or from any anchor the span lists as a member, to the span's end.

The same span serves both lifts, which is the node sharing that Section 5 described. Running the tree gives:

The span runs from ${\alpha }_{12}$ to ${\alpha }_{15}$, with members $\{{\alpha }_{13},{\alpha }_{14},{\alpha }_{15}\}$. Merging A with the unlifted X would fail, because $15\ne 12$.

The merged stamp stays on the receiving bundle A and keeps A's fee. Literal sets would make the last row's header far larger than the first, which is why the real header has only commitments, and they have the same size in every row.

The block

A miner who wants to use this aggregate must include every bundle it covers, and it strips the stamps from the covered ones:

The block carries 1 proof where the four separate transactions carried 4. It still carries all 12 tachygrams and all 8 action and fee digests, because the verifier needs them. A validator collects the digests from the four transactions, takes the tachygrams and anchor from A's stamp, and checks the one proof against the header those values produce. If a miner leaves Z out of the block, the rebuilt action set has 6 digests instead of 8. The header no longer matches the one the proof was made for, so the proof fails.

This shows how a verifier uses the header in practice. The stamp carries no proof header, so the verifier builds it from the published data, as the verification code does. The validator also checks the anchor against the chain, which is the comparison that Section 7 required. So the part that aggregation removes is the proofs, while the public descriptors and tachygrams all remain on chain.

Removing a contributor

A step does not have to make its header cover more. Blocks keep arriving while an aggregator works, and the aggregator's guide describes how it recovers when some of its inputs get mined first:

Suppose a block includes X on its own while the aggregator is still working. The merged stamp holds 12 tachygrams, and publishing it now would repeat those of X. StampUnmerge takes the merged stamp and a stamp of X lifted to the same anchor, and it produces a stamp with 9 tachygrams and 6 action digests, which covers A, Y and Z. Its header states less than its input did, which is permitted, because a step only has to establish the relation it declares between its inputs and its output.

The chapter on aggregation and bundles covers fees, stripping, and the wire format in detail.

12. The rest of Tachyon's proof tree

Stamps sit at the top of a larger tree, and different parties run the nodes below them, which is the first property from Section 1 at full scale. The following graph traces one spend in an epoch after its note's creation, up to an aggregate. Each box names a step, and each edge label names the header it passes on. We have simplified the graph by leaving out the steps that feed the sync service, the variants of some steps, and merging with other actions.

Three things from this chapter appear in this graph. The header type changes from step to step, so the suffixes keep each state separate. NoteSecret feeds two later steps, so the history shares nodes. Finally, the parties see different things. The sync service builds its ArbitraryUnspent segments without holding the note or its commitment, and only the wallet's UnspentBind step connects those segments to a note. The chapter on the proof tree walks through each of these steps.

13. Where this chapter leaves us

This chapter took the following steps:

1. Proof-carrying data arranges a computation as a tree of nodes, where each node produces a header and a proof covering everything below it.
2. A header states what a node claims, and it has to hold enough for later rules to catch repeats and gaps while staying a fixed size.
3. A step is the rule relating input headers and a witness to an output header. Correct steps mean that every header they can produce is true.
4. A node's proof states that its step accepted its inputs and that those inputs have valid proofs. This recursion lets one proof stand for the whole tree, provided the verifier also compares the final header with what it wants to know.
5. Succinctness requires a proof check that stays small however much history the proof covers, because each node has to run that check on its children.
6. Ragu gives every node two inputs, confines the base case to one internal step, and separates large uncompressed proofs from small compressed ones that cannot currently be fused further.
7. Tachyon's aggregation applies this model to stamps, removing proofs from the chain while keeping every descriptor and tachygram public.

Everything here assumed a proof system that can prove a step's check and verify another proof inside a step. The rest of the site builds that system. The next chapter, Statements and Challenges, starts with what it means to prove a statement and how random challenges make a large check small.