Argon2 on x86-64: prove filling columns and block addresses

[reaperhulk]

Compute the current filling column, its cyclic predecessor, and lane-major block pointers in baseline x86-64 code. The predecessor wraps to the last column at column zero. Reference coordinates may be secret: pointer arithmetic has a fixed trace, and the column branch depends only on public loop coordinates.

Prove the exact natural-number formulas, fault-free execution, memory and permission preservation, enclosing loop register preservation, and MXCSR preservation. Target-independent bounds establish that the current, previous and reference cells are in the matrix; cell_contains covers each complete 1024-byte block. Checked literals support later artifact checks.

This continues the whole-derive implementation above #479. These are inline helpers, with no new API, specification, TCB changes or emitted assembly. The filling operation and complete derive proof remain to be assembled.

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