feat: optimise constraints arising from control-flow

[DavePearce]

Summary

Consider the following simple program (basic_32.zkc):

pub input data(address:u16) -> (byte:u16)

// prove that two numbers add up to a third.
fn main() {
    var n:u16 = data[0]
    var r:u16 = data[1]
    var i:u16 = 0
    var v:u16 = 1
    //
    while i != n {
        v = v + v
        i = i + 1
    }
    //
    if v != r {
        fail
    }
}

This generates the following MIR constraints:

And then the following (abbreviated) AIR constraints:

(module data)

(inputs
   (address u16 0x0)
)

(outputs
   (byte u16 0x0)
)


(module main)

(computed
   (n u16 0x0)
   (r u16 0x0)
   (i u16 0x0)
   (v u16 0x0)
   ($4 u0 0x0)
   ($5 u1 0x0)
   ($pc u2 0x0)
   ($ret u1 0x0)
   ("(inv main:$pc)" 𝔽 0x0)
   ("(inv (- main:$pc 1))" 𝔽 0x7f000000)
   ("(inv (- main:n main:i))" 𝔽 0x0)
   ("(inv (- main:r main:v))" 𝔽 0x0)
   ("(inv (- main:$pc 2))" 𝔽 0x3f800000)
   ("(inv (- (shift main:n -1) main:i))" 𝔽 0x0)
   ("(inv (- (shift main:r -1) main:v))" 𝔽 0x0)
)
...
(vanish main:pc0#0 (* (- 1 (* (- $pc 1) "(inv (- main:$pc 1))")) $4))
(vanish main:pc0#1 (* (- 1 (* (- $pc 1) "(inv (- main:$pc 1))")) (- $5 1)))
(vanish main:pc0#2 (* (- 1 (* (- $pc 1) "(inv (- main:$pc 1))")) i))
(vanish main:pc0#3 (* (- 1 (* (- $pc 1) "(inv (- main:$pc 1))")) (- v 1)))
(vanish main:pc0#4 (
   *
   (- 1 (* (- $pc 1) "(inv (- main:$pc 1))"))
   (- n i)
   (- (shift $pc "1") 2)))

(vanish main:pc0#5 (* (- 1 (* (- $pc 1) "(inv (- main:$pc 1))")) (- n i) $ret))
(vanish main:pc0#6 (
   *
   (- 1 (* (- $pc 1) "(inv (- main:$pc 1))"))
   (- 1 (* (- n i) "(inv (- main:n main:i))"))
   (- r v)))

(vanish main:pc0#7 (
   *
   (- 1 (* (- $pc 1) "(inv (- main:$pc 1))"))
   (- 1 (* (- n i) "(inv (- main:n main:i))"))
   (- 1 (* (- r v) "(inv (- main:r main:v))"))
   (- $ret 1)))
...

What we see is a lot of repetition in the generated constraints (e.g. (- 1 (* (- $pc 1) "(inv (- main:$pc 1))")))

Approach

A simple approach to this optimisation is to transform a ZkC program into a form where conditionals are represented using binary "control lines". So, for example, this:

fn max(x:u16, y:u16) -> (z:u16) {
   if x > y {
      z = x
   } else { z = y }
}

becomes this:

fn max(x:u16, y:u16) -> (z:u16) {
   var $1:u1 = x > y
   //
   if $1 {
      z = x
   } else { z = y }
}

There are some challenges with this, as care must be taken to ensure the transformation produces an equivalent program.