TensorConvolution.band_call_valid: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/tensor_convolution.bend as TensorConvolution
Lines 285-295 of stelliferous@0.0.2.0/tensor_convolution.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/tensor_convolution.bend&start_line=285&end_line=295

import Base
import stelliferous@0.0.2.0/kernel_shape.bend as KernelShape
import stelliferous@0.0.2.0/tensor_band.bend as Bands

# What a call on bands needs: bands that cover the images of the geometry, and
# parameters whose lengths fit the shape and their capacities.
def band_call_valid(+dimensions: KernelShape.Dimensions,+count: U32,layout: Bands.Geometry,inspection: Bands.Inspection,+weight_length: Nat,+weight_depth: Nat,
  +bias_length: Nat,+bias_depth: Nat) -> Bool:
  KernelShape.Dimensions{+ci,rows,+h,+w,k,s,p} = dimensions
  Bands.Geometry{batch,channels,height,width} = layout
  Bands.Inspection{valid,first,end,leaves} = inspection
  valid && U32.is_zero(first) && Nat.is_eq(U32.to_nat(end),Nat.mul(U32.to_nat(count),h)) &&
    U32.is_eq(batch,count) && Nat.is_eq(U32.to_nat(channels),ci) && Nat.is_eq(U32.to_nat(height),h) && Nat.is_eq(U32.to_nat(width),w) &&
    KernelShape.valid(dimensions,Nat.mul(ci,Nat.mul(h,w)),weight_length,bias_length) &&
    Nat.is_le(weight_length,U32.to_nat(U32.shln(1,weight_depth))) && Nat.is_le(bias_length,U32.to_nat(U32.shln(1,bias_depth)))

Uses (15):
  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.is_eq
  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.is_eq
  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.shln
  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=valid
  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.bend&name=Inspection