Cryptography · 8 min
Hash a message with SHA-256
SHA-256 produces 256 bits, commonly written as 64 hexadecimal characters. This file includes a small Lean implementation, so it runs with the existing browser compiler and requires no additional library download.
Edit message at the top of the file, then run main. SHA256.digest first encodes the string as UTF-8 bytes. A different encoding, an extra space, or a newline changes those bytes and usually changes the digest.
To detect changes, compare the digest with a reference received through a trusted channel. A hash does not encrypt the message, and an attacker who can replace both the message and the reference can defeat this comparison.
The implementation is educational and has reference-vector tests. Those tests do not prove its correctness for every input. The array and bitwise examples explain the syntax used in the implementation.
Exercise
Change message to "Lean" and run the program. The implementation below can stay as it is.
Open exercise in editordef message : String := "abc"
-- 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
def main : IO Unit := IO.println (SHA256.digest message)
Hint
Only the string on the first line needs changing. Then try "Lean" followed by a newline as a separate experiment.
Solution
def message : String := "Lean"
-- 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
def main : IO Unit := IO.println (SHA256.digest message)