Skip to content
This repository has been archived by the owner on Jun 4, 2024. It is now read-only.

Latest commit

 

History

History
17 lines (9 loc) · 2.17 KB

README.md

File metadata and controls

17 lines (9 loc) · 2.17 KB

Stalk

CI

Stalk allows you to write a pure Haskell program and generate a system of arithmetic constraints corresponding to that program. Such constraint languages are often written in terms of a low-level "gadget libraries", or a language that has been specifically tailored for such purposes and only superficially resemble a "normal" programming language. Other approaches attempt to take advantage of existing compilers targeting e.g. RISC-V, but the resulting compiled programs are not "first class" expressions in the language. With Stalk, a pure Haskell expression can be compiled to an equivalent constraint representation which is first class in the Haskell language. These expressions can be futher compiled for use in zero-knowledge protocols using Snarkl and arkworks.

Example

A tutorial is currently in-progress, but it is instructive to compare the sudoku solver written in as pure Haskell expression, versus the one written in the snarkl DSL.

Approach

Stalk implements a Cartesian closed category for snarkl and is meant to build with the Categorifier GHC plugin. This is a very general approach spearheaded by Conal Elliott's work Compiling to Categories. In general, one has to implement the typeclasses for an increasingly expressive cartesian closed category that matches the capability of the target, which in this case is snarkl. The purpose of this library is to follow snarkl closely and to allow as general Haskell expressions as possible to be compiled to constraint languages.

Usage

For tested correct code, see the examples. Due to the utilization of the Categorifier as a GHC plugin, there are some limitations in what versions of GHC that is supported. Look for the example files as well as the nix files for correct usage.