KernelShape.packed_bounds: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/kernel_shape.bend as KernelShape
Lines 31-38 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=31&end_line=38

import Base

def packed_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)
  +padded = Nat.mul(Nat.div(Nat.add(Nat.mul(oh,ow),7n),8n),8n)
  direct_bounds(dimension,capacity,coordinate,shape,input_length,weight_length) &&
  Nat.is_le(Nat.mul(padded,Nat.mul(ci,Nat.mul(kernel,kernel))),U32.to_nat(capacity)) &&
  Nat.is_le(Nat.mul(padded,co),U32.to_nat(capacity))

Uses (12):
  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.div
  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
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/kernel_shape.bend&name=direct_bounds