The temp allocator implementation isn't guaranteed to detect it, and the article doesn't go into implementation details and guarantees (which is good, because capabilities will be added on the road to 1.0).
> I tries searching how these contracts work in the C3 website [1] and these seems to be no guaranteed static checking of such contracts.
No, there is no guarantee at the language level because doing so would make a conforming implementation of the compiler harder than it needs to be. In addition, setting exact limits may hamper innovation of compilers that wish to add more analysis but will hesitate to reject code that can be statically know to violate contracts.
At higher optimizations, the compiler is allowed to assume that the contracts evaluate to true. This means that code like `assert(i == 1); if (i != 1) return false;` can be reduced to a no-op.
So the danger here is then if you rely on the function giving you a valid result even if the indata is not one that the function should work with.
And yes, it will be optional to have those "assumes" inserted.
Already today in current compiler, doing something trivial like writing `foo(0)` to a function that requires that the parameter > 1 is caught at compile time. And it's not doing any real analysis yet, but it will definitely happen.