def packed_bounds

stelliferous@0.0.2.0 · kernel_shape.bend:31

import Base

31def packed_bounds(dimension: U32,+capacity: U32,coordinate: U32,+shape: Dimensions,input_length: Nat,weight_length: Nat) -> Bool:
32  Dimensions{+ci,+co,+height,+width,+kernel,+stride,+padding} = shape
33  +oh = axis_size(height,kernel,stride,padding)
34  +ow = axis_size(width,kernel,stride,padding)
35  +padded = Nat.mul(Nat.div(Nat.add(Nat.mul(oh,ow),7n),8n),8n)
36  direct_bounds(dimension,capacity,coordinate,shape,input_length,weight_length) &&
37  Nat.is_le(Nat.mul(padded,Nat.mul(ci,Nat.mul(kernel,kernel))),U32.to_nat(capacity)) &&
38  Nat.is_le(Nat.mul(padded,co),U32.to_nat(capacity))