A rollup is a scaling solution built on top of an existing blockchain. Rollups separate execution from consensus, but are required to post the data used for state updates to the underlying blockchain. This data is required to ensure that execution of state updates are performed correctly. As writing data to a public blockchain is not free, rollups are incentivized to minimize the amount of data they post on-chain. Rollups therefore aggregate and compress the data used for executions in order to save on fees associated with writing data to the blockchain. In this work, we explore the methods for posting data on-chain and the compression techniques used by real-world rollups. We explore differences in implementations and contrast the approaches used by both optimistic and zero-knowledge rollups. We also explore approaches which enable domain-specific compression, consider upcoming changes to data storage on Ethereum, and suggest improvements for rollup compression.

The blockchain ecosystem has evolved into a multi-chain world with various blockchains vying for use. Although each blockchain may have its own native cryptocurrency or digital assets, there are use cases to transfer these assets between blockchains. Systems that bring these digital assets across blockchains are called bridges, and have become important parts of the ecosystem. The designs of bridges vary and range from quite primitive to extremely complex. However, they typically consist of smart contracts holding and releasing digital assets, as well as nodes that help facilitate user interactions between chains. In this paper we first provide a high level break-down of components in a bridge and the different processes for some bridge designs. Then, we analyse past exploits in the blockchain ecosystem that specifically targeted bridges. In doing this, we identify risks associated with bridge components.

Abstract Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. The first approach lifted from propositional logic delays resolution with unit clauses, which are clauses that have a single literal. The second approach is partial regularization, which removes an inference $\eta $ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $\eta $ to the root of the proof. This paper describes the generalization of the algorithms LowerUnits and RecyclePivotsWithIntersection (Fontaine et al.. Compression of propositional resolution proofs via partial regularization. In Automated Deduction—CADE-23—23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011, p. 237--251. Springer, 2011) from propositional logic to first-order logic. The generalized algorithms compresses resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of these approaches is included.

Models are good at expressing information that is known but do not typically have support for representing what information a modeler does not know or does not care about at a particular stage in the software development process. Partial models address this by being able to precisely represent uncertainty about model content. In previous work, we have defined a general approach for defining partial model semantics using a first order logic encoding. In this paper, we use this FO encoding to formally define the conditions for partial model refinement in the manner of the refinement of algebraic specifications. We use this approach to verify both manual refinements and automated transformation-based refinements. We illustrate our approach using example models and transformations.