Fix floating-point remainder soundness and add soundness documentation

[feliperodri]

Two soundness-related fixes:

1. Fix incorrect floating-point remainder (Incorrect floating point result with remainder (%) operator #2669): The % operator on f32/f64 was silently producing wrong results because Kani emitted CBMC's integer mod operation for floating-point operands. CBMC ignores integer mod on floatbv types, leading to incorrect verification results (false negatives).

2. Add soundness documentation (Soundness documentation #1495): New docs/src/soundness.md page documenting what Kani checks, what it does not check, and known soundness caveats.

Fix for #2669

Added FloatbvMod as a new BinaryOperator variant that maps to CBMC's floatbv_mod expression, which implements IEEE 754 fmod semantics. The Expr::rem() method now dispatches to FloatbvMod for floating-point operands and Mod for integers.

Changes:

• cprover_bindings/src/goto_program/expr.rs — Add FloatbvMod variant, type validation, return type, and conditional dispatch in rem().
• cprover_bindings/src/irep/irep_id.rs — Add FloatbvMod IREP ID and string mapping.
• cprover_bindings/src/irep/to_irep.rs — Add FloatbvMod → IrepId::FloatbvMod conversion.
• tests/kani/FloatingPoint/float_remainder.rs — Regression test with symbolic f32 and f64 remainder verification.

Fix for #1495

New documentation page covering:

• What Kani checks: Arithmetic overflow, division by zero, pointer validity, array bounds, panics, shift distance, float-to-int conversion, NaN, memory leaks (always on); valid value invariants and uninitialized memory (opt-in).
• What Kani does NOT check: Data races, aliasing violations, immutable data mutation, inline assembly, ABI violations, transmute of invalid values.
• Soundness caveats: CBMC backend risks, bounded verification, floating-point model, object size limits, function pointer imprecision.

Resolves #2669
Resolves #1495

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[feliperodri]

Neither benchmark uses floating-point. Our change didn't cause this perf-benchcomp. These are solver runtime fluctuations: the SAT solver (CaDiCaL) is nondeterministic in its performance on shared CI runners. The same benchmarks that regressed on main (inet::checksum::tests::differential at 2.3x) are different from the ones regressing here, which confirms this is runner-level noise, not a code change effect.

The perf-regression.yaml threshold is solver_runtime > 1.5x with a minimum of 10 seconds. These benchmarks are in the 35-82 second range where a 1.5-1.7x fluctuation is common on shared GitHub-hosted runners due to CPU contention from other jobs on the same host.

This is not caused by the floatbv_mod change; neither benchmark involves floating-point operations. This is the same class of CI flakiness that affects the main branch (which also failed its perf benchmark with different benchmarks regressing).