Chapter 4: Multiple StepTypes#
To avoid the soundness error from evil_witness in Chapter 3, we need to constrain that forward signals “a” and “b” are both 1 in the first step instance. Because this isn’t true for all step instances, we need to create a new step type, called FiboFirstStep, which is identical to FiboStep except two additional constraints for “a” and “b”:
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. |
… |
… |
… |
… |
The following shows the incremental code of FiboFirstStep compared to FiboStep:
class FiboFirstStep(StepType):
def setup(self):
# ...
self.constr(eq(self.circuit.a, 1))
self.constr(eq(self.circuit.b, 1))
def wg(self, args):
# ...
Next, in circuit setup, we need to append this step type and constrain that the first step instance is FiboFirstStep. Otherwise setup is identical to that in Chapter 3:
class Fibonacci(Circuit):
def setup(self):
# ...
self.fibo_first_step = self.step_type(FiboFirstStep(self, "fibo_first_step"))
self.pragma_first_step(self.fibo_first_step)
def trace(self, args):
# TODO
Finally, in circuit trace, we need to instantiate FiboFirstStep for the first step instance. Otherwise trace is identical to that in Chapter 3:
class Fibonacci(Circuit):
def setup(self):
# ...
def trace(self, args):
self.add(self.fibo_first_step, (1, 1))
# ...
Putting everything together, we have the following circuit with two step types:
from chiquito.dsl import Circuit, StepType
from chiquito.cb import eq
from chiquito.util import F
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()))
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 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_first_step = self.step_type(FiboFirstStep(self, "fibo_first_step"))
self.fibo_step = self.step_type(FiboStep(self, "fibo_step"))
self.pragma_num_steps(4)
self.pragma_first_step(self.fibo_first_step)
def trace(self, args):
self.add(self.fibo_first_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
fibo = Fibonacci()
fibo_witness = fibo.gen_witness(None)
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(
{
107394379366394054393668600732442036746: StepType {
id: 107394379366394054393668600732442036746,
signals: [
InternalSignal {
id: 107394386100787868107202960445504358922,
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))),
},
],
lookups: [],
},
107394432686947426494166216988007467530: StepType {
id: 107394432686947426494166216988007467530,
signals: [
InternalSignal {
id: 107394439262884915179504041986500463114,
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(
(),
)
We construct and pass over the same evil_witness from Chapter 3. This time evil_witness fails at the two new constraints we wrote, e.g. a == 1 and b == 1 from FiboFirstStep.
evil_witness = fibo_witness.evil_witness_test(step_instance_indices=[0, 0, 1, 1, 2, 2, 3, 3, 3], assignment_indices=[0, 1, 0, 2, 1, 2, 0, 1, 2], rhs=[F(0), F(2), F(2), F(4), F(4), F(6), F(4), F(6), F(10)])
fibo.halo2_mock_prover(evil_witness)
Err(
[
ConstraintCaseDebug {
constraint: Constraint {
gate: Gate {
index: 0,
name: "main",
},
index: 0,
name: "fibo_first_step::(a == 1) => (a + (-0xe0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x0e0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)))))",
},
location: InRegion {
region: Region 0 ('circuit'),
offset: 0,
},
cell_values: [
(
DebugVirtualCell {
name: "",
column: DebugColumn {
column_type: Advice,
index: 0,
annotation: "srcm forward a",
},
rotation: 0,
},
"0",
),
(
DebugVirtualCell {
name: "",
column: DebugColumn {
column_type: Advice,
index: 3,
annotation: "'step selector for fibo_first_step'",
},
rotation: 0,
},
"1",
),
(
DebugVirtualCell {
name: "",
column: DebugColumn {
column_type: Fixed,
index: 0,
annotation: "q_enable",
},
rotation: 0,
},
"1",
),
],
},
ConstraintCaseDebug {
constraint: Constraint {
gate: Gate {
index: 0,
name: "main",
},
index: 1,
name: "fibo_first_step::(b == 1) => (b + (-0xe0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x0e0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)))))",
},
location: InRegion {
region: Region 0 ('circuit'),
offset: 0,
},
cell_values: [
(
DebugVirtualCell {
name: "",
column: DebugColumn {
column_type: Advice,
index: 1,
annotation: "srcm forward b",
},
rotation: 0,
},
"0x1c14ef83340fbe5eccdd46def0f28c5c6df8ed2b3ec19a53592c68389ffffff6",
),
(
DebugVirtualCell {
name: "",
column: DebugColumn {
column_type: Advice,
index: 3,
annotation: "'step selector for fibo_first_step'",
},
rotation: 0,
},
"1",
),
(
DebugVirtualCell {
name: "",
column: DebugColumn {
column_type: Fixed,
index: 0,
annotation: "q_enable",
},
rotation: 0,
},
"1",
),
],
},
],
)
Constraint 0 ('fibo_first_step::(a == 1) => (a + (-0xe0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x0e0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0
- Column('Advice', 0 - srcm forward a)@0 = 0
- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1
- Column('Fixed', 0 - q_enable)@0 = 1
Constraint 1 ('fibo_first_step::(b == 1) => (b + (-0xe0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x0e0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0
- Column('Advice', 1 - srcm forward b)@0 = 0x1c14ef83340fbe5eccdd46def0f28c5c6df8ed2b3ec19a53592c68389ffffff6
- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1
- Column('Fixed', 0 - q_enable)@0 = 1
By adding new constraints to eliminate soundness errors, this chapter demonstrated an iterative way of developing zero knowledge circuits. Circuit engineer can proactively generate witnesses in edge cases and if a false positive passes the circuit, add more constraints to prevent these edge cases.
Besides, we learned that with multiple step types, Chiquito can create step instances with different signals and constraints, thereby allowing great versatility in circuit design.
Finally, this example shows again that circuit setup and witness generation are separate processes. There can be multiple witnesses for the same circuit setup. As a great analogy, a circuit can be considered a piece of “hardware” whereas its witnesses “software” that are compatible with the hardware.