Argon2 on x86-64: prove complete filling random-word dispatch

[reaperhulk]

Select the random word for an active filling cell using the reviewed Argon2d/i/id addressing predicate. Dependent addressing reads the previous cell's first word; independent addressing generates or reuses its specified address block and reads the indexed word.

Prove both paths return FillStep.random, retain the represented matrix and filling allocation, preserve callee-saved registers, permissions and MXCSR, and satisfy the scratch/counter memory frame. The resulting cache invariant remains valid for the next index. Prove the dispatcher and both sources have identical traces for equal public parameters, without equating secret matrix contents or random words.

Builds on #501. Inline implementation and proofs only; no specification, TCB, public API or generated assembly changes.

Validation: targeted Lean correctness and 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.