|
| 1 | +/* Cross-check of the carry-less multiply implementations in clmul.c. |
| 2 | + * |
| 3 | + * `HexGF2/SPEC/hex-gf2.md` requires that tests exercise each compiled wrapper |
| 4 | + * path, not merely whichever one the host happens to select. A build picks its |
| 5 | + * path with preprocessor guards, so a single build can only ever run one of |
| 6 | + * them; `scripts/ci/check_clmul_paths.sh` therefore compiles this twice, once |
| 7 | + * plain and once with the flags that enable an intrinsic, and this program |
| 8 | + * reports which path it got. |
| 9 | + * |
| 10 | + * When an intrinsic is compiled it is compared against the portable reference |
| 11 | + * on every vector, which is the divergence the SPEC is worried about. When it |
| 12 | + * is not, the portable path is still checked against known-answer vectors, so |
| 13 | + * a plain build is not vacuous. |
| 14 | + * |
| 15 | + * The Lean side of the same obligation is `conformance/HexGF2/CrossCheck.lean`, |
| 16 | + * which compares the extern against `Hex.pureClmul` over a pseudorandom stream. |
| 17 | + */ |
| 18 | +#include <stdint.h> |
| 19 | +#include <stdio.h> |
| 20 | + |
| 21 | +void hex_clmul_portable(uint64_t a, uint64_t b, uint64_t* hi, uint64_t* lo); |
| 22 | +int hex_clmul_uses_intrinsic(void); |
| 23 | +#if defined(HEX_CLMUL_SELFTEST_EXPECT_INTRINSIC) |
| 24 | +void hex_clmul_intrinsic(uint64_t a, uint64_t b, uint64_t* hi, uint64_t* lo); |
| 25 | +#endif |
| 26 | + |
| 27 | +/* Known answers, computed independently of this C code: the first three are |
| 28 | + hand-derived, the rest come from `Hex.pureClmul` evaluated in Lean. */ |
| 29 | +struct known { uint64_t a, b, hi, lo; }; |
| 30 | +static const struct known KNOWN[] = { |
| 31 | + { 0u, 0u, 0u, 0u }, |
| 32 | + { 1u, 1u, 0u, 1u }, |
| 33 | + { 2u, 2u, 0u, 4u }, |
| 34 | + { 3u, 3u, 0u, 5u }, |
| 35 | + { 0xFFu, 0xFFu, 0u, 0x5555u }, |
| 36 | + { 0x8000000000000000ull, 2u, 1u, 0u }, |
| 37 | + { 0x8000000000000000ull, 0x8000000000000000ull, 0x4000000000000000ull, 0u }, |
| 38 | +}; |
| 39 | + |
| 40 | +/* Deterministic MMIX linear congruential generator, the same one the Lean |
| 41 | + cross-check uses, so the two halves sweep comparable input shapes. */ |
| 42 | +static uint64_t next(uint64_t* state) { |
| 43 | + *state = *state * 6364136223846793005ull + 1442695040888963407ull; |
| 44 | + return *state; |
| 45 | +} |
| 46 | + |
| 47 | +int main(void) { |
| 48 | + int intrinsic = hex_clmul_uses_intrinsic(); |
| 49 | + printf("clmul self-test: intrinsic path %s\n", |
| 50 | + intrinsic ? "compiled" : "not compiled (portable fallback)"); |
| 51 | + |
| 52 | +#if defined(HEX_CLMUL_SELFTEST_EXPECT_INTRINSIC) |
| 53 | + if (!intrinsic) { |
| 54 | + fprintf(stderr, |
| 55 | + "clmul self-test: expected an intrinsic build, but the guards " |
| 56 | + "selected the portable path; the flags did not take effect\n"); |
| 57 | + return 2; |
| 58 | + } |
| 59 | +#endif |
| 60 | + |
| 61 | + for (unsigned i = 0; i < sizeof(KNOWN) / sizeof(KNOWN[0]); ++i) { |
| 62 | + uint64_t hi, lo; |
| 63 | + hex_clmul_portable(KNOWN[i].a, KNOWN[i].b, &hi, &lo); |
| 64 | + if (hi != KNOWN[i].hi || lo != KNOWN[i].lo) { |
| 65 | + fprintf(stderr, |
| 66 | + "clmul self-test: portable disagrees with known answer at " |
| 67 | + "vector %u: got (%llx, %llx), want (%llx, %llx)\n", |
| 68 | + i, (unsigned long long)hi, (unsigned long long)lo, |
| 69 | + (unsigned long long)KNOWN[i].hi, |
| 70 | + (unsigned long long)KNOWN[i].lo); |
| 71 | + return 1; |
| 72 | + } |
| 73 | + } |
| 74 | + |
| 75 | +#if defined(HEX_CLMUL_SELFTEST_EXPECT_INTRINSIC) |
| 76 | + uint64_t state = 0x243F6A8885A308D3ull; |
| 77 | + for (unsigned i = 0; i < 100000u; ++i) { |
| 78 | + uint64_t a = next(&state); |
| 79 | + uint64_t b = next(&state); |
| 80 | + uint64_t phi, plo, ihi, ilo; |
| 81 | + hex_clmul_portable(a, b, &phi, &plo); |
| 82 | + hex_clmul_intrinsic(a, b, &ihi, &ilo); |
| 83 | + if (phi != ihi || plo != ilo) { |
| 84 | + fprintf(stderr, |
| 85 | + "clmul self-test: intrinsic and portable disagree on " |
| 86 | + "(%llx, %llx): portable (%llx, %llx), intrinsic (%llx, %llx)\n", |
| 87 | + (unsigned long long)a, (unsigned long long)b, |
| 88 | + (unsigned long long)phi, (unsigned long long)plo, |
| 89 | + (unsigned long long)ihi, (unsigned long long)ilo); |
| 90 | + return 1; |
| 91 | + } |
| 92 | + } |
| 93 | + printf("clmul self-test: intrinsic agrees with portable on 100000 pairs\n"); |
| 94 | +#else |
| 95 | + (void)next; |
| 96 | +#endif |
| 97 | + |
| 98 | + printf("clmul self-test: OK\n"); |
| 99 | + return 0; |
| 100 | +} |
0 commit comments