Investigate: verify.rs opaque-float shared const name may unify distinct float ops (verifier soundness)

[avrabe]

Investigate: verify.rs opaque-float shared const name may unify DISTINCT float ops (potential verifier unsoundness)

Surfaced during the ordeal migration gap analysis of loom-core/src/verify.rs. Flagging for confirmation — if real, it's an unsoundness in the verifier itself (the check could accept a wrong transform), which is more serious than a pass bug.

The concern

Float ops are modeled as opaque bitvectors: each f32.*/f64.* op pushes a fixed-named fresh const, e.g. BV::new_const("f32_add_result", 32) (~verify.rs:4921-4927). The intent is that identical float ops in the original and optimized encodings unify to the same symbolic const so they compare equal. But a fixed name shared across all sites means two different float-op sites also unify: f32.add(a,b) (original) and f32.add(c,d) (optimized) both become the same const f32_add_result even when a,b ≠ c,d. The equivalence check orig ≠ opt could then be UNSAT for the wrong reason — proving two non-equivalent functions "equivalent" and accepting an unsound float transform.

Contrast

The havoc/opaque-call path is done right — it uses a deterministic per-encode call_id counter so corresponding calls unify but distinct calls don't (verify.rs:4652-4684). The float path appears to use a fixed name instead of the same discipline.

Ask

1. Confirm whether a per-site counter (or operand-dependent encoding) actually mitigates this, or the fixed name is used verbatim.
2. If unmitigated: model an opaque float op as an uninterpreted function over its operands — f32_add(a,b) via FuncDecl/congruence (equal only when operands equal), the same congruence trick the pure-call path uses — so distinct sites don't wrongly unify while identical sites still do. Add a regression: a fixture where a pass rewrites f32.add(a,b) to a non-equivalent f32.add(c,d) must be REJECTED by verify.
3. Cross-check with the behavioral differential gate (Behavioral differential as an optimization gate (self-certify non-Z3-backstoppable transforms) #238) — it would catch a float miscompile by execution even if the SMT check is fooled.

Note: loom skips float load/store functions entirely (SkippedMemory), which may limit exposure — part of what needs confirming. Refs: gap analysis of verify.rs float modeling.