Argon2 on x86-64: prove reference-window counts and starts - #466
Merged
Merged
Conversation
* 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>
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 reference blocks are selected from different chronological windows depending on the pass, slice, segment index and whether the reference is in the current lane. This adds internal x86-64 code and proofs for the two candidate counts, their selection, and the starting column of the window.
The selected count is proven equal to the reviewed
referenceCountspecification. The start is proven equal to the starting-column expression inreference. Branches depend on the public pass and slice; the same-lane test and zero-index adjustment use masks. The proofs cover termination, register preservation, memory preservation and execution-trace agreement, including agreement on the public starting-column result.Builds on the memory initialization and reference-index arithmetic merged in #456 and #457. Changes are confined to
Impl/andProof/; these helpers will be composed into the whole derive proof. Public APIs and emitted assembly are unchanged.Validation: targeted Lean builds of
ReferenceCount,ReferenceStartandReferenceStartCT; direct standard-axiom, compiler-override and specification-origin audits; Lean import and proof-speed checks, architecture gates, variant propagation andgit diff --check. CI runs the full repository checks.