Allow bedrock2 pipeline to call external functions.

[jadephilipoom]

This PR allows the bedrock2 backend for fiat-crypto to interpret add-carry and sub-borrow instructions by calling external bedrock2 functions. I changed the arguments to the fiat-crypto pipeline so that it produces expressions containing mul_split, add_get_carry, add_with_get_carry, sub_get_borrow, and sub_with_get_borrow, then implemented support for the add/sub instructions.

The next step is to add support for mul_split; I'd like to hand that task off to someone else at this point, but I prepared some debugging printouts in p224_64_new.v that are similar to the printouts I used while developing the add/sub code.

Other, secondary changes in this PR include:

• removing autogenerated names in the synthesis proofs
  • the spec_of preconditions added new hypotheses, which made the autogenerated names break; I tried to remove all the auto-generated names I came across
• adjusting how the Expr layer of the bedrock2 translation handles casts
  • previously we called the fiat-crypto pipeline with a flag that casted everything to the machine wordsize
  • to track bounds on carries we needed to remove that flag, so translate_expr now has to handle other cast sizes; it does this by introducing and operations whenever the cast doesn't match the word size. This might result in a few superfluous ands, but hopefully C compilers will be able to optimize them away.

Most of those secondary changes are one-time, so mul_split should be less complicated. The commit that adds subtraction (message: "works with sub, but fails to handle carries which are literals") should give a good sense of what needs to change to add a new special-case function