Model-Generic Incrementally Verifiable Computation from Updatable BARGs
Abstract
Incrementally verifiable computation () is a computationally sound proof system that allows a prover to certify the correctness of a long or ongoing computation in an incremental manner, by repeatedly updating a proof certifying the computation so far. Updating the proof does not require access to the entire trace of the computation, which makes the IVC-prover memory efficient. Recently, such schemes were constructed for deterministic Turing machines from standard cryptographic assumptions (Paneth and Pass, FOCS 2022, and Devadas et al., FOCS 2022).
In this work we generalize and extend to support incremental certification and verifiability of a large set of computation models, focusing on distributed and online computation. This allows distributed algorithms to efficiently certify their own execution using low memory and communication overhead. We construct for a variety of computation models by proving one generic lifting theorem from a classical (non-incremental) delegation scheme (also known as ) into full-fledged , while preserving the delegation scheme’s succinctness properties (up to an additive factor which is polynomial in the security parameter and independent of the size of the computation). Using this lifting theorem, we obtain for the following computation models:
-
RAM and exclusive-read exclusive-write (EREW) PRAM algorithms, using existing delegation schemes for these models.
-
Streaming algorithms, using the natural memory-efficiency properties of the model.
-
Massively parallel computation (MPC). Notably, in this model, memory efficiency is a critical bottleneck: the machines participating in an MPC algorithm usually cannot store the entire trace of their computation. Thus, certifying MPC algorithms naturally benefits from . Moreover, since prior to our work, no delegation scheme for this model was known, we also construct a delegation scheme for one-round massively parallel computations, and then apply our lifting theorem to it.
-
Distributed graph algorithms, using existing distributed delegation schemes (also known as locally verifiable distributed s). Here, in order to use our lifting theorem we have to first make some observations about the verification procedure of these existing schemes.
At the heart of this work is a new abstraction, updatable batch arguments for (s), which we define and construct. Standard s allow one to prove a batch of -statements using a proof whose length barely grows with ; however, the statements and their witnesses must all be known in advance. In contrast, s support adding statements and witnesses on the fly, making them a flexible tool for constructing across different computational models.
Keywords and phrases:
incrementally verifiable computation, massively parallel computation, streaming, parallel RAM, batch arguments, SNARGFunding:
Eden Aldema Tshuva: Research supported by the Israeli Science Foundation, Grant No. 2338/23, and by AFOSR award FA9550-24-1-0156.Copyright and License:
2012 ACM Subject Classification:
Theory of computation Cryptographic protocolsEditor:
Shubhangi SarafSeries and Publisher:
Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik
1 Introduction
Delegation schemes [19, 16, 17] enable a computationally weak entity to outsource a computation to a more powerful entity without having to trust it: the powerful entity returns the result alongside with a succinct proof of correct execution, which the weak entity can verify efficiently. Delegation schemes typically require the prover to access the entire trace of the computation, which can be impractical. Incrementally verifiable computation () [23] avoids this by maintaining the proof incrementally: given the state of the computation after steps, and proof showing that the first steps have been executed correctly, the prover updates the proof to a new proof that the first steps have been executed correctly, without having to store in memory the entire trace of the computation so far. This makes a natural fit for scenarios where long computations must be executed reliably over time: for example, resuming a paused computation from an intermediate verified state, or continuously auditing the correctness of outsourced computation performed by an untrusted server or cloud. While [23] and follow-up work [5, 4] show how to construct for from heuristic (non-falsifiable) assumptions, recently for deterministic computations was constructed from LWE [20, 11],111While the constructions in [20, 11] are using specifically LWE, combining them with the works [24, 7] gives the same results also under bilinear maps assumption or under subexponential security of DDH. and this is the setting we adopt in the current paper.
While [20, 11] develop for sequential RAM, there are many other computation models that would benefit from . In fact, a natural application of is to computations that are distributed or reactive in nature, where the inputs arrive over time, or are jointly held by multiple parties that collaborate to carry out the computation, such as in streaming algorithms and in massively parallel computations. The incremental structure of is particularly well-suited to such computation models, where it is usually impractical to store the full trace of the computation, which is required for non-incremental delegation schemes (i.e., succinct non-interactive arguments (s)). For example, when a computation is outsourced to a server farm, typically no single server has enough memory to store the entire trace of the full computation carried out across all the servers. Incremental verification avoids the need to store the full trace, and allows us instead to create a succinct proof of correctness and update it on-the-fly as the computation proceeds, with no asymptotic memory overhead other than the proof itself.
Despite this apparent fit, for reactive and distributed computation models has received very little attention in the context of standard cryptographic assumptions.222From heuristic assumptions, schemes have been developed for streaming algorithms [13, 22], and a generalization of , known as proof-carrying data (PCD), may be considered as a form of distributed for some types of distributed computations [6, 5]. To our knowledge, the only work in this direction is [1], which developed zero-knowledge for streaming algorithms (using a different completeness notion and techniques than ours). In this paper we extend the scope of to encompass such distributed and reactive models of computation, bringing the benefits of incremental verification to settings that arguably stand to gain from it the most. We do this in a generic and modular way, by giving a lifting theorem that applies to any deterministic computation model represented as a labelled transition system (LTS), and allows us to lift a succinct proof for the correctness of one computation step in the model into full multi-step .
Constructing incrementally verifiable computation.
Consider a computation starting from an initial configuration and ending at configuration . Proving that the computation is correct boils down to proving the conjunction of statements: “for each , the system transitions from configuration to configuration in one step”. In Valiant’s paper introducing [23], this was done using a primitive he called noninteractive computationally sound proof of knowledge, and involved a tree-based construction where proofs for short computations are merged into proofs for longer ones: conceptually, at each point in time, the proof consists of a forest, where each tree proves correctness of a sub-computation of the form for some . There is at most one tree of any given height, and the proof stores only the roots of the trees, not the entire forest (making it succinct). To update the proof, the prover creates a new tree of height 1 for the last computation step , and then repeatedly merges any two consecutive proof-trees of the same height, until the invariant that there is at most one tree of any given height is restored. Merging two proof trees for sub-computations and yields a new tree proving the sub-computation , whose height is greater by 1 than the merged trees.
In [23], Valiant constructed noninteractive CS proofs of knowledge in the random oracle model; unfortunately, to date no construction of such proof system from standard assumptions is known. Follow-up work on (non-incremental) delegation [9, 15, 24, 7] and on [11, 20] follows the conceptual idea of Valiant’s construction but replaces noninteractive CS proofs of knowledge with batch arguments for (s), which are known to be constructible from standard assumptions [20, 11]. Informally, a for an -language allows us to prove the conjunction of statements, each of the form “”, using a proof whose length grows linearly with the length of a single -witness for , and only polylogarithmically with the number of statements .
The transition from noninteractive CS proofs of knowledge (used in [23]) to s for (used in the of [11, 20]) is not as smooth as one might hope: many technical issues arise, which are resolved in an ad-hoc manner specific to each construction. Trying to extend these constructions to more complex computation models becomes prohibitively complicated. One key difference is that in standard sequential computation (e.g., Turing machines or RAM), given the initial configuration, the entire trace of the computation is determined; even though the prover does not actually store the entire trace, this fact is crucial for the soundness proof of [11, 20]. In contrast, in more complex models such as distributed and streaming algorithms, the computation trace (of a single machine, in the distributed case) cannot be determined from the initial configuration alone, because it depends on inputs or messages that arrive during the computation. Fundamentally, while standard sequential requires us to prove a predictable sequence of statements , in more complex models we cannot predict in advance the statements that we will need to prove, as each statement has the form “”, where is the input (or message) that arrives in step .
A generic framework for incrementally verifiable computation.
To handle inputs that arrive over time in a simple and unified way across different computation models, we define and construct an updatable form of s, which we call updatable hash-and- (). An proves the conjunction of -statements, like a regular ; however, unlike a regular , the exposes a hash of the statements that it proves, and can be updated on-the-fly to add a new statement (which is not true for plain s). Moreover, the supports a consistency check specified by the user, which is applied to every pair of consecutive statements added to the . This is especially useful for , where we prove a batch of statements that each have the form “”; in order for the conjunction of these statements to represent an actual trace of a computation, we must require that for each , and this is enabled by a consistency check applied to the statements “” and “”.
With the in hand, we are able to extend delegation schemes into . To give a unified statement which applies to diverse computational models, we use the general notion of deterministic computation models represented as a labeled transition system. This allows us to generalize the concept of delegation, and refer to a delegation from a stronger model of computation (where the prover is implemented) to a weaker model of computation (where the verifier is implemented). For instance, in the case of RAM delegation, the prover is a RAM machine and the verifier is a low-space Turing machine. Note that since the prover and verifier are in different models of computation, and thus have different computational power, even delegating one step of computation on a stronger model to a weaker model may be non-trivial (and this is the exact case in some of the models we handle, such as the massively parallel computation model).
Our main contribution is the following “lifting”-type theorem from one-step delegation to multi-step :
Theorem 1 (Informal).
Let be deterministic computation models represented as labeled transition systems, such that
-
1.
There exists a delegation scheme succinctly proving the correctness of a single computation step of , where the prover runs in the model and the verifier runs in ; and
-
2.
The prover and the verifier of the can be implemented in and , respectively.
Then there is an scheme for , where the prover runs in and the verifier runs in .
The construction described in Theorem 1 and its analysis are relatively straightforward compared to prior work on : the interface of the allows us to cleanly implement Valiant’s construction [23], avoiding many of the complications that arise in prior work. The construction of the itself is closely based on [20], but there are some subtleties. For example, as part of the ’s interface, we must be able to provide an opening of the hash to any given statement, without holding all the statements in the clear, even though we do not know what statements will arrive in the future and go into the hash after the statement we are interested in. We show that we can compute the required openings in hindsight, using properties of tree-based hash families with local openings.
Applications.
Using Theorem 1 we develop for several reactive and distributed computation models: streaming algorithms,concurrent PRAM algorithms in the exclusive-read exclusive-write model (EREW), distributed algorithms in the CONGEST model, and distributed algorithms in the massively parallel computing (MPC) model. CONGEST is a model of network algorithms: it features a network of processors that communicate synchronously over some graph topology, with the number of bits that can be sent across any communication link bounded per synchronous round. The focus in this model is on communication as a bottleneck, not on space or even on local computation steps. In contrast, MPC is a model of server farms or cloud computing, where a large number of space-bounded machines collaborate to compute on an input partitioned between them. In each synchronous round, each machine can communicate with multiple other machines arbitrarily, subject only to a bound on the total number of bits sent and received.
While most of the models we consider already have non-incremental delegation schemes, for the MPC model this is not the case: proving the correctness of MPC computations almost requires , because no single machine can even store the entire input, much less the entire trace of the distributed computation. Thus, while communication-efficient distributed provers have already been developed for other distributed models which are not space-bounded [12, 2, 3], prior to our work no such construction was known for MPC, even if we do not insist on and are willing to settle for a non-incremental construction. In fact, even proving the correctness of a single global computation step of the MPC model (i.e., a single synchronized round, where each machine receives messages, computes locally, and sends messages) is non-trivial, as it involves message exchanges between a large number of machines. To instantiate Theorem 1, we first use s to construct a one-step delegation scheme for the MPC model, and then apply the theorem to obtain for MPC.
We consider two use cases for our for MPC. The first is reliable delegation to the cloud: here, the user holds an input , and outsources a difficult computation on to a server farm or a cloud provider, which returns both the output and a short correctness certificate. The user is a single time- and space-bounded machine; it hashes once, never re-reads (only its hash), and verifies the result of the computation in time polylogarithmic in . The second use case that we consider is providing internal reliability to an MPC computation: instead of an external user, here it is the network itself that wants to verify that the computation so far has proceeded correctly (e.g., to protect against faults or issues with some of the machines). Our distributed allows the network to maintain a succinct, continuously updatable correctness proof that any machine can individually store and verify locally against its own input, such that if all machines accept the proof, then the computation is correct (except with negligible probability). This use case resembles a distributed fault-tolerance mechanism for the CONGEST model called proof labeling schemes [18], where each machine stores a short certificate, and the machines communicate with each other to verify that the network is in a legal configuration. Our for MPC scheme is more efficient, as our proof size grows polylogarithmically with the network and input size (in proof labeling schemes, the overall proof size is at least linear in the network size), and verifying the proof requires no communication between the machines. We note that the construction that we give for the CONGEST model returns to the traditional proof labeling scheme model, and has the machines each store a short certificate and communicate with its neighbors to verify it (as is also done in the non-incremental delegation schemes of [12, 2, 3]).
1.1 Related Work
We briefly survey related work. Since our results and techniques lie in the regime of arguments and delegation schemes from standard, and more importantly, falsifiable, cryptographic assumptions, we focus here on constructions in this regime.
Incrementally verifiable computation from LWE.
The recent work of Paneth and Pass [20] and Devadas et al. [11] constructs from standard cryptographic assumptions. Our construction is similar in spirit to these constructions (specifically to [20]), but the provers of [20, 11] require access to the full current state of the system, and their verifiers must read the full state of the system to verify it. We allow for more limited access; for instance, in distributed graph algorithms our prover updates the proof without any single entity knowing the entire communication graph state. That said, these works are closely related to ours: both [20, 11] construct rate-1 batch arguments, which we use to construct our s, and the framework of [20] for constructing serves as a starting point for the construction of our s.
Works from indistinguishability obfuscation.
In general, succinct arguments from have some major drawbacks; in order to instantiate them from falsifiable assumptions they usually require the CRS to be non-succinct and the underlying assumption to be exponentially secure. In contrast, all of our results are instantiable from either LWE, bilinear maps assumptions, or subexponential security of DDH. Nevertheless, the following recent works are related to ours. The first notion of updatable batch arguments was defined and constructed in [14] from . As is the case with the earlier for from [21], their argument is non-adaptively sound. That is, the statements in the soundness game are chosen before the CRS, and the latter may depend on them. The somewhere argument of knowledge property is incomparable, as it is on one hand adaptive (the CRS is chosen before the statements) but on the other hand only provides guarantee somewhere (while non-adaptive soundness is a guarantee about all locations at the same time).
Very recently, [10] constructed for from the combination of and LWE with proofs which grow polynomially with the size of one configuration and polylogarithmically with the number of steps. They also offered an with proofs which do not grow with the size of one configuration which works for the special case of trapdoor languages.
2 Preliminaries
Algorithms, computation models and traces.
We represent an algorithm by a labeled transition system (LTS) , where is a set of configurations (i.e., states of the algorithm), is a set of labels, and is a transition relation between configurations. The labels typically represent the input to the algorithm, but in some scenarios they may represent something else (e.g., a message received by a machine in the MPC model). We restrict to deterministic algorithms, where is single-valued: for any configuration and label there is a unique configuration such that . We sometimes represent is a function, .
A computation model is simply a set of algorithms (i.e., LTSs). A trace or computation of an algorithm is a sequence , such that for each .
The common reference string model and computational hardness.
Our work is set in the common reference string (CRS) model, where all parties have access to a string that is sampled randomly by a trusted setup process, denoted , which takes a security parameter and returns the CRS. The security parameter governs the computational resources that must be invested to break security: we say that a task involving the CRS is computationally hard there is no adversary that takes and runs in time polynomial in , can succeed in the task, except with negligible probability in . The following primitives are all in the CRS model and all include CRS generation as part of their interface.
Delegation schemes.
A delegation scheme involves a prover and a verifier; the prover tries to convince the verifier of the correctness of some computation. The goal here is succinctness: the proof short, and in this context, succinct means polylogarithmic in the size of the input to the computation. We adopt the notion from [16], where the proof is with respect to a digest (a hash) of the initial and final configuration of the computation. The digest is computed honestly by calling with a configuration , and the algorithm satisfies computational collision-resistance. Soundness requires that a dishonest prover cannot convince the verifier of two “contradictory statements” , where each asserts that from an initial configuration represented by the same digest , the computation reaches a final configuration represented by digest , but .
In this work we use a generalized notion of delegation scheme we call - delegation, where the digest and prover are algorithms and the verifier is a algorithm. We moreover adjust the syntax to fit label transition systems, and add a label digest algorithm. The syntax is given below.
-
: A -algorithm that takes a reference string , and a configuration . It outputs digest .
-
: A -algorithm that takes a reference string and a series of labels . It outputs digest .
-
: A -algorithm that takes a reference string , a -algorithm a configuration , a number of steps , and a set of labels . It outputs a proof .
-
: A -algorithm that takes a reference string , a -algorithm , an initial digest , a final digest , a number of steps , and a proof . It outputs an acceptance bit .
Incrementally Verifiable Computation ().
An scheme is similar to a delegation scheme, but the prover incrementally updates an existing proof, and is therefore represented by an update procedure that takes the current configuration and proof , and returns the next configuration and proof . The verifier also takes the current number of steps . Soundness is the same as for delegation. However, completeness is replaced by incremental completeness, which intuitively requires that any proof accepted by the verifier can be extended into a proof for the next step:
-
Incremental completeness: for any generated by , step count , digest , machine , configuration and proof , if and
, then for and , we have .
This formulation does not involve input that arrives during the computation. In reactive models, the prover takes the input in addition to the current configuration, and produces a digest of the inputs in addition to the new configuration and proof. The verifier is given the digest of the inputs in addition to the parameters it is given above.
Somewhere extractable batch arguments for NP.
A batch argument () [8] allows a prover to succinctly prove the conjunction of statements, with a proof whose size is roughly the same as the size of one witness and barely grows with . The interface is as follows:
-
: takes a reference string , an -machine , instances and witnesses , and outputs a proof .
-
: takes a , an -machine , and proof and outputs an acceptance bit .
Note that the prover requires all statements and corresponding witnesses to construct the proof; this is one key difference between plain s and the s that we introduce later.
We say a is somewhere extractable if it allows the extraction of one witness from a convincing proof : the generation procedure can be called in trapdoor mode, where it takes as additional input an index , called the binding index. In this mode, outputs a pair , where is a trapdoor that can later be used to recover the -th witness. In trapdoor mode, the procedure has a property called index hiding: given (without ), it is computationally hard to find the binding index . We require somewhere argument of knowledge: there exists an efficient extractor , which satisfies the following. Suppose we call in trapdoor mode with a binding index and obtain . Given only , it is computationally hard to find a proof that is accepted by the verifier, such that when we extract a witness using , we have .
3 Technical Overview
In this section we give an overview of our construction, focusing on the definition and construction of the , the proof of Theorem 1, which lifts from one-step delegation to , and the application to massively parallel computation (MPC).
3.1 Defining Updatable Hash-and-s
An updatable hash-and- is defined with respect to some hash family with local opening; for simplicity, in this overview we use a Merkle tree. The consists of three algorithms, , where is a CRS generation algorithm, and are update and verification algorithms, respectively, with the following syntax.
-
: the ’s update procedure takes as input a hash key , common reference string , -machine , hash value , proof , and new statement and witness , and outputs a new hash value and proof .
-
: the verifier takes a hash key , common reference string , -machine , hash value and proof , and outputs an acceptance bit .
Note the difference between the ’s interface and the interface of a plain : first, the ’s update procedure does not require access to all the statements and witness, only to the current and the new statement and witness . In addition, the directly exposes a hash of the statements, in addition to the proof . This differs from plain s, where only the proof is exposed (implicitly, there is still a hash of the statements, but it is part of the proof and is not accessible to the user of the ). For our applications it is crucial to expose the hash, because in a reactive computation model it is meaningless to say that a computation starting in configuration and ending in is “correct”; we can only say that it is correct with respect to the input that arrived as the computation was ongoing. Thus, the verifier requires access to a hash of the statements (which include the input), not just the proof of their conjunction.
Our satisfies the usual succinctness and index hiding properties of a , but completeness and somewhere argument of knowledge are strengthened as follows:
-
Incremental completeness: if and , then we also have , where .
-
Somewhere argument of knowledge: upon using the trapdoor version of , programmed to location , the extractor extracts not only a witness , but also a statement and an opening proving that indeed opens to in the index .
The opening extracted by is crucial to the soundness of our (discussed below), but it is non-trivial to obtain: at the time the -th statement and witness are added to the , we do not yet know what the opening to index will be, because future statements added to the will change it. We show that we can use the structure of Merkle trees and auxiliary information computed at update time to compute this opening in hindsight.
Supporting consistency checks.
Our requires the ability to claim that two extracted instances are consistent with each other, for a definition of “consistent” that is supplied by the user. To that end, we extend the syntax above, and give the update and verification procedures two additional inputs: a Turing machine specifying the consistency check, and a “last instance” , which is intended to be the last statement added to the . The incremental completeness guarantee now applies only when , that is, only when the new statement is “consistent” with the preceding statement . Also, the extractor of the somewhere argument of knowledge guarantee now additionally extracts a previous instance and a respective opening , and we require in addition to the previous requirements that (1) opens to in location and this is proved by the opening , and (2) . Finally, in the version which supports consistency checks we also require a useful property that we call last-statement collision-resistance: it is computationally hard to find a tuple , two different last statements , and an opening , such that accepts , but proves that opens to in the location of the final instance.
3.2 Lifting One-Step Delegation into using s
We now outline our generic construction using s (Theorem 1). Let be the computation model whose executions we would like to incrementally prove correct; we assume that the prover also runs in the model . However, the verifier may be computationally weaker, and runs in some other model . We require that the ’s prover and verifier run in the models and , respectively; this is not a significant limitation, because in our construction both are space-efficient Turing machines.
Suppose we have a (non-incremental) delegation scheme that can succinctly prove one-step computations in , and let be an algorithm (represented as an LTS). Let be an algorithm in that implements the verifier , with the parameters of the delegation scheme (e.g., the , the algorithm and the security parameter) hardwired: takes as input digests , a label and a proof , interprets as digests , and computes the output of the verifier on .
Our prover is quite simple: it maintains an for the language , viewed as an -language where the statement is the triplet and the witness is the one-step delegation proof (so that iff the verifier of the one-step delegation scheme accepts). We use a simple consistency check which requires that for any two consecutive statements and we have . The prover runs alongside the algorithm ; whenever transitions from to upon receiving input , the prover computes , and uses to obtain a proof for the (digested) transition . Then it updates the by adding the instance-witness pair .
The prove soundness, we show that if an adversary convinces the verifier to accept two contradictory proofs for final digests with respect to the same initial digest , input hash and step number , then for each , a similar adversary can do the same when we use the CRS generator of the in trapdoor mode to bind location . This allows us to extract instances from the two respective proofs, alongside with their respective witnesses, which are proofs for the state transition in the delegation scheme: and . We then prove by induction on that in the th experiment described above, we have with overwhelming probability . Then, using the last-statement collision resistance property for experiment , we argue that it must be that and , which implies that final digests were the same, , a contradiction.
To prove the th induction step, we use the index hiding property to move from the induction hypothesis experiment into a hybrid experiment where the is binding in both indices , and then use the consistent argument of knowledge property of the , the soundness property of the underlying delegation scheme, and the collision resistance property of the hash family to prove that in this hybrid experiment. We finally use the index hiding property again to move into the next experiment of the induction, where the is only binding on .
One way in which this construction and its analysis differ from previous constructions (e.g., [20, 11]) is the explicit use of consistency checks to enforce equality between the last and first configurations (respectively) of every two successive transitions; prior work, which did not have consistency checks, used somewhat ad-hoc solutions to ensure this equality.
3.3 Constructing an Updatable Hash-and-
Our construction is similar to [20], with the main differences being the extractor’s ability to extract an opening in hindsight, and the support for consistency checks, which also requires extraction of the opening to the next-to-last statement. We briefly review the parts of the construction that are similar to [20], and then explain how the unique features of the (which are not present in [20]) are implemented.
In [20] (as in prior work on delegation and ), the proof of a conjunction of statements with corresponding witnesses is represented as a forest of complete binary trees. The leaves of the trees are individual statements and witnesses, and each inner node intuitively represents a proof for the conjunction of its two children, so that the root of each tree (informally) proves all the statements represented by its leaves. We do not store the entire forest, but rather only the root of each tree; in addition, we make sure that there is always at most one tree of any given height, so that the total number of trees is .
We refer to the height of a trees as its level, and we define a different verifier for each level: at level 0 (a leaf), the verifier is simply the -verifier of the language, which takes and accepts or rejects. At levels , each node stores a proof asserting that the level- verifier accepts both of its children. The witness for each child is the level- proof that it represents, if the child is an inner node, or if the child is a leaf, the witness for the statement represented by the leaf. In turn, the level- verifier is the verifier of the constructed for level-. To add a new statement and witness , the prover creates a new leaf for . It then repeatedly merges any two consecutive trees of the same level , by creating a new level- node with a asserting that the roots of both trees are accepted by the level- verifier, and then discarding the two level- roots.
To extract the -th witness, we find the tree root containing statement (this is determined by the index and the levels of the trees, as all trees are complete). From the root, we descend down the tree to the leaf representing the -th statement and witness, at each step using the extractor of the at the current node to obtain the proof of the child to which we descend, until we arrive at a leaf; in [20], at the leaf we extract the -th witness , which we then return.
Maintaining an explicit hash of statements, and tying it to the proof.
In the we expose to the user a hash with local openings of the statements that went into the (which is not done in prior work). This is straightforward: we maintain a separate hash forest, with the same structure as the proof forest described above – at the leaves we hash the statements themselves, and each inner node is the hash of its two children. To tie the proof forest to the hash forest so that it “refers” to the same statements and supports extraction, we modify the level- verifier: at leaf nodes (), the verifier takes the statement stored in the leaf of the hash forest and the witness stored in the leaf of the proof forest, and checks that the -verifier accepts them. At inner nodes (), the verifier checks that the current node in the hash forest indeed stores the hash of its two children (in addition to verifying the level- as before). The witness for this claim is the pair , i.e., the hashes represented by the children.
Extracting openings in hindsight.
The extractor of the must return the -th statement and a corresponding opening in the hash forest, in addition to the witness whose extraction we described above. Extracting the statement is easy: as we descend towards the -th leaf, we hold at each point a proof for some node in the proof forest, and the hash of the corresponding node in the hash forest. We extract from the proof both the proof of the child to which we descend, and also the hash at that child – recall that the hashes of both children are part of the witness. This allows us to continue our descent, until we arrive at a leaf in the proof forest, which stores the witness , and simultaneously a leaf in the hash forest, which stores the statement .
To extract an opening to index in the hash forest, we rely on the structure of a Merkle tree opening – see Figure 1. The opening is assembled as we recurse down the tree: at each node in the hash tree, we descend to some child (for ), but the witness that we extract provides both and , that is, it provides the sibling of the node to which we descend. We append this sibling to the opening, and continue our descent.
Supporting consistency checks.
Fix a consistency-checking machine . In order to support consistency checks, we store additional information in the proof forest, which allows us to locate and open the last statement added. We also modify the verifiers of the proof forest, to check that this auxiliary information correctly reflects the structure of the forest.
We observe that the opening to index consists of three parts, ordered top-down each of which might be empty (see Figure 1 for an illustration):
-
1.
A prefix consisting of the opening to the lowest common ancestor of and : this part of the opening to index is shared with the opening to index (in Figure 1, the lowest common ancestor is , and the opening to it is ).
-
2.
A middle part consisting of a single node – the right child of the lowest common ancestor of and , where the paths to branch left and right, respectively (in Figure 1, this is ).
-
3.
A suffix consisting of the opening to from the left child of the common ancestor down to index , which must be the rightmost child in the subtree. Importantly, this suffix is the same as the opening from the root of a Merkle tree containing only the first statements (in Figure 1, this is ), which we can compute at the time statement is added (i.e., it does not require us to know what future statements will be added). While the trees containing and/or may be merged with other trees in the future, the opening from the lowest common ancestor of to does not change.
The description above assumes that and are in the same tree in the forest. If they are not, then is the rightmost leaf in its tree, and is the leftmost leaf in its tree; the first two parts described above are empty, and the third part is simply the opening from the root to the rightmost leaf in the tree containing .
We already saw how to extract an opening to index , and during this process we obtain the first two parts of the opening to index : the opening from the root to the lowest common ancestor of and , as well as the right child of (which is on the path down to ). It remains to obtain the third part: the opening to the leaf that precedes the leftmost leaf in ’s subtree.
Obtaining this information at extraction time requires us to store additional information when we construct the hash tree: when a node is constructed, we store at node , where and are the level and hash root (respectively) of the tree containing the leaf immediately preceding the leftmost leaf in ’s subtree, and is the opening to this rightmost leaf (from the root ). We emphasize that this information is computed and stored at construction time, and may be rendered inaccurate by future updates: for example, may no longer be the root of the tree containing the desired leaf, as that tree can be merged with other trees. Nevertheless, our observation above shows that the information we store at construction time is exactly what we need to compute the opening to the preceding statement: as we descend to index , we identify the lowest common ancestor of and , where the path to index diverges from the path to ; we descend to the right child of , and take from to complete the opening to index .
We must also modify the proofs and verifiers at each level, to ensure that the additional information is correct. For nodes at level , the now asserts an asymmetric conjunction, which states as before that the level- verifier accepts each child node (with an appropriate witness), but also that each child of the current node “points correctly” towards the tree containing the leaf that immediately preceded its subtree at construction time: the left child of a node must point towards the same leaf that node itself points to, whereas the right child of must point towards the left child of (hence the asymmetry).
Finally, at each leaf node we additionally store the preceding statement , which allows us to extract together with . The level- verifier checks that accepts (i.e., statement is “consistent” with ), and also that if is the extra information stored at leaf , then indeed opens to at index using the opening .
3.4 Delegating One-Round Massively Parallel Computations
In the MPC model, space-bounded machines communicate in synchronized rounds. Each machine has bits of memory, and in each round it can send and receive messages from any other machine, provided the total number of bits sent or received does not exceed . In this section we outline how we use s to construct a one-round delegation scheme for MPC, which we then lift into using Theorem 1.
One MPC round as a RAM program.
We observe that one round of MPC on machines can be described as a RAM program, which takes a vector of the machines’ initial states , and outputs the machines’ states in the end of the round . Each state or is an -bit vector, where is the space bound of an individual machine. To construct a delegation scheme for one-round-MPC, we imitate a delegation scheme for the program above. However, while a RAM program is executed on a single machine that can access any place in its random-access memory, in the MPC model, the “memory” is partitioned across the machines. Fortunately, existing RAM delegation schemes have the property that constructing the proof does not require access to the entire memory configuration: it is enough to have a hash with local openings of the memory, and openings to the locations that are accessed by the algorithm in each step. Thus, to construct our desired RAM-delegation-like proof for the MPC model, we need to go through the following three stages: (1) Obtain a hash of the state vector ; (2) For each machine , obtain openings of the above hash value to the messages (where ) that machine receives during the round333We assume for simplicity that the messages each machine sends are stored as part of its state at the beginning of the round. ; and (3) Using the openings, prove the transition . The main challenge in this scheme is that each stage must be implemented in the MPC network: we do not truly have random access to the state assignments, because these are actual states of individual machines. For all three stages, our solution is based on having the machines simulate some process on a tree-structured network. This network is an -ary tree with leaves which represent the states of the actual machines, and the rest of the nodes are virtual nodes, simulated by the real machines.
Using a virtual tree-structured network.
To obtain a hash of the state assignment , we aggregate the hash up the tree: the leaves send their state to their parents, and each inner node, upon receiving values from its children, hashes the values it received and sends them up to its parent. The root of the tree then obtains a hash of the entire state assignment. In order for each machine to obtain an opening to its state , we proceed this time down the tree, with each inner node receiving from its parent a partial opening down to its index, extending it to an opening for each of its children’s indices, and sending each extended opening to the corresponding child. Each inner node is able to extend the opening because it is the one that hashed all of its children’s values together. Eventually, each machine receives from its parent a complete opening down to index . Finally, we construct a proof for the alleged RAM computation . To do so, we first observe that this transition is defined by separate computations, and for each , we prove that when the network state assignment is , the next state of machine is . Each such statement can be proved at machine , as follows. Let be a machine that sends message to machine during the round. Recall that after the previous stage, machine has an opening from the global hash to its state . Machine now computes an opening from to and sends this opening to machine . Each machine, upon receiving these openings, uses a RAM-delegation prover to prove that its transition is legal.
The remaining challenge is to aggregate the individual proofs of the machines into one global succinct proof while maintaining soundness. To do this we use the virtual network again: we proceed up the tree, with each node sending its current proof up to its parent. Upon receiving the proofs from its children, each inner node uses an to obtain a proof of the conjunction of its children’s statements. Finally, at the root of the tree, we obtain our one succinct proof for the entire transition . We remark that the soundness of this scheme is non-trivial, and to argue soundness we have to use special properties of the hash family (shortly, that an opening to always contains the hash of ).
3.5 Incrementally Verifying Distributed Graph Algorithms
We briefly discuss how we obtain incrementally verifiable computation for CONGEST algorithms. Importantly, in the delegation schemes which exist for this model [2, 3], the verification takes one communication round between the nodes, and the proof is considered accepted if and only if all nodes accept. For this reason, our does not trivially apply to this model, so we cannot simply apply our lifting theorem to the existing constructions. To resolve this, instead of using the existing delegation schemes to construct directly, we first show that the existing delegation schemes can be transformed into delegation schemes for a different model which verification does not include communication. Instead, the nodes have access to labels which are assigned to their edges. In this model, we can apply our theorem as s are easily implemented there. Finally, we make some observations about the verifier communication in the distributed delegation scheme of [3], which allow us to use only one round of communication to verify many computation rounds.
4 Updatable Hash-and-s (s)
In this section we define and construct an updatable hash-and- scheme, with and without consistency checks. Since the syntax and definition of the two versions mostly overlap, we define the notion once, and give one construction, where all of the parts which are only relevant to the version with consistency checks appear in gray. Specifically, in the syntax some inputs and outputs are obligatory and relevant only for the consistency checks version and in the definition, some properties are extended for the consistency checks version.
Syntax.
An is associated with a recursive hash family with local opening
and consists of the following algorithms.
-
: A randomized setup algorithm that takes as input a security parameter , It outputs a common reference string .
-
: A randomized setup trapdoor algorithm that takes as input a security parameter , and an index . It outputs a common reference string , and a trapdoor .
-
: A deterministic, polynomial-time update algorithm that takes as input a hash key , a common reference string , a machine , a hash value , a proof , and a new statement and witness . Optionally, for the consistency checks version, it also takes a consistency checking machine , and a previous statement . It outputs a hash value and a new proof .
-
: A deterministic, polynomial-time verifier algorithm that takes a hash key , a common reference string , a machine , a hash value , and proof . Optionally, for the consistency checking version, it also takes a consistency check machine and a last statement . It outputs an acceptance bit .
-
: A deterministic, polynomial-time extraction algorithm that takes as input a hash key , a trapdoor , a machine , a hash value , and a proof . Optionally, for the consistency checks version, it also takes a consistency check machine . It outputs a statement , an opening , and a proof . Optionally, in the consistency checks version, it also outputs a previous statement and opening .
Definition 2 ().
An updatable batch argument satisfies the following properties.
Incremental Completeness.
For any , machines , and , hash key in the support of and in the support of :
-
The verifier always accepts an empty proof: .
-
For every , a hash set such that , proof , new statement and witness , and for the consistency checks version, a consistency checks machine and last statement , if , , and , then .
Efficiency and Succinctness.
In the completeness experiment above, after applying for times with instance-witness pairs :
-
The size of the reference string and the size of the hash value are both , and the size of the proof is , where is the maximal size of an instance or a witness for .
-
The verification algorithm runs in time .
Index hiding.
For every poly-size adversary , there exists a negligible function such that for every and index ,
Somewhere Consistent Argument of Knowledge.
For any poly-size adversary , and polynomials , , , for the experiments , defined as follows:
there exists a negligible function such that
and for every and index ,
where for a machine , input , and , if and only if accepts within steps.
Last-Statement Collision-Resistance.
In the version with consistency chekcs, for any poly-size adversary , and polynomial , for the following experiment:
there exists a negligible function such that for every :
Theorem 3.
Updatable hash-and- exist assuming either: (1) Polynomial hardness of LWE; (2) Subexponential hardness of DDH; (3) Polynomial hardness of DDH and -Lin.
4.1 Construction from Rate-1 s and Recursive Hash Families
Let be a rate-1 somewhere extractable batch argument for , and let a collision-resistant hash family ensemble. Let be the recursive hash family with local opening which is the result of constructing Merkle forests from the ensemble ; that is:
-
randomly chooses .
-
uses to construct a Merkle forest over , that is, a set of Merkle trees of descending heights. It outputs the list of roots of trees, each coupled with its height.
-
returns the opening path from the respective tree in the forest.
-
, finds the respective root in using and then checks there that opens to in the respective location using the opening path .
In what follows we describe the construction of an updatable hash-and- scheme .
Moreover, we denote by the set of all heights of roots in the set , and by the size of the hashed content in the set : .
.
-
1.
For every , set . Set .
.
-
1.
Let be ’s bit representation, from least to most significant bit. For every , set . Set and . Set .
We now define a series of verifiers: , using a series of helper, parametrised machines , and a helper algorithm , all of which will take part in the following algorithms .
.
-
1.
Parse: . Parse .
-
2.
Verify: .
-
3.
Verify: .
-
4.
Verify: .
-
5.
If , verify .
-
6.
If , verify .
-
7.
Accept if and only if all checks pass.
for .
-
1.
Parse .
-
2.
If , verify .
Otherwise, verify . -
3.
Parse .
-
4.
If , verify and .
-
5.
If , Verify , and .
-
6.
Accept if and only if all checks pass.
for .
-
1.
Parse , and set (for , set ).
-
2.
Parse: , and .
-
3.
Verify: .
-
4.
Let . Verify .
.
-
1.
Parse .
-
2.
.
-
3.
While there exist such that :444We assume here implicitly that the newer tuple is and the older one is . This could be made formal with more notation, but we decided to omit it for the sake of simplicity and readability.
-
(a)
Set to be such that and .
-
(b)
Set and .
-
(c)
Set .
-
(d)
Set
-
(e)
Let .
-
(f)
Set .
-
(g)
Parse .
-
(h)
Set .
-
(i)
Set .
-
(j)
If , set .
-
(k)
Set .
-
(l)
Set .
-
(a)
-
4.
Output .
We continue to define the remaining algorithms .
.
-
1.
Parse .
-
2.
Set .
-
3.
If , parse , , and set . Otherwise, set , and .
-
4.
Set . Set , and .
-
5.
Set , and .
-
6.
Set .
-
7.
Set , and set to be s.t .
-
8.
Set .
-
9.
Set
-
10.
Output .
.
-
1.
Parse , and for every , set .
-
2.
If either of the following is true, then verify all of them are true, and if so accept and finish: (1) , (2) and (3) . In any other case, continue.
-
3.
Parse , and , and set .
-
4.
Verify that , and that for every , we have .
-
5.
For every , for such that and , verify: (For , omit from the input).
-
6.
Verify .
-
7.
Verify .
-
8.
Verify that and that .
-
9.
Let . Verify .
-
10.
Accept if all checks pass.
.
-
1.
Parse , , and .
-
2.
Let be ’s bit representation, from least significant bit to most significant bit.
-
3.
Set to be such that
-
4.
Parse , and set .
-
5.
Set to be such that and .
-
6.
Set . Set .
-
7.
Set .
-
8.
If , let be the index of the most significant bit where and disagree.
-
9.
While :
-
(a)
Parse , and .
-
(b)
Set , and let . Set .
-
(c)
Set .
-
(d)
Set .
-
(e)
If , , set . If , set .
-
(a)
-
10.
Parse .
-
11.
Set .
-
12.
Output additionally, .
5 One-step Delegation to IVC via UpBARGs
In this section we show how to use to lift a delegation scheme for one step into an , using our , in a generic manner: for deterministic computational models and , we define and construct incrementally verifiable - delegation scheme, in which computations in the model are incrementally proven using a -algorithm to a verifier runs which is in a -algorithm.
Below we formally define our notion of - delegation scheme. We then present our construction.
5.1 Incrementally Verifiable - Delegation.
Syntax.
Incrementally Verifiable - Delegation consists of the following algorithms:
-
: A randomized setup algorithm that takes as input a security parameter and outputs a common reference string .
-
: A -algorithm that takes a reference string , and a configuration . It outputs digest .
-
: A -algorithm that takes a reference string and a label . It outputs digest .
-
: A -algorithm that takes a reference string , a a -algorithm , an initial configuration , a current configuration , a label , a number of steps , a label digest , and a proof . It outputs a new configuration , a new label digest , and a new proof .
-
: A algorithm that takes a reference string , a -algorithm , an initial digest , a possibly empty hash of labels , a final digest , a number of steps , and a proof . It outputs an acceptance bit .
Definition 4 (- Incrementally verifiable Delegation).
A - incrementally verifiable delegation scheme satisfies the same collision resistance succinctness, and soundness properties as a (non-incremental) - delegation scheme. In addition, it satisfies the following incremental completeness property: For any , algorithm and in the support of :
-
The verifier accepts the 0-steps statement with an empty proof. For every hash value : .
-
For every , initial digest , configuration , label , hash of labels and proof , we have that for , if , then where and .
5.2 Construction
In our construction, we use a - delegation scheme, and a - , defined below.
Definition 5 (- ).
A - has the syntax of an updatable hash-and- (see Definition 2) and satisfies the same properties, with the following generalizations:
-
In the input to , instead of being Turing machines, are -algorithms, which can also take labels in their input if is a model of labeled algorithms.
-
is a algorithm and is a algorithm.
-
In the associated hash family , is a -algorithm and is a -algorithm.
Moreover, we use an extension to the usual syntax of hash family with local opening which allows us to hash different vectors separately using the same invocation, that is: . Note that using simply a pair of Merkle trees instead of one allows for such hash families with all the properties of hash families with local opening.
Let be an updatable hash-and- scheme for , associated with the recursive hash family with local openings , which in turn admits the extended syntax mentioned above. Let be a one-step - delegation scheme. For our construction we use the extended syntax for hash sets of the family, and the extended syntax for that is extractable in locations. As with regular s, this could be achieved for s by doubling the proof and CRS size.
We first define for every -algorithm , reference string and hash value two helper -algorithms, and , and then continue to define the scheme’s algorithms.
Helper algorithms and .
-
: If , parse and accept if and only if . Otherwise, Parse and , and verify that .
-
: Parse ,
and verify .
.
-
1.
.
-
2.
.
-
3.
.
-
4.
Output .
.
-
1.
Parse .
-
2.
Parse . (If , set .)
-
3.
Set .
-
4.
Set .
-
5.
Set .
-
6.
Set .
-
7.
Set .
-
8.
Set .
-
9.
Set .
-
10.
Parse .
-
11.
Set .
-
12.
Output .
.
-
1.
Parse .
-
2.
If , verify that and that , and finish. Otherwise, continue.
-
3.
Parse .
-
4.
Parse , and verify that .
-
5.
and verify .
-
6.
Verify .
-
7.
Verify .
-
8.
Accept if all checks pass.
References
- [1] Abtin Afshar and Rishab Goyal. Verifiable streaming computation and step-by-step zero-knowledge. Cryptology ePrint Archive, Paper 2025/251, 2025. URL: https://eprint.iacr.org/2025/251.
- [2] Eden Aldema Tshuva, Elette Boyle, Ran Cohen, Tal Moran, and Rotem Oshman. Locally verifiable distributed SNARGs. In TCC, pages 65–90. Springer, 2023. doi:10.1007/978-3-031-48615-9_3.
- [3] Eden Aldema Tshuva and Rotem Oshman. Fully Local Succinct Distributed Arguments. In DISC, pages 1:1–1:24. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.DISC.2024.1.
- [4] Eli Ben-Sasson, Alessandro Chiesa, Eran Tromer, and Madars Virza. Scalable zero knowledge via cycles of elliptic curves. Algorithmica, 79:1102–1160, 2017. doi:10.1007/S00453-016-0221-0.
- [5] Nir Bitansky, Ran Canetti, Alessandro Chiesa, and Eran Tromer. Recursive composition and bootstrapping for snarks and proof-carrying data. In STOC, pages 111–120, 2013. doi:10.1145/2488608.2488623.
- [6] Alessandro Chiesa and Eran Tromer. Proof-carrying data and hearsay arguments from signature cards. In ICS (Vol. 10), pages 310–331, 2010. URL: http://conference.iiis.tsinghua.edu.cn/ICS2010/content/papers/25.html.
- [7] Arka Rai Choudhuri, Sanjam Garg, Abhishek Jain, Zhengzhong Jin, and Jiaheng Zhang. Correlation intractability and snargs from sub-exponential ddh. In Crypto, pages 635–668. Springer, 2023. doi:10.1007/978-3-031-38551-3_20.
- [8] Arka Rai Choudhuri, Abhishek Jain, and Zhengzhong Jin. Non-interactive batch arguments for NP from standard assumptions. In Annual International Cryptology Conference, pages 394–423. Springer, 2021. doi:10.1007/978-3-030-84259-8_14.
- [9] Arka Rai Choudhuri, Abhishek Jain, and Zhengzhong Jin. SNARGs for P from LWE. In FOCS, pages 68–79, 2021.
- [10] Pratish Datta, Abhishek Jain, Zhengzhong Jin, Alexis Korb, Surya Mathialagan, and Amit Sahai. Incrementally verifiable computation for np from standard assumptions. In Annual International Cryptology Conference, pages 611–642. Springer, 2025. doi:10.1007/978-3-032-01907-3_20.
- [11] Lalita Devadas, Rishab Goyal, Yael Kalai, and Vinod Vaikuntanathan. Rate-1 non-interactive arguments for batch-NP and applications. In FOCS, pages 1057–1068, 2022. doi:10.1109/FOCS54457.2022.00103.
- [12] Yuval Emek, Yuval Gil, and Shay Kutten. Locally Restricted Proof Labeling Schemes. In 36th International Symposium on Distributed Computing (DISC 2022), volume 246, pages 20:1–20:22, 2022. doi:10.4230/LIPIcs.DISC.2022.20.
- [13] Dario Fiore and Ida Tucker. Efficient zero-knowledge proofs on signed data with applications to verifiable computation on data streams. In CCS, pages 1067–1080, 2022. doi:10.1145/3548606.3560630.
- [14] Rachit Garg, Kristin Sheridan, Brent Waters, and David J Wu. Fully succinct batch arguments for NP from indistinguishability obfuscation. In Theory of Cryptography Conference, pages 526–555. Springer, 2022. doi:10.1007/978-3-031-22318-1_19.
- [15] Yael Kalai, Alex Lombardi, Vinod Vaikuntanathan, and Daniel Wichs. Boosting batch arguments and RAM delegation. In Proceedings of the 55th Annual ACM Symposium on Theory of Computing (STOC), pages 1545–1552, 2023. doi:10.1145/3564246.3585200.
- [16] Yael Kalai and Omer Paneth. Delegating ram computations. In TCC, pages 91–118. Springer, 2016.
- [17] Yael Tauman Kalai, Omer Paneth, and Lisa Yang. How to delegate computations publicly. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, pages 1115–1124, 2019. doi:10.1145/3313276.3316411.
- [18] Amos Korman, Shay Kutten, and David Peleg. Proof labeling schemes. In PODC, pages 9–18, 2005. doi:10.1145/1073814.1073817.
- [19] Silvio Micali. Computationally sound proofs. SIAM Journal on Computing, 30(4):1253–1298, 2000. doi:10.1137/S0097539795284959.
- [20] Omer Paneth and Rafael Pass. Incrementally verifiable computation via rate-1 batch arguments. In FOCS, pages 1045–1056, 2022. doi:10.1109/FOCS54457.2022.00102.
- [21] Amit Sahai and Brent Waters. How to use indistinguishability obfuscation: deniable encryption, and more. In Proceedings of the forty-sixth annual ACM symposium on Theory of computing, pages 475–484, 2014. doi:10.1145/2591796.2591825.
- [22] Janwillem Swalens, Lode Hoste, Emad Heydari Beni, and Lieven Trappeniers. zkstream: a framework for trustworthy stream processing. In International Middleware Conference, pages 252–265, 2024. doi:10.1145/3652892.3700763.
- [23] Paul Valiant. Incrementally verifiable computation or proofs of knowledge imply time/space efficiency. In TCC, pages 1–18. Springer, 2008. doi:10.1007/978-3-540-78524-8_1.
- [24] Brent Waters and David J Wu. Batch arguments for NP and more from standard bilinear group assumptions. In Crypto, pages 433–463. Springer, 2022. doi:10.1007/978-3-031-15979-4_15.
