def covers

stelliferous@0.0.2.0 · kernel_window.bend:28

import Base

28# The checked facts that let a band stand in for its parent over a nonempty
29# span: rows inside the parent window, a stride-aligned first row that no read
30# needs above, an end no read needs below (or the image end), and room for the
31# kernel. The comparisons avoid wrapped sums: rows are bounded by the parent end
32# minus the first row. Pipelines copy only a band that passes; any other split
33# keeps a clone of the parent.
34def covers(+parent_first: U32,+parent_rows: U32,+height: U32,+kernel: U32,+stride: U32,+padding: U32,+output_width: U32,+offset: U32,+span: U32,
35  +band: Band) -> Bool:
36  Band{+first,+rows} = band
37  +parent_end = (parent_first + parent_rows : U32)
38  +top = (offset / output_width * stride : U32)
39  +bottom = ((offset + span - 1) / output_width * stride + kernel : U32)
40  +end = (first + rows : U32)
41  U32.is_lt(0,span) && U32.is_lt(0,rows) && U32.is_le(parent_first,first) && U32.is_le(first,parent_end) &&
42    U32.is_le(rows,(parent_end - first : U32)) && U32.is_zero((first % stride : U32)) &&
43    (U32.is_zero(first) || U32.is_le((first + padding : U32),top)) &&
44    (U32.is_eq(end,height) || U32.is_le(bottom,(end + padding : U32))) &&
45    U32.is_le(kernel,(rows + padding + padding : U32))