2 Search Results for "Goldberg, Lior"

Document
DOI: 10.4230/LIPIcs.ITP.2023.7
A Proof-Producing Compiler for Blockchain Applications

Authors: Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Cairo is a programming language for running decentralized applications (dapps) at scale. Programs written in the Cairo language are compiled to machine code for the Cairo CPU architecture, and cryptographic protocols are used to verify the results of the execution traces efficiently on blockchain. We explain how we have extended the Cairo 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 computations with an elliptic curve over a large finite field, as well as their use in the validation of cryptographic signatures.
Cite as

Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman. A Proof-Producing Compiler for Blockchain Applications. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{avigad_et_al:LIPIcs.ITP.2023.7,
  author =	{Avigad, Jeremy and Goldberg, Lior and Levit, David and Seginer, Yoav and Titelman, Alon},
  title =	{{A Proof-Producing Compiler for Blockchain Applications}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.7},
  URN =		{urn:nbn:de:0030-drops-183820},
  doi =		{10.4230/LIPIcs.ITP.2023.7},
  annote =	{Keywords: formal verification, smart contracts, interactive proof systems}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.5
DEEP-FRI: Sampling Outside the Box Improves Soundness

Authors: Eli Ben-Sasson, Lior Goldberg, Swastik Kopparty, and Shubhangi Saraf

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
Motivated by the quest for scalable and succinct zero knowledge arguments, we revisit worst-case-to-average-case reductions for linear spaces, raised by [Rothblum, Vadhan, Wigderson, STOC 2013]. The previous state of the art by [Ben-Sasson, Kopparty, Saraf, CCC 2018] showed that if some member of an affine space U is δ-far in relative Hamming distance from a linear code V - this is the worst-case assumption - then most elements of U are almost-δ-far from V - this is the average case. However, this result was known to hold only below the "double Johnson" function of the relative distance δ_V of the code V, i.e., only when δ < 1-(1-δ_V)^(1/4). First, we increase the soundness-bound to the "one-and-a-half Johnson" function of δ_V and show that the average distance of U from V is nearly δ for any worst-case distance δ smaller than 1-(1-δ_V)^(1/3). This bound is tight, which is somewhat surprising because the one-and-a-half Johnson function is unfamiliar in the literature on error correcting codes. To improve soundness further for Reed Solomon codes we sample outside the box. We suggest a new protocol in which the verifier samples a single point z outside the box D on which codewords are evaluated, and asks the prover for the value at z of the interpolating polynomial of a random element of U. Intuitively, the answer provided by the prover "forces" it to choose one codeword from a list of "pretenders" that are close to U. We call this technique Domain Extending for Eliminating Pretenders (DEEP). The DEEP method improves the soundness of the worst-case-to-average-case reduction for RS codes up their list decoding radius. This radius is bounded from below by the Johnson bound, implying average distance is approximately δ for all δ < 1-(1-δ_V)^(1/2). Under a plausible conjecture about the list decoding radius of Reed-Solomon codes, average distance from V is approximately δ for all δ. The DEEP technique can be generalized to all linear codes, giving improved reductions for capacity-achieving list-decodable codes. Finally, we use the DEEP technique to devise two new protocols: - An Interactive Oracle Proof of Proximity (IOPP) for RS codes, called DEEP-FRI. The soundness of the protocol improves upon that of the FRI protocol of [Ben-Sasson et al., ICALP 2018] while retaining linear arithmetic proving complexity and logarithmic verifier arithmetic complexity. - An Interactive Oracle Proof (IOP) for the Algebraic Linking IOP (ALI) protocol used to construct zero knowledge scalable transparent arguments of knowledge (ZK-STARKs) in [Ben-Sasson et al., eprint 2018]. The new protocol, called DEEP-ALI, improves soundness of this crucial step from a small constant < 1/8 to a constant arbitrarily close to 1.
Cite as

Eli Ben-Sasson, Lior Goldberg, Swastik Kopparty, and Shubhangi Saraf. DEEP-FRI: Sampling Outside the Box Improves Soundness. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 5:1-5:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bensasson_et_al:LIPIcs.ITCS.2020.5,
  author =	{Ben-Sasson, Eli and Goldberg, Lior and Kopparty, Swastik and Saraf, Shubhangi},
  title =	{{DEEP-FRI: Sampling Outside the Box Improves Soundness}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{5:1--5:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.5},
  URN =		{urn:nbn:de:0030-drops-116901},
  doi =		{10.4230/LIPIcs.ITCS.2020.5},
  annote =	{Keywords: Interactive Oracle Proofs of Proximity, STARK, Low Degree Testing}
}
  • Refine by Author
  • 2 Goldberg, Lior
  • 1 Avigad, Jeremy
  • 1 Ben-Sasson, Eli
  • 1 Kopparty, Swastik
  • 1 Levit, David
  • Show More...

  • Refine by Classification
  • 1 General and reference → Verification
  • 1 Mathematics of computing → Coding theory
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation → Interactive proof systems
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 Interactive Oracle Proofs of Proximity
  • 1 Low Degree Testing
  • 1 STARK
  • 1 formal verification
  • 1 interactive proof systems
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2020
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact