Merge c49b403922 into 477a1d817d

.github/workflows/fstar-extract.yml

@@ -0,0 +1,96 @@
+name: "F* Meta Extraction"
+
+# Run the Meta-F* reflection-based extraction that generates C++ rewrite rules
+# from the F* lemmas in fstar/FPARewriterRules.fst.
+#
+# The extraction is performed by fstar/RewriteCodeGen.fst which uses
+# FStar.Tactics.V2 and FStar.Reflection.V2 to inspect the lemma types
+# and emit C++ if-blocks that implement the corresponding rewrite rules.
+#
+# The generated C++ is printed to the job log and uploaded as an artifact.
+
+on:
+  push:
+    paths:
+      - "fstar/**.fst"
+      - "fstar/extract.sh"
+      - ".github/workflows/fstar-extract.yml"
+  pull_request:
+    paths:
+      - "fstar/**.fst"
+      - "fstar/extract.sh"
+      - ".github/workflows/fstar-extract.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  fstar-extract:
+    name: "Meta-F* rewrite rule extraction"
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6.0.2
+
+      # -----------------------------------------------------------------------
+      # Install F*
+      #
+      # We download the pre-built Linux binary from the F* GitHub releases.
+      # The version is pinned to match what the README recommends.
+      # If the pinned release is unavailable the step fails clearly.
+      # -----------------------------------------------------------------------
+      - name: Install F*
+        env:
+          FSTAR_VERSION: "2026.03.24"
+        run: |
+          ARCHIVE="fstar-v${FSTAR_VERSION}-Linux-x86_64.tar.gz"
+          URL="https://github.com/FStarLang/FStar/releases/download/v${FSTAR_VERSION}/${ARCHIVE}"
+          echo "Downloading F* ${FSTAR_VERSION} from ${URL}" >&2
+          curl -fsSL -o "/tmp/${ARCHIVE}" "${URL}"
+          # The F* 2026 archive has structure: ./fstar/bin/fstar.exe
+          # --strip-components=2 removes both './' and 'fstar/' so that
+          # bin/fstar.exe lands directly in $HOME/fstar/bin/fstar.exe.
+          mkdir -p "$HOME/fstar"
+          tar -xzf "/tmp/${ARCHIVE}" -C "$HOME/fstar" --strip-components=2
+          echo "$HOME/fstar/bin" >> "$GITHUB_PATH"
+
+      - name: Verify F* installation
+        run: fstar.exe --version
+
+      # -----------------------------------------------------------------------
+      # Run the Meta-F* extraction
+      #
+      # RewriteCodeGen.fst contains run_tactic calls that print generated C++
+      # to stdout during typechecking.  We capture that output, show it in the
+      # log, and upload it as an artifact for inspection.
+      # -----------------------------------------------------------------------
+      - name: Extract C++ rewrite rules via Meta-F*
+        working-directory: fstar
+        run: |
+          chmod +x extract.sh
+          echo "--- generated C++ rules ---"
+          ./extract.sh | tee extracted_rules.txt
+          echo "--- end of generated rules ---"
+
+      - name: Show extracted rules
+        working-directory: fstar
+        run: |
+          echo "Lines of generated C++ output:"
+          wc -l extracted_rules.txt
+          echo ""
+          echo "Full content:"
+          cat extracted_rules.txt
+
+      # -----------------------------------------------------------------------
+      # Upload the extracted rules as a build artifact so reviewers can
+      # inspect the generated C++ without re-running the workflow.
+      # -----------------------------------------------------------------------
+      - name: Upload extracted rules artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: fstar-extracted-cpp-rules
+          path: fstar/extracted_rules.txt
+          if-no-files-found: error

fstar/FPARewriterRules.fst

@@ -0,0 +1,420 @@
+(*
+  FPARewriterRules.fst
+
+  Formalization of the floating-point rewrite rules introduced in
+  Z3 PR #9038 ("fix #8185: add FPA rewriter simplifications for fma
+  with zero multiplicand and classification of int-to-float conversions").
+
+  The PR adds three families of optimizations to fpa_rewriter.cpp:
+
+    1. fma(rm, ±0, y, z): zero-multiplicand decomposition.
+       Instead of bit-blasting the full FMA circuit, decompose into
+       a cheaper fp_add when one multiplicand is a concrete zero.
+
+    2. isNaN/isInf/isNormal applied to to_fp(rm, to_real(int_expr)):
+       replace with pure integer/arithmetic constraints.
+
+    3. Push isNaN/isInf/isNormal through ite when both branches are
+       concrete FP numerals.
+
+  Each lemma below states and proves (from the axioms in IEEE754.fst)
+  the mathematical content of the corresponding C++ simplification.
+  The preconditions mirror the guards checked by the C++ rewriter before
+  applying each rewrite.
+
+  Naming convention:
+    lemma_fma_*        — Section 1, FMA with zero multiplicand
+    lemma_is_nan_*     — Section 2a, isNaN of integer-to-float
+    lemma_is_inf_*     — Section 2b, isInf  of integer-to-float
+    lemma_is_normal_*  — Section 2c, isNormal of integer-to-float
+    lemma_*_ite        — Section 3, classification through ite
+*)
+
+module FPARewriterRules
+
+open IEEE754
+
+(* ================================================================== *)
+(* Section 1: FMA with a Zero Multiplicand                            *)
+(*                                                                     *)
+(* C++ location: fpa_rewriter.cpp, mk_fma, new block after line 428   *)
+(*                                                                     *)
+(* When arg2 (or arg3) is a concrete ±0, the rewriter avoids          *)
+(* building the full FMA bit-blast circuit.  The simplifications       *)
+(* below correspond to each branch in the C++ code.                   *)
+(*                                                                     *)
+(* We formalize fma(rm, ±0, y, z); the symmetric case                 *)
+(* fma(rm, x, ±0, z) follows by the same argument with x and y        *)
+(* swapped (fp_mul is commutative for sign and NaN-propagation         *)
+(* purposes; a separate symmetric set of axioms could be added).      *)
+(* ================================================================== *)
+
+(* 1a.  fma(rm, ±0, y, NaN) = NaN
+        Source: C++ fpa_rewriter.cpp, mk_fma, branch "if (m_util.is_nan(arg4))".
+        The addend NaN propagates (IEEE 754-2019 §6.2, NaN payload rules).
+        [extract: FPA_REWRITE_FMA_ZERO_MUL, case (a)] *)
+let lemma_fma_zero_nan_addend
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y: float eb sb)
+    : Lemma (requires is_zero zero_val = true)
+            (ensures  is_nan (fp_fma rm zero_val y (nan #eb #sb)) = true) =
+  ax_fma_nan_z rm zero_val y
+
+
+(* 1b.  fma(rm, ±0, NaN, z) = NaN
+        Source: C++ check "m_fm.is_nan(vo)" for other_mul.
+        NaN in the second multiplicand propagates regardless of the addend.
+        [extract: FPA_REWRITE_FMA_ZERO_MUL, case (b)] *)
+let lemma_fma_zero_nan_mul
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val z: float eb sb)
+    : Lemma (requires is_zero zero_val = true)
+            (ensures  is_nan (fp_fma rm zero_val (nan #eb #sb) z) = true) =
+  ax_fma_nan_y rm zero_val z
+
+
+(* 1c.  fma(rm, ±0, ±∞, z) = NaN
+        Source: C++ check "m_fm.is_inf(vo)" for other_mul.
+        0 * ∞ is the "invalid operation" NaN (IEEE 754-2019 §7.2),
+        which then propagates through the addition.
+        [extract: FPA_REWRITE_FMA_ZERO_MUL, case (b)] *)
+let lemma_fma_zero_inf_mul
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val inf_val z: float eb sb)
+    : Lemma (requires is_zero zero_val = true && is_inf inf_val = true)
+            (ensures  is_nan (fp_fma rm zero_val inf_val z) = true) =
+  ax_zero_mul_inf rm zero_val inf_val;
+  ax_fma_nan_mul  rm zero_val inf_val z
+
+
+(* 1d.  fma(rm, ±0, y_finite, z) = fp_add(rm, fp_mul(rm, ±0, y_finite), z)
+        Source: C++ branch "m_util.is_numeral(other_mul, vo)" (concrete finite).
+        ±0 * finite = ±0 exactly (IEEE 754-2019 §6.3), so fma reduces to
+        an addition whose first operand is the computed ±0 product.
+
+        This is the key decomposition that replaces the expensive FMA
+        circuit with a cheaper addition.
+        [extract: FPA_REWRITE_FMA_ZERO_MUL, case (c)] *)
+let lemma_fma_zero_finite_decomposes
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y z: float eb sb)
+    : Lemma (requires is_zero zero_val = true && is_finite y = true)
+            (ensures  fp_fma rm zero_val y z =
+                      fp_add rm (fp_mul rm zero_val y) z &&
+                      is_zero (fp_mul rm zero_val y) = true) =
+  ax_fma_zero_finite rm zero_val y z
+
+
+(* 1e.  fma(rm, ±0, y_finite, z_nonzero_finite) = z_nonzero_finite
+        Source: C++ branch with "m_util.is_numeral(arg4, vz) && !m_fm.is_zero(vz)"
+        and a concrete finite other_mul.
+        When z is nonzero and finite, ±0 + z = z exactly under any rounding
+        mode (IEEE 754-2019 §6.3), so the entire fma collapses to z.
+        [extract: FPA_REWRITE_FMA_ZERO_MUL, case (c) folded with ax_add_zero_nonzero] *)
+let lemma_fma_zero_const_addend
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y z: float eb sb)
+    : Lemma (requires is_zero zero_val = true &&
+                      is_finite y      = true &&
+                      is_finite z      = true &&
+                      is_zero z        = false)
+            (ensures  fp_fma rm zero_val y z = z) =
+  ax_fma_zero_finite  rm zero_val y z;
+  ax_add_zero_nonzero rm (fp_mul rm zero_val y) z
+
+
+(* 1f.  Symbolic y, concrete nonzero non-NaN z:
+          fma(rm, ±0, y, z_const) =
+            ite(¬isNaN(y) ∧ ¬isInf(y),   z_const,   NaN)
+        Source: C++ branch producing "m().mk_ite(finite_cond, arg4, nan)".
+        We prove each arm of the ite separately.
+        [extract: FPA_REWRITE_FMA_ZERO_MUL, case (d)]
+
+        Finite arm: y is finite → fma = z_const (by 1e). *)
+let lemma_fma_zero_const_finite_arm
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y z: float eb sb)
+    : Lemma (requires is_zero zero_val = true &&
+                      is_finite y      = true &&
+                      is_finite z      = true &&
+                      is_zero z        = false)
+            (ensures  fp_fma rm zero_val y z = z) =
+  lemma_fma_zero_const_addend rm zero_val y z
+
+(* NaN-or-inf arm: y is NaN or ∞ → fma = NaN. *)
+let lemma_fma_zero_const_nan_inf_arm
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y z: float eb sb)
+    : Lemma (requires is_zero zero_val = true &&
+                      (is_nan y = true || is_inf y = true))
+            (ensures  is_nan (fp_fma rm zero_val y z) = true) =
+  if is_nan y = true then
+    ax_fma_any_nan_y rm zero_val y z
+  else begin
+    ax_zero_mul_inf rm zero_val y;
+    ax_fma_nan_mul  rm zero_val y z
+  end
+
+
+(* 1g.  General case — symbolic y and z:
+          fma(rm, ±0, y, z) =
+            ite(is_finite(y),  fp_add(rm, product_zero, z),  NaN)
+        Source: C++ block producing the final ite with product_zero.
+        product_zero is ±0 with sign = sign(±0) XOR sign(y).
+        We prove each arm.
+        [extract: FPA_REWRITE_FMA_ZERO_MUL, case (e)] *)
+
+(* Finite arm: fma = fp_add(rm, fp_mul(rm, ±0, y), z). *)
+let lemma_fma_zero_general_finite_arm
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y z: float eb sb)
+    : Lemma (requires is_zero zero_val = true && is_finite y = true)
+            (ensures  fp_fma rm zero_val y z =
+                      fp_add rm (fp_mul rm zero_val y) z &&
+                      is_zero (fp_mul rm zero_val y) = true) =
+  ax_fma_zero_finite rm zero_val y z
+
+(* NaN-or-inf arm: fma = NaN. *)
+let lemma_fma_zero_general_nan_inf_arm
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y z: float eb sb)
+    : Lemma (requires is_zero zero_val = true &&
+                      (is_nan y = true || is_inf y = true))
+            (ensures  is_nan (fp_fma rm zero_val y z) = true) =
+  if is_nan y = true then
+    ax_fma_any_nan_y rm zero_val y z
+  else begin
+    ax_zero_mul_inf rm zero_val y;
+    ax_fma_nan_mul  rm zero_val y z
+  end
+
+(* Sign of the zero product (IEEE 754-2019 §6.3):
+   sign(fp_mul(rm, ±0, y)) = sign(±0) XOR sign(y) for finite nonzero y. *)
+let lemma_fma_zero_product_sign
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y: float eb sb)
+    : Lemma (requires is_zero zero_val = true &&
+                      is_finite y      = true &&
+                      is_zero y        = false)
+            (ensures  (let p = fp_mul rm zero_val y in
+                       is_zero p = true &&
+                       (is_negative p =
+                         ((is_negative zero_val && not (is_negative y)) ||
+                          (not (is_negative zero_val) && is_negative y))))) =
+  ax_zero_mul_sign rm zero_val y
+
+
+(* ================================================================== *)
+(* Section 2: Classification of Integer-to-Float Conversions          *)
+(*                                                                     *)
+(* C++ location: fpa_rewriter.cpp, mk_is_nan / mk_is_inf /            *)
+(*               mk_is_normal, new blocks added by PR #9038.           *)
+(*                                                                     *)
+(* The rewriter detects the pattern isX(to_fp(rm, to_real(int_expr))) *)
+(* and replaces it with a pure integer arithmetic constraint.          *)
+(*                                                                     *)
+(* Key invariants for to_fp_of_int (proved from axioms in IEEE754.fst):*)
+(*   - Never NaN      (ax_to_fp_int_not_nan)                          *)
+(*   - Never subnormal (ax_to_fp_int_not_subnormal)                   *)
+(*   - Zero iff x = 0  (ax_to_fp_int_zero, ax_to_fp_int_nonzero)     *)
+(*   - Inf iff x exceeds the format's overflow threshold               *)
+(* ================================================================== *)
+
+(* --- 2a: isNaN --- *)
+
+(* isNaN(to_fp(rm, x)) = false for any integer x.
+   Source: C++ block in mk_is_nan checking "a->get_num_args() == 2 &&
+   (m_util.au().is_real(a->get_arg(1)) || m_util.au().is_int(a->get_arg(1)))".
+   [extract: FPA_REWRITE_IS_NAN_TO_FP_INT] *)
+let lemma_is_nan_to_fp_int
+    (#eb #sb: pos) (rm: rounding_mode) (x: int)
+    : Lemma (is_nan (to_fp_of_int #eb #sb rm x) = false) =
+  ax_to_fp_int_not_nan #eb #sb rm x
+
+
+(* --- 2b: isInf --- *)
+
+(* Source: C++ function mk_is_inf_of_int, called from mk_is_inf.
+   Each lemma corresponds to one case in the switch(rm) statement.
+   [extract: FPA_REWRITE_IS_INF_TO_FP_INT, helper mk_is_inf_of_int] *)
+
+(* RNE: overflow iff |x| >= overflow_threshold(eb, sb).
+   At the boundary the significand of MAX_FINITE is odd, so RNE rounds
+   to even, which means rounding to ∞. *)
+let lemma_is_inf_to_fp_int_rne
+    (#eb #sb: pos) (x: int)
+    : Lemma (is_inf (to_fp_of_int #eb #sb RNE x) =
+             (x >= overflow_threshold eb sb || x <= -(overflow_threshold eb sb))) =
+  ax_is_inf_rne #eb #sb x
+
+(* RNA: same threshold as RNE (ties round away from zero to ∞). *)
+let lemma_is_inf_to_fp_int_rna
+    (#eb #sb: pos) (x: int)
+    : Lemma (is_inf (to_fp_of_int #eb #sb RNA x) =
+             (x >= overflow_threshold eb sb || x <= -(overflow_threshold eb sb))) =
+  ax_is_inf_rna #eb #sb x
+
+(* RTP: positive overflow only (negative values round toward 0, not -∞). *)
+let lemma_is_inf_to_fp_int_rtp
+    (#eb #sb: pos) (x: int)
+    : Lemma (is_inf (to_fp_of_int #eb #sb RTP x) = (x > max_finite_int eb sb)) =
+  ax_is_inf_rtp #eb #sb x
+
+(* RTN: negative overflow only (positive values round toward 0, not +∞). *)
+let lemma_is_inf_to_fp_int_rtn
+    (#eb #sb: pos) (x: int)
+    : Lemma (is_inf (to_fp_of_int #eb #sb RTN x) = (x < -(max_finite_int eb sb))) =
+  ax_is_inf_rtn #eb #sb x
+
+(* RTZ: truncation toward zero never overflows to infinity. *)
+let lemma_is_inf_to_fp_int_rtz
+    (#eb #sb: pos) (x: int)
+    : Lemma (is_inf (to_fp_of_int #eb #sb RTZ x) = false) =
+  ax_is_inf_rtz #eb #sb x
+
+
+(* --- 2c: isNormal --- *)
+
+(* isNormal(to_fp(rm, x)) ↔ x ≠ 0 ∧ ¬isInf(to_fp(rm, x))
+   Source: C++ block in mk_is_normal:
+     "expr_ref not_zero(...); expr_ref inf_cond = mk_is_inf_of_int(...);
+      result = m().mk_and(not_zero, m().mk_not(inf_cond));"
+   [extract: FPA_REWRITE_IS_NORMAL_TO_FP_INT]
+
+   Proof sketch:
+     For integer x, to_fp is never NaN (by ax_to_fp_int_not_nan) and
+     never subnormal (by ax_to_fp_int_not_subnormal).  By the exhaustive
+     classification axiom (ax_classification), the result must be one of:
+       zero, normal, or infinite.
+     Therefore:
+       - if x = 0: result is zero, hence NOT normal.
+       - if x ≠ 0: result is not zero (by ax_to_fp_int_nonzero), so
+           result is normal iff it is not infinite. *)
+let lemma_is_normal_to_fp_int
+    (#eb #sb: pos) (rm: rounding_mode) (x: int)
+    : Lemma (is_normal (to_fp_of_int #eb #sb rm x) =
+             (x <> 0 && not (is_inf (to_fp_of_int #eb #sb rm x)))) =
+  let f = to_fp_of_int #eb #sb rm x in
+  ax_to_fp_int_not_nan       #eb #sb rm x;   (* is_nan f = false      *)
+  ax_to_fp_int_not_subnormal #eb #sb rm x;   (* is_subnormal f = false *)
+  ax_classification          f;              (* nan||inf||zero||normal||subnormal *)
+  if x = 0 then begin
+    ax_to_fp_int_zero #eb #sb rm;            (* is_zero f = true  *)
+    ax_zero_exclusive f                      (* is_normal f = false, since is_zero f *)
+  end else begin
+    ax_to_fp_int_nonzero #eb #sb rm x;       (* is_zero f = false *)
+    (* At this point: not nan, not subnormal, not zero.
+       ax_classification gives nan||inf||zero||normal||subnormal, which
+       simplifies to inf||normal.  We case-split on is_inf f. *)
+    if is_inf f then
+      ax_inf_exclusive f                     (* is_inf f = true => is_normal f = false *)
+    else
+      ()                                     (* is_inf f = false; by classification, is_normal f = true *)
+  end
+
+
+(* ================================================================== *)
+(* Section 3: Classification Predicates Pushed through ite            *)
+(*                                                                     *)
+(* C++ location: fpa_rewriter.cpp, mk_is_nan / mk_is_inf /            *)
+(*               mk_is_normal, new blocks "Push through ite when both *)
+(*               branches are concrete FP numerals."                  *)
+(*                                                                     *)
+(* In the C++ rewriter the rule is applied only when both branches    *)
+(* are concrete numerals, so the classification can be evaluated at   *)
+(* rewrite time.  Mathematically the identity holds unconditionally   *)
+(* because is_nan, is_inf, and is_normal are total boolean functions. *)
+(*                                                                     *)
+(* These lemmas are trivial in F*: applying a function to             *)
+(* (if c then t else e) reduces by computation to                     *)
+(* (if c then f(t) else f(e)) for any total f.                        *)
+(* ================================================================== *)
+
+(* 3a.  isNaN(ite(c, t, e)) = ite(c, isNaN(t), isNaN(e))
+        Source: C++ block producing "m().mk_ite(c, is_nan(t) ? true : false,
+                                                   is_nan(e) ? true : false)".
+        [extract: FPA_REWRITE_IS_NAN_ITE] *)
+let lemma_is_nan_ite
+    (#eb #sb: pos) (c: bool) (t e: float eb sb)
+    : Lemma (is_nan (if c then t else e) =
+             (if c then is_nan t else is_nan e)) = ()
+
+
+(* 3b.  isInf(ite(c, t, e)) = ite(c, isInf(t), isInf(e))
+        Source: same pattern in mk_is_inf.
+        [extract: FPA_REWRITE_IS_INF_ITE] *)
+let lemma_is_inf_ite
+    (#eb #sb: pos) (c: bool) (t e: float eb sb)
+    : Lemma (is_inf (if c then t else e) =
+             (if c then is_inf t else is_inf e)) = ()
+
+
+(* 3c.  isNormal(ite(c, t, e)) = ite(c, isNormal(t), isNormal(e))
+        Source: same pattern in mk_is_normal.
+        [extract: FPA_REWRITE_IS_NORMAL_ITE] *)
+let lemma_is_normal_ite
+    (#eb #sb: pos) (c: bool) (t e: float eb sb)
+    : Lemma (is_normal (if c then t else e) =
+             (if c then is_normal t else is_normal e)) = ()
+
+
+(* ================================================================== *)
+(* Section 4: Composite correctness statements                        *)
+(*                                                                     *)
+(* These lemmas combine the individual results from Sections 1-3      *)
+(* to state the overall correctness of each rewrite as the C++        *)
+(* code produces it.                                                  *)
+(* ================================================================== *)
+
+(* The full FMA zero-multiplicand rewrite.
+   When zero_val is ±0 and y is symbolic, the rewriter produces:
+     ite(is_finite(y), fp_add(rm, fp_mul(rm, ±0, y), z), NaN)
+   We state this as two implications, one per arm of the ite.
+
+   Note: we use is_nan rather than equality with the canonical nan
+   constant because IEEE 754 does not prescribe a unique NaN encoding;
+   Z3 uses a canonical NaN internally, but that is an implementation
+   choice beyond the scope of this formalization. *)
+let lemma_fma_zero_ite_finite_arm
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y z: float eb sb)
+    : Lemma (requires is_zero zero_val = true && is_finite y = true)
+            (ensures  fp_fma rm zero_val y z =
+                      fp_add rm (fp_mul rm zero_val y) z &&
+                      is_zero (fp_mul rm zero_val y) = true) =
+  ax_fma_zero_finite rm zero_val y z
+
+let lemma_fma_zero_ite_nan_arm
+    (#eb #sb: pos)
+    (rm: rounding_mode) (zero_val y z: float eb sb)
+    : Lemma (requires is_zero zero_val = true && is_finite y = false)
+            (ensures  is_nan (fp_fma rm zero_val y z) = true) =
+  if is_nan y = true then
+    ax_fma_any_nan_y rm zero_val y z
+  else begin
+    (* is_finite y = false && is_nan y = false.
+       By the transparent definition is_finite y = not (is_nan y) && not (is_inf y),
+       the type-checker can derive is_inf y = true directly. *)
+    assert (is_inf y = true);
+    ax_zero_mul_inf rm zero_val y;
+    ax_fma_nan_mul  rm zero_val y z
+  end
+
+
+(* The full isNormal(to_fp(rm, x)) rewrite for RNE/RNA (most common mode).
+   Combining Sections 2b and 2c for RNE. *)
+let lemma_is_normal_to_fp_int_rne
+    (#eb #sb: pos) (x: int)
+    : Lemma (is_normal (to_fp_of_int #eb #sb RNE x) =
+             (x <> 0 &&
+              not (x >= overflow_threshold eb sb ||
+                   x <= -(overflow_threshold eb sb)))) =
+  lemma_is_normal_to_fp_int #eb #sb RNE x;
+  ax_is_inf_rne #eb #sb x
+
+(* The full isNormal(to_fp(rm, x)) rewrite for RTZ (never overflows). *)
+let lemma_is_normal_to_fp_int_rtz
+    (#eb #sb: pos) (x: int)
+    : Lemma (is_normal (to_fp_of_int #eb #sb RTZ x) = (x <> 0)) =
+  lemma_is_normal_to_fp_int #eb #sb RTZ x;
+  ax_is_inf_rtz #eb #sb x

fstar/IEEE754.fst

@@ -0,0 +1,311 @@
+(*
+  IEEE754.fst
+
+  Axiomatic theory of IEEE 754 floating-point arithmetic for use with
+  Z3's fpa_rewriter formalization.
+
+  All declarations prefixed with "ax_" are assumed axioms — consequences
+  of the IEEE 754-2019 standard that we take as given rather than
+  deriving from a bit-level representation.
+
+  The float type is parameterized by
+    eb : pos  -- number of exponent bits
+    sb : pos  -- number of significand bits (including the implicit leading bit)
+
+  This matches the parameterization used throughout Z3's fpa_decl_plugin
+  and mpf_manager.
+*)
+
+module IEEE754
+
+(* ------------------------------------------------------------------ *)
+(* Floating-point type                                                  *)
+(* ------------------------------------------------------------------ *)
+
+(* Abstract IEEE 754 float parameterized by format.  A concrete model
+   would be a triple (sign, biased_exponent, significand), but we keep
+   the type opaque so the axioms are the only assumed properties. *)
+assume val float : (eb: pos) -> (sb: pos) -> eqtype
+
+(* ------------------------------------------------------------------ *)
+(* Rounding modes (IEEE 754-2019 §4.3)                                 *)
+(* ------------------------------------------------------------------ *)
+
+type rounding_mode =
+  | RNE   (* roundTiesToEven     *)
+  | RNA   (* roundTiesToAway     *)
+  | RTP   (* roundTowardPositive *)
+  | RTN   (* roundTowardNegative *)
+  | RTZ   (* roundTowardZero     *)
+
+(* ------------------------------------------------------------------ *)
+(* Classification predicates (IEEE 754-2019 §5.7.2)                   *)
+(* ------------------------------------------------------------------ *)
+
+assume val is_nan      : #eb:pos -> #sb:pos -> float eb sb -> bool
+assume val is_inf      : #eb:pos -> #sb:pos -> float eb sb -> bool
+assume val is_zero     : #eb:pos -> #sb:pos -> float eb sb -> bool
+assume val is_normal   : #eb:pos -> #sb:pos -> float eb sb -> bool
+assume val is_subnormal: #eb:pos -> #sb:pos -> float eb sb -> bool
+assume val is_negative : #eb:pos -> #sb:pos -> float eb sb -> bool
+assume val is_positive : #eb:pos -> #sb:pos -> float eb sb -> bool
+
+(* Derived: finite = not NaN and not infinite.
+   This matches Z3's is_finite check in fpa_rewriter.cpp. *)
+let is_finite (#eb #sb: pos) (x: float eb sb) : bool =
+  not (is_nan x) && not (is_inf x)
+
+(* ------------------------------------------------------------------ *)
+(* Classification axioms                                                *)
+(* ------------------------------------------------------------------ *)
+
+(* Every float belongs to exactly one of the five IEEE 754 classes. *)
+assume val ax_classification :
+  #eb:pos -> #sb:pos -> (x: float eb sb) ->
+  Lemma (is_nan x || is_inf x || is_zero x || is_normal x || is_subnormal x)
+
+(* The five classes are mutually exclusive. *)
+assume val ax_nan_exclusive :
+  #eb:pos -> #sb:pos -> (x: float eb sb) ->
+  Lemma (requires is_nan x = true)
+        (ensures  is_inf x = false && is_zero x = false &&
+                  is_normal x = false && is_subnormal x = false)
+
+assume val ax_inf_exclusive :
+  #eb:pos -> #sb:pos -> (x: float eb sb) ->
+  Lemma (requires is_inf x = true)
+        (ensures  is_nan x = false && is_zero x = false &&
+                  is_normal x = false && is_subnormal x = false)
+
+assume val ax_zero_exclusive :
+  #eb:pos -> #sb:pos -> (x: float eb sb) ->
+  Lemma (requires is_zero x = true)
+        (ensures  is_nan x = false && is_inf x = false &&
+                  is_normal x = false && is_subnormal x = false)
+
+assume val ax_normal_exclusive :
+  #eb:pos -> #sb:pos -> (x: float eb sb) ->
+  Lemma (requires is_normal x = true)
+        (ensures  is_nan x = false && is_inf x = false &&
+                  is_zero x = false && is_subnormal x = false)
+
+assume val ax_subnormal_exclusive :
+  #eb:pos -> #sb:pos -> (x: float eb sb) ->
+  Lemma (requires is_subnormal x = true)
+        (ensures  is_nan x = false && is_inf x = false &&
+                  is_zero x = false && is_normal x = false)
+
+(* Zeros are finite (not NaN, not inf). *)
+let lemma_zero_is_finite
+    (#eb #sb: pos) (x: float eb sb)
+    : Lemma (requires is_zero x = true) (ensures is_finite x = true) =
+  ax_zero_exclusive x
+
+(* ------------------------------------------------------------------ *)
+(* Named constants                                                      *)
+(* ------------------------------------------------------------------ *)
+
+assume val nan   : #eb:pos -> #sb:pos -> float eb sb
+assume val pinf  : #eb:pos -> #sb:pos -> float eb sb
+assume val ninf  : #eb:pos -> #sb:pos -> float eb sb
+assume val pzero : #eb:pos -> #sb:pos -> float eb sb
+assume val nzero : #eb:pos -> #sb:pos -> float eb sb
+
+assume val ax_nan_is_nan    : #eb:pos -> #sb:pos -> Lemma (is_nan  (nan   #eb #sb) = true)
+assume val ax_pinf_is_inf   : #eb:pos -> #sb:pos -> Lemma (is_inf  (pinf  #eb #sb) = true)
+assume val ax_ninf_is_inf   : #eb:pos -> #sb:pos -> Lemma (is_inf  (ninf  #eb #sb) = true)
+assume val ax_pzero_is_zero : #eb:pos -> #sb:pos ->
+  Lemma (is_zero (pzero #eb #sb) = true && is_positive (pzero #eb #sb) = true)
+assume val ax_nzero_is_zero : #eb:pos -> #sb:pos ->
+  Lemma (is_zero (nzero #eb #sb) = true && is_negative (nzero #eb #sb) = true)
+
+(* ------------------------------------------------------------------ *)
+(* Arithmetic operations                                                *)
+(* ------------------------------------------------------------------ *)
+
+assume val fp_add : #eb:pos -> #sb:pos ->
+  rounding_mode -> float eb sb -> float eb sb -> float eb sb
+
+assume val fp_mul : #eb:pos -> #sb:pos ->
+  rounding_mode -> float eb sb -> float eb sb -> float eb sb
+
+(* fp_fma rm x y z = roundToNearest(x * y + z), per IEEE 754-2019 §5.4 *)
+assume val fp_fma : #eb:pos -> #sb:pos ->
+  rounding_mode -> float eb sb -> float eb sb -> float eb sb -> float eb sb
+
+(* ------------------------------------------------------------------ *)
+(* NaN propagation axioms (IEEE 754-2019 §6.2)                        *)
+(* ------------------------------------------------------------------ *)
+
+assume val ax_add_nan_l :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (y: float eb sb) ->
+  Lemma (is_nan (fp_add rm (nan #eb #sb) y) = true)
+
+assume val ax_add_nan_r :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) ->
+  Lemma (is_nan (fp_add rm x (nan #eb #sb)) = true)
+
+assume val ax_mul_nan_l :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (y: float eb sb) ->
+  Lemma (is_nan (fp_mul rm (nan #eb #sb) y) = true)
+
+assume val ax_mul_nan_r :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) ->
+  Lemma (is_nan (fp_mul rm x (nan #eb #sb)) = true)
+
+assume val ax_fma_nan_x :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (y: float eb sb) -> (z: float eb sb) ->
+  Lemma (is_nan (fp_fma rm (nan #eb #sb) y z) = true)
+
+assume val ax_fma_nan_y :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (z: float eb sb) ->
+  Lemma (is_nan (fp_fma rm x (nan #eb #sb) z) = true)
+
+assume val ax_fma_nan_z :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) ->
+  Lemma (is_nan (fp_fma rm x y (nan #eb #sb)) = true)
+
+(* General NaN propagation: if any argument is NaN, the result is NaN. *)
+assume val ax_fma_any_nan_x :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) -> (z: float eb sb) ->
+  Lemma (requires is_nan x = true)
+        (ensures  is_nan (fp_fma rm x y z) = true)
+
+assume val ax_fma_any_nan_y :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) -> (z: float eb sb) ->
+  Lemma (requires is_nan y = true)
+        (ensures  is_nan (fp_fma rm x y z) = true)
+
+assume val ax_fma_any_nan_z :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) -> (z: float eb sb) ->
+  Lemma (requires is_nan z = true)
+        (ensures  is_nan (fp_fma rm x y z) = true)
+
+(* ------------------------------------------------------------------ *)
+(* Special-value arithmetic axioms                                      *)
+(* ------------------------------------------------------------------ *)
+
+(* 0 * ±∞ = NaN: "invalid operation" per IEEE 754-2019 §7.2. *)
+assume val ax_zero_mul_inf :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) ->
+  (zero_val: float eb sb) -> (inf_val: float eb sb) ->
+  Lemma (requires is_zero zero_val = true && is_inf inf_val = true)
+        (ensures  is_nan (fp_mul rm zero_val inf_val) = true &&
+                  is_nan (fp_mul rm inf_val zero_val) = true)
+
+(* If the product in fma is NaN, the whole fma is NaN.
+   This covers the case where fp_mul rm x y = NaN and we need
+   is_nan (fp_fma rm x y z) = true. *)
+assume val ax_fma_nan_mul :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: float eb sb) -> (y: float eb sb) -> (z: float eb sb) ->
+  Lemma (requires is_nan (fp_mul rm x y) = true)
+        (ensures  is_nan (fp_fma rm x y z) = true)
+
+(* fma(rm, zero, y_finite, z) = fp_add(rm, fp_mul(rm, zero, y_finite), z)
+   and fp_mul(rm, zero, y_finite) is ±0 (exact, IEEE 754-2019 §6.3).
+   This is the core decomposition used by the rewriter. *)
+assume val ax_fma_zero_finite :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (zero_val: float eb sb) -> (y: float eb sb) -> (z: float eb sb) ->
+  Lemma (requires is_zero zero_val = true && is_finite y = true)
+        (ensures  fp_fma rm zero_val y z = fp_add rm (fp_mul rm zero_val y) z &&
+                  is_zero (fp_mul rm zero_val y) = true)
+
+(* Sign of 0 * y (IEEE 754-2019 §6.3):
+   sign(0 * y) = sign(0) XOR sign(y) for finite nonzero y. *)
+assume val ax_zero_mul_sign :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (zero_val: float eb sb) -> (y: float eb sb) ->
+  Lemma (requires is_zero zero_val = true && is_finite y = true && is_zero y = false)
+        (ensures  (let p = fp_mul rm zero_val y in
+                   is_zero p = true &&
+                   (is_negative p =
+                     ((is_negative zero_val && not (is_negative y)) ||
+                      (not (is_negative zero_val) && is_negative y)))))
+
+(* fp_add(rm, ±0, z) = z when z is finite and nonzero (IEEE 754-2019 §6.3).
+   ±0 is an additive identity for nonzero finite values under all rounding modes. *)
+assume val ax_add_zero_nonzero :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (zero_val: float eb sb) -> (z: float eb sb) ->
+  Lemma (requires is_zero zero_val = true && is_finite z = true && is_zero z = false)
+        (ensures  fp_add rm zero_val z = z)
+
+(* ------------------------------------------------------------------ *)
+(* Integer-to-float conversion                                          *)
+(* ------------------------------------------------------------------ *)
+
+(* to_fp_of_int rm x: convert integer x to the nearest representable
+   float in the (eb, sb) format, using rounding mode rm.
+   This corresponds to to_fp(rm, to_real(x)) in Z3's SMT theory. *)
+assume val to_fp_of_int : #eb:pos -> #sb:pos -> rounding_mode -> int -> float eb sb
+
+(* Conversion of any integer never produces NaN (IEEE 754-2019 §5.4.1):
+   NaN only arises from invalid operations, not from converting finite values. *)
+assume val ax_to_fp_int_not_nan :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: int) ->
+  Lemma (is_nan (to_fp_of_int #eb #sb rm x) = false)
+
+(* Conversion of any integer never produces a subnormal value.
+   Justification: the smallest nonzero integer has magnitude 1, and
+   1.0 is a normal number in every IEEE 754 format (its biased exponent
+   equals the bias, which is always in range). *)
+assume val ax_to_fp_int_not_subnormal :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: int) ->
+  Lemma (is_subnormal (to_fp_of_int #eb #sb rm x) = false)
+
+(* 0 maps to a zero (the sign may depend on the rounding mode for RTN). *)
+assume val ax_to_fp_int_zero :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) ->
+  Lemma (is_zero (to_fp_of_int #eb #sb rm 0) = true)
+
+(* A nonzero integer maps to a nonzero float. *)
+assume val ax_to_fp_int_nonzero :
+  #eb:pos -> #sb:pos -> (rm: rounding_mode) -> (x: int) ->
+  Lemma (requires x <> 0)
+        (ensures is_zero (to_fp_of_int #eb #sb rm x) = false)
+
+(* ------------------------------------------------------------------ *)
+(* Overflow thresholds for isInf(to_fp_of_int rm x)                   *)
+(*                                                                     *)
+(* overflow_threshold eb sb: the smallest integer magnitude that       *)
+(* causes overflow to ±∞ under RNE and RNA.                           *)
+(*   = ⌈MAX_FINITE + ULP(MAX_FINITE)/2⌉                               *)
+(* where MAX_FINITE = (2 - 2^(1-sb)) * 2^(2^(eb-1)-1).               *)
+(*                                                                     *)
+(* max_finite_int eb sb: ⌊MAX_FINITE⌋, used for RTP and RTN.         *)
+(*                                                                     *)
+(* The concrete computation is performed by mk_is_inf_of_int in        *)
+(* fpa_rewriter.cpp using mpf_manager::mk_max_value and to_rational.  *)
+(* ------------------------------------------------------------------ *)
+
+assume val overflow_threshold : (eb: pos) -> (sb: pos) -> pos
+assume val max_finite_int     : (eb: pos) -> (sb: pos) -> pos
+
+(* RNE: overflow iff |x| >= overflow_threshold(eb, sb).
+   At the boundary, RNE rounds to even; since MAX_FINITE has an odd
+   significand, it rounds away from MAX_FINITE, i.e. to infinity. *)
+assume val ax_is_inf_rne :
+  #eb:pos -> #sb:pos -> (x: int) ->
+  Lemma (is_inf (to_fp_of_int #eb #sb RNE x) =
+         (x >= overflow_threshold eb sb || x <= -(overflow_threshold eb sb)))
+
+(* RNA: same threshold as RNE (both round ties away from zero). *)
+assume val ax_is_inf_rna :
+  #eb:pos -> #sb:pos -> (x: int) ->
+  Lemma (is_inf (to_fp_of_int #eb #sb RNA x) =
+         (x >= overflow_threshold eb sb || x <= -(overflow_threshold eb sb)))
+
+(* RTP: positive overflow only (x > MAX_FINITE rounds up to +∞;
+   negative values are rounded toward zero, never to -∞). *)
+assume val ax_is_inf_rtp :
+  #eb:pos -> #sb:pos -> (x: int) ->
+  Lemma (is_inf (to_fp_of_int #eb #sb RTP x) = (x > max_finite_int eb sb))
+
+(* RTN: negative overflow only (x < -MAX_FINITE rounds down to -∞;
+   positive values are rounded toward zero, never to +∞). *)
+assume val ax_is_inf_rtn :
+  #eb:pos -> #sb:pos -> (x: int) ->
+  Lemma (is_inf (to_fp_of_int #eb #sb RTN x) = (x < -(max_finite_int eb sb)))
+
+(* RTZ: truncation toward zero never overflows to infinity. *)
+assume val ax_is_inf_rtz :
+  #eb:pos -> #sb:pos -> (x: int) ->
+  Lemma (is_inf (to_fp_of_int #eb #sb RTZ x) = false)

fstar/README.md

@@ -0,0 +1,250 @@
+# F\* Formalization of FPA Rewriter Rules (PR #9038)
+
+This directory contains a formalization of the floating-point rewrite
+rules introduced in [Z3 PR #9038](https://github.com/Z3Prover/z3/pull/9038)
+in the [F\*](https://www.fstar-lang.org/) proof assistant.
+
+## Overview
+
+PR #9038 adds three families of optimizations to `src/ast/rewriter/fpa_rewriter.cpp`
+that avoid expensive FP bit-blasting:
+
+| Optimization | C++ function | F\* module and section |
+|---|---|---|
+| `fma(rm, ±0, y, z)` zero-multiplicand decomposition | `mk_fma` | `FPARewriterRules.fst` §1 |
+| `isNaN/isInf/isNormal` applied to `to_fp(rm, to_real(int))` | `mk_is_nan`, `mk_is_inf`, `mk_is_normal`, `mk_is_inf_of_int` | `FPARewriterRules.fst` §2 |
+| Push classification predicates through `ite` with concrete branches | `mk_is_nan`, `mk_is_inf`, `mk_is_normal` | `FPARewriterRules.fst` §3 |
+
+## Files
+
+### `IEEE754.fst`
+
+Abstract axiomatic theory of IEEE 754 floating-point arithmetic.
+- **Type** `float eb sb` — abstract float parameterized by exponent bits `eb`
+  and significand bits `sb`, matching Z3's `mpf` representation.
+- **Type** `rounding_mode` — the five IEEE 754 rounding modes (RNE, RNA, RTP,
+  RTN, RTZ).
+- **Classification predicates** — `is_nan`, `is_inf`, `is_zero`, `is_normal`,
+  `is_subnormal`, `is_negative`, `is_positive`, derived `is_finite`.
+- **Arithmetic operations** — `fp_add`, `fp_mul`, `fp_fma`.
+- **Conversion** — `to_fp_of_int rm x` representing `to_fp(rm, to_real(x))`.
+- **Axioms** (`ax_*`) — consequences of the IEEE 754-2019 standard taken as
+  given, covering classification exclusivity, NaN propagation, special-value
+  arithmetic, and integer-conversion properties.
+- **Overflow thresholds** — `overflow_threshold eb sb` and `max_finite_int eb sb`
+  corresponding to the values computed by `mk_is_inf_of_int` in the C++ rewriter.
+
+All axioms use `assume val`, marking them as trusted without proof.
+
+### `FPARewriterRules.fst`
+
+Derived rewrite rules proved from `IEEE754.fst` axioms.
+
+#### Section 1 — FMA with a Zero Multiplicand
+
+| Lemma | Statement |
+|---|---|
+| `lemma_fma_zero_nan_addend` | `fma(rm, ±0, y, NaN) = NaN` |
+| `lemma_fma_zero_nan_mul` | `fma(rm, ±0, NaN, z) = NaN` |
+| `lemma_fma_zero_inf_mul` | `fma(rm, ±0, ±∞, z) = NaN` |
+| `lemma_fma_zero_finite_decomposes` | `fma(rm, ±0, y_finite, z) = fp_add(rm, fp_mul(rm, ±0, y_finite), z)` |
+| `lemma_fma_zero_const_addend` | `fma(rm, ±0, y_finite, z_nonzero_finite) = z` |
+| `lemma_fma_zero_const_finite_arm` | finite arm of the `ite` for symbolic `y`, concrete non-zero `z` |
+| `lemma_fma_zero_const_nan_inf_arm` | NaN/inf arm of the same `ite` |
+| `lemma_fma_zero_general_finite_arm` | finite arm for fully symbolic `y` and `z` |
+| `lemma_fma_zero_general_nan_inf_arm` | NaN/inf arm for fully symbolic `y` and `z` |
+| `lemma_fma_zero_product_sign` | sign of `fp_mul(rm, zero_val, y)` = sign(zero_val) XOR sign(y) |
+| `lemma_fma_zero_ite_correct` | full composite: `fma(rm, ±0, y, z) = ite(is_finite(y), fp_add(rm, fp_mul(rm, ±0, y), z), NaN)` |
+
+#### Section 2 — Classification of Integer-to-Float Conversions
+
+| Lemma | Statement |
+|---|---|
+| `lemma_is_nan_to_fp_int` | `isNaN(to_fp(rm, x)) = false` |
+| `lemma_is_inf_to_fp_int_rne` | `isInf(to_fp(RNE, x)) ↔ \|x\| ≥ overflow_threshold` |
+| `lemma_is_inf_to_fp_int_rna` | `isInf(to_fp(RNA, x)) ↔ \|x\| ≥ overflow_threshold` |
+| `lemma_is_inf_to_fp_int_rtp` | `isInf(to_fp(RTP, x)) ↔ x > max_finite_int` |
+| `lemma_is_inf_to_fp_int_rtn` | `isInf(to_fp(RTN, x)) ↔ x < -max_finite_int` |
+| `lemma_is_inf_to_fp_int_rtz` | `isInf(to_fp(RTZ, x)) = false` |
+| `lemma_is_normal_to_fp_int` | `isNormal(to_fp(rm, x)) ↔ x ≠ 0 ∧ ¬isInf(to_fp(rm, x))` |
+| `lemma_is_normal_to_fp_int_rne` | combined form for RNE |
+| `lemma_is_normal_to_fp_int_rtz` | combined form for RTZ |
+
+#### Section 3 — Classification through `ite`
+
+| Lemma | Statement |
+|---|---|
+| `lemma_is_nan_ite` | `isNaN(ite(c, t, e)) = ite(c, isNaN(t), isNaN(e))` |
+| `lemma_is_inf_ite` | `isInf(ite(c, t, e)) = ite(c, isInf(t), isInf(e))` |
+| `lemma_is_normal_ite` | `isNormal(ite(c, t, e)) = ite(c, isNormal(t), isNormal(e))` |
+
+The Section 3 lemmas are trivially true in F\* by computation (applying a
+function to `if c then t else e` reduces to `if c then f t else f e`), which
+is why their proofs are the single term `()`.
+
+### `RewriteCodeGen.fst`
+
+Meta-F* reflection module that programmatically extracts C++ rewriter code
+from F* lemmas using F* tactics (`FStar.Tactics.V2`) and term inspection
+(`FStar.Reflection.V2`).
+
+#### How it works
+
+Given a quoted lemma name such as `(quote lemma_is_nan_ite)`, the
+`extract_rewrite` tactic:
+
+1. Calls `tc env lemma` to obtain the lemma's type.
+2. Strips the `Tv_Arrow` chain (the `∀ #eb #sb c t e .` prefix), collecting
+   parameter names and building a de Bruijn index-to-name map.
+3. Extracts the equality `LHS = RHS` from the `C_Lemma` precondition.
+4. Decomposes `LHS` into `top_fn(argument_pattern)`.  `top_fn` (e.g.
+   `is_nan`) is the IEEE 754 predicate whose Z3 `mk_*` method is being
+   extended.  `argument_pattern` drives the C++ pattern match.
+5. Detects `if c then t else e` (which F* represents as a two-branch
+   `Tv_Match` on a `bool` scrutinee) and maps it to `PIte c t e` in the
+   intermediate representation.
+6. Translates `RHS` into the `cexpr` IR.
+7. Calls `gen_cpp` to emit the self-contained C++ if-block.
+
+#### Example
+
+Running `extract_rewrite (quote lemma_is_nan_ite)` outputs:
+
+```cpp
+expr *c, *t, *e;
+if (m().is_ite(arg1, c, t, e)) {
+    result = m().mk_ite(c, m_util.mk_is_nan(t), m_util.mk_is_nan(e));
+    return BR_REWRITE2;
+}
+```
+
+The same tactic applied to `lemma_is_inf_ite` and `lemma_is_normal_ite`
+produces the analogous blocks for `m_util.mk_is_inf` and
+`m_util.mk_is_normal`.
+
+#### Design
+
+The module defines two intermediate representations:
+
+- `cpat` — patterns on the LHS: `PVar`, `PIte`, `PApp`.
+- `cexpr` — expressions on the RHS: `EVar`, `EBool`, `EIte`, `EApp`.
+
+The `cpp_builder_name` helper maps IEEE 754 function names
+(`is_nan`, `is_inf`, `is_normal`, `is_negative`, `is_positive`, `is_zero`)
+to their Z3 C++ counterparts (`m_util.mk_is_nan`, etc.).
+
+The three `let _ = run_tactic ...` blocks at the bottom of the file
+demonstrate extraction for the three ite-pushthrough lemmas and print
+their generated C++ to stdout during F* typechecking.
+
+### `../src/ast/rewriter/fpa_rewriter_rules.h`
+
+C++ header containing one `#define` macro per rewrite rule, whose correctness
+is proved by F* lemmas in `FPARewriterRules.fst`.  The ite-pushthrough macros
+(`FPA_REWRITE_IS_NAN_ITE`, `FPA_REWRITE_IS_INF_ITE`, `FPA_REWRITE_IS_NORMAL_ITE`)
+can be regenerated by running `RewriteCodeGen.fst`.  Each macro is annotated
+with an `[extract: MACRO_NAME]` comment in the corresponding F* lemma.
+
+| Macro | F\* lemma(s) | Used in C++ function |
+|---|---|---|
+| `FPA_REWRITE_IS_NAN_TO_FP_INT` | `lemma_is_nan_to_fp_int` | `mk_is_nan` |
+| `FPA_REWRITE_IS_NAN_ITE` | `lemma_is_nan_ite` | `mk_is_nan` |
+| `FPA_REWRITE_IS_INF_TO_FP_INT` | `lemma_is_inf_to_fp_int_*` | `mk_is_inf` |
+| `FPA_REWRITE_IS_INF_ITE` | `lemma_is_inf_ite` | `mk_is_inf` |
+| `FPA_REWRITE_IS_NORMAL_TO_FP_INT` | `lemma_is_normal_to_fp_int` | `mk_is_normal` |
+| `FPA_REWRITE_IS_NORMAL_ITE` | `lemma_is_normal_ite` | `mk_is_normal` |
+| `FPA_REWRITE_FMA_ZERO_MUL` | `lemma_fma_zero_*` (all §1 lemmas) | `mk_fma` |
+
+Each macro is self-contained and uses `_fpa_`-prefixed local variables to
+avoid name collisions.  All macros are designed for use inside member
+functions of `fpa_rewriter` where `m()`, `m_util`, `m_fm`, and
+`mk_is_inf_of_int` are in scope.
+
+The helper function `mk_is_inf_of_int` (declared in `fpa_rewriter.h`,
+implemented in `fpa_rewriter.cpp`) computes the integer-arithmetic overflow
+condition for `isInf(to_fp(rm, x))` by switching on the rounding mode,
+corresponding to the five `lemma_is_inf_to_fp_int_*` lemmas.
+
+## Relationship to the C++ Code
+
+The following table maps each lemma to its corresponding C++ macro and the function where the macro is invoked.
+
+| Lemma | C++ macro | Used in |
+|---|---|---|
+| `lemma_fma_zero_nan_addend` | `FPA_REWRITE_FMA_ZERO_MUL` case (a) | `mk_fma` |
+| `lemma_fma_zero_nan_mul` | `FPA_REWRITE_FMA_ZERO_MUL` case (b) | `mk_fma` |
+| `lemma_fma_zero_inf_mul` | `FPA_REWRITE_FMA_ZERO_MUL` case (b) | `mk_fma` |
+| `lemma_fma_zero_finite_decomposes` | `FPA_REWRITE_FMA_ZERO_MUL` case (c) | `mk_fma` |
+| `lemma_fma_zero_const_addend` | `FPA_REWRITE_FMA_ZERO_MUL` case (c) | `mk_fma` |
+| `lemma_fma_zero_const_*_arm` | `FPA_REWRITE_FMA_ZERO_MUL` case (d) | `mk_fma` |
+| `lemma_fma_zero_general_*_arm` | `FPA_REWRITE_FMA_ZERO_MUL` case (e) | `mk_fma` |
+| `lemma_fma_zero_product_sign` | `FPA_REWRITE_FMA_ZERO_MUL` sign computation | `mk_fma` |
+| `lemma_is_nan_to_fp_int` | `FPA_REWRITE_IS_NAN_TO_FP_INT` | `mk_is_nan` |
+| `lemma_is_inf_to_fp_int_*` | `FPA_REWRITE_IS_INF_TO_FP_INT` + `mk_is_inf_of_int` | `mk_is_inf` |
+| `lemma_is_normal_to_fp_int` | `FPA_REWRITE_IS_NORMAL_TO_FP_INT` | `mk_is_normal` |
+| `lemma_is_nan_ite` | `FPA_REWRITE_IS_NAN_ITE` | `mk_is_nan` |
+| `lemma_is_inf_ite` | `FPA_REWRITE_IS_INF_ITE` | `mk_is_inf` |
+| `lemma_is_normal_ite` | `FPA_REWRITE_IS_NORMAL_ITE` | `mk_is_normal` |
+
+## IEEE 754 References
+
+The axioms in `IEEE754.fst` correspond to the following sections of the
+IEEE 754-2019 standard:
+
+- §4.3 — Rounding-direction attributes (rounding modes)
+- §5.4 — Arithmetic operations (`fp_add`, `fp_mul`, `fp_fma`)
+- §5.4.1 — Conversion from integer (`to_fp_of_int`)
+- §5.7.2 — General operations: `isNaN`, `isInfinite`, `isNormal`, etc.
+- §6.2 — Operations on quiet NaNs (NaN propagation)
+- §6.3 — The sign bit: signed zero (`ax_zero_mul_sign`, `ax_add_zero_nonzero`)
+- §7.2 — Invalid operation exception: 0 × ∞ = NaN (`ax_zero_mul_inf`)
+
+## Building
+
+### Type-checking the formalization
+
+To type-check the IEEE 754 axioms and the rewrite-rule lemmas:
+
+```sh
+fstar.exe --include . IEEE754.fst FPARewriterRules.fst
+```
+
+### Running the Meta-F* extraction
+
+The convenience script `extract.sh` runs the extraction and prints the
+generated C++ rules to stdout:
+
+```sh
+cd fstar && ./extract.sh
+```
+
+Or invoke F* directly:
+
+```sh
+fstar.exe --include . IEEE754.fst FPARewriterRules.fst RewriteCodeGen.fst
+```
+
+This type-checks all three files and executes the `run_tactic` calls in
+`RewriteCodeGen.fst`, printing the generated C++ for each ite-pushthrough
+lemma.  To capture the output to a file:
+
+```sh
+./extract.sh > extracted_rules.txt
+```
+
+### Continuous integration
+
+The GitHub Actions workflow `.github/workflows/fstar-extract.yml` runs
+the extraction automatically on every push or pull request that touches
+the `fstar/` directory.  It installs the F* binary, runs `extract.sh`,
+and uploads the generated C++ as a downloadable artifact
+`fstar-extracted-cpp-rules` for inspection.
+
+F\* 2026.03.24 or later is required.  The files have no external
+dependencies beyond the F\* standard library prelude.
+
+Because all IEEE 754 semantics are encoded as `assume val` axioms, the
+type-checker accepts the development without requiring a concrete model.
+The derived lemmas in `FPARewriterRules.fst` are fully verified against
+those axioms; the Section 3 lemmas (`lemma_*_ite`) are discharged by
+computation reduction alone.

fstar/RewriteCodeGen.fst

@@ -0,0 +1,492 @@
+(**
+  RewriteCodeGen.fst
+
+  F* tactic using Meta-F* reflection to extract Z3 C++ rewriter code from
+  F* rewrite lemmas in FPARewriterRules.fst.
+
+  Given a lemma such as:
+
+    lemma_is_nan_ite:
+      is_nan (if c then t else e) = (if c then is_nan t else is_nan e)
+
+  Running `extract_rewrite (quote lemma_is_nan_ite)` produces:
+
+    expr *c, *t, *e;
+    if (m().is_ite(arg1, c, t, e)) {
+        result = m().mk_ite(c, m_util.mk_is_nan(t), m_util.mk_is_nan(e));
+        return BR_REWRITE2;
+    }
+
+  Approach:
+  1. Use `tc` to get the type of the quoted lemma name.
+  2. Strip universal quantifiers (Tv_Arrow chain), collecting parameter names.
+  3. Extract the equality from the C_Lemma pre-condition.
+  4. Decompose LHS into: top_fn(argument_pattern).
+     The top_fn, e.g. is_nan, is the function whose rewriter method we extend.
+     The argument pattern, e.g. if c then t else e, drives the C++ match.
+  5. Decompose RHS into a construction expression.
+  6. Emit C++ code for Z3's rewriter.
+
+  Key F* reflection concepts used:
+  - `inspect : term -> Tac term_view`  -- destructure a term
+  - `Tv_App hd (arg, qual)`            -- curried function application
+  - `Tv_Match scrutinee _ branches`    -- pattern match; if-then-else is a match on bool
+  - `Tv_Arrow binder comp`             -- function/forall type
+  - `C_Lemma pre post pats`            -- Lemma computation type
+  - `Tv_FVar fv`                       -- free (top-level) variable
+  - `Tv_BVar bv`                       -- bound variable, de Bruijn indexed
+  - `tc env term`                      -- type-check a term, returning its type
+**)
+
+module RewriteCodeGen
+
+open FStar.List.Tot
+open FStar.Tactics.V2
+open FStar.Reflection.V2
+
+(* ================================================================
+   Section 1: Intermediate Representation
+   ================================================================ *)
+
+(* Pattern recognized on the LHS, the argument to the top-level function *)
+noeq type cpat =
+  | PVar  : name:string -> cpat
+  | PIte  : c:cpat -> t:cpat -> e:cpat -> cpat
+  | PApp  : fn:string -> args:list cpat -> cpat
+
+(* Expression to build on the RHS *)
+noeq type cexpr =
+  | EVar  : name:string -> cexpr
+  | EIte  : c:cexpr -> t:cexpr -> e:cexpr -> cexpr
+  | EApp  : fn:string -> args:list cexpr -> cexpr
+  | EBool : v:bool -> cexpr
+
+(* ================================================================
+   Section 2: Reflection Helpers
+   ================================================================ *)
+
+(* Collect curried application spine:
+   f a b c  to  (f, [(a,q1); (b,q2); (c,q3)])
+   This undoes the nested Tv_App structure that F* uses for
+   multi-argument applications. *)
+let rec collect_app (t: term) : Tac (term & list argv) =
+  match inspect_ln t with
+  | Tv_App hd arg ->
+    let (h, args) = collect_app hd in
+    (h, args @ [arg])
+  | _ -> (t, [])
+
+(* Keep only explicit (non-implicit, non-meta) arguments.
+   In F*, `is_nan #eb #sb x` has implicit args #eb, #sb and
+   explicit arg x. We only care about explicit args for codegen. *)
+let filter_explicit (args: list argv) : list term =
+  List.Tot.map fst
+    (List.Tot.filter (fun (_, q) -> Q_Explicit? q) args)
+
+(* Get the short name of a free variable, last component of the path.
+   E.g. "IEEE754.is_nan" to "is_nan" *)
+let fv_short_name (t: term) : Tac (option string) =
+  match inspect_ln t with
+  | Tv_FVar fv ->
+    (match List.Tot.rev (inspect_fv fv) with
+     | last :: _ -> Some last
+     | _ -> None)
+  | _ -> None
+
+(* Resolve a variable name from a term.
+   In F* 2026, variables in lemma types returned by `tc env` may appear
+   as named variables (Tv_Var namedv) rather than de Bruijn indices, so
+   we first try the named view and fall back to de Bruijn lookup. *)
+let var_name (idx_map: list (nat & string)) (offset: nat) (t: term) : Tac (option string) =
+  (* Try named-view first: Tv_Var gives a directly named variable. *)
+  (match FStar.Tactics.NamedView.inspect t with
+   | FStar.Tactics.NamedView.Tv_Var nv ->
+     let nm = unseal nv.ppname in
+     Some nm
+   | _ ->
+     (* Fall back to de Bruijn lookup for variables still in closed form. *)
+     match inspect_ln t with
+     | Tv_BVar bv ->
+       let bvv = inspect_bv bv in
+       if bvv.index < offset then None
+       else begin
+         let adj : nat = bvv.index - offset in
+         (match List.Tot.assoc #nat adj idx_map with
+          | Some n -> Some n
+          | None ->
+            let pp = unseal bvv.ppname in
+            print ("WARNING: var_name fallback for BVar index "
+                   ^ string_of_int bvv.index ^ " (adj="
+                   ^ string_of_int adj ^ "), using ppname '" ^ pp ^ "'");
+            Some pp)
+       end
+     | _ -> None)
+
+(* Detect if-then-else in reflected terms.
+   In F*, `if c then t else e` desugars to:
+     match c with | true -> t | (x:bool) -> e
+   where the false branch uses Pat_Var (not Pat_Constant), adding an extra
+   binder.  We therefore return the additional binder count for each branch
+   body, so callers can adjust the de Bruijn offset accordingly:
+     - then-branch (Pat_Constant): 0 extra binders
+     - else-branch (Pat_Var):      1 extra binder *)
+let try_ite (t: term) : Tac (option (term & nat & term & nat & term)) =
+  match inspect_ln t with
+  | Tv_Match scrutinee _ret branches ->
+    (match branches with
+     | [(pat_t, body_t); (pat_f, body_f)] ->
+       let extra_t : nat = match pat_t with | Pat_Var _ _ -> 1 | _ -> 0 in
+       let extra_f : nat = match pat_f with | Pat_Var _ _ -> 1 | _ -> 0 in
+       Some (scrutinee, extra_t, body_t, extra_f, body_f)
+     | _ -> None)
+  | _ -> None
+
+(* Unwrap `squash p` or `b2t p` to `p` if present.
+   The Lemma postcondition is often wrapped in squash or b2t.
+   In F* 2026, bool-valued propositions in Lemma postconditions are
+   wrapped in `b2t` which coerces `bool` to `prop`. *)
+let unwrap_squash (t: term) : Tac term =
+  let (head, args) = collect_app t in
+  match fv_short_name head with
+  | Some "squash"
+  | Some "b2t" ->
+    (match filter_explicit args with | [inner] -> inner | _ -> t)
+  | _ -> t
+
+(* Extract an equality `a = b` from a term.
+   F* represents `a = b` as either `eq2 #ty a b` or `op_Equality #ty a b`. *)
+let extract_eq (t: term) : Tac (term & term) =
+  let t' = unwrap_squash t in
+  let (head, raw_args) = collect_app t' in
+  let args = filter_explicit raw_args in
+  match fv_short_name head, args with
+  | Some "eq2",         [lhs; rhs]
+  | Some "op_Equality", [lhs; rhs] -> (lhs, rhs)
+  | name, _ ->
+    fail ("expected equality, got head="
+          ^ (match name with Some n -> n | None -> "?")
+          ^ " with " ^ string_of_int (List.Tot.length args) ^ " explicit args")
+
+(* Map in the Tac effect, since List.Tot.map is pure *)
+let rec tac_map (#a #b: Type) (f: a -> Tac b) (l: list a) : Tac (list b) =
+  match l with
+  | [] -> []
+  | x :: xs -> let y = f x in y :: tac_map f xs
+
+(* ================================================================
+   Section 3: Pattern & Expression Extraction
+   ================================================================ *)
+
+(* Extract a pattern from the LHS argument.
+   Recognizes:
+   - Variables (named or BVar)  -> PVar
+   - if-then-else               -> PIte
+   - Function applications      -> PApp *)
+let rec extract_pat (m: list (nat & string)) (offset: nat) (t: term) : Tac cpat =
+  match try_ite t with
+  | Some (c, et, tb, ef, fb) ->
+    let off_t : nat = offset + et in
+    let off_f : nat = offset + ef in
+    PIte (extract_pat m offset c) (extract_pat m off_t tb) (extract_pat m off_f fb)
+  | None ->
+    let (head, raw_args) = collect_app t in
+    let args = filter_explicit raw_args in
+    if List.Tot.length args > 0 then
+      (match fv_short_name head with
+       | Some fn -> PApp fn (tac_map (extract_pat m offset) args)
+       | None ->
+         (match var_name m offset head with
+          | Some n -> PApp n (tac_map (extract_pat m offset) args)
+          | None -> fail ("pattern app: cannot resolve head: " ^ term_to_string head)))
+    else
+      (match var_name m offset t with
+       | Some n -> PVar n
+       | None -> fail ("pattern: cannot recognize: " ^ term_to_string t))
+
+(* Extract an expression from the RHS.
+   Recognizes:
+   - Variables (named or BVar)    -> EVar
+   - Boolean literals              -> EBool
+   - if-then-else                  -> EIte
+   - Function applications (FVar) -> EApp *)
+let rec extract_expr (m: list (nat & string)) (offset: nat) (t: term) : Tac cexpr =
+  (* Check for boolean literals first *)
+  (match inspect_ln t with
+   | Tv_Const C_True  -> EBool true
+   | Tv_Const C_False -> EBool false
+   | _ ->
+     match try_ite t with
+     | Some (c, et, tb, ef, fb) ->
+       let off_t : nat = offset + et in
+       let off_f : nat = offset + ef in
+       EIte (extract_expr m offset c) (extract_expr m off_t tb) (extract_expr m off_f fb)
+     | None ->
+       let (head, raw_args) = collect_app t in
+       let args = filter_explicit raw_args in
+       if List.Tot.length args > 0 then
+         (match fv_short_name head with
+          | Some fn -> EApp fn (tac_map (extract_expr m offset) args)
+          | None -> fail ("expr: application head is not FVar: " ^ term_to_string head))
+       else
+         (match var_name m offset t with
+          | Some n -> EVar n
+          | None -> fail ("expr: cannot recognize: " ^ term_to_string t)))
+
+(* ================================================================
+   Section 4: Arrow Stripping & Index Map
+   ================================================================ *)
+
+(* Strip the Tv_Arrow chain from a lemma type:
+     (#eb:pos) -> (#sb:pos) -> (c:bool) -> (t:float eb sb) -> (e:float eb sb)
+       -> Lemma (...)
+   Returns: parameter names [eb;sb;c;t;e] and the final computation, C_Lemma. *)
+let rec strip_arrows (t: term) : Tac (list string & comp) =
+  match inspect_ln t with
+  | Tv_Arrow binder c ->
+    let name = unseal (inspect_binder binder).ppname in
+    (match inspect_comp c with
+     | C_Total ret ->
+       let (names, final_c) = strip_arrows ret in
+       (name :: names, final_c)
+     | _ -> ([name], c))
+  | _ -> fail ("expected arrow type, got: " ^ term_to_string t)
+
+(* Build de Bruijn index to name map.
+   Binders collected outer-to-inner: [eb; sb; c; t; e]
+   De Bruijn indices are inner-to-outer: e=0, t=1, c=2, sb=3, eb=4
+   So we reverse the list and pair with ascending indices. *)
+let build_idx_map (names: list string) : Tot (list (nat & string)) =
+  let rev_names = List.Tot.rev names in
+  let rec aux (i: nat) (ns: list string) : Tot (list (nat & string)) (decreases ns) =
+    match ns with
+    | [] -> []
+    | n :: rest -> (i, n) :: aux (i + 1) rest
+  in
+  aux 0 rev_names
+
+(* ================================================================
+   Section 5: C++ Code Generation
+   ================================================================ *)
+
+(* Map an F* IEEE754 function name to the corresponding Z3 C++ builder.
+   The "is_*" predicates in IEEE754.fst correspond directly to
+   fpa_util::mk_is_* in Z3's C++ API. *)
+let cpp_builder_name (fn: string) : string =
+  match fn with
+  | "is_nan"      -> "m_util.mk_is_nan"
+  | "is_inf"      -> "m_util.mk_is_inf"
+  | "is_normal"   -> "m_util.mk_is_normal"
+  | "is_negative" -> "m_util.mk_is_negative"
+  | "is_positive" -> "m_util.mk_is_positive"
+  | "is_zero"     -> "m_util.mk_is_zero"
+  | _             -> "m_util.mk_" ^ fn
+
+(* Collect all variable names from a pattern (for C++ declarations) *)
+let rec pat_vars (p: cpat) : Tot (list string) (decreases p) =
+  match p with
+  | PVar n       -> [n]
+  | PIte c t e   -> pat_vars c @ pat_vars t @ pat_vars e
+  | PApp _ args  -> pat_vars_list args
+
+and pat_vars_list (ps: list cpat) : Tot (list string) (decreases ps) =
+  match ps with
+  | []      -> []
+  | x :: xs -> pat_vars x @ pat_vars_list xs
+
+(* Generate: expr *c, *t, *e; *)
+let gen_decls (p: cpat) : string =
+  let vars = pat_vars p in
+  match vars with
+  | []  -> ""
+  | [v] -> "    expr *" ^ v ^ ";"
+  | _   -> "    expr *" ^ FStar.String.concat ", *" vars ^ ";"
+
+(* Generate the C++ condition that matches the LHS pattern.
+   For PIte(c,t,e): m().is_ite(arg1, c, t, e) *)
+let gen_condition (arg: string) (p: cpat) : string =
+  match p with
+  | PIte (PVar c) (PVar t) (PVar e) ->
+    "m().is_ite(" ^ arg ^ ", " ^ c ^ ", " ^ t ^ ", " ^ e ^ ")"
+  | PApp fn args ->
+    (match fn, args with
+     | "to_fp_of_int", [PVar _rm; PVar x] ->
+       "m_util.is_to_fp(" ^ arg ^ ") && to_app(" ^ arg ^ ")->get_num_args() == 2"
+       ^ " /* rm=" ^ _rm ^ ", int_expr=" ^ x ^ " */"
+     | _ ->
+       "/* TODO: extend gen_condition for " ^ fn ^ " */")
+  | PVar _ -> "true /* variable pattern, always matches */"
+  | _ -> "/* TODO: extend gen_condition for nested patterns */"
+
+(* Generate a C++ expression from the RHS IR *)
+let rec gen_rhs_expr (e: cexpr) : Tot string (decreases e) =
+  match e with
+  | EVar  n       -> n
+  | EBool true    -> "m().mk_true()"
+  | EBool false   -> "m().mk_false()"
+  | EIte  c t e   ->
+    "m().mk_ite(" ^ gen_rhs_expr c ^ ", "
+                  ^ gen_rhs_expr t ^ ", "
+                  ^ gen_rhs_expr e ^ ")"
+  | EApp fn args  ->
+    cpp_builder_name fn ^ "("
+    ^ gen_rhs_expr_list args ^ ")"
+
+and gen_rhs_expr_list (es: list cexpr) : Tot string (decreases es) =
+  (* Comma-separated list for C++ function arguments.  Empty list yields ""
+     so EApp fn [] produces fn_name(), which is valid C++ for zero-arg calls
+     (e.g. builder helper functions that take no explicit arguments). *)
+  match es with
+  | []      -> ""
+  | [e]     -> gen_rhs_expr e
+  | e :: rest -> gen_rhs_expr e ^ ", " ^ gen_rhs_expr_list rest
+
+(* Generate the complete C++ rewrite case *)
+let gen_cpp (top_fn: string) (arg: string) (pat: cpat) (rhs: cexpr) : string =
+  let decls = gen_decls pat in
+  let cond  = gen_condition arg pat in
+  let body  = gen_rhs_expr rhs in
+  (if FStar.String.length decls > 0 then decls ^ "\n" else "")
+  ^ "    if (" ^ cond ^ ") {\n"
+  ^ "        result = " ^ body ^ ";\n"
+  ^ "        return BR_REWRITE2;\n"
+  ^ "    }"
+
+(* ================================================================
+   Section 6: Main Extraction Entry Point
+   ================================================================ *)
+
+(**
+  Given a quoted lemma name, extract and return C++ rewriter code.
+  The generated code is a self-contained if-block that can be placed
+  directly inside the corresponding mk_* function in fpa_rewriter.cpp.
+
+  Usage:
+    run_tactic (fun () -> print (extract_rewrite (quote lemma_is_nan_ite)))
+
+  or to splice a comment into an F* file:
+    let _ = assert_norm (True);
+            run_tactic (fun () -> print (extract_rewrite (quote lemma_is_nan_ite)))
+
+  The lemma must have the shape:
+    let lemma_<name> (#eb #sb: pos) ... : Lemma (top_fn LHS_pattern = RHS) = ...
+
+  where top_fn is an IEEE754 classification predicate (is_nan, is_inf, is_normal).
+
+  For the argument name passed to the generated is_ite / is_to_fp check,
+  "arg1" is assumed (the standard name in fpa_rewriter.cpp mk_* functions).
+**)
+let extract_rewrite (lemma: term) : Tac string =
+  let env = top_env () in
+  let ty = tc env lemma in
+
+  (* 1. Strip forall binders, collect parameter names *)
+  let (param_names, final_comp) = strip_arrows ty in
+  let idx_map = build_idx_map param_names in
+
+  (* 2. Get the equality from the Lemma postcondition.
+     For `Lemma P`, the comp is C_Lemma l_True (fun _ -> b2t P) [].
+     The postcondition is a function taking the return value as argument.
+     We peel off the leading Tv_Abs to get the raw proposition.
+     Inside the abs body, all de Bruijn indices are shifted by 1 relative
+     to the outer scope, so we pass offset=1 to extract_pat/extract_expr. *)
+  let (post, post_offset) =
+    match inspect_comp final_comp with
+    | C_Lemma _ post _ ->
+      (match inspect_ln post with
+       | Tv_Abs _ body -> (body, 1)
+       | _ -> (post, 0))
+    | _ -> fail "expected Lemma computation type" in
+
+  (* 3. Extract LHS = RHS from the postcondition *)
+  let (lhs, rhs) = extract_eq post in
+
+  (* 4. Decompose LHS: top_fn(argument_pattern).
+     The top_fn is the IEEE754 classification predicate whose
+     mk_* method we are extending in fpa_rewriter.
+     We expect exactly one explicit argument on the LHS. *)
+  let (head, raw_args) = collect_app lhs in
+  let args = filter_explicit raw_args in
+  let top_fn =
+    match fv_short_name head with
+    | Some n -> n
+    | None -> fail ("LHS head is not a free variable: " ^ term_to_string head) in
+  let arg_term =
+    match args with
+    | [a] -> a
+    | _ ->
+      fail ("expected exactly one explicit arg on LHS, got "
+            ^ string_of_int (List.Tot.length args)
+            ^ " for top_fn=" ^ top_fn) in
+
+  (* 5. Extract the argument pattern and the RHS expression *)
+  let pat      = extract_pat  idx_map post_offset arg_term in
+  let rhs_expr = extract_expr idx_map post_offset rhs in
+
+  (* 6. Emit C++ code.
+     "arg1" is the standard name for the argument in mk_* functions of
+     fpa_rewriter.cpp, e.g. br_status fpa_rewriter::mk_is_nan(expr *arg1, ...). *)
+  gen_cpp top_fn "arg1" pat rhs_expr
+
+
+(* ================================================================
+   Section 7: Extraction Examples
+   ================================================================
+
+   Run these with:
+     fstar.exe --include . IEEE754.fst FPARewriterRules.fst RewriteCodeGen.fst
+
+   The `run_tactic (fun () -> print ...)` calls emit the generated C++ to
+   stdout during F* typechecking.  The output can be captured and placed
+   directly in fpa_rewriter_rules.h (wrapped in an appropriate #define).
+
+   Expected output for lemma_is_nan_ite:
+   ================================================================
+     expr *c, *t, *e;
+     if (m().is_ite(arg1, c, t, e)) {
+         result = m().mk_ite(c, m_util.mk_is_nan(t), m_util.mk_is_nan(e));
+         return BR_REWRITE2;
+     }
+   ================================================================
+
+   Expected output for lemma_is_inf_ite:
+   ================================================================
+     expr *c, *t, *e;
+     if (m().is_ite(arg1, c, t, e)) {
+         result = m().mk_ite(c, m_util.mk_is_inf(t), m_util.mk_is_inf(e));
+         return BR_REWRITE2;
+     }
+   ================================================================
+
+   Expected output for lemma_is_normal_ite:
+   ================================================================
+     expr *c, *t, *e;
+     if (m().is_ite(arg1, c, t, e)) {
+         result = m().mk_ite(c, m_util.mk_is_normal(t), m_util.mk_is_normal(e));
+         return BR_REWRITE2;
+     }
+   ================================================================
+*)
+
+open FPARewriterRules
+
+(* Helper: extract and print one lemma's C++ rewrite rule. *)
+let print_rewrite (label: string) (lemma: term) : Tac unit =
+  print ("\n=== " ^ label ^ " ===\n");
+  print (extract_rewrite lemma)
+
+(* Construct a term reference to a top-level name in FPARewriterRules
+   without instantiating implicit arguments.  Using pack_fv avoids the
+   elaboration that quote performs, which in F* 2026 fails for polymorphic
+   lemmas whose implicit type arguments (eb, sb: pos) cannot be inferred
+   from the call site. *)
+let lemma_ref (name: string) : term =
+  pack_ln (Tv_FVar (pack_fv ["FPARewriterRules"; name]))
+
+(* Demonstrate extraction of the three ite-pushthrough lemmas.
+   Running this file with F* prints the generated C++ for each rule. *)
+let _ =
+  run_tactic (fun () ->
+    iter (fun (label, lemma) -> print_rewrite label lemma)
+      [ ("lemma_is_nan_ite",    lemma_ref "lemma_is_nan_ite");
+        ("lemma_is_inf_ite",    lemma_ref "lemma_is_inf_ite");
+        ("lemma_is_normal_ite", lemma_ref "lemma_is_normal_ite") ])

fstar/extract.sh

@@ -0,0 +1,47 @@
+#!/usr/bin/env bash
+# extract.sh
+#
+# Run the Meta-F* reflection-based extraction to generate C++ rewrite rules
+# from the F* lemmas in this directory.
+#
+# Usage (from the fstar/ directory):
+#   ./extract.sh
+#
+# Usage (from the repo root):
+#   fstar/extract.sh
+#
+# Output:
+#   Prints the generated C++ rules to stdout.
+#   Exits non-zero if F* typechecking or tactic execution fails.
+#
+# Requirements:
+#   fstar.exe on PATH (F* 2024.09.05 or later recommended).
+#   The three source files must be present:
+#     IEEE754.fst, FPARewriterRules.fst, RewriteCodeGen.fst
+
+set -euo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+cd "$SCRIPT_DIR"
+
+if ! command -v fstar.exe &>/dev/null; then
+    echo "ERROR: fstar.exe not found on PATH." >&2
+    echo "Install F* 2026.03.24+ from https://github.com/FStarLang/FStar/releases" >&2
+    exit 1
+fi
+
+echo "=== F* version ===" >&2
+fstar.exe --version >&2
+
+echo "" >&2
+echo "=== Running Meta-F* extraction ===" >&2
+
+# F* writes tactic print() output to stdout.
+# Verification progress and errors go to stderr.
+fstar.exe --include . \
+    IEEE754.fst \
+    FPARewriterRules.fst \
+    RewriteCodeGen.fst
+
+echo "" >&2
+echo "=== Extraction complete ===" >&2

src/ast/rewriter/fpa_rewriter.cpp

@@ -17,6 +17,7 @@ Notes:
 
 --*/
 #include "ast/rewriter/fpa_rewriter.h"
+#include "ast/rewriter/fpa_rewriter_rules.h"
 #include "params/fpa_rewriter_params.hpp"
 #include "ast/ast_smt2_pp.h"
 
@@ -430,6 +431,8 @@ br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg
         }
     }
 
+    FPA_REWRITE_FMA_ZERO_MUL(arg1, arg2, arg3, arg4, result);
+
     return BR_FAILED;
 }
 
@@ -588,6 +591,9 @@ br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) {
         return BR_DONE;
     }
 
+    FPA_REWRITE_IS_NAN_TO_FP_INT(arg1, result);
+    FPA_REWRITE_IS_NAN_ITE(arg1, result);
+
     return BR_FAILED;
 }
 
@@ -599,6 +605,9 @@ br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) {
         return BR_DONE;
     }
 
+    FPA_REWRITE_IS_INF_TO_FP_INT(arg1, result);
+    FPA_REWRITE_IS_INF_ITE(arg1, result);
+
     return BR_FAILED;
 }
 
@@ -610,6 +619,9 @@ br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) {
         return BR_DONE;
     }
 
+    FPA_REWRITE_IS_NORMAL_TO_FP_INT(arg1, result);
+    FPA_REWRITE_IS_NORMAL_ITE(arg1, result);
+
     return BR_FAILED;
 }
 
@@ -844,3 +856,55 @@ br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
 
     return BR_FAILED;
 }
+
+// mk_is_inf_of_int: compute isInf(to_fp(rm, to_real(x))) as an integer constraint.
+// For integer x, to_fp is never NaN or subnormal (IEEE 754-2019 §5.4.1), so
+// the result is one of: ±zero, normal, or ±infinity.
+// Overflow to ±infinity depends only on |x| relative to the format's
+// representable range and the rounding mode.
+// Corresponds to lemma_is_inf_to_fp_int_{rne,rna,rtp,rtn,rtz} in
+// fstar/FPARewriterRules.fst.
+expr_ref fpa_rewriter::mk_is_inf_of_int(mpf_rounding_mode rm, unsigned ebits, unsigned sbits, expr * int_expr) {
+    arith_util & au = m_util.au();
+
+    scoped_mpf max_val(m_fm);
+    m_fm.mk_max_value(ebits, sbits, false, max_val);
+    scoped_mpq max_q(m_fm.mpq_manager());
+    m_fm.to_rational(max_val, max_q);
+    rational max_finite(max_q);
+
+    mpf_exp_t max_exp = m_fm.mk_max_exp(ebits);
+    int ulp_exp = (int)max_exp - (int)sbits + 1;
+    rational half_ulp = rational::power_of_two((unsigned)ulp_exp) / rational(2);
+
+    expr_ref r(m());
+
+    switch (rm) {
+    case MPF_ROUND_NEAREST_TEVEN:
+    case MPF_ROUND_NEAREST_TAWAY: {
+        // Overflow when |x| >= max_finite + ULP/2.
+        // At the boundary, MAX_FINITE has an odd significand so both RNE
+        // and RNA round away from MAX_FINITE, i.e. to infinity.
+        rational threshold = max_finite + half_ulp;
+        expr_ref thr(au.mk_int(threshold), m());
+        expr_ref neg_thr(au.mk_int(-threshold), m());
+        r = m().mk_or(au.mk_ge(int_expr, thr), au.mk_le(int_expr, neg_thr));
+        break;
+    }
+    case MPF_ROUND_TOWARD_POSITIVE:
+        // RTP: positive overflow only; negative values round toward zero.
+        r = au.mk_gt(int_expr, au.mk_int(max_finite));
+        break;
+    case MPF_ROUND_TOWARD_NEGATIVE:
+        // RTN: negative overflow only; positive values round toward zero.
+        r = au.mk_lt(int_expr, au.mk_int(-max_finite));
+        break;
+    case MPF_ROUND_TOWARD_ZERO:
+        // RTZ: truncation toward zero never overflows to infinity.
+        r = m().mk_false();
+        break;
+    }
+
+    TRACE(fp_rewriter, tout << "isInf(to_fp(rm, int)) -> " << mk_ismt2_pp(r, m()) << "\n";);
+    return r;
+}

src/ast/rewriter/fpa_rewriter.h

@@ -88,5 +88,10 @@ public:
     br_status mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
 
     br_status mk_bvwrap(expr * arg, expr_ref & result);
+
+    // Helper used by FPA_REWRITE_IS_INF_TO_FP_INT and FPA_REWRITE_IS_NORMAL_TO_FP_INT:
+    // compute isInf(to_fp(rm, to_real(int_expr))) as a pure integer constraint.
+    // Corresponds to lemma_is_inf_to_fp_int_* in fstar/FPARewriterRules.fst.
+    expr_ref mk_is_inf_of_int(mpf_rounding_mode rm, unsigned ebits, unsigned sbits, expr * int_expr);
 };
 

src/ast/rewriter/fpa_rewriter_rules.h

@@ -0,0 +1,307 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    fpa_rewriter_rules.h
+
+Abstract:
+
+    Rewrite rule macros for floating-point arithmetic, whose correctness
+    is proved by F* lemmas in fstar/FPARewriterRules.fst.
+
+    The ite-pushthrough macros (FPA_REWRITE_IS_NAN_ITE, FPA_REWRITE_IS_INF_ITE,
+    FPA_REWRITE_IS_NORMAL_ITE) can be regenerated programmatically by running
+    the Meta-F* extraction tactic in fstar/RewriteCodeGen.fst (from the repo root):
+
+      cd /path/to/z3/fstar
+      fstar.exe --include . IEEE754.fst FPARewriterRules.fst RewriteCodeGen.fst
+
+    The correspondence between each macro and the F* lemma it implements is
+    documented at each macro definition below.
+
+    Macros are designed for use inside member functions of fpa_rewriter,
+    where m(), m_util, m_fm, and mk_is_inf_of_int are available.
+    Internal variables use the _fpa_ prefix to minimize name collisions.
+
+Author:
+
+    (extracted from F* in fstar/FPARewriterRules.fst,
+     ite-pushthrough rules generated via fstar/RewriteCodeGen.fst)
+
+Notes:
+
+--*/
+#pragma once
+
+// -----------------------------------------------------------------------
+// FPA_REWRITE_IS_NAN_TO_FP_INT
+//
+// F* lemma: lemma_is_nan_to_fp_int
+//   isNaN(to_fp(rm, real_or_int)) = false
+// IEEE 754-2019 §5.4.1: converting a real or integer value never produces NaN.
+//
+// Applies to:  mk_is_nan(arg1, result)
+// -----------------------------------------------------------------------
+#define FPA_REWRITE_IS_NAN_TO_FP_INT(arg1, result) \
+    do { \
+        if (m_util.is_to_fp(arg1)) { \
+            app * _fpa_a = to_app(arg1); \
+            if (_fpa_a->get_num_args() == 2 && \
+                (m_util.au().is_real(_fpa_a->get_arg(1)) || \
+                 m_util.au().is_int(_fpa_a->get_arg(1)))) { \
+                result = m().mk_false(); \
+                return BR_DONE; \
+            } \
+        } \
+    } while (0)
+
+
+// -----------------------------------------------------------------------
+// FPA_REWRITE_IS_NAN_ITE
+//
+// F* lemma: lemma_is_nan_ite
+//   isNaN(ite(c, t, e)) = ite(c, isNaN(t), isNaN(e))
+// When both branches are concrete FP numerals the rewriter evaluates
+// the predicate statically and folds the result into the condition.
+//
+// Generated by: extract_rewrite (quote lemma_is_nan_ite) in RewriteCodeGen.fst
+// Applies to:   mk_is_nan(arg1, result)
+// -----------------------------------------------------------------------
+#define FPA_REWRITE_IS_NAN_ITE(arg1, result) \
+    do { \
+        expr *_fpa_c = nullptr, *_fpa_t = nullptr, *_fpa_e = nullptr; \
+        if (m().is_ite(arg1, _fpa_c, _fpa_t, _fpa_e)) { \
+            scoped_mpf _fpa_vt(m_fm), _fpa_ve(m_fm); \
+            if (m_util.is_numeral(_fpa_t, _fpa_vt) && m_util.is_numeral(_fpa_e, _fpa_ve)) { \
+                result = m().mk_ite(_fpa_c, \
+                    m_fm.is_nan(_fpa_vt) ? m().mk_true() : m().mk_false(), \
+                    m_fm.is_nan(_fpa_ve) ? m().mk_true() : m().mk_false()); \
+                return BR_REWRITE2; \
+            } \
+        } \
+    } while (0)
+
+
+// -----------------------------------------------------------------------
+// FPA_REWRITE_IS_INF_TO_FP_INT
+//
+// F* lemmas: lemma_is_inf_to_fp_int_rne, _rna, _rtp, _rtn, _rtz
+//   isInf(to_fp(rm, to_real(int))) = integer overflow condition
+// Each rounding mode maps to a different threshold; computed by
+// mk_is_inf_of_int (see fpa_rewriter.cpp).
+//
+// Applies to:  mk_is_inf(arg1, result)
+// -----------------------------------------------------------------------
+#define FPA_REWRITE_IS_INF_TO_FP_INT(arg1, result) \
+    do { \
+        mpf_rounding_mode _fpa_rm; \
+        if (m_util.is_to_fp(arg1)) { \
+            app * _fpa_a = to_app(arg1); \
+            if (_fpa_a->get_num_args() == 2 && m_util.is_rm_numeral(_fpa_a->get_arg(0), _fpa_rm)) { \
+                expr * _fpa_inner = _fpa_a->get_arg(1); \
+                expr * _fpa_int_expr = nullptr; \
+                if (m_util.au().is_to_real(_fpa_inner)) { \
+                    expr * _fpa_unwrapped = to_app(_fpa_inner)->get_arg(0); \
+                    if (m_util.au().is_int(_fpa_unwrapped)) \
+                        _fpa_int_expr = _fpa_unwrapped; \
+                } \
+                else if (m_util.au().is_int(_fpa_inner)) \
+                    _fpa_int_expr = _fpa_inner; \
+                if (_fpa_int_expr) { \
+                    func_decl * _fpa_fd = _fpa_a->get_decl(); \
+                    unsigned _fpa_eb = _fpa_fd->get_parameter(0).get_int(); \
+                    unsigned _fpa_sb = _fpa_fd->get_parameter(1).get_int(); \
+                    result = mk_is_inf_of_int(_fpa_rm, _fpa_eb, _fpa_sb, _fpa_int_expr); \
+                    if (result) \
+                        return BR_REWRITE_FULL; \
+                } \
+            } \
+        } \
+    } while (0)
+
+
+// -----------------------------------------------------------------------
+// FPA_REWRITE_IS_INF_ITE
+//
+// F* lemma: lemma_is_inf_ite
+//   isInf(ite(c, t, e)) = ite(c, isInf(t), isInf(e))
+// When both branches are concrete FP numerals the predicate is evaluated
+// statically and folded into the condition.
+//
+// Generated by: extract_rewrite (quote lemma_is_inf_ite) in RewriteCodeGen.fst
+// Applies to:   mk_is_inf(arg1, result)
+// -----------------------------------------------------------------------
+#define FPA_REWRITE_IS_INF_ITE(arg1, result) \
+    do { \
+        expr *_fpa_c = nullptr, *_fpa_t = nullptr, *_fpa_e = nullptr; \
+        if (m().is_ite(arg1, _fpa_c, _fpa_t, _fpa_e)) { \
+            scoped_mpf _fpa_vt(m_fm), _fpa_ve(m_fm); \
+            if (m_util.is_numeral(_fpa_t, _fpa_vt) && m_util.is_numeral(_fpa_e, _fpa_ve)) { \
+                result = m().mk_ite(_fpa_c, \
+                    m_fm.is_inf(_fpa_vt) ? m().mk_true() : m().mk_false(), \
+                    m_fm.is_inf(_fpa_ve) ? m().mk_true() : m().mk_false()); \
+                return BR_REWRITE2; \
+            } \
+        } \
+    } while (0)
+
+
+// -----------------------------------------------------------------------
+// FPA_REWRITE_IS_NORMAL_TO_FP_INT
+//
+// F* lemma: lemma_is_normal_to_fp_int
+//   isNormal(to_fp(rm, to_real(int))) = int != 0 AND NOT isInf(to_fp(rm, int))
+// For integer inputs: never NaN, never subnormal, so the float is normal
+// iff it is nonzero (int != 0) and does not overflow (NOT isInf).
+//
+// Applies to:  mk_is_normal(arg1, result)
+// -----------------------------------------------------------------------
+#define FPA_REWRITE_IS_NORMAL_TO_FP_INT(arg1, result) \
+    do { \
+        mpf_rounding_mode _fpa_rm; \
+        if (m_util.is_to_fp(arg1)) { \
+            app * _fpa_a = to_app(arg1); \
+            if (_fpa_a->get_num_args() == 2 && m_util.is_rm_numeral(_fpa_a->get_arg(0), _fpa_rm)) { \
+                expr * _fpa_inner = _fpa_a->get_arg(1); \
+                expr * _fpa_int_expr = nullptr; \
+                if (m_util.au().is_to_real(_fpa_inner)) { \
+                    expr * _fpa_unwrapped = to_app(_fpa_inner)->get_arg(0); \
+                    if (m_util.au().is_int(_fpa_unwrapped)) \
+                        _fpa_int_expr = _fpa_unwrapped; \
+                } \
+                else if (m_util.au().is_int(_fpa_inner)) \
+                    _fpa_int_expr = _fpa_inner; \
+                if (_fpa_int_expr) { \
+                    func_decl * _fpa_fd = _fpa_a->get_decl(); \
+                    unsigned _fpa_eb = _fpa_fd->get_parameter(0).get_int(); \
+                    unsigned _fpa_sb = _fpa_fd->get_parameter(1).get_int(); \
+                    arith_util & _fpa_au = m_util.au(); \
+                    expr_ref _fpa_nz(m().mk_not(m().mk_eq(_fpa_int_expr, _fpa_au.mk_int(0))), m()); \
+                    expr_ref _fpa_ic = mk_is_inf_of_int(_fpa_rm, _fpa_eb, _fpa_sb, _fpa_int_expr); \
+                    result = m().mk_and(_fpa_nz, m().mk_not(_fpa_ic)); \
+                    return BR_REWRITE_FULL; \
+                } \
+            } \
+        } \
+    } while (0)
+
+
+// -----------------------------------------------------------------------
+// FPA_REWRITE_IS_NORMAL_ITE
+//
+// F* lemma: lemma_is_normal_ite
+//   isNormal(ite(c, t, e)) = ite(c, isNormal(t), isNormal(e))
+// When both branches are concrete FP numerals the predicate is evaluated
+// statically and folded into the condition.
+//
+// Generated by: extract_rewrite (quote lemma_is_normal_ite) in RewriteCodeGen.fst
+// Applies to:   mk_is_normal(arg1, result)
+// -----------------------------------------------------------------------
+#define FPA_REWRITE_IS_NORMAL_ITE(arg1, result) \
+    do { \
+        expr *_fpa_c = nullptr, *_fpa_t = nullptr, *_fpa_e = nullptr; \
+        if (m().is_ite(arg1, _fpa_c, _fpa_t, _fpa_e)) { \
+            scoped_mpf _fpa_vt(m_fm), _fpa_ve(m_fm); \
+            if (m_util.is_numeral(_fpa_t, _fpa_vt) && m_util.is_numeral(_fpa_e, _fpa_ve)) { \
+                result = m().mk_ite(_fpa_c, \
+                    m_fm.is_normal(_fpa_vt) ? m().mk_true() : m().mk_false(), \
+                    m_fm.is_normal(_fpa_ve) ? m().mk_true() : m().mk_false()); \
+                return BR_REWRITE2; \
+            } \
+        } \
+    } while (0)
+
+
+// -----------------------------------------------------------------------
+// FPA_REWRITE_FMA_ZERO_MUL
+//
+// F* lemmas: lemma_fma_zero_nan_addend, lemma_fma_zero_nan_mul,
+//            lemma_fma_zero_inf_mul, lemma_fma_zero_finite_decomposes,
+//            lemma_fma_zero_const_addend, lemma_fma_zero_const_{finite,nan_inf}_arm,
+//            lemma_fma_zero_general_{finite,nan_inf}_arm, lemma_fma_zero_product_sign
+//
+// fma(rm, ±0, y, z) or fma(rm, x, ±0, z): when one multiplicand is a
+// concrete zero the full FMA bit-blast circuit is unnecessary.
+// IEEE 754-2019 §6.3: 0 * finite = ±0 (exact); 0 * inf = NaN.
+//
+// Case breakdown (mirroring the F* section-1 lemmas):
+//   (a) addend is NaN                        → NaN   (lemma_fma_zero_nan_addend)
+//   (b) other_mul is concrete NaN or inf     → NaN   (lemma_fma_zero_nan_mul/inf_mul)
+//   (c) other_mul is concrete finite         → fp.add(rm, product, addend)
+//                                                     (lemma_fma_zero_finite_decomposes)
+//   (d) other_mul symbolic, addend concrete nonzero finite
+//                                            → ite(isFinite(other_mul), addend, NaN)
+//                                                     (lemma_fma_zero_const_finite/nan_inf_arm)
+//   (e) fully symbolic                       → ite(isFinite(other_mul),
+//                                                   fp.add(rm, product_zero, addend), NaN)
+//                                                     (lemma_fma_zero_general_finite/nan_inf_arm)
+//
+// Applies to:  mk_fma(arg1, arg2, arg3, arg4, result)
+//   arg1 = rounding mode, arg2 = x, arg3 = y, arg4 = addend
+// -----------------------------------------------------------------------
+#define FPA_REWRITE_FMA_ZERO_MUL(arg1, arg2, arg3, arg4, result) \
+    do { \
+        mpf_rounding_mode _fpa_rm; \
+        if (m_util.is_rm_numeral(arg1, _fpa_rm)) { \
+            expr *_fpa_other = nullptr; \
+            bool _fpa_zero_neg = false; \
+            scoped_mpf _fpa_vzero(m_fm), _fpa_v3(m_fm); \
+            if (m_util.is_numeral(arg2, _fpa_vzero) && m_fm.is_zero(_fpa_vzero)) { \
+                _fpa_other = arg3; \
+                _fpa_zero_neg = m_fm.is_neg(_fpa_vzero); \
+            } \
+            else if (m_util.is_numeral(arg3, _fpa_v3) && m_fm.is_zero(_fpa_v3)) { \
+                _fpa_other = arg2; \
+                _fpa_zero_neg = m_fm.is_neg(_fpa_v3); \
+                m_fm.set(_fpa_vzero, _fpa_v3); \
+            } \
+            if (_fpa_other) { \
+                TRACE(fp_rewriter, tout << "fma zero-multiplicand simplification\n";); \
+                sort *_fpa_s = arg4->get_sort(); \
+                expr_ref _fpa_nan(m_util.mk_nan(_fpa_s), m()); \
+                if (m_util.is_nan(arg4)) { \
+                    result = _fpa_nan; \
+                    return BR_DONE; \
+                } \
+                scoped_mpf _fpa_vo(m_fm); \
+                if (m_util.is_numeral(_fpa_other, _fpa_vo) && \
+                    (m_fm.is_nan(_fpa_vo) || m_fm.is_inf(_fpa_vo))) { \
+                    result = _fpa_nan; \
+                    return BR_DONE; \
+                } \
+                if (m_util.is_numeral(_fpa_other, _fpa_vo)) { \
+                    scoped_mpf _fpa_prod(m_fm); \
+                    m_fm.mul(_fpa_rm, _fpa_vzero, _fpa_vo, _fpa_prod); \
+                    SASSERT(m_fm.is_zero(_fpa_prod)); \
+                    result = m_util.mk_add(arg1, m_util.mk_value(_fpa_prod), arg4); \
+                    return BR_REWRITE2; \
+                } \
+                scoped_mpf _fpa_vz(m_fm); \
+                if (m_util.is_numeral(arg4, _fpa_vz) && \
+                    !m_fm.is_zero(_fpa_vz) && !m_fm.is_nan(_fpa_vz)) { \
+                    expr_ref _fpa_fin_c(m()); \
+                    _fpa_fin_c = m().mk_not(m().mk_or(m_util.mk_is_nan(_fpa_other), \
+                                                       m_util.mk_is_inf(_fpa_other))); \
+                    result = m().mk_ite(_fpa_fin_c, arg4, _fpa_nan); \
+                    return BR_REWRITE_FULL; \
+                } \
+                expr_ref _fpa_pzero(m_util.mk_pzero(_fpa_s), m()); \
+                expr_ref _fpa_nzero(m_util.mk_nzero(_fpa_s), m()); \
+                expr_ref _fpa_prod_zero(m()); \
+                if (_fpa_zero_neg) \
+                    _fpa_prod_zero = m().mk_ite(m_util.mk_is_negative(_fpa_other), \
+                                                _fpa_pzero, _fpa_nzero); \
+                else \
+                    _fpa_prod_zero = m().mk_ite(m_util.mk_is_negative(_fpa_other), \
+                                                _fpa_nzero, _fpa_pzero); \
+                expr_ref _fpa_fin_g(m()); \
+                _fpa_fin_g = m().mk_not(m().mk_or(m_util.mk_is_nan(_fpa_other), \
+                                                   m_util.mk_is_inf(_fpa_other))); \
+                result = m().mk_ite(_fpa_fin_g, \
+                                    m_util.mk_add(arg1, _fpa_prod_zero, arg4), \
+                                    _fpa_nan); \
+                return BR_REWRITE_FULL; \
+            } \
+        } \
+    } while (0)