[AdaWorldAPI]

Follow-up to #374, which made wasm F32x16::mul_add and F64x8::mul_add round once.

What changes

Edge fixtures for the F64 guard (crates/simd-masking-parity). The wasm F64x8::mul_add vector path (Dekker product, two-sum, round-to-odd) is exact only for 2^-460 <= |a|, |b| <= 2^460, |c| <= 2^960. Each v128 pair outside that range goes lane by lane to the integer FMA in simd_fma.rs. Until now the 0x11xx group reached that fallback only through random bit patterns. Widening the lower bound to 2^-600 stayed green.

Round 5 (edge_lanes_f64) adds lanes on both sides of every bound, plus:

• |c| == 2^960;
• mixed pairs (one lane inside, one outside);
• products below the subnormal range and above f64::MAX;
• a zero, infinity or NaN in a or b, against every kind of c.

Each lane the emulation gets wrong shares its pair with an in-range lane, so a widened guard sends it to the vector path. The reference is still the 4608-bit integer oracle. New anti-vacuity codes:

• 0x11F2: lanes where a scalar copy of the unguarded emulation is wrong;
• 0x11F3: pairs on the vector path;
• 0x11F4: mixed pairs;
• 0x11F5: pairs on the repaired path.

Exact-product repair (src/simd_wasm.rs). A lane whose a or b is a zero, an infinity or NaN has an exact product, so a * b + c rounds once. That is the IEEE result, and it is the identity simd_fma::fma_f64 starts with. Such pairs now stay in the vector with a per-lane select. Before, one zero sent the whole pair to the integer FMA. The in-domain path is unchanged.

Relaxed SIMD (scripts/masking-parity.sh wasm-relaxed, one CI step). No source path selects on relaxed-simd. The parity wasm built with +simd128,+relaxed-simd has a code section byte-identical to the +simd128 build, with 0 relaxed-SIMD opcodes. A control that calls f64x2_relaxed_madd shows the opcode scan can fire. The new arm runs the parity program in that configuration, so a relaxed path cannot appear later unnoticed. It does not exercise an engine executing relaxed instructions, because none are emitted.

Proof obligations (.claude/knowledge/wasm-fma-proof-obligations.md). Each obligation is marked by kind of evidence:

• Proven here: the F32 path end to end; for F64, no overflow, the Dekker condition (e_a + e_b >= -970 against the guard's -920), TwoSum, round-to-odd through the midpoint argument (subnormal intermediates included), near-zero cancellation, the exact-product repair, bit-select and mixed pairs.
• Cited, not re-proven: the Veltkamp split, Dekker's product and Knuth's TwoSum.
• Tested only: the integer fallback, and compiler output per realization.
• Open: there is no mechanized proof.

The measured margin of the guard is labelled as a measurement, not proof, and the guard is unchanged.

Board. New blackboard entries for the fix and for this audit. Coresearch row X11 now states its current status first; its superseded wording is kept in the audit entry.

Evidence

• Arms green: masking-parity.sh wasm, wasm-scalar, wasm-relaxed and native (AVX-512 host with hardware FMA), plus scripts/wasm-parity.sh. Parity crate clippy -D warnings is clean.
• Disable runs, red (each restored): guard removed; lower bound 2^-520; a/b upper bound 2^530; per-pair all_true → any_true; f32 round-to-odd dropped; f64 round-to-odd dropped; round-to-odd step always up; repair returns c; repair drops c; tiny a treated as an exact product; large or non-finite c treated as an exact product.
• Disable runs, green, and why:
  • Lower bound 2^-500: inside the proven condition.
  • c bound 2^1023: no counterexample exists given the a/b bounds.
  • Three disables that narrow the repair predicate: the lanes they drop fall back to the exact integer FMA. They are performance regressions, not wrong results.
• V8 (node 22), ns per element:
  • in-domain path: ~6.2, against ~1.1 for unfused a * b + c;
  • lane fallback: ~50–58;
  • 10% zeros in a: 9–13 → ~7.0;
  • 50% zeros: 28–33 → ~9.3.

Not claimed

• NaN payload bits or NaN sign: any NaN matches any NaN.
• reduce_sum is a separate contract. Its summation order differs per backend.
• Exhaustive coverage of the input space. The fixtures are random and adversarial.

lance-graph is untouched. D-WFL-DET may rely on a verified single-rounding mul_add across realizations. D-OIF-4's kernel is defined as multiply then add, and must not become a fused FMA.

🤖 Generated with Claude Code

https://claude.ai/code/session_01XAqKMPh2Seh2WLccCksAdY

[coderabbitai]

Important

• 🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: c3368170-a971-4707-9f16-61ec4ebb65aa

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Warning

Billing warning: we have not been able to collect payment for this subscription for more than 72 hours. Please update the payment method or pay any pending invoices in Billing to avoid service interruption.

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-27T10:37:02.011252Z	7861a5f	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.