// A 32767-pixel axis bound keeps width*height*3 within unsigned 32-bit range.
// Reject larger records before using their addresses, including wrapped extents.
%gg = buffer.assume.memory_space<global> %geometry : buffer
%gv = buffer.view %gg[%off] : buffer -> view<@GEOMETRY_COUNT@xi32>
%g0raw = index.mul %face, %three : index
%g1raw = index.add %g0raw, %one : index
%g2raw = index.add %g0raw, %two : index
%g0 = index.assume %g0raw [range(%g0raw, 0, @GEOMETRY_LAST@)] : index
%g1 = index.assume %g1raw [range(%g1raw, 0, @GEOMETRY_LAST@)] : index
%g2 = index.assume %g2raw [range(%g2raw, 0, @GEOMETRY_LAST@)] : index
%offset_i = view.load %gv[%g0] : view<@GEOMETRY_COUNT@xi32> -> i32
%width_i = view.load %gv[%g1] : view<@GEOMETRY_COUNT@xi32> -> i32
%height_i = view.load %gv[%g2] : view<@GEOMETRY_COUNT@xi32> -> i32
%offset_raw = index.cast %offset_i : i32 to index
%width_raw = index.cast %width_i : i32 to index
%height_raw = index.cast %height_i : i32 to index
%input_size = index.constant @INPUT@ : index
%offset_ok = index.cmp ult, %offset_raw, %input_size : index
%axis_limit = index.constant 32767 : index
%width_ok = index.cmp ule, %width_raw, %axis_limit : index
%height_limit_ok = index.cmp ule, %height_raw, %axis_limit : index
%width_nonzero = index.cmp ugt, %width_raw, %zero : index
%height_nonzero = index.cmp ugt, %height_raw, %zero : index
%safe_offset = scf.select %offset_ok, %offset_raw, %zero : index
%safe_width = scf.select %width_ok, %width_raw, %one : index
%sw_raw = scf.select %width_nonzero, %safe_width, %one : index
%sw = index.assume %sw_raw [range(%sw_raw, 1, 32767)] : index
%source_offset = index.assume %safe_offset [range(%safe_offset, 0, @LAST_INPUT@)] : index
%available_raw = index.sub %input_size, %source_offset : index
%available = index.assume %available_raw [range(%available_raw, 0, @INPUT@)] : index
%available_i = index.cast %available : index to i32
%channels_i = scalar.constant 3 : i32
%area_i = scalar.muli %width_i, %height_i : i32
%extent_i = scalar.muli %area_i, %channels_i : i32
%extent_ok = scalar.cmpi ule, %extent_i, %available_i : i32
%height_ok = scalar.andi %height_limit_ok, %extent_ok : i1
%ok0 = scalar.andi %offset_ok, %width_ok : i1
%ok1 = scalar.andi %width_nonzero, %height_nonzero : i1
%ok2 = scalar.andi %ok0, %ok1 : i1
%geometry_ok = scalar.andi %ok2, %height_ok : i1
%fw = scalar.uitofp %width_i : i32 to f32
%fh = scalar.uitofp %height_i : i32 to f32