Vectorize x86-64 RC2 mashing schedule scans with SSE2

[reaperhulk]

RC2-CBC block processing currently scans the 64-word key schedule one scalar candidate at a time during each mashing lookup. This replaces those scans with baseline SSE2 operations that select eight schedule words per vector, while retaining the fixed traversal of every candidate.

The existing RC2 block and CBC contracts, public API, dispatch, and scratch sizes are unchanged. Each lookup temporarily uses a fixed 16-byte slot in the existing scratch buffer and restores its original contents. The proof establishes the exact schedule selection and unchanged memory, then composes it into the existing block and CBC verification. No Spec/ or TCB/ changes.

This follows the key-expansion vector scan in #462. OpenSSL and AWS-LC instead perform secret-indexed schedule loads in their mashing rounds; those accesses cannot be copied here. Primary upstream references: OpenSSL RC2 rounds, AWS-LC RC2.

Two alternating baseline/candidate pairs on an Intel Xeon E5-2696 v4 (Broadwell), pinned to core 2, using the normal public API with VG_CPU_FEATURES=none, 30 samples, 0.5-second warmup and 1-second measurement per workload. Baseline is #462. Times include initialization, update, finalization, and wiping.

Operation	Size	Baseline runs 1 / 2	Candidate runs 1 / 2	Lower time
Encrypt	64 B	17.464 / 17.611 µs	14.517 / 14.539 µs	16.9–17.4%
Decrypt	64 B	16.831 / 16.957 µs	13.792 / 13.771 µs	18.1–18.8%
Encrypt	1 KiB	98.663 / 99.854 µs	53.210 / 53.541 µs	46.1–46.4%
Decrypt	1 KiB	90.261 / 89.286 µs	40.269 / 40.074 µs	55.1–55.4%
Encrypt	16 KiB	1402.6 / 1408.4 µs	678.47 / 673.04 µs	51.6–52.2%
Decrypt	16 KiB	1259.3 / 1250.4 µs	463.17 / 464.23 µs	62.9–63.2%

Team builds and other benchmarks were excluded by locks. An unrelated Lean build outside those locks was present on the host; absolute times are higher than earlier samples, but the two alternating comparisons agree closely. These local results do not establish CI performance.

Validation: full lake build (5,542 jobs), emitter generation and --check including artifact audits; all required Python checks; Cargo formatting and Clippy for library/tests and benchmarks; complete Wycheproof tests both normally and with VG_CPU_FEATURES=none through cpu-features-env. The rebase onto #462's current CI-fixed head leaves all RC2 implementation/proof/generated code unchanged and is checked with the RC2 artifact target. No resource limits or proof shortcuts were added.

Benchmark dependency metadata now includes the generated rc2 module alongside rc2_cbc, so RC2-only changes select these benchmarks.

The ARM benchmark container also uses a fresh RUSTUP_HOME, matching the merged CI fix in #458. Its first run failed while rustup removed a stale image component; this one-line repair is shared with #460 and changes no cryptographic code.