Hamburger Factory Validity

Apr 15

Cover image by @gajis_amy. Special thanks to @QiuhaoLi and @opensensepw for feedback and review.

Validity Proof

We have three numbers: A, B, C, and we need to sort them in ascending order.

Here’s how we do it in Python:

if A > B:
    A, B = B, A
if A > C:
    A, C = C, A
if B > C:
    B, C = C, B
    
print(A, B, C)

And here’s how it’s done in a circuit-fashion, the only operation is enforce.

input: A, B, C

enforce({A', B', C'} is a permutation of {A, B, C})
enforce(A' <= B')
enforce(B' <= C')

output: A', B', C'

What's the difference? In the circuit approach, we are not concerned with the process to achieve the result, but only that the result is correct. This is written in a non-constructive way. Our goal is to ensure that valid executions always satisfy all the constraints, while invalid executions can never satisfy all the constraints.

Hamburger Validity Proof

Alice goes to McDonald's and orders a hamburger. She wants to use a zk circuit to prove the hamburger is fresh and delicious.

Suppose she already knows that the only ingredients are bread and vegetables, with a maximum of 5 pieces of each and a possibility of having zero bread or vegetables.

She builds a magical hamburger deconstruction machine:

input: hamburger h

enforce(h is made from B[] and V[])

output: breads B[], vegetables V[]

Then, she builds a bread checker, which takes bread from the array and check them one by one. In addition to the input and output, we need to introduce some intermediate variables. Unlike the input and output, the values of intermediate variables are not predetermined. We can assign any value to them as long as they satisfy all the constraints:

input: breads B[]

for i in range(5) {
    enforce(if B is nonempty then flag is true, else flag is false)
    enforce(if flag is true, then b = pop(B))
    enforce(if flag is true, then b is fresh and delicious)
}

output: None

To make it clearer, let’s expand on what the actual intermediate variables are:

intermediate variables: B0, b0, flag0, B1, b1, flag1, ...

enforce(B0 = B)
// round 1
enforce(if B0 is nonempty then flag0 is true, else flag0 is false)
enforce(if flag0 is true, then (b0, B1) = pop(B0))
enforce(if flag0 is true, then b0 is fresh and delicious)
// round 2
enforce(if B1 is nonempty then flag1 is true, else flag1 is false)
enforce(if flag1 is true, then (b1, B2) = pop(B1))
enforce(if flag1 is true, then b1 is fresh and delicious)
......

The same process applies for the vegetable checker.

input: vegetables V[]

for i in range(5) {
    enforce(if V is nonempty then flag is true, else flag is false)
    enforce(if flag is true, then v = pop(V))
    enforce(if flag is true, then v is fresh and delicious)
}

output: None

Finally, she builds a conveyor belt circuit, we use fit(circuit c, input i, output o) to denote that the input i and output o (along with some intermediate variables) satisfy all the constraints in the circuit c.

input: hamburger h

enforce(fit(deconstruction machine, hamburger h, (breads B[], vegetables V[])))
enforce(if B[] is nonempty, then fit(bread checker, B[], ()))
enforce(if V[] is nonempty, then fit(vegetable checker, V[], ()))

output: None

One might question why the checker's output is 'none'; shouldn't it indicate good or bad? Since a good hamburger satisfies all the constraints, we can generate a proof stating that it's good. Conversely, bad hamburgers, which contain at least one piece that is not fresh or delicious, will never satisfy all the constraints and therefore can never be proven to be good. Thus, we do not need an explicit output.

Done, can you spot the bug?

(Stop and Think!!!!!!)

There's no bug—just kidding.

Remember there is a prerequisite that there are at most 5 pieces of bread and 5 pieces of vegetables in it. Let's consider what happens if the actual upper bound is 6?

We could have a bad hamburger which contains a spoiled tomato at the end of the array. Since we only check the first five, the bad tomato would be overlooked. We could still generate a proof that claims the hamburger is good! This is known as a soundness bug (rip Alice).

What if the original circuit is modified to:

input: breads B[]

for i in range(5) {
    enforce(if B is nonempty then flag is true, else flag is false)
    enforce(if flag is true, then b = pop(B))
    enforce(if flag is true, then b is fresh and delicious)
}
enforce(B is now empty)

output: None

Then, a bad hamburger will not satisfy the newly added constraints. However, we won't be able to prove that a good hamburger with 6 pieces is good. This results in what is known as a completeness bug.

Hamburger Factory Validity Proof

Now, the real challenge begins. Alice wants to bring zk technology into the hamburger factory. The maximum limit is set to 5 again. (we don't care about larger inputs)

input: raw breads rB[], raw vegetables rV[]

enforce(if rB[] is nonempty, then fit(bread baker, raw breads rB[], cooked breads cB[]))
enforce(if rV[] is nonempty, then fit(vegetable baker, raw vegetables rV[], cooked vegetables cV[]))
enforce(fit(assembly machine, (cB[], cV[]), hamburger H))

output: hamburger H

Here is the bread baker below:

input: raw breads rB[]

enforce(cooked bread cB[] is empty at first)
for i in range(5) {
    enforce(if rB is nonempty then flag is true, else flag is false)
    enforce(if flag is true, then rb = pop(rB))
    enforce(if flag is true, then cb is baked from rb)
    enforce(if flag is true, then cB.push(cb))
}

output: cooked breads cB[]

And the vegetable baker:

input: raw vegetables rV[]

enforce(cooked vegetables cV[] is empty at first)
for i in range(5) {
    enforce(if rV is nonempty then flag is true, else flag is false)
    enforce(if flag is true, then rv = pop(rV))
    enforce(if flag is true, then cv is baked from rv)
    enforce(if flag is true, then cV.push(cv))
}

output: cooked vegetables cV[]

Finally, the super assembly machine:

input: cooked breads cB[], cooked vegetables cV[] 

enforce(h is made from cB[] and cV[])

output: hamburger h

Can you spot the bug?

(Since this is an open scenario, you might find some answers that seem reasonable. However, if you're not 100% confident in your answer, it's likely you haven't found the one I hope you to find.)

Winnie X