I think that's not the point here. Consider this:
b = f(a)
c = g(b)
d = h(a, c)
Let's assume c results in -2 with a certain b.
Even if c=-2 and c=3 are interchangeable mathematically, h might not work as expected as the pair (a, c) belong together.
So, it could be the case that h(a, -2) != h(a, 3) for the very same a. This must be avoided at any cost.
That IS the case, as h == verify, verify WORKS (validates) on "3" (and it SHOULD work on "3") and doesn't work on "-2",
(that's why you can see those "Generated incorrect block messages")
The point here is: 'SHOULD work on "3"' has to be proved.
Maybe, there are some negative numbers c so that (a, c') validates ALTHOUGH a is invalid. (where c' is the positive equivalent of c)
Maybe not.
So, proof of the algo as well as the code is needed.
