implicit_predicates_gen/range.rs
1//! The range of leaf magnitudes and the buffer sizes of the exact stages.
2//!
3//! An exact stage evaluates a polynomial bottom up with floating-point
4//! expansions: a product of two `f64` is `two_product`, an expansion times an
5//! `f64` is a scaling, an expansion times an expansion is a sum of scalings,
6//! and sums and differences are exact merges. Every exact product of the
7//! arithmetic core needs both operands to be zero or to lie in its product
8//! domain, and every value it handles must stay below `2^1020`. This module
9//! derives the inputs for which that holds, and how long each temporary
10//! expansion can get.
11
12mod shape;
13
14use crate::differences::DiffGraph;
15use crate::dyadic::Dyadic;
16use crate::error::Error;
17use crate::graph::Graph;
18use crate::parse::Position;
19use shape::{MAX_LENGTH, Shape};
20
21/// The exponent of the overflow limit of the arithmetic core: every
22/// component and scalar operand of its expansion functions has magnitude
23/// below `2^1020`.
24const OVERFLOW_EXPONENT: i64 = 1020;
25
26/// The magnitudes of leaves for which an exact stage is valid: every
27/// nonzero leaf `x` must satisfy `min <= |x| <= max`. Both are powers of two.
28///
29/// A leaf is an input coordinate for the raw form, the computed difference
30/// for a difference form with [`Leaves::One`], and each of the two
31/// coordinates that are subtracted for a difference form with
32/// [`Leaves::Two`].
33///
34/// # Why the range is sufficient
35///
36/// Write `m = min`, `M = max` and `u = 2^-53`.
37///
38/// **Grid.** A nonzero `f64` of magnitude at least `m`, a normal power of
39/// two, is an integer multiple of `q = m 2^-52`; so is zero. For a power of
40/// two `g`, the rounding of a multiple of `g` to `f64` is a multiple of `g`:
41/// where the spacing of `f64` near the value is at least `g`, every `f64`
42/// there is a multiple of `g`; where it is smaller, the value is
43/// representable and rounds to itself. Every error-free transformation
44/// returns a rounded value and the exact difference between the true result
45/// and it, so with multiples of `g` as inputs (of `g_a g_b` for a product of
46/// multiples of `g_a` and `g_b`) both outputs are multiples of `g`. Hence
47/// every value an evaluation handles, every component of the expansion of a
48/// node included, is a multiple of the node's *grid*: `q` for a leaf (also
49/// for both components of a difference `two_diff(a, b)`, which can be far
50/// below `m` after cancellation but are still multiples of `q`), the smaller
51/// grid of the operands for a sum, and the product of the grids for a
52/// product. A nonzero component is at least its grid in magnitude; for a
53/// node of degree `g` in the leaves, the grid is `q^g`.
54///
55/// **Magnitude.** Each error-free transformation turns inputs `a`, `b`
56/// into `x + y = r`, where `r` is `a + b` or `a b`, with `|y| <= u |x|`;
57/// then `|x| <= |r| / (1 - u)` and `|x| + |y| <= (1 + 3u)(|a| + |b|)`, or
58/// `(1 + 3u) |a| |b|` for a product. Follow the multiset of values an
59/// evaluation holds (pending inputs, with the factor of a scaling applied,
60/// and outputs): its sum of magnitudes grows by at most a factor `1 + 3u` per
61/// transformation, and the output expansion is part of it. So the sum of the
62/// magnitudes of the components of a node, and every value handled on the
63/// way, is at most `(1 + 3u)^T S <= (1 + 6uT) S`, where `T <= 2^51` is the
64/// number of transformations the node depends on, counted with multiplicity
65/// (see the operation counts below), and `S` follows the structure: `M` for
66/// a coordinate or a computed difference, `2M` for the two components of a
67/// difference of coordinates, `|n|` for a constant `n`, the sum of the
68/// operands' `S` for a sum or difference, their product for a product.
69///
70/// **Rule.** The range is the widest pair of powers of two within
71/// `[operand_min, operand_max]` such that, for every operand of every
72/// product, the grid is at least `operand_min` and `(1 + 6uT) S` is at most
73/// `operand_max`, and `(1 + 6uT) S < 2^1020` at every node. Every factor
74/// of every exact product is then zero or in the product domain, and no value
75/// overflows. The grid condition depends only on `m` and the magnitude
76/// conditions only on `M`, and both are monotone, so the two ends are found
77/// separately.
78///
79/// The operation counts, with `l_x` the worst-case length of `x`: a
80/// difference of two coordinates is one transformation; a sum or difference
81/// at most `2 (l_x + l_y)`; a product at most `3 l_x l_y` for the exact
82/// products of the scalings plus `4 l_x l_y (l_x + l_y)` for merging them,
83/// whichever operand is scaled and in whatever order the scalings are
84/// merged.
85#[derive(Clone, Copy, Debug, PartialEq)]
86pub struct ExactRange {
87 /// The smallest admissible magnitude of a nonzero leaf.
88 pub min: f64,
89 /// The largest admissible magnitude of a leaf.
90 pub max: f64,
91}
92
93/// What an exact stage needs: the range of its leaves and the size of its
94/// temporaries.
95#[derive(Clone, Debug, PartialEq)]
96pub struct ExactPlan {
97 /// The magnitudes of the leaves for which the stage is valid.
98 pub range: ExactRange,
99 /// The worst-case length of the expansion of each node, in the order of
100 /// the graph: 1 or 2 for a leaf (see [`Leaves`]), 1 for a nonzero
101 /// constant and 0 for zero, `l_x + l_y` for a sum or difference,
102 /// `2 l_x l_y` for a product and `l_x` for a negation.
103 pub lengths: Vec<usize>,
104 /// The sum of `lengths`: the size of all the temporaries, each shared
105 /// node counted once.
106 pub total: usize,
107}
108
109/// The components of each leaf of a difference form.
110#[derive(Clone, Copy, Debug, PartialEq, Eq)]
111pub enum Leaves {
112 /// One: every difference was computed exactly in `f64`.
113 One,
114 /// Two: each difference is the exact `two_diff` of two coordinates.
115 Two,
116}
117
118/// Derives the exact stage of the raw form, whose leaves are the input
119/// coordinates, for the product domain `[operand_min, operand_max]`.
120///
121/// See [`ExactRange`] for the rule and why it is sound.
122///
123/// # Errors
124///
125/// Returns an error, at `position` (the name of the form) in `file`, when no
126/// range satisfies the rule, when a constant is not exact in `f64`, or when
127/// the evaluation is too large: a temporary longer than `2^32` components,
128/// temporaries longer than that in all, or a node that depends on more than
129/// `2^51` error-free transformations.
130///
131/// # Panics
132///
133/// Panics if `operand_min` and `operand_max` are not normal powers of two
134/// with `operand_min <= operand_max`.
135pub fn exact_plan_raw(
136 graph: &Graph,
137 file: &str,
138 position: Position,
139 operand_min: f64,
140 operand_max: f64,
141) -> Result<ExactPlan, Error> {
142 let (low, high) = domain(operand_min, operand_max);
143 Shape::raw(graph)
144 .and_then(|shape| plan(&shape, low, high))
145 .map_err(|message| Error::at(file, position, message))
146}
147
148/// Derives the exact stage of a difference form whose leaves have the given
149/// number of components, for the product domain `[operand_min, operand_max]`.
150///
151/// See [`ExactRange`] for the rule and why it is sound.
152///
153/// # Errors
154///
155/// As [`exact_plan_raw`], except that a difference form has no constants.
156///
157/// # Panics
158///
159/// As [`exact_plan_raw`].
160pub fn exact_plan_differences(
161 graph: &DiffGraph,
162 leaves: Leaves,
163 file: &str,
164 position: Position,
165 operand_min: f64,
166 operand_max: f64,
167) -> Result<ExactPlan, Error> {
168 let (low, high) = domain(operand_min, operand_max);
169 Shape::differences(graph, leaves)
170 .and_then(|shape| plan(&shape, low, high))
171 .map_err(|message| Error::at(file, position, message))
172}
173
174/// The exponents of the bounds of the product domain.
175fn domain(operand_min: f64, operand_max: f64) -> (i64, i64) {
176 let (low, high) = (exponent(operand_min), exponent(operand_max));
177 assert!(low <= high, "the product domain is empty");
178 (low, high)
179}
180
181/// The plan for the product domain `[2^low, 2^high]`, or the message to
182/// report.
183fn plan(shape: &Shape, low: i64, high: i64) -> Result<ExactPlan, String> {
184 let min = first_failure(low, high, |m| !grids_fit(shape, m, low));
185 let max = first_failure(low, high, |big_m| magnitudes_fit(shape, big_m, high)) - 1;
186 if min > high || max < low || min > max {
187 let degree = shape
188 .operands()
189 .map(|x| shape.degrees[x])
190 .max()
191 .unwrap_or(0);
192 return Err(format!(
193 "no input range keeps every exact product inside the operand domain \
194 [2^{low}, 2^{high}] of the exact arithmetic: a product operand of \
195 degree {degree} needs nonzero inputs of magnitude at least 2^{min}, \
196 and keeping every operand within the domain and every value below \
197 2^{OVERFLOW_EXPONENT} needs inputs of at most 2^{max}"
198 ));
199 }
200 let total = shape
201 .lengths
202 .iter()
203 .try_fold(0u64, |sum, &n| sum.checked_add(n as u64))
204 .filter(|&total| total < MAX_LENGTH)
205 .ok_or_else(|| {
206 "the expression is too large for exact evaluation: its temporaries \
207 would need 2^32 components or more in all"
208 .to_string()
209 })?;
210 Ok(ExactPlan {
211 range: ExactRange {
212 min: Dyadic::pow2(min).round_up(),
213 max: Dyadic::pow2(max).round_up(),
214 },
215 lengths: shape.lengths.clone(),
216 total: usize::try_from(total).expect("below 2^32"),
217 })
218}
219
220/// Whether, with nonzero leaves of magnitude at least `2^m`, every nonzero
221/// component of every product operand is at least `2^low`.
222fn grids_fit(shape: &Shape, m: i64, low: i64) -> bool {
223 let grids = shape.grids(m);
224 shape
225 .operands()
226 .all(|x| grids[x].is_none_or(|grid| grid >= low))
227}
228
229/// Whether, with leaves of magnitude at most `2^big_m`, every component of
230/// every product operand is at most `2^high` and every value is below the
231/// overflow limit.
232fn magnitudes_fit(shape: &Shape, big_m: i64, high: i64) -> bool {
233 let bounds = shape.component_bounds(big_m);
234 let overflow = Dyadic::pow2(OVERFLOW_EXPONENT);
235 let operand_max = Dyadic::pow2(high);
236 bounds.iter().all(|bound| *bound < overflow)
237 && shape.operands().all(|x| bounds[x] <= operand_max)
238}
239
240/// The first `e` in `low..=high` for which `holds(e)` is false, or
241/// `high + 1`, for a `holds` that is true up to some point and false after.
242fn first_failure(low: i64, high: i64, holds: impl Fn(i64) -> bool) -> i64 {
243 let (mut low, mut high) = (low, high + 1);
244 while low < high {
245 let middle = low + (high - low) / 2;
246 if holds(middle) {
247 low = middle + 1;
248 } else {
249 high = middle;
250 }
251 }
252 low
253}
254
255/// The exponent of a normal power of two.
256fn exponent(x: f64) -> i64 {
257 assert!(
258 x.is_normal() && x > 0.0 && x.to_bits() & ((1 << 52) - 1) == 0,
259 "a bound of the product domain must be a normal power of two, not {x}"
260 );
261 i64::try_from(x.to_bits() >> 52).expect("11 bits") - 1023
262}
263
264#[cfg(test)]
265mod tests;