Cryptography

SHA-256 without extra libraries

Compute SHA-256 digests using the implementation included in this file.

-- A self-contained educational implementation of SHA-256.
-- Specification: FIPS 180-4, sections 4.1.2, 4.2.2, 5, and 6.2.
-- Uses only Lean core. Tested, but not a formally verified crypto library.
namespace SHA256

-- UInt32 addition wraps modulo 2^32, as required by SHA-256.
private def rotateRight (x n : UInt32) : UInt32 :=
  (x >>> n) ||| (x <<< (32 - n))

private def constants : Array UInt32 := #[
  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]

private def initial : Array UInt32 := #[
  0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a,
  0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19]

private def pad (input : ByteArray) : ByteArray := Id.run do
  let bitLength := input.size * 8
  let mut bytes := input.push 0x80
  -- Reserve the final eight bytes of a block for the message length.
  for _ in [0:(64 + 56 - bytes.size % 64) % 64] do
    bytes := bytes.push 0
  for i in [0:8] do
    bytes := bytes.push (UInt8.ofNat (bitLength >>> (8 * (7 - i))))
  return bytes

private def compress (state : Array UInt32) (bytes : ByteArray)
    (offset : Nat) : Array UInt32 := Id.run do
  let mut words : Array UInt32 := #[]
  -- Read sixteen big-endian words from this 64-byte block.
  for i in [0:16] do
    let mut word : UInt32 := 0
    for j in [0:4] do
      word := (word <<< 8) ||| UInt32.ofNat bytes[offset + 4 * i + j]!.toNat
    words := words.push word
  -- Extend the message schedule to sixty-four words.
  for i in [16:64] do
    let x := words[i - 15]!
    let y := words[i - 2]!
    let s0 := rotateRight x 7 ^^^ rotateRight x 18 ^^^ (x >>> 3)
    let s1 := rotateRight y 17 ^^^ rotateRight y 19 ^^^ (y >>> 10)
    words := words.push (words[i - 16]! + s0 + words[i - 7]! + s1)
  let mut working := state
  for i in [0:64] do
    let a := working[0]!; let b := working[1]!
    let c := working[2]!; let d := working[3]!
    let e := working[4]!; let f := working[5]!
    let g := working[6]!; let h := working[7]!
    let big1 := rotateRight e 6 ^^^ rotateRight e 11 ^^^ rotateRight e 25
    let choose := (e &&& f) ^^^ ((~~~e) &&& g)
    let t1 := h + big1 + choose + constants[i]! + words[i]!
    let big0 := rotateRight a 2 ^^^ rotateRight a 13 ^^^ rotateRight a 22
    let majority := (a &&& b) ^^^ (a &&& c) ^^^ (b &&& c)
    working := #[t1 + big0 + majority, a, b, c, d + t1, e, f, g]
  return (List.range 8).toArray.map (fun i => state[i]! + working[i]!)

private def hexWord (word : UInt32) : String :=
  let digits := "0123456789abcdef".toList.toArray
  String.ofList ((List.range 8).map fun i =>
    digits[((word >>> UInt32.ofNat (4 * (7 - i))) &&& 15).toNat]!)

-- Hash UTF-8 bytes and return 64 lowercase hexadecimal characters.
def digest (message : String) : String := Id.run do
  let bytes := pad message.toUTF8
  let mut state := initial
  for block in [0:bytes.size / 64] do
    state := compress state bytes (block * 64)
  return state.foldl (fun text word => text ++ hexWord word) ""

end SHA256

-- Basic usage: change the message passed to SHA256.digest.
def main : IO Unit := do
  IO.println (SHA256.digest "abc")
  IO.println (SHA256.digest "")
  let original := SHA256.digest "abc"
  let unchanged := SHA256.digest "abc"
  let changed := SHA256.digest "abd"
  IO.println s!"Same message: {original == unchanged}"
  IO.println s!"Changed message: {original == changed}"

Explanation

Expected output

Reference only. Run the file to check its actual result.

ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855
Same message: true
Changed message: false

Exercise

Add a newline to "abc" and compare its digest with the original.