diff --git a/.gitignore b/.gitignore index 1f5d26ad1..6d21269cd 100644 --- a/.gitignore +++ b/.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 diff --git a/ALGORITHMS.md b/ALGORITHMS.md index 6ba3808ba..c756f6ea2 100644 --- a/ALGORITHMS.md +++ b/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 | diff --git a/BENCHMARKS.md b/BENCHMARKS.md index 5166598e3..e660cf31c 100644 --- a/BENCHMARKS.md +++ b/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) | diff --git a/admin/prove b/admin/prove index 269745a89..cacf29d27 100755 --- a/admin/prove +++ b/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 -# `/.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 `/.ml` reads its object code from `/.bin`, the +# block's bytes, which `asm_block` writes, or `/.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 diff --git a/benchmarks/kixtop-dark.svg b/benchmarks/kixtop-dark.svg index 316883303..d1d4eccd3 100644 --- a/benchmarks/kixtop-dark.svg +++ b/benchmarks/kixtop-dark.svg @@ -558,10 +558,12 @@ Hashes and KDFs SHA-256, 64 B -SHA-256, 64 B, rind: 90 ns, 2.54× the fastest -90 ns -SHA-256, 64 B, rind (DIT held): 37 ns, 1.04× the fastest -37 ns +SHA-256, 64 B, rind: 90 ns, 2.54× the fastest; verified: 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 +90 ns + +SHA-256, 64 B, rind (DIT held): 37 ns, 1.04× the fastest; verified: 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 +37 ns + SHA-256, 64 B, aws-lc-rs: 70 ns, 1.99× the fastest 70 ns SHA-256, 64 B, ring: 44 ns, 1.25× the fastest @@ -576,10 +578,12 @@ SHA-256, 64 B, OpenSSL: 159 ns, 4.51× the fastest 159 ns SHA-256, 1350 B -SHA-256, 1350 B, rind: 485 ns, 1.18× the fastest -485 ns -SHA-256, 1350 B, rind (DIT held): 409 ns, 1.00× the fastest -409 ns +SHA-256, 1350 B, rind: 485 ns, 1.18× the fastest; verified: 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 +485 ns + +SHA-256, 1350 B, rind (DIT held): 409 ns, 1.00× the fastest; verified: 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 +409 ns + SHA-256, 1350 B, aws-lc-rs: 434 ns, 1.06× the fastest 434 ns SHA-256, 1350 B, ring: 410 ns, 1.00× the fastest @@ -594,10 +598,12 @@ SHA-256, 1350 B, OpenSSL: 533 ns, 1.30× the fastest 533 ns SHA-256, 16 KB -SHA-256, 16 KB, rind: 4.93 µs, 1.02× the fastest -4.93 µs -SHA-256, 16 KB, rind (DIT held): 5.01 µs, 1.04× the fastest -5.01 µs +SHA-256, 16 KB, rind: 4.93 µs, 1.02× the fastest; verified: 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 +4.93 µs + +SHA-256, 16 KB, rind (DIT held): 5.01 µs, 1.04× the fastest; verified: 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 +5.01 µs + SHA-256, 16 KB, aws-lc-rs: 4.86 µs, 1.00× the fastest 4.86 µs SHA-256, 16 KB, ring: 4.84 µs, 1.00× the fastest @@ -666,10 +672,12 @@ SHA-512, 16 KB, OpenSSL: 9.33 µs, 1.09× the fastest 9.33 µs HMAC-SHA256, 64 B -HMAC-SHA256, 64 B, rind: 189 ns, 1.90× the fastest -189 ns -HMAC-SHA256, 64 B, rind (DIT held): 110 ns, 1.10× the fastest -110 ns +HMAC-SHA256, 64 B, rind: 189 ns, 1.90× the fastest; verified: 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 +189 ns + +HMAC-SHA256, 64 B, rind (DIT held): 110 ns, 1.10× the fastest; verified: 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 +110 ns + HMAC-SHA256, 64 B, aws-lc-rs: 245 ns, 2.47× the fastest 245 ns HMAC-SHA256, 64 B, ring: 134 ns, 1.35× the fastest @@ -684,10 +692,12 @@ HMAC-SHA256, 64 B, OpenSSL: 2.09 µs, 21.07× the fastest 2.09 µs HMAC-SHA256, 1350 B -HMAC-SHA256, 1350 B, rind: 559 ns, 1.11× the fastest -559 ns -HMAC-SHA256, 1350 B, rind (DIT held): 487 ns, 0.97× the fastest -487 ns +HMAC-SHA256, 1350 B, rind: 559 ns, 1.11× the fastest; verified: 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 +559 ns + +HMAC-SHA256, 1350 B, rind (DIT held): 487 ns, 0.97× the fastest; verified: 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 +487 ns + HMAC-SHA256, 1350 B, aws-lc-rs: 597 ns, 1.19× the fastest 597 ns HMAC-SHA256, 1350 B, ring: 502 ns, 1.00× the fastest @@ -702,10 +712,12 @@ HMAC-SHA256, 1350 B, OpenSSL: 2.41 µs, 4.80× the fastest 2.41 µs HKDF-SHA256 extract and expand -HKDF-SHA256 extract and expand, rind: 338 ns, 1.60× the fastest -338 ns -HKDF-SHA256 extract and expand, rind (DIT held): 226 ns, 1.07× the fastest -226 ns +HKDF-SHA256 extract and expand, rind: 338 ns, 1.60× the fastest; verified: 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 +338 ns + +HKDF-SHA256 extract and expand, rind (DIT held): 226 ns, 1.07× the fastest; verified: 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 +226 ns + HKDF-SHA256 extract and expand, aws-lc-rs: 330 ns, 1.56× the fastest 330 ns HKDF-SHA256 extract and expand, ring: 273 ns, 1.29× the fastest @@ -718,10 +730,12 @@ HKDF-SHA256 extract and expand, OpenSSL: 2.16 µs, 10.20× the fastest 2.16 µs HKDF-SHA256 expand -HKDF-SHA256 expand, rind: 107 ns, 1.56× the fastest -107 ns -HKDF-SHA256 expand, rind (DIT held): 74 ns, 1.08× the fastest -74 ns +HKDF-SHA256 expand, rind: 107 ns, 1.56× the fastest; verified: 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 +107 ns + +HKDF-SHA256 expand, rind (DIT held): 74 ns, 1.08× the fastest; verified: 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 +74 ns + HKDF-SHA256 expand, aws-lc-rs: 154 ns, 2.23× the fastest 154 ns HKDF-SHA256 expand, ring: 93 ns, 1.35× the fastest diff --git a/benchmarks/kixtop.svg b/benchmarks/kixtop.svg index b2621257a..343177e07 100644 --- a/benchmarks/kixtop.svg +++ b/benchmarks/kixtop.svg @@ -558,10 +558,12 @@ Hashes and KDFs SHA-256, 64 B -SHA-256, 64 B, rind: 90 ns, 2.54× the fastest -90 ns -SHA-256, 64 B, rind (DIT held): 37 ns, 1.04× the fastest -37 ns +SHA-256, 64 B, rind: 90 ns, 2.54× the fastest; verified: 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 +90 ns + +SHA-256, 64 B, rind (DIT held): 37 ns, 1.04× the fastest; verified: 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 +37 ns + SHA-256, 64 B, aws-lc-rs: 70 ns, 1.99× the fastest 70 ns SHA-256, 64 B, ring: 44 ns, 1.25× the fastest @@ -576,10 +578,12 @@ SHA-256, 64 B, OpenSSL: 159 ns, 4.51× the fastest 159 ns SHA-256, 1350 B -SHA-256, 1350 B, rind: 485 ns, 1.18× the fastest -485 ns -SHA-256, 1350 B, rind (DIT held): 409 ns, 1.00× the fastest -409 ns +SHA-256, 1350 B, rind: 485 ns, 1.18× the fastest; verified: 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 +485 ns + +SHA-256, 1350 B, rind (DIT held): 409 ns, 1.00× the fastest; verified: 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 +409 ns + SHA-256, 1350 B, aws-lc-rs: 434 ns, 1.06× the fastest 434 ns SHA-256, 1350 B, ring: 410 ns, 1.00× the fastest @@ -594,10 +598,12 @@ SHA-256, 1350 B, OpenSSL: 533 ns, 1.30× the fastest 533 ns SHA-256, 16 KB -SHA-256, 16 KB, rind: 4.93 µs, 1.02× the fastest -4.93 µs -SHA-256, 16 KB, rind (DIT held): 5.01 µs, 1.04× the fastest -5.01 µs +SHA-256, 16 KB, rind: 4.93 µs, 1.02× the fastest; verified: 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 +4.93 µs + +SHA-256, 16 KB, rind (DIT held): 5.01 µs, 1.04× the fastest; verified: 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 +5.01 µs + SHA-256, 16 KB, aws-lc-rs: 4.86 µs, 1.00× the fastest 4.86 µs SHA-256, 16 KB, ring: 4.84 µs, 1.00× the fastest @@ -666,10 +672,12 @@ SHA-512, 16 KB, OpenSSL: 9.33 µs, 1.09× the fastest 9.33 µs HMAC-SHA256, 64 B -HMAC-SHA256, 64 B, rind: 189 ns, 1.90× the fastest -189 ns -HMAC-SHA256, 64 B, rind (DIT held): 110 ns, 1.10× the fastest -110 ns +HMAC-SHA256, 64 B, rind: 189 ns, 1.90× the fastest; verified: 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 +189 ns + +HMAC-SHA256, 64 B, rind (DIT held): 110 ns, 1.10× the fastest; verified: 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 +110 ns + HMAC-SHA256, 64 B, aws-lc-rs: 245 ns, 2.47× the fastest 245 ns HMAC-SHA256, 64 B, ring: 134 ns, 1.35× the fastest @@ -684,10 +692,12 @@ HMAC-SHA256, 64 B, OpenSSL: 2.09 µs, 21.07× the fastest 2.09 µs HMAC-SHA256, 1350 B -HMAC-SHA256, 1350 B, rind: 559 ns, 1.11× the fastest -559 ns -HMAC-SHA256, 1350 B, rind (DIT held): 487 ns, 0.97× the fastest -487 ns +HMAC-SHA256, 1350 B, rind: 559 ns, 1.11× the fastest; verified: 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 +559 ns + +HMAC-SHA256, 1350 B, rind (DIT held): 487 ns, 0.97× the fastest; verified: 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 +487 ns + HMAC-SHA256, 1350 B, aws-lc-rs: 597 ns, 1.19× the fastest 597 ns HMAC-SHA256, 1350 B, ring: 502 ns, 1.00× the fastest @@ -702,10 +712,12 @@ HMAC-SHA256, 1350 B, OpenSSL: 2.41 µs, 4.80× the fastest 2.41 µs HKDF-SHA256 extract and expand -HKDF-SHA256 extract and expand, rind: 338 ns, 1.60× the fastest -338 ns -HKDF-SHA256 extract and expand, rind (DIT held): 226 ns, 1.07× the fastest -226 ns +HKDF-SHA256 extract and expand, rind: 338 ns, 1.60× the fastest; verified: 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 +338 ns + +HKDF-SHA256 extract and expand, rind (DIT held): 226 ns, 1.07× the fastest; verified: 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 +226 ns + HKDF-SHA256 extract and expand, aws-lc-rs: 330 ns, 1.56× the fastest 330 ns HKDF-SHA256 extract and expand, ring: 273 ns, 1.29× the fastest @@ -718,10 +730,12 @@ HKDF-SHA256 extract and expand, OpenSSL: 2.16 µs, 10.20× the fastest 2.16 µs HKDF-SHA256 expand -HKDF-SHA256 expand, rind: 107 ns, 1.56× the fastest -107 ns -HKDF-SHA256 expand, rind (DIT held): 74 ns, 1.08× the fastest -74 ns +HKDF-SHA256 expand, rind: 107 ns, 1.56× the fastest; verified: 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 +107 ns + +HKDF-SHA256 expand, rind (DIT held): 74 ns, 1.08× the fastest; verified: 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 +74 ns + HKDF-SHA256 expand, aws-lc-rs: 154 ns, 2.23× the fastest 154 ns HKDF-SHA256 expand, ring: 93 ns, 1.35× the fastest diff --git a/benchmarks/overview-dark.svg b/benchmarks/overview-dark.svg index 73e0d3aa6..a85dcf053 100644 --- a/benchmarks/overview-dark.svg +++ b/benchmarks/overview-dark.svg @@ -1429,10 +1429,12 @@ SHA-256, 64 B, rind on nixos: 69 ns, 1.17× the fastest SHA-256, 64 B, rind on desktop: 28 ns, 1.00× the fastest SHA-256, 64 B, rind on nixos2: 244 ns, 1.00× the fastest -SHA-256, 64 B, rind on kixtop: 90 ns, 2.54× the fastest +SHA-256, 64 B, rind on kixtop: 90 ns, 2.54× the fastest; verified: 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 + SHA-256, 64 B, rind on ovh-iad: 399 ns, 1.00× the fastest SHA-256, 64 B, rind on ovh-sea: 386 ns, 1.00× the fastest -SHA-256, 64 B, rind (DIT held) on kixtop: 37 ns, 1.04× the fastest +SHA-256, 64 B, rind (DIT held) on kixtop: 37 ns, 1.04× the fastest; verified: 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 + SHA-256, 64 B, aws-lc-rs on nixos: 96 ns, 1.63× the fastest SHA-256, 64 B, aws-lc-rs on desktop: 57 ns, 2.02× the fastest SHA-256, 64 B, aws-lc-rs on nixos2: 307 ns, 1.26× the fastest @@ -1477,10 +1479,12 @@ SHA-256, 1350 B, rind on nixos: 620 ns, 1.00× the fastest SHA-256, 1350 B, rind on desktop: 269 ns, 1.00× the fastest SHA-256, 1350 B, rind on nixos2: 2.46 µs, 1.00× the fastest -SHA-256, 1350 B, rind on kixtop: 485 ns, 1.18× the fastest +SHA-256, 1350 B, rind on kixtop: 485 ns, 1.18× the fastest; verified: 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 + SHA-256, 1350 B, rind on ovh-iad: 3.87 µs, 1.00× the fastest SHA-256, 1350 B, rind on ovh-sea: 3.85 µs, 1.00× the fastest -SHA-256, 1350 B, rind (DIT held) on kixtop: 409 ns, 1.00× the fastest +SHA-256, 1350 B, rind (DIT held) on kixtop: 409 ns, 1.00× the fastest; verified: 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 + SHA-256, 1350 B, aws-lc-rs on nixos: 740 ns, 1.20× the fastest SHA-256, 1350 B, aws-lc-rs on desktop: 306 ns, 1.14× the fastest SHA-256, 1350 B, aws-lc-rs on nixos2: 2.79 µs, 1.14× the fastest @@ -1525,10 +1529,12 @@ SHA-256, 16 KB, rind on nixos: 6.86 µs, 1.00× the fastest SHA-256, 16 KB, rind on desktop: 3.19 µs, 1.00× the fastest SHA-256, 16 KB, rind on nixos2: 28.06 µs, 1.00× the fastest -SHA-256, 16 KB, rind on kixtop: 4.93 µs, 1.02× the fastest +SHA-256, 16 KB, rind on kixtop: 4.93 µs, 1.02× the fastest; verified: 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 + SHA-256, 16 KB, rind on ovh-iad: 45.11 µs, 1.00× the fastest SHA-256, 16 KB, rind on ovh-sea: 43.51 µs, 1.00× the fastest -SHA-256, 16 KB, rind (DIT held) on kixtop: 5.01 µs, 1.04× the fastest +SHA-256, 16 KB, rind (DIT held) on kixtop: 5.01 µs, 1.04× the fastest; verified: 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 + SHA-256, 16 KB, aws-lc-rs on nixos: 6.88 µs, 1.00× the fastest SHA-256, 16 KB, aws-lc-rs on desktop: 3.23 µs, 1.01× the fastest SHA-256, 16 KB, aws-lc-rs on nixos2: 31.46 µs, 1.12× the fastest @@ -1729,10 +1735,12 @@ HMAC-SHA256, 64 B, rind on nixos: 147 ns, 1.00× the fastest HMAC-SHA256, 64 B, rind on desktop: 75 ns, 1.00× the fastest HMAC-SHA256, 64 B, rind on nixos2: 628 ns, 1.00× the fastest -HMAC-SHA256, 64 B, rind on kixtop: 189 ns, 1.90× the fastest +HMAC-SHA256, 64 B, rind on kixtop: 189 ns, 1.90× the fastest; verified: 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 + HMAC-SHA256, 64 B, rind on ovh-iad: 1.16 µs, 1.00× the fastest HMAC-SHA256, 64 B, rind on ovh-sea: 963 ns, 1.00× the fastest -HMAC-SHA256, 64 B, rind (DIT held) on kixtop: 110 ns, 1.10× the fastest +HMAC-SHA256, 64 B, rind (DIT held) on kixtop: 110 ns, 1.10× the fastest; verified: 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 + HMAC-SHA256, 64 B, aws-lc-rs on nixos: 264 ns, 1.80× the fastest HMAC-SHA256, 64 B, aws-lc-rs on desktop: 180 ns, 2.40× the fastest HMAC-SHA256, 64 B, aws-lc-rs on nixos2: 811 ns, 1.29× the fastest @@ -1777,10 +1785,12 @@ HMAC-SHA256, 1350 B, rind on nixos: 692 ns, 1.00× the fastest HMAC-SHA256, 1350 B, rind on desktop: 328 ns, 1.00× the fastest HMAC-SHA256, 1350 B, rind on nixos2: 2.79 µs, 1.00× the fastest -HMAC-SHA256, 1350 B, rind on kixtop: 559 ns, 1.11× the fastest +HMAC-SHA256, 1350 B, rind on kixtop: 559 ns, 1.11× the fastest; verified: 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 + HMAC-SHA256, 1350 B, rind on ovh-iad: 4.82 µs, 1.00× the fastest HMAC-SHA256, 1350 B, rind on ovh-sea: 4.31 µs, 1.00× the fastest -HMAC-SHA256, 1350 B, rind (DIT held) on kixtop: 487 ns, 0.97× the fastest +HMAC-SHA256, 1350 B, rind (DIT held) on kixtop: 487 ns, 0.97× the fastest; verified: 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 + HMAC-SHA256, 1350 B, aws-lc-rs on nixos: 853 ns, 1.23× the fastest HMAC-SHA256, 1350 B, aws-lc-rs on desktop: 435 ns, 1.33× the fastest HMAC-SHA256, 1350 B, aws-lc-rs on nixos2: 3.30 µs, 1.18× the fastest @@ -1825,10 +1835,12 @@ HKDF-SHA256 extract and expand, rind on nixos: 257 ns, 1.00× the fastest HKDF-SHA256 extract and expand, rind on desktop: 158 ns, 1.00× the fastest HKDF-SHA256 extract and expand, rind on nixos2: 1.15 µs, 1.00× the fastest -HKDF-SHA256 extract and expand, rind on kixtop: 338 ns, 1.60× the fastest +HKDF-SHA256 extract and expand, rind on kixtop: 338 ns, 1.60× the fastest; verified: 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 + HKDF-SHA256 extract and expand, rind on ovh-iad: 2.10 µs, 1.01× the fastest HKDF-SHA256 extract and expand, rind on ovh-sea: 1.70 µs, 1.00× the fastest -HKDF-SHA256 extract and expand, rind (DIT held) on kixtop: 226 ns, 1.07× the fastest +HKDF-SHA256 extract and expand, rind (DIT held) on kixtop: 226 ns, 1.07× the fastest; verified: 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 + HKDF-SHA256 extract and expand, aws-lc-rs on nixos: 369 ns, 1.44× the fastest HKDF-SHA256 extract and expand, aws-lc-rs on desktop: 285 ns, 1.80× the fastest HKDF-SHA256 extract and expand, aws-lc-rs on nixos2: 1.44 µs, 1.25× the fastest @@ -1869,10 +1881,12 @@ HKDF-SHA256 expand, rind on nixos: 89 ns, 1.00× the fastest HKDF-SHA256 expand, rind on desktop: 66 ns, 1.00× the fastest HKDF-SHA256 expand, rind on nixos2: 300 ns, 1.00× the fastest -HKDF-SHA256 expand, rind on kixtop: 107 ns, 1.56× the fastest +HKDF-SHA256 expand, rind on kixtop: 107 ns, 1.56× the fastest; verified: 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 + HKDF-SHA256 expand, rind on ovh-iad: 540 ns, 1.00× the fastest HKDF-SHA256 expand, rind on ovh-sea: 464 ns, 1.00× the fastest -HKDF-SHA256 expand, rind (DIT held) on kixtop: 74 ns, 1.08× the fastest +HKDF-SHA256 expand, rind (DIT held) on kixtop: 74 ns, 1.08× the fastest; verified: 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 + HKDF-SHA256 expand, aws-lc-rs on nixos: 179 ns, 2.02× the fastest HKDF-SHA256 expand, aws-lc-rs on desktop: 124 ns, 1.88× the fastest HKDF-SHA256 expand, aws-lc-rs on nixos2: 636 ns, 2.12× the fastest diff --git a/benchmarks/overview.svg b/benchmarks/overview.svg index 2d5782aba..43107f9b2 100644 --- a/benchmarks/overview.svg +++ b/benchmarks/overview.svg @@ -1429,10 +1429,12 @@ SHA-256, 64 B, rind on nixos: 69 ns, 1.17× the fastest SHA-256, 64 B, rind on desktop: 28 ns, 1.00× the fastest SHA-256, 64 B, rind on nixos2: 244 ns, 1.00× the fastest -SHA-256, 64 B, rind on kixtop: 90 ns, 2.54× the fastest +SHA-256, 64 B, rind on kixtop: 90 ns, 2.54× the fastest; verified: 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 + SHA-256, 64 B, rind on ovh-iad: 399 ns, 1.00× the fastest SHA-256, 64 B, rind on ovh-sea: 386 ns, 1.00× the fastest -SHA-256, 64 B, rind (DIT held) on kixtop: 37 ns, 1.04× the fastest +SHA-256, 64 B, rind (DIT held) on kixtop: 37 ns, 1.04× the fastest; verified: 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 + SHA-256, 64 B, aws-lc-rs on nixos: 96 ns, 1.63× the fastest SHA-256, 64 B, aws-lc-rs on desktop: 57 ns, 2.02× the fastest SHA-256, 64 B, aws-lc-rs on nixos2: 307 ns, 1.26× the fastest @@ -1477,10 +1479,12 @@ SHA-256, 1350 B, rind on nixos: 620 ns, 1.00× the fastest SHA-256, 1350 B, rind on desktop: 269 ns, 1.00× the fastest SHA-256, 1350 B, rind on nixos2: 2.46 µs, 1.00× the fastest -SHA-256, 1350 B, rind on kixtop: 485 ns, 1.18× the fastest +SHA-256, 1350 B, rind on kixtop: 485 ns, 1.18× the fastest; verified: 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 + SHA-256, 1350 B, rind on ovh-iad: 3.87 µs, 1.00× the fastest SHA-256, 1350 B, rind on ovh-sea: 3.85 µs, 1.00× the fastest -SHA-256, 1350 B, rind (DIT held) on kixtop: 409 ns, 1.00× the fastest +SHA-256, 1350 B, rind (DIT held) on kixtop: 409 ns, 1.00× the fastest; verified: 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 + SHA-256, 1350 B, aws-lc-rs on nixos: 740 ns, 1.20× the fastest SHA-256, 1350 B, aws-lc-rs on desktop: 306 ns, 1.14× the fastest SHA-256, 1350 B, aws-lc-rs on nixos2: 2.79 µs, 1.14× the fastest @@ -1525,10 +1529,12 @@ SHA-256, 16 KB, rind on nixos: 6.86 µs, 1.00× the fastest SHA-256, 16 KB, rind on desktop: 3.19 µs, 1.00× the fastest SHA-256, 16 KB, rind on nixos2: 28.06 µs, 1.00× the fastest -SHA-256, 16 KB, rind on kixtop: 4.93 µs, 1.02× the fastest +SHA-256, 16 KB, rind on kixtop: 4.93 µs, 1.02× the fastest; verified: 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 + SHA-256, 16 KB, rind on ovh-iad: 45.11 µs, 1.00× the fastest SHA-256, 16 KB, rind on ovh-sea: 43.51 µs, 1.00× the fastest -SHA-256, 16 KB, rind (DIT held) on kixtop: 5.01 µs, 1.04× the fastest +SHA-256, 16 KB, rind (DIT held) on kixtop: 5.01 µs, 1.04× the fastest; verified: 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 + SHA-256, 16 KB, aws-lc-rs on nixos: 6.88 µs, 1.00× the fastest SHA-256, 16 KB, aws-lc-rs on desktop: 3.23 µs, 1.01× the fastest SHA-256, 16 KB, aws-lc-rs on nixos2: 31.46 µs, 1.12× the fastest @@ -1729,10 +1735,12 @@ HMAC-SHA256, 64 B, rind on nixos: 147 ns, 1.00× the fastest HMAC-SHA256, 64 B, rind on desktop: 75 ns, 1.00× the fastest HMAC-SHA256, 64 B, rind on nixos2: 628 ns, 1.00× the fastest -HMAC-SHA256, 64 B, rind on kixtop: 189 ns, 1.90× the fastest +HMAC-SHA256, 64 B, rind on kixtop: 189 ns, 1.90× the fastest; verified: 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 + HMAC-SHA256, 64 B, rind on ovh-iad: 1.16 µs, 1.00× the fastest HMAC-SHA256, 64 B, rind on ovh-sea: 963 ns, 1.00× the fastest -HMAC-SHA256, 64 B, rind (DIT held) on kixtop: 110 ns, 1.10× the fastest +HMAC-SHA256, 64 B, rind (DIT held) on kixtop: 110 ns, 1.10× the fastest; verified: 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 + HMAC-SHA256, 64 B, aws-lc-rs on nixos: 264 ns, 1.80× the fastest HMAC-SHA256, 64 B, aws-lc-rs on desktop: 180 ns, 2.40× the fastest HMAC-SHA256, 64 B, aws-lc-rs on nixos2: 811 ns, 1.29× the fastest @@ -1777,10 +1785,12 @@ HMAC-SHA256, 1350 B, rind on nixos: 692 ns, 1.00× the fastest HMAC-SHA256, 1350 B, rind on desktop: 328 ns, 1.00× the fastest HMAC-SHA256, 1350 B, rind on nixos2: 2.79 µs, 1.00× the fastest -HMAC-SHA256, 1350 B, rind on kixtop: 559 ns, 1.11× the fastest +HMAC-SHA256, 1350 B, rind on kixtop: 559 ns, 1.11× the fastest; verified: 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 + HMAC-SHA256, 1350 B, rind on ovh-iad: 4.82 µs, 1.00× the fastest HMAC-SHA256, 1350 B, rind on ovh-sea: 4.31 µs, 1.00× the fastest -HMAC-SHA256, 1350 B, rind (DIT held) on kixtop: 487 ns, 0.97× the fastest +HMAC-SHA256, 1350 B, rind (DIT held) on kixtop: 487 ns, 0.97× the fastest; verified: 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 + HMAC-SHA256, 1350 B, aws-lc-rs on nixos: 853 ns, 1.23× the fastest HMAC-SHA256, 1350 B, aws-lc-rs on desktop: 435 ns, 1.33× the fastest HMAC-SHA256, 1350 B, aws-lc-rs on nixos2: 3.30 µs, 1.18× the fastest @@ -1825,10 +1835,12 @@ HKDF-SHA256 extract and expand, rind on nixos: 257 ns, 1.00× the fastest HKDF-SHA256 extract and expand, rind on desktop: 158 ns, 1.00× the fastest HKDF-SHA256 extract and expand, rind on nixos2: 1.15 µs, 1.00× the fastest -HKDF-SHA256 extract and expand, rind on kixtop: 338 ns, 1.60× the fastest +HKDF-SHA256 extract and expand, rind on kixtop: 338 ns, 1.60× the fastest; verified: 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 + HKDF-SHA256 extract and expand, rind on ovh-iad: 2.10 µs, 1.01× the fastest HKDF-SHA256 extract and expand, rind on ovh-sea: 1.70 µs, 1.00× the fastest -HKDF-SHA256 extract and expand, rind (DIT held) on kixtop: 226 ns, 1.07× the fastest +HKDF-SHA256 extract and expand, rind (DIT held) on kixtop: 226 ns, 1.07× the fastest; verified: 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 + HKDF-SHA256 extract and expand, aws-lc-rs on nixos: 369 ns, 1.44× the fastest HKDF-SHA256 extract and expand, aws-lc-rs on desktop: 285 ns, 1.80× the fastest HKDF-SHA256 extract and expand, aws-lc-rs on nixos2: 1.44 µs, 1.25× the fastest @@ -1869,10 +1881,12 @@ HKDF-SHA256 expand, rind on nixos: 89 ns, 1.00× the fastest HKDF-SHA256 expand, rind on desktop: 66 ns, 1.00× the fastest HKDF-SHA256 expand, rind on nixos2: 300 ns, 1.00× the fastest -HKDF-SHA256 expand, rind on kixtop: 107 ns, 1.56× the fastest +HKDF-SHA256 expand, rind on kixtop: 107 ns, 1.56× the fastest; verified: 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 + HKDF-SHA256 expand, rind on ovh-iad: 540 ns, 1.00× the fastest HKDF-SHA256 expand, rind on ovh-sea: 464 ns, 1.00× the fastest -HKDF-SHA256 expand, rind (DIT held) on kixtop: 74 ns, 1.08× the fastest +HKDF-SHA256 expand, rind (DIT held) on kixtop: 74 ns, 1.08× the fastest; verified: 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 + HKDF-SHA256 expand, aws-lc-rs on nixos: 179 ns, 2.02× the fastest HKDF-SHA256 expand, aws-lc-rs on desktop: 124 ns, 1.88× the fastest HKDF-SHA256 expand, aws-lc-rs on nixos2: 636 ns, 2.12× the fastest diff --git a/benchmarks/verified.toml b/benchmarks/verified.toml index 2417c0857..35546b306 100644 --- a/benchmarks/verified.toml +++ b/benchmarks/verified.toml @@ -34,7 +34,8 @@ # graviola has none. Its X25519 and Ed25519 run only s2n-bignum's verified # routines, but convert between bytes and limbs in unverified Rust. # -# rind: X25519, P-256 ECDH and ECDSA on aarch64, and SHA-512 and Ed25519 +# rind: X25519, P-256 ECDH and ECDSA on aarch64, SHA-256, HMAC-SHA256, and +# HKDF-SHA256 on aarch64 with the crypto extension, and SHA-512 and Ed25519 # where the SHA-512 block routine's proof states the routine's result, whose # Rust `proofs/` proves against s2n-bignum's and aws-lc-verification's # theorems, ChaCha20 header protection, whose Rust `proofs/` proves against @@ -46,8 +47,9 @@ # state, and on x86_64 CPUs with AVX2, or AMD's, rind runs OpenSSL's or # aws-lc's unproven routines, which are faster there, so neither SHA-512 nor # Ed25519 earns the ✓ there. Every other rind operation runs unverified code, -# such as SHA-256's block function, under padding and HMAC glue that -# `proofs/` proves, or x86_64 P-256 ECDH's Jacobian-to-affine conversion. +# such as SHA-256's block function on x86_64 or without the crypto extension, +# under padding and HMAC glue that `proofs/` proves, or x86_64 P-256 ECDH's +# Jacobian-to-affine conversion. [[verified]] library = "rind" operations = ["x25519-ecdh"] @@ -108,6 +110,14 @@ arch = "aarch64" proof = "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" link = "https://github.com/moq-dev/rind/blob/main/proofs/Rind/Aarch64/P256Signature.lean" +[[verified]] +library = "rind" +operations = ["sha256/*", "hmac-sha256/*", "hkdf-sha256/*"] +arch = "aarch64" +cpu = ["aes", "pmull", "sha2"] +proof = "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" +link = "https://github.com/moq-dev/rind/blob/main/proofs/Rind/Aarch64/Sha256Hw.lean" + [[verified]] library = "rind" operations = ["quic-header-protection/chacha20"] diff --git a/proofs/README.md b/proofs/README.md index 56076e251..8a14ab4c4 100644 --- a/proofs/README.md +++ b/proofs/README.md @@ -30,6 +30,23 @@ hol-light` checks them alone, in nixpkgs' HOL Light. - `aarch64/bignum_eq.ml`: `BIGNUM_EQ_CORRECT`, s2n-bignum's proof of `bignum_eq` on the block in `low::aarch64::bignum_eq::bignum_eq`, which is s2n-bignum's routine without its `ret`. +- `aarch64/sha256_block_data_order_hw.ml`: `SHA256_HW_SUBROUTINE_CORRECT`, + rind's proof that the naked function + `low::aarch64::sha256::sha256_block_data_order_hw`, aws-lc's routine for + the SHA-256 instructions, computes s2n-bignum's FIPS 180-4 spec, + `sha256_hash_blocks`. A naked function's object code is its whole section + with its relocations and the read-only data they reach, here the round + constants, which `admin/prove` extracts as an object file; the proof checks + the constants against FIPS 180-4's. + +`hol-light/s2n-bignum/` holds, at their paths in s2n-bignum, the specs these +proofs need from s2n-bignum pull requests not yet merged, ahead of the +submodule on HOL Light's load path. Each is the pull request's file unchanged, +so a submodule bump past its merge deletes it: + +- `x86/proofs/utils/sha256_spec.ml`: SHA-256's, from + [awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415) at + `79120e64ed55e37c9652565ff272b7ef17f76738`. ## What is proven @@ -112,7 +129,7 @@ public key's is any point on the curve, so `p256_ecdsa_public_key_new` takes `P256_GROUP_ELEMENT_ORDER` proves from the group's size, which Mathlib cannot count yet. Key generation and signing need only G's order. The message's SHA-256 is FIPS 180-4's (`sha256E`), through the SHA-256 proof below, so -signing and verification take its `ShaBlocks` and messages of at most +signing and verification take its `Sha256Blocks` and messages of at most `maxInput` bytes. Signing draws nonces until r and s are both nonzero, with no bound, so `p256_ecdsa_sign` says what a returned signature is, not that one returns. The nonces come from RFC 6979's HMAC-DRBG, hedged @@ -155,13 +172,18 @@ against FIPS 180-4 and RFC 2104 as `Rind/HashSpec.lean` transliterates them: meeting `HashSpec`, and `hmac_sha256_sign`, `hmac_sha1_sign` over SHA-256 and SHA-1. -No proof covers a SHA-1 or SHA-256 block function rind runs on either target, -so these theorems take `ShaBlocks` as a hypothesis, in each target's own -`Rind//ShaBlocks.lean`: each routine computes FIPS 180-4's block -function, x86_64's SHA extensions' routines for SHA-1's padded last blocks -and SHA-256's finish pad, and SHA-256's encodes, as FIPS 180-4 does, and -rind's checks pass. They add no axiom, which -`Rind//HashAxioms.lean` checks. An input is at most `maxInput` +Below rind's padding, these theorems take `Sha1Blocks` or `Sha256Blocks` as +a hypothesis, in each target's own `Rind//ShaBlocks.lean`. No proof +covers a SHA-1 block function rind runs, or a SHA-256 one on x86_64, so there +each states that every routine computes FIPS 180-4's block function, x86_64's +SHA extensions' routines for SHA-1's padded last blocks and SHA-256's finish +pad, and SHA-256's encodes, as FIPS 180-4 does, and that rind's checks pass. +On aarch64, `Sha256Blocks` states only that the CPU has the crypto extension +and rind's checks pass: `Rind/Aarch64/Sha256Hw.lean` restates the HOL Light +proof above as the axiom `sha256_block_data_order_hw_spec`, and +`Rind/S2nSha256.lean` proves s2n-bignum's spec FIPS 180-4's block function. +`Rind//HashAxioms.lean` checks the axioms each theorem rests on: none +on x86_64, and that one for SHA-256 on aarch64. An input is at most `maxInput` (2^61 - 1) bytes, under FIPS 180-4's 2^64-bit limit. `Rind/HashSpecTest.lean` checks the transliterations against FIPS 180-4's, RFC 4231's, RFC 5869's, and RFC 6070's vectors. @@ -187,8 +209,8 @@ and RFC 8018 as `Rind/HashSpec.lean` transliterates them: into `Rind//Kdf/{Types,Funs}.lean`, with the first pass's items and the HMAC model opaque below it; `Rind/X86_64/HkdfExpand.lean` models `Prk::expand_into`, whose slice of borrowed slices Aeneas cannot translate. -The theorems over an HMAC algorithm assume `RunsHmac`: `ShaBlocks` for SHA-1 -and SHA-256, `RunsSha512` for SHA-384 and SHA-512, so `Rind//Axioms.lean` +The theorems over an HMAC algorithm assume `RunsHmac`: `Sha1Blocks` for SHA-1, +`Sha256Blocks` for SHA-256, and `RunsSha512` for SHA-384 and SHA-512, so `Rind//Axioms.lean` checks their axioms. `hmac::verify` and `Secret::verify` compare in constant time through inline assembly no Lean proof covers, so their theorems take `CtEqual` as a @@ -308,7 +330,8 @@ dispatch models' quotes, if it builds a digest `Algorithm` outside ## Layout -- `hol-light//`: rind's HOL Light proofs, one file per routine. +- `hol-light//`: rind's HOL Light proofs, one file per routine, and + `hol-light/s2n-bignum/`, the unmerged s2n-bignum specs they use. - `Rind//{Types,Funs}.lean`: Aeneas's translation, which `admin/prove` writes and git ignores. - `Rind//{Types,Funs}External.lean` and `Rind/Core.lean`: what the @@ -340,7 +363,9 @@ dispatch models' quotes, if it builds a digest `Algorithm` outside the AES-GCM proof, on x86_64 alone. - `Rind//ShaBlocks.lean`: SHA-1 and SHA-256's block functions on each target, SHA-1's padded last blocks, and SHA-256's padded last blocks and - finish. + finish; `Rind/Aarch64/Sha256Hw.lean`, the axiom for aarch64's routine with + the SHA-256 instructions, and `Rind/S2nSha256.lean`, s2n-bignum's SHA-256 + spec, transliterated, and its proof that it is `Rind/HashSpec.lean`'s. - `admin/prove` copies the other `Rind/X86_64/` models and proofs to `Rind/Aarch64/` with the target renamed. - `Rind/P256Group.lean`: that `p256` is prime, by a Pratt certificate, and @@ -379,7 +404,8 @@ Beyond Lean's kernel: `p256Pow`, and `p256Inv` in `Rind/Spec.lean` are trusted to be `weierstrass_add`, `group_pow`, and `ring_inv` on `p256_group`. - That `Rind/Sha2.lean` restates cryptol-specs' SHA-512 around - `processBlock_Common`. + `processBlock_Common`, and `Rind/S2nSha256.lean` transliterates + s2n-bignum's SHA-256 spec. - That `Rind/Spec.lean`'s ChaCha20 transliterates RFC 8439 and RFC 9001, its ECDSA FIPS 186-5, and `Rind/Ed25519.lean` RFC 8032 and s2n-bignum's encoding and decoding of diff --git a/proofs/Rind/Aarch64/Axioms.lean b/proofs/Rind/Aarch64/Axioms.lean index 34fc82a66..4b485ad59 100644 --- a/proofs/Rind/Aarch64/Axioms.lean +++ b/proofs/Rind/Aarch64/Axioms.lean @@ -96,47 +96,91 @@ A change here is a change to the trust base. #guard_msgs in #print axioms sha512_family_context -/-- info: 'rind.aarch64.key_new_spec' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.key_new_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms key_new_spec -/-- info: 'rind.aarch64.sign_spec' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.sign_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms sign_spec -/-- info: 'rind.aarch64.verify_spec' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.verify_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms verify_spec -/-- info: 'rind.aarch64.context_with_key_spec' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.context_with_key_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms context_with_key_spec -/-- info: 'rind.aarch64.context_update_spec'' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.context_update_spec'' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms context_update_spec' -/-- info: 'rind.aarch64.context_sign_spec' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.context_sign_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms context_sign_spec -/-- info: 'rind.aarch64.kdf.salt_extract_spec' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.kdf.salt_extract_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms kdf.salt_extract_spec -/-- info: 'rind.aarch64.kdf.okm_fill_spec' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.kdf.okm_fill_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms kdf.okm_fill_spec -/-- info: 'rind.aarch64.kdf.hkdf_fill' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.kdf.hkdf_fill' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms kdf.hkdf_fill -/-- info: 'rind.aarch64.kdf.derive_spec' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.kdf.derive_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms kdf.derive_spec -/-- info: 'rind.aarch64.kdf.verify_spec' depends on axioms: [propext, Classical.choice, Quot.sound, compress_nohw_spec] -/ +/-- info: 'rind.aarch64.kdf.verify_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + compress_nohw_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms kdf.verify_spec @@ -238,7 +282,8 @@ A change here is a change to the trust base. bignum_montmul_spec, bignum_montsqr_p256_spec, bignum_tomont_p256_spec, - p256_scalarmulbase_spec] -/ + p256_scalarmulbase_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms p256_ecdsa_sign @@ -273,7 +318,8 @@ A change here is a change to the trust base. p256_montjadd_spec, p256_montjdouble_spec, p256_montjmixadd_spec, - p256_scalarmulbase_spec] -/ + p256_scalarmulbase_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms p256_ecdsa_key_pair_verify @@ -294,6 +340,7 @@ A change here is a change to the trust base. bignum_tomont_p256_spec, p256_montjadd_spec, p256_montjdouble_spec, - p256_montjmixadd_spec] -/ + p256_montjmixadd_spec, + sha256_block_data_order_hw_spec] -/ #guard_msgs in #print axioms p256_ecdsa_public_key_new diff --git a/proofs/Rind/Aarch64/FunsExternal.lean b/proofs/Rind/Aarch64/FunsExternal.lean index 189e3d124..ecc6d71df 100644 --- a/proofs/Rind/Aarch64/FunsExternal.lean +++ b/proofs/Rind/Aarch64/FunsExternal.lean @@ -220,14 +220,24 @@ opaque low.entry.Entry.assert_held : Result Unit opaque low.aarch64.cpu.HaveSha3.check : Result (Option low.aarch64.cpu.HaveSha3) -/-! SHA-1 and SHA-256's block functions, whose contracts `Rind.Aarch64.ShaBlocks` -states as hypotheses. Each picks between aws-lc's routines by the CPU through -raw pointers, which Aeneas cannot translate. -/ +opaque low.aarch64.cpu.HaveCryptoExt.check : Result (Option low.aarch64.cpu.HaveCryptoExt) + +/-! SHA-1's block function, whose contract `Rind.Aarch64.ShaBlocks` states as a +hypothesis. It picks between aws-lc's routines by the CPU through raw +pointers, which Aeneas cannot translate. -/ opaque low.aarch64.sha1.sha1_compress_blocks : Array Std.U32 5#usize → Slice Std.U8 → Result (Array Std.U32 5#usize) -opaque low.aarch64.sha256.sha256_compress_blocks +/-! aws-lc's SHA-256 routines, behind their Rust wrappers. `Rind.Aarch64.Sha256Hw` +states the first's contract, rind's HOL Light proof's theorem. -/ + +opaque low.aarch64.sha256.compress_hw + : + low.aarch64.cpu.HaveCryptoExt → Array Std.U32 8#usize → Slice Std.U8 → Result + (Array Std.U32 8#usize) + +opaque low.aarch64.sha256.compress_nohw : Array Std.U32 8#usize → Slice Std.U8 → Result (Array Std.U32 8#usize) /-! The other curves, which X25519's and P-256's results never depend on. -/ diff --git a/proofs/Rind/Aarch64/HashAxioms.lean b/proofs/Rind/Aarch64/HashAxioms.lean new file mode 100644 index 000000000..ed0695e89 --- /dev/null +++ b/proofs/Rind/Aarch64/HashAxioms.lean @@ -0,0 +1,68 @@ +import Rind.Aarch64.Hmac +import Rind.Aarch64.DigestApi +open rind.aarch64 + +/-! +The axioms the SHA-1, SHA-256, HMAC, and digest API theorems rest on, beyond +Lean's own. SHA-1's block function's contract is `Sha1Blocks`, a hypothesis of +each theorem. SHA-256's is `Sha256Blocks`, which only asks that the CPU has the +crypto extension, and whose theorem rests on `sha256_block_data_order_hw_spec`, +rind's HOL Light proof of the routine. `Axioms` pins the theorems over every +HMAC algorithm, which rest on SHA-512's too. A change here is a change to the +trust base. `admin/prove` copies the files beside it from x86_64's, but not +this one, since aarch64's SHA-256 theorems rest on an axiom x86_64's do not. +-/ + +/-- info: 'rind.aarch64.sha256_hash' depends on axioms: [propext, Classical.choice, Quot.sound, sha256_block_data_order_hw_spec] -/ +#guard_msgs in +#print axioms sha256_hash + +/-- info: 'rind.aarch64.sha1_hash' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms sha1_hash + +/-- info: 'rind.aarch64.hmac_sha256_sign' depends on axioms: [propext, + Classical.choice, + Quot.sound, + sha256_block_data_order_hw_spec] -/ +#guard_msgs in +#print axioms hmac_sha256_sign + +/-- info: 'rind.aarch64.hmac_sha1_sign' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms hmac_sha1_sign + +/-- info: 'rind.aarch64.hmac_start_spec' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms hmac_start_spec + +/-- info: 'rind.aarch64.hmac_update_spec' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms hmac_update_spec + +/-- info: 'rind.aarch64.hmac_finish_spec' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms hmac_finish_spec + +/-- info: 'rind.aarch64.digest_spec' depends on axioms: [propext, Classical.choice, Quot.sound, sha256_block_data_order_hw_spec] -/ +#guard_msgs in +#print axioms digest_spec + +/-- info: 'rind.aarch64.digest_ctx_new_spec' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in +#print axioms digest_ctx_new_spec + +/-- info: 'rind.aarch64.digest_ctx_update_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + sha256_block_data_order_hw_spec] -/ +#guard_msgs in +#print axioms digest_ctx_update_spec + +/-- info: 'rind.aarch64.digest_ctx_finish_spec' depends on axioms: [propext, + Classical.choice, + Quot.sound, + sha256_block_data_order_hw_spec] -/ +#guard_msgs in +#print axioms digest_ctx_finish_spec + diff --git a/proofs/Rind/Aarch64/P256Signature.lean b/proofs/Rind/Aarch64/P256Signature.lean index 9f15bc2d0..09c2e4d3f 100644 --- a/proofs/Rind/Aarch64/P256Signature.lean +++ b/proofs/Rind/Aarch64/P256Signature.lean @@ -324,7 +324,7 @@ def sha256E (msg : List U8) : Nat := /-- The digest the ECDSA layer hashes `msg` to, given the block functions' contracts, encodes `sha256E`'s integer. -/ -theorem ecdsa_sha256_spec (hsha : ShaBlocks) (msg : Slice U8) (hm : msg.length ≤ maxInput) : +theorem ecdsa_sha256_spec (hsha : Sha256Blocks) (msg : Slice U8) (hm : msg.length ≤ maxInput) : ∃ d dg, Sha256Sig.HashInst.hash msg = ok d ∧ high.digest.Digest.Insts.CoreConvertAsRefSliceU8.as_ref d = ok dg ∧ 32 ≤ dg.length ∧ beNat (dg.val.take 32) % n256 = sha256E msg.val := by @@ -412,7 +412,7 @@ nonce in [1, n), neither zero. Signing is refused only if the nonce's random input cannot be drawn. The nonces, RFC 6979's hedged with that input, are outside the functional spec. -/ theorem p256_ecdsa_sign (h : Runs) (hdrbg : Drbg) (hfill : Fills) - (hsha : ShaBlocks) (kp : high.signature.EcdsaKeyPair) (d : Nat) (hkp : EcdsaKeyPairOf kp d) + (hsha : Sha256Blocks) (kp : high.signature.EcdsaKeyPair) (d : Nat) (hkp : EcdsaKeyPairOf kp d) (msg : Slice U8) (hm : msg.length ≤ maxInput) : high.signature.EcdsaKeyPair.sign kp msg ⦃ r => (∀ sig, r = .Ok sig → high.signature.Signature.Insts.CoreConvertAsRefSliceU8.as_ref sig ⦃ b => @@ -517,7 +517,7 @@ theorem p256_ecdsa_key_pair_public_key (h : Runs) (hheld : Held) (hc : Cached) /-- Verification with a key pair's public key: ECDSA's verification of `msg`'s SHA-256 under its scalar times the generator. -/ theorem p256_ecdsa_key_pair_verify (h : Runs) (hheld : Held) (hc : Cached) - (hsha : ShaBlocks) (kp : high.signature.EcdsaKeyPair) (d : Nat) (hkp : EcdsaKeyPairOf kp d) + (hsha : Sha256Blocks) (kp : high.signature.EcdsaKeyPair) (d : Nat) (hkp : EcdsaKeyPairOf kp d) (msg sig : Slice U8) (hm : msg.length ≤ maxInput) : (do let pk ← high.signature.EcdsaKeyPair.impl.public_key kp @@ -540,7 +540,7 @@ theorem p256_ecdsa_key_pair_verify (h : Runs) (hheld : Held) (hc : Cached) X9.62 uncompressed point on the curve, and otherwise its verification is ECDSA's of a message's SHA-256 under that point. -/ theorem p256_ecdsa_public_key_new (ho : P256Order) (h : Runs) (hheld : Held) (hc : Cached) - (hsha : ShaBlocks) (bytes : Slice U8) : + (hsha : Sha256Blocks) (bytes : Slice U8) : high.signature.PublicKey.new high.signature.verify.ECDSA_P256_SHA256_FIXED bytes ⦃ r => x962Outcome bytes.val (fun pk => ∀ (msg sig : Slice U8), msg.length ≤ maxInput → high.signature.PublicKey.verify pk msg sig ⦃ v => diff --git a/proofs/Rind/Aarch64/Sha256Hw.lean b/proofs/Rind/Aarch64/Sha256Hw.lean new file mode 100644 index 000000000..19a8e73ac --- /dev/null +++ b/proofs/Rind/Aarch64/Sha256Hw.lean @@ -0,0 +1,60 @@ +import Rind.Aarch64.Blockwise +import Rind.S2nSha256 +import Rind.Sha2Lemmas +open Aeneas Aeneas.Std Result rind.spec + +/-! +# SHA-256's block function with the crypto extension on aarch64 + +rind's HOL Light proof `SHA256_HW_SUBROUTINE_CORRECT`, in +`proofs/hol-light/aarch64/sha256_block_data_order_hw.ml` at rind's commit, +that rind's naked function `sha256_block_data_order_hw`, as rind's build +emits it, computes s2n-bignum's `sha256_hash_blocks`, restated as an axiom +about the Rust wrapper `compress_hw` around it. `admin/prove` checks the HOL +Light proof against the object code rind's release build emits, its +instructions, relocations, and the `K256` table they read. + +The theorem's hypotheses hold for every call `compress_hw`'s safety contract +allows: `state` and `blocks` are distinct allocations, neither overlapping the +code, the table, or the 16 bytes below the stack pointer the routine saves its +frame to; `blocks` is a whole number of blocks, at least one and, as a slice, +fewer than 2^64; the linker places the table within the reach of the `adrp` +that addresses it; and the ABI keeps the stack pointer 16-byte aligned. The +restatement, and that the wrapper passes the pointers and block count the +theorem names, are trusted. + +`S2nSha256` proves s2n-bignum's spec FIPS 180-4's, as `Rind.HashSpec` states +it, so the dispatch meets `Compresses` wherever the CPU has the extension. +-/ + +namespace rind.aarch64 + +/-- `SHA256_HW_SUBROUTINE_CORRECT`: for `n` blocks, at least one, whose `i`th +block's `j`th word, read big-endian, is the `j`th word of `m i`, the state's +eight words, read little-endian, become `sha256_hash_blocks m state n`. -/ +@[step] +axiom sha256_block_data_order_hw_spec (c : low.aarch64.cpu.HaveCryptoExt) + (state : Std.Array U32 8#usize) (blocks : Slice U8) + (hm : blocks.length % 64 = 0) (hn : blocks.length ≠ 0) : + low.aarch64.sha256.compress_hw c state blocks ⦃ r => + words r.val = s2n.hashBlocks (fun i => rind.spec.words (((bv blocks.val).drop (64 * i)).take 64)) + (words state.val) (blocks.length / 64) ⦄ + +/-- The dispatch, on a CPU with the crypto extension, compresses every whole +block, and returns the state for none. -/ +theorem sha256_compress_blocks_hw_spec (hc : ∃ c, low.aarch64.cpu.HaveCryptoExt.check = ok (some c)) : + Compresses sha256.compress low.aarch64.sha256.sha256_compress_blocks := by + intro h s hl + obtain ⟨c, hc⟩ := hc + unfold low.aarch64.sha256.sha256_compress_blocks + step* + · have hs : s.val = [] := by + rw [← List.length_eq_zero_iff]; simp_all + rw [hs, show bv ([] : List U8) = [] from rfl, blocks] + simp + · rw [hc] + step with sha256_block_data_order_hw_spec as ⟨r, hr⟩ + rw [hr] + simpa [bv] using s2n.hashBlocks_eq (words h.val) (by simp [words]) (bv s.val) + +end rind.aarch64 diff --git a/proofs/Rind/Aarch64/ShaBlocks.lean b/proofs/Rind/Aarch64/ShaBlocks.lean index 3a932c401..ffb113e12 100644 --- a/proofs/Rind/Aarch64/ShaBlocks.lean +++ b/proofs/Rind/Aarch64/ShaBlocks.lean @@ -1,34 +1,48 @@ -import Rind.Aarch64.Blockwise +import Rind.Aarch64.Sha256Hw open Aeneas Aeneas.Std Result rind.spec /-! # SHA-1 and SHA-256's block functions on aarch64 -No proof covers aws-lc's SHA-1 or SHA-256 routines that aarch64 runs, so the -theorems over them take `ShaBlocks` as a hypothesis instead of an axiom, as on -x86_64. `Rind.X86_64.ShaBlocks` states the same names for x86_64. +No proof covers aws-lc's SHA-1 routines that aarch64 runs, so the theorems +over them take `Sha1Blocks` as a hypothesis instead of an axiom, as on x86_64. +SHA-256's routine for the crypto extension is proven, `Rind.Aarch64.Sha256Hw`, +so the SHA-256 theorems take `Sha256Blocks`, only that the CPU has it. +`Rind.X86_64.ShaBlocks` states the same names for x86_64. -/ namespace rind.aarch64 -/-- What the SHA-1 and SHA-256 theorems assume of the code below rind's -padding on aarch64: each routine computes FIPS 180-4's block function, and -the entry checks pass. None reads an input. -/ -structure ShaBlocks : Prop where +/-- What the SHA-1 theorems assume of the code below rind's padding on +aarch64: the routine computes FIPS 180-4's block function, and the entry +checks pass. None reads an input. -/ +structure Sha1Blocks : Prop where entry : ∃ e, low.entry.Entry.new_secret = ok e held : low.entry.Entry.assert_held = ok () sha1 : Compresses sha1.compress low.aarch64.sha1.sha1_compress_blocks - sha256 : Compresses sha256.compress low.aarch64.sha256.sha256_compress_blocks + +/-- What the SHA-256 theorems assume on aarch64: the CPU has the crypto +extension, so rind runs the proven routine, and the entry checks pass. None +reads an input. -/ +structure Sha256Blocks : Prop where + entry : ∃ e, low.entry.Entry.new_secret = ok e + held : low.entry.Entry.assert_held = ok () + crypto : ∃ c, low.aarch64.cpu.HaveCryptoExt.check = ok (some c) + +/-- SHA-256's block function, the dispatch to the proven routine. -/ +theorem Sha256Blocks.sha256 (hb : Sha256Blocks) : + Compresses sha256.compress low.aarch64.sha256.sha256_compress_blocks := + sha256_compress_blocks_hw_spec hb.crypto /-- SHA-256's block function as `Sha256State` calls it. -/ -theorem sha256_block_spec (hb : ShaBlocks) : Compresses sha256.compress mid.sha2.Sha256State.compress := by +theorem sha256_block_spec (hb : Sha256Blocks) : Compresses sha256.compress mid.sha2.Sha256State.compress := by intro h b hl unfold mid.sha2.Sha256State.compress rw [hb.held] simpa using hb.sha256 h b hl /-- SHA-1's block function as `Sha1State` calls it. -/ -theorem sha1_block_spec (hb : ShaBlocks) : +theorem sha1_block_spec (hb : Sha1Blocks) : Compresses sha1.compress mid.sha1.Sha1State.compress := by intro h b hl unfold mid.sha1.Sha1State.compress @@ -36,7 +50,7 @@ theorem sha1_block_spec (hb : ShaBlocks) : simpa using hb.sha1 h b hl /-- SHA-1's padded last blocks. -/ -theorem sha1_compress_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std.Array U32 5#usize) +theorem sha1_compress_padded_spec (hb : Sha1Blocks) (P : List U8) (state : Std.Array U32 5#usize) (message : Slice U8) (length : Std.Array U8 8#usize) (hR : Absorbed sha1.compress sha1.H0 P state) : low.aarch64.sha1.sha1_compress_padded state message length ⦃ h' => @@ -59,7 +73,7 @@ theorem sha1_compress_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std.Ar omega) /-- SHA-256's padded last blocks. -/ -theorem sha256_compress_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std.Array U32 8#usize) +theorem sha256_compress_padded_spec (hb : Sha256Blocks) (P : List U8) (state : Std.Array U32 8#usize) (message : Slice U8) (length : Std.Array U8 8#usize) (hR : Absorbed sha256.compress sha256.H0 P state) : low.aarch64.sha256.sha256_compress_padded state message length ⦃ h' => @@ -97,7 +111,7 @@ theorem sha256_compress_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std. exact tail bl re ⟨hs1, hs2, hs3, hs4⟩ /-- SHA-256's digest of what `state` has absorbed followed by `message`. -/ -theorem sha256_finish_spec (hb : ShaBlocks) (P : List U8) (state : Std.Array U32 8#usize) +theorem sha256_finish_spec (hb : Sha256Blocks) (P : List U8) (state : Std.Array U32 8#usize) (message : Slice U8) (length : Std.Array U8 8#usize) (hR : Absorbed sha256.compress sha256.H0 P state) : low.aarch64.sha256.sha256_finish state message length ⦃ r => diff --git a/proofs/Rind/Aarch64/TypesExternal.lean b/proofs/Rind/Aarch64/TypesExternal.lean index 77713288a..5410df378 100644 --- a/proofs/Rind/Aarch64/TypesExternal.lean +++ b/proofs/Rind/Aarch64/TypesExternal.lean @@ -18,6 +18,10 @@ opaque low.entry.Entry : Type /-- The token proving the CPU has the SHA-512 instructions. -/ opaque low.aarch64.cpu.HaveSha3 : Type +/-- The token proving the CPU has the crypto extension's instructions, SHA-256's +among them. -/ +opaque low.aarch64.cpu.HaveCryptoExt : Type + /-- A value its owner builds once and keeps, whose atomics Aeneas cannot translate. -/ opaque low.generic.reuse_cache.ReuseCache (T : Type) : Type diff --git a/proofs/Rind/S2nSha256.lean b/proofs/Rind/S2nSha256.lean new file mode 100644 index 000000000..9e141ddaf --- /dev/null +++ b/proofs/Rind/S2nSha256.lean @@ -0,0 +1,221 @@ +import Rind.HashSpec +open rind.spec + +/-! +# s2n-bignum's SHA-256 spec + +s2n-bignum's FIPS 180-4 spec of SHA-256's block function, from +`x86/proofs/utils/sha256_spec.ml` in awslabs/s2n-bignum#415 at 79120e64, +which `proofs/hol-light/s2n-bignum/` holds, and `arm/proofs/sha256.ml`'s round +functions it reuses, transliterated: HOL Light's `EL n l` is `l[n]!`, `word_ror` +is `rotateRight`, `word_ushr` is `>>>`, and `word_add` is `+`, each grouped as +the HOL Light is. The theorems rind's HOL Light proofs state are about these, +and `block_words` proves this block function is `Rind.HashSpec`'s. +-/ + +namespace rind.spec.s2n + +/-- `sha_msg_sigma_0`. -/ +def msgSigma0 (x : BitVec 32) : BitVec 32 := x.rotateRight 7 ^^^ (x.rotateRight 18 ^^^ x >>> 3) +/-- `sha_msg_sigma_1`. -/ +def msgSigma1 (x : BitVec 32) : BitVec 32 := x.rotateRight 17 ^^^ (x.rotateRight 19 ^^^ x >>> 10) +/-- `sha_choose`. -/ +def choose (x y z : BitVec 32) : BitVec 32 := ((y ^^^ z) &&& x) ^^^ z +/-- `sha_maj`. -/ +def maj (x y z : BitVec 32) : BitVec 32 := (x &&& y) ||| ((x ||| y) &&& z) +/-- `sha_hash_sigma_0`. -/ +def hashSigma0 (x : BitVec 32) : BitVec 32 := x.rotateRight 2 ^^^ (x.rotateRight 13 ^^^ x.rotateRight 22) +/-- `sha_hash_sigma_1`. -/ +def hashSigma1 (x : BitVec 32) : BitVec 32 := x.rotateRight 6 ^^^ (x.rotateRight 11 ^^^ x.rotateRight 25) + +/-- `sha256_constants`. -/ +def constants : List (BitVec 32) := + [0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5, + 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174, + 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da, + 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967, + 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85, + 0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070, + 0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3, + 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2] + +/-- `sha256_msg_schedule`. -/ +def msgSchedule (m : List (BitVec 32)) (t : Nat) : BitVec 32 := + if t < 16 then m[t]! + else msgSigma1 (msgSchedule m (t - 2)) + msgSchedule m (t - 7) + + (msgSigma0 (msgSchedule m (t - 15)) + msgSchedule m (t - 16)) +termination_by t +decreasing_by all_goals omega + +/-- `sha256_round`. -/ +def round (hsh : List (BitVec 32)) (k w : BitVec 32) : List (BitVec 32) := + let a := hsh[0]!; let b := hsh[1]!; let c := hsh[2]!; let d := hsh[3]! + let e := hsh[4]!; let f := hsh[5]!; let g := hsh[6]!; let h := hsh[7]! + let t1 := h + (hashSigma1 e + (choose e f g + (k + w))) + let t2 := hashSigma0 a + maj a b c + [t1 + t2, a, b, c, d + t1, e, f, g] + +/-- `sha256_compress_rounds`. -/ +def compressRounds (m hsh : List (BitVec 32)) : Nat → List (BitVec 32) + | 0 => hsh + | n + 1 => round (compressRounds m hsh n) constants[n]! (msgSchedule m n) + +/-- `sha256_block`. -/ +def block (m hsh : List (BitVec 32)) : List (BitVec 32) := + let res := compressRounds m hsh 64 + [res[0]! + hsh[0]!, res[1]! + hsh[1]!, res[2]! + hsh[2]!, res[3]! + hsh[3]!, + res[4]! + hsh[4]!, res[5]! + hsh[5]!, res[6]! + hsh[6]!, res[7]! + hsh[7]!] + +/-- `sha256_hash_blocks`. -/ +def hashBlocks (m : Nat → List (BitVec 32)) (hsh : List (BitVec 32)) : Nat → List (BitVec 32) + | 0 => hsh + | n + 1 => block (m n) (hashBlocks m hsh n) + +/-! The bridge to `Rind.HashSpec`. -/ + +theorem constants_eq : constants = sha256.K := rfl + +theorem choose_eq (x y z : BitVec 32) : choose x y z = ch x y z := by + unfold choose ch; ext i hi; simp; cases x[i] <;> cases y[i] <;> cases z[i] <;> rfl + +theorem maj_eq (x y z : BitVec 32) : maj x y z = rind.spec.maj x y z := by + unfold maj rind.spec.maj; ext i hi; simp; cases x[i] <;> cases y[i] <;> cases z[i] <;> rfl + +theorem msgSigma0_eq (x : BitVec 32) : msgSigma0 x = sha256.smallSigma0 x := by + simp only [msgSigma0, sha256.smallSigma0, BitVec.xor_assoc] + +theorem msgSigma1_eq (x : BitVec 32) : msgSigma1 x = sha256.smallSigma1 x := by + simp only [msgSigma1, sha256.smallSigma1, BitVec.xor_assoc] + +theorem hashSigma0_eq (x : BitVec 32) : hashSigma0 x = sha256.bigSigma0 x := by + simp only [hashSigma0, sha256.bigSigma0, BitVec.xor_assoc] + +theorem hashSigma1_eq (x : BitVec 32) : hashSigma1 x = sha256.bigSigma1 x := by + simp only [hashSigma1, sha256.bigSigma1, BitVec.xor_assoc] + +theorem msgSchedule_lt (m : List (BitVec 32)) {t : Nat} (ht : t < 16) : msgSchedule m t = m[t]! := by + rw [msgSchedule]; simp [ht] + +theorem msgSchedule_add16 (m : List (BitVec 32)) (t : Nat) : + msgSchedule m (t + 16) = sha256.smallSigma1 (msgSchedule m (t + 14)) + msgSchedule m (t + 9) + + sha256.smallSigma0 (msgSchedule m (t + 1)) + msgSchedule m t := by + rw [msgSchedule] + simp only [show ¬ t + 16 < 16 by omega, ite_false, show t + 16 - 2 = t + 14 by omega, + show t + 16 - 7 = t + 9 by omega, show t + 16 - 15 = t + 1 by omega, + show t + 16 - 16 = t by omega, msgSigma0_eq, msgSigma1_eq, BitVec.add_assoc] + +/-- The first `16 + k` words of `Rind.HashSpec`'s schedule, after `k` of its +steps, are `msgSchedule`'s. -/ +theorem schedule_prefix (M : List (BitVec 32)) (hM : M.length = 16) (k : Nat) (hk : k ≤ 48) : + let W := (List.range k).foldl + (fun W t => W ++ [sha256.smallSigma1 W[t + 14]! + W[t + 9]! + sha256.smallSigma0 W[t + 1]! + W[t]!]) M + W.length = 16 + k ∧ ∀ t < 16 + k, W[t]! = msgSchedule M t := by + induction k with + | zero => + refine ⟨by simpa using hM, fun t ht => ?_⟩ + simp [msgSchedule_lt M (show t < 16 by omega)] + | succ k ih => + obtain ⟨hl, hW⟩ := ih (by omega) + simp only [List.range_succ, List.foldl_append, List.foldl_cons, List.foldl_nil] + generalize hX : (List.range k).foldl _ M = X at hl hW + refine ⟨by simp [hl]; omega, fun t ht => ?_⟩ + rcases Nat.lt_or_ge t (16 + k) with h | h + · rw [← hW t h] + simp [List.getElem!_eq_getElem?_getD, List.getElem?_append_left (show t < X.length by omega)] + · have ht' : t = k + 16 := by omega + subst ht' + have last : ∀ v : BitVec 32, (X ++ [v])[k + 16]! = v := fun v => by + simp [show k + 16 = X.length by omega] + rw [last, msgSchedule_add16, hW _ (by omega), hW _ (by omega), hW _ (by omega), hW _ (by omega)] + +theorem schedule_getElem (M : List (BitVec 32)) (hM : M.length = 16) {t : Nat} (ht : t < 64) : + (sha256.schedule M)[t]! = msgSchedule M t := + (schedule_prefix M hM 48 le_rfl).2 t ht + +/-- `Rind.HashSpec`'s round is `round`. -/ +theorem round_eq (s : List (BitVec 32)) (k w : BitVec 32) : + (let T1 := s[7]! + sha256.bigSigma1 s[4]! + ch s[4]! s[5]! s[6]! + k + w + let T2 := sha256.bigSigma0 s[0]! + rind.spec.maj s[0]! s[1]! s[2]! + [T1 + T2, s[0]!, s[1]!, s[2]!, s[3]! + T1, s[4]!, s[5]!, s[6]!]) = round s k w := by + simp only [round, choose_eq, maj_eq, hashSigma0_eq, hashSigma1_eq, BitVec.add_assoc] + +theorem rounds_eq (M H : List (BitVec 32)) (hM : M.length = 16) (n : Nat) (hn : n ≤ 64) : + (List.range n).foldl (fun (s : List (BitVec 32)) t => + let T1 := s[7]! + sha256.bigSigma1 s[4]! + ch s[4]! s[5]! s[6]! + sha256.K[t]! + + (sha256.schedule M)[t]! + let T2 := sha256.bigSigma0 s[0]! + rind.spec.maj s[0]! s[1]! s[2]! + [T1 + T2, s[0]!, s[1]!, s[2]!, s[3]! + T1, s[4]!, s[5]!, s[6]!]) H = + compressRounds M H n := by + induction n with + | zero => rfl + | succ n ih => + rw [List.range_succ, List.foldl_append, ih (by omega), List.foldl_cons, List.foldl_nil, + compressRounds, schedule_getElem M hM (by omega), ← constants_eq] + exact round_eq _ _ _ + +theorem length_round (s : List (BitVec 32)) (k w : BitVec 32) : (round s k w).length = 8 := rfl + +theorem length_compressRounds (M H : List (BitVec 32)) (hH : H.length = 8) (n : Nat) : + (compressRounds M H n).length = 8 := by + cases n with + | zero => exact hH + | succ n => exact length_round _ _ _ + +/-- s2n-bignum's block function is `Rind.HashSpec`'s, on a 64-byte block and +an 8-word hash value. -/ +theorem block_words (H : List (BitVec 32)) (b : List Byte) (hH : H.length = 8) (hb : b.length = 64) : + block (words b) H = sha256.compress H b := by + have hM : (words b).length = 16 := by simp [words, hb] + have hR := length_compressRounds (words b) H hH 64 + rw [sha256.compress] + simp only + rw [rounds_eq (words b) H hM 64 le_rfl, block] + generalize compressRounds (words b) H 64 = R at * + match R, H, hR, hH with + | [r0, r1, r2, r3, r4, r5, r6, r7], [h0, h1, h2, h3, h4, h5, h6, h7], _, _ => rfl + +/-- `Rind.HashSpec`'s blocks of `bytes`, by index. -/ +theorem blocks_eq (bytes : List Byte) : + blocks 64 bytes = (List.range (bytes.length / 64)).map fun i => (bytes.drop (64 * i)).take 64 := by + induction h : bytes.length using Nat.strong_induction_on generalizing bytes with + | _ n ih => + subst h + rw [blocks] + by_cases hl : 64 ≤ bytes.length + · rw [ite_eq_left ⟨by decide, hl⟩, show bytes.length / 64 = (bytes.length - 64) / 64 + 1 by omega, + List.range_succ_eq_map, List.map_cons, List.map_map, + ih (bytes.length - 64) (by omega) (bytes.drop 64) (by simp)] + simp only [Nat.mul_zero, List.drop_zero, List.cons.injEq, true_and] + apply List.map_congr_left + intro i _ + simp [List.drop_drop, Nat.mul_succ, Nat.add_comm] + · rw [ite_eq_right (fun h => hl h.2), show bytes.length / 64 = 0 by omega] + rfl + +theorem length_hashBlocks (m : Nat → List (BitVec 32)) (H : List (BitVec 32)) (hH : H.length = 8) + (n : Nat) : (hashBlocks m H n).length = 8 := by + cases n with + | zero => exact hH + | succ n => rfl + +/-- s2n-bignum's hash of `n` blocks, the `i`th of which is the `i`th 64 bytes +of `bytes` as big-endian words, is `Rind.HashSpec`'s. -/ +theorem hashBlocks_eq (H : List (BitVec 32)) (hH : H.length = 8) (bytes : List Byte) : + hashBlocks (fun i => words ((bytes.drop (64 * i)).take 64)) H (bytes.length / 64) = + (blocks 64 bytes).foldl sha256.compress H := by + rw [blocks_eq] + suffices ∀ n ≤ bytes.length / 64, + hashBlocks (fun i => words ((bytes.drop (64 * i)).take 64)) H n = + ((List.range n).map fun i => (bytes.drop (64 * i)).take 64).foldl sha256.compress H from + this _ le_rfl + intro n hn + induction n with + | zero => rfl + | succ n ih => + rw [hashBlocks, ih (by omega), List.range_succ, List.map_append, List.foldl_append, List.map_cons, + List.map_nil, List.foldl_cons, List.foldl_nil, ← ih (by omega)] + apply block_words _ _ (length_hashBlocks _ _ hH _) + simp only [List.length_take, List.length_drop] + omega + +end rind.spec.s2n diff --git a/proofs/Rind/X86_64/DigestApi.lean b/proofs/Rind/X86_64/DigestApi.lean index 39731aa9f..bedeb52c7 100644 --- a/proofs/Rind/X86_64/DigestApi.lean +++ b/proofs/Rind/X86_64/DigestApi.lean @@ -70,10 +70,16 @@ def digestHash : high.digest.Algorithm → List Byte → List Byte | .SHA1 => sha1.hash | _ => sha256.hash +/-- What `a`'s hash assumes of its block functions. -/ +def ShaBlocksOf : high.digest.Algorithm → Prop + | .SHA1 => Sha1Blocks + | .SHA256 => Sha256Blocks + | _ => True + /-- What the digest API under `a` needs: `a` is SHA-1 or SHA-256, the entry -guard passes, and the block functions meet their contracts. -/ +guard passes, and its block functions meet their contracts. -/ def RunsDigest (a : high.digest.Algorithm) : Prop := - (a = .SHA1 ∨ a = .SHA256) ∧ (∃ e, low.entry.Entry.new_secret = ok e) ∧ ShaBlocks + (a = .SHA1 ∨ a = .SHA256) ∧ (∃ e, low.entry.Entry.new_secret = ok e) ∧ ShaBlocksOf a /-- `c` is a `Context` of `a` that has been given `p`. -/ def CtxOf (a : high.digest.Algorithm) (p : List U8) : high.digest.State → Prop diff --git a/proofs/Rind/X86_64/FunsExternal.lean b/proofs/Rind/X86_64/FunsExternal.lean index f73e5d94a..1e79971b8 100644 --- a/proofs/Rind/X86_64/FunsExternal.lean +++ b/proofs/Rind/X86_64/FunsExternal.lean @@ -251,7 +251,7 @@ opaque low.x86_64.sha1_mux.path : Result low.x86_64.sha1_mux.Path opaque low.x86_64.sha256_mux.path : Result low.x86_64.sha256_mux.Path /-! SHA-1 and SHA-256's block and finishing functions, whose contracts `Rind.X86_64.ShaBlocks` -states as hypotheses. SHA-1's block function is its whole dispatch, which `ShaBlocks` states +states as hypotheses. SHA-1's block function is its whole dispatch, which `Sha1Blocks` states as one. -/ opaque low.x86_64.sha1_mux.sha1_compress_blocks diff --git a/proofs/Rind/X86_64/HashAxioms.lean b/proofs/Rind/X86_64/HashAxioms.lean index c5b30b391..183476cad 100644 --- a/proofs/Rind/X86_64/HashAxioms.lean +++ b/proofs/Rind/X86_64/HashAxioms.lean @@ -4,8 +4,8 @@ open rind.x86_64 /-! The axioms the SHA-1, SHA-256, HMAC, and digest API theorems rest on, beyond -Lean's own: none. The block functions' contracts are `ShaBlocks`, a hypothesis -of each theorem. `Axioms` pins the theorems over every HMAC algorithm, which +Lean's own: none. The block functions' contracts are `Sha1Blocks` and +`Sha256Blocks`, a hypothesis of each theorem. `Axioms` pins the theorems over every HMAC algorithm, which rest on SHA-512's. A change here is a change to the trust base. -/ diff --git a/proofs/Rind/X86_64/Hmac.lean b/proofs/Rind/X86_64/Hmac.lean index 868e6ff2a..51f8fbac9 100644 --- a/proofs/Rind/X86_64/Hmac.lean +++ b/proofs/Rind/X86_64/Hmac.lean @@ -7,7 +7,7 @@ open Aeneas Aeneas.Std Result rind.spec `HmacKey` and `Hmac` compute RFC 2104's HMAC, as HACL*'s `Spec.Agile.HMAC` states it, over any hash whose `Hash` impl meets `HashSpec`: SHA-1's and -SHA-256's do, given `ShaBlocks`. +SHA-256's do, given `Sha1Blocks` and `Sha256Blocks`. -/ namespace rind.x86_64 @@ -358,18 +358,18 @@ end /-! ## SHA-1, SHA-256, and HMAC over them -/ /-- SHA-256 of a message is FIPS 180-4's, given the block functions' contracts. -/ -theorem sha256_hash (hb : ShaBlocks) (m : Slice U8) (hm : m.length ≤ maxInput) : +theorem sha256_hash (hb : Sha256Blocks) (m : Slice U8) (hm : m.length ≤ maxInput) : Sha256Hash.hash m ⦃ d => digestBytes d = sha256.hash (bv m.val) ⦄ := WP.spec_mono ((sha256_hashSpec hb).hash_spec m hm) fun _ h => h.2 /-- SHA-1 of a message is FIPS 180-4's, given the block functions' contracts. -/ -theorem sha1_hash (hb : ShaBlocks) (m : Slice U8) (hm : m.length ≤ maxInput) : +theorem sha1_hash (hb : Sha1Blocks) (m : Slice U8) (hm : m.length ≤ maxInput) : Sha1Hash.hash m ⦃ d => digestBytes d = sha1.hash (bv m.val) ⦄ := WP.spec_mono ((sha1_hashSpec hb).hash_spec m hm) fun _ h => h.2 /-- HMAC-SHA256's tag of `m` under `key` is RFC 2104's, given the block functions' contracts. -/ -theorem hmac_sha256_sign (hb : ShaBlocks) (key m : Slice U8) (hk : key.length ≤ maxInput) +theorem hmac_sha256_sign (hb : Sha256Blocks) (key m : Slice U8) (hk : key.length ≤ maxInput) (hm : 64 + m.length ≤ maxInput) : (do let k ← high.hmac.HmacKey.new Sha256Hash key @@ -381,7 +381,7 @@ theorem hmac_sha256_sign (hb : ShaBlocks) (key m : Slice U8) (hk : key.length /-- HMAC-SHA1's tag of `m` under `key` is RFC 2104's, given the block functions' contracts. -/ -theorem hmac_sha1_sign (hb : ShaBlocks) (key m : Slice U8) (hk : key.length ≤ maxInput) +theorem hmac_sha1_sign (hb : Sha1Blocks) (key m : Slice U8) (hk : key.length ≤ maxInput) (hm : 64 + m.length ≤ maxInput) : (do let k ← high.hmac.HmacKey.new Sha1Hash key diff --git a/proofs/Rind/X86_64/HmacApi.lean b/proofs/Rind/X86_64/HmacApi.lean index 475e90b94..5b6d0fa8e 100644 --- a/proofs/Rind/X86_64/HmacApi.lean +++ b/proofs/Rind/X86_64/HmacApi.lean @@ -39,12 +39,13 @@ def hmacOf (a : high.hmac.Algorithm) (key text : List Byte) : List Byte := hmac (hmacHash a) (hmacBlock a) key text /-- What HMAC under `a` needs: the entry guard passes, and the CPU runs the -hash's routines (`ShaBlocks` for SHA-1 and SHA-256, `RunsSha512` for SHA-384 -and SHA-512). -/ +hash's routines (`Sha1Blocks` for SHA-1, `Sha256Blocks` for SHA-256, and +`RunsSha512` for SHA-384 and SHA-512). -/ def RunsHmac (a : high.hmac.Algorithm) : Prop := (∃ e, low.entry.Entry.new_secret = ok e) ∧ match a with - | .HMAC_SHA1 | .HMAC_SHA256 => ShaBlocks + | .HMAC_SHA1 => Sha1Blocks + | .HMAC_SHA256 => Sha256Blocks | .HMAC_SHA384 | .HMAC_SHA512 => RunsSha512 /-- `k` is the key `Key::new(a, key)` makes. -/ diff --git a/proofs/Rind/X86_64/Sha.lean b/proofs/Rind/X86_64/Sha.lean index 8d20f8cb8..d840de2b5 100644 --- a/proofs/Rind/X86_64/Sha.lean +++ b/proofs/Rind/X86_64/Sha.lean @@ -5,8 +5,9 @@ open Aeneas Aeneas.Std Result rind.spec /-! # SHA-1 and SHA-256, from their `Hash` impls to the block functions -The hash of a message is FIPS 180-4's, given `ShaBlocks`: the contracts of the -block functions below rind's padding, which no proof covers yet. +The hash of a message is FIPS 180-4's, given `Sha1Blocks` or `Sha256Blocks`: +the contracts of the block functions below rind's padding, which no proof +covers yet on x86_64. `admin/prove` writes the aarch64 proof from this file by renaming the target. -/ @@ -123,7 +124,7 @@ theorem sha256_length_spec (P : List U8) (s : mid.sha2.Sha256State) (more : Usiz simp only [lift, WP.spec_ok] at hbytes exact ⟨bits, by rw [hm.2.1, h8, ha.2.1]; omega, hbytes⟩ -theorem sha256_finish_with_spec (hb : ShaBlocks) (P : List U8) (s : mid.sha2.Sha256State) +theorem sha256_finish_with_spec (hb : Sha256Blocks) (P : List U8) (s : mid.sha2.Sha256State) (message : Slice U8) (hs : Sha256Absorbed P s) (hlen : 8 * (P.length + message.length) ≤ U64.max) : mid.sha2.Sha256State.finish_with s message ⦃ r => @@ -146,7 +147,7 @@ theorem saturating_add_val (x y : U64) (h : x.val + y.val ≤ U64.max) : simp only [BitVec.toNat_ofNat] exact Nat.mod_eq_of_lt (by scalar_tac) -theorem sha256_update_blocks_spec (hb : ShaBlocks) (P : List U8) (s : mid.sha2.Sha256State) +theorem sha256_update_blocks_spec (hb : Sha256Blocks) (P : List U8) (s : mid.sha2.Sha256State) (blk : Slice U8) (hs : Sha256Absorbed P s) (hl : blk.length % 64 = 0) (hbound : P.length + blk.length ≤ U64.max) : mid.sha2.Sha256State.Insts.RindLowGenericBlockwiseUpdateBlocks.update_blocks s blk ⦃ s' => Sha256Absorbed (P ++ blk.val) s' ⦄ := by @@ -202,7 +203,7 @@ theorem sha256_resume_spec (P : List U8) (s : mid.sha2.Sha256State) (hs : Sha256 step with blockwise_new_spec as ⟨bw, hbw⟩ exact ⟨by simp [hbw], P, hs, by simp [hbw]⟩ -theorem sha256_ctx_update_spec (hb : ShaBlocks) (p : List U8) (c : mid.sha2.Sha256Context) +theorem sha256_ctx_update_spec (hb : Sha256Blocks) (p : List U8) (c : mid.sha2.Sha256Context) (bytes : Slice U8) (hc : Sha256Ctx p c) (hlen : p.length + bytes.length ≤ maxInput) : mid.sha2.Sha256Context.update c bytes ⦃ c' => Sha256Ctx (p ++ bytes.val) c' ⦄ := by unfold mid.sha2.Sha256Context.update @@ -213,7 +214,7 @@ theorem sha256_ctx_update_spec (hb : ShaBlocks) (p : List U8) (c : mid.sha2.Sha2 p c.blockwise bytes c.state hc (by decide) hlen as ⟨bw, s', h⟩ exact h -theorem sha256_ctx_finish_spec (hb : ShaBlocks) (p : List U8) (c : mid.sha2.Sha256Context) +theorem sha256_ctx_finish_spec (hb : Sha256Blocks) (p : List U8) (c : mid.sha2.Sha256Context) (hc : Sha256Ctx p c) (hlen : p.length ≤ maxInput) : mid.sha2.Sha256Context.finish c ⦃ r => bv r.val = sha256.hash (bv p) ⦄ := by obtain ⟨hu, q, hq, hqp⟩ := hc @@ -348,8 +349,8 @@ theorem sha256_hash_length (m : List Byte) : (sha256.hash m).length = 32 := by foldl_length _ 8 sha256_compress_length _ _ (by simp [sha256.H0])] rfl -/-- SHA-256's `Hash` impl computes FIPS 180-4's SHA-256, given `ShaBlocks`. -/ -theorem sha256_hashSpec (hb : ShaBlocks) : +/-- SHA-256's `Hash` impl computes FIPS 180-4's SHA-256, given `Sha256Blocks`. -/ +theorem sha256_hashSpec (hb : Sha256Blocks) : HashSpec high.hash.Sha256.Insts.RindHighHashHashSha256ContextSha256State sha256.hash 64 32 maxInput Sha256Absorbed Sha256Ctx where out := ⟨by decide, by decide, by decide, by unfold maxInput; scalar_tac, sha256_hash_length⟩ @@ -413,7 +414,7 @@ theorem sha256_hashSpec (hb : ShaBlocks) : def Sha1Absorbed (P : List U8) (s : mid.sha1.Sha1State) : Prop := Absorbed sha1.compress sha1.H0 P s.h ∧ s.nblocks.val * 64 = P.length -theorem sha1_finish_with_spec (hb : ShaBlocks) (P : List U8) (s : mid.sha1.Sha1State) +theorem sha1_finish_with_spec (hb : Sha1Blocks) (P : List U8) (s : mid.sha1.Sha1State) (message : Slice U8) (hs : Sha1Absorbed P s) (hlen : 8 * (P.length + message.length) ≤ U64.max) : mid.sha1.Sha1State.finish_with s message ⦃ r => @@ -459,7 +460,7 @@ theorem sha1_finish_with_spec (hb : ShaBlocks) (P : List U8) (s : mid.sha1.Sha1S rfl all_goals simp [iter_post, iter_post1, s_post, Array.val_to_slice] -theorem sha1_update_blocks_spec (hb : ShaBlocks) (P : List U8) (s : mid.sha1.Sha1State) +theorem sha1_update_blocks_spec (hb : Sha1Blocks) (P : List U8) (s : mid.sha1.Sha1State) (blk : Slice U8) (hs : Sha1Absorbed P s) (hl : blk.length % 64 = 0) (hbound : P.length + blk.length ≤ U64.max) : mid.sha1.Sha1State.Insts.RindLowGenericBlockwiseUpdateBlocks.update_blocks s blk ⦃ s' => Sha1Absorbed (P ++ blk.val) s' ⦄ := by @@ -507,7 +508,7 @@ theorem sha1_resume_spec (P : List U8) (s : mid.sha1.Sha1State) (hs : Sha1Absorb step with blockwise_new_spec as ⟨bw, hbw⟩ exact ⟨by simp [hbw], P, hs, by simp [hbw]⟩ -theorem sha1_ctx_update_spec (hb : ShaBlocks) (p : List U8) (c : mid.sha1.Sha1Context) +theorem sha1_ctx_update_spec (hb : Sha1Blocks) (p : List U8) (c : mid.sha1.Sha1Context) (bytes : Slice U8) (hc : Sha1Ctx p c) (hlen : p.length + bytes.length ≤ maxInput) : mid.sha1.Sha1Context.update c bytes ⦃ c' => Sha1Ctx (p ++ bytes.val) c' ⦄ := by unfold mid.sha1.Sha1Context.update @@ -518,7 +519,7 @@ theorem sha1_ctx_update_spec (hb : ShaBlocks) (p : List U8) (c : mid.sha1.Sha1Co p c.blockwise bytes c.state hc (by decide) hlen as ⟨bw, s', h⟩ exact h -theorem sha1_ctx_finish_spec (hb : ShaBlocks) (p : List U8) (c : mid.sha1.Sha1Context) +theorem sha1_ctx_finish_spec (hb : Sha1Blocks) (p : List U8) (c : mid.sha1.Sha1Context) (hc : Sha1Ctx p c) (hlen : p.length ≤ maxInput) : mid.sha1.Sha1Context.finish c ⦃ r => bv r.val = sha1.hash (bv p) ⦄ := by obtain ⟨hu, q, hq, hqp⟩ := hc @@ -542,8 +543,8 @@ theorem sha1_hash_length (m : List Byte) : (sha1.hash m).length = 20 := by foldl_length _ 5 sha1_compress_length _ _ (by simp [sha1.H0])] rfl -/-- SHA-1's `Hash` impl computes FIPS 180-4's SHA-1, given `ShaBlocks`. -/ -theorem sha1_hashSpec (hb : ShaBlocks) : +/-- SHA-1's `Hash` impl computes FIPS 180-4's SHA-1, given `Sha1Blocks`. -/ +theorem sha1_hashSpec (hb : Sha1Blocks) : HashSpec high.hash.LegacySha1.Insts.RindHighHashHashSha1ContextSha1State sha1.hash 64 20 maxInput Sha1Absorbed Sha1Ctx where out := ⟨by decide, by decide, by decide, by unfold maxInput; scalar_tac, sha1_hash_length⟩ diff --git a/proofs/Rind/X86_64/ShaBlocks.lean b/proofs/Rind/X86_64/ShaBlocks.lean index cf15564b3..4f6eef85f 100644 --- a/proofs/Rind/X86_64/ShaBlocks.lean +++ b/proofs/Rind/X86_64/ShaBlocks.lean @@ -5,24 +5,23 @@ open Aeneas Aeneas.Std Result rind.spec # SHA-1 and SHA-256's block functions on x86_64 No proof covers any block function x86_64 runs for SHA-1 or SHA-256, so the -theorems over them take `ShaBlocks` as a hypothesis instead of an axiom: each -routine's contract, FIPS 180-4's block function over every whole block it is -given, and that rind's checks pass. On the SHA extensions, SHA-1 and SHA-256 -pad their last block in registers, so those routines' contracts cover the -padding too. Once a routine's published proof lands, -an axiom restating it under the composition rule discharges its field. +theorems over them take `Sha1Blocks` or `Sha256Blocks` as a hypothesis instead +of an axiom: each routine's contract, FIPS 180-4's block function over every +whole block it is given, and that rind's checks pass. On the SHA extensions, +SHA-1 and SHA-256 pad their last block in registers, so those routines' +contracts cover the padding too. Once a routine's published proof lands, an +axiom restating it under the composition rule discharges its field. -/ namespace rind.x86_64 -/-- What the SHA-1 and SHA-256 theorems assume of the code below rind's -padding on x86_64: each routine computes FIPS 180-4's block function, or pads -and compresses as FIPS 180-4 does on the SHA extensions, the CPU dispatch -picks one, and the entry checks pass. None reads an input. -/ -structure ShaBlocks : Prop where +/-- What the SHA-1 theorems assume of the code below rind's padding on +x86_64: each routine computes FIPS 180-4's block function, or pads and +compresses as FIPS 180-4 does on the SHA extensions, the CPU dispatch picks +one, and the entry checks pass. None reads an input. -/ +structure Sha1Blocks : Prop where entry : ∃ e, low.entry.Entry.new_secret = ok e held : low.entry.Entry.assert_held = ok () - path : ∃ p, low.x86_64.sha256_mux.path = ok p sha1_path : ∃ p, low.x86_64.sha1_mux.path = ok p /-- SHA-1's padded compression on the SHA extensions: `m` padded and closed by `length`. -/ @@ -33,6 +32,13 @@ structure ShaBlocks : Prop where (words h.val) ⦄ -- After `sha1_shaext`, whose `sha1.compress` would otherwise name this field. sha1 : Compresses sha1.compress low.x86_64.sha1_mux.sha1_compress_blocks + +/-- What the SHA-256 theorems assume of the code below rind's padding on +x86_64, as `Sha1Blocks` does for SHA-1's. -/ +structure Sha256Blocks : Prop where + entry : ∃ e, low.entry.Entry.new_secret = ok e + held : low.entry.Entry.assert_held = ok () + path : ∃ p, low.x86_64.sha256_mux.path = ok p shaext : ∀ t, Compresses sha256.compress fun h b => low.x86_64.sha256.sha256_compress_blocks_shaext h b t /-- The SHA extensions' finish: `m` padded and closed by `length`, and the @@ -49,7 +55,7 @@ structure ShaBlocks : Prop where low.x86_64.sha256.sha256_compress_blocks_ssse3 h b t nohw : Compresses sha256.compress low.x86_64.sha256.sha256_compress_blocks_nohw -theorem sha256_compress_blocks_spec (hb : ShaBlocks) : +theorem sha256_compress_blocks_spec (hb : Sha256Blocks) : Compresses sha256.compress low.x86_64.sha256_mux.sha256_compress_blocks := by intro h b hl obtain ⟨p, hp⟩ := hb.path @@ -63,14 +69,14 @@ theorem sha256_compress_blocks_spec (hb : ShaBlocks) : | Nohw => exact (by simpa using hb.nohw h b hl) /-- SHA-256's block function as `Sha256State` calls it. -/ -theorem sha256_block_spec (hb : ShaBlocks) : Compresses sha256.compress mid.sha2.Sha256State.compress := by +theorem sha256_block_spec (hb : Sha256Blocks) : Compresses sha256.compress mid.sha2.Sha256State.compress := by intro h b hl unfold mid.sha2.Sha256State.compress rw [hb.held] simpa using sha256_compress_blocks_spec hb h b hl /-- SHA-1's block function as `Sha1State` calls it. -/ -theorem sha1_block_spec (hb : ShaBlocks) : +theorem sha1_block_spec (hb : Sha1Blocks) : Compresses sha1.compress mid.sha1.Sha1State.compress := by intro h b hl unfold mid.sha1.Sha1State.compress @@ -78,7 +84,7 @@ theorem sha1_block_spec (hb : ShaBlocks) : simpa using hb.sha1 h b hl /-- SHA-1's padded last blocks. -/ -theorem sha1_compress_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std.Array U32 5#usize) +theorem sha1_compress_padded_spec (hb : Sha1Blocks) (P : List U8) (state : Std.Array U32 5#usize) (message : Slice U8) (length : Std.Array U8 8#usize) (hR : Absorbed sha1.compress sha1.H0 P state) : low.x86_64.sha1_mux.sha1_compress_padded state message length ⦃ h' => @@ -130,7 +136,7 @@ theorem sha1_compress_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std.Ar /-- SHA-256's padded last blocks, on the routines that do not finish a hash themselves. -/ -theorem sha256_compress_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std.Array U32 8#usize) +theorem sha256_compress_padded_spec (hb : Sha256Blocks) (P : List U8) (state : Std.Array U32 8#usize) (message : Slice U8) (length : Std.Array U8 8#usize) (hR : Absorbed sha256.compress sha256.H0 P state) : low.x86_64.sha256_mux.sha256_compress_padded state message length ⦃ h' => @@ -169,7 +175,7 @@ theorem sha256_compress_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std. /-- The routines that do not finish a hash: the padded last blocks, then the digest's encoding. -/ -theorem sha256_finish_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std.Array U32 8#usize) +theorem sha256_finish_padded_spec (hb : Sha256Blocks) (P : List U8) (state : Std.Array U32 8#usize) (message : Slice U8) (length : Std.Array U8 8#usize) (hR : Absorbed sha256.compress sha256.H0 P state) : (do @@ -183,7 +189,7 @@ theorem sha256_finish_padded_spec (hb : ShaBlocks) (P : List U8) (state : Std.Ar rfl /-- SHA-256's digest of what `state` has absorbed followed by `message`. -/ -theorem sha256_finish_spec (hb : ShaBlocks) (P : List U8) (state : Std.Array U32 8#usize) +theorem sha256_finish_spec (hb : Sha256Blocks) (P : List U8) (state : Std.Array U32 8#usize) (message : Slice U8) (length : Std.Array U8 8#usize) (hR : Absorbed sha256.compress sha256.H0 P state) : low.x86_64.sha256_mux.sha256_finish state message length ⦃ r => diff --git a/proofs/hol-light/aarch64/sha256_block_data_order_hw.ml b/proofs/hol-light/aarch64/sha256_block_data_order_hw.ml new file mode 100644 index 000000000..868b98d23 --- /dev/null +++ b/proofs/hol-light/aarch64/sha256_block_data_order_hw.ml @@ -0,0 +1,621 @@ +(* + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0 + *) + +(* ========================================================================= *) +(* SHA-256 block compression with the Armv8 crypto extension, as rind's *) +(* build emits it. *) +(* ========================================================================= *) + +(* rind's naked function low::aarch64::sha256::sha256_block_data_order_hw is + aws-lc's sha256_block_data_order_hw (crypto/fipsmodule/sha/asm/ + sha256-armv8.pl, the ARMv8 path), which reads its round constants from the + K256 table beside it. Its result is s2n-bignum's FIPS 180-4 spec, + sha256_hash_blocks, from s2n-bignum pull request #415, which + proofs/hol-light/s2n-bignum/ holds until it merges. The proof steps the + loop body's 115 instructions symbolically, rewriting each SHA256H/SHA256H2 + pair to four rounds and each SHA256SU0/SHA256SU1 pair to four message + schedule words, so no case split on the data is needed. *) + +needs "arm/proofs/base.ml";; +needs "x86/proofs/utils/sha256_spec.ml";; + +(* admin/prove writes the function's object, as rind's release build emits + it, to aarch64/sha256_block_data_order_hw.o: its instructions as .text, + with relocations, and the K256 table as .rodata. The definition fails + unless the instructions and relocations are these, and sha256_hw_k256 is + the table's bytes, which SHA256_HW_K256_QUADS checks against FIPS 180-4's + constants. *) +let sha256_hw_mc,sha256_hw_data = + define_assert_relocs_from_elf + ~map_symbol_name:(fun _ -> "sha256_hw_k256") + "sha256_hw_mc" "aarch64/sha256_block_data_order_hw.o" +(fun w BL ADR ADRP ADD_rri64 -> [ + w 0xa9bf7bfd; (* arm_STP X29 X30 SP (Preimmediate_Offset (iword (-- &16))) *) + w 0x910003fd; (* arm_ADD X29 SP (rvalue (word 0)) *) + w 0x4c40a800; (* arm_LDP Q0 Q1 X0 No_Offset *) + ADRP (mk_var("sha256_hw_k256",`:num`),0,12,3); + ADD_rri64 (mk_var("sha256_hw_k256",`:num`),0,3,3); + w 0x4cdf2024; (* arm_LDP4 Q4 Q5 Q6 Q7 X1 (Postimmediate_Offset (word 64)) *) + w 0xd1000442; (* arm_SUB X2 X2 (rvalue (word 1)) *) + w 0x4cdf7870; (* arm_LDR Q16 X3 (Postimmediate_Offset (word 16)) *) + w 0x6e200884; (* arm_REV32_VEC Q4 Q4 8 *) + w 0x6e2008a5; (* arm_REV32_VEC Q5 Q5 8 *) + w 0x6e2008c6; (* arm_REV32_VEC Q6 Q6 8 *) + w 0x6e2008e7; (* arm_REV32_VEC Q7 Q7 8 *) + w 0x4ea01c12; (* arm_MOV_VEC Q18 Q0 128 *) + w 0x4ea11c33; (* arm_MOV_VEC Q19 Q1 128 *) + w 0x4cdf7871; (* arm_LDR Q17 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea48610; (* arm_ADD_VEC Q16 Q16 Q4 32 128 *) + w 0x5e2828a4; (* arm_SHA256SU0 Q4 Q5 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e104020; (* arm_SHA256H Q0 Q1 Q16 *) + w 0x5e105041; (* arm_SHA256H2 Q1 Q2 Q16 *) + w 0x5e0760c4; (* arm_SHA256SU1 Q4 Q6 Q7 *) + w 0x4cdf7870; (* arm_LDR Q16 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea58631; (* arm_ADD_VEC Q17 Q17 Q5 32 128 *) + w 0x5e2828c5; (* arm_SHA256SU0 Q5 Q6 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e114020; (* arm_SHA256H Q0 Q1 Q17 *) + w 0x5e115041; (* arm_SHA256H2 Q1 Q2 Q17 *) + w 0x5e0460e5; (* arm_SHA256SU1 Q5 Q7 Q4 *) + w 0x4cdf7871; (* arm_LDR Q17 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea68610; (* arm_ADD_VEC Q16 Q16 Q6 32 128 *) + w 0x5e2828e6; (* arm_SHA256SU0 Q6 Q7 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e104020; (* arm_SHA256H Q0 Q1 Q16 *) + w 0x5e105041; (* arm_SHA256H2 Q1 Q2 Q16 *) + w 0x5e056086; (* arm_SHA256SU1 Q6 Q4 Q5 *) + w 0x4cdf7870; (* arm_LDR Q16 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea78631; (* arm_ADD_VEC Q17 Q17 Q7 32 128 *) + w 0x5e282887; (* arm_SHA256SU0 Q7 Q4 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e114020; (* arm_SHA256H Q0 Q1 Q17 *) + w 0x5e115041; (* arm_SHA256H2 Q1 Q2 Q17 *) + w 0x5e0660a7; (* arm_SHA256SU1 Q7 Q5 Q6 *) + w 0x4cdf7871; (* arm_LDR Q17 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea48610; (* arm_ADD_VEC Q16 Q16 Q4 32 128 *) + w 0x5e2828a4; (* arm_SHA256SU0 Q4 Q5 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e104020; (* arm_SHA256H Q0 Q1 Q16 *) + w 0x5e105041; (* arm_SHA256H2 Q1 Q2 Q16 *) + w 0x5e0760c4; (* arm_SHA256SU1 Q4 Q6 Q7 *) + w 0x4cdf7870; (* arm_LDR Q16 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea58631; (* arm_ADD_VEC Q17 Q17 Q5 32 128 *) + w 0x5e2828c5; (* arm_SHA256SU0 Q5 Q6 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e114020; (* arm_SHA256H Q0 Q1 Q17 *) + w 0x5e115041; (* arm_SHA256H2 Q1 Q2 Q17 *) + w 0x5e0460e5; (* arm_SHA256SU1 Q5 Q7 Q4 *) + w 0x4cdf7871; (* arm_LDR Q17 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea68610; (* arm_ADD_VEC Q16 Q16 Q6 32 128 *) + w 0x5e2828e6; (* arm_SHA256SU0 Q6 Q7 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e104020; (* arm_SHA256H Q0 Q1 Q16 *) + w 0x5e105041; (* arm_SHA256H2 Q1 Q2 Q16 *) + w 0x5e056086; (* arm_SHA256SU1 Q6 Q4 Q5 *) + w 0x4cdf7870; (* arm_LDR Q16 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea78631; (* arm_ADD_VEC Q17 Q17 Q7 32 128 *) + w 0x5e282887; (* arm_SHA256SU0 Q7 Q4 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e114020; (* arm_SHA256H Q0 Q1 Q17 *) + w 0x5e115041; (* arm_SHA256H2 Q1 Q2 Q17 *) + w 0x5e0660a7; (* arm_SHA256SU1 Q7 Q5 Q6 *) + w 0x4cdf7871; (* arm_LDR Q17 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea48610; (* arm_ADD_VEC Q16 Q16 Q4 32 128 *) + w 0x5e2828a4; (* arm_SHA256SU0 Q4 Q5 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e104020; (* arm_SHA256H Q0 Q1 Q16 *) + w 0x5e105041; (* arm_SHA256H2 Q1 Q2 Q16 *) + w 0x5e0760c4; (* arm_SHA256SU1 Q4 Q6 Q7 *) + w 0x4cdf7870; (* arm_LDR Q16 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea58631; (* arm_ADD_VEC Q17 Q17 Q5 32 128 *) + w 0x5e2828c5; (* arm_SHA256SU0 Q5 Q6 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e114020; (* arm_SHA256H Q0 Q1 Q17 *) + w 0x5e115041; (* arm_SHA256H2 Q1 Q2 Q17 *) + w 0x5e0460e5; (* arm_SHA256SU1 Q5 Q7 Q4 *) + w 0x4cdf7871; (* arm_LDR Q17 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea68610; (* arm_ADD_VEC Q16 Q16 Q6 32 128 *) + w 0x5e2828e6; (* arm_SHA256SU0 Q6 Q7 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e104020; (* arm_SHA256H Q0 Q1 Q16 *) + w 0x5e105041; (* arm_SHA256H2 Q1 Q2 Q16 *) + w 0x5e056086; (* arm_SHA256SU1 Q6 Q4 Q5 *) + w 0x4cdf7870; (* arm_LDR Q16 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea78631; (* arm_ADD_VEC Q17 Q17 Q7 32 128 *) + w 0x5e282887; (* arm_SHA256SU0 Q7 Q4 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e114020; (* arm_SHA256H Q0 Q1 Q17 *) + w 0x5e115041; (* arm_SHA256H2 Q1 Q2 Q17 *) + w 0x5e0660a7; (* arm_SHA256SU1 Q7 Q5 Q6 *) + w 0x4cdf7871; (* arm_LDR Q17 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea48610; (* arm_ADD_VEC Q16 Q16 Q4 32 128 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e104020; (* arm_SHA256H Q0 Q1 Q16 *) + w 0x5e105041; (* arm_SHA256H2 Q1 Q2 Q16 *) + w 0x4cdf7870; (* arm_LDR Q16 X3 (Postimmediate_Offset (word 16)) *) + w 0x4ea58631; (* arm_ADD_VEC Q17 Q17 Q5 32 128 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e114020; (* arm_SHA256H Q0 Q1 Q17 *) + w 0x5e115041; (* arm_SHA256H2 Q1 Q2 Q17 *) + w 0x4c407871; (* arm_LDR Q17 X3 No_Offset *) + w 0x4ea68610; (* arm_ADD_VEC Q16 Q16 Q6 32 128 *) + w 0xd103c063; (* arm_SUB X3 X3 (rvalue (word 240)) *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e104020; (* arm_SHA256H Q0 Q1 Q16 *) + w 0x5e105041; (* arm_SHA256H2 Q1 Q2 Q16 *) + w 0x4ea78631; (* arm_ADD_VEC Q17 Q17 Q7 32 128 *) + w 0x4ea01c02; (* arm_MOV_VEC Q2 Q0 128 *) + w 0x5e114020; (* arm_SHA256H Q0 Q1 Q17 *) + w 0x5e115041; (* arm_SHA256H2 Q1 Q2 Q17 *) + w 0x4eb28400; (* arm_ADD_VEC Q0 Q0 Q18 32 128 *) + w 0x4eb38421; (* arm_ADD_VEC Q1 Q1 Q19 32 128 *) + w 0xb5fff1a2; (* arm_CBNZ X2 (word 2096692) *) + w 0x4c00a800; (* arm_STP Q0 Q1 X0 No_Offset *) + w 0xf84107fd; (* arm_LDR X29 SP (Postimmediate_Offset (word 16)) *) + w 0xd65f03c0 (* arm_RET X30 *) +]);; +let sha256_hw_k256 = last sha256_hw_data;; +let SHA256_HW_EXEC = ARM_MK_EXEC_RULE sha256_hw_mc;; + +(* ------------------------------------------------------------------------- *) +(* The SHA256H/SHA256H2 instructions as four rounds of the spec. *) +(* ------------------------------------------------------------------------- *) + +let sha256_quad = new_definition + `sha256_quad (a:int32) (b:int32) (c:int32) (d:int32) : int128 = + word_join (word_join d c:int64) (word_join b a:int64)`;; + +let SHA256_QUAD_SUBWORDS = prove + (`!a b c d:int32. + word_subword (sha256_quad a b c d) (0,32) = a /\ + word_subword (sha256_quad a b c d) (32,32) = b /\ + word_subword (sha256_quad a b c d) (64,32) = c /\ + word_subword (sha256_quad a b c d) (96,32) = d`, + REWRITE_TAC[sha256_quad] THEN CONV_TAC WORD_BLAST);; + +let SHA256_ROL_LEMMA = prove + (`!a b c d e f g h p q:int32. + word_rol (word_join + ((word_join:int32->96 word->int128) p (word_subword (sha256_quad a b c d) (0,96))) + ((word_join:int32->96 word->int128) q (word_subword (sha256_quad e f g h) (0,96))) :256 word) 32 = + word_join (sha256_quad q a b c) (sha256_quad p e f g)`, + REWRITE_TAC[sha256_quad] THEN CONV_TAC WORD_BLAST);; + +let SHA256HASH_LOOP_ROUND = prove + (`!i a b c d e f g h k w W. + elem W i 32 = word_add k w + ==> sha256hash_loop i (sha256_quad a b c d) (sha256_quad e f g h) W = + let l = sha256_round [a;b;c;d;e;f;g;h] k w in + word_join (sha256_quad (EL 0 l) (EL 1 l) (EL 2 l) (EL 3 l)) + (sha256_quad (EL 4 l) (EL 5 l) (EL 6 l) (EL 7 l))`, + REPEAT STRIP_TAC THEN + REWRITE_TAC[sha256hash_loop; sha256_round] THEN ASM_REWRITE_TAC[] THEN + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + REWRITE_TAC[SHA256_QUAD_SUBWORDS; SHA256_ROL_LEMMA] THEN + CONV_TAC(DEPTH_CONV EL_CONV) THEN REWRITE_TAC[WORD_ADD_AC]);; + +let sha256_abcd = new_definition + `sha256_abcd (l:int32 list) = sha256_quad (EL 0 l) (EL 1 l) (EL 2 l) (EL 3 l)`;; +let sha256_efgh = new_definition + `sha256_efgh (l:int32 list) = sha256_quad (EL 4 l) (EL 5 l) (EL 6 l) (EL 7 l)`;; + +let SHA256_ROUND_ELS = prove + (`!l k w. sha256_round l k w = + sha256_round [EL 0 l; EL 1 l; EL 2 l; EL 3 l; EL 4 l; EL 5 l; EL 6 l; EL 7 l] k w`, + REWRITE_TAC[sha256_round] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + CONV_TAC(DEPTH_CONV EL_CONV) THEN REWRITE_TAC[]);; + +let SHA256HASH_LOOP_STATE = prove + (`!i l k w W. + elem W i 32 = word_add k w + ==> sha256hash_loop i (sha256_abcd l) (sha256_efgh l) W = + word_join (sha256_abcd (sha256_round l k w)) (sha256_efgh (sha256_round l k w))`, + REPEAT STRIP_TAC THEN REWRITE_TAC[sha256_abcd; sha256_efgh] THEN + ASM_SIMP_TAC[SHA256HASH_LOOP_ROUND] THEN + GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SHA256_ROUND_ELS] THEN + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REFL_TAC);; + +let SHA256_JOIN128_SUBWORDS = prove + (`!x y:int128. word_subword ((word_join:int128->int128->256 word) x y) (128,128) = x /\ + word_subword ((word_join:int128->int128->256 word) x y) (0,128) = y`, + CONV_TAC WORD_BLAST);; + +let SHA256_ELEM_QUAD = prove + (`!a b c d:int32. elem (sha256_quad a b c d) 0 32 = a /\ elem (sha256_quad a b c d) 1 32 = b /\ + elem (sha256_quad a b c d) 2 32 = c /\ elem (sha256_quad a b c d) 3 32 = d`, + REWRITE_TAC[elem] THEN CONV_TAC(DEPTH_CONV NUM_RED_CONV) THEN REWRITE_TAC[SHA256_QUAD_SUBWORDS]);; + +let SHA256HASH_LOOP_QUAD = prove + (`!k0 w0 k1 w1 k2 w2 k3 w3. + let W = sha256_quad (word_add k0 w0) (word_add k1 w1) (word_add k2 w2) (word_add k3 w3) in + (!l. sha256hash_loop 0 (sha256_abcd l) (sha256_efgh l) W = + word_join (sha256_abcd (sha256_round l k0 w0)) (sha256_efgh (sha256_round l k0 w0))) /\ + (!l. sha256hash_loop 1 (sha256_abcd l) (sha256_efgh l) W = + word_join (sha256_abcd (sha256_round l k1 w1)) (sha256_efgh (sha256_round l k1 w1))) /\ + (!l. sha256hash_loop 2 (sha256_abcd l) (sha256_efgh l) W = + word_join (sha256_abcd (sha256_round l k2 w2)) (sha256_efgh (sha256_round l k2 w2))) /\ + (!l. sha256hash_loop 3 (sha256_abcd l) (sha256_efgh l) W = + word_join (sha256_abcd (sha256_round l k3 w3)) (sha256_efgh (sha256_round l k3 w3)))`, + REPEAT GEN_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + REPEAT CONJ_TAC THEN GEN_TAC THEN MATCH_MP_TAC SHA256HASH_LOOP_STATE THEN + REWRITE_TAC[SHA256_ELEM_QUAD]);; + +let SHA256H_4ROUNDS = prove + (`!l k0 k1 k2 k3 w0 w1 w2 w3. + let W = sha256_quad (word_add k0 w0) (word_add k1 w1) (word_add k2 w2) (word_add k3 w3) in + let l4 = sha256_round (sha256_round (sha256_round (sha256_round l k0 w0) k1 w1) k2 w2) k3 w3 in + sha256h (sha256_abcd l) (sha256_efgh l) W = sha256_abcd l4 /\ + sha256h2 (sha256_efgh l) (sha256_abcd l) W = sha256_efgh l4`, + REPEAT GEN_TAC THEN + MP_TAC(CONV_RULE(TOP_DEPTH_CONV let_CONV) + (SPECL [`k0:int32`; `w0:int32`; `k1:int32`; `w1:int32`; + `k2:int32`; `w2:int32`; `k3:int32`; `w3:int32`] SHA256HASH_LOOP_QUAD)) THEN + STRIP_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + REWRITE_TAC[sha256h; sha256h2; sha256hash] THEN + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + ASM_REWRITE_TAC[SHA256_JOIN128_SUBWORDS]);; +(* ------------------------------------------------------------------------- *) +(* The SHA256SU0/SHA256SU1 instructions as the message schedule. *) +(* ------------------------------------------------------------------------- *) + +let SHA256_QUAD_NESTED = prove + (`!a b c d:int32. + sha256_quad a b c d = + (word_join:int32->96 word->int128) d + ((word_join:int32->64 word->96 word) c ((word_join:int32->int32->int64) b a))`, + REWRITE_TAC[sha256_quad] THEN CONV_TAC WORD_BLAST);; + +let SHA256SU_SCHEDULE = prove + (`!w0 w1 w2 w3 w4 w5 w6 w7 w8 w9 w10 w11 w12 w13 w14 w15:int32. + let x16 = word_add (word_add (sha_msg_sigma_1 w14) w9) (word_add (sha_msg_sigma_0 w1) w0) in + let x17 = word_add (word_add (sha_msg_sigma_1 w15) w10) (word_add (sha_msg_sigma_0 w2) w1) in + let x18 = word_add (word_add (sha_msg_sigma_1 x16) w11) (word_add (sha_msg_sigma_0 w3) w2) in + let x19 = word_add (word_add (sha_msg_sigma_1 x17) w12) (word_add (sha_msg_sigma_0 w4) w3) in + sha256su1 (sha256su0 (sha256_quad w0 w1 w2 w3) (sha256_quad w4 w5 w6 w7)) + (sha256_quad w8 w9 w10 w11) (sha256_quad w12 w13 w14 w15) = + sha256_quad x16 x17 x18 x19`, + REPEAT GEN_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + REWRITE_TAC[sha256su0; sha256su1; sha256su0_loop; sha256su1_loop0; sha256su1_loop1; elem] THEN + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN CONV_TAC(DEPTH_CONV NUM_RED_CONV) THEN + REWRITE_TAC[SHA256_QUAD_NESTED] THEN + CONV_TAC(TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV) THEN + REWRITE_TAC[sha_msg_sigma_0; sha_msg_sigma_1] THEN + REWRITE_TAC[WORD_ADD_AC]);; +(* ------------------------------------------------------------------------- *) +(* Four rounds and four schedule words at a time, for the loop body. *) +(* ------------------------------------------------------------------------- *) + +let SHA256_REVERSE_BYTEREVERSE = prove + (`!x:int32. word_reversefields 8 (word_bytereverse x) = x`, + CONV_TAC WORD_BLAST);; + +let SHA256_ROUNDS_STEP = prove + (`!m hs n. + sha256h (sha256_abcd (sha256_compress_rounds m hs n)) (sha256_efgh (sha256_compress_rounds m hs n)) + (sha256_quad (word_add (EL n sha256_constants) (sha256_msg_schedule m n)) + (word_add (EL (n+1) sha256_constants) (sha256_msg_schedule m (n+1))) + (word_add (EL (n+2) sha256_constants) (sha256_msg_schedule m (n+2))) + (word_add (EL (n+3) sha256_constants) (sha256_msg_schedule m (n+3)))) = + sha256_abcd (sha256_compress_rounds m hs (n+4)) /\ + sha256h2 (sha256_efgh (sha256_compress_rounds m hs n)) (sha256_abcd (sha256_compress_rounds m hs n)) + (sha256_quad (word_add (EL n sha256_constants) (sha256_msg_schedule m n)) + (word_add (EL (n+1) sha256_constants) (sha256_msg_schedule m (n+1))) + (word_add (EL (n+2) sha256_constants) (sha256_msg_schedule m (n+2))) + (word_add (EL (n+3) sha256_constants) (sha256_msg_schedule m (n+3)))) = + sha256_efgh (sha256_compress_rounds m hs (n+4))`, + REPEAT GEN_TAC THEN + REWRITE_TAC[ARITH_RULE `n + 4 = (((n + 1) + 1) + 1) + 1`] THEN + REWRITE_TAC[sha256_compress_rounds] THEN + REWRITE_TAC[GSYM ADD_ASSOC] THEN CONV_TAC(DEPTH_CONV NUM_ADD_CONV) THEN + MP_TAC(CONV_RULE(TOP_DEPTH_CONV let_CONV) (ISPEC `sha256_compress_rounds m hs n` SHA256H_4ROUNDS)) THEN + SIMP_TAC[]);; + +let SHA256_MSG_SCHEDULE_REC = prove + (`!m t. sha256_msg_schedule m (t + 16) = + word_add (word_add (sha_msg_sigma_1 (sha256_msg_schedule m (t + 14))) + (sha256_msg_schedule m (t + 9))) + (word_add (sha_msg_sigma_0 (sha256_msg_schedule m (t + 1))) + (sha256_msg_schedule m t))`, + REPEAT GEN_TAC THEN GEN_REWRITE_TAC LAND_CONV [sha256_msg_schedule] THEN + REWRITE_TAC[ARITH_RULE `~(t + 16 < 16) /\ (t + 16) - 2 = t + 14 /\ (t + 16) - 7 = t + 9 /\ + (t + 16) - 15 = t + 1 /\ (t + 16) - 16 = t`]);; + +let SHA256_SCHED_STEP = prove + (`!m n. + sha256su1 + (sha256su0 + (sha256_quad (sha256_msg_schedule m n) (sha256_msg_schedule m (n+1)) + (sha256_msg_schedule m (n+2)) (sha256_msg_schedule m (n+3))) + (sha256_quad (sha256_msg_schedule m (n+4)) (sha256_msg_schedule m (n+5)) + (sha256_msg_schedule m (n+6)) (sha256_msg_schedule m (n+7)))) + (sha256_quad (sha256_msg_schedule m (n+8)) (sha256_msg_schedule m (n+9)) + (sha256_msg_schedule m (n+10)) (sha256_msg_schedule m (n+11))) + (sha256_quad (sha256_msg_schedule m (n+12)) (sha256_msg_schedule m (n+13)) + (sha256_msg_schedule m (n+14)) (sha256_msg_schedule m (n+15))) = + sha256_quad (sha256_msg_schedule m (n+16)) (sha256_msg_schedule m (n+17)) + (sha256_msg_schedule m (n+18)) (sha256_msg_schedule m (n+19))`, + REPEAT GEN_TAC THEN + REWRITE_TAC[SHA256SU_SCHEDULE |> SPEC_ALL |> CONV_RULE(TOP_DEPTH_CONV let_CONV)] THEN + let inst k = CONV_RULE(DEPTH_CONV NUM_ADD_CONV) + (REWRITE_RULE[GSYM ADD_ASSOC] (SPECL [`m:int32 list`; mk_comb(mk_comb(`(+)`,`n:num`),mk_small_numeral k)] SHA256_MSG_SCHEDULE_REC)) in + REWRITE_TAC(GSYM(SPECL [`m:int32 list`; `n:num`] SHA256_MSG_SCHEDULE_REC) :: + map (fun k -> GSYM(inst k)) [1;2;3]) THEN + ALL_TAC);; +let SHA256_ROUNDS_AT n = + let th = CONV_RULE(DEPTH_CONV NUM_ADD_CONV) (SPECL [`m:int32 list`; `hs:int32 list`; mk_small_numeral n] SHA256_ROUNDS_STEP) in + if n = 0 then REWRITE_RULE[CONJUNCT1 sha256_compress_rounds] th else th;; +let SHA256_SCHED_AT n = + CONV_RULE(DEPTH_CONV NUM_ADD_CONV) (SPECL [`m:int32 list`; mk_small_numeral n] SHA256_SCHED_STEP);; +let SHA256_BODY_THS = + map SHA256_ROUNDS_AT (0--15 |> map (( * ) 4)) @ map SHA256_SCHED_AT (0--11 |> map (( * ) 4));; + +let SHA256_SIMP_QREG_TAC = + let is_qread th = + let c = concl th in + is_eq c && (let l = lhs c in + try let r,_ = dest_comb l in let rd,comp = dest_comb r in + name_of rd = "read" && is_const comp && String.sub (name_of comp) 0 1 = "Q" + with _ -> false) in + let rule = REWRITE_RULE SHA256_BODY_THS o REWRITE_RULE[GSYM sha256_quad] o + CONV_RULE(TOP_DEPTH_CONV WORD_SIMPLE_SUBWORD_CONV) o + REWRITE_RULE[SHA256_QUAD_SUBWORDS; SHA256_REVERSE_BYTEREVERSE] in + RULE_ASSUM_TAC(fun th -> if is_qread th then rule th else th);; + +let SHA256_STEPS_TAC ns = + MAP_EVERY (fun n -> ARM_STEPS_TAC SHA256_HW_EXEC [n] THEN SHA256_SIMP_QREG_TAC) ns;; + +(* ------------------------------------------------------------------------- *) +(* The round constants and the message words in memory. *) +(* ------------------------------------------------------------------------- *) + +let quad_of f i = list_mk_comb(`sha256_quad`, map (fun k -> f (i+k)) [0;1;2;3]);; +let kconst t = mk_comb(mk_comb(`EL:num->int32 list->int32`, mk_small_numeral t), `sha256_constants`);; + +let SHA256_HW_K256_QUADS = + let at j = mk_comb(`word:num->int64`, mk_binop `(+):num->num->num` `k:num` (mk_small_numeral (16*j))) in + let kfacts = list_mk_conj(map (fun j -> mk_eq(subst [at j,`a:int64`] `read (memory :> bytes128 a) s`, quad_of kconst (4*j))) (0--15)) in + prove + (mk_forall(`s:armstate`, mk_forall(`k:num`, mk_imp(`bytes_loaded s (word (k + 0)) sha256_hw_k256`, kfacts))), + REPEAT GEN_TAC THEN REWRITE_TAC[sha256_hw_k256] THEN + CONV_TAC(LAND_CONV DATA64_CONV) THEN STRIP_TAC THEN + REWRITE_TAC[CONJUNCT1(CONJUNCT2 READ_MEMORY_BYTESIZED_SPLIT); GSYM WORD_ADD] THEN + REWRITE_TAC[GSYM ADD_ASSOC] THEN CONV_TAC(DEPTH_CONV NUM_ADD_CONV) THEN + ASM_REWRITE_TAC[sha256_quad; sha256_constants] THEN + CONV_TAC(DEPTH_CONV EL_CONV) THEN CONV_TAC WORD_REDUCE_CONV);; +let SHA256_READ_QUAD = prove + (`!a s. read (memory :> bytes128 a) s = + sha256_quad (read (memory :> bytes32 a) s) + (read (memory :> bytes32 (word_add a (word 4))) s) + (read (memory :> bytes32 (word_add a (word 8))) s) + (read (memory :> bytes32 (word_add a (word 12))) s)`, + REWRITE_TAC[CONJUNCT1(CONJUNCT2 READ_MEMORY_BYTESIZED_SPLIT); + CONJUNCT1(CONJUNCT2(CONJUNCT2 READ_MEMORY_BYTESIZED_SPLIT))] THEN + REWRITE_TAC[sha256_quad; GSYM WORD_ADD_ASSOC; GSYM WORD_ADD] THEN + CONV_TAC(DEPTH_CONV NUM_ADD_CONV) THEN REWRITE_TAC[]);; + +let sha256_hw_inputs = new_definition + `sha256_hw_inputs (k256:num) (data:int64) (n:num) (m:num->int32 list) (M:int64->byte) <=> + read (bytelist (word k256,LENGTH sha256_hw_k256)) M = sha256_hw_k256 /\ + !i j. i < n /\ j < 16 + ==> read (bytes32 (word_add data (word (64 * i + 4 * j)))) M = + word_bytereverse (EL j (m i))`;; + +let SHA256_MEM0_TAC = + FIRST_X_ASSUM(fun th -> + match concl th with + Comb(Comb(Const("=",_),Comb(Comb(Const("read",_),Const("memory",_)),_)),Var("mem0",_)) -> + RULE_ASSUM_TAC(REWRITE_RULE[th]) THEN ASSUME_TAC th + | _ -> failwith "SHA256_MEM0_TAC");; +let SHA256_MSCH_SMALL = + map (fun t -> CONV_RULE(RAND_CONV(RATOR_CONV(LAND_CONV NUM_LT_CONV) THENC REWRITE_CONV[])) + (REWR_CONV sha256_msg_schedule (mk_comb(`sha256_msg_schedule mm`, mk_small_numeral t)))) + (0--15);; + +let SHA256_DATA_TAC = + let dq q = let a = if q = 0 then `word_add (data:int64) (word (64 * i))` + else mk_comb(mk_comb(`word_add:int64->int64->int64`, `word_add (data:int64) (word (64 * i))`), + mk_comb(`word:num->int64`, mk_small_numeral (16*q))) in + mk_eq(subst [a,`a:int64`] `read (memory :> bytes128 (a:int64)) (s0:armstate)`, + quad_of (fun t -> mk_comb(`word_bytereverse:int32->int32`, + mk_comb(`sha256_msg_schedule (m(i:num))`, mk_small_numeral t))) (4*q)) in + let goal = list_mk_conj(map dq (0--3)) in + SUBGOAL_THEN goal STRIP_ASSUME_TAC THENL + [FIRST_ASSUM(MP_TAC o CONJUNCT2 o GEN_REWRITE_RULE I [sha256_hw_inputs]) THEN + DISCH_THEN(fun th -> MP_TAC(end_itlist CONJ (map (fun j -> SPECL [`i:num`; mk_small_numeral j] th) (0--15)))) THEN + ASM_REWRITE_TAC[] THEN CONV_TAC(DEPTH_CONV NUM_RED_CONV) THEN REWRITE_TAC[ADD_CLAUSES] THEN + STRIP_TAC THEN + REWRITE_TAC(SHA256_READ_QUAD :: READ_COMPONENT_COMPOSE :: SHA256_MSCH_SMALL) THEN + ASM_REWRITE_TAC[GSYM WORD_ADD_ASSOC; GSYM WORD_ADD] THEN + CONV_TAC(DEPTH_CONV NUM_ADD_CONV) THEN ASM_REWRITE_TAC[GSYM ADD_ASSOC] THEN + CONV_TAC(DEPTH_CONV NUM_ADD_CONV) THEN ASM_REWRITE_TAC[]; + ALL_TAC];; + +let SHA256_K256_TAC = + FIRST_ASSUM(MP_TAC o CONJUNCT1 o GEN_REWRITE_RULE I [sha256_hw_inputs]) THEN + FIRST_ASSUM(fun th -> + match concl th with + Comb(Comb(Const("=",_),Comb(Comb(Const("read",_),Const("memory",_)),_)),Var("mem0",_)) -> + REWRITE_TAC[SYM th; GSYM READ_COMPONENT_COMPOSE] + | _ -> failwith "") THEN + REWRITE_TAC[GSYM bytes_loaded] THEN + ONCE_REWRITE_TAC[ARITH_RULE `k256 = k256 + 0`] THEN + DISCH_THEN(MP_TAC o MATCH_MP SHA256_HW_K256_QUADS) THEN + REWRITE_TAC[ADD_CLAUSES; WORD_ADD; WORD_ADD_0] THEN STRIP_TAC;; + +(* ------------------------------------------------------------------------- *) +(* Correctness of the loop, from after the prologue to before the epilogue. *) +(* ------------------------------------------------------------------------- *) + +let SHA256_ABBREV_D_TAC = + ABBREV_TAC `d = word_add data (word (64 * i)):int64` THEN + POP_ASSUM(fun th -> RULE_ASSUM_TAC(REWRITE_RULE[th]) THEN ASSUME_TAC th);; +let SHA256_QUAD_INJ = prove + (`!a b c d x y z w:int32. + sha256_quad a b c d = sha256_quad x y z w <=> a = x /\ b = y /\ c = z /\ d = w`, + REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN + DISCH_THEN(fun th -> MAP_EVERY (fun p -> MP_TAC(AP_TERM (subst [p,`p:num#num`] `\q:int128. (word_subword q p:int32)`) th)) [`0,32`; `32,32`; `64,32`; `96,32`]) THEN + REWRITE_TAC[SHA256_QUAD_SUBWORDS] THEN SIMP_TAC[]);; + +let SHA256_READ_QUAD_SPLIT = prove + (`!a s x0 x1 x2 x3. + read (memory :> bytes128 a) s = sha256_quad x0 x1 x2 x3 + ==> read (memory :> bytes32 a) s = x0 /\ + read (memory :> bytes32 (word_add a (word 4))) s = x1 /\ + read (memory :> bytes32 (word_add a (word 8))) s = x2 /\ + read (memory :> bytes32 (word_add a (word 12))) s = x3`, + REWRITE_TAC[SHA256_READ_QUAD; SHA256_QUAD_INJ]);; + +let SHA256_HW_CORRECT = prove + (`!pc k256 state data n h0 h1 h2 h3 h4 h5 h6 h7 m. + 0 < n /\ n < 2 EXP 64 /\ + nonoverlapping (word pc,0x1f0) (state,32) /\ + adrp_within_bounds (word k256) (word (pc + 12)) + ==> ensures arm + (\s. aligned_bytes_loaded s (word pc) (sha256_hw_mc pc k256) /\ + read PC s = word(pc + 0x8) /\ + C_ARGUMENTS [state; data; word n] s /\ + bytes_loaded s (word k256) sha256_hw_k256 /\ + read (memory :> bytes32 state) s = h0 /\ + read (memory :> bytes32 (word_add state (word 4))) s = h1 /\ + read (memory :> bytes32 (word_add state (word 8))) s = h2 /\ + read (memory :> bytes32 (word_add state (word 12))) s = h3 /\ + read (memory :> bytes32 (word_add state (word 16))) s = h4 /\ + read (memory :> bytes32 (word_add state (word 20))) s = h5 /\ + read (memory :> bytes32 (word_add state (word 24))) s = h6 /\ + read (memory :> bytes32 (word_add state (word 28))) s = h7 /\ + (!i j. i < n /\ j < 16 + ==> read (memory :> bytes32 (word_add data (word (64 * i + 4 * j)))) s = + word_bytereverse (EL j (m i)))) + (\s. read PC s = word(pc + 0x1e8) /\ + let h' = sha256_hash_blocks m [h0;h1;h2;h3;h4;h5;h6;h7] n in + read (memory :> bytes32 state) s = EL 0 h' /\ + read (memory :> bytes32 (word_add state (word 4))) s = EL 1 h' /\ + read (memory :> bytes32 (word_add state (word 8))) s = EL 2 h' /\ + read (memory :> bytes32 (word_add state (word 12))) s = EL 3 h' /\ + read (memory :> bytes32 (word_add state (word 16))) s = EL 4 h' /\ + read (memory :> bytes32 (word_add state (word 20))) s = EL 5 h' /\ + read (memory :> bytes32 (word_add state (word 24))) s = EL 6 h' /\ + read (memory :> bytes32 (word_add state (word 28))) s = EL 7 h') + (MAYCHANGE [PC; X1; X2; X3] ,, + MAYCHANGE [Q0; Q1; Q2; Q4; Q5; Q6; Q7; Q16; Q17; Q18; Q19] ,, + MAYCHANGE [events] ,, MAYCHANGE [memory :> bytes(state,32)])`, + MAP_EVERY X_GEN_TAC [`pc:num`; `k256:num`; `state:int64`; `data:int64`; `n:num`; + `h0:int32`; `h1:int32`; `h2:int32`; `h3:int32`; `h4:int32`; `h5:int32`; `h6:int32`; `h7:int32`; + `m:num->int32 list`] THEN + REWRITE_TAC[C_ARGUMENTS; NONOVERLAPPING_CLAUSES; fst SHA256_HW_EXEC; bytes_loaded] THEN + STRIP_TAC THEN + ENSURES_WHILE_UP_TAC `n:num` `pc + 0x14` `pc + 0x1e0` + `\i s. read X0 s = state /\ + read X1 s = word_add data (word (64 * i)) /\ + read X2 s = word (n - i) /\ + read X3 s = word k256 /\ + read Q0 s = sha256_abcd (sha256_hash_blocks m [h0;h1;h2;h3;h4;h5;h6;h7] i) /\ + read Q1 s = sha256_efgh (sha256_hash_blocks m [h0;h1;h2;h3;h4;h5;h6;h7] i) /\ + sha256_hw_inputs k256 data n m (read memory s)` THEN + REPEAT CONJ_TAC THENL + [(* n > 0 *) + ASM_ARITH_TAC; + GHOST_INTRO_TAC `mem0:int64->byte` `read memory` THEN + ENSURES_INIT_TAC "s0" THEN + SUBGOAL_THEN `sha256_hw_inputs k256 data n m mem0` ASSUME_TAC THENL + [FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN + ASM_REWRITE_TAC[sha256_hw_inputs; GSYM READ_COMPONENT_COMPOSE]; ALL_TAC] THEN + SUBGOAL_THEN `read (memory :> bytes128 state) s0 = sha256_quad h0 h1 h2 h3 /\ + read (memory :> bytes128 (word_add state (word 16))) s0 = sha256_quad h4 h5 h6 h7` + STRIP_ASSUME_TAC THENL + [REWRITE_TAC[SHA256_READ_QUAD; GSYM WORD_ADD_ASSOC; GSYM WORD_ADD] THEN + CONV_TAC(DEPTH_CONV NUM_ADD_CONV) THEN ASM_REWRITE_TAC[]; + ALL_TAC] THEN + ARM_STEPS_TAC SHA256_HW_EXEC (1--3) THEN + FIRST_ASSUM(SUBST_ALL_TAC o MATCH_MP ADRP_ADD_FOLD) THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REWRITE_TAC[sha256_hash_blocks; sha256_abcd; sha256_efgh; MULT_CLAUSES; WORD_ADD_0; SUB_0] THEN + CONV_TAC(DEPTH_CONV EL_CONV) THEN ASM_REWRITE_TAC[]; + X_GEN_TAC `i:num` THEN STRIP_TAC THEN + GHOST_INTRO_TAC `mem0:int64->byte` `read memory` THEN + ENSURES_INIT_TAC "s0" THEN SHA256_MEM0_TAC THEN + SHA256_DATA_TAC THEN SHA256_K256_TAC THEN SHA256_ABBREV_D_TAC THEN + SHA256_STEPS_TAC (1--115) THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + REWRITE_TAC[GSYM ADD1; sha256_hash_blocks] THEN REWRITE_TAC[ADD1] THEN + REWRITE_TAC[sha256_block; sha256_abcd; sha256_efgh; SHA256_QUAD_SUBWORDS] THEN + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN CONV_TAC(DEPTH_CONV EL_CONV) THEN REWRITE_TAC[] THEN + REPEAT CONJ_TAC THENL + [REWRITE_TAC[WORD_ADD]; + EXPAND_TAC "d" THEN REWRITE_TAC[GSYM WORD_ADD_ASSOC; GSYM WORD_ADD; LEFT_ADD_DISTRIB; MULT_CLAUSES]; + REWRITE_TAC[WORD_SUB] THEN ASM_SIMP_TAC[ARITH_RULE `i < n ==> i <= n /\ i + 1 <= n`] THEN REWRITE_TAC[WORD_ADD] THEN + CONV_TAC WORD_RULE]; + X_GEN_TAC `i:num` THEN STRIP_TAC THEN + GHOST_INTRO_TAC `mem0:int64->byte` `read memory` THEN + ENSURES_INIT_TAC "s0" THEN SHA256_MEM0_TAC THEN + ARM_STEPS_TAC SHA256_HW_EXEC [1] THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + SUBGOAL_THEN `val (word (n - i):int64) = n - i` SUBST1_TAC THENL + [MATCH_MP_TAC VAL_WORD_EQ THEN REWRITE_TAC[DIMINDEX_64] THEN ASM_ARITH_TAC; + ASM_SIMP_TAC[ARITH_RULE `i < n ==> ~(n - i = 0)`]]; + REWRITE_TAC[SUB_REFL] THEN ENSURES_INIT_TAC "s0" THEN + ARM_STEPS_TAC SHA256_HW_EXEC (1--2) THEN + ENSURES_FINAL_STATE_TAC THEN ASM_REWRITE_TAC[] THEN + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP SHA256_READ_QUAD_SPLIT o + REWRITE_RULE[sha256_abcd; sha256_efgh] o + check (can (term_match [] `read (memory :> bytes128 a) s = x`) o concl))) THEN + REWRITE_TAC[GSYM WORD_ADD_ASSOC; GSYM WORD_ADD] THEN + CONV_TAC(DEPTH_CONV NUM_ADD_CONV) THEN SIMP_TAC[]]);; + +(* ------------------------------------------------------------------------- *) +(* Correctness of the whole function, with its frame and return. *) +(* ------------------------------------------------------------------------- *) + +let SHA256_HW_BYTES_LOADED = prove + (`bytes_loaded s tab sha256_hw_k256 <=> + read (memory :> bytes(tab,320)) s = num_of_bytelist sha256_hw_k256`, + REWRITE_TAC[bytes_loaded; READ_BYTELIST_EQ_BYTES; + CONV_RULE (RAND_CONV LENGTH_CONV) (AP_TERM `LENGTH:byte list->num` sha256_hw_k256)]);; + +let SHA256_HW_SUBROUTINE_CORRECT = prove + (`!pc k256 state data n h0 h1 h2 h3 h4 h5 h6 h7 m stackpointer returnaddress. + 0 < n /\ n < 2 EXP 64 /\ + aligned 16 stackpointer /\ + adrp_within_bounds (word k256) (word (pc + 12)) /\ + ALLPAIRS nonoverlapping + [(state,32); (word_sub stackpointer (word 16),16)] + [(word pc,0x1f0); (data,64 * n); (word k256,320)] /\ + nonoverlapping (state,32) (word_sub stackpointer (word 16),16) + ==> ensures arm + (\s. aligned_bytes_loaded s (word pc) (sha256_hw_mc pc k256) /\ + read PC s = word pc /\ + read SP s = stackpointer /\ + read X30 s = returnaddress /\ + C_ARGUMENTS [state; data; word n] s /\ + bytes_loaded s (word k256) sha256_hw_k256 /\ + read (memory :> bytes32 state) s = h0 /\ + read (memory :> bytes32 (word_add state (word 4))) s = h1 /\ + read (memory :> bytes32 (word_add state (word 8))) s = h2 /\ + read (memory :> bytes32 (word_add state (word 12))) s = h3 /\ + read (memory :> bytes32 (word_add state (word 16))) s = h4 /\ + read (memory :> bytes32 (word_add state (word 20))) s = h5 /\ + read (memory :> bytes32 (word_add state (word 24))) s = h6 /\ + read (memory :> bytes32 (word_add state (word 28))) s = h7 /\ + (!i j. i < n /\ j < 16 + ==> read (memory :> bytes32 (word_add data (word (64 * i + 4 * j)))) s = + word_bytereverse (EL j (m i)))) + (\s. read PC s = returnaddress /\ + let h' = sha256_hash_blocks m [h0;h1;h2;h3;h4;h5;h6;h7] n in + read (memory :> bytes32 state) s = EL 0 h' /\ + read (memory :> bytes32 (word_add state (word 4))) s = EL 1 h' /\ + read (memory :> bytes32 (word_add state (word 8))) s = EL 2 h' /\ + read (memory :> bytes32 (word_add state (word 12))) s = EL 3 h' /\ + read (memory :> bytes32 (word_add state (word 16))) s = EL 4 h' /\ + read (memory :> bytes32 (word_add state (word 20))) s = EL 5 h' /\ + read (memory :> bytes32 (word_add state (word 24))) s = EL 6 h' /\ + read (memory :> bytes32 (word_add state (word 28))) s = EL 7 h') + (MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI ,, + MAYCHANGE [memory :> bytes(state,32); + memory :> bytes(word_sub stackpointer (word 16),16)])`, + REWRITE_TAC[SHA256_HW_BYTES_LOADED; fst SHA256_HW_EXEC] THEN + ARM_ADD_RETURN_STACK_TAC ~pre_post_nsteps:(2,1) SHA256_HW_EXEC + (REWRITE_RULE[SHA256_HW_BYTES_LOADED; fst SHA256_HW_EXEC] SHA256_HW_CORRECT) + `[X29; X30]` 16);; diff --git a/proofs/hol-light/s2n-bignum/x86/proofs/utils/sha256_spec.ml b/proofs/hol-light/s2n-bignum/x86/proofs/utils/sha256_spec.ml new file mode 100644 index 000000000..33131e3b7 --- /dev/null +++ b/proofs/hol-light/s2n-bignum/x86/proofs/utils/sha256_spec.ml @@ -0,0 +1,236 @@ +(* + * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. + * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0 + *) + +(* ========================================================================= *) +(* Specification of the SHA-256 hash computation (FIPS 180-4). *) +(* *) +(* The compression-function primitives sha_choose (Ch), sha_maj (Maj) and *) +(* sha_hash_sigma_0/1 (the "big" Sigma_0/Sigma_1) are reused from the ARM *) +(* SHA-256 intrinsics specification arm/proofs/sha256.ml, which depends *) +(* only on the word library. This file adds the message-schedule sigmas, *) +(* the round-constant table, the message schedule, the compression rounds *) +(* and the (multi-)block hash function, all on int32 list state. *) +(* *) +(* A message block is a list of 16 int32 words, i.e. the 64 data bytes *) +(* already assembled big-endian (FIPS 180-4 section 5.2.1); a hash state is *) +(* a list of 8 int32 words [a;b;c;d;e;f;g;h]. *) +(* ========================================================================= *) + +needs "Library/words.ml";; +needs "arm/proofs/sha256.ml";; + +(* ------------------------------------------------------------------------- *) +(* The message-schedule "small" sigma functions (FIPS 180-4, section 4.1.2). *) +(* ------------------------------------------------------------------------- *) + +let sha_msg_sigma_0 = new_definition + `sha_msg_sigma_0 (x:int32) : int32 = + word_xor (word_ror x 7) (word_xor (word_ror x 18) (word_ushr x 3))`;; + +let sha_msg_sigma_1 = new_definition + `sha_msg_sigma_1 (x:int32) : int32 = + word_xor (word_ror x 17) (word_xor (word_ror x 19) (word_ushr x 10))`;; + +(* ------------------------------------------------------------------------- *) +(* The 64 round constants (FIPS 180-4, section 4.2.2). *) +(* ------------------------------------------------------------------------- *) + +let sha256_constants = define + `sha256_constants:int32 list = + [word 0x428a2f98; word 0x71374491; word 0xb5c0fbcf; word 0xe9b5dba5; + word 0x3956c25b; word 0x59f111f1; word 0x923f82a4; word 0xab1c5ed5; + word 0xd807aa98; word 0x12835b01; word 0x243185be; word 0x550c7dc3; + word 0x72be5d74; word 0x80deb1fe; word 0x9bdc06a7; word 0xc19bf174; + word 0xe49b69c1; word 0xefbe4786; word 0x0fc19dc6; word 0x240ca1cc; + word 0x2de92c6f; word 0x4a7484aa; word 0x5cb0a9dc; word 0x76f988da; + word 0x983e5152; word 0xa831c66d; word 0xb00327c8; word 0xbf597fc7; + word 0xc6e00bf3; word 0xd5a79147; word 0x06ca6351; word 0x14292967; + word 0x27b70a85; word 0x2e1b2138; word 0x4d2c6dfc; word 0x53380d13; + word 0x650a7354; word 0x766a0abb; word 0x81c2c92e; word 0x92722c85; + word 0xa2bfe8a1; word 0xa81a664b; word 0xc24b8b70; word 0xc76c51a3; + word 0xd192e819; word 0xd6990624; word 0xf40e3585; word 0x106aa070; + word 0x19a4c116; word 0x1e376c08; word 0x2748774c; word 0x34b0bcb5; + word 0x391c0cb3; word 0x4ed8aa4a; word 0x5b9cca4f; word 0x682e6ff3; + word 0x748f82ee; word 0x78a5636f; word 0x84c87814; word 0x8cc70208; + word 0x90befffa; word 0xa4506ceb; word 0xbef9a3f7; word 0xc67178f2]`;; + +(* ------------------------------------------------------------------------- *) +(* The initial hash value (FIPS 180-4, section 5.3.3). *) +(* ------------------------------------------------------------------------- *) + +let sha256_iv = define + `sha256_iv:int32 list = + [word 0x6a09e667; word 0xbb67ae85; word 0x3c6ef372; word 0xa54ff53a; + word 0x510e527f; word 0x9b05688c; word 0x1f83d9ab; word 0x5be0cd19]`;; + +(* ------------------------------------------------------------------------- *) +(* The message schedule W_t for a 16-word block m (FIPS 180-4, sec. 6.2.2). *) +(* ------------------------------------------------------------------------- *) + +let sha256_msg_schedule = define + `sha256_msg_schedule (m:int32 list) (t:num) : int32 = + if t < 16 then EL t m + else word_add + (word_add (sha_msg_sigma_1 (sha256_msg_schedule m (t - 2))) + (sha256_msg_schedule m (t - 7))) + (word_add (sha_msg_sigma_0 (sha256_msg_schedule m (t - 15))) + (sha256_msg_schedule m (t - 16)))`;; + +(* ------------------------------------------------------------------------- *) +(* A single compression round on the 8-word working state, with round *) +(* constant k and message-schedule word w (FIPS 180-4, section 6.2.2 step 3).*) +(* ------------------------------------------------------------------------- *) + +let sha256_round = new_definition + `sha256_round (hsh:int32 list) (k:int32) (w:int32) : int32 list = + let a = EL 0 hsh and b = EL 1 hsh and c = EL 2 hsh and d = EL 3 hsh + and e = EL 4 hsh and f = EL 5 hsh and g = EL 6 hsh and h = EL 7 hsh in + let t1 = word_add h + (word_add (sha_hash_sigma_1 e) + (word_add (sha_choose e f g) (word_add k w))) in + let t2 = word_add (sha_hash_sigma_0 a) (sha_maj a b c) in + [word_add t1 t2; a; b; c; word_add d t1; e; f; g]`;; + +(* ------------------------------------------------------------------------- *) +(* n rounds of compression of block m starting from working state hsh. *) +(* ------------------------------------------------------------------------- *) + +let sha256_compress_rounds = define + `sha256_compress_rounds (m:int32 list) (hsh:int32 list) 0 = hsh /\ + sha256_compress_rounds m hsh (n + 1) = + sha256_round (sha256_compress_rounds m hsh n) + (EL n sha256_constants) + (sha256_msg_schedule m n)`;; + +(* ------------------------------------------------------------------------- *) +(* The full compression of one block: 64 rounds then the feed-forward *) +(* addition of the input hash state (FIPS 180-4, section 6.2.2 step 4). *) +(* ------------------------------------------------------------------------- *) + +let sha256_block = new_definition + `sha256_block (m:int32 list) (hsh:int32 list) : int32 list = + let res = sha256_compress_rounds m hsh 64 in + [word_add (EL 0 res) (EL 0 hsh); word_add (EL 1 res) (EL 1 hsh); + word_add (EL 2 res) (EL 2 hsh); word_add (EL 3 res) (EL 3 hsh); + word_add (EL 4 res) (EL 4 hsh); word_add (EL 5 res) (EL 5 hsh); + word_add (EL 6 res) (EL 6 hsh); word_add (EL 7 res) (EL 7 hsh)]`;; + +(* ------------------------------------------------------------------------- *) +(* Hashing n consecutive blocks, where m gives the i'th 16-word block. *) +(* ------------------------------------------------------------------------- *) + +let sha256_hash_blocks = define + `sha256_hash_blocks (m:num->int32 list) (hsh:int32 list) 0 = hsh /\ + sha256_hash_blocks m hsh (n + 1) = + sha256_block (m n) (sha256_hash_blocks m hsh n)`;; + +(* ------------------------------------------------------------------------- *) +(* Length sanity lemmas: everything stays an 8-word state. *) +(* ------------------------------------------------------------------------- *) + +let LENGTH_SHA256_ROUND = prove + (`!hsh k w. LENGTH(sha256_round hsh k w) = 8`, + REPEAT GEN_TAC THEN REWRITE_TAC[sha256_round] THEN + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + CONV_TAC(ONCE_DEPTH_CONV LENGTH_CONV) THEN REFL_TAC);; + +let LENGTH_SHA256_COMPRESS_ROUNDS = prove + (`!m hsh n. LENGTH hsh = 8 + ==> LENGTH(sha256_compress_rounds m hsh n) = 8`, + REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN + INDUCT_TAC THEN + ASM_REWRITE_TAC[sha256_compress_rounds; ADD1; LENGTH_SHA256_ROUND]);; + +let LENGTH_SHA256_BLOCK = prove + (`!m hsh. LENGTH(sha256_block m hsh) = 8`, + REPEAT GEN_TAC THEN REWRITE_TAC[sha256_block] THEN + CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN + CONV_TAC(ONCE_DEPTH_CONV LENGTH_CONV) THEN REFL_TAC);; + +let LENGTH_SHA256_HASH_BLOCKS = prove + (`!m hsh n. LENGTH hsh = 8 + ==> LENGTH(sha256_hash_blocks m hsh n) = 8`, + REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN + INDUCT_TAC THEN + ASM_REWRITE_TAC[sha256_hash_blocks; ADD1; LENGTH_SHA256_BLOCK]);; + +(* ------------------------------------------------------------------------- *) +(* Evaluation of sha256_block on literal arguments, by memoizing one *) +(* theorem per message-schedule word and one per compression round. *) +(* ------------------------------------------------------------------------- *) + +let SHA256_BLOCK_CONV : conv = + let block_pat = `sha256_block m (h:int32 list)` + and msched_pat = `sha256_msg_schedule m t` + and rounds_pat = `sha256_compress_rounds m h t` + and rounds_succ_pat = `sha256_compress_rounds m h (t + 1)` + and el_k_pat = `EL t sha256_constants` + and m_tm = `m:int32 list` and h_tm = `h:int32 list` and t_tm = `t:num` in + let kthm = Array.init 64 (fun t -> + (REWRITE_CONV[sha256_constants] THENC EL_CONV) + (vsubst [mk_small_numeral t,t_tm] el_k_pat)) in + fun tm -> + match tm with + Comb(Comb(Const("sha256_block",_),mtm),htm) -> + let inst t pat = + vsubst [mtm,m_tm; htm,h_tm; mk_small_numeral t,t_tm] pat in + let msched = Array.make 64 TRUTH in + (for t = 0 to 15 do + msched.(t) <- + CONV_RULE(RAND_CONV(DEPTH_CONV NUM_RED_CONV THENC + REWRITE_CONV[] THENC EL_CONV)) + (REWR_CONV sha256_msg_schedule (inst t msched_pat)) + done; + for t = 16 to 63 do + msched.(t) <- + CONV_RULE(RAND_CONV(DEPTH_CONV NUM_RED_CONV THENC + REWRITE_CONV[msched.(t-2); msched.(t-7); msched.(t-15); + msched.(t-16); + sha_msg_sigma_0; sha_msg_sigma_1] THENC + WORD_REDUCE_CONV)) + (REWR_CONV sha256_msg_schedule (inst t msched_pat)) + done); + let round_th = Array.make 65 TRUTH in + round_th.(0) <- + REWRITE_CONV[sha256_compress_rounds] (inst 0 rounds_pat); + for t = 0 to 63 do + round_th.(t+1) <- + CONV_RULE(LAND_CONV(RAND_CONV NUM_RED_CONV)) + ((REWRITE_CONV[sha256_compress_rounds] THENC + REWRITE_CONV[round_th.(t); kthm.(t); msched.(t); + sha256_round] THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV EL_CONV THENC + REWRITE_CONV[sha_choose; sha_maj; + sha_hash_sigma_0; sha_hash_sigma_1] THENC + WORD_REDUCE_CONV) (inst t rounds_succ_pat)) + done; + CONV_RULE(RAND_CONV( + REWRITE_CONV[round_th.(64)] THENC + TOP_DEPTH_CONV let_CONV THENC + DEPTH_CONV EL_CONV THENC + WORD_REDUCE_CONV)) + (REWR_CONV sha256_block tm) + | _ -> failwith "SHA256_BLOCK_CONV: inapplicable";; + +(* ------------------------------------------------------------------------- *) +(* Spec KAT: FIPS 180-4 single-block known answer, SHA256("abc"). *) +(* "abc" padded per section 5.1.1 and assembled big-endian per 5.2.1; *) +(* expected digest ba7816bf 8f01cfea 414140de 5dae2223 *) +(* b00361a3 96177a9c b410ff61 f20015ad. *) +(* Failure of this proof means the spec is wrong; it gates every load. *) +(* ------------------------------------------------------------------------- *) + +let SHA256_ABC_KAT = prove + (`sha256_block + [word 0x61626380; word 0; word 0; word 0; + word 0; word 0; word 0; word 0; + word 0; word 0; word 0; word 0; + word 0; word 0; word 0; word 0x18] + sha256_iv = + [word 0xba7816bf; word 0x8f01cfea; word 0x414140de; word 0x5dae2223; + word 0xb00361a3; word 0x96177a9c; word 0xb410ff61; word 0xf20015ad]`, + REWRITE_TAC[sha256_iv] THEN + CONV_TAC(LAND_CONV SHA256_BLOCK_CONV) THEN REFL_TAC);; diff --git a/quest/m2/verified/README.md b/quest/m2/verified/README.md index d383f16f9..3e957c0e3 100644 --- a/quest/m2/verified/README.md +++ b/quest/m2/verified/README.md @@ -16,5 +16,4 @@ Staging (maintainer, 2026-11-09): ✅ calibrate first, and move the cold tiers t - [The hash and KDF glue's constant-time compares are proven](/quest/m2/verified/hash-glue.md) - the compares behind `hmac::verify` and `pbkdf2::Secret::verify`, in HOL Light - [HKDF's key conversions are proven](/quest/m2/verified/hkdf-okm.md) - the `From` keys QUIC's packet protection starts from -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [The Lean models of CPU intrinsics are tested against the instructions](/quest/m2/verified/simd-models.md) - a model that misreads the manual fails `admin/prove` diff --git a/quest/m2/verified/sha256-aarch64-hw.md b/quest/m2/verified/sha256-aarch64-hw.md deleted file mode 100644 index 2ced1e8db..000000000 --- a/quest/m2/verified/sha256-aarch64-hw.md +++ /dev/null @@ -1,24 +0,0 @@ -# [L] aarch64 SHA-256 on the SHA-2 instructions is proven - -## Goal - -SHA-256, and HMAC, HKDF, and PBKDF2 over it, earn the ✓ on aarch64 with the crypto extension, the hash under every TLS 1.3 handshake's transcript and key schedule there. Its PR also reports what the proof cost and how an SMT-backed route compares on the same routine, the measurement every later proof of unproven assembly is sized from. - -## Plan - -Staging (maintainer, 2026-11-09): ✅ calibrate first, and move the cold tiers to m5 (rejected: calibrate only, leave the 2026-11-07 plan). This is the calibration: the first HOL Light proof rind writes for assembly nobody has proven, picked because it is the smallest such routine on a hot path. Every other quest that writes one requires it. - -- Runs: aws-lc's `sha256_block_data_order_hw` (`low/aarch64/aws_lc/sha256_block_data_order_hw.*.s`, 123 instructions), under the padding, HMAC, HKDF, and PBKDF2 glue `proofs/` proves. It keeps a register copy off each round's dependency chain, where LLVM's code for rind's intrinsics puts one on it, so it is faster than those intrinsics. pyca's Lean-proven routine is 1.9x slower. -- Already proven: nothing. s2n-bignum models `sha256h`, `sha256h2`, `sha256su0`, and `sha256su1` but has no SHA-256 routine. -- Route: a HOL Light proof of the routine in s2n-bignum's aarch64 model against [awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415)'s FIPS 180-4 SHA-256 spec, which [#450](https://github.com/awslabs/s2n-bignum/pull/450)'s x86_64 proof also uses, estimated at 3-5 person-weeks for someone fluent in s2n-bignum. It then enters `proofs/Rind/Aarch64/ShaBlocks.lean` as an axiom, retiring that hypothesis's SHA-256 half on this tier. -- Spec pin: build on [awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415)'s spec at a pinned commit while it is unmerged, and move to the merged version when it lands; `benchmarks/verified.toml`'s ✓ notes the pin (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). Both PRs keep the spec in `x86/proofs/utils/sha256_spec.ml`, so an aarch64 proof loads it from the x86 tree. On 2026-11-09 both were drafts, #415 untouched since 2026-06-23 and #450 since 2026-09-08. -- How the pin comes in: consider vendoring s2n-bignum (maintainer, 2026-11-09). It is a submodule at one upstream commit today (`thirdparty/s2n-bignum`). A draft PR's commit can vanish on a force-push, and one submodule commit cannot hold #415, #420, and #450 at once without a fork, which the 2026-11-07 decision rejected. Recommended: keep the submodule for merged upstream, and vendor only the unmerged spec and proof files into `proofs/hol-light/`, each with its source PR and commit recorded; vendor the whole tree only if that cannot build. This quest is the first to build on a pin, so it settles the question for [the x86_64 SHA-256 proof](/quest/m3/verified/sha256-block.md) and the rest. -- Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - -The measurement, in the PR's body: - -- The cost of the HOL Light proof: its lines, split into the proof, its lemmas, and any addition to the instruction model; the agent sessions and wall time it took; the time `admin/prove` takes to check it, against the `prove` workflow's 60 minutes (`.github/workflows/prove.yml:30`); and each place it stalled, with what moved it on. -- The same figures for the Lean side: restating the theorem as an axiom, and bridging s2n-bignum's SHA-256 spec to `Rind/HashSpec.lean`'s. -- For scale, upstream's own proofs, neither merged: #450 proves its SHA-NI routine, a 299-line source file, in 13,570 lines of HOL Light, and #415 its scalar one, 1,429 lines, in 12,830. -- A second route on the same routine: prove it by symbolic execution with an SMT solver or a bit-vector decision procedure, such as SAW, which aws-lc-verification's SHA-512 proof that `proofs/Rind/X86_64/AwsLc.lean` restates used, or Lean's `bv_decide` over a small model of the instructions the routine runs. Report its cost in the same figures, what it trusts that the HOL Light proof does not (the solver, its instruction model, how its theorem would enter under the composition rule), and where it stopped if it did not finish. -- From both, a proposed size for each quest that requires this one, given its routine's instruction count and whether it loops, branches, or needs instructions the model lacks. Which route those quests take stays HOL Light in `proofs/hol-light/` unless the maintainer picks otherwise from this report; the ✓ here rests on the HOL Light proof. diff --git a/quest/m3/verified/README.md b/quest/m3/verified/README.md index d0afe76d0..6b78c0c0a 100644 --- a/quest/m3/verified/README.md +++ b/quest/m3/verified/README.md @@ -38,7 +38,7 @@ Decided with the maintainer on 2026-11-03, after the benchmark report (`BENCHMAR - armv7 without NEON keeps aws-lc's integer ChaCha20 and SHA-512 block function, which should be proven instead ([moq-dev/rind#327](https://github.com/moq-dev/rind/pull/327)). libcrux's HACL\* SHA-512 measured 6-7% slower at every size, and its AEAD 1-8% slower from 512 B; its compiled decrypt also checks the tag with early-exit branches, which rules it out with NEON too, where it seals 1.09-1.18x faster up to 64 B. The maintainer's rule (2026-11-03) keeps a verified switch only where it is at least as fast at every size. - Accepted unless a route changes it: AES and GHASH on x86_64 without AVX, aarch64 without the crypto extension, and armv7; VAES AES-GCM; SIMD ChaCha20-Poly1305; x86_64 P-256 generator multiplication (s2n-bignum's proven routine cost 12-17%); RSA off x86_64 ADX and key generation; armv7's curves; SHA-1; parsing for now. - AES-GCM on the Vale tier for AAD or messages of 2^32 bytes and more (2026-11-07, from [moq-dev/rind#480](https://github.com/moq-dev/rind/pull/480)): Vale's routines cannot resume a GHASH or counter across chunks, so these run by-8, which [x86_64's by-8 and by-16 AES-GCM intrinsics are proven](/quest/m4/verified/aes-gcm-x86-intrinsics.md) proves along with the tier's short seals. - - aarch64 SHA-256 on the SHA-2 instructions (2026-11-03): nothing proven runs at full speed, so [its proof](/quest/m2/verified/sha256-aarch64-hw.md) is planned on a pinned commit of the unmerged spec, as the calibration for every later HOL Light proof. s2n-bignum models the instructions but has no SHA-2 routine, and pyca/verified-garbage's Lean-proven one is 1.9x slower. Once #450's FIPS 180-4 spec lands, revisit a HOL Light proof of aws-lc's `sha256_block_data_order_hw` on it: 123 instructions, an estimated 3-5 person-weeks for someone fluent in s2n-bignum. + - aarch64 SHA-256 on the SHA-2 instructions (2026-11-03): nothing proven runs at full speed, so its proof was planned on a pinned commit of the unmerged spec, as the calibration for every later HOL Light proof, and landed in [moq-dev/rind#552](https://github.com/moq-dev/rind/pull/552). s2n-bignum models the instructions but has no SHA-2 routine, and pyca/verified-garbage's Lean-proven one is 1.9x slower. - Randomness, including the HMAC-DRBG behind ECDSA's hedged nonces, is outside the functional spec: a proof shows the output is right for whatever was drawn. ## Required diff --git a/quest/m3/verified/sha256-block.md b/quest/m3/verified/sha256-block.md index 7dc3dca15..1f4993a36 100644 --- a/quest/m3/verified/sha256-block.md +++ b/quest/m3/verified/sha256-block.md @@ -1,4 +1,4 @@ -# [L] x86_64 SHA-NI SHA-256 block function is proven +# [M] x86_64 SHA-NI SHA-256 block function is proven ## Goal @@ -16,10 +16,6 @@ Route (maintainer, 2026-11-09: ✅ start on #450 at a pinned commit; rejected: k 1. Measure its `sha256_compress_hw` against today's routine on the GitHub runners and on Arrow Lake, rows up to 64 bytes and HMAC included. Switch only if it ties at every size. 2. Otherwise, freeze LLVM's output for today's routine as assembly and prove it on #450's spec in HOL Light, adding to s2n-bignum's x86_64 model any instruction that output uses and #450 does not add. -aarch64's routine is proven in [the calibration quest](/quest/m2/verified/sha256-aarch64-hw.md), on the same FIPS 180-4 spec. +aarch64's routine is proven on the same FIPS 180-4 spec, in `proofs/hol-light/aarch64/sha256_block_data_order_hw.ml` ([moq-dev/rind#552](https://github.com/moq-dev/rind/pull/552)), whose body measures what such a proof costs. -Consider vendoring s2n-bignum rather than pinning it (maintainer, 2026-11-09). Today it is a submodule at one upstream commit (`thirdparty/s2n-bignum`, 90 MB checked out). A draft PR's commit can vanish on a force-push, and one submodule commit cannot hold #415, #420, and #450 at once without a fork, which the 2026-11-07 decision rejected. Recommended: keep the submodule for merged upstream, and vendor only the unmerged spec and proof files into `proofs/hol-light/`, each with its source PR and commit recorded; vendor the whole tree only if that cannot build. The calibration quest is the first to build on a pin, so it settles this and this quest follows it. - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs, and how unmerged upstream comes in +Unmerged upstream comes in as the calibration settled: the submodule stays at merged upstream, and each unmerged s2n-bignum file rind needs is vendored unchanged under `proofs/hol-light/s2n-bignum/`, at its upstream path, ahead of the submodule on HOL Light's load path, with its PR and commit in `proofs/README.md`. Vendor #450's model additions and spec the same way. diff --git a/quest/m4/verified/README.md b/quest/m4/verified/README.md index 5dca44152..16d77f373 100644 --- a/quest/m4/verified/README.md +++ b/quest/m4/verified/README.md @@ -10,7 +10,7 @@ Decided with the maintainer on 2026-11-07, planning m4's long-term work with no - Prove the fast code rind runs; never swap in slower verified code to earn a ✓. Where no proof of a routine exists, write one in HOL Light, in [`proofs/hol-light/`](/proofs/README.md#hol-light-proofs), or in Lean. Offering it upstream is optional, with no standing approval: each quest stops and asks the maintainer before posting to awslabs/s2n-bignum or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - The m3 epic's settled choices hold: Aeneas to Lean for rind's Rust, and its composition rule. -- Staging (maintainer, 2026-11-09, after an audit found most children are person-months of HOL Light with no measured cost and nothing ordering them): ✅ calibrate first, and move the cold tiers to m5 (rejected: calibrate only, leave this plan as written). [The aarch64 SHA-256 proof](/quest/m2/verified/sha256-aarch64-hw.md) moved to m2 as the calibration, and every child here that writes new HOL Light requires it. armv7, MD5, SHA-1, and the tiers without AES or SHA hardware moved to [m5](/quest/m5/verified/README.md). +- Staging (maintainer, 2026-11-09, after an audit found most children are person-months of HOL Light with no measured cost and nothing ordering them): ✅ calibrate first, and move the cold tiers to m5 (rejected: calibrate only, leave this plan as written). The aarch64 SHA-256 proof moved to m2 as the calibration and landed in [moq-dev/rind#552](https://github.com/moq-dev/rind/pull/552), whose body proposes a size for each child here that writes new HOL Light. armv7, MD5, SHA-1, and the tiers without AES or SHA hardware moved to [m5](/quest/m5/verified/README.md). - Audit ([moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448), 2026-11-06), counting [the m3 epic](/quest/m3/verified/README.md)'s open quests as done: the ✓ then holds for X25519 and ChaCha20 header protection on x86_64 and aarch64, P-256 on aarch64, AES-GCM on x86_64's Vale tier, SHA-256 and its MACs and KDFs on x86_64 with SHA-NI, and SHA-384/512 and Ed25519 on Intel x86_64 with AVX but not AVX2 and on aarch64 without the SHA-512 instructions. Every other cell is a child below, ranked by how often the operation and tier run. - Upstream since m3: s2n-bignum proves aarch64 AES-GCM against SP 800-38D, out of place only, and models the aarch64 SHA-512 instructions; its FIPS 180-4 specs and x86_64 SHA-NI proof ([awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415), [#420](https://github.com/awslabs/s2n-bignum/pull/420), [#450](https://github.com/awslabs/s2n-bignum/pull/450)) are still open. No proof covers the ChaCha20-Poly1305 or VAES AES-GCM assembly rind runs, or any aarch64 ChaCha20 or Poly1305; aws-lc-verification and HACL\* have added nothing rind runs. - Most children write HOL Light for assembly no one has proven. Decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448): those proofs live in [`proofs/hol-light/`](/proofs/README.md#hol-light-proofs), run by `admin/prove` beside the Lean proofs over a pinned or vendored s2n-bignum, not in a fork. The SHA-2 children may pin [awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415)'s and [#420](https://github.com/awslabs/s2n-bignum/pull/420)'s unmerged specs by commit, moving to the merged versions when they land, with the ✓ noting the pin. diff --git a/quest/m4/verified/aes-gcm-aarch64-192.md b/quest/m4/verified/aes-gcm-aarch64-192.md index 386c116f8..7f88d503e 100644 --- a/quest/m4/verified/aes-gcm-aarch64-192.md +++ b/quest/m4/verified/aes-gcm-aarch64-192.md @@ -11,12 +11,11 @@ Found by the 2026-11-09 audit: [moq-dev/rind#460](https://github.com/moq-dev/rin - Runs (`low/aarch64/aes_gcm.rs:310-316`, `:340-379`): `low/aarch64/aws_lc/aesv8_gcm_8x_{enc,dec}_192.*.s`, 1,393 and 1,383 lines from aws-lc's `aesv8-gcm-armv8-unroll8.pl`, eight blocks at a time on `eor3`, called past the short pass's lengths with a whole number of blocks, the same input and output pointer, the running GHASH, the counter block, 13 round keys, and the 12-entry H table. Cores without SHA3 run AES-CTR and GHASH in turn, which [AES-GCM on aarch64](/quest/m4/verified/aes-gcm-aarch64.md) proves. - Already proven: nothing of these two. s2n-bignum has no AES-192 kernel and no PR for one (searched 2026-11-09). Its `aes{128,256}_gcm_{enc,dec}_alt` are whole-block forms of the same aws-lc eight-way code, proven against `common/gcm.ml`: at rind's pin `arm/proofs/aes128_gcm_enc_alt.ml` is 11,713 lines for a 1,939-line source, and `aes256_gcm_dec_alt.ml` 14,358. The draft [awslabs/s2n-bignum#490](https://github.com/awslabs/s2n-bignum/pull/490) moves most of each into shared files (`aes_gcm_enc_alt_proof.ml`, `aes_gcm_dec_alt_common.ml`) and cuts `aes128_gcm_enc_alt.ml` to about 1,800 lines, with in-place use allowed. - Route: HOL Light proofs of rind's two routines in `proofs/hol-light/`, built on those shared files once #490 is in the pin, for 12 rounds, with the precondition rind's call meets (a nonzero whole number of blocks, `in_p = out_p`). aws-lc's routines also take a partial last block, masked in their tail, where the s2n-bignum forms return at once for one; rind passes whole blocks, so the theorem is stated for those, and the tail's masking is the code that differs most from the proven forms. Then an axiom per routine in `proofs/Rind/Aarch64/`, and the two match arms join the Lean proof of `aes_gcm.rs`. -- Sized XL on the pinned proofs' length. If #490's shared proof takes a 12-round instance cheaply, this is far smaller: re-size it from [the calibration](/quest/m2/verified/sha256-aarch64-hw.md) and from #490 as merged. +- Sized XL on the pinned proofs' length. If #490's shared proof takes a 12-round instance cheaply, this is far smaller: re-size it from the calibration in [moq-dev/rind#552](https://github.com/moq-dev/rind/pull/552) and from #490 as merged. - Traffic is low: no TLS 1.3 or QUIC cipher suite uses AES-192, so this ranks behind every AES-128 and AES-256 proof. - Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [aarch64's AES-GCM kernels are proven in place](/quest/m4/verified/aes-gcm-aarch64-in-place.md) - the pin with s2n-bignum's shared eight-way proofs and in-place theorems - [AES-GCM on aarch64 is proven](/quest/m4/verified/aes-gcm-aarch64.md) - the Lean proof of `aes_gcm.rs` these kernels' axioms slot into diff --git a/quest/m4/verified/aes-gcm-x86-vaes.md b/quest/m4/verified/aes-gcm-x86-vaes.md index 86d8a75e6..179475d2c 100644 --- a/quest/m4/verified/aes-gcm-x86-vaes.md +++ b/quest/m4/verified/aes-gcm-x86-vaes.md @@ -22,5 +22,4 @@ AES-GCM earns the ✓ on x86_64 CPUs with VAES and VPCLMULQDQ (Ice Lake and late ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [x86_64's by-8 and by-16 AES-GCM intrinsics are proven](/quest/m4/verified/aes-gcm-x86-intrinsics.md) - the short messages this tier hands to them diff --git a/quest/m4/verified/aes-modes.md b/quest/m4/verified/aes-modes.md index baa7855b8..a9d9b9d29 100644 --- a/quest/m4/verified/aes-modes.md +++ b/quest/m4/verified/aes-modes.md @@ -12,5 +12,4 @@ ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [AES and QUIC AES header protection are proven with AES hardware](/quest/m4/verified/aes-header-protection.md) - the block cipher and its intrinsic models diff --git a/quest/m4/verified/chacha20-poly1305-aarch64.md b/quest/m4/verified/chacha20-poly1305-aarch64.md index fe43cc452..d0fa643d9 100644 --- a/quest/m4/verified/chacha20-poly1305-aarch64.md +++ b/quest/m4/verified/chacha20-poly1305-aarch64.md @@ -13,5 +13,4 @@ ChaCha20-Poly1305, XChaCha20-Poly1305, and `cipher::ChaCha20` earn the ✓ on aa ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [ChaCha20-Poly1305 is proven on x86_64](/quest/m4/verified/chacha20-poly1305-x86.md) - the HOL Light ChaCha20 and Poly1305 specs and the shared glue's proof diff --git a/quest/m4/verified/chacha20-poly1305-x86.md b/quest/m4/verified/chacha20-poly1305-x86.md index 393ff2ac4..70d04409e 100644 --- a/quest/m4/verified/chacha20-poly1305-x86.md +++ b/quest/m4/verified/chacha20-poly1305-x86.md @@ -12,7 +12,3 @@ ChaCha20-Poly1305 and XChaCha20-Poly1305, TLS's and QUIC's other AEAD, and `ciph - Route otherwise: write ChaCha20 and Poly1305 specs in HOL Light against RFC 8439, and prove aws-lc's routines in s2n-bignum's x86_64 model, whose AVX2 decoding is broad; prove the AEAD glue and HChaCha20 with Aeneas, and rind's AVX2 ChaCha20 kernels (`low/x86_64/chacha20.rs`) with Aeneas over modelled intrinsics. - The specs are [aarch64's quest](/quest/m4/verified/chacha20-poly1305-aarch64.md)'s too. - Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs diff --git a/quest/m4/verified/p256-x86.md b/quest/m4/verified/p256-x86.md index 8b1b104cf..26a6d8a16 100644 --- a/quest/m4/verified/p256-x86.md +++ b/quest/m4/verified/p256-x86.md @@ -13,7 +13,3 @@ P-256 key agreement, ECDSA signing, and ECDSA verification, which every TLS cert 2. k·G: HOL Light proofs of aws-lc's select and mixed-addition routines in s2n-bignum's x86_64 model against its P-256 specs, then Aeneas for the Booth driver, and a proof that the x86_64 table holds the multiples of G those proofs assume, as `Rind/Aarch64/P256Table.lean` does. Verification's u1·G reads the same table. 3. Run `admin/prove`'s P-256 proofs on x86_64, with its own axioms in `Rind/X86_64/S2nBignum.lean` (the ADX routines and their `_alt` forms). - Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs diff --git a/quest/m4/verified/rsa-aarch64-mont.md b/quest/m4/verified/rsa-aarch64-mont.md index 441b8df71..d1c8315e4 100644 --- a/quest/m4/verified/rsa-aarch64-mont.md +++ b/quest/m4/verified/rsa-aarch64-mont.md @@ -10,7 +10,3 @@ aws-lc's aarch64 `bn_mul_mont`, which rind runs for every RSA modulus there, is - Route: prove each routine in s2n-bignum's aarch64 model, scalar instructions only, against `bignum_montmul`'s specification. The width-generic loops need loop invariants like s2n-bignum's own generic `bignum_montmul`'s. - Import the theorems into `proofs/Rind/Aarch64/` as axioms under the composition rule, retiring the products hypothesis on aarch64. - Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs diff --git a/quest/m4/verified/rsa-x86-ifma.md b/quest/m4/verified/rsa-x86-ifma.md index 85bec562f..e15c23e7f 100644 --- a/quest/m4/verified/rsa-x86-ifma.md +++ b/quest/m4/verified/rsa-x86-ifma.md @@ -13,5 +13,4 @@ On x86_64 CPUs with AVX-512 IFMA (Ice Lake and later, Zen 4 and later), where bo ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [RSA signing, decryption, and key generation are proven](/quest/m4/verified/rsa-sign.md) - the CRT glue this exponentiation slots into diff --git a/quest/m4/verified/rsa-x86-mont.md b/quest/m4/verified/rsa-x86-mont.md index 126452d78..9f7c79ece 100644 --- a/quest/m4/verified/rsa-x86-mont.md +++ b/quest/m4/verified/rsa-x86-mont.md @@ -1,4 +1,4 @@ -# [XL] x86_64's other RSA Montgomery products are proven +# [L] x86_64's other RSA Montgomery products are proven ## Goal @@ -10,7 +10,3 @@ Every RSA Montgomery product x86_64 runs outside s2n-bignum's Karatsuba routines - Route: HOL Light proofs in s2n-bignum's x86_64 model against its Montgomery specification; RSAZ AVX2 needs the 29-bit-limb representation's lemmas and any AVX2 instruction the model lacks. - Import the theorems as axioms, retiring the products hypothesis [RSA verification](/quest/m4/verified/rsa-verify.md) leaves for these paths. - Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs diff --git a/quest/m4/verified/sha256-x86-avx2.md b/quest/m4/verified/sha256-x86-avx2.md index 33f1837bf..f15938b0f 100644 --- a/quest/m4/verified/sha256-x86-avx2.md +++ b/quest/m4/verified/sha256-x86-avx2.md @@ -11,7 +11,3 @@ SHA-256, and HMAC, HKDF, and PBKDF2 over it, earn the ✓ on x86_64 CPUs with AV - Route: a HOL Light proof in s2n-bignum's x86_64 model against [awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415)'s FIPS 180-4 SHA-256 spec, sharing the AVX2 model work with [x86_64 SHA-512 on AVX2](/quest/m4/verified/sha512-x86-avx2.md), whose routine comes from the same `sha512-x86_64.pl`. It enters `proofs/Rind/X86_64/ShaBlocks.lean` as an axiom. - Spec pin: build on [awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415)'s spec at a pinned commit while it is unmerged, and move to the merged version when it lands; `benchmarks/verified.toml`'s ✓ notes the pin (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs diff --git a/quest/m4/verified/sha512-aarch64-hw.md b/quest/m4/verified/sha512-aarch64-hw.md index 4214bc196..1c157a744 100644 --- a/quest/m4/verified/sha512-aarch64-hw.md +++ b/quest/m4/verified/sha512-aarch64-hw.md @@ -11,7 +11,3 @@ SHA-384, SHA-512, and SHA-512/256, and with them Ed25519 and HMAC and HKDF over - Route: a HOL Light proof of the whole routine in s2n-bignum's aarch64 model, which already models `sha512h`, `sha512h2`, `sha512su0`, and `sha512su1`, against [awslabs/s2n-bignum#420](https://github.com/awslabs/s2n-bignum/pull/420)'s FIPS 180-4 SHA-512 spec, then an axiom in `proofs/Rind/Aarch64/AwsLc.lean` beside the `nohw` one. This also drops NSym's ArmSpecGap caveat from this path. - Spec pin: build on [awslabs/s2n-bignum#420](https://github.com/awslabs/s2n-bignum/pull/420)'s spec at a pinned commit while it is unmerged, and move to the merged version when it lands; `benchmarks/verified.toml`'s ✓ notes the pin (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs diff --git a/quest/m4/verified/sha512-x86-avx2.md b/quest/m4/verified/sha512-x86-avx2.md index 971c4c3d6..5589d5055 100644 --- a/quest/m4/verified/sha512-x86-avx2.md +++ b/quest/m4/verified/sha512-x86-avx2.md @@ -11,7 +11,3 @@ SHA-384, SHA-512, and SHA-512/256, and with them Ed25519 and HMAC and HKDF over - Route: a HOL Light proof in s2n-bignum's x86_64 model, whose AVX2 decoding is broad (add any instruction the routine uses that it lacks, such as BMI2's `rorx`), against [awslabs/s2n-bignum#420](https://github.com/awslabs/s2n-bignum/pull/420)'s FIPS 180-4 SHA-512 spec. Then an axiom in `proofs/Rind/X86_64/AwsLc.lean`'s place for this routine, and `RunsSha512` widened to this tier. - Spec pin: build on [awslabs/s2n-bignum#420](https://github.com/awslabs/s2n-bignum/pull/420)'s spec at a pinned commit while it is unmerged, and move to the merged version when it lands; `benchmarks/verified.toml`'s ✓ notes the pin (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs diff --git a/quest/m4/verified/sha512-x86-ext.md b/quest/m4/verified/sha512-x86-ext.md index 7f851c494..7763a9722 100644 --- a/quest/m4/verified/sha512-x86-ext.md +++ b/quest/m4/verified/sha512-x86-ext.md @@ -14,5 +14,4 @@ SHA-384, SHA-512, SHA-512/256, Ed25519, and HMAC and HKDF over SHA-384 earn the ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [x86_64 SHA-512 on AVX2 is proven](/quest/m4/verified/sha512-x86-avx2.md) - the SHA-512 spec work and the `RunsSha512` widening this extends diff --git a/quest/m5/verified-armv7/assembly.md b/quest/m5/verified-armv7/assembly.md index 5aade726c..740d2d0d5 100644 --- a/quest/m5/verified-armv7/assembly.md +++ b/quest/m5/verified-armv7/assembly.md @@ -20,7 +20,6 @@ Route: prove each against the HOL Light or Lean specs the x86_64 and aarch64 que ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [An AArch32 instruction model checks armv7's assembly](/quest/m5/verified-armv7/model.md) - the model the proofs run on - [armv7 runs the Rust proofs](/quest/m5/verified-armv7/prove.md) - the armv7 translation these routines' theorems compose with - [ChaCha20-Poly1305 is proven on x86_64](/quest/m4/verified/chacha20-poly1305-x86.md) - the RFC 8439 ChaCha20 and Poly1305 specs and the AEAD glue's proof diff --git a/quest/m5/verified-armv7/curve25519.md b/quest/m5/verified-armv7/curve25519.md index 29d97c93f..9ebf039b4 100644 --- a/quest/m5/verified-armv7/curve25519.md +++ b/quest/m5/verified-armv7/curve25519.md @@ -12,6 +12,5 @@ X25519 and Ed25519 earn the ✓ on armv7. ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [armv7 runs the Rust proofs](/quest/m5/verified-armv7/prove.md) - the armv7 translation - [An AArch32 instruction model checks armv7's assembly](/quest/m5/verified-armv7/model.md) - the model `neon2`'s proof runs on diff --git a/quest/m5/verified-armv7/model.md b/quest/m5/verified-armv7/model.md index 0133cb5fd..ed11da6b0 100644 --- a/quest/m5/verified-armv7/model.md +++ b/quest/m5/verified-armv7/model.md @@ -11,7 +11,3 @@ A machine-checked model of the 32-bit Arm instructions armv7's assembly uses, in - Options, for the maintainer to pick from what this finds: extend s2n-bignum with an AArch32 model in HOL Light (its tactics and specs carry over; asking s2n-bignum whether they would take it is a post outside the moq-dev and kixelated orgs, so stop and ask the maintainer first, with no standing approval), or a Lean model derived from Arm's ASL through Sail if it covers AArch32, so armv7's proofs live beside `proofs/`. - Validate the model against hardware or qemu by random-instruction testing, as s2n-bignum validates its own. - Prove the smallest routine first, `low/arm/bignum_eq.rs`'s compare, to exercise the model end to end. - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs diff --git a/quest/m5/verified/aarch64-no-crypto.md b/quest/m5/verified/aarch64-no-crypto.md index 3dad9de52..279cc6e18 100644 --- a/quest/m5/verified/aarch64-no-crypto.md +++ b/quest/m5/verified/aarch64-no-crypto.md @@ -14,5 +14,4 @@ Every operation earns the ✓ on aarch64 cores without the crypto extension (the ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [AES-GCM on aarch64 is proven](/quest/m4/verified/aes-gcm-aarch64.md) - the AEAD glue this tier shares diff --git a/quest/m5/verified/sha1.md b/quest/m5/verified/sha1.md index 7ae084ebb..850e89af5 100644 --- a/quest/m5/verified/sha1.md +++ b/quest/m5/verified/sha1.md @@ -1,4 +1,4 @@ -# [L] SHA-1 is proven on every x86_64 and aarch64 tier +# [XL] SHA-1 is proven on every x86_64 and aarch64 tier ## Goal @@ -15,7 +15,3 @@ Runs, block function by tier, under padding and HMAC glue that `proofs/` already Each enters as the `ShaBlocks` hypothesis's SHA-1 half does today, which this retires. - Upstream: offering this work to awslabs/s2n-bignum is optional, and there is no standing approval: stop and ask the maintainer before posting there or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)). - -## Required - -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs diff --git a/quest/m5/verified/sha2-x86-no-avx2.md b/quest/m5/verified/sha2-x86-no-avx2.md index b3827b70c..180fc693a 100644 --- a/quest/m5/verified/sha2-x86-no-avx2.md +++ b/quest/m5/verified/sha2-x86-no-avx2.md @@ -14,6 +14,5 @@ SHA-256, SHA-384, and SHA-512, and the MACs and KDFs over them, earn the ✓ on ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [x86_64 SHA-256 on AVX2 without SHA-NI is proven](/quest/m4/verified/sha256-x86-avx2.md) - the SHA-256 spec work and its `ShaBlocks` axiom shape - [x86_64 SHA-512 on AVX2 is proven](/quest/m4/verified/sha512-x86-avx2.md) - the SHA-512 spec work and the `RunsSha512` widening diff --git a/quest/m5/verified/x86-no-aesni.md b/quest/m5/verified/x86-no-aesni.md index 4c1f67bee..c2f83d368 100644 --- a/quest/m5/verified/x86-no-aesni.md +++ b/quest/m5/verified/x86-no-aesni.md @@ -14,5 +14,4 @@ AES-GCM, AES header protection, and the AES modes earn the ✓ on x86_64 CPUs wi ## Required -- [aarch64 SHA-256 on the SHA-2 instructions is proven](/quest/m2/verified/sha256-aarch64-hw.md) - the calibration: what a hand-written HOL Light proof of unproven assembly costs - [x86_64's by-8 and by-16 AES-GCM intrinsics are proven](/quest/m4/verified/aes-gcm-x86-intrinsics.md) - the AES-GCM glue and specs this tier reuses diff --git a/rind/src/low/aarch64/sha256.rs b/rind/src/low/aarch64/sha256.rs index 76aaa4a1e..296aae5f5 100644 --- a/rind/src/low/aarch64/sha256.rs +++ b/rind/src/low/aarch64/sha256.rs @@ -3,10 +3,13 @@ //! SHA-256 compression with aws-lc's `sha256-armv8` routines, imported by //! `admin/import-aws-lc`: the SHA-256 instructions where the CPU has them, -//! and scalar code otherwise. Neither is formally verified: their -//! correctness rests on their use and testing in OpenSSL, BoringSSL, and -//! aws-lc, and on rind's tests of each against the other, CAVP, and -//! aws-lc-rs. +//! and scalar code otherwise. +//! +//! rind's HOL Light proof, `proofs/hol-light/aarch64/sha256_block_data_order_hw.ml`, +//! covers the routine for the SHA-256 instructions as rind's build emits it. +//! The scalar routine is not formally verified: its correctness rests on its +//! use and testing in OpenSSL, BoringSSL, and aws-lc, and on rind's tests of +//! it against the other, CAVP, and aws-lc-rs. use super::cpu::HaveCryptoExt; @@ -17,16 +20,36 @@ pub(crate) fn sha256_compress_blocks(state: &mut [u32; 8], blocks: &[u8]) { if blocks.is_empty() { return; } - let (data, num) = (blocks.as_ptr(), blocks.len() / 64); match HaveCryptoExt::check() { - // SAFETY: `blocks` is `num` readable blocks, and the token proves the - // CPU has the SHA-256 instructions. - Some(_) => unsafe { sha256_block_data_order_hw(state, data, num) }, - // SAFETY: `blocks` is `num` readable blocks. - None => unsafe { sha256_block_data_order_nohw(state, data, num) }, + // SAFETY: `blocks` is a whole number of blocks, and not empty. + Some(crypto) => unsafe { compress_hw(crypto, state, blocks) }, + // SAFETY: `blocks` is a whole number of blocks, and not empty. + None => unsafe { compress_nohw(state, blocks) }, } } +/// Compresses `blocks`, a whole number of them, into `state` with the +/// SHA-256 instructions. +/// +/// # Safety +/// +/// `blocks` must hold at least one whole block. +unsafe fn compress_hw(_: HaveCryptoExt, state: &mut [u32; 8], blocks: &[u8]) { + // SAFETY: `blocks` is `len / 64` readable blocks, at least one, and the + // token proves the CPU has the SHA-256 instructions. + unsafe { sha256_block_data_order_hw(state, blocks.as_ptr(), blocks.len() / 64) } +} + +/// As [`compress_hw`], with the scalar routine. +/// +/// # Safety +/// +/// `blocks` must hold at least one whole block. +unsafe fn compress_nohw(state: &mut [u32; 8], blocks: &[u8]) { + // SAFETY: `blocks` is `len / 64` readable blocks, at least one. + unsafe { sha256_block_data_order_nohw(state, blocks.as_ptr(), blocks.len() / 64) } +} + /// Compresses the end of `message`, padded and closed by `length`. // Out of line, as `sha1_compress_padded` is, so `finish_with` inlines. #[inline(never)]