[atiernan]

Stacked on #13. This is the first shipped cryptography: a new crate, clazel-crypto, that instantiates clazel-tls's provider traits with libcrux. clazel-tls itself stays parameterised and free of axioms.

Commits

• 329172b contracts: src/spec.rs holds uninterpreted spec functions for SHA-256, HMAC-SHA256, HKDF-SHA256, ChaCha20-Poly1305 and X25519. src/axioms.rs is the trust boundary: one external_body wrapper per libcrux call, each with an // AXIOM: that states only libcrux's documented input and output types, plus one proof axiom for the 16-octet tag length. That makes 9 axioms. Inputs over u32::MAX, which libcrux refuses or panics on, abort the process instead of returning a value no axiom covers. The commit also adds the docs/DEPENDENCIES.md rows.
• ba1a820 adapters and tests: src/provider.rs implements schedule::crypto::Crypto, traffic::provider::{Factory, KeyedAead} with record::Aead, and hello::key_exchange::KeyExchange, all checked by Verus against the traits' contracts. The 32-octet AEAD key is a type invariant. tests/known_answers.rs runs the standards' own vectors through the traits:
  • FIPS 180-2 B.1 (SHA-256);
  • RFC 4231 §4.2–4.3 (HMAC-SHA256);
  • RFC 5869 A.1 and A.3 (HKDF-SHA256);
  • RFC 8439 §2.8.2 (ChaCha20-Poly1305), with tampered ciphertext, tag and additional data;
  • RFC 7748 §6.1 (X25519), and refusal of an all-zero shared secret.

Dependencies (decided 2026-10-26)

• Compiled into the browser:
  • libcrux verified-hacl crates with no unsafe: libcrux-sha2, -hmac, -hkdf, -chacha20poly1305, -poly1305 and -curve25519, all at exact 0.0.x versions;
  • their pre-verification support crates: libcrux-hacl-rs, -traits, -secrets and -macros, the last compile-time only;
  • rand and rand_core, which libcrux-traits requires but we never call.
• Compiled but never called: libcrux-hmac 0.0.9 has a mandatory dependency on libcrux-sha3 (pre-verification) for its HMAC-SHA3 types. That brings in libcrux-intrinsics (193 unsafe mentions) and libcrux-platform. Our HMAC-SHA256 path calls only libcrux-sha2. Alex chose libcrux's verified HMAC and HKDF over writing our own, since HACL* proves the timing independence that our own code would lack. Their rows say so.
• 50 rows locked but never compiled: packages reached only under cfg(hax) or cfg(valgrind_ct_test), which our builds never set.
• 19 existing rows raised to shipped, because libcrux now reaches them through normal dependency edges; each row says whether that use is compiled. The libc row also notes libcrux-platform.

Local results

• Verus on clazel-crypto: 13 verified, 0 errors, fresh run.
• cargo test -p clazel-crypto: 8 passed, 0 failed.
• Strict clippy and cargo fmt --check are clean. cargo xtask check reported STATIC CHECKS PASSED with 9 documented axioms.
• No full verify has run. The crate is at tier = 0 and target-tier = 0, since it parses nothing.

Needs, before it lands

• A review of src/axioms.rs by a different session Done, twice. Neither reviewer wrote the code, and both read it against the pinned libcrux sources.
  • The first review, of f6f7249e…d508, found that hkdf_expand could panic on an info within 33 octets of u32::MAX, and that the input cap sat past HACL*'s preconditions. Both are fixed in a335ece.
  • The second review, of c05d4642…42e3 (the current file), found all 9 axioms sound and every finding fixed. Its wording notes are fixed in 51e67fd, which leaves axioms.rs unchanged.
  • Caveat: the HACL* F* preconditions behind MAX_INPUT were recalled, not read, because the pinned crates ship only the extracted Rust.
• Not in this PR:
  • signature verification (ECDSA P-256, RSA-PSS and Ed25519 from libcrux, and RSA PKCS#1 v1.5 from clazel-pkcs1), which comes with path validation;
  • the README's safe-Rust line, which phase-3.md 3.0 says 3.5f updates (VERIFICATION.md's TCB line is now updated, in a335ece and 51e67fd);
  • the timing-safe finished_equal.

🤖 Generated with Claude Code