[reaperhulk]

ARMv7 SM4-CBC decryption called the full ECB entry point for every block, preparing the same round-key table repeatedly and using one of eight cipher lanes. Prepare the decryption keys once, decrypt up to eight ciphertext blocks independently, then XOR with preceding ciphertext in reverse order before it is overwritten. Save the last ciphertext for the continuation IV.

Enable the generated ARM/Thumb implementation with complete functional and constant-time proofs against the unchanged shared CBC decryption contract. The proofs cover arbitrary lengths, empty input, partial final batches, continuation IVs, memory frames, and ABI preservation. The verified stack wrapper wipes all 1512 bytes of working space; stack use falls from 1560 to 1520 bytes. Encryption retains its existing serial implementation. No specification or TCB changes.

The Thumb hot round loop is placed on a four-byte boundary with a self move whose identity is verified, following the measured placement improvement in #3033. Local disassembly confirms the aligned loop at function offset 0x76c in a section with four-byte alignment.

Validation: full Lean build (22423 jobs), scoped emitter generation/audits and generated-code check; public-import checks on all 13 changed modules; static import/module/registration/proof-speed, algorithm-table, architecture/variant and MCDT checks; CBC integration tests, ARM/Thumb library compilation, ARM Clippy and Rustfmt. Existing tests compare to ECB, exercise the published vectors, chaining and invalid lengths. Full CI passed, including native ARM/Thumb tests, Lean, emitter audits and static checks.

Rebased onto main after #3033/#3036/#3037 merged. This diff contains only CBC decryption changes.

Native AArch32 benchmark, paired against the parent on Neoverse N2, OpenSSL enabled. Times in microseconds; lower is better:

Bytes	ARM parent	ARM new	OpenSSL	Thumb parent	Thumb new	OpenSSL
64	4.96	2.04	1.42	5.14	2.05	1.42
1024	63.42	7.87	8.45	66.49	7.90	8.46
16384	998.70	107.39	121.04	~1050	107.89	121.01

Bulk decryption is approximately 9.3–9.7 times as fast as the parent and 11% faster than OpenSSL. The 64-byte case remains slower than OpenSSL. CBC encryption is unchanged and remains about 7.8 times slower at 16 KiB; this PR makes no encryption speed claim.

CI after rebasing onto main passed.

Rebased again after CBC encryption (#3040) merged, resolving the shared registration and documentation. Full Lean build (22449 jobs), emitter audits/check, public-import checks, ARM/Thumb compilation, Rustfmt and ARM Clippy pass. The generated decryption function is byte-for-byte identical to the benchmarked version; no unchanged-code benchmark rerun was needed.