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