Development

Start with lib/hpke.mli for the public contract and lib/hpke.ml for the implementation.

Set up

Use an initialized opam switch with 64-bit OCaml 4.14+ and Dune 3.12+.

git clone https://github.com/thevilledev/ocaml-hpke.git
cd ocaml-hpke
opam install . --deps-only --with-test --with-doc --with-dev-setup

Build and test

opam exec -- dune build @all @doc
opam exec -- dune runtest

Generated API documentation is in _build/default/_doc/_html/. Tests cover published vectors, supported suites and modes, error contracts, malformed inputs, and interruption. OCaml 5 also runs the domain concurrency test. Lean conformance vectors run as part of dune runtest.

Source map

lib/hpke.mli           public API and error contracts
lib/hpke.ml            KEMs, key schedules, contexts, single-shot API
lib/hpke_for_testing.* deterministic senders for vector tests
test/                  vectors, round trips, properties, error contracts
test/internal/         internal boundary checks
test/concurrency/      OCaml 5 domain contention
test/interrupt/        interruption checks
test/signals/          signal checks
fuzz/                  Crowbar targets for peer input
test-vectors/          pinned fixtures and provenance
tools/                 vector extractors and Go fixture generator
verification/          Lean proofs, TLA+ models, conformance tests
website/               static HTML documentation

Format and check metadata

opam exec -- dune fmt
opam lint hpke.opam

Formatting uses ocamlformat 0.29.0 with the conventional profile. CI requires formatting to leave no diff.

Run the fuzz smoke test

opam exec -- dune build --profile fuzz fuzz/fuzz_hpke.exe
opam exec -- _build/default/fuzz/fuzz_hpke.exe --repeat 1000 --seed 9180

Crowbar exercises key parsing, receiver setup, and ciphertext opening. The executable is built only under the fuzz profile.

Check the formal models

verification/check.sh

Requires elan with Lean 4.34.0, a JDK, and tla2tools.jar. See the verification guide for setup, coverage, and assumptions. Changes to modeled code also need updated mirrors and regenerated conformance vectors.

Reproduce deterministic vectors

hpke.for_testing lets a test choose a DHKEM sender's ephemeral private key:

Hpke_for_testing.setup_base_sender suite ~ephemeral ~recipient ~info

The other RFC modes have matching helpers. For ML-KEM and hybrids, Base/PSK helpers return Invalid_private_key and Auth/AuthPSK helpers return Unsupported_mode. Reproduce those KEMs' randomness through the ordinary API's ~rng, as in test/test_vectors.ml.

Never link hpke.for_testing outside tests. Sender ephemeral keys must be fresh and secret for each context.

Test vectors

Fixtures are pinned to immutable source commits. Record the standard revision and source commit when adding or changing them; see provenance and regeneration commands.

Continuous integration

CI builds and tests on Linux and macOS, checks declared dependency minimums, installs the package with tests and docs, checks formatting, and runs fuzz tests. The weekly fuzz run is longer. Exact versions and commands are in ci.yml.

Contribute

Back wire changes and new suites with a pinned vector from a standard or independent implementation.
Document public signatures, validation, and error behavior in hpke.mli.
Keep protocol changes in the module for their standard version.
Run the checks relevant to your change before opening a pull request.

Use issues for bugs and proposals, and private reports for vulnerabilities. Contributions use the ISC license.