Chapter 2: StepType and Circuit

Chapter 2: StepType and Circuit#

In this Chapter, we code out the concepts learned in Chapter 1 in PyChiquito, but before that, let’s import the dependencies first.

Imports#

The following imports are required, including:

Circuit and StepType, the most important data types, from the domain specific language (dsl).
Equal constraint eq from the constraint builder (cb).
Field element F from utils.

from chiquito.dsl import Circuit, StepType
from chiquito.cb import eq
from chiquito.util import F

StepType#

Before putting everything together into a circuit, we need to define the step types first. Remember that the Fibonacci circuit is composed of one single step type, defined as 3 signals “a”, “b”, and “c”, plus three constraints a + b == c, b == a.next, and c == b.next, where “next” means the same signal in the next step instance:

Step Type	Step Instance Index		Signals			Setups
		a	b	c	constraint 1	constraint 2	constraint 3
fibo step	0	1	1	2	a + b == c	b == a.next	c == b.next
fibo step	1	1	2	3	a + b == c	b == a.next	c == b.next
fibo step	2	2	3	5	a + b == c	b == a.next	c == b.next
fibo step	3	3	5	8	a + b == c	b == a.next	c == b.next
…	…		…			…

PyChiquito provides a StepType parent class that we can customarily inherit. For each StepType, we need to define two functions:

setup, which defines constraints using signals
wg, which defines witness assignment for the step type

Signal Types#

Now, a bit more on the signals. In Chiquito, there are signals that we can only query for the current step instance, which we call “internal signals”. There are also signals that we can query for non-current step instances, such as the next step instance, which we call “forward signals”. In the example above, “a” and “b” were both queried at the next step instance as a.next and b.next respectively, and therefore are “forward signals”. “c” is only ever queried at the current step instance, and therefore is called “internal signal”. In Chiquito, querying to a non-current step instance is also referred to as “rotation”, which is a positive or negative number relative to the current step instance. We can call next on a forward signal, implying a rotation of +1. There are additional Chiquito signal types, such as “shared signal” and “fixed signal”, which allows for arbitrary positive or negative rotation. However, in this Fibonacci example, we will only use forward signals “a” and “b” as well as internal signal “c”.

FiboStep Setup#

We now define the only step type, FiboStep:

class FiboStep(StepType):
    def setup(self):
        self.c = self.internal("c")
        self.constr(eq(self.circuit.a + self.circuit.b, self.c))
        self.transition(eq(self.circuit.b, self.circuit.a.next()))
        self.transition(eq(self.c, self.circuit.b.next()))

    def wg(self):
        # TODO

Here, “c” is defined using self.internal as an internal signal that’s only queried within a FiboStep instance. We didn’t define “a” and “b”, as they are forward signals which Chiquito defines on the circuit-level. More on that later.

Next, we define constraints among signals, both forward and internal. There are two types of constraints in PyChiquito:

constr stands for constraints among signals that are queried within a step type instance, i.e. internal signals.
transition stands for constraints involving circuit-level signals, i.e. forward signals and etc.

In the code snippet above, forward signals “a” and “b” are expressed as self.circuit.a and self.circuit.b, whereas internal signal “c” is expressed as self.c, because “a” and “b” are at the circuit-level. self.circuit.a.next() queries the value of circuit-level signal “a” at the next step instance. eq is a constraint builder that enforces equality between the two arguments passed in. It builds the three constraints of FiboStep: a + b == c, b == a.next, and c == b.next.

FiboStep Witness Generation#

class FiboStep(StepType):
    def setup(self):
        # ...

    def wg(self, args):
        a_value, b_value = args # `args` is a tuple of (int, int)
        self.assign(self.circuit.a, F(a_value))
        self.assign(self.circuit.b, F(b_value))
        self.assign(self.c, F(a_value + b_value))

In the example above, wg (witness generation) defines witness value assignments at the step type level. Here, the args we pass in is a tuple of values for signals “a” and “b”. We assign them to forward signals “a” and “b” and then their sum to internal signal “c”.

Note that in self.assign, a_value and b_value are both wrapped in F, which converts them from int to field elements. All witness assignments in PyChiquito are field elements.

Putting everything for FiboStep together, we have:

class FiboStep(StepType):
    def setup(self):
        self.c = self.internal("c")
        self.constr(eq(self.circuit.a + self.circuit.b, self.c))
        self.transition(eq(self.circuit.b, self.circuit.a.next()))
        self.transition(eq(self.c, self.circuit.b.next()))

    def wg(self, args):
        a_value, b_value = args
        self.assign(self.circuit.a, F(a_value))
        self.assign(self.circuit.b, F(b_value))
        self.assign(self.c, F(a_value + b_value))

Circuit#

Now that we finished constructing the only step type FiboStep, we can build a Circuit object in PyChiquito. PyChiquito provides a Circuit parent class that we can customarily inherit. For each Circuit, we need to define two functions:

setup, which configures the circuit with signals and step types.
trace, which instantiates step types and defines the trace of assigning witness values.

Circuit Setup#

We first define the circuit setup:

class Fibonacci(Circuit):
    def setup(self):
        self.a = self.forward("a")
        self.b = self.forward("b")
        
        self.fibo_step = self.step_type(FiboStep(self, "fibo_step"))
        self.pragma_num_steps(4)

    def trace(self):
        # TODO

Remember that previously we already added internal signal “c” to FiboStep. Now we add two forward signals “a” and “b” to the circuit-level. We append these signals to the circuit by defining them as self.a and self.b. Forward signals are created using self.forward.

Next, we append the only step type to the circuit by defining it as self.fibo_step. step_type function only has one argument, which is the FiboStep object created using its class constructor.

Finally, we constrain the total number of step instances to 4, by using self.pragma_num_steps.

Circuit Trace#

Now we instantiate step types and assign witness values using trace:

class Fibonacci(Circuit):
    def setup(self):
        # ...
        
    def trace(self, args):
        self.add(self.fibo_step, (1, 1))
        a = 1
        b = 2
        for i in range(1, 4):
            self.add(self.fibo_step, (a, b))
            prev_a = a
            a = b
            b += prev_a

trace takes two arguments, the Fibonacci circuit itself and the witness value assignment arguments args. We call self.add to instantiate fibo_step we defined and pass in the witness values for “a” and “b”. Note that we only hardcoded witness values for the first step instance as (1, 1), because all other witness values can be calculated given the nature of Fibonacci.

Note that self.add creates step instance by calling wg function associated with the step type, which we defined earlier. The second argument of self.add, e.g. (a, b) in self.add(self.fibo_step, (a, b)), is actually the input for wg. Therefore, (a, b) needs to match args in FiboStep wg, i.e. tuple of a_value, b_value.

We didn’t pass in witness values for “c”, because they are calculated in FiboStep wg.

After creating the first FiboStep instance, we loop over FiboStep instantiation for 3 more times, each time calculating and passing in a different tuple of assignments. Voila, here’s our Fibonacci circuit with 4 FiboStep instances:

class FiboStep(StepType):
    def setup(self):
        self.c = self.internal("c")
        self.constr(eq(self.circuit.a + self.circuit.b, self.c))
        self.transition(eq(self.circuit.b, self.circuit.a.next()))
        self.transition(eq(self.c, self.circuit.b.next()))

    def wg(self, args):
        a_value, b_value = args
        self.assign(self.circuit.a, F(a_value))
        self.assign(self.circuit.b, F(b_value))
        self.assign(self.c, F(a_value + b_value))

class Fibonacci(Circuit):
    def setup(self):
        self.a = self.forward("a")
        self.b = self.forward("b")
        
        self.fibo_step = self.step_type(FiboStep(self, "fibo_step"))
        self.pragma_num_steps(4)
        
    def trace(self, args):
        self.add(self.fibo_step, (1, 1))
        a = 1
        b = 2
        for i in range(1, 4):
            self.add(self.fibo_step, (a, b))
            prev_a = a
            a = b
            b += prev_a

Putting Everything Together#

Everything we went through above defines how the circuit and its step type are configured and witness values assigned to them. To instantiate the circuit, we call the class constructor:

fibo = Fibonacci()

You can also print the circuit. In the print out, you will see the single step type FiboStep and two forward signals “a” and “b” at the circuit-level. Within FiboStep, you will see one internal signal “c” and the constraints. The big random looking numbers are UUIDs that we use to uniquely identify objects in the circuit, which you don’t need to worry about.

print(fibo)

ASTCircuit(
	step_types={
		105094138062140778571875773958161304074: ASTStepType(
			id=105094138062140778571875773958161304074,
			name='fibo_step',
			signals=[
				InternalSignal(id=105094144479621942225764057936239921674, annotation='c')
			],
			constraints=[
				Constraint(
					annotation='((a + b) == c)',
					expr=(a + b - (-c))
				)
			],
			transition_constraints=[
				TransitionConstraint((b == next(a))),
				TransitionConstraint((c == next(b)))
			],
			lookups=[],
			annotations={
				105094144479621942225764057936239921674: c
			}
		)
	},
	forward_signals=[
		ForwardSignal(id=105094119998119725319401044422165137930, phase=0, annotation='a'),
		ForwardSignal(id=105094131723887777427206951566041549322, phase=0, annotation='b')
	],
	shared_signals=[],
	fixed_signals=[],
	exposed=[],
	annotations={
		105094119998119725319401044422165137930: a,
		105094131723887777427206951566041549322: b,
		105094138062140778571875773958161304074: fibo_step
	},
	fixed_assignments=None,
	first_step=None,
	last_step=None,
	num_steps=4
	q_enable=True
)

After initiating the Fibonacci circuit, we can generate witness assignments for it. gen_witness takes one argument of external input with Any type. However, because the only external input, (1, 1), was hardcoded in trace, we don’t need to provide an additional one and can put None for this argument. In practice, one circuit can have many different sets of witness assignments, each generated by a different external input argument. This is why we expose the gen_witness function to you.

fibo_witness = fibo.gen_witness(None)

Again, you can print the witness assignments:

print(fibo_witness)

TraceWitness(
	step_instances={
		StepInstance(
			step_type_uuid=105094138062140778571875773958161304074,
			assignments={
				a = 1,
				b = 1,
				c = 2
			},
		),
		StepInstance(
			step_type_uuid=105094138062140778571875773958161304074,
			assignments={
				a = 1,
				b = 2,
				c = 3
			},
		),
		StepInstance(
			step_type_uuid=105094138062140778571875773958161304074,
			assignments={
				a = 2,
				b = 3,
				c = 5
			},
		),
		StepInstance(
			step_type_uuid=105094138062140778571875773958161304074,
			assignments={
				a = 3,
				b = 5,
				c = 8
			},
		)
	},
)

Finally, we can generate and verify proof with the witness using the Halo2 mock prover. The print out includes Halo2 and ChiquitoCore debug messages. Ok(()) means that proof was correctly generated and verified for the witness and circuit. Err() prints out Halo2 and ChiquitoCore error messages, usually because some constraints in the circuit were not satisfied. Here, you should see the Ok(()) print out.

fibo.halo2_mock_prover(fibo_witness)

------ Visiting map -------

key = annotations
key = exposed
key = first_step
key = fixed_assignments
key = fixed_signals
key = forward_signals
key = id
key = last_step
key = num_steps
key = q_enable
key = shared_signals
key = step_types
------ Visiting step_types -------
step_types = Some(
    {
        105094138062140778571875773958161304074: StepType {
            id: 105094138062140778571875773958161304074,
            signals: [
                InternalSignal {
                    id: 105094144479621942225764057936239921674,
                    annotation: "c",
                },
            ],
            constraints: [
                Constraint {
                    annotation: "((a + b) == c)",
                    expr: (a + b + (-c)),
                },
            ],
            transition_constraints: [
                TransitionConstraint {
                    annotation: "(b == next(a))",
                    expr: (b + (-next(a))),
                },
                TransitionConstraint {
                    annotation: "(c == next(b))",
                    expr: (c + (-next(b))),
                },
            ],
            lookups: [],
        },
    },
)
Ok(
    (),
)

Congratulations! Now you finished writing your first Fibonacci circuit and learned about the most essential concepts behind the step-based design of Chiquito, which simply combines step instances into a circuit! With abstraction, composability, modularity, and smooth user experience as the key tenets, writing Halo2 circuits has never been easier with PyChiquito!

Next up, in Chapter 3, you will learn about testing your circuit with multiple different witnesses.