Skip to content

Commit

Permalink
vm completed more or less
Browse files Browse the repository at this point in the history
  • Loading branch information
@erhant
erhant committed Jul 18, 2023
1 parent 6a61318 commit 2d01944
Show file tree
Hide file tree
Showing 9 changed files with 328 additions and 124 deletions.
5 changes: 4 additions & 1 deletion .gitignore
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
node_modules
build
circuits/test
circuits/main
circuits/main

# ignore binary
vm/bin/main
21 changes: 21 additions & 0 deletions LICENSE
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
MIT License

Copyright (c) 2023 Erhan Tezcan

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
104 changes: 64 additions & 40 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -1,60 +1,84 @@
# Circomfuck
# zkBrainfuck

> A [Brainfuck](https://en.wikipedia.org/wiki/Brainfuck) ZKVM to prove correct execution of a Brainfuck program.
> A [Brainfuck](https://en.wikipedia.org/wiki/Brainfuck) zkVM to prove correct execution of a Brainfuck program with secret inputs.
Brainfuck has 8 operations defined as follows:
Brainfuck is a Turing-complete language that has only 8 operations defined as follows:

| Code | Operation |
| ---- | ----------------------------------------------- |
| `>` | increment data pointer |
| `<` | decrement data pointer |
| `+` | increment pointed data |
| `-` | decrement pointed data |
| `.` | read from pointed data |
| `,` | write to pointed data |
| `[` | if pointed data is non-zero, go to matching `]` |
| `]` | if pointed data is non-zero, go to matching `[` |
| Code | Operation |
| ---- | ------------------------------------------------ |
| `>` | increment data pointer |
| `<` | decrement data pointer |
| `+` | increment pointed data |
| `-` | decrement pointed data |
| `.` | read from pointed data |
| `,` | write to pointed data |
| `[` | if pointed data is zero, `goto` matching `]` |
| `]` | if pointed data is non-zero, `goto` matching `[` |

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

Consider a data pointer `p`, a current memory `m` and next memory `m'` where `m[p]` refers to the data pointed by the pointer `p` in that state. Likewise, data pointer in the next state is `p'`. Let `i'` denote the current instruction pointer and `i'` the next instruction pointer.
## Virtual Machine

We have the following operations defined in Brainfuck in terms of state changes per instruction:
We have written a Brainfuck compiler & runner in Go, which you can find under the [vm](./vm/) folder. Assuming you have Go installed, you can build the binary simply via:

| Number | Token | Operation |
| ------ | ----- | --------------------------------- |
| 62 | `>` | `p' <== p + 1` |
| 60 | `<` | `p' <== p - 1` |
| 43 | `+` | `m'[p] <== m[p] + 1` |
| 45 | `-` | `m'[p] <== m[p] - 1` |
| 46 | `.` | `out <== m[p]` |
| 44 | `,` | `m'[p] <== in` |
| | `[` | if `m[p] != 0` then `i' <== j[i]` |
| | `]` | if `m[p] != 0` then `i' <== j[i]` |
```sh
yarn vm:build
```

Number refers to the value returned by `charCodeAt` (in JS) for that character, yielding the ASCII value. We will treat the corresponding field elements for instruction codes.
Afterwards, you can run the binary with:

```sh
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
```

If not specified otherwise, the following happens during the state transition:
You may find a few example Brainfuck codes in [here](./vm/code). To run them, pass their paths via the `-p` 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.

- `p' <== p` data pointer stays the same
- `i' <== i + 1` instruction pointer is incremented
- `m'[:] <== m[:]` memory blocks stay the same
## Proving Execution

If an unknown token is received, it is ignored and default behavior state transitions occur.
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.

### Looping
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.

To make looping more snark-friendly, we will replace the `[` and `]` with their respective target position in the code. For example:
With that said, let us define the requirements for the circuit to prove a step of execution:

```bf
0 1 2 3 4 5 6 7 8 # position
> + + [ + - - ] + . # input
> + + 6 + - - 2 + . # converted
```
- Current memory layout `m`
- Next memory layout `m'`
- Current instruction pointer `i`
- Next instruction pointer `i'`
- Current memory pointer `p`
- Next memory pointer `p'`

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:

| `op` | Code | Operation |
| ------- | ---- | -------------------------------------------------- |
| 0 | | ignore |
| 1 | `>` | `p' <== p + 1` and `i <== i + 1` |
| 2 | `<` | `p' <== p - 1` and `i <== i + 1` |
| 3 | `+` | `m'[p] <== m[p] + 1` and `i <== i + 1` |
| 4 | `-` | `m'[p] <== m[p] - 1` and `i <== i + 1` |
| 5 | `.` | `out <== m[p]` and `i <== i + 1` |
| 6 | `,` | `m'[p] <== in` and `i <== i + 1` |
| $i > 6$ | `[` | if `m[p] == 0` then `i' <== op` else `i <== i + 1` |
| $j > 6$ | `]` | if `m[p] != 0` then `i' <== op` else `i <== i + 1` |

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?)**

## Honorable Mentions

- [Typefuck](https://github.com/susisu/typefuck) is a Brainfuck interpreter using the type-system of Typescript alone.
- [How Brainfuck Works](https://gist.github.com/roachhd/dce54bec8ba55fb17d3a) is a great Gist about Brainfuck.
- [Brainfuck in STARK](https://neptune.cash/learn/brainfuck-tutorial/) is a quite nice example of another zkBrainfuck.
- [Brainfuck in STARK](https://neptune.cash/learn/brainfuck-tutorial/) is a quite nice example of another zkBrainfuck based on STARK.
- [Brainfuck in Golang](https://github.com/kgabis/brainfuck-go/blob/master/bf.go) is another implementation of Brainfuck in go.
2 changes: 1 addition & 1 deletion circuits/brainfuck.circom
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ include "./vm.circom"
// MEM: memory size
// LEN: code size
// CLK: number of clock-cycles
template Brainfuck(MEM, LEN, CLK) {
template Brainfuck(MEMORY, CLOCKS) {
signal input code[LEN];

component vm = VM(MEM);
Expand Down
10 changes: 6 additions & 4 deletions package.json
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,14 @@
{
"author": "erhant",
"license": "MIT",
"private": true,
"scripts": {
"test": "npx mocha"
},
"dependencies": {
"circomkit": "^0.0.14"
"test": "npx mocha",
"vm:run": "./vm/bin/main",
"vm:build": "cd vm && go build -o ./bin/main -ldflags \"-s -w\" main.go"
},
"devDependencies": {
"circomkit": "^0.0.14",
"@types/mocha": "^10.0.1",
"mocha": "^10.2.0",
"ts-node": "^10.9.1",
Expand Down
22 changes: 22 additions & 0 deletions vm/code/example.bf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
(example from wikipedia)
++ Cell c0 = 2
> +++++ Cell c1 = 5
[ Start your loops with your cell pointer on the loop counter (c1 in our case)
< + Add 1 to c0
> - Subtract 1 from c1
] End your loops with the cell pointer on the loop counter
At this point our program has added 5 to 2 leaving 7 in c0 and 0 in c1
but we cannot output this value to the terminal since it is not ASCII encoded
To display the ASCII character "7" we must add 48 to the value 7
We use a loop to compute 48 = 6 * 8
++++ ++++ c1 = 8 and this will be our loop counter again
[
< +++ +++ Add 6 to c0
> - Subtract 1 from c1
]
< . Print out c0 which has the value 55 which translates to "7"!
46 changes: 46 additions & 0 deletions vm/code/helloworld.bf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
(example from wikipedia)
[ This program prints "Hello World!" and a newline to the screen, its
length is 106 active command characters. [It is not the shortest.]
This loop is an "initial comment loop", a simple way of adding a comment
to a BF program such that you don't have to worry about any command
characters. Any ".", ",", "+", "-", "<" and ">" characters are simply
ignored, the "[" and "]" characters just have to be balanced. This
loop and the commands it contains are ignored because the current cell
defaults to a value of 0; the 0 value causes this loop to be skipped.
]
++++++++ Set Cell #0 to 8
[
>++++ Add 4 to Cell #1; this will always set Cell #1 to 4
[ as the cell will be cleared by the loop
>++ Add 2 to Cell #2
>+++ Add 3 to Cell #3
>+++ Add 3 to Cell #4
>+ Add 1 to Cell #5
<<<<- Decrement the loop counter in Cell #1
] Loop until Cell #1 is zero; number of iterations is 4
>+ Add 1 to Cell #2
>+ Add 1 to Cell #3
>- Subtract 1 from Cell #4
>>+ Add 1 to Cell #6
[<] Move back to the first zero cell you find; this will
be Cell #1 which was cleared by the previous loop
<- Decrement the loop Counter in Cell #0
] Loop until Cell #0 is zero; number of iterations is 8
The result of this is:
Cell no : 0 1 2 3 4 5 6
Contents: 0 0 72 104 88 32 8
Pointer : ^
>>. Cell #2 has value 72 which is 'H'
>---. Subtract 3 from Cell #3 to get 101 which is 'e'
+++++++..+++. Likewise for 'llo' from Cell #3
>>. Cell #5 is 32 for the space
<-. Subtract 1 from Cell #4 for 87 to give a 'W'
<. Cell #3 was set to 'o' from the end of 'Hello'
+++.------.--------. Cell #3 for 'rl' and 'd'
>>+. Add 1 to Cell #5 gives us an exclamation point
>++. And finally a newline from Cell #6
2 changes: 1 addition & 1 deletion vm/go.mod
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
module vm
module brainfuckvm

go 1.20
Loading

0 comments on commit 2d01944

Please sign in to comment.