Argon2 on x86-64: prove memory initialization and reference-index arithmetic - #456
Merged
Merged
Conversation
reaperhulk
force-pushed
the
argon2-memory-init
branch
from
October 1, 2026 13:57
151c3a1 to
f30c886
Compare
reaperhulk
enabled auto-merge
October 1, 2026 14:00
* Argon2 on x86-64: prove reference-window arithmetic * Argon2 on x86-64: prove fixed-time reference-lane selection --------- Co-authored-by: Paul Kehrer <161495+reaperhulk@users.noreply.github.com>
reaperhulk
force-pushed
the
argon2-memory-init
branch
from
October 1, 2026 14:03
5ffd329 to
19d8c62
Compare
reaperhulk
changed the title
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.
Argon2's x86-64 derivation can now initialize its entire memory matrix from H₀ using the supplied BLAKE2b backend. The code clears the allocation, then computes H′(1024, H₀ || LE32(column) || LE32(lane)) for columns zero and one of each lane. It works from arbitrary initial allocation contents and leaves all other cells zero, matching
Spec.Argon2.initMemory.The proofs establish termination and permitted memory accesses for both loops, correctness of every matrix cell against the reviewed spec, preservation of H₀ and enclosing-frame arguments, and bounded writes to the matrix, hash scratch, call stack and eight-byte column/lane suffix. Relational proofs establish the public trace of the complete initialization program, composing the allocation-clearing loop, parameter setup and all lanes through generic H′ calls. H₀ and incoming values in registers overwritten by setup may differ between runs; only public bases and dimensions determine the trace.
The reference-index layer merged from #457 adds fixed-time J₂ lane division, the squared J₁ relative-position mapping and chronological-window wraparound. Its proofs establish the reviewed natural-number formulas under the valid parameter bounds, unchanged memory and execution traces independent of secret numerators.
These are inline building blocks for the eventual derive artifact, following #440. It introduces no spec or TCB changes, independent helper API, emitted assembly or Rust cryptographic code. The complete derive
Verifiedcertificate still requires the memory filling, finalization and composition with the other derivation layers; this PR does not claim complete Argon2 verification. The final generic caller will supply the H′ symbol for each backend.Validation: targeted Lean builds of the complete memory-initialization trace and reference-index proofs after rebasing; direct standard-axiom, compiler-override and spec-origin audits; Lean imports/speed, vector provenance, architecture-gate and variant checks; Rust formatting/clippy and normal/baseline Wycheproof test suites. Earlier versions of both layers passed full local Lean builds and emitter checks; CI runs those checks on the current combined PR. No architecture support or public API changes, so no algorithm-table or benchmark changes.