mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-07 05:02:48 +00:00
Code Activity

fstar: formalize FPA rewriter rules from PR #9038 in F* using IEEE 754 axioms

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7899b653-a7f0-443c-894a-32376baea5c0

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-03 18:05:00 +00:00 • committed by GitHub
parent 8d7ed66ebf
commit e3aa907098
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 836 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

407
fstar/FPARewriterRules.fst Normal file
View file

@ -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

295
fstar/IEEE754.fst Normal file
View file

@ -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)

134
fstar/README.md Normal file
View file

@ -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.