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