mirror of
https://github.com/qwang98/PyChiquito.git
synced 2026-04-22 03:00:16 -04:00
jupyter notebook tutorial
This commit is contained in:
Steve Wang
2
.gitignore
vendored
2
.gitignore
vendored
@@ -20,3 +20,5 @@ packages.png
|
||||
.env
|
||||
.vscode
|
||||
.devcontainer
|
||||
.ipynb_checkpoints
|
||||
dsl-ipynb_checkpoints
|
||||
@@ -83,7 +83,7 @@ class ASTCircuit:
|
||||
)
|
||||
|
||||
return (
|
||||
f"ASTCircuit(\n"
|
||||
f"Circuit(\n"
|
||||
f"\tstep_types={{{step_types_str}}},\n"
|
||||
f"\tforward_signals=[{forward_signals_str}],\n"
|
||||
f"\tshared_signals=[{shared_signals_str}],\n"
|
||||
@@ -209,7 +209,7 @@ class ASTStepType:
|
||||
)
|
||||
|
||||
return (
|
||||
f"ASTStepType(\n"
|
||||
f"StepType(\n"
|
||||
f"\t\t\tid={self.id},\n"
|
||||
f"\t\t\tname='{self.name}',\n"
|
||||
f"\t\t\tsignals=[{signals_str}],\n"
|
||||
|
||||
@@ -107,6 +107,9 @@ class Circuit:
|
||||
witness_json: str = witness.get_witness_json()
|
||||
rust_chiquito.verify_proof(witness_json, self.rust_ast_id)
|
||||
|
||||
def __str__(self: Circuit) -> str:
|
||||
return self.ast.__str__()
|
||||
|
||||
|
||||
class StepTypeMode(Enum):
|
||||
NoMode = 0
|
||||
|
||||
@@ -63,6 +63,7 @@ class FiboLastStep(StepType):
|
||||
|
||||
|
||||
fibo = Fibonacci()
|
||||
print(fibo)
|
||||
fibo_witness = fibo.gen_witness(None)
|
||||
fibo.ast_to_halo2()
|
||||
fibo.verify_proof(fibo_witness)
|
||||
|
||||
948
pychiquito/tutorial.ipynb
Normal file
948
pychiquito/tutorial.ipynb
Normal file
@@ -0,0 +1,948 @@
|
||||
{
|
||||
"cells": [
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "0d703199-2067-4ebc-b6ed-b04470587279",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"# Chapter 1: Introduction to PyChiquito\n",
|
||||
"Welcome to PyChiquito, a step-based high-level rust DSL (pychiquito is a python DSL for chiquito) that provides better syntax and abstraction for constraint building and column placement when writing PLONKish circuits, which supports custom gates and lookup arguments. PyChiquito has a Halo2 backend, which is a low level zkDSL that writes circuits using the PLONKish arithemtization. PyChiquito is working on supporting additional backends.\n",
|
||||
"\n",
|
||||
"PyChiquito is composed of two parts. [The Python part](https://github.com/qwang98/PyChiquito) exposes functions that user writes circuits with. [The Rust part](https://github.com/privacy-scaling-explorations/chiquito) is called by the Python functions behind the scenes and converts what the user writes into a Halo2 circuit.\n",
|
||||
"\n",
|
||||
"The key advantages of PyChiquito include: \n",
|
||||
"- Abstraction and simplification on the readability and learnability of Halo2 circuits.\n",
|
||||
"- Composabiity with other Halo2 circuits.\n",
|
||||
"- Modularity of using multiple frontends (Python and Rust) and backends (Halo2 and beyond).\n",
|
||||
"- Smooth user experience with a dynamically typed language (Python).\n",
|
||||
"\n",
|
||||
"For more on why you need PyChiquito, refer to the [Chiquito README](https://github.com/privacy-scaling-explorations/chiquito#readme) and the [Appendix](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#design-principles) on its design principles. For more on PLONKish concepts and Halo2 circuits, refer to the [Halo2 book](https://zcash.github.io/halo2/index.html).\n",
|
||||
"\n",
|
||||
"# Chapter 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."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "2234edbd-89fb-40bb-82f8-360ed6846765",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"# Create a virtual environment\n",
|
||||
"python3 -m venv .env\n",
|
||||
"\n",
|
||||
"# Activate the virtual environment\n",
|
||||
"source .env/bin/activate\n",
|
||||
"\n",
|
||||
"# Install the required packages\n",
|
||||
"pip install maturin\n",
|
||||
"pip install py_ecc\n",
|
||||
"\n",
|
||||
"# Build the project\n",
|
||||
"maturin develop"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "6f4b6361-2e5a-44bb-b98c-4aa5563e9e16",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Now, run the following in your local command line to navigate to the `PyChiquito/pychiquito` directory which contains all the Python files and activate Jupyter Lab. Finally, in the browser, navigate to `tutorial.ipynb` to start using this interactive tutorial."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "c0b9a7fd-ee1d-4e4f-bec3-a31c6fb386fb",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"# Navigate to the pychiquito Python directory\n",
|
||||
"cd pychiquito\n",
|
||||
"\n",
|
||||
"# If you haven't installed Jupyter Lab\n",
|
||||
"pip install jupyterlab\n",
|
||||
"\n",
|
||||
"# Activate Jupyter Lab\n",
|
||||
"jupyter lab"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "5ff73c57-3470-40e6-8b89-1a9ee83d3bb1",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Once in Jupyter Lab browser, make sure you are using the Python virtual environment rather than default for kernel."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "fa607d5d-7ce1-4162-b7a1-88a73c1a888e",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"# Chapter 3: Fibonacci Example–Part 1 (Do NOT run Chapter 3 code chunks)\n",
|
||||
"The best learning is by doing. We will now walk through the [fibonacci.py](https://github.com/qwang98/PyChiquito/blob/main/pychiquito/fibonacci.py) example with the following PLONKish table layout and three signals–a, b, and c.\n",
|
||||
"| a | b | c |\n",
|
||||
"| - | - | - |\n",
|
||||
"| 1 | 1 | 2 |\n",
|
||||
"| 1 | 2 | 3 |\n",
|
||||
"| 2 | 3 | 5 |\n",
|
||||
"| 3 | 5 | 8 |\n",
|
||||
"| ... | | |\n",
|
||||
"## Imports\n",
|
||||
"These imports are for the typing hints included in this example. Python is a dynamically typed interpreted language and typings aren't enforced."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "8b6ebe49-4952-43e5-86e0-3ec84bd93313",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"from __future__ import annotations\n",
|
||||
"from typing import Tuple"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "56e56385-8e08-4e39-b5a6-18c7e20022dd",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"The following imports are required, including:\n",
|
||||
"- `Circuit` and `StepType`, the most important data types, from the domain specific language (dsl).\n",
|
||||
"- Equal constraint `eq` from the constraint builder (cb).\n",
|
||||
"- `Queriable` type used to query signals.\n",
|
||||
"- Field element `F` from utils."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "ae3bac4e-c0e1-48c5-891f-f7286b5a05de",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"from dsl import Circuit, StepType\n",
|
||||
"from cb import eq\n",
|
||||
"from query import Queriable\n",
|
||||
"from util import F"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "39432fc0-ded0-47ff-bab3-16019f479ffd",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Circuit\n",
|
||||
"On the highest level, we are building a `Circuit` object in PyChiquito, that's why we start with creating a `Fibonacci` class that inherits the `Circuit` parent class. Within the `Fibonacci` class, we define two functions:\n",
|
||||
"- `setup`, which defines the circuit configuration using signals and step types (more on this later).\n",
|
||||
"- `trace`, which defines the circuit layout and the trace of assigning witness values."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "8d900fe0-df0a-410e-ba2a-5bfee679893e",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class Fibonacci(Circuit):\n",
|
||||
" def setup(self: Fibonacci):\n",
|
||||
" # TODO\n",
|
||||
"\n",
|
||||
" def trace(self: Fibonacci, args: Any):\n",
|
||||
" # TODO"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "38727b52-78fe-48ea-9f8f-91d664e2e981",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Circuit Setup\n",
|
||||
"We `setup` circuit configuration using signals and step types. \"Signals\" are variables we use to express custom constraints and lookup arguments. PyChiquito is a step-based language, for which we configure different \"step types\". Each step type defines different relationships among the signals. Each circuit is an arbitrary combination of arbitrary instances of step types. Think of the step types as different burger ingredients, such as bun, lettuce, and patties. Think of their instantiation as combining different amounts of ingredients to make the burger, such as 1 bun, 1 lettuce, 2 patties, and 1 bun. Think of the PyChiquito circuit as the burger you create. It's that simple!\n",
|
||||
"\n",
|
||||
"Now back to signals. Because we can assign different values to the same signal at different step instances, we can query the signal at different positions, and that's why signals are also called `Queriable` in PyChiquito. There are signals that live on the circuit top-level, called \"forward signals\", which we can query at different step instances. There are signals that live in a specific step type, called \"internal signals\".\n",
|
||||
"\n",
|
||||
"In the following example, we add two signals, \"a\" and \"b\", to the Fibonacci circuit. Here, signal definitions start with `self.a` and `self.b`, because we append them directly to the Circuit. Because they are circuit top-level signals rather than specific to a step-type, they are forward signals created using `self.forward`."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "efa3b548-4a6b-4334-8338-5f014b9f8778",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class Fibonacci(Circuit):\n",
|
||||
" def setup(self: Fibonacci):\n",
|
||||
" self.a: Queriable = self.forward(\"a\")\n",
|
||||
" self.b: Queriable = self.forward(\"b\")\n",
|
||||
" # TODO"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "255d7bbf-8913-45d9-807a-70930ed5a03a",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Now back to step types. In the Fibonacci cicuit, we consider each row a step instance. For example, in row 1, a=1 b=1 c=2. In row 2, a=1 b=2 c=3. Given the nature of Fibonacci, We want to enforce the constraint that b in the current step instance equals a in the next step instance and that c in the current step instance equals b in the next step instance. We created \"a\" and \"b\" as forward signals, because they are referred to across multiple step instances.\n",
|
||||
"\n",
|
||||
"We define two step types in the Fibonacci circuit, `fibo_step` and `fibo_last_step`, because the last step instance cannot enforce constraints that involve a signal in the next step instance, as there's no next step instance. More on the step type setup later. For now, we simply initiate and append them to the circuit using `self.step_type`."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "e36de184-19ca-4eff-b949-242fa5a4f933",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
" # ...\n",
|
||||
" self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
|
||||
" self.fibo_last_step = self.step_type(FiboLastStep(self, \"fibo_last_step\"))\n",
|
||||
" # TODO"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "dfcec095-cff1-41cc-8f44-676e51addf12",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Additionally, we need to constrain that the first step is indeed an instance of `fibo_step` and the last step an instance of `fibo_last_step`. We also want to enforce the total number of steps. See code below:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "d4c70884-474a-4262-a62a-6a368ca5e93a",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
" # ...\n",
|
||||
" self.pragma_first_step(self.fibo_step)\n",
|
||||
" self.pragma_last_step(self.fibo_last_step)\n",
|
||||
" self.pragma_num_steps(11)\n",
|
||||
" # TODO"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "618bf3c9-7e1d-452c-803b-4d0600f30f13",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"Putting the circuit `setup` together:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "0ca0472e-e048-40d3-8bea-dbd5f945dd2a",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class Fibonacci(Circuit):\n",
|
||||
" def setup(self: Fibonacci):\n",
|
||||
" self.a: Queriable = self.forward(\"a\")\n",
|
||||
" self.b: Queriable = self.forward(\"b\")\n",
|
||||
"\n",
|
||||
" self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
|
||||
" self.fibo_last_step = self.step_type(FiboLastStep(self, \"fibo_last_step\"))\n",
|
||||
"\n",
|
||||
" self.pragma_first_step(self.fibo_step)\n",
|
||||
" self.pragma_last_step(self.fibo_last_step)\n",
|
||||
" self.pragma_num_steps(11)\n",
|
||||
"\n",
|
||||
" def trace(self: Fibonacci, args: Any):\n",
|
||||
" # TODO"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "c47d0360-c3ea-4c01-9c09-f7e5eb76a77d",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## Circuit Trace\n",
|
||||
"Now we finished defining the ingredients (step types). Let's make the burger (combining step instances)!\n",
|
||||
"\n",
|
||||
"In `trace`, we define the circuit layout using step instances and a trace of witness value assignments. `trace` takes two arguments, the `Fibonacci` circuit itself and the witness value assignment arguments `args`.\n",
|
||||
"\n",
|
||||
"We call `self.add` to instantiate a specific step type we defined (`fibo_step` or `fibo_last_step`) 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. We didn't pass in witness values for \"c\", because they are only ever calculated.\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",
|
||||
"\n",
|
||||
"After creating the first `fibo_step` instance, we loop over `fibo_step` creation for 9 more times, each time calculating and passing in a different tuple of assignments. We close off the circuit with a `fibo_last_step` instance. Voila, here's our PyChiquito Fibonacci \"burger\" with 10 patties (`fibo_step`) and 1 bun (`fibo_last_step`)!"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "4e0f37a3-4ae7-42df-b5f1-b55f3179ac11",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class Fibonacci(Circuit):\n",
|
||||
" def setup(self: Fibonacci):\n",
|
||||
" # ...\n",
|
||||
" \n",
|
||||
" def trace(self: Fibonacci, args: Any):\n",
|
||||
" self.add(self.fibo_step, (1, 1))\n",
|
||||
" a = 1\n",
|
||||
" b = 2\n",
|
||||
" for i in range(1, 10):\n",
|
||||
" self.add(self.fibo_step, (a, b))\n",
|
||||
" prev_a = a\n",
|
||||
" a = b\n",
|
||||
" b += prev_a\n",
|
||||
" self.add(self.fibo_last_step, (a, b))"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "d0fdbf3a-3a7d-44d1-bafa-c90228550ce5",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"# Chapter 4: Fibonacci Example–Part 2 (Do NOT run Chapter 4 code chunks)\n",
|
||||
"Now that we have the Fibonacci circuit configured with signals and step types using `setup` and layout defined with step instances and witness assignments using `trace`, we move forward to configuring `fibo_step` and `fibo_last_step`.\n",
|
||||
"## StepType\n",
|
||||
"PyChiquito provides a `StepType` parent class that we can customarily inherit. Again, for each `StepType`, we define two functions:\n",
|
||||
"- `setup`, which defines the step type configuration using signals\n",
|
||||
"- `wg`, which defines witness assignment within the step type"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "f97bf512-1345-4bca-9619-8ece82dd9595",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class FiboStep(StepType):\n",
|
||||
" def setup(self: FiboStep):\n",
|
||||
" # TODO\n",
|
||||
"\n",
|
||||
" def wg(self: FiboStep, args: Tuple[int, int]):\n",
|
||||
" # TODO\n",
|
||||
"\n",
|
||||
"\n",
|
||||
"class FiboLastStep(StepType):\n",
|
||||
" def setup(self: FiboLastStep):\n",
|
||||
" # TODO\n",
|
||||
"\n",
|
||||
" def wg(self: FiboLastStep, values=Tuple[int, int]):\n",
|
||||
" # TODO"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "a9afed15-cffd-445f-9abc-f7922552a4ad",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## FiboStep Setup\n",
|
||||
"As each step instance contains three signals, only two of which we've defined so far, we define a third signal \"c\", whose relationship is only defined within the step type and therefore an internal signal created using `self.internal`.\n",
|
||||
"\n",
|
||||
"Next, we define constraints among signals, both forward and internal. There are two types of constraints in PyChiquito:\n",
|
||||
"- `constr` stands for constraints among signals that are specific to the step type, i.e. internal signals.\n",
|
||||
"- `transition` stands for constraints involving circuit-level signals, i.e. forward signals and etc.\n",
|
||||
"\n",
|
||||
"In the code snippet below, forward signals \"a\" and \"b\" are expressed as `self.circuit.a` and `self.circuit.b`, whereas internal signal \"c\" is expressed `self.c`, because \"a\" and \"b\" are at the circuit-level. `self.circuit.a.next()` queries the value of circuit-level signal \"a\" at the next step instance. `eq` is a constraint builder that enforces equality between the two arguments passed in. The following constraints are translated as:\n",
|
||||
"- a + b == c\n",
|
||||
"- b == value of a in next step instance\n",
|
||||
"- c = value of b in next step instance"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "ebc70e2d-c5ad-4f51-8eeb-497c5d193607",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class FiboStep(StepType):\n",
|
||||
" def setup(self: FiboStep):\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()))"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "95948d6e-c8c8-4ff0-8a41-6b94b9bf0ed6",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## FiboStep Witness Generation\n",
|
||||
"Similar to `trace`, `wg` (witness generation) defines witness value assignments at the step type level. Here, the `args` we pass in is a tuple of values for signals \"a\" and \"b\". We assign them to forward signals \"a\" and \"b\" and then their sum to internal signal \"c\". Note that the format of `args` in `wg` needs to match `args` in the `add` function called in `trace`, e.g. `(a, b)` in `self.add(self.fibo_step, (a, b))`. This is because `add` creates step instance by calling `wg` associated with the step type. Here in `wg`, we don't pass in any hardcoded values, because we need to make the function generic for `add` to use across different step instances.\n",
|
||||
"\n",
|
||||
"Finally, note that in `self.assign`, `a_value` and `b_value` are both wrapped in `F`, which converts them from int to field elements. All witness assignments in PyChiquito are field elements."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "c36560fc-5c82-4682-90d3-51c12f30d04b",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class FiboStep(StepType):\n",
|
||||
" def setup(self: FiboStep):\n",
|
||||
" # ...\n",
|
||||
"\n",
|
||||
" def wg(self: FiboStep, args: Tuple[int, int]):\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))"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "e5b8fe10-2fa5-4eb5-b438-74890d9d600a",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Putting everything for `FiboStep` together, we have:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "ca5e3661-ec6d-4cff-8c6f-dec8312f243d",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class FiboStep(StepType):\n",
|
||||
" def setup(self: FiboStep):\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: FiboStep, args: Tuple[int, int]):\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))"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "b11a5494-5c36-46e3-8fdb-e0f62278138b",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"## FiboLastStep Setup and Witness Generation\n",
|
||||
"`FiboLastStep` is identical except that we don't create transition constraints like \"b == a.next\", because there's no next step instance after the last."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": null,
|
||||
"id": "116b5269-6720-4b93-b43f-6e135f8d03ad",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"class FiboLastStep(StepType):\n",
|
||||
" def setup(self: FiboLastStep):\n",
|
||||
" self.c = self.internal(\"c\")\n",
|
||||
" self.constr(eq(self.circuit.a + self.circuit.b, self.c))\n",
|
||||
"\n",
|
||||
" def wg(self: FiboLastStep, values=Tuple[int, int]):\n",
|
||||
" a_value, b_value = values\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))"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "5df5b508-4895-4991-8689-246eb209ceb8",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"# Chapter 5: Fibonacci Example–Part 3 (Code chunks CAN be run)\n",
|
||||
"Putting everything together, let's run the `fibonacci.py` example:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 3,
|
||||
"id": "f7514278-e22a-4cba-8eab-0f0c956d5dc8",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"from __future__ import annotations\n",
|
||||
"from typing import Tuple\n",
|
||||
"\n",
|
||||
"from dsl import Circuit, StepType\n",
|
||||
"from cb import eq\n",
|
||||
"from query import Queriable\n",
|
||||
"from util import F\n",
|
||||
"\n",
|
||||
"\n",
|
||||
"class Fibonacci(Circuit):\n",
|
||||
" def setup(self: Fibonacci):\n",
|
||||
" self.a: Queriable = self.forward(\"a\")\n",
|
||||
" self.b: Queriable = self.forward(\"b\")\n",
|
||||
"\n",
|
||||
" self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n",
|
||||
" self.fibo_last_step = self.step_type(FiboLastStep(self, \"fibo_last_step\"))\n",
|
||||
"\n",
|
||||
" self.pragma_first_step(self.fibo_step)\n",
|
||||
" self.pragma_last_step(self.fibo_last_step)\n",
|
||||
" self.pragma_num_steps(11)\n",
|
||||
"\n",
|
||||
" def trace(self: Fibonacci, args: Any):\n",
|
||||
" self.add(self.fibo_step, (1, 1))\n",
|
||||
" a = 1\n",
|
||||
" b = 2\n",
|
||||
" for i in range(1, 10):\n",
|
||||
" self.add(self.fibo_step, (a, b))\n",
|
||||
" prev_a = a\n",
|
||||
" a = b\n",
|
||||
" b += prev_a\n",
|
||||
" self.add(self.fibo_last_step, (a, b))\n",
|
||||
"\n",
|
||||
"\n",
|
||||
"class FiboStep(StepType):\n",
|
||||
" def setup(self: FiboStep):\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: FiboStep, args: Tuple[int, int]):\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",
|
||||
"\n",
|
||||
"class FiboLastStep(StepType):\n",
|
||||
" def setup(self: FiboLastStep):\n",
|
||||
" self.c = self.internal(\"c\")\n",
|
||||
" self.constr(eq(self.circuit.a + self.circuit.b, self.c))\n",
|
||||
"\n",
|
||||
" def wg(self: FiboLastStep, values=Tuple[int, int]):\n",
|
||||
" a_value, b_value = values\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))"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "f4fbe5a7-5d21-486d-96a0-be7f3cc7afa8",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Everything we went through in the code chunk above defines how the circuit and its step types are configured and witness values assigned to them. To initiate the circuit, we call the class constructor:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 4,
|
||||
"id": "0d7abe66-d47b-4c54-9820-866afaa154d3",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"fibo = Fibonacci()"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "43a48d84-cd10-4365-889a-2a88756f6ca0",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"You can also print the circuit. In the print out, you will see the two step types and two forward signals \"a\" and \"b\" at the circuit top-level. Within each step type, you will see the internal signals and constraints. The big random looking numbers are UUIDs that we use to uniquely identify objects in the circuit, which you don't need to worry about."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 5,
|
||||
"id": "0b13121f-c6a9-4326-bef4-8f63d045a727",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"Circuit(\n",
|
||||
"\tstep_types={\n",
|
||||
"\t\t128256994632759118053530467296915098122: ASTStepType(\n",
|
||||
"\t\t\tid=128256994632759118053530467296915098122,\n",
|
||||
"\t\t\tname='fibo_step',\n",
|
||||
"\t\t\tsignals=[\n",
|
||||
"\t\t\t\tInternalSignal(id=128257112682721264306777895903334894090, annotation='c')\n",
|
||||
"\t\t\t],\n",
|
||||
"\t\t\tconstraints=[\n",
|
||||
"\t\t\t\tConstraint(\n",
|
||||
"\t\t\t\t\tannotation='((a + b) == c)',\n",
|
||||
"\t\t\t\t\texpr=(a + b - (-c))\n",
|
||||
"\t\t\t\t)\n",
|
||||
"\t\t\t],\n",
|
||||
"\t\t\ttransition_constraints=[\n",
|
||||
"\t\t\t\tTransitionConstraint((b == next(a))),\n",
|
||||
"\t\t\t\tTransitionConstraint((c == next(b)))\n",
|
||||
"\t\t\t],\n",
|
||||
"\t\t\tannotations={\n",
|
||||
"\t\t\t\t128257112682721264306777895903334894090: c\n",
|
||||
"\t\t\t}\n",
|
||||
"\t\t),\n",
|
||||
"\t\t128257260047103540840494676250559384074: ASTStepType(\n",
|
||||
"\t\t\tid=128257260047103540840494676250559384074,\n",
|
||||
"\t\t\tname='fibo_last_step',\n",
|
||||
"\t\t\tsignals=[\n",
|
||||
"\t\t\t\tInternalSignal(id=128257273515891168262993086479833106954, annotation='c')\n",
|
||||
"\t\t\t],\n",
|
||||
"\t\t\tconstraints=[\n",
|
||||
"\t\t\t\tConstraint(\n",
|
||||
"\t\t\t\t\tannotation='((a + b) == c)',\n",
|
||||
"\t\t\t\t\texpr=(a + b - (-c))\n",
|
||||
"\t\t\t\t)\n",
|
||||
"\t\t\t],\n",
|
||||
"\t\t\ttransition_constraints=[],\n",
|
||||
"\t\t\tannotations={\n",
|
||||
"\t\t\t\t128257273515891168262993086479833106954: c\n",
|
||||
"\t\t\t}\n",
|
||||
"\t\t)\n",
|
||||
"\t},\n",
|
||||
"\tforward_signals=[\n",
|
||||
"\t\tForwardSignal(id=128256819538519961529048555364261956106, phase=0, annotation='a'),\n",
|
||||
"\t\tForwardSignal(id=128256872621388846084146700554854861322, phase=0, annotation='b')\n",
|
||||
"\t],\n",
|
||||
"\tshared_signals=[],\n",
|
||||
"\tfixed_signals=[],\n",
|
||||
"\texposed=[],\n",
|
||||
"\tannotations={\n",
|
||||
"\t\t128256819538519961529048555364261956106: a,\n",
|
||||
"\t\t128256872621388846084146700554854861322: b,\n",
|
||||
"\t\t128256994632759118053530467296915098122: fibo_step,\n",
|
||||
"\t\t128257260047103540840494676250559384074: fibo_last_step\n",
|
||||
"\t},\n",
|
||||
"\tfixed_gen=None,\n",
|
||||
"\tfirst_step=128256994632759118053530467296915098122,\n",
|
||||
"\tlast_step=128257260047103540840494676250559384074,\n",
|
||||
"\tnum_steps=11\n",
|
||||
"\tq_enable=True\n",
|
||||
")\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"print(fibo)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "34999740-3aea-42bf-b9a2-9516f26e768c",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"After initiating the Fibonacci circuit, we can generate witness assignments for it. `gen_witness` takes one argument of external input with `Any` type. However, because the only external input, `(1, 1)`, was hardcoded in `trace`, we don't need to provide an additional one and can put `None` for this argument. In practice, one circuit can have many different sets of witness assignments, each generated by a different external input argument. This is why we expose the `gen_witness` function to you."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 6,
|
||||
"id": "7013cda1-3ace-40e0-99b7-240501ab981e",
|
||||
"metadata": {},
|
||||
"outputs": [],
|
||||
"source": [
|
||||
"fibo_witness = fibo.gen_witness(None)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "e5c3f1db-d3b7-43ca-90c1-efd626526297",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Again, you can print the witness assignments:"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 7,
|
||||
"id": "af232353-f420-4846-8c2d-aac4245f6da6",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"TraceWitness(\n",
|
||||
"\tstep_instances={\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\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},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\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},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\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},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\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},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\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},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\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},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\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},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\n",
|
||||
"\t\t\tassignments={\n",
|
||||
"\t\t\t\ta = 21,\n",
|
||||
"\t\t\t\tb = 34,\n",
|
||||
"\t\t\t\tc = 55\n",
|
||||
"\t\t\t},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\n",
|
||||
"\t\t\tassignments={\n",
|
||||
"\t\t\t\ta = 34,\n",
|
||||
"\t\t\t\tb = 55,\n",
|
||||
"\t\t\t\tc = 89\n",
|
||||
"\t\t\t},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128256994632759118053530467296915098122,\n",
|
||||
"\t\t\tassignments={\n",
|
||||
"\t\t\t\ta = 55,\n",
|
||||
"\t\t\t\tb = 89,\n",
|
||||
"\t\t\t\tc = 144\n",
|
||||
"\t\t\t},\n",
|
||||
"\t\t),\n",
|
||||
"\t\tStepInstance(\n",
|
||||
"\t\t\tstep_type_uuid=128257260047103540840494676250559384074,\n",
|
||||
"\t\t\tassignments={\n",
|
||||
"\t\t\t\ta = 89,\n",
|
||||
"\t\t\t\tb = 144,\n",
|
||||
"\t\t\t\tc = 233\n",
|
||||
"\t\t\t},\n",
|
||||
"\t\t)\n",
|
||||
"\t},\n",
|
||||
"\theight=0,\n",
|
||||
")\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"print(fibo_witness)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "f4e1dcda-744b-4574-aac3-02032d2f9501",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"We can convert and register the PyChiquito circuit as a Halo2 circuit in Rust Chiquito. `ast_to_halo2` function achieves this purpose and prints out the Halo2 circuit UUID generated for our PyChiquito circuit. You don't need to do anything with the UUID."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 9,
|
||||
"id": "cb3e4dd3-5ba8-4e14-98ba-b51a5d02f5d4",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"name": "stdout",
|
||||
"output_type": "stream",
|
||||
"text": [
|
||||
"155598347502771109092689974944871352842\n",
|
||||
"155598347502771109092689974944871352842\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"fibo.ast_to_halo2()"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "46cc251c-fbe5-4aad-84c4-3fd7c42fb2b7",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Finally, we can verify the proof with the witness. The print out includes Halo2 and Rust Chiquito debug messages. `Ok(())` means that proof was correctly generated and verified for the witness assignments and circuit. `Err()` prints out Halo2 and Rust Chiquito error messages, usually because some constraints in the circuit were not satisfied."
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "code",
|
||||
"execution_count": 11,
|
||||
"id": "13288d58-3272-4142-b69c-debd899a6d8c",
|
||||
"metadata": {},
|
||||
"outputs": [
|
||||
{
|
||||
"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: 4,\n",
|
||||
" name: \"q_first => Product(Fixed { query_index: 1, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 4, column_index: 4, 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: 4,\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",
|
||||
" ConstraintCaseDebug {\n",
|
||||
" constraint: Constraint {\n",
|
||||
" gate: Gate {\n",
|
||||
" index: 0,\n",
|
||||
" name: \"main\",\n",
|
||||
" },\n",
|
||||
" index: 5,\n",
|
||||
" name: \"q_last => Product(Fixed { query_index: 2, column_index: 2, 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: 10,\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_last_step'\",\n",
|
||||
" },\n",
|
||||
" rotation: 0,\n",
|
||||
" },\n",
|
||||
" \"0\",\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",
|
||||
" \"1\",\n",
|
||||
" ),\n",
|
||||
" ],\n",
|
||||
" },\n",
|
||||
" ],\n",
|
||||
")\n",
|
||||
"Constraint 4 ('q_first => Product(Fixed { query_index: 1, column_index: 1, rotation: Rotation(0) }, Sum(Constant(0x0000000000000000000000000000000000000000000000000000000000000001), Negated(Advice { query_index: 4, column_index: 4, rotation: Rotation(0) })))') in gate 0 ('main') is not satisfied in Region 0 ('circuit') at offset 0\n",
|
||||
"- Column('Advice', 4 - 'step selector for fibo_step')@0 = 0\n",
|
||||
"- Column('Fixed', 1 - q_first)@0 = 1\n",
|
||||
"\n",
|
||||
"Constraint 5 ('q_last => Product(Fixed { query_index: 2, column_index: 2, 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 10\n",
|
||||
"- Column('Advice', 3 - 'step selector for fibo_last_step')@0 = 0\n",
|
||||
"- Column('Fixed', 2 - q_last)@0 = 1\n",
|
||||
"\n"
|
||||
]
|
||||
}
|
||||
],
|
||||
"source": [
|
||||
"fibo.verify_proof(fibo_witness)"
|
||||
]
|
||||
},
|
||||
{
|
||||
"cell_type": "markdown",
|
||||
"id": "26a85381-1921-4599-9861-1e3d287ec24e",
|
||||
"metadata": {},
|
||||
"source": [
|
||||
"Congratulations! Now you finished writing your first Fibonacci circuit and learned about the most essential concepts behind the step-based design of PyChiquito, which is really as easy as bun-lettuce-patty-patty-bun, basically combining step instances to a PyChiquito burger! With abstraction, composability, modularity, and smooth user experience as the key tenets, writing Halo2 circuits has never been easier with PyChiquito!"
|
||||
]
|
||||
}
|
||||
],
|
||||
"metadata": {
|
||||
"kernelspec": {
|
||||
"display_name": "myenv",
|
||||
"language": "python",
|
||||
"name": "myenv"
|
||||
},
|
||||
"language_info": {
|
||||
"codemirror_mode": {
|
||||
"name": "ipython",
|
||||
"version": 3
|
||||
},
|
||||
"file_extension": ".py",
|
||||
"mimetype": "text/x-python",
|
||||
"name": "python",
|
||||
"nbconvert_exporter": "python",
|
||||
"pygments_lexer": "ipython3",
|
||||
"version": "3.11.4"
|
||||
}
|
||||
},
|
||||
"nbformat": 4,
|
||||
"nbformat_minor": 5
|
||||
}
|
||||
Reference in New Issue
Block a user