Paper 2022/1211 Original: eprint.iacr.org/2022/1211 ↗
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.
Metadata
- Available format(s)
PDF- Category
- Applications
- Publication info
- Preprint.
- History
- 2022-09-13: last updated
- 2022-09-13: published
- Short URL
- https://ia.cr/2022/1211
- License
- https://creativecommons.org/licenses/by/4.0/
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},
url = {https://eprint.iacr.org/2022/1211}
}