github/chiquito
1
1
Fork 0
mirror of https://github.com/privacy-scaling-explorations/chiquito.git synced 2026-01-08 21:48:03 -05:00
Code Issues Packages Projects Releases Wiki Activity
Files
8817d866d2549b877220bcb5f98688129ddba3bd
chiquito/book/part2_chapter5.ipynb
Dimitris Apostolou 8817d866d2 Fix typos (#210)
2024-02-26 08:13:44 +00:00

475 lines
21 KiB
Plaintext
Raw Blame History

{
"cells": [
{
"cell_type": "markdown",
"id": "5ec470ae-aca1-4c7e-a048-d115633531d8",
"metadata": {},
"source": [
"# Chapter 5: Padding and Exposing Signals\n",
"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.\n",
"\n",
"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.\n",
"\n",
"## Padding\n",
"In Chiquito, you can achieve fixed circuit setup with flexible witnesses through a technique called \"padding\":\n",
"- 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.\n",
"- To have flexible witnesses that still pass the same circuit setup, we add \"padding step instances\" towards the end of the witness.\n",
"- For example, if we want to calculate 4 rounds for the Fibonacci series, we add 6 padding step instances:\n",
"\n",
"| Step Type | Step Instance Index || Signals |||| Setups |||\n",
"| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n",
"||| a | b | c | constraint 1 | constraint 2 | constraint 3 | constraint 4 | constraint 5 |\n",
"| fibo first step | 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next | a == 1 | b == 1 |\n",
"| fibo step | 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
"| fibo step | 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
"| fibo step | 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
"| padding | 4 |||||||||\n",
"| padding | 5 |||||||||\n",
"| padding | 6 |||||||||\n",
"| padding | 7 |||||||||\n",
"| padding | 8 |||||||||\n",
"| padding | 9 |||||||||\n",
"\n",
"- If we want 7 rounds, we add 3 padding step instances.\n",
"\n",
"| Step Type | Step Instance Index || Signals |||| Setups |||\n",
"| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n",
"||| a | b | c | constraint 1 | constraint 2 | constraint 3 | constraint 4 | constraint 5 |\n",
"| fibo first step | 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next | a == 1 | b == 1 |\n",
"| fibo step | 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
"| fibo step | 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
"| fibo step | 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
"| fibo step | 4 | 5 | 8 | 13 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
"| fibo step | 5 | 8 | 13 | 21 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
"| fibo step | 6 | 13 | 21 | 34 | a + b == c | b == a.next | c == b.next | n.a. | n.a. |\n",
"| padding | 7 |||||||||\n",
"| padding | 8 |||||||||\n",
"| padding | 9 |||||||||\n",
"\n",
"## Exposing Signals\n",
"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.\n",
"\n",
"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.\n",
"\n",
"Building on top of the table example above where `n == 7`, we create a new signal `n` and populate the three padding step instances:\n",
"\n",
"| Step Type | Step Instance Index || Signals ||||| Setups ||||\n",
"| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n",
"||| a | b | c | n | constraint 1 | constraint 2 | constraint 3 | constraint 4 | constraint 5 | constraint 6 |\n",
"| fibo first step | 0 | 1 | 1 | 2 | 7 | a + b == c | b == a.next | c == b.next | a == 1 | b == 1 | n == n.next |\n",
"| fibo step | 1 | 1 | 2 | 3 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
"| fibo step | 2 | 2 | 3 | 5 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
"| fibo step | 3 | 3 | 5 | 8 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
"| fibo step | 4 | 5 | 8 | 13 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
"| fibo step | 5 | 8 | 13 | 21 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
"| fibo step | 6 | 13 | 21 | 34 | 7 | a + b == c | b == a.next | c == b.next | n == n.next | n.a. | n.a. |\n",
"| padding | 7 | 21 | 34 | n.a. | 7 | n == n.next | b == b.next | n.a. | n.a. | n.a. | n.a. |\n",
"| padding | 8 | n.a. | 34 | n.a. | 7 | n == n.next | b == b.next | n.a. | n.a. | n.a. | n.a. |\n",
"| padding | 9 | n.a. | 34 | n.a. | 7 | n == n.next | b == b.next | n.a. | n.a. | n.a. | n.a. |\n",
"\n",
"## Coding up the Concepts\n",
"Now that we introduced padding and exposing signals, let's express the table above in a Chiquito circuit.\n",
"\n",
"First, let's add the padding step type: \n",
"\n",
"```python\n",
"class Padding(StepType):\n",
" def setup(self):\n",
" self.transition(eq(self.circuit.b, self.circuit.b.next()))\n",
" self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
"\n",
" def wg(self, args):\n",
" a_value, b_value, n_value = args\n",
" self.assign(self.circuit.a, F(a_value))\n",
" self.assign(self.circuit.b, F(b_value))\n",
" self.assign(self.circuit.n, F(n_value))\n",
"```\n",
"\n",
"In `setup`, we added two transition constraints. \n",
"- `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 == 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.\n",
"\n",
"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`.\n",
"\n",
"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`.\n",
"\n",
"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`:\n",
"\n",
"```python\n",
"class FiboFirstStep(StepType):\n",
" def setup(self):\n",
" # ...\n",
" self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
"\n",
" def wg(self, args):\n",
" a_value, b_value, n_value = args\n",
" # ...\n",
" self.assign(self.circuit.n, F(n_value))\n",
"\n",
"class FiboStep(StepType):\n",
" def setup(self):\n",
" # ...\n",
" self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
"\n",
" def wg(self, args):\n",
" a_value, b_value, n_value = args\n",
" # ...\n",
" self.assign(self.circuit.n, F(n_value))\n",
"```\n",
"\n",
"Third, let's modify the circuit `setup`:\n",
"\n",
"```python\n",
"class Fibonacci(Circuit):\n",
" def setup(self):\n",
" self.a = self.forward(\"a\")\n",
" self.b = self.forward(\"b\")\n",
" self.n = self.forward(\"n\")\n",
" \n",
" self.fibo_first_step = self.step_type(FiboFirstStep(self, \"fibo_first_step\"))\n",
" self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
" self.padding = self.step_type(Padding(self, \"padding\"))\n",
"\n",
" self.pragma_num_steps(10)\n",
" self.pragma_first_step(self.fibo_first_step)\n",
" self.pragma_last_step(self.padding)\n",
"\n",
" self.expose(self.b, Last())\n",
" self.expose(self.n, Last())\n",
" \n",
" def trace(self, n):\n",
" # TODO\n",
"```\n",
"\n",
"The code above did a few things:\n",
"- Add forward signal `n` and append it to the circuit\n",
"- Add padding step and append it to the circuit\n",
"- Modify `pragma_num_steps` to `10`, the maximum number of steps that won't be exceeded by all plausible witnesses\n",
"- Constrain that the last step instance is `Padding`\n",
"- 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`.\n",
"\n",
"Finally, we instantiate step instances and generate witness using `trace`, with the following step instance combination:\n",
"- `FiboFirstStep` for the 1st step instance\n",
"- `FiboStep` for the 2nd through n-th step instance\n",
"- `Padding` for the rest step instances such that there are 10 step instances in total, as specified by `self.pragma_num_steps(10)`\n",
"\n",
"```python\n",
"class Fibonacci(Circuit):\n",
" def setup(self):\n",
" # ...\n",
" \n",
" def trace(self, n):\n",
" self.add(self.fibo_first_step, (1, 1, n))\n",
" a = 1\n",
" b = 2\n",
" for i in range(1, n):\n",
" self.add(self.fibo_step, (a, b, n))\n",
" prev_a = a\n",
" a = b\n",
" b += prev_a\n",
" while(self.needs_padding()):\n",
" self.add(self.padding, (a, b, n))\n",
"```\n",
"\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`:\n",
"- In `self.add(self.fibo_first_step, (1, 1, n))`, `(1, 1, n)` correspond to `a_value, b_value, n_value` in `FiboFirstStep` `wg`\n",
"- In `self.add(self.fibo_step, (a, b, n))`, `(a, b, n)` correspond to `a_value, b_value, n_value` in `FiboStep` `wg`\n",
"- In `self.add(self.padding, (a, b, n))`, `(a, b, n)` correspond to `a_value, b_value, n_value` in `Padding` `wg`\n",
"\n",
"## Putting Everything Together\n",
"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:"
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "525c00f0-210f-4328-85a6-eac0beeb3124",
"metadata": {},
"outputs": [],
"source": [
"from chiquito.dsl import Circuit, StepType\n",
"from chiquito.cb import eq\n",
"from chiquito.util import F\n",
"from chiquito.chiquito_ast import Last\n",
"\n",
"class FiboFirstStep(StepType):\n",
" def setup(self):\n",
" self.c = self.internal(\"c\")\n",
" self.constr(eq(self.circuit.a, 1))\n",
" self.constr(eq(self.circuit.b, 1))\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",
" self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
"\n",
" def wg(self, args):\n",
" a_value, b_value, n_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",
" self.assign(self.circuit.n, F(n_value))\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",
" self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
"\n",
" def wg(self, args):\n",
" a_value, b_value, n_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",
" self.assign(self.circuit.n, F(n_value))\n",
"\n",
"class Padding(StepType):\n",
" def setup(self):\n",
" self.transition(eq(self.circuit.b, self.circuit.b.next()))\n",
" self.transition(eq(self.circuit.n, self.circuit.n.next()))\n",
"\n",
" def wg(self, args):\n",
" a_value, b_value, n_value = args\n",
" self.assign(self.circuit.a, F(a_value))\n",
" self.assign(self.circuit.b, F(b_value))\n",
" self.assign(self.circuit.n, F(n_value))\n",
"\n",
"class Fibonacci(Circuit):\n",
" def setup(self):\n",
" self.a = self.forward(\"a\")\n",
" self.b = self.forward(\"b\")\n",
" self.n = self.forward(\"n\")\n",
" \n",
" self.fibo_first_step = self.step_type(FiboFirstStep(self, \"fibo_first_step\"))\n",
" self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
" self.padding = self.step_type(Padding(self, \"padding\"))\n",
"\n",
" self.pragma_num_steps(10)\n",
" self.pragma_first_step(self.fibo_first_step)\n",
" self.pragma_last_step(self.padding)\n",
"\n",
" self.expose(self.b, Last())\n",
" self.expose(self.n, Last())\n",
" \n",
" def trace(self, n):\n",
" self.add(self.fibo_first_step, (1, 1, n))\n",
" a = 1\n",
" b = 2\n",
" for i in range(1, n):\n",
" self.add(self.fibo_step, (a, b, n))\n",
" prev_a = a\n",
" a = b\n",
" b += prev_a\n",
" while(self.needs_padding()):\n",
" self.add(self.padding, (a, b, n))"
]
},
{
"cell_type": "markdown",
"id": "048c2b46-fa2c-4e5d-afe6-4c47df8520ce",
"metadata": {},
"source": [
"We initialize the circuit, generate a witness with 7 fibo first and fibo step instances (plus 3 padding step instances), and print the witness:"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "39763670-a983-49cc-b812-164be8535997",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"TraceWitness(\n",
"\tstep_instances={\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878500215820179858595561677932595722,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 1,\n",
"\t\t\t\tb = 1,\n",
"\t\t\t\tc = 2,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t),\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878756122785100930893623775025826314,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 1,\n",
"\t\t\t\tb = 2,\n",
"\t\t\t\tc = 3,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t),\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878756122785100930893623775025826314,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 2,\n",
"\t\t\t\tb = 3,\n",
"\t\t\t\tc = 5,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t),\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878756122785100930893623775025826314,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 3,\n",
"\t\t\t\tb = 5,\n",
"\t\t\t\tc = 8,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t),\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878756122785100930893623775025826314,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 5,\n",
"\t\t\t\tb = 8,\n",
"\t\t\t\tc = 13,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t),\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878756122785100930893623775025826314,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 8,\n",
"\t\t\t\tb = 13,\n",
"\t\t\t\tc = 21,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t),\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878756122785100930893623775025826314,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 13,\n",
"\t\t\t\tb = 21,\n",
"\t\t\t\tc = 34,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t),\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878853573424993475991146187205511690,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 21,\n",
"\t\t\t\tb = 34,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t),\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878853573424993475991146187205511690,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 21,\n",
"\t\t\t\tb = 34,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t),\n",
"\t\tStepInstance(\n",
"\t\t\tstep_type_uuid=324878853573424993475991146187205511690,\n",
"\t\t\tassignments={\n",
"\t\t\t\ta = 21,\n",
"\t\t\t\tb = 34,\n",
"\t\t\t\tn = 7\n",
"\t\t\t},\n",
"\t\t)\n",
"\t},\n",
")\n"
]
}
],
"source": [
"fibo = Fibonacci()\n",
"fibo_witness = fibo.gen_witness(7)\n",
"print(fibo_witness)"
]
},
{
"cell_type": "markdown",
"id": "3aeae320-256c-4cf9-8ee2-92a5d7e58c07",
"metadata": {},
"source": [
"Generate and verify proof with this witness. Should return `Ok(())`:"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "3c429c18-a38e-48ed-b547-e0a9823a663a",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"325455621127741210431323199129011227146\n",
"Ok(\n",
" (),\n",
")\n"
]
}
],
"source": [
"fibo.halo2_mock_prover(fibo_witness)"
]
},
{
"cell_type": "markdown",
"id": "ed1c45e6-4f4d-434a-a061-18193af3ba44",
"metadata": {},
"source": [
"Generate another witness with 4 fibo first and fibo step instances (plus 6 padding step instances) and verify. Should return `Ok(())`:"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "3039a36e-30f0-4a81-b1a3-e22ffe1ce39f",
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Ok(\n",
" (),\n",
")\n"
]
}
],
"source": [
"another_fibo_witness = fibo.gen_witness(4)\n",
"fibo.halo2_mock_prover(another_fibo_witness)"
]
},
{
"cell_type": "markdown",
"id": "20d3d27c-6a3e-41f7-a476-5d589afe7247",
"metadata": {},
"source": [
"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`."
]
}
],
"metadata": {
"kernelspec": {
"display_name": "chiquito_kernel",
"language": "python",
"name": "chiquito_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
}
Reference in New Issue View Git Blame Copy Permalink