Argon2 on x86-64: prove compression calls and block updates

[reaperhulk]

Call the verified Argon2 G primitive using the previous and reference block pointers, then write its temporary result into the current matrix cell. Pass zero copies G; later passes XOR G with the old cell. The temporary output follows the first 4096 bytes of scratch, and a frame slot retains the destination across the call.

Prove the compression-call boundary, including narrowed permissions, return-address handling, input preservation, calling-convention obligations and its memory frame. Compose the call, restored arguments and full block write under explicit frame and destination separation invariants. Prove the combined result, memory safety, register/permission preservation, full MXCSR preservation, and equal traces when permitted argument addresses and public frame words agree. Add a permission-widening wrapper so the block write works inside the larger matrix allocation.

This continues whole-derive implementation above #483. The save/setup/reload blocks are individually proven; composition of their invariants with the filling loops follows next. No new public API, specification, TCB changes or emitted assembly.

Validation: targeted Lean builds of 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.