In the typical framework (refinement), if you prove your function does X, Y, and Z, then it does exactly X, Y, and Z. Please don't take my comment out of the co

In the typical framework (refinement), if you prove your function does X, Y, and Z, then it does exactly X, Y, and Z. Please don't take my comment out of the context of formal, machine-checked proofs. It is hard, and that's my point.