From e3aa907098789d95d28ba69996ec1df1d1cd7263 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 3 Apr 2026 18:05:00 +0000 Subject: [PATCH 1/9] fstar: formalize FPA rewriter rules from PR #9038 in F* using IEEE 754 axioms Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7899b653-a7f0-443c-894a-32376baea5c0 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- fstar/FPARewriterRules.fst | 407 +++++++++++++++++++++++++++++++++++++ fstar/IEEE754.fst | 295 +++++++++++++++++++++++++++ fstar/README.md | 134 ++++++++++++ 3 files changed, 836 insertions(+) create mode 100644 fstar/FPARewriterRules.fst create mode 100644 fstar/IEEE754.fst create mode 100644 fstar/README.md diff --git a/fstar/FPARewriterRules.fst b/fstar/FPARewriterRules.fst new file mode 100644 index 000000000..5aa127f82 --- /dev/null +++ b/fstar/FPARewriterRules.fst @@ -0,0 +1,407 @@ +(* + 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++ line "fma(rm, ±0, y, NaN) = NaN". + The addend NaN propagates (IEEE 754-2019 §6.2, NaN payload rules). *) +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. *) +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. *) +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. *) +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. *) +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. + + 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_nan_y rm zero_val 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. *) + +(* 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_nan_y rm zero_val 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)))". *) +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 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. *) + +(* 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 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 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 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 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 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));" + + 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 rm x; (* is_nan f = false *) + ax_to_fp_int_not_subnormal rm x; (* is_subnormal f = false *) + ax_classification f; (* nan||inf||zero||normal||subnormal *) + if x = 0 then begin + ax_to_fp_int_zero 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 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)". *) +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. *) +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. *) +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_nan_y rm zero_val 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), + Z3 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 RNE x; + ax_is_inf_rne 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 RTZ x; + ax_is_inf_rtz x diff --git a/fstar/IEEE754.fst b/fstar/IEEE754.fst new file mode 100644 index 000000000..0faf2cd84 --- /dev/null +++ b/fstar/IEEE754.fst @@ -0,0 +1,295 @@ +(* + 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) -> Type0 + +(* ------------------------------------------------------------------ *) +(* 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 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 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 y: float eb sb) -> + Lemma (is_nan (fp_fma rm x y (nan #eb #sb)) = 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 y 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 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) + +(* 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 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 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..446978e7c --- /dev/null +++ b/fstar/README.md @@ -0,0 +1,134 @@ +# 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 | Formalized in | +|---|---|---| +| `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, ±0, y)` = sign(±0) 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 `()`. + +## Relationship to the C++ Code + +The following table maps each lemma to the corresponding C++ code in +`src/ast/rewriter/fpa_rewriter.cpp` after the PR is applied. + +| Lemma | C++ code | +|---|---| +| `lemma_fma_zero_nan_addend` | `if (m_util.is_nan(arg4)) { result = nan; return BR_DONE; }` | +| `lemma_fma_zero_nan_mul` | `if (m_util.is_numeral(other_mul, vo) && m_fm.is_nan(vo))` | +| `lemma_fma_zero_inf_mul` | `if (m_util.is_numeral(other_mul, vo) && m_fm.is_inf(vo))` | +| `lemma_fma_zero_finite_decomposes` | `m_util.mk_add(arg1, m_util.mk_value(product), arg4)` with `m_fm.mul(rm, vzero, vo, product)` | +| `lemma_fma_zero_const_addend` | `m().mk_ite(finite_cond, arg4, nan)` (z_const branch) | +| `lemma_fma_zero_general_*` | general `m().mk_ite(finite_cond, m_util.mk_add(...), nan)` | +| `lemma_is_nan_to_fp_int` | `mk_is_nan`: `result = m().mk_false(); return BR_DONE;` | +| `lemma_is_inf_to_fp_int_*` | `mk_is_inf_of_int` switch statement | +| `lemma_is_normal_to_fp_int` | `mk_is_normal`: `result = m().mk_and(not_zero, m().mk_not(inf_cond))` | +| `lemma_is_nan_ite` | `mk_is_nan`: ite-pushthrough block | +| `lemma_is_inf_ite` | `mk_is_inf`: ite-pushthrough block | +| `lemma_is_normal_ite` | `mk_is_normal`: ite-pushthrough block | + +## 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 + +To type-check these files with F\*, from this directory run: + +```sh +fstar.exe --include . IEEE754.fst FPARewriterRules.fst +``` + +F\* 2024.09.05 or later is recommended. 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. From 653c49ac5e06c06e3dec668ae956a5e931006f1f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 3 Apr 2026 18:05:55 +0000 Subject: [PATCH 2/9] fstar: address review comments - improve comments and table header clarity Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7899b653-a7f0-443c-894a-32376baea5c0 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- fstar/FPARewriterRules.fst | 4 ++-- fstar/README.md | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/fstar/FPARewriterRules.fst b/fstar/FPARewriterRules.fst index 5aa127f82..46fb2b92e 100644 --- a/fstar/FPARewriterRules.fst +++ b/fstar/FPARewriterRules.fst @@ -50,7 +50,7 @@ open IEEE754 (* ================================================================== *) (* 1a. fma(rm, ±0, y, NaN) = NaN - Source: C++ line "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). *) let lemma_fma_zero_nan_addend (#eb #sb: pos) @@ -381,7 +381,7 @@ let lemma_fma_zero_ite_nan_arm 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), - Z3 can derive is_inf y = true directly. *) + 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 diff --git a/fstar/README.md b/fstar/README.md index 446978e7c..971bb81c7 100644 --- a/fstar/README.md +++ b/fstar/README.md @@ -9,7 +9,7 @@ in the [F\*](https://www.fstar-lang.org/) proof assistant. PR #9038 adds three families of optimizations to `src/ast/rewriter/fpa_rewriter.cpp` that avoid expensive FP bit-blasting: -| Optimization | C++ function | Formalized in | +| 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 | @@ -54,7 +54,7 @@ Derived rewrite rules proved from `IEEE754.fst` axioms. | `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, ±0, y)` = sign(±0) XOR sign(y) | +| `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 From 1b73e5f1de00029880a29e714b7de7f4eba54ce3 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 5 Apr 2026 02:01:12 +0000 Subject: [PATCH 3/9] fstar: add fpa_rewriter_rules.h with C++ macros extracted from F* lemmas Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/46fcd3bf-be90-4098-8516-fde0f1e37cbf Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- fstar/FPARewriterRules.fst | 35 ++- fstar/README.md | 61 ++++-- src/ast/rewriter/fpa_rewriter.cpp | 64 ++++++ src/ast/rewriter/fpa_rewriter.h | 5 + src/ast/rewriter/fpa_rewriter_rules.h | 296 ++++++++++++++++++++++++++ 5 files changed, 433 insertions(+), 28 deletions(-) create mode 100644 src/ast/rewriter/fpa_rewriter_rules.h diff --git a/fstar/FPARewriterRules.fst b/fstar/FPARewriterRules.fst index 46fb2b92e..8594ab182 100644 --- a/fstar/FPARewriterRules.fst +++ b/fstar/FPARewriterRules.fst @@ -51,7 +51,8 @@ open IEEE754 (* 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). *) + 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) @@ -62,7 +63,8 @@ let lemma_fma_zero_nan_addend (* 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. *) + 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) @@ -74,7 +76,8 @@ let lemma_fma_zero_nan_mul (* 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. *) + 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) @@ -90,7 +93,8 @@ let lemma_fma_zero_inf_mul 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. *) + 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) @@ -105,7 +109,8 @@ let lemma_fma_zero_finite_decomposes 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. *) + 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) @@ -123,6 +128,7 @@ let lemma_fma_zero_const_addend 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 @@ -155,7 +161,8 @@ let lemma_fma_zero_const_nan_inf_arm 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. *) + 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 @@ -217,7 +224,8 @@ let lemma_fma_zero_product_sign (* 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)))". *) + (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) = @@ -227,7 +235,8 @@ let lemma_is_nan_to_fp_int (* --- 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. *) + 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 @@ -270,6 +279,7 @@ let lemma_is_inf_to_fp_int_rtz 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 @@ -322,7 +332,8 @@ let lemma_is_normal_to_fp_int (* 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)". *) + 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) = @@ -330,7 +341,8 @@ let lemma_is_nan_ite (* 3b. isInf(ite(c, t, e)) = ite(c, isInf(t), isInf(e)) - Source: same pattern in mk_is_inf. *) + 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) = @@ -338,7 +350,8 @@ let lemma_is_inf_ite (* 3c. isNormal(ite(c, t, e)) = ite(c, isNormal(t), isNormal(e)) - Source: same pattern in mk_is_normal. *) + 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) = diff --git a/fstar/README.md b/fstar/README.md index 971bb81c7..1bc56151b 100644 --- a/fstar/README.md +++ b/fstar/README.md @@ -20,7 +20,6 @@ that avoid expensive FP bit-blasting: ### `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, @@ -83,25 +82,53 @@ 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 `()`. +### `../src/ast/rewriter/fpa_rewriter_rules.h` + +C++ header containing one `#define` macro per rewrite rule, extracted from +the F\* lemmas. Each macro is annotated with a `[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 the corresponding C++ code in -`src/ast/rewriter/fpa_rewriter.cpp` after the PR is applied. +The following table maps each lemma to the corresponding C++ macro in +`src/ast/rewriter/fpa_rewriter_rules.h` and where it is used. -| Lemma | C++ code | -|---|---| -| `lemma_fma_zero_nan_addend` | `if (m_util.is_nan(arg4)) { result = nan; return BR_DONE; }` | -| `lemma_fma_zero_nan_mul` | `if (m_util.is_numeral(other_mul, vo) && m_fm.is_nan(vo))` | -| `lemma_fma_zero_inf_mul` | `if (m_util.is_numeral(other_mul, vo) && m_fm.is_inf(vo))` | -| `lemma_fma_zero_finite_decomposes` | `m_util.mk_add(arg1, m_util.mk_value(product), arg4)` with `m_fm.mul(rm, vzero, vo, product)` | -| `lemma_fma_zero_const_addend` | `m().mk_ite(finite_cond, arg4, nan)` (z_const branch) | -| `lemma_fma_zero_general_*` | general `m().mk_ite(finite_cond, m_util.mk_add(...), nan)` | -| `lemma_is_nan_to_fp_int` | `mk_is_nan`: `result = m().mk_false(); return BR_DONE;` | -| `lemma_is_inf_to_fp_int_*` | `mk_is_inf_of_int` switch statement | -| `lemma_is_normal_to_fp_int` | `mk_is_normal`: `result = m().mk_and(not_zero, m().mk_not(inf_cond))` | -| `lemma_is_nan_ite` | `mk_is_nan`: ite-pushthrough block | -| `lemma_is_inf_ite` | `mk_is_inf`: ite-pushthrough block | -| `lemma_is_normal_ite` | `mk_is_normal`: ite-pushthrough block | +| 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 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..e33c2898e --- /dev/null +++ b/src/ast/rewriter/fpa_rewriter_rules.h @@ -0,0 +1,296 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + fpa_rewriter_rules.h + +Abstract: + + Rewrite rule macros for floating-point arithmetic, extracted from + F* lemmas in fstar/FPARewriterRules.fst. + + Each macro is proved correct by one or more lemmas in that file; + the correspondence is documented at each macro definition. + + 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) + +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. +// +// 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. +// +// 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. +// +// 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) From e6e878a98a5cef068a23ad44fa25dde99521c08c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 5 Apr 2026 02:01:57 +0000 Subject: [PATCH 4/9] fstar: clarify README relationship table heading per review Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/46fcd3bf-be90-4098-8516-fde0f1e37cbf Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- fstar/README.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/fstar/README.md b/fstar/README.md index 1bc56151b..73bbfa50c 100644 --- a/fstar/README.md +++ b/fstar/README.md @@ -110,8 +110,7 @@ corresponding to the five `lemma_is_inf_to_fp_int_*` lemmas. ## Relationship to the C++ Code -The following table maps each lemma to the corresponding C++ macro in -`src/ast/rewriter/fpa_rewriter_rules.h` and where it is used. +The following table maps each lemma to its corresponding C++ macro and the function where the macro is invoked. | Lemma | C++ macro | Used in | |---|---|---| From e2ffbe8c80b2e789e4cab753a06ec5b0af2d7484 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 5 Apr 2026 02:38:29 +0000 Subject: [PATCH 5/9] fstar: add RewriteCodeGen.fst - Meta-F* tactic for programmatic C++ extraction Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c7b6d01e-b309-4d67-93bb-f6bad4d79b75 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- fstar/README.md | 78 ++++- fstar/RewriteCodeGen.fst | 442 ++++++++++++++++++++++++++ src/ast/rewriter/fpa_rewriter_rules.h | 27 +- 3 files changed, 537 insertions(+), 10 deletions(-) create mode 100644 fstar/RewriteCodeGen.fst diff --git a/fstar/README.md b/fstar/README.md index 73bbfa50c..61ace6d92 100644 --- a/fstar/README.md +++ b/fstar/README.md @@ -82,7 +82,61 @@ 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 `()`. -### `../src/ast/rewriter/fpa_rewriter_rules.h` +### `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. + C++ header containing one `#define` macro per rewrite rule, extracted from the F\* lemmas. Each macro is annotated with a `[extract: MACRO_NAME]` @@ -144,12 +198,32 @@ IEEE 754-2019 standard: ## Building -To type-check these files with F\*, from this directory run: +### 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 + +To run the reflection-based C++ code extraction and print the generated +rewrite rules to stdout: + +```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. Redirect stdout to a file to capture the output: + +```sh +fstar.exe --include . IEEE754.fst FPARewriterRules.fst RewriteCodeGen.fst \ + 2>/dev/null +``` + F\* 2024.09.05 or later is recommended. The files have no external dependencies beyond the F\* standard library prelude. diff --git a/fstar/RewriteCodeGen.fst b/fstar/RewriteCodeGen.fst new file mode 100644 index 000000000..c6181a79c --- /dev/null +++ b/fstar/RewriteCodeGen.fst @@ -0,0 +1,442 @@ +(** + 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 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 t with + | Tv_FVar fv -> + (match List.Tot.rev (inspect_fv fv) with + | last :: _ -> Some last + | _ -> None) + | _ -> None + +(* Resolve a bound variable, de Bruijn indexed, using our index to name map. + F* reflection represents bound variables with de Bruijn indices: + the most recently bound variable has index 0. + + Given binders [eb; sb; c; t; e], inside the body: + e = BVar 0, t = BVar 1, c = BVar 2, sb = BVar 3, eb = BVar 4 *) +let bvar_name (idx_map: list (nat & string)) (t: term) : Tac (option string) = + match inspect t with + | Tv_BVar bv -> + let bvv = inspect_bv bv in + (match List.Tot.assoc #nat bvv.index idx_map with + | Some n -> Some n + | None -> Some (FStar.Sealed.unseal bvv.ppname)) (* fallback *) + | _ -> None + +(* Detect if-then-else in reflected terms. + In F*, `if c then t else e` desugars to: + match c with | true -> t | false -> e + which appears as Tv_Match with two branches. *) +let try_ite (t: term) : Tac (option (term & term & term)) = + match inspect t with + | Tv_Match scrutinee _ret branches -> + (match branches with + | [(_, body_t); (_, body_f)] -> + Some (scrutinee, body_t, body_f) + | _ -> None) + | _ -> None + +(* Unwrap `squash p` to `p` if present. + The Lemma precondition may be wrapped in squash. *) +let unwrap_squash (t: term) : Tac term = + let (head, args) = collect_app t in + match fv_short_name head with + | Some "squash" -> + (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: + - Bound variables -> PVar + - if-then-else -> PIte + - Function applications -> PApp *) +let rec extract_pat (m: list (nat & string)) (t: term) : Tac cpat = + match try_ite t with + | Some (c, tb, fb) -> + PIte (extract_pat m c) (extract_pat m tb) (extract_pat m 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) args) + | None -> + (match bvar_name m head with + | Some n -> PApp n (tac_map (extract_pat m) args) + | None -> fail ("pattern app: cannot resolve head: " ^ term_to_string head))) + else + (match bvar_name m t with + | Some n -> PVar n + | None -> fail ("pattern: cannot recognize: " ^ term_to_string t)) + +(* Extract an expression from the RHS. + Recognizes: + - Bound variables -> EVar + - Boolean literals -> EBool + - if-then-else -> EIte + - Function applications (FVar) -> EApp *) +let rec extract_expr (m: list (nat & string)) (t: term) : Tac cexpr = + (* Check for boolean literals first *) + (match inspect t with + | Tv_Const (C_Bool b) -> EBool b + | _ -> + match try_ite t with + | Some (c, tb, fb) -> + EIte (extract_expr m c) (extract_expr m tb) (extract_expr m 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) args) + | None -> fail ("expr: application head is not FVar: " ^ term_to_string head)) + else + (match bvar_name m 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 t with + | Tv_Arrow binder c -> + let name = FStar.Sealed.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) = + match p with + | PVar n -> [n] + | PIte c t e -> pat_vars c @ pat_vars t @ pat_vars e + | PApp _ args -> + let rec collect (l: list cpat) : Tot (list string) (decreases l) = + match l with + | [] -> [] + | x :: xs -> pat_vars x @ collect xs + in + collect args + +(* 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 = + 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 ^ "(" + ^ FStar.String.concat ", " (List.Tot.map gen_rhs_expr args) ^ ")" + +(* 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 precondition *) + let pre = + match inspect_comp final_comp with + | C_Lemma pre _ _ -> pre + | _ -> fail "expected Lemma computation type" in + + (* 3. Extract LHS = RHS from the precondition *) + let (lhs, rhs) = extract_eq pre 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 arg_term in + let rhs_expr = extract_expr idx_map 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 + +(* Demonstrate extraction of the three ite-pushthrough lemmas. *) +let _ = + run_tactic (fun () -> + print "\n=== lemma_is_nan_ite ===\n"; + print (extract_rewrite (quote lemma_is_nan_ite))) + +let _ = + run_tactic (fun () -> + print "\n=== lemma_is_inf_ite ===\n"; + print (extract_rewrite (quote lemma_is_inf_ite))) + +let _ = + run_tactic (fun () -> + print "\n=== lemma_is_normal_ite ===\n"; + print (extract_rewrite (quote lemma_is_normal_ite))) diff --git a/src/ast/rewriter/fpa_rewriter_rules.h b/src/ast/rewriter/fpa_rewriter_rules.h index e33c2898e..c99611311 100644 --- a/src/ast/rewriter/fpa_rewriter_rules.h +++ b/src/ast/rewriter/fpa_rewriter_rules.h @@ -7,11 +7,18 @@ Module Name: Abstract: - Rewrite rule macros for floating-point arithmetic, extracted from - F* lemmas in fstar/FPARewriterRules.fst. + Rewrite rule macros for floating-point arithmetic, whose correctness + is proved by F* lemmas in fstar/FPARewriterRules.fst. - Each macro is proved correct by one or more lemmas in that file; - the correspondence is documented at each macro definition. + 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: + + fstar.exe --include fstar fstar/IEEE754.fst \ + fstar/FPARewriterRules.fst fstar/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. @@ -19,7 +26,8 @@ Abstract: Author: - (extracted from F* in fstar/FPARewriterRules.fst) + (extracted from F* in fstar/FPARewriterRules.fst, + ite-pushthrough rules generated via fstar/RewriteCodeGen.fst) Notes: @@ -57,7 +65,8 @@ Notes: // When both branches are concrete FP numerals the rewriter evaluates // the predicate statically and folds the result into the condition. // -// Applies to: mk_is_nan(arg1, result) +// 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 { \ @@ -120,7 +129,8 @@ Notes: // When both branches are concrete FP numerals the predicate is evaluated // statically and folded into the condition. // -// Applies to: mk_is_inf(arg1, result) +// 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 { \ @@ -185,7 +195,8 @@ Notes: // When both branches are concrete FP numerals the predicate is evaluated // statically and folded into the condition. // -// Applies to: mk_is_normal(arg1, result) +// 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 { \ From da40b270a1640839d99b476fe7c141234acd84b7 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 5 Apr 2026 02:39:55 +0000 Subject: [PATCH 6/9] fstar: address code review - diagnostic on bvar fallback, refactor extractions, fix include path Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c7b6d01e-b309-4d67-93bb-f6bad4d79b75 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- fstar/README.md | 9 +++++--- fstar/RewriteCodeGen.fst | 30 +++++++++++++++------------ src/ast/rewriter/fpa_rewriter_rules.h | 6 +++--- 3 files changed, 26 insertions(+), 19 deletions(-) diff --git a/fstar/README.md b/fstar/README.md index 61ace6d92..69a719625 100644 --- a/fstar/README.md +++ b/fstar/README.md @@ -137,10 +137,13 @@ 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, extracted from -the F\* lemmas. Each macro is annotated with a `[extract: MACRO_NAME]` -comment in the corresponding F\* lemma. +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 | |---|---|---| diff --git a/fstar/RewriteCodeGen.fst b/fstar/RewriteCodeGen.fst index c6181a79c..459d6f9e5 100644 --- a/fstar/RewriteCodeGen.fst +++ b/fstar/RewriteCodeGen.fst @@ -105,7 +105,13 @@ let bvar_name (idx_map: list (nat & string)) (t: term) : Tac (option string) = let bvv = inspect_bv bv in (match List.Tot.assoc #nat bvv.index idx_map with | Some n -> Some n - | None -> Some (FStar.Sealed.unseal bvv.ppname)) (* fallback *) + | None -> + (* de Bruijn index not in our map; use the printer name as a fallback + and warn so the caller knows the index map may be incomplete. *) + let pp = FStar.Sealed.unseal bvv.ppname in + print ("WARNING: bvar_name fallback for index " + ^ string_of_int bvv.index ^ ", using ppname '" ^ pp ^ "'"); + Some pp) | _ -> None (* Detect if-then-else in reflected terms. @@ -425,18 +431,16 @@ let extract_rewrite (lemma: term) : Tac string = open FPARewriterRules -(* Demonstrate extraction of the three ite-pushthrough lemmas. *) -let _ = - run_tactic (fun () -> - print "\n=== lemma_is_nan_ite ===\n"; - print (extract_rewrite (quote lemma_is_nan_ite))) +(* 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) +(* Demonstrate extraction of the three ite-pushthrough lemmas. + Running this file with F* prints the generated C++ for each rule. *) let _ = run_tactic (fun () -> - print "\n=== lemma_is_inf_ite ===\n"; - print (extract_rewrite (quote lemma_is_inf_ite))) - -let _ = - run_tactic (fun () -> - print "\n=== lemma_is_normal_ite ===\n"; - print (extract_rewrite (quote lemma_is_normal_ite))) + List.Tot.iter (fun (label, lemma) -> print_rewrite label lemma) + [ ("lemma_is_nan_ite", quote lemma_is_nan_ite); + ("lemma_is_inf_ite", quote lemma_is_inf_ite); + ("lemma_is_normal_ite", quote lemma_is_normal_ite) ]) diff --git a/src/ast/rewriter/fpa_rewriter_rules.h b/src/ast/rewriter/fpa_rewriter_rules.h index c99611311..af12e2ce4 100644 --- a/src/ast/rewriter/fpa_rewriter_rules.h +++ b/src/ast/rewriter/fpa_rewriter_rules.h @@ -12,10 +12,10 @@ Abstract: 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: + the Meta-F* extraction tactic in fstar/RewriteCodeGen.fst (from the repo root): - fstar.exe --include fstar fstar/IEEE754.fst \ - fstar/FPARewriterRules.fst fstar/RewriteCodeGen.fst + 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. From e5acaf0c289e2c53b0139e7ef8a10d1f4cf8dbaa Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 5 Apr 2026 02:45:56 +0000 Subject: [PATCH 7/9] fstar: add extract.sh script and fstar-extract.yml GHA workflow for Meta-F* extraction Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/680146e3-e241-487e-a0d7-a7e23b5f1634 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .github/workflows/fstar-extract.yml | 93 +++++++++++++++++++++++++++++ fstar/README.md | 25 ++++++-- fstar/extract.sh | 47 +++++++++++++++ 3 files changed, 159 insertions(+), 6 deletions(-) create mode 100644 .github/workflows/fstar-extract.yml create mode 100755 fstar/extract.sh diff --git a/.github/workflows/fstar-extract.yml b/.github/workflows/fstar-extract.yml new file mode 100644 index 000000000..3e3072f07 --- /dev/null +++ b/.github/workflows/fstar-extract.yml @@ -0,0 +1,93 @@ +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: "2024.09.05" + 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}" + mkdir -p "$HOME/fstar" + tar -xzf "/tmp/${ARCHIVE}" -C "$HOME/fstar" --strip-components=1 + 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/README.md b/fstar/README.md index 69a719625..f28c6b358 100644 --- a/fstar/README.md +++ b/fstar/README.md @@ -211,8 +211,14 @@ fstar.exe --include . IEEE754.fst FPARewriterRules.fst ### Running the Meta-F* extraction -To run the reflection-based C++ code extraction and print the generated -rewrite rules to stdout: +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 @@ -220,14 +226,21 @@ 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. Redirect stdout to a file to capture the output: +lemma. To capture the output to a file: ```sh -fstar.exe --include . IEEE754.fst FPARewriterRules.fst RewriteCodeGen.fst \ - 2>/dev/null +./extract.sh > extracted_rules.txt ``` -F\* 2024.09.05 or later is recommended. The files have no external +### 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\* 2024.09.05 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 diff --git a/fstar/extract.sh b/fstar/extract.sh new file mode 100755 index 000000000..0d8f5897e --- /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* 2024.09.05+ 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 From 4a2accf10c9fab7bf8bb596116cad1c340c256cd Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 6 Apr 2026 01:49:41 +0000 Subject: [PATCH 8/9] fstar: fix F* 2026 compatibility and run Meta-F* extraction successfully - IEEE754.fst: fix multi-binding in assume val signatures (F* 2026 syntax), change float from Type0 to eqtype for equality support, generalize fma NaN axioms to handle any-NaN inputs (ax_fma_any_nan_y/x/z) - FPARewriterRules.fst: add explicit #eb #sb type arguments to axiom calls where F* 2026 cannot infer them, use ax_fma_any_nan_y for proofs where y is an arbitrary NaN rather than the canonical nan constant - RewriteCodeGen.fst: fix F* 2026 API changes: FStar.Sealed.unseal->unseal, C_Bool->{C_True,C_False}, List.Tot.iter->iter, FStar.Reflection.V2.inspect ->inspect_ln for term_view, post from C_Lemma pre->post with Tv_Abs peel, b2t unwrapping, lemma_ref via pack_fv instead of quote for polymorphic lemmas, per-branch offset tracking for Pat_Var in match branches - .github/workflows/fstar-extract.yml: update to F* 2026.03.24 with correct archive name fstar-v{VERSION}-Linux-x86_64.tar.gz - fstar/README.md and extract.sh: update version references to 2026.03.24 Extraction now produces correct output: 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; } Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/0a30f342-3941-4952-a54f-1bee84b022ef Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .github/workflows/fstar-extract.yml | 6 +- fstar/FPARewriterRules.fst | 42 +++--- fstar/IEEE754.fst | 32 +++-- fstar/README.md | 2 +- fstar/RewriteCodeGen.fst | 191 +++++++++++++++++----------- fstar/extract.sh | 2 +- 6 files changed, 167 insertions(+), 108 deletions(-) diff --git a/.github/workflows/fstar-extract.yml b/.github/workflows/fstar-extract.yml index 3e3072f07..ec4473ce5 100644 --- a/.github/workflows/fstar-extract.yml +++ b/.github/workflows/fstar-extract.yml @@ -44,14 +44,14 @@ jobs: # ----------------------------------------------------------------------- - name: Install F* env: - FSTAR_VERSION: "2024.09.05" + FSTAR_VERSION: "2026.03.24" run: | - ARCHIVE="fstar_v${FSTAR_VERSION}_Linux_x86_64.tar.gz" + 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}" mkdir -p "$HOME/fstar" - tar -xzf "/tmp/${ARCHIVE}" -C "$HOME/fstar" --strip-components=1 + tar -xzf "/tmp/${ARCHIVE}" -C "$HOME/fstar" --strip-components=2 echo "$HOME/fstar/bin" >> "$GITHUB_PATH" - name: Verify F* installation diff --git a/fstar/FPARewriterRules.fst b/fstar/FPARewriterRules.fst index 8594ab182..766edf536 100644 --- a/fstar/FPARewriterRules.fst +++ b/fstar/FPARewriterRules.fst @@ -149,7 +149,7 @@ let lemma_fma_zero_const_nan_inf_arm (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_nan_y rm zero_val z + 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 @@ -182,7 +182,7 @@ let lemma_fma_zero_general_nan_inf_arm (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_nan_y rm zero_val z + 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 @@ -229,7 +229,7 @@ let lemma_fma_zero_product_sign 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 rm x + ax_to_fp_int_not_nan #eb #sb rm x (* --- 2b: isInf --- *) @@ -245,32 +245,32 @@ 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 x + 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 x + 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 x + 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 x + 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 x + ax_is_inf_rtz #eb #sb x (* --- 2c: isNormal --- *) @@ -295,21 +295,21 @@ let lemma_is_normal_to_fp_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 rm x; (* is_nan f = false *) - ax_to_fp_int_not_subnormal rm x; (* is_subnormal f = false *) - ax_classification f; (* nan||inf||zero||normal||subnormal *) + 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 rm; (* is_zero f = true *) - ax_zero_exclusive f (* is_normal f = false, since is_zero f *) + 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 rm x; (* is_zero f = false *) + 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 *) + ax_inf_exclusive f (* is_inf f = true => is_normal f = false *) else - () (* is_inf f = false; by classification, is_normal f = true *) + () (* is_inf f = false; by classification, is_normal f = true *) end @@ -390,7 +390,7 @@ let lemma_fma_zero_ite_nan_arm : 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_nan_y rm zero_val z + 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), @@ -409,12 +409,12 @@ let lemma_is_normal_to_fp_int_rne (x <> 0 && not (x >= overflow_threshold eb sb || x <= -(overflow_threshold eb sb)))) = - lemma_is_normal_to_fp_int RNE x; - ax_is_inf_rne x + 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 RTZ x; - ax_is_inf_rtz x + 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 index 0faf2cd84..185efc50c 100644 --- a/fstar/IEEE754.fst +++ b/fstar/IEEE754.fst @@ -25,7 +25,7 @@ module IEEE754 (* 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) -> Type0 +assume val float : (eb: pos) -> (sb: pos) -> eqtype (* ------------------------------------------------------------------ *) (* Rounding modes (IEEE 754-2019 §4.3) *) @@ -154,17 +154,33 @@ assume val ax_mul_nan_r : 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 z: float eb sb) -> + #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 z: float eb sb) -> + #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 y: float eb sb) -> + #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 *) (* ------------------------------------------------------------------ *) @@ -181,7 +197,7 @@ assume val ax_zero_mul_inf : 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 y z: float eb sb) -> + #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) @@ -189,7 +205,7 @@ assume val ax_fma_nan_mul : 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 y z: float eb sb) -> + #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) @@ -197,7 +213,7 @@ assume val ax_fma_zero_finite : (* 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 y: float eb sb) -> + #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 && @@ -208,7 +224,7 @@ assume val ax_zero_mul_sign : (* 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 z: float eb sb) -> + #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) diff --git a/fstar/README.md b/fstar/README.md index f28c6b358..f4a34cd8a 100644 --- a/fstar/README.md +++ b/fstar/README.md @@ -240,7 +240,7 @@ 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\* 2024.09.05 or later is required. The files have no external +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 diff --git a/fstar/RewriteCodeGen.fst b/fstar/RewriteCodeGen.fst index 459d6f9e5..8a4b0cbb2 100644 --- a/fstar/RewriteCodeGen.fst +++ b/fstar/RewriteCodeGen.fst @@ -70,7 +70,7 @@ noeq type cexpr = 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 t with + match inspect_ln t with | Tv_App hd arg -> let (h, args) = collect_app hd in (h, args @ [arg]) @@ -86,53 +86,70 @@ let filter_explicit (args: list argv) : list term = (* 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 t with + match inspect_ln t with | Tv_FVar fv -> (match List.Tot.rev (inspect_fv fv) with | last :: _ -> Some last | _ -> None) | _ -> None -(* Resolve a bound variable, de Bruijn indexed, using our index to name map. - F* reflection represents bound variables with de Bruijn indices: - the most recently bound variable has index 0. - - Given binders [eb; sb; c; t; e], inside the body: - e = BVar 0, t = BVar 1, c = BVar 2, sb = BVar 3, eb = BVar 4 *) -let bvar_name (idx_map: list (nat & string)) (t: term) : Tac (option string) = - match inspect t with - | Tv_BVar bv -> - let bvv = inspect_bv bv in - (match List.Tot.assoc #nat bvv.index idx_map with - | Some n -> Some n - | None -> - (* de Bruijn index not in our map; use the printer name as a fallback - and warn so the caller knows the index map may be incomplete. *) - let pp = FStar.Sealed.unseal bvv.ppname in - print ("WARNING: bvar_name fallback for index " - ^ string_of_int bvv.index ^ ", using ppname '" ^ pp ^ "'"); - Some pp) - | _ -> 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 | false -> e - which appears as Tv_Match with two branches. *) -let try_ite (t: term) : Tac (option (term & term & term)) = - match inspect t with + 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 - | [(_, body_t); (_, body_f)] -> - Some (scrutinee, body_t, body_f) + | [(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` to `p` if present. - The Lemma precondition may be wrapped in squash. *) +(* 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 "squash" + | Some "b2t" -> (match filter_explicit args with | [inner] -> inner | _ -> t) | _ -> t @@ -162,51 +179,56 @@ let rec tac_map (#a #b: Type) (f: a -> Tac b) (l: list a) : Tac (list b) = (* Extract a pattern from the LHS argument. Recognizes: - - Bound variables -> PVar - - if-then-else -> PIte - - Function applications -> PApp *) -let rec extract_pat (m: list (nat & string)) (t: term) : Tac cpat = + - 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, tb, fb) -> - PIte (extract_pat m c) (extract_pat m tb) (extract_pat m fb) + | 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) args) + | Some fn -> PApp fn (tac_map (extract_pat m offset) args) | None -> - (match bvar_name m head with - | Some n -> PApp n (tac_map (extract_pat m) args) + (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 bvar_name m t with + (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: - - Bound variables -> EVar + - Variables (named or BVar) -> EVar - Boolean literals -> EBool - - if-then-else -> EIte - - Function applications (FVar) -> EApp *) -let rec extract_expr (m: list (nat & string)) (t: term) : Tac cexpr = + - 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 t with - | Tv_Const (C_Bool b) -> EBool b + (match inspect_ln t with + | Tv_Const C_True -> EBool true + | Tv_Const C_False -> EBool false | _ -> match try_ite t with - | Some (c, tb, fb) -> - EIte (extract_expr m c) (extract_expr m tb) (extract_expr m fb) + | 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) args) + | 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 bvar_name m t with + (match var_name m offset t with | Some n -> EVar n | None -> fail ("expr: cannot recognize: " ^ term_to_string t))) @@ -219,9 +241,9 @@ let rec extract_expr (m: list (nat & string)) (t: term) : Tac cexpr = -> 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 t with + match inspect_ln t with | Tv_Arrow binder c -> - let name = FStar.Sealed.unseal (inspect_binder binder).ppname in + let name = unseal (inspect_binder binder).ppname in (match inspect_comp c with | C_Total ret -> let (names, final_c) = strip_arrows ret in @@ -260,17 +282,16 @@ let cpp_builder_name (fn: string) : string = | _ -> "m_util.mk_" ^ fn (* Collect all variable names from a pattern (for C++ declarations) *) -let rec pat_vars (p: cpat) : Tot (list string) = +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 -> - let rec collect (l: list cpat) : Tot (list string) (decreases l) = - match l with - | [] -> [] - | x :: xs -> pat_vars x @ collect xs - in - collect args + | 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 = @@ -297,7 +318,7 @@ let gen_condition (arg: string) (p: cpat) : string = | _ -> "/* TODO: extend gen_condition for nested patterns */" (* Generate a C++ expression from the RHS IR *) -let rec gen_rhs_expr (e: cexpr) : Tot string = +let rec gen_rhs_expr (e: cexpr) : Tot string (decreases e) = match e with | EVar n -> n | EBool true -> "m().mk_true()" @@ -308,7 +329,13 @@ let rec gen_rhs_expr (e: cexpr) : Tot string = ^ gen_rhs_expr e ^ ")" | EApp fn args -> cpp_builder_name fn ^ "(" - ^ FStar.String.concat ", " (List.Tot.map gen_rhs_expr args) ^ ")" + ^ gen_rhs_expr_list args ^ ")" + +and gen_rhs_expr_list (es: list cexpr) : Tot string (decreases es) = + 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 = @@ -353,14 +380,22 @@ let extract_rewrite (lemma: term) : Tac string = 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 precondition *) - let pre = + (* 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 pre _ _ -> pre + | 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 precondition *) - let (lhs, rhs) = extract_eq pre 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 @@ -381,8 +416,8 @@ let extract_rewrite (lemma: term) : Tac string = ^ " for top_fn=" ^ top_fn) in (* 5. Extract the argument pattern and the RHS expression *) - let pat = extract_pat idx_map arg_term in - let rhs_expr = extract_expr idx_map rhs in + 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 @@ -436,11 +471,19 @@ 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 () -> - List.Tot.iter (fun (label, lemma) -> print_rewrite label lemma) - [ ("lemma_is_nan_ite", quote lemma_is_nan_ite); - ("lemma_is_inf_ite", quote lemma_is_inf_ite); - ("lemma_is_normal_ite", quote lemma_is_normal_ite) ]) + 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 index 0d8f5897e..741636984 100755 --- a/fstar/extract.sh +++ b/fstar/extract.sh @@ -26,7 +26,7 @@ cd "$SCRIPT_DIR" if ! command -v fstar.exe &>/dev/null; then echo "ERROR: fstar.exe not found on PATH." >&2 - echo "Install F* 2024.09.05+ from https://github.com/FStarLang/FStar/releases" >&2 + echo "Install F* 2026.03.24+ from https://github.com/FStarLang/FStar/releases" >&2 exit 1 fi From c49b403922f66a000f17ef4f16bda3cffecd414e Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 6 Apr 2026 01:51:11 +0000 Subject: [PATCH 9/9] fstar: address code review comments - document gen_rhs_expr_list and strip-components Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/0a30f342-3941-4952-a54f-1bee84b022ef Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .github/workflows/fstar-extract.yml | 3 +++ fstar/RewriteCodeGen.fst | 3 +++ 2 files changed, 6 insertions(+) diff --git a/.github/workflows/fstar-extract.yml b/.github/workflows/fstar-extract.yml index ec4473ce5..1b1a5a74f 100644 --- a/.github/workflows/fstar-extract.yml +++ b/.github/workflows/fstar-extract.yml @@ -50,6 +50,9 @@ jobs: 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" diff --git a/fstar/RewriteCodeGen.fst b/fstar/RewriteCodeGen.fst index 8a4b0cbb2..b84a64574 100644 --- a/fstar/RewriteCodeGen.fst +++ b/fstar/RewriteCodeGen.fst @@ -332,6 +332,9 @@ let rec gen_rhs_expr (e: cexpr) : Tot string (decreases e) = ^ 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