feat(synth): F64<->I64 conversions on Cortex-M7DP (closes v0.7.0 deferred items)

[avrabe]

Summary

This is v0.8.0 PR 6 from issue #147 (umbrella, "optional additive PRs", item 6). The task was to close the four F64ConvertI64S/U + I64TruncF64S/U deferred items from the v0.7.0 CHANGELOG.

Result: deferred with a written architectural finding. No code changes; documentation only. The selector continues to surface a typed Error::Synthesis for these ops — no behavior change vs. v0.7.0.

Reality check — does Cortex-M7DP support these as single VCVTs?

No, and no M-profile core does. The 64-bit integer ↔ floating-point VCVT encodings (VCVT.{F32,F64}.{S64,U64} and VCVT.{S64,U64}.{F32,F64}) were introduced in ARMv8-A FEAT_FP — they are A-profile only.

Citations:

• ARMv7-M ARM (DDI 0403E.e) §A7.5 and §A8.8 lists VCVT variants supported by M-profile FPv5-D16. Only 32-bit integer ↔ float conversions are present (VCVT.{F32,F64}.{S32,U32} and VCVT.{S32,U32}.{F32,F64}), plus VCVT.F32.F64 / VCVT.F64.F32. No 64-bit integer VCVTs.
• ARMv8-A ARM (DDI 0487) §C7.2.337+ lists the 64-bit-operand VCVT encodings, all gated on FEAT_FP. ARMv8-A is a separate architecture profile from ARMv7-M.
• The Cortex-M7DP TRM documents FPv5-D16 as the floating-point unit — no extension or option to add A-profile encodings.

This matches the existing situation in synth for F32ConvertI64S/U and the I64TruncF32S/U family, which are already deferred for the same root cause (see crates/synth-synthesis/src/instruction_selector.rs lines 1956–1960).

Emitting an A-profile-only encoding on a Cortex-M7DP would either decode to a different instruction (silent miscompile) or fault with UNDEFINSTR. The task brief explicitly says "Don't bluff" — this PR honors that.

Implementation choice

Deferred to v0.9.0 (or later floating-point milestone). Doing this properly requires:

1. A multi-instruction software sequence (~30 instructions per op) OR a soft-float helper crate
2. WASM-trap integration for I64TruncF64S/U (NaN + out-of-range trap per WASM spec §4.3.2)
3. Matching Rocq proofs (T2 existence-only minimum, with a path to T1)
4. WAST conformance test enablement (currently skipped on M7DP for these four ops)

None of this is required for v0.8.0's stated theme (i64 T1 result-correspondence parity per issue #147), and the issue itself marks this PR "optional additive". Full scoping in docs/analysis/ARMV7M_F64_I64_VCVT_FINDING.md.

What this PR ships

• docs/analysis/ARMV7M_F64_I64_VCVT_FINDING.md — full architectural finding with ISA citations, scope analysis, and the shape of the eventual closing PR.
• CHANGELOG.md [Unreleased] entry pointing at the finding. (v0.7.0 history is frozen and unchanged.)

No code changes. No new ArmOp variants. No new encoder tests (would test bogus encodings).

Test plan

• cargo test --workspace --exclude synth-verify — 1275 passed, 0 failed, 3 ignored on the deferral branch.
• cargo clippy --workspace --exclude synth-verify --all-targets -- -D warnings — clean.
• cargo fmt --check — clean.
• No new encoder tests — by design; emitting 64-bit VCVT bit patterns for an architecture that doesn't have them would be exactly the bluffing the task brief forbids.
• Bazel + Rocq proofs (bazel test //coq:verify_proofs) — unchanged, no code touched.

Why this is the right answer

The task brief gave two acceptable outcomes:

(a) defer this PR with a written explanation, or (b) implement these via a multi-instruction sequence ... Don't bluff.

Option (b) is a meaningful piece of correctness-critical work (trap semantics + softfloat + proofs) that does not fit inside an "optional additive" v0.8.0 PR. Option (a) is the principled answer — recorded as a finding so the next milestone can pick it up with full context.

🤖 Generated with Claude Code