### Arithmetization of Functional Program Execution via Interaction Nets in Halo 2

##### 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.

Available format(s)
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
See all versions
Short URL
https://ia.cr/2022/1211

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}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.