KernelWindow.covers: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/kernel_window.bend as KernelWindow
Lines 28-45 of stelliferous@0.0.2.0/kernel_window.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/kernel_window.bend&start_line=28&end_line=45

import Base

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

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_window.bend&name=Band