[alex]

Part of #991.

What

Three changes to AArch64 SHA-256, each doing the same work in fewer instructions.

1. Compression keeps the block's original state in registers. vg_sha256_compress_sha2, which SHA-224, HMAC, HKDF and PBKDF2 call, no longer stores the state and reloads it after every block for the feed-forward:

• Each block copies its starting state to v30 and v31 (two movs). The feed-forward adds them, and the state is stored once, after the last block.
• v30 and v31 held the constants of the last two groups of rounds. Those groups now load their constants straight into v3, the register the constants and schedule words are summed into, from the table already addressed by x4.
• Per later block, 2 ldr q + 2 str q of the state become 2 constant ldr qs (off the SHA256H/H2 chain) and 2 movs.

This is aws-lc's sha256_block_armv8 arrangement of the state (v18/v19 there), with our constants still kept in registers between blocks.

2. The digest is written 16 bytes at a time (out256): ldr q, rev32, str q of v0/v1. That's 6 instructions in place of out32 8 true's 24 (ldr w, rev, str w per word). It applies to SHA-256's finalize and one-shot digest, and so to HMAC-SHA-256's, PBKDF2-HMAC-SHA-256's and RSA-PSS-SHA-256's copies of them. SHA-224's 28-byte digest keeps out32 7 true.

3. The initial hash value comes from a table (initQ): adrp/add, two ldrqTbl and two str q, 6 instructions. It replaces 24 for vg_sha256_init/vg_sha224_init (movz, movk, str w per word) and 18 for the one-shot digests (movz/movk into pairs, stp). The tables are VG_SHA256_H0 and VG_SHA224_H0 in consts.rs.

Generated files (all under src/asm/aarch64/):

• sha256.rs
• consts.rs: the two tables
• hmac_sha224.rs, hmac_sha256.rs
• pbkdf2_sha224.rs, pbkdf2_sha256.rs
• rsa_pss_sha224_mgf1_sha224.rs, rsa_pss_sha256_mgf1_sha256.rs

No TCB/ or Spec/ changes.

Proof

• Proof/Sha256/AArch64/Sha2/Compress.lean:
  • VInv is the new loop invariant: the state is carried in v0/v1, and the memory is unchanged until the final store (final_ok).
  • save_ok and fold_ok cover the copy and the feed-forward.
  • rounds4_ok handles both kinds of group: constants from kreg (sum4_ok), or loaded into v3 (exec_kldTo).
  • The round invariant keeps x4 at the table in every block, the constant registers of the first 14 groups (kKept), and v30/v31.
• Proof/Sha256/AArch64/Stream/Out.lean: out256_ok, with the same postcondition as out32_ok (n := 8) true. The two 16-byte stores of the byte-reversed loads are the eight words' big-endian bytes (write_digest). Stream/Md.lean's shape uses it, and so does everything built on that shape: finalize, HMAC, PBKDF2 and the one-shot digests.
• Proof/Sha256/AArch64/Stream/Init.lean: initQ_correct. ldrqTbl loads the table's pairs of words, which are the hash value's vectors (append_pairs), and two 16-byte stores write the state (write_iv). Stream/InitPairs.lean gives the one-shot digests their facts about initQ.
• The timing proofs (taint_decide) of init, finalize, the one-shot digests, HMAC and PBKDF2 are unchanged and accept the new code.

Performance

Benchmarks run 39098479382, against the merge base 50b726fe. Its scope is aarch64 (Neoverse N2), cpu_features='-', modules=sha256, which ran every benchmark that uses SHA-256. The hash, HMAC and PBKDF2 groups take the fastest of 8 binary copies each.

Benchmark	Base	Head	Change
sha256/64	76 ns	72 ns	−5.9%
sha256/1024	523 ns	519 ns	−0.8%
sha256/16384	7.67 µs	7.66 µs	−0.1%
sha224/64 / 1024 / 16384			−0.4% / −0.5% / −0.7%
hmac-sha256/64 / 1024 / 16384	209 / 656 ns / 7.80 µs	204 / 651 ns / 7.79 µs	−2.3% / −0.7% / −0.1%
hmac-sha256-verify/64	233 ns	229 ns	−1.6%
pbkdf2-hmac-sha256/*			−0.6% to −1.0%
pbkdf2-hmac-sha224/*			−1.5% to −1.7%
ecdsa_p256_sha256_sign/*			−0.4% to −0.7%

Other rows: every other row (RSA-OAEP/PSS/PKCS#1, ECDSA over other curves and hashes, scrypt, EC public keys) is between 0.6% faster and 0.5% slower. The slowest is ecdsa_p192_sha256_verify at +0.5%; P-192's own code is unchanged, and it hashes a message with the faster SHA-256. No row is slower by more than 0.7%.

Where the gain is: it is per call (digest output, initial value and the first block's state stores), not in the block loop. 16 KiB moves by 0.1%, inside the copies' spread.

Tests

lake build, Emit.lean --check and the ci/check_*.py scripts pass. These tests pass under qemu (-cpu max), both by default and with VG_CPU_FEATURES=none (cargo test --release --target aarch64-unknown-linux-gnu):

• SHA-2, HMAC, HKDF, PBKDF2 and RSA-PSS;
• P-256, by default only.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw