pub fn overlay_bounds(
_: (u32, u32),
_: (u32, u32),
x: u32,
y: u32,
) -> (u32, u32)Expand description
Calculate the region that can be copied from top to bottom.
Given image size of bottom and top image, and a point at which we want to place the top image onto the bottom image, how large can we be? Have to wary of the following issues:
- Top might be larger than bottom
- Overflows in the computation
- Coordinates could be completely out of bounds
The main idea is to make use of inequalities provided by the nature of saturating_add and
saturating_sub. These intrinsically validate that all resulting coordinates will be in bounds
for both images.
We want that all these coordinate accesses are safe:
bottom.get_pixel(x + [0..x_range), y + [0..y_range))top.get_pixel([0..x_range), [0..y_range))
Proof that the function provides the necessary bounds for width. Note that all unaugmented math operations are to be read in standard arithmetic, not integer arithmetic. Since no direct integer arithmetic occurs in the implementation, this is unambiguous.
Three short notes/lemmata:
- Iff `(a - b) <= 0` then `a.saturating_sub(b) = 0`
- Iff `(a - b) >= 0` then `a.saturating_sub(b) = a - b`
- If `a <= c` then `a.saturating_sub(b) <= c.saturating_sub(b)`
1.1 We show that if `bottom_width <= x`, then `x_range = 0` therefore `x + [0..x_range)` is empty.
x_range
= (top_width.saturating_add(x).min(bottom_width)).saturating_sub(x)
<= bottom_width.saturating_sub(x)
bottom_width <= x
<==> bottom_width - x <= 0
<==> bottom_width.saturating_sub(x) = 0
==> x_range <= 0
==> x_range = 0
1.2 If `x < bottom_width` then `x + x_range < bottom_width`
x + x_range
<= x + bottom_width.saturating_sub(x)
= x + (bottom_width - x)
= bottom_width
2. We show that `x_range <= top_width`
x_range
= (top_width.saturating_add(x).min(bottom_width)).saturating_sub(x)
<= top_width.saturating_add(x).saturating_sub(x)
<= (top_wdith + x).saturating_sub(x)
= top_width (due to `top_width >= 0` and `x >= 0`)Proof is the same for height.