Bring (py)Chiquito in

.gitignore

@@ -1,3 +1,6 @@
 /target
 /Cargo.lock
 .vscode
+.env
+__pycache__
+*.so

Cargo.toml

@@ -8,10 +8,13 @@ authors = ["Leo Lara <[email protected]>"]
 # 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"] }

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,29 +24,53 @@ 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
 ```
 
 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

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)

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)."
+        )