File Structure for Auditing KBB2017
-----------------------------------

*Security Engineers and Auditors: Everything that says "Unmodified" is a verbatim copy of the Prosecco source code. The git commit and authenticated timestamps are available in <diskuv-communicator-models>/dirsp-exchange/dirsp_exchange.mli*.

``kobeissi_bhargavan_blanchet.ml``
    **Auto-generated**. This is a ProScript-to-OCaml translation of ``proscript-messaging/ps/sp.js`` (aka KBB2017).
    Generated from the dirsp-ps2ocaml.exe program, with auto-formatting by ocamlformat.

``kobeissi_bhargavan_blanchet_intf.ml``
    **New content**. OCaml interface for ``proscript-messaging/ps/sp.js``, plus a few shims for functions that could
    not be machine translated.

``proscript-messaging/*.rst``
    **New content**. The documentation you are reading now.

``proscript-messaging/pscl/pscl.js``
    **Unmodified**. Javascript implementation of the ProScript Cryptography Library. This has implementations
    of SHA256 and other core security primitives.

``proscript-messaging/pscl/dirsp_Dirsp_proscript_intf.ml``
    **New content**. OCaml interface for the ProScript runtime. This is an OCaml reimagining of the
    Javascript API implicit in ``pscl.js``.

``proscript-messaging/pscl/dirsp_proscript.mli``
    **New content**. Just includes the ``Dirsp_proscript_intf.ml``. This is a way to share the same interfaces
    for external use (you!) and internal library use.

``proscript-messaging/pscl/dirsp_proscript.ml``
    **New content**. A hand-written OCaml implementation of the ProScript runtime. It mimics ``pscl.js``.

``proscript-messaging/ps/sp.js``
    **Unmodified**. ProScript implementation of what the Prosecco team calls the version 3 of the
    "Signal Protocol" (X3DH and Double Ratchet). We call it KBB2017.

``proscript-messaging/ps2pv/LICENSE``
    **Unmodified**. License file from the proscript-messaging team

``proscript-messaging/ps2pv/globals.ml``
    **Unmodified**. Global variables and common utility functions.

``proscript-messaging/ps2pv/lexer.ml``
    **Unmodified**. Lexical instructions for how to create tokens (ex. ``BOOL``, ``FUNCTION``, ``FINALLY``, ``IF``) from the ProScript dialect of JavaScript.

``proscript-messaging/ps2pv/ast.ml``
    **Unmodified**. The abstract syntax tree of ProScript. The tree contains the relevant details of ProScript that are necessary
    for recreating a proof with the author's ProVerif tool; it is **not** a perfect representation of ProScript. So we need
    to replace the lossiness (like losing arrays of hexadecimal constants).

``proscript-messaging/ps2pv/parser.mly``
    **Unmodified**. Instructions for how to produce the AST from the lexer.

``proscript-messaging/ps2pv/pretty.ml``
    **Unmodified**. Pretty-printer of the AST.

``proscript-messaging/ps2pv/_tags``
    **Unmodified**. Build instructions for the legacy ``ocamlbuild`` tool. It allows for building a legacy syntax and parser
    generators for OCaml called ``camlp4``, which is difficult to build with modern OCaml tooling.

``proscript-messaging/ps2pv/lexerror.ml``
    **New content**. Error utility functions to report lexical information (line and column) when there is an error.
    Similar to the Prosecco team's ``error.ml`` file, which is not included in this distribution.

``proscript-messaging/ps2pv/ast2ocaml.ml`` ``proscript-messaging/ps2pv/astpredicates.ml``
    **New content**. Translates the AST into OCaml source code.
    Similar to the Prosecco team's ``pretty.ml`` file; both of which walk the AST.

``proscript-messaging/ps2pv/ast2ocaml_tests.ml``
    **New content**. Tests for ``ast2ocaml.ml`` (ex. overflow/underflow compliance).

``proscript-messaging/ps2pv/dirsp_ps2ocamlcore.ml``
    **New content**. Parses source code into AST and translates via ``ast2ocaml.ml`` into OCaml.

``proscript-messaging/ps2pv/dirsp_ps2ocaml.ml``
    **New content**. A command-line driver. When you run ``dirsp-ps2ocaml.exe`` you are running this.

``proscript-messaging/.gitignore``
    **New content**. Which files are ignored for git

``proscript-messaging/.ocamlformat``, ``proscript-messaging/.ocamlformat-ignore``
    **New content**. Formatting instructions for new content.

``proscript-messaging/debug-parsing.mlt``
    **New content**. Instructions for ``utop`` to quickly begin a debug session.