Argon2 on x86-64: prove filling pointers and block writes

[reaperhulk]

Prepare the current, previous and reference matrix pointers from the filling loop coordinates and the verified reference mapping. Preserve the loop registers and retain the current pointer across the remaining setup. Reference coordinates can be secret without affecting the setup trace.

Add the block write step: pass zero copies the temporary compression result, and later passes XOR it with the previous contents of the current matrix cell. Prove every word and compose the complete block by induction. The proof preserves unread destination words, source contents, memory outside the destination, loop registers, permissions and MXCSR. The write trace depends only on public pointers and pass number.

This continues whole-derive implementation above #480. The helpers remain inline, with no new APIs, specification, TCB changes or emitted assembly. Compression-call composition and the filling loops follow in subsequent implementation work.

Validation: targeted Lean builds of the changed proof modules and checked literals; standard-axiom, compiler-override and specification-origin audits; Lean import and proof-speed checks; git diff --check. Full checks run in CI.