Implement verified Argon2 on x86-64

[reaperhulk]

Implements Argon2d, Argon2i, and Argon2id version 1.3 on x86-64 against the merged specification and ISA models. The public argon2::derive API supports passwords, salts, secrets, associated data, memory and iteration costs, lanes, worker limits, and variable-length output. Rust validates parameters and allocates memory; the entire derivation runs in Lean-generated assembly. Lanes are evaluated serially.

The complete entry point is proven Verified against Spec.Argon2.deriveContract, including H₀, initialization, every filling pass, final reduction and H′, memory framing, termination, ABI preservation, and the shared contract’s exact leakage policy. Argon2i leaks no input contents; Argon2d/id permit precisely the specified flattened reference-index log. The implementation is generic over the BLAKE2b backend, so future variants propagate through H′ and the whole derivation.

This consolidates the implementation and proof stack into one complete platform PR. There are no changes to Spec/ or TCB/, no unverified proof shortcuts or resource-limit overrides, and no manually written assembly. Stack arguments remain read-only; normalized copies live in the verified private frame.

Validation:

• Targeted complete-derivation, registration, and Argon2 golden-test builds pass, including standard-axiom, compiler-override, and spec-origin audits.
• The repository-wide emitter check passed for the completed implementation before the latest main update. After this rebase, the Argon2 registration build and scoped emitter check pass; unrelated full checks are left to CI.
• The Rust suite passes with Wycheproof; RFC 9106 vectors cover all three variants, and 360 cases match OpenSSL across costs, lanes, output lengths, empty inputs, secrets, and associated data. Baseline CPU-feature tests pass.
• New Rust API and RFC test code have 100% line coverage. Formatting and clippy pass, as do import, proof-speed, vector provenance, architecture gate, variant propagation, MCDT, and algorithm-table checks.
• End-to-end benchmarks cover all three variants at 1 MiB and 16 MiB. The runners use OpenSSL 3.0, which predates Argon2, so they benchmark this library alone. On OpenSSL 3.2+ hosts, cargo bench --manifest-path bench/Cargo.toml --features openssl-argon2 enables the comparison and cargo test --manifest-path bench/Cargo.toml --features openssl-argon2 --test argon2 runs the differential tests. Benchmark smoke tests and clippy also pass against the runners’ exact OpenSSL 3.0.13 version.

Rebased onto main at ac71ac2a; the complete Argon2 registration build and scoped emitter audits pass after the rebase, and generated Argon2 assembly remains unchanged.