[first_amendment]

One is a requirement, the other is a promise. The promise "result >= 0" is necessary because the compiler may not be able to prove that on its own.