make display (freeze, ladderstep with adc)

2 files changed, 77 insertions, 96 deletions

diff --git a/src/Specific/IntegrationTestFreezeDisplay.log b/src/Specific/IntegrationTestFreezeDisplay.log
index 6ae4cff79..55504a7fb 100644
--- a/src/Specific/IntegrationTestFreezeDisplay.log
+++ b/src/Specific/IntegrationTestFreezeDisplay.log
@@ -3,36 +3,21 @@ Interp-η
 (λ var : Syntax.base_type → Type,
  λ '(x7, x8, x6, x4, x2)%core,
  uint64_t x10, ℤ x11 = Op (Syntax.AddWithGetCarry 51 (Syntax.TWord 0) (Syntax.TWord 6) Syntax.TZ (Syntax.TWord 6) Syntax.TZ) (0x0, Return x2, Const (-2251799813685229));
- uint64_t x13, bool x14 = addcarryx_u51(0x0, 0x0, x10);
- ℤ x15 = x11 + x14;
- uint64_t x17, ℤ x18 = Op (Syntax.AddWithGetCarry 51 (Syntax.TWord 0) (Syntax.TWord 6) Syntax.TZ (Syntax.TWord 6) Syntax.TZ) (0x0, Return x4, Const (-2251799813685247));
- uint64_t x20, ℤ x21 = Op (Syntax.AddWithGetCarry 51 (Syntax.TWord 0) Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) Syntax.TZ) (0x0, Return x15, Return x17);
- ℤ x22 = x18 + x21;
- uint64_t x24, ℤ x25 = Op (Syntax.AddWithGetCarry 51 (Syntax.TWord 0) (Syntax.TWord 6) Syntax.TZ (Syntax.TWord 6) Syntax.TZ) (0x0, Return x6, Const (-2251799813685247));
- uint64_t x27, ℤ x28 = Op (Syntax.AddWithGetCarry 51 (Syntax.TWord 0) Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) Syntax.TZ) (0x0, Return x22, Return x24);
- ℤ x29 = x25 + x28;
- uint64_t x31, ℤ x32 = Op (Syntax.AddWithGetCarry 51 (Syntax.TWord 0) (Syntax.TWord 6) Syntax.TZ (Syntax.TWord 6) Syntax.TZ) (0x0, Return x8, Const (-2251799813685247));
- uint64_t x34, ℤ x35 = Op (Syntax.AddWithGetCarry 51 (Syntax.TWord 0) Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) Syntax.TZ) (0x0, Return x29, Return x31);
- ℤ x36 = x32 + x35;
- uint64_t x38, ℤ x39 = Op (Syntax.AddWithGetCarry 51 (Syntax.TWord 0) (Syntax.TWord 6) Syntax.TZ (Syntax.TWord 6) Syntax.TZ) (0x0, Return x7, Const (-2251799813685247));
- uint64_t x41, ℤ x42 = Op (Syntax.AddWithGetCarry 51 (Syntax.TWord 0) Syntax.TZ (Syntax.TWord 6) (Syntax.TWord 6) Syntax.TZ) (0x0, Return x36, Return x38);
- ℤ x43 = x39 + x42;
- uint64_t x44 = (uint64_t) (x43 == 0 ? 0x0 : 0xffffffffffffffffL);
- uint64_t x46, bool x47 = addcarryx_u51(0x0, x13, x44 & 0x7ffffffffffed);
- uint64_t x49, bool x50 = addcarryx_u51(0x0, 0x0, x46);
- bool x51 = x47 + x50;
- uint64_t x53, bool x54 = addcarryx_u51(0x0, x20, x44 & 0x7ffffffffffff);
- uint64_t x56, bool x57 = addcarryx_u51(0x0, x51, x53);
- uint64_t x58 = (uint64_t) x54 + x57;
- uint64_t x60, bool x61 = addcarryx_u51(0x0, x27, x44 & 0x7ffffffffffff);
- uint64_t x63, bool x64 = addcarryx_u51(0x0, x58, x60);
- uint64_t x65 = (uint64_t) x61 + x64;
- uint64_t x67, bool x68 = addcarryx_u51(0x0, x34, x44 & 0x7ffffffffffff);
- uint64_t x70, bool x71 = addcarryx_u51(0x0, x65, x67);
- uint64_t x72 = (uint64_t) x68 + x71;
- uint64_t x74, bool x75 = addcarryx_u51(0x0, x41, x44 & 0x7ffffffffffff);
- uint64_t x77, bool x78 = addcarryx_u51(0x0, x72, x74);
- uint64_t _ = (uint64_t) x75 + x78;
- return (x77, x70, x63, x56, x49))
+ uint64_t x13, ℤ x14 = Op (Syntax.AddWithGetCarry 51 Syntax.TZ (Syntax.TWord 6) Syntax.TZ (Syntax.TWord 6) Syntax.TZ) (Return x11, Return x4, Const (-2251799813685247));
+ uint64_t x16, ℤ x17 = Op (Syntax.AddWithGetCarry 51 Syntax.TZ (Syntax.TWord 6) Syntax.TZ (Syntax.TWord 6) Syntax.TZ) (Return x14, Return x6, Const (-2251799813685247));
+ uint64_t x19, ℤ x20 = Op (Syntax.AddWithGetCarry 51 Syntax.TZ (Syntax.TWord 6) Syntax.TZ (Syntax.TWord 6) Syntax.TZ) (Return x17, Return x8, Const (-2251799813685247));
+ uint64_t x22, ℤ x23 = Op (Syntax.AddWithGetCarry 51 Syntax.TZ (Syntax.TWord 6) Syntax.TZ (Syntax.TWord 6) Syntax.TZ) (Return x20, Return x7, Const (-2251799813685247));
+ uint64_t x24 = (uint64_t) (x23 == 0 ? 0x0 : 0xffffffffffffffffL);
+ uint64_t x25 = x24 & 0x7ffffffffffed;
+ uint64_t x27, bool x28 = addcarryx_u51(0x0, x10, x25);
+ uint64_t x29 = x24 & 0x7ffffffffffff;
+ uint64_t x31, bool x32 = addcarryx_u51(x28, x13, x29);
+ uint64_t x33 = x24 & 0x7ffffffffffff;
+ uint64_t x35, bool x36 = addcarryx_u51(x32, x16, x33);
+ uint64_t x37 = x24 & 0x7ffffffffffff;
+ uint64_t x39, bool x40 = addcarryx_u51(x36, x19, x37);
+ uint64_t x41 = x24 & 0x7ffffffffffff;
+ uint64_t x43, bool _ = addcarryx_u51(x40, x22, x41);
+ (Return x43, Return x39, Return x35, Return x31, Return x27))
 x
      : word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t)
diff --git a/src/Specific/IntegrationTestLadderstepDisplay.log b/src/Specific/IntegrationTestLadderstepDisplay.log
index 5895c9c61..cb7d11ba4 100644
--- a/src/Specific/IntegrationTestLadderstepDisplay.log
+++ b/src/Specific/IntegrationTestLadderstepDisplay.log
@@ -302,71 +302,67 @@ let (a, b) := Interp-η
  uint128_t x350 = (uint128_t) x345 * 0x1db41;
  uint128_t x351 = (uint128_t) x344 * 0x1db41;
  uint128_t x352 = (uint128_t) x343 * 0x1db41;
- uint64_t _ = x343 * 0x13;
- uint64_t _ = x346 * 0x13;
- uint64_t _ = x345 * 0x13;
- uint64_t _ = x344 * 0x13;
- uint64_t x357 = (uint64_t) (x348 >> 0x33);
- uint64_t x358 = (uint64_t) x348 & 0x7ffffffffffff;
- uint128_t x359 = x357 + x349;
- uint64_t x360 = (uint64_t) (x359 >> 0x33);
- uint64_t x361 = (uint64_t) x359 & 0x7ffffffffffff;
- uint128_t x362 = x360 + x350;
- uint64_t x363 = (uint64_t) (x362 >> 0x33);
- uint64_t x364 = (uint64_t) x362 & 0x7ffffffffffff;
- uint128_t x365 = x363 + x351;
- uint64_t x366 = (uint64_t) (x365 >> 0x33);
- uint64_t x367 = (uint64_t) x365 & 0x7ffffffffffff;
- uint128_t x368 = x366 + x352;
- uint64_t x369 = (uint64_t) (x368 >> 0x33);
- uint64_t x370 = (uint64_t) x368 & 0x7ffffffffffff;
- uint64_t x371 = x358 + 0x13 * x369;
- bool x372 = (bool) (x371 >> 0x33);
- uint64_t x373 = x371 & 0x7ffffffffffff;
- uint64_t x374 = x372 + x361;
- bool x375 = (bool) (x374 >> 0x33);
- uint64_t x376 = x374 & 0x7ffffffffffff;
- uint64_t x377 = x375 + x364;
- uint64_t x378 = x370 + x270;
- uint64_t x379 = x367 + x267;
- uint64_t x380 = x377 + x277;
- uint64_t x381 = x376 + x276;
- uint64_t x382 = x373 + x273;
- uint128_t x383 = (uint128_t) x347 * x382;
- uint128_t x384 = (uint128_t) x347 * x381 + (uint128_t) x346 * x382;
- uint128_t x385 = (uint128_t) x347 * x380 + (uint128_t) x345 * x382 + (uint128_t) x346 * x381;
- uint128_t x386 = (uint128_t) x347 * x379 + (uint128_t) x344 * x382 + (uint128_t) x346 * x380 + (uint128_t) x345 * x381;
- uint128_t x387 = (uint128_t) x347 * x378 + (uint128_t) x343 * x382 + (uint128_t) x344 * x381 + (uint128_t) x346 * x379 + (uint128_t) x345 * x380;
- uint64_t x388 = x343 * 0x13;
- uint64_t x389 = x346 * 0x13;
- uint64_t x390 = x345 * 0x13;
- uint64_t x391 = x344 * 0x13;
- uint128_t x392 = x383 + (uint128_t) x388 * x381 + (uint128_t) x389 * x378 + (uint128_t) x390 * x379 + (uint128_t) x391 * x380;
- uint128_t x393 = x384 + (uint128_t) x388 * x380 + (uint128_t) x390 * x378 + (uint128_t) x391 * x379;
- uint128_t x394 = x385 + (uint128_t) x388 * x379 + (uint128_t) x391 * x378;
- uint128_t x395 = x386 + (uint128_t) x388 * x378;
- uint64_t x396 = (uint64_t) (x392 >> 0x33);
- uint64_t x397 = (uint64_t) x392 & 0x7ffffffffffff;
- uint128_t x398 = x396 + x393;
- uint64_t x399 = (uint64_t) (x398 >> 0x33);
- uint64_t x400 = (uint64_t) x398 & 0x7ffffffffffff;
- uint128_t x401 = x399 + x394;
- uint64_t x402 = (uint64_t) (x401 >> 0x33);
- uint64_t x403 = (uint64_t) x401 & 0x7ffffffffffff;
- uint128_t x404 = x402 + x395;
- uint64_t x405 = (uint64_t) (x404 >> 0x33);
- uint64_t x406 = (uint64_t) x404 & 0x7ffffffffffff;
- uint128_t x407 = x405 + x387;
- uint64_t x408 = (uint64_t) (x407 >> 0x33);
- uint64_t x409 = (uint64_t) x407 & 0x7ffffffffffff;
- uint64_t x410 = x397 + 0x13 * x408;
- uint64_t x411 = x410 >> 0x33;
- uint64_t x412 = x410 & 0x7ffffffffffff;
- uint64_t x413 = x411 + x400;
- bool x414 = (bool) (x413 >> 0x33);
- uint64_t x415 = x413 & 0x7ffffffffffff;
- uint64_t x416 = x414 + x403;
- return (Return x335, Return x332, Return x342, Return x341, Return x338, (Return x409, Return x406, Return x416, Return x415, Return x412), (Return x174, Return x171, Return x181, Return x180, Return x177, (Return x239, Return x236, Return x246, Return x245, Return x242))))
+ uint64_t x353 = (uint64_t) (x348 >> 0x33);
+ uint64_t x354 = (uint64_t) x348 & 0x7ffffffffffff;
+ uint128_t x355 = x353 + x349;
+ uint64_t x356 = (uint64_t) (x355 >> 0x33);
+ uint64_t x357 = (uint64_t) x355 & 0x7ffffffffffff;
+ uint128_t x358 = x356 + x350;
+ uint64_t x359 = (uint64_t) (x358 >> 0x33);
+ uint64_t x360 = (uint64_t) x358 & 0x7ffffffffffff;
+ uint128_t x361 = x359 + x351;
+ uint64_t x362 = (uint64_t) (x361 >> 0x33);
+ uint64_t x363 = (uint64_t) x361 & 0x7ffffffffffff;
+ uint128_t x364 = x362 + x352;
+ uint64_t x365 = (uint64_t) (x364 >> 0x33);
+ uint64_t x366 = (uint64_t) x364 & 0x7ffffffffffff;
+ uint64_t x367 = x354 + 0x13 * x365;
+ bool x368 = (bool) (x367 >> 0x33);
+ uint64_t x369 = x367 & 0x7ffffffffffff;
+ uint64_t x370 = x368 + x357;
+ bool x371 = (bool) (x370 >> 0x33);
+ uint64_t x372 = x370 & 0x7ffffffffffff;
+ uint64_t x373 = x371 + x360;
+ uint64_t x374 = x366 + x270;
+ uint64_t x375 = x363 + x267;
+ uint64_t x376 = x373 + x277;
+ uint64_t x377 = x372 + x276;
+ uint64_t x378 = x369 + x273;
+ uint128_t x379 = (uint128_t) x347 * x378;
+ uint128_t x380 = (uint128_t) x347 * x377 + (uint128_t) x346 * x378;
+ uint128_t x381 = (uint128_t) x347 * x376 + (uint128_t) x345 * x378 + (uint128_t) x346 * x377;
+ uint128_t x382 = (uint128_t) x347 * x375 + (uint128_t) x344 * x378 + (uint128_t) x346 * x376 + (uint128_t) x345 * x377;
+ uint128_t x383 = (uint128_t) x347 * x374 + (uint128_t) x343 * x378 + (uint128_t) x344 * x377 + (uint128_t) x346 * x375 + (uint128_t) x345 * x376;
+ uint64_t x384 = x343 * 0x13;
+ uint64_t x385 = x346 * 0x13;
+ uint64_t x386 = x345 * 0x13;
+ uint64_t x387 = x344 * 0x13;
+ uint128_t x388 = x379 + (uint128_t) x384 * x377 + (uint128_t) x385 * x374 + (uint128_t) x386 * x375 + (uint128_t) x387 * x376;
+ uint128_t x389 = x380 + (uint128_t) x384 * x376 + (uint128_t) x386 * x374 + (uint128_t) x387 * x375;
+ uint128_t x390 = x381 + (uint128_t) x384 * x375 + (uint128_t) x387 * x374;
+ uint128_t x391 = x382 + (uint128_t) x384 * x374;
+ uint64_t x392 = (uint64_t) (x388 >> 0x33);
+ uint64_t x393 = (uint64_t) x388 & 0x7ffffffffffff;
+ uint128_t x394 = x392 + x389;
+ uint64_t x395 = (uint64_t) (x394 >> 0x33);
+ uint64_t x396 = (uint64_t) x394 & 0x7ffffffffffff;
+ uint128_t x397 = x395 + x390;
+ uint64_t x398 = (uint64_t) (x397 >> 0x33);
+ uint64_t x399 = (uint64_t) x397 & 0x7ffffffffffff;
+ uint128_t x400 = x398 + x391;
+ uint64_t x401 = (uint64_t) (x400 >> 0x33);
+ uint64_t x402 = (uint64_t) x400 & 0x7ffffffffffff;
+ uint128_t x403 = x401 + x383;
+ uint64_t x404 = (uint64_t) (x403 >> 0x33);
+ uint64_t x405 = (uint64_t) x403 & 0x7ffffffffffff;
+ uint64_t x406 = x393 + 0x13 * x404;
+ uint64_t x407 = x406 >> 0x33;
+ uint64_t x408 = x406 & 0x7ffffffffffff;
+ uint64_t x409 = x407 + x396;
+ bool x410 = (bool) (x409 >> 0x33);
+ uint64_t x411 = x409 & 0x7ffffffffffff;
+ uint64_t x412 = x410 + x399;
+ return (Return x335, Return x332, Return x342, Return x341, Return x338, (Return x405, Return x402, Return x412, Return x411, Return x408), (Return x174, Return x171, Return x181, Return x180, Return x177, (Return x239, Return x236, Return x246, Return x245, Return x242))))
 (x, (x0, x1), (x2, x3))%core in
 (let (a0, b0) := a in
 (a0, b0), let (a0, b0) := b in