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, 31 insertions, 31 deletions

diff --git a/src/Specific/IntegrationTestSquareDisplay.log b/src/Specific/IntegrationTestSquareDisplay.log
index d502d6ccc..006b83cd9 100644
--- a/src/Specific/IntegrationTestSquareDisplay.log
+++ b/src/Specific/IntegrationTestSquareDisplay.log
@@ -2,36 +2,36 @@
 Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x7, x8, x6, x4, x2)%core,
- uint64_t x9[1] = {(x2[0] * 0x2)};
- uint64_t x10[1] = {(x4[0] * 0x2)};
- uint64_t x11[1] = {(x6[0] * 0x2 * 0x13)};
- uint64_t x12[1] = {(x7[0] * 0x13)};
- uint64_t x13[1] = {(x12[0] * 0x2)};
- uint128_t x14[1] = {((uint128_t) (x2[0]) * x2[0] + (uint128_t) (x13[0]) * x4[0] + (uint128_t) (x11[0]) * x8[0])};
- uint128_t x15[1] = {((uint128_t) (x9[0]) * x4[0] + (uint128_t) (x13[0]) * x6[0] + (uint128_t) (x8[0]) * (x8[0] * 0x13))};
- uint128_t x16[1] = {((uint128_t) (x9[0]) * x6[0] + (uint128_t) (x4[0]) * x4[0] + (uint128_t) (x13[0]) * x8[0])};
- uint128_t x17[1] = {((uint128_t) (x9[0]) * x8[0] + (uint128_t) (x10[0]) * x6[0] + (uint128_t) (x7[0]) * x12[0])};
- uint128_t x18[1] = {((uint128_t) (x9[0]) * x7[0] + (uint128_t) (x10[0]) * x8[0] + (uint128_t) (x6[0]) * x6[0])};
- uint64_t x19[1] = {((uint64_t) (x14[0] >> 0x33))};
- uint64_t x20[1] = {((uint64_t) (x14[0]) & 0x7ffffffffffff)};
- uint128_t x21[1] = {(x19[0] + x15[0])};
- uint64_t x22[1] = {((uint64_t) (x21[0] >> 0x33))};
- uint64_t x23[1] = {((uint64_t) (x21[0]) & 0x7ffffffffffff)};
- uint128_t x24[1] = {(x22[0] + x16[0])};
- uint64_t x25[1] = {((uint64_t) (x24[0] >> 0x33))};
- uint64_t x26[1] = {((uint64_t) (x24[0]) & 0x7ffffffffffff)};
- uint128_t x27[1] = {(x25[0] + x17[0])};
- uint64_t x28[1] = {((uint64_t) (x27[0] >> 0x33))};
- uint64_t x29[1] = {((uint64_t) (x27[0]) & 0x7ffffffffffff)};
- uint128_t x30[1] = {(x28[0] + x18[0])};
- uint64_t x31[1] = {((uint64_t) (x30[0] >> 0x33))};
- uint64_t x32[1] = {((uint64_t) (x30[0]) & 0x7ffffffffffff)};
- uint64_t x33[1] = {(x20[0] + 0x13 * x31[0])};
- uint64_t x34[1] = {(x33[0] >> 0x33)};
- uint64_t x35[1] = {(x33[0] & 0x7ffffffffffff)};
- uint64_t x36[1] = {(x34[0] + x23[0])};
- uint64_t x37[1] = {(x36[0] >> 0x33)};
- uint64_t x38[1] = {(x36[0] & 0x7ffffffffffff)};
- return (x32[0], x29[0], x37[0] + x26[0], x38[0], x35[0]))
+ uint64_t x9 = x2 * 0x2;
+ uint64_t x10 = x4 * 0x2;
+ uint64_t x11 = x6 * 0x2 * 0x13;
+ uint64_t x12 = x7 * 0x13;
+ uint64_t x13 = x12 * 0x2;
+ uint128_t x14 = (uint128_t) x2 * x2 + (uint128_t) x13 * x4 + (uint128_t) x11 * x8;
+ uint128_t x15 = (uint128_t) x9 * x4 + (uint128_t) x13 * x6 + (uint128_t) x8 * (x8 * 0x13);
+ uint128_t x16 = (uint128_t) x9 * x6 + (uint128_t) x4 * x4 + (uint128_t) x13 * x8;
+ uint128_t x17 = (uint128_t) x9 * x8 + (uint128_t) x10 * x6 + (uint128_t) x7 * x12;
+ uint128_t x18 = (uint128_t) x9 * x7 + (uint128_t) x10 * x8 + (uint128_t) x6 * x6;
+ uint64_t x19 = (uint64_t) (x14 >> 0x33);
+ uint64_t x20 = (uint64_t) x14 & 0x7ffffffffffff;
+ uint128_t x21 = x19 + x15;
+ uint64_t x22 = (uint64_t) (x21 >> 0x33);
+ uint64_t x23 = (uint64_t) x21 & 0x7ffffffffffff;
+ uint128_t x24 = x22 + x16;
+ uint64_t x25 = (uint64_t) (x24 >> 0x33);
+ uint64_t x26 = (uint64_t) x24 & 0x7ffffffffffff;
+ uint128_t x27 = x25 + x17;
+ uint64_t x28 = (uint64_t) (x27 >> 0x33);
+ uint64_t x29 = (uint64_t) x27 & 0x7ffffffffffff;
+ uint128_t x30 = x28 + x18;
+ uint64_t x31 = (uint64_t) (x30 >> 0x33);
+ uint64_t x32 = (uint64_t) x30 & 0x7ffffffffffff;
+ uint64_t x33 = x20 + 0x13 * x31;
+ uint64_t x34 = x33 >> 0x33;
+ uint64_t x35 = x33 & 0x7ffffffffffff;
+ uint64_t x36 = x34 + x23;
+ uint64_t x37 = x36 >> 0x33;
+ uint64_t x38 = x36 & 0x7ffffffffffff;
+ return (Return x32, Return x29, x37 + x26, Return x38, Return x35))
 x
      : word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)