diff --git a/.github/workflows/fstar-extract.yml b/.github/workflows/fstar-extract.yml new file mode 100644 index 000000000..1b1a5a74f --- /dev/null +++ b/.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 diff --git a/fstar/FPARewriterRules.fst b/fstar/FPARewriterRules.fst new file mode 100644 index 000000000..766edf536 --- /dev/null +++ b/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 diff --git a/fstar/IEEE754.fst b/fstar/IEEE754.fst new file mode 100644 index 000000000..185efc50c --- /dev/null +++ b/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) diff --git a/fstar/README.md b/fstar/README.md new file mode 100644 index 000000000..f4a34cd8a --- /dev/null +++ b/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. diff --git a/fstar/RewriteCodeGen.fst b/fstar/RewriteCodeGen.fst new file mode 100644 index 000000000..b84a64574 --- /dev/null +++ b/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_ (#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") ]) diff --git a/fstar/extract.sh b/fstar/extract.sh new file mode 100755 index 000000000..741636984 --- /dev/null +++ b/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 diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index c2c888885..358a1c1f0 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/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; +} diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 333302eec..17d72ebc6 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/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); }; diff --git a/src/ast/rewriter/fpa_rewriter_rules.h b/src/ast/rewriter/fpa_rewriter_rules.h new file mode 100644 index 000000000..af12e2ce4 --- /dev/null +++ b/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)