A Brainfuck zkVM to prove correct execution of a Brainfuck program with secret inputs.

Brainfuck is a Turing-complete language that has only 8 operations defined as follows:

Any other symbol is ignored, and may effectively be used as comments.

We have written a Brainfuck compiler & runner in Go, which you can find under the vm folder. Assuming you have Go installed, you can build the binary simply via:

yarn vm:build

Afterwards, you can run the binary with:

yarn vm:run
  -clocks int
    # maximum number of "clock cycles" (default 65536)
  -code string
    # brainfuck code (default ",+++++[-.]")
  -memory int
    # memory size (default 128)
  -num
    # use numbers for input & output
  -path string
    # path to file with brainfuck code
  -verbose
    # print compiled code

You may find a few example Brainfuck codes in here. To run them, pass their paths via the -path option. By default, the VM will run ,+++++[-.] which takes an input, increments it 5 times and then starts decrementing it, printing the value each time.

Our objective with zkBrainfuck is to prove correct execution of Brainfuck while hiding our inputs. To do that, instead of writing the Brainfuck VM as a circuit itself, we will write a constraining circuit that checks the execution steps and confirm that these steps are valid for a Brainfuck program.

To re-iterate what we mean here, consider a square-root circuit where given n it outputs sqrt(n). Well, instead of doing that square-root stuff in a circuit, we could ask for an input m that will be output directly, and add a constraint such that n === m * m which makes things so much easier while still providing execution correctness.

With that said, let us define the requirements for the circuit to prove a step of execution:

• Current input in
• Current output out
• Current & next instruction i and _i
• Current & next memory layouts m and _m
• Current & next memory pointers p and _p

These inputs are given for each clock cycle. Only the the list of instructions and outputs are public, the rest are private inputs.

zkBrainfuck operates over numbers instead of tokens, and we want this to be as circuit-friendly as possible. For that, the following methodology is used (think for each clock cycle):

To disambugate op values from jump targets, compiled code will be prepended with 7 zeros, one for each op. This way, op checks can be made with number comparisons and jump targets are safe. The circuit only has to assert that (TODO: maybe make no-op 7 and rest be from 0..6?)

• Typefuck is a Brainfuck interpreter using the type-system of Typescript alone.
• How Brainfuck Works is a great Gist about Brainfuck.
• Brainfuck in STARK is a quite nice example of another zkBrainfuck based on STARK.
• Brainfuck in Golang is another implementation of Brainfuck in go.