Chapter 3: Witness

Chapter 3: Witness#

Now, we will generate multiple witnesses to test the soundness of our circuit constraints. Note that we only intend to accept the following set of values for signals “a”, “b”, and “c”. “Soundness” in this context refers to faulty witness successfully verified against the constraints (false positives), so any set of witness assignments that is different from the table below but still passes the constraints incurs a “soundness” error.

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
…	…		…			…

Setup#

We setup the same circuit and witness in Chapter 2 which were successfully verified:

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

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

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(
    {
        106216022312130389015997492066735753738: StepType {
            id: 106216022312130389015997492066735753738,
            signals: [
                InternalSignal {
                    id: 106216029284208690269478589595931773450,
                    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(
    (),
)

Now we swap the first step instance from (1, 1, 2) to (0, 2, 2). We use the evil_witness_test function to swap step index 0 assignment index 0 to F(0) and step index 0 assignment index 0 to F(2).

evil_witness = fibo_witness.evil_witness_test(step_instance_indices=[0, 0], assignment_indices=[0, 1], rhs=[F(0), F(2)])

According to the three constraints a + b == c, b == a.next, and c == b.next, we swap the second step instance from (1, 2, 3) to (2, 2, 4) and modify the third and fourth step instances likewise, resulting in a new witness displayed below:

	Signals
a	b	c
0	2	2
2	2	4
2	4	6
4	6	10
	…

We use the evil_witness_test function to further modify the evil_witness:

evil_witness = evil_witness.evil_witness_test(step_instance_indices=[1, 1, 2, 2, 3, 3, 3], assignment_indices=[0, 2, 1, 2, 0, 1, 2], rhs=[F(2), F(4), F(4), F(6), F(4), F(6), F(10)])

Print the evil_witness to confirm that the swap was successful:

print(evil_witness)

TraceWitness(
	step_instances={
		StepInstance(
			step_type_uuid=106216022312130389015997492066735753738,
			assignments={
				a = 0,
				b = 2,
				c = 2
			},
		),
		StepInstance(
			step_type_uuid=106216022312130389015997492066735753738,
			assignments={
				a = 2,
				b = 2,
				c = 4
			},
		),
		StepInstance(
			step_type_uuid=106216022312130389015997492066735753738,
			assignments={
				a = 2,
				b = 4,
				c = 6
			},
		),
		StepInstance(
			step_type_uuid=106216022312130389015997492066735753738,
			assignments={
				a = 4,
				b = 6,
				c = 10
			},
		)
	},
)

Now, generate and verify the proof with evil_witness:

fibo.halo2_mock_prover(evil_witness)

Ok(
    (),
)

Surprisingly, evil_witness generated a proof that passed verification. This constitutes a soundness error, because the first step instance isn’t (1, 1, 2) as we initially specified, so why can the witness still pass the constraints?

The answer is simple, because in the first step instance, we never constrained the values of “a” and “b” to 1 and 1 in setup of FiboStep.

You might be wondering: in trace, didn’t we set “a” and “b” to (1, 1) and added FiboStep as the first step instance? In fact, trace and wg are really helper functions for the prover to easily generate a witness, whose data can be tampered with as shown in evil_witness_test. The only conditions enforced are defined in circuit and step type setup. Therefore, to fix the soundness error, we need to add more constraints, in Chapter 4.

Chapter 3: Witness

Contents

Chapter 3: Witness#

Setup#