more thoughts on adding constraints to models

Ran into a (probably minor) problem:
A type definition introduces both a new type and some new constants. If
the type is constrained but the constants are not, there is no guarantee
that the default (non-constrained) semantics of the constants will be
suitable for the new (constrained) value of the type. So there will
probably need to be some condition on the constraints, saying that if
you constrain a type, you also have to constrain any constants whose
types include that type.
prove constrained interpretation is still well-formed

needed to add a condition on the constraints as described in previous
commit
Speed up ASM -> x86-64 proof.

The x64_enc_deterministic proof was taking a long time. The total build time
has gone from 1.5hrs to about 9 minutes.
strengthen compile_special_thm, weaken COMPILER_RUN_INV

we know the handler will not change
add targets/x64 to build-sequence
Merge remote-tracking branch 'origin/master' into fmap_refactor