Guard bedrock2 C output against mismatched target word width

[JasonGross]

Fixes scrutineer finding #2509.

The bug

The bedrock2 C backend types every word as br_word_t, an alias of uintptr_t, and the prelude's _br_load/_br_store access sizeof(br_word_t) bytes. The limb stride and buffer sizes baked into the generated code, however, come from the synthesis word size (the 32/64 in the file name). Compiling one of the fiat-bedrock2/src/*_32.c files on a 64-bit target therefore reads and writes 4 bytes past the end of every caller buffer (160 of the 183 public wrappers write out of bounds) and computes wrong field arithmetic even when buffers are over-allocated (e.g. mul(R, R) != R). The prelude's static_assert(UINTPTR_MAX <= BR_WORD_MAX, ...) cannot catch this because BR_WORD_MAX is #defined as UINTPTR_MAX. Nothing else caught it either: make only-test-bedrock2-files compiled the 14 _32 files on x86-64 CI without complaint, and no documentation said the _32 files require a 32-bit target.

The fix

• Emitter (src/Bedrock/Field/Stringification/Stringification.v): the ToString.header hook of OutputBedrock2API already receives machine_wordsize but discarded it. It now appends, after the bedrock2 prelude, a guard tied to the synthesis word size:

  // This file was synthesized for 32-bit words; br_word_t (uintptr_t) must be exactly that wide on the target.
  static_assert(BR_WORD_MAX == UINT32_MAX, "this file was synthesized for 32-bit words; compile it only for a target whose uintptr_t is 32 bits wide");

  and the UINT64_MAX counterpart for 64-bit files. A word-width mismatch is now a compile-time error in both directions instead of a silent memory-safety and correctness bug. The BR_WORD_MAX == UINTnn_MAX form matches how the prelude itself selects its _br_mulhuu implementation.
• Generated files: all 31 fiat-bedrock2/src/*.c regenerated with rebuilt synthesis binaries. The diff to each file is exactly the blank line, the comment and the static_assert (93 insertions, 0 deletions across 31 files).
• Test rule (Makefile.examples): test-bedrock2-files/only-test-bedrock2-files now compile the *_64.c files with the host default (BEDROCK2_CFLAGS_64, empty) and the *_32.c files with BEDROCK2_CFLAGS_32 (default -m32); both variables are overridable for cross compilers. A make-time check errors out if a bedrock2 file name does not end in _32/_64. The alternative of simply skipping the _32 files would have removed the only compile coverage they have; -m32 keeps CI compiling every file while honouring the new guard.
• Negative test (second commit): the same rule then compiles one _32 file with the 64-bit flags and one _64 file with the 32-bit flags and requires each to fail with the synthesized for NN-bit words message, so CI checks that the guard actually fires and not only that correctly-targeted builds succeed. The idea of a negative test is adopted from the codex/fix-2509-bedrock2-word-width branch.
• CI (.github/workflows/c.yml): install gcc-multilib so -m32 works on ubuntu-latest.
• Docs (README.md): note in the bedrock2 section that *_32.c files are for 32-bit targets and *_64.c files for 64-bit targets, and that each file rejects a mismatched target at compile time.

The vacuous static_assert(UINTPTR_MAX <= BR_WORD_MAX, "pointer fits in int") is emitted from the bedrock2 submodule's ToCString.prelude, not from fiat-crypto, so it is left untouched here; it could be dropped upstream.

Verification

All on this x86-64 host (gcc 12.2, clang available, gcc multilib installed).

• Compiled src/Bedrock/Field/Stringification/Stringification.v and src/Bedrock/Standalone/StandaloneOCamlMain.v with coqc against the installed coq-fiat-crypto-with-bedrock library (overlay build; the only upstream file that differs from HEAD in the installed copy is src/Bedrock/Field/Common/Types.v, #[export] vs #[global] on instance attributes, which cannot affect emitted text), extracted and built bedrock2_unsaturated_solinas, bedrock2_word_by_word_montgomery, bedrock2_dettman_multiplication and bedrock2_solinas_reduction with the flags from Makefile.standalone, then ran make -f Makefile.examples bedrock2-files with the four BEDROCK2_* variables pointed at those binaries. git diff -- fiat-bedrock2 | grep '^[+-]' shows only the three new lines per file.
• cc -c fiat-bedrock2/src/p256_64.c: succeeds. cc -m32 -c p256_64.c: fails with static assertion failed: "this file was synthesized for 64-bit words; ...".
• cc -c fiat-bedrock2/src/p256_32.c: fails with static assertion failed: "this file was synthesized for 32-bit words; ...". cc -m32 -c p256_32.c: succeeds. Same behaviour with clang.
• make -f Makefile.examples only-test-bedrock2-files SKIP_INCLUDE=1: exit 0, 31 object files produced (17 _64 at host width, 14 _32 under -m32), negative check passes. With BEDROCK2_CFLAGS_32=-m64 or BEDROCK2_CFLAGS_64=-m32 the rule fails at the compile step with the static_assert message. The negative check's own failure branches were exercised from a scratch makefile: swapped flags report "compiled ... but should have been rejected", and a bogus flag reports "rejected ... for the wrong reason" with the compiler output.
• Runtime self-check mul(R, R) == R via fiat_p256_set_one/fiat_p256_mul on the regenerated files: p256_32.c under -m32 reports sizeof(br_word_t)=4 limbs=8 wrong=0; p256_64.c reports sizeof(br_word_t)=8 limbs=4 wrong=0 (the finding's reproducer reported 8 of 8 limbs wrong for the _32 file on 64-bit).

Not verified: the full make of the Coq development (only the changed file and its downstream cone were compiled); the Haskell and js_of_ocaml standalone builds, which share StandaloneOCamlMain.v's dependency on the changed file but were not rebuilt; the CI run itself with gcc-multilib (the apt package name is the standard Debian/Ubuntu one and the same flag was exercised locally).

🤖 Generated with Claude Code

https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD