A Proof-Producing Compiler for Blockchain Applications

• URL: http://arxiv.org/abs/2501.15002v1
• Date: Sat, 25 Jan 2025 00:31:47 GMT
• Title: A Proof-Producing Compiler for Blockchain Applications
• Authors: Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman,
• Abstract summary: CairoZero is a programming language for running decentralized applications (dApps) at scale. cryptographic protocols are used to verify the results of execution efficiently on blockchain. We show how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications.
• Score: 0.0873811641236639
• License:
• Abstract: CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications. We demonstrate the success of our approach by verifying primitives for computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach.

Related papers

• Commit0: Library Generation from Scratch [77.38414688148006]
  Commit0 is a benchmark that challenges AI agents to write libraries from scratch. Agents are provided with a specification document outlining the library's API as well as a suite of interactive unit tests. Commit0 also offers an interactive environment where models receive static analysis and execution feedback on the code they generate.
  arXiv  Detail & Related papers  (2024-12-02T18:11:30Z)
• The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
  We study the interplay between threshold cryptography and a class of blockchains that use Byzantine-fault tolerant (BFT) consensus protocols. Existing approaches for threshold cryptosystems introduce a latency overhead of at least one message delay for running the threshold cryptographic protocol. We propose a mechanism to eliminate this overhead for blockchain-native threshold cryptosystems with tight thresholds.
  arXiv  Detail & Related papers  (2024-07-16T20:53:04Z)
• Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
  We advocate using secure program partitioning to synthesize cryptographic applications. This approach is promising, but formal results for the security of such compilers are limited in scope. We develop a compiler security proof that handles subtleties essential for robust, efficient applications.
  arXiv  Detail & Related papers  (2024-01-06T02:57:44Z)
• Towards a zk-SNARK compiler for Wolfram language [0.0]
  This project builds upon Wolfram's ZeroKnowledgeProofs paclet and implements a zk-SNARK compiler based on Pinocchio protocol. Interactive proofs are not suited for blockchain applications but novel protocols such as zk-SNARKs have made zero-knowledge ledgers like Zcash possible.
  arXiv  Detail & Related papers  (2024-01-05T18:24:32Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  We propose Chain of Code, a simple yet surprisingly effective extension that improves LM code-driven reasoning. The key idea is to encourage LMs to format semantic sub-tasks in a program as flexible pseudocode that the interpreter can explicitly catch.
  arXiv  Detail & Related papers  (2023-12-07T17:51:43Z)
• Molly: A Verified Compiler for Cryptoprotocol Roles [0.0]
  Molly compiles cryptographic protocol roles into straight-line programs. We define a denotational semantics for protocol roles based on an axiomatization of the runtime.
  arXiv  Detail & Related papers  (2023-11-22T21:04:07Z)
• Exploring Continual Learning for Code Generation Models [80.78036093054855]
  Continual Learning (CL) is an important aspect that remains underexplored in the code domain. We introduce a benchmark called CodeTask-CL that covers a wide range of tasks, including code generation, translation, summarization, and refinement. We find that effective methods like Prompt Pooling (PP) suffer from catastrophic forgetting due to the unstable training of the prompt selection mechanism.
  arXiv  Detail & Related papers  (2023-07-05T16:58:39Z)
• Bounding the quantum value of compiled nonlocal games: from CHSH to BQP verification [2.298932494750101]
  Kalai et al. defined a black-box cryptographic compilation procedure that applies to any nonlocal game. We make progress towards a full understanding of the quantum value of the single-prover protocols. We give a single-prover cryptographically sound classical verification protocol for BQP, and we prove its soundness using our CHSH rigidity analysis.
  arXiv  Detail & Related papers  (2023-03-02T19:20:59Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  cryptography has been an exception, where many performance-critical routines have been written directly in assembly. We present CryptOpt, the first compilation pipeline that specializes high-level cryptographic functional programs into assembly code significantly faster than what GCC or Clang produce. On the formal-verification side, we connect to the FiatOpt framework (which translates functional programs into C-like IR code) and extend it with a new formally verified program-equivalence checker.
  arXiv  Detail & Related papers  (2022-11-19T11:07:39Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  We propose a retrieval-augmented code completion framework, leveraging both lexical copying and referring to code with similar semantics by retrieval. We evaluate our approach in the code completion task in Python and Java programming languages, achieving a state-of-the-art performance on CodeXGLUE benchmark.
  arXiv  Detail & Related papers  (2022-03-15T08:25:08Z)
• Extending C++ for Heterogeneous Quantum-Classical Computing [56.782064931823015]
  qcor is a language extension to C++ and compiler implementation that enables heterogeneous quantum-classical programming, compilation, and execution in a single-source context. Our work provides a first-of-its-kind C++ compiler enabling high-level quantum kernel (function) expression in a quantum-language manner.
  arXiv  Detail & Related papers  (2020-10-08T12:49:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.