aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/solinas32_2e338m15/femulDisplay.log
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-01 23:11:41 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-11-01 23:11:41 -0400
commitb0ee1d0e200654042e52cd125a7a07884026aa98 (patch)
treea1788cf0436a712ce531119c863712cd4c3f46e1 /src/Specific/solinas32_2e338m15/femulDisplay.log
parent3e808d79ad4ff9be1d538f6de8ff531da545b80d (diff)
Update display logs
Diffstat (limited to 'src/Specific/solinas32_2e338m15/femulDisplay.log')
-rw-r--r--src/Specific/solinas32_2e338m15/femulDisplay.log126
1 files changed, 61 insertions, 65 deletions
diff --git a/src/Specific/solinas32_2e338m15/femulDisplay.log b/src/Specific/solinas32_2e338m15/femulDisplay.log
index 56393ea9e..8de8577af 100644
--- a/src/Specific/solinas32_2e338m15/femulDisplay.log
+++ b/src/Specific/solinas32_2e338m15/femulDisplay.log
@@ -1,68 +1,64 @@
-λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32,
+λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32,
Interp-η
(λ var : Syntax.base_type → Type,
- λ '(x28, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x54, x55, x53, x51, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31))%core,
- uint64_t x56 = (uint64_t) x5 * x54 + (0x2 * ((uint64_t) x7 * x55) + (0x2 * ((uint64_t) x9 * x53) + (0x2 * ((uint64_t) x11 * x51) + (0x2 * ((uint64_t) x13 * x49) + (0x2 * ((uint64_t) x15 * x47) + ((uint64_t) x17 * x45 + ((uint64_t) x19 * x43 + (0x2 * ((uint64_t) x21 * x41) + (0x2 * ((uint64_t) x23 * x39) + (0x2 * ((uint64_t) x25 * x37) + (0x2 * ((uint64_t) x27 * x35) + (0x2 * ((uint64_t) x29 * x33) + (uint64_t) x28 * x31))))))))))));
- uint64_t x57 = (uint64_t) x5 * x55 + (0x2 * ((uint64_t) x7 * x53) + (0x2 * ((uint64_t) x9 * x51) + (0x2 * ((uint64_t) x11 * x49) + (0x2 * ((uint64_t) x13 * x47) + ((uint64_t) x15 * x45 + ((uint64_t) x17 * x43 + ((uint64_t) x19 * x41 + (0x2 * ((uint64_t) x21 * x39) + (0x2 * ((uint64_t) x23 * x37) + (0x2 * ((uint64_t) x25 * x35) + (0x2 * ((uint64_t) x27 * x33) + (uint64_t) x29 * x31))))))))))) + 0xf * ((uint64_t) x28 * x54);
- uint64_t x58 = (uint64_t) x5 * x53 + (0x2 * ((uint64_t) x7 * x51) + (0x2 * ((uint64_t) x9 * x49) + (0x2 * ((uint64_t) x11 * x47) + ((uint64_t) x13 * x45 + ((uint64_t) x15 * x43 + ((uint64_t) x17 * x41 + ((uint64_t) x19 * x39 + (0x2 * ((uint64_t) x21 * x37) + (0x2 * ((uint64_t) x23 * x35) + (0x2 * ((uint64_t) x25 * x33) + (uint64_t) x27 * x31)))))))))) + 0xf * ((uint64_t) x29 * x54 + (uint64_t) x28 * x55);
- uint64_t x59 = (uint64_t) x5 * x51 + (0x2 * ((uint64_t) x7 * x49) + (0x2 * ((uint64_t) x9 * x47) + ((uint64_t) x11 * x45 + ((uint64_t) x13 * x43 + ((uint64_t) x15 * x41 + ((uint64_t) x17 * x39 + ((uint64_t) x19 * x37 + (0x2 * ((uint64_t) x21 * x35) + (0x2 * ((uint64_t) x23 * x33) + (uint64_t) x25 * x31))))))))) + 0xf * ((uint64_t) x27 * x54 + ((uint64_t) x29 * x55 + (uint64_t) x28 * x53));
- uint64_t x60 = (uint64_t) x5 * x49 + (0x2 * ((uint64_t) x7 * x47) + ((uint64_t) x9 * x45 + ((uint64_t) x11 * x43 + ((uint64_t) x13 * x41 + ((uint64_t) x15 * x39 + ((uint64_t) x17 * x37 + ((uint64_t) x19 * x35 + (0x2 * ((uint64_t) x21 * x33) + (uint64_t) x23 * x31)))))))) + 0xf * ((uint64_t) x25 * x54 + ((uint64_t) x27 * x55 + ((uint64_t) x29 * x53 + (uint64_t) x28 * x51)));
- uint64_t x61 = (uint64_t) x5 * x47 + ((uint64_t) x7 * x45 + ((uint64_t) x9 * x43 + ((uint64_t) x11 * x41 + ((uint64_t) x13 * x39 + ((uint64_t) x15 * x37 + ((uint64_t) x17 * x35 + ((uint64_t) x19 * x33 + (uint64_t) x21 * x31))))))) + 0xf * ((uint64_t) x23 * x54 + ((uint64_t) x25 * x55 + ((uint64_t) x27 * x53 + ((uint64_t) x29 * x51 + (uint64_t) x28 * x49))));
- uint64_t x62 = (uint64_t) x5 * x45 + (0x2 * ((uint64_t) x7 * x43) + (0x2 * ((uint64_t) x9 * x41) + (0x2 * ((uint64_t) x11 * x39) + (0x2 * ((uint64_t) x13 * x37) + (0x2 * ((uint64_t) x15 * x35) + (0x2 * ((uint64_t) x17 * x33) + (uint64_t) x19 * x31)))))) + 0xf * (0x2 * ((uint64_t) x21 * x54) + (0x2 * ((uint64_t) x23 * x55) + (0x2 * ((uint64_t) x25 * x53) + (0x2 * ((uint64_t) x27 * x51) + (0x2 * ((uint64_t) x29 * x49) + 0x2 * ((uint64_t) x28 * x47))))));
- uint64_t x63 = (uint64_t) x5 * x43 + (0x2 * ((uint64_t) x7 * x41) + (0x2 * ((uint64_t) x9 * x39) + (0x2 * ((uint64_t) x11 * x37) + (0x2 * ((uint64_t) x13 * x35) + (0x2 * ((uint64_t) x15 * x33) + (uint64_t) x17 * x31))))) + 0xf * ((uint64_t) x19 * x54 + (0x2 * ((uint64_t) x21 * x55) + (0x2 * ((uint64_t) x23 * x53) + (0x2 * ((uint64_t) x25 * x51) + (0x2 * ((uint64_t) x27 * x49) + (0x2 * ((uint64_t) x29 * x47) + (uint64_t) x28 * x45))))));
- uint64_t x64 = (uint64_t) x5 * x41 + (0x2 * ((uint64_t) x7 * x39) + (0x2 * ((uint64_t) x9 * x37) + (0x2 * ((uint64_t) x11 * x35) + (0x2 * ((uint64_t) x13 * x33) + (uint64_t) x15 * x31)))) + 0xf * ((uint64_t) x17 * x54 + ((uint64_t) x19 * x55 + (0x2 * ((uint64_t) x21 * x53) + (0x2 * ((uint64_t) x23 * x51) + (0x2 * ((uint64_t) x25 * x49) + (0x2 * ((uint64_t) x27 * x47) + ((uint64_t) x29 * x45 + (uint64_t) x28 * x43)))))));
- uint64_t x65 = (uint64_t) x5 * x39 + (0x2 * ((uint64_t) x7 * x37) + (0x2 * ((uint64_t) x9 * x35) + (0x2 * ((uint64_t) x11 * x33) + (uint64_t) x13 * x31))) + 0xf * ((uint64_t) x15 * x54 + ((uint64_t) x17 * x55 + ((uint64_t) x19 * x53 + (0x2 * ((uint64_t) x21 * x51) + (0x2 * ((uint64_t) x23 * x49) + (0x2 * ((uint64_t) x25 * x47) + ((uint64_t) x27 * x45 + ((uint64_t) x29 * x43 + (uint64_t) x28 * x41))))))));
- uint64_t x66 = (uint64_t) x5 * x37 + (0x2 * ((uint64_t) x7 * x35) + (0x2 * ((uint64_t) x9 * x33) + (uint64_t) x11 * x31)) + 0xf * ((uint64_t) x13 * x54 + ((uint64_t) x15 * x55 + ((uint64_t) x17 * x53 + ((uint64_t) x19 * x51 + (0x2 * ((uint64_t) x21 * x49) + (0x2 * ((uint64_t) x23 * x47) + ((uint64_t) x25 * x45 + ((uint64_t) x27 * x43 + ((uint64_t) x29 * x41 + (uint64_t) x28 * x39)))))))));
- uint64_t x67 = (uint64_t) x5 * x35 + (0x2 * ((uint64_t) x7 * x33) + (uint64_t) x9 * x31) + 0xf * ((uint64_t) x11 * x54 + ((uint64_t) x13 * x55 + ((uint64_t) x15 * x53 + ((uint64_t) x17 * x51 + ((uint64_t) x19 * x49 + (0x2 * ((uint64_t) x21 * x47) + ((uint64_t) x23 * x45 + ((uint64_t) x25 * x43 + ((uint64_t) x27 * x41 + ((uint64_t) x29 * x39 + (uint64_t) x28 * x37))))))))));
- uint64_t x68 = (uint64_t) x5 * x33 + (uint64_t) x7 * x31 + 0xf * ((uint64_t) x9 * x54 + ((uint64_t) x11 * x55 + ((uint64_t) x13 * x53 + ((uint64_t) x15 * x51 + ((uint64_t) x17 * x49 + ((uint64_t) x19 * x47 + ((uint64_t) x21 * x45 + ((uint64_t) x23 * x43 + ((uint64_t) x25 * x41 + ((uint64_t) x27 * x39 + ((uint64_t) x29 * x37 + (uint64_t) x28 * x35)))))))))));
- uint64_t x69 = (uint64_t) x5 * x31 + 0xf * (0x2 * ((uint64_t) x7 * x54) + (0x2 * ((uint64_t) x9 * x55) + (0x2 * ((uint64_t) x11 * x53) + (0x2 * ((uint64_t) x13 * x51) + (0x2 * ((uint64_t) x15 * x49) + (0x2 * ((uint64_t) x17 * x47) + ((uint64_t) x19 * x45 + (0x2 * ((uint64_t) x21 * x43) + (0x2 * ((uint64_t) x23 * x41) + (0x2 * ((uint64_t) x25 * x39) + (0x2 * ((uint64_t) x27 * x37) + (0x2 * ((uint64_t) x29 * x35) + 0x2 * ((uint64_t) x28 * x33)))))))))))));
- uint64_t x70 = x69 >> 0x19;
- uint32_t x71 = (uint32_t) x69 & 0x1ffffff;
- uint64_t x72 = x70 + x68;
- uint64_t x73 = x72 >> 0x18;
- uint32_t x74 = (uint32_t) x72 & 0xffffff;
- uint64_t x75 = x73 + x67;
- uint64_t x76 = x75 >> 0x18;
- uint32_t x77 = (uint32_t) x75 & 0xffffff;
- uint64_t x78 = x76 + x66;
- uint64_t x79 = x78 >> 0x18;
- uint32_t x80 = (uint32_t) x78 & 0xffffff;
- uint64_t x81 = x79 + x65;
- uint64_t x82 = x81 >> 0x18;
- uint32_t x83 = (uint32_t) x81 & 0xffffff;
- uint64_t x84 = x82 + x64;
- uint64_t x85 = x84 >> 0x18;
- uint32_t x86 = (uint32_t) x84 & 0xffffff;
- uint64_t x87 = x85 + x63;
- uint64_t x88 = x87 >> 0x18;
- uint32_t x89 = (uint32_t) x87 & 0xffffff;
- uint64_t x90 = x88 + x62;
- uint32_t x91 = (uint32_t) (x90 >> 0x19);
- uint32_t x92 = (uint32_t) x90 & 0x1ffffff;
- uint64_t x93 = x91 + x61;
- uint32_t x94 = (uint32_t) (x93 >> 0x18);
- uint32_t x95 = (uint32_t) x93 & 0xffffff;
- uint64_t x96 = x94 + x60;
- uint32_t x97 = (uint32_t) (x96 >> 0x18);
- uint32_t x98 = (uint32_t) x96 & 0xffffff;
- uint64_t x99 = x97 + x59;
- uint32_t x100 = (uint32_t) (x99 >> 0x18);
- uint32_t x101 = (uint32_t) x99 & 0xffffff;
- uint64_t x102 = x100 + x58;
- uint32_t x103 = (uint32_t) (x102 >> 0x18);
- uint32_t x104 = (uint32_t) x102 & 0xffffff;
- uint64_t x105 = x103 + x57;
- uint32_t x106 = (uint32_t) (x105 >> 0x18);
- uint32_t x107 = (uint32_t) x105 & 0xffffff;
- uint64_t x108 = x106 + x56;
- uint32_t x109 = (uint32_t) (x108 >> 0x18);
- uint32_t x110 = (uint32_t) x108 & 0xffffff;
- uint64_t x111 = x71 + (uint64_t) 0xf * x109;
- uint32_t x112 = (uint32_t) (x111 >> 0x19);
- uint32_t x113 = (uint32_t) x111 & 0x1ffffff;
- uint32_t x114 = x112 + x74;
- uint32_t x115 = x114 >> 0x18;
- uint32_t x116 = x114 & 0xffffff;
- return (Return x110, Return x107, Return x104, Return x101, Return x98, Return x95, Return x92, Return x89, Return x86, Return x83, Return x80, x115 + x77, Return x116, Return x113))
+ λ '(x26, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x50, x51, x49, x47, x45, x43, x41, x39, x37, x35, x33, x31, x29))%core,
+ uint64_t x52 = (((uint64_t)x5 * x50) + (((uint64_t)x7 * x51) + (((uint64_t)x9 * x49) + (((uint64_t)x11 * x47) + (((uint64_t)x13 * x45) + (((uint64_t)x15 * x43) + (((uint64_t)x17 * x41) + (((uint64_t)x19 * x39) + (((uint64_t)x21 * x37) + (((uint64_t)x23 * x35) + (((uint64_t)x25 * x33) + (((uint64_t)x27 * x31) + ((uint64_t)x26 * x29)))))))))))));
+ uint64_t x53 = ((((uint64_t)x5 * x51) + (((uint64_t)x7 * x49) + (((uint64_t)x9 * x47) + (((uint64_t)x11 * x45) + (((uint64_t)x13 * x43) + (((uint64_t)x15 * x41) + (((uint64_t)x17 * x39) + (((uint64_t)x19 * x37) + (((uint64_t)x21 * x35) + (((uint64_t)x23 * x33) + (((uint64_t)x25 * x31) + ((uint64_t)x27 * x29)))))))))))) + (0xf * ((uint64_t)x26 * x50)));
+ uint64_t x54 = ((((uint64_t)x5 * x49) + (((uint64_t)x7 * x47) + (((uint64_t)x9 * x45) + (((uint64_t)x11 * x43) + (((uint64_t)x13 * x41) + (((uint64_t)x15 * x39) + (((uint64_t)x17 * x37) + (((uint64_t)x19 * x35) + (((uint64_t)x21 * x33) + (((uint64_t)x23 * x31) + ((uint64_t)x25 * x29))))))))))) + (0xf * (((uint64_t)x27 * x50) + ((uint64_t)x26 * x51))));
+ uint64_t x55 = ((((uint64_t)x5 * x47) + (((uint64_t)x7 * x45) + (((uint64_t)x9 * x43) + (((uint64_t)x11 * x41) + (((uint64_t)x13 * x39) + (((uint64_t)x15 * x37) + (((uint64_t)x17 * x35) + (((uint64_t)x19 * x33) + (((uint64_t)x21 * x31) + ((uint64_t)x23 * x29)))))))))) + (0xf * (((uint64_t)x25 * x50) + (((uint64_t)x27 * x51) + ((uint64_t)x26 * x49)))));
+ uint64_t x56 = ((((uint64_t)x5 * x45) + (((uint64_t)x7 * x43) + (((uint64_t)x9 * x41) + (((uint64_t)x11 * x39) + (((uint64_t)x13 * x37) + (((uint64_t)x15 * x35) + (((uint64_t)x17 * x33) + (((uint64_t)x19 * x31) + ((uint64_t)x21 * x29))))))))) + (0xf * (((uint64_t)x23 * x50) + (((uint64_t)x25 * x51) + (((uint64_t)x27 * x49) + ((uint64_t)x26 * x47))))));
+ uint64_t x57 = ((((uint64_t)x5 * x43) + (((uint64_t)x7 * x41) + (((uint64_t)x9 * x39) + (((uint64_t)x11 * x37) + (((uint64_t)x13 * x35) + (((uint64_t)x15 * x33) + (((uint64_t)x17 * x31) + ((uint64_t)x19 * x29)))))))) + (0xf * (((uint64_t)x21 * x50) + (((uint64_t)x23 * x51) + (((uint64_t)x25 * x49) + (((uint64_t)x27 * x47) + ((uint64_t)x26 * x45)))))));
+ uint64_t x58 = ((((uint64_t)x5 * x41) + (((uint64_t)x7 * x39) + (((uint64_t)x9 * x37) + (((uint64_t)x11 * x35) + (((uint64_t)x13 * x33) + (((uint64_t)x15 * x31) + ((uint64_t)x17 * x29))))))) + (0xf * (((uint64_t)x19 * x50) + (((uint64_t)x21 * x51) + (((uint64_t)x23 * x49) + (((uint64_t)x25 * x47) + (((uint64_t)x27 * x45) + ((uint64_t)x26 * x43))))))));
+ uint64_t x59 = ((((uint64_t)x5 * x39) + (((uint64_t)x7 * x37) + (((uint64_t)x9 * x35) + (((uint64_t)x11 * x33) + (((uint64_t)x13 * x31) + ((uint64_t)x15 * x29)))))) + (0xf * (((uint64_t)x17 * x50) + (((uint64_t)x19 * x51) + (((uint64_t)x21 * x49) + (((uint64_t)x23 * x47) + (((uint64_t)x25 * x45) + (((uint64_t)x27 * x43) + ((uint64_t)x26 * x41)))))))));
+ uint64_t x60 = ((((uint64_t)x5 * x37) + (((uint64_t)x7 * x35) + (((uint64_t)x9 * x33) + (((uint64_t)x11 * x31) + ((uint64_t)x13 * x29))))) + (0xf * (((uint64_t)x15 * x50) + (((uint64_t)x17 * x51) + (((uint64_t)x19 * x49) + (((uint64_t)x21 * x47) + (((uint64_t)x23 * x45) + (((uint64_t)x25 * x43) + (((uint64_t)x27 * x41) + ((uint64_t)x26 * x39))))))))));
+ uint64_t x61 = ((((uint64_t)x5 * x35) + (((uint64_t)x7 * x33) + (((uint64_t)x9 * x31) + ((uint64_t)x11 * x29)))) + (0xf * (((uint64_t)x13 * x50) + (((uint64_t)x15 * x51) + (((uint64_t)x17 * x49) + (((uint64_t)x19 * x47) + (((uint64_t)x21 * x45) + (((uint64_t)x23 * x43) + (((uint64_t)x25 * x41) + (((uint64_t)x27 * x39) + ((uint64_t)x26 * x37)))))))))));
+ uint64_t x62 = ((((uint64_t)x5 * x33) + (((uint64_t)x7 * x31) + ((uint64_t)x9 * x29))) + (0xf * (((uint64_t)x11 * x50) + (((uint64_t)x13 * x51) + (((uint64_t)x15 * x49) + (((uint64_t)x17 * x47) + (((uint64_t)x19 * x45) + (((uint64_t)x21 * x43) + (((uint64_t)x23 * x41) + (((uint64_t)x25 * x39) + (((uint64_t)x27 * x37) + ((uint64_t)x26 * x35))))))))))));
+ uint64_t x63 = ((((uint64_t)x5 * x31) + ((uint64_t)x7 * x29)) + (0xf * (((uint64_t)x9 * x50) + (((uint64_t)x11 * x51) + (((uint64_t)x13 * x49) + (((uint64_t)x15 * x47) + (((uint64_t)x17 * x45) + (((uint64_t)x19 * x43) + (((uint64_t)x21 * x41) + (((uint64_t)x23 * x39) + (((uint64_t)x25 * x37) + (((uint64_t)x27 * x35) + ((uint64_t)x26 * x33)))))))))))));
+ uint64_t x64 = (((uint64_t)x5 * x29) + (0xf * (((uint64_t)x7 * x50) + (((uint64_t)x9 * x51) + (((uint64_t)x11 * x49) + (((uint64_t)x13 * x47) + (((uint64_t)x15 * x45) + (((uint64_t)x17 * x43) + (((uint64_t)x19 * x41) + (((uint64_t)x21 * x39) + (((uint64_t)x23 * x37) + (((uint64_t)x25 * x35) + (((uint64_t)x27 * x33) + ((uint64_t)x26 * x31))))))))))))));
+ uint64_t x65 = (x64 >> 0x1a);
+ uint32_t x66 = ((uint32_t)x64 & 0x3ffffff);
+ uint64_t x67 = (x65 + x63);
+ uint64_t x68 = (x67 >> 0x1a);
+ uint32_t x69 = ((uint32_t)x67 & 0x3ffffff);
+ uint64_t x70 = (x68 + x62);
+ uint64_t x71 = (x70 >> 0x1a);
+ uint32_t x72 = ((uint32_t)x70 & 0x3ffffff);
+ uint64_t x73 = (x71 + x61);
+ uint64_t x74 = (x73 >> 0x1a);
+ uint32_t x75 = ((uint32_t)x73 & 0x3ffffff);
+ uint64_t x76 = (x74 + x60);
+ uint64_t x77 = (x76 >> 0x1a);
+ uint32_t x78 = ((uint32_t)x76 & 0x3ffffff);
+ uint64_t x79 = (x77 + x59);
+ uint64_t x80 = (x79 >> 0x1a);
+ uint32_t x81 = ((uint32_t)x79 & 0x3ffffff);
+ uint64_t x82 = (x80 + x58);
+ uint64_t x83 = (x82 >> 0x1a);
+ uint32_t x84 = ((uint32_t)x82 & 0x3ffffff);
+ uint64_t x85 = (x83 + x57);
+ uint64_t x86 = (x85 >> 0x1a);
+ uint32_t x87 = ((uint32_t)x85 & 0x3ffffff);
+ uint64_t x88 = (x86 + x56);
+ uint64_t x89 = (x88 >> 0x1a);
+ uint32_t x90 = ((uint32_t)x88 & 0x3ffffff);
+ uint64_t x91 = (x89 + x55);
+ uint64_t x92 = (x91 >> 0x1a);
+ uint32_t x93 = ((uint32_t)x91 & 0x3ffffff);
+ uint64_t x94 = (x92 + x54);
+ uint64_t x95 = (x94 >> 0x1a);
+ uint32_t x96 = ((uint32_t)x94 & 0x3ffffff);
+ uint64_t x97 = (x95 + x53);
+ uint64_t x98 = (x97 >> 0x1a);
+ uint32_t x99 = ((uint32_t)x97 & 0x3ffffff);
+ uint64_t x100 = (x98 + x52);
+ uint64_t x101 = (x100 >> 0x1a);
+ uint32_t x102 = ((uint32_t)x100 & 0x3ffffff);
+ uint64_t x103 = (x66 + (0xf * x101));
+ uint32_t x104 = (uint32_t) (x103 >> 0x1a);
+ uint32_t x105 = ((uint32_t)x103 & 0x3ffffff);
+ uint32_t x106 = (x104 + x69);
+ uint32_t x107 = (x106 >> 0x1a);
+ uint32_t x108 = (x106 & 0x3ffffff);
+ return (Return x102, Return x99, Return x96, Return x93, Return x90, Return x87, Return x84, Return x81, Return x78, Return x75, (x107 + x72), Return x108, Return x105))
(x, x0)%core
- : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)
+ : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 → ReturnType (uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)