Add C-371 (Float32 arithmetic rounds to binary32) and C-372 (Float32 shortest display)

[O6lvl4]

This PR adds two contracts for almide#3080, almide#3082, almide#3079 and almide#3081. The implementation PRs in almide/almide will declare them after the pin advances.

• C-371 (ALS-T28): Float32 arithmetic.
  • What it states:
    • Each Float32 + - * / % ** and unary - result is rounded to binary32 (round-to-nearest-even), on every leg.
    • ** is the vendored libm pow of the widened operands, rounded once.
    • Conversions into Float32 round once.
    • Comparisons read the rounded values.
    • No math.* function takes a Float32.
  • Fixture: spec/wasm_cross/float32_arithmetic_rounds.almd.
• C-372 (ALS-T29): Float32 display.
  • What it states:
    • A Float32 prints as the shortest decimal that round-trips to the same binary32 (Rust f32 Display).
    • An exact tie rounds the magnitude up.
    • Interpolation and container display drop the .0 (C-011's rule); float32.to_string keeps it.
    • The digits are the same top-level and nested in a list, record, option, tuple or variant.
  • Fixture: spec/wasm_cross/float32_display_shortest.almd.

Ref evaluator.

• New binary32 semantics:
  • Float32 + - * / % **, unary -, comparisons and ==, with a bare float literal operand narrowed to Float32.
  • float.to_float32 and float32.to_float64.
  • Float32 display, top-level and nested, and float32.to_string in the shortest-f32 form. These run the existing free-format digit generator over the f32 significand and exponent.
• Tie fix. The generator broke an exact tie toward an even digit. Rust Display rounds the magnitude up (2^-12 prints 0.00024414063; 1669760939663944.25 prints ...944.3), so the generator now does the same. The f64 tie case is added to the oracle test.
• New oracle test. ref/tests/fmt_oracle.rs::f32_display_matches_host_shortest compares the ref against the host f32 Display over every f32 biased exponent (with the significand edges, both signs) and 3,000 pseudo-random patterns: 6,584 values, all equal.

Checked locally.

• Both fixtures run on the ref, and their output matches native almide byte for byte. The wasm leg and the interpreter still diverge; that is the divergence the two implementation PRs fix.
• All the CLAUDE.md pre-commit gates pass, plus check-ref-totality, check-ref-independence, and the ref's cargo test.