Add simple ensures, requires, safety predicates

[celinval]

I also added one proof-of-concept harness to ensure Kani can verify it.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.