Tutorial 14: Logic in a Circuit

The code in an o1js method looks like usual TypeScript, but it does not run like usual TypeScript. This tutorial shows the mistakes that this causes, and the correct code for each mistake.

Each section has three parts:

The wrong code.
What goes wrong: the error message, or the wrong result. Each message on this page is the real text from o1js 3.0.0.
The correct code.

A test in the example project proves each claim on this page. The name of each test is the claim.

The full source code for this tutorial is in the examples/zkapps/14-circuit-logic directory on GitHub.

Prerequisites

Make sure your environment meets the Prerequisites for zkApp Developer Tutorials. o1js 3 requires Node.js 22 or later.

You must know how to write a ZkProgram. To learn about ZkProgram, see Tutorial 9: Recursion or ZkProgram in the o1Labs docs.

This tutorial has been tested with:

o1js version 3.0.0
Node.js version 22

Get the example project

git clone https://github.com/MinaProtocol/docs2.git
cd docs2/examples/zkapps/14-circuit-logic
npm install
npm start

npm start runs src/main.ts. It shows the wrong result and the correct result for most sections of this page.

How o1js runs a method

These terms are necessary for the rest of this page:

A circuit is the list of equations that a proof must satisfy. Each equation is a constraint. A row is one line of the circuit, which holds one or two constraints.
The prover is the program that makes a proof. The verifier is the program that checks a proof. The verifier uses the verification key, which compile() makes from the circuit.
A variable is a value in the circuit that can be different in each proof, for example a method input. While o1js makes the circuit, a variable has no value.
A constant is a value that is fixed in the circuit, for example Field(3). It is the same in each proof.
A witness is a value that the prover computes outside the circuit and gives to the circuit as a variable.

o1js runs your method code at least two times:

At compile time (compile() and analyzeMethods()), o1js runs the method to record the circuit. The inputs are variables with no values.
At proving time, o1js runs the method again with the real input values, to compute each variable and make the proof.

Your JavaScript code runs in both. A JavaScript if, for or === runs while o1js records the circuit, so the circuit keeps only the result. The circuit does not keep the JavaScript statement. Most mistakes on this page come from this fact.

For more about circuits, see What is a ZK constraint system? in the o1Labs docs.

Constants and variables

A JavaScript value in a method becomes a constant of the circuit. o1js does arithmetic on constants in JavaScript and adds no constraint. A product of two variables adds a constraint:

src/constants.ts
// Each argument is a constant: o1js computes the result in JavaScript and
// adds no constraint
export function constantMath() {
  return Field(2).mul(3).add(4);
}

// `x` is a variable: the product of two variables needs a constraint
export function variableMath() {
  const x = Provable.witness(Field, () => Field(2));
  return x.mul(x).add(4);
}

// A variable times a constant, plus a constant, is a linear combination.
// o1js keeps it as a formula and adds no constraint for it.
export function linearMath() {
  const x = Provable.witness(Field, () => Field(2));
  return x.mul(3).add(4);
}

Provable.constraintSystem() gives 0 rows for constantMath(), and more than 0 rows for variableMath(). A variable times a constant, plus a constant, also gives 0 rows: o1js keeps this linear combination as a formula, and uses it in the next constraint. isConstant() tells you which values are constants.

The wrong way: a JavaScript value as a rule

This program proves that a secret is more than a minimum. The minimum is a JavaScript value:

src/constants.ts
// A JavaScript value. The circuit reads it once, when the program is
// compiled, and keeps it as a constant.
export const config = { minimum: 10 };

export const BakedMinimum = ZkProgram({
  name: 'baked-minimum',
  methods: {
    check: {
      privateInputs: [Field],
      async method(secret: Field) {
        secret.assertGreaterThan(config.minimum);
      },
    },
  },
});

What goes wrong

compile() reads config.minimum one time and puts the value 10 into the circuit. The verification key is for the minimum 10 only.

If you change config.minimum to 20 after compile(), the prover runs the method with 20, but the circuit has 10. The prover cannot make a proof, for any secret:

the proof could not be constructed: rest of division by vanishing polynomial

A secret of 25 is more than both minimums, but the proof fails. If you compile again, you get a different verification key. A proof for the new key is not valid for the old key.

Thus, a constant is a part of the circuit. To change a constant, you must compile again, and each verifier must get the new verification key.

The right way: a provable input

When the value can change, make it a method input:

src/constants.ts
// The minimum is a public input: the prover chooses it for each proof, and the
// verifier sees which minimum the proof is for
export const InputMinimum = ZkProgram({
  name: 'input-minimum',
  publicInput: Field,
  methods: {
    check: {
      privateInputs: [Field],
      async method(minimum: Field, secret: Field) {
        secret.assertGreaterThan(minimum);
      },
    },
  },
});

One verification key is valid for each minimum. Because minimum is a public input, the verifier reads from proof.publicInput which minimum the proof is for. A secret that is not more than the minimum gives the error Constraint unsatisfied.

Use a constant only for a value that must be the same in each proof, for example the maximum length of a list.

The tests are in src/constants.test.ts:

adds no constraints for arithmetic on constants
adds no constraints for a variable times a constant plus a constant
marks a Field made from a JavaScript value as a constant, and a witness as a variable
proves a secret more than the minimum that was compiled in
cannot prove a secret that is not more than the minimum
cannot prove after the JavaScript value changes, until the program is compiled again
gives a different verification key for a different constant
proves against different minimums with one verification key
cannot prove a secret that is not more than the minimum input

Branches: `Provable.if` and a JavaScript `if`

The wrong way: a JavaScript `if` on a `Bool`

This program gives a bonus of 10 for a score of more than 100:

src/branching.ts
export const BonusWithJsIf = ZkProgram({
  name: 'bonus-with-js-if',
  publicInput: Field,
  publicOutput: Field,
  methods: {
    bonus: {
      privateInputs: [],
      async method(score: Field) {
        let bonus = Field(0);
        // WRONG: `score.greaterThan(100)` returns a Bool object, and
        // JavaScript treats every object as true
        if (score.greaterThan(100)) {
          bonus = Field(10);
        }
        return { publicOutput: bonus };
      },
    },
  },
});

What goes wrong

There is no error. TypeScript accepts the code, and compile() and proving are successful. But the result is wrong: a score of 5 gets the bonus of 10.

score.greaterThan(100) returns a Bool. A Bool is a JavaScript object, and JavaScript treats each object as true. The if runs one time, at compile time, and always takes the first branch. The circuit only has bonus = Field(10).

If you add .toBoolean() to get a JavaScript boolean, the mistake becomes an error at compile time:

src/branching.ts
export const BonusWithToBoolean = ZkProgram({
  name: 'bonus-with-to-boolean',
  publicInput: Field,
  publicOutput: Field,
  methods: {
    bonus: {
      privateInputs: [],
      async method(score: Field) {
        let bonus = Field(0);
        // WRONG: a variable has no JavaScript value at compile time
        if (score.greaterThan(100).toBoolean()) {
          bonus = Field(10);
        }
        return { publicOutput: bonus };
      },
    },
  },
});

b.toBoolean() was called on a variable Bool `b` in provable code.
This is not supported, because variables represent an abstract computation,
which only carries actual values during proving, but not during compiling.

The right way: `Provable.if`

Provable.if(condition, a, b) adds constraints that select a when the condition is true and b when the condition is false:

src/branching.ts
export const BonusWithProvableIf = ZkProgram({
  name: 'bonus-with-provable-if',
  publicInput: Field,
  publicOutput: Field,
  methods: {
    bonus: {
      privateInputs: [],
      async method(score: Field) {
        const bonus = Provable.if(score.greaterThan(100), Field(10), Field(0));
        return { publicOutput: bonus };
      },
    },
  },
});

A score of 5 gives 0 and a score of 150 gives 10. Both proofs are valid for the same verification key.

`Provable.if` computes both branches

Provable.if is not a JavaScript if. Both a and b are computed before Provable.if selects one, and the constraints of both are in the circuit. A constraint that fails in the branch that is not selected makes the proof fail:

src/branching.ts
// WRONG: Provable.if computes both branches. When y is 0, `x.div(y)` fails,
// although its result is not selected.
export function divideOrZeroWrong(x: Field, y: Field) {
  return Provable.if(y.equals(0), Field(0), x.div(y));
}

For y = 0, the division adds a constraint that has no solution:

Constraint unsatisfied (unreduced):
generic

Make each branch correct for all inputs. Here, the code divides by 1 when y is 0, and then selects 0:

src/branching.ts
// Make each branch safe for all inputs: divide by 1 when y is 0, then select
export function divideOrZero(x: Field, y: Field) {
  const yIsZero = y.equals(0);
  const safeY = Provable.if(yIsZero, Field(1), y);
  return Provable.if(yIsZero, Field(0), x.div(safeY));
}

For more about conditions, see Conditional logic in the o1Labs docs.

The tests are in src/branching.test.ts:

compiles with no error
always takes the true branch, so a score of 5 gets the bonus
fails at compile time with toBoolean()
selects the bonus in the proof for each score
computes both branches, so a division by 0 in the branch that is not selected fails
gives 0 for y = 0 and x / y otherwise when each branch is safe

Loops

The wrong way: a loop bound that is a variable

This program sums the first n items of a list. The number of steps comes from the input n:

src/loops.ts
export const SumFirstWrong = ZkProgram({
  name: 'sum-first-wrong',
  publicInput: Field,
  publicOutput: Field,
  methods: {
    sum: {
      privateInputs: [Provable.Array(Field, 8)],
      async method(n: Field, xs: Field[]) {
        let sum = Field(0);
        // WRONG: the number of steps depends on a variable
        for (let i = 0; i < n.toBigInt(); i++) {
          sum = sum.add(xs[i]);
        }
        return { publicOutput: sum };
      },
    },
  },
});

What goes wrong

compile() fails:

x.toBigInt() was called on a variable field element `x` in provable code.
This is not supported, because variables represent an abstract computation,
which only carries actual values during proving, but not during compiling.

At compile time, n has no value, so the loop cannot know how many steps to run. A circuit has a fixed size. It cannot have more constraints for one proof and fewer for a different proof.

A JavaScript loop unrolls

A for loop with a bound that is known at compile time is correct. The loop runs at compile time, and each step adds its own constraints to the circuit. This is unrolling:

src/loops.ts
// A loop with a bound that is known at compile time. Compiling runs the loop,
// and each step adds its own constraints, so the circuit grows with `length`.
export function sumOfSquares(length: number) {
  return ZkProgram({
    name: `sum-of-squares-${length}`,
    publicOutput: Field,
    methods: {
      sum: {
        privateInputs: [Provable.Array(Field, length)],
        async method(xs: Field[]) {
          let sum = Field(0);
          for (let i = 0; i < length; i++) {
            sum = sum.add(xs[i].mul(xs[i]));
          }
          return { publicOutput: sum };
        },
      },
    },
  });
}

analyzeMethods() shows the size of the circuit. A loop of 8 steps has two times the rows of a loop of 4 steps, and a loop of 16 steps has two times the rows of a loop of 8 steps. A long loop makes a large circuit, and a large circuit makes proving slower.

The right way: a fixed maximum and `Provable.if`

Run the loop for a fixed maximum number of steps. For each step, compute in the circuit if the step is in use, and use Provable.if to add 0 for a step that is not in use:

src/loops.ts
export const MAX_LENGTH = 8;

// Always run MAX_LENGTH steps. A Bool switches off the steps after the first n.
export const SumFirst = ZkProgram({
  name: 'sum-first',
  publicInput: Field,
  publicOutput: Field,
  methods: {
    sum: {
      privateInputs: [Provable.Array(Field, MAX_LENGTH)],
      async method(n: Field, xs: Field[]) {
        n.assertLessThanOrEqual(MAX_LENGTH, 'n is more than MAX_LENGTH');
        let sum = Field(0);
        let active = Bool(true);
        for (let i = 0; i < MAX_LENGTH; i++) {
          active = active.and(n.equals(i).not());
          sum = sum.add(Provable.if(active, xs[i], Field(0)));
        }
        return { publicOutput: sum };
      },
    },
  },
});

The circuit always has MAX_LENGTH steps. One verification key is valid for each n from 0 to MAX_LENGTH. The assertion on n is necessary: without it, an n of more than MAX_LENGTH gives the sum of all items, not an error.

The tests are in src/loops.test.ts:

fails at compile time when the loop bound depends on a variable
unrolls a JavaScript loop: twice the steps give twice the rows
sums the first n items for n from 0 to MAX_LENGTH, with one circuit
cannot prove for n more than MAX_LENGTH

Find a value in a list

This section uses the two mistakes above together. The task is: does a list of Field values include x?

The wrong way: the JavaScript array functions

src/includes.ts
// WRONG: Array.includes() compares objects, not values. Two Field objects
// are never the same object, so the result is false.
export function includesWrong(list: Field[], x: Field): boolean {
  return list.includes(x);
}

// WRONG: equals() returns a Bool object, and JavaScript treats every object as
// true. The result is true for each list that is not empty.
export function includesWithSomeWrong(list: Field[], x: Field): boolean {
  return list.some((item) => item.equals(x));
}

What goes wrong

There is no error, but both results are wrong. For the list [1, 2, 3]:

includesWrong(list, 2) is false. Array.includes() compares objects with ===. Each Field is a different object, so no item is the same object as x.
includesWithSomeWrong(list, 7) is true. The callback returns a Bool object, and JavaScript treats each object as true.

Both functions return a JavaScript boolean. A JavaScript boolean in a method is a constant: o1js computes it one time at compile time, and it is the same in each proof.

The right way: `equals()` and `or()`

src/includes.ts
// Compare x with each item and combine the results with or().
// The result is a Bool variable, so the circuit can use it.
export function includes(list: Field[], x: Field): Bool {
  return list.reduce((found, item) => found.or(item.equals(x)), Bool(false));
}

The result is a Bool variable. You can assert it with assertTrue(), or use it in Provable.if. For the list [1, 2, 3], the result is true for 2 and false for 7.

For more about arrays in a circuit, see Arrays in the o1Labs docs.

The tests are in src/includes.test.ts:

is not found by Array.includes(), although the list has it
is found by Array.some() with equals(), although the list does not have it
is found by includes() with or() only when the list has it

Witnesses

Provable.witness(type, compute) makes a variable. The compute function runs only in the prover, outside the circuit. Use a witness when a value is difficult to compute in the circuit but easy to check, for example a square root.

In this example, the prover code is in a separate object, so that a test can replace it:

src/witness.ts
// Code that runs only in the prover. An honest prover uses this function;
// a malicious prover can replace it with any code.
export const hints = {
  sqrt: (x: Field): Field => x.sqrt(),
};

The wrong way: a witness with no constraint

src/witness.ts
export const UnsafeSqrt = ZkProgram({
  name: 'unsafe-sqrt',
  publicInput: Field,
  publicOutput: Field,
  methods: {
    sqrt: {
      privateInputs: [],
      async method(x: Field) {
        // WRONG: nothing connects y to x
        const y = Provable.witness(Field, () => hints.sqrt(x));
        return { publicOutput: y };
      },
    },
  },
});

What goes wrong

The compute function is not a part of the circuit. The verifier does not know which function the prover used. The verification key is the same when you compile with a different compute function.

A malicious prover replaces hints.sqrt with a function that returns 7. The proof says that 7 is the square root of 9. There is no error, and verify() returns true.

danger

A witness with no constraint is a value that the prover chooses. A proof says nothing about it.

The right way: constrain each witness

Add a constraint that checks the witness:

src/witness.ts
export const SafeSqrt = ZkProgram({
  name: 'safe-sqrt',
  publicInput: Field,
  publicOutput: Field,
  methods: {
    sqrt: {
      privateInputs: [],
      async method(x: Field) {
        const y = Provable.witness(Field, () => hints.sqrt(x));
        // The constraint: y * y must equal x
        y.mul(y).assertEquals(x, 'y is not a square root of x');
        return { publicOutput: y };
      },
    },
  },
});

An honest prover gets 3 (or the other square root of 9 in the field, which also satisfies y * y = 9). The malicious prover cannot make a proof:

y is not a square root of x
Constraint unsatisfied (unreduced):
rule_main

For more about witnesses, see Witnesses in the o1Labs docs.

The tests are in src/witness.test.ts:

gives an honest prover a square root
accepts any witness when there is no constraint: a malicious prover proves that 7 is the square root of 9
does not put the witness code in the verification key
rejects the same malicious witness when a constraint checks it

`toBigInt()`, `toString()` and debugging

The wrong way: read a JavaScript value from a variable

src/conversions.ts
export const IsEvenWrong = ZkProgram({
  name: 'is-even-wrong',
  publicInput: Field,
  publicOutput: Bool,
  methods: {
    isEven: {
      privateInputs: [],
      async method(x: Field) {
        // WRONG: reads a JavaScript value from a variable
        return { publicOutput: Bool(x.toBigInt() % 2n === 0n) };
      },
    },
  },
});

src/conversions.ts
export const LogWrong = ZkProgram({
  name: 'log-wrong',
  publicInput: Field,
  methods: {
    log: {
      privateInputs: [],
      async method(x: Field) {
        // WRONG: the same error as toBigInt()
        console.log('x is', x.toString());
      },
    },
  },
});

What goes wrong

compile() fails for both programs. The message for toBigInt() is:

x.toBigInt() was called on a variable field element `x` in provable code.
This is not supported, because variables represent an abstract computation,
which only carries actual values during proving, but not during compiling.

Also, reading out JS values means that whatever you're doing with those values will no longer be
linked to the original variable in the proof, which makes this pattern prone to security holes.

The message for toString() starts with x.toString() was called on a variable field element `x` in provable code. toBoolean() on a Bool variable gives the same error. Outside a method, for example on proof.publicOutput, these functions work.

The right way: compute in the circuit

To get information from a variable, use o1js functions that add constraints. For example, the lowest bit of x tells if x is even:

src/conversions.ts
// The bits of x are variables too, and toBits() adds the constraints that
// connect them to x
export const IsEven = ZkProgram({
  name: 'is-even',
  publicInput: Field,
  publicOutput: Bool,
  methods: {
    isEven: {
      privateInputs: [],
      async method(x: Field) {
        const lowestBit = x.toBits(64)[0];
        return { publicOutput: lowestBit.not() };
      },
    },
  },
});

toBits(64) also asserts that x is less than 2⁶⁴.

The right way to debug: `Provable.asProver` and `Provable.log`

To read or print a value while proving, use Provable.asProver() or Provable.log():

src/conversions.ts
// Values that the prover saw, to show what Provable.asProver() can read
export const seenByProver: bigint[] = [];

export const Square = ZkProgram({
  name: 'square',
  publicInput: Field,
  publicOutput: Field,
  methods: {
    square: {
      privateInputs: [],
      async method(x: Field) {
        // Runs only when the prover has values. It adds no constraints.
        Provable.asProver(() => {
          seenByProver.push(x.toBigInt());
        });
        // Prints the value when proving
        Provable.log('x is', x);
        return { publicOutput: x.mul(x) };
      },
    },
  },
});

The callback of Provable.asProver() runs only when the prover has values. compile() does not run it. In the callback, toBigInt() and toString() work. Provable.asProver() and Provable.log() add no constraints, so a value that you compute in the callback is not in the proof. Do not use such a value to change the circuit.

The tests are in src/conversions.test.ts:

fails at compile time with toBigInt()
fails at compile time with toString()
proves if a number is even with constrained bits
runs Provable.asProver only when proving, with the values
adds no constraints for Provable.asProver and Provable.log

Assertions and returned `Bool` values

A method can return a Bool, or it can assert a condition. The two are not the same.

The wrong way: return a `Bool` that nobody checks

src/assertions.ts
// A proof of this method is valid for every age. The output says if the age
// is 18 or more, so the verifier must read it.
export const IsAdult = ZkProgram({
  name: 'is-adult',
  publicInput: Field,
  publicOutput: Bool,
  methods: {
    check: {
      privateInputs: [],
      async method(age: Field) {
        return { publicOutput: age.greaterThanOrEqual(18) };
      },
    },
  },
});

What goes wrong

For an age of 12, the prover makes a proof, and verify() returns true. The output is false. A valid proof says only that the output is correct. It does not say that the output is true. If the verifier does not read proof.publicOutput, the verifier accepts the proof of a person who is 12.

A returned Bool is correct when the verifier, or the next method, must know the result in both cases. Then it must read the result.

The right way: assert the condition

src/assertions.ts
// There is no proof of this method for an age less than 18
export const AssertAdult = ZkProgram({
  name: 'assert-adult',
  publicInput: Field,
  methods: {
    check: {
      privateInputs: [],
      async method(age: Field) {
        age.assertGreaterThanOrEqual(18, 'age is less than 18');
      },
    },
  },
});

For an age of 12, the prover cannot make a proof:

age is less than 18

A proof of this method exists only for an age of 18 or more. The second argument of an assertion is the message of the error. Give each assertion a message, so that you know which assertion failed.

The tests are in src/assertions.test.ts:

gives a valid proof for an age of 12 when the method returns a Bool: the output is false
cannot prove an age of 12 when the method asserts
proves an age of 30 when the method asserts

Run the tests

npm test

The tests compile the programs and make real proofs. They take some minutes.

Summary

Wrong	Result	Right
A JavaScript value for a rule that changes	Proving fails after the value changes. A new verification key for each value.	A method input
`if (bool)` on a `Bool`	No error. The first branch always.	`Provable.if`
`bool.toBoolean()`, `x.toBigInt()`, `x.toString()` in a method	Error at compile time	o1js functions, for example `toBits()`, `equals()`, `or()`
A division or assertion in the branch of `Provable.if` that is not selected	Proving fails	Make each branch correct for all inputs
A loop bound that is a variable	Error at compile time	A fixed maximum and `Provable.if`
`Array.includes()`, `Array.some()`	No error. A wrong constant result.	`reduce()` with `equals()` and `or()`
`Provable.witness` with no constraint	A malicious prover makes a valid proof of a false result	Add a constraint that checks the witness
A returned `Bool` that nobody reads	A valid proof of a false condition	An assertion

Conclusion

You have seen that o1js runs your method code at compile time, with variables that have no value, and that a circuit keeps the result of JavaScript code, not the code. Each JavaScript value is a constant, each JavaScript branch and loop runs one time at compile time, and each witness is a value that the prover chooses until a constraint checks it.

To see the size of your own circuits, see Analyzing constraint systems in the o1Labs docs.

Prerequisites​

Get the example project​

How o1js runs a method​

Constants and variables​

The wrong way: a JavaScript value as a rule​

What goes wrong​

The right way: a provable input​

Branches: Provable.if and a JavaScript if​

The wrong way: a JavaScript if on a Bool​

What goes wrong​

The right way: Provable.if​

Provable.if computes both branches​

Loops​

The wrong way: a loop bound that is a variable​

What goes wrong​

A JavaScript loop unrolls​

The right way: a fixed maximum and Provable.if​

Find a value in a list​

The wrong way: the JavaScript array functions​

What goes wrong​

The right way: equals() and or()​

Witnesses​

The wrong way: a witness with no constraint​

What goes wrong​

The right way: constrain each witness​

toBigInt(), toString() and debugging​

The wrong way: read a JavaScript value from a variable​

What goes wrong​

The right way: compute in the circuit​

The right way to debug: Provable.asProver and Provable.log​

Assertions and returned Bool values​

The wrong way: return a Bool that nobody checks​

What goes wrong​

The right way: assert the condition​

Run the tests​

Summary​

Conclusion​

Prerequisites

Get the example project

How o1js runs a method

Constants and variables

The wrong way: a JavaScript value as a rule

What goes wrong

The right way: a provable input

Branches: `Provable.if` and a JavaScript `if`

The wrong way: a JavaScript `if` on a `Bool`

What goes wrong

The right way: `Provable.if`

`Provable.if` computes both branches

Loops

The wrong way: a loop bound that is a variable

What goes wrong

A JavaScript loop unrolls

The right way: a fixed maximum and `Provable.if`

Find a value in a list

The wrong way: the JavaScript array functions

What goes wrong

The right way: `equals()` and `or()`

Witnesses

The wrong way: a witness with no constraint

What goes wrong

The right way: constrain each witness

`toBigInt()`, `toString()` and debugging

The wrong way: read a JavaScript value from a variable

What goes wrong

The right way: compute in the circuit

The right way to debug: `Provable.asProver` and `Provable.log`

Assertions and returned `Bool` values

The wrong way: return a `Bool` that nobody checks

What goes wrong

The right way: assert the condition

Run the tests

Summary

Conclusion