TensorConvolution.dense_call_valid: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/tensor_convolution.bend as TensorConvolution
Lines 220-228 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=220&end_line=228

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

# What a dense call needs of its three buffers: lengths that fit the shape and
# the capacities that hold them.
def dense_call_valid(+dimensions: KernelShape.Dimensions,+count: U32,+input_length: Nat,+input_depth: Nat,+weight_length: Nat,+weight_depth: Nat,
  +bias_length: Nat,+bias_depth: Nat) -> Bool:
  KernelShape.Dimensions{+ci,rows,+h,+w,k,s,p} = dimensions
  KernelShape.valid(dimensions,Nat.mul(ci,Nat.mul(h,w)),weight_length,bias_length) &&
    Nat.is_eq(input_length,Nat.mul(U32.to_nat(count),Nat.mul(ci,Nat.mul(h,w)))) &&
    Nat.is_le(input_length,U32.to_nat(U32.shln(1,input_depth))) &&
    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 (11):
  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.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