Future: switch Float SMT encoding from Real to FPSort (IEEE-754)

[alcides]

Future work: switch Float SMT encoding from Real to FPSort

Today Float is encoded as z3 Real. This keeps SMT reasoning decidable, sort-uniform and rounding-mode-free, but it does not match runtime IEEE-754 semantics (rounding, overflow, NaN, infinities). This issue tracks what it would take to move to a true floating-point encoding (FPSort), and what we would gain. It is intentionally left for the future — it is a design change, not a one-line sort swap. See the analysis comments below for the empirical evidence (verified against z3 4.15.3) of why a naive swap fails.

Current state (entry points)

• get_sort: Float -> z3.RealSort() — aeon/verification/smt.py:554-555
• make_variable: Float vars -> Real(name) — aeon/verification/smt.py:631
• base_functions: all numeric operators (+ - * / == != < <= > >=) are generic Python operators shared between Int and Float — aeon/verification/smt.py:116-138

The Real encoding works precisely because that one generic, sort-agnostic operator table can serve both Int and Float.

What needs to be done

1. Introduce explicit float widths. There is no single "Float" in FP: results depend on precision (0.1 + 0.2 == 0.3 is unsat at FP64, sat over Real). A fixed FPSort(8, 24) bakes a representation choice into the type system, so this likely means a Float32/Float64 type family rather than one Float, with FPSort(8, 24) / FPSort(11, 53) respectively.
2. Make operator translation sort-aware. FP sorts do not mix with the Int/Real literals we emit (FP + IntVal(1) and FP + RealVal(1.5) both raise sort mismatch). translate_app / base_functions can no longer be type-agnostic: each operator must dispatch on operand sort and insert coercions (fpToReal, fpToFP, ToReal, fpToInt, …) for mixed Int/Float refinements.
3. Thread a rounding mode through arithmetic. FP + - * / require an explicit rounding mode (fpAdd(RNE(), x, y), not fpAdd(x, y)). Pick and thread a policy (default roundNearestTiesToEven), and decide whether it is user-controllable.
4. Handle NaN / infinities in comparisons. Over FP, x == x is not a tautology (NaN) and x + 1.0 > x can fail (infinities/saturation). Equality and ordering need FP-aware predicates (fpEQ, fpLT, …) and the type system must decide how NaN/Inf interact with refinements (e.g. exclude NaN by default, or expose isNaN/isInfinite).
5. Float literals. Emit FPVal(v, sort) instead of RealVal, and route literal typing through the chosen width.
6. Migrate / re-validate existing specs. Algebraic specs that verify today under Real (e.g. def half (x : Float) : {y:Float | y * 2.0 == x} = x / 2.0;) may no longer be valid under FP. Existing Float refinements and tests in tests/smt_test.py must be reviewed.

What would be gained

• Faithful runtime semantics: verification would reason about the same rounding/overflow/NaN behaviour that the evaluator actually produces, closing the gap where a refinement is proven over Real but violated at runtime by rounding.
• Ability to express and check FP-specific properties: NaN-freedom, absence of overflow/underflow, bounds that account for representable values, etc.
• Correctness for numerically sensitive code (the kind where 0.1 + 0.2 != 0.3 matters).

Trade-off to keep in mind

We would lose the exact, decidable, sort-uniform, rounding-free arithmetic that makes the current generic translation simple and makes clean algebraic refinements valid. FP solving is also generally harder for the SMT backend. A reasonable path is to keep Real as the default and add FP behind an explicit opt-in fixed-width float type, only where IEEE-754-accurate refinements are actually needed.

---

Note: the previous inline TODO/commented-out FPSort(8, 24) stub in make_variable was removed in #314; this issue is now the canonical record of the plan.

[alcides]

Why a fixed-precision FPSort does not work as a drop-in replacement for RealSort

I looked into swapping the current real encoding for z3 floating-point sorts. The relevant code is in aeon/verification/smt.py:

• smt_base_type_to_z3 maps t_float → z3.RealSort() (smt.py:108-109)
• float literals become z3.RealVal (smt.py:122-123)
• all arithmetic/comparison operators are translated generically with Python operators (+, -, *, /, <, ==, …) in translate_app (smt.py:155-188)

Switching t_float to z3.FPSort(e, s) (e.g. Float32 = FPSort(8, 24), Float64 = FPSort(11, 53)) breaks in several ways. I verified each of these against z3 4.15.3:

1. FP sorts don't mix with the Int/Real sorts we already emit

Aeon emits IntVal/RealVal for int/float literals and shares operator translation across all numeric types. An FPSort term cannot be combined with either:

x : FPSort(8,24)
x + IntVal(1)    -> Z3Exception: sort mismatch
x + RealVal(1.5) -> Z3Exception: sort mismatch

So translate_app can no longer be type-agnostic; every operator would need to know the operand sort and insert conversions (fpToReal, fpToFP, ToReal, …). Mixed Int/Float refinements would need explicit coercions everywhere.

2. FP operations require an explicit rounding mode

Unlike Real, FP arithmetic is not just a + b:

fpAdd(x, y)      -> Z3Exception: sort mismatch   (no rounding mode)
fpAdd(RNE(), x, y) -> fpADD(roundNearestTiesToEven, x, y)  (ok)

Every + - * / would have to thread a rounding mode through, and the rounding-mode choice is itself a semantic decision that real arithmetic doesn't have.

3. NaN / infinities break the equational reasoning refinements rely on

Over reals, basic facts that liquid types depend on are tautologies. Over FP they are not:

exists x. not(x == x)        -> sat    (x = NaN; reflexivity of == fails)
exists x. not(x + 1.0 > x)   -> sat    (infinities / saturation)

Refinements like {y:Float | y == y} or {y:Float | y + 1.0 > y} would suddenly become invalid, so existing specs would stop verifying.

4. Results depend on the precision you pick — there is no single "Float"

The same refinement gives different answers at different widths, so a fixed precision bakes a representation choice into the type system:

FP64:  0.1 + 0.2 == 0.3   -> unsat   (false, matches IEEE-754 double)
Real:  0.1 + 0.2 == 0.3   -> sat     (true)

Today this verifies exactly because of the real encoding:

def half (x : Float) : {y:Float | y * 2.0 == x} { x / 2.0 }

half(10.0) returns 5.0 and the spec y * 2.0 == x holds exactly. Under FP, division + equality reasoning is subject to rounding and this kind of clean algebraic spec is no longer generally valid.

Summary

Reals give exact, sort-uniform, rounding-mode-free, total arithmetic, which is what makes the current generic translation in translate_app work and what most refinements implicitly assume. A fixed-precision FPSort would require: per-operand sort tracking and coercions, an explicit rounding-mode policy, handling of NaN/Inf in every comparison, and would change which refinements are valid depending on the chosen width. That's why a straight RealSort → FPSort swap doesn't work; modelling true float semantics is a much larger design change (effectively a separate Float32/Float64 type family with FP-aware translation), not a one-line sort substitution.

[alcides]

Why FPSort with a fixed precision does not work as a drop-in for RealSort

I re-investigated the commented-out FPSort(8, 24) path. Current code references (line numbers have shifted since the issue was filed):

• get_sort maps Float → z3.RealSort() — aeon/verification/smt.py:554-555
• make_variable builds Float vars as z3.Real(name), with the FPSort/FP attempt left as a TODO — aeon/verification/smt.py:631-638
• all numeric operators are translated with plain Python operators in base_functions (x + y, x == y, x < y, …) and are shared between Int and Float — aeon/verification/smt.py:115-138

The last point is the crux: the translation is deliberately sort-agnostic. Real is the only numeric sort that lets one set of generic operators serve both Int and Float. Swapping in FPSort breaks that in four independent ways. I reproduced each against z3 4.15.3:

1. FP sorts don't mix with the Int/Real terms we emit

x : FPSort(8,24)
x + IntVal(1)      # Z3Exception: sort mismatch
x + RealVal(1.5)   # Z3Exception: sort mismatch
x + FPVal(1.0, fp) # ok

translate_app could no longer be type-agnostic — every operator would need to know its operand sort and insert coercions (fpToReal, fpToFP, ToReal, …). Mixed Int/Float refinements would need explicit casts everywhere.

2. FP arithmetic needs an explicit rounding mode

fpAdd(x, y)        # error: missing argument (no rounding mode)
fpAdd(RNE(), x, y) # ok

Every + - * / would have to thread a rounding mode through, and picking one is itself a semantic decision that real arithmetic doesn't force on us.

3. NaN / infinities break the equational reasoning refinements rely on

Facts that are tautologies over Real become satisfiable (i.e. have counterexamples) over FP:

exists x. not(x == x)        # reals: unsat   | FP: sat  (x = NaN)
exists x. not(x + 1.0 > x)   # FP: sat  (infinities / saturation)

So refinements like {y:Float | y == y} or {y:Float | y + 1.0 > y} would stop verifying. Both verify today under the Real encoding — confirmed by running them through aeon.

4. Results depend on the width you pick — there is no single "Float"

0.1 + 0.2 == 0.3   # reals: sat (true) | FP64: unsat (false, matches IEEE-754)

A fixed precision bakes a representation choice into the type system. This spec verifies today precisely because of the real encoding:

def half (x : Float) : {y:Float | y * 2.0 == x} = x / 2.0;

half 10.0 returns 5.0 and y * 2.0 == x holds exactly. Under FP, division + equality is subject to rounding and this kind of clean algebraic spec is no longer generally valid.

Conclusion

Real gives exact, sort-uniform, rounding-mode-free, total arithmetic — exactly the properties that let the generic base_functions translation serve every numeric type and that most refinements implicitly assume. A RealSort → FPSort swap would require per-operand sort tracking + coercions, an explicit rounding-mode policy, NaN/Inf handling in every comparison, and would change which refinements are valid depending on the chosen width. Modelling true float semantics is therefore a much larger design change — effectively a separate Float32/Float64 type family with FP-aware translation — not a one-line sort substitution. Recommendation: keep the Real encoding; only pursue FP behind an explicit opt-in fixed-width float type if/when IEEE-754-accurate refinements are actually needed.

_{Verified empirically against z3 4.15.3; aeon Float examples (half, {y:Float | y == y}, {y:Float | y + 1.0 > y}) run and verify under the current encoding; tests/smt_test.py green.}

[alcides]

Closing as wontfix: the issue is intentionally deferred, and the current Real-based Float encoding remains the supported design.