def direct_bounds

stelliferous@0.0.2.0 · kernel_shape.bend:19

import Base

19def direct_bounds(+dimension: U32,+capacity: U32,+coordinate: U32,shape: Dimensions,input_length: Nat,weight_length: Nat) -> Bool:
20  Dimensions{+ci,+co,+height,+width,+kernel,+stride,+padding} = shape
21  +oh = axis_size(height,kernel,stride,padding)
22  +ow = axis_size(width,kernel,stride,padding)
23  Nat.is_le(ci,U32.to_nat(dimension)) && Nat.is_le(co,U32.to_nat(dimension)) &&
24  Nat.is_le(height,U32.to_nat(dimension)) && Nat.is_le(width,U32.to_nat(dimension)) &&
25  Nat.is_le(kernel,U32.to_nat(dimension)) && Nat.is_le(stride,U32.to_nat(dimension)) && Nat.is_le(padding,U32.to_nat(dimension)) &&
26  Nat.is_le(input_length,U32.to_nat(capacity)) && Nat.is_le(weight_length,U32.to_nat(capacity)) &&
27  Nat.is_le(Nat.mul(co,Nat.mul(oh,ow)),U32.to_nat(capacity)) &&
28  Nat.is_le(Nat.add(Nat.mul(oh,stride),kernel),U32.to_nat(coordinate)) &&
29  Nat.is_le(Nat.add(Nat.mul(ow,stride),kernel),U32.to_nat(coordinate))