Chapter 5: Padding and Exposing Signals

Chapter 5: Padding and Exposing Signals#

In prior examples, all Fibonacci circuit witnesses have the same number of step instances. According to our analogy where a circuit is considered a piece of hardware and its witnesses compatible software, it’s natural to think that we’d allow for more flexibility for our witnesses. Most immediately, and we shouldn’t limit all Fibonacci circuit witnesses to have the same number of step instances.

However, you might wonder, doesn’t self.pragma_num_steps(4) limit the number of step instances to 4? Besides, doesn’t this function guarantee the Fibonacci circuit’s security, such that we have a fixed circuit setup with a specific number of step instances, thereby making the circuit a piece of “hardware” that cannot be tampered with? How can we allow for BOTH a fixed circuit setup AND flexible witnesses? This problem is frequently encountered in projects like PSE’s zkEVM, where witnesses with very different sizes are passed into the same circuit.

Padding#

In Chiquito, you can achieve fixed circuit setup with flexible witnesses through a technique called “padding”:

  • To have a fixed circuit setup, we specify a maximum number of steps that won’t be exceeded by all plausible witnesses. For example, we can set this number to 10 for the Fibonacci circuit, but it’s really up to you.

  • To have flexible witnesses that still pass the same circuit setup, we add “padding step instances” towards the end of the witness.

  • For example, if we want to calculate 4 rounds for the Fibonacci series, we add 6 padding step instances:

Step Type

Step Instance Index

Signals

Setups

a

b

c

constraint 1

constraint 2

constraint 3

constraint 4

constraint 5

fibo first step

0

1

1

2

a + b == c

b == a.next

c == b.next

a == 1

b == 1

fibo step

1

1

2

3

a + b == c

b == a.next

c == b.next

n.a.

n.a.

fibo step

2

2

3

5

a + b == c

b == a.next

c == b.next

n.a.

n.a.

fibo step

3

3

5

8

a + b == c

b == a.next

c == b.next

n.a.

n.a.

padding

4

padding

5

padding

6

padding

7

padding

8

padding

9

  • If we want 7 rounds, we add 3 padding step instances.

Step Type

Step Instance Index

Signals

Setups

a

b

c

constraint 1

constraint 2

constraint 3

constraint 4

constraint 5

fibo first step

0

1

1

2

a + b == c

b == a.next

c == b.next

a == 1

b == 1

fibo step

1

1

2

3

a + b == c

b == a.next

c == b.next

n.a.

n.a.

fibo step

2

2

3

5

a + b == c

b == a.next

c == b.next

n.a.

n.a.

fibo step

3

3

5

8

a + b == c

b == a.next

c == b.next

n.a.

n.a.

fibo step

4

5

8

13

a + b == c

b == a.next

c == b.next

n.a.

n.a.

fibo step

5

8

13

21

a + b == c

b == a.next

c == b.next

n.a.

n.a.

fibo step

6

13

21

34

a + b == c

b == a.next

c == b.next

n.a.

n.a.

padding

7

padding

8

padding

9

Exposing Signals#

In prior examples, the witnesses we generate are all PRIVATE by default. While they are visible to the prover, or in the context of Chiquito, the writer of trace function, they are not visible to the verifier. However, it’s common in zero knowledge proof systems to expose some witness values to both the prover and the verifier. Common examples include output of a hash function or the root of a Merkle tree.

For pure demonstration purpose, say that we want to expose the result of our Fibonacci calculation after an arbitrary number of n rounds (where n <= 10). We also want to expose the round number n. Because we need to specify which instance of the signal to expose and because we want to allow for witnesses with arbitrary number of step instances, we cannot expose a specific step instance. Rather, the best practice is to copy over the Fibonacci result for all padding steps and n for all steps through the last step and expose the last step instance.

Building on top of the table example above where n == 7, we create a new signal n and populate the three padding step instances:

Step Type

Step Instance Index

Signals

Setups

a

b

c

n

constraint 1

constraint 2

constraint 3

constraint 4

constraint 5

constraint 6

fibo first step

0

1

1

2

7

a + b == c

b == a.next

c == b.next

a == 1

b == 1

n == n.next

fibo step

1

1

2

3

7

a + b == c

b == a.next

c == b.next

n == n.next

n.a.

n.a.

fibo step

2

2

3

5

7

a + b == c

b == a.next

c == b.next

n == n.next

n.a.

n.a.

fibo step

3

3

5

8

7

a + b == c

b == a.next

c == b.next

n == n.next

n.a.

n.a.

fibo step

4

5

8

13

7

a + b == c

b == a.next

c == b.next

n == n.next

n.a.

n.a.

fibo step

5

8

13

21

7

a + b == c

b == a.next

c == b.next

n == n.next

n.a.

n.a.

fibo step

6

13

21

34

7

a + b == c

b == a.next

c == b.next

n == n.next

n.a.

n.a.

padding

7

21

34

n.a.

7

n == n.next

b == b.next

n.a.

n.a.

n.a.

n.a.

padding

8

n.a.

34

n.a.

7

n == n.next

b == b.next

n.a.

n.a.

n.a.

n.a.

padding

9

n.a.

34

n.a.

7

n == n.next

b == b.next

n.a.

n.a.

n.a.

n.a.

Coding up the Concepts#

Now that we introduced padding and exposing signals, let’s express the table above in a Chiquito circuit.

First, let’s add the padding step type:

class Padding(StepType):
    def setup(self):
        self.transition(eq(self.circuit.b, self.circuit.b.next()))
        self.transition(eq(self.circuit.n, self.circuit.n.next()))

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

In setup, we added two transition constraints.

  • b == b.next copies the Fibonacci result after n rounds through the last padding step. Note that “b” in the first Padding step instance equals “c” in the last FiboStep instance, which is the final result.

  • n == n.next copies the n for exposing at the last step instance. Note that exposing b and n is done at the circuit level setup, which we leave for later.

Note that the new signal n is not added in setup, because it’ll be a forward signal to be added in circuit level setup.

In wg, we assign a_value, b_value, and n_value to their corresponding signals. We assign a_value, although it’s not exposed in the last padding step, because the last FiboStep instance constraints b == a.next.

Second, let’s modify all existing step types to account for the new signal n, basically adding a new constraint n == n.next in setup and assigning n_value in wg:

class FiboFirstStep(StepType):
    def setup(self):
        # ...
        self.transition(eq(self.circuit.n, self.circuit.n.next()))

    def wg(self, args):
        a_value, b_value, n_value = args
        # ...
        self.assign(self.circuit.n, F(n_value))

class FiboStep(StepType):
    def setup(self):
        # ...
        self.transition(eq(self.circuit.n, self.circuit.n.next()))

    def wg(self, args):
        a_value, b_value, n_value = args
        # ...
        self.assign(self.circuit.n, F(n_value))

Third, let’s modify the circuit setup:

class Fibonacci(Circuit):
    def setup(self):
        self.a = self.forward("a")
        self.b = self.forward("b")
        self.n = self.forward("n")
        
        self.fibo_first_step = self.step_type(FiboFirstStep(self, "fibo_first_step"))
        self.fibo_step = self.step_type(FiboStep(self, "fibo_step"))
        self.padding = self.step_type(Padding(self, "padding"))

        self.pragma_num_steps(10)
        self.pragma_first_step(self.fibo_first_step)
        self.pragma_last_step(self.padding)

        self.expose(self.b, Last())
        self.expose(self.n, Last())
        
    def trace(self, n):
        # TODO

The code above did a few things:

  • Add forward signal n and append it to the circuit

  • Add padding step and append it to the circuit

  • Modify pragma_num_steps to 10, the maximum number of steps that won’t be exceeded by all plausible witnesses

  • Constrain that the last step instance is Padding

  • Expose the last instances of signals b (the final Fibonacci result) and n (the number of non-padding step instances). self.expose takes two parameters: the signal to expose and the step instance of the signal to expose. In the example above Last() means the last step instance. In Chiquito, you can also specify First() for the first step instance or Step(index) for the step instance at a specific index.

Finally, we instantiate step instances and generate witness using trace, with the following step instance combination:

  • FiboFirstStep for the 1st step instance

  • FiboStep for the 2nd through n-th step instance

  • Padding for the rest step instances such that there are 10 step instances in total, as specified by self.pragma_num_steps(10)

class Fibonacci(Circuit):
    def setup(self):
        # ...
        
    def trace(self, n):
        self.add(self.fibo_first_step, (1, 1, n))
        a = 1
        b = 2
        for i in range(1, n):
            self.add(self.fibo_step, (a, b, n))
            prev_a = a
            a = b
            b += prev_a
        while(self.needs_padding()):
            self.add(self.padding, (a, b, n))

In the code above, we added a new parameter n for trace, which is the user’s input when calling gen_witness. n is passed into self.add as an input parameter to instantiate different step types. Again, note the matching relationship of witness generation parameters between self.add and wg:

  • In self.add(self.fibo_first_step, (1, 1, n)), (1, 1, n) correspond to a_value, b_value, n_value in FiboFirstStep wg

  • In self.add(self.fibo_step, (a, b, n)), (a, b, n) correspond to a_value, b_value, n_value in FiboStep wg

  • In self.add(self.padding, (a, b, n)), (a, b, n) correspond to a_value, b_value, n_value in Padding wg

Putting Everything Together#

Putting all pieces together, we have the following circuit, which allows for a fixed circuit setup with 10 step instances, as well as flexible witnesses with an arbitrary number of n step instances up to 10, filled with Padding step instances if fewer than 10:

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

class FiboFirstStep(StepType):
    def setup(self):
        self.c = self.internal("c")
        self.constr(eq(self.circuit.a, 1))
        self.constr(eq(self.circuit.b, 1))
        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()))
        self.transition(eq(self.circuit.n, self.circuit.n.next()))

    def wg(self, args):
        a_value, b_value, n_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))
        self.assign(self.circuit.n, F(n_value))

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()))
        self.transition(eq(self.circuit.n, self.circuit.n.next()))

    def wg(self, args):
        a_value, b_value, n_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))
        self.assign(self.circuit.n, F(n_value))

class Padding(StepType):
    def setup(self):
        self.transition(eq(self.circuit.b, self.circuit.b.next()))
        self.transition(eq(self.circuit.n, self.circuit.n.next()))

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

class Fibonacci(Circuit):
    def setup(self):
        self.a = self.forward("a")
        self.b = self.forward("b")
        self.n = self.forward("n")
        
        self.fibo_first_step = self.step_type(FiboFirstStep(self, "fibo_first_step"))
        self.fibo_step = self.step_type(FiboStep(self, "fibo_step"))
        self.padding = self.step_type(Padding(self, "padding"))

        self.pragma_num_steps(10)
        self.pragma_first_step(self.fibo_first_step)
        self.pragma_last_step(self.padding)

        self.expose(self.b, Last())
        self.expose(self.n, Last())
        
    def trace(self, n):
        self.add(self.fibo_first_step, (1, 1, n))
        a = 1
        b = 2
        for i in range(1, n):
            self.add(self.fibo_step, (a, b, n))
            prev_a = a
            a = b
            b += prev_a
        while(self.needs_padding()):
            self.add(self.padding, (a, b, n))

We initialize the circuit, generate a witness with 7 fibo first and fibo step instances (plus 3 padding step instances), and print the witness:

fibo = Fibonacci()
fibo_witness = fibo.gen_witness(7)
print(fibo_witness)
TraceWitness(
	step_instances={
		StepInstance(
			step_type_uuid=108744396990479038257644790982661245450,
			assignments={
				a = 1,
				b = 1,
				c = 2,
				n = 7
			},
		),
		StepInstance(
			step_type_uuid=108744457758479686700441988961231571466,
			assignments={
				a = 1,
				b = 2,
				c = 3,
				n = 7
			},
		),
		StepInstance(
			step_type_uuid=108744457758479686700441988961231571466,
			assignments={
				a = 2,
				b = 3,
				c = 5,
				n = 7
			},
		),
		StepInstance(
			step_type_uuid=108744457758479686700441988961231571466,
			assignments={
				a = 3,
				b = 5,
				c = 8,
				n = 7
			},
		),
		StepInstance(
			step_type_uuid=108744457758479686700441988961231571466,
			assignments={
				a = 5,
				b = 8,
				c = 13,
				n = 7
			},
		),
		StepInstance(
			step_type_uuid=108744457758479686700441988961231571466,
			assignments={
				a = 8,
				b = 13,
				c = 21,
				n = 7
			},
		),
		StepInstance(
			step_type_uuid=108744457758479686700441988961231571466,
			assignments={
				a = 13,
				b = 21,
				c = 34,
				n = 7
			},
		),
		StepInstance(
			step_type_uuid=108744488182094092178673267372068571658,
			assignments={
				a = 21,
				b = 34,
				n = 7
			},
		),
		StepInstance(
			step_type_uuid=108744488182094092178673267372068571658,
			assignments={
				a = 21,
				b = 34,
				n = 7
			},
		),
		StepInstance(
			step_type_uuid=108744488182094092178673267372068571658,
			assignments={
				a = 21,
				b = 34,
				n = 7
			},
		)
	},
)

Generate and verify proof with this witness. Should return Ok(()):

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(
    {
        108744488182094092178673267372068571658: StepType {
            id: 108744488182094092178673267372068571658,
            signals: [],
            constraints: [],
            transition_constraints: [
                TransitionConstraint {
                    annotation: "(b == next(b))",
                    expr: (b + (-next(b))),
                },
                TransitionConstraint {
                    annotation: "(n == next(n))",
                    expr: (n + (-next(n))),
                },
            ],
            lookups: [],
        },
        108744396990479038257644790982661245450: StepType {
            id: 108744396990479038257644790982661245450,
            signals: [
                InternalSignal {
                    id: 108744403645644689456949434524315027978,
                    annotation: "c",
                },
            ],
            constraints: [
                Constraint {
                    annotation: "(a == 1)",
                    expr: (a + (-0xe0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)),
                },
                Constraint {
                    annotation: "(b == 1)",
                    expr: (b + (-0xe0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)),
                },
                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))),
                },
                TransitionConstraint {
                    annotation: "(n == next(n))",
                    expr: (n + (-next(n))),
                },
            ],
            lookups: [],
        },
        108744457758479686700441988961231571466: StepType {
            id: 108744457758479686700441988961231571466,
            signals: [
                InternalSignal {
                    id: 108744464651329825438233359614820878858,
                    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))),
                },
                TransitionConstraint {
                    annotation: "(n == next(n))",
                    expr: (n + (-next(n))),
                },
            ],
            lookups: [],
        },
    },
)
Ok(
    (),
)

Generate another witness with 4 fibo first and fibo step instances (plus 6 padding step instances) and verify. Should return Ok(()):

another_fibo_witness = fibo.gen_witness(4)
fibo.halo2_mock_prover(another_fibo_witness)
Ok(
    (),
)

In this chapter, we learned how to construct a circuit with a fixed setup but flexible witnesses. Specifically, we fixed the number of step instances for the circuit setup but allowed for arbitrary numbers of step instances for the witnesses, by allowing the user to customize witnesses with parameter n.