Orbis Specification Language (OSL)
Last updated
Last updated
Designing and coding arithmetic circuits manually are laborious and error-prone. Therefore, Orbis Labs sought an automated method of creating arithmetic circuits. The goal of this research is to enable the relations to be arithmetized, to be written in a specification language, without any nonessential implementation details, and then transform those specifications into code to build arithmetic circuits.
The only way to validate the specification is to be able to look at it and know intuitively that it does specify the intended relation. For this, the specification must be as obvious and clear as practicable.
Programming languages do not necessarily make good specification languages. For this reason, instead of leveraging an existing zk-SNARK programming language, Orbis Labs opted to create a new specification language for expressing the Orbis rollup validity relations. This specification language must satisfy two design constraints:
It must allow the Orbis rollup validity relations to be fluently expressed without nonessential information.
A provably correct and reasonably efficient method must exist for translating the specification into a Halo 2 circuit.
For these purposes, Orbis Labs created the Orbis Specification Language (OSL).
Orbis Specification Language (OSL) is similar to languages like Haskell and Coq, which can express statements in a math-like, machine-readable notation. The difference is that OSL is engineered to be amenable to translation into a form which can be used to make zk-SNARK proofs. OSL takes away the zk-SNARK engineer's burden of making a non-obvious translation of a statement into a form which can be proven by a zk-SNARK.
Our published paper is shown below:
Orbis Labs is investigating two approaches for scaling the proof system by using recursion.
In the first approach, proofs are passed as parameters in the OSL spec, which asserts that the proofs are verifiable. This approach is more straightforward to understand, but it has the disadvantage of adding incidental complexity to the spec, and the use of recursive proofs would not be expressed as part of the spec.
The next potential approach incorporates recursive proofs into the Σ¹₁ arithmetization scheme. The concept is that we would like to prove a statement for which the corresponding circuit would have a potentially infinite number of rows. A feature which Halo 2 does not support.