First commit

circuits/jose.jaz

@@ -0,0 +1,11 @@
+template AND() {
+    signal input s1;
+    signal input s2;
+    signal output s3;
+
+    s3 <== s1*s2;
+    s1*(s1-1) === 0;
+    s2*(s2-1) === 0;
+}
+
+component main = AND();

circuits/multiplexer.jaz

@@ -0,0 +1,74 @@
+// --> Assignation without constrain
+// <-- Assignation without constrain
+// === Constrain
+// <== Assignation with constrain
+// ==> Assignation with constrain
+// All variables are members of the field F[p]
+// https://github.com/zcash-hackworks/sapling-crypto
+// https://github.com/ebfull/bellman
+
+/*
+function log2(a) {
+    if (a==0) {
+        return 0;
+    }
+    let n = 1;
+    let r = 1;
+    while (n<a) {
+        r++;
+        n *= 2;
+    }
+    return r;
+}
+*/
+
+template EscalarProduct(w) {
+    signal input in1[w];
+    signal input in2[w];
+    signal output out;
+    signal aux[w];
+    var lc = 0;
+    for (var i=0; i<w; i++) {
+        aux[i] <== in1[i]*in2[i];
+        lc = lc + aux[i];
+    }
+    out <== lc;
+}
+
+template Decoder(w) {
+    signal input inp;
+    signal output out[w];
+    signal output success;
+    var lc=0;
+
+    for (var i=0; i<w; i++) {
+        out[i] <-- (inp == i) ? 1 : 0;
+        out[i] * (inp-i) === 0;
+        lc = lc + out[i];
+    }
+
+    lc ==> success;
+    success * (success -1) === 0;
+}
+
+
+template Multiplexor(wIn, nIn) {
+    signal input inp[nIn][wIn];
+    signal input sel;
+    signal output out[wIn];
+    component Decoder(nIn) dec;
+    component EscalarProduct(nIn) ep[wIn];
+    sel ==> dec.inp;
+    for (var j=0; j<wIn; j++) {
+        for (var k=0; k<nIn; k++) {
+            inp[k][j] ==> ep[j].in1[k];
+            dec.out[k] ==> ep[j].in2[k];
+        }
+        ep[j].out ==> out[j];
+    }
+    dec.success === 1;
+}
+
+component Multiplexor(8,3) main;
+
+

circuits/sha256/binsum.jaz

@@ -0,0 +1,74 @@
+/*
+
+Binary Sum
+==========
+
+This component creates a binary sum componet of ops operands and n bits each operand.
+
+e is Number of carries: Depends on the number of operands in the input.
+
+Main Constrain:
+   in[0][0]     * 2^0  +  in[0][1]     * 2^1  + ..... + in[0][n-1]    * 2^(n-1)  +
+ + in[1][0]     * 2^0  +  in[1][1]     * 2^1  + ..... + in[1][n-1]    * 2^(n-1)  +
+ + ..
+ + in[ops-1][0] * 2^0  +  in[ops-1][1] * 2^1  + ..... + in[ops-1][n-1] * 2^(n-1)  +
+ ===
+   out[0] * 2^0  + out[1] * 2^1 +   + out[n+e-1] *2(n+e-1)
+
+To waranty binary outputs:
+
+    out[0]     * (out[0] - 1) === 0
+    out[1]     * (out[0] - 1) === 0
+    .
+    .
+    .
+    out[n+e-1] * (out[n+e-1] - 1) == 0
+
+ */
+
+
+/*
+    This function calculates the number of extra bits in the output to do the full sum.
+ */
+
+function nbits(a) {
+    var n = 1;
+    var r = 0;
+    while (n-1<a) {
+        r++;
+        n *= 2;
+    }
+    return r;
+}
+
+
+template BinSum(n, ops) {
+    var nout = nbits((2**n -1)*ops);
+    signal input in[ops][n];
+    signal output out[nout];
+
+    var lin = 0;
+    var lout = 0;
+
+    var k;
+    var j;
+
+    for (k=0; k<n; k++) {
+        for (j=0; j<ops; j++) {
+            lin += in[j][k] * 2**k;
+        }
+    }
+
+    for (k=0; k<nout; k++) {
+        out[k] <-- (lin >> k) & 1;
+
+        // Ensure out is binary
+        out[k] * (out[k] - 1) === 0;
+
+        lout += out[k] * 2**k;
+    }
+
+    // Ensure the sum;
+
+    lin === lout;
+}

circuits/sha256/bitify.jaz

@@ -0,0 +1,28 @@
+
+
+template Num2Bits(n) {
+    signal input in;
+    signal output out[n];
+    var lc1=0;
+
+    for (var i = 0; i<n; i++) {
+        out[i] <-- (in >> i) & 1;
+        out[i] * (out[i] -1 ) === 0;
+        lc1 += out[i] * 2**i;
+    }
+
+    lc1 === in;
+
+}
+
+template Bits2Num(n) {
+    signal input in[n];
+    signal output out;
+    var lc1=0;
+
+    for (var i = 0; i<n; i++) {
+        lc1 += in[i] * 2**i;
+    }
+
+    lc1 ==> out;
+}

circuits/sha256/constants.jaz

@@ -0,0 +1,35 @@
+
+
+template H(x) {
+    signal output out[32];
+    var c = [0x6a09e667,
+             0xbb67ae85,
+             0x3c6ef372,
+             0xa54ff53a,
+             0x510e527f,
+             0x9b05688c,
+             0x1f83d9ab,
+             0x5be0cd19];
+
+    for (var i=0; i<32; i++) {
+        out[i] = (c[x] >> i) & 1;
+    }
+}
+
+template K(x) {
+    signal output out[32];
+    var c = [
+        0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5,
+        0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174,
+        0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da,
+        0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967,
+        0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85,
+        0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070,
+        0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3,
+        0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2
+    ];
+
+    for (var i=0; i<32; i++) {
+        out[i] = (c[x] >> i) & 1;
+    }
+}

circuits/sha256/gates.jaz

@@ -0,0 +1,67 @@
+
+template XOR() {
+    signal input a;
+    signal input b;
+    signal output out;
+
+    out <== a + b - 2*a*b;
+}
+
+template AND() {
+    signal input a;
+    signal input b;
+    signal output out;
+
+    out <== a*b;
+}
+
+template OR() {
+    signal input a;
+    signal input b;
+    signal output out;
+
+    out <== a + b - a*b;
+}
+
+template NOT() {
+    signal input in;
+    signal output out;
+
+    out <== 1 + in - 2*in;
+}
+
+template NAND() {
+    signal input a;
+    signal input b;
+    signal output out;
+
+    out <== 1 - a*b;
+}
+
+template NOR() {
+    signal input a;
+    signal input b;
+    signal output out;
+
+    out <== a*b + 1 - a - b;
+}
+
+template Xor3(n) {
+    signal input a[n];
+    signal input b[n];
+    signal input c[n];
+    signal output out[n];
+
+    component xor1[n] = XOR();
+    component xor2[n] = XOR();
+
+    for (var k=0; k<n; k++) {
+        xor1[k].a <== a[k];
+        xor1[k].b <== b[k];
+
+        xor2[k].a <== xor1[k].out;
+        xor2[k].b <== c[k];
+
+        out[k] <== xor2[k].out;
+    }
+}

circuits/sha256/input_h0.json

@@ -0,0 +1,3 @@
+{
+	"in": "0xd807aa98"
+}

circuits/sha256/input_sum_test.json

@@ -0,0 +1,4 @@
+{
+    "a": "111",
+    "b": "222"
+}

circuits/sha256/main.jaz

@@ -0,0 +1,50 @@
+
+/*
+include "sha256_2.jaz";
+
+component main = SHA256_2();
+*/
+
+/*
+include "constants.jaz"
+
+template A() {
+    signal input in;
+    component h0;
+    h0 = K(8);
+
+    var lc = 0;
+    var e = 1;
+    for (var i=0; i<32; i++) {
+        lc = lc + e*h0.out[i];
+        e *= 2;
+    }
+
+    lc === in;
+}
+
+component main = A();
+*/
+
+include "bitify.jaz"
+
+template A() {
+    signal input in;
+    signal output out;
+
+    component n2b;
+    component b2n;
+
+    n2b = Num2Bits(216);
+    b2n = Bits2Num(216);
+
+    n2b.in <== in;
+
+    for (var i=0; i<216; i++) {
+        b2n.in[i] <== n2b.out[i];
+    }
+
+    out <== b2n.out;
+}
+
+component main = A();

circuits/sha256/rotate.jaz

@@ -0,0 +1,10 @@
+
+
+template RotR(n, r) {
+    signal input in[n];
+    signal output out[n];
+
+    for (i=0; i<n; i++) {
+        out[i] <== in[ (i+r)%n ];
+    }
+}

circuits/sha256/sha256_2.jaz

@@ -0,0 +1,44 @@
+
+include "sha256compression.jaz";
+include "bitify.jaz"
+
+component sha256_2() {
+    signal input a;
+    signal input b;
+    signal output out;
+
+    component num2bits[2] = Num2Bits(216);
+    component bits2num = Bits2Num(216);
+
+    num2bits[0].inp <== a;
+    num2bits[1].inp <== b;
+
+    component sha256compression = Sha256compression() ;
+
+    var i;
+
+    for (i=0; i<216; i++) {
+        sha256compression.inp[i] <== num2bits[0].out[i];
+        sha256compression.inp[i+216] <== num2bits[1].out[i];
+    }
+
+    for (i=432; i<247; i++) {
+        sha256compression.inp[i] <== 0;
+    }
+
+    sha256compression.inp[247] <== 1;
+    sha256compression.inp[248] <== 1;
+    sha256compression.inp[249] <== 0;
+    sha256compression.inp[250] <== 1;
+    sha256compression.inp[251] <== 1;
+    sha256compression.inp[252] <== 0;
+    sha256compression.inp[253] <== 0;
+    sha256compression.inp[254] <== 0;
+    sha256compression.inp[255] <== 0;
+
+    for (i=0; i<216; i++) {
+        bits2num.inp[i] <== sha256compression.out[i];
+    }
+
+    out <== bits2num.out;
+}

circuits/sha256/sha256compression.jaz

@@ -0,0 +1,145 @@
+
+include "constants.jaz";
+include "t1.jaz";
+include "t2.jaz";
+include "sum.jaz";
+include "sigmaplus.jaz";
+
+template sha256compression() {
+    signal input inp[512];
+    signal output out[256];
+    signal a[64][32];
+    signal b[64][32];
+    signal c[64][32];
+    signal d[64][32];
+    signal e[64][32];
+    signal f[64][32];
+    signal g[64][32];
+    signal h[64][32];
+    signal w[64][512];
+
+    var i;
+
+    component sigmaPlus[48] = SigmaPlus();
+
+    component k[64];
+    for (i=0; i<64; i++) k[i] = K(i);
+
+    component ha0 = H0(0);
+    component hb0 = H0(1);
+    component hc0 = H0(2);
+    component hd0 = H0(3);
+    component he0 = H0(4);
+    component hf0 = H0(5);
+    component hg0 = H0(6);
+    component hh0 = H0(7);
+
+    component t1[64] = T1();
+    component t2[64] = T2();
+
+    component suma[64] = Sum2(32);
+    component sume[64] = Sum2(32);
+    component fsum[8]  = Sum2(32);
+
+    var k;
+    var t;
+
+    for (t=0; t<64; t++) {
+        if (t<16) {
+            for (k=0; k<256; k++) {
+                w[t][k] <== inp[k];
+            }
+        } else {
+            for (k=0; k<256; k++) {
+                sigmaPlus[t-16].in2[k] <== w[t-2][k];
+                sigmaPlus[t-16].in7[k] <== w[t-2][k];
+                sigmaPlus[t-16].in15[k] <== w[t-15][k];
+                sigmaPlus[t-16].in16[k] <== w[t-16][k];
+                w[t][k] <== sigmaPlus[t-16].out[k];
+            }
+        }
+    }
+
+    for (k=0; k<32; k++ ) {
+        a[0][k] <== ha0.out[k]
+        b[0][k] <== hb0.out[k]
+        c[0][k] <== hc0.out[k]
+        d[0][k] <== hd0.out[k]
+        e[0][k] <== he0.out[k]
+        f[0][k] <== hf0.out[k]
+        g[0][k] <== hg0.out[k]
+        h[0][k] <== hh0.out[k]
+    }
+
+    for (t = 0; t<63; t++) {
+        for (k=0; k<32; k++) {
+            t1[t].h[k] <== h[k];
+            t1[t].e[k] <== e[k];
+            t1[t].f[k] <== f[k];
+            t1[t].g[k] <== g[k];
+            if (t<20) {
+                t1[t].g[k] <== K0.out[k];
+            } else if (t<40) {
+                t1[t].g[k] <== K20.out[k];
+            } else if (t<60) {
+                t1[t].g[k] <== K40.out[k];
+            } else {
+                t1[t].g[k] <== K60.out[k];
+            }
+            t1[t].w[k] <== w[t][k];
+
+            t2[t].a[k] <== a[k];
+            t2[t].b[k] <== a[k];
+            t2[t].c[k] <== a[k];
+        }
+
+        for (k=0; k<32; k++) {
+            sume[t].a[k] <== d[k];
+            sume[t].b[k] <== t1[t].out[k];
+
+            suma[t].a[k] <== t1[t].out[k];
+            suma[t].b[k] <== t2[t].out[k];
+        }
+
+        for (k=0; k<32; k++) {
+            h[t+1] <== g[t];
+            g[t+1] <== f[t];
+            f[t+1] <== e[t];
+            e[t+1] <== sume[t].out[k];
+            d[t+1] <== c[t];
+            c[t+1] <== b[t];
+            b[t+1] <== a[t];
+            a[t+1] <== suma[t].out[k];
+        }
+    }
+
+    for (k=0; k<32; k++) {
+        fsum[0].a[k] <==  ha0.out[k];
+        fsum[0].b[k] <==  a[64][k];
+        fsum[1].a[k] <==  hb0.out[k];
+        fsum[1].b[k] <==  b[64][k];
+        fsum[2].a[k] <==  hc0.out[k];
+        fsum[2].b[k] <==  c[64][k];
+        fsum[3].a[k] <==  hd0.out[k];
+        fsum[3].b[k] <==  d[64][k];
+        fsum[4].a[k] <==  he0.out[k];
+        fsum[4].b[k] <==  e[64][k];
+        fsum[5].a[k] <==  hf0.out[k];
+        fsum[5].b[k] <==  f[64][k];
+        fsum[6].a[k] <==  hg0.out[k];
+        fsum[6].b[k] <==  g[64][k];
+        fsum[7].a[k] <==  hh0.out[k];
+        fsum[7].b[k] <==  h[64][k];
+    }
+
+    for (k=0; k<32; k++) {
+        out[k]    <== fsum[0].out[k];
+        out[32+k] <== fsum[1].out[k];
+        out[64+k] <== fsum[2].out[k];
+        out[96+k] <== fsum[2].out[k];
+        out[128+k] <== fsum[2].out[k];
+        out[160+k] <== fsum[2].out[k];
+        out[192+k] <== fsum[2].out[k];
+        out[224+k] <== fsum[2].out[k];
+    }
+}

circuits/sha256/sigma.jaz

@@ -0,0 +1,25 @@
+include "gates.jaz";
+include "rotate.jaz";
+
+template Sigma(ra, rb, rc) {
+    signal input in;
+    signal output out;
+
+    component xor3 = Xor3(32);
+
+    component rota = RotR(32, ra);
+    component rotb = RotR(32, rb);
+    component rotc = RotR(32, rc);
+
+    for (var k=0; k<32; k++) {
+        rota.in[k] <== in[k];
+        rotb.in[k] <== in[k];
+        rotc.in[k] <== in[k];
+
+        xor3.a[k] <== rota.out[k];
+        xor3.b[k] <== rotb.out[k];
+        xor3.c[k] <== rotc.out[k];
+
+        out[k] <== xor3.out[k];
+    }
+}

circuits/sha256/sigmaplus.jaz

@@ -0,0 +1,26 @@
+include "sum.jaz"
+include "sigma.jaz"
+
+template SigmaPlus() {
+    signal input in2[32];
+    signal input in7[32];
+    signal input in15[32];
+    signal input in16[32];
+    signal output out[32];
+
+    component sum = Sum(32, 4);
+    component sigma1 = Sigma(17,19,10);
+    component sigma0 = Sigma(7, 18, 3);
+
+    for (var k=0; k<32; k++) {
+        sigma1.in[k] <== in2[k];
+        sigma0.in[k] <== in15[k];
+
+        sum.in[0][k] <== sigma1.out[k];
+        sum.in[1][k] <== in7[k];
+        sum.in[2][k] <== sigma0.out[k];
+        sum.in[3][k] <== in16[k];
+
+        out[k] <== sum.out[k];
+    }
+}

circuits/sha256/sum_test.jaz

@@ -0,0 +1,26 @@
+include "bitify.jaz"
+include "binsum.jaz"
+
+template A() {
+    signal input a;
+    signal input b;
+    signal output out;
+
+    component n2ba = Num2Bits(32);
+    component n2bb = Num2Bits(32);
+    component sum = BinSum(32,2);
+    component b2n = Bits2Num(32);
+
+    n2ba.in <== a;
+    n2bb.in <== b;
+
+    for (var i=0; i<32; i++) {
+        sum.in[0][i] <== n2ba.out[i];
+        sum.in[1][i] <== n2bb.out[i];
+        b2n.in[i] <== sum.out[i];
+    }
+
+    out <== b2n.out;
+}
+
+component main = A();

circuits/tobin.jaz

@@ -0,0 +1,20 @@
+
+
+
+template toBin(n) {
+    signal input inp;
+    signal output out[n];
+    var lc1=0;
+
+    for (var i = 0; i<n; i++) {
+        out[i] <-- (inp >> i) & 1;
+        out[i] * (out[i] -1 ) === 0;
+        lc1 += out[i] * 2**i;
+    }
+
+    lc1 === inp;
+
+}
+
+
+component toBin(3) main;