Guard generated C against non-arithmetic signed right shift (scrutineer #2526)

[JasonGross]

Fixes scrutineer finding #2526 (CWE-758, severity Low).

Bug

The C emitter (src/Stringification/C.v) prepends one target guard to every generated file, #if (-1 & 3) != 3 / #error "This code only works on a two's complement system". That guard tests the representation of negative integers only. The generated subborrowx_u<w> functions for non-power-of-two limb widths (curve25519, p448_solinas, p521, poly1305) compute the borrow as (int1)(x1 >> w) on a negative int<bits>_t, which relies on >> being an arithmetic (sign-extending) shift. C99/C11/C17 6.5.7p5 leave that implementation-defined; only C23 mandates it. Under the other conforming choice (shifting in zeros), fiat_25519_subborrowx_u26 returns out2 = 193 for 5 of 6 in-bounds test inputs, outside its printed output bound [0x0 ~> 0x1] (reproduced locally with the finding's harness). No toolchain in current use does this, so this is a completeness gap in the compile-time refusal the project advertises, not a live bug.

Fix

Emit a second guard immediately after the existing one:

#if ((-1) >> 1) != -1
#error "This code only works on a system with arithmetic right shift of negative signed values"
#endif

#if arithmetic is done in intmax_t, so this tests exactly the property the generated code depends on, and a logical-shift implementation would refuse to compile the file instead of silently returning out-of-bound borrows.

Alternatives considered:

• Only documenting the assumption in the file-header NOTE. Weaker: a guard refuses to compile rather than relying on the integrator reading a comment, and matches the existing two's-complement treatment.
• Rewriting the emitted borrow computation to avoid signed shifts. Far more invasive (touches the pipeline and proofs) for a property every real compiler already provides.

Other backends need no change: Rust, Go, Java and Zig define >> on signed integers as arithmetic in their language specs; JSON carries no semantics; the bedrock2 C output contains no signed right shifts at all, and its prelude is produced by bedrock2's own ToCString, not this emitter.

Generated files

All 32 fiat-c/src/*.c files were updated by script (the guard is fixed text inserted directly after the existing #endif), not by regenerating with a rebuilt binary. The regeneration check in CI must confirm they match the emitter. No other tracked file carries the two's-complement guard (git grep over the tree finds only fiat-c/src/*.c and C.v).

Verification

• coqc -q -R src Crypto ... src/Stringification/C.v against the installed library: compiles (only the pre-existing missing-proof-command warning on line 398).
• The new guard expression, together with the old one, compiles with -Wall -Wextra -Wpedantic -Werror under gcc 12.2 and clang 14.0 for -std=c99, c11, c17, c2x (8/8 ok). A negated control (#if ((-1) >> 1) != 0) correctly triggers the #error, so the guard is live rather than vacuous.
• make -f Makefile.examples only-test-c-files CC=gcc and CC=clang (i.e. -Wall -Wno-unused-function -Wpedantic -Werror -c over all 32 fiat-c/src/*.c plus inversion/c/*_test.c): both exit 0, 36 object files each.
• Repro: the emitted fiat_25519_subborrowx_u26 beside a copy with a logical shift gives out2 = 193 for 5 of 6 in-bounds inputs, confirming the claim in the finding.

Not verified: no synthesis binary was rebuilt, so the regenerated-output equality relies on CI.

🤖 Generated with Claude Code

https://claude.ai/code/session_016Rbn2gww3MGhvrh52fNjpD