Skip to content

Commit

Permalink
Merge pull request #2 from nalinbhardwaj/nibnalin/devops
Browse files Browse the repository at this point in the history 
Poetry, black, mypy
  • Loading branch information
@therealyingtong
therealyingtong authored Jan 22, 2023
2 parents 9cd1a82 + a795d58 commit ab6b185
Show file tree
Hide file tree
Showing 14 changed files with 1,080 additions and 453 deletions.
75 changes: 40 additions & 35 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,12 @@ The parts of PlonK that are responsible for ensuring strong privacy are left out
A lookup argument allows us to prove that a certain element can be found in a public lookup table. [PlonKup](https://eprint.iacr.org/2022/086.pdf) introduces lookup arguments to PlonK. Try to understand the construction in the paper and implement it here.

## Getting started
To see the proof system in action, run `python3 test.py` from the root of the repository. This will take you through the workflow of setup, proof generation, and verification for several example programs.

To get started, you'll need to have a Python version >= 3.8 and [`poetry`](https://python-poetry.org) installed: `curl -sSL https://install.python-poetry.org | python3 -`.

Then, run `poetry install` in the root of the repository. This will install all the dependencies in a virtualenv.

Then, to see the proof system in action, run `poetry run python test.py` from the root of the repository. This will take you through the workflow of setup, proof generation, and verification for several example programs.
### Compiler
#### Program
We specify our program logic in a high-level language involving constraints and variable assignments. Here is a program that lets you prove that you know two small numbers that multiply to a given number (in our example we'll use 91) without revealing what those numbers are:
Expand Down Expand Up @@ -68,11 +73,11 @@ class GateWires:
```

Examples of valid program constraints, and corresponding assembly:
| program constraint | assembly |
|--------------------------|-------------------------------------------------|
|a === 9 | ([None, None, 'a'], {'': 9}) |
|b <== a * c | (['a', 'c', 'b'], {'a*c': 1}) |
|d <== a * c - 45 * a + 987| (['a', 'c', 'd'], {'a*c': 1, 'a': -45, '': 987})|
| program constraint | assembly |
| -------------------------- | ------------------------------------------------ |
| a === 9 | ([None, None, 'a'], {'': 9}) |
| b <== a * c | (['a', 'c', 'b'], {'a*c': 1}) |
| d <== a * c - 45 * a + 987 | (['a', 'c', 'd'], {'a*c': 1, 'a': -45, '': 987}) |


### Setup
Expand Down Expand Up @@ -113,23 +118,23 @@ class Proof:

The proof consists of:

| proof element | remark |
|----------------------------------|----------------------------------------------------------------------------------------------|
|$[a(x)]_1$ | commitment to left wire polynomial |
|$[b(x)]_1$ | commitment to right wire polynomial |
|$[c(x)]_1$ | commitment to output wire polynomial |
|$[z(x)]_1$ | commitment to permutation polynomial |
|$[t_{lo}(x)]_1$ | commitment to $t_{lo}(X)$, the low chunk of the quotient polynomial $t(X)$ |
|$[t_{mid}(x)]_1$ | commitment to $t_{mid}(X)$, the middle chunk of the quotient polynomial $t(X)$ |
|$[t_{hi}(x)]_1$ | commitment to $t_{hi}(X)$, the high chunk of the quotient polynomial $t(X)$ |
|$\overline{a}$ | opening of $a(X)$ at evaluation challenge $\zeta$ |
|$\overline{b}$ | opening of $b(X)$ at evaluation challenge $\zeta$ |
|$\overline{c}$ | opening of $c(X)$ at evaluation challenge $\zeta$ |
|$\overline{\mathsf{s}}_{\sigma1}$ |opening of the first permutation polynomial $S_{\sigma1}(X)$ at evaluation challenge $\zeta$ |
|$\overline{\mathsf{s}}_{\sigma2}$ |opening of the second permutation polynomial $S_{\sigma2}(X)$ at evaluation challenge $\zeta$ |
|$\overline{z}_\omega$ | opening of shifted permutation polynomial $z(X)$ at shifted challenge $\zeta\omega$ |
|$[W_\zeta(X)]_1$ | commitment to the opening proof polynomial |
|$[W_{\zeta\omega}(X)]_1$ | commitment to the opening proof polynomial |
| proof element | remark |
| --------------------------------- | --------------------------------------------------------------------------------------------- |
| $[a(x)]_1$ | commitment to left wire polynomial |
| $[b(x)]_1$ | commitment to right wire polynomial |
| $[c(x)]_1$ | commitment to output wire polynomial |
| $[z(x)]_1$ | commitment to permutation polynomial |
| $[t_{lo}(x)]_1$ | commitment to $t_{lo}(X)$, the low chunk of the quotient polynomial $t(X)$ |
| $[t_{mid}(x)]_1$ | commitment to $t_{mid}(X)$, the middle chunk of the quotient polynomial $t(X)$ |
| $[t_{hi}(x)]_1$ | commitment to $t_{hi}(X)$, the high chunk of the quotient polynomial $t(X)$ |
| $\overline{a}$ | opening of $a(X)$ at evaluation challenge $\zeta$ |
| $\overline{b}$ | opening of $b(X)$ at evaluation challenge $\zeta$ |
| $\overline{c}$ | opening of $c(X)$ at evaluation challenge $\zeta$ |
| $\overline{\mathsf{s}}_{\sigma1}$ | opening of the first permutation polynomial $S_{\sigma1}(X)$ at evaluation challenge $\zeta$ |
| $\overline{\mathsf{s}}_{\sigma2}$ | opening of the second permutation polynomial $S_{\sigma2}(X)$ at evaluation challenge $\zeta$ |
| $\overline{z}_\omega$ | opening of shifted permutation polynomial $z(X)$ at shifted challenge $\zeta\omega$ |
| $[W_\zeta(X)]_1$ | commitment to the opening proof polynomial |
| $[W_{\zeta\omega}(X)]_1$ | commitment to the opening proof polynomial |


### Verifier
Expand All @@ -145,15 +150,15 @@ class VerificationKey:

The `VerificationKey` contains:

| verification key element | remark |
|----------------------------------|-------------------------------------------------------------------|
| $[q_M(x)]_1$ |commitment to multiplication selector polynomial |
| $[q_L(x)]_1$ |commitment to left selector polynomial |
| $[q_R(x)]_1$ |commitment to right selector polynomial |
| $[q_O(x)]_1$ |commitment to output selector polynomial |
| $[q_C(x)]_1$ |commitment to constants selector polynomial |
| $[S_{\sigma1}(x)]_1$ |commitment to the first permutation polynomial $S_{\sigma1}(X)$ |
| $[S_{\sigma2}(x)]_1$ |commitment to the second permutation polynomial $S_{\sigma2}(X)$ |
| $[S_{\sigma3}(x)]_1$ |commitment to the third permutation polynomial $S_{\sigma3}(X)$ |
| $[x]_2 = xH$ |(from the $\mathsf{srs}$) |
| $\omega$ |an $n$th root of unity, where $n$ is the program's group order. |
| verification key element | remark |
| ------------------------ | ---------------------------------------------------------------- |
| $[q_M(x)]_1$ | commitment to multiplication selector polynomial |
| $[q_L(x)]_1$ | commitment to left selector polynomial |
| $[q_R(x)]_1$ | commitment to right selector polynomial |
| $[q_O(x)]_1$ | commitment to output selector polynomial |
| $[q_C(x)]_1$ | commitment to constants selector polynomial |
| $[S_{\sigma1}(x)]_1$ | commitment to the first permutation polynomial $S_{\sigma1}(X)$ |
| $[S_{\sigma2}(x)]_1$ | commitment to the second permutation polynomial $S_{\sigma2}(X)$ |
| $[S_{\sigma3}(x)]_1$ | commitment to the third permutation polynomial $S_{\sigma3}(X)$ |
| $[x]_2 = xH$ | (from the $\mathsf{srs}$) |
| $\omega$ | an $n$th root of unity, where $n$ is the program's group order. |
84 changes: 40 additions & 44 deletions compiler/assembly.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,28 +3,34 @@
from typing import Optional
from dataclasses import dataclass


@dataclass
class GateWires:
"""Variable names for Left, Right, and Output wires."""

L: Optional[str]
R: Optional[str]
O: Optional[str]

def as_list(self) -> list[Optional[str]]:
return [self.L, self.R, self.O]


@dataclass
class Gate:
"""Gate polynomial"""

L: f_inner = f_inner(0)
R: f_inner = f_inner(0)
M: f_inner = f_inner(0)
O: f_inner = f_inner(0)
C: f_inner = f_inner(0)


@dataclass
class AssemblyEqn:
"""Assembly equation mapping wires to coefficients."""

wires: GateWires
coeffs: dict[Optional[str], int]

Expand All @@ -37,78 +43,71 @@ def R(self) -> f_inner:
return f_inner(0)

def C(self) -> f_inner:
return f_inner(-self.coeffs.get('', 0))
return f_inner(-self.coeffs.get("", 0))

def O(self) -> f_inner:
return f_inner(self.coeffs.get('$output_coeff', 1))
return f_inner(self.coeffs.get("$output_coeff", 1))

def M(self) -> f_inner:
if None not in self.wires.as_list():
return f_inner(-self.coeffs.get(get_product_key(self.wires.L, self.wires.R), 0))
return f_inner(
-self.coeffs.get(get_product_key(self.wires.L, self.wires.R), 0)
)
return f_inner(0)

def gate(self) -> Gate:
return Gate(
self.L(),
self.R(),
self.M(),
self.O(),
self.C()
)
return Gate(self.L(), self.R(), self.M(), self.O(), self.C())


# Converts a arithmetic expression containing numbers, variables and {+, -, *}
# into a mapping of term to coefficient
#
# For example:
# ['a', '+', 'b', '*', 'c', '*', '5'] becomes {'a': 1, 'b*c': 5}
#
#
# Note that this is a recursive algo, so the input can be a mix of tokens and
# mapping expressions
#
def evaluate(exprs: list[str], first_is_negative=False) -> dict[Optional[str], int]:
# Splits by + and - first, then *, to follow order of operations
# The first_is_negative flag helps us correctly interpret expressions
# like 6000 - 700 - 80 + 9 (that's 5229)
if '+' in exprs:
L = evaluate(exprs[:exprs.index('+')], first_is_negative)
R = evaluate(exprs[exprs.index('+')+1:], False)
return {
x: L.get(x, 0) + R.get(x, 0) for x in set(L.keys()).union(R.keys())
}
elif '-' in exprs:
L = evaluate(exprs[:exprs.index('-')], first_is_negative)
R = evaluate(exprs[exprs.index('-')+1:], True)
return {
x: L.get(x, 0) + R.get(x, 0) for x in set(L.keys()).union(R.keys())
}
elif '*' in exprs:
L = evaluate(exprs[:exprs.index('*')], first_is_negative)
R = evaluate(exprs[exprs.index('*')+1:], first_is_negative)
if "+" in exprs:
L = evaluate(exprs[: exprs.index("+")], first_is_negative)
R = evaluate(exprs[exprs.index("+") + 1 :], False)
return {x: L.get(x, 0) + R.get(x, 0) for x in set(L.keys()).union(R.keys())}
elif "-" in exprs:
L = evaluate(exprs[: exprs.index("-")], first_is_negative)
R = evaluate(exprs[exprs.index("-") + 1 :], True)
return {x: L.get(x, 0) + R.get(x, 0) for x in set(L.keys()).union(R.keys())}
elif "*" in exprs:
L = evaluate(exprs[: exprs.index("*")], first_is_negative)
R = evaluate(exprs[exprs.index("*") + 1 :], first_is_negative)
o = {}
for k1 in L.keys():
for k2 in R.keys():
o[get_product_key(k1, k2)] = L[k1] * R[k2]
return o
elif len(exprs) > 1:
raise Exception("No ops, expected sub-expr to be a unit: {}"
.format(exprs[1]))
elif exprs[0][0] == '-':
raise Exception("No ops, expected sub-expr to be a unit: {}".format(exprs[1]))
elif exprs[0][0] == "-":
return evaluate([exprs[0][1:]], not first_is_negative)
elif exprs[0].isnumeric():
return {'': int(exprs[0]) * (-1 if first_is_negative else 1)}
return {"": int(exprs[0]) * (-1 if first_is_negative else 1)}
elif is_valid_variable_name(exprs[0]):
return {exprs[0]: -1 if first_is_negative else 1}
else:
raise Exception("ok wtf is {}".format(exprs[0]))


# Converts an equation to a mapping of term to coefficient, and verifies that
# the operations in the equation are valid.
#
# Also outputs a triple containing the L and R input variables and the output
# variable
#
# Think of the list of (variable triples, coeffs) pairs as this language's
# version of "assembly"
# version of "assembly"
#
# Example valid equations, and output:
# a === 9 ([None, None, 'a'], {'': 9})
Expand All @@ -121,27 +120,27 @@ def evaluate(exprs: list[str], first_is_negative=False) -> dict[Optional[str], i
# e <== a + b * c * d # Multiplicative degree > 2
#
def eq_to_assembly(eq: str) -> AssemblyEqn:
tokens = eq.rstrip('\n').split(' ')
if tokens[1] in ('<==', '==='):
tokens = eq.rstrip("\n").split(" ")
if tokens[1] in ("<==", "==="):
# First token is the output variable
out = tokens[0]
# Convert the expression to coefficient map form
coeffs = evaluate(tokens[2:])
# Handle the "-x === a * b" case
if out[0] == '-':
if out[0] == "-":
out = out[1:]
coeffs['$output_coeff'] = -1
coeffs["$output_coeff"] = -1
# Check out variable name validity
if not is_valid_variable_name(out):
raise Exception("Invalid out variable name: {}".format(out))
# Gather list of variables used in the expression
variables = []
for t in tokens[2:]:
var = t.lstrip('-')
var = t.lstrip("-")
if is_valid_variable_name(var) and var not in variables:
variables.append(var)
# Construct the list of allowed coefficients
allowed_coeffs = variables + ['', '$output_coeff']
# Construct the list of allowed coefficients
allowed_coeffs = variables + ["", "$output_coeff"]
if len(variables) == 0:
pass
elif len(variables) == 1:
Expand All @@ -157,14 +156,11 @@ def eq_to_assembly(eq: str) -> AssemblyEqn:
raise Exception("Disallowed multiplication: {}".format(key))
# Return output
wires = variables + [None] * (2 - len(variables)) + [out]
return AssemblyEqn(
GateWires(wires[0], wires[1], wires[2]),
coeffs
)
elif tokens[1] == 'public':
return AssemblyEqn(GateWires(wires[0], wires[1], wires[2]), coeffs)
elif tokens[1] == "public":
return AssemblyEqn(
GateWires(tokens[0], None, None),
{tokens[0]: -1, '$output_coeff': 0, '$public': True}
{tokens[0]: -1, "$output_coeff": 0, "$public": True},
)
else:
raise Exception("Unsupported op: {}".format(tokens[1]))
Loading

0 comments on commit ab6b185

Please sign in to comment.