ProVerif analysis of the v1 ML-KEM Braid (hax Rust→ProVerif) + proof-status docs - #4
Draft
karthikbhargavan wants to merge 7 commits into
Draft
ProVerif analysis of the v1 ML-KEM Braid (hax Rust→ProVerif) + proof-status docs#4karthikbhargavan wants to merge 7 commits into
karthikbhargavan wants to merge 7 commits into
Conversation
…ng refactors cfg(hax_backend_proverif)-gated pv_extern/replace_body annotations mapping each crypto leaf onto the symbolic model, plus the behaviour-preserving refactors they require (Authenticator::update made consuming; struct-literal field order; rng threading). Inert in normal builds (52 tests pass).
handwritten/ reference (spqr-cka, spqr-dr, cryptolib); extraction/lib.pvl compiled from src/v1/unchunked by hax's ProVerif backend, rooted at the state-machine entry points; extraction-model/ composition (symbolic crypto, ping-pong + fixed-compromise process model, per-property queries with sound nounif + EXPECTPV blocks).
hax.py {setup,extract-proverif,verify-proverif,check-proverif} is the sole driver; setup-hax.sh builds the pinned backend (Rust-only); proverif.yml verifies per-push and re-extracts + drift-checks nightly.
proofs/PROOF_STATUS.md is the single source for what is proven + the trust boundary (F* panic-freedom + GF(2^16) correctness modulo a documented assume/admit boundary; ProVerif CKA security with the honest forward-secrecy / post-compromise nuance). Per-tool REPRODUCING guides; README defers to them. Corrects the earlier flat FS/PCS and 'panic-free and correct' claims.
…nt extraction)
The rust ProVerif engine delegates its import phase to the OCaml hax-engine, located via $HAX_ENGINE_BINARY (else a bare 'hax-engine' PATH lookup). The shell's active opam switch usually ships a mismatched hax-engine build -> the import panics ('ocaml engine crashed'). _proverif_env now resolves the matching engine from the hax-proverif switch (override via $HAX_OPAM_SWITCH / $HAX_ENGINE_BINARY), so extract-proverif works regardless of the active switch. Verified byte-reproducible under the default switch.
…ment the switch requirement Extraction runs its import phase through the OCaml hax-engine, so the rust-only build was insufficient. setup-hax.sh now creates the hax-proverif switch and builds+installs the matching OCaml engine (opam pin engine/) — inlined, because hax's setup-local.sh is an untracked local convention NOT in the committed hax tree, so a fresh clone wouldn't have it. Same latent bug fixed in the proverif.yml nightly extract job (it also called ./hax-engine/setup-local.sh). REPRODUCING.md: corrected the 'no OCaml/opam' claim, added the OCaml-engine toolchain row (needs opam/node/jq), documented hax.py auto-resolving the engine (override via $HAX_OPAM_SWITCH / $HAX_ENGINE_BINARY).
karthikbhargavan
force-pushed
the
spqr-proverif-backend
branch
from
July 13, 2026 12:51
47a1c0d to
0694785
Compare
The doc quoted an expected SHA-256 of 51b54eed55ee23d19386f7a62fb68dbf3a25ef80d5567c77f86e1c8d20f6395b, but the real digest of the committed extraction/lib.pvl -- and the value in extraction/lib.pvl.sha256 -- is 4914798cd53878dec1b3f43a00dad9d322013cd0cc09f14e7634e6366c70572c. The prose copy had gone stale. Nothing was actually wrong with the extraction: the L2 recipe checks the .sha256 file, not the doc, so it kept passing. But anyone eyeballing REPRODUCING.md would conclude the extraction had drifted when it had not -- which is a bad failure mode for a document whose whole job is to certify byte-identity. Point at extraction/lib.pvl.sha256 instead of restating the value. That file is regenerated alongside lib.pvl, so it cannot drift, and it is what `shasum -c` already verifies. Repeating the digest next to the file that holds it is what caused this, so the fix removes the duplication rather than refreshing it.
karthikbhargavan
force-pushed
the
spqr-proverif-backend
branch
from
September 2, 2026 14:47
fd0bfdf to
e4ed860
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What this adds
Machine-checked ProVerif analysis of the SPQR public ratchet (the v1 ML-KEM Braid
continuous key agreement), with the protocol model compiled from the Rust source by
hax's ProVerif backend rather than hand-transcribed,
plus a unified F*/ProVerif proof-status doc set.
Draft: the ProVerif extraction depends on the hax ProVerif backend (cryspen/hax
proverif-rust-backend, upstream draft PR #2068);CI builds it via
proofs/proverif/setup-hax.shat the pinned commit.Commits (reviewable chunks)
cfg(hax_backend_proverif)-gatedpv_extern/replace_bodyon the crypto leaves + the behaviour-preserving refactors they need.Inert in normal builds (52 tests pass).
spqr-cka/spqr-dr) + thehax-extracted
extraction/lib.pvl(rooted at the state-machine entry points) + thecomposition (symbolic crypto, compromise model, per-property queries with sound
nounif+EXPECTPVblocks).hax.py {setup,extract-proverif,verify-proverif, check-proverif}as the sole driver +setup-hax.sh+ a two-tierproverif.yml(verify per-push, re-extract + drift-check nightly).
proofs/PROOF_STATUS.md(single source for what's proven + the trustboundary) + per-tool
REPRODUCING.mds; README defers to them.What is proven (see
proofs/PROOF_STATUS.md)secrecy, and mutual authentication for the CKA. Post-compromise healing holds against
a KEM-key compromise but not an authenticator compromise (a MAC-chain property,
shared with the hand-written model) — documented honestly rather than claimed flatly.
correctness, modulo a documented assume/admit trust boundary (ML-KEM is trusted as an
interface).
Note on wording
The docs correct two earlier over-broad claims: flat "post-compromise security" → the
FS-yes / PCS-partial nuance above; and "proved panic-free and correct" →
panic-freedom modulo the documented trust boundary. No code behaviour changes.
Not included here
An experimental Aeneas-backend ProVerif + Lean driver (
hax-aeneas.py) reproduces thesame ProVerif verdicts via an independent toolchain (charon → aeneas Pure-IR →
proverif-from-pure); it lives on its own branch (needs external aeneas tooling, notCI-runnable).
AI assisted.