uadd.sat(X, Y) u>= X + Y
usub.sat(X, Y) u<= X, Y
These patterns are found in harfbuzz/typst. Alive2: https://alive2.llvm.org/ce/z/cxyjYV