Mapping finite state machines to zk-SNARKS Using Category Theory

TL;DR

This paper introduces a categorical method to convert finite state machine graphs into boolean circuits suitable for zk-SNARKs, enabling efficient proof systems for path verification in graphs.

Contribution

It presents a novel categorical framework for mapping finite state machine graphs to boolean circuits for zk-SNARKs, including generalizations to arbitrary graphs.

Findings

Circuits verify paths in finite state machine graphs.

The categorical mappings are pseudofunctorial.

Framework generalizes to arbitrary graph path verification.

Abstract

We provide a categorical procedure to turn graphs corresponding to state spaces of finite state machines into boolean circuits, leveraging on the fact that boolean circuits can be easily turned into zk-SNARKS. Our circuits verify that a given sequence of edges and nodes is indeed a path in the graph they represent. We then generalize to circuits verifying paths in arbitrary graphs. We prove that all of our correspondences are pseudofunctorial, and behave nicely with respect to each other.