mirror of
https://github.com/qwang98/PyChiquito.git
synced 2026-04-22 03:00:16 -04:00
09ef47ad6a
* updated tutorial * update tutorial * new error emerge after updating submodule, was fully debugged previously * updated rust bindings and formatted python files * minor * updated submodule * cargo fmt * cleaned latest merge main; debugged and updated all tutorial files * addressed leo's comments' * removed num_step_instances * updated dependencies and deleted unwanted functions
253 lines
8.2 KiB
Plaintext
253 lines
8.2 KiB
Plaintext
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "aab29f93-4311-4bff-a123-38f412556922",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Part 3: Fibonacci Example\n",
|
|
"# Chapter 3: Witness\n",
|
|
"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.\n",
|
|
"| Step Type | Step Instance Index || Signals ||| Setups ||\n",
|
|
"| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n",
|
|
"||| a | b | c | constraint 1 | constraint 2 | constraint 3 |\n",
|
|
"| fibo step | 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next |\n",
|
|
"| fibo step | 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next |\n",
|
|
"| fibo step | 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next |\n",
|
|
"| fibo step | 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next |\n",
|
|
"| ... | ... || ... ||| ... ||\n",
|
|
"\n",
|
|
"## Setup\n",
|
|
"We setup the same circuit and witness in Part 1 which were successfully verified:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 1,
|
|
"id": "e0114f48-0fe6-4141-b29e-63bc07411092",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"167511621523169244061366759362598144522\n",
|
|
"Ok(\n",
|
|
" (),\n",
|
|
")\n"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"from chiquito.dsl import Circuit, StepType\n",
|
|
"from chiquito.cb import eq\n",
|
|
"from chiquito.util import F\n",
|
|
"\n",
|
|
"class FiboStep(StepType):\n",
|
|
" def setup(self):\n",
|
|
" self.c = self.internal(\"c\")\n",
|
|
" self.constr(eq(self.circuit.a + self.circuit.b, self.c))\n",
|
|
" self.transition(eq(self.circuit.b, self.circuit.a.next()))\n",
|
|
" self.transition(eq(self.c, self.circuit.b.next()))\n",
|
|
"\n",
|
|
" def wg(self, args):\n",
|
|
" a_value, b_value = args\n",
|
|
" self.assign(self.circuit.a, F(a_value))\n",
|
|
" self.assign(self.circuit.b, F(b_value))\n",
|
|
" self.assign(self.c, F(a_value + b_value))\n",
|
|
"\n",
|
|
"class Fibonacci(Circuit):\n",
|
|
" def setup(self):\n",
|
|
" self.a = self.forward(\"a\")\n",
|
|
" self.b = self.forward(\"b\")\n",
|
|
" \n",
|
|
" self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
|
|
" self.pragma_num_steps(4)\n",
|
|
" \n",
|
|
" def trace(self, args):\n",
|
|
" self.add(self.fibo_step, (1, 1))\n",
|
|
" a = 1\n",
|
|
" b = 2\n",
|
|
" for i in range(1, 4):\n",
|
|
" self.add(self.fibo_step, (a, b))\n",
|
|
" prev_a = a\n",
|
|
" a = b\n",
|
|
" b += prev_a\n",
|
|
"\n",
|
|
"fibo = Fibonacci()\n",
|
|
"fibo_witness = fibo.gen_witness(None)\n",
|
|
"fibo.halo2_mock_prover(fibo_witness)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "182101e0-f5ee-4c16-a7c1-d09909dcbb3b",
|
|
"metadata": {},
|
|
"source": [
|
|
"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)`."
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 2,
|
|
"id": "4e1481de-fa95-4022-9771-66aae4fe842c",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"evil_witness = fibo_witness.evil_witness_test(step_instance_indices=[0, 0], assignment_indices=[0, 1], rhs=[F(0), F(2)])"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "a9291c66-5fd9-48a1-8980-7b4283cc3ca8",
|
|
"metadata": {},
|
|
"source": [
|
|
"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:\n",
|
|
"\n",
|
|
"||Signals||\n",
|
|
"| :-: | :-: | :-: |\n",
|
|
"| a | b | c |\n",
|
|
"| 0 | 2 | 2 |\n",
|
|
"| 2 | 2 | 4 |\n",
|
|
"| 2 | 4 | 6 |\n",
|
|
"| 4 | 6 | 10 |\n",
|
|
"|| ... ||\n",
|
|
"\n",
|
|
"We use the `evil_witness_test` function to further modify the `evil_witness`:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 3,
|
|
"id": "77168c22-aaea-4890-89ba-b3b3cf37c86d",
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"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)])"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "19c5a476-e31e-4bc6-9bb2-7635c16b37ba",
|
|
"metadata": {},
|
|
"source": [
|
|
"Print the `evil_witness` to confirm that the swap was successful:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 4,
|
|
"id": "dcd26089-ecb0-4a5e-8296-318a7b644b98",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"TraceWitness(\n",
|
|
"\tstep_instances={\n",
|
|
"\t\tStepInstance(\n",
|
|
"\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n",
|
|
"\t\t\tassignments={\n",
|
|
"\t\t\t\ta = 0,\n",
|
|
"\t\t\t\tb = 2,\n",
|
|
"\t\t\t\tc = 2\n",
|
|
"\t\t\t},\n",
|
|
"\t\t),\n",
|
|
"\t\tStepInstance(\n",
|
|
"\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n",
|
|
"\t\t\tassignments={\n",
|
|
"\t\t\t\ta = 2,\n",
|
|
"\t\t\t\tb = 2,\n",
|
|
"\t\t\t\tc = 4\n",
|
|
"\t\t\t},\n",
|
|
"\t\t),\n",
|
|
"\t\tStepInstance(\n",
|
|
"\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n",
|
|
"\t\t\tassignments={\n",
|
|
"\t\t\t\ta = 2,\n",
|
|
"\t\t\t\tb = 4,\n",
|
|
"\t\t\t\tc = 6\n",
|
|
"\t\t\t},\n",
|
|
"\t\t),\n",
|
|
"\t\tStepInstance(\n",
|
|
"\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n",
|
|
"\t\t\tassignments={\n",
|
|
"\t\t\t\ta = 4,\n",
|
|
"\t\t\t\tb = 6,\n",
|
|
"\t\t\t\tc = 10\n",
|
|
"\t\t\t},\n",
|
|
"\t\t)\n",
|
|
"\t},\n",
|
|
")\n"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"print(evil_witness)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "52508cf9-6b61-4838-9f37-a2ed5d4e1dbd",
|
|
"metadata": {},
|
|
"source": [
|
|
"Now, generate and verify the proof with `evil_witness`:"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": 5,
|
|
"id": "044e067e-77fa-4027-94dd-e39a35e87de8",
|
|
"metadata": {},
|
|
"outputs": [
|
|
{
|
|
"name": "stdout",
|
|
"output_type": "stream",
|
|
"text": [
|
|
"Ok(\n",
|
|
" (),\n",
|
|
")\n"
|
|
]
|
|
}
|
|
],
|
|
"source": [
|
|
"fibo.halo2_mock_prover(evil_witness)"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"id": "7329efe2-c60f-4e4a-9288-27cab5af827f",
|
|
"metadata": {},
|
|
"source": [
|
|
"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?\n",
|
|
"\n",
|
|
"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`.\n",
|
|
"\n",
|
|
"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."
|
|
]
|
|
}
|
|
],
|
|
"metadata": {
|
|
"kernelspec": {
|
|
"display_name": "pychiquito_kernel",
|
|
"language": "python",
|
|
"name": "pychiquito_kernel"
|
|
},
|
|
"language_info": {
|
|
"codemirror_mode": {
|
|
"name": "ipython",
|
|
"version": 3
|
|
},
|
|
"file_extension": ".py",
|
|
"mimetype": "text/x-python",
|
|
"name": "python",
|
|
"nbconvert_exporter": "python",
|
|
"pygments_lexer": "ipython3",
|
|
"version": "3.11.4"
|
|
}
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 5
|
|
}
|