LibsignalHmac.lean🔗

Tier 2 · definitions used by the symbolic proof 2 headline theorems depend on it 13 of 52 lines trusted trust banner B2, trusted: definitions used by the statement 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.

SHA-256 Compression Hook and Chaining-State Layout

Trusted: definitions used by the statement. Memory layout of sha2's 8-word little-endian SHA-256 chaining state (shaStateBytes, readShaState) and the extern hook compress256Hook modeling sha2::sha256::compress256(state: &mut [u32; 8], blocks: &[[u8; 64]]) over an abstract compression function F : ShaState → List (BitVec 8) → ShaState. See Computational/docs/TRUSTED_BASE.md.

@[expose] public section

namespace CryptoVerification

namespace LibsignalHmac

open Arm64 ProofLib CryptoGames CryptoGames.HMAC

open CryptoVerification.LibsignalAesCbc (returnToLinkRegister toLEBytes)

def shaStateBytesL35–37 ↗#

The 32 bytes of a chaining state as stored by sha2 ([u32; 8], native LE words).

def shaStateBytes (h : ShaState) : List (BitVec 8) :=
  h.toList.flatMap (toLEBytes 4)

def readShaStateL39–41 ↗#

The chaining state stored at a: 8 LE 32-bit words.

def readShaState (m : Memory) (a : BitVec 64) : ShaState :=
  List.Vector.ofFn fun i : Fin 8 => m.read32 (a + BitVec.ofNat 64 (4 * i.val))

def compress256HookL43–49 ↗#

sha2::sha256::compress256(state = x0, blocks.ptr = x1, blocks.len = x2): with st the 8 LE words at x0 and bs the x2 · 64 bytes at x1, mem[x0 .. x0+32] := shaStateBytes ((chunks64 bs).foldl F st) (all inputs read before writing); pc := lr.

def compress256Hook (F : ShaState → List (BitVec 8) → ShaState) (s : State) : State :=
  let st := readShaState s.mem (s.readReg64 .x0)
  let bs := s.mem.readBytes (s.readReg64 .x1) (64 * (s.readReg64 .x2).toNat)
  returnToLinkRegister (s.setMem (s.mem.writeBytes (s.readReg64 .x0) (shaStateBytes ((chunks64 bs).foldl F st))))

end LibsignalHmac

end CryptoVerification