Snaarkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell
Verifiable computing (VC) uses cryptography to delegate computation to untrusted workers. But in most VC schemes, the delegated program must first be arithmetized – expressed as a circuit with multiplication and addition over a finite field. Previous work has compiled subsets of languages like C, LLVM, and bespoke assembly to arithmetic circuits. In this paper, we report on a new DSL for VC, called Snaarkl (``Snorkel''), that supports encodings of language features familiar from functional programming such as products, case analysis, and inductive datatypes. We demonstrate that simple constraint-minimization techniques are an effective means of optimizing and solving the resulting encodings, and therefore of generating and constructing witnesses for small circuits.
Tue 9 JanDisplayed time zone: Tijuana, Baja California change
10:30 - 12:00
|Hygienic Source-Code Generation Using Functors|
A: Karl Crary Carnegie Mellon University
|Snaarkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell|
|Rewriting High-Level Spreadsheet Structures into Higher-Order Functional Programs|