Paper 2022/1003

Orbis Specification Language: a type theory for zk-SNARK programming

Morgan Thomas, Orbis Labs
Abstract

Orbis Specification Language (OSL) is a language for writing statements to be proven by zk-SNARKs. zk-SNARK theories allow for proving wide classes of statements. They usually require the statement to be proven to be expressed as a constraint system, called an arithmetic circuit, which can take various forms depending on the theory. It is difficult to express complex statements in the form of arithmetic circuits. OSL is a language of statements which is similar to type theories used in proof engineering, such as Agda and Coq. OSL has a feature set which is sufficiently limited to make it feasible to compile a statement expressed in OSL to an arithmetic circuit which expresses the same statement. This work builds on Σ¹₁ arithmetization [5] in Halo 2 [3, 4], by defining a frontend for a user-friendly circuit compiler.

Metadata
Available format(s)
PDF
Category
Applications
Publication info
Preprint.
Keywords
arithmetization Halo 2 PLONK second order logic type theory
Contact author(s)
team @ orbislabs com
History
2022-08-10: revised
2022-08-04: received
See all versions
Short URL
https://ia.cr/2022/1003
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2022/1003,
      author = {Morgan Thomas},
      title = {Orbis Specification Language: a type theory for zk-{SNARK} programming},
      howpublished = {Cryptology {ePrint} Archive, Paper 2022/1003},
      year = {2022},
      url = {https://eprint.iacr.org/2022/1003}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.