diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 59cd75104f82..67daf68b1585 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -1353,6 +1353,7 @@ jobs:
     - uses: ./.github/actions/install-rust
     - run: cargo run -p cranelift-isle-veri --bin veri -- --config cranelift/isle/veri/configs/aarch64-fast.args --skip-solver
     - run: cargo run -p cranelift-isle-veri --bin veri -- --name x64 --rule iadd_base_case_32_or_64_lea --skip-solver
+    - run: cargo run -p cranelift-isle-veri --bin veri -- --name opt --only-root simplify --default-excludes --skip-solver
 
   # Perform release builds of `wasmtime` and `libwasmtime.so`. Builds a variety
   # of platforms and architectures and then uploads the release artifacts to
diff --git a/cranelift/codegen/meta/src/isle.rs b/cranelift/codegen/meta/src/isle.rs
index 540cabbe0b6f..6f39a34e1390 100644
--- a/cranelift/codegen/meta/src/isle.rs
+++ b/cranelift/codegen/meta/src/isle.rs
@@ -130,6 +130,14 @@ pub fn get_isle_compilations(
         inputs.extend(extra.iter().map(|f| spec_dir.join(f)));
         inputs
     };
+    let lower_spec_inputs = |extra: &[&str]| -> Vec<std::path::PathBuf> {
+        let mut inputs = spec_inputs(extra);
+        if cfg!(feature = "spec") {
+            let spec_dir = codegen_crate_dir.join("src").join("spec");
+            inputs.push(spec_dir.join("prelude_lower_spec.isle"));
+        }
+        inputs
+    };
 
     // Directory for mid-end optimizations.
     let src_opts = codegen_crate_dir.join("src").join("opts");
@@ -166,7 +174,7 @@ pub fn get_isle_compilations(
                 output: gen_dir.join("isle_opt.rs"),
                 tracked_inputs: [
                     vec![prelude_isle.clone(), prelude_opt_isle],
-                    spec_inputs(&[]),
+                    spec_inputs(&["fpconst.isle", "opt.isle"]),
                     vec![
                         src_opts.join("arithmetic.isle"),
                         src_opts.join("bitops.isle"),
@@ -191,7 +199,7 @@ pub fn get_isle_compilations(
                 output: gen_dir.join("isle_x64.rs"),
                 tracked_inputs: [
                     vec![prelude_isle.clone(), prelude_lower_isle.clone()],
-                    spec_inputs(&["state.isle"]),
+                    lower_spec_inputs(&["fpconst.isle", "state.isle"]),
                     vec![
                         src_isa_x64.join("inst.isle"),
                         src_isa_x64.join("lower.isle"),
@@ -210,7 +218,7 @@ pub fn get_isle_compilations(
                 output: gen_dir.join("isle_aarch64.rs"),
                 tracked_inputs: [
                     vec![prelude_isle.clone(), prelude_lower_isle.clone()],
-                    spec_inputs(&["fpconst.isle", "state.isle"]),
+                    lower_spec_inputs(&["fpconst.isle", "state.isle"]),
                     vec![
                         src_isa_aarch64.join("inst.isle"),
                         src_isa_aarch64.join("inst_neon.isle"),
@@ -235,7 +243,7 @@ pub fn get_isle_compilations(
                 output: gen_dir.join("isle_s390x.rs"),
                 tracked_inputs: [
                     vec![prelude_isle.clone(), prelude_lower_isle.clone()],
-                    spec_inputs(&[]),
+                    lower_spec_inputs(&[]),
                     vec![
                         src_isa_s390x.join("inst.isle"),
                         src_isa_s390x.join("lower.isle"),
@@ -250,7 +258,7 @@ pub fn get_isle_compilations(
                 output: gen_dir.join("isle_riscv64.rs"),
                 tracked_inputs: [
                     vec![prelude_isle.clone(), prelude_lower_isle.clone()],
-                    spec_inputs(&[]),
+                    lower_spec_inputs(&[]),
                     vec![
                         src_isa_risc_v.join("inst.isle"),
                         src_isa_risc_v.join("inst_vector.isle"),
diff --git a/cranelift/codegen/src/opts/arithmetic.isle b/cranelift/codegen/src/opts/arithmetic.isle
index 07faaba82148..2083ff8bee85 100644
--- a/cranelift/codegen/src/opts/arithmetic.isle
+++ b/cranelift/codegen/src/opts/arithmetic.isle
@@ -5,7 +5,7 @@
 ;; the right, and thus only simplify patterns like `x+0`, not `0+x`.
 
 ;; x+0 == x.
-(rule (simplify (iadd ty
+(rule iadd_x_plus_zero (simplify (iadd ty
                       x
                       (iconst_u ty 0)))
       (subsume x))
@@ -191,7 +191,7 @@
 
 ;; If both of the multiplied arguments to an `fmul` are negated then remove
 ;; both of them since they cancel out.
-(rule (simplify (fmul ty (fneg ty x) (fneg ty y)))
+(rule fmul_fneg_fneg (simplify (fmul ty (fneg ty x) (fneg ty y)))
       (fmul ty x y))
 
 ;; Detect people open-coding `mulhi`: (x as big * y as big) >> bits
@@ -567,4 +567,4 @@
 (rule (simplify (ult ty (umax ty y x) x)) (iconst_u ty 0))
 
 ;; (-X) * C = X * (-C)
-(rule (simplify (imul (fits_in_64 ty) (ineg ty x) (iconst ty y))) (imul ty x (iconst ty (imm64_neg ty y))))
+(rule imul_ineg_const (simplify (imul (fits_in_64 ty) (ineg ty x) (iconst ty y))) (imul ty x (iconst ty (imm64_neg ty y))))
diff --git a/cranelift/codegen/src/prelude_opt.isle b/cranelift/codegen/src/prelude_opt.isle
index f333d51bd019..e855b5bc2f3b 100644
--- a/cranelift/codegen/src/prelude_opt.isle
+++ b/cranelift/codegen/src/prelude_opt.isle
@@ -627,3 +627,7 @@
         (isub $I64 numerator tt)))
 (rule (apply_div_const_magic_s64_finish (Opcode.Sdiv) _numerator _divisor qf)
       qf)
+
+(model Inst (type (bv)))
+(model ValueArray2 (type (bv)))
+(model ValueArray3 (type (bv)))
\ No newline at end of file
diff --git a/cranelift/codegen/src/spec/inst_specs.isle b/cranelift/codegen/src/spec/inst_specs.isle
index 6f4e808b42c9..92eda9446210 100644
--- a/cranelift/codegen/src/spec/inst_specs.isle
+++ b/cranelift/codegen/src/spec/inst_specs.isle
@@ -2,6 +2,7 @@
 
 (model Imm64 (type (bv 64)))
 
+(model Ieee16 (type (bv 16)))
 (model Ieee32 (type (bv 32)))
 (model Ieee64 (type (bv 64)))
 
@@ -61,6 +62,18 @@
     (type Bool)
     (default (not clif_trap)))
 
+; Whether the value being rewritten is a nondeterministic arithmetic NaN,
+; which loosens the mid-end `simplify` soundness contract from exact bitwise
+; equality to `fp_equiv!` (see `opt.isle`). Relevant floating-point arithmetic
+; instructions (`fadd`/`fmul`/...) set to true exactly when they produce a NaN;
+; deterministic float bit-ops (`fneg`/`fabs`/`fcopysign`) leave it at the
+; default `false`. Modeled as execution state (like `clif_trap`) so the relaxation
+; is expressed declaratively in specs rather than special-cased in the verifier
+; (because `simplify` does not consume the value type).
+(state relax_nan
+    (type Bool)
+    (default (not relax_nan)))
+
 ;;;; Common Term Forms ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (form
@@ -367,16 +380,14 @@
     ((args (named Type) (bv 64)) (ret (bv 32))))
 
 (form extend
-    ((args (named Type) (bv  8)) (ret (bv  8)))
     ((args (named Type) (bv  8)) (ret (bv 16)))
     ((args (named Type) (bv  8)) (ret (bv 32)))
     ((args (named Type) (bv  8)) (ret (bv 64)))
-    ((args (named Type) (bv 16)) (ret (bv 16)))
     ((args (named Type) (bv 16)) (ret (bv 32)))
     ((args (named Type) (bv 16)) (ret (bv 64)))
-    ((args (named Type) (bv 32)) (ret (bv 32)))
     ((args (named Type) (bv 32)) (ret (bv 64))))
-    ;; Note: (bv 64) -> (bv 64) not accepted in clif
+    ;; Note: extends must strictly widen, so same-width instantiations
+    ;; (8->8, 16->16, 32->32, 64->64) are not accepted in clif.
 
 (spec (uextend ty x)
     (provide (= result (zero_ext (widthof result) x))
@@ -388,16 +399,6 @@
              (= (:bits ty) (widthof result))))
 (instantiate sextend extend)
 
-;; `maybe_uextend` "sees through" a `uextend`: given the outer value `result`,
-;; it yields the inner value `value`. When `result` is defined by a `uextend`,
-;; `value` is that uextend's argument; otherwise `value` is `result` itself. In
-;; both cases the inner value is the low bits of the outer value, i.e. the outer
-;; value is the zero-extension of the inner one to the outer width (in the
-;; fall-through case the two widths are equal, so this is the identity). The
-;; extractor is total (it always matches), so no `match` clause is needed.
-(spec (maybe_uextend value)
-    (provide (= result (zero_ext (widthof result) value))))
-
 (spec (smin ty x y)
     (provide (= result (if (bvsle x y) x y))
              (= (:bits ty) (widthof result))))
@@ -710,7 +711,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (fadd ty x y)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
@@ -751,7 +755,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (fsub ty x y)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
@@ -794,7 +801,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (fmul ty x y)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
@@ -837,7 +847,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (fdiv ty x y)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
@@ -884,7 +897,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (fmin ty x y)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
@@ -911,7 +927,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (fmax ty x y)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If either z1 or z2 is a NaN, then return an element of nans{z1,z2}.
@@ -967,14 +986,11 @@
 (spec (fneg ty x)
     (provide
         (= (:bits ty) (widthof result))
-        (= result
-            ; If z is a NaN, then return z with negated sign.
-            (if (fp.isNaN x)
-                (nan_neg! x)
-            ; Else if z is an infinity, then return that infinity negated.
-            ; Else if z is a zero, then return that zero negated.
-            ; Else return z negated.
-                (fp.neg x))))) ; Remaining cases of the spec handled by SMT fp.neg
+        ; IEEE-754 negation just toggles the sign bit for every input (normal,
+        ; +/-0, +/-inf, NaN), so model it directly in the bit-vector theory: this
+        ; is bit-exact and avoids an fp<->bv bridge that makes queries like
+        ; `fmul_fneg_fneg` intractable.
+        (= result (bvxor x (fp_sign_bit_set! (widthof x))))))
 (instantiate fneg
     ((args (named Type) (bv 32)) (ret (bv 32)))
     ((args (named Type) (bv 64)) (ret (bv 64))))
@@ -984,7 +1000,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (sqrt ty x)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If z is a NaN, then return an element of nans{z}.
@@ -1012,7 +1031,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (ceil ty x)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If z is a NaN, then return an element of nans{z}.
@@ -1037,7 +1059,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (floor ty x)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If z is a NaN, then return an element of nans{z}.
@@ -1062,7 +1087,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (trunc ty x)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If z is a NaN, then return an element of nans{z}.
@@ -1089,7 +1117,10 @@
 ;
 ; Specification derived from WebAssembly Specification prose (Floating Point Numerics, section 4.3.3).
 (spec (nearest ty x)
+    (modifies relax_nan produces_nan)
     (provide
+        (= produces_nan (fp.isNaN result))
+        (=> produces_nan relax_nan)
         (= (:bits ty) (widthof result))
         (= result
             ; If z is a NaN, then return an element of nans{z}.
diff --git a/cranelift/codegen/src/spec/opt.isle b/cranelift/codegen/src/spec/opt.isle
new file mode 100644
index 000000000000..06f67b6baaff
--- /dev/null
+++ b/cranelift/codegen/src/spec/opt.isle
@@ -0,0 +1,687 @@
+;;;; Specs for mid-end (`opt`) helper terms declared in `prelude_opt.isle`,
+;;;; rather than in the shared `inst_specs.isle`.
+
+;; Soundness contract for the top-level rewrite term: by default a rewrite must
+;; preserve the value exactly (bitwise equality). This holds for all non-floating
+;; point rules and for most float values, including deterministic float bit-ops
+;; (`fneg`/`fabs`/`fcopysign`) and float arithmetic that does not produce a NaN.
+;;
+;; The one exception is float arithmetic that produces a NaN: because Wasm
+;; arithmetic NaN payloads are nondeterministic, exact bit-equality is too
+;; strong. When the value being rewritten was produced by a float-arithmetic op
+;; that returned a NaN (tracked by the `relax_nan` execution state, set in
+;; `inst_specs.isle`), the contract relaxes to CLIF-level float equivalence
+;; (`fp_equiv!`: bitwise-equal or both arithmetic NaNs). This matches Wasm
+;; semantics for existing rules that compose operations on floats, but could be
+;; unsound on future rules that compute on floats yet discard the float result
+;; in favor of returning e.g. an integer result (where `fp_equiv!` on an
+;; integer-typed result would wrongly treat NaN-patterned bits as equivalent).
+(spec (simplify arg)
+    (provide
+        (if relax_nan
+            (fp_equiv! result arg)
+            (= result arg))))
+(instantiate simplify
+    ((args (bv  8)) (ret (bv  8)))
+    ((args (bv 16)) (ret (bv 16)))
+    ((args (bv 32)) (ret (bv 32)))
+    ((args (bv 64)) (ret (bv 64))))
+
+;; `remat` and `subsume` annotate a rewrite without changing the value.
+(spec (remat x) (provide (= result x)))
+(spec (subsume x) (provide (= result x)))
+
+;; `imm64_*` constant folding: the wrapping op masked to the low `ty` bits (the
+;; Rust impls `& ty_mask`), keeping `Imm64` consistent with the `iconst` spec.
+(spec (imm64_add ty x y)
+    (provide (= result (bvand (bvadd x y) (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_sub ty x y)
+    (provide (= result (bvand (bvsub x y) (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_neg ty x)
+    (provide (= result (bvand (bvneg x) (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_not ty x)
+    (provide (= result (bvand (bvnot x) (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_mul ty x y)
+    (provide (= result (bvand (bvmul x y) (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_and ty x y)
+    (provide (= result (bvand (bvand x y) (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_or ty x y)
+    (provide (= result (bvand (bvor x y) (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_xor ty x y)
+    (provide (= result (bvand (bvxor x y) (low_bits_mask! 64 (:bits ty))))))
+
+;; `imm64_shl`/`imm64_ushr`: the shift amount is masked to `ty.bits()-1` on
+;; 64-bit `Imm64` values.
+(spec (imm64_shl ty x y)
+    (provide (= result
+                (bvand (bvshl x (bvand y (bvsub (int2bv 64 (:bits ty)) #x0000000000000001)))
+                       (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_ushr ty x y)
+    (provide (= result
+                (bvlshr (bvand x (low_bits_mask! 64 (:bits ty)))
+                        (bvand y (bvsub (int2bv 64 (:bits ty)) #x0000000000000001))))))
+
+;; `iconst_u`/`iconst_s` are `(decl rec ...)` (their 128-bit/vector rules
+;; recur), so they are cyclic and need specs rather than chaining. As
+;; extractors they yield the constant `c` as the zero/sign-extension of the
+;; matched value to 64 bits, mirroring the `iconst` spec.
+(spec (iconst_u ty c)
+    (provide (= c (zero_ext 64 result))
+             (= (:bits ty) (widthof result))))
+(instantiate iconst_u
+    ((args (named Type) (bv 64)) (ret (bv 8)))
+    ((args (named Type) (bv 64)) (ret (bv 16)))
+    ((args (named Type) (bv 64)) (ret (bv 32)))
+    ((args (named Type) (bv 64)) (ret (bv 64))))
+(spec (iconst_s ty c)
+    (provide (= c (sign_ext 64 result))
+             (= (:bits ty) (widthof result))))
+(instantiate iconst_s
+    ((args (named Type) (bv 64)) (ret (bv 8)))
+    ((args (named Type) (bv 64)) (ret (bv 16)))
+    ((args (named Type) (bv 64)) (ret (bv 32)))
+    ((args (named Type) (bv 64)) (ret (bv 64))))
+
+;; Comparison helpers, each an extractor for an `icmp` with a fixed condition
+;; code; mirroring the `icmp` spec (result `#x01`/`#x00`).
+(form comparison
+    ((args (named Type) (bv  8) (bv  8)) (ret (bv 8)))
+    ((args (named Type) (bv 16) (bv 16)) (ret (bv 8)))
+    ((args (named Type) (bv 32) (bv 32)) (ret (bv 8)))
+    ((args (named Type) (bv 64) (bv 64)) (ret (bv 8))))
+(spec (eq ty x y)
+    (provide (= result (if (= x y) #x01 #x00))))
+(spec (ne ty x y)
+    (provide (= result (if (not (= x y)) #x01 #x00))))
+(spec (ult ty x y)
+    (provide (= result (if (bvult x y) #x01 #x00))))
+(spec (ule ty x y)
+    (provide (= result (if (bvule x y) #x01 #x00))))
+(spec (ugt ty x y)
+    (provide (= result (if (bvugt x y) #x01 #x00))))
+(spec (uge ty x y)
+    (provide (= result (if (bvuge x y) #x01 #x00))))
+(spec (slt ty x y)
+    (provide (= result (if (bvslt x y) #x01 #x00))))
+(spec (sle ty x y)
+    (provide (= result (if (bvsle x y) #x01 #x00))))
+(spec (sgt ty x y)
+    (provide (= result (if (bvsgt x y) #x01 #x00))))
+(spec (sge ty x y)
+    (provide (= result (if (bvsge x y) #x01 #x00))))
+(instantiate eq comparison)
+(instantiate ne comparison)
+(instantiate ult comparison)
+(instantiate ule comparison)
+(instantiate ugt comparison)
+(instantiate uge comparison)
+(instantiate slt comparison)
+(instantiate sle comparison)
+(instantiate sgt comparison)
+(instantiate sge comparison)
+
+;; Pure constant-folding helpers on 64-bit immediates.
+(spec (i64_wrapping_neg x) (provide (= result (bvneg x))))
+(spec (u64_lt x y) (provide (= result (bvult x y))))
+(spec (imm64 x) (provide (= result x)))
+
+(spec (cmp_true ty) (provide (= result (zero_ext (widthof result) #b1))))
+(instantiate cmp_true
+    ((args (named Type)) (ret (bv  8)))
+    ((args (named Type)) (ret (bv 16)))
+    ((args (named Type)) (ret (bv 32)))
+    ((args (named Type)) (ret (bv 64))))
+
+;; Type-derived `u64` helpers. `ty_mask` is the low `ty.bits()` set (Rust
+;; `u64::MAX >> (64 - ty.bits())`), `ty_umax` is defined as `ty_mask`, and
+;; `ty_bits_u64` is the bitwidth itself.
+(spec (ty_mask ty) (provide (= result (low_bits_mask! 64 (:bits ty)))))
+(spec (ty_umax ty) (provide (= result (low_bits_mask! 64 (:bits ty)))))
+(spec (ty_bits_u64 ty) (provide (= result (int2bv 64 (:bits ty)))))
+
+;; `uextend_maybe` "sees through" a `uextend`: given the outer value `result`,
+;; it yields the inner `val`, with the outer being the zero-extension of the
+;; inner to `ty` bits. Mirrors `maybe_uextend`.
+(spec (uextend_maybe ty val)
+    (provide (= result (zero_ext (widthof result) val))
+             (= (:bits ty) (widthof result))))
+
+;; The rule `(uextend_maybe ty val) => (uextend ty val)` needs concrete widths to
+;; type-check standalone (its spec leaves `val`'s width free). Unlike `uextend`,
+;; `uextend_maybe` also has an identity rule for the same-width case, so allow
+;; every `val`-width <= `ty`-width pairing rather than reusing strict `extend`.
+(instantiate uextend_maybe
+    ((args (named Type) (bv  8)) (ret (bv  8)))
+    ((args (named Type) (bv  8)) (ret (bv 16)))
+    ((args (named Type) (bv  8)) (ret (bv 32)))
+    ((args (named Type) (bv  8)) (ret (bv 64)))
+    ((args (named Type) (bv 16)) (ret (bv 16)))
+    ((args (named Type) (bv 16)) (ret (bv 32)))
+    ((args (named Type) (bv 16)) (ret (bv 64)))
+    ((args (named Type) (bv 32)) (ret (bv 32)))
+    ((args (named Type) (bv 32)) (ret (bv 64)))
+    ((args (named Type) (bv 64)) (ret (bv 64))))
+
+(attr splat (tag vector))
+
+;;;; Concrete `f32`/`f64` sign bit-ops ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Total sign-bit folds (`Ieee{32,64}` model as `(bv {32,64})`); no NaN-sign case
+;; analysis needed, unlike the `fneg`/`fabs`/`fcopysign` instruction specs.
+(spec (f32_neg x) (provide (= result (bvxor x (fp_sign_bit_set! (widthof x))))))
+(spec (f64_neg x) (provide (= result (bvxor x (fp_sign_bit_set! (widthof x))))))
+(spec (f32_abs x) (provide (= result (bvand x (bvnot (fp_sign_bit_set! (widthof x)))))))
+(spec (f64_abs x) (provide (= result (bvand x (bvnot (fp_sign_bit_set! (widthof x)))))))
+(spec (f32_copysign x y)
+    (provide
+        (= result
+            (bvor (bvand x (bvnot (fp_sign_bit_set! (widthof x))))
+                  (bvand y (fp_sign_bit_set! (widthof y)))))))
+(spec (f64_copysign x y)
+    (provide
+        (= result
+            (bvor (bvand x (bvnot (fp_sign_bit_set! (widthof x))))
+                  (bvand y (fp_sign_bit_set! (widthof y)))))))
+
+;;;; Concrete `f32`/`f64` arithmetic constant-folds ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Partial: Rust `.non_nan()` returns None on a NaN result, so the `match` rules
+;; out NaN-producing inputs (relax_nan stays false; exact equality required). Each
+;; `fold_f*` macro copies the non-NaN branches of the `inst_specs.isle` result, so
+;; `lhs == rhs` is structural rather than a 64-bit IEEE-equivalence query.
+(macro (fold_fadd x y)
+    (if (or (fp.isNaN x) (fp.isNaN y))
+        (nans2! x y)
+    (if (and (fp.isInfinite x) (fp.isInfinite y) (fp_opposite_sign! x y))
+        (nans0! (widthof x))
+    (if (and (fp.isInfinite x) (fp.isInfinite y) (fp_equal_sign! x y))
+        x
+    (if (fp.isInfinite x)
+        x
+    (if (fp.isInfinite y)
+        y
+    (if (and (fp.isZero x) (fp.isZero y) (fp_opposite_sign! x y))
+        (fp.+zero (widthof x))
+    (if (and (fp.isZero x) (fp.isZero y) (fp_equal_sign! x y))
+        x
+    (if (fp.isZero x)
+        y
+    (if (fp.isZero y)
+        x
+    (if (and (= (fp_magnitude! x) (fp_magnitude! y)) (fp_opposite_sign! x y))
+        (fp.+zero (widthof x))
+        (fp.add x y))))))))))))
+
+(macro (fold_fsub x y)
+    (if (or (fp.isNaN x) (fp.isNaN y))
+        (nans2! x y)
+    (if (and (fp.isInfinite x) (fp.isInfinite y) (fp_equal_sign! x y))
+        (nans0! (widthof x))
+    (if (and (fp.isInfinite x) (fp.isInfinite y) (fp_opposite_sign! x y))
+        x
+    (if (fp.isInfinite x)
+        x
+    (if (fp.isInfinite y)
+        (fp.neg y)
+    (if (and (fp.isZero x) (fp.isZero y) (fp_equal_sign! x y))
+        (fp.+zero (widthof x))
+    (if (and (fp.isZero x) (fp.isZero y) (fp_opposite_sign! x y))
+        x
+    (if (fp.isZero y)
+        x
+    (if (fp.isZero x)
+        (fp.neg y)
+    (if (and (= (fp_magnitude! x) (fp_magnitude! y)) (fp_equal_sign! x y))
+        (fp.+zero (widthof x))
+        (fp.sub x y))))))))))))
+
+(macro (fold_fmul x y)
+    (if (or (fp.isNaN x) (fp.isNaN y))
+        (nans2! x y)
+    (if (and (fp.isZero x) (fp.isInfinite y))
+        (nans0! (widthof x))
+    (if (and (fp.isInfinite x) (fp.isZero y))
+        (nans0! (widthof x))
+    (if (and (fp.isInfinite x) (fp.isInfinite y) (fp_equal_sign! x y))
+        (fp.+oo (widthof x))
+    (if (and (fp.isInfinite x) (fp.isInfinite y) (fp_opposite_sign! x y))
+        (fp.-oo (widthof x))
+    (if (and (fp.isInfinite x) (fp_equal_sign! x y))
+        (fp.+oo (widthof x))
+    (if (and (fp.isInfinite y) (fp_equal_sign! x y))
+        (fp.+oo (widthof x))
+    (if (and (fp.isInfinite x) (fp_opposite_sign! x y))
+        (fp.-oo (widthof x))
+    (if (and (fp.isInfinite y) (fp_opposite_sign! x y))
+        (fp.-oo (widthof x))
+    (if (and (fp.isZero x) (fp.isZero y) (fp_equal_sign! x y))
+        (fp.+zero (widthof x))
+    (if (and (fp.isZero x) (fp.isZero y) (fp_opposite_sign! x y))
+        (fp.-zero (widthof x))
+        (fp.mul x y)))))))))))))
+
+(macro (fold_fdiv x y)
+    (if (or (fp.isNaN x) (fp.isNaN y))
+        (nans2! x y)
+    (if (and (fp.isInfinite x) (fp.isInfinite y))
+        (nans0! (widthof x))
+    (if (and (fp.isZero x) (fp.isZero y))
+        (nans2! x y)
+    (if (and (fp.isInfinite x) (fp_equal_sign! x y))
+        (fp.+oo (widthof x))
+    (if (and (fp.isInfinite x) (fp_opposite_sign! x y))
+        (fp.-oo (widthof x))
+    (if (and (fp.isInfinite y) (fp_equal_sign! x y))
+        (fp.+zero (widthof x))
+    (if (and (fp.isInfinite y) (fp_opposite_sign! x y))
+        (fp.-zero (widthof x))
+    (if (and (fp.isZero x) (fp_equal_sign! x y))
+        (fp.+zero (widthof x))
+    (if (and (fp.isZero x) (fp_opposite_sign! x y))
+        (fp.-zero (widthof x))
+    (if (and (fp.isZero y) (fp_equal_sign! x y))
+        (fp.+oo (widthof x))
+    (if (and (fp.isZero y) (fp_opposite_sign! x y))
+        (fp.-oo (widthof x))
+        (fp.div x y)))))))))))))
+
+(spec (f32_add x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))
+                (not (and (fp.isInfinite x) (fp.isInfinite y) (fp_opposite_sign! x y)))))
+    (provide (= result (fold_fadd! x y))))
+(spec (f64_add x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))
+                (not (and (fp.isInfinite x) (fp.isInfinite y) (fp_opposite_sign! x y)))))
+    (provide (= result (fold_fadd! x y))))
+(spec (f32_sub x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))
+                (not (and (fp.isInfinite x) (fp.isInfinite y) (fp_equal_sign! x y)))))
+    (provide (= result (fold_fsub! x y))))
+(spec (f64_sub x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))
+                (not (and (fp.isInfinite x) (fp.isInfinite y) (fp_equal_sign! x y)))))
+    (provide (= result (fold_fsub! x y))))
+
+;; cvc5 answers `unknown` on the bit-blasted `fsub` fold queries; route them to z3
+(attr f32_sub (tag solver_z3))
+(attr f64_sub (tag solver_z3))
+(spec (f32_mul x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))
+                (not (and (fp.isZero x) (fp.isInfinite y)))
+                (not (and (fp.isInfinite x) (fp.isZero y)))))
+    (provide (= result (fold_fmul! x y))))
+
+(spec (f64_mul x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))
+                (not (and (fp.isZero x) (fp.isInfinite y)))
+                (not (and (fp.isInfinite x) (fp.isZero y)))))
+    (provide (= result (fold_fmul! x y))))
+
+(spec (f32_div x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))
+                (not (and (fp.isInfinite x) (fp.isInfinite y)))
+                (not (and (fp.isZero x) (fp.isZero y)))))
+    (provide (= result (fold_fdiv! x y))))
+
+(spec (f64_div x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))
+                (not (and (fp.isInfinite x) (fp.isInfinite y)))
+                (not (and (fp.isZero x) (fp.isZero y)))))
+    (provide (= result (fold_fdiv! x y))))
+
+;; Fold `minimum`/`maximum` (partial: None iff a NaN input). `fp.min`/`fp.max` are
+;; unspecified on opposite-sign zeros, where IEEE returns -0/+0.
+(spec (f32_min x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))))
+    (provide (= result
+        (if (and (fp.isZero x) (fp.isZero y) (fp_opposite_sign! x y))
+            (fp.-zero (widthof x))
+            (fp.min x y)))))
+
+(spec (f64_min x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))))
+    (provide (= result
+        (if (and (fp.isZero x) (fp.isZero y) (fp_opposite_sign! x y))
+            (fp.-zero (widthof x))
+            (fp.min x y)))))
+
+(spec (f32_max x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))))
+    (provide (= result
+        (if (and (fp.isZero x) (fp.isZero y) (fp_opposite_sign! x y))
+            (fp.+zero (widthof x))
+            (fp.max x y)))))
+
+(spec (f64_max x y)
+    (match (and (not (fp.isNaN x)) (not (fp.isNaN y))))
+    (provide (= result
+        (if (and (fp.isZero x) (fp.isZero y) (fp_opposite_sign! x y))
+            (fp.+zero (widthof x))
+            (fp.max x y)))))
+
+;; Partial (None on negative/NaN input). `fp.sqrt` is uninterpreted (see
+;; `solver.rs`), so the +inf and zero cases are spelled out.
+(spec (f32_sqrt x)
+    (match (or (fp.isZero x) (fp.isPositive x)))
+    (provide (= result
+        (if (and (fp.isInfinite x) (fp.isPositive x))
+            (fp.+oo (widthof x))
+        (if (fp.isZero x)
+            x
+            (fp.sqrt x))))))
+
+(spec (f64_sqrt x)
+    (match (or (fp.isZero x) (fp.isPositive x)))
+    (provide (= result
+        (if (and (fp.isInfinite x) (fp.isPositive x))
+            (fp.+oo (widthof x))
+        (if (fp.isZero x)
+            x
+            (fp.sqrt x))))))
+
+;; `roundToIntegral` with a directed mode; partial only on NaN input. `fp.ceil`/
+;; etc. are real ops that already handle the inf/zero/small-magnitude cases, so
+;; the bare op suffices.
+(spec (f32_ceil x)    (match (not (fp.isNaN x))) (provide (= result (fp.ceil x))))
+(spec (f64_ceil x)    (match (not (fp.isNaN x))) (provide (= result (fp.ceil x))))
+(spec (f32_floor x)   (match (not (fp.isNaN x))) (provide (= result (fp.floor x))))
+(spec (f64_floor x)   (match (not (fp.isNaN x))) (provide (= result (fp.floor x))))
+(spec (f32_trunc x)   (match (not (fp.isNaN x))) (provide (= result (fp.trunc x))))
+(spec (f64_trunc x)   (match (not (fp.isNaN x))) (provide (= result (fp.trunc x))))
+(spec (f32_nearest x) (match (not (fp.isNaN x))) (provide (= result (fp.nearest x))))
+(spec (f64_nearest x) (match (not (fp.isNaN x))) (provide (= result (fp.nearest x))))
+
+;;;; Concrete int-to-float constant-folds ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Fold `n as f{32,64}` on a 64-bit immediate: convert un/signed to the dest float
+;; width under round-nearest-ties-to-even.
+(spec (f32_from_uint n) (provide (= result (to_fp_unsigned (widthof result) n))))
+(spec (f64_from_uint n) (provide (= result (to_fp_unsigned (widthof result) n))))
+(spec (f32_from_sint n) (provide (= result (to_fp (widthof result) n))))
+(spec (f64_from_sint n) (provide (= result (to_fp (widthof result) n))))
+
+;;;; Generated `u64`/`i64` numeric helpers (`numerics.isle`) ;;;;;;;;;;;;;;;;;;;;;
+;; `gen_isle.rs` primitives on `u64`/`i64` (model as `(bv 64)`); `u64_*` unsigned,
+;; `i64_*` signed. `u64_checked_rem` is partial (None on a zero divisor).
+(spec (u64_and x y) (provide (= result (bvand x y))))
+(spec (u64_or x y) (provide (= result (bvor x y))))
+(spec (u64_not x) (provide (= result (bvnot x))))
+
+;; Byte-reverse the low 16/32/64 bits (`(n as u_).swap_bytes()`).
+(spec (u64_bswap16 n)
+    (provide (= result (zero_ext 64 (concat (extract 7 0 n) (extract 15 8 n))))))
+(spec (u64_bswap32 n)
+    (provide (= result (zero_ext 64 (concat (extract 7 0 n)
+                                    (concat (extract 15 8 n)
+                                    (concat (extract 23 16 n) (extract 31 24 n))))))))
+(spec (u64_bswap64 n)
+    (provide (= result (concat (extract 7 0 n)
+                       (concat (extract 15 8 n)
+                       (concat (extract 23 16 n)
+                       (concat (extract 31 24 n)
+                       (concat (extract 39 32 n)
+                       (concat (extract 47 40 n)
+                       (concat (extract 55 48 n) (extract 63 56 n)))))))))))
+(spec (u64_lt_eq x y) (provide (= result (bvule x y))))
+(spec (u64_checked_rem x y)
+    (match (not (bv_is_zero! y)))
+    (provide (= result (bvurem x y))))
+
+;; Non-partial (panic on zero divisor): `require` non-zero, discharged by the
+;; caller's `u64_checked_rem` guard. Tagged `slow` below (the division rules that
+;; reach them are `unknown` at 64 bits).
+(spec (u64_div x y)
+    (require (not (bv_is_zero! y)))
+    (provide (= result (bvudiv x y))))
+(spec (u64_rem x y)
+    (require (not (bv_is_zero! y)))
+    (provide (= result (bvurem x y))))
+(spec (i64_eq x y) (provide (= result (= x y))))
+(spec (u64_extract_non_zero x)
+    (match (not (bv_is_zero! result)))
+    (provide (= x result)))
+(spec (i64_lt x y) (provide (= result (bvslt x y))))
+(spec (i64_gt_eq x y) (provide (= result (bvsge x y))))
+
+;;;; Type-derived signed bounds ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Signed min/max of `ty` in the low bits: `(i64::{MIN,MAX} as u64) >> (64-bits)`.
+(spec (ty_smin ty)
+    (provide (= result (bvlshr #x8000000000000000 (bvsub (int2bv 64 64) (int2bv 64 (:bits ty)))))))
+(spec (ty_smax ty)
+    (provide (= result (bvlshr #x7fffffffffffffff (bvsub (int2bv 64 64) (int2bv 64 (:bits ty)))))))
+
+;; Partial: half-width integer type (i16->i8, ...); undefined for i8.
+(spec (ty_half_width ty)
+    (match (bvuge (int2bv 64 (:bits ty)) (int2bv 64 16)))
+    (provide (= (int2bv 64 (:bits result)) (bvlshr (int2bv 64 (:bits ty)) (int2bv 64 1)))))
+(spec (ty_equal lhs rhs) (provide (= result (= lhs rhs))))
+
+;; Partial: bit width (8/16/32) -> that integer type.
+(spec (shift_amt_to_type v)
+    (match (or (= v (int2bv 64 8)) (= v (int2bv 64 16)) (= v (int2bv 64 32))))
+    (provide (= (int2bv 64 (:bits result)) v)))
+
+;;;; `imm64_*` min/max/shift folding ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; 64-bit `Imm64`, masked to the low `ty` bits. Signed ops sign-extend those bits
+;; first (Rust `sign_extend_from_width` = shl then ashr by `64-bits`; `sext_ty!`).
+(macro (sext_ty x ty)
+    (bvashr (bvshl x (bvsub (int2bv 64 64) (int2bv 64 (:bits ty))))
+            (bvsub (int2bv 64 64) (int2bv 64 (:bits ty)))))
+(spec (i64_sextend_u64 ty x) (provide (= result (sext_ty! x ty))))
+(spec (imm64_umin ty x y)
+    (provide (= result (if (bvule (bvand x (low_bits_mask! 64 (:bits ty)))
+                                  (bvand y (low_bits_mask! 64 (:bits ty))))
+                           (bvand x (low_bits_mask! 64 (:bits ty)))
+                           (bvand y (low_bits_mask! 64 (:bits ty)))))))
+(spec (imm64_umax ty x y)
+    (provide (= result (if (bvuge (bvand x (low_bits_mask! 64 (:bits ty)))
+                                  (bvand y (low_bits_mask! 64 (:bits ty))))
+                           (bvand x (low_bits_mask! 64 (:bits ty)))
+                           (bvand y (low_bits_mask! 64 (:bits ty)))))))
+(spec (imm64_smin ty x y)
+    (provide (= result (bvand (if (bvsle (sext_ty! x ty) (sext_ty! y ty))
+                                  (sext_ty! x ty) (sext_ty! y ty))
+                              (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_smax ty x y)
+    (provide (= result (bvand (if (bvsge (sext_ty! x ty) (sext_ty! y ty))
+                                  (sext_ty! x ty) (sext_ty! y ty))
+                              (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_sshr ty x y)
+    (provide (= result (bvand (bvashr (sext_ty! x ty)
+                                      (bvand y (bvsub (int2bv 64 (:bits ty)) (int2bv 64 1))))
+                              (low_bits_mask! 64 (:bits ty))))))
+(spec (imm64_masked ty x)
+    (provide (= result (bvand x (low_bits_mask! 64 (:bits ty))))))
+
+;;;; `imm64_*` bit-count / rotate / compare folding ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; `clz` counts leading zeros within `ty` (subtract the `64-bits` offset); `ctz`
+;; is `clz` of the bit-reversed value, or `ty.bits()` for zero. Rotates are shifts.
+(macro (bits ty) (int2bv 64 (:bits ty)))
+(macro (mask ty) (low_bits_mask! 64 (:bits ty)))
+(spec (imm64_clz ty a)
+    (provide (= result (bvsub (clz a) (bvsub (int2bv 64 64) (bits! ty))))))
+(spec (imm64_ctz ty a)
+    (provide (= result (if (bv_is_zero! a) (bits! ty) (clz (rev a))))))
+(spec (imm64_rotl ty x y)
+    (provide (= result
+        (bvand (bvor (bvshl (bvand x (mask! ty)) (bvand y (bvsub (bits! ty) (int2bv 64 1))))
+                     (bvlshr (bvand x (mask! ty))
+                             (bvsub (bits! ty) (bvand y (bvsub (bits! ty) (int2bv 64 1))))))
+               (mask! ty)))))
+(spec (imm64_rotr ty x y)
+    (provide (= result
+        (bvand (bvor (bvlshr (bvand x (mask! ty)) (bvand y (bvsub (bits! ty) (int2bv 64 1))))
+                     (bvshl (bvand x (mask! ty))
+                            (bvsub (bits! ty) (bvand y (bvsub (bits! ty) (int2bv 64 1))))))
+               (mask! ty)))))
+
+;; Fold an integer compare to `1`/`0`: unsigned codes on the masked values, signed
+;; codes on the sign-extended ones.
+(spec (imm64_icmp ty cc x y)
+    (provide (= result
+        (if (match cc
+                ((Equal) (= (bvand x (mask! ty)) (bvand y (mask! ty))))
+                ((NotEqual) (not (= (bvand x (mask! ty)) (bvand y (mask! ty)))))
+                ((UnsignedGreaterThan) (bvugt (bvand x (mask! ty)) (bvand y (mask! ty))))
+                ((UnsignedGreaterThanOrEqual) (bvuge (bvand x (mask! ty)) (bvand y (mask! ty))))
+                ((UnsignedLessThan) (bvult (bvand x (mask! ty)) (bvand y (mask! ty))))
+                ((UnsignedLessThanOrEqual) (bvule (bvand x (mask! ty)) (bvand y (mask! ty))))
+                ((SignedGreaterThan) (bvsgt (sext_ty! x ty) (sext_ty! y ty)))
+                ((SignedGreaterThanOrEqual) (bvsge (sext_ty! x ty) (sext_ty! y ty)))
+                ((SignedLessThan) (bvslt (sext_ty! x ty) (sext_ty! y ty)))
+                ((SignedLessThanOrEqual) (bvsle (sext_ty! x ty) (sext_ty! y ty))))
+            (int2bv 64 1) (int2bv 64 0)))))
+
+;; Partial extractor: matches a positive power-of-two (`result`) and yields its
+;; log2 (`x` = trailing-zero count).
+(spec (imm64_power_of_two x)
+    (match (and (bvsge result (int2bv 64 0))
+                (not (bv_is_zero! result))
+                (bv_is_zero! (bvand result (bvsub result (int2bv 64 1))))))
+    (provide (= x (clz (rev result)))))
+
+;;;; Condition-code helpers ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; `IntCC::complement` (negate) / `IntCC::swap_args` (swap operands), per
+;; `ir/condcodes.rs`.
+(spec (intcc_complement cc)
+    (provide (= result
+        (match cc
+            ((Equal) (IntCC.NotEqual))
+            ((NotEqual) (IntCC.Equal))
+            ((SignedLessThan) (IntCC.SignedGreaterThanOrEqual))
+            ((SignedGreaterThanOrEqual) (IntCC.SignedLessThan))
+            ((SignedGreaterThan) (IntCC.SignedLessThanOrEqual))
+            ((SignedLessThanOrEqual) (IntCC.SignedGreaterThan))
+            ((UnsignedLessThan) (IntCC.UnsignedGreaterThanOrEqual))
+            ((UnsignedGreaterThanOrEqual) (IntCC.UnsignedLessThan))
+            ((UnsignedGreaterThan) (IntCC.UnsignedLessThanOrEqual))
+            ((UnsignedLessThanOrEqual) (IntCC.UnsignedGreaterThan))))))
+(spec (intcc_swap_args cc)
+    (provide (= result
+        (match cc
+            ((Equal) (IntCC.Equal))
+            ((NotEqual) (IntCC.NotEqual))
+            ((SignedGreaterThan) (IntCC.SignedLessThan))
+            ((SignedGreaterThanOrEqual) (IntCC.SignedLessThanOrEqual))
+            ((SignedLessThan) (IntCC.SignedGreaterThan))
+            ((SignedLessThanOrEqual) (IntCC.SignedGreaterThanOrEqual))
+            ((UnsignedGreaterThan) (IntCC.UnsignedLessThan))
+            ((UnsignedGreaterThanOrEqual) (IntCC.UnsignedLessThanOrEqual))
+            ((UnsignedLessThan) (IntCC.UnsignedGreaterThan))
+            ((UnsignedLessThanOrEqual) (IntCC.UnsignedGreaterThanOrEqual))))))
+
+;; `intcc_class`: class bitset (unsigned=1, signed=2, eq=3). `intcc_comparable`
+;; succeeds when the classes overlap and yields whether the overlap is the signed
+;; bit. Inlined via `icc_class!` since a spec can't call the `intcc_class` term.
+(macro (icc_class cc)
+    (match cc
+        ((UnsignedLessThan) (int2bv 64 1))
+        ((UnsignedLessThanOrEqual) (int2bv 64 1))
+        ((UnsignedGreaterThan) (int2bv 64 1))
+        ((UnsignedGreaterThanOrEqual) (int2bv 64 1))
+        ((SignedLessThan) (int2bv 64 2))
+        ((SignedLessThanOrEqual) (int2bv 64 2))
+        ((SignedGreaterThan) (int2bv 64 2))
+        ((SignedGreaterThanOrEqual) (int2bv 64 2))
+        ((Equal) (int2bv 64 3))
+        ((NotEqual) (int2bv 64 3))))
+(spec (intcc_class cc) (provide (= result (icc_class! cc))))
+(spec (intcc_comparable cc1 cc2)
+    (match (not (bv_is_zero! (bvand (icc_class! cc1) (icc_class! cc2)))))
+    (provide (= result (= (bvand (icc_class! cc1) (icc_class! cc2)) (int2bv 64 2)))))
+
+;; `decompose_intcc`: per-condition tag (eq=1, lt=2, le=3, gt=4, ge=5, ne=6).
+;; `compose_icmp`: the inverse -- tag `v` (0=const-false, 7=const-true, else the
+;; matching icmp) with a `signed` flag. Power the `band`/`bor`-of-icmp rules.
+(spec (decompose_intcc cc)
+    (provide (= result
+        (match cc
+            ((Equal) (int2bv 64 1))
+            ((UnsignedLessThan) (int2bv 64 2))
+            ((SignedLessThan) (int2bv 64 2))
+            ((UnsignedLessThanOrEqual) (int2bv 64 3))
+            ((SignedLessThanOrEqual) (int2bv 64 3))
+            ((UnsignedGreaterThan) (int2bv 64 4))
+            ((SignedGreaterThan) (int2bv 64 4))
+            ((UnsignedGreaterThanOrEqual) (int2bv 64 5))
+            ((SignedGreaterThanOrEqual) (int2bv 64 5))
+            ((NotEqual) (int2bv 64 6))))))
+(macro (icmp_bit c) (if c #x01 #x00))
+(spec (compose_icmp ty v signed x y)
+    (provide (= result
+        (if (= v (int2bv 64 0)) #x00
+        (if (= v (int2bv 64 1)) (icmp_bit! (= x y))
+        (if (= v (int2bv 64 2)) (icmp_bit! (if signed (bvslt x y) (bvult x y)))
+        (if (= v (int2bv 64 3)) (icmp_bit! (if signed (bvsle x y) (bvule x y)))
+        (if (= v (int2bv 64 4)) (icmp_bit! (if signed (bvsgt x y) (bvugt x y)))
+        (if (= v (int2bv 64 5)) (icmp_bit! (if signed (bvsge x y) (bvuge x y)))
+        (if (= v (int2bv 64 6)) (icmp_bit! (not (= x y)))
+        #x01))))))))))
+
+;; Reached only at `ty = I8` (icmp results are `(bv 8)`), so all operands/result bv8.
+(instantiate compose_icmp
+    ((args (named Type) (bv 64) Bool (bv 8) (bv 8)) (ret (bv 8))))
+
+;;;; Bit-manipulation instructions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; `bitrev` = `rev`. `bmask` broadcasts truthiness to an all-ones/all-zeros mask of
+;; the (possibly different-width) result type.
+(spec (bitrev ty x)
+    (provide (= result (rev x)) (= (:bits ty) (widthof result))))
+(instantiate bitrev bv_unary_8_to_64)
+(spec (bmask ty v)
+    (provide (= result (if (bv_is_zero! v) (bvzero! (widthof result)) (bvones! (widthof result))))
+             (= (:bits ty) (widthof result))))
+(instantiate bmask
+    ((args (named Type) (bv  8)) (ret (bv  8)))
+    ((args (named Type) (bv  8)) (ret (bv 16)))
+    ((args (named Type) (bv  8)) (ret (bv 32)))
+    ((args (named Type) (bv  8)) (ret (bv 64)))
+    ((args (named Type) (bv 16)) (ret (bv  8)))
+    ((args (named Type) (bv 16)) (ret (bv 16)))
+    ((args (named Type) (bv 16)) (ret (bv 32)))
+    ((args (named Type) (bv 16)) (ret (bv 64)))
+    ((args (named Type) (bv 32)) (ret (bv  8)))
+    ((args (named Type) (bv 32)) (ret (bv 16)))
+    ((args (named Type) (bv 32)) (ret (bv 32)))
+    ((args (named Type) (bv 32)) (ret (bv 64)))
+    ((args (named Type) (bv 64)) (ret (bv  8)))
+    ((args (named Type) (bv 64)) (ret (bv 16)))
+    ((args (named Type) (bv 64)) (ret (bv 32)))
+    ((args (named Type) (bv 64)) (ret (bv 64))))
+
+;;;; Spaceship helpers (declared in `prelude_opt.isle`) ;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; `spaceship_s`/`spaceship_u ty x y` are `isub $I8 (sgt/ugt ty x y) (slt/ult ty x
+;; y))` three-way comparisons resulting in an `i8` (`1`/`0`/`-1`).  Result is
+;; `(bv 8)`; the operands have width `ty`.
+(spec (spaceship_s ty x y)
+    (provide (= result (bvsub (if (bvsgt x y) #x01 #x00) (if (bvslt x y) #x01 #x00)))))
+(spec (spaceship_u ty x y)
+    (provide (= result (bvsub (if (bvugt x y) #x01 #x00) (if (bvult x y) #x01 #x00)))))
+(instantiate spaceship_s comparison)
+(instantiate spaceship_u comparison)
+
+;;;; Chaining ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(attr iadd_uextend (veri chain))
+(attr isub_uextend (veri chain))
+(attr truthy (veri chain))
+
+;;;; Coverage-gap tags ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(attr multi_lane (tag vector))
+(attr ty_int_vec128 (tag vector))
+(attr fma (tag vector))
+(attr iconcat (tag i128))
+(attr f16const (tag narrowfloat))
+(attr ieee128_constant (tag i128))
+
+;; `make_inst` builds a pure node from an `InstructionData`, so every expansion
+;; that verifies an instruction's own *constructor body* (rather than using its
+;; spec as a leaf) reaches it. The verifier has no model for `InstructionData`
+;; or its `ValueArray2`/`ValueArray3` argument arrays, so those expansions fail
+;; with "unspecified model for type `ValueArray2`/`ValueArray3`". No verified
+;; `simplify` expansion reaches `make_inst` (rewrite rules use instruction specs
+;; as leaves), so tagging it excludes exactly the un-modelable construction
+;; expansions.
+(attr make_inst (tag TODO))
+
+;; Slow/unknown
+(attr u64_div (tag slow))
+(attr u64_rem (tag slow))
+(attr rule imul_ineg_const (tag slow))
diff --git a/cranelift/codegen/src/spec/prelude_lower_spec.isle b/cranelift/codegen/src/spec/prelude_lower_spec.isle
new file mode 100644
index 000000000000..8df726952377
--- /dev/null
+++ b/cranelift/codegen/src/spec/prelude_lower_spec.isle
@@ -0,0 +1,15 @@
+;; Specs for terms declared in `prelude_lower.isle`, i.e. terms that exist only
+;; in the lowering compilations and not in the mid-end `opt` compilation. Kept
+;; separate from the shared `inst_specs.isle` so that every spec in that file
+;; targets a term present in *all* compilations, and the verifier's
+;; unknown-term check stays a useful linter against stale specs.
+
+;; `maybe_uextend` "sees through" a `uextend`: given the outer value `result`,
+;; it yields the inner value `value`. When `result` is defined by a `uextend`,
+;; `value` is that uextend's argument; otherwise `value` is `result` itself. In
+;; both cases the inner value is the low bits of the outer value, i.e. the outer
+;; value is the zero-extension of the inner one to the outer width (in the
+;; fall-through case the two widths are equal, so this is the identity). The
+;; extractor is total (it always matches), so no `match` clause is needed.
+(spec (maybe_uextend value)
+    (provide (= result (zero_ext (widthof result) value))))
diff --git a/cranelift/codegen/src/spec/prelude_spec.isle b/cranelift/codegen/src/spec/prelude_spec.isle
index c9c5266e02ab..271b6a8a160f 100644
--- a/cranelift/codegen/src/spec/prelude_spec.isle
+++ b/cranelift/codegen/src/spec/prelude_spec.isle
@@ -80,3 +80,22 @@
 
 ; Bit-vector with the sign bit set.
 (macro (fp_sign_bit_set w) (bvshl_int! (bvone! w) (fp_sign_bit! w)))
+
+; Whether a floating-point value is an *arithmetic* NaN: a NaN with the top
+; fraction bit set. CLIF/Wasm arithmetic operations that return a NaN must
+; return an arithmetic NaN, but its sign and remaining payload bits are
+; nondeterministic.
+;
+; An arithmetic NaN is exactly a value whose exponent is all ones and whose top
+; fraction bit is set (which also implies a nonzero mantissa, so it is a NaN
+; rather than an infinity). Those are precisely the bits set in the positive
+; canonical NaN, so the test is `(x & nan_canon) == nan_canon`. Expressed purely
+; in the bit-vector theory (no `fp.isNaN`) so the solver need not bridge the
+; floating-point and bit-vector theories.
+(macro (is_arith_nan x)
+    (= (bvand x (nan_canon! (widthof x))) (nan_canon! (widthof x))))
+
+; CLIF-level floating-point value equivalence. Two results are equivalent if
+; they are bitwise equal, or both are arithmetic NaNs.
+(macro (fp_equiv a b)
+    (or (= a b) (and (is_arith_nan! a) (is_arith_nan! b))))
diff --git a/cranelift/isle/veri/README.md b/cranelift/isle/veri/README.md
index 96c3220df518..3fd879daeebb 100644
--- a/cranelift/isle/veri/README.md
+++ b/cranelift/isle/veri/README.md
@@ -143,6 +143,127 @@ cargo run -p cranelift-isle-veri --bin veri -- --name x64 --rule iadd_base_case_
 Here, `--name` specifies the ISLE compilation unit name, and `iadd_base_case_32_or_64_lea` scopes to a single
 `lower` rule.
 
+## Running for the mid-end (`opt`)
+
+The mid-end optimization (`opt`) rules can be verified with the same tool using
+`--name opt` (for the `opt`imization compilation unit). The mid-end rules rewrite CLIF values
+primarily via the `simplify` term. There are also `simplify_skeleton` rules, but support for those
+has not yet been added.
+
+For most chains of `simplify` rules, the soundness condition is that the
+rewritten value is equivalent to the original (floating point rules are the exception, as detailed below).
+
+To verify a specific rule, such as the `x + 0 == x` rewrite in `cranelift/codegen/src/opts/arithmetic.isle`, name
+the rule:
+
+```
+;; x+0 == x.
+(rule iadd_x_plus_zero (simplify (iadd ty x (iconst_u ty 0)))
+      (subsume x))
+```
+
+and run:
+
+```
+cargo run -p cranelift-isle-veri --bin veri -- --name opt --rule iadd_x_plus_zero
+```
+
+This verifies the rule across the monomorphized integer types (`i8`, `i16`, `i32`, `i64`):
+
+```
+Type instantiations: 4
+Applicable:          4
+Verification passed: 4
+```
+
+Specs for the mid-end helper terms live in
+[`cranelift/codegen/src/spec/opt.isle`](../../codegen/src/spec/opt.isle).
+This is where the `simplify` soundness contract is stated (`result == arg`,
+relaxed to floating-point equivalence for NaN-producing rewrites; see
+[Floating-point rewrites](#floating-point-rewrites) below),
+along with specs for relevant helpers.
+Most helper terms are verified by rule chaining; the `iconst_u`/`iconst_s`
+helpers are recursive and thus cyclic, so they have explicit hand-written specs.
+Other terms with external extractors also have hand-written specs.
+
+### Floating-point rewrites
+
+Floating-point `simplify` rules need a weaker soundness contract than integer
+rules. A CLIF floating-point *arithmetic* operation that produces a NaN may
+return *any* arithmetic NaN (any sign and payload with the top fraction bit set),
+so a rewrite that yields a different NaN bit pattern is still correct; requiring
+exact bitwise equality (`result == arg`) wrongly rejects sound rules.
+
+This is modeled with the same execution-state mechanism as traps (see the
+`(state ...)`/`(modifies ...)` forms in `inst_specs.isle`), so it lives entirely
+in the specs with no special case in the verifier. A `relax_nan` state flag
+defaults to false; each floating-point arithmetic op (`fadd`/`fsub`/`fmul`/
+`fdiv`/`sqrt`/`fmin`/`fmax`/...) declares `(modifies relax_nan ...)` and sets it
+true exactly when it produces a NaN. Deterministic bit-operations (`fneg`/
+`fabs`/`fcopysign`) leave it alone. The `simplify` contract then reads the flag:
+
+```
+(if relax_nan (fp_equiv! result arg) (= result arg))
+```
+
+where `fp_equiv` holds when the two values are bitwise equal *or* both arithmetic
+NaNs. So a rewrite is checked for exact equality unless one of its values came
+from a NaN-producing arithmetic op, in which case NaN payload differences are
+allowed.
+
+For example, `(fmul (fneg x) (fneg y)) => (fmul x y)` is sound only under this
+relaxation: when `x` or `y` is a NaN the two sides produce NaNs of different
+sign. Verify it with:
+
+```
+cargo run -p cranelift-isle-veri --bin veri -- --name opt --rule fmul_fneg_fneg
+```
+
+```
+Type instantiations: 2
+Applicable:          2
+Verification passed: 2
+```
+
+#### Caveat: relaxation assumes float-typed results
+
+`relax_nan` is a single execution-state flag, not a per-value property, and
+`fp_equiv!` interprets the bits of both values as floats. The relaxation is
+therefore only sound when the rewritten value really is float-typed. It matches
+Wasm semantics for the current rules, which all compose float operations into a
+float result.
+
+It could become unsound for a future rule that computes on floats but discards
+the float result in favor of returning e.g. an integer. A NaN-producing arithmetic
+op anywhere in the expansion sets `relax_nan`, so `simplify` would check the
+integer-typed result with `fp_equiv!` and wrongly accept two integers whose bit
+patterns merely both happen to look like arithmetic NaNs, even though the integer
+values differ. In practice, such a rule would also be incorrect on other integer
+bitpatterns that do not look like an arithmetic NaN, so the rule would fail on those
+counterexamples.
+
+### Running the whole mid-end suite
+
+To sweep every mid-end rewrite in one run, seed from `simplify` and apply the
+default excludes (see [above](#verifying-a-family-of-rules-at-once) for why these
+flags are needed):
+
+```
+cargo run -p cranelift-isle-veri --bin veri -- --name opt --only-root simplify --default-excludes
+```
+
+On a 12-core M2 MacBook this takes under two minutes:
+
+```
+Total expansions:    1312
+In scope expansions: 1040
+Type instantiations: 4064
+Applicable:          4058
+Verification passed: 4058
+Verification failed: 0
+Verification unknown: 0
+```
+
 ## ISA Specifications
 
 Where possible, we derive ISA specifications in VeriISLE format from
diff --git a/cranelift/isle/veri/veri/src/debug.rs b/cranelift/isle/veri/veri/src/debug.rs
index f5c3a00ac451..8e3c7eb501e8 100644
--- a/cranelift/isle/veri/veri/src/debug.rs
+++ b/cranelift/isle/veri/veri/src/debug.rs
@@ -285,7 +285,7 @@ pub fn binding_string(
             source = source.index(),
             field = field.index()
         ),
-        Binding::Iterator { .. } => unimplemented!("iterator bindings unsupported"),
+        Binding::Iterator { source } => format!("iterator({source})", source = source.index()),
     }
 }
 
diff --git a/cranelift/isle/veri/veri/src/expand.rs b/cranelift/isle/veri/veri/src/expand.rs
index a96e268bbfa9..3dbc0ff56710 100644
--- a/cranelift/isle/veri/veri/src/expand.rs
+++ b/cranelift/isle/veri/veri/src/expand.rs
@@ -213,6 +213,28 @@ impl Expansion {
 
         // Result.
         self.result = reindex.id(self.result);
+
+        // Equals.
+        //
+        // Rebuild the equality sets with the reindex applied, so that the
+        // deleted `target` binding is replaced by `replace`. Without this, a
+        // deleted binding can linger in the disjoint set (possibly as a set
+        // representative), and `equalities()` would later return a reference to
+        // a binding that no longer exists.
+        let mut equals = DisjointSets::default();
+        for i in 0..self.bindings.len() {
+            let binding_id = i.try_into().unwrap();
+            if let Some(eq) = self.equals.find(binding_id)
+                && eq != binding_id
+            {
+                let a = reindex.id(binding_id);
+                let b = reindex.id(eq);
+                if a != b {
+                    equals.merge(a, b);
+                }
+            }
+        }
+        self.equals = equals;
     }
 }
 
@@ -884,7 +906,9 @@ impl Reindex {
                 field: *field,
             },
 
-            Binding::Iterator { .. } => unimplemented!("iterator bindings not supported"),
+            Binding::Iterator { source } => Binding::Iterator {
+                source: self.id(*source),
+            },
         }
     }
 }
diff --git a/cranelift/isle/veri/veri/src/trie.rs b/cranelift/isle/veri/veri/src/trie.rs
index 0f9136b465d4..23f574ead1a9 100644
--- a/cranelift/isle/veri/veri/src/trie.rs
+++ b/cranelift/isle/veri/veri/src/trie.rs
@@ -153,7 +153,12 @@ pub fn binding_type(
             }
         }
 
-        Binding::Iterator { .. } => unimplemented!("iterator bindings not supported"),
+        Binding::Iterator { source } => {
+            // The yielded element has the source term's element type, which we
+            // model as its (single) return type.
+            let source_binding = lookup_binding(*source);
+            binding_type(&source_binding, term_id, prog, lookup_binding)
+        }
     }
 }
 
@@ -169,6 +174,8 @@ fn external_sig_return_type(sig: &ExternalSig) -> BindingType {
     match sig.ret_kind {
         ReturnKind::Option => BindingType::Option(Box::new(ty)),
         ReturnKind::Plain => ty,
-        ReturnKind::Iterator => unimplemented!("extractor iterator return"),
+        // Model an iterator term as producing a single element of `ty`, which
+        // `Binding::Iterator` then picks out.
+        ReturnKind::Iterator => ty,
     }
 }
diff --git a/cranelift/isle/veri/veri/src/veri.rs b/cranelift/isle/veri/veri/src/veri.rs
index 308a2e786241..80030ba76ef5 100644
--- a/cranelift/isle/veri/veri/src/veri.rs
+++ b/cranelift/isle/veri/veri/src/veri.rs
@@ -1127,7 +1127,7 @@ impl<'a> ConditionsBuilder<'a> {
                 term, parameters, ..
             } => self.constructor(id, *term, parameters, Invocation::Caller),
 
-            Binding::Iterator { .. } => unimplemented!("iterator bindings"),
+            Binding::Iterator { source } => self.iterator(id, *source),
 
             Binding::MakeVariant {
                 ty,
@@ -1630,6 +1630,16 @@ impl<'a> ConditionsBuilder<'a> {
         Ok(())
     }
 
+    fn iterator(&mut self, id: BindingId, source: BindingId) -> Result<()> {
+        // We model the multi-term as producing exactly one value, so the
+        // yielded element equals the source value.
+        let source = self.binding_value[&source].clone();
+        let v = self.binding_value[&id].clone();
+        let eq = self.values_equal(v, source)?;
+        self.conditions.assumptions.push(eq);
+        Ok(())
+    }
+
     fn constrain(&mut self, constrain: &Constrain) -> Result<ExprId> {
         match constrain {
             Constrain::Match(binding_id, constraint) => self.constraint(*binding_id, constraint),
@@ -1917,7 +1927,15 @@ impl<'a> ConditionsBuilder<'a> {
             })),
             Type::Int => Ok(self.constant(Const::Int(val))),
             Type::BitVector(Width::Bits(w)) => {
-                Ok(self.constant(Const::BitVector(*w, val.try_into()?)))
+                // Two's-complement bit pattern of the given width; masking
+                // handles negative literals (e.g. `-1`), unlike a `u64` cast.
+                let mask: u128 = if *w >= 128 {
+                    u128::MAX
+                } else {
+                    (1u128 << w) - 1
+                };
+                let bits = (val as u128) & mask;
+                Ok(self.constant(Const::BitVector(*w, bits.into())))
             }
             _ => bail!("cannot construct constant of type {ty}"),
         }