HOL-Light: Provide a document explaining specification style for correctness, memory-safety, and constant-time specs

[mkannwischer]

Identified during the 2026 soundness review (#1582, SOUNDNESS.md).

The HOL Light specifications encode functional correctness, memory safety, and secret-independent execution properties for the assembly routines. However, the specification style and conventions are not documented, making it difficult for external reviewers to assess the faithfulness of the specifications.

Provide a document explaining the specification style and conventions used in the HOL Light proofs.