def valid

stelliferous@0.0.2.0 · kernel_shape.bend:12

import Base

12def valid(shape: Dimensions,input_length: Nat,weight_length: Nat,bias_length: Nat) -> Bool:
13  Dimensions{+ci,+co,+height,+width,+kernel,+stride,+padding} = shape
14  Nat.is_lt(0n,ci) && Nat.is_lt(0n,co) && Nat.is_lt(0n,height) && Nat.is_lt(0n,width) && Nat.is_lt(0n,kernel) && Nat.is_lt(0n,stride) &&
15  Nat.is_le(kernel,Nat.add(height,Nat.mul(2n,padding))) && Nat.is_le(kernel,Nat.add(width,Nat.mul(2n,padding))) &&
16  Nat.is_eq(input_length,Nat.mul(ci,Nat.mul(height,width))) &&
17  Nat.is_eq(weight_length,Nat.mul(co,Nat.mul(ci,Nat.mul(kernel,kernel)))) && Nat.is_eq(bias_length,co)