[−][src]Function image::imageops::overlay_bounds

pub fn overlay_bounds(
    (bottom_width, bottom_height): (u32, u32), 
    (top_width, top_height): (u32, u32), 
    x: u32, 
    y: u32
) -> (u32, u32)

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:

The main idea is to make use of inequalities provided by the nature of saturing_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:

  1. bottom.get_pixel(x + [0..x_range), y + [0..y_range))
  2. 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.