[reaperhulk]

ARMv7 SM4-CFB128 encryption called the full ECB entry point for each feedback block, preparing the same round keys repeatedly. Prepare the bitsliced keys once per call and reuse them along the serial ciphertext feedback chain.

The generated ARM/Thumb implementation has complete functional and constant-time proofs against the unchanged shared encryption contract, including empty input, arbitrary block counts, 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. Decryption keeps the batched implementation from #3033. No specification or TCB changes.

Validation: full Lean build (22419 jobs), scoped emitter generation/audits and generated-code checks, public-import checks for all nine changed modules, static checks, CFB integration tests, ARM/Thumb assembly compilation, ARM Clippy and Rustfmt. Native ARM/Thumb benchmark passed; Full CI passed, including native ARM/Thumb tests, Lean, emitter audits and static checks.

Stacked on #3033 for the prepared-key and workspace proof helpers. This PR's diff contains only serial CFB encryption changes. The serial cipher still computes eight lanes per feedback block; this change removes repeated key preparation and does not claim to close the entire OpenSSL gap.

Local Thumb disassembly confirms the hot round loop is word-aligned at function offset 0x780; the alignment padding is a verified identity.

CFB encryption timings in microseconds, paired against the parent on Neoverse N2 (lower is better):

Bytes	ARM parent	ARM new	OpenSSL	Thumb parent	Thumb new	OpenSSL
64	4.96	4.45	1.35	4.99	4.49	1.35
1024	63.36	52.71	8.84	64.04	52.75	8.83
16384	997.68	824.38	128.98	~1010	824.61	128.99

Bulk encryption improves by 17.4% on ARM and 18.3% on Thumb, but remains 6.4 times slower than OpenSSL. Decryption is unchanged in the paired benchmark and still beats OpenSSL at 1 KiB and 16 KiB.

[reaperhulk]

The implementation is already included in main as 324009e (matching stable patch ID). Closing this superseded PR; final S-box integration is tracked in #3035.