Define a common Validatable trait

[robin-aws]

In all my experimentation with creating an "external invariant" in order to allow a subset of preconditions and postconditions on external methods, the idea of a generic trait that defines the Valid() predicate seems to be a necessary piece of the puzzle.

I have a version that seems to work well which we should be able to apply to the ESDK ahead of time, which will help establish this idiom better for new Dafny programmers, reduce some code duplication, and make some progress towards the eventual solution for #165.