KernelShape.direct_bounds: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/kernel_shape.bend as KernelShape
Lines 19-29 of stelliferous@0.0.2.0/kernel_shape.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/kernel_shape.bend&start_line=19&end_line=29

import Base

def direct_bounds(+dimension: U32,+capacity: U32,+coordinate: U32,shape: Dimensions,input_length: Nat,weight_length: Nat) -> Bool:
  Dimensions{+ci,+co,+height,+width,+kernel,+stride,+padding} = shape
  +oh = axis_size(height,kernel,stride,padding)
  +ow = axis_size(width,kernel,stride,padding)
  Nat.is_le(ci,U32.to_nat(dimension)) && Nat.is_le(co,U32.to_nat(dimension)) &&
  Nat.is_le(height,U32.to_nat(dimension)) && Nat.is_le(width,U32.to_nat(dimension)) &&
  Nat.is_le(kernel,U32.to_nat(dimension)) && Nat.is_le(stride,U32.to_nat(dimension)) && Nat.is_le(padding,U32.to_nat(dimension)) &&
  Nat.is_le(input_length,U32.to_nat(capacity)) && Nat.is_le(weight_length,U32.to_nat(capacity)) &&
  Nat.is_le(Nat.mul(co,Nat.mul(oh,ow)),U32.to_nat(capacity)) &&
  Nat.is_le(Nat.add(Nat.mul(oh,stride),kernel),U32.to_nat(coordinate)) &&
  Nat.is_le(Nat.add(Nat.mul(ow,stride),kernel),U32.to_nat(coordinate))

Uses (10):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.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.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_shape.bend&name=Dimensions
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_shape.bend&name=axis_size