Skip to content

elreal Phase 8: real floating-point conversion #932

@Ravenwater

Description

@Ravenwater

Parent epic: #923
Depends on: Phase 4 (addition) at minimum; ideally Phase 7 for full coverage

Goal

Round a `ZBCL` to a target floating-point format. This is how elreal interoperates with the rest of the library: take an exact-real intermediate, ask for a `double`, `cfloat<N,E>`, `dd`, or `qd` approximation.

Primitives

  • `round_to(ZBCL x) -> Target` with rounding mode parameter `{nearest, toward_zero, toward_pos_inf, toward_neg_inf}`. Default nearest.
  • Specialisations for common targets: `double`, `float`, `cfloat<N,E>`, `dd`, `qd`.

Correctness obligations

  • Idempotence: `round_to(round_to(x)) == round_to(x)` for the same rounding mode.
  • Monotonicity: rounding nested precisions is consistent. If `prec1 >= prec2`, then `round_to(round_to(x)) == round_to(x)`.
  • Determinism: same input + same rounding mode -> same output, independent of the path that produced the ZBCL.

Acceptance criteria

  • `round_to(ZBCL, rounding_mode)` implemented per dissertation 4.3
  • Four rounding modes supported: nearest, toward zero, toward +inf, toward -inf
  • Specialisations for `double`, `float`, `cfloat<...>`, `dd`, `qd`
  • Idempotence tested on random inputs
  • Monotonicity tested on prec pairs `(double, float)`, `(dd, double)`, `(qd, dd)`
  • Cross-check: `round_to(from_native(x)) == x` (lossless roundtrip)
  • Tests live in `elastic/elreal/rounding/`

Out of scope

  • IEEE-754 exception flag propagation (defer)
  • Stochastic rounding -- could be a future addition

Reference

McCleeary 2019 dissertation, Section 4.3 (real floating-point).

Metadata

Metadata

Assignees

No fields configured for Feature.

Projects

Status

No status

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions