`Verify` and `NoVerify` types for fragments and functions

[andrew-johnson-4]

Verify fragments and functions are required to prove all properties that they declare or depend on. Verify dependencies must also be either Verify or NoVerify. A compiler flag could be used to add Verify to all bindings which would make the program very strict. Library kernels could be frozen with very few NoVerify symbols.

This is the basis of 100% formally verified code. Fully verified includes explicit memory model with limited hard-coded assumptions such as sys_brk SUCCESS.