Reviewing guidelines

This page contains some guidelines for potential reviewers of new and updated specs.

Questions to ask

• Look for all the checkboxes in the gold standard list
• Does the structure of the implementation match the original human-readable spec? It should be easy to scroll down the spec and the implementation at the same time and see the same functions in the same order. If that's not easy to do, please flag in the review
• Is every explicit property from the spec recorded + with a docstring?
• Are there implicit properties missing (e.g. scheme-level properties, like correctness of encryption)?
• Are there other reasonable properties / checks / invariants that are missing?
• Are there test vectors? If not, should there be?
• Does the documentation make sense?
• Are all parameter assumptions either enforced through a type-level constraint, enforced through a runtime check, or documented explicitly as an assumption the caller must enforce?
• Are all failure modes explicitly called out in the documentation? Especially ones that Cryptol cannot protect against (randomness sampling, system-level requirements)?
• Does the code make sense? Are there places an inline comment would be helpful? Are there places where it doesn't look how you expected, based on the spec?
• Are there any annoying formatting things that make it hard to understand the code?
• (If you have Haskell/Cryptol experience): Is there any non-standard formatting that stands out?
• Do names match the spec? If not in the spec explicitly, do they make sense? Do they match naming conventions?

General guidelines

• Feel free to be nitpicky / tend toward more questions on PRs! Specs need to be correct to be useful, so tiny-detail questions are worth asking, even if they don't seem important.
• Try loading each (concrete, non-parameterized) module and running :check-docstrings with the SMT solvers delivered in what4-solvers to make sure the tests will work. Eventually this will be part of CI.

Gold standard criteria

A gold standard specification has the following requirements:

• the specification is written in Literate Cryptol in either Markdown or LaTeX.
  • Markdown is used for specifications whose original format was ASCII, such as an IETF RFC.
  • LaTeX is used for specifications whose original format is anything else, such as a NIST FIPS standard written in Word.
  • Processing a Literate Cryptol file into a PDF should result in a document that resembles the original semi-formal specification; it need not be identical.
• Non-Literate versions of formal specifications should be either automatically derived from the Literate specifications (by eliding non-Cryptol contents through text processing) or can be hand-written. In the latter case, a traceable equivalence must be defined between key elements of both specifications (preferably at the core function level) and proven correct.
• The large-scale structure of the specification mirrors that of the original specification. E.g., modules reflect original specification Sections and conceptual structural features.
• The small-scale structure of the specification mirrors that of the original specification, particularly with the naming of constants, variables, data types, and functions, and their introduction order.
• Every canonical data type and functional specification mirrors that of the original semi-formal specification as closely as possible, even if the encoding is not canonical Cryptol or is inefficient.
• Introducing alternative data types, helper variables or functions, or function specifications in order to improve legibility, efficiency, or otherwise must be traceably related to the original canonical specifications, preferably through an equivalence property, and that property must be proven correct.
  • Justification for and explanations of alternative encodings of data types or functions, or explanations of complex formalizations, should be explained in consistent call-outs, such as indented *italicized* inline text or in a pop-out text box.
  • The alternative relation permitted in such specifications is a refinement property that preserves substitutability of the old form with the new. Usually this is accomplished through a covariant substitution refinement, a la Liskov.
• Every lemma/theory/property expressed in the original semi-formal specification must be captured in an equivalent Cryptol property.
• Every Cryptol property must be named in such a way and documented as to indicate whether it is meant to be proven or checked, and if checked, if it is exhaustive.
  • Docstrings are a great way to do this
  • Batching properties in assurance modules or icry files is permitted, especially if there is a need for a fast-fail on continuous verification.

Examples of "near golden" specifications include:

• the ChaCha20 and Poly1305, Salsa20, TripleDES, PRINCE, HKDF, MD5 specifications written in Markdown, and
• the Kyber, FALCON, and SPHINCS+ specifications written in Markdown and LaTeX.