Argon2 on x86-64: prove complete active-cell filling step

[reaperhulk]

Compose the active-cell filling step on x86-64: reload the lane count, map the secret random word to the reviewed reference coordinates, reload the matrix base, compute current/previous/reference pointers, and run the verified compression and first/later-pass update.

Prove the complete step's result, memory frame, callee-saved registers, permissions and MXCSR from one matrix allocation invariant. Every matrix cell's bounds and separation follow from the parameter/position bounds. Prove equal traces when public layout and position agree and the permitted reference coordinates agree, without requiring equal random words. Factor the predecessor word arithmetic so both pointer proofs reuse it.

Builds on #495. This inline layer is ready for the matrix-state and nested-loop composition. No specification, TCB, public API or generated assembly changes.

Validation: targeted Lean correctness/trace builds, standard-axiom and compiler-override audits, specification-origin audit, Lean import/proof-speed checks, and git diff --check. Full checks run in CI.

[alex]

why are there 900 PRs for different parts of teh argon2 proof... there should be a single PR, per platform, adding the ASM and proofs required for it, not this fucking trash.

[reaperhulk]

Consolidated the implementation and proofs into #479, rebased onto current main, and closed the component PRs. #479 is now a draft until the complete x86-64 assembly, shared-contract proof, API, tests, and benchmarks are ready.