Correctness Proofs for SHA-3 (Part 2): Proofs for Portable Keccak-f1600 #1408
Open
karthikbhargavan wants to merge 14 commits into
Open
Correctness Proofs for SHA-3 (Part 2): Proofs for Portable Keccak-f1600 #1408karthikbhargavan wants to merge 14 commits into
karthikbhargavan wants to merge 14 commits into
Conversation
Adds a Hacspec specification of FIPS 202 (SHA-3 / SHAKE) under specs/sha3, with hax extraction to F* and verification of the four root modules (Hacspec_sha3, .Keccak_f, .Sha3, .Sponge). The spec compiles against hax-lib 0.3.6 and verifies at the default rlimit (no Proof_Utils dependency, no fstar! escape hatches): properties beyond well-typedness and bound checks are deferred to a follow-up that brings the implementation proofs. Adds the new crate to the specs/ sub-workspace. Spec authored by Karthik Bhargavan. Claude (Opus 4.7) was used to review and test the spec; it did not author the spec content.
The KeccakState helpers used 5*j+i but the rest of the impl (and the corresponding hacspec spec, see specs/sha3) treats the lane layout as 5*i+j. Aligns with FIPS 202 §3.1.2 lane indexing. Authored by Karthik Bhargavan with Claude (Opus 4.7) used to review and test.
Adds crates/algorithms/sha3/tests/cross_spec.rs comparing the public SHA-3/SHAKE API (including AVX2 x4 SHAKE256 and Neon x2 parallel variants) against hacspec_sha3 on boundary input sizes. Adds an embedded #[cfg(test)] mod cross_spec_tests in generic_keccak.rs that compares each permutation step (theta, rho, pi, chi, iota, keccakf1600) and the simd::portable load_block / load_last / store_block helpers against the spec. Exposes generic_keccak::constants as pub(crate) for the test mod. Adds hacspec_sha3 as a [dev-dependencies] entry in the sha3 crate's Cargo.toml. Tests authored by Karthik Bhargavan. Claude (Opus 4.7) was used to review and test.
The script’s rename helpers used `sed -i""` (no space) which is the GNU-sed in-place form. macOS’ system sed is BSD and parses it as `-i "" -e ...`, treating `-e` as the input filename and bombing the first rename step. Detect the OS at script start: use `gsed` (GNU sed via the Homebrew `gnu-sed` package) on Darwin; the system `sed` everywhere else (Linux’ system sed is already GNU sed). Both invocations route through a \$SED variable in the rename helpers. Authored by Karthikeyan Bhargavan with Claude (Opus 4.7) used to review and test.
The portable keccakf1600 equivalence proofs added in the next commits depend on hax-lib lemmas that today live only on cryspen/hax's `integer-lemmas` branch (a PR upstreaming them into hax main is in flight; we'll switch back to a tagged hax-lib release once it merges). Bumps the workspace dependency for hax-lib in Cargo.toml and adds a [patch.crates-io] entry so transitively-pulled hax-lib versions (via stale published libcrux crates pulled by hpke-rs dev-deps) also resolve to the fork; otherwise cargo metadata returns two hax-lib paths and confuses F*'s include resolution. Aligns specs/sha3/Cargo.toml's hax-lib pin with the workspace. Authored by Karthikeyan Bhargavan with Claude (Opus 4.7) used to review and test.
The replace block on `buf_to_slices` was a workaround for a hax extraction bug (cryspen/hax#1920): `core::array::from_fn` was extracted with an explicit type parameter that bypassed the typeclass-based implicit, breaking the F* signature. That bug is fixed in the cryspen/hax:integer-lemmas hax-lib bump landed in the previous commit (Core_models.Array.from_fn now refines its closure parameter to (i: usize{i <. v_N})). The Rust source can now extract directly via `core::array::from_fn` and F* discharges the indexing precondition without an escape hatch. Removing the replace block also closes a soundness gap: the replace described an F* function (Core_models.Array.from_fn) that, before the hax fix, had a different shape than what Rust actually called. Authored by Karthikeyan Bhargavan with Claude (Opus 4.7) used to review and test.
Adds [@@ "opaque_to_smt"] to the F*-side createi (via the existing fstar::replace block) plus a companion createi_lemma that gives the expected indexing property as an SMTPat. Without opacity, hax's extraction of `core::array::from_fn` allows Z3 to unfold createi's body recursively through array_from_fn's inner `Seq.index`/`ApplyTT` quantifier and trigger a cascade — verified at the load_block proof site (~195M instances of the inner anonymous quantifier in the queries-Libcrux_sha3.Simd.Arm64.fst.smt2 dump on the related sha3-proofs-focused worktree, 2026-05-05). Opacity collapses the cascade; the SMTPat lemma keeps the indexing property accessible to consumers via reveal_opaque. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three helper modules consumed by the portable keccakf1600 equivalence proofs (added in the next commit): - Proof_Utils.NatFold: lemmas about natural-number folds over ranges (e.g. lemma_fold_range_unroll, lemma_fold_range_is_nat). - Proof_Utils.FoldRange: a single step lemma for fold_range chunk decomposition. - Proof_Utils.Lemmas: thin wrappers around upstream hax-lib lemmas (logand_commutative, lemma_rotate_left_zero, lemma_index_update_at_range) from the cryspen/hax:integer-lemmas branch (an upstream PR is in flight to merge these into hax main). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
F* equivalence proofs that the libcrux-sha3 portable keccakf1600
permutation matches Hacspec_sha3.Keccak_f.keccak_f.
Modules:
- EquivImplSpec.Keccakf.ChiFold: per-position equality lemma chaining
the impl's chi unrolled form to the spec's chi_inner_val. Heaviest
query is lemma_chi_outer_unfolds_generic (~108s at fuel=6 ifuel=0
rlimit=800).
- EquivImplSpec.Keccakf.SpecRounds: spec-side iteration helper.
- EquivImplSpec.Keccakf.Generic: generic-over-T proof framework
(~72 lemmas, 2024 lines) — rho/theta/pi/chi extract-lane lemmas
and lemma_keccakf1600_to_spec.
- EquivImplSpec.Keccakf.Portable: instantiates Generic for the
scalar u64 portable lane impl.
Plus stubs/Spec.Utils.{fst,fsti} — a small workaround so the
shared Libcrux_intrinsics.Avx2_extract.fsti references resolve in
this proof set without pulling in libcrux-ml-kem's full Spec.Utils
(SHA-3 doesn't exercise those AVX2 intrinsics).
Plus a trimmed equivalence/Makefile with ROOTS limited to the
seven in-scope modules (Proof_Utils helpers + 4 keccakf modules).
Sponge-level and platform (Arm64, AVX2) equivalence proofs are
deferred to follow-up PRs.
Verifies cleanly from cold cache against cryspen/hax:integer-lemmas
(prove + equiv: ~9 minutes wall on a 12-thread laptop, JOBS=2;
distribution ~37% Generic / 27% ChiFold).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Three small comment fixes in the proof files added in this PR: - EquivImplSpec.Keccakf.Generic.fst: the "Admitted (library-level…)" block listed lemmas that are in fact proven (lemma_rotate_left_zero, logand_commutative via Proof_Utils.Lemmas; lemma_rho_offsets_values, lemma_keccakf1600_is_rounds, lemma_keccak_f_is_rounds via Proof_Utils + EquivImplSpec.Keccakf.SpecRounds). Reword to "discharged via Proof_Utils.Lemmas + EquivImplSpec.Keccakf.SpecRounds". - EquivImplSpec.Keccakf.Generic.fst: drop a sprint-internal datestamp on a Theta+Rho commutativity comment; keep the architectural note. - Proof_Utils.NatFold.fst: drop dangling references to [Libcrux_sha3.Proof_utils.Folds] and [Test_Norm_Plain] / [Test_Keccakf_NatFold] — those modules live only on the proof-focused branch and aren't part of PR-2. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds: - proofs/fstar/equivalence/README.md documenting the two PR-2 claims (panic-freedom for spec + impl; portable keccakf1600 ↔ spec correctness), the load-bearing theorems, scope, dependencies, and per-module timing. - proofs/fstar/equivalence/.hints/*.fst.hints (6 files, ~460KB total) recorded after a successful cold-cache build. Replay shrinks the build from ~7 min to seconds for re-verification (Generic dominates; ChiFold currently doesn't write a hint file, so its proof re-runs in ~2 min on every cold-cache invocation — F* idiosyncrasy with this proof; investigation deferred). - equivalence/Makefile: override HINT_DIR to point at the tracked .hints/ directory so checkouts pick up the shipped hints. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lifts the verification-status script from the proof-focused branch
into the SHA-3 crate. The script reads the F* extraction Makefile's
ADMIT_MODULES list plus per-function `#[hax_lib::fstar::*]`
annotations in the Rust source and produces a Markdown table
classifying each function at one of six tiers (lax / unverified /
panic-free / math / bounds / hacspec).
Files:
- proofs/generate_verification_status.sh — bash entry point.
- proofs/generate_verification_status.py — implementation
(~900 LoC; reusable across crates via a JSON config).
- proofs/verification_status.config.json — SHA-3 module map.
- proofs/verification_status.md — generated output
(regenerate after re-extraction with
`bash proofs/generate_verification_status.sh
--config proofs/verification_status.config.json --root .`).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
karthikbhargavan
changed the title
jschneider-bensch
added
the
waiting-on-review
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
2 participants
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.
This PR adds F* equivalence proofs that the portable implementation of the
keccakf1600permutationmatches its Rust specification
hacspec_sha3::keccak_f::keccak_f, and confirms panic-freedom forthe entire portable surface.
The full theorem statements, scope, dependencies, per-module timing, and build instructions live in
crates/algorithms/sha3/proofs/fstar/equivalence/README.md. PR readers should start there.Implementation <-> Spec correctness
We prove in F* that
Libcrux_sha3.Generic_keccak.impl_2__keccakf1600at (N=1, T=u64) is equal toHacspec_sha3.Keccak_f.keccak_fon every input. The main lemmas arelemma_keccakf1600_portable(inEquivImplSpec.Keccakf.Portable.fst) and the parametriclemma_keccakf1600_to_spec(inEquivImplSpec.Keccakf.Generic.fst). The parametric form is the reusable boundary: future Arm64 / AVX2PRs only need to populate a lane_correctness record at their respective (N, T) to inherit the equivalence.
Sponge-level (absorb / squeeze / XOF) equivalence, top-level digest API equivalence, and Arm64 / AVX2 backend equivalence are out of scope for this PR.
Dependencies
We use a branch of
hax-libwhich will be repointed to main when the corresponding PR is merges.Verification
The crate also ships
proofs/generate_verification_status.sh, which classifies every Rust function at one of six tiers (lax / unverified / panic-free / math / bounds / hacspec) and writes into a table atproofs/verification_status.md.Authorship
The F* proofs (
Proof_Utils.*, EquivImplSpec.Keccakf.*) were authored by Claude Opus 4.6 and 4.7 over many sessions,with guidance from Karthik Bhargavan on common F* pitfalls — opaque predicates and SMTPat hygiene, quantifier cascades, hax-lib workarounds, the panic-free / lax / equivalence ladder, and the smtprofiling workflow.