Argon2 on x86-64: compose the complete block update proof

[reaperhulk]

Compose destination saving, scratch/output setup, the verified compression call, argument restoration and first/later-pass writing into a complete block update. Derive the intermediate operation invariants from the caller's readable frame fields, writable allocations and region separation.

Prove that saving the destination preserves both input blocks and the old matrix cell; that frame pass/scratch fields survive; and that the complete sequence writes G on pass zero or G XOR the old destination on later passes. Include the exact memory frame, enclosing-loop register and permission preservation, full MXCSR preservation, and trace equivalence when the allowed argument addresses and public frame words agree. Split the existing code into setup followed by operation to match the proof composition; instruction order is unchanged.

Builds on #484. This is still an inline filling layer; independent address generation, the pass loops, finalization and whole-derive registration follow. No specification, TCB or public API changes, and no assembly emitted yet.

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