Joshua Fitzgerald

@lopeetall

Joined on Jun 1, 2020

  • Interesting tidbits Sometimes a CSP is called a "database" because the theory of CSPs and relational databases overlap. A CSP over a finite domain is the same thing as a relational database. A CSP instance can be called a "query" of the database. An "instance" is a particular representation of a CSP, with variables and constraints enumerated. An example of two different instances of the same CSP are $X_1 = {x}$, $C_1 = {x(x-1)(x-2)(x-3)}$ vs $X_2 = {x, b_0, b_1}$, $C_2 = {b_0^2 - b_0, b_1^2 - b_1, x - 2b_1 - b_0}$. Both instances constrain $x$ to be 0, 1, 2, or 3 despite having different variable sets and constraint sets. The proofs that ZKPs exist was based on graph coloring. Intents can be formulated as CSPs. CSP solving can be distributed! Each solver gets a small portion of the CSP to examine and communicates with other solvers to reach a solution. This works best when the CSP is "sparse and loose", meaning each variable relates to just a few other variables and there are many satisfying assignments for each constraint. An example could be a CSP to find a small non-trivial Pythagorean Triple. Three solvers approach the problem, each focusing on a particular variable. Solver A focuses on the $a^2$ portion of the problem and makes an ordered list of a few possibilities: $(1, 4, 9, 16, 25)$. Solver B focuses on $b^2$ but is more optimistic, making a shorter list; $(1, 4, 9)$. Solvers A and B send their lists to Solver C, who makes a list of all possible sums of their value sets and puts them in order: $(2, 5, 8, 10, 13, 17, 18, 20, 25, 26, 29, 34)$. Meanwhile, the final Solver D makes an ordered list of possible values for $c^2$: $(1, 4, 9, 16, 25, 36)$. Solver C sends its list to Solver D, who searches for a match in the list. When the final solver finds a match, it sends its choice back to the other solvers who construct a solution $(3, 4, 5)$. Tweets For Anoma we are researching best ways to formalize intents. What precisely are they, what are their components, how do we combine intents efficiently, and so on.
     Like  Bookmark
  • To do: consider speccing a "Plonkish IR" encompassing Halo2, Plonk-3, Plonk-4, ACIR with different configs spec out ACIR, Evaluated, Partially Evaluated, CCS sketch out transformation algorithms (flatten/unflatten, evaluate/unevaluate, others?) and their difficulties Diagram https://excalidraw.com/#json=yJaqzS5aODMD2aJCyYrun,9YgROu_OmfnX2b8_wUfWXg VAMP-IR Modules
     Like  Bookmark
  • Errata Section 2.1 (page 9)The exponent $l$ is missing in the definition of $\widetilde{f}$. It should be: $\widetilde{f}: \mathbb{F}^l \to \mathbb{F}$ Section 3, Equation 5 (page 12) The $N$ in the index set of the sum should be lowercase to match the previous variable name (?) Section 4.1, paragraph following proof of equation 8, 4th line The tuple $(j, r_x)$ should be $(j, r_y)$
     Like 3 Bookmark
  • The Taiga as a Product group consists of Vasily (co-lead), Joshua (co-lead), Xuyang, Alberto, Yulia, and Joe. It should be noted that two group members (Vasily and Alberto) had time off during this cycle and two others (Yulia and Joshua) were speaking at EthCC during this cycle. What we worked on We began this cycle by choosing from a list of issues that were identified last cycle. The issues we chose to work on were: Taiga APIs Execution of Vamp-IR validity predicates Unify the number and layout of VP public inputs. Adjust the vp implementation accordingly Design the VP time awareness feature (block height, “epoch”, etc. as an input to VP) Taiga tutorial
     Like  Bookmark
  • Our compiler stack consists of Juvix, GEB, Vamp-IR, and Taiga. Juvix can compile to GEB and then to Vamp-IR or directly to Vamp-IR. Taiga can then call Vamp-IR functions to create or verify proofs as a part of its execution model. Status Currently, we can take a Juvix program and compile it directly into Vamp-IR (bypassing GEB). Then Taiga can call Vamp-IR functions to prove or verify using the Vamp-IR circuit generated by Juvix. GEB is bypassed currently due to some missing features that are necessary to integrate GEB with Juvix. Strengths This stack's primary strength is the uniformity in approach between the elements of the stack. The functional/category theoretic approach is present in each compiler, making the interface between elements simpler to maintain and modify. As a concrete example, the Vamp-IR compiler allows the inclusion of higher-order "intrinsic functions" like map and fold which correspond to those functorial operations in GEB and Juvix. We believe this uniform approach is the right one for meeting Anoma's needs. Another strength of our stack is that the overall design sticks close to the mathematical objects we are trying to use. Juvix describes a simply-typed lambda calculus, Vamp-IR describes arithmetic circuits as systems of polynomials, GEB describes transformations between STLC and polynomials. While perhaps not the most friendly to developer onboarding, this approach allows quick integration of other tools (like Z3 for analyzing arithmetic circuits in Vamp-IR) and known PLT and compiler design techniques.
     Like  Bookmark
  • Deliverables Report on the current compiler stack considered as a holistic product (Juvix-VampIR-Taiga), considering which parts are strong, which parts are weak, where the open questions are, and what we need to prioritise in the immediate future across the whole stack. People Joshua (lead), Jan, Lukasz Links Matching Experiment doc: https://hackmd.io/@heliax/ByxPTlQOh Report Outline
     Like  Bookmark
  • Title: LLVM for polynomial circuits (now with benchmarks!) Primary purpose: Give a practical introduction to Vamp-IR Secondary purposes:
     Like  Bookmark
  • Plonkish Constraint Forms A Plonkish "constraint form" is defined by a single, fixed, multivariable polynomial. The variables of this polynomial are called wire columns (sometimes shortened to just wires, although this is not precisely correct). Wire columns represent indeterminate data. This data can be private to the Prover, or public and provided by the Prover, Verifier, or both, at proof time. The halo2 book uses the terms advice and instance for the private and public wire columns, respectively. Together these wire columns can be thought of as the inputs and outputs of each node in an arithmetic circuit. The coefficients of this polynomial are fixed in advance. Most of the coefficients come from selectors which turn certain rows and columns on or off, and a few come from other parameters. These are called fixed columns in the halo2 book. Original Plonk Constraint Form The original Plonk paper used three private wire columns ($a$, $b$, and $c$), one public column $pi$, and five selectors ($q_M, q_L, q_R, q_O, q_C$). The polynomial defining original Plonk is this:
     Like  Bookmark
  • Vamp-IR a universal intermediate representation for circuits VAMP-IR is a proof system agnostic language for arithmetic circuits. Circuits written in VAMP-IR can be compiled to any proof system backend using any arithmetic constraint system or configuration, including those with custom gates or lookup tables Arithmetic Circuits Arithmetic circuits are a representation of systems of polynomial constraints.
     Like  Bookmark