1 files changed, 0 insertions, 100 deletions
diff --git a/src/Specific/solinas32_2e511m187_22limbs/femulDisplay.log b/src/Specific/solinas32_2e511m187_22limbs/femulDisplay.log
deleted file mode 100644
index ae153fcc0..000000000
--- a/src/Specific/solinas32_2e511m187_22limbs/femulDisplay.log
+++ /dev/null
@@ -1,100 +0,0 @@
-λ x x0 : word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32 * word32,
-Interp-η
-(λ var : Syntax.base_type → Type,
- λ '(x44, x45, x43, x41, x39, x37, x35, x33, x31, x29, x27, x25, x23, x21, x19, x17, x15, x13, x11, x9, x7, x5, (x86, x87, x85, x83, x81, x79, x77, x75, x73, x71, x69, x67, x65, x63, x61, x59, x57, x55, x53, x51, x49, x47))%core,
- uint64_t x88 = (((uint64_t)x5 * x86) + ((0x2 * ((uint64_t)x7 * x87)) + ((0x2 * ((uint64_t)x9 * x85)) + ((0x2 * ((uint64_t)x11 * x83)) + (((uint64_t)x13 * x81) + ((0x2 * ((uint64_t)x15 * x79)) + ((0x2 * ((uint64_t)x17 * x77)) + ((0x2 * ((uint64_t)x19 * x75)) + (((uint64_t)x21 * x73) + ((0x2 * ((uint64_t)x23 * x71)) + ((0x2 * ((uint64_t)x25 * x69)) + ((0x2 * ((uint64_t)x27 * x67)) + ((0x2 * ((uint64_t)x29 * x65)) + (((uint64_t)x31 * x63) + ((0x2 * ((uint64_t)x33 * x61)) + ((0x2 * ((uint64_t)x35 * x59)) + ((0x2 * ((uint64_t)x37 * x57)) + (((uint64_t)x39 * x55) + ((0x2 * ((uint64_t)x41 * x53)) + ((0x2 * ((uint64_t)x43 * x51)) + ((0x2 * ((uint64_t)x45 * x49)) + ((uint64_t)x44 * x47))))))))))))))))))))));
- uint64_t x89 = ((((uint64_t)x5 * x87) + ((0x2 * ((uint64_t)x7 * x85)) + ((0x2 * ((uint64_t)x9 * x83)) + (((uint64_t)x11 * x81) + (((uint64_t)x13 * x79) + ((0x2 * ((uint64_t)x15 * x77)) + ((0x2 * ((uint64_t)x17 * x75)) + (((uint64_t)x19 * x73) + (((uint64_t)x21 * x71) + ((0x2 * ((uint64_t)x23 * x69)) + ((0x2 * ((uint64_t)x25 * x67)) + ((0x2 * ((uint64_t)x27 * x65)) + (((uint64_t)x29 * x63) + (((uint64_t)x31 * x61) + ((0x2 * ((uint64_t)x33 * x59)) + ((0x2 * ((uint64_t)x35 * x57)) + (((uint64_t)x37 * x55) + (((uint64_t)x39 * x53) + ((0x2 * ((uint64_t)x41 * x51)) + ((0x2 * ((uint64_t)x43 * x49)) + ((uint64_t)x45 * x47))))))))))))))))))))) + (0xbb * ((uint64_t)x44 * x86)));
- uint64_t x90 = ((((uint64_t)x5 * x85) + ((0x2 * ((uint64_t)x7 * x83)) + (((uint64_t)x9 * x81) + (((uint64_t)x11 * x79) + (((uint64_t)x13 * x77) + ((0x2 * ((uint64_t)x15 * x75)) + (((uint64_t)x17 * x73) + (((uint64_t)x19 * x71) + (((uint64_t)x21 * x69) + ((0x2 * ((uint64_t)x23 * x67)) + ((0x2 * ((uint64_t)x25 * x65)) + (((uint64_t)x27 * x63) + (((uint64_t)x29 * x61) + (((uint64_t)x31 * x59) + ((0x2 * ((uint64_t)x33 * x57)) + (((uint64_t)x35 * x55) + (((uint64_t)x37 * x53) + (((uint64_t)x39 * x51) + ((0x2 * ((uint64_t)x41 * x49)) + ((uint64_t)x43 * x47)))))))))))))))))))) + (0xbb * (((uint64_t)x45 * x86) + ((uint64_t)x44 * x87))));
- uint64_t x91 = ((((uint64_t)x5 * x83) + (((uint64_t)x7 * x81) + (((uint64_t)x9 * x79) + (((uint64_t)x11 * x77) + (((uint64_t)x13 * x75) + (((uint64_t)x15 * x73) + (((uint64_t)x17 * x71) + (((uint64_t)x19 * x69) + (((uint64_t)x21 * x67) + ((0x2 * ((uint64_t)x23 * x65)) + (((uint64_t)x25 * x63) + (((uint64_t)x27 * x61) + (((uint64_t)x29 * x59) + (((uint64_t)x31 * x57) + (((uint64_t)x33 * x55) + (((uint64_t)x35 * x53) + (((uint64_t)x37 * x51) + (((uint64_t)x39 * x49) + ((uint64_t)x41 * x47))))))))))))))))))) + (0xbb * (((uint64_t)x43 * x86) + (((uint64_t)x45 * x87) + ((uint64_t)x44 * x85)))));
- uint64_t x92 = ((((uint64_t)x5 * x81) + ((0x2 * ((uint64_t)x7 * x79)) + ((0x2 * ((uint64_t)x9 * x77)) + ((0x2 * ((uint64_t)x11 * x75)) + (((uint64_t)x13 * x73) + ((0x2 * ((uint64_t)x15 * x71)) + ((0x2 * ((uint64_t)x17 * x69)) + ((0x2 * ((uint64_t)x19 * x67)) + ((0x2 * ((uint64_t)x21 * x65)) + ((0x2 * ((uint64_t)x23 * x63)) + ((0x2 * ((uint64_t)x25 * x61)) + ((0x2 * ((uint64_t)x27 * x59)) + ((0x2 * ((uint64_t)x29 * x57)) + (((uint64_t)x31 * x55) + ((0x2 * ((uint64_t)x33 * x53)) + ((0x2 * ((uint64_t)x35 * x51)) + ((0x2 * ((uint64_t)x37 * x49)) + ((uint64_t)x39 * x47)))))))))))))))))) + (0xbb * ((0x2 * ((uint64_t)x41 * x86)) + ((0x2 * ((uint64_t)x43 * x87)) + ((0x2 * ((uint64_t)x45 * x85)) + (0x2 * ((uint64_t)x44 * x83)))))));
- uint64_t x93 = ((((uint64_t)x5 * x79) + ((0x2 * ((uint64_t)x7 * x77)) + ((0x2 * ((uint64_t)x9 * x75)) + (((uint64_t)x11 * x73) + (((uint64_t)x13 * x71) + ((0x2 * ((uint64_t)x15 * x69)) + ((0x2 * ((uint64_t)x17 * x67)) + ((0x2 * ((uint64_t)x19 * x65)) + (((uint64_t)x21 * x63) + ((0x2 * ((uint64_t)x23 * x61)) + ((0x2 * ((uint64_t)x25 * x59)) + ((0x2 * ((uint64_t)x27 * x57)) + (((uint64_t)x29 * x55) + (((uint64_t)x31 * x53) + ((0x2 * ((uint64_t)x33 * x51)) + ((0x2 * ((uint64_t)x35 * x49)) + ((uint64_t)x37 * x47))))))))))))))))) + (0xbb * (((uint64_t)x39 * x86) + ((0x2 * ((uint64_t)x41 * x87)) + ((0x2 * ((uint64_t)x43 * x85)) + ((0x2 * ((uint64_t)x45 * x83)) + ((uint64_t)x44 * x81)))))));
- uint64_t x94 = ((((uint64_t)x5 * x77) + ((0x2 * ((uint64_t)x7 * x75)) + (((uint64_t)x9 * x73) + (((uint64_t)x11 * x71) + (((uint64_t)x13 * x69) + ((0x2 * ((uint64_t)x15 * x67)) + ((0x2 * ((uint64_t)x17 * x65)) + (((uint64_t)x19 * x63) + (((uint64_t)x21 * x61) + ((0x2 * ((uint64_t)x23 * x59)) + ((0x2 * ((uint64_t)x25 * x57)) + (((uint64_t)x27 * x55) + (((uint64_t)x29 * x53) + (((uint64_t)x31 * x51) + ((0x2 * ((uint64_t)x33 * x49)) + ((uint64_t)x35 * x47)))))))))))))))) + (0xbb * (((uint64_t)x37 * x86) + (((uint64_t)x39 * x87) + ((0x2 * ((uint64_t)x41 * x85)) + ((0x2 * ((uint64_t)x43 * x83)) + (((uint64_t)x45 * x81) + ((uint64_t)x44 * x79))))))));
- uint64_t x95 = ((((uint64_t)x5 * x75) + (((uint64_t)x7 * x73) + (((uint64_t)x9 * x71) + (((uint64_t)x11 * x69) + (((uint64_t)x13 * x67) + ((0x2 * ((uint64_t)x15 * x65)) + (((uint64_t)x17 * x63) + (((uint64_t)x19 * x61) + (((uint64_t)x21 * x59) + ((0x2 * ((uint64_t)x23 * x57)) + (((uint64_t)x25 * x55) + (((uint64_t)x27 * x53) + (((uint64_t)x29 * x51) + (((uint64_t)x31 * x49) + ((uint64_t)x33 * x47))))))))))))))) + (0xbb * (((uint64_t)x35 * x86) + (((uint64_t)x37 * x87) + (((uint64_t)x39 * x85) + ((0x2 * ((uint64_t)x41 * x83)) + (((uint64_t)x43 * x81) + (((uint64_t)x45 * x79) + ((uint64_t)x44 * x77)))))))));
- uint64_t x96 = ((((uint64_t)x5 * x73) + ((0x2 * ((uint64_t)x7 * x71)) + ((0x2 * ((uint64_t)x9 * x69)) + ((0x2 * ((uint64_t)x11 * x67)) + ((0x2 * ((uint64_t)x13 * x65)) + ((0x2 * ((uint64_t)x15 * x63)) + ((0x2 * ((uint64_t)x17 * x61)) + ((0x2 * ((uint64_t)x19 * x59)) + ((0x2 * ((uint64_t)x21 * x57)) + ((0x2 * ((uint64_t)x23 * x55)) + ((0x2 * ((uint64_t)x25 * x53)) + ((0x2 * ((uint64_t)x27 * x51)) + ((0x2 * ((uint64_t)x29 * x49)) + ((uint64_t)x31 * x47)))))))))))))) + (0xbb * ((0x2 * ((uint64_t)x33 * x86)) + ((0x2 * ((uint64_t)x35 * x87)) + ((0x2 * ((uint64_t)x37 * x85)) + ((0x2 * ((uint64_t)x39 * x83)) + ((0x2 * ((uint64_t)x41 * x81)) + ((0x2 * ((uint64_t)x43 * x79)) + ((0x2 * ((uint64_t)x45 * x77)) + (0x2 * ((uint64_t)x44 * x75)))))))))));
- uint64_t x97 = ((((uint64_t)x5 * x71) + ((0x2 * ((uint64_t)x7 * x69)) + ((0x2 * ((uint64_t)x9 * x67)) + ((0x2 * ((uint64_t)x11 * x65)) + (((uint64_t)x13 * x63) + ((0x2 * ((uint64_t)x15 * x61)) + ((0x2 * ((uint64_t)x17 * x59)) + ((0x2 * ((uint64_t)x19 * x57)) + (((uint64_t)x21 * x55) + ((0x2 * ((uint64_t)x23 * x53)) + ((0x2 * ((uint64_t)x25 * x51)) + ((0x2 * ((uint64_t)x27 * x49)) + ((uint64_t)x29 * x47))))))))))))) + (0xbb * (((uint64_t)x31 * x86) + ((0x2 * ((uint64_t)x33 * x87)) + ((0x2 * ((uint64_t)x35 * x85)) + ((0x2 * ((uint64_t)x37 * x83)) + (((uint64_t)x39 * x81) + ((0x2 * ((uint64_t)x41 * x79)) + ((0x2 * ((uint64_t)x43 * x77)) + ((0x2 * ((uint64_t)x45 * x75)) + ((uint64_t)x44 * x73)))))))))));
- uint64_t x98 = ((((uint64_t)x5 * x69) + ((0x2 * ((uint64_t)x7 * x67)) + ((0x2 * ((uint64_t)x9 * x65)) + (((uint64_t)x11 * x63) + (((uint64_t)x13 * x61) + ((0x2 * ((uint64_t)x15 * x59)) + ((0x2 * ((uint64_t)x17 * x57)) + (((uint64_t)x19 * x55) + (((uint64_t)x21 * x53) + ((0x2 * ((uint64_t)x23 * x51)) + ((0x2 * ((uint64_t)x25 * x49)) + ((uint64_t)x27 * x47)))))))))))) + (0xbb * (((uint64_t)x29 * x86) + (((uint64_t)x31 * x87) + ((0x2 * ((uint64_t)x33 * x85)) + ((0x2 * ((uint64_t)x35 * x83)) + (((uint64_t)x37 * x81) + (((uint64_t)x39 * x79) + ((0x2 * ((uint64_t)x41 * x77)) + ((0x2 * ((uint64_t)x43 * x75)) + (((uint64_t)x45 * x73) + ((uint64_t)x44 * x71))))))))))));
- uint64_t x99 = ((((uint64_t)x5 * x67) + ((0x2 * ((uint64_t)x7 * x65)) + (((uint64_t)x9 * x63) + (((uint64_t)x11 * x61) + (((uint64_t)x13 * x59) + ((0x2 * ((uint64_t)x15 * x57)) + (((uint64_t)x17 * x55) + (((uint64_t)x19 * x53) + (((uint64_t)x21 * x51) + ((0x2 * ((uint64_t)x23 * x49)) + ((uint64_t)x25 * x47))))))))))) + (0xbb * (((uint64_t)x27 * x86) + (((uint64_t)x29 * x87) + (((uint64_t)x31 * x85) + ((0x2 * ((uint64_t)x33 * x83)) + (((uint64_t)x35 * x81) + (((uint64_t)x37 * x79) + (((uint64_t)x39 * x77) + ((0x2 * ((uint64_t)x41 * x75)) + (((uint64_t)x43 * x73) + (((uint64_t)x45 * x71) + ((uint64_t)x44 * x69)))))))))))));
- uint64_t x100 = ((((uint64_t)x5 * x65) + (((uint64_t)x7 * x63) + (((uint64_t)x9 * x61) + (((uint64_t)x11 * x59) + (((uint64_t)x13 * x57) + (((uint64_t)x15 * x55) + (((uint64_t)x17 * x53) + (((uint64_t)x19 * x51) + (((uint64_t)x21 * x49) + ((uint64_t)x23 * x47)))))))))) + (0xbb * (((uint64_t)x25 * x86) + (((uint64_t)x27 * x87) + (((uint64_t)x29 * x85) + (((uint64_t)x31 * x83) + (((uint64_t)x33 * x81) + (((uint64_t)x35 * x79) + (((uint64_t)x37 * x77) + (((uint64_t)x39 * x75) + (((uint64_t)x41 * x73) + (((uint64_t)x43 * x71) + (((uint64_t)x45 * x69) + ((uint64_t)x44 * x67))))))))))))));
- uint64_t x101 = ((((uint64_t)x5 * x63) + ((0x2 * ((uint64_t)x7 * x61)) + ((0x2 * ((uint64_t)x9 * x59)) + ((0x2 * ((uint64_t)x11 * x57)) + (((uint64_t)x13 * x55) + ((0x2 * ((uint64_t)x15 * x53)) + ((0x2 * ((uint64_t)x17 * x51)) + ((0x2 * ((uint64_t)x19 * x49)) + ((uint64_t)x21 * x47))))))))) + (0xbb * ((0x2 * ((uint64_t)x23 * x86)) + ((0x2 * ((uint64_t)x25 * x87)) + ((0x2 * ((uint64_t)x27 * x85)) + ((0x2 * ((uint64_t)x29 * x83)) + (((uint64_t)x31 * x81) + ((0x2 * ((uint64_t)x33 * x79)) + ((0x2 * ((uint64_t)x35 * x77)) + ((0x2 * ((uint64_t)x37 * x75)) + (((uint64_t)x39 * x73) + ((0x2 * ((uint64_t)x41 * x71)) + ((0x2 * ((uint64_t)x43 * x69)) + ((0x2 * ((uint64_t)x45 * x67)) + (0x2 * ((uint64_t)x44 * x65))))))))))))))));
- uint64_t x102 = ((((uint64_t)x5 * x61) + ((0x2 * ((uint64_t)x7 * x59)) + ((0x2 * ((uint64_t)x9 * x57)) + (((uint64_t)x11 * x55) + (((uint64_t)x13 * x53) + ((0x2 * ((uint64_t)x15 * x51)) + ((0x2 * ((uint64_t)x17 * x49)) + ((uint64_t)x19 * x47)))))))) + (0xbb * (((uint64_t)x21 * x86) + ((0x2 * ((uint64_t)x23 * x87)) + ((0x2 * ((uint64_t)x25 * x85)) + ((0x2 * ((uint64_t)x27 * x83)) + (((uint64_t)x29 * x81) + (((uint64_t)x31 * x79) + ((0x2 * ((uint64_t)x33 * x77)) + ((0x2 * ((uint64_t)x35 * x75)) + (((uint64_t)x37 * x73) + (((uint64_t)x39 * x71) + ((0x2 * ((uint64_t)x41 * x69)) + ((0x2 * ((uint64_t)x43 * x67)) + ((0x2 * ((uint64_t)x45 * x65)) + ((uint64_t)x44 * x63))))))))))))))));
- uint64_t x103 = ((((uint64_t)x5 * x59) + ((0x2 * ((uint64_t)x7 * x57)) + (((uint64_t)x9 * x55) + (((uint64_t)x11 * x53) + (((uint64_t)x13 * x51) + ((0x2 * ((uint64_t)x15 * x49)) + ((uint64_t)x17 * x47))))))) + (0xbb * (((uint64_t)x19 * x86) + (((uint64_t)x21 * x87) + ((0x2 * ((uint64_t)x23 * x85)) + ((0x2 * ((uint64_t)x25 * x83)) + (((uint64_t)x27 * x81) + (((uint64_t)x29 * x79) + (((uint64_t)x31 * x77) + ((0x2 * ((uint64_t)x33 * x75)) + (((uint64_t)x35 * x73) + (((uint64_t)x37 * x71) + (((uint64_t)x39 * x69) + ((0x2 * ((uint64_t)x41 * x67)) + ((0x2 * ((uint64_t)x43 * x65)) + (((uint64_t)x45 * x63) + ((uint64_t)x44 * x61)))))))))))))))));
- uint64_t x104 = ((((uint64_t)x5 * x57) + (((uint64_t)x7 * x55) + (((uint64_t)x9 * x53) + (((uint64_t)x11 * x51) + (((uint64_t)x13 * x49) + ((uint64_t)x15 * x47)))))) + (0xbb * (((uint64_t)x17 * x86) + (((uint64_t)x19 * x87) + (((uint64_t)x21 * x85) + ((0x2 * ((uint64_t)x23 * x83)) + (((uint64_t)x25 * x81) + (((uint64_t)x27 * x79) + (((uint64_t)x29 * x77) + (((uint64_t)x31 * x75) + (((uint64_t)x33 * x73) + (((uint64_t)x35 * x71) + (((uint64_t)x37 * x69) + (((uint64_t)x39 * x67) + ((0x2 * ((uint64_t)x41 * x65)) + (((uint64_t)x43 * x63) + (((uint64_t)x45 * x61) + ((uint64_t)x44 * x59))))))))))))))))));
- uint64_t x105 = ((((uint64_t)x5 * x55) + ((0x2 * ((uint64_t)x7 * x53)) + ((0x2 * ((uint64_t)x9 * x51)) + ((0x2 * ((uint64_t)x11 * x49)) + ((uint64_t)x13 * x47))))) + (0xbb * ((0x2 * ((uint64_t)x15 * x86)) + ((0x2 * ((uint64_t)x17 * x87)) + ((0x2 * ((uint64_t)x19 * x85)) + ((0x2 * ((uint64_t)x21 * x83)) + ((0x2 * ((uint64_t)x23 * x81)) + ((0x2 * ((uint64_t)x25 * x79)) + ((0x2 * ((uint64_t)x27 * x77)) + ((0x2 * ((uint64_t)x29 * x75)) + (((uint64_t)x31 * x73) + ((0x2 * ((uint64_t)x33 * x71)) + ((0x2 * ((uint64_t)x35 * x69)) + ((0x2 * ((uint64_t)x37 * x67)) + ((0x2 * ((uint64_t)x39 * x65)) + ((0x2 * ((uint64_t)x41 * x63)) + ((0x2 * ((uint64_t)x43 * x61)) + ((0x2 * ((uint64_t)x45 * x59)) + (0x2 * ((uint64_t)x44 * x57))))))))))))))))))));
- uint64_t x106 = ((((uint64_t)x5 * x53) + ((0x2 * ((uint64_t)x7 * x51)) + ((0x2 * ((uint64_t)x9 * x49)) + ((uint64_t)x11 * x47)))) + (0xbb * (((uint64_t)x13 * x86) + ((0x2 * ((uint64_t)x15 * x87)) + ((0x2 * ((uint64_t)x17 * x85)) + ((0x2 * ((uint64_t)x19 * x83)) + (((uint64_t)x21 * x81) + ((0x2 * ((uint64_t)x23 * x79)) + ((0x2 * ((uint64_t)x25 * x77)) + ((0x2 * ((uint64_t)x27 * x75)) + (((uint64_t)x29 * x73) + (((uint64_t)x31 * x71) + ((0x2 * ((uint64_t)x33 * x69)) + ((0x2 * ((uint64_t)x35 * x67)) + ((0x2 * ((uint64_t)x37 * x65)) + (((uint64_t)x39 * x63) + ((0x2 * ((uint64_t)x41 * x61)) + ((0x2 * ((uint64_t)x43 * x59)) + ((0x2 * ((uint64_t)x45 * x57)) + ((uint64_t)x44 * x55))))))))))))))))))));
- uint64_t x107 = ((((uint64_t)x5 * x51) + ((0x2 * ((uint64_t)x7 * x49)) + ((uint64_t)x9 * x47))) + (0xbb * (((uint64_t)x11 * x86) + (((uint64_t)x13 * x87) + ((0x2 * ((uint64_t)x15 * x85)) + ((0x2 * ((uint64_t)x17 * x83)) + (((uint64_t)x19 * x81) + (((uint64_t)x21 * x79) + ((0x2 * ((uint64_t)x23 * x77)) + ((0x2 * ((uint64_t)x25 * x75)) + (((uint64_t)x27 * x73) + (((uint64_t)x29 * x71) + (((uint64_t)x31 * x69) + ((0x2 * ((uint64_t)x33 * x67)) + ((0x2 * ((uint64_t)x35 * x65)) + (((uint64_t)x37 * x63) + (((uint64_t)x39 * x61) + ((0x2 * ((uint64_t)x41 * x59)) + ((0x2 * ((uint64_t)x43 * x57)) + (((uint64_t)x45 * x55) + ((uint64_t)x44 * x53)))))))))))))))))))));
- uint64_t x108 = ((((uint64_t)x5 * x49) + ((uint64_t)x7 * x47)) + (0xbb * (((uint64_t)x9 * x86) + (((uint64_t)x11 * x87) + (((uint64_t)x13 * x85) + ((0x2 * ((uint64_t)x15 * x83)) + (((uint64_t)x17 * x81) + (((uint64_t)x19 * x79) + (((uint64_t)x21 * x77) + ((0x2 * ((uint64_t)x23 * x75)) + (((uint64_t)x25 * x73) + (((uint64_t)x27 * x71) + (((uint64_t)x29 * x69) + (((uint64_t)x31 * x67) + ((0x2 * ((uint64_t)x33 * x65)) + (((uint64_t)x35 * x63) + (((uint64_t)x37 * x61) + (((uint64_t)x39 * x59) + ((0x2 * ((uint64_t)x41 * x57)) + (((uint64_t)x43 * x55) + (((uint64_t)x45 * x53) + ((uint64_t)x44 * x51))))))))))))))))))))));
- uint64_t x109 = (((uint64_t)x5 * x47) + (0xbb * ((0x2 * ((uint64_t)x7 * x86)) + ((0x2 * ((uint64_t)x9 * x87)) + ((0x2 * ((uint64_t)x11 * x85)) + ((0x2 * ((uint64_t)x13 * x83)) + ((0x2 * ((uint64_t)x15 * x81)) + ((0x2 * ((uint64_t)x17 * x79)) + ((0x2 * ((uint64_t)x19 * x77)) + ((0x2 * ((uint64_t)x21 * x75)) + ((0x2 * ((uint64_t)x23 * x73)) + ((0x2 * ((uint64_t)x25 * x71)) + ((0x2 * ((uint64_t)x27 * x69)) + ((0x2 * ((uint64_t)x29 * x67)) + ((0x2 * ((uint64_t)x31 * x65)) + ((0x2 * ((uint64_t)x33 * x63)) + ((0x2 * ((uint64_t)x35 * x61)) + ((0x2 * ((uint64_t)x37 * x59)) + ((0x2 * ((uint64_t)x39 * x57)) + ((0x2 * ((uint64_t)x41 * x55)) + ((0x2 * ((uint64_t)x43 * x53)) + ((0x2 * ((uint64_t)x45 * x51)) + (0x2 * ((uint64_t)x44 * x49))))))))))))))))))))))));
- uint64_t x110 = (x109 >> 0x18);
- uint32_t x111 = ((uint32_t)x109 & 0xffffff);
- uint64_t x112 = (x110 + x108);
- uint64_t x113 = (x112 >> 0x17);
- uint32_t x114 = ((uint32_t)x112 & 0x7fffff);
- uint64_t x115 = (x113 + x107);
- uint64_t x116 = (x115 >> 0x17);
- uint32_t x117 = ((uint32_t)x115 & 0x7fffff);
- uint64_t x118 = (x116 + x106);
- uint64_t x119 = (x118 >> 0x17);
- uint32_t x120 = ((uint32_t)x118 & 0x7fffff);
- uint64_t x121 = (x119 + x105);
- uint64_t x122 = (x121 >> 0x18);
- uint32_t x123 = ((uint32_t)x121 & 0xffffff);
- uint64_t x124 = (x122 + x104);
- uint64_t x125 = (x124 >> 0x17);
- uint32_t x126 = ((uint32_t)x124 & 0x7fffff);
- uint64_t x127 = (x125 + x103);
- uint64_t x128 = (x127 >> 0x17);
- uint32_t x129 = ((uint32_t)x127 & 0x7fffff);
- uint64_t x130 = (x128 + x102);
- uint64_t x131 = (x130 >> 0x17);
- uint32_t x132 = ((uint32_t)x130 & 0x7fffff);
- uint64_t x133 = (x131 + x101);
- uint64_t x134 = (x133 >> 0x18);
- uint32_t x135 = ((uint32_t)x133 & 0xffffff);
- uint64_t x136 = (x134 + x100);
- uint64_t x137 = (x136 >> 0x17);
- uint32_t x138 = ((uint32_t)x136 & 0x7fffff);
- uint64_t x139 = (x137 + x99);
- uint64_t x140 = (x139 >> 0x17);
- uint32_t x141 = ((uint32_t)x139 & 0x7fffff);
- uint64_t x142 = (x140 + x98);
- uint64_t x143 = (x142 >> 0x17);
- uint32_t x144 = ((uint32_t)x142 & 0x7fffff);
- uint64_t x145 = (x143 + x97);
- uint64_t x146 = (x145 >> 0x17);
- uint32_t x147 = ((uint32_t)x145 & 0x7fffff);
- uint64_t x148 = (x146 + x96);
- uint64_t x149 = (x148 >> 0x18);
- uint32_t x150 = ((uint32_t)x148 & 0xffffff);
- uint64_t x151 = (x149 + x95);
- uint64_t x152 = (x151 >> 0x17);
- uint32_t x153 = ((uint32_t)x151 & 0x7fffff);
- uint64_t x154 = (x152 + x94);
- uint64_t x155 = (x154 >> 0x17);
- uint32_t x156 = ((uint32_t)x154 & 0x7fffff);
- uint64_t x157 = (x155 + x93);
- uint64_t x158 = (x157 >> 0x17);
- uint32_t x159 = ((uint32_t)x157 & 0x7fffff);
- uint64_t x160 = (x158 + x92);
- uint64_t x161 = (x160 >> 0x18);
- uint32_t x162 = ((uint32_t)x160 & 0xffffff);
- uint64_t x163 = (x161 + x91);
- uint64_t x164 = (x163 >> 0x17);
- uint32_t x165 = ((uint32_t)x163 & 0x7fffff);
- uint64_t x166 = (x164 + x90);
- uint64_t x167 = (x166 >> 0x17);
- uint32_t x168 = ((uint32_t)x166 & 0x7fffff);
- uint64_t x169 = (x167 + x89);
- uint64_t x170 = (x169 >> 0x17);
- uint32_t x171 = ((uint32_t)x169 & 0x7fffff);
- uint64_t x172 = (x170 + x88);
- uint64_t x173 = (x172 >> 0x17);
- uint32_t x174 = ((uint32_t)x172 & 0x7fffff);
- uint64_t x175 = (x111 + (0xbb * x173));
- uint32_t x176 = (uint32_t) (x175 >> 0x18);
- uint32_t x177 = ((uint32_t)x175 & 0xffffff);
- uint32_t x178 = (x176 + x114);
- uint32_t x179 = (x178 >> 0x17);
- uint32_t x180 = (x178 & 0x7fffff);
- return (Return x174, Return x171, Return x168, Return x165, Return x162, Return x159, Return x156, Return x153, Return x150, Return x147, Return x144, Return x141, Return x138, Return x135, Return x132, Return x129, Return x126, Return x123, Return x120, (x179 + x117), Return x180, Return x177))
-(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 * 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 * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t * uint32_t)