Arithmetization of Functional Program Execution via Interaction Nets in Halo 2

Anthony Hart

Paper 2022/1211

Arithmetization of Functional Program Execution via Interaction Nets in Halo 2

Anthony Hart, Orbis Labs

Abstract

We sketch a method for creating a zero-knowledge proof of knowledge for the correct execution of a program within a model of higher-order, recursive, purely functional programming by leveraging Halo 2. To our knowledge, this is the first ZKP for general purpose computation based on purely functional computation. This is an attractive alternative to using a von Neumann architecture based zero-knowledge virtual machine for verified computing of functional programs, as compilation will be more direct, making it more easily verifiable and potentially more efficient. Interaction nets are a natural setting for recursive, higher-order functional programming where all computation steps are linear and local. Interaction nets are graphs and traces for such programs are hyper-graphs. Correctness of a trace is a simple syntactic check over the structure of the trace represented as a hyper-graph. We reformulate this syntactic check as a Halo 2 circuit which is universal over all traces.

Metadata

Available format(s): PDF
Category: Applications
Publication info: Preprint.
Keywords: Functional Programming Halo 2 Interaction Nets Combinators Lambda Calculus String Diagrams
Contact author(s): team @ orbislabs com
History: 2022-09-14: approved; 2022-09-13: received; See all versions
Short URL: https://ia.cr/2022/1211
License: CC BY

BibTeX

@misc{cryptoeprint:2022/1211,
      author = {Anthony Hart},
      title = {Arithmetization of Functional Program Execution via Interaction Nets in Halo 2},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1211},
      year = {2022},
      note = {\url{https://eprint.iacr.org/2022/1211}},
      url = {https://eprint.iacr.org/2022/1211}
}