aarch64 SHA-256 on the SHA-2 instructions is proven

.gitignore

@@ -17,7 +17,6 @@ proofs/Rind/Aarch64/ChaCha20.lean
 proofs/Rind/Aarch64/Blockwise.lean
 proofs/Rind/Aarch64/Sha.lean
 proofs/Rind/Aarch64/Hmac.lean
-proofs/Rind/Aarch64/HashAxioms.lean
 proofs/Rind/Aarch64/SignatureDispatch.lean
 proofs/Rind/Aarch64/Ed25519.lean
 proofs/Rind/Aarch64/HmacDispatch.lean

ALGORITHMS.md

@@ -253,9 +253,9 @@ not cover rind's in-place calls.
 | `bignum_neg_p256` | `bignum_neg_p256`: none | `bignum_neg_p256`: none |
 | `bignum_neg_p384` | `bignum_neg_p384`: `BIGNUM_NEG_P384_SUBROUTINE_SAFE` | `bignum_neg_p384`: `BIGNUM_NEG_P384_SUBROUTINE_SAFE` |
 | `bignum_neg_p521` | `bignum_neg_p521`: `BIGNUM_NEG_P521_SUBROUTINE_SAFE` | `bignum_neg_p521`: `BIGNUM_NEG_P521_SUBROUTINE_SAFE` |
-| `bignum_negmodinv` | `bignum_negmodinv`: none | `bignum_negmodinv`: none |
+| `bignum_negmodinv` | `bignum_negmodinv`: none | not imported |
 | `bignum_optsub` | `bignum_optsub`: none | `bignum_optsub`: `BIGNUM_OPTSUB_SUBROUTINE_SAFE` |
-| `bignum_sqr_p521` | `bignum_sqr_p521`: `BIGNUM_SQR_P521_SUBROUTINE_SAFE` | `bignum_sqr_p521_alt`: `BIGNUM_SQR_P521_ALT_SUBROUTINE_SAFE` |
+| `bignum_sqr_p521` | `bignum_sqr_p521`: `BIGNUM_SQR_P521_SUBROUTINE_SAFE` | not imported |
 | `bignum_sqr_p521_alt` | `bignum_sqr_p521_alt`: `BIGNUM_SQR_P521_ALT_SUBROUTINE_SAFE` | not imported |
 | `bignum_tomont_p256` | `bignum_tomont_p256`: none | `bignum_tomont_p256`: none |
 | `bignum_tomont_p256_alt` | `bignum_tomont_p256_alt`: none | not imported |

BENCHMARKS.md

@@ -308,16 +308,16 @@ The maintainer's MacBook, in daily use. Its cores have DIT, which rind sets arou
 | Ed25519 verify | 18.81 µs | - | 18.48 µs | 20.22 µs | 18.60 µs | 18.94 µs | 29.44 µs ✓ | 41.29 µs |
 | P-256 ECDSA sign | 7.13 µs ✓ | - | 11.16 µs | 10.91 µs | 43.98 µs | 8.58 µs | 66.95 µs ✓ | 12.43 µs |
 | P-256 ECDSA verify | 26.25 µs ✓ | - | 27.38 µs | 29.22 µs | 151.69 µs | 28.18 µs | 156.18 µs ✓ | 41.90 µs |
-| SHA-256, 64 B | 90 ns | 37 ns | 70 ns | 44 ns | 36 ns | 35 ns | 225 ns ✓ | 159 ns |
-| SHA-256, 1350 B | 485 ns | 409 ns | 434 ns | 410 ns | 473 ns | 480 ns | 2.46 µs ✓ | 533 ns |
-| SHA-256, 16 KB | 4.93 µs | 5.01 µs | 4.86 µs | 4.84 µs | 5.66 µs | 5.79 µs | 29.00 µs ✓ | 4.98 µs |
+| SHA-256, 64 B | 90 ns ✓ | 37 ns ✓ | 70 ns | 44 ns | 36 ns | 35 ns | 225 ns ✓ | 159 ns |
+| SHA-256, 1350 B | 485 ns ✓ | 409 ns ✓ | 434 ns | 410 ns | 473 ns | 480 ns | 2.46 µs ✓ | 533 ns |
+| SHA-256, 16 KB | 4.93 µs ✓ | 5.01 µs ✓ | 4.86 µs | 4.84 µs | 5.66 µs | 5.79 µs | 29.00 µs ✓ | 4.98 µs |
 | SHA-512, 64 B | 108 ns | 75 ns | 105 ns | 84 ns | 77 ns | 175 ns | 142 ns ✓ | 205 ns |
 | SHA-512, 1350 B | 810 ns | 730 ns | 768 ns | 743 ns | 723 ns | 1.87 µs | 1.56 µs ✓ | 893 ns |
 | SHA-512, 16 KB | 8.85 µs | 8.72 µs | 8.91 µs | 8.70 µs | 8.59 µs | 21.69 µs | 18.39 µs ✓ | 9.33 µs |
-| HMAC-SHA256, 64 B | 189 ns | 110 ns | 245 ns | 134 ns | 99 ns | 112 ns | 564 ns ✓ | 2.09 µs |
-| HMAC-SHA256, 1350 B | 559 ns | 487 ns | 597 ns | 502 ns | 545 ns | 562 ns | 2.80 µs ✓ | 2.41 µs |
-| HKDF-SHA256 extract and expand | 338 ns | 226 ns | 330 ns | 273 ns | 212 ns | - | 936 ns ✓ | 2.16 µs |
-| HKDF-SHA256 expand | 107 ns | 74 ns | 154 ns | 93 ns | 69 ns | - | 481 ns ✓ | 1.55 µs |
+| HMAC-SHA256, 64 B | 189 ns ✓ | 110 ns ✓ | 245 ns | 134 ns | 99 ns | 112 ns | 564 ns ✓ | 2.09 µs |
+| HMAC-SHA256, 1350 B | 559 ns ✓ | 487 ns ✓ | 597 ns | 502 ns | 545 ns | 562 ns | 2.80 µs ✓ | 2.41 µs |
+| HKDF-SHA256 extract and expand | 338 ns ✓ | 226 ns ✓ | 330 ns | 273 ns | 212 ns | - | 936 ns ✓ | 2.16 µs |
+| HKDF-SHA256 expand | 107 ns ✓ | 74 ns ✓ | 154 ns | 93 ns | 69 ns | - | 481 ns ✓ | 1.55 µs |
 | RSA-2048 PKCS#1 sign | 275.40 µs | - | 283.82 µs | 323.02 µs | 588.22 µs | 551.44 µs | - | 340.40 µs |
 | RSA-2048 PKCS#1 verify | 8.41 µs | - | 9.54 µs | 11.01 µs | 30.97 µs | 18.43 µs | - | 16.81 µs |
 | RSA-2048 PSS sign | 275.82 µs | - | 285.36 µs | 323.17 µs | 589.96 µs | 551.49 µs | 4.47 ms ✓ | 341.81 µs |
@@ -836,6 +836,7 @@ A ✓ means a published, machine-checked proof shows that all the code computing
 | rind | `ed25519-sign`, `ed25519-verify` | aarch64 without sha3 | [rind's Lean proof, through Aeneas and a hand model of the function-pointer dispatch Aeneas cannot translate, of its signature API's Ed25519 key loading, signing, and verification, small-order key refusal included, down to s2n-bignum's routines and its SHA-512 down to aws-lc's sha512_block_data_order_nohw, which rind runs without the SHA-512 instructions, composed with s2n-bignum's HOL Light proofs of edwards25519_decode_alt, edwards25519_scalarmulbase_alt, edwards25519_scalarmuldouble_alt, bignum_madd_n25519_alt, bignum_mod_n25519, bignum_neg_p25519, and bignum_lt, of s2n-bignum's own object code, which rind transliterates, and rind's HOL Light proof of bignum_eq, of the object code rind's build emits, and aws-lc-verification's NSym proof of that SHA-512 routine, with its ArmSpecGap caveat](https://github.com/moq-dev/rind/blob/main/proofs/Rind/X86_64/Ed25519.lean) |
 | rind | `p256-ecdh` | aarch64 | [rind's Lean proof, through Aeneas and hand models of the function-pointer dispatch and of key generation's draws through a dyn RandomSource, which Aeneas cannot translate, of its agreement API's P-256 key generation, public key, and agreement down to s2n-bignum's routines, composed with s2n-bignum's HOL Light proofs of p256_scalarmulbase_alt, p256_scalarmul_alt, bignum_tomont_p256, bignum_demont_p256, bignum_add_p256, bignum_montmul_p256, bignum_montsqr_p256, and bignum_mod_n256_4, of s2n-bignum's own object code, which rind transliterates, and rind's HOL Light proof of bignum_eq, of the object code rind's build emits, with rind's generator table proven to hold the multiples of G that s2n-bignum's proof assumes](https://github.com/moq-dev/rind/blob/main/proofs/Rind/Aarch64/P256.lean) |
 | rind | `p256-ecdsa-sign`, `p256-ecdsa-verify` | aarch64 | [rind's Lean proof, through Aeneas and hand models of the function-pointer dispatch and of the nonces' draws through a dyn RandomSource, which Aeneas cannot translate, of its signature API's P-256 ECDSA with SHA-256 and fixed-length signatures, key generation and loading, signing, and verification, down to s2n-bignum's routines, composed with s2n-bignum's HOL Light proofs of p256_scalarmulbase_alt, p256_montjadd_alt, p256_montjdouble_alt, p256_montjmixadd_alt, bignum_inv_p256, bignum_neg_p256, bignum_tomont_p256, bignum_demont_p256, bignum_add_p256, bignum_montmul_p256, bignum_montsqr_p256, bignum_mod_n256_4, bignum_modadd, bignum_montmul, bignum_demont, and bignum_modinv, of s2n-bignum's own object code, which rind transliterates, and rind's HOL Light proof of bignum_eq, of the object code rind's build emits, with the group laws its twin multiplication relies on proven from Mathlib's and the generator's order n proven, assuming HOL Light's P256_GROUP_ELEMENT_ORDER, that a point has order n, only for verification with a parsed public key, and proving a signature right when signing returns, as its nonce loop has no bound](https://github.com/moq-dev/rind/blob/main/proofs/Rind/Aarch64/P256Signature.lean) |
+| rind | `sha256/*`, `hmac-sha256/*`, `hkdf-sha256/*` | aarch64 with aes, pmull, sha2 | [rind's Lean proof, through Aeneas and hand models of the function-pointer dispatch and of HKDF-Expand's loop over its info slices, which Aeneas cannot translate, of its digest, HMAC, and HKDF APIs' SHA-256, padding included, down to aws-lc's sha256_block_data_order_hw, which rind runs with the crypto extension, composed with rind's HOL Light proof of that routine, of the object code rind's build emits, against s2n-bignum's FIPS 180-4 spec from awslabs/s2n-bignum#415, unmerged, which rind pins at 79120e64 and proves FIPS 180-4's](https://github.com/moq-dev/rind/blob/main/proofs/Rind/Aarch64/Sha256Hw.lean) |
 | rind | `quic-header-protection/chacha20` | x86_64 | [rind's Lean proof, through Aeneas and a hand model of the function-pointer dispatch Aeneas cannot translate, which assumes each key's mask is its own cipher's, the only one rind builds, of its header-protection API's ChaCha20 against RFC 9001 and RFC 8439, HACL*'s rounds included](https://github.com/moq-dev/rind/blob/main/proofs/Rind/X86_64/ChaCha20.lean) |
 | rind | `quic-header-protection/chacha20` | aarch64 | [rind's Lean proof, through Aeneas and a hand model of the function-pointer dispatch Aeneas cannot translate, which assumes each key's mask is its own cipher's, the only one rind builds, of its header-protection API's ChaCha20 against RFC 9001 and RFC 8439, HACL*'s rounds included](https://github.com/moq-dev/rind/blob/main/proofs/Rind/X86_64/ChaCha20.lean) |
 | rind | `aes128-gcm/*`, `aes128-gcm-open/*`, `aes256-gcm/*`, `aes256-gcm-open/*` | x86_64 with aes, pclmulqdq, ssse3, sse4.1, avx, movbe without vaes | [rind's Lean proof, through Aeneas and hand models of the function-pointer dispatch, of the AES-NI key expansion and block cipher's raw-pointer loads, and of the SIMD intrinsics as Intel's manual defines them, of its AEAD API's AES-GCM key setup, seal, and open, for AAD and messages under 2^32 bytes, down to HACL*'s Vale AES-GCM routines, composed with Vale's F* proofs of Gcm_blocks_stdcall, Gcm_blocks_decrypt_stdcall, and Compute_iv_stdcall, of the code Vale prints at HACL* f557259007db, which rind imports](https://github.com/moq-dev/rind/blob/main/proofs/Rind/X86_64/AesGcm.lean) |

admin/prove

@@ -8,7 +8,7 @@
 # so no Lean module imports both. The aarch64 hand models and its X25519,
 # SHA-512, ChaCha20, Ed25519, SHA-1, SHA-256, HMAC, digest, HKDF, and PBKDF2 proofs are the
 # x86_64 ones with the target renamed, which this writes too, all but each
-# target's own `ShaBlocks.lean`.
+# target's own `ShaBlocks.lean` and `HashAxioms.lean`.
 #
 # Usage: admin/prove [bytes | hol-light | lean]
 #
@@ -192,15 +192,47 @@ symbol_bounds() {
         b[m] == s && a[n] != "*UND*" { print a[n], a[1], b[1] }'
 }
 
-# rind's own HOL Light proofs, each of the `asm!` block in a Rust function,
-# on s2n-bignum's model, tactics, and specs at its submodule's commit, the
-# revision rind's transliteration pins. Each reads its block's bytes from
-# `<arch>/<file>.bin`, which `asm_block` writes, and asserts they are the ones
-# it lists. A target's proofs compile into one program, as s2n-bignum's
+# Writes to `dest` an object holding the naked Rust function at `path`, as
+# rind's release build for `arch` Linux emits it: the function's own section,
+# renamed `.text`, its relocations, and the one read-only data section they
+# all refer to, renamed `.rodata`. s2n-bignum's `define_assert_relocs_from_elf`
+# reads it, failing unless its instructions and relocations are the ones the
+# proof lists, and gives the proof that section's bytes. Anything else fails:
+# a function that is not its whole section, or relocations to other sections.
+asm_function() {
+    local arch=$1 path=$2 dest=$3
+    local found obj sym section size secsize target
+    found=$(rind_symbol "$arch" "$path")
+    read -r obj sym <<<"$found"
+    read -r section _ size < <(symbol_bounds "$obj" "$sym")
+    secsize=$("$tools/llvm-objdump" -h "$obj" | awk -v s="$section" '$2 == s { print $3 }')
+    if [[ $section != ".text.$sym" || $((16#$size)) != $((16#${secsize:-0})) ]]; then
+        echo "admin/prove: $path is not the whole of its own section" >&2
+        return 1
+    fi
+    target=$(relocations "$obj" "$section" | awk '{ sub(/[-+].*/, "", $3); print $3 }' | sort -u)
+    if [[ $(wc -l <<<"$target") != 1 || $target != .rodata.* ]]; then
+        echo "admin/prove: $path's relocations refer to other than one .rodata section:" $target >&2
+        return 1
+    fi
+    "$tools/llvm-objcopy" --only-section="$section" --only-section=".rela$section" \
+        --only-section="$target" --rename-section="$section=.text" --rename-section="$target=.rodata" \
+        "$obj" "$dest"
+}
+
+# rind's own HOL Light proofs, each of the `asm!` block in a Rust function or
+# of a naked one, on s2n-bignum's model, tactics, and specs at its submodule's
+# commit, the revision rind's transliteration pins, with the specs of
+# s2n-bignum pull requests not yet merged from `proofs/hol-light/s2n-bignum/`.
+# Each `<arch>/<file>.ml` reads its object code from `<arch>/<file>.bin`, the
+# block's bytes, which `asm_block` writes, or `<arch>/<file>.o`, the naked
+# function's object, which `asm_function` writes, and asserts it is what it
+# lists. A target's proofs compile into one program, as s2n-bignum's
 # `tools/build-proof.sh` compiles each of its own, which fails on an error or
 # an axiom beyond HOL Light's.
 hol_light_proofs=(
-    "aarch64 bignum_eq rind::low::aarch64::bignum_eq::bignum_eq"
+    "aarch64 bignum_eq.bin rind::low::aarch64::bignum_eq::bignum_eq"
+    "aarch64 sha256_block_data_order_hw.o rind::low::aarch64::sha256::sha256_block_data_order_hw"
 )
 hol_light() {
     local dir=$out/hol-light root=$PWD arches arch file path proof
@@ -215,12 +247,15 @@ hol_light() {
     done
     for proof in "${hol_light_proofs[@]}"; do
         read -r arch file path <<<"$proof"
-        asm_block "$arch" "$path" "$dir/$arch/$file.bin"
-        echo "loadt \"$arch/$file.ml\";;" >>"$dir/$arch.ml"
+        case $file in
+        *.bin) asm_block "$arch" "$path" "$dir/$arch/$file" ;;
+        *.o) asm_function "$arch" "$path" "$dir/$arch/$file" ;;
+        esac
+        echo "loadt \"$arch/${file%.*}.ml\";;" >>"$dir/$arch.ml"
     done
     for arch in $arches; do
         printf 'check_axioms ();; Printf.printf "%s: %%.0f s\\n" (Unix.time () -. prove_start);;\n' "$arch" >>"$dir/$arch.ml"
-        (cd "$dir" && HOLLIGHT_LOAD_PATH="$root/proofs/hol-light:$root/thirdparty/s2n-bignum" \
+        (cd "$dir" && HOLLIGHT_LOAD_PATH="$root/proofs/hol-light:$root/proofs/hol-light/s2n-bignum:$root/thirdparty/s2n-bignum" \
             ocaml "$HOLLIGHT_DIR/inline_load.ml" "$arch.ml" "$arch-inlined.ml")
         OCAMLRUNPARAM=l=2000000000 ocamlopt.byte -pp "$("$HOLLIGHT_DIR/hol.sh" -pp)" \
             -I "$HOLLIGHT_DIR" -I +unix -c hol_lib.cmxa "$dir/$arch-inlined.ml" -o "$dir/$arch.cmx" -w -a
@@ -695,14 +730,15 @@ extract aarch64 Aarch64 \
     --opaque 'crate::mid::p256::_::new_random' \
     --include crate::low::aarch64::sha1::sha1_compress_padded \
     --include crate::low::aarch64::sha256 \
-    --opaque crate::low::aarch64::sha256::sha256_compress_blocks
+    --opaque crate::low::aarch64::sha256::compress_hw \
+    --opaque crate::low::aarch64::sha256::compress_nohw
 
 extract_kdf x86_64 X86_64
 extract_kdf aarch64 Aarch64
 
 mkdir -p proofs/Rind/Aarch64/Kdf
 for file in Dispatch X25519 DigestAlgorithm DigestDispatch Sha512 ChaCha20 SignatureDispatch Ed25519 \
-    Blockwise Sha Hmac HashAxioms HmacDispatch HkdfExpand Kdf/TypesExternal Kdf/FunsExternal \
+    Blockwise Sha Hmac HmacDispatch HkdfExpand Kdf/TypesExternal Kdf/FunsExternal \
     HmacApi DigestApi Hkdf Pbkdf2; do
     sed 's/X86_64/Aarch64/g; s/x86_64/aarch64/g' "proofs/Rind/X86_64/$file.lean" >"proofs/Rind/Aarch64/$file.lean"
 done