Function bounded_sum

examples/06_effectful_verifier/python/main.py:57–60

(x: Annotated[int, Gt(0)], y: Annotated[int, Gt(0)])

def bounded_sum(x: Annotated[int, Gt(0)], y: Annotated[int, Gt(0)]):
    s = x + y
    assert_refined(s, Gt(1))  # x > 0 ∧ y > 0 → x + y > 1   ✓
    assert_refined(s, Ge(2))  # x > 0 ∧ y > 0 → x + y >= 2  ✓


assert verify(bounded_sum)