def pool_geometry

stelliferous@0.0.2.0 · tensor_operations.bend:186

import Base
import stelliferous@0.0.2.0/tensor_access.bend as Access

186# The window geometry is exact and every sample address stays in U32.
187def pool_geometry(+pool: Access.Pool) -> Bool:
188  Access.Pool{+height,+width,+kernel,+stride,+padding,+out_height,+out_width} = pool
189  small(height) && small(width) && small(kernel) && small(stride) && small(padding) && U32.is_lt(0,kernel) && U32.is_lt(0,stride) &&
190    U32.is_le(kernel,(height + 2 * padding : U32)) && U32.is_le(kernel,(width + 2 * padding : U32)) &&
191    U32.is_eq(out_height,((height + 2 * padding - kernel : U32) / stride + 1 : U32)) &&
192    U32.is_eq(out_width,((width + 2 * padding - kernel : U32) / stride + 1 : U32))