Arithmetization of Σ¹₁ relations with polynomial bounds in Halo 2

Arithmetization of Σ¹₁ relations with polynomial bounds in Halo 2

image

We're excited to announce our third publication, which is a follow-up to our first paper. Arithmetization of Σ¹₁ relations with polynomial bounds in Halo 2 is Orbis Labs' latest publication on Σ¹₁ arithmetization written by Anthony Hart and Morgan Thomas. This paper greatly simplifies the definition of Σ¹₁ arithmetization while also making it far more efficient for certain use cases. The theoretical simplification comes from introducing more stages into the compilation process, allowing for greater separation of concerns in the definition of Σ¹₁ arithmetization. The efficiency gains come from allowing quantifier bounds to be variable, instead of constant. This reduces the number of rows required in the resulting circuit when dealing with nested data structures, such a list of variable-length lists.

Σ¹₁ arithmetization is a process for compiling a spec of a set of facts to be proven into an arithmetic circuit for proving those facts in zk-SNARKs. Orbis Labs is building a formally verified circuit compiler based on Σ¹₁ arithmetization. This will reduce the effort required to create a correct arithmetic circuit, by reducing it to the problem of creating a correct spec. If the spec is correct, then the correctness proof of the circuit compiler will imply that the resulting circuit is correct. If the spec is correct and the underlying proving system is sound, then the statements proven by the resulting zk-SNARKs are true, with overwhelming probability.

We look forward to our future publications which will further outline the techniques and technologies we are using to build Orbis, the first general purpose layer 2 scaling solution for Cardano.

Posts

Footer Links