Fix floating-point division normalization

[1sgtpepper]

Summary

Preserve exact denormal leading-zero counts in symbolic fp.div and support valid
formats with ebits > sbits. Division owns the wider leading-zero and exponent
workspaces, handles exceptional exponents before calling the operation-independent
rounder, and preserves sticky information through deep underflow.

The shared round contract remains sig = sbits + 4 and exp = ebits + 2. Its generic
shift counts retain their exact bounded values without widening the shifted data path.
Deep underflow is rounded locally with sticky preservation.

Fixes #10175.

Regression coverage: Z3Prover/z3test#60 and Z3Prover/z3test#63.

Testing

• Proof-only commit 4a15d7e9b, directly atop this PR head, records the
  independent oracle, coverage, expected output, replay instructions, and hashes.
• python3 proofs/verify_ebits_gt_sbits.py | diff -u proofs/verify_ebits_gt_sbits.expected.json -
• python3 proofs/verify_fp_div_semantics.py | diff -u proofs/verify_fp_div_semantics.expected.json -
• sha256sum -c proofs/SHA256SUMS
• Exact paired fork validation at f42bacbf1 combines this source head 51b80b21a
  with z3test head 9593fb035: build/test
  (14/14 jobs) and OCaml bindings
  (2/2 jobs), both successful.
• The cap-width control
  changes only the shift-cap width; the dedicated FP(2,16) regression fails when 18
  wraps to 2.
• The known-bad replay
  uses the unpatched PR base with the current z3test head; all 24 isolated wide cases
  fail in each of its eight regression configurations.
• No local Z3 build or solver executable was used; validation used fork CI and the
  lightweight Python proofs above.

[Copilot]

Pull request overview

This PR adjusts the fpa2bv_converter floating-point division (fp.div) lowering to bit-vectors to preserve exact denormal leading-zero counts and to widen the signed intermediate exponent representation only when needed for the given (ebits, sbits) format, avoiding leading-zero truncation and exponent wraparound for supported ebits <= sbits formats (Fixes #10175).

Changes:

• Introduce unpack_with_lz_width(...) to control the bit-width used to represent leading-zero counts during unpacking/normalization.
• Update mk_div to compute a format-dependent exponent width (exp_bits) and choose an appropriate lz_bits for exact denormal handling.
• Generalize round(...) to operate correctly with exponents wider than the legacy ebits + 2 intermediate width, while preserving the previous formula shape for legacy-width callers.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
src/ast/fpa/fpa2bv_converter.h	Adds a private helper declaration to unpack with a configurable leading-zero bit-width.
src/ast/fpa/fpa2bv_converter.cpp	Implements division/exponent-width adjustments, adds unpack_with_lz_width, and updates rounding to support wider exponent intermediates.

[Nikolaj Bjorner (NikolajBjorner)]

How do we best validate this change (and changes like these)?
Should we declare victory for now if it fixes a reported bug and passes the CI and fixes the bug,
or should it have self-contained unit tests or a form of an IEEE spec reference?

[Nikolaj Bjorner (NikolajBjorner)]

Regression tests mirroring these unit tests have been added (as .smt2.disabled) to z3prover/z3test under regressions/smt2/ (commit 0c4d428):

File	Test	Expected
fp-div-norm-1	FP(2,6) bug reproducer: -oo = -3.25/0.0625	unsat
fp-div-norm-2	FP(2,6) RTZ overflow clips to −3.9375	sat
fp-div-norm-3	FP(2,6) exact 2.0/1.0	sat
fp-div-norm-4	FP(2,6) denormal 0.0625/0.0625	sat
fp-div-norm-5	FP(2,6) max-neg/self	sat
fp-div-norm-6	FP(2,5) basic	sat
fp-div-norm-7	FP(2,5) RNE overflow → +oo	sat
fp-div-norm-8	Float32 6.0/2.0	sat
fp-div-norm-9	Float16 1.0/2.0	sat
fp-div-norm-10	FP(3,8) boundary	sat

The disabled unit tests are pushed to z3test as SMT-LIB2 regressions; each has a matching .expected.out file. All outputs were verified against a fixed z3 build.

[1sgtpepper]

Nikolaj Bjorner (@NikolajBjorner), sorry—I may have misunderstood the testing convention and added the regression in z3test#60. Should I also add a src/test test?

[Christoph M. Wintersteiger (wintersteiger)]

The changes in unpack are too extensive for me to review in detail in reasonable time, and that function is used in every single FP function, i.e. potentially breaks lots of stuff. At the very least, we need to run all of the SMT-LIB benchmarks through it.

IMHO, those changes are not right: unpack does not get a special branch for division, anything that is specific to division needs to stay in mk_div. Also, I have a hunch that the general fix for ebits > sbits could be less complicated while also covering this special case, so perhaps we should go for that right away.

[1sgtpepper]

Thanks. I may revert that part, but I’d like to first investigate whether a smaller mk_div-local fix can also handle the general ebits > sbits case.

[Christoph M. Wintersteiger (wintersteiger)]

Thanks. I may revert that part, but I’d like to first investigate whether a smaller mk_div-local fix can also handle the general ebits > sbits case.

Absolutely, it would be awesome if we could close this gap!

[Nikolaj Bjorner (NikolajBjorner)]

Nikolaj Bjorner (@NikolajBjorner), sorry—I may have misunderstood the testing convention and added the regression in z3test#60. Should I also add a src/test test?

you did the right thing. I didnt' see your PR until now. Merged it.

[Nikolaj Bjorner (NikolajBjorner)]

Can I merge this?

[Christoph M. Wintersteiger (wintersteiger)]

I think this is still being worked on; perhaps mark it as draft for now?

[1sgtpepper]

Let me take a quick look..... last time I checked I thought it was good to go for review

[1sgtpepper]

Christoph M. Wintersteiger (@wintersteiger), I think this is ready for another look now—could you re-review when you have a chance?

[Nikolaj Bjorner (NikolajBjorner)]

Christoph M. Wintersteiger (@wintersteiger) - thanks for reviewing!

[1sgtpepper]

Thanks for the review. Marking this draft for now while I think this through, will get back to you

[Nikolaj Bjorner (NikolajBjorner)]

thanks for the update

[Nikolaj Bjorner (NikolajBjorner)]

Christoph M. Wintersteiger (@wintersteiger) - appropriate to merge at this point?

[Nikolaj Bjorner (NikolajBjorner)]

Fairly indirect and a poor-man's one-shot prompt investigation.
But additional evidence that isn't entirely in the "trust me" mode for this PR with cross reference to IEEE spec and code.

(*
   FloatsIEEE754Division.fst

   Formal model of the width-sensitive fp.div transformation in Z3 PR #10216,
   source head 51b80b21ac59a35f474860ed2e63cc502098e1f1.

   IEEE 754-2019 connections
   -------------------------
   * 3.3 and 3.4: finite binary values and subnormal encodings.
   * 4.3.1-4.3.3: nearest and directed rounding attributes.
   * 5.4.1: division computes the infinitely precise quotient and rounds it
     once to the destination format.
   * 7.5: tiny inexact results use gradual underflow; discarded nonzero bits
     therefore remain relevant to rounding.

   Source connections (line numbers are at the PR head above)
   -----------------------------------------------------------
   * 960-1014: exact local leading-zero counts and operand normalization.
   * 1025-1038: widened signed exponent arithmetic.
   * 1073-1093: quotient normalization and matching exponent correction.
   * 1101-1175: local deep-underflow shift, sticky bit, and rounding.
   * 4108-4149: shared rounding-decision truth table.
   * 4265-4319: widened/capped shared-round shift counts.

   The module deliberately models mathematical integers rather than F* machine
   integers.  The lemmas below prove the range conditions under which the C++
   fixed-width bit-vector operations denote these mathematical operations.
   No axiom or assume is introduced by this module.
*)
module FloatsIEEE754Division

open FloatsIEEE754Spec

#push-options "--fuel 2 --ifuel 1 --z3rlimit 80"

(* ------------------------------------------------------------------------- *)
(* 1. Width predicates and exact leading-zero transport.                     *)
(* ------------------------------------------------------------------------- *)

let unsigned_fits (w:pos) (n:nat) : prop = n < pow2n w

let signed_fits (w:pos{w >= 2}) (n:int) : prop =
  -(pow2n (w - 1)) <= n /\ n < pow2n (w - 1)

(* mk_leading_zeros returns the exact count modulo 2^w.  A nonzero s-bit
   significand has at most s-1 leading zeroes, so s <= 2^w is precisely the
   condition that prevents wrapping.  This is the invariant used at
   fpa2bv_converter.cpp:962-984 and 1002-1007. *)
val leading_zero_width_is_exact (s w:pos) (lz:nat)
  : Lemma
      (requires lz < s /\ s <= pow2n w)
      (ensures unsigned_fits w lz)
let leading_zero_width_is_exact s w lz = ()

(* A dyadic pair (coefficient, exponent) denotes coefficient * 2^exponent.
   Equality is expressed without division or negative powers. *)
type dyadic = {
  coefficient : nat;
  exponent : int;
}

let dyadic_equal (a b:dyadic) : prop =
  if a.exponent <= b.exponent
  then a.coefficient == b.coefficient * pow2n (b.exponent - a.exponent)
  else b.coefficient == a.coefficient * pow2n (a.exponent - b.exponent)

let normalize (x:dyadic) (lz:nat) : dyadic =
  { coefficient = x.coefficient * pow2n lz;
    exponent = x.exponent - lz }

(* The source shifts the significand left by lz and subtracts lz from the
   exponent (lines 1011-1014 and 1036-1038).  This preserves the represented
   exact dyadic value. *)
val normalization_preserves_value (x:dyadic) (lz:nat)
  : Lemma (ensures dyadic_equal (normalize x lz) x)
let normalization_preserves_value x lz = ()

val pow2n_add (a b:nat)
  : Lemma (ensures pow2n (a + b) == pow2n a * pow2n b)
           (decreases a)
let rec pow2n_add a b =
  if a = 0 then ()
  else pow2n_add (a - 1) b

type exact_quotient = {
  numerator : nat;
  denominator : nat;
  scale : int;
}

let quotient_of (a b:dyadic) : exact_quotient =
  { numerator = a.coefficient;
    denominator = b.coefficient;
    scale = a.exponent - b.exponent }

(* Equality of (n/d)*2^scale is reduced to equality of two cross-multiplied
   dyadics, avoiding real division and any nonzero side condition. *)
let quotient_equal (a b:exact_quotient) : prop =
  dyadic_equal
    { coefficient = a.numerator * b.denominator; exponent = a.scale }
    { coefficient = b.numerator * a.denominator; exponent = b.scale }

(* This composes the two source transformations at lines 1011-1014 and
   1033-1038: applying independent exact leading-zero normalizations to the
   dividend and divisor leaves their infinitely precise quotient unchanged. *)
val operand_normalization_preserves_quotient
      (a b:dyadic) (a_lz b_lz:nat)
  : Lemma
      (ensures
        quotient_equal
          (quotient_of (normalize a a_lz) (normalize b b_lz))
          (quotient_of a b))
let operand_normalization_preserves_quotient a b a_lz b_lz =
  if a_lz <= b_lz
  then pow2n_add a_lz (b_lz - a_lz)
  else pow2n_add b_lz (a_lz - b_lz)

(* ------------------------------------------------------------------------- *)
(* 2. Exact exponent bounds and absence of bit-vector wrap.                  *)
(* ------------------------------------------------------------------------- *)

val pow2n_step (k:pos)
  : Lemma (ensures pow2n k == 2 * pow2n (k - 1))
let pow2n_step k = ()

let ieee_emin (ebits:pos{ebits >= 2}) : int =
  2 - pow2n (ebits - 1)

let ieee_emax (ebits:pos{ebits >= 2}) : int =
  pow2n (ebits - 1) - 1

let division_exp
      (a_exp b_exp:int) (a_lz b_lz:nat) (quotient_correction:nat)
    : int =
  (a_exp - a_lz) - (b_exp - b_lz) - quotient_correction

let division_exp_min (ebits sbits:pos) : int =
  3 - pow2n ebits - sbits

let division_exp_max (ebits sbits:pos) : int =
  pow2n ebits + sbits - 4

(* Unpacked finite operands have exponent in [emin, emax], each exact
   leading-zero count is in [0,sbits-1], and the normalized quotient needs
   either zero or one further left shift.  These facts imply the bounds stated
   by the source at lines 968-975. *)
val division_exponent_bounds
      (ebits:pos{ebits >= 2}) (sbits:pos{sbits >= 2})
      (a_exp b_exp:int) (a_lz b_lz quotient_correction:nat)
  : Lemma
      (requires
        ieee_emin ebits <= a_exp /\ a_exp <= ieee_emax ebits /\
        ieee_emin ebits <= b_exp /\ b_exp <= ieee_emax ebits /\
        a_lz < sbits /\ b_lz < sbits /\ quotient_correction <= 1)
      (ensures
        division_exp_min ebits sbits <=
          division_exp a_exp b_exp a_lz b_lz quotient_correction /\
        division_exp a_exp b_exp a_lz b_lz quotient_correction <=
          division_exp_max ebits sbits)
let division_exponent_bounds ebits sbits a_exp b_exp a_lz b_lz quotient_correction =
  pow2n_step ebits

(* C++ chooses one sign bit beyond floor(log2(max_exp)).  The equivalent
   arithmetic contract is max_exp < 2^(w-1).  Since the negative endpoint is
   -(max_exp+1), that single condition covers both endpoints. *)
val widened_exponent_does_not_wrap
      (ebits:pos{ebits >= 2}) (sbits:pos{sbits >= 2})
      (w:pos{w >= 2}) (result_exp:int)
  : Lemma
      (requires
        division_exp_min ebits sbits <= result_exp /\
        result_exp <= division_exp_max ebits sbits /\
        division_exp_max ebits sbits < pow2n (w - 1))
      (ensures signed_fits w result_exp)
let widened_exponent_does_not_wrap ebits sbits w result_exp = ()

(* The quotient correction at lines 1087-1091 is transported by either
   extraction or zero extension.  Its mathematical value is unchanged when it
   fits the destination width. *)
val quotient_shift_transport_is_exact (w:pos) (shift:nat)
  : Lemma
      (requires shift < pow2n w)
      (ensures unsigned_fits w shift)
let quotient_shift_transport_is_exact w shift = ()

(* ------------------------------------------------------------------------- *)
(* 3. Sticky preservation for the local deep-underflow path.                 *)
(* ------------------------------------------------------------------------- *)

let bit (b:bool) : nat = if b then 1 else 0

(* The ideal sticky bit after two consecutive discarded regions is the OR of
   both regions.  C++ can only inspect the second region after the physical
   right shift. *)
let ideal_sticky (first_discarded second_discarded:bool) : bool =
  first_discarded || second_discarded

let cpp_sticky (second_discarded:bool) : bool = second_discarded

(* Lines 1139-1144 establish the key invariant: either the shift remains in
   the appended zero padding (nothing was discarded by the first shift), or
   the normalized leading one remains in the low slice reduced by BREDOR
   (second_discarded is true).  Under exactly that invariant the local sticky
   bit equals the infinitely precise sticky bit. *)
val deep_underflow_sticky_is_exact
      (first_discarded second_discarded:bool)
  : Lemma
      (requires (not first_discarded) \/ second_discarded)
      (ensures cpp_sticky second_discarded ==
               ideal_sticky first_discarded second_discarded)
let deep_underflow_sticky_is_exact first_discarded second_discarded = ()

(* The source's stated numeric bounds imply that a deep-underflow shift remains
   inside the doubled significand.  This is what makes the second-region test
   above available rather than shifting the entire source away. *)
val deep_underflow_shift_stays_in_workspace
      (ebits:pos{ebits >= 2}) (sbits:pos{sbits > pow2n ebits})
      (shift:nat)
  : Lemma
      (requires shift <= sbits + pow2n (ebits - 1) - 2)
      (ensures shift < 2 * (sbits + 4))
let deep_underflow_shift_stays_in_workspace ebits sbits shift =
  pow2n_step ebits

(* res_sig is normalized with its leading one at bit sbits+2.  Appending
   sbits+4 zeroes puts that bit at 2*sbits+6.  If a shift passes the padding,
   the bounds at lines 1139-1141 prove that this one survives and lands below
   bit sbits+6, inside the slice reduced to sticky. *)
val normalized_one_remains_in_sticky_slice
      (ebits:pos{ebits >= 2}) (sbits:pos{sbits > pow2n ebits})
      (shift:nat)
  : Lemma
      (requires
        sbits + 4 < shift /\
        shift <= sbits + pow2n (ebits - 1) - 2)
      (ensures
        shift <= 2 * sbits + 6 /\
        2 * sbits + 6 - shift < sbits + 6)
let normalized_one_remains_in_sticky_slice ebits sbits shift =
  pow2n_step ebits

(* Being below the ebits+2 signed rounder range forces at least an eight-bit
   right shift.  Hence the retained significand has a leading zero and adding
   one for rounding cannot carry into the minimum normal encoding
   (lines 1160-1164). *)
val deep_underflow_has_no_normal_carry
      (ebits:pos{ebits >= 2}) (shift:nat)
  : Lemma
      (requires 2 + 3 * pow2n (ebits - 1) <= shift)
      (ensures 8 <= shift)
let deep_underflow_has_no_normal_carry ebits shift = ()

(* ------------------------------------------------------------------------- *)
(* 4. IEEE 754 rounding decision and source truth-table equivalence.         *)
(* ------------------------------------------------------------------------- *)

(* Boolean transcription of fpa2bv_converter.cpp:4130-4146.  sign=true means
   a negative result; last is the least retained bit; round is the half-ulp
   bit; sticky is the OR of all less-significant discarded bits. *)
let cpp_rounding_increment
      (rm:rmode) (sign last round sticky:bool)
    : bool =
  match rm with
  | RNE -> round && (last || sticky)
  | RNA -> round
  | RTP -> not sign && (round || sticky)
  | RTN -> sign && (round || sticky)
  | RTZ -> false

(* IEEE 754-2019 4.3, expressed as the increment decision on a nonnegative
   retained magnitude. *)
let ieee_rounding_increment
      (rm:rmode) (sign last round sticky:bool)
    : bool =
  let inexact = round || sticky in
  match rm with
  | RNE -> round && (sticky || last)       (* nearest, ties to even *)
  | RNA -> round                           (* nearest, ties away *)
  | RTP -> not sign && inexact             (* toward +infinity *)
  | RTN -> sign && inexact                 (* toward -infinity *)
  | RTZ -> false                           (* toward zero *)

val rounding_decision_matches_ieee
      (rm:rmode) (sign last round sticky:bool)
  : Lemma (ensures cpp_rounding_increment rm sign last round sticky ==
                   ieee_rounding_increment rm sign last round sticky)
let rounding_decision_matches_ieee rm sign last round sticky = ()

(* Replacing the ideal sticky by the locally computed sticky therefore leaves
   every IEEE rounding mode unchanged. *)
val deep_underflow_rounding_is_equivalent
      (rm:rmode) (sign last round:bool)
      (first_discarded second_discarded:bool)
  : Lemma
      (requires (not first_discarded) \/ second_discarded)
      (ensures
        cpp_rounding_increment rm sign last round
          (cpp_sticky second_discarded)
        ==
        ieee_rounding_increment rm sign last round
          (ideal_sticky first_discarded second_discarded))
let deep_underflow_rounding_is_equivalent
      rm sign last round first_discarded second_discarded =
  deep_underflow_sticky_is_exact first_discarded second_discarded;
  rounding_decision_matches_ieee
    rm sign last round (ideal_sticky first_discarded second_discarded)

(* ------------------------------------------------------------------------- *)
(* 5. Shared-round shift cap.                                                *)
(* ------------------------------------------------------------------------- *)

let bounded_right_shift (sigma:int) (cap:nat) : nat =
  if sigma < 0
  then let magnitude = -sigma in if magnitude <= cap then magnitude else cap
  else 0

(* Lines 4265-4305 widen sigma before negation and represent cap in a width
   where it cannot wrap.  At the mathematical level this is exactly
   min(-sigma, cap), and it never exceeds cap. *)
val bounded_round_shift_is_safe (sigma:int) (cap:nat)
  : Lemma (ensures bounded_right_shift sigma cap <= cap)
let bounded_round_shift_is_safe sigma cap = ()

(* Concrete regression at FP(2,16): the old four-bit cap encoded 18 as 2,
   while the widened comparison keeps the required shift 6. *)
val fp_2_16_cap_regression (u:unit)
  : Lemma
      (ensures
        18 % pow2n 4 == 2 /\
        bounded_right_shift (-6) 18 == 6 /\
        bounded_right_shift (-6) 18 < 2 * (16 + 4))
let fp_2_16_cap_regression () =
  pow2n_step 4;
  pow2n_step 3;
  pow2n_step 2;
  pow2n_step 1

#pop-options

[Christoph M. Wintersteiger (wintersteiger)]

I haven't had any time too look at this yet, but from a cursory glance I'll have to go through the details of the division changes and I'm still unhappy with the changes to round. There is nothing here requires a change of rounding behavior and if we do change the rounder, we will have to run at least all SMT-LIB benchmarks because rounding is used literally in every single operation.

Nikolaj Bjorner (@NikolajBjorner): careful with IEEE 754: this PR is specifically about very weird formats, e.g. tiny width, or ebits > sbits, for which 754-assumptions and properties don't necessarily apply.

[Christoph M. Wintersteiger (wintersteiger)]

Unnecessary comment change; no need to comment on what you're keeping.

[Christoph M. Wintersteiger (wintersteiger)]

What's a "workspace"?

The exponent is always wide enough by definition, because we can't change the output width and the additional two bits in the input are enough to make any rounding decision. Is there an example of an operation different from division that requires these changes?

[Christoph M. Wintersteiger (wintersteiger)]

Is this about the potential corner-case during negation of sigma? I think that was covered before, but it's of course possible that I'm wrong. If so however, that would be fixed by making sigma one bit wider instead of this complicated construction here. I would like to see a concrete example of this though, ideally without involving division.