Skip to content

Commit

Permalink
Constant-propogate 0+x and x+0 after bounds
Browse files Browse the repository at this point in the history 
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%
  • Loading branch information
@JasonGross
JasonGross committed Jan 16, 2019
1 parent cadf213 commit c07d388
Show file tree
Hide file tree
Showing 14 changed files with 1,266 additions and 1,252 deletions.
136 changes: 67 additions & 69 deletions curve25519_32.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
}

/*
Expand Down Expand Up @@ -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;
}

158 changes: 73 additions & 85 deletions p224_32.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

/*
Expand Down Expand Up @@ -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;
}

Loading

0 comments on commit c07d388

Please sign in to comment.