TensorBandSchedule.sized: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/tensor_band_schedule.bend as TensorBandSchedule
Lines 24-34 of stelliferous@0.0.2.0/tensor_band_schedule.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/tensor_band_schedule.bend&start_line=24&end_line=34

import Base
import stelliferous@0.0.2.0/tensor_band.bend as Bands
import stelliferous@0.0.2.0/kernel_cost.bend as Cost

# The whole operation, not each leaf, must reach the grain: small leaves only
# lengthen the runtime's rounds, which the region estimate already counts.
def sized(geometry: Bands.Geometry,+workers: U32,element_ns: F32,config: Cost.Configuration,size: Size) -> Bool:
  Bands.Geometry{batch,channels,height,width} = geometry
  Cost.Configuration{mac,byte_ns,operation_ns,grain,wake} = config
  Size{+leaves,rows,maximum} = size
  +row_ns = (U32.to_f32(channels) * U32.to_f32(width) * element_ns : F32)
  +total = (U32.to_f32(height) * row_ns : F32)
  U32.is_eq(batch,1) && U32.is_lt(1,workers) && U32.is_lt(1,leaves) && U32.is_le(leaves,(U32.min(workers,858993459) * 5 : U32)) &&
    F32.is_le(grain,total) &&
    F32.is_lt((Cost.region_ns(workers,leaves,(U32.to_f32(maximum) * row_ns : F32)) + 2.0 * wake : F32),total)

Uses (18):
  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=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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.min
  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.to_f32
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_cost.bend&name=Configuration
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_cost.bend&name=region_ns
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_band.bend&name=Geometry
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_band_schedule.bend&name=Size