Function next_multiple_of 

pub open spec fn next_multiple_of(x: int, y: int) -> int

recommends

y > 0,

{ if x % y == 0 { x } else { x + (y - x % y) } }

The smallest multiple of y that is >= x (for y > 0), matching the value std’s next_multiple_of / checked_next_multiple_of compute.