[Resource Topic] 2022/1003: Orbis Specification Language: a type theory for zk-SNARK programming

Welcome to the resource topic for 2022/1003

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

Authors: Morgan Thomas


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.

ePrint: https://eprint.iacr.org/2022/1003

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .