From 35726a82cd0c49a34ee18821d011da793afefd00 Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Mon, 14 Aug 2023 18:57:47 +0800 Subject: [PATCH 01/11] updated tutorial --- pychiquito/fibonacci.py | 113 ++++++++++++++-------- pychiquito/tutorial_pt3_ch1.ipynb | 2 +- pychiquito/tutorial_pt3_ch2.ipynb | 90 +++++++----------- pychiquito/tutorial_pt3_ch3.ipynb | 152 ++++++++++++++++++++++-------- 4 files changed, 225 insertions(+), 132 deletions(-) diff --git a/pychiquito/fibonacci.py b/pychiquito/fibonacci.py index e9398e0..4c5f1ec 100644 --- a/pychiquito/fibonacci.py +++ b/pychiquito/fibonacci.py @@ -5,63 +5,102 @@ from cb import eq from query import Queriable from util import F +import rust_chiquito -class Fibonacci(Circuit): - def setup(self: Fibonacci): - self.a: Queriable = self.forward("a") - self.b: Queriable = self.forward("b") +# class Fibonacci(Circuit): +# def setup(self: Fibonacci): +# self.a: Queriable = self.forward("a") +# self.b: Queriable = self.forward("b") - self.fibo_step = self.step_type(FiboStep(self, "fibo_step")) - self.fibo_last_step = self.step_type(FiboLastStep(self, "fibo_last_step")) +# self.fibo_step = self.step_type(FiboStep(self, "fibo_step")) +# self.fibo_last_step = self.step_type(FiboLastStep(self, "fibo_last_step")) - self.pragma_first_step(self.fibo_step) - self.pragma_last_step(self.fibo_last_step) - self.pragma_num_steps(11) - # self.pragma_disable_q_enable() +# self.pragma_first_step(self.fibo_step) +# self.pragma_last_step(self.fibo_last_step) +# self.pragma_num_steps(11) +# # self.pragma_disable_q_enable() - # self.expose(self.b, First()) - # self.expose(self.a, Last()) - # self.expose(self.a, Step(1)) +# # self.expose(self.b, First()) +# # self.expose(self.a, Last()) +# # self.expose(self.a, Step(1)) + +# def trace(self: Fibonacci, args: Any): +# self.add(self.fibo_step, (1, 1)) +# a = 1 +# b = 2 +# for i in range(1, 10): +# self.add(self.fibo_step, (a, b)) +# prev_a = a +# a = b +# b += prev_a +# self.add(self.fibo_last_step, (a, b)) + + +# class FiboStep(StepType): +# def setup(self: FiboStep): +# 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: FiboStep, args: Tuple[int, int]): +# 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)) - def trace(self: Fibonacci, args: Any): - self.add(self.fibo_step, (1, 1)) - a = 1 - b = 2 - for i in range(1, 10): - self.add(self.fibo_step, (a, b)) - prev_a = a - a = b - b += prev_a - self.add(self.fibo_last_step, (a, b)) +# class FiboLastStep(StepType): +# def setup(self: FiboLastStep): +# self.c = self.internal("c") +# self.constr(eq(self.circuit.a + self.circuit.b, self.c)) + +# def wg(self: FiboLastStep, values=Tuple[int, int]): +# a_value, b_value = values +# 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)) + + +# fibo = Fibonacci() +# fibo_witness = fibo.gen_witness(None) +# fibo.halo2_mock_prover(fibo_witness) class FiboStep(StepType): - def setup(self: FiboStep): + 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: FiboStep, args: Tuple[int, int]): + 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 FiboLastStep(StepType): - def setup(self: FiboLastStep): - self.c = self.internal("c") - self.constr(eq(self.circuit.a + self.circuit.b, self.c)) - - def wg(self: FiboLastStep, values=Tuple[int, int]): - a_value, b_value = values - 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) + self.pragma_first_step(self.fibo_step) + + 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() +print(fibo) +rust_chiquito.convert_and_print_ast(fibo.get_ast_json()) fibo_witness = fibo.gen_witness(None) fibo.halo2_mock_prover(fibo_witness) diff --git a/pychiquito/tutorial_pt3_ch1.ipynb b/pychiquito/tutorial_pt3_ch1.ipynb index 1f9abf0..01325c7 100644 --- a/pychiquito/tutorial_pt3_ch1.ipynb +++ b/pychiquito/tutorial_pt3_ch1.ipynb @@ -26,7 +26,7 @@ "| 3 | 5 | 8 |\n", "|| ... ||\n", "\n", - "Besides assigning values to these signals, we also need to define the mathematical relationships among them, which we call \"constraints: in Chiquito. For each row:\n", + "Besides assigning values to these signals, we also need to define the mathematical relationships among them, which we call \"constraints\" in Chiquito. For each row:\n", "- a + b == c\n", "- b = a in the next row\n", "- c = b in the next row\n", diff --git a/pychiquito/tutorial_pt3_ch2.ipynb b/pychiquito/tutorial_pt3_ch2.ipynb index 390919e..d9db81a 100644 --- a/pychiquito/tutorial_pt3_ch2.ipynb +++ b/pychiquito/tutorial_pt3_ch2.ipynb @@ -8,19 +8,7 @@ "# Part 3: Fibonacci Example\n", "# Chapter 2: StepType and Circuit\n", "In this Chapter, we code out the concepts learned in Chapter 1 in PyChiquito, but before that, let's import the dependencies first.\n", - "## Imports\n", - "These imports are for the typing hints included in this example. They are not required, because Python is a dynamically typed interpreted language and typings aren't enforced." - ] - }, - { - "cell_type": "code", - "execution_count": 1, - "id": "88bf1890-2e87-4aeb-967c-809fa1ddb6e6", - "metadata": {}, - "outputs": [], - "source": [ - "from __future__ import annotations\n", - "from typing import Tuple" + "## Imports" ] }, { @@ -36,7 +24,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 1, "id": "bf77f66c-2e81-4b51-b7f1-24c1be6c9b99", "metadata": {}, "outputs": [], @@ -95,11 +83,11 @@ "## FiboStep Witness Generation\n", "```\n", "class FiboStep(StepType):\n", - " def setup(self: FiboStep):\n", + " def setup(self):\n", " # ...\n", "\n", - " def wg(self: FiboStep, args: Tuple[int, int]):\n", - " a_value, b_value = args\n", + " def wg(self, args):\n", + " a_value, b_value = args # `args` is a tuple of (int, int)\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", @@ -138,6 +126,7 @@ " 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):\n", " # TODO\n", @@ -146,6 +135,8 @@ "\n", "Next, we append the only step type to the circuit by defining it as `self.fibo_step`. `step_type` function only has one argument, which is the `FiboStep` object created using its class constructor.\n", "\n", + "Finally, we constrain the total number of step instances to 4, by using `self.pragma_num_steps`.\n", + "\n", "## Circuit Trace\n", "Now we instantiate step types and assign witness values using `trace`:\n", "```\n", @@ -165,18 +156,18 @@ "```\n", "`trace` takes two arguments, the `Fibonacci` circuit itself and the witness value assignment arguments `args`. We call `self.add` to instantiate `fibo_step` we defined and pass in the witness values for \"a\" and \"b\". Note that we only hardcoded witness values for the first step instance as `(1, 1)`, because all other witness values can be calculated given the nature of Fibonacci. \n", "\n", - "Note that `self.add` creates step instance by calling `wg` associated with the step type. Therefore, the second input of `self.add`, e.g. `(a, b)` in `self.add(self.fibo_step, (a, b))`, needs to match `args` in `FiboStep` `wg`, i.e. tuple of `a_value, b_value`.\n", + "Note that `self.add` creates step instance by calling `wg` function associated with the step type, which we defined earlier. The second argument of `self.add`, e.g. `(a, b)` in `self.add(self.fibo_step, (a, b))`, is actually the input for `wg`. Therefore, `(a, b)` needs to match `args` in `FiboStep` `wg`, i.e. tuple of `a_value, b_value`.\n", "\n", "We didn't pass in witness values for \"c\", because they are calculated in `FiboStep` `wg`.\n", "\n", "Note that we need to pass in witness value assignments in a single argument `args` and therefore we use a tuple in this case. `args` can really be any data type as long as it's one single argument.\n", - "FiboStep\n", + "\n", "After creating the first `FiboStep` instance, we loop over `FiboStep` instantiation for 3 more times, each time calculating and passing in a different tuple of assignments. Voila, here's our Fibonacci circuit with 4 `FiboStep` instances:" ] }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 8, "id": "d7c21e5d-5a9c-47b8-8c18-ed59fe885709", "metadata": {}, "outputs": [], @@ -200,6 +191,7 @@ " 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", @@ -223,7 +215,7 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 9, "id": "c0c9db95-8da8-49d6-a403-895491c833fe", "metadata": {}, "outputs": [], @@ -241,7 +233,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 10, "id": "d259b3b8-a15c-416c-9076-24c06f5b22e6", "metadata": {}, "outputs": [ @@ -251,11 +243,11 @@ "text": [ "ASTCircuit(\n", "\tstep_types={\n", - "\t\t175487786213455723101965983777064356362: ASTStepType(\n", - "\t\t\tid=175487786213455723101965983777064356362,\n", + "\t\t257330087498007521101900253648606857738: ASTStepType(\n", + "\t\t\tid=257330087498007521101900253648606857738,\n", "\t\t\tname='fibo_step',\n", "\t\t\tsignals=[\n", - "\t\t\t\tInternalSignal(id=175487817112439103662857355366257789450, annotation='c')\n", + "\t\t\t\tInternalSignal(id=257330145334566156513039079911908313610, annotation='c')\n", "\t\t\t],\n", "\t\t\tconstraints=[\n", "\t\t\t\tConstraint(\n", @@ -268,26 +260,26 @@ "\t\t\t\tTransitionConstraint((c == next(b)))\n", "\t\t\t],\n", "\t\t\tannotations={\n", - "\t\t\t\t175487817112439103662857355366257789450: c\n", + "\t\t\t\t257330145334566156513039079911908313610: c\n", "\t\t\t}\n", "\t\t)\n", "\t},\n", "\tforward_signals=[\n", - "\t\tForwardSignal(id=175487708569856459120001313145084316170, phase=0, annotation='a'),\n", - "\t\tForwardSignal(id=175487756106753967678767124757946698250, phase=0, annotation='b')\n", + "\t\tForwardSignal(id=257329883089348234298700045805266012682, phase=0, annotation='a'),\n", + "\t\tForwardSignal(id=257330063729558766821948768389220141578, phase=0, annotation='b')\n", "\t],\n", "\tshared_signals=[],\n", "\tfixed_signals=[],\n", "\texposed=[],\n", "\tannotations={\n", - "\t\t175487708569856459120001313145084316170: a,\n", - "\t\t175487756106753967678767124757946698250: b,\n", - "\t\t175487786213455723101965983777064356362: fibo_step\n", + "\t\t257329883089348234298700045805266012682: a,\n", + "\t\t257330063729558766821948768389220141578: b,\n", + "\t\t257330087498007521101900253648606857738: fibo_step\n", "\t},\n", "\tfixed_gen=None,\n", "\tfirst_step=None,\n", "\tlast_step=None,\n", - "\tnum_steps=0\n", + "\tnum_steps=4\n", "\tq_enable=True\n", ")\n" ] @@ -307,7 +299,7 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 11, "id": "24a0d3d8-710e-42fe-99ae-7491b50d7cd7", "metadata": {}, "outputs": [], @@ -325,7 +317,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 12, "id": "d1aaca8a-35eb-4c9d-8794-56869f696849", "metadata": {}, "outputs": [ @@ -336,7 +328,7 @@ "TraceWitness(\n", "\tstep_instances={\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=175487786213455723101965983777064356362,\n", + "\t\t\tstep_type_uuid=257330087498007521101900253648606857738,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 1,\n", @@ -344,7 +336,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=175487786213455723101965983777064356362,\n", + "\t\t\tstep_type_uuid=257330087498007521101900253648606857738,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 2,\n", @@ -352,7 +344,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=175487786213455723101965983777064356362,\n", + "\t\t\tstep_type_uuid=257330087498007521101900253648606857738,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 3,\n", @@ -360,7 +352,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=175487786213455723101965983777064356362,\n", + "\t\t\tstep_type_uuid=257330087498007521101900253648606857738,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 3,\n", "\t\t\t\tb = 5,\n", @@ -386,28 +378,18 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 13, "id": "a3f8d245-adab-4e68-9ee6-5f6bafc12bd1", "metadata": {}, "outputs": [ { - "name": "stderr", + "name": "stdout", "output_type": "stream", "text": [ - "thread '' panicked at 'attempt to subtract with overflow', src/chiquito/src/compiler.rs:808:21\n", - "note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace\n" - ] - }, - { - "ename": "PanicException", - "evalue": "attempt to subtract with overflow", - "output_type": "error", - "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[0;31mPanicException\u001b[0m Traceback (most recent call last)", - "Cell \u001b[0;32mIn[8], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mfibo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mhalo2_mock_prover\u001b[49m\u001b[43m(\u001b[49m\u001b[43mfibo_witness\u001b[49m\u001b[43m)\u001b[49m\n", - "File \u001b[0;32m~/Documents/repo/pychiquito-7_25_23-v7/PyChiquito/pychiquito/dsl.py:103\u001b[0m, in \u001b[0;36mCircuit.halo2_mock_prover\u001b[0;34m(self, witness)\u001b[0m\n\u001b[1;32m 101\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id \u001b[38;5;241m==\u001b[39m \u001b[38;5;241m0\u001b[39m:\n\u001b[1;32m 102\u001b[0m ast_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mget_ast_json()\n\u001b[0;32m--> 103\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id: \u001b[38;5;28mint\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[43mrust_chiquito\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mast_to_halo2\u001b[49m\u001b[43m(\u001b[49m\u001b[43mast_json\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 104\u001b[0m witness_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m witness\u001b[38;5;241m.\u001b[39mget_witness_json()\n\u001b[1;32m 105\u001b[0m rust_chiquito\u001b[38;5;241m.\u001b[39mhalo2_mock_prover(witness_json, \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id)\n", - "\u001b[0;31mPanicException\u001b[0m: attempt to subtract with overflow" + "260415491222404396048804715742414637578\n", + "Ok(\n", + " (),\n", + ")\n" ] } ], diff --git a/pychiquito/tutorial_pt3_ch3.ipynb b/pychiquito/tutorial_pt3_ch3.ipynb index 872bfab..f05d594 100644 --- a/pychiquito/tutorial_pt3_ch3.ipynb +++ b/pychiquito/tutorial_pt3_ch3.ipynb @@ -23,35 +23,70 @@ }, { "cell_type": "code", - "execution_count": 1, + "execution_count": 11, "id": "e0114f48-0fe6-4141-b29e-63bc07411092", "metadata": {}, "outputs": [ { - "name": "stderr", + "name": "stdout", "output_type": "stream", "text": [ - "thread '' panicked at 'attempt to subtract with overflow', src/chiquito/src/compiler.rs:808:21\n", - "note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace\n" - ] - }, - { - "ename": "PanicException", - "evalue": "attempt to subtract with overflow", - "output_type": "error", - "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[0;31mPanicException\u001b[0m Traceback (most recent call last)", - "Cell \u001b[0;32mIn[1], line 40\u001b[0m\n\u001b[1;32m 38\u001b[0m fibo \u001b[38;5;241m=\u001b[39m Fibonacci()\n\u001b[1;32m 39\u001b[0m fibo_witness \u001b[38;5;241m=\u001b[39m fibo\u001b[38;5;241m.\u001b[39mgen_witness(\u001b[38;5;28;01mNone\u001b[39;00m)\n\u001b[0;32m---> 40\u001b[0m \u001b[43mfibo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mhalo2_mock_prover\u001b[49m\u001b[43m(\u001b[49m\u001b[43mfibo_witness\u001b[49m\u001b[43m)\u001b[49m\n", - "File \u001b[0;32m~/Documents/repo/pychiquito-7_25_23-v7/PyChiquito/pychiquito/dsl.py:103\u001b[0m, in \u001b[0;36mCircuit.halo2_mock_prover\u001b[0;34m(self, witness)\u001b[0m\n\u001b[1;32m 101\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id \u001b[38;5;241m==\u001b[39m \u001b[38;5;241m0\u001b[39m:\n\u001b[1;32m 102\u001b[0m ast_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mget_ast_json()\n\u001b[0;32m--> 103\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id: \u001b[38;5;28mint\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[43mrust_chiquito\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mast_to_halo2\u001b[49m\u001b[43m(\u001b[49m\u001b[43mast_json\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 104\u001b[0m witness_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m witness\u001b[38;5;241m.\u001b[39mget_witness_json()\n\u001b[1;32m 105\u001b[0m rust_chiquito\u001b[38;5;241m.\u001b[39mhalo2_mock_prover(witness_json, \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id)\n", - "\u001b[0;31mPanicException\u001b[0m: attempt to subtract with overflow" + "there's last step\n", + "4\n", + "1\n", + "237409307236249817799321350805519993354\n", + "Err(\n", + " [\n", + " ConstraintCaseDebug {\n", + " constraint: Constraint {\n", + " gate: Gate {\n", + " index: 0,\n", + " name: \"main\",\n", + " },\n", + " index: 3,\n", + " name: \"q_first => Product(Fixed { query_index: 2, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) })))\",\n", + " },\n", + " location: InRegion {\n", + " region: Region 0 ('circuit'),\n", + " offset: 0,\n", + " },\n", + " cell_values: [\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 3,\n", + " annotation: \"'step selector for fibo_step'\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"0\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Fixed,\n", + " index: 1,\n", + " annotation: \"q_first\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " ],\n", + " },\n", + " ],\n", + ")\n", + "Constraint 3 ('q_first => Product(Fixed { query_index: 2, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) })))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "- Column('Advice', 3 - 'step selector for fibo_step')@0 = 0\n", + "- Column('Fixed', 1 - q_first)@0 = 1\n", + "\n" ] } ], "source": [ - "from __future__ import annotations\n", - "from typing import Tuple\n", - "\n", "from dsl import Circuit, StepType\n", "from cb import eq\n", "from util import F\n", @@ -75,6 +110,8 @@ " self.b = self.forward(\"b\")\n", " \n", " self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n", + " self.pragma_first_step(self.fibo_step)\n", + " self.pragma_num_steps(4)\n", " \n", " def trace(self, args):\n", " self.add(self.fibo_step, (1, 1))\n", @@ -101,7 +138,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 12, "id": "4e1481de-fa95-4022-9771-66aae4fe842c", "metadata": {}, "outputs": [], @@ -119,7 +156,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 13, "id": "dcd26089-ecb0-4a5e-8296-318a7b644b98", "metadata": {}, "outputs": [ @@ -130,7 +167,7 @@ "TraceWitness(\n", "\tstep_instances={\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\n", + "\t\t\tstep_type_uuid=237407242550334696074761953987734931978,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 0,\n", "\t\t\t\tb = 2,\n", @@ -138,7 +175,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\n", + "\t\t\tstep_type_uuid=237407242550334696074761953987734931978,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 2,\n", @@ -146,7 +183,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\n", + "\t\t\tstep_type_uuid=237407242550334696074761953987734931978,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 3,\n", @@ -154,7 +191,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\n", + "\t\t\tstep_type_uuid=237407242550334696074761953987734931978,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 3,\n", "\t\t\t\tb = 5,\n", @@ -180,27 +217,62 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 14, "id": "044e067e-77fa-4027-94dd-e39a35e87de8", "metadata": {}, "outputs": [ { - "name": "stderr", + "name": "stdout", "output_type": "stream", "text": [ - "thread '' panicked at 'attempt to subtract with overflow', src/chiquito/src/compiler.rs:808:21\n" - ] - }, - { - "ename": "PanicException", - "evalue": "attempt to subtract with overflow", - "output_type": "error", - "traceback": [ - "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", - "\u001b[0;31mPanicException\u001b[0m Traceback (most recent call last)", - "Cell \u001b[0;32mIn[4], line 1\u001b[0m\n\u001b[0;32m----> 1\u001b[0m \u001b[43mfibo\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mhalo2_mock_prover\u001b[49m\u001b[43m(\u001b[49m\u001b[43mevil_witness\u001b[49m\u001b[43m)\u001b[49m\n", - "File \u001b[0;32m~/Documents/repo/pychiquito-7_25_23-v7/PyChiquito/pychiquito/dsl.py:103\u001b[0m, in \u001b[0;36mCircuit.halo2_mock_prover\u001b[0;34m(self, witness)\u001b[0m\n\u001b[1;32m 101\u001b[0m \u001b[38;5;28;01mif\u001b[39;00m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id \u001b[38;5;241m==\u001b[39m \u001b[38;5;241m0\u001b[39m:\n\u001b[1;32m 102\u001b[0m ast_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mget_ast_json()\n\u001b[0;32m--> 103\u001b[0m \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id: \u001b[38;5;28mint\u001b[39m \u001b[38;5;241m=\u001b[39m \u001b[43mrust_chiquito\u001b[49m\u001b[38;5;241;43m.\u001b[39;49m\u001b[43mast_to_halo2\u001b[49m\u001b[43m(\u001b[49m\u001b[43mast_json\u001b[49m\u001b[43m)\u001b[49m\n\u001b[1;32m 104\u001b[0m witness_json: \u001b[38;5;28mstr\u001b[39m \u001b[38;5;241m=\u001b[39m witness\u001b[38;5;241m.\u001b[39mget_witness_json()\n\u001b[1;32m 105\u001b[0m rust_chiquito\u001b[38;5;241m.\u001b[39mhalo2_mock_prover(witness_json, \u001b[38;5;28mself\u001b[39m\u001b[38;5;241m.\u001b[39mrust_ast_id)\n", - "\u001b[0;31mPanicException\u001b[0m: attempt to subtract with overflow" + "Err(\n", + " [\n", + " ConstraintCaseDebug {\n", + " constraint: Constraint {\n", + " gate: Gate {\n", + " index: 0,\n", + " name: \"main\",\n", + " },\n", + " index: 3,\n", + " name: \"q_first => Product(Fixed { query_index: 2, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) })))\",\n", + " },\n", + " location: InRegion {\n", + " region: Region 0 ('circuit'),\n", + " offset: 0,\n", + " },\n", + " cell_values: [\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 3,\n", + " annotation: \"'step selector for fibo_step'\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"0\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Fixed,\n", + " index: 1,\n", + " annotation: \"q_first\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " ],\n", + " },\n", + " ],\n", + ")\n", + "Constraint 3 ('q_first => Product(Fixed { query_index: 2, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) })))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "- Column('Advice', 3 - 'step selector for fibo_step')@0 = 0\n", + "- Column('Fixed', 1 - q_first)@0 = 1\n", + "\n" ] } ], From fffcd9b2fd7c5a428a8d255a1d3c69551aac3885 Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Tue, 15 Aug 2023 20:00:14 +0800 Subject: [PATCH 02/11] update tutorial --- pychiquito/dsl.py | 11 ++ pychiquito/fibonacci.py | 54 +++++- pychiquito/tutorial_pt3_ch3.ipynb | 168 ++++++----------- pychiquito/tutorial_pt3_ch4.ipynb | 244 ++++++++++++++++++++++++ pychiquito/tutorial_pt3_ch5.ipynb | 303 ++++++++++++++++++++++++++++++ 5 files changed, 657 insertions(+), 123 deletions(-) create mode 100644 pychiquito/tutorial_pt3_ch4.ipynb create mode 100644 pychiquito/tutorial_pt3_ch5.ipynb diff --git a/pychiquito/dsl.py b/pychiquito/dsl.py index e1d6b9c..bfaaaef 100644 --- a/pychiquito/dsl.py +++ b/pychiquito/dsl.py @@ -22,6 +22,7 @@ def __init__(self: Circuit): self.ast = ASTCircuit() self.witness = TraceWitness() self.rust_ast_id = 0 + self.num_step_instances = 0 self.mode = CircuitMode.SETUP self.setup() @@ -82,8 +83,18 @@ def pragma_disable_q_enable(self: Circuit) -> None: def add(self: Circuit, step_type: StepType, args: Any): assert self.mode == CircuitMode.Trace + if self.num_step_instances >= self.ast.num_steps: + raise ValueError(f"Number of step instances exceeds {self.ast.num_steps}") + self.num_step_instances += 1 step_instance: StepInstance = step_type.gen_step_instance(args) self.witness.step_instances.append(step_instance) + + def needs_padding(self: Circuit) -> bool: + return self.num_step_instances < self.ast.num_steps + + def padding(self: Circuit, step_type: StepType, args: Any): + while(self.needs_padding()): + self.add(step_type, args) def gen_witness(self: Circuit, args: Any) -> TraceWitness: self.mode = CircuitMode.Trace diff --git a/pychiquito/fibonacci.py b/pychiquito/fibonacci.py index 4c5f1ec..e00058d 100644 --- a/pychiquito/fibonacci.py +++ b/pychiquito/fibonacci.py @@ -1,5 +1,6 @@ from __future__ import annotations from typing import Tuple +from chiquito_ast import Last from dsl import Circuit, StepType from cb import eq @@ -67,6 +68,21 @@ # fibo_witness = fibo.gen_witness(None) # fibo.halo2_mock_prover(fibo_witness) +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") @@ -80,27 +96,49 @@ def wg(self, args): self.assign(self.circuit.b, F(b_value)) self.assign(self.c, F(a_value + b_value)) +class Padding(StepType): + def setup(self): + self.transition(eq(self.circuit.a, self.circuit.a.next())) + + def wg(self, a_value): + self.assign(self.circuit.a, F(a_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_step) + self.padding = self.step_type(Padding(self, "padding")) + + self.pragma_num_steps(100) + self.pragma_first_step(self.fibo_first_step) + self.pragma_last_step(self.padding) + + self.expose(self.a, Last()) - def trace(self, args): - self.add(self.fibo_step, (1, 1)) + def trace(self, n): + self.add(self.fibo_first_step, (1, 1)) a = 1 b = 2 - for i in range(1, 4): + for i in range(1, n): self.add(self.fibo_step, (a, b)) prev_a = a a = b b += prev_a + while(self.needs_padding()): + self.add(self.padding, prev_a) fibo = Fibonacci() -print(fibo) -rust_chiquito.convert_and_print_ast(fibo.get_ast_json()) -fibo_witness = fibo.gen_witness(None) +# print(fibo.get_ast_json()) + +# success +fibo_witness = fibo.gen_witness(30) +# print(fibo_witness) fibo.halo2_mock_prover(fibo_witness) + +# fails +# 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) diff --git a/pychiquito/tutorial_pt3_ch3.ipynb b/pychiquito/tutorial_pt3_ch3.ipynb index f05d594..7dd091a 100644 --- a/pychiquito/tutorial_pt3_ch3.ipynb +++ b/pychiquito/tutorial_pt3_ch3.ipynb @@ -23,7 +23,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 29, "id": "e0114f48-0fe6-4141-b29e-63bc07411092", "metadata": {}, "outputs": [ @@ -34,55 +34,10 @@ "there's last step\n", "4\n", "1\n", - "237409307236249817799321350805519993354\n", - "Err(\n", - " [\n", - " ConstraintCaseDebug {\n", - " constraint: Constraint {\n", - " gate: Gate {\n", - " index: 0,\n", - " name: \"main\",\n", - " },\n", - " index: 3,\n", - " name: \"q_first => Product(Fixed { query_index: 2, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) })))\",\n", - " },\n", - " location: InRegion {\n", - " region: Region 0 ('circuit'),\n", - " offset: 0,\n", - " },\n", - " cell_values: [\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Advice,\n", - " index: 3,\n", - " annotation: \"'step selector for fibo_step'\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"0\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Fixed,\n", - " index: 1,\n", - " annotation: \"q_first\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"1\",\n", - " ),\n", - " ],\n", - " },\n", - " ],\n", - ")\n", - "Constraint 3 ('q_first => Product(Fixed { query_index: 2, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) })))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", - "- Column('Advice', 3 - 'step selector for fibo_step')@0 = 0\n", - "- Column('Fixed', 1 - q_first)@0 = 1\n", - "\n" + "194893930440567836774815565731016083978\n", + "Ok(\n", + " (),\n", + ")\n" ] } ], @@ -110,7 +65,6 @@ " self.b = self.forward(\"b\")\n", " \n", " self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n", - " self.pragma_first_step(self.fibo_step)\n", " self.pragma_num_steps(4)\n", " \n", " def trace(self, args):\n", @@ -133,12 +87,12 @@ "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` function to swap step index 0 assignment index 0 to `F(0)` and step index 0 assignment index 0 to `F(2)`." + "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": 12, + "execution_count": 30, "id": "4e1481de-fa95-4022-9771-66aae4fe842c", "metadata": {}, "outputs": [], @@ -146,6 +100,35 @@ "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": 31, + "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", @@ -156,7 +139,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 32, "id": "dcd26089-ecb0-4a5e-8296-318a7b644b98", "metadata": {}, "outputs": [ @@ -167,7 +150,7 @@ "TraceWitness(\n", "\tstep_instances={\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=237407242550334696074761953987734931978,\n", + "\t\t\tstep_type_uuid=194891702544637935660060827380995459594,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 0,\n", "\t\t\t\tb = 2,\n", @@ -175,27 +158,27 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=237407242550334696074761953987734931978,\n", + "\t\t\tstep_type_uuid=194891702544637935660060827380995459594,\n", "\t\t\tassignments={\n", - "\t\t\t\ta = 1,\n", + "\t\t\t\ta = 2,\n", "\t\t\t\tb = 2,\n", - "\t\t\t\tc = 3\n", + "\t\t\t\tc = 4\n", "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=237407242550334696074761953987734931978,\n", + "\t\t\tstep_type_uuid=194891702544637935660060827380995459594,\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\tb = 4,\n", + "\t\t\t\tc = 6\n", "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=237407242550334696074761953987734931978,\n", + "\t\t\tstep_type_uuid=194891702544637935660060827380995459594,\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\ta = 4,\n", + "\t\t\t\tb = 6,\n", + "\t\t\t\tc = 10\n", "\t\t\t},\n", "\t\t)\n", "\t},\n", @@ -217,7 +200,7 @@ }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 33, "id": "044e067e-77fa-4027-94dd-e39a35e87de8", "metadata": {}, "outputs": [ @@ -225,54 +208,9 @@ "name": "stdout", "output_type": "stream", "text": [ - "Err(\n", - " [\n", - " ConstraintCaseDebug {\n", - " constraint: Constraint {\n", - " gate: Gate {\n", - " index: 0,\n", - " name: \"main\",\n", - " },\n", - " index: 3,\n", - " name: \"q_first => Product(Fixed { query_index: 2, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) })))\",\n", - " },\n", - " location: InRegion {\n", - " region: Region 0 ('circuit'),\n", - " offset: 0,\n", - " },\n", - " cell_values: [\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Advice,\n", - " index: 3,\n", - " annotation: \"'step selector for fibo_step'\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"0\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Fixed,\n", - " index: 1,\n", - " annotation: \"q_first\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"1\",\n", - " ),\n", - " ],\n", - " },\n", - " ],\n", - ")\n", - "Constraint 3 ('q_first => Product(Fixed { query_index: 2, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) })))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", - "- Column('Advice', 3 - 'step selector for fibo_step')@0 = 0\n", - "- Column('Fixed', 1 - q_first)@0 = 1\n", - "\n" + "Ok(\n", + " (),\n", + ")\n" ] } ], @@ -287,7 +225,7 @@ "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`. We also didn't constrain the first step instance to be `FiboStep`.\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." ] diff --git a/pychiquito/tutorial_pt3_ch4.ipynb b/pychiquito/tutorial_pt3_ch4.ipynb new file mode 100644 index 0000000..09b5299 --- /dev/null +++ b/pychiquito/tutorial_pt3_ch4.ipynb @@ -0,0 +1,244 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "291ef2c6-bce5-4166-973d-d34d04f31bfb", + "metadata": {}, + "source": [ + "# Part 3: Fibonacci Example\n", + "# Chapter 4: Multiple StepTypes" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "bb11d921-5785-4c25-bab8-07df4a049cec", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "there's last step\n", + "4\n", + "1\n", + "23084509758196191005326514439957645834\n", + "Ok(\n", + " (),\n", + ")\n", + "Err(\n", + " [\n", + " ConstraintCaseDebug {\n", + " constraint: Constraint {\n", + " gate: Gate {\n", + " index: 0,\n", + " name: \"main\",\n", + " },\n", + " index: 3,\n", + " name: \"fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", + " },\n", + " location: InRegion {\n", + " region: Region 0 ('circuit'),\n", + " offset: 0,\n", + " },\n", + " cell_values: [\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 0,\n", + " annotation: \"srcm forward a\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"0\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 4,\n", + " annotation: \"'step selector for fibo_first_step'\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Fixed,\n", + " index: 0,\n", + " annotation: \"q_enable\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " ],\n", + " },\n", + " ConstraintCaseDebug {\n", + " constraint: Constraint {\n", + " gate: Gate {\n", + " index: 0,\n", + " name: \"main\",\n", + " },\n", + " index: 4,\n", + " name: \"fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", + " },\n", + " location: InRegion {\n", + " region: Region 0 ('circuit'),\n", + " offset: 0,\n", + " },\n", + " cell_values: [\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 1,\n", + " annotation: \"srcm forward b\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"0x2bd7f2a3058aaa39904c1bc95d70baba121deb53c223d90fb8b7400adb62329c\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 4,\n", + " annotation: \"'step selector for fibo_first_step'\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Fixed,\n", + " index: 0,\n", + " annotation: \"q_enable\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " ],\n", + " },\n", + " ],\n", + ")\n", + "Constraint 3 ('fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "- Column('Advice', 0 - srcm forward a)@0 = 0\n", + "- Column('Advice', 4 - 'step selector for fibo_first_step')@0 = 1\n", + "- Column('Fixed', 0 - q_enable)@0 = 1\n", + "\n", + "Constraint 4 ('fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "- Column('Advice', 1 - srcm forward b)@0 = 0x2bd7f2a3058aaa39904c1bc95d70baba121deb53c223d90fb8b7400adb62329c\n", + "- Column('Advice', 4 - 'step selector for fibo_first_step')@0 = 1\n", + "- Column('Fixed', 0 - q_enable)@0 = 1\n", + "\n" + ] + } + ], + "source": [ + "from dsl import Circuit, StepType\n", + "from cb import eq\n", + "from util import F\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", + "\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 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_first_step = self.step_type(FiboFirstStep(self, \"fibo_first_step\"))\n", + " self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n", + " self.pragma_num_steps(4)\n", + " self.pragma_first_step(self.fibo_first_step)\n", + " \n", + " def trace(self, args):\n", + " self.add(self.fibo_first_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", + "\n", + "# success\n", + "fibo_witness = fibo.gen_witness(None)\n", + "fibo.halo2_mock_prover(fibo_witness)\n", + "\n", + "# fails\n", + "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)])\n", + "fibo.halo2_mock_prover(evil_witness)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "f9d65edb-99ee-44fa-ae20-f0bad93269ee", + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "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 +} diff --git a/pychiquito/tutorial_pt3_ch5.ipynb b/pychiquito/tutorial_pt3_ch5.ipynb new file mode 100644 index 0000000..067d270 --- /dev/null +++ b/pychiquito/tutorial_pt3_ch5.ipynb @@ -0,0 +1,303 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "5ec470ae-aca1-4c7e-a048-d115633531d8", + "metadata": {}, + "source": [ + "# Part 3: Fibonacci Example\n", + "# Chapter 5: Padding" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "525c00f0-210f-4328-85a6-eac0beeb3124", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "there's last step\n", + "100\n", + "1\n", + "243437734546730727453508299613593537034\n", + "Err(\n", + " [\n", + " ConstraintCaseDebug {\n", + " constraint: Constraint {\n", + " gate: Gate {\n", + " index: 0,\n", + " name: \"main\",\n", + " },\n", + " index: 1,\n", + " name: \"fibo_step::(b == next(a)) => (b + -next(a)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Fixed { query_index: 1, column_index: 2, 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(Advice { query_index: 4, column_index: 0, rotation: Rotation(1) })))))\",\n", + " },\n", + " location: InRegion {\n", + " region: Region 0 ('circuit'),\n", + " offset: 29,\n", + " },\n", + " cell_values: [\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 0,\n", + " annotation: \"srcm forward a\",\n", + " },\n", + " rotation: 1,\n", + " },\n", + " \"0x2b44d974a1c0ffa0e68289e4a08a5d135c0c499d8c12a99d91dac7b8d6e66fda\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 1,\n", + " annotation: \"srcm forward b\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"0x1c267c4330ad83827a0855880da9c6005115d28a51dc050bc18f2e2fd395960b\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 3,\n", + " annotation: \"'step selector for fibo_step'\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Fixed,\n", + " index: 0,\n", + " annotation: \"q_enable\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Fixed,\n", + " index: 2,\n", + " annotation: \"q_last\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"0\",\n", + " ),\n", + " ],\n", + " },\n", + " ConstraintCaseDebug {\n", + " constraint: Constraint {\n", + " gate: Gate {\n", + " index: 0,\n", + " name: \"main\",\n", + " },\n", + " index: 2,\n", + " name: \"fibo_step::(c == next(b)) => (c + -next(b)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Fixed { query_index: 1, column_index: 2, rotation: Rotation(0) })), Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 3, column_index: 2, rotation: Rotation(0) }, Negated(Advice { query_index: 5, column_index: 1, rotation: Rotation(1) })))))\",\n", + " },\n", + " location: InRegion {\n", + " region: Region 0 ('circuit'),\n", + " offset: 29,\n", + " },\n", + " cell_values: [\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 1,\n", + " annotation: \"srcm forward b\",\n", + " },\n", + " rotation: 1,\n", + " },\n", + " \"0\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 2,\n", + " annotation: \"srcm internal signal c\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"0x17070744f13ce2f9a83a99b62cb2cab684ee33df64353e180f880054ba7c05e4\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Advice,\n", + " index: 3,\n", + " annotation: \"'step selector for fibo_step'\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Fixed,\n", + " index: 0,\n", + " annotation: \"q_enable\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"1\",\n", + " ),\n", + " (\n", + " DebugVirtualCell {\n", + " name: \"\",\n", + " column: DebugColumn {\n", + " column_type: Fixed,\n", + " index: 2,\n", + " annotation: \"q_last\",\n", + " },\n", + " rotation: 0,\n", + " },\n", + " \"0\",\n", + " ),\n", + " ],\n", + " },\n", + " ],\n", + ")\n", + "Constraint 1 ('fibo_step::(b == next(a)) => (b + -next(a)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Fixed { query_index: 1, column_index: 2, 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(Advice { query_index: 4, column_index: 0, rotation: Rotation(1) })))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 29\n", + "- Column('Advice', 0 - srcm forward a)@1 = 0x2b44d974a1c0ffa0e68289e4a08a5d135c0c499d8c12a99d91dac7b8d6e66fda\n", + "- Column('Advice', 1 - srcm forward b)@0 = 0x1c267c4330ad83827a0855880da9c6005115d28a51dc050bc18f2e2fd395960b\n", + "- Column('Advice', 3 - 'step selector for fibo_step')@0 = 1\n", + "- Column('Fixed', 0 - q_enable)@0 = 1\n", + "- Column('Fixed', 2 - q_last)@0 = 0\n", + "\n", + "Constraint 2 ('fibo_step::(c == next(b)) => (c + -next(b)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Fixed { query_index: 1, column_index: 2, rotation: Rotation(0) })), Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 3, column_index: 2, rotation: Rotation(0) }, Negated(Advice { query_index: 5, column_index: 1, rotation: Rotation(1) })))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 29\n", + "- Column('Advice', 1 - srcm forward b)@1 = 0\n", + "- Column('Advice', 2 - srcm internal signal c)@0 = 0x17070744f13ce2f9a83a99b62cb2cab684ee33df64353e180f880054ba7c05e4\n", + "- Column('Advice', 3 - 'step selector for fibo_step')@0 = 1\n", + "- Column('Fixed', 0 - q_enable)@0 = 1\n", + "- Column('Fixed', 2 - q_last)@0 = 0\n", + "\n" + ] + } + ], + "source": [ + "from dsl import Circuit, StepType\n", + "from cb import eq\n", + "from util import F\n", + "from 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", + "\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 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 Padding(StepType):\n", + " def setup(self):\n", + " self.transition(eq(self.circuit.b, self.circuit.b.next()))\n", + "\n", + " def wg(self, b_value):\n", + " self.assign(self.circuit.b, F(b_value))\n", + "\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_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(100)\n", + " self.pragma_first_step(self.fibo_first_step)\n", + " self.pragma_last_step(self.padding)\n", + "\n", + " self.expose(self.a, Last())\n", + " \n", + " def trace(self, n):\n", + " self.add(self.fibo_first_step, (1, 1))\n", + " a = 1\n", + " b = 2\n", + " for i in range(1, n):\n", + " self.add(self.fibo_step, (a, b))\n", + " prev_a = a\n", + " a = b\n", + " b += prev_a\n", + " while(self.needs_padding()):\n", + " self.add(self.padding, prev_a)\n", + "\n", + "fibo = Fibonacci()\n", + "fibo_witness = fibo.gen_witness(30)\n", + "fibo.halo2_mock_prover(fibo_witness)" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "496c8617-8a8b-47a6-a6b7-c5a3a9ec8733", + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "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 +} From 4749da901081486bace4ffaaa2c067fe1d77a2e1 Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Wed, 16 Aug 2023 18:17:07 +0800 Subject: [PATCH 03/11] new error emerge after updating submodule, was fully debugged previously --- pychiquito/dsl.py | 1 + pychiquito/fibonacci.py | 106 ++---- pychiquito/tutorial_pt3_ch4.ipynb | 233 +++++++----- pychiquito/tutorial_pt3_ch5.ipynb | 572 +++++++++++++++++++----------- src/chiquito | 2 +- 5 files changed, 546 insertions(+), 368 deletions(-) diff --git a/pychiquito/dsl.py b/pychiquito/dsl.py index bfaaaef..59f922d 100644 --- a/pychiquito/dsl.py +++ b/pychiquito/dsl.py @@ -97,6 +97,7 @@ def padding(self: Circuit, step_type: StepType, args: Any): self.add(step_type, args) def gen_witness(self: Circuit, args: Any) -> TraceWitness: + self.num_step_instances = 0 self.mode = CircuitMode.Trace self.witness = TraceWitness() self.trace(args) diff --git a/pychiquito/fibonacci.py b/pychiquito/fibonacci.py index e00058d..0d69542 100644 --- a/pychiquito/fibonacci.py +++ b/pychiquito/fibonacci.py @@ -1,72 +1,7 @@ -from __future__ import annotations -from typing import Tuple -from chiquito_ast import Last - from dsl import Circuit, StepType from cb import eq -from query import Queriable from util import F -import rust_chiquito - - -# class Fibonacci(Circuit): -# def setup(self: Fibonacci): -# self.a: Queriable = self.forward("a") -# self.b: Queriable = self.forward("b") - -# self.fibo_step = self.step_type(FiboStep(self, "fibo_step")) -# self.fibo_last_step = self.step_type(FiboLastStep(self, "fibo_last_step")) - -# self.pragma_first_step(self.fibo_step) -# self.pragma_last_step(self.fibo_last_step) -# self.pragma_num_steps(11) -# # self.pragma_disable_q_enable() - -# # self.expose(self.b, First()) -# # self.expose(self.a, Last()) -# # self.expose(self.a, Step(1)) - -# def trace(self: Fibonacci, args: Any): -# self.add(self.fibo_step, (1, 1)) -# a = 1 -# b = 2 -# for i in range(1, 10): -# self.add(self.fibo_step, (a, b)) -# prev_a = a -# a = b -# b += prev_a -# self.add(self.fibo_last_step, (a, b)) - - -# class FiboStep(StepType): -# def setup(self: FiboStep): -# 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: FiboStep, args: Tuple[int, int]): -# 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 FiboLastStep(StepType): -# def setup(self: FiboLastStep): -# self.c = self.internal("c") -# self.constr(eq(self.circuit.a + self.circuit.b, self.c)) - -# def wg(self: FiboLastStep, values=Tuple[int, int]): -# a_value, b_value = values -# 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)) - - -# fibo = Fibonacci() -# fibo_witness = fibo.gen_witness(None) -# fibo.halo2_mock_prover(fibo_witness) +from chiquito_ast import Last class FiboFirstStep(StepType): def setup(self): @@ -76,12 +11,14 @@ def setup(self): 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 = 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): @@ -89,56 +26,55 @@ def setup(self): 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 = 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.a, self.circuit.a.next())) + self.transition(eq(self.circuit.b, self.circuit.b.next())) + self.transition(eq(self.circuit.n, self.circuit.n.next())) - def wg(self, a_value): + 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(100) + self.pragma_num_steps(10) self.pragma_first_step(self.fibo_first_step) self.pragma_last_step(self.padding) - self.expose(self.a, Last()) + self.expose(self.b, Last()) + self.expose(self.n, Last()) def trace(self, n): - self.add(self.fibo_first_step, (1, 1)) + 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)) + self.add(self.fibo_step, (a, b, n)) prev_a = a a = b b += prev_a while(self.needs_padding()): - self.add(self.padding, prev_a) + self.add(self.padding, (a, b, n)) fibo = Fibonacci() -# print(fibo.get_ast_json()) - -# success -fibo_witness = fibo.gen_witness(30) -# print(fibo_witness) +fibo_witness = fibo.gen_witness(7) fibo.halo2_mock_prover(fibo_witness) - -# fails -# 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) diff --git a/pychiquito/tutorial_pt3_ch4.ipynb b/pychiquito/tutorial_pt3_ch4.ipynb index 09b5299..8340e1c 100644 --- a/pychiquito/tutorial_pt3_ch4.ipynb +++ b/pychiquito/tutorial_pt3_ch4.ipynb @@ -9,23 +9,145 @@ "# Chapter 4: Multiple StepTypes" ] }, + { + "cell_type": "markdown", + "id": "d7a26b56-e0c7-4e35-a064-5899aa2ef6b7", + "metadata": {}, + "source": [ + "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 idential to `FiboStep` except two additional constraints for \"a\" and \"b\":\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", + "| ... | ... || ... |||| ... |||\n", + "\n", + "The following shows the incremental code of `FiboFirstStep` compared to `FiboStep`:\n", + "\n", + "```\n", + "class FiboFirstStep(StepType):\n", + " def setup(self):\n", + " # ...\n", + " self.constr(eq(self.circuit.a, 1))\n", + " self.constr(eq(self.circuit.b, 1))\n", + "\n", + " def wg(self, args):\n", + " # ...\n", + "```\n", + "\n", + "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:\n", + "\n", + "```\n", + "class Fibonacci(Circuit):\n", + " def setup(self):\n", + " # ...\n", + " self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n", + " self.pragma_first_step(self.fibo_first_step)\n", + " \n", + " def trace(self, args):\n", + " # TODO\n", + "```\n", + "\n", + "Finally, in circuit `trace`, we need to instantiate `FiboFirstStep` for the first step instance. Otherwise `trace` is identical to that in Chapter 3:\n", + "\n", + "```\n", + "class Fibonacci(Circuit):\n", + " def setup(self):\n", + " # ...\n", + " \n", + " def trace(self, args):\n", + " self.add(self.fibo_first_step, (1, 1))\n", + " # ...\n", + "```\n", + "\n", + "Putting everything together, we have the following circuit with two step types:" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "id": "10ce06ce-1345-4c00-9265-d59cb93a8014", + "metadata": {}, + "outputs": [], + "source": [ + "from dsl import Circuit, StepType\n", + "from cb import eq\n", + "from util import F\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", + "\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 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_first_step = self.step_type(FiboFirstStep(self, \"fibo_first_step\"))\n", + " self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n", + " self.pragma_num_steps(4)\n", + " self.pragma_first_step(self.fibo_first_step)\n", + " \n", + " def trace(self, args):\n", + " self.add(self.fibo_first_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": "5571eca6-af48-419f-8a87-2c472b3f246f", + "metadata": {}, + "source": [ + "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`." + ] + }, { "cell_type": "code", - "execution_count": 7, - "id": "bb11d921-5785-4c25-bab8-07df4a049cec", + "execution_count": 4, + "id": "5a615f38-417f-4928-bc24-5578bc5d92f3", "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "there's last step\n", - "4\n", - "1\n", - "23084509758196191005326514439957645834\n", - "Ok(\n", - " (),\n", - ")\n", "Err(\n", " [\n", " ConstraintCaseDebug {\n", @@ -34,8 +156,8 @@ " index: 0,\n", " name: \"main\",\n", " },\n", - " index: 3,\n", - " name: \"fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", + " index: 0,\n", + " name: \"fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", " },\n", " location: InRegion {\n", " region: Region 0 ('circuit'),\n", @@ -59,7 +181,7 @@ " name: \"\",\n", " column: DebugColumn {\n", " column_type: Advice,\n", - " index: 4,\n", + " index: 3,\n", " annotation: \"'step selector for fibo_first_step'\",\n", " },\n", " rotation: 0,\n", @@ -86,8 +208,8 @@ " index: 0,\n", " name: \"main\",\n", " },\n", - " index: 4,\n", - " name: \"fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", + " index: 1,\n", + " name: \"fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", " },\n", " location: InRegion {\n", " region: Region 0 ('circuit'),\n", @@ -111,7 +233,7 @@ " name: \"\",\n", " column: DebugColumn {\n", " column_type: Advice,\n", - " index: 4,\n", + " index: 3,\n", " annotation: \"'step selector for fibo_first_step'\",\n", " },\n", " rotation: 0,\n", @@ -134,90 +256,35 @@ " },\n", " ],\n", ")\n", - "Constraint 3 ('fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "Constraint 0 ('fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", "- Column('Advice', 0 - srcm forward a)@0 = 0\n", - "- Column('Advice', 4 - 'step selector for fibo_first_step')@0 = 1\n", + "- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1\n", "- Column('Fixed', 0 - q_enable)@0 = 1\n", "\n", - "Constraint 4 ('fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "Constraint 1 ('fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", "- Column('Advice', 1 - srcm forward b)@0 = 0x2bd7f2a3058aaa39904c1bc95d70baba121deb53c223d90fb8b7400adb62329c\n", - "- Column('Advice', 4 - 'step selector for fibo_first_step')@0 = 1\n", + "- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1\n", "- Column('Fixed', 0 - q_enable)@0 = 1\n", "\n" ] } ], "source": [ - "from dsl import Circuit, StepType\n", - "from cb import eq\n", - "from util import F\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", - "\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 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_first_step = self.step_type(FiboFirstStep(self, \"fibo_first_step\"))\n", - " self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n", - " self.pragma_num_steps(4)\n", - " self.pragma_first_step(self.fibo_first_step)\n", - " \n", - " def trace(self, args):\n", - " self.add(self.fibo_first_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", - "\n", - "# success\n", - "fibo_witness = fibo.gen_witness(None)\n", - "fibo.halo2_mock_prover(fibo_witness)\n", - "\n", - "# fails\n", "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)])\n", "fibo.halo2_mock_prover(evil_witness)" ] }, { - "cell_type": "code", - "execution_count": null, - "id": "f9d65edb-99ee-44fa-ae20-f0bad93269ee", + "cell_type": "markdown", + "id": "10ba5900-2619-4c87-8351-1cbdc8f5628b", "metadata": {}, - "outputs": [], - "source": [] + "source": [ + "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. \n", + "\n", + "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.\n", + "\n", + "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 \"softwares\" that are compatible with the hardware." + ] } ], "metadata": { diff --git a/pychiquito/tutorial_pt3_ch5.ipynb b/pychiquito/tutorial_pt3_ch5.ipynb index 067d270..76c6ce2 100644 --- a/pychiquito/tutorial_pt3_ch5.ipynb +++ b/pychiquito/tutorial_pt3_ch5.ipynb @@ -6,196 +6,186 @@ "metadata": {}, "source": [ "# Part 3: Fibonacci Example\n", - "# Chapter 5: Padding" + "# 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 softwares, 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", + "```\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", + "```\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", + "```\n", + "class Fibonacci(Circuit):\n", + " def setup(self):\n", + " self.a = self.forward(\"a\")\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", + "```\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": 2, + "execution_count": 1, "id": "525c00f0-210f-4328-85a6-eac0beeb3124", "metadata": {}, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "there's last step\n", - "100\n", - "1\n", - "243437734546730727453508299613593537034\n", - "Err(\n", - " [\n", - " ConstraintCaseDebug {\n", - " constraint: Constraint {\n", - " gate: Gate {\n", - " index: 0,\n", - " name: \"main\",\n", - " },\n", - " index: 1,\n", - " name: \"fibo_step::(b == next(a)) => (b + -next(a)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Fixed { query_index: 1, column_index: 2, 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(Advice { query_index: 4, column_index: 0, rotation: Rotation(1) })))))\",\n", - " },\n", - " location: InRegion {\n", - " region: Region 0 ('circuit'),\n", - " offset: 29,\n", - " },\n", - " cell_values: [\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Advice,\n", - " index: 0,\n", - " annotation: \"srcm forward a\",\n", - " },\n", - " rotation: 1,\n", - " },\n", - " \"0x2b44d974a1c0ffa0e68289e4a08a5d135c0c499d8c12a99d91dac7b8d6e66fda\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Advice,\n", - " index: 1,\n", - " annotation: \"srcm forward b\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"0x1c267c4330ad83827a0855880da9c6005115d28a51dc050bc18f2e2fd395960b\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Advice,\n", - " index: 3,\n", - " annotation: \"'step selector for fibo_step'\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"1\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Fixed,\n", - " index: 0,\n", - " annotation: \"q_enable\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"1\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Fixed,\n", - " index: 2,\n", - " annotation: \"q_last\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"0\",\n", - " ),\n", - " ],\n", - " },\n", - " ConstraintCaseDebug {\n", - " constraint: Constraint {\n", - " gate: Gate {\n", - " index: 0,\n", - " name: \"main\",\n", - " },\n", - " index: 2,\n", - " name: \"fibo_step::(c == next(b)) => (c + -next(b)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Fixed { query_index: 1, column_index: 2, rotation: Rotation(0) })), Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 3, column_index: 2, rotation: Rotation(0) }, Negated(Advice { query_index: 5, column_index: 1, rotation: Rotation(1) })))))\",\n", - " },\n", - " location: InRegion {\n", - " region: Region 0 ('circuit'),\n", - " offset: 29,\n", - " },\n", - " cell_values: [\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Advice,\n", - " index: 1,\n", - " annotation: \"srcm forward b\",\n", - " },\n", - " rotation: 1,\n", - " },\n", - " \"0\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Advice,\n", - " index: 2,\n", - " annotation: \"srcm internal signal c\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"0x17070744f13ce2f9a83a99b62cb2cab684ee33df64353e180f880054ba7c05e4\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Advice,\n", - " index: 3,\n", - " annotation: \"'step selector for fibo_step'\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"1\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Fixed,\n", - " index: 0,\n", - " annotation: \"q_enable\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"1\",\n", - " ),\n", - " (\n", - " DebugVirtualCell {\n", - " name: \"\",\n", - " column: DebugColumn {\n", - " column_type: Fixed,\n", - " index: 2,\n", - " annotation: \"q_last\",\n", - " },\n", - " rotation: 0,\n", - " },\n", - " \"0\",\n", - " ),\n", - " ],\n", - " },\n", - " ],\n", - ")\n", - "Constraint 1 ('fibo_step::(b == next(a)) => (b + -next(a)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Fixed { query_index: 1, column_index: 2, 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(Advice { query_index: 4, column_index: 0, rotation: Rotation(1) })))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 29\n", - "- Column('Advice', 0 - srcm forward a)@1 = 0x2b44d974a1c0ffa0e68289e4a08a5d135c0c499d8c12a99d91dac7b8d6e66fda\n", - "- Column('Advice', 1 - srcm forward b)@0 = 0x1c267c4330ad83827a0855880da9c6005115d28a51dc050bc18f2e2fd395960b\n", - "- Column('Advice', 3 - 'step selector for fibo_step')@0 = 1\n", - "- Column('Fixed', 0 - q_enable)@0 = 1\n", - "- Column('Fixed', 2 - q_last)@0 = 0\n", - "\n", - "Constraint 2 ('fibo_step::(c == next(b)) => (c + -next(b)) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Fixed { query_index: 1, column_index: 2, rotation: Rotation(0) })), Product(Advice { query_index: 0, column_index: 3, rotation: Rotation(0) }, Sum(Advice { query_index: 3, column_index: 2, rotation: Rotation(0) }, Negated(Advice { query_index: 5, column_index: 1, rotation: Rotation(1) })))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 29\n", - "- Column('Advice', 1 - srcm forward b)@1 = 0\n", - "- Column('Advice', 2 - srcm internal signal c)@0 = 0x17070744f13ce2f9a83a99b62cb2cab684ee33df64353e180f880054ba7c05e4\n", - "- Column('Advice', 3 - 'step selector for fibo_step')@0 = 1\n", - "- Column('Fixed', 0 - q_enable)@0 = 1\n", - "- Column('Fixed', 2 - q_last)@0 = 0\n", - "\n" - ] - } - ], + "outputs": [], "source": [ "from dsl import Circuit, StepType\n", "from cb import eq\n", @@ -210,12 +200,14 @@ " 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 = 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", @@ -223,60 +215,242 @@ " 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 = 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, b_value):\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", - "\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(100)\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.a, Last())\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", + " 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", + " 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, prev_a)\n", - "\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=57986403194690670908975341018702023178,\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=57986625825827335993858997128859879946,\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=57986625825827335993858997128859879946,\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=57986625825827335993858997128859879946,\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=57986625825827335993858997128859879946,\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=57986625825827335993858997128859879946,\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=57986625825827335993858997128859879946,\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=57986707430834725686872345692435253770,\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=57986707430834725686872345692435253770,\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=57986707430834725686872345692435253770,\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(30)\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": [ + "there's last step\n", + "10\n", + "1\n", + "58992563621385446294927224019566070282\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": null, - "id": "496c8617-8a8b-47a6-a6b7-c5a3a9ec8733", + "execution_count": 4, + "id": "3039a36e-30f0-4a81-b1a3-e22ffe1ce39f", "metadata": {}, - "outputs": [], - "source": [] + "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": { diff --git a/src/chiquito b/src/chiquito index 4866c8f..6494658 160000 --- a/src/chiquito +++ b/src/chiquito @@ -1 +1 @@ -Subproject commit 4866c8f7bded04cfa7c3a21607fb28183d2230ab +Subproject commit 6494658e89da7ad2a33bb55fe46817e9c1c8db6d From 3879e24ac9ec31b30daf4684ea85072cad63adda Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Thu, 17 Aug 2023 09:45:48 +0800 Subject: [PATCH 04/11] updated rust bindings and formatted python files --- pychiquito/dsl.py | 6 ++--- pychiquito/fibonacci.py | 12 +++++++--- pychiquito/tutorial_pt3_ch2.ipynb | 40 +++++++++++++++---------------- pychiquito/tutorial_pt3_ch3.ipynb | 23 ++++++++---------- pychiquito/tutorial_pt3_ch4.ipynb | 37 ++++++++++++++++++---------- pychiquito/tutorial_pt3_ch5.ipynb | 25 +++++++++---------- src/chiquito | 2 +- src/lib.rs | 11 ++++++++- 8 files changed, 88 insertions(+), 68 deletions(-) diff --git a/pychiquito/dsl.py b/pychiquito/dsl.py index 59f922d..0e0bd73 100644 --- a/pychiquito/dsl.py +++ b/pychiquito/dsl.py @@ -88,12 +88,12 @@ def add(self: Circuit, step_type: StepType, args: Any): self.num_step_instances += 1 step_instance: StepInstance = step_type.gen_step_instance(args) self.witness.step_instances.append(step_instance) - + def needs_padding(self: Circuit) -> bool: return self.num_step_instances < self.ast.num_steps - + def padding(self: Circuit, step_type: StepType, args: Any): - while(self.needs_padding()): + while self.needs_padding(): self.add(step_type, args) def gen_witness(self: Circuit, args: Any) -> TraceWitness: diff --git a/pychiquito/fibonacci.py b/pychiquito/fibonacci.py index 0d69542..e220529 100644 --- a/pychiquito/fibonacci.py +++ b/pychiquito/fibonacci.py @@ -2,6 +2,8 @@ from cb import eq from util import F from chiquito_ast import Last +import rust_chiquito + class FiboFirstStep(StepType): def setup(self): @@ -20,6 +22,7 @@ def wg(self, args): 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") @@ -35,6 +38,7 @@ def wg(self, args): 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())) @@ -46,12 +50,13 @@ def wg(self, args): 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")) @@ -62,7 +67,7 @@ def setup(self): 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 @@ -72,9 +77,10 @@ def trace(self, n): prev_a = a a = b b += prev_a - while(self.needs_padding()): + while self.needs_padding(): self.add(self.padding, (a, b, n)) + fibo = Fibonacci() fibo_witness = fibo.gen_witness(7) fibo.halo2_mock_prover(fibo_witness) diff --git a/pychiquito/tutorial_pt3_ch2.ipynb b/pychiquito/tutorial_pt3_ch2.ipynb index d9db81a..b994a8d 100644 --- a/pychiquito/tutorial_pt3_ch2.ipynb +++ b/pychiquito/tutorial_pt3_ch2.ipynb @@ -167,7 +167,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 2, "id": "d7c21e5d-5a9c-47b8-8c18-ed59fe885709", "metadata": {}, "outputs": [], @@ -215,7 +215,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 3, "id": "c0c9db95-8da8-49d6-a403-895491c833fe", "metadata": {}, "outputs": [], @@ -233,7 +233,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 4, "id": "d259b3b8-a15c-416c-9076-24c06f5b22e6", "metadata": {}, "outputs": [ @@ -243,11 +243,11 @@ "text": [ "ASTCircuit(\n", "\tstep_types={\n", - "\t\t257330087498007521101900253648606857738: ASTStepType(\n", - "\t\t\tid=257330087498007521101900253648606857738,\n", + "\t\t263045834685725738101873136979667454474: ASTStepType(\n", + "\t\t\tid=263045834685725738101873136979667454474,\n", "\t\t\tname='fibo_step',\n", "\t\t\tsignals=[\n", - "\t\t\t\tInternalSignal(id=257330145334566156513039079911908313610, annotation='c')\n", + "\t\t\t\tInternalSignal(id=263045899652818999796921973527026469386, annotation='c')\n", "\t\t\t],\n", "\t\t\tconstraints=[\n", "\t\t\t\tConstraint(\n", @@ -260,21 +260,21 @@ "\t\t\t\tTransitionConstraint((c == next(b)))\n", "\t\t\t],\n", "\t\t\tannotations={\n", - "\t\t\t\t257330145334566156513039079911908313610: c\n", + "\t\t\t\t263045899652818999796921973527026469386: c\n", "\t\t\t}\n", "\t\t)\n", "\t},\n", "\tforward_signals=[\n", - "\t\tForwardSignal(id=257329883089348234298700045805266012682, phase=0, annotation='a'),\n", - "\t\tForwardSignal(id=257330063729558766821948768389220141578, phase=0, annotation='b')\n", + "\t\tForwardSignal(id=263045762588097850118931419227795098122, phase=0, annotation='a'),\n", + "\t\tForwardSignal(id=263045810917276983821371649615788116490, phase=0, annotation='b')\n", "\t],\n", "\tshared_signals=[],\n", "\tfixed_signals=[],\n", "\texposed=[],\n", "\tannotations={\n", - "\t\t257329883089348234298700045805266012682: a,\n", - "\t\t257330063729558766821948768389220141578: b,\n", - "\t\t257330087498007521101900253648606857738: fibo_step\n", + "\t\t263045762588097850118931419227795098122: a,\n", + "\t\t263045810917276983821371649615788116490: b,\n", + "\t\t263045834685725738101873136979667454474: fibo_step\n", "\t},\n", "\tfixed_gen=None,\n", "\tfirst_step=None,\n", @@ -299,7 +299,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 5, "id": "24a0d3d8-710e-42fe-99ae-7491b50d7cd7", "metadata": {}, "outputs": [], @@ -317,7 +317,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 6, "id": "d1aaca8a-35eb-4c9d-8794-56869f696849", "metadata": {}, "outputs": [ @@ -328,7 +328,7 @@ "TraceWitness(\n", "\tstep_instances={\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=257330087498007521101900253648606857738,\n", + "\t\t\tstep_type_uuid=263045834685725738101873136979667454474,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 1,\n", @@ -336,7 +336,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=257330087498007521101900253648606857738,\n", + "\t\t\tstep_type_uuid=263045834685725738101873136979667454474,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 2,\n", @@ -344,7 +344,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=257330087498007521101900253648606857738,\n", + "\t\t\tstep_type_uuid=263045834685725738101873136979667454474,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 3,\n", @@ -352,7 +352,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=257330087498007521101900253648606857738,\n", + "\t\t\tstep_type_uuid=263045834685725738101873136979667454474,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 3,\n", "\t\t\t\tb = 5,\n", @@ -378,7 +378,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 7, "id": "a3f8d245-adab-4e68-9ee6-5f6bafc12bd1", "metadata": {}, "outputs": [ @@ -386,7 +386,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "260415491222404396048804715742414637578\n", + "266610265349471482662161864321976109578\n", "Ok(\n", " (),\n", ")\n" diff --git a/pychiquito/tutorial_pt3_ch3.ipynb b/pychiquito/tutorial_pt3_ch3.ipynb index 7dd091a..cdb62c6 100644 --- a/pychiquito/tutorial_pt3_ch3.ipynb +++ b/pychiquito/tutorial_pt3_ch3.ipynb @@ -23,7 +23,7 @@ }, { "cell_type": "code", - "execution_count": 29, + "execution_count": 1, "id": "e0114f48-0fe6-4141-b29e-63bc07411092", "metadata": {}, "outputs": [ @@ -31,10 +31,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "there's last step\n", - "4\n", - "1\n", - "194893930440567836774815565731016083978\n", + "277786757227377212257160741090518239754\n", "Ok(\n", " (),\n", ")\n" @@ -92,7 +89,7 @@ }, { "cell_type": "code", - "execution_count": 30, + "execution_count": 2, "id": "4e1481de-fa95-4022-9771-66aae4fe842c", "metadata": {}, "outputs": [], @@ -121,7 +118,7 @@ }, { "cell_type": "code", - "execution_count": 31, + "execution_count": 3, "id": "77168c22-aaea-4890-89ba-b3b3cf37c86d", "metadata": {}, "outputs": [], @@ -139,7 +136,7 @@ }, { "cell_type": "code", - "execution_count": 32, + "execution_count": 4, "id": "dcd26089-ecb0-4a5e-8296-318a7b644b98", "metadata": {}, "outputs": [ @@ -150,7 +147,7 @@ "TraceWitness(\n", "\tstep_instances={\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=194891702544637935660060827380995459594,\n", + "\t\t\tstep_type_uuid=277786217683590490113731286578468882954,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 0,\n", "\t\t\t\tb = 2,\n", @@ -158,7 +155,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=194891702544637935660060827380995459594,\n", + "\t\t\tstep_type_uuid=277786217683590490113731286578468882954,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 2,\n", @@ -166,7 +163,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=194891702544637935660060827380995459594,\n", + "\t\t\tstep_type_uuid=277786217683590490113731286578468882954,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 4,\n", @@ -174,7 +171,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=194891702544637935660060827380995459594,\n", + "\t\t\tstep_type_uuid=277786217683590490113731286578468882954,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 4,\n", "\t\t\t\tb = 6,\n", @@ -200,7 +197,7 @@ }, { "cell_type": "code", - "execution_count": 33, + "execution_count": 5, "id": "044e067e-77fa-4027-94dd-e39a35e87de8", "metadata": {}, "outputs": [ diff --git a/pychiquito/tutorial_pt3_ch4.ipynb b/pychiquito/tutorial_pt3_ch4.ipynb index 8340e1c..4bc3bea 100644 --- a/pychiquito/tutorial_pt3_ch4.ipynb +++ b/pychiquito/tutorial_pt3_ch4.ipynb @@ -68,10 +68,21 @@ }, { "cell_type": "code", - "execution_count": null, + "execution_count": 1, "id": "10ce06ce-1345-4c00-9265-d59cb93a8014", "metadata": {}, - "outputs": [], + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "311144493459252589786446983247350598154\n", + "Ok(\n", + " (),\n", + ")\n" + ] + } + ], "source": [ "from dsl import Circuit, StepType\n", "from cb import eq\n", @@ -140,7 +151,7 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 2, "id": "5a615f38-417f-4928-bc24-5578bc5d92f3", "metadata": {}, "outputs": [ @@ -156,8 +167,8 @@ " index: 0,\n", " name: \"main\",\n", " },\n", - " index: 0,\n", - " name: \"fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", + " index: 3,\n", + " name: \"fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", " },\n", " location: InRegion {\n", " region: Region 0 ('circuit'),\n", @@ -181,7 +192,7 @@ " name: \"\",\n", " column: DebugColumn {\n", " column_type: Advice,\n", - " index: 3,\n", + " index: 4,\n", " annotation: \"'step selector for fibo_first_step'\",\n", " },\n", " rotation: 0,\n", @@ -208,8 +219,8 @@ " index: 0,\n", " name: \"main\",\n", " },\n", - " index: 1,\n", - " name: \"fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", + " index: 4,\n", + " name: \"fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", " },\n", " location: InRegion {\n", " region: Region 0 ('circuit'),\n", @@ -233,7 +244,7 @@ " name: \"\",\n", " column: DebugColumn {\n", " column_type: Advice,\n", - " index: 3,\n", + " index: 4,\n", " annotation: \"'step selector for fibo_first_step'\",\n", " },\n", " rotation: 0,\n", @@ -256,14 +267,14 @@ " },\n", " ],\n", ")\n", - "Constraint 0 ('fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "Constraint 3 ('fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", "- Column('Advice', 0 - srcm forward a)@0 = 0\n", - "- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1\n", + "- Column('Advice', 4 - 'step selector for fibo_first_step')@0 = 1\n", "- Column('Fixed', 0 - q_enable)@0 = 1\n", "\n", - "Constraint 1 ('fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "Constraint 4 ('fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", "- Column('Advice', 1 - srcm forward b)@0 = 0x2bd7f2a3058aaa39904c1bc95d70baba121deb53c223d90fb8b7400adb62329c\n", - "- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1\n", + "- Column('Advice', 4 - 'step selector for fibo_first_step')@0 = 1\n", "- Column('Fixed', 0 - q_enable)@0 = 1\n", "\n" ] diff --git a/pychiquito/tutorial_pt3_ch5.ipynb b/pychiquito/tutorial_pt3_ch5.ipynb index 76c6ce2..e7d3f04 100644 --- a/pychiquito/tutorial_pt3_ch5.ipynb +++ b/pychiquito/tutorial_pt3_ch5.ipynb @@ -286,7 +286,7 @@ "TraceWitness(\n", "\tstep_instances={\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986403194690670908975341018702023178,\n", + "\t\t\tstep_type_uuid=320823874132656277603294324471666182666,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 1,\n", @@ -295,7 +295,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986625825827335993858997128859879946,\n", + "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 2,\n", @@ -304,7 +304,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986625825827335993858997128859879946,\n", + "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 3,\n", @@ -313,7 +313,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986625825827335993858997128859879946,\n", + "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 3,\n", "\t\t\t\tb = 5,\n", @@ -322,7 +322,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986625825827335993858997128859879946,\n", + "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 5,\n", "\t\t\t\tb = 8,\n", @@ -331,7 +331,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986625825827335993858997128859879946,\n", + "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 8,\n", "\t\t\t\tb = 13,\n", @@ -340,7 +340,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986625825827335993858997128859879946,\n", + "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 13,\n", "\t\t\t\tb = 21,\n", @@ -349,7 +349,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986707430834725686872345692435253770,\n", + "\t\t\tstep_type_uuid=320824157769478078669332145708066277898,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 21,\n", "\t\t\t\tb = 34,\n", @@ -357,7 +357,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986707430834725686872345692435253770,\n", + "\t\t\tstep_type_uuid=320824157769478078669332145708066277898,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 21,\n", "\t\t\t\tb = 34,\n", @@ -365,7 +365,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=57986707430834725686872345692435253770,\n", + "\t\t\tstep_type_uuid=320824157769478078669332145708066277898,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 21,\n", "\t\t\t\tb = 34,\n", @@ -401,10 +401,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "there's last step\n", - "10\n", - "1\n", - "58992563621385446294927224019566070282\n", + "322089641479461542938288310451956222474\n", "Ok(\n", " (),\n", ")\n" diff --git a/src/chiquito b/src/chiquito index 6494658..882aee9 160000 --- a/src/chiquito +++ b/src/chiquito @@ -1 +1 @@ -Subproject commit 6494658e89da7ad2a33bb55fe46817e9c1c8db6d +Subproject commit 882aee97e8dbf6b0350b1c5ce802c690caced966 diff --git a/src/lib.rs b/src/lib.rs index 5e5aa07..7b6e115 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,6 +1,6 @@ use chiquito::{ ast::Circuit, - frontend::pychiquito::{chiquito_ast_to_halo2, chiquito_halo2_mock_prover}, + frontend::pychiquito::{chiquito_ast_to_halo2, chiquito_halo2_mock_prover, chiquito_print_plaf_witness}, wit_gen::TraceWitness, }; use halo2_proofs::halo2curves::bn256::Fr; @@ -40,11 +40,20 @@ fn halo2_mock_prover(witness_json: &PyString, ast_uuid: &PyLong) { ); } +#[pyfunction] +fn print_plaf_witness(witness_json: &PyString, ast_uuid: &PyLong) { + chiquito_print_plaf_witness( + witness_json.to_str().expect("PyString convertion failed."), + ast_uuid.extract().expect("PyLong convertion failed."), + ); +} + #[pymodule] fn rust_chiquito(_py: Python, m: &PyModule) -> PyResult<()> { m.add_function(wrap_pyfunction!(convert_and_print_ast, m)?)?; m.add_function(wrap_pyfunction!(convert_and_print_trace_witness, m)?)?; m.add_function(wrap_pyfunction!(ast_to_halo2, m)?)?; m.add_function(wrap_pyfunction!(halo2_mock_prover, m)?)?; + m.add_function(wrap_pyfunction!(print_plaf_witness, m)?)?; Ok(()) } From f63f42892acbd1a57c206c5487ba79ee778318e3 Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Thu, 17 Aug 2023 09:46:10 +0800 Subject: [PATCH 05/11] minor --- pychiquito/fibonacci.py | 1 - 1 file changed, 1 deletion(-) diff --git a/pychiquito/fibonacci.py b/pychiquito/fibonacci.py index e220529..73983c6 100644 --- a/pychiquito/fibonacci.py +++ b/pychiquito/fibonacci.py @@ -2,7 +2,6 @@ from cb import eq from util import F from chiquito_ast import Last -import rust_chiquito class FiboFirstStep(StepType): From 9f058ea02e2ab0dc2aa6ce2aa39954d2eafb0e40 Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Thu, 17 Aug 2023 10:01:43 +0800 Subject: [PATCH 06/11] updated submodule --- src/chiquito | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/chiquito b/src/chiquito index 882aee9..66adae5 160000 --- a/src/chiquito +++ b/src/chiquito @@ -1 +1 @@ -Subproject commit 882aee97e8dbf6b0350b1c5ce802c690caced966 +Subproject commit 66adae5aedad3307fc2d46c37ea4f8585ffe0405 From f56ec2724019e8573975aab2909c476f7b99ca81 Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Thu, 17 Aug 2023 10:02:58 +0800 Subject: [PATCH 07/11] cargo fmt --- src/lib.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/lib.rs b/src/lib.rs index 7b6e115..06877ec 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,6 +1,8 @@ use chiquito::{ ast::Circuit, - frontend::pychiquito::{chiquito_ast_to_halo2, chiquito_halo2_mock_prover, chiquito_print_plaf_witness}, + frontend::pychiquito::{ + chiquito_ast_to_halo2, chiquito_halo2_mock_prover, chiquito_print_plaf_witness, + }, wit_gen::TraceWitness, }; use halo2_proofs::halo2curves::bn256::Fr; From 06c898c9326b69cea54f27a0f11af16f9661646f Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Thu, 17 Aug 2023 10:40:12 +0800 Subject: [PATCH 08/11] cleaned latest merge main; debugged and updated all tutorial files --- examples/fibonacci.py | 106 ++++++++++-------- examples/simple.py | 19 ---- examples/tutorial_pt2.ipynb | 5 +- examples/tutorial_pt3_ch2.ipynb | 30 ++--- examples/tutorial_pt3_ch3.ipynb | 16 +-- .../tutorial_pt3_ch4.ipynb | 28 ++--- .../tutorial_pt3_ch5.ipynb | 30 ++--- python/chiquito/chiquito_ast.py | 5 +- python/chiquito/dsl.py | 7 +- python/chiquito/wit_gen.py | 2 +- 10 files changed, 119 insertions(+), 129 deletions(-) delete mode 100644 examples/simple.py rename {python/chiquito => examples}/tutorial_pt3_ch4.ipynb (93%) rename {python/chiquito => examples}/tutorial_pt3_ch5.ipynb (95%) diff --git a/examples/fibonacci.py b/examples/fibonacci.py index 9274733..5d90614 100644 --- a/examples/fibonacci.py +++ b/examples/fibonacci.py @@ -1,73 +1,85 @@ -from __future__ import annotations -from typing import Tuple - -# from chiquito import (dsl, cb, query, util) -# from dsl import Circuit, StepType -# from cb import eq -# from query import Queriable -# from util import F - from chiquito.dsl import Circuit, StepType from chiquito.cb import eq -from chiquito.query import Queriable from chiquito.util import F +from chiquito.chiquito_ast import Last -class Fibonacci(Circuit): - def setup(self: Fibonacci): - self.a: Queriable = self.forward("a") - self.b: Queriable = self.forward("b") - - self.fibo_step = self.step_type(FiboStep(self, "fibo_step")) - self.fibo_last_step = self.step_type(FiboLastStep(self, "fibo_last_step")) - - self.pragma_first_step(self.fibo_step) - self.pragma_last_step(self.fibo_last_step) - self.pragma_num_steps(11) - # self.pragma_disable_q_enable() - - # self.expose(self.b, First()) - # self.expose(self.a, Last()) - # self.expose(self.a, Step(1)) +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 trace(self: Fibonacci, args: Any): - self.add(self.fibo_step, (1, 1)) - a = 1 - b = 2 - for i in range(1, 10): - self.add(self.fibo_step, (a, b)) - prev_a = a - a = b - b += prev_a - self.add(self.fibo_last_step, (a, b)) + 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: FiboStep): + 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: FiboStep, args: Tuple[int, int]): - a_value, b_value = args + 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 FiboLastStep(StepType): - def setup(self: FiboLastStep): - self.c = self.internal("c") - self.constr(eq(self.circuit.a + self.circuit.b, self.c)) +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: FiboLastStep, values=Tuple[int, int]): - a_value, b_value = values + 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 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)) fibo = Fibonacci() -fibo_witness = fibo.gen_witness(None) +fibo_witness = fibo.gen_witness(7) fibo.halo2_mock_prover(fibo_witness) diff --git a/examples/simple.py b/examples/simple.py deleted file mode 100644 index 6a10b14..0000000 --- a/examples/simple.py +++ /dev/null @@ -1,19 +0,0 @@ -from __future__ import annotations -from typing import Tuple - -from chiquito.dsl import Circuit, StepType -from chiquito.cb import eq -from chiquito.query import Queriable -from chiquito.util import F -import chiquito -# from chiquito import chiquito - - -# def main(): -print("Hello, world!") -# print(Circuit) -# print(StepType) -# print(eq) -# print(Queriable) -# print(chiquito.__all__) -print(dir(chiquito)) \ No newline at end of file diff --git a/examples/tutorial_pt2.ipynb b/examples/tutorial_pt2.ipynb index d76ea96..d2b04a1 100644 --- a/examples/tutorial_pt2.ipynb +++ b/examples/tutorial_pt2.ipynb @@ -8,15 +8,14 @@ "# Part 2: Quick Start\n", "PyChiquito requires using a Python virtual environment for its dependencies, which you should have setup following the [PyChiquito README](https://github.com/qwang98/PyChiquito#readme).\n", "\n", - "Specifically, after cloning PyChiquito, you need to run the following commands in your local repo (NOT in this Jupyter Notebook), till you see `(.env)` at the start of your command line, which means that you've successfully enabled the virtual environment. You also need to install `maturin` and `py_ecc` dependencies to your local environment and build the project using `maturin develop`. Again, these are all done in your local command line.\n", + "Specifically, after cloning PyChiquito, you need to run the following commands in your local repo (NOT in this Jupyter Notebook), till you see `(.env)` at the start of your command line, which means that you've successfully enabled the virtual environment. You also need to install required dependencies to your local environment and build the project using `maturin develop`. Again, these are all done in your local command line.\n", "\n", "```\n", "python3 -m venv .env\n", "\n", "source .env/bin/activate\n", "\n", - "pip install maturin\n", - "pip install py_ecc\n", + "pip install -r requirements.txt\n", "\n", "maturin develop\n", "```\n", diff --git a/examples/tutorial_pt3_ch2.ipynb b/examples/tutorial_pt3_ch2.ipynb index f5cc43d..4110317 100644 --- a/examples/tutorial_pt3_ch2.ipynb +++ b/examples/tutorial_pt3_ch2.ipynb @@ -243,11 +243,11 @@ "text": [ "ASTCircuit(\n", "\tstep_types={\n", - "\t\t263045834685725738101873136979667454474: ASTStepType(\n", - "\t\t\tid=263045834685725738101873136979667454474,\n", + "\t\t142788599383371455194542612232465418762: ASTStepType(\n", + "\t\t\tid=142788599383371455194542612232465418762,\n", "\t\t\tname='fibo_step',\n", "\t\t\tsignals=[\n", - "\t\t\t\tInternalSignal(id=263045899652818999796921973527026469386, annotation='c')\n", + "\t\t\t\tInternalSignal(id=142788636620607836899675527199131830794, annotation='c')\n", "\t\t\t],\n", "\t\t\tconstraints=[\n", "\t\t\t\tConstraint(\n", @@ -260,21 +260,21 @@ "\t\t\t\tTransitionConstraint((c == next(b)))\n", "\t\t\t],\n", "\t\t\tannotations={\n", - "\t\t\t\t263045899652818999796921973527026469386: c\n", + "\t\t\t\t142788636620607836899675527199131830794: c\n", "\t\t\t}\n", "\t\t)\n", "\t},\n", "\tforward_signals=[\n", - "\t\tForwardSignal(id=263045762588097850118931419227795098122, phase=0, annotation='a'),\n", - "\t\tForwardSignal(id=263045810917276983821371649615788116490, phase=0, annotation='b')\n", + "\t\tForwardSignal(id=142788527285743567215743361712843786762, phase=0, annotation='a'),\n", + "\t\tForwardSignal(id=142788567692106449489348851195099875850, phase=0, annotation='b')\n", "\t],\n", "\tshared_signals=[],\n", "\tfixed_signals=[],\n", "\texposed=[],\n", "\tannotations={\n", - "\t\t263045762588097850118931419227795098122: a,\n", - "\t\t263045810917276983821371649615788116490: b,\n", - "\t\t263045834685725738101873136979667454474: fibo_step\n", + "\t\t142788527285743567215743361712843786762: a,\n", + "\t\t142788567692106449489348851195099875850: b,\n", + "\t\t142788599383371455194542612232465418762: fibo_step\n", "\t},\n", "\tfixed_gen=None,\n", "\tfirst_step=None,\n", @@ -328,7 +328,7 @@ "TraceWitness(\n", "\tstep_instances={\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=263045834685725738101873136979667454474,\n", + "\t\t\tstep_type_uuid=142788599383371455194542612232465418762,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 1,\n", @@ -336,7 +336,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=263045834685725738101873136979667454474,\n", + "\t\t\tstep_type_uuid=142788599383371455194542612232465418762,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 2,\n", @@ -344,7 +344,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=263045834685725738101873136979667454474,\n", + "\t\t\tstep_type_uuid=142788599383371455194542612232465418762,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 3,\n", @@ -352,7 +352,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=263045834685725738101873136979667454474,\n", + "\t\t\tstep_type_uuid=142788599383371455194542612232465418762,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 3,\n", "\t\t\t\tb = 5,\n", @@ -386,7 +386,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "266610265349471482662161864321976109578\n", + "145806696406867587164175801408658475530\n", "Ok(\n", " (),\n", ")\n" @@ -410,7 +410,7 @@ ], "metadata": { "kernelspec": { - "display_name": ".env", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, diff --git a/examples/tutorial_pt3_ch3.ipynb b/examples/tutorial_pt3_ch3.ipynb index cdb62c6..dfa914d 100644 --- a/examples/tutorial_pt3_ch3.ipynb +++ b/examples/tutorial_pt3_ch3.ipynb @@ -31,7 +31,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "277786757227377212257160741090518239754\n", + "167511621523169244061366759362598144522\n", "Ok(\n", " (),\n", ")\n" @@ -39,9 +39,9 @@ } ], "source": [ - "from dsl import Circuit, StepType\n", - "from cb import eq\n", - "from util import F\n", + "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", @@ -147,7 +147,7 @@ "TraceWitness(\n", "\tstep_instances={\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=277786217683590490113731286578468882954,\n", + "\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 0,\n", "\t\t\t\tb = 2,\n", @@ -155,7 +155,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=277786217683590490113731286578468882954,\n", + "\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 2,\n", @@ -163,7 +163,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=277786217683590490113731286578468882954,\n", + "\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 4,\n", @@ -171,7 +171,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=277786217683590490113731286578468882954,\n", + "\t\t\tstep_type_uuid=167510131241432350748376109967127218698,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 4,\n", "\t\t\t\tb = 6,\n", diff --git a/python/chiquito/tutorial_pt3_ch4.ipynb b/examples/tutorial_pt3_ch4.ipynb similarity index 93% rename from python/chiquito/tutorial_pt3_ch4.ipynb rename to examples/tutorial_pt3_ch4.ipynb index 4bc3bea..36b6d82 100644 --- a/python/chiquito/tutorial_pt3_ch4.ipynb +++ b/examples/tutorial_pt3_ch4.ipynb @@ -76,7 +76,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "311144493459252589786446983247350598154\n", + "186650748934699451528647048735450860042\n", "Ok(\n", " (),\n", ")\n" @@ -84,9 +84,9 @@ } ], "source": [ - "from dsl import Circuit, StepType\n", - "from cb import eq\n", - "from util import F\n", + "from chiquito.dsl import Circuit, StepType\n", + "from chiquito.cb import eq\n", + "from chiquito.util import F\n", "\n", "class FiboFirstStep(StepType):\n", " def setup(self):\n", @@ -167,8 +167,8 @@ " index: 0,\n", " name: \"main\",\n", " },\n", - " index: 3,\n", - " name: \"fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", + " index: 0,\n", + " name: \"fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", " },\n", " location: InRegion {\n", " region: Region 0 ('circuit'),\n", @@ -192,7 +192,7 @@ " name: \"\",\n", " column: DebugColumn {\n", " column_type: Advice,\n", - " index: 4,\n", + " index: 3,\n", " annotation: \"'step selector for fibo_first_step'\",\n", " },\n", " rotation: 0,\n", @@ -219,8 +219,8 @@ " index: 0,\n", " name: \"main\",\n", " },\n", - " index: 4,\n", - " name: \"fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", + " index: 1,\n", + " name: \"fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))\",\n", " },\n", " location: InRegion {\n", " region: Region 0 ('circuit'),\n", @@ -244,7 +244,7 @@ " name: \"\",\n", " column: DebugColumn {\n", " column_type: Advice,\n", - " index: 4,\n", + " index: 3,\n", " annotation: \"'step selector for fibo_first_step'\",\n", " },\n", " rotation: 0,\n", @@ -267,14 +267,14 @@ " },\n", " ],\n", ")\n", - "Constraint 3 ('fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 1, column_index: 0, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "Constraint 0 ('fibo_first_step::(a == 1) => (a + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", "- Column('Advice', 0 - srcm forward a)@0 = 0\n", - "- Column('Advice', 4 - 'step selector for fibo_first_step')@0 = 1\n", + "- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1\n", "- Column('Fixed', 0 - q_enable)@0 = 1\n", "\n", - "Constraint 4 ('fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => Product(Fixed { query_index: 0, column_index: 0, rotation: Rotation(0) }, Product(Advice { query_index: 6, column_index: 4, rotation: Rotation(0) }, Sum(Advice { query_index: 2, column_index: 1, rotation: Rotation(0) }, Negated(Constant(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", + "Constraint 1 ('fibo_first_step::(b == 1) => (b + -0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e) => 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(0x15ebf95182c5551cc8260de4aeb85d5d090ef5a9e111ec87dc5ba0056db1194e)))))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n", "- Column('Advice', 1 - srcm forward b)@0 = 0x2bd7f2a3058aaa39904c1bc95d70baba121deb53c223d90fb8b7400adb62329c\n", - "- Column('Advice', 4 - 'step selector for fibo_first_step')@0 = 1\n", + "- Column('Advice', 3 - 'step selector for fibo_first_step')@0 = 1\n", "- Column('Fixed', 0 - q_enable)@0 = 1\n", "\n" ] diff --git a/python/chiquito/tutorial_pt3_ch5.ipynb b/examples/tutorial_pt3_ch5.ipynb similarity index 95% rename from python/chiquito/tutorial_pt3_ch5.ipynb rename to examples/tutorial_pt3_ch5.ipynb index e7d3f04..90d110a 100644 --- a/python/chiquito/tutorial_pt3_ch5.ipynb +++ b/examples/tutorial_pt3_ch5.ipynb @@ -187,10 +187,10 @@ "metadata": {}, "outputs": [], "source": [ - "from dsl import Circuit, StepType\n", - "from cb import eq\n", - "from util import F\n", - "from chiquito_ast import Last\n", + "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", @@ -286,7 +286,7 @@ "TraceWitness(\n", "\tstep_instances={\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320823874132656277603294324471666182666,\n", + "\t\t\tstep_type_uuid=218549979944188879026240919924757891594,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 1,\n", @@ -295,7 +295,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", + "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 1,\n", "\t\t\t\tb = 2,\n", @@ -304,7 +304,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", + "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 2,\n", "\t\t\t\tb = 3,\n", @@ -313,7 +313,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", + "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 3,\n", "\t\t\t\tb = 5,\n", @@ -322,7 +322,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", + "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 5,\n", "\t\t\t\tb = 8,\n", @@ -331,7 +331,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", + "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 8,\n", "\t\t\t\tb = 13,\n", @@ -340,7 +340,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320824088048695066117534437046594701834,\n", + "\t\t\tstep_type_uuid=218550191483382792109835797068016912906,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 13,\n", "\t\t\t\tb = 21,\n", @@ -349,7 +349,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320824157769478078669332145708066277898,\n", + "\t\t\tstep_type_uuid=218550284180332933799493868957742008842,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 21,\n", "\t\t\t\tb = 34,\n", @@ -357,7 +357,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320824157769478078669332145708066277898,\n", + "\t\t\tstep_type_uuid=218550284180332933799493868957742008842,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 21,\n", "\t\t\t\tb = 34,\n", @@ -365,7 +365,7 @@ "\t\t\t},\n", "\t\t),\n", "\t\tStepInstance(\n", - "\t\t\tstep_type_uuid=320824157769478078669332145708066277898,\n", + "\t\t\tstep_type_uuid=218550284180332933799493868957742008842,\n", "\t\t\tassignments={\n", "\t\t\t\ta = 21,\n", "\t\t\t\tb = 34,\n", @@ -401,7 +401,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "322089641479461542938288310451956222474\n", + "219491840378750327758403926198542010890\n", "Ok(\n", " (),\n", ")\n" diff --git a/python/chiquito/chiquito_ast.py b/python/chiquito/chiquito_ast.py index 1f4b28c..1fbbcf1 100644 --- a/python/chiquito/chiquito_ast.py +++ b/python/chiquito/chiquito_ast.py @@ -1,9 +1,8 @@ from __future__ import annotations -from typing import Callable, List, Dict, Optional, Any, Tuple +from typing import Callable, List, Dict, Optional, Tuple from dataclasses import dataclass, field, asdict -# from chiquito import wit_gen, expr, query, util -from chiquito.wit_gen import FixedGenContext, StepInstance +from chiquito.wit_gen import FixedGenContext from chiquito.expr import Expr from chiquito.util import uuid from chiquito.query import Queriable diff --git a/python/chiquito/dsl.py b/python/chiquito/dsl.py index 2d05c1a..e207e50 100644 --- a/python/chiquito/dsl.py +++ b/python/chiquito/dsl.py @@ -1,15 +1,14 @@ from __future__ import annotations from enum import Enum from typing import Callable, Any -from chiquito import rust_chiquito # rust bindings import json -from chiquito import (chiquito_ast, wit_gen) from chiquito.chiquito_ast import ASTCircuit, ASTStepType, ExposeOffset from chiquito.query import Internal, Forward, Queriable, Shared, Fixed from chiquito.wit_gen import FixedGenContext, StepInstance, TraceWitness from chiquito.cb import Constraint, Typing, ToConstraint, to_constraint from chiquito.util import CustomEncoder, F +from chiquito.rust_chiquito import ast_to_halo2, halo2_mock_prover class CircuitMode(Enum): @@ -113,9 +112,9 @@ def get_ast_json(self: Circuit) -> str: def halo2_mock_prover(self: Circuit, witness: TraceWitness): if self.rust_ast_id == 0: ast_json: str = self.get_ast_json() - self.rust_ast_id: int = rust_chiquito.ast_to_halo2(ast_json) + self.rust_ast_id: int = ast_to_halo2(ast_json) witness_json: str = witness.get_witness_json() - rust_chiquito.halo2_mock_prover(witness_json, self.rust_ast_id) + halo2_mock_prover(witness_json, self.rust_ast_id) def __str__(self: Circuit) -> str: return self.ast.__str__() diff --git a/python/chiquito/wit_gen.py b/python/chiquito/wit_gen.py index b740875..2b8af91 100644 --- a/python/chiquito/wit_gen.py +++ b/python/chiquito/wit_gen.py @@ -1,6 +1,6 @@ from __future__ import annotations from dataclasses import dataclass, field -from typing import Dict, List, Callable, Any +from typing import Dict, List import json from chiquito.query import Queriable, Fixed From 1be48e14956b898b8b819f1184796030638bfd28 Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Thu, 17 Aug 2023 10:49:41 +0800 Subject: [PATCH 09/11] addressed leo's comments' --- python/chiquito/dsl.py | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/python/chiquito/dsl.py b/python/chiquito/dsl.py index e207e50..e07780b 100644 --- a/python/chiquito/dsl.py +++ b/python/chiquito/dsl.py @@ -83,21 +83,19 @@ def pragma_disable_q_enable(self: Circuit) -> None: def add(self: Circuit, step_type: StepType, args: Any): assert self.mode == CircuitMode.Trace - if self.num_step_instances >= self.ast.num_steps: + if len(self.witness.step_instances) >= self.ast.num_steps: raise ValueError(f"Number of step instances exceeds {self.ast.num_steps}") - self.num_step_instances += 1 step_instance: StepInstance = step_type.gen_step_instance(args) self.witness.step_instances.append(step_instance) def needs_padding(self: Circuit) -> bool: - return self.num_step_instances < self.ast.num_steps + return len(self.witness.step_instances) < self.ast.num_steps def padding(self: Circuit, step_type: StepType, args: Any): while self.needs_padding(): self.add(step_type, args) def gen_witness(self: Circuit, args: Any) -> TraceWitness: - self.num_step_instances = 0 self.mode = CircuitMode.Trace self.witness = TraceWitness() self.trace(args) From 77cf0153412276f255a1436d87c3ef85d9e15932 Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Thu, 17 Aug 2023 12:44:45 +0800 Subject: [PATCH 10/11] removed num_step_instances --- python/chiquito/dsl.py | 1 - 1 file changed, 1 deletion(-) diff --git a/python/chiquito/dsl.py b/python/chiquito/dsl.py index e07780b..45be3ec 100644 --- a/python/chiquito/dsl.py +++ b/python/chiquito/dsl.py @@ -22,7 +22,6 @@ def __init__(self: Circuit): self.ast = ASTCircuit() self.witness = TraceWitness() self.rust_ast_id = 0 - self.num_step_instances = 0 self.mode = CircuitMode.SETUP self.setup() From 3b1f4f2aa9d1b3e21549fac975ff387090497a9c Mon Sep 17 00:00:00 2001 From: Steve Wang Date: Thu, 17 Aug 2023 17:15:41 +0800 Subject: [PATCH 11/11] updated dependencies and deleted unwanted functions --- src/chiquito | 2 +- src/lib.rs | 13 +------------ 2 files changed, 2 insertions(+), 13 deletions(-) diff --git a/src/chiquito b/src/chiquito index 66adae5..f6a4cb0 160000 --- a/src/chiquito +++ b/src/chiquito @@ -1 +1 @@ -Subproject commit 66adae5aedad3307fc2d46c37ea4f8585ffe0405 +Subproject commit f6a4cb0f494d24ad6251bd13ba0d4064a42539a0 diff --git a/src/lib.rs b/src/lib.rs index 06877ec..5e5aa07 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,8 +1,6 @@ use chiquito::{ ast::Circuit, - frontend::pychiquito::{ - chiquito_ast_to_halo2, chiquito_halo2_mock_prover, chiquito_print_plaf_witness, - }, + frontend::pychiquito::{chiquito_ast_to_halo2, chiquito_halo2_mock_prover}, wit_gen::TraceWitness, }; use halo2_proofs::halo2curves::bn256::Fr; @@ -42,20 +40,11 @@ fn halo2_mock_prover(witness_json: &PyString, ast_uuid: &PyLong) { ); } -#[pyfunction] -fn print_plaf_witness(witness_json: &PyString, ast_uuid: &PyLong) { - chiquito_print_plaf_witness( - witness_json.to_str().expect("PyString convertion failed."), - ast_uuid.extract().expect("PyLong convertion failed."), - ); -} - #[pymodule] fn rust_chiquito(_py: Python, m: &PyModule) -> PyResult<()> { m.add_function(wrap_pyfunction!(convert_and_print_ast, m)?)?; m.add_function(wrap_pyfunction!(convert_and_print_trace_witness, m)?)?; m.add_function(wrap_pyfunction!(ast_to_halo2, m)?)?; m.add_function(wrap_pyfunction!(halo2_mock_prover, m)?)?; - m.add_function(wrap_pyfunction!(print_plaf_witness, m)?)?; Ok(()) }