Challenge Two: Crafting Constraint Systems
References
 [1] E. BenSasson, A. Chiesa, C. Garman, Green, I. Miers, E. Tromer and M. Virza (2014), Zerocash: decentralized anonymous payments from Bitcoin. In Proceedings of the 2014 IEEE Symposium on Security and Privacy, SP ’14, pp. 459–474. External Links: Link.
 [2] E. BenSasson, A. Chiesa, D. Genkin, E. Tromer and M. Virza (2013), SNARKs for C: verifying program executions succinctly and in zero knowledge (extended version). Note: Cryptology ePrint Archive, Report 2013/507. External Links: Link.
 [3] E. BenSasson, A. Chiesa, D. Genkin, E. Tromer and M. Virza (2013), SNARKs for C: verifying program executions succinctly and in zero knowledge. In CRYPTO ’13, pp. 90–108. Note: Extended version: [2].
 [4] E. BenSasson, A. Chiesa, E. Tromer and M. Virza (2014), Succinct noninteractive zero knowledge for a von Neumann architecture. In USENIX Security 2014, pp. 781–796. External Links: Link.
 [5] N. Bitansky, R. Canetti, A. Chiesa, S. Goldwasser, H. Lin, A. Rubinstein and E. Tromer, The hunting of the SNARK. Journal of Cryptology. Note: to appear. External Links: Link.
 [6] (2016) BIU winter school: cryptography in the cloud — verifiable computation and special encryption. Note: workshop (with video recording). External Links: Link.
 [7] V. Buterin (2017), zkSNARKs: under the hood. Note: blog posts. External Links: Link.
 [8] A. Gabizon (2017), Explaining snarks (parts i through vii). Note: blog posts. External Links: Link.
 [9] R. Gennaro, C. Gentry, B. Parno and M. Raykova (2013), Quadratic span programs and succinct NIZKs without PCPs. In EUROCRYPT ’13, pp. 626–645. External Links: Link.
 [10] S. Goldwasser, S. Micali and C. Rackoff (1985), The knowledge complexity of interactive proofsystems. In STOC 1985, pp. 291–304. External Links: Link.
 [11] M. Green (2014), Zero knowledge proofs: an illustrated primer. Note: blog post. External Links: Link.
 [12] M. Naor, Y. Naor and O. Reingold (1999), Applied kid cryptography or how to convince your children you are not cheating. In Eurocrypt ’94, pp. 1–12.
 [13] M. Naor(Website). External Links: Link.
 [14] B. Parno, J. Howell, C. Gentry and M. Raykova (2013), Pinocchio: nearly practical verifiable computation. In IEEE Symposium on Security and Privacy, pp. 238–252. External Links: Link.
 [15] C. Reitwiessner (2016), zkSNARKs in a nutshell. Note: blog post. External Links: Link.
 [16] D. Benarroch and A. Zohar (2017), Trustless Computing on Private Data. Note: blog post. External Links: Link.
 [17] (2017) QEDit Meetup, Proveit, Blockchainit: ZKP in Action. Note: Tel Aviv Meetup (with video recording). External Links: Link.
 [18] T. Sander and A. TaShma (1999)Auditable, anonymous electronic cash.In Proceedings of the 19th Annual International Cryptology Conference on Advances in Cryptology,CRYPTO ’99, pp. 555–572. External Links: Link.
BCS Definition
Definition. Let ${n}_{\U0001d5d1},{n}_{\U0001d5d0},{n}_{\U0001d5bc}$ be positive integers, and ${n}_{\U0001d5d3}={n}_{\U0001d5d1}+{n}_{\U0001d5d0}+1$. A bilinear constraint system over ${\mathbb{F}}_{q}$ is a tuple $\mathbf{S}=({({\overrightarrow{a}}_{j},{\overrightarrow{b}}_{j},{\overrightarrow{c}}_{j})}_{j=1}^{{n}_{\U0001d5bc}},{n}_{\U0001d5d1})$ where ${\overrightarrow{a}}_{j},{\overrightarrow{b}}_{j},{\overrightarrow{c}}_{j}\in {\mathbb{F}}_{q}^{{n}_{\U0001d5d3}}$. Such a system $\mathbf{S}$ is satisfiable with an input $\overrightarrow{x}\in {\mathbb{F}}_{q}^{{n}_{\U0001d5d1}}$ if the following is true:

For these ${\mathbf{S}}{=}{(}{{(}{\overrightarrow{{a}}}_{{j}}{,}{\overrightarrow{{b}}}_{{j}}{,}{\overrightarrow{{c}}}_{{j}}{)}}_{{j}{=}{1}}^{{{n}}_{{\U0001d5bc}}}{,}{{n}}_{{\U0001d5d1}}{)}$ and $\overrightarrow{{x}}{\in}{{\mathbb{F}}}_{{q}}^{{{n}}_{{\U0001d5d1}}}$;

there exists a witness $\overrightarrow{{w}}{\in}{{\mathbb{F}}}_{{q}}^{{{n}}_{{\U0001d5d0}}}$;

such that ${\u27e8}{\overrightarrow{{a}}}_{{j}}{,}\overrightarrow{{z}}{\u27e9}{\cdot}{\u27e8}{\overrightarrow{{b}}}_{{j}}{,}\overrightarrow{{z}}{\u27e9}{=}{\u27e8}{\overrightarrow{{c}}}_{{j}}{,}\overrightarrow{{z}}{\u27e9}$ for all for ${j}{\in}{[}{{n}}_{{\U0001d5bc}}{]}$, where $\overrightarrow{{z}}{=}{(}{1}{,}\overrightarrow{{x}}{,}\overrightarrow{{w}}{)}{\in}{{\mathbb{F}}}_{{q}}^{{{n}}_{{\U0001d5d3}}}$ .
Above, $\u27e8\mathrm{\cdots},\mathrm{\cdots}\u27e9$ denotes inner product of vectors over ${\mathbb{F}}_{q}$, and $\cdot $ denotes multiplication in ${\mathbb{F}}_{q}$.
For example, the bilinear constraint system
$$\mathbf{S}=(\left(\begin{array}{c}\hfill {\overrightarrow{a}}_{1}=(0,3,0,0),{\overrightarrow{b}}_{1}=(1,1,0,0),{\overrightarrow{c}}_{1}=(4,0,5,0)\\ \hfill {\overrightarrow{a}}_{2}=(0,1,2,0),{\overrightarrow{b}}_{2}=(6,0,1,0),{\overrightarrow{c}}_{2}=(7,0,0,1)\end{array}\right),1)$$  (1) 
represents the two bilinear constraints
$$\begin{array}{cc}\hfill \u27e8(0,3,0,0),\overrightarrow{z}\u27e9\cdot \u27e8(1,1,0,0),\overrightarrow{z}\u27e9& =\u27e8(4,0,5,0),\overrightarrow{z}\u27e9\hfill \\ \hfill \u27e8(0,1,2,0),\overrightarrow{z}\u27e9\cdot \u27e8(6,0,1,0),\overrightarrow{z}\u27e9& =\u27e8(7,0,0,1),\overrightarrow{z}\u27e9\hfill \end{array}\mathit{\hspace{1em}}\text{where}\overrightarrow{z}=(1,{x}_{1},{w}_{1},{w}_{2})$$  (2) 
or simply:
$3{x}_{1}\cdot (1+{x}_{1})$  $=5{w}_{1}+4$  (3)  
$({x}_{1}+2{w}_{1})\cdot ({w}_{1}+6)$  $={w}_{2}+7$ 
By definition, this system $\mathbf{S}$ is satisfiable with input ${x}_{1}$ if the following is true:

For the instance ${{x}}_{{1}}$;

there exist a witness ${{w}}_{{1}}{,}{{w}}_{{2}}$;

such that
${3}{}{{x}}_{{1}}{\cdot}{(}{1}{+}{{x}}_{{1}}{)}$ ${=}{5}{}{{w}}_{{1}}{+}{4}$ ${(}{{x}}_{{1}}{+}{2}{}{{w}}_{{1}}{)}{\cdot}{(}{{w}}_{{1}}{+}{6}{)}$ ${=}{{w}}_{{2}}{+}{7}$
Gadgets
We recall the gadgets introduced previously.
$\begin{array}{c}\mathrm{\text{Boolean}}(v):=\{\mathit{\hspace{1em}}\text{//}v\text{is 0 or 1}\hfill \\ \mathit{\hspace{1em}}\begin{array}{c}v\cdot (v1)=0\hfill \end{array}\hfill \\ \}\hfill \end{array}$
$\begin{array}{c}\mathrm{\text{Square}}(v):=\{\mathit{\hspace{1em}}\text{//}v\in {\mathbb{F}}_{q}\text{is a square (i.e., quadratic residue) in}{\mathbb{F}}_{q}\hfill \\ \mathit{\hspace{1em}}\begin{array}{c}u:\text{//}u\text{is a square root of}v\hfill \\ u\cdot u=v\hfill \end{array}\hfill \\ \}\hfill \end{array}$
$\begin{array}{c}\mathrm{\text{Booleanify}}(v,b):=\{\mathit{\hspace{1em}}\text{// for}v\in {\mathbb{F}}_{q}\text{, if}v=0\text{then}b=0\text{, else}b=1\hfill \\ \mathit{\hspace{1em}}\begin{array}{c}u\text{// if}v\ne 0\text{then}u={v}^{1}\text{over}{\mathbb{F}}_{q}\text{, otherwise}u\text{is arbitrary}\hfill \\ u\cdot v=b\hfill \\ b\cdot v=v\hfill \end{array}\hfill \\ \}\hfill \end{array}$
$\begin{array}{c}\mathrm{\text{Or}}(a,b,c):=\{\mathit{\hspace{1em}}\text{//}a,b,c\in \{0,1\}\subset {\mathbb{F}}_{q}\text{, and}c=a\wedge b\text{as Boolean variables}\hfill \\ \mathit{\hspace{1em}}\begin{array}{c}s:\hfill \\ \mathrm{\text{Boolean}}(a)\hfill \\ \mathrm{\text{Boolean}}(b)\hfill \\ a+b=s\hfill \\ \mathrm{\text{Booleanify}}(s,c)\hfill \end{array}\hfill \\ \}\hfill \end{array}$
$\begin{array}{c}\mathrm{\text{IsEqual}}(a,b,c):=\{\mathit{\hspace{1em}}\text{// if}a=b\text{then}c=1\text{, else}c=0\hfill \\ \mathit{\hspace{1em}}\begin{array}{c}d,e:\hfill \\ ab=d\hfill \\ \mathrm{\text{Booleanify}}(d,e)\hfill \\ 1e=c\hfill \end{array}\hfill \\ \}\hfill \end{array}$