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