force carry intermediates to be bound early

4 files changed, 316 insertions, 314 deletions

diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index f294c06fc..b86ac09b9 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -430,7 +430,9 @@ Module B.
       Definition carryterm_cps (w fw:Z) (t:limb) {T} (f:list limb->T) :=
         if dec (fst t = w)
         then dlet t2 := snd t in
-             f ((w*fw, div t2 fw) :: (w, modulo t2 fw) :: @nil limb)
+             dlet d2 := div t2 fw in
+             dlet m2 := modulo t2 fw in
+             f ((w*fw, d2) :: (w, m2) :: @nil limb)
         else f [t].
 
       Definition carryterm w fw t := carryterm_cps w fw t id.
diff --git a/src/Specific/IntegrationTestLadderstepDisplay.log b/src/Specific/IntegrationTestLadderstepDisplay.log
index 0a2657d7a..beac5d641 100644
--- a/src/Specific/IntegrationTestLadderstepDisplay.log
+++ b/src/Specific/IntegrationTestLadderstepDisplay.log
@@ -50,27 +50,27 @@ let (a, b) := Interp-η
  uint128_t x98 = (uint128_t) x55 * x55;
  uint128_t x99 = x97 + x98;
  uint64_t x100 = (uint64_t) (x78 >> 0x33);
- uint128_t x101 = x100 + x84;
- uint64_t x102 = (uint64_t) (x101 >> 0x33);
- uint128_t x103 = x102 + x89;
- uint64_t x104 = (uint64_t) (x103 >> 0x33);
- uint128_t x105 = x104 + x94;
+ uint64_t x101 = (uint64_t) x78 & 0x7ffffffffffff;
+ uint128_t x102 = x100 + x84;
+ uint64_t x103 = (uint64_t) (x102 >> 0x33);
+ uint64_t x104 = (uint64_t) x102 & 0x7ffffffffffff;
+ uint128_t x105 = x103 + x89;
  uint64_t x106 = (uint64_t) (x105 >> 0x33);
- uint128_t x107 = x106 + x99;
- uint64_t x108 = (uint64_t) x78 & 0x7ffffffffffff;
- uint64_t x109 = (uint64_t) (x107 >> 0x33);
- uint64_t x110 = 0x13 * x109;
- uint64_t x111 = x108 + x110;
- uint64_t x112 = x111 >> 0x33;
- uint64_t x113 = (uint64_t) x101 & 0x7ffffffffffff;
- uint64_t x114 = x112 + x113;
- uint64_t x115 = (uint64_t) x107 & 0x7ffffffffffff;
- uint64_t x116 = (uint64_t) x105 & 0x7ffffffffffff;
- uint64_t x117 = x114 >> 0x33;
- uint64_t x118 = (uint64_t) x103 & 0x7ffffffffffff;
- uint64_t x119 = x117 + x118;
- uint64_t x120 = x114 & 0x7ffffffffffff;
- uint64_t x121 = x111 & 0x7ffffffffffff;
+ uint64_t x107 = (uint64_t) x105 & 0x7ffffffffffff;
+ uint128_t x108 = x106 + x94;
+ uint64_t x109 = (uint64_t) (x108 >> 0x33);
+ uint64_t x110 = (uint64_t) x108 & 0x7ffffffffffff;
+ uint128_t x111 = x109 + x99;
+ uint64_t x112 = (uint64_t) (x111 >> 0x33);
+ uint64_t x113 = (uint64_t) x111 & 0x7ffffffffffff;
+ uint64_t x114 = 0x13 * x112;
+ uint64_t x115 = x101 + x114;
+ uint64_t x116 = x115 >> 0x33;
+ uint64_t x117 = x115 & 0x7ffffffffffff;
+ uint64_t x118 = x116 + x104;
+ uint64_t x119 = x118 >> 0x33;
+ uint64_t x120 = x118 & 0x7ffffffffffff;
+ uint64_t x121 = x119 + x107;
  uint64_t x122 = x67 * 0x2;
  uint64_t x123 = x65 * 0x2;
  uint64_t x124 = x63 * 0x2;
@@ -104,140 +104,140 @@ let (a, b) := Interp-η
  uint128_t x152 = (uint128_t) x63 * x63;
  uint128_t x153 = x151 + x152;
  uint64_t x154 = (uint64_t) (x132 >> 0x33);
- uint128_t x155 = x154 + x138;
- uint64_t x156 = (uint64_t) (x155 >> 0x33);
- uint128_t x157 = x156 + x143;
- uint64_t x158 = (uint64_t) (x157 >> 0x33);
- uint128_t x159 = x158 + x148;
+ uint64_t x155 = (uint64_t) x132 & 0x7ffffffffffff;
+ uint128_t x156 = x154 + x138;
+ uint64_t x157 = (uint64_t) (x156 >> 0x33);
+ uint64_t x158 = (uint64_t) x156 & 0x7ffffffffffff;
+ uint128_t x159 = x157 + x143;
  uint64_t x160 = (uint64_t) (x159 >> 0x33);
- uint128_t x161 = x160 + x153;
- uint64_t x162 = (uint64_t) x132 & 0x7ffffffffffff;
- uint64_t x163 = (uint64_t) (x161 >> 0x33);
- uint64_t x164 = 0x13 * x163;
- uint64_t x165 = x162 + x164;
- uint64_t x166 = x165 >> 0x33;
- uint64_t x167 = (uint64_t) x155 & 0x7ffffffffffff;
- uint64_t x168 = x166 + x167;
- uint64_t x169 = (uint64_t) x161 & 0x7ffffffffffff;
- uint64_t x170 = (uint64_t) x159 & 0x7ffffffffffff;
- uint64_t x171 = x168 >> 0x33;
- uint64_t x172 = (uint64_t) x157 & 0x7ffffffffffff;
- uint64_t x173 = x171 + x172;
- uint64_t x174 = x168 & 0x7ffffffffffff;
- uint64_t x175 = x165 & 0x7ffffffffffff;
- uint128_t x176 = (uint128_t) x121 * x175;
- uint128_t x177 = (uint128_t) x121 * x174;
- uint128_t x178 = (uint128_t) x120 * x175;
+ uint64_t x161 = (uint64_t) x159 & 0x7ffffffffffff;
+ uint128_t x162 = x160 + x148;
+ uint64_t x163 = (uint64_t) (x162 >> 0x33);
+ uint64_t x164 = (uint64_t) x162 & 0x7ffffffffffff;
+ uint128_t x165 = x163 + x153;
+ uint64_t x166 = (uint64_t) (x165 >> 0x33);
+ uint64_t x167 = (uint64_t) x165 & 0x7ffffffffffff;
+ uint64_t x168 = 0x13 * x166;
+ uint64_t x169 = x155 + x168;
+ uint64_t x170 = x169 >> 0x33;
+ uint64_t x171 = x169 & 0x7ffffffffffff;
+ uint64_t x172 = x170 + x158;
+ uint64_t x173 = x172 >> 0x33;
+ uint64_t x174 = x172 & 0x7ffffffffffff;
+ uint64_t x175 = x173 + x161;
+ uint128_t x176 = (uint128_t) x117 * x171;
+ uint128_t x177 = (uint128_t) x117 * x174;
+ uint128_t x178 = (uint128_t) x120 * x171;
  uint128_t x179 = x177 + x178;
- uint128_t x180 = (uint128_t) x121 * x173;
- uint128_t x181 = (uint128_t) x119 * x175;
+ uint128_t x180 = (uint128_t) x117 * x175;
+ uint128_t x181 = (uint128_t) x121 * x171;
  uint128_t x182 = x180 + x181;
  uint128_t x183 = (uint128_t) x120 * x174;
  uint128_t x184 = x182 + x183;
- uint128_t x185 = (uint128_t) x121 * x170;
- uint128_t x186 = (uint128_t) x116 * x175;
+ uint128_t x185 = (uint128_t) x117 * x164;
+ uint128_t x186 = (uint128_t) x110 * x171;
  uint128_t x187 = x185 + x186;
- uint128_t x188 = (uint128_t) x120 * x173;
+ uint128_t x188 = (uint128_t) x120 * x175;
  uint128_t x189 = x187 + x188;
- uint128_t x190 = (uint128_t) x119 * x174;
+ uint128_t x190 = (uint128_t) x121 * x174;
  uint128_t x191 = x189 + x190;
- uint128_t x192 = (uint128_t) x121 * x169;
- uint128_t x193 = (uint128_t) x115 * x175;
+ uint128_t x192 = (uint128_t) x117 * x167;
+ uint128_t x193 = (uint128_t) x113 * x171;
  uint128_t x194 = x192 + x193;
- uint128_t x195 = (uint128_t) x116 * x174;
+ uint128_t x195 = (uint128_t) x110 * x174;
  uint128_t x196 = x194 + x195;
- uint128_t x197 = (uint128_t) x120 * x170;
+ uint128_t x197 = (uint128_t) x120 * x164;
  uint128_t x198 = x196 + x197;
- uint128_t x199 = (uint128_t) x119 * x173;
+ uint128_t x199 = (uint128_t) x121 * x175;
  uint128_t x200 = x198 + x199;
- uint64_t x201 = x115 * 0x13;
+ uint64_t x201 = x113 * 0x13;
  uint64_t x202 = x120 * 0x13;
- uint64_t x203 = x119 * 0x13;
- uint64_t x204 = x116 * 0x13;
+ uint64_t x203 = x121 * 0x13;
+ uint64_t x204 = x110 * 0x13;
  uint128_t x205 = (uint128_t) x201 * x174;
  uint128_t x206 = x176 + x205;
- uint128_t x207 = (uint128_t) x202 * x169;
+ uint128_t x207 = (uint128_t) x202 * x167;
  uint128_t x208 = x206 + x207;
- uint128_t x209 = (uint128_t) x203 * x170;
+ uint128_t x209 = (uint128_t) x203 * x164;
  uint128_t x210 = x208 + x209;
- uint128_t x211 = (uint128_t) x204 * x173;
+ uint128_t x211 = (uint128_t) x204 * x175;
  uint128_t x212 = x210 + x211;
- uint128_t x213 = (uint128_t) x201 * x173;
+ uint128_t x213 = (uint128_t) x201 * x175;
  uint128_t x214 = x179 + x213;
- uint128_t x215 = (uint128_t) x203 * x169;
+ uint128_t x215 = (uint128_t) x203 * x167;
  uint128_t x216 = x214 + x215;
- uint128_t x217 = (uint128_t) x204 * x170;
+ uint128_t x217 = (uint128_t) x204 * x164;
  uint128_t x218 = x216 + x217;
- uint128_t x219 = (uint128_t) x201 * x170;
+ uint128_t x219 = (uint128_t) x201 * x164;
  uint128_t x220 = x184 + x219;
- uint128_t x221 = (uint128_t) x204 * x169;
+ uint128_t x221 = (uint128_t) x204 * x167;
  uint128_t x222 = x220 + x221;
- uint128_t x223 = (uint128_t) x201 * x169;
+ uint128_t x223 = (uint128_t) x201 * x167;
  uint128_t x224 = x191 + x223;
  uint64_t x225 = (uint64_t) (x212 >> 0x33);
- uint128_t x226 = x225 + x218;
- uint64_t x227 = (uint64_t) (x226 >> 0x33);
- uint128_t x228 = x227 + x222;
- uint64_t x229 = (uint64_t) (x228 >> 0x33);
- uint128_t x230 = x229 + x224;
+ uint64_t x226 = (uint64_t) x212 & 0x7ffffffffffff;
+ uint128_t x227 = x225 + x218;
+ uint64_t x228 = (uint64_t) (x227 >> 0x33);
+ uint64_t x229 = (uint64_t) x227 & 0x7ffffffffffff;
+ uint128_t x230 = x228 + x222;
  uint64_t x231 = (uint64_t) (x230 >> 0x33);
- uint128_t x232 = x231 + x200;
- uint64_t x233 = (uint64_t) x212 & 0x7ffffffffffff;
- uint64_t x234 = (uint64_t) (x232 >> 0x33);
- uint64_t x235 = 0x13 * x234;
- uint64_t x236 = x233 + x235;
- uint64_t x237 = x236 >> 0x33;
- uint64_t x238 = (uint64_t) x226 & 0x7ffffffffffff;
- uint64_t x239 = x237 + x238;
- uint64_t x240 = (uint64_t) x232 & 0x7ffffffffffff;
- uint64_t x241 = (uint64_t) x230 & 0x7ffffffffffff;
- uint64_t x242 = x239 >> 0x33;
- uint64_t x243 = (uint64_t) x228 & 0x7ffffffffffff;
- uint64_t x244 = x242 + x243;
- uint64_t x245 = x239 & 0x7ffffffffffff;
- uint64_t x246 = x236 & 0x7ffffffffffff;
- uint64_t x247 = 0xffffffffffffe + x115;
- uint64_t x248 = x247 - x169;
- uint64_t x249 = 0xffffffffffffe + x116;
- uint64_t x250 = x249 - x170;
- uint64_t x251 = 0xffffffffffffe + x119;
- uint64_t x252 = x251 - x173;
+ uint64_t x232 = (uint64_t) x230 & 0x7ffffffffffff;
+ uint128_t x233 = x231 + x224;
+ uint64_t x234 = (uint64_t) (x233 >> 0x33);
+ uint64_t x235 = (uint64_t) x233 & 0x7ffffffffffff;
+ uint128_t x236 = x234 + x200;
+ uint64_t x237 = (uint64_t) (x236 >> 0x33);
+ uint64_t x238 = (uint64_t) x236 & 0x7ffffffffffff;
+ uint64_t x239 = 0x13 * x237;
+ uint64_t x240 = x226 + x239;
+ uint64_t x241 = x240 >> 0x33;
+ uint64_t x242 = x240 & 0x7ffffffffffff;
+ uint64_t x243 = x241 + x229;
+ uint64_t x244 = x243 >> 0x33;
+ uint64_t x245 = x243 & 0x7ffffffffffff;
+ uint64_t x246 = x244 + x232;
+ uint64_t x247 = 0xffffffffffffe + x113;
+ uint64_t x248 = x247 - x167;
+ uint64_t x249 = 0xffffffffffffe + x110;
+ uint64_t x250 = x249 - x164;
+ uint64_t x251 = 0xffffffffffffe + x121;
+ uint64_t x252 = x251 - x175;
  uint64_t x253 = 0xffffffffffffe + x120;
  uint64_t x254 = x253 - x174;
- uint64_t x255 = 0xfffffffffffda + x121;
- uint64_t x256 = x255 - x175;
+ uint64_t x255 = 0xfffffffffffda + x117;
+ uint64_t x256 = x255 - x171;
  uint128_t x257 = (uint128_t) 0x1db41 * x256;
  uint128_t x258 = (uint128_t) 0x1db41 * x254;
  uint128_t x259 = (uint128_t) 0x1db41 * x252;
  uint128_t x260 = (uint128_t) 0x1db41 * x250;
  uint128_t x261 = (uint128_t) 0x1db41 * x248;
  uint64_t x262 = (uint64_t) (x257 >> 0x33);
- uint128_t x263 = x262 + x258;
- uint64_t x264 = (uint64_t) (x263 >> 0x33);
- uint128_t x265 = x264 + x259;
- uint64_t x266 = (uint64_t) (x265 >> 0x33);
- uint128_t x267 = x266 + x260;
+ uint64_t x263 = (uint64_t) x257 & 0x7ffffffffffff;
+ uint128_t x264 = x262 + x258;
+ uint64_t x265 = (uint64_t) (x264 >> 0x33);
+ uint64_t x266 = (uint64_t) x264 & 0x7ffffffffffff;
+ uint128_t x267 = x265 + x259;
  uint64_t x268 = (uint64_t) (x267 >> 0x33);
- uint128_t x269 = x268 + x261;
- uint64_t x270 = (uint64_t) x257 & 0x7ffffffffffff;
- uint64_t x271 = (uint64_t) (x269 >> 0x33);
- uint64_t x272 = 0x13 * x271;
- uint64_t x273 = x270 + x272;
- uint64_t x274 = x273 >> 0x33;
- uint64_t x275 = (uint64_t) x263 & 0x7ffffffffffff;
- uint64_t x276 = x274 + x275;
- uint64_t x277 = (uint64_t) x269 & 0x7ffffffffffff;
- uint64_t x278 = (uint64_t) x267 & 0x7ffffffffffff;
- uint64_t x279 = x276 >> 0x33;
- uint64_t x280 = (uint64_t) x265 & 0x7ffffffffffff;
- uint64_t x281 = x279 + x280;
- uint64_t x282 = x276 & 0x7ffffffffffff;
- uint64_t x283 = x273 & 0x7ffffffffffff;
- uint64_t x284 = x115 + x277;
- uint64_t x285 = x116 + x278;
- uint64_t x286 = x119 + x281;
+ uint64_t x269 = (uint64_t) x267 & 0x7ffffffffffff;
+ uint128_t x270 = x268 + x260;
+ uint64_t x271 = (uint64_t) (x270 >> 0x33);
+ uint64_t x272 = (uint64_t) x270 & 0x7ffffffffffff;
+ uint128_t x273 = x271 + x261;
+ uint64_t x274 = (uint64_t) (x273 >> 0x33);
+ uint64_t x275 = (uint64_t) x273 & 0x7ffffffffffff;
+ uint64_t x276 = 0x13 * x274;
+ uint64_t x277 = x263 + x276;
+ uint64_t x278 = x277 >> 0x33;
+ uint64_t x279 = x277 & 0x7ffffffffffff;
+ uint64_t x280 = x278 + x266;
+ uint64_t x281 = x280 >> 0x33;
+ uint64_t x282 = x280 & 0x7ffffffffffff;
+ uint64_t x283 = x281 + x269;
+ uint64_t x284 = x113 + x275;
+ uint64_t x285 = x110 + x272;
+ uint64_t x286 = x121 + x283;
  uint64_t x287 = x120 + x282;
- uint64_t x288 = x121 + x283;
+ uint64_t x288 = x117 + x279;
  uint128_t x289 = (uint128_t) x256 * x288;
  uint128_t x290 = (uint128_t) x256 * x287;
  uint128_t x291 = (uint128_t) x254 * x288;
@@ -288,27 +288,27 @@ let (a, b) := Interp-η
  uint128_t x336 = (uint128_t) x314 * x284;
  uint128_t x337 = x304 + x336;
  uint64_t x338 = (uint64_t) (x325 >> 0x33);
- uint128_t x339 = x338 + x331;
- uint64_t x340 = (uint64_t) (x339 >> 0x33);
- uint128_t x341 = x340 + x335;
- uint64_t x342 = (uint64_t) (x341 >> 0x33);
- uint128_t x343 = x342 + x337;
+ uint64_t x339 = (uint64_t) x325 & 0x7ffffffffffff;
+ uint128_t x340 = x338 + x331;
+ uint64_t x341 = (uint64_t) (x340 >> 0x33);
+ uint64_t x342 = (uint64_t) x340 & 0x7ffffffffffff;
+ uint128_t x343 = x341 + x335;
  uint64_t x344 = (uint64_t) (x343 >> 0x33);
- uint128_t x345 = x344 + x313;
- uint64_t x346 = (uint64_t) x325 & 0x7ffffffffffff;
- uint64_t x347 = (uint64_t) (x345 >> 0x33);
- uint64_t x348 = 0x13 * x347;
- uint64_t x349 = x346 + x348;
- uint64_t x350 = x349 >> 0x33;
- uint64_t x351 = (uint64_t) x339 & 0x7ffffffffffff;
- uint64_t x352 = x350 + x351;
- uint64_t x353 = (uint64_t) x345 & 0x7ffffffffffff;
- uint64_t x354 = (uint64_t) x343 & 0x7ffffffffffff;
- uint64_t x355 = x352 >> 0x33;
- uint64_t x356 = (uint64_t) x341 & 0x7ffffffffffff;
- uint64_t x357 = x355 + x356;
- uint64_t x358 = x352 & 0x7ffffffffffff;
- uint64_t x359 = x349 & 0x7ffffffffffff;
+ uint64_t x345 = (uint64_t) x343 & 0x7ffffffffffff;
+ uint128_t x346 = x344 + x337;
+ uint64_t x347 = (uint64_t) (x346 >> 0x33);
+ uint64_t x348 = (uint64_t) x346 & 0x7ffffffffffff;
+ uint128_t x349 = x347 + x313;
+ uint64_t x350 = (uint64_t) (x349 >> 0x33);
+ uint64_t x351 = (uint64_t) x349 & 0x7ffffffffffff;
+ uint64_t x352 = 0x13 * x350;
+ uint64_t x353 = x339 + x352;
+ uint64_t x354 = x353 >> 0x33;
+ uint64_t x355 = x353 & 0x7ffffffffffff;
+ uint64_t x356 = x354 + x342;
+ uint64_t x357 = x356 >> 0x33;
+ uint64_t x358 = x356 & 0x7ffffffffffff;
+ uint64_t x359 = x357 + x345;
  uint64_t x360 = x43 + x51;
  uint64_t x361 = x44 + x52;
  uint64_t x362 = x42 + x50;
@@ -374,27 +374,27 @@ let (a, b) := Interp-η
  uint128_t x422 = (uint128_t) x400 * x59;
  uint128_t x423 = x390 + x422;
  uint64_t x424 = (uint64_t) (x411 >> 0x33);
- uint128_t x425 = x424 + x417;
- uint64_t x426 = (uint64_t) (x425 >> 0x33);
- uint128_t x427 = x426 + x421;
- uint64_t x428 = (uint64_t) (x427 >> 0x33);
- uint128_t x429 = x428 + x423;
+ uint64_t x425 = (uint64_t) x411 & 0x7ffffffffffff;
+ uint128_t x426 = x424 + x417;
+ uint64_t x427 = (uint64_t) (x426 >> 0x33);
+ uint64_t x428 = (uint64_t) x426 & 0x7ffffffffffff;
+ uint128_t x429 = x427 + x421;
  uint64_t x430 = (uint64_t) (x429 >> 0x33);
- uint128_t x431 = x430 + x399;
- uint64_t x432 = (uint64_t) x411 & 0x7ffffffffffff;
- uint64_t x433 = (uint64_t) (x431 >> 0x33);
- uint64_t x434 = 0x13 * x433;
- uint64_t x435 = x432 + x434;
- uint64_t x436 = x435 >> 0x33;
- uint64_t x437 = (uint64_t) x425 & 0x7ffffffffffff;
- uint64_t x438 = x436 + x437;
- uint64_t x439 = (uint64_t) x431 & 0x7ffffffffffff;
- uint64_t x440 = (uint64_t) x429 & 0x7ffffffffffff;
- uint64_t x441 = x438 >> 0x33;
- uint64_t x442 = (uint64_t) x427 & 0x7ffffffffffff;
- uint64_t x443 = x441 + x442;
- uint64_t x444 = x438 & 0x7ffffffffffff;
- uint64_t x445 = x435 & 0x7ffffffffffff;
+ uint64_t x431 = (uint64_t) x429 & 0x7ffffffffffff;
+ uint128_t x432 = x430 + x423;
+ uint64_t x433 = (uint64_t) (x432 >> 0x33);
+ uint64_t x434 = (uint64_t) x432 & 0x7ffffffffffff;
+ uint128_t x435 = x433 + x399;
+ uint64_t x436 = (uint64_t) (x435 >> 0x33);
+ uint64_t x437 = (uint64_t) x435 & 0x7ffffffffffff;
+ uint64_t x438 = 0x13 * x436;
+ uint64_t x439 = x425 + x438;
+ uint64_t x440 = x439 >> 0x33;
+ uint64_t x441 = x439 & 0x7ffffffffffff;
+ uint64_t x442 = x440 + x428;
+ uint64_t x443 = x442 >> 0x33;
+ uint64_t x444 = x442 & 0x7ffffffffffff;
+ uint64_t x445 = x443 + x431;
  uint128_t x446 = (uint128_t) x374 * x57;
  uint128_t x447 = (uint128_t) x374 * x56;
  uint128_t x448 = (uint128_t) x372 * x57;
@@ -445,32 +445,32 @@ let (a, b) := Interp-η
  uint128_t x493 = (uint128_t) x471 * x53;
  uint128_t x494 = x461 + x493;
  uint64_t x495 = (uint64_t) (x482 >> 0x33);
- uint128_t x496 = x495 + x488;
- uint64_t x497 = (uint64_t) (x496 >> 0x33);
- uint128_t x498 = x497 + x492;
- uint64_t x499 = (uint64_t) (x498 >> 0x33);
- uint128_t x500 = x499 + x494;
+ uint64_t x496 = (uint64_t) x482 & 0x7ffffffffffff;
+ uint128_t x497 = x495 + x488;
+ uint64_t x498 = (uint64_t) (x497 >> 0x33);
+ uint64_t x499 = (uint64_t) x497 & 0x7ffffffffffff;
+ uint128_t x500 = x498 + x492;
  uint64_t x501 = (uint64_t) (x500 >> 0x33);
- uint128_t x502 = x501 + x470;
- uint64_t x503 = (uint64_t) x482 & 0x7ffffffffffff;
- uint64_t x504 = (uint64_t) (x502 >> 0x33);
- uint64_t x505 = 0x13 * x504;
- uint64_t x506 = x503 + x505;
- uint64_t x507 = x506 >> 0x33;
- uint64_t x508 = (uint64_t) x496 & 0x7ffffffffffff;
- uint64_t x509 = x507 + x508;
- uint64_t x510 = (uint64_t) x502 & 0x7ffffffffffff;
- uint64_t x511 = (uint64_t) x500 & 0x7ffffffffffff;
- uint64_t x512 = x509 >> 0x33;
- uint64_t x513 = (uint64_t) x498 & 0x7ffffffffffff;
- uint64_t x514 = x512 + x513;
- uint64_t x515 = x509 & 0x7ffffffffffff;
- uint64_t x516 = x506 & 0x7ffffffffffff;
- uint64_t x517 = x510 + x439;
- uint64_t x518 = x511 + x440;
- uint64_t x519 = x514 + x443;
+ uint64_t x502 = (uint64_t) x500 & 0x7ffffffffffff;
+ uint128_t x503 = x501 + x494;
+ uint64_t x504 = (uint64_t) (x503 >> 0x33);
+ uint64_t x505 = (uint64_t) x503 & 0x7ffffffffffff;
+ uint128_t x506 = x504 + x470;
+ uint64_t x507 = (uint64_t) (x506 >> 0x33);
+ uint64_t x508 = (uint64_t) x506 & 0x7ffffffffffff;
+ uint64_t x509 = 0x13 * x507;
+ uint64_t x510 = x496 + x509;
+ uint64_t x511 = x510 >> 0x33;
+ uint64_t x512 = x510 & 0x7ffffffffffff;
+ uint64_t x513 = x511 + x499;
+ uint64_t x514 = x513 >> 0x33;
+ uint64_t x515 = x513 & 0x7ffffffffffff;
+ uint64_t x516 = x514 + x502;
+ uint64_t x517 = x508 + x437;
+ uint64_t x518 = x505 + x434;
+ uint64_t x519 = x516 + x445;
  uint64_t x520 = x515 + x444;
- uint64_t x521 = x516 + x445;
+ uint64_t x521 = x512 + x441;
  uint64_t x522 = x521 * 0x2;
  uint64_t x523 = x520 * 0x2;
  uint64_t x524 = x519 * 0x2;
@@ -504,37 +504,37 @@ let (a, b) := Interp-η
  uint128_t x552 = (uint128_t) x519 * x519;
  uint128_t x553 = x551 + x552;
  uint64_t x554 = (uint64_t) (x532 >> 0x33);
- uint128_t x555 = x554 + x538;
- uint64_t x556 = (uint64_t) (x555 >> 0x33);
- uint128_t x557 = x556 + x543;
- uint64_t x558 = (uint64_t) (x557 >> 0x33);
- uint128_t x559 = x558 + x548;
+ uint64_t x555 = (uint64_t) x532 & 0x7ffffffffffff;
+ uint128_t x556 = x554 + x538;
+ uint64_t x557 = (uint64_t) (x556 >> 0x33);
+ uint64_t x558 = (uint64_t) x556 & 0x7ffffffffffff;
+ uint128_t x559 = x557 + x543;
  uint64_t x560 = (uint64_t) (x559 >> 0x33);
- uint128_t x561 = x560 + x553;
- uint64_t x562 = (uint64_t) x532 & 0x7ffffffffffff;
- uint64_t x563 = (uint64_t) (x561 >> 0x33);
- uint64_t x564 = 0x13 * x563;
- uint64_t x565 = x562 + x564;
- uint64_t x566 = x565 >> 0x33;
- uint64_t x567 = (uint64_t) x555 & 0x7ffffffffffff;
- uint64_t x568 = x566 + x567;
- uint64_t x569 = (uint64_t) x561 & 0x7ffffffffffff;
- uint64_t x570 = (uint64_t) x559 & 0x7ffffffffffff;
- uint64_t x571 = x568 >> 0x33;
- uint64_t x572 = (uint64_t) x557 & 0x7ffffffffffff;
- uint64_t x573 = x571 + x572;
- uint64_t x574 = x568 & 0x7ffffffffffff;
- uint64_t x575 = x565 & 0x7ffffffffffff;
- uint64_t x576 = 0xffffffffffffe + x510;
- uint64_t x577 = x576 - x439;
- uint64_t x578 = 0xffffffffffffe + x511;
- uint64_t x579 = x578 - x440;
- uint64_t x580 = 0xffffffffffffe + x514;
- uint64_t x581 = x580 - x443;
+ uint64_t x561 = (uint64_t) x559 & 0x7ffffffffffff;
+ uint128_t x562 = x560 + x548;
+ uint64_t x563 = (uint64_t) (x562 >> 0x33);
+ uint64_t x564 = (uint64_t) x562 & 0x7ffffffffffff;
+ uint128_t x565 = x563 + x553;
+ uint64_t x566 = (uint64_t) (x565 >> 0x33);
+ uint64_t x567 = (uint64_t) x565 & 0x7ffffffffffff;
+ uint64_t x568 = 0x13 * x566;
+ uint64_t x569 = x555 + x568;
+ uint64_t x570 = x569 >> 0x33;
+ uint64_t x571 = x569 & 0x7ffffffffffff;
+ uint64_t x572 = x570 + x558;
+ uint64_t x573 = x572 >> 0x33;
+ uint64_t x574 = x572 & 0x7ffffffffffff;
+ uint64_t x575 = x573 + x561;
+ uint64_t x576 = 0xffffffffffffe + x508;
+ uint64_t x577 = x576 - x437;
+ uint64_t x578 = 0xffffffffffffe + x505;
+ uint64_t x579 = x578 - x434;
+ uint64_t x580 = 0xffffffffffffe + x516;
+ uint64_t x581 = x580 - x445;
  uint64_t x582 = 0xffffffffffffe + x515;
  uint64_t x583 = x582 - x444;
- uint64_t x584 = 0xfffffffffffda + x516;
- uint64_t x585 = x584 - x445;
+ uint64_t x584 = 0xfffffffffffda + x512;
+ uint64_t x585 = x584 - x441;
  uint64_t x586 = x585 * 0x2;
  uint64_t x587 = x583 * 0x2;
  uint64_t x588 = x581 * 0x2;
@@ -568,51 +568,51 @@ let (a, b) := Interp-η
  uint128_t x616 = (uint128_t) x581 * x581;
  uint128_t x617 = x615 + x616;
  uint64_t x618 = (uint64_t) (x596 >> 0x33);
- uint128_t x619 = x618 + x602;
- uint64_t x620 = (uint64_t) (x619 >> 0x33);
- uint128_t x621 = x620 + x607;
- uint64_t x622 = (uint64_t) (x621 >> 0x33);
- uint128_t x623 = x622 + x612;
+ uint64_t x619 = (uint64_t) x596 & 0x7ffffffffffff;
+ uint128_t x620 = x618 + x602;
+ uint64_t x621 = (uint64_t) (x620 >> 0x33);
+ uint64_t x622 = (uint64_t) x620 & 0x7ffffffffffff;
+ uint128_t x623 = x621 + x607;
  uint64_t x624 = (uint64_t) (x623 >> 0x33);
- uint128_t x625 = x624 + x617;
- uint64_t x626 = (uint64_t) x596 & 0x7ffffffffffff;
- uint64_t x627 = (uint64_t) (x625 >> 0x33);
- uint64_t x628 = 0x13 * x627;
- uint64_t x629 = x626 + x628;
- uint64_t x630 = x629 >> 0x33;
- uint64_t x631 = (uint64_t) x619 & 0x7ffffffffffff;
- uint64_t x632 = x630 + x631;
- uint64_t x633 = (uint64_t) x625 & 0x7ffffffffffff;
- uint64_t x634 = (uint64_t) x623 & 0x7ffffffffffff;
- uint64_t x635 = x632 >> 0x33;
- uint64_t x636 = (uint64_t) x621 & 0x7ffffffffffff;
- uint64_t x637 = x635 + x636;
- uint64_t x638 = x632 & 0x7ffffffffffff;
- uint64_t x639 = x629 & 0x7ffffffffffff;
- uint128_t x640 = (uint128_t) x10 * x639;
+ uint64_t x625 = (uint64_t) x623 & 0x7ffffffffffff;
+ uint128_t x626 = x624 + x612;
+ uint64_t x627 = (uint64_t) (x626 >> 0x33);
+ uint64_t x628 = (uint64_t) x626 & 0x7ffffffffffff;
+ uint128_t x629 = x627 + x617;
+ uint64_t x630 = (uint64_t) (x629 >> 0x33);
+ uint64_t x631 = (uint64_t) x629 & 0x7ffffffffffff;
+ uint64_t x632 = 0x13 * x630;
+ uint64_t x633 = x619 + x632;
+ uint64_t x634 = x633 >> 0x33;
+ uint64_t x635 = x633 & 0x7ffffffffffff;
+ uint64_t x636 = x634 + x622;
+ uint64_t x637 = x636 >> 0x33;
+ uint64_t x638 = x636 & 0x7ffffffffffff;
+ uint64_t x639 = x637 + x625;
+ uint128_t x640 = (uint128_t) x10 * x635;
  uint128_t x641 = (uint128_t) x10 * x638;
- uint128_t x642 = (uint128_t) x12 * x639;
+ uint128_t x642 = (uint128_t) x12 * x635;
  uint128_t x643 = x641 + x642;
- uint128_t x644 = (uint128_t) x10 * x637;
- uint128_t x645 = (uint128_t) x14 * x639;
+ uint128_t x644 = (uint128_t) x10 * x639;
+ uint128_t x645 = (uint128_t) x14 * x635;
  uint128_t x646 = x644 + x645;
  uint128_t x647 = (uint128_t) x12 * x638;
  uint128_t x648 = x646 + x647;
- uint128_t x649 = (uint128_t) x10 * x634;
- uint128_t x650 = (uint128_t) x16 * x639;
+ uint128_t x649 = (uint128_t) x10 * x628;
+ uint128_t x650 = (uint128_t) x16 * x635;
  uint128_t x651 = x649 + x650;
- uint128_t x652 = (uint128_t) x12 * x637;
+ uint128_t x652 = (uint128_t) x12 * x639;
  uint128_t x653 = x651 + x652;
  uint128_t x654 = (uint128_t) x14 * x638;
  uint128_t x655 = x653 + x654;
- uint128_t x656 = (uint128_t) x10 * x633;
- uint128_t x657 = (uint128_t) x15 * x639;
+ uint128_t x656 = (uint128_t) x10 * x631;
+ uint128_t x657 = (uint128_t) x15 * x635;
  uint128_t x658 = x656 + x657;
  uint128_t x659 = (uint128_t) x16 * x638;
  uint128_t x660 = x658 + x659;
- uint128_t x661 = (uint128_t) x12 * x634;
+ uint128_t x661 = (uint128_t) x12 * x628;
  uint128_t x662 = x660 + x661;
- uint128_t x663 = (uint128_t) x14 * x637;
+ uint128_t x663 = (uint128_t) x14 * x639;
  uint128_t x664 = x662 + x663;
  uint64_t x665 = x15 * 0x13;
  uint64_t x666 = x12 * 0x13;
@@ -620,47 +620,47 @@ let (a, b) := Interp-η
  uint64_t x668 = x16 * 0x13;
  uint128_t x669 = (uint128_t) x665 * x638;
  uint128_t x670 = x640 + x669;
- uint128_t x671 = (uint128_t) x666 * x633;
+ uint128_t x671 = (uint128_t) x666 * x631;
  uint128_t x672 = x670 + x671;
- uint128_t x673 = (uint128_t) x667 * x634;
+ uint128_t x673 = (uint128_t) x667 * x628;
  uint128_t x674 = x672 + x673;
- uint128_t x675 = (uint128_t) x668 * x637;
+ uint128_t x675 = (uint128_t) x668 * x639;
  uint128_t x676 = x674 + x675;
- uint128_t x677 = (uint128_t) x665 * x637;
+ uint128_t x677 = (uint128_t) x665 * x639;
  uint128_t x678 = x643 + x677;
- uint128_t x679 = (uint128_t) x667 * x633;
+ uint128_t x679 = (uint128_t) x667 * x631;
  uint128_t x680 = x678 + x679;
- uint128_t x681 = (uint128_t) x668 * x634;
+ uint128_t x681 = (uint128_t) x668 * x628;
  uint128_t x682 = x680 + x681;
- uint128_t x683 = (uint128_t) x665 * x634;
+ uint128_t x683 = (uint128_t) x665 * x628;
  uint128_t x684 = x648 + x683;
- uint128_t x685 = (uint128_t) x668 * x633;
+ uint128_t x685 = (uint128_t) x668 * x631;
  uint128_t x686 = x684 + x685;
- uint128_t x687 = (uint128_t) x665 * x633;
+ uint128_t x687 = (uint128_t) x665 * x631;
  uint128_t x688 = x655 + x687;
  uint64_t x689 = (uint64_t) (x676 >> 0x33);
- uint128_t x690 = x689 + x682;
- uint64_t x691 = (uint64_t) (x690 >> 0x33);
- uint128_t x692 = x691 + x686;
- uint64_t x693 = (uint64_t) (x692 >> 0x33);
- uint128_t x694 = x693 + x688;
+ uint64_t x690 = (uint64_t) x676 & 0x7ffffffffffff;
+ uint128_t x691 = x689 + x682;
+ uint64_t x692 = (uint64_t) (x691 >> 0x33);
+ uint64_t x693 = (uint64_t) x691 & 0x7ffffffffffff;
+ uint128_t x694 = x692 + x686;
  uint64_t x695 = (uint64_t) (x694 >> 0x33);
- uint128_t x696 = x695 + x664;
- uint64_t x697 = (uint64_t) x676 & 0x7ffffffffffff;
- uint64_t x698 = (uint64_t) (x696 >> 0x33);
- uint64_t x699 = 0x13 * x698;
- uint64_t x700 = x697 + x699;
- uint64_t x701 = x700 >> 0x33;
- uint64_t x702 = (uint64_t) x690 & 0x7ffffffffffff;
- uint64_t x703 = x701 + x702;
- uint64_t x704 = (uint64_t) x696 & 0x7ffffffffffff;
- uint64_t x705 = (uint64_t) x694 & 0x7ffffffffffff;
- uint64_t x706 = x703 >> 0x33;
- uint64_t x707 = (uint64_t) x692 & 0x7ffffffffffff;
- uint64_t x708 = x706 + x707;
- uint64_t x709 = x703 & 0x7ffffffffffff;
- uint64_t x710 = x700 & 0x7ffffffffffff;
- (Return x240, Return x241, Return x244, Return x245, Return x246, (Return x353, Return x354, Return x357, Return x358, Return x359), (Return x569, Return x570, Return x573, Return x574, Return x575, (Return x704, Return x705, Return x708, Return x709, Return x710))))
+ uint64_t x696 = (uint64_t) x694 & 0x7ffffffffffff;
+ uint128_t x697 = x695 + x688;
+ uint64_t x698 = (uint64_t) (x697 >> 0x33);
+ uint64_t x699 = (uint64_t) x697 & 0x7ffffffffffff;
+ uint128_t x700 = x698 + x664;
+ uint64_t x701 = (uint64_t) (x700 >> 0x33);
+ uint64_t x702 = (uint64_t) x700 & 0x7ffffffffffff;
+ uint64_t x703 = 0x13 * x701;
+ uint64_t x704 = x690 + x703;
+ uint64_t x705 = x704 >> 0x33;
+ uint64_t x706 = x704 & 0x7ffffffffffff;
+ uint64_t x707 = x705 + x693;
+ uint64_t x708 = x707 >> 0x33;
+ uint64_t x709 = x707 & 0x7ffffffffffff;
+ uint64_t x710 = x708 + x696;
+ (Return x238, Return x235, Return x246, Return x245, Return x242, (Return x351, Return x348, Return x359, Return x358, Return x355), (Return x567, Return x564, Return x575, Return x574, Return x571, (Return x702, Return x699, Return x710, Return x709, Return x706))))
 (x, (x0, x1), (x2, x3))%core in
 (let (a0, b0) := a in
 (a0, b0), let (a0, b0) := b in
diff --git a/src/Specific/IntegrationTestMulDisplay.log b/src/Specific/IntegrationTestMulDisplay.log
index 7e13085cc..5f2d7c372 100644
--- a/src/Specific/IntegrationTestMulDisplay.log
+++ b/src/Specific/IntegrationTestMulDisplay.log
@@ -52,27 +52,27 @@ Interp-η
  uint128_t x67 = (uint128_t) x45 * x18;
  uint128_t x68 = x35 + x67;
  uint64_t x69 = (uint64_t) (x56 >> 0x33);
- uint128_t x70 = x69 + x62;
- uint64_t x71 = (uint64_t) (x70 >> 0x33);
- uint128_t x72 = x71 + x66;
- uint64_t x73 = (uint64_t) (x72 >> 0x33);
- uint128_t x74 = x73 + x68;
+ uint64_t x70 = (uint64_t) x56 & 0x7ffffffffffff;
+ uint128_t x71 = x69 + x62;
+ uint64_t x72 = (uint64_t) (x71 >> 0x33);
+ uint64_t x73 = (uint64_t) x71 & 0x7ffffffffffff;
+ uint128_t x74 = x72 + x66;
  uint64_t x75 = (uint64_t) (x74 >> 0x33);
- uint128_t x76 = x75 + x44;
- uint64_t x77 = (uint64_t) x56 & 0x7ffffffffffff;
- uint64_t x78 = (uint64_t) (x76 >> 0x33);
- uint64_t x79 = 0x13 * x78;
- uint64_t x80 = x77 + x79;
- uint64_t x81 = x80 >> 0x33;
- uint64_t x82 = (uint64_t) x70 & 0x7ffffffffffff;
- uint64_t x83 = x81 + x82;
- uint64_t x84 = (uint64_t) x76 & 0x7ffffffffffff;
- uint64_t x85 = (uint64_t) x74 & 0x7ffffffffffff;
- uint64_t x86 = x83 >> 0x33;
- uint64_t x87 = (uint64_t) x72 & 0x7ffffffffffff;
- uint64_t x88 = x86 + x87;
- uint64_t x89 = x83 & 0x7ffffffffffff;
- uint64_t x90 = x80 & 0x7ffffffffffff;
- (Return x84, Return x85, Return x88, Return x89, Return x90))
+ uint64_t x76 = (uint64_t) x74 & 0x7ffffffffffff;
+ uint128_t x77 = x75 + x68;
+ uint64_t x78 = (uint64_t) (x77 >> 0x33);
+ uint64_t x79 = (uint64_t) x77 & 0x7ffffffffffff;
+ uint128_t x80 = x78 + x44;
+ uint64_t x81 = (uint64_t) (x80 >> 0x33);
+ uint64_t x82 = (uint64_t) x80 & 0x7ffffffffffff;
+ uint64_t x83 = 0x13 * x81;
+ uint64_t x84 = x70 + x83;
+ uint64_t x85 = x84 >> 0x33;
+ uint64_t x86 = x84 & 0x7ffffffffffff;
+ uint64_t x87 = x85 + x73;
+ uint64_t x88 = x87 >> 0x33;
+ uint64_t x89 = x87 & 0x7ffffffffffff;
+ uint64_t x90 = x88 + x76;
+ (Return x82, Return x79, Return x90, Return x89, Return x86))
 (x, x0)%core
      : word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/IntegrationTestSquareDisplay.log b/src/Specific/IntegrationTestSquareDisplay.log
index 9d193c47d..385cc6b06 100644
--- a/src/Specific/IntegrationTestSquareDisplay.log
+++ b/src/Specific/IntegrationTestSquareDisplay.log
@@ -35,27 +35,27 @@ Interp-η
  uint128_t x39 = (uint128_t) x6 * x6;
  uint128_t x40 = x38 + x39;
  uint64_t x41 = (uint64_t) (x19 >> 0x33);
- uint128_t x42 = x41 + x25;
- uint64_t x43 = (uint64_t) (x42 >> 0x33);
- uint128_t x44 = x43 + x30;
- uint64_t x45 = (uint64_t) (x44 >> 0x33);
- uint128_t x46 = x45 + x35;
+ uint64_t x42 = (uint64_t) x19 & 0x7ffffffffffff;
+ uint128_t x43 = x41 + x25;
+ uint64_t x44 = (uint64_t) (x43 >> 0x33);
+ uint64_t x45 = (uint64_t) x43 & 0x7ffffffffffff;
+ uint128_t x46 = x44 + x30;
  uint64_t x47 = (uint64_t) (x46 >> 0x33);
- uint128_t x48 = x47 + x40;
- uint64_t x49 = (uint64_t) x19 & 0x7ffffffffffff;
- uint64_t x50 = (uint64_t) (x48 >> 0x33);
- uint64_t x51 = 0x13 * x50;
- uint64_t x52 = x49 + x51;
- uint64_t x53 = x52 >> 0x33;
- uint64_t x54 = (uint64_t) x42 & 0x7ffffffffffff;
- uint64_t x55 = x53 + x54;
- uint64_t x56 = (uint64_t) x48 & 0x7ffffffffffff;
- uint64_t x57 = (uint64_t) x46 & 0x7ffffffffffff;
- uint64_t x58 = x55 >> 0x33;
- uint64_t x59 = (uint64_t) x44 & 0x7ffffffffffff;
- uint64_t x60 = x58 + x59;
- uint64_t x61 = x55 & 0x7ffffffffffff;
- uint64_t x62 = x52 & 0x7ffffffffffff;
- (Return x56, Return x57, Return x60, Return x61, Return x62))
+ uint64_t x48 = (uint64_t) x46 & 0x7ffffffffffff;
+ uint128_t x49 = x47 + x35;
+ uint64_t x50 = (uint64_t) (x49 >> 0x33);
+ uint64_t x51 = (uint64_t) x49 & 0x7ffffffffffff;
+ uint128_t x52 = x50 + x40;
+ uint64_t x53 = (uint64_t) (x52 >> 0x33);
+ uint64_t x54 = (uint64_t) x52 & 0x7ffffffffffff;
+ uint64_t x55 = 0x13 * x53;
+ uint64_t x56 = x42 + x55;
+ uint64_t x57 = x56 >> 0x33;
+ uint64_t x58 = x56 & 0x7ffffffffffff;
+ uint64_t x59 = x57 + x45;
+ uint64_t x60 = x59 >> 0x33;
+ uint64_t x61 = x59 & 0x7ffffffffffff;
+ uint64_t x62 = x60 + x48;
+ (Return x54, Return x51, Return x62, Return x61, Return x58))
 x
      : word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)