diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-16 00:24:19 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-16 16:51:11 -0500 |
| commit | 4441785fb44b88bb6943ddbf639d872c8c903281 (patch) | |
| tree | 880ac538d950628dd526bb63580201f2093c59f0 | |
| parent | 60bade02ccd577550bfcd5974d3c62a3d40e751a (diff) | |
Constant-propogate 0+x and x+0 after bounds
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------
21m22.67s | Total | 21m28.24s || -0m05.56s | -0.43%
--------------------------------------------------------------------------------------------
4m09.95s | PushButtonSynthesis.vo | 4m14.76s || -0m04.81s | -1.88%
3m07.95s | p384_32.c | 3m11.17s || -0m03.21s | -1.68%
2m06.43s | Rewriter.vo | 2m06.15s || +0m00.28s | +0.22%
1m55.83s | RewriterWf2.vo | 1m56.15s || -0m00.32s | -0.27%
1m52.36s | RewriterRulesGood.vo | 1m52.34s || +0m00.01s | +0.01%
1m46.52s | RewriterRulesInterpGood.vo | 1m45.70s || +0m00.82s | +0.77%
0m46.56s | RewriterInterpProofs1.vo | 0m46.72s || -0m00.15s | -0.34%
0m45.04s | ExtractionHaskell/word_by_word_montgomery | 0m45.33s || -0m00.28s | -0.63%
0m39.17s | p521_32.c | 0m39.07s || +0m00.10s | +0.25%
0m32.40s | p521_64.c | 0m32.64s || -0m00.24s | -0.73%
0m31.13s | ExtractionHaskell/unsaturated_solinas | 0m30.88s || +0m00.25s | +0.80%
0m24.20s | ExtractionHaskell/saturated_solinas | 0m24.27s || -0m00.07s | -0.28%
0m23.72s | RewriterWf1.vo | 0m23.42s || +0m00.29s | +1.28%
0m17.52s | ExtractionOCaml/word_by_word_montgomery | 0m17.10s || +0m00.41s | +2.45%
0m13.39s | secp256k1_32.c | 0m13.29s || +0m00.10s | +0.75%
0m13.08s | p256_32.c | 0m13.26s || -0m00.17s | -1.35%
0m11.49s | p484_64.c | 0m11.18s || +0m00.31s | +2.77%
0m10.68s | ExtractionOCaml/unsaturated_solinas | 0m10.64s || +0m00.03s | +0.37%
0m10.11s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.10s || +0m00.00s | +0.09%
0m07.96s | ExtractionOCaml/saturated_solinas | 0m07.95s || +0m00.00s | +0.12%
0m06.81s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.76s || +0m00.04s | +0.73%
0m06.30s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.26s || +0m00.04s | +0.63%
0m06.07s | p224_32.c | 0m05.94s || +0m00.12s | +2.18%
0m06.06s | BoundsPipeline.vo | 0m06.08s || -0m00.02s | -0.32%
0m05.46s | p384_64.c | 0m05.30s || +0m00.16s | +3.01%
0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.18s || +0m00.10s | +1.93%
0m04.97s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.99s || -0m00.02s | -0.40%
0m04.13s | ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.03s | +0.73%
0m02.34s | curve25519_32.c | 0m02.21s || +0m00.12s | +5.88%
0m01.59s | curve25519_64.c | 0m01.47s || +0m00.12s | +8.16%
0m01.46s | CLI.vo | 0m01.48s || -0m00.02s | -1.35%
0m01.15s | secp256k1_64.c | 0m01.03s || +0m00.11s | +11.65%
0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88%
0m01.14s | StandaloneHaskellMain.vo | 0m01.09s || +0m00.04s | +4.58%
0m01.14s | StandaloneOCamlMain.vo | 0m01.12s || +0m00.01s | +1.78%
0m01.09s | p256_64.c | 0m00.98s || +0m00.11s | +11.22%
0m01.06s | p224_64.c | 0m01.00s || +0m00.06s | +6.00%
| -rw-r--r-- | curve25519_32.c | 136 | ||||
| -rw-r--r-- | p224_32.c | 158 | ||||
| -rw-r--r-- | p224_64.c | 114 | ||||
| -rw-r--r-- | p256_32.c | 186 | ||||
| -rw-r--r-- | p256_64.c | 134 | ||||
| -rw-r--r-- | p384_32.c | 286 | ||||
| -rw-r--r-- | p384_64.c | 224 | ||||
| -rw-r--r-- | p484_64.c | 266 | ||||
| -rw-r--r-- | p521_32.c | 326 | ||||
| -rw-r--r-- | p521_64.c | 238 | ||||
| -rw-r--r-- | secp256k1_32.c | 186 | ||||
| -rw-r--r-- | secp256k1_64.c | 134 | ||||
| -rw-r--r-- | src/Rewriter.v | 7 | ||||
| -rw-r--r-- | src/arith_with_casts_rewrite_head.out | 123 |
14 files changed, 1266 insertions, 1252 deletions
diff --git a/curve25519_32.c b/curve25519_32.c index 508141786..820a5c9bb 100644 --- a/curve25519_32.c +++ b/curve25519_32.c @@ -749,41 +749,40 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) { uint8_t x82 = (uint8_t)(x80 >> 8); uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff)); uint8_t x84 = (uint8_t)(x82 & UINT8_C(0xff)); - uint32_t x85 = (0x0 + x32); - uint32_t x86 = (x85 >> 8); - uint8_t x87 = (uint8_t)(x85 & UINT8_C(0xff)); - uint32_t x88 = (x86 >> 8); - uint8_t x89 = (uint8_t)(x86 & UINT8_C(0xff)); - fiat_25519_uint1 x90 = (fiat_25519_uint1)(x88 >> 8); - uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff)); - uint32_t x92 = (x90 + x45); - uint32_t x93 = (x92 >> 8); - uint8_t x94 = (uint8_t)(x92 & UINT8_C(0xff)); - uint32_t x95 = (x93 >> 8); - uint8_t x96 = (uint8_t)(x93 & UINT8_C(0xff)); - uint8_t x97 = (uint8_t)(x95 >> 8); - uint8_t x98 = (uint8_t)(x95 & UINT8_C(0xff)); - uint32_t x99 = (x97 + x44); - uint32_t x100 = (x99 >> 8); - uint8_t x101 = (uint8_t)(x99 & UINT8_C(0xff)); - uint32_t x102 = (x100 >> 8); - uint8_t x103 = (uint8_t)(x100 & UINT8_C(0xff)); - uint8_t x104 = (uint8_t)(x102 >> 8); - uint8_t x105 = (uint8_t)(x102 & UINT8_C(0xff)); - uint32_t x106 = (x104 + x43); - uint32_t x107 = (x106 >> 8); - uint8_t x108 = (uint8_t)(x106 & UINT8_C(0xff)); - uint32_t x109 = (x107 >> 8); - uint8_t x110 = (uint8_t)(x107 & UINT8_C(0xff)); - uint8_t x111 = (uint8_t)(x109 >> 8); - uint8_t x112 = (uint8_t)(x109 & UINT8_C(0xff)); - uint32_t x113 = (x111 + x42); - uint32_t x114 = (x113 >> 8); - uint8_t x115 = (uint8_t)(x113 & UINT8_C(0xff)); - uint32_t x116 = (x114 >> 8); - uint8_t x117 = (uint8_t)(x114 & UINT8_C(0xff)); - uint8_t x118 = (uint8_t)(x116 >> 8); - uint8_t x119 = (uint8_t)(x116 & UINT8_C(0xff)); + uint32_t x85 = (x32 >> 8); + uint8_t x86 = (uint8_t)(x32 & UINT8_C(0xff)); + uint32_t x87 = (x85 >> 8); + uint8_t x88 = (uint8_t)(x85 & UINT8_C(0xff)); + fiat_25519_uint1 x89 = (fiat_25519_uint1)(x87 >> 8); + uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff)); + uint32_t x91 = (x89 + x45); + uint32_t x92 = (x91 >> 8); + uint8_t x93 = (uint8_t)(x91 & UINT8_C(0xff)); + uint32_t x94 = (x92 >> 8); + uint8_t x95 = (uint8_t)(x92 & UINT8_C(0xff)); + uint8_t x96 = (uint8_t)(x94 >> 8); + uint8_t x97 = (uint8_t)(x94 & UINT8_C(0xff)); + uint32_t x98 = (x96 + x44); + uint32_t x99 = (x98 >> 8); + uint8_t x100 = (uint8_t)(x98 & UINT8_C(0xff)); + uint32_t x101 = (x99 >> 8); + uint8_t x102 = (uint8_t)(x99 & UINT8_C(0xff)); + uint8_t x103 = (uint8_t)(x101 >> 8); + uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff)); + uint32_t x105 = (x103 + x43); + uint32_t x106 = (x105 >> 8); + uint8_t x107 = (uint8_t)(x105 & UINT8_C(0xff)); + uint32_t x108 = (x106 >> 8); + uint8_t x109 = (uint8_t)(x106 & UINT8_C(0xff)); + uint8_t x110 = (uint8_t)(x108 >> 8); + uint8_t x111 = (uint8_t)(x108 & UINT8_C(0xff)); + uint32_t x112 = (x110 + x42); + uint32_t x113 = (x112 >> 8); + uint8_t x114 = (uint8_t)(x112 & UINT8_C(0xff)); + uint32_t x115 = (x113 >> 8); + uint8_t x116 = (uint8_t)(x113 & UINT8_C(0xff)); + uint8_t x117 = (uint8_t)(x115 >> 8); + uint8_t x118 = (uint8_t)(x115 & UINT8_C(0xff)); out1[0] = x51; out1[1] = x53; out1[2] = x55; @@ -800,22 +799,22 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) { out1[13] = x81; out1[14] = x83; out1[15] = x84; - out1[16] = x87; - out1[17] = x89; - out1[18] = x91; - out1[19] = x94; - out1[20] = x96; - out1[21] = x98; - out1[22] = x101; - out1[23] = x103; - out1[24] = x105; - out1[25] = x108; - out1[26] = x110; - out1[27] = x112; - out1[28] = x115; - out1[29] = x117; - out1[30] = x119; - out1[31] = x118; + out1[16] = x86; + out1[17] = x88; + out1[18] = x90; + out1[19] = x93; + out1[20] = x95; + out1[21] = x97; + out1[22] = x100; + out1[23] = x102; + out1[24] = x104; + out1[25] = x107; + out1[26] = x109; + out1[27] = x111; + out1[28] = x114; + out1[29] = x116; + out1[30] = x118; + out1[31] = x117; } /* @@ -880,28 +879,27 @@ static void fiat_25519_from_bytes(uint32_t out1[10], const uint8_t arg1[32]) { uint32_t x53 = (x51 & UINT32_C(0x1ffffff)); uint32_t x54 = (x52 + x41); uint32_t x55 = (x54 & UINT32_C(0x3ffffff)); - uint32_t x56 = (0x0 + x40); - uint8_t x57 = (uint8_t)(x56 >> 25); - uint32_t x58 = (x56 & UINT32_C(0x1ffffff)); - uint32_t x59 = (x57 + x39); - uint8_t x60 = (uint8_t)(x59 >> 26); - uint32_t x61 = (x59 & UINT32_C(0x3ffffff)); - uint32_t x62 = (x60 + x38); - uint8_t x63 = (uint8_t)(x62 >> 25); - uint32_t x64 = (x62 & UINT32_C(0x1ffffff)); - uint32_t x65 = (x63 + x37); - uint8_t x66 = (uint8_t)(x65 >> 26); - uint32_t x67 = (x65 & UINT32_C(0x3ffffff)); - uint32_t x68 = (x66 + x36); + uint8_t x56 = (uint8_t)(x40 >> 25); + uint32_t x57 = (x40 & UINT32_C(0x1ffffff)); + uint32_t x58 = (x56 + x39); + uint8_t x59 = (uint8_t)(x58 >> 26); + uint32_t x60 = (x58 & UINT32_C(0x3ffffff)); + uint32_t x61 = (x59 + x38); + uint8_t x62 = (uint8_t)(x61 >> 25); + uint32_t x63 = (x61 & UINT32_C(0x1ffffff)); + uint32_t x64 = (x62 + x37); + uint8_t x65 = (uint8_t)(x64 >> 26); + uint32_t x66 = (x64 & UINT32_C(0x3ffffff)); + uint32_t x67 = (x65 + x36); out1[0] = x35; out1[1] = x47; out1[2] = x50; out1[3] = x53; out1[4] = x55; - out1[5] = x58; - out1[6] = x61; - out1[7] = x64; - out1[8] = x67; - out1[9] = x68; + out1[5] = x57; + out1[6] = x60; + out1[7] = x63; + out1[8] = x66; + out1[9] = x67; } @@ -2632,81 +2632,75 @@ static void fiat_p224_to_bytes(uint8_t out1[28], const uint32_t arg1[7]) { uint8_t x12 = (uint8_t)(x10 >> 8); uint8_t x13 = (uint8_t)(x10 & UINT8_C(0xff)); uint8_t x14 = (uint8_t)(x12 & UINT8_C(0xff)); - uint32_t x15 = (0x0 + x6); - uint32_t x16 = (x15 >> 8); - uint8_t x17 = (uint8_t)(x15 & UINT8_C(0xff)); - uint32_t x18 = (x16 >> 8); - uint8_t x19 = (uint8_t)(x16 & UINT8_C(0xff)); - uint8_t x20 = (uint8_t)(x18 >> 8); - uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff)); - uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); - uint32_t x23 = (0x0 + x5); - uint32_t x24 = (x23 >> 8); - uint8_t x25 = (uint8_t)(x23 & UINT8_C(0xff)); - uint32_t x26 = (x24 >> 8); + uint32_t x15 = (x6 >> 8); + uint8_t x16 = (uint8_t)(x6 & UINT8_C(0xff)); + uint32_t x17 = (x15 >> 8); + uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff)); + uint8_t x19 = (uint8_t)(x17 >> 8); + uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff)); + uint8_t x21 = (uint8_t)(x19 & UINT8_C(0xff)); + uint32_t x22 = (x5 >> 8); + uint8_t x23 = (uint8_t)(x5 & UINT8_C(0xff)); + uint32_t x24 = (x22 >> 8); + uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); + uint8_t x26 = (uint8_t)(x24 >> 8); uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); - uint8_t x28 = (uint8_t)(x26 >> 8); - uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); - uint8_t x30 = (uint8_t)(x28 & UINT8_C(0xff)); - uint32_t x31 = (0x0 + x4); - uint32_t x32 = (x31 >> 8); - uint8_t x33 = (uint8_t)(x31 & UINT8_C(0xff)); - uint32_t x34 = (x32 >> 8); - uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); - uint8_t x36 = (uint8_t)(x34 >> 8); - uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff)); - uint8_t x38 = (uint8_t)(x36 & UINT8_C(0xff)); - uint32_t x39 = (0x0 + x3); - uint32_t x40 = (x39 >> 8); - uint8_t x41 = (uint8_t)(x39 & UINT8_C(0xff)); - uint32_t x42 = (x40 >> 8); - uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff)); - uint8_t x44 = (uint8_t)(x42 >> 8); - uint8_t x45 = (uint8_t)(x42 & UINT8_C(0xff)); - uint8_t x46 = (uint8_t)(x44 & UINT8_C(0xff)); - uint32_t x47 = (0x0 + x2); - uint32_t x48 = (x47 >> 8); + uint8_t x28 = (uint8_t)(x26 & UINT8_C(0xff)); + uint32_t x29 = (x4 >> 8); + uint8_t x30 = (uint8_t)(x4 & UINT8_C(0xff)); + uint32_t x31 = (x29 >> 8); + uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); + uint8_t x33 = (uint8_t)(x31 >> 8); + uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); + uint8_t x35 = (uint8_t)(x33 & UINT8_C(0xff)); + uint32_t x36 = (x3 >> 8); + uint8_t x37 = (uint8_t)(x3 & UINT8_C(0xff)); + uint32_t x38 = (x36 >> 8); + uint8_t x39 = (uint8_t)(x36 & UINT8_C(0xff)); + uint8_t x40 = (uint8_t)(x38 >> 8); + uint8_t x41 = (uint8_t)(x38 & UINT8_C(0xff)); + uint8_t x42 = (uint8_t)(x40 & UINT8_C(0xff)); + uint32_t x43 = (x2 >> 8); + uint8_t x44 = (uint8_t)(x2 & UINT8_C(0xff)); + uint32_t x45 = (x43 >> 8); + uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); + uint8_t x47 = (uint8_t)(x45 >> 8); + uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); uint8_t x49 = (uint8_t)(x47 & UINT8_C(0xff)); - uint32_t x50 = (x48 >> 8); - uint8_t x51 = (uint8_t)(x48 & UINT8_C(0xff)); - uint8_t x52 = (uint8_t)(x50 >> 8); + uint32_t x50 = (x1 >> 8); + uint8_t x51 = (uint8_t)(x1 & UINT8_C(0xff)); + uint32_t x52 = (x50 >> 8); uint8_t x53 = (uint8_t)(x50 & UINT8_C(0xff)); - uint8_t x54 = (uint8_t)(x52 & UINT8_C(0xff)); - uint32_t x55 = (0x0 + x1); - uint32_t x56 = (x55 >> 8); - uint8_t x57 = (uint8_t)(x55 & UINT8_C(0xff)); - uint32_t x58 = (x56 >> 8); - uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); - uint8_t x60 = (uint8_t)(x58 >> 8); - uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); + uint8_t x54 = (uint8_t)(x52 >> 8); + uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); out1[0] = x9; out1[1] = x11; out1[2] = x13; out1[3] = x14; - out1[4] = x17; - out1[5] = x19; - out1[6] = x21; - out1[7] = x22; - out1[8] = x25; - out1[9] = x27; - out1[10] = x29; - out1[11] = x30; - out1[12] = x33; - out1[13] = x35; - out1[14] = x37; - out1[15] = x38; - out1[16] = x41; - out1[17] = x43; - out1[18] = x45; - out1[19] = x46; - out1[20] = x49; - out1[21] = x51; - out1[22] = x53; - out1[23] = x54; - out1[24] = x57; - out1[25] = x59; - out1[26] = x61; - out1[27] = x60; + out1[4] = x16; + out1[5] = x18; + out1[6] = x20; + out1[7] = x21; + out1[8] = x23; + out1[9] = x25; + out1[10] = x27; + out1[11] = x28; + out1[12] = x30; + out1[13] = x32; + out1[14] = x34; + out1[15] = x35; + out1[16] = x37; + out1[17] = x39; + out1[18] = x41; + out1[19] = x42; + out1[20] = x44; + out1[21] = x46; + out1[22] = x48; + out1[23] = x49; + out1[24] = x51; + out1[25] = x53; + out1[26] = x55; + out1[27] = x54; } /* @@ -2752,23 +2746,17 @@ static void fiat_p224_from_bytes(uint32_t out1[7], const uint8_t arg1[28]) { uint32_t x34 = (x16 + (x15 + (x14 + x13))); uint32_t x35 = (x20 + (x19 + (x18 + x17))); uint32_t x36 = (x24 + (x23 + (x22 + x21))); - uint32_t x37 = (0x0 + x36); - uint32_t x38 = (x37 & UINT32_C(0xffffffff)); - uint32_t x39 = (0x0 + x35); - uint32_t x40 = (x39 & UINT32_C(0xffffffff)); - uint32_t x41 = (0x0 + x34); - uint32_t x42 = (x41 & UINT32_C(0xffffffff)); - uint32_t x43 = (0x0 + x33); - uint32_t x44 = (x43 & UINT32_C(0xffffffff)); - uint32_t x45 = (0x0 + x32); - uint32_t x46 = (x45 & UINT32_C(0xffffffff)); - uint32_t x47 = (0x0 + x31); + uint32_t x37 = (x36 & UINT32_C(0xffffffff)); + uint32_t x38 = (x35 & UINT32_C(0xffffffff)); + uint32_t x39 = (x34 & UINT32_C(0xffffffff)); + uint32_t x40 = (x33 & UINT32_C(0xffffffff)); + uint32_t x41 = (x32 & UINT32_C(0xffffffff)); out1[0] = x30; - out1[1] = x38; - out1[2] = x40; - out1[3] = x42; - out1[4] = x44; - out1[5] = x46; - out1[6] = x47; + out1[1] = x37; + out1[2] = x38; + out1[3] = x39; + out1[4] = x40; + out1[5] = x41; + out1[6] = x31; } @@ -1163,25 +1163,25 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { uint8_t x17 = (uint8_t)(x15 >> 8); uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff)); uint8_t x19 = (uint8_t)(x17 & UINT8_C(0xff)); - uint64_t x20 = (0x0 + x3); - uint64_t x21 = (x20 >> 8); - uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); - uint64_t x23 = (x21 >> 8); - uint8_t x24 = (uint8_t)(x21 & UINT8_C(0xff)); - uint64_t x25 = (x23 >> 8); - uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); - uint64_t x27 = (x25 >> 8); - uint8_t x28 = (uint8_t)(x25 & UINT8_C(0xff)); - uint64_t x29 = (x27 >> 8); - uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); - uint64_t x31 = (x29 >> 8); - uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); - uint8_t x33 = (uint8_t)(x31 >> 8); - uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); - uint8_t x35 = (uint8_t)(x33 & UINT8_C(0xff)); - uint64_t x36 = (0x0 + x2); - uint64_t x37 = (x36 >> 8); - uint8_t x38 = (uint8_t)(x36 & UINT8_C(0xff)); + uint64_t x20 = (x3 >> 8); + uint8_t x21 = (uint8_t)(x3 & UINT8_C(0xff)); + uint64_t x22 = (x20 >> 8); + uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff)); + uint64_t x24 = (x22 >> 8); + uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); + uint64_t x26 = (x24 >> 8); + uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); + uint64_t x28 = (x26 >> 8); + uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); + uint64_t x30 = (x28 >> 8); + uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); + uint8_t x32 = (uint8_t)(x30 >> 8); + uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); + uint8_t x34 = (uint8_t)(x32 & UINT8_C(0xff)); + uint64_t x35 = (x2 >> 8); + uint8_t x36 = (uint8_t)(x2 & UINT8_C(0xff)); + uint64_t x37 = (x35 >> 8); + uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff)); uint64_t x39 = (x37 >> 8); uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); uint64_t x41 = (x39 >> 8); @@ -1190,19 +1190,16 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); uint64_t x45 = (x43 >> 8); uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); - uint64_t x47 = (x45 >> 8); + uint8_t x47 = (uint8_t)(x45 >> 8); uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); - uint8_t x49 = (uint8_t)(x47 >> 8); - uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); - uint8_t x51 = (uint8_t)(x49 & UINT8_C(0xff)); - uint64_t x52 = (0x0 + x1); - uint64_t x53 = (x52 >> 8); - uint8_t x54 = (uint8_t)(x52 & UINT8_C(0xff)); - uint64_t x55 = (x53 >> 8); - uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff)); - uint8_t x57 = (uint8_t)(x55 >> 8); - uint8_t x58 = (uint8_t)(x55 & UINT8_C(0xff)); - uint8_t x59 = (uint8_t)(x57 & UINT8_C(0xff)); + uint8_t x49 = (uint8_t)(x47 & UINT8_C(0xff)); + uint64_t x50 = (x1 >> 8); + uint8_t x51 = (uint8_t)(x1 & UINT8_C(0xff)); + uint64_t x52 = (x50 >> 8); + uint8_t x53 = (uint8_t)(x50 & UINT8_C(0xff)); + uint8_t x54 = (uint8_t)(x52 >> 8); + uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); + uint8_t x56 = (uint8_t)(x54 & UINT8_C(0xff)); out1[0] = x6; out1[1] = x8; out1[2] = x10; @@ -1211,26 +1208,26 @@ static void fiat_p224_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { out1[5] = x16; out1[6] = x18; out1[7] = x19; - out1[8] = x22; - out1[9] = x24; - out1[10] = x26; - out1[11] = x28; - out1[12] = x30; - out1[13] = x32; - out1[14] = x34; - out1[15] = x35; - out1[16] = x38; - out1[17] = x40; - out1[18] = x42; - out1[19] = x44; - out1[20] = x46; - out1[21] = x48; - out1[22] = x50; - out1[23] = x51; - out1[24] = x54; - out1[25] = x56; - out1[26] = x58; - out1[27] = x59; + out1[8] = x21; + out1[9] = x23; + out1[10] = x25; + out1[11] = x27; + out1[12] = x29; + out1[13] = x31; + out1[14] = x33; + out1[15] = x34; + out1[16] = x36; + out1[17] = x38; + out1[18] = x40; + out1[19] = x42; + out1[20] = x44; + out1[21] = x46; + out1[22] = x48; + out1[23] = x49; + out1[24] = x51; + out1[25] = x53; + out1[26] = x55; + out1[27] = x56; out1[28] = 0x0; out1[29] = 0x0; out1[30] = 0x0; @@ -1274,17 +1271,14 @@ static void fiat_p224_from_bytes(uint64_t out1[4], const uint8_t arg1[32]) { uint8_t x28 = (arg1[0]); uint64_t x29 = (x28 + (x27 + (x26 + (x25 + (x24 + (x23 + (x22 + x21))))))); uint64_t x30 = (x29 & UINT64_C(0xffffffffffffffff)); - uint64_t x31 = (x4 + (x3 + (x2 + (x1 + (uint64_t)0x0)))); + uint64_t x31 = (x4 + (x3 + (x2 + x1))); uint64_t x32 = (x12 + (x11 + (x10 + (x9 + (x8 + (x7 + (x6 + x5))))))); uint64_t x33 = (x20 + (x19 + (x18 + (x17 + (x16 + (x15 + (x14 + x13))))))); - uint64_t x34 = (0x0 + x33); - uint64_t x35 = (x34 & UINT64_C(0xffffffffffffffff)); - uint64_t x36 = (0x0 + x32); - uint64_t x37 = (x36 & UINT64_C(0xffffffffffffffff)); - uint64_t x38 = (0x0 + x31); + uint64_t x34 = (x33 & UINT64_C(0xffffffffffffffff)); + uint64_t x35 = (x32 & UINT64_C(0xffffffffffffffff)); out1[0] = x30; - out1[1] = x35; - out1[2] = x37; - out1[3] = x38; + out1[1] = x34; + out1[2] = x35; + out1[3] = x31; } @@ -3072,93 +3072,86 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { uint8_t x13 = (uint8_t)(x11 >> 8); uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff)); uint8_t x15 = (uint8_t)(x13 & UINT8_C(0xff)); - uint32_t x16 = (0x0 + x7); - uint32_t x17 = (x16 >> 8); - uint8_t x18 = (uint8_t)(x16 & UINT8_C(0xff)); - uint32_t x19 = (x17 >> 8); - uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff)); - uint8_t x21 = (uint8_t)(x19 >> 8); - uint8_t x22 = (uint8_t)(x19 & UINT8_C(0xff)); - uint8_t x23 = (uint8_t)(x21 & UINT8_C(0xff)); - uint32_t x24 = (0x0 + x6); - uint32_t x25 = (x24 >> 8); - uint8_t x26 = (uint8_t)(x24 & UINT8_C(0xff)); - uint32_t x27 = (x25 >> 8); + uint32_t x16 = (x7 >> 8); + uint8_t x17 = (uint8_t)(x7 & UINT8_C(0xff)); + uint32_t x18 = (x16 >> 8); + uint8_t x19 = (uint8_t)(x16 & UINT8_C(0xff)); + uint8_t x20 = (uint8_t)(x18 >> 8); + uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff)); + uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); + uint32_t x23 = (x6 >> 8); + uint8_t x24 = (uint8_t)(x6 & UINT8_C(0xff)); + uint32_t x25 = (x23 >> 8); + uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); + uint8_t x27 = (uint8_t)(x25 >> 8); uint8_t x28 = (uint8_t)(x25 & UINT8_C(0xff)); - uint8_t x29 = (uint8_t)(x27 >> 8); - uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); - uint8_t x31 = (uint8_t)(x29 & UINT8_C(0xff)); - uint32_t x32 = (0x0 + x5); - uint32_t x33 = (x32 >> 8); - uint8_t x34 = (uint8_t)(x32 & UINT8_C(0xff)); - uint32_t x35 = (x33 >> 8); - uint8_t x36 = (uint8_t)(x33 & UINT8_C(0xff)); - uint8_t x37 = (uint8_t)(x35 >> 8); - uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff)); - uint8_t x39 = (uint8_t)(x37 & UINT8_C(0xff)); - uint32_t x40 = (0x0 + x4); - uint32_t x41 = (x40 >> 8); - uint8_t x42 = (uint8_t)(x40 & UINT8_C(0xff)); - uint32_t x43 = (x41 >> 8); - uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); - uint8_t x45 = (uint8_t)(x43 >> 8); - uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); - uint8_t x47 = (uint8_t)(x45 & UINT8_C(0xff)); - uint32_t x48 = (0x0 + x3); - uint32_t x49 = (x48 >> 8); + uint8_t x29 = (uint8_t)(x27 & UINT8_C(0xff)); + uint32_t x30 = (x5 >> 8); + uint8_t x31 = (uint8_t)(x5 & UINT8_C(0xff)); + uint32_t x32 = (x30 >> 8); + uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); + uint8_t x34 = (uint8_t)(x32 >> 8); + uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); + uint8_t x36 = (uint8_t)(x34 & UINT8_C(0xff)); + uint32_t x37 = (x4 >> 8); + uint8_t x38 = (uint8_t)(x4 & UINT8_C(0xff)); + uint32_t x39 = (x37 >> 8); + uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); + uint8_t x41 = (uint8_t)(x39 >> 8); + uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); + uint8_t x43 = (uint8_t)(x41 & UINT8_C(0xff)); + uint32_t x44 = (x3 >> 8); + uint8_t x45 = (uint8_t)(x3 & UINT8_C(0xff)); + uint32_t x46 = (x44 >> 8); + uint8_t x47 = (uint8_t)(x44 & UINT8_C(0xff)); + uint8_t x48 = (uint8_t)(x46 >> 8); + uint8_t x49 = (uint8_t)(x46 & UINT8_C(0xff)); uint8_t x50 = (uint8_t)(x48 & UINT8_C(0xff)); - uint32_t x51 = (x49 >> 8); - uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff)); - uint8_t x53 = (uint8_t)(x51 >> 8); + uint32_t x51 = (x2 >> 8); + uint8_t x52 = (uint8_t)(x2 & UINT8_C(0xff)); + uint32_t x53 = (x51 >> 8); uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff)); - uint8_t x55 = (uint8_t)(x53 & UINT8_C(0xff)); - uint32_t x56 = (0x0 + x2); - uint32_t x57 = (x56 >> 8); - uint8_t x58 = (uint8_t)(x56 & UINT8_C(0xff)); - uint32_t x59 = (x57 >> 8); - uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff)); - uint8_t x61 = (uint8_t)(x59 >> 8); - uint8_t x62 = (uint8_t)(x59 & UINT8_C(0xff)); - uint8_t x63 = (uint8_t)(x61 & UINT8_C(0xff)); - uint32_t x64 = (0x0 + x1); - uint32_t x65 = (x64 >> 8); - uint8_t x66 = (uint8_t)(x64 & UINT8_C(0xff)); - uint32_t x67 = (x65 >> 8); - uint8_t x68 = (uint8_t)(x65 & UINT8_C(0xff)); - uint8_t x69 = (uint8_t)(x67 >> 8); - uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff)); + uint8_t x55 = (uint8_t)(x53 >> 8); + uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff)); + uint8_t x57 = (uint8_t)(x55 & UINT8_C(0xff)); + uint32_t x58 = (x1 >> 8); + uint8_t x59 = (uint8_t)(x1 & UINT8_C(0xff)); + uint32_t x60 = (x58 >> 8); + uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); + uint8_t x62 = (uint8_t)(x60 >> 8); + uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); out1[0] = x10; out1[1] = x12; out1[2] = x14; out1[3] = x15; - out1[4] = x18; - out1[5] = x20; - out1[6] = x22; - out1[7] = x23; - out1[8] = x26; - out1[9] = x28; - out1[10] = x30; - out1[11] = x31; - out1[12] = x34; - out1[13] = x36; - out1[14] = x38; - out1[15] = x39; - out1[16] = x42; - out1[17] = x44; - out1[18] = x46; - out1[19] = x47; - out1[20] = x50; - out1[21] = x52; - out1[22] = x54; - out1[23] = x55; - out1[24] = x58; - out1[25] = x60; - out1[26] = x62; - out1[27] = x63; - out1[28] = x66; - out1[29] = x68; - out1[30] = x70; - out1[31] = x69; + out1[4] = x17; + out1[5] = x19; + out1[6] = x21; + out1[7] = x22; + out1[8] = x24; + out1[9] = x26; + out1[10] = x28; + out1[11] = x29; + out1[12] = x31; + out1[13] = x33; + out1[14] = x35; + out1[15] = x36; + out1[16] = x38; + out1[17] = x40; + out1[18] = x42; + out1[19] = x43; + out1[20] = x45; + out1[21] = x47; + out1[22] = x49; + out1[23] = x50; + out1[24] = x52; + out1[25] = x54; + out1[26] = x56; + out1[27] = x57; + out1[28] = x59; + out1[29] = x61; + out1[30] = x63; + out1[31] = x62; } /* @@ -3209,26 +3202,19 @@ static void fiat_p256_from_bytes(uint32_t out1[8], const uint8_t arg1[32]) { uint32_t x39 = (x20 + (x19 + (x18 + x17))); uint32_t x40 = (x24 + (x23 + (x22 + x21))); uint32_t x41 = (x28 + (x27 + (x26 + x25))); - uint32_t x42 = (0x0 + x41); - uint32_t x43 = (x42 & UINT32_C(0xffffffff)); - uint32_t x44 = (0x0 + x40); - uint32_t x45 = (x44 & UINT32_C(0xffffffff)); - uint32_t x46 = (0x0 + x39); - uint32_t x47 = (x46 & UINT32_C(0xffffffff)); - uint32_t x48 = (0x0 + x38); - uint32_t x49 = (x48 & UINT32_C(0xffffffff)); - uint32_t x50 = (0x0 + x37); - uint32_t x51 = (x50 & UINT32_C(0xffffffff)); - uint32_t x52 = (0x0 + x36); - uint32_t x53 = (x52 & UINT32_C(0xffffffff)); - uint32_t x54 = (0x0 + x35); + uint32_t x42 = (x41 & UINT32_C(0xffffffff)); + uint32_t x43 = (x40 & UINT32_C(0xffffffff)); + uint32_t x44 = (x39 & UINT32_C(0xffffffff)); + uint32_t x45 = (x38 & UINT32_C(0xffffffff)); + uint32_t x46 = (x37 & UINT32_C(0xffffffff)); + uint32_t x47 = (x36 & UINT32_C(0xffffffff)); out1[0] = x34; - out1[1] = x43; - out1[2] = x45; - out1[3] = x47; - out1[4] = x49; - out1[5] = x51; - out1[6] = x53; - out1[7] = x54; + out1[1] = x42; + out1[2] = x43; + out1[3] = x44; + out1[4] = x45; + out1[5] = x46; + out1[6] = x47; + out1[7] = x35; } @@ -1079,25 +1079,25 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { uint8_t x17 = (uint8_t)(x15 >> 8); uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff)); uint8_t x19 = (uint8_t)(x17 & UINT8_C(0xff)); - uint64_t x20 = (0x0 + x3); - uint64_t x21 = (x20 >> 8); - uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); - uint64_t x23 = (x21 >> 8); - uint8_t x24 = (uint8_t)(x21 & UINT8_C(0xff)); - uint64_t x25 = (x23 >> 8); - uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); - uint64_t x27 = (x25 >> 8); - uint8_t x28 = (uint8_t)(x25 & UINT8_C(0xff)); - uint64_t x29 = (x27 >> 8); - uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); - uint64_t x31 = (x29 >> 8); - uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); - uint8_t x33 = (uint8_t)(x31 >> 8); - uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); - uint8_t x35 = (uint8_t)(x33 & UINT8_C(0xff)); - uint64_t x36 = (0x0 + x2); - uint64_t x37 = (x36 >> 8); - uint8_t x38 = (uint8_t)(x36 & UINT8_C(0xff)); + uint64_t x20 = (x3 >> 8); + uint8_t x21 = (uint8_t)(x3 & UINT8_C(0xff)); + uint64_t x22 = (x20 >> 8); + uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff)); + uint64_t x24 = (x22 >> 8); + uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); + uint64_t x26 = (x24 >> 8); + uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); + uint64_t x28 = (x26 >> 8); + uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); + uint64_t x30 = (x28 >> 8); + uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); + uint8_t x32 = (uint8_t)(x30 >> 8); + uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); + uint8_t x34 = (uint8_t)(x32 & UINT8_C(0xff)); + uint64_t x35 = (x2 >> 8); + uint8_t x36 = (uint8_t)(x2 & UINT8_C(0xff)); + uint64_t x37 = (x35 >> 8); + uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff)); uint64_t x39 = (x37 >> 8); uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); uint64_t x41 = (x39 >> 8); @@ -1106,26 +1106,23 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); uint64_t x45 = (x43 >> 8); uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); - uint64_t x47 = (x45 >> 8); + uint8_t x47 = (uint8_t)(x45 >> 8); uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); - uint8_t x49 = (uint8_t)(x47 >> 8); - uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); - uint8_t x51 = (uint8_t)(x49 & UINT8_C(0xff)); - uint64_t x52 = (0x0 + x1); - uint64_t x53 = (x52 >> 8); - uint8_t x54 = (uint8_t)(x52 & UINT8_C(0xff)); - uint64_t x55 = (x53 >> 8); - uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff)); - uint64_t x57 = (x55 >> 8); - uint8_t x58 = (uint8_t)(x55 & UINT8_C(0xff)); - uint64_t x59 = (x57 >> 8); - uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff)); - uint64_t x61 = (x59 >> 8); - uint8_t x62 = (uint8_t)(x59 & UINT8_C(0xff)); - uint64_t x63 = (x61 >> 8); - uint8_t x64 = (uint8_t)(x61 & UINT8_C(0xff)); - uint8_t x65 = (uint8_t)(x63 >> 8); - uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff)); + uint8_t x49 = (uint8_t)(x47 & UINT8_C(0xff)); + uint64_t x50 = (x1 >> 8); + uint8_t x51 = (uint8_t)(x1 & UINT8_C(0xff)); + uint64_t x52 = (x50 >> 8); + uint8_t x53 = (uint8_t)(x50 & UINT8_C(0xff)); + uint64_t x54 = (x52 >> 8); + uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); + uint64_t x56 = (x54 >> 8); + uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff)); + uint64_t x58 = (x56 >> 8); + uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); + uint64_t x60 = (x58 >> 8); + uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); + uint8_t x62 = (uint8_t)(x60 >> 8); + uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); out1[0] = x6; out1[1] = x8; out1[2] = x10; @@ -1134,30 +1131,30 @@ static void fiat_p256_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { out1[5] = x16; out1[6] = x18; out1[7] = x19; - out1[8] = x22; - out1[9] = x24; - out1[10] = x26; - out1[11] = x28; - out1[12] = x30; - out1[13] = x32; - out1[14] = x34; - out1[15] = x35; - out1[16] = x38; - out1[17] = x40; - out1[18] = x42; - out1[19] = x44; - out1[20] = x46; - out1[21] = x48; - out1[22] = x50; - out1[23] = x51; - out1[24] = x54; - out1[25] = x56; - out1[26] = x58; - out1[27] = x60; - out1[28] = x62; - out1[29] = x64; - out1[30] = x66; - out1[31] = x65; + out1[8] = x21; + out1[9] = x23; + out1[10] = x25; + out1[11] = x27; + out1[12] = x29; + out1[13] = x31; + out1[14] = x33; + out1[15] = x34; + out1[16] = x36; + out1[17] = x38; + out1[18] = x40; + out1[19] = x42; + out1[20] = x44; + out1[21] = x46; + out1[22] = x48; + out1[23] = x49; + out1[24] = x51; + out1[25] = x53; + out1[26] = x55; + out1[27] = x57; + out1[28] = x59; + out1[29] = x61; + out1[30] = x63; + out1[31] = x62; } /* @@ -1204,14 +1201,11 @@ static void fiat_p256_from_bytes(uint64_t out1[4], const uint8_t arg1[32]) { uint64_t x35 = (x8 + (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + x1))))))); uint64_t x36 = (x16 + (x15 + (x14 + (x13 + (x12 + (x11 + (x10 + x9))))))); uint64_t x37 = (x24 + (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + x17))))))); - uint64_t x38 = (0x0 + x37); - uint64_t x39 = (x38 & UINT64_C(0xffffffffffffffff)); - uint64_t x40 = (0x0 + x36); - uint64_t x41 = (x40 & UINT64_C(0xffffffffffffffff)); - uint64_t x42 = (0x0 + x35); + uint64_t x38 = (x37 & UINT64_C(0xffffffffffffffff)); + uint64_t x39 = (x36 & UINT64_C(0xffffffffffffffff)); out1[0] = x34; - out1[1] = x39; - out1[2] = x41; - out1[3] = x42; + out1[1] = x38; + out1[2] = x39; + out1[3] = x35; } @@ -7265,141 +7265,130 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint32_t arg1[12]) { uint8_t x17 = (uint8_t)(x15 >> 8); uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff)); uint8_t x19 = (uint8_t)(x17 & UINT8_C(0xff)); - uint32_t x20 = (0x0 + x11); - uint32_t x21 = (x20 >> 8); - uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); - uint32_t x23 = (x21 >> 8); - uint8_t x24 = (uint8_t)(x21 & UINT8_C(0xff)); - uint8_t x25 = (uint8_t)(x23 >> 8); - uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); - uint8_t x27 = (uint8_t)(x25 & UINT8_C(0xff)); - uint32_t x28 = (0x0 + x10); - uint32_t x29 = (x28 >> 8); - uint8_t x30 = (uint8_t)(x28 & UINT8_C(0xff)); - uint32_t x31 = (x29 >> 8); + uint32_t x20 = (x11 >> 8); + uint8_t x21 = (uint8_t)(x11 & UINT8_C(0xff)); + uint32_t x22 = (x20 >> 8); + uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff)); + uint8_t x24 = (uint8_t)(x22 >> 8); + uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); + uint8_t x26 = (uint8_t)(x24 & UINT8_C(0xff)); + uint32_t x27 = (x10 >> 8); + uint8_t x28 = (uint8_t)(x10 & UINT8_C(0xff)); + uint32_t x29 = (x27 >> 8); + uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); + uint8_t x31 = (uint8_t)(x29 >> 8); uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); - uint8_t x33 = (uint8_t)(x31 >> 8); - uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); - uint8_t x35 = (uint8_t)(x33 & UINT8_C(0xff)); - uint32_t x36 = (0x0 + x9); - uint32_t x37 = (x36 >> 8); - uint8_t x38 = (uint8_t)(x36 & UINT8_C(0xff)); - uint32_t x39 = (x37 >> 8); - uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); - uint8_t x41 = (uint8_t)(x39 >> 8); - uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); - uint8_t x43 = (uint8_t)(x41 & UINT8_C(0xff)); - uint32_t x44 = (0x0 + x8); - uint32_t x45 = (x44 >> 8); - uint8_t x46 = (uint8_t)(x44 & UINT8_C(0xff)); - uint32_t x47 = (x45 >> 8); - uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); - uint8_t x49 = (uint8_t)(x47 >> 8); - uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); - uint8_t x51 = (uint8_t)(x49 & UINT8_C(0xff)); - uint32_t x52 = (0x0 + x7); - uint32_t x53 = (x52 >> 8); + uint8_t x33 = (uint8_t)(x31 & UINT8_C(0xff)); + uint32_t x34 = (x9 >> 8); + uint8_t x35 = (uint8_t)(x9 & UINT8_C(0xff)); + uint32_t x36 = (x34 >> 8); + uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff)); + uint8_t x38 = (uint8_t)(x36 >> 8); + uint8_t x39 = (uint8_t)(x36 & UINT8_C(0xff)); + uint8_t x40 = (uint8_t)(x38 & UINT8_C(0xff)); + uint32_t x41 = (x8 >> 8); + uint8_t x42 = (uint8_t)(x8 & UINT8_C(0xff)); + uint32_t x43 = (x41 >> 8); + uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); + uint8_t x45 = (uint8_t)(x43 >> 8); + uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); + uint8_t x47 = (uint8_t)(x45 & UINT8_C(0xff)); + uint32_t x48 = (x7 >> 8); + uint8_t x49 = (uint8_t)(x7 & UINT8_C(0xff)); + uint32_t x50 = (x48 >> 8); + uint8_t x51 = (uint8_t)(x48 & UINT8_C(0xff)); + uint8_t x52 = (uint8_t)(x50 >> 8); + uint8_t x53 = (uint8_t)(x50 & UINT8_C(0xff)); uint8_t x54 = (uint8_t)(x52 & UINT8_C(0xff)); - uint32_t x55 = (x53 >> 8); - uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff)); - uint8_t x57 = (uint8_t)(x55 >> 8); + uint32_t x55 = (x6 >> 8); + uint8_t x56 = (uint8_t)(x6 & UINT8_C(0xff)); + uint32_t x57 = (x55 >> 8); uint8_t x58 = (uint8_t)(x55 & UINT8_C(0xff)); - uint8_t x59 = (uint8_t)(x57 & UINT8_C(0xff)); - uint32_t x60 = (0x0 + x6); - uint32_t x61 = (x60 >> 8); - uint8_t x62 = (uint8_t)(x60 & UINT8_C(0xff)); - uint32_t x63 = (x61 >> 8); - uint8_t x64 = (uint8_t)(x61 & UINT8_C(0xff)); - uint8_t x65 = (uint8_t)(x63 >> 8); - uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff)); - uint8_t x67 = (uint8_t)(x65 & UINT8_C(0xff)); - uint32_t x68 = (0x0 + x5); - uint32_t x69 = (x68 >> 8); - uint8_t x70 = (uint8_t)(x68 & UINT8_C(0xff)); + uint8_t x59 = (uint8_t)(x57 >> 8); + uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff)); + uint8_t x61 = (uint8_t)(x59 & UINT8_C(0xff)); + uint32_t x62 = (x5 >> 8); + uint8_t x63 = (uint8_t)(x5 & UINT8_C(0xff)); + uint32_t x64 = (x62 >> 8); + uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff)); + uint8_t x66 = (uint8_t)(x64 >> 8); + uint8_t x67 = (uint8_t)(x64 & UINT8_C(0xff)); + uint8_t x68 = (uint8_t)(x66 & UINT8_C(0xff)); + uint32_t x69 = (x4 >> 8); + uint8_t x70 = (uint8_t)(x4 & UINT8_C(0xff)); uint32_t x71 = (x69 >> 8); uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff)); uint8_t x73 = (uint8_t)(x71 >> 8); uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff)); uint8_t x75 = (uint8_t)(x73 & UINT8_C(0xff)); - uint32_t x76 = (0x0 + x4); - uint32_t x77 = (x76 >> 8); - uint8_t x78 = (uint8_t)(x76 & UINT8_C(0xff)); - uint32_t x79 = (x77 >> 8); - uint8_t x80 = (uint8_t)(x77 & UINT8_C(0xff)); - uint8_t x81 = (uint8_t)(x79 >> 8); - uint8_t x82 = (uint8_t)(x79 & UINT8_C(0xff)); - uint8_t x83 = (uint8_t)(x81 & UINT8_C(0xff)); - uint32_t x84 = (0x0 + x3); - uint32_t x85 = (x84 >> 8); - uint8_t x86 = (uint8_t)(x84 & UINT8_C(0xff)); - uint32_t x87 = (x85 >> 8); + uint32_t x76 = (x3 >> 8); + uint8_t x77 = (uint8_t)(x3 & UINT8_C(0xff)); + uint32_t x78 = (x76 >> 8); + uint8_t x79 = (uint8_t)(x76 & UINT8_C(0xff)); + uint8_t x80 = (uint8_t)(x78 >> 8); + uint8_t x81 = (uint8_t)(x78 & UINT8_C(0xff)); + uint8_t x82 = (uint8_t)(x80 & UINT8_C(0xff)); + uint32_t x83 = (x2 >> 8); + uint8_t x84 = (uint8_t)(x2 & UINT8_C(0xff)); + uint32_t x85 = (x83 >> 8); + uint8_t x86 = (uint8_t)(x83 & UINT8_C(0xff)); + uint8_t x87 = (uint8_t)(x85 >> 8); uint8_t x88 = (uint8_t)(x85 & UINT8_C(0xff)); - uint8_t x89 = (uint8_t)(x87 >> 8); - uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff)); - uint8_t x91 = (uint8_t)(x89 & UINT8_C(0xff)); - uint32_t x92 = (0x0 + x2); - uint32_t x93 = (x92 >> 8); - uint8_t x94 = (uint8_t)(x92 & UINT8_C(0xff)); - uint32_t x95 = (x93 >> 8); - uint8_t x96 = (uint8_t)(x93 & UINT8_C(0xff)); - uint8_t x97 = (uint8_t)(x95 >> 8); - uint8_t x98 = (uint8_t)(x95 & UINT8_C(0xff)); - uint8_t x99 = (uint8_t)(x97 & UINT8_C(0xff)); - uint32_t x100 = (0x0 + x1); - uint32_t x101 = (x100 >> 8); - uint8_t x102 = (uint8_t)(x100 & UINT8_C(0xff)); - uint32_t x103 = (x101 >> 8); - uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff)); - uint8_t x105 = (uint8_t)(x103 >> 8); - uint8_t x106 = (uint8_t)(x103 & UINT8_C(0xff)); + uint8_t x89 = (uint8_t)(x87 & UINT8_C(0xff)); + uint32_t x90 = (x1 >> 8); + uint8_t x91 = (uint8_t)(x1 & UINT8_C(0xff)); + uint32_t x92 = (x90 >> 8); + uint8_t x93 = (uint8_t)(x90 & UINT8_C(0xff)); + uint8_t x94 = (uint8_t)(x92 >> 8); + uint8_t x95 = (uint8_t)(x92 & UINT8_C(0xff)); out1[0] = x14; out1[1] = x16; out1[2] = x18; out1[3] = x19; - out1[4] = x22; - out1[5] = x24; - out1[6] = x26; - out1[7] = x27; - out1[8] = x30; - out1[9] = x32; - out1[10] = x34; - out1[11] = x35; - out1[12] = x38; - out1[13] = x40; - out1[14] = x42; - out1[15] = x43; - out1[16] = x46; - out1[17] = x48; - out1[18] = x50; - out1[19] = x51; - out1[20] = x54; - out1[21] = x56; - out1[22] = x58; - out1[23] = x59; - out1[24] = x62; - out1[25] = x64; - out1[26] = x66; - out1[27] = x67; - out1[28] = x70; - out1[29] = x72; - out1[30] = x74; - out1[31] = x75; - out1[32] = x78; - out1[33] = x80; - out1[34] = x82; - out1[35] = x83; - out1[36] = x86; - out1[37] = x88; - out1[38] = x90; - out1[39] = x91; - out1[40] = x94; - out1[41] = x96; - out1[42] = x98; - out1[43] = x99; - out1[44] = x102; - out1[45] = x104; - out1[46] = x106; - out1[47] = x105; + out1[4] = x21; + out1[5] = x23; + out1[6] = x25; + out1[7] = x26; + out1[8] = x28; + out1[9] = x30; + out1[10] = x32; + out1[11] = x33; + out1[12] = x35; + out1[13] = x37; + out1[14] = x39; + out1[15] = x40; + out1[16] = x42; + out1[17] = x44; + out1[18] = x46; + out1[19] = x47; + out1[20] = x49; + out1[21] = x51; + out1[22] = x53; + out1[23] = x54; + out1[24] = x56; + out1[25] = x58; + out1[26] = x60; + out1[27] = x61; + out1[28] = x63; + out1[29] = x65; + out1[30] = x67; + out1[31] = x68; + out1[32] = x70; + out1[33] = x72; + out1[34] = x74; + out1[35] = x75; + out1[36] = x77; + out1[37] = x79; + out1[38] = x81; + out1[39] = x82; + out1[40] = x84; + out1[41] = x86; + out1[42] = x88; + out1[43] = x89; + out1[44] = x91; + out1[45] = x93; + out1[46] = x95; + out1[47] = x94; } /* @@ -7470,38 +7459,27 @@ static void fiat_p384_from_bytes(uint32_t out1[12], const uint8_t arg1[48]) { uint32_t x59 = (x36 + (x35 + (x34 + x33))); uint32_t x60 = (x40 + (x39 + (x38 + x37))); uint32_t x61 = (x44 + (x43 + (x42 + x41))); - uint32_t x62 = (0x0 + x61); - uint32_t x63 = (x62 & UINT32_C(0xffffffff)); - uint32_t x64 = (0x0 + x60); - uint32_t x65 = (x64 & UINT32_C(0xffffffff)); - uint32_t x66 = (0x0 + x59); - uint32_t x67 = (x66 & UINT32_C(0xffffffff)); - uint32_t x68 = (0x0 + x58); - uint32_t x69 = (x68 & UINT32_C(0xffffffff)); - uint32_t x70 = (0x0 + x57); - uint32_t x71 = (x70 & UINT32_C(0xffffffff)); - uint32_t x72 = (0x0 + x56); - uint32_t x73 = (x72 & UINT32_C(0xffffffff)); - uint32_t x74 = (0x0 + x55); - uint32_t x75 = (x74 & UINT32_C(0xffffffff)); - uint32_t x76 = (0x0 + x54); - uint32_t x77 = (x76 & UINT32_C(0xffffffff)); - uint32_t x78 = (0x0 + x53); - uint32_t x79 = (x78 & UINT32_C(0xffffffff)); - uint32_t x80 = (0x0 + x52); - uint32_t x81 = (x80 & UINT32_C(0xffffffff)); - uint32_t x82 = (0x0 + x51); + uint32_t x62 = (x61 & UINT32_C(0xffffffff)); + uint32_t x63 = (x60 & UINT32_C(0xffffffff)); + uint32_t x64 = (x59 & UINT32_C(0xffffffff)); + uint32_t x65 = (x58 & UINT32_C(0xffffffff)); + uint32_t x66 = (x57 & UINT32_C(0xffffffff)); + uint32_t x67 = (x56 & UINT32_C(0xffffffff)); + uint32_t x68 = (x55 & UINT32_C(0xffffffff)); + uint32_t x69 = (x54 & UINT32_C(0xffffffff)); + uint32_t x70 = (x53 & UINT32_C(0xffffffff)); + uint32_t x71 = (x52 & UINT32_C(0xffffffff)); out1[0] = x50; - out1[1] = x63; - out1[2] = x65; - out1[3] = x67; - out1[4] = x69; - out1[5] = x71; - out1[6] = x73; - out1[7] = x75; - out1[8] = x77; - out1[9] = x79; - out1[10] = x81; - out1[11] = x82; + out1[1] = x62; + out1[2] = x63; + out1[3] = x64; + out1[4] = x65; + out1[5] = x66; + out1[6] = x67; + out1[7] = x68; + out1[8] = x69; + out1[9] = x70; + out1[10] = x71; + out1[11] = x51; } @@ -2364,25 +2364,25 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) { uint8_t x19 = (uint8_t)(x17 >> 8); uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff)); uint8_t x21 = (uint8_t)(x19 & UINT8_C(0xff)); - uint64_t x22 = (0x0 + x5); - uint64_t x23 = (x22 >> 8); - uint8_t x24 = (uint8_t)(x22 & UINT8_C(0xff)); - uint64_t x25 = (x23 >> 8); - uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); - uint64_t x27 = (x25 >> 8); - uint8_t x28 = (uint8_t)(x25 & UINT8_C(0xff)); - uint64_t x29 = (x27 >> 8); - uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); - uint64_t x31 = (x29 >> 8); - uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); - uint64_t x33 = (x31 >> 8); - uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); - uint8_t x35 = (uint8_t)(x33 >> 8); - uint8_t x36 = (uint8_t)(x33 & UINT8_C(0xff)); - uint8_t x37 = (uint8_t)(x35 & UINT8_C(0xff)); - uint64_t x38 = (0x0 + x4); - uint64_t x39 = (x38 >> 8); - uint8_t x40 = (uint8_t)(x38 & UINT8_C(0xff)); + uint64_t x22 = (x5 >> 8); + uint8_t x23 = (uint8_t)(x5 & UINT8_C(0xff)); + uint64_t x24 = (x22 >> 8); + uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); + uint64_t x26 = (x24 >> 8); + uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); + uint64_t x28 = (x26 >> 8); + uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); + uint64_t x30 = (x28 >> 8); + uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); + uint64_t x32 = (x30 >> 8); + uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); + uint8_t x34 = (uint8_t)(x32 >> 8); + uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); + uint8_t x36 = (uint8_t)(x34 & UINT8_C(0xff)); + uint64_t x37 = (x4 >> 8); + uint8_t x38 = (uint8_t)(x4 & UINT8_C(0xff)); + uint64_t x39 = (x37 >> 8); + uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); uint64_t x41 = (x39 >> 8); uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); uint64_t x43 = (x41 >> 8); @@ -2391,58 +2391,53 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) { uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); uint64_t x47 = (x45 >> 8); uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); - uint64_t x49 = (x47 >> 8); + uint8_t x49 = (uint8_t)(x47 >> 8); uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); - uint8_t x51 = (uint8_t)(x49 >> 8); - uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff)); - uint8_t x53 = (uint8_t)(x51 & UINT8_C(0xff)); - uint64_t x54 = (0x0 + x3); - uint64_t x55 = (x54 >> 8); - uint8_t x56 = (uint8_t)(x54 & UINT8_C(0xff)); - uint64_t x57 = (x55 >> 8); - uint8_t x58 = (uint8_t)(x55 & UINT8_C(0xff)); - uint64_t x59 = (x57 >> 8); - uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff)); - uint64_t x61 = (x59 >> 8); - uint8_t x62 = (uint8_t)(x59 & UINT8_C(0xff)); - uint64_t x63 = (x61 >> 8); - uint8_t x64 = (uint8_t)(x61 & UINT8_C(0xff)); - uint64_t x65 = (x63 >> 8); - uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff)); - uint8_t x67 = (uint8_t)(x65 >> 8); - uint8_t x68 = (uint8_t)(x65 & UINT8_C(0xff)); - uint8_t x69 = (uint8_t)(x67 & UINT8_C(0xff)); - uint64_t x70 = (0x0 + x2); - uint64_t x71 = (x70 >> 8); - uint8_t x72 = (uint8_t)(x70 & UINT8_C(0xff)); + uint8_t x51 = (uint8_t)(x49 & UINT8_C(0xff)); + uint64_t x52 = (x3 >> 8); + uint8_t x53 = (uint8_t)(x3 & UINT8_C(0xff)); + uint64_t x54 = (x52 >> 8); + uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); + uint64_t x56 = (x54 >> 8); + uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff)); + uint64_t x58 = (x56 >> 8); + uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); + uint64_t x60 = (x58 >> 8); + uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); + uint64_t x62 = (x60 >> 8); + uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); + uint8_t x64 = (uint8_t)(x62 >> 8); + uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff)); + uint8_t x66 = (uint8_t)(x64 & UINT8_C(0xff)); + uint64_t x67 = (x2 >> 8); + uint8_t x68 = (uint8_t)(x2 & UINT8_C(0xff)); + uint64_t x69 = (x67 >> 8); + uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff)); + uint64_t x71 = (x69 >> 8); + uint8_t x72 = (uint8_t)(x69 & UINT8_C(0xff)); uint64_t x73 = (x71 >> 8); uint8_t x74 = (uint8_t)(x71 & UINT8_C(0xff)); uint64_t x75 = (x73 >> 8); uint8_t x76 = (uint8_t)(x73 & UINT8_C(0xff)); uint64_t x77 = (x75 >> 8); uint8_t x78 = (uint8_t)(x75 & UINT8_C(0xff)); - uint64_t x79 = (x77 >> 8); + uint8_t x79 = (uint8_t)(x77 >> 8); uint8_t x80 = (uint8_t)(x77 & UINT8_C(0xff)); - uint64_t x81 = (x79 >> 8); - uint8_t x82 = (uint8_t)(x79 & UINT8_C(0xff)); - uint8_t x83 = (uint8_t)(x81 >> 8); - uint8_t x84 = (uint8_t)(x81 & UINT8_C(0xff)); - uint8_t x85 = (uint8_t)(x83 & UINT8_C(0xff)); - uint64_t x86 = (0x0 + x1); - uint64_t x87 = (x86 >> 8); - uint8_t x88 = (uint8_t)(x86 & UINT8_C(0xff)); - uint64_t x89 = (x87 >> 8); - uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff)); - uint64_t x91 = (x89 >> 8); - uint8_t x92 = (uint8_t)(x89 & UINT8_C(0xff)); - uint64_t x93 = (x91 >> 8); - uint8_t x94 = (uint8_t)(x91 & UINT8_C(0xff)); - uint64_t x95 = (x93 >> 8); - uint8_t x96 = (uint8_t)(x93 & UINT8_C(0xff)); - uint64_t x97 = (x95 >> 8); - uint8_t x98 = (uint8_t)(x95 & UINT8_C(0xff)); - uint8_t x99 = (uint8_t)(x97 >> 8); - uint8_t x100 = (uint8_t)(x97 & UINT8_C(0xff)); + uint8_t x81 = (uint8_t)(x79 & UINT8_C(0xff)); + uint64_t x82 = (x1 >> 8); + uint8_t x83 = (uint8_t)(x1 & UINT8_C(0xff)); + uint64_t x84 = (x82 >> 8); + uint8_t x85 = (uint8_t)(x82 & UINT8_C(0xff)); + uint64_t x86 = (x84 >> 8); + uint8_t x87 = (uint8_t)(x84 & UINT8_C(0xff)); + uint64_t x88 = (x86 >> 8); + uint8_t x89 = (uint8_t)(x86 & UINT8_C(0xff)); + uint64_t x90 = (x88 >> 8); + uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff)); + uint64_t x92 = (x90 >> 8); + uint8_t x93 = (uint8_t)(x90 & UINT8_C(0xff)); + uint8_t x94 = (uint8_t)(x92 >> 8); + uint8_t x95 = (uint8_t)(x92 & UINT8_C(0xff)); out1[0] = x8; out1[1] = x10; out1[2] = x12; @@ -2451,46 +2446,46 @@ static void fiat_p384_to_bytes(uint8_t out1[48], const uint64_t arg1[6]) { out1[5] = x18; out1[6] = x20; out1[7] = x21; - out1[8] = x24; - out1[9] = x26; - out1[10] = x28; - out1[11] = x30; - out1[12] = x32; - out1[13] = x34; - out1[14] = x36; - out1[15] = x37; - out1[16] = x40; - out1[17] = x42; - out1[18] = x44; - out1[19] = x46; - out1[20] = x48; - out1[21] = x50; - out1[22] = x52; - out1[23] = x53; - out1[24] = x56; - out1[25] = x58; - out1[26] = x60; - out1[27] = x62; - out1[28] = x64; - out1[29] = x66; - out1[30] = x68; - out1[31] = x69; - out1[32] = x72; - out1[33] = x74; - out1[34] = x76; - out1[35] = x78; - out1[36] = x80; - out1[37] = x82; - out1[38] = x84; - out1[39] = x85; - out1[40] = x88; - out1[41] = x90; - out1[42] = x92; - out1[43] = x94; - out1[44] = x96; - out1[45] = x98; - out1[46] = x100; - out1[47] = x99; + out1[8] = x23; + out1[9] = x25; + out1[10] = x27; + out1[11] = x29; + out1[12] = x31; + out1[13] = x33; + out1[14] = x35; + out1[15] = x36; + out1[16] = x38; + out1[17] = x40; + out1[18] = x42; + out1[19] = x44; + out1[20] = x46; + out1[21] = x48; + out1[22] = x50; + out1[23] = x51; + out1[24] = x53; + out1[25] = x55; + out1[26] = x57; + out1[27] = x59; + out1[28] = x61; + out1[29] = x63; + out1[30] = x65; + out1[31] = x66; + out1[32] = x68; + out1[33] = x70; + out1[34] = x72; + out1[35] = x74; + out1[36] = x76; + out1[37] = x78; + out1[38] = x80; + out1[39] = x81; + out1[40] = x83; + out1[41] = x85; + out1[42] = x87; + out1[43] = x89; + out1[44] = x91; + out1[45] = x93; + out1[46] = x95; + out1[47] = x94; } /* @@ -2555,20 +2550,15 @@ static void fiat_p384_from_bytes(uint64_t out1[6], const uint8_t arg1[48]) { uint64_t x53 = (x24 + (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + x17))))))); uint64_t x54 = (x32 + (x31 + (x30 + (x29 + (x28 + (x27 + (x26 + x25))))))); uint64_t x55 = (x40 + (x39 + (x38 + (x37 + (x36 + (x35 + (x34 + x33))))))); - uint64_t x56 = (0x0 + x55); - uint64_t x57 = (x56 & UINT64_C(0xffffffffffffffff)); - uint64_t x58 = (0x0 + x54); - uint64_t x59 = (x58 & UINT64_C(0xffffffffffffffff)); - uint64_t x60 = (0x0 + x53); - uint64_t x61 = (x60 & UINT64_C(0xffffffffffffffff)); - uint64_t x62 = (0x0 + x52); - uint64_t x63 = (x62 & UINT64_C(0xffffffffffffffff)); - uint64_t x64 = (0x0 + x51); + uint64_t x56 = (x55 & UINT64_C(0xffffffffffffffff)); + uint64_t x57 = (x54 & UINT64_C(0xffffffffffffffff)); + uint64_t x58 = (x53 & UINT64_C(0xffffffffffffffff)); + uint64_t x59 = (x52 & UINT64_C(0xffffffffffffffff)); out1[0] = x50; - out1[1] = x57; - out1[2] = x59; - out1[3] = x61; - out1[4] = x63; - out1[5] = x64; + out1[1] = x56; + out1[2] = x57; + out1[3] = x58; + out1[4] = x59; + out1[5] = x51; } @@ -2960,25 +2960,25 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) { uint8_t x20 = (uint8_t)(x18 >> 8); uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff)); uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); - uint64_t x23 = (0x0 + x6); - uint64_t x24 = (x23 >> 8); - uint8_t x25 = (uint8_t)(x23 & UINT8_C(0xff)); - uint64_t x26 = (x24 >> 8); - uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); - uint64_t x28 = (x26 >> 8); - uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); - uint64_t x30 = (x28 >> 8); - uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); - uint64_t x32 = (x30 >> 8); - uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); - uint64_t x34 = (x32 >> 8); - uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); - uint8_t x36 = (uint8_t)(x34 >> 8); - uint8_t x37 = (uint8_t)(x34 & UINT8_C(0xff)); - uint8_t x38 = (uint8_t)(x36 & UINT8_C(0xff)); - uint64_t x39 = (0x0 + x5); - uint64_t x40 = (x39 >> 8); - uint8_t x41 = (uint8_t)(x39 & UINT8_C(0xff)); + uint64_t x23 = (x6 >> 8); + uint8_t x24 = (uint8_t)(x6 & UINT8_C(0xff)); + uint64_t x25 = (x23 >> 8); + uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); + uint64_t x27 = (x25 >> 8); + uint8_t x28 = (uint8_t)(x25 & UINT8_C(0xff)); + uint64_t x29 = (x27 >> 8); + uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); + uint64_t x31 = (x29 >> 8); + uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); + uint64_t x33 = (x31 >> 8); + uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); + uint8_t x35 = (uint8_t)(x33 >> 8); + uint8_t x36 = (uint8_t)(x33 & UINT8_C(0xff)); + uint8_t x37 = (uint8_t)(x35 & UINT8_C(0xff)); + uint64_t x38 = (x5 >> 8); + uint8_t x39 = (uint8_t)(x5 & UINT8_C(0xff)); + uint64_t x40 = (x38 >> 8); + uint8_t x41 = (uint8_t)(x38 & UINT8_C(0xff)); uint64_t x42 = (x40 >> 8); uint8_t x43 = (uint8_t)(x40 & UINT8_C(0xff)); uint64_t x44 = (x42 >> 8); @@ -2987,73 +2987,67 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) { uint8_t x47 = (uint8_t)(x44 & UINT8_C(0xff)); uint64_t x48 = (x46 >> 8); uint8_t x49 = (uint8_t)(x46 & UINT8_C(0xff)); - uint64_t x50 = (x48 >> 8); + uint8_t x50 = (uint8_t)(x48 >> 8); uint8_t x51 = (uint8_t)(x48 & UINT8_C(0xff)); - uint8_t x52 = (uint8_t)(x50 >> 8); - uint8_t x53 = (uint8_t)(x50 & UINT8_C(0xff)); - uint8_t x54 = (uint8_t)(x52 & UINT8_C(0xff)); - uint64_t x55 = (0x0 + x4); - uint64_t x56 = (x55 >> 8); - uint8_t x57 = (uint8_t)(x55 & UINT8_C(0xff)); - uint64_t x58 = (x56 >> 8); - uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); - uint64_t x60 = (x58 >> 8); - uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); - uint64_t x62 = (x60 >> 8); - uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); - uint64_t x64 = (x62 >> 8); - uint8_t x65 = (uint8_t)(x62 & UINT8_C(0xff)); - uint64_t x66 = (x64 >> 8); - uint8_t x67 = (uint8_t)(x64 & UINT8_C(0xff)); - uint8_t x68 = (uint8_t)(x66 >> 8); - uint8_t x69 = (uint8_t)(x66 & UINT8_C(0xff)); - uint8_t x70 = (uint8_t)(x68 & UINT8_C(0xff)); - uint64_t x71 = (0x0 + x3); - uint64_t x72 = (x71 >> 8); - uint8_t x73 = (uint8_t)(x71 & UINT8_C(0xff)); + uint8_t x52 = (uint8_t)(x50 & UINT8_C(0xff)); + uint64_t x53 = (x4 >> 8); + uint8_t x54 = (uint8_t)(x4 & UINT8_C(0xff)); + uint64_t x55 = (x53 >> 8); + uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff)); + uint64_t x57 = (x55 >> 8); + uint8_t x58 = (uint8_t)(x55 & UINT8_C(0xff)); + uint64_t x59 = (x57 >> 8); + uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff)); + uint64_t x61 = (x59 >> 8); + uint8_t x62 = (uint8_t)(x59 & UINT8_C(0xff)); + uint64_t x63 = (x61 >> 8); + uint8_t x64 = (uint8_t)(x61 & UINT8_C(0xff)); + uint8_t x65 = (uint8_t)(x63 >> 8); + uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff)); + uint8_t x67 = (uint8_t)(x65 & UINT8_C(0xff)); + uint64_t x68 = (x3 >> 8); + uint8_t x69 = (uint8_t)(x3 & UINT8_C(0xff)); + uint64_t x70 = (x68 >> 8); + uint8_t x71 = (uint8_t)(x68 & UINT8_C(0xff)); + uint64_t x72 = (x70 >> 8); + uint8_t x73 = (uint8_t)(x70 & UINT8_C(0xff)); uint64_t x74 = (x72 >> 8); uint8_t x75 = (uint8_t)(x72 & UINT8_C(0xff)); uint64_t x76 = (x74 >> 8); uint8_t x77 = (uint8_t)(x74 & UINT8_C(0xff)); uint64_t x78 = (x76 >> 8); uint8_t x79 = (uint8_t)(x76 & UINT8_C(0xff)); - uint64_t x80 = (x78 >> 8); + uint8_t x80 = (uint8_t)(x78 >> 8); uint8_t x81 = (uint8_t)(x78 & UINT8_C(0xff)); - uint64_t x82 = (x80 >> 8); - uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff)); - uint8_t x84 = (uint8_t)(x82 >> 8); - uint8_t x85 = (uint8_t)(x82 & UINT8_C(0xff)); - uint8_t x86 = (uint8_t)(x84 & UINT8_C(0xff)); - uint64_t x87 = (0x0 + x2); - uint64_t x88 = (x87 >> 8); - uint8_t x89 = (uint8_t)(x87 & UINT8_C(0xff)); - uint64_t x90 = (x88 >> 8); - uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff)); - uint64_t x92 = (x90 >> 8); - uint8_t x93 = (uint8_t)(x90 & UINT8_C(0xff)); - uint64_t x94 = (x92 >> 8); - uint8_t x95 = (uint8_t)(x92 & UINT8_C(0xff)); - uint64_t x96 = (x94 >> 8); - uint8_t x97 = (uint8_t)(x94 & UINT8_C(0xff)); - uint64_t x98 = (x96 >> 8); - uint8_t x99 = (uint8_t)(x96 & UINT8_C(0xff)); - uint8_t x100 = (uint8_t)(x98 >> 8); + uint8_t x82 = (uint8_t)(x80 & UINT8_C(0xff)); + uint64_t x83 = (x2 >> 8); + uint8_t x84 = (uint8_t)(x2 & UINT8_C(0xff)); + uint64_t x85 = (x83 >> 8); + uint8_t x86 = (uint8_t)(x83 & UINT8_C(0xff)); + uint64_t x87 = (x85 >> 8); + uint8_t x88 = (uint8_t)(x85 & UINT8_C(0xff)); + uint64_t x89 = (x87 >> 8); + uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff)); + uint64_t x91 = (x89 >> 8); + uint8_t x92 = (uint8_t)(x89 & UINT8_C(0xff)); + uint64_t x93 = (x91 >> 8); + uint8_t x94 = (uint8_t)(x91 & UINT8_C(0xff)); + uint8_t x95 = (uint8_t)(x93 >> 8); + uint8_t x96 = (uint8_t)(x93 & UINT8_C(0xff)); + uint8_t x97 = (uint8_t)(x95 & UINT8_C(0xff)); + uint64_t x98 = (x1 >> 8); + uint8_t x99 = (uint8_t)(x1 & UINT8_C(0xff)); + uint64_t x100 = (x98 >> 8); uint8_t x101 = (uint8_t)(x98 & UINT8_C(0xff)); - uint8_t x102 = (uint8_t)(x100 & UINT8_C(0xff)); - uint64_t x103 = (0x0 + x1); - uint64_t x104 = (x103 >> 8); - uint8_t x105 = (uint8_t)(x103 & UINT8_C(0xff)); + uint64_t x102 = (x100 >> 8); + uint8_t x103 = (uint8_t)(x100 & UINT8_C(0xff)); + uint64_t x104 = (x102 >> 8); + uint8_t x105 = (uint8_t)(x102 & UINT8_C(0xff)); uint64_t x106 = (x104 >> 8); uint8_t x107 = (uint8_t)(x104 & UINT8_C(0xff)); - uint64_t x108 = (x106 >> 8); + uint8_t x108 = (uint8_t)(x106 >> 8); uint8_t x109 = (uint8_t)(x106 & UINT8_C(0xff)); - uint64_t x110 = (x108 >> 8); - uint8_t x111 = (uint8_t)(x108 & UINT8_C(0xff)); - uint64_t x112 = (x110 >> 8); - uint8_t x113 = (uint8_t)(x110 & UINT8_C(0xff)); - uint8_t x114 = (uint8_t)(x112 >> 8); - uint8_t x115 = (uint8_t)(x112 & UINT8_C(0xff)); - uint8_t x116 = (uint8_t)(x114 & UINT8_C(0xff)); + uint8_t x110 = (uint8_t)(x108 & UINT8_C(0xff)); out1[0] = x9; out1[1] = x11; out1[2] = x13; @@ -3062,53 +3056,53 @@ static void fiat_p484_to_bytes(uint8_t out1[56], const uint64_t arg1[7]) { out1[5] = x19; out1[6] = x21; out1[7] = x22; - out1[8] = x25; - out1[9] = x27; - out1[10] = x29; - out1[11] = x31; - out1[12] = x33; - out1[13] = x35; - out1[14] = x37; - out1[15] = x38; - out1[16] = x41; - out1[17] = x43; - out1[18] = x45; - out1[19] = x47; - out1[20] = x49; - out1[21] = x51; - out1[22] = x53; - out1[23] = x54; - out1[24] = x57; - out1[25] = x59; - out1[26] = x61; - out1[27] = x63; - out1[28] = x65; - out1[29] = x67; - out1[30] = x69; - out1[31] = x70; - out1[32] = x73; - out1[33] = x75; - out1[34] = x77; - out1[35] = x79; - out1[36] = x81; - out1[37] = x83; - out1[38] = x85; - out1[39] = x86; - out1[40] = x89; - out1[41] = x91; - out1[42] = x93; - out1[43] = x95; - out1[44] = x97; - out1[45] = x99; - out1[46] = x101; - out1[47] = x102; - out1[48] = x105; - out1[49] = x107; - out1[50] = x109; - out1[51] = x111; - out1[52] = x113; - out1[53] = x115; - out1[54] = x116; + out1[8] = x24; + out1[9] = x26; + out1[10] = x28; + out1[11] = x30; + out1[12] = x32; + out1[13] = x34; + out1[14] = x36; + out1[15] = x37; + out1[16] = x39; + out1[17] = x41; + out1[18] = x43; + out1[19] = x45; + out1[20] = x47; + out1[21] = x49; + out1[22] = x51; + out1[23] = x52; + out1[24] = x54; + out1[25] = x56; + out1[26] = x58; + out1[27] = x60; + out1[28] = x62; + out1[29] = x64; + out1[30] = x66; + out1[31] = x67; + out1[32] = x69; + out1[33] = x71; + out1[34] = x73; + out1[35] = x75; + out1[36] = x77; + out1[37] = x79; + out1[38] = x81; + out1[39] = x82; + out1[40] = x84; + out1[41] = x86; + out1[42] = x88; + out1[43] = x90; + out1[44] = x92; + out1[45] = x94; + out1[46] = x96; + out1[47] = x97; + out1[48] = x99; + out1[49] = x101; + out1[50] = x103; + out1[51] = x105; + out1[52] = x107; + out1[53] = x109; + out1[54] = x110; out1[55] = 0x0; } @@ -3176,29 +3170,23 @@ static void fiat_p484_from_bytes(uint64_t out1[7], const uint8_t arg1[56]) { uint8_t x55 = (arg1[0]); uint64_t x56 = (x55 + (x54 + (x53 + (x52 + (x51 + (x50 + (x49 + x48))))))); uint64_t x57 = (x56 & UINT64_C(0xffffffffffffffff)); - uint64_t x58 = (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + (x1 + (uint64_t)0x0))))))); + uint64_t x58 = (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + x1)))))); uint64_t x59 = (x15 + (x14 + (x13 + (x12 + (x11 + (x10 + (x9 + x8))))))); uint64_t x60 = (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + (x17 + x16))))))); uint64_t x61 = (x31 + (x30 + (x29 + (x28 + (x27 + (x26 + (x25 + x24))))))); uint64_t x62 = (x39 + (x38 + (x37 + (x36 + (x35 + (x34 + (x33 + x32))))))); uint64_t x63 = (x47 + (x46 + (x45 + (x44 + (x43 + (x42 + (x41 + x40))))))); - uint64_t x64 = (0x0 + x63); - uint64_t x65 = (x64 & UINT64_C(0xffffffffffffffff)); - uint64_t x66 = (0x0 + x62); - uint64_t x67 = (x66 & UINT64_C(0xffffffffffffffff)); - uint64_t x68 = (0x0 + x61); - uint64_t x69 = (x68 & UINT64_C(0xffffffffffffffff)); - uint64_t x70 = (0x0 + x60); - uint64_t x71 = (x70 & UINT64_C(0xffffffffffffffff)); - uint64_t x72 = (0x0 + x59); - uint64_t x73 = (x72 & UINT64_C(0xffffffffffffffff)); - uint64_t x74 = (0x0 + x58); + uint64_t x64 = (x63 & UINT64_C(0xffffffffffffffff)); + uint64_t x65 = (x62 & UINT64_C(0xffffffffffffffff)); + uint64_t x66 = (x61 & UINT64_C(0xffffffffffffffff)); + uint64_t x67 = (x60 & UINT64_C(0xffffffffffffffff)); + uint64_t x68 = (x59 & UINT64_C(0xffffffffffffffff)); out1[0] = x57; - out1[1] = x65; - out1[2] = x67; - out1[3] = x69; - out1[4] = x71; - out1[5] = x73; - out1[6] = x74; + out1[1] = x64; + out1[2] = x65; + out1[3] = x66; + out1[4] = x67; + out1[5] = x68; + out1[6] = x58; } @@ -1201,100 +1201,98 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) { uint8_t x131 = (uint8_t)(x129 >> 8); uint8_t x132 = (uint8_t)(x129 & UINT8_C(0xff)); uint8_t x133 = (uint8_t)(x131 & UINT8_C(0xff)); - uint32_t x134 = (0x0 + x48); - uint32_t x135 = (x134 >> 8); - uint8_t x136 = (uint8_t)(x134 & UINT8_C(0xff)); - uint32_t x137 = (x135 >> 8); - uint8_t x138 = (uint8_t)(x135 & UINT8_C(0xff)); - uint8_t x139 = (uint8_t)(x137 >> 8); - uint8_t x140 = (uint8_t)(x137 & UINT8_C(0xff)); - uint64_t x141 = (x139 + x78); - uint32_t x142 = (uint32_t)(x141 >> 8); - uint8_t x143 = (uint8_t)(x141 & UINT8_C(0xff)); - uint32_t x144 = (x142 >> 8); - uint8_t x145 = (uint8_t)(x142 & UINT8_C(0xff)); - uint32_t x146 = (x144 >> 8); - uint8_t x147 = (uint8_t)(x144 & UINT8_C(0xff)); - uint8_t x148 = (uint8_t)(x146 >> 8); - uint8_t x149 = (uint8_t)(x146 & UINT8_C(0xff)); - uint64_t x150 = (x148 + x77); - uint32_t x151 = (uint32_t)(x150 >> 8); - uint8_t x152 = (uint8_t)(x150 & UINT8_C(0xff)); - uint32_t x153 = (x151 >> 8); - uint8_t x154 = (uint8_t)(x151 & UINT8_C(0xff)); - uint32_t x155 = (x153 >> 8); - uint8_t x156 = (uint8_t)(x153 & UINT8_C(0xff)); - uint8_t x157 = (uint8_t)(x155 >> 8); - uint8_t x158 = (uint8_t)(x155 & UINT8_C(0xff)); - uint64_t x159 = (x157 + x76); - uint32_t x160 = (uint32_t)(x159 >> 8); - uint8_t x161 = (uint8_t)(x159 & UINT8_C(0xff)); - uint32_t x162 = (x160 >> 8); - uint8_t x163 = (uint8_t)(x160 & UINT8_C(0xff)); - uint32_t x164 = (x162 >> 8); - uint8_t x165 = (uint8_t)(x162 & UINT8_C(0xff)); - uint8_t x166 = (uint8_t)(x164 >> 8); - uint8_t x167 = (uint8_t)(x164 & UINT8_C(0xff)); - uint64_t x168 = (x166 + x75); - uint32_t x169 = (uint32_t)(x168 >> 8); - uint8_t x170 = (uint8_t)(x168 & UINT8_C(0xff)); - uint32_t x171 = (x169 >> 8); - uint8_t x172 = (uint8_t)(x169 & UINT8_C(0xff)); - uint32_t x173 = (x171 >> 8); - uint8_t x174 = (uint8_t)(x171 & UINT8_C(0xff)); - uint8_t x175 = (uint8_t)(x173 >> 8); - uint8_t x176 = (uint8_t)(x173 & UINT8_C(0xff)); - uint32_t x177 = (x175 + x74); - uint32_t x178 = (x177 >> 8); - uint8_t x179 = (uint8_t)(x177 & UINT8_C(0xff)); - uint32_t x180 = (x178 >> 8); - uint8_t x181 = (uint8_t)(x178 & UINT8_C(0xff)); - uint8_t x182 = (uint8_t)(x180 >> 8); - uint8_t x183 = (uint8_t)(x180 & UINT8_C(0xff)); - uint8_t x184 = (uint8_t)(x182 & UINT8_C(0xff)); - uint32_t x185 = (0x0 + x60); - uint32_t x186 = (x185 >> 8); - uint8_t x187 = (uint8_t)(x185 & UINT8_C(0xff)); - uint32_t x188 = (x186 >> 8); + uint32_t x134 = (x48 >> 8); + uint8_t x135 = (uint8_t)(x48 & UINT8_C(0xff)); + uint32_t x136 = (x134 >> 8); + uint8_t x137 = (uint8_t)(x134 & UINT8_C(0xff)); + uint8_t x138 = (uint8_t)(x136 >> 8); + uint8_t x139 = (uint8_t)(x136 & UINT8_C(0xff)); + uint64_t x140 = (x138 + x78); + uint32_t x141 = (uint32_t)(x140 >> 8); + uint8_t x142 = (uint8_t)(x140 & UINT8_C(0xff)); + uint32_t x143 = (x141 >> 8); + uint8_t x144 = (uint8_t)(x141 & UINT8_C(0xff)); + uint32_t x145 = (x143 >> 8); + uint8_t x146 = (uint8_t)(x143 & UINT8_C(0xff)); + uint8_t x147 = (uint8_t)(x145 >> 8); + uint8_t x148 = (uint8_t)(x145 & UINT8_C(0xff)); + uint64_t x149 = (x147 + x77); + uint32_t x150 = (uint32_t)(x149 >> 8); + uint8_t x151 = (uint8_t)(x149 & UINT8_C(0xff)); + uint32_t x152 = (x150 >> 8); + uint8_t x153 = (uint8_t)(x150 & UINT8_C(0xff)); + uint32_t x154 = (x152 >> 8); + uint8_t x155 = (uint8_t)(x152 & UINT8_C(0xff)); + uint8_t x156 = (uint8_t)(x154 >> 8); + uint8_t x157 = (uint8_t)(x154 & UINT8_C(0xff)); + uint64_t x158 = (x156 + x76); + uint32_t x159 = (uint32_t)(x158 >> 8); + uint8_t x160 = (uint8_t)(x158 & UINT8_C(0xff)); + uint32_t x161 = (x159 >> 8); + uint8_t x162 = (uint8_t)(x159 & UINT8_C(0xff)); + uint32_t x163 = (x161 >> 8); + uint8_t x164 = (uint8_t)(x161 & UINT8_C(0xff)); + uint8_t x165 = (uint8_t)(x163 >> 8); + uint8_t x166 = (uint8_t)(x163 & UINT8_C(0xff)); + uint64_t x167 = (x165 + x75); + uint32_t x168 = (uint32_t)(x167 >> 8); + uint8_t x169 = (uint8_t)(x167 & UINT8_C(0xff)); + uint32_t x170 = (x168 >> 8); + uint8_t x171 = (uint8_t)(x168 & UINT8_C(0xff)); + uint32_t x172 = (x170 >> 8); + uint8_t x173 = (uint8_t)(x170 & UINT8_C(0xff)); + uint8_t x174 = (uint8_t)(x172 >> 8); + uint8_t x175 = (uint8_t)(x172 & UINT8_C(0xff)); + uint32_t x176 = (x174 + x74); + uint32_t x177 = (x176 >> 8); + uint8_t x178 = (uint8_t)(x176 & UINT8_C(0xff)); + uint32_t x179 = (x177 >> 8); + uint8_t x180 = (uint8_t)(x177 & UINT8_C(0xff)); + uint8_t x181 = (uint8_t)(x179 >> 8); + uint8_t x182 = (uint8_t)(x179 & UINT8_C(0xff)); + uint8_t x183 = (uint8_t)(x181 & UINT8_C(0xff)); + uint32_t x184 = (x60 >> 8); + uint8_t x185 = (uint8_t)(x60 & UINT8_C(0xff)); + uint32_t x186 = (x184 >> 8); + uint8_t x187 = (uint8_t)(x184 & UINT8_C(0xff)); + uint8_t x188 = (uint8_t)(x186 >> 8); uint8_t x189 = (uint8_t)(x186 & UINT8_C(0xff)); - uint8_t x190 = (uint8_t)(x188 >> 8); - uint8_t x191 = (uint8_t)(x188 & UINT8_C(0xff)); - uint64_t x192 = (x190 + x73); - uint32_t x193 = (uint32_t)(x192 >> 8); - uint8_t x194 = (uint8_t)(x192 & UINT8_C(0xff)); + uint64_t x190 = (x188 + x73); + uint32_t x191 = (uint32_t)(x190 >> 8); + uint8_t x192 = (uint8_t)(x190 & UINT8_C(0xff)); + uint32_t x193 = (x191 >> 8); + uint8_t x194 = (uint8_t)(x191 & UINT8_C(0xff)); uint32_t x195 = (x193 >> 8); uint8_t x196 = (uint8_t)(x193 & UINT8_C(0xff)); - uint32_t x197 = (x195 >> 8); + uint8_t x197 = (uint8_t)(x195 >> 8); uint8_t x198 = (uint8_t)(x195 & UINT8_C(0xff)); - uint8_t x199 = (uint8_t)(x197 >> 8); - uint8_t x200 = (uint8_t)(x197 & UINT8_C(0xff)); - uint64_t x201 = (x199 + x72); - uint32_t x202 = (uint32_t)(x201 >> 8); - uint8_t x203 = (uint8_t)(x201 & UINT8_C(0xff)); + uint64_t x199 = (x197 + x72); + uint32_t x200 = (uint32_t)(x199 >> 8); + uint8_t x201 = (uint8_t)(x199 & UINT8_C(0xff)); + uint32_t x202 = (x200 >> 8); + uint8_t x203 = (uint8_t)(x200 & UINT8_C(0xff)); uint32_t x204 = (x202 >> 8); uint8_t x205 = (uint8_t)(x202 & UINT8_C(0xff)); - uint32_t x206 = (x204 >> 8); + uint8_t x206 = (uint8_t)(x204 >> 8); uint8_t x207 = (uint8_t)(x204 & UINT8_C(0xff)); - uint8_t x208 = (uint8_t)(x206 >> 8); - uint8_t x209 = (uint8_t)(x206 & UINT8_C(0xff)); - uint64_t x210 = (x208 + x71); - uint32_t x211 = (uint32_t)(x210 >> 8); - uint8_t x212 = (uint8_t)(x210 & UINT8_C(0xff)); + uint64_t x208 = (x206 + x71); + uint32_t x209 = (uint32_t)(x208 >> 8); + uint8_t x210 = (uint8_t)(x208 & UINT8_C(0xff)); + uint32_t x211 = (x209 >> 8); + uint8_t x212 = (uint8_t)(x209 & UINT8_C(0xff)); uint32_t x213 = (x211 >> 8); uint8_t x214 = (uint8_t)(x211 & UINT8_C(0xff)); - uint32_t x215 = (x213 >> 8); + uint8_t x215 = (uint8_t)(x213 >> 8); uint8_t x216 = (uint8_t)(x213 & UINT8_C(0xff)); - uint8_t x217 = (uint8_t)(x215 >> 8); - uint8_t x218 = (uint8_t)(x215 & UINT8_C(0xff)); - uint64_t x219 = (x217 + x70); - uint32_t x220 = (uint32_t)(x219 >> 8); - uint8_t x221 = (uint8_t)(x219 & UINT8_C(0xff)); + uint64_t x217 = (x215 + x70); + uint32_t x218 = (uint32_t)(x217 >> 8); + uint8_t x219 = (uint8_t)(x217 & UINT8_C(0xff)); + uint32_t x220 = (x218 >> 8); + uint8_t x221 = (uint8_t)(x218 & UINT8_C(0xff)); uint32_t x222 = (x220 >> 8); uint8_t x223 = (uint8_t)(x220 & UINT8_C(0xff)); - uint32_t x224 = (x222 >> 8); + fiat_p521_uint1 x224 = (fiat_p521_uint1)(x222 >> 8); uint8_t x225 = (uint8_t)(x222 & UINT8_C(0xff)); - fiat_p521_uint1 x226 = (fiat_p521_uint1)(x224 >> 8); - uint8_t x227 = (uint8_t)(x224 & UINT8_C(0xff)); out1[0] = x85; out1[1] = x87; out1[2] = x89; @@ -1318,49 +1316,49 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) { out1[20] = x130; out1[21] = x132; out1[22] = x133; - out1[23] = x136; - out1[24] = x138; - out1[25] = x140; - out1[26] = x143; - out1[27] = x145; - out1[28] = x147; - out1[29] = x149; - out1[30] = x152; - out1[31] = x154; - out1[32] = x156; - out1[33] = x158; - out1[34] = x161; - out1[35] = x163; - out1[36] = x165; - out1[37] = x167; - out1[38] = x170; - out1[39] = x172; - out1[40] = x174; - out1[41] = x176; - out1[42] = x179; - out1[43] = x181; - out1[44] = x183; - out1[45] = x184; - out1[46] = x187; - out1[47] = x189; - out1[48] = x191; - out1[49] = x194; - out1[50] = x196; - out1[51] = x198; - out1[52] = x200; - out1[53] = x203; - out1[54] = x205; - out1[55] = x207; - out1[56] = x209; - out1[57] = x212; - out1[58] = x214; - out1[59] = x216; - out1[60] = x218; - out1[61] = x221; - out1[62] = x223; - out1[63] = x225; - out1[64] = x227; - out1[65] = x226; + out1[23] = x135; + out1[24] = x137; + out1[25] = x139; + out1[26] = x142; + out1[27] = x144; + out1[28] = x146; + out1[29] = x148; + out1[30] = x151; + out1[31] = x153; + out1[32] = x155; + out1[33] = x157; + out1[34] = x160; + out1[35] = x162; + out1[36] = x164; + out1[37] = x166; + out1[38] = x169; + out1[39] = x171; + out1[40] = x173; + out1[41] = x175; + out1[42] = x178; + out1[43] = x180; + out1[44] = x182; + out1[45] = x183; + out1[46] = x185; + out1[47] = x187; + out1[48] = x189; + out1[49] = x192; + out1[50] = x194; + out1[51] = x196; + out1[52] = x198; + out1[53] = x201; + out1[54] = x203; + out1[55] = x205; + out1[56] = x207; + out1[57] = x210; + out1[58] = x212; + out1[59] = x214; + out1[60] = x216; + out1[61] = x219; + out1[62] = x221; + out1[63] = x223; + out1[64] = x225; + out1[65] = x224; } /* @@ -1469,52 +1467,50 @@ static void fiat_p521_from_bytes(uint32_t out1[17], const uint8_t arg1[66]) { uint32_t x97 = (uint32_t)(x95 & UINT32_C(0x7fffffff)); uint32_t x98 = (x96 + x81); uint32_t x99 = (x98 & UINT32_C(0x3fffffff)); - uint32_t x100 = (0x0 + x80); - fiat_p521_uint1 x101 = (fiat_p521_uint1)(x100 >> 31); - uint32_t x102 = (x100 & UINT32_C(0x7fffffff)); - uint64_t x103 = (x101 + x79); - uint8_t x104 = (uint8_t)(x103 >> 31); - uint32_t x105 = (uint32_t)(x103 & UINT32_C(0x7fffffff)); - uint64_t x106 = (x104 + x78); - uint8_t x107 = (uint8_t)(x106 >> 30); - uint32_t x108 = (uint32_t)(x106 & UINT32_C(0x3fffffff)); - uint64_t x109 = (x107 + x77); - uint8_t x110 = (uint8_t)(x109 >> 31); - uint32_t x111 = (uint32_t)(x109 & UINT32_C(0x7fffffff)); - uint64_t x112 = (x110 + x76); - uint8_t x113 = (uint8_t)(x112 >> 31); - uint32_t x114 = (uint32_t)(x112 & UINT32_C(0x7fffffff)); - uint32_t x115 = (x113 + x75); - uint32_t x116 = (x115 & UINT32_C(0x3fffffff)); - uint32_t x117 = (0x0 + x74); - fiat_p521_uint1 x118 = (fiat_p521_uint1)(x117 >> 31); - uint32_t x119 = (x117 & UINT32_C(0x7fffffff)); - uint64_t x120 = (x118 + x73); - uint8_t x121 = (uint8_t)(x120 >> 31); - uint32_t x122 = (uint32_t)(x120 & UINT32_C(0x7fffffff)); - uint64_t x123 = (x121 + x72); - uint8_t x124 = (uint8_t)(x123 >> 30); - uint32_t x125 = (uint32_t)(x123 & UINT32_C(0x3fffffff)); - uint64_t x126 = (x124 + x71); - uint8_t x127 = (uint8_t)(x126 >> 31); - uint32_t x128 = (uint32_t)(x126 & UINT32_C(0x7fffffff)); - uint32_t x129 = (x127 + x70); + fiat_p521_uint1 x100 = (fiat_p521_uint1)(x80 >> 31); + uint32_t x101 = (x80 & UINT32_C(0x7fffffff)); + uint64_t x102 = (x100 + x79); + uint8_t x103 = (uint8_t)(x102 >> 31); + uint32_t x104 = (uint32_t)(x102 & UINT32_C(0x7fffffff)); + uint64_t x105 = (x103 + x78); + uint8_t x106 = (uint8_t)(x105 >> 30); + uint32_t x107 = (uint32_t)(x105 & UINT32_C(0x3fffffff)); + uint64_t x108 = (x106 + x77); + uint8_t x109 = (uint8_t)(x108 >> 31); + uint32_t x110 = (uint32_t)(x108 & UINT32_C(0x7fffffff)); + uint64_t x111 = (x109 + x76); + uint8_t x112 = (uint8_t)(x111 >> 31); + uint32_t x113 = (uint32_t)(x111 & UINT32_C(0x7fffffff)); + uint32_t x114 = (x112 + x75); + uint32_t x115 = (x114 & UINT32_C(0x3fffffff)); + fiat_p521_uint1 x116 = (fiat_p521_uint1)(x74 >> 31); + uint32_t x117 = (x74 & UINT32_C(0x7fffffff)); + uint64_t x118 = (x116 + x73); + uint8_t x119 = (uint8_t)(x118 >> 31); + uint32_t x120 = (uint32_t)(x118 & UINT32_C(0x7fffffff)); + uint64_t x121 = (x119 + x72); + uint8_t x122 = (uint8_t)(x121 >> 30); + uint32_t x123 = (uint32_t)(x121 & UINT32_C(0x3fffffff)); + uint64_t x124 = (x122 + x71); + uint8_t x125 = (uint8_t)(x124 >> 31); + uint32_t x126 = (uint32_t)(x124 & UINT32_C(0x7fffffff)); + uint32_t x127 = (x125 + x70); out1[0] = x69; out1[1] = x88; out1[2] = x91; out1[3] = x94; out1[4] = x97; out1[5] = x99; - out1[6] = x102; - out1[7] = x105; - out1[8] = x108; - out1[9] = x111; - out1[10] = x114; - out1[11] = x116; - out1[12] = x119; - out1[13] = x122; - out1[14] = x125; - out1[15] = x128; - out1[16] = x129; + out1[6] = x101; + out1[7] = x104; + out1[8] = x107; + out1[9] = x110; + out1[10] = x113; + out1[11] = x115; + out1[12] = x117; + out1[13] = x120; + out1[14] = x123; + out1[15] = x126; + out1[16] = x127; } @@ -647,70 +647,70 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) { uint8_t x101 = (uint8_t)(x99 >> 8); uint8_t x102 = (uint8_t)(x99 & UINT8_C(0xff)); uint8_t x103 = (uint8_t)(x101 & UINT8_C(0xff)); - uint64_t x104 = (0x0 + x28); - uint64_t x105 = (x104 >> 8); - uint8_t x106 = (uint8_t)(x104 & UINT8_C(0xff)); - uint64_t x107 = (x105 >> 8); - uint8_t x108 = (uint8_t)(x105 & UINT8_C(0xff)); - uint64_t x109 = (x107 >> 8); - uint8_t x110 = (uint8_t)(x107 & UINT8_C(0xff)); - uint64_t x111 = (x109 >> 8); - uint8_t x112 = (uint8_t)(x109 & UINT8_C(0xff)); - uint64_t x113 = (x111 >> 8); - uint8_t x114 = (uint8_t)(x111 & UINT8_C(0xff)); - uint64_t x115 = (x113 >> 8); - uint8_t x116 = (uint8_t)(x113 & UINT8_C(0xff)); - uint8_t x117 = (uint8_t)(x115 >> 8); - uint8_t x118 = (uint8_t)(x115 & UINT8_C(0xff)); - uint64_t x119 = (x117 + x40); - uint64_t x120 = (x119 >> 8); - uint8_t x121 = (uint8_t)(x119 & UINT8_C(0xff)); - uint64_t x122 = (x120 >> 8); - uint8_t x123 = (uint8_t)(x120 & UINT8_C(0xff)); - uint64_t x124 = (x122 >> 8); - uint8_t x125 = (uint8_t)(x122 & UINT8_C(0xff)); - uint64_t x126 = (x124 >> 8); - uint8_t x127 = (uint8_t)(x124 & UINT8_C(0xff)); - uint64_t x128 = (x126 >> 8); - uint8_t x129 = (uint8_t)(x126 & UINT8_C(0xff)); - uint64_t x130 = (x128 >> 8); - uint8_t x131 = (uint8_t)(x128 & UINT8_C(0xff)); - uint8_t x132 = (uint8_t)(x130 >> 8); - uint8_t x133 = (uint8_t)(x130 & UINT8_C(0xff)); - uint64_t x134 = (x132 + x39); - uint64_t x135 = (x134 >> 8); - uint8_t x136 = (uint8_t)(x134 & UINT8_C(0xff)); - uint64_t x137 = (x135 >> 8); - uint8_t x138 = (uint8_t)(x135 & UINT8_C(0xff)); - uint64_t x139 = (x137 >> 8); - uint8_t x140 = (uint8_t)(x137 & UINT8_C(0xff)); - uint64_t x141 = (x139 >> 8); - uint8_t x142 = (uint8_t)(x139 & UINT8_C(0xff)); - uint64_t x143 = (x141 >> 8); - uint8_t x144 = (uint8_t)(x141 & UINT8_C(0xff)); - uint64_t x145 = (x143 >> 8); - uint8_t x146 = (uint8_t)(x143 & UINT8_C(0xff)); - uint8_t x147 = (uint8_t)(x145 >> 8); - uint8_t x148 = (uint8_t)(x145 & UINT8_C(0xff)); - uint64_t x149 = (x147 + x38); - uint64_t x150 = (x149 >> 8); - uint8_t x151 = (uint8_t)(x149 & UINT8_C(0xff)); - uint64_t x152 = (x150 >> 8); - uint8_t x153 = (uint8_t)(x150 & UINT8_C(0xff)); - uint64_t x154 = (x152 >> 8); - uint8_t x155 = (uint8_t)(x152 & UINT8_C(0xff)); - uint64_t x156 = (x154 >> 8); - uint8_t x157 = (uint8_t)(x154 & UINT8_C(0xff)); - uint64_t x158 = (x156 >> 8); - uint8_t x159 = (uint8_t)(x156 & UINT8_C(0xff)); - uint64_t x160 = (x158 >> 8); - uint8_t x161 = (uint8_t)(x158 & UINT8_C(0xff)); - uint8_t x162 = (uint8_t)(x160 >> 8); - uint8_t x163 = (uint8_t)(x160 & UINT8_C(0xff)); - uint8_t x164 = (uint8_t)(x162 & UINT8_C(0xff)); - uint64_t x165 = (0x0 + x36); - uint64_t x166 = (x165 >> 8); - uint8_t x167 = (uint8_t)(x165 & UINT8_C(0xff)); + uint64_t x104 = (x28 >> 8); + uint8_t x105 = (uint8_t)(x28 & UINT8_C(0xff)); + uint64_t x106 = (x104 >> 8); + uint8_t x107 = (uint8_t)(x104 & UINT8_C(0xff)); + uint64_t x108 = (x106 >> 8); + uint8_t x109 = (uint8_t)(x106 & UINT8_C(0xff)); + uint64_t x110 = (x108 >> 8); + uint8_t x111 = (uint8_t)(x108 & UINT8_C(0xff)); + uint64_t x112 = (x110 >> 8); + uint8_t x113 = (uint8_t)(x110 & UINT8_C(0xff)); + uint64_t x114 = (x112 >> 8); + uint8_t x115 = (uint8_t)(x112 & UINT8_C(0xff)); + uint8_t x116 = (uint8_t)(x114 >> 8); + uint8_t x117 = (uint8_t)(x114 & UINT8_C(0xff)); + uint64_t x118 = (x116 + x40); + uint64_t x119 = (x118 >> 8); + uint8_t x120 = (uint8_t)(x118 & UINT8_C(0xff)); + uint64_t x121 = (x119 >> 8); + uint8_t x122 = (uint8_t)(x119 & UINT8_C(0xff)); + uint64_t x123 = (x121 >> 8); + uint8_t x124 = (uint8_t)(x121 & UINT8_C(0xff)); + uint64_t x125 = (x123 >> 8); + uint8_t x126 = (uint8_t)(x123 & UINT8_C(0xff)); + uint64_t x127 = (x125 >> 8); + uint8_t x128 = (uint8_t)(x125 & UINT8_C(0xff)); + uint64_t x129 = (x127 >> 8); + uint8_t x130 = (uint8_t)(x127 & UINT8_C(0xff)); + uint8_t x131 = (uint8_t)(x129 >> 8); + uint8_t x132 = (uint8_t)(x129 & UINT8_C(0xff)); + uint64_t x133 = (x131 + x39); + uint64_t x134 = (x133 >> 8); + uint8_t x135 = (uint8_t)(x133 & UINT8_C(0xff)); + uint64_t x136 = (x134 >> 8); + uint8_t x137 = (uint8_t)(x134 & UINT8_C(0xff)); + uint64_t x138 = (x136 >> 8); + uint8_t x139 = (uint8_t)(x136 & UINT8_C(0xff)); + uint64_t x140 = (x138 >> 8); + uint8_t x141 = (uint8_t)(x138 & UINT8_C(0xff)); + uint64_t x142 = (x140 >> 8); + uint8_t x143 = (uint8_t)(x140 & UINT8_C(0xff)); + uint64_t x144 = (x142 >> 8); + uint8_t x145 = (uint8_t)(x142 & UINT8_C(0xff)); + uint8_t x146 = (uint8_t)(x144 >> 8); + uint8_t x147 = (uint8_t)(x144 & UINT8_C(0xff)); + uint64_t x148 = (x146 + x38); + uint64_t x149 = (x148 >> 8); + uint8_t x150 = (uint8_t)(x148 & UINT8_C(0xff)); + uint64_t x151 = (x149 >> 8); + uint8_t x152 = (uint8_t)(x149 & UINT8_C(0xff)); + uint64_t x153 = (x151 >> 8); + uint8_t x154 = (uint8_t)(x151 & UINT8_C(0xff)); + uint64_t x155 = (x153 >> 8); + uint8_t x156 = (uint8_t)(x153 & UINT8_C(0xff)); + uint64_t x157 = (x155 >> 8); + uint8_t x158 = (uint8_t)(x155 & UINT8_C(0xff)); + uint64_t x159 = (x157 >> 8); + uint8_t x160 = (uint8_t)(x157 & UINT8_C(0xff)); + uint8_t x161 = (uint8_t)(x159 >> 8); + uint8_t x162 = (uint8_t)(x159 & UINT8_C(0xff)); + uint8_t x163 = (uint8_t)(x161 & UINT8_C(0xff)); + uint64_t x164 = (x36 >> 8); + uint8_t x165 = (uint8_t)(x36 & UINT8_C(0xff)); + uint64_t x166 = (x164 >> 8); + uint8_t x167 = (uint8_t)(x164 & UINT8_C(0xff)); uint64_t x168 = (x166 >> 8); uint8_t x169 = (uint8_t)(x166 & UINT8_C(0xff)); uint64_t x170 = (x168 >> 8); @@ -719,10 +719,8 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) { uint8_t x173 = (uint8_t)(x170 & UINT8_C(0xff)); uint64_t x174 = (x172 >> 8); uint8_t x175 = (uint8_t)(x172 & UINT8_C(0xff)); - uint64_t x176 = (x174 >> 8); + fiat_p521_uint1 x176 = (fiat_p521_uint1)(x174 >> 8); uint8_t x177 = (uint8_t)(x174 & UINT8_C(0xff)); - fiat_p521_uint1 x178 = (fiat_p521_uint1)(x176 >> 8); - uint8_t x179 = (uint8_t)(x176 & UINT8_C(0xff)); out1[0] = x45; out1[1] = x47; out1[2] = x49; @@ -752,43 +750,43 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) { out1[26] = x100; out1[27] = x102; out1[28] = x103; - out1[29] = x106; - out1[30] = x108; - out1[31] = x110; - out1[32] = x112; - out1[33] = x114; - out1[34] = x116; - out1[35] = x118; - out1[36] = x121; - out1[37] = x123; - out1[38] = x125; - out1[39] = x127; - out1[40] = x129; - out1[41] = x131; - out1[42] = x133; - out1[43] = x136; - out1[44] = x138; - out1[45] = x140; - out1[46] = x142; - out1[47] = x144; - out1[48] = x146; - out1[49] = x148; - out1[50] = x151; - out1[51] = x153; - out1[52] = x155; - out1[53] = x157; - out1[54] = x159; - out1[55] = x161; - out1[56] = x163; - out1[57] = x164; - out1[58] = x167; - out1[59] = x169; - out1[60] = x171; - out1[61] = x173; - out1[62] = x175; - out1[63] = x177; - out1[64] = x179; - out1[65] = x178; + out1[29] = x105; + out1[30] = x107; + out1[31] = x109; + out1[32] = x111; + out1[33] = x113; + out1[34] = x115; + out1[35] = x117; + out1[36] = x120; + out1[37] = x122; + out1[38] = x124; + out1[39] = x126; + out1[40] = x128; + out1[41] = x130; + out1[42] = x132; + out1[43] = x135; + out1[44] = x137; + out1[45] = x139; + out1[46] = x141; + out1[47] = x143; + out1[48] = x145; + out1[49] = x147; + out1[50] = x150; + out1[51] = x152; + out1[52] = x154; + out1[53] = x156; + out1[54] = x158; + out1[55] = x160; + out1[56] = x162; + out1[57] = x163; + out1[58] = x165; + out1[59] = x167; + out1[60] = x169; + out1[61] = x171; + out1[62] = x173; + out1[63] = x175; + out1[64] = x177; + out1[65] = x176; } /* @@ -883,26 +881,24 @@ static void fiat_p521_from_bytes(uint64_t out1[9], const uint8_t arg1[66]) { uint64_t x83 = (x81 & UINT64_C(0x3ffffffffffffff)); uint64_t x84 = (x82 + x75); uint64_t x85 = (x84 & UINT64_C(0x3ffffffffffffff)); - uint64_t x86 = (0x0 + x74); - uint8_t x87 = (uint8_t)(x86 >> 58); - uint64_t x88 = (x86 & UINT64_C(0x3ffffffffffffff)); - uint64_t x89 = (x87 + x73); - uint8_t x90 = (uint8_t)(x89 >> 58); - uint64_t x91 = (x89 & UINT64_C(0x3ffffffffffffff)); - uint64_t x92 = (x90 + x72); - uint8_t x93 = (uint8_t)(x92 >> 58); - uint64_t x94 = (x92 & UINT64_C(0x3ffffffffffffff)); - uint64_t x95 = (x93 + x71); - uint64_t x96 = (x95 & UINT64_C(0x3ffffffffffffff)); - uint64_t x97 = (0x0 + x70); + uint8_t x86 = (uint8_t)(x74 >> 58); + uint64_t x87 = (x74 & UINT64_C(0x3ffffffffffffff)); + uint64_t x88 = (x86 + x73); + uint8_t x89 = (uint8_t)(x88 >> 58); + uint64_t x90 = (x88 & UINT64_C(0x3ffffffffffffff)); + uint64_t x91 = (x89 + x72); + uint8_t x92 = (uint8_t)(x91 >> 58); + uint64_t x93 = (x91 & UINT64_C(0x3ffffffffffffff)); + uint64_t x94 = (x92 + x71); + uint64_t x95 = (x94 & UINT64_C(0x3ffffffffffffff)); out1[0] = x69; out1[1] = x80; out1[2] = x83; out1[3] = x85; - out1[4] = x88; - out1[5] = x91; - out1[6] = x94; - out1[7] = x96; - out1[8] = x97; + out1[4] = x87; + out1[5] = x90; + out1[6] = x93; + out1[7] = x95; + out1[8] = x70; } diff --git a/secp256k1_32.c b/secp256k1_32.c index a4015f134..ec19bd1a9 100644 --- a/secp256k1_32.c +++ b/secp256k1_32.c @@ -3846,93 +3846,86 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint32_t arg1[8]) { uint8_t x13 = (uint8_t)(x11 >> 8); uint8_t x14 = (uint8_t)(x11 & UINT8_C(0xff)); uint8_t x15 = (uint8_t)(x13 & UINT8_C(0xff)); - uint32_t x16 = (0x0 + x7); - uint32_t x17 = (x16 >> 8); - uint8_t x18 = (uint8_t)(x16 & UINT8_C(0xff)); - uint32_t x19 = (x17 >> 8); - uint8_t x20 = (uint8_t)(x17 & UINT8_C(0xff)); - uint8_t x21 = (uint8_t)(x19 >> 8); - uint8_t x22 = (uint8_t)(x19 & UINT8_C(0xff)); - uint8_t x23 = (uint8_t)(x21 & UINT8_C(0xff)); - uint32_t x24 = (0x0 + x6); - uint32_t x25 = (x24 >> 8); - uint8_t x26 = (uint8_t)(x24 & UINT8_C(0xff)); - uint32_t x27 = (x25 >> 8); + uint32_t x16 = (x7 >> 8); + uint8_t x17 = (uint8_t)(x7 & UINT8_C(0xff)); + uint32_t x18 = (x16 >> 8); + uint8_t x19 = (uint8_t)(x16 & UINT8_C(0xff)); + uint8_t x20 = (uint8_t)(x18 >> 8); + uint8_t x21 = (uint8_t)(x18 & UINT8_C(0xff)); + uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); + uint32_t x23 = (x6 >> 8); + uint8_t x24 = (uint8_t)(x6 & UINT8_C(0xff)); + uint32_t x25 = (x23 >> 8); + uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); + uint8_t x27 = (uint8_t)(x25 >> 8); uint8_t x28 = (uint8_t)(x25 & UINT8_C(0xff)); - uint8_t x29 = (uint8_t)(x27 >> 8); - uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); - uint8_t x31 = (uint8_t)(x29 & UINT8_C(0xff)); - uint32_t x32 = (0x0 + x5); - uint32_t x33 = (x32 >> 8); - uint8_t x34 = (uint8_t)(x32 & UINT8_C(0xff)); - uint32_t x35 = (x33 >> 8); - uint8_t x36 = (uint8_t)(x33 & UINT8_C(0xff)); - uint8_t x37 = (uint8_t)(x35 >> 8); - uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff)); - uint8_t x39 = (uint8_t)(x37 & UINT8_C(0xff)); - uint32_t x40 = (0x0 + x4); - uint32_t x41 = (x40 >> 8); - uint8_t x42 = (uint8_t)(x40 & UINT8_C(0xff)); - uint32_t x43 = (x41 >> 8); - uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); - uint8_t x45 = (uint8_t)(x43 >> 8); - uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); - uint8_t x47 = (uint8_t)(x45 & UINT8_C(0xff)); - uint32_t x48 = (0x0 + x3); - uint32_t x49 = (x48 >> 8); + uint8_t x29 = (uint8_t)(x27 & UINT8_C(0xff)); + uint32_t x30 = (x5 >> 8); + uint8_t x31 = (uint8_t)(x5 & UINT8_C(0xff)); + uint32_t x32 = (x30 >> 8); + uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); + uint8_t x34 = (uint8_t)(x32 >> 8); + uint8_t x35 = (uint8_t)(x32 & UINT8_C(0xff)); + uint8_t x36 = (uint8_t)(x34 & UINT8_C(0xff)); + uint32_t x37 = (x4 >> 8); + uint8_t x38 = (uint8_t)(x4 & UINT8_C(0xff)); + uint32_t x39 = (x37 >> 8); + uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); + uint8_t x41 = (uint8_t)(x39 >> 8); + uint8_t x42 = (uint8_t)(x39 & UINT8_C(0xff)); + uint8_t x43 = (uint8_t)(x41 & UINT8_C(0xff)); + uint32_t x44 = (x3 >> 8); + uint8_t x45 = (uint8_t)(x3 & UINT8_C(0xff)); + uint32_t x46 = (x44 >> 8); + uint8_t x47 = (uint8_t)(x44 & UINT8_C(0xff)); + uint8_t x48 = (uint8_t)(x46 >> 8); + uint8_t x49 = (uint8_t)(x46 & UINT8_C(0xff)); uint8_t x50 = (uint8_t)(x48 & UINT8_C(0xff)); - uint32_t x51 = (x49 >> 8); - uint8_t x52 = (uint8_t)(x49 & UINT8_C(0xff)); - uint8_t x53 = (uint8_t)(x51 >> 8); + uint32_t x51 = (x2 >> 8); + uint8_t x52 = (uint8_t)(x2 & UINT8_C(0xff)); + uint32_t x53 = (x51 >> 8); uint8_t x54 = (uint8_t)(x51 & UINT8_C(0xff)); - uint8_t x55 = (uint8_t)(x53 & UINT8_C(0xff)); - uint32_t x56 = (0x0 + x2); - uint32_t x57 = (x56 >> 8); - uint8_t x58 = (uint8_t)(x56 & UINT8_C(0xff)); - uint32_t x59 = (x57 >> 8); - uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff)); - uint8_t x61 = (uint8_t)(x59 >> 8); - uint8_t x62 = (uint8_t)(x59 & UINT8_C(0xff)); - uint8_t x63 = (uint8_t)(x61 & UINT8_C(0xff)); - uint32_t x64 = (0x0 + x1); - uint32_t x65 = (x64 >> 8); - uint8_t x66 = (uint8_t)(x64 & UINT8_C(0xff)); - uint32_t x67 = (x65 >> 8); - uint8_t x68 = (uint8_t)(x65 & UINT8_C(0xff)); - uint8_t x69 = (uint8_t)(x67 >> 8); - uint8_t x70 = (uint8_t)(x67 & UINT8_C(0xff)); + uint8_t x55 = (uint8_t)(x53 >> 8); + uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff)); + uint8_t x57 = (uint8_t)(x55 & UINT8_C(0xff)); + uint32_t x58 = (x1 >> 8); + uint8_t x59 = (uint8_t)(x1 & UINT8_C(0xff)); + uint32_t x60 = (x58 >> 8); + uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); + uint8_t x62 = (uint8_t)(x60 >> 8); + uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); out1[0] = x10; out1[1] = x12; out1[2] = x14; out1[3] = x15; - out1[4] = x18; - out1[5] = x20; - out1[6] = x22; - out1[7] = x23; - out1[8] = x26; - out1[9] = x28; - out1[10] = x30; - out1[11] = x31; - out1[12] = x34; - out1[13] = x36; - out1[14] = x38; - out1[15] = x39; - out1[16] = x42; - out1[17] = x44; - out1[18] = x46; - out1[19] = x47; - out1[20] = x50; - out1[21] = x52; - out1[22] = x54; - out1[23] = x55; - out1[24] = x58; - out1[25] = x60; - out1[26] = x62; - out1[27] = x63; - out1[28] = x66; - out1[29] = x68; - out1[30] = x70; - out1[31] = x69; + out1[4] = x17; + out1[5] = x19; + out1[6] = x21; + out1[7] = x22; + out1[8] = x24; + out1[9] = x26; + out1[10] = x28; + out1[11] = x29; + out1[12] = x31; + out1[13] = x33; + out1[14] = x35; + out1[15] = x36; + out1[16] = x38; + out1[17] = x40; + out1[18] = x42; + out1[19] = x43; + out1[20] = x45; + out1[21] = x47; + out1[22] = x49; + out1[23] = x50; + out1[24] = x52; + out1[25] = x54; + out1[26] = x56; + out1[27] = x57; + out1[28] = x59; + out1[29] = x61; + out1[30] = x63; + out1[31] = x62; } /* @@ -3983,26 +3976,19 @@ static void fiat_secp256k1_from_bytes(uint32_t out1[8], const uint8_t arg1[32]) uint32_t x39 = (x20 + (x19 + (x18 + x17))); uint32_t x40 = (x24 + (x23 + (x22 + x21))); uint32_t x41 = (x28 + (x27 + (x26 + x25))); - uint32_t x42 = (0x0 + x41); - uint32_t x43 = (x42 & UINT32_C(0xffffffff)); - uint32_t x44 = (0x0 + x40); - uint32_t x45 = (x44 & UINT32_C(0xffffffff)); - uint32_t x46 = (0x0 + x39); - uint32_t x47 = (x46 & UINT32_C(0xffffffff)); - uint32_t x48 = (0x0 + x38); - uint32_t x49 = (x48 & UINT32_C(0xffffffff)); - uint32_t x50 = (0x0 + x37); - uint32_t x51 = (x50 & UINT32_C(0xffffffff)); - uint32_t x52 = (0x0 + x36); - uint32_t x53 = (x52 & UINT32_C(0xffffffff)); - uint32_t x54 = (0x0 + x35); + uint32_t x42 = (x41 & UINT32_C(0xffffffff)); + uint32_t x43 = (x40 & UINT32_C(0xffffffff)); + uint32_t x44 = (x39 & UINT32_C(0xffffffff)); + uint32_t x45 = (x38 & UINT32_C(0xffffffff)); + uint32_t x46 = (x37 & UINT32_C(0xffffffff)); + uint32_t x47 = (x36 & UINT32_C(0xffffffff)); out1[0] = x34; - out1[1] = x43; - out1[2] = x45; - out1[3] = x47; - out1[4] = x49; - out1[5] = x51; - out1[6] = x53; - out1[7] = x54; + out1[1] = x42; + out1[2] = x43; + out1[3] = x44; + out1[4] = x45; + out1[5] = x46; + out1[6] = x47; + out1[7] = x35; } diff --git a/secp256k1_64.c b/secp256k1_64.c index a80485a4f..0481fab65 100644 --- a/secp256k1_64.c +++ b/secp256k1_64.c @@ -1256,25 +1256,25 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { uint8_t x17 = (uint8_t)(x15 >> 8); uint8_t x18 = (uint8_t)(x15 & UINT8_C(0xff)); uint8_t x19 = (uint8_t)(x17 & UINT8_C(0xff)); - uint64_t x20 = (0x0 + x3); - uint64_t x21 = (x20 >> 8); - uint8_t x22 = (uint8_t)(x20 & UINT8_C(0xff)); - uint64_t x23 = (x21 >> 8); - uint8_t x24 = (uint8_t)(x21 & UINT8_C(0xff)); - uint64_t x25 = (x23 >> 8); - uint8_t x26 = (uint8_t)(x23 & UINT8_C(0xff)); - uint64_t x27 = (x25 >> 8); - uint8_t x28 = (uint8_t)(x25 & UINT8_C(0xff)); - uint64_t x29 = (x27 >> 8); - uint8_t x30 = (uint8_t)(x27 & UINT8_C(0xff)); - uint64_t x31 = (x29 >> 8); - uint8_t x32 = (uint8_t)(x29 & UINT8_C(0xff)); - uint8_t x33 = (uint8_t)(x31 >> 8); - uint8_t x34 = (uint8_t)(x31 & UINT8_C(0xff)); - uint8_t x35 = (uint8_t)(x33 & UINT8_C(0xff)); - uint64_t x36 = (0x0 + x2); - uint64_t x37 = (x36 >> 8); - uint8_t x38 = (uint8_t)(x36 & UINT8_C(0xff)); + uint64_t x20 = (x3 >> 8); + uint8_t x21 = (uint8_t)(x3 & UINT8_C(0xff)); + uint64_t x22 = (x20 >> 8); + uint8_t x23 = (uint8_t)(x20 & UINT8_C(0xff)); + uint64_t x24 = (x22 >> 8); + uint8_t x25 = (uint8_t)(x22 & UINT8_C(0xff)); + uint64_t x26 = (x24 >> 8); + uint8_t x27 = (uint8_t)(x24 & UINT8_C(0xff)); + uint64_t x28 = (x26 >> 8); + uint8_t x29 = (uint8_t)(x26 & UINT8_C(0xff)); + uint64_t x30 = (x28 >> 8); + uint8_t x31 = (uint8_t)(x28 & UINT8_C(0xff)); + uint8_t x32 = (uint8_t)(x30 >> 8); + uint8_t x33 = (uint8_t)(x30 & UINT8_C(0xff)); + uint8_t x34 = (uint8_t)(x32 & UINT8_C(0xff)); + uint64_t x35 = (x2 >> 8); + uint8_t x36 = (uint8_t)(x2 & UINT8_C(0xff)); + uint64_t x37 = (x35 >> 8); + uint8_t x38 = (uint8_t)(x35 & UINT8_C(0xff)); uint64_t x39 = (x37 >> 8); uint8_t x40 = (uint8_t)(x37 & UINT8_C(0xff)); uint64_t x41 = (x39 >> 8); @@ -1283,26 +1283,23 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { uint8_t x44 = (uint8_t)(x41 & UINT8_C(0xff)); uint64_t x45 = (x43 >> 8); uint8_t x46 = (uint8_t)(x43 & UINT8_C(0xff)); - uint64_t x47 = (x45 >> 8); + uint8_t x47 = (uint8_t)(x45 >> 8); uint8_t x48 = (uint8_t)(x45 & UINT8_C(0xff)); - uint8_t x49 = (uint8_t)(x47 >> 8); - uint8_t x50 = (uint8_t)(x47 & UINT8_C(0xff)); - uint8_t x51 = (uint8_t)(x49 & UINT8_C(0xff)); - uint64_t x52 = (0x0 + x1); - uint64_t x53 = (x52 >> 8); - uint8_t x54 = (uint8_t)(x52 & UINT8_C(0xff)); - uint64_t x55 = (x53 >> 8); - uint8_t x56 = (uint8_t)(x53 & UINT8_C(0xff)); - uint64_t x57 = (x55 >> 8); - uint8_t x58 = (uint8_t)(x55 & UINT8_C(0xff)); - uint64_t x59 = (x57 >> 8); - uint8_t x60 = (uint8_t)(x57 & UINT8_C(0xff)); - uint64_t x61 = (x59 >> 8); - uint8_t x62 = (uint8_t)(x59 & UINT8_C(0xff)); - uint64_t x63 = (x61 >> 8); - uint8_t x64 = (uint8_t)(x61 & UINT8_C(0xff)); - uint8_t x65 = (uint8_t)(x63 >> 8); - uint8_t x66 = (uint8_t)(x63 & UINT8_C(0xff)); + uint8_t x49 = (uint8_t)(x47 & UINT8_C(0xff)); + uint64_t x50 = (x1 >> 8); + uint8_t x51 = (uint8_t)(x1 & UINT8_C(0xff)); + uint64_t x52 = (x50 >> 8); + uint8_t x53 = (uint8_t)(x50 & UINT8_C(0xff)); + uint64_t x54 = (x52 >> 8); + uint8_t x55 = (uint8_t)(x52 & UINT8_C(0xff)); + uint64_t x56 = (x54 >> 8); + uint8_t x57 = (uint8_t)(x54 & UINT8_C(0xff)); + uint64_t x58 = (x56 >> 8); + uint8_t x59 = (uint8_t)(x56 & UINT8_C(0xff)); + uint64_t x60 = (x58 >> 8); + uint8_t x61 = (uint8_t)(x58 & UINT8_C(0xff)); + uint8_t x62 = (uint8_t)(x60 >> 8); + uint8_t x63 = (uint8_t)(x60 & UINT8_C(0xff)); out1[0] = x6; out1[1] = x8; out1[2] = x10; @@ -1311,30 +1308,30 @@ static void fiat_secp256k1_to_bytes(uint8_t out1[32], const uint64_t arg1[4]) { out1[5] = x16; out1[6] = x18; out1[7] = x19; - out1[8] = x22; - out1[9] = x24; - out1[10] = x26; - out1[11] = x28; - out1[12] = x30; - out1[13] = x32; - out1[14] = x34; - out1[15] = x35; - out1[16] = x38; - out1[17] = x40; - out1[18] = x42; - out1[19] = x44; - out1[20] = x46; - out1[21] = x48; - out1[22] = x50; - out1[23] = x51; - out1[24] = x54; - out1[25] = x56; - out1[26] = x58; - out1[27] = x60; - out1[28] = x62; - out1[29] = x64; - out1[30] = x66; - out1[31] = x65; + out1[8] = x21; + out1[9] = x23; + out1[10] = x25; + out1[11] = x27; + out1[12] = x29; + out1[13] = x31; + out1[14] = x33; + out1[15] = x34; + out1[16] = x36; + out1[17] = x38; + out1[18] = x40; + out1[19] = x42; + out1[20] = x44; + out1[21] = x46; + out1[22] = x48; + out1[23] = x49; + out1[24] = x51; + out1[25] = x53; + out1[26] = x55; + out1[27] = x57; + out1[28] = x59; + out1[29] = x61; + out1[30] = x63; + out1[31] = x62; } /* @@ -1381,14 +1378,11 @@ static void fiat_secp256k1_from_bytes(uint64_t out1[4], const uint8_t arg1[32]) uint64_t x35 = (x8 + (x7 + (x6 + (x5 + (x4 + (x3 + (x2 + x1))))))); uint64_t x36 = (x16 + (x15 + (x14 + (x13 + (x12 + (x11 + (x10 + x9))))))); uint64_t x37 = (x24 + (x23 + (x22 + (x21 + (x20 + (x19 + (x18 + x17))))))); - uint64_t x38 = (0x0 + x37); - uint64_t x39 = (x38 & UINT64_C(0xffffffffffffffff)); - uint64_t x40 = (0x0 + x36); - uint64_t x41 = (x40 & UINT64_C(0xffffffffffffffff)); - uint64_t x42 = (0x0 + x35); + uint64_t x38 = (x37 & UINT64_C(0xffffffffffffffff)); + uint64_t x39 = (x36 & UINT64_C(0xffffffffffffffff)); out1[0] = x34; - out1[1] = x39; - out1[2] = x41; - out1[3] = x42; + out1[1] = x38; + out1[2] = x39; + out1[3] = x35; } diff --git a/src/Rewriter.v b/src/Rewriter.v index 8bbf13173..fb14b31f0 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -1793,6 +1793,13 @@ Module Compilers. ; make_rewriteo (??') (fun r v => ##(lower r) when lower r =? upper r) ; make_rewriteo + (#?ℤ +' ??') + (fun rp z rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? ZRange.normalize rp)%zrange) + ; make_rewriteo + (??' +' #?ℤ ) + (fun rp rv v z => cst rv v when (z =? 0) && (ZRange.normalize rv <=? ZRange.normalize rp)%zrange) + + ; make_rewriteo (#?ℤ - (-'??')) (fun z rnv rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) ; make_rewriteo (#?ℤ - ?? ) (fun z v => -v when z =? 0) diff --git a/src/arith_with_casts_rewrite_head.out b/src/arith_with_casts_rewrite_head.out index 053110d89..a179fff11 100644 --- a/src/arith_with_casts_rewrite_head.out +++ b/src/arith_with_casts_rewrite_head.out @@ -950,6 +950,126 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | None => None end | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t1 idc1) x2) => + args <- invert_bind_args idc1 Raw.ident.Z_cast; + args0 <- invert_bind_args idc0 Raw.ident.Literal; + _ <- invert_bind_args idc Raw.ident.Z_add; + match + pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype + ((projT1 args0) -> s1)%ptype option (fun x3 : option => x3) + with + | Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + ((projT1 args0) -> s1)%ptype + then + xv <- ident.unify pattern.ident.Literal ##(projT2 args0); + v <- type.try_make_transport_cps s1 ℤ; + fv <- (x3 <- (if + ((let (x3, _) := xv in x3) =? 0) && + (ZRange.normalize args <=? + ZRange.normalize range)%zrange + then + Some + (#(Z_cast args)%expr @ + v (Compile.reflect x2))%expr_pat + else None); + Some (Base x3)); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) (@expr.App _ _ _ s1 _ ($_)%expr _) | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) + (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _) | @expr.App _ _ _ s + _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) + (@expr.App _ _ _ s1 _ (_ @ _)%expr_pat _) | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) + (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) => None + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) #(_)%expr_pat | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) ($_)%expr | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) (@expr.Abs _ _ _ _ _ _) | @expr.App _ + _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Ident _ _ _ t0 idc0)) (@expr.LetIn _ _ _ _ _ _ _) => None + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) + (@expr.Ident _ _ _ t1 idc1) => + args <- invert_bind_args idc1 Raw.ident.Literal; + args0 <- invert_bind_args idc0 Raw.ident.Z_cast; + _ <- invert_bind_args idc Raw.ident.Z_add; + match + pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype + (s1 -> (projT1 args))%ptype option (fun x3 : option => x3) + with + | Some (_, _)%zrange => + if + type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype + (s1 -> (projT1 args))%ptype + then + v <- type.try_make_transport_cps s1 ℤ; + xv <- ident.unify pattern.ident.Literal ##(projT2 args); + fv <- (x3 <- (if + ((let (x3, _) := xv in x3) =? 0) && + (ZRange.normalize args0 <=? + ZRange.normalize range)%zrange + then + Some + (#(Z_cast args0)%expr @ + v (Compile.reflect x2))%expr_pat + else None); + Some (Base x3)); + Some (fv0 <-- fv; + Base fv0)%under_lets + else None + | None => None + end + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) ($_)%expr | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) + (@expr.Abs _ _ _ _ _ _) | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) + (_ @ _)%expr_pat | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t0 idc0) x2)) + (@expr.LetIn _ _ _ _ _ _ _) => None + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ ($_)%expr _)) _ | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.Abs _ _ _ _ _ _) _)) _ | @expr.App _ _ + _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (_ @ _)%expr_pat _)) _ | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _)) _ => None + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) ($_)%expr) _ | + @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.Abs _ _ _ _ _ _)) _ | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) + (@expr.LetIn _ _ _ _ _ _ _)) _ => None + | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t idc) x2) x1) x0 => _ <- invert_bind_args idc Raw.ident.Z_add_with_carry; @@ -985,8 +1105,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.App _ _ _ s1 _ (@expr.LetIn _ _ _ _ _ _ _) _) _) _ => None - | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(_)%expr_pat _) _ | - @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App + | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => None |