1
 2
 3template BabyAdd() {
 4    signal input x1;
 5    signal input y1;
 6    signal input x2;
 7    signal input y2;
 8    signal output xout;
 9    signal output yout;
10
11    signal beta;
12    signal gamma;
13    signal delta;
14    signal tau;
15
16    var a = 168700;
17    var d = 168696;
18
19    beta <== x1*y2;
20    gamma <== y1*x2;
21    delta <== (-a*x1+y1)*(x2 + y2);
22    tau <== beta * gamma;
23
24    xout <-- (beta + gamma) / (1+ d*tau);
25    (1+ d*tau) * xout === (beta + gamma);
26
27    yout <-- (delta + a*beta - gamma) / (1-d*tau);
28    (1-d*tau)*yout === (delta + a*beta - gamma);
29}
30
31template BabyDbl() {
32    signal input x;
33    signal input y;
34    signal output xout;
35    signal output yout;
36
37    component adder = BabyAdd();
38    adder.x1 <== x;
39    adder.y1 <== y;
40    adder.x2 <== x;
41    adder.y2 <== y;
42
43    adder.xout ==> xout;
44    adder.yout ==> yout;
45}
46
47
48template BabyCheck() {
49    signal input x;
50    signal input y;
51
52    signal x2;
53    signal y2;
54
55    var a = 168700;
56    var d = 168696;
57
58    x2 <== x*x;
59    y2 <== y*y;
60
61    a*x2 + y2 === 1 + d*x2*y2;
62}