From 2472e4c3cf7ca6b8f39580ae08fb407cc87e8fd7 Mon Sep 17 00:00:00 2001 From: trangnv Date: Thu, 17 Aug 2023 11:37:15 +0700 Subject: [PATCH 1/7] frontend as maturin project --- frontend/python/.github/workflows/CI.yml | 120 +++++++++++++++++++++++ frontend/python/.gitignore | 72 ++++++++++++++ frontend/python/Cargo.toml | 13 +++ frontend/python/pyproject.toml | 16 +++ frontend/python/src/lib.rs | 14 +++ 5 files changed, 235 insertions(+) create mode 100644 frontend/python/.github/workflows/CI.yml create mode 100644 frontend/python/.gitignore create mode 100644 frontend/python/Cargo.toml create mode 100644 frontend/python/pyproject.toml create mode 100644 frontend/python/src/lib.rs diff --git a/frontend/python/.github/workflows/CI.yml b/frontend/python/.github/workflows/CI.yml new file mode 100644 index 00000000..8c6a5eaf --- /dev/null +++ b/frontend/python/.github/workflows/CI.yml @@ -0,0 +1,120 @@ +# This file is autogenerated by maturin v1.2.0 +# To update, run +# +# maturin generate-ci github +# +name: CI + +on: + push: + branches: + - main + - master + tags: + - '*' + pull_request: + workflow_dispatch: + +permissions: + contents: read + +jobs: + linux: + runs-on: ubuntu-latest + strategy: + matrix: + target: [x86_64, x86, aarch64, armv7, s390x, ppc64le] + steps: + - uses: actions/checkout@v3 + - uses: actions/setup-python@v4 + with: + python-version: '3.10' + - name: Build wheels + uses: PyO3/maturin-action@v1 + with: + target: ${{ matrix.target }} + args: --release --out dist --find-interpreter + sccache: 'true' + manylinux: auto + - name: Upload wheels + uses: actions/upload-artifact@v3 + with: + name: wheels + path: dist + + windows: + runs-on: windows-latest + strategy: + matrix: + target: [x64, x86] + steps: + - uses: actions/checkout@v3 + - uses: actions/setup-python@v4 + with: + python-version: '3.10' + architecture: ${{ matrix.target }} + - name: Build wheels + uses: PyO3/maturin-action@v1 + with: + target: ${{ matrix.target }} + args: --release --out dist --find-interpreter + sccache: 'true' + - name: Upload wheels + uses: actions/upload-artifact@v3 + with: + name: wheels + path: dist + + macos: + runs-on: macos-latest + strategy: + matrix: + target: [x86_64, aarch64] + steps: + - uses: actions/checkout@v3 + - uses: actions/setup-python@v4 + with: + python-version: '3.10' + - name: Build wheels + uses: PyO3/maturin-action@v1 + with: + target: ${{ matrix.target }} + args: --release --out dist --find-interpreter + sccache: 'true' + - name: Upload wheels + uses: actions/upload-artifact@v3 + with: + name: wheels + path: dist + + sdist: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v3 + - name: Build sdist + uses: PyO3/maturin-action@v1 + with: + command: sdist + args: --out dist + - name: Upload sdist + uses: actions/upload-artifact@v3 + with: + name: wheels + path: dist + + release: + name: Release + runs-on: ubuntu-latest + if: "startsWith(github.ref, 'refs/tags/')" + needs: [linux, windows, macos, sdist] + steps: + - uses: actions/download-artifact@v3 + with: + name: wheels + - name: Publish to PyPI + uses: PyO3/maturin-action@v1 + env: + MATURIN_PYPI_TOKEN: ${{ secrets.PYPI_API_TOKEN }} + with: + command: upload + args: --skip-existing * diff --git a/frontend/python/.gitignore b/frontend/python/.gitignore new file mode 100644 index 00000000..af3ca5ef --- /dev/null +++ b/frontend/python/.gitignore @@ -0,0 +1,72 @@ +/target + +# Byte-compiled / optimized / DLL files +__pycache__/ +.pytest_cache/ +*.py[cod] + +# C extensions +*.so + +# Distribution / packaging +.Python +.venv/ +env/ +bin/ +build/ +develop-eggs/ +dist/ +eggs/ +lib/ +lib64/ +parts/ +sdist/ +var/ +include/ +man/ +venv/ +*.egg-info/ +.installed.cfg +*.egg + +# Installer logs +pip-log.txt +pip-delete-this-directory.txt +pip-selfcheck.json + +# Unit test / coverage reports +htmlcov/ +.tox/ +.coverage +.cache +nosetests.xml +coverage.xml + +# Translations +*.mo + +# Mr Developer +.mr.developer.cfg +.project +.pydevproject + +# Rope +.ropeproject + +# Django stuff: +*.log +*.pot + +.DS_Store + +# Sphinx documentation +docs/_build/ + +# PyCharm +.idea/ + +# VSCode +.vscode/ + +# Pyenv +.python-version \ No newline at end of file diff --git a/frontend/python/Cargo.toml b/frontend/python/Cargo.toml new file mode 100644 index 00000000..67f0f075 --- /dev/null +++ b/frontend/python/Cargo.toml @@ -0,0 +1,13 @@ +[package] +name = "python" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html +[lib] +name = "python" +crate-type = ["cdylib"] + +[dependencies] +pyo3 = "0.19.0" +chiquito = { path = "../my_lib" } diff --git a/frontend/python/pyproject.toml b/frontend/python/pyproject.toml new file mode 100644 index 00000000..9bd5ee2b --- /dev/null +++ b/frontend/python/pyproject.toml @@ -0,0 +1,16 @@ +[build-system] +requires = ["maturin>=1.2,<2.0"] +build-backend = "maturin" + +[project] +name = "python" +requires-python = ">=3.7" +classifiers = [ + "Programming Language :: Rust", + "Programming Language :: Python :: Implementation :: CPython", + "Programming Language :: Python :: Implementation :: PyPy", +] + + +[tool.maturin] +features = ["pyo3/extension-module"] diff --git a/frontend/python/src/lib.rs b/frontend/python/src/lib.rs new file mode 100644 index 00000000..87838129 --- /dev/null +++ b/frontend/python/src/lib.rs @@ -0,0 +1,14 @@ +use pyo3::prelude::*; + +/// Formats the sum of two numbers as string. +#[pyfunction] +fn sum_as_string(a: usize, b: usize) -> PyResult { + Ok((a + b).to_string()) +} + +/// A Python module implemented in Rust. +#[pymodule] +fn python(_py: Python, m: &PyModule) -> PyResult<()> { + m.add_function(wrap_pyfunction!(sum_as_string, m)?)?; + Ok(()) +} \ No newline at end of file From 9c0fe1f6033ee0eb5192d69530ff0d1483ce75a7 Mon Sep 17 00:00:00 2001 From: trangnv Date: Thu, 17 Aug 2023 13:58:27 +0700 Subject: [PATCH 2/7] frontend/python/chiquito --- .gitignore | 3 + Cargo.toml | 7 +- examples/fibonacci.py | 62 +++ frontend/python/.github/workflows/CI.yml | 120 ------ frontend/python/.gitignore | 72 ---- frontend/python/Cargo.toml | 13 - frontend/python/chiquito/__init__.py | 0 frontend/python/chiquito/cb.py | 224 ++++++++++ frontend/python/chiquito/chiquito_ast.py | 386 ++++++++++++++++++ frontend/python/chiquito/dsl.py | 165 ++++++++ frontend/python/chiquito/expr.py | 157 +++++++ frontend/python/chiquito/query.py | 138 +++++++ frontend/python/chiquito/util.py | 31 ++ frontend/python/chiquito/wit_gen.py | 122 ++++++ frontend/python/src/lib.rs | 14 - .../python/pyproject.toml => pyproject.toml | 9 +- src/lib.rs | 1 + src/python.rs | 50 +++ 18 files changed, 1351 insertions(+), 223 deletions(-) create mode 100644 examples/fibonacci.py delete mode 100644 frontend/python/.github/workflows/CI.yml delete mode 100644 frontend/python/.gitignore delete mode 100644 frontend/python/Cargo.toml create mode 100644 frontend/python/chiquito/__init__.py create mode 100644 frontend/python/chiquito/cb.py create mode 100644 frontend/python/chiquito/chiquito_ast.py create mode 100644 frontend/python/chiquito/dsl.py create mode 100644 frontend/python/chiquito/expr.py create mode 100644 frontend/python/chiquito/query.py create mode 100644 frontend/python/chiquito/util.py create mode 100644 frontend/python/chiquito/wit_gen.py delete mode 100644 frontend/python/src/lib.rs rename frontend/python/pyproject.toml => pyproject.toml (65%) create mode 100644 src/python.rs diff --git a/.gitignore b/.gitignore index 5b70a898..b55d2a6f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,6 @@ /target /Cargo.lock .vscode +.env +__pycache__ +*.so \ No newline at end of file diff --git a/Cargo.toml b/Cargo.toml index 5265c2f4..fa4144a1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -8,10 +8,13 @@ authors = ["Leo Lara "] # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] +pyo3 = { version = "0.19.1", features = ["extension-module"] } halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", features = [ - "circuit-params", + "circuit-params", ], tag = "v2023_04_20" } -halo2curves = { git = 'https://github.com/privacy-scaling-explorations/halo2curves', tag = "0.3.2", features = [ "derive_serde" ] } +halo2curves = { git = 'https://github.com/privacy-scaling-explorations/halo2curves', tag = "0.3.2", features = [ + "derive_serde", +] } polyexen = { git = "https://github.com/Dhole/polyexen.git", rev = "67148a8aabb000a61a169b2533b2526c5b76c42f" } num-bigint = { version = "0.4", features = ["rand"] } uuid = { version = "1.4.0", features = ["v1", "rng"] } diff --git a/examples/fibonacci.py b/examples/fibonacci.py new file mode 100644 index 00000000..7fd7ee38 --- /dev/null +++ b/examples/fibonacci.py @@ -0,0 +1,62 @@ +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 + + +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) + + 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) diff --git a/frontend/python/.github/workflows/CI.yml b/frontend/python/.github/workflows/CI.yml deleted file mode 100644 index 8c6a5eaf..00000000 --- a/frontend/python/.github/workflows/CI.yml +++ /dev/null @@ -1,120 +0,0 @@ -# This file is autogenerated by maturin v1.2.0 -# To update, run -# -# maturin generate-ci github -# -name: CI - -on: - push: - branches: - - main - - master - tags: - - '*' - pull_request: - workflow_dispatch: - -permissions: - contents: read - -jobs: - linux: - runs-on: ubuntu-latest - strategy: - matrix: - target: [x86_64, x86, aarch64, armv7, s390x, ppc64le] - steps: - - uses: actions/checkout@v3 - - uses: actions/setup-python@v4 - with: - python-version: '3.10' - - name: Build wheels - uses: PyO3/maturin-action@v1 - with: - target: ${{ matrix.target }} - args: --release --out dist --find-interpreter - sccache: 'true' - manylinux: auto - - name: Upload wheels - uses: actions/upload-artifact@v3 - with: - name: wheels - path: dist - - windows: - runs-on: windows-latest - strategy: - matrix: - target: [x64, x86] - steps: - - uses: actions/checkout@v3 - - uses: actions/setup-python@v4 - with: - python-version: '3.10' - architecture: ${{ matrix.target }} - - name: Build wheels - uses: PyO3/maturin-action@v1 - with: - target: ${{ matrix.target }} - args: --release --out dist --find-interpreter - sccache: 'true' - - name: Upload wheels - uses: actions/upload-artifact@v3 - with: - name: wheels - path: dist - - macos: - runs-on: macos-latest - strategy: - matrix: - target: [x86_64, aarch64] - steps: - - uses: actions/checkout@v3 - - uses: actions/setup-python@v4 - with: - python-version: '3.10' - - name: Build wheels - uses: PyO3/maturin-action@v1 - with: - target: ${{ matrix.target }} - args: --release --out dist --find-interpreter - sccache: 'true' - - name: Upload wheels - uses: actions/upload-artifact@v3 - with: - name: wheels - path: dist - - sdist: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v3 - - name: Build sdist - uses: PyO3/maturin-action@v1 - with: - command: sdist - args: --out dist - - name: Upload sdist - uses: actions/upload-artifact@v3 - with: - name: wheels - path: dist - - release: - name: Release - runs-on: ubuntu-latest - if: "startsWith(github.ref, 'refs/tags/')" - needs: [linux, windows, macos, sdist] - steps: - - uses: actions/download-artifact@v3 - with: - name: wheels - - name: Publish to PyPI - uses: PyO3/maturin-action@v1 - env: - MATURIN_PYPI_TOKEN: ${{ secrets.PYPI_API_TOKEN }} - with: - command: upload - args: --skip-existing * diff --git a/frontend/python/.gitignore b/frontend/python/.gitignore deleted file mode 100644 index af3ca5ef..00000000 --- a/frontend/python/.gitignore +++ /dev/null @@ -1,72 +0,0 @@ -/target - -# Byte-compiled / optimized / DLL files -__pycache__/ -.pytest_cache/ -*.py[cod] - -# C extensions -*.so - -# Distribution / packaging -.Python -.venv/ -env/ -bin/ -build/ -develop-eggs/ -dist/ -eggs/ -lib/ -lib64/ -parts/ -sdist/ -var/ -include/ -man/ -venv/ -*.egg-info/ -.installed.cfg -*.egg - -# Installer logs -pip-log.txt -pip-delete-this-directory.txt -pip-selfcheck.json - -# Unit test / coverage reports -htmlcov/ -.tox/ -.coverage -.cache -nosetests.xml -coverage.xml - -# Translations -*.mo - -# Mr Developer -.mr.developer.cfg -.project -.pydevproject - -# Rope -.ropeproject - -# Django stuff: -*.log -*.pot - -.DS_Store - -# Sphinx documentation -docs/_build/ - -# PyCharm -.idea/ - -# VSCode -.vscode/ - -# Pyenv -.python-version \ No newline at end of file diff --git a/frontend/python/Cargo.toml b/frontend/python/Cargo.toml deleted file mode 100644 index 67f0f075..00000000 --- a/frontend/python/Cargo.toml +++ /dev/null @@ -1,13 +0,0 @@ -[package] -name = "python" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html -[lib] -name = "python" -crate-type = ["cdylib"] - -[dependencies] -pyo3 = "0.19.0" -chiquito = { path = "../my_lib" } diff --git a/frontend/python/chiquito/__init__.py b/frontend/python/chiquito/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/frontend/python/chiquito/cb.py b/frontend/python/chiquito/cb.py new file mode 100644 index 00000000..f6058b67 --- /dev/null +++ b/frontend/python/chiquito/cb.py @@ -0,0 +1,224 @@ +from __future__ import annotations +from dataclasses import dataclass +from enum import Enum, auto +from typing import List + +from chiquito.util import F +from chiquito.expr import Expr, Const, Neg, to_expr, ToExpr +from chiquito.query import StepTypeNext +from chiquito.chiquito_ast import ASTStepType + + +class Typing(Enum): + Unknown = auto() + Boolean = auto() + AntiBooly = auto() + + +@dataclass +class Constraint: + annotation: str + expr: Expr + typing: Typing + + def from_expr( + expr: Expr, + ) -> Constraint: # Cannot call function `from`, a reserved keyword in Python. + annotation: str = str(expr) + if isinstance(expr, StepTypeNext): + return Constraint(annotation, expr, Typing.Boolean) + else: + return Constraint(annotation, expr, Typing.Unknown) + + def __str__(self: Constraint) -> str: + return self.annotation + + +def cb_and( + inputs: List[ToConstraint], +) -> Constraint: # Cannot call function `and`, a reserved keyword in Python + inputs = [to_constraint(input) for input in inputs] + annotations: List[str] = [] + expr = Const(F(1)) + for constraint in inputs: + if constraint.typing == Typing.Boolean or constraint.typing == Typing.Unknown: + annotations.append(constraint.annotation) + expr = expr * constraint.expr + else: + raise ValueError( + f"Expected Boolean or Unknown constraint, got AntiBooly (constraint: {constraint.annotation})" + ) + return Constraint(f"({' AND '.join(annotations)})", expr, Typing.Boolean) + + +def cb_or( + inputs: List[ToConstraint], +) -> Constraint: # Cannot call function `or`, a reserved keyword in Python + inputs = [to_constraint(input) for input in inputs] + annotations: List[str] = [] + exprs: List[Expr] = [] + for constraint in inputs: + if constraint.typing == Typing.Boolean or constraint.typing == Typing.Unknown: + annotations.append(constraint.annotation) + exprs.append(constraint.expr) + else: + raise ValueError( + f"Expected Boolean or Unknown constraint, got AntiBooly (constraint: {constraint.annotation})" + ) + result: Constraint = Constraint.cb_not( + Constraint.cb_and([Constraint.cb_not(expr) for expr in exprs]) + ) + return Constraint(f"({' OR '.join(annotations)})", result.expr, Typing.Boolean) + + +def xor(lhs: ToConstraint, rhs: ToConstraint) -> Constraint: + (lhs, rhs) = (to_constraint(lhs), to_constraint(rhs)) + if (lhs.typing == Typing.Boolean or lhs.typing == Typing.Unknown) and ( + rhs.typing == Typing.Boolean or rhs.typing == Typing.Unknown + ): + return Constraint( + f"({lhs.annotation} XOR {rhs.annotation})", + lhs.expr + rhs.expr - F(2) * lhs.expr * rhs.expr, + Typing.Boolean, + ) + else: + raise ValueError( + f"Expected Boolean or Unknown constraints, got AntiBooly in one of lhs or rhs constraints (lhs constraint: {lhs.annotation}) (rhs constraint: {rhs.annotation})" + ) + + +def eq(lhs: ToConstraint, rhs: ToConstraint) -> Constraint: + (lhs, rhs) = (to_constraint(lhs), to_constraint(rhs)) + return Constraint( + f"({lhs.annotation} == {rhs.annotation})", + lhs.expr - rhs.expr, + Typing.AntiBooly, + ) + + +def select( + selector: ToConstraint, when_true: ToConstraint, when_false: ToConstraint +) -> Constraint: + (selector, when_true, when_false) = ( + to_constraint(selector), + to_constraint(when_true), + to_constraint(when_false), + ) + if selector.typing == Typing.AntiBooly: + raise ValueError( + f"Expected Boolean or Unknown selector, got AntiBooly (selector: {selector.annotation})" + ) + return Constraint( + f"if({selector.annotation})then({when_true.annotation})else({when_false.annotation})", + selector.expr * when_true.expr + (F(1) - selector.expr) * when_false.expr, + when_true.typing if when_true.typing == when_false.typing else Typing.Unknown, + ) + + +def when(selector: ToConstraint, when_true: ToConstraint) -> Constraint: + (selector, when_true) = (to_constraint(selector), to_constraint(when_true)) + if selector.typing == Typing.AntiBooly: + raise ValueError( + f"Expected Boolean or Unknown selector, got AntiBooly (selector: {selector.annotation})" + ) + return Constraint( + f"if({selector.annotation})then({when_true.annotation})", + selector.expr * when_true.expr, + when_true.typing, + ) + + +def unless(selector: ToConstraint, when_false: ToConstraint) -> Constraint: + (selector, when_false) = (to_constraint(selector), to_constraint(when_false)) + if selector.typing == Typing.AntiBooly: + raise ValueError( + f"Expected Boolean or Unknown selector, got AntiBooly (selector: {selector.annotation})" + ) + return Constraint( + f"unless({selector.annotation})then({when_false.annotation})", + (F(1) - selector.expr) * when_false.expr, + when_false.typing, + ) + + +def cb_not( + constraint: ToConstraint, +) -> Constraint: # Cannot call function `not`, a reserved keyword in Python + constraint = to_constraint(constraint) + if constraint.typing == Typing.AntiBooly: + raise ValueError( + f"Expected Boolean or Unknown constraint, got AntiBooly (constraint: {constraint.annotation})" + ) + return Constraint( + f"NOT({constraint.annotation})", F(1) - constraint.expr, Typing.Boolean + ) + + +def isz(constraint: ToConstraint) -> Constraint: + constraint = to_constraint(constraint) + return Constraint( + f"0 == {constraint.annotation}", constraint.expr, Typing.AntiBooly + ) + + +def if_next_step(step_type: ASTStepType, constraint: ToConstraint) -> Constraint: + constraint = to_constraint(constraint) + return Constraint( + f"if(next step is {step_type.annotation})then({constraint.annotation})", + StepTypeNext(step_type) * constraint.expr, + constraint.typing, + ) + + +def next_step_must_be(step_type: ASTStepType) -> Constraint: + return Constraint( + f"next step must be {step_type.annotation}", + Constraint.cb_not(StepTypeNext(step_type)), + Typing.AntiBooly, + ) + + +def next_step_must_not_be(step_type: ASTStepType) -> Constraint: + return Constraint( + f"next step must not be {step_type.annotation}", + StepTypeNext(step_type), + Typing.AntiBooly, + ) + + +def rlc(exprs: List[ToExpr], randomness: Expr) -> Expr: + if len(exprs) > 0: + exprs: List[Expr] = [to_expr(expr) for expr in exprs].reverse() + init: Expr = exprs[0] + for expr in exprs[1:]: + init = init * randomness + expr + return init + else: + return Expr(Const(F(0))) + + +# TODO: Implement lookup table after the lookup abstraction PR is merged. + + +ToConstraint = Constraint | Expr | int | F + + +def to_constraint(v: ToConstraint) -> Constraint: + if isinstance(v, Constraint): + return v + elif isinstance(v, Expr): + if isinstance(v, StepTypeNext): + return Constraint(str(v), v, Typing.Boolean) + else: + return Constraint(str(v), v, Typing.Unknown) + elif isinstance(v, int): + if v >= 0: + return to_constraint(Const(F(v))) + else: + return to_constraint(Neg(Const(F(-v)))) + elif isinstance(v, F): + return to_constraint(Const(v)) + else: + raise TypeError( + f"Type `{type(v)}` is not ToConstraint (one of Constraint, Expr, int, or F)." + ) diff --git a/frontend/python/chiquito/chiquito_ast.py b/frontend/python/chiquito/chiquito_ast.py new file mode 100644 index 00000000..1f4b28c2 --- /dev/null +++ b/frontend/python/chiquito/chiquito_ast.py @@ -0,0 +1,386 @@ +from __future__ import annotations +from typing import Callable, List, Dict, Optional, Any, Tuple +from dataclasses import dataclass, field, asdict +# from chiquito import wit_gen, expr, query, util + +from chiquito.wit_gen import FixedGenContext, StepInstance +from chiquito.expr import Expr +from chiquito.util import uuid +from chiquito.query import Queriable + + +# pub struct Circuit { +# pub step_types: HashMap>>, + +# pub forward_signals: Vec, +# pub shared_signals: Vec, +# pub fixed_signals: Vec, +# pub halo2_advice: Vec, +# pub halo2_fixed: Vec, +# pub exposed: Vec, + +# pub annotations: HashMap, + +# pub trace: Option>>, +# pub fixed_gen: Option>>, + +# pub first_step: Option, +# pub last_step: Option, +# pub num_steps: usize, +# } + + +@dataclass +class ASTCircuit: + step_types: Dict[int, ASTStepType] = field(default_factory=dict) + forward_signals: List[ForwardSignal] = field(default_factory=list) + shared_signals: List[SharedSignal] = field(default_factory=list) + fixed_signals: List[FixedSignal] = field(default_factory=list) + exposed: List[Tuple[Queriable, ExposeOffset]] = field(default_factory=list) + annotations: Dict[int, str] = field(default_factory=dict) + fixed_gen: Optional[Callable] = None + first_step: Optional[int] = None + last_step: Optional[int] = None + num_steps: int = 0 + q_enable: bool = True + id: int = uuid() + + def __str__(self: ASTCircuit): + step_types_str = ( + "\n\t\t" + + ",\n\t\t".join(f"{k}: {v}" for k, v in self.step_types.items()) + + "\n\t" + if self.step_types + else "" + ) + forward_signals_str = ( + "\n\t\t" + ",\n\t\t".join(str(fs) for fs in self.forward_signals) + "\n\t" + if self.forward_signals + else "" + ) + shared_signals_str = ( + "\n\t\t" + ",\n\t\t".join(str(ss) for ss in self.shared_signals) + "\n\t" + if self.shared_signals + else "" + ) + fixed_signals_str = ( + "\n\t\t" + ",\n\t\t".join(str(fs) for fs in self.fixed_signals) + "\n\t" + if self.fixed_signals + else "" + ) + exposed_str = ( + "\n\t\t" + + ",\n\t\t".join(f"({str(lhs)}, {str(rhs)})" for (lhs, rhs) in self.exposed) + + "\n\t" + if self.exposed + else "" + ) + annotations_str = ( + "\n\t\t" + + ",\n\t\t".join(f"{k}: {v}" for k, v in self.annotations.items()) + + "\n\t" + if self.annotations + else "" + ) + + return ( + f"ASTCircuit(\n" + f"\tstep_types={{{step_types_str}}},\n" + f"\tforward_signals=[{forward_signals_str}],\n" + f"\tshared_signals=[{shared_signals_str}],\n" + f"\tfixed_signals=[{fixed_signals_str}],\n" + f"\texposed=[{exposed_str}],\n" + f"\tannotations={{{annotations_str}}},\n" + f"\tfixed_gen={self.fixed_gen},\n" + f"\tfirst_step={self.first_step},\n" + f"\tlast_step={self.last_step},\n" + f"\tnum_steps={self.num_steps}\n" + f"\tq_enable={self.q_enable}\n" + f")" + ) + + def __json__(self: ASTCircuit): + return { + "step_types": {k: v.__json__() for k, v in self.step_types.items()}, + "forward_signals": [x.__json__() for x in self.forward_signals], + "shared_signals": [x.__json__() for x in self.shared_signals], + "fixed_signals": [x.__json__() for x in self.fixed_signals], + "exposed": [ + [queriable.__json__(), offset.__json__()] + for (queriable, offset) in self.exposed + ], + "annotations": self.annotations, + "first_step": self.first_step, + "last_step": self.last_step, + "num_steps": self.num_steps, + "q_enable": self.q_enable, + "id": self.id, + } + + def add_forward(self: ASTCircuit, name: str, phase: int) -> ForwardSignal: + signal = ForwardSignal(phase, name) + self.forward_signals.append(signal) + self.annotations[signal.id] = name + return signal + + def add_shared(self: ASTCircuit, name: str, phase: int) -> SharedSignal: + signal = SharedSignal(phase, name) + self.shared_signals.append(signal) + self.annotations[signal.id] = name + return signal + + def add_fixed(self: ASTCircuit, name: str) -> FixedSignal: + signal = FixedSignal(name) + self.fixed_signals.append(signal) + self.annotations[signal.id] = name + return signal + + def expose(self: ASTCircuit, signal: Queriable, offset: ExposeOffset): + self.exposed.append((signal, offset)) + + def add_step_type(self: ASTCircuit, step_type: ASTStepType, name: str): + self.annotations[step_type.id] = name + self.step_types[step_type.id] = step_type + + def set_fixed_gen(self, fixed_gen_def: Callable[[FixedGenContext], None]): + if self.fixed_gen is not None: + raise Exception("ASTCircuit cannot have more than one fixed generator.") + else: + self.fixed_gen = fixed_gen_def + + def get_step_type(self, uuid: int) -> ASTStepType: + if uuid in self.step_types.keys(): + return self.step_types[uuid] + else: + raise ValueError("ASTStepType not found.") + + +# pub struct StepType { +# id: StepTypeUUID, + +# pub name: String, +# pub signals: Vec, +# pub constraints: Vec>, +# pub transition_constraints: Vec>, +# pub lookups: Vec>, +# pub annotations: HashMap, +# } + + +@dataclass +class ASTStepType: + id: int + name: str + signals: List[InternalSignal] + constraints: List[ASTConstraint] + transition_constraints: List[TransitionConstraint] + annotations: Dict[int, str] + + def new(name: str) -> ASTStepType: + return ASTStepType(uuid(), name, [], [], [], {}) + + def __str__(self): + signals_str = ( + "\n\t\t\t\t" + + ",\n\t\t\t\t".join(str(signal) for signal in self.signals) + + "\n\t\t\t" + if self.signals + else "" + ) + constraints_str = ( + "\n\t\t\t\t" + + ",\n\t\t\t\t".join(str(constraint) for constraint in self.constraints) + + "\n\t\t\t" + if self.constraints + else "" + ) + transition_constraints_str = ( + "\n\t\t\t\t" + + ",\n\t\t\t\t".join(str(tc) for tc in self.transition_constraints) + + "\n\t\t\t" + if self.transition_constraints + else "" + ) + annotations_str = ( + "\n\t\t\t\t" + + ",\n\t\t\t\t".join(f"{k}: {v}" for k, v in self.annotations.items()) + + "\n\t\t\t" + if self.annotations + else "" + ) + + return ( + f"ASTStepType(\n" + f"\t\t\tid={self.id},\n" + f"\t\t\tname='{self.name}',\n" + f"\t\t\tsignals=[{signals_str}],\n" + f"\t\t\tconstraints=[{constraints_str}],\n" + f"\t\t\ttransition_constraints=[{transition_constraints_str}],\n" + f"\t\t\tannotations={{{annotations_str}}}\n" + f"\t\t)" + ) + + def __json__(self): + return { + "id": self.id, + "name": self.name, + "signals": [x.__json__() for x in self.signals], + "constraints": [x.__json__() for x in self.constraints], + "transition_constraints": [ + x.__json__() for x in self.transition_constraints + ], + "annotations": self.annotations, + } + + def add_signal(self: ASTStepType, name: str) -> InternalSignal: + signal = InternalSignal(name) + self.signals.append(signal) + self.annotations[signal.id] = name + return signal + + def add_constr(self: ASTStepType, annotation: str, expr: Expr): + condition = ASTConstraint(annotation, expr) + self.constraints.append(condition) + + def add_transition(self: ASTStepType, annotation: str, expr: Expr): + condition = TransitionConstraint(annotation, expr) + self.transition_constraints.append(condition) + + def __eq__(self: ASTStepType, other: ASTStepType) -> bool: + if isinstance(self, ASTStepType) and isinstance(other, ASTStepType): + return self.id == other.id + return False + + def __req__(other: ASTStepType, self: ASTStepType) -> bool: + return ASTStepType.__eq__(self, other) + + def __hash__(self: ASTStepType): + return hash(self.id) + + +@dataclass +class ASTConstraint: + annotation: str + expr: Expr + + def __str__(self: ASTConstraint): + return ( + f"Constraint(\n" + f"\t\t\t\t\tannotation='{self.annotation}',\n" + f"\t\t\t\t\texpr={self.expr}\n" + f"\t\t\t\t)" + ) + + def __json__(self: ASTConstraint): + return {"annotation": self.annotation, "expr": self.expr.__json__()} + + +@dataclass +class TransitionConstraint: + annotation: str + expr: Expr + + def __str__(self: TransitionConstraint): + return f"TransitionConstraint({self.annotation})" + + def __json__(self: TransitionConstraint): + return {"annotation": self.annotation, "expr": self.expr.__json__()} + + +@dataclass +class ForwardSignal: + id: int + phase: int + annotation: str + + def __init__(self: ForwardSignal, phase: int, annotation: str): + self.id: int = uuid() + self.phase = phase + self.annotation = annotation + + def __str__(self: ForwardSignal): + return f"ForwardSignal(id={self.id}, phase={self.phase}, annotation='{self.annotation}')" + + def __json__(self: ForwardSignal): + return asdict(self) + + +@dataclass +class SharedSignal: + id: int + phase: int + annotation: str + + def __init__(self: SharedSignal, phase: int, annotation: str): + self.id: int = uuid() + self.phase = phase + self.annotation = annotation + + def __str__(self: SharedSignal): + return f"SharedSignal(id={self.id}, phase={self.phase}, annotation='{self.annotation}')" + + def __json__(self: SharedSignal): + return asdict(self) + + +class ExposeOffset: + pass + + +class First(ExposeOffset): + def __str__(self: First): + return "First" + + def __json__(self: First): + return {"First": 0} + + +class Last(ExposeOffset): + def __str__(self: Last): + return "Last" + + def __json__(self: Last): + return {"Last": -1} + + +@dataclass +class Step(ExposeOffset): + offset: int + + def __str__(self: Step): + return f"Step({self.offset})" + + def __json__(self: Step): + return {"Step": self.offset} + + +@dataclass +class FixedSignal: + id: int + annotation: str + + def __init__(self: FixedSignal, annotation: str): + self.id: int = uuid() + self.annotation = annotation + + def __str__(self: FixedSignal): + return f"FixedSignal(id={self.id}, annotation='{self.annotation}')" + + def __json__(self: FixedSignal): + return asdict(self) + + +@dataclass +class InternalSignal: + id: int + annotation: str + + def __init__(self: InternalSignal, annotation: str): + self.id = uuid() + self.annotation = annotation + + def __str__(self: InternalSignal): + return f"InternalSignal(id={self.id}, annotation='{self.annotation}')" + + def __json__(self: InternalSignal): + return asdict(self) diff --git a/frontend/python/chiquito/dsl.py b/frontend/python/chiquito/dsl.py new file mode 100644 index 00000000..7201f09e --- /dev/null +++ b/frontend/python/chiquito/dsl.py @@ -0,0 +1,165 @@ +from __future__ import annotations +from enum import Enum +from typing import Callable, Any +# import rust_chiquito # rust bindings +from chiquito import rust_chiquito +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 + + +class CircuitMode(Enum): + NoMode = 0 + SETUP = 1 + Trace = 2 + + +class Circuit: + def __init__(self: Circuit): + self.ast = ASTCircuit() + self.witness = TraceWitness() + self.rust_ast_id = 0 + self.mode = CircuitMode.SETUP + self.setup() + + def forward(self: Circuit, name: str) -> Forward: + assert self.mode == CircuitMode.SETUP + return Forward(self.ast.add_forward(name, 0), False) + + def forward_with_phase(self: Circuit, name: str, phase: int) -> Forward: + assert self.mode == CircuitMode.SETUP + return Forward(self.ast.add_forward(name, phase), False) + + def shared(self: Circuit, name: str) -> Shared: + assert self.mode == CircuitMode.SETUP + return Shared(self.ast.add_shared(name, 0), 0) + + def shared_with_phase(self: Circuit, name: str, phase: int) -> Shared: + assert self.mode == CircuitMode.SETUP + return Shared(self.ast.add_shared(name, phase), 0) + + def fixed(self: Circuit, name: str) -> Fixed: + assert self.mode == CircuitMode.SETUP + return Fixed(self.ast.add_fixed(name), 0) + + def expose(self: Circuit, signal: Queriable, offset: ExposeOffset): + assert self.mode == CircuitMode.SETUP + if isinstance(signal, (Forward, Shared)): + self.ast.expose(signal, offset) + else: + raise TypeError(f"Can only expose ForwardSignal or SharedSignal.") + + def step_type(self: Circuit, step_type: StepType) -> StepType: + assert self.mode == CircuitMode.SETUP + self.ast.add_step_type(step_type.step_type, step_type.step_type.name) + return step_type + + def step_type_def(self: StepType) -> StepType: + assert self.mode == CircuitMode.SETUP + self.ast.add_step_type_def() + + def fixed_gen(self: Circuit, fixed_gen_def: Callable[[FixedGenContext], None]): + self.ast.set_fixed_gen(fixed_gen_def) + + def pragma_first_step(self: Circuit, step_type: StepType) -> None: + assert self.mode == CircuitMode.SETUP + self.ast.first_step = step_type.step_type.id + + def pragma_last_step(self: Circuit, step_type: StepType) -> None: + assert self.mode == CircuitMode.SETUP + self.ast.last_step = step_type.step_type.id + + def pragma_num_steps(self: Circuit, num_steps: int) -> None: + assert self.mode == CircuitMode.SETUP + self.ast.num_steps = num_steps + + def pragma_disable_q_enable(self: Circuit) -> None: + assert self.mode == CircuitMode.SETUP + self.ast.q_enable = False + + def add(self: Circuit, step_type: StepType, args: Any): + assert self.mode == CircuitMode.Trace + step_instance: StepInstance = step_type.gen_step_instance(args) + self.witness.step_instances.append(step_instance) + + def gen_witness(self: Circuit, args: Any) -> TraceWitness: + self.mode = CircuitMode.Trace + self.witness = TraceWitness() + self.trace(args) + self.mode = CircuitMode.NoMode + witness = self.witness + del self.witness + return witness + + def get_ast_json(self: Circuit) -> str: + return json.dumps(self.ast, cls=CustomEncoder, indent=4) + + 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) + witness_json: str = witness.get_witness_json() + rust_chiquito.halo2_mock_prover(witness_json, self.rust_ast_id) + + def __str__(self: Circuit) -> str: + return self.ast.__str__() + + +class StepTypeMode(Enum): + NoMode = 0 + SETUP = 1 + WG = 2 + + +class StepType: + def __init__(self: StepType, circuit: Circuit, step_type_name: str): + self.step_type = ASTStepType.new(step_type_name) + self.circuit = circuit + self.mode = StepTypeMode.SETUP + self.setup() + + def gen_step_instance(self: StepType, args: Any) -> StepInstance: + self.mode = StepTypeMode.WG + self.step_instance = StepInstance.new(self.step_type.id) + self.wg(args) + self.mode = StepTypeMode.NoMode + step_instance = self.step_instance + del self.step_instance + return step_instance + + def internal(self: StepType, name: str) -> Internal: + assert self.mode == StepTypeMode.SETUP + + return Internal(self.step_type.add_signal(name)) + + def constr(self: StepType, constraint: ToConstraint): + assert self.mode == StepTypeMode.SETUP + + constraint = to_constraint(constraint) + StepType.enforce_constraint_typing(constraint) + self.step_type.add_constr(constraint.annotation, constraint.expr) + + def transition(self: StepType, constraint: ToConstraint): + assert self.mode == StepTypeMode.SETUP + + constraint = to_constraint(constraint) + StepType.enforce_constraint_typing(constraint) + self.step_type.add_transition(constraint.annotation, constraint.expr) + + def enforce_constraint_typing(constraint: Constraint): + if constraint.typing != Typing.AntiBooly: + raise ValueError( + f"Expected AntiBooly constraint, got {constraint.typing} (constraint: {constraint.annotation})" + ) + + def assign(self: StepType, lhs: Queriable, rhs: F): + assert self.mode == StepTypeMode.WG + + self.step_instance.assign(lhs, rhs) + + # TODO: Implement add_lookup after lookup abstraction PR is merged. diff --git a/frontend/python/chiquito/expr.py b/frontend/python/chiquito/expr.py new file mode 100644 index 00000000..52f99364 --- /dev/null +++ b/frontend/python/chiquito/expr.py @@ -0,0 +1,157 @@ +from __future__ import annotations +from typing import List +from dataclasses import dataclass + +from chiquito.util import F + + +# pub enum Expr { +# Const(F), +# Sum(Vec>), +# Mul(Vec>), +# Neg(Box>), +# Pow(Box>, u32), +# Query(Queriable), +# Halo2Expr(Expression), +# } + + +@dataclass +class Expr: + def __neg__(self: Expr) -> Neg: + return Neg(self) + + def __add__(self: Expr, rhs: ToExpr) -> Sum: + rhs = to_expr(rhs) + return Sum([self, rhs]) + + def __radd__(self: Expr, lhs: ToExpr) -> Sum: + return Expr.__add__(lhs, self) + + def __sub__(self: Expr, rhs: ToExpr) -> Sum: + rhs = to_expr(rhs) + return Sum([self, Neg(rhs)]) + + def __rsub__(self: Expr, lhs: ToExpr) -> Sum: + return Expr.__sub__(lhs, self) + + def __mul__(self: Expr, rhs: ToExpr) -> Mul: + rhs = to_expr(rhs) + return Mul([self, rhs]) + + def __rmul__(self: Expr, lhs: ToExpr) -> Mul: + return Expr.__mul__(lhs, self) + + def __pow__(self: Expr, rhs: int) -> Pow: + return Pow(self, rhs) + + +@dataclass +class Const(Expr): + value: F + + def __str__(self: Const) -> str: + return str(self.value) + + def __json__(self): + return {"Const": self.value} + + +@dataclass +class Sum(Expr): + exprs: List[Expr] + + def __str__(self: Sum) -> str: + result = "(" + for i, expr in enumerate(self.exprs): + if type(expr) is Neg: + if i == 0: + result += "-" + else: + result += " - " + else: + if i > 0: + result += " + " + result += str(expr) + result += ")" + return result + + def __json__(self): + return {"Sum": [expr.__json__() for expr in self.exprs]} + + def __add__(self: Sum, rhs: ToExpr) -> Sum: + rhs = to_expr(rhs) + return Sum(self.exprs + [rhs]) + + def __radd__(self: Sum, lhs: ToExpr) -> Sum: + return Sum.__add__(lhs, self) + + def __sub__(self: Sum, rhs: ToExpr) -> Sum: + rhs = to_expr(rhs) + return Sum(self.exprs + [Neg(rhs)]) + + def __rsub__(self: Sum, lhs: ToExpr) -> Sum: + return Sum.__sub__(lhs, self) + + +@dataclass +class Mul(Expr): + exprs: List[Expr] + + def __str__(self: Mul) -> str: + return "*".join([str(expr) for expr in self.exprs]) + + def __json__(self): + return {"Mul": [expr.__json__() for expr in self.exprs]} + + def __mul__(self: Mul, rhs: ToExpr) -> Mul: + rhs = to_expr(rhs) + return Mul(self.exprs + [rhs]) + + def __rmul__(self: Mul, lhs: ToExpr) -> Mul: + return Mul.__mul__(lhs, self) + + +@dataclass +class Neg(Expr): + expr: Expr + + def __str__(self: Neg) -> str: + return "(-" + str(self.expr) + ")" + + def __json__(self): + return {"Neg": self.expr.__json__()} + + def __neg__(self: Neg) -> Expr: + return self.expr + + +@dataclass +class Pow(Expr): + expr: Expr + pow: int + + def __str__(self: Pow) -> str: + return str(self.expr) + "^" + str(self.pow) + + def __json__(self): + return {"Pow": [self.expr.__json__(), self.pow]} + + +ToExpr = Expr | int | F + + +def to_expr(v: ToExpr) -> Expr: + if isinstance(v, Expr): + return v + elif isinstance(v, int): + if v >= 0: + return Const(F(v)) + else: + return Neg(Const(F(-v))) + elif isinstance(v, F): + return Const(v) + else: + raise TypeError( + f"Type {type(v)} is not ToExpr (one of Expr, int, F, or Constraint)." + ) diff --git a/frontend/python/chiquito/query.py b/frontend/python/chiquito/query.py new file mode 100644 index 00000000..9dafb6c2 --- /dev/null +++ b/frontend/python/chiquito/query.py @@ -0,0 +1,138 @@ +from __future__ import annotations + +from chiquito.expr import Expr + +# Commented out to avoid circular reference +# from chiquito_ast import InternalSignal, ForwardSignal, SharedSignal, FixedSignal, ASTStepType + + +# pub enum Queriable { +# Internal(InternalSignal), +# Forward(ForwardSignal, bool), +# Shared(SharedSignal, i32), +# Fixed(FixedSignal, i32), +# StepTypeNext(ASTStepTypeHandler), +# Halo2AdviceQuery(ImportedHalo2Advice, i32), +# Halo2FixedQuery(ImportedHalo2Fixed, i32), +# #[allow(non_camel_case_types)] +# _unaccessible(PhantomData), +# } + + +class Queriable(Expr): + # __hash__ method is required, because Queriable is used as a key in the assignment dictionary. + def __hash__(self: Queriable): + return hash(self.uuid()) + + # Implemented in all children classes, and only children instances will ever be created for Queriable. + def uuid(self: Queriable) -> int: + pass + + +# Not defined as @dataclass, because inherited __hash__ will be set to None. +class Internal(Queriable): + def __init__(self: Internal, signal: InternalSignal): + self.signal = signal + + def uuid(self: Internal) -> int: + return self.signal.id + + def __str__(self: Internal) -> str: + return self.signal.annotation + + def __json__(self): + return {"Internal": self.signal.__json__()} + + +class Forward(Queriable): + def __init__(self: Forward, signal: ForwardSignal, rotation: bool): + self.signal = signal + self.rotation = rotation + + def next(self: Forward) -> Forward: + if self.rotation: + raise ValueError("Cannot rotate Forward twice.") + else: + return Forward(self.signal, True) + + def uuid(self: Forward) -> int: + return self.signal.id + + def __str__(self: Forward) -> str: + if not self.rotation: + return self.signal.annotation + else: + return f"next({self.signal.annotation})" + + def __json__(self): + return {"Forward": [self.signal.__json__(), self.rotation]} + + +class Shared(Queriable): + def __init__(self: Shared, signal: SharedSignal, rotation: int): + self.signal = signal + self.rotation = rotation + + def next(self: Shared) -> Shared: + return Shared(self.signal, self.rotation + 1) + + def prev(self: Shared) -> Shared: + return Shared(self.signal, self.rotation - 1) + + def rot(self: Shared, rotation: int) -> Shared: + return Shared(self.signal, self.rotation + rotation) + + def uuid(self: Shared) -> int: + return self.signal.id + + def __str__(self: Shared) -> str: + if self.rotation == 0: + return self.signal.annotation + else: + return f"{self.signal.annotation}(rot {self.rotation})" + + def __json__(self): + return {"Shared": [self.signal.__json__(), self.rotation]} + + +class Fixed(Queriable): + def __init__(self: Fixed, signal: FixedSignal, rotation: int): + self.signal = signal + self.rotation = rotation + + def next(self: Fixed) -> Fixed: + return Fixed(self.signal, self.rotation + 1) + + def prev(self: Fixed) -> Fixed: + return Fixed(self.signal, self.rotation - 1) + + def rot(self: Fixed, rotation: int) -> Fixed: + return Fixed(self.signal, self.rotation + rotation) + + def uuid(self: Fixed) -> int: + return self.signal.id + + def __str__(self: Fixed) -> str: + if self.rotation == 0: + return self.signal.annotation + else: + return f"{self.signal.annotation}(rot {self.rotation})" + + def __json__(self): + return {"Fixed": [self.signal.__json__(), self.rotation]} + + +class StepTypeNext(Queriable): + def __init__(self: StepTypeNext, step_type: ASTStepType): + self.step_type = step_type + + def uuid(self: ASTStepType) -> int: + return self.id + + def __str__(self: ASTStepType) -> str: + return self.name + + def __json__(self): + return { + "StepTypeNext": {"id": self.step_type.id, "annotation": self.step_type.name} + } diff --git a/frontend/python/chiquito/util.py b/frontend/python/chiquito/util.py new file mode 100644 index 00000000..d838aa19 --- /dev/null +++ b/frontend/python/chiquito/util.py @@ -0,0 +1,31 @@ +from __future__ import annotations +from py_ecc import bn128 +from uuid import uuid1 +import json + +F = bn128.FQ + + +def json_method(self: F): + # Convert the integer to a byte array + byte_array = self.n.to_bytes(32, "little") + + # Split into four 64-bit integers + ints = [int.from_bytes(byte_array[i * 8 : i * 8 + 8], "little") for i in range(4)] + + return ints + + +F.__json__ = json_method + + +class CustomEncoder(json.JSONEncoder): + def default(self, obj): + if hasattr(obj, "__json__"): + return obj.__json__() + return super().default(obj) + + +# int field is the u128 version of uuid. +def uuid() -> int: + return uuid1(node=int.from_bytes([10, 10, 10, 10, 10, 10], byteorder="little")).int diff --git a/frontend/python/chiquito/wit_gen.py b/frontend/python/chiquito/wit_gen.py new file mode 100644 index 00000000..b7408756 --- /dev/null +++ b/frontend/python/chiquito/wit_gen.py @@ -0,0 +1,122 @@ +from __future__ import annotations +from dataclasses import dataclass, field +from typing import Dict, List, Callable, Any +import json + +from chiquito.query import Queriable, Fixed +from chiquito.util import F, CustomEncoder + +# Commented out to avoid circular reference +# from dsl import Circuit, StepType + + +@dataclass +class StepInstance: + step_type_uuid: int = 0 + assignments: Dict[Queriable, F] = field(default_factory=dict) + + def new(step_type_uuid: int) -> StepInstance: + return StepInstance(step_type_uuid, {}) + + def assign(self: StepInstance, lhs: Queriable, rhs: F): + self.assignments[lhs] = rhs + + def __str__(self: StepInstance): + assignments_str = ( + "\n\t\t\t\t" + + ",\n\t\t\t\t".join( + f"{str(lhs)} = {rhs}" for (lhs, rhs) in self.assignments.items() + ) + + "\n\t\t\t" + if self.assignments + else "" + ) + return ( + f"StepInstance(\n" + f"\t\t\tstep_type_uuid={self.step_type_uuid},\n" + f"\t\t\tassignments={{{assignments_str}}},\n" + f"\t\t)" + ) + + # For assignments, return "uuid: (Queriable, F)" rather than "Queriable: F", because JSON doesn't accept Dict as key. + def __json__(self: StepInstance): + return { + "step_type_uuid": self.step_type_uuid, + "assignments": { + lhs.uuid(): [lhs, rhs] for (lhs, rhs) in self.assignments.items() + }, + } + + +Witness = List[StepInstance] + + +@dataclass +class TraceWitness: + step_instances: Witness = field(default_factory=list) + + def __str__(self: TraceWitness): + step_instances_str = ( + "\n\t\t" + + ",\n\t\t".join( + str(step_instance) for step_instance in self.step_instances + ) + + "\n\t" + if self.step_instances + else "" + ) + return f"TraceWitness(\n" f"\tstep_instances={{{step_instances_str}}},\n" f")" + + def __json__(self: TraceWitness): + return { + "step_instances": [ + step_instance.__json__() for step_instance in self.step_instances + ] + } + + def get_witness_json(self: TraceWitness) -> str: + return json.dumps(self, cls=CustomEncoder, indent=4) + + def evil_witness_test( + self: TraceWitness, + step_instance_indices: List[int], + assignment_indices: List[int], + rhs: List[F], + ) -> TraceWitness: + if not len(step_instance_indices) == len(assignment_indices) == len(rhs): + raise ValueError(f"`evil_witness_test` inputs have different lengths.") + new_step_instances = self.step_instances.copy() + for i in range(len(step_instance_indices)): + keys = list(new_step_instances[step_instance_indices[i]].assignments.keys()) + new_step_instances[step_instance_indices[i]].assignments[ + keys[assignment_indices[i]] + ] = rhs[i] + return TraceWitness(new_step_instances) + + +FixedAssigment = Dict[Queriable, List[F]] + + +@dataclass +class FixedGenContext: + assignments: FixedAssigment = field(default_factory=dict) + num_steps: int = 0 + + def new(num_steps: int) -> FixedGenContext: + return FixedGenContext({}, num_steps) + + def assign(self: FixedGenContext, offset: int, lhs: Queriable, rhs: F): + if not FixedGenContext.is_fixed_queriable(lhs): + raise ValueError(f"Cannot assign to non-fixed signal.") + if lhs in self.assignments.keys(): + self.assignments[lhs][offset] = rhs + else: + self.assignments[lhs] = [F.zero()] * self.num_steps + self.assignments[lhs][offset] = rhs + + def is_fixed_queriable(q: Queriable) -> bool: + match q.enum: + case Fixed(_, _): + return True + case _: + return False diff --git a/frontend/python/src/lib.rs b/frontend/python/src/lib.rs deleted file mode 100644 index 87838129..00000000 --- a/frontend/python/src/lib.rs +++ /dev/null @@ -1,14 +0,0 @@ -use pyo3::prelude::*; - -/// Formats the sum of two numbers as string. -#[pyfunction] -fn sum_as_string(a: usize, b: usize) -> PyResult { - Ok((a + b).to_string()) -} - -/// A Python module implemented in Rust. -#[pymodule] -fn python(_py: Python, m: &PyModule) -> PyResult<()> { - m.add_function(wrap_pyfunction!(sum_as_string, m)?)?; - Ok(()) -} \ No newline at end of file diff --git a/frontend/python/pyproject.toml b/pyproject.toml similarity index 65% rename from frontend/python/pyproject.toml rename to pyproject.toml index 9bd5ee2b..08fea9f5 100644 --- a/frontend/python/pyproject.toml +++ b/pyproject.toml @@ -1,9 +1,11 @@ + [build-system] -requires = ["maturin>=1.2,<2.0"] +requires = ["maturin>=1.1,<2.0"] build-backend = "maturin" [project] -name = "python" +name = "chiquito" +dependencies = ["py_ecc"] requires-python = ">=3.7" classifiers = [ "Programming Language :: Rust", @@ -13,4 +15,7 @@ classifiers = [ [tool.maturin] +bindings = 'pyo3' features = ["pyo3/extension-module"] +python-source = "frontend/python" +module-name = "chiquito.rust_chiquito" diff --git a/src/lib.rs b/src/lib.rs index 678d35d7..b1554919 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,6 +1,7 @@ pub mod ast; pub mod frontend; pub mod plonkish; +pub mod python; pub mod stdlib; mod util; pub mod wit_gen; diff --git a/src/python.rs b/src/python.rs new file mode 100644 index 00000000..c11d2c85 --- /dev/null +++ b/src/python.rs @@ -0,0 +1,50 @@ +use crate::{ + ast::Circuit, + frontend::pychiquito::{chiquito_ast_to_halo2, chiquito_halo2_mock_prover}, + wit_gen::TraceWitness, +}; +use halo2_proofs::halo2curves::bn256::Fr; +use pyo3::{ + prelude::*, + types::{PyLong, PyString}, +}; + +#[pyfunction] +fn convert_and_print_ast(json: &PyString) { + let circuit: Circuit = + serde_json::from_str(json.to_str().expect("PyString convertion failed.")) + .expect("Json deserialization to Circuit failed."); + println!("{:?}", circuit); +} + +#[pyfunction] +fn convert_and_print_trace_witness(json: &PyString) { + let trace_witness: TraceWitness = + serde_json::from_str(json.to_str().expect("PyString convertion failed.")) + .expect("Json deserialization to TraceWitness failed."); + println!("{:?}", trace_witness); +} + +#[pyfunction] +fn ast_to_halo2(json: &PyString) -> u128 { + let uuid = chiquito_ast_to_halo2(json.to_str().expect("PyString convertion failed.")); + + uuid +} + +#[pyfunction] +fn halo2_mock_prover(witness_json: &PyString, ast_uuid: &PyLong) { + chiquito_halo2_mock_prover( + 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)?)?; + Ok(()) +} From 4fb8fc32edd4f7729faac2a8d5b18425368d0e33 Mon Sep 17 00:00:00 2001 From: trangnv Date: Fri, 18 Aug 2023 09:47:31 +0700 Subject: [PATCH 3/7] add python session on README --- README.md | 34 ++++++++++++++++++++++++++++++---- 1 file changed, 30 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 4ea9d170..7bc4a3fa 100644 --- a/README.md +++ b/README.md @@ -4,16 +4,18 @@ Chiquito is 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 and has a Halo2 backend, and other backends are in the works. It allows the user to manipulate an AST that’s compiled to a Chiquito Halo2 backend, which can be integrated into any Halo2 circuit. -It's **HIGHLY RECOMMENDED** that you read the [design principles](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#design-principles), [architecture, and specific terms](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#architecture) of a Chiquito circuit before getting started. +It's **HIGHLY RECOMMENDED** that you read the [design principles](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#design-principles), [architecture, and specific terms](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#architecture) of a Chiquito circuit before getting started. -You can also learn about the project's [current status](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#project-status-as-of-april-2023)) and its [next steps](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#vision-and-next-steps). +You can also learn about the project's [current status](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#project-status-as-of-april-2023) and its [next steps](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#vision-and-next-steps). # Getting Started ## Setup + Run the following in command line to add Chiquito as a dependency for your project: + ``` -cargo add --git https://github.com/privacy-scaling-explorations/chiquito +cargo add --git https://github.com/privacy-scaling-explorations/chiquito ``` Use the following examples to understand how Chiquito works or use them as starting templates for building your own Chiquito circuit. @@ -22,9 +24,10 @@ Refer to the Appendix on the [exposed user functions](https://github.com/privacy Refer to [Testing and Links](#testing-and-links) on detailed API documentations. - ## Example: Fibonacci Circuit + Run the following in command line: + ``` cargo run --example fibonacci ``` @@ -32,19 +35,42 @@ cargo run --example fibonacci This example demonstrates how to construct signals, step types, constraints, and witness generation in Chiquito. Best for first time Chiquito users. ## Example: MiMC7 Circuit + TODO: annotate this code example This example demonstrates how to construct a lookup table and use external inputs as trace arguments in Chiquito, besides covering concepts in the Fibonacci example. MiMC7 is a zk-friendly hashing function. ## Example: zkEVM Bytecode Circuit + https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/1348 This example rewrites the zkEVM bytecode circuit using Chiquito and passes all original tests. It demonstrates how Chiquito can standardize and simplify larger scale circuits on the production level. +## Python bindings + +### Install chiquito with pip + +```bash +pip install chiquito +``` + +### Build from source + +In the root of this repo run + +```bash +python -m venv .env +source .env/bin/activate +pip install maturin +maturin develop +``` + # Testing and Links + **API documentation**: `cargo doc --no-deps --package chiquito --open` Currently API documentation is only written for exposed user functions, which are scattered across the DSL, constraint builder, compiler, and AST. **Refer to the following subdirectories for specific functions:** + - Circuit building (DSL): https://qwang98.github.io/chiquito/chiquito/dsl/index.html - Constraint building (constraint builder): https://qwang98.github.io/chiquito/chiquito/dsl/cb/index.html - Witness generation (compiler): https://qwang98.github.io/chiquito/chiquito/compiler/trait.WitnessGenContext.html From 78de022624b84c814577b7f7cf5098274c6fb14a Mon Sep 17 00:00:00 2001 From: trangnv Date: Mon, 21 Aug 2023 11:44:48 +0700 Subject: [PATCH 4/7] restruct and modify README --- .gitignore | 2 +- README.md | 13 ++++++++++++- pyproject.toml | 2 +- src/frontend/mod.rs | 1 + .../frontend}/python/chiquito/__init__.py | 0 {frontend => src/frontend}/python/chiquito/cb.py | 0 .../frontend}/python/chiquito/chiquito_ast.py | 0 {frontend => src/frontend}/python/chiquito/dsl.py | 0 {frontend => src/frontend}/python/chiquito/expr.py | 0 {frontend => src/frontend}/python/chiquito/query.py | 0 {frontend => src/frontend}/python/chiquito/util.py | 0 .../frontend}/python/chiquito/wit_gen.py | 0 src/{python.rs => frontend/python/mod.rs} | 0 src/lib.rs | 1 - 14 files changed, 15 insertions(+), 4 deletions(-) rename {frontend => src/frontend}/python/chiquito/__init__.py (100%) rename {frontend => src/frontend}/python/chiquito/cb.py (100%) rename {frontend => src/frontend}/python/chiquito/chiquito_ast.py (100%) rename {frontend => src/frontend}/python/chiquito/dsl.py (100%) rename {frontend => src/frontend}/python/chiquito/expr.py (100%) rename {frontend => src/frontend}/python/chiquito/query.py (100%) rename {frontend => src/frontend}/python/chiquito/util.py (100%) rename {frontend => src/frontend}/python/chiquito/wit_gen.py (100%) rename src/{python.rs => frontend/python/mod.rs} (100%) diff --git a/.gitignore b/.gitignore index b55d2a6f..ee6af51a 100644 --- a/.gitignore +++ b/.gitignore @@ -3,4 +3,4 @@ .vscode .env __pycache__ -*.so \ No newline at end of file +*.so diff --git a/README.md b/README.md index 7bc4a3fa..35f814e7 100644 --- a/README.md +++ b/README.md @@ -48,15 +48,26 @@ This example rewrites the zkEVM bytecode circuit using Chiquito and passes all o ## Python bindings +There are 2 ways to install chiquito python bindings + ### Install chiquito with pip +To use chiquito in Python, just need to install it with pip + ```bash pip install chiquito ``` ### Build from source -In the root of this repo run +Chiquito is built in Rust. First [install Rust](https://www.rust-lang.org/tools/install), then clone this repo and enter the repo directory. + +```bash +git clone https://github.com/privacy-scaling-explorations/chiquito +cd chiquito +``` + +Then build the python bindings with maturin ```bash python -m venv .env diff --git a/pyproject.toml b/pyproject.toml index 08fea9f5..fc3da75c 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -17,5 +17,5 @@ classifiers = [ [tool.maturin] bindings = 'pyo3' features = ["pyo3/extension-module"] -python-source = "frontend/python" +python-source = "src/frontend/python" module-name = "chiquito.rust_chiquito" diff --git a/src/frontend/mod.rs b/src/frontend/mod.rs index f39746ef..91f79c65 100644 --- a/src/frontend/mod.rs +++ b/src/frontend/mod.rs @@ -1,2 +1,3 @@ pub mod dsl; pub mod pychiquito; +pub mod python; diff --git a/frontend/python/chiquito/__init__.py b/src/frontend/python/chiquito/__init__.py similarity index 100% rename from frontend/python/chiquito/__init__.py rename to src/frontend/python/chiquito/__init__.py diff --git a/frontend/python/chiquito/cb.py b/src/frontend/python/chiquito/cb.py similarity index 100% rename from frontend/python/chiquito/cb.py rename to src/frontend/python/chiquito/cb.py diff --git a/frontend/python/chiquito/chiquito_ast.py b/src/frontend/python/chiquito/chiquito_ast.py similarity index 100% rename from frontend/python/chiquito/chiquito_ast.py rename to src/frontend/python/chiquito/chiquito_ast.py diff --git a/frontend/python/chiquito/dsl.py b/src/frontend/python/chiquito/dsl.py similarity index 100% rename from frontend/python/chiquito/dsl.py rename to src/frontend/python/chiquito/dsl.py diff --git a/frontend/python/chiquito/expr.py b/src/frontend/python/chiquito/expr.py similarity index 100% rename from frontend/python/chiquito/expr.py rename to src/frontend/python/chiquito/expr.py diff --git a/frontend/python/chiquito/query.py b/src/frontend/python/chiquito/query.py similarity index 100% rename from frontend/python/chiquito/query.py rename to src/frontend/python/chiquito/query.py diff --git a/frontend/python/chiquito/util.py b/src/frontend/python/chiquito/util.py similarity index 100% rename from frontend/python/chiquito/util.py rename to src/frontend/python/chiquito/util.py diff --git a/frontend/python/chiquito/wit_gen.py b/src/frontend/python/chiquito/wit_gen.py similarity index 100% rename from frontend/python/chiquito/wit_gen.py rename to src/frontend/python/chiquito/wit_gen.py diff --git a/src/python.rs b/src/frontend/python/mod.rs similarity index 100% rename from src/python.rs rename to src/frontend/python/mod.rs diff --git a/src/lib.rs b/src/lib.rs index b1554919..678d35d7 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,7 +1,6 @@ pub mod ast; pub mod frontend; pub mod plonkish; -pub mod python; pub mod stdlib; mod util; pub mod wit_gen; From 25225456c06173853c85d6c2b550a78bcfaaf98e Mon Sep 17 00:00:00 2001 From: trangnv Date: Mon, 21 Aug 2023 14:29:50 +0700 Subject: [PATCH 5/7] move pychiquito.rs content to python/mod.rs --- src/frontend/mod.rs | 1 - src/frontend/pychiquito.rs | 1415 ----------------------------------- src/frontend/python/mod.rs | 1422 +++++++++++++++++++++++++++++++++++- 3 files changed, 1416 insertions(+), 1422 deletions(-) delete mode 100644 src/frontend/pychiquito.rs diff --git a/src/frontend/mod.rs b/src/frontend/mod.rs index 91f79c65..4b6c4645 100644 --- a/src/frontend/mod.rs +++ b/src/frontend/mod.rs @@ -1,3 +1,2 @@ pub mod dsl; -pub mod pychiquito; pub mod python; diff --git a/src/frontend/pychiquito.rs b/src/frontend/pychiquito.rs deleted file mode 100644 index 0b5371f2..00000000 --- a/src/frontend/pychiquito.rs +++ /dev/null @@ -1,1415 +0,0 @@ -use crate::{ - ast::{ - expr::{query::Queriable, Expr}, - Circuit, Constraint, ExposeOffset, FixedSignal, ForwardSignal, InternalSignal, - SharedSignal, StepType, StepTypeUUID, TransitionConstraint, - }, - frontend::dsl::StepTypeHandler, - plonkish::{ - backend::halo2::{chiquito2Halo2, ChiquitoHalo2, ChiquitoHalo2Circuit}, - compiler::{ - cell_manager::SingleRowCellManager, compile, config, - step_selector::SimpleStepSelectorBuilder, - }, - ir::assignments::AssignmentGenerator, - }, - util::{uuid, UUID}, - wit_gen::{StepInstance, TraceContext, TraceWitness}, -}; - -use core::result::Result; -use halo2_proofs::{dev::MockProver, halo2curves::bn256::Fr}; -use serde::de::{self, Deserialize, Deserializer, IgnoredAny, MapAccess, Visitor}; -use std::{cell::RefCell, collections::HashMap, fmt, rc::Rc}; - -type CircuitMapStore = (ChiquitoHalo2, Option>); -type CircuitMap = RefCell>; - -thread_local! { - pub static CIRCUIT_MAP: CircuitMap = RefCell::new(HashMap::new()); -} - -pub fn chiquito_ast_to_halo2(ast_json: &str) -> UUID { - let circuit: Circuit = - serde_json::from_str(ast_json).expect("Json deserialization to Circuit failed."); - - let config = config(SingleRowCellManager {}, SimpleStepSelectorBuilder {}); - let (chiquito, assignment_generator) = compile(config, &circuit); - let chiquito_halo2 = chiquito2Halo2(chiquito); - let uuid = uuid(); - - CIRCUIT_MAP.with(|circuit_map| { - circuit_map - .borrow_mut() - .insert(uuid, (chiquito_halo2, assignment_generator)); - }); - - println!("{:?}", uuid); - - uuid -} - -fn uuid_to_halo2(uuid: UUID) -> CircuitMapStore { - CIRCUIT_MAP.with(|circuit_map| { - let circuit_map = circuit_map.borrow(); - circuit_map.get(&uuid).unwrap().clone() - }) -} - -pub fn chiquito_halo2_mock_prover(witness_json: &str, ast_id: UUID) { - let trace_witness: TraceWitness = - serde_json::from_str(witness_json).expect("Json deserialization to TraceWitness failed."); - let (compiled, assignment_generator) = uuid_to_halo2(ast_id); - let circuit: ChiquitoHalo2Circuit<_> = ChiquitoHalo2Circuit::new( - compiled, - assignment_generator.map(|g| g.generate_with_witness(trace_witness)), - ); - - let prover = MockProver::::run(7, &circuit, circuit.instance()).unwrap(); - - let result = prover.verify_par(); - - println!("{:#?}", result); - - if let Err(failures) = &result { - for failure in failures.iter() { - println!("{}", failure); - } - } -} - -struct CircuitVisitor; - -impl<'de> Visitor<'de> for CircuitVisitor { - type Value = Circuit; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str("struct Cricuit") - } - - fn visit_map(self, mut map: A) -> Result, A::Error> - where - A: MapAccess<'de>, - { - let mut step_types = None; - let mut forward_signals = None; - let mut shared_signals = None; - let mut fixed_signals = None; - let mut exposed = None; - let mut annotations = None; - let mut first_step = None; - let mut last_step = None; - let mut num_steps = None; - let mut q_enable = None; - let mut id = None; - - while let Some(key) = map.next_key::()? { - match key.as_str() { - "step_types" => { - if step_types.is_some() { - return Err(de::Error::duplicate_field("step_types")); - } - step_types = Some(map.next_value::>>()?); - } - "forward_signals" => { - if forward_signals.is_some() { - return Err(de::Error::duplicate_field("forward_signals")); - } - forward_signals = Some(map.next_value::>()?); - } - "shared_signals" => { - if shared_signals.is_some() { - return Err(de::Error::duplicate_field("shared_signals")); - } - shared_signals = Some(map.next_value::>()?); - } - "fixed_signals" => { - if fixed_signals.is_some() { - return Err(de::Error::duplicate_field("fixed_signals")); - } - fixed_signals = Some(map.next_value::>()?); - } - "exposed" => { - if exposed.is_some() { - return Err(de::Error::duplicate_field("exposed")); - } - exposed = Some(map.next_value::, ExposeOffset)>>()?); - } - "annotations" => { - if annotations.is_some() { - return Err(de::Error::duplicate_field("annotations")); - } - annotations = Some(map.next_value::>()?); - } - "first_step" => { - if first_step.is_some() { - return Err(de::Error::duplicate_field("first_step")); - } - first_step = Some(map.next_value::>()?); - } - "last_step" => { - if last_step.is_some() { - return Err(de::Error::duplicate_field("last_step")); - } - last_step = Some(map.next_value::>()?); - } - "num_steps" => { - if num_steps.is_some() { - return Err(de::Error::duplicate_field("num_steps")); - } - num_steps = Some(map.next_value::()?); - } - "q_enable" => { - if q_enable.is_some() { - return Err(de::Error::duplicate_field("q_enable")); - } - q_enable = Some(map.next_value::()?); - } - "id" => { - if id.is_some() { - return Err(de::Error::duplicate_field("id")); - } - id = Some(map.next_value()?); - } - _ => { - return Err(de::Error::unknown_field( - &key, - &[ - "step_types", - "forward_signals", - "shared_signals", - "fixed_signals", - "exposed", - "annotations", - "first_step", - "last_step", - "num_steps", - "q_enable", - "id", - ], - )) - } - } - } - let step_types = step_types - .ok_or_else(|| de::Error::missing_field("step_types"))? - .into_iter() - .map(|(k, v)| (k, Rc::new(v))) - .collect(); - let forward_signals = - forward_signals.ok_or_else(|| de::Error::missing_field("forward_signals"))?; - let shared_signals = - shared_signals.ok_or_else(|| de::Error::missing_field("shared_signals"))?; - let fixed_signals = - fixed_signals.ok_or_else(|| de::Error::missing_field("fixed_signals"))?; - let exposed = exposed.ok_or_else(|| de::Error::missing_field("exposed"))?; - let annotations = annotations.ok_or_else(|| de::Error::missing_field("annotations"))?; - let first_step = first_step.ok_or_else(|| de::Error::missing_field("first_step"))?; - let last_step = last_step.ok_or_else(|| de::Error::missing_field("last_step"))?; - let num_steps = num_steps.ok_or_else(|| de::Error::missing_field("num_steps"))?; - let q_enable = q_enable.ok_or_else(|| de::Error::missing_field("q_enable"))?; - let id = id.ok_or_else(|| de::Error::missing_field("id"))?; - - Ok(Circuit { - step_types, - forward_signals, - shared_signals, - fixed_signals, - halo2_advice: Default::default(), - halo2_fixed: Default::default(), - exposed, - num_steps, - annotations, - trace: Some(Rc::new(|_: &mut TraceContext<_>, _: _| {})), - fixed_gen: None, - first_step, - last_step, - q_enable, - id, - }) - } -} -struct StepTypeVisitor; - -impl<'de> Visitor<'de> for StepTypeVisitor { - type Value = StepType; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str("struct StepType") - } - - fn visit_map(self, mut map: A) -> Result, A::Error> - where - A: MapAccess<'de>, - { - let mut id = None; - let mut name = None; - let mut signals = None; - let mut constraints = None; - let mut transition_constraints = None; - let mut annotations = None; - - while let Some(key) = map.next_key::()? { - match key.as_str() { - "id" => { - if id.is_some() { - return Err(de::Error::duplicate_field("id")); - } - id = Some(map.next_value()?); - } - "name" => { - if name.is_some() { - return Err(de::Error::duplicate_field("name")); - } - name = Some(map.next_value::()?); - } - "signals" => { - if signals.is_some() { - return Err(de::Error::duplicate_field("signals")); - } - signals = Some(map.next_value::>()?); - } - "constraints" => { - if constraints.is_some() { - return Err(de::Error::duplicate_field("constraints")); - } - constraints = Some(map.next_value::>>()?); - } - "transition_constraints" => { - if transition_constraints.is_some() { - return Err(de::Error::duplicate_field("transition_constraints")); - } - transition_constraints = - Some(map.next_value::>>()?); - } - "annotations" => { - if annotations.is_some() { - return Err(de::Error::duplicate_field("annotations")); - } - annotations = Some(map.next_value::>()?); - } - _ => { - return Err(de::Error::unknown_field( - &key, - &[ - "id", - "name", - "signals", - "constraints", - "transition_constraints", - "annotations", - ], - )) - } - } - } - let id = id.ok_or_else(|| de::Error::missing_field("id"))?; - let name = name.ok_or_else(|| de::Error::missing_field("name"))?; - let signals = signals.ok_or_else(|| de::Error::missing_field("signals"))?; - let constraints = constraints.ok_or_else(|| de::Error::missing_field("constraints"))?; - let transition_constraints = transition_constraints - .ok_or_else(|| de::Error::missing_field("transition_constraints"))?; - let annotations = annotations.ok_or_else(|| de::Error::missing_field("annotations"))?; - - let mut step_type = StepType::::new(id, name); - step_type.signals = signals; - step_type.constraints = constraints; - step_type.transition_constraints = transition_constraints; - step_type.lookups = Default::default(); - step_type.annotations = annotations; - - Ok(step_type) - } -} - -macro_rules! impl_visitor_constraint_transition { - ($name:ident, $type:ty, $display:expr) => { - struct $name; - - impl<'de> Visitor<'de> for $name { - type Value = $type; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str($display) - } - - fn visit_map(self, mut map: A) -> Result<$type, A::Error> - where - A: MapAccess<'de>, - { - let mut annotation = None; - let mut expr = None; - while let Some(key) = map.next_key::()? { - match key.as_str() { - "annotation" => { - if annotation.is_some() { - return Err(de::Error::duplicate_field("annotation")); - } - annotation = Some(map.next_value::()?); - } - "expr" => { - if expr.is_some() { - return Err(de::Error::duplicate_field("expr")); - } - expr = Some(map.next_value::>()?); - } - _ => return Err(de::Error::unknown_field(&key, &["annotation", "expr"])), - } - } - let annotation = - annotation.ok_or_else(|| de::Error::missing_field("annotation"))?; - let expr = expr.ok_or_else(|| de::Error::missing_field("expr"))?; - Ok(Self::Value { annotation, expr }) - } - } - }; -} - -impl_visitor_constraint_transition!(ConstraintVisitor, Constraint, "struct Constraint"); -impl_visitor_constraint_transition!( - TransitionConstraintVisitor, - TransitionConstraint, - "struct TransitionConstraint" -); - -struct ExprVisitor; - -impl<'de> Visitor<'de> for ExprVisitor { - type Value = Expr; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str("enum Expr") - } - - fn visit_map(self, mut map: A) -> Result, A::Error> - where - A: MapAccess<'de>, - { - let key: String = map - .next_key()? - .ok_or_else(|| de::Error::custom("map is empty"))?; - match key.as_str() { - "Const" => map.next_value().map(Expr::Const), - "Sum" => map.next_value().map(Expr::Sum), - "Mul" => map.next_value().map(Expr::Mul), - "Neg" => map.next_value().map(Expr::Neg), - "Pow" => map.next_value().map(|(expr, pow)| Expr::Pow(expr, pow)), - "Internal" => map - .next_value() - .map(|signal| Expr::Query(Queriable::Internal(signal))), - "Forward" => map - .next_value() - .map(|(signal, rotation)| Expr::Query(Queriable::Forward(signal, rotation))), - "Shared" => map - .next_value() - .map(|(signal, rotation)| Expr::Query(Queriable::Shared(signal, rotation))), - "Fixed" => map - .next_value() - .map(|(signal, rotation)| Expr::Query(Queriable::Fixed(signal, rotation))), - "StepTypeNext" => map - .next_value() - .map(|step_type| Expr::Query(Queriable::StepTypeNext(step_type))), - _ => Err(de::Error::unknown_variant( - &key, - &[ - "Const", - "Sum", - "Mul", - "Neg", - "Pow", - "Internal", - "Forward", - "Shared", - "Fixed", - "StepTypeNext", - ], - )), - } - } -} - -struct QueriableVisitor; - -impl<'de> Visitor<'de> for QueriableVisitor { - type Value = Queriable; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str("enum Queriable") - } - - fn visit_map(self, mut map: A) -> Result, A::Error> - where - A: MapAccess<'de>, - { - let key: String = map - .next_key()? - .ok_or_else(|| de::Error::custom("map is empty"))?; - match key.as_str() { - "Internal" => map.next_value().map(Queriable::Internal), - "Forward" => map - .next_value() - .map(|(signal, rotation)| Queriable::Forward(signal, rotation)), - "Shared" => map - .next_value() - .map(|(signal, rotation)| Queriable::Shared(signal, rotation)), - "Fixed" => map - .next_value() - .map(|(signal, rotation)| Queriable::Fixed(signal, rotation)), - "StepTypeNext" => map.next_value().map(Queriable::StepTypeNext), - _ => Err(de::Error::unknown_variant( - &key, - &["Internal", "Forward", "Shared", "Fixed", "StepTypeNext"], - )), - } - } -} - -struct ExposeOffsetVisitor; - -impl<'de> Visitor<'de> for ExposeOffsetVisitor { - type Value = ExposeOffset; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str("enum ExposeOffset") - } - - fn visit_map(self, mut map: A) -> Result - where - A: MapAccess<'de>, - { - let key: String = map - .next_key()? - .ok_or_else(|| de::Error::custom("map is empty"))?; - match key.as_str() { - "First" => { - let _ = map.next_value::()?; - Ok(ExposeOffset::First) - } - "Last" => { - let _ = map.next_value::()?; - Ok(ExposeOffset::Last) - } - "Step" => map.next_value().map(ExposeOffset::Step), - _ => Err(de::Error::unknown_variant(&key, &["First", "Last", "Step"])), - } - } -} - -macro_rules! impl_visitor_internal_fixed_steptypehandler { - ($name:ident, $type:ty, $display:expr) => { - struct $name; - - impl<'de> Visitor<'de> for $name { - type Value = $type; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str($display) - } - - fn visit_map(self, mut map: A) -> Result<$type, A::Error> - where - A: MapAccess<'de>, - { - let mut id = None; - let mut annotation = None; - while let Some(key) = map.next_key::()? { - match key.as_str() { - "id" => { - if id.is_some() { - return Err(de::Error::duplicate_field("id")); - } - id = Some(map.next_value()?); - } - "annotation" => { - if annotation.is_some() { - return Err(de::Error::duplicate_field("annotation")); - } - annotation = Some(map.next_value::()?); - } - _ => return Err(de::Error::unknown_field(&key, &["id", "annotation"])), - } - } - let id = id.ok_or_else(|| de::Error::missing_field("id"))?; - let annotation = - annotation.ok_or_else(|| de::Error::missing_field("annotation"))?; - Ok(<$type>::new_with_id(id, annotation)) - } - } - }; -} - -impl_visitor_internal_fixed_steptypehandler!( - InternalSignalVisitor, - InternalSignal, - "struct InternalSignal" -); -impl_visitor_internal_fixed_steptypehandler!(FixedSignalVisitor, FixedSignal, "struct FixedSignal"); -impl_visitor_internal_fixed_steptypehandler!( - StepTypeHandlerVisitor, - StepTypeHandler, - "struct StepTypeHandler" -); - -macro_rules! impl_visitor_forward_shared { - ($name:ident, $type:ty, $display:expr) => { - struct $name; - - impl<'de> Visitor<'de> for $name { - type Value = $type; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str($display) - } - - fn visit_map(self, mut map: A) -> Result<$type, A::Error> - where - A: MapAccess<'de>, - { - let mut id = None; - let mut phase = None; - let mut annotation = None; - while let Some(key) = map.next_key::()? { - match key.as_str() { - "id" => { - if id.is_some() { - return Err(de::Error::duplicate_field("id")); - } - id = Some(map.next_value()?); - } - "phase" => { - if phase.is_some() { - return Err(de::Error::duplicate_field("phase")); - } - phase = Some(map.next_value()?); - } - "annotation" => { - if annotation.is_some() { - return Err(de::Error::duplicate_field("annotation")); - } - annotation = Some(map.next_value::()?); - } - _ => { - return Err(de::Error::unknown_field( - &key, - &["id", "phase", "annotation"], - )) - } - } - } - let id = id.ok_or_else(|| de::Error::missing_field("id"))?; - let phase = phase.ok_or_else(|| de::Error::missing_field("phase"))?; - let annotation = - annotation.ok_or_else(|| de::Error::missing_field("annotation"))?; - Ok(<$type>::new_with_id(id, phase, annotation)) - } - } - }; -} - -impl_visitor_forward_shared!(ForwardSignalVisitor, ForwardSignal, "struct ForwardSignal"); -impl_visitor_forward_shared!(SharedSignalVisitor, SharedSignal, "struct SharedSignal"); - -struct TraceWitnessVisitor; - -impl<'de> Visitor<'de> for TraceWitnessVisitor { - type Value = TraceWitness; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str("struct TraceWitness") - } - - fn visit_map(self, mut map: A) -> Result, A::Error> - where - A: MapAccess<'de>, - { - let mut step_instances = None; - - while let Some(key) = map.next_key::()? { - match key.as_str() { - "step_instances" => { - if step_instances.is_some() { - return Err(de::Error::duplicate_field("step_instances")); - } - step_instances = Some(map.next_value()?); - } - _ => return Err(de::Error::unknown_field(&key, &["step_instances"])), - } - } - let step_instances = - step_instances.ok_or_else(|| de::Error::missing_field("step_instances"))?; - Ok(Self::Value { step_instances }) - } -} - -struct StepInstanceVisitor; - -impl<'de> Visitor<'de> for StepInstanceVisitor { - type Value = StepInstance; - - fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { - formatter.write_str("struct StepInstance") - } - - fn visit_map(self, mut map: A) -> Result, A::Error> - where - A: MapAccess<'de>, - { - let mut step_type_uuid = None; - let mut assignments = None; - - while let Some(key) = map.next_key::()? { - match key.as_str() { - "step_type_uuid" => { - if step_type_uuid.is_some() { - return Err(de::Error::duplicate_field("step_type_uuid")); - } - step_type_uuid = Some(map.next_value()?); - } - "assignments" => { - if assignments.is_some() { - return Err(de::Error::duplicate_field("assignments")); - } - assignments = Some(map.next_value::, Fr)>>()?); - } - _ => { - return Err(de::Error::unknown_field( - &key, - &["step_type_uuid", "assignments"], - )) - } - } - } - let step_type_uuid = - step_type_uuid.ok_or_else(|| de::Error::missing_field("step_type_uuid"))?; - - let assignments: HashMap, Fr> = assignments - .ok_or_else(|| de::Error::missing_field("assignments"))? - .into_values() - .collect(); - - Ok(Self::Value { - step_type_uuid, - assignments, - }) - } -} - -macro_rules! impl_deserialize { - ($name:ident, $type:ty) => { - impl<'de> Deserialize<'de> for $type { - fn deserialize(deserializer: D) -> Result<$type, D::Error> - where - D: Deserializer<'de>, - { - deserializer.deserialize_map($name) - } - } - }; -} - -impl_deserialize!(ExprVisitor, Expr); -impl_deserialize!(QueriableVisitor, Queriable); -impl_deserialize!(ExposeOffsetVisitor, ExposeOffset); -impl_deserialize!(InternalSignalVisitor, InternalSignal); -impl_deserialize!(FixedSignalVisitor, FixedSignal); -impl_deserialize!(ForwardSignalVisitor, ForwardSignal); -impl_deserialize!(SharedSignalVisitor, SharedSignal); -impl_deserialize!(StepTypeHandlerVisitor, StepTypeHandler); -impl_deserialize!(ConstraintVisitor, Constraint); -impl_deserialize!(TransitionConstraintVisitor, TransitionConstraint); -impl_deserialize!(StepTypeVisitor, StepType); -impl_deserialize!(TraceWitnessVisitor, TraceWitness); -impl_deserialize!(StepInstanceVisitor, StepInstance); - -impl<'de> Deserialize<'de> for Circuit { - fn deserialize(deserializer: D) -> Result, D::Error> - where - D: Deserializer<'de>, - { - deserializer.deserialize_map(CircuitVisitor) - } -} - -#[cfg(test)] -mod tests { - use super::*; - #[test] - fn test_trace_witness() { - let json = r#" - { - "step_instances": [ - { - "step_type_uuid": 270606747459021742275781620564109167114, - "assignments": { - "270606737951642240564318377467548666378": [ - { - "Forward": [ - { - "id": 270606737951642240564318377467548666378, - "phase": 0, - "annotation": "a" - }, - false - ] - }, - [ - 55, - 0, - 0, - 0 - ] - ], - "270606743497613616562965561253747624458": [ - { - "Forward": [ - { - "id": 270606743497613616562965561253747624458, - "phase": 0, - "annotation": "b" - }, - false - ] - }, - [ - 89, - 0, - 0, - 0 - ] - ], - "270606753004993118272949371872716917258": [ - { - "Internal": { - "id": 270606753004993118272949371872716917258, - "annotation": "c" - } - }, - [ - 144, - 0, - 0, - 0 - ] - ] - } - }, - { - "step_type_uuid": 270606783111694873693576112554652600842, - "assignments": { - "270606737951642240564318377467548666378": [ - { - "Forward": [ - { - "id": 270606737951642240564318377467548666378, - "phase": 0, - "annotation": "a" - }, - false - ] - }, - [ - 89, - 0, - 0, - 0 - ] - ], - "270606743497613616562965561253747624458": [ - { - "Forward": [ - { - "id": 270606743497613616562965561253747624458, - "phase": 0, - "annotation": "b" - }, - false - ] - }, - [ - 144, - 0, - 0, - 0 - ] - ], - "270606786280821374261518951164072823306": [ - { - "Internal": { - "id": 270606786280821374261518951164072823306, - "annotation": "c" - } - }, - [ - 233, - 0, - 0, - 0 - ] - ] - } - } - ] - } - "#; - let trace_witness: TraceWitness = serde_json::from_str(json).unwrap(); - println!("{:?}", trace_witness); - } - - #[test] - fn test_expose_offset() { - let mut json = r#" - { - "Step": 1 - } - "#; - let _: ExposeOffset = serde_json::from_str(json).unwrap(); - json = r#" - { - "Last": -1 - } - "#; - let _: ExposeOffset = serde_json::from_str(json).unwrap(); - json = r#" - { - "First": 1 - } - "#; - let _: ExposeOffset = serde_json::from_str(json).unwrap(); - } - - #[test] - fn test_circuit() { - let json = r#" - { - "step_types": { - "205524326356431126935662643926474033674": { - "id": 205524326356431126935662643926474033674, - "name": "fibo_step", - "signals": [ - { - "id": 205524332694684128074575021569884162570, - "annotation": "c" - } - ], - "constraints": [ - { - "annotation": "((a + b) == c)", - "expr": { - "Sum": [ - { - "Forward": [ - { - "id": 205524314472206749795829327634996267530, - "phase": 0, - "annotation": "a" - }, - false - ] - }, - { - "Forward": [ - { - "id": 205524322395023001221676493137926294026, - "phase": 0, - "annotation": "b" - }, - false - ] - }, - { - "Neg": { - "Internal": { - "id": 205524332694684128074575021569884162570, - "annotation": "c" - } - } - } - ] - } - } - ], - "transition_constraints": [ - { - "annotation": "(b == next(a))", - "expr": { - "Sum": [ - { - "Forward": [ - { - "id": 205524322395023001221676493137926294026, - "phase": 0, - "annotation": "b" - }, - false - ] - }, - { - "Neg": { - "Forward": [ - { - "id": 205524314472206749795829327634996267530, - "phase": 0, - "annotation": "a" - }, - true - ] - } - } - ] - } - }, - { - "annotation": "(c == next(b))", - "expr": { - "Sum": [ - { - "Internal": { - "id": 205524332694684128074575021569884162570, - "annotation": "c" - } - }, - { - "Neg": { - "Forward": [ - { - "id": 205524322395023001221676493137926294026, - "phase": 0, - "annotation": "b" - }, - true - ] - } - } - ] - } - } - ], - "annotations": { - "205524332694684128074575021569884162570": "c" - } - }, - "205524373893328635494146417612672338442": { - "id": 205524373893328635494146417612672338442, - "name": "fibo_last_step", - "signals": [ - { - "id": 205524377062455136063336753318874188298, - "annotation": "c" - } - ], - "constraints": [ - { - "annotation": "((a + b) == c)", - "expr": { - "Sum": [ - { - "Forward": [ - { - "id": 205524314472206749795829327634996267530, - "phase": 0, - "annotation": "a" - }, - false - ] - }, - { - "Forward": [ - { - "id": 205524322395023001221676493137926294026, - "phase": 0, - "annotation": "b" - }, - false - ] - }, - { - "Neg": { - "Internal": { - "id": 205524377062455136063336753318874188298, - "annotation": "c" - } - } - } - ] - } - } - ], - "transition_constraints": [], - "annotations": { - "205524377062455136063336753318874188298": "c" - } - } - }, - "forward_signals": [ - { - "id": 205524314472206749795829327634996267530, - "phase": 0, - "annotation": "a" - }, - { - "id": 205524322395023001221676493137926294026, - "phase": 0, - "annotation": "b" - } - ], - "shared_signals": [], - "fixed_signals": [], - "exposed": [ - [ - { - "Forward": [ - { - "id": 205524322395023001221676493137926294026, - "phase": 0, - "annotation": "b" - }, - false - ] - }, - { - "First": 0 - } - ], - [ - { - "Forward": [ - { - "id": 205524314472206749795829327634996267530, - "phase": 0, - "annotation": "a" - }, - false - ] - }, - { - "Last": -1 - } - ], - [ - { - "Forward": [ - { - "id": 205524314472206749795829327634996267530, - "phase": 0, - "annotation": "a" - }, - false - ] - }, - { - "Step": 1 - } - ] - ], - "annotations": { - "205524314472206749795829327634996267530": "a", - "205524322395023001221676493137926294026": "b", - "205524326356431126935662643926474033674": "fibo_step", - "205524373893328635494146417612672338442": "fibo_last_step" - }, - "first_step": 205524326356431126935662643926474033674, - "last_step": 205524373893328635494146417612672338442, - "num_steps": 0, - "q_enable": false, - "id": 205522563529815184552233780032226069002 - } - "#; - let circuit: Circuit = serde_json::from_str(json).unwrap(); - println!("{:?}", circuit); - } - - #[test] - fn test_step_type() { - let json = r#" - { - "id":1, - "name":"fibo", - "signals":[ - { - "id":1, - "annotation":"a" - }, - { - "id":2, - "annotation":"b" - } - ], - "constraints":[ - { - "annotation":"constraint", - "expr":{ - "Sum":[ - { - "Const":[1, 0, 0, 0] - }, - { - "Mul":[ - { - "Internal":{ - "id":3, - "annotation":"c" - } - }, - { - "Const":[3, 0, 0, 0] - } - ] - } - ] - } - }, - { - "annotation":"constraint", - "expr":{ - "Sum":[ - { - "Const":[1, 0, 0, 0] - }, - { - "Mul":[ - { - "Shared":[ - { - "id":4, - "phase":2, - "annotation":"d" - }, - 1 - ] - }, - { - "Const":[3, 0, 0, 0] - } - ] - } - ] - } - } - ], - "transition_constraints":[ - { - "annotation":"trans", - "expr":{ - "Sum":[ - { - "Const":[1, 0, 0, 0] - }, - { - "Mul":[ - { - "Forward":[ - { - "id":5, - "phase":1, - "annotation":"e" - }, - true - ] - }, - { - "Const":[3, 0, 0, 0] - } - ] - } - ] - } - }, - { - "annotation":"trans", - "expr":{ - "Sum":[ - { - "Const":[1, 0, 0, 0] - }, - { - "Mul":[ - { - "Fixed":[ - { - "id":6, - "annotation":"e" - }, - 2 - ] - }, - { - "Const":[3, 0, 0, 0] - } - ] - } - ] - } - } - ], - "annotations":{ - "5":"a", - "6":"b", - "7":"c" - } - } - "#; - let step_type: StepType = serde_json::from_str(json).unwrap(); - println!("{:?}", step_type); - } - - #[test] - fn test_constraint() { - let json = r#" - {"annotation": "constraint", - "expr": - { - "Sum": [ - { - "Internal": { - "id": 27, - "annotation": "a" - } - }, - { - "Fixed": [ - { - "id": 28, - "annotation": "b" - }, - 1 - ] - }, - { - "Shared": [ - { - "id": 29, - "phase": 1, - "annotation": "c" - }, - 2 - ] - }, - { - "Forward": [ - { - "id": 30, - "phase": 2, - "annotation": "d" - }, - true - ] - }, - { - "StepTypeNext": { - "id": 31, - "annotation": "e" - } - }, - { - "Const": [3, 0, 0, 0] - }, - { - "Mul": [ - { - "Const": [4, 0, 0, 0] - }, - { - "Const": [5, 0, 0, 0] - } - ] - }, - { - "Neg": { - "Const": [2, 0, 0, 0] - } - }, - { - "Pow": [ - { - "Const": [3, 0, 0, 0] - }, - 4 - ] - } - ] - } - }"#; - let constraint: Constraint = serde_json::from_str(json).unwrap(); - println!("{:?}", constraint); - let transition_constraint: TransitionConstraint = serde_json::from_str(json).unwrap(); - println!("{:?}", transition_constraint); - } - - #[test] - fn test_expr() { - let json = r#" - { - "Sum": [ - { - "Internal": { - "id": 27, - "annotation": "a" - } - }, - { - "Fixed": [ - { - "id": 28, - "annotation": "b" - }, - 1 - ] - }, - { - "Shared": [ - { - "id": 29, - "phase": 1, - "annotation": "c" - }, - 2 - ] - }, - { - "Forward": [ - { - "id": 30, - "phase": 2, - "annotation": "d" - }, - true - ] - }, - { - "StepTypeNext": { - "id": 31, - "annotation": "e" - } - }, - { - "Const": [3, 0, 0, 0] - }, - { - "Mul": [ - { - "Const": [4, 0, 0, 0] - }, - { - "Const": [5, 0, 0, 0] - } - ] - }, - { - "Neg": { - "Const": [2, 0, 0, 0] - } - }, - { - "Pow": [ - { - "Const": [3, 0, 0, 0] - }, - 4 - ] - } - ] - }"#; - let expr: Expr = serde_json::from_str(json).unwrap(); - println!("{:?}", expr); - } -} diff --git a/src/frontend/python/mod.rs b/src/frontend/python/mod.rs index c11d2c85..8e32e83b 100644 --- a/src/frontend/python/mod.rs +++ b/src/frontend/python/mod.rs @@ -1,14 +1,1424 @@ -use crate::{ - ast::Circuit, - frontend::pychiquito::{chiquito_ast_to_halo2, chiquito_halo2_mock_prover}, - wit_gen::TraceWitness, -}; -use halo2_proofs::halo2curves::bn256::Fr; use pyo3::{ prelude::*, types::{PyLong, PyString}, }; +use crate::{ + ast::{ + expr::{query::Queriable, Expr}, + Circuit, Constraint, ExposeOffset, FixedSignal, ForwardSignal, InternalSignal, + SharedSignal, StepType, StepTypeUUID, TransitionConstraint, + }, + frontend::dsl::StepTypeHandler, + plonkish::{ + backend::halo2::{chiquito2Halo2, ChiquitoHalo2, ChiquitoHalo2Circuit}, + compiler::{ + cell_manager::SingleRowCellManager, compile, config, + step_selector::SimpleStepSelectorBuilder, + }, + ir::assignments::AssignmentGenerator, + }, + util::{uuid, UUID}, + wit_gen::{StepInstance, TraceContext, TraceWitness}, +}; + +use core::result::Result; +use halo2_proofs::{dev::MockProver, halo2curves::bn256::Fr}; +use serde::de::{self, Deserialize, Deserializer, IgnoredAny, MapAccess, Visitor}; +use std::{cell::RefCell, collections::HashMap, fmt, rc::Rc}; + +type CircuitMapStore = (ChiquitoHalo2, Option>); +type CircuitMap = RefCell>; + +thread_local! { + pub static CIRCUIT_MAP: CircuitMap = RefCell::new(HashMap::new()); +} + +pub fn chiquito_ast_to_halo2(ast_json: &str) -> UUID { + let circuit: Circuit = + serde_json::from_str(ast_json).expect("Json deserialization to Circuit failed."); + + let config = config(SingleRowCellManager {}, SimpleStepSelectorBuilder {}); + let (chiquito, assignment_generator) = compile(config, &circuit); + let chiquito_halo2 = chiquito2Halo2(chiquito); + let uuid = uuid(); + + CIRCUIT_MAP.with(|circuit_map| { + circuit_map + .borrow_mut() + .insert(uuid, (chiquito_halo2, assignment_generator)); + }); + + println!("{:?}", uuid); + + uuid +} + +fn uuid_to_halo2(uuid: UUID) -> CircuitMapStore { + CIRCUIT_MAP.with(|circuit_map| { + let circuit_map = circuit_map.borrow(); + circuit_map.get(&uuid).unwrap().clone() + }) +} + +pub fn chiquito_halo2_mock_prover(witness_json: &str, ast_id: UUID) { + let trace_witness: TraceWitness = + serde_json::from_str(witness_json).expect("Json deserialization to TraceWitness failed."); + let (compiled, assignment_generator) = uuid_to_halo2(ast_id); + let circuit: ChiquitoHalo2Circuit<_> = ChiquitoHalo2Circuit::new( + compiled, + assignment_generator.map(|g| g.generate_with_witness(trace_witness)), + ); + + let prover = MockProver::::run(7, &circuit, circuit.instance()).unwrap(); + + let result = prover.verify_par(); + + println!("{:#?}", result); + + if let Err(failures) = &result { + for failure in failures.iter() { + println!("{}", failure); + } + } +} + +struct CircuitVisitor; + +impl<'de> Visitor<'de> for CircuitVisitor { + type Value = Circuit; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("struct Cricuit") + } + + fn visit_map(self, mut map: A) -> Result, A::Error> + where + A: MapAccess<'de>, + { + let mut step_types = None; + let mut forward_signals = None; + let mut shared_signals = None; + let mut fixed_signals = None; + let mut exposed = None; + let mut annotations = None; + let mut first_step = None; + let mut last_step = None; + let mut num_steps = None; + let mut q_enable = None; + let mut id = None; + + while let Some(key) = map.next_key::()? { + match key.as_str() { + "step_types" => { + if step_types.is_some() { + return Err(de::Error::duplicate_field("step_types")); + } + step_types = Some(map.next_value::>>()?); + } + "forward_signals" => { + if forward_signals.is_some() { + return Err(de::Error::duplicate_field("forward_signals")); + } + forward_signals = Some(map.next_value::>()?); + } + "shared_signals" => { + if shared_signals.is_some() { + return Err(de::Error::duplicate_field("shared_signals")); + } + shared_signals = Some(map.next_value::>()?); + } + "fixed_signals" => { + if fixed_signals.is_some() { + return Err(de::Error::duplicate_field("fixed_signals")); + } + fixed_signals = Some(map.next_value::>()?); + } + "exposed" => { + if exposed.is_some() { + return Err(de::Error::duplicate_field("exposed")); + } + exposed = Some(map.next_value::, ExposeOffset)>>()?); + } + "annotations" => { + if annotations.is_some() { + return Err(de::Error::duplicate_field("annotations")); + } + annotations = Some(map.next_value::>()?); + } + "first_step" => { + if first_step.is_some() { + return Err(de::Error::duplicate_field("first_step")); + } + first_step = Some(map.next_value::>()?); + } + "last_step" => { + if last_step.is_some() { + return Err(de::Error::duplicate_field("last_step")); + } + last_step = Some(map.next_value::>()?); + } + "num_steps" => { + if num_steps.is_some() { + return Err(de::Error::duplicate_field("num_steps")); + } + num_steps = Some(map.next_value::()?); + } + "q_enable" => { + if q_enable.is_some() { + return Err(de::Error::duplicate_field("q_enable")); + } + q_enable = Some(map.next_value::()?); + } + "id" => { + if id.is_some() { + return Err(de::Error::duplicate_field("id")); + } + id = Some(map.next_value()?); + } + _ => { + return Err(de::Error::unknown_field( + &key, + &[ + "step_types", + "forward_signals", + "shared_signals", + "fixed_signals", + "exposed", + "annotations", + "first_step", + "last_step", + "num_steps", + "q_enable", + "id", + ], + )) + } + } + } + let step_types = step_types + .ok_or_else(|| de::Error::missing_field("step_types"))? + .into_iter() + .map(|(k, v)| (k, Rc::new(v))) + .collect(); + let forward_signals = + forward_signals.ok_or_else(|| de::Error::missing_field("forward_signals"))?; + let shared_signals = + shared_signals.ok_or_else(|| de::Error::missing_field("shared_signals"))?; + let fixed_signals = + fixed_signals.ok_or_else(|| de::Error::missing_field("fixed_signals"))?; + let exposed = exposed.ok_or_else(|| de::Error::missing_field("exposed"))?; + let annotations = annotations.ok_or_else(|| de::Error::missing_field("annotations"))?; + let first_step = first_step.ok_or_else(|| de::Error::missing_field("first_step"))?; + let last_step = last_step.ok_or_else(|| de::Error::missing_field("last_step"))?; + let num_steps = num_steps.ok_or_else(|| de::Error::missing_field("num_steps"))?; + let q_enable = q_enable.ok_or_else(|| de::Error::missing_field("q_enable"))?; + let id = id.ok_or_else(|| de::Error::missing_field("id"))?; + + Ok(Circuit { + step_types, + forward_signals, + shared_signals, + fixed_signals, + halo2_advice: Default::default(), + halo2_fixed: Default::default(), + exposed, + num_steps, + annotations, + trace: Some(Rc::new(|_: &mut TraceContext<_>, _: _| {})), + fixed_gen: None, + first_step, + last_step, + q_enable, + id, + }) + } +} +struct StepTypeVisitor; + +impl<'de> Visitor<'de> for StepTypeVisitor { + type Value = StepType; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("struct StepType") + } + + fn visit_map(self, mut map: A) -> Result, A::Error> + where + A: MapAccess<'de>, + { + let mut id = None; + let mut name = None; + let mut signals = None; + let mut constraints = None; + let mut transition_constraints = None; + let mut annotations = None; + + while let Some(key) = map.next_key::()? { + match key.as_str() { + "id" => { + if id.is_some() { + return Err(de::Error::duplicate_field("id")); + } + id = Some(map.next_value()?); + } + "name" => { + if name.is_some() { + return Err(de::Error::duplicate_field("name")); + } + name = Some(map.next_value::()?); + } + "signals" => { + if signals.is_some() { + return Err(de::Error::duplicate_field("signals")); + } + signals = Some(map.next_value::>()?); + } + "constraints" => { + if constraints.is_some() { + return Err(de::Error::duplicate_field("constraints")); + } + constraints = Some(map.next_value::>>()?); + } + "transition_constraints" => { + if transition_constraints.is_some() { + return Err(de::Error::duplicate_field("transition_constraints")); + } + transition_constraints = + Some(map.next_value::>>()?); + } + "annotations" => { + if annotations.is_some() { + return Err(de::Error::duplicate_field("annotations")); + } + annotations = Some(map.next_value::>()?); + } + _ => { + return Err(de::Error::unknown_field( + &key, + &[ + "id", + "name", + "signals", + "constraints", + "transition_constraints", + "annotations", + ], + )) + } + } + } + let id = id.ok_or_else(|| de::Error::missing_field("id"))?; + let name = name.ok_or_else(|| de::Error::missing_field("name"))?; + let signals = signals.ok_or_else(|| de::Error::missing_field("signals"))?; + let constraints = constraints.ok_or_else(|| de::Error::missing_field("constraints"))?; + let transition_constraints = transition_constraints + .ok_or_else(|| de::Error::missing_field("transition_constraints"))?; + let annotations = annotations.ok_or_else(|| de::Error::missing_field("annotations"))?; + + let mut step_type = StepType::::new(id, name); + step_type.signals = signals; + step_type.constraints = constraints; + step_type.transition_constraints = transition_constraints; + step_type.lookups = Default::default(); + step_type.annotations = annotations; + + Ok(step_type) + } +} + +macro_rules! impl_visitor_constraint_transition { + ($name:ident, $type:ty, $display:expr) => { + struct $name; + + impl<'de> Visitor<'de> for $name { + type Value = $type; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str($display) + } + + fn visit_map(self, mut map: A) -> Result<$type, A::Error> + where + A: MapAccess<'de>, + { + let mut annotation = None; + let mut expr = None; + while let Some(key) = map.next_key::()? { + match key.as_str() { + "annotation" => { + if annotation.is_some() { + return Err(de::Error::duplicate_field("annotation")); + } + annotation = Some(map.next_value::()?); + } + "expr" => { + if expr.is_some() { + return Err(de::Error::duplicate_field("expr")); + } + expr = Some(map.next_value::>()?); + } + _ => return Err(de::Error::unknown_field(&key, &["annotation", "expr"])), + } + } + let annotation = + annotation.ok_or_else(|| de::Error::missing_field("annotation"))?; + let expr = expr.ok_or_else(|| de::Error::missing_field("expr"))?; + Ok(Self::Value { annotation, expr }) + } + } + }; +} + +impl_visitor_constraint_transition!(ConstraintVisitor, Constraint, "struct Constraint"); +impl_visitor_constraint_transition!( + TransitionConstraintVisitor, + TransitionConstraint, + "struct TransitionConstraint" +); + +struct ExprVisitor; + +impl<'de> Visitor<'de> for ExprVisitor { + type Value = Expr; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("enum Expr") + } + + fn visit_map(self, mut map: A) -> Result, A::Error> + where + A: MapAccess<'de>, + { + let key: String = map + .next_key()? + .ok_or_else(|| de::Error::custom("map is empty"))?; + match key.as_str() { + "Const" => map.next_value().map(Expr::Const), + "Sum" => map.next_value().map(Expr::Sum), + "Mul" => map.next_value().map(Expr::Mul), + "Neg" => map.next_value().map(Expr::Neg), + "Pow" => map.next_value().map(|(expr, pow)| Expr::Pow(expr, pow)), + "Internal" => map + .next_value() + .map(|signal| Expr::Query(Queriable::Internal(signal))), + "Forward" => map + .next_value() + .map(|(signal, rotation)| Expr::Query(Queriable::Forward(signal, rotation))), + "Shared" => map + .next_value() + .map(|(signal, rotation)| Expr::Query(Queriable::Shared(signal, rotation))), + "Fixed" => map + .next_value() + .map(|(signal, rotation)| Expr::Query(Queriable::Fixed(signal, rotation))), + "StepTypeNext" => map + .next_value() + .map(|step_type| Expr::Query(Queriable::StepTypeNext(step_type))), + _ => Err(de::Error::unknown_variant( + &key, + &[ + "Const", + "Sum", + "Mul", + "Neg", + "Pow", + "Internal", + "Forward", + "Shared", + "Fixed", + "StepTypeNext", + ], + )), + } + } +} + +struct QueriableVisitor; + +impl<'de> Visitor<'de> for QueriableVisitor { + type Value = Queriable; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("enum Queriable") + } + + fn visit_map(self, mut map: A) -> Result, A::Error> + where + A: MapAccess<'de>, + { + let key: String = map + .next_key()? + .ok_or_else(|| de::Error::custom("map is empty"))?; + match key.as_str() { + "Internal" => map.next_value().map(Queriable::Internal), + "Forward" => map + .next_value() + .map(|(signal, rotation)| Queriable::Forward(signal, rotation)), + "Shared" => map + .next_value() + .map(|(signal, rotation)| Queriable::Shared(signal, rotation)), + "Fixed" => map + .next_value() + .map(|(signal, rotation)| Queriable::Fixed(signal, rotation)), + "StepTypeNext" => map.next_value().map(Queriable::StepTypeNext), + _ => Err(de::Error::unknown_variant( + &key, + &["Internal", "Forward", "Shared", "Fixed", "StepTypeNext"], + )), + } + } +} + +struct ExposeOffsetVisitor; + +impl<'de> Visitor<'de> for ExposeOffsetVisitor { + type Value = ExposeOffset; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("enum ExposeOffset") + } + + fn visit_map(self, mut map: A) -> Result + where + A: MapAccess<'de>, + { + let key: String = map + .next_key()? + .ok_or_else(|| de::Error::custom("map is empty"))?; + match key.as_str() { + "First" => { + let _ = map.next_value::()?; + Ok(ExposeOffset::First) + } + "Last" => { + let _ = map.next_value::()?; + Ok(ExposeOffset::Last) + } + "Step" => map.next_value().map(ExposeOffset::Step), + _ => Err(de::Error::unknown_variant(&key, &["First", "Last", "Step"])), + } + } +} + +macro_rules! impl_visitor_internal_fixed_steptypehandler { + ($name:ident, $type:ty, $display:expr) => { + struct $name; + + impl<'de> Visitor<'de> for $name { + type Value = $type; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str($display) + } + + fn visit_map(self, mut map: A) -> Result<$type, A::Error> + where + A: MapAccess<'de>, + { + let mut id = None; + let mut annotation = None; + while let Some(key) = map.next_key::()? { + match key.as_str() { + "id" => { + if id.is_some() { + return Err(de::Error::duplicate_field("id")); + } + id = Some(map.next_value()?); + } + "annotation" => { + if annotation.is_some() { + return Err(de::Error::duplicate_field("annotation")); + } + annotation = Some(map.next_value::()?); + } + _ => return Err(de::Error::unknown_field(&key, &["id", "annotation"])), + } + } + let id = id.ok_or_else(|| de::Error::missing_field("id"))?; + let annotation = + annotation.ok_or_else(|| de::Error::missing_field("annotation"))?; + Ok(<$type>::new_with_id(id, annotation)) + } + } + }; +} + +impl_visitor_internal_fixed_steptypehandler!( + InternalSignalVisitor, + InternalSignal, + "struct InternalSignal" +); +impl_visitor_internal_fixed_steptypehandler!(FixedSignalVisitor, FixedSignal, "struct FixedSignal"); +impl_visitor_internal_fixed_steptypehandler!( + StepTypeHandlerVisitor, + StepTypeHandler, + "struct StepTypeHandler" +); + +macro_rules! impl_visitor_forward_shared { + ($name:ident, $type:ty, $display:expr) => { + struct $name; + + impl<'de> Visitor<'de> for $name { + type Value = $type; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str($display) + } + + fn visit_map(self, mut map: A) -> Result<$type, A::Error> + where + A: MapAccess<'de>, + { + let mut id = None; + let mut phase = None; + let mut annotation = None; + while let Some(key) = map.next_key::()? { + match key.as_str() { + "id" => { + if id.is_some() { + return Err(de::Error::duplicate_field("id")); + } + id = Some(map.next_value()?); + } + "phase" => { + if phase.is_some() { + return Err(de::Error::duplicate_field("phase")); + } + phase = Some(map.next_value()?); + } + "annotation" => { + if annotation.is_some() { + return Err(de::Error::duplicate_field("annotation")); + } + annotation = Some(map.next_value::()?); + } + _ => { + return Err(de::Error::unknown_field( + &key, + &["id", "phase", "annotation"], + )) + } + } + } + let id = id.ok_or_else(|| de::Error::missing_field("id"))?; + let phase = phase.ok_or_else(|| de::Error::missing_field("phase"))?; + let annotation = + annotation.ok_or_else(|| de::Error::missing_field("annotation"))?; + Ok(<$type>::new_with_id(id, phase, annotation)) + } + } + }; +} + +impl_visitor_forward_shared!(ForwardSignalVisitor, ForwardSignal, "struct ForwardSignal"); +impl_visitor_forward_shared!(SharedSignalVisitor, SharedSignal, "struct SharedSignal"); + +struct TraceWitnessVisitor; + +impl<'de> Visitor<'de> for TraceWitnessVisitor { + type Value = TraceWitness; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("struct TraceWitness") + } + + fn visit_map(self, mut map: A) -> Result, A::Error> + where + A: MapAccess<'de>, + { + let mut step_instances = None; + + while let Some(key) = map.next_key::()? { + match key.as_str() { + "step_instances" => { + if step_instances.is_some() { + return Err(de::Error::duplicate_field("step_instances")); + } + step_instances = Some(map.next_value()?); + } + _ => return Err(de::Error::unknown_field(&key, &["step_instances"])), + } + } + let step_instances = + step_instances.ok_or_else(|| de::Error::missing_field("step_instances"))?; + Ok(Self::Value { step_instances }) + } +} + +struct StepInstanceVisitor; + +impl<'de> Visitor<'de> for StepInstanceVisitor { + type Value = StepInstance; + + fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("struct StepInstance") + } + + fn visit_map(self, mut map: A) -> Result, A::Error> + where + A: MapAccess<'de>, + { + let mut step_type_uuid = None; + let mut assignments = None; + + while let Some(key) = map.next_key::()? { + match key.as_str() { + "step_type_uuid" => { + if step_type_uuid.is_some() { + return Err(de::Error::duplicate_field("step_type_uuid")); + } + step_type_uuid = Some(map.next_value()?); + } + "assignments" => { + if assignments.is_some() { + return Err(de::Error::duplicate_field("assignments")); + } + assignments = Some(map.next_value::, Fr)>>()?); + } + _ => { + return Err(de::Error::unknown_field( + &key, + &["step_type_uuid", "assignments"], + )) + } + } + } + let step_type_uuid = + step_type_uuid.ok_or_else(|| de::Error::missing_field("step_type_uuid"))?; + + let assignments: HashMap, Fr> = assignments + .ok_or_else(|| de::Error::missing_field("assignments"))? + .into_values() + .collect(); + + Ok(Self::Value { + step_type_uuid, + assignments, + }) + } +} + +macro_rules! impl_deserialize { + ($name:ident, $type:ty) => { + impl<'de> Deserialize<'de> for $type { + fn deserialize(deserializer: D) -> Result<$type, D::Error> + where + D: Deserializer<'de>, + { + deserializer.deserialize_map($name) + } + } + }; +} + +impl_deserialize!(ExprVisitor, Expr); +impl_deserialize!(QueriableVisitor, Queriable); +impl_deserialize!(ExposeOffsetVisitor, ExposeOffset); +impl_deserialize!(InternalSignalVisitor, InternalSignal); +impl_deserialize!(FixedSignalVisitor, FixedSignal); +impl_deserialize!(ForwardSignalVisitor, ForwardSignal); +impl_deserialize!(SharedSignalVisitor, SharedSignal); +impl_deserialize!(StepTypeHandlerVisitor, StepTypeHandler); +impl_deserialize!(ConstraintVisitor, Constraint); +impl_deserialize!(TransitionConstraintVisitor, TransitionConstraint); +impl_deserialize!(StepTypeVisitor, StepType); +impl_deserialize!(TraceWitnessVisitor, TraceWitness); +impl_deserialize!(StepInstanceVisitor, StepInstance); + +impl<'de> Deserialize<'de> for Circuit { + fn deserialize(deserializer: D) -> Result, D::Error> + where + D: Deserializer<'de>, + { + deserializer.deserialize_map(CircuitVisitor) + } +} + +#[cfg(test)] +mod tests { + use super::*; + #[test] + fn test_trace_witness() { + let json = r#" + { + "step_instances": [ + { + "step_type_uuid": 270606747459021742275781620564109167114, + "assignments": { + "270606737951642240564318377467548666378": [ + { + "Forward": [ + { + "id": 270606737951642240564318377467548666378, + "phase": 0, + "annotation": "a" + }, + false + ] + }, + [ + 55, + 0, + 0, + 0 + ] + ], + "270606743497613616562965561253747624458": [ + { + "Forward": [ + { + "id": 270606743497613616562965561253747624458, + "phase": 0, + "annotation": "b" + }, + false + ] + }, + [ + 89, + 0, + 0, + 0 + ] + ], + "270606753004993118272949371872716917258": [ + { + "Internal": { + "id": 270606753004993118272949371872716917258, + "annotation": "c" + } + }, + [ + 144, + 0, + 0, + 0 + ] + ] + } + }, + { + "step_type_uuid": 270606783111694873693576112554652600842, + "assignments": { + "270606737951642240564318377467548666378": [ + { + "Forward": [ + { + "id": 270606737951642240564318377467548666378, + "phase": 0, + "annotation": "a" + }, + false + ] + }, + [ + 89, + 0, + 0, + 0 + ] + ], + "270606743497613616562965561253747624458": [ + { + "Forward": [ + { + "id": 270606743497613616562965561253747624458, + "phase": 0, + "annotation": "b" + }, + false + ] + }, + [ + 144, + 0, + 0, + 0 + ] + ], + "270606786280821374261518951164072823306": [ + { + "Internal": { + "id": 270606786280821374261518951164072823306, + "annotation": "c" + } + }, + [ + 233, + 0, + 0, + 0 + ] + ] + } + } + ] + } + "#; + let trace_witness: TraceWitness = serde_json::from_str(json).unwrap(); + println!("{:?}", trace_witness); + } + + #[test] + fn test_expose_offset() { + let mut json = r#" + { + "Step": 1 + } + "#; + let _: ExposeOffset = serde_json::from_str(json).unwrap(); + json = r#" + { + "Last": -1 + } + "#; + let _: ExposeOffset = serde_json::from_str(json).unwrap(); + json = r#" + { + "First": 1 + } + "#; + let _: ExposeOffset = serde_json::from_str(json).unwrap(); + } + + #[test] + fn test_circuit() { + let json = r#" + { + "step_types": { + "205524326356431126935662643926474033674": { + "id": 205524326356431126935662643926474033674, + "name": "fibo_step", + "signals": [ + { + "id": 205524332694684128074575021569884162570, + "annotation": "c" + } + ], + "constraints": [ + { + "annotation": "((a + b) == c)", + "expr": { + "Sum": [ + { + "Forward": [ + { + "id": 205524314472206749795829327634996267530, + "phase": 0, + "annotation": "a" + }, + false + ] + }, + { + "Forward": [ + { + "id": 205524322395023001221676493137926294026, + "phase": 0, + "annotation": "b" + }, + false + ] + }, + { + "Neg": { + "Internal": { + "id": 205524332694684128074575021569884162570, + "annotation": "c" + } + } + } + ] + } + } + ], + "transition_constraints": [ + { + "annotation": "(b == next(a))", + "expr": { + "Sum": [ + { + "Forward": [ + { + "id": 205524322395023001221676493137926294026, + "phase": 0, + "annotation": "b" + }, + false + ] + }, + { + "Neg": { + "Forward": [ + { + "id": 205524314472206749795829327634996267530, + "phase": 0, + "annotation": "a" + }, + true + ] + } + } + ] + } + }, + { + "annotation": "(c == next(b))", + "expr": { + "Sum": [ + { + "Internal": { + "id": 205524332694684128074575021569884162570, + "annotation": "c" + } + }, + { + "Neg": { + "Forward": [ + { + "id": 205524322395023001221676493137926294026, + "phase": 0, + "annotation": "b" + }, + true + ] + } + } + ] + } + } + ], + "annotations": { + "205524332694684128074575021569884162570": "c" + } + }, + "205524373893328635494146417612672338442": { + "id": 205524373893328635494146417612672338442, + "name": "fibo_last_step", + "signals": [ + { + "id": 205524377062455136063336753318874188298, + "annotation": "c" + } + ], + "constraints": [ + { + "annotation": "((a + b) == c)", + "expr": { + "Sum": [ + { + "Forward": [ + { + "id": 205524314472206749795829327634996267530, + "phase": 0, + "annotation": "a" + }, + false + ] + }, + { + "Forward": [ + { + "id": 205524322395023001221676493137926294026, + "phase": 0, + "annotation": "b" + }, + false + ] + }, + { + "Neg": { + "Internal": { + "id": 205524377062455136063336753318874188298, + "annotation": "c" + } + } + } + ] + } + } + ], + "transition_constraints": [], + "annotations": { + "205524377062455136063336753318874188298": "c" + } + } + }, + "forward_signals": [ + { + "id": 205524314472206749795829327634996267530, + "phase": 0, + "annotation": "a" + }, + { + "id": 205524322395023001221676493137926294026, + "phase": 0, + "annotation": "b" + } + ], + "shared_signals": [], + "fixed_signals": [], + "exposed": [ + [ + { + "Forward": [ + { + "id": 205524322395023001221676493137926294026, + "phase": 0, + "annotation": "b" + }, + false + ] + }, + { + "First": 0 + } + ], + [ + { + "Forward": [ + { + "id": 205524314472206749795829327634996267530, + "phase": 0, + "annotation": "a" + }, + false + ] + }, + { + "Last": -1 + } + ], + [ + { + "Forward": [ + { + "id": 205524314472206749795829327634996267530, + "phase": 0, + "annotation": "a" + }, + false + ] + }, + { + "Step": 1 + } + ] + ], + "annotations": { + "205524314472206749795829327634996267530": "a", + "205524322395023001221676493137926294026": "b", + "205524326356431126935662643926474033674": "fibo_step", + "205524373893328635494146417612672338442": "fibo_last_step" + }, + "first_step": 205524326356431126935662643926474033674, + "last_step": 205524373893328635494146417612672338442, + "num_steps": 0, + "q_enable": false, + "id": 205522563529815184552233780032226069002 + } + "#; + let circuit: Circuit = serde_json::from_str(json).unwrap(); + println!("{:?}", circuit); + } + + #[test] + fn test_step_type() { + let json = r#" + { + "id":1, + "name":"fibo", + "signals":[ + { + "id":1, + "annotation":"a" + }, + { + "id":2, + "annotation":"b" + } + ], + "constraints":[ + { + "annotation":"constraint", + "expr":{ + "Sum":[ + { + "Const":[1, 0, 0, 0] + }, + { + "Mul":[ + { + "Internal":{ + "id":3, + "annotation":"c" + } + }, + { + "Const":[3, 0, 0, 0] + } + ] + } + ] + } + }, + { + "annotation":"constraint", + "expr":{ + "Sum":[ + { + "Const":[1, 0, 0, 0] + }, + { + "Mul":[ + { + "Shared":[ + { + "id":4, + "phase":2, + "annotation":"d" + }, + 1 + ] + }, + { + "Const":[3, 0, 0, 0] + } + ] + } + ] + } + } + ], + "transition_constraints":[ + { + "annotation":"trans", + "expr":{ + "Sum":[ + { + "Const":[1, 0, 0, 0] + }, + { + "Mul":[ + { + "Forward":[ + { + "id":5, + "phase":1, + "annotation":"e" + }, + true + ] + }, + { + "Const":[3, 0, 0, 0] + } + ] + } + ] + } + }, + { + "annotation":"trans", + "expr":{ + "Sum":[ + { + "Const":[1, 0, 0, 0] + }, + { + "Mul":[ + { + "Fixed":[ + { + "id":6, + "annotation":"e" + }, + 2 + ] + }, + { + "Const":[3, 0, 0, 0] + } + ] + } + ] + } + } + ], + "annotations":{ + "5":"a", + "6":"b", + "7":"c" + } + } + "#; + let step_type: StepType = serde_json::from_str(json).unwrap(); + println!("{:?}", step_type); + } + + #[test] + fn test_constraint() { + let json = r#" + {"annotation": "constraint", + "expr": + { + "Sum": [ + { + "Internal": { + "id": 27, + "annotation": "a" + } + }, + { + "Fixed": [ + { + "id": 28, + "annotation": "b" + }, + 1 + ] + }, + { + "Shared": [ + { + "id": 29, + "phase": 1, + "annotation": "c" + }, + 2 + ] + }, + { + "Forward": [ + { + "id": 30, + "phase": 2, + "annotation": "d" + }, + true + ] + }, + { + "StepTypeNext": { + "id": 31, + "annotation": "e" + } + }, + { + "Const": [3, 0, 0, 0] + }, + { + "Mul": [ + { + "Const": [4, 0, 0, 0] + }, + { + "Const": [5, 0, 0, 0] + } + ] + }, + { + "Neg": { + "Const": [2, 0, 0, 0] + } + }, + { + "Pow": [ + { + "Const": [3, 0, 0, 0] + }, + 4 + ] + } + ] + } + }"#; + let constraint: Constraint = serde_json::from_str(json).unwrap(); + println!("{:?}", constraint); + let transition_constraint: TransitionConstraint = serde_json::from_str(json).unwrap(); + println!("{:?}", transition_constraint); + } + + #[test] + fn test_expr() { + let json = r#" + { + "Sum": [ + { + "Internal": { + "id": 27, + "annotation": "a" + } + }, + { + "Fixed": [ + { + "id": 28, + "annotation": "b" + }, + 1 + ] + }, + { + "Shared": [ + { + "id": 29, + "phase": 1, + "annotation": "c" + }, + 2 + ] + }, + { + "Forward": [ + { + "id": 30, + "phase": 2, + "annotation": "d" + }, + true + ] + }, + { + "StepTypeNext": { + "id": 31, + "annotation": "e" + } + }, + { + "Const": [3, 0, 0, 0] + }, + { + "Mul": [ + { + "Const": [4, 0, 0, 0] + }, + { + "Const": [5, 0, 0, 0] + } + ] + }, + { + "Neg": { + "Const": [2, 0, 0, 0] + } + }, + { + "Pow": [ + { + "Const": [3, 0, 0, 0] + }, + 4 + ] + } + ] + }"#; + let expr: Expr = serde_json::from_str(json).unwrap(); + println!("{:?}", expr); + } +} + #[pyfunction] fn convert_and_print_ast(json: &PyString) { let circuit: Circuit = From 4f63fd039172a901f00f2b54dd96565db912ab5c Mon Sep 17 00:00:00 2001 From: trangnv Date: Mon, 21 Aug 2023 14:31:12 +0700 Subject: [PATCH 6/7] add tutorials --- tutorials/tutorial_pt1.ipynb | 47 ++++ tutorials/tutorial_pt2.ipynb | 57 ++++ tutorials/tutorial_pt3_ch1.ipynb | 89 ++++++ tutorials/tutorial_pt3_ch2.ipynb | 450 +++++++++++++++++++++++++++++++ tutorials/tutorial_pt3_ch3.ipynb | 245 +++++++++++++++++ 5 files changed, 888 insertions(+) create mode 100644 tutorials/tutorial_pt1.ipynb create mode 100644 tutorials/tutorial_pt2.ipynb create mode 100644 tutorials/tutorial_pt3_ch1.ipynb create mode 100644 tutorials/tutorial_pt3_ch2.ipynb create mode 100644 tutorials/tutorial_pt3_ch3.ipynb diff --git a/tutorials/tutorial_pt1.ipynb b/tutorials/tutorial_pt1.ipynb new file mode 100644 index 00000000..a6d5ec1f --- /dev/null +++ b/tutorials/tutorial_pt1.ipynb @@ -0,0 +1,47 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "0d703199-2067-4ebc-b6ed-b04470587279", + "metadata": {}, + "source": [ + "# Part 1: Introduction to Chiquito and PyChiquito\n", + "\n", + "Chiquito is a high-level structured language for implementing zero knowledge proof applications, currently being implemented in the DSL Working Group of PSE, Ethereum Foundation. It is a step-based zkDSL (zero knowledge domain specific language) that provides better syntax and abstraction for features like constraint building and column placement when writing PLONKish circuits, which supports custom gates and lookup arguments. Chiquito has a Halo2 backend, which is a low level zkDSL that writes circuits using the PLONKish arithemtization. Chiquito is working on supporting additional backends.\n", + "\n", + "Chiquito comes in two flavors: ChiquitoCore (Rust) and PyChiquito (Python). This tutorial focuses on PyChiquito.\n", + "\n", + "[PyChiquito](https://github.com/qwang98/PyChiquito) is the Python front end of ChiquitoCore. It exposes Python functions that user writes circuits with. [ChiquitoCore](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 Chiquito/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 Chiquito/PyChiquito, refer to [What is Chiquito?](https://hackmd.io/h6innd6RTwex4aBExignhw), [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)." + ] + } + ], + "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/tutorials/tutorial_pt2.ipynb b/tutorials/tutorial_pt2.ipynb new file mode 100644 index 00000000..d76ea966 --- /dev/null +++ b/tutorials/tutorial_pt2.ipynb @@ -0,0 +1,57 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "11105438-f775-4ff5-a91c-b236aedd9eb1", + "metadata": {}, + "source": [ + "# 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", + "\n", + "```\n", + "python3 -m venv .env\n", + "\n", + "source .env/bin/activate\n", + "\n", + "pip install maturin\n", + "pip install py_ecc\n", + "\n", + "maturin develop\n", + "```\n", + "\n", + "Now, run the following in your local command line to navigate to the `PyChiquito/pychiquito` directory which contains all the Python files. Install Jupyter Lab if you haven't. Then install your local Python virtual environment that's already setup as a Jupyter Lab Kernel called `pychiquito_kernel`. After that, activate Jupyter Lab. Finally, in the browser, navigate to `tutorial_pt3_ch1.ipynb` to start using the interactive part of this tutorial. Make sure you are using the Jupyter Lab Kernel called `pychiquito_kernel`, which you can change by going to the `Kernel` tab of Jupyter Lab's top menu bar and click `Change Kernel...`\n", + "\n", + "```\n", + "cd pychiquito\n", + "\n", + "pip install jupyterlab\n", + "python -m ipykernel install --user --name=pychiquito_kernel\n", + "jupyter lab\n", + "```" + ] + } + ], + "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/tutorials/tutorial_pt3_ch1.ipynb b/tutorials/tutorial_pt3_ch1.ipynb new file mode 100644 index 00000000..1f9abf00 --- /dev/null +++ b/tutorials/tutorial_pt3_ch1.ipynb @@ -0,0 +1,89 @@ +{ + "cells": [ + { + "attachments": {}, + "cell_type": "markdown", + "id": "14a9a617-1c05-40c8-b4ef-3cc2fbcf99fe", + "metadata": {}, + "source": [ + "# Part 3: Fibonacci Example\n", + "The best learning is by doing, In this Chapter, we will walk through the [fibonacci.py](https://github.com/qwang98/PyChiquito/blob/main/pychiquito/fibonacci.py) example.\n", + "# Chapter 1: Fibonacci and Chiquito Concepts\n", + "The Fibonacci series is an infinite series, starting from \"1\" and \"1\", in which every number in the series is the sum of two numbers preceding it in the series. The first few rounds for the Fibonacci series are:\n", + "- 1 + 1 = 2\n", + "- 1 + 2 = 3\n", + "- 2 + 3 = 5\n", + "- 3 + 5 = 8\n", + "\n", + "Therefore, to express these mathematical equations, we need three variables \"a\", \"b\", and \"c\", which we call \"signals\" in Chiquito. Because zero knowledge proofs typically express mathematical equations in the matrix form, we construct the following table:\n", + "\n", + "||Signals||\n", + "| :-: | :-: | :-: |\n", + "| a | b | c |\n", + "| 1 | 1 | 2 |\n", + "| 1 | 2 | 3 |\n", + "| 2 | 3 | 5 |\n", + "| 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", + "- a + b == c\n", + "- b = a in the next row\n", + "- c = b in the next row\n", + "\n", + "||Signals|||Setups||\n", + "| :-: | :-: | :-: | :-: | :-: | :-: |\n", + "| a | b | c | constraint 1 | constraint 2 | constraint 3 |\n", + "| 1 | 1 | 2 | a + b == c | b == a.next | c == b.next |\n", + "| 1 | 2 | 3 | a + b == c | b == a.next | c == b.next |\n", + "| 2 | 3 | 5 | a + b == c | b == a.next | c == b.next |\n", + "| 3 | 5 | 8 | a + b == c | b == a.next | c == b.next |\n", + "|| ... ||| ... ||\n", + "\n", + "Chiquito is a step-based language for constructing zero knowledge circuits, which means that instead of expressing all signals and constraints above as one entirety, we separate them into smaller chunks, called \"step instances\". In this example, each row, together with its signals and constraints, are collectively called a \"step instance\". We add indices for these step instances to the table, starting from 0:\n", + "\n", + "| Step Instance Index || Signals ||| Setups ||\n", + "| :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n", + "|| a | b | c | constraint 1 | constraint 2 | constraint 3 |\n", + "| 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next |\n", + "| 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next |\n", + "| 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next |\n", + "| 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next |\n", + "| ... || ... ||| ... ||\n", + "\n", + "Note that these 4 step instances share the same signals and constraints, although not the same value assignments for signals. They are essentially different instantiations of the same signals and constraints, or different \"step instances\" of the same \"step type\". In Chiquito, we define signals and constraints in \"step types\" and we generate \"witness assignments\" for signal values. \"Step types\" with \"witness assignments\" become \"step instances\". In the example above, we have 4 step instances but only 1 step type, defined as the same 3 signals and 3 constraints. For simplicity, we call this single step type \"fibo step\", also added to the table below:\n", + "| Step Type | Step Instance Index || Signals ||| Setups ||\n", + "| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n", + "||| a | b | c | constraint 1 | constraint 2 | constraint 3 |\n", + "| fibo step | 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next |\n", + "| fibo step | 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next |\n", + "| fibo step | 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next |\n", + "| fibo step | 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next |\n", + "| ... | ... || ... ||| ... ||\n", + "\n", + "As a recap, to construct a Fibonacci circuit, we need three signals-\"a\", \"b\", and \"c\". In Chiquito, \"circuit\" is a set of constraints that signals of the circuit need to satisfy. Each Chiquito circuit is composed of multiple \"step instances\", which are instantiations of \"step types\". Each \"step type\" contains a subset of signals and constraints that these signals need to satisfy. " + ] + } + ], + "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/tutorials/tutorial_pt3_ch2.ipynb b/tutorials/tutorial_pt3_ch2.ipynb new file mode 100644 index 00000000..a763a729 --- /dev/null +++ b/tutorials/tutorial_pt3_ch2.ipynb @@ -0,0 +1,450 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "8ab5d5e4-6d9e-4856-ad0b-0e2cf7bb13fb", + "metadata": {}, + "source": [ + "# 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" + ] + }, + { + "cell_type": "markdown", + "id": "081fd1f7-ba9e-471a-8b10-ff54a9257539", + "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", + "- Field element `F` from utils." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "bf77f66c-2e81-4b51-b7f1-24c1be6c9b99", + "metadata": {}, + "outputs": [], + "source": [ + "from chiquito.dsl import Circuit, StepType\n", + "from chiquito.cb import eq\n", + "from chiquito.util import F" + ] + }, + { + "attachments": {}, + "cell_type": "markdown", + "id": "de1bb748-3e94-42ea-9bad-689d5da0d468", + "metadata": {}, + "source": [ + "## StepType\n", + "Before putting everything together into a circuit, we need to define the step types first. Remember that the Fibonacci circuit is composed of one single step type, defined as 3 signals \"a\", \"b\", and \"c\", plus three constraints `a + b == c`, `b == a.next`, and `c == b.next`, where \"next\" means the same signal in the next step instance:\n", + "\n", + "| Step Type | Step Instance Index || Signals ||| Setups ||\n", + "| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n", + "||| a | b | c | constraint 1 | constraint 2 | constraint 3 |\n", + "| fibo step | 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next |\n", + "| fibo step | 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next |\n", + "| fibo step | 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next |\n", + "| fibo step | 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next |\n", + "| ... | ... || ... ||| ... ||\n", + "\n", + "PyChiquito provides a `StepType` parent class that we can customarily inherit. For each `StepType`, we need to define two functions:\n", + "- `setup`, which defines constraints using signals\n", + "- `wg`, which defines witness assignment for the step type\n", + "\n", + "## Signal Types\n", + "Now, a bit more on the signals. In Chiquito, there are signals that we can only query for the current step instance, which we call \"internal signals\". There are also signals that we can query for non-current step instances, such as the next step instance, which we call \"forward signals\". In the example above, \"a\" and \"b\" were both queried at the next step instance as `a.next` and `b.next` respectively, and therefore are \"forward signals\". \"c\" is only ever queried at the current step instance, and therefore is called \"internal signal\". In Chiquito, querying to a non-current step instance is also referred to as \"rotation\", which is a positive or negative number relative to the current step instance. We can call `next` on a forward signal, implying a rotation of `+1`. There are additional Chiquito signal types, such as \"shared signal\" and \"fixed signal\", which allows for arbitrary positive or negative rotation. However, in this Fibonacci example, we will only use forward signals \"a\" and \"b\" as well as internal signal \"c\".\n", + "\n", + "## FiboStep Setup\n", + "We now define the only step type, `FiboStep`:\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):\n", + " # TODO\n", + "```\n", + "Here, \"c\" is defined using `self.internal` as an internal signal that's only queried within a `FiboStep` instance. We didn't define \"a\" and \"b\", as they are forward signals which Chiquito defines on the circuit-level. More on that later.\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 queried within a step type instance, 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 above, forward signals \"a\" and \"b\" are expressed as `self.circuit.a` and `self.circuit.b`, whereas internal signal \"c\" is expressed as `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. It builds the three constraints of `FiboStep`: `a + b == c`, `b == a.next`, and `c == b.next`.\n", + "\n", + "## FiboStep Witness Generation\n", + "```\n", + "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))\n", + "```\n", + "In the example above, `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\".\n", + "\n", + "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.\n", + "\n", + "Putting everything for `FiboStep` together, we have:\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", + "\n", + "## Circuit\n", + "Now that we finished constructing the only step type `FiboStep`, we can build a `Circuit` object in PyChiquito. PyChiquito provides a `Circuit` parent class that we can customarily inherit. For each `Circuit`, we need to define two functions:\n", + "- `setup`, which configures the circuit with signals and step types.\n", + "- `trace`, which instantiates step types and defines the trace of assigning witness values.\n", + "\n", + "## Circuit Setup\n", + "We first define the circuit `setup`:\n", + "```\n", + "class Fibonacci(Circuit):\n", + " def setup(self):\n", + " self.a = self.forward(\"a\")\n", + " self.b = self.forward(\"b\")\n", + " \n", + " self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n", + "\n", + " def trace(self):\n", + " # TODO\n", + "```\n", + "Remember that previously we already added internal signal \"c\" to `FiboStep`. Now we add two forward signals \"a\" and \"b\" to the circuit-level. We append these signals to the circuit by defining them as `self.a` and `self.b`. Forward signals are created using `self.forward`.\n", + "\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", + "## Circuit Trace\n", + "Now we instantiate step types and assign witness values using `trace`:\n", + "```\n", + "class Fibonacci(Circuit):\n", + " def setup(self):\n", + " # ...\n", + " \n", + " def trace(self, args):\n", + " self.add(self.fibo_step, (1, 1))\n", + " a = 1\n", + " b = 2\n", + " for i in range(1, 4):\n", + " self.add(self.fibo_step, (a, b))\n", + " prev_a = a\n", + " a = b\n", + " b += prev_a\n", + "```\n", + "`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", + "\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", + "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, + "id": "d7c21e5d-5a9c-47b8-8c18-ed59fe885709", + "metadata": {}, + "outputs": [], + "source": [ + "class FiboStep(StepType):\n", + " def setup(self):\n", + " self.c = self.internal(\"c\")\n", + " self.constr(eq(self.circuit.a + self.circuit.b, self.c))\n", + " self.transition(eq(self.circuit.b, self.circuit.a.next()))\n", + " self.transition(eq(self.c, self.circuit.b.next()))\n", + "\n", + " def wg(self, args):\n", + " a_value, b_value = args\n", + " self.assign(self.circuit.a, F(a_value))\n", + " self.assign(self.circuit.b, F(b_value))\n", + " self.assign(self.c, F(a_value + b_value))\n", + "\n", + "class Fibonacci(Circuit):\n", + " def setup(self):\n", + " self.a = self.forward(\"a\")\n", + " self.b = self.forward(\"b\")\n", + " \n", + " self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n", + " \n", + " def trace(self, args):\n", + " self.add(self.fibo_step, (1, 1))\n", + " a = 1\n", + " b = 2\n", + " for i in range(1, 4):\n", + " self.add(self.fibo_step, (a, b))\n", + " prev_a = a\n", + " a = b\n", + " b += prev_a" + ] + }, + { + "cell_type": "markdown", + "id": "ca7b3167-e811-4427-9151-a85eaed20cb3", + "metadata": {}, + "source": [ + "## Putting Everything Together\n", + "Everything we went through above defines how the circuit and its step type are configured and witness values assigned to them. To instantiate the circuit, we call the class constructor:" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "c0c9db95-8da8-49d6-a403-895491c833fe", + "metadata": {}, + "outputs": [], + "source": [ + "fibo = Fibonacci()" + ] + }, + { + "cell_type": "markdown", + "id": "cba8d58a-81b6-449b-aa02-b54fa9b076c4", + "metadata": {}, + "source": [ + "You can also print the circuit. In the print out, you will see the single step type `FiboStep` and two forward signals \"a\" and \"b\" at the circuit-level. Within `FiboStep`, you will see one internal signal \"c\" and the 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": "d259b3b8-a15c-416c-9076-24c06f5b22e6", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "ASTCircuit(\n", + "\tstep_types={\n", + "\t\t175487786213455723101965983777064356362: ASTStepType(\n", + "\t\t\tid=175487786213455723101965983777064356362,\n", + "\t\t\tname='fibo_step',\n", + "\t\t\tsignals=[\n", + "\t\t\t\tInternalSignal(id=175487817112439103662857355366257789450, 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\t175487817112439103662857355366257789450: 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],\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},\n", + "\tfixed_gen=None,\n", + "\tfirst_step=None,\n", + "\tlast_step=None,\n", + "\tnum_steps=0\n", + "\tq_enable=True\n", + ")\n" + ] + } + ], + "source": [ + "print(fibo)" + ] + }, + { + "cell_type": "markdown", + "id": "a2358ce7-8192-4dc5-971e-1314d287ae3b", + "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": "24a0d3d8-710e-42fe-99ae-7491b50d7cd7", + "metadata": {}, + "outputs": [], + "source": [ + "fibo_witness = fibo.gen_witness(None)" + ] + }, + { + "cell_type": "markdown", + "id": "f4762085-fa23-4e39-9380-e816cdf4eaaa", + "metadata": {}, + "source": [ + "Again, you can print the witness assignments:" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "d1aaca8a-35eb-4c9d-8794-56869f696849", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "TraceWitness(\n", + "\tstep_instances={\n", + "\t\tStepInstance(\n", + "\t\t\tstep_type_uuid=175487786213455723101965983777064356362,\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=175487786213455723101965983777064356362,\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=175487786213455723101965983777064356362,\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=175487786213455723101965983777064356362,\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},\n", + ")\n" + ] + } + ], + "source": [ + "print(fibo_witness)" + ] + }, + { + "cell_type": "markdown", + "id": "f8937921-d923-4802-bc52-b3dbadb53c73", + "metadata": {}, + "source": [ + "Finally, we can generate and verify proof with the witness using the Halo2 mock prover. The print out includes Halo2 and ChiquitoCore debug messages. `Ok(())` means that proof was correctly generated and verified for the witness and circuit. `Err()` prints out Halo2 and ChiquitoCore error messages, usually because some constraints in the circuit were not satisfied. Here, you should see the `Ok(())` print out." + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "a3f8d245-adab-4e68-9ee6-5f6bafc12bd1", + "metadata": {}, + "outputs": [ + { + "name": "stderr", + "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" + ] + } + ], + "source": [ + "fibo.halo2_mock_prover(fibo_witness)" + ] + }, + { + "cell_type": "markdown", + "id": "fa056c5c-95b0-44c7-9566-c030ac071cf3", + "metadata": {}, + "source": [ + "Congratulations! Now you finished writing your first Fibonacci circuit and learned about the most essential concepts behind the step-based design of Chiquito, which simply combines step instances into a circuit! With abstraction, composability, modularity, and smooth user experience as the key tenets, writing Halo2 circuits has never been easier with PyChiquito!\n", + "\n", + "Next up, in Chapter 3, you will learn about testing your circuit with multiple different witnesses." + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": ".env", + "language": "python", + "name": "python3" + }, + "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/tutorials/tutorial_pt3_ch3.ipynb b/tutorials/tutorial_pt3_ch3.ipynb new file mode 100644 index 00000000..872bfab7 --- /dev/null +++ b/tutorials/tutorial_pt3_ch3.ipynb @@ -0,0 +1,245 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "aab29f93-4311-4bff-a123-38f412556922", + "metadata": {}, + "source": [ + "# Part 3: Fibonacci Example\n", + "# Chapter 3: Witness\n", + "Now, we will generate multiple witnesses to test the soundness of our circuit constraints. Note that we only intend to accept the following set of values for signals \"a\", \"b\", and \"c\". \"Soundness\" in this context refers to faulty witness successfully verified against the constraints (false positives), so any set of witness assignments that is different from the table below but still passes the constraints incurs a \"soundness\" error.\n", + "| Step Type | Step Instance Index || Signals ||| Setups ||\n", + "| :-: | :-: | :-: | :-: | :-: | :-: | :-: | :-: |\n", + "||| a | b | c | constraint 1 | constraint 2 | constraint 3 |\n", + "| fibo step | 0 | 1 | 1 | 2 | a + b == c | b == a.next | c == b.next |\n", + "| fibo step | 1 | 1 | 2 | 3 | a + b == c | b == a.next | c == b.next |\n", + "| fibo step | 2 | 2 | 3 | 5 | a + b == c | b == a.next | c == b.next |\n", + "| fibo step | 3 | 3 | 5 | 8 | a + b == c | b == a.next | c == b.next |\n", + "| ... | ... || ... ||| ... ||\n", + "\n", + "## Setup\n", + "We setup the same circuit and witness in Part 1 which were successfully verified:" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "e0114f48-0fe6-4141-b29e-63bc07411092", + "metadata": {}, + "outputs": [ + { + "name": "stderr", + "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" + ] + } + ], + "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", + "\n", + "class FiboStep(StepType):\n", + " def setup(self):\n", + " self.c = self.internal(\"c\")\n", + " self.constr(eq(self.circuit.a + self.circuit.b, self.c))\n", + " self.transition(eq(self.circuit.b, self.circuit.a.next()))\n", + " self.transition(eq(self.c, self.circuit.b.next()))\n", + "\n", + " def wg(self, args):\n", + " a_value, b_value = args\n", + " self.assign(self.circuit.a, F(a_value))\n", + " self.assign(self.circuit.b, F(b_value))\n", + " self.assign(self.c, F(a_value + b_value))\n", + "\n", + "class Fibonacci(Circuit):\n", + " def setup(self):\n", + " self.a = self.forward(\"a\")\n", + " self.b = self.forward(\"b\")\n", + " \n", + " self.fibo_step = self.step_type(FiboStep(self, \"fibo_step\"))\n", + " \n", + " def trace(self, args):\n", + " self.add(self.fibo_step, (1, 1))\n", + " a = 1\n", + " b = 2\n", + " for i in range(1, 4):\n", + " self.add(self.fibo_step, (a, b))\n", + " prev_a = a\n", + " a = b\n", + " b += prev_a\n", + "\n", + "fibo = Fibonacci()\n", + "fibo_witness = fibo.gen_witness(None)\n", + "fibo.halo2_mock_prover(fibo_witness)" + ] + }, + { + "cell_type": "markdown", + "id": "182101e0-f5ee-4c16-a7c1-d09909dcbb3b", + "metadata": {}, + "source": [ + "Now we swap the first step instance from `(1, 1, 2)` to `(0, 2, 2)`. We use the `evil_witness` function to swap step index 0 assignment index 0 to `F(0)` and step index 0 assignment index 0 to `F(2)`." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "4e1481de-fa95-4022-9771-66aae4fe842c", + "metadata": {}, + "outputs": [], + "source": [ + "evil_witness = fibo_witness.evil_witness_test(step_instance_indices=[0, 0], assignment_indices=[0, 1], rhs=[F(0), F(2)])" + ] + }, + { + "cell_type": "markdown", + "id": "19c5a476-e31e-4bc6-9bb2-7635c16b37ba", + "metadata": {}, + "source": [ + "Print the `evil_witness` to confirm that the swap was successful:" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "dcd26089-ecb0-4a5e-8296-318a7b644b98", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "TraceWitness(\n", + "\tstep_instances={\n", + "\t\tStepInstance(\n", + "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\n", + "\t\t\tassignments={\n", + "\t\t\t\ta = 0,\n", + "\t\t\t\tb = 2,\n", + "\t\t\t\tc = 2\n", + "\t\t\t},\n", + "\t\t),\n", + "\t\tStepInstance(\n", + "\t\t\tstep_type_uuid=82722411778406487845332704800562350602,\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=82722411778406487845332704800562350602,\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=82722411778406487845332704800562350602,\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},\n", + ")\n" + ] + } + ], + "source": [ + "print(evil_witness)" + ] + }, + { + "cell_type": "markdown", + "id": "52508cf9-6b61-4838-9f37-a2ed5d4e1dbd", + "metadata": {}, + "source": [ + "Now, generate and verify the proof with `evil_witness`:" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "044e067e-77fa-4027-94dd-e39a35e87de8", + "metadata": {}, + "outputs": [ + { + "name": "stderr", + "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" + ] + } + ], + "source": [ + "fibo.halo2_mock_prover(evil_witness)" + ] + }, + { + "cell_type": "markdown", + "id": "7329efe2-c60f-4e4a-9288-27cab5af827f", + "metadata": {}, + "source": [ + "Surprisingly, `evil_witness` generated a proof that passed verification. This constitutes a soundness error, because the first step instance isn't `(1, 1, 2)` as we initially specified, so why can the witness still pass the constraints?\n", + "\n", + "The answer is simple, because in the first step instance, we never constrained the values of \"a\" and \"b\" to 1 and 1 in `setup` of `FiboStep`. We also didn't constrain the first step instance to be `FiboStep`.\n", + "\n", + "You might be wondering: in `trace`, didn't we set \"a\" and \"b\" to `(1, 1)` and added `FiboStep` as the first step instance? In fact, `trace` and `wg` are really helper functions for the prover to easily generate a witness, whose data can be tampered with as shown in `evil_witness_test`. The only conditions enforced are defined in circuit and step type `setup`. Therefore, to fix the soundness error, we need to add more constraints, in Chapter 4." + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "pychiquito_kernel", + "language": "python", + "name": "pychiquito_kernel" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.11.4" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} From b6df58fa3d4e96087506dd10f4ea2aa2d6c66979 Mon Sep 17 00:00:00 2001 From: trangnv Date: Mon, 21 Aug 2023 14:35:08 +0700 Subject: [PATCH 7/7] add make build --- Makefile | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index a7ef69a6..26747673 100644 --- a/Makefile +++ b/Makefile @@ -4,4 +4,8 @@ precommit: cargo clippy --all-targets --all-features -- -D warnings cargo fmt --all -- --check -.PHONY: precommit +build: + cargo build + maturin develop + +.PHONY: precommit build