Revert PR #203

As per
https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309060964
and
https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309101747

Revert "update ocq2C sed script"

This reverts commit 4a39f39e195b9b7273810a83de78dfd1d150783e.

Revert "make display"

This reverts commit cbf6d013c533d5165d749d0f9405a15d1ff0b43e.

Revert "Make use of CArrayNotations"

This reverts commit cae0e80ae76b76091e7fb86fcd794358a4fe55bb.

Revert "Fix CArrayNotations"

This reverts commit d0d0fbd4499296a2164e209466227892671556f0.

Revert "Revert "Revert "Add CArrayNotations"""

This reverts commit b2b8403ca76f6fd461d9a71ac2e9add4359bba8c.

1 files changed, 55 insertions, 55 deletions

diff --git a/src/Specific/IntegrationTestKaratsubaMulDisplay.log b/src/Specific/IntegrationTestKaratsubaMulDisplay.log
index 05a321ebf..e57c7dbc5 100644
--- a/src/Specific/IntegrationTestKaratsubaMulDisplay.log
+++ b/src/Specific/IntegrationTestKaratsubaMulDisplay.log
@@ -2,60 +2,60 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core,
- uint128_t x32[1] = {((uint128_t) (x11[0] + x16[0]) * (x25[0] + x30[0]) - (uint128_t) (x11[0]) * x25[0])};
- uint128_t x33[1] = {((uint128_t) (x9[0] + x17[0]) * (x25[0] + x30[0]) + (uint128_t) (x11[0] + x16[0]) * (x23[0] + x31[0]) - ((uint128_t) (x9[0]) * x25[0] + (uint128_t) (x11[0]) * x23[0]))};
- uint128_t x34[1] = {((uint128_t) (x7[0] + x15[0]) * (x25[0] + x30[0]) + ((uint128_t) (x9[0] + x17[0]) * (x23[0] + x31[0]) + (uint128_t) (x11[0] + x16[0]) * (x21[0] + x29[0])) - ((uint128_t) (x7[0]) * x25[0] + ((uint128_t) (x9[0]) * x23[0] + (uint128_t) (x11[0]) * x21[0])))};
- uint128_t x35[1] = {((uint128_t) (x5[0] + x13[0]) * (x25[0] + x30[0]) + ((uint128_t) (x7[0] + x15[0]) * (x23[0] + x31[0]) + ((uint128_t) (x9[0] + x17[0]) * (x21[0] + x29[0]) + (uint128_t) (x11[0] + x16[0]) * (x19[0] + x27[0]))) - ((uint128_t) (x5[0]) * x25[0] + ((uint128_t) (x7[0]) * x23[0] + ((uint128_t) (x9[0]) * x21[0] + (uint128_t) (x11[0]) * x19[0]))))};
- uint128_t x36[1] = {((uint128_t) (x5[0] + x13[0]) * (x23[0] + x31[0]) + ((uint128_t) (x7[0] + x15[0]) * (x21[0] + x29[0]) + (uint128_t) (x9[0] + x17[0]) * (x19[0] + x27[0])) - ((uint128_t) (x5[0]) * x23[0] + ((uint128_t) (x7[0]) * x21[0] + (uint128_t) (x9[0]) * x19[0])))};
- uint128_t x37[1] = {((uint128_t) (x5[0] + x13[0]) * (x21[0] + x29[0]) + (uint128_t) (x7[0] + x15[0]) * (x19[0] + x27[0]) - ((uint128_t) (x5[0]) * x21[0] + (uint128_t) (x7[0]) * x19[0]))};
- uint128_t x38[1] = {((uint128_t) (x5[0] + x13[0]) * (x19[0] + x27[0]) - (uint128_t) (x5[0]) * x19[0])};
- uint128_t x39[1] = {((uint128_t) (x11[0]) * x25[0] + (uint128_t) (x16[0]) * x30[0] + x36[0] + x32[0])};
- uint128_t x40[1] = {((uint128_t) (x9[0]) * x25[0] + (uint128_t) (x11[0]) * x23[0] + ((uint128_t) (x17[0]) * x30[0] + (uint128_t) (x16[0]) * x31[0]) + x37[0] + x33[0])};
- uint128_t x41[1] = {((uint128_t) (x7[0]) * x25[0] + ((uint128_t) (x9[0]) * x23[0] + (uint128_t) (x11[0]) * x21[0]) + ((uint128_t) (x15[0]) * x30[0] + ((uint128_t) (x17[0]) * x31[0] + (uint128_t) (x16[0]) * x29[0])) + x38[0] + x34[0])};
- uint128_t x42[1] = {((uint128_t) (x5[0]) * x25[0] + ((uint128_t) (x7[0]) * x23[0] + ((uint128_t) (x9[0]) * x21[0] + (uint128_t) (x11[0]) * x19[0])) + ((uint128_t) (x13[0]) * x30[0] + ((uint128_t) (x15[0]) * x31[0] + ((uint128_t) (x17[0]) * x29[0] + (uint128_t) (x16[0]) * x27[0]))))};
- uint128_t x43[1] = {((uint128_t) (x5[0]) * x23[0] + ((uint128_t) (x7[0]) * x21[0] + (uint128_t) (x9[0]) * x19[0]) + ((uint128_t) (x13[0]) * x31[0] + ((uint128_t) (x15[0]) * x29[0] + (uint128_t) (x17[0]) * x27[0])) + x32[0])};
- uint128_t x44[1] = {((uint128_t) (x5[0]) * x21[0] + (uint128_t) (x7[0]) * x19[0] + ((uint128_t) (x13[0]) * x29[0] + (uint128_t) (x15[0]) * x27[0]) + x33[0])};
- uint128_t x45[1] = {((uint128_t) (x5[0]) * x19[0] + (uint128_t) (x13[0]) * x27[0] + x34[0])};
- uint64_t x46[1] = {((uint64_t) (x42[0] >> 0x38))};
- uint64_t x47[1] = {((uint64_t) (x42[0]) & 0xffffffffffffff)};
- uint64_t x48[1] = {((uint64_t) (x35[0] >> 0x38))};
- uint64_t x49[1] = {((uint64_t) (x35[0]) & 0xffffffffffffff)};
- uint128_t x50[1] = {((uint128_t) (Const 72057594037927936) * x48[0] + x49[0])};
- uint64_t x51[1] = {((uint64_t) (x50[0] >> 0x38))};
- uint64_t x52[1] = {((uint64_t) (x50[0]) & 0xffffffffffffff)};
- uint128_t x53[1] = {(x45[0] + x51[0])};
- uint64_t x54[1] = {((uint64_t) (x53[0] >> 0x38))};
- uint64_t x55[1] = {((uint64_t) (x53[0]) & 0xffffffffffffff)};
- uint128_t x56[1] = {(x46[0] + x41[0] + x51[0])};
- uint64_t x57[1] = {((uint64_t) (x56[0] >> 0x38))};
- uint64_t x58[1] = {((uint64_t) (x56[0]) & 0xffffffffffffff)};
- uint128_t x59[1] = {(x54[0] + x44[0])};
- uint64_t x60[1] = {((uint64_t) (x59[0] >> 0x38))};
- uint64_t x61[1] = {((uint64_t) (x59[0]) & 0xffffffffffffff)};
- uint128_t x62[1] = {(x57[0] + x40[0])};
- uint64_t x63[1] = {((uint64_t) (x62[0] >> 0x38))};
- uint64_t x64[1] = {((uint64_t) (x62[0]) & 0xffffffffffffff)};
- uint128_t x65[1] = {(x60[0] + x43[0])};
- uint64_t x66[1] = {((uint64_t) (x65[0] >> 0x38))};
- uint64_t x67[1] = {((uint64_t) (x65[0]) & 0xffffffffffffff)};
- uint128_t x68[1] = {(x63[0] + x39[0])};
- uint64_t x69[1] = {((uint64_t) (x68[0] >> 0x38))};
- uint64_t x70[1] = {((uint64_t) (x68[0]) & 0xffffffffffffff)};
- uint64_t x71[1] = {(x66[0] + x47[0])};
- uint64_t x72[1] = {(x71[0] >> 0x38)};
- uint64_t x73[1] = {(x71[0] & 0xffffffffffffff)};
- uint64_t x74[1] = {(x69[0] + x52[0])};
- uint64_t x75[1] = {(x74[0] >> 0x38)};
- uint64_t x76[1] = {(x74[0] & 0xffffffffffffff)};
- uint64_t x77[1] = {(Const 72057594037927936 * x75[0] + x76[0])};
- uint64_t x78[1] = {(x77[0] >> 0x38)};
- uint64_t x79[1] = {(x77[0] & 0xffffffffffffff)};
- uint64_t x80[1] = {(x72[0] + x58[0] + x78[0])};
- uint64_t x81[1] = {(x80[0] >> 0x38)};
- uint64_t x82[1] = {(x80[0] & 0xffffffffffffff)};
- uint64_t x83[1] = {(x55[0] + x78[0])};
- uint64_t x84[1] = {(x83[0] >> 0x38)};
- uint64_t x85[1] = {(x83[0] & 0xffffffffffffff)};
- return (x79[0], x70[0], x81[0] + x64[0], x82[0], x73[0], x67[0], x84[0] + x61[0], x85[0]))
+ uint128_t x32 = (uint128_t) (x11 + x16) * (x25 + x30) - (uint128_t) x11 * x25;
+ uint128_t x33 = (uint128_t) (x9 + x17) * (x25 + x30) + (uint128_t) (x11 + x16) * (x23 + x31) - ((uint128_t) x9 * x25 + (uint128_t) x11 * x23);
+ uint128_t x34 = (uint128_t) (x7 + x15) * (x25 + x30) + ((uint128_t) (x9 + x17) * (x23 + x31) + (uint128_t) (x11 + x16) * (x21 + x29)) - ((uint128_t) x7 * x25 + ((uint128_t) x9 * x23 + (uint128_t) x11 * x21));
+ uint128_t x35 = (uint128_t) (x5 + x13) * (x25 + x30) + ((uint128_t) (x7 + x15) * (x23 + x31) + ((uint128_t) (x9 + x17) * (x21 + x29) + (uint128_t) (x11 + x16) * (x19 + x27))) - ((uint128_t) x5 * x25 + ((uint128_t) x7 * x23 + ((uint128_t) x9 * x21 + (uint128_t) x11 * x19)));
+ uint128_t x36 = (uint128_t) (x5 + x13) * (x23 + x31) + ((uint128_t) (x7 + x15) * (x21 + x29) + (uint128_t) (x9 + x17) * (x19 + x27)) - ((uint128_t) x5 * x23 + ((uint128_t) x7 * x21 + (uint128_t) x9 * x19));
+ uint128_t x37 = (uint128_t) (x5 + x13) * (x21 + x29) + (uint128_t) (x7 + x15) * (x19 + x27) - ((uint128_t) x5 * x21 + (uint128_t) x7 * x19);
+ uint128_t x38 = (uint128_t) (x5 + x13) * (x19 + x27) - (uint128_t) x5 * x19;
+ uint128_t x39 = (uint128_t) x11 * x25 + (uint128_t) x16 * x30 + x36 + x32;
+ uint128_t x40 = (uint128_t) x9 * x25 + (uint128_t) x11 * x23 + ((uint128_t) x17 * x30 + (uint128_t) x16 * x31) + x37 + x33;
+ uint128_t x41 = (uint128_t) x7 * x25 + ((uint128_t) x9 * x23 + (uint128_t) x11 * x21) + ((uint128_t) x15 * x30 + ((uint128_t) x17 * x31 + (uint128_t) x16 * x29)) + x38 + x34;
+ uint128_t x42 = (uint128_t) x5 * x25 + ((uint128_t) x7 * x23 + ((uint128_t) x9 * x21 + (uint128_t) x11 * x19)) + ((uint128_t) x13 * x30 + ((uint128_t) x15 * x31 + ((uint128_t) x17 * x29 + (uint128_t) x16 * x27)));
+ uint128_t x43 = (uint128_t) x5 * x23 + ((uint128_t) x7 * x21 + (uint128_t) x9 * x19) + ((uint128_t) x13 * x31 + ((uint128_t) x15 * x29 + (uint128_t) x17 * x27)) + x32;
+ uint128_t x44 = (uint128_t) x5 * x21 + (uint128_t) x7 * x19 + ((uint128_t) x13 * x29 + (uint128_t) x15 * x27) + x33;
+ uint128_t x45 = (uint128_t) x5 * x19 + (uint128_t) x13 * x27 + x34;
+ uint64_t x46 = (uint64_t) (x42 >> 0x38);
+ uint64_t x47 = (uint64_t) x42 & 0xffffffffffffff;
+ uint64_t x48 = (uint64_t) (x35 >> 0x38);
+ uint64_t x49 = (uint64_t) x35 & 0xffffffffffffff;
+ uint128_t x50 = (uint128_t) (Const 72057594037927936) * x48 + x49;
+ uint64_t x51 = (uint64_t) (x50 >> 0x38);
+ uint64_t x52 = (uint64_t) x50 & 0xffffffffffffff;
+ uint128_t x53 = x45 + x51;
+ uint64_t x54 = (uint64_t) (x53 >> 0x38);
+ uint64_t x55 = (uint64_t) x53 & 0xffffffffffffff;
+ uint128_t x56 = x46 + x41 + x51;
+ uint64_t x57 = (uint64_t) (x56 >> 0x38);
+ uint64_t x58 = (uint64_t) x56 & 0xffffffffffffff;
+ uint128_t x59 = x54 + x44;
+ uint64_t x60 = (uint64_t) (x59 >> 0x38);
+ uint64_t x61 = (uint64_t) x59 & 0xffffffffffffff;
+ uint128_t x62 = x57 + x40;
+ uint64_t x63 = (uint64_t) (x62 >> 0x38);
+ uint64_t x64 = (uint64_t) x62 & 0xffffffffffffff;
+ uint128_t x65 = x60 + x43;
+ uint64_t x66 = (uint64_t) (x65 >> 0x38);
+ uint64_t x67 = (uint64_t) x65 & 0xffffffffffffff;
+ uint128_t x68 = x63 + x39;
+ uint64_t x69 = (uint64_t) (x68 >> 0x38);
+ uint64_t x70 = (uint64_t) x68 & 0xffffffffffffff;
+ uint64_t x71 = x66 + x47;
+ uint64_t x72 = x71 >> 0x38;
+ uint64_t x73 = x71 & 0xffffffffffffff;
+ uint64_t x74 = x69 + x52;
+ uint64_t x75 = x74 >> 0x38;
+ uint64_t x76 = x74 & 0xffffffffffffff;
+ uint64_t x77 = Const 72057594037927936 * x75 + x76;
+ uint64_t x78 = x77 >> 0x38;
+ uint64_t x79 = x77 & 0xffffffffffffff;
+ uint64_t x80 = x72 + x58 + x78;
+ uint64_t x81 = x80 >> 0x38;
+ uint64_t x82 = x80 & 0xffffffffffffff;
+ uint64_t x83 = x55 + x78;
+ uint64_t x84 = x83 >> 0x38;
+ uint64_t x85 = x83 & 0xffffffffffffff;
+ return (Return x79, Return x70, x81 + x64, Return x82, Return x73, Return x67, x84 + x61, Return x85))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)