Add keccak.

Cryptography/Hashes/SHA3/Basic.lean

@@ -425,3 +425,15 @@ def SHA3_384 : HashFunction := HashFunction.ofParams 96 0x06 48
 def SHA3_512 : HashFunction := HashFunction.ofParams 128 0x06 64
 def SHAKE128 : XOF := HashFunction.ofParams 32 0x1f 32
 def SHAKE256 : XOF := HashFunction.ofParams 64 0x1f 64
+
+/-
+Keccak (original, pre-NIST-standardization) hash functions. These use
+the same KECCAK-p[1600,24] permutation and capacities as their SHA-3
+counterparts, but with the original `pad10*1` multi-rate padding
+(delimiter `0x01`) instead of the SHA-3 domain-separated padding
+(`0x06`). Keccak-256 is the variant used by Ethereum.
+-/
+def Keccak_224 : HashFunction := HashFunction.ofParams 56 0x01 28
+def Keccak_256 : HashFunction := HashFunction.ofParams 64 0x01 32
+def Keccak_384 : HashFunction := HashFunction.ofParams 96 0x01 48
+def Keccak_512 : HashFunction := HashFunction.ofParams 128 0x01 64

Cryptography/Hashes/SHA3/test.lean

@@ -167,6 +167,22 @@ def SHA3_512Files :=
   "Cryptography/test/Hashes/SHA3/sha-3bytetestvectors/SHA3_512LongMsg.rsp",
   "Cryptography/test/Hashes/SHA3/sha-3bytetestvectors/SHA3_512Monte.rsp"]
 
+def Keccak_224Files :=
+  ["Cryptography/test/Hashes/SHA3/keccakbytetestvectors/Keccak_224ShortMsg.rsp",
+  "Cryptography/test/Hashes/SHA3/keccakbytetestvectors/Keccak_224LongMsg.rsp"]
+
+def Keccak_256Files :=
+  ["Cryptography/test/Hashes/SHA3/keccakbytetestvectors/Keccak_256ShortMsg.rsp",
+  "Cryptography/test/Hashes/SHA3/keccakbytetestvectors/Keccak_256LongMsg.rsp"]
+
+def Keccak_384Files :=
+  ["Cryptography/test/Hashes/SHA3/keccakbytetestvectors/Keccak_384ShortMsg.rsp",
+  "Cryptography/test/Hashes/SHA3/keccakbytetestvectors/Keccak_384LongMsg.rsp"]
+
+def Keccak_512Files :=
+  ["Cryptography/test/Hashes/SHA3/keccakbytetestvectors/Keccak_512ShortMsg.rsp",
+  "Cryptography/test/Hashes/SHA3/keccakbytetestvectors/Keccak_512LongMsg.rsp"]
+
 def SHAKE128_Files :=
   ["Cryptography/test/Hashes/SHA3/shakebytetestvectors/SHAKE128ShortMsg.rsp",
   "Cryptography/test/Hashes/SHA3/shakebytetestvectors/SHAKE128LongMsg.rsp",
@@ -217,6 +233,22 @@ def main : IO Unit := do
     let (t,p,f) ← testHashMsg file SHA3_512.hashData
     IO.println s!"{file} total: {t} pass: {p} fail: {f}"
 
+  for file in Keccak_224Files do
+    let (t,p,f) ← testHashMsg file Keccak_224.hashData
+    IO.println s!"{file} total: {t} pass: {p} fail: {f}"
+
+  for file in Keccak_256Files do
+    let (t,p,f) ← testHashMsg file Keccak_256.hashData
+    IO.println s!"{file} total: {t} pass: {p} fail: {f}"
+
+  for file in Keccak_384Files do
+    let (t,p,f) ← testHashMsg file Keccak_384.hashData
+    IO.println s!"{file} total: {t} pass: {p} fail: {f}"
+
+  for file in Keccak_512Files do
+    let (t,p,f) ← testHashMsg file Keccak_512.hashData
+    IO.println s!"{file} total: {t} pass: {p} fail: {f}"
+
   for file in (SHAKE128_Files.take 2 ) do
     let (t,p,f) ← testSpongeMsg file (fun  msg outLen =>
       (SHAKE128.mk |> (SHAKE128.absorb · msg) |> (SHAKE128.squeeze · outLen)).2 )

Cryptography/test/Hashes/SHA3/Readme.md

@@ -1 +1,12 @@
-Test vectors from [NIST](https://csrc.nist.gov/projects/cryptographic-algorithm-validation-program/secure-hashing)
+SHA-3 / SHAKE test vectors (`sha-3bytetestvectors/`, `shakebytetestvectors/`) are from
+[NIST CAVP](https://csrc.nist.gov/projects/cryptographic-algorithm-validation-program/secure-hashing).
+
+Keccak test vectors (`keccakbytetestvectors/`) are derived from the original
+KeccakKAT files published by the Keccak Team (Bertoni, Daemen, Peeters,
+Van Assche), specifically the `ShortMsgKAT_*.txt` and `LongMsgKAT_*.txt`
+files for original-padding Keccak-224/256/384/512. They were obtained
+via the [damaki/libkeccak](https://github.com/damaki/libkeccak) mirror
+under `tests/kat/testvectors/Keccak/`, filtered to byte-aligned message
+lengths and reformatted as NIST CAVS-style `.rsp` files (uppercase MDs
+lowercased, `[L = …]` header added) so the existing `slurpMsgFile`
+parser can read them.