Adds hardened preconditions (bounds checks and similar) that implementations may enable, specified with contract semantics.