ByteSpecs.lean🔗

Tier 2 · definitions used by the symbolic proof 4 headline theorems depend on it 27 of 60 lines trusted source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Byte-Level SHA-256 and HMAC-SHA256

Pure byte-list specifications of SHA-256 and HMAC-SHA256 parameterized by a 64-byte block compression function F.

@[expose] public section

namespace ByteSpecs

abbrev ShaStateL26–27 ↗#

SHA-256 chaining state: eight 32-bit words H₀ … H₇.

abbrev ShaState := List.Vector (BitVec 32) 8

def sha256IVL29–32 ↗#

FIPS 180-4 §5.3.3 initial hash value for SHA-256.

def sha256IV : ShaState :=
  ⟨[0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a,
    0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19], rfl⟩

def toBEBytesL34–36 ↗#

Big-endian n-byte encoding of x.

def toBEBytes (n : ℕ) {w : ℕ} (x : BitVec w) : List (BitVec 8) :=
  List.ofFn fun j : Fin n => x.extractLsb' (8 * (n - 1 - j.val)) 8

def sha256PadL38–41 ↗#

FIPS 180-4 §5.1.1 message padding to a multiple of 64 bytes.

def sha256Pad (m : List (BitVec 8)) : List (BitVec 8) :=
  m ++ [0x80] ++ List.replicate ((119 - m.length % 64) % 64) 0 ++
    toBEBytes 8 (BitVec.ofNat 64 (8 * m.length))

def chunks64L43–45 ↗#

Splits bs into 64-byte blocks, dropping any trailing partial block.

def chunks64 (bs : List (BitVec 8)) : List (List (BitVec 8)) :=
  List.ofFn fun i : Fin (bs.length / 64) => (bs.drop (64 * i.val)).take 64

def sha256WithL47–50 ↗#

SHA-256 of m under compression function F.

def sha256With (F : ShaState → List (BitVec 8) → ShaState) (m : List (BitVec 8)) :
    List (BitVec 8) :=
  ((chunks64 (sha256Pad m)).foldl F sha256IV).toList.flatMap (toBEBytes 4)

def hmacWithL52–61 ↗#

RFC 2104 HMAC-SHA256 under compression function F.

def hmacWith (F : ShaState → List (BitVec 8) → ShaState) (k m : List (BitVec 8)) :
    List (BitVec 8) :=
  let k' := if 64 < k.length then sha256With F k else k
  let k₀ := k' ++ List.replicate (64 - k'.length) 0
  let inner := sha256With F (k₀.map (· ^^^ 0x36) ++ m)
  sha256With F (k₀.map (· ^^^ 0x5c) ++ inner)

end ByteSpecs