Skip to content

Commit

Permalink
docs and structure, constraint tests todo
Browse files Browse the repository at this point in the history
  • Loading branch information
@erhant
erhant committed Jul 21, 2023
1 parent 0fa0f61 commit 5ea4ef4
Show file tree
Hide file tree
Showing 15 changed files with 286 additions and 105 deletions.
102 changes: 71 additions & 31 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,20 +2,22 @@

> A [Brainfuck](https://en.wikipedia.org/wiki/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:
Brainfuck is a Turing-complete language that has only 8 operations, shown in the table below. Any other symbol is ignored, and may effectively be used as comments.

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

Any other symbol is ignored, and may effectively be used as comments. We have written a smol Brainfuck VM in Go, which you can find under the [vm](./vm/) folder. Assuming you have Go installed, you can build the binary simply via:
## Usage

We have written a small Brainfuck compiler & executer in Go, which you can find under the [vm](./vm/) folder. Assuming you have Go installed, you can build the binary simply via:

```sh
yarn vm:build
Expand All @@ -34,44 +36,82 @@ yarn vm:run
-num # use numbers for input & output instead of runes
```

You may find a few example Brainfuck codes in [here](./vm/sample). To run them, pass their paths via the `-path` option. Our VM does not allow for underflows, neither for the program counter or memory pointer. The default code `,[-]` simply takes an input and counts down, terminating when it reaches 0.
You may find a few example Brainfuck codes in [here](./vm/sample). To run your own Brainfuck code, provide its path to the `--path` option. If your inputs & outputs are numbers (not characters) make sure you also pass in the `--num` option. If the default tick amount is not enough, increase it with `--tick <amount>`.

To export the execution of the code, you will need to pass in `--export <path>` option. This will include all the operations, inputs and outputs that were encountered within the program. You can use the `ops`, `inputs` and `outputs` there as circuit signals. Note that you may have to append zeros to match signal sizes depending on the circuit template parameters. We do this [automatically](./tests/utils/index.ts) in our tests.

## Brainfuck Circuit

We will write the Brainfuck VM as an algebraic circuit, meaning that instead of tokens (like `+` or `-`) we shall operate on numbers. This is the reason we compile Brainfuck code in the first place, the result of compilation is simply an array of non-negative integers. The circuit asserts each "tick" to be valid, eventually running the program until no more ticks are left. Here is a rough demonstration of the instructions:

| `op` | Code | Constraint |
| -------- | ---- | ------------------------------------------------------- |
| 0 | | |
| 1 | `>` | `next_mem_ptr <== mem_ptr + 1` |
| 2 | `<` | `next_mem_ptr <== mem_ptr - 1` |
| 3 | `+` | `next_mem[mem_ptr] <== mem[mem_ptr] + 1` |
| 4 | `-` | `next_mem[mem_ptr] <== mem[mem_ptr] - 1` |
| 5 | `,` | `next_mem[mem_ptr] <== in` |
| 6 | `.` | `out === mem[mem_ptr]` |
| `i < op` | `[` | `next_pgm_ctr <== mem[mem_ptr] == 0 ? op : pgm_ctr + 1` |
| `i > op` | `]` | `next_pgm_ctr <== mem[mem_ptr] != 0 ? op : pgm_ctr + 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 simple equality checks, and jump targets can be assumed safe. Brainfuck programs usually terminate when there is no more instructions left; however, we can't do that in our circuit. In particular, the circuit will operate until each "tick" is processed, whether there are any ops left or not is not of concern. For this reason, the compiled code will have a no-op (`0`) at the end, corresponding to "terminating the program". In a no-op, the program counter is NOT incremented, thereby consuming ticks at that position until the circuit is finished.

### Parameters

The Brainfuck circuit is instantiated with the following parameters:

### From Code to Integers
- `TICKS`: number of ticks to run
- `MEMSIZE`: maximum memory size
- `OPSIZE`: maximum number of operations
- `INSIZE`: maximum number of inputs
- `OUTSIZE`: maximum number of outputs

...
Note that we particularly use the word "maximum" because you do not necessarily have to provide exactly that many inputs, for any input with less elements for that parameter is assumed to be appended zeros. Our circuit has three inputs:

## Proving Execution
- `ops`: compiled code
- `inputs`: inputs in the order they appear
- `outputs`: outputs in the order they appear

TODO
For example, the object below belongs to the execution of `,[.-]`. Notice the prepended 7 zeros and 1 extra zero at the end for `op`. In this particular execution, the user has given the input `5` and got the output `5 4 3 2 1`. Extra information such as memory usage and ticks is also included here.

| `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 < op` | `[` | if `m[p] == 0` then `_i' <== op` else `_i <== i + 1` |
| `i > op` | `]` | if `m[p] != 0` then `_i' <== op` else `_i <== i + 1` |
```json
{
"ticks": 22,
"memsize": 0,
"opsize": 13,
"insize": 1,
"outsize": 5,
"ops": [0, 0, 0, 0, 0, 0, 0, 5, 11, 6, 4, 8, 0],
"inputs": [5],
"outputs": [5, 4, 3, 2, 1]
}
```

To prepare this object as a circuit input, we append necessary zeros to inputs, outputs, and ops to match `INSIZE`, `OUTSIZE` and `OPSIZE` respectively. We also check the tick count and memory size to see if we can safely use the circuit.

### Constraints

todo: tests will give us the results here

## Testing

Tests have been written with [Circomkit](https://github.com/erhant/circomkit). You can run tests via:

```sh
yarn test
```

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
It will compile & run the circuit for 3 different programs.

## Constraints
## Drawbacks

Below are some example instantations with their constraint counts (using optimization level 1). With optimization level 2, one can get rid of linear constraints at the cost of a sligthly longer compilation time.
First and foremost, the constraint count is HUGE. This is mostly because of the `ArrayRead` circuit which reads from an array with unknown index. Doing so requires an entire pass over the array with an equality check for each index. For small input arrays this should not be too much of a problem, but inputs may change from time to time.

| Ticks | Memory Size | Operation Count | Non-linear Constraints | Linear Constraints |
| ----- | ----------- | --------------- | ---------------------- | ------------------ |
| 1024 | 256 | 20 | 1.65m | 565k |
| 256 | 256 | 20 | 414k | 141k |
| 1024 | 64 | 20 | 486k | 171k |
| 256 | 64 | 20 | 120k | 43k |
| 256 | 64 | 80 | 167k | 58k |
| 2048 | 32 | 60 | 767k | 274k |
The second problem is that due to the constraint count, a single huge circuit with many ticks, sufficient memory size, input size, and output size would be rather expensive (although possible). We believe folding may be used to fold each tick in a single recursive proof, perhaps using a tool such as Nova Scotia.

Constraints grow in linear with the tick size and memory size. Operation count grows the circuit sub-linearly.
Third drawback is that, who even writes Brainfuck?

## Honorable Mentions

Expand Down
2 changes: 1 addition & 1 deletion circuits.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
"bf": {
"file": "brainfuck",
"template": "Brainfuck",
"params": [256, 32, 60, 10, 10],
"params": [30, 5, 15, 1, 5],
"pubs": ["outputs"]
}
}
21 changes: 1 addition & 20 deletions circuits/utils.circom → circuits/utils/arrays.circom
View file
Original file line number Diff line number Diff line change
@@ -1,25 +1,6 @@
pragma circom 2.1.0;

include "circomlib/circuits/comparators.circom";
include "./functions/bits.circom";

// If-else branching.
//
// Inputs:
// - `cond`: a boolean condition
// - `ifTrue`: signal to be returned if condition is true
// - `ifFalse`: signal to be returned if condition is false
//
// Outputs:
// - `out`: equals `cond ? ifTrue : ifFalse`
template IfElse() {
signal input cond;
signal input ifTrue;
signal input ifFalse;
signal output out;

out <== cond * (ifTrue - ifFalse) + ifFalse;
}
include "./common.circom";

// Array access `out <== in[index]`.
// If `index >= n`, then this returns 0
Expand Down
101 changes: 101 additions & 0 deletions circuits/utils/common.circom
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,101 @@
pragma circom 2.1.0;

// Checks if two numbers are equal.
//
// Inputs:
// - `in`: two numbers
//
// Outputs:
// - `out`: 1 if `in[0] == in[1]`, 0 otherwise
template IsEqual() {
signal input in[2];
signal output {bool} out;

out <== IsZero()(in[1] - in[0]);
}

// Checks if a number is zero.
//
// Inputs:
// - `in`: a number
//
// Outputs:
// - `out`: 1 if `in == 0`, 0 otherwise
template IsZero() {
signal input in;
signal output {bool} out;

signal inv <-- in != 0 ? (1 / in) : 0;

out <== (-in * inv) + 1;
in * out === 0;
}

// If-else branching.
//
// Inputs:
// - `cond`: a boolean condition
// - `ifTrue`: signal to be returned if condition is true
// - `ifFalse`: signal to be returned if condition is false
//
// Outputs:
// - `out`: equals `cond ? ifTrue : ifFalse`
template IfElse() {
signal input cond;
signal input ifTrue;
signal input ifFalse;
signal output out;

out <== cond * (ifTrue - ifFalse) + ifFalse;
}

// Computes `in[0] < in[1]`.
//
// Parameters:
// - `n`: min number of bits to represent the inputs
//
// Inputs:
// - `in`: two numbers
//
// Outputs:
// - `out`: 1 if `in[0] < in[1]`, 0 otherwise.
template LessThan(n) {
assert(n <= 252);
signal input in[2];
signal output out;

component bits = Num2Bits(n+1);

bits.in <== in[0]+ (1<<n) - in[1];

out <== 1-bits.out[n];
}

// Decomposes a number to its bits.
//
// Parameters:
// - `n`: number of bits
//
// Inputs:
// - `in`: two numbers
//
// Outputs:
// - `out`: an array of bits
template Num2Bits(n) {
assert(n < 254);
signal input in;
signal output out[n];

var lc = 0;
var bit_value = 1;

for (var i = 0; i < n; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] - 1) === 0;

lc += out[i] * bit_value;
bit_value <<= 1;
}

lc === in;
}
27 changes: 19 additions & 8 deletions circuits/vm.circom
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,16 @@
pragma circom 2.1.0;

include "./utils.circom";
include "./utils/arrays.circom";
include "./utils/common.circom";
include "./functions/bits.circom";

// The VM template handles a single "tick" of the Brainfuck code.
// Given the current state (such as program counter, memory pointer etc.)
// it will compute the next state.
//
// The output is not "assigned to" but instead "asserted equal". This is because
// we run into "signal already assigned" error in the prior case. Outputting something
// is rather equivalent to getting it as a public input and asserting equality.
template VM(MEMSIZE, OPSIZE) {
var OP_NOOP = 0; // no operation
var OP_INC_PTR = 1; // > move pointer right
Expand Down Expand Up @@ -45,15 +54,15 @@ template VM(MEMSIZE, OPSIZE) {
is_OP_OUTPUT
]);

// if no OP is matched, we must be looping
// if none of the OPs are matched, we must be looping
signal is_LOOP <== 1 - is_OP;

// currently pointed value `mem[mem_ptr]` is referred to as `val`
signal val <== ArrayRead(MEMSIZE)(mem, mem_ptr);
signal val_is0 <== IsZero()(val);

// determine jump destination; since program counter is incremented
// we can jump by adding (destination - 1 - pgm_ctr) to the default value
// determine jump destination; since program counter is incremented by default,
// we can jump by adding (destination - 1 - pgm_ctr) to it
// if not, the offset is kept to be 0
signal is_pgm_ctr_lt_op <== LessThan(numBits(OPSIZE)+1)([pgm_ctr, op]);
signal is_LOOP_BEGIN <== is_LOOP * is_pgm_ctr_lt_op;
Expand All @@ -62,7 +71,7 @@ template VM(MEMSIZE, OPSIZE) {
signal jmp_offset <== is_LOOP_JUMP * (op - 1 - pgm_ctr);

// program counter is incremented by default
// if there is a loop, we add `jump_target - 1` to cancel incremention
// if there is a loop, we add `destination - 1 - pgm_ctr` to cancel incremention
// and set the counter to target
// if no-op, we cancel the incremention to cause program to halt
next_pgm_ctr <== pgm_ctr + 1 + jmp_offset - is_OP_NOOP;
Expand All @@ -87,9 +96,11 @@ template VM(MEMSIZE, OPSIZE) {
]);
next_mem <== ArrayWrite(MEMSIZE)(mem, mem_ptr, val + delta_val);

// output is only set during its respective op
var expectedOut = IfElse()(is_OP_OUTPUT, val, out);
out === expectedOut;
// expected output is provided by the prover
// at the output operation, the actual output is compared
// to the expect one, failing if they do not match
var tick_out = IfElse()(is_OP_OUTPUT, val, out);
out === tick_out;

// in case of emergency, break glass
// log("op:", op, "\tval", val, "\tp:", mem_ptr, "\ti:", pgm_ctr);
Expand Down
5 changes: 1 addition & 4 deletions package.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
"vm:build": "cd vm && go build -o ./bin/main -ldflags \"-s -w\" ./cmd/main.go",
"vm:hello": "./vm/bin/main --path ./vm/sample/helloworld.bf --export ./vm/out/hello.json",
"vm:countdown": "./vm/bin/main --path ./vm/sample/countdown.bf --num --export ./vm/out/countdown.json",
"vm:mul": "./vm/bin/main --path ./vm/sample/multiply.bf --export ./vm/out/multiply.json"
"vm:mul": "./vm/bin/main --path ./vm/sample/multiply.bf --num --export ./vm/out/multiply.json"
},
"devDependencies": {
"@types/mocha": "^10.0.1",
Expand All @@ -17,9 +17,6 @@
"ts-node": "^10.9.1",
"typescript": "^5.1.6"
},
"dependencies": {
"circomlib": "^2.0.5"
},
"prettier": {
"printWidth": 120
}
Expand Down
Loading

0 comments on commit 5ea4ef4

Please sign in to comment.