Epic: bring Checked C specification into agreement with the compiler implementation

[dtarditi]

The Checked C specification currently describes features that aren't implemented and doesn't describe some features that are implemented. This makes it confusing for programmers to use. We should update it to clearly describe what is implemented and move future work to the end.

Here is the list of work to do:

• Update description of program scopes for checked pointer types in specification #491
• Move planned features to a new section in the specification #492
• Remove speculative features from specification #493
• Move static checking descriptions of bounds to the end of the specification. #494
• Update description of flow-sensitive bounds declarations. #495
• Update description of generic types in the specification #497
• Add description of format string support checking for varargs #499
• Improve description of bounds widening #500.