Add specification review checklist (Type 3)

[nebeid]

Summary

Fills in the empty "Type 3: Adding a New Specification" section of the PR review checklist based on John Harrison's presentation on formal specification style and validation (2026-04-08 team meeting).
The meeting discussed how specifications for non-mathematical functions (AES, SHA) carry higher risk of spec bugs than clean mathematical specs (bignum arithmetic, elliptic curves). The checklist now reflects this distinction and provides concrete validation steps for each case.

Changes

Adds checklist items covering:

• Specification style: abstract/mathematical over code-like; implication not equivalence
• Layered specifications: multiple levels with proven implications between them
• Spec validation ("gap A"): test vectors, cross-system comparison, human review of standards correspondence
• Executability (mathematical specs): abstract specs sacrifice executability for clarity — compensate with proven-equivalent executable forms or test-vector validation of the proof chain
• Standards relationship: documenting which standard is formalized, watching for implicit behaviors